[analyzer] Fix Z3 backend after D48205

[mikhail.ramalho]

Summary

An assertion was added in D48205 to catch places where a nonloc::SymbolVal was wrapping a loc object.

This patch fixes that in the Z3 backend by making the SValBuilder object accessible from inherited instances of SimpleConstraintManager and calling SVB.makeSymbolVal(foo) instead of nonloc::SymbolVal(foo).

[NoQ]

Yup, that's the intended approach :)

cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h

protected:
   virtual ProgramStateRef assumeSymUnsupported(ProgramStateRef State,
                                                SymbolRef Sym,
                                                bool Assumption) = 0;
 
   //===------------------------------------------------------------------===//
   // Internal implementation.
   //===------------------------------------------------------------------===//
 
+  SValBuilder &getSValBuilder() const { return SVB; }
   BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); }
   SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); }
 
 private:
   ProgramStateRef assume(ProgramStateRef State, NonLoc Cond, bool Assumption);
 
   ProgramStateRef assumeAux(ProgramStateRef State, NonLoc Cond,
                             bool Assumption);
 };
 
 } // end namespace ento
 
 } // end namespace clang
 
 #endif

cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

 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);
+  if (isa<SymbolData>(Sym))
+    return true;
+
+  SValBuilder &SVB = getSValBuilder();
+
+  if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
+    return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
+
+  if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
+    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
+      return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
+
+    if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
+      return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));
+
+    if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
+      return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
+             canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
 
-  return true;
+  llvm_unreachable("Unsupported expression to reason about!");
 }
 
 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);