Opaque block fresh soundness

[keyboardDrummer]

Fixed #6060

What was changed?

Always introduce a new heap variable after an opaque block. I think if no reference 'escapes' the opaque block, then the new heap variable is not needed, and it would be better not to create it, but I couldn't find the machinery to check for the escaping.

How has this been tested?

Added a test for the soundness bug

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[RustanLeino]

Looks good and fixes the soundness issue.

Remarks:

• A possible way to optimize the heap treatment is to look inside the body of the opaque block to see if it ever updates the heap any way. If it does not, then it is safe not to havoc the heap for the use of the opaque block.
• Currently, such syntactic scans are only done in Boogie, during its processing of loops. One way to make use of it would be to translate the opaque block into loop in Boogie. (I'm not sure that's the best idea, but it may be fine.)
• We don't have any mechanism that looks at a spec (e.g., the ensures clause of a method) to see if it would be sound to not modify the heap. It would be good to develop such a mechanism, even it if is rather conservative.

[RustanLeino]

Adding to my remark above, here is an example that shows that trying to avoid advancing the heap is deceptively tricky.

Consider this method spec:

method M(c: C) returns (d: D)
  ensures d.c == c

At first glance, this method seems like a good candidate for not advancing the heap. In other words, it looks like one could model a call to M as one that does not change the heap.

But consider this:

class C { }

class D {
  var c: C
  constructor (c: C)
    ensures this.c == c
  {
    this.c := c;
  }
}

method M(c: C) returns (d: D)
  ensures d.c == c
{
  d := new D(c);
}

method Caller() {
  var c := new C;
  assert forall d: D :: d.c != c;
  var d := M(c);
  assert forall d: D :: d.c != c; // currently does not verify (good!)
}

The first assertion in Caller is provable. It quantifies over all existing D objects. The reason we can prove it is that the newly allocated C object was part of a 1-object allocation and the object returned was not used anywhere before.
But now, if the call to M is modeled as not advancing the heap, then the second assertion would quantify over the same set of existing D objects, so then the asserted condition would still hold. Yet, that contradicts the postcondition we get from M.

In this example, I used a method (with an empty modifies clause and an innocent-looking ensures clause). What I said also applies to an opaque block (with an empty modifies clause and an innocent-looking ensures clause):

opaque
  ensures d.c == c