Skip to content

Commit

Permalink
Use optimized overflow operation everywhere
Browse files Browse the repository at this point in the history 
This is related to the performance degradation we are seeing in the
toolchain upgrade: model-checking#2293
  • Loading branch information
@celinval
celinval committed Apr 25, 2023
1 parent b5c116d commit d7fd6ec
Show file tree
Hide file tree
Showing 3 changed files with 97 additions and 55 deletions.
13 changes: 11 additions & 2 deletions cprover_bindings/src/goto_program/expr.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 addition
/// 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 {
Expand All @@ -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)
}
Expand Down Expand Up @@ -1448,6 +1456,7 @@ impl Expr {

/// `ArithmeticOverflowResult r; >>>r.overflowed = builtin_sub_overflow(self, e, &r.result)<<<`
pub fn mul_overflow(self, e: Expr) -> ArithmeticOverflowResult {
// TODO: Should we always use the one below?
let result = self.clone().mul(e.clone());
let overflowed = self.mul_overflow_p(e);
ArithmeticOverflowResult { result, overflowed }
Expand Down
67 changes: 30 additions & 37 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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) => {{
Expand Down Expand Up @@ -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" => {
Expand Down Expand Up @@ -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!(),
Expand Down Expand Up @@ -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),
Expand Down Expand Up @@ -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<Expr>,
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<Expr>, p: &Place<'tcx>, loc: Location) -> Stmt {
// Check for undefined behavior conditions defined in
// https://doc.rust-lang.org/std/intrinsics/fn.exact_div.html
Expand Down
72 changes: 56 additions & 16 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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 => {
Expand Down

0 comments on commit d7fd6ec

Please sign in to comment.