r345284 - [analyzer] Move canReasonAbout from Z3ConstraintManager to SMTConstraintManager
Mikhail R. Gadelha via cfe-commits
cfe-commits at lists.llvm.org
Thu Oct 25 10:27:42 PDT 2018
Author: mramalho
Date: Thu Oct 25 10:27:42 2018
New Revision: 345284
URL: http://llvm.org/viewvc/llvm-project?rev=345284&view=rev
Log:
[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
Modified:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=345284&r1=345283&r2=345284&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Thu Oct 25 10:27:42 2018
@@ -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(); }
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h?rev=345284&r1=345283&r2=345284&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h Thu Oct 25 10:27:42 2018
@@ -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;
};
Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=345284&r1=345283&r2=345284&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Thu Oct 25 10:27:42 2018
@@ -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 SMTCo
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
More information about the cfe-commits
mailing list