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

[Gabor Marton via Phabricator via cfe-commits]

This revision was automatically updated to reflect the committed changes.
Closed by commit rG806329da0700: [analyzer][solver] Iterate to a fixpoint 
during symbol simplification with… (authored by martong).

Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106823

Files:
  
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
  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-iteration-unreachable-code.cpp
  clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
  clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
  clang/test/Analysis/symbol-simplification-reassume.cpp

Index: clang/test/Analysis/symbol-simplification-reassume.cpp
===
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-reassume.cpp
@@ -0,0 +1,37 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -verify
+
+// In this test we check whether the solver's symbol simplification mechanism
+// is capable of re-assuming simiplified symbols.
+
+void clang_analyzer_eval(bool);
+void clang_analyzer_warnIfReached();
+
+void test_reassume_false_range(int x, int y) {
+  if (x + y != 0) // x + y == 0
+return;
+  if (x != 1) // x == 1
+return;
+  clang_analyzer_eval(y == -1); // expected-warning{{TRUE}}
+}
+
+void test_reassume_true_range(int x, int y) {
+  if (x + y != 1) // x + y == 1
+return;
+  if (x != 1) // x == 1
+return;
+  clang_analyzer_eval(y == 0); // expected-warning{{TRUE}}
+}
+
+void test_reassume_inclusive_range(int x, int y) {
+  if (x + y < 0 || x + y > 1) // x + y: [0, 1]
+return;
+  if (x != 1) // x == 1
+return;
+  // y: [-1, 0]
+  clang_analyzer_eval(y > 0); // expected-warning{{FALSE}}
+  clang_analyzer_eval(y < -1);// expected-warning{{FALSE}}
+}
Index: clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
===
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
@@ -0,0 +1,45 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   2>&1 | FileCheck %s
+
+// In this test we check whether the solver's symbol simplification mechanism
+// is capable of reaching a fixpoint. This should be done after TWO iterations.
+
+void clang_analyzer_printState();
+
+void test(int a, int b, int c, int d) {
+  if (a + b + c != d)
+return;
+  if (c + b != 0)
+return;
+  clang_analyzer_printState();
+  // CHECK:  "constraints": [
+  // CHECK-NEXT:   { "symbol": "(((reg_$0) + (reg_$1)) + (reg_$2)) != (reg_$3)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "(reg_$2) + (reg_$1)", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "equivalence_classes": [
+  // CHECK-NEXT:   [ "((reg_$0) + (reg_$1)) + (reg_$2)", "reg_$3" ]
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "disequality_info": null,
+
+  // Simplification starts here.
+  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,
+
+  // Keep the symbols and the constraints! alive.
+  (void)(a * b * c * d);
+  return;
+}
Index: clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
===
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
@@ -0,0 +1,40 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   2>&1 | FileCheck %s
+
+// In this test we check whether the solver's symbol simplification mechanism
+// is capable of reaching a fixpoint. This should be done after one iteration.
+
+void clang_analyzer_printState();
+
+void test(int a, int b, int c) {
+  if (a + b != c)
+return;
+  clang_analyzer_printState();
+  // CHECK:  "constraints": [
+  // CHECK-NEXT:   { "symbol": "((reg_$0) + (reg_$1)) != (reg_$2)", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: 

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

[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.

In D106823#3109469 , @martong wrote:

>> As of diff 5, line 1767 and all the code in the block at line 2184 are 
>> uncovered by the tests you provided.
>
> Thanks, I've added new tests that cover the re-assume logic (the block of 
> line 2184).
>
> However, I was unable to add a test that covers  the case when the 
> simplification of a trivial symbol in the disequality info results an 
> infeasible state (line 1767). Here is how I tried: I had changed the line to 
> an assertion and then initiated the static analysis of the following 
> opensource projects: 
> memcached,tmux,curl,twin,redis,vim,openssl,sqlite,ffmpeg,postgresql,tinyxml2,libwebm,xerces,bitcoin,protobuf.
>  My idea had been, if the assertion would fired then I would use creduce to 
> the create the test case (btw, this is how I added the other infeasible state 
> test case). However, it did not fired.
>
> IMHO, having a defensive check at L1767 is correct b/c there is a slight 
> chance of reaching an infeasible state there. Although the chance is minimal, 
> I cannot prove that is 0.

It's fine by me. Thanks for the investigation.

In D106823#310 , @martong wrote:

> There are no runtime or peak memory usage growth with this patch (actually, 
> the runtime decreases with a few %).
> I am attaching the measurements results of the latest Diff.F20089096: 
> stats.html 

Great!

The tests refer to `reg_$0` by spelling the id number, which is unfortunate, 
but I suspect these tests will break for the slightest changes in the solver 
anyway so I'm not too bothered with this.

Please wait a week for the rest of the members of the community to have a look 
before committing.
@NoQ @Szelethus @ASDenysPetrov


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106823

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

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

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

There are no runtime or peak memory usage growth with this patch (actually, the 
runtime decreases with a few %).
I am attaching the measurements results of the latest Diff.F20089096: 
stats.html 


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106823

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

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

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

> As of diff 5, line 1767 and all the code in the block at line 2184 are 
> uncovered by the tests you provided.

Thanks, I've added new tests that cover the re-assume logic (the block of line 
2184).

However, I was unable to add a test that covers  the case when the 
simplification of a trivial symbol in the disequality info results an 
infeasible state (line 1767). Here is how I tried: I had changed the line to an 
assertion and then initiated the static analysis of the following opensource 
projects: 
memcached,tmux,curl,twin,redis,vim,openssl,sqlite,ffmpeg,postgresql,tinyxml2,libwebm,xerces,bitcoin,protobuf.
 My idea had been, if the assertion would fired then I would use creduce to the 
create the test case (btw, this is how I added the other infeasible state test 
case). However, it did not fired.

IMHO, having a defensive check at L1767 is correct b/c there is a slight chance 
of reaching an infeasible state there. Although the chance is minimal, I cannot 
prove that is 0.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106823

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

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

[Gabor Marton via Phabricator via cfe-commits]

martong updated this revision to Diff 384802.
martong added a comment.

- Add new tests to cover missing line coverage.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106823

Files:
  
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
  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-iteration-unreachable-code.cpp
  clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
  clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
  clang/test/Analysis/symbol-simplification-reassume.cpp

Index: clang/test/Analysis/symbol-simplification-reassume.cpp
===
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-reassume.cpp
@@ -0,0 +1,37 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -verify
+
+// In this test we check whether the solver's symbol simplification mechanism
+// is capable of re-assuming simiplified symbols.
+
+void clang_analyzer_eval(bool);
+void clang_analyzer_warnIfReached();
+
+void test_reassume_false_range(int x, int y) {
+  if (x + y != 0) // x + y == 0
+return;
+  if (x != 1) // x == 1
+return;
+  clang_analyzer_eval(y == -1); // expected-warning{{TRUE}}
+}
+
+void test_reassume_true_range(int x, int y) {
+  if (x + y != 1) // x + y == 1
+return;
+  if (x != 1) // x == 1
+return;
+  clang_analyzer_eval(y == 0); // expected-warning{{TRUE}}
+}
+
+void test_reassume_inclusive_range(int x, int y) {
+  if (x + y < 0 || x + y > 1) // x + y: [0, 1]
+return;
+  if (x != 1) // x == 1
+return;
+  // y: [-1, 0]
+  clang_analyzer_eval(y > 0); // expected-warning{{FALSE}}
+  clang_analyzer_eval(y < -1);// expected-warning{{FALSE}}
+}
Index: clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
===
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
@@ -0,0 +1,45 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   2>&1 | FileCheck %s
+
+// In this test we check whether the solver's symbol simplification mechanism
+// is capable of reaching a fixpoint. This should be done after TWO iterations.
+
+void clang_analyzer_printState();
+
+void test(int a, int b, int c, int d) {
+  if (a + b + c != d)
+return;
+  if (c + b != 0)
+return;
+  clang_analyzer_printState();
+  // CHECK:  "constraints": [
+  // CHECK-NEXT:   { "symbol": "(((reg_$0) + (reg_$1)) + (reg_$2)) != (reg_$3)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "(reg_$2) + (reg_$1)", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "equivalence_classes": [
+  // CHECK-NEXT:   [ "((reg_$0) + (reg_$1)) + (reg_$2)", "reg_$3" ]
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "disequality_info": null,
+
+  // Simplification starts here.
+  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,
+
+  // Keep the symbols and the constraints! alive.
+  (void)(a * b * c * d);
+  return;
+}
Index: clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
===
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
@@ -0,0 +1,40 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   2>&1 | FileCheck %s
+
+// In this test we check whether the solver's symbol simplification mechanism
+// is capable of reaching a fixpoint. This should be done after one iteration.
+
+void clang_analyzer_printState();
+
+void test(int a, int b, int c) {
+  if (a + b != c)
+return;
+  clang_analyzer_printState();
+  // CHECK:  "constraints": [
+  // CHECK-NEXT:   { "symbol": "((reg_$0) + (reg_$1)) != (reg_$2)", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "equivalence_classes": [
+  // CHECK-NEXT:   [ "(reg_$0) + (reg_$1)", "reg_$2" ]
+  // 

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

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

steakhal added inline comments.



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1732
+  if (!State)
+return false;
+}

martong wrote:
> steakhal wrote:
> > I'd love to see a coverage report of the tests you add with this patch.
> Ok, I am going to check the coverage and add the missing cases.
> Ok, I am going to check the coverage and add the missing cases.
As of diff 5, line 1767 and all the code in the block at line 2184 are 
uncovered by the tests you provided.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106823

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

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

[Gabor Marton via Phabricator via cfe-commits]

martong updated this revision to Diff 384122.
martong added a comment.

- Add essay about complexity.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106823

Files:
  
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
  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-iteration-unreachable-code.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
===
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
@@ -0,0 +1,45 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   2>&1 | FileCheck %s
+
+// In this test we check whether the solver's symbol simplification mechanism
+// is capable of reaching a fixpoint. This should be done after TWO iterations.
+
+void clang_analyzer_printState();
+
+void test(int a, int b, int c, int d) {
+  if (a + b + c != d)
+return;
+  if (c + b != 0)
+return;
+  clang_analyzer_printState();
+  // CHECK:  "constraints": [
+  // CHECK-NEXT:   { "symbol": "(((reg_$0) + (reg_$1)) + (reg_$2)) != (reg_$3)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "(reg_$2) + (reg_$1)", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "equivalence_classes": [
+  // CHECK-NEXT:   [ "((reg_$0) + (reg_$1)) + (reg_$2)", "reg_$3" ]
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "disequality_info": null,
+
+  // Simplification starts here.
+  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,
+
+  // Keep the symbols and the constraints! alive.
+  (void)(a * b * c * d);
+  return;
+}
Index: clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
===
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
@@ -0,0 +1,40 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   2>&1 | FileCheck %s
+
+// In this test we check whether the solver's symbol simplification mechanism
+// is capable of reaching a fixpoint. This should be done after one iteration.
+
+void clang_analyzer_printState();
+
+void test(int a, int b, int c) {
+  if (a + b != c)
+return;
+  clang_analyzer_printState();
+  // CHECK:  "constraints": [
+  // CHECK-NEXT:   { "symbol": "((reg_$0) + (reg_$1)) != (reg_$2)", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "equivalence_classes": [
+  // CHECK-NEXT:   [ "(reg_$0) + (reg_$1)", "reg_$2" ]
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "disequality_info": null,
+
+  // Simplification starts here.
+  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-NEXT: "disequality_info": null,
+
+  // Keep the symbols and the constraints! alive.
+  (void)(a * b * c);
+  return;
+}
Index: clang/test/Analysis/symbol-simplification-fixpoint-iteration-unreachable-code.cpp
===
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-fixpoint-iteration-unreachable-code.cpp
@@ -0,0 +1,44 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -verify
+
+// In this test we check whether the solver's symbol simplification mechanism
+// is capable of reaching a fixpoint.
+
+void clang_analyzer_warnIfReached();
+
+void test_contradiction(int a, int b, int c, int d, int x) {
+  if (a + b + c != d)
+return;
+  if (a == d)
+return;
+  if (b + c != 0)
+return;
+  clang_analyzer_warnIfReached(); 

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

[Gabor Marton via Phabricator via cfe-commits]

martong added inline comments.



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1699-1701
+  ProgramStateRef OldState;
+  do {
+OldState = State;

steakhal wrote:
> IMO we should have a `llvm::Statistic` here, tracking the maximum iteration 
> count to reach the fixed point and an average iteration count.
We can't do this once we reach the fixpoint with recursive `assume` calls.



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1732
+  if (!State)
+return false;
+}

steakhal wrote:
> I'd love to see a coverage report of the tests you add with this patch.
Ok, I am going to check the coverage and add the missing cases.



Comment at: clang/test/Analysis/expr-inspection-printState-eq-classes.c:11
 return;
-  if (b != 0)
+  if (a != c)
 return;

steakhal wrote:
> Why do you need to change this?
We don't need it, I removed.



Comment at: 
clang/test/Analysis/symbol-simplification-fixpoint-iteration-unreachable-code.cpp:16
+return;
+  if (c + b != 0)
+return;

steakhal wrote:
> Is it important to have this instead of `b + c`?
No, I changed it to `b+c` as you suggested.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106823

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

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

[Gabor Marton via Phabricator via cfe-commits]

martong updated this revision to Diff 384117.
martong marked 3 inline comments as done.
martong added a comment.

- Reach the fixpoint by recursively calling `State->assume` on the simplified 
symbol.
- Address review nits.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106823

Files:
  
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
  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-iteration-unreachable-code.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
===
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
@@ -0,0 +1,45 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   2>&1 | FileCheck %s
+
+// In this test we check whether the solver's symbol simplification mechanism
+// is capable of reaching a fixpoint. This should be done after TWO iterations.
+
+void clang_analyzer_printState();
+
+void test(int a, int b, int c, int d) {
+  if (a + b + c != d)
+return;
+  if (c + b != 0)
+return;
+  clang_analyzer_printState();
+  // CHECK:  "constraints": [
+  // CHECK-NEXT:   { "symbol": "(((reg_$0) + (reg_$1)) + (reg_$2)) != (reg_$3)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "(reg_$2) + (reg_$1)", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "equivalence_classes": [
+  // CHECK-NEXT:   [ "((reg_$0) + (reg_$1)) + (reg_$2)", "reg_$3" ]
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "disequality_info": null,
+
+  // Simplification starts here.
+  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,
+
+  // Keep the symbols and the constraints! alive.
+  (void)(a * b * c * d);
+  return;
+}
Index: clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
===
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
@@ -0,0 +1,40 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   2>&1 | FileCheck %s
+
+// In this test we check whether the solver's symbol simplification mechanism
+// is capable of reaching a fixpoint. This should be done after one iteration.
+
+void clang_analyzer_printState();
+
+void test(int a, int b, int c) {
+  if (a + b != c)
+return;
+  clang_analyzer_printState();
+  // CHECK:  "constraints": [
+  // CHECK-NEXT:   { "symbol": "((reg_$0) + (reg_$1)) != (reg_$2)", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "equivalence_classes": [
+  // CHECK-NEXT:   [ "(reg_$0) + (reg_$1)", "reg_$2" ]
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "disequality_info": null,
+
+  // Simplification starts here.
+  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-NEXT: "disequality_info": null,
+
+  // Keep the symbols and the constraints! alive.
+  (void)(a * b * c);
+  return;
+}
Index: clang/test/Analysis/symbol-simplification-fixpoint-iteration-unreachable-code.cpp
===
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-fixpoint-iteration-unreachable-code.cpp
@@ -0,0 +1,44 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -verify
+
+// In this test we check whether the solver's symbol simplification mechanism
+// is capable of reaching a fixpoint.
+
+void clang_analyzer_warnIfReached();
+
+void test_contradiction(int a, int b, int c, int d, int x) {
+  if (a 

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

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

steakhal added a comment.

I'm gonna get back to this on Monday.




Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1699-1701
+  ProgramStateRef OldState;
+  do {
+OldState = State;

IMO we should have a `llvm::Statistic` here, tracking the maximum iteration 
count to reach the fixed point and an average iteration count.



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1732
+  if (!State)
+return false;
+}

I'd love to see a coverage report of the tests you add with this patch.



Comment at: clang/test/Analysis/expr-inspection-printState-eq-classes.c:11
 return;
-  if (b != 0)
+  if (a != c)
 return;

Why do you need to change this?



Comment at: 
clang/test/Analysis/symbol-simplification-fixpoint-iteration-unreachable-code.cpp:16
+return;
+  if (c + b != 0)
+return;

Is it important to have this instead of `b + c`?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106823

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

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

[Gabor Marton via Phabricator via cfe-commits]

martong added inline comments.



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2108
+LLVM_NODISCARD ProgramStateRef
+EquivalenceClass::removeMember(ProgramStateRef State, const SymbolRef Old) {
+

Remove `const `



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2123
+  ClsMembers = F.remove(ClsMembers, Old);
+  assert(!ClsMembers.isEmpty() &&
+ "Class should have had at least two members before member removal");

Comment that this is a precondition.



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2156
+  assert(find(State, MemberSym) == find(State, SimplifiedMemberSym));
+  // Remove the old and more complex symbol.
+  State = find(State, MemberSym).removeMember(State, MemberSym);

TODO add Performance and complexity essay here.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106823

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

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

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

@vsavchenko gentle ping


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106823

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

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

[Gabor Marton via Phabricator via cfe-commits]

martong updated this revision to Diff 364373.
martong marked 4 inline comments as done.
martong edited the summary of this revision.
martong added a comment.

- Remove superfluous clang_analyzer_printState
- Assert on isEmpty instead of using getHeight


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106823

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-iteration-unreachable-code.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
===
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
@@ -0,0 +1,45 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   2>&1 | FileCheck %s
+
+// In this test we check whether the solver's symbol simplification mechanism
+// is capable of reaching a fixpoint. This should be done after TWO iterations.
+
+void clang_analyzer_printState();
+
+void test(int a, int b, int c, int d) {
+  if (a + b + c != d)
+return;
+  if (c + b != 0)
+return;
+  clang_analyzer_printState();
+  // CHECK:  "constraints": [
+  // CHECK-NEXT:   { "symbol": "(((reg_$0) + (reg_$1)) + (reg_$2)) != (reg_$3)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "(reg_$2) + (reg_$1)", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "equivalence_classes": [
+  // CHECK-NEXT:   [ "((reg_$0) + (reg_$1)) + (reg_$2)", "reg_$3" ]
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "disequality_info": null,
+
+  // Simplification starts here.
+  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,
+
+  // Keep the symbols and the constraints! alive.
+  (void)(a * b * c * d);
+  return;
+}
Index: clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
===
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
@@ -0,0 +1,40 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   2>&1 | FileCheck %s
+
+// In this test we check whether the solver's symbol simplification mechanism
+// is capable of reaching a fixpoint. This should be done after one iteration.
+
+void clang_analyzer_printState();
+
+void test(int a, int b, int c) {
+  if (a + b != c)
+return;
+  clang_analyzer_printState();
+  // CHECK:  "constraints": [
+  // CHECK-NEXT:   { "symbol": "((reg_$0) + (reg_$1)) != (reg_$2)", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "equivalence_classes": [
+  // CHECK-NEXT:   [ "(reg_$0) + (reg_$1)", "reg_$2" ]
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "disequality_info": null,
+
+  // Simplification starts here.
+  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-NEXT: "disequality_info": null,
+
+  // Keep the symbols and the constraints! alive.
+  (void)(a * b * c);
+  return;
+}
Index: clang/test/Analysis/symbol-simplification-fixpoint-iteration-unreachable-code.cpp
===
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-fixpoint-iteration-unreachable-code.cpp
@@ -0,0 +1,44 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -verify
+
+// In this test we check whether the solver's symbol simplification mechanism
+// is capable of reaching a fixpoint.
+
+void clang_analyzer_warnIfReached();
+
+void test_contradiction(int a, int b, int c, int d, int x) {
+  if (a + b + c != d)
+return;
+  if (a == d)
+return;

[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) != (reg_$2)" ],
+  // CHECK-NEXT: [ "reg_$0", "reg_$2" ]

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) + (reg_$1)) != (reg_$2)`. The first and only member of this class can be simplified with 
`(reg_$0) != (reg_$2)` 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) + (reg_$1)) != (reg_$2)` and `(reg_$0) != (reg_$2)`. And then we remove the old symbol from the class. That results in a 
non-trivial class with one member: `(reg_$0) != (reg_$2)`.



Comment at: 
clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp:36
+  // CHECK-NEXT:  "equivalence_classes": [
+  // CHECK-NEXT:[ "(reg_$0) != (reg_$3)" ],
+  // CHECK-NEXT:[ "reg_$0", "reg_$3" ],

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

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

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

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added a comment.

Looking great!
I have a couple of nit picks and I kind of want to check that it doesn't affect 
the performance on a different set of projects as well.




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");
+

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.



Comment at: 
clang/test/Analysis/symbol-simplification-fixpoint-iteration-unreachable-code.cpp:20
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  clang_analyzer_printState();
+

Do we need to print states in this test?



Comment at: 
clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp:32
+  // CHECK-NEXT:   "equivalence_classes": [
+  // CHECK-NEXT: [ "(reg_$0) != (reg_$2)" ],
+  // CHECK-NEXT: [ "reg_$0", "reg_$2" ]

Same question here



Comment at: 
clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp:36
+  // CHECK-NEXT:  "equivalence_classes": [
+  // CHECK-NEXT:[ "(reg_$0) != (reg_$3)" ],
+  // CHECK-NEXT:[ "reg_$0", "reg_$3" ],

OK, I understand the next two classes.
But how did we produce this one?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106823

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

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

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

Ping. @vsavchenko Could you please take a look?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106823

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

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

[Gabor Marton via Phabricator via cfe-commits]

martong updated this revision to Diff 361793.
martong added a comment.

- Rename test functions


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106823

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-iteration-unreachable-code.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
===
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
@@ -0,0 +1,45 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   2>&1 | FileCheck %s
+
+// In this test we check whether the solver's symbol simplification mechanism
+// is capable of reaching a fixpoint. This should be done after TWO iterations.
+
+void clang_analyzer_printState();
+
+void test(int a, int b, int c, int d) {
+  if (a + b + c != d)
+return;
+  if (c + b != 0)
+return;
+  clang_analyzer_printState();
+  // CHECK:  "constraints": [
+  // CHECK-NEXT:   { "symbol": "(((reg_$0) + (reg_$1)) + (reg_$2)) != (reg_$3)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "(reg_$2) + (reg_$1)", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "equivalence_classes": [
+  // CHECK-NEXT:   [ "((reg_$0) + (reg_$1)) + (reg_$2)", "reg_$3" ]
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "disequality_info": null,
+
+  // Simplification starts here.
+  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,
+
+  // Keep the symbols and the constraints! alive.
+  (void)(a * b * c * d);
+  return;
+}
Index: clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
===
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
@@ -0,0 +1,40 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   2>&1 | FileCheck %s
+
+// In this test we check whether the solver's symbol simplification mechanism
+// is capable of reaching a fixpoint. This should be done after one iteration.
+
+void clang_analyzer_printState();
+
+void test(int a, int b, int c) {
+  if (a + b != c)
+return;
+  clang_analyzer_printState();
+  // CHECK:  "constraints": [
+  // CHECK-NEXT:   { "symbol": "((reg_$0) + (reg_$1)) != (reg_$2)", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "equivalence_classes": [
+  // CHECK-NEXT:   [ "(reg_$0) + (reg_$1)", "reg_$2" ]
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "disequality_info": null,
+
+  // Simplification starts here.
+  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-NEXT: "disequality_info": null,
+
+  // Keep the symbols and the constraints! alive.
+  (void)(a * b * c);
+  return;
+}
Index: clang/test/Analysis/symbol-simplification-fixpoint-iteration-unreachable-code.cpp
===
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-fixpoint-iteration-unreachable-code.cpp
@@ -0,0 +1,47 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -verify
+
+// In this test we check whether the solver's symbol simplification mechanism
+// is capable of reaching a fixpoint.
+
+void clang_analyzer_printState();
+void clang_analyzer_warnIfReached();
+
+void test_contradiction(int a, int b, int c, int d, int x) {
+  if (a + b + c != d)
+return;
+  if (a == d)
+return;
+  if (c + b != 0)
+return;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  

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

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

F18155698: image.png 

For more details please check out this html file:
F18155704: stats.html 


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106823

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

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

[Gabor Marton via Phabricator via cfe-commits]

martong created this revision.
martong added reviewers: vsavchenko, NoQ, steakhal.
Herald added subscribers: manas, ASDenysPetrov, gamesh411, dkrupp, donat.nagy, 
Szelethus, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware, 
xazax.hun, whisperity.
Herald added a reviewer: Szelethus.
martong requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

D103314  introduced symbol simplification 
when a new constant constraint is
added. Currently, we simplify existing equivalence classes by iterating over
all existing members of them and trying to simplify each member symbol with
simplifySVal.

At the end of such a simplification round we may end up introducing a
new constant constraint. Example:

  if (a + b + c != d)
return;
  if (c + b != 0)
return;
  // Simplification starts here.
  if (b != 0)
return;

The `c == 0` constraint is the result of the first simplification iteration.
However, we could do another round of simplification to reach the conclusion
that `a == d`. Generally, we could do as many new iterations until we reach a
fixpoint.

Why should we do this? By reaching a fixpoint in simplification we are capable
of discovering infeasible states at the moment of the introduction of the
**first** constant constraint.
Let's modify the previous example just a bit, and consider what happens without
the fixpoint iteration.

  if (a + b + c != d)
return;
  if (c + b != 0)
return;
  // Adding a new constraint.
  if (a == d)
return;
  // This brings in a contradiction.
  if (b != 0)
return;
  clang_analyzer_warnIfReached(); // This produces a warning.
  // The path is already infeasible...
  if (c == 0) // ...but we realize that only when we evaluate `c == 0`.
return;

What happens currently, without the fixpoint iteration? As the inline comments
suggest, without the fixpoint iteration we are doomed to realize that we are on
an infeasible path only after we are already walking on that. With fixpoint
iteration we can detect that before stepping on that. With fixpoint iteration,
the `clang_analyzer_warnIfReached` does not warn in the above example b/c
during the evaluation of `b == 0` we realize the contradiction. The engine and
the checkers do rely on that either `assume(Cond)` or `assume(!Cond)` should be
feasible. This is in fact assured by the so called expensive checks
(LLVM_ENABLE_EXPENSIVE_CHECKS). The StdLibraryFuncionsChecker is notably one of
the checkers that has a very similar assertion.

Consequently, either we do a fixpoint iteration or we should dump the whole
idea of the symbol simplification.

Before this patch, we simply added the simplified symbol to the equivalence
class. In this patch, after we have added the simplified symbol, we remove the
old (more complex) symbol from the members of the equivalence class
(`ClassMembers`). Removing the old symbol is beneficial because during the next
iteration of the simplification we don't have to consider again the old symbol.

Contrary to how we handle `ClassMembers`, we don't remove the old Sym->Class
relation from the `ClassMap`. This is important for two reasons: The
constraints of the old symbol can still be found via it's equivalence class
that it used to be the member of (1). We can spare one removal and thus one
additional tree in the forest of `ClassMap` (2).

Performance and complexity: Let us assume that in a State we have N non-trivial
equivalence classes and that all constraints and disequality info is related to
non-trivial classes. In the worst case, we can simplify only one symbol of one
class in each iteration. The number of symbols in one class cannot grow b/c we
replace the old symbol with the simplified one. Also, the number of the
equivalence classes can decrease only, b/c the algorithm does a merge operation
optionally. We need N iterations in this case to reach the fixpoint. Thus, the
steps needed to be done in the worst case is proportional to `N*N`. Empirical
results (attached) show that there is some hardly noticeable run-time and peak
memory discrepancy compared to the baseline. In my opinion, these differences
could be the result of measurement error.
This worst case scenario can be extended to that cases when we have trivial
classes in the constraints and in the disequality map are transforming to such
a State where there are only non-trivial classes, b/c the algorithm does merge
operations. A merge operation on two trivial classes results in one non-trivial
class.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D106823

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-iteration-unreachable-code.cpp
  clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp