1
Vote

Problem using return value in ensures code expression.

description

The current version of Boogie ("version 2.2.30705.1126") from Codeplex without any command line flags falsely reports an error on the following program.
procedure p() returns ($r: int)
  ensures |{ $bb0: return ($r == 1); }|; // IS BROKEN
  // ensures $r == 1; // WORKS AS EXPECTED
{
  $r := 1;
  return;
}
In a quick investigation with /traceverify it seems that the conversion to passive commands throws out my assignment to $r without propagating it's value to the generated assertion assert $r == 1, as happens in the commented out ensures which does not use code expressions.

comments

mje wrote Jul 31, 2014 at 4:21 PM

The following program also has Boogie falsely reporting an error, for seemingly related reasons.
procedure p()
  ensures |{ var $b: bool; $0: $b := true; goto $1; $1: return $b; }|;
{
}
I suspect this problem is related since the conversion to passive commands again breaks in the presence of code expressions.

mje wrote Aug 7, 2014 at 6:45 PM

I have isolated the causes of these two problems as follows.

The first is due to the fact that the $r in the code expression above is resolved to the formal (out) parameter $r of the procedure p, rather than the $r of the implementation p. These end up being different since the implementation's formals are clones of the procedure's formals, with any where clauses stripped away. Then when it comes time to passify p, the $r used in the code expression does not match the $r entry in the incarnation map from the assignment $r := 1, which is resolved to the formal $r of p's implementation.

I do not understand however the best way to fix this problem.

The second problem is simpler: the Predecessors of blocks arising from code expressions are never computed. Then during passification, the incarnation map of block $0 which maps $b to true is not forwarded to block $1, since its Predecessors list appears empty.

The fix for this problem is simply to ensure that Predecessors is computed for blocks arising from code expressions. While I do not know the ideal place to compute this, I have verified that such a fix works by computing Predessessors in ConditionGeneration::ThreadInCodeExpr.