Updating coroutines branch #5772

ssomayyajula · 2024-09-16T18:23:08Z

Description

How has this been tested?

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

### Description This PR changes how the language server unit tests execute, retrying them up to three times if they fail. Ultimately, this is what we're doing by hand, anyway, so we might as well automate it. The proper solution to this problem is to ensure that the language server tests don't spuriously fail, but this will accelerate our development process in the meantime. ### How has this been tested? By running CI normally. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

### Description This is a refactoring-only PR intended to make implementing [`decreases to`](#5252) more straightforward when we do it. ### How has this been tested? With the existing test suite, as it's purely a refactoring. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

### Description Adds a first pass of proof obligation description expressions, towards resolving #2987. It also adds a new hidden option, `--show-proof-obligation-expressions`, which adds to each (supported) failed proof obligation error message an equivalent Dafny assertion. This option is used to automate tests for the newly added proof obligation description expressions, but this PR does not backfill tests for existing PODesc expressions. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --------- Co-authored-by: Aaron Tomb <[email protected]>

This PR changes the remaining 5 of the 10 `dafny0/ResolutionErrors*.dfy` tests so that they test not only the legacy resolver, but also the resolver refresh. * fix: Remove `this` from the scope when resolving `static const` fields * fix: Remove `this` from the scope when resolving type constraints and type witnesses * Adjust tests and expected output for `dafny0/ResolutionErrors[45679].dfy` * Add test for for unary TLA-style expressions (these worked, but did not have specific tests) * chore: Remove `TernaryExpr.PrefixEqUsesNat`, which wasn't needed ### Regression The one place where the new type inference was not able to do as well as the old is the code snippet ``` dafny var c := d; var xx := c[25..50][10].x; ``` from `dafny0/ResolutionErrors4.dfy`. Here, the new resolver does not thread the element type of `d` through the array-to-sequence conversion `c[25..50]`, and therefore the `.x` gives an error. The workaround is to declare the type of `c` explicitly in the code. I don't see a quick fix for this in the type inference. A good improvement, which I believe would also fix this problem, is to do member resolution (like `.x`) lazily instead of eagerly. This would allow the type-inference machinery to start making some decisions, which will lead to it figuring out a type for `c`, after which types for the other expressions, including the `.x`, can be inferred. I would love to see this improvement in the type inference, and the new resolver has "guarded constraints" that exist in order to lazy inference. However, such a change will take some effort, because the methods that currently try to do member lookup too easily generate errors (rather than saying "please try again later"). Such a change is out of scope for this PR. 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).

### Description The previous implementation had two issues: * It displayed only the milliseconds portion of the duration, so would be incorrect for any verification lasting longer than a second. * The use of exponential notation for resource count made it more difficult to compare values, and impossible to identify small differences. This also changes the overall format of the message slightly. ### How has this been tested? Existing tests have been updated to reflect the changes in formatting. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

Build against the newer GoLang 1.22, since the download for 1.15 seems to have been taken down 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).

### Description - Refactoring: let `Method` and `Function` share the field `Ins` (for inputs) and the related property `HasPreconditions`, using the class `MethodOrFunction`. - Do not refer to auditor code when building a Dafny library - Previously, using `{:termination false}` in a library was not allowed, but after this PR it is. I believe it should be allowed, since currently there is no workaround. - For all "auditor assumptions" that had `allowedInLibraries: false`, there were existing warnings for: - assume without `{:axiom}` - forall without a body - loop without a body - functions or methods without a body - usage of `{:only}` - For the other "auditor assumptions", new warnings have been added. - Emit a warning when `{:verify false}` is used - Emit a warning when exporting a declaration that has requires clauses or subset type inputs - Emit a warning when importing a declaration that has ensures clauses or subset type outputs - Add an option `--allow-external-contracts` that silences the previous two warnings. - Add warning for bodyless functions marked with {:extern}, and an option `--allow-external-function` to silence this warning. - I have decided not to warn on `{:assume_concurrent}` without `{:axiom}`, since the `{:assume_concurrent}` attribute is only useful when using `{:concurrent}`, which you would add in a rather late stage anyways. ### How has this been tested? - Updated CLI tests for the new warnings and options 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).

### Description Turning on doofiles/Test4.dfy ### How has this been tested? It's adding a test 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).

### 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 <[email protected]>

This reverts commit 3e38580 to fix failing nightly: https://github.com/dafny-lang/dafny/actions/runs/8868313153 --------- Co-authored-by: Fabio Madge <[email protected]>

### Changes - To enable smoothly working with multiple projects inside a single repository, Dafny now allows using a Dafny project file as an argument to `--library`. This does the following: 1. Call `dafny build -t:lib` using the project file to get a doo file. In the future we plan to let this be a NOOP if the right build file is already there. 1. Replace the usage of the project file in the origin call to `dafny`, with this doo file. - Extract code from `DafnyFile.CreateAndValidate` into methods - When parsing a file, correctly pass parse options to included files. This does not have any particular affect because only doo files are passed with different options, and those do not use includes. However, doing this does seem more correct and it was useful previously, so I'll keep it in. - Move `ReadsClausesOnMethods` option code - Do not let project files include themselves through something like `includes = ["**/*"]` ### How has this been tested? - Add the CLI test `projectAsLibrary.dfy` 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 <[email protected]>

This PR is a replay of #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 <[email protected]>

This reverts commit 44ca1b2. ### Description The recently merged PR #5342 argues that we should automatically retry failing IDE tests, because that's what we manually do anyways. However, we only do that in some cases. Specifically, when any of us make changes that may create unstable tests, such as changes in the IDE, then failing IDE tests should not be retried, manually or automatically. PR5342 makes it so that such a retry happens automatically, thereby making it much easier to introduce non-deterministic bugs either in IDE code or tests. That's why this PR is reverting that one. IMO there is little difference between a test that fails 100% of the time and one that fails <100% of the time. Retrying a failing test that fails <100% of the time is similar to saying "I believe my PR is not at fault for this test failing, please ignore it". A similar situation occurs when a PR gets merged that causes nightly to fail. However then we don't have a way for new PRs to say "please ignore nightly failing", and we explicitly block all PR until nightly is fixed again. A similar approach to unstable tests would be to not to retry failing builds until the instability is resolved, but instead to wait until an instability fix PR is merged. ### How has this been tested? It's a revert. 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).

### Description Remove 'note,' at the start of some warnings ### How has this been tested? Updated expect files 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).

This PR fixes the standard library so that it is compatible with general newtypes. Fixes #5345 ### How has this been tested? I added a verification test for just a small project with a dfyconfig file including the standard library 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: Fabio Madge <[email protected]>

This reverts commit 0b629ea to fix failing nightly: https://github.com/dafny-lang/dafny/actions/runs/8896634004/job/24436389955 Unfortunately I approved #5380 before all of the deep tests had run, and because the extra checks aren't normally run for a PR unless it has the `run-deep-tests` label, they can't be required checks, so the PR was auto-merged even though several Windows runs timed out after 2 hours.

Fixes #5337 ### Description - Add the field `base` to Dafny project files, which allows a project file to inherit fields from another one. Options from the current file override options from the base. Includes from the current file override excludes from the base, and excludes from the current file override includes from the base. The base may itself also have a base. - Small improvements to project file error reporting. See the updates in existing tests for more information. ### How has this been tested? - Added the test `cli/projectFile/base/included.dfy` 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).

### Description Merging from the released 4.6 branch. 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: Remy Willems <[email protected]>

### Description Add more logging to QuickEditsInLargeFile ### How has this been tested? Test logging change, no additional tests needed 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).

### Description Setting up a daily scheduled build to run the LSP tests 5 times on each platform, in an effort to proactively uncover flaky test failures that show up at the worst possible time as you're trying to get your wonderful PR you've been working on for weeks merged or even worse that break the nightly build for the third day in a row forcing the team to drop everything to click Retry Failed Jobs two or three times before ANY PRs can be merged not that I'm frustrated or anything. :) The PR CI was previously running the LSP tests twice every time for the same reason. Given this daily job will soak them more deeply, and that the `osx` unit test job on PRs in particular has been taking almost 45 minutes and becoming the limiting factor, I've opted to just run them once on PRs now. Note that unlike the original double run, it was simpler to use matrices just as we do for integration tests, only in this case just iterating the same test run in parallel 5 times. It's possible running twice on the same runner might trigger more failures, but it seems unlikely since the second run happens in a fresh process and no state leaks between the runs AFAICT. ### How has this been tested? Dry-run on my fork: https://github.com/robin-aws/dafny/actions/runs/8914692810 I've run it a few times without any failures yet, but we'll have to see what happens after a week or so of scheduled runs. 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).

### Description - Fix bug in reporting of time taken when a verification timeout occurs - Make test 3855 stable by redacting the time taken ### How has this been tested? - Fix is not tested - Flaky test is updated 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).

#5386) ### Changes Fix a bug in AwaitNextNotificationAsync that prevented the 'Waited for' log line to show up, to help debug #5384 ### Testing Since this was a bug in the testing code, I'm OK with not testing it. 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).

Fixes #4985 ### Description #### Main Change Options come in several flavors. Some options do not affect the correctness of the program, such as those that affect logging or performance. Other options do affects the semantics. These may be configurable per module, such as `function-syntax`, or they may be 'global', which means the value this has for a dependency affects what value it should have for the dependent, such as `unicode-char` or `allow-warnings`. Previously, options were only marked as global or not, so it was not possible to distinguish between non-semantic options and semantic options that are configurable at the module level. This PR adds registration to make that distinction, and uses that to determine which module level options to track in doo files, which fixes bugs that would occur when using non-default values for these options in combination with doo files. #### Minor changes - Fix a bug that would prevent using Doo files, due to their read stream being disposed before they were fully read. - Add a hidden option `--hidden-no-verify` that allows building doo files without verifying then, as if you had verified them. This is useful for building and committing the standard library without verifying it, which is safe because CI will still build it with verification as well. ### How has this been tested? - Added the test `semanticOptions.dfy` 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).

### Description   This PR adds support for passing `--go-module-name` flag to the translate go command to conform to the Go Module project structure. Example: CLI: `dafny translate go --go-module-name MyModule` It also uses `dtr` files to fetch the right `go-module-name` for dependencies. ### How has this been tested?  Added integration tests which use checked-in DafnyRuntimeGo libs using the `replace` `go.mod` directive. See the `go-module` directory. 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 <[email protected]>

### Description Introduce a new option `--unsafe-dependencies` which is always on for `dafny server` and `dafny resolve`, optionally enabled for `dafny verify`, and off for all other commands. This option only affects compilation when a dependency (--library) is specified using a Dafny project file. In case the option is off, that dependency project is used to build a library file, which is then used as the dependency. In case the option is on, the source files from the dependency project are included but not verified or translated. The goal of this PR is to to enable practical development of Dafny projects where multiple projects that depend on each other live inside a single repository, while not affecting the CI of Dafny projects in any way. ### How has this been tested? - Updated the test projectAsLibrary 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).

UPDATE: The commit 8661eb0 fixed the previous nightly issue that multi-compiler tests on Windows were taking 15x longer. UPDATE: That works only for the ResolvedDesugaredExecutableDafny compiler. Enabling the Dafny-to-Rust compiler again triggers that 15x slowdown. **Do not merge yet** ### 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. - `make pr` now prepares a codebase for a (regenerates everything and reformats everything in the correct order). ### 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).

Includes changes from #5394 ### Description - `ProgramParser.ParseFiles` already was an asynchronous operation, but the parse caching mechanism did not take this into account, so it could start pruning the caching before a parsing run was completed, causing cache entries to be incorrectly pruned, leading to less caching of parsing. The resolution cache depends on GUIDs from the parsing cache to determine cache keys for modules, so this also broke resolution caching. - `PruneIfNotUsedSinceLastPruneCache` was not thread-safe, so doing two use+prune operations concurrently could serialize to a use+use+prune+prune operation, which would incorrectly prune things. - Fix a bug in `ProjectManager` that cause one compilation in a sequence of a compilations for a particular project, to have a crash. - A profiling session showed lots of time going into computing `Count` on `ConcatReadOnlyList`, so that property is now computed just once for such a list. However, this problem really requires more IDE performance tests. - Update included files message ### How has this been tested? - Added a test `ConcurrentCompilationDoesNotBreakCaching` to check that caching work swell when concurrent operations occur - Added a test `DocumentAddedToExistingProjectDoesNotCrash` that checks whether adding documents to an existing project does not cause a compilation to crash. 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 <[email protected]>

…uage server (#5161) ### Description This change will add an interface for plugins to add request handlers to the Dafny language server, which allows plugins to provide more features than just code actions. ### How has this been tested? Test has been added to `DafnyLanguageServer.Test` in a similar way to how a test for `GetDafnyCodeActionProviders()` was added. 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: Mikaël Mayer <[email protected]>

Fixes #5428 ### Description - Revert part of #5243 because this caused complication and it needs better consideration before being done. ### How has this been tested? - Added `ResolutionErrorMigration` to verify #5428 is fixed - Update `CorrectParseDiagnosticsDoNotOverridePreviousResolutionOnes` to account for resolution diagnostics no longer being migrated 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).

### Description Add `--performance-stats` option and use this on the SchorrWaite test ### How has this been tested? Updated `SchorrWaite.dfy` 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).

### Description   ### How has this been tested?  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).

### Description I recently stumbled on this random Mac failure: https://github.com/dafny-lang/dafny/actions/runs/10359400713/job/28675744622?pr=5684 After careful investigation of the stack trace, it looks like the static constructor of `DafnyFile` did not run before `OptionRegistry.CheckOptionsAreKnown(AllOptions);`, resulting in the option `DoNotVerifyDependencies` to not be registered. This PR fixes that by forcing the execution of the static `DafnyFile` constructor, guaranteed to not run if that constructor was already called. https://learn.microsoft.com/en-us/dotnet/api/system.runtime.compilerservices.runtimehelpers.runclassconstructor?view=net-8.0 ### How has this been tested? I can't think of a way this change can be tested, the failure happens extremely rarely. Please make yourself convinced that this PR solves the issue given in the link. 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).

### Description After #5632, Dafny started complaining about traits lacking constructors (which they can't have) when `--enforce-determinism` was enabled. This changes back to the previous behavior of warning only about classes without constructors. ### How has this been tested? Updated `dafny0/ForbidNondeterminismResolve.dfy` to include a trait declaration. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

### Description - Update Boogie to 3.2.4 ### How has this been tested? - Updated test expect files 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).

This PR adds the following language features: * type parameters of `newtype` declarations * optional `witness` clause of constraint-less `newtype` declarations * tool tips show auto-completed type parameters * tool tips show inferred `(==)` characteristics Along the way, the PR also fixes two previous soundness issues: * fix: Check the emptiness status of constraint-less `newtype` declarations (#5520) * fix: Don't let `newtype` well-formedness checking affect witness checking (#5521) Fixes #5520 Fixes #5521 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).

Bumps [rexml](https://github.com/ruby/rexml) from 3.3.3 to 3.3.6. Signed-off-by: dependabot[bot] <[email protected]> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> Co-authored-by: Fabio Madge <[email protected]>

## Description This PR adds a way to extract a Dafny model into set of Boogie declarations. This new feature can be of general use, but its main application is to justify various axioms in Dafny's `DafnyPrelude.bpl` by providing a model for them. ## Impact on the Dafny tool The model for Dafny's underlying type `Seq` is given in `Source/DafnyCore/Prelude/Sequences.dfy`. The file `Source/DafnyCore/DafnyPrelude.bpl` should no longer be edited by hand. Instead, it is now generated from `Source/DafnyCore/Prelude/PreludeCore.bpl` and from the model `Sequences.dfy` (and other models in the future, for example for multisets). To generate a new version of `DafnyPrelude.bpl`, run `make extract` in the `Source/DafnyCore` folder. This will run `make` in the `Source/DafnyCore/Prelude` folder and will then copy the generated `Prelude/DafnyPrelude.bpl` to `DafnyPrelude.bpl`. ## CLI option This PR adds a CLI option `--extract:<file>` (where `<file>` is allowed to be `-` to denote standard output, just like for the various print options). This option works with the `dafny verify` command. Caveats: This gets the job done, but is probably not the best way of doing it. For instance, one could imagine a `dafny extract` command that performs this task. I'm unsure of the code I added to handle this CLI option. In particular, I don't understand if I have added it just for the `dafny verify` command or also for other commands, and I don't understand if I have made the option available via the language server (or if we care). ## Changes to `DafnyPrelude.bpl` This PR contains changes to `DafnyPrelude.bpl`. The claim is that these changes make no semantic difference. The changes are: * differences in whitespace * other changes to format the code like the Boogie `/print` option does (for example, `s: Seq, t: Seq` instead of `s, t: Seq`) * in the `Seq` part of `DafnyPrelude.bpl`, the declarations that are not part of the model in `Sequences.dfy` have been moved to the end, so that the extracted declarations can be in one contiguous part of the file The third of these bullets do change the order in which things are sent to the SMT solver, and thus this may impact some users. ## Extract mechanism Upon successful verification, the new extract mechanism added by this PR will visit the AST of the given program. For any module marked with `{:extract}`, the extract-worthy material from the module is output. The output declarations will be in the same order as they appear textually in the module (in particular, the fact that module-level Dafny declarations are collected in an internal class `_default` has no bearing on the output order). Three kinds of declarations are extract-worthy: * A type declaration `A<X, Y, Z>` that bears an attribute `{:extract_name B}` is extracted into a Boogie type declaration `type B _ _ _;`. The definition of the type is ignored. (The intended usage for an extracted type is that the Dafny program give a definition for the type, which goes to show the existence of such a type.) * A function declaration `F(x: X, y: Y): Z` that bears an attribute `{:extract_name G}` is extracted into a Boogie function declaration `function G(x: X, y: Y): Z;`. The body of the Dafny function is ignored. (The intended usage for an extracted function is that the Dafny program give a definition for the function, which goes to show the existence of such a function.) * A lemma declaration `L(x: X, y: Y) requires P ensures Q` that bears an attribute `{:extract_pattern ...}` or an attribute `{:extract_used_by ...}` is extracted into a Boogie `axiom`. The axiom has the basic form `axiom (forall x: X, y: Y :: P ==> Q);`. If the lemma has an attribute `{:extract_used_by F}`, then the axiom will be emitted into the `uses` clause of the Boogie function generated for Dafny function `F`. If the lemma has no in-parameters, the axiom is just `P ==> Q`. If the lemma has in-parameters, then any attribute `{:extract_pattern E, F, G}` adds a matching pattern `{ E, F, G }` to the emitted quantifier. Also, any attribute `{:extract_attribute "name", E, F, G}` adds an attribute `{:name E, F, G}` to the quantifier. ## Expressions The pre- and postconditions of extracted lemmas turn into analogous Boogie expressions, and the types of function/lemma parameters and bound variables are extracted into analogous Boogie types. The intended usage of the extract mechanism is that these expressions and types do indeed have analogous Boogie types. At this time, only a limited set of expressions and types are supported, but more can be added in the future. Any `forall` and `exists` quantifiers in expressions are allowed to use `:extract_pattern` and `:extract_attribute` attributes, as described above for lemmas. Some extracted expressions are simplified. For example, `true && !!P` is simplified to `P`. ## Soundness The Dafny program that is used as input for the extraction is treated like any other Dafny program. The intended usage of the extraction mechanism is to prove parts of the axiomatization in `DafnyPrelude.bpl` to be logically consistent. Whether or not the extracted Boogie declarations meet this goal depends on the given Dafny program. For example, if the given Dafny program formalizes sequences in terms of maps and formalizes maps in terms of sequences, then the extraction probably does not provide guarantees of consistency. 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).

### Description Previously, the order of modules depended on the ordering of the hashes of instances of ModuleDefinition, which likely depended on run-time addresses. To ensure we generate code deterministically irrespective of run-time addresses, I sort the module definitions by their full name before iterative over them, for the Dafny code generator as it's the only one that might care about it for now. ### How has this been tested? I added a test that was failing without the code change to DafnyCodeGenerator.cs, which tests that modules are emitted alphabetically in Rust. 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).

### Description Merging the release 4.8.0 branch into master It brings several modifications that were deemed necessary - Updated the doo files from the DafnyStandardLibraries, - Updated doo files and dtr files from the test suite - Renamed dfy files for externs so that they are in the same order and don't cause issue as a workaround for #5728 and updated README about the naming of those files - Added %rm %mv and %cp command which are used in tests but not available on every windows machine (mine included) - Added support for any exit code so that `%rm` won't fail if a file or a folder does not exist (which is the case the first time) - Added ability to run a command within a given folder as some commands would not run on my Windows. - Added `-f` option to cp and mv to be able to run the same test multiple times - Added missing sources to recompile multiple doo files in the test suite. ### How has this been tested? Tests are passing on the CI and previously offending tests are also passing on my Windows machine. 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: Aaron Tomb <[email protected]> Co-authored-by: Siva Somayyajula <[email protected]> Co-authored-by: Siva Somayyajula <[email protected]>

### Description This fixes a lot of issues in the Rust compiler, and implements the following features as well: - Support for externs and appropriate documentation - Compiled subset constraints in quantifiers - Eta-expansion of lambdas (Fabio) - Reserved names fixups - Elephant operator fixup (Siva) - Issues with maps in the runtime - special field: map.Items - Type tests - Fix ambiguity in rendering / parsing - Full path use for hashing to avoid ambiguity - Support for type synonyms - Removed of dead code (phantom variants that are useless, upcast for _default classes) - Separation Name vs. Var so that escaping can be different and appropriate - Paths are now shared between types and expressions - Generated code factors some paths in use declarations for debuggability and readability - Generation of Rust code by nested modules instead of encoding with "_d" as the separator of modules - Interop: Ability to create objects given a sized struct - Fixed coercions - *Tested option for raw pointers* with the flag `--raw-pointers` - Documentation for GenTypeContext 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: Siva Somayyajula <[email protected]> Co-authored-by: Fabio Madge <[email protected]> Co-authored-by: Robin Salkeld <[email protected]>

…ssion branch (#5681) I'm putting this PR on hold, since it increases the size of the generated Boogie. Example: https://diff.corp.amazon.com/compare/9ap5cvpm ### Description If the result of an expression does not satisfy the constraints of its context, then an error is reported in the branch of the expression that does not satisfy the context. Effected contexts: - Function postconditions - Witness expressions - Expression default values - Subset type checks for function call arguments - Assignment to a subset type local Example of improved error reporting: ```dafny function ElseError(x: int): int // previous primary error location ensures ElseError(x) == 0 // related error location { if x == 0 then 0 else 1 // new primary error location } function ThenError(x: int): int // previous primary error location ensures ThenError(x) == 0 // related error location { if x == 0 then 1 // new primary error location else 0 } function CaseError(x: int): int // previous primary error location ensures CaseError(x) == 1 // related error location { match x { case 0 => 1 case 1 => 0 // new primary error location case _ => 1 } } function LetError(x: int): int // previous primary error location ensures LetError(x) == 1 // related error location { var r := 3; r // new primary error location } ``` ### How has this been tested? - Added CLI test `ast/functions/ensuresReporting.dfy` - `ast/subsetTypes/errorReporting.dfy` - `ast/expression/functionCall.dfy` - `ast/statement/localAssignment.dfy` 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: Stefan Zetzsche <[email protected]>

Previously, we used list for the children of a verification tree. However, processes might concurrently add to this list and try to make a copy of it, which sometimes triggered issues. By switching to a concurrentbag, these issues should go away. The list of children is not ordered anyway. Fixes #5744 ### Description Not visible by users ### How has this been tested? CI will test that change. 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).

This PR fixes #5643 I added the corresponding test. 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).

### Description This PR contains various fixes in the new resolver, found while preparing Dafny to switch to `--type-system-refresh` as the default. ### How has this been tested? These issues that this PR fixes were found when running the test suite with a version of `dafny` that uses `--type-system-refresh --general-traits=datatype --general-newtypes` by default. However, since not all test files pass with these options, this PR does not change the default options, which also means that the existing tests don't test for the behavior that has been fixed. The purpose of this PR is to get these fixes in as soon as possible (and to make sure they don't break any existing functionality). The full testing will happen in a future PR that changes the default options. 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).

) Fixes #5719 Fixes #5726 ## Description This PR solves both soundness and incompleteness problems related to when a nullable type extends a trait. To fix the soundness issue (#5726), the resolver was changed to check type bounds after type inference. For example, the resolver now generates an error if a nullable reference type `E?` is used as a type argument with a bound `B` that is not a nullable reference type. Note that this check cannot be done completely during pre-type inference, because pre-types don't distinguish between `E?` and `E`; therefore, the definitive check for this is done in the same place where type arguments are checked to have the specified type characteristics (`(==)`, `(0)`, ...). To fix the incompleteness issues (#5719), changes were made in the generated axioms. To describe them, consider the following types: ``` dafny trait RefTrait extends object { } trait GeneralTrait { } // does not extend object, and thus is not a reference type class /* or trait */ E extends RefTrait, GeneralTrait { } ``` * Previously, this generated the following _type axioms_ (and analogous _allocation axioms_ for `$IsAlloc`): ``` boogie // type axiom for trait parent: E extends RefTrait axiom (forall $o: ref :: { $Is($o, Tclass.E?()) } $o != null && $Is($o, Tclass.E?()) // CHANGE: remove o != null ==> $Is($o, Tclass.RefTrait())); // CHANGE: RefTrait --> RefTrait? // type axiom for trait parent: E extends GeneralTrait axiom (forall $o: ref :: { $Is($o, Tclass.E?()) } // CHANGE: replace E? with E $o != null && $Is($o, Tclass.E?()) // CHANGE: remove o != null, and replace E? with E ==> $IsBox($Box($o), Tclass.GeneralTrait())); ``` The new axioms say: ``` boogie // type axiom for trait parent: E extends RefTrait axiom (forall $o: ref :: { $Is($o, Tclass.E?()) } $Is($o, Tclass.E?()) ==> $Is($o, Tclass.RefTrait?())); // type axiom for trait parent: E extends GeneralTrait axiom (forall $o: ref :: { $Is($o, Tclass.E()) } $Is($o, Tclass.E()) ==> $IsBox($Box($o), Tclass.GeneralTrait())); ``` * To make the first of these axioms still be able to connect `E?` with `RefTrait`, the axiom that connects a nullable type `X?` with its non-null reference type `X` was extended with an additional matching pattern: ``` boogie // $Is axiom for non-null type X axiom (forall c#0: ref :: { $Is(c#0, Tclass.X()) } { $Is(c#0, Tclass.X?()) } // CHANGE: this matching pattern was added $Is(c#0, Tclass.X()) <==> $Is(c#0, Tclass.X?()) && c#0 != null); ``` * The property that a type parameter `T` with a bound `B` has is (elsewhere) given as a quantification over boxes. To make this property known of a type that extends a trait, the following axioms were added: ``` boogie axiom (forall bx: Box :: { $IsBox(bx, Tclass.E?()) } $IsBox(bx, Tclass.E?()) ==> $IsBox(bx, Tclass.RefTrait?())); axiom (forall bx: Box :: { $IsBox(bx, Tclass.E()) } $IsBox(bx, Tclass.E()) ==> $IsBox(bx, Tclass.GeneralTrait())); ``` These are essentially box versions of the type axioms above. 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).

Fixes #5749 ### How has this been tested? The CI should pass. 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).

This PR fixes #5647 I added the corresponding test. 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).

This PR fixes #5642 I added the corresponding test. 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).

### Description This PR adds support for pools consisting on one exact element, both for quantifiers (expression version) and collection builders (statement version) ### How has this been tested? I modified an existing test that was no longer passing, and this PR made it to pass 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: Fabio Madge <[email protected]>

This PR increases the Runtime coverage by adding more tests to cover previously uncovered lines. 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).

### Description Allow revealing using a static receiver ### How has this been tested? Added the test `revealQualifiedId.dfy` 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).

### Description   I have modified the fuzzing workflow to handle PR from forks. Fuzzing will only be triggered on PR created by verified contributors to prevent potential security risks. **ALL WILL BE FUZZED** mwahaha This change also fix the following annoying issues: - Reporting bugs already caught by CI: Fuzzing will now be delayed and only run if all CI checks have passed. This is implemented outside of the workflow, the PR will not be blocked. - Reporting non-bugs in Rust: Added pattern matching to ignore error that comes from not yet implemented features in Dafny-to-Rust. (sorry Mikael!) ### How has this been tested? Tested on my own dummy repo  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).

Fixes #5763 Requires the upcoming Boogie version 3.2.5, for which this PR needs to be merged first: boogie-org/boogie#945 ### Description - No longer allow hiding functions from the Dafny prelude by using `hide *`. This affected recursive functions because they use `$LS` which is defined in the prelude. ### How has this been tested? - Added a CLI test-case to `revealFunctions.dfy` 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).

This PR detects all tests and creates adequate equivalent Rust tests in the same file, by calling methods via top-level functions and translating `{:test}` attributes to the equivalent `#[test]` in Rust. Moreover, it translates the `{:test}` annotation on modules to the equivalent `#[cfg(test)]` in Rust, so that it makes it possible to exclude entire modules when not in test mode. I wrote a test that verifies that tests can be executed and that the resulting source code emits `#[cfg(test)]` 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 <[email protected]>

…of two (#5770) Fixes #5753 ### Description I ensures the flaky test does not test for a single diagnostic but for two, and if there are two the two should be timeouts. ### How has this been tested? No tests can be performed on a flaky test but at least it looks like it should prevent the issue since that issue was diagnosed. 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).

### Description - Add opaque blocks to the language ### How has this been tested? - Add the CLI test `opaqueBlock.dfy` 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).

Fixes partially #5641 This PR adds `--rust-module-name` so that all absolute paths from crate insert the given module name after "crate" if the option is provided. ### Description I could have made it a boolean option since it should match the name of the generated file, but by consistency with other backends, I made it so that the option accepts any string. Let me know if you think a boolean would be better. ### How has this been tested? - A test verifies that in the generated source code, the provided module name is correctly inserted. 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 <[email protected]>

atomb and others added 30 commits April 19, 2024 14:01

Revert "Feat: Rust operators and immutable collections (#5081)" (#5377)

ea63179

This reverts commit 3e38580 to fix failing nightly: https://github.com/dafny-lang/dafny/actions/runs/8868313153 --------- Co-authored-by: Fabio Madge <[email protected]>

feat: Translation records (#5346)

2e6938d

keyboardDrummer and others added 28 commits August 16, 2024 10:32

ssomayyajula marked this pull request as ready for review September 16, 2024 18:24

ssomayyajula merged commit c53025d into iterator-exp Sep 16, 2024
4 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Updating coroutines branch #5772

Updating coroutines branch #5772

Uh oh!

ssomayyajula commented Sep 16, 2024

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

15 participants

Updating coroutines branch #5772

Updating coroutines branch #5772

Uh oh!

Conversation

ssomayyajula commented Sep 16, 2024

Description

How has this been tested?

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

15 participants