LLBC: translate wrapping arithmetic as wrapping, and cover what the Charon bump will touch

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,

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\
+}

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);
+}

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\
+}

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);
+}

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\
+}

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);
+}

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\
+}

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();
+}

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\
+}

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);
+}

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\
+}

tests/llbc/generic/expected

@@ -0,0 +1,44 @@
+pub enum core::option::Option<T> =\
+|  None()\
+|  Some(0: T)
+
+pub fn test::add_opt(@1: @Adt0<i32>, @2: @Adt0<i32>) -> @Adt0<i32>\
+{\
+    let @0: @Adt0<i32>; // return\
+    let x@1: @Adt0<i32>; // arg #1\
+    let y@2: @Adt0<i32>; // 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\
+}

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\
+}