[PATCH] D106823: [analyzer][solver] Iterate to a fixpoint during symbol simplification with constants

[Gabor Marton via Phabricator via cfe-commits]

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

Thanks for the review!



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2112-2113
+  assert(ClsMembers.contains(Old));
+  assert(ClsMembers.getHeight() > 1 &&
+         "Class should have at least two members");
+
----------------
vsavchenko wrote:
> Maybe after removing you can check that `ClsMembers` is not empty?
> I just don't like relying on `getHeight` because it looks like an implementation detail and shouldn't be used.  We use it only in one place in the whole codebase (in equivalence classes :) ), but since we can re-write this assertion to have a simpler condition, I think that it should be preferred.
Okay, I've also found it inconvenient to use `getHeight` but the API of immutable maps is quite sparse, I mean there is no way to query the size. The solution you suggest is better in the sense we don't have to use the internal API, so I've changed it that way, though, it has the disadvantage that we must check the precondition of the function in the middle of it which is weird to read. 
What about having a free function that takes a tree as a param and returns whether it has two members? Or we could even extend the API of the immutable AVL  tree with a new member function.


================
Comment at: clang/test/Analysis/symbol-simplification-fixpoint-iteration-unreachable-code.cpp:20
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  clang_analyzer_printState();
+
----------------
vsavchenko wrote:
> Do we need to print states in this test?
Good point, I've accidentally left it here.


================
Comment at: clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp:32
+  // CHECK-NEXT:   "equivalence_classes": [
+  // CHECK-NEXT:     [ "(reg_$0<int a>) != (reg_$2<int c>)" ],
+  // CHECK-NEXT:     [ "reg_$0<int a>", "reg_$2<int c>" ]
----------------
vsavchenko wrote:
> Same question here
> OK, I understand the next two classes. But how did we produce this one?

Simplification is done on each equivalence class we can find in the state, no matter if they are non-trivial or trivial classes.

Here is what happens in this case: We skim through the constraints and try to simplify all equivalence classes there. During this we start simplifying the trivial equivalence class `((reg_$0<int a>) + (reg_$1<int b>)) != (reg_$2<int c>)`. The first and only member of this class can be simplified with `(reg_$0<int a>) != (reg_$2<int c>)` because `b==0`. Now, we merge the two trivial classes of the original non-simplified and the new simplified symbols. At this point we receive a non-trivial class with two members: `((reg_$0<int a>) + (reg_$1<int b>)) != (reg_$2<int c>)` and `(reg_$0<int a>) != (reg_$2<int c>)`. And then we remove the old symbol from the class. That results in a non-trivial class with one member: `(reg_$0<int a>) != (reg_$2<int c>)`.


================
Comment at: clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp:36
+  // CHECK-NEXT:  "equivalence_classes": [
+  // CHECK-NEXT:    [ "(reg_$0<int a>) != (reg_$3<int d>)" ],
+  // CHECK-NEXT:    [ "reg_$0<int a>", "reg_$3<int d>" ],
----------------
vsavchenko wrote:
> OK, I understand the next two classes.
> But how did we produce this one?
I am giving an answer to this in the previous test file, because that case is shorter and easier to explain.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106823