Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Test Generation] Fix bug in function to function-by-method transformation #4067

Merged
merged 3 commits into from
May 25, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 21 additions & 0 deletions Source/DafnyTestGeneration.Test/Various.cs
Original file line number Diff line number Diff line change
Expand Up @@ -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();
}

}
}
7 changes: 4 additions & 3 deletions Source/DafnyTestGeneration/Utils.cs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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 });
}
}
Expand Down
1 change: 1 addition & 0 deletions docs/dev/4067.fix
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