fix: !(x < y) is rewritten to y <= x even for floats

Source/AbstractInterpretation/IntervalDomain.cs

@@ -724,6 +724,16 @@ E_Common Constraint(Expr expr, Node state)
               var n = new Node(v, null, BigInteger.One);
               return new E(n);
             }
+            else
+            {
+              // A negation written with "!" never went through Expr.Not, so push it inwards now, with the
+              // types it needs in place. This fails on a float's order relation, which cannot be
+              // reversed, and there is nothing to learn from the negation itself.
+              if (Expr.TryPushNegation(e, out var pushed))
+              {
+                return Constraint(pushed, state);
+              }
+            }
           }
         }
         else if (e.Fun is BinaryOperator)

Source/Core/AST/Expression/AbsyExpr.cs

@@ -301,6 +301,17 @@ public static Expr Not(Expr e1)
           BinaryOperator op = (BinaryOperator) nary.Fun;
           Expr arg0 = Cce.NonNull(nary.Args[0]);
           Expr arg1 = Cce.NonNull(nary.Args[1]);
+          // A negated order relation is the reverse relation only where the order is total. On floats it
+          // is not: every IEEE comparison is false when an operand is NaN, so "!(a < b)" holds of a NaN
+          // while "b <= a" does not. Equality is different -- Boogie's == on floats is bit identity,
+          // which is total -- so complementing Eq and Neq stays correct.
+          //
+          // The type is not always known here, and cannot be made so: an "if" or "while" guard is negated
+          // from the Implementation constructor, which flattens the structured statements into blocks
+          // (BigBlocksResolutionContext) while parsing -- before any identifier has been resolved, let
+          // alone typechecked. An unknown type is therefore treated as possibly float, and
+          // Program.ReverseGuardNegations asks again once types exist.
+          var knownTotalOrder = arg0.Type != null && !arg0.Type.IsFloat;
           if (op.Op == BinaryOperator.Opcode.Eq)
           {
             return Neq(arg0, arg1);
@@ -309,19 +320,19 @@ public static Expr Not(Expr e1)
           {
             return Eq(arg0, arg1);
           }
-          else if (op.Op == BinaryOperator.Opcode.Lt)
+          else if (knownTotalOrder && op.Op == BinaryOperator.Opcode.Lt)
           {
             return Le(arg1, arg0);
           }
-          else if (op.Op == BinaryOperator.Opcode.Le)
+          else if (knownTotalOrder && op.Op == BinaryOperator.Opcode.Le)
           {
             return Lt(arg1, arg0);
           }
-          else if (op.Op == BinaryOperator.Opcode.Ge)
+          else if (knownTotalOrder && op.Op == BinaryOperator.Opcode.Ge)
           {
             return Gt(arg1, arg0);
           }
-          else if (op.Op == BinaryOperator.Opcode.Gt)
+          else if (knownTotalOrder && op.Op == BinaryOperator.Opcode.Gt)
           {
             return Ge(arg1, arg0);
           }
@@ -331,6 +342,35 @@ public static Expr Not(Expr e1)
       return Unary(Token.NoToken, UnaryOperator.Opcode.Not, e1);
     }
 
+    /// <summary>
+    /// Negates what "negation" negates, for a negation that Not was not able to push inwards when it was
+    /// built -- either because the operand had no type yet or because it never went through Not at all.
+    /// Fails when there is still nothing to be had, which is when the result is a negation again.
+    /// </summary>
+    public static bool TryPushNegation(NAryExpr negation, out Expr pushed)
+    {
+      Contract.Requires(negation.Fun is UnaryOperator { Op: UnaryOperator.Opcode.Not });
+      pushed = Not(negation.Args[0]);
+      if (pushed is NAryExpr { Fun: UnaryOperator { Op: UnaryOperator.Opcode.Not } })
+      {
+        return false;
+      }
+
+      // Not is normally called before typechecking, so what it builds carries no type. Compare
+      // BinaryOperator.ResolveOverloading, which types a node it builds in the same two steps. This is
+      // also why callers must be past typechecking: setting TypeParameters is what tells
+      // NAryExpr.Typecheck a node has been checked already, so doing it earlier would skip the check.
+      if (pushed is NAryExpr nary)
+      {
+        // Set independently: whoever built the node may have given it a type without marking it checked,
+        // and MonomorphizationDuplicator reads TypeParameters of every NAryExpr it visits.
+        nary.Type ??= Type.Bool;
+        nary.TypeParameters ??= SimpleTypeParamInstantiation.EMPTY;
+      }
+
+      return true;
+    }
+
     public static Expr Neg(Expr e1)
     {
       Contract.Requires(e1 != null);

Source/Core/AST/Program.cs

@@ -207,6 +207,34 @@ public override void Typecheck(TypecheckingContext tc)
       {
         seeker.Visit(d);
       }
+
+      ReverseGuardNegations();
+    }
+  }
+
+  /// <summary>
+  /// Finishes negating the guards of "if" and "while". They are negated from the Implementation
+  /// constructor, while parsing, so nothing has a type yet and Expr.Not leaves an order relation alone --
+  /// see there. Asking it again here reverses the ones it can, and still leaves a float's alone.
+  ///
+  /// This reaches the blocks, which is what gets verified. It cannot reach a -print taken of the program
+  /// as parsed: that happens before resolution (ExecutionEngine.ProcessProgram), while the blocks already
+  /// exist, because the Implementation constructor built them. So such a print shows the unreversed
+  /// guard, which is why Test/inline/test4.bpl expects one.
+  /// </summary>
+  private void ReverseGuardNegations()
+  {
+    foreach (var cmd in Implementations
+               .SelectMany(impl => impl.Blocks)
+               .SelectMany(block => block.Cmds)
+               .OfType<AssumeCmd>()
+               .Where(cmd => cmd.Attributes.FindBoolAttribute("partition")))
+    {
+      if (cmd.Expr is NAryExpr { Fun: UnaryOperator { Op: UnaryOperator.Opcode.Not } } negation &&
+          Expr.TryPushNegation(negation, out var reversed))
+      {
+        cmd.Expr = reversed;
+      }
     }
   }
 

Test/aitest0/GuardNegation.bpl

@@ -0,0 +1,54 @@
+// RUN: %parallel-boogie -infer:t -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// The desugaring of "if" and "while" negates the guard while the parser is still building blocks, before
+// anything has a type, and Expr.Not will not reverse an order relation without knowing whether the type
+// orders totally. Program.Typecheck asks it again afterwards, so the printed blocks below show an integer
+// guard reversed and a float's left as a negation.
+//
+// The trivial domain is enough to get the blocks printed, and keeps whatever another domain would infer
+// out of the expectation.
+
+procedure IntGuard() returns (r: int)
+{
+  var i: int;
+  i := 0;
+  while (i < 3)
+  {
+    i := i + 1;
+  }
+
+  if (7 <= i)
+  {
+    r := 1;
+  }
+  else
+  {
+    r := 0;
+  }
+}
+
+procedure FloatGuard(f: float24e8) returns (r: int)
+{
+  if (f < 0x1.0e0f24e8)
+  {
+    r := 1;
+  }
+  else
+  {
+    r := 0;
+  }
+}
+
+// A bool guard has no relation to reverse either way.
+procedure BoolGuard(b: bool) returns (r: int)
+{
+  if (b)
+  {
+    r := 1;
+  }
+  else
+  {
+    r := 0;
+  }
+}

Test/aitest0/GuardNegation.bpl.expect

@@ -0,0 +1,108 @@
+procedure IntGuard() returns (r: int);
+
+
+
+implementation IntGuard() returns (r: int)
+{
+  var i: int;
+
+  anon0:
+    assume {:inferred} true;
+    i := 0;
+    assume {:inferred} true;
+    goto anon5_LoopHead;
+
+  anon5_LoopHead:  // cut point
+    assume {:inferred} true;
+    assume {:inferred} true;
+    goto anon5_LoopDone, anon5_LoopBody;
+
+  anon5_LoopBody:
+    assume {:inferred} true;
+    assume {:partition} i < 3;
+    i := i + 1;
+    assume {:inferred} true;
+    goto anon5_LoopHead;
+
+  anon5_LoopDone:
+    assume {:inferred} true;
+    assume {:partition} 3 <= i;
+    assume {:inferred} true;
+    goto anon6_Then, anon6_Else;
+
+  anon6_Else:
+    assume {:inferred} true;
+    assume {:partition} i < 7;
+    r := 0;
+    assume {:inferred} true;
+    return;
+
+  anon6_Then:
+    assume {:inferred} true;
+    assume {:partition} 7 <= i;
+    r := 1;
+    assume {:inferred} true;
+    return;
+}
+
+
+
+procedure FloatGuard(f: float24e8) returns (r: int);
+
+
+
+implementation FloatGuard(f: float24e8) returns (r: int)
+{
+
+  anon0:
+    assume {:inferred} true;
+    assume {:inferred} true;
+    goto anon3_Then, anon3_Else;
+
+  anon3_Else:
+    assume {:inferred} true;
+    assume {:partition} !(f < 0x1.0e0f24e8);
+    r := 0;
+    assume {:inferred} true;
+    return;
+
+  anon3_Then:
+    assume {:inferred} true;
+    assume {:partition} f < 0x1.0e0f24e8;
+    r := 1;
+    assume {:inferred} true;
+    return;
+}
+
+
+
+procedure BoolGuard(b: bool) returns (r: int);
+
+
+
+implementation BoolGuard(b: bool) returns (r: int)
+{
+
+  anon0:
+    assume {:inferred} true;
+    assume {:inferred} true;
+    goto anon3_Then, anon3_Else;
+
+  anon3_Else:
+    assume {:inferred} true;
+    assume {:partition} !b;
+    r := 0;
+    assume {:inferred} true;
+    return;
+
+  anon3_Then:
+    assume {:inferred} true;
+    assume {:partition} b;
+    r := 1;
+    assume {:inferred} true;
+    return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors

Test/aitest0/NegatedConstraint.bpl

@@ -0,0 +1,44 @@
+// RUN: %parallel-boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// A negation written by hand never went through Expr.Not, so the domain ignored it. It now pushes the
+// negation inwards with the same rewriting Expr.Not applies elsewhere, which by then has the types it
+// needs. Three shapes it did not read before, and one it must still refuse.
+
+procedure NegatedComparisons()
+{
+  var i: int;
+  var j: int;
+
+  havoc i, j;
+  assume !(i < 3);         // i >= 3
+  assume !(7 <= j);        // j < 7
+}
+
+procedure NegatedEquality()
+{
+  var x: int;
+
+  havoc x;
+  assume 5 <= x;
+  assume !(x == 5);        // with the bound above, x >= 6
+}
+
+procedure DoubleNegation()
+{
+  var y: int;
+
+  havoc y;
+  assume !!(3 <= y);       // y >= 3
+}
+
+// A float's order is partial, so a negated float comparison holds of a NaN and the reverse relation does
+// not. Expr.Not declines to reverse it and hands the negation back unchanged, which is how the domain
+// recognises there is nothing to learn: no element below mentions f.
+procedure FloatRefused(f: float24e8)
+{
+  var k: int;
+
+  k := 0;
+  assume !(f < 0x1.0e0f24e8);
+}