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/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/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/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..9d2836cdde33 100644 --- a/tests/llbc/projection/expected +++ b/tests/llbc/projection/expected @@ -0,0 +1,78 @@ +pub enum test::MyEnum =\ +| A(0: @Adt\ +| B(0: (i32, i32)) + +pub enum test::MyEnum0 =\ +| A(0: @Adt\ +| B() + +pub fn test::enum_match(@1: @Adt\ +{\ + let @0: i32; // return\ + let e@1: @Adt\ + let @2: isize; // anonymous local\ + let s@3: @Adt\ + let e0@4: @Adt\ + let @5: isize; // anonymous local\ + let s1@6: @Adt\ + 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/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/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/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/traitimpl/expected b/tests/llbc/traitimpl/expected index e69de29bb2d1..498618bb1739 100644 --- a/tests/llbc/traitimpl/expected +++ b/tests/llbc/traitimpl/expected @@ -0,0 +1,27 @@ +pub fn test::get_valA<'_0>(@1: &'_0 (@Adt\ +{\ + let @0: i32; // return\ + let self@1: &'_ (@Adt\ +\ + @0 := copy ((*(self@1)).val)\ + return\ +} + +pub fn test::get_valB<'_0>(@1: &'_0 (@Adt\ +{\ + let @0: i32; // return\ + let self@1: &'_ (@Adt\ +\ + @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\ +} 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); +}