[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

martong added inline comments.



Comment at: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp:46
+ConstraintManager::ProgramStatePair
+ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) {
+  ProgramStateRef StTrue = assume(State, Cond, true);

TODO We should have a very similar implementation for 
`assumeInclusiveRangeDual`! (Not that high prio, that is used only by the 
BoolAssignmentChecker).


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

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

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Nico Weber via Phabricator via cfe-commits]

thakis added a comment.

https://github.com/llvm/llvm-project/commit/21feafaeb85aad2847db44aa2208999b166ba4a9
 fixed it, thanks!


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

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

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Nico Weber via Phabricator via cfe-commits]

thakis added a comment.

One of your 3 commits in 
https://github.com/llvm/llvm-project/compare/3d888b0491f8...34ac048aef29 broke 
check-clang on Windows: http://45.33.8.238/win/57870/step_7.txt

Please take a look, and revert for now if it takes a while to fix.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

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

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

This revision was automatically updated to reflect the committed changes.
Closed by commit rGc4fa05f5f778: [analyzer] Indicate if a parent state is 
infeasible (authored by martong).

Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
  clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/ProgramState.cpp
  clang/test/Analysis/infeasible-sink.c

Index: clang/test/Analysis/infeasible-sink.c
===
--- /dev/null
+++ clang/test/Analysis/infeasible-sink.c
@@ -0,0 +1,80 @@
+// 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 that if it turns out that the parent state is infeasible then
+// both children States (more precisely the ExplodedNodes) are marked as a
+// Sink.
+// We rely on existing defects of the underlying constraint solver. However,
+// in the future we might strengthen the solver to discover the infeasibility
+// right when we create the parent state. At that point some of these tests
+// will fail, and either we shall find another solver weakness to have the test
+// case functioning, or we shall simply remove that.
+
+void clang_analyzer_warnIfReached();
+void clang_analyzer_eval(int);
+
+void test1(int x) {
+  if (x * x != 4)
+return;
+  if (x < 0 || x > 1)
+return;
+
+  // { x^2 == 4 and x:[0,1] }
+  // This state is already infeasible.
+
+  // Perfectly constraining 'x' will trigger constant folding,
+  // when we realize we were already infeasible.
+  // The same happens for the 'else' branch.
+  if (x == 0) {
+clang_analyzer_warnIfReached(); // no-warning
+  } else {
+clang_analyzer_warnIfReached(); // no-warning
+  }
+  clang_analyzer_warnIfReached(); // no-warning
+  (void)x;
+}
+
+int a, b, c, d, e;
+void test2() {
+
+  if (a == 0)
+return;
+
+  if (e != c)
+return;
+
+  d = e - c;
+  b = d;
+  a -= d;
+
+  if (a != 0)
+return;
+
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+
+  /* The BASELINE passes these checks ('wrning' is used to avoid lit to match)
+  // The parent state is already infeasible, look at this contradiction:
+  clang_analyzer_eval(b > 0);  // expected-wrning{{FALSE}}
+  clang_analyzer_eval(b <= 0); // expected-wrning{{FALSE}}
+  // Crashes with expensive checks.
+  if (b > 0) {
+clang_analyzer_warnIfReached(); // no-warning, OK
+return;
+  }
+  // Should not be reachable.
+  clang_analyzer_warnIfReached(); // expected-wrning{{REACHABLE}}
+  */
+
+  // The parent state is already infeasible, but we realize that only if b is
+  // constrained.
+  clang_analyzer_eval(b > 0);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(b <= 0); // expected-warning{{UNKNOWN}}
+  if (b > 0) {
+clang_analyzer_warnIfReached(); // no-warning
+return;
+  }
+  clang_analyzer_warnIfReached(); // no-warning
+}
Index: clang/lib/StaticAnalyzer/Core/ProgramState.cpp
===
--- clang/lib/StaticAnalyzer/Core/ProgramState.cpp
+++ clang/lib/StaticAnalyzer/Core/ProgramState.cpp
@@ -55,7 +55,7 @@
 
 ProgramState::ProgramState(const ProgramState )
 : stateMgr(RHS.stateMgr), Env(RHS.Env), store(RHS.store), GDM(RHS.GDM),
-  refCount(0) {
+  PosteriorlyOverconstrained(RHS.PosteriorlyOverconstrained), refCount(0) {
   stateMgr->getStoreManager().incrementReferenceCount(store);
 }
 
@@ -429,6 +429,12 @@
   return getStateManager().getPersistentState(NewSt);
 }
 
+ProgramStateRef ProgramState::cloneAsPosteriorlyOverconstrained() const {
+  ProgramState NewSt(*this);
+  NewSt.PosteriorlyOverconstrained = true;
+  return getStateManager().getPersistentState(NewSt);
+}
+
 void ProgramState::setStore(const StoreRef ) {
   Store newStoreStore = newStore.getStore();
   if (newStoreStore)
Index: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
===
--- clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@ -41,3 +41,32 @@
 return ConditionTruthVal(true);
   return {};
 }
+
+ConstraintManager::ProgramStatePair
+ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) {
+  ProgramStateRef StTrue = assume(State, Cond, true);
+
+  if (!StTrue) {
+ProgramStateRef StFalse = assume(State, Cond, false);
+if (LLVM_UNLIKELY(!StFalse)) { // both infeasible
+  ProgramStateRef StInfeasible = State->cloneAsPosteriorlyOverconstrained();
+  

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

martong updated this revision to Diff 427625.
martong marked 2 inline comments as done.
martong added a comment.

- Fix typos in essay


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
  clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/ProgramState.cpp
  clang/test/Analysis/infeasible-sink.c

Index: clang/test/Analysis/infeasible-sink.c
===
--- /dev/null
+++ clang/test/Analysis/infeasible-sink.c
@@ -0,0 +1,80 @@
+// 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 that if it turns out that the parent state is infeasible then
+// both children States (more precisely the ExplodedNodes) are marked as a
+// Sink.
+// We rely on existing defects of the underlying constraint solver. However,
+// in the future we might strengthen the solver to discover the infeasibility
+// right when we create the parent state. At that point some of these tests
+// will fail, and either we shall find another solver weakness to have the test
+// case functioning, or we shall simply remove that.
+
+void clang_analyzer_warnIfReached();
+void clang_analyzer_eval(int);
+
+void test1(int x) {
+  if (x * x != 4)
+return;
+  if (x < 0 || x > 1)
+return;
+
+  // { x^2 == 4 and x:[0,1] }
+  // This state is already infeasible.
+
+  // Perfectly constraining 'x' will trigger constant folding,
+  // when we realize we were already infeasible.
+  // The same happens for the 'else' branch.
+  if (x == 0) {
+clang_analyzer_warnIfReached(); // no-warning
+  } else {
+clang_analyzer_warnIfReached(); // no-warning
+  }
+  clang_analyzer_warnIfReached(); // no-warning
+  (void)x;
+}
+
+int a, b, c, d, e;
+void test2() {
+
+  if (a == 0)
+return;
+
+  if (e != c)
+return;
+
+  d = e - c;
+  b = d;
+  a -= d;
+
+  if (a != 0)
+return;
+
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+
+  /* The BASELINE passes these checks ('wrning' is used to avoid lit to match)
+  // The parent state is already infeasible, look at this contradiction:
+  clang_analyzer_eval(b > 0);  // expected-wrning{{FALSE}}
+  clang_analyzer_eval(b <= 0); // expected-wrning{{FALSE}}
+  // Crashes with expensive checks.
+  if (b > 0) {
+clang_analyzer_warnIfReached(); // no-warning, OK
+return;
+  }
+  // Should not be reachable.
+  clang_analyzer_warnIfReached(); // expected-wrning{{REACHABLE}}
+  */
+
+  // The parent state is already infeasible, but we realize that only if b is
+  // constrained.
+  clang_analyzer_eval(b > 0);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(b <= 0); // expected-warning{{UNKNOWN}}
+  if (b > 0) {
+clang_analyzer_warnIfReached(); // no-warning
+return;
+  }
+  clang_analyzer_warnIfReached(); // no-warning
+}
Index: clang/lib/StaticAnalyzer/Core/ProgramState.cpp
===
--- clang/lib/StaticAnalyzer/Core/ProgramState.cpp
+++ clang/lib/StaticAnalyzer/Core/ProgramState.cpp
@@ -55,7 +55,7 @@
 
 ProgramState::ProgramState(const ProgramState )
 : stateMgr(RHS.stateMgr), Env(RHS.Env), store(RHS.store), GDM(RHS.GDM),
-  refCount(0) {
+  PosteriorlyOverconstrained(RHS.PosteriorlyOverconstrained), refCount(0) {
   stateMgr->getStoreManager().incrementReferenceCount(store);
 }
 
@@ -429,6 +429,12 @@
   return getStateManager().getPersistentState(NewSt);
 }
 
+ProgramStateRef ProgramState::cloneAsPosteriorlyOverconstrained() const {
+  ProgramState NewSt(*this);
+  NewSt.PosteriorlyOverconstrained = true;
+  return getStateManager().getPersistentState(NewSt);
+}
+
 void ProgramState::setStore(const StoreRef ) {
   Store newStoreStore = newStore.getStore();
   if (newStoreStore)
Index: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
===
--- clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@ -41,3 +41,32 @@
 return ConditionTruthVal(true);
   return {};
 }
+
+ConstraintManager::ProgramStatePair
+ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) {
+  ProgramStateRef StTrue = assume(State, Cond, true);
+
+  if (!StTrue) {
+ProgramStateRef StFalse = assume(State, Cond, false);
+if (LLVM_UNLIKELY(!StFalse)) { // both infeasible
+  ProgramStateRef StInfeasible = State->cloneAsPosteriorlyOverconstrained();
+  assert(StInfeasible->isPosteriorlyOverconstrained());
+  // Checkers might rely on the 

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

martong added inline comments.



Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:99
+  // recognise that a parent is infeasible only *after* a new and more specific
+  // constraint and its negation is evaluated.
+  //

Yeah, thx, I've also found one more typo. That's the problem with long comments 
:D


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

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

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

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

steakhal accepted this revision.
steakhal added a comment.

only a few typos




Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:89-114
+  // A state is infeasible if there is a contradiction among the constraints.
+  // An infeasible state is represented by a nullptr.
+  // In the sense of `assumeDual`, a state can have two children by adding a
+  // new constraint and the negation of that new constraint. A parent state is
+  // over-constrained if both of its children are infeasible. In the
+  // mathematical sense it means that the parent is infeasible and we should
+  // have realised that at the moment when we have created it. However, we




Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

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

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

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

- Add explanatory comment, rename to PosteriorlyOverconstrained


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
  clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/ProgramState.cpp
  clang/test/Analysis/infeasible-sink.c

Index: clang/test/Analysis/infeasible-sink.c
===
--- /dev/null
+++ clang/test/Analysis/infeasible-sink.c
@@ -0,0 +1,80 @@
+// 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 that if it turns out that the parent state is infeasible then
+// both children States (more precisely the ExplodedNodes) are marked as a
+// Sink.
+// We rely on existing defects of the underlying constraint solver. However,
+// in the future we might strengthen the solver to discover the infeasibility
+// right when we create the parent state. At that point some of these tests
+// will fail, and either we shall find another solver weakness to have the test
+// case functioning, or we shall simply remove that.
+
+void clang_analyzer_warnIfReached();
+void clang_analyzer_eval(int);
+
+void test1(int x) {
+  if (x * x != 4)
+return;
+  if (x < 0 || x > 1)
+return;
+
+  // { x^2 == 4 and x:[0,1] }
+  // This state is already infeasible.
+
+  // Perfectly constraining 'x' will trigger constant folding,
+  // when we realize we were already infeasible.
+  // The same happens for the 'else' branch.
+  if (x == 0) {
+clang_analyzer_warnIfReached(); // no-warning
+  } else {
+clang_analyzer_warnIfReached(); // no-warning
+  }
+  clang_analyzer_warnIfReached(); // no-warning
+  (void)x;
+}
+
+int a, b, c, d, e;
+void test2() {
+
+  if (a == 0)
+return;
+
+  if (e != c)
+return;
+
+  d = e - c;
+  b = d;
+  a -= d;
+
+  if (a != 0)
+return;
+
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+
+  /* The BASELINE passes these checks ('wrning' is used to avoid lit to match)
+  // The parent state is already infeasible, look at this contradiction:
+  clang_analyzer_eval(b > 0);  // expected-wrning{{FALSE}}
+  clang_analyzer_eval(b <= 0); // expected-wrning{{FALSE}}
+  // Crashes with expensive checks.
+  if (b > 0) {
+clang_analyzer_warnIfReached(); // no-warning, OK
+return;
+  }
+  // Should not be reachable.
+  clang_analyzer_warnIfReached(); // expected-wrning{{REACHABLE}}
+  */
+
+  // The parent state is already infeasible, but we realize that only if b is
+  // constrained.
+  clang_analyzer_eval(b > 0);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(b <= 0); // expected-warning{{UNKNOWN}}
+  if (b > 0) {
+clang_analyzer_warnIfReached(); // no-warning
+return;
+  }
+  clang_analyzer_warnIfReached(); // no-warning
+}
Index: clang/lib/StaticAnalyzer/Core/ProgramState.cpp
===
--- clang/lib/StaticAnalyzer/Core/ProgramState.cpp
+++ clang/lib/StaticAnalyzer/Core/ProgramState.cpp
@@ -55,7 +55,7 @@
 
 ProgramState::ProgramState(const ProgramState )
 : stateMgr(RHS.stateMgr), Env(RHS.Env), store(RHS.store), GDM(RHS.GDM),
-  refCount(0) {
+  PosteriorlyOverconstrained(RHS.PosteriorlyOverconstrained), refCount(0) {
   stateMgr->getStoreManager().incrementReferenceCount(store);
 }
 
@@ -429,6 +429,12 @@
   return getStateManager().getPersistentState(NewSt);
 }
 
+ProgramStateRef ProgramState::cloneAsPosteriorlyOverconstrained() const {
+  ProgramState NewSt(*this);
+  NewSt.PosteriorlyOverconstrained = true;
+  return getStateManager().getPersistentState(NewSt);
+}
+
 void ProgramState::setStore(const StoreRef ) {
   Store newStoreStore = newStore.getStore();
   if (newStoreStore)
Index: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
===
--- clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@ -41,3 +41,32 @@
 return ConditionTruthVal(true);
   return {};
 }
+
+ConstraintManager::ProgramStatePair
+ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) {
+  ProgramStateRef StTrue = assume(State, Cond, true);
+
+  if (!StTrue) {
+ProgramStateRef StFalse = assume(State, Cond, false);
+if (LLVM_UNLIKELY(!StFalse)) { // both infeasible
+  ProgramStateRef StInfeasible = State->cloneAsPosteriorlyOverconstrained();
+  

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

martong marked an inline comment as done.
martong added a comment.

In D124674#3491710 , @NoQ wrote:

> Yes, we've discussed this before, and I'm very much in favor of this change. 
> This is assertion removal, and the assertion has been really useful back in 
> the day, but the assertion doesn't seem to be realistic to maintain with all 
> the new logic in the constraint solver coming in in recent years.

Thanks for your review and support!




Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:88
   GenericDataMap   GDM;  // Custom data stored by a client of this class.
+  bool Infeasible = false;
   unsigned refCount;

NoQ wrote:
> The reader deserves a massive amount of explanation here. Normally infeasible 
> states are just null states. We need to explain how these new infeasible 
> states are different.
> 
> Maybe a longer name? `IsPostOverconstrained` or something like that.
Okay, I've added an essay that explains these differences.

> Maybe a longer name? IsPostOverconstrained or something like that.
Yeah, I agree a longer name could reflect that this is something that requires 
special handling. I chose `PosteriorlyOverconstrained`.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

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

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

Yes, we've discussed this before, and I'm very much in favor of this change. 
This is assertion removal, and the assertion has been really useful back in the 
day, but the assertion doesn't seem to be realistic to maintain with all the 
new logic in the constraint solver coming in in recent years.




Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:88
   GenericDataMap   GDM;  // Custom data stored by a client of this class.
+  bool Infeasible = false;
   unsigned refCount;

The reader deserves a massive amount of explanation here. Normally infeasible 
states are just null states. We need to explain how these new infeasible states 
are different.

Maybe a longer name? `IsPostOverconstrained` or something like that.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

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

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

@NoQ Could you please take a look? This change effects the very core of the 
analyzer.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

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

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

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

- Add LLVM_UNLIKELY


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
  clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/ProgramState.cpp
  clang/test/Analysis/infeasible-sink.c

Index: clang/test/Analysis/infeasible-sink.c
===
--- /dev/null
+++ clang/test/Analysis/infeasible-sink.c
@@ -0,0 +1,80 @@
+// 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 that if it turns out that the parent state is infeasible then
+// both children States (more precisely the ExplodedNodes) are marked as a
+// Sink.
+// We rely on existing defects of the underlying constraint solver. However,
+// in the future we might strengthen the solver to discover the infeasibility
+// right when we create the parent state. At that point some of these tests
+// will fail, and either we shall find another solver weakness to have the test
+// case functioning, or we shall simply remove that.
+
+void clang_analyzer_warnIfReached();
+void clang_analyzer_eval(int);
+
+void test1(int x) {
+  if (x * x != 4)
+return;
+  if (x < 0 || x > 1)
+return;
+
+  // { x^2 == 4 and x:[0,1] }
+  // This state is already infeasible.
+
+  // Perfectly constraining 'x' will trigger constant folding,
+  // when we realize we were already infeasible.
+  // The same happens for the 'else' branch.
+  if (x == 0) {
+clang_analyzer_warnIfReached(); // no-warning
+  } else {
+clang_analyzer_warnIfReached(); // no-warning
+  }
+  clang_analyzer_warnIfReached(); // no-warning
+  (void)x;
+}
+
+int a, b, c, d, e;
+void test2() {
+
+  if (a == 0)
+return;
+
+  if (e != c)
+return;
+
+  d = e - c;
+  b = d;
+  a -= d;
+
+  if (a != 0)
+return;
+
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+
+  /* The BASELINE passes these checks ('wrning' is used to avoid lit to match)
+  // The parent state is already infeasible, look at this contradiction:
+  clang_analyzer_eval(b > 0);  // expected-wrning{{FALSE}}
+  clang_analyzer_eval(b <= 0); // expected-wrning{{FALSE}}
+  // Crashes with expensive checks.
+  if (b > 0) {
+clang_analyzer_warnIfReached(); // no-warning, OK
+return;
+  }
+  // Should not be reachable.
+  clang_analyzer_warnIfReached(); // expected-wrning{{REACHABLE}}
+  */
+
+  // The parent state is already infeasible, but we realize that only if b is
+  // constrained.
+  clang_analyzer_eval(b > 0);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(b <= 0); // expected-warning{{UNKNOWN}}
+  if (b > 0) {
+clang_analyzer_warnIfReached(); // no-warning
+return;
+  }
+  clang_analyzer_warnIfReached(); // no-warning
+}
Index: clang/lib/StaticAnalyzer/Core/ProgramState.cpp
===
--- clang/lib/StaticAnalyzer/Core/ProgramState.cpp
+++ clang/lib/StaticAnalyzer/Core/ProgramState.cpp
@@ -55,7 +55,7 @@
 
 ProgramState::ProgramState(const ProgramState )
 : stateMgr(RHS.stateMgr), Env(RHS.Env), store(RHS.store), GDM(RHS.GDM),
-  refCount(0) {
+  Infeasible(RHS.Infeasible), refCount(0) {
   stateMgr->getStoreManager().incrementReferenceCount(store);
 }
 
@@ -429,6 +429,12 @@
   return getStateManager().getPersistentState(NewSt);
 }
 
+ProgramStateRef ProgramState::cloneAsInfeasible() const {
+  ProgramState NewSt(*this);
+  NewSt.Infeasible = true;
+  return getStateManager().getPersistentState(NewSt);
+}
+
 void ProgramState::setStore(const StoreRef ) {
   Store newStoreStore = newStore.getStore();
   if (newStoreStore)
Index: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
===
--- clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@ -41,3 +41,32 @@
 return ConditionTruthVal(true);
   return {};
 }
+
+ConstraintManager::ProgramStatePair
+ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) {
+  ProgramStateRef StTrue = assume(State, Cond, true);
+
+  if (!StTrue) {
+ProgramStateRef StFalse = assume(State, Cond, false);
+if (LLVM_UNLIKELY(!StFalse)) { // both infeasible
+  ProgramStateRef StInfeasible = State->cloneAsInfeasible();
+  assert(StInfeasible->isInfeasible());
+  // Checkers might rely on the API contract that both returned states
+  // cannot be null. Thus, we return StInfeasible for both branches because
+  // it might 

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

martong added inline comments.



Comment at: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp:51
+ProgramStateRef StFalse = assume(State, Cond, false);
+if (!StFalse) { // both infeasible
+  ProgramStateRef Infeasible = State->cloneAsInfeasible();

martong wrote:
> martong wrote:
> > martong wrote:
> > > steakhal wrote:
> > > > Should we mark this `LLVM_UNLIKELY(cond)`?
> > > > I would expect this function to be quite hot, and infeasible states 
> > > > rare.
> > > > 
> > > > Could we measure this one?
> > > Yes, it could be.
> > > 
> > > Let me come back with some measurement results soon. I am going to use 
> > > llvm statistics macros to measure this, but that makes sense on top of 
> > > D124758
> > This is what I use for the measurement, stay tuned for the results.
> > ```
> > diff --git a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp 
> > b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
> > index ef98ed7d36e9..82097d67ec0f 100644
> > --- a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
> > +++ b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
> > @@ -16,10 +16,16 @@
> >  #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
> >  #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
> >  #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
> > +#include "llvm/ADT/Statistic.h"
> > 
> >  using namespace clang;
> >  using namespace ento;
> > 
> > +#define DEBUG_TYPE "CoreEngine"
> > +
> > +STATISTIC(NumInfeasible, "The # of infeasible states");
> > +STATISTIC(NumFeasible, "The # of feasible states");
> > +
> >  ConstraintManager::~ConstraintManager() = default;
> > 
> >  static DefinedSVal getLocFromSymbol(const ProgramStateRef ,
> > @@ -51,16 +57,20 @@ ConstraintManager::assumeDual(ProgramStateRef State, 
> > DefinedSVal Cond) {
> >  if (!StFalse) { // both infeasible
> >ProgramStateRef Infeasible = State->cloneAsInfeasible();
> >assert(Infeasible->isInfeasible());
> > +  ++NumInfeasible;
> >return ProgramStatePair(Infeasible, Infeasible);
> >  }
> > +++NumFeasible;
> >  return ProgramStatePair(nullptr, StFalse);
> >}
> > 
> >ProgramStateRef StFalse = assumeInternal(State, Cond, false);
> >if (!StFalse) {
> > +++NumFeasible;
> >  return ProgramStatePair(StTrue, nullptr);
> >}
> > 
> > +  ++NumFeasible;
> >return ProgramStatePair(StTrue, StFalse);
> >  }
> > ```
> Ups, the purpose of the measure is to determine if UNLIKELY is justified, so 
> this diff seems better, restarted the measurement with it.
> ```
> --- a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
> +++ b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
> @@ -16,10 +16,16 @@
>  #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
>  #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
>  #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
> +#include "llvm/ADT/Statistic.h"
> 
>  using namespace clang;
>  using namespace ento;
> 
> +#define DEBUG_TYPE "CoreEngine"
> +
> +STATISTIC(NumInfeasible, "The # of infeasible states");
> +STATISTIC(NumFeasible, "The # of feasible states");
> +
>  ConstraintManager::~ConstraintManager() = default;
> 
>  static DefinedSVal getLocFromSymbol(const ProgramStateRef ,
> @@ -51,8 +57,10 @@ ConstraintManager::assumeDual(ProgramStateRef State, 
> DefinedSVal Cond) {
>  if (!StFalse) { // both infeasible
>ProgramStateRef Infeasible = State->cloneAsInfeasible();
>assert(Infeasible->isInfeasible());
> +  ++NumInfeasible;
>return ProgramStatePair(Infeasible, Infeasible);
>  }
> +++NumFeasible;
>  return ProgramStatePair(nullptr, StFalse);
>}
> 
> ```
This is indeed UNLIKELY. Seems like a good upper-bound for the ratio's order of 
magnitude is around 1000 / 10 million i.e. 0.0001.
{F22964634}


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

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

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

martong marked an inline comment as done.
martong added inline comments.



Comment at: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp:51
+ProgramStateRef StFalse = assume(State, Cond, false);
+if (!StFalse) { // both infeasible
+  ProgramStateRef Infeasible = State->cloneAsInfeasible();

martong wrote:
> martong wrote:
> > steakhal wrote:
> > > Should we mark this `LLVM_UNLIKELY(cond)`?
> > > I would expect this function to be quite hot, and infeasible states rare.
> > > 
> > > Could we measure this one?
> > Yes, it could be.
> > 
> > Let me come back with some measurement results soon. I am going to use llvm 
> > statistics macros to measure this, but that makes sense on top of D124758
> This is what I use for the measurement, stay tuned for the results.
> ```
> diff --git a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp 
> b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
> index ef98ed7d36e9..82097d67ec0f 100644
> --- a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
> +++ b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
> @@ -16,10 +16,16 @@
>  #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
>  #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
>  #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
> +#include "llvm/ADT/Statistic.h"
> 
>  using namespace clang;
>  using namespace ento;
> 
> +#define DEBUG_TYPE "CoreEngine"
> +
> +STATISTIC(NumInfeasible, "The # of infeasible states");
> +STATISTIC(NumFeasible, "The # of feasible states");
> +
>  ConstraintManager::~ConstraintManager() = default;
> 
>  static DefinedSVal getLocFromSymbol(const ProgramStateRef ,
> @@ -51,16 +57,20 @@ ConstraintManager::assumeDual(ProgramStateRef State, 
> DefinedSVal Cond) {
>  if (!StFalse) { // both infeasible
>ProgramStateRef Infeasible = State->cloneAsInfeasible();
>assert(Infeasible->isInfeasible());
> +  ++NumInfeasible;
>return ProgramStatePair(Infeasible, Infeasible);
>  }
> +++NumFeasible;
>  return ProgramStatePair(nullptr, StFalse);
>}
> 
>ProgramStateRef StFalse = assumeInternal(State, Cond, false);
>if (!StFalse) {
> +++NumFeasible;
>  return ProgramStatePair(StTrue, nullptr);
>}
> 
> +  ++NumFeasible;
>return ProgramStatePair(StTrue, StFalse);
>  }
> ```
Ups, the purpose of the measure is to determine if UNLIKELY is justified, so 
this diff seems better, restarted the measurement with it.
```
--- a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@ -16,10 +16,16 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
+#include "llvm/ADT/Statistic.h"

 using namespace clang;
 using namespace ento;

+#define DEBUG_TYPE "CoreEngine"
+
+STATISTIC(NumInfeasible, "The # of infeasible states");
+STATISTIC(NumFeasible, "The # of feasible states");
+
 ConstraintManager::~ConstraintManager() = default;

 static DefinedSVal getLocFromSymbol(const ProgramStateRef ,
@@ -51,8 +57,10 @@ ConstraintManager::assumeDual(ProgramStateRef State, 
DefinedSVal Cond) {
 if (!StFalse) { // both infeasible
   ProgramStateRef Infeasible = State->cloneAsInfeasible();
   assert(Infeasible->isInfeasible());
+  ++NumInfeasible;
   return ProgramStatePair(Infeasible, Infeasible);
 }
+++NumFeasible;
 return ProgramStatePair(nullptr, StFalse);
   }

```


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

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

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

martong marked an inline comment as done.
martong added inline comments.



Comment at: clang/test/Analysis/sink-infeasible.c:37-48
+  /* The BASELINE passes these checks ('wrning' is used to avoid lit to match)
+  // The parent state is already infeasible, look at this contradiction:
+  clang_analyzer_eval(b > 0);  // expected-wrning{{FALSE}}
+  clang_analyzer_eval(b <= 0); // expected-wrning{{FALSE}}
+  // Crashes with expensive checks.
+  if (b > 0) {
+clang_analyzer_warnIfReached(); // no-warning, OK

steakhal wrote:
> martong wrote:
> > steakhal wrote:
> > > You could use a non-default check prefix.
> > No I can't, because this test code in the comment is meaningful only in the 
> > baseline, I cannot run both clang versions from lit.
> > 
> > So, actually there is no RUN line for these, it is here only to demonstrate 
> > what happens in the baseline.
> Okay, why don't we drop these if these are only applicable to the baseline?
> Should we really introduce 'stale' comments?
Ok, I can remove them if you insist, but I thought it might make it easier to 
understand what is changed.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

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

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

martong added inline comments.



Comment at: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp:51
+ProgramStateRef StFalse = assume(State, Cond, false);
+if (!StFalse) { // both infeasible
+  ProgramStateRef Infeasible = State->cloneAsInfeasible();

martong wrote:
> steakhal wrote:
> > Should we mark this `LLVM_UNLIKELY(cond)`?
> > I would expect this function to be quite hot, and infeasible states rare.
> > 
> > Could we measure this one?
> Yes, it could be.
> 
> Let me come back with some measurement results soon. I am going to use llvm 
> statistics macros to measure this, but that makes sense on top of D124758
This is what I use for the measurement, stay tuned for the results.
```
diff --git a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp 
b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
index ef98ed7d36e9..82097d67ec0f 100644
--- a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@ -16,10 +16,16 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
+#include "llvm/ADT/Statistic.h"

 using namespace clang;
 using namespace ento;

+#define DEBUG_TYPE "CoreEngine"
+
+STATISTIC(NumInfeasible, "The # of infeasible states");
+STATISTIC(NumFeasible, "The # of feasible states");
+
 ConstraintManager::~ConstraintManager() = default;

 static DefinedSVal getLocFromSymbol(const ProgramStateRef ,
@@ -51,16 +57,20 @@ ConstraintManager::assumeDual(ProgramStateRef State, 
DefinedSVal Cond) {
 if (!StFalse) { // both infeasible
   ProgramStateRef Infeasible = State->cloneAsInfeasible();
   assert(Infeasible->isInfeasible());
+  ++NumInfeasible;
   return ProgramStatePair(Infeasible, Infeasible);
 }
+++NumFeasible;
 return ProgramStatePair(nullptr, StFalse);
   }

   ProgramStateRef StFalse = assumeInternal(State, Cond, false);
   if (!StFalse) {
+++NumFeasible;
 return ProgramStatePair(StTrue, nullptr);
   }

+  ++NumFeasible;
   return ProgramStatePair(StTrue, StFalse);
 }
```


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

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

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

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

- Add a simpler test case


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
  clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/ProgramState.cpp
  clang/test/Analysis/infeasible-sink.c

Index: clang/test/Analysis/infeasible-sink.c
===
--- /dev/null
+++ clang/test/Analysis/infeasible-sink.c
@@ -0,0 +1,80 @@
+// 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 that if it turns out that the parent state is infeasible then
+// both children States (more precisely the ExplodedNodes) are marked as a
+// Sink.
+// We rely on existing defects of the underlying constraint solver. However,
+// in the future we might strengthen the solver to discover the infeasibility
+// right when we create the parent state. At that point some of these tests
+// will fail, and either we shall find another solver weakness to have the test
+// case functioning, or we shall simply remove that.
+
+void clang_analyzer_warnIfReached();
+void clang_analyzer_eval(int);
+
+void test1(int x) {
+  if (x * x != 4)
+return;
+  if (x < 0 || x > 1)
+return;
+
+  // { x^2 == 4 and x:[0,1] }
+  // This state is already infeasible.
+
+  // Perfectly constraining 'x' will trigger constant folding,
+  // when we realize we were already infeasible.
+  // The same happens for the 'else' branch.
+  if (x == 0) {
+clang_analyzer_warnIfReached(); // no-warning
+  } else {
+clang_analyzer_warnIfReached(); // no-warning
+  }
+  clang_analyzer_warnIfReached(); // no-warning
+  (void)x;
+}
+
+int a, b, c, d, e;
+void test2() {
+
+  if (a == 0)
+return;
+
+  if (e != c)
+return;
+
+  d = e - c;
+  b = d;
+  a -= d;
+
+  if (a != 0)
+return;
+
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+
+  /* The BASELINE passes these checks ('wrning' is used to avoid lit to match)
+  // The parent state is already infeasible, look at this contradiction:
+  clang_analyzer_eval(b > 0);  // expected-wrning{{FALSE}}
+  clang_analyzer_eval(b <= 0); // expected-wrning{{FALSE}}
+  // Crashes with expensive checks.
+  if (b > 0) {
+clang_analyzer_warnIfReached(); // no-warning, OK
+return;
+  }
+  // Should not be reachable.
+  clang_analyzer_warnIfReached(); // expected-wrning{{REACHABLE}}
+  */
+
+  // The parent state is already infeasible, but we realize that only if b is
+  // constrained.
+  clang_analyzer_eval(b > 0);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(b <= 0); // expected-warning{{UNKNOWN}}
+  if (b > 0) {
+clang_analyzer_warnIfReached(); // no-warning
+return;
+  }
+  clang_analyzer_warnIfReached(); // no-warning
+}
Index: clang/lib/StaticAnalyzer/Core/ProgramState.cpp
===
--- clang/lib/StaticAnalyzer/Core/ProgramState.cpp
+++ clang/lib/StaticAnalyzer/Core/ProgramState.cpp
@@ -55,7 +55,7 @@
 
 ProgramState::ProgramState(const ProgramState )
 : stateMgr(RHS.stateMgr), Env(RHS.Env), store(RHS.store), GDM(RHS.GDM),
-  refCount(0) {
+  Infeasible(RHS.Infeasible), refCount(0) {
   stateMgr->getStoreManager().incrementReferenceCount(store);
 }
 
@@ -429,6 +429,12 @@
   return getStateManager().getPersistentState(NewSt);
 }
 
+ProgramStateRef ProgramState::cloneAsInfeasible() const {
+  ProgramState NewSt(*this);
+  NewSt.Infeasible = true;
+  return getStateManager().getPersistentState(NewSt);
+}
+
 void ProgramState::setStore(const StoreRef ) {
   Store newStoreStore = newStore.getStore();
   if (newStoreStore)
Index: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
===
--- clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@ -41,3 +41,32 @@
 return ConditionTruthVal(true);
   return {};
 }
+
+ConstraintManager::ProgramStatePair
+ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) {
+  ProgramStateRef StTrue = assume(State, Cond, true);
+
+  if (!StTrue) {
+ProgramStateRef StFalse = assume(State, Cond, false);
+if (!StFalse) { // both infeasible
+  ProgramStateRef StInfeasible = State->cloneAsInfeasible();
+  assert(StInfeasible->isInfeasible());
+  // Checkers might rely on the API contract that both returned states
+  // cannot be null. Thus, we return StInfeasible for both branches because
+  // it might happen 

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

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

steakhal added a comment.

I think I don't have anything left.
Let's see the numbers.




Comment at: clang/test/Analysis/sink-infeasible.c:37-48
+  /* The BASELINE passes these checks ('wrning' is used to avoid lit to match)
+  // The parent state is already infeasible, look at this contradiction:
+  clang_analyzer_eval(b > 0);  // expected-wrning{{FALSE}}
+  clang_analyzer_eval(b <= 0); // expected-wrning{{FALSE}}
+  // Crashes with expensive checks.
+  if (b > 0) {
+clang_analyzer_warnIfReached(); // no-warning, OK

martong wrote:
> steakhal wrote:
> > You could use a non-default check prefix.
> No I can't, because this test code in the comment is meaningful only in the 
> baseline, I cannot run both clang versions from lit.
> 
> So, actually there is no RUN line for these, it is here only to demonstrate 
> what happens in the baseline.
Okay, why don't we drop these if these are only applicable to the baseline?
Should we really introduce 'stale' comments?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

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

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

In D124674#3482765 , @steakhal wrote:

> Finally, we have this!

Thanks for the review.

> Can we have this https://godbolt.org/z/oferc6P5Y in addition to the one you 
> proposed?
> I find it more readable.

Sure, I find it also more readable. I will update soon.

> What performance hit will we suffer from this change?
> Please do a differential analysis.

I am doing that with the dependent patch https://reviews.llvm.org/D124758


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

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

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

martong added inline comments.



Comment at: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp:51
+ProgramStateRef StFalse = assume(State, Cond, false);
+if (!StFalse) { // both infeasible
+  ProgramStateRef Infeasible = State->cloneAsInfeasible();

steakhal wrote:
> Should we mark this `LLVM_UNLIKELY(cond)`?
> I would expect this function to be quite hot, and infeasible states rare.
> 
> Could we measure this one?
Yes, it could be.

Let me come back with some measurement results soon. I am going to use llvm 
statistics macros to measure this, but that makes sense on top of D124758



Comment at: clang/test/Analysis/sink-infeasible.c:37-48
+  /* The BASELINE passes these checks ('wrning' is used to avoid lit to match)
+  // The parent state is already infeasible, look at this contradiction:
+  clang_analyzer_eval(b > 0);  // expected-wrning{{FALSE}}
+  clang_analyzer_eval(b <= 0); // expected-wrning{{FALSE}}
+  // Crashes with expensive checks.
+  if (b > 0) {
+clang_analyzer_warnIfReached(); // no-warning, OK

steakhal wrote:
> You could use a non-default check prefix.
No I can't, because this test code in the comment is meaningful only in the 
baseline, I cannot run both clang versions from lit.

So, actually there is no RUN line for these, it is here only to demonstrate 
what happens in the baseline.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

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

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

martong updated this revision to Diff 426635.
martong marked 6 inline comments as done.
martong added a comment.

- Update according to review comments


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
  clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/ProgramState.cpp
  clang/test/Analysis/sink-infeasible.c

Index: clang/test/Analysis/sink-infeasible.c
===
--- /dev/null
+++ clang/test/Analysis/sink-infeasible.c
@@ -0,0 +1,59 @@
+// 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 that if it turns out that the parent state is infeasible then
+// both children States (more precisely the ExplodedNodes) are marked as a
+// Sink.
+// We rely on an existing defect of the underlying constraint solver. However,
+// in the future we might strengthen the solver to discover the infeasibility
+// right when we create the parent state. At that point this test will fail,
+// and either we shall find another solver weakness to have this test case
+// functioning, or we shall simply remove this test.
+
+void clang_analyzer_warnIfReached();
+void clang_analyzer_eval(int);
+
+int a, b, c, d, e;
+void f() {
+
+  if (a == 0)
+return;
+
+  if (e != c)
+return;
+
+  d = e - c;
+  b = d;
+  a -= d;
+
+  if (a != 0)
+return;
+
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+
+  /* The BASELINE passes these checks ('wrning' is used to avoid lit to match)
+  // The parent state is already infeasible, look at this contradiction:
+  clang_analyzer_eval(b > 0);  // expected-wrning{{FALSE}}
+  clang_analyzer_eval(b <= 0); // expected-wrning{{FALSE}}
+  // Crashes with expensive checks.
+  if (b > 0) {
+clang_analyzer_warnIfReached(); // no-warning, OK
+return;
+  }
+  // Should not be reachable.
+  clang_analyzer_warnIfReached(); // expected-wrning{{REACHABLE}}
+  */
+
+  // The parent state is already infeasible, but we realize that only if b is
+  // constrained.
+  clang_analyzer_eval(b > 0);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(b <= 0); // expected-warning{{UNKNOWN}}
+  if (b > 0) {
+clang_analyzer_warnIfReached(); // no-warning
+return;
+  }
+  clang_analyzer_warnIfReached(); // no-warning
+}
Index: clang/lib/StaticAnalyzer/Core/ProgramState.cpp
===
--- clang/lib/StaticAnalyzer/Core/ProgramState.cpp
+++ clang/lib/StaticAnalyzer/Core/ProgramState.cpp
@@ -55,7 +55,7 @@
 
 ProgramState::ProgramState(const ProgramState )
 : stateMgr(RHS.stateMgr), Env(RHS.Env), store(RHS.store), GDM(RHS.GDM),
-  refCount(0) {
+  Infeasible(RHS.Infeasible), refCount(0) {
   stateMgr->getStoreManager().incrementReferenceCount(store);
 }
 
@@ -429,6 +429,12 @@
   return getStateManager().getPersistentState(NewSt);
 }
 
+ProgramStateRef ProgramState::cloneAsInfeasible() const {
+  ProgramState NewSt(*this);
+  NewSt.Infeasible = true;
+  return getStateManager().getPersistentState(NewSt);
+}
+
 void ProgramState::setStore(const StoreRef ) {
   Store newStoreStore = newStore.getStore();
   if (newStoreStore)
Index: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
===
--- clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@ -41,3 +41,32 @@
 return ConditionTruthVal(true);
   return {};
 }
+
+ConstraintManager::ProgramStatePair
+ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) {
+  ProgramStateRef StTrue = assume(State, Cond, true);
+
+  if (!StTrue) {
+ProgramStateRef StFalse = assume(State, Cond, false);
+if (!StFalse) { // both infeasible
+  ProgramStateRef StInfeasible = State->cloneAsInfeasible();
+  assert(StInfeasible->isInfeasible());
+  // Checkers might rely on the API contract that both returned states
+  // cannot be null. Thus, we return StInfeasible for both branches because
+  // it might happen that a Checker uncoditionally uses one of them if the
+  // other is a nullptr. This may also happen with the non-dual and
+  // adjacent `assume(true)` and `assume(false)` calls. By implementing
+  // assume in therms of assumeDual, we can keep our API contract there as
+  // well.
+  return ProgramStatePair(StInfeasible, StInfeasible);
+}
+return ProgramStatePair(nullptr, StFalse);
+  }
+
+  ProgramStateRef StFalse = assume(State, Cond, false);

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

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

steakhal added a comment.

Finally, we have this!

Can we have this https://godbolt.org/z/oferc6P5Y in addition to the one you 
proposed?
I find it more readable.

What performance hit will we suffer from this change?
Please do a differential analysis.




Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:93
   /// assumed to be true or false, respectively.
-  ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond) {
-ProgramStateRef StTrue = assume(State, Cond, true);
-
-// If StTrue is infeasible, asserting the falseness of Cond is unnecessary
-// because the existing constraints already establish this.
-if (!StTrue) {
-#ifdef EXPENSIVE_CHECKS
-  assert(assume(State, Cond, false) && "System is over constrained.");
-#endif
-  return ProgramStatePair((ProgramStateRef)nullptr, State);
-}
-
-ProgramStateRef StFalse = assume(State, Cond, false);
-if (!StFalse) {
-  // We are careful to return the original state, /not/ StTrue,
-  // because we want to avoid having callers generate a new node
-  // in the ExplodedGraph.
-  return ProgramStatePair(State, (ProgramStateRef)nullptr);
-}
-
-return ProgramStatePair(StTrue, StFalse);
-  }
+  ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond);
 

I would leave a note here that these two states might be equal in a very rare 
case (*); but one should not depend on that.



Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h:293
  ExplodedNode *Pred) {
-return generateNodeImpl(PP, State, Pred, false);
+return generateNodeImpl(PP, State, Pred, State->isInfeasible());
   }





Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:86
   GenericDataMap   GDM;  // Custom data stored by a client of this class.
+  bool Infeasible = false;
   unsigned refCount;

For the record, back then we had such flag. IDK when did we remove it, but we 
had it for sure.



Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:113-115
+  ProgramStateRef cloneAsInfeasible() const;
+  bool isInfeasible() const { return Infeasible; }
+

These should not be public. Make friends if required.



Comment at: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp:51
+ProgramStateRef StFalse = assume(State, Cond, false);
+if (!StFalse) { // both infeasible
+  ProgramStateRef Infeasible = State->cloneAsInfeasible();

Should we mark this `LLVM_UNLIKELY(cond)`?
I would expect this function to be quite hot, and infeasible states rare.

Could we measure this one?



Comment at: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp:52-54
+  ProgramStateRef Infeasible = State->cloneAsInfeasible();
+  assert(Infeasible->isInfeasible());
+  return ProgramStatePair(Infeasible, Infeasible);

Add here some comments on why we return (`Infeasible`,`Infeasible`).
I would rather see `StInfeasible` to better discriminate what we are talking 
about. We already use `StTrue` and `StFalse` in this context though.



Comment at: clang/test/Analysis/sink-infeasible.c:37-48
+  /* The BASELINE passes these checks ('wrning' is used to avoid lit to match)
+  // The parent state is already infeasible, look at this contradiction:
+  clang_analyzer_eval(b > 0);  // expected-wrning{{FALSE}}
+  clang_analyzer_eval(b <= 0); // expected-wrning{{FALSE}}
+  // Crashes with expensive checks.
+  if (b > 0) {
+clang_analyzer_warnIfReached(); // no-warning, OK

You could use a non-default check prefix.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

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

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

martong added inline comments.



Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:96-97
-
-// If StTrue is infeasible, asserting the falseness of Cond is unnecessary
-// because the existing constraints already establish this.
-if (!StTrue) {

This statement is false because our constraint solver is not precise.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124674

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

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

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

In some cases a parent State is already infeasible, but we recognize
this only if an additonal constraint is added. This patch is the first
of a series to address this issue. In this patch `assumeDual` is changed
to clone the parent State but with an `Infeasible` flag set, and this
infeasible-parent is returned both for the true and false case. Then
when we add a new transition in the exploded graph and the destination
is marked as infeasible, the node will be a sink node.

Related bug:
https://github.com/llvm/llvm-project/issues/50883
Actually, this patch does not solve that bug in the solver, rather with
this patch we can handle the general parent-infeasible cases.

Next step would be to change the State API and require all checkers to
use the `assume*Dual` API and deprecate the simple `assume` calls.

Hopefully, the next patch will introduce `assumeInBoundDual` and will
solve the CRASH we have here:
https://github.com/llvm/llvm-project/issues/54272


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D124674

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
  clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/ProgramState.cpp
  clang/test/Analysis/sink-infeasible.c

Index: clang/test/Analysis/sink-infeasible.c
===
--- /dev/null
+++ clang/test/Analysis/sink-infeasible.c
@@ -0,0 +1,59 @@
+// 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 that if it turns out that the parent state is infeasible then
+// both children States (more precisely the ExplodedNodes) are marked as a
+// Sink.
+// We rely on an existing defect of the underlying constraint solver. However,
+// in the future we might strengthen the solver to discover the infeasibility
+// right when we create the parent state. At that point this test will fail,
+// and either we shall find another solver weakness to have this test case
+// functioning, or we shall simply remove this test.
+
+void clang_analyzer_warnIfReached();
+void clang_analyzer_eval(int);
+
+int a, b, c, d, e;
+void f() {
+
+  if (a == 0)
+return;
+
+  if (e != c)
+return;
+
+  d = e - c;
+  b = d;
+  a -= d;
+
+  if (a != 0)
+return;
+
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+
+  /* The BASELINE passes these checks ('wrning' is used to avoid lit to match)
+  // The parent state is already infeasible, look at this contradiction:
+  clang_analyzer_eval(b > 0);  // expected-wrning{{FALSE}}
+  clang_analyzer_eval(b <= 0); // expected-wrning{{FALSE}}
+  // Crashes with expensive checks.
+  if (b > 0) {
+clang_analyzer_warnIfReached(); // no-warning, OK
+return;
+  }
+  // Should not be reachable.
+  clang_analyzer_warnIfReached(); // expected-wrning{{REACHABLE}}
+  */
+
+  // The parent state is already infeasible, but we realize that only if b is
+  // constrained.
+  clang_analyzer_eval(b > 0);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(b <= 0); // expected-warning{{UNKNOWN}}
+  if (b > 0) {
+clang_analyzer_warnIfReached(); // no-warning
+return;
+  }
+  clang_analyzer_warnIfReached(); // no-warning
+}
Index: clang/lib/StaticAnalyzer/Core/ProgramState.cpp
===
--- clang/lib/StaticAnalyzer/Core/ProgramState.cpp
+++ clang/lib/StaticAnalyzer/Core/ProgramState.cpp
@@ -55,7 +55,7 @@
 
 ProgramState::ProgramState(const ProgramState )
 : stateMgr(RHS.stateMgr), Env(RHS.Env), store(RHS.store), GDM(RHS.GDM),
-  refCount(0) {
+  Infeasible(RHS.Infeasible), refCount(0) {
   stateMgr->getStoreManager().incrementReferenceCount(store);
 }
 
@@ -429,6 +429,12 @@
   return getStateManager().getPersistentState(NewSt);
 }
 
+ProgramStateRef ProgramState::cloneAsInfeasible() const {
+  ProgramState NewSt(*this);
+  NewSt.Infeasible = true;
+  return getStateManager().getPersistentState(NewSt);
+}
+
 void ProgramState::setStore(const StoreRef ) {
   Store newStoreStore = newStore.getStore();
   if (newStoreStore)
Index: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
===
--- clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@