Index: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h =================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -58,10 +58,6 @@ 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; Index: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h =================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h @@ -18,6 +18,7 @@ namespace clang { namespace ento { +/// Generic base class for SMT contexts class SMTContext { public: SMTContext() = default; Index: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h =================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h @@ -21,6 +21,7 @@ namespace clang { namespace ento { +/// Generic base class for SMT exprs class SMTExpr { public: SMTExpr() = default; @@ -47,9 +48,12 @@ 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; } // namespace ento Index: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h =================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h @@ -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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 &ASTs) { assert(!ASTs.empty()); @@ -106,7 +110,7 @@ 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 @@ 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 @@ 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 @@ case BO_Or: return mkBVOr(LHS, RHS); - // Logical operators + // Logical operators case BO_LAnd: return mkAnd(LHS, RHS); @@ -178,8 +182,7 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ } // 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(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(Sym)) { @@ -398,21 +402,15 @@ 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 @@ 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 @@ // 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 @@ 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 @@ // 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 @@ // 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 @@ // 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 @@ } } - // 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 @@ 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 @@ virtual void print(raw_ostream &OS) const = 0; }; +/// Shared pointer for SMTSolvers. using SMTSolverRef = std::shared_ptr; +/// Convenience method to create and Z3Solver object std::unique_ptr CreateZ3Solver(); } // namespace ento Index: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h =================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h @@ -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 @@ 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 @@ 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; } // namespace ento Index: cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp =================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp +++ cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp @@ -30,8 +30,7 @@ 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 @@ 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 @@ 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); Index: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp =================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -27,6 +27,7 @@ namespace { +/// Configuration class for Z3 class Z3Config { friend class Z3Context; @@ -45,17 +46,21 @@ ~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 @@ } }; // end class Z3Context +/// Wrapper for Z3 Sort class Z3Sort : public SMTSort { friend class Z3Solver; @@ -73,6 +79,7 @@ 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(Sort)); } @@ -637,23 +644,23 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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);