Incomplete map expressions in the Boogie output

[junkil-park]

The current version of Move Prover is not compatible with Boogie version 2.14.0 (and later). It seems that, after This PR, Boogie strictly initializes model states and so outputs additional information like model states. Below is a diff of the output of boogie 2.13.4 and boogie 2.14.0.

The newly added map entries (highlighted in green in the screen shots below) have no "value" parts (e.g., the right-hand side of -> is missing in the expression $abort_code ->). I am wondering if this is expected behavior of Boogie? If so, does it mean that the variable $abort_code can have any value? Or, could it be a bug of Boogie?

[shazqadeer]

It is certainly possible for an SMT solver to return a partial model where not all values are filled in. Sometimes, even a partial model is enough to justify the satisfiability of a formula. It looks like this is happening for the model being returned in your problem. It also seems that the behavior of Boogie changed. Earlier, if the assignment for a variable was unavailable, it was not being mentioned but now it is being mentioned with a missing value after the ->. Regardless, it seems that for the particular problem in your issue, $abort_code and $abort_flag could have any value without compromising the justification of the counterexample.

[junkil-park]

Thank you @shazqadeer ! The output of the newer version contains " STATE ... END_STATE" inside of "MODEL". What's "STATE" and how is it different from "MODEL"?

[shazqadeer]

I don't know.

@keyboardDrummer ?

[keyboardDrummer]

I don't have much background on this, but I think we can see from the tests what the difference between state and model is. the program https://github.com/boogie-org/boogie/blob/master/Test/test15/CaptureState.bpl and its model output https://github.com/boogie-org/boogie/blob/master/Test/test15/CaptureState.bpl.expect provide a good example.

procedure P(this: Ref, x: int, y: int) returns (r: int)
  requires 118 <= 3 * x && 4 * x < 163 && Heap[this, F] * 5 == -x;  // make output deterministic
  ensures 0 <= r;
{
  var m: int;

  assume {:captureState "top"} true;

  m := Heap[this, F];
  if (0 <= x) {
    assume {:captureState "then"} true;
    m := m + 1;
    assume {:captureState "postUpdate0"} true;
  } else {
    assume {:captureState "else"} true;
    m := (m + y) * (m + y);
    assume {:captureState "postUpdate1"} true;
  }
  r := m + m;
  m := 7;
  assume {:captureState "end"} true;
}

You can see the model captures the value of variables, and for functions, captures what inputs map to what outputs. However, for some variables the model doesn't contain values, namely for variables that are locals in an implementation that are re-assigned using :=. For these variables, the model contains the versions of the variable that exist in SSA form, and each of those is assigned a value, like for the variable m:

m -> 
m@0 -> (- 8)
m@1 -> (- 7)
m@2 -> 0
m@3 -> (- 7)

Boogie also allows placing statements of the form assume {:captureState "then"} true;. These create a *** STATE ... *** END_STATE entry inside of MODEL. That entry contains a mapping of variables to values, even for variables that were assigned to. The chosen value of a variable is the one that was logically assigned to it at the position where the assume {:captureState "then"} true; is located:

*** STATE <initial>
  Heap -> |T@[Ref,FieldName]Int!val!0|
  m -> 
  r -> 
  this -> T@Ref!val!0
  x -> 40
  y -> 0
*** END_STATE
*** STATE top
*** END_STATE
*** STATE then
  m -> (- 8)
*** END_STATE
*** STATE postUpdate0
  m -> (- 7)
*** END_STATE
*** STATE end
  m -> 7
  r -> (- 14)
*** END_STATE

@junkil-park I'm not sure why the variables without values in your model don't have them. I'm guessing that at least like @shazqadeer said those variables aren't relevant to the model, but then it seems confusing to include them in the print.

[junkil-park]

Thank you for your explanation, @shazqadeer, @keyboardDrummer. That really helps!