fix: Unsound interval rules for *, div, mod, / and **

Source/AbstractInterpretation/IntervalDomain.cs

@@ -1285,24 +1285,22 @@ public override Expr VisitNAryExpr(NAryExpr node)
               break;
             case BinaryOperator.Opcode.Mul:
               // this uses an incomplete approximation that could be tightened up
-              if (lo0 != null && lo1 != null)
+              // Nonnegative operands only. A negative operand needs all four corner products, so it
+              // needs an upper bound on both operands, and neither of those is always known.
+              if (lo0 != null && lo1 != null && 0 <= (BigInteger) lo0 && 0 <= (BigInteger) lo1)
               {
-                if (0 <= (BigInteger) lo0 && 0 <= (BigInteger) lo1)
-                {
-                  Lo = lo0 * lo1;
-                  Hi = hi0 == null || hi1 == null ? null : isReal ? hi0 * hi1 : (hi0 - 1) * (hi1 - 1) + 1;
-                }
-                else if ((BigInteger) lo0 < 0 && (BigInteger) lo1 < 0)
-                {
-                  Lo = null; // approximation
-                  Hi = isReal ? lo0 * lo1 : lo0 * lo1 + 1;
-                }
+                Lo = lo0 * lo1;
+                Hi = hi0 == null || hi1 == null ? null : isReal ? hi0 * hi1 : (hi0 - 1) * (hi1 - 1) + 1;
               }
 
               break;
             case BinaryOperator.Opcode.Div:
+            case BinaryOperator.Opcode.RealDiv:
               // this uses an incomplete approximation that could be tightened up
-              if (lo0 != null && lo1 != null && 0 <= (BigInteger) lo0 && 0 <= (BigInteger) lo1)
+              // Division by zero is underspecified, so the divisor must be known nonzero. An integer
+              // bound cannot say "positive but below one", so a real divisor in that range yields
+              // nothing rather than a bound the quotient can exceed.
+              if (lo0 != null && lo1 != null && 0 <= (BigInteger) lo0 && 1 <= (BigInteger) lo1)
               {
                 Lo = BigInteger.Zero;
                 Hi = hi0;
@@ -1311,7 +1309,8 @@ public override Expr VisitNAryExpr(NAryExpr node)
               break;
             case BinaryOperator.Opcode.Mod:
               // this uses an incomplete approximation that could be tightened up
-              if (lo0 != null && lo1 != null && 0 <= (BigInteger) lo0 && 0 <= (BigInteger) lo1)
+              // As for Div, the divisor must be known nonzero.
+              if (lo0 != null && lo1 != null && 0 <= (BigInteger) lo0 && 1 <= (BigInteger) lo1)
               {
                 Lo = BigInteger.Zero;
                 Hi = hi1;
@@ -1322,24 +1321,6 @@ public override Expr VisitNAryExpr(NAryExpr node)
                 }
               }
 
-              break;
-            case BinaryOperator.Opcode.RealDiv:
-              // this uses an incomplete approximation that could be tightened up
-              if (lo0 != null && lo1 != null && 0 <= (BigInteger) lo0 && 0 <= (BigInteger) lo1)
-              {
-                Lo = BigInteger.Zero;
-                Hi = 1 <= (BigInteger) lo1 ? hi0 : null;
-              }
-
-              break;
-            case BinaryOperator.Opcode.Pow:
-              // this uses an incomplete approximation that could be tightened up
-              if (lo0 != null && lo1 != null && 0 <= (BigInteger) lo0 && 0 <= (BigInteger) lo1)
-              {
-                Lo = 1 <= (BigInteger) lo1 ? BigInteger.One : BigInteger.Zero;
-                Hi = hi1;
-              }
-
               break;
             default:
               break;

Test/aitest0/DivisionByZeroBounds.bpl

@@ -0,0 +1,44 @@
+// RUN: %parallel-boogie -infer:j "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Div, Mod and RealDiv bounded their result whenever both operands had a lower bound of at least zero,
+// which admits a zero divisor. Division and mod by zero are underspecified in SMT-LIB, so the result is
+// an arbitrary value and no bound holds of it. Each rule now requires a divisor of at least one.
+//
+// Each quotient is computed in a loop because an inferred fact reaches the prover at a loop head.
+
+procedure IntDiv(a: int)
+  requires 0 <= a;
+{
+  var q: int;
+  var i: int;
+
+  q := a div 0;
+  i := 0;
+  while (i < 3) { q := a div 0; i := i + 1; }
+  assert 0 <= q;
+}
+
+procedure IntMod(a: int)
+  requires 0 <= a;
+{
+  var m: int;
+  var i: int;
+
+  m := a mod 0;
+  i := 0;
+  while (i < 3) { m := a mod 0; i := i + 1; }
+  assert m == 0;
+}
+
+procedure RealDiv(r: real)
+  requires 0e0 <= r;
+{
+  var d: real;
+  var i: int;
+
+  d := r / 0e0;
+  i := 0;
+  while (i < 3) { d := r / 0e0; i := i + 1; }
+  assert 0e0 <= d;
+}

Test/aitest0/DivisionByZeroBounds.bpl.expect

@@ -0,0 +1,17 @@
+DivisionByZeroBounds.bpl(19,3): Error: this assertion could not be proved
+Execution trace:
+    DivisionByZeroBounds.bpl(16,5): anon0
+    DivisionByZeroBounds.bpl(18,3): anon3_LoopHead
+    DivisionByZeroBounds.bpl(18,3): anon3_LoopDone
+DivisionByZeroBounds.bpl(31,3): Error: this assertion could not be proved
+Execution trace:
+    DivisionByZeroBounds.bpl(28,5): anon0
+    DivisionByZeroBounds.bpl(30,3): anon3_LoopHead
+    DivisionByZeroBounds.bpl(30,3): anon3_LoopDone
+DivisionByZeroBounds.bpl(43,3): Error: this assertion could not be proved
+Execution trace:
+    DivisionByZeroBounds.bpl(40,5): anon0
+    DivisionByZeroBounds.bpl(42,3): anon3_LoopHead
+    DivisionByZeroBounds.bpl(42,3): anon3_LoopDone
+
+Boogie program verifier finished with 0 verified, 3 errors

Test/aitest0/MulNegativeBounds.bpl

@@ -0,0 +1,35 @@
+// RUN: %parallel-boogie -infer:j "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Mul had a branch for two negative lower bounds that claimed Hi = lo0 * lo1, deriving an upper bound
+// from two lower bounds. It holds only if both operands are also bounded above by zero, which nothing
+// established. The real form is reachable from Dafny, which emits `*` on reals natively and enables this
+// analysis unconditionally, and there it proves `false`.
+//
+// Each product is computed in a loop because an inferred fact reaches the prover at a loop head.
+
+procedure MulInt(x: int, y: int)
+  requires -3 <= x;
+  requires -3 <= y;
+{
+  var z: int;
+  var i: int;
+
+  z := x * y;
+  i := 0;
+  while (i < 3) { z := x * y; i := i + 1; }
+  assert z < 10;   // x == y == 1000 gives 1000000
+}
+
+procedure MulReal(r: real, s: real)
+  requires -3e0 <= r;
+  requires -3e0 <= s;
+{
+  var d: real;
+  var i: int;
+
+  d := r * s;
+  i := 0;
+  while (i < 3) { d := r * s; i := i + 1; }
+  assert d <= 9e0;  // r == s == 1000.0 gives 1000000.0
+}

Test/aitest0/MulNegativeBounds.bpl.expect

@@ -0,0 +1,12 @@
+MulNegativeBounds.bpl(21,3): Error: this assertion could not be proved
+Execution trace:
+    MulNegativeBounds.bpl(18,5): anon0
+    MulNegativeBounds.bpl(20,3): anon3_LoopHead
+    MulNegativeBounds.bpl(20,3): anon3_LoopDone
+MulNegativeBounds.bpl(34,3): Error: this assertion could not be proved
+Execution trace:
+    MulNegativeBounds.bpl(31,5): anon0
+    MulNegativeBounds.bpl(33,3): anon3_LoopHead
+    MulNegativeBounds.bpl(33,3): anon3_LoopDone
+
+Boogie program verifier finished with 0 verified, 2 errors

Test/aitest0/PowerBounds.bpl

@@ -0,0 +1,22 @@
+// RUN: %parallel-boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %OutputCheck "--file-to-check=%t" "%s"
+// CHECK-NOT-L: <= p
+
+// Pow bounded the power by the bounds of its *exponent*: Lo was one for a nonzero exponent and Hi was the
+// exponent's own upper bound. Neither follows -- 3.0 ** 2.0 is 9.0, above the exponent's bound of 2.0 --
+// so the rule is gone and no bound on the power is inferred.
+//
+// Unlike the other rules this one cannot be caught by a false assertion: "**" is emitted as real_pow,
+// which no prover declares, so any program whose verification condition mentions it dies in the solver.
+// The inferred invariant is therefore checked directly, with -noVerify.
+
+procedure PowBounds(x: real, y: real) returns (p: real)
+{
+  var i: int;
+
+  assume 0e0 <= x;
+  assume 1e0 <= y && y <= 2e0;
+  p := x ** y;
+  i := 0;
+  while (i < 3) { i := i + 1; }
+}

Test/aitest1/Linear5.bpl.expect

@@ -30,11 +30,11 @@ implementation p()
   C:
     assume {:inferred} -1 <= x && 0 <= y;
     x := x * x;
-    assume {:inferred} x < 2 && 0 <= y;
+    assume {:inferred} 0 <= y;
     goto D, E;
 
   D:
-    assume {:inferred} x < 2 && 0 <= y;
+    assume {:inferred} 0 <= y;
     x := y;
     assume {:inferred} 0 <= x && 0 <= y;
     return;