hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
200 stars 21 forks source link

Driver: call the frontend once #277

Open W95Psp opened 1 year ago

W95Psp commented 1 year ago

Currently:

  1. cargo-hax calls cargo build with our driver, then for each selected package: a. cargo runs our driver b. the driver runs Rustc with special hooks c. we export a THIR AST d. pipe it as JSON to the engine e. write F/Coq/ files

It would be better to buffer all JSON at 1.c., and call the engine once.

Pros:

Cons:

Nadrieril commented 7 months ago

Regarding the point about rustc errors, we're having similar considerations over on charon&aeneas. Are you sure it would be so hard to generate errors ourselves? Getting the right file/line info out of a span is easy, and many crates provide rustc-like error output. We can also do rust-specific things like merging spans and resolving spans across macro expansions before we turn them into our own dumb spans. I don't see any major obstacle. What obstacles do you see that I don't?