Inconsistent variable reference between procedure spec and body

[aaronbembenek]

Hi there,

I ran the attached program through Basil (commit 95d40e0):

$ cat global/global.c
void __VERIFIER_assert(int e) {
        while (!e) ;
}

int x = 42;

int main() {
        __VERIFIER_assert(x == 42);
        return 0;
}
$ ./mill run --input global/global.-O0.gts --relf global/global.-O0.relf --output global/global.-O0.bpl --simplify --dsa=  --dsa-split --dsa-checks --memory-transform --noif

Basil produced this Boogie code:

procedure p$main_4196204(#R0_in: bv64, #R1_in: bv64, #R29_in: bv64, #R30_in: bv64, #R31_in: bv64, #_PC_in: bv64) returns (#R0_out: bv64, #R29_out: bv64);
  modifies $Global_4325416_4325420;
  free requires (memory_load64_le($mem, 4325400bv64) == 0bv64);
  free requires (memory_load64_le($mem, 4325408bv64) == 0bv64);
  free requires (memory_load8_le($mem, 4325416bv64) == 42bv8); // <-- Reference to global variable `x`
  free requires (memory_load8_le($mem, 4325417bv64) == 0bv8);
  free requires (memory_load8_le($mem, 4325418bv64) == 0bv8);
  free requires (memory_load8_le($mem, 4325419bv64) == 0bv8);
  free requires (memory_load32_le($mem, 4196272bv64) == 131073bv32);

implementation p$main_4196204(#R0_in: bv64, #R1_in: bv64, #R29_in: bv64, #R30_in: bv64, #R31_in: bv64, #_PC_in: bv64) returns (#R0_out: bv64, #R29_out: bv64)
{
  var #Exp14__5_27_1: bv32;
  var #Exp16__5_24_1: bv64;
  var #Exp18__5_25_1: bv64;
  var #R0_9: bv64;
  var #Stack_n16_n8: bv64;
  var #Stack_n8_0: bv64;
  b#main_entry:
    #Stack_n16_n8 := #R29_in;
    #Stack_n8_0 := #R30_in;
    #Exp14__5_27_1 := $Global_4325416_4325420; // <-- Reference to global variable `x`
    goto b#phi_3, b#phi_4;

As I've annotated in this output, the global variable x is referenced differently in the spec than in the procedure body. This means that the program fails to verify, even though it shouldn't.

Thanks!

global.zip

[l-kent]

This is part of the same core problem as #531 - the --memory-transform flag currently ignores everything to do with specifications, which causes inconsistencies. I've been working on addressing that recently but it's still a work in progress as it requires some substantial changes.

[aaronbembenek]

Okay, no problem - I think I should be able to work around this for now!