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

[Gabor Marton via Phabricator via cfe-commits]

martong marked 13 inline comments as done.
martong added a comment.

In D125395#3506854 <https://reviews.llvm.org/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.



================
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
----------------
steakhal wrote:
> The comment says that it would work with both `-` and `~`.
> Why do you check against only `-`?
Unfortunately, the complement operation is not implemented on the RangeSet. So, yes, in this sense the comment is misleading, I've changed it.


================
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}}
----------------
steakhal wrote:
> 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.
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}}
```


================
Comment at: clang/test/Analysis/constraint_manager_negate.c:46
+    return;
+  clang_analyzer_eval(-a == INT_MIN); // expected-warning{{TRUE}}
+}
----------------
steakhal wrote:
> Let's also assert `a == INT_MIN` just for the symmetry.
That would be superfluous in my opinion, since I have changed the `if` to an
```
  assert(a == INT_MIN);
```


================
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}}
----------------
steakhal wrote:
> 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.
Ok, I changed to `assert` everywhere.


================
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}}
+  }
----------------
steakhal wrote:
> Add an equality comparison which results in `TRUE`.
Sure.


================
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}}
+  }
+}
----------------
steakhal wrote:
> I believe the eval query can be sharper than this.
Ok.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D125395