Closure with effects

[EmilyOng]

This is an example of failed entailment with closures.

let closure_with_effects ()
(*@ ex i; ex j; ens i->2*j->4 @*)
= let i = ref 1 in
  let j = ref 2 in
  let f () =
    j := !j + 2;
    i := !i + 1 in
  f ()

Interestingly, this example passes

We switch `i` and `j`'s let bindings. ```ocaml let closure_with_effects () (*@ ex i; ex j; ens i->2*j->4 @*) = let j = ref 2 in let i = ref 1 in let f () = j := !j + 2; i := !i + 1 in f () ``` Or, we can switch the order in which `i` and `j` are updated: ```ocaml let closure_with_effects () (*@ ex i; ex j; ens i->2*j->4 @*) = let i = ref 1 in let j = ref 2 in let f () = i := !i + 1; j := !j + 2 in f () ```

Tracing

In the normalization step:

normalize step | _1182
----------------------
ex v22 v24 v25 v26 v41 v42 v43 v44;
req emp;
Norm(
    v26->1*v25->2
    /\ v24=lambda(\v1 v21 -> ex v10 v11 v13 v14 v15 v9; req v25->v9*v26->v13; Norm(v25->v11*v26->v15/\v11=v9+2/\v15=v13+1/\v21=()))
)

The following deletion from heap list occurs:

delete from heap list | _1183
# Here, v25 and v26 pass the same_loc check since both are in the list of existentials and may_be_equal is always true
# But, (t1=1) != (t2=v44)
(v26, 1) -* [(v25, v44); (v26, v42)] = ([(v26, v42)], 1=v44)
ex [v22; v24; v25; v26; v41; v42; v43; v44]

delete from heap list | _1184
# Similarly, 2 != v42
(v25, 2) -* [(v26, v42)] = ([], 2=v42)
ex [v22; v24; v25; v26; v41; v42; v43; v44]

delete from heap list | _1185
(v25, v44) -* [(v26, 1); (v25, 2)] = ([(v25, 2)], v44=1)
ex [v22; v24; v25; v26; v41; v42; v43; v44]

delete from heap list | _1186
(v26, v42) -* [(v25, 2)] = ([], v42=2)
ex [v22; v24; v25; v26; v41; v42; v43; v44]

This leads to inferring(?) v44=1 and v42=2, which fails both VC for postcondition of normal stage:

VC for postcondition of normal stage | _1391
--------------------------------------------
# Should be v44=2, v42=1?
1=v44/\2=v42/\v44=1/\v42=2/\v41=v44+2/\v43=v42+1/\res=()/\1=v44/\2=v42 => ex i,j. 4=v43/\2=v41
...
z3 sat check | _1398 <-_1397
satisfiable
...
valid? | _1400
false

VC for postcondition of normal stage | _1476
--------------------------------------------
1=v44/\2=v42/\v44=1/\v42=2/\v41=v44+2/\v43=v42+1/\res=()/\1=v44/\2=v42 => ex i,j. 4=v41/\2=v43
...
z3 sat check | _1483 <-_1482
satisfiable
...
valid? | _1485
false

This entailment can temporarily "pass" if we make the tweak in same_loc (code).

let may_be_equal _assumptions _x _y =
  # Check what this means if the formula is satisfiable
  (* proving at this point is not effective as we may not be able to prove unsat, but later the constraints may be violated, resulting in false anyway. returning true here is just the worst case version of that *)
  true
...
let same_loc =
  # Check if two existential instantiations point to the same location
  let exists_eq =
    List.mem x existential && List.mem y existential
      # may_be_equal is always true
      && may_be_equal True (Var x) (Var y)
    in

-   String.equal x y || exists_eq
+   String.equal x y