[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

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

steakhal abandoned this revision.
steakhal added a comment.

I no longer think that we should support Symbol to Symbol comparisons.
It would introduce certain anomalies, like //Why could the CM reason about this 
and that comparisons wile could not in others//.

As of now, it's clear that we can not compare Symbols to Symbols - preventing 
such confusing questions to arise in the future.
If we were to implement Symbol to Symbol comparisons, we should cover a lot 
more cases than this patch could.

So I decided to abandon this patch.


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

https://reviews.llvm.org/D77792

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

[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

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

steakhal created this revision.
steakhal added reviewers: NoQ, baloghadamsoftware, Charusso, Szelethus.
Herald added subscribers: cfe-commits, ASDenysPetrov, martong, dkrupp, 
donat.nagy, mikhail.ramalho, a.sidorin, rnkovacs, szepet, xazax.hun, whisperity.
Herald added a project: clang.

This patch extends the constraint manager to be able to reason about trivial 
sym-sym comparisons.

We all know that `a < b` if the maximum value of `a` is still less than the 
minimum value of `b`.
This reasoning can be applied for the <,<=,>,>= relation operators.
This patch solely implements this functionality.

This patch does not address transitity like:
If `a < b` and `b < c` than `a < c`.

This patch is necessary to be able to express //hidden function preconditions//.
For example, with the `D69726` we could express the connection between the 
extent size of `src` and the size (`n`) parameter of the function.

  #define ANALYZER_ASSERT assert
  
  void my_memcpy(char *dst, char *src, int n) {
ANALYZER_ASSERT(clang_analyzer_getExtent(src) >= n)
ANALYZER_ASSERT(clang_analyzer_getExtent(dst) >= n)

for (int i = 0; i < n; ++i) {
  // The extent of dst would be compared to the index i.
  dst[i] = src[i]; // each memory access in-bound, no-warning
}
  }


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D77792

Files:
  
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  clang/test/Analysis/constraint-manager-sym-sym.c

Index: clang/test/Analysis/constraint-manager-sym-sym.c
===
--- /dev/null
+++ clang/test/Analysis/constraint-manager-sym-sym.c
@@ -0,0 +1,172 @@
+// RUN: %clang_analyze_cc1 -verify -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false %s
+
+
+void clang_analyzer_eval(int);
+
+extern void __assert_fail(__const char *__assertion, __const char *__file,
+  unsigned int __line, __const char *__function)
+__attribute__((__noreturn__));
+#define assert(expr) \
+  ((expr) ? (void)(0) : __assert_fail(#expr, __FILE__, __LINE__, __func__))
+
+
+// Given [a1,a2] and [b1,b2] intervals.
+// Pin the [b1,b2] interval to eg. [5,10]
+// Choose the a1,a2 points from 0,2,5,7,10,12 where a1 < a2.
+// There will be 5+4+3+2+1 cases.
+
+// [0,2] and [5,10]
+void test_range1(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 2);
+  clang_analyzer_eval(l <  r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l >  r); // expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{FALSE}}
+}
+
+// [0,5] and [5,10]
+void test_range2(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 5);
+  clang_analyzer_eval(l <  r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l >  r); // expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,7] and [5,10]
+void test_range3(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 7);
+  clang_analyzer_eval(l <  r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >  r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,10] and [5,10]
+void test_range4(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 10);
+  clang_analyzer_eval(l <  r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >  r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,12] and [5,10]
+void test_range5(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 12);
+  clang_analyzer_eval(l <  r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >  r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+
+// [2,5] and [5,10]
+void test_range6(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 5);
+  clang_analyzer_eval(l <  r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l >  r); // expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,7] and [5,10]
+void test_range7(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 7);
+  clang_analyzer_eval(l <  r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >  r); // expected-warning{{UNKNOWN}}
+  clang

[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

[Kristóf Umann via Phabricator via cfe-commits]

Szelethus added a comment.

You seem to have forgotten `-U` :^)


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D77792



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

[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

I like it, nice work!




Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:774
 
+Optional RangeConstraintManager::tryAssumeSymSymOp(
+ProgramStateRef State, BinaryOperator::Opcode Op, SymbolRef LHSSym,

Is it possible to ever return with `None`? Other `assume` functions usually 
just return with `nullptr` on infeasible state as you do. What would be the 
meaning if `None` is returned, is that another kind of infeasibility?



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:797
+
+  switch (Op) {
+  case BO_LT:

Perhaps this hunk could be greatly simplified if `CompareResult` was actually 
`BinaryOperator::Opcode`.

Maybe (?):
```
if (Res == Op)
  return State;
return InfeasibleState;
```



Comment at: clang/test/Analysis/constraint-manager-sym-sym.c:70
+
+// [2,5] and [5,10]
+void test_range6(int l, int r) {

How is it different than `// [0,5] and [5,10]`?



Comment at: clang/test/Analysis/constraint-manager-sym-sym.c:172
+}
+

I think we could benefit from tests for cases like this: 
```
{[0,1],[5,6]} < {[9,9],[11,42],[44,44]}
```


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D77792



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

[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

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

steakhal updated this revision to Diff 256420.
steakhal marked 4 inline comments as done.
steakhal added a comment.

- add full diff context
- NFC refactored `RangeSet` comparison function
- add tests for compund `RangeSet`s like: `{[0,1],[5,6]} < 
{[9,9],[11,42],[44,44]}`
- NFC clang-format test file


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

https://reviews.llvm.org/D77792

Files:
  
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  clang/test/Analysis/constraint-manager-sym-sym.c

Index: clang/test/Analysis/constraint-manager-sym-sym.c
===
--- /dev/null
+++ clang/test/Analysis/constraint-manager-sym-sym.c
@@ -0,0 +1,197 @@
+// RUN: %clang_analyze_cc1 -verify -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false %s
+
+void clang_analyzer_eval(int);
+
+extern void __assert_fail(__const char *__assertion, __const char *__file,
+  unsigned int __line, __const char *__function)
+__attribute__((__noreturn__));
+#define assert(expr) \
+  ((expr) ? (void)(0) : __assert_fail(#expr, __FILE__, __LINE__, __func__))
+
+// Given [a1,a2] and [b1,b2] intervals.
+// Pin the [b1,b2] interval to eg. [5,10]
+// Choose the a1,a2 points from 0,2,5,7,10,12 where a1 < a2.
+// There will be 5+4+3+2+1 cases.
+
+// [0,2] and [5,10]
+void test_range1(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 2);
+  clang_analyzer_eval(l < r);  // expected-warning{{TRUE}}
+  clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{FALSE}}
+}
+
+// [0,5] and [5,10]
+void test_range2(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 5);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,7] and [5,10]
+void test_range3(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 7);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,10] and [5,10]
+void test_range4(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 10);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,12] and [5,10]
+void test_range5(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 12);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,5] and [5,10]
+void test_range6(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 5);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,7] and [5,10]
+void test_range7(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 7);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,10] and [5,10]
+void test_range8(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 10);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,12] and [5,10]
+void test_range9(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 12);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [5,7] and [5,10]
+void test_range10(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(5 <= l && l <= 7);
+  clang_analyzer_eval(l < r);  // expect

[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

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

steakhal added a comment.

In D77792#1971921 , @Szelethus wrote:

> You seem to have forgotten `-U` :^)


Nice catch!




Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:774
 
+Optional RangeConstraintManager::tryAssumeSymSymOp(
+ProgramStateRef State, BinaryOperator::Opcode Op, SymbolRef LHSSym,

martong wrote:
> Is it possible to ever return with `None`? Other `assume` functions usually 
> just return with `nullptr` on infeasible state as you do. What would be the 
> meaning if `None` is returned, is that another kind of infeasibility?
The rest of the functions there is no `maybe` answer. There is always `yes` or 
`no`, returning the `State` or the `nullptr`.
In our case, we don't know in advance that we know a definitive answer.

Imagine the following:
When the analyzer sees the `a < b` comparison.
It queries whether it `canReasonAbout()`. In our case that would return `true` 
due to my change.
When tries to reason about the given `SymSymExpr` (`a < b`), we don't know if 
the corresponding value ranges of `a` and `b` are disjunct or not, we need to 
check that.
If we can prove that the ranges are disjunct (or just connected: `a: [a1,x]` 
and `b: [x,b2]`) then we know an answer. That can be `true` (`State`) or 
`false` (`nullptr`). Otherwise the result should be `UNKNOWN` (`llvm::None`).



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:797
+
+  switch (Op) {
+  case BO_LT:

martong wrote:
> Perhaps this hunk could be greatly simplified if `CompareResult` was actually 
> `BinaryOperator::Opcode`.
> 
> Maybe (?):
> ```
> if (Res == Op)
>   return State;
> return InfeasibleState;
> ```
Honestly, I had exactly the same thoughts.

I think an `Opcode` is a different thing than a result of a comparison.
Here, we have a partial ordering among `RangeSet`s.
But you can convince me :)

But I agree, it looks clunky, looking forward to a better solution. Any idea?



Comment at: clang/test/Analysis/constraint-manager-sym-sym.c:70
+
+// [2,5] and [5,10]
+void test_range6(int l, int r) {

martong wrote:
> How is it different than `// [0,5] and [5,10]`?
It covers the same. I just wanted a full and clear showcase of the possible 
intervals.
I can be convinced to remove this testcase.



Comment at: clang/test/Analysis/constraint-manager-sym-sym.c:172
+}
+

martong wrote:
> I think we could benefit from tests for cases like this: 
> ```
> {[0,1],[5,6]} < {[9,9],[11,42],[44,44]}
> ```
Really good idea.

I added tests for these. But I'm not really sure what's going on there :D
I'm sure that these test cases are not testing what I meant to test.
//(The exploded graphs are showing that each subrange is assumed for a given 
value (`l` and `r`) on a given path)//

Any idea of how to express the proper value ranges?


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

https://reviews.llvm.org/D77792



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

[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

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

steakhal updated this revision to Diff 256551.
steakhal added a comment.

- rewritten the `RangeSet::compare` function and checked the assumptions on 
WolframAlpha
- moved the `RangeSet::compare` function to a cpp file
- added comments to the `RangeSet::compare` function
- fixed the comment in `RangeConstraintManager::canReasonAbout` function
- introduced the `RangeSet::CompareResult::identical` enum value to be complete
- updated the `RangeConstraintManager::tryAssumeSymSymOp` accoding the 
`identical` CompareResult.
- omited testing the `[2,5] < [5,10]` testcase, since that is covered by `[0,5] 
< [5,10]`


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

https://reviews.llvm.org/D77792

Files:
  
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  clang/test/Analysis/constraint-manager-sym-sym.c

Index: clang/test/Analysis/constraint-manager-sym-sym.c
===
--- /dev/null
+++ clang/test/Analysis/constraint-manager-sym-sym.c
@@ -0,0 +1,189 @@
+// RUN: %clang_analyze_cc1 -verify -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false %s
+
+void clang_analyzer_eval(int);
+
+extern void __assert_fail(__const char *__assertion, __const char *__file,
+  unsigned int __line, __const char *__function)
+__attribute__((__noreturn__));
+#define assert(expr) \
+  ((expr) ? (void)(0) : __assert_fail(#expr, __FILE__, __LINE__, __func__))
+
+// Given [a1,a2] and [b1,b2] intervals.
+// Pin the [b1,b2] interval to eg. [5,10]
+// Choose the a1,a2 points from 0,2,5,7,10,12 where a1 < a2.
+// There will be 5+4+3+2+1 cases.
+
+// [0,2] and [5,10]
+void test_range1(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 2);
+  clang_analyzer_eval(l < r);  // expected-warning{{TRUE}}
+  clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{FALSE}}
+}
+
+// [0,5] and [5,10]
+void test_range2(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 5);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,7] and [5,10]
+void test_range3(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 7);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,10] and [5,10]
+void test_range4(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 10);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,12] and [5,10]
+void test_range5(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 12);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,5] and [5,10] omitted because it is the same as the '[0,5] and [5,10]'
+
+// [2,7] and [5,10]
+void test_range7(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 7);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,10] and [5,10]
+void test_range8(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 10);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,12] and [5,10]
+void test_range9(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 12);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [5,7] and [5,10]
+void test_range10(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(5 <= l && l <= 7);
+  clang_analyz

[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov added a comment.

@steakhal 
What about unsigneds? Does it work for unsigned values as well?


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

https://reviews.llvm.org/D77792



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

[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added inline comments.



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:814
 
+Optional RangeConstraintManager::tryAssumeSymSymOp(
+ProgramStateRef State, BinaryOperator::Opcode Op, SymbolRef LHSSym,

I believe you don't need to return an optional here. The method simply 
acknowledges any assumptions it could make in the existing state and returns 
the updated state. Therefore, if it wasn't able to record any assumptions, it 
returns the existing state. Because the only reasonable behavior the caller 
could implement when the current implementation returns `None` is to roll back 
to the existing state anyway.



Comment at: clang/test/Analysis/constraint-manager-sym-sym.c:182
+void test_range18(int l, int r) {
+  assert((9 <= r && r <= 9) || (11 <= r && r <= 42) || (44 <= r && r <= 44));
+  assert((0 <= l && l <= 1) || (20 <= l && l <= 20));

You can also explicitly create a single path with disconnected ranges (as 
opposed to like 3 different paths on each of which the range is a single 
segment) like this:
```lang=c++
assert(r >= 9 && r <= 44 && r != 10 && r != 43);
```


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

https://reviews.llvm.org/D77792



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

[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov added inline comments.



Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h:103-110
+  enum class CompareResult {
+unknown,
+identical,
+less,
+less_equal,
+greater,
+greater_equal

Can we use `Optional` instead, to reduce similar enums? Or 
you want to separate the meaning in a such way?



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:30-33
+  const int LMaxRMin =
+  llvm::APSInt::compareValues(getMaxValue(), other.getMinValue());
+  const int LMinRMax =
+  llvm::APSInt::compareValues(getMinValue(), other.getMaxValue());

As you use here `getMaxValue` twice which is not O(1), it'd better to use a 
buffer variable.



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:106-113
+const llvm::APSInt &RangeSet::getMaxValue() const {
+  assert(!isEmpty());
+  auto last = ranges.begin();
+  for (auto it = std::next(ranges.begin()); it != ranges.end(); ++it)
+last = it;
+  return last->To();
+}

Can we improve `llvm::ImmutableSet` this to make `getMaxValue` complexity O(1)?



Comment at: clang/test/Analysis/constraint-manager-sym-sym.c:181
+// {[0,1],[20,20]} and {[9,9],[11,42],[44,44]}
+void test_range18(int l, int r) {
+  assert((9 <= r && r <= 9) || (11 <= r && r <= 42) || (44 <= r && r <= 44));

Could you add some tests for `unsigned, unsigned` and `signed, unsigned`?


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

https://reviews.llvm.org/D77792



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

[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

[Balogh , Ádám via Phabricator via cfe-commits]

baloghadamsoftware commandeered this revision.
baloghadamsoftware edited reviewers, added: steakhal; removed: 
baloghadamsoftware.
baloghadamsoftware added a comment.
Herald added a subscriber: gamesh411.

We found use cases which can be solved using this improvement. That is why I 
commandeer this patch now.


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

https://reviews.llvm.org/D77792

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

[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

[Balogh , Ádám via Phabricator via cfe-commits]

baloghadamsoftware updated this revision to Diff 292755.
baloghadamsoftware added a comment.

Crash fixed and new tests added.


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

https://reviews.llvm.org/D77792

Files:
  
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  clang/test/Analysis/constraint-manager-sym-sym.c

Index: clang/test/Analysis/constraint-manager-sym-sym.c
===
--- /dev/null
+++ clang/test/Analysis/constraint-manager-sym-sym.c
@@ -0,0 +1,206 @@
+// RUN: %clang_analyze_cc1 -verify -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false %s
+
+void clang_analyzer_eval(int);
+
+extern void __assert_fail(__const char *__assertion, __const char *__file,
+  unsigned int __line, __const char *__function)
+__attribute__((__noreturn__));
+#define assert(expr) \
+  ((expr) ? (void)(0) : __assert_fail(#expr, __FILE__, __LINE__, __func__))
+
+// Given [a1,a2] and [b1,b2] intervals.
+// Pin the [b1,b2] interval to eg. [5,10]
+// Choose the a1,a2 points from 0,2,5,7,10,12 where a1 < a2.
+// There will be 5+4+3+2+1 cases.
+
+// [0,2] and [5,10]
+void test_range1(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 2);
+  clang_analyzer_eval(l < r);  // expected-warning{{TRUE}}
+  clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{FALSE}}
+}
+
+// [0,5] and [5,10]
+void test_range2(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 5);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,7] and [5,10]
+void test_range3(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 7);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,10] and [5,10]
+void test_range4(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 10);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,12] and [5,10]
+void test_range5(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 12);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,5] and [5,10] omitted because it is the same as the '[0,5] and [5,10]'
+
+// [2,7] and [5,10]
+void test_range7(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 7);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,10] and [5,10]
+void test_range8(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 10);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,12] and [5,10]
+void test_range9(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 12);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [5,7] and [5,10]
+void test_range10(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(5 <= l && l <= 7);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [5,10] and [5,10]
+void test_range11(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(5 <= l && l <= 10);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  

[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

[Balogh , Ádám via Phabricator via cfe-commits]

baloghadamsoftware added inline comments.



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:814
 
+Optional RangeConstraintManager::tryAssumeSymSymOp(
+ProgramStateRef State, BinaryOperator::Opcode Op, SymbolRef LHSSym,

NoQ wrote:
> I believe you don't need to return an optional here. The method simply 
> acknowledges any assumptions it could make in the existing state and returns 
> the updated state. Therefore, if it wasn't able to record any assumptions, it 
> returns the existing state. Because the only reasonable behavior the caller 
> could implement when the current implementation returns `None` is to roll 
> back to the existing state anyway.
Actually, `tryAssumeSymSymOp()` does not assume anything and therefore it does 
not return a new state. What it actually returns is a ternary logical value: 
the assumption is either valid, invalid or we cannot reason about it. Maybe 
Optional would be better here and we should also chose a less misleading 
name, because it does not "try to assume" anything, but tries to reason about 
the existing assumption.


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

https://reviews.llvm.org/D77792

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

[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

[Balogh , Ádám via Phabricator via cfe-commits]

baloghadamsoftware added inline comments.



Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h:103-110
+  enum class CompareResult {
+unknown,
+identical,
+less,
+less_equal,
+greater,
+greater_equal

ASDenysPetrov wrote:
> Can we use `Optional` instead, to reduce similar enums? 
> Or you want to separate the meaning in a such way?
Good question. @NoQ?



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:30-33
+  const int LMaxRMin =
+  llvm::APSInt::compareValues(getMaxValue(), other.getMinValue());
+  const int LMinRMax =
+  llvm::APSInt::compareValues(getMinValue(), other.getMaxValue());

ASDenysPetrov wrote:
> As you use here `getMaxValue` twice which is not O(1), it'd better to use a 
> buffer variable.
`getMaxValue()` for the current and `other.getMaxValue()` are different.



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:106-113
+const llvm::APSInt &RangeSet::getMaxValue() const {
+  assert(!isEmpty());
+  auto last = ranges.begin();
+  for (auto it = std::next(ranges.begin()); it != ranges.end(); ++it)
+last = it;
+  return last->To();
+}

ASDenysPetrov wrote:
> Can we improve `llvm::ImmutableSet` this to make `getMaxValue` complexity 
> O(1)?
`llvm::ImmutableSet` seems to me a //heap//-like structure, a tree optimized 
for minimum-search: the mininum is in the root of the tree. Maximum is linear.



Comment at: clang/test/Analysis/constraint-manager-sym-sym.c:181
+// {[0,1],[20,20]} and {[9,9],[11,42],[44,44]}
+void test_range18(int l, int r) {
+  assert((9 <= r && r <= 9) || (11 <= r && r <= 42) || (44 <= r && r <= 44));

ASDenysPetrov wrote:
> Could you add some tests for `unsigned, unsigned` and `signed, unsigned`?
I will do it.


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

https://reviews.llvm.org/D77792

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

[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

[Balogh , Ádám via Phabricator via cfe-commits]

baloghadamsoftware updated this revision to Diff 293111.
baloghadamsoftware added a comment.

Tests updated: some execution paths merged by refactoring assertions.


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

https://reviews.llvm.org/D77792

Files:
  
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  clang/test/Analysis/constraint-manager-sym-sym.c

Index: clang/test/Analysis/constraint-manager-sym-sym.c
===
--- /dev/null
+++ clang/test/Analysis/constraint-manager-sym-sym.c
@@ -0,0 +1,205 @@
+// RUN: %clang_analyze_cc1 -verify -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false %s
+
+void clang_analyzer_eval(int);
+
+extern void __assert_fail(__const char *__assertion, __const char *__file,
+  unsigned int __line, __const char *__function)
+__attribute__((__noreturn__));
+#define assert(expr) \
+  ((expr) ? (void)(0) : __assert_fail(#expr, __FILE__, __LINE__, __func__))
+
+// Given [a1,a2] and [b1,b2] intervals.
+// Pin the [b1,b2] interval to eg. [5,10]
+// Choose the a1,a2 points from 0,2,5,7,10,12 where a1 < a2.
+// There will be 5+4+3+2+1 cases.
+
+// [0,2] and [5,10]
+void test_range1(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 2);
+  clang_analyzer_eval(l < r);  // expected-warning{{TRUE}}
+  clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{FALSE}}
+}
+
+// [0,5] and [5,10]
+void test_range2(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 5);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,7] and [5,10]
+void test_range3(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 7);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,10] and [5,10]
+void test_range4(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 10);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,12] and [5,10]
+void test_range5(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 12);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,5] and [5,10] omitted because it is the same as the '[0,5] and [5,10]'
+
+// [2,7] and [5,10]
+void test_range7(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 7);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,10] and [5,10]
+void test_range8(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 10);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,12] and [5,10]
+void test_range9(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 12);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [5,7] and [5,10]
+void test_range10(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(5 <= l && l <= 7);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [5,10] and [5,10]
+void test_range11(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(5 <= l && l <= 10);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r

[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

[Gabor Marton via Phabricator via cfe-commits]

martong added a reviewer: vsavchenko.
martong added a comment.

Adding Valeriy as a reviewer. He's been working with the solver recently, so 
his insights might be really useful here.


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

https://reviews.llvm.org/D77792

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

[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added a comment.

Hi @baloghadamsoftware

Great job!  I also wanted to support more operations for range-based logic.

However, I don't think that this is the right place to make this kind of 
assumptions.  A couple months ago, I added the `SymbolicRangeInferrer` 
component to aggregate all of the reasoning we have about range constraints and 
I strongly believe that the logic from this patch should be integrated in that 
component.


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

https://reviews.llvm.org/D77792

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

[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added inline comments.



Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h:103-110
+  enum class CompareResult {
+unknown,
+identical,
+less,
+less_equal,
+greater,
+greater_equal

baloghadamsoftware wrote:
> ASDenysPetrov wrote:
> > Can we use `Optional` instead, to reduce similar enums? 
> > Or you want to separate the meaning in a such way?
> Good question. @NoQ?
The meaning is obviously completely different even when the names actually 
match. `BO_LT` is not a "result", it's the operation itself. It gets even worse 
for other opcodes (what kind of comparison result is `BO_PtrMemI`???).

The idea to re-use the enum is noble but we definitely need to find some other 
enum.



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:814
 
+Optional RangeConstraintManager::tryAssumeSymSymOp(
+ProgramStateRef State, BinaryOperator::Opcode Op, SymbolRef LHSSym,

baloghadamsoftware wrote:
> NoQ wrote:
> > I believe you don't need to return an optional here. The method simply 
> > acknowledges any assumptions it could make in the existing state and 
> > returns the updated state. Therefore, if it wasn't able to record any 
> > assumptions, it returns the existing state. Because the only reasonable 
> > behavior the caller could implement when the current implementation returns 
> > `None` is to roll back to the existing state anyway.
> Actually, `tryAssumeSymSymOp()` does not assume anything and therefore it 
> does not return a new state. What it actually returns is a ternary logical 
> value: the assumption is either valid, invalid or we cannot reason about it. 
> Maybe Optional would be better here and we should also chose a less 
> misleading name, because it does not "try to assume" anything, but tries to 
> reason about the existing assumption.
I dislike this design because it turns the code into a spaghetti in which every 
facility in the constraint manager has to be aware of any other facility in the 
constraint manager and agree on who's responsible for what. It's too easy to 
miss something and missing something isn't as bad as doing double work.

Like, should different facilities in the constraint manager try to record as 
*much* information in the program state ("fat constraints") as possible or as 
*little* as possible ("thin constraints")? Eg., in this example, if we know 
that the range for `$x` is strictly below the range for `$y`, should we also 
add the opaque constraint `$x < $y` to the program state, or should we instead 
teach every facility to infer that `$x < $y` by looking at their ranges?

I feel we should go with fat constraints.

1. Con: They're fat. They eat more memory, cause more immutable tree 
rebalances, etc.
2. Con: It's easy to accidentally make two similar states look different. Eg., 
`{ $x: [1, 2], $y: [3, 4] }` and `{ $x : [1, 2], $y: [3, 4], $x < $y: true }` 
are the same state but they won't be deduplicated and if they appear on 
different paths at the same program point these paths won't get merged.
3. Pro: They minimize the amount of false positives by giving every facility in 
the constraint manager as much data as possible to conclude that the state is 
infeasible.
4. Pro: As i said above, they're easier to implement and to get right. In case 
of thin constraints, every facility has to actively let other facilites know 
that they don't need to handle the assumption anymore because this facility has 
"consumed" it. In our example it means returning an `Optional` 
which would be empty if the constraint wasn't consumed and needs to be handled 
by another facility (namely, `assumeSymUnsupported`). In case of fat 
constraints you simply add your information and you don't care if other 
facilities ever read it or not.

Con 1. should be dismissed as a premature optimization: we can always add some 
thinness to fat constraints if we have a proof that their fatness is an actual 
problem. Con 2. is a real issue but it's a fairly minor issue; path merges are 
fairly rare anyway; mergeability is a nice goal to pursue but not at the cost 
of having false positives. So i think pros outweight the cons here.


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

https://reviews.llvm.org/D77792

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

Re: [PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

[Denis Petrov via cfe-commits]

Welcome to my another idea to improve RangeConstraintManager? 
https://reviews.llvm.org/D78933



Denys Petrov
Senior С++ Developer | Kharkiv, Ukraine


От: Balazs Benics via Phabricator 
Отправлено: 10 апреля 2020 г. 15:53
Кому: benicsbal...@gmail.com; noqnoq...@gmail.com; adam.bal...@ericsson.com; 
dabis.csab...@gmail.com; dkszelet...@gmail.com
Копия: richard.sza...@ericsson.com; xazax@gmail.com; 
peterszecs...@gmail.com; rekanikol...@gmail.com; a.sido...@samsung.com; 
mikhail.rama...@gmail.com; donat.n...@ericsson.com; daniel.kr...@ericsson.com; 
martongab...@gmail.com; Denis Petrov; cfe-commits@lists.llvm.org; 
mlek...@skidmore.edu; blitzrak...@gmail.com; shen...@google.com; 
1.in...@gmail.com
Тема: [PATCH] D77792: [analyzer] Extend constraint manager to be able to 
compare simple SymSymExprs

CAUTION: This email originated from outside of the organization. Do not click 
links or open attachments unless you recognize the sender and know the content 
is safe.  If you suspect potential phishing or spam email, report it to 
reports...@accesssoftek.com

steakhal updated this revision to Diff 256551.
steakhal added a comment.

- rewritten the `RangeSet::compare` function and checked the assumptions on 
WolframAlpha
- moved the `RangeSet::compare` function to a cpp file
- added comments to the `RangeSet::compare` function
- fixed the comment in `RangeConstraintManager::canReasonAbout` function
- introduced the `RangeSet::CompareResult::identical` enum value to be complete
- updated the `RangeConstraintManager::tryAssumeSymSymOp` accoding the 
`identical` CompareResult.
- omited testing the `[2,5] < [5,10]` testcase, since that is covered by `[0,5] 
< [5,10]`


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

https://reviews.llvm.org/D77792

Files:
  
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  clang/test/Analysis/constraint-manager-sym-sym.c

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