r337919 - [analyzer] Moved non solver specific code from Z3ConstraintManager to SMTConstraintManager
Mikhail R. Gadelha via cfe-commits
cfe-commits at lists.llvm.org
Wed Jul 25 05:49:29 PDT 2018
Author: mramalho
Date: Wed Jul 25 05:49:29 2018
New Revision: 337919
URL: http://llvm.org/viewvc/llvm-project?rev=337919&view=rev
Log:
[analyzer] Moved non solver specific code from Z3ConstraintManager to SMTConstraintManager
Summary:
This patch moves a lot of code from `Z3ConstraintManager` to `SMTConstraintManager`, leaving only the necessary:
* `canReasonAbout` which returns if a Solver can handle a given `SVal` (should be moved to `SMTSolver` in the future).
* `removeDeadBindings`, `assumeExpr` and `print`: methods that need to use `ConstraintZ3Ty`, can probably be moved to `SMTConstraintManager` in the future.
The patch creates a new file, `SMTConstraintManager.cpp` with the moved code. Conceptually, this is move in the right direction and needs further improvements: `SMTConstraintManager` still does a lot of things that are not required by a `ConstraintManager`.
We ought to move the unrelated to `SMTSolver` and remove everything that's not related to a `ConstraintManager`. In particular, we could remove `addRangeConstraints` and `isModelFeasible`, and make the refutation manager create an Z3Solver directly.
Reviewers: NoQ, george.karpenkov
Reviewed By: george.karpenkov
Subscribers: mgorny, xazax.hun, szepet, a.sidorin
Differential Revision: https://reviews.llvm.org/D49668
Added:
cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
Modified:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt
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=337919&r1=337918&r2=337919&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Wed Jul 25 05:49:29 2018
@@ -16,27 +16,254 @@
#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h"
namespace clang {
namespace ento {
class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
+ SMTSolverRef &Solver;
public:
- SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB)
- : SimpleConstraintManager(SE, SB) {}
+ SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB,
+ SMTSolverRef &S)
+ : SimpleConstraintManager(SE, SB), Solver(S) {}
virtual ~SMTConstraintManager() = default;
+ //===------------------------------------------------------------------===//
+ // Implementation for interface from SimpleConstraintManager.
+ //===------------------------------------------------------------------===//
+
+ ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym,
+ bool Assumption) override;
+
+ ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
+ const llvm::APSInt &From,
+ const llvm::APSInt &To,
+ bool InRange) override;
+
+ ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
+ bool Assumption) override;
+
+ //===------------------------------------------------------------------===//
+ // Implementation for interface from ConstraintManager.
+ //===------------------------------------------------------------------===//
+
+ ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
+
+ const llvm::APSInt *getSymVal(ProgramStateRef State,
+ SymbolRef Sym) const override;
+
/// Converts the ranged constraints of a set of symbols to SMT
///
/// \param CR The set of constraints.
- virtual void addRangeConstraints(clang::ento::ConstraintRangeTy CR) = 0;
+ void addRangeConstraints(clang::ento::ConstraintRangeTy CR);
/// Checks if the added constraints are satisfiable
- virtual clang::ento::ConditionTruthVal isModelFeasible() = 0;
+ clang::ento::ConditionTruthVal isModelFeasible();
/// Dumps SMT formula
- LLVM_DUMP_METHOD virtual void dump() const = 0;
+ LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
+
+protected:
+ //===------------------------------------------------------------------===//
+ // Internal implementation.
+ //===------------------------------------------------------------------===//
+
+ // Check whether a new model is satisfiable, and update the program state.
+ virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
+ const SMTExprRef &Exp) = 0;
+
+ /// Given a program state, construct the logical conjunction and add it to
+ /// the solver
+ virtual void addStateConstraints(ProgramStateRef State) const = 0;
+
+ // Generate and check a Z3 model, using the given constraint.
+ ConditionTruthVal checkModel(ProgramStateRef State,
+ const SMTExprRef &Exp) const;
+
+ // Generate a Z3Expr that represents the given symbolic expression.
+ // Sets the hasComparison parameter if the expression has a comparison
+ // operator.
+ // Sets the RetTy parameter to the final return type after promotions and
+ // casts.
+ SMTExprRef getExpr(SymbolRef Sym, QualType *RetTy = nullptr,
+ bool *hasComparison = nullptr) const;
+
+ // Generate a Z3Expr that takes the logical not of an expression.
+ SMTExprRef getNotExpr(const SMTExprRef &Exp) const;
+
+ // Generate a Z3Expr that compares the expression to zero.
+ SMTExprRef getZeroExpr(const SMTExprRef &Exp, QualType RetTy,
+ bool Assumption) const;
+
+ // Recursive implementation to unpack and generate symbolic expression.
+ // Sets the hasComparison and RetTy parameters. See getZ3Expr().
+ SMTExprRef getSymExpr(SymbolRef Sym, QualType *RetTy,
+ bool *hasComparison) const;
+
+ // Wrapper to generate Z3Expr from SymbolData.
+ SMTExprRef getDataExpr(const SymbolID ID, QualType Ty) const;
+
+ // Wrapper to generate Z3Expr from SymbolCast.
+ SMTExprRef getCastExpr(const SMTExprRef &Exp, QualType FromTy,
+ QualType Ty) const;
+
+ // Wrapper to generate Z3Expr from BinarySymExpr.
+ // Sets the hasComparison and RetTy parameters. See getZ3Expr().
+ SMTExprRef getSymBinExpr(const BinarySymExpr *BSE, bool *hasComparison,
+ QualType *RetTy) const;
+
+ // Wrapper to generate Z3Expr from unpacked binary symbolic expression.
+ // Sets the RetTy parameter. See getZ3Expr().
+ SMTExprRef getBinExpr(const SMTExprRef &LHS, QualType LTy,
+ BinaryOperator::Opcode Op, const SMTExprRef &RHS,
+ QualType RTy, QualType *RetTy) const;
+
+ // Wrapper to generate Z3Expr from a range. If From == To, an equality will
+ // be created instead.
+ SMTExprRef getRangeExpr(SymbolRef Sym, const llvm::APSInt &From,
+ const llvm::APSInt &To, bool InRange);
+
+ //===------------------------------------------------------------------===//
+ // Helper functions.
+ //===------------------------------------------------------------------===//
+
+ // Recover the QualType of an APSInt.
+ // TODO: Refactor to put elsewhere
+ QualType getAPSIntType(const llvm::APSInt &Int) const;
+
+ // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
+ std::pair<llvm::APSInt, QualType> fixAPSInt(const llvm::APSInt &Int) const;
+
+ // Perform implicit type conversion on binary symbolic expressions.
+ // May modify all input parameters.
+ // TODO: Refactor to use built-in conversion functions
+ void doTypeConversion(SMTExprRef &LHS, SMTExprRef &RHS, QualType <y,
+ QualType &RTy) const;
+
+ // Perform implicit integer type conversion.
+ // May modify all input parameters.
+ // TODO: Refactor to use Sema::handleIntegerConversion()
+ template <typename T, T (SMTSolver::*doCast)(const T &, QualType, uint64_t,
+ QualType, uint64_t)>
+ void doIntTypeConversion(T &LHS, QualType <y, T &RHS, QualType &RTy) const {
+ ASTContext &Ctx = getBasicVals().getContext();
+ uint64_t LBitWidth = Ctx.getTypeSize(LTy);
+ uint64_t RBitWidth = Ctx.getTypeSize(RTy);
+
+ assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
+ // Always perform integer promotion before checking type equality.
+ // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
+ if (LTy->isPromotableIntegerType()) {
+ QualType NewTy = Ctx.getPromotedIntegerType(LTy);
+ uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
+ LHS = ((*Solver).*doCast)(LHS, NewTy, NewBitWidth, LTy, LBitWidth);
+ LTy = NewTy;
+ LBitWidth = NewBitWidth;
+ }
+ if (RTy->isPromotableIntegerType()) {
+ QualType NewTy = Ctx.getPromotedIntegerType(RTy);
+ uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
+ RHS = ((*Solver).*doCast)(RHS, NewTy, NewBitWidth, RTy, RBitWidth);
+ RTy = NewTy;
+ RBitWidth = NewBitWidth;
+ }
+
+ if (LTy == RTy)
+ return;
+
+ // Perform integer type conversion
+ // Note: Safe to skip updating bitwidth because this must terminate
+ bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType();
+ bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType();
+
+ int order = Ctx.getIntegerTypeOrder(LTy, RTy);
+ if (isLSignedTy == isRSignedTy) {
+ // Same signedness; use the higher-ranked type
+ if (order == 1) {
+ RHS = ((*Solver).*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
+ RTy = LTy;
+ } else {
+ LHS = ((*Solver).*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
+ LTy = RTy;
+ }
+ } else if (order != (isLSignedTy ? 1 : -1)) {
+ // The unsigned type has greater than or equal rank to the
+ // signed type, so use the unsigned type
+ if (isRSignedTy) {
+ RHS = ((*Solver).*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
+ RTy = LTy;
+ } else {
+ LHS = ((*Solver).*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
+ LTy = RTy;
+ }
+ } else if (LBitWidth != RBitWidth) {
+ // The two types are different widths; if we are here, that
+ // means the signed type is larger than the unsigned type, so
+ // use the signed type.
+ if (isLSignedTy) {
+ RHS = ((*Solver).*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
+ RTy = LTy;
+ } else {
+ LHS = ((*Solver).*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
+ LTy = RTy;
+ }
+ } else {
+ // The signed type is higher-ranked than the unsigned type,
+ // but isn't actually any bigger (like unsigned int and long
+ // on most 32-bit systems). Use the unsigned type corresponding
+ // to the signed type.
+ QualType NewTy =
+ Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);
+ RHS = ((*Solver).*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
+ RTy = NewTy;
+ LHS = ((*Solver).*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
+ LTy = NewTy;
+ }
+ }
+
+ // Perform implicit floating-point type conversion.
+ // May modify all input parameters.
+ // TODO: Refactor to use Sema::handleFloatConversion()
+ template <typename T, T (SMTSolver::*doCast)(const T &, QualType, uint64_t,
+ QualType, uint64_t)>
+ void doFloatTypeConversion(T &LHS, QualType <y, T &RHS,
+ QualType &RTy) const {
+ ASTContext &Ctx = getBasicVals().getContext();
+
+ uint64_t LBitWidth = Ctx.getTypeSize(LTy);
+ uint64_t RBitWidth = Ctx.getTypeSize(RTy);
+
+ // Perform float-point type promotion
+ if (!LTy->isRealFloatingType()) {
+ LHS = ((*Solver).*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
+ LTy = RTy;
+ LBitWidth = RBitWidth;
+ }
+ if (!RTy->isRealFloatingType()) {
+ RHS = ((*Solver).*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
+ RTy = LTy;
+ RBitWidth = LBitWidth;
+ }
+
+ if (LTy == RTy)
+ return;
+
+ // If we have two real floating types, convert the smaller operand to the
+ // bigger result
+ // Note: Safe to skip updating bitwidth because this must terminate
+ int order = Ctx.getFloatingTypeOrder(LTy, RTy);
+ if (order > 0) {
+ RHS = ((*Solver).*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
+ RTy = LTy;
+ } else if (order == 0) {
+ LHS = ((*Solver).*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
+ LTy = RTy;
+ } else {
+ llvm_unreachable("Unsupported floating-point type cast!");
+ }
+ }
}; // end class SMTConstraintManager
} // namespace ento
Modified: cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt?rev=337919&r1=337918&r2=337919&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt Wed Jul 25 05:49:29 2018
@@ -48,6 +48,7 @@ add_clang_library(clangStaticAnalyzerCor
SVals.cpp
SimpleConstraintManager.cpp
SimpleSValBuilder.cpp
+ SMTConstraintManager.cpp
Store.cpp
SubEngine.cpp
SymbolManager.cpp
Added: cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp?rev=337919&view=auto
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp (added)
+++ cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp Wed Jul 25 05:49:29 2018
@@ -0,0 +1,479 @@
+//== SMTConstraintManager.cpp -----------------------------------*- C++ -*--==//
+//
+// The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
+#include "clang/Basic/TargetInfo.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+
+using namespace clang;
+using namespace ento;
+
+void SMTConstraintManager::addRangeConstraints(ConstraintRangeTy CR) {
+ Solver->reset();
+
+ for (const auto &I : CR) {
+ SymbolRef Sym = I.first;
+
+ SMTExprRef Constraints = Solver->fromBoolean(false);
+ for (const auto &Range : I.second) {
+ SMTExprRef SymRange =
+ getRangeExpr(Sym, Range.From(), Range.To(), /*InRange=*/true);
+
+ // FIXME: the last argument (isSigned) is not used when generating the
+ // or expression, as both arguments are booleans
+ Constraints =
+ Solver->fromBinOp(Constraints, BO_LOr, SymRange, /*IsSigned=*/true);
+ }
+ Solver->addConstraint(Constraints);
+ }
+}
+
+clang::ento::ConditionTruthVal SMTConstraintManager::isModelFeasible() {
+ return Solver->check();
+}
+
+ProgramStateRef SMTConstraintManager::assumeSym(ProgramStateRef State,
+ SymbolRef Sym,
+ bool Assumption) {
+ QualType RetTy;
+ bool hasComparison;
+
+ SMTExprRef Exp = getExpr(Sym, &RetTy, &hasComparison);
+ // Create zero comparison for implicit boolean cast, with reversed assumption
+ if (!hasComparison && !RetTy->isBooleanType())
+ return assumeExpr(State, Sym, getZeroExpr(Exp, RetTy, !Assumption));
+
+ return assumeExpr(State, Sym, Assumption ? Exp : getNotExpr(Exp));
+}
+
+ProgramStateRef SMTConstraintManager::assumeSymInclusiveRange(
+ ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
+ const llvm::APSInt &To, bool InRange) {
+ return assumeExpr(State, Sym, getRangeExpr(Sym, From, To, InRange));
+}
+
+ProgramStateRef
+SMTConstraintManager::assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
+ bool Assumption) {
+ // Skip anything that is unsupported
+ return State;
+}
+
+ConditionTruthVal SMTConstraintManager::checkNull(ProgramStateRef State,
+ SymbolRef Sym) {
+ QualType RetTy;
+ // The expression may be casted, so we cannot call getZ3DataExpr() directly
+ SMTExprRef VarExp = getExpr(Sym, &RetTy);
+ SMTExprRef Exp = getZeroExpr(VarExp, RetTy, true);
+
+ // Negate the constraint
+ SMTExprRef NotExp = getZeroExpr(VarExp, RetTy, false);
+
+ Solver->reset();
+ addStateConstraints(State);
+
+ Solver->push();
+ Solver->addConstraint(Exp);
+ ConditionTruthVal isSat = Solver->check();
+
+ Solver->pop();
+ Solver->addConstraint(NotExp);
+ ConditionTruthVal isNotSat = Solver->check();
+
+ // Zero is the only possible solution
+ if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
+ return true;
+
+ // Zero is not a solution
+ if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
+ return false;
+
+ // Zero may be a solution
+ return ConditionTruthVal();
+}
+
+const llvm::APSInt *SMTConstraintManager::getSymVal(ProgramStateRef State,
+ SymbolRef Sym) const {
+ BasicValueFactory &BVF = getBasicVals();
+ ASTContext &Ctx = BVF.getContext();
+
+ if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
+ QualType Ty = Sym->getType();
+ assert(!Ty->isRealFloatingType());
+ llvm::APSInt Value(Ctx.getTypeSize(Ty),
+ !Ty->isSignedIntegerOrEnumerationType());
+
+ SMTExprRef Exp = getDataExpr(SD->getSymbolID(), Ty);
+
+ Solver->reset();
+ addStateConstraints(State);
+
+ // Constraints are unsatisfiable
+ ConditionTruthVal isSat = Solver->check();
+ if (!isSat.isConstrainedTrue())
+ return nullptr;
+
+ // Model does not assign interpretation
+ if (!Solver->getInterpretation(Exp, Value))
+ return nullptr;
+
+ // A value has been obtained, check if it is the only value
+ SMTExprRef NotExp = Solver->fromBinOp(
+ Exp, BO_NE,
+ Ty->isBooleanType() ? Solver->fromBoolean(Value.getBoolValue())
+ : Solver->fromAPSInt(Value),
+ false);
+
+ Solver->addConstraint(NotExp);
+
+ ConditionTruthVal isNotSat = Solver->check();
+ if (isNotSat.isConstrainedTrue())
+ return nullptr;
+
+ // This is the only solution, store it
+ return &BVF.getValue(Value);
+ }
+
+ if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
+ SymbolRef CastSym = SC->getOperand();
+ QualType CastTy = SC->getType();
+ // Skip the void type
+ if (CastTy->isVoidType())
+ return nullptr;
+
+ const llvm::APSInt *Value;
+ if (!(Value = getSymVal(State, CastSym)))
+ return nullptr;
+ return &BVF.Convert(SC->getType(), *Value);
+ }
+
+ if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
+ const llvm::APSInt *LHS, *RHS;
+ if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
+ LHS = getSymVal(State, SIE->getLHS());
+ RHS = &SIE->getRHS();
+ } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
+ LHS = &ISE->getLHS();
+ RHS = getSymVal(State, ISE->getRHS());
+ } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
+ // Early termination to avoid expensive call
+ LHS = getSymVal(State, SSM->getLHS());
+ RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
+ } else {
+ llvm_unreachable("Unsupported binary expression to get symbol value!");
+ }
+
+ if (!LHS || !RHS)
+ return nullptr;
+
+ llvm::APSInt ConvertedLHS, ConvertedRHS;
+ QualType LTy, RTy;
+ std::tie(ConvertedLHS, LTy) = fixAPSInt(*LHS);
+ std::tie(ConvertedRHS, RTy) = fixAPSInt(*RHS);
+ doIntTypeConversion<llvm::APSInt, &SMTSolver::castAPSInt>(
+ ConvertedLHS, LTy, ConvertedRHS, RTy);
+ return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
+ }
+
+ llvm_unreachable("Unsupported expression to get symbol value!");
+}
+
+//===------------------------------------------------------------------===//
+// Internal implementation.
+//===------------------------------------------------------------------===//
+
+ConditionTruthVal
+SMTConstraintManager::checkModel(ProgramStateRef State,
+ const SMTExprRef &Exp) const {
+ Solver->reset();
+ Solver->addConstraint(Exp);
+ addStateConstraints(State);
+ return Solver->check();
+}
+
+SMTExprRef SMTConstraintManager::getExpr(SymbolRef Sym, QualType *RetTy,
+ bool *hasComparison) const {
+ if (hasComparison) {
+ *hasComparison = false;
+ }
+
+ return getSymExpr(Sym, RetTy, hasComparison);
+}
+
+SMTExprRef SMTConstraintManager::getNotExpr(const SMTExprRef &Exp) const {
+ return Solver->fromUnOp(UO_LNot, Exp);
+}
+
+SMTExprRef SMTConstraintManager::getZeroExpr(const SMTExprRef &Exp, QualType Ty,
+ bool Assumption) const {
+ ASTContext &Ctx = getBasicVals().getContext();
+ if (Ty->isRealFloatingType()) {
+ llvm::APFloat Zero = llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
+ return Solver->fromFloatBinOp(Exp, Assumption ? BO_EQ : BO_NE,
+ Solver->fromAPFloat(Zero));
+ }
+
+ if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
+ Ty->isBlockPointerType() || Ty->isReferenceType()) {
+
+ // Skip explicit comparison for boolean types
+ bool isSigned = Ty->isSignedIntegerOrEnumerationType();
+ if (Ty->isBooleanType())
+ return Assumption ? getNotExpr(Exp) : Exp;
+
+ return Solver->fromBinOp(Exp, Assumption ? BO_EQ : BO_NE,
+ Solver->fromInt("0", Ctx.getTypeSize(Ty)),
+ isSigned);
+ }
+
+ llvm_unreachable("Unsupported type for zero value!");
+}
+
+SMTExprRef SMTConstraintManager::getSymExpr(SymbolRef Sym, QualType *RetTy,
+ bool *hasComparison) const {
+ if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
+ if (RetTy)
+ *RetTy = Sym->getType();
+
+ return getDataExpr(SD->getSymbolID(), Sym->getType());
+ }
+
+ if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
+ if (RetTy)
+ *RetTy = Sym->getType();
+
+ QualType FromTy;
+ SMTExprRef Exp = getSymExpr(SC->getOperand(), &FromTy, hasComparison);
+ // Casting an expression with a comparison invalidates it. Note that this
+ // must occur after the recursive call above.
+ // e.g. (signed char) (x > 0)
+ if (hasComparison)
+ *hasComparison = false;
+ return getCastExpr(Exp, FromTy, Sym->getType());
+ }
+
+ if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
+ SMTExprRef Exp = getSymBinExpr(BSE, hasComparison, RetTy);
+ // Set the hasComparison parameter, in post-order traversal order.
+ if (hasComparison)
+ *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
+ return Exp;
+ }
+
+ llvm_unreachable("Unsupported SymbolRef type!");
+}
+
+SMTExprRef SMTConstraintManager::getDataExpr(const SymbolID ID,
+ QualType Ty) const {
+ ASTContext &Ctx = getBasicVals().getContext();
+ return Solver->fromData(ID, Ty, Ctx.getTypeSize(Ty));
+}
+
+SMTExprRef SMTConstraintManager::getCastExpr(const SMTExprRef &Exp,
+ QualType FromTy,
+ QualType ToTy) const {
+ ASTContext &Ctx = getBasicVals().getContext();
+ return Solver->fromCast(Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
+ Ctx.getTypeSize(FromTy));
+}
+
+SMTExprRef SMTConstraintManager::getSymBinExpr(const BinarySymExpr *BSE,
+ bool *hasComparison,
+ QualType *RetTy) const {
+ QualType LTy, RTy;
+ BinaryOperator::Opcode Op = BSE->getOpcode();
+
+ if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
+ SMTExprRef LHS = getSymExpr(SIE->getLHS(), <y, hasComparison);
+ llvm::APSInt NewRInt;
+ std::tie(NewRInt, RTy) = fixAPSInt(SIE->getRHS());
+ SMTExprRef RHS = Solver->fromAPSInt(NewRInt);
+ return getBinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
+ }
+
+ if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
+ llvm::APSInt NewLInt;
+ std::tie(NewLInt, LTy) = fixAPSInt(ISE->getLHS());
+ SMTExprRef LHS = Solver->fromAPSInt(NewLInt);
+ SMTExprRef RHS = getSymExpr(ISE->getRHS(), &RTy, hasComparison);
+ return getBinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
+ }
+
+ if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
+ SMTExprRef LHS = getSymExpr(SSM->getLHS(), <y, hasComparison);
+ SMTExprRef RHS = getSymExpr(SSM->getRHS(), &RTy, hasComparison);
+ return getBinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
+ }
+
+ llvm_unreachable("Unsupported BinarySymExpr type!");
+}
+
+SMTExprRef SMTConstraintManager::getBinExpr(const SMTExprRef &LHS, QualType LTy,
+ BinaryOperator::Opcode Op,
+ const SMTExprRef &RHS, QualType RTy,
+ QualType *RetTy) const {
+ SMTExprRef NewLHS = LHS;
+ SMTExprRef NewRHS = RHS;
+ doTypeConversion(NewLHS, NewRHS, LTy, RTy);
+
+ // Update the return type parameter if the output type has changed.
+ if (RetTy) {
+ // A boolean result can be represented as an integer type in C/C++, but at
+ // this point we only care about the Z3 type. Set it as a boolean type to
+ // avoid subsequent Z3 errors.
+ if (BinaryOperator::isComparisonOp(Op) || BinaryOperator::isLogicalOp(Op)) {
+ ASTContext &Ctx = getBasicVals().getContext();
+ *RetTy = Ctx.BoolTy;
+ } else {
+ *RetTy = LTy;
+ }
+
+ // If the two operands are pointers and the operation is a subtraction, the
+ // result is of type ptrdiff_t, which is signed
+ if (LTy->isAnyPointerType() && RTy->isAnyPointerType() && Op == BO_Sub) {
+ *RetTy = getBasicVals().getContext().getPointerDiffType();
+ }
+ }
+
+ return LTy->isRealFloatingType()
+ ? Solver->fromFloatBinOp(NewLHS, Op, NewRHS)
+ : Solver->fromBinOp(NewLHS, Op, NewRHS,
+ LTy->isSignedIntegerOrEnumerationType());
+}
+
+SMTExprRef SMTConstraintManager::getRangeExpr(SymbolRef Sym,
+ const llvm::APSInt &From,
+ const llvm::APSInt &To,
+ bool InRange) {
+ // Convert lower bound
+ QualType FromTy;
+ llvm::APSInt NewFromInt;
+ std::tie(NewFromInt, FromTy) = fixAPSInt(From);
+ SMTExprRef FromExp = Solver->fromAPSInt(NewFromInt);
+
+ // Convert symbol
+ QualType SymTy;
+ SMTExprRef Exp = getExpr(Sym, &SymTy);
+
+ // Construct single (in)equality
+ if (From == To)
+ return getBinExpr(Exp, SymTy, InRange ? BO_EQ : BO_NE, FromExp, FromTy,
+ /*RetTy=*/nullptr);
+
+ QualType ToTy;
+ llvm::APSInt NewToInt;
+ std::tie(NewToInt, ToTy) = fixAPSInt(To);
+ SMTExprRef ToExp = Solver->fromAPSInt(NewToInt);
+ assert(FromTy == ToTy && "Range values have different types!");
+
+ // Construct two (in)equalities, and a logical and/or
+ SMTExprRef LHS = getBinExpr(Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
+ FromTy, /*RetTy=*/nullptr);
+ SMTExprRef RHS = getBinExpr(Exp, SymTy, InRange ? BO_LE : BO_GT, ToExp, ToTy,
+ /*RetTy=*/nullptr);
+
+ return Solver->fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
+ SymTy->isSignedIntegerOrEnumerationType());
+}
+
+//===------------------------------------------------------------------===//
+// Helper functions.
+//===------------------------------------------------------------------===//
+
+QualType SMTConstraintManager::getAPSIntType(const llvm::APSInt &Int) const {
+ ASTContext &Ctx = getBasicVals().getContext();
+ return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
+}
+
+std::pair<llvm::APSInt, QualType>
+SMTConstraintManager::fixAPSInt(const llvm::APSInt &Int) const {
+ llvm::APSInt NewInt;
+
+ // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
+ // but the former is not available in Clang. Instead, extend the APSInt
+ // directly.
+ if (Int.getBitWidth() == 1 && getAPSIntType(Int).isNull()) {
+ ASTContext &Ctx = getBasicVals().getContext();
+ NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
+ } else
+ NewInt = Int;
+
+ return std::make_pair(NewInt, getAPSIntType(NewInt));
+}
+
+void SMTConstraintManager::doTypeConversion(SMTExprRef &LHS, SMTExprRef &RHS,
+ QualType <y,
+ QualType &RTy) const {
+ assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
+
+ ASTContext &Ctx = getBasicVals().getContext();
+
+ // Perform type conversion
+ if ((LTy->isIntegralOrEnumerationType() &&
+ RTy->isIntegralOrEnumerationType()) &&
+ (LTy->isArithmeticType() && RTy->isArithmeticType())) {
+ doIntTypeConversion<SMTExprRef, &SMTSolver::fromCast>(LHS, LTy, RHS, RTy);
+ return;
+ }
+
+ if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
+ doFloatTypeConversion<SMTExprRef, &SMTSolver::fromCast>(LHS, LTy, RHS, RTy);
+ return;
+ }
+
+ if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
+ (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||
+ (LTy->isReferenceType() || RTy->isReferenceType())) {
+ // TODO: Refactor to Sema::FindCompositePointerType(), and
+ // Sema::CheckCompareOperands().
+
+ uint64_t LBitWidth = Ctx.getTypeSize(LTy);
+ uint64_t RBitWidth = Ctx.getTypeSize(RTy);
+
+ // Cast the non-pointer type to the pointer type.
+ // TODO: Be more strict about this.
+ if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||
+ (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||
+ (LTy->isReferenceType() ^ RTy->isReferenceType())) {
+ if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||
+ LTy->isReferenceType()) {
+ LHS = Solver->fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
+ LTy = RTy;
+ } else {
+ RHS = Solver->fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);
+ RTy = LTy;
+ }
+ }
+
+ // Cast the void pointer type to the non-void pointer type.
+ // For void types, this assumes that the casted value is equal to the value
+ // of the original pointer, and does not account for alignment requirements.
+ if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {
+ assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
+ "Pointer types have different bitwidths!");
+ if (RTy->isVoidPointerType())
+ RTy = LTy;
+ else
+ LTy = RTy;
+ }
+
+ if (LTy == RTy)
+ return;
+ }
+
+ // Fallback: for the solver, assume that these types don't really matter
+ if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||
+ (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType())) {
+ LTy = RTy;
+ return;
+ }
+
+ // TODO: Refine behavior for invalid type casts
+}
Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=337919&r1=337918&r2=337919&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Jul 25 05:49:29 2018
@@ -320,11 +320,11 @@ class Z3Solver : public SMTSolver {
Z3_solver Solver;
+public:
Z3Solver() : SMTSolver(), Solver(Z3_mk_simple_solver(Context.Context)) {
Z3_solver_inc_ref(Context.Context, Solver);
}
-public:
/// Override implicit copy constructor for correct reference counting.
Z3Solver(const Z3Solver &Copy)
: SMTSolver(), Context(Copy.Context), Solver(Copy.Solver) {
@@ -932,807 +932,114 @@ public:
}; // end class Z3Solver
class Z3ConstraintManager : public SMTConstraintManager {
- mutable Z3Solver Solver;
+ SMTSolverRef Solver = std::make_shared<Z3Solver>();
public:
Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
- : SMTConstraintManager(SE, SB) {}
-
- //===------------------------------------------------------------------===//
- // Implementation for Refutation.
- //===------------------------------------------------------------------===//
-
- void addRangeConstraints(clang::ento::ConstraintRangeTy CR) override;
-
- ConditionTruthVal isModelFeasible() override;
-
- LLVM_DUMP_METHOD void dump() const override;
-
- //===------------------------------------------------------------------===//
- // Implementation for interface from ConstraintManager.
- //===------------------------------------------------------------------===//
-
- bool canReasonAbout(SVal X) const override;
-
- ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
-
- const llvm::APSInt *getSymVal(ProgramStateRef State,
- SymbolRef Sym) const override;
-
- ProgramStateRef removeDeadBindings(ProgramStateRef St,
- SymbolReaper &SymReaper) override;
-
- void print(ProgramStateRef St, raw_ostream &Out, const char *nl,
- const char *sep) override;
-
- //===------------------------------------------------------------------===//
- // Implementation for interface from SimpleConstraintManager.
- //===------------------------------------------------------------------===//
-
- ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym,
- bool Assumption) override;
-
- ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
- const llvm::APSInt &From,
- const llvm::APSInt &To,
- bool InRange) override;
-
- ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
- bool Assumption) override;
-
-private:
- //===------------------------------------------------------------------===//
- // Internal implementation.
- //===------------------------------------------------------------------===//
-
- /// Given a program state, construct the logical conjunction and add it to
- /// the solver
- void addStateConstraints(ProgramStateRef State) const;
-
- // Check whether a new model is satisfiable, and update the program state.
- ProgramStateRef assumeZ3Expr(ProgramStateRef State, SymbolRef Sym,
- const SMTExprRef &Exp);
-
- // Generate and check a Z3 model, using the given constraint.
- ConditionTruthVal checkZ3Model(ProgramStateRef State,
- const SMTExprRef &Exp) const;
-
- // Generate a Z3Expr that represents the given symbolic expression.
- // Sets the hasComparison parameter if the expression has a comparison
- // operator.
- // Sets the RetTy parameter to the final return type after promotions and
- // casts.
- SMTExprRef getZ3Expr(SymbolRef Sym, QualType *RetTy = nullptr,
- bool *hasComparison = nullptr) const;
-
- // Generate a Z3Expr that takes the logical not of an expression.
- SMTExprRef getZ3NotExpr(const SMTExprRef &Exp) const;
-
- // Generate a Z3Expr that compares the expression to zero.
- SMTExprRef getZ3ZeroExpr(const SMTExprRef &Exp, QualType RetTy,
- bool Assumption) const;
-
- // Recursive implementation to unpack and generate symbolic expression.
- // Sets the hasComparison and RetTy parameters. See getZ3Expr().
- SMTExprRef getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
- bool *hasComparison) const;
-
- // Wrapper to generate Z3Expr from SymbolData.
- SMTExprRef getZ3DataExpr(const SymbolID ID, QualType Ty) const;
-
- // Wrapper to generate Z3Expr from SymbolCast.
- SMTExprRef getZ3CastExpr(const SMTExprRef &Exp, QualType FromTy,
- QualType Ty) const;
-
- // Wrapper to generate Z3Expr from BinarySymExpr.
- // Sets the hasComparison and RetTy parameters. See getZ3Expr().
- SMTExprRef getZ3SymBinExpr(const BinarySymExpr *BSE, bool *hasComparison,
- QualType *RetTy) const;
-
- // Wrapper to generate Z3Expr from unpacked binary symbolic expression.
- // Sets the RetTy parameter. See getZ3Expr().
- SMTExprRef getZ3BinExpr(const SMTExprRef &LHS, QualType LTy,
- BinaryOperator::Opcode Op, const SMTExprRef &RHS,
- QualType RTy, QualType *RetTy) const;
-
- // Wrapper to generate Z3Expr from a range. If From == To, an equality will
- // be created instead.
- SMTExprRef getZ3RangeExpr(SymbolRef Sym, const llvm::APSInt &From,
- const llvm::APSInt &To, bool InRange);
-
- //===------------------------------------------------------------------===//
- // Helper functions.
- //===------------------------------------------------------------------===//
-
- // Recover the QualType of an APSInt.
- // TODO: Refactor to put elsewhere
- QualType getAPSIntType(const llvm::APSInt &Int) const;
-
- // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
- std::pair<llvm::APSInt, QualType> fixAPSInt(const llvm::APSInt &Int) const;
-
- // Perform implicit type conversion on binary symbolic expressions.
- // May modify all input parameters.
- // TODO: Refactor to use built-in conversion functions
- void doTypeConversion(SMTExprRef &LHS, SMTExprRef &RHS, QualType <y,
- QualType &RTy) const;
-
- // Perform implicit integer type conversion.
- // May modify all input parameters.
- // TODO: Refactor to use Sema::handleIntegerConversion()
- template <typename T, T (SMTSolver::*doCast)(const T &, QualType, uint64_t,
- QualType, uint64_t)>
- void doIntTypeConversion(T &LHS, QualType <y, T &RHS, QualType &RTy) const;
-
- // Perform implicit floating-point type conversion.
- // May modify all input parameters.
- // TODO: Refactor to use Sema::handleFloatConversion()
- template <typename T, T (SMTSolver::*doCast)(const T &, QualType, uint64_t,
- QualType, uint64_t)>
- void doFloatTypeConversion(T &LHS, QualType <y, T &RHS,
- QualType &RTy) const;
-}; // end class Z3ConstraintManager
-
-} // end anonymous namespace
-
-void Z3ConstraintManager::addStateConstraints(ProgramStateRef State) const {
- // TODO: Don't add all the constraints, only the relevant ones
- ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
- ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end();
-
- // Construct the logical AND of all the constraints
- if (I != IE) {
- std::vector<SMTExprRef> ASTs;
-
- while (I != IE)
- ASTs.push_back(Solver.newExprRef(Z3Expr(I++->second)));
-
- Solver.addConstraint(Solver.fromNBinOp(BO_LAnd, ASTs));
- }
-}
-
-ProgramStateRef Z3ConstraintManager::assumeSym(ProgramStateRef State,
- SymbolRef Sym, bool Assumption) {
- QualType RetTy;
- bool hasComparison;
-
- SMTExprRef Exp = getZ3Expr(Sym, &RetTy, &hasComparison);
- // Create zero comparison for implicit boolean cast, with reversed assumption
- if (!hasComparison && !RetTy->isBooleanType())
- return assumeZ3Expr(State, Sym, getZ3ZeroExpr(Exp, RetTy, !Assumption));
-
- return assumeZ3Expr(State, Sym, Assumption ? Exp : getZ3NotExpr(Exp));
-}
-
-ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange(
- ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
- const llvm::APSInt &To, bool InRange) {
- return assumeZ3Expr(State, Sym, getZ3RangeExpr(Sym, From, To, InRange));
-}
-
-ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State,
- SymbolRef Sym,
- bool Assumption) {
- // Skip anything that is unsupported
- return State;
-}
-
-bool Z3ConstraintManager::canReasonAbout(SVal X) const {
- const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
-
- Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
- if (!SymVal)
- return true;
+ : SMTConstraintManager(SE, SB, Solver) {}
- 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;
+ void addStateConstraints(ProgramStateRef State) const override {
+ // TODO: Don't add all the constraints, only the relevant ones
+ ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
+ ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end();
+
+ // Construct the logical AND of all the constraints
+ if (I != IE) {
+ std::vector<SMTExprRef> ASTs;
+
+ SMTExprRef Constraint = Solver->newExprRef(I++->second);
+ while (I != IE) {
+ Constraint = Solver->mkAnd(Constraint, Solver->newExprRef(I++->second));
+ }
- if (isa<SymbolData>(Sym))
- return true;
+ Solver->addConstraint(Constraint);
+ }
+ }
- SValBuilder &SVB = getSValBuilder();
+ bool canReasonAbout(SVal X) const override {
+ const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
- if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
- return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
+ Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
+ if (!SymVal)
+ return true;
- if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
- if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
- return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
+ const SymExpr *Sym = SymVal->getSymbol();
+ QualType Ty = Sym->getType();
- if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
- return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));
+ // Complex types are not modeled
+ if (Ty->isComplexType() || Ty->isComplexIntegerType())
+ return false;
- if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
- return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
- canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
- }
+ // 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;
- llvm_unreachable("Unsupported expression to reason about!");
-}
+ if (isa<SymbolData>(Sym))
+ return true;
-ConditionTruthVal Z3ConstraintManager::checkNull(ProgramStateRef State,
- SymbolRef Sym) {
- QualType RetTy;
- // The expression may be casted, so we cannot call getZ3DataExpr() directly
- SMTExprRef VarExp = getZ3Expr(Sym, &RetTy);
- SMTExprRef Exp = getZ3ZeroExpr(VarExp, RetTy, true);
+ SValBuilder &SVB = getSValBuilder();
- // Negate the constraint
- SMTExprRef NotExp = getZ3ZeroExpr(VarExp, RetTy, false);
+ if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
+ return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
- Solver.reset();
- addStateConstraints(State);
+ if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
+ if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
+ return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
- Solver.push();
- Solver.addConstraint(Exp);
- ConditionTruthVal isSat = Solver.check();
+ if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
+ return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));
- Solver.pop();
- Solver.addConstraint(NotExp);
- ConditionTruthVal isNotSat = Solver.check();
+ if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
+ return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
+ canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
+ }
- // Zero is the only possible solution
- if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
- return true;
+ llvm_unreachable("Unsupported expression to reason about!");
+ }
- // Zero is not a solution
- if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
- return false;
-
- // Zero may be a solution
- return ConditionTruthVal();
-}
-
-const llvm::APSInt *Z3ConstraintManager::getSymVal(ProgramStateRef State,
- SymbolRef Sym) const {
- BasicValueFactory &BVF = getBasicVals();
- ASTContext &Ctx = BVF.getContext();
+ ProgramStateRef removeDeadBindings(ProgramStateRef State,
+ SymbolReaper &SymReaper) override {
+ ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
+ ConstraintZ3Ty::Factory &CZFactory = State->get_context<ConstraintZ3>();
- if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
- QualType Ty = Sym->getType();
- assert(!Ty->isRealFloatingType());
- llvm::APSInt Value(Ctx.getTypeSize(Ty),
- !Ty->isSignedIntegerOrEnumerationType());
-
- SMTExprRef Exp = getZ3DataExpr(SD->getSymbolID(), Ty);
-
- Solver.reset();
- addStateConstraints(State);
-
- // Constraints are unsatisfiable
- ConditionTruthVal isSat = Solver.check();
- if (!isSat.isConstrainedTrue())
- return nullptr;
-
- // Model does not assign interpretation
- if (!Solver.getInterpretation(Exp, Value))
- return nullptr;
-
- // A value has been obtained, check if it is the only value
- SMTExprRef NotExp = Solver.fromBinOp(
- Exp, BO_NE,
- Ty->isBooleanType() ? Solver.fromBoolean(Value.getBoolValue())
- : Solver.fromAPSInt(Value),
- false);
-
- Solver.addConstraint(NotExp);
-
- ConditionTruthVal isNotSat = Solver.check();
- if (isNotSat.isConstrainedTrue())
- return nullptr;
-
- // This is the only solution, store it
- return &BVF.getValue(Value);
- } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
- SymbolRef CastSym = SC->getOperand();
- QualType CastTy = SC->getType();
- // Skip the void type
- if (CastTy->isVoidType())
- return nullptr;
-
- const llvm::APSInt *Value;
- if (!(Value = getSymVal(State, CastSym)))
- return nullptr;
- return &BVF.Convert(SC->getType(), *Value);
- } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
- const llvm::APSInt *LHS, *RHS;
- if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
- LHS = getSymVal(State, SIE->getLHS());
- RHS = &SIE->getRHS();
- } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
- LHS = &ISE->getLHS();
- RHS = getSymVal(State, ISE->getRHS());
- } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
- // Early termination to avoid expensive call
- LHS = getSymVal(State, SSM->getLHS());
- RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
- } else {
- llvm_unreachable("Unsupported binary expression to get symbol value!");
+ for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
+ if (SymReaper.maybeDead(I->first))
+ CZ = CZFactory.remove(CZ, *I);
}
- if (!LHS || !RHS)
- return nullptr;
-
- llvm::APSInt ConvertedLHS, ConvertedRHS;
- QualType LTy, RTy;
- std::tie(ConvertedLHS, LTy) = fixAPSInt(*LHS);
- std::tie(ConvertedRHS, RTy) = fixAPSInt(*RHS);
- doIntTypeConversion<llvm::APSInt, &SMTSolver::castAPSInt>(
- ConvertedLHS, LTy, ConvertedRHS, RTy);
- return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
- }
-
- llvm_unreachable("Unsupported expression to get symbol value!");
-}
-
-ProgramStateRef
-Z3ConstraintManager::removeDeadBindings(ProgramStateRef State,
- SymbolReaper &SymReaper) {
- ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
- ConstraintZ3Ty::Factory &CZFactory = State->get_context<ConstraintZ3>();
-
- for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
- if (SymReaper.maybeDead(I->first))
- CZ = CZFactory.remove(CZ, *I);
- }
-
- return State->set<ConstraintZ3>(CZ);
-}
-
-void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy CR) {
- Solver.reset();
-
- for (const auto &I : CR) {
- SymbolRef Sym = I.first;
-
- SMTExprRef Constraints = Solver.fromBoolean(false);
- for (const auto &Range : I.second) {
- SMTExprRef SymRange =
- getZ3RangeExpr(Sym, Range.From(), Range.To(), /*InRange=*/true);
-
- // FIXME: the last argument (isSigned) is not used when generating the
- // or expression, as both arguments are booleans
- Constraints =
- Solver.fromBinOp(Constraints, BO_LOr, SymRange, /*IsSigned=*/true);
- }
- Solver.addConstraint(Constraints);
+ return State->set<ConstraintZ3>(CZ);
}
-}
-clang::ento::ConditionTruthVal Z3ConstraintManager::isModelFeasible() {
- return Solver.check();
-}
-
-LLVM_DUMP_METHOD void Z3ConstraintManager::dump() const { Solver.dump(); }
-
-//===------------------------------------------------------------------===//
-// Internal implementation.
-//===------------------------------------------------------------------===//
-
-ProgramStateRef Z3ConstraintManager::assumeZ3Expr(ProgramStateRef State,
- SymbolRef Sym,
- const SMTExprRef &Exp) {
- // Check the model, avoid simplifying AST to save time
- if (checkZ3Model(State, Exp).isConstrainedTrue())
- return State->add<ConstraintZ3>(std::make_pair(Sym, toZ3Expr(*Exp)));
-
- return nullptr;
-}
-
-ConditionTruthVal
-Z3ConstraintManager::checkZ3Model(ProgramStateRef State,
- const SMTExprRef &Exp) const {
- Solver.reset();
- Solver.addConstraint(Exp);
- addStateConstraints(State);
- return Solver.check();
-}
-
-SMTExprRef Z3ConstraintManager::getZ3Expr(SymbolRef Sym, QualType *RetTy,
- bool *hasComparison) const {
- if (hasComparison) {
- *hasComparison = false;
- }
-
- return getZ3SymExpr(Sym, RetTy, hasComparison);
-}
-
-SMTExprRef Z3ConstraintManager::getZ3NotExpr(const SMTExprRef &Exp) const {
- return Solver.fromUnOp(UO_LNot, Exp);
-}
-
-SMTExprRef Z3ConstraintManager::getZ3ZeroExpr(const SMTExprRef &Exp,
- QualType Ty,
- bool Assumption) const {
- ASTContext &Ctx = getBasicVals().getContext();
- if (Ty->isRealFloatingType()) {
- llvm::APFloat Zero = llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
- return Solver.fromFloatBinOp(Exp, Assumption ? BO_EQ : BO_NE,
- Solver.fromAPFloat(Zero));
- } else if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
- Ty->isBlockPointerType() || Ty->isReferenceType()) {
- bool isSigned = Ty->isSignedIntegerOrEnumerationType();
- // Skip explicit comparison for boolean types
- if (Ty->isBooleanType())
- return Assumption ? getZ3NotExpr(Exp) : Exp;
- return Solver.fromBinOp(Exp, Assumption ? BO_EQ : BO_NE,
- Solver.fromInt("0", Ctx.getTypeSize(Ty)), isSigned);
- }
-
- llvm_unreachable("Unsupported type for zero value!");
-}
-
-SMTExprRef Z3ConstraintManager::getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
- bool *hasComparison) const {
- if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
- if (RetTy)
- *RetTy = Sym->getType();
-
- return getZ3DataExpr(SD->getSymbolID(), Sym->getType());
- } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
- if (RetTy)
- *RetTy = Sym->getType();
-
- QualType FromTy;
- SMTExprRef Exp = getZ3SymExpr(SC->getOperand(), &FromTy, hasComparison);
- // Casting an expression with a comparison invalidates it. Note that this
- // must occur after the recursive call above.
- // e.g. (signed char) (x > 0)
- if (hasComparison)
- *hasComparison = false;
- return getZ3CastExpr(Exp, FromTy, Sym->getType());
- } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
- SMTExprRef Exp = getZ3SymBinExpr(BSE, hasComparison, RetTy);
- // Set the hasComparison parameter, in post-order traversal order.
- if (hasComparison)
- *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
- return Exp;
- }
-
- llvm_unreachable("Unsupported SymbolRef type!");
-}
-
-SMTExprRef Z3ConstraintManager::getZ3DataExpr(const SymbolID ID,
- QualType Ty) const {
- ASTContext &Ctx = getBasicVals().getContext();
- return Solver.fromData(ID, Ty, Ctx.getTypeSize(Ty));
-}
-
-SMTExprRef Z3ConstraintManager::getZ3CastExpr(const SMTExprRef &Exp,
- QualType FromTy,
- QualType ToTy) const {
- ASTContext &Ctx = getBasicVals().getContext();
- return Solver.fromCast(Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
- Ctx.getTypeSize(FromTy));
-}
-
-SMTExprRef Z3ConstraintManager::getZ3SymBinExpr(const BinarySymExpr *BSE,
- bool *hasComparison,
- QualType *RetTy) const {
- QualType LTy, RTy;
- BinaryOperator::Opcode Op = BSE->getOpcode();
-
- if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
- SMTExprRef LHS = getZ3SymExpr(SIE->getLHS(), <y, hasComparison);
- llvm::APSInt NewRInt;
- std::tie(NewRInt, RTy) = fixAPSInt(SIE->getRHS());
- SMTExprRef RHS = Solver.fromAPSInt(NewRInt);
- return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
- } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
- llvm::APSInt NewLInt;
- std::tie(NewLInt, LTy) = fixAPSInt(ISE->getLHS());
- SMTExprRef LHS = Solver.fromAPSInt(NewLInt);
- SMTExprRef RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison);
- return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
- } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
- SMTExprRef LHS = getZ3SymExpr(SSM->getLHS(), <y, hasComparison);
- SMTExprRef RHS = getZ3SymExpr(SSM->getRHS(), &RTy, hasComparison);
- return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
- } else {
- llvm_unreachable("Unsupported BinarySymExpr type!");
- }
-}
-
-SMTExprRef Z3ConstraintManager::getZ3BinExpr(
- const SMTExprRef &LHS, QualType LTy, BinaryOperator::Opcode Op,
- const SMTExprRef &RHS, QualType RTy, QualType *RetTy) const {
- SMTExprRef NewLHS = LHS;
- SMTExprRef NewRHS = RHS;
- doTypeConversion(NewLHS, NewRHS, LTy, RTy);
- // Update the return type parameter if the output type has changed.
- if (RetTy) {
- // A boolean result can be represented as an integer type in C/C++, but at
- // this point we only care about the Z3 type. Set it as a boolean type to
- // avoid subsequent Z3 errors.
- if (BinaryOperator::isComparisonOp(Op) || BinaryOperator::isLogicalOp(Op)) {
- ASTContext &Ctx = getBasicVals().getContext();
- *RetTy = Ctx.BoolTy;
- } else {
- *RetTy = LTy;
- }
+ ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
+ const SMTExprRef &Exp) override {
+ // Check the model, avoid simplifying AST to save time
+ if (checkModel(State, Exp).isConstrainedTrue())
+ return State->add<ConstraintZ3>(std::make_pair(Sym, toZ3Expr(*Exp)));
- // If the two operands are pointers and the operation is a subtraction, the
- // result is of type ptrdiff_t, which is signed
- if (LTy->isAnyPointerType() && RTy->isAnyPointerType() && Op == BO_Sub) {
- *RetTy = getBasicVals().getContext().getPointerDiffType();
- }
+ return nullptr;
}
- return LTy->isRealFloatingType()
- ? Solver.fromFloatBinOp(NewLHS, Op, NewRHS)
- : Solver.fromBinOp(NewLHS, Op, NewRHS,
- LTy->isSignedIntegerOrEnumerationType());
-}
-
-SMTExprRef Z3ConstraintManager::getZ3RangeExpr(SymbolRef Sym,
- const llvm::APSInt &From,
- const llvm::APSInt &To,
- bool InRange) {
- // Convert lower bound
- QualType FromTy;
- llvm::APSInt NewFromInt;
- std::tie(NewFromInt, FromTy) = fixAPSInt(From);
- SMTExprRef FromExp = Solver.fromAPSInt(NewFromInt);
-
- // Convert symbol
- QualType SymTy;
- SMTExprRef Exp = getZ3Expr(Sym, &SymTy);
-
- // Construct single (in)equality
- if (From == To)
- return getZ3BinExpr(Exp, SymTy, InRange ? BO_EQ : BO_NE, FromExp, FromTy,
- /*RetTy=*/nullptr);
-
- QualType ToTy;
- llvm::APSInt NewToInt;
- std::tie(NewToInt, ToTy) = fixAPSInt(To);
- SMTExprRef ToExp = Solver.fromAPSInt(NewToInt);
- assert(FromTy == ToTy && "Range values have different types!");
-
- // Construct two (in)equalities, and a logical and/or
- SMTExprRef LHS = getZ3BinExpr(Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
- FromTy, /*RetTy=*/nullptr);
- SMTExprRef RHS =
- getZ3BinExpr(Exp, SymTy, InRange ? BO_LE : BO_GT, ToExp, ToTy,
- /*RetTy=*/nullptr);
-
- return Solver.fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
- SymTy->isSignedIntegerOrEnumerationType());
-}
-
-//===------------------------------------------------------------------===//
-// Helper functions.
-//===------------------------------------------------------------------===//
-
-QualType Z3ConstraintManager::getAPSIntType(const llvm::APSInt &Int) const {
- ASTContext &Ctx = getBasicVals().getContext();
- return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
-}
-
-std::pair<llvm::APSInt, QualType>
-Z3ConstraintManager::fixAPSInt(const llvm::APSInt &Int) const {
- llvm::APSInt NewInt;
-
- // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
- // but the former is not available in Clang. Instead, extend the APSInt
- // directly.
- if (Int.getBitWidth() == 1 && getAPSIntType(Int).isNull()) {
- ASTContext &Ctx = getBasicVals().getContext();
- NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
- } else
- NewInt = Int;
-
- return std::make_pair(NewInt, getAPSIntType(NewInt));
-}
-
-void Z3ConstraintManager::doTypeConversion(SMTExprRef &LHS, SMTExprRef &RHS,
- QualType <y, QualType &RTy) const {
- ASTContext &Ctx = getBasicVals().getContext();
-
- assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
- // Perform type conversion
- if (LTy->isIntegralOrEnumerationType() &&
- RTy->isIntegralOrEnumerationType()) {
- if (LTy->isArithmeticType() && RTy->isArithmeticType()) {
- doIntTypeConversion<SMTExprRef, &Z3Solver::fromCast>(LHS, LTy, RHS, RTy);
- return;
- }
- } else if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
- doFloatTypeConversion<SMTExprRef, &Z3Solver::fromCast>(LHS, LTy, RHS, RTy);
- return;
- } else if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
- (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||
- (LTy->isReferenceType() || RTy->isReferenceType())) {
- // TODO: Refactor to Sema::FindCompositePointerType(), and
- // Sema::CheckCompareOperands().
-
- uint64_t LBitWidth = Ctx.getTypeSize(LTy);
- uint64_t RBitWidth = Ctx.getTypeSize(RTy);
-
- // Cast the non-pointer type to the pointer type.
- // TODO: Be more strict about this.
- if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||
- (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||
- (LTy->isReferenceType() ^ RTy->isReferenceType())) {
- if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||
- LTy->isReferenceType()) {
- LHS = Solver.fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
- LTy = RTy;
- } else {
- RHS = Solver.fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);
- RTy = LTy;
- }
- }
+ //==------------------------------------------------------------------------==/
+ // Pretty-printing.
+ //==------------------------------------------------------------------------==/
- // Cast the void pointer type to the non-void pointer type.
- // For void types, this assumes that the casted value is equal to the value
- // of the original pointer, and does not account for alignment requirements.
- if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {
- assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
- "Pointer types have different bitwidths!");
- if (RTy->isVoidPointerType())
- RTy = LTy;
- else
- LTy = RTy;
- }
+ void print(ProgramStateRef St, raw_ostream &OS, const char *nl,
+ const char *sep) override {
- if (LTy == RTy)
- return;
- }
+ ConstraintZ3Ty CZ = St->get<ConstraintZ3>();
- // Fallback: for the solver, assume that these types don't really matter
- if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||
- (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType())) {
- LTy = RTy;
- return;
- }
-
- // TODO: Refine behavior for invalid type casts
-}
-
-template <typename T, T (SMTSolver::*doCast)(const T &, QualType, uint64_t,
- QualType, uint64_t)>
-void Z3ConstraintManager::doIntTypeConversion(T &LHS, QualType <y, T &RHS,
- QualType &RTy) const {
- ASTContext &Ctx = getBasicVals().getContext();
- uint64_t LBitWidth = Ctx.getTypeSize(LTy);
- uint64_t RBitWidth = Ctx.getTypeSize(RTy);
-
- assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
- // Always perform integer promotion before checking type equality.
- // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
- if (LTy->isPromotableIntegerType()) {
- QualType NewTy = Ctx.getPromotedIntegerType(LTy);
- uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
- LHS = (Solver.*doCast)(LHS, NewTy, NewBitWidth, LTy, LBitWidth);
- LTy = NewTy;
- LBitWidth = NewBitWidth;
- }
- if (RTy->isPromotableIntegerType()) {
- QualType NewTy = Ctx.getPromotedIntegerType(RTy);
- uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
- RHS = (Solver.*doCast)(RHS, NewTy, NewBitWidth, RTy, RBitWidth);
- RTy = NewTy;
- RBitWidth = NewBitWidth;
- }
-
- if (LTy == RTy)
- return;
-
- // Perform integer type conversion
- // Note: Safe to skip updating bitwidth because this must terminate
- bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType();
- bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType();
-
- int order = Ctx.getIntegerTypeOrder(LTy, RTy);
- if (isLSignedTy == isRSignedTy) {
- // Same signedness; use the higher-ranked type
- if (order == 1) {
- RHS = (Solver.*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
- RTy = LTy;
- } else {
- LHS = (Solver.*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
- LTy = RTy;
+ OS << nl << sep << "Constraints:";
+ for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
+ OS << nl << ' ' << I->first << " : ";
+ I->second.print(OS);
}
- } else if (order != (isLSignedTy ? 1 : -1)) {
- // The unsigned type has greater than or equal rank to the
- // signed type, so use the unsigned type
- if (isRSignedTy) {
- RHS = (Solver.*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
- RTy = LTy;
- } else {
- LHS = (Solver.*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
- LTy = RTy;
- }
- } else if (LBitWidth != RBitWidth) {
- // The two types are different widths; if we are here, that
- // means the signed type is larger than the unsigned type, so
- // use the signed type.
- if (isLSignedTy) {
- RHS = (Solver.*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
- RTy = LTy;
- } else {
- LHS = (Solver.*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
- LTy = RTy;
- }
- } else {
- // The signed type is higher-ranked than the unsigned type,
- // but isn't actually any bigger (like unsigned int and long
- // on most 32-bit systems). Use the unsigned type corresponding
- // to the signed type.
- QualType NewTy = Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);
- RHS = (Solver.*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
- RTy = NewTy;
- LHS = (Solver.*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
- LTy = NewTy;
- }
-}
-
-template <typename T, T (SMTSolver::*doCast)(const T &, QualType, uint64_t,
- QualType, uint64_t)>
-void Z3ConstraintManager::doFloatTypeConversion(T &LHS, QualType <y, T &RHS,
- QualType &RTy) const {
- ASTContext &Ctx = getBasicVals().getContext();
-
- uint64_t LBitWidth = Ctx.getTypeSize(LTy);
- uint64_t RBitWidth = Ctx.getTypeSize(RTy);
-
- // Perform float-point type promotion
- if (!LTy->isRealFloatingType()) {
- LHS = (Solver.*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
- LTy = RTy;
- LBitWidth = RBitWidth;
- }
- if (!RTy->isRealFloatingType()) {
- RHS = (Solver.*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
- RTy = LTy;
- RBitWidth = LBitWidth;
- }
-
- if (LTy == RTy)
- return;
-
- // If we have two real floating types, convert the smaller operand to the
- // bigger result
- // Note: Safe to skip updating bitwidth because this must terminate
- int order = Ctx.getFloatingTypeOrder(LTy, RTy);
- if (order > 0) {
- RHS = (Solver.*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
- RTy = LTy;
- } else if (order == 0) {
- LHS = (Solver.*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
- LTy = RTy;
- } else {
- llvm_unreachable("Unsupported floating-point type cast!");
- }
-}
-
-//==------------------------------------------------------------------------==/
-// Pretty-printing.
-//==------------------------------------------------------------------------==/
-
-void Z3ConstraintManager::print(ProgramStateRef St, raw_ostream &OS,
- const char *nl, const char *sep) {
-
- ConstraintZ3Ty CZ = St->get<ConstraintZ3>();
-
- OS << nl << sep << "Constraints:";
- for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
- OS << nl << ' ' << I->first << " : ";
- I->second.print(OS);
+ OS << nl;
}
- OS << nl;
-}
+}; // end class Z3ConstraintManager
+
+} // end anonymous namespace
#endif
More information about the cfe-commits
mailing list