fix: Use {:test} and {:synthesize} in automatically generated tests

RELEASE_NOTES.md

@@ -8,6 +8,7 @@
 - fix: Prevent the language server from crashing and not responding on resolution or ghost diagnostics errors (https://github.com/dafny-lang/dafny/pull/2080)
 - fix: Correctly specify the type of the receiver parameter when translating tail-recursive member functions to C# (https://github.com/dafny-lang/dafny/pull/2205)
 - fix: Added support for type parameters in automatically generated tests (https://github.com/dafny-lang/dafny/pull/2227)
+- fix: Methods produced by the test generation code can now be compiled directly to the C#'s XUnit tests (https://github.com/dafny-lang/dafny/pull/2269)
 
 # 3.6.0
 

Source/DafnyTestGeneration/Main.cs

@@ -106,6 +106,7 @@ public static async IAsyncEnumerable<TestMethod> GetTestMethodsForProgram(
  /// </summary>
  public static async IAsyncEnumerable<string> GetTestClassForProgram(string sourceFile) {
 
+ TestMethod.ClearTypesToSynthesize();
  var source = new StreamReader(sourceFile).ReadToEnd();
  var program = Utils.Parse(source, sourceFile);
  if (program == null) {
@@ -128,6 +129,8 @@ string EscapeDafnyStringLiteral(string str) {
  yield return method.ToString();
  }
 
+ yield return TestMethod.EmitSynthesizeMethods();
+
  yield return "}";
  }
  }

Source/DafnyTestGeneration/README.md

@@ -5,7 +5,6 @@
 [**Implementation**](#implementation) <br>
 [**How to Generate Tests?**](#how-to-generate-tests) <br>
 [**How to Run Tests?**](#how-to-run-tests) <br>
-[**Example**](#example) <br>
 [**Dead Code Identification Example**](#dead-code-identification-example)
 
 ## Purpose
@@ -21,9 +20,7 @@ To generate a test that covers a particular basic block or path, we add an asser
 
 While these manipulations could be done with the Dafny source directly, we instead modify the Boogie translation, since it is much easier to work with basic blocks and paths on this lower level.
 
-Objects present an obstacle for test generation since it is not possible to mock objects in Dafny and the prover model does not specify how an object was allocated\constructed. Currently, we require that a test method take any object it needs as an argument. This allows us to compile the test methods to Java or another language where object mocking is possible (see [How to Run Tests?](#how-to-run-tests)).
-
-Even though it is possible to run the tests in this way, we currently provide no oracle against which to compare the result. In the future, it may be possible to generate an oracle directly from the prover model provided that there is no non-determinism in the tested code.
+We currently provide no oracle against which to compare the result. In the future, it may be possible to generate an oracle directly from the prover model provided that there is no non-determinism in the tested code.
 
 
 ## Implementation
@@ -47,36 +44,6 @@ Even though it is possible to run the tests in this way, we currently provide no
 
 ## How to Run Tests?
 
-To run the tests, you would first need to compile the code to some other language. Once this is done, the main difficulty is to mock the arguments that the test methods take. The following code (to be inserted into the class with the tests) should do the job in Java (you would also need to add `import java.lang.reflect.*;` at the top of the file):
-
-```java
-public static void main(String[] args) throws Exception {
- for (Method method: __default.class.getDeclaredMethods()) {
- if (!method.getName().startsWith("test"))
- continue;
- Object result = method.invoke(null, mockParameters(method));
- String resultString = result == null ? "null" : result.toString();
- System.out.println(method.getName() + " " + resultString);
- }
-}
-
-
-public static Object[] mockParameters(Method method) {
- Object[] parameters = null;;
- try {
- Class<?>[] types = method.getParameterTypes();
- parameters = new Object[types.length];
- for (int i = 0; i < types.length; i++)
- parameters[i] = types[i].getConstructor().newInstance();
- } catch (Exception e) {
- e.printStackTrace();
- }
- return parameters;
-}
-```
-
-## Example
-
 Suppose you have a file called `object.dfy` with the following code:
 ```dafny
 module M {
@@ -93,7 +60,7 @@ module M {
  }
 }
 ```
-The tests can be run like this (in this particular case, `/definiteAssignment:3` adds proof obligations that cause the Dafny to Boogie translator to emit an implementation for the target method):
+The tests can be generated like this:
 
 ```dafny /definiteAssignment:3 /generateTestMode:Block object.dfy ```
 
@@ -102,33 +69,38 @@ Dafny will give the following list of tests as output (tabulation added manually
 include "object.dfy"
 module objectUnitTests {
  import M
- method test0(v0:M.Value) returns (r0:int) modifies v0 {
+ method {:test} test0() {
+ var v0 := getFreshMValue();
  v0.v := -39;
- r0 := M.compareToZero(v0);
+ var r0 := M.compareToZero(v0);
  }
- method test1(v0:M.Value) returns (r0:int) modifies v0 {
+ method {:test} test1() {
+ var v0 := getFreshMValue();
  v0.v := 39;
- r0 := M.compareToZero(v0);
+ var r0 := M.compareToZero(v0);
  }
- method test2(v0:M.Value) returns (r0:int) modifies v0 {
+ method {:test} test2() {
+ var v0 := getFreshMValue();
  v0.v := 0;
- r0 := M.compareToZero(v0);
+ var r0 := M.compareToZero(v0);
  }
+ method {:synthesize} getFreshMValue() 
+ returns (o:M.Value) 
+ ensures fresh(o)
 }
 ```
 
-Saving these tests in a file `test.dfy` and compiling the code to Java using `dafny /compileTarget:java test.dfy` produces directory `test-java`. The tests are located in `test-java/objectUnitTests_Compile/__default.java`. To run the tests, it is first necessary to add the code shown [above](#how-to-run-tests) to the file with the tests. The code can then be compiled to bytecode using:
+Saving these tests in a file `test.dfy` and compiling the code to C# using `dafny /compileVerbose:1 /compile:0 /spillTargetCode:3 /noVerify test.dfy` produces a file `test.cs`. 
 
-```
-javac -cp PATH_TO_DafnyRuntime.jar:test-java test-java/objectUnitTests_Compile/__default.java
-```
+You can then run `dotnet test YourCSProjectFile.csproj` to execute the tests.
 
-Finally, running the code with `java -cp PATH_TO_DafnyRuntime.jar:test-java objectUnitTests_Compile/__default` yields:
+Note that your `.csproj` file must include `xunit` and `Moq` libraries: 
 
 ```
-test1 1
-test0 -1
-test2 0
+<ItemGroup>
+ <PackageReference Include="xunit" Version="2.4.1" />
+ <PackageReference Include="Moq" Version="4.16.1" />
+</ItemGroup>
 ```
 
 ## Dead Code Identification Example

Source/DafnyTestGeneration/TestMethod.cs

@@ -24,11 +24,15 @@ public class TestMethod {
  // values of the arguments to be passed to the method call
  public readonly List<string> ArgValues;
  // number of type parameters for the method (all will be set to defaultType)
- public readonly int NOfTypeParams = 0;
+ public readonly int NOfTypeParams;
  // default type to replace any type variable with
  private readonly DafnyModelType defaultType = new("int");
  // the DafnyModel that describes the inputs to this test method
- private DafnyModel dafnyModel;
+ private readonly DafnyModel dafnyModel;
+
+ // Set of all types for which a {:synthesize} - annotated method is needed
+ // These methods are used to get fresh instances of the corresponding types
+ private static readonly HashSet<DafnyModelType> TypesToSynthesize = new();
 
  public TestMethod(DafnyInfo dafnyInfo, string log) {
  DafnyInfo = dafnyInfo;
@@ -41,6 +45,32 @@ public TestMethod(DafnyInfo dafnyInfo, string log) {
  ArgValues = ExtractInputs(dafnyModel.States.First(), argumentNames, typeNames);
  }
 
+ public static void ClearTypesToSynthesize() {
+ TypesToSynthesize.Clear();
+ }
+
+ /// <summary>
+ /// Returns the name given to a {:synthesize} - annotated method that
+ /// returns a value of certain type
+ /// </summary>
+ private static string GetSynthesizeMethodName(DafnyModelType typ) {
+ return "getFresh" + Regex.Replace(typ.ToString(), "[^a-zA-Z]", "");
+ }
+
+ /// <summary>
+ /// Returns a string that contains all the {:synthesize} annotated methods
+ /// necessary to compile the tests
+ /// </summary>
+ public static string EmitSynthesizeMethods() {
+ var result = "";
+ foreach (var typ in TypesToSynthesize) {
+ var methodName = GetSynthesizeMethodName(typ);
+ result += $"\nmethod {{:synthesize}} {methodName}() " +
+ $"returns (o:{typ}) ensures fresh(o)";
+ }
+ return result;
+ }
+
  /// <summary>
  /// Extract values that certain elements have at a certain state in the
  /// model.
@@ -153,6 +183,7 @@ private string ExtractVariable(DafnyModelVariable variable) {
  var varId = $"v{ObjectsToMock.Count}";
  var dafnyType = variableType.GetNonNullable().InDafnyFormat();
  ObjectsToMock.Add(new(varId, dafnyType));
+ TypesToSynthesize.Add(dafnyType);
  mockedVarId[variable] = varId;
  foreach (var filedName in variable.children.Keys) {
  if (variable.children[filedName].Count != 1) {
@@ -191,6 +222,7 @@ private string GetDefaultValue(DafnyModelType type) {
  // this should only be reached if the type is non-nullable
  var varId = $"v{ObjectsToMock.Count}";
  ObjectsToMock.Add(new(varId, type));
+ TypesToSynthesize.Add(type);
  return varId;
  }
 
@@ -227,20 +259,16 @@ private List<string> TestMethodLines() {
  List<string> lines = new();
 
  // test method parameters and declaration:
- var parameters = string.Join(", ", ObjectsToMock
- .Select(kVPair => $"{kVPair.id}:{kVPair.type}"));
+ var mockedLines = ObjectsToMock
+ .Select(kVPair => $"var {kVPair.id} := " +
+ $"{GetSynthesizeMethodName(kVPair.type)}();");
  var returnParNames = new List<string>();
  for (var i = 0; i < DafnyInfo.GetReturnTypes(MethodName).Count; i++) {
  returnParNames.Add("r" + i);
  }
 
- var returnsDeclaration = string.Join(", ",
- Enumerable.Range(0, returnParNames.Count).Select(i =>
- $"{returnParNames[i]}:{DafnyInfo.GetReturnTypes(MethodName)[i]}"));
- var modifiesClause = string.Join("",
- ObjectsToMock.Select(i => $" modifies {i.id}"));
- lines.Add($"method test{id}({parameters}) " +
- $"returns ({returnsDeclaration}) {modifiesClause} {{");
+ lines.Add($"method {{:test}} test{id}() {{");
+ lines.AddRange(mockedLines);
 
  // assignments necessary to set up the test case:
  foreach (var assignment in Assignments) {
@@ -266,7 +294,7 @@ private List<string> TestMethodLines() {
 
  var returnValues = "";
  if (returnParNames.Count != 0) {
- returnValues = string.Join(", ", returnParNames) + " := ";
+ returnValues = "var " + string.Join(", ", returnParNames) + " := ";
  }
 
  lines.Add(returnValues + methodCall);

Test/DafnyTestGeneration/TestGeneration.csproj

@@ -0,0 +1,12 @@
+<?xml version="1.0" encoding="utf-8"?>
+<Project Sdk="Microsoft.NET.Sdk">
+ <PropertyGroup>
+ <TargetFramework>net6.0</TargetFramework>
+ </PropertyGroup>
+ <ItemGroup>
+ <PackageReference Include="Microsoft.NET.Test.Sdk" Version="16.10.0" />
+ <PackageReference Include="xunit" Version="2.4.1" />
+ <PackageReference Include="Moq" Version="4.16.1" />
+ <PackageReference Include="xunit.runner.visualstudio" Version="2.4.3" />
+ </ItemGroup>
+</Project>

Test/DafnyTestGeneration/TestGeneration.dfy

@@ -1,18 +1,11 @@
 // Generating tests:
 // RUN: cp %S/TestGeneration.dfy %t.dfy
 // RUN: %dafny /definiteAssignment:3 /generateTestMode:Block %t.dfy > %t-tests.dfy
+// RUN: %dafny_0 /compileVerbose:1 /compile:0 /spillTargetCode:3 /noVerify "%t-tests.dfy" > "%t"
+// RUN: dotnet test -v:q -noLogo %S >> %t || true
 
-// Compiling test to java:
-// RUN: %dafny /compileTarget:java /out:%t-tests.dfy %t-tests.dfy
-
-// Adding reflection code that allows running the tests:
-// RUN: perl -pe 's|import M_Compile.*;|`cat %S/import.txt`|ge' -i %t-tests-java/TestGenerationUnitTests_Compile/__default.java
-// RUN: perl -pe 's|public class __default \{|`cat %S/reflectionCode.txt`|ge' -i %t-tests-java/TestGenerationUnitTests_Compile/__default.java
-
-// Compiling to bytecode and running the tests
-// RUN: javac -cp %t-tests-java:%binaryDir/DafnyRuntime.jar %t-tests-java/TestGenerationUnitTests_Compile/__default.java
-// RUN: java -cp %t-tests-java:%binaryDir/DafnyRuntime.jar TestGenerationUnitTests_Compile/__default > %t
-// RUN: %diff "%s.expect" "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK: .*Passed! - Failed: 0, Passed: 3, Skipped: 0, Total: 3*
 
 module M {
  class Value {