diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index ab944957bd18..4f04094f7bf7 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -184,6 +184,9 @@ pub enum BinaryOperator { OverflowMinus, OverflowMult, OverflowPlus, + OverflowResultMinus, + OverflowResultMult, + OverflowResultPlus, Plus, ROk, Rol, @@ -243,6 +246,26 @@ pub struct ArithmeticOverflowResult { pub overflowed: Expr, } +pub const ARITH_OVERFLOW_RESULT_FIELD: &str = "result"; +pub const ARITH_OVERFLOW_OVERFLOWED_FIELD: &str = "overflowed"; + +/// For arithmetic-overflow-with-result operators, CBMC returns a struct whose +/// first component is the result, and whose second component is whether the +/// operation overflowed +pub fn arithmetic_overflow_result_type(operand_type: Type) -> Type { + assert!(operand_type.is_integer()); + // give the struct the name "overflow_result_", e.g. + // "overflow_result_Unsignedbv" + let name: InternedString = format!("overflow_result_{:?}", operand_type).into(); + Type::struct_type( + name, + vec![ + DatatypeComponent::field(ARITH_OVERFLOW_RESULT_FIELD, operand_type), + DatatypeComponent::field(ARITH_OVERFLOW_OVERFLOWED_FIELD, Type::bool()), + ], + ) +} + /////////////////////////////////////////////////////////////////////////////////////////////// /// Implementations /////////////////////////////////////////////////////////////////////////////////////////////// @@ -898,11 +921,11 @@ impl Expr { // Floating Point Equalities IeeeFloatEqual | IeeeFloatNotequal => lhs.typ == rhs.typ && lhs.typ.is_floating_point(), // Overflow flags - OverflowMinus => { + OverflowMinus | OverflowResultMinus => { (lhs.typ == rhs.typ && (lhs.typ.is_pointer() || lhs.typ.is_numeric())) || (lhs.typ.is_pointer() && rhs.typ.is_integer()) } - OverflowMult | OverflowPlus => { + OverflowMult | OverflowPlus | OverflowResultMult | OverflowResultPlus => { (lhs.typ == rhs.typ && lhs.typ.is_integer()) || (lhs.typ.is_pointer() && rhs.typ.is_integer()) } @@ -948,6 +971,10 @@ impl Expr { IeeeFloatEqual | IeeeFloatNotequal => Type::bool(), // Overflow flags OverflowMinus | OverflowMult | OverflowPlus => Type::bool(), + OverflowResultMinus | OverflowResultMult | OverflowResultPlus => { + let struct_type = arithmetic_overflow_result_type(lhs.typ.clone()); + Type::struct_tag(struct_type.tag().unwrap()) + } ROk => Type::bool(), } } @@ -1297,6 +1324,24 @@ impl Expr { ArithmeticOverflowResult { result, overflowed } } + /// Uses CBMC's add-with-overflow operation that performs a single addition + /// operation + /// `struct (T, bool) overflow(+, self, e)` where `T` is the type of `self` + /// Pseudocode: + /// ``` + /// struct overflow_result_t { + /// T result; + /// bool overflowed; + /// } overflow_result; + /// raw_result = (cast to wider type) self + (cast to wider type) e; + /// overflow_result.result = (cast to T) raw_result; + /// overflow_result.overflowed = raw_result > maximum value of T; + /// return overflow_result; + /// ``` + pub fn add_overflow_result(self, e: Expr) -> Expr { + self.binop(OverflowResultPlus, e) + } + /// `&self[0]`. Converts arrays into pointers pub fn array_to_ptr(self) -> Self { assert!(self.typ().is_array_like()); @@ -1329,6 +1374,14 @@ impl Expr { ArithmeticOverflowResult { result, overflowed } } + /// Uses CBMC's multiply-with-overflow operation that performs a single + /// multiplication operation + /// `struct (T, bool) overflow(*, self, e)` where `T` is the type of `self` + /// See pseudocode in `add_overflow_result` + pub fn mul_overflow_result(self, e: Expr) -> Expr { + self.binop(OverflowResultMult, e) + } + /// Reinterpret the bits of `self` as being of type `t`. /// Note that this differs from standard casts, which may convert values. /// in C++ syntax: `(uint32_t)(1.0) == 1`, while `reinterpret_cast(1.0) == 0x3f800000` @@ -1352,6 +1405,14 @@ impl Expr { ArithmeticOverflowResult { result, overflowed } } + /// Uses CBMC's subtract-with-overflow operation that performs a single + /// subtraction operation + /// See pseudocode in `add_overflow_result` + /// `struct (T, bool) overflow(-, self, e)` where `T` is the type of `self` + pub fn sub_overflow_result(self, e: Expr) -> Expr { + self.binop(OverflowResultMinus, e) + } + /// `__CPROVER_same_object(self, e)` pub fn same_object(self, e: Expr) -> Self { self.pointer_object().eq(e.pointer_object()) diff --git a/cprover_bindings/src/goto_program/mod.rs b/cprover_bindings/src/goto_program/mod.rs index 6a65972909f0..e72c66414f32 100644 --- a/cprover_bindings/src/goto_program/mod.rs +++ b/cprover_bindings/src/goto_program/mod.rs @@ -18,7 +18,8 @@ mod typ; pub use builtin::BuiltinFn; pub use expr::{ - ArithmeticOverflowResult, BinaryOperator, Expr, ExprValue, SelfOperator, UnaryOperator, + arithmetic_overflow_result_type, ArithmeticOverflowResult, BinaryOperator, Expr, ExprValue, + SelfOperator, UnaryOperator, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, }; pub use location::Location; pub use stmt::{Stmt, StmtBody, SwitchCase}; diff --git a/cprover_bindings/src/irep/irep_id.rs b/cprover_bindings/src/irep/irep_id.rs index 41cd7718f947..c4280a28be47 100644 --- a/cprover_bindings/src/irep/irep_id.rs +++ b/cprover_bindings/src/irep/irep_id.rs @@ -463,6 +463,9 @@ pub enum IrepId { OverflowPlus, OverflowMinus, OverflowMult, + OverflowResultPlus, + OverflowResultMinus, + OverflowResultMult, OverflowUnaryMinus, ObjectDescriptor, IsDynamicObject, @@ -1322,6 +1325,9 @@ impl ToString for IrepId { IrepId::OverflowPlus => "overflow-+", IrepId::OverflowMinus => "overflow--", IrepId::OverflowMult => "overflow-*", + IrepId::OverflowResultPlus => "overflow_result-+", + IrepId::OverflowResultMinus => "overflow_result--", + IrepId::OverflowResultMult => "overflow_result-*", IrepId::OverflowUnaryMinus => "overflow-unary-", IrepId::ObjectDescriptor => "object_descriptor", IrepId::IsDynamicObject => "is_dynamic_object", diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index e40ea58994ff..5e1fa5f40f2f 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -75,6 +75,9 @@ impl ToIrepId for BinaryOperator { BinaryOperator::OverflowMinus => IrepId::OverflowMinus, BinaryOperator::OverflowMult => IrepId::OverflowMult, BinaryOperator::OverflowPlus => IrepId::OverflowPlus, + BinaryOperator::OverflowResultMinus => IrepId::OverflowResultMinus, + BinaryOperator::OverflowResultMult => IrepId::OverflowResultMult, + BinaryOperator::OverflowResultPlus => IrepId::OverflowResultPlus, BinaryOperator::Plus => IrepId::Plus, BinaryOperator::ROk => IrepId::ROk, BinaryOperator::Rol => IrepId::Rol, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 2920f69f11ee..ec536a9c2f69 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -4,7 +4,10 @@ use super::typ::pointee_type; use super::PropertyClass; use crate::codegen_cprover_gotoc::GotocCtx; -use cbmc::goto_program::{ArithmeticOverflowResult, BuiltinFn, Expr, Location, Stmt, Type}; +use cbmc::goto_program::{ + arithmetic_overflow_result_type, ArithmeticOverflowResult, 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; use rustc_middle::ty::{self, Ty}; @@ -186,13 +189,28 @@ impl<'tcx> GotocCtx<'tcx> { 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, - vec![res.result, res.overflowed.cast_to(Type::c_bool())], + 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, e) + self.codegen_expr_to_place( + p, + Expr::statement_expression(vec![decl, e.as_stmt(loc)], t), + ) }}; } @@ -201,15 +219,35 @@ impl<'tcx> GotocCtx<'tcx> { ($f:ident) => {{ 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); let check = self.codegen_assert( - res.overflowed.not(), + var.clone() + .member(ARITH_OVERFLOW_OVERFLOWED_FIELD, &self.symbol_table) + .cast_to(Type::c_bool()) + .not(), PropertyClass::ArithmeticOverflow, format!("attempt to compute {} which would overflow", intrinsic).as_str(), loc, ); - let expr_place = self.codegen_expr_to_place(p, res.result); - Stmt::block(vec![expr_place, check], loc) + self.codegen_expr_to_place( + p, + Expr::statement_expression( + vec![ + decl, + check, + var.member(ARITH_OVERFLOW_RESULT_FIELD, &self.symbol_table) + .as_stmt(loc), + ], + op_type, + ), + ) }}; } @@ -396,7 +434,7 @@ impl<'tcx> GotocCtx<'tcx> { } match intrinsic { - "add_with_overflow" => codegen_op_with_overflow!(add_overflow), + "add_with_overflow" => codegen_op_with_overflow!(add_overflow_result), "arith_offset" => self.codegen_offset(intrinsic, instance, fargs, p, loc), "assert_inhabited" => self.codegen_assert_intrinsic(instance, intrinsic, span), "assert_uninit_valid" => self.codegen_assert_intrinsic(instance, intrinsic, span), @@ -560,7 +598,7 @@ 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), + "mul_with_overflow" => codegen_op_with_overflow!(mul_overflow_result), "nearbyintf32" => codegen_simple_intrinsic!(Nearbyintf), "nearbyintf64" => codegen_simple_intrinsic!(Nearbyint), "needs_drop" => codegen_intrinsic_const!(), @@ -625,7 +663,7 @@ 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), + "sub_with_overflow" => codegen_op_with_overflow!(sub_overflow_result), "transmute" => self.codegen_intrinsic_transmute(fargs, ret_ty, p), "truncf32" => codegen_simple_intrinsic!(Truncf), "truncf64" => codegen_simple_intrinsic!(Trunc), @@ -639,9 +677,9 @@ impl<'tcx> GotocCtx<'tcx> { "unaligned_volatile_load" => { unstable_codegen!(self.codegen_expr_to_place(p, fargs.remove(0).dereference())) } - "unchecked_add" => codegen_op_with_overflow_check!(add_overflow), + "unchecked_add" => codegen_op_with_overflow_check!(add_overflow_result), "unchecked_div" => codegen_op_with_div_overflow_check!(div), - "unchecked_mul" => codegen_op_with_overflow_check!(mul_overflow), + "unchecked_mul" => codegen_op_with_overflow_check!(mul_overflow_result), "unchecked_rem" => codegen_op_with_div_overflow_check!(rem), "unchecked_shl" => codegen_intrinsic_binop!(shl), "unchecked_shr" => { @@ -651,7 +689,7 @@ impl<'tcx> GotocCtx<'tcx> { codegen_intrinsic_binop!(lshr) } } - "unchecked_sub" => codegen_op_with_overflow_check!(sub_overflow), + "unchecked_sub" => codegen_op_with_overflow_check!(sub_overflow_result), "unlikely" => self.codegen_expr_to_place(p, fargs.remove(0)), "unreachable" => unreachable!( "Expected `std::intrinsics::unreachable` to be handled by `TerminatorKind::Unreachable`" @@ -1456,4 +1494,19 @@ impl<'tcx> GotocCtx<'tcx> { ); (size_of_count_elems.result, assert_stmt) } + + /// Codegens the struct type that CBMC produces for its arithmetic with overflow operators: + /// ``` + /// struct overflow_result_ { + /// operand_type result; // the result of the operation + /// bool overflowed; // whether the operation overflowed + /// } + /// ``` + /// and adds the type to the symbol table + fn codegen_arithmetic_overflow_result_type(&mut self, operand_type: Type) -> Type { + let res_type = arithmetic_overflow_result_type(operand_type); + self.ensure_struct(res_type.tag().unwrap(), res_type.tag().unwrap(), |_, _| { + res_type.components().unwrap().clone() + }) + } }