Merge remote-tracking branch 'origin/master' into isolatePaths

.github/workflows/doc-tests.yml

@@ -37,7 +37,7 @@ jobs:
         path: dafny
     - name: Load Z3
       run: |
-        sudo apt-get install -qq libarchive-tools
+        sudo apt-get update && sudo apt-get install -qq libarchive-tools
         mkdir -p dafny/Binaries/z3/bin
         wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip | bsdtar -xf -
         mv z3-* dafny/Binaries/z3/bin/

.github/workflows/integration-tests-reusable.yml

@@ -142,7 +142,7 @@ jobs:
     - name: Load Z3
       if: "!inputs.all_platforms"
       run: |
-        sudo apt-get install -qq libarchive-tools
+        sudo apt-get update && sudo apt-get install -qq libarchive-tools
         mkdir -p dafny/Binaries/z3/bin
         wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip | bsdtar -xf -
         mv z3-4.12.1 dafny/Binaries/z3/bin/

Makefile

@@ -1,3 +1,6 @@
+# Run these tasks even if eponymous files or folders exist
+.PHONY: test-dafny exe
+
 DIR=$(realpath $(dir $(firstword $(MAKEFILE_LIST))))
 
 default: exe
@@ -30,6 +33,24 @@ tests:
 test:
 	(cd "${DIR}"; dotnet test Source/IntegrationTests --filter "DisplayName~${name}")
 
+# Run Dafny on an integration test case directly in the folder itself.
+# make test-run name=<part of the path> action="run ..."
+test-dafny:
+	name="$(name)"; \
+	files=$$(cd "${DIR}"/Source/IntegrationTests/TestFiles/LitTests/LitTest; find . -type f -wholename "*$$name*" | grep -E '\.dfy$$'); \
+	count=$$(echo "$$files" | wc -l); \
+  echo "$${files}"; \
+	if [ "$$count" -eq 0 ]; then \
+		echo "No files found matching pattern: $$name"; \
+		exit 1; \
+	else \
+		echo "$$count test files found."; \
+		for file in $$files; do \
+			filedir=$$(dirname "$$file"); \
+			(cd "${DIR}/Source/IntegrationTests/TestFiles/LitTests/LitTest/$${filedir}"; dotnet run --project "${DIR}"/Source/Dafny -- $(action)  "$$(basename $$file)" ); \
+		done; \
+	fi
+
 tests-verbose:
 	(cd "${DIR}"; dotnet test --logger "console;verbosity=normal" Source/IntegrationTests )
 

RELEASE_NOTES.md

@@ -2,6 +2,79 @@
 
 See [docs/dev/news/](docs/dev/news/).
 
+# 4.8.1
+
+## New features
+
+- feat: allow type parameters of `newtype` declarations
+  feat: support optional `witness` clause of constraint-less `newtype` declarations
+  feat: show tool tips for auto-completed type parameters
+  feat: show tool tips for inferred `(==)` characteristics
+  fix: Don't let `newtype` well-formedness checking affect witness checking (fixes ##5520)
+  fix: Check the emptiness status of constraint-less `newtype` declarations (fixes #5521)
+  (https://github.com/dafny-lang/dafny/pull/5495)
+
+- New feature: model extractor
+
+  ### CLI option
+
+  The `dafny verify` command now has an option `--extract:<file>`, where (just like for the various print options) `<file>` is allowed to be `-` to denote standard output.
+
+  ### Extract mechanism
+
+  Upon successful verification, the new extract mechanism visits the AST of the given program. For any module marked with `{:extract}`, the extract-worthy material from the module is output. The output declarations will be in the same order as they appear textually in the module (in particular, the fact that module-level Dafny declarations are collected in an internal class `_default` has no bearing on the output order).
+
+  Three kinds of declarations are extract-worthy:
+
+  * A type declaration `A<X, Y, Z>` that bears an attribute `{:extract_name B}` is extracted into a Boogie type declaration `type B _ _ _;`.
+
+      The definition of the type is ignored. (The intended usage for an extracted type is that the Dafny program give a definition for the type, which goes to show the existence of such a type.)
+
+  * A function declaration `F(x: X, y: Y): Z` that bears an attribute `{:extract_name G}` is extracted into a Boogie function declaration `function G(x: X, y: Y): Z;`.
+
+      The body of the Dafny function is ignored. (The intended usage for an extracted function is that the Dafny program give a definition for the function, which goes to show the existence of such a function.)
+
+  * A lemma declaration `L(x: X, y: Y) requires P ensures Q` that bears an attribute `{:extract_pattern ...}` or an attribute `{:extract_used_by ...}` is extracted into a Boogie `axiom`. The axiom has the basic form `axiom (forall x: X, y: Y :: P ==> Q);`.
+
+      If the lemma has an attribute `{:extract_used_by F}`, then the axiom will be emitted into the `uses` clause of the Boogie function generated for Dafny function `F`.
+
+      If the lemma has no in-parameters, the axiom is just `P ==> Q`.
+
+      If the lemma has in-parameters, then any attribute `{:extract_pattern E, F, G}` adds a matching pattern `{ E, F, G }` to the emitted quantifier. Also, any attribute `{:extract_attribute "name", E, F, G}` adds an attribute `{:name E, F, G}` to the quantifier.
+
+  ### Expressions
+
+  The pre- and postconditions of extracted lemmas turn into analogous Boogie expressions, and the types of function/lemma parameters and bound variables are extracted into analogous Boogie types. The intended usage of the extract mechanism is that these expressions and types do indeed have analogous Boogie types.
+
+  At this time, only a limited set of expressions and types are supported, but more can be added in the future.
+
+  Any `forall` and `exists` quantifiers in expressions are allowed to use `:extract_pattern` and `:extract_attribute` attributes, as described above for lemmas.
+
+  Some extracted expressions are simplified. For example, `true && !!P` is simplified to `P`.
+
+  ### Soundness
+
+  The Dafny program that is used as input for the extraction is treated like any other Dafny program. The intended usage of the extraction mechanism is to prove parts of the axiomatization in `DafnyPrelude.bpl` to be logically consistent. Whether or not the extracted Boogie declarations meet this goal depends on the given Dafny program. For example, if the given Dafny program formalizes sequences in terms of maps and formalizes maps in terms of sequences, then the extraction probably does not provide guarantees of consistency.
+  (https://github.com/dafny-lang/dafny/pull/5621)
+
+- Dafny-to-Rust: `{:test}` methods generate `#[test]` wrappers in Rust that can be invoked using `cargo test`.
+  Similarly, `{:rust_cfg_test}` on modules generates a `#[cfg(test)]` in the resulting rust module.
+  (https://github.com/dafny-lang/dafny/pull/5676)
+
+## Bug fixes
+
+- Allow hiding instance member using a static reference
+
+- Enable using "hide *" in the context of a recursive function
+
+- Support for double constant initialization in Dafny-to-Rust (https://github.com/dafny-lang/dafny/pull/5642)
+
+- Support for enumerating datatypes in the Rust backend (https://github.com/dafny-lang/dafny/pull/5643)
+
+- Tail-Recursion for the Dafny-to-Rust compiler (https://github.com/dafny-lang/dafny/pull/5647)
+
+- The new resolver (accessible using `--type-system-refresh`) can now handle revealing instance functions using a static receiver, as it is the case for the current resolver (https://github.com/dafny-lang/dafny/pull/5760)
+
 # 4.8.0
 
 ## New features

Source/DafnyCore.Test/WriterFromOutputHelper.cs

@@ -25,17 +25,29 @@ public override void Write(char value) {
   public override Encoding Encoding => Encoding.Default;
 
   public override void WriteLine(string? value) {
-    output.WriteLine(buffer + value);
+    try {
+      output.WriteLine(buffer + value);
+    } catch {
+      // ignored because of https://github.com/dafny-lang/dafny/issues/5723
+    }
     buffer.Clear();
   }
 
   public override void WriteLine(string format, params object?[] arg) {
-    output.WriteLine(buffer + format, arg);
+    try {
+      output.WriteLine(buffer + format, arg);
+    } catch {
+      // ignored because of https://github.com/dafny-lang/dafny/issues/5723
+    }
     buffer.Clear();
   }
 
   public override void Flush() {
-    output.WriteLine(buffer.ToString());
+    try {
+      output.WriteLine(buffer.ToString());
+    } catch {
+      // ignored because of https://github.com/dafny-lang/dafny/issues/5723
+    }
     base.Flush();
   }
 }

Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs

@@ -28,6 +28,7 @@ public NestedMatchExpr(Cloner cloner, NestedMatchExpr original) : base(cloner, o
     this.Source = cloner.CloneExpr(original.Source);
     this.Cases = original.Cases.Select(cloner.CloneNestedMatchCaseExpr).ToList();
     this.UsesOptionalBraces = original.UsesOptionalBraces;
+
     if (cloner.CloneResolvedFields) {
       Flattened = cloner.CloneExpr(original.Flattened);
     }

Source/DafnyCore/AST/Expressions/StmtExpr.cs

@@ -53,20 +53,25 @@ public override IEnumerable<Expression> TerminalExpressions {
   /// S is executed.
   /// This method should be called only after successful resolution of the expression.
   /// </summary>
-  public Expression GetSConclusion() {
-    // this is one place where we actually investigate what kind of statement .S is
-    if (S is PredicateStmt) {
-      var s = (PredicateStmt)S;
-      return s.Expr;
-    } else if (S is CalcStmt) {
-      var s = (CalcStmt)S;
-      return s.Result;
-    } else if (S is HideRevealStmt) {
-      return CreateBoolLiteral(tok, true);  // one could use the definition axiom or the referenced labeled assertions, but "true" is conservative and much simpler :)
-    } else if (S is AssignStatement) {
-      return CreateBoolLiteral(tok, true);  // one could use the postcondition of the method, suitably instantiated, but "true" is conservative and much simpler :)
-    } else {
-      Contract.Assert(false); throw new cce.UnreachableException();  // unexpected statement
+  public Expression GetStatementConclusion() {
+    return GetStatementConclusion(S);
+  }
+
+  private Expression GetStatementConclusion(Statement statement) {
+    switch (statement) {
+      // this is one place where we actually investigate what kind of statement .S is
+      case PredicateStmt stmt:
+        return stmt.Expr;
+      case CalcStmt stmt:
+        return stmt.Result;
+      case HideRevealStmt:
+        return CreateBoolLiteral(tok, true);  // one could use the definition axiom or the referenced labeled assertions, but "true" is conservative and much simpler :)
+      case AssignStatement:
+        return CreateBoolLiteral(tok, true);  // one could use the postcondition of the method, suitably instantiated, but "true" is conservative and much simpler :)
+      case BlockByProofStmt stmt:
+        return GetStatementConclusion(stmt.Body);
+      default:
+        Contract.Assert(false); throw new cce.UnreachableException();  // unexpected statement
     }
   }