ConstraintAnalysis: Fix missing overflow checks in x++

src/ir/constraint.cpp

@@ -808,11 +808,19 @@ void BasicBlockConstraintMap::set(Index index, Expression* value) {
         case Eq:
           *N = N->add(Literal::makeFromInt32(1, N->type));
           break;
-        // x >= N, x++  =>  x > N
+        // x >= N, x++  =>  x > N if no overflow
         case GeS:
+          if (old.proves({LtS, Literal::makeSignedMax(N->type)}) != True) {
+            iter = new_.erase(iter);
+            continue;
+          }
           c.op = GtS;
           break;
         case GeU:
+          if (old.proves({LtU, Literal::makeUnsignedMax(N->type)}) != True) {
+            iter = new_.erase(iter);
+            continue;
+          }
           c.op = GtU;
           break;
         // x < N, x++  =>  x <= N
@@ -1022,7 +1030,7 @@ std::ostream& operator<<(std::ostream& o, const Constraint& c) {
   if (auto* cc = std::get_if<Literal>(&c.term)) {
     o << *cc;
   } else if (auto* i = std::get_if<Index>(&c.term)) {
-    o << "Index(" << *i << ')';
+    o << "$" << *i;
   }
   o << '}';
   return o;

test/gtest/constraint.cpp

@@ -595,15 +595,31 @@ TEST(ConstraintTest, TestIncrement) {
   map.set(0, &add);
   check(map.get(0), {Eq, {Literal(int32_t(1))}});
 
-  // $0 >= 5, $0++  =>  $0 > 5 (signed)
+  // $0 >= 5, $0++  =>  nothing, since the ++ might overflow into negative
   map.set(0, {GeS, {Literal(int32_t(5))}});
   map.set(0, &add);
-  check(map.get(0), {GtS, {Literal(int32_t(5))}});
+  EXPECT_TRUE(map.get(0).empty());
 
-  // Ditto, unsigned
+  // $0 >= 5, $0 < 100, $0++  =>  $0 > 5, $0 <= 100 (signed)
+  Constraint lts100{LtS, {Literal(int32_t(100))}};
+  Constraint les100{LeS, {Literal(int32_t(100))}};
+  map.set(0, {{GeS, {Literal(int32_t(5))}}, lts100});
+  map.set(0, &add);
+  EXPECT_EQ(map.get(0),
+            (AndedConstraintSet{{GtS, {Literal(int32_t(5))}}, les100}));
+
+  // Ditto, unsigned: without an upper bound we can overflow.
   map.set(0, {GeU, {Literal(int32_t(5))}});
   map.set(0, &add);
-  check(map.get(0), {GtU, {Literal(int32_t(5))}});
+  EXPECT_TRUE(map.get(0).empty());
+
+  // With an upper bound, we can optimize like before.
+  Constraint ltu100{LtU, {Literal(int32_t(100))}};
+  Constraint leu100{LeU, {Literal(int32_t(100))}};
+  map.set(0, {{GeU, {Literal(int32_t(5))}}, ltu100});
+  map.set(0, &add);
+  EXPECT_EQ(map.get(0),
+            (AndedConstraintSet{{GtU, {Literal(int32_t(5))}}, leu100}));
 
   // $0 < 5, $0++  =>  $0 <= 5 (signed)
   map.set(0, {LtS, {Literal(int32_t(5))}});
@@ -656,18 +672,37 @@ TEST(ConstraintTest, TestIncrement) {
             (AndedConstraintSet{{GtS, {Literal(int32_t(10))}},
                                 {LeS, {Literal(int32_t(20))}}}));
 
-  // $0 >= 10 && $0 <= max_signed, $0++  =>  $0 > 10 (overflowing constraint
-  // removed)
+  // $0 >= 10 && $0 <= max_signed, $0++  =>  nothing, as we may overflow.
   map.set(0, {GeS, {Literal(int32_t(10))}});
   map.approximateAnd(0, {LeS, {Literal::makeSignedMax(Type::i32)}});
   map.set(0, &add);
-  EXPECT_EQ(map.get(0), (AndedConstraintSet{{GtS, {Literal(int32_t(10))}}}));
+  EXPECT_EQ(map.get(0).size(), 0);
 
-  // $0 >= 10 && $0 == $2, $0++  =>  $0 > 10 (non-constant term removed)
-  map.set(0, {GeS, {Literal(int32_t(10))}});
+  // Ditto, unsigned.
+  map.set(0, {GeU, {Literal(int32_t(10))}});
+  map.approximateAnd(0, {LeU, {Literal::makeUnsignedMax(Type::i32)}});
+  map.set(0, &add);
+  EXPECT_EQ(map.get(0).size(), 0);
+
+  // Ditto, 64-bit signed.
+  map.set(0, {GeS, {Literal(int64_t(10))}});
+  map.approximateAnd(0, {LeS, {Literal::makeSignedMax(Type::i64)}});
+  map.set(0, &add);
+  EXPECT_EQ(map.get(0).size(), 0);
+
+  // Ditto, 64-bit unsigned.
+  map.set(0, {GeU, {Literal(int64_t(10))}});
+  map.approximateAnd(0, {LeU, {Literal::makeUnsignedMax(Type::i64)}});
+  map.set(0, &add);
+  EXPECT_EQ(map.get(0).size(), 0);
+
+  // $0 >= 5 && $0 < 100 && $0 == $2, $0++  =>  we increment and remove the non-
+  // constant term, leaving $0 > 5 && $0 <= 100.
+  map.set(0, {{GeS, {Literal(int32_t(5))}}, lts100});
   map.approximateAnd(0, {Eq, {Index(2)}});
   map.set(0, &add);
-  EXPECT_EQ(map.get(0), (AndedConstraintSet{{GtS, {Literal(int32_t(10))}}}));
+  EXPECT_EQ(map.get(0),
+            (AndedConstraintSet{{GtS, {Literal(int32_t(5))}}, les100}));
 }
 
 TEST(ConstraintTest, TestEqConstraints) {

test/lit/passes/constraint-analysis-loops.wast

@@ -1573,4 +1573,219 @@
       )
     )
   )
+
+  ;; CHECK:      (func $add-overflow (type $1) (param $x i32)
+  ;; CHECK-NEXT:  (if
+  ;; CHECK-NEXT:   (i32.ge_s
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (i32.const 0)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (then
+  ;; CHECK-NEXT:    (local.set $x
+  ;; CHECK-NEXT:     (i32.add
+  ;; CHECK-NEXT:      (local.get $x)
+  ;; CHECK-NEXT:      (i32.const 1)
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.gt_s
+  ;; CHECK-NEXT:      (local.get $x)
+  ;; CHECK-NEXT:      (i32.const 0)
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  (func $add-overflow (param $x i32)
+    (if
+      (i32.ge_s
+        (local.get $x)
+        (i32.const 0)
+      )
+      (then
+        ;; Normally, x >= 0 and x++ lead to x > 0. However, we overflow if
+        ;; x == MAX_INT, so we cannot optimize the dropped value below us.
+        (local.set $x
+          (i32.add
+            (local.get $x)
+            (i32.const 1)
+          )
+        )
+        (drop
+          (i32.gt_s
+            (local.get $x)
+            (i32.const 0)
+          )
+        )
+      )
+    )
+  )
+
+  ;; CHECK:      (func $add-overflow-yes (type $1) (param $x i32)
+  ;; CHECK-NEXT:  (if
+  ;; CHECK-NEXT:   (i32.ge_s
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (i32.const 0)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (then
+  ;; CHECK-NEXT:    (if
+  ;; CHECK-NEXT:     (i32.le_s
+  ;; CHECK-NEXT:      (local.get $x)
+  ;; CHECK-NEXT:      (i32.const 1000)
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:     (then
+  ;; CHECK-NEXT:      (local.set $x
+  ;; CHECK-NEXT:       (i32.add
+  ;; CHECK-NEXT:        (local.get $x)
+  ;; CHECK-NEXT:        (i32.const 1)
+  ;; CHECK-NEXT:       )
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:      (drop
+  ;; CHECK-NEXT:       (i32.const 1)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  (func $add-overflow-yes (param $x i32)
+    ;; As above, but we add an inner if that does x < 1000. Now x cannot be
+    ;; MAX_INT, so we do optimize to 1.
+    (if
+      (i32.ge_s
+        (local.get $x)
+        (i32.const 0)
+      )
+      (then
+        (if
+          (i32.le_s
+            (local.get $x)
+            (i32.const 1000)
+          )
+          (then
+            (local.set $x
+              (i32.add
+                (local.get $x)
+                (i32.const 1)
+              )
+            )
+            (drop
+              (i32.gt_s
+                (local.get $x)
+                (i32.const 0)
+              )
+            )
+          )
+        )
+      )
+    )
+  )
+
+  ;; CHECK:      (func $add-overflow-unsigned (type $1) (param $x i32)
+  ;; CHECK-NEXT:  (if
+  ;; CHECK-NEXT:   (i32.ge_u
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (i32.const 1)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (then
+  ;; CHECK-NEXT:    (local.set $x
+  ;; CHECK-NEXT:     (i32.add
+  ;; CHECK-NEXT:      (local.get $x)
+  ;; CHECK-NEXT:      (i32.const 1)
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (drop
+  ;; CHECK-NEXT:     (i32.gt_u
+  ;; CHECK-NEXT:      (local.get $x)
+  ;; CHECK-NEXT:      (i32.const 1)
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  (func $add-overflow-unsigned (param $x i32)
+    ;; As above, but unsigned. We change the 0 to 1, as x >= 0 is always true
+    ;; for unsigned anyhow.
+    (if
+      (i32.ge_u
+        (local.get $x)
+        (i32.const 1)
+      )
+      (then
+        (local.set $x
+          (i32.add
+            (local.get $x)
+            (i32.const 1)
+          )
+        )
+        ;; We do not optimize, due to the risk of overflow.
+        (drop
+          (i32.gt_u
+            (local.get $x)
+            (i32.const 1)
+          )
+        )
+      )
+    )
+  )
+
+  ;; CHECK:      (func $add-overflow-unsigned-yes (type $1) (param $x i32)
+  ;; CHECK-NEXT:  (if
+  ;; CHECK-NEXT:   (i32.ge_u
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:    (i32.const 1)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (then
+  ;; CHECK-NEXT:    (if
+  ;; CHECK-NEXT:     (i32.le_u
+  ;; CHECK-NEXT:      (local.get $x)
+  ;; CHECK-NEXT:      (i32.const 1000)
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:     (then
+  ;; CHECK-NEXT:      (local.set $x
+  ;; CHECK-NEXT:       (i32.add
+  ;; CHECK-NEXT:        (local.get $x)
+  ;; CHECK-NEXT:        (i32.const 1)
+  ;; CHECK-NEXT:       )
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:      (drop
+  ;; CHECK-NEXT:       (i32.const 1)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  (func $add-overflow-unsigned-yes (param $x i32)
+    ;; As above, but unsigned.
+    (if
+      (i32.ge_u
+        (local.get $x)
+        (i32.const 1)
+      )
+      (then
+        (if
+          (i32.le_u
+            (local.get $x)
+            (i32.const 1000)
+          )
+          (then
+            (local.set $x
+              (i32.add
+                (local.get $x)
+                (i32.const 1)
+              )
+            )
+            ;; We do optimize to 1.
+            (drop
+              (i32.gt_u
+                (local.get $x)
+                (i32.const 1)
+              )
+            )
+          )
+        )
+      )
+    )
+  )
 )