[cfe-commits] r167195 - /cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h

[Jordan Rose]

Author: jrose
Date: Wed Oct 31 20:05:39 2012
New Revision: 167195

URL: http://llvm.org/viewvc/llvm-project?rev=167195&view=rev
Log:
[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!

Modified:
    cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h

Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h?rev=167195&r1=167194&r2=167195&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h Wed Oct 31 20:05:39 2012
@@ -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