From 040bc2559aa5988618fe601103b4454c835b0f43 Mon Sep 17 00:00:00 2001 From: "Mikhail R. Gadelha" Date: Thu, 25 Oct 2018 17:27:42 +0000 Subject: [PATCH] [analyzer] Move canReasonAbout from Z3ConstraintManager to SMTConstraintManager 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? Reviewers: george.karpenkov, NoQ Reviewed By: george.karpenkov Subscribers: mehdi_amini, xazax.hun, szepet, a.sidorin, dexonsmith, Szelethus, donat.nagy, dkrupp Differential Revision: https://reviews.llvm.org/D53694 git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@345284 91177308-0d34-0410-b5e6-96231b3b80d8 --- .../Core/PathSensitive/SMTConstraintManager.h | 46 +++++++++++++++++++ .../Core/PathSensitive/SMTSolver.h | 3 ++ .../Core/Z3ConstraintManager.cpp | 45 +----------------- 3 files changed, 51 insertions(+), 43 deletions(-) diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h index db05bdaa4d..54cf3c39dd 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -218,6 +218,52 @@ public: OS << nl; } + bool canReasonAbout(SVal X) const override { + const TargetInfo &TI = getBasicVals().getContext().getTargetInfo(); + + Optional SymVal = X.getAs(); + 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(Sym)) + return true; + + SValBuilder &SVB = getSValBuilder(); + + if (const SymbolCast *SC = dyn_cast(Sym)) + return canReasonAbout(SVB.makeSymbolVal(SC->getOperand())); + + if (const BinarySymExpr *BSE = dyn_cast(Sym)) { + if (const SymIntExpr *SIE = dyn_cast(BSE)) + return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS())); + + if (const IntSymExpr *ISE = dyn_cast(BSE)) + return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS())); + + if (const SymSymExpr *SSE = dyn_cast(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(); } diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h index 0db1e364b6..2abe5fc987 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h @@ -285,6 +285,9 @@ public: /// 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; }; diff --git a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp index e6a5f11fa1..028010726a 100644 --- a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -860,6 +860,8 @@ public: 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); } @@ -874,49 +876,6 @@ class Z3ConstraintManager : public SMTConstraintManager { public: Z3ConstraintManager(SubEngine *SE, SValBuilder &SB) : SMTConstraintManager(SE, SB, Solver) {} - - bool canReasonAbout(SVal X) const override { - const TargetInfo &TI = getBasicVals().getContext().getTargetInfo(); - - Optional SymVal = X.getAs(); - 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(Sym)) - return true; - - SValBuilder &SVB = getSValBuilder(); - - if (const SymbolCast *SC = dyn_cast(Sym)) - return canReasonAbout(SVB.makeSymbolVal(SC->getOperand())); - - if (const BinarySymExpr *BSE = dyn_cast(Sym)) { - if (const SymIntExpr *SIE = dyn_cast(BSE)) - return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS())); - - if (const IntSymExpr *ISE = dyn_cast(BSE)) - return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS())); - - if (const SymSymExpr *SSE = dyn_cast(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 -- 2.40.0