Fix encoding of signed integer divisions

viperproject · Mar 25, 2024 · 6cc13ec · 6cc13ec
1 parent 2c82f4d
commit 6cc13ec
Show file tree

Hide file tree

Showing 6 changed files with 170 additions and 7 deletions.
diff --git a/prusti-tests/tests/verify_overflow/fail/issues/issue-1505.rs 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<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(){}
diff --git a/prusti-tests/tests/verify_safe_clients/fail/dev_tests/signed_ops.rs b/prusti-tests/tests/verify_safe_clients/fail/dev_tests/signed_ops.rs
@@ -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);
+
+    assert!(false); // Smoke check
+    //~^ 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);
+
+    assert!(false); // Smoke check
+    //~^ ERROR the asserted expression might not hold
+}
+
+fn main(){}
diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs
@@ -81,7 +81,7 @@ lazy_static::lazy_static! {
         settings.set_default("check_panics", true).unwrap();
         settings.set_default("encode_unsigned_num_constraint", false).unwrap();
         settings.set_default("encode_bitvectors", false).unwrap();
-        settings.set_default("simplify_encoding", true).unwrap();
+        settings.set_default("simplify_encoding", false).unwrap();
         settings.set_default("log", "").unwrap();
         settings.set_default("log_style", "auto").unwrap();
         settings.set_default("log_dir", "log").unwrap();

diff --git a/prusti-viper/src/encoder/mir_encoder/operations.rs b/prusti-viper/src/encoder/mir_encoder/operations.rs
@@ -40,8 +40,20 @@ pub fn encode_bin_op_expr(
         mir::BinOp::Le => vir::Expr::le_cmp(left, right),
         mir::BinOp::Add => vir::Expr::add(left, right),
         mir::BinOp::Sub => vir::Expr::sub(left, right),
-        mir::BinOp::Rem => vir::Expr::rem(left, right),
-        mir::BinOp::Div => vir::Expr::div(left, right),
+        mir::BinOp::Rem => {
+            if matches!(ty.kind(), ty::TyKind::Uint(_)) {
+                vir::Expr::modulo(left, right)
+            } else {
+                vir::Expr::rem(left, right)
+            }
+        }
+        mir::BinOp::Div => {
+            if matches!(ty.kind(), ty::TyKind::Uint(_)) {
+                vir::Expr::unsigned_div(left, right)
+            } else {
+                vir::Expr::div(left, right)
+            }
+        }
         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
@@ -151,7 +151,7 @@ __binary_op__! {
     add Add,
     sub Sub,
     mul Mul,
-    div Div,
+    unsigned_div Div,
     modulo Mod,
     and And,
     or Or,
@@ -316,7 +316,22 @@ 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::or(
+                Expr::ge_cmp(left.clone(), 0.into()),
+                Expr::eq_cmp(Expr::modulo(left.clone(), right.clone()), 0.into()),
+            ),
+            // positive value or left % right == 0
+            Expr::unsigned_div(left.clone(), right.clone()),
+            // negative value
+            Expr::minus(Expr::unsigned_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
@@ -546,16 +546,38 @@ impl Expr {
     }
 
     #[allow(clippy::should_implement_trait)]
+    /// Encode Rust's unsigned division. This is the same as Viper's division.
+    pub fn unsigned_div(left: Expr, right: Expr) -> Self {
+        Expr::BinOp(
+            BinaryOpKind::Div,
+            Box::new(left),
+            Box::new(right),
+            Position::default(),
+        )
+    }
+
+    #[allow(clippy::should_implement_trait)]
+    /// Encode Rust's division. This is *not* Viper's division.
     pub fn div(left: Expr, right: Expr) -> Self {
-        Expr::BinOp(BinaryOpKind::Div, box left, box right, Position::default())
+        Expr::ite(
+            Expr::or(
+                Expr::ge_cmp(left.clone(), 0.into()),
+                Expr::eq_cmp(Expr::modulo(left.clone(), right.clone()), 0.into()),
+            ),
+            // positive value or left % right == 0
+            Expr::unsigned_div(left.clone(), right.clone()),
+            // negative value
+            Expr::minus(Expr::unsigned_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, box left, box right, Position::default())
     }
 
     #[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()),