Feat: Rust operators and immutable collections #5081

MikaelMayer · 2024-02-13T00:04:12Z

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.

Dafny clone more generic Test for native array pointers

Ensure formatting only consider the opened file

Added Rust Fun AST

Functions in Rust

# Conflicts: # Source/DafnyCore/AST/Grammar/IndentationFormatter.cs # Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs

Added multisets

Pretty-print the ! (==) and all the other operators are now supported

Rust AST for many expressions Detection of unimplemented features Code review Rewriting of a few Rust AST to make them more appealing Support for operators, it compiles

robin-aws

Okay I'm ready to ship, with just two blocking comments:

The remaining compileName += $"({why})"; without failing compilation (and any others I didn't catch), since that means emitting bad code without failing the pipeline by default.
The point about using options.Get instead of adding another flag to the legacy options implementation (weaker but should be a quick fix).

I still don't feel like I've give the core code generation logic in Dafny enough of a review, but I think that can be backfilled before marking the backend stable.

robin-aws · 2024-04-16T17:55:50Z

Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs

+          if (!isTpSupported(typeArg.Formal, out var why)) {
+            compileName += $"({why})";


Another case of emitting bad code without emitUncompilableCode.

I'd strongly suggest using compiler.AddUnsupported instead now that you have it, so it's harder to make this mistake.

robin-aws · 2024-04-16T17:58:10Z

docs/DafnyRef/integration- rust/IntegrationRust.md

+  cargo.toml
+```
+
+With `dafny translate`, only `program-rust/src/program.rs` is emitted.


Just FYI, note this is debatably not correct: #5203

Yep indeed, will have to fix it separately.

docs/DafnyRef/integration- rust/IntegrationRust.md

robin-aws · 2024-04-16T18:00:58Z

docs/DafnyRef/integration- rust/IntegrationRust.md

+- Function parameters always take primitive types without borrowing them (`bool`, `u32`, etc.) 
+- Function parameters always borrows variables of other types (`DafnyString`, structs, etc.), because
+  borrowing is always cheaper than cloning for non-Copy types.  
+  Open question: There are at least two more alternatives make


Source/TestDafny/MultiBackendTest.cs

robin-aws · 2024-04-16T20:02:12Z

Source/DafnyCore/Backends/DafnyExecutableBackend.cs

@@ -11,14 +11,17 @@ namespace Microsoft.Dafny.Compilers;

 public abstract class DafnyExecutableBackend : ExecutableBackend {

+  protected virtual bool PreventShadowing => true;
+  protected virtual bool SupportsUncompilableCode => true;


nit: reads like "can compile uncompilable code" but I think we want a shorter version of "supports outputting partial code for programs that have uncompilable code"

Renamed to CanEmitUncompilableCode

robin-aws · 2024-04-16T20:14:13Z

Source/DafnyCore/DafnyOptions.cs

@@ -360,6 +360,7 @@ public enum ContractTestingMode {
    public int DeprecationNoise = 1;
    public bool VerifyAllModules = false;
    public bool SeparateModuleOutput = false;
+    public bool EmitUncompilableCode { get; set; }


options.Get(CommonOptionBag.EmitUncompilableCode) is the incantation you're looking for. :)

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>

This reverts commit ff40edc.

…afny into feat-rust-operators

robin-aws

🚀 🦀

Rocket craaaaaaaaab, burning out his fumes out here alone...

…)" This reverts commit 3e38580.

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

### 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 <salkeldr@amazon.com>

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 <salkeldr@amazon.com>

MikaelMayer added 30 commits December 21, 2023 15:14

Added initial tests to support allocation

0628309

Implemented codatatypes

7649600

Sequences now defined. Only need to define more methods

06c65ba

Support for traits and mutable variables without dynamic dispatch(?)

5fc5bf4

Arguments always borrowed, deallocation more general now

b72cec9

Conversion to/from Rust strings, better handling of is_string

c2f8b24

Dafny clone more generic Test for native array pointers

Got rid of DafnyClone

bed8f90

Immutable lazy maps

79f1503

Support to subtype testing

4b0fae7

Make sure StreamReaders are closed after use

754022c

Formatting fix 2

22a2897

Ensure formatting only consider the opened file

Needed to updated GeneratedFromDafny apparently

ae3081c

Aligning with existing runtime

705b1ca

More idiomatic rust identifiers, started to deal with indentation

13defc6

Allow dead code + finished all trivial impl

ded93a3

Added standard library

70e1dcf

Added Rust Fun AST

Support for subset of standard libraries

6c6236a

Functions in Rust

much better Rust output

aa3e84a

Proof that ID encoding is bijective so that there is no collision

eccae5e

Constant initialization for datatypes and tests with closures

5ba5c93

Merge branch 'master' into feat-rust

c7fb7c0

# Conflicts: # Source/DafnyCore/AST/Grammar/IndentationFormatter.cs # Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs

Fixed the merge build

770da14

Set and print

70732a7

Ongoing work

b09c1a0

Ensure we don't mess up with the system

21a0074

Added multisets

Fixed the build

a2ef3f8

Better reporting

9704661

Simplified a bit

58229de

Removed useless interfaces in lib.rs

43c60ae

Pretty-print the ! (==) and all the other operators are now supported

Newtype decls now fully erase, support for 128 bit operations

ec7188a

Rust AST for many expressions Detection of unimplemented features Code review Rewriting of a few Rust AST to make them more appealing Support for operators, it compiles

Merge branch 'master' into feat-rust-operators

9fa45e9

robin-aws mentioned this pull request Apr 16, 2024

Document minimum requirements for compiled code in each language #1983

Open

robin-aws reviewed Apr 16, 2024

View reviewed changes

MikaelMayer and others added 10 commits April 17, 2024 09:03

Update docs/DafnyRef/integration- rust/IntegrationRust.md

b08160e

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>

Review comments

7a1112b

Merge branch 'master' into feat-rust-operators

428edc1

formatting

ff40edc

Revert "formatting"

628f55b

This reverts commit ff40edc.

Fixed the format command.

dc3e8eb

Fixed CI Tests

bd632f5

Merge branch 'master' into feat-rust-operators

04f055e

emitUncompilableCode using the new CLI option format

1adb784

Merge branch 'feat-rust-operators' of https://github.com/dafny-lang/d…

4b9323e

…afny into feat-rust-operators

robin-aws previously approved these changes Apr 17, 2024

View reviewed changes

MikaelMayer added 2 commits April 19, 2024 09:59

Merge branch 'master' into feat-rust-operators

0787071

Merge branch 'master' into feat-rust-operators

d160b19

MikaelMayer enabled auto-merge (squash) April 19, 2024 15:19

MikaelMayer and others added 2 commits April 25, 2024 16:55

Merge branch 'master' into feat-rust-operators

94060a0

Addressing CI failures

ea057e3

MikaelMayer dismissed robin-aws’s stale review via ea057e3 April 26, 2024 16:03

Missing check files

71f9e96

MikaelMayer mentioned this pull request Apr 26, 2024

Chore rust operators followup #5373

Closed

robin-aws approved these changes Apr 26, 2024

View reviewed changes

MikaelMayer merged commit 3e38580 into master Apr 26, 2024
20 checks passed

MikaelMayer deleted the feat-rust-operators branch April 26, 2024 17:09

keyboardDrummer added a commit to keyboardDrummer/dafny that referenced this pull request Apr 29, 2024

Revert "Feat: Rust operators and immutable collections (dafny-lang#5081…

d50f957

…)" This reverts commit 3e38580.

MikaelMayer mentioned this pull request Apr 29, 2024

Feat rust operators #5380

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Feat: Rust operators and immutable collections #5081

Feat: Rust operators and immutable collections #5081

MikaelMayer commented Feb 13, 2024 •

edited

Loading

robin-aws left a comment

robin-aws Apr 16, 2024

robin-aws Apr 16, 2024

MikaelMayer Apr 17, 2024

robin-aws Apr 16, 2024

robin-aws Apr 16, 2024

MikaelMayer Apr 17, 2024

robin-aws Apr 16, 2024

robin-aws left a comment

		if (!isTpSupported(typeArg.Formal, out var why)) {
		compileName += $"({why})";

Feat: Rust operators and immutable collections #5081

Feat: Rust operators and immutable collections #5081

Conversation

MikaelMayer commented Feb 13, 2024 • edited Loading

Description

How has this been tested?

robin-aws left a comment

Choose a reason for hiding this comment

robin-aws Apr 16, 2024

Choose a reason for hiding this comment

robin-aws Apr 16, 2024

Choose a reason for hiding this comment

MikaelMayer Apr 17, 2024

Choose a reason for hiding this comment

robin-aws Apr 16, 2024

Choose a reason for hiding this comment

robin-aws Apr 16, 2024

Choose a reason for hiding this comment

MikaelMayer Apr 17, 2024

Choose a reason for hiding this comment

robin-aws Apr 16, 2024

Choose a reason for hiding this comment

robin-aws left a comment

Choose a reason for hiding this comment

MikaelMayer commented Feb 13, 2024 •

edited

Loading