[Test Generation] Fix bug in function to function-by-method transform…

…ation (dafny-lang#4067) This PR fixes a bug in function to function-by-method transformation pass that can lead to parsing errors during test generation. The fix is to use the cloner API instead of copying AST nodes by reference. The PR also includes a test that can catch this bug. <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: Aleksandr Fedchin <[email protected]>
suisui-daigaku · May 25, 2023 · b3045a8 · b3045a8
1 parent df1f683
commit b3045a8
Show file tree

Hide file tree

Showing 3 changed files with 26 additions and 3 deletions.
diff --git a/Source/DafnyTestGeneration.Test/Various.cs b/Source/DafnyTestGeneration.Test/Various.cs
@@ -636,5 +636,26 @@ modifies this
       Assert.True(methods.All(m => m.ToString().Contains("expect instance0.i == 10")));
     }
 
+    /// <summary>
+    /// This test may fail if function to method translation implemented by AddByMethodRewriter
+    /// does not use the cloner to copy the body of the function
+    /// </summary>
+    [Fact]
+    public async Task FunctionToMethodTranslation() {
+      var source = @"
+module M {
+
+  function test(b: bool): bool {
+      assert true by {
+        calc { true; }
+      }
+      true
+  }
+}
+".TrimStart();
+      var program = Utils.Parse(Setup.GetDafnyOptions(output), source);
+      await Main.GetTestMethodsForProgram(program).ToListAsync();
+    }
+
   }
 }
diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs
@@ -128,7 +128,7 @@ public static string GetStringRepresentation(DafnyOptions options, Microsoft.Boo
     }
 
     /// <summary>
-    /// Turns each function-method into a function-by-method.
+    /// Turns each function into a function-by-method.
     /// Copies body of the function into the body of the corresponding method.
     /// </summary>
     private class AddByMethodRewriter : IRewriter {
@@ -174,8 +174,9 @@ private static void AddByMethod(Function func) {
           return;
         }
         var returnStatement = new ReturnStmt(new RangeToken(new Token(), new Token()),
-          new List<AssignmentRhs> { new ExprRhs(func.Body) });
-        func.ByMethodBody = new BlockStmt(new RangeToken(new Token(), new Token()),
+          new List<AssignmentRhs> { new ExprRhs(new Cloner().CloneExpr(func.Body)) });
+        func.ByMethodBody = new BlockStmt(
+          new RangeToken(new Token(), new Token()),
           new List<Statement> { returnStatement });
       }
     }

diff --git a/docs/dev/4067.fix b/docs/dev/4067.fix
@@ -0,0 +1 @@
+Fix function to function-by-method transformation pass in test generation that could previously lead to parsing errors
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		Fix function to function-by-method transformation pass in test generation that could previously lead to parsing errors