From 0d4a8d497ac1e540d48ef50a031d53b4e3ae36e2 Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Tue, 26 Mar 2024 14:08:03 +0100 Subject: [PATCH] Fix issue #1505 (#1511) * Add regression test for issue #1505 * Fix encoding of signed integer divisions --- .../verify_overflow/fail/issues/issue-1505.rs | 57 +++++++++++++++++++ prusti-viper/src/encoder/mir_encoder/mod.rs | 9 ++- vir/defs/polymorphic/ast/expr.rs | 16 +++++- vir/src/legacy/ast/expr.rs | 18 +++++- 4 files changed, 95 insertions(+), 5 deletions(-) create mode 100644 prusti-tests/tests/verify_overflow/fail/issues/issue-1505.rs diff --git a/prusti-tests/tests/verify_overflow/fail/issues/issue-1505.rs b/prusti-tests/tests/verify_overflow/fail/issues/issue-1505.rs new file mode 100644 index 00000000000..84b62b55b79 --- /dev/null +++ b/prusti-tests/tests/verify_overflow/fail/issues/issue-1505.rs @@ -0,0 +1,57 @@ +use prusti_contracts::*; + +// To inhibit constant-propagation optimizations: +#[pure] +fn id(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(){} diff --git a/prusti-viper/src/encoder/mir_encoder/mod.rs b/prusti-viper/src/encoder/mir_encoder/mod.rs index 700807d8833..16fd39310c6 100644 --- a/prusti-viper/src/encoder/mir_encoder/mod.rs +++ b/prusti-viper/src/encoder/mir_encoder/mod.rs @@ -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), diff --git a/vir/defs/polymorphic/ast/expr.rs b/vir/defs/polymorphic/ast/expr.rs index e85ee38e739..7d36499160f 100644 --- a/vir/defs/polymorphic/ast/expr.rs +++ b/vir/defs/polymorphic/ast/expr.rs @@ -151,7 +151,7 @@ __binary_op__! { add Add, sub Sub, mul Mul, - div Div, + viper_div Div, modulo Mod, and And, or Or, @@ -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()), diff --git a/vir/src/legacy/ast/expr.rs b/vir/src/legacy/ast/expr.rs index 14876f6a800..ae1b19ae5a0 100644 --- a/vir/src/legacy/ast/expr.rs +++ b/vir/src/legacy/ast/expr.rs @@ -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), @@ -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, @@ -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()),