Fix a soundness issue that could be triggered by calling ensures fres…

[keyboardDrummer]

Fixes #4700

Description

Fix a soundness issue that could be triggered by calling ensures fresh in the post-condition of a constructor.

How has this been tested?

Added a littish test

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

[MikaelMayer]

Wonderful! You totally crushed this soundness issue!

[MikaelMayer]

Oh nice, I see now the soundness issue fix Rustan was talking about. Well done spotting it.

[RustanLeino]

This PR does not completely fix the problem identified by #4700. The PR moves the this parameter from being an in-parameter to being an out-parameter for any Boogie procedure generated from a Dafny constructor. However, it is also necessary to alter the where clause for that parameter.

My comment on #4700 said to remove the $IsAlloc conjunct from that where clause. (This is accomplished by changing the if condition on line 2925 of BoogieGenerator.cs to m is Constructor && kind is MethodTranslationKind.Implementation or MethodTranslationKind.SpecWellformedness.) But more needs to be done.

In my comments on #5136, I said that the entire where clause for this should be removed (for both the Impl$$ procedure and the CheckWellFormed$$ procedure). Instead, the contents of that where clause (which is generated by the GetWhereClause method in the Dafny implementation) should be assumed after the havoc this; that is part of both of these procedures.

So, the full fix of both #4700 and #5136 is to:

• For the Impl$$ and CheckWellFormed$$ procedures generated for a Dafny constructor:
  • Make the this parameter an out-parameter
  • Do not give a where clause for this this parameter
  • In the assumptions that follow the havoc this; (which occurs in the body of both the procedures), add the assumption $Is(this, Tclass._module.Test()) (which can be obtained by calling GetWhereClause). It's okay if the assumed condition also includes the $IsAlloc condition, but that condition is in effect already assumed in the assumptions after the havoc this;.
• No change to the Call$$ procedure is necessary. (It's fine and appropriate for it to use this as an out-parameter with a where clause that includes the $IsAlloc conjunct.)

[keyboardDrummer]

@RustanLeino could you provide a failing test-case, that highlights the changes you describe are still necessary? I trust that your suggestions are correct, but without a test-case I can not validate that, and I'm not sure how to reverse engineer a test-case from what you're describing.