[analyzer][solver] Handle UnarySymExpr in RangeConstraintSolver

[martong]

• Add false positive test

[martong]

Fixes https://github.com/llvm/llvm-project/issues/55241

[steakhal]

Great content!
I've got a long list of nits though. Nothing personal :D

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1462–1463

This SymMgr is acquired multiple times. We could hoist it and use it everywhere.

1463

1464–1466

The comment says that it would work with both - and ~.
Why do you check against only -?

1467–1468

clang/test/Analysis/constraint_manager_negate.c

17–21

We can probably spare the unimportant stuff.

24–25

Why don't you use assert(-a > 0) here? It should be equivalent. Same for the rest.

28–30

You can also query if the bound is sharp, by asking the same question but with a slightly different value and expect UNKNOWN.

clang_analyzer_eval(a < 0); // expected-warning{{TRUE}}
clang_analyzer_eval(a < -1); // expected-warning{{UNKNOWN}}

I also believe that a >= INT_MIN is TRUE for all a anyway, thus it can be omitted.
Checking against equality won't help much either, because we had no equality check before, thus it should result in FALSE unconditionally.

47

Let's also assert a == INT_MIN just for the symmetry.

70–74

Sweet!!

77

Well, this is the third form of expressing constraints.

1. Using asserts.
2. Use ifs but with early returns.
3. Use ifs but embed the code into the true branch.

Please, settle on one method.

88–89

Add an equality comparison which results in TRUE.

93–99

Leave a comment here that this is the only value besides zero where the negated is equal to the original value in the unsigned int domain.

101–106

I believe the eval query can be sharper than this.

[martong]

In D125395#3506854, @steakhal wrote:

Great content!
I've got a long list of nits though. Nothing personal :D

No worries, thank you for being assiduous.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1464–1466

Unfortunately, the complement operation is not implemented on the RangeSet. So, yes, in this sense the comment is misleading, I've changed it.

clang/test/Analysis/constraint_manager_negate.c

28–30

Okay, I changed it to something very obvious:

clang_analyzer_eval(a < 0); // expected-warning{{TRUE}}
clang_analyzer_eval(a > INT_MIN); // expected-warning{{TRUE}}

47

That would be superfluous in my opinion, since I have changed the if to an

assert(a == INT_MIN);

77

Ok, I changed to assert everywhere.

88–89

Sure.

101–106

Ok.

[martong]

• Address steakhal review comments

[martong]

• Add a test case for casts related crash

[steakhal]

LGTM

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

private:
   }
 
   /// Return a range set subtracting zero from \p Domain.
   RangeSet assumeNonZero(RangeSet Domain, QualType T) {
     APSIntType IntType = ValueFactory.getAPSIntType(T);
     return RangeFactory.deletePoint(Domain, IntType.getZeroValue());
   }
 
-  // FIXME: Once SValBuilder supports unary minus, we should use SValBuilder to
-  //        obtain the negated symbolic expression instead of constructing the
-  //        symbol manually. This will allow us to support finding ranges of not
-  //        only negated SymSymExpr-type expressions, but also of other, simpler
-  //        expressions which we currently do not know how to negate.
   Optional<RangeSet> getRangeForNegatedSub(SymbolRef Sym) {
-    if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) {
-      if (SSE->getOpcode() == BO_Sub) {
-        QualType T = Sym->getType();
-
-        // Do not negate unsigned ranges
-        if (!T->isUnsignedIntegerOrEnumerationType() &&
-            !T->isSignedIntegerOrEnumerationType())
-          return llvm::None;
+    // Do not negate if the type cannot be meaningfully negated.
+    if (!Sym->getType()->isUnsignedIntegerOrEnumerationType() &&
+        !Sym->getType()->isSignedIntegerOrEnumerationType())
 
-        SymbolManager &SymMgr = State->getSymbolManager();
+    const RangeSet *NegatedRange = nullptr;
+    if (const auto *USE = dyn_cast<UnarySymExpr>(Sym)) {
+      if (USE->getOpcode() == UO_Minus) {
+        // Just get the operand when we negate a symbol that is already negated.
+        // -(-a) == a
+        NegatedRange = getConstraint(State, USE->getOperand());
+      }
+    } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) {
+      if (SSE->getOpcode() == BO_Sub) {
+        QualType T = Sym->getType();
         SymbolRef NegatedSym =
             SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), T);
-
-        if (const RangeSet *NegatedRange = getConstraint(State, NegatedSym)) {
-          return RangeFactory.negate(*NegatedRange);
-        }
+        NegatedRange = getConstraint(State, NegatedSym);
       }
+    } else {
+      SymbolRef NegatedSym =
+          SymMgr.getUnarySymExpr(Sym, UO_Minus, Sym->getType());
+      NegatedRange = getConstraint(State, NegatedSym);
     }
+
+    if (NegatedRange)
+      return RangeFactory.negate(*NegatedRange);
     return llvm::None;
   }
 
   // Returns ranges only for binary comparison operators (except <=>)
   // when left and right operands are symbolic values.
   // Finds any other comparisons with the same operands.
   // Then do logical calculations and refuse impossible branches.
   // E.g. (x < y) and (x > y) at the same time are impossible.

clang/test/Analysis/constraint_manager_negate.c

+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -verify %s
+
+void clang_analyzer_eval(int);
+void clang_analyzer_dump(int);
+
+void exit(int);
+
+#define UINT_MIN (0U)
+#define UINT_MAX (~UINT_MIN)
+#define UINT_MID (UINT_MAX / 2 + 1)
+#define INT_MAX (UINT_MAX & (UINT_MAX >> 1))
+#define INT_MIN (UINT_MAX & ~(UINT_MAX >> 1))
+
+extern void abort() __attribute__((__noreturn__));
+#define assert(expr) ((expr) ? (void)(0) : abort())
+
+void negate_positive_range(int a) {
+  assert(-a > 0);
+  // -a: [1, INT_MAX]
+  // a: [INT_MIN + 1, -1]
+  clang_analyzer_eval(a < 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(a > INT_MIN); // expected-warning{{TRUE}}
+}
+
+void negate_positive_range2(int a) {
+  assert(a > 0);
+  // a: [1, INT_MAX]
+  // -a: [INT_MIN + 1, -1]
+  clang_analyzer_eval(-a < 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(-a > INT_MIN); // expected-warning{{TRUE}}
+}
+
+// INT_MIN equals 0b100...00.
+// Its two's compelement is 0b011...11 + 1 = 0b100...00 (itself).
+_Static_assert(INT_MIN == -INT_MIN, "");
+void negate_int_min(int a) {
+  assert(a == INT_MIN);
+  clang_analyzer_eval(-a == INT_MIN); // expected-warning{{TRUE}}
+}
+
+void negate_mixed(int a) {
+  assert(a > 0 || a == INT_MIN);
+  clang_analyzer_eval(-a <= 0); // expected-warning{{TRUE}}
+}
+
+void effective_range(int a) {
+  assert(a >= 0);
+  assert(-a >= 0);
+  clang_analyzer_eval(a == 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(-a == 0); // expected-warning{{TRUE}}
+}
+
+_Static_assert(-INT_MIN == INT_MIN, "");
+void effective_range_2(int a) {
+  assert(a <= 0);
+  assert(-a <= 0);
+  clang_analyzer_eval(a == 0 || a == INT_MIN); // expected-warning{{TRUE}}
+}
+
+void negate_symexpr(int a, int b) {
+  assert(3 <= a * b && a * b <= 5);
+  clang_analyzer_eval(-(a * b) >= -5); // expected-warning{{TRUE}}
+  clang_analyzer_eval(-(a * b) <= -3); // expected-warning{{TRUE}}
+}
+
+void negate_unsigned_min(unsigned a) {
+  assert(a == UINT_MIN);
+  clang_analyzer_eval(-a == UINT_MIN); // expected-warning{{TRUE}}
+  clang_analyzer_eval(-a != UINT_MIN); // expected-warning{{FALSE}}
+  clang_analyzer_eval(-a > UINT_MIN);  // expected-warning{{FALSE}}
+  clang_analyzer_eval(-a < UINT_MIN);  // expected-warning{{FALSE}}
+}
+
+_Static_assert(7u - 3u != 3u - 7u, "");
+_Static_assert(-4u == UINT_MAX - 3u, "");
+void negate_unsigned_4(unsigned a) {
+  assert(a == 4u);
+  clang_analyzer_eval(-a == 4u); // expected-warning{{FALSE}}
+  clang_analyzer_eval(-a != 4u); // expected-warning{{TRUE}}
+  clang_analyzer_eval(-a == UINT_MAX - 3u); // expected-warning{{TRUE}}
+}
+
+// UINT_MID equals 0b100...00.
+// Its two's compelement is 0b011...11 + 1 = 0b100...00 (itself).
+_Static_assert(UINT_MID == -UINT_MID, "");
+void negate_unsigned_mid(unsigned a) {
+  assert(a == UINT_MID);
+  clang_analyzer_eval(-a == UINT_MID); // expected-warning{{TRUE}}
+  clang_analyzer_eval(-a != UINT_MID); // expected-warning{{FALSE}}
+}
+
+void negate_unsigned_mid2(unsigned a) {
+  assert(UINT_MIN < a && a < UINT_MID);
+  // a:  [UINT_MIN+1, UINT_MID-1]
+  // -a: [UINT_MID+1, UINT_MAX]
+  clang_analyzer_eval(-a > UINT_MID); // expected-warning{{TRUE}}
+  clang_analyzer_eval(-a <= UINT_MAX); // expected-warning{{TRUE}}
+}
+
+_Static_assert(1u - 2u == UINT_MAX, "");
+_Static_assert(2u - 1u == 1, "");
+void negate_unsigned_max(unsigned a) {
+  assert(a == UINT_MAX);
+  clang_analyzer_eval(-a == 1); // expected-warning{{TRUE}}
+  clang_analyzer_eval(-a != 1); // expected-warning{{FALSE}}
+}
+void negate_unsigned_one(unsigned a) {
+  assert(a == 1);
+  clang_analyzer_eval(-a == UINT_MAX); // expected-warning{{TRUE}}
+  clang_analyzer_eval(-a < UINT_MAX);  // expected-warning{{FALSE}}
+}

clang/test/Analysis/constraint_manager_negate_difference.c

-// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin -analyzer-config aggressive-binary-operation-simplification=true -verify %s
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -verify %s
 
 void clang_analyzer_eval(int);
 
 void exit(int);
 
 #define UINT_MIN (0U)
 #define UINT_MAX (~UINT_MIN)
 #define UINT_MID (UINT_MAX / 2 + 1)
 #define INT_MAX (UINT_MAX & (UINT_MAX >> 1))
 #define INT_MIN (UINT_MAX & ~(UINT_MAX >> 1))
 
-extern void __assert_fail (__const char *__assertion, __const char *__file,
-    unsigned int __line, __const char *__function)
-     __attribute__ ((__noreturn__));
-#define assert(expr) \
-  ((expr)  ? (void)(0)  : __assert_fail (#expr, __FILE__, __LINE__, __func__))
+extern void abort() __attribute__((__noreturn__));
+#define assert(expr) ((expr) ? (void)(0) : abort())
 
 void assert_in_range(int x) {
   assert(x <= ((int)INT_MAX / 4));
   assert(x >= -(((int)INT_MAX) / 4));
 }
 
 void assert_in_wide_range(int x) {
   assert(x <= ((int)INT_MAX / 2));
   assert(x >= -(((int)INT_MAX) / 2));
 }
 
 void assert_in_range_2(int m, int n) {
   assert_in_range(m);
   assert_in_range(n);
 }
 
 void equal(int m, int n) {
   assert_in_range_2(m, n);
-  if (m != n)
-    return;
+  assert(m == n);
   assert_in_wide_range(m - n);
   clang_analyzer_eval(n == m); // expected-warning{{TRUE}}
 }
 
 void non_equal(int m, int n) {
   assert_in_range_2(m, n);
-  if (m == n)
-    return;
+  assert(m != n);
   assert_in_wide_range(m - n);
   clang_analyzer_eval(n != m); // expected-warning{{TRUE}}
 }
 
 void less_or_equal(int m, int n) {
   assert_in_range_2(m, n);
-  if (m < n)
-    return;
+  assert(m >= n);
   assert_in_wide_range(m - n);
   clang_analyzer_eval(n <= m); // expected-warning{{TRUE}}
 }
 
 void less(int m, int n) {
   assert_in_range_2(m, n);
-  if (m <= n)
-    return;
+  assert(m > n);
   assert_in_wide_range(m - n);
   clang_analyzer_eval(n < m); // expected-warning{{TRUE}}
 }
 
 void greater_or_equal(int m, int n) {
   assert_in_range_2(m, n);
-  if (m > n)
-    return;
+  assert(m <= n);
   assert_in_wide_range(m - n);
   clang_analyzer_eval(n >= m); // expected-warning{{TRUE}}
 }
 
 void greater(int m, int n) {
   assert_in_range_2(m, n);
-  if (m >= n)
-    return;
+  assert(m < n);
   assert_in_wide_range(m - n);
   clang_analyzer_eval(n > m); // expected-warning{{TRUE}}
 }
 
 void negate_positive_range(int m, int n) {
-  if (m - n <= 0)
-    return;
+  assert(m - n > 0);
   clang_analyzer_eval(n - m < 0); // expected-warning{{TRUE}}
   clang_analyzer_eval(n - m > INT_MIN); // expected-warning{{TRUE}}
-  clang_analyzer_eval(n - m == INT_MIN); // expected-warning{{FALSE}}
 }
 
+_Static_assert(INT_MIN == -INT_MIN, "");
 void negate_int_min(int m, int n) {
-  if (m - n != INT_MIN)
-    return;
+  assert(m - n == INT_MIN);
   clang_analyzer_eval(n - m == INT_MIN); // expected-warning{{TRUE}}
 }
 
 void negate_mixed(int m, int n) {
-  if (m -n > INT_MIN && m - n <= 0)
-    return;
+  assert(m - n > 0 || m - n == INT_MIN);
   clang_analyzer_eval(n - m <= 0); // expected-warning{{TRUE}}
 }
 
 void effective_range(int m, int n) {
   assert(m - n >= 0);
   assert(n - m >= 0);
   clang_analyzer_eval(m - n == 0); // expected-warning{{TRUE}}
   clang_analyzer_eval(n - m == 0); // expected-warning{{TRUE}}
 }
 
+_Static_assert(INT_MIN == -INT_MIN, "");
 void effective_range_2(int m, int n) {
   assert(m - n <= 0);
   assert(n - m <= 0);
-  clang_analyzer_eval(m - n == 0); // expected-warning{{TRUE}} expected-warning{{FALSE}}
-  clang_analyzer_eval(n - m == 0); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+  clang_analyzer_eval(m - n == 0 || m - n == INT_MIN); // expected-warning{{TRUE}}
 }
 
 void negate_unsigned_min(unsigned m, unsigned n) {
-  if (m - n == UINT_MIN) {
-    clang_analyzer_eval(n - m == UINT_MIN); // expected-warning{{TRUE}}
-    clang_analyzer_eval(n - m != UINT_MIN); // expected-warning{{FALSE}}
-    clang_analyzer_eval(n - m > UINT_MIN);  // expected-warning{{FALSE}}
-    clang_analyzer_eval(n - m < UINT_MIN);  // expected-warning{{FALSE}}
-  }
+  assert(m - n == UINT_MIN);
+
+_Static_assert(7u - 3u != 3u - 7u, "");
+void negate_unsigned_4(unsigned m, unsigned n) {
+  assert(m - n == 4u);
+  clang_analyzer_eval(n - m == 4u); // expected-warning{{FALSE}}
+  clang_analyzer_eval(n - m != 4u); // expected-warning{{TRUE}}
 }
 
+_Static_assert(UINT_MID == -UINT_MID, "");
 void negate_unsigned_mid(unsigned m, unsigned n) {
-  if (m - n == UINT_MID) {
-    clang_analyzer_eval(n - m == UINT_MID); // expected-warning{{TRUE}}
-    clang_analyzer_eval(n - m != UINT_MID); // expected-warning{{FALSE}}
-  }
-}
+  assert(m - n == UINT_MID);
 
 void negate_unsigned_mid2(unsigned m, unsigned n) {
-  if (m - n < UINT_MID && m - n > UINT_MIN) {
-    clang_analyzer_eval(n - m > UINT_MID); // expected-warning{{TRUE}}
-    clang_analyzer_eval(n - m < UINT_MID); // expected-warning{{FALSE}}
-  }
+  assert(UINT_MIN < m - n && m - n < UINT_MID);
+  clang_analyzer_eval(n - m <= UINT_MAX); // expected-warning{{TRUE}}
 }
 
+_Static_assert(1u - 2u == UINT_MAX, "");
+_Static_assert(2u - 1u == 1, "");
 void negate_unsigned_max(unsigned m, unsigned n) {
-  if (m - n == UINT_MAX) {
-    clang_analyzer_eval(n - m == 1); // expected-warning{{TRUE}}
-    clang_analyzer_eval(n - m != 1); // expected-warning{{FALSE}}
-  }
-}
+  assert(m - n == UINT_MAX);
 
 void negate_unsigned_one(unsigned m, unsigned n) {
-  if (m - n == 1) {
-    clang_analyzer_eval(n - m == UINT_MAX); // expected-warning{{TRUE}}
-    clang_analyzer_eval(n - m < UINT_MAX);  // expected-warning{{FALSE}}
-  }
-}
+  assert(m - n == 1);
 
 // The next code is a repro for the bug PR41588
 void negated_unsigned_range(unsigned x, unsigned y) {
-  clang_analyzer_eval(x - y != 0); // expected-warning{{FALSE}} expected-warning{{TRUE}}
-  clang_analyzer_eval(y - x != 0); // expected-warning{{FALSE}} expected-warning{{TRUE}}
+  clang_analyzer_eval(x - y != 0); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(y - x != 0); // expected-warning{{UNKNOWN}}
   // expected no assertion on the next line
-  clang_analyzer_eval(x - y != 0); // expected-warning{{FALSE}} expected-warning{{TRUE}}
+  clang_analyzer_eval(x - y != 0); // expected-warning{{UNKNOWN}}
 }

clang/test/Analysis/unary-sym-expr-no-crash.c

+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -analyzer-config support-symbolic-integer-casts=false \
+// RUN:   -verify
+
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -analyzer-config support-symbolic-integer-casts=true \
+// RUN:   -verify
+
+// expected-no-diagnostics
+
+void clang_analyzer_eval(int);
+void clang_analyzer_dump(int);
+
+void crash(int b, long c) {
+  b = c;
+  if (b > 0)
+    if(-b) // should not crash here
+      ;
+}

clang/test/Analysis/unary-sym-expr.c

 
 void test_svalbuilder_simplification(int x, int y) {
   if (x + y != 3)
     return;
   clang_analyzer_eval(-(x + y) == -3); // expected-warning{{TRUE}}
   // FIXME Commutativity is not supported yet.
   clang_analyzer_eval(-(y + x) == -3); // expected-warning{{UNKNOWN}}
 }
+
+int test_fp(int flag) {
+  int value;
+  if (flag == 0)
+    value = 1;
+  if (-flag == 0)
+    return value; // no-warning
+  return 42;
+}