Merge pull request #794 from viperproject/meilers_fix_782

Only simplify div and mod for positive arguments (like Carbon does)

Author: marcoeilers

src/main/scala/viper/silver/ast/utility/Simplifier.scala

@@ -116,10 +116,15 @@ object Simplifier {
         IntLit(left - right)(root.pos, root.info)
       case root @ Mul(IntLit(left), IntLit(right)) =>
         IntLit(left * right)(root.pos, root.info)
-      case root @ Div(IntLit(left), IntLit(right)) if right != bigIntZero =>
+      /* In the general case, Viper uses the SMT division and modulo. Scala's division is not in-sync with SMT division.
+         For nonnegative dividends and divisors, all used division and modulo definitions coincide. So, in order to not
+         not make any assumptions on the SMT division, division and modulo are simplified only if the dividend and divisor
+         are nonnegative. Also see Carbon PR #448.
+       */
+      case root @ Div(IntLit(left), IntLit(right)) if left >= bigIntZero && right > bigIntZero =>
         IntLit(left / right)(root.pos, root.info)
-      case root @ Mod(IntLit(left), IntLit(right)) if right != bigIntZero =>
-        IntLit((right.abs + (left % right)) % right.abs)(root.pos, root.info)
+      case root @ Mod(IntLit(left), IntLit(right)) if left >= bigIntZero && right > bigIntZero =>
+        IntLit(left % right)(root.pos, root.info)
 
       // statement simplifications
       case Seqn(EmptyStmt, _) => EmptyStmt // remove empty Seqn (including unnecessary scopedDecls)

src/test/scala/SimplifierTests.scala

@@ -36,18 +36,21 @@ class SimplifierTests extends AnyFunSuite with Matchers {
   test("div") {
     simplify(Div(0, 0)()) should be(Div(0, 0)())
     simplify(Div(8, 2)()) should be(4: IntLit)
+    simplify(Div(-3, 2)()) should be(Div(-3, 2)())
+    simplify(Div(3, 2)()) should be(1: IntLit)
+    simplify(Div(3, -2)()) should be(Div(3, -2)())
   }
 
   test("mod") {
     simplify(Mod(0, 0)()) should be (Mod(0, 0)())
     simplify(Mod(8, 3)()) should be (2: IntLit)
     simplify(Mod(3, 8)()) should be (3: IntLit)
-    simplify(Mod(8, -3)()) should be (2: IntLit)
-    simplify(Mod(3, -8)()) should be (3: IntLit)
-    simplify(Mod(-8, 3)()) should be (1: IntLit)
-    simplify(Mod(-3, 8)()) should be (5: IntLit)
-    simplify(Mod(-8, -3)()) should be (1: IntLit)
-    simplify(Mod(-3, -8)()) should be (5: IntLit)
+    simplify(Mod(8, -3)()) should be (Mod(8, -3)())
+    simplify(Mod(3, -8)()) should be (Mod(3, -8)())
+    simplify(Mod(-8, 3)()) should be (Mod(-8, 3)())
+    simplify(Mod(-3, 8)()) should be (Mod(-3, 8)())
+    simplify(Mod(-8, -3)()) should be (Mod(-8, -3)())
+    simplify(Mod(-3, -8)()) should be (Mod(-3, -8)())
   }
 
   test("equality") {