Merge branch 'master' into issue-5274

CONTRIBUTING.md

@@ -74,7 +74,7 @@ After doing these steps once, for other PRs, one only needs to re-run deep check
 - If some required tests fail, investigate and push more commits, but know that each CI run takes a lot of time, so try to fix the problem with as few commits as possible (ideally 1)
   It is also possible you find some tests that fail randomly, in that case, re-run them and report to the team. Avoid using the re-run all failed jobs here, because it will re-run _all_ jobs, so select them individually instead.
 - Have someone approve the PR and merge it (or auto-merge).
-- Once the PR with the fix to the CI is merged to master, go to https://github.com/dafny-lang/dafny/actions/workflows/deep-tests.yml
+- Once the PR with the fix to the CI is merged to master, go to https://github.com/dafny-lang/dafny/actions/workflows/nightly-build.yml
 - Select "Run workflow..."
 - Select master
 - Wait for this new run to succeed.
@@ -106,4 +106,4 @@ You can find a description of the release process in [docs/dev/RELEASE.md](https
 
 Dafny is still changing and backwards incompatible changes may be made. Any backwards compatibility breaking change must be easy to adapt to, such as by adding a command line option. In the future, we plan to add a `dafny migrate` command which should support migrating any Dafny codebase from the previous to the current CLI version. 
 
-As rule, Dafny features must be marked as deprecated, including migration instructions, at least one release before they are removed.
+As rule, Dafny features must be marked as deprecated, including migration instructions, at least one release before they are removed.

Source/DafnyDriver/CliCompilation.cs

@@ -24,6 +24,7 @@ public class CliCompilation {
   public Compilation Compilation { get; }
   private readonly ConcurrentDictionary<MessageSource, int> errorsPerSource = new();
   private int errorCount;
+  private int warningCount;
   public bool DidVerification { get; private set; }
 
   private CliCompilation(
@@ -48,22 +49,33 @@ private CliCompilation(
     Compilation = createCompilation(executionEngine, input);
   }
 
-  public int ExitCode => (int)ExitValue;
+  public async Task<int> GetAndReportExitCode() {
+    var value = await GetAndReportExitValue();
+    return (int)value;
+  }
 
-  public ExitValue ExitValue {
-    get {
+  public async Task<ExitValue> GetAndReportExitValue() {
+    if (errorCount > 0) {
       if (HasErrorsFromSource(MessageSource.Project)) {
         return ExitValue.PREPROCESSING_ERROR;
       }
 
       if (HasErrorsFromSource(MessageSource.Verifier)) {
         return ExitValue.VERIFICATION_ERROR;
       }
-      return errorCount > 0 ? ExitValue.DAFNY_ERROR : ExitValue.SUCCESS;
+      return ExitValue.DAFNY_ERROR;
+    }
 
-      bool HasErrorsFromSource(MessageSource source) {
-        return errorsPerSource.GetOrAdd(source, _ => 0) != 0;
-      }
+    if (warningCount > 0 && !Options.Get(CommonOptionBag.AllowWarnings)) {
+      await Options.OutputWriter.WriteLineAsync(
+        "Compilation failed because warnings were found and --allow-warnings is false");
+      return ExitValue.DAFNY_ERROR;
+    }
+
+    return ExitValue.SUCCESS;
+
+    bool HasErrorsFromSource(MessageSource source) {
+      return errorsPerSource.GetOrAdd(source, _ => 0) != 0;
     }
   }
 
@@ -105,6 +117,10 @@ public void Start() {
             (_, previous) => previous + 1);
           Interlocked.Increment(ref errorCount);
         }
+
+        if (newDiagnostic.Diagnostic.Level == ErrorLevel.Warning) {
+          Interlocked.Increment(ref warningCount);
+        }
         var dafnyDiagnostic = newDiagnostic.Diagnostic;
         consoleReporter.Message(dafnyDiagnostic.Source, dafnyDiagnostic.Level,
           dafnyDiagnostic.ErrorId, dafnyDiagnostic.Token, dafnyDiagnostic.Message);

Source/DafnyDriver/Commands/MeasureComplexityCommand.cs

@@ -71,7 +71,7 @@ private static async Task<int> Execute(DafnyOptions options) {
       await verificationResultsLogged;
     }
 
-    return compilation.ExitCode;
+    return await compilation.GetAndReportExitCode();
   }
 
   private static async Task RunVerificationIterations(DafnyOptions options, CliCompilation compilation,

Source/DafnyDriver/Commands/ResolveCommand.cs

@@ -17,10 +17,11 @@ public static Command Create() {
       compilation.Start();
       await compilation.Resolution;
 
-      if (compilation.ExitValue == ExitValue.SUCCESS) {
+      var value = await compilation.GetAndReportExitValue();
+      if (value == ExitValue.SUCCESS) {
         await options.OutputWriter.WriteLineAsync("\nDafny program verifier did not attempt verification");
       }
-      return compilation.ExitCode;
+      return (int)value;
     });
     return result;
   }

Source/DafnyDriver/Commands/VerifyCommand.cs

@@ -69,7 +69,7 @@ public static async Task<int> HandleVerification(DafnyOptions options) {
       await verificationResultsLogged;
     }
 
-    return compilation.ExitCode;
+    return await compilation.GetAndReportExitCode();
   }
   public static async Task ReportVerificationSummary(
     CliCompilation cliCompilation,

Source/DafnyDriver/DafnyNewCli.cs

@@ -224,11 +224,7 @@ private static async Task<bool> ProcessProjectFile(DafnyOptions dafnyOptions, Fi
 
     foreach (var diagnostic in projectFile.Errors.AllMessages) {
       var message = $"{diagnostic.Level}: {diagnostic.Message}";
-      if (diagnostic.Level == ErrorLevel.Error) {
-        await dafnyOptions.ErrorWriter.WriteLineAsync(message);
-      } else {
-        await dafnyOptions.OutputWriter.WriteLineAsync(message);
-      }
+      await dafnyOptions.OutputWriter.WriteLineAsync(message);
     }
 
     projectFile.Validate(dafnyOptions.OutputWriter, AllOptions);

Source/DafnyStandardLibraries/scripts/check-examples

@@ -219,6 +219,7 @@ do
           ec=2
         elif [ "$command" == "%check-resolve-warn" ]; then
           com=resolve
+          dOptions="$dOptions --allow-warnings"
           ec=0
         elif [ "$command" == "%check-translate" ]; then
           com=translate

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/assume.dfy

@@ -1,6 +1,6 @@
-// RUN: %testDafnyForEachResolver "%s" -- --allow-axioms=false 
+// RUN: ! %testDafnyForEachResolver "%s" -- --allow-axioms=false
 // NONUNIFORM: warning will be the same for all back-end
-// RUN: %verify --standard-libraries --allow-axioms:false "%s" > "%t"
+// RUN: ! %verify --standard-libraries --allow-axioms:false "%s" &> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method Foo() {

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/assume.dfy.expect

@@ -3,3 +3,4 @@ assume.dfy(11,10): Warning: assume keyword in assign-such-that statement has no
 assume.dfy(13,11): Warning: assume keyword in update-with-failure statement has no {:axiom} annotation
 
 Dafny program verifier finished with 2 verified, 0 errors
+Compilation failed because warnings were found and --allow-warnings is false

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/function.dfy

@@ -1,6 +1,6 @@
-// RUN: %verify --allow-axioms:false --type-system-refresh "%s" > "%t"
+// RUN: ! %verify --allow-axioms:false --type-system-refresh "%s" &> "%t"
 // NONUNIFORM: warning will be the same for all back-end
-// RUN: ! %run --allow-axioms:false "%s" >> "%t"
+// RUN: ! %run --allow-axioms:false "%s" &>> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/function.dfy.expect

@@ -4,6 +4,7 @@ function.dfy(8,36): Warning: This ensures clause is part of a bodyless function.
 function.dfy(8,50): Warning: This ensures clause is part of a bodyless function. Add the {:axiom} attribute to it or the enclosing function to suppress this warning
 
 Dafny program verifier finished with 9 verified, 0 errors
+Compilation failed because warnings were found and --allow-warnings is false
 function.dfy(7,33): Warning: This ensures clause is part of a bodyless function. Add the {:axiom} attribute to it or the enclosing function to suppress this warning
 function.dfy(7,47): Warning: This ensures clause is part of a bodyless function. Add the {:axiom} attribute to it or the enclosing function to suppress this warning
 function.dfy(8,36): Warning: This ensures clause is part of a bodyless function. Add the {:axiom} attribute to it or the enclosing function to suppress this warning

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/method.dfy

@@ -1,4 +1,4 @@
-// RUN: %verify --allow-axioms:false --type-system-refresh "%s" > "%t"
+// RUN: %verify --allow-axioms:false --type-system-refresh --allow-warnings "%s" > "%t"
 // NONUNIFORM: warning will be the same for all back-ends
 // RUN: ! %run --allow-axioms:false "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"

Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy

@@ -1,40 +1,40 @@
 // Invalid value gives error and stops compilation
-// RUN: ! %resolve --warn-shadowing=true %S/broken/invalidValue.toml 2> "%t"
+// RUN: ! %resolve --warn-shadowing=true %S/broken/invalidValue.toml &> "%t"
 
 // A project file can specify input files and configure options
-// RUN: %resolve "%S/dfyconfig.toml" >> "%t"
+// RUN: ! %resolve "%S/dfyconfig.toml" &>> "%t"
 
 // Test using a URL instead of a local file as a project file
-// RUN: ! %resolve "https://github.com/dafny-lang/dafny/blob/master/web.toml" 2>> %t
+// RUN: ! %resolve "https://github.com/dafny-lang/dafny/blob/master/web.toml" &>> %t
 
 // Test option override behavior
-// RUN: %resolve "%S/dfyconfig.toml" --warn-shadowing=false >> "%t"
+// RUN: %resolve "%S/dfyconfig.toml" --warn-shadowing=false &>> "%t"
 
 // Test option with default override behavior
-// RUN: ! %resolve "%S/dfyconfig.toml" --function-syntax=3 >> "%t"
+// RUN: ! %resolve "%S/dfyconfig.toml" --function-syntax=3 &>> "%t"
 
 // Multiple project files are not allowed
-// RUN: ! %resolve "%S/dfyconfig.toml" "%S/broken/dfyconfig.toml" 2>> %t
+// RUN: ! %resolve "%S/dfyconfig.toml" "%S/broken/dfyconfig.toml" &>> %t
 
 // Project files may not contain unknown properties
-// RUN: ! %resolve "%S/broken/dfyconfig.toml" 2>> %t
+// RUN: ! %resolve "%S/broken/dfyconfig.toml" &>> %t
 
 // Warn if file contains options that don't exist
-// RUN: %resolve "%S/broken/invalidOption.toml" >> "%t"
+// RUN: ! %resolve "%S/broken/invalidOption.toml" &>> "%t"
 
 // Project files must be files on disk.
-// RUN: ! %resolve "%S/doesNotExist.toml" 2>> %t
+// RUN: ! %resolve "%S/doesNotExist.toml" &>> %t
 
 // Project file options must have the right type
-// RUN: ! %resolve "%S/badTypes/dfyconfig.toml" >> "%t"
+// RUN: ! %resolve "%S/badTypes/dfyconfig.toml" &>> "%t"
 
 // A project file without includes will take all .dfy files as input
-// RUN: %resolve "%S/noIncludes/dfyconfig.toml" >> "%t"
+// RUN: ! %resolve "%S/noIncludes/dfyconfig.toml" &>> "%t"
 
 // Files included by the project file and on the CLI, duplicate is ignored.
-// RUN: %resolve "%S/dfyconfig.toml" "%S/src/input.dfy" >> "%t"
+// RUN: ! %resolve "%S/dfyconfig.toml" "%S/src/input.dfy" &>> "%t"
 
 // Files excluded by the project file and included on the CLI, are included
-// RUN: ! %resolve "%S/dfyconfig.toml" "%S/src/excluded.dfy" >> "%t"
+// RUN: ! %resolve "%S/dfyconfig.toml" "%S/src/excluded.dfy" &>> "%t"
 
 // RUN: %diff "%s.expect" "%t"

Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy.expect

@@ -1,8 +1,8 @@
 Error: The Dafny project file invalidValue.toml contains the following errors: (3,14) : error : Unexpected token `NoIncludes` for a value
 
+Warning: only Dafny project files named dfyconfig.toml are recognised by the Dafny IDE.
 input.dfy(6,8): Warning: Shadowed local-variable name: x
-
-Dafny program verifier did not attempt verification
+Compilation failed because warnings were found and --allow-warnings is false
 Error: file web.toml not found
 
 Dafny program verifier did not attempt verification
@@ -14,17 +14,14 @@ Error: The Dafny project file dfyconfig.toml contains the following errors: (1,1
 Warning: only Dafny project files named dfyconfig.toml are recognised by the Dafny IDE.
 Warning: option 'does-not-exist' that was specified in the project file, is not a valid Dafny option.
 invalidOption.toml(1,0): Warning: only Dafny project files named dfyconfig.toml are recognised by the Dafny IDE.
-
-Dafny program verifier did not attempt verification
+Compilation failed because warnings were found and --allow-warnings is false
 Error: file doesNotExist.toml not found
 dfyconfig.toml(1,0): Error: could not parse value '3' for option 'warn-shadowing' that has type 'Boolean'
 input.dfy(6,8): Warning: Shadowed local-variable name: x
 moreInput.dfy(6,8): Warning: Shadowed local-variable name: x
-
-Dafny program verifier did not attempt verification
+Compilation failed because warnings were found and --allow-warnings is false
 input.dfy(6,8): Warning: Shadowed local-variable name: x
-
-Dafny program verifier did not attempt verification
+Compilation failed because warnings were found and --allow-warnings is false
 excluded.dfy(3,7): Error: Duplicate member name: Foo
 input.dfy(6,8): Warning: Shadowed local-variable name: x
 excluded.dfy(6,8): Warning: Shadowed local-variable name: z

Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-CachedBuilds.dfy

@@ -1,4 +1,4 @@
-// RUN: %verify --manual-triggers "%s" > "%t"
+// RUN: %verify --manual-triggers --allow-deprecation "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This module proves the correctness of the algorithms.  It leaves a number of things undefined.
@@ -959,7 +959,7 @@ abstract module M0 {
     ensures p.fst == pC.fst
     ensures StateCorrespondence(p.snd, pC.snd)
   {
-    assume |args| == Arity(primExec) ==>
+    assume {:axiom} |args| == Arity(primExec) ==>
       ValidArgs(primExec, args, stCombined) == ValidArgs(primExec, args, stCombinedC);  // TODO:  This will require some work!
 
     if |args| == Arity(primExec) && ValidArgs(primExec, args, stCombined) {

Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-CachedBuilds.dfy.expect

@@ -1,6 +1,2 @@
-CloudMake-CachedBuilds.dfy(107,6): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead
-CloudMake-CachedBuilds.dfy(447,4): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead
-CloudMake-CachedBuilds.dfy(1249,8): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead
-CloudMake-CachedBuilds.dfy(962,4): Warning: assume statement has no {:axiom} annotation
 
 Dafny program verifier finished with 76 verified, 0 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ParallelBuilds.dfy

@@ -1,4 +1,4 @@
-// RUN: %verify --relax-definite-assignment --manual-triggers "%s" > "%t"
+// RUN: %verify --relax-definite-assignment --manual-triggers --allow-deprecation "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This module proves the correctness of the algorithms.  It leaves a number of things undefined.

Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-ParallelBuilds.dfy.expect

@@ -1,3 +1,2 @@
-CloudMake-ParallelBuilds.dfy(562,6): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead
 
 Dafny program verifier finished with 101 verified, 0 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DirtyLoops.dfy

@@ -1,5 +1,5 @@
 // RUN: %exits-with 4 %verify --relax-definite-assignment --print:"%t.dprint.dfy" "%s" > "%t"
-// RUN: %resolve "%t.dprint.dfy" >> "%t"
+// RUN: %resolve "%t.dprint.dfy" --allow-warnings >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // For a body-less loop specification, a local variable or

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ISets.dfy

@@ -35,9 +35,9 @@ ghost method m1() {
  assert s2 - s3 == iset{3}; // set difference
 
  assert (iset x | x in s2 :: x+1) == iset{2,3,4}; // set comprehension
- assert 17 in (iset x: int | true :: x); // set comprehension
+ assert 17 in (iset x: int {:trigger} | true :: x); // set comprehension
 
- assert (imap x: int | true :: x+1)[14] == 15;
+ assert (imap x: int {:trigger} | true :: x+1)[14] == 15;
 }
 
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ISets.dfy.expect

@@ -1,4 +1,2 @@
-ISets.dfy(38,15): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
-ISets.dfy(40,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 
 Dafny program verifier finished with 2 verified, 0 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/JustWarnings.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s" -- --warn-shadowing
+// RUN: %testDafnyForEachResolver "%s" -- --warn-shadowing --allow-warnings
 
 
 // This file tests the behavior where the Resolver reports some warnings

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrecedenceLinter.dfy

@@ -1,4 +1,4 @@
-// RUN: %resolve "%s" > "%t"
+// RUN: %resolve "%s" --allow-warnings > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 ghost predicate P0(A: bool, B: bool, C: bool) {

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SmallTests.dfy

@@ -1,5 +1,5 @@
 // RUN: %exits-with 4 %verify --relax-definite-assignment --allow-axioms --allow-deprecation --print "%t.dprint.dfy" "%s" > "%t"
-// RUN: %resolve --allow-axioms "%t.dprint.dfy" >> "%t"
+// RUN: %resolve --allow-axioms --allow-warnings "%t.dprint.dfy" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class Node {

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Stdin.dfy

@@ -1,6 +1,6 @@
 // RUN: %exits-with 0 %stdin "module A{}" %baredafny verify --show-snippets:false --stdin > "%t"
 // RUN: %exits-with 4 %stdin "method a() { assert false; }" %baredafny verify --show-snippets:false --stdin >> "%t"
-// RUN: %exits-with 0 %stdin "" %baredafny verify --show-snippets:false --stdin >> "%t"
+// RUN: %exits-with 0 %stdin "" %baredafny verify --allow-warnings --show-snippets:false --stdin >> "%t"
 // Ensuring include statements work when processing standard in too
 // (regression test for https://github.com/dafny-lang/dafny/issues/4135)
 // We don't capture the output to %t because it ends up including paths,

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite-stages.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --allow-deprecation
 
 
 // Schorr-Waite algorithms, written and verified in Dafny.

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite-stages.dfy.expect

@@ -1,23 +1,2 @@
-SchorrWaite-stages.dfy(149,7): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(150,10): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(161,9): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(162,16): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(164,11): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(168,15): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(174,11): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(175,11): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(201,7): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(202,10): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(221,9): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(223,11): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(225,16): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(230,11): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(236,11): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(239,11): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(255,7): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(256,10): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(260,9): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(261,16): Warning: the ... refinement feature in statements is deprecated
-SchorrWaite-stages.dfy(263,11): Warning: the ... refinement feature in statements is deprecated
 
 Dafny program verifier finished with 7 verified, 0 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/MonotonicHeapstate.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --allow-deprecation
 
 
 module M0 {

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/MonotonicHeapstate.dfy.expect

@@ -1,7 +1,2 @@
-MonotonicHeapstate.dfy(92,13): Warning: the ... refinement feature in statements is deprecated
-MonotonicHeapstate.dfy(99,13): Warning: the ... refinement feature in statements is deprecated
-MonotonicHeapstate.dfy(106,13): Warning: the ... refinement feature in statements is deprecated
-MonotonicHeapstate.dfy(146,9): Warning: the ... refinement feature in statements is deprecated
-MonotonicHeapstate.dfy(147,13): Warning: the ... refinement feature in statements is deprecated
 
 Dafny program verifier finished with 24 verified, 0 errors