diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index f0bd945d63ce..b1c7ec455bc5 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -142,7 +142,7 @@ pub enum ExprValue { StringConstant { s: InternedString, }, - /// Struct initializer + /// Struct initializer /// `struct foo the_foo = >>> {field1, field2, ... } <<<` Struct { values: Vec, @@ -153,7 +153,7 @@ pub enum ExprValue { }, /// `(typ) self`. Target type is in the outer `Expr` struct. Typecast(Expr), - /// Union initializer + /// Union initializer /// `union foo the_foo = >>> {.field = value } <<<` Union { value: Expr, @@ -703,7 +703,7 @@ impl Expr { expr!(StatementExpression { statements: ops }, typ) } - /// Internal helper function for Struct initalizer + /// Internal helper function for Struct initalizer /// `struct foo the_foo = >>> {.field1 = val1, .field2 = val2, ... } <<<` /// ALL fields must be given, including padding fn struct_expr_with_explicit_padding( @@ -720,7 +720,7 @@ impl Expr { expr!(Struct { values }, typ) } - /// Struct initializer + /// Struct initializer /// `struct foo the_foo = >>> {.field1 = val1, .field2 = val2, ... } <<<` /// Note that only the NON padding fields should be explicitly given. /// Padding fields are automatically inserted using the type from the `SymbolTable` @@ -786,7 +786,7 @@ impl Expr { Expr::struct_expr_from_values(typ, values, symbol_table) } - /// Struct initializer + /// Struct initializer /// `struct foo the_foo = >>> {field1, field2, ... } <<<` /// Note that only the NON padding fields should be explicitly given. /// Padding fields are automatically inserted using the type from the `SymbolTable` @@ -822,7 +822,7 @@ impl Expr { Expr::struct_expr_with_explicit_padding(typ, fields, values) } - /// Struct initializer + /// Struct initializer /// `struct foo the_foo = >>> {field1, padding2, field3, ... } <<<` /// Note that padding fields should be explicitly given. /// This would be used when the values and padding have already been combined, @@ -881,7 +881,7 @@ impl Expr { self.transmute_to(t, st) } - /// Union initializer + /// Union initializer /// `union foo the_foo = >>> {.field = value } <<<` pub fn union_expr>( typ: Type, @@ -1403,9 +1403,9 @@ impl Expr { ArithmeticOverflowResult { result, overflowed } } - /// Uses CBMC's add-with-overflow operation that performs a single addition + /// Uses CBMC's [binop]-with-overflow operation that performs a single arithmetic /// operation - /// `struct (T, bool) overflow(+, self, e)` where `T` is the type of `self` + /// `struct (T, bool) overflow(binop, self, e)` where `T` is the type of `self` /// Pseudocode: /// ``` /// struct overflow_result_t { @@ -1417,6 +1417,14 @@ impl Expr { /// overflow_result.overflowed = raw_result > maximum value of T; /// return overflow_result; /// ``` + pub fn overflow_op(self, op: BinaryOperator, e: Expr) -> Expr { + assert!( + matches!(op, OverflowResultMinus | OverflowResultMult | OverflowResultPlus), + "Expected an overflow operation, but found: `{op:?}`" + ); + self.binop(op, e) + } + pub fn add_overflow_result(self, e: Expr) -> Expr { self.binop(OverflowResultPlus, e) } @@ -1448,6 +1456,8 @@ impl Expr { /// `ArithmeticOverflowResult r; >>>r.overflowed = builtin_sub_overflow(self, e, &r.result)<<<` pub fn mul_overflow(self, e: Expr) -> ArithmeticOverflowResult { + // TODO: We should replace these calls by *overflow_result. + // https://github.com/model-checking/kani/issues/1483 let result = self.clone().mul(e.clone()); let overflowed = self.mul_overflow_p(e); ArithmeticOverflowResult { result, overflowed } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 6e63f2dfe70a..df89deb7cc59 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -5,8 +5,8 @@ use super::typ::{self, pointee_type}; use super::PropertyClass; use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::{ - arithmetic_overflow_result_type, ArithmeticOverflowResult, BuiltinFn, Expr, Location, Stmt, - Type, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, + arithmetic_overflow_result_type, ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, + Location, Stmt, Type, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, }; use rustc_middle::mir::{BasicBlock, Operand, Place}; use rustc_middle::ty::layout::LayoutOf; @@ -172,38 +172,6 @@ impl<'tcx> GotocCtx<'tcx> { }}; } - // Intrinsics of the form *_with_overflow - macro_rules! codegen_op_with_overflow { - ($f:ident) => {{ - let pt = self.place_ty(p); - let t = self.codegen_ty(pt); - let a = fargs.remove(0); - let b = fargs.remove(0); - let op_type = a.typ().clone(); - let res = a.$f(b); - // add to symbol table - let struct_tag = self.codegen_arithmetic_overflow_result_type(op_type.clone()); - assert_eq!(*res.typ(), struct_tag); - - // store the result in a temporary variable - let (var, decl) = self.decl_temp_variable(struct_tag, Some(res), loc); - // cast into result type - let e = Expr::struct_expr_from_values( - t.clone(), - vec![ - var.clone().member(ARITH_OVERFLOW_RESULT_FIELD, &self.symbol_table), - var.member(ARITH_OVERFLOW_OVERFLOWED_FIELD, &self.symbol_table) - .cast_to(Type::c_bool()), - ], - &self.symbol_table, - ); - self.codegen_expr_to_place( - p, - Expr::statement_expression(vec![decl, e.as_stmt(loc)], t), - ) - }}; - } - // Intrinsics which encode a simple arithmetic operation with overflow check macro_rules! codegen_op_with_overflow_check { ($f:ident) => {{ @@ -362,7 +330,9 @@ impl<'tcx> GotocCtx<'tcx> { } match intrinsic { - "add_with_overflow" => codegen_op_with_overflow!(add_overflow_result), + "add_with_overflow" => { + self.codegen_op_with_overflow(BinaryOperator::OverflowResultPlus, fargs, p, loc) + } "arith_offset" => self.codegen_offset(intrinsic, instance, fargs, p, loc), "assert_inhabited" => self.codegen_assert_intrinsic(instance, intrinsic, span), "assert_mem_uninitialized_valid" => { @@ -528,7 +498,9 @@ impl<'tcx> GotocCtx<'tcx> { "min_align_of_val" => codegen_size_align!(align), "minnumf32" => codegen_simple_intrinsic!(Fminf), "minnumf64" => codegen_simple_intrinsic!(Fmin), - "mul_with_overflow" => codegen_op_with_overflow!(mul_overflow_result), + "mul_with_overflow" => { + self.codegen_op_with_overflow(BinaryOperator::OverflowResultMult, fargs, p, loc) + } "nearbyintf32" => codegen_simple_intrinsic!(Nearbyintf), "nearbyintf64" => codegen_simple_intrinsic!(Nearbyint), "needs_drop" => codegen_intrinsic_const!(), @@ -615,7 +587,9 @@ impl<'tcx> GotocCtx<'tcx> { "size_of_val" => codegen_size_align!(size), "sqrtf32" => unstable_codegen!(codegen_simple_intrinsic!(Sqrtf)), "sqrtf64" => unstable_codegen!(codegen_simple_intrinsic!(Sqrt)), - "sub_with_overflow" => codegen_op_with_overflow!(sub_overflow_result), + "sub_with_overflow" => { + self.codegen_op_with_overflow(BinaryOperator::OverflowResultMinus, fargs, p, loc) + } "transmute" => self.codegen_intrinsic_transmute(fargs, ret_ty, p), "truncf32" => codegen_simple_intrinsic!(Truncf), "truncf64" => codegen_simple_intrinsic!(Trunc), @@ -719,6 +693,25 @@ impl<'tcx> GotocCtx<'tcx> { dividend_is_int_min.and(divisor_is_minus_one).not() } + /// Intrinsics of the form *_with_overflow + fn codegen_op_with_overflow( + &mut self, + binop: BinaryOperator, + mut fargs: Vec, + place: &Place<'tcx>, + loc: Location, + ) -> Stmt { + let place_ty = self.place_ty(place); + let result_type = self.codegen_ty(place_ty); + let left = fargs.remove(0); + let right = fargs.remove(0); + let res = self.codegen_binop_with_overflow(binop, left, right, result_type.clone(), loc); + self.codegen_expr_to_place( + place, + Expr::statement_expression(vec![res.as_stmt(loc)], result_type), + ) + } + fn codegen_exact_div(&mut self, mut fargs: Vec, p: &Place<'tcx>, loc: Location) -> Stmt { // Check for undefined behavior conditions defined in // https://doc.rust-lang.org/std/intrinsics/fn.exact_div.html diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index e47b0984d440..01dacb3b10d5 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -10,7 +10,10 @@ use crate::kani_middle::coercion::{ extract_unsize_casting, CoerceUnsizedInfo, CoerceUnsizedIterator, CoercionBase, }; use crate::unwrap_or_return_codegen_unimplemented; -use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type}; +use cbmc::goto_program::{ + arithmetic_overflow_result_type, BinaryOperator, Expr, Location, Stmt, Symbol, Type, + ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, +}; use cbmc::MachineModel; use cbmc::{btree_string_map, InternString, InternedString}; use num::bigint::BigInt; @@ -165,6 +168,37 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Generate code for a binary operation with an overflow and returns a tuple (res, overflow). + pub fn codegen_binop_with_overflow( + &mut self, + bin_op: BinaryOperator, + left: Expr, + right: Expr, + expected_typ: Type, + loc: Location, + ) -> Expr { + // Create CBMC result type and add to the symbol table. + let res_type = arithmetic_overflow_result_type(left.typ().clone()); + let tag = res_type.tag().unwrap(); + let struct_tag = + self.ensure_struct(tag, tag, |_, _| res_type.components().unwrap().clone()); + let res = left.overflow_op(bin_op, right); + // store the result in a temporary variable + let (var, decl) = self.decl_temp_variable(struct_tag, Some(res), loc); + // cast into result type + let cast = Expr::struct_expr_from_values( + expected_typ.clone(), + vec![ + var.clone().member(ARITH_OVERFLOW_RESULT_FIELD, &self.symbol_table), + var.member(ARITH_OVERFLOW_OVERFLOWED_FIELD, &self.symbol_table) + .cast_to(Type::c_bool()), + ], + &self.symbol_table, + ); + Expr::statement_expression(vec![decl, cast.as_stmt(loc)], expected_typ) + } + + /// Generate code for a binary arithmetic operation with UB / overflow checks in place. fn codegen_rvalue_checked_binary_op( &mut self, op: &BinOp, @@ -199,27 +233,33 @@ impl<'tcx> GotocCtx<'tcx> { match op { BinOp::Add => { - let res = ce1.add_overflow(ce2); - Expr::struct_expr_from_values( - self.codegen_ty(res_ty), - vec![res.result, res.overflowed.cast_to(Type::c_bool())], - &self.symbol_table, + let res_type = self.codegen_ty(res_ty); + self.codegen_binop_with_overflow( + BinaryOperator::OverflowResultPlus, + ce1, + ce2, + res_type, + Location::None, ) } BinOp::Sub => { - let res = ce1.sub_overflow(ce2); - Expr::struct_expr_from_values( - self.codegen_ty(res_ty), - vec![res.result, res.overflowed.cast_to(Type::c_bool())], - &self.symbol_table, + let res_type = self.codegen_ty(res_ty); + self.codegen_binop_with_overflow( + BinaryOperator::OverflowResultMinus, + ce1, + ce2, + res_type, + Location::None, ) } BinOp::Mul => { - let res = ce1.mul_overflow(ce2); - Expr::struct_expr_from_values( - self.codegen_ty(res_ty), - vec![res.result, res.overflowed.cast_to(Type::c_bool())], - &self.symbol_table, + let res_type = self.codegen_ty(res_ty); + self.codegen_binop_with_overflow( + BinaryOperator::OverflowResultMult, + ce1, + ce2, + res_type, + Location::None, ) } BinOp::Shl => { diff --git a/tests/ui/cbmc_checks/signed-overflow/expected b/tests/ui/cbmc_checks/signed-overflow/expected index 2922f224a5d1..b725337fbddb 100644 --- a/tests/ui/cbmc_checks/signed-overflow/expected +++ b/tests/ui/cbmc_checks/signed-overflow/expected @@ -7,12 +7,7 @@ Failed Checks: attempt to calculate the remainder with a divisor of zero Failed Checks: attempt to calculate the remainder with overflow Failed Checks: attempt to shift left with overflow Failed Checks: attempt to shift right with overflow -Failed Checks: arithmetic overflow on signed addition -Failed Checks: arithmetic overflow on signed subtraction -Failed Checks: arithmetic overflow on signed multiplication -Failed Checks: shift distance is negative -Failed Checks: shift distance too large -Failed Checks: shift operand is negative Failed Checks: arithmetic overflow on signed shl +Failed Checks: shift operand is negative Failed Checks: shift distance is negative -Failed Checks: shift distance too large +Failed Checks: shift distance too large \ No newline at end of file diff --git a/tests/ui/cbmc_checks/unsigned-overflow/expected b/tests/ui/cbmc_checks/unsigned-overflow/expected index b9cde3bb478b..ef0f06506b36 100644 --- a/tests/ui/cbmc_checks/unsigned-overflow/expected +++ b/tests/ui/cbmc_checks/unsigned-overflow/expected @@ -1,7 +1,8 @@ Failed Checks: attempt to divide by zero Failed Checks: attempt to calculate the remainder with a divisor of zero -Failed Checks: arithmetic overflow on unsigned addition -Failed Checks: arithmetic overflow on unsigned subtraction -Failed Checks: arithmetic overflow on unsigned multiplication -Failed Checks: shift distance too large +Failed Checks: attempt to add with overflow +Failed Checks: attempt to subtract with overflow +Failed Checks: attempt to multiply with overflow +Failed Checks: attempt to shift right with overflow +Failed Checks: attempt to shift left with overflow Failed Checks: shift distance too large