diff --git a/.github/workflows/compfuzzci_close_pr.yaml b/.github/workflows/compfuzzci_close_pr.yaml new file mode 100644 index 00000000000..fec95d7b6b2 --- /dev/null +++ b/.github/workflows/compfuzzci_close_pr.yaml @@ -0,0 +1,29 @@ +# This workflow is triggered on PR being closed. +# It dispatches workflow on CompFuzzCI repository, where the bugs found in the PR head is discarded from the database. + +name: Updating CompFuzzCI on PR Closed +on: + pull_request: + branches: + - master + types: [closed] + +jobs: + UpdatePRClosed: + if: github.event.pull_request.base.ref == 'master' && github.event.pull_request.head.repo.owner.login == 'dafny-lang' + runs-on: ubuntu-latest + steps: + - name: Trigger CompFuzzCI + uses: actions/github-script@v7 + with: + github-token: ${{ secrets.COMPFUZZCI_PAT }} + script: | + await github.rest.actions.createWorkflowDispatch({ + owner: 'CompFuzzCI', + repo: 'DafnyCompilerFuzzer', + workflow_id: 'update_pr_close.yaml', + ref: 'main', + inputs: { + pr_head_ref: '${{github.event.pull_request.head.ref}}' + } + }) \ No newline at end of file diff --git a/.github/workflows/compfuzzci_fuzz.yaml b/.github/workflows/compfuzzci_fuzz.yaml new file mode 100644 index 00000000000..720f6a02a76 --- /dev/null +++ b/.github/workflows/compfuzzci_fuzz.yaml @@ -0,0 +1,37 @@ +# This workflow is triggered on PR being opened, synced, reopened, closed. +# It dispatches workflow on CompFuzzCI repository, where fuzzing of the PR is handled. +# For problems or suggestions, contact karnbongkot.boonriong23@imperial.ac.uk + +name: Fuzzing on PR +on: + pull_request_target: + branches: + - master + +jobs: + FuzzOnPR: + if: github.event.pull_request.base.ref == 'master' && + (github.event.pull_request.author_association == 'COLLABORATOR' || + github.event.pull_request.author_association == 'MEMBER' || + github.event.pull_request.author_association == 'OWNER') + runs-on: ubuntu-latest + steps: + - name: Trigger CompFuzzCI + uses: actions/github-script@v7 + with: + github-token: ${{ secrets.COMPFUZZCI_PAT }} + script: | + await github.rest.actions.createWorkflowDispatch({ + owner: 'CompFuzzCI', + repo: 'DafnyCompilerFuzzer', + workflow_id: 'fuzz.yaml', + ref: 'main', + inputs: { + pr: '${{github.event.pull_request.number}}', + author: '${{github.event.pull_request.user.login}}', + branch: '${{github.event.pull_request.head.ref}}', + head_sha: '${{github.event.pull_request.head.sha}}', + duration: '3600', + instance: '2' + } + }) \ No newline at end of file diff --git a/.github/workflows/compfuzzci_process_issues.yaml b/.github/workflows/compfuzzci_process_issues.yaml new file mode 100644 index 00000000000..2228ef0a2d9 --- /dev/null +++ b/.github/workflows/compfuzzci_process_issues.yaml @@ -0,0 +1,51 @@ +# This workflow is triggered on issue being opened, closed, reopened. +# The CompFuzzCI fuzzer needs to keep track of active issues in the repository to ensure that the fuzzer does not report the same issue multiple times. +# For open and reopen events: It dispatches workflow on CompFuzzCI repository, where the issue is added to the database. +# For close event: It dispatches workflow on CompFuzzCI repository, where the issue is removed from the database. + +name: Issue Update for Fuzzer +on: + issues: + branches: + - master + types: [opened, closed, reopened] + +jobs: + UpdateIssueOpened: + if: github.event.action == 'opened' || github.event.action == 'reopened' + runs-on: ubuntu-latest + steps: + - name: Trigger CompFuzzCI + uses: actions/github-script@v7 + with: + github-token: ${{ secrets.COMPFUZZCI_PAT }} + script: | + await github.rest.actions.createWorkflowDispatch({ + owner: 'CompFuzzCI', + repo: 'DafnyCompilerFuzzer', + workflow_id: 'update_issue_open.yaml', + ref: 'main', + inputs: { + issue_number: '${{github.event.issue.number}}', + issuer: '${{github.event.issue.user.login}}', + commit: '${{ github.sha }}' + } + }) + UpdateIssueClosed: + if: github.event.action == 'closed' + runs-on: ubuntu-latest + steps: + - name: Trigger CompFuzzCI + uses: actions/github-script@v7 + with: + github-token: ${{ secrets.COMPFUZZCI_PAT }} + script: | + await github.rest.actions.createWorkflowDispatch({ + owner: 'CompFuzzCI', + repo: 'DafnyCompilerFuzzer', + workflow_id: 'update_issue_close.yaml', + ref: 'main', + inputs: { + issue_number: '${{github.event.issue.number}}' + } + }) \ No newline at end of file diff --git a/.github/workflows/daily-soak-test-build.yml b/.github/workflows/daily-soak-test-build.yml new file mode 100644 index 00000000000..98f9025f244 --- /dev/null +++ b/.github/workflows/daily-soak-test-build.yml @@ -0,0 +1,23 @@ + +# Scheduled daily build +# +# The purpose of this build is to run tests that may have non-deterministic failures +# many times over, in the hopes of more aggressively revealing +# flaky tests that occasionally slow down unrelated development. + +name: Daily soak test workflow + +on: + schedule: + # Chosen to be hopefully outside of business hours for most contributors' + # time zones, and not on the hour to avoid heavy scheduled-job times: + # https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#schedule + - cron: "30 3 * * *" + workflow_dispatch: + +jobs: + daily-soak-build-for-master: + if: github.repository_owner == 'dafny-lang' || github.event_name == 'workflow_dispatch' + uses: ./.github/workflows/xunit-tests-reusable.yml + with: + soak_test: true diff --git a/.github/workflows/integration-tests-reusable.yml b/.github/workflows/integration-tests-reusable.yml index 086b547eb1b..7dc0d80617f 100644 --- a/.github/workflows/integration-tests-reusable.yml +++ b/.github/workflows/integration-tests-reusable.yml @@ -12,11 +12,15 @@ on: ref: required: true type: string + compilers: + description: 'Compilers to use' + type: string + required: false + default: "" env: dotnet-version: 6.0.x # SDK Version for building Dafny - jobs: # This job is used to dynamically calculate the matrix dimensions. # For now that just makes the sharding a little cleaner, but it will shortly @@ -27,7 +31,7 @@ jobs: - name: Populate OS list (all platforms) id: populate-os-list-all if: inputs.all_platforms - run: echo "os-list=[\"ubuntu-latest\", \"ubuntu-20.04\", \"macos-latest\", \"windows-2019\"]" >> $GITHUB_OUTPUT + run: echo "os-list=[\"ubuntu-20.04\", \"macos-13\", \"windows-2019\"]" >> $GITHUB_OUTPUT - name: Populate OS list (one platform) id: populate-os-list-one if: "!inputs.all_platforms" @@ -35,7 +39,7 @@ jobs: - name: Populate OS mapping for package.py id: populate-os-mapping run: | - echo "os-mapping={\"ubuntu-latest\": \"ubuntu\", \"ubuntu-20.04\": \"ubuntu\", \"macos-latest\": \"macos\", \"windows-2019\": \"windows\"}" >> $GITHUB_OUTPUT + echo "os-mapping={\"ubuntu-20.04\": \"ubuntu\", \"macos-13\": \"macos\", \"windows-2019\": \"windows\"}" >> $GITHUB_OUTPUT - name: Populate target runtime version list (all platforms) id: populate-target-runtime-version-all if: inputs.all_platforms @@ -91,12 +95,12 @@ jobs: - name: Set up oldest supported Go uses: actions/setup-go@v5 with: - go-version: '1.15' + go-version: '1.21' cache: false - name: Set up goimports env: GO111MODULE: on - run: go get golang.org/x/tools/cmd/goimports@release-branch.go1.15 + run: go install golang.org/x/tools/cmd/goimports@latest - name: Set up Python uses: actions/setup-python@v5 with: @@ -151,6 +155,7 @@ jobs: XUNIT_SHARD: ${{ matrix.shard }} XUNIT_SHARD_COUNT: ${{ inputs.num_shards }} DAFNY_RELEASE: ${{ github.workspace }}\unzippedRelease\dafny + DAFNY_INTEGRATION_TESTS_ONLY_COMPILERS: ${{ inputs.compilers }} run: | cmd /c mklink D:\a\dafny\dafny\unzippedRelease\dafny\z3\bin\z3-4.12.1 D:\a\dafny\dafny\unzippedRelease\dafny\z3\bin\z3-4.12.1.exe dotnet test --logger trx --logger "console;verbosity=normal" --collect:"XPlat Code Coverage" --settings dafny/Source/IntegrationTests/coverlet.runsettings dafny/Source/IntegrationTests/IntegrationTests.csproj @@ -167,6 +172,7 @@ jobs: env: XUNIT_SHARD: ${{ matrix.shard }} XUNIT_SHARD_COUNT: ${{ inputs.num_shards }} + DAFNY_INTEGRATION_TESTS_ONLY_COMPILERS: ${{ inputs.compilers }} run: | ${{ inputs.all_platforms }} && export DAFNY_RELEASE="${{ github.workspace }}/unzippedRelease/dafny" dotnet test --logger trx --logger "console;verbosity=normal" --collect:"XPlat Code Coverage" --settings dafny/Source/IntegrationTests/coverlet.runsettings dafny/Source/IntegrationTests diff --git a/.github/workflows/msbuild.yml b/.github/workflows/msbuild.yml index ee69aec54c3..a36595910f6 100644 --- a/.github/workflows/msbuild.yml +++ b/.github/workflows/msbuild.yml @@ -37,7 +37,7 @@ jobs: run: dotnet tool restore - name: Check whitespace and style working-directory: dafny - run: dotnet format whitespace Source/Dafny.sln --verify-no-changes --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs + run: dotnet format whitespace Source/Dafny.sln --verify-no-changes --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs - name: Get Boogie Version run: | sudo apt-get update @@ -67,7 +67,7 @@ jobs: integration-tests: needs: check-deep-tests - if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' ))) + if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests') || contains(github.event.pull_request.labels.*.name, 'run-integration-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' ))) uses: ./.github/workflows/integration-tests-reusable.yml with: ref: ${{ github.ref }} @@ -76,6 +76,8 @@ jobs: # This is the best way to fix an issue in master that was only caught by the nightly build. all_platforms: ${{ contains(github.event.pull_request.labels.*.name, 'run-deep-tests') || contains(github.event.push.labels.*.name, 'run-deep-tests')}} num_shards: 5 + # Omit Rust in the nightly build (or rather simulating it here) because Rust is known to have random issues + compilers: ${{ (contains(github.event.pull_request.labels.*.name, 'run-deep-tests') || contains(github.event.push.labels.*.name, 'run-deep-tests')) && 'cs,java,go,js,cpp,dfy,py' || '' }} test-coverage-analysis: runs-on: ubuntu-20.04 @@ -159,7 +161,7 @@ jobs: output: both # Fail if less than 86% total coverage, measured across all packages combined. # Report "yellow" status if less than 90% total coverage. - thresholds: '86 90' + thresholds: '85 90' - name: Code coverage report (LSP) uses: irongut/CodeCoverageSummary@v1.3.0 diff --git a/.github/workflows/nightly-build-reusable.yml b/.github/workflows/nightly-build-reusable.yml index 6eaf53fa2b1..4b659ebba7b 100644 --- a/.github/workflows/nightly-build-reusable.yml +++ b/.github/workflows/nightly-build-reusable.yml @@ -25,7 +25,9 @@ jobs: with: ref: ${{ inputs.ref }} all_platforms: true - num_shards: 5 + num_shards: 10 + # Omit Rust because Rust is known to have random issues + compilers: cs,java,go,js,cpp,dfy,py determine-vars: if: github.repository_owner == 'dafny-lang' && inputs.publish-prerelease diff --git a/.github/workflows/publish-release-reusable.yml b/.github/workflows/publish-release-reusable.yml index a86b9e1edeb..d288548bf83 100644 --- a/.github/workflows/publish-release-reusable.yml +++ b/.github/workflows/publish-release-reusable.yml @@ -35,7 +35,7 @@ env: jobs: publish-release: - runs-on: macos-latest # Put back 'ubuntu-20.04' if macos-latest fails in any way + runs-on: macos-13 # Put back 'ubuntu-20.04' if macos-latest fails in any way steps: - name: Print version run: echo ${{ inputs.name }} diff --git a/.github/workflows/release-brew.yml b/.github/workflows/release-brew.yml index 00c910954f9..c6867f03326 100644 --- a/.github/workflows/release-brew.yml +++ b/.github/workflows/release-brew.yml @@ -10,7 +10,7 @@ concurrency: jobs: build: - runs-on: macos-latest + runs-on: macos-13 steps: - name: Install dafny diff --git a/.github/workflows/release-downloads-nuget.yml b/.github/workflows/release-downloads-nuget.yml index 31d0e91d585..09c25932a11 100644 --- a/.github/workflows/release-downloads-nuget.yml +++ b/.github/workflows/release-downloads-nuget.yml @@ -32,7 +32,7 @@ jobs: fail-fast: false matrix: # This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906 - os: [ ubuntu-22.04, ubuntu-20.04, macos-11, windows-2019 ] + os: [ ubuntu-22.04, ubuntu-20.04, macos-13, windows-2019 ] steps: - name: OS @@ -85,7 +85,7 @@ jobs: excludes: prerelease, draft - name: Verify Dafny version if: "${{ steps.dafny.outputs.release != '' }}" - run: version="${{ steps.dafny.outputs.release }}"; dafny -version | grep -iE "Dafny "${version:1}".[0-9]{5}" + run: version="${{ steps.dafny.outputs.release }}"; dafny -version | grep -iE "Dafny "${version:1}".[0-9]+" shell: bash ## Check that a simple program compiles and runs on each supported platform ## Now that the dotnet tool distribution doesn't include the Scripts, @@ -111,7 +111,7 @@ jobs: # but note we need to skip Dafny since nuget install doesn't work for dotnet tools. library-name: [ DafnyPipeline, DafnyServer, DafnyLanguageServer, DafnyRuntime, DafnyCore, DafnyDriver ] # This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906 - os: [ ubuntu-latest, ubuntu-20.04, macos-latest, windows-2019 ] + os: [ ubuntu-latest, ubuntu-20.04, macos-13, windows-2019 ] steps: # Verify that the dependencies of the libraries we publish (e.g. DafnyLanguageServer) diff --git a/.github/workflows/release-downloads.yml b/.github/workflows/release-downloads.yml index f6158a53d4c..74c68178672 100644 --- a/.github/workflows/release-downloads.yml +++ b/.github/workflows/release-downloads.yml @@ -18,14 +18,14 @@ jobs: fail-fast: false matrix: # This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906 - os: [ ubuntu-latest, ubuntu-20.04, macos-latest, windows-2019 ] + os: [ ubuntu-latest, ubuntu-20.04, macos-13, windows-2019 ] include: - os: 'ubuntu-latest' osn: 'ubuntu-20.04' - os: 'ubuntu-20.04' osn: 'ubuntu-20.04' - - os: 'macos-latest' - osn: 'x64-macos-11' + - os: 'macos-13' + osn: 'x64-macos-13' - os: 'windows-2019' osn: 'windows-2019' # There is no hosted environment for Ubuntu 14.04 or for debian diff --git a/.github/workflows/runtime-tests.yml b/.github/workflows/runtime-tests.yml index 5f2db0e25dd..c3756189bd9 100644 --- a/.github/workflows/runtime-tests.yml +++ b/.github/workflows/runtime-tests.yml @@ -33,12 +33,12 @@ jobs: - name: Set up Go uses: actions/setup-go@v5 with: - go-version: '1.15' + go-version: '1.21' cache: false - name: Set up goimports env: GO111MODULE: on - run: go get golang.org/x/tools/cmd/goimports@release-branch.go1.15 + run: go install golang.org/x/tools/cmd/goimports@latest - name: Build Dafny run: dotnet build Source/Dafny.sln - name: Get Z3 @@ -48,7 +48,7 @@ jobs: cd ./Source/DafnyCore make test make check-format - - name: Test DafnyRuntime (C#) + - name: Test DafnyRuntime (C#, Rust) run: | cd ./Source/DafnyRuntime make all @@ -72,3 +72,7 @@ jobs: run: | cd ./Source/DafnyRuntime/DafnyRuntimeJs make all + - name: Test DafnyRuntimeRust + run: | + cd ./Source/DafnyRuntime/DafnyRuntimeRust + make all diff --git a/.github/workflows/standard-libraries.yml b/.github/workflows/standard-libraries.yml index d79e0df0e8d..dd966bbc82f 100644 --- a/.github/workflows/standard-libraries.yml +++ b/.github/workflows/standard-libraries.yml @@ -17,7 +17,7 @@ jobs: build: needs: check-deep-tests if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' ))) - runs-on: macos-latest + runs-on: macos-13 steps: - name: Checkout Dafny @@ -32,12 +32,12 @@ jobs: - name: Set up Go uses: actions/setup-go@v5 with: - go-version: '1.15' + go-version: '1.21' cache: false - name: Set up goimports env: GO111MODULE: on - run: go get golang.org/x/tools/cmd/goimports@release-branch.go1.15 + run: go install golang.org/x/tools/cmd/goimports@latest - name: Build Dafny run: dotnet build Source/Dafny.sln - name: Get Z3 diff --git a/.github/workflows/xunit-tests-reusable.yml b/.github/workflows/xunit-tests-reusable.yml index b4f7c95c86c..68576f2315f 100644 --- a/.github/workflows/xunit-tests-reusable.yml +++ b/.github/workflows/xunit-tests-reusable.yml @@ -2,7 +2,17 @@ name: Run XUnit tests on: workflow_dispatch: + inputs: + soak_test: + required: false + type: boolean + default: false workflow_call: + inputs: + soak_test: + required: false + type: boolean + default: false ## In the matrix: ## os - name of the Github actions runner @@ -15,15 +25,34 @@ defaults: working-directory: dafny jobs: + populate-matrix-dimensions: + runs-on: ubuntu-latest + steps: + - name: Populate iterations (normal mode) + id: populate-iterations-normal + if: "!inputs.soak_test" + working-directory: . + run: echo "iterations=[1]" >> $GITHUB_OUTPUT + - name: Populate iterations (soak test mode) + id: populate-iterations-soak + if: inputs.soak_test + working-directory: . + run: echo "iterations=[`seq -s , 1 5`]" >> $GITHUB_OUTPUT + outputs: + iterations: ${{ steps.populate-iterations-normal.outputs.iterations }} ${{ steps.populate-iterations-soak.outputs.iterations }} + build: + needs: populate-matrix-dimensions runs-on: ${{matrix.os}} timeout-minutes: 60 - name: ${{matrix.suffix}} + name: ${{matrix.suffix}} (${{matrix.iteration}}) strategy: fail-fast: false matrix: + os: [ubuntu-20.04, windows-2019, macos-13] + iteration: ${{ fromJson(needs.populate-matrix-dimensions.outputs.iterations) }} include: - - os: macos-11 + - os: macos-13 suffix: osx chmod: true - os: windows-2019 @@ -34,7 +63,7 @@ jobs: chmod: true env: solutionPath: Source/Dafny.sln - z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02 + z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2024-04-10 Logging__LogLevel__Microsoft: Debug steps: - uses: actions/checkout@v4 @@ -66,27 +95,34 @@ jobs: - name: Build run: dotnet build --no-restore ${{env.solutionPath}} - name: Run DafnyCore Tests + if: "!inputs.soak_test" run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyCore.Test/coverlet.runsettings Source/DafnyCore.Test + - name: Run DafnyLanguageServer Tests (soak test - iteration ${{matrix.iteration}}) + if: inputs.soak_test + run: | + dotnet test --no-restore --blame-crash --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyLanguageServer.Test/coverlet.runsettings Source/DafnyLanguageServer.Test - name: Run DafnyLanguageServer Tests + if: "!inputs.soak_test" run: | - ## Run twice to catch unstable code (Issue #2673) - dotnet test --no-restore --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyLanguageServer.Test/coverlet.runsettings Source/DafnyLanguageServer.Test - ## On the second run, collect test coverage data ## Note that, for some mysterious reason, --collect doesn't work with the DafnyLanguageServer.Test package dotnet coverage collect -o DafnyLanguageServer.Test.coverage dotnet test --no-restore --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx Source/DafnyLanguageServer.Test - - name: Run DafnyDriver Tests + if: "!inputs.soak_test" run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyDriver.Test/coverlet.runsettings Source/DafnyDriver.Test - name: Run DafnyPipeline Tests + if: "!inputs.soak_test" run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyPipeline.Test/coverlet.runsettings Source/DafnyPipeline.Test - name: Run DafnyTestGeneration Tests - run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyTestGeneration.Test/coverlet.runsettings Source/DafnyTestGeneration.Test + if: "!inputs.soak_test" + run: dotnet test --no-restore --blame-hang-timeout 5m --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyTestGeneration.Test/coverlet.runsettings Source/DafnyTestGeneration.Test - name: Run AutoExtern Tests + if: "!inputs.soak_test" run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/AutoExtern.Test/coverlet.runsettings Source/AutoExtern.Test - name: Run DafnyRuntime Tests + if: "!inputs.soak_test" run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyRuntime.Tests/coverlet.runsettings Source/DafnyRuntime.Tests - uses: actions/upload-artifact@v4 - if: always() + if: always() && !inputs.soak_test with: name: unit-test-results-${{ matrix.os }} path: | diff --git a/.gitignore b/.gitignore index 3a841b1d10a..beb07d34a9c 100644 --- a/.gitignore +++ b/.gitignore @@ -81,3 +81,12 @@ Source/IntegrationTests/TestFiles/LitTests/LitTest/server/*.bvd /Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/model Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/*.html Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/**/*.html +Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.dtr +/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libs/usesLibrary-lib +/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libs/usesLibrary.doo +Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.deps.json +Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.csproj +/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule2 +/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/PythonModule1 +/Source/DafnyCore/Prelude/DafnyPrelude.bpl +/Source/DafnyCore/Prelude/Sequences.bpl diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml index 9c4a8290fd2..46b4b28d51d 100644 --- a/.pre-commit-config.yaml +++ b/.pre-commit-config.yaml @@ -4,5 +4,6 @@ repos: - id: dotnet-format name: dotnet-format language: system - entry: dotnet format whitespace Source/Dafny.sln --include + entry: dotnet format whitespace Source/Dafny.sln -v:d --include + exclude: 'GeneratedFromDafny|Source/DafnyRuntime/DafnyRuntimeSystemModule.cs' types_or: ["c#"] diff --git a/Makefile b/Makefile index d6256e00c2e..05fff0ed28e 100644 --- a/Makefile +++ b/Makefile @@ -5,82 +5,114 @@ default: exe all: exe refman exe: - (cd ${DIR} ; dotnet build Source/Dafny.sln ) ## includes parser + (cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser -dfyprodformat: +format-dfy: (cd "${DIR}"/Source/DafnyCore ; ../../Binaries/Dafny.exe format .) -dfyprodinit: +dfy-to-cs: (cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh) -dfyprod: dfyprodformat dfyprodinit - (cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser +dfy-to-cs-exe: dfy-to-cs + (cd "${DIR}" ; dotnet build Source/Dafny.sln ) -dfydevinit: - (cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh --no-verify --no-format) +dfy-to-cs-noverify: + (cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh --no-verify) -dfydev: dfydevinit - (cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser +dfy-to-cs-noverify-exe: dfy-to-cs-noverify exe boogie: ${DIR}/boogie/Binaries/Boogie.exe tests: - (cd ${DIR}; dotnet test Source/IntegrationTests) + (cd "${DIR}"; dotnet test Source/IntegrationTests) + +# make test name= +test: + (cd "${DIR}"; dotnet test Source/IntegrationTests --filter "DisplayName~${name}") tests-verbose: - (cd ${DIR}; dotnet test --logger "console;verbosity=normal" Source/IntegrationTests ) + (cd "${DIR}"; dotnet test --logger "console;verbosity=normal" Source/IntegrationTests ) ${DIR}/boogie/Binaries/Boogie.exe: - (cd ${DIR}/boogie ; dotnet build -c Release Source/Boogie.sln ) + (cd "${DIR}"/boogie ; dotnet build -c Release Source/Boogie.sln ) refman: exe - make -C ${DIR}/docs/DafnyRef + make -C "${DIR}"/docs/DafnyRef refman-release: exe - make -C ${DIR}/docs/DafnyRef release + make -C "${DIR}"/docs/DafnyRef release z3-mac: - mkdir -p ${DIR}/Binaries/z3/bin + mkdir -p "${DIR}"/Binaries/z3/bin wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-macos-11-bin.zip unzip z3-4.12.1-x64-macos-11-bin.zip rm z3-4.12.1-x64-macos-11-bin.zip wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-macos-11-bin.zip unzip z3-4.8.5-x64-macos-11-bin.zip rm z3-4.8.5-x64-macos-11-bin.zip - mv z3-* ${DIR}/Binaries/z3/bin/ - chmod +x ${DIR}/Binaries/z3/bin/z3-* + mv z3-* "${DIR}"/Binaries/z3/bin/ + chmod +x "${DIR}"/Binaries/z3/bin/z3-* z3-mac-arm: - mkdir -p ${DIR}/Binaries/z3/bin + mkdir -p "${DIR}"/Binaries/z3/bin wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-arm64-macos-11-bin.zip unzip z3-4.12.1-arm64-macos-11-bin.zip rm z3-4.12.1-arm64-macos-11-bin.zip wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-macos-11-bin.zip unzip z3-4.8.5-x64-macos-11-bin.zip rm z3-4.8.5-x64-macos-11-bin.zip - mv z3-* ${DIR}/Binaries/z3/bin/ - chmod +x ${DIR}/Binaries/z3/bin/z3-* + mv z3-* "${DIR}"/Binaries/z3/bin/ + chmod +x "${DIR}"/Binaries/z3/bin/z3-* z3-ubuntu: - mkdir -p ${DIR}/Binaries/z3/bin + mkdir -p "${DIR}"/Binaries/z3/bin wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip unzip z3-4.12.1-x64-ubuntu-20.04-bin.zip rm z3-4.12.1-x64-ubuntu-20.04-bin.zip wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-ubuntu-20.04-bin.zip unzip z3-4.8.5-x64-ubuntu-20.04-bin.zip rm z3-4.8.5-x64-ubuntu-20.04-bin.zip - mv z3-* ${DIR}/Binaries/z3/bin/ - chmod +x ${DIR}/Binaries/z3/bin/z3-* + mv z3-* "${DIR}"/Binaries/z3/bin/ + chmod +x "${DIR}"/Binaries/z3/bin/z3-* format: - dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs + dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.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) - (cd ${DIR} ; dotnet build Source/Dafny.sln -v:q --nologo -target:clean ) - make -C ${DIR}/Source/DafnyCore -f Makefile clean - (cd ${DIR}/Source/Dafny && rm -rf Scanner.cs Parser.cs obj ) - (cd ${DIR}/Source/DafnyRuntime/DafnyRuntimeJava; ./gradlew clean) - make -C ${DIR}/docs/DafnyRef 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) + (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) + (cd "${DIR}" ; dotnet build Source/Dafny.sln -v:q --nologo -target:clean ) + make -C "${DIR}"/Source/DafnyCore -f Makefile clean + (cd "${DIR}"/Source/Dafny && rm -rf Scanner.cs Parser.cs obj ) + (cd "${DIR}"/Source/DafnyRuntime/DafnyRuntimeJava; ./gradlew clean) + make -C "${DIR}"/docs/DafnyRef 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) echo Source/*/bin Source/*/obj + +update-cs-module: + (cd "${DIR}"; cd Source/DafnyRuntime; make update-system-module) + +update-rs-module: + (cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeRust; make update-system-module) + +update-go-module: + (cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeGo; make update-system-module) + +update-runtime-dafny: + (cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeDafny; make update-go) + +pr-nogeneration: format-dfy format update-runtime-dafny update-cs-module update-rs-module update-go-module update-rs-module + +update-standard-libraries: + (cd "${DIR}"; cd Source/DafnyStandardLibraries; make update-binary) + +# `make pr` will bring you in a state suitable for submitting a PR +# - Builds the Dafny executable +# - Use the build to convert core .dfy files to .cs +# - Rebuilds the Dafny executable with this .cs files +# - Apply dafny format on all dfy files +# - Apply dotnet format on all cs files except the generated ones +# - Rebuild the Go and C# runtime modules as needed. +pr: exe dfy-to-cs-exe pr-nogeneration + +# Same as `make pr` but useful when resolving conflicts, to take the last compiled version of Dafny first +pr-conflict: dfy-to-cs-exe dfy-to-cs-exe pr-nogeneration diff --git a/README.md b/README.md index 9407f36d35e..ddaf9d5950c 100644 --- a/README.md +++ b/README.md @@ -21,7 +21,7 @@ This github site contains these materials: * the [issue tracker](https://github.com/dafny-lang/dafny/issues) * the wiki, including [frequently asked questions](https://github.com/dafny-lang/dafny/wiki/FAQ) -Documentation about the dafny language and tools is located +Documentation about the Dafny language and tools is located [here](https://dafny-lang.github.io/dafny). A reference manual is available both [online](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef) and as [pdf](https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/out/DafnyRef.pdf). (A LaTeX version can be produced if needed.) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 6124b11a42c..2e52b713dfc 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -2,6 +2,168 @@ See [docs/dev/news/](docs/dev/news/). +# 4.8.0 + +## New features + +- Introduce `hide` statements that enable hiding the body of a function at a particular proof location, which allows simplifying the verification of that proof in case the body of the function is not needed for the proof. `Hide` statements make the opaque keyword on functions obsolete. (https://github.com/dafny-lang/dafny/pull/5562) + +- Let the command `measure-complexity` output which verification tasks performed the worst in terms of resource count. Output looks like: + ... + Verification task on line 8 in file measure-complexity.dfy consumed 9984 resources + Verification task on line 7 in file measure-complexity.dfy consumed 9065 resources + ... + (https://github.com/dafny-lang/dafny/pull/5631) + +- Enable the option `--enforce-determinism` for the commands `resolve` and `verify` (https://github.com/dafny-lang/dafny/pull/5632) + +- Method calls get an optional by-proof that hides the precondtion and its proof (https://github.com/dafny-lang/dafny/pull/5662) + +## Bug fixes + +- Clarify error location of inlined `is` predicates. (https://github.com/dafny-lang/dafny/pull/5587) + +- Optimize the compilation of single-LHS assignment statements to allow the RHS to be a deeply nested expression. This solves a problem in compiling to Java, since `javac` does not deal gracefully with nested lambda expressions. (https://github.com/dafny-lang/dafny/pull/5589) + +- Crash when compiling an empty source file while including testing code (https://github.com/dafny-lang/dafny/pull/5638) + +- Let the options --print-mode=NoGhostOrIncludes and --print-mode=NoIncludes work (https://github.com/dafny-lang/dafny/pull/5645) + +- Verification in the IDE now works correctly when declaring nested module in a different file than their parent. (https://github.com/dafny-lang/dafny/pull/5650) + +- Fix NRE that would occur when using --legacy-data-constructors (https://github.com/dafny-lang/dafny/pull/5655) + +# 4.7.0 + +## New features + +- Add the option --find-project that given a Dafny file traverses up the file tree until it finds a Dafny project that includes that path. This is useful when developing a particular file and doing CLI invocations as part of your development workflow. + +- Improved error reporting when verification times out or runs out of resources, so that when using `--isolate-assertions`, the error message points to the problematic assertion. (https://github.com/dafny-lang/dafny/pull/5281) + +- Support newtypes based on map and imap (https://github.com/dafny-lang/dafny/pull/5175) + +- To enable smoothly working with multiple projects inside a single repository, Dafny now allows using a Dafny project file as an argument to `--library`. When using `dafny verify`, Dafny ensures that any dependencies specified through a project are verified as well, unless using the flag `--dont-verify-dependencies`. (https://github.com/dafny-lang/dafny/pull/5297) + +- Experimental Dafny-to-Rust compiler development + - Supports emitting code even if malformed with option `--emit-uncompilable-code`. + - Supports for immutable collections and operators + (https://github.com/dafny-lang/dafny/pull/5081) + +- Allow for plugins to add custom request handlers to the language server. (https://github.com/dafny-lang/dafny/pull/5161) + +- Deprecated the unicode-char option (https://github.com/dafny-lang/dafny/pull/5302) + +- Warn when passing a Dafny source file to `--library` (https://github.com/dafny-lang/dafny/pull/5313) + +- Add support for "translation records", which record the options used when translating library code. + * `--translation-record` - Provides a `.dtr` file from a previous translation of library code. Can be specified multiple times. + * `--translation-record-output` - Customizes where to write the translation record for the current translation. Defaults to the output directory. + Providing translation records is necessary to handle options such as `--outer-module` that affect how code is translated. + (https://github.com/dafny-lang/dafny/pull/5346) + +- The new `decreases to` expression makes it possible to write an explicit assertion equivalent to the internal check Dafny does to prove that a loop or recursive call terminates. (https://github.com/dafny-lang/dafny/pull/5367) + +- The new `assigned` expression makes it possible to explicitly assert that a variable, constant, out-parameter, or object field is definitely assigned. (https://github.com/dafny-lang/dafny/pull/5501) + +- Greatly reduced the size of generated code for the backends: C#, Python, GoLang and JavaScript. + +- Introduce additional warnings that previously only appeared when running the `dafny audit` command. Two warnings are as follows: + - Emit a warning when exporting a declaration that has requires clauses or subset type inputs + - Emit a warning when importing a declaration that has ensures clauses or subset type outputs +Those two can be silenced with the flag `--allow-external-contracts`. A third new warning occurs when using bodyless functions marked with `{:extern}`, and can be silenced using the option `--allow-external-function`. + +- Enable project files to specify another project file as a base, which copies all configuration from that base file. More information can be found in the reference manual. + +## Bug fixes + +- Fix a common memory leak that occurred when doing verification in the IDE that could easily consume gigabytes of memory. + +- Fix bugs that could cause the IDE to become unresponsive + +- Improve the performance of the Dafny IDE by fixing bugs in its caching code + +- No longer reuse SMT solver processes between different document version when using the IDE, making the IDE verification behavior more inline to that of the CLI + +- Fix bugs that caused Dafny IDE internal errors (https://github.com/dafny-lang/dafny/issues/5355, https://github.com/dafny-lang/dafny/pull/5543, https://github.com/dafny-lang/dafny/pull/5548) + +- Fix bugs in the Dafny IDEs code navigation and renaming features when working with definition that are not referred to. + +- Fix a code navigation bug that could occur when navigating to and from module imports +- +- Fix a code navigation bug that could occur when navigating to and from explicit types of variables + (https://github.com/dafny-lang/dafny/pull/5419) + +- Let the IDE no longer show diagnostics for projects for which all files have been closed (https://github.com/dafny-lang/dafny/pull/5437) + +- Fix bug that could lead to an unresponsive IDE when working with project files (https://github.com/dafny-lang/dafny/pull/5444) + +- Fix bugs in Dafny library files that could cause them not to work with certain option values, such as --function-syntax=3 + +- Fix a bug that prevented building Dafny libraries for Dafny projects that could verify without errors. + +- Reserved module identifiers correctly escaped in GoLang (https://github.com/dafny-lang/dafny/pull/4181) + +- Fix a soundness issue that could be triggered by calling ensures fresh in the post-condition of a constructor (https://github.com/dafny-lang/dafny/pull/4700) + +- Ability to cast a datatype to its trait when overriding functions (https://github.com/dafny-lang/dafny/pull/4823) + +- Fix crash that could occur when using a constructor in a match pattern where a tuple was expected (https://github.com/dafny-lang/dafny/pull/4860) + +- No longer emit an incorrect internal error while waiting for verification message (https://github.com/dafny-lang/dafny/pull/5209) + +- More helpful error messages when read fields not mentioned in reads clauses (https://github.com/dafny-lang/dafny/pull/5262) + +- Check datatype constructors for bad type-parameter instantiations (https://github.com/dafny-lang/dafny/pull/5278) + +- Avoid name clashes with Go built-in modules (https://github.com/dafny-lang/dafny/pull/5283) + +- Invalid Python code for nested set and map comprehensions (https://github.com/dafny-lang/dafny/pull/5287) + +- Stop incorrectly emitting the error message "Dafny encountered an internal error while waiting for this symbol to verify" (https://github.com/dafny-lang/dafny/pull/5295) + +- Rename the `dafny generate-tests` option `--coverage-report` to `--expected-coverage-report` (https://github.com/dafny-lang/dafny/pull/5301) + +- Stop giving an incorrect warning about a missing {:axiom} clause on an opaque constant. (https://github.com/dafny-lang/dafny/pull/5306) + +- No new resolver crash when datatype update expressions are partially resolved (https://github.com/dafny-lang/dafny/pull/5331) + +- Optional pre-type won't cause a crash anymore (https://github.com/dafny-lang/dafny/pull/5369) + +- Unguarded enumeration of bound variables in set and map comprehensions (https://github.com/dafny-lang/dafny/pull/5402) + +- Reference the correct `this` after removing the tail call of a function or method (https://github.com/dafny-lang/dafny/pull/5474) + +- Apply name mangling to datatype names in Python more often (https://github.com/dafny-lang/dafny/pull/5476) + +- Only guard `this` when eliminating tail calls, if possible (https://github.com/dafny-lang/dafny/pull/5524) + +- Compiled disjunctive nested pattern matching no longer crashing (https://github.com/dafny-lang/dafny/pull/5572) + +# 4.6.0 + +## New features + +- Add a check to `dafny run` that notifies the user when a value that was parsed as a user program argument, and which occurs before a `--` token, starts with `--`, since this indicates they probably mistyped a Dafny option name. (https://github.com/dafny-lang/dafny/pull/5097) + +- Add an option --progress that can be used to track the progress of verification. (https://github.com/dafny-lang/dafny/pull/5150) + +- Add the attribute `{:isolate_assertions}`, which does the same as `{:vcs_split_on_every_assert}`. Deprecated `{:vcs_split_on_every_assert}` (https://github.com/dafny-lang/dafny/pull/5247) + +## Bug fixes + +- (soundness issue) Twostate predicate now check if their not new arguments are allocated in the previous heap (https://github.com/dafny-lang/dafny/pull/4844) + +- Add uniform checking of type characteristics in refinement modules (https://github.com/dafny-lang/dafny/pull/5146) + +- Fixed links associated with the standard libraries. (https://github.com/dafny-lang/dafny/pull/5176) + +- fix: Disable the "erase datatype wrappers" optimization if the datatype implements any traits. + feat: Allow the "erase datatype wrappers" optimization if the only fields in the datatype are ghost fields. + (https://github.com/dafny-lang/dafny/pull/5234) + +- Fix the default string value emitted for JavaScript (https://github.com/dafny-lang/dafny/pull/5239) + # 4.5.0 ## New features diff --git a/Scripts/prepare_release.py b/Scripts/prepare_release.py index 1c6823e9bc1..bb625bb63c0 100755 --- a/Scripts/prepare_release.py +++ b/Scripts/prepare_release.py @@ -322,6 +322,18 @@ def _push_release_branch(self): self.REMOTE, f"{self.release_branch_path}:{self.release_branch_path}", check=True) + def set_next_version(self): + assert_one(f"Is {self.version} a valid version number?", + self._parse_vernum) + assert_one(f"Can we find `{self.build_props_path}`?", + self._build_props_file_exists) + assert_one(f"Can we parse `{self.build_props_path}`?", + self._build_props_file_parses) + assert_one(f"Can we create a section for `{self.version}` in `{self.release_notes_md_path}`?", + self._version_number_is_fresh) + run_one(f"Updating `{self.build_props_path}`...", + self._update_build_props_file) + # Still TODO: # - Run deep test as part of release workflow @@ -430,7 +442,7 @@ def parse_arguments() -> argparse.Namespace: parser.add_argument("--source-branch", help="Which branch to release from (optional, defaults to 'master')", default="master") parser.add_argument("version", help="Version number for this release (A.B.C-xyz)") parser.add_argument("action", help="Which part of the release process to run", - choices=["prepare", "release"]) + choices=["prepare", "release", "set-next-version"]) return parser.parse_args() def main() -> None: @@ -438,6 +450,7 @@ def main() -> None: try: release = (DryRunRelease if args.dry_run else Release)(args.version, args.source_branch) {"prepare": release.prepare, + "set-next-version": release.set_next_version, "release": release.release}[args.action]() except CannotReleaseError: sys.exit(1) diff --git a/Scripts/quicktest.sh b/Scripts/quicktest.sh index ae8053131b4..4909759f8e7 100755 --- a/Scripts/quicktest.sh +++ b/Scripts/quicktest.sh @@ -64,7 +64,7 @@ $DAFNY build -t:go c.dfy | diff - $tmp || exit 1 (cd c-go; GO111MODULE=auto GOPATH=`pwd` go run src/c.go) | diff - $tmpx || exit 1 echo Building with Python $DAFNY build -t:py c.dfy | diff - $tmp || exit 1 -python c-py/c.py | diff - $tmpx || exit 1 +python c-py/__main__.py | diff - $tmpx || exit 1 echo Building with Rust $DAFNY build -t:rs c.dfy | diff - $tmp || exit 1 ./c-rust/target/debug/c | diff - $tmpx || exit 1 diff --git a/Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect b/Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect index 03a358a4c2b..44366de2ee0 100644 --- a/Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect +++ b/Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect @@ -2,6 +2,7 @@ Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help Dafny program verifier did not attempt verification Wrote textual form of target program to GroceryListPrinter.cs +Additional output written to GroceryListPrinter-cs.dtr # Printing a grocery list (2 items in the list) ## Apple: 3 @ 1.00 diff --git a/Source/Dafny/Dafny.csproj b/Source/Dafny/Dafny.csproj index 0ac53285657..ff383440c30 100644 --- a/Source/Dafny/Dafny.csproj +++ b/Source/Dafny/Dafny.csproj @@ -6,6 +6,7 @@ true TRACE net6.0 + Major ..\..\Binaries\ false diff --git a/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj b/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj index d10cb4ca84e..9cf987817bc 100644 --- a/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj +++ b/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj @@ -2,6 +2,7 @@ net6.0 + Major enable enable ..\..\Binaries\ diff --git a/Source/DafnyCore.Test/ClonerTest.cs b/Source/DafnyCore.Test/ClonerTest.cs index eac50ae3280..5d7d645b769 100644 --- a/Source/DafnyCore.Test/ClonerTest.cs +++ b/Source/DafnyCore.Test/ClonerTest.cs @@ -1,6 +1,7 @@ using Microsoft.Dafny; using Microsoft.Extensions.Logging; using Microsoft.Extensions.Logging.Abstractions; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Tomlyn; namespace DafnyCore.Test; @@ -13,6 +14,11 @@ public DummyDecl(Cloner cloner, Declaration original) : base(cloner, original) { public DummyDecl(RangeToken rangeToken, Name name, Attributes attributes, bool isRefining) : base(rangeToken, name, attributes, isRefining) { } + + public override SymbolKind? Kind => null; + public override string GetDescription(DafnyOptions options) { + return ""; + } } [Fact] diff --git a/Source/DafnyCore.Test/DafnyProjectTest.cs b/Source/DafnyCore.Test/DafnyProjectTest.cs index ffc1167bcb6..891e2ecc38e 100644 --- a/Source/DafnyCore.Test/DafnyProjectTest.cs +++ b/Source/DafnyCore.Test/DafnyProjectTest.cs @@ -6,25 +6,22 @@ public class DafnyProjectTest { [Fact] public void Equality() { var randomFileName = Path.GetTempFileName(); - var first = new DafnyProject() { - Uri = new Uri(randomFileName, UriKind.Absolute), - Includes = new[] { "a", "a2" }, - Excludes = new[] { "b", "b2" }, - Options = new Dictionary() { + var first = new DafnyProject(new Uri(randomFileName, UriKind.Absolute), null, + new[] { "a", "a2" }.ToHashSet(), + new[] { "b", "b2" }.ToHashSet(), new Dictionary() { { "c", "d" }, { "e", "f" } } - }; + ); - var second = new DafnyProject() { - Uri = new Uri(randomFileName, UriKind.Absolute), - Includes = new[] { "a2", "a" }, - Excludes = new[] { "b2", "b" }, - Options = new Dictionary() { + var second = new DafnyProject(new Uri(randomFileName, UriKind.Absolute), null, + new[] { "a2", "a" }.ToHashSet(), + new[] { "b2", "b" }.ToHashSet(), + new Dictionary() { { "e", "f" }, { "c", "d" }, } - }; + ); Assert.Equal(first, second); diff --git a/Source/DafnyCore.Test/GeneratedDafnyTest.cs b/Source/DafnyCore.Test/GeneratedDafnyTest.cs new file mode 100644 index 00000000000..72600e6f7c6 --- /dev/null +++ b/Source/DafnyCore.Test/GeneratedDafnyTest.cs @@ -0,0 +1,11 @@ +using System.Collections.Concurrent; +using Microsoft.Dafny; + +namespace DafnyCore.Test; + +public class GeneratedDafnyTest { + [Fact] + public void TestDafnyGeneratedCode() { + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestExpr(); + } +} \ No newline at end of file diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs b/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs new file mode 100644 index 00000000000..8319b008012 --- /dev/null +++ b/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs @@ -0,0 +1,162 @@ +// Dafny program the_program compiled into C# +// To recompile, you will need the libraries +// System.Runtime.Numerics.dll System.Collections.Immutable.dll +// but the 'dotnet' tool in net6.0 should pick those up automatically. +// Optionally, you may want to include compiler switches like +// /debug /nowarn:162,164,168,183,219,436,1717,1718 + +using System; +using System.Numerics; +using System.Collections; +#pragma warning disable CS0164 // This label has not been referenced +#pragma warning disable CS0162 // Unreachable code detected +#pragma warning disable CS1717 // Assignment made to same variable + +namespace DafnyToRustCompilerCoverage.RASTCoverage { + + public partial class __default { + public static void TestExpr() + { + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestOptimizeToString(); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestPrintingInfo(); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoExtraSemicolonAfter(); + FactorPathsOptimizationTest.__default.TestApply(); + } + public static void TestNoOptimize(RAST._IExpr e) + { + } + public static RAST._IExpr ConversionNum(RAST._IType t, RAST._IExpr x) + { + return RAST.Expr.create_Call(RAST.Expr.create_ExprFromPath(RAST.Path.create_PMemberSelect(RAST.Path.create_PMemberSelect(RAST.Path.create_Global(), Dafny.Sequence.UnicodeFromString("dafny_runtime")), Dafny.Sequence.UnicodeFromString("truncate!"))), Dafny.Sequence.FromElements(x, RAST.Expr.create_ExprFromType(t))); + } + public static RAST._IExpr DafnyIntLiteral(Dafny.ISequence s) { + return RAST.Expr.create_Call(RAST.Expr.create_ExprFromPath(RAST.Path.create_PMemberSelect(RAST.__default.dafny__runtime, Dafny.Sequence.UnicodeFromString("int!"))), Dafny.Sequence.FromElements(RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("1")))); + } + public static void TestOptimizeToString() + { + RAST._IExpr _0_x; + _0_x = RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")); + RAST._IExpr _1_y; + _1_y = RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("y")); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), RAST.Expr.create_Call(RAST.Expr.create_Select(_0_x, Dafny.Sequence.UnicodeFromString("clone")), Dafny.Sequence.FromElements()), DAST.Format.UnaryOpFormat.create_NoFormat())).Optimize(), RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), _0_x, DAST.Format.UnaryOpFormat.create_NoFormat()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), RAST.Expr.create_Call(RAST.Expr.create_Select(_0_x, Dafny.Sequence.UnicodeFromString("clone")), Dafny.Sequence.FromElements(_1_y)), DAST.Format.UnaryOpFormat.create_NoFormat())); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("=="), _0_x, _1_y, DAST.Format.BinaryOpFormat.create_NoFormat()), DAST.Format.UnaryOpFormat.create_CombineFormat())).Optimize(), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("!="), _0_x, _1_y, DAST.Format.BinaryOpFormat.create_NoFormat()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<"), _0_x, _1_y, DAST.Format.BinaryOpFormat.create_NoFormat()), DAST.Format.UnaryOpFormat.create_CombineFormat())).Optimize(), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">="), _0_x, _1_y, DAST.Format.BinaryOpFormat.create_NoFormat()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<"), _0_x, _1_y, DAST.Format.BinaryOpFormat.create_ReverseFormat()), DAST.Format.UnaryOpFormat.create_CombineFormat())).Optimize(), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<="), _1_y, _0_x, DAST.Format.BinaryOpFormat.create_NoFormat()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_I128(), DafnyToRustCompilerCoverage.RASTCoverage.__default.DafnyIntLiteral(Dafny.Sequence.UnicodeFromString("1")))).Optimize(), RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("1")))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_I128(), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("z"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), RAST.Expr.create_StmtExpr(RAST.__default.AssignVar(Dafny.Sequence.UnicodeFromString("z"), _1_y), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("return"))))).Optimize(), RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("z"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_Some(_1_y)), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("return"))))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("z"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), RAST.Expr.create_StmtExpr(RAST.__default.AssignVar(Dafny.Sequence.UnicodeFromString("w"), _1_y), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("return"))))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(_0_x); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(_0_x, _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_Match(_0_x, Dafny.Sequence.FromElements()), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_StructBuild(_0_x, Dafny.Sequence.FromElements()), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_Tuple(Dafny.Sequence.FromElements()), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), _0_x, DAST.Format.UnaryOpFormat.create_NoFormat()), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("&&"), _0_x, _0_x, DAST.Format.BinaryOpFormat.create_NoFormat()), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_TypeAscription(_0_x, RAST.Type.create_I128()), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("1")), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("2"), true, false), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("3"), false, true), _0_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("z"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), RAST.Expr.create_StmtExpr(RAST.__default.AssignVar(Dafny.Sequence.UnicodeFromString("z"), _1_y), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("return"))))).Optimize(), RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("z"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_Some(_1_y)), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("return"))))); + Dafny.ISequence _2_coverageExpression; + _2_coverageExpression = Dafny.Sequence.FromElements(RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("abc")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Match(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.FromElements(RAST.MatchCase.create(Dafny.Sequence.UnicodeFromString("abc"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))))), RAST.Expr.create_StmtExpr(RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("panic!()")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("a"))), RAST.Expr.create_Block(RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("abc"))), RAST.Expr.create_StructBuild(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("dummy")), Dafny.Sequence.FromElements(RAST.AssignIdentifier.create(Dafny.Sequence.UnicodeFromString("foo"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("bar"))))), RAST.Expr.create_StructBuild(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("dummy")), Dafny.Sequence.FromElements(RAST.AssignIdentifier.create(Dafny.Sequence.UnicodeFromString("foo"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("bar"))), RAST.AssignIdentifier.create(Dafny.Sequence.UnicodeFromString("foo2"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("bar"))))), RAST.Expr.create_Tuple(Dafny.Sequence.FromElements(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")))), RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("-"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), DAST.Format.UnaryOpFormat.create_NoFormat()), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("+"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("y")), DAST.Format.BinaryOpFormat.create_NoFormat()), RAST.Expr.create_TypeAscription(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Type.create_I128()), RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("322")), RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("abc"), true, false), RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("abc"), false, true), RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("abc"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), RAST.Expr.create_DeclareVar(RAST.DeclareType.create_CONST(), Dafny.Sequence.UnicodeFromString("abc"), Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")))), RAST.__default.AssignVar(Dafny.Sequence.UnicodeFromString("abc"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_IfExpr(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_Loop(Std.Wrappers.Option.create_Some(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_For(Dafny.Sequence.UnicodeFromString("abc"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_Labelled(Dafny.Sequence.UnicodeFromString("abc"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_Break(Std.Wrappers.Option>.create_None()), RAST.Expr.create_Break(Std.Wrappers.Option>.create_Some(Dafny.Sequence.UnicodeFromString("l"))), RAST.Expr.create_Continue(Std.Wrappers.Option>.create_None()), RAST.Expr.create_Continue(Std.Wrappers.Option>.create_Some(Dafny.Sequence.UnicodeFromString("l"))), RAST.Expr.create_Return(Std.Wrappers.Option.create_None()), RAST.Expr.create_Return(Std.Wrappers.Option.create_Some(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")))), RAST.Expr.create_Call(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.FromElements()), RAST.Expr.create_Call(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.FromElements(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("y")))), RAST.Expr.create_CallType(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.FromElements(RAST.Type.create_I128(), RAST.Type.create_U32())), RAST.Expr.create_Select(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.UnicodeFromString("abc")), RAST.Expr.create_ExprFromPath(RAST.Path.create_PMemberSelect(RAST.Path.create_Crate(), Dafny.Sequence.UnicodeFromString("abc"))), RAST.Expr.create_ExprFromPath(RAST.Path.create_PMemberSelect(RAST.Path.create_Global(), Dafny.Sequence.UnicodeFromString("abc")))); + BigInteger _hi0 = new BigInteger((_2_coverageExpression).Count); + for (BigInteger _3_i = BigInteger.Zero; _3_i < _hi0; _3_i++) { + RAST._IExpr _4_c; + _4_c = (_2_coverageExpression).Select(_3_i); + RAST._IPrintingInfo _5___v0; + _5___v0 = (_4_c).printingInfo; + RAST._IExpr _6___v1; + _6___v1 = (_4_c).Optimize(); + Dafny.IMap> _7___v2; + _7___v2 = Dafny.Map>.FromElements(new Dafny.Pair>(_4_c, (_4_c)._ToString(Dafny.Sequence.UnicodeFromString("")))); + RAST._IExpr _8___v3; + _8___v3 = (RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("abc"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), _4_c)).Optimize(); + RAST._IExpr _9___v4; + _9___v4 = (RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("abc"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), RAST.Expr.create_StmtExpr(RAST.__default.AssignVar(Dafny.Sequence.UnicodeFromString("abc"), _4_c), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString(""))))).Optimize(); + RAST._IExpr _10___v5; + _10___v5 = (RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), _4_c, DAST.Format.UnaryOpFormat.create_NoFormat())).Optimize(); + RAST._IExpr _11___v6; + _11___v6 = (RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), _4_c, DAST.Format.UnaryOpFormat.create_NoFormat())).Optimize(); + RAST._IExpr _12___v7; + _12___v7 = (DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_U8(), _4_c)).Optimize(); + RAST._IExpr _13___v8; + _13___v8 = (DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_U8(), RAST.Expr.create_Call(_4_c, Dafny.Sequence.FromElements()))).Optimize(); + Std.Wrappers._IOption> _14___v9; + _14___v9 = (_4_c).RightMostIdentifier(); + } + } + public static void TestPrintingInfo() + { + RAST._IExpr _0_x; + _0_x = RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")); + RAST._IExpr _1_y; + _1_y = RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("y")); + DAST.Format._IBinaryOpFormat _2_bnf; + _2_bnf = DAST.Format.BinaryOpFormat.create_NoFormat(); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(((RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("x"))).printingInfo).is_UnknownPrecedence); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((_0_x).printingInfo, RAST.PrintingInfo.create_Precedence(BigInteger.One))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("3"))).printingInfo, RAST.PrintingInfo.create_Precedence(BigInteger.One))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("abc"), true, false)).printingInfo, RAST.PrintingInfo.create_Precedence(BigInteger.One))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("?"), _0_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_SuffixPrecedence(new BigInteger(5)))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("-"), _0_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_Precedence(new BigInteger(6)))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("*"), _0_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_Precedence(new BigInteger(6)))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), _0_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_Precedence(new BigInteger(6)))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), _0_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_Precedence(new BigInteger(6)))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&mut"), _0_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_Precedence(new BigInteger(6)))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!!"), _0_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_UnknownPrecedence())); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_Select(_0_x, Dafny.Sequence.UnicodeFromString("name"))).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(2), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_ExprFromPath(RAST.Path.create_PMemberSelect(RAST.Path.create_Global(), Dafny.Sequence.UnicodeFromString("name")))).printingInfo, RAST.PrintingInfo.create_Precedence(new BigInteger(2)))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_Call(_0_x, Dafny.Sequence.FromElements())).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(2), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_TypeAscription(_0_x, RAST.Type.create_I128())).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(10), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("*"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(20), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("/"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(20), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("%"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(20), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("+"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(30), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("-"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(30), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<<"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(40), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">>"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(40), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("&"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(50), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("^"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(60), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("|"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(70), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("=="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("!="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("&&"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(90), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("||"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(100), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(".."), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("..="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("+="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("-="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("*="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("/="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("%="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("&="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("|="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("^="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<<="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">>="), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("?!?"), _0_x, _1_y, _2_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(BigInteger.Zero, RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_Break(Std.Wrappers.Option>.create_None())).printingInfo, RAST.PrintingInfo.create_UnknownPrecedence())); + } + public static void AssertCoverage(bool x) + { + } + public static void TestNoExtraSemicolonAfter() + { + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage((RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString(";"))).NoExtraSemicolonAfter()); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(!((RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("a"))).NoExtraSemicolonAfter())); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage((RAST.Expr.create_Return(Std.Wrappers.Option.create_None())).NoExtraSemicolonAfter()); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage((RAST.Expr.create_Continue(Std.Wrappers.Option>.create_None())).NoExtraSemicolonAfter()); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage((RAST.Expr.create_Break(Std.Wrappers.Option>.create_None())).NoExtraSemicolonAfter()); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage((RAST.__default.AssignVar(Dafny.Sequence.UnicodeFromString("x"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("y")))).NoExtraSemicolonAfter()); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage((RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("x"), Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_None())).NoExtraSemicolonAfter()); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(!((RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))).NoExtraSemicolonAfter())); + } + } +} // end of namespace DafnyToRustCompilerCoverage.RASTCoverage \ No newline at end of file diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs b/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs new file mode 100644 index 00000000000..619b9656ad7 --- /dev/null +++ b/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs @@ -0,0 +1,47 @@ +// Dafny program the_program compiled into C# +// To recompile, you will need the libraries +// System.Runtime.Numerics.dll System.Collections.Immutable.dll +// but the 'dotnet' tool in net6.0 should pick those up automatically. +// Optionally, you may want to include compiler switches like +// /debug /nowarn:162,164,168,183,219,436,1717,1718 + +using System; +using System.Numerics; +using System.Collections; +#pragma warning disable CS0164 // This label has not been referenced +#pragma warning disable CS0162 // Unreachable code detected +#pragma warning disable CS1717 // Assignment made to same variable + +namespace FactorPathsOptimizationTest { + + public partial class __default { + public static void ShouldBeEqual(RAST._IMod a, RAST._IMod b) + { + Dafny.ISequence _0_sA; + _0_sA = (a)._ToString(Dafny.Sequence.UnicodeFromString("")); + Dafny.ISequence _1_sB; + _1_sB = (b)._ToString(Dafny.Sequence.UnicodeFromString("")); + if (!(_0_sA).Equals(_1_sB)) { + Dafny.Helpers.Print((Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("Got:\n"), _0_sA), Dafny.Sequence.UnicodeFromString("\n"))).ToVerbatimString(false)); + Dafny.Helpers.Print((Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("Expected:\n"), _1_sB), Dafny.Sequence.UnicodeFromString("\n"))).ToVerbatimString(false)); + if (!((_0_sA).Equals(_1_sB))) { + throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-path-simplification.dfy(12,6): " + Dafny.Sequence.UnicodeFromString("expectation violation").ToVerbatimString(false));} + } + } + public static void TestApply() + { + RAST._ITypeParamDecl _0_T__Decl; + _0_T__Decl = RAST.TypeParamDecl.create(Dafny.Sequence.UnicodeFromString("T"), Dafny.Sequence.FromElements(RAST.__default.DafnyType)); + RAST._ITypeParamDecl _1_T__Decl__simp; + _1_T__Decl__simp = RAST.TypeParamDecl.create(Dafny.Sequence.UnicodeFromString("T"), Dafny.Sequence.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("DafnyType")))); + RAST._IType _2_T; + _2_T = RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("T")); + RAST._IPath _3_std__any__Any; + _3_std__any__Any = (((RAST.__default.@global).MSel(Dafny.Sequence.UnicodeFromString("std"))).MSel(Dafny.Sequence.UnicodeFromString("any"))).MSel(Dafny.Sequence.UnicodeFromString("Any")); + RAST._IType _4_Any; + _4_Any = RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("Any")); + FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence>.FromElements(), Dafny.Sequence.FromElements(RAST.ModDecl.create_StructDecl(RAST.Struct.create(Dafny.Sequence>.FromElements(), Dafny.Sequence.UnicodeFromString("test"), Dafny.Sequence.FromElements(_0_T__Decl), RAST.Fields.create_NamedFields(Dafny.Sequence.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence.UnicodeFromString("a"), (_3_std__any__Any).AsType())))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence.FromElements(_0_T__Decl), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.UnicodeFromString(""), Dafny.Sequence.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence.FromElements(_0_T__Decl), (_3_std__any__Any).AsType(), ((((RAST.__default.crate).MSel(Dafny.Sequence.UnicodeFromString("onemodule"))).MSel(Dafny.Sequence.UnicodeFromString("test"))).AsType()).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.UnicodeFromString(""), Dafny.Sequence.FromElements()))))), RAST.Mod.create_Mod(Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence>.FromElements(), Dafny.Sequence.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), _3_std__any__Any)), RAST.ModDecl.create_StructDecl(RAST.Struct.create(Dafny.Sequence>.FromElements(), Dafny.Sequence.UnicodeFromString("test"), Dafny.Sequence.FromElements(_1_T__Decl__simp), RAST.Fields.create_NamedFields(Dafny.Sequence.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence.UnicodeFromString("a"), _4_Any)))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.UnicodeFromString(""), Dafny.Sequence.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence.FromElements(_1_T__Decl__simp), _4_Any, (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.UnicodeFromString(""), Dafny.Sequence.FromElements()))))); + FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence>.FromElements(), Dafny.Sequence.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence.FromElements(_0_T__Decl), (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("UpcastObject"))).AsType()).Apply(Dafny.Sequence.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.UnicodeFromString(""), Dafny.Sequence.FromElements()))))), RAST.Mod.create_Mod(Dafny.Sequence.UnicodeFromString("onemodule"), Dafny.Sequence>.FromElements(), Dafny.Sequence.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("UpcastObject")))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("UpcastObject"))).Apply(Dafny.Sequence.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence.UnicodeFromString("test"))).Apply(Dafny.Sequence.FromElements(_2_T)), Dafny.Sequence.UnicodeFromString(""), Dafny.Sequence.FromElements()))))); + } + } +} // end of namespace FactorPathsOptimizationTest \ No newline at end of file diff --git a/Source/DafnyCore/AST/AstVisitor.cs b/Source/DafnyCore/AST/AstVisitor.cs index f9922cd68ea..cf1388b50d9 100644 --- a/Source/DafnyCore/AST/AstVisitor.cs +++ b/Source/DafnyCore/AST/AstVisitor.cs @@ -136,12 +136,12 @@ public virtual void VisitFunction(Function function) { VisitAttributes(function, function.EnclosingClass.EnclosingModuleDefinition); - foreach (var formal in function.Formals) { + foreach (var formal in function.Ins) { VisitUserProvidedType(formal.Type, context); } VisitUserProvidedType(function.ResultType, context); - VisitDefaultParameterValues(function.Formals, context); + VisitDefaultParameterValues(function.Ins, context); function.Req.ForEach(aexpr => VisitAttributedExpression(aexpr, context)); @@ -328,12 +328,12 @@ protected virtual void VisitStatement(Statement stmt, VisitorContext context) { // Visit user-provided types if (stmt is VarDeclStmt varDeclStmt) { foreach (var local in varDeclStmt.Locals) { - VisitUserProvidedType(local.OptionalType, context); + VisitUserProvidedType(local.SyntacticType, context); } } else if (stmt is VarDeclPattern varDeclPattern) { foreach (var local in varDeclPattern.LocalVars) { - VisitUserProvidedType(local.OptionalType, context); + VisitUserProvidedType(local.SyntacticType, context); } } else if (stmt is AssignStmt assignStmt) { diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index 36fef7059bc..d42e6358abc 100644 --- a/Source/DafnyCore/AST/Cloner.cs +++ b/Source/DafnyCore/AST/Cloner.cs @@ -86,12 +86,13 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne } else if (d is NewtypeDecl) { var dd = (NewtypeDecl)d; if (dd.Var == null) { - return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, CloneType(dd.BaseType), + return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), dd.TypeArgs.ConvertAll(CloneTypeParam), newParent, + CloneType(dd.BaseType), dd.WitnessKind, CloneExpr(dd.Witness), dd.ParentTraits.ConvertAll(CloneType), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); } else { - return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, CloneBoundVar(dd.Var, false), - CloneExpr(dd.Constraint), dd.WitnessKind, CloneExpr(dd.Witness), + return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), dd.TypeArgs.ConvertAll(CloneTypeParam), newParent, + CloneBoundVar(dd.Var, false), CloneExpr(dd.Constraint), dd.WitnessKind, CloneExpr(dd.Witness), dd.ParentTraits.ConvertAll(CloneType), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); } @@ -194,7 +195,7 @@ public DatatypeCtor CloneCtor(DatatypeCtor ct) { public TypeParameter CloneTypeParam(TypeParameter tp) { return (TypeParameter)typeParameterClones.GetOrCreate(tp, () => new TypeParameter(Range(tp.RangeToken), tp.NameNode.Clone(this), tp.VarianceSyntax, - CloneTPChar(tp.Characteristics))); + CloneTPChar(tp.Characteristics), tp.TypeBounds.ConvertAll(CloneType))); } public virtual MemberDecl CloneMember(MemberDecl member, bool isReference) { @@ -517,7 +518,7 @@ public virtual Field CloneField(Field f) { public virtual Function CloneFunction(Function f, string newName = null) { var tps = f.TypeArgs.ConvertAll(CloneTypeParam); - var formals = f.Formals.ConvertAll(p => CloneFormal(p, false)); + var formals = f.Ins.ConvertAll(p => CloneFormal(p, false)); var result = f.Result != null ? CloneFormal(f.Result, false) : null; var req = f.Req.ConvertAll(CloneAttributedExpr); var reads = CloneSpecFrameExpr(f.Reads); diff --git a/Source/DafnyCore/AST/CompilationData.cs b/Source/DafnyCore/AST/CompilationData.cs index 45f9c30a283..d6a4508b230 100644 --- a/Source/DafnyCore/AST/CompilationData.cs +++ b/Source/DafnyCore/AST/CompilationData.cs @@ -1,11 +1,10 @@ using System; using System.Collections.Generic; +using DafnyCore.Options; namespace Microsoft.Dafny; public class CompilationData { - public readonly FreshIdGenerator IdGenerator = new(); - public CompilationData(ErrorReporter errorReporter, List includes, IList rootSourceUris, ISet alreadyVerifiedRoots, ISet alreadyCompiledRoots) { Includes = includes; ErrorReporter = errorReporter; @@ -28,4 +27,6 @@ public CompilationData(ErrorReporter errorReporter, List includes, ILis // TODO move to DocumentAfterParsing once that's used by the CLI [FilledInDuringResolution] public ISet UrisToCompile; + + public TranslationRecord AlreadyTranslatedRecord { get; set; } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Expressions/Applications/FunctionCallExpr.cs b/Source/DafnyCore/AST/Expressions/Applications/FunctionCallExpr.cs index aadb24fcdcc..b2fd5b53536 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/FunctionCallExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/FunctionCallExpr.cs @@ -4,7 +4,7 @@ namespace Microsoft.Dafny; -public class FunctionCallExpr : Expression, IHasUsages, ICloneable { +public class FunctionCallExpr : Expression, IHasReferences, ICloneable { public string Name; public readonly Expression Receiver; public readonly IToken OpenParen; // can be null if Args.Count == 0 @@ -144,9 +144,9 @@ public override IEnumerable SubExpressions { } public override IEnumerable ComponentTypes => Util.Concat(TypeApplication_AtEnclosingClass, TypeApplication_JustFunction); - public IEnumerable GetResolvedDeclarations() { + public IEnumerable GetReferences() { return Enumerable.Repeat(Function, 1); } - public IToken NameToken => tok; + public IToken NavigationToken => tok; } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs b/Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs index b8b27eb640b..0d5466b02fd 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs @@ -4,7 +4,7 @@ namespace Microsoft.Dafny; -public class MemberSelectExpr : Expression, IHasUsages, ICloneable { +public class MemberSelectExpr : Expression, IHasReferences, ICloneable { public readonly Expression Obj; public string MemberName; [FilledInDuringResolution] public MemberDecl Member; // will be a Field or Function @@ -15,25 +15,25 @@ public class MemberSelectExpr : Expression, IHasUsages, ICloneable - [FilledInDuringResolution] public List PreTypeApplication_AtEnclosingClass; + [FilledInDuringResolution] public List PreTypeApplicationAtEnclosingClass; /// /// PreTypeApplication_JustMember is the list of type arguments used to instantiate the type parameters /// of Member. /// - [FilledInDuringResolution] public List PreTypeApplication_JustMember; + [FilledInDuringResolution] public List PreTypeApplicationJustMember; /// /// TypeApplication_AtEnclosingClass is the list of type arguments used to instantiate the type that /// declares Member (which is some supertype of the receiver type). /// - [FilledInDuringResolution] public List TypeApplication_AtEnclosingClass; + [FilledInDuringResolution] public List TypeApplicationAtEnclosingClass; /// /// TypeApplication_JustMember is the list of type arguments used to instantiate the type parameters /// of Member. /// - [FilledInDuringResolution] public List TypeApplication_JustMember; + [FilledInDuringResolution] public List TypeApplicationJustMember; /// /// Returns a mapping from formal type parameters to actual type arguments. For example, given @@ -54,21 +54,21 @@ public Dictionary TypeArgumentSubstitutionsAtMemberDeclarat // Add the mappings from the member's own type parameters if (Member is ICallable icallable) { - Contract.Assert(TypeApplication_JustMember.Count == icallable.TypeArgs.Count); + Contract.Assert(TypeApplicationJustMember.Count == icallable.TypeArgs.Count); for (var i = 0; i < icallable.TypeArgs.Count; i++) { - subst.Add(icallable.TypeArgs[i], TypeApplication_JustMember[i]); + subst.Add(icallable.TypeArgs[i], TypeApplicationJustMember[i]); } } else { - Contract.Assert(TypeApplication_JustMember.Count == 0); + Contract.Assert(TypeApplicationJustMember.Count == 0); } // Add the mappings from the enclosing class. TopLevelDecl cl = Member.EnclosingClass; // Expand the type down to its non-null type, if any if (cl != null) { - Contract.Assert(cl.TypeArgs.Count == TypeApplication_AtEnclosingClass.Count); + Contract.Assert(cl.TypeArgs.Count == TypeApplicationAtEnclosingClass.Count); for (var i = 0; i < cl.TypeArgs.Count; i++) { - subst.Add(cl.TypeArgs[i], TypeApplication_AtEnclosingClass[i]); + subst.Add(cl.TypeArgs[i], TypeApplicationAtEnclosingClass[i]); } } @@ -94,21 +94,21 @@ public Dictionary PreTypeArgumentSubstitutionsAtMemberDe // Add the mappings from the member's own type parameters if (Member is ICallable icallable) { - Contract.Assert(PreTypeApplication_JustMember.Count == icallable.TypeArgs.Count); + Contract.Assert(PreTypeApplicationJustMember.Count == icallable.TypeArgs.Count); for (var i = 0; i < icallable.TypeArgs.Count; i++) { - subst.Add(icallable.TypeArgs[i], PreTypeApplication_JustMember[i]); + subst.Add(icallable.TypeArgs[i], PreTypeApplicationJustMember[i]); } } else { - Contract.Assert(PreTypeApplication_JustMember.Count == 0); + Contract.Assert(PreTypeApplicationJustMember.Count == 0); } // Add the mappings from the enclosing class. TopLevelDecl cl = Member.EnclosingClass; // Expand the type down to its non-null type, if any if (cl != null) { - Contract.Assert(cl.TypeArgs.Count == PreTypeApplication_AtEnclosingClass.Count); + Contract.Assert(cl.TypeArgs.Count == PreTypeApplicationAtEnclosingClass.Count); for (var i = 0; i < cl.TypeArgs.Count; i++) { - subst.Add(cl.TypeArgs[i], PreTypeApplication_AtEnclosingClass[i]); + subst.Add(cl.TypeArgs[i], PreTypeApplicationAtEnclosingClass[i]); } } @@ -134,7 +134,7 @@ public Dictionary TypeArgumentSubstitutionsWithParents() { Contract.Requires(WasResolved()); Contract.Ensures(Contract.Result>() != null); - return TypeArgumentSubstitutionsWithParentsAux(Obj.Type, Member, TypeApplication_JustMember); + return TypeArgumentSubstitutionsWithParentsAux(Obj.Type, Member, TypeApplicationJustMember); } public static Dictionary TypeArgumentSubstitutionsWithParentsAux(Type receiverType, MemberDecl member, List typeApplicationMember) { @@ -193,8 +193,8 @@ public static Dictionary TypeArgumentSubstitutionsWithParen void ObjectInvariant() { Contract.Invariant(Obj != null); Contract.Invariant(MemberName != null); - Contract.Invariant((Member != null) == (TypeApplication_AtEnclosingClass != null)); // TypeApplication_* are set whenever Member is set - Contract.Invariant((Member != null) == (TypeApplication_JustMember != null)); // TypeApplication_* are set whenever Member is set + Contract.Invariant((Member != null) == (TypeApplicationAtEnclosingClass != null)); // TypeApplication_* are set whenever Member is set + Contract.Invariant((Member != null) == (TypeApplicationJustMember != null)); // TypeApplication_* are set whenever Member is set } public MemberSelectExpr Clone(Cloner cloner) { @@ -209,8 +209,8 @@ public MemberSelectExpr(Cloner cloner, MemberSelectExpr original) : base(cloner, Member = cloner.CloneMember(original.Member, true); AtLabel = original.AtLabel; InCompiledContext = original.InCompiledContext; - TypeApplication_AtEnclosingClass = original.TypeApplication_AtEnclosingClass; - TypeApplication_JustMember = original.TypeApplication_JustMember; + TypeApplicationAtEnclosingClass = original.TypeApplicationAtEnclosingClass; + TypeApplicationJustMember = original.TypeApplicationJustMember; } } @@ -236,17 +236,16 @@ public MemberSelectExpr(IToken tok, Expression obj, Field field) this.Member = field; // resolve here var receiverType = obj.Type.NormalizeExpand(); - this.TypeApplication_AtEnclosingClass = receiverType.TypeArgs; - this.TypeApplication_JustMember = new List(); - this.ResolvedOutparameterTypes = new List(); + this.TypeApplicationAtEnclosingClass = receiverType.TypeArgs; + this.TypeApplicationJustMember = new List(); var typeMap = new Dictionary(); if (receiverType is UserDefinedType udt) { var cl = udt.ResolvedClass as TopLevelDeclWithMembers; Contract.Assert(cl != null); - Contract.Assert(cl.TypeArgs.Count == TypeApplication_AtEnclosingClass.Count); + Contract.Assert(cl.TypeArgs.Count == TypeApplicationAtEnclosingClass.Count); for (var i = 0; i < cl.TypeArgs.Count; i++) { - typeMap.Add(cl.TypeArgs[i], TypeApplication_AtEnclosingClass[i]); + typeMap.Add(cl.TypeArgs[i], TypeApplicationAtEnclosingClass[i]); } foreach (var entry in cl.ParentFormalTypeParametersToActuals) { var v = entry.Value.Subst(typeMap); @@ -255,9 +254,9 @@ public MemberSelectExpr(IToken tok, Expression obj, Field field) } else if (field.EnclosingClass == null) { // leave typeMap as the empty substitution } else { - Contract.Assert(field.EnclosingClass.TypeArgs.Count == TypeApplication_AtEnclosingClass.Count); + Contract.Assert(field.EnclosingClass.TypeArgs.Count == TypeApplicationAtEnclosingClass.Count); for (var i = 0; i < field.EnclosingClass.TypeArgs.Count; i++) { - typeMap.Add(field.EnclosingClass.TypeArgs[i], TypeApplication_AtEnclosingClass[i]); + typeMap.Add(field.EnclosingClass.TypeArgs[i], TypeApplicationAtEnclosingClass[i]); } } this.Type = field.Type.Subst(typeMap); // resolve here @@ -290,13 +289,13 @@ public override IEnumerable SubExpressions { get { yield return Obj; } } - public override IEnumerable ComponentTypes => Util.Concat(TypeApplication_AtEnclosingClass, TypeApplication_JustMember); + public override IEnumerable ComponentTypes => Util.Concat(TypeApplicationAtEnclosingClass, TypeApplicationJustMember); [FilledInDuringResolution] public List ResolvedOutparameterTypes; - public IEnumerable GetResolvedDeclarations() { + public IEnumerable GetReferences() { return new[] { Member }; } - public IToken NameToken => tok; -} \ No newline at end of file + public IToken NavigationToken => tok; +} diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs index 603ec190c30..8ed0207b4b5 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs @@ -1,6 +1,7 @@ using System; using System.Collections.Generic; using System.Diagnostics.Contracts; +using System.IO; using System.Linq; namespace Microsoft.Dafny; @@ -35,4 +36,10 @@ public void Resolve(ModuleResolver resolver, resolver.ConstrainSubtypeRelation(resultType, Body.Type, Body.tok, "type of case bodies do not agree (found {0}, previous types {1})", Body.Type, resultType); } } + + public override string ToString() { + var writer = new StringWriter(); + new Printer(writer, DafnyOptions.Default).PrintNestedMatchCase(false, false, this, false, false); + return writer.ToString(); + } } diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs index f362acdd8dd..d5e5e2e4c23 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs @@ -8,12 +8,16 @@ namespace Microsoft.Dafny; interface INestedMatch : INode { Expression Source { get; } string MatchTypeName { get; } + IReadOnlyList Cases { get; } } public class NestedMatchExpr : Expression, ICloneable, ICanFormat, INestedMatch { public Expression Source { get; } public string MatchTypeName => "expression"; - public readonly List Cases; + public List Cases { get; } + + IReadOnlyList INestedMatch.Cases => Cases; + public readonly bool UsesOptionalBraces; public Attributes Attributes; diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs index ecd4c7f0e33..68a6cf14c09 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs @@ -8,7 +8,10 @@ namespace Microsoft.Dafny; public class NestedMatchStmt : Statement, ICloneable, ICanFormat, INestedMatch, ICanResolve { public Expression Source { get; } public string MatchTypeName => "statement"; - public readonly List Cases; + public List Cases { get; } + + IReadOnlyList INestedMatch.Cases => Cases; + public readonly bool UsesOptionalBraces; [FilledInDuringResolution] public Statement Flattened { get; set; } diff --git a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/ExtendedPattern.cs b/Source/DafnyCore/AST/Expressions/Conditional/Patterns/ExtendedPattern.cs index e745cb7fc71..553d85e5100 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/ExtendedPattern.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/Patterns/ExtendedPattern.cs @@ -97,14 +97,13 @@ public void CheckLinearExtendedPattern(Type type, ResolutionContext resolutionCo Contract.Assert(tupleTypeDecl.Ctors[0] == tupleTypeDecl.GroundingCtor); idpat.Ctor = tupleTypeDecl.GroundingCtor; - //We expect the number of arguments in the type of the matchee and the provided pattern to match, except if the pattern is a bound variable - if (udt.TypeArgs.Count != idpat.Arguments.Count) { + if (idpat.Id != tupleTypeDecl.GroundingCtor.Name) { if (idpat.Id.StartsWith(SystemModuleManager.TupleTypeCtorNamePrefix)) { resolver.reporter.Error(MessageSource.Resolver, this.Tok, $"the case pattern is a {idpat.Arguments.Count}-element tuple, while the match expression is a {udt.TypeArgs.Count}-element tuple"); } else { - resolver.reporter.Error(MessageSource.Resolver, this.Tok, - $"case pattern {idpat.Id} has {idpat.Arguments.Count} arguments whereas the match expression has {udt.TypeArgs.Count}"); + resolver.Reporter.Error(MessageSource.Resolver, idpat.Tok, + $"found constructor {idpat.Id} but expected a {tupleTypeDecl.Dims}-tuple"); } } diff --git a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs b/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs index 4d444832148..fd31b87de28 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs @@ -1,29 +1,30 @@ using System; using System.Collections.Generic; -using System.Diagnostics; using System.Diagnostics.Contracts; using System.Linq; -using System.Security.AccessControl; -using Microsoft.CodeAnalysis.CSharp.Syntax; namespace Microsoft.Dafny; -public class IdPattern : ExtendedPattern, IHasUsages { +public class IdPattern : ExtendedPattern, IHasReferences { public bool HasParenthesis { get; } public String Id; public PreType PreType; public Type Type; // This is the syntactic type, ExtendedPatterns disappear during resolution. - public IVariable BoundVar { get; set; } + + public IVariable BoundVar { get; set; } // Only set if there are no arguments + public List Arguments; // null if just an identifier; possibly empty argument list if a constructor call public LiteralExpr ResolvedLit; // null if just an identifier [FilledInDuringResolution] public DatatypeCtor Ctor; public bool IsWildcardPattern => - Arguments == null && Id.StartsWith("_"); + Arguments == null && Id.StartsWith(WildcardString); public bool IsWildcardExact => - Arguments == null && Id == "_"; + Arguments == null && Id == WildcardString; + + public const string WildcardString = "_"; public void MakeAConstructor() { this.Arguments = new List(); @@ -129,11 +130,11 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti } } - public IEnumerable GetResolvedDeclarations() { - return new IDeclarationOrUsage[] { Ctor }.Where(x => x != null); + public IEnumerable GetReferences() { + return new ISymbol[] { Ctor }.Where(x => x != null); } - public IToken NameToken => Tok; + public IToken NavigationToken => Tok; public void CheckLinearVarPattern(Type type, ResolutionContext resolutionContext, ModuleResolver resolver) { if (Arguments != null) { diff --git a/Source/DafnyCore/AST/Expressions/Conditional/TernaryExpr.cs b/Source/DafnyCore/AST/Expressions/Conditional/TernaryExpr.cs index 4483e88214d..e91962963ac 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/TernaryExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/TernaryExpr.cs @@ -8,8 +8,7 @@ public class TernaryExpr : Expression, ICloneable { public readonly Expression E0; public readonly Expression E1; public readonly Expression E2; - public enum Opcode { /*SOON: IfOp,*/ PrefixEqOp, PrefixNeqOp } - public static readonly bool PrefixEqUsesNat = false; // "k" is either a "nat" or an "ORDINAL" + public enum Opcode { PrefixEqOp, PrefixNeqOp } public TernaryExpr(Cloner cloner, TernaryExpr original) : base(cloner, original) { Op = original.Op; diff --git a/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeUpdateExpr.cs b/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeUpdateExpr.cs index 658cc08d330..865eb478cd1 100644 --- a/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeUpdateExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeUpdateExpr.cs @@ -5,7 +5,7 @@ namespace Microsoft.Dafny; -public class DatatypeUpdateExpr : ConcreteSyntaxExpression, IHasUsages, ICloneable { +public class DatatypeUpdateExpr : ConcreteSyntaxExpression, IHasReferences, ICloneable { public readonly Expression Root; public readonly List> Updates; [FilledInDuringResolution] public List Members; @@ -62,11 +62,11 @@ public override IEnumerable SubExpressions { } } - public IEnumerable GetResolvedDeclarations() { - return (IEnumerable)LegalSourceConstructors ?? Array.Empty(); + public IEnumerable GetReferences() { + return (IEnumerable)LegalSourceConstructors ?? Array.Empty(); } - public IToken NameToken => tok; + public IToken NavigationToken => tok; public override IEnumerable PreResolveSubExpressions { get { diff --git a/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs b/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs index 9cd5476536b..ef817d6efc3 100644 --- a/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs +++ b/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs @@ -4,7 +4,7 @@ namespace Microsoft.Dafny; -public class DatatypeValue : Expression, IHasUsages, ICloneable, ICanFormat { +public class DatatypeValue : Expression, IHasReferences, ICloneable, ICanFormat { public readonly string DatatypeName; public readonly string MemberName; public readonly ActualBindings Bindings; @@ -64,11 +64,11 @@ public DatatypeValue(IToken tok, string datatypeName, string memberName, List SubExpressions => Arguments ?? Enumerable.Empty(); - public IEnumerable GetResolvedDeclarations() { + public IEnumerable GetReferences() { return Enumerable.Repeat(Ctor, 1); } - public IToken NameToken => tok; + public IToken NavigationToken => tok; public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { formatter.SetMethodLikeIndent(StartToken, OwnedTokens, indentBefore); return true; diff --git a/Source/DafnyCore/AST/Expressions/Expression.cs b/Source/DafnyCore/AST/Expressions/Expression.cs index 0be7447988e..7b4f54224e3 100644 --- a/Source/DafnyCore/AST/Expressions/Expression.cs +++ b/Source/DafnyCore/AST/Expressions/Expression.cs @@ -1,6 +1,7 @@ using System; using System.Collections.Generic; using System.Diagnostics.Contracts; +using System.Linq; using System.Numerics; namespace Microsoft.Dafny; @@ -49,7 +50,7 @@ public virtual IEnumerable TerminalExpressions { public Type Type { get { Contract.Ensures(type != null || Contract.Result() == null); // useful in conjunction with postcondition of constructor - return type == null ? null : type.Normalize(); + return type?.Normalize(); } set { Contract.Requires(!WasResolved()); // set it only once @@ -106,6 +107,7 @@ protected Expression(Cloner cloner, Expression original) { if (cloner.CloneResolvedFields && original.Type != null) { Type = original.Type; + PreType = original.PreType; } } @@ -126,6 +128,23 @@ public virtual IEnumerable SubExpressions { get { yield break; } } + public IEnumerable DescendantsAndSelf { + get { + Stack todo = new(); + List result = new(); + todo.Push(this); + while (todo.Any()) { + var current = todo.Pop(); + result.Add(current); + foreach (var child in current.SubExpressions) { + todo.Push(child); + } + } + + return result; + } + } + /// /// Returns the list of types that appear in this expression proper (that is, not including types that /// may appear in subexpressions). Types occurring in substatements of the expression are not included. @@ -135,9 +154,7 @@ public virtual IEnumerable ComponentTypes { get { yield break; } } - public virtual bool IsImplicit { - get { return false; } - } + public virtual bool IsImplicit => false; public static IEnumerable Conjuncts(Expression expr) { Contract.Requires(expr != null); @@ -723,7 +740,7 @@ public static Expression CreateITE(Expression test, Expression e0, Expression e1 /// public static Expression CreateResolvedCall(IToken tok, Expression receiver, Function function, List arguments, List typeArguments, SystemModuleManager systemModuleManager) { - Contract.Requires(function.Formals.Count == arguments.Count); + Contract.Requires(function.Ins.Count == arguments.Count); Contract.Requires(function.TypeArgs.Count == typeArguments.Count); var call = new FunctionCallExpr(tok, function.Name, receiver, tok, tok, arguments) { @@ -768,7 +785,7 @@ public static Expression CreateFieldSelect(IToken tok, Expression receiver, Fiel /// Wrap the resolved MemberSelectExpr in the usual unresolved structure, in case the expression is cloned and re-resolved. /// public static Expression WrapResolvedMemberSelect(MemberSelectExpr memberSelectExpr) { - List optTypeArguments = memberSelectExpr.TypeApplication_JustMember.Count == 0 ? null : memberSelectExpr.TypeApplication_JustMember; + List optTypeArguments = memberSelectExpr.TypeApplicationJustMember.Count == 0 ? null : memberSelectExpr.TypeApplicationJustMember; return new ExprDotName(memberSelectExpr.tok, memberSelectExpr.Obj, memberSelectExpr.MemberName, optTypeArguments) { ResolvedExpression = memberSelectExpr, Type = memberSelectExpr.Type @@ -907,4 +924,10 @@ public string AsStringLiteral() { public override IEnumerable Children => SubExpressions; public override IEnumerable PreResolveChildren => Children; + + public static Expression CreateAssigned(IToken tok, IdentifierExpr inner) { + return new UnaryOpExpr(tok, UnaryOpExpr.Opcode.Assigned, inner) { + Type = Type.Bool + }; + } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Expressions/Heap/FrameExpression.cs b/Source/DafnyCore/AST/Expressions/Heap/FrameExpression.cs index fa767652ceb..d946addaa92 100644 --- a/Source/DafnyCore/AST/Expressions/Heap/FrameExpression.cs +++ b/Source/DafnyCore/AST/Expressions/Heap/FrameExpression.cs @@ -4,7 +4,7 @@ namespace Microsoft.Dafny; -public class FrameExpression : TokenNode, IHasUsages { +public class FrameExpression : TokenNode, IHasReferences { public readonly Expression OriginalExpression; // may be a WildcardExpr [FilledInDuringResolution] public Expression DesugaredExpression; // may be null for modifies clauses, even after resolution @@ -48,10 +48,10 @@ public FrameExpression(Cloner cloner, FrameExpression original) { } } - public IToken NameToken => tok; + public IToken NavigationToken => tok; public override IEnumerable Children => new[] { E }; public override IEnumerable PreResolveChildren => Children; - public IEnumerable GetResolvedDeclarations() { + public IEnumerable GetReferences() { return new[] { Field }.Where(x => x != null); } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Expressions/Operators/BinaryExpr.cs b/Source/DafnyCore/AST/Expressions/Operators/BinaryExpr.cs index b81c90e4840..74da619191e 100644 --- a/Source/DafnyCore/AST/Expressions/Operators/BinaryExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Operators/BinaryExpr.cs @@ -114,14 +114,14 @@ public enum ResolvedOpcode { } private ResolvedOpcode _theResolvedOp = ResolvedOpcode.YetUndetermined; public ResolvedOpcode ResolvedOp { - set { - Contract.Assume(_theResolvedOp == ResolvedOpcode.YetUndetermined || _theResolvedOp == value); // there's never a reason for resolution to change its mind, is there? - _theResolvedOp = value; - } get { Debug.Assert(_theResolvedOp != ResolvedOpcode.YetUndetermined); // shouldn't read it until it has been properly initialized return _theResolvedOp; } + set { + Contract.Assume(_theResolvedOp == ResolvedOpcode.YetUndetermined || _theResolvedOp == value); // there's never a reason for resolution to change its mind, is there? + _theResolvedOp = value; + } } public ResolvedOpcode ResolvedOp_PossiblyStillUndetermined { // offer a way to return _theResolveOp -- for experts only! get { return _theResolvedOp; } diff --git a/Source/DafnyCore/AST/Expressions/Operators/DecreasesToExpr.cs b/Source/DafnyCore/AST/Expressions/Operators/DecreasesToExpr.cs new file mode 100644 index 00000000000..7d8ee2abb01 --- /dev/null +++ b/Source/DafnyCore/AST/Expressions/Operators/DecreasesToExpr.cs @@ -0,0 +1,32 @@ +using System; +using System.Collections.Generic; +using System.Linq; + +namespace Microsoft.Dafny; + +public class DecreasesToExpr : Expression, ICloneable { + public IReadOnlyList OldExpressions { get; } + public IReadOnlyList NewExpressions { get; } + + public bool AllowNoChange { get; } + + public DecreasesToExpr(IToken tok, + IReadOnlyList oldExpressions, + IReadOnlyList newExpressions, bool allowNoChange) : base(tok) { + OldExpressions = oldExpressions; + NewExpressions = newExpressions; + AllowNoChange = allowNoChange; + } + + public DecreasesToExpr(Cloner cloner, DecreasesToExpr original) : base(cloner, original) { + OldExpressions = original.OldExpressions.Select(cloner.CloneExpr).ToList(); + NewExpressions = original.NewExpressions.Select(cloner.CloneExpr).ToList(); + AllowNoChange = original.AllowNoChange; + } + + public DecreasesToExpr Clone(Cloner cloner) { + return new DecreasesToExpr(cloner, this); + } + + public override IEnumerable SubExpressions => OldExpressions.Concat(NewExpressions); +} diff --git a/Source/DafnyCore/AST/Expressions/Operators/UnaryOpExpr.cs b/Source/DafnyCore/AST/Expressions/Operators/UnaryOpExpr.cs index 44c3ed134ec..bf1f6d82a85 100644 --- a/Source/DafnyCore/AST/Expressions/Operators/UnaryOpExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Operators/UnaryOpExpr.cs @@ -9,6 +9,7 @@ public enum Opcode { Fresh, // fresh also has a(n optional) second argument, namely the @-label Allocated, Lit, // there is no syntax for this operator, but it is sometimes introduced during translation + Assigned, } public readonly Opcode Op; @@ -22,7 +23,8 @@ public enum ResolvedOpcode { MapCard, Fresh, Allocated, - Lit + Lit, + Assigned, } private ResolvedOpcode _ResolvedOp = ResolvedOpcode.YetUndetermined; @@ -42,6 +44,7 @@ public ResolvedOpcode ResolveOp() { (Opcode.Fresh, _) => ResolvedOpcode.Fresh, (Opcode.Allocated, _) => ResolvedOpcode.Allocated, (Opcode.Lit, _) => ResolvedOpcode.Lit, + (Opcode.Assigned, _) => ResolvedOpcode.Assigned, _ => ResolvedOpcode.YetUndetermined // Unreachable }; Contract.Assert(_ResolvedOp != ResolvedOpcode.YetUndetermined); diff --git a/Source/DafnyCore/AST/Expressions/StmtExpr.cs b/Source/DafnyCore/AST/Expressions/StmtExpr.cs index 8af66ea9d28..ea509b3c1a3 100644 --- a/Source/DafnyCore/AST/Expressions/StmtExpr.cs +++ b/Source/DafnyCore/AST/Expressions/StmtExpr.cs @@ -61,7 +61,7 @@ public Expression GetSConclusion() { } else if (S is CalcStmt) { var s = (CalcStmt)S; return s.Result; - } else if (S is RevealStmt) { + } 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 UpdateStmt) { return CreateBoolLiteral(tok, true); // one could use the postcondition of the method, suitably instantiated, but "true" is conservative and much simpler :) diff --git a/Source/DafnyCore/AST/Expressions/Variables/Formal.cs b/Source/DafnyCore/AST/Expressions/Variables/Formal.cs index cdbff00e752..c3fc0844884 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/Formal.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/Formal.cs @@ -35,11 +35,11 @@ public Formal(IToken tok, string name, Type type, bool inParam, bool isGhost, Ex public bool HasName => !Name.StartsWith("#"); - private string sanitizedName; - public override string SanitizedName => - sanitizedName ??= SanitizeName(Name); // No unique-ification - public override string CompileName => - compileName ??= SanitizeName(NameForCompilation); + public override string GetOrCreateCompileName(CodeGenIdGenerator generator) { + return CompileName; + } + + public string CompileName => compileName ??= SanitizeName(NameForCompilation); public override IEnumerable Children => (DefaultValue != null ? new List { DefaultValue } : Enumerable.Empty()).Concat(base.Children); diff --git a/Source/DafnyCore/AST/Expressions/Variables/IVariable.cs b/Source/DafnyCore/AST/Expressions/Variables/IVariable.cs index 36f35a0ed1f..c8f174a0788 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/IVariable.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/IVariable.cs @@ -19,14 +19,14 @@ string UniqueName { bool HasBeenAssignedUniqueName { // unique names are not assigned until the Translator; if you don't already know if that stage has run, this boolean method will tell you get; } - static FreshIdGenerator CompileNameIdGenerator = new FreshIdGenerator(); - string AssignUniqueName(FreshIdGenerator generator); - string SanitizedName { - get; - } - string CompileName { - get; - } + string AssignUniqueName(VerificationIdGenerator generator); + + /// + /// A name suitable for compilation, but without the unique identifier. + /// Useful to generate readable identifiers in the generated source code. + /// + string CompileNameShadowable { get; } + string GetOrCreateCompileName(CodeGenIdGenerator generator); PreType PreType { get; diff --git a/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs b/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs index 0fe8374904f..9880d147130 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs @@ -35,18 +35,21 @@ public bool HasBeenAssignedUniqueName { throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here } } - public string SanitizedName { - get { - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here - } + public string SanitizedName(CodeGenIdGenerator generator) { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here } - public string CompileName { + + public string CompileNameShadowable { get { Contract.Ensures(Contract.Result() != null); throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here } } + public string GetOrCreateCompileName(CodeGenIdGenerator generator) { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here + } public Type Type { get { Contract.Ensures(Contract.Result() != null); @@ -81,13 +84,13 @@ public bool IsGhost { public void MakeGhost() { throw new NotImplementedException(); } - public string AssignUniqueName(FreshIdGenerator generator) { + public string AssignUniqueName(VerificationIdGenerator generator) { Contract.Ensures(Contract.Result() != null); throw new NotImplementedException(); } - public abstract IToken NameToken { get; } - public SymbolKind Kind => throw new NotImplementedException(); + public abstract IToken NavigationToken { get; } + public SymbolKind? Kind => throw new NotImplementedException(); public string GetDescription(DafnyOptions options) { throw new NotImplementedException(); } diff --git a/Source/DafnyCore/AST/Expressions/Variables/IdentifierExpr.cs b/Source/DafnyCore/AST/Expressions/Variables/IdentifierExpr.cs index 1693a8e3a17..c1c3777b450 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/IdentifierExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/IdentifierExpr.cs @@ -4,7 +4,7 @@ namespace Microsoft.Dafny; -public class IdentifierExpr : Expression, IHasUsages, ICloneable { +public class IdentifierExpr : Expression, IHasReferences, ICloneable { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Name != null); @@ -52,11 +52,11 @@ public static bool Is(Expression expr, IVariable variable) { return expr.Resolved is IdentifierExpr identifierExpr && identifierExpr.Var == variable; } - public IEnumerable GetResolvedDeclarations() { + public IEnumerable GetReferences() { return Enumerable.Repeat(Var, 1); } - public IToken NameToken => tok; + public IToken NavigationToken => tok; public override IEnumerable Children { get; } = Enumerable.Empty(); } diff --git a/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs b/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs index f81d643d644..26ad772c020 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs @@ -8,6 +8,17 @@ namespace Microsoft.Dafny; public abstract class NonglobalVariable : TokenNode, IVariable { readonly string name; + protected NonglobalVariable(IToken tok, string name, Type type, bool isGhost) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(type != null); + this.tok = tok; + this.name = name; + IsTypeExplicit = type != null; + this.type = type ?? new InferredTypeProxy(); + this.isGhost = isGhost; + } + [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(name != null); @@ -27,7 +38,7 @@ public string Name { private string uniqueName; public string UniqueName => uniqueName; public bool HasBeenAssignedUniqueName => uniqueName != null; - public string AssignUniqueName(FreshIdGenerator generator) { + public string AssignUniqueName(VerificationIdGenerator generator) { return uniqueName ??= generator.FreshId(Name + "#"); } @@ -74,16 +85,19 @@ public static string SanitizeName(string nm) { } } - private string sanitizedName; - public virtual string SanitizedName => - sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizeName(Name)}"; + private string sanitizedNameShadowable; + + public virtual string CompileNameShadowable => + sanitizedNameShadowable ??= SanitizeName(Name); protected string compileName; - public virtual string CompileName => - compileName ??= SanitizedName; + + public virtual string GetOrCreateCompileName(CodeGenIdGenerator generator) { + return compileName ??= $"_{generator.FreshNumericId()}_{CompileNameShadowable}"; + } Type type; - public bool IsTypeExplicit = false; + public bool IsTypeExplicit { get; set; } public Type SyntacticType { get { return type; } } // returns the non-normalized type public PreType PreType { get; set; } @@ -122,20 +136,10 @@ public void MakeGhost() { IsGhost = true; } - public NonglobalVariable(IToken tok, string name, Type type, bool isGhost) { - Contract.Requires(tok != null); - Contract.Requires(name != null); - Contract.Requires(type != null); - this.tok = tok; - this.name = name; - this.type = type; - this.isGhost = isGhost; - } - - public IToken NameToken => tok; + public IToken NavigationToken => tok; public override IEnumerable Children => IsTypeExplicit ? new List { Type } : Enumerable.Empty(); public override IEnumerable PreResolveChildren => IsTypeExplicit ? new List() { Type } : Enumerable.Empty(); - public SymbolKind Kind => SymbolKind.Variable; + public SymbolKind? Kind => SymbolKind.Variable; public string GetDescription(DafnyOptions options) { return this.AsText(); } diff --git a/Source/DafnyCore/AST/Expressions/Variables/Resolver_IdentifierExpr.cs b/Source/DafnyCore/AST/Expressions/Variables/Resolver_IdentifierExpr.cs index e781b702630..79365f377f2 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/Resolver_IdentifierExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/Resolver_IdentifierExpr.cs @@ -8,7 +8,7 @@ namespace Microsoft.Dafny; /// /// This class is used only inside the resolver itself. It gets hung in the AST in uncompleted name segments. /// -class Resolver_IdentifierExpr : Expression, IHasUsages, ICloneable { +class Resolver_IdentifierExpr : Expression, IHasReferences, ICloneable { public readonly TopLevelDecl Decl; public readonly List TypeArgs; [ContractInvariantMethod] @@ -75,11 +75,11 @@ public Resolver_IdentifierExpr(IToken tok, TypeParameter tp) Contract.Requires(tp != null); } - public IEnumerable GetResolvedDeclarations() { + public IEnumerable GetReferences() { return new[] { Decl }; } - public IToken NameToken => tok; + public IToken NavigationToken => tok; public Resolver_IdentifierExpr Clone(Cloner cloner) { return new Resolver_IdentifierExpr(cloner, this); } diff --git a/Source/DafnyCore/AST/Formatting.dfy b/Source/DafnyCore/AST/Formatting.dfy index 0d9269e440e..bfaabd16e2a 100644 --- a/Source/DafnyCore/AST/Formatting.dfy +++ b/Source/DafnyCore/AST/Formatting.dfy @@ -36,7 +36,7 @@ module {:extern "Microsoft"} {:options "-functionSyntax:4"} Microsoft { 2) Reindentation algorithm provided by the same reindent */ method ReindentProgramFromFirstToken(firstToken: IToken, reindent: IIndentationFormatter) returns (s: CsString) requires firstToken.Valid() - ensures forall token <- firstToken.allTokens :: s.Contains(token.val) + ensures forall token: IToken <- firstToken.allTokens :: s.Contains(token.val) { var token: IToken? := firstToken; var sb := new CsStringBuilder(); @@ -49,7 +49,7 @@ module {:extern "Microsoft"} {:options "-functionSyntax:4"} Microsoft { && token.Valid() && i < |allTokens| && token == allTokens[i] - invariant forall t <- allTokens[0..i] :: sb.built.Contains(t.val) + invariant forall t: IToken <- allTokens[0..i] :: sb.built.Contains(t.val) { if(token.Next == null) { firstToken.TokenNextIsNullImpliesLastToken(token, i); @@ -65,7 +65,7 @@ module {:extern "Microsoft"} {:options "-functionSyntax:4"} Microsoft { sb.Append(token.val); sb.Append(newTrailingTrivia); ContainsTransitive(); - assert {:split_here} forall t <- allTokens[0..i+1] :: sb.built.Contains(t.val); + assert {:split_here} forall t: IToken <- allTokens[0..i+1] :: sb.built.Contains(t.val); token := token.Next; i := i + 1; } diff --git a/Source/DafnyCore/AST/Grammar/ParseErrors.cs b/Source/DafnyCore/AST/Grammar/ParseErrors.cs index 01a6d1cb11c..8e666089d15 100644 --- a/Source/DafnyCore/AST/Grammar/ParseErrors.cs +++ b/Source/DafnyCore/AST/Grammar/ParseErrors.cs @@ -139,6 +139,8 @@ public enum ErrorId { p_file_has_no_code, p_general_traits_datatype, p_general_traits_full, + p_decreases_without_to, + p_binding_in_decreases_to, } static ParseErrors() { diff --git a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs index 86c8c4c59c0..783e1716810 100644 --- a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs +++ b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs @@ -25,6 +25,8 @@ public Parser(DafnyOptions options, Scanner/*!*/ scanner, Errors/*!*/ errors, Ca theModule = new FileModuleDefinition(scanner.FirstToken); } + bool IsReveal(IToken nextToken) => la.kind == _reveal || (la.kind == _hide && nextToken.kind is _star or _ident); + bool IsIdentifier(int kind) { return kind == _ident || kind == _least || kind == _greatest || kind == _older || kind == _opaque; } @@ -156,7 +158,12 @@ bool IsWitness() { } bool IsFunctionDecl() { - switch (la.kind) { + var kind = la.kind; + return IsFunctionDecl(kind); + } + + private bool IsFunctionDecl(int kind) { + switch (kind) { case _function: case _predicate: case _copredicate: @@ -184,6 +191,9 @@ bool IsParenStar() { bool IsExpliesOp() => IsExpliesOp(la); bool IsAndOp() => IsAndOp(la); bool IsOrOp() => IsOrOp(la); + bool IsComma() { + return la.val == ","; + } static bool IsEquivOp(IToken la) { return la.val == "<==>"; } @@ -617,7 +627,6 @@ class DeclModifierData { public bool IsOpaque; public IToken OpaqueToken; public IToken FirstToken; - } private ModuleKindEnum GetModuleKind(DeclModifierData mods) { @@ -682,6 +691,39 @@ bool IsAssumeTypeKeyword(IToken la) { return la.kind == _assume || la.kind == _assert || la.kind == _expect; } + Expression ProcessTupleArgs(List args, IToken lp) { + if (args.Count == 1 && !args[0].IsGhost) { + if (args[0].FormalParameterName != null) { + SemErr(ErrorId.p_no_parenthesized_binding, lp, "binding not allowed in parenthesized expression"); + } + return args[0].Actual; + } else { + // Compute the actual position of ghost arguments + var ghostness = new bool[args.Count]; + for (var i = 0; i < args.Count; i++) { + ghostness[i] = false; + } + for (var i = 0; i < args.Count; i++) { + var arg = args[i]; + if (arg.IsGhost) { + if (arg.FormalParameterName == null) { + ghostness[i] = true; + } else { + var success = int.TryParse(arg.FormalParameterName.val, out var index); + if (success && 0 <= index && index < args.Count) { + ghostness[index] = true; + } + } + } + } + var argumentGhostness = ghostness.ToList(); + // make sure the corresponding tuple type exists + SystemModuleModifiers.Add(b => b.TupleType(lp, args.Count, true, argumentGhostness)); + return new DatatypeValue(lp, SystemModuleManager.TupleTypeName(argumentGhostness), SystemModuleManager.TupleTypeCtorName(args.Count), args); + } + } + + public void ApplyOptionsFromAttributes(Attributes attrs) { var overrides = attrs.AsEnumerable().Where(a => a.Name == "options") .Reverse().Select(a => @@ -764,4 +806,4 @@ void CheckDeclModifiers(ref DeclModifierData dmod, string declCaption, AllowedDe } } -} \ No newline at end of file +} diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs index 1bfc36a281f..a95048f8f31 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs @@ -767,6 +767,10 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, wr.Write("Lit("); PrintExpression(e.E, false); wr.Write(")"); + } else if (e.Op == UnaryOpExpr.Opcode.Assigned) { + wr.Write("assigned("); + PrintExpression(e.E, false); + wr.Write(")"); } else { Contract.Assert(e.Op != UnaryOpExpr.Opcode.Fresh); // this is handled is "is FreshExpr" case above // Prefix operator. @@ -1145,12 +1149,7 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, int i = 0; foreach (var mc in e.Cases) { bool isLastCase = i == e.Cases.Count - 1; - wr.Write(" case"); - PrintAttributes(mc.Attributes); - wr.Write(" "); - PrintExtendedPattern(mc.Pat); - wr.Write(" => "); - PrintExpression(mc.Body, isRightmost && isLastCase, !parensNeeded && isFollowedBySemicolon); + PrintNestedMatchCase(isRightmost, isFollowedBySemicolon, mc, isLastCase, parensNeeded); i++; } if (e.UsesOptionalBraces) { wr.Write(" }"); } else if (parensNeeded) { wr.Write(")"); } @@ -1198,9 +1197,41 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, wr.Write("[BoogieFunctionCall]"); // this prevents debugger watch window crash } else if (expr is Resolver_IdentifierExpr) { wr.Write("[Resolver_IdentifierExpr]"); // we can get here in the middle of a debugging session + } else if (expr is DecreasesToExpr decreasesToExpr) { + var comma = false; + foreach (var oldExpr in decreasesToExpr.OldExpressions) { + if (comma) { + wr.Write(", "); + } + PrintExpression(oldExpr, false); + comma = true; + } + if (decreasesToExpr.AllowNoChange) { + wr.Write(" nonincreases to "); + } else { + wr.Write(" decreases to "); + } + comma = false; + foreach (var newExpr in decreasesToExpr.NewExpressions) { + if (comma) { + wr.Write(", "); + } + PrintExpression(newExpr, false); + comma = true; + } } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression } } + + public void PrintNestedMatchCase(bool isRightmost, bool isFollowedBySemicolon, NestedMatchCaseExpr mc, bool isLastCase, + bool parensNeeded) { + wr.Write(" case"); + PrintAttributes(mc.Attributes); + wr.Write(" "); + PrintExtendedPattern(mc.Pat); + wr.Write(" => "); + PrintExpression(mc.Body, isRightmost && isLastCase, !parensNeeded && isFollowedBySemicolon); + } } } diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs index 151ac8a0037..ef97d0be06f 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs @@ -29,7 +29,7 @@ public partial class Printer { public void PrintStatement(Statement stmt, int indent) { Contract.Requires(stmt != null); - if (stmt.IsGhost && printMode == PrintModes.NoGhost) { return; } + if (stmt.IsGhost && printMode == PrintModes.NoGhostOrIncludes) { return; } for (LList