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.

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

Use optimized overflow operation everywhere #2405

Merged
merged 7 commits into from
Apr 28, 2023
Merged
Changes from 4 commits
Commits
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
13 changes: 11 additions & 2 deletions cprover_bindings/src/goto_program/expr.rs
Original file line number Diff line number Diff line change
@@ -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
tautschnig marked this conversation as resolved.
Show resolved Hide resolved
/// 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,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 }
celinval marked this conversation as resolved.
Show resolved Hide resolved
67 changes: 30 additions & 37 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
@@ -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<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
72 changes: 56 additions & 16 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
@@ -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 => {
9 changes: 1 addition & 8 deletions tests/ui/cbmc_checks/signed-overflow/expected
Original file line number Diff line number Diff line change
@@ -7,12 +7,5 @@ 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 distance is negative
Failed Checks: shift distance too large
tautschnig marked this conversation as resolved.
Show resolved Hide resolved
Failed Checks: shift operand is negative
10 changes: 5 additions & 5 deletions tests/ui/cbmc_checks/unsigned-overflow/expected
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
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: 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