AeneasVerif / charon

Interface with the rustc compiler for the purpose of program verification
Apache License 2.0
75 stars 15 forks source link

Expose charon as a rust library #178

Closed Nadrieril closed 1 month ago

Nadrieril commented 3 months ago

We'd like other rust users to be able to use Charon code. This may involve:

Nadrieril commented 2 months ago

https://github.com/AeneasVerif/charon/pull/284 does most of that. charon-lib (which includes the ast definition and the control-flow reconstruction) should be pretty compatible with other rustc nightlies now. The only thing that remains would be to replace our usage of rustc internal crates for error reporting.

zhassan-aws commented 1 month ago

Did you have plans/thoughts on how Charon can be restructured so that the library can be included without including the toolchain-dependent crates in the dependencies (e.g. hax-frontend-exporter)?

Currently, including the Charon library as a dependency brings in the dependencies used in the binaries as well.

Unfortunately, cargo doesn't allow specifying binary-specific dependencies easily:

https://github.com/rust-lang/cargo/issues/1982

The workarounds from what I understand are:

  1. Use a workspace, and use different packages for the library and the binaries
  2. Make hax-frontend-exporter an optional dependency under a feature that is only used for the binaries. One would need to pass --features X when building the binaries though.
Nadrieril commented 1 month ago

Oh yeah, I was thinking we'd add a feature flag. Either is fine probably.

Nadrieril commented 1 month ago

Alright, this should now work on many nightly compilers:

[dependencies]
charon = { git = "https://github.com/AeneasVerif/charon", default-features = false }
Nadrieril commented 1 month ago

The most interesting modules are ast which contains all the ast definitions, and transform which contains the code for the various transformations we do after translation, including control-flow reconstruction.

I believe the current state is good enough to close this issue, lmk if not.

zhassan-aws commented 1 month ago

Awesome, thanks @Nadrieril!