[analyzer] The result of && or || is always a 1 or 0.

Forgetting to at least cast the result was giving us Loc/NonLoc problems
in SValBuilder (hitting an assertion). But the standard (both C and C++)
does actually guarantee that && and || will result in the actual values
1 and 0, typed as 'int' in C and 'bool' in C++, and we can easily model that.

PR13461

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@162209 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 20 insertions, 2 deletions

diff --git a/lib/StaticAnalyzer/Core/ExprEngineC.cpp b/lib/StaticAnalyzer/Core/ExprEngineC.cpp
index 46cba81b14..3e14765875 100644
--- a/lib/StaticAnalyzer/Core/ExprEngineC.cpp
+++ b/lib/StaticAnalyzer/Core/ExprEngineC.cpp
@@ -531,10 +531,28 @@ void ExprEngine::VisitLogicalExpr(const BinaryOperator* B, ExplodedNode *Pred,
   else {
     // If there is no terminator, by construction the last statement
     // in SrcBlock is the value of the enclosing expression.
+    // However, we still need to constrain that value to be 0 or 1.
     assert(!SrcBlock->empty());
     CFGStmt Elem = cast<CFGStmt>(*SrcBlock->rbegin());
-    const Stmt *S = Elem.getStmt();
-    X = N->getState()->getSVal(S, Pred->getLocationContext());
+    const Expr *RHS = cast<Expr>(Elem.getStmt());
+    SVal RHSVal = N->getState()->getSVal(RHS, Pred->getLocationContext());
+
+    DefinedOrUnknownSVal DefinedRHS = cast<DefinedOrUnknownSVal>(RHSVal);
+    ProgramStateRef StTrue, StFalse;
+    llvm::tie(StTrue, StFalse) = N->getState()->assume(DefinedRHS);
+    if (StTrue) {
+      if (StFalse) {
+        // We can't constrain the value to 0 or 1; the best we can do is a cast.
+        X = getSValBuilder().evalCast(RHSVal, B->getType(), RHS->getType());
+      } else {
+        // The value is known to be true.
+        X = getSValBuilder().makeIntVal(1, B->getType());
+      }
+    } else {
+      // The value is known to be false.
+      assert(StFalse && "Infeasible path!");
+      X = getSValBuilder().makeIntVal(0, B->getType());
+    }
   }
 
   Bldr.generateNode(B, Pred, state->BindExpr(B, Pred->getLocationContext(), X));