[PATCH] D125395: [analyzer][solver] Handle UnarySymExpr in RangeConstraintSolver

[Balázs Benics via Phabricator via cfe-commits]

steakhal added a comment.

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



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1453
+    const RangeSet *NegatedRange = nullptr;
+    if (const UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) {
+      if (USE->getOpcode() == UO_Minus) {
----------------



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1454-1456
+      if (USE->getOpcode() == UO_Minus) {
+        // Just get the operand when we negate a symbol that is already negated.
+        // -(-a) == a, ~(~a) == a
----------------
The comment says that it would work with both `-` and `~`.
Why do you check against only `-`?


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1457-1458
+        // -(-a) == a, ~(~a) == a
+        SymbolRef NegatedSym = USE->getOperand();
+        NegatedRange = getConstraint(State, NegatedSym);
+      }
----------------



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1464
+        QualType T = Sym->getType();
         SymbolManager &SymMgr = State->getSymbolManager();
         SymbolRef NegatedSym =
----------------
This `SymMgr` is acquired multiple times. We could hoist it and use it everywhere.


================
Comment at: clang/test/Analysis/constraint_manager_negate.c:16-20
+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__))
----------------
We can probably spare the unimportant stuff.


================
Comment at: clang/test/Analysis/constraint_manager_negate.c:23-24
+void negate_positive_range(int a) {
+  if (-a <= 0)
+    return;
+  // -a: [1, INT_MAX]
----------------
Why don't you use `assert(-a > 0)` here? It should be equivalent. Same for the rest.


================
Comment at: clang/test/Analysis/constraint_manager_negate.c:27-29
+  clang_analyzer_eval(a < 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(a >= INT_MIN); // expected-warning{{TRUE}}
+  clang_analyzer_eval(a == INT_MIN); // expected-warning{{FALSE}}
----------------
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.


================
Comment at: clang/test/Analysis/constraint_manager_negate.c:46
+    return;
+  clang_analyzer_eval(-a == INT_MIN); // expected-warning{{TRUE}}
+}
----------------
Let's also assert `a == INT_MIN` just for the symmetry.


================
Comment at: clang/test/Analysis/constraint_manager_negate.c:69-73
+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}}
+}
----------------
Sweet!!


================
Comment at: clang/test/Analysis/constraint_manager_negate.c:76
+void negate_unsigned_min(unsigned a) {
+  if (a == UINT_MIN) {
+    clang_analyzer_eval(-a == UINT_MIN); // expected-warning{{TRUE}}
----------------
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.


================
Comment at: clang/test/Analysis/constraint_manager_negate.c:87-88
+  if (a == 4u) {
+    clang_analyzer_eval(-a == 4u); // expected-warning{{FALSE}}
+    clang_analyzer_eval(-a != 4u); // expected-warning{{TRUE}}
+  }
----------------
Add an equality comparison which results in `TRUE`.


================
Comment at: clang/test/Analysis/constraint_manager_negate.c:92-98
+_Static_assert(UINT_MID == -UINT_MID, "");
+void negate_unsigned_mid(unsigned a) {
+  if (a == UINT_MID) {
+    clang_analyzer_eval(-a == UINT_MID); // expected-warning{{TRUE}}
+    clang_analyzer_eval(-a != UINT_MID); // expected-warning{{FALSE}}
+  }
+}
----------------
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.


================
Comment at: clang/test/Analysis/constraint_manager_negate.c:100-105
+void negate_unsigned_mid2(unsigned a) {
+  if (a < UINT_MID && a > UINT_MIN) {
+    clang_analyzer_eval(-a > UINT_MID); // expected-warning{{TRUE}}
+    clang_analyzer_eval(-a < UINT_MID); // expected-warning{{FALSE}}
+  }
+}
----------------
I believe the eval query can be sharper than this.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D125395/new/

https://reviews.llvm.org/D125395