Skip to content

LLBC: name inherent methods instead of aborting, and deduplicate the name builders - #4882

Merged
tautschnig merged 3 commits into
model-checking:mainfrom
feliperodri:llbc-names-refactor
Sep 29, 2026
Merged

tautschnig merged 3 commits into
model-checking:mainfrom
feliperodri:llbc-names-refactor

Conversation

@feliperodri

@feliperodri feliperodri commented Sep 27, 2026 •

Copy link
Copy Markdown
Member

Rebased onto main after #4881 merged; three commits: 29c3b1eb2, 697526953, and dfc1b0592 (see below).

Second step toward the Charon bump (#4834), still on the old pin.

The bug. Calling any inherent method aborts the compiler with the LLBC backend. A local type is enough:

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 #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 #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 #4886; see #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 #3585.

feliperodri and others added 3 commits September 29, 2026 17:49
…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.
`wrap`'s call to `u8::wrapping_add` prints the callee as `@Fun1` on
nightly-2026-09-23 but `@Fun2` on nightly-2026-09-24, because function ids
follow the fingerprint order in which Kani reaches items. The callee's name is
already checked by the `core::num::wrapping_addu8` declaration line, so cut
the call line right after `@Fun`.

Checked with the llbc suite (21/21) 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
tautschnig added this pull request to the merge queue Sep 29, 2026
Merged via the queue into model-checking:main with commit bd66942 Sep 29, 2026
21 of 22 checks passed
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>
tautschnig added a commit to feliperodri/kani that referenced this pull request Sep 30, 2026
…odel-checking#4886)

The rest of the Charon stack (model-checking#4881, model-checking#4882, model-checking#4883) has merged, and this
is rebased onto `main`. Three commits: `ac73eb722` (the lint gate),
`9fafffbb5` (method names, see the end), and `70806c417` (a comment
noting that the `-D warnings` build also covers Charon).

Last step of the Charon plan in model-checking#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 warnings` build left out `llbc` because 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 model-checking#4881).

**What.** Charon now builds warning-free, and model-checking#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 with `llbc` — gains a `-D warnings` build and a `clippy
-p kani-compiler --features llbc -- -D warnings`. The TODO in
`kani-regression.sh` becomes 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
planted `let_and_return` makes 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's `PathElem::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, and
`tests/llbc/impl_paths` covers generic inherent and trait impls.

Resolves model-checking#4884

---------

Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
srivatsansamraj pushed a commit to srivatsansamraj/kani that referenced this pull request Sep 30, 2026
…del-checking#4923)

Pass `--harness-timeout 5m` to
`script-based-pre/cargo_autoharness_fmt_impls`, as the other autoharness
tests (`bounded`, `bounds`, `byte_str`, `c_str`, `formatter`, `wtf8`)
already do.

**Why.** On the macOS x86_64 runners (`regression (macos-15-intel)`),
the `LowerExp`, `UpperExp` and `Pointer` harnesses of this test take
40–60 s, right at `kani autoharness`'s default `--harness-timeout` of 60
s. When one of them times out, CBMC reports `CBMC timed out` instead of
the expected failure, the test's `Failed Checks: "lower exp"` / `"upper
exp"` / `"pointer"` line is missing, and the test fails. The same
harnesses take about 10 s on Linux.

**Evidence.** I went through the logs of the `regression
(macos-15-intel)` jobs between 2026-09-28 and 2026-09-30. 33 of them
failed. This test failed in all 33, with 1–3 of those three harnesses
timing out each time, and in 32 of them it was the only failing test.
The one exception, model-checking#4903's merge-queue push run, also had
`cargo_autoharness_wtf8`'s `len` harness time out, at 5 m. On main
pushes alone, the job failed 7 times out of 12 on 2026-09-30. The
failures are independent of the changes under test:

- Today's automated toolchain upgrade, model-checking#4917: [run
36663872235](https://github.com/model-checking/kani/actions/runs/36663872235/job/109726991201)
(`LowExp`, `UpExp`, `Ptr` timed out; every other regression job passed)
- `main` pushes:
[36654469481](https://github.com/model-checking/kani/actions/runs/36654469481/job/109695682794),
[36656240395](https://github.com/model-checking/kani/actions/runs/36656240395/job/109701095388),
[36657849257](https://github.com/model-checking/kani/actions/runs/36657849257/job/109705923680),
[36659060566](https://github.com/model-checking/kani/actions/runs/36659060566/job/109709545862),
[36670355214](https://github.com/model-checking/kani/actions/runs/36670355214/job/109743820142),
[36674524840](https://github.com/model-checking/kani/actions/runs/36674524840/job/109756493668)
- Merge queue: model-checking#4895
[36650793954](https://github.com/model-checking/kani/actions/runs/36650793954/job/109684194253),
model-checking#4896
[36650908721](https://github.com/model-checking/kani/actions/runs/36650908721/job/109684568489),
model-checking#4809
[36654883143](https://github.com/model-checking/kani/actions/runs/36654883143/job/109696960300),
model-checking#4848
[36663305755](https://github.com/model-checking/kani/actions/runs/36663305755/job/109722546228),
model-checking#4903
[36667236036](https://github.com/model-checking/kani/actions/runs/36667236036/job/109734401431),
model-checking#4856
[36670723600](https://github.com/model-checking/kani/actions/runs/36670723600/job/109744937944),
model-checking#4881
[36596324505](https://github.com/model-checking/kani/actions/runs/36596324505/job/109502054372),
model-checking#4882
[36612997613](https://github.com/model-checking/kani/actions/runs/36612997613/job/109558873539)
- Pull requests: model-checking#4875
[36427316996](https://github.com/model-checking/kani/actions/runs/36427316996/job/109072277288),
model-checking#4895
[36443349794](https://github.com/model-checking/kani/actions/runs/36443349794/job/108999214513),
model-checking#4771
[36620184925](https://github.com/model-checking/kani/actions/runs/36620184925/job/109677883533)

The runner image version (`20260819.586`) was the same in passing and
failing runs.

**Manual testing.** Locally the three harnesses take about 10 s each.
Running the test with `--harness-timeout 3s` reproduces the CI failure
exactly: the same three harnesses time out, their `Failed Checks` lines
are missing, and the summary still reports 9 failures. With this change,
`cargo run -p compiletest -- --suite script-based-pre --mode exec
cargo_autoharness_fmt_impls` passes.

If the macOS Intel runner gets much slower, a longer timeout alone may
not be enough; making these three harnesses cheaper would be the next
step.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants