DSA: Inconsistent regions for global variable

[aaronbembenek]

Hi there,

I tried running BASIL (commit a7c77db) on this program (bad-regions/clasloc.c):

#define LO 0
#define HI 1

int z;

int source() {
    z = LO;
    return 42;
}

int main() {
    return source();
}

I ran BASIL like so:

./mill run --input bad-regions/clasloc.adt --relf bad-regions/clasloc.relf --spec bad-regions/clasloc.spec --output bad-regions/clasloc.bpl --analyse --memory-regions dsa --simplify

Here's the spec:

Globals:
z: bv32

L: z -> true

Subroutine: source
Ensures: Gamma_R0_out <==> z != 1bv32

BASIL produced the following Boogie code (excerpted):

const {:extern} $z_addr: bv64;
axiom ($z_addr == 131092bv64);

...

procedure source_1812() returns (R0_out: bv64, Gamma_R0_out: bool);
  modifies Gamma_mem_1, Gamma_mem_2, mem_1, mem_2;
  // !!! global `z` accessed via `mem_2`
  ensures (Gamma_R0_out <==> (memory_load32_le(mem_2, $z_addr) != 1bv32));

implementation source_1812() returns (R0_out: bv64, Gamma_R0_out: bool)
{
  lsource:
    assume {:captureState "lsource"} true;
    call rely();
    assert (L(131092bv64) ==> true);
    // !!! global `z` accessed via `mem_1`
    mem_1, Gamma_mem_1 := memory_store32_le(mem_1, 131092bv64, 0bv32), gamma_store32(Gamma_mem_1, 131092bv64, true);
    assume {:captureState "%000002f6"} true;
    assert true; //is returning to caller-set R30
    goto source_1812_basil_return;
  source_1812_basil_return:
    assume {:captureState "source_1812_basil_return"} true;
    R0_out := 42bv64;
    Gamma_R0_out := true;
    return;
}

As I noted in my comments, in the precondition of source_1812 the global var z is referenced via mem_2, but in the body it is referenced via mem_1. This means that the procedure does not verify (even though it should).

Thanks!

bad-regions.zip