R31 not properly constrained

[aaronbembenek]

Hi there,

I ran the attached program with BASIL main branch (commit 880b0e4) like so:

./mill run --input dataflow-2a/dataflow-2a.adt --relf dataflow-2a/dataflow-2a.relf --spec dataflow-2a/dataflow-2a.spec --output dataflow-2a/dataflow-2a.bpl --analyse --memory-regions dsa --simplify

Boogie rejects the program that BASIL generates. However, I believe that BASIL should generate a program that Boogie accepts. The code that BASIL currently generates never constrains the variable R31 with respect to R31_in; both R31 and R31_in are used to access the same part of stack memory, but there's no way for Boogie to know that these accesses are the same location (which leads to the verification failure).

If we add this line to the beginning of the lmain block, Boogie accepts the program (dataflow-2a-fixed.bpl):

R31 := bvadd64(R31_in, 18446744073709551584bv64); // R31 := R31_in - 32

Note that Boogie also rejects the program generated by BASIL without using the --analyse --memory-regions dsa --simplify flags (although I haven't dug into whether the root cause is the same).

Thanks!

dataflow-2a.zip