[PATCH] D113753: [Analyzer][Core] Better simplification in SimpleSValBuilder::evalBinOpNN

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

steakhal added inline comments.



Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:372
   QualType resultTy)  {
   NonLoc InputLHS = lhs;
   NonLoc InputRHS = rhs;

martong wrote:
> steakhal wrote:
> > @martong, you simplified the operands, but you overwrite only the lhs and 
> > rhs. Shouldnt you overwite these as well?
> > What is the purpose of these variables, do you know?
> > @martong, you simplified the operands, but you overwrite only the lhs and 
> > rhs. Shouldnt you overwite these as well?
> > What is the purpose of these variables, do you know?
> 
> They are used exclusively to create `SymExpr`s with `makeSymExprValNN` when 
> both lhs and rhs are symbols. If we were to simplify the `Input` variables 
> then it might happen that we end up with a non symbol (i.e. a concrete int) 
> and then `makeSymExprValNN` would fail miserably (would assert I guess). 
I see. Although, it still seems suboptimal.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D113753

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

[PATCH] D113753: [Analyzer][Core] Better simplification in SimpleSValBuilder::evalBinOpNN

[Gabor Marton via Phabricator via cfe-commits]

martong added inline comments.



Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:372
   QualType resultTy)  {
   NonLoc InputLHS = lhs;
   NonLoc InputRHS = rhs;

steakhal wrote:
> @martong, you simplified the operands, but you overwrite only the lhs and 
> rhs. Shouldnt you overwite these as well?
> What is the purpose of these variables, do you know?
> @martong, you simplified the operands, but you overwrite only the lhs and 
> rhs. Shouldnt you overwite these as well?
> What is the purpose of these variables, do you know?

They are used exclusively to create `SymExpr`s with `makeSymExprValNN` when 
both lhs and rhs are symbols. If we were to simplify the `Input` variables then 
it might happen that we end up with a non symbol (i.e. a concrete int) and then 
`makeSymExprValNN` would fail miserably (would assert I guess). 


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D113753

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

[PATCH] D113753: [Analyzer][Core] Better simplification in SimpleSValBuilder::evalBinOpNN

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

steakhal added inline comments.



Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:372
   QualType resultTy)  {
   NonLoc InputLHS = lhs;
   NonLoc InputRHS = rhs;

@martong, you simplified the operands, but you overwrite only the lhs and rhs. 
Shouldnt you overwite these as well?
What is the purpose of these variables, do you know?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D113753

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

[PATCH] D113753: [Analyzer][Core] Better simplification in SimpleSValBuilder::evalBinOpNN

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

Here is a smaller reproducer:

  void bar(short k) {
++k; // k1 = k0 + 1
assert(k == 1);  // k1 == 1 --> k0 == 0
(long)k << 16;   // k0 + 1 <<  16
  }

And the explanation is the following. With this patch, when the analyzer 
evaluates the `(long)k << 16` expression then it can properly deduce the value 
of `k` being `1`. However, it was not possible in the baseline. Since we do not 
model neither promotion nor explicit casts we get the false positive report. 
This issue highlights the importance of the patch stack to implement the 
modeling of casts (starting with https://reviews.llvm.org/D99797).


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D113753

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

[PATCH] D113753: [Analyzer][Core] Better simplification in SimpleSValBuilder::evalBinOpNN

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

steakhal added a comment.

In D113753#3156270 , @bjope wrote:

> This seem to cause some weird results.
>
> Given this input:
>
>   bar(short k) {
> k++;
> for (short f = 0; f < k; f++)
>   ;
> (long)k << 16;
>   }
>
> we get
>
>   > clang  --analyze --target=x86_64 'bbi-63538.c'
>   bbi-63538.c:5:11: warning: The result of the left shift is undefined due to 
> shifting '1' by '16', which is unrepresentable in the unsigned version of the 
> return type 'long' [core.UndefinedBinaryOperatorResult]
> (long)k << 16;
> ~~~ ^
>   bbi-63538.c:5:11: warning: The result of the left shift is undefined due to 
> shifting '2' by '16', which is unrepresentable in the unsigned version of the 
> return type 'long' [core.UndefinedBinaryOperatorResult]
> (long)k << 16;
> ~~~ ^
>   bbi-63538.c:5:11: warning: The result of the left shift is undefined due to 
> shifting '3' by '16', which is unrepresentable in the unsigned version of the 
> return type 'long' [core.UndefinedBinaryOperatorResult]
> (long)k << 16;
> ~~~ ^
>   3 warnings generated.

Good catch @bjope !
Here is an example without the loop: https://godbolt.org/z/z3rqMz4bs
We'll have a closer look.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D113753

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

[PATCH] D113753: [Analyzer][Core] Better simplification in SimpleSValBuilder::evalBinOpNN

[Bjorn Pettersson via Phabricator via cfe-commits]

bjope added a comment.

This seem to cause some weird results.

Given this input:

  bar(short k) {
k++;
for (short f = 0; f < k; f++)
  ;
(long)k << 16;
  }

we get

  > clang  --analyze --target=x86_64 'bbi-63538.c'
  bbi-63538.c:5:11: warning: The result of the left shift is undefined due to 
shifting '1' by '16', which is unrepresentable in the unsigned version of the 
return type 'long' [core.UndefinedBinaryOperatorResult]
(long)k << 16;
~~~ ^
  bbi-63538.c:5:11: warning: The result of the left shift is undefined due to 
shifting '2' by '16', which is unrepresentable in the unsigned version of the 
return type 'long' [core.UndefinedBinaryOperatorResult]
(long)k << 16;
~~~ ^
  bbi-63538.c:5:11: warning: The result of the left shift is undefined due to 
shifting '3' by '16', which is unrepresentable in the unsigned version of the 
return type 'long' [core.UndefinedBinaryOperatorResult]
(long)k << 16;
~~~ ^
  3 warnings generated.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D113753

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

[PATCH] D113753: [Analyzer][Core] Better simplification in SimpleSValBuilder::evalBinOpNN

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

I'm attaching the coverage of the new test file for the related change:

  375 :   // Constraints may have changed since the creation of a 
bound SVal. Check if
  376 :   // the values can be simplified based on those new 
constraints.
  377  12 :   SVal simplifiedLhs = simplifySVal(state, lhs);
  378  12 :   SVal simplifiedRhs = simplifySVal(state, rhs);
  379  12 :   if (auto simplifiedLhsAsNonLoc = 
simplifiedLhs.getAs())
  380  12 : lhs = *simplifiedLhsAsNonLoc;
  381  12 :   if (auto simplifiedRhsAsNonLoc = 
simplifiedRhs.getAs())
  382  12 : rhs = *simplifiedRhsAsNonLoc;
  383 :


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D113753

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

[PATCH] D113753: [Analyzer][Core] Better simplification in SimpleSValBuilder::evalBinOpNN

[Gabor Marton via Phabricator via cfe-commits]

This revision was landed with ongoing or failed builds.
This revision was automatically updated to reflect the committed changes.
Closed by commit rG12887a202404: [Analyzer][Core] Better simplification in 
SimpleSValBuilder::evalBinOpNN (authored by martong).

Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D113753

Files:
  clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  clang/test/Analysis/svalbuilder-simplify-in-evalbinop.cpp


Index: clang/test/Analysis/svalbuilder-simplify-in-evalbinop.cpp
===
--- /dev/null
+++ clang/test/Analysis/svalbuilder-simplify-in-evalbinop.cpp
@@ -0,0 +1,30 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -verify
+
+// Here we test whether the SValBuilder is capable to simplify existing
+// SVals based on a newly added constraints when evaluating a BinOp.
+
+void clang_analyzer_eval(bool);
+
+void test_evalBinOp_simplifies_lhs(int y) {
+  int x = y / 77;
+  if (y != 77)
+return;
+
+  // Below `x` is the LHS being simplified.
+  clang_analyzer_eval(x == 1); // expected-warning{{TRUE}}
+  (void)(x * y);
+}
+
+void test_evalBinOp_simplifies_rhs(int y) {
+  int x = y / 77;
+  if (y != 77)
+return;
+
+  // Below `x` is the RHS being simplified.
+  clang_analyzer_eval(1 == x); // expected-warning{{TRUE}}
+  (void)(x * y);
+}
Index: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
===
--- clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -372,6 +372,15 @@
   NonLoc InputLHS = lhs;
   NonLoc InputRHS = rhs;
 
+  // Constraints may have changed since the creation of a bound SVal. Check if
+  // the values can be simplified based on those new constraints.
+  SVal simplifiedLhs = simplifySVal(state, lhs);
+  SVal simplifiedRhs = simplifySVal(state, rhs);
+  if (auto simplifiedLhsAsNonLoc = simplifiedLhs.getAs())
+lhs = *simplifiedLhsAsNonLoc;
+  if (auto simplifiedRhsAsNonLoc = simplifiedRhs.getAs())
+rhs = *simplifiedRhsAsNonLoc;
+
   // Handle trivial case where left-side and right-side are the same.
   if (lhs == rhs)
 switch (op) {
@@ -619,16 +628,6 @@
 }
   }
 
-  // Does the symbolic expression simplify to a constant?
-  // If so, "fold" the constant by setting 'lhs' to a ConcreteInt
-  // and try again.
-  SVal simplifiedLhs = simplifySVal(state, lhs);
-  if (simplifiedLhs != lhs)
-if (auto simplifiedLhsAsNonLoc = simplifiedLhs.getAs()) {
-  lhs = *simplifiedLhsAsNonLoc;
-  continue;
-}
-
   // Is the RHS a constant?
   if (const llvm::APSInt *RHSValue = getKnownValue(state, rhs))
 return MakeSymIntVal(Sym, op, *RHSValue, resultTy);


Index: clang/test/Analysis/svalbuilder-simplify-in-evalbinop.cpp
===
--- /dev/null
+++ clang/test/Analysis/svalbuilder-simplify-in-evalbinop.cpp
@@ -0,0 +1,30 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -verify
+
+// Here we test whether the SValBuilder is capable to simplify existing
+// SVals based on a newly added constraints when evaluating a BinOp.
+
+void clang_analyzer_eval(bool);
+
+void test_evalBinOp_simplifies_lhs(int y) {
+  int x = y / 77;
+  if (y != 77)
+return;
+
+  // Below `x` is the LHS being simplified.
+  clang_analyzer_eval(x == 1); // expected-warning{{TRUE}}
+  (void)(x * y);
+}
+
+void test_evalBinOp_simplifies_rhs(int y) {
+  int x = y / 77;
+  if (y != 77)
+return;
+
+  // Below `x` is the RHS being simplified.
+  clang_analyzer_eval(1 == x); // expected-warning{{TRUE}}
+  (void)(x * y);
+}
Index: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
===
--- clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -372,6 +372,15 @@
   NonLoc InputLHS = lhs;
   NonLoc InputRHS = rhs;
 
+  // Constraints may have changed since the creation of a bound SVal. Check if
+  // the values can be simplified based on those new constraints.
+  SVal simplifiedLhs = simplifySVal(state, lhs);
+  SVal simplifiedRhs = simplifySVal(state, rhs);
+  if (auto simplifiedLhsAsNonLoc = simplifiedLhs.getAs())
+lhs = *simplifiedLhsAsNonLoc;
+  if (auto simplifiedRhsAsNonLoc = simplifiedRhs.getAs())
+rhs = *simplifiedRhsAsNonLoc;
+
   // Handle trivial case where left-side and right-side are the same.
   if (lhs == rhs)
 switch (op) {
@@ -619,16 +628,6 @@
 }
   }
 
-  // Does the symbolic 

[PATCH] D113753: [Analyzer][Core] Better simplification in SimpleSValBuilder::evalBinOpNN

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

Awesome!


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D113753

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

[PATCH] D113753: [Analyzer][Core] Better simplification in SimpleSValBuilder::evalBinOpNN

[Gabor Marton via Phabricator via cfe-commits]

martong updated this revision to Diff 389186.
martong marked an inline comment as done.
martong added a comment.

- Add new test case


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D113753

Files:
  clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  clang/test/Analysis/svalbuilder-simplify-in-evalbinop.cpp


Index: clang/test/Analysis/svalbuilder-simplify-in-evalbinop.cpp
===
--- /dev/null
+++ clang/test/Analysis/svalbuilder-simplify-in-evalbinop.cpp
@@ -0,0 +1,30 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -verify
+
+// Here we test whether the SValBuilder is capable to simplify existing
+// SVals based on a newly added constraints when evaluating a BinOp.
+
+void clang_analyzer_eval(bool);
+
+void test_evalBinOp_simplifies_lhs(int y) {
+  int x = y / 77;
+  if (y != 77)
+return;
+
+  // Below `x` is the LHS being simplified.
+  clang_analyzer_eval(x == 1); // expected-warning{{TRUE}}
+  (void)(x * y);
+}
+
+void test_evalBinOp_simplifies_rhs(int y) {
+  int x = y / 77;
+  if (y != 77)
+return;
+
+  // Below `x` is the RHS being simplified.
+  clang_analyzer_eval(1 == x); // expected-warning{{TRUE}}
+  (void)(x * y);
+}
Index: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
===
--- clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -372,6 +372,15 @@
   NonLoc InputLHS = lhs;
   NonLoc InputRHS = rhs;
 
+  // Constraints may have changed since the creation of a bound SVal. Check if
+  // the values can be simplified based on those new constraints.
+  SVal simplifiedLhs = simplifySVal(state, lhs);
+  SVal simplifiedRhs = simplifySVal(state, rhs);
+  if (auto simplifiedLhsAsNonLoc = simplifiedLhs.getAs())
+lhs = *simplifiedLhsAsNonLoc;
+  if (auto simplifiedRhsAsNonLoc = simplifiedRhs.getAs())
+rhs = *simplifiedRhsAsNonLoc;
+
   // Handle trivial case where left-side and right-side are the same.
   if (lhs == rhs)
 switch (op) {
@@ -619,16 +628,6 @@
 }
   }
 
-  // Does the symbolic expression simplify to a constant?
-  // If so, "fold" the constant by setting 'lhs' to a ConcreteInt
-  // and try again.
-  SVal simplifiedLhs = simplifySVal(state, lhs);
-  if (simplifiedLhs != lhs)
-if (auto simplifiedLhsAsNonLoc = simplifiedLhs.getAs()) {
-  lhs = *simplifiedLhsAsNonLoc;
-  continue;
-}
-
   // Is the RHS a constant?
   if (const llvm::APSInt *RHSValue = getKnownValue(state, rhs))
 return MakeSymIntVal(Sym, op, *RHSValue, resultTy);


Index: clang/test/Analysis/svalbuilder-simplify-in-evalbinop.cpp
===
--- /dev/null
+++ clang/test/Analysis/svalbuilder-simplify-in-evalbinop.cpp
@@ -0,0 +1,30 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -verify
+
+// Here we test whether the SValBuilder is capable to simplify existing
+// SVals based on a newly added constraints when evaluating a BinOp.
+
+void clang_analyzer_eval(bool);
+
+void test_evalBinOp_simplifies_lhs(int y) {
+  int x = y / 77;
+  if (y != 77)
+return;
+
+  // Below `x` is the LHS being simplified.
+  clang_analyzer_eval(x == 1); // expected-warning{{TRUE}}
+  (void)(x * y);
+}
+
+void test_evalBinOp_simplifies_rhs(int y) {
+  int x = y / 77;
+  if (y != 77)
+return;
+
+  // Below `x` is the RHS being simplified.
+  clang_analyzer_eval(1 == x); // expected-warning{{TRUE}}
+  (void)(x * y);
+}
Index: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
===
--- clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -372,6 +372,15 @@
   NonLoc InputLHS = lhs;
   NonLoc InputRHS = rhs;
 
+  // Constraints may have changed since the creation of a bound SVal. Check if
+  // the values can be simplified based on those new constraints.
+  SVal simplifiedLhs = simplifySVal(state, lhs);
+  SVal simplifiedRhs = simplifySVal(state, rhs);
+  if (auto simplifiedLhsAsNonLoc = simplifiedLhs.getAs())
+lhs = *simplifiedLhsAsNonLoc;
+  if (auto simplifiedRhsAsNonLoc = simplifiedRhs.getAs())
+rhs = *simplifiedRhsAsNonLoc;
+
   // Handle trivial case where left-side and right-side are the same.
   if (lhs == rhs)
 switch (op) {
@@ -619,16 +628,6 @@
 }
   }
 
-  // Does the symbolic expression simplify to a constant?
-  // If so, "fold" the constant by setting 'lhs' to a ConcreteInt
-  // and try 

[PATCH] D113753: [Analyzer][Core] Better simplification in SimpleSValBuilder::evalBinOpNN

[Gabor Marton via Phabricator via cfe-commits]

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

I'm attaching the coverage of the new test file for the related change:

  375 :   // Constraints may have changed since the creation of a 
bound SVal. Check if
  376 :   // the values can be simplified based on those new 
constraints.
  377  12 :   SVal simplifiedLhs = simplifySVal(state, lhs);
  378  12 :   SVal simplifiedRhs = simplifySVal(state, rhs);
  379  12 :   if (auto simplifiedLhsAsNonLoc = 
simplifiedLhs.getAs())
  380  12 : lhs = *simplifiedLhsAsNonLoc;
  381  12 :   if (auto simplifiedRhsAsNonLoc = 
simplifiedRhs.getAs())
  382  12 : rhs = *simplifiedRhsAsNonLoc;
  383 :




Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:378
+  SVal simplifiedLhs = simplifySVal(state, lhs);
+  SVal simplifiedRhs = simplifySVal(state, rhs);
+  if (auto simplifiedLhsAsNonLoc = simplifiedLhs.getAs())

steakhal wrote:
> It seems like you simplify the `rhs` as well. Could we have a test for that?
Ok, I've added a new test case and reworked the existing a bit.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D113753

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

[PATCH] D113753: [Analyzer][Core] Better simplification in SimpleSValBuilder::evalBinOpNN

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

steakhal added inline comments.



Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:378
+  SVal simplifiedLhs = simplifySVal(state, lhs);
+  SVal simplifiedRhs = simplifySVal(state, rhs);
+  if (auto simplifiedLhsAsNonLoc = simplifiedLhs.getAs())

It seems like you simplify the `rhs` as well. Could we have a test for that?



Comment at: clang/test/Analysis/svalbuilder-simplify-in-evalbinop.cpp:13
+void test_evalBinOp_simplifies(int x, int y) {
+  x = y / 77;
+  if (y != 77)

Please declare `x` in this statement.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D113753

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

[PATCH] D113753: [Analyzer][Core] Better simplification in SimpleSValBuilder::evalBinOpNN

[Gabor Marton via Phabricator via cfe-commits]

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

Make the SValBuilder capable to simplify existing
SVals based on a newly added constraints when evaluating a BinOp.

Before this patch, we called `simplify` only in some edge cases.
However, we can and should investigate the constraints in all cases.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D113753

Files:
  clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  clang/test/Analysis/svalbuilder-simplify-in-evalbinop.cpp


Index: clang/test/Analysis/svalbuilder-simplify-in-evalbinop.cpp
===
--- /dev/null
+++ clang/test/Analysis/svalbuilder-simplify-in-evalbinop.cpp
@@ -0,0 +1,18 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -verify
+
+// Here we test whether the SValBuilder is capable to simplify existing
+// SVals based on a newly added constraints when evaluating a BinOp.
+
+void clang_analyzer_eval(bool);
+
+void test_evalBinOp_simplifies(int x, int y) {
+  x = y / 77;
+  if (y != 77)
+return;
+  clang_analyzer_eval(x == 1); // expected-warning{{TRUE}}
+  (void)(x * y);
+}
Index: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
===
--- clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -372,6 +372,15 @@
   NonLoc InputLHS = lhs;
   NonLoc InputRHS = rhs;
 
+  // Constraints may have changed since the creation of a bound SVal. Check if
+  // the values can be simplified based on those new constraints.
+  SVal simplifiedLhs = simplifySVal(state, lhs);
+  SVal simplifiedRhs = simplifySVal(state, rhs);
+  if (auto simplifiedLhsAsNonLoc = simplifiedLhs.getAs())
+lhs = *simplifiedLhsAsNonLoc;
+  if (auto simplifiedRhsAsNonLoc = simplifiedRhs.getAs())
+rhs = *simplifiedRhsAsNonLoc;
+
   // Handle trivial case where left-side and right-side are the same.
   if (lhs == rhs)
 switch (op) {
@@ -619,16 +628,6 @@
 }
   }
 
-  // Does the symbolic expression simplify to a constant?
-  // If so, "fold" the constant by setting 'lhs' to a ConcreteInt
-  // and try again.
-  SVal simplifiedLhs = simplifySVal(state, lhs);
-  if (simplifiedLhs != lhs)
-if (auto simplifiedLhsAsNonLoc = simplifiedLhs.getAs()) {
-  lhs = *simplifiedLhsAsNonLoc;
-  continue;
-}
-
   // Is the RHS a constant?
   if (const llvm::APSInt *RHSValue = getKnownValue(state, rhs))
 return MakeSymIntVal(Sym, op, *RHSValue, resultTy);


Index: clang/test/Analysis/svalbuilder-simplify-in-evalbinop.cpp
===
--- /dev/null
+++ clang/test/Analysis/svalbuilder-simplify-in-evalbinop.cpp
@@ -0,0 +1,18 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -verify
+
+// Here we test whether the SValBuilder is capable to simplify existing
+// SVals based on a newly added constraints when evaluating a BinOp.
+
+void clang_analyzer_eval(bool);
+
+void test_evalBinOp_simplifies(int x, int y) {
+  x = y / 77;
+  if (y != 77)
+return;
+  clang_analyzer_eval(x == 1); // expected-warning{{TRUE}}
+  (void)(x * y);
+}
Index: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
===
--- clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -372,6 +372,15 @@
   NonLoc InputLHS = lhs;
   NonLoc InputRHS = rhs;
 
+  // Constraints may have changed since the creation of a bound SVal. Check if
+  // the values can be simplified based on those new constraints.
+  SVal simplifiedLhs = simplifySVal(state, lhs);
+  SVal simplifiedRhs = simplifySVal(state, rhs);
+  if (auto simplifiedLhsAsNonLoc = simplifiedLhs.getAs())
+lhs = *simplifiedLhsAsNonLoc;
+  if (auto simplifiedRhsAsNonLoc = simplifiedRhs.getAs())
+rhs = *simplifiedRhsAsNonLoc;
+
   // Handle trivial case where left-side and right-side are the same.
   if (lhs == rhs)
 switch (op) {
@@ -619,16 +628,6 @@
 }
   }
 
-  // Does the symbolic expression simplify to a constant?
-  // If so, "fold" the constant by setting 'lhs' to a ConcreteInt
-  // and try again.
-  SVal simplifiedLhs = simplifySVal(state, lhs);
-  if (simplifiedLhs != lhs)
-if (auto