[PATCH] D111642: [Analyzer][solver] Simplification: reorganize equalities with adjustment

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

In D111642#3059467 <https://reviews.llvm.org/D111642#3059467>, @steakhal wrote:

> The coverage report of the test shows that L2124 is uncovered. Please add a test demonstrating that path as well.

I've added such a test, thanks for the notice!



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2126-2130
+      // Initiate the reorganization of the equality information. E.g., if we
+      // have `c + 1 == 0` then we'd like to express that `c == -1`. It makes
+      // sense to do this only with `SymIntExpr`s.
+      // TODO Handle `IntSymExpr` as well, once computeAdjustment can handle
+      // them.
----------------
steakhal wrote:
> Can the simplification of a `SymSymExpr` result in `IntSymExpr`? If it can happen, then we could see such instances and we should do the right thing with them as well.
> WDYT?
> Can the simplification of a `SymSymExpr` result in `IntSymExpr`?
Yes it can. However, in order to handle them we should extend `computeAdjustment` properly, which is absolutely not trivial - considering the test cases in `additive-folding.cpp` -  So, I'd rather address that in another patch.



================
Comment at: clang/test/Analysis/solver-sym-simplification-adjustment.c:36
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  if (b != 1)                      // b == 1  --> c + 1: [-1,0] --> c: [-2,-1]
+    return;
----------------
steakhal wrote:
> Please express that `C: [-2,-1]` is then intersected with the already associated range which is `[-1,1]`, thus we get `c: [-1,-1]`.
Ok, I've added that comment.


================
Comment at: clang/test/Analysis/solver-sym-simplification-adjustment.c:55
+  if (b != 1)         // b == 1  --> c + 1 == 0 --> c == -1 contradiction
+    return;
+  clang_analyzer_warnIfReached(); // no warning
----------------
steakhal wrote:
> Can we infer within this true branch that `b` must be `0` to make this path feasible?
> If we already can infer this, can we put there the appropriate assertion?
> If not, an assertion would be justified with a FIXME.
> Can we infer within this true branch that `b` must be `0` to make this path feasible?
Yes, we can.

> If we already can infer this, can we put there the appropriate assertion?
Ok, I've added the appropriate `clang_analyzer_eval` to check this.



Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D111642