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

llvm-svn: 167195

1 files changed, 24 insertions, 6 deletions

diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
index 6f1e70bdfd5a..34779e875c0d 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -69,12 +69,30 @@ public:
                                  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