Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix: Factorization of all paths in the generated Rust AST #5757

Merged
merged 33 commits into from
Sep 17, 2024

Conversation

MikaelMayer
Copy link
Member

@MikaelMayer MikaelMayer commented Sep 6, 2024

Fixes #5755

Description

  • This PR refactors the Rust-to-Rust path simplification phase that makes absolute paths relative, so that the visiting/replacing phase is separate from the actual collection of data and the replacement itself.
    • Since the new type system does not yet support the dfyconfig.toml of DafnyCore, I'm using the old one.
    • Instead of a trait to encode the visitor pattern, I designed a datatype whose fields are the methods to override.
  • I removed all but one occurrences of R.RawExpr() (and the remaining one has an empty string in argument) so that now the entire tree is correctly searchable/replaceable.
  • I piggy-backed on the new architecture to move away the Optimization in a separate phase easier to maintain
    • Removed Height() function and special decreases clause on Expression.ToString(). The optimization being bottom-up in a separate phase, there is no more need for a special decreases clause to verify that ToString() finishes, when it was doing optimizations at the same time. Also, reduces maintenance burden and potential issues.
  • C# Runtime Because I am using lambdas, I need to depend on some of the C# Runtime's extensions; However, the Runtime is already included in DafnyCore but FuncExtensions is internal; having twice the same type is not possible. To fix that, I made FuncExtensions public, and only emitted for arity 16 and above if the runtime is linked.
  • New Dafny AST node: Primitive.Native; Any number type that can be used to normally index an array. Before that, there was a compilation issue that would arise only if expressions were not simplified, regarding the conversion of integer literals to "usize" in Rust. (it would convert 0 to a DafnyInt, and then truncate it to a u64, but u64 is not necessarily usize)
  • Path.MSels to create a path from a list of Rust identifiers, and SplitRustPathElement that takes care of splitting extern identifiers along ::, to ensure that if a module is named through an extern A::B, we don't end up having use Enclosing::A::B; and a usage like A::B::function() + ambiguities for potential other Bs in scope, but instead B::function() and avoidance of ambiguities.

How has this been tested?

  • I separated the coverage tests from the path simplification tests, so that they can be run separately
  • Path simplification tests were augmented to ensure it works on complex expressions as well as macros.
  • Existing tests should pass

What's next?

I can't wait to refactor RAST into its own file.

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

@MikaelMayer MikaelMayer added the run-integration-tests Forces running the CI for integration tests even if the deep tests fail label Sep 16, 2024
Copy link
Contributor

@ssomayyajula ssomayyajula left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Approved, thanks for taking out RawExpr and Height.

@MikaelMayer MikaelMayer merged commit cc73a34 into master Sep 17, 2024
22 checks passed
@MikaelMayer MikaelMayer deleted the fix-5755-simplify-paths branch September 17, 2024 19:09
MikaelMayer added a commit that referenced this pull request Oct 29, 2024
…romDafnyPost.py instead (#5860)

### Description
#5757 made `FuncExtensions` in the C# runtime public instead of
internal, which is not ideal since it increases the API surface area of
the runtime and is a one-way door (and causes false positives in
prerelease regressions testing). It was done because it seemed to be
necessary, but the actual root cause was dropping these extension
methods when post-processing Dafny's output. This PR reverts the change
and special-cases the class in the python script instead.

### How has this been tested?
Existing tests.

<small>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).</small>

---------

Co-authored-by: Mikael Mayer <[email protected]>
MikaelMayer added a commit that referenced this pull request Oct 30, 2024
…romDafnyPost.py instead (#5860)

### Description
#5757 made `FuncExtensions` in the C# runtime public instead of
internal, which is not ideal since it increases the API surface area of
the runtime and is a one-way door (and causes false positives in
prerelease regressions testing). It was done because it seemed to be
necessary, but the actual root cause was dropping these extension
methods when post-processing Dafny's output. This PR reverts the change
and special-cases the class in the python script instead.

### How has this been tested?
Existing tests.

<small>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).</small>

---------

Co-authored-by: Mikael Mayer <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
run-integration-tests Forces running the CI for integration tests even if the deep tests fail
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Dafny-to-Rust code generation is not simplifying all paths
2 participants