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

Refactor of the frontend #743

Merged
merged 39 commits into from
Jul 5, 2024
Merged

Refactor of the frontend #743

merged 39 commits into from
Jul 5, 2024

Conversation

W95Psp
Copy link
Collaborator

@W95Psp W95Psp commented Jun 30, 2024

This PR is a "big" refactor, I guess that's my way of killing time on this scary election Sunday in France...

Sorry for the bulky monolithic PR, that's a big refactor thing with a lot of very related changes, that would have been 5 or 10 PRs, that would have been a pain to push and merge.

  • Architecture:
    • cargo-hax now:
      1. calls cargo build, which calls multiple times our custom rustc driver. Instead of running the engine itself or spitting out JSON, the rustc driver now creates a haxmeta file per crate in the target directory (along with rmeta rustc files).
        A haxmeta file is a full CBOR bincode export of the AST of a crate by hax's exporter. It contains all the data we need.
        It also communicates on stderr what haxmeta files have been produced.
        This haxmeta file mechanism respects much more what rustc does itself, allowing us to benefit from the cache of cargo and rustc. Also, we need that mechanism for things like allow trait param with empty predicates #371: with haxmeta files, we will be able to do cross-crate reasoning.
      2. reading the stderr of cargo build, we now what haxmeta files were produced.
      3. we process those haxmeta files, and call the engine
    • The engine is now communicating with cargo-hax with messages (on stdin/stdout). Before, the communication was done with one JSON input payload at the beginning and one JSON payload at the end. Now, the engine can communicate interactively with cargo-hax. This is useful for:
      • dynamic error reporting
      • rustfmt requests
      • diagnostics pretty printing
      • in the future, a nicer debugging tool
    • I removed the crates hax-cli-options, hax-cli-options-engine, and hax-diagnostics.
      • This stratification stems from us thinking we needed some crates to be nightly and some to be stable, that's not the case
      • I merged everything into a hax-types crate, which contains all the types required for communicating between cargo-hax, hax-engine and the custom rustc driver.
  • Minor changes:

The `rustc` feature enables the conversion bridges from rustc types
(and AST) to the ones defined in `hax-frontend-exporter`. Enabling
`rustc` adds a dependency to `librustc_driver`.
Copy link
Member

@franziskuskiefer franziskuskiefer left a comment

Choose a reason for hiding this comment

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

Thanks, only a few nits.

Cargo.toml Outdated Show resolved Hide resolved
Cargo.toml Show resolved Hide resolved
cli/driver/src/exporter.rs Show resolved Hide resolved
cli/subcommands/src/cargo_hax.rs Outdated Show resolved Hide resolved
cli/subcommands/src/cargo_hax.rs Outdated Show resolved Hide resolved
frontend/exporter/adt-into/src/lib.rs Outdated Show resolved Hide resolved
frontend/exporter/src/types/copied.rs Outdated Show resolved Hide resolved
frontend/exporter/src/types/serialize_int.rs Show resolved Hide resolved
frontend/exporter/src/index_vec.rs Outdated Show resolved Hide resolved
frontend/exporter/src/lib.rs Outdated Show resolved Hide resolved
@W95Psp
Copy link
Collaborator Author

W95Psp commented Jul 4, 2024

Thanks for the review 😃 I addressed all your points I think :)

Copy link
Member

@franziskuskiefer franziskuskiefer left a comment

Choose a reason for hiding this comment

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

Thanks, lgtm with a few more nits. Approving already, but please address them before mergin.g
Let's try to keep dependencies to a minimum and really only depend on what we need.

cli/subcommands/Cargo.toml Show resolved Hide resolved
frontend/exporter/src/lib.rs Outdated Show resolved Hide resolved
frontend/exporter/src/types/copied.rs Show resolved Hide resolved
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
No open projects
Status: Done
Development

Successfully merging this pull request may close these issues.

Move diagnostics reporting to annotate_snippets Remove linter
2 participants