[analyzer] Move canReasonAbout from Z3ConstraintManager to SMTConstraintManager

[mikhail.ramalho]

Summary

This patch moves the last method in Z3ConstraintManager to SMTConstraintManager: canReasonAbout().

The canReasonAbout() method checks if a given SVal can be encoded in SMT. I've added a new method to the SMT API to return true if a solver can encode floating-point arithmetics and it was enough to make canReasonAbout() solver independent.

As an annoying side-effect, Z3ConstraintManager is pretty empty now and only (1) creates the Z3 solver object by calling CreateZ3Solver() and (2) instantiates SMTConstraintManager. Maybe we can get rid of this class altogether in the future: a CreateSMTConstraintManager() method that does (1) and (2) and returns the constraint manager object?

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

void print(ProgramStateRef St, raw_ostream &OS, const char *nl,
     OS << nl << sep << "Constraints:";
     for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
       OS << nl << ' ' << I->first << " : ";
       I->second.print(OS);
     }
     OS << nl;
   }
 
+  bool canReasonAbout(SVal X) const override {
+    const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
+
+    Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
+    if (!SymVal)
+      return true;
+
+    const SymExpr *Sym = SymVal->getSymbol();
+    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 (Ty->isRealFloatingType())
+      return Solver->isFPSupported();
+
+    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()));
+    }
+
+    llvm_unreachable("Unsupported expression to reason about!");
+  }
+
   /// Dumps SMT formula
   LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
 
 protected:
   // Check whether a new model is satisfiable, and update the program state.
   virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
                                      const SMTExprRef &Exp) {
     // Check the model, avoid simplifying AST to save time

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

public:
   virtual void push() = 0;
 
   /// Pop the previous solver state
   virtual void pop(unsigned NumStates = 1) = 0;
 
   /// Reset the solver and remove all constraints.
   virtual void reset() = 0;
 
+  /// Checks if the solver supports floating-points.
+  virtual bool isFPSupported() = 0;
+
   virtual void print(raw_ostream &OS) const = 0;
 };
 
 /// Shared pointer for SMTSolvers.
 using SMTSolverRef = std::shared_ptr<SMTSolver>;
 
 /// Convenience method to create and Z3Solver object
 SMTSolverRef CreateZ3Solver();
 
 } // namespace ento
 } // namespace clang
 
 #endif

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

public:
   }
 
   /// Get a model from the solver. Caller should check the model is
   /// satisfiable.
   Z3Model getModel() {
     return Z3Model(Context, Z3_solver_get_model(Context.Context, Solver));
   }
 
+  bool isFPSupported() override { return true; }
+
   /// Reset the solver and remove all constraints.
   void reset() override { Z3_solver_reset(Context.Context, Solver); }
 
   void print(raw_ostream &OS) const override {
     OS << Z3_solver_to_string(Context.Context, Solver);
   }
 }; // end class Z3Solver
 
 class Z3ConstraintManager : public SMTConstraintManager<ConstraintZ3, Z3Expr> {
   SMTSolverRef Solver = CreateZ3Solver();
 
 public:
   Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
       : SMTConstraintManager(SE, SB, Solver) {}
-
-  bool canReasonAbout(SVal X) const override {
-    const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
-
-    Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
-    if (!SymVal)
-      return true;
-
-    const SymExpr *Sym = SymVal->getSymbol();
-    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))
-      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()));
-    }
-
-    llvm_unreachable("Unsupported expression to reason about!");
-  }
 }; // end class Z3ConstraintManager
 
 } // end anonymous namespace
 
 #endif
 
 SMTSolverRef clang::ento::CreateZ3Solver() {
 #if CLANG_ANALYZER_WITH_Z3