[analyzer] Optimize assumeDual by assuming constraint managers are consistent.
Specifically, if adding a constraint makes the current system infeasible,
assume the constraint is false, instead of attempting to add its negation.
In +Asserts builds we will still assert that at least one state is feasible.
Patch by Ryan Govostes!
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@167195 91177308-0d34-0410-b5e6-96231b3b80d8
diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
index 6f1e70b..34779e8 100644
--- a/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ b/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -69,12 +69,30 @@
bool Assumption) = 0;
typedef std::pair<ProgramStateRef, ProgramStateRef> ProgramStatePair;
-
- ProgramStatePair assumeDual(ProgramStateRef state, DefinedSVal Cond) {
- ProgramStatePair res(assume(state, Cond, true),
- assume(state, Cond, false));
- assert(!(!res.first && !res.second) && "System is over constrained.");
- return res;
+
+ /// 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) {
+ // FIXME: This is fairly expensive and should be disabled even in
+ // Release+Asserts builds.
+ assert(assume(State, Cond, false) && "System is over constrained.");
+ return ProgramStatePair(NULL, 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, NULL);
+ }
+
+ return ProgramStatePair(StTrue, StFalse);
}
/// \brief If a symbol is perfectly constrained to a constant, attempt
