Skip to content

Commit

Permalink
Fix issue #1505 (#1511)
Browse files Browse the repository at this point in the history
* Add regression test for issue #1505
* Fix encoding of signed integer divisions
  • Loading branch information
fpoli authored Mar 26, 2024
1 parent 528f4c2 commit 0d4a8d4
Show file tree
Hide file tree
Showing 4 changed files with 95 additions and 5 deletions.
57 changes: 57 additions & 0 deletions prusti-tests/tests/verify_overflow/fail/issues/issue-1505.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
use prusti_contracts::*;

// To inhibit constant-propagation optimizations:
#[pure]
fn id<T: Copy>(x: T) -> T { x }

fn check_division(){
assert!(id(3i32) / 2 == 1);
assert!(id(-3i32) / 2 == -1);
assert!(id(3i32) / -2 == -1);
assert!(id(-3i32) / -2 == 1);
prusti_assert!(id(3i32) / 2 == 1);
prusti_assert!(id(-3i32) / 2 == -1);
prusti_assert!(id(3i32) / -2 == -1);
prusti_assert!(id(-3i32) / -2 == 1);

// Smoke test
assert!(false); //~ ERROR the asserted expression might not hold
}

fn check_modulo() {
assert!(id(10) % 3 == 1);
assert!(id(10) % -3 == 1);
assert!(id(-10) % 3 == -1);
assert!(id(-10) % -3 == -1);
prusti_assert!(id(10) % 3 == 1);
prusti_assert!(id(10) % -3 == 1);
prusti_assert!(id(-10) % 3 == -1);
prusti_assert!(id(-10) % -3 == -1);

assert!(id(3) % 3 == 0);
assert!(id(2) % 3 == 2);
assert!(id(1) % 3 == 1);
assert!(id(0) % 3 == 0);
assert!(id(-1) % 3 == -1);
assert!(id(-2) % 3 == -2);
assert!(id(-3) % 3 == 0);
assert!(id(-4) % 3 == -1);
assert!(id(-5) % 3 == -2);
prusti_assert!(id(3) % 3 == 0);
prusti_assert!(id(2) % 3 == 2);
prusti_assert!(id(1) % 3 == 1);
prusti_assert!(id(0) % 3 == 0);
prusti_assert!(id(-1) % 3 == -1);
prusti_assert!(id(-2) % 3 == -2);
prusti_assert!(id(-3) % 3 == 0);
prusti_assert!(id(-4) % 3 == -1);
prusti_assert!(id(-5) % 3 == -2);

assert!(id(-4) % 2 == 0);
prusti_assert!(id(-4) % 2 == 0);

// Smoke test
assert!(false); //~ ERROR the asserted expression might not hold
}

fn main(){}
9 changes: 8 additions & 1 deletion prusti-viper/src/encoder/mir_encoder/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -494,7 +494,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> MirEncoder<'p, 'v, 'tcx> {
vir::Expr::rem(left, right)
}
}
mir::BinOp::Div => vir::Expr::div(left, right),
mir::BinOp::Div => {
if matches!(ty.kind(), ty::TyKind::Int(_)) {
vir::Expr::div(left, right)
} else {
// floats, unsigned integers
vir::Expr::viper_div(left, right)
}
}
mir::BinOp::MulUnchecked | mir::BinOp::Mul => vir::Expr::mul(left, right),
mir::BinOp::BitAnd if is_bool => vir::Expr::and(left, right),
mir::BinOp::BitOr if is_bool => vir::Expr::or(left, right),
Expand Down
16 changes: 14 additions & 2 deletions vir/defs/polymorphic/ast/expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -151,7 +151,7 @@ __binary_op__! {
add Add,
sub Sub,
mul Mul,
div Div,
viper_div Div,
modulo Mod,
and And,
or Or,
Expand Down Expand Up @@ -316,7 +316,19 @@ impl Expr {
}

#[allow(clippy::should_implement_trait)]
/// Encode Rust reminder. This is *not* Viper modulo.
/// Encode Rust's division. This is *not* Viper's division.
pub fn div(left: Expr, right: Expr) -> Self {
Expr::ite(
Expr::ge_cmp(left.clone(), 0.into()),
// positive value or left % right == 0
Expr::viper_div(left.clone(), right.clone()),
// negative value
Expr::minus(Expr::viper_div(Expr::minus(left), right)),
)
}

#[allow(clippy::should_implement_trait)]
/// Encode Rust's signed reminder. This is *not* Viper's modulo.
pub fn rem(left: Expr, right: Expr) -> Self {
let abs_right = Expr::ite(
Expr::ge_cmp(right.clone(), 0.into()),
Expand Down
18 changes: 16 additions & 2 deletions vir/src/legacy/ast/expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -561,7 +561,8 @@ impl Expr {
}

#[allow(clippy::should_implement_trait)]
pub fn div(left: Expr, right: Expr) -> Self {
/// Encode Rust's unsigned division. This is the same as Viper's division.
pub fn viper_div(left: Expr, right: Expr) -> Self {
Expr::BinOp(
BinaryOpKind::Div,
Box::new(left),
Expand All @@ -570,6 +571,19 @@ impl Expr {
)
}

#[allow(clippy::should_implement_trait)]
/// Encode Rust's division. This is *not* Viper's division.
pub fn div(left: Expr, right: Expr) -> Self {
Expr::ite(
Expr::ge_cmp(left.clone(), 0.into()),
// positive value or left % right == 0
Expr::viper_div(left.clone(), right.clone()),
// negative value
Expr::minus(Expr::viper_div(Expr::minus(left), right)),
)
}

/// Encode Rust's unsigned reminder. This is the same as Viper's modulo.
pub fn modulo(left: Expr, right: Expr) -> Self {
Expr::BinOp(
BinaryOpKind::Mod,
Expand All @@ -580,7 +594,7 @@ impl Expr {
}

#[allow(clippy::should_implement_trait)]
/// Encode Rust reminder. This is *not* Viper modulo.
/// Encode Rust's signed reminder. This is *not* Viper's modulo.
pub fn rem(left: Expr, right: Expr) -> Self {
let abs_right = Expr::ite(
Expr::ge_cmp(right.clone(), 0.into()),
Expand Down

0 comments on commit 0d4a8d4

Please sign in to comment.