vendor/clang/clang-trunk-r300422

21 files changed, 2317 insertions, 434 deletions

diff --git a/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp b/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
index 15422633ba33c..45ef612ee1d58 100644
--- a/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
+++ b/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
@@ -230,7 +230,7 @@ bool AnalyzerOptions::shouldSuppressInlinedDefensiveChecks() {
 bool AnalyzerOptions::shouldSuppressFromCXXStandardLibrary() {
   return getBooleanOption(SuppressFromCXXStandardLibrary,
                           "suppress-c++-stdlib",
-                          /* Default = */ false);
+                          /* Default = */ true);
 }
 
 bool AnalyzerOptions::shouldReportIssuesInMainSourceFile() {
diff --git a/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp b/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
index c3c3f2ff76ecf..7309741d22e39 100644
--- a/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ b/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -1027,7 +1027,7 @@ bool bugreporter::trackNullOrUndefValue(const ExplodedNode *N,
       R = LVState->getSVal(Inner, LVNode->getLocationContext()).getAsRegion();
 
       // If this is a C++ reference to a null pointer, we are tracking the
-      // pointer. In additon, we should find the store at which the reference
+      // pointer. In addition, we should find the store at which the reference
       // got initialized.
       if (const MemRegion *RR = getLocationRegionIfReference(Inner, N)) {
         if (Optional<KnownSVal> KV = LVal.getAs<KnownSVal>())
@@ -1290,7 +1290,7 @@ std::shared_ptr<PathDiagnosticPiece> ConditionBRVisitor::VisitTerminator(
     break;
   case Stmt::BinaryOperatorClass:
     // When we encounter a logical operator (&& or ||) as a CFG terminator,
-    // then the condition is actually its LHS; otheriwse, we'd encounter
+    // then the condition is actually its LHS; otherwise, we'd encounter
     // the parent, such as if-statement, as a terminator.
     const auto *BO = cast<BinaryOperator>(Term);
     assert(BO->isLogicalOp() &&
@@ -1659,7 +1659,7 @@ LikelyFalsePositiveSuppressionBRVisitor::getEndPath(BugReporterContext &BRC,
 
       // The analyzer issues a false use-after-free when std::list::pop_front
       // or std::list::pop_back are called multiple times because we cannot
-      // reason about the internal invariants of the datastructure.
+      // reason about the internal invariants of the data structure.
       if (const CXXMethodDecl *MD = dyn_cast<CXXMethodDecl>(D)) {
         const CXXRecordDecl *CD = MD->getParent();
         if (CD->getName() == "list") {
@@ -1690,7 +1690,7 @@ LikelyFalsePositiveSuppressionBRVisitor::getEndPath(BugReporterContext &BRC,
         // and
         //   std::u16string s; s += u'a';
         // because we cannot reason about the internal invariants of the
-        // datastructure.
+        // data structure.
         if (CD->getName() == "basic_string") {
           BR.markInvalid(getTag(), nullptr);
           return nullptr;
diff --git a/lib/StaticAnalyzer/Core/CMakeLists.txt b/lib/StaticAnalyzer/Core/CMakeLists.txt
index aaffb0b82ce00..85878f5e96ee7 100644
--- a/lib/StaticAnalyzer/Core/CMakeLists.txt
+++ b/lib/StaticAnalyzer/Core/CMakeLists.txt
@@ -1,5 +1,12 @@
 set(LLVM_LINK_COMPONENTS support)
 
+# Link Z3 if the user wants to build it.
+if(CLANG_ANALYZER_WITH_Z3)
+  set(Z3_LINK_FILES ${Z3_LIBRARIES})
+else()
+  set(Z3_LINK_FILES "")
+endif()
+
 add_clang_library(clangStaticAnalyzerCore
   APSIntType.cpp
   AnalysisManager.cpp
@@ -34,6 +41,7 @@ add_clang_library(clangStaticAnalyzerCore
   PlistDiagnostics.cpp
   ProgramState.cpp
   RangeConstraintManager.cpp
+  RangedConstraintManager.cpp
   RegionStore.cpp
   SValBuilder.cpp
   SVals.cpp
@@ -42,6 +50,7 @@ add_clang_library(clangStaticAnalyzerCore
   Store.cpp
   SubEngine.cpp
   SymbolManager.cpp
+  Z3ConstraintManager.cpp
 
   LINK_LIBS
   clangAST
@@ -49,4 +58,12 @@ add_clang_library(clangStaticAnalyzerCore
   clangBasic
   clangLex
   clangRewrite
+  ${Z3_LINK_FILES}
   )
+
+if(CLANG_ANALYZER_WITH_Z3)
+  target_include_directories(clangStaticAnalyzerCore SYSTEM
+    PRIVATE
+    ${Z3_INCLUDE_DIR}
+    )
+endif()
diff --git a/lib/StaticAnalyzer/Core/CallEvent.cpp b/lib/StaticAnalyzer/Core/CallEvent.cpp
index 420e2a6b5c8c2..ee761689f479b 100644
--- a/lib/StaticAnalyzer/Core/CallEvent.cpp
+++ b/lib/StaticAnalyzer/Core/CallEvent.cpp
@@ -212,9 +212,12 @@ ProgramPoint CallEvent::getProgramPoint(bool IsPreVisit,
 
 bool CallEvent::isCalled(const CallDescription &CD) const {
   assert(getKind() != CE_ObjCMessage && "Obj-C methods are not supported");
-  if (!CD.II)
+  if (!CD.IsLookupDone) {
+    CD.IsLookupDone = true;
     CD.II = &getState()->getStateManager().getContext().Idents.get(CD.FuncName);
-  if (getCalleeIdentifier() != CD.II)
+  }
+  const IdentifierInfo *II = getCalleeIdentifier();
+  if (!II || II != CD.II)
     return false;
   return (CD.RequiredArgs == CallDescription::NoArgRequirement ||
           CD.RequiredArgs == getNumArgs());
@@ -692,13 +695,15 @@ void ObjCMethodCall::getExtraInvalidatedValues(
   if (const ObjCPropertyDecl *PropDecl = getAccessedProperty()) {
     if (const ObjCIvarDecl *PropIvar = PropDecl->getPropertyIvarDecl()) {
       SVal IvarLVal = getState()->getLValue(PropIvar, getReceiverSVal());
-      const MemRegion *IvarRegion = IvarLVal.getAsRegion();
-      ETraits->setTrait(
+      if (const MemRegion *IvarRegion = IvarLVal.getAsRegion()) {
+        ETraits->setTrait(
           IvarRegion,
           RegionAndSymbolInvalidationTraits::TK_DoNotInvalidateSuperRegion);
-      ETraits->setTrait(IvarRegion,
-                        RegionAndSymbolInvalidationTraits::TK_SuppressEscape);
-      Values.push_back(IvarLVal);
+        ETraits->setTrait(
+          IvarRegion,
+          RegionAndSymbolInvalidationTraits::TK_SuppressEscape);
+        Values.push_back(IvarLVal);
+      }
       return;
     }
   }
@@ -896,6 +901,38 @@ bool ObjCMethodCall::canBeOverridenInSubclass(ObjCInterfaceDecl *IDecl,
   llvm_unreachable("The while loop should always terminate.");
 }
 
+static const ObjCMethodDecl *findDefiningRedecl(const ObjCMethodDecl *MD) {
+  if (!MD)
+    return MD;
+
+  // Find the redeclaration that defines the method.
+  if (!MD->hasBody()) {
+    for (auto I : MD->redecls())
+      if (I->hasBody())
+        MD = cast<ObjCMethodDecl>(I);
+  }
+  return MD;
+}
+
+static bool isCallToSelfClass(const ObjCMessageExpr *ME) {
+  const Expr* InstRec = ME->getInstanceReceiver();
+  if (!InstRec)
+    return false;
+  const auto *InstRecIg = dyn_cast<DeclRefExpr>(InstRec->IgnoreParenImpCasts());
+
+  // Check that receiver is called 'self'.
+  if (!InstRecIg || !InstRecIg->getFoundDecl() ||
+      !InstRecIg->getFoundDecl()->getName().equals("self"))
+    return false;
+
+  // Check that the method name is 'class'.
+  if (ME->getSelector().getNumArgs() != 0 ||
+      !ME->getSelector().getNameForSlot(0).equals("class"))
+    return false;
+
+  return true;
+}
+
 RuntimeDefinition ObjCMethodCall::getRuntimeDefinition() const {
   const ObjCMessageExpr *E = getOriginExpr();
   assert(E);
@@ -910,6 +947,7 @@ RuntimeDefinition ObjCMethodCall::getRuntimeDefinition() const {
     const MemRegion *Receiver = nullptr;
 
     if (!SupersType.isNull()) {
+      // The receiver is guaranteed to be 'super' in this case.
       // Super always means the type of immediate predecessor to the method
       // where the call occurs.
       ReceiverT = cast<ObjCObjectPointerType>(SupersType);
@@ -921,7 +959,7 @@ RuntimeDefinition ObjCMethodCall::getRuntimeDefinition() const {
       DynamicTypeInfo DTI = getDynamicTypeInfo(getState(), Receiver);
       QualType DynType = DTI.getType();
       CanBeSubClassed = DTI.canBeASubClass();
-      ReceiverT = dyn_cast<ObjCObjectPointerType>(DynType);
+      ReceiverT = dyn_cast<ObjCObjectPointerType>(DynType.getCanonicalType());
 
       if (ReceiverT && CanBeSubClassed)
         if (ObjCInterfaceDecl *IDecl = ReceiverT->getInterfaceDecl())
@@ -929,7 +967,32 @@ RuntimeDefinition ObjCMethodCall::getRuntimeDefinition() const {
             CanBeSubClassed = false;
     }
 
-    // Lookup the method implementation.
+    // Handle special cases of '[self classMethod]' and
+    // '[[self class] classMethod]', which are treated by the compiler as
+    // instance (not class) messages. We will statically dispatch to those.
+    if (auto *PT = dyn_cast_or_null<ObjCObjectPointerType>(ReceiverT)) {
+      // For [self classMethod], return the compiler visible declaration.
+      if (PT->getObjectType()->isObjCClass() &&
+          Receiver == getSelfSVal().getAsRegion())
+        return RuntimeDefinition(findDefiningRedecl(E->getMethodDecl()));
+
+      // Similarly, handle [[self class] classMethod].
+      // TODO: We are currently doing a syntactic match for this pattern with is
+      // limiting as the test cases in Analysis/inlining/InlineObjCClassMethod.m
+      // shows. A better way would be to associate the meta type with the symbol
+      // using the dynamic type info tracking and use it here. We can add a new
+      // SVal for ObjC 'Class' values that know what interface declaration they
+      // come from. Then 'self' in a class method would be filled in with
+      // something meaningful in ObjCMethodCall::getReceiverSVal() and we could
+      // do proper dynamic dispatch for class methods just like we do for
+      // instance methods now.
+      if (E->getInstanceReceiver())
+        if (const auto *M = dyn_cast<ObjCMessageExpr>(E->getInstanceReceiver()))
+          if (isCallToSelfClass(M))
+            return RuntimeDefinition(findDefiningRedecl(E->getMethodDecl()));
+    }
+
+    // Lookup the instance method implementation.
     if (ReceiverT)
       if (ObjCInterfaceDecl *IDecl = ReceiverT->getInterfaceDecl()) {
         // Repeatedly calling lookupPrivateMethod() is expensive, especially
diff --git a/lib/StaticAnalyzer/Core/CheckerManager.cpp b/lib/StaticAnalyzer/Core/CheckerManager.cpp
index 79e204cdafec9..49f3edef2a2d3 100644
--- a/lib/StaticAnalyzer/Core/CheckerManager.cpp
+++ b/lib/StaticAnalyzer/Core/CheckerManager.cpp
@@ -521,17 +521,19 @@ void CheckerManager::runCheckersForDeadSymbols(ExplodedNodeSet &Dst,
 /// \brief Run checkers for region changes.
 ProgramStateRef
 CheckerManager::runCheckersForRegionChanges(ProgramStateRef state,
-                                    const InvalidatedSymbols *invalidated,
-                                    ArrayRef<const MemRegion *> ExplicitRegions,
-                                    ArrayRef<const MemRegion *> Regions,
-                                    const CallEvent *Call) {
+                                            const InvalidatedSymbols *invalidated,
+                                            ArrayRef<const MemRegion *> ExplicitRegions,
+                                            ArrayRef<const MemRegion *> Regions,
+                                            const LocationContext *LCtx,
+                                            const CallEvent *Call) {
   for (unsigned i = 0, e = RegionChangesCheckers.size(); i != e; ++i) {
     // If any checker declares the state infeasible (or if it starts that way),
     // bail out.
     if (!state)
       return nullptr;
     state = RegionChangesCheckers[i](state, invalidated,
-                                     ExplicitRegions, Regions, Call);
+                                     ExplicitRegions, Regions,
+                                     LCtx, Call);
   }
   return state;
 }
diff --git a/lib/StaticAnalyzer/Core/ConstraintManager.cpp b/lib/StaticAnalyzer/Core/ConstraintManager.cpp
index b7db8333aaac6..8de2b0e8d271d 100644
--- a/lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@ -20,8 +20,8 @@ ConstraintManager::~ConstraintManager() {}
 
 static DefinedSVal getLocFromSymbol(const ProgramStateRef &State,
                                     SymbolRef Sym) {
-  const MemRegion *R = State->getStateManager().getRegionManager()
-                                               .getSymbolicRegion(Sym);
+  const MemRegion *R =
+      State->getStateManager().getRegionManager().getSymbolicRegion(Sym);
   return loc::MemRegionVal(R);
 }
 
diff --git a/lib/StaticAnalyzer/Core/DynamicTypeMap.cpp b/lib/StaticAnalyzer/Core/DynamicTypeMap.cpp
index fd35b664a9127..a01ff36a8aae0 100644
--- a/lib/StaticAnalyzer/Core/DynamicTypeMap.cpp
+++ b/lib/StaticAnalyzer/Core/DynamicTypeMap.cpp
@@ -8,7 +8,7 @@
 //===----------------------------------------------------------------------===//
 //
 //  This file defines APIs that track and query dynamic type information. This
-//  information can be used to devirtualize calls during the symbolic exection
+//  information can be used to devirtualize calls during the symbolic execution
 //  or do type checking.
 //
 //===----------------------------------------------------------------------===//
diff --git a/lib/StaticAnalyzer/Core/ExprEngine.cpp b/lib/StaticAnalyzer/Core/ExprEngine.cpp
index d563f8e9eac02..9e6ec09010e91 100644
--- a/lib/StaticAnalyzer/Core/ExprEngine.cpp
+++ b/lib/StaticAnalyzer/Core/ExprEngine.cpp
@@ -182,19 +182,25 @@ ProgramStateRef ExprEngine::getInitialState(const LocationContext *InitLoc) {
 ProgramStateRef
 ExprEngine::createTemporaryRegionIfNeeded(ProgramStateRef State,
                                           const LocationContext *LC,
-                                          const Expr *Ex,
+                                          const Expr *InitWithAdjustments,
                                           const Expr *Result) {
-  SVal V = State->getSVal(Ex, LC);
+  // FIXME: This function is a hack that works around the quirky AST
+  // we're often having with respect to C++ temporaries. If only we modelled
+  // the actual execution order of statements properly in the CFG,
+  // all the hassle with adjustments would not be necessary,
+  // and perhaps the whole function would be removed.
+  SVal InitValWithAdjustments = State->getSVal(InitWithAdjustments, LC);
   if (!Result) {
     // If we don't have an explicit result expression, we're in "if needed"
     // mode. Only create a region if the current value is a NonLoc.
-    if (!V.getAs<NonLoc>())
+    if (!InitValWithAdjustments.getAs<NonLoc>())
       return State;
-    Result = Ex;
+    Result = InitWithAdjustments;
   } else {
     // We need to create a region no matter what. For sanity, make sure we don't
     // try to stuff a Loc into a non-pointer temporary region.
-    assert(!V.getAs<Loc>() || Loc::isLocType(Result->getType()) ||
+    assert(!InitValWithAdjustments.getAs<Loc>() ||
+           Loc::isLocType(Result->getType()) ||
            Result->getType()->isMemberPointerType());
   }
 
@@ -226,7 +232,8 @@ ExprEngine::createTemporaryRegionIfNeeded(ProgramStateRef State,
   SmallVector<const Expr *, 2> CommaLHSs;
   SmallVector<SubobjectAdjustment, 2> Adjustments;
 
-  const Expr *Init = Ex->skipRValueSubobjectAdjustments(CommaLHSs, Adjustments);
+  const Expr *Init = InitWithAdjustments->skipRValueSubobjectAdjustments(
+      CommaLHSs, Adjustments);
 
   const TypedValueRegion *TR = nullptr;
   if (const MaterializeTemporaryExpr *MT =
@@ -241,6 +248,7 @@ ExprEngine::createTemporaryRegionIfNeeded(ProgramStateRef State,
     TR = MRMgr.getCXXTempObjectRegion(Init, LC);
 
   SVal Reg = loc::MemRegionVal(TR);
+  SVal BaseReg = Reg;
 
   // Make the necessary adjustments to obtain the sub-object.
   for (auto I = Adjustments.rbegin(), E = Adjustments.rend(); I != E; ++I) {
@@ -254,19 +262,47 @@ ExprEngine::createTemporaryRegionIfNeeded(ProgramStateRef State,
       break;
     case SubobjectAdjustment::MemberPointerAdjustment:
       // FIXME: Unimplemented.
-      State->bindDefault(Reg, UnknownVal());
+      State = State->bindDefault(Reg, UnknownVal(), LC);
       return State;
     }
   }
 
-  // Try to recover some path sensitivity in case we couldn't compute the value.
-  if (V.isUnknown())
-    V = getSValBuilder().conjureSymbolVal(Result, LC, TR->getValueType(),
-                                          currBldrCtx->blockCount());
-  // Bind the value of the expression to the sub-object region, and then bind
-  // the sub-object region to our expression.
-  State = State->bindLoc(Reg, V);
+  // What remains is to copy the value of the object to the new region.
+  // FIXME: In other words, what we should always do is copy value of the
+  // Init expression (which corresponds to the bigger object) to the whole
+  // temporary region TR. However, this value is often no longer present
+  // in the Environment. If it has disappeared, we instead invalidate TR.
+  // Still, what we can do is assign the value of expression Ex (which
+  // corresponds to the sub-object) to the TR's sub-region Reg. At least,
+  // values inside Reg would be correct.
+  SVal InitVal = State->getSVal(Init, LC);
+  if (InitVal.isUnknown()) {
+    InitVal = getSValBuilder().conjureSymbolVal(Result, LC, Init->getType(),
+                                                currBldrCtx->blockCount());
+    State = State->bindLoc(BaseReg.castAs<Loc>(), InitVal, LC, false);
+
+    // Then we'd need to take the value that certainly exists and bind it over.
+    if (InitValWithAdjustments.isUnknown()) {
+      // Try to recover some path sensitivity in case we couldn't
+      // compute the value.
+      InitValWithAdjustments = getSValBuilder().conjureSymbolVal(
+          Result, LC, InitWithAdjustments->getType(),
+          currBldrCtx->blockCount());
+    }
+    State =
+        State->bindLoc(Reg.castAs<Loc>(), InitValWithAdjustments, LC, false);
+  } else {
+    State = State->bindLoc(BaseReg.castAs<Loc>(), InitVal, LC, false);
+  }
+
+  // The result expression would now point to the correct sub-region of the
+  // newly created temporary region. Do this last in order to getSVal of Init
+  // correctly in case (Result == Init).
   State = State->BindExpr(Result, LC, Reg);
+
+  // Notify checkers once for two bindLoc()s.
+  State = processRegionChange(State, TR, LC);
+
   return State;
 }
 
@@ -286,9 +322,11 @@ ExprEngine::processRegionChanges(ProgramStateRef state,
                                  const InvalidatedSymbols *invalidated,
                                  ArrayRef<const MemRegion *> Explicits,
                                  ArrayRef<const MemRegion *> Regions,
+                                 const LocationContext *LCtx,
                                  const CallEvent *Call) {
   return getCheckerManager().runCheckersForRegionChanges(state, invalidated,
-                                                      Explicits, Regions, Call);
+                                                         Explicits, Regions,
+                                                         LCtx, Call);
 }
 
 void ExprEngine::printState(raw_ostream &Out, ProgramStateRef State,
@@ -613,7 +651,15 @@ void ExprEngine::ProcessAutomaticObjDtor(const CFGAutomaticObjDtor Dtor,
   const MemRegion *Region = dest.castAs<loc::MemRegionVal>().getRegion();
 
   if (varType->isReferenceType()) {
-    Region = state->getSVal(Region).getAsRegion()->getBaseRegion();
+    const MemRegion *ValueRegion = state->getSVal(Region).getAsRegion();
+    if (!ValueRegion) {
+      // FIXME: This should not happen. The language guarantees a presence
+      // of a valid initializer here, so the reference shall not be undefined.
+      // It seems that we're calling destructors over variables that
+      // were not initialized yet.
+      return;
+    }
+    Region = ValueRegion->getBaseRegion();
     varType = cast<TypedValueRegion>(Region)->getValueType();
   }
 
@@ -767,7 +813,7 @@ void ExprEngine::Visit(const Stmt *S, ExplodedNode *Pred,
   assert(!isa<Expr>(S) || S == cast<Expr>(S)->IgnoreParens());
 
   switch (S->getStmtClass()) {
-    // C++ and ARC stuff we don't support yet.
+    // C++, OpenMP and ARC stuff we don't support yet.
     case Expr::ObjCIndirectCopyRestoreExprClass:
     case Stmt::CXXDependentScopeMemberExprClass:
     case Stmt::CXXInheritedCtorInitExprClass:
@@ -790,41 +836,13 @@ void ExprEngine::Visit(const Stmt *S, ExplodedNode *Pred,
     case Stmt::FunctionParmPackExprClass:
     case Stmt::CoroutineBodyStmtClass:
     case Stmt::CoawaitExprClass:
+    case Stmt::DependentCoawaitExprClass:
     case Stmt::CoreturnStmtClass:
     case Stmt::CoyieldExprClass:
     case Stmt::SEHTryStmtClass:
     case Stmt::SEHExceptStmtClass:
     case Stmt::SEHLeaveStmtClass:
-    case Stmt::SEHFinallyStmtClass: {
-      const ExplodedNode *node = Bldr.generateSink(S, Pred, Pred->getState());
-      Engine.addAbortedBlock(node, currBldrCtx->getBlock());
-      break;
-    }
-
-    case Stmt::ParenExprClass:
-      llvm_unreachable("ParenExprs already handled.");
-    case Stmt::GenericSelectionExprClass:
-      llvm_unreachable("GenericSelectionExprs already handled.");
-    // Cases that should never be evaluated simply because they shouldn't
-    // appear in the CFG.
-    case Stmt::BreakStmtClass:
-    case Stmt::CaseStmtClass:
-    case Stmt::CompoundStmtClass:
-    case Stmt::ContinueStmtClass:
-    case Stmt::CXXForRangeStmtClass:
-    case Stmt::DefaultStmtClass:
-    case Stmt::DoStmtClass:
-    case Stmt::ForStmtClass:
-    case Stmt::GotoStmtClass:
-    case Stmt::IfStmtClass:
-    case Stmt::IndirectGotoStmtClass:
-    case Stmt::LabelStmtClass:
-    case Stmt::NoStmtClass:
-    case Stmt::NullStmtClass:
-    case Stmt::SwitchStmtClass:
-    case Stmt::WhileStmtClass:
-    case Expr::MSDependentExistsStmtClass:
-    case Stmt::CapturedStmtClass:
+    case Stmt::SEHFinallyStmtClass:
     case Stmt::OMPParallelDirectiveClass:
     case Stmt::OMPSimdDirectiveClass:
     case Stmt::OMPForDirectiveClass:
@@ -872,6 +890,36 @@ void ExprEngine::Visit(const Stmt *S, ExplodedNode *Pred,
     case Stmt::OMPTargetTeamsDistributeParallelForDirectiveClass:
     case Stmt::OMPTargetTeamsDistributeParallelForSimdDirectiveClass:
     case Stmt::OMPTargetTeamsDistributeSimdDirectiveClass:
+    case Stmt::CapturedStmtClass:
+    {
+      const ExplodedNode *node = Bldr.generateSink(S, Pred, Pred->getState());
+      Engine.addAbortedBlock(node, currBldrCtx->getBlock());
+      break;
+    }
+
+    case Stmt::ParenExprClass:
+      llvm_unreachable("ParenExprs already handled.");
+    case Stmt::GenericSelectionExprClass:
+      llvm_unreachable("GenericSelectionExprs already handled.");
+    // Cases that should never be evaluated simply because they shouldn't
+    // appear in the CFG.
+    case Stmt::BreakStmtClass:
+    case Stmt::CaseStmtClass:
+    case Stmt::CompoundStmtClass:
+    case Stmt::ContinueStmtClass:
+    case Stmt::CXXForRangeStmtClass:
+    case Stmt::DefaultStmtClass:
+    case Stmt::DoStmtClass:
+    case Stmt::ForStmtClass:
+    case Stmt::GotoStmtClass:
+    case Stmt::IfStmtClass:
+    case Stmt::IndirectGotoStmtClass:
+    case Stmt::LabelStmtClass:
+    case Stmt::NoStmtClass:
+    case Stmt::NullStmtClass:
+    case Stmt::SwitchStmtClass:
+    case Stmt::WhileStmtClass:
+    case Expr::MSDependentExistsStmtClass:
       llvm_unreachable("Stmt should not be in analyzer evaluation loop");
 
     case Stmt::ObjCSubscriptRefExprClass:
@@ -2165,7 +2213,9 @@ public:
 // (3) We are binding to a MemRegion with stack storage that the store
 //     does not understand.
 ProgramStateRef ExprEngine::processPointerEscapedOnBind(ProgramStateRef State,
-                                                        SVal Loc, SVal Val) {
+                                                        SVal Loc,
+                                                        SVal Val,
+                                                        const LocationContext *LCtx) {
   // Are we storing to something that causes the value to "escape"?
   bool escapes = true;
 
@@ -2181,7 +2231,7 @@ ProgramStateRef ExprEngine::processPointerEscapedOnBind(ProgramStateRef State,
       // same state.
       SVal StoredVal = State->getSVal(regionLoc->getRegion());
       if (StoredVal != Val)
-        escapes = (State == (State->bindLoc(*regionLoc, Val)));
+        escapes = (State == (State->bindLoc(*regionLoc, Val, LCtx)));
     }
   }
 
@@ -2278,7 +2328,7 @@ void ExprEngine::evalBind(ExplodedNodeSet &Dst, const Stmt *StoreE,
     const ProgramPoint L = PostStore(StoreE, LC, /*Loc*/nullptr,
                                      /*tag*/nullptr);
     ProgramStateRef state = Pred->getState();
-    state = processPointerEscapedOnBind(state, location, Val);
+    state = processPointerEscapedOnBind(state, location, Val, LC);
     Bldr.generateNode(L, state, Pred);
     return;
   }
@@ -2288,13 +2338,13 @@ void ExprEngine::evalBind(ExplodedNodeSet &Dst, const Stmt *StoreE,
     ExplodedNode *PredI = *I;
     ProgramStateRef state = PredI->getState();
 
-    state = processPointerEscapedOnBind(state, location, Val);
+    state = processPointerEscapedOnBind(state, location, Val, LC);
 
     // When binding the value, pass on the hint that this is a initialization.
     // For initializations, we do not need to inform clients of region
     // changes.
     state = state->bindLoc(location.castAs<Loc>(),
-                           Val, /* notifyChanges = */ !atDeclInit);
+                           Val, LC, /* notifyChanges = */ !atDeclInit);
 
     const MemRegion *LocReg = nullptr;
     if (Optional<loc::MemRegionVal> LocRegVal =
@@ -2520,7 +2570,7 @@ void ExprEngine::VisitGCCAsmStmt(const GCCAsmStmt *A, ExplodedNode *Pred,
     assert (!X.getAs<NonLoc>());  // Should be an Lval, or unknown, undef.
 
     if (Optional<Loc> LV = X.getAs<Loc>())
-      state = state->bindLoc(*LV, UnknownVal());
+      state = state->bindLoc(*LV, UnknownVal(), Pred->getLocationContext());
   }
 
   Bldr.generateNode(A, Pred, state);
diff --git a/lib/StaticAnalyzer/Core/ExprEngineC.cpp b/lib/StaticAnalyzer/Core/ExprEngineC.cpp
index 89fab1d56af00..8f720a2067b15 100644
--- a/lib/StaticAnalyzer/Core/ExprEngineC.cpp
+++ b/lib/StaticAnalyzer/Core/ExprEngineC.cpp
@@ -227,12 +227,13 @@ void ExprEngine::VisitBlockExpr(const BlockExpr *BE, ExplodedNode *Pred,
 
       if (capturedR != originalR) {
         SVal originalV;
+        const LocationContext *LCtx = Pred->getLocationContext();
         if (copyExpr) {
-          originalV = State->getSVal(copyExpr, Pred->getLocationContext());
+          originalV = State->getSVal(copyExpr, LCtx);
         } else {
           originalV = State->getSVal(loc::MemRegionVal(originalR));
         }
-        State = State->bindLoc(loc::MemRegionVal(capturedR), originalV);
+        State = State->bindLoc(loc::MemRegionVal(capturedR), originalV, LCtx);
       }
     }
   }
@@ -534,7 +535,7 @@ void ExprEngine::VisitCompoundLiteralExpr(const CompoundLiteralExpr *CL,
   } else {
     assert(isa<InitListExpr>(Init));
     Loc CLLoc = State->getLValue(CL, LCtx);
-    State = State->bindLoc(CLLoc, V);
+    State = State->bindLoc(CLLoc, V, LCtx);
 
     if (CL->isGLValue())
       V = CLLoc;
@@ -1053,7 +1054,7 @@ void ExprEngine::VisitIncrementDecrementOperator(const UnaryOperator* U,
     // Conjure a new symbol if necessary to recover precision.
     if (Result.isUnknown()){
       DefinedOrUnknownSVal SymVal =
-        svalBuilder.conjureSymbolVal(nullptr, Ex, LCtx,
+        svalBuilder.conjureSymbolVal(nullptr, U, LCtx,
                                      currBldrCtx->blockCount());
       Result = SymVal;
 
diff --git a/lib/StaticAnalyzer/Core/ExprEngineCXX.cpp b/lib/StaticAnalyzer/Core/ExprEngineCXX.cpp
index 7e9b2033ca373..03e0095d0e837 100644
--- a/lib/StaticAnalyzer/Core/ExprEngineCXX.cpp
+++ b/lib/StaticAnalyzer/Core/ExprEngineCXX.cpp
@@ -317,7 +317,7 @@ void ExprEngine::VisitCXXConstructExpr(const CXXConstructExpr *CE,
         // actually make things worse. Placement new makes this tricky as well,
         // since it's then possible to be initializing one part of a multi-
         // dimensional array.
-        State = State->bindDefault(loc::MemRegionVal(Target), ZeroVal);
+        State = State->bindDefault(loc::MemRegionVal(Target), ZeroVal, LCtx);
         Bldr.generateNode(CE, *I, State, /*tag=*/nullptr,
                           ProgramPoint::PreStmtKind);
       }
@@ -512,7 +512,8 @@ void ExprEngine::VisitCXXNewExpr(const CXXNewExpr *CNE, ExplodedNode *Pred,
   if (CNE->isArray()) {
     // FIXME: allocating an array requires simulating the constructors.
     // For now, just return a symbolicated region.
-    const MemRegion *NewReg = symVal.castAs<loc::MemRegionVal>().getRegion();
+    const SubRegion *NewReg =
+        symVal.castAs<loc::MemRegionVal>().getRegionAs<SubRegion>();
     QualType ObjTy = CNE->getType()->getAs<PointerType>()->getPointeeType();
     const ElementRegion *EleReg =
       getStoreManager().GetElementZeroRegion(NewReg, ObjTy);
@@ -572,7 +573,7 @@ void ExprEngine::VisitCXXCatchStmt(const CXXCatchStmt *CS,
   SVal V = svalBuilder.conjureSymbolVal(CS, LCtx, VD->getType(),
                                         currBldrCtx->blockCount());
   ProgramStateRef state = Pred->getState();
-  state = state->bindLoc(state->getLValue(VD, LCtx), V);
+  state = state->bindLoc(state->getLValue(VD, LCtx), V, LCtx);
 
   StmtNodeBuilder Bldr(Pred, Dst, *currBldrCtx);
   Bldr.generateNode(CS, Pred, state);
@@ -627,7 +628,7 @@ void ExprEngine::VisitLambdaExpr(const LambdaExpr *LE, ExplodedNode *Pred,
       InitVal = State->getSVal(SizeExpr, LocCtxt);
     }
 
-    State = State->bindLoc(FieldLoc, InitVal);
+    State = State->bindLoc(FieldLoc, InitVal, LocCtxt);
   }
 
   // Decay the Loc into an RValue, because there might be a
diff --git a/lib/StaticAnalyzer/Core/ExprEngineObjC.cpp b/lib/StaticAnalyzer/Core/ExprEngineObjC.cpp
index 92c5fe6b6f1a3..f5e64f4a5a8c6 100644
--- a/lib/StaticAnalyzer/Core/ExprEngineObjC.cpp
+++ b/lib/StaticAnalyzer/Core/ExprEngineObjC.cpp
@@ -115,11 +115,11 @@ void ExprEngine::VisitObjCForCollectionStmt(const ObjCForCollectionStmt *S,
         SymbolRef Sym = SymMgr.conjureSymbol(elem, LCtx, T,
                                              currBldrCtx->blockCount());
         SVal V = svalBuilder.makeLoc(Sym);
-        hasElems = hasElems->bindLoc(elementV, V);
+        hasElems = hasElems->bindLoc(elementV, V, LCtx);
 
         // Bind the location to 'nil' on the false branch.
         SVal nilV = svalBuilder.makeIntVal(0, T);
-        noElems = noElems->bindLoc(elementV, nilV);
+        noElems = noElems->bindLoc(elementV, nilV, LCtx);
       }
 
     // Create the new nodes.
diff --git a/lib/StaticAnalyzer/Core/MemRegion.cpp b/lib/StaticAnalyzer/Core/MemRegion.cpp
index d6e8fe5b51b36..7bc186d5b9941 100644
--- a/lib/StaticAnalyzer/Core/MemRegion.cpp
+++ b/lib/StaticAnalyzer/Core/MemRegion.cpp
@@ -31,54 +31,56 @@ using namespace ento;
 // MemRegion Construction.
 //===----------------------------------------------------------------------===//
 
-template <typename RegionTy, typename A1>
-RegionTy* MemRegionManager::getSubRegion(const A1 a1,
-                                         const MemRegion *superRegion) {
+template <typename RegionTy, typename SuperTy, typename Arg1Ty>
+RegionTy* MemRegionManager::getSubRegion(const Arg1Ty arg1,
+                                         const SuperTy *superRegion) {
   llvm::FoldingSetNodeID ID;
-  RegionTy::ProfileRegion(ID, a1, superRegion);
+  RegionTy::ProfileRegion(ID, arg1, superRegion);
   void *InsertPos;
   RegionTy* R = cast_or_null<RegionTy>(Regions.FindNodeOrInsertPos(ID,
                                                                    InsertPos));
 
   if (!R) {
     R = A.Allocate<RegionTy>();
-    new (R) RegionTy(a1, superRegion);
+    new (R) RegionTy(arg1, superRegion);
     Regions.InsertNode(R, InsertPos);
   }
 
   return R;
 }
 
-template <typename RegionTy, typename A1, typename A2>
-RegionTy* MemRegionManager::getSubRegion(const A1 a1, const A2 a2,
-                                         const MemRegion *superRegion) {
+template <typename RegionTy, typename SuperTy, typename Arg1Ty, typename Arg2Ty>
+RegionTy* MemRegionManager::getSubRegion(const Arg1Ty arg1, const Arg2Ty arg2,
+                                         const SuperTy *superRegion) {
   llvm::FoldingSetNodeID ID;
-  RegionTy::ProfileRegion(ID, a1, a2, superRegion);
+  RegionTy::ProfileRegion(ID, arg1, arg2, superRegion);
   void *InsertPos;
   RegionTy* R = cast_or_null<RegionTy>(Regions.FindNodeOrInsertPos(ID,
                                                                    InsertPos));
 
   if (!R) {
     R = A.Allocate<RegionTy>();
-    new (R) RegionTy(a1, a2, superRegion);
+    new (R) RegionTy(arg1, arg2, superRegion);
     Regions.InsertNode(R, InsertPos);
   }
 
   return R;
 }
 
-template <typename RegionTy, typename A1, typename A2, typename A3>
-RegionTy* MemRegionManager::getSubRegion(const A1 a1, const A2 a2, const A3 a3,
-                                         const MemRegion *superRegion) {
+template <typename RegionTy, typename SuperTy,
+          typename Arg1Ty, typename Arg2Ty, typename Arg3Ty>
+RegionTy* MemRegionManager::getSubRegion(const Arg1Ty arg1, const Arg2Ty arg2,
+                                         const Arg3Ty arg3,
+                                         const SuperTy *superRegion) {
   llvm::FoldingSetNodeID ID;
-  RegionTy::ProfileRegion(ID, a1, a2, a3, superRegion);
+  RegionTy::ProfileRegion(ID, arg1, arg2, arg3, superRegion);
   void *InsertPos;
   RegionTy* R = cast_or_null<RegionTy>(Regions.FindNodeOrInsertPos(ID,
                                                                    InsertPos));
 
   if (!R) {
     R = A.Allocate<RegionTy>();
-    new (R) RegionTy(a1, a2, a3, superRegion);
+    new (R) RegionTy(arg1, arg2, arg3, superRegion);
     Regions.InsertNode(R, InsertPos);
   }
 
@@ -180,8 +182,8 @@ DefinedOrUnknownSVal StringRegion::getExtent(SValBuilder &svalBuilder) const {
                                 svalBuilder.getArrayIndexType());
 }
 
-ObjCIvarRegion::ObjCIvarRegion(const ObjCIvarDecl *ivd, const MemRegion* sReg)
-  : DeclRegion(ivd, sReg, ObjCIvarRegionKind) {}
+ObjCIvarRegion::ObjCIvarRegion(const ObjCIvarDecl *ivd, const SubRegion *sReg)
+    : DeclRegion(ivd, sReg, ObjCIvarRegionKind) {}
 
 const ObjCIvarDecl *ObjCIvarRegion::getDecl() const {
   return cast<ObjCIvarDecl>(D);
@@ -379,10 +381,8 @@ void CXXBaseObjectRegion::Profile(llvm::FoldingSetNodeID &ID) const {
 //===----------------------------------------------------------------------===//
 
 void GlobalsSpaceRegion::anchor() { }
-void HeapSpaceRegion::anchor() { }
-void UnknownSpaceRegion::anchor() { }
-void StackLocalsSpaceRegion::anchor() { }
-void StackArgumentsSpaceRegion::anchor() { }
+void NonStaticGlobalSpaceRegion::anchor() { }
+void StackSpaceRegion::anchor() { }
 void TypedRegion::anchor() { }
 void TypedValueRegion::anchor() { }
 void CodeTextRegion::anchor() { }
@@ -737,12 +737,14 @@ const CodeSpaceRegion *MemRegionManager::getCodeRegion() {
 // Constructing regions.
 //===----------------------------------------------------------------------===//
 const StringRegion* MemRegionManager::getStringRegion(const StringLiteral* Str){
-  return getSubRegion<StringRegion>(Str, getGlobalsRegion());
+  return getSubRegion<StringRegion>(
+      Str, cast<GlobalInternalSpaceRegion>(getGlobalsRegion()));
 }
 
 const ObjCStringRegion *
 MemRegionManager::getObjCStringRegion(const ObjCStringLiteral* Str){
-  return getSubRegion<ObjCStringRegion>(Str, getGlobalsRegion());
+  return getSubRegion<ObjCStringRegion>(
+      Str, cast<GlobalInternalSpaceRegion>(getGlobalsRegion()));
 }
 
 /// Look through a chain of LocationContexts to either find the
@@ -871,7 +873,7 @@ const BlockDataRegion *
 MemRegionManager::getBlockDataRegion(const BlockCodeRegion *BC,
                                      const LocationContext *LC,
                                      unsigned blockCount) {
-  const MemRegion *sReg = nullptr;
+  const MemSpaceRegion *sReg = nullptr;
   const BlockDecl *BD = BC->getDecl();
   if (!BD->hasCaptures()) {
     // This handles 'static' blocks.
@@ -904,7 +906,7 @@ MemRegionManager::getCXXStaticTempObjectRegion(const Expr *Ex) {
 const CompoundLiteralRegion*
 MemRegionManager::getCompoundLiteralRegion(const CompoundLiteralExpr *CL,
                                            const LocationContext *LC) {
-  const MemRegion *sReg = nullptr;
+  const MemSpaceRegion *sReg = nullptr;
 
   if (CL->isFileScope())
     sReg = getGlobalsRegion();
@@ -919,7 +921,7 @@ MemRegionManager::getCompoundLiteralRegion(const CompoundLiteralExpr *CL,
 
 const ElementRegion*
 MemRegionManager::getElementRegion(QualType elementType, NonLoc Idx,
-                                   const MemRegion* superRegion,
+                                   const SubRegion* superRegion,
                                    ASTContext &Ctx){
   QualType T = Ctx.getCanonicalType(elementType).getUnqualifiedType();
 
@@ -962,13 +964,13 @@ const SymbolicRegion *MemRegionManager::getSymbolicHeapRegion(SymbolRef Sym) {
 
 const FieldRegion*
 MemRegionManager::getFieldRegion(const FieldDecl *d,
-                                 const MemRegion* superRegion){
+                                 const SubRegion* superRegion){
   return getSubRegion<FieldRegion>(d, superRegion);
 }
 
 const ObjCIvarRegion*
 MemRegionManager::getObjCIvarRegion(const ObjCIvarDecl *d,
-                                    const MemRegion* superRegion) {
+                                    const SubRegion* superRegion) {
   return getSubRegion<ObjCIvarRegion>(d, superRegion);
 }
 
@@ -1004,7 +1006,7 @@ static bool isValidBaseClass(const CXXRecordDecl *BaseClass,
 
 const CXXBaseObjectRegion *
 MemRegionManager::getCXXBaseObjectRegion(const CXXRecordDecl *RD,
-                                         const MemRegion *Super,
+                                         const SubRegion *Super,
                                          bool IsVirtual) {
   if (isa<TypedValueRegion>(Super)) {
     assert(isValidBaseClass(RD, dyn_cast<TypedValueRegion>(Super), IsVirtual));
@@ -1015,7 +1017,7 @@ MemRegionManager::getCXXBaseObjectRegion(const CXXRecordDecl *RD,
       // are different.
       while (const CXXBaseObjectRegion *Base =
                dyn_cast<CXXBaseObjectRegion>(Super)) {
-        Super = Base->getSuperRegion();
+        Super = cast<SubRegion>(Base->getSuperRegion());
       }
       assert(Super && !isa<MemSpaceRegion>(Super));
     }
diff --git a/lib/StaticAnalyzer/Core/ProgramState.cpp b/lib/StaticAnalyzer/Core/ProgramState.cpp
index 03ace35965cba..31556c792fc5b 100644
--- a/lib/StaticAnalyzer/Core/ProgramState.cpp
+++ b/lib/StaticAnalyzer/Core/ProgramState.cpp
@@ -111,24 +111,29 @@ ProgramStateManager::removeDeadBindings(ProgramStateRef state,
   return ConstraintMgr->removeDeadBindings(Result, SymReaper);
 }
 
-ProgramStateRef ProgramState::bindLoc(Loc LV, SVal V, bool notifyChanges) const {
+ProgramStateRef ProgramState::bindLoc(Loc LV,
+                                      SVal V,
+                                      const LocationContext *LCtx,
+                                      bool notifyChanges) const {
   ProgramStateManager &Mgr = getStateManager();
   ProgramStateRef newState = makeWithStore(Mgr.StoreMgr->Bind(getStore(),
                                                              LV, V));
   const MemRegion *MR = LV.getAsRegion();
   if (MR && Mgr.getOwningEngine() && notifyChanges)
-    return Mgr.getOwningEngine()->processRegionChange(newState, MR);
+    return Mgr.getOwningEngine()->processRegionChange(newState, MR, LCtx);
 
   return newState;
 }
 
-ProgramStateRef ProgramState::bindDefault(SVal loc, SVal V) const {
+ProgramStateRef ProgramState::bindDefault(SVal loc,
+                                          SVal V,
+                                          const LocationContext *LCtx) const {
   ProgramStateManager &Mgr = getStateManager();
   const MemRegion *R = loc.castAs<loc::MemRegionVal>().getRegion();
   const StoreRef &newStore = Mgr.StoreMgr->BindDefault(getStore(), R, V);
   ProgramStateRef new_state = makeWithStore(newStore);
   return Mgr.getOwningEngine() ?
-           Mgr.getOwningEngine()->processRegionChange(new_state, R) :
+           Mgr.getOwningEngine()->processRegionChange(new_state, R, LCtx) :
            new_state;
 }
 
@@ -202,7 +207,7 @@ ProgramState::invalidateRegionsImpl(ValueList Values,
     }
 
     return Eng->processRegionChanges(newState, IS, TopLevelInvalidated,
-                                     Invalidated, Call);
+                                     Invalidated, LCtx, Call);
   }
 
   const StoreRef &newStore =
diff --git a/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index 15073bb82b366..e0ad2d8ad45c2 100644
--- a/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -12,7 +12,7 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "SimpleConstraintManager.h"
+#include "RangedConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
@@ -282,12 +282,31 @@ REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintRange,
                                                              RangeSet))
 
 namespace {
-class RangeConstraintManager : public SimpleConstraintManager {
-  RangeSet getRange(ProgramStateRef State, SymbolRef Sym);
-
+class RangeConstraintManager : public RangedConstraintManager {
 public:
   RangeConstraintManager(SubEngine *SE, SValBuilder &SVB)
-      : SimpleConstraintManager(SE, SVB) {}
+      : RangedConstraintManager(SE, SVB) {}
+
+  //===------------------------------------------------------------------===//
+  // Implementation for interface from ConstraintManager.
+  //===------------------------------------------------------------------===//
+
+  bool canReasonAbout(SVal X) const override;
+
+  ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
+
+  const llvm::APSInt *getSymVal(ProgramStateRef State,
+                                SymbolRef Sym) const override;
+
+  ProgramStateRef removeDeadBindings(ProgramStateRef State,
+                                     SymbolReaper &SymReaper) override;
+
+  void print(ProgramStateRef State, raw_ostream &Out, const char *nl,
+             const char *sep) override;
+
+  //===------------------------------------------------------------------===//
+  // Implementation for interface from RangedConstraintManager.
+  //===------------------------------------------------------------------===//
 
   ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,
                               const llvm::APSInt &V,
@@ -313,26 +332,19 @@ public:
                               const llvm::APSInt &V,
                               const llvm::APSInt &Adjustment) override;
 
-  ProgramStateRef assumeSymbolWithinInclusiveRange(
+  ProgramStateRef assumeSymWithinInclusiveRange(
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
       const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
 
-  ProgramStateRef assumeSymbolOutOfInclusiveRange(
+  ProgramStateRef assumeSymOutsideInclusiveRange(
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
       const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
 
-  const llvm::APSInt *getSymVal(ProgramStateRef St,
-                                SymbolRef Sym) const override;
-  ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
-
-  ProgramStateRef removeDeadBindings(ProgramStateRef St,
-                                     SymbolReaper &SymReaper) override;
-
-  void print(ProgramStateRef St, raw_ostream &Out, const char *nl,
-             const char *sep) override;
-
 private:
   RangeSet::Factory F;
+
+  RangeSet getRange(ProgramStateRef State, SymbolRef Sym);
+
   RangeSet getSymLTRange(ProgramStateRef St, SymbolRef Sym,
                          const llvm::APSInt &Int,
                          const llvm::APSInt &Adjustment);
@@ -356,10 +368,46 @@ ento::CreateRangeConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
   return llvm::make_unique<RangeConstraintManager>(Eng, StMgr.getSValBuilder());
 }
 
-const llvm::APSInt *RangeConstraintManager::getSymVal(ProgramStateRef St,
-                                                      SymbolRef Sym) const {
-  const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(Sym);
-  return T ? T->getConcreteValue() : nullptr;
+bool RangeConstraintManager::canReasonAbout(SVal X) const {
+  Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
+  if (SymVal && SymVal->isExpression()) {
+    const SymExpr *SE = SymVal->getSymbol();
+
+    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
+      switch (SIE->getOpcode()) {
+      // We don't reason yet about bitwise-constraints on symbolic values.
+      case BO_And:
+      case BO_Or:
+      case BO_Xor:
+        return false;
+      // We don't reason yet about these arithmetic constraints on
+      // symbolic values.
+      case BO_Mul:
+      case BO_Div:
+      case BO_Rem:
+      case BO_Shl:
+      case BO_Shr:
+        return false;
+      // All other cases.
+      default:
+        return true;
+      }
+    }
+
+    if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
+      if (BinaryOperator::isComparisonOp(SSE->getOpcode())) {
+        // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
+        if (Loc::isLocType(SSE->getLHS()->getType())) {
+          assert(Loc::isLocType(SSE->getRHS()->getType()));
+          return true;
+        }
+      }
+    }
+
+    return false;
+  }
+
+  return true;
 }
 
 ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State,
@@ -386,6 +434,12 @@ ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State,
   return ConditionTruthVal();
 }
 
+const llvm::APSInt *RangeConstraintManager::getSymVal(ProgramStateRef St,
+                                                      SymbolRef Sym) const {
+  const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(Sym);
+  return T ? T->getConcreteValue() : nullptr;
+}
+
 /// Scan all symbols referenced by the constraints. If the symbol is not alive
 /// as marked in LSymbols, mark it as dead in DSymbols.
 ProgramStateRef
@@ -429,7 +483,7 @@ RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
 }
 
 //===------------------------------------------------------------------------===
-// assumeSymX methods: public interface for RangeConstraintManager.
+// assumeSymX methods: protected interface for RangeConstraintManager.
 //===------------------------------------------------------------------------===/
 
 // The syntax for ranges below is mathematical, using [x, y] for closed ranges
@@ -646,7 +700,7 @@ RangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym,
   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
-ProgramStateRef RangeConstraintManager::assumeSymbolWithinInclusiveRange(
+ProgramStateRef RangeConstraintManager::assumeSymWithinInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
     const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
   RangeSet New = getSymGERange(State, Sym, From, Adjustment);
@@ -656,7 +710,7 @@ ProgramStateRef RangeConstraintManager::assumeSymbolWithinInclusiveRange(
   return New.isEmpty() ? nullptr : State->set<ConstraintRange>(Sym, New);
 }
 
-ProgramStateRef RangeConstraintManager::assumeSymbolOutOfInclusiveRange(
+ProgramStateRef RangeConstraintManager::assumeSymOutsideInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
     const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
   RangeSet RangeLT = getSymLTRange(State, Sym, From, Adjustment);
diff --git a/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp b/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
new file mode 100644
index 0000000000000..1304116f4974b
--- /dev/null
+++ b/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -0,0 +1,204 @@
+//== RangedConstraintManager.cpp --------------------------------*- C++ -*--==//
+//
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+//  This file defines RangedConstraintManager, a class that provides a
+//  range-based constraint manager interface.
+//
+//===----------------------------------------------------------------------===//
+
+#include "RangedConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+
+namespace clang {
+
+namespace ento {
+
+RangedConstraintManager::~RangedConstraintManager() {}
+
+ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
+                                                   SymbolRef Sym,
+                                                   bool Assumption) {
+  // Handle SymbolData.
+  if (isa<SymbolData>(Sym)) {
+    return assumeSymUnsupported(State, Sym, Assumption);
+
+    // Handle symbolic expression.
+  } else if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Sym)) {
+    // We can only simplify expressions whose RHS is an integer.
+
+    BinaryOperator::Opcode op = SIE->getOpcode();
+    if (BinaryOperator::isComparisonOp(op)) {
+      if (!Assumption)
+        op = BinaryOperator::negateComparisonOp(op);
+
+      return assumeSymRel(State, SIE->getLHS(), op, SIE->getRHS());
+    }
+
+  } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) {
+    // Translate "a != b" to "(b - a) != 0".
+    // We invert the order of the operands as a heuristic for how loop
+    // conditions are usually written ("begin != end") as compared to length
+    // calculations ("end - begin"). The more correct thing to do would be to
+    // canonicalize "a - b" and "b - a", which would allow us to treat
+    // "a != b" and "b != a" the same.
+    SymbolManager &SymMgr = getSymbolManager();
+    BinaryOperator::Opcode Op = SSE->getOpcode();
+    assert(BinaryOperator::isComparisonOp(Op));
+
+    // For now, we only support comparing pointers.
+    assert(Loc::isLocType(SSE->getLHS()->getType()));
+    assert(Loc::isLocType(SSE->getRHS()->getType()));
+    QualType DiffTy = SymMgr.getContext().getPointerDiffType();
+    SymbolRef Subtraction =
+        SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), DiffTy);
+
+    const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy);
+    Op = BinaryOperator::reverseComparisonOp(Op);
+    if (!Assumption)
+      Op = BinaryOperator::negateComparisonOp(Op);
+    return assumeSymRel(State, Subtraction, Op, Zero);
+  }
+
+  // If we get here, there's nothing else we can do but treat the symbol as
+  // opaque.
+  return assumeSymUnsupported(State, Sym, Assumption);
+}
+
+ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(
+    ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
+    const llvm::APSInt &To, bool InRange) {
+  // Get the type used for calculating wraparound.
+  BasicValueFactory &BVF = getBasicVals();
+  APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType());
+
+  llvm::APSInt Adjustment = WraparoundType.getZeroValue();
+  SymbolRef AdjustedSym = Sym;
+  computeAdjustment(AdjustedSym, Adjustment);
+
+  // Convert the right-hand side integer as necessary.
+  APSIntType ComparisonType = std::max(WraparoundType, APSIntType(From));
+  llvm::APSInt ConvertedFrom = ComparisonType.convert(From);
+  llvm::APSInt ConvertedTo = ComparisonType.convert(To);
+
+  // Prefer unsigned comparisons.
+  if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
+      ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
+    Adjustment.setIsSigned(false);
+
+  if (InRange)
+    return assumeSymWithinInclusiveRange(State, AdjustedSym, ConvertedFrom,
+                                         ConvertedTo, Adjustment);
+  return assumeSymOutsideInclusiveRange(State, AdjustedSym, ConvertedFrom,
+                                        ConvertedTo, Adjustment);
+}
+
+ProgramStateRef
+RangedConstraintManager::assumeSymUnsupported(ProgramStateRef State,
+                                              SymbolRef Sym, bool Assumption) {
+  BasicValueFactory &BVF = getBasicVals();
+  QualType T = Sym->getType();
+
+  // Non-integer types are not supported.
+  if (!T->isIntegralOrEnumerationType())
+    return State;
+
+  // Reverse the operation and add directly to state.
+  const llvm::APSInt &Zero = BVF.getValue(0, T);
+  if (Assumption)
+    return assumeSymNE(State, Sym, Zero, Zero);
+  else
+    return assumeSymEQ(State, Sym, Zero, Zero);
+}
+
+ProgramStateRef RangedConstraintManager::assumeSymRel(ProgramStateRef State,
+                                                      SymbolRef Sym,
+                                                      BinaryOperator::Opcode Op,
+                                                      const llvm::APSInt &Int) {
+  assert(BinaryOperator::isComparisonOp(Op) &&
+         "Non-comparison ops should be rewritten as comparisons to zero.");
+
+  // Simplification: translate an assume of a constraint of the form
+  // "(exp comparison_op expr) != 0" to true into an assume of
+  // "exp comparison_op expr" to true. (And similarly, an assume of the form
+  // "(exp comparison_op expr) == 0" to true into an assume of
+  // "exp comparison_op expr" to false.)
+  if (Int == 0 && (Op == BO_EQ || Op == BO_NE)) {
+    if (const BinarySymExpr *SE = dyn_cast<BinarySymExpr>(Sym))
+      if (BinaryOperator::isComparisonOp(SE->getOpcode()))
+        return assumeSym(State, Sym, (Op == BO_NE ? true : false));
+  }
+
+  // Get the type used for calculating wraparound.
+  BasicValueFactory &BVF = getBasicVals();
+  APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType());
+
+  // We only handle simple comparisons of the form "$sym == constant"
+  // or "($sym+constant1) == constant2".
+  // The adjustment is "constant1" in the above expression. It's used to
+  // "slide" the solution range around for modular arithmetic. For example,
+  // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
+  // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
+  // the subclasses of SimpleConstraintManager to handle the adjustment.
+  llvm::APSInt Adjustment = WraparoundType.getZeroValue();
+  computeAdjustment(Sym, Adjustment);
+
+  // Convert the right-hand side integer as necessary.
+  APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int));
+  llvm::APSInt ConvertedInt = ComparisonType.convert(Int);
+
+  // Prefer unsigned comparisons.
+  if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
+      ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
+    Adjustment.setIsSigned(false);
+
+  switch (Op) {
+  default:
+    llvm_unreachable("invalid operation not caught by assertion above");
+
+  case BO_EQ:
+    return assumeSymEQ(State, Sym, ConvertedInt, Adjustment);
+
+  case BO_NE:
+    return assumeSymNE(State, Sym, ConvertedInt, Adjustment);
+
+  case BO_GT:
+    return assumeSymGT(State, Sym, ConvertedInt, Adjustment);
+
+  case BO_GE:
+    return assumeSymGE(State, Sym, ConvertedInt, Adjustment);
+
+  case BO_LT:
+    return assumeSymLT(State, Sym, ConvertedInt, Adjustment);
+
+  case BO_LE:
+    return assumeSymLE(State, Sym, ConvertedInt, Adjustment);
+  } // end switch
+}
+
+void RangedConstraintManager::computeAdjustment(SymbolRef &Sym,
+                                                llvm::APSInt &Adjustment) {
+  // Is it a "($sym+constant1)" expression?
+  if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
+    BinaryOperator::Opcode Op = SE->getOpcode();
+    if (Op == BO_Add || Op == BO_Sub) {
+      Sym = SE->getLHS();
+      Adjustment = APSIntType(Adjustment).convert(SE->getRHS());
+
+      // Don't forget to negate the adjustment if it's being subtracted.
+      // This should happen /after/ promotion, in case the value being
+      // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
+      if (Op == BO_Sub)
+        Adjustment = -Adjustment;
+    }
+  }
+}
+
+} // end of namespace ento
+
+} // end of namespace clang
diff --git a/lib/StaticAnalyzer/Core/SimpleConstraintManager.h b/lib/StaticAnalyzer/Core/RangedConstraintManager.h
index 1128e775b3205..a4e6062a4f576 100644
--- a/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
+++ b/lib/StaticAnalyzer/Core/RangedConstraintManager.h
@@ -1,4 +1,4 @@
-//== SimpleConstraintManager.h ----------------------------------*- C++ -*--==//
+//== RangedConstraintManager.h ----------------------------------*- C++ -*--==//
 //
 //                     The LLVM Compiler Infrastructure
 //
@@ -7,59 +7,55 @@
 //
 //===----------------------------------------------------------------------===//
 //
-//  Code shared between BasicConstraintManager and RangeConstraintManager.
+//  Ranged constraint manager, built on SimpleConstraintManager.
 //
 //===----------------------------------------------------------------------===//
 
-#ifndef LLVM_CLANG_LIB_STATICANALYZER_CORE_SIMPLECONSTRAINTMANAGER_H
-#define LLVM_CLANG_LIB_STATICANALYZER_CORE_SIMPLECONSTRAINTMANAGER_H
+#ifndef LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H
+#define LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H
 
-#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
 
 namespace clang {
 
 namespace ento {
 
-class SimpleConstraintManager : public ConstraintManager {
-  SubEngine *SU;
-  SValBuilder &SVB;
-
+class RangedConstraintManager : public SimpleConstraintManager {
 public:
-  SimpleConstraintManager(SubEngine *SE, SValBuilder &SB) : SU(SE), SVB(SB) {}
-  ~SimpleConstraintManager() override;
+  RangedConstraintManager(SubEngine *SE, SValBuilder &SB)
+      : SimpleConstraintManager(SE, SB) {}
+
+  ~RangedConstraintManager() override;
 
   //===------------------------------------------------------------------===//
-  // Common implementation for the interface provided by ConstraintManager.
+  // Implementation for interface from SimpleConstraintManager.
   //===------------------------------------------------------------------===//
 
-  ProgramStateRef assume(ProgramStateRef State, DefinedSVal Cond,
-                         bool Assumption) override;
+  ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
+                            bool Assumption) override;
 
-  ProgramStateRef assume(ProgramStateRef State, NonLoc Cond, bool Assumption);
+  ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
+                                          const llvm::APSInt &From,
+                                          const llvm::APSInt &To,
+                                          bool InRange) override;
 
-  ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value,
-                                       const llvm::APSInt &From,
-                                       const llvm::APSInt &To,
-                                       bool InRange) override;
+  ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
+                                       bool Assumption) override;
 
-  ProgramStateRef assumeSymRel(ProgramStateRef State, const SymExpr *LHS,
-                               BinaryOperator::Opcode Op,
+protected:
+  /// Assume a constraint between a symbolic expression and a concrete integer.
+  virtual ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym,
+                               BinaryOperator::Opcode op,
                                const llvm::APSInt &Int);
 
-  ProgramStateRef assumeSymWithinInclusiveRange(ProgramStateRef State,
-                                                SymbolRef Sym,
-                                                const llvm::APSInt &From,
-                                                const llvm::APSInt &To,
-                                                bool InRange);
-
-protected:
   //===------------------------------------------------------------------===//
   // Interface that subclasses must implement.
   //===------------------------------------------------------------------===//
 
   // Each of these is of the form "$Sym+Adj <> V", where "<>" is the comparison
   // operation for the method being invoked.
+
   virtual ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,
                                       const llvm::APSInt &V,
                                       const llvm::APSInt &Adjustment) = 0;
@@ -84,28 +80,19 @@ protected:
                                       const llvm::APSInt &V,
                                       const llvm::APSInt &Adjustment) = 0;
 
-  virtual ProgramStateRef assumeSymbolWithinInclusiveRange(
+  virtual ProgramStateRef assumeSymWithinInclusiveRange(
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
       const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
 
-  virtual ProgramStateRef assumeSymbolOutOfInclusiveRange(
+  virtual ProgramStateRef assumeSymOutsideInclusiveRange(
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
       const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
 
   //===------------------------------------------------------------------===//
   // Internal implementation.
   //===------------------------------------------------------------------===//
-
-  BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); }
-  SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); }
-
-  bool canReasonAbout(SVal X) const override;
-
-  ProgramStateRef assumeAux(ProgramStateRef State, NonLoc Cond,
-                            bool Assumption);
-
-  ProgramStateRef assumeAuxForSymbol(ProgramStateRef State, SymbolRef Sym,
-                                     bool Assumption);
+private:
+  static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);
 };
 
 } // end GR namespace
diff --git a/lib/StaticAnalyzer/Core/RegionStore.cpp b/lib/StaticAnalyzer/Core/RegionStore.cpp
index 934cc5cd3ac46..dd7e9dd117815 100644
--- a/lib/StaticAnalyzer/Core/RegionStore.cpp
+++ b/lib/StaticAnalyzer/Core/RegionStore.cpp
@@ -494,6 +494,11 @@ public: // Part of public interface to class.
     return getBinding(getRegionBindings(S), L, T);
   }
 
+  Optional<SVal> getDefaultBinding(Store S, const MemRegion *R) override {
+    RegionBindingsRef B = getRegionBindings(S);
+    return B.getDefaultBinding(R);
+  }
+
   SVal getBinding(RegionBindingsConstRef B, Loc L, QualType T = QualType());
 
   SVal getBindingForElement(RegionBindingsConstRef B, const ElementRegion *R);
@@ -1336,7 +1341,8 @@ SVal RegionStoreManager::ArrayToPointer(Loc Array, QualType T) {
   if (!Array.getAs<loc::MemRegionVal>())
     return UnknownVal();
 
-  const MemRegion* R = Array.castAs<loc::MemRegionVal>().getRegion();
+  const SubRegion *R =
+      cast<SubRegion>(Array.castAs<loc::MemRegionVal>().getRegion());
   NonLoc ZeroIdx = svalBuilder.makeZeroArrayIndex();
   return loc::MemRegionVal(MRMgr.getElementRegion(T, ZeroIdx, R, Ctx));
 }
@@ -1379,7 +1385,7 @@ SVal RegionStoreManager::getBinding(RegionBindingsConstRef B, Loc L, QualType T)
         T = SR->getSymbol()->getType();
       }
     }
-    MR = GetElementZeroRegion(MR, T);
+    MR = GetElementZeroRegion(cast<SubRegion>(MR), T);
   }
 
   // FIXME: Perhaps this method should just take a 'const MemRegion*' argument
diff --git a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
index 0e512ff808617..adb40178f5b16 100644
--- a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -7,12 +7,12 @@
 //
 //===----------------------------------------------------------------------===//
 //
-//  This file defines SimpleConstraintManager, a class that holds code shared
-//  between BasicConstraintManager and RangeConstraintManager.
+//  This file defines SimpleConstraintManager, a class that provides a
+//  simplified constraint manager interface, compared to ConstraintManager.
 //
 //===----------------------------------------------------------------------===//
 
-#include "SimpleConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
@@ -23,48 +23,6 @@ namespace ento {
 
 SimpleConstraintManager::~SimpleConstraintManager() {}
 
-bool SimpleConstraintManager::canReasonAbout(SVal X) const {
-  Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
-  if (SymVal && SymVal->isExpression()) {
-    const SymExpr *SE = SymVal->getSymbol();
-
-    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
-      switch (SIE->getOpcode()) {
-      // We don't reason yet about bitwise-constraints on symbolic values.
-      case BO_And:
-      case BO_Or:
-      case BO_Xor:
-        return false;
-      // We don't reason yet about these arithmetic constraints on
-      // symbolic values.
-      case BO_Mul:
-      case BO_Div:
-      case BO_Rem:
-      case BO_Shl:
-      case BO_Shr:
-        return false;
-      // All other cases.
-      default:
-        return true;
-      }
-    }
-
-    if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
-      if (BinaryOperator::isComparisonOp(SSE->getOpcode())) {
-        // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
-        if (Loc::isLocType(SSE->getLHS()->getType())) {
-          assert(Loc::isLocType(SSE->getRHS()->getType()));
-          return true;
-        }
-      }
-    }
-
-    return false;
-  }
-
-  return true;
-}
-
 ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef State,
                                                 DefinedSVal Cond,
                                                 bool Assumption) {
@@ -92,23 +50,6 @@ ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef State,
   return State;
 }
 
-ProgramStateRef
-SimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State,
-                                            SymbolRef Sym, bool Assumption) {
-  BasicValueFactory &BVF = getBasicVals();
-  QualType T = Sym->getType();
-
-  // None of the constraint solvers currently support non-integer types.
-  if (!T->isIntegralOrEnumerationType())
-    return State;
-
-  const llvm::APSInt &zero = BVF.getValue(0, T);
-  if (Assumption)
-    return assumeSymNE(State, Sym, zero, zero);
-  else
-    return assumeSymEQ(State, Sym, zero, zero);
-}
-
 ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef State,
                                                    NonLoc Cond,
                                                    bool Assumption) {
@@ -118,7 +59,8 @@ ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef State,
   if (!canReasonAbout(Cond)) {
     // Just add the constraint to the expression without trying to simplify.
     SymbolRef Sym = Cond.getAsSymExpr();
-    return assumeAuxForSymbol(State, Sym, Assumption);
+    assert(Sym);
+    return assumeSymUnsupported(State, Sym, Assumption);
   }
 
   switch (Cond.getSubKind()) {
@@ -129,51 +71,7 @@ ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef State,
     nonloc::SymbolVal SV = Cond.castAs<nonloc::SymbolVal>();
     SymbolRef Sym = SV.getSymbol();
     assert(Sym);
-
-    // Handle SymbolData.
-    if (!SV.isExpression()) {
-      return assumeAuxForSymbol(State, Sym, Assumption);
-
-      // Handle symbolic expression.
-    } else if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
-      // We can only simplify expressions whose RHS is an integer.
-
-      BinaryOperator::Opcode Op = SE->getOpcode();
-      if (BinaryOperator::isComparisonOp(Op)) {
-        if (!Assumption)
-          Op = BinaryOperator::negateComparisonOp(Op);
-
-        return assumeSymRel(State, SE->getLHS(), Op, SE->getRHS());
-      }
-
-    } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) {
-      // Translate "a != b" to "(b - a) != 0".
-      // We invert the order of the operands as a heuristic for how loop
-      // conditions are usually written ("begin != end") as compared to length
-      // calculations ("end - begin"). The more correct thing to do would be to
-      // canonicalize "a - b" and "b - a", which would allow us to treat
-      // "a != b" and "b != a" the same.
-      SymbolManager &SymMgr = getSymbolManager();
-      BinaryOperator::Opcode Op = SSE->getOpcode();
-      assert(BinaryOperator::isComparisonOp(Op));
-
-      // For now, we only support comparing pointers.
-      assert(Loc::isLocType(SSE->getLHS()->getType()));
-      assert(Loc::isLocType(SSE->getRHS()->getType()));
-      QualType DiffTy = SymMgr.getContext().getPointerDiffType();
-      SymbolRef Subtraction =
-          SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), DiffTy);
-
-      const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy);
-      Op = BinaryOperator::reverseComparisonOp(Op);
-      if (!Assumption)
-        Op = BinaryOperator::negateComparisonOp(Op);
-      return assumeSymRel(State, Subtraction, Op, Zero);
-    }
-
-    // If we get here, there's nothing else we can do but treat the symbol as
-    // opaque.
-    return assumeAuxForSymbol(State, Sym, Assumption);
+    return assumeSym(State, Sym, Assumption);
   }
 
   case nonloc::ConcreteIntKind: {
@@ -206,7 +104,7 @@ ProgramStateRef SimpleConstraintManager::assumeInclusiveRange(
     // Just add the constraint to the expression without trying to simplify.
     SymbolRef Sym = Value.getAsSymExpr();
     assert(Sym);
-    return assumeSymWithinInclusiveRange(State, Sym, From, To, InRange);
+    return assumeSymInclusiveRange(State, Sym, From, To, InRange);
   }
 
   switch (Value.getSubKind()) {
@@ -217,7 +115,7 @@ ProgramStateRef SimpleConstraintManager::assumeInclusiveRange(
   case nonloc::LocAsIntegerKind:
   case nonloc::SymbolValKind: {
     if (SymbolRef Sym = Value.getAsSymbol())
-      return assumeSymWithinInclusiveRange(State, Sym, From, To, InRange);
+      return assumeSymInclusiveRange(State, Sym, From, To, InRange);
     return State;
   } // end switch
 
@@ -230,118 +128,6 @@ ProgramStateRef SimpleConstraintManager::assumeInclusiveRange(
   } // end switch
 }
 
-static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) {
-  // Is it a "($sym+constant1)" expression?
-  if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
-    BinaryOperator::Opcode Op = SE->getOpcode();
-    if (Op == BO_Add || Op == BO_Sub) {
-      Sym = SE->getLHS();
-      Adjustment = APSIntType(Adjustment).convert(SE->getRHS());
-
-      // Don't forget to negate the adjustment if it's being subtracted.
-      // This should happen /after/ promotion, in case the value being
-      // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
-      if (Op == BO_Sub)
-        Adjustment = -Adjustment;
-    }
-  }
-}
-
-ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef State,
-                                                      const SymExpr *LHS,
-                                                      BinaryOperator::Opcode Op,
-                                                      const llvm::APSInt &Int) {
-  assert(BinaryOperator::isComparisonOp(Op) &&
-         "Non-comparison ops should be rewritten as comparisons to zero.");
-
-  SymbolRef Sym = LHS;
-
-  // Simplification: translate an assume of a constraint of the form
-  // "(exp comparison_op expr) != 0" to true into an assume of 
-  // "exp comparison_op expr" to true. (And similarly, an assume of the form
-  // "(exp comparison_op expr) == 0" to true into an assume of
-  // "exp comparison_op expr" to false.)
-  if (Int == 0 && (Op == BO_EQ || Op == BO_NE)) {
-    if (const BinarySymExpr *SE = dyn_cast<BinarySymExpr>(Sym))
-      if (BinaryOperator::isComparisonOp(SE->getOpcode()))
-        return assume(State, nonloc::SymbolVal(Sym), (Op == BO_NE ? true : false));
-  }
-
-  // Get the type used for calculating wraparound.
-  BasicValueFactory &BVF = getBasicVals();
-  APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType());
-
-  // We only handle simple comparisons of the form "$sym == constant"
-  // or "($sym+constant1) == constant2".
-  // The adjustment is "constant1" in the above expression. It's used to
-  // "slide" the solution range around for modular arithmetic. For example,
-  // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
-  // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
-  // the subclasses of SimpleConstraintManager to handle the adjustment.
-  llvm::APSInt Adjustment = WraparoundType.getZeroValue();
-  computeAdjustment(Sym, Adjustment);
-
-  // Convert the right-hand side integer as necessary.
-  APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int));
-  llvm::APSInt ConvertedInt = ComparisonType.convert(Int);
-
-  // Prefer unsigned comparisons.
-  if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
-      ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
-    Adjustment.setIsSigned(false);
-
-  switch (Op) {
-  default:
-    llvm_unreachable("invalid operation not caught by assertion above");
-
-  case BO_EQ:
-    return assumeSymEQ(State, Sym, ConvertedInt, Adjustment);
-
-  case BO_NE:
-    return assumeSymNE(State, Sym, ConvertedInt, Adjustment);
-
-  case BO_GT:
-    return assumeSymGT(State, Sym, ConvertedInt, Adjustment);
-
-  case BO_GE:
-    return assumeSymGE(State, Sym, ConvertedInt, Adjustment);
-
-  case BO_LT:
-    return assumeSymLT(State, Sym, ConvertedInt, Adjustment);
-
-  case BO_LE:
-    return assumeSymLE(State, Sym, ConvertedInt, Adjustment);
-  } // end switch
-}
-
-ProgramStateRef SimpleConstraintManager::assumeSymWithinInclusiveRange(
-    ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
-    const llvm::APSInt &To, bool InRange) {
-  // Get the type used for calculating wraparound.
-  BasicValueFactory &BVF = getBasicVals();
-  APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType());
-
-  llvm::APSInt Adjustment = WraparoundType.getZeroValue();
-  SymbolRef AdjustedSym = Sym;
-  computeAdjustment(AdjustedSym, Adjustment);
-
-  // Convert the right-hand side integer as necessary.
-  APSIntType ComparisonType = std::max(WraparoundType, APSIntType(From));
-  llvm::APSInt ConvertedFrom = ComparisonType.convert(From);
-  llvm::APSInt ConvertedTo = ComparisonType.convert(To);
-
-  // Prefer unsigned comparisons.
-  if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
-      ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
-    Adjustment.setIsSigned(false);
-
-  if (InRange)
-    return assumeSymbolWithinInclusiveRange(State, AdjustedSym, ConvertedFrom,
-                                            ConvertedTo, Adjustment);
-  return assumeSymbolOutOfInclusiveRange(State, AdjustedSym, ConvertedFrom,
-                                         ConvertedTo, Adjustment);
-}
-
 } // end of namespace ento
 
 } // end of namespace clang
diff --git a/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp b/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
index 28b43dd566d5c..82ce8b45fe781 100644
--- a/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ b/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -14,6 +14,7 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h"
 
 using namespace clang;
 using namespace ento;
@@ -44,6 +45,10 @@ public:
   ///  (integer) value, that value is returned. Otherwise, returns NULL.
   const llvm::APSInt *getKnownValue(ProgramStateRef state, SVal V) override;
 
+  /// Recursively descends into symbolic expressions and replaces symbols
+  /// with their known values (in the sense of the getKnownValue() method).
+  SVal simplifySVal(ProgramStateRef State, SVal V) override;
+
   SVal MakeSymIntVal(const SymExpr *LHS, BinaryOperator::Opcode op,
                      const llvm::APSInt &RHS, QualType resultTy);
 };
@@ -362,6 +367,9 @@ SVal SimpleSValBuilder::evalBinOpNN(ProgramStateRef state,
                              resultTy);
         case nonloc::ConcreteIntKind: {
           // Transform the integer into a location and compare.
+          // FIXME: This only makes sense for comparisons. If we want to, say,
+          // add 1 to a LocAsInteger, we'd better unpack the Loc and add to it,
+          // then pack it back into a LocAsInteger.
           llvm::APSInt i = rhs.castAs<nonloc::ConcreteInt>().getValue();
           BasicVals.getAPSIntType(Context.VoidPtrTy).apply(i);
           return evalBinOpLL(state, op, lhsL, makeLoc(i), resultTy);
@@ -534,11 +542,12 @@ SVal SimpleSValBuilder::evalBinOpNN(ProgramStateRef state,
       // Does the symbolic expression simplify to a constant?
       // If so, "fold" the constant by setting 'lhs' to a ConcreteInt
       // and try again.
-      ConstraintManager &CMgr = state->getConstraintManager();
-      if (const llvm::APSInt *Constant = CMgr.getSymVal(state, Sym)) {
-        lhs = nonloc::ConcreteInt(*Constant);
-        continue;
-      }
+      SVal simplifiedLhs = simplifySVal(state, lhs);
+      if (simplifiedLhs != lhs)
+        if (auto simplifiedLhsAsNonLoc = simplifiedLhs.getAs<NonLoc>()) {
+          lhs = *simplifiedLhsAsNonLoc;
+          continue;
+        }
 
       // Is the RHS a constant?
       if (const llvm::APSInt *RHSValue = getKnownValue(state, rhs))
@@ -941,20 +950,26 @@ SVal SimpleSValBuilder::evalBinOpLN(ProgramStateRef state,
   if (const MemRegion *region = lhs.getAsRegion()) {
     rhs = convertToArrayIndex(rhs).castAs<NonLoc>();
     SVal index = UnknownVal();
-    const MemRegion *superR = nullptr;
+    const SubRegion *superR = nullptr;
+    // We need to know the type of the pointer in order to add an integer to it.
+    // Depending on the type, different amount of bytes is added.
     QualType elementType;
 
     if (const ElementRegion *elemReg = dyn_cast<ElementRegion>(region)) {
       assert(op == BO_Add || op == BO_Sub);
       index = evalBinOpNN(state, op, elemReg->getIndex(), rhs,
                           getArrayIndexType());
-      superR = elemReg->getSuperRegion();
+      superR = cast<SubRegion>(elemReg->getSuperRegion());
       elementType = elemReg->getElementType();
     }
     else if (isa<SubRegion>(region)) {
       assert(op == BO_Add || op == BO_Sub);
       index = (op == BO_Add) ? rhs : evalMinus(rhs);
-      superR = region;
+      superR = cast<SubRegion>(region);
+      // TODO: Is this actually reliable? Maybe improving our MemRegion
+      // hierarchy to provide typed regions for all non-void pointers would be
+      // better. For instance, we cannot extend this towards LocAsInteger
+      // operations, where result type of the expression is integer.
       if (resultTy->isAnyPointerType())
         elementType = resultTy->getPointeeType();
     }
@@ -984,3 +999,74 @@ const llvm::APSInt *SimpleSValBuilder::getKnownValue(ProgramStateRef state,
   // FIXME: Add support for SymExprs.
   return nullptr;
 }
+
+SVal SimpleSValBuilder::simplifySVal(ProgramStateRef State, SVal V) {
+  // For now, this function tries to constant-fold symbols inside a
+  // nonloc::SymbolVal, and does nothing else. More simplifications should
+  // be possible, such as constant-folding an index in an ElementRegion.
+
+  class Simplifier : public FullSValVisitor<Simplifier, SVal> {
+    ProgramStateRef State;
+    SValBuilder &SVB;
+
+  public:
+    Simplifier(ProgramStateRef State)
+        : State(State), SVB(State->getStateManager().getSValBuilder()) {}
+
+    SVal VisitSymbolData(const SymbolData *S) {
+      if (const llvm::APSInt *I =
+              SVB.getKnownValue(State, nonloc::SymbolVal(S)))
+        return Loc::isLocType(S->getType()) ? (SVal)SVB.makeIntLocVal(*I)
+                                            : (SVal)SVB.makeIntVal(*I);
+      return nonloc::SymbolVal(S);
+    }
+
+    // TODO: Support SymbolCast. Support IntSymExpr when/if we actually
+    // start producing them.
+
+    SVal VisitSymIntExpr(const SymIntExpr *S) {
+      SVal LHS = Visit(S->getLHS());
+      SVal RHS;
+      // By looking at the APSInt in the right-hand side of S, we cannot
+      // figure out if it should be treated as a Loc or as a NonLoc.
+      // So make our guess by recalling that we cannot multiply pointers
+      // or compare a pointer to an integer.
+      if (Loc::isLocType(S->getLHS()->getType()) &&
+          BinaryOperator::isComparisonOp(S->getOpcode())) {
+        // The usual conversion of $sym to &SymRegion{$sym}, as they have
+        // the same meaning for Loc-type symbols, but the latter form
+        // is preferred in SVal computations for being Loc itself.
+        if (SymbolRef Sym = LHS.getAsSymbol()) {
+          assert(Loc::isLocType(Sym->getType()));
+          LHS = SVB.makeLoc(Sym);
+        }
+        RHS = SVB.makeIntLocVal(S->getRHS());
+      } else {
+        RHS = SVB.makeIntVal(S->getRHS());
+      }
+      return SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType());
+    }
+
+    SVal VisitSymSymExpr(const SymSymExpr *S) {
+      SVal LHS = Visit(S->getLHS());
+      SVal RHS = Visit(S->getRHS());
+      return SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType());
+    }
+
+    SVal VisitSymExpr(SymbolRef S) { return nonloc::SymbolVal(S); }
+
+    SVal VisitMemRegion(const MemRegion *R) { return loc::MemRegionVal(R); }
+
+    SVal VisitNonLocSymbolVal(nonloc::SymbolVal V) {
+      // Simplification is much more costly than computing complexity.
+      // For high complexity, it may be not worth it.
+      if (V.getSymbol()->computeComplexity() > 100)
+        return V;
+      return Visit(V.getSymbol());
+    }
+
+    SVal VisitSVal(SVal V) { return V; }
+  };
+
+  return Simplifier(State).Visit(V);
+}
diff --git a/lib/StaticAnalyzer/Core/Store.cpp b/lib/StaticAnalyzer/Core/Store.cpp
index aca6e3b6255b8..ba48a60d5a1cc 100644
--- a/lib/StaticAnalyzer/Core/Store.cpp
+++ b/lib/StaticAnalyzer/Core/Store.cpp
@@ -42,8 +42,9 @@ StoreRef StoreManager::enterStackFrame(Store OldStore,
   return Store;
 }
 
-const MemRegion *StoreManager::MakeElementRegion(const MemRegion *Base,
-                                              QualType EleTy, uint64_t index) {
+const ElementRegion *StoreManager::MakeElementRegion(const SubRegion *Base,
+                                                     QualType EleTy,
+                                                     uint64_t index) {
   NonLoc idx = svalBuilder.makeArrayIndex(index);
   return MRMgr.getElementRegion(EleTy, idx, Base, svalBuilder.getContext());
 }
@@ -52,7 +53,7 @@ StoreRef StoreManager::BindDefault(Store store, const MemRegion *R, SVal V) {
   return StoreRef(store, *this);
 }
 
-const ElementRegion *StoreManager::GetElementZeroRegion(const MemRegion *R,
+const ElementRegion *StoreManager::GetElementZeroRegion(const SubRegion *R,
                                                         QualType T) {
   NonLoc idx = svalBuilder.makeZeroArrayIndex();
   assert(!T.isNull());
@@ -126,7 +127,7 @@ const MemRegion *StoreManager::castRegion(const MemRegion *R, QualType CastToTy)
     case MemRegion::VarRegionKind:
     case MemRegion::CXXTempObjectRegionKind:
     case MemRegion::CXXBaseObjectRegionKind:
-      return MakeElementRegion(R, PointeeTy);
+      return MakeElementRegion(cast<SubRegion>(R), PointeeTy);
 
     case MemRegion::ElementRegionKind: {
       // If we are casting from an ElementRegion to another type, the
@@ -171,7 +172,7 @@ const MemRegion *StoreManager::castRegion(const MemRegion *R, QualType CastToTy)
         }
 
         // Otherwise, create a new ElementRegion at offset 0.
-        return MakeElementRegion(baseR, PointeeTy);
+        return MakeElementRegion(cast<SubRegion>(baseR), PointeeTy);
       }
 
       // We have a non-zero offset from the base region.  We want to determine
@@ -202,10 +203,11 @@ const MemRegion *StoreManager::castRegion(const MemRegion *R, QualType CastToTy)
       if (!newSuperR) {
         // Create an intermediate ElementRegion to represent the raw byte.
         // This will be the super region of the final ElementRegion.
-        newSuperR = MakeElementRegion(baseR, Ctx.CharTy, off.getQuantity());
+        newSuperR = MakeElementRegion(cast<SubRegion>(baseR), Ctx.CharTy,
+                                      off.getQuantity());
       }
 
-      return MakeElementRegion(newSuperR, PointeeTy, newIndex);
+      return MakeElementRegion(cast<SubRegion>(newSuperR), PointeeTy, newIndex);
     }
   }
 
@@ -271,9 +273,8 @@ SVal StoreManager::evalDerivedToBase(SVal Derived, QualType BaseType,
     BaseDecl = BaseType->getAsCXXRecordDecl();
   assert(BaseDecl && "not a C++ object?");
 
-  const MemRegion *BaseReg =
-    MRMgr.getCXXBaseObjectRegion(BaseDecl, DerivedRegVal->getRegion(),
-                                 IsVirtual);
+  const MemRegion *BaseReg = MRMgr.getCXXBaseObjectRegion(
+      BaseDecl, cast<SubRegion>(DerivedRegVal->getRegion()), IsVirtual);
 
   return loc::MemRegionVal(BaseReg);
 }
@@ -390,11 +391,11 @@ SVal StoreManager::getLValueFieldOrIvar(const Decl *D, SVal Base) {
     return Base;
 
   Loc BaseL = Base.castAs<Loc>();
-  const MemRegion* BaseR = nullptr;
+  const SubRegion* BaseR = nullptr;
 
   switch (BaseL.getSubKind()) {
   case loc::MemRegionValKind:
-    BaseR = BaseL.castAs<loc::MemRegionVal>().getRegion();
+    BaseR = cast<SubRegion>(BaseL.castAs<loc::MemRegionVal>().getRegion());
     break;
 
   case loc::GotoLabelKind:
@@ -434,7 +435,8 @@ SVal StoreManager::getLValueElement(QualType elementType, NonLoc Offset,
   if (Base.isUnknownOrUndef() || Base.getAs<loc::ConcreteInt>())
     return Base;
 
-  const MemRegion* BaseRegion = Base.castAs<loc::MemRegionVal>().getRegion();
+  const SubRegion *BaseRegion =
+      Base.castAs<loc::MemRegionVal>().getRegionAs<SubRegion>();
 
   // Pointer of any type can be cast and used as array base.
   const ElementRegion *ElemR = dyn_cast<ElementRegion>(BaseRegion);
@@ -471,9 +473,8 @@ SVal StoreManager::getLValueElement(QualType elementType, NonLoc Offset,
     if (isa<ElementRegion>(BaseRegion->StripCasts()))
       return UnknownVal();
 
-    return loc::MemRegionVal(MRMgr.getElementRegion(elementType, Offset,
-                                                    ElemR->getSuperRegion(),
-                                                    Ctx));
+    return loc::MemRegionVal(MRMgr.getElementRegion(
+        elementType, Offset, cast<SubRegion>(ElemR->getSuperRegion()), Ctx));
   }
 
   const llvm::APSInt& OffI = Offset.castAs<nonloc::ConcreteInt>().getValue();
@@ -484,7 +485,7 @@ SVal StoreManager::getLValueElement(QualType elementType, NonLoc Offset,
                                                                     OffI));
 
   // Construct the new ElementRegion.
-  const MemRegion *ArrayR = ElemR->getSuperRegion();
+  const SubRegion *ArrayR = cast<SubRegion>(ElemR->getSuperRegion());
   return loc::MemRegionVal(MRMgr.getElementRegion(elementType, NewIdx, ArrayR,
                                                   Ctx));
 }
diff --git a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
new file mode 100644
index 0000000000000..f9f9057a89cd7
--- /dev/null
+++ b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -0,0 +1,1618 @@
+//== Z3ConstraintManager.cpp --------------------------------*- C++ -*--==//
+//
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Basic/TargetInfo.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
+
+#include "clang/Config/config.h"
+
+using namespace clang;
+using namespace ento;
+
+#if CLANG_ANALYZER_WITH_Z3
+
+#include <z3.h>
+
+// Forward declarations
+namespace {
+class Z3Expr;
+class ConstraintZ3 {};
+} // end anonymous namespace
+
+typedef llvm::ImmutableSet<std::pair<SymbolRef, Z3Expr>> ConstraintZ3Ty;
+
+// Expansion of REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintZ3, Z3SetPair)
+namespace clang {
+namespace ento {
+template <>
+struct ProgramStateTrait<ConstraintZ3>
+    : public ProgramStatePartialTrait<ConstraintZ3Ty> {
+  static void *GDMIndex() {
+    static int Index;
+    return &Index;
+  }
+};
+} // end namespace ento
+} // end namespace clang
+
+namespace {
+
+class Z3Config {
+  friend class Z3Context;
+
+  Z3_config Config;
+
+public:
+  Z3Config() : Config(Z3_mk_config()) {
+    // Enable model finding
+    Z3_set_param_value(Config, "model", "true");
+    // Disable proof generation
+    Z3_set_param_value(Config, "proof", "false");
+    // Set timeout to 15000ms = 15s
+    Z3_set_param_value(Config, "timeout", "15000");
+  }
+
+  ~Z3Config() { Z3_del_config(Config); }
+}; // end class Z3Config
+
+class Z3Context {
+  Z3_context ZC_P;
+
+public:
+  static Z3_context ZC;
+
+  Z3Context() : ZC_P(Z3_mk_context_rc(Z3Config().Config)) { ZC = ZC_P; }
+
+  ~Z3Context() {
+    Z3_del_context(ZC);
+    Z3_finalize_memory();
+    ZC_P = nullptr;
+  }
+}; // end class Z3Context
+
+class Z3Sort {
+  friend class Z3Expr;
+
+  Z3_sort Sort;
+
+  Z3Sort() : Sort(nullptr) {}
+  Z3Sort(Z3_sort ZS) : Sort(ZS) {
+    Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
+  }
+
+public:
+  /// Override implicit copy constructor for correct reference counting.
+  Z3Sort(const Z3Sort &Copy) : Sort(Copy.Sort) {
+    Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
+  }
+
+  /// Provide move constructor
+  Z3Sort(Z3Sort &&Move) : Sort(nullptr) { *this = std::move(Move); }
+
+  /// Provide move assignment constructor
+  Z3Sort &operator=(Z3Sort &&Move) {
+    if (this != &Move) {
+      if (Sort)
+        Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
+      Sort = Move.Sort;
+      Move.Sort = nullptr;
+    }
+    return *this;
+  }
+
+  ~Z3Sort() {
+    if (Sort)
+      Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
+  }
+
+  // Return a boolean sort.
+  static Z3Sort getBoolSort() { return Z3Sort(Z3_mk_bool_sort(Z3Context::ZC)); }
+
+  // Return an appropriate bitvector sort for the given bitwidth.
+  static Z3Sort getBitvectorSort(unsigned BitWidth) {
+    return Z3Sort(Z3_mk_bv_sort(Z3Context::ZC, BitWidth));
+  }
+
+  // Return an appropriate floating-point sort for the given bitwidth.
+  static Z3Sort getFloatSort(unsigned BitWidth) {
+    Z3_sort Sort;
+
+    switch (BitWidth) {
+    default:
+      llvm_unreachable("Unsupported floating-point bitwidth!");
+      break;
+    case 16:
+      Sort = Z3_mk_fpa_sort_16(Z3Context::ZC);
+      break;
+    case 32:
+      Sort = Z3_mk_fpa_sort_32(Z3Context::ZC);
+      break;
+    case 64:
+      Sort = Z3_mk_fpa_sort_64(Z3Context::ZC);
+      break;
+    case 128:
+      Sort = Z3_mk_fpa_sort_128(Z3Context::ZC);
+      break;
+    }
+    return Z3Sort(Sort);
+  }
+
+  // Return an appropriate sort for the given AST.
+  static Z3Sort getSort(Z3_ast AST) {
+    return Z3Sort(Z3_get_sort(Z3Context::ZC, AST));
+  }
+
+  Z3_sort_kind getSortKind() const {
+    return Z3_get_sort_kind(Z3Context::ZC, Sort);
+  }
+
+  unsigned getBitvectorSortSize() const {
+    assert(getSortKind() == Z3_BV_SORT && "Not a bitvector sort!");
+    return Z3_get_bv_sort_size(Z3Context::ZC, Sort);
+  }
+
+  unsigned getFloatSortSize() const {
+    assert(getSortKind() == Z3_FLOATING_POINT_SORT &&
+           "Not a floating-point sort!");
+    return Z3_fpa_get_ebits(Z3Context::ZC, Sort) +
+           Z3_fpa_get_sbits(Z3Context::ZC, Sort);
+  }
+
+  bool operator==(const Z3Sort &Other) const {
+    return Z3_is_eq_sort(Z3Context::ZC, Sort, Other.Sort);
+  }
+
+  Z3Sort &operator=(const Z3Sort &Move) {
+    Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Move.Sort));
+    Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
+    Sort = Move.Sort;
+    return *this;
+  }
+
+  void print(raw_ostream &OS) const {
+    OS << Z3_sort_to_string(Z3Context::ZC, Sort);
+  }
+
+  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
+}; // end class Z3Sort
+
+class Z3Expr {
+  friend class Z3Model;
+  friend class Z3Solver;
+
+  Z3_ast AST;
+
+  Z3Expr(Z3_ast ZA) : AST(ZA) { Z3_inc_ref(Z3Context::ZC, AST); }
+
+  // Return an appropriate floating-point rounding mode.
+  static Z3Expr getFloatRoundingMode() {
+    // TODO: Don't assume nearest ties to even rounding mode
+    return Z3Expr(Z3_mk_fpa_rne(Z3Context::ZC));
+  }
+
+  // Determine whether two float semantics are equivalent
+  static bool areEquivalent(const llvm::fltSemantics &LHS,
+                            const llvm::fltSemantics &RHS) {
+    return (llvm::APFloat::semanticsPrecision(LHS) ==
+            llvm::APFloat::semanticsPrecision(RHS)) &&
+           (llvm::APFloat::semanticsMinExponent(LHS) ==
+            llvm::APFloat::semanticsMinExponent(RHS)) &&
+           (llvm::APFloat::semanticsMaxExponent(LHS) ==
+            llvm::APFloat::semanticsMaxExponent(RHS)) &&
+           (llvm::APFloat::semanticsSizeInBits(LHS) ==
+            llvm::APFloat::semanticsSizeInBits(RHS));
+  }
+
+public:
+  /// Override implicit copy constructor for correct reference counting.
+  Z3Expr(const Z3Expr &Copy) : AST(Copy.AST) { Z3_inc_ref(Z3Context::ZC, AST); }
+
+  /// Provide move constructor
+  Z3Expr(Z3Expr &&Move) : AST(nullptr) { *this = std::move(Move); }
+
+  /// Provide move assignment constructor
+  Z3Expr &operator=(Z3Expr &&Move) {
+    if (this != &Move) {
+      if (AST)
+        Z3_dec_ref(Z3Context::ZC, AST);
+      AST = Move.AST;
+      Move.AST = nullptr;
+    }
+    return *this;
+  }
+
+  ~Z3Expr() {
+    if (AST)
+      Z3_dec_ref(Z3Context::ZC, AST);
+  }
+
+  /// Get the corresponding IEEE floating-point type for a given bitwidth.
+  static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
+    switch (BitWidth) {
+    default:
+      llvm_unreachable("Unsupported floating-point semantics!");
+      break;
+    case 16:
+      return llvm::APFloat::IEEEhalf();
+    case 32:
+      return llvm::APFloat::IEEEsingle();
+    case 64:
+      return llvm::APFloat::IEEEdouble();
+    case 128:
+      return llvm::APFloat::IEEEquad();
+    }
+  }
+
+  /// Construct a Z3Expr from a unary operator, given a Z3_context.
+  static Z3Expr fromUnOp(const UnaryOperator::Opcode Op, const Z3Expr &Exp) {
+    Z3_ast AST;
+
+    switch (Op) {
+    default:
+      llvm_unreachable("Unimplemented opcode");
+      break;
+
+    case UO_Minus:
+      AST = Z3_mk_bvneg(Z3Context::ZC, Exp.AST);
+      break;
+
+    case UO_Not:
+      AST = Z3_mk_bvnot(Z3Context::ZC, Exp.AST);
+      break;
+
+    case UO_LNot:
+      AST = Z3_mk_not(Z3Context::ZC, Exp.AST);
+      break;
+    }
+
+    return Z3Expr(AST);
+  }
+
+  /// Construct a Z3Expr from a floating-point unary operator, given a
+  /// Z3_context.
+  static Z3Expr fromFloatUnOp(const UnaryOperator::Opcode Op,
+                              const Z3Expr &Exp) {
+    Z3_ast AST;
+
+    switch (Op) {
+    default:
+      llvm_unreachable("Unimplemented opcode");
+      break;
+
+    case UO_Minus:
+      AST = Z3_mk_fpa_neg(Z3Context::ZC, Exp.AST);
+      break;
+
+    case UO_LNot:
+      return Z3Expr::fromUnOp(Op, Exp);
+    }
+
+    return Z3Expr(AST);
+  }
+
+  /// Construct a Z3Expr from a n-ary binary operator.
+  static Z3Expr fromNBinOp(const BinaryOperator::Opcode Op,
+                           const std::vector<Z3_ast> &ASTs) {
+    Z3_ast AST;
+
+    switch (Op) {
+    default:
+      llvm_unreachable("Unimplemented opcode");
+      break;
+
+    case BO_LAnd:
+      AST = Z3_mk_and(Z3Context::ZC, ASTs.size(), ASTs.data());
+      break;
+
+    case BO_LOr:
+      AST = Z3_mk_or(Z3Context::ZC, ASTs.size(), ASTs.data());
+      break;
+    }
+
+    return Z3Expr(AST);
+  }
+
+  /// Construct a Z3Expr from a binary operator, given a Z3_context.
+  static Z3Expr fromBinOp(const Z3Expr &LHS, const BinaryOperator::Opcode Op,
+                          const Z3Expr &RHS, bool isSigned) {
+    Z3_ast AST;
+
+    assert(Z3Sort::getSort(LHS.AST) == Z3Sort::getSort(RHS.AST) &&
+           "AST's must have the same sort!");
+
+    switch (Op) {
+    default:
+      llvm_unreachable("Unimplemented opcode");
+      break;
+
+    // Multiplicative operators
+    case BO_Mul:
+      AST = Z3_mk_bvmul(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+    case BO_Div:
+      AST = isSigned ? Z3_mk_bvsdiv(Z3Context::ZC, LHS.AST, RHS.AST)
+                     : Z3_mk_bvudiv(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+    case BO_Rem:
+      AST = isSigned ? Z3_mk_bvsrem(Z3Context::ZC, LHS.AST, RHS.AST)
+                     : Z3_mk_bvurem(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+
+    // Additive operators
+    case BO_Add:
+      AST = Z3_mk_bvadd(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+    case BO_Sub:
+      AST = Z3_mk_bvsub(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+
+    // Bitwise shift operators
+    case BO_Shl:
+      AST = Z3_mk_bvshl(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+    case BO_Shr:
+      AST = isSigned ? Z3_mk_bvashr(Z3Context::ZC, LHS.AST, RHS.AST)
+                     : Z3_mk_bvlshr(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+
+    // Relational operators
+    case BO_LT:
+      AST = isSigned ? Z3_mk_bvslt(Z3Context::ZC, LHS.AST, RHS.AST)
+                     : Z3_mk_bvult(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+    case BO_GT:
+      AST = isSigned ? Z3_mk_bvsgt(Z3Context::ZC, LHS.AST, RHS.AST)
+                     : Z3_mk_bvugt(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+    case BO_LE:
+      AST = isSigned ? Z3_mk_bvsle(Z3Context::ZC, LHS.AST, RHS.AST)
+                     : Z3_mk_bvule(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+    case BO_GE:
+      AST = isSigned ? Z3_mk_bvsge(Z3Context::ZC, LHS.AST, RHS.AST)
+                     : Z3_mk_bvuge(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+
+    // Equality operators
+    case BO_EQ:
+      AST = Z3_mk_eq(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+    case BO_NE:
+      return Z3Expr::fromUnOp(UO_LNot,
+                              Z3Expr::fromBinOp(LHS, BO_EQ, RHS, isSigned));
+      break;
+
+    // Bitwise operators
+    case BO_And:
+      AST = Z3_mk_bvand(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+    case BO_Xor:
+      AST = Z3_mk_bvxor(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+    case BO_Or:
+      AST = Z3_mk_bvor(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+
+    // Logical operators
+    case BO_LAnd:
+    case BO_LOr: {
+      std::vector<Z3_ast> Args = {LHS.AST, RHS.AST};
+      return Z3Expr::fromNBinOp(Op, Args);
+    }
+    }
+
+    return Z3Expr(AST);
+  }
+
+  /// Construct a Z3Expr from a special floating-point binary operator, given
+  /// a Z3_context.
+  static Z3Expr fromFloatSpecialBinOp(const Z3Expr &LHS,
+                                      const BinaryOperator::Opcode Op,
+                                      const llvm::APFloat::fltCategory &RHS) {
+    Z3_ast AST;
+
+    switch (Op) {
+    default:
+      llvm_unreachable("Unimplemented opcode");
+      break;
+
+    // Equality operators
+    case BO_EQ:
+      switch (RHS) {
+      case llvm::APFloat::fcInfinity:
+        AST = Z3_mk_fpa_is_infinite(Z3Context::ZC, LHS.AST);
+        break;
+      case llvm::APFloat::fcNaN:
+        AST = Z3_mk_fpa_is_nan(Z3Context::ZC, LHS.AST);
+        break;
+      case llvm::APFloat::fcNormal:
+        AST = Z3_mk_fpa_is_normal(Z3Context::ZC, LHS.AST);
+        break;
+      case llvm::APFloat::fcZero:
+        AST = Z3_mk_fpa_is_zero(Z3Context::ZC, LHS.AST);
+        break;
+      }
+      break;
+    case BO_NE:
+      return Z3Expr::fromFloatUnOp(
+          UO_LNot, Z3Expr::fromFloatSpecialBinOp(LHS, BO_EQ, RHS));
+      break;
+    }
+
+    return Z3Expr(AST);
+  }
+
+  /// Construct a Z3Expr from a floating-point binary operator, given a
+  /// Z3_context.
+  static Z3Expr fromFloatBinOp(const Z3Expr &LHS,
+                               const BinaryOperator::Opcode Op,
+                               const Z3Expr &RHS) {
+    Z3_ast AST;
+
+    assert(Z3Sort::getSort(LHS.AST) == Z3Sort::getSort(RHS.AST) &&
+           "AST's must have the same sort!");
+
+    switch (Op) {
+    default:
+      llvm_unreachable("Unimplemented opcode");
+      break;
+
+    // Multiplicative operators
+    case BO_Mul: {
+      Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
+      AST = Z3_mk_fpa_mul(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
+      break;
+    }
+    case BO_Div: {
+      Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
+      AST = Z3_mk_fpa_div(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
+      break;
+    }
+    case BO_Rem:
+      AST = Z3_mk_fpa_rem(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+
+    // Additive operators
+    case BO_Add: {
+      Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
+      AST = Z3_mk_fpa_add(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
+      break;
+    }
+    case BO_Sub: {
+      Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
+      AST = Z3_mk_fpa_sub(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
+      break;
+    }
+
+    // Relational operators
+    case BO_LT:
+      AST = Z3_mk_fpa_lt(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+    case BO_GT:
+      AST = Z3_mk_fpa_gt(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+    case BO_LE:
+      AST = Z3_mk_fpa_leq(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+    case BO_GE:
+      AST = Z3_mk_fpa_geq(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+
+    // Equality operators
+    case BO_EQ:
+      AST = Z3_mk_fpa_eq(Z3Context::ZC, LHS.AST, RHS.AST);
+      break;
+    case BO_NE:
+      return Z3Expr::fromFloatUnOp(UO_LNot,
+                                   Z3Expr::fromFloatBinOp(LHS, BO_EQ, RHS));
+      break;
+
+    // Logical operators
+    case BO_LAnd:
+    case BO_LOr:
+      return Z3Expr::fromBinOp(LHS, Op, RHS, false);
+    }
+
+    return Z3Expr(AST);
+  }
+
+  /// Construct a Z3Expr from a SymbolData, given a Z3_context.
+  static Z3Expr fromData(const SymbolID ID, bool isBool, bool isFloat,
+                         uint64_t BitWidth) {
+    llvm::Twine Name = "$" + llvm::Twine(ID);
+
+    Z3Sort Sort;
+    if (isBool)
+      Sort = Z3Sort::getBoolSort();
+    else if (isFloat)
+      Sort = Z3Sort::getFloatSort(BitWidth);
+    else
+      Sort = Z3Sort::getBitvectorSort(BitWidth);
+
+    Z3_symbol Symbol = Z3_mk_string_symbol(Z3Context::ZC, Name.str().c_str());
+    Z3_ast AST = Z3_mk_const(Z3Context::ZC, Symbol, Sort.Sort);
+    return Z3Expr(AST);
+  }
+
+  /// Construct a Z3Expr from a SymbolCast, given a Z3_context.
+  static Z3Expr fromCast(const Z3Expr &Exp, QualType ToTy, uint64_t ToBitWidth,
+                         QualType FromTy, uint64_t FromBitWidth) {
+    Z3_ast AST;
+
+    if ((FromTy->isIntegralOrEnumerationType() &&
+         ToTy->isIntegralOrEnumerationType()) ||
+        (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) ||
+        (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) ||
+        (FromTy->isReferenceType() ^ ToTy->isReferenceType())) {
+      // Special case: Z3 boolean type is distinct from bitvector type, so
+      // must use if-then-else expression instead of direct cast
+      if (FromTy->isBooleanType()) {
+        assert(ToBitWidth > 0 && "BitWidth must be positive!");
+        Z3Expr Zero = Z3Expr::fromInt("0", ToBitWidth);
+        Z3Expr One = Z3Expr::fromInt("1", ToBitWidth);
+        AST = Z3_mk_ite(Z3Context::ZC, Exp.AST, One.AST, Zero.AST);
+      } else if (ToBitWidth > FromBitWidth) {
+        AST = FromTy->isSignedIntegerOrEnumerationType()
+                  ? Z3_mk_sign_ext(Z3Context::ZC, ToBitWidth - FromBitWidth,
+                                   Exp.AST)
+                  : Z3_mk_zero_ext(Z3Context::ZC, ToBitWidth - FromBitWidth,
+                                   Exp.AST);
+      } else if (ToBitWidth < FromBitWidth) {
+        AST = Z3_mk_extract(Z3Context::ZC, ToBitWidth - 1, 0, Exp.AST);
+      } else {
+        // Both are bitvectors with the same width, ignore the type cast
+        return Exp;
+      }
+    } else if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {
+      if (ToBitWidth != FromBitWidth) {
+        Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
+        Z3Sort Sort = Z3Sort::getFloatSort(ToBitWidth);
+        AST = Z3_mk_fpa_to_fp_float(Z3Context::ZC, RoundingMode.AST, Exp.AST,
+                                    Sort.Sort);
+      } else {
+        return Exp;
+      }
+    } else if (FromTy->isIntegralOrEnumerationType() &&
+               ToTy->isRealFloatingType()) {
+      Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
+      Z3Sort Sort = Z3Sort::getFloatSort(ToBitWidth);
+      AST = FromTy->isSignedIntegerOrEnumerationType()
+                ? Z3_mk_fpa_to_fp_signed(Z3Context::ZC, RoundingMode.AST,
+                                         Exp.AST, Sort.Sort)
+                : Z3_mk_fpa_to_fp_unsigned(Z3Context::ZC, RoundingMode.AST,
+                                           Exp.AST, Sort.Sort);
+    } else if (FromTy->isRealFloatingType() &&
+               ToTy->isIntegralOrEnumerationType()) {
+      Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
+      AST = ToTy->isSignedIntegerOrEnumerationType()
+                ? Z3_mk_fpa_to_sbv(Z3Context::ZC, RoundingMode.AST, Exp.AST,
+                                   ToBitWidth)
+                : Z3_mk_fpa_to_ubv(Z3Context::ZC, RoundingMode.AST, Exp.AST,
+                                   ToBitWidth);
+    } else {
+      llvm_unreachable("Unsupported explicit type cast!");
+    }
+
+    return Z3Expr(AST);
+  }
+
+  /// Construct a Z3Expr from a boolean, given a Z3_context.
+  static Z3Expr fromBoolean(const bool Bool) {
+    Z3_ast AST = Bool ? Z3_mk_true(Z3Context::ZC) : Z3_mk_false(Z3Context::ZC);
+    return Z3Expr(AST);
+  }
+
+  /// Construct a Z3Expr from a finite APFloat, given a Z3_context.
+  static Z3Expr fromAPFloat(const llvm::APFloat &Float) {
+    Z3_ast AST;
+    Z3Sort Sort = Z3Sort::getFloatSort(
+        llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
+
+    llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), true);
+    Z3Expr Z3Int = Z3Expr::fromAPSInt(Int);
+    AST = Z3_mk_fpa_to_fp_bv(Z3Context::ZC, Z3Int.AST, Sort.Sort);
+
+    return Z3Expr(AST);
+  }
+
+  /// Construct a Z3Expr from an APSInt, given a Z3_context.
+  static Z3Expr fromAPSInt(const llvm::APSInt &Int) {
+    Z3Sort Sort = Z3Sort::getBitvectorSort(Int.getBitWidth());
+    Z3_ast AST =
+        Z3_mk_numeral(Z3Context::ZC, Int.toString(10).c_str(), Sort.Sort);
+    return Z3Expr(AST);
+  }
+
+  /// Construct a Z3Expr from an integer, given a Z3_context.
+  static Z3Expr fromInt(const char *Int, uint64_t BitWidth) {
+    Z3Sort Sort = Z3Sort::getBitvectorSort(BitWidth);
+    Z3_ast AST = Z3_mk_numeral(Z3Context::ZC, Int, Sort.Sort);
+    return Z3Expr(AST);
+  }
+
+  /// Construct an APFloat from a Z3Expr, given the AST representation
+  static bool toAPFloat(const Z3Sort &Sort, const Z3_ast &AST,
+                        llvm::APFloat &Float, bool useSemantics = true) {
+    assert(Sort.getSortKind() == Z3_FLOATING_POINT_SORT &&
+           "Unsupported sort to floating-point!");
+
+    llvm::APSInt Int(Sort.getFloatSortSize(), true);
+    const llvm::fltSemantics &Semantics =
+        Z3Expr::getFloatSemantics(Sort.getFloatSortSize());
+    Z3Sort BVSort = Z3Sort::getBitvectorSort(Sort.getFloatSortSize());
+    if (!Z3Expr::toAPSInt(BVSort, AST, Int, true)) {
+      return false;
+    }
+
+    if (useSemantics &&
+        !Z3Expr::areEquivalent(Float.getSemantics(), Semantics)) {
+      assert(false && "Floating-point types don't match!");
+      return false;
+    }
+
+    Float = llvm::APFloat(Semantics, Int);
+    return true;
+  }
+
+  /// Construct an APSInt from a Z3Expr, given the AST representation
+  static bool toAPSInt(const Z3Sort &Sort, const Z3_ast &AST, llvm::APSInt &Int,
+                       bool useSemantics = true) {
+    switch (Sort.getSortKind()) {
+    default:
+      llvm_unreachable("Unsupported sort to integer!");
+    case Z3_BV_SORT: {
+      if (useSemantics && Int.getBitWidth() != Sort.getBitvectorSortSize()) {
+        assert(false && "Bitvector types don't match!");
+        return false;
+      }
+
+      uint64_t Value[2];
+      // Force cast because Z3 defines __uint64 to be a unsigned long long
+      // type, which isn't compatible with a unsigned long type, even if they
+      // are the same size.
+      Z3_get_numeral_uint64(Z3Context::ZC, AST,
+                            reinterpret_cast<__uint64 *>(&Value[0]));
+      if (Sort.getBitvectorSortSize() <= 64) {
+        Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]), true);
+      } else if (Sort.getBitvectorSortSize() == 128) {
+        Z3Expr ASTHigh = Z3Expr(Z3_mk_extract(Z3Context::ZC, 127, 64, AST));
+        Z3_get_numeral_uint64(Z3Context::ZC, AST,
+                              reinterpret_cast<__uint64 *>(&Value[1]));
+        Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), true);
+      } else {
+        assert(false && "Bitwidth not supported!");
+        return false;
+      }
+      return true;
+    }
+    case Z3_BOOL_SORT:
+      if (useSemantics && Int.getBitWidth() < 1) {
+        assert(false && "Boolean type doesn't match!");
+        return false;
+      }
+      Int = llvm::APSInt(
+          llvm::APInt(Int.getBitWidth(),
+                      Z3_get_bool_value(Z3Context::ZC, AST) == Z3_L_TRUE ? 1
+                                                                         : 0),
+          true);
+      return true;
+    }
+  }
+
+  void Profile(llvm::FoldingSetNodeID &ID) const {
+    ID.AddInteger(Z3_get_ast_hash(Z3Context::ZC, AST));
+  }
+
+  bool operator<(const Z3Expr &Other) const {
+    llvm::FoldingSetNodeID ID1, ID2;
+    Profile(ID1);
+    Other.Profile(ID2);
+    return ID1 < ID2;
+  }
+
+  /// Comparison of AST equality, not model equivalence.
+  bool operator==(const Z3Expr &Other) const {
+    assert(Z3_is_eq_sort(Z3Context::ZC, Z3_get_sort(Z3Context::ZC, AST),
+                         Z3_get_sort(Z3Context::ZC, Other.AST)) &&
+           "AST's must have the same sort");
+    return Z3_is_eq_ast(Z3Context::ZC, AST, Other.AST);
+  }
+
+  /// Override implicit move constructor for correct reference counting.
+  Z3Expr &operator=(const Z3Expr &Move) {
+    Z3_inc_ref(Z3Context::ZC, Move.AST);
+    Z3_dec_ref(Z3Context::ZC, AST);
+    AST = Move.AST;
+    return *this;
+  }
+
+  void print(raw_ostream &OS) const {
+    OS << Z3_ast_to_string(Z3Context::ZC, AST);
+  }
+
+  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
+}; // end class Z3Expr
+
+class Z3Model {
+  Z3_model Model;
+
+public:
+  Z3Model(Z3_model ZM) : Model(ZM) { Z3_model_inc_ref(Z3Context::ZC, Model); }
+
+  /// Override implicit copy constructor for correct reference counting.
+  Z3Model(const Z3Model &Copy) : Model(Copy.Model) {
+    Z3_model_inc_ref(Z3Context::ZC, Model);
+  }
+
+  /// Provide move constructor
+  Z3Model(Z3Model &&Move) : Model(nullptr) { *this = std::move(Move); }
+
+  /// Provide move assignment constructor
+  Z3Model &operator=(Z3Model &&Move) {
+    if (this != &Move) {
+      if (Model)
+        Z3_model_dec_ref(Z3Context::ZC, Model);
+      Model = Move.Model;
+      Move.Model = nullptr;
+    }
+    return *this;
+  }
+
+  ~Z3Model() {
+    if (Model)
+      Z3_model_dec_ref(Z3Context::ZC, Model);
+  }
+
+  /// Given an expression, extract the value of this operand in the model.
+  bool getInterpretation(const Z3Expr &Exp, llvm::APSInt &Int) const {
+    Z3_func_decl Func =
+        Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST));
+    if (Z3_model_has_interp(Z3Context::ZC, Model, Func) != Z3_L_TRUE)
+      return false;
+
+    Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model, Func);
+    Z3Sort Sort = Z3Sort::getSort(Assign);
+    return Z3Expr::toAPSInt(Sort, Assign, Int, true);
+  }
+
+  /// Given an expression, extract the value of this operand in the model.
+  bool getInterpretation(const Z3Expr &Exp, llvm::APFloat &Float) const {
+    Z3_func_decl Func =
+        Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST));
+    if (Z3_model_has_interp(Z3Context::ZC, Model, Func) != Z3_L_TRUE)
+      return false;
+
+    Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model, Func);
+    Z3Sort Sort = Z3Sort::getSort(Assign);
+    return Z3Expr::toAPFloat(Sort, Assign, Float, true);
+  }
+
+  void print(raw_ostream &OS) const {
+    OS << Z3_model_to_string(Z3Context::ZC, Model);
+  }
+
+  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
+}; // end class Z3Model
+
+class Z3Solver {
+  friend class Z3ConstraintManager;
+
+  Z3_solver Solver;
+
+  Z3Solver(Z3_solver ZS) : Solver(ZS) {
+    Z3_solver_inc_ref(Z3Context::ZC, Solver);
+  }
+
+public:
+  /// Override implicit copy constructor for correct reference counting.
+  Z3Solver(const Z3Solver &Copy) : Solver(Copy.Solver) {
+    Z3_solver_inc_ref(Z3Context::ZC, Solver);
+  }
+
+  /// Provide move constructor
+  Z3Solver(Z3Solver &&Move) : Solver(nullptr) { *this = std::move(Move); }
+
+  /// Provide move assignment constructor
+  Z3Solver &operator=(Z3Solver &&Move) {
+    if (this != &Move) {
+      if (Solver)
+        Z3_solver_dec_ref(Z3Context::ZC, Solver);
+      Solver = Move.Solver;
+      Move.Solver = nullptr;
+    }
+    return *this;
+  }
+
+  ~Z3Solver() {
+    if (Solver)
+      Z3_solver_dec_ref(Z3Context::ZC, Solver);
+  }
+
+  /// Given a constraint, add it to the solver
+  void addConstraint(const Z3Expr &Exp) {
+    Z3_solver_assert(Z3Context::ZC, Solver, Exp.AST);
+  }
+
+  /// Given a program state, construct the logical conjunction and add it to
+  /// the solver
+  void addStateConstraints(ProgramStateRef State) {
+    // TODO: Don't add all the constraints, only the relevant ones
+    ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
+    ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end();
+
+    // Construct the logical AND of all the constraints
+    if (I != IE) {
+      std::vector<Z3_ast> ASTs;
+
+      while (I != IE)
+        ASTs.push_back(I++->second.AST);
+
+      Z3Expr Conj = Z3Expr::fromNBinOp(BO_LAnd, ASTs);
+      addConstraint(Conj);
+    }
+  }
+
+  /// Check if the constraints are satisfiable
+  Z3_lbool check() { return Z3_solver_check(Z3Context::ZC, Solver); }
+
+  /// Push the current solver state
+  void push() { return Z3_solver_push(Z3Context::ZC, Solver); }
+
+  /// Pop the previous solver state
+  void pop(unsigned NumStates = 1) {
+    assert(Z3_solver_get_num_scopes(Z3Context::ZC, Solver) >= NumStates);
+    return Z3_solver_pop(Z3Context::ZC, Solver, NumStates);
+  }
+
+  /// Get a model from the solver. Caller should check the model is
+  /// satisfiable.
+  Z3Model getModel() {
+    return Z3Model(Z3_solver_get_model(Z3Context::ZC, Solver));
+  }
+
+  /// Reset the solver and remove all constraints.
+  void reset() { Z3_solver_reset(Z3Context::ZC, Solver); }
+}; // end class Z3Solver
+
+void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
+  llvm::report_fatal_error("Z3 error: " +
+                           llvm::Twine(Z3_get_error_msg_ex(Context, Error)));
+}
+
+class Z3ConstraintManager : public SimpleConstraintManager {
+  Z3Context Context;
+  mutable Z3Solver Solver;
+
+public:
+  Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
+      : SimpleConstraintManager(SE, SB),
+        Solver(Z3_mk_simple_solver(Z3Context::ZC)) {
+    Z3_set_error_handler(Z3Context::ZC, Z3ErrorHandler);
+  }
+
+  //===------------------------------------------------------------------===//
+  // Implementation for interface from ConstraintManager.
+  //===------------------------------------------------------------------===//
+
+  bool canReasonAbout(SVal X) const override;
+
+  ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
+
+  const llvm::APSInt *getSymVal(ProgramStateRef State,
+                                SymbolRef Sym) const override;
+
+  ProgramStateRef removeDeadBindings(ProgramStateRef St,
+                                     SymbolReaper &SymReaper) override;
+
+  void print(ProgramStateRef St, raw_ostream &Out, const char *nl,
+             const char *sep) override;
+
+  //===------------------------------------------------------------------===//
+  // Implementation for interface from SimpleConstraintManager.
+  //===------------------------------------------------------------------===//
+
+  ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym,
+                            bool Assumption) override;
+
+  ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
+                                          const llvm::APSInt &From,
+                                          const llvm::APSInt &To,
+                                          bool InRange) override;
+
+  ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
+                                       bool Assumption) override;
+
+private:
+  //===------------------------------------------------------------------===//
+  // Internal implementation.
+  //===------------------------------------------------------------------===//
+
+  // Check whether a new model is satisfiable, and update the program state.
+  ProgramStateRef assumeZ3Expr(ProgramStateRef State, SymbolRef Sym,
+                               const Z3Expr &Exp);
+
+  // Generate and check a Z3 model, using the given constraint.
+  Z3_lbool checkZ3Model(ProgramStateRef State, const Z3Expr &Exp) const;
+
+  // Generate a Z3Expr that represents the given symbolic expression.
+  // Sets the hasComparison parameter if the expression has a comparison
+  // operator.
+  // Sets the RetTy parameter to the final return type after promotions and
+  // casts.
+  Z3Expr getZ3Expr(SymbolRef Sym, QualType *RetTy = nullptr,
+                   bool *hasComparison = nullptr) const;
+
+  // Generate a Z3Expr that takes the logical not of an expression.
+  Z3Expr getZ3NotExpr(const Z3Expr &Exp) const;
+
+  // Generate a Z3Expr that compares the expression to zero.
+  Z3Expr getZ3ZeroExpr(const Z3Expr &Exp, QualType RetTy,
+                       bool Assumption) const;
+
+  // Recursive implementation to unpack and generate symbolic expression.
+  // Sets the hasComparison and RetTy parameters. See getZ3Expr().
+  Z3Expr getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
+                      bool *hasComparison) const;
+
+  // Wrapper to generate Z3Expr from SymbolData.
+  Z3Expr getZ3DataExpr(const SymbolID ID, QualType Ty) const;
+
+  // Wrapper to generate Z3Expr from SymbolCast.
+  Z3Expr getZ3CastExpr(const Z3Expr &Exp, QualType FromTy, QualType Ty) const;
+
+  // Wrapper to generate Z3Expr from BinarySymExpr.
+  // Sets the hasComparison and RetTy parameters. See getZ3Expr().
+  Z3Expr getZ3SymBinExpr(const BinarySymExpr *BSE, bool *hasComparison,
+                         QualType *RetTy) const;
+
+  // Wrapper to generate Z3Expr from unpacked binary symbolic expression.
+  // Sets the RetTy parameter. See getZ3Expr().
+  Z3Expr getZ3BinExpr(const Z3Expr &LHS, QualType LTy,
+                      BinaryOperator::Opcode Op, const Z3Expr &RHS,
+                      QualType RTy, QualType *RetTy) const;
+
+  //===------------------------------------------------------------------===//
+  // Helper functions.
+  //===------------------------------------------------------------------===//
+
+  // Recover the QualType of an APSInt.
+  // TODO: Refactor to put elsewhere
+  QualType getAPSIntType(const llvm::APSInt &Int) const;
+
+  // Perform implicit type conversion on binary symbolic expressions.
+  // May modify all input parameters.
+  // TODO: Refactor to use built-in conversion functions
+  void doTypeConversion(Z3Expr &LHS, Z3Expr &RHS, QualType &LTy,
+                        QualType &RTy) const;
+
+  // Perform implicit integer type conversion.
+  // May modify all input parameters.
+  // TODO: Refactor to use Sema::handleIntegerConversion()
+  template <typename T,
+            T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
+  void doIntTypeConversion(T &LHS, QualType &LTy, T &RHS, QualType &RTy) const;
+
+  // Perform implicit floating-point type conversion.
+  // May modify all input parameters.
+  // TODO: Refactor to use Sema::handleFloatConversion()
+  template <typename T,
+            T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
+  void doFloatTypeConversion(T &LHS, QualType &LTy, T &RHS,
+                             QualType &RTy) const;
+
+  // Callback function for doCast parameter on APSInt type.
+  static llvm::APSInt castAPSInt(const llvm::APSInt &V, QualType ToTy,
+                                 uint64_t ToWidth, QualType FromTy,
+                                 uint64_t FromWidth);
+}; // end class Z3ConstraintManager
+
+Z3_context Z3Context::ZC;
+
+} // end anonymous namespace
+
+ProgramStateRef Z3ConstraintManager::assumeSym(ProgramStateRef State,
+                                               SymbolRef Sym, bool Assumption) {
+  QualType RetTy;
+  bool hasComparison;
+
+  Z3Expr Exp = getZ3Expr(Sym, &RetTy, &hasComparison);
+  // Create zero comparison for implicit boolean cast, with reversed assumption
+  if (!hasComparison && !RetTy->isBooleanType())
+    return assumeZ3Expr(State, Sym, getZ3ZeroExpr(Exp, RetTy, !Assumption));
+
+  return assumeZ3Expr(State, Sym, Assumption ? Exp : getZ3NotExpr(Exp));
+}
+
+ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange(
+    ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
+    const llvm::APSInt &To, bool InRange) {
+  QualType RetTy;
+  // The expression may be casted, so we cannot call getZ3DataExpr() directly
+  Z3Expr Exp = getZ3Expr(Sym, &RetTy);
+
+  assert((getAPSIntType(From) == getAPSIntType(To)) &&
+         "Range values have different types!");
+  QualType RTy = getAPSIntType(From);
+  bool isSignedTy = RetTy->isSignedIntegerOrEnumerationType();
+  Z3Expr FromExp = Z3Expr::fromAPSInt(From);
+  Z3Expr ToExp = Z3Expr::fromAPSInt(To);
+
+  // Construct single (in)equality
+  if (From == To)
+    return assumeZ3Expr(State, Sym,
+                        getZ3BinExpr(Exp, RetTy, InRange ? BO_EQ : BO_NE,
+                                     FromExp, RTy, nullptr));
+
+  // Construct two (in)equalities, and a logical and/or
+  Z3Expr LHS =
+      getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, RTy, nullptr);
+  Z3Expr RHS =
+      getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, RTy, nullptr);
+  return assumeZ3Expr(
+      State, Sym,
+      Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS, isSignedTy));
+}
+
+ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State,
+                                                          SymbolRef Sym,
+                                                          bool Assumption) {
+  // Skip anything that is unsupported
+  return State;
+}
+
+bool Z3ConstraintManager::canReasonAbout(SVal X) const {
+  const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
+
+  Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
+  if (!SymVal)
+    return true;
+
+  const SymExpr *Sym = SymVal->getSymbol();
+  do {
+    QualType Ty = Sym->getType();
+
+    // Complex types are not modeled
+    if (Ty->isComplexType() || Ty->isComplexIntegerType())
+      return false;
+
+    // Non-IEEE 754 floating-point types are not modeled
+    if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
+         (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
+          &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
+      return false;
+
+    if (isa<SymbolData>(Sym)) {
+      break;
+    } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
+      Sym = SC->getOperand();
+    } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
+      if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
+        Sym = SIE->getLHS();
+      } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
+        Sym = ISE->getRHS();
+      } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
+        return canReasonAbout(nonloc::SymbolVal(SSM->getLHS())) &&
+               canReasonAbout(nonloc::SymbolVal(SSM->getRHS()));
+      } else {
+        llvm_unreachable("Unsupported binary expression to reason about!");
+      }
+    } else {
+      llvm_unreachable("Unsupported expression to reason about!");
+    }
+  } while (Sym);
+
+  return true;
+}
+
+ConditionTruthVal Z3ConstraintManager::checkNull(ProgramStateRef State,
+                                                 SymbolRef Sym) {
+  QualType RetTy;
+  // The expression may be casted, so we cannot call getZ3DataExpr() directly
+  Z3Expr VarExp = getZ3Expr(Sym, &RetTy);
+  Z3Expr Exp = getZ3ZeroExpr(VarExp, RetTy, true);
+  // Negate the constraint
+  Z3Expr NotExp = getZ3ZeroExpr(VarExp, RetTy, false);
+
+  Solver.reset();
+  Solver.addStateConstraints(State);
+
+  Solver.push();
+  Solver.addConstraint(Exp);
+  Z3_lbool isSat = Solver.check();
+
+  Solver.pop();
+  Solver.addConstraint(NotExp);
+  Z3_lbool isNotSat = Solver.check();
+
+  // Zero is the only possible solution
+  if (isSat == Z3_L_TRUE && isNotSat == Z3_L_FALSE)
+    return true;
+  // Zero is not a solution
+  else if (isSat == Z3_L_FALSE && isNotSat == Z3_L_TRUE)
+    return false;
+
+  // Zero may be a solution
+  return ConditionTruthVal();
+}
+
+const llvm::APSInt *Z3ConstraintManager::getSymVal(ProgramStateRef State,
+                                                   SymbolRef Sym) const {
+  BasicValueFactory &BV = getBasicVals();
+  ASTContext &Ctx = BV.getContext();
+
+  if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
+    QualType Ty = Sym->getType();
+    assert(!Ty->isRealFloatingType());
+    llvm::APSInt Value(Ctx.getTypeSize(Ty),
+                       !Ty->isSignedIntegerOrEnumerationType());
+
+    Z3Expr Exp = getZ3DataExpr(SD->getSymbolID(), Ty);
+
+    Solver.reset();
+    Solver.addStateConstraints(State);
+
+    // Constraints are unsatisfiable
+    if (Solver.check() != Z3_L_TRUE)
+      return nullptr;
+
+    Z3Model Model = Solver.getModel();
+    // Model does not assign interpretation
+    if (!Model.getInterpretation(Exp, Value))
+      return nullptr;
+
+    // A value has been obtained, check if it is the only value
+    Z3Expr NotExp = Z3Expr::fromBinOp(
+        Exp, BO_NE,
+        Ty->isBooleanType() ? Z3Expr::fromBoolean(Value.getBoolValue())
+                            : Z3Expr::fromAPSInt(Value),
+        false);
+
+    Solver.addConstraint(NotExp);
+    if (Solver.check() == Z3_L_TRUE)
+      return nullptr;
+
+    // This is the only solution, store it
+    return &BV.getValue(Value);
+  } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
+    SymbolRef CastSym = SC->getOperand();
+    QualType CastTy = SC->getType();
+    // Skip the void type
+    if (CastTy->isVoidType())
+      return nullptr;
+
+    const llvm::APSInt *Value;
+    if (!(Value = getSymVal(State, CastSym)))
+      return nullptr;
+    return &BV.Convert(SC->getType(), *Value);
+  } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
+    const llvm::APSInt *LHS, *RHS;
+    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
+      LHS = getSymVal(State, SIE->getLHS());
+      RHS = &SIE->getRHS();
+    } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
+      LHS = &ISE->getLHS();
+      RHS = getSymVal(State, ISE->getRHS());
+    } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
+      // Early termination to avoid expensive call
+      LHS = getSymVal(State, SSM->getLHS());
+      RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
+    } else {
+      llvm_unreachable("Unsupported binary expression to get symbol value!");
+    }
+
+    if (!LHS || !RHS)
+      return nullptr;
+
+    llvm::APSInt ConvertedLHS = *LHS, ConvertedRHS = *RHS;
+    QualType LTy = getAPSIntType(*LHS), RTy = getAPSIntType(*RHS);
+    doIntTypeConversion<llvm::APSInt, Z3ConstraintManager::castAPSInt>(
+        ConvertedLHS, LTy, ConvertedRHS, RTy);
+    return BV.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
+  }
+
+  llvm_unreachable("Unsupported expression to get symbol value!");
+}
+
+ProgramStateRef
+Z3ConstraintManager::removeDeadBindings(ProgramStateRef State,
+                                        SymbolReaper &SymReaper) {
+  ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
+  ConstraintZ3Ty::Factory &CZFactory = State->get_context<ConstraintZ3>();
+
+  for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
+    if (SymReaper.maybeDead(I->first))
+      CZ = CZFactory.remove(CZ, *I);
+  }
+
+  return State->set<ConstraintZ3>(CZ);
+}
+
+//===------------------------------------------------------------------===//
+// Internal implementation.
+//===------------------------------------------------------------------===//
+
+ProgramStateRef Z3ConstraintManager::assumeZ3Expr(ProgramStateRef State,
+                                                  SymbolRef Sym,
+                                                  const Z3Expr &Exp) {
+  // Check the model, avoid simplifying AST to save time
+  if (checkZ3Model(State, Exp) == Z3_L_TRUE)
+    return State->add<ConstraintZ3>(std::make_pair(Sym, Exp));
+
+  return nullptr;
+}
+
+Z3_lbool Z3ConstraintManager::checkZ3Model(ProgramStateRef State,
+                                           const Z3Expr &Exp) const {
+  Solver.reset();
+  Solver.addConstraint(Exp);
+  Solver.addStateConstraints(State);
+  return Solver.check();
+}
+
+Z3Expr Z3ConstraintManager::getZ3Expr(SymbolRef Sym, QualType *RetTy,
+                                      bool *hasComparison) const {
+  if (hasComparison) {
+    *hasComparison = false;
+  }
+
+  return getZ3SymExpr(Sym, RetTy, hasComparison);
+}
+
+Z3Expr Z3ConstraintManager::getZ3NotExpr(const Z3Expr &Exp) const {
+  return Z3Expr::fromUnOp(UO_LNot, Exp);
+}
+
+Z3Expr Z3ConstraintManager::getZ3ZeroExpr(const Z3Expr &Exp, QualType Ty,
+                                          bool Assumption) const {
+  ASTContext &Ctx = getBasicVals().getContext();
+  if (Ty->isRealFloatingType()) {
+    llvm::APFloat Zero = llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
+    return Z3Expr::fromFloatBinOp(Exp, Assumption ? BO_EQ : BO_NE,
+                                  Z3Expr::fromAPFloat(Zero));
+  } else if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
+             Ty->isBlockPointerType() || Ty->isReferenceType()) {
+    bool isSigned = Ty->isSignedIntegerOrEnumerationType();
+    // Skip explicit comparison for boolean types
+    if (Ty->isBooleanType())
+      return Assumption ? getZ3NotExpr(Exp) : Exp;
+    return Z3Expr::fromBinOp(Exp, Assumption ? BO_EQ : BO_NE,
+                             Z3Expr::fromInt("0", Ctx.getTypeSize(Ty)),
+                             isSigned);
+  }
+
+  llvm_unreachable("Unsupported type for zero value!");
+}
+
+Z3Expr Z3ConstraintManager::getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
+                                         bool *hasComparison) const {
+  if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
+    if (RetTy)
+      *RetTy = Sym->getType();
+
+    return getZ3DataExpr(SD->getSymbolID(), Sym->getType());
+  } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
+    if (RetTy)
+      *RetTy = Sym->getType();
+
+    QualType FromTy;
+    Z3Expr Exp = getZ3SymExpr(SC->getOperand(), &FromTy, hasComparison);
+    // Casting an expression with a comparison invalidates it. Note that this
+    // must occur after the recursive call above.
+    // e.g. (signed char) (x > 0)
+    if (hasComparison)
+      *hasComparison = false;
+    return getZ3CastExpr(Exp, FromTy, Sym->getType());
+  } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
+    Z3Expr Exp = getZ3SymBinExpr(BSE, hasComparison, RetTy);
+    // Set the hasComparison parameter, in post-order traversal order.
+    if (hasComparison)
+      *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
+    return Exp;
+  }
+
+  llvm_unreachable("Unsupported SymbolRef type!");
+}
+
+Z3Expr Z3ConstraintManager::getZ3DataExpr(const SymbolID ID,
+                                          QualType Ty) const {
+  ASTContext &Ctx = getBasicVals().getContext();
+  return Z3Expr::fromData(ID, Ty->isBooleanType(), Ty->isRealFloatingType(),
+                          Ctx.getTypeSize(Ty));
+}
+
+Z3Expr Z3ConstraintManager::getZ3CastExpr(const Z3Expr &Exp, QualType FromTy,
+                                          QualType ToTy) const {
+  ASTContext &Ctx = getBasicVals().getContext();
+  return Z3Expr::fromCast(Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
+                          Ctx.getTypeSize(FromTy));
+}
+
+Z3Expr Z3ConstraintManager::getZ3SymBinExpr(const BinarySymExpr *BSE,
+                                            bool *hasComparison,
+                                            QualType *RetTy) const {
+  QualType LTy, RTy;
+  BinaryOperator::Opcode Op = BSE->getOpcode();
+
+  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
+    RTy = getAPSIntType(SIE->getRHS());
+    Z3Expr LHS = getZ3SymExpr(SIE->getLHS(), &LTy, hasComparison);
+    Z3Expr RHS = Z3Expr::fromAPSInt(SIE->getRHS());
+    return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
+  } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
+    LTy = getAPSIntType(ISE->getLHS());
+    Z3Expr LHS = Z3Expr::fromAPSInt(ISE->getLHS());
+    Z3Expr RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison);
+    return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
+  } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
+    Z3Expr LHS = getZ3SymExpr(SSM->getLHS(), &LTy, hasComparison);
+    Z3Expr RHS = getZ3SymExpr(SSM->getRHS(), &RTy, hasComparison);
+    return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
+  } else {
+    llvm_unreachable("Unsupported BinarySymExpr type!");
+  }
+}
+
+Z3Expr Z3ConstraintManager::getZ3BinExpr(const Z3Expr &LHS, QualType LTy,
+                                         BinaryOperator::Opcode Op,
+                                         const Z3Expr &RHS, QualType RTy,
+                                         QualType *RetTy) const {
+  Z3Expr NewLHS = LHS;
+  Z3Expr NewRHS = RHS;
+  doTypeConversion(NewLHS, NewRHS, LTy, RTy);
+  // Update the return type parameter if the output type has changed.
+  if (RetTy) {
+    // A boolean result can be represented as an integer type in C/C++, but at
+    // this point we only care about the Z3 type. Set it as a boolean type to
+    // avoid subsequent Z3 errors.
+    if (BinaryOperator::isComparisonOp(Op) || BinaryOperator::isLogicalOp(Op)) {
+      ASTContext &Ctx = getBasicVals().getContext();
+      *RetTy = Ctx.BoolTy;
+    } else {
+      *RetTy = LTy;
+    }
+
+    // If the two operands are pointers and the operation is a subtraction, the
+    // result is of type ptrdiff_t, which is signed
+    if (LTy->isAnyPointerType() && LTy == RTy && Op == BO_Sub) {
+      ASTContext &Ctx = getBasicVals().getContext();
+      *RetTy = Ctx.getIntTypeForBitwidth(Ctx.getTypeSize(LTy), true);
+    }
+  }
+
+  return LTy->isRealFloatingType()
+             ? Z3Expr::fromFloatBinOp(NewLHS, Op, NewRHS)
+             : Z3Expr::fromBinOp(NewLHS, Op, NewRHS,
+                                 LTy->isSignedIntegerOrEnumerationType());
+}
+
+//===------------------------------------------------------------------===//
+// Helper functions.
+//===------------------------------------------------------------------===//
+
+QualType Z3ConstraintManager::getAPSIntType(const llvm::APSInt &Int) const {
+  ASTContext &Ctx = getBasicVals().getContext();
+  return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
+}
+
+void Z3ConstraintManager::doTypeConversion(Z3Expr &LHS, Z3Expr &RHS,
+                                           QualType &LTy, QualType &RTy) const {
+  ASTContext &Ctx = getBasicVals().getContext();
+
+  // Perform type conversion
+  if (LTy->isIntegralOrEnumerationType() &&
+      RTy->isIntegralOrEnumerationType()) {
+    if (LTy->isArithmeticType() && RTy->isArithmeticType())
+      return doIntTypeConversion<Z3Expr, Z3Expr::fromCast>(LHS, LTy, RHS, RTy);
+  } else if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
+    return doFloatTypeConversion<Z3Expr, Z3Expr::fromCast>(LHS, LTy, RHS, RTy);
+  } else if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
+             (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||
+             (LTy->isReferenceType() || RTy->isReferenceType())) {
+    // TODO: Refactor to Sema::FindCompositePointerType(), and
+    // Sema::CheckCompareOperands().
+
+    uint64_t LBitWidth = Ctx.getTypeSize(LTy);
+    uint64_t RBitWidth = Ctx.getTypeSize(RTy);
+
+    // Cast the non-pointer type to the pointer type.
+    // TODO: Be more strict about this.
+    if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||
+        (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||
+        (LTy->isReferenceType() ^ RTy->isReferenceType())) {
+      if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||
+          LTy->isReferenceType()) {
+        LHS = Z3Expr::fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
+        LTy = RTy;
+      } else {
+        RHS = Z3Expr::fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);
+        RTy = LTy;
+      }
+    }
+
+    // Cast the void pointer type to the non-void pointer type.
+    // For void types, this assumes that the casted value is equal to the value
+    // of the original pointer, and does not account for alignment requirements.
+    if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {
+      assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
+             "Pointer types have different bitwidths!");
+      if (RTy->isVoidPointerType())
+        RTy = LTy;
+      else
+        LTy = RTy;
+    }
+
+    if (LTy == RTy)
+      return;
+  }
+
+  // Fallback: for the solver, assume that these types don't really matter
+  if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||
+      (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType())) {
+    LTy = RTy;
+    return;
+  }
+
+  // TODO: Refine behavior for invalid type casts
+}
+
+template <typename T,
+          T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
+void Z3ConstraintManager::doIntTypeConversion(T &LHS, QualType &LTy, T &RHS,
+                                              QualType &RTy) const {
+  ASTContext &Ctx = getBasicVals().getContext();
+
+  uint64_t LBitWidth = Ctx.getTypeSize(LTy);
+  uint64_t RBitWidth = Ctx.getTypeSize(RTy);
+
+  // Always perform integer promotion before checking type equality.
+  // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
+  if (LTy->isPromotableIntegerType()) {
+    QualType NewTy = Ctx.getPromotedIntegerType(LTy);
+    uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
+    LHS = (*doCast)(LHS, NewTy, NewBitWidth, LTy, LBitWidth);
+    LTy = NewTy;
+    LBitWidth = NewBitWidth;
+  }
+  if (RTy->isPromotableIntegerType()) {
+    QualType NewTy = Ctx.getPromotedIntegerType(RTy);
+    uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
+    RHS = (*doCast)(RHS, NewTy, NewBitWidth, RTy, RBitWidth);
+    RTy = NewTy;
+    RBitWidth = NewBitWidth;
+  }
+
+  if (LTy == RTy)
+    return;
+
+  // Perform integer type conversion
+  // Note: Safe to skip updating bitwidth because this must terminate
+  bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType();
+  bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType();
+
+  int order = Ctx.getIntegerTypeOrder(LTy, RTy);
+  if (isLSignedTy == isRSignedTy) {
+    // Same signedness; use the higher-ranked type
+    if (order == 1) {
+      RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
+      RTy = LTy;
+    } else {
+      LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
+      LTy = RTy;
+    }
+  } else if (order != (isLSignedTy ? 1 : -1)) {
+    // The unsigned type has greater than or equal rank to the
+    // signed type, so use the unsigned type
+    if (isRSignedTy) {
+      RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
+      RTy = LTy;
+    } else {
+      LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
+      LTy = RTy;
+    }
+  } else if (LBitWidth != RBitWidth) {
+    // The two types are different widths; if we are here, that
+    // means the signed type is larger than the unsigned type, so
+    // use the signed type.
+    if (isLSignedTy) {
+      RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
+      RTy = LTy;
+    } else {
+      LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
+      LTy = RTy;
+    }
+  } else {
+    // The signed type is higher-ranked than the unsigned type,
+    // but isn't actually any bigger (like unsigned int and long
+    // on most 32-bit systems).  Use the unsigned type corresponding
+    // to the signed type.
+    QualType NewTy = Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);
+    RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
+    RTy = NewTy;
+    LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
+    LTy = NewTy;
+  }
+}
+
+template <typename T,
+          T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
+void Z3ConstraintManager::doFloatTypeConversion(T &LHS, QualType &LTy, T &RHS,
+                                                QualType &RTy) const {
+  ASTContext &Ctx = getBasicVals().getContext();
+
+  uint64_t LBitWidth = Ctx.getTypeSize(LTy);
+  uint64_t RBitWidth = Ctx.getTypeSize(RTy);
+
+  // Perform float-point type promotion
+  if (!LTy->isRealFloatingType()) {
+    LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
+    LTy = RTy;
+    LBitWidth = RBitWidth;
+  }
+  if (!RTy->isRealFloatingType()) {
+    RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
+    RTy = LTy;
+    RBitWidth = LBitWidth;
+  }
+
+  if (LTy == RTy)
+    return;
+
+  // If we have two real floating types, convert the smaller operand to the
+  // bigger result
+  // Note: Safe to skip updating bitwidth because this must terminate
+  int order = Ctx.getFloatingTypeOrder(LTy, RTy);
+  if (order > 0) {
+    RHS = Z3Expr::fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);
+    RTy = LTy;
+  } else if (order == 0) {
+    LHS = Z3Expr::fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
+    LTy = RTy;
+  } else {
+    llvm_unreachable("Unsupported floating-point type cast!");
+  }
+}
+
+llvm::APSInt Z3ConstraintManager::castAPSInt(const llvm::APSInt &V,
+                                             QualType ToTy, uint64_t ToWidth,
+                                             QualType FromTy,
+                                             uint64_t FromWidth) {
+  APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType());
+  return TargetType.convert(V);
+}
+
+//==------------------------------------------------------------------------==/
+// Pretty-printing.
+//==------------------------------------------------------------------------==/
+
+void Z3ConstraintManager::print(ProgramStateRef St, raw_ostream &OS,
+                                const char *nl, const char *sep) {
+
+  ConstraintZ3Ty CZ = St->get<ConstraintZ3>();
+
+  OS << nl << sep << "Constraints:";
+  for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
+    OS << nl << ' ' << I->first << " : ";
+    I->second.print(OS);
+  }
+  OS << nl;
+}
+
+#endif
+
+std::unique_ptr<ConstraintManager>
+ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
+#if CLANG_ANALYZER_WITH_Z3
+  return llvm::make_unique<Z3ConstraintManager>(Eng, StMgr.getSValBuilder());
+#else
+  llvm::report_fatal_error("Clang was not compiled with Z3 support!", false);
+  return nullptr;
+#endif
+}