Fix: (soundness issue) Twostate predicate now check if their not new …

…arguments are allocated in the previous heap (dafny-lang#5142)

This PR fixes dafny-lang#4844 according to Rustan's remarks

Fixes dafny-lang#5132 as well by
modifying the error message to be more explicit about the possibilities

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

---------

Co-authored-by: Rustan Leino <leino@amazon.com>

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs

@@ -711,7 +711,10 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
                     Bpl.Expr wh = GetWhereClause(ee.tok, etran.TrExpr(ee), ee.Type, etran.OldAt(e.AtLabel), ISALLOC, true);
                     if (wh != null) {
                       var pIdx = e.Args.Count == 1 ? "" : " at index " + i;
-                      var desc = new PODesc.IsAllocated($"argument{pIdx} ('{formal.Name}')", "in the two-state function's previous state");
+                      var desc = new PODesc.IsAllocated($"argument{pIdx} for parameter '{formal.Name}'",
+                        "in the two-state function's previous state" +
+                          PODesc.IsAllocated.HelperFormal(formal)
+                        );
                       builder.Add(Assert(GetToken(ee), wh, desc));
                     }
                   }

Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs

@@ -477,7 +477,7 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
       olderInParams.Add(bv);
       args.Add(formal);
       // add well-typedness conjunct to antecedent
-      Bpl.Expr wh = GetWhereClause(p.tok, formal, p.Type, p.IsOld ? etran.Old : etran, NOALLOC);
+      Bpl.Expr wh = GetWhereClause(p.tok, formal, p.Type, p.IsOld ? etran.Old : etran, ISALLOC);
       if (wh != null) { ante = BplAnd(ante, wh); }
       wh = GetWhereClause(p.tok, formal, p.Type, p.IsOld ? etranHeap.Old : etranHeap, ISALLOC);
       if (wh != null) { anteIsAlloc = BplAnd(anteIsAlloc, wh); }

Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs

@@ -1668,7 +1668,9 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
           if (formal.IsOld) {
             var dafnyFormalIdExpr = new IdentifierExpr(formal.tok, formal);
             var pIdx = m.Ins.Count == 1 ? "" : " at index " + index;
-            var desc = new PODesc.IsAllocated($"parameter{pIdx} ('{formal.Name}')", "in the two-state lemma's previous state");
+            var desc = new PODesc.IsAllocated($"argument{pIdx} for parameter '{formal.Name}'",
+              "in the two-state lemma's previous state" +
+              PODesc.IsAllocated.HelperFormal(formal));
             var require = Requires(formal.tok, false, MkIsAlloc(etran.TrExpr(dafnyFormalIdExpr), formal.Type, prevHeap),
               desc.FailureDescription, desc.SuccessDescription, null);
             require.Description = desc;

Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs

@@ -1903,7 +1903,10 @@ void ProcessCallStmt(CallStmt cs, Dictionary<TypeParameter, Type> tySubst, Bpl.E
             Bpl.Expr wh = GetWhereClause(ee.tok, etran.TrExpr(ee), ee.Type, etran.OldAt(atLabel), ISALLOC, true);
             if (wh != null) {
               var pIdx = Args.Count == 1 ? "" : " at index " + i;
-              var desc = new PODesc.IsAllocated($"parameter{pIdx} ('{formal.Name}')", "in the two-state lemma's previous state");
+              var desc = new PODesc.IsAllocated($"argument{pIdx} for parameter '{formal.Name}'",
+                "in the two-state lemma's previous state" +
+                PODesc.IsAllocated.HelperFormal(formal)
+                );
               builder.Add(Assert(ee.tok, wh, desc));
             }
           }

Source/DafnyCore/Verifier/ProofObligationDescription.cs

@@ -260,7 +260,7 @@ public class IsAllocated : ProofObligationDescription {
     $"{PluralSuccess}{what} is always allocated{WhenSuffix}";
 
   public override string FailureDescription =>
-    $"{PluralFailure}{what} might not be allocated{WhenSuffix}";
+    $"{PluralFailure}{what} could not be proved to be allocated{WhenSuffix}";
 
   public override string ShortDescription => $"{what} allocated";
 
@@ -271,6 +271,11 @@ public class IsAllocated : ProofObligationDescription {
   private string PluralSuccess => plural ? "each " : "";
   private string PluralFailure => plural ? "some " : "";
 
+  public static string HelperFormal(Formal formal) {
+    return $" -- if you add 'new' before the parameter declaration, like 'new {formal.Name}: {formal.Type.ToString()}',"
+           + " arguments can refer to expressions possibly unallocated in the previous state";
+  }
+
   public IsAllocated(string what, string when, bool plural = false) {
     this.what = what;
     this.when = when;

Source/DafnyDriver.Test/LanguageServerProcessTest.cs

@@ -79,7 +79,7 @@ public async Task LanguageServerStaysAliveIfParentDiesButNoParentIdWasProvided()
       }
     }
 
-    [Fact(Timeout = 10_000)]
+    [Fact(Timeout = 20_000)]
     public async Task LanguageServerShutsDownIfParentDies() {
       var process = await StartLanguageServerRunnerProcess();
 

Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs

@@ -36,7 +36,7 @@ protected override Task SetUp(Action<DafnyOptions> modifyOptions) {
   /// </summary>
   [Fact]
   public async Task QuickEditsInLargeFile() {
-    string GetLineContent(int index) => $"method Foo{index}() {{ assume false; }}";
+    string GetLineContent(int index) => $"method Foo{index}() {{ assume {{:axiom}} false; }}";
     var contentBuilder = new StringBuilder();
     for (int lineNumber = 0; lineNumber < 1000; lineNumber++) {
       contentBuilder.AppendLine(GetLineContent(lineNumber));

Source/DafnyPipeline.Test/ProverLogStability.cs

@@ -86,6 +86,8 @@ public ProverLogStabilityTest(ITestOutputHelper testOutputHelper) {
       this.testOutputHelper = testOutputHelper;
     }
 
+    private static bool updateProverLog = false; // Should always be false in committed code
+
     /// <summary>
     /// This test is meant to detect _any_ changes in Dafny's verification behavior.
     /// Dafny's verification is powered by an SMT solver. For difficult inputs, such solvers may change their behavior,
@@ -97,12 +99,14 @@ public ProverLogStabilityTest(ITestOutputHelper testOutputHelper) {
     ///
     /// If this test fails, that means a change was made to Dafny that changes the SMT input it sends.
     /// If this was intentional, you should update this test's expect file with the new SMT input.
+    /// To do so, set the static field above "updateProverLog" to true, run this test, set the flag back to false, and
+    /// run the test again to verify it works.
     /// The git history of updates to this test allows us to easily see when Dafny's verification has changed.
     ///
     /// If you make a change to Dafny verification and this test does not fail, then likely the Dafny code in the test
     /// does not sufficiently cover the language to detect your change. In that case, please update the test so it does.
     /// 
-    /// Note that this test does not detect changes in DafnyPrelude.bplf
+    /// Note that this test does not detect changes in DafnyPrelude.bpl
     /// 
     /// </summary>
     [Fact]
@@ -111,8 +115,16 @@ public async Task ProverLogRegression() {
 
       var filePath = Path.Combine(Directory.GetCurrentDirectory(), "expectedProverLog.smt2");
       var expectation = await File.ReadAllTextAsync(filePath);
+      expectation = expectation.Replace("\r", "");
       var regularProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, originalProgram));
-      Assert.Equal(expectation.Replace("\r", ""), regularProverLog.Replace("\r", ""));
+      regularProverLog = regularProverLog.Replace("\r", "");
+      if (updateProverLog) {
+        var path = Path.GetFullPath(filePath).Replace("bin" + Path.DirectorySeparatorChar + "Debug" + Path.DirectorySeparatorChar + "net6.0" + Path.DirectorySeparatorChar, "");
+        await File.WriteAllTextAsync(path, regularProverLog);
+        await Console.Out.WriteLineAsync("Updated prover log file at " + path);
+      } else {
+        Assert.Equal(expectation, regularProverLog);
+      }
     }
 
     private async Task<string> GetProverLogForProgramAsync(DafnyOptions options, IEnumerable<Microsoft.Boogie.Program> boogiePrograms) {