[PATCH] D114619: [Analyzer][solver] Do not remove the simplified symbol from the eq class

2021-12-01 Thread Nico Weber via Phabricator via cfe-commits 
thakis added a comment.

Thanks for the fix!


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D114619

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D114619: [Analyzer][solver] Do not remove the simplified symbol from the eq class

2021-12-01 Thread Gabor Marton via Phabricator via cfe-commits 
martong added a comment.

I've had the confidence to commit D114887 , 
the test should not be flaky anymore.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D114619

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D114619: [Analyzer][solver] Do not remove the simplified symbol from the eq class

2021-12-01 Thread Gabor Marton via Phabricator via cfe-commits 
martong added a comment.

@thakis, if the issue is really disturbing and cannot wait until the review of 
D114887  finishes then please do a revert of 
this patch. But then the dependent child patch D103317 
 needs to be reverted as well.
I am trying my best to make D114887  reviewed 
in the next 24 hours.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D114619

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D114619: [Analyzer][solver] Do not remove the simplified symbol from the eq class

2021-12-01 Thread Gabor Marton via Phabricator via cfe-commits 
martong added a comment.

In D114619#3164898 , @thakis wrote:

> The test sometimes fails flakily: http://45.33.8.238/macm1/22813/step_7.txt

Thanks @thakis for the report, I am aware of the issue and addressing that in
https://reviews.llvm.org/D114887


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D114619

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D114619: [Analyzer][solver] Do not remove the simplified symbol from the eq class

2021-12-01 Thread Nico Weber via Phabricator via cfe-commits 
thakis added a comment.

The test sometimes fails flakily: http://45.33.8.238/macm1/22813/step_7.txt


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D114619

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D114619: [Analyzer][solver] Do not remove the simplified symbol from the eq class

2021-11-30 Thread Gabor Marton via Phabricator via cfe-commits 
This revision was automatically updated to reflect the committed changes.
Closed by commit rGf02c5f347831: [Analyzer][solver] Do not remove the 
simplified symbol from the eq class (authored by martong).

Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D114619

Files:
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/test/Analysis/expr-inspection-printState-eq-classes.c
  clang/test/Analysis/symbol-simplification-disequality-info.cpp
  clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
  clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp

Index: clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
===
--- clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
+++ clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
@@ -27,17 +27,20 @@
   if (b != 0)
 return;
   clang_analyzer_printState();
-  // CHECK:   "constraints": [
-  // CHECK-NEXT:{ "symbol": "(reg_$0) != (reg_$3)", "range": "{ [0, 0] }" },
-  // CHECK-NEXT:{ "symbol": "reg_$1", "range": "{ [0, 0] }" },
-  // CHECK-NEXT:{ "symbol": "reg_$2", "range": "{ [0, 0] }" }
-  // CHECK-NEXT:  ],
-  // CHECK-NEXT:  "equivalence_classes": [
-  // CHECK-NEXT:[ "(reg_$0) != (reg_$3)" ],
-  // CHECK-NEXT:[ "reg_$0", "reg_$3" ],
-  // CHECK-NEXT:[ "reg_$2" ]
-  // CHECK-NEXT:  ],
-  // CHECK-NEXT:  "disequality_info": null,
+  // CHECK:  "constraints": [
+  // CHECK-NEXT:   { "symbol": "(((reg_$0) + (reg_$1)) + (reg_$2)) != (reg_$3)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "((reg_$0) + (reg_$2)) != (reg_$3)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "(reg_$0) != (reg_$3)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "(reg_$2) + (reg_$1)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "reg_$1", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "reg_$2", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "equivalence_classes": [
+  // CHECK-NEXT:   [ "(((reg_$0) + (reg_$1)) + (reg_$2)) != (reg_$3)", "((reg_$0) + (reg_$2)) != (reg_$3)", "(reg_$0) != (reg_$3)" ],
+  // CHECK-NEXT:   [ "((reg_$0) + (reg_$1)) + (reg_$2)", "(reg_$0) + (reg_$2)", "reg_$0", "reg_$3" ],
+  // CHECK-NEXT:   [ "(reg_$2) + (reg_$1)", "reg_$2" ]
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "disequality_info": null,
 
   // Keep the symbols and the constraints! alive.
   (void)(a * b * c * d);
Index: clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
===
--- clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
+++ clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
@@ -24,14 +24,15 @@
   if (b != 0)
 return;
   clang_analyzer_printState();
-  // CHECK:"constraints": [
-  // CHECK-NEXT: { "symbol": "(reg_$0) != (reg_$2)", "range": "{ [0, 0] }" },
-  // CHECK-NEXT: { "symbol": "reg_$1", "range": "{ [0, 0] }" }
-  // CHECK-NEXT:   ],
-  // CHECK-NEXT:   "equivalence_classes": [
-  // CHECK-NEXT: [ "(reg_$0) != (reg_$2)" ],
-  // CHECK-NEXT: [ "reg_$0", "reg_$2" ]
-  // CHECK-NEXT:   ],
+  // CHECK:  "constraints": [
+  // CHECK-NEXT:   { "symbol": "((reg_$0) + (reg_$1)) != (reg_$2)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "(reg_$0) != (reg_$2)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "reg_$1", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "equivalence_classes": [
+  // CHECK-NEXT:   [ "((reg_$0) + (reg_$1)) != (reg_$2)", "(reg_$0) != (reg_$2)" ],
+  // CHECK-NEXT:   [ "(reg_$0) + (reg_$1)", "reg_$0", "reg_$2" ]
+  // CHECK-NEXT: ],
   // CHECK-NEXT: "disequality_info": null,
 
   // Keep the symbols and the constraints! alive.
Index: clang/test/Analysis/symbol-simplification-disequality-info.cpp
===
--- clang/test/Analysis/symbol-simplification-disequality-info.cpp
+++ clang/test/Analysis/symbol-simplification-disequality-info.cpp
@@ -12,18 +12,18 @@
   if (a + b + c == d)
 return;
   clang_analyzer_printState();
-  // CHECK:   "disequality_info": [
-  // CHECK-NEXT:{
-  // CHECK-NEXT:  "class": [ "((reg_$0) + (reg_$1)) + (reg_$2)" ],
-  // CHECK-NEXT:  "disequal_to": [
-  // CHECK-NEXT:[ "reg_$3" ]]
-  // CHECK-NEXT:},
-  // CHECK-NEXT:{
-  // CHECK-NEXT:  "class": [ "reg_$3" ],
-  // CHECK-NEXT:  "disequal_to": [
-  // CHECK-NEXT:[ "((reg_$0) + (reg_$1)) + (reg_$2)" ]]
-  // CHECK-NEXT:}
-  // CHECK-NEXT:  ],
+  // CHECK:  "disequality_info": [
+  // CHECK-NEXT:   {
+  // CHECK-NEXT: "class": [ "((reg_$0) + (reg_$1)) + (reg_$2)" ],
+  // CHECK-NEXT: "disequal_to": [
+  // CHECK-NEXT:   [ "reg_$3" ]]
+  //

[PATCH] D114619: [Analyzer][solver] Do not remove the simplified symbol from the eq class

2021-11-29 Thread Balázs Benics via Phabricator via cfe-commits 
steakhal accepted this revision.
steakhal added a comment.
This revision is now accepted and ready to land.

I think it looks great.




Comment at: clang/test/Analysis/symbol-simplification-disequality-info.cpp:15-26
+  // CHECK:  "disequality_info": [
+  // CHECK-NEXT:   {
+  // CHECK-NEXT: "class": [ "((reg_$0) + (reg_$1)) + 
(reg_$2)" ],
+  // CHECK-NEXT: "disequal_to": [
+  // CHECK-NEXT:   [ "reg_$3" ]]
+  // CHECK-NEXT:   },
+  // CHECK-NEXT:   {

martong wrote:
> steakhal wrote:
> > Please try to omit unnecessary changes.
> I've made this change intentionally, so all hunks for each simplification 
> steps are indented similarly. E.g., after the `CHECK-NEXT:` string comes 3 
> space characters until we the `{` character, see L16 and L34 and L51. 
> Actually, I've made an indentation error in a previous patch, which I though 
> I can correct now.
> 
Fine by me.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D114619

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D114619: [Analyzer][solver] Do not remove the simplified symbol from the eq class

2021-11-29 Thread Gabor Marton via Phabricator via cfe-commits 
martong added a comment.

In D114619#3155363 , @steakhal wrote:

> I see. Simplification is always good. Let's measure and compare the runtime 
> characteristics before moving forward.

Here they are. Seems like the runtime and memory consumption are pretty much 
the same.

F20788018: no_removemember.png 

F20788026: stats.html 


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D114619

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D114619: [Analyzer][solver] Do not remove the simplified symbol from the eq class

2021-11-29 Thread Gabor Marton via Phabricator via cfe-commits 
martong added inline comments.



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2226
+  //
+  // Empirical measurements show that if we relax assumption G then the
+  // runtime does not grow noticeably. This is most probably because the

steakhal wrote:
> Emphasize what you mean by //relaxation//. You meant probably something like 
> //not replacing the complex symbol, just adding the simplified version to the 
> class//.
ok



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2227
+  // Empirical measurements show that if we relax assumption G then the
+  // runtime does not grow noticeably. This is most probably because the
+  // cost of removing the simplified member is much higher than the cost of

steakhal wrote:
> nor memory consumption
ok



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2228-2229
+  // runtime does not grow noticeably. This is most probably because the
+  // cost of removing the simplified member is much higher than the cost of
+  // simplifying the symbol.
   State = reAssume(State, ClassConstraint, SimplifiedMemberVal);

steakhal wrote:
> Could you please elaborate on this in the review? I don't get the reasoning. 
> I might miss something.
It's not a reasoning, just a guessing. Another reason could be that simply the 
time we spend here is negligible compared to the time we spend e.g. in 
removeDeadBindings. (Actually,  removeDeadBindings is very hot and takes 
roughly 15-20 % of the runtime.) Perhaps I could do a measurement with a 
sampling profiler to be able to provide a precise explanation to this. But I 
think the point is that the runtime/memory consumption do not grow and the 
concrete reason is secondary.

However, you are right, I should not get into guessing here, I'll just remove 
this sentence.



Comment at: clang/test/Analysis/symbol-simplification-disequality-info.cpp:15-26
+  // CHECK:  "disequality_info": [
+  // CHECK-NEXT:   {
+  // CHECK-NEXT: "class": [ "((reg_$0) + (reg_$1)) + 
(reg_$2)" ],
+  // CHECK-NEXT: "disequal_to": [
+  // CHECK-NEXT:   [ "reg_$3" ]]
+  // CHECK-NEXT:   },
+  // CHECK-NEXT:   {

steakhal wrote:
> Please try to omit unnecessary changes.
I've made this change intentionally, so all hunks for each simplification steps 
are indented similarly. E.g., after the `CHECK-NEXT:` string comes 3 space 
characters until we the `{` character, see L16 and L34 and L51. Actually, I've 
made an indentation error in a previous patch, which I though I can correct now.



Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D114619

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D114619: [Analyzer][solver] Do not remove the simplified symbol from the eq class

2021-11-29 Thread Gabor Marton via Phabricator via cfe-commits 
martong updated this revision to Diff 390349.
martong marked 4 inline comments as done.
martong added a comment.

- Update a comment


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D114619

Files:
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/test/Analysis/expr-inspection-printState-eq-classes.c
  clang/test/Analysis/symbol-simplification-disequality-info.cpp
  clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
  clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp

Index: clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
===
--- clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
+++ clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
@@ -27,17 +27,20 @@
   if (b != 0)
 return;
   clang_analyzer_printState();
-  // CHECK:   "constraints": [
-  // CHECK-NEXT:{ "symbol": "(reg_$0) != (reg_$3)", "range": "{ [0, 0] }" },
-  // CHECK-NEXT:{ "symbol": "reg_$1", "range": "{ [0, 0] }" },
-  // CHECK-NEXT:{ "symbol": "reg_$2", "range": "{ [0, 0] }" }
-  // CHECK-NEXT:  ],
-  // CHECK-NEXT:  "equivalence_classes": [
-  // CHECK-NEXT:[ "(reg_$0) != (reg_$3)" ],
-  // CHECK-NEXT:[ "reg_$0", "reg_$3" ],
-  // CHECK-NEXT:[ "reg_$2" ]
-  // CHECK-NEXT:  ],
-  // CHECK-NEXT:  "disequality_info": null,
+  // CHECK:  "constraints": [
+  // CHECK-NEXT:   { "symbol": "(((reg_$0) + (reg_$1)) + (reg_$2)) != (reg_$3)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "((reg_$0) + (reg_$2)) != (reg_$3)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "(reg_$0) != (reg_$3)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "(reg_$2) + (reg_$1)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "reg_$1", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "reg_$2", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "equivalence_classes": [
+  // CHECK-NEXT:   [ "(((reg_$0) + (reg_$1)) + (reg_$2)) != (reg_$3)", "((reg_$0) + (reg_$2)) != (reg_$3)", "(reg_$0) != (reg_$3)" ],
+  // CHECK-NEXT:   [ "((reg_$0) + (reg_$1)) + (reg_$2)", "(reg_$0) + (reg_$2)", "reg_$0", "reg_$3" ],
+  // CHECK-NEXT:   [ "(reg_$2) + (reg_$1)", "reg_$2" ]
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "disequality_info": null,
 
   // Keep the symbols and the constraints! alive.
   (void)(a * b * c * d);
Index: clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
===
--- clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
+++ clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
@@ -24,14 +24,15 @@
   if (b != 0)
 return;
   clang_analyzer_printState();
-  // CHECK:"constraints": [
-  // CHECK-NEXT: { "symbol": "(reg_$0) != (reg_$2)", "range": "{ [0, 0] }" },
-  // CHECK-NEXT: { "symbol": "reg_$1", "range": "{ [0, 0] }" }
-  // CHECK-NEXT:   ],
-  // CHECK-NEXT:   "equivalence_classes": [
-  // CHECK-NEXT: [ "(reg_$0) != (reg_$2)" ],
-  // CHECK-NEXT: [ "reg_$0", "reg_$2" ]
-  // CHECK-NEXT:   ],
+  // CHECK:  "constraints": [
+  // CHECK-NEXT:   { "symbol": "((reg_$0) + (reg_$1)) != (reg_$2)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "(reg_$0) != (reg_$2)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "reg_$1", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "equivalence_classes": [
+  // CHECK-NEXT:   [ "((reg_$0) + (reg_$1)) != (reg_$2)", "(reg_$0) != (reg_$2)" ],
+  // CHECK-NEXT:   [ "(reg_$0) + (reg_$1)", "reg_$0", "reg_$2" ]
+  // CHECK-NEXT: ],
   // CHECK-NEXT: "disequality_info": null,
 
   // Keep the symbols and the constraints! alive.
Index: clang/test/Analysis/symbol-simplification-disequality-info.cpp
===
--- clang/test/Analysis/symbol-simplification-disequality-info.cpp
+++ clang/test/Analysis/symbol-simplification-disequality-info.cpp
@@ -12,18 +12,18 @@
   if (a + b + c == d)
 return;
   clang_analyzer_printState();
-  // CHECK:   "disequality_info": [
-  // CHECK-NEXT:{
-  // CHECK-NEXT:  "class": [ "((reg_$0) + (reg_$1)) + (reg_$2)" ],
-  // CHECK-NEXT:  "disequal_to": [
-  // CHECK-NEXT:[ "reg_$3" ]]
-  // CHECK-NEXT:},
-  // CHECK-NEXT:{
-  // CHECK-NEXT:  "class": [ "reg_$3" ],
-  // CHECK-NEXT:  "disequal_to": [
-  // CHECK-NEXT:[ "((reg_$0) + (reg_$1)) + (reg_$2)" ]]
-  // CHECK-NEXT:}
-  // CHECK-NEXT:  ],
+  // CHECK:  "disequality_info": [
+  // CHECK-NEXT:   {
+  // CHECK-NEXT: "class": [ "((reg_$0) + (reg_$1)) + (reg_$2)" ],
+  // CHECK-NEXT: "disequal_to": [
+  // CHECK-NEXT:   [ "reg_$3" ]]
+  // CHECK-NEXT:   },
+  // CHECK-NEXT:   {
+  // CHECK-NEXT: "class": [ "reg_$3"

[PATCH] D114619: [Analyzer][solver] Do not remove the simplified symbol from the eq class

2021-11-26 Thread Balázs Benics via Phabricator via cfe-commits 
steakhal added a comment.

I see. Simplification is always good. Let's measure and compare the runtime 
characteristics before moving forward.




Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2226
+  //
+  // Empirical measurements show that if we relax assumption G then the
+  // runtime does not grow noticeably. This is most probably because the

Emphasize what you mean by //relaxation//. You meant probably something like 
//not replacing the complex symbol, just adding the simplified version to the 
class//.



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2227
+  // Empirical measurements show that if we relax assumption G then the
+  // runtime does not grow noticeably. This is most probably because the
+  // cost of removing the simplified member is much higher than the cost of

nor memory consumption



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2228-2229
+  // runtime does not grow noticeably. This is most probably because the
+  // cost of removing the simplified member is much higher than the cost of
+  // simplifying the symbol.
   State = reAssume(State, ClassConstraint, SimplifiedMemberVal);

Could you please elaborate on this in the review? I don't get the reasoning. I 
might miss something.



Comment at: clang/test/Analysis/symbol-simplification-disequality-info.cpp:15-26
+  // CHECK:  "disequality_info": [
+  // CHECK-NEXT:   {
+  // CHECK-NEXT: "class": [ "((reg_$0) + (reg_$1)) + 
(reg_$2)" ],
+  // CHECK-NEXT: "disequal_to": [
+  // CHECK-NEXT:   [ "reg_$3" ]]
+  // CHECK-NEXT:   },
+  // CHECK-NEXT:   {

Please try to omit unnecessary changes.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D114619

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D114619: [Analyzer][solver] Do not remove the simplified symbol from the eq class

2021-11-26 Thread Gabor Marton via Phabricator via cfe-commits 
martong created this revision.
martong added a reviewer: steakhal.
Herald added subscribers: manas, ASDenysPetrov, gamesh411, dkrupp, donat.nagy, 
Szelethus, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware, 
xazax.hun.
Herald added a reviewer: Szelethus.
martong requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

Currently, during symbol simplification we remove the original member symbol
from the equivalence class (`ClassMembers` trait). However, we keep the
reverse link (`ClassMap` trait), in order to be able the query the
related constraints even for the old member. This asymmetry can lead to
a problem when we merge equivalence classes:

  ClassA: [a, b]   // ClassMembers trait,
  a->a, b->a   // ClassMap trait, a is the representative symbol

Now lets delete `a`:

  ClassA: [b]
  a->a, b->a

Let's merge the trivial class `c` into ClassA:

  ClassA: [c, b]
  c->c, b->c, a->a

Now after the merge operation, `c` and `a` are actually in different
equivalence classes, which is inconsistent.

One solution to this problem is to simply avoid removing the original
member and this is what this patch does.

Other options I have considered:

1. Always merge the trivial class into the non-trivial class. This might work 
most of the time, however, will fail if we have to merge two non-trivial 
classes (in that case we no longer can track equivalences precisely).
2. In `removeMember`, update the reverse link as well. This would cease the 
inconsistency, but we'd loose precision since we could not query the 
constraints for the removed member.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D114619

Files:
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/test/Analysis/expr-inspection-printState-eq-classes.c
  clang/test/Analysis/symbol-simplification-disequality-info.cpp
  clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
  clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp

Index: clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
===
--- clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
+++ clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
@@ -27,17 +27,20 @@
   if (b != 0)
 return;
   clang_analyzer_printState();
-  // CHECK:   "constraints": [
-  // CHECK-NEXT:{ "symbol": "(reg_$0) != (reg_$3)", "range": "{ [0, 0] }" },
-  // CHECK-NEXT:{ "symbol": "reg_$1", "range": "{ [0, 0] }" },
-  // CHECK-NEXT:{ "symbol": "reg_$2", "range": "{ [0, 0] }" }
-  // CHECK-NEXT:  ],
-  // CHECK-NEXT:  "equivalence_classes": [
-  // CHECK-NEXT:[ "(reg_$0) != (reg_$3)" ],
-  // CHECK-NEXT:[ "reg_$0", "reg_$3" ],
-  // CHECK-NEXT:[ "reg_$2" ]
-  // CHECK-NEXT:  ],
-  // CHECK-NEXT:  "disequality_info": null,
+  // CHECK:  "constraints": [
+  // CHECK-NEXT:   { "symbol": "(((reg_$0) + (reg_$1)) + (reg_$2)) != (reg_$3)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "((reg_$0) + (reg_$2)) != (reg_$3)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "(reg_$0) != (reg_$3)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "(reg_$2) + (reg_$1)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "reg_$1", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "reg_$2", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "equivalence_classes": [
+  // CHECK-NEXT:   [ "(((reg_$0) + (reg_$1)) + (reg_$2)) != (reg_$3)", "((reg_$0) + (reg_$2)) != (reg_$3)", "(reg_$0) != (reg_$3)" ],
+  // CHECK-NEXT:   [ "((reg_$0) + (reg_$1)) + (reg_$2)", "(reg_$0) + (reg_$2)", "reg_$0", "reg_$3" ],
+  // CHECK-NEXT:   [ "(reg_$2) + (reg_$1)", "reg_$2" ]
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "disequality_info": null,
 
   // Keep the symbols and the constraints! alive.
   (void)(a * b * c * d);
Index: clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
===
--- clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
+++ clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
@@ -24,14 +24,15 @@
   if (b != 0)
 return;
   clang_analyzer_printState();
-  // CHECK:"constraints": [
-  // CHECK-NEXT: { "symbol": "(reg_$0) != (reg_$2)", "range": "{ [0, 0] }" },
-  // CHECK-NEXT: { "symbol": "reg_$1", "range": "{ [0, 0] }" }
-  // CHECK-NEXT:   ],
-  // CHECK-NEXT:   "equivalence_classes": [
-  // CHECK-NEXT: [ "(reg_$0) != (reg_$2)" ],
-  // CHECK-NEXT: [ "reg_$0", "reg_$2" ]
-  // CHECK-NEXT:   ],
+  // CHECK:  "constraints": [
+  // CHECK-NEXT:   { "symbol": "((reg_$0) + (reg_$1)) != (reg_$2)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "(reg_$0) != (reg_$2)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "reg_$1", "range": "{ [0, 0] }" }
+  //