Build and lint the LLBC backend with warnings denied in its CI job - #4886
Open
feliperodri wants to merge 16 commits into
Open
feliperodri wants to merge 16 commits into
feliperodri wants to merge 16 commits into
Conversation
…haron bump will touch
A plain MIR `BinaryOp(Add|Sub|Mul)` wraps on overflow -- the checked form is a
separate `CheckedBinaryOp` -- but the LLBC backend mapped both to Charon's
`CheckedAdd`/`CheckedSub`/`CheckedMul`. Those produce a `(result, overflowed)`
pair, so e.g. `intrinsics::wrapping_add` came out type-incorrect:
@0 := copy (a@1) checked.+ copy (b@2) // @0: u8
Map `BinaryOp` to Charon's wrapping operators and keep the `Checked*` operators
for `CheckedBinaryOp`, which Charon's `remove_dynamic_checks` then folds with
the overflow assert into a panicking operator, as before.
The new tests are the safety net for moving the Charon pin (model-checking#4834): Charon
reworked how arithmetic overflow, integer types and literals, and switches are
represented, and a mechanical port can change what they mean while still
compiling. Each test pins the current, hand-reviewed LLBC for one of those
constructs so the bump has to account for every difference. Arrays, slices,
`str`, `Box`, casts, const generics, supertraits and associated consts are not
covered because the backend does not translate them yet.
Verified that only `arith_wrapping` fails without the compiler change.
…ng to check `expected` mode ignores the exit status and only looks for the expected lines, so an empty `expected` file passes no matter what -- including when Kani panics. Seven of the ten original LLBC tests (enum, generic, option, projection, struct, traitimpl, tuple) had one, so they checked nothing, and they cover exactly the constructs the Charon bump re-represents: ADTs, tuples, generics and trait impls. Pin the current, hand-reviewed type declarations and function bodies for each. As with the other expectations, `main` is left out because its `@FunN` ids are allocation order.
…e walker
Calling any inherent method aborted the compiler with the LLBC backend -- a
local `impl Counter { fn get(&self) }` was enough, as was `x.wrapping_add(y)`
from `core`:
expected impl trait, found inherent impl on DefId(0:6 ~ test[4a52]::{impl#0})
To keep methods of different impls apart (their `{impl}` path element is
skipped), a method's name is suffixed with the implementing type, which was
read off the impl's trait ref -- and only trait impls have one. Take it from
the impl's self type instead, which exists for both kinds and prints the same as
before for trait impls (`traitimpl` still expects `get_valA`/`get_valB`). Only
trait impls are registered as trait impls now.
The path walk itself existed three times (`defid_to_name`, `def_to_name`,
`adtdef_to_name`), differing only in where the span came from and in the ADT
copy panicking on an `{impl}` element that the others skip. Keep one, and build
the other two on it.
Part of the names cleanup tracked in model-checking#3585.
`translate_allocation` and `translate_switch_targets` each carried a 12-arm table from integer type to Charon scalar value. Both inputs are two's-complement bit patterns, so one truncating conversion serves both. The Charon bump (model-checking#4834) replaces `ScalarValue` with `IntegerValue`; this way it does so in one place. No change to the emitted LLBC: `int_literals` (negative values at every width) and `switch_int` are unchanged.
Charon at `nightly-2026.09.26` (67da6d3b, 2,176 commits past our pin) builds on our toolchain without any patch, so `scripts/charon-patch.diff`, the CI step that applied it, and the workspace `[patch]` that redirected Charon's `annotate-snippets` git dependency all go. That dependency is now a crates.io release. Charon picked up a new git dependency, `serde_state` (Nadrieril's fork, not the unrelated crates.io crate of that name), which `cargo deny` rejects; allow it next to `tracing-tree`. AeneasVerif/charon#1486 asks whether it can be published. The LLBC backend does not compile against this Charon yet; the following commits port it.
Kani kept its own copies of Charon's option defaults and of its list of transformation passes, and each Charon release changed both underneath it -- this Charon no longer has `ULLBC_PASSES`/`LLBC_PASSES`, a top-level `reorder_decls`, or most of the `TranslateOptions` fields we set. Charon now exposes the pieces its own driver uses. Build `CliOpts` with the `aeneas` preset (the configuration Aeneas consumes), derive `TranslateOptions` from it with `TranslateOptions::new`, and after Kani's own MIR-to-ULLBC translation run `run_transformation_passes`. That covers the opacity policy we hand-built -- `_` foreign, `crate` transparent, `Allocator` and its impls hidden -- and the LLBC printing the expected tests use, so all of it goes. The MIR level is no longer set: only Charon's own MIR fetcher reads it, and Kani translates the MIR it has already transformed.
The four MPL-2.0 exceptions (brownstone, colored, indent_write, nom-supreme) were for Charon dependencies that are gone; `ustr` (BSD-2-Clause-Patent) is new. Two new dependencies carry unmaintained-crate advisories: `paste` (RUSTSEC-2024-0436), used by Charon directly, and `atomic-polyfill` (RUSTSEC-2023-0089), via postcard -> heapless. Neither is a vulnerability, and both are only reached through the LLBC backend, which sits behind the `llbc` feature and is not part of Kani releases, so ignore them with that reason. `cargo deny --all-features --workspace check` passes.
Charon's AST was reorganised between our old pin and nightly-2026.09.26, and
some of it was redesigned rather than renamed. The renames are mechanical; for
every redesigned construct, this follows what Charon's own MIR translator
(`bin/charon-driver/translate`) emits, since that is what the passes and Aeneas
expect:
- Arithmetic carries an overflow mode: MIR `Add`/`Sub`/`Mul`/shifts are
`Wrap`, their `*Unchecked` forms and `Div`/`Rem` are `UB`, and
`CheckedBinaryOp` is `AddChecked`/... (upstream's `translate_binaryop_kind`).
- `Assert` is a terminator whose `check_kind` records the check. Kani dropped
the MIR assert message; it is translated now, because
`reconstruct_fallible_operations` only folds an overflow, bounds or division
check into the operation it guards when it knows which check it is.
- Constants are `ConstantExpr::new(kind, ty)`, with `Literal` and
`ConstGeneric` merged into `ConstantExprKind`; integer values come from
`IntegerValue::from_bits` instead of a hand-written table.
- Switches are `SwitchData` plus a branch table, built as upstream does.
- Builtin types are type declarations: tuples point at `TypeDeclId::UNIT`,
`str` is the builtin `struct str { _0: [u8] }`, `Box` is tagged builtin.
- Drops are terminators naming their drop glue. Upstream reaches it through a
proof for its synthetic `Destruct::drop_glue`; Kani points at
`drop_in_place::<T>`, which is that glue.
- `TraitDecl` is built around associated items, `TraitRef` is hash-consed, and
`FunDecl` holds the generics that used to be on the signature.
Three things Charon's own driver sets up and Kani now does too:
- `TypeDeclId::UNIT` must be the declaration of `()`. Every tuple points there,
so without reserving it first, tuples silently named whichever ADT was
registered first.
- The target information, which `compute_layout_guarantees` requires.
- `item_names`, which the printer and `compute_short_names` read; LLBC is now
printed with item names instead of `@Adt0`/`@Fun1`.
Charon now type-checks the translation, and it caught a mismatch that the old
pin never checked: a function binds a region for each late-bound region of its
reference inputs, but calls passed none. Calls now pass them as erased, as
upstream does, from the same helper the declaration uses.
Trait-clause proofs stay placeholders (`BuiltinOrAuto`), as they were, and
trait objects become an explicit `TyKind::Error` instead of a placeholder
predicate the new AST no longer has; neither is reachable from the tests.
Every expected file changed, and I reviewed each against its old version for meaning rather than format. What changed: - Formatting: `_0 = copy i == const 0i32` for `@0 := copy (i@1) == const (0 : i32)`, `storage_live`, and a `↳⚡` line for each call's unwind edge (Kani's existing abort block, now printed). - Items are printed by name (`is_zero(..)`, `(i32, i32)`, `Option<T>`) rather than by id, now that `item_names` is filled in. Since ids no longer appear, `main` is included again; `diverging_call`'s real check is the call in `main`. The `()` declaration is left out, as it is the same in every test. - Arithmetic spells its overflow mode: wrapping `wrap.+`, checked `panic.+` (was `+`, "fails on overflow"), and `/`, `%`, shifts and negation `panic.`, all as before. `unchecked_*` is now `ub.+` where it was `+`: its overflow is undefined behavior, which the old AST could not express. - Drops name their glue: `drop[drop_glue<'_, Option<i32>>] b`, with the types matching the values dropped. Nothing else changed meaning: literal values (negative ones at every width), switch arms, enum and tuple projections, trait impl and inherent method names are the same.
Nothing in CI checked the LLBC backend for warnings or lints: the regression script's `-D warnings` build left out the `llbc` feature because the old Charon had warnings of its own (the TODO said to revisit once the pin moved), and the clippy job only lints the default features. Thirteen clippy errors had accumulated in the backend as a result. Charon now builds warning-free, and the port removed ten of those errors; fix the remaining three. Rather than make the main regression job build Charon, add a `-D warnings` build and a clippy run to `kani-llbc-regression.sh`, which only the LLBC job runs and which already builds with `llbc`. Verified that a planted lint fails the script.
github-actions
Bot
added
Z-EndToEndBenchCI
2 of 7 tasks
With Charon's type check now running on the translation, several common
signatures made it reject Kani's output ("Found incorrect region var" /
"Found incorrect type var") and the compiler then hit a `todo!()`:
- `fn get(x: Option<&u32>)`, `fn deref2(x: &&u32)`, `fn read(h: Holder<'_>)`:
only top-level `&T` inputs contributed late-bound regions, so a region
nested in an ADT or another reference was undeclared. `fn pick<'a>(x: &'a
u32, y: &'a u32)` declared `'a` twice, once per input.
- `fn f<'a, T: 'a>(x: &'a T)`, `fn rd<'a, T>(x: R<'a, T>)`, methods of an
`impl<'a>`: parameters were numbered with rustc's index, which counts all
kinds together (and parent generics first), while Charon numbers each kind
from zero. Late-bound regions also reused the ids of early-bound ones.
- `FnDef::fn_sig` erases early-bound regions, so `f` above printed
`x: &'_ T`.
- Function-pointer types declared no regions for their own binder.
Now, as in Charon's translation:
- the late-bound regions are the signature binder's bound variables (all of
them, each once, wherever they occur), numbered after the early-bound
regions;
- every generic parameter gets its position among parameters of the same
kind, computed per item from `generics_of`, including parents; an
`ItemGenerics` scope is active while translating a type, trait or function
declaration (and a function's generic body, which mentions its
parameters);
- the declaration's signature comes from `tcx.fn_sig(..).instantiate_identity()`;
- function-pointer types bind their regions, and item parameters inside
them are referenced one binder further out.
Elided regions (`'_`) stay unnamed, as Charon leaves them.
`tests/llbc/regions` covers each case; it fails without this change.
The llbc suite passes (22/22), and fmt and both CI clippy invocations are
clean. `cargo clippy --features llbc` still reports the three pre-existing
lints that model-checking#4886 fixes.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…rrors Charon's pass pipeline type-checks the translation, so its error count is no longer zero in practice: on an input it rejects, Kani printed Charon's errors, then panicked with "not yet implemented" and reported an internal compiler error. Emit a fatal error that says Charon reported errors instead; Charon has already printed each of them, and no LLBC file is written. Checked by temporarily undoing the region declarations of the previous commit: `fn get(x: Option<&u32>)` now ends with "error: Charon reported 2 error(s) while translating to LLBC" and no `.llbc` file, instead of a panic. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The comment on the `Drop` terminator said the glue for `T` is `drop_in_place::<T>`, but `Instance::resolve_drop_in_place` resolves to the `core::ptr::drop_glue` lang item (which `drop_in_place` wraps), and that is what the LLBC prints. `translate_generic_args_without_trait` took a `DefId` that it discarded; remove it. No change to the emitted LLBC. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…git source Charon's nightly-2026.09.29 tag (962e40b0) differs from nightly-2026.09.26 only in depending on the published `serde_state_perfect_derive` 1.0.0 (MIT OR Apache-2.0) instead of the `serde_state` git fork (AeneasVerif/charon#1486, model-checking#1487). With no git source left besides `tracing-tree`, `deny.toml`'s `allow-git` is back to what main has. `cargo update -p charon` changes only the two `serde_state` entries in Cargo.lock. The llbc suite passes (22/22); `cargo deny check licenses sources bans` is ok. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
added a commit
to feliperodri/kani
that referenced
this pull request
Sep 29, 2026
With Charon's type check now running on the translation, several common
signatures made it reject Kani's output ("Found incorrect region var" /
"Found incorrect type var") and the compiler then hit a `todo!()`:
- `fn get(x: Option<&u32>)`, `fn deref2(x: &&u32)`, `fn read(h: Holder<'_>)`:
only top-level `&T` inputs contributed late-bound regions, so a region
nested in an ADT or another reference was undeclared. `fn pick<'a>(x: &'a
u32, y: &'a u32)` declared `'a` twice, once per input.
- `fn f<'a, T: 'a>(x: &'a T)`, `fn rd<'a, T>(x: R<'a, T>)`, methods of an
`impl<'a>`: parameters were numbered with rustc's index, which counts all
kinds together (and parent generics first), while Charon numbers each kind
from zero. Late-bound regions also reused the ids of early-bound ones.
- `FnDef::fn_sig` erases early-bound regions, so `f` above printed
`x: &'_ T`.
- Function-pointer types declared no regions for their own binder.
Now, as in Charon's translation:
- the late-bound regions are the signature binder's bound variables (all of
them, each once, wherever they occur), numbered after the early-bound
regions;
- every generic parameter gets its position among parameters of the same
kind, computed per item from `generics_of`, including parents; an
`ItemGenerics` scope is active while translating a type, trait or function
declaration (and a function's generic body, which mentions its
parameters);
- the declaration's signature comes from `tcx.fn_sig(..).instantiate_identity()`;
- function-pointer types bind their regions, and item parameters inside
them are referenced one binder further out.
Elided regions (`'_`) stay unnamed, as Charon leaves them.
`tests/llbc/regions` covers each case; it fails without this change.
The llbc suite passes (22/22), and fmt and both CI clippy invocations are
clean. `cargo clippy --features llbc` still reports the three pre-existing
lints that model-checking#4886 fixes.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
… suffix
The name builder dropped the `{impl}` element of a method's path and
appended the implementing type to the method name instead:
`core::num::wrapping_addu8`, `test::getCounter`, `test::get_valA`, and for a
generic impl `test::getWrapper<T>` (the rendered type, generics included).
Charon's own translation keeps the impl in the path, which Aeneas and
Charon's name matching and short-name computation expect.
Build the element as Charon does:
- an inherent impl is `PathElem::Impl(ImplElem::Ty(..))`: its self type,
bound by the impl's generics (`{Wrapper<T>}`, `{u8}`);
- a trait impl is `PathElem::Impl(ImplElem::Trait(id))`, which refers to a
trait impl declaration. Kani now declares trait impls the way it declares
trait decls: the implemented trait and the generics, with no associated
items, methods or vtable (`VTableDecl::Unknown`). The declaration is
created the first time the impl is named; its id is registered before its
own name (which contains the impl) is computed.
So `u8::wrapping_add` is `core::num::{u8}::wrapping_add`, `Counter::get` is
`test::{Counter}::get`, and `<A as T>::get_val` is
`test::{impl T for A}::get_val` (printed with Charon's short name
`impl_T_for_A::get_val`). The expected output of the four tests with
methods changes accordingly; in `regions`, the inherent method and the free
function are both named `get` now, so Charon prints both by full path.
`tests/llbc/impl_paths` covers generic inherent and trait impls and a trait
impl for a reference type.
The llbc suite passes (23/23); `kani-llbc-regression.sh` (with the
`-D warnings` build and llbc clippy), fmt and both CI clippy invocations
pass.
Resolves model-checking#4884
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
added a commit
to feliperodri/kani
that referenced
this pull request
Sep 29, 2026
…name builders (model-checking#4882) Rebased onto main after model-checking#4881 merged; three commits: `29c3b1eb2`, `697526953`, and `dfc1b0592` (see below). Second step toward the Charon bump (model-checking#4834), still on the old pin. **The bug.** Calling *any* inherent method aborts the compiler with the LLBC backend. A local type is enough: ```rust impl Counter { fn get(&self) -> u32 { self.n } } ``` ``` expected impl trait, found inherent impl on DefId(0:6 ~ test[4a52]::{impl#0}) ``` and so is `x.wrapping_add(y)` from `core`. Method names get the implementing type appended so methods from different impls don't collide, and that type was read from the impl's trait ref — which only trait impls have. It now comes from the impl's self type, which both kinds have and which prints identically for trait impls: `traitimpl` (pinned in model-checking#4881) still expects `get_valA` / `get_valB`. Two new tests cover the local and the `core` case; both crashed before. **The cleanup.** The path-to-name walk existed three times (`defid_to_name`, `def_to_name`, `adtdef_to_name`), differing only in where the span came from — and the ADT copy panicked on an `{impl}` path element the other two skip. Now there's one. Separately, the integer-type → scalar-value table was duplicated between constants and switch targets; it's one function now, so the bump rewrites it in one place. **No behaviour change beyond the crash** — that's the point of doing this before the bump. All 19 expectations from model-checking#4881 are untouched, including `int_literals` (negatives at every width) and `switch_int`, which exercise the merged table. The third commit stops `inherent_core/expected` from pinning the callee's `@FunN` id: ids follow the fingerprint order in which Kani reaches items, which changed with nightly-2026-09-24 (`@Fun1` became `@Fun2`). The callee's name is still checked by its declaration line. **Where I'd like input:** the suffix scheme itself (`getCounter`, `core::num::wrapping_addu8`) is kept as-is, because changing it here would muddy the "nothing changed" signal. Charon's own naming uses a proper `{impl}` path element instead; I'd rather adopt that in the bump, where names change anyway. Shout if you'd prefer it now. (Now done on top of the bump, in model-checking#4886; see model-checking#4884.) I also dropped a planned "route every redesigned construct through helpers" step after looking closely: those call sites already sit in five functions (`translate_ty`, `translate_allocation`, `translate_switch_targets`, `translate_bin_op`, the trait-decl builder), so a helper layer would add indirection without making the bump meaningfully smaller. `tests/llbc` 21/21, `kani-llbc-regression.sh`, fmt, clippy. Part of the names item in model-checking#3585. --------- Co-authored-by: Michael Tautschnig <tautschn@amazon.com> Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
added a commit
to feliperodri/kani
that referenced
this pull request
Sep 29, 2026
With Charon's type check now running on the translation, several common
signatures made it reject Kani's output ("Found incorrect region var" /
"Found incorrect type var") and the compiler then hit a `todo!()`:
- `fn get(x: Option<&u32>)`, `fn deref2(x: &&u32)`, `fn read(h: Holder<'_>)`:
only top-level `&T` inputs contributed late-bound regions, so a region
nested in an ADT or another reference was undeclared. `fn pick<'a>(x: &'a
u32, y: &'a u32)` declared `'a` twice, once per input.
- `fn f<'a, T: 'a>(x: &'a T)`, `fn rd<'a, T>(x: R<'a, T>)`, methods of an
`impl<'a>`: parameters were numbered with rustc's index, which counts all
kinds together (and parent generics first), while Charon numbers each kind
from zero. Late-bound regions also reused the ids of early-bound ones.
- `FnDef::fn_sig` erases early-bound regions, so `f` above printed
`x: &'_ T`.
- Function-pointer types declared no regions for their own binder.
Now, as in Charon's translation:
- the late-bound regions are the signature binder's bound variables (all of
them, each once, wherever they occur), numbered after the early-bound
regions;
- every generic parameter gets its position among parameters of the same
kind, computed per item from `generics_of`, including parents; an
`ItemGenerics` scope is active while translating a type, trait or function
declaration (and a function's generic body, which mentions its
parameters);
- the declaration's signature comes from `tcx.fn_sig(..).instantiate_identity()`;
- function-pointer types bind their regions, and item parameters inside
them are referenced one binder further out.
Elided regions (`'_`) stay unnamed, as Charon leaves them.
`tests/llbc/regions` covers each case; it fails without this change.
The llbc suite passes (22/22), and fmt and both CI clippy invocations are
clean. `cargo clippy --features llbc` still reports the three pre-existing
lints that model-checking#4886 fixes.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
kasimte
pushed a commit
to kasimte/kani
that referenced
this pull request
Sep 30, 2026
…ecking#4883) Rebased onto main after model-checking#4881 and model-checking#4882 merged. Nine commits: five for the bump itself (from `cbd1e83c7`) and four follow-ups (see "Follow-ups" below). They're split so each can be read on its own. Resolves model-checking#4834: Charon goes from a commit 2,176 commits old to `nightly-2026.09.29`, and `scripts/charon-patch.diff`, the CI step that applied it, and the workspace `[patch]` for its git dependency all go away. Charon itself builds unpatched on our toolchain. ## Why it's shaped this way Every past Charon bump broke Kani because we hand-copied Charon's option defaults and its list of passes. Charon now exposes both, so the LLBC backend configures Charon exactly as `charon --preset aeneas` does and runs `run_transformation_passes` after our own MIR-to-ULLBC step. That deletes about 90 lines, and the next bump should be mostly renames. For the translation itself, wherever the AST was *redesigned* rather than renamed, I copied what Charon's own MIR translator emits instead of inventing a mapping — the arithmetic overflow modes, assert kinds, switches, builtin types, drops. The commit message lists each one. ## What the review should focus on The risk the issue called out is a port that compiles but changes meaning. model-checking#4881 pinned the old output first, and I reviewed every changed expected file against its old version. The expected-file commit lists what changed; in short: formatting, names instead of `@Adt0`, and two deliberate refinements — `unchecked_add` overflow is now `ub.+` rather than a panic (the old AST couldn't say UB), and drops name their glue type. Three things I'd especially like eyes on, because each was a silent bug waiting to happen: - **`TypeDeclId::UNIT` must be `()`**. Every tuple points at id 0, and Charon's driver reserves it before anything else. Kani didn't, so without that tuples would have silently named whichever ADT got registered first. The `tuple` and `projection` tests now print `(i32, i32)` where that would show. - **Asserts need their `check_kind`**. We dropped the MIR assert message; the new `reconstruct_fallible_operations` only folds an overflow check into `panic.+` when it knows which check it is. Without it, `arith_checked` quietly stops folding. - **Charon now type-checks the translation**, and it caught a real mismatch the old pin never checked: calls didn't pass the late-bound regions the callee declares. Calls now pass them as erased, from the same helper the declaration uses. A follow-up (`f5c3d5139`) makes the declarations themselves match Charon's numbering; see below. ## Things I'd like input on - `deny.toml` (its own commit): swap four stale MPL exceptions for `ustr` (BSD-2-Clause-Patent), and **ignore two "unmaintained" advisories** (`paste`, `atomic-polyfill`) that only Charon pulls in. They're not vulnerabilities and the LLBC backend isn't in releases, but ignoring advisories is a policy call — happy to handle it differently. - Drops point at the glue `Instance::resolve_drop_in_place` returns, the `core::ptr::drop_glue` instance that `drop_in_place::<T>` wraps. Upstream reaches the glue through a proof for a synthetic `Destruct::drop_glue` method, which Kani doesn't model. If Aeneas specifically wants the trait form, that's a bigger follow-up. ## Not in this PR - **Charon's `{impl}` path naming** (model-checking#4884): it isn't needed for model-checking#4834 and renames every method, so it is in model-checking#4886 instead. - Arrays, slices, `str` literals, `Box`, casts, const generics, supertraits and associated consts still stop at Kani's own `todo!()`s — same as before, independent of Charon. Listed with reproducers in model-checking#4885. - Trait-clause proofs stay placeholders, as they were. `both_none`'s output also shows model-checking#3585's generic-vs-monomorphized mismatch more visibly now (a generic signature over a monomorphic body) — pre-existing, not introduced here. ## Follow-ups - `f5c3d5139` declares generic parameters and regions the way Charon numbers them. Signatures with a reference that isn't a top-level `&T` input (`Option<&u32>`, `&&u32`, `Holder<'_>`), with a region used twice (`pick<'a>(x: &'a u32, y: &'a u32)`), with an early-bound region before a type parameter (`fn f<'a, T: 'a>`), or in an `impl<'a>` failed Charon's type check. Now all late-bound regions of the signature binder are declared once, after the early-bound ones; every parameter gets its per-kind position; the declared signature keeps its early-bound regions; and fn-pointer types bind their own regions. New test `tests/llbc/regions`. - `817c2aa1f` stops with an error ("Charon reported N error(s) while translating to LLBC") instead of the `todo!()` when Charon reports errors. - `3a07dcfc0` fixes the drop-glue comment and removes an unused parameter. - `c00ab4007` moves the pin to `nightly-2026.09.29`, which differs from `nightly-2026.09.26` only in using the published `serde_state_perfect_derive` (AeneasVerif/charon#1486), so `deny.toml` no longer allows the `serde_state` git source. `tests/llbc` 22/22, `kani-llbc-regression.sh`, kani 613, expected 478, ui 152, cargo-kani 71, unit tests with and without `llbc`, `cargo deny --all-features`, fmt, clippy. --------- Co-authored-by: Michael Tautschnig <tautschn@amazon.com> Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
# Conflicts: # Cargo.lock # kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs # tests/llbc/inherent_core/expected # tests/llbc/inherent_local/expected # tests/llbc/regions/expected # tests/llbc/traitimpl/expected
feliperodri
enabled auto-merge
September 30, 2026 05:17
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The rest of the Charon stack (#4881, #4882, #4883) has merged, and
mainis merged in. Two commits remain on top of it:a201193f1(the lint gate) and1e22d6f4c(method names, see the end).Last step of the Charon plan in #4834: make sure the LLBC backend can't quietly rot again.
Why. Nothing in CI checked the LLBC backend for warnings or lints. The regression script's
-D warningsbuild left outllbcbecause the old Charon had warnings of its own — its TODO said to revisit once the pin moved — and the clippy job only lints the default features. So the backend had accumulated 13 clippy errors that nobody could see (I found them while doing #4881).What. Charon now builds warning-free, and #4883 already removed ten of those errors; this fixes the last three. Then
kani-llbc-regression.sh— which only the LLBC job runs, and which already builds withllbc— gains a-D warningsbuild and aclippy -p kani-compiler --features llbc -- -D warnings. The TODO inkani-regression.shbecomes a pointer to it.The call I'd like checked: I put the gate in the LLBC job rather than the main regression and clippy jobs, so that those don't have to build Charon on every PR. The trade-off is that a PR which breaks only the LLBC lints fails in the LLBC job rather than the clippy one — same signal, different place. Easy to move if you'd rather have it next to the other clippy run.
Verified the gate actually gates: the script runs under
errexit, and a plantedlet_and_returnmakes it exit 101.Also: name methods the way Charon does. The last commit replaces the implementing-type suffix on method names (
core::num::wrapping_addu8,test::getCounter,getWrapper<T>) with Charon'sPathElem::Impl:{u8}/{Wrapper<T>}for inherent impls, and{impl T for A}for trait impls. The trait-impl form refers to a trait impl declaration, which Kani now emits minimally, like trait declarations: the implemented trait and the generics, with no methods, associated items or vtable. The expected output of the four tests with methods changes accordingly, andtests/llbc/impl_pathscovers generic inherent and trait impls.Resolves #4884