From e292fc2496bd6500e724c94c85540d1e37d405f6 Mon Sep 17 00:00:00 2001
From: Federico Poli <federpoli@gmail.com>
Date: Mon, 25 Mar 2024 15:12:01 +0100
Subject: [PATCH] Fix encoding of signed integer divisions

---
 .../verify_overflow/fail/issues/issue-1505.rs  | 16 +++++++++++++++-
 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, 53 insertions(+), 6 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
index 4a42eda82a1..84b62b55b79 100644
--- a/prusti-tests/tests/verify_overflow/fail/issues/issue-1505.rs
+++ b/prusti-tests/tests/verify_overflow/fail/issues/issue-1505.rs
@@ -2,7 +2,7 @@ use prusti_contracts::*;
 
 // To inhibit constant-propagation optimizations:
 #[pure]
-fn id<T>(x: T) -> T { x}
+fn id<T: Copy>(x: T) -> T { x }
 
 fn check_division(){
     assert!(id(3i32) / 2 == 1);
@@ -23,6 +23,10 @@ fn check_modulo() {
     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);
@@ -33,8 +37,18 @@ fn check_modulo() {
     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
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()),