LLBC: translate wrapping arithmetic as wrapping, and cover what the Charon bump will touch - #4881
Merged
Merged
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.
github-actions
Bot
added
Z-EndToEndBenchCI
…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.
This was referenced Sep 27, 2026
feliperodri
added
the
Z-Kani Compiler
Contributor
There was a problem hiding this comment.
Copilot review overview
🟢 Approval recommended
The arithmetic correction is narrowly scoped and covered by comprehensive LLBC regression expectations.
Review effort: Balanced
Findings: None
What changed in this PR
Fixes LLBC arithmetic translation and establishes regression baselines before upgrading Charon.
Changes:
- Translates plain MIR addition, subtraction, and multiplication as wrapping operations while preserving checked operations.
- Adds nine LLBC regression fixtures for arithmetic, literals, unary operations, and switches.
- Populates seven previously empty LLBC expectations.
| File | Description |
|---|---|
kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs |
Separates checked and wrapping arithmetic translation. |
tests/llbc/arith_checked/test.rs |
Exercises checked arithmetic. |
tests/llbc/arith_checked/expected |
Pins checked arithmetic LLBC. |
tests/llbc/arith_unchecked/test.rs |
Exercises unchecked arithmetic. |
tests/llbc/arith_unchecked/expected |
Pins unchecked arithmetic LLBC. |
tests/llbc/arith_wrapping/test.rs |
Exercises wrapping arithmetic. |
tests/llbc/arith_wrapping/expected |
Verifies wrapping operators. |
tests/llbc/bool_char/test.rs |
Exercises Boolean and character literals. |
tests/llbc/bool_char/expected |
Pins literal translation. |
tests/llbc/div_rem/test.rs |
Exercises division and remainder. |
tests/llbc/div_rem/expected |
Pins division and remainder LLBC. |
tests/llbc/enum/expected |
Adds the enum baseline. |
tests/llbc/generic/expected |
Adds the generic baseline. |
tests/llbc/int_literals/test.rs |
Exercises all integer widths. |
tests/llbc/int_literals/expected |
Pins integer literal translation. |
tests/llbc/option/expected |
Adds the generic Option baseline. |
tests/llbc/projection/expected |
Adds nested projection coverage. |
tests/llbc/shifts/test.rs |
Exercises signed and unsigned shifts. |
tests/llbc/shifts/expected |
Pins shift translation. |
tests/llbc/struct/expected |
Adds the struct baseline. |
tests/llbc/switch_int/test.rs |
Exercises integer switch reconstruction. |
tests/llbc/switch_int/expected |
Pins multi-arm switch LLBC. |
tests/llbc/traitimpl/expected |
Adds trait implementation coverage. |
tests/llbc/tuple/expected |
Adds the tuple baseline. |
tests/llbc/unops/test.rs |
Exercises negation and not operations. |
tests/llbc/unops/expected |
Pins unary-operation LLBC. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
Charon's printer at the current pin refers to type declarations by id, and the ids follow the order in which Kani reaches the items, which is sorted by fingerprint (`collect_reachable_items`). That order changed with nightly-2026-09-24: `projection` now numbers `MyStruct`, `MyEnum` and `MyEnum0` as @aDt0, @adt1, @adt2 instead of @adt1, @aDt0, @adt2, so the test fails once this is merged onto current main. `traitimpl` pins two ids the same way and would break on the next reordering. Cut the affected lines right after `@Adt`, keeping everything before the id. The type declarations themselves are still checked in full by name, and the Charon bump replaces these ids with names anyway. Checked with the llbc suite (19/19) on this branch (nightly-2026-09-23) and merged onto main c35cb96 (nightly-2026-09-24). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
approved these changes
Sep 29, 2026
tautschnig
enabled auto-merge
September 29, 2026 15:37
Merged
via the queue into
model-checking:main
with commit Sep 29, 2026
40fd009
31 of 32 checks passed
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>
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
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.
First of the PRs toward moving our Charon pin to current (#4834). The plan is in that issue's thread; this one lands on the old pin, on purpose.
Why tests first. Between our pin and Charon's latest tag, the AST changed how arithmetic overflow, integer types and literals, and switches are represented. The port will compile long before it's correct, and today only the 10 tests in
tests/llbcwould notice a change in meaning — none of which do arithmetic. So this adds nine tests pinning the current, hand-reviewed LLBC for exactly those constructs. When the bump lands, every changed expected file has to be explained as formatting or intended.The bug it found. Writing the arithmetic tests turned up a real one: MIR's plain
Add/Sub/Mulwrap on overflow, but we translated them to Charon'sCheckedAdd/CheckedSub/CheckedMul, which return a(result, overflowed)pair. Sointrinsics::wrapping_addproduced type-incorrect LLBC:Now it's
wrapping.+. Checked arithmetic (a + bwith overflow checks) still goes throughCheckedBinaryOp, which Charon folds with the overflow assert into a panicking+— unchanged, and covered byarith_checked. I confirmedarith_wrappingis the only test that fails without the fix.Worth a look: I reviewed each expected file by hand rather than trusting the output, and two shapes look odd but are correct —
!prints as~for bothu8andbool(Charon uses one symbol forNot), and inswitch_intthe0arm falls through to code after theswitch, which is how control-flow reconstruction places it. The expected files leave outmain, since its@FunNids are allocation order and will churn with the bump.Also: seven existing tests were checking nothing.
expectedmode ignores the exit status and only looks for the expected lines, so an emptyexpectedfile always passes — even if Kani panics.enum,generic,option,projection,struct,traitimplandtupleall had one, and they cover exactly what the bump re-represents (ADTs, tuples, generics, trait impls). The second commit pins their current, hand-reviewed output. Separately, it might be worth makingexpectedmode reject an empty file outright; I haven't done that here.Not covered yet, because the backend doesn't translate them today: arrays, slices,
str,Box, casts, const generics, supertraits, associated consts. Those are coverage the bump has to add rather than preserve.tests/llbc19/19,kani-llbc-regression.sh, fmt, clippy.