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 &RHS)
: 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 &newStore) {
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,25 @@
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 Infeasible = State->cloneAsInfeasible();
+ assert(Infeasible->isInfeasible());
+ return ProgramStatePair(Infeasible, Infeasible);
+ }
+ return ProgramStatePair(nullptr, StFalse);
+ }
+
+ ProgramStateRef StFalse = assume(State, Cond, false);
+ if (!StFalse) {
+ return ProgramStatePair(StTrue, nullptr);
+ }
+
+ return ProgramStatePair(StTrue, StFalse);
+}
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
@@ -83,6 +83,7 @@
Environment Env; // Maps a Stmt to its current SVal.
Store store; // Maps a location to its current value.
GenericDataMap GDM; // Custom data stored by a client of this class.
+ bool Infeasible = false;
unsigned refCount;
/// makeWithStore - Return a ProgramState with the same values as the current
@@ -109,6 +110,9 @@
return *stateMgr;
}
+ ProgramStateRef cloneAsInfeasible() const;
+ bool isInfeasible() const { return Infeasible; }
+
AnalysisManager &getAnalysisManager() const;
/// Return the ConstraintManager.
@@ -135,6 +139,7 @@
V->Env.Profile(ID);
ID.AddPointer(V->store);
V->GDM.Profile(ID);
+ ID.AddBoolean(V->Infeasible);
}
/// Profile - Used to profile the contents of this object for inclusion
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
@@ -290,7 +290,7 @@
ExplodedNode *generateNode(const ProgramPoint &PP,
ProgramStateRef State,
ExplodedNode *Pred) {
- return generateNodeImpl(PP, State, Pred, false);
+ return generateNodeImpl(PP, State, Pred, State->isInfeasible());
}
/// Generates a sink in the ExplodedGraph.
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -90,28 +90,7 @@
/// Returns a pair of states (StTrue, StFalse) where the given condition is
/// 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);
virtual ProgramStateRef assumeInclusiveRange(ProgramStateRef State,
NonLoc Value,
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
