From 0b629eae7a518d5b735a0f34519dcb85ad5fb996 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Mon, 29 Apr 2024 16:53:15 -0500 Subject: [PATCH] Feat rust operators (#5380) This PR is a replay of https://github.com/dafny-lang/dafny/pull/5081 after fixing the issue with the paths too long for Windows, so it should no longer break the CI. ### Description This PR implements most immutable types in Dafny (Sequence, Set, Multiset, Map) and implements most if not all operators on them. It also sets an architecture that can now be relied on. List of features in this PR: - More comprehensive Rust AST, precedence and associativity to render parentheses - The Rust compiler no longer crash when not in /runAllTests, but emits invalid code. It makes it possible to see which features are missing by searching for `` in the generated code. - Made verification of GenExpr less brittle - Previous PR review comments - Ability to use shadowed identifiers to avoid numbers in names. Rust has the same rules as Dafny for shadowing, and I will continue to monitor cases where semantics might differ. ### How has this been tested? I added an integration test for compiling Dafny to Rust, and I added unit tests for the runtime in Rust *All tests for each compiler now have a `.rs.check` if they fail.*. By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --------- Co-authored-by: Robin Salkeld --- .github/workflows/msbuild.yml | 2 +- .pre-commit-config.yaml | 2 +- Makefile | 4 +- Source/DafnyCore.Test/GeneratedDafnyTest.cs | 11 + ...afnyToRustCompilerCoverage_RASTCoverage.cs | 162 + .../AST/Expressions/Variables/IVariable.cs | 4 + .../Variables/IVariableContracts.cs | 7 + .../Variables/NonglobalVariable.cs | 7 +- .../Statements/Assignment/LocalVariable.cs | 8 +- .../AST/TypeDeclarations/NewtypeDecl.cs | 2 +- .../Backends/CSharp/CsharpCodeGenerator.cs | 7 +- .../Backends/Cplusplus/CppCodeGenerator.cs | 5 +- Source/DafnyCore/Backends/Dafny/AST.dfy | 68 +- Source/DafnyCore/Backends/Dafny/ASTBuilder.cs | 241 +- .../Backends/Dafny/BuilderSyntaxTree.cs | 12 +- .../Backends/Dafny/DafnyCodeGenerator.cs | 1062 +- .../Backends/DafnyExecutableBackend.cs | 5 +- .../Backends/GoLang/GoCodeGenerator.cs | 7 +- .../Backends/Java/JavaCodeGenerator.cs | 7 +- .../JavaScript/JavaScriptCodeGenerator.cs | 5 +- .../Backends/Library/LibraryBackend.cs | 3 + .../Backends/Python/PythonCodeGenerator.cs | 5 +- ...ResolvedDesugaredExecutableDafnyBackend.cs | 2 +- .../Rust/Dafny-compiler-rust-coverage.dfy | 200 + .../Rust/Dafny-compiler-rust-proofs.dfy | 233 +- .../Backends/Rust/Dafny-compiler-rust.dfy | 2782 +- Source/DafnyCore/Backends/Rust/RustBackend.cs | 4 + .../Backends/Rust/RustCodeGenerator.cs | 4 +- .../Backends/SinglePassCodeGenerator.cs | 22 +- Source/DafnyCore/DafnyGeneratedFromDafny.sh | 24 +- .../DafnyCore/DafnyGeneratedFromDafnyPost.py | 68 + Source/DafnyCore/DafnyMain.cs | 3 + Source/DafnyCore/DafnyOptions.cs | 9 + Source/DafnyCore/Feature.cs | 16 + Source/DafnyCore/GeneratedFromDafny.cs | 21419 ---------------- .../GeneratedFromDafny/D2DPrettyPrinter.cs | 23 + Source/DafnyCore/GeneratedFromDafny/DAST.cs | 6876 +++++ .../GeneratedFromDafny/DAST_Format.cs | 218 + Source/DafnyCore/GeneratedFromDafny/DCOMP.cs | 11602 +++++++++ .../GeneratedFromDafny/Formatting.cs | 46 + Source/DafnyCore/GeneratedFromDafny/RAST.cs | 6390 +++++ .../ResolvedDesugaredExecutableDafnyPlugin.cs | 33 + .../GeneratedFromDafny/Std_Arithmetic.cs | 14 + .../Std_Arithmetic_DivInternals.cs | 46 + .../Std_Arithmetic_DivInternalsNonlinear.cs | 14 + .../Std_Arithmetic_DivMod.cs | 20 + .../Std_Arithmetic_GeneralInternals.cs | 14 + .../Std_Arithmetic_Logarithm.cs | 31 + .../Std_Arithmetic_ModInternals.cs | 35 + .../Std_Arithmetic_ModInternalsNonlinear.cs | 14 + .../GeneratedFromDafny/Std_Arithmetic_Mul.cs | 14 + .../Std_Arithmetic_MulInternals.cs | 39 + .../Std_Arithmetic_MulInternalsNonlinear.cs | 14 + .../Std_Arithmetic_Power.cs | 31 + .../Std_Arithmetic_Power2.cs | 19 + .../GeneratedFromDafny/Std_Collections_Seq.cs | 422 + .../DafnyCore/GeneratedFromDafny/Std_Math.cs | 47 + .../GeneratedFromDafny/Std_Strings.cs | 44 + .../Std_Strings_CharStrEscaping.cs | 68 + .../Std_Strings_DecimalConversion.cs | 195 + .../Std_Strings_HexConversion.cs | 195 + .../GeneratedFromDafny/Std_Wrappers.cs | 529 + Source/DafnyCore/Makefile | 8 +- Source/DafnyCore/Options/CommonOptionBag.cs | 6 + Source/DafnyCore/Options/DafnyCommands.cs | 1 + Source/DafnyCore/Resolver/ModuleResolver.cs | 2 + Source/DafnyDriver/DafnyCliTests.cs | 11 +- Source/DafnyRuntime.Tests/TupleTest.cs | 448 + .../DafnyRuntime/DafnyRuntimeRust/src/lib.rs | 1915 +- .../DafnyRuntimeRust/src/tests/mod.rs | 197 + .../TestFiles/LitTests/LitTest/README.md | 15 +- .../VSComp2010/Problem4-Queens.dfy.rs.check | 1 + .../VerifyThis2015/Problem1.dfy.rs.check | 1 + .../VerifyThis2015/Problem2.dfy.rs.check | 1 + .../VerifyThis2015/Problem3.dfy.rs.check | 1 + .../LitTests/LitTest/c++/arrays.dfy.rs.check | 1 + .../LitTest/c++/bit-vectors.dfy.rs.check | 1 + .../LitTests/LitTest/c++/class.dfy.rs.check | 1 + .../LitTests/LitTest/c++/const.dfy.rs.check | 1 + .../LitTest/c++/datatypes.dfy.rs.check | 1 + .../LitTests/LitTest/c++/generic.dfy.rs.check | 1 + .../LitTests/LitTest/c++/maps.dfy.rs.check | 1 + .../LitTest/c++/recursion.dfy.rs.check | 1 + .../LitTests/LitTest/c++/seqs.dfy.rs.check | 1 + .../LitTests/LitTest/c++/sets.dfy.rs.check | 1 + .../LitTests/LitTest/comp/Arrays.dfy.rs.check | 1 + .../comp/AsIs-Compile-Expanded.dfy.rs.check | 1 + .../LitTest/comp/AsIs-Compile.dfy.rs.check | 1 + .../LitTest/comp/AutoInit.dfy.rs.check | 1 + .../LitTest/comp/BuiltIns.dfy.rs.check | 1 + .../comp/BuiltIns_Unsupported.dfy.rs.check | 1 + .../comp/ByMethodCompilation.dfy.rs.check | 1 + .../LitTests/LitTest/comp/Calls.dfy.rs.check | 1 + .../LitTests/LitTest/comp/Class.dfy.rs.check | 1 + .../LitTest/comp/Collections.dfy.rs.check | 1 + .../LitTest/comp/Comprehensions.dfy.rs.check | 1 + .../comp/ComprehensionsNewSyntax.dfy.rs.check | 1 + .../comp/CovariantCollections.dfy.rs.check | 1 + .../LitTest/comp/Datatype.dfy.rs.check | 1 + .../DefaultParameters-Compile.dfy.rs.check | 1 + .../LitTest/comp/DowncastClone.dfy.rs.check | 1 + .../comp/DuplicateArrowNames.dfy.rs.check | 1 + .../comp/ErasableTypeWrappers.dfy.rs.check | 1 + .../comp/EuclideanDivision.dfy.rs.check | 2 + .../comp/ForLoops-Compilation.dfy.rs.check | 1 + .../LitTests/LitTest/comp/Forall.dfy.rs.check | 1 + .../LitTest/comp/ForallNewSyntax.dfy.rs.check | 1 + .../LitTest/comp/GeneralNewtypes.dfy.rs.check | 1 + .../LitTest/comp/Iterators.dfy.rs.check | 1 + .../LitTests/LitTest/comp/Let.dfy.rs.check | 1 + .../LitTest/comp/MoreAutoInit.dfy.rs.check | 1 + .../LitTest/comp/NativeNumbers.dfy.rs.check | 1 + .../LitTest/comp/NestedArrays.dfy.rs.check | 1 + .../LitTest/comp/Numbers.dfy.rs.check | 1 + .../LitTests/LitTest/comp/Poly.dfy.rs.check | 1 + .../StaticMembersOfGenericTypes.dfy.rs.check | 1 + .../LitTest/comp/TailRecursion.dfy.rs.check | 1 + .../LitTest/comp/TypeDescriptors.dfy.rs.check | 1 + .../LitTest/comp/TypeParams.dfy.rs.check | 1 + .../LitTest/comp/UnicodeStrings.dfy.rs.check | 1 + .../LitTest/comp/Uninitialized.dfy.rs.check | 1 + ...optimizedErasableTypeWrappers.dfy.rs.check | 1 + .../LitTest/comp/Variance.dfy.rs.check | 1 + .../LitTest/comp/Various.dfy.rs.check | 1 + .../comp/firstSteps/1_Calls-F.dfy.rs.check | 1 + .../comp/firstSteps/2_Modules.dfy.rs.check | 1 + .../comp/firstSteps/3_Calls-As.dfy.rs.check | 1 + ...alls-FunctionsValues-Class+NT.dfy.rs.check | 1 + .../5_Calls-FunctionsValues-Dt.dfy.rs.check | 1 + .../6_Calls-VariableCapture.dfy.rs.check | 1 + .../comp/firstSteps/7_Arrays.dfy.rs.check | 1 + .../firstSteps/7_Dt_Algebraic.dfy.rs.check | 1 + .../replaceableHappyflow.dfy.rs.check | 1 + .../LitTests/LitTest/comp/rust/operators.dfy | 317 + .../LitTest/comp/rust/operators.dfy.expect | 12 + .../ArrayElementInitCompile.dfy.rs.check | 1 + .../LitTest/dafny0/Bitvectors.dfy.rs.check | 1 + .../LitTest/dafny0/Constant.dfy.rs.check | 1 + .../dafny0/DiscoverBounds.dfy.rs.check | 1 + .../dafny0/DividedConstructors.dfy.rs.check | 1 + .../dafny0/EqualityTypesCompile.dfy.rs.check | 1 + .../ForallCompilationNewSyntax.dfy.rs.check | 1 + .../GeneralNewtypeCollections.dfy.rs.check | 1 + .../dafny0/GhostITECompilation.dfy.rs.check | 1 + .../LitTest/dafny0/InitialValues.dfy.rs.check | 1 + .../LitTest/dafny0/MatchBraces.dfy.rs.check | 1 + .../dafny0/MoForallCompilation.dfy.rs.check | 1 + .../dafny0/NameclashesCompile.dfy.rs.check | 1 + .../NonZeroInitializationCompile.dfy.rs.check | 1 + .../NullComparisonWarnings.dfy.rs.check | 1 + .../dafny0/RangeCompilation.dfy.rs.check | 1 + .../dafny0/RuntimeTypeTests0.dfy.rs.check | 1 + .../LitTest/dafny0/SeqFromArray.dfy.rs.check | 1 + .../SharedDestructorsCompile.dfy.rs.check | 1 + .../dafny0/SiblingImports.dfy.rs.check | 1 + .../LitTest/dafny0/Strings.dfy.rs.check | 1 + .../TypeConversionsCompile.dfy.rs.check | 1 + .../LitTest/dafny0/TypeMembers.dfy.rs.check | 1 + .../LitTest/dafny0/Wellfounded.dfy.rs.check | 1 + .../LitTest/dafny2/MinWindowMax.dfy.rs.check | 1 + ...llestMissingNumber-functional.dfy.rs.check | 1 + ...llestMissingNumber-imperative.dfy.rs.check | 1 + .../dafny2/StoreAndRetrieve.dfy.rs.check | 1 + .../pq-intrinsic-extrinsic.dfy.rs.check | 1 + .../LitTest/dafny3/Abstemious.dfy.rs.check | 1 + .../dafny3/CachedContainer.dfy.rs.check | 1 + .../LitTests/LitTest/dafny3/Iter.dfy.rs.check | 1 + .../LitTest/dafny4/Ackermann.dfy.rs.check | 1 + .../LitTest/dafny4/Bug107.dfy.rs.check | 1 + .../LitTest/dafny4/Bug108.dfy.rs.check | 1 + .../LitTest/dafny4/Bug116.dfy.rs.check | 1 + .../LitTest/dafny4/Bug140.dfy.rs.check | 1 + .../LitTest/dafny4/Bug148.dfy.rs.check | 1 + .../LitTest/dafny4/Bug49.dfy.rs.check | 1 + .../LitTest/dafny4/Bug60.dfy.rs.check | 1 + .../LitTest/dafny4/Bug67.dfy.rs.check | 1 + .../LitTest/dafny4/Bug68.dfy.rs.check | 1 + .../LitTest/dafny4/Bug94.dfy.rs.check | 1 + .../dafny4/ClassRefinement.dfy.rs.check | 1 + .../dafny4/ExpandedGuardedness.dfy.rs.check | 1 + .../LitTest/dafny4/FlyingRobots.dfy.rs.check | 1 + .../LitTest/dafny4/McCarthy91.dfy.rs.check | 1 + .../LitTest/dafny4/NatList.dfy.rs.check | 1 + .../LitTest/dafny4/Regression2.dfy.rs.check | 1 + .../LitTest/dafny4/Regression3.dfy.rs.check | 1 + .../LitTest/dafny4/Regression4.dfy.rs.check | 1 + .../LitTest/dafny4/Regression6.dfy.rs.check | 1 + .../LitTest/dafny4/Regression7.dfy.rs.check | 1 + .../LitTest/dafny4/Regression9.dfy.rs.check | 1 + .../LitTest/dafny4/UnionFind.dfy.rs.check | 1 + .../LitTests/LitTest/dafny4/gcd.dfy.rs.check | 1 + .../LitTest/dafny4/git-issue104.dfy.rs.check | 1 + .../LitTest/dafny4/git-issue15.dfy.rs.check | 1 + .../LitTest/dafny4/git-issue195.dfy.rs.check | 1 + .../LitTest/dafny4/git-issue196.dfy.rs.check | 1 + .../LitTest/dafny4/git-issue4.dfy.rs.check | 1 + .../LitTest/dafny4/git-issue76.dfy.rs.check | 1 + .../LitTest/dafny4/git-issue88.dfy.rs.check | 1 + .../exceptions/Exceptions1.dfy.rs.check | 1 + .../Exceptions1Expressions.dfy.rs.check | 1 + .../LitTest/exports/FIFO.dfy.rs.check | 1 + .../LitTest/exports/LIFO.dfy.rs.check | 1 + .../LitTest/exports/xrefine2.dfy.rs.check | 1 + .../LitTest/exports/xrefine3.dfy.rs.check | 1 + .../LitTests/LitTest/ghost/Comp.dfy.rs.check | 1 + .../git-issues/git-issue-1029.dfy.rs.check | 1 + .../git-issues/git-issue-1093.dfy.rs.check | 1 + .../git-issues/git-issue-1150.dfy.rs.check | 1 + .../git-issues/git-issue-1185.dfy.rs.check | 1 + .../git-issues/git-issue-1514.dfy.rs.check | 1 + .../git-issues/git-issue-1514b.dfy.rs.check | 1 + .../git-issues/git-issue-1514c.dfy.rs.check | 1 + .../git-issues/git-issue-1553.dfy.rs.check | 1 + .../git-issues/git-issue-1604.dfy.rs.check | 1 + .../git-issues/git-issue-1604b.dfy.rs.check | 1 + .../git-issues/git-issue-1607.dfy.rs.check | 1 + .../git-issues/git-issue-1714.dfy.rs.check | 1 + .../git-issues/git-issue-1815a.dfy.rs.check | 1 + .../git-issues/git-issue-1815b.dfy.rs.check | 1 + .../git-issues/git-issue-1852.dfy.rs.check | 1 + .../git-issues/git-issue-1903.dfy.rs.check | 1 + .../git-issues/git-issue-1909.dfy.rs.check | 1 + .../git-issues/git-issue-2013.dfy.rs.check | 1 + .../git-issues/git-issue-2103.dfy.rs.check | 1 + .../git-issues/git-issue-2173.dfy.rs.check | 1 + .../git-issues/git-issue-2510.dfy.rs.check | 1 + .../git-issues/git-issue-258.dfy.rs.check | 1 + .../git-issues/git-issue-2581.dfy.rs.check | 1 + .../git-issues/git-issue-261.dfy.rs.check | 1 + .../git-issues/git-issue-262.dfy.rs.check | 1 + .../git-issues/git-issue-2672.dfy.rs.check | 1 + .../git-issues/git-issue-2708.dfy.rs.check | 1 + .../git-issues/git-issue-2726a.dfy.rs.check | 1 + .../git-issues/git-issue-2792.dfy.rs.check | 1 + .../git-issues/git-issue-283.dfy.rs.check | 1 + .../git-issues/git-issue-283f.dfy.rs.check | 1 + .../git-issues/git-issue-354.dfy.rs.check | 1 + .../git-issues/git-issue-356.dfy.rs.check | 1 + .../git-issues/git-issue-364.dfy.rs.check | 1 + .../git-issues/git-issue-3734.dfy.rs.check | 1 + .../git-issues/git-issue-3868.dfy.rs.check | 1 + .../git-issues/git-issue-3873.dfy.rs.check | 1 + .../git-issues/git-issue-3883.dfy.rs.check | 1 + .../git-issues/git-issue-3978.dfy.rs.check | 1 + .../git-issues/git-issue-3987.dfy.rs.check | 1 + .../git-issues/git-issue-4007.dfy.rs.check | 1 + .../git-issues/git-issue-4012.dfy.rs.check | 1 + .../git-issues/git-issue-4141.dfy.rs.check | 1 + .../git-issues/git-issue-4152.dfy.rs.check | 1 + .../git-issues/git-issue-4233.dfy.rs.check | 1 + .../git-issues/git-issue-443.dfy.rs.check | 1 + .../git-issues/git-issue-446.dfy.rs.check | 1 + .../git-issues/git-issue-446a.dfy.rs.check | 1 + .../git-issues/git-issue-446b.dfy.rs.check | 1 + .../git-issues/git-issue-452.dfy.rs.check | 1 + .../git-issues/git-issue-452c.dfy.rs.check | 1 + .../git-issues/git-issue-4939c.dfy.rs.check | 1 + .../git-issues/git-issue-506.dfy.rs.check | 1 + .../git-issues/git-issue-5065.dfy.rs.check | 1 + .../git-issues/git-issue-5092.dfy.rs.check | 1 + .../git-issues/git-issue-5238.dfy.rs.check | 1 + .../git-issues/git-issue-5285.dfy.rs.check | 1 + .../git-issues/git-issue-532.dfy.rs.check | 1 + .../git-issues/git-issue-549.dfy.rs.check | 1 + .../git-issues/git-issue-610.dfy.rs.check | 1 + .../git-issues/git-issue-674.dfy.rs.check | 1 + .../git-issues/git-issue-684.dfy.rs.check | 1 + .../git-issues/git-issue-686.dfy.rs.check | 1 + .../git-issues/git-issue-697.dfy.rs.check | 1 + .../git-issues/git-issue-697b.dfy.rs.check | 1 + .../git-issues/git-issue-697d.dfy.rs.check | 1 + .../git-issues/git-issue-697e.dfy.rs.check | 1 + .../git-issues/git-issue-697f.dfy.rs.check | 1 + .../git-issues/git-issue-697g.dfy.rs.check | 1 + .../git-issues/git-issue-697j.dfy.rs.check | 1 + .../git-issues/git-issue-697k.dfy.rs.check | 1 + .../git-issues/git-issue-698.dfy.rs.check | 1 + .../git-issues/git-issue-698b.dfy.rs.check | 1 + .../git-issues/git-issue-701.dfy.rs.check | 1 + .../git-issues/git-issue-731.dfy.rs.check | 1 + .../git-issues/git-issue-731b.dfy.rs.check | 1 + .../git-issues/git-issue-784.dfy.rs.check | 1 + .../git-issues/git-issue-817.dfy.rs.check | 1 + .../git-issues/git-issue-817a.dfy.rs.check | 1 + .../git-issues/git-issue-859.dfy.rs.check | 1 + .../git-issues/git-issue-864rr.dfy.rs.check | 1 + .../git-issues/git-issue-953.dfy.rs.check | 1 + .../git-issues/github-issue-2928.dfy.rs.check | 1 + .../github-issue-3766-a.dfy.rs.check | 1 + .../github-issue-3766-b.dfy.rs.check | 1 + .../github-issue-3766-c.dfy.rs.check | 1 + .../git-issues/github-issue-3871.dfy.rs.check | 1 + .../git-issues/github-issue-3874.dfy.rs.check | 1 + .../git-issues/github-issue-4483.dfy.rs.check | 1 + .../LitTest/hofs/Compilation.dfy.rs.check | 1 + .../LitTests/LitTest/hofs/Fold.dfy.rs.check | 1 + .../LitTest/hofs/Renaming.dfy.rs.check | 1 + .../LitTest/hofs/TreeMapSimple.dfy.rs.check | 1 + .../LitTest/hofs/VectorUpdate.dfy.rs.check | 1 + .../LitTest/hofs/WhileLoop.dfy.rs.check | 1 + .../ConsistentWhenSupported.dfy.rs.check | 1 + .../metatests/OutputEncoding.dfy.rs.check | 1 + .../LitTest/patterns/OrPatterns.dfy.rs.check | 1 + .../patterns/PatternMatching.dfy.rs.check | 1 + .../stdlibs/StandardLibraries.dfy.rs.check | 1 + .../traits/GeneralTraitsCompile.dfy.rs.check | 1 + .../NonReferenceTraitsCompile.dfy.rs.check | 1 + .../LitTest/traits/TraitCompile.dfy.rs.check | 1 + .../LitTest/traits/TraitExample.dfy.rs.check | 1 + .../LitTest/traits/Traits-Fields.dfy.rs.check | 1 + .../TraitsMultipleInheritance.dfy.rs.check | 1 + .../unicodechars/comp/Arrays.dfy.rs.check | 1 + .../comp/Collections.dfy.rs.check | 1 + .../comp/Comprehensions.dfy.rs.check | 1 + .../comp/NativeNumbers.dfy.rs.check | 1 + .../unicodechars/comp/Numbers.dfy.rs.check | 1 + .../git-issues/github-issue-2928.dfy.rs.check | 1 + .../comp/Collections.dfy.rs.check | 1 + .../comp/Comprehensions.dfy.rs.check | 1 + .../comp/NativeNumbers.dfy.rs.check | 1 + .../git-issues/github-issue-2928.dfy.rs.check | 1 + Source/TestDafny/MultiBackendTest.cs | 165 +- Source/XUnitExtensions/Lit/DiffCommand.cs | 2 +- .../XUnitExtensions/Lit/OutputCheckCommand.cs | 3 +- Source/XUnitExtensions/Lit/ShellLitCommand.cs | 9 +- docs/DafnyRef/Options.txt | 5 + .../integration- rust/IntegrationRust.md | 86 + docs/dev/news/5081.feat | 3 + 328 files changed, 33378 insertions(+), 23491 deletions(-) create mode 100644 Source/DafnyCore.Test/GeneratedDafnyTest.cs create mode 100644 Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs create mode 100644 Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-coverage.dfy create mode 100644 Source/DafnyCore/DafnyGeneratedFromDafnyPost.py delete mode 100644 Source/DafnyCore/GeneratedFromDafny.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/D2DPrettyPrinter.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/DAST.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/DAST_Format.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/DCOMP.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Formatting.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/RAST.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/ResolvedDesugaredExecutableDafnyPlugin.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternals.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternalsNonlinear.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivMod.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_GeneralInternals.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Logarithm.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_ModInternals.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_ModInternalsNonlinear.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Mul.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternals.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternalsNonlinear.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power2.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Collections_Seq.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Math.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Strings.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Strings_CharStrEscaping.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Strings_DecimalConversion.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Strings_HexConversion.cs create mode 100644 Source/DafnyCore/GeneratedFromDafny/Std_Wrappers.cs create mode 100644 Source/DafnyRuntime.Tests/TupleTest.cs create mode 100644 Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/VSComp2010/Problem4-Queens.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/VerifyThis2015/Problem1.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/VerifyThis2015/Problem2.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/VerifyThis2015/Problem3.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/arrays.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/bit-vectors.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/class.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/const.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/datatypes.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/generic.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/maps.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/recursion.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/seqs.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/sets.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Arrays.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/AsIs-Compile-Expanded.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/AsIs-Compile.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/AutoInit.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/BuiltIns.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/BuiltIns_Unsupported.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ByMethodCompilation.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Calls.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Class.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Collections.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Comprehensions.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ComprehensionsNewSyntax.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CovariantCollections.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Datatype.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/DefaultParameters-Compile.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/DowncastClone.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/DuplicateArrowNames.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ErasableTypeWrappers.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/EuclideanDivision.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ForLoops-Compilation.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Forall.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ForallNewSyntax.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/GeneralNewtypes.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Iterators.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Let.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/MoreAutoInit.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/NativeNumbers.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/NestedArrays.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Numbers.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Poly.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/StaticMembersOfGenericTypes.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/TailRecursion.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/TypeDescriptors.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/TypeParams.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/UnicodeStrings.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Uninitialized.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/UnoptimizedErasableTypeWrappers.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Variance.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Various.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/firstSteps/1_Calls-F.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/firstSteps/2_Modules.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/firstSteps/3_Calls-As.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/firstSteps/4_Calls-FunctionsValues-Class+NT.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/firstSteps/5_Calls-FunctionsValues-Dt.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/firstSteps/6_Calls-VariableCapture.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/firstSteps/7_Arrays.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/firstSteps/7_Dt_Algebraic.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/replaceableHappyflow.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/operators.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/operators.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ArrayElementInitCompile.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Bitvectors.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Constant.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DiscoverBounds.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DividedConstructors.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/EqualityTypesCompile.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilationNewSyntax.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeCollections.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GhostITECompilation.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/InitialValues.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/MatchBraces.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/MoForallCompilation.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NameclashesCompile.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NonZeroInitializationCompile.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NullComparisonWarnings.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RangeCompilation.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RuntimeTypeTests0.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SeqFromArray.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SharedDestructorsCompile.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SiblingImports.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Strings.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeConversionsCompile.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeMembers.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Wellfounded.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/MinWindowMax.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SmallestMissingNumber-functional.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SmallestMissingNumber-imperative.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/StoreAndRetrieve.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/pq-intrinsic-extrinsic.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Abstemious.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/CachedContainer.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Iter.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Ackermann.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug107.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug108.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug116.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug140.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug148.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug49.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug60.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug67.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug68.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug94.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/ClassRefinement.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/ExpandedGuardedness.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/FlyingRobots.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/McCarthy91.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/NatList.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression2.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression3.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression4.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression6.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression7.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression9.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/UnionFind.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/gcd.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue104.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue15.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue195.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue196.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue4.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue76.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue88.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/Exceptions1.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/Exceptions1Expressions.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/FIFO.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/LIFO.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/xrefine2.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/xrefine3.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ghost/Comp.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1029.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1093.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1150.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1185.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514b.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1514c.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1553.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1604.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1604b.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1607.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1714.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1815a.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1815b.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1852.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1903.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1909.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2013.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2103.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2173.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2510.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-258.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2581.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-261.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-262.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2672.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2708.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2726a.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2792.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-283.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-283f.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-354.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-356.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-364.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3734.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3868.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3873.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3883.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3978.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3987.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4007.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4012.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4141.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4152.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4233.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-443.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-446.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-446a.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-446b.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-452.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-452c.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939c.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-506.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5065.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5092.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5285.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-532.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-549.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-610.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-674.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-684.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-686.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697b.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697d.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697e.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697f.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697g.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697k.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-698.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-698b.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-701.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-731.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-731b.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-784.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-817.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-817a.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-859.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-864rr.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-953.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-2928.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-3766-a.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-3766-b.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-3766-c.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-3871.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-3874.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4483.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Compilation.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Fold.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Renaming.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/TreeMapSimple.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/VectorUpdate.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/WhileLoop.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/ConsistentWhenSupported.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/OutputEncoding.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/OrPatterns.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/PatternMatching.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/GeneralTraitsCompile.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraitsCompile.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitCompile.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitExample.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/Traits-Fields.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitsMultipleInheritance.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/Arrays.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/Collections.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/Comprehensions.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/NativeNumbers.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/Numbers.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/git-issues/github-issue-2928.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodecharsFalse/comp/Collections.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodecharsFalse/comp/Comprehensions.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodecharsFalse/comp/NativeNumbers.dfy.rs.check create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodecharsFalse/git-issues/github-issue-2928.dfy.rs.check create mode 100644 docs/DafnyRef/integration- rust/IntegrationRust.md create mode 100644 docs/dev/news/5081.feat diff --git a/.github/workflows/msbuild.yml b/.github/workflows/msbuild.yml index ee69aec54c3..41fc5b53520 100644 --- a/.github/workflows/msbuild.yml +++ b/.github/workflows/msbuild.yml @@ -37,7 +37,7 @@ jobs: run: dotnet tool restore - name: Check whitespace and style working-directory: dafny - run: dotnet format whitespace Source/Dafny.sln --verify-no-changes --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs + run: dotnet format whitespace Source/Dafny.sln --verify-no-changes --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs - name: Get Boogie Version run: | sudo apt-get update diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml index 9c4a8290fd2..daba3a64a4d 100644 --- a/.pre-commit-config.yaml +++ b/.pre-commit-config.yaml @@ -4,5 +4,5 @@ repos: - id: dotnet-format name: dotnet-format language: system - entry: dotnet format whitespace Source/Dafny.sln --include + entry: dotnet format whitespace Source/Dafny.sln -v:d --include types_or: ["c#"] diff --git a/Makefile b/Makefile index d6256e00c2e..45248b3bf74 100644 --- a/Makefile +++ b/Makefile @@ -17,7 +17,7 @@ dfyprod: dfyprodformat dfyprodinit (cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser dfydevinit: - (cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh --no-verify --no-format) + (cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh --no-verify) dfydev: dfydevinit (cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser @@ -73,7 +73,7 @@ z3-ubuntu: chmod +x ${DIR}/Binaries/z3/bin/z3-* format: - dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs + dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs clean: (cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin) diff --git a/Source/DafnyCore.Test/GeneratedDafnyTest.cs b/Source/DafnyCore.Test/GeneratedDafnyTest.cs new file mode 100644 index 00000000000..72600e6f7c6 --- /dev/null +++ b/Source/DafnyCore.Test/GeneratedDafnyTest.cs @@ -0,0 +1,11 @@ +using System.Collections.Concurrent; +using Microsoft.Dafny; + +namespace DafnyCore.Test; + +public class GeneratedDafnyTest { + [Fact] + public void TestDafnyGeneratedCode() { + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestExpr(); + } +} \ No newline at end of file diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs b/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs new file mode 100644 index 00000000000..015267d20c0 --- /dev/null +++ b/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs @@ -0,0 +1,162 @@ +// Dafny program the_program compiled into C# +// To recompile, you will need the libraries +// System.Runtime.Numerics.dll System.Collections.Immutable.dll +// but the 'dotnet' tool in net6.0 should pick those up automatically. +// Optionally, you may want to include compiler switches like +// /debug /nowarn:162,164,168,183,219,436,1717,1718 + +using System; +using System.Numerics; +using System.Collections; + +namespace DafnyToRustCompilerCoverage.RASTCoverage { + + public partial class __default { + public static void TestNoOptimize(RAST._IExpr e) + { + } + public static void TestOptimizeToString() + { + RAST._IExpr _1833_x; + _1833_x = RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")); + RAST._IExpr _1834_y; + _1834_y = RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("y")); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), RAST.Expr.create_Call(RAST.Expr.create_Select(_1833_x, Dafny.Sequence.UnicodeFromString("clone")), Dafny.Sequence.FromElements(), Dafny.Sequence.FromElements()), DAST.Format.UnaryOpFormat.create_NoFormat())).Optimize(), RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), _1833_x, DAST.Format.UnaryOpFormat.create_NoFormat()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), RAST.Expr.create_Call(RAST.Expr.create_Select(_1833_x, Dafny.Sequence.UnicodeFromString("clone")), Dafny.Sequence.FromElements(), Dafny.Sequence.FromElements(_1834_y)), DAST.Format.UnaryOpFormat.create_NoFormat())); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("=="), _1833_x, _1834_y, DAST.Format.BinaryOpFormat.create_NoFormat()), DAST.Format.UnaryOpFormat.create_CombineFormat())).Optimize(), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("!="), _1833_x, _1834_y, DAST.Format.BinaryOpFormat.create_NoFormat()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<"), _1833_x, _1834_y, DAST.Format.BinaryOpFormat.create_NoFormat()), DAST.Format.UnaryOpFormat.create_CombineFormat())).Optimize(), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">="), _1833_x, _1834_y, DAST.Format.BinaryOpFormat.create_NoFormat()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<"), _1833_x, _1834_y, DAST.Format.BinaryOpFormat.create_ReverseFormat()), DAST.Format.UnaryOpFormat.create_CombineFormat())).Optimize(), RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<="), _1834_y, _1833_x, DAST.Format.BinaryOpFormat.create_NoFormat()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_ConversionNum(RAST.Type.create_I128(), RAST.Expr.create_Call(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("")), Dafny.Sequence.UnicodeFromString("dafny_runtime")), Dafny.Sequence.UnicodeFromString("DafnyInt")), Dafny.Sequence.UnicodeFromString("from")), Dafny.Sequence.FromElements(), Dafny.Sequence.FromElements(RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("1")))))).Optimize(), RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("/*optimized*/1")))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_ConversionNum(RAST.Type.create_I128(), RAST.Expr.create_Call(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("")), Dafny.Sequence.UnicodeFromString("dafny_runtime")), Dafny.Sequence.UnicodeFromString("DafnyInt")), Dafny.Sequence.UnicodeFromString("from")), Dafny.Sequence.FromElements(), Dafny.Sequence.FromElements(RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("1"), false))))).Optimize(), RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("/*optimized*/1")))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize((RAST.Expr.create_ConversionNum(RAST.Type.create_I128(), RAST.Expr.create_Call(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("")), Dafny.Sequence.UnicodeFromString("dafny_runtime")), Dafny.Sequence.UnicodeFromString("DafnyInt")), Dafny.Sequence.UnicodeFromString("from")), Dafny.Sequence.FromElements(), Dafny.Sequence.FromElements(_1833_x)))).Optimize()); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize((RAST.Expr.create_ConversionNum(RAST.Type.create_I128(), RAST.Expr.create_Call(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("")), Dafny.Sequence.UnicodeFromString("dafny_runtime")), Dafny.Sequence.UnicodeFromString("DafnyInt")), Dafny.Sequence.UnicodeFromString("from")), Dafny.Sequence.FromElements(), Dafny.Sequence.FromElements(RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("1")), RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("2")))))).Optimize()); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_ConversionNum(RAST.Type.create_I128(), _1833_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.Expr.create_AssignVar(Dafny.Sequence.UnicodeFromString("z"), _1834_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(_1834_y)), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("return"))))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("z"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), RAST.Expr.create_StmtExpr(RAST.Expr.create_AssignVar(Dafny.Sequence.UnicodeFromString("w"), _1834_y), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("return"))))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(_1833_x); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(_1833_x, _1833_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_Match(_1833_x, Dafny.Sequence.FromElements()), _1833_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_StructBuild(Dafny.Sequence.UnicodeFromString("x"), Dafny.Sequence.FromElements()), _1833_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_Tuple(Dafny.Sequence.FromElements()), _1833_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), _1833_x, DAST.Format.UnaryOpFormat.create_NoFormat()), _1833_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("&&"), _1833_x, _1833_x, DAST.Format.BinaryOpFormat.create_NoFormat()), _1833_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_TypeAscription(_1833_x, RAST.Type.create_I128()), _1833_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("1")), _1833_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("1"), true), _1833_x)); + DafnyToRustCompilerCoverage.RASTCoverage.__default.TestNoOptimize(RAST.Expr.create_StmtExpr(RAST.Expr.create_ConversionNum(RAST.Type.create_I128(), _1833_x), _1833_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.Expr.create_AssignVar(Dafny.Sequence.UnicodeFromString("z"), _1834_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(_1834_y)), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("return"))))); + Dafny.ISequence _1835_coverageExpression; + _1835_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(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(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), RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("abc"), false), RAST.Expr.create_ConversionNum(RAST.Type.create_I128(), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), RAST.Expr.create_ConversionNum(RAST.__default.RawType(Dafny.Sequence.UnicodeFromString("X")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))), 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.Expr.create_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(), Dafny.Sequence.FromElements()), RAST.Expr.create_Call(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), Dafny.Sequence.FromElements(RAST.Type.create_I128(), RAST.Type.create_I32()), Dafny.Sequence.FromElements(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("y")))), 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"))); + BigInteger _hi4 = new BigInteger((_1835_coverageExpression).Count); + for (BigInteger _1836_i = BigInteger.Zero; _1836_i < _hi4; _1836_i++) { + RAST._IExpr _1837_c; + _1837_c = (_1835_coverageExpression).Select(_1836_i); + RAST._IPrintingInfo _1838___v0; + _1838___v0 = (_1837_c).printingInfo; + RAST._IExpr _1839___v1; + _1839___v1 = (_1837_c).Optimize(); + Dafny.IMap> _1840___v2; + _1840___v2 = Dafny.Map>.FromElements(new Dafny.Pair>(_1837_c, (_1837_c)._ToString(Dafny.Sequence.UnicodeFromString("")))); + RAST._IExpr _1841___v3; + _1841___v3 = (RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("abc"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), _1837_c)).Optimize(); + RAST._IExpr _1842___v4; + _1842___v4 = (RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("abc"), Std.Wrappers.Option.create_Some(RAST.Type.create_I128()), Std.Wrappers.Option.create_None()), RAST.Expr.create_StmtExpr(RAST.Expr.create_AssignVar(Dafny.Sequence.UnicodeFromString("abc"), _1837_c), RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString(""))))).Optimize(); + RAST._IExpr _1843___v5; + _1843___v5 = (RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&"), _1837_c, DAST.Format.UnaryOpFormat.create_NoFormat())).Optimize(); + RAST._IExpr _1844___v6; + _1844___v6 = (RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("!"), _1837_c, DAST.Format.UnaryOpFormat.create_NoFormat())).Optimize(); + RAST._IExpr _1845___v7; + _1845___v7 = (RAST.Expr.create_ConversionNum(RAST.Type.create_U8(), _1837_c)).Optimize(); + RAST._IExpr _1846___v8; + _1846___v8 = (RAST.Expr.create_ConversionNum(RAST.Type.create_U8(), RAST.Expr.create_Call(_1837_c, Dafny.Sequence.FromElements(), Dafny.Sequence.FromElements()))).Optimize(); + RAST._IExpr _1847___v9; + _1847___v9 = (RAST.Expr.create_ConversionNum(RAST.Type.create_U8(), RAST.Expr.create_Call(RAST.Expr.create_MemberSelect(_1837_c, Dafny.Sequence.UnicodeFromString("from")), Dafny.Sequence.FromElements(), Dafny.Sequence.FromElements()))).Optimize(); + RAST._IExpr _1848___v10; + _1848___v10 = (RAST.Expr.create_ConversionNum(RAST.Type.create_U8(), RAST.Expr.create_Call(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(_1837_c, Dafny.Sequence.UnicodeFromString("DafnyInt")), Dafny.Sequence.UnicodeFromString("from")), Dafny.Sequence.FromElements(), Dafny.Sequence.FromElements()))).Optimize(); + RAST._IExpr _1849___v11; + _1849___v11 = (RAST.Expr.create_ConversionNum(RAST.Type.create_U8(), RAST.Expr.create_Call(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(_1837_c, Dafny.Sequence.UnicodeFromString("dafny_runtime")), Dafny.Sequence.UnicodeFromString("DafnyInt")), Dafny.Sequence.UnicodeFromString("from")), Dafny.Sequence.FromElements(), Dafny.Sequence.FromElements()))).Optimize(); + RAST._IExpr _1850___v12; + _1850___v12 = (RAST.Expr.create_ConversionNum(RAST.Type.create_U8(), RAST.Expr.create_Call(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(RAST.Expr.create_MemberSelect(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("")), Dafny.Sequence.UnicodeFromString("dafny_runtime")), Dafny.Sequence.UnicodeFromString("DafnyInt")), Dafny.Sequence.UnicodeFromString("from")), Dafny.Sequence.FromElements(), Dafny.Sequence.FromElements(_1837_c)))).Optimize(); + Std.Wrappers._IOption> _1851___v13; + _1851___v13 = (_1837_c).RightMostIdentifier(); + } + } + public static void TestPrintingInfo() + { + RAST._IExpr _1852_x; + _1852_x = RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x")); + RAST._IExpr _1853_y; + _1853_y = RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("y")); + DAST.Format._IBinaryOpFormat _1854_bnf; + _1854_bnf = DAST.Format.BinaryOpFormat.create_NoFormat(); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(((RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("x"))).printingInfo).is_UnknownPrecedence); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((_1852_x).printingInfo, RAST.PrintingInfo.create_Precedence(BigInteger.One))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_LiteralInt(Dafny.Sequence.UnicodeFromString("3"))).printingInfo, RAST.PrintingInfo.create_Precedence(BigInteger.One))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("abc"), true)).printingInfo, RAST.PrintingInfo.create_Precedence(BigInteger.One))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("?"), _1852_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_SuffixPrecedence(new BigInteger(5)))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("-"), _1852_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("*"), _1852_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("!"), _1852_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("&"), _1852_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_Precedence(new BigInteger(6)))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_UnaryOp(Dafny.Sequence.UnicodeFromString("&mut"), _1852_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("!!"), _1852_x, DAST.Format.UnaryOpFormat.create_NoFormat())).printingInfo, RAST.PrintingInfo.create_UnknownPrecedence())); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_Select(_1852_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(_1852_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_Call(_1852_x, Dafny.Sequence.FromElements(), 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(_1852_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("*"), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(20), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("/"), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(20), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("%"), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(20), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("+"), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(30), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("-"), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(30), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<<"), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(40), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">>"), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(40), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("&"), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(50), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("^"), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(60), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("|"), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(70), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("=="), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("!="), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<"), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">"), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<="), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">="), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(80), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("&&"), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(90), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("||"), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(100), RAST.Associativity.create_LeftToRight()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(".."), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("..="), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RequiresParentheses()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("="), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("+="), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("-="), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("*="), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("/="), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("%="), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("&="), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("|="), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("^="), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("<<="), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString(">>="), _1852_x, _1853_y, _1854_bnf)).printingInfo, RAST.PrintingInfo.create_PrecedenceAssociativity(new BigInteger(110), RAST.Associativity.create_RightToLeft()))); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(object.Equals((RAST.Expr.create_BinaryOp(Dafny.Sequence.UnicodeFromString("?!?"), _1852_x, _1853_y, _1854_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) + { + } + public static void TestNoExtraSemicolonAfter() + { + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage((RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString(";"))).NoExtraSemicolonAfter()); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(!((RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("a"))).NoExtraSemicolonAfter())); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage((RAST.Expr.create_Return(Std.Wrappers.Option.create_None())).NoExtraSemicolonAfter()); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage((RAST.Expr.create_Continue(Std.Wrappers.Option>.create_None())).NoExtraSemicolonAfter()); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage((RAST.Expr.create_Break(Std.Wrappers.Option>.create_None())).NoExtraSemicolonAfter()); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage((RAST.Expr.create_AssignVar(Dafny.Sequence.UnicodeFromString("x"), RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("y")))).NoExtraSemicolonAfter()); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage((RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("x"), Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_None())).NoExtraSemicolonAfter()); + DafnyToRustCompilerCoverage.RASTCoverage.__default.AssertCoverage(!((RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("x"))).NoExtraSemicolonAfter())); + } + } +} // end of namespace DafnyToRustCompilerCoverage.RASTCoverage \ No newline at end of file diff --git a/Source/DafnyCore/AST/Expressions/Variables/IVariable.cs b/Source/DafnyCore/AST/Expressions/Variables/IVariable.cs index 36f35a0ed1f..b262ff36001 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/IVariable.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/IVariable.cs @@ -24,6 +24,10 @@ string UniqueName { string SanitizedName { get; } + string SanitizedNameShadowable { // A name suitable for compilation, but without the unique identifier. + // Useful to generate readable identifiers in the generated source code. + get; + } string CompileName { get; } diff --git a/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs b/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs index 0fe8374904f..9ebe8a5af79 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs @@ -41,6 +41,13 @@ public string SanitizedName { throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here } } + + public string SanitizedNameShadowable { + get { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here + } + } public string CompileName { get { Contract.Ensures(Contract.Result() != null); diff --git a/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs b/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs index f81d643d644..98c24af35d7 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs @@ -74,9 +74,14 @@ public static string SanitizeName(string nm) { } } + private string sanitizedNameShadowable; + + public virtual string SanitizedNameShadowable => + sanitizedNameShadowable ??= SanitizeName(Name); + private string sanitizedName; public virtual string SanitizedName => - sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizeName(Name)}"; + sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizedNameShadowable}"; protected string compileName; public virtual string CompileName => diff --git a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs index 3ae978865a6..880044f70ee 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs @@ -68,9 +68,15 @@ public string AssignUniqueName(FreshIdGenerator generator) { return uniqueName ??= generator.FreshId(Name + "#"); } + private string sanitizedNameShadowable; + + public string SanitizedNameShadowable => + sanitizedNameShadowable ??= NonglobalVariable.SanitizeName(Name); + private string sanitizedName; + public string SanitizedName => - sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{NonglobalVariable.SanitizeName(Name)}"; + sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizedNameShadowable}"; string compileName; public string CompileName => diff --git a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs index 8d9e9b7414a..efd594d52f4 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs @@ -174,7 +174,7 @@ public class NativeType { public readonly BigInteger LowerBound; public readonly BigInteger UpperBound; public readonly int Bitwidth; // for unassigned types, this shows the number of bits in the type; else is 0 - public enum Selection { Byte, SByte, UShort, Short, UInt, Int, Number, ULong, Long } + public enum Selection { Byte, SByte, UShort, Short, UInt, Int, Number, ULong, Long, UDoubleLong, DoubleLong } public readonly Selection Sel; public NativeType(string Name, BigInteger LowerBound, BigInteger UpperBound, int bitwidth, Selection sel) { Contract.Requires(Name != null); diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index 3b3b7d85dfc..e1f169c90f0 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -3422,15 +3422,16 @@ protected override ConcreteSyntaxTree EmitMapBuilder_Add(MapType mt, IToken tok, return termLeftWriter; } - protected override string GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName, ConcreteSyntaxTree wr) { + protected override void GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName, + ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmt) { if (ct is SetType) { var typeName = TypeName(ct.Arg, wr, tok); - return string.Format($"{DafnySetClass}<{typeName}>.FromCollection({collName})"); + wr.Write(string.Format($"{DafnySetClass}<{typeName}>.FromCollection({collName})")); } else if (ct is MapType) { var mt = (MapType)ct; var domtypeName = TypeName(mt.Domain, wr, tok); var rantypeName = TypeName(mt.Range, wr, tok); - return $"{DafnyMapClass}<{domtypeName},{rantypeName}>.FromCollection({collName})"; + wr.Write($"{DafnyMapClass}<{domtypeName},{rantypeName}>.FromCollection({collName})"); } else { Contract.Assume(false); // unexpected collection type throw new cce.UnreachableException(); // please compiler diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs index 4daa13de548..ca0ecc56b6d 100644 --- a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs @@ -2455,9 +2455,10 @@ protected override ConcreteSyntaxTree EmitMapBuilder_Add(MapType mt, IToken tok, throw new UnsupportedFeatureException(tok, Feature.MapComprehensions); } - protected override string GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName, ConcreteSyntaxTree wr) { + protected override void GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName, + ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmt) { // collections are built in place - return collName; + wr.Write(collName); } protected override void EmitSingleValueGenerator(Expression e, bool inLetExprBody, string type, diff --git a/Source/DafnyCore/Backends/Dafny/AST.dfy b/Source/DafnyCore/Backends/Dafny/AST.dfy index 32721b9e081..7d508fa1060 100644 --- a/Source/DafnyCore/Backends/Dafny/AST.dfy +++ b/Source/DafnyCore/Backends/Dafny/AST.dfy @@ -1,3 +1,22 @@ +module {:extern "DAST.Format"} DAST.Format + /* Cues about how to format different AST elements if necessary, + e.g. to generate idiomatic code when needed. */ +{ + // Dafny AST compilation tenets: + // - The Compiled Dafny AST should be minimal + // - The generated code should look idiomatic and close to the original Dafny file if possible + // Since the two might conflict, the second one is taken care of by adding formatting information + + datatype UnaryOpFormat = + | NoFormat + | CombineFormat + datatype BinaryOpFormat = + | NoFormat + | ImpliesFormat + | EquivalenceFormat + | ReverseFormat +} + module {:extern "DAST"} DAST { import opened Std.Wrappers @@ -19,13 +38,22 @@ module {:extern "DAST"} DAST { Set(element: Type) | Multiset(element: Type) | Map(key: Type, value: Type) | + SetBuilder(element: Type) | + MapBuilder(key: Type, value: Type) | Arrow(args: seq, result: Type) | Primitive(Primitive) | Passthrough(string) | TypeArg(Ident) datatype Primitive = Int | Real | String | Bool | Char - datatype ResolvedType = Datatype(path: seq) | Trait(path: seq) | Newtype(Type) + datatype NewtypeRange = + | U8 | I8 | U16 | I16 | U32 | I32 | U64 | I64 | U128 | I128 | BigInt + | NoRange + + datatype ResolvedType = + | Datatype(path: seq) + | Trait(path: seq) + | Newtype(baseType: Type, range: NewtypeRange, erase: bool) datatype Ident = Ident(id: string) @@ -37,7 +65,7 @@ module {:extern "DAST"} DAST { datatype DatatypeCtor = DatatypeCtor(name: string, args: seq, hasAnyArgs: bool /* includes ghost */) - datatype Newtype = Newtype(name: string, typeParams: seq, base: Type, witnessStmts: seq, witnessExpr: Option) + datatype Newtype = Newtype(name: string, typeParams: seq, base: Type, range: NewtypeRange, witnessStmts: seq, witnessExpr: Option) datatype ClassItem = Method(Method) @@ -47,6 +75,10 @@ module {:extern "DAST"} DAST { datatype Method = Method(isStatic: bool, hasBody: bool, overridingPath: Option>, name: string, typeParams: seq, params: seq, body: seq, outTypes: seq, outVars: Option>) + datatype CallName = + Name(name: string) | + MapBuilderAdd | MapBuilderBuild | SetBuilderAdd | SetBuilderBuild + datatype Statement = DeclareVar(name: string, typ: Type, maybeValue: Option) | Assign(lhs: AssignLhs, value: Expression) | @@ -54,7 +86,7 @@ module {:extern "DAST"} DAST { Labeled(lbl: string, body: seq) | While(cond: Expression, body: seq) | Foreach(boundName: string, boundType: Type, over: Expression, body: seq) | - Call(on: Expression, name: string, typeArgs: seq, args: seq, outs: Option>) | + Call(on: Expression, callName: CallName, typeArgs: seq, args: seq, outs: Option>) | Return(expr: Expression) | EarlyReturn() | Break(toLabel: Option) | @@ -72,13 +104,21 @@ module {:extern "DAST"} DAST { datatype BinOp = Eq(referential: bool, nullable: bool) | - Neq(referential: bool, nullable: bool) | Div() | EuclidianDiv() | Mod() | EuclidianMod() | - Implies() | // TODO: REplace by Not Or + Lt() | // a <= b is !(b < a) + LtChar() | + Plus() | Minus() | Times() | + BitwiseAnd() | BitwiseOr() | BitwiseXor() | + BitwiseShiftRight() | BitwiseShiftLeft() | + And() | Or() | In() | - NotIn() | // TODO: Replace by Not In - SetDifference() | + SeqProperPrefix() | SeqPrefix() | + SetMerge() | SetSubtraction() | SetIntersection() | + Subset() | ProperSubset() | SetDisjoint() | + MapMerge() | MapSubtraction() | + MultisetMerge() | MultisetSubtraction() | MultisetIntersection() | + Submultiset() | ProperSubmultiset() | MultisetDisjoint() | Concat() | Passthrough(string) @@ -94,18 +134,26 @@ module {:extern "DAST"} DAST { SeqConstruct(length: Expression, elem: Expression) | SeqValue(elements: seq, typ: Type) | SetValue(elements: seq) | + MultisetValue(elements: seq) | MapValue(mapElems: seq<(Expression, Expression)>) | + MapBuilder(keyType: Type, valueType: Type) | + SeqUpdate(expr: Expression, indexExpr: Expression, value: Expression) | + MapUpdate(expr: Expression, indexExpr: Expression, value: Expression) | + SetBuilder(elemType: Type) | + ToMultiset(Expression) | This() | Ite(cond: Expression, thn: Expression, els: Expression) | - UnOp(unOp: UnaryOp, expr: Expression) | - BinOp(op: BinOp, left: Expression, right: Expression) | + UnOp(unOp: UnaryOp, expr: Expression, format1: Format.UnaryOpFormat) | + BinOp(op: BinOp, left: Expression, right: Expression, format2: Format.BinaryOpFormat) | ArrayLen(expr: Expression, dim: nat) | + MapKeys(expr: Expression) | + MapValues(expr: Expression) | Select(expr: Expression, field: string, isConstant: bool, onDatatype: bool) | SelectFn(expr: Expression, field: string, onDatatype: bool, isStatic: bool, arity: nat) | Index(expr: Expression, collKind: CollKind, indices: seq) | IndexRange(expr: Expression, isArray: bool, low: Option, high: Option) | TupleSelect(expr: Expression, index: nat) | - Call(on: Expression, name: Ident, typeArgs: seq, args: seq) | + 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(name: Ident, typ: Type, value: Expression, iifeBody: Expression) | diff --git a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs index 6d8330abe7a..42f19c75760 100644 --- a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs +++ b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs @@ -2,12 +2,18 @@ using System.Collections.Generic; using Dafny; using DAST; +using DAST.Format; +using JetBrains.Annotations; using Microsoft.CodeAnalysis; using Microsoft.Dafny.Compilers; using Std.Wrappers; namespace Microsoft.Dafny.Compilers { + interface Container { + public void AddUnsupported(string why); + } + class ProgramBuilder : ModuleContainer { readonly List items = new(); @@ -18,14 +24,23 @@ public void AddModule(Module item) { public List Finish() { return items; } + + public void AddUnsupported(string why) { + items.Add(ModuleContainer.UnsupportedToModule(why)); + } } - interface ModuleContainer { + interface ModuleContainer : Container { void AddModule(Module item); public ModuleBuilder Module(string name, bool isExtern) { return new ModuleBuilder(this, name, isExtern); } + + static public Module UnsupportedToModule(string why) { + return new Module(Sequence.UnicodeFromString(why), true, + Sequence.FromArray(new ModuleItem[] { })); + } } class ModuleBuilder : ClassContainer, TraitContainer, NewtypeContainer, DatatypeContainer { @@ -68,9 +83,13 @@ public object Finish() { )); return parent; } + + public void AddUnsupported(string why) { + body.Add((ModuleItem)ModuleItem.create_Module(ModuleContainer.UnsupportedToModule(why))); + } } - interface ClassContainer { + interface ClassContainer : Container { void AddClass(Class item); public ClassBuilder Class(string name, string enclosingModule, List typeParams, List superClasses) { @@ -116,7 +135,7 @@ public object Finish() { } } - interface TraitContainer { + interface TraitContainer : Container { void AddTrait(Trait item); public TraitBuilder Trait(string name, List typeParams) { @@ -162,11 +181,12 @@ public object Finish() { } } - interface NewtypeContainer { + interface NewtypeContainer : Container { void AddNewtype(Newtype item); - public NewtypeBuilder Newtype(string name, List typeParams, DAST.Type baseType, List witnessStmts, DAST.Expression witness) { - return new NewtypeBuilder(this, name, typeParams, baseType, witnessStmts, witness); + public NewtypeBuilder Newtype(string name, List typeParams, + DAST.Type baseType, DAST.NewtypeRange newtypeRange, List witnessStmts, DAST.Expression witness) { + return new NewtypeBuilder(this, name, typeParams, newtypeRange, baseType, witnessStmts, witness); } } @@ -175,13 +195,16 @@ class NewtypeBuilder : ClassLike { readonly string name; readonly List typeParams; readonly DAST.Type baseType; + private readonly DAST.NewtypeRange newtypeRange; readonly List witnessStmts; readonly DAST.Expression witness; - public NewtypeBuilder(NewtypeContainer parent, string name, List typeParams, DAST.Type baseType, List statements, DAST.Expression witness) { + public NewtypeBuilder(NewtypeContainer parent, string name, List typeParams, + DAST.NewtypeRange newtypeRange, DAST.Type baseType, List statements, DAST.Expression witness) { this.parent = parent; this.name = name; this.typeParams = typeParams; + this.newtypeRange = newtypeRange; this.baseType = baseType; this.witnessStmts = statements; this.witness = witness; @@ -200,6 +223,7 @@ public object Finish() { Sequence.UnicodeFromString(this.name), Sequence.FromArray(this.typeParams.ToArray()), this.baseType, + newtypeRange, Sequence.FromArray(this.witnessStmts.ToArray()), this.witness == null ? Option.create_None() : Option.create_Some(this.witness) )); @@ -207,7 +231,7 @@ public object Finish() { } } - interface DatatypeContainer { + interface DatatypeContainer : Container { void AddDatatype(Datatype item); public DatatypeBuilder Datatype(string name, string enclosingModule, List typeParams, List ctors, bool isCo) { @@ -335,13 +359,21 @@ public DAST.Method Build() { outVars != null ? Option>>.create_Some(Sequence>.FromArray(outVars.ToArray())) : Option>>.create_None() ); } + + public void AddUnsupported(string why) { + AddStatement(StatementContainer.UnsupportedToStatement(why)); + } } - interface StatementContainer { + interface StatementContainer : Container { void AddStatement(DAST.Statement item); void AddBuildable(BuildableStatement item); + public static DAST.Statement UnsupportedToStatement(string why) { + return (DAST.Statement)DAST.Statement.create_Print(ExprContainer.UnsupportedToExpr(why)); + } + List ForkList(); public StatementContainer Fork() { @@ -445,6 +477,10 @@ public List ForkList() { list.Add(ret); return ret; } + + public void AddUnsupported(string why) { + AddStatement(StatementContainer.UnsupportedToStatement(why)); + } } class DeclareBuilder : ExprContainer, BuildableStatement { @@ -482,6 +518,10 @@ public DAST.Statement Build() { return (DAST.Statement)DAST.Statement.create_DeclareVar(Sequence.UnicodeFromString(name), type, Option.create_Some(builtValue[0])); } } + + public void AddUnsupported(string why) { + AddExpr(Compilers.ExprContainer.UnsupportedToExpr(why)); + } } class AssignBuilder : LhsContainer, ExprContainer, BuildableStatement { @@ -519,18 +559,23 @@ public void AddBuildable(BuildableExpr value) { this.value = value; } } + public void AddUnsupported(string why) { + AddExpr(Compilers.ExprContainer.UnsupportedToExpr(why)); + } public DAST.Statement Build() { + + var builtLhs = LhsContainer.Build(lhs); + DAST.Expression rhs; if (this.value == null) { - throw new InvalidOperationException("Cannot assign null value to variable: " + lhs); + rhs = ExprContainer.UnsupportedToExpr("Cannot assign null value to variable: " + lhs); } else { var builtValue = new List(); ExprContainer.RecursivelyBuild(new List { value }, builtValue); - - var builtLhs = LhsContainer.Build(lhs); - - return (DAST.Statement)DAST.Statement.create_Assign(builtLhs, builtValue[0]); + rhs = builtValue[0]; } + + return (DAST.Statement)DAST.Statement.create_Assign(builtLhs, rhs); } } @@ -591,7 +636,9 @@ public ElseBuilder Else() { public DAST.Statement Build() { List builtCondition = new(); - ExprContainer.RecursivelyBuild(new List { condition }, builtCondition); + ExprContainer.RecursivelyBuild(new List { + condition ?? ExprContainer.UnsupportedToExpr("condition to if expression") + }, builtCondition); List builtIfStatements = new(); StatementContainer.RecursivelyBuild(ifBody, builtIfStatements); @@ -605,6 +652,10 @@ public DAST.Statement Build() { Sequence.FromArray(builtElseStatements.ToArray()) ); } + + public void AddUnsupported(string why) { + condition = ExprContainer.UnsupportedToExpr(why); + } } class ElseBuilder : StatementContainer { @@ -625,6 +676,10 @@ public void AddStatement(DAST.Statement item) { public void AddBuildable(BuildableStatement item) { parent.AddElseBuildable(item); } + + public void AddUnsupported(string why) { + AddStatement(StatementContainer.UnsupportedToStatement(why)); + } } class WhileBuilder : ExprContainer, StatementContainer, BuildableStatement { @@ -673,6 +728,10 @@ public DAST.Statement Build() { Sequence.FromArray(builtStatements.ToArray()) ); } + + public void AddUnsupported(string why) { + AddStatement(StatementContainer.UnsupportedToStatement(why)); + } } class ForeachBuilder : ExprContainer, StatementContainer, BuildableStatement { @@ -718,7 +777,9 @@ public List ForkList() { public DAST.Statement Build() { List builtOver = new(); - ExprContainer.RecursivelyBuild(new List { over }, builtOver); + ExprContainer.RecursivelyBuild(new List { + over ?? ExprContainer.UnsupportedToExpr("Foreach over is null") + }, builtOver); List builtStatements = new(); StatementContainer.RecursivelyBuild(body, builtStatements); @@ -730,6 +791,10 @@ public DAST.Statement Build() { Sequence.FromArray(builtStatements.ToArray()) ); } + + public void AddUnsupported(string why) { + AddStatement(StatementContainer.UnsupportedToStatement(why)); + } } class TailRecursiveBuilder : StatementContainer, BuildableStatement { @@ -759,18 +824,22 @@ public DAST.Statement Build() { Sequence.FromArray(builtStatements.ToArray()) ); } + + public void AddUnsupported(string why) { + AddStatement(StatementContainer.UnsupportedToStatement(why)); + } } class CallStmtBuilder : ExprContainer, BuildableStatement { object on = null; - string name = null; + DAST.CallName name = null; List typeArgs = null; readonly List args = new(); List> outs = null; public CallStmtBuilder() { } - public void SetName(string name) { + public void SetName(CallName name) { if (this.name != null) { throw new InvalidOperationException(); } else { @@ -819,12 +888,16 @@ public DAST.Statement Build() { return (DAST.Statement)DAST.Statement.create_Call( builtOn[0], - Sequence.UnicodeFromString(name), + name, Sequence.FromArray(typeArgs.ToArray()), Sequence.FromArray(builtArgs.ToArray()), outs == null ? Option>>.create_None() : Option>>.create_Some(Sequence>.FromArray(outs.ToArray())) ); } + + public void AddUnsupported(string why) { + AddExpr(ExprContainer.UnsupportedToExpr(why)); + } } class ReturnBuilder : ExprContainer, BuildableStatement { @@ -850,10 +923,17 @@ public void AddBuildable(BuildableExpr value) { public DAST.Statement Build() { var builtValue = new List(); + if (value == null) { + return (DAST.Statement)DAST.Statement.create_EarlyReturn(); + } ExprContainer.RecursivelyBuild(new List { value }, builtValue); return (DAST.Statement)DAST.Statement.create_Return(builtValue[0]); } + + public void AddUnsupported(string why) { + value = ExprContainer.UnsupportedToExpr(why); + } } class LabeledBuilder : BuildableStatement, StatementContainer { @@ -891,6 +971,10 @@ public DAST.Statement Build() { Sequence.FromArray(builtStatements.ToArray()) ); } + + public void AddUnsupported(string why) { + AddStatement(StatementContainer.UnsupportedToStatement(why)); + } } class StatementBuffer : StatementContainer { @@ -916,9 +1000,13 @@ public List ForkList() { return builtResult; } + + public void AddUnsupported(string why) { + AddStatement(StatementContainer.UnsupportedToStatement(why)); + } } - class ExprBuffer : ExprContainer { + class ExprBuffer : ExprContainer, BuildableExpr { Stack exprs = new(); public readonly object parent; @@ -956,15 +1044,25 @@ public void AddBuildable(BuildableExpr item) { public DAST.Expression Finish() { if (exprs.Count != 1) { + return ExprContainer.UnsupportedToExpr("Expected exactly one expression in buffer, got " + + exprs.Comma(e => e.ToString())); throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests); // Warning: this is an invalid operation //throw new InvalidOperationException("Expected exactly one expression in buffer, got " + exprs.Comma(e => e.ToString())); } else { return PopN(1)[0]; } } + + public void AddUnsupported(string why) { + AddExpr(ExprContainer.UnsupportedToExpr(why)); + } + + public DAST.Expression Build() { + return Finish(); + } } - interface ExprContainer { + interface ExprContainer : Container { void AddExpr(DAST.Expression item); void AddBuildable(BuildableExpr item); @@ -975,6 +1073,12 @@ BinOpBuilder BinOp(DAST.BinOp op) { return ret; } + BinOpBuilder BinOp(string op, Func callback) { + var ret = new BinOpBuilder(op, callback); + AddBuildable(ret); + return ret; + } + CallExprBuilder Call() { var ret = new CallExprBuilder(); AddBuildable(ret); @@ -1024,13 +1128,23 @@ protected static void RecursivelyBuild(List body, List } else if (maybeBuilt is BuildableExpr buildable) { builtExprs.Add(buildable.Build()); } else { - throw new InvalidOperationException("Unknown buildable type: " + maybeBuilt.GetType()); + throw new InvalidOperationException( + "Unknown buildable type: " + + (maybeBuilt == null ? "NULL" : + maybeBuilt.GetType()) + ); } } } + + static DAST.Expression UnsupportedToExpr(string why) { + return (DAST.Expression)DAST.Expression.create_Ident( + Sequence>.UnicodeFromString($"Unsupported: {why}") + ); + } } - interface LhsContainer { + interface LhsContainer : Container { void AddLhs(DAST.AssignLhs lhs); void AddBuildable(BuildableLhs lhs); @@ -1090,6 +1204,10 @@ public DAST.AssignLhs Build() { return (DAST.AssignLhs)DAST.AssignLhs.create_Index(builtArrayExpr[0], Sequence.FromArray(indices.ToArray())); } + + public void AddUnsupported(string why) { + arrayExpr = ExprContainer.UnsupportedToExpr(why); + } } interface BuildableExpr { @@ -1097,11 +1215,19 @@ interface BuildableExpr { } class BinOpBuilder : ExprContainer, BuildableExpr { - readonly DAST.BinOp op; + private readonly Func internalBuilder; readonly List operands = new(); + private readonly string op; public BinOpBuilder(DAST.BinOp op) { + this.internalBuilder = (DAST.Expression left, DAST.Expression right) => + (DAST.Expression)DAST.Expression.create_BinOp(op, left, right, new BinaryOpFormat_NoFormat()); + this.op = op.ToString(); + } + + public BinOpBuilder(string op, Func callback) { this.op = op; + internalBuilder = callback; } public void AddExpr(DAST.Expression item) { @@ -1113,26 +1239,33 @@ public void AddBuildable(BuildableExpr item) { } public DAST.Expression Build() { + var builtOperands = new List(); + ExprContainer.RecursivelyBuild(operands, builtOperands); + if (operands.Count != 2) { - throw new InvalidOperationException("Expected exactly two operands, got " + operands.Comma(o => o.ToString())); + builtOperands.Insert(0, ExprContainer.UnsupportedToExpr(op + " with not 2 elements")); + return (DAST.Expression)DAST.Expression.create_SetValue( + Sequence.FromElements(builtOperands.ToArray())); } - var builtOperands = new List(); - ExprContainer.RecursivelyBuild(operands, builtOperands); - return (DAST.Expression)DAST.Expression.create_BinOp(op, builtOperands[0], builtOperands[1]); + return internalBuilder(builtOperands[0], builtOperands[1]); + } + + public void AddUnsupported(string why) { + AddExpr(ExprContainer.UnsupportedToExpr(why)); } } class CallExprBuilder : ExprContainer, BuildableExpr { object on = null; - string name = null; + DAST.CallName name = null; List typeArgs = null; readonly List args = new(); List> outs = null; public CallExprBuilder() { } - public void SetName(string name) { + public void SetName(DAST.CallName name) { if (this.name != null) { throw new InvalidOperationException(); } else { @@ -1181,11 +1314,15 @@ public DAST.Expression Build() { return (DAST.Expression)DAST.Expression.create_Call( builtOn[0], - Sequence.UnicodeFromString(name), + name, Sequence.FromArray((typeArgs ?? new()).ToArray()), Sequence.FromArray(builtArgs.ToArray()) ); } + + public void AddUnsupported(string why) { + AddExpr(ExprContainer.UnsupportedToExpr(why)); + } } class ApplyExprBuilder : ExprContainer, BuildableExpr { @@ -1222,6 +1359,10 @@ public DAST.Expression Build() { Sequence.FromArray(builtArgs.ToArray()) ); } + + public void AddUnsupported(string why) { + AddExpr(ExprContainer.UnsupportedToExpr(why)); + } } class LambdaExprBuilder : StatementContainer, BuildableExpr { @@ -1258,6 +1399,10 @@ public DAST.Expression Build() { Sequence.FromArray(builtBody.ToArray()) ); } + + public void AddUnsupported(string why) { + AddStatement(StatementContainer.UnsupportedToStatement(why)); + } } class IIFEExprBuilder : ExprContainer, BuildableExpr { @@ -1297,7 +1442,9 @@ public DAST.Expression Build() { ExprContainer.RecursivelyBuild(new List { body }, builtBody); var builtValue = new List(); - ExprContainer.RecursivelyBuild(new List { value }, builtValue); + ExprContainer.RecursivelyBuild(new List { value + ?? ExprContainer.UnsupportedToExpr("IIFEExprBuilder with empty value") + }, builtValue); return (DAST.Expression)DAST.Expression.create_IIFE( Sequence.UnicodeFromString(name), @@ -1306,6 +1453,10 @@ public DAST.Expression Build() { builtBody[0] ); } + + public void AddUnsupported(string why) { + AddExpr(ExprContainer.UnsupportedToExpr(why)); + } } class IIFEExprRhs : ExprContainer { @@ -1330,6 +1481,10 @@ public void AddBuildable(BuildableExpr item) { parent.value = item; } } + + public void AddUnsupported(string why) { + AddExpr(ExprContainer.UnsupportedToExpr(why)); + } } class BetaRedexBuilder : ExprContainer, BuildableExpr { @@ -1360,6 +1515,10 @@ public DAST.Expression Build() { builtBody[0] ); } + + public void AddUnsupported(string why) { + AddExpr(ExprContainer.UnsupportedToExpr(why)); + } } class ConvertBuilder : ExprContainer, BuildableExpr { @@ -1390,14 +1549,24 @@ public void AddBuildable(BuildableExpr item) { public DAST.Expression Build() { var builtValue = new List(); - ExprContainer.RecursivelyBuild(new List { value }, builtValue); + DAST.Expression v; + if (value == null) { + v = ExprContainer.UnsupportedToExpr($"Conversion from {fromType} to {toType} of something missing"); + } else { + ExprContainer.RecursivelyBuild(new List { value }, builtValue); + v = builtValue[0]; + } return (DAST.Expression)DAST.Expression.create_Convert( - builtValue[0], + v, fromType, toType ); } + + public void AddUnsupported(string why) { + AddExpr(ExprContainer.UnsupportedToExpr(why)); + } } class IndexBuilder : ExprContainer, BuildableExpr { @@ -1436,6 +1605,10 @@ public DAST.Expression Build() { Sequence.FromArray(indices.ToArray()) ); } + + public void AddUnsupported(string why) { + AddExpr(ExprContainer.UnsupportedToExpr(why)); + } } } diff --git a/Source/DafnyCore/Backends/Dafny/BuilderSyntaxTree.cs b/Source/DafnyCore/Backends/Dafny/BuilderSyntaxTree.cs index 8cb941f8752..c1a14b17ce1 100644 --- a/Source/DafnyCore/Backends/Dafny/BuilderSyntaxTree.cs +++ b/Source/DafnyCore/Backends/Dafny/BuilderSyntaxTree.cs @@ -4,27 +4,29 @@ namespace Microsoft.Dafny.Compilers { class BuilderSyntaxTree : ConcreteSyntaxTree { public readonly T Builder; + public readonly DafnyCodeGenerator Compiler; - public BuilderSyntaxTree(T builder) { + public BuilderSyntaxTree(T builder, DafnyCodeGenerator compiler) { if (builder == null) { throw new ArgumentNullException(nameof(builder)); } Builder = builder; + Compiler = compiler; } public override ConcreteSyntaxTree Fork(int relativeIndent = 0) { if (Builder is StatementContainer statementContainer) { - return new BuilderSyntaxTree(statementContainer.Fork()); + return new BuilderSyntaxTree(statementContainer.Fork(), Compiler); } else { - DafnyCodeGenerator.ThrowGeneralUnsupported(); // Warning: this is an invalid operation: cannot fork builder of type Builder.GetType() - throw new InvalidOperationException(); + // Warning: this is an invalid operation: cannot fork builder of type Builder.GetType() + throw new InvalidOperationException("Builder not StatementContainer but " + Builder.GetType().ToString()); } } public override ConcreteSyntaxTree ForkInParens() { // TODO(shadaj): perhaps should check if we are an expr container - return new BuilderSyntaxTree(Builder); + return new BuilderSyntaxTree(Builder, Compiler); } } } diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs index c205bd9eb76..6ee17e90993 100644 --- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs @@ -1,5 +1,6 @@ using System; using System.Collections.Generic; +using System.Diagnostics; using Dafny; using JetBrains.Annotations; using DAST; @@ -7,6 +8,8 @@ using Microsoft.BaseTypes; using System.Linq; using System.Diagnostics.Contracts; +using System.IO; +using DAST.Format; using Std.Wrappers; namespace Microsoft.Dafny.Compilers { @@ -14,6 +17,8 @@ namespace Microsoft.Dafny.Compilers { class DafnyCodeGenerator : SinglePassCodeGenerator { ProgramBuilder items; public object currentBuilder; + public bool emitUncompilableCode; + public bool preventShadowing; public void Start() { if (items != null) { @@ -31,16 +36,34 @@ public List Build() { return res; } - public DafnyCodeGenerator(DafnyOptions options, ErrorReporter reporter) : base(options, reporter) { + public DafnyCodeGenerator(DafnyOptions options, ErrorReporter reporter, bool preventShadowing, bool canEmitUncompilableCode) : base(options, reporter) { options.SystemModuleTranslationMode = CommonOptionBag.SystemModuleMode.Include; if (Options?.CoverageLegendFile != null) { Imports.Add("DafnyProfiling"); } + + emitUncompilableCode = options.Get(CommonOptionBag.EmitUncompilableCode) && canEmitUncompilableCode; + this.preventShadowing = preventShadowing; + } + + protected override string GetCompileNameNotProtected(IVariable v) { + return preventShadowing ? v.CompileName : v.SanitizedNameShadowable; + } + + public void AddUnsupported(string why) { + if (emitUncompilableCode && currentBuilder is Container container) { + container.AddUnsupported(why); + } else { + throw new UnsupportedInvalidOperationException(why); + } } - public static void ThrowGeneralUnsupported() { - // throw new InvalidOperationException(); // (useful for debugging) - throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests); + public void AddUnsupportedFeature(IToken token, Feature feature) { + if (emitUncompilableCode && currentBuilder is Container container) { + container.AddUnsupported("" + feature.ToString() + ""); + } else { + throw new RecoverableUnsupportedFeatureException(token, feature); + } } public override IReadOnlySet UnsupportedFeatures => new HashSet { @@ -67,7 +90,9 @@ public static void ThrowGeneralUnsupported() { Feature.TuplesWiderThan20, Feature.ForLoops, Feature.Traits, - Feature.RuntimeCoverageReport + Feature.RuntimeCoverageReport, + Feature.MultiDimensionalArrays, + Feature.NonNativeNewtypes }; private readonly List Imports = new() { DafnyDefaultModule }; @@ -81,13 +106,13 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) { } public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) { - ThrowGeneralUnsupported(); - throw new InvalidOperationException(); + AddUnsupported("Call to main"); } protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string argsParameterName) { - ThrowGeneralUnsupported(); - throw new InvalidOperationException(); + AddUnsupported("create static main"); + return new BuilderSyntaxTree( + new ExprBuffer(this), this); } protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule, @@ -118,7 +143,7 @@ private static string MangleName(string name) { protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type from, Type to, IToken tok, ConcreteSyntaxTree wr, Type toOrig = null) { if (currentBuilder is ExprBuffer buf && wr is not BuilderSyntaxTree) { // the writers are not currently wired properly for DatatypeValue - wr = new BuilderSyntaxTree(buf); + wr = new BuilderSyntaxTree(buf, this); } if (from == to) { @@ -137,13 +162,13 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type from, Type to to = toNonNull.RhsWithArgument(toUdt.TypeArgs); } - return EmitCoercionIfNecessary(from, to, tok, new BuilderSyntaxTree(nullConvert)); + return EmitCoercionIfNecessary(from, to, tok, new BuilderSyntaxTree(nullConvert, this)); } else { return base.EmitCoercionIfNecessary(from, to, tok, wr); } } else if (from != null && to != null && (from.AsSubsetType != null || to.AsSubsetType != null)) { if (wr is BuilderSyntaxTree stmt) { - return new BuilderSyntaxTree(stmt.Builder.Convert(GenType(from), GenType(to))); + return new BuilderSyntaxTree(stmt.Builder.Convert(GenType(from), GenType(to)), this); } else { return base.EmitCoercionIfNecessary(from, to, tok, wr); } @@ -151,8 +176,9 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type from, Type to if (from == null || to == null || from.Equals(to, true)) { return wr; } else { - ThrowGeneralUnsupported(); - throw new InvalidOperationException(); + AddUnsupported($"Coercion from {from} to {to}"); + return new BuilderSyntaxTree( + new ExprBuffer(this), this); } } } @@ -162,11 +188,12 @@ protected override IClassWriter CreateClass(string moduleName, string name, bool if (currentBuilder is ClassContainer builder) { List typeParams = new(); foreach (var tp in typeParameters) { - if (!isTpSupported(tp)) { - ThrowGeneralUnsupported(); //("Contravariance in type parameters"); + var compileName = IdProtect(tp.GetCompileName(Options)); + if (!isTpSupported(tp, out var why)) { + AddUnsupported(why); } - typeParams.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence.UnicodeFromString(IdProtect(tp.GetCompileName(Options))))); + typeParams.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence.UnicodeFromString(compileName))); } return new ClassWriter(this, typeParams.Count > 0, builder.Class(name, moduleName, typeParams, superClasses.Select(t => GenType(t)).ToList())); @@ -177,39 +204,49 @@ protected override IClassWriter CreateClass(string moduleName, string name, bool protected override IClassWriter CreateTrait(string name, bool isExtern, List typeParameters, TraitDecl trait, List superClasses, IToken tok, ConcreteSyntaxTree wr) { - throw new UnsupportedFeatureException(Token.NoToken, Feature.Traits); - // traits need a bit more work - // if (currentBuilder is TraitContainer builder) { - // List typeParams = new(); - // foreach (var tp in trait.TypeArgs) { - // typeParams.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence.UnicodeFromString(IdProtect(tp.GetCompileName(Options))))); - // } + if (currentBuilder is TraitContainer builder) { + List typeParams = new(); + foreach (var tp in trait.TypeArgs) { + typeParams.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence.UnicodeFromString(IdProtect(tp.GetCompileName(Options))))); + } - // return new ClassWriter(this, builder.Trait(name, typeParams)); - // } else { - // throw new InvalidOperationException(); - // } + return new ClassWriter(this, typeParameters.Any(), builder.Trait(name, typeParams)); + } else { + throw new InvalidOperationException(); + } } protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, ConcreteSyntaxTree wr) { - throw new UnsupportedFeatureException(Token.NoToken, Feature.Iterators); + AddUnsupportedFeature(iter.tok, Feature.Iterators); + return wr; } - private static bool isTpSupported(TypeParameter tp) { - return tp.Variance == TypeParameter.TPVariance.Non && - tp.Characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified; + private static bool isTpSupported(TypeParameter tp, [CanBeNull] out string why) { + if (tp.Variance != TypeParameter.TPVariance.Non) { + why = $"Unsupported: Type variance {tp.Variance} not supported"; + return false; + } + + if (tp.Characteristics.EqualitySupport != TypeParameter.EqualitySupportValue.Unspecified) { + why = $"Unsupported: Type parameter Equality support {tp.Characteristics.EqualitySupport} not supported for type parameters"; + return false; + } + + why = null; + return true; } protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxTree wr) { if (currentBuilder is DatatypeContainer builder) { List typeParams = new(); foreach (var tp in dt.TypeArgs) { - if (!isTpSupported(tp) && !(dt is TupleTypeDecl)) { - ThrowGeneralUnsupported(); //("Contravariance in type parameters"); + var compileName = IdProtect(tp.GetCompileName(Options)); + if (!isTpSupported(tp, out var why) && !(dt is TupleTypeDecl)) { + AddUnsupported(why); } - typeParams.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence.UnicodeFromString(IdProtect(tp.GetCompileName(Options))))); + typeParams.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence.UnicodeFromString(compileName))); } List ctors = new(); @@ -241,19 +278,22 @@ protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTre List witnessStmts = new(); DAST.Expression witness = null; + var buf = new ExprBuffer(null); + var statementBuf = new StatementBuffer(); if (nt.WitnessKind == SubsetTypeDecl.WKind.Compiled) { - var buf = new ExprBuffer(null); - var statementBuf = new StatementBuffer(); EmitExpr( nt.Witness, false, - EmitCoercionIfNecessary(nt.Witness.Type, erasedType, null, new BuilderSyntaxTree(buf)), - new BuilderSyntaxTree(statementBuf) + EmitCoercionIfNecessary(nt.Witness.Type, erasedType, null, + new BuilderSyntaxTree(buf, this)), + new BuilderSyntaxTree(statementBuf, this) ); witness = buf.Finish(); witnessStmts = statementBuf.PopAll(); } - return new ClassWriter(this, false, builder.Newtype(nt.GetCompileName(Options), new(), GenType(erasedType), witnessStmts, witness)); + return new ClassWriter(this, false, builder.Newtype( + nt.GetCompileName(Options), new(), + GenType(erasedType), NativeTypeToNewtypeRange(nt.NativeType), witnessStmts, witness)); } else { throw new InvalidOperationException(); } @@ -291,6 +331,8 @@ private DAST.Type GenType(Type typ) { 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")), _ => throw new InvalidOperationException(), }); } else if (xType is SeqType seq) { @@ -307,11 +349,12 @@ private DAST.Type GenType(Type typ) { var valueType = map.Range; return (DAST.Type)DAST.Type.create_Map(GenType(keyType), GenType(valueType)); } else if (xType is BitvectorType) { - ThrowGeneralUnsupported(); //("Bitvector types"); - throw new InvalidOperationException(); + AddUnsupported("Bitvector types"); + return (DAST.Type)DAST.Type.create_Passthrough(Sequence.UnicodeFromString("Missing feature: Bitvector types")); } else { - ThrowGeneralUnsupported(); //("Type name for " + xType + " (" + typ.GetType() + ")"); - throw new InvalidOperationException(); + var why = "Type name for " + xType + " (" + typ.GetType() + ")"; + AddUnsupported(why); + return (DAST.Type)DAST.Type.create_Passthrough(Sequence.UnicodeFromString($"Unsupported: {why}")); } } @@ -321,28 +364,33 @@ protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree List witnessStmts = new(); DAST.Expression witness = null; + var statementBuf = new StatementBuffer(); + var buf = new ExprBuffer(null); if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) { - var statementBuf = new StatementBuffer(); - var buf = new ExprBuffer(null); EmitExpr( sst.Witness, false, - EmitCoercionIfNecessary(sst.Witness.Type, erasedType, null, new BuilderSyntaxTree(buf)), - new BuilderSyntaxTree(statementBuf) + EmitCoercionIfNecessary(sst.Witness.Type, erasedType, null, new BuilderSyntaxTree(buf, this)), + new BuilderSyntaxTree(statementBuf, this) ); witness = buf.Finish(); witnessStmts = statementBuf.PopAll(); } + string baseName = sst.Var.CompileName; + DAST.Expression baseConstraint = buf.Finish(); + var baseConstraintStmts = statementBuf.PopAll(); // TODO: Integrate in AST. List typeParams = new(); foreach (var tp in sst.TypeArgs) { - if (!isTpSupported(tp)) { - ThrowGeneralUnsupported(); //("Contravariance in type parameters"); + var compileName = tp.Name; + if (!isTpSupported(tp, out var why)) { + AddUnsupported(why); } - typeParams.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence.UnicodeFromString(tp.Name))); + typeParams.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence.UnicodeFromString(compileName))); } - builder.Newtype(sst.GetCompileName(Options), typeParams, GenType(erasedType), witnessStmts, witness).Finish(); + builder.Newtype(sst.GetCompileName(Options), typeParams, + GenType(erasedType), (NewtypeRange)NewtypeRange.create_NoRange(), witnessStmts, witness).Finish(); } else { throw new InvalidOperationException(); } @@ -369,16 +417,18 @@ public ClassWriter(DafnyCodeGenerator compiler, bool hasTypeArgs, ClassLike buil public ConcreteSyntaxTree CreateMethod(Method m, List typeArgs, bool createBody, bool forBodyInheritance, bool lookasideBody) { if (m.IsStatic && this.hasTypeArgs) { - ThrowGeneralUnsupported(); //("Static methods with type arguments"); + compiler.AddUnsupported("Static methods with type arguments"); + return new ConcreteSyntaxTree(); } List astTypeArgs = new(); foreach (var typeArg in typeArgs) { - if (!isTpSupported(typeArg.Formal)) { - ThrowGeneralUnsupported(); //("Contravariance in type parameters") + var compileName = compiler.IdProtect(typeArg.Formal.GetCompileName(compiler.Options)); + if (!isTpSupported(typeArg.Formal, out var why)) { + compiler.AddUnsupported(why); } - astTypeArgs.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence.UnicodeFromString(compiler.IdProtect(typeArg.Formal.GetCompileName(compiler.Options))))); + astTypeArgs.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence.UnicodeFromString(compileName))); } List params_ = new(); @@ -408,7 +458,7 @@ public ConcreteSyntaxTree CreateMethod(Method m, List methods.Add(builder); if (createBody) { - return new BuilderSyntaxTree(builder); + return new BuilderSyntaxTree(builder, this.compiler); } else { // TODO(shadaj): actually create a trait return null; @@ -416,23 +466,26 @@ public ConcreteSyntaxTree CreateMethod(Method m, List } public ConcreteSyntaxTree SynthesizeMethod(Method m, List typeArgs, bool createBody, bool forBodyInheritance, bool lookasideBody) { - throw new UnsupportedFeatureException(Token.NoToken, Feature.MethodSynthesis); + compiler.AddUnsupportedFeature(m.tok, Feature.MethodSynthesis); + return new ConcreteSyntaxTree(); } public ConcreteSyntaxTree CreateFunction(string name, List typeArgs, List formals, Type resultType, IToken tok, bool isStatic, bool createBody, MemberDecl member, bool forBodyInheritance, bool lookasideBody) { if (isStatic && this.hasTypeArgs) { - ThrowGeneralUnsupported(); //("Static methods with type arguments"); + compiler.AddUnsupported("Static functions with type arguments"); + return new ConcreteSyntaxTree(); } List astTypeArgs = new(); foreach (var typeArg in typeArgs) { - if (!isTpSupported(typeArg.Formal)) { - ThrowGeneralUnsupported(); //("Contravariance in type parameters"); + var compileName = compiler.IdProtect(typeArg.Formal.GetCompileName(compiler.Options)); + if (!isTpSupported(typeArg.Formal, out var why)) { + compiler.AddUnsupported(why); } - astTypeArgs.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence.UnicodeFromString(compiler.IdProtect(typeArg.Formal.GetCompileName(compiler.Options))))); + astTypeArgs.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence.UnicodeFromString(compileName))); } List params_ = new(); @@ -456,7 +509,7 @@ public ConcreteSyntaxTree CreateFunction(string name, List(builder); + return new BuilderSyntaxTree(builder, this.compiler); } else { return null; } @@ -465,7 +518,8 @@ public ConcreteSyntaxTree CreateFunction(string name, ListStatic fields with type arguments"); + return new ConcreteSyntaxTree(); } var overridingTrait = member.OverriddenMember?.EnclosingClass; @@ -482,7 +536,7 @@ public ConcreteSyntaxTree CreateGetter(string name, TopLevelDecl enclosingDecl, methods.Add(builder); if (createBody) { - return new BuilderSyntaxTree(builder); + return new BuilderSyntaxTree(builder, this.compiler); } else { return null; } @@ -490,8 +544,14 @@ public ConcreteSyntaxTree CreateGetter(string name, TopLevelDecl enclosingDecl, public ConcreteSyntaxTree CreateGetterSetter(string name, Type resultType, IToken tok, bool createBody, MemberDecl member, out ConcreteSyntaxTree setterWriter, bool forBodyInheritance) { - ThrowGeneralUnsupported(); - throw new InvalidOperationException(); + compiler.AddUnsupported("Create Getter Setter"); + if (createBody) { + setterWriter = new ConcreteSyntaxTree(); + return new ConcreteSyntaxTree(); + } else { + setterWriter = null; + return null; + } } public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic, bool isConst, Type type, @@ -531,7 +591,7 @@ public void Finish() { protected override ConcreteSyntaxTree EmitReturnExpr(ConcreteSyntaxTree wr) { if (wr is BuilderSyntaxTree stmtContainer) { - return new BuilderSyntaxTree(stmtContainer.Builder.Return()); + return new BuilderSyntaxTree(stmtContainer.Builder.Return(), this); } else { throw new InvalidOperationException(); } @@ -572,7 +632,7 @@ protected override ConcreteSyntaxTree EmitMethodReturns(Method m, ConcreteSyntax protected override ConcreteSyntaxTree EmitTailCallStructure(MemberDecl member, ConcreteSyntaxTree wr) { if (wr is BuilderSyntaxTree stmtContainer) { var recBuilder = stmtContainer.Builder.TailRecursive(); - return new BuilderSyntaxTree(recBuilder); + return new BuilderSyntaxTree(recBuilder, this); } else { throw new InvalidOperationException(); } @@ -605,11 +665,11 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree } else { if (type.AsNewtype != null && type.AsNewtype.WitnessKind == SubsetTypeDecl.WKind.Compiled) { var buf = new ExprBuffer(null); - EmitExpr(type.AsNewtype.Witness, false, new BuilderSyntaxTree(buf), null); + EmitExpr(type.AsNewtype.Witness, false, new BuilderSyntaxTree(buf, this), null); bufferedInitializationValue = Option.create_Some(buf.Finish()); } else if (type.AsSubsetType != null && type.AsSubsetType.WitnessKind == SubsetTypeDecl.WKind.Compiled) { var buf = new ExprBuffer(null); - EmitExpr(type.AsSubsetType.Witness, false, new BuilderSyntaxTree(buf), null); + EmitExpr(type.AsSubsetType.Witness, false, new BuilderSyntaxTree(buf, this), null); bufferedInitializationValue = Option.create_Some(buf.Finish()); } else if (type.AsDatatype != null && type.AsDatatype.Ctors.Count == 1 && type.AsDatatype.Ctors[0].EnclosingDatatype is TupleTypeDecl tupleDecl) { var elems = new List(); @@ -629,8 +689,11 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree ); } } else if (type.IsArrowType) { - ThrowGeneralUnsupported(); - throw new InvalidOperationException(); + if (emitUncompilableCode) { + this.AddUnsupported("Initializer for arrow type"); + } else { + throw new UnsupportedInvalidOperationException("Initializer for arrow type"); + } } else { bufferedInitializationValue = Option.create_Some( DAST.Expression.create_InitializationValue(GenType(type)) @@ -654,7 +717,7 @@ protected override string TypeName_Companion(Type type, ConcreteSyntaxTree wr, I throw new InvalidOperationException(); } - EmitTypeName_Companion(type, new BuilderSyntaxTree(actualBuilder), wr, tok, member); + EmitTypeName_Companion(type, new BuilderSyntaxTree(actualBuilder, this), wr, tok, member); return ""; } @@ -666,6 +729,9 @@ protected override void EmitTypeName_Companion(Type type, ConcreteSyntaxTree wr, DatatypeWrapperEraser.IsErasableDatatypeWrapper(Options, dt, out _)) { container.Builder.AddExpr((DAST.Expression)DAST.Expression.create_Companion(PathFromTopLevel(udt.ResolvedClass))); } else { + if (type.AsTopLevelTypeWithMembers == null) { // git-issues/git-issue-697g.dfy while iterating over "nat" + throw new UnsupportedFeatureException(tok, Feature.RunAllTests); + } container.Builder.AddExpr((DAST.Expression)DAST.Expression.create_Companion(PathFromTopLevel(type.AsTopLevelTypeWithMembers))); } } else { @@ -674,12 +740,16 @@ protected override void EmitTypeName_Companion(Type type, ConcreteSyntaxTree wr, } protected override void EmitNameAndActualTypeArgs(string protectedName, List typeArgs, IToken tok, ConcreteSyntaxTree wr) { - if (wr is BuilderSyntaxTree st && st.Builder is CallExprBuilder callExpr) { - callExpr.SetName(protectedName); - } else if (wr is BuilderSyntaxTree st2 && st2.Builder is CallStmtBuilder callStmt) { - callStmt.SetName(protectedName); + if (GetExprBuilder(wr, out var st) && st.Builder is CallExprBuilder callExpr) { + callExpr.SetName((DAST.CallName)DAST.CallName.create_Name(Sequence.UnicodeFromString(protectedName))); + } else if (GetExprBuilder(wr, out var st2) && st2.Builder is CallStmtBuilder callStmt) { + callStmt.SetName((DAST.CallName)DAST.CallName.create_Name(Sequence.UnicodeFromString(protectedName))); } else { - ThrowGeneralUnsupported(); + AddUnsupported("Builder issue: wr is as " + wr.GetType() + + (GetExprBuilder(wr, out var st3) ? + " and its builder is a " + st3.Builder.GetType() : "" + )); + return; } base.EmitNameAndActualTypeArgs(protectedName, typeArgs, tok, wr); @@ -691,8 +761,8 @@ protected override void TypeArgDescriptorUse(bool isStatic, bool lookasideBody, } protected override bool DeclareFormal(string prefix, string name, Type type, IToken tok, bool isInParam, ConcreteSyntaxTree wr) { - ThrowGeneralUnsupported(); - throw new InvalidOperationException(); + AddUnsupported("Declare formal"); + return true; } protected override void DeclareLocalVar(string name, Type type, IToken tok, bool leaveRoomForRhs, string rhs, @@ -709,7 +779,8 @@ protected override void DeclareLocalVar(string name, Type type, IToken tok, bool } } else if (rhs == "BUFFERED") { if (bufferedInitializationValue == null) { - throw new InvalidOperationException("Expected a buffered value to have been populated because rhs != null"); + throw new InvalidOperationException( + "Expected a buffered value to have been populated because rhs != null"); } var rhsValue = bufferedInitializationValue; @@ -733,7 +804,7 @@ protected override void DeclareLocalVar(string name, Type type, IToken tok, bool protected override ConcreteSyntaxTree DeclareLocalVar(string name, Type type, IToken tok, ConcreteSyntaxTree wr) { if (wr is BuilderSyntaxTree stmtContainer) { var variable = stmtContainer.Builder.DeclareAndAssign(GenType(type), name); - return new BuilderSyntaxTree(variable); + return new BuilderSyntaxTree(variable, this); } else { throw new InvalidOperationException(); } @@ -748,7 +819,7 @@ protected override void DeclareLocalOutVar(string name, Type type, IToken tok, s } protected override void EmitCallReturnOuts(List outTmps, ConcreteSyntaxTree wr) { - if (wr is BuilderSyntaxTree builder && builder.Builder is CallStmtBuilder call) { + if (GetExprBuilder(wr, out var builder) && builder.Builder is CallStmtBuilder call) { call.SetOuts(outTmps.Select(i => Sequence.UnicodeFromString(i)).ToList()); } else { throw new InvalidOperationException(); @@ -761,7 +832,7 @@ protected override void TrCallStmt(CallStmt s, string receiverReplacement, Concr base.TrCallStmt(s, receiverReplacement, wr, wrStmts, wrStmtsAfterCall); } else { var callBuilder = stmtContainer.Builder.Call(); - base.TrCallStmt(s, receiverReplacement, new BuilderSyntaxTree(callBuilder), wrStmts, wrStmtsAfterCall); + base.TrCallStmt(s, receiverReplacement, new BuilderSyntaxTree(callBuilder, this), wrStmts, wrStmtsAfterCall); } } else { throw new InvalidOperationException("Cannot call statement in this context: " + currentBuilder); @@ -771,9 +842,9 @@ protected override void TrCallStmt(CallStmt s, string receiverReplacement, Concr 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(); - base.EmitCallToInheritedMethod(method, heir, new BuilderSyntaxTree(callBuilder), wStmts, wStmtsAfterCall); + base.EmitCallToInheritedMethod(method, heir, new BuilderSyntaxTree(callBuilder, this), wStmts, wStmtsAfterCall); } else { - throw new InvalidOperationException("Cannot call statement in this context: " + currentBuilder); + AddUnsupported("Cannot call statement in this context: " + currentBuilder); } } @@ -788,16 +859,16 @@ protected override void CompileFunctionCallExpr(FunctionCallExpr e, ConcreteSynt if (wr is BuilderSyntaxTree builder) { var callBuilder = builder.Builder.Call(); - base.CompileFunctionCallExpr(e, new BuilderSyntaxTree(callBuilder), inLetExprBody, wStmts, tr, true); + base.CompileFunctionCallExpr(e, new BuilderSyntaxTree(callBuilder, this), inLetExprBody, wStmts, tr, true); } else { throw new InvalidOperationException("Cannot call function in this context: " + currentBuilder); } } protected override void EmitActualTypeArgs(List typeArgs, IToken tok, ConcreteSyntaxTree wr) { - if (wr is BuilderSyntaxTree st && st.Builder is CallExprBuilder callExpr) { + if (GetExprBuilder(wr, out var st) && st.Builder is CallExprBuilder callExpr) { callExpr.SetTypeArgs(typeArgs.Select(GenType).ToList()); - } else if (wr is BuilderSyntaxTree st2 && st2.Builder is CallStmtBuilder callStmt) { + } else if (GetExprBuilder(wr, out var st2) && st2.Builder is CallStmtBuilder callStmt) { callStmt.SetTypeArgs(typeArgs.Select(GenType).ToList()); } else { throw new InvalidOperationException("Cannot emit actual type args in this context: " + currentBuilder); @@ -806,9 +877,11 @@ protected override void EmitActualTypeArgs(List typeArgs, IToken tok, Conc private class BuilderLvalue : ILvalue { readonly string name; + private readonly DafnyCodeGenerator compiler; - public BuilderLvalue(string name) { + public BuilderLvalue(string name, DafnyCodeGenerator compiler) { this.name = name; + this.compiler = compiler; } public void EmitRead(ConcreteSyntaxTree wr) { @@ -819,7 +892,7 @@ public ConcreteSyntaxTree EmitWrite(ConcreteSyntaxTree wr) { if (wr is BuilderSyntaxTree stmtContainer) { var assign = stmtContainer.Builder.Assign(); assign.AddLhs((DAST.AssignLhs)DAST.AssignLhs.create_Ident(Sequence.UnicodeFromString(name))); - return new BuilderSyntaxTree(assign); + return new BuilderSyntaxTree(assign, this.compiler); } else { throw new InvalidOperationException(); } @@ -829,17 +902,19 @@ public ConcreteSyntaxTree EmitWrite(ConcreteSyntaxTree wr) { private class ExprLvalue : ILvalue { readonly DAST.Expression expr; readonly DAST.AssignLhs assignExpr; + private readonly DafnyCodeGenerator compiler; - public ExprLvalue(DAST.Expression expr, DAST.AssignLhs assignExpr) { + public ExprLvalue(DAST.Expression expr, DAST.AssignLhs assignExpr, DafnyCodeGenerator compiler) { this.expr = expr; this.assignExpr = assignExpr; + this.compiler = compiler; } public void EmitRead(ConcreteSyntaxTree wr) { - if (wr is BuilderSyntaxTree exprContainer) { + if (GetExprBuilder(wr, out var exprContainer)) { exprContainer.Builder.AddExpr(expr); } else { - throw new InvalidOperationException(); + compiler.AddUnsupported("EmitRead without ExprContainer builder"); } } @@ -851,7 +926,7 @@ public ConcreteSyntaxTree EmitWrite(ConcreteSyntaxTree wr) { if (wr is BuilderSyntaxTree stmtContainer) { var assign = stmtContainer.Builder.Assign(); assign.AddLhs(assignExpr); - return new BuilderSyntaxTree(assign); + return new BuilderSyntaxTree(assign, this.compiler); } else { throw new InvalidOperationException(); } @@ -863,7 +938,7 @@ protected override void EmitAssignment(string lhs, Type/*?*/ lhsType, string rhs } protected override ILvalue IdentLvalue(string var) { - return new BuilderLvalue(var); + return new BuilderLvalue(var, this); } protected override ILvalue SeqSelectLvalue(SeqSelectExpr ll, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { @@ -873,13 +948,13 @@ protected override ILvalue SeqSelectLvalue(SeqSelectExpr ll, ConcreteSyntaxTree EmitCoercionIfNecessary( ll.Seq.Type, ll.Seq.Type.IsNonNullRefType || !ll.Seq.Type.IsRefType ? null : UserDefinedType.CreateNonNullType((UserDefinedType)ll.Seq.Type.NormalizeExpand()), - null, new BuilderSyntaxTree(sourceBuf) + null, new BuilderSyntaxTree(sourceBuf, this) ), wStmts ); var indexBuf = new ExprBuffer(null); - EmitExpr(ll.E0, false, new BuilderSyntaxTree(indexBuf), wStmts); + EmitExpr(ll.E0, false, new BuilderSyntaxTree(indexBuf, this), wStmts); var source = sourceBuf.Finish(); var index = indexBuf.Finish(); @@ -896,19 +971,19 @@ protected override ILvalue SeqSelectLvalue(SeqSelectExpr ll, ConcreteSyntaxTree return new ExprLvalue( (DAST.Expression)DAST.Expression.create_Index(source, collKind, Sequence.FromElements(index)), - (DAST.AssignLhs)DAST.AssignLhs.create_Index(source, Sequence.FromElements(index)) + (DAST.AssignLhs)DAST.AssignLhs.create_Index(source, Sequence.FromElements(index)), + this ); } protected override ILvalue MultiSelectLvalue(MultiSelectExpr ll, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { - ThrowGeneralUnsupported(); - throw new InvalidOperationException(); + throw new UnsupportedFeatureException(ll.tok, Feature.MultiDimensionalArrays); } protected override void EmitPrintStmt(ConcreteSyntaxTree wr, Expression arg) { if (wr is BuilderSyntaxTree stmtContainer) { ExprBuffer buffer = new(null); - EmitExpr(arg, false, new BuilderSyntaxTree(buffer), wr); + EmitExpr(arg, false, new BuilderSyntaxTree(buffer, this), wr); stmtContainer.Builder.Print(buffer.Finish()); } else { throw new InvalidOperationException("Cannot print outside of a statement container: " + currentBuilder); @@ -926,7 +1001,7 @@ protected override void EmitReturn(List outParams, ConcreteSyntaxTree wr protected override ConcreteSyntaxTree CreateLabeledCode(string label, bool createContinueLabel, ConcreteSyntaxTree wr) { if (wr is BuilderSyntaxTree stmtContainer) { var labelBuilder = stmtContainer.Builder.Labeled((createContinueLabel ? "continue_" : "goto_") + label); - return new BuilderSyntaxTree(labelBuilder); + return new BuilderSyntaxTree(labelBuilder, this); } else { throw new InvalidOperationException(); } @@ -953,7 +1028,7 @@ protected override void EmitContinue(string label, ConcreteSyntaxTree wr) { } protected override void EmitYield(ConcreteSyntaxTree wr) { - throw new UnsupportedFeatureException(Token.NoToken, Feature.Iterators); + AddUnsupportedFeature(Token.NoToken, Feature.Iterators); } protected override void EmitAbsurd(string message, ConcreteSyntaxTree wr) { @@ -980,7 +1055,7 @@ protected override ConcreteSyntaxTree EmitIf(out ConcreteSyntaxTree guardWriter, var containingBuilder = statementContainer.Builder; if (elseBuilderStack.Count > 0 && elseBuilderStack.Peek().Item2 == statementContainer.Builder) { var popped = elseBuilderStack.Pop(); - statementContainer = new BuilderSyntaxTree(popped.Item1); + statementContainer = new BuilderSyntaxTree(popped.Item1, this); containingBuilder = popped.Item2; } @@ -989,8 +1064,8 @@ protected override ConcreteSyntaxTree EmitIf(out ConcreteSyntaxTree guardWriter, elseBuilderStack.Push((ifBuilder.Else(), containingBuilder)); } - guardWriter = new BuilderSyntaxTree(ifBuilder); - return new BuilderSyntaxTree(ifBuilder); + guardWriter = new BuilderSyntaxTree(ifBuilder, this); + return new BuilderSyntaxTree(ifBuilder, this); } else { throw new InvalidOperationException(); } @@ -999,7 +1074,7 @@ protected override ConcreteSyntaxTree EmitIf(out ConcreteSyntaxTree guardWriter, protected override ConcreteSyntaxTree EmitBlock(ConcreteSyntaxTree wr) { if (wr is BuilderSyntaxTree statementContainer) { if (elseBuilderStack.Count > 0 && elseBuilderStack.Peek().Item2 == statementContainer.Builder) { - return new BuilderSyntaxTree(elseBuilderStack.Pop().Item1); + return new BuilderSyntaxTree(elseBuilderStack.Pop().Item1, this); } else { return wr.Fork(); } @@ -1010,44 +1085,47 @@ protected override ConcreteSyntaxTree EmitBlock(ConcreteSyntaxTree wr) { protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string endVarName, List body, LList