From a21bebc6739eee85939ac2a6a8793f92e378a73b Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Sun, 27 Sep 2026 18:20:22 +0000 Subject: [PATCH 1/3] LLBC: translate wrapping arithmetic as wrapping, and cover what the Charon 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 (#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. --- .../codegen_aeneas_llbc/mir_to_ullbc/mod.rs | 22 +++++++++-- tests/llbc/arith_checked/expected | 38 +++++++++++++++++++ tests/llbc/arith_checked/test.rs | 22 +++++++++++ tests/llbc/arith_unchecked/expected | 29 ++++++++++++++ tests/llbc/arith_unchecked/test.rs | 26 +++++++++++++ tests/llbc/arith_wrapping/expected | 29 ++++++++++++++ tests/llbc/arith_wrapping/test.rs | 28 ++++++++++++++ tests/llbc/bool_char/expected | 16 ++++++++ tests/llbc/bool_char/test.rs | 17 +++++++++ tests/llbc/div_rem/expected | 32 ++++++++++++++++ tests/llbc/div_rem/test.rs | 18 +++++++++ tests/llbc/int_literals/expected | 15 ++++++++ tests/llbc/int_literals/test.rs | 18 +++++++++ tests/llbc/shifts/expected | 25 ++++++++++++ tests/llbc/shifts/test.rs | 18 +++++++++ tests/llbc/switch_int/expected | 21 ++++++++++ tests/llbc/switch_int/test.rs | 18 +++++++++ tests/llbc/unops/expected | 29 ++++++++++++++ tests/llbc/unops/test.rs | 21 ++++++++++ 19 files changed, 438 insertions(+), 4 deletions(-) create mode 100644 tests/llbc/arith_checked/expected create mode 100644 tests/llbc/arith_checked/test.rs create mode 100644 tests/llbc/arith_unchecked/expected create mode 100644 tests/llbc/arith_unchecked/test.rs create mode 100644 tests/llbc/arith_wrapping/expected create mode 100644 tests/llbc/arith_wrapping/test.rs create mode 100644 tests/llbc/bool_char/expected create mode 100644 tests/llbc/bool_char/test.rs create mode 100644 tests/llbc/div_rem/expected create mode 100644 tests/llbc/div_rem/test.rs create mode 100644 tests/llbc/int_literals/expected create mode 100644 tests/llbc/int_literals/test.rs create mode 100644 tests/llbc/shifts/expected create mode 100644 tests/llbc/shifts/test.rs create mode 100644 tests/llbc/switch_int/expected create mode 100644 tests/llbc/switch_int/test.rs create mode 100644 tests/llbc/unops/expected create mode 100644 tests/llbc/unops/test.rs diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs index 392a43f4c2a8..bcd44422f1ca 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs @@ -1665,7 +1665,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { self.translate_operand(rhs), ), Rvalue::CheckedBinaryOp(bin_op, lhs, rhs) => CharonRvalue::BinaryOp( - translate_bin_op(*bin_op), + translate_checked_bin_op(*bin_op), self.translate_operand(lhs), self.translate_operand(rhs), ), @@ -2011,14 +2011,28 @@ fn translate_uint_ty(uint_ty: UintTy) -> CharonIntegerTy { } } +/// The operator of a MIR `CheckedBinaryOp`, which yields `(result, overflowed)`. Charon folds it with +/// the overflow `Assert` that follows into a panicking operator (`remove_dynamic_checks`). +fn translate_checked_bin_op(bin_op: BinOp) -> CharonBinOp { + match bin_op { + BinOp::Add => CharonBinOp::CheckedAdd, + BinOp::Sub => CharonBinOp::CheckedSub, + BinOp::Mul => CharonBinOp::CheckedMul, + _ => translate_bin_op(bin_op), + } +} + +/// The operator of a plain MIR `BinaryOp`. MIR's `Add`/`Sub`/`Mul` wrap on overflow -- checked +/// arithmetic is a separate `CheckedBinaryOp` -- so they must not become Charon's `Checked*` +/// operators, which produce a `(result, overflowed)` pair. fn translate_bin_op(bin_op: BinOp) -> CharonBinOp { match bin_op { BinOp::AddUnchecked => CharonBinOp::Add, - BinOp::Add => CharonBinOp::CheckedAdd, + BinOp::Add => CharonBinOp::WrappingAdd, BinOp::SubUnchecked => CharonBinOp::Sub, - BinOp::Sub => CharonBinOp::CheckedSub, + BinOp::Sub => CharonBinOp::WrappingSub, BinOp::MulUnchecked => CharonBinOp::Mul, - BinOp::Mul => CharonBinOp::CheckedMul, + BinOp::Mul => CharonBinOp::WrappingMul, BinOp::Div => CharonBinOp::Div, BinOp::Rem => CharonBinOp::Rem, BinOp::BitXor => CharonBinOp::BitXor, diff --git a/tests/llbc/arith_checked/expected b/tests/llbc/arith_checked/expected new file mode 100644 index 000000000000..882578b9dc66 --- /dev/null +++ b/tests/llbc/arith_checked/expected @@ -0,0 +1,38 @@ +pub fn test::add(@1: u8, @2: u8) -> u8\ +{\ + let @0: u8; // return\ + let a@1: u8; // arg #1\ + let b@2: u8; // arg #2\ + let @3: (u8, bool); // anonymous local\ +\ + nop\ + nop\ + @0 := copy (a@1) + copy (b@2)\ + return\ +} + +pub fn test::mul(@1: u32, @2: u32) -> u32\ +{\ + let @0: u32; // return\ + let a@1: u32; // arg #1\ + let b@2: u32; // arg #2\ + let @3: (u32, bool); // anonymous local\ +\ + nop\ + nop\ + @0 := copy (a@1) * copy (b@2)\ + return\ +} + +pub fn test::sub(@1: i16, @2: i16) -> i16\ +{\ + let @0: i16; // return\ + let a@1: i16; // arg #1\ + let b@2: i16; // arg #2\ + let @3: (i16, bool); // anonymous local\ +\ + nop\ + nop\ + @0 := copy (a@1) - copy (b@2)\ + return\ +} diff --git a/tests/llbc/arith_checked/test.rs b/tests/llbc/arith_checked/test.rs new file mode 100644 index 000000000000..5e369d86f5ba --- /dev/null +++ b/tests/llbc/arith_checked/test.rs @@ -0,0 +1,22 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zlean --print-llbc + +//! This test checks that Kani's LLBC backend handles overflow-checked arithmetic: MIR's +//! `CheckedBinaryOp` plus its overflow `Assert` fold into a panicking operator. + +fn add(a: u8, b: u8) -> u8 { + a + b +} +fn sub(a: i16, b: i16) -> i16 { + a - b +} +fn mul(a: u32, b: u32) -> u32 { + a * b +} +#[kani::proof] +fn main() { + let _ = add(1, 2); + let _ = sub(5, 2); + let _ = mul(3, 4); +} diff --git a/tests/llbc/arith_unchecked/expected b/tests/llbc/arith_unchecked/expected new file mode 100644 index 000000000000..e23d7147cde9 --- /dev/null +++ b/tests/llbc/arith_unchecked/expected @@ -0,0 +1,29 @@ +pub fn test::add(@1: u8, @2: u8) -> u8\ +{\ + let @0: u8; // return\ + let a@1: u8; // arg #1\ + let b@2: u8; // arg #2\ +\ + @0 := copy (a@1) + copy (b@2)\ + return\ +} + +pub fn test::mul(@1: u32, @2: u32) -> u32\ +{\ + let @0: u32; // return\ + let a@1: u32; // arg #1\ + let b@2: u32; // arg #2\ +\ + @0 := copy (a@1) * copy (b@2)\ + return\ +} + +pub fn test::sub(@1: i16, @2: i16) -> i16\ +{\ + let @0: i16; // return\ + let a@1: i16; // arg #1\ + let b@2: i16; // arg #2\ +\ + @0 := copy (a@1) - copy (b@2)\ + return\ +} diff --git a/tests/llbc/arith_unchecked/test.rs b/tests/llbc/arith_unchecked/test.rs new file mode 100644 index 000000000000..ab057f0f08d6 --- /dev/null +++ b/tests/llbc/arith_unchecked/test.rs @@ -0,0 +1,26 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zlean --print-llbc + +//! This test checks that Kani's LLBC backend handles unchecked arithmetic (`unchecked_*` +//! intrinsics), whose overflow is undefined behavior. + +#![feature(core_intrinsics)] +#![allow(internal_features)] + +use std::intrinsics::{unchecked_add, unchecked_mul, unchecked_sub}; +fn add(a: u8, b: u8) -> u8 { + unsafe { unchecked_add(a, b) } +} +fn sub(a: i16, b: i16) -> i16 { + unsafe { unchecked_sub(a, b) } +} +fn mul(a: u32, b: u32) -> u32 { + unsafe { unchecked_mul(a, b) } +} +#[kani::proof] +fn main() { + let _ = add(1, 2); + let _ = sub(5, 2); + let _ = mul(3, 4); +} diff --git a/tests/llbc/arith_wrapping/expected b/tests/llbc/arith_wrapping/expected new file mode 100644 index 000000000000..ce7d085abb9b --- /dev/null +++ b/tests/llbc/arith_wrapping/expected @@ -0,0 +1,29 @@ +pub fn test::add(@1: u8, @2: u8) -> u8\ +{\ + let @0: u8; // return\ + let a@1: u8; // arg #1\ + let b@2: u8; // arg #2\ +\ + @0 := copy (a@1) wrapping.+ copy (b@2)\ + return\ +} + +pub fn test::mul(@1: u32, @2: u32) -> u32\ +{\ + let @0: u32; // return\ + let a@1: u32; // arg #1\ + let b@2: u32; // arg #2\ +\ + @0 := copy (a@1) wrapping.* copy (b@2)\ + return\ +} + +pub fn test::sub(@1: i16, @2: i16) -> i16\ +{\ + let @0: i16; // return\ + let a@1: i16; // arg #1\ + let b@2: i16; // arg #2\ +\ + @0 := copy (a@1) wrapping.- copy (b@2)\ + return\ +} diff --git a/tests/llbc/arith_wrapping/test.rs b/tests/llbc/arith_wrapping/test.rs new file mode 100644 index 000000000000..8ccb8f829516 --- /dev/null +++ b/tests/llbc/arith_wrapping/test.rs @@ -0,0 +1,28 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zlean --print-llbc + +//! This test checks that Kani's LLBC backend handles wrapping arithmetic. A plain MIR +//! `Add`/`Sub`/`Mul` wraps on overflow, so it must become Charon's `wrapping.` operators rather +//! than `checked.`, which produce a `(result, overflowed)` pair and made the LLBC type-incorrect: +//! `u8 := a checked.+ b`. + +#![feature(core_intrinsics)] +#![allow(internal_features)] + +use std::intrinsics::{wrapping_add, wrapping_mul, wrapping_sub}; +fn add(a: u8, b: u8) -> u8 { + wrapping_add(a, b) +} +fn sub(a: i16, b: i16) -> i16 { + wrapping_sub(a, b) +} +fn mul(a: u32, b: u32) -> u32 { + wrapping_mul(a, b) +} +#[kani::proof] +fn main() { + let _ = add(200, 100); + let _ = sub(-1, 2); + let _ = mul(3, 4); +} diff --git a/tests/llbc/bool_char/expected b/tests/llbc/bool_char/expected new file mode 100644 index 000000000000..5104e759f5e6 --- /dev/null +++ b/tests/llbc/bool_char/expected @@ -0,0 +1,16 @@ +pub fn test::always() -> bool\ +{\ + let @0: bool; // return\ +\ + @0 := const (true)\ + return\ +} + +pub fn test::is_a(@1: char) -> bool\ +{\ + let @0: bool; // return\ + let c@1: char; // arg #1\ +\ + @0 := copy (c@1) == const (a)\ + return\ +} diff --git a/tests/llbc/bool_char/test.rs b/tests/llbc/bool_char/test.rs new file mode 100644 index 000000000000..22c5d56dbd33 --- /dev/null +++ b/tests/llbc/bool_char/test.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zlean --print-llbc + +//! This test checks that Kani's LLBC backend handles `bool` and `char` literals. + +fn is_a(c: char) -> bool { + c == 'a' +} +fn always() -> bool { + true +} +#[kani::proof] +fn main() { + let _ = is_a('b'); + let _ = always(); +} diff --git a/tests/llbc/div_rem/expected b/tests/llbc/div_rem/expected new file mode 100644 index 000000000000..36d8b3c6577c --- /dev/null +++ b/tests/llbc/div_rem/expected @@ -0,0 +1,32 @@ +pub fn test::div(@1: u32, @2: u32) -> u32\ +{\ + let @0: u32; // return\ + let a@1: u32; // arg #1\ + let b@2: u32; // arg #2\ + let @3: bool; // anonymous local\ +\ + nop\ + nop\ + @0 := copy (a@1) / copy (b@2)\ + return\ +} + +pub fn test::rem(@1: i32, @2: i32) -> i32\ +{\ + let @0: i32; // return\ + let a@1: i32; // arg #1\ + let b@2: i32; // arg #2\ + let @3: bool; // anonymous local\ + let @4: bool; // anonymous local\ + let @5: bool; // anonymous local\ + let @6: bool; // anonymous local\ +\ + nop\ + nop\ + nop\ + nop\ + nop\ + nop\ + @0 := copy (a@1) % copy (b@2)\ + return\ +} diff --git a/tests/llbc/div_rem/test.rs b/tests/llbc/div_rem/test.rs new file mode 100644 index 000000000000..c3296611499c --- /dev/null +++ b/tests/llbc/div_rem/test.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zlean --print-llbc + +//! This test checks that Kani's LLBC backend handles division and remainder, whose division-by-zero +//! and overflow checks fold into the operator. + +fn div(a: u32, b: u32) -> u32 { + a / b +} +fn rem(a: i32, b: i32) -> i32 { + a % b +} +#[kani::proof] +fn main() { + let _ = div(7, 2); + let _ = rem(7, 2); +} diff --git a/tests/llbc/int_literals/expected b/tests/llbc/int_literals/expected new file mode 100644 index 000000000000..14c624b30b0e --- /dev/null +++ b/tests/llbc/int_literals/expected @@ -0,0 +1,15 @@ +pub fn test::signed() -> (i8, i16, i32, i64, i128, isize)\ +{\ + let @0: (i8, i16, i32, i64, i128, isize); // return\ +\ + @0 := (const (-1 : i8), const (-2 : i16), const (-3 : i32), const (-4 : i64), const (-5 : i128), const (-6 : isize))\ + return\ +} + +pub fn test::unsigned() -> (u8, u16, u32, u64, u128, usize)\ +{\ + let @0: (u8, u16, u32, u64, u128, usize); // return\ +\ + @0 := (const (1 : u8), const (2 : u16), const (3 : u32), const (4 : u64), const (5 : u128), const (6 : usize))\ + return\ +} diff --git a/tests/llbc/int_literals/test.rs b/tests/llbc/int_literals/test.rs new file mode 100644 index 000000000000..d6dcb189f1e9 --- /dev/null +++ b/tests/llbc/int_literals/test.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zlean --print-llbc + +//! This test checks that Kani's LLBC backend handles integer literals of every width, signed and +//! unsigned. + +fn signed() -> (i8, i16, i32, i64, i128, isize) { + (-1, -2, -3, -4, -5, -6) +} +fn unsigned() -> (u8, u16, u32, u64, u128, usize) { + (1, 2, 3, 4, 5, 6) +} +#[kani::proof] +fn main() { + let _ = signed(); + let _ = unsigned(); +} diff --git a/tests/llbc/shifts/expected b/tests/llbc/shifts/expected new file mode 100644 index 000000000000..6701d652fab3 --- /dev/null +++ b/tests/llbc/shifts/expected @@ -0,0 +1,25 @@ +pub fn test::shl(@1: u32, @2: u32) -> u32\ +{\ + let @0: u32; // return\ + let a@1: u32; // arg #1\ + let b@2: u32; // arg #2\ + let @3: bool; // anonymous local\ +\ + nop\ + nop\ + @0 := copy (a@1) << copy (b@2)\ + return\ +} + +pub fn test::shr(@1: i64, @2: u32) -> i64\ +{\ + let @0: i64; // return\ + let a@1: i64; // arg #1\ + let b@2: u32; // arg #2\ + let @3: bool; // anonymous local\ +\ + nop\ + nop\ + @0 := copy (a@1) >> copy (b@2)\ + return\ +} diff --git a/tests/llbc/shifts/test.rs b/tests/llbc/shifts/test.rs new file mode 100644 index 000000000000..94932a8459f2 --- /dev/null +++ b/tests/llbc/shifts/test.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zlean --print-llbc + +//! This test checks that Kani's LLBC backend handles shifts, whose shift-amount check folds into +//! the operator. + +fn shl(a: u32, b: u32) -> u32 { + a << b +} +fn shr(a: i64, b: u32) -> i64 { + a >> b +} +#[kani::proof] +fn main() { + let _ = shl(1, 3); + let _ = shr(-8, 1); +} diff --git a/tests/llbc/switch_int/expected b/tests/llbc/switch_int/expected new file mode 100644 index 000000000000..3f2b4506548c --- /dev/null +++ b/tests/llbc/switch_int/expected @@ -0,0 +1,21 @@ +pub fn test::classify(@1: u8) -> u8\ +{\ + let @0: u8; // return\ + let x@1: u8; // arg #1\ +\ + switch copy (x@1) {\ + 0 : u8 => {\ + nop\ + },\ + 1 : u8 | 2 : u8 => {\ + @0 := const (20 : u8)\ + return\ + },\ + _ => {\ + @0 := const (30 : u8)\ + return\ + },\ + }\ + @0 := const (10 : u8)\ + return\ +} diff --git a/tests/llbc/switch_int/test.rs b/tests/llbc/switch_int/test.rs new file mode 100644 index 000000000000..f86a52382867 --- /dev/null +++ b/tests/llbc/switch_int/test.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zlean --print-llbc + +//! This test checks that Kani's LLBC backend handles a `match` on an integer, which becomes a +//! `SwitchInt` with a multi-value arm and a default. + +fn classify(x: u8) -> u8 { + match x { + 0 => 10, + 1 | 2 => 20, + _ => 30, + } +} +#[kani::proof] +fn main() { + let _ = classify(1); +} diff --git a/tests/llbc/unops/expected b/tests/llbc/unops/expected new file mode 100644 index 000000000000..9e048a4f41d7 --- /dev/null +++ b/tests/llbc/unops/expected @@ -0,0 +1,29 @@ +pub fn test::lnot(@1: bool) -> bool\ +{\ + let @0: bool; // return\ + let a@1: bool; // arg #1\ +\ + @0 := ~(copy (a@1))\ + return\ +} + +pub fn test::neg(@1: i32) -> i32\ +{\ + let @0: i32; // return\ + let a@1: i32; // arg #1\ + let @2: bool; // anonymous local\ +\ + nop\ + nop\ + @0 := -(copy (a@1))\ + return\ +} + +pub fn test::not(@1: u8) -> u8\ +{\ + let @0: u8; // return\ + let a@1: u8; // arg #1\ +\ + @0 := ~(copy (a@1))\ + return\ +} diff --git a/tests/llbc/unops/test.rs b/tests/llbc/unops/test.rs new file mode 100644 index 000000000000..54dd540deecf --- /dev/null +++ b/tests/llbc/unops/test.rs @@ -0,0 +1,21 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zlean --print-llbc + +//! This test checks that Kani's LLBC backend handles unary negation and bitwise/logical not. + +fn neg(a: i32) -> i32 { + -a +} +fn not(a: u8) -> u8 { + !a +} +fn lnot(a: bool) -> bool { + !a +} +#[kani::proof] +fn main() { + let _ = neg(3); + let _ = not(1); + let _ = lnot(true); +} From 275e3436bc3662431c78fcee65f83b2a586f2de9 Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Sun, 27 Sep 2026 18:26:14 +0000 Subject: [PATCH 2/3] LLBC: give the seven existing tests with empty expected files something 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. --- tests/llbc/enum/expected | 26 ++++++++++++ tests/llbc/generic/expected | 44 +++++++++++++++++++ tests/llbc/option/expected | 38 +++++++++++++++++ tests/llbc/projection/expected | 78 ++++++++++++++++++++++++++++++++++ tests/llbc/struct/expected | 14 ++++++ tests/llbc/traitimpl/expected | 27 ++++++++++++ tests/llbc/tuple/expected | 17 ++++++++ 7 files changed, 244 insertions(+) diff --git a/tests/llbc/enum/expected b/tests/llbc/enum/expected index e69de29bb2d1..62d41c0f4f34 100644 --- a/tests/llbc/enum/expected +++ b/tests/llbc/enum/expected @@ -0,0 +1,26 @@ +pub enum test::MyEnum =\ +| A(0: i32)\ +| B() + +pub fn test::enum_match(@1: @Adt0) -> i32\ +{\ + let @0: i32; // return\ + let e@1: @Adt0; // arg #1\ + let @2: isize; // anonymous local\ + let i@3: i32; // local\ +\ + nop\ + match e@1 {\ + test::MyEnum::A => {\ + nop\ + },\ + test::MyEnum::B => {\ + @0 := const (0 : i32)\ + return\ + },\ + }\ + i@3 := copy ((e@1 as variant @0).0)\ + @0 := copy (i@3)\ + storage_dead(i@3)\ + return\ +} diff --git a/tests/llbc/generic/expected b/tests/llbc/generic/expected index e69de29bb2d1..75e0d7fa3baa 100644 --- a/tests/llbc/generic/expected +++ b/tests/llbc/generic/expected @@ -0,0 +1,44 @@ +pub enum core::option::Option =\ +| None()\ +| Some(0: T) + +pub fn test::add_opt(@1: @Adt0, @2: @Adt0) -> @Adt0\ +{\ + let @0: @Adt0; // return\ + let x@1: @Adt0; // arg #1\ + let y@2: @Adt0; // arg #2\ + let @3: isize; // anonymous local\ + let u@4: i32; // local\ + let @5: isize; // anonymous local\ + let v@6: i32; // local\ + let @7: i32; // anonymous local\ + let @8: (i32, bool); // anonymous local\ +\ + nop\ + match x@1 {\ + core::option::Option::Some => {\ + u@4 := copy ((x@1 as variant @1).0)\ + nop\ + match y@2 {\ + core::option::Option::Some => {\ + v@6 := copy ((y@2 as variant @1).0)\ + nop\ + nop\ + @7 := copy (u@4) + copy (v@6)\ + @0 := core::option::Option::Some { 0: move (@7) }\ + storage_dead(@7)\ + return\ + },\ + core::option::Option::None => {\ + @0 := core::option::Option::None { }\ + return\ + },\ + }\ + },\ + core::option::Option::None => {\ + @0 := core::option::Option::None { }\ + return\ + },\ + }\ + undefined_behavior\ +} diff --git a/tests/llbc/option/expected b/tests/llbc/option/expected index e69de29bb2d1..7dea7051bd70 100644 --- a/tests/llbc/option/expected +++ b/tests/llbc/option/expected @@ -0,0 +1,38 @@ +pub enum core::option::Option =\ +| None()\ +| Some(0: T) + +pub fn core::ptr::drop_glue<'_0, T>(@1: &'_0 mut (T)) + +pub fn test::both_none(@1: @Adt0, @2: @Adt0) -> bool\ +{\ + let @0: bool; // return\ + let a@1: @Adt0; // arg #1\ + let b@2: @Adt0; // arg #2\ + let @3: isize; // anonymous local\ + let @4: isize; // anonymous local\ +\ + nop\ + match a@1 {\ + core::option::Option::None => {\ + nop\ + match b@2 {\ + core::option::Option::None => {\ + @0 := const (true)\ + nop\ + },\ + core::option::Option::Some => {\ + @0 := const (false)\ + nop\ + },\ + }\ + },\ + core::option::Option::Some => {\ + @0 := const (false)\ + nop\ + },\ + }\ + drop b@2\ + drop a@1\ + return\ +} diff --git a/tests/llbc/projection/expected b/tests/llbc/projection/expected index e69de29bb2d1..b58a35285ba9 100644 --- a/tests/llbc/projection/expected +++ b/tests/llbc/projection/expected @@ -0,0 +1,78 @@ +pub enum test::MyEnum =\ +| A(0: @Adt1, 1: @Adt2)\ +| B(0: (i32, i32)) + +pub enum test::MyEnum0 =\ +| A(0: @Adt1, 1: i32)\ +| B() + +pub fn test::enum_match(@1: @Adt0) -> i32\ +{\ + let @0: i32; // return\ + let e@1: @Adt0; // arg #1\ + let @2: isize; // anonymous local\ + let s@3: @Adt1; // local\ + let e0@4: @Adt2; // local\ + let @5: isize; // anonymous local\ + let s1@6: @Adt1; // local\ + let b@7: i32; // local\ + let @8: i32; // anonymous local\ + let @9: (i32, bool); // anonymous local\ + let @10: i32; // anonymous local\ + let @11: i32; // anonymous local\ + let @12: (i32, bool); // anonymous local\ + let a@13: i32; // local\ + let b@14: i32; // local\ + let @15: (i32, bool); // anonymous local\ +\ + nop\ + match e@1 {\ + test::MyEnum::A => {\ + s@3 := move ((e@1 as variant @0).0)\ + e0@4 := move ((e@1 as variant @0).1)\ + nop\ + match e0@4 {\ + test::MyEnum0::A => {\ + s1@6 := move ((e0@4 as variant @0).0)\ + b@7 := copy ((e0@4 as variant @0).1)\ + @8 := copy ((s1@6).a)\ + nop\ + nop\ + @0 := copy (@8) + copy (b@7)\ + storage_dead(@8)\ + storage_dead(s1@6)\ + storage_dead(e0@4)\ + storage_dead(s@3)\ + return\ + },\ + test::MyEnum0::B => {\ + @10 := copy ((s@3).a)\ + @11 := copy ((s@3).b)\ + nop\ + nop\ + @0 := copy (@10) + copy (@11)\ + storage_dead(@11)\ + storage_dead(@10)\ + storage_dead(e0@4)\ + storage_dead(s@3)\ + return\ + },\ + }\ + },\ + test::MyEnum::B => {\ + a@13 := copy (((e@1 as variant @1).0).0)\ + b@14 := copy (((e@1 as variant @1).0).1)\ + nop\ + nop\ + @0 := copy (a@13) + copy (b@14)\ + return\ + },\ + }\ + undefined_behavior\ +} + +pub struct test::MyStruct =\ +{\ + a: i32,\ + b: i32,\ +} diff --git a/tests/llbc/struct/expected b/tests/llbc/struct/expected index e69de29bb2d1..f5e66a86f257 100644 --- a/tests/llbc/struct/expected +++ b/tests/llbc/struct/expected @@ -0,0 +1,14 @@ +pub fn test::struct_project(@1: @Adt0) -> i32\ +{\ + let @0: i32; // return\ + let s@1: @Adt0; // arg #1\ +\ + @0 := copy ((s@1).a)\ + return\ +} + +pub struct test::MyStruct =\ +{\ + a: i32,\ + b: bool,\ +} diff --git a/tests/llbc/traitimpl/expected b/tests/llbc/traitimpl/expected index e69de29bb2d1..44665cf4e7bb 100644 --- a/tests/llbc/traitimpl/expected +++ b/tests/llbc/traitimpl/expected @@ -0,0 +1,27 @@ +pub fn test::get_valA<'_0>(@1: &'_0 (@Adt1)) -> i32\ +{\ + let @0: i32; // return\ + let self@1: &'_ (@Adt1); // arg #1\ +\ + @0 := copy ((*(self@1)).val)\ + return\ +} + +pub fn test::get_valB<'_0>(@1: &'_0 (@Adt0)) -> i32\ +{\ + let @0: i32; // return\ + let self@1: &'_ (@Adt0); // arg #1\ +\ + @0 := copy ((*(self@1)).index)\ + return\ +} + +pub struct test::A =\ +{\ + val: i32,\ +} + +pub struct test::B =\ +{\ + index: i32,\ +} diff --git a/tests/llbc/tuple/expected b/tests/llbc/tuple/expected index e69de29bb2d1..b62479aee00f 100644 --- a/tests/llbc/tuple/expected +++ b/tests/llbc/tuple/expected @@ -0,0 +1,17 @@ +pub fn test::tuple_add(@1: (i32, i32)) -> i32\ +{\ + let @0: i32; // return\ + let t@1: (i32, i32); // arg #1\ + let @2: i32; // anonymous local\ + let @3: i32; // anonymous local\ + let @4: (i32, bool); // anonymous local\ +\ + @2 := copy ((t@1).0)\ + @3 := copy ((t@1).1)\ + nop\ + nop\ + @0 := copy (@2) + copy (@3)\ + storage_dead(@3)\ + storage_dead(@2)\ + return\ +} From 87a19aa28bf67b5feb4c6d31f113ba0e1507728b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 29 Sep 2026 14:29:22 +0000 Subject: [PATCH 3/3] LLBC: don't pin `@AdtN` ids in the projection and traitimpl expectations 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 c35cb962263 (nightly-2026-09-24). Co-authored-by: Kiro --- tests/llbc/projection/expected | 14 +++++++------- tests/llbc/traitimpl/expected | 8 ++++---- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/tests/llbc/projection/expected b/tests/llbc/projection/expected index b58a35285ba9..9d2836cdde33 100644 --- a/tests/llbc/projection/expected +++ b/tests/llbc/projection/expected @@ -1,20 +1,20 @@ pub enum test::MyEnum =\ -| A(0: @Adt1, 1: @Adt2)\ +| A(0: @Adt\ | B(0: (i32, i32)) pub enum test::MyEnum0 =\ -| A(0: @Adt1, 1: i32)\ +| A(0: @Adt\ | B() -pub fn test::enum_match(@1: @Adt0) -> i32\ +pub fn test::enum_match(@1: @Adt\ {\ let @0: i32; // return\ - let e@1: @Adt0; // arg #1\ + let e@1: @Adt\ let @2: isize; // anonymous local\ - let s@3: @Adt1; // local\ - let e0@4: @Adt2; // local\ + let s@3: @Adt\ + let e0@4: @Adt\ let @5: isize; // anonymous local\ - let s1@6: @Adt1; // local\ + let s1@6: @Adt\ let b@7: i32; // local\ let @8: i32; // anonymous local\ let @9: (i32, bool); // anonymous local\ diff --git a/tests/llbc/traitimpl/expected b/tests/llbc/traitimpl/expected index 44665cf4e7bb..498618bb1739 100644 --- a/tests/llbc/traitimpl/expected +++ b/tests/llbc/traitimpl/expected @@ -1,16 +1,16 @@ -pub fn test::get_valA<'_0>(@1: &'_0 (@Adt1)) -> i32\ +pub fn test::get_valA<'_0>(@1: &'_0 (@Adt\ {\ let @0: i32; // return\ - let self@1: &'_ (@Adt1); // arg #1\ + let self@1: &'_ (@Adt\ \ @0 := copy ((*(self@1)).val)\ return\ } -pub fn test::get_valB<'_0>(@1: &'_0 (@Adt0)) -> i32\ +pub fn test::get_valB<'_0>(@1: &'_0 (@Adt\ {\ let @0: i32; // return\ - let self@1: &'_ (@Adt0); // arg #1\ + let self@1: &'_ (@Adt\ \ @0 := copy ((*(self@1)).index)\ return\