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

Add unchecked/SIMD bitshift checks and disable CBMC flag #2630

Merged
merged 8 commits into from
Jul 31, 2023
Merged
Show file tree
Hide file tree
Changes from all 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
81 changes: 71 additions & 10 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -538,16 +538,8 @@ impl<'tcx> GotocCtx<'tcx> {
// TODO: `simd_div` and `simd_rem` don't check for overflow cases.
// <https://github.com/model-checking/kani/issues/1970>
"simd_rem" => codegen_intrinsic_binop!(rem),
// TODO: `simd_shl` and `simd_shr` don't check overflow cases.
// <https://github.com/model-checking/kani/issues/1963>
"simd_shl" => codegen_intrinsic_binop!(shl),
"simd_shr" => {
if fargs[0].typ().base_type().unwrap().is_signed(self.symbol_table.machine_model())
{
codegen_intrinsic_binop!(ashr)
} else {
codegen_intrinsic_binop!(lshr)
}
"simd_shl" | "simd_shr" => {
self.codegen_simd_shift_with_distance_check(fargs, intrinsic, p, loc)
}
// "simd_shuffle#" => handled in an `if` preceding this match
"simd_sub" => self.codegen_simd_op_with_overflow(
Expand Down Expand Up @@ -1560,6 +1552,75 @@ impl<'tcx> GotocCtx<'tcx> {
Stmt::block(vec![expr_place, check_stmt], loc)
}

/// Intrinsics which encode a SIMD bitshift.
/// Also checks for valid shift distance. Shifts on an integer of type T are UB if shift
/// distance < 0 or >= T::BITS.
fn codegen_simd_shift_with_distance_check(
&mut self,
mut fargs: Vec<Expr>,
intrinsic: &str,
p: &Place<'tcx>,
loc: Location,
) -> Stmt {
let values = fargs.remove(0);
let distances = fargs.remove(0);

let values_len = values.typ().len().unwrap();
let distances_len = distances.typ().len().unwrap();
assert_eq!(values_len, distances_len, "expected same length vectors");

let value_type = values.typ().base_type().unwrap();
let distance_type = distances.typ().base_type().unwrap();
let value_width = value_type.sizeof_in_bits(&self.symbol_table);
let value_width_expr = Expr::int_constant(value_width, distance_type.clone());
let distance_is_signed = distance_type.is_signed(self.symbol_table.machine_model());

let mut excessive_check = Expr::bool_false();
let mut negative_check = Expr::bool_false();
for i in 0..distances_len {
let index = Expr::int_constant(i, Type::ssize_t());
let distance = distances.clone().index_array(index);
let excessive_distance_cond = distance.clone().ge(value_width_expr.clone());
excessive_check = excessive_check.or(excessive_distance_cond);
if distance_is_signed {
let negative_distance_cond = distance.is_negative();
negative_check = negative_check.or(negative_distance_cond);
}
}
let excessive_check_stmt = self.codegen_assert_assume(
excessive_check.not(),
PropertyClass::ArithmeticOverflow,
format!("attempt {intrinsic} with excessive shift distance").as_str(),
loc,
);

let op_fun = match intrinsic {
"simd_shl" => Expr::shl,
"simd_shr" => {
if distance_is_signed {
Expr::ashr
} else {
Expr::lshr
}
}
_ => unreachable!("expected a simd shift intrinsic"),
};
let res = op_fun(values, distances);
let expr_place = self.codegen_expr_to_place(p, res);

if distance_is_signed {
let negative_check_stmt = self.codegen_assert_assume(
negative_check.not(),
PropertyClass::ArithmeticOverflow,
format!("attempt {intrinsic} with negative shift distance").as_str(),
loc,
);
Stmt::block(vec![excessive_check_stmt, negative_check_stmt, expr_place], loc)
} else {
Stmt::block(vec![excessive_check_stmt, expr_place], loc)
}
}

/// `simd_shuffle` constructs a new vector from the elements of two input
/// vectors, choosing values according to an input array of indexes.
///
Expand Down
54 changes: 49 additions & 5 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -116,6 +116,14 @@ impl<'tcx> GotocCtx<'tcx> {
BinOp::BitXor => ce1.bitxor(ce2),
BinOp::Div => ce1.div(ce2),
BinOp::Rem => ce1.rem(ce2),
BinOp::ShlUnchecked => ce1.shl(ce2),
BinOp::ShrUnchecked => {
if self.operand_ty(e1).is_signed() {
ce1.ashr(ce2)
} else {
ce1.lshr(ce2)
}
}
_ => unreachable!("Unexpected {:?}", op),
}
}
Expand Down Expand Up @@ -343,11 +351,14 @@ impl<'tcx> GotocCtx<'tcx> {
BinOp::Add | BinOp::Sub | BinOp::Mul | BinOp::Shl | BinOp::Shr => {
self.codegen_scalar_binop(op, e1, e2)
}
// We currently rely on CBMC's UB checks for shift which isn't always accurate.
// We should implement the checks ourselves.
// See https://github.com/model-checking/kani/issues/2374
BinOp::ShlUnchecked => self.codegen_scalar_binop(&BinOp::Shl, e1, e2),
BinOp::ShrUnchecked => self.codegen_scalar_binop(&BinOp::Shr, e1, e2),
BinOp::ShlUnchecked | BinOp::ShrUnchecked => {
let result = self.codegen_unchecked_scalar_binop(op, e1, e2);
let check = self.check_unchecked_shift_distance(e1, e2, loc);
Expr::statement_expression(
vec![check, result.clone().as_stmt(loc)],
result.typ().clone(),
)
}
BinOp::AddUnchecked | BinOp::MulUnchecked | BinOp::SubUnchecked => {
self.codegen_binop_with_overflow_check(op, e1, e2, loc)
}
Expand Down Expand Up @@ -455,6 +466,39 @@ impl<'tcx> GotocCtx<'tcx> {
}
}

/// Check for valid unchecked shift distance.
/// Shifts on an integer of type T are UB if shift distance < 0 or >= T::BITS.
fn check_unchecked_shift_distance(
&mut self,
value: &Operand<'tcx>,
distance: &Operand<'tcx>,
loc: Location,
) -> Stmt {
let value_expr = self.codegen_operand(value);
let distance_expr = self.codegen_operand(distance);
let value_width = value_expr.typ().sizeof_in_bits(&self.symbol_table);
let value_width_expr = Expr::int_constant(value_width, distance_expr.typ().clone());

let excessive_distance_check = self.codegen_assert_assume(
distance_expr.clone().lt(value_width_expr),
PropertyClass::ArithmeticOverflow,
"attempt to shift by excessive shift distance",
loc,
);

if distance_expr.typ().is_signed(self.symbol_table.machine_model()) {
let negative_distance_check = self.codegen_assert_assume(
distance_expr.is_non_negative(),
PropertyClass::ArithmeticOverflow,
"attempt to shift by negative distance",
loc,
);
Stmt::block(vec![negative_distance_check, excessive_distance_check], loc)
} else {
excessive_distance_check
}
}

/// Create an initializer for a generator struct.
fn codegen_rvalue_generator(
&mut self,
Expand Down
1 change: 0 additions & 1 deletion kani-driver/src/call_cbmc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -167,7 +167,6 @@ impl KaniSession {
args.push("--div-by-zero-check".into());
args.push("--float-overflow-check".into());
args.push("--nan-check".into());
args.push("--undefined-shift-check".into());
// With PR #647 we use Rust's `-C overflow-checks=on` instead of:
// --unsigned-overflow-check
// --signed-overflow-check
Expand Down

This file was deleted.

27 changes: 0 additions & 27 deletions tests/expected/intrinsics/simd-shl-operand-negative/main.rs

This file was deleted.

Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
FAILURE\
shift distance is negative
attempt simd_shl with negative shift distance
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,6 @@ extern "platform-intrinsic" {
#[kani::proof]
fn test_simd_shl() {
let value = kani::any();
kani::assume(value >= 0);
let values = i32x2(value, value);
let shift = kani::any();
kani::assume(shift < 32);
Expand Down
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
FAILURE\
shift distance too large
attempt simd_shl with excessive shift distance
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,6 @@ extern "platform-intrinsic" {
#[kani::proof]
fn test_simd_shl() {
let value = kani::any();
kani::assume(value >= 0);
let values = i32x2(value, value);
let shift = kani::any();
kani::assume(shift >= 0);
Expand Down
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
FAILURE\
shift distance is negative
attempt simd_shr with negative shift distance
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,6 @@ extern "platform-intrinsic" {
#[kani::proof]
fn test_simd_shr() {
let value = kani::any();
kani::assume(value >= 0);
let values = i32x2(value, value);
let shift = kani::any();
kani::assume(shift < 32);
Expand Down
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
FAILURE\
shift distance too large
attempt simd_shr with excessive shift distance
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,6 @@ extern "platform-intrinsic" {
#[kani::proof]
fn test_simd_shr() {
let value = kani::any();
kani::assume(value >= 0);
let values = i32x2(value, value);
let shift = kani::any();
kani::assume(shift >= 0);
Expand Down
23 changes: 23 additions & 0 deletions tests/kani/BitwiseShiftOperators/shift_neg_vals.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//
// Ensure that shifting negative values yields the expected results.

#[kani::proof]
#[kani::unwind(5)]
fn sheck_shl() {
let val: i32 = kani::any();
let dist: u8 = kani::any();
kani::assume(dist < 32);
assert_eq!(val << dist, val.wrapping_mul(2_i32.wrapping_pow(dist.into())));
}

#[kani::proof]
#[kani::unwind(5)]
fn check_shr() {
let val: i32 = kani::any();
let dist: u8 = kani::any();
kani::assume(dist < 32);
let result = (val as i64).div_euclid(2_i64.pow(dist.into()));
assert_eq!(val >> dist, result as i32);
}
1 change: 0 additions & 1 deletion tests/kani/Intrinsics/SIMD/Operators/bitshift.rs
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,6 @@ extern "platform-intrinsic" {
#[kani::proof]
fn test_simd_shl() {
let value = kani::any();
kani::assume(value >= 0);
let values = i32x2(value, value);
let shift = kani::any();
kani::assume(shift >= 0);
Expand Down
1 change: 0 additions & 1 deletion tests/ui/cbmc_checks/signed-overflow/expected
Original file line number Diff line number Diff line change
Expand Up @@ -8,4 +8,3 @@ 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 shl
Failed Checks: shift operand is negative
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
undefined-shift\
arithmetic_overflow\
Status: FAILURE\
Description: "shift distance too large"
Description: "attempt to shift by excessive shift distance"

Failed Checks: panicked on the `1` arm!
Failed Checks: panicked on the `0` arm!
Failed Checks: shift distance too large
Failed Checks: attempt to shift by excessive shift distance

VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected)
Loading