diff options
author | Mikhail R. Gadelha <mikhail.ramalho@gmail.com> | 2018-10-25 17:27:42 +0000 |
---|---|---|
committer | Mikhail R. Gadelha <mikhail.ramalho@gmail.com> | 2018-10-25 17:27:42 +0000 |
commit | 040bc2559aa5988618fe601103b4454c835b0f43 (patch) | |
tree | c1b079eec397750155767b920482351ae407909b | |
parent | b264f83ea398d5c0131d7e31c6d814ae7ecd5b72 (diff) |
[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
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<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(); } 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<ConstraintZ3, Z3Expr> { 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 |