Add an LLBC backend #3514
Add an LLBC backend #3514
Conversation
zhassan-aws
force-pushed
the
llbc4
branch
4 times, most recently
from
c56066c
to
69840fb
Compare
There was a problem hiding this comment.
I haven't reviewed the backend code yet, but I'm curious about how this affects our released software. Are we shipping the new backend?
That was the plan (it's under an unstable feature). If we prefer to not include it in the release at this point, we can disable the feature by default and have a separate set of regressions for this feature.
There was a problem hiding this comment.
I think it would be great if we could eventually simplify the naming schema, and remove the name generation code. This seems fairly fragile, hard to maintain and I worry that this will not work (or even be unsound) if 2+ crates have the same name. That said, I think it is out of scope of this PR since you are only trying to match Aeneas name schema.
The handling of monomorphic vs generic code also need some improvement. To unblock this PR, can we add an error if we encounter generic code? I think none of your tests depend on generic code.
@celinval pointed out that `cargo update` will attempt to update the `charon` submodule as well. Exclude the `charon` submodule from the workspace so that it's not considered when running `cargo update`, `cargo deny`, `cargo clippy`, and `cargo fmt`. The PR also reverts some of the configuration changes made in #3514. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
In #3514, the LLBC does not keep the variable names from the Rust source. This PR extracts the names of variables from MIR and carries it over to the LLBC. For instance, for `tests/expected/llbc/basic1` which has the following Rust: ```rust fn select(s: bool, x: i32, y: i32) -> i32 { if s { x } else { y } } ``` without this PR, running Aeneas on the output LLBC produces: ```lean def select (b : Bool) (i : I32) (i1 : I32) : Result I32 := if b then Result.ok i else Result.ok i1 ``` but with this PR, it produces: ```lean def select (s : Bool) (x : I32) (y : I32) : Result I32 := if s then Result.ok x else Result.ok y ``` This should not be merged before #3514, so keeping it as a draft for the time being. The actual diff on top of #3514 can be viewed here: zhassan-aws/kani@llbc4...zhassan-aws:kani:llbc-names By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
This is a follow-up on #3514. As @celinval suggested ([here](#3514 (comment))), renaming all user-facing options from "Aeneas" to Lean. Inside the Kani compiler which is only concerned with producing LLBC (and doesn't know about Lean/Aeneas), I'm renaming the relevant feature from `aeneas` to `llbc`, and the backend is now called the LLBC backend as opposed to the Aeneas backend. Towards #3585 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
This PR adds a new codegen backend that generates low-level borrow calculus (LLBC), which is the format defined by Charon and Aeneas.
The backend can be invoked using
-Zaeneas, and will generate a.llbcfile. This file can then be passed to Aeneas to generate Lean for example. Currently, Aeneas needs to be manually run on the generated LLBC.The PR translates stable MIR to unstructured LLBC (ULLBC) and then uses the Charon library to apply transformations that reconstruct the control flow to regain some of the high-level structure (loops, if statements, etc.).
In this PR, very few MIR constructs are handled, but the PR is already pretty big. More support to come in subsequent PRs.
Call-outs:
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.