r340534 - [analyzer] Moved all CSA code from the SMT API to a new header, `SMTConv.h`. NFC.
Mikhail R. Gadelha via cfe-commits
cfe-commits at lists.llvm.org
Thu Aug 23 06:21:31 PDT 2018
Author: mramalho
Date: Thu Aug 23 06:21:31 2018
New Revision: 340534
URL: http://llvm.org/viewvc/llvm-project?rev=340534&view=rev
Log:
[analyzer] Moved all CSA code from the SMT API to a new header, `SMTConv.h`. NFC.
Summary:
With this patch, the SMT backend is almost completely detached from the CSA.
Unfortunate consequence is that we missed the `ConditionTruthVal` from the CSA and had to use `Optional<bool>`.
The Z3 solver implementation is still in the same file as the `Z3ConstraintManager`, in `lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp` though, but except for that, the SMT API can be moved to anywhere in the codebase.
Reviewers: NoQ, george.karpenkov
Reviewed By: george.karpenkov
Subscribers: xazax.hun, szepet, a.sidorin, Szelethus
Differential Revision: https://reviews.llvm.org/D50772
Added:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
Modified:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
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=340534&r1=340533&r2=340534&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Thu Aug 23 06:21:31 2018
@@ -16,7 +16,7 @@
#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
namespace clang {
namespace ento {
@@ -42,13 +42,14 @@ public:
QualType RetTy;
bool hasComparison;
- SMTExprRef Exp = Solver->getExpr(Ctx, Sym, &RetTy, &hasComparison);
+ SMTExprRef Exp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
// Create zero comparison for implicit boolean cast, with reversed
// assumption
if (!hasComparison && !RetTy->isBooleanType())
- return assumeExpr(State, Sym,
- Solver->getZeroExpr(Ctx, Exp, RetTy, !Assumption));
+ return assumeExpr(
+ State, Sym,
+ SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption));
return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
}
@@ -58,8 +59,8 @@ public:
const llvm::APSInt &To,
bool InRange) override {
ASTContext &Ctx = getBasicVals().getContext();
- return assumeExpr(State, Sym,
- Solver->getRangeExpr(Ctx, Sym, From, To, InRange));
+ return assumeExpr(
+ State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange));
}
ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
@@ -77,31 +78,37 @@ public:
QualType RetTy;
// The expression may be casted, so we cannot call getZ3DataExpr() directly
- SMTExprRef VarExp = Solver->getExpr(Ctx, Sym, &RetTy);
+ SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
SMTExprRef Exp =
- Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/true);
+ SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
// Negate the constraint
SMTExprRef NotExp =
- Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/false);
+ SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
Solver->reset();
addStateConstraints(State);
Solver->push();
Solver->addConstraint(Exp);
- ConditionTruthVal isSat = Solver->check();
+
+ Optional<bool> isSat = Solver->check();
+ if (!isSat.hasValue())
+ return ConditionTruthVal();
Solver->pop();
Solver->addConstraint(NotExp);
- ConditionTruthVal isNotSat = Solver->check();
+
+ Optional<bool> isNotSat = Solver->check();
+ if (!isNotSat.hasValue())
+ return ConditionTruthVal();
// Zero is the only possible solution
- if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
+ if (isSat.getValue() && !isNotSat.getValue())
return true;
// Zero is not a solution
- if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
+ if (!isSat.getValue() && isNotSat.getValue())
return false;
// Zero may be a solution
@@ -120,14 +127,14 @@ public:
!Ty->isSignedIntegerOrEnumerationType());
SMTExprRef Exp =
- Solver->fromData(SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
+ SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
Solver->reset();
addStateConstraints(State);
// Constraints are unsatisfiable
- ConditionTruthVal isSat = Solver->check();
- if (!isSat.isConstrainedTrue())
+ Optional<bool> isSat = Solver->check();
+ if (!isSat.hasValue() || !isSat.getValue())
return nullptr;
// Model does not assign interpretation
@@ -135,16 +142,16 @@ public:
return nullptr;
// A value has been obtained, check if it is the only value
- SMTExprRef NotExp = Solver->fromBinOp(
- Exp, BO_NE,
+ SMTExprRef NotExp = SMTConv::fromBinOp(
+ Solver, Exp, BO_NE,
Ty->isBooleanType() ? Solver->fromBoolean(Value.getBoolValue())
: Solver->fromAPSInt(Value),
false);
Solver->addConstraint(NotExp);
- ConditionTruthVal isNotSat = Solver->check();
- if (isNotSat.isConstrainedTrue())
+ Optional<bool> isNotSat = Solver->check();
+ if (!isSat.hasValue() || isNotSat.getValue())
return nullptr;
// This is the only solution, store it
@@ -185,10 +192,10 @@ public:
llvm::APSInt ConvertedLHS, ConvertedRHS;
QualType LTy, RTy;
- std::tie(ConvertedLHS, LTy) = Solver->fixAPSInt(Ctx, *LHS);
- std::tie(ConvertedRHS, RTy) = Solver->fixAPSInt(Ctx, *RHS);
- Solver->doIntTypeConversion<llvm::APSInt, &SMTSolver::castAPSInt>(
- Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
+ std::tie(ConvertedLHS, LTy) = SMTConv::fixAPSInt(Ctx, *LHS);
+ std::tie(ConvertedRHS, RTy) = SMTConv::fixAPSInt(Ctx, *RHS);
+ SMTConv::doIntTypeConversion<llvm::APSInt, &SMTConv::castAPSInt>(
+ Solver, Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
}
@@ -262,9 +269,13 @@ protected:
Solver->reset();
Solver->addConstraint(Exp);
addStateConstraints(State);
- return Solver->check();
- }
+ Optional<bool> res = Solver->check();
+ if (!res.hasValue())
+ return ConditionTruthVal();
+
+ return ConditionTruthVal(res.getValue());
+ }
}; // end class SMTConstraintManager
} // namespace ento
Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h?rev=340534&view=auto
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h (added)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h Thu Aug 23 06:21:31 2018
@@ -0,0 +1,750 @@
+//== SMTConv.h --------------------------------------------------*- C++ -*--==//
+//
+// The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines a set of functions to create SMT expressions
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
+#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
+
+#include "clang/AST/Expr.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h"
+
+namespace clang {
+namespace ento {
+
+class SMTConv {
+public:
+ // Returns an appropriate sort, given a QualType and it's bit width.
+ static inline SMTSortRef mkSort(SMTSolverRef &Solver, const QualType &Ty,
+ unsigned BitWidth) {
+ if (Ty->isBooleanType())
+ return Solver->getBoolSort();
+
+ if (Ty->isRealFloatingType())
+ return Solver->getFloatSort(BitWidth);
+
+ return Solver->getBitvectorSort(BitWidth);
+ }
+
+ /// Constructs an SMTExprRef from an unary operator.
+ static inline SMTExprRef fromUnOp(SMTSolverRef &Solver,
+ const UnaryOperator::Opcode Op,
+ const SMTExprRef &Exp) {
+ switch (Op) {
+ case UO_Minus:
+ return Solver->mkBVNeg(Exp);
+
+ case UO_Not:
+ return Solver->mkBVNot(Exp);
+
+ case UO_LNot:
+ return Solver->mkNot(Exp);
+
+ default:;
+ }
+ llvm_unreachable("Unimplemented opcode");
+ }
+
+ /// Constructs an SMTExprRef from a floating-point unary operator.
+ static inline SMTExprRef fromFloatUnOp(SMTSolverRef &Solver,
+ const UnaryOperator::Opcode Op,
+ const SMTExprRef &Exp) {
+ switch (Op) {
+ case UO_Minus:
+ return Solver->mkFPNeg(Exp);
+
+ case UO_LNot:
+ return fromUnOp(Solver, Op, Exp);
+
+ default:;
+ }
+ llvm_unreachable("Unimplemented opcode");
+ }
+
+ /// Construct an SMTExprRef from a n-ary binary operator.
+ static inline SMTExprRef fromNBinOp(SMTSolverRef &Solver,
+ const BinaryOperator::Opcode Op,
+ const std::vector<SMTExprRef> &ASTs) {
+ assert(!ASTs.empty());
+
+ if (Op != BO_LAnd && Op != BO_LOr)
+ llvm_unreachable("Unimplemented opcode");
+
+ SMTExprRef res = ASTs.front();
+ for (std::size_t i = 1; i < ASTs.size(); ++i)
+ res = (Op == BO_LAnd) ? Solver->mkAnd(res, ASTs[i])
+ : Solver->mkOr(res, ASTs[i]);
+ return res;
+ }
+
+ /// Construct an SMTExprRef from a binary operator.
+ static inline SMTExprRef fromBinOp(SMTSolverRef &Solver,
+ const SMTExprRef &LHS,
+ const BinaryOperator::Opcode Op,
+ const SMTExprRef &RHS, bool isSigned) {
+ assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
+ "AST's must have the same sort!");
+
+ switch (Op) {
+ // Multiplicative operators
+ case BO_Mul:
+ return Solver->mkBVMul(LHS, RHS);
+
+ case BO_Div:
+ return isSigned ? Solver->mkBVSDiv(LHS, RHS) : Solver->mkBVUDiv(LHS, RHS);
+
+ case BO_Rem:
+ return isSigned ? Solver->mkBVSRem(LHS, RHS) : Solver->mkBVURem(LHS, RHS);
+
+ // Additive operators
+ case BO_Add:
+ return Solver->mkBVAdd(LHS, RHS);
+
+ case BO_Sub:
+ return Solver->mkBVSub(LHS, RHS);
+
+ // Bitwise shift operators
+ case BO_Shl:
+ return Solver->mkBVShl(LHS, RHS);
+
+ case BO_Shr:
+ return isSigned ? Solver->mkBVAshr(LHS, RHS) : Solver->mkBVLshr(LHS, RHS);
+
+ // Relational operators
+ case BO_LT:
+ return isSigned ? Solver->mkBVSlt(LHS, RHS) : Solver->mkBVUlt(LHS, RHS);
+
+ case BO_GT:
+ return isSigned ? Solver->mkBVSgt(LHS, RHS) : Solver->mkBVUgt(LHS, RHS);
+
+ case BO_LE:
+ return isSigned ? Solver->mkBVSle(LHS, RHS) : Solver->mkBVUle(LHS, RHS);
+
+ case BO_GE:
+ return isSigned ? Solver->mkBVSge(LHS, RHS) : Solver->mkBVUge(LHS, RHS);
+
+ // Equality operators
+ case BO_EQ:
+ return Solver->mkEqual(LHS, RHS);
+
+ case BO_NE:
+ return fromUnOp(Solver, UO_LNot,
+ fromBinOp(Solver, LHS, BO_EQ, RHS, isSigned));
+
+ // Bitwise operators
+ case BO_And:
+ return Solver->mkBVAnd(LHS, RHS);
+
+ case BO_Xor:
+ return Solver->mkBVXor(LHS, RHS);
+
+ case BO_Or:
+ return Solver->mkBVOr(LHS, RHS);
+
+ // Logical operators
+ case BO_LAnd:
+ return Solver->mkAnd(LHS, RHS);
+
+ case BO_LOr:
+ return Solver->mkOr(LHS, RHS);
+
+ default:;
+ }
+ llvm_unreachable("Unimplemented opcode");
+ }
+
+ /// Construct an SMTExprRef from a special floating-point binary operator.
+ static inline SMTExprRef
+ fromFloatSpecialBinOp(SMTSolverRef &Solver, const SMTExprRef &LHS,
+ const BinaryOperator::Opcode Op,
+ const llvm::APFloat::fltCategory &RHS) {
+ switch (Op) {
+ // Equality operators
+ case BO_EQ:
+ switch (RHS) {
+ case llvm::APFloat::fcInfinity:
+ return Solver->mkFPIsInfinite(LHS);
+
+ case llvm::APFloat::fcNaN:
+ return Solver->mkFPIsNaN(LHS);
+
+ case llvm::APFloat::fcNormal:
+ return Solver->mkFPIsNormal(LHS);
+
+ case llvm::APFloat::fcZero:
+ return Solver->mkFPIsZero(LHS);
+ }
+ break;
+
+ case BO_NE:
+ return fromFloatUnOp(Solver, UO_LNot,
+ fromFloatSpecialBinOp(Solver, LHS, BO_EQ, RHS));
+
+ default:;
+ }
+
+ llvm_unreachable("Unimplemented opcode");
+ }
+
+ /// Construct an SMTExprRef from a floating-point binary operator.
+ static inline SMTExprRef fromFloatBinOp(SMTSolverRef &Solver,
+ const SMTExprRef &LHS,
+ const BinaryOperator::Opcode Op,
+ const SMTExprRef &RHS) {
+ assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
+ "AST's must have the same sort!");
+
+ switch (Op) {
+ // Multiplicative operators
+ case BO_Mul:
+ return Solver->mkFPMul(LHS, RHS);
+
+ case BO_Div:
+ return Solver->mkFPDiv(LHS, RHS);
+
+ case BO_Rem:
+ return Solver->mkFPRem(LHS, RHS);
+
+ // Additive operators
+ case BO_Add:
+ return Solver->mkFPAdd(LHS, RHS);
+
+ case BO_Sub:
+ return Solver->mkFPSub(LHS, RHS);
+
+ // Relational operators
+ case BO_LT:
+ return Solver->mkFPLt(LHS, RHS);
+
+ case BO_GT:
+ return Solver->mkFPGt(LHS, RHS);
+
+ case BO_LE:
+ return Solver->mkFPLe(LHS, RHS);
+
+ case BO_GE:
+ return Solver->mkFPGe(LHS, RHS);
+
+ // Equality operators
+ case BO_EQ:
+ return Solver->mkFPEqual(LHS, RHS);
+
+ case BO_NE:
+ return fromFloatUnOp(Solver, UO_LNot,
+ fromFloatBinOp(Solver, LHS, BO_EQ, RHS));
+
+ // Logical operators
+ case BO_LAnd:
+ case BO_LOr:
+ return fromBinOp(Solver, LHS, Op, RHS, false);
+
+ default:;
+ }
+
+ llvm_unreachable("Unimplemented opcode");
+ }
+
+ /// Construct an SMTExprRef from a QualType FromTy to a QualType ToTy, and
+ /// their bit widths.
+ static inline SMTExprRef fromCast(SMTSolverRef &Solver, const SMTExprRef &Exp,
+ QualType ToTy, uint64_t ToBitWidth,
+ QualType FromTy, uint64_t FromBitWidth) {
+ if ((FromTy->isIntegralOrEnumerationType() &&
+ ToTy->isIntegralOrEnumerationType()) ||
+ (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) ||
+ (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) ||
+ (FromTy->isReferenceType() ^ ToTy->isReferenceType())) {
+
+ if (FromTy->isBooleanType()) {
+ assert(ToBitWidth > 0 && "BitWidth must be positive!");
+ return Solver->mkIte(
+ Exp, Solver->mkBitvector(llvm::APSInt("1"), ToBitWidth),
+ Solver->mkBitvector(llvm::APSInt("0"), ToBitWidth));
+ }
+
+ if (ToBitWidth > FromBitWidth)
+ return FromTy->isSignedIntegerOrEnumerationType()
+ ? Solver->mkBVSignExt(ToBitWidth - FromBitWidth, Exp)
+ : Solver->mkBVZeroExt(ToBitWidth - FromBitWidth, Exp);
+
+ if (ToBitWidth < FromBitWidth)
+ return Solver->mkBVExtract(ToBitWidth - 1, 0, Exp);
+
+ // Both are bitvectors with the same width, ignore the type cast
+ return Exp;
+ }
+
+ if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {
+ if (ToBitWidth != FromBitWidth)
+ return Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth));
+
+ return Exp;
+ }
+
+ if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) {
+ SMTSortRef Sort = Solver->getFloatSort(ToBitWidth);
+ return FromTy->isSignedIntegerOrEnumerationType()
+ ? Solver->mkFPtoSBV(Exp, Sort)
+ : Solver->mkFPtoUBV(Exp, Sort);
+ }
+
+ if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType())
+ return ToTy->isSignedIntegerOrEnumerationType()
+ ? Solver->mkSBVtoFP(Exp, ToBitWidth)
+ : Solver->mkUBVtoFP(Exp, ToBitWidth);
+
+ llvm_unreachable("Unsupported explicit type cast!");
+ }
+
+ // Callback function for doCast parameter on APSInt type.
+ static inline llvm::APSInt castAPSInt(SMTSolverRef &Solver,
+ const llvm::APSInt &V, QualType ToTy,
+ uint64_t ToWidth, QualType FromTy,
+ uint64_t FromWidth) {
+ APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType());
+ return TargetType.convert(V);
+ }
+
+ /// Construct an SMTExprRef from a SymbolData.
+ static inline SMTExprRef fromData(SMTSolverRef &Solver, const SymbolID ID,
+ const QualType &Ty, uint64_t BitWidth) {
+ llvm::Twine Name = "$" + llvm::Twine(ID);
+ return Solver->mkSymbol(Name.str().c_str(), mkSort(Solver, Ty, BitWidth));
+ }
+
+ // Wrapper to generate SMTExprRef from SymbolCast data.
+ static inline SMTExprRef getCastExpr(SMTSolverRef &Solver, ASTContext &Ctx,
+ const SMTExprRef &Exp, QualType FromTy,
+ QualType ToTy) {
+ return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
+ Ctx.getTypeSize(FromTy));
+ }
+
+ // Wrapper to generate SMTExprRef from unpacked binary symbolic expression.
+ // Sets the RetTy parameter. See getSMTExprRef().
+ static inline SMTExprRef getBinExpr(SMTSolverRef &Solver, ASTContext &Ctx,
+ const SMTExprRef &LHS, QualType LTy,
+ BinaryOperator::Opcode Op,
+ const SMTExprRef &RHS, QualType RTy,
+ QualType *RetTy) {
+ SMTExprRef NewLHS = LHS;
+ SMTExprRef NewRHS = RHS;
+ doTypeConversion(Solver, Ctx, 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 SMT sorts. Set it as a boolean type
+ // to avoid subsequent SMT errors.
+ if (BinaryOperator::isComparisonOp(Op) ||
+ BinaryOperator::isLogicalOp(Op)) {
+ *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 = Ctx.getPointerDiffType();
+ }
+ }
+
+ return LTy->isRealFloatingType()
+ ? fromFloatBinOp(Solver, NewLHS, Op, NewRHS)
+ : fromBinOp(Solver, NewLHS, Op, NewRHS,
+ LTy->isSignedIntegerOrEnumerationType());
+ }
+
+ // Wrapper to generate SMTExprRef from BinarySymExpr.
+ // Sets the hasComparison and RetTy parameters. See getSMTExprRef().
+ static inline SMTExprRef getSymBinExpr(SMTSolverRef &Solver, ASTContext &Ctx,
+ const BinarySymExpr *BSE,
+ bool *hasComparison, QualType *RetTy) {
+ QualType LTy, RTy;
+ BinaryOperator::Opcode Op = BSE->getOpcode();
+
+ if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
+ SMTExprRef LHS =
+ getSymExpr(Solver, Ctx, SIE->getLHS(), <y, hasComparison);
+ llvm::APSInt NewRInt;
+ std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS());
+ SMTExprRef RHS = Solver->fromAPSInt(NewRInt);
+ return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
+ }
+
+ if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
+ llvm::APSInt NewLInt;
+ std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS());
+ SMTExprRef LHS = Solver->fromAPSInt(NewLInt);
+ SMTExprRef RHS =
+ getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison);
+ return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
+ }
+
+ if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
+ SMTExprRef LHS =
+ getSymExpr(Solver, Ctx, SSM->getLHS(), <y, hasComparison);
+ SMTExprRef RHS =
+ getSymExpr(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison);
+ return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
+ }
+
+ llvm_unreachable("Unsupported BinarySymExpr type!");
+ }
+
+ // Recursive implementation to unpack and generate symbolic expression.
+ // Sets the hasComparison and RetTy parameters. See getExpr().
+ static inline SMTExprRef getSymExpr(SMTSolverRef &Solver, ASTContext &Ctx,
+ SymbolRef Sym, QualType *RetTy,
+ bool *hasComparison) {
+ if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
+ if (RetTy)
+ *RetTy = Sym->getType();
+
+ return fromData(Solver, SD->getSymbolID(), Sym->getType(),
+ Ctx.getTypeSize(Sym->getType()));
+ }
+
+ if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
+ if (RetTy)
+ *RetTy = Sym->getType();
+
+ QualType FromTy;
+ SMTExprRef Exp =
+ getSymExpr(Solver, Ctx, 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(Solver, Ctx, Exp, FromTy, Sym->getType());
+ }
+
+ if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
+ SMTExprRef Exp = getSymBinExpr(Solver, Ctx, 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!");
+ }
+
+ // Generate an SMTExprRef 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.
+ static inline SMTExprRef getExpr(SMTSolverRef &Solver, ASTContext &Ctx,
+ SymbolRef Sym, QualType *RetTy = nullptr,
+ bool *hasComparison = nullptr) {
+ if (hasComparison) {
+ *hasComparison = false;
+ }
+
+ return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison);
+ }
+
+ // Generate an SMTExprRef that compares the expression to zero.
+ static inline SMTExprRef getZeroExpr(SMTSolverRef &Solver, ASTContext &Ctx,
+ const SMTExprRef &Exp, QualType Ty,
+ bool Assumption) {
+
+ if (Ty->isRealFloatingType()) {
+ llvm::APFloat Zero =
+ llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
+ return fromFloatBinOp(Solver, 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 ? fromUnOp(Solver, UO_LNot, Exp) : Exp;
+
+ return fromBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,
+ Solver->fromInt("0", Ctx.getTypeSize(Ty)), isSigned);
+ }
+
+ llvm_unreachable("Unsupported type for zero value!");
+ }
+
+ // Wrapper to generate SMTExprRef from a range. If From == To, an equality
+ // will be created instead.
+ static inline SMTExprRef getRangeExpr(SMTSolverRef &Solver, ASTContext &Ctx,
+ 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(Ctx, From);
+ SMTExprRef FromExp = Solver->fromAPSInt(NewFromInt);
+
+ // Convert symbol
+ QualType SymTy;
+ SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy);
+
+ // Construct single (in)equality
+ if (From == To)
+ return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE,
+ FromExp, FromTy, /*RetTy=*/nullptr);
+
+ QualType ToTy;
+ llvm::APSInt NewToInt;
+ std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, 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(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
+ FromTy, /*RetTy=*/nullptr);
+ SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy,
+ InRange ? BO_LE : BO_GT, ToExp, ToTy,
+ /*RetTy=*/nullptr);
+
+ return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS,
+ SymTy->isSignedIntegerOrEnumerationType());
+ }
+
+ // Recover the QualType of an APSInt.
+ // TODO: Refactor to put elsewhere
+ static inline QualType getAPSIntType(ASTContext &Ctx,
+ const llvm::APSInt &Int) {
+ return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
+ }
+
+ // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
+ static inline std::pair<llvm::APSInt, QualType>
+ fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int) {
+ 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(Ctx, Int).isNull()) {
+ NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
+ } else
+ NewInt = Int;
+
+ return std::make_pair(NewInt, getAPSIntType(Ctx, NewInt));
+ }
+
+ // Perform implicit type conversion on binary symbolic expressions.
+ // May modify all input parameters.
+ // TODO: Refactor to use built-in conversion functions
+ static inline void doTypeConversion(SMTSolverRef &Solver, ASTContext &Ctx,
+ SMTExprRef &LHS, SMTExprRef &RHS,
+ QualType <y, QualType &RTy) {
+ assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
+
+ // Perform type conversion
+ if ((LTy->isIntegralOrEnumerationType() &&
+ RTy->isIntegralOrEnumerationType()) &&
+ (LTy->isArithmeticType() && RTy->isArithmeticType())) {
+ SMTConv::doIntTypeConversion<SMTExprRef, &fromCast>(Solver, Ctx, LHS, LTy,
+ RHS, RTy);
+ return;
+ }
+
+ if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
+ SMTConv::doFloatTypeConversion<SMTExprRef, &fromCast>(Solver, Ctx, 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 = fromCast(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
+ LTy = RTy;
+ } else {
+ RHS = fromCast(Solver, 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
+ }
+
+ // Perform implicit integer type conversion.
+ // May modify all input parameters.
+ // TODO: Refactor to use Sema::handleIntegerConversion()
+ template <typename T, T (*doCast)(SMTSolverRef &Solver, const T &, QualType,
+ uint64_t, QualType, uint64_t)>
+ static inline void doIntTypeConversion(SMTSolverRef &Solver, ASTContext &Ctx,
+ T &LHS, QualType <y, T &RHS,
+ QualType &RTy) {
+
+ 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 = (*doCast)(Solver, LHS, NewTy, NewBitWidth, LTy, LBitWidth);
+ LTy = NewTy;
+ LBitWidth = NewBitWidth;
+ }
+ if (RTy->isPromotableIntegerType()) {
+ QualType NewTy = Ctx.getPromotedIntegerType(RTy);
+ uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
+ RHS = (*doCast)(Solver, 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 = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
+ RTy = LTy;
+ } else {
+ LHS = (*doCast)(Solver, 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 = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
+ RTy = LTy;
+ } else {
+ LHS = (*doCast)(Solver, 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 = (doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
+ RTy = LTy;
+ } else {
+ LHS = (*doCast)(Solver, 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 = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
+ RTy = NewTy;
+ LHS = (doCast)(Solver, 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 (*doCast)(SMTSolverRef &Solver, const T &, QualType,
+ uint64_t, QualType, uint64_t)>
+ static inline void
+ doFloatTypeConversion(SMTSolverRef &Solver, ASTContext &Ctx, T &LHS,
+ QualType <y, T &RHS, QualType &RTy) {
+
+ uint64_t LBitWidth = Ctx.getTypeSize(LTy);
+ uint64_t RBitWidth = Ctx.getTypeSize(RTy);
+
+ // Perform float-point type promotion
+ if (!LTy->isRealFloatingType()) {
+ LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
+ LTy = RTy;
+ LBitWidth = RBitWidth;
+ }
+ if (!RTy->isRealFloatingType()) {
+ RHS = (*doCast)(Solver, 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 = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
+ RTy = LTy;
+ } else if (order == 0) {
+ LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
+ LTy = RTy;
+ } else {
+ llvm_unreachable("Unsupported floating-point type cast!");
+ }
+ }
+};
+} // namespace ento
+} // namespace clang
+
+#endif
\ No newline at end of file
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=340534&r1=340533&r2=340534&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h Thu Aug 23 06:21:31 2018
@@ -15,12 +15,9 @@
#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
-#include "clang/AST/Expr.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h"
+#include "llvm/ADT/APSInt.h"
namespace clang {
namespace ento {
@@ -53,683 +50,6 @@ public:
llvm_unreachable("Unsupported floating-point bitwidth!");
}
- // Returns an appropriate sort, given a QualType and it's bit width.
- SMTSortRef mkSort(const QualType &Ty, unsigned BitWidth) {
- if (Ty->isBooleanType())
- return getBoolSort();
-
- if (Ty->isRealFloatingType())
- return getFloatSort(BitWidth);
-
- return getBitvectorSort(BitWidth);
- }
-
- /// Constructs an SMTExprRef from an unary operator.
- SMTExprRef fromUnOp(const UnaryOperator::Opcode Op, const SMTExprRef &Exp) {
- switch (Op) {
- case UO_Minus:
- return mkBVNeg(Exp);
-
- case UO_Not:
- return mkBVNot(Exp);
-
- case UO_LNot:
- return mkNot(Exp);
-
- default:;
- }
- llvm_unreachable("Unimplemented opcode");
- }
-
- /// Constructs an SMTExprRef from a floating-point unary operator.
- SMTExprRef fromFloatUnOp(const UnaryOperator::Opcode Op,
- const SMTExprRef &Exp) {
- switch (Op) {
- case UO_Minus:
- return mkFPNeg(Exp);
-
- case UO_LNot:
- return fromUnOp(Op, Exp);
-
- default:;
- }
- llvm_unreachable("Unimplemented opcode");
- }
-
- /// Construct an SMTExprRef from a n-ary binary operator.
- SMTExprRef fromNBinOp(const BinaryOperator::Opcode Op,
- const std::vector<SMTExprRef> &ASTs) {
- assert(!ASTs.empty());
-
- if (Op != BO_LAnd && Op != BO_LOr)
- llvm_unreachable("Unimplemented opcode");
-
- SMTExprRef res = ASTs.front();
- for (std::size_t i = 1; i < ASTs.size(); ++i)
- res = (Op == BO_LAnd) ? mkAnd(res, ASTs[i]) : mkOr(res, ASTs[i]);
- return res;
- }
-
- /// Construct an SMTExprRef from a binary operator.
- SMTExprRef fromBinOp(const SMTExprRef &LHS, const BinaryOperator::Opcode Op,
- const SMTExprRef &RHS, bool isSigned) {
- assert(*getSort(LHS) == *getSort(RHS) && "AST's must have the same sort!");
-
- switch (Op) {
- // Multiplicative operators
- case BO_Mul:
- return mkBVMul(LHS, RHS);
-
- case BO_Div:
- return isSigned ? mkBVSDiv(LHS, RHS) : mkBVUDiv(LHS, RHS);
-
- case BO_Rem:
- return isSigned ? mkBVSRem(LHS, RHS) : mkBVURem(LHS, RHS);
-
- // Additive operators
- case BO_Add:
- return mkBVAdd(LHS, RHS);
-
- case BO_Sub:
- return mkBVSub(LHS, RHS);
-
- // Bitwise shift operators
- case BO_Shl:
- return mkBVShl(LHS, RHS);
-
- case BO_Shr:
- return isSigned ? mkBVAshr(LHS, RHS) : mkBVLshr(LHS, RHS);
-
- // Relational operators
- case BO_LT:
- return isSigned ? mkBVSlt(LHS, RHS) : mkBVUlt(LHS, RHS);
-
- case BO_GT:
- return isSigned ? mkBVSgt(LHS, RHS) : mkBVUgt(LHS, RHS);
-
- case BO_LE:
- return isSigned ? mkBVSle(LHS, RHS) : mkBVUle(LHS, RHS);
-
- case BO_GE:
- return isSigned ? mkBVSge(LHS, RHS) : mkBVUge(LHS, RHS);
-
- // Equality operators
- case BO_EQ:
- return mkEqual(LHS, RHS);
-
- case BO_NE:
- return fromUnOp(UO_LNot, fromBinOp(LHS, BO_EQ, RHS, isSigned));
-
- // Bitwise operators
- case BO_And:
- return mkBVAnd(LHS, RHS);
-
- case BO_Xor:
- return mkBVXor(LHS, RHS);
-
- case BO_Or:
- return mkBVOr(LHS, RHS);
-
- // Logical operators
- case BO_LAnd:
- return mkAnd(LHS, RHS);
-
- case BO_LOr:
- return mkOr(LHS, RHS);
-
- default:;
- }
- llvm_unreachable("Unimplemented opcode");
- }
-
- /// Construct an SMTExprRef from a special floating-point binary operator.
- SMTExprRef fromFloatSpecialBinOp(const SMTExprRef &LHS,
- const BinaryOperator::Opcode Op,
- const llvm::APFloat::fltCategory &RHS) {
- switch (Op) {
- // Equality operators
- case BO_EQ:
- switch (RHS) {
- case llvm::APFloat::fcInfinity:
- return mkFPIsInfinite(LHS);
-
- case llvm::APFloat::fcNaN:
- return mkFPIsNaN(LHS);
-
- case llvm::APFloat::fcNormal:
- return mkFPIsNormal(LHS);
-
- case llvm::APFloat::fcZero:
- return mkFPIsZero(LHS);
- }
- break;
-
- case BO_NE:
- return fromFloatUnOp(UO_LNot, fromFloatSpecialBinOp(LHS, BO_EQ, RHS));
-
- default:;
- }
-
- llvm_unreachable("Unimplemented opcode");
- }
-
- /// Construct an SMTExprRef from a floating-point binary operator.
- SMTExprRef fromFloatBinOp(const SMTExprRef &LHS,
- const BinaryOperator::Opcode Op,
- const SMTExprRef &RHS) {
- assert(*getSort(LHS) == *getSort(RHS) && "AST's must have the same sort!");
-
- switch (Op) {
- // Multiplicative operators
- case BO_Mul:
- return mkFPMul(LHS, RHS);
-
- case BO_Div:
- return mkFPDiv(LHS, RHS);
-
- case BO_Rem:
- return mkFPRem(LHS, RHS);
-
- // Additive operators
- case BO_Add:
- return mkFPAdd(LHS, RHS);
-
- case BO_Sub:
- return mkFPSub(LHS, RHS);
-
- // Relational operators
- case BO_LT:
- return mkFPLt(LHS, RHS);
-
- case BO_GT:
- return mkFPGt(LHS, RHS);
-
- case BO_LE:
- return mkFPLe(LHS, RHS);
-
- case BO_GE:
- return mkFPGe(LHS, RHS);
-
- // Equality operators
- case BO_EQ:
- return mkFPEqual(LHS, RHS);
-
- case BO_NE:
- return fromFloatUnOp(UO_LNot, fromFloatBinOp(LHS, BO_EQ, RHS));
-
- // Logical operators
- case BO_LAnd:
- case BO_LOr:
- return fromBinOp(LHS, Op, RHS, false);
-
- default:;
- }
-
- llvm_unreachable("Unimplemented opcode");
- }
-
- /// Construct an SMTExprRef from a QualType FromTy to a QualType ToTy, and
- /// their bit widths.
- SMTExprRef fromCast(const SMTExprRef &Exp, QualType ToTy, uint64_t ToBitWidth,
- QualType FromTy, uint64_t FromBitWidth) {
- if ((FromTy->isIntegralOrEnumerationType() &&
- ToTy->isIntegralOrEnumerationType()) ||
- (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) ||
- (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) ||
- (FromTy->isReferenceType() ^ ToTy->isReferenceType())) {
-
- if (FromTy->isBooleanType()) {
- assert(ToBitWidth > 0 && "BitWidth must be positive!");
- return mkIte(Exp, mkBitvector(llvm::APSInt("1"), ToBitWidth),
- mkBitvector(llvm::APSInt("0"), ToBitWidth));
- }
-
- if (ToBitWidth > FromBitWidth)
- return FromTy->isSignedIntegerOrEnumerationType()
- ? mkBVSignExt(ToBitWidth - FromBitWidth, Exp)
- : mkBVZeroExt(ToBitWidth - FromBitWidth, Exp);
-
- if (ToBitWidth < FromBitWidth)
- return mkBVExtract(ToBitWidth - 1, 0, Exp);
-
- // Both are bitvectors with the same width, ignore the type cast
- return Exp;
- }
-
- if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {
- if (ToBitWidth != FromBitWidth)
- return mkFPtoFP(Exp, getFloatSort(ToBitWidth));
-
- return Exp;
- }
-
- if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) {
- SMTSortRef Sort = getFloatSort(ToBitWidth);
- return FromTy->isSignedIntegerOrEnumerationType() ? mkFPtoSBV(Exp, Sort)
- : mkFPtoUBV(Exp, Sort);
- }
-
- if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType())
- return ToTy->isSignedIntegerOrEnumerationType()
- ? mkSBVtoFP(Exp, ToBitWidth)
- : mkUBVtoFP(Exp, ToBitWidth);
-
- llvm_unreachable("Unsupported explicit type cast!");
- }
-
- // Callback function for doCast parameter on APSInt type.
- llvm::APSInt castAPSInt(const llvm::APSInt &V, QualType ToTy,
- uint64_t ToWidth, QualType FromTy,
- uint64_t FromWidth) {
- APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType());
- return TargetType.convert(V);
- }
-
- // Generate an SMTExprRef 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(ASTContext &Ctx, SymbolRef Sym, QualType *RetTy = nullptr,
- bool *hasComparison = nullptr) {
- if (hasComparison) {
- *hasComparison = false;
- }
-
- return getSymExpr(Ctx, Sym, RetTy, hasComparison);
- }
-
- // Generate an SMTExprRef that compares the expression to zero.
- SMTExprRef getZeroExpr(ASTContext &Ctx, const SMTExprRef &Exp, QualType Ty,
- bool Assumption) {
-
- if (Ty->isRealFloatingType()) {
- llvm::APFloat Zero =
- llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
- return fromFloatBinOp(Exp, Assumption ? BO_EQ : BO_NE, 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 ? fromUnOp(UO_LNot, Exp) : Exp;
-
- return fromBinOp(Exp, Assumption ? BO_EQ : BO_NE,
- fromInt("0", Ctx.getTypeSize(Ty)), isSigned);
- }
-
- llvm_unreachable("Unsupported type for zero value!");
- }
-
- // Recursive implementation to unpack and generate symbolic expression.
- // Sets the hasComparison and RetTy parameters. See getExpr().
- SMTExprRef getSymExpr(ASTContext &Ctx, SymbolRef Sym, QualType *RetTy,
- bool *hasComparison) {
- if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
- if (RetTy)
- *RetTy = Sym->getType();
-
- return fromData(SD->getSymbolID(), Sym->getType(),
- Ctx.getTypeSize(Sym->getType()));
- }
-
- if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
- if (RetTy)
- *RetTy = Sym->getType();
-
- QualType FromTy;
- SMTExprRef Exp =
- getSymExpr(Ctx, 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(Ctx, Exp, FromTy, Sym->getType());
- }
-
- if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
- SMTExprRef Exp = getSymBinExpr(Ctx, 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!");
- }
-
- // Wrapper to generate SMTExprRef from SymbolCast data.
- SMTExprRef getCastExpr(ASTContext &Ctx, const SMTExprRef &Exp,
- QualType FromTy, QualType ToTy) {
- return fromCast(Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
- Ctx.getTypeSize(FromTy));
- }
-
- // Wrapper to generate SMTExprRef from BinarySymExpr.
- // Sets the hasComparison and RetTy parameters. See getSMTExprRef().
- SMTExprRef getSymBinExpr(ASTContext &Ctx, const BinarySymExpr *BSE,
- bool *hasComparison, QualType *RetTy) {
- QualType LTy, RTy;
- BinaryOperator::Opcode Op = BSE->getOpcode();
-
- if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
- SMTExprRef LHS = getSymExpr(Ctx, SIE->getLHS(), <y, hasComparison);
- llvm::APSInt NewRInt;
- std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS());
- SMTExprRef RHS = fromAPSInt(NewRInt);
- return getBinExpr(Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
- }
-
- if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
- llvm::APSInt NewLInt;
- std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS());
- SMTExprRef LHS = fromAPSInt(NewLInt);
- SMTExprRef RHS = getSymExpr(Ctx, ISE->getRHS(), &RTy, hasComparison);
- return getBinExpr(Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
- }
-
- if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
- SMTExprRef LHS = getSymExpr(Ctx, SSM->getLHS(), <y, hasComparison);
- SMTExprRef RHS = getSymExpr(Ctx, SSM->getRHS(), &RTy, hasComparison);
- return getBinExpr(Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
- }
-
- llvm_unreachable("Unsupported BinarySymExpr type!");
- }
-
- // Wrapper to generate SMTExprRef from unpacked binary symbolic expression.
- // Sets the RetTy parameter. See getSMTExprRef().
- SMTExprRef getBinExpr(ASTContext &Ctx, const SMTExprRef &LHS, QualType LTy,
- BinaryOperator::Opcode Op, const SMTExprRef &RHS,
- QualType RTy, QualType *RetTy) {
- SMTExprRef NewLHS = LHS;
- SMTExprRef NewRHS = RHS;
- doTypeConversion(Ctx, 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 SMT sorts. Set it as a boolean type
- // to avoid subsequent SMT errors.
- if (BinaryOperator::isComparisonOp(Op) ||
- BinaryOperator::isLogicalOp(Op)) {
- *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 = Ctx.getPointerDiffType();
- }
- }
-
- return LTy->isRealFloatingType()
- ? fromFloatBinOp(NewLHS, Op, NewRHS)
- : fromBinOp(NewLHS, Op, NewRHS,
- LTy->isSignedIntegerOrEnumerationType());
- }
-
- // Wrapper to generate SMTExprRef from a range. If From == To, an equality
- // will be created instead.
- SMTExprRef getRangeExpr(ASTContext &Ctx, 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(Ctx, From);
- SMTExprRef FromExp = fromAPSInt(NewFromInt);
-
- // Convert symbol
- QualType SymTy;
- SMTExprRef Exp = getExpr(Ctx, Sym, &SymTy);
-
- // Construct single (in)equality
- if (From == To)
- return getBinExpr(Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE, FromExp,
- FromTy, /*RetTy=*/nullptr);
-
- QualType ToTy;
- llvm::APSInt NewToInt;
- std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To);
- SMTExprRef ToExp = fromAPSInt(NewToInt);
- assert(FromTy == ToTy && "Range values have different types!");
-
- // Construct two (in)equalities, and a logical and/or
- SMTExprRef LHS = getBinExpr(Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT,
- FromExp, FromTy, /*RetTy=*/nullptr);
- SMTExprRef RHS =
- getBinExpr(Ctx, Exp, SymTy, InRange ? BO_LE : BO_GT, ToExp, ToTy,
- /*RetTy=*/nullptr);
-
- return fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
- SymTy->isSignedIntegerOrEnumerationType());
- }
-
- // Recover the QualType of an APSInt.
- // TODO: Refactor to put elsewhere
- QualType getAPSIntType(ASTContext &Ctx, const llvm::APSInt &Int) {
- return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
- }
-
- // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
- std::pair<llvm::APSInt, QualType> fixAPSInt(ASTContext &Ctx,
- const llvm::APSInt &Int) {
- 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(Ctx, Int).isNull()) {
- NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
- } else
- NewInt = Int;
-
- return std::make_pair(NewInt, getAPSIntType(Ctx, NewInt));
- }
-
- // Perform implicit type conversion on binary symbolic expressions.
- // May modify all input parameters.
- // TODO: Refactor to use built-in conversion functions
- void doTypeConversion(ASTContext &Ctx, SMTExprRef &LHS, SMTExprRef &RHS,
- QualType <y, QualType &RTy) {
- assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
-
- // Perform type conversion
- if ((LTy->isIntegralOrEnumerationType() &&
- RTy->isIntegralOrEnumerationType()) &&
- (LTy->isArithmeticType() && RTy->isArithmeticType())) {
- doIntTypeConversion<SMTExprRef, &SMTSolver::fromCast>(Ctx, LHS, LTy, RHS,
- RTy);
- return;
- }
-
- if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
- doFloatTypeConversion<SMTExprRef, &SMTSolver::fromCast>(Ctx, 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 = fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
- LTy = RTy;
- } else {
- RHS = 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
- }
-
- // 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(ASTContext &Ctx, T &LHS, QualType <y, T &RHS,
- QualType &RTy) {
-
- 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 = (this->*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 = (this->*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 = (this->*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
- RTy = LTy;
- } else {
- LHS = (this->*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 = (this->*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
- RTy = LTy;
- } else {
- LHS = (this->*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 = (this->*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
- RTy = LTy;
- } else {
- LHS = (this->*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 = (this->*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
- RTy = NewTy;
- LHS = (this->*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(ASTContext &Ctx, T &LHS, QualType <y, T &RHS,
- QualType &RTy) {
-
- uint64_t LBitWidth = Ctx.getTypeSize(LTy);
- uint64_t RBitWidth = Ctx.getTypeSize(RTy);
-
- // Perform float-point type promotion
- if (!LTy->isRealFloatingType()) {
- LHS = (this->*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
- LTy = RTy;
- LBitWidth = RBitWidth;
- }
- if (!RTy->isRealFloatingType()) {
- RHS = (this->*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 = (this->*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
- RTy = LTy;
- } else if (order == 0) {
- LHS = (this->*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
- LTy = RTy;
- } else {
- llvm_unreachable("Unsupported floating-point type cast!");
- }
- }
-
// Returns a boolean sort.
virtual SMTSortRef getBoolSort() = 0;
@@ -965,12 +285,8 @@ public:
/// Construct an SMTExprRef value from an integer.
virtual SMTExprRef fromInt(const char *Int, uint64_t BitWidth) = 0;
- /// Construct an SMTExprRef from a SymbolData.
- virtual SMTExprRef fromData(const SymbolID ID, const QualType &Ty,
- uint64_t BitWidth) = 0;
-
/// Check if the constraints are satisfiable
- virtual ConditionTruthVal check() const = 0;
+ virtual Optional<bool> check() const = 0;
/// Push the current solver state
virtual void push() = 0;
@@ -988,7 +304,7 @@ public:
using SMTSolverRef = std::shared_ptr<SMTSolver>;
/// Convenience method to create and Z3Solver object
-std::unique_ptr<SMTSolver> CreateZ3Solver();
+SMTSolverRef CreateZ3Solver();
} // namespace ento
} // namespace clang
Modified: cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp?rev=340534&r1=340533&r2=340534&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp Thu Aug 23 06:21:31 2018
@@ -42,10 +42,10 @@
#include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
#include "llvm/ADT/ArrayRef.h"
#include "llvm/ADT/None.h"
#include "llvm/ADT/Optional.h"
@@ -2504,7 +2504,7 @@ void FalsePositiveRefutationBRVisitor::f
VisitNode(EndPathNode, nullptr, BRC, BR);
// Create a refutation manager
- std::unique_ptr<SMTSolver> RefutationSolver = CreateZ3Solver();
+ SMTSolverRef RefutationSolver = CreateZ3Solver();
ASTContext &Ctx = BRC.getASTContext();
// Add constraints to the solver
@@ -2514,15 +2514,19 @@ void FalsePositiveRefutationBRVisitor::f
SMTExprRef Constraints = RefutationSolver->fromBoolean(false);
for (const auto &Range : I.second) {
Constraints = RefutationSolver->mkOr(
- Constraints,
- RefutationSolver->getRangeExpr(Ctx, Sym, Range.From(), Range.To(),
- /*InRange=*/true));
+ Constraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
+ Range.From(), Range.To(),
+ /*InRange=*/true));
}
RefutationSolver->addConstraint(Constraints);
}
// And check for satisfiability
- if (RefutationSolver->check().isConstrainedFalse())
+ Optional<bool> isSat = RefutationSolver->check();
+ if (!isSat.hasValue())
+ return;
+
+ if (!isSat.getValue())
BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
}
Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=340534&r1=340533&r2=340534&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Thu Aug 23 06:21:31 2018
@@ -11,9 +11,7 @@
#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
#include "clang/Config/config.h"
@@ -749,12 +747,6 @@ public:
return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));
}
- SMTExprRef fromData(const SymbolID ID, const QualType &Ty,
- uint64_t BitWidth) override {
- llvm::Twine Name = "$" + llvm::Twine(ID);
- return mkSymbol(Name.str().c_str(), mkSort(Ty, BitWidth));
- }
-
SMTExprRef fromBoolean(const bool Bool) override {
Z3_ast AST =
Bool ? Z3_mk_true(Context.Context) : Z3_mk_false(Context.Context);
@@ -872,7 +864,7 @@ public:
return toAPFloat(Sort, Assign, Float, true);
}
- ConditionTruthVal check() const override {
+ Optional<bool> check() const override {
Z3_lbool res = Z3_solver_check(Context.Context, Solver);
if (res == Z3_L_TRUE)
return true;
@@ -880,7 +872,7 @@ public:
if (res == Z3_L_FALSE)
return false;
- return ConditionTruthVal();
+ return Optional<bool>();
}
void push() override { return Z3_solver_push(Context.Context, Solver); }
@@ -959,7 +951,7 @@ public:
#endif
-std::unique_ptr<SMTSolver> clang::ento::CreateZ3Solver() {
+SMTSolverRef clang::ento::CreateZ3Solver() {
#if CLANG_ANALYZER_WITH_Z3
return llvm::make_unique<Z3Solver>();
#else
More information about the cfe-commits
mailing list