r337954 - [analyzer] Update SMT API documentation and methods
Mikhail R. Gadelha via cfe-commits
cfe-commits at lists.llvm.org
Wed Jul 25 12:34:49 PDT 2018
Author: mramalho
Date: Wed Jul 25 12:34:48 2018
New Revision: 337954
URL: http://llvm.org/viewvc/llvm-project?rev=337954&view=rev
Log:
[analyzer] Update SMT API documentation and methods
Summary:
Update the documentation of all the classes introduced with the new generic SMT API, most of them were referencing Z3 and how previous operations were being done (like including the context as parameter in a few methods).
Renamed the following methods, so it's clear that the operate on bitvectors:
*`mkSignExt` -> `mkBVSignExt`
*`mkZeroExt` -> `mkBVZeroExt`
*`mkExtract` -> `mkBVExtract`
*`mkConcat` -> `mkBVConcat`
Removed the unecessary methods:
* `getDataExpr`: it was an one line method that called `fromData`
* `mkBitvector(const llvm::APSInt Int)`: it was not being used anywhere
Reviewers: NoQ, george.karpenkov
Reviewed By: george.karpenkov
Subscribers: xazax.hun, szepet, a.sidorin
Differential Revision: https://reviews.llvm.org/D49799
Modified:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h
cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.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=337954&r1=337953&r2=337954&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Wed Jul 25 12:34:48 2018
@@ -58,10 +58,6 @@ public:
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;
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h?rev=337954&r1=337953&r2=337954&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h Wed Jul 25 12:34:48 2018
@@ -18,6 +18,7 @@
namespace clang {
namespace ento {
+/// Generic base class for SMT contexts
class SMTContext {
public:
SMTContext() = default;
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h?rev=337954&r1=337953&r2=337954&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h Wed Jul 25 12:34:48 2018
@@ -21,6 +21,7 @@
namespace clang {
namespace ento {
+/// Generic base class for SMT exprs
class SMTExpr {
public:
SMTExpr() = default;
@@ -47,9 +48,12 @@ public:
LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
protected:
+ /// Query the SMT solver and returns true if two sorts are equal (same kind
+ /// and bit width). This does not check if the two sorts are the same objects.
virtual bool equal_to(SMTExpr const &other) const = 0;
};
+/// Shared pointer for SMTExprs, used by SMTSolver API.
using SMTExprRef = std::shared_ptr<SMTExpr>;
} // namespace ento
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=337954&r1=337953&r2=337954&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h Wed Jul 25 12:34:48 2018
@@ -25,6 +25,11 @@
namespace clang {
namespace ento {
+/// Generic base class for SMT Solvers
+///
+/// This class is responsible for wrapping all sorts and expression generation,
+/// through the mk* methods. It also provides methods to create SMT expressions
+/// straight from clang's AST, through the from* methods.
class SMTSolver {
public:
SMTSolver() = default;
@@ -32,7 +37,7 @@ public:
LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
- // Return an appropriate floating-point sort for the given bitwidth.
+ // Returns an appropriate floating-point sort for the given bitwidth.
SMTSortRef getFloatSort(unsigned BitWidth) {
switch (BitWidth) {
case 16:
@@ -48,7 +53,7 @@ public:
llvm_unreachable("Unsupported floating-point bitwidth!");
}
- // Return an appropriate sort, given a QualType
+ // Returns an appropriate sort, given a QualType and it's bit width.
SMTSortRef mkSort(const QualType &Ty, unsigned BitWidth) {
if (Ty->isBooleanType())
return getBoolSort();
@@ -59,7 +64,7 @@ public:
return getBitvectorSort(BitWidth);
}
- /// Construct a Z3Expr from a unary operator, given a Z3_context.
+ /// Constructs an SMTExprRef from an unary operator.
SMTExprRef fromUnOp(const UnaryOperator::Opcode Op, const SMTExprRef &Exp) {
switch (Op) {
case UO_Minus:
@@ -76,8 +81,7 @@ public:
llvm_unreachable("Unimplemented opcode");
}
- /// Construct a Z3Expr from a floating-point unary operator, given a
- /// Z3_context.
+ /// Constructs an SMTExprRef from a floating-point unary operator.
SMTExprRef fromFloatUnOp(const UnaryOperator::Opcode Op,
const SMTExprRef &Exp) {
switch (Op) {
@@ -92,7 +96,7 @@ public:
llvm_unreachable("Unimplemented opcode");
}
- /// Construct a Z3Expr from a n-ary binary operator.
+ /// Construct an SMTExprRef from a n-ary binary operator.
SMTExprRef fromNBinOp(const BinaryOperator::Opcode Op,
const std::vector<SMTExprRef> &ASTs) {
assert(!ASTs.empty());
@@ -106,7 +110,7 @@ public:
return res;
}
- /// Construct a Z3Expr from a binary operator, given a Z3_context.
+ /// 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!");
@@ -122,21 +126,21 @@ public:
case BO_Rem:
return isSigned ? mkBVSRem(LHS, RHS) : mkBVURem(LHS, RHS);
- // Additive operators
+ // Additive operators
case BO_Add:
return mkBVAdd(LHS, RHS);
case BO_Sub:
return mkBVSub(LHS, RHS);
- // Bitwise shift operators
+ // Bitwise shift operators
case BO_Shl:
return mkBVShl(LHS, RHS);
case BO_Shr:
return isSigned ? mkBVAshr(LHS, RHS) : mkBVLshr(LHS, RHS);
- // Relational operators
+ // Relational operators
case BO_LT:
return isSigned ? mkBVSlt(LHS, RHS) : mkBVUlt(LHS, RHS);
@@ -149,14 +153,14 @@ public:
case BO_GE:
return isSigned ? mkBVSge(LHS, RHS) : mkBVUge(LHS, RHS);
- // Equality operators
+ // Equality operators
case BO_EQ:
return mkEqual(LHS, RHS);
case BO_NE:
return fromUnOp(UO_LNot, fromBinOp(LHS, BO_EQ, RHS, isSigned));
- // Bitwise operators
+ // Bitwise operators
case BO_And:
return mkBVAnd(LHS, RHS);
@@ -166,7 +170,7 @@ public:
case BO_Or:
return mkBVOr(LHS, RHS);
- // Logical operators
+ // Logical operators
case BO_LAnd:
return mkAnd(LHS, RHS);
@@ -178,8 +182,7 @@ public:
llvm_unreachable("Unimplemented opcode");
}
- /// Construct a Z3Expr from a special floating-point binary operator, given
- /// a Z3_context.
+ /// Construct an SMTExprRef from a special floating-point binary operator.
SMTExprRef fromFloatSpecialBinOp(const SMTExprRef &LHS,
const BinaryOperator::Opcode Op,
const llvm::APFloat::fltCategory &RHS) {
@@ -210,8 +213,7 @@ public:
llvm_unreachable("Unimplemented opcode");
}
- /// Construct a Z3Expr from a floating-point binary operator, given a
- /// Z3_context.
+ /// Construct an SMTExprRef from a floating-point binary operator.
SMTExprRef fromFloatBinOp(const SMTExprRef &LHS,
const BinaryOperator::Opcode Op,
const SMTExprRef &RHS) {
@@ -266,7 +268,8 @@ public:
llvm_unreachable("Unimplemented opcode");
}
- /// Construct a Z3Expr from a SymbolCast, given a Z3_context.
+ /// 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() &&
@@ -283,11 +286,11 @@ public:
if (ToBitWidth > FromBitWidth)
return FromTy->isSignedIntegerOrEnumerationType()
- ? mkSignExt(ToBitWidth - FromBitWidth, Exp)
- : mkZeroExt(ToBitWidth - FromBitWidth, Exp);
+ ? mkBVSignExt(ToBitWidth - FromBitWidth, Exp)
+ : mkBVZeroExt(ToBitWidth - FromBitWidth, Exp);
if (ToBitWidth < FromBitWidth)
- return mkExtract(ToBitWidth - 1, 0, Exp);
+ return mkBVExtract(ToBitWidth - 1, 0, Exp);
// Both are bitvectors with the same width, ignore the type cast
return Exp;
@@ -322,7 +325,7 @@ public:
return TargetType.convert(V);
}
- // Generate a Z3Expr that represents the given symbolic expression.
+ // 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
@@ -336,7 +339,7 @@ public:
return getSymExpr(Ctx, Sym, RetTy, hasComparison);
}
- // Generate a Z3Expr that compares the expression to zero.
+ // Generate an SMTExprRef that compares the expression to zero.
SMTExprRef getZeroExpr(ASTContext &Ctx, const SMTExprRef &Exp, QualType Ty,
bool Assumption) {
@@ -362,14 +365,15 @@ public:
}
// Recursive implementation to unpack and generate symbolic expression.
- // Sets the hasComparison and RetTy parameters. See getZ3Expr().
+ // 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 getDataExpr(Ctx, SD->getSymbolID(), Sym->getType());
+ return fromData(SD->getSymbolID(), Sym->getType(),
+ Ctx.getTypeSize(Sym->getType()));
}
if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
@@ -398,21 +402,15 @@ public:
llvm_unreachable("Unsupported SymbolRef type!");
}
- // Wrapper to generate Z3Expr from SymbolData.
- SMTExprRef getDataExpr(ASTContext &Ctx, const SymbolID ID, QualType Ty) {
- return fromData(ID, Ty, Ctx.getTypeSize(Ty));
- }
-
- // Wrapper to generate Z3Expr from SymbolCast.
+ // 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 Z3Expr from BinarySymExpr.
- // Sets the hasComparison and RetTy parameters. See getZ3Expr().
+ // 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;
@@ -443,8 +441,8 @@ public:
llvm_unreachable("Unsupported BinarySymExpr type!");
}
- // Wrapper to generate Z3Expr from unpacked binary symbolic expression.
- // Sets the RetTy parameter. See getZ3Expr().
+ // 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) {
@@ -455,11 +453,10 @@ public:
// 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.
+ // 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;
@@ -478,8 +475,8 @@ public:
LTy->isSignedIntegerOrEnumerationType());
}
- // Wrapper to generate Z3Expr from a range. If From == To, an equality will
- // be created instead.
+ // 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) {
@@ -496,8 +493,7 @@ public:
// Construct single (in)equality
if (From == To)
return getBinExpr(Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE, FromExp,
- FromTy,
- /*RetTy=*/nullptr);
+ FromTy, /*RetTy=*/nullptr);
QualType ToTy;
llvm::APSInt NewToInt;
@@ -519,7 +515,6 @@ public:
// 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());
}
@@ -532,7 +527,6 @@ public:
// 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;
@@ -736,189 +730,221 @@ public:
}
}
- // Return a boolean sort.
+ // Returns a boolean sort.
virtual SMTSortRef getBoolSort() = 0;
- // Return an appropriate bitvector sort for the given bitwidth.
+ // Returns an appropriate bitvector sort for the given bitwidth.
virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0;
- // Return a floating-point sort of width 16
+ // Returns a floating-point sort of width 16
virtual SMTSortRef getFloat16Sort() = 0;
- // Return a floating-point sort of width 32
+ // Returns a floating-point sort of width 32
virtual SMTSortRef getFloat32Sort() = 0;
- // Return a floating-point sort of width 64
+ // Returns a floating-point sort of width 64
virtual SMTSortRef getFloat64Sort() = 0;
- // Return a floating-point sort of width 128
+ // Returns a floating-point sort of width 128
virtual SMTSortRef getFloat128Sort() = 0;
- // Return an appropriate sort for the given AST.
+ // Returns an appropriate sort for the given AST.
virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;
- // Return a new SMTExprRef from an SMTExpr
+ // Returns a new SMTExprRef from an SMTExpr
virtual SMTExprRef newExprRef(const SMTExpr &E) const = 0;
- /// Given a constraint, add it to the solver
+ /// Given a constraint, adds it to the solver
virtual void addConstraint(const SMTExprRef &Exp) const = 0;
- /// Create a bitvector addition operation
+ /// Creates a bitvector addition operation
virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector subtraction operation
+ /// Creates a bitvector subtraction operation
virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector multiplication operation
+ /// Creates a bitvector multiplication operation
virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector signed modulus operation
+ /// Creates a bitvector signed modulus operation
virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector unsigned modulus operation
+ /// Creates a bitvector unsigned modulus operation
virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector signed division operation
+ /// Creates a bitvector signed division operation
virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector unsigned division operation
+ /// Creates a bitvector unsigned division operation
virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector logical shift left operation
+ /// Creates a bitvector logical shift left operation
virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector arithmetic shift right operation
+ /// Creates a bitvector arithmetic shift right operation
virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector logical shift right operation
+ /// Creates a bitvector logical shift right operation
virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector negation operation
+ /// Creates a bitvector negation operation
virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0;
- /// Create a bitvector not operation
+ /// Creates a bitvector not operation
virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0;
- /// Create a bitvector xor operation
+ /// Creates a bitvector xor operation
virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector or operation
+ /// Creates a bitvector or operation
virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector and operation
+ /// Creates a bitvector and operation
virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector unsigned less-than operation
+ /// Creates a bitvector unsigned less-than operation
virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector signed less-than operation
+ /// Creates a bitvector signed less-than operation
virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector unsigned greater-than operation
+ /// Creates a bitvector unsigned greater-than operation
virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector signed greater-than operation
+ /// Creates a bitvector signed greater-than operation
virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector unsigned less-equal-than operation
+ /// Creates a bitvector unsigned less-equal-than operation
virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector signed less-equal-than operation
+ /// Creates a bitvector signed less-equal-than operation
virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector unsigned greater-equal-than operation
+ /// Creates a bitvector unsigned greater-equal-than operation
virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a bitvector signed greater-equal-than operation
+ /// Creates a bitvector signed greater-equal-than operation
virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
- /// Create a boolean not operation
+ /// Creates a boolean not operation
virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0;
- /// Create a bitvector equality operation
+ /// Creates a boolean equality operation
virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+ /// Creates a boolean and operation
virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+ /// Creates a boolean or operation
virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+ /// Creates a boolean ite operation
virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
const SMTExprRef &F) = 0;
- virtual SMTExprRef mkSignExt(unsigned i, const SMTExprRef &Exp) = 0;
+ /// Creates a bitvector sign extension operation
+ virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) = 0;
- virtual SMTExprRef mkZeroExt(unsigned i, const SMTExprRef &Exp) = 0;
+ /// Creates a bitvector zero extension operation
+ virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) = 0;
- virtual SMTExprRef mkExtract(unsigned High, unsigned Low,
- const SMTExprRef &Exp) = 0;
+ /// Creates a bitvector extract operation
+ virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low,
+ const SMTExprRef &Exp) = 0;
- virtual SMTExprRef mkConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+ /// Creates a bitvector concat operation
+ virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS,
+ const SMTExprRef &RHS) = 0;
+ /// Creates a floating-point negation operation
virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0;
+ /// Creates a floating-point isInfinite operation
virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) = 0;
+ /// Creates a floating-point isNaN operation
virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) = 0;
+ /// Creates a floating-point isNormal operation
virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) = 0;
+ /// Creates a floating-point isZero operation
virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp) = 0;
+ /// Creates a floating-point multiplication operation
virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+ /// Creates a floating-point division operation
virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+ /// Creates a floating-point remainder operation
virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+ /// Creates a floating-point addition operation
virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+ /// Creates a floating-point subtraction operation
virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+ /// Creates a floating-point less-than operation
virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+ /// Creates a floating-point greater-than operation
virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+ /// Creates a floating-point less-than-or-equal operation
virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+ /// Creates a floating-point greater-than-or-equal operation
virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+ /// Creates a floating-point equality operation
virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS,
const SMTExprRef &RHS) = 0;
+ /// Creates a floating-point conversion from floatint-point to floating-point
+ /// operation
virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0;
+ /// Creates a floating-point conversion from floatint-point to signed
+ /// bitvector operation
virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From,
const SMTSortRef &To) = 0;
+ /// Creates a floating-point conversion from floatint-point to unsigned
+ /// bitvector operation
virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From,
const SMTSortRef &To) = 0;
+ /// Creates a floating-point conversion from signed bitvector to
+ /// floatint-point operation
virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From, unsigned ToWidth) = 0;
+ /// Creates a floating-point conversion from unsigned bitvector to
+ /// floatint-point operation
virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From, unsigned ToWidth) = 0;
+ /// Creates a new symbol, given a name and a sort
virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0;
- // Return an appropriate floating-point rounding mode.
+ // Returns an appropriate floating-point rounding mode.
virtual SMTExprRef getFloatRoundingMode() = 0;
+ // If the a model is available, returns the value of a given bitvector symbol
virtual const llvm::APSInt getBitvector(const SMTExprRef &Exp) = 0;
+ // If the a model is available, returns the value of a given boolean symbol
virtual bool getBoolean(const SMTExprRef &Exp) = 0;
- /// Construct a const SMTExprRef &From a boolean.
+ /// Constructs an SMTExprRef from a boolean.
virtual SMTExprRef mkBoolean(const bool b) = 0;
- /// Construct a const SMTExprRef &From a finite APFloat.
+ /// Constructs an SMTExprRef from a finite APFloat.
virtual SMTExprRef mkFloat(const llvm::APFloat Float) = 0;
- /// Construct a const SMTExprRef &From an APSInt.
+ /// Constructs an SMTExprRef from an APSInt and its bit width
virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0;
- SMTExprRef mkBitvector(const llvm::APSInt Int) {
- return mkBitvector(Int, Int.getBitWidth());
- }
-
/// Given an expression, extract the value of this operand in the model.
virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) = 0;
@@ -926,18 +952,19 @@ public:
virtual bool getInterpretation(const SMTExprRef &Exp,
llvm::APFloat &Float) = 0;
- /// Construct a Z3Expr from a boolean, given a Z3_context.
+ /// Construct an SMTExprRef value from a boolean.
virtual SMTExprRef fromBoolean(const bool Bool) = 0;
- /// Construct a Z3Expr from a finite APFloat, given a Z3_context.
+
+ /// Construct an SMTExprRef value from a finite APFloat.
virtual SMTExprRef fromAPFloat(const llvm::APFloat &Float) = 0;
- /// Construct a Z3Expr from an APSInt, given a Z3_context.
+ /// Construct an SMTExprRef value from an APSInt.
virtual SMTExprRef fromAPSInt(const llvm::APSInt &Int) = 0;
- /// Construct a Z3Expr from an integer, given a Z3_context.
+ /// Construct an SMTExprRef value from an integer.
virtual SMTExprRef fromInt(const char *Int, uint64_t BitWidth) = 0;
- /// Construct a const SMTExprRef &From a SymbolData, given a SMT_context.
+ /// Construct an SMTExprRef from a SymbolData.
virtual SMTExprRef fromData(const SymbolID ID, const QualType &Ty,
uint64_t BitWidth) = 0;
@@ -956,8 +983,10 @@ public:
virtual void print(raw_ostream &OS) const = 0;
};
+/// Shared pointer for SMTSolvers.
using SMTSolverRef = std::shared_ptr<SMTSolver>;
+/// Convenience method to create and Z3Solver object
std::unique_ptr<SMTSolver> CreateZ3Solver();
} // namespace ento
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h?rev=337954&r1=337953&r2=337954&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h Wed Jul 25 12:34:48 2018
@@ -20,15 +20,23 @@
namespace clang {
namespace ento {
+/// Generic base class for SMT sorts
class SMTSort {
public:
SMTSort() = default;
virtual ~SMTSort() = default;
+ /// Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); }
+
+ /// Returns true if the sort is a floating-point, calls isFloatSortImpl().
virtual bool isFloatSort() const { return isFloatSortImpl(); }
+
+ /// Returns true if the sort is a boolean, calls isBooleanSortImpl().
virtual bool isBooleanSort() const { return isBooleanSortImpl(); }
+ /// Returns the bitvector size, fails if the sort is not a bitvector
+ /// Calls getBitvectorSortSizeImpl().
virtual unsigned getBitvectorSortSize() const {
assert(isBitvectorSort() && "Not a bitvector sort!");
unsigned Size = getBitvectorSortSizeImpl();
@@ -36,6 +44,8 @@ public:
return Size;
};
+ /// Returns the floating-point size, fails if the sort is not a floating-point
+ /// Calls getFloatSortSizeImpl().
virtual unsigned getFloatSortSize() const {
assert(isFloatSort() && "Not a floating-point sort!");
unsigned Size = getFloatSortSizeImpl();
@@ -52,19 +62,27 @@ public:
LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
protected:
+ /// Query the SMT solver and returns true if two sorts are equal (same kind
+ /// and bit width). This does not check if the two sorts are the same objects.
virtual bool equal_to(SMTSort const &other) const = 0;
+ /// Query the SMT solver and checks if a sort is bitvector.
virtual bool isBitvectorSortImpl() const = 0;
+ /// Query the SMT solver and checks if a sort is floating-point.
virtual bool isFloatSortImpl() const = 0;
+ /// Query the SMT solver and checks if a sort is boolean.
virtual bool isBooleanSortImpl() const = 0;
+ /// Query the SMT solver and returns the sort bit width.
virtual unsigned getBitvectorSortSizeImpl() const = 0;
+ /// Query the SMT solver and returns the sort bit width.
virtual unsigned getFloatSortSizeImpl() const = 0;
};
+/// Shared pointer for SMTSorts, used by SMTSolver API.
using SMTSortRef = std::shared_ptr<SMTSort>;
} // namespace ento
Modified: cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp?rev=337954&r1=337953&r2=337954&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp Wed Jul 25 12:34:48 2018
@@ -30,8 +30,7 @@ ProgramStateRef SMTConstraintManager::as
return assumeExpr(State, Sym,
Solver->getZeroExpr(Ctx, Exp, RetTy, !Assumption));
- return assumeExpr(State, Sym,
- Assumption ? Exp : Solver->fromUnOp(UO_LNot, Exp));
+ return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
}
ProgramStateRef SMTConstraintManager::assumeSymInclusiveRange(
@@ -56,10 +55,11 @@ ConditionTruthVal SMTConstraintManager::
QualType RetTy;
// The expression may be casted, so we cannot call getZ3DataExpr() directly
SMTExprRef VarExp = Solver->getExpr(Ctx, Sym, &RetTy);
- SMTExprRef Exp = Solver->getZeroExpr(Ctx, VarExp, RetTy, true);
+ SMTExprRef Exp = Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/true);
// Negate the constraint
- SMTExprRef NotExp = Solver->getZeroExpr(Ctx, VarExp, RetTy, false);
+ SMTExprRef NotExp =
+ Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/false);
Solver->reset();
addStateConstraints(State);
@@ -95,7 +95,8 @@ const llvm::APSInt *SMTConstraintManager
llvm::APSInt Value(Ctx.getTypeSize(Ty),
!Ty->isSignedIntegerOrEnumerationType());
- SMTExprRef Exp = Solver->getDataExpr(Ctx, SD->getSymbolID(), Ty);
+ SMTExprRef Exp =
+ Solver->fromData(SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
Solver->reset();
addStateConstraints(State);
Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=337954&r1=337953&r2=337954&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Jul 25 12:34:48 2018
@@ -27,6 +27,7 @@ using namespace ento;
namespace {
+/// Configuration class for Z3
class Z3Config {
friend class Z3Context;
@@ -45,17 +46,21 @@ public:
~Z3Config() { Z3_del_config(Config); }
}; // end class Z3Config
+// Function used to report errors
void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
llvm::report_fatal_error("Z3 error: " +
llvm::Twine(Z3_get_error_msg_ex(Context, Error)));
}
+/// Wrapper for Z3 context
class Z3Context : public SMTContext {
public:
Z3_context Context;
Z3Context() : SMTContext() {
Context = Z3_mk_context_rc(Z3Config().Config);
+ // The error function is set here because the context is the first object
+ // created by the backend
Z3_set_error_handler(Context, Z3ErrorHandler);
}
@@ -65,6 +70,7 @@ public:
}
}; // end class Z3Context
+/// Wrapper for Z3 Sort
class Z3Sort : public SMTSort {
friend class Z3Solver;
@@ -73,6 +79,7 @@ class Z3Sort : public SMTSort {
Z3_sort Sort;
public:
+ /// Default constructor, mainly used by make_shared
Z3Sort(Z3Context &C, Z3_sort ZS) : SMTSort(), Context(C), Sort(ZS) {
Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
}
@@ -637,23 +644,23 @@ public:
toZ3Expr(*T).AST, toZ3Expr(*F).AST)));
}
- SMTExprRef mkSignExt(unsigned i, const SMTExprRef &Exp) override {
+ SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) override {
return newExprRef(Z3Expr(
Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
}
- SMTExprRef mkZeroExt(unsigned i, const SMTExprRef &Exp) override {
+ SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) override {
return newExprRef(Z3Expr(
Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
}
- SMTExprRef mkExtract(unsigned High, unsigned Low,
- const SMTExprRef &Exp) override {
+ SMTExprRef mkBVExtract(unsigned High, unsigned Low,
+ const SMTExprRef &Exp) override {
return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low,
toZ3Expr(*Exp).AST)));
}
- SMTExprRef mkConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+ SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
return newExprRef(
Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,
toZ3Expr(*RHS).AST)));
@@ -737,27 +744,23 @@ public:
return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
}
- // Return an appropriate floating-point rounding mode.
SMTExprRef getFloatRoundingMode() override {
// TODO: Don't assume nearest ties to even rounding mode
return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));
}
- /// Construct a Z3Expr from a SymbolData, given a Z3_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));
}
- /// Construct a Z3Expr from a boolean, given a Z3_context.
SMTExprRef fromBoolean(const bool Bool) override {
Z3_ast AST =
Bool ? Z3_mk_true(Context.Context) : Z3_mk_false(Context.Context);
return newExprRef(Z3Expr(Context, AST));
}
- /// Construct a Z3Expr from a finite APFloat, given a Z3_context.
SMTExprRef fromAPFloat(const llvm::APFloat &Float) override {
SMTSortRef Sort =
getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
@@ -769,7 +772,6 @@ public:
toZ3Sort(*Sort).Sort)));
}
- /// Construct a Z3Expr from an APSInt, given a Z3_context.
SMTExprRef fromAPSInt(const llvm::APSInt &Int) override {
SMTSortRef Sort = getBitvectorSort(Int.getBitWidth());
Z3_ast AST = Z3_mk_numeral(Context.Context, Int.toString(10).c_str(),
@@ -777,7 +779,6 @@ public:
return newExprRef(Z3Expr(Context, AST));
}
- /// Construct a Z3Expr from an integer, given a Z3_context.
SMTExprRef fromInt(const char *Int, uint64_t BitWidth) override {
SMTSortRef Sort = getBitvectorSort(BitWidth);
Z3_ast AST = Z3_mk_numeral(Context.Context, Int, toZ3Sort(*Sort).Sort);
@@ -823,7 +824,7 @@ public:
Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]),
Int.isUnsigned());
} else if (Sort->getBitvectorSortSize() == 128) {
- SMTExprRef ASTHigh = mkExtract(127, 64, AST);
+ SMTExprRef ASTHigh = mkBVExtract(127, 64, AST);
Z3_get_numeral_uint64(Context.Context, toZ3Expr(*AST).AST,
reinterpret_cast<__uint64 *>(&Value[1]));
Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value),
@@ -849,8 +850,6 @@ public:
llvm_unreachable("Unsupported sort to integer!");
}
- /// Given an expression and a model, extract the value of this operand in
- /// the model.
bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override {
Z3Model Model = getModel();
Z3_func_decl Func = Z3_get_app_decl(
@@ -865,8 +864,6 @@ public:
return toAPSInt(Sort, Assign, Int, true);
}
- /// Given an expression and a model, extract the value of this operand in
- /// the model.
bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override {
Z3Model Model = getModel();
Z3_func_decl Func = Z3_get_app_decl(
@@ -881,7 +878,6 @@ public:
return toAPFloat(Sort, Assign, Float, true);
}
- /// Check if the constraints are satisfiable
ConditionTruthVal check() const override {
Z3_lbool res = Z3_solver_check(Context.Context, Solver);
if (res == Z3_L_TRUE)
@@ -893,10 +889,8 @@ public:
return ConditionTruthVal();
}
- /// Push the current solver state
void push() override { return Z3_solver_push(Context.Context, Solver); }
- /// Pop the previous solver state
void pop(unsigned NumStates = 1) override {
assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);
return Z3_solver_pop(Context.Context, Solver, NumStates);
More information about the cfe-commits
mailing list