Feat rust externs subsets eta names tests #5613

MikaelMayer · 2024-07-10T14:15:17Z

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.

…onym types and UTF8 char literals.

…clarations.

…ppropriate Fixed support for "this" and constants in reference counting mode. Removed old obsolete class implementations Added all tuples till 16 with a script Support for arrays with 16 dimensions Feature classes and arrays Added documentation about target type Full feat rust Support for Reference counted pointers everywhere. Fixed self type for datatypes vs classes Fixed detection of uninitialized reference counted array Fixed an issue about elseBranch's statements being in the wrong fork. No reading of objects, only borrows Assertion fixed fixup for feat-rust-classes: Nightly crimes no longer printing anything

…, loops & quantifiers, datatype fields ownership, fixed cloning of closed lambda objects, fixed coercion problems Fixup for feat-rust-loops

… correctly.

…names escaped reserved names: {s,S}elf become r#_{s,S}elf rather than r#{s,S}elf + removed them from reserved_rust

Fixup feat-rust-traits expected test fixup traits - no full qualifier for methods if not necessary

…ctions members in datatypes, reserved names - PartialEq, Eq, and Default traits not implemented when datatype contains non-equatable types - note: PartialEq does not have to be manually implemented for parameterized types - note: Auto-generated implementations of Hash constrain type arguments to be subtypes of DafnyType, not DafnyTypeEq - Implementations of fmt_print write "<function>" for members of function type - Implementations of hash ignore members of function type datatypes: style fixes reserved names: destructors containing reserved field names avoid field punning

…ironment closures owned

… memory leaks with MIRI

… function outputs

…panic

fixup extern: ExternCompanion fixup externs: Ensure it works for traits as well. Test for the compilation error Fixup external classes test Fixup external classes when no conflict + documentation Ensure order of imports is deterministic and alphabetic Fixup advanced externs and patterns Fixup: no emitting pub use extern if everything is defined. Fixed field change Fixup externs Fixup externs: Ensure the default class decl does not need the extern attribute Fixup externs fixup externs: Classes are extern means their implementation must be provided externally Function externs correctly have their full extern path

… in quantifiers Fixup init value for synonym types

…lambdas functions: more robust eta-expansion

constants: test to make sure constant lambdas are compiled properly (eta-expanded and type-annotated)

…evel and value-level (variables, etc.) names differently, the latter accounting for reserved fields

…les in scope - desugaring of elephant operator now declares and initializes head variable after error handling - as a result, code generation avoids declaring the head variable - the old type system now avoids duplicating the head variable in scope - NB: the new type system does not have this fix yet b/c by changing the declaration order of the head variable, a resolver invariant is broken

…e, conversions, etc. Items and map no longer requires V to have Eq trait

…ithub.com/dafny-lang/dafny into feat-rust-externs-subsets-eta-names-tests

robin-aws

And the rest!

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs

robin-aws · 2024-08-21T21:37:43Z

Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs

(out of scope but top of mind) For the next PR, let's put a banner that says something like "all contents subject to change except for..." and define exactly the scope of symbols non-Dafny generated code is allowed to refer to.

robin-aws · 2024-08-21T21:46:43Z

Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs

@@ -441,38 +441,6 @@ mod tests {
        assert_eq!(Rc::strong_count(&x_copy.data), 1);
    }

-    #[test]


Were these just dropped or moved somewhere else?

Just dropped because we don't wrap classes with box anymore and we won't support it in the near-term.

robin-aws · 2024-08-21T21:48:24Z

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs

+              //   print "Left:"
+              //   print _e0;
+              //   print "Right:"
+              //   print _e1;


nit: should \n as well (the actually implementation does)

robin-aws · 2024-08-21T21:52:14Z

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs

-            EmitExpr(negated, false, guardWriter, wStmts);
-            EmitHalt(s.Tok, s.Message, bodyWriter);
+            if (
+              Options.Get(CommonOptionBag.Verbose) &&


I think it would be great to enable this unconditionally, personally. Just getting a source location and "expectation violation" is often very unhelpful, and most tests don't bother with a second argument to expect to help describe the failure.

As we discussed, I enabled it unconditionally, but only for the Rust backend since printing is not doing its expected job in other backends.

robin-aws · 2024-08-21T22:02:22Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/continue.dfy

@@ -0,0 +1,38 @@
+// NONUNIFORM: Temporary development of the Rust compiler


I'd replace these comments with something like "rust-specific tests". Otherwise I can just imagine finding this "Temporary" years later and being just a bit embarrassed. :)

Nothing wrong with having some tests written for specific backends - we still have c++ tests after all.

Although we should also follow up with running these tests on all backends with %testDafnyForEachCompiler soon, as that will check that Rust behaves consistently. We can run all rust tests with and without --raw-pointers just as we run all C# tests with and without --include-runtime

Just on top of my mind, it occurs to me that, whenever we run a Rust test, I believe it fetches all dependencies directly from the internet. The target folder weights 1.5Gb every time. This worries me for the CI capacity but I don't know if we can do something about it.

I probably don't want to run tests with the two possible option values for --raw-pointers, because most tests don't have pointers, so that would be wasting CI resources.
But I'll replace temporary with something more appropriate

robin-aws · 2024-08-21T22:06:53Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/externalclasses.dfy

+  }
+}
+
+module Dafny.FileIO {


If this implementation is working, why not move it to the actual DafnyStandardLibraries?? (Can be in a follow-up PR for sure, but worth prioritizing)

This is only a mock implementation of Dafny.FileIO. The extern actually don't read the file system. But it gives an idea on how to achieve that. Let's think of a proper standard library in an upcoming PR.

robin-aws · 2024-08-21T22:07:49Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/externalclasses.rs

+  pub mod FileIO {
+    pub fn INTERNAL_ReadBytesFromFile(path: &::dafny_runtime::DafnyString)
+      -> ::dafny_runtime::DafnyString {
+      return ::dafny_runtime::string_of("Everything is ok.");


Ah damn, never mind :) (would still love to fill in the real thing ASAP though)

robin-aws · 2024-08-21T22:08:35Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/nestedmodules.dfy

+// NONUNIFORM: Temporary development of the Rust compiler
+// RUN: %baredafny run --target=rs "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// RUN: %OutputCheck --file-to-check "%S/nestedmodules-rust/src/nestedmodules.rs" "%S/nestedmodules.check"


Deserves a comment as to what the CHECK pattern is checking

// Checks that, despite module B being prefixed with A, there will be a "mod B" somewhere // and not an encoding like "mod A_B". // This module will automatically be in mod A and referred to as "A::B"

robin-aws · 2024-08-21T22:19:29Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/autoinit.dfy.expect

@@ -0,0 +1,3 @@
+
+Dafny program verifier finished with 2 verified, 0 errors
+(0,-1): Error: Microsoft.Dafny.UnsupportedInvalidOperationException: Creation of object of type Test<Positive> requires a constructor


kbuaaaaaa · 2024-08-23T14:41:09Z

Hi! Sorry to bother but the fuzzers started running when this PR got synced and they all tripped on this:

Code:
Anything
Command:
dafny run/build/translate
Output:
Error: --raw-pointers can only be used after --target:rs or -t:rs

Not sure if this is something you intended to do.

robin-aws · 2024-08-23T22:45:08Z

@kbuaaaaaa Thanks for the heads up! As it happens the CI caught this too just fine. Would it be worth having the fuzzer integration only run when the CI for a PR is green first, or at least check the CI results if fuzzing fails?

Source/DafnyCore/Options/CommonOptionBag.cs

robin-aws · 2024-08-23T22:43:06Z

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs

+            // For now, this code prints nicely only in the Rust code generator until we make it work for every code generator
+            var specialExpectEqualHandling = Options.Backend.TargetId == "rs";


Happy with this for now, but can you cut an issue linked to #5561 to track this? At a minimum I'd like to tweak the output format a little too.

Here is the issue.
#5720
However, I'm not sure I should track it to the Dafny-to-Rust code generator since it's not related.

kbuaaaaaa · 2024-08-23T23:37:36Z

@kbuaaaaaa Thanks for the heads up! As it happens the CI caught this too just fine. Would it be worth having the fuzzer integration only run when the CI for a PR is green first, or at least check the CI results if fuzzing fails?

Thank you for the feedback! Just checked the CI and you’re right. It is definitely more resource efficient to wait for the CI first before fuzzing in this case.

PR has been fully reviewed

Co-authored-by: Robin Salkeld <[email protected]>

robin-aws

🦀 🎉 🦀 🎉 🦀 🎉 🦀 🎉 🦀

MikaelMayer and others added 30 commits June 24, 2024 12:46

feat-rust-synonymtype-charliterals Feat: Added support for erased syn…

b8b7788

…onym types and UTF8 char literals.

feat-rust-maybeuninit-out-vars: Feat: MaybeUninit for out variable de…

cf95ebd

…clarations.

feat-rust-for-loops: Feat: Rust for loops

2a42759

feat-rust-boundedpool-loops: MapBoundedPool domain, map builder fixed…

e3e1e2d

…, loops & quantifiers, datatype fields ownership, fixed cloning of closed lambda objects, fixed coercion problems Fixup for feat-rust-loops

feat-rust-borrowing-calls: Ensure borrowing of first argument is done…

7e3346b

… correctly.

feat-rust-dafny-test: Support for dafny test

1e60595

feat-rust-reserved-names: construction of Rust structs now has field …

0ffa0c2

…names escaped reserved names: {s,S}elf become r#_{s,S}elf rather than r#{s,S}elf + removed them from reserved_rust

feat-rust-traits: Support for traits, constructors, classes, self type

e107306

Fixup feat-rust-traits expected test fixup traits - no full qualifier for methods if not necessary

feat-rust-native-fix: Fixed owned conversion for newtypes

67a050f

feat-rust-coercion-upcast-downcast: Coercion for upcast/downcast, env…

ff611ed

…ironment closures owned

feat-rust-fixup-hash-sequences-miri: Loosen Hash for sequences, fixed…

61527d7

… memory leaks with MIRI

feat-rust-object-variance: Covariance and invariance on datatypes and…

203b8da

… function outputs

Back-ported fix from #5574

a7fde0e

Fixup: Function's Hash on datatypes

bb2ca4d

Fixup: Removed merge conflict in mod.rs

2adb014

Fixup: Non-overriden Destructor name not overriding existing one

351f38e

arrays and usize

73b3561

MAybeuninit fix: Function by method's return statement is correct.

5082cb5

fixup traits: Correct paths when method names contain special characters

7a42ea3

fixup classes: Avoid soundness issue with raw pointers + unreachable …

6ebdce7

…panic

feat-rust-subset-constraints: Support for compiled subset constraints…

fe888e0

… in quantifiers Fixup init value for synonym types

functions: eta-expansion of top level functions and correct type for …

bd46d20

…lambdas functions: more robust eta-expansion

constants: function constants are eta-expanded with an additional call

aafca78

constants: test to make sure constant lambdas are compiled properly (eta-expanded and type-annotated)

reserved names: refactoring of name escaping to handle module-/type-l…

acdda1f

…evel and value-level (variables, etc.) names differently, the latter accounting for reserved fields

fix-maps-issues: Fixed several issues regarding maps, datatype erasur…

e196ed0

…e, conversions, etc. Items and map no longer requires V to have Eq trait

maps: special field .Items now implemented

3c235a6

Merge branch 'feat-rust-externs-subsets-eta-names-tests' of https://g…

5d90e60

…ithub.com/dafny-lang/dafny into feat-rust-externs-subsets-eta-names-tests

robin-aws reviewed Aug 21, 2024

View reviewed changes

Review comments

9cbfe25

Fixed the check for --raw-pointers

4a4cc38

MikaelMayer requested a review from robin-aws August 23, 2024 21:10

MikaelMayer added 2 commits August 23, 2024 16:48

Removing undefined behavior

34091f7

Fixed rust tests

a0265d8

robin-aws previously approved these changes Aug 23, 2024

View reviewed changes

Update Source/DafnyCore/Options/CommonOptionBag.cs

eccadb1

Co-authored-by: Robin Salkeld <[email protected]>

MikaelMayer dismissed robin-aws’s stale review via eccadb1 August 26, 2024 13:32

MikaelMayer mentioned this pull request Aug 26, 2024

expect statements to print more user-friendly outputs #5720

Open

MikaelMayer added 3 commits August 26, 2024 09:58

Merge branch 'master' into feat-rust-externs-subsets-eta-names-tests

d662e3f

Fixed a test case

c6d477d

Updated DCOMP

d5a7743

dnezam mentioned this pull request Aug 30, 2024

Dafny IR contains singleton tuples when compiling pair with ghost #5739

Open

MikaelMayer and others added 4 commits September 3, 2024 14:50

Ability to run one test with the makefile

618131a

Fixed a CI test

a31cd03

Regenerated C# files

fc2de36

Merge branch 'master' into feat-rust-externs-subsets-eta-names-tests

4323517

MikaelMayer enabled auto-merge (squash) September 3, 2024 19:58

MikaelMayer and others added 3 commits September 3, 2024 15:11

Added missing makefile

5405773

Removed outdated tests in the Rust runtime

354e19b

Merge branch 'master' into feat-rust-externs-subsets-eta-names-tests

a20aafa

robin-aws approved these changes Sep 4, 2024

View reviewed changes

MikaelMayer merged commit c9fe1be into master Sep 4, 2024
22 checks passed

MikaelMayer deleted the feat-rust-externs-subsets-eta-names-tests branch September 4, 2024 15:33

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Feat rust externs subsets eta names tests #5613

Feat rust externs subsets eta names tests #5613

MikaelMayer commented Jul 10, 2024

robin-aws left a comment

robin-aws Aug 21, 2024

robin-aws Aug 21, 2024

MikaelMayer Aug 22, 2024

robin-aws Aug 21, 2024

robin-aws Aug 21, 2024

MikaelMayer Aug 23, 2024

robin-aws Aug 21, 2024

MikaelMayer Aug 22, 2024

MikaelMayer Aug 22, 2024

robin-aws Aug 21, 2024

MikaelMayer Aug 22, 2024

robin-aws Aug 21, 2024

robin-aws Aug 21, 2024

MikaelMayer Aug 23, 2024

robin-aws Aug 21, 2024

kbuaaaaaa commented Aug 23, 2024 •

edited

Loading

robin-aws commented Aug 23, 2024

robin-aws Aug 23, 2024

MikaelMayer Aug 26, 2024

kbuaaaaaa commented Aug 23, 2024

robin-aws left a comment

		@@ -0,0 +1,38 @@
		// NONUNIFORM: Temporary development of the Rust compiler

		@@ -0,0 +1,3 @@

		Dafny program verifier finished with 2 verified, 0 errors
		(0,-1): Error: Microsoft.Dafny.UnsupportedInvalidOperationException: Creation of object of type Test<Positive> requires a constructor

		// For now, this code prints nicely only in the Rust code generator until we make it work for every code generator
		var specialExpectEqualHandling = Options.Backend.TargetId == "rs";

Feat rust externs subsets eta names tests #5613

Feat rust externs subsets eta names tests #5613

Conversation

MikaelMayer commented Jul 10, 2024

Description

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kbuaaaaaa commented Aug 23, 2024 • edited Loading

robin-aws commented Aug 23, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kbuaaaaaa commented Aug 23, 2024

robin-aws left a comment

Choose a reason for hiding this comment

kbuaaaaaa commented Aug 23, 2024 •

edited

Loading