/// 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);
- }
+ /// (Note that these two states might be equal if the parent state turns out
+ /// to be infeasible. This may happen if the underlying constraint solver is
+ /// not perfectly precise and this may happen very rarely.)
+ ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond);
virtual ProgramStateRef assumeInclusiveRange(ProgramStateRef State,
NonLoc Value,
ExplodedNode *generateNode(const ProgramPoint &PP,
ProgramStateRef State,
ExplodedNode *Pred) {
- return generateNodeImpl(PP, State, Pred, false);
+ return generateNodeImpl(
+ PP, State, Pred,
+ /*MarkAsSink=*/State->isPosteriorlyOverconstrained());
}
/// Generates a sink in the ExplodedGraph.
friend class ProgramStateManager;
friend class ExplodedGraph;
friend class ExplodedNode;
+ friend class NodeBuilder;
+ friend class ConstraintManager;
ProgramStateManager *stateMgr;
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.
+
+ // 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 realized that at the moment when we have created it. However, we
+ // could not recognize that because of the imperfection of the underlying
+ // constraint solver. We say it is posteriorly over-constrained because we
+ // recognize that a parent is infeasible only *after* a new and more specific
+ // constraint and its negation are evaluated.
+ //
+ // Example:
+ //
+ // x * x = 4 and x is in the range [0, 1]
+ // This is an already infeasible state, but the constraint solver is not
+ // capable of handling sqrt, thus we don't know it yet.
+ //
+ // Then a new constraint `x = 0` is added. At this moment the constraint
+ // solver re-evaluates the existing constraints and realizes the
+ // contradiction `0 * 0 = 4`.
+ // We also evaluate the negated constraint `x != 0`; the constraint solver
+ // deduces `x = 1` and then realizes the contradiction `1 * 1 = 4`.
+ // Both children are infeasible, thus the parent state is marked as
+ // posteriorly over-constrained. These parents are handled with special care:
+ // we do not allow transitions to exploded nodes with such states.
+ bool PosteriorlyOverconstrained = false;
+
unsigned refCount;
/// makeWithStore - Return a ProgramState with the same values as the current
void setStore(const StoreRef &storeRef);
+ ProgramStateRef cloneAsPosteriorlyOverconstrained() const;
+ bool isPosteriorlyOverconstrained() const {
+ return PosteriorlyOverconstrained;
+ }
+
public:
/// This ctor is used when creating the first ProgramState object.
ProgramState(ProgramStateManager *mgr, const Environment& env,
V->Env.Profile(ID);
ID.AddPointer(V->store);
V->GDM.Profile(ID);
+ ID.AddBoolean(V->PosteriorlyOverconstrained);
}
/// Profile - Used to profile the contents of this object for inclusion
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 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);
+ if (!StFalse) {
+ return ProgramStatePair(StTrue, nullptr);
+ }
+
+ return ProgramStatePair(StTrue, StFalse);
+}
ProgramState::ProgramState(const ProgramState &RHS)
: stateMgr(RHS.stateMgr), Env(RHS.Env), store(RHS.store), GDM(RHS.GDM),
- refCount(0) {
+ PosteriorlyOverconstrained(RHS.PosteriorlyOverconstrained), refCount(0) {
stateMgr->getStoreManager().incrementReferenceCount(store);
}
return getStateManager().getPersistentState(NewSt);
}
+ProgramStateRef ProgramState::cloneAsPosteriorlyOverconstrained() const {
+ ProgramState NewSt(*this);
+ NewSt.PosteriorlyOverconstrained = true;
+ return getStateManager().getPersistentState(NewSt);
+}
+
void ProgramState::setStore(const StoreRef &newStore) {
Store newStoreStore = newStore.getStore();
if (newStoreStore)
--- /dev/null
+// 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
+}