Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Use CBMC's arithmetic operators that return both the result and whether it overflowed #1426

Merged
merged 7 commits into from
Aug 9, 2022
Merged

Use CBMC's arithmetic operators that return both the result and whether it overflowed #1426

Show file tree
Hide file tree
Changes from 6 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
894ef5d
Use CBMC's arithmetic operators that return both the result and wheth…
zhassan-aws Jul 28, 2022
3c1b18e
Make clippy happy
zhassan-aws Jul 29, 2022
abe24df
Address PR comments
zhassan-aws Jul 29, 2022
6cee49e
Add helper function
zhassan-aws Aug 2, 2022
21001c9
Merge branch 'main' into arithmetic-overflow-result
zhassan-aws Aug 2, 2022
45477f3
Add documentation for method
zhassan-aws Aug 2, 2022
f7db2d0
Merge branch 'main' into arithmetic-overflow-result
tedinski Aug 9, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
65 changes: 63 additions & 2 deletions cprover_bindings/src/goto_program/expr.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -184,6 +184,9 @@ pub enum BinaryOperator {
OverflowMinus,
OverflowMult,
OverflowPlus,
OverflowResultMinus,
OverflowResultMult,
OverflowResultPlus,
Plus,
ROk,
Rol,
Expand Down Expand Up @@ -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_<type>", 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
///////////////////////////////////////////////////////////////////////////////////////////////
Expand Down Expand Up @@ -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())
}
Expand Down Expand Up @@ -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(),
}
}
Expand Down Expand Up @@ -1297,6 +1324,24 @@ impl Expr {
ArithmeticOverflowResult { result, overflowed }
}

/// Uses CBMC's add-with-overflow operation that performs a single addition
/// operation
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Give C or pseudocode example

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done.

/// `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());
Expand Down Expand Up @@ -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<uin32_t>(1.0) == 0x3f800000`
Expand All @@ -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())
Expand Down
3 changes: 2 additions & 1 deletion cprover_bindings/src/goto_program/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down
6 changes: 6 additions & 0 deletions cprover_bindings/src/irep/irep_id.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -463,6 +463,9 @@ pub enum IrepId {
OverflowPlus,
OverflowMinus,
OverflowMult,
OverflowResultPlus,
OverflowResultMinus,
OverflowResultMult,
OverflowUnaryMinus,
ObjectDescriptor,
IsDynamicObject,
Expand Down Expand Up @@ -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",
Expand Down
3 changes: 3 additions & 0 deletions cprover_bindings/src/irep/to_irep.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
79 changes: 66 additions & 13 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -181,13 +184,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),
)
}};
}

Expand All @@ -196,15 +214,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(),
Comment on lines 230 to +234
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Were you going to split this off?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This case wasn't difficult to handle. The other cases, e.g. in count_in_bytes, codegen_ptr_offset_from_expr, and codegen_ptr_offset_from_unsigned are a bit more challenging, and I'm splitting those off to a later PR.

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

Expand Down Expand Up @@ -391,7 +429,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),
Expand Down Expand Up @@ -555,7 +593,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!(),
Expand Down Expand Up @@ -620,7 +658,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),
Expand All @@ -634,9 +672,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" => {
Expand All @@ -646,7 +684,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`"
Expand Down Expand Up @@ -1451,4 +1489,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> {
/// 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()
})
}
}