Merge branch 'master' of https://github.com/dafny-lang/dafny into git…

…hub-issue-511

# Conflicts:
#	Source/DafnyCore/Options/CommonOptionBag.cs
#	Source/DafnyCore/Options/DafnyCommands.cs
#	Source/DafnyPipeline/DafnyPipeline.csproj

.github/PULL_REQUEST_TEMPLATE.md

@@ -3,6 +3,6 @@
 <!-- Is this a bug fix for an issue visible in the latest release?  Mention this in the PR details and ensure a patch release is considered -->
 
 ### How has this been tested?
-<!-- Tests can be added to `Test/` or to `Source/*.Test/…` and run with `dotnet test` -->
+<!-- Tests can be added to `Source/IntegrationTests/TestFiles/LitTests/LitTest/` or to `Source/*.Test/…` and run with `dotnet test` -->
 
 <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>

.github/workflows/check-deep-tests-reusable.yml

@@ -8,7 +8,7 @@ jobs:
     runs-on: ubuntu-20.04
     steps:
     - name: Checkout Dafny
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         path: dafny
         submodules: recursive

.github/workflows/doc-tests.yml

@@ -30,7 +30,7 @@ jobs:
       with:
         dotnet-version: 6.0.x
     - name: Checkout Dafny
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         submodules: recursive
         path: dafny

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

@@ -76,7 +76,7 @@ jobs:
       run: |
         sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-9 60
     - name: Set up oldest supported JDK
-      if: matrix.target-language-version == 'oldest'
+      if: matrix.target-language-version != 'newest'
       uses: actions/setup-java@v3
       with:
         java-version: 8
@@ -98,7 +98,7 @@ jobs:
     - uses: actions/setup-node@v3
     - run: npm install bignumber.js
     - name: Checkout Dafny
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         path: dafny
         ref: ${{ inputs.ref }}

.github/workflows/msbuild.yml

@@ -27,7 +27,7 @@ jobs:
       with:
         dotnet-version: ${{env.dotnet-version}}
     - name: Checkout Dafny
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         path: dafny
         submodules: recursive
@@ -43,7 +43,7 @@ jobs:
       working-directory: dafny
       run: git apply customBoogie.patch
     - name: Checkout Boogie
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         repository: boogie-org/boogie
         path: dafny/boogie
@@ -53,7 +53,7 @@ jobs:
       run: dotnet build Source/Dafny.sln
     - name: Check whitespace and style
       working-directory: dafny
-      run: dotnet tool run dotnet-format -w -s error --check Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs --exclude DafnyCore/GeneratedFromDafny.cs --exclude DafnyCore/GeneratedFromDafnyRust.cs
+      run: dotnet tool run dotnet-format -w -s error --check Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs --exclude DafnyCore/GeneratedFromDafny.cs
     - name: Create NuGet package (just to make sure it works)
       run: dotnet pack --no-build dafny/Source/Dafny.sln
     - name: Check uniformity of integration tests that exercise backends
@@ -85,7 +85,7 @@ jobs:
     steps:
       # Check out Dafny so that highlighted source is possible
       - name: Checkout Dafny
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: dafny
           submodules: recursive

.github/workflows/nightly-build-reusable.yml

@@ -32,7 +32,7 @@ jobs:
     runs-on: ubuntu-22.04
     steps:
       - name: Checkout Dafny
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           ref: ${{ inputs.ref }}
           submodules: recursive

.github/workflows/nightly-build.yml

@@ -28,14 +28,6 @@ jobs:
     uses: ./.github/workflows/nightly-build-reusable.yml
     with:
       ref: master
-    secrets:
-      nuget_api_key: ${{ secrets.NUGET_API_KEY }}
-
-  nightly-build-for-4-3:
-    if: github.repository_owner == 'dafny-lang'
-    uses: ./.github/workflows/nightly-build-reusable.yml
-    with:
-      ref: 4.3
       publish-prerelease: true
     secrets:
       nuget_api_key: ${{ secrets.NUGET_API_KEY }}

.github/workflows/publish-release-reusable.yml

@@ -40,7 +40,7 @@ jobs:
     - name: Print version
       run: echo ${{ inputs.name }}
     - name: Checkout Dafny
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         path: dafny
         ref: ${{ inputs.ref }}

.github/workflows/refman.yml

@@ -29,7 +29,7 @@ jobs:
       with:
         dotnet-version: 6.0.x
     - name: Checkout Dafny
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         submodules: recursive
         path: dafny

.github/workflows/release-downloads-nuget.yml

@@ -91,7 +91,7 @@ jobs:
     ## Now that the dotnet tool distribution doesn't include the Scripts,
     ## so we need to clone the repository to get them.
     - name: Checkout Dafny
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         submodules: recursive
         path: dafny-repo

.github/workflows/runtime-tests.yml

@@ -21,7 +21,7 @@ jobs:
 
     steps:
       - name: Checkout Dafny
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           submodules: true
       - name: Set up JDK 18

.github/workflows/standard-libraries.yml

@@ -0,0 +1,37 @@
+name: Build and Test Dafny Standard Libraries
+
+on:
+  workflow_dispatch:
+  pull_request:
+    branches: [ master, main-* ]
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  check-deep-tests:
+     uses: ./.github/workflows/check-deep-tests-reusable.yml
+
+  build:
+    needs: check-deep-tests
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout Dafny
+        uses: actions/checkout@v3
+        with:
+          submodules: true
+      - name: Set up JDK 18
+        uses: actions/setup-java@v3
+        with:
+          java-version: 18
+          distribution: corretto
+      - name: Build Dafny
+        run: dotnet build Source/Dafny.sln
+      - name: Get Z3
+        run: make z3-ubuntu
+      - run: npm install bignumber.js
+      - name: Test DafnyStandardLibraries
+        run: make -C Source/DafnyStandardLibraries all
+

.github/workflows/test-report.yml

@@ -14,7 +14,7 @@ jobs:
     if: always()
 
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           submodules: recursive
 

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

@@ -37,7 +37,7 @@ jobs:
       z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02
       Logging__LogLevel__Microsoft: Debug
     steps:
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
       with:
         path: dafny
         submodules: recursive

.gitignore

@@ -58,6 +58,9 @@ Source/.vs
 # Generated by VS Code
 .vscode/*
 
+# Generated by Dafny tooling
+/Source/DafnyStandardLibraries/build
+
 # Generated by Java tools (gradle/javac/etc)
 
 /Source/DafnyRuntime/DafnyRuntimeJava/.gradle
@@ -70,3 +73,5 @@ package-lock.json
 docs/dev/*.fix
 docs/dev/*.feat
 docs/dev/*.break
+
+

.gitmodules

@@ -1,3 +1,3 @@
 [submodule "Test/libraries"]
-	path = Test/libraries
+	path = Source/IntegrationTests/TestFiles/LitTests/LitTest/libraries
 	url = https://github.com/dafny-lang/libraries.git

CONTRIBUTING.md

@@ -36,9 +36,9 @@ If your change is user-visible, then part of the PR should be corresponding chan
 Any PR should have tests that check whether the bug-fix fixes the problem addressed or that the new functionality 
 is properly working.
 
-  - Dafny's integration tests are in [`Test`](../Test).  PRs that fix issues reported on GitHub should include a test in [`Test/git-issues/`](../Test/git-issues/).
+  - Dafny's integration tests are in [this directory](Source/IntegrationTests/TestFiles/LitTests/LitTest).  PRs that fix issues reported on GitHub should include a test under [`git-issues/`](Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/).
 
-    Each `.dfy` file in `Test/` is a test, with a  [`lit`](https://llvm.org/docs/CommandGuide/lit.html) header describing how to run it and a `.expect` file indicating the expected output.  See [`Test/README.md`](../Test/README.md) for more info on running Dafny' integration tests.
+    Each `.dfy` file in this directory is a test, with a  [`lit`](https://llvm.org/docs/CommandGuide/lit.html) header describing how to run it and a `.expect` file indicating the expected output.  See [this README.md file](Source/IntegrationTests/TestFiles/LitTests/LitTest/README.md) for more info on running Dafny' integration tests.
 
   - Dafny's unit tests are in various `*.Test` directories in [`Source`](../Source).
 

Makefile

@@ -7,6 +7,10 @@ all: exe refman
 exe:
 	(cd ${DIR} ; dotnet build Source/Dafny.sln ) ## includes parser
 
+dfydev:
+	(cd ${DIR}/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh)
+	(cd ${DIR} ; dotnet build Source/Dafny.sln ) ## includes parser
+
 boogie: ${DIR}/boogie/Binaries/Boogie.exe
 
 tests:
@@ -58,7 +62,7 @@ z3-ubuntu:
 	chmod +x ${DIR}/Binaries/z3/bin/z3-*
 
 format:
-	dotnet tool run dotnet-format -w -s error Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs --exclude DafnyCore/GeneratedFromDafny.cs --exclude DafnyCore/GeneratedFromDafnyRust.cs
+	dotnet tool run dotnet-format -w -s error Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs --exclude DafnyCore/GeneratedFromDafny.cs
 
 clean:
 	(cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)

Source/Dafny/Dafny.cs

@@ -4,6 +4,6 @@ namespace Dafny;
 
 public class Dafny {
   public static int Main(string[] args) {
-    return DafnyDriver.Main(args);
+    return DafnyCli.Main(args);
   }
 }

Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj

@@ -5,10 +5,16 @@
         <ImplicitUsings>enable</ImplicitUsings>
         <Nullable>enable</Nullable>
         <OutputPath>..\..\Binaries\</OutputPath>
+        <PackageLicenseExpression>MIT</PackageLicenseExpression>
+        <PackageReadmeFile>README.md</PackageReadmeFile>
     </PropertyGroup>
 
     <ItemGroup>
       <ProjectReference Include="..\DafnyCore\DafnyCore.csproj" />
     </ItemGroup>
 
+    <ItemGroup>
+        <None Include="README.md" Pack="true" PackagePath="\" />
+    </ItemGroup>
+
 </Project>

Source/DafnyCore/AST/Expressions/Comprehensions/ExistsExpr.cs

@@ -30,4 +30,39 @@ public override Expression LogicalBody(bool bypassSplitQuantifier = false) {
     body.Type = Term.Type;
     return body;
   }
+
+  /// <summary>
+  /// Returns an expression like 'exists' but where the bound variables have been renamed to have
+  /// 'prefix' as a prefix to their previous names.
+  /// Assumes the expression has been resolved.
+  /// </summary>
+  public Expression AlphaRename(string prefix) {
+    Contract.Requires(this != null);
+    Contract.Requires(prefix != null);
+
+    if (SplitQuantifier != null) {
+      // TODO: what to do?  Substitute(exists.SplitQuantifierExpression);
+    }
+
+    var substMap = new Dictionary<IVariable, Expression>();
+    var var4var = new Dictionary<BoundVar, BoundVar>();
+    var bvars = new List<BoundVar>();
+    foreach (var bv in BoundVars) {
+      var newBv = new BoundVar(bv.tok, prefix + bv.Name, bv.Type);
+      bvars.Add(newBv);
+      var4var.Add(bv, newBv);
+      var ie = new IdentifierExpr(newBv.tok, newBv.Name);
+      ie.Var = newBv;  // resolve here
+      ie.Type = newBv.Type;  // resolve here
+      substMap.Add(bv, ie);
+    }
+    var s = new Substituter(null, substMap, new Dictionary<TypeParameter, Type>());
+    var range = Range == null ? null : s.Substitute(Range);
+    var term = s.Substitute(Term);
+    var attrs = s.SubstAttributes(Attributes);
+    var ex = new ExistsExpr(tok, RangeToken, bvars, range, term, attrs);
+    ex.Type = Type.Bool;
+    ex.Bounds = s.SubstituteBoundedPoolList(Bounds);
+    return ex;
+  }
 }

Source/DafnyCore/AST/Grammar/Printer.cs

@@ -1018,6 +1018,9 @@ public void PrintMethod(Method method, int indent, bool printSignatureOnly) {
 
       int ind = indent + IndentAmount;
       PrintSpec("requires", method.Req, ind);
+      if (method.Reads.Expressions != null) {
+        PrintFrameSpecLine("reads", method.Reads, ind);
+      }
       if (method.Mod.Expressions != null) {
         PrintFrameSpecLine("modifies", method.Mod, ind);
       }
@@ -1236,6 +1239,7 @@ public void PrintStatement(Statement stmt, int indent) {
         } else if (expectStmt != null && expectStmt.Message != null) {
           wr.Write(", ");
           PrintExpression(expectStmt.Message, true);
+          wr.Write(";");
         } else {
           wr.Write(";");
         }