fix: Continue to compilation tests after comparing .verifier.expect (d…

…afny-lang#4356)

This PR fixes and changes the behavior of `%testDafnyForEachCompiler`
tests. The bug that is fixed had caused 16 compiler tests in the Dafny
test suite to not run.

Here is a description of the new behavior, where _italicized_ parts
indicate changes from before:

* Verification is expected to go through with a 0 exit code.
* If there is a `.verifier.expect` file, then the actual output is
expected to contain a blank line followed by a line that starts with
`Dafny program verifier`, and this portion of the output will be removed
before comparing the output. The remaining output is compared with the
contents of the `.verifier.expect` file and is expected to match.
* If there is no `.verifier.expect` file, the verifier output minus the
`Dafny program verifier` line (see previous bullet) is expected to be
empty.
* When running the test for each compiler, if the output contains a line
starting with `Dafny program verifier`, then _everything up to and
include that line is removed_ before comparing the output.

This PR adds add test in `Test/metatests`.

Fixes dafny-lang#4355

<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: Robin Salkeld <[email protected]>

Source/TestDafny/MultiBackendTest.cs

@@ -94,33 +94,34 @@ private int ForEachCompiler(ForEachCompilerOptions options) {
     output.WriteLine("Verifying...");
 
     var (exitCode, outputString, error) = RunDafny(options.DafnyCliPath, dafnyArgs);
+    // If there is a .verifier.expect file, then we expect the output to match the .verifier.expect file contents. Otherwise, we
+    // expect the output to be empty.
+    var expectedOutput = "";
+    var expectFileForVerifier = $"{options.TestFile}.verifier.expect";
+    if (File.Exists(expectFileForVerifier)) {
+      expectedOutput = File.ReadAllText(expectFileForVerifier);
+    }
+    // Chop off the "Dafny program verifier finished with..." trailer
+    var trailer = new Regex("\r?\nDafny program verifier[^\r\n]*\r?\n").Match(outputString);
+    var actualOutput = outputString.Remove(trailer.Index, trailer.Length);
+    var diffMessage = AssertWithDiff.GetDiffMessage(expectedOutput, actualOutput);
+    if (diffMessage != null) {
+      output.WriteLine(diffMessage);
+      return 1;
+    }
+    // We expect verification to return exit code 0.
     if (exitCode != 0) {
       output.WriteLine("Verification failed. Output:");
       output.WriteLine(outputString);
       output.WriteLine("Error:");
       output.WriteLine(error);
       return exitCode;
     }
-    var expectFileForVerifier = $"{options.TestFile}.verifier.expect";
-    if (File.Exists(expectFileForVerifier)) {
-      var expectedOutput = File.ReadAllText(expectFileForVerifier);
-      // Chop off the "Dafny program verifier finished with..." trailer
-      var trailer = new Regex("\r?\nDafny program verifier[^\r\n]*\r?\n").Match(outputString);
-      var actualOutput = outputString.Remove(trailer.Index, trailer.Length);
-      var diffMessage = AssertWithDiff.GetDiffMessage(expectedOutput, actualOutput);
-      if (diffMessage == null) {
-        return 0;
-      }
-
-      output.WriteLine(diffMessage);
-      return 1;
-    }
 
     // Then execute the program for each available compiler.
 
     string expectFile = options.TestFile + ".expect";
-    var commonExpectedOutput = "\nDafny program verifier did not attempt verification\n" +
-                         File.ReadAllText(expectFile);
+    var commonExpectedOutput = File.ReadAllText(expectFile);
 
     var success = true;
     foreach (var plugin in dafnyOptions.Plugins) {
@@ -132,12 +133,11 @@ private int ForEachCompiler(ForEachCompilerOptions options) {
         }
 
         // Check for backend-specific exceptions (because of known bugs or inconsistencies)
-        var expectedOutput = commonExpectedOutput;
+        expectedOutput = commonExpectedOutput;
         string? checkFile = null;
         var expectFileForBackend = $"{options.TestFile}.{compiler.TargetId}.expect";
         if (File.Exists(expectFileForBackend)) {
-          expectedOutput = "\nDafny program verifier did not attempt verification\n" +
-                           File.ReadAllText(expectFileForBackend);
+          expectedOutput = File.ReadAllText(expectFileForBackend);
         }
         var checkFileForBackend = $"{options.TestFile}.{compiler.TargetId}.check";
         if (File.Exists(checkFileForBackend)) {
@@ -185,6 +185,10 @@ private int RunWithCompiler(ForEachCompilerOptions options, IExecutableBackend b
     }.Concat(options.OtherArgs);
 
     var (exitCode, outputString, error) = RunDafny(options.DafnyCliPath, dafnyArgs);
+    var compilationOutputPrior = new Regex("\r?\nDafny program verifier[^\r\n]*\r?\n").Match(outputString);
+    if (compilationOutputPrior.Success) {
+      outputString = outputString.Remove(0, compilationOutputPrior.Index + compilationOutputPrior.Length);
+    }
 
     if (exitCode == 0) {
       var diffMessage = AssertWithDiff.GetDiffMessage(expectedOutput, outputString);
@@ -273,11 +277,6 @@ private static bool IsAllowedOutputLine(IExecutableBackend backend, string line)
       return true;
     }
 
-    // This is the first non-blank line we expect when we pass /noVerify
-    if (line == "Dafny program verifier did not attempt verification") {
-      return true;
-    }
-
     // This is output if the compiler emits any errors
     if (line.StartsWith("Wrote textual form of partial target program to")) {
       return true;

Test/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect

@@ -2,44 +2,34 @@ Verifying...
 Executing on C#...
 AssertEqualWithDiff() Failure
 Diff (changing expected into actual):
-
- Dafny program verifier did not attempt verification
 -Different than any output
 +0
 
 
 Executing on JavaScript...
 AssertEqualWithDiff() Failure
 Diff (changing expected into actual):
-
- Dafny program verifier did not attempt verification
 -Different than any output
 +0
 
 
 Executing on Go...
 AssertEqualWithDiff() Failure
 Diff (changing expected into actual):
-
- Dafny program verifier did not attempt verification
 -Different than any output
 +0
 
 
 Executing on Java...
 AssertEqualWithDiff() Failure
 Diff (changing expected into actual):
-
- Dafny program verifier did not attempt verification
 -Different than any output
 +0
 
 
 Executing on Python...
 AssertEqualWithDiff() Failure
 Diff (changing expected into actual):
-
- Dafny program verifier did not attempt verification
 -Different than any output
 +0
 

Test/metatests/TestBeyondVerifierExpect.dfy

@@ -0,0 +1,9 @@
+// RUN: ! %testDafnyForEachCompiler "%s" > "%t"
+// RUN: %diff "%s.testdafny.expect" "%t"
+
+method Main() {
+  ghost var n := 15;
+  if j :| 0 <= j < n { // this gives a no-trigger warning
+  }
+  print "hello\n";
+}

Test/metatests/TestBeyondVerifierExpect.dfy.expect

@@ -0,0 +1 @@
+good bye

Test/metatests/TestBeyondVerifierExpect.dfy.testdafny.expect

@@ -0,0 +1,37 @@
+Verifying...
+Executing on C#...
+AssertEqualWithDiff() Failure
+Diff (changing expected into actual):
+-good bye
++hello
+
+
+Executing on JavaScript...
+AssertEqualWithDiff() Failure
+Diff (changing expected into actual):
+-good bye
++hello
+
+
+Executing on Go...
+AssertEqualWithDiff() Failure
+Diff (changing expected into actual):
+-good bye
++hello
+
+
+Executing on Java...
+AssertEqualWithDiff() Failure
+Diff (changing expected into actual):
+-good bye
++hello
+
+
+Executing on Python...
+AssertEqualWithDiff() Failure
+Diff (changing expected into actual):
+-good bye
++hello
+
+
+Executing on C++...

Test/metatests/TestBeyondVerifierExpect.dfy.verifier.expect

@@ -0,0 +1 @@
+TestBeyondVerifierExpect.dfy(6,5): Warning: /!\ No terms found to trigger on.

Test/metatests/TestDoesNotVerify.dfy

@@ -0,0 +1,8 @@
+// RUN: ! %testDafnyForEachCompiler "%s" > "%t"
+// RUN: %diff "%s.testdafny.expect" "%t"
+
+method Main() {
+  ghost var n := 15;
+  assert n < 12; // error: the verifier complains about this
+  print "hello\n";
+}

Test/metatests/TestDoesNotVerify.dfy.expect

@@ -0,0 +1 @@
+hello

Test/metatests/TestDoesNotVerify.dfy.testdafny.expect

@@ -0,0 +1,8 @@
+Verifying...
+Verification failed. Output:
+TestDoesNotVerify.dfy(6,11): Error: assertion might not hold
+
+Dafny program verifier finished with 0 verified, 1 error
+
+Error:
+

Test/metatests/TestDoesNotVerify.dfy.verifier.expect

@@ -0,0 +1 @@
+TestDoesNotVerify.dfy(6,11): Error: assertion might not hold

Test/metatests/TestMissingVerifierExpect.dfy

@@ -0,0 +1,9 @@
+// RUN: ! %testDafnyForEachCompiler "%s" > "%t"
+// RUN: %diff "%s.testdafny.expect" "%t"
+
+method Main() {
+  ghost var n := 15;
+  if j :| 0 <= j < n { // this gives a no-trigger warning
+  }
+  print "hello\n";
+}

Test/metatests/TestMissingVerifierExpect.dfy.expect

@@ -0,0 +1 @@
+hello

Test/metatests/TestMissingVerifierExpect.dfy.testdafny.expect

@@ -0,0 +1,6 @@
+Verifying...
+AssertEqualWithDiff() Failure
+Diff (changing expected into actual):
++TestMissingVerifierExpect.dfy(6,5): Warning: /!\ No terms found to trigger on.
++
+

Test/metatests/TestWrongVerifierExpect.dfy

@@ -0,0 +1,9 @@
+// RUN: ! %testDafnyForEachCompiler "%s" > "%t"
+// RUN: %diff "%s.testdafny.expect" "%t"
+
+method Main() {
+  ghost var n := 15;
+  if j :| 0 <= j < n { // this gives a no-trigger warning
+  }
+  print "hello\n";
+}

Test/metatests/TestWrongVerifierExpect.dfy.expect

@@ -0,0 +1 @@
+hello

Test/metatests/TestWrongVerifierExpect.dfy.testdafny.expect

@@ -0,0 +1,7 @@
+Verifying...
+AssertEqualWithDiff() Failure
+Diff (changing expected into actual):
+-warning: out of bananas
++TestWrongVerifierExpect.dfy(6,5): Warning: /!\ No terms found to trigger on.
+
+

Test/metatests/TestWrongVerifierExpect.dfy.verifier.expect

@@ -0,0 +1 @@
+warning: out of bananas