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_no_forks.yaml b/.github/workflows/compfuzzci_fuzz_no_forks.yaml new file mode 100644 index 00000000000..ee41745889c --- /dev/null +++ b/.github/workflows/compfuzzci_fuzz_no_forks.yaml @@ -0,0 +1,32 @@ +# This workflow is triggered on PR being opened, synced, reopened, closed. +# It dispatches workflow on CompFuzzCI repository, where fuzzing of the PR is handled. + +name: Fuzzing on PR (excluding forks) +on: + pull_request: + branches: + - master + +jobs: + FuzzOnPR: + 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: 'fuzz.yaml', + ref: 'main', + inputs: { + commit: '${{ github.event.pull_request.head.sha }}', + main_commit: '${{github.event.pull_request.base.sha}}', + branch: '${{github.event.pull_request.head.ref}}', + 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/msbuild.yml b/.github/workflows/msbuild.yml index 2b1fc10479a..a36595910f6 100644 --- a/.github/workflows/msbuild.yml +++ b/.github/workflows/msbuild.yml @@ -161,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/runtime-tests.yml b/.github/workflows/runtime-tests.yml index 08696e824b5..c3756189bd9 100644 --- a/.github/workflows/runtime-tests.yml +++ b/.github/workflows/runtime-tests.yml @@ -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/.gitignore b/.gitignore index 34f20c8c80f..beb07d34a9c 100644 --- a/.gitignore +++ b/.gitignore @@ -88,3 +88,5 @@ 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/Makefile b/Makefile index d6d9295fa64..d7e8959495e 100644 --- a/Makefile +++ b/Makefile @@ -26,6 +26,10 @@ boogie: ${DIR}/boogie/Binaries/Boogie.exe tests: (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 ) @@ -87,12 +91,20 @@ clean: 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-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 @@ -100,4 +112,7 @@ update-runtime-dafny: # - 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 format-dfy format update-runtime-dafny update-cs-module update-go-module +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/RELEASE_NOTES.md b/RELEASE_NOTES.md index a934cb41aa6..2e52b713dfc 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -2,6 +2,37 @@ 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 diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs b/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs index 8a4171f4809..8319b008012 100644 --- a/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs +++ b/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs @@ -15,15 +15,22 @@ 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_MemberSelect(RAST.Expr.create_MemberSelect(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("")), Dafny.Sequence.UnicodeFromString("dafny_runtime")), Dafny.Sequence.UnicodeFromString("truncate!")), Dafny.Sequence.FromElements(x, RAST.Expr.create_ExprFromType(t))); + 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_MemberSelect(RAST.__default.dafny__runtime, Dafny.Sequence.UnicodeFromString("int!")), Dafny.Sequence.FromElements(RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("1")))); + 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() { @@ -53,7 +60,7 @@ public static void TestOptimizeToString() 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_MemberSelect(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.UnicodeFromString("abc"))); + _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; @@ -76,14 +83,8 @@ public static void TestOptimizeToString() _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(); - RAST._IExpr _14___v9; - _14___v9 = (DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_U8(), RAST.Expr.create_Call(RAST.Expr.create_MemberSelect(_4_c, Dafny.Sequence.UnicodeFromString("int!")), Dafny.Sequence.FromElements()))).Optimize(); - RAST._IExpr _15___v10; - _15___v10 = (DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_U8(), RAST.Expr.create_Call(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(_4_c, Dafny.Sequence.UnicodeFromString("dafny_runtime")), Dafny.Sequence.UnicodeFromString("int!")), Dafny.Sequence.FromElements()))).Optimize(); - RAST._IExpr _16___v11; - _16___v11 = (DafnyToRustCompilerCoverage.RASTCoverage.__default.ConversionNum(RAST.Type.create_U8(), RAST.Expr.create_Call(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("")), Dafny.Sequence.UnicodeFromString("dafny_runtime")), Dafny.Sequence.UnicodeFromString("int!")), Dafny.Sequence.FromElements(_4_c)))).Optimize(); - Std.Wrappers._IOption> _17___v12; - _17___v12 = (_4_c).RightMostIdentifier(); + Std.Wrappers._IOption> _14___v9; + _14___v9 = (_4_c).RightMostIdentifier(); } } public static void TestPrintingInfo() @@ -106,7 +107,7 @@ public static void TestPrintingInfo() 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_MemberSelect(_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()))); @@ -143,12 +144,6 @@ public static void TestPrintingInfo() 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 TestExpr() - { - DafnyToRustCompilerCoverage.RASTCoverage.__default.TestOptimizeToString(); - DafnyToRustCompilerCoverage.RASTCoverage.__default.TestPrintingInfo(); - DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoExtraSemicolonAfter(); - } public static void AssertCoverage(bool x) { } diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs b/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs new file mode 100644 index 00000000000..02b63cfbb13 --- /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(FactorPathsOptimization.__default.apply(RAST.Mod.create_Mod(Dafny.Sequence.UnicodeFromString("onemodule"), 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(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(FactorPathsOptimization.__default.apply(RAST.Mod.create_Mod(Dafny.Sequence.UnicodeFromString("onemodule"), 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(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/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index fcceee43562..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); } diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs index 26227fae09a..ef97d0be06f 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs @@ -363,7 +363,7 @@ public void PrintStatement(Statement stmt, int indent) { wr.Write(" "); } PrintUpdateRHS(s, indent); - wr.Write(";"); + PrintBy(s); } else if (stmt is CallStmt) { // Most calls are printed from their concrete syntax given in the input. However, recursive calls to @@ -395,8 +395,7 @@ public void PrintStatement(Statement stmt, int indent) { wr.Write(" "); PrintUpdateRHS(s.Update, indent); } - wr.Write(";"); - + PrintBy(s.Update); } else if (stmt is VarDeclPattern) { var s = (VarDeclPattern)stmt; if (s.tok is AutoGeneratedToken) { @@ -455,6 +454,20 @@ public void PrintStatement(Statement stmt, int indent) { } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement } + + void PrintBy(ConcreteUpdateStatement statement) { + BlockStmt proof = statement switch { + UpdateStmt updateStmt => updateStmt.Proof, + AssignOrReturnStmt returnStmt => returnStmt.Proof, + _ => null + }; + if (proof != null) { + wr.Write(" by "); + PrintStatement(proof, indent); + } else { + wr.Write(";"); + } + } } private void PrintHideReveal(HideRevealStmt revealStmt) { diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs index dbd0e854ae4..5cd7c07e953 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs @@ -35,7 +35,7 @@ static Printer() { options.PrintMode = value; }); - DooFile.RegisterNoChecksNeeded(PrintMode, false); + OptionRegistry.RegisterOption(PrintMode, OptionScope.Cli); } public static readonly Option PrintMode = new("--print-mode", () => PrintModes.Everything, @" @@ -308,11 +308,11 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable typeArgs) { Contract.Requires(typeArgs != null); Contract.Requires( - typeArgs.All(tp => tp.Name.StartsWith("_")) || - typeArgs.All(tp => !tp.Name.StartsWith("_"))); + typeArgs.All(tp => tp.IsAutoCompleted) || + typeArgs.All(tp => !tp.IsAutoCompleted)); - if (typeArgs.Count != 0 && !typeArgs[0].Name.StartsWith("_")) { + if (typeArgs.Count != 0 && !typeArgs[0].IsAutoCompleted) { wr.Write("<{0}>", Util.Comma(typeArgs, TypeParamString)); } } + public static string TypeParameterToString(TypeParameter tp) { + return TypeParamVariance(tp) + tp.Name + TPCharacteristicsSuffix(tp.Characteristics, true); + } + public string TypeParamString(TypeParameter tp) { Contract.Requires(tp != null); - string variance; + var paramString = TypeParamVariance(tp) + tp.Name + TPCharacteristicsSuffix(tp.Characteristics); + foreach (var typeBound in tp.TypeBounds) { + paramString += $" extends {typeBound.TypeName(options, null, true)}"; + } + return paramString; + } + + public static string TypeParamVariance(TypeParameter tp) { switch (tp.VarianceSyntax) { case TypeParameter.TPVarianceSyntax.Covariant_Permissive: - variance = "*"; - break; + return "*"; case TypeParameter.TPVarianceSyntax.Covariant_Strict: - variance = "+"; - break; + return "+"; case TypeParameter.TPVarianceSyntax.NonVariant_Permissive: - variance = "!"; - break; + return "!"; case TypeParameter.TPVarianceSyntax.NonVariant_Strict: - variance = ""; - break; + return ""; case TypeParameter.TPVarianceSyntax.Contravariance: - variance = "-"; - break; + return "-"; default: Contract.Assert(false); // unexpected VarianceSyntax throw new cce.UnreachableException(); } - var paramString = variance + tp.Name + TPCharacteristicsSuffix(tp.Characteristics); - foreach (var typeBound in tp.TypeBounds) { - paramString += $" extends {typeBound.TypeName(options, null, true)}"; - } - return paramString; } private void PrintArrowType(string arrow, string internalName, List typeArgs) { @@ -1184,9 +1185,13 @@ public void PrintType(string prefix, Type ty) { } public string TPCharacteristicsSuffix(TypeParameter.TypeParameterCharacteristics characteristics) { + return TPCharacteristicsSuffix(characteristics, options.DafnyPrintResolvedFile != null); + } + + public static string TPCharacteristicsSuffix(TypeParameter.TypeParameterCharacteristics characteristics, bool printInferredTypeCharacteristics) { string s = null; if (characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.Required || - (characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.InferredRequired && options.DafnyPrintResolvedFile != null)) { + (characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.InferredRequired && printInferredTypeCharacteristics)) { s = "=="; } if (characteristics.HasCompiledValue) { diff --git a/Source/DafnyCore/AST/Members/Function.cs b/Source/DafnyCore/AST/Members/Function.cs index aff0218bdef..714be37301a 100644 --- a/Source/DafnyCore/AST/Members/Function.cs +++ b/Source/DafnyCore/AST/Members/Function.cs @@ -329,7 +329,7 @@ static Function() { DafnyOptions.RegisterLegacyBinding(FunctionSyntaxOption, (options, value) => { options.FunctionSyntax = functionSyntaxOptionsMap[value]; }); - DooFile.RegisterNoChecksNeeded(FunctionSyntaxOption, true); + OptionRegistry.RegisterOption(FunctionSyntaxOption, OptionScope.Module); } public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { diff --git a/Source/DafnyCore/AST/Members/ICodeContext.cs b/Source/DafnyCore/AST/Members/ICodeContext.cs index a5ab7e0886e..d01e78f5b6f 100644 --- a/Source/DafnyCore/AST/Members/ICodeContext.cs +++ b/Source/DafnyCore/AST/Members/ICodeContext.cs @@ -145,6 +145,8 @@ public interface RedirectingTypeDecl : ICallable { Attributes Attributes { get; } ModuleDefinition Module { get; } BoundVar/*?*/ Var { get; } + PreType BasePreType { get; } + Type BaseType { get; } Expression/*?*/ Constraint { get; } SubsetTypeDecl.WKind WitnessKind { get; } Expression/*?*/ Witness { get; } // non-null iff WitnessKind is Compiled or Ghost diff --git a/Source/DafnyCore/AST/Members/Method.cs b/Source/DafnyCore/AST/Members/Method.cs index 73a4be9c63f..37b7958ab35 100644 --- a/Source/DafnyCore/AST/Members/Method.cs +++ b/Source/DafnyCore/AST/Members/Method.cs @@ -21,7 +21,7 @@ static Method() { DafnyOptions.RegisterLegacyUi(ReadsClausesOnMethods, DafnyOptions.ParseBoolean, "Language feature selection", "readsClausesOnMethods", @" 0 (default) - Reads clauses on methods are forbidden. 1 - Reads clauses on methods are permitted (with a default of 'reads *').".TrimStart(), defaultValue: false); - DooFile.RegisterLibraryCheck(ReadsClausesOnMethods, OptionCompatibility.CheckOptionLocalImpliesLibrary); + OptionRegistry.RegisterGlobalOption(ReadsClausesOnMethods, OptionCompatibility.CheckOptionLocalImpliesLibrary); } public override IEnumerable Children => new Node[] { Body, Decreases }.Where(x => x != null). diff --git a/Source/DafnyCore/AST/Members/MethodOrFunction.cs b/Source/DafnyCore/AST/Members/MethodOrFunction.cs index eef6b372148..2b5167ed426 100644 --- a/Source/DafnyCore/AST/Members/MethodOrFunction.cs +++ b/Source/DafnyCore/AST/Members/MethodOrFunction.cs @@ -11,7 +11,7 @@ public abstract class MethodOrFunction : MemberDecl, ICodeContainer { "Allow exporting callables with preconditions, and importing callables with postconditions"); static MethodOrFunction() { - DooFile.RegisterLibraryCheck(AllowExternalContracts, OptionCompatibility.OptionLibraryImpliesLocalError); + OptionRegistry.RegisterGlobalOption(AllowExternalContracts, OptionCompatibility.OptionLibraryImpliesLocalError); } [FilledInDuringResolution] diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index f165d89b5f3..c7b1b971f80 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs @@ -1,8 +1,11 @@ using System; using System.Collections.Generic; using System.Collections.Immutable; +using System.CommandLine; using System.Diagnostics.Contracts; using System.Linq; +using DafnyCore; +using DafnyCore.Options; using Microsoft.Dafny.Auditor; using Microsoft.Dafny.Compilers; using OmniSharp.Extensions.LanguageServer.Protocol.Models; @@ -25,6 +28,18 @@ public enum ImplementationKind { public record Implements(ImplementationKind Kind, ModuleQualifiedId Target); public class ModuleDefinition : RangeNode, IAttributeBearingDeclaration, ICloneable, IHasSymbolChildren { + + public static readonly Option LegacyModuleNames = new("--legacy-module-names", + @" +Generate module names in the older A_mB_mC style instead of the current A.B.C scheme".TrimStart()) { + IsHidden = true + }; + + static ModuleDefinition() { + DafnyOptions.RegisterLegacyUi(LegacyModuleNames, DafnyOptions.ParseBoolean, "Compilation options", legacyName: "legacyModuleNames", defaultValue: false); + OptionRegistry.RegisterOption(LegacyModuleNames, OptionScope.Translation); + } + public IToken BodyStartTok = Token.NoToken; public IToken TokenWithTrailingDocString = Token.NoToken; public string DafnyName => NameNode.StartToken.val; // The (not-qualified) name as seen in Dafny source code @@ -215,11 +230,15 @@ public string GetCompileName(DafnyOptions options) { if (IsBuiltinName) { compileName = Name; } else if (EnclosingModule is { TryToAvoidName: false }) { - // Include all names in the module tree path, to disambiguate when compiling - // a flat list of modules. - // Use an "underscore-escaped" character as a module name separator, since - // underscores are already used as escape characters in SanitizeName() - compileName = EnclosingModule.GetCompileName(options) + options.Backend.ModuleSeparator + NonglobalVariable.SanitizeName(Name); + if (options.Get(LegacyModuleNames)) { + compileName = SanitizedName; + } else { + // Include all names in the module tree path, to disambiguate when compiling + // a flat list of modules. + // Use an "underscore-escaped" character as a module name separator, since + // underscores are already used as escape characters in SanitizeName() + compileName = EnclosingModule.GetCompileName(options) + options.Backend.ModuleSeparator + NonglobalVariable.SanitizeName(Name); + } } else { compileName = NonglobalVariable.SanitizeName(Name); } diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs index 0b6199ae2bb..a598f530af8 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs @@ -9,6 +9,7 @@ public class AssignOrReturnStmt : ConcreteUpdateStatement, ICloneable Rhss; public readonly AttributedToken KeywordToken; + public readonly BlockStmt Proof; [FilledInDuringResolution] public readonly List ResolvedStatements = new List(); public override IEnumerable SubStatements => ResolvedStatements; public override IToken Tok { @@ -22,7 +23,7 @@ public override IToken Tok { } } - public override IEnumerable Children => ResolvedStatements; + public override IEnumerable Children => ResolvedStatements.Concat(Proof?.Children ?? new List()); public override IEnumerable PreResolveSubStatements => Enumerable.Empty(); [ContractInvariantMethod] @@ -43,13 +44,14 @@ public AssignOrReturnStmt(Cloner cloner, AssignOrReturnStmt original) : base(clo Rhs = (ExprRhs)cloner.CloneRHS(original.Rhs); Rhss = original.Rhss.ConvertAll(cloner.CloneRHS); KeywordToken = cloner.AttributedTok(original.KeywordToken); + Proof = cloner.CloneBlockStmt(original.Proof); if (cloner.CloneResolvedFields) { ResolvedStatements = original.ResolvedStatements.Select(stmt => cloner.CloneStmt(stmt, false)).ToList(); } } - public AssignOrReturnStmt(RangeToken rangeToken, List lhss, ExprRhs rhs, AttributedToken keywordToken, List rhss) + public AssignOrReturnStmt(RangeToken rangeToken, List lhss, ExprRhs rhs, AttributedToken keywordToken, List rhss, BlockStmt proof = null) : base(rangeToken, lhss) { Contract.Requires(rangeToken != null); Contract.Requires(lhss != null); @@ -59,6 +61,7 @@ public AssignOrReturnStmt(RangeToken rangeToken, List lhss, ExprRhs Rhs = rhs; Rhss = rhss; KeywordToken = keywordToken; + Proof = proof; } public override IEnumerable PreResolveSubExpressions { @@ -190,6 +193,8 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti return; } + ModuleResolver.ResolveByProof(resolver, Proof, resolutionContext); + Expression lhsExtract = null; if (expectExtract) { if (resolutionContext.CodeContext is Method caller && caller.Outs.Count == 0 && KeywordToken == null) { @@ -285,7 +290,7 @@ private void DesugarElephantStatement(bool expectExtract, Expression lhsExtract, } } // " temp, ... := MethodOrExpression, ...;" - UpdateStmt up = new UpdateStmt(RangeToken, lhss2, rhss2); + UpdateStmt up = new UpdateStmt(RangeToken, lhss2, rhss2, Proof); if (expectExtract) { up.OriginalInitialLhs = Lhss.Count == 0 ? null : Lhss[0]; } diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs index 1d1db731578..9e28b8bfce7 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs @@ -77,6 +77,10 @@ public override void GenResolve(INewOrOldResolver resolver, ResolutionContext re Contract.Requires(this != null); Contract.Requires(resolutionContext != null); + if (!resolutionContext.IsGhost && resolver.Options.ForbidNondeterminism) { + resolver.Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_assign_such_that_forbidden, + Tok, "assign-such-that statement forbidden by the --enforce-determinism option"); + } base.GenResolve(resolver, resolutionContext); if (AssumeToken != null) { diff --git a/Source/DafnyCore/AST/Statements/Assignment/HavocRhs.cs b/Source/DafnyCore/AST/Statements/Assignment/HavocRhs.cs index 73e32f52b8e..6146bc29952 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/HavocRhs.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/HavocRhs.cs @@ -16,4 +16,10 @@ private HavocRhs(Cloner cloner, HavocRhs havocRhs) : base(cloner, havocRhs) { public override bool CanAffectPreviouslyKnownExpressions { get { return false; } } public override IEnumerable Children => Enumerable.Empty(); public override IEnumerable PreResolveChildren => Enumerable.Empty(); + + public void Resolve(INewOrOldResolver resolver, ResolutionContext resolutionContext) { + if (!resolutionContext.IsGhost && resolver.Options.ForbidNondeterminism) { + resolver.Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_nondeterminism_forbidden, Tok, "nondeterministic assignment forbidden by the --enforce-determinism option"); + } + } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs index cc3fe0507f1..0b61df6ab30 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs @@ -8,6 +8,7 @@ public class UpdateStmt : ConcreteUpdateStatement, ICloneable, ICanR public readonly List Rhss; public readonly bool CanMutateKnownState; public Expression OriginalInitialLhs = null; + public readonly BlockStmt Proof; public override IToken Tok { get { @@ -22,7 +23,7 @@ public override IToken Tok { } [FilledInDuringResolution] public List ResolvedStatements; - public override IEnumerable SubStatements => Children.OfType(); + public override IEnumerable SubStatements => Children.OfType().Concat(Proof != null ? Proof.SubStatements : new List()); public override IEnumerable NonSpecificationSubExpressions => ResolvedStatements == null ? Rhss.SelectMany(r => r.NonSpecificationSubExpressions) : Enumerable.Empty(); @@ -45,26 +46,29 @@ public UpdateStmt Clone(Cloner cloner) { public UpdateStmt(Cloner cloner, UpdateStmt original) : base(cloner, original) { Rhss = original.Rhss.Select(cloner.CloneRHS).ToList(); CanMutateKnownState = original.CanMutateKnownState; + Proof = cloner.CloneBlockStmt(original.Proof); if (cloner.CloneResolvedFields) { ResolvedStatements = original.ResolvedStatements.Select(stmt => cloner.CloneStmt(stmt, false)).ToList(); } } - public UpdateStmt(RangeToken rangeToken, List lhss, List rhss) + public UpdateStmt(RangeToken rangeToken, List lhss, List rhss, BlockStmt proof = null) : base(rangeToken, lhss) { Contract.Requires(cce.NonNullElements(lhss)); Contract.Requires(cce.NonNullElements(rhss)); Contract.Requires(lhss.Count != 0 || rhss.Count == 1); Rhss = rhss; CanMutateKnownState = false; + Proof = proof; } - public UpdateStmt(RangeToken rangeToken, List lhss, List rhss, bool mutate) + public UpdateStmt(RangeToken rangeToken, List lhss, List rhss, bool mutate, BlockStmt proof = null) : base(rangeToken, lhss) { Contract.Requires(cce.NonNullElements(lhss)); Contract.Requires(cce.NonNullElements(rhss)); Contract.Requires(lhss.Count != 0 || rhss.Count == 1); Rhss = rhss; CanMutateKnownState = mutate; + Proof = proof; } public override IEnumerable PreResolveSubExpressions { @@ -123,6 +127,9 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti resolver.ResolveAttributes(rhs, resolutionContext); } + // resolve proof + ModuleResolver.ResolveByProof(resolver, Proof, resolutionContext); + // figure out what kind of UpdateStmt this is if (firstEffectfulRhs == null) { if (Lhss.Count == 0) { @@ -178,7 +185,7 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti foreach (var ll in Lhss) { resolvedLhss.Add(ll.Resolved); } - CallStmt a = new CallStmt(RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok); + CallStmt a = new CallStmt(RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok, Proof); a.OriginalInitialLhs = OriginalInitialLhs; ResolvedStatements.Add(a); } diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/AlternativeStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/AlternativeStmt.cs index 60e52485d2a..4ad76ab0c4f 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/AlternativeStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/AlternativeStmt.cs @@ -57,4 +57,49 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { formatter.VisitAlternatives(Alternatives, indentBefore); }); } + + public void Resolve(INewOrOldResolver resolver, ResolutionContext resolutionContext) { + if (!resolutionContext.IsGhost && resolver.Options.ForbidNondeterminism && 2 <= Alternatives.Count) { + resolver.Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_case_based_if_forbidden, Tok, + "case-based if statement forbidden by the --enforce-determinism option"); + } + ResolveAlternatives(resolver, Alternatives, null, resolutionContext); + } + + public static void ResolveAlternatives(INewOrOldResolver resolver, List alternatives, + AlternativeLoopStmt loopToCatchBreaks, ResolutionContext resolutionContext) { + Contract.Requires(alternatives != null); + Contract.Requires(resolutionContext != null); + + // first, resolve the guards + foreach (var alternative in alternatives) { + int prevErrorCount = resolver.Reporter.Count(ErrorLevel.Error); + resolver.ResolveExpression(alternative.Guard, resolutionContext); // follows from postcondition of ResolveExpression + bool successfullyResolved = resolver.Reporter.Count(ErrorLevel.Error) == prevErrorCount; + resolver.ConstrainTypeExprBool(alternative.Guard, "condition is expected to be of type bool, but is {0}"); + } + + if (loopToCatchBreaks != null) { + resolver.LoopStack.Add(loopToCatchBreaks); // push + } + foreach (var alternative in alternatives) { + resolver.Scope.PushMarker(); + resolver.DominatingStatementLabels.PushMarker(); + if (alternative.IsBindingGuard) { + var exists = (ExistsExpr)alternative.Guard; + foreach (var v in exists.BoundVars) { + resolver.ScopePushAndReport(resolver.Scope, v, "bound-variable"); + } + } + resolver.ResolveAttributes(alternative, resolutionContext); + foreach (Statement ss in alternative.Body) { + resolver.ResolveStatementWithLabels(ss, resolutionContext); + } + resolver.DominatingStatementLabels.PopMarker(); + resolver.Scope.PopMarker(); + } + if (loopToCatchBreaks != null) { + resolver.LoopStack.RemoveAt(resolver.LoopStack.Count - 1); // pop + } + } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/IfStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/IfStmt.cs index 78b9ed3bbaf..ed5717638e4 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/IfStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/IfStmt.cs @@ -86,4 +86,36 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { } return false; } + + public void Resolve(INewOrOldResolver resolver, ResolutionContext resolutionContext) { + if (Guard != null) { + if (!resolutionContext.IsGhost && IsBindingGuard && resolver.Options.ForbidNondeterminism) { + resolver.Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_binding_if_forbidden, Tok, "binding if statement forbidden by the --enforce-determinism option"); + } + resolver.ResolveExpression(Guard, resolutionContext); + resolver.ConstrainTypeExprBool(Guard, "condition is expected to be of type bool, but is {0}"); + } else { + if (!resolutionContext.IsGhost && resolver.Options.ForbidNondeterminism) { + resolver.Reporter.Error(MessageSource.Resolver, GeneratorErrors.ErrorId.c_nondeterministic_if_forbidden, Tok, "nondeterministic if statement forbidden by the --enforce-determinism option"); + } + } + + resolver.Scope.PushMarker(); + if (IsBindingGuard) { + var exists = (ExistsExpr)Guard; + foreach (var v in exists.BoundVars) { + resolver.ScopePushAndReport(resolver.Scope, v.Name, v, v.Tok, "bound-variable"); + } + } + resolver.DominatingStatementLabels.PushMarker(); + resolver.ResolveBlockStatement(Thn, resolutionContext); + resolver.DominatingStatementLabels.PopMarker(); + resolver.Scope.PopMarker(); + + if (Els != null) { + resolver.DominatingStatementLabels.PushMarker(); + resolver.ResolveStatement(Els, resolutionContext); + resolver.DominatingStatementLabels.PopMarker(); + } + } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs b/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs index fc52debc2a6..41348dae006 100644 --- a/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs +++ b/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs @@ -25,11 +25,12 @@ void ObjectInvariant() { public readonly ActualBindings Bindings; public List Args => Bindings.Arguments; public Expression OriginalInitialLhs = null; + public readonly BlockStmt Proof; public Expression Receiver { get { return MethodSelect.Obj; } } public Method Method { get { return (Method)MethodSelect.Member; } } - public CallStmt(RangeToken rangeToken, List lhs, MemberSelectExpr memSel, List args, IToken overrideToken = null) + public CallStmt(RangeToken rangeToken, List lhs, MemberSelectExpr memSel, List args, IToken overrideToken = null, BlockStmt proof = null) : base(rangeToken) { Contract.Requires(rangeToken != null); Contract.Requires(cce.NonNullElements(lhs)); @@ -41,6 +42,7 @@ public CallStmt(RangeToken rangeToken, List lhs, MemberSelectExpr me this.MethodSelect = memSel; this.overrideToken = overrideToken; this.Bindings = new ActualBindings(args); + Proof = proof; } public CallStmt Clone(Cloner cloner) { @@ -52,14 +54,15 @@ public CallStmt(Cloner cloner, CallStmt original) : base(cloner, original) { Lhs = original.Lhs.Select(cloner.CloneExpr).ToList(); Bindings = new ActualBindings(cloner, original.Bindings); overrideToken = original.overrideToken; + Proof = cloner.CloneBlockStmt(original.Proof); } /// /// This constructor is intended to be used when constructing a resolved CallStmt. The "args" are expected /// to be already resolved, and are all given positionally. /// - public CallStmt(RangeToken rangeToken, List lhs, MemberSelectExpr memSel, List args) - : this(rangeToken, lhs, memSel, args.ConvertAll(e => new ActualBinding(null, e))) { + public CallStmt(RangeToken rangeToken, List lhs, MemberSelectExpr memSel, List args, BlockStmt proof = null) + : this(rangeToken, lhs, memSel, args.ConvertAll(e => new ActualBinding(null, e)), proof: proof) { Bindings.AcceptArgumentExpressionsAsExactParameterList(); } diff --git a/Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs b/Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs index cf08c54bfa6..42ec4a47507 100644 --- a/Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs +++ b/Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs @@ -17,10 +17,7 @@ static PrintStmt() { options.EnforcePrintEffects = value; }); - DooFile.RegisterLibraryChecks( - checks: new Dictionary { - { TrackPrintEffectsOption, OptionCompatibility.CheckOptionLocalImpliesLibrary } - }); + OptionRegistry.RegisterGlobalOption(TrackPrintEffectsOption, OptionCompatibility.CheckOptionLocalImpliesLibrary); } [ContractInvariantMethod] diff --git a/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs b/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs index 295803e9e6e..306f1d4815b 100644 --- a/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs @@ -89,16 +89,7 @@ public override void GenResolve(INewOrOldResolver resolver, ResolutionContext co base.GenResolve(resolver, context); - if (Proof != null) { - // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave a the proof body - var prevLblStmts = resolver.EnclosingStatementLabels; - var prevLoopStack = resolver.LoopStack; - resolver.EnclosingStatementLabels = new Scope(resolver.Options); - resolver.LoopStack = new List(); - resolver.ResolveStatement(Proof, context); - resolver.EnclosingStatementLabels = prevLblStmts; - resolver.LoopStack = prevLoopStack; - } + ModuleResolver.ResolveByProof(resolver, Proof, context); } public bool HasAssertOnlyAttribute(out AssertOnlyKind assertOnlyKind) { diff --git a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs index ba3f7a8ab20..ba9804f4edd 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs @@ -9,6 +9,7 @@ public class NewtypeDecl : TopLevelDeclWithMembers, RevealableTypeDecl, Redirect public override string WhatKind { get { return "newtype"; } } public override bool CanBeRevealed() { return true; } public PreType BasePreType; + PreType RedirectingTypeDecl.BasePreType => BasePreType; public Type BaseType { get; set; } // null when refining public BoundVar Var { get; set; } // can be null (if non-null, then object.ReferenceEquals(Var.Type, BaseType)) public Expression Constraint { get; set; } // is null iff Var is @@ -31,19 +32,25 @@ bool RedirectingTypeDecl.ConstraintIsCompilable { [FilledInDuringResolution] public bool TargetTypeCoversAllBitPatterns; // "target complete" -- indicates that any bit pattern that can fill the target type is a value of the newtype - public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Type baseType, List parentTraits, - List members, Attributes attributes, bool isRefining) - : base(rangeToken, name, module, new List(), members, attributes, isRefining, parentTraits) { + public NewtypeDecl(RangeToken rangeToken, Name name, List typeParameters, ModuleDefinition module, + Type baseType, + SubsetTypeDecl.WKind witnessKind, Expression witness, List parentTraits, List members, Attributes attributes, bool isRefining) + : base(rangeToken, name, module, typeParameters, members, attributes, isRefining, parentTraits) { Contract.Requires(rangeToken != null); Contract.Requires(name != null); Contract.Requires(module != null); Contract.Requires(isRefining ^ (baseType != null)); + Contract.Requires((witnessKind == SubsetTypeDecl.WKind.Compiled || witnessKind == SubsetTypeDecl.WKind.Ghost) == (witness != null)); Contract.Requires(members != null); BaseType = baseType; + Witness = witness; + WitnessKind = witnessKind; this.NewSelfSynonym(); } - public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, BoundVar bv, Expression constraint, - SubsetTypeDecl.WKind witnessKind, Expression witness, List parentTraits, List members, Attributes attributes, bool isRefining) : base(rangeToken, name, module, new List(), members, attributes, isRefining, parentTraits) { + public NewtypeDecl(RangeToken rangeToken, Name name, List typeParameters, ModuleDefinition module, + BoundVar bv, Expression constraint, + SubsetTypeDecl.WKind witnessKind, Expression witness, List parentTraits, List members, Attributes attributes, bool isRefining) + : base(rangeToken, name, module, typeParameters, members, attributes, isRefining, parentTraits) { Contract.Requires(rangeToken != null); Contract.Requires(name != null); Contract.Requires(module != null); @@ -60,11 +67,16 @@ public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Bo public Type ConcreteBaseType(List typeArguments) { Contract.Requires(TypeArgs.Count == typeArguments.Count); + if (typeArguments.Count == 0) { + // this optimization seems worthwhile + return BaseType; + } var subst = TypeParameter.SubstitutionMap(TypeArgs, typeArguments); return BaseType.Subst(subst); } - /// /// Return .BaseType instantiated with "typeArgs", but only look at the part of .BaseType that is in scope. + /// + /// Return .BaseType instantiated with "typeArgs", but only look at the part of .BaseType that is in scope. /// public Type RhsWithArgument(List typeArgs) { Contract.Requires(typeArgs != null); @@ -78,21 +90,7 @@ public Type RhsWithArgument(List typeArgs) { return rtd.SelfSynonym(typeArgs); } } - return RhsWithArgumentIgnoringScope(typeArgs); - } - /// - /// Returns the declared .BaseType but with formal type arguments replaced by the given actuals. - /// - public Type RhsWithArgumentIgnoringScope(List typeArgs) { - Contract.Requires(typeArgs != null); - Contract.Requires(typeArgs.Count == TypeArgs.Count); - // Instantiate with the actual type arguments - if (typeArgs.Count == 0) { - // this optimization seems worthwhile - return BaseType; - } else { - return ConcreteBaseType(typeArgs); - } + return ConcreteBaseType(typeArgs); } public TopLevelDecl AsTopLevelDecl => this; @@ -121,7 +119,7 @@ public TypeParameter.EqualitySupportValue EqualitySupport { bool ICodeContext.IsGhost { get { throw new NotSupportedException(); } // if .IsGhost is needed, the object should always be wrapped in an CodeContextWrapper } - List ICodeContext.TypeArgs { get { return new List(); } } + List ICodeContext.TypeArgs { get { return TypeArgs; } } List ICodeContext.Ins { get { return new List(); } } ModuleDefinition IASTVisitorContext.EnclosingModule { get { return EnclosingModuleDefinition; } } bool ICodeContext.MustReverify { get { return false; } } diff --git a/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs index 15c2a5a2e82..d5c473087ac 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs @@ -50,6 +50,8 @@ public SubsetTypeDecl(RangeToken rangeToken, Name name, TypeParameter.TypeParame ); BoundVar RedirectingTypeDecl.Var => Var; + PreType RedirectingTypeDecl.BasePreType => Var.PreType; + Type RedirectingTypeDecl.BaseType => Var.Type; Expression RedirectingTypeDecl.Constraint => Constraint; WKind RedirectingTypeDecl.WitnessKind => WitnessKind; Expression RedirectingTypeDecl.Witness => Witness; diff --git a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs index 57f35075f3e..3466a7113f6 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs @@ -64,6 +64,8 @@ public Type RhsWithArgumentIgnoringScope(List typeArgs) { Attributes RedirectingTypeDecl.Attributes { get { return Attributes; } } ModuleDefinition RedirectingTypeDecl.Module { get { return EnclosingModuleDefinition; } } BoundVar RedirectingTypeDecl.Var { get { return null; } } + PreType RedirectingTypeDecl.BasePreType { get { return null; } } + Type RedirectingTypeDecl.BaseType { get { return null; } } Expression RedirectingTypeDecl.Constraint { get { return null; } } bool RedirectingTypeDecl.ConstraintIsCompilable { diff --git a/Source/DafnyCore/AST/Types/TypeParameter.cs b/Source/DafnyCore/AST/Types/TypeParameter.cs index 9faeb2dcefe..7b4a5e1d70d 100644 --- a/Source/DafnyCore/AST/Types/TypeParameter.cs +++ b/Source/DafnyCore/AST/Types/TypeParameter.cs @@ -7,10 +7,13 @@ namespace Microsoft.Dafny; public class TypeParameter : TopLevelDecl { public interface ParentType { string FullName { get; } + IToken Tok { get; } } public override string WhatKind => "type parameter"; + public bool IsAutoCompleted => Name.StartsWith("_"); + ParentType parent; public ParentType Parent { get { diff --git a/Source/DafnyCore/AST/Types/Types.cs b/Source/DafnyCore/AST/Types/Types.cs index 19950989125..7c49af62df7 100644 --- a/Source/DafnyCore/AST/Types/Types.cs +++ b/Source/DafnyCore/AST/Types/Types.cs @@ -338,11 +338,10 @@ public bool IsNumericBased(NumericPersuasion p) { } else if (t.IsRealType) { return p == NumericPersuasion.Real; } - var d = t.AsNewtype; - if (d == null) { + if (t.AsNewtype is not { } newtypeDecl) { return false; } - t = d.BaseType; + t = newtypeDecl.RhsWithArgument(t.TypeArgs); } } diff --git a/Source/DafnyCore/Auditor/Auditor.cs b/Source/DafnyCore/Auditor/Auditor.cs index f6f2e7f8e76..a09dbeee9c2 100644 --- a/Source/DafnyCore/Auditor/Auditor.cs +++ b/Source/DafnyCore/Auditor/Auditor.cs @@ -66,9 +66,9 @@ static Auditor() { "md-ietf", "markdown-ietf", "txt"); - DooFile.RegisterNoChecksNeeded(ReportFileOption, false); - DooFile.RegisterNoChecksNeeded(ReportFormatOption, false); - DooFile.RegisterNoChecksNeeded(CompareReportOption, false); + OptionRegistry.RegisterOption(ReportFileOption, OptionScope.Cli); + OptionRegistry.RegisterOption(ReportFormatOption, OptionScope.Cli); + OptionRegistry.RegisterOption(CompareReportOption, OptionScope.Cli); } /// diff --git a/Source/DafnyCore/Backends/BoogieExtractor.cs b/Source/DafnyCore/Backends/BoogieExtractor.cs new file mode 100644 index 00000000000..86b110d7091 --- /dev/null +++ b/Source/DafnyCore/Backends/BoogieExtractor.cs @@ -0,0 +1,350 @@ +//----------------------------------------------------------------------------- +// +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT +// +//----------------------------------------------------------------------------- + +#nullable enable + +using System; +using System.Collections.Generic; +using System.Linq; +using System.Numerics; +using System.Diagnostics.Contracts; +using Microsoft.BaseTypes; +using Microsoft.Boogie; + +namespace Microsoft.Dafny.Compilers { + public class ExtractorError : Exception { + public ExtractorError(string message) + : base(message) { + } + } + + public class BoogieExtractor : ASTVisitor { + /// + /// Says to look inside the module for contents to extract. + /// Can be applied to a module. + /// + /// Note: This attribute isn't used yet, so the use of the attribute is just a stylistic thing at the moment. + /// Similarly, one can imagine that the extractor will look at a module's export clauses, to--in some way--check that + /// the set of Boogie declarations exported are self consistent. But that isn't done yet, either. Instead, all contents + /// of all files given to the extractor are considered for extraction. + /// + private const string ExtractAttribute = "extract_boogie"; + + /// + /// Gives the Boogie name to be used in the extraction. + /// Can be applied to types and functions. + /// + private const string NameAttribute = "extract_boogie_name"; + + /// + /// Says to place the extracted axiom declaration in the "uses" block of the given function. + /// Can be applied to lemmas. + /// + private const string UsedByAttribute = "extract_used_by"; + + /// + /// Gives a matching pattern to be applied in the quantifier emitted from a lemma or from a quantifier. + /// Can be applied to lemmas and quantifiers. + /// + private const string PatternAttribute = "extract_pattern"; + + /// + /// Specifies an additional attribute to be attached to the quantifier emitted from a lemma. + /// Can be applied to lemmas. + /// + private const string AttributeAttribute = "extract_attribute"; + + /// + /// Throws an "ExtractorError" if the input is unexpected or unsupported. + /// + public static Boogie.Program Extract(Program program) { + var extractor = new BoogieExtractor(); + extractor.VisitModule(program.DefaultModule); + extractor.FixUpUsedByInformation(); + + var extractedProgram = new Boogie.Program(); + extractedProgram.AddTopLevelDeclarations(extractor.allDeclarations); + return extractedProgram; + } + + private List declarations = new(); // for the current module + private List allDeclarations = new(); // these are the declarations for all modules marked with {:extract} + private readonly Dictionary functionExtractions = new(); + private readonly List<(Boogie.Axiom, Function)> axiomUsedBy = new(); + + private BoogieExtractor() { + } + + void FixUpUsedByInformation() { + foreach (var (axiom, function) in axiomUsedBy) { + if (!functionExtractions.TryGetValue(function, out var boogieFunction)) { + throw new ExtractorError($":{UsedByAttribute} attribute mentions non-extracted function: {function.Name}"); + } + boogieFunction.OtherDefinitionAxioms.Add(axiom); + } + axiomUsedBy.Clear(); + } + + public override IASTVisitorContext GetContext(IASTVisitorContext astVisitorContext, bool inFunctionPostcondition) { + return astVisitorContext; + } + + void VisitModule(ModuleDecl module) { + var previousDeclarations = declarations; + declarations = new(); + + VisitDeclarations(module.Signature.TopLevels.Values.ToList()); + + if (Attributes.Contains(module.Signature.ModuleDef.Attributes, ExtractAttribute)) { + declarations.Sort((d0, d1) => d0.tok.pos - d1.tok.pos); + allDeclarations.AddRange(declarations); + } + declarations = previousDeclarations; + } + + protected override void VisitOneDeclaration(TopLevelDecl decl) { + if (decl is ModuleDecl moduleDecl) { + VisitModule(moduleDecl); + return; + } + + if (GetExtractName(decl.Attributes) is { } extractName) { + var ty = new Boogie.TypeCtorDecl(decl.tok, extractName, decl.TypeArgs.Count); + declarations.Add(ty); + } + + base.VisitOneDeclaration(decl); // this will visit the declaration's members + } + + public override void VisitMethod(Method method) { + if (method is not Lemma lemma) { + return; + } + + var patterns = Attributes.FindAllExpressions(lemma.Attributes, PatternAttribute); + var usedByInfo = Attributes.Find(lemma.Attributes, UsedByAttribute); + if (patterns == null && usedByInfo == null) { + return; + } + + if ((lemma.Ins.Count == 0) != (patterns == null)) { + throw new ExtractorError($"a parameterized lemma must specify at least one :{PatternAttribute}: {lemma.Name}"); + } + if (lemma.TypeArgs.Count != 0) { + throw new ExtractorError($"an extracted lemma is not allowed to have type parameters: {lemma.Name}"); + } + if (lemma.Outs.Count != 0) { + throw new ExtractorError($"an extracted lemma is not allowed to have out-parameters: {lemma.Name}"); + } + + var tok = lemma.tok; + + var boundVars = lemma.Ins.ConvertAll(formal => + (Boogie.Variable)new Boogie.BoundVariable(tok, new TypedIdent(tok, formal.Name, ExtractType(formal.Type))) + ); + + var triggers = GetTriggers(tok, patterns); + + var ante = BoogieGenerator.BplAnd(lemma.Req.ConvertAll(req => ExtractExpr(req.E))); + var post = BoogieGenerator.BplAnd(lemma.Ens.ConvertAll(ens => ExtractExpr(ens.E))); + var body = BoogieGenerator.BplImp(ante, post); + + Boogie.Expr axiomBody; + if (boundVars.Count == 0) { + axiomBody = body; + } else { + var kv = GetKeyValues(tok, lemma.Attributes); + axiomBody = new Boogie.ForallExpr(tok, new List(), boundVars, kv, triggers, body); + } + var axiom = new Boogie.Axiom(tok, axiomBody); + declarations.Add(axiom); + + if (usedByInfo != null) { + if (usedByInfo.Args.Count == 1 && usedByInfo.Args[0].Resolved is MemberSelectExpr { Member: Function function }) { + axiomUsedBy.Add((axiom, function)); + } else { + throw new ExtractorError($":{UsedByAttribute} argument on lemma '{lemma.Name}' is expected to be an extracted function"); + } + } + } + + private Trigger? GetTriggers(IToken tok, List>? patterns) { + if (patterns == null) { + return null; + } + + Boogie.Trigger? triggers = null; + for (var i = 0; i < patterns.Count; i++) { + var terms = patterns![i].ConvertAll(ExtractExpr); + triggers = new Boogie.Trigger(tok, true, terms, triggers); + } + + return triggers; + } + + private QKeyValue? GetKeyValues(IToken tok, Attributes attributes) { + Boogie.QKeyValue kv = null; + var extractAttributes = Attributes.FindAllExpressions(attributes, AttributeAttribute); + if (extractAttributes != null) { + if (extractAttributes.Count == 0) { + throw new ExtractorError($"first argument to :{AttributeAttribute} is expected to be a literal string; got no arguments"); + } + for (var i = extractAttributes.Count; 0 <= --i;) { + string? attrName = null; + var parameters = new List(); + foreach (var argument in extractAttributes[i]) { + if (attrName != null) { + parameters.Add(ExtractExpr(argument)); + } else if (argument is StringLiteralExpr { Value: string name }) { + attrName = name; + } else { + throw new ExtractorError($"first argument to :{AttributeAttribute} is expected to be a literal string; got: {argument}"); + } + } + + kv = new Boogie.QKeyValue(tok, attrName, parameters, kv); + } + } + + return kv; + } + + public override void VisitFunction(Function function) { + if (GetExtractName(function.Attributes) is { } extractName) { + var tok = function.tok; + if (function.TypeArgs.Count != 0) { + throw new ExtractorError($"an extracted function is not allowed to have type parameters: {function.Name}"); + } + var inParams = function.Ins.ConvertAll(formal => + (Boogie.Variable)new Boogie.Formal(tok, new TypedIdent(tok, formal.Name, ExtractType(formal.Type)), true) + ); + var result = new Boogie.Formal(tok, new TypedIdent(tok, TypedIdent.NoName, ExtractType(function.ResultType)), false); + var fn = new Boogie.Function(tok, extractName, inParams, result); + declarations.Add(fn); + functionExtractions.Add(function, fn); + } + } + + private Boogie.Type ExtractType(Type type) { + switch (type) { + case IntType: + return Boogie.Type.Int; + case BoolType: + return Boogie.Type.Bool; + case UserDefinedType udt: { + var cl = udt.ResolvedClass; + var name = GetExtractName(cl.Attributes) ?? cl.Name; + return new Boogie.UnresolvedTypeIdentifier(Boogie.Token.NoToken, name, udt.TypeArgs.ConvertAll(ExtractType)); + } + default: + throw new ExtractorError($"type not supported by extractor: {type}"); + } + } + + private string? GetExtractName(Attributes attributes) { + if (Attributes.Find(attributes, NameAttribute) is { } extractNameAttribute) { + if (extractNameAttribute.Args.Count == 1 && extractNameAttribute.Args[0] is StringLiteralExpr { Value: string extractName }) { + return extractName; + } + } + return null; + } + + private Boogie.Expr ExtractExpr(Expression expr) { + expr = expr.Resolved; + var tok = expr.tok; + switch (expr) { + case LiteralExpr literalExpr: { + if (literalExpr.Value is bool boolValue) { + // use the specific literals, rather than Boogie.LiteralExpr(bool), in order for the + // peephole optimizations to kick in + return boolValue ? Boogie.Expr.True : Boogie.Expr.False; + } else if (literalExpr.Value is BigInteger intValue) { + var n = BigNum.FromBigInt(intValue); + return Boogie.Expr.Literal(n); + } + break; + } + + case IdentifierExpr identifierExpr: + return new Boogie.IdentifierExpr(tok, identifierExpr.Name); + + case FunctionCallExpr functionCallExpr: { + var function = functionCallExpr.Function; + var functionName = GetExtractName(function.Attributes) ?? function.Name; + Contract.Assert(function.IsStatic); + var arguments = functionCallExpr.Args.ConvertAll(ExtractExpr); + return new Boogie.NAryExpr(tok, new Boogie.FunctionCall(new Boogie.IdentifierExpr(tok, functionName)), arguments); + } + + case BinaryExpr binaryExpr: { + var e0 = ExtractExpr(binaryExpr.E0); + var e1 = ExtractExpr(binaryExpr.E1); + switch (binaryExpr.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.EqCommon: + return Boogie.Expr.Eq(e0, e1); + case BinaryExpr.ResolvedOpcode.NeqCommon: + return Boogie.Expr.Neq(e0, e1); + case BinaryExpr.ResolvedOpcode.Iff: + return BoogieGenerator.BplIff(e0, e1); + case BinaryExpr.ResolvedOpcode.Imp: + return BoogieGenerator.BplImp(e0, e1); + case BinaryExpr.ResolvedOpcode.And: + return BoogieGenerator.BplAnd(e0, e1); + case BinaryExpr.ResolvedOpcode.Or: + return BoogieGenerator.BplOr(e0, e1); + case BinaryExpr.ResolvedOpcode.Le: + return Boogie.Expr.Le(e0, e1); + case BinaryExpr.ResolvedOpcode.Lt: + return Boogie.Expr.Lt(e0, e1); + case BinaryExpr.ResolvedOpcode.Add: + return Boogie.Expr.Add(e0, e1); + case BinaryExpr.ResolvedOpcode.Sub: + return Boogie.Expr.Sub(e0, e1); + default: + break; + } + break; + } + + case UnaryOpExpr unaryOpExpr: + if (unaryOpExpr.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BoolNot) { + var e = ExtractExpr(unaryOpExpr.E); + return Boogie.Expr.Not(e); + } else { + throw new ExtractorError($"extractor does not support unary operator {unaryOpExpr.ResolvedOp}"); + } + + case QuantifierExpr quantifierExpr: { + var boundVars = quantifierExpr.BoundVars.ConvertAll(boundVar => + (Boogie.Variable)new Boogie.BoundVariable(tok, new TypedIdent(tok, boundVar.Name, ExtractType(boundVar.Type))) + ); + + var patterns = Attributes.FindAllExpressions(quantifierExpr.Attributes, PatternAttribute); + if (patterns.Count == 0) { + throw new ExtractorError($"extraction expects every quantifier to specify at least one :{PatternAttribute}"); + } + var triggers = GetTriggers(tok, patterns); + + var kv = GetKeyValues(tok, quantifierExpr.Attributes); + var body = ExtractExpr(quantifierExpr.LogicalBody()); + if (quantifierExpr is ExistsExpr) { + return new Boogie.ExistsExpr(tok, new List(), boundVars, kv, triggers, body); + } else { + Contract.Assert(quantifierExpr is ForallExpr); + return new Boogie.ForallExpr(tok, new List(), boundVars, kv, triggers, body); + } + } + + default: + break; + } + + throw new ExtractorError($"extraction does not support expression of type {expr.GetType()}: {expr}"); + } + } +} diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index 7db21e91763..f6e21f77093 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -1572,7 +1572,7 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, return "bool"; } else if (xType is CharType) { return CharTypeName; - } else if (xType is IntType || xType is BigOrdinalType) { + } else if (xType is IntType or BigOrdinalType) { return "BigInteger"; } else if (xType is RealType) { return "Dafny.BigRational"; @@ -1580,11 +1580,11 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, var t = (BitvectorType)xType; return t.NativeType != null ? GetNativeTypeName(t.NativeType) : "BigInteger"; } else if (xType.AsNewtype != null && member == null) { // when member is given, use UserDefinedType case below - var nativeType = xType.AsNewtype.NativeType; - if (nativeType != null) { + var newtypeDecl = xType.AsNewtype; + if (newtypeDecl.NativeType is { } nativeType) { return GetNativeTypeName(nativeType); } - return TypeName(xType.AsNewtype.BaseType, wr, tok); + return TypeName(newtypeDecl.ConcreteBaseType(xType.TypeArgs), wr, tok); } else if (xType.IsObjectQ) { return "object"; } else if (xType.IsArrayType) { @@ -1679,7 +1679,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree return "false"; } else if (xType is CharType) { return UnicodeCharEnabled ? $"new {CharTypeName}({CharType.DefaultValueAsString})" : CharType.DefaultValueAsString; - } else if (xType is IntType || xType is BigOrdinalType) { + } else if (xType is IntType or BigOrdinalType) { return "BigInteger.Zero"; } else if (xType is RealType) { return "Dafny.BigRational.ZERO"; @@ -1708,7 +1708,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree } else if (td.NativeType != null) { return "0"; } else { - return TypeInitializationValue(td.BaseType, wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); + return TypeInitializationValue(td.ConcreteBaseType(udt.TypeArgs), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); } } else if (cl is SubsetTypeDecl) { var td = (SubsetTypeDecl)cl; diff --git a/Source/DafnyCore/Backends/CodeGeneratorTypeExtensions.cs b/Source/DafnyCore/Backends/CodeGeneratorTypeExtensions.cs index e72ebd608c2..1fae5747c3e 100644 --- a/Source/DafnyCore/Backends/CodeGeneratorTypeExtensions.cs +++ b/Source/DafnyCore/Backends/CodeGeneratorTypeExtensions.cs @@ -14,8 +14,7 @@ public static class CompilerTypeExtensions { /// public static Type GetRuntimeType(this Type typ) { while (typ.AsNewtype is { NativeType: null } newtypeDecl) { - var subst = TypeParameter.SubstitutionMap(newtypeDecl.TypeArgs, typ.TypeArgs); - typ = newtypeDecl.BaseType.Subst(subst); + typ = newtypeDecl.ConcreteBaseType(typ.TypeArgs); } return typ.NormalizeExpand(); } diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs index 30c188ebc8c..8eada0edcdf 100644 --- a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs @@ -923,7 +923,7 @@ protected string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDe return "bool"; } else if (xType is CharType) { return "char"; - } else if (xType is IntType || xType is BigOrdinalType) { + } else if (xType is IntType or BigOrdinalType) { UnsupportedFeatureError(tok, Feature.UnboundedIntegers); return "BigNumber"; } else if (xType is RealType) { @@ -933,11 +933,11 @@ protected string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDe var t = (BitvectorType)xType; return t.NativeType != null ? GetNativeTypeName(t.NativeType) : "BigNumber"; } else if (xType.AsNewtype != null) { - NativeType nativeType = xType.AsNewtype.NativeType; - if (nativeType != null) { + var newtypeDecl = xType.AsNewtype; + if (newtypeDecl.NativeType is { } nativeType) { return GetNativeTypeName(nativeType); } - return TypeName(xType.AsNewtype.BaseType, wr, tok); + return TypeName(newtypeDecl.ConcreteBaseType(xType.TypeArgs), wr, tok, member); } else if (xType.IsObjectQ) { return "object"; } else if (xType.IsArrayType) { @@ -1046,7 +1046,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree } else if (td.NativeType != null) { return "0"; } else { - return TypeInitializationValue(td.BaseType, wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); + return TypeInitializationValue(td.ConcreteBaseType(udt.TypeArgs), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); } } else if (cl is SubsetTypeDecl) { var td = (SubsetTypeDecl)cl; diff --git a/Source/DafnyCore/Backends/Dafny/AST.dfy b/Source/DafnyCore/Backends/Dafny/AST.dfy index 410ec735605..379456535d7 100644 --- a/Source/DafnyCore/Backends/Dafny/AST.dfy +++ b/Source/DafnyCore/Backends/Dafny/AST.dfy @@ -36,7 +36,11 @@ module {:extern "DAST"} DAST { // See issue https://github.com/dafny-lang/dafny/issues/5345 datatype Name = Name(dafny_name: string) - datatype Module = Module(name: Name, attributes: seq, body: Option>) + // A special Dafny name wrapper for variable names. + // For example, the identifier 'None' needs to be escaped in Rust, but not as a constructor. + datatype VarName = VarName(dafny_name: string) + + datatype Module = Module(name: Name, attributes: seq, requiresExterns: bool, body: Option>) datatype ModuleItem = | Module(Module) @@ -45,6 +49,28 @@ module {:extern "DAST"} DAST { | Newtype(Newtype) | SynonymType(SynonymType) | Datatype(Datatype) + { + function name(): Name { + match this { + case Module(m) => m.name + case Class(m) => m.name + case Trait(m) => m.name + case Newtype(m) => m.name + case SynonymType(m) => m.name + case Datatype(m) => m.name + } + } + function attributes(): seq { + match this { + case Module(m) => m.attributes + case Class(m) => m.attributes + case Trait(m) => m.attributes + case Newtype(m) => m.attributes + case SynonymType(m) => m.attributes + case Datatype(m) => m.attributes + } + } + } datatype Type = UserDefined(resolved: ResolvedType) | @@ -127,7 +153,7 @@ module {:extern "DAST"} DAST { typeArgs: seq, kind: ResolvedTypeBase, attributes: seq, - properMethods: seq, + properMethods: seq, extendedTypes: seq) { function Replace(mapping: map): ResolvedType { ResolvedType( @@ -175,7 +201,7 @@ module {:extern "DAST"} DAST { datatype Field = Field(formal: Formal, defaultValue: Option) - datatype Formal = Formal(name: Name, typ: Type, attributes: seq) + datatype Formal = Formal(name: VarName, typ: Type, attributes: seq) datatype Method = Method( isStatic: bool, @@ -188,22 +214,22 @@ module {:extern "DAST"} DAST { params: seq, body: seq, outTypes: seq, - outVars: Option>) + outVars: Option>) datatype CallSignature = CallSignature(parameters: seq) datatype CallName = - CallName(name: Name, onType: Option, receiverArgs: Option, signature: CallSignature) | + CallName(name: Name, onType: Option, receiverArg: Option, receiverAsArgument: bool, signature: CallSignature) | MapBuilderAdd | MapBuilderBuild | SetBuilderAdd | SetBuilderBuild datatype Statement = - DeclareVar(name: Name, typ: Type, maybeValue: Option) | + DeclareVar(name: VarName, typ: Type, maybeValue: Option) | Assign(lhs: AssignLhs, value: Expression) | If(cond: Expression, thn: seq, els: seq) | Labeled(lbl: string, body: seq) | While(cond: Expression, body: seq) | - Foreach(boundName: Name, boundType: Type, over: Expression, body: seq) | - Call(on: Expression, callName: CallName, typeArgs: seq, args: seq, outs: Option>) | + Foreach(boundName: VarName, boundType: Type, over: Expression, body: seq) | + Call(on: Expression, callName: CallName, typeArgs: seq, args: seq, outs: Option>) | Return(expr: Expression) | EarlyReturn() | Break(toLabel: Option) | @@ -216,8 +242,8 @@ module {:extern "DAST"} DAST { } datatype AssignLhs = - Ident(ident: Ident) | - Select(expr: Expression, field: Name) | + Ident(ident: VarName) | + Select(expr: Expression, field: VarName) | Index(expr: Expression, indices: seq) datatype CollKind = Seq | Array | Map @@ -244,14 +270,15 @@ module {:extern "DAST"} DAST { datatype Expression = Literal(Literal) | - Ident(name: Name) | + Ident(name: VarName) | Companion(seq, typeArgs: seq) | + ExternCompanion(seq) | Tuple(seq) | New(path: seq, typeArgs: seq, args: seq) | NewUninitArray(dims: seq, typ: Type) | ArrayIndexToInt(value: Expression) | FinalizeNewArray(value: Expression, typ: Type) | - DatatypeValue(datatypeType: ResolvedType, typeArgs: seq, variant: Name, isCo: bool, contents: seq<(string, Expression)>) | + DatatypeValue(datatypeType: ResolvedType, typeArgs: seq, variant: Name, isCo: bool, contents: seq<(VarName, Expression)>) | Convert(value: Expression, from: Type, typ: Type) | SeqConstruct(length: Expression, elem: Expression) | SeqValue(elements: seq, typ: Type) | @@ -270,23 +297,25 @@ module {:extern "DAST"} DAST { ArrayLen(expr: Expression, exprType: Type, dim: nat, native: bool) | MapKeys(expr: Expression) | MapValues(expr: Expression) | - Select(expr: Expression, field: Name, isConstant: bool, onDatatype: bool, fieldType: Type) | - SelectFn(expr: Expression, field: Name, onDatatype: bool, isStatic: bool, arity: nat) | + MapItems(expr: Expression) | + Select(expr: Expression, field: VarName, isConstant: bool, onDatatype: bool, fieldType: Type) | + SelectFn(expr: Expression, field: VarName, onDatatype: bool, isStatic: bool, isConstant: bool, arguments: seq) | Index(expr: Expression, collKind: CollKind, indices: seq) | IndexRange(expr: Expression, isArray: bool, low: Option, high: Option) | TupleSelect(expr: Expression, index: nat, fieldType: Type) | Call(on: Expression, callName: CallName, typeArgs: seq, args: seq) | Lambda(params: seq, retType: Type, body: seq) | BetaRedex(values: seq<(Formal, Expression)>, retType: Type, expr: Expression) | - IIFE(ident: Ident, typ: Type, value: Expression, iifeBody: Expression) | + IIFE(ident: VarName, typ: Type, value: Expression, iifeBody: Expression) | Apply(expr: Expression, args: seq) | TypeTest(on: Expression, dType: seq, variant: Name) | + Is(expr: Expression, fromType: Type, toType: Type) | InitializationValue(typ: Type) | BoolBoundedPool() | SetBoundedPool(of: Expression) | MapBoundedPool(of: Expression) | SeqBoundedPool(of: Expression, includeDuplicates: bool) | - IntRange(lo: Expression, hi: Expression, up: bool) | + IntRange(elemType: Type, lo: Expression, hi: Expression, up: bool) | UnboundedIntRange(start: Expression, up: bool) | Quantifier(elemType: Type, collection: Expression, is_forall: bool, lambda: Expression) diff --git a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs index 0c4396a9d33..9e6e32ae148 100644 --- a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs +++ b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs @@ -35,13 +35,13 @@ public void AddUnsupported(string why) { interface ModuleContainer : Container { void AddModule(Module item); - public ModuleBuilder Module(string name, Sequence attributes) { - return new ModuleBuilder(this, name, attributes); + public ModuleBuilder Module(string name, Sequence attributes, bool requiresExterns) { + return new ModuleBuilder(this, name, attributes, requiresExterns); } static public Module UnsupportedToModule(string why) { return new Module(Sequence.UnicodeFromString(why), Sequence.FromElements((Attribute)Attribute.create_Attribute( - Sequence.UnicodeFromString(why), Sequence>.Empty)), + Sequence.UnicodeFromString(why), Sequence>.Empty)), false, Std.Wrappers.Option>.create_None()); } } @@ -51,11 +51,13 @@ class ModuleBuilder : ClassContainer, TraitContainer, NewtypeContainer, Datatype readonly string name; readonly Sequence attributes; readonly List body = new(); + private readonly bool requiresExterns; - public ModuleBuilder(ModuleContainer parent, string name, Sequence attributes) { + public ModuleBuilder(ModuleContainer parent, string name, Sequence attributes, bool requiresExterns) { this.parent = parent; this.name = name; this.attributes = attributes; + this.requiresExterns = requiresExterns; } public void AddModule(Module item) { @@ -82,6 +84,7 @@ public object Finish() { parent.AddModule((Module)Module.create( Sequence.UnicodeFromString(this.name), attributes, + requiresExterns, Std.Wrappers.Option>.create_Some((Sequence)Sequence.FromArray(body.ToArray())) )); @@ -1834,6 +1837,7 @@ public DAST.Expression Build() { } return (DAST.Expression)DAST.Expression.create_IntRange( + DAST.Type.create_Primitive(DAST.Primitive.create_Int()), startExpr, endExpr, true); } diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs index 15d864b0ab9..980d0fcc3b5 100644 --- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs @@ -92,6 +92,7 @@ public void AddUnsupportedFeature(IToken token, Feature feature) { Feature.ExternalConstructors, Feature.SubtypeConstraintsInQuantifiers, Feature.TuplesWiderThan20, + Feature.ArraysWithMoreThan16Dims, Feature.ForLoops, Feature.Traits, Feature.RuntimeCoverageReport, @@ -119,6 +120,11 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a new ExprBuffer(this), this); } + private bool NeedsExternalImport(MemberDecl memberDecl) { + return !memberDecl.IsGhost && memberDecl.HasExternAttribute && + memberDecl is Function { Body: null } or Method { Body: null }; + } + protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule, string libraryName, ConcreteSyntaxTree wr) { if (currentBuilder is ModuleContainer moduleBuilder) { @@ -126,7 +132,17 @@ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDef if (externModule != null) { attributes = (Sequence)ParseAttributes(externModule.Attributes); } - currentBuilder = moduleBuilder.Module(moduleName, attributes); + + var requiresExternImport = enclosingModule.TopLevelDecls.Any((TopLevelDecl decl) => + (decl is DefaultClassDecl defaultClassDecl && + GetIsExternAndIncluded(defaultClassDecl) is (_, included: false) + && defaultClassDecl.Members.Exists(NeedsExternalImport) + ) || + (decl is ClassLikeDecl classLikeDecl && + GetIsExternAndIncluded(classLikeDecl) is (classIsExtern: true, _)) || + (decl is AbstractTypeDecl) + ); + currentBuilder = moduleBuilder.Module(moduleName, attributes, requiresExternImport); } else { throw new InvalidOperationException(); } @@ -357,17 +373,34 @@ private DAST.Type GenType(Type typ) { return FullTypeNameAST(udt, null); } else if (AsNativeType(typ) != null) { - return (DAST.Type)(AsNativeType(typ).Sel switch { - NativeType.Selection.Byte => DAST.Type.create_Passthrough(Sequence.UnicodeFromString("u8")), - NativeType.Selection.SByte => DAST.Type.create_Passthrough(Sequence.UnicodeFromString("i8")), - NativeType.Selection.Short => DAST.Type.create_Passthrough(Sequence.UnicodeFromString("i16")), - NativeType.Selection.UShort => DAST.Type.create_Passthrough(Sequence.UnicodeFromString("u16")), - NativeType.Selection.Int => DAST.Type.create_Passthrough(Sequence.UnicodeFromString("i32")), - NativeType.Selection.UInt => DAST.Type.create_Passthrough(Sequence.UnicodeFromString("u32")), - NativeType.Selection.Long => DAST.Type.create_Passthrough(Sequence.UnicodeFromString("i64")), - NativeType.Selection.ULong => DAST.Type.create_Passthrough(Sequence.UnicodeFromString("u64")), - NativeType.Selection.DoubleLong => DAST.Type.create_Passthrough(Sequence.UnicodeFromString("i128")), - NativeType.Selection.UDoubleLong => DAST.Type.create_Passthrough(Sequence.UnicodeFromString("u128")), + var CreateNewtype = (string baseName, DAST._INewtypeRange newTypeRange) => + DAST.Type.create_UserDefined( + DAST.ResolvedType.create_ResolvedType( + Sequence>.FromElements( + Sequence.UnicodeFromString(baseName) + ), + Sequence.Empty, + DAST.ResolvedTypeBase.create_Newtype( + DAST.Type.create_Primitive(DAST.Primitive.create_Int()), + newTypeRange, + true + ), + Sequence.Empty, + Sequence>.Empty, + Sequence.Empty + ) + ); + return (DAST.Type)(AsNativeType(xType).Sel switch { + NativeType.Selection.Byte => CreateNewtype("u8", DAST.NewtypeRange.create_U8()), + NativeType.Selection.SByte => CreateNewtype("i8", DAST.NewtypeRange.create_I8()), + NativeType.Selection.Short => CreateNewtype("i16", DAST.NewtypeRange.create_I16()), + NativeType.Selection.UShort => CreateNewtype("u16", DAST.NewtypeRange.create_U16()), + NativeType.Selection.Int => CreateNewtype("i32", DAST.NewtypeRange.create_I32()), + NativeType.Selection.UInt => CreateNewtype("u32", DAST.NewtypeRange.create_U32()), + NativeType.Selection.Long => CreateNewtype("i64", DAST.NewtypeRange.create_I64()), + NativeType.Selection.ULong => CreateNewtype("u64", DAST.NewtypeRange.create_U64()), + NativeType.Selection.DoubleLong => CreateNewtype("i128", DAST.NewtypeRange.create_I128()), + NativeType.Selection.UDoubleLong => CreateNewtype("u128", DAST.NewtypeRange.create_U128()), _ => throw new InvalidOperationException(), }); } else if (xType is SeqType seq) { @@ -832,10 +865,10 @@ protected override void EmitNameAndActualTypeArgs(string protectedName, List.UnicodeFromString(protectedName), receiverType, receiverArg, signature)); + callExpr.SetName((DAST.CallName)DAST.CallName.create_CallName(Sequence.UnicodeFromString(protectedName), receiverType, receiverArg, receiverAsArgument, signature)); } else if (GetExprBuilder(wr, out var st2) && st2.Builder is CallStmtBuilder callStmt) { var signature = callStmt.Signature; - callStmt.SetName((DAST.CallName)DAST.CallName.create_CallName(Sequence.UnicodeFromString(protectedName), receiverType, receiverArg, signature)); + callStmt.SetName((DAST.CallName)DAST.CallName.create_CallName(Sequence.UnicodeFromString(protectedName), receiverType, receiverArg, receiverAsArgument, signature)); } else { AddUnsupported("Builder issue: wr is as " + wr.GetType() + (GetExprBuilder(wr, out var st3) ? @@ -889,7 +922,7 @@ protected override void DeclareLocalVar(string name, Type type, IToken tok, bool var rhsValue = bufferedInitializationValue; bufferedInitializationValue = null; - if (bufferedInitializationStmts.is_Some) { + if (bufferedInitializationStmts is { is_Some: true }) { foreach (var stmt in bufferedInitializationStmts.dtor_value) { stmtContainer.Builder.AddStatement(stmt); } @@ -957,6 +990,19 @@ public override bool NeedsCustomReceiverNotTrait(MemberDecl member) { return member is Constructor || base.NeedsCustomReceiverNotTrait(member); } + protected override void EmitStaticExternMethodQualifier(string qual, ConcreteSyntaxTree wr) { + if (GetExprBuilder(wr, out var builder)) { + builder.Builder.AddExpr((DAST.Expression)DAST.Expression.create_ExternCompanion( + Sequence>.FromArray(new[] { + DCOMP.COMP.DAFNY__EXTERN__MODULE, + Sequence.UnicodeFromString(qual) + }) + )); + } else { + throw new InvalidOperationException(); + } + } + protected override void EmitCallToInheritedMethod(Method method, [CanBeNull] TopLevelDeclWithMembers heir, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts, ConcreteSyntaxTree wStmtsAfterCall) { if (wr is BuilderSyntaxTree stmtContainer) { var callBuilder = stmtContainer.Builder.Call(GenFormals(method.Ins)); @@ -972,8 +1018,13 @@ protected override void EmitMultiReturnTuple(List outs, List outTy protected override void CompileFunctionCallExpr(FunctionCallExpr e, ConcreteSyntaxTree wr, bool inLetExprBody, ConcreteSyntaxTree wStmts, FCE_Arg_Translator tr, bool alreadyCoerced) { - var toType = thisContext == null ? e.Type : e.Type.Subst(thisContext.ParentFormalTypeParametersToActuals); - wr = EmitCoercionIfNecessary(e.Function.Original.ResultType, toType, e.tok, wr); + var toType = e.Type.Subst(e.GetTypeArgumentSubstitutions()); + var fromType = e.Function.Original.ResultType.Subst(e.GetTypeArgumentSubstitutions()); + if (thisContext != null) { + toType = toType.Subst(thisContext.ParentFormalTypeParametersToActuals); + fromType = fromType.Subst(thisContext.ParentFormalTypeParametersToActuals); + } + wr = EmitCoercionIfNecessary(fromType, toType, e.tok, wr); if (wr is BuilderSyntaxTree builder) { var callBuilder = builder.Builder.Call(GenFormals(e.Function.Ins)); @@ -1214,16 +1265,21 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde start, goingUp )); - TrStmtList(body, new BuilderSyntaxTree(foreachBuilder, this)); + ConcreteSyntaxTree bodyWr = new BuilderSyntaxTree(foreachBuilder, this); + bodyWr = EmitContinueLabel(labels, bodyWr); + TrStmtList(body, bodyWr); return new BuilderSyntaxTree(startBuilder, this); } else { var loHiBuilder = ((ExprContainer)foreachBuilder).BinOp("int_range", (DAST.Expression lo, DAST.Expression hi) => (DAST.Expression)DAST.Expression.create_IntRange( + GenType(loopIndex.Type), lo, hi, goingUp )); - TrStmtList(body, new BuilderSyntaxTree(foreachBuilder, this)); + ConcreteSyntaxTree bodyWr = new BuilderSyntaxTree(foreachBuilder, this); + bodyWr = EmitContinueLabel(labels, bodyWr); + TrStmtList(body, bodyWr); BuilderSyntaxTree toReturn; if (goingUp) { var loBuf = new ExprBuffer(null); @@ -1349,6 +1405,10 @@ protected override void EmitNew(Type type, IToken tok, CallStmt initCall, Concre }); } + if (ctor == null) { + AddUnsupported("Creation of object of type " + type.ToString() + " requires a constructor"); + } + var typeArgs = type.TypeArgs.Select(GenType).ToArray(); builder.Builder.AddExpr((DAST.Expression)DAST.Expression.create_New( @@ -1389,6 +1449,28 @@ protected override void EmitIdentifier(string ident, ConcreteSyntaxTree wr) { } } + // Overriden from SinglePassCodeGenerator to return a BuilderSyntaxTree + // To avoid UnsupportedInvalidOperationException in EmitIdentifier by way of set comprehension (github issue 5644) + protected override ConcreteSyntaxTree MaybeEmitCallToIsMethod(RedirectingTypeDecl declWithConstraints, List typeArguments, ConcreteSyntaxTree wr) { + Contract.Requires(declWithConstraints is SubsetTypeDecl or NewtypeDecl); + Contract.Requires(declWithConstraints.TypeArgs.Count == typeArguments.Count); + Contract.Requires(declWithConstraints.ConstraintIsCompilable); + switch (declWithConstraints) { + case NonNullTypeDecl: + // Non-null types don't have a special target class, so we just do the non-null constraint check here. + return EmitNullTest(false, wr); + case NewtypeDecl { TargetTypeCoversAllBitPatterns: true }: { + EmitLiteralExpr(wr, Expression.CreateBoolLiteral(declWithConstraints.tok, true)); + return new BuilderSyntaxTree(new ExprBuffer(null), this); + } + default: { + // in mind that type parameters are not accessible in static methods in some target languages). + var type = UserDefinedType.FromTopLevelDecl(declWithConstraints.tok, (TopLevelDecl)declWithConstraints, typeArguments); + return EmitCallToIsMethod(declWithConstraints, type, wr); + } + } + } + protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) { if (GetExprBuilder(wr, out var builder)) { DAST.Expression baseExpr; @@ -1640,7 +1722,7 @@ private DAST.Type TypeNameASTFromTopLevel(TopLevelDecl topLevel, List type GenType(EraseNewtypeLayers(topLevel)), range, true); } else if (topLevel is TypeSynonymDecl typeSynonym) { // Also SubsetTypeDecl resolvedTypeBase = (DAST.ResolvedTypeBase)DAST.ResolvedTypeBase.create_Newtype( - GenType(typeSynonym.Rhs.NormalizeExpand()), NewtypeRange.create_NoRange(), true); + GenType(typeSynonym.Rhs.Subst(typeSynonym.TypeArgs.Zip(typeArgs).ToDictionary(kv => kv.Item1, kv => kv.Item2)).NormalizeExpand()), NewtypeRange.create_NoRange(), true); } else if (topLevel is TraitDecl) { resolvedTypeBase = (DAST.ResolvedTypeBase)DAST.ResolvedTypeBase.create_Trait(); } else if (topLevel is DatatypeDecl dd) { @@ -1803,6 +1885,8 @@ protected override void GetSpecialFieldInfo(SpecialField.ID id, object idParam, break; case SpecialField.ID.Values: break; + case SpecialField.ID.Items: + break; default: AddUnsupported("Special field: " + id + ""); break; @@ -1868,6 +1952,11 @@ protected override ILvalue EmitMemberSelect(Action obj, Type var objExpr = objReceiver.Finish(); return new ExprLvalue((DAST.Expression)DAST.Expression.create_MapValues( objExpr), null, this); + } else if (member is SpecialField { SpecialId: SpecialField.ID.Items }) { + obj(new BuilderSyntaxTree(objReceiver, this)); + var objExpr = objReceiver.Finish(); + return new ExprLvalue((DAST.Expression)DAST.Expression.create_MapItems( + objExpr), null, this); } else if (member is SpecialField sf && sf.SpecialId != SpecialField.ID.UseIdParam) { obj(new BuilderSyntaxTree(objReceiver, this)); var objExpr = objReceiver.Finish(); @@ -1901,7 +1990,8 @@ protected override ILvalue EmitMemberSelect(Action obj, Type Sequence.UnicodeFromString(member.GetCompileName(Options)), member.EnclosingClass is DatatypeDecl, member.IsStatic, - expectedType.AsArrowType.Arity + member.IsInstanceIndependentConstant, + Sequence.FromElements(expectedType.AsArrowType.Args.Select(GenType).ToArray()) ), null, this); } else if (internalAccess && (member is ConstantField || member.EnclosingClass is TraitDecl)) { return new ExprLvalue((DAST.Expression)DAST.Expression.create_Select( @@ -2238,12 +2328,28 @@ protected override ConcreteSyntaxTree EmitCallToIsMethod(RedirectingTypeDecl dec throw new InvalidOperationException(); } + if (declWithConstraints is SubsetTypeDecl subsetTypeDecl) { + // Since this type becomes a type synonym at run-time, we simply inline the condition + // We put it as a IIFE + var constraint = subsetTypeDecl.Constraint; + + var statementBuf = new NoStatementBuffer(); + ConcreteSyntaxTree sNoStmt = new BuilderSyntaxTree(statementBuf, this); + CreateIIFE(GetCompileNameNotProtected(subsetTypeDecl.Var), subsetTypeDecl.Var.Type, subsetTypeDecl.Var.tok, + Type.Bool, constraint.tok, wr, ref sNoStmt, out ConcreteSyntaxTree wrRhs, out ConcreteSyntaxTree wrBody); + if (!GetExprBuilder(wrBody, out var wrBodyBuilder)) { + throw new InvalidOperationException(); + } + wrBodyBuilder.Builder.AddExpr(ConvertExpression(constraint, sNoStmt)); + return wrRhs; + } + var signature = Sequence<_IFormal>.FromArray(new[] { new DAST.Formal(Sequence.UnicodeFromString("_dummy_"), GenType(type), Sequence.Empty) }); var c = builder.Builder.Call(signature); c.SetName((DAST.CallName)DAST.CallName.create_CallName(Sequence.UnicodeFromString("is"), - Option<_IType>.create_None(), Option<_IFormal>.create_None(), signature)); + Option<_IType>.create_None(), Option<_IFormal>.create_None(), false, signature)); var wrc = new BuilderSyntaxTree(c, this); EmitTypeName_Companion(type, wrc, wr, declWithConstraints.tok, null); @@ -2700,7 +2806,15 @@ protected override void EmitConstructorCheck(string source, DatatypeCtor ctor, C } protected override void EmitTypeTest(string localName, Type fromType, Type toType, IToken tok, ConcreteSyntaxTree wr) { - AddUnsupportedFeature(tok, Feature.TypeTests); + if (GetExprBuilder(wr, out var builder)) { + builder.Builder.AddExpr((DAST.Expression)DAST.Expression.create_Is( + DAST.Expression.create_Ident(Sequence.UnicodeFromString(localName)), + GenType(fromType), + GenType(toType) + )); + } else { + throw new InvalidOperationException(); + } } protected override void EmitIsIntegerTest(Expression source, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { @@ -2947,6 +3061,7 @@ protected override (Type, Action) EmitIntegerRange(Type type if (GetExprBuilder(wr, out var builder)) { builder.Builder.AddExpr((DAST.Expression)DAST.Expression.create_IntRange( + GenType(result), loBuf.Finish(), hiBuf.Finish(), true @@ -2967,6 +3082,12 @@ protected override void EmitSingleValueGenerator(Expression e, bool inLetExprBod AddUnsupportedFeature(e.Tok, Feature.ExactBoundedPool); } + protected override void OrganizeModules(Program program, out List modules) { + modules = program.CompileModules.ToList(); + modules.Sort((a, b) => + String.Compare(a.FullDafnyName, b.FullDafnyName, StringComparison.Ordinal)); + } + protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody, ConcreteSyntaxTree wr) { TrStmt(body, wr); } diff --git a/Source/DafnyCore/Backends/DafnyExecutableBackend.cs b/Source/DafnyCore/Backends/DafnyExecutableBackend.cs index 19ed5bf777e..b3d74485093 100644 --- a/Source/DafnyCore/Backends/DafnyExecutableBackend.cs +++ b/Source/DafnyCore/Backends/DafnyExecutableBackend.cs @@ -1,4 +1,7 @@ +using System.Collections.Generic; using System.Collections.ObjectModel; +using System.IO; +using System.Linq; using Dafny; namespace Microsoft.Dafny.Compilers; @@ -7,11 +10,14 @@ public abstract class DafnyExecutableBackend : ExecutableBackend { protected virtual bool PreventShadowing => true; protected virtual bool CanEmitUncompilableCode => true; + public override bool SupportsDatatypeWrapperErasure => false; protected virtual string InternalFieldPrefix => "_i_"; protected DafnyWrittenCodeGenerator DafnyCodeGenerator; + public List ImportedFiles = new(); + protected DafnyExecutableBackend(DafnyOptions options) : base(options) { } @@ -27,6 +33,20 @@ public override void OnPreCompile(ErrorReporter reporter, ReadOnlyCollection ImportFilesMapping(string dafnyProgramName) { + Dictionary importedFilesMapping = new(); + return importedFilesMapping; + } + + public IEnumerable ImportFiles(string dafnyProgramName) { + var result = ImportFilesMapping(dafnyProgramName).Values.ToList(); + result.Sort(); + return result; + } + public override void Compile(Program dafnyProgram, string dafnyProgramName, ConcreteSyntaxTree output) { ProcessTranslationRecords(dafnyProgram, dafnyProgramName, output); CheckInstantiationReplaceableModules(dafnyProgram); @@ -35,7 +55,12 @@ public override void Compile(Program dafnyProgram, string dafnyProgramName, Conc ((DafnyCodeGenerator)codeGenerator).Start(); codeGenerator.Compile(dafnyProgram, new ConcreteSyntaxTree()); var dast = ((DafnyCodeGenerator)codeGenerator).Build(); - var o = DafnyCodeGenerator.Compile((Sequence)Sequence.FromArray(dast.ToArray())); + var o = DafnyCodeGenerator.Compile( + (Sequence)Sequence.FromArray(dast.ToArray()), + (Sequence>)Sequence>.FromArray( + ImportFiles(dafnyProgramName).Select(fileName => + Sequence.UnicodeFromString(Path.GetFileName(fileName))).ToArray() + )); output.Write(o.ToVerbatimString(false)); } diff --git a/Source/DafnyCore/Backends/DafnyWrittenCodeGenerator.cs b/Source/DafnyCore/Backends/DafnyWrittenCodeGenerator.cs index 63c88d5d870..e2a67e13d7a 100644 --- a/Source/DafnyCore/Backends/DafnyWrittenCodeGenerator.cs +++ b/Source/DafnyCore/Backends/DafnyWrittenCodeGenerator.cs @@ -5,7 +5,7 @@ namespace Microsoft.Dafny.Compilers { public abstract class DafnyWrittenCodeGenerator { - public abstract ISequence Compile(Sequence program); + public abstract ISequence Compile(Sequence program, Sequence> otherFiles); public abstract ISequence EmitCallToMain(string fullName); diff --git a/Source/DafnyCore/Backends/GoLang/GoBackend.cs b/Source/DafnyCore/Backends/GoLang/GoBackend.cs index 2772a36b90a..7ef9f0dedff 100644 --- a/Source/DafnyCore/Backends/GoLang/GoBackend.cs +++ b/Source/DafnyCore/Backends/GoLang/GoBackend.cs @@ -40,9 +40,7 @@ public override string TargetBaseDir(string dafnyProgramName) { public override IEnumerable> SupportedOptions => new List> { GoModuleNameCliOption }; static GoBackend() { - TranslationRecord.RegisterLibraryChecks(new Dictionary { - { GoModuleNameCliOption, OptionCompatibility.NoOpOptionCheck } - }); + OptionRegistry.RegisterOption(GoModuleNameCliOption, OptionScope.Translation); } protected override SinglePassCodeGenerator CreateCodeGenerator() { diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index dd5b3574d6b..55ddecdc1e5 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -1593,11 +1593,11 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, var t = (BitvectorType)xType; return t.NativeType != null ? GetNativeTypeName(t.NativeType) : "_dafny.BV"; } else if (xType.AsNewtype != null && member == null) { // when member is given, use UserDefinedType case below - NativeType nativeType = xType.AsNewtype.NativeType; - if (nativeType != null) { + var newtypeDecl = xType.AsNewtype; + if (newtypeDecl.NativeType is { } nativeType) { return GetNativeTypeName(nativeType); } - return TypeName(xType.AsNewtype.BaseType, wr, tok); + return TypeName(newtypeDecl.ConcreteBaseType(xType.TypeArgs), wr, tok); } else if (xType.IsObjectQ) { return AnyType; } else if (xType.IsArrayType) { @@ -1652,7 +1652,7 @@ string nil() { return "false"; } else if (xType is CharType) { return $"{CharTypeName}({CharType.DefaultValueAsString})"; - } else if (xType is IntType || xType is BigOrdinalType) { + } else if (xType is IntType or BigOrdinalType) { return "_dafny.Zero"; } else if (xType is RealType) { return "_dafny.ZeroReal"; @@ -1696,7 +1696,7 @@ string nil() { } else if (td.NativeType != null) { return GetNativeTypeName(td.NativeType) + "(0)"; } else { - return TypeInitializationValue(td.BaseType, wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); + return TypeInitializationValue(td.ConcreteBaseType(udt.TypeArgs), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors); } } else if (cl is SubsetTypeDecl) { var td = (SubsetTypeDecl)cl; @@ -3915,9 +3915,7 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type/*?*/ from, Ty return w; } } else if (from.AsNewtype is { } fromNewtypeDecl) { - var subst = TypeParameter.SubstitutionMap(fromNewtypeDecl.TypeArgs, from.TypeArgs); - from = fromNewtypeDecl.BaseType.Subst(subst); - return EmitCoercionIfNecessary(from, to, tok, wr, toOrig); + return EmitCoercionIfNecessary(fromNewtypeDecl.ConcreteBaseType(from.TypeArgs), to, tok, wr, toOrig); } else { // It's unclear to me whether it's possible to hit this case with a valid Dafny program, // so I'm not using UnsupportedFeatureError for now. diff --git a/Source/DafnyCore/Backends/Java/JavaBackend.cs b/Source/DafnyCore/Backends/Java/JavaBackend.cs index f0de140c466..a0dd281c25d 100644 --- a/Source/DafnyCore/Backends/Java/JavaBackend.cs +++ b/Source/DafnyCore/Backends/Java/JavaBackend.cs @@ -37,7 +37,7 @@ public override string TargetBaseDir(string dafnyProgramName) => }; static JavaBackend() { DafnyOptions.RegisterLegacyUi(LegacyDataConstructors, DafnyOptions.ParseBoolean, "Compilation options", legacyName: "legacyDataConstructors", defaultValue: false); - DooFile.RegisterNoChecksNeeded(LegacyDataConstructors, false); + OptionRegistry.RegisterOption(LegacyDataConstructors, OptionScope.Cli); } public override IEnumerable