[PATCH] D113754: [Analyzer][Core] Simplify IntSym in SValBuilder

[Gabor Marton via Phabricator via cfe-commits]

This revision was automatically updated to reflect the committed changes.
Closed by commit rGffc32efd1cd6: [Analyzer][Core] Simplify IntSym in 
SValBuilder (authored by martong).

Changed prior to commit:
  https://reviews.llvm.org/D113754?vs=386800=388927#toc

Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D113754

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


Index: clang/test/Analysis/svalbuilder-simplify-intsym.cpp
===
--- /dev/null
+++ clang/test/Analysis/svalbuilder-simplify-intsym.cpp
@@ -0,0 +1,20 @@
+// 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
+// IntSym expressions based on a newly added constraint on the sub-expression.
+
+void clang_analyzer_eval(bool);
+
+void test_SValBuilder_simplifies_IntSym(int x, int y) {
+  // Most IntSym BinOps are transformed to SymInt in SimpleSValBuilder.
+  // Division is one exception.
+  x = 77 / y;
+  if (y != 1)
+return;
+  clang_analyzer_eval(x == 77); // 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
@@ -1183,6 +1183,19 @@
   S, SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType()));
 }
 
+SVal VisitIntSymExpr(const IntSymExpr *S) {
+  auto I = Cached.find(S);
+  if (I != Cached.end())
+return I->second;
+
+  SVal RHS = Visit(S->getRHS());
+  if (isUnchanged(S->getRHS(), RHS))
+return skip(S);
+  SVal LHS = SVB.makeIntVal(S->getLHS());
+  return cache(
+  S, SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType()));
+}
+
 SVal VisitSymSymExpr(const SymSymExpr *S) {
   auto I = Cached.find(S);
   if (I != Cached.end())


Index: clang/test/Analysis/svalbuilder-simplify-intsym.cpp
===
--- /dev/null
+++ clang/test/Analysis/svalbuilder-simplify-intsym.cpp
@@ -0,0 +1,20 @@
+// 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
+// IntSym expressions based on a newly added constraint on the sub-expression.
+
+void clang_analyzer_eval(bool);
+
+void test_SValBuilder_simplifies_IntSym(int x, int y) {
+  // Most IntSym BinOps are transformed to SymInt in SimpleSValBuilder.
+  // Division is one exception.
+  x = 77 / y;
+  if (y != 1)
+return;
+  clang_analyzer_eval(x == 77); // 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
@@ -1183,6 +1183,19 @@
   S, SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType()));
 }
 
+SVal VisitIntSymExpr(const IntSymExpr *S) {
+  auto I = Cached.find(S);
+  if (I != Cached.end())
+return I->second;
+
+  SVal RHS = Visit(S->getRHS());
+  if (isUnchanged(S->getRHS(), RHS))
+return skip(S);
+  SVal LHS = SVB.makeIntVal(S->getLHS());
+  return cache(
+  S, SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType()));
+}
+
 SVal VisitSymSymExpr(const SymSymExpr *S) {
   auto I = Cached.find(S);
   if (I != Cached.end())
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D113754: [Analyzer][Core] Simplify IntSym in SValBuilder

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

steakhal added a comment.

Great news, thanks.




Comment at: clang/test/Analysis/svalbuilder-simplify-intsym.cpp:18
+return;
+  clang_analyzer_eval(x == 77); // expected-warning{{TRUE}}
+  (void)(x * y);

extra spaces?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D113754

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

[PATCH] D113754: [Analyzer][Core] Simplify IntSym in SValBuilder

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

In D113754#3127245 , @steakhal wrote:

> Great stuff. Have you checked the coverage?

Thanks for the review! So, here are the coverage results for the new test file:

  1186   2 : SVal VisitIntSymExpr(const IntSymExpr *S) {
  1187   2 :   auto I = Cached.find(S);
  1188   2 :   if (I != Cached.end())
  1189   0 : return I->second;
  1190 :
  1191   2 :   SVal RHS = Visit(S->getRHS());
  1192   2 :   if (isUnchanged(S->getRHS(), RHS))
  1193   0 : return skip(S);
  1194   2 :   SVal LHS = SVB.makeIntVal(S->getLHS());
  1195 :   return cache(
  1196   2 :   S, SVB.evalBinOp(State, S->getOpcode(), LHS, 
RHS, S->getType()));
  1197 : }

L1189 is not covered, but that is related to the caching mechanism, which is 
already existing and this patch is independent from that. We have the very same 
caching implementation in all the other `Visit` functions.
L1193 There is an existing test case in `find-binop-constraints.cpp` which 
covers this line. :

  int test_lhs_and_rhs_further_constrained(int x, int y) {
if (x % y != 1)
  return 0;
if (x != 1)
  return 0;
if (y != 2)
  return 0;
clang_analyzer_eval(x % y == 1); // expected-warning{{TRUE}}
clang_analyzer_eval(y == 2); // expected-warning{{TRUE}}
return 0;
  }

I could have replicated this test case here, but hadn't been able to formulate 
any new expectations with a `clang_analyzer_` function. So there is no visible 
functional change in this case with this patch concerning this line. Besides, 
all other existing `Visit` functions have the same optimization and they do an 
early return with `skip` if the symbol is unchanged.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D113754

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

[PATCH] D113754: [Analyzer][Core] Simplify IntSym in SValBuilder

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

Great stuff. Have you checked the coverage?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D113754

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

[PATCH] D113754: [Analyzer][Core] Simplify IntSym in SValBuilder

[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 SimpleSValBuilder capable to simplify existing IntSym
expressions based on a newly added constraint on the sub-expression.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D113754

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


Index: clang/test/Analysis/svalbuilder-simplify-intsym.cpp
===
--- /dev/null
+++ clang/test/Analysis/svalbuilder-simplify-intsym.cpp
@@ -0,0 +1,20 @@
+// 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
+// IntSym expressions based on a newly added constraint on the sub-expression.
+
+void clang_analyzer_eval(bool);
+
+void test_SValBuilder_simplifies_IntSym(int x, int y) {
+  // Most IntSym BinOps are transformed to SymInt in SimpleSValBuilder.
+  // Division is one exception.
+  x = 77 / y;
+  if (y != 1)
+return;
+  clang_analyzer_eval(x == 77); // 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
@@ -1183,6 +1183,19 @@
   S, SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType()));
 }
 
+SVal VisitIntSymExpr(const IntSymExpr *S) {
+  auto I = Cached.find(S);
+  if (I != Cached.end())
+return I->second;
+
+  SVal RHS = Visit(S->getRHS());
+  if (isUnchanged(S->getRHS(), RHS))
+return skip(S);
+  SVal LHS = SVB.makeIntVal(S->getLHS());
+  return cache(
+  S, SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType()));
+}
+
 SVal VisitSymSymExpr(const SymSymExpr *S) {
   auto I = Cached.find(S);
   if (I != Cached.end())


Index: clang/test/Analysis/svalbuilder-simplify-intsym.cpp
===
--- /dev/null
+++ clang/test/Analysis/svalbuilder-simplify-intsym.cpp
@@ -0,0 +1,20 @@
+// 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
+// IntSym expressions based on a newly added constraint on the sub-expression.
+
+void clang_analyzer_eval(bool);
+
+void test_SValBuilder_simplifies_IntSym(int x, int y) {
+  // Most IntSym BinOps are transformed to SymInt in SimpleSValBuilder.
+  // Division is one exception.
+  x = 77 / y;
+  if (y != 1)
+return;
+  clang_analyzer_eval(x == 77); // 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
@@ -1183,6 +1183,19 @@
   S, SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType()));
 }
 
+SVal VisitIntSymExpr(const IntSymExpr *S) {
+  auto I = Cached.find(S);
+  if (I != Cached.end())
+return I->second;
+
+  SVal RHS = Visit(S->getRHS());
+  if (isUnchanged(S->getRHS(), RHS))
+return skip(S);
+  SVal LHS = SVB.makeIntVal(S->getLHS());
+  return cache(
+  S, SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType()));
+}
+
 SVal VisitSymSymExpr(const SymSymExpr *S) {
   auto I = Cached.find(S);
   if (I != Cached.end())
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits