Index: include/clang/StaticAnalyzer/Checkers/Checkers.td =================================================================== --- include/clang/StaticAnalyzer/Checkers/Checkers.td +++ include/clang/StaticAnalyzer/Checkers/Checkers.td @@ -148,6 +148,10 @@ HelpText<"Loss of sign/precision in implicit conversions">, DescFile<"ConversionChecker.cpp">; +def FloatingPointMathChecker : Checker<"FPMath">, + HelpText<"Check for domain errors in floating-point math functions">, + DescFile<"FloatingPointMath.cpp">; + def IdenticalExprChecker : Checker<"IdenticalExpr">, HelpText<"Warn about unintended use of identical expressions in operators">, DescFile<"IdenticalExprChecker.cpp">; Index: include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h =================================================================== --- include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h +++ include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h @@ -85,11 +85,14 @@ class BasicValueFactory { typedef llvm::FoldingSet > APSIntSetTy; + typedef llvm::FoldingSet > + APFloatSetTy; ASTContext &Ctx; llvm::BumpPtrAllocator& BPAlloc; APSIntSetTy APSIntSet; + APFloatSetTy APFloatSet; void * PersistentSVals; void * PersistentSValPairs; @@ -117,6 +120,9 @@ const llvm::APSInt& getValue(const llvm::APInt& X, bool isUnsigned); const llvm::APSInt& getValue(uint64_t X, QualType T); + const llvm::APFloat &getValue(const llvm::APFloat& X); + const llvm::APFloat &getValue(int64_t X, const llvm::fltSemantics &S); + /// Returns the type of the APSInt used to store values of the given QualType. APSIntType getAPSIntType(QualType T) const { assert(T->isIntegralOrEnumerationType() || Loc::isLocType(T)); @@ -143,6 +149,49 @@ return getValue(TargetType.convert(From)); } + const llvm::APFloat &Convert(const llvm::APSInt &From, + const llvm::fltSemantics &S) { + llvm::APFloat To(S, llvm::APFloat::uninitialized); + assert(Convert(To, From) && "Failed to convert integer to floating-point!"); + return getValue(To); + } + + const llvm::APFloat &Convert(QualType T, const llvm::APFloat &From) { + bool lossOfPrecision; + llvm::APFloat To = From; + llvm::APFloat::opStatus Status = To.convert(Ctx.getFloatTypeSemantics(T), + llvm::APFloat::rmNearestTiesToEven, &lossOfPrecision); + assert(!(Status & (llvm::APFloat::opOverflow | llvm::APFloat::opInvalidOp))); + return getValue(To); + } + + /// Fills an existing APFloat with the floating-point representation of an + /// APSInt. Returns true if the conversion is successful. + static bool Convert(llvm::APFloat &Float, const llvm::APSInt &Int) { + llvm::APFloat::opStatus Status = Float.convertFromAPInt( + Int, Int.isSigned(), llvm::APFloat::rmNearestTiesToEven); + // Cannot be represented in destination type, this is undefined behavior + if (llvm::APFloat::opOverflow & Status || + llvm::APFloat::opInvalidOp & Status) + return false; + + return true; + } + + /// Fills an existing APSInt with the integer representation of an + /// APFloat. Returns true if the conversion is successful. + static bool Convert(llvm::APSInt &Int, const llvm::APFloat &Float) { + bool isExact; + llvm::APFloat::opStatus Status = Float.convertToInteger( + Int, llvm::APFloat::rmNearestTiesToEven, &isExact); + // Cannot be represented in destination type, this is undefined behavior + if (llvm::APFloat::opOverflow & Status || + llvm::APFloat::opInvalidOp & Status) + return false; + + return true; + } + const llvm::APSInt& getIntValue(uint64_t X, bool isUnsigned) { QualType T = isUnsigned ? Ctx.UnsignedIntTy : Ctx.IntTy; return getValue(X, T); @@ -225,8 +274,16 @@ const nonloc::PointerToMember &PTM); const llvm::APSInt* evalAPSInt(BinaryOperator::Opcode Op, - const llvm::APSInt& V1, - const llvm::APSInt& V2); + const llvm::APSInt& V1, + const llvm::APSInt& V2); + + const llvm::APFloat* evalAPFloat(BinaryOperator::Opcode Op, + const llvm::APFloat& V1, + const llvm::APFloat& V2); + + const llvm::APSInt* evalAPFloatComparison(BinaryOperator::Opcode Op, + const llvm::APFloat& V1, + const llvm::APFloat& V2); const std::pair& getPersistentSValWithData(const SVal& V, uintptr_t Data); Index: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h =================================================================== --- include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h +++ include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h @@ -139,6 +139,16 @@ return nullptr; } + /// \brief If a symbol is perfectly constrained to a constant, attempt + /// to return the concrete value. + /// + /// Note that a ConstraintManager is not obligated to return a concretized + /// value for a symbol, even if it is perfectly constrained. + virtual const llvm::APFloat* getSymFloatVal(ProgramStateRef state, + SymbolRef sym) const { + return nullptr; + } + /// Scan all symbols referenced by the constraints. If the symbol is not /// alive, remove it. virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, Index: include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h =================================================================== --- include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h +++ include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h @@ -109,10 +109,14 @@ virtual SVal evalBinOpLN(ProgramStateRef state, BinaryOperator::Opcode op, Loc lhs, NonLoc rhs, QualType resultTy) = 0; - /// Evaluates a given SVal. If the SVal has only one possible (integer) value, + /// Evaluates a given SVal. If the SVal has only one possible integer value, /// that value is returned. Otherwise, returns NULL. virtual const llvm::APSInt *getKnownValue(ProgramStateRef state, SVal val) = 0; - + + /// Evaluates a given SVal. If the SVal has only one possible float value, + /// that value is returned. Otherwise, returns NULL. + virtual const llvm::APFloat *getKnownFloatValue(ProgramStateRef state, SVal val) = 0; + /// Constructs a symbolic expression for two non-location values. SVal makeSymExprValNN(ProgramStateRef state, BinaryOperator::Opcode op, NonLoc lhs, NonLoc rhs, QualType resultTy); @@ -290,6 +294,20 @@ return nonloc::LocAsInteger(BasicVals.getPersistentSValWithData(loc, bits)); } + nonloc::ConcreteFloat makeFloatVal(const FloatingLiteral *F) { + return nonloc::ConcreteFloat(BasicVals.getValue(F->getValue())); + } + + nonloc::ConcreteFloat makeFloatVal(const llvm::APFloat &F) { + return nonloc::ConcreteFloat(BasicVals.getValue(F)); + } + + DefinedSVal makeFloatVal(uint64_t V, QualType T) { + assert(!Loc::isLocType(T)); + return nonloc::ConcreteFloat(BasicVals.getValue(V, + Context.getFloatTypeSemantics(T))); + } + NonLoc makeNonLoc(const SymExpr *lhs, BinaryOperator::Opcode op, const llvm::APSInt& rhs, QualType type); @@ -297,6 +315,12 @@ const SymExpr *lhs, QualType type); NonLoc makeNonLoc(const SymExpr *lhs, BinaryOperator::Opcode op, + const llvm::APFloat& rhs, QualType type); + + NonLoc makeNonLoc(const llvm::APFloat& lhs, BinaryOperator::Opcode op, + const SymExpr *rhs, QualType type); + + NonLoc makeNonLoc(const SymExpr *lhs, BinaryOperator::Opcode op, const SymExpr *rhs, QualType type); /// \brief Create a NonLoc value for cast. Index: include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h =================================================================== --- include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h +++ include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h @@ -131,10 +131,14 @@ return getRawKind() > UnknownValKind; } + bool isFloat() const; + bool isConstant() const; bool isConstant(int I) const; + bool isConstant(llvm::APFloat &V) const; + bool isZeroConstant() const; /// hasConjuredSymbol - If this SVal wraps a conjured symbol, return true; @@ -183,7 +187,7 @@ return SymExpr::symbol_iterator(); } - SymExpr::symbol_iterator symbol_end() const { + SymExpr::symbol_iterator symbol_end() const { return SymExpr::symbol_end(); } }; @@ -206,26 +210,26 @@ // tautologically false. bool isUndef() const = delete; bool isValid() const = delete; - + protected: DefinedOrUnknownSVal() {} explicit DefinedOrUnknownSVal(const void *d, bool isLoc, unsigned ValKind) : SVal(d, isLoc, ValKind) {} - + explicit DefinedOrUnknownSVal(BaseKind k, void *D = nullptr) : SVal(k, D) {} - + private: friend class SVal; static bool isKind(const SVal& V) { return !V.isUndef(); } }; - + class UnknownVal : public DefinedOrUnknownSVal { public: explicit UnknownVal() : DefinedOrUnknownSVal(UnknownValKind) {} - + private: friend class SVal; static bool isKind(const SVal &V) { @@ -290,7 +294,7 @@ void dumpToStream(raw_ostream &Out) const; static inline bool isLocType(QualType T) { - return T->isAnyPointerType() || T->isBlockPointerType() || + return T->isAnyPointerType() || T->isBlockPointerType() || T->isReferenceType() || T->isNullPtrType(); } @@ -368,6 +372,34 @@ } }; +/// \brief Value representing floating-point constant. +class ConcreteFloat : public NonLoc { +public: + explicit ConcreteFloat(const llvm::APFloat& V) : NonLoc(ConcreteFloatKind, &V) {} + + const llvm::APFloat& getValue() const { + return *static_cast(Data); + } + + // Transfer functions for binary/unary operations on ConcreteFloats. + SVal evalBinOp(SValBuilder &svalBuilder, BinaryOperator::Opcode Op, + const ConcreteFloat& R) const; + + ConcreteFloat evalMinus(SValBuilder &svalBuilder) const; + +private: + friend class SVal; + ConcreteFloat() {} + static bool isKind(const SVal& V) { + return V.getBaseKind() == NonLocKind && + V.getSubKind() == ConcreteFloatKind; + } + + static bool isKind(const NonLoc& V) { + return V.getSubKind() == ConcreteFloatKind; + } +}; + class LocAsInteger : public NonLoc { friend class ento::SValBuilder; Index: include/clang/StaticAnalyzer/Core/PathSensitive/SVals.def =================================================================== --- include/clang/StaticAnalyzer/Core/PathSensitive/SVals.def +++ include/clang/StaticAnalyzer/Core/PathSensitive/SVals.def @@ -63,6 +63,7 @@ ABSTRACT_SVAL_WITH_KIND(NonLoc, DefinedSVal) NONLOC_SVAL(CompoundVal, NonLoc) NONLOC_SVAL(ConcreteInt, NonLoc) + NONLOC_SVAL(ConcreteFloat, NonLoc) NONLOC_SVAL(LazyCompoundVal, NonLoc) NONLOC_SVAL(LocAsInteger, NonLoc) NONLOC_SVAL(SymbolVal, NonLoc) Index: include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h =================================================================== --- include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h +++ include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h @@ -356,6 +356,77 @@ } }; + +/// \brief Represents a symbolic expression like 'x' + 3.0. +class SymFloatExpr : public BinarySymExpr { + const SymExpr *LHS; + const llvm::APFloat& RHS; + +public: + SymFloatExpr(const SymExpr *lhs, BinaryOperator::Opcode op, + const llvm::APFloat& rhs, QualType t) + : BinarySymExpr(SymFloatExprKind, op, t), LHS(lhs), RHS(rhs) {} + + void dumpToStream(raw_ostream &os) const override; + + const SymExpr *getLHS() const { return LHS; } + const llvm::APFloat &getRHS() const { return RHS; } + + static void Profile(llvm::FoldingSetNodeID& ID, const SymExpr *lhs, + BinaryOperator::Opcode op, const llvm::APFloat& rhs, + QualType t) { + ID.AddInteger((unsigned) SymFloatExprKind); + ID.AddPointer(lhs); + ID.AddInteger(op); + ID.AddPointer(&rhs); + ID.Add(t); + } + + void Profile(llvm::FoldingSetNodeID& ID) override { + Profile(ID, LHS, getOpcode(), RHS, getType()); + } + + // Implement isa support. + static inline bool classof(const SymExpr *SE) { + return SE->getKind() == SymFloatExprKind; + } +}; + +/// \brief Represents a symbolic expression like 3.0 - 'x'. +class FloatSymExpr : public BinarySymExpr { + const llvm::APFloat& LHS; + const SymExpr *RHS; + +public: + FloatSymExpr(const llvm::APFloat& lhs, BinaryOperator::Opcode op, + const SymExpr *rhs, QualType t) + : BinarySymExpr(FloatSymExprKind, op, t), LHS(lhs), RHS(rhs) {} + + void dumpToStream(raw_ostream &os) const override; + + const SymExpr *getRHS() const { return RHS; } + const llvm::APFloat &getLHS() const { return LHS; } + + static void Profile(llvm::FoldingSetNodeID& ID, const llvm::APFloat& lhs, + BinaryOperator::Opcode op, const SymExpr *rhs, + QualType t) { + ID.AddInteger((unsigned) FloatSymExprKind); + ID.AddPointer(&lhs); + ID.AddInteger(op); + ID.AddPointer(rhs); + ID.Add(t); + } + + void Profile(llvm::FoldingSetNodeID& ID) override { + Profile(ID, LHS, getOpcode(), RHS, getType()); + } + + // Implement isa support. + static inline bool classof(const SymExpr *SE) { + return SE->getKind() == FloatSymExprKind; + } +}; + /// \brief Represents a symbolic expression like 'x' + 'y'. class SymSymExpr : public BinarySymExpr { const SymExpr *LHS; @@ -459,6 +530,20 @@ BinaryOperator::Opcode op, const SymExpr *rhs, QualType t); + const SymFloatExpr *getSymFloatExpr(const SymExpr *lhs, + BinaryOperator::Opcode op, + const llvm::APFloat& rhs, QualType t); + + const SymFloatExpr *getSymFloatExpr(const SymExpr &lhs, + BinaryOperator::Opcode op, + const llvm::APFloat& rhs, QualType t) { + return getSymFloatExpr(&lhs, op, rhs, t); + } + + const FloatSymExpr *getFloatSymExpr(const llvm::APFloat& lhs, + BinaryOperator::Opcode op, + const SymExpr *rhs, QualType t); + const SymSymExpr *getSymSymExpr(const SymExpr *lhs, BinaryOperator::Opcode op, const SymExpr *rhs, QualType t); Index: include/clang/StaticAnalyzer/Core/PathSensitive/Symbols.def =================================================================== --- include/clang/StaticAnalyzer/Core/PathSensitive/Symbols.def +++ include/clang/StaticAnalyzer/Core/PathSensitive/Symbols.def @@ -37,6 +37,8 @@ ABSTRACT_SYMBOL(BinarySymExpr, SymExpr) SYMBOL(IntSymExpr, BinarySymExpr) SYMBOL(SymIntExpr, BinarySymExpr) + SYMBOL(FloatSymExpr, BinarySymExpr) + SYMBOL(SymFloatExpr, BinarySymExpr) SYMBOL(SymSymExpr, BinarySymExpr) SYMBOL_RANGE(BINARYSYMEXPRS, IntSymExprKind, SymSymExprKind) Index: lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp =================================================================== --- lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp +++ lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp @@ -41,6 +41,80 @@ default: return false; + case Builtin::BI__builtin_inf: + case Builtin::BI__builtin_inff: + case Builtin::BI__builtin_infl: { + SValBuilder &SVB = C.getSValBuilder(); + ASTContext &Ctx = SVB.getContext(); + llvm::APFloat Inf = llvm::APFloat::getInf( + Ctx.getFloatTypeSemantics(FD->getReturnType())); + SVal V = SVB.makeFloatVal(Inf); + C.addTransition(state->BindExpr(CE, LCtx, V)); + return true; + } + + // TODO: Model the string argument as well + case Builtin::BI__builtin_nan: + case Builtin::BI__builtin_nanf: + case Builtin::BI__builtin_nanl: { + SValBuilder &SVB = C.getSValBuilder(); + ASTContext &Ctx = SVB.getContext(); + llvm::APFloat NaN = llvm::APFloat::getQNaN( + Ctx.getFloatTypeSemantics(FD->getReturnType())); + SVal V = SVB.makeFloatVal(NaN); + C.addTransition(state->BindExpr(CE, LCtx, V)); + return true; + } + + case Builtin::BI__builtin_isinf: { + SValBuilder &SVB = C.getSValBuilder(); + ASTContext &Ctx = SVB.getContext(); + assert(CE->arg_begin() + 1 == CE->arg_end()); + DefinedOrUnknownSVal V = + state->getSVal(*(CE->arg_begin()), LCtx).castAs(); + + llvm::APFloat PInf = llvm::APFloat::getInf( + Ctx.getFloatTypeSemantics((*(CE->arg_begin()))->getType()), false); + DefinedOrUnknownSVal SPInf = SVB.makeFloatVal(PInf); + DefinedOrUnknownSVal isPInf = SVB.evalEQ(state, V, SPInf); + if (isPInf.isConstant(1)) { + C.addTransition(state->BindExpr(CE, LCtx, isPInf)); + return true; + } + + llvm::APFloat NInf = llvm::APFloat::getInf( + Ctx.getFloatTypeSemantics((*(CE->arg_begin()))->getType()), true); + DefinedOrUnknownSVal SNInf = SVB.makeFloatVal(NInf); + DefinedOrUnknownSVal isNInf = SVB.evalEQ(state, V, SNInf); + if (isPInf.isZeroConstant() && isNInf.isConstant(1)) { + C.addTransition(state->BindExpr(CE, LCtx, isNInf)); + return true; + } + + // TODO: FIXME + // This should be BO_LOr for (V == -\inf) || (V == \inf), but logical + // operations are handled much earlier during ExplodedGraph generation. + // However, since both sides are Boolean/Int1Ty, we can use bitwise or. + // If/when this is fixed, also remove the explicit short-circuits above. + SVal isInf = SVB.evalBinOp(state, BO_Or, isPInf, isNInf, + SVB.getConditionType()); + C.addTransition(state->BindExpr(CE, LCtx, isInf)); + return true; + } + + // TODO: FIXME + // IEEE-754 changes evaluation of direct comparison to NaN, which makes it + // difficult to express NaN constraints for the symbolic executor. + // As a workaround, express this as V != V, for which only NaN satisfies. + case Builtin::BI__builtin_isnan: { + SValBuilder &SVB = C.getSValBuilder(); + assert(CE->arg_begin() + 1 == CE->arg_end()); + SVal V = state->getSVal(*(CE->arg_begin()), LCtx); + SVal isNaN = SVB.evalBinOp(state, BO_NE, V, V, SVB.getConditionType()); + C.addTransition(state->BindExpr(CE, LCtx, isNaN)); + return true; + } + case Builtin::BI__builtin_unpredictable: case Builtin::BI__builtin_expect: case Builtin::BI__builtin_assume_aligned: Index: lib/StaticAnalyzer/Checkers/CMakeLists.txt =================================================================== --- lib/StaticAnalyzer/Checkers/CMakeLists.txt +++ lib/StaticAnalyzer/Checkers/CMakeLists.txt @@ -36,6 +36,7 @@ DynamicTypeChecker.cpp ExprInspectionChecker.cpp FixedAddressChecker.cpp + FloatingPointMath.cpp GenericTaintChecker.cpp GTestChecker.cpp IdenticalExprChecker.cpp Index: lib/StaticAnalyzer/Checkers/FloatingPointMath.cpp =================================================================== --- /dev/null +++ lib/StaticAnalyzer/Checkers/FloatingPointMath.cpp @@ -0,0 +1,326 @@ +//=== FloatingPointMathChecker.cpp --------------------------------*- C++ +//-*-===// +// +// The LLVM Compiler Infrastructure +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +// +// This checker evaluates calls to floating-point math functions for domain +// errors. +// +//===----------------------------------------------------------------------===// + +#include "ClangSACheckers.h" +#include "clang/Basic/Builtins.h" +#include "clang/StaticAnalyzer/Core/BugReporter/BugType.h" +#include "clang/StaticAnalyzer/Core/Checker.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h" + +using namespace clang; +using namespace ento; + +namespace { +class FloatingPointMathChecker : public Checker { + mutable std::unique_ptr BT; + + void reportError(ProgramStateRef State, CheckerContext &C) const; + + void inline handleAssumption(ProgramStateRef T, ProgramStateRef F, + ProgramStateRef State, CheckerContext &C) const; + +public: + void checkPreCall(const CallEvent &Call, CheckerContext &C) const; +}; + +} // end anonymous namespace + +void FloatingPointMathChecker::reportError(ProgramStateRef State, + CheckerContext &C) const { + if (ExplodedNode *N = C.generateNonFatalErrorNode(State)) { + if (!BT) + BT.reset(new BuiltinBug(this, "Domain/range error")); + C.emitReport(llvm::make_unique( + *BT, "Argument value is out of valid domain for function call", N)); + } +} + +void FloatingPointMathChecker::handleAssumption(ProgramStateRef T, + ProgramStateRef F, + ProgramStateRef State, + CheckerContext &C) const { + if (F) { + reportError(State, C); + + if (!T) + C.addTransition(F); + return; + } + + if (!F && T) + C.addTransition(T); + return; +} + +void FloatingPointMathChecker::checkPreCall(const CallEvent &Call, + CheckerContext &C) const { + ProgramStateRef State = C.getState(); + const Decl *D = Call.getDecl(); + if (!D) + return; + const FunctionDecl *FD = dyn_cast(D); + if (!FD) + return; + + ConstraintManager &CM = C.getConstraintManager(); + SValBuilder &SVB = C.getSValBuilder(); + BasicValueFactory &BVF = SVB.getBasicValueFactory(); + ASTContext &Ctx = SVB.getContext(); + QualType Int32Ty = Ctx.getIntTypeForBitwidth(32, true); + + switch (FD->getBuiltinID()) { + default: + return; + + // acos(x): -1 <= x <= 1 + case Builtin::BIacos: + case Builtin::BIacosf: + case Builtin::BIacosl: + case Builtin::BIasin: + case Builtin::BIasinf: + case Builtin::BIasinl: + case Builtin::BI__builtin_acos: + case Builtin::BI__builtin_acosf: + case Builtin::BI__builtin_acosl: + case Builtin::BI__builtin_asin: + case Builtin::BI__builtin_asinf: + case Builtin::BI__builtin_asinl: { + assert(Call.getNumArgs() == 1); + SVal V = Call.getArgSVal(0); + llvm::APSInt From = BVF.getValue(-1, Int32Ty); + llvm::APSInt To = BVF.getValue(1, Int32Ty); + + // Skip if known to be NaN, otherwise assume to be not NaN + SVal notNaN = SVB.evalBinOp(State, BO_EQ, V, V, SVB.getConditionType()); + if (notNaN.isUnknown() || notNaN.isZeroConstant()) { + return; + } + + ProgramStateRef StIR, StOR; + // This relies on the constraint manager promoting from APSInt to APFloat + // because the type of V is floating-point. + std::tie(StIR, StOR) = + CM.assumeInclusiveRangeDual(State, V.castAs(), From, To); + return handleAssumption(StIR, StOR, State, C); + } + + // acosh(x): x >= 1 + case Builtin::BIacosh: + case Builtin::BIacoshf: + case Builtin::BIacoshl: + case Builtin::BI__builtin_acosh: + case Builtin::BI__builtin_acoshf: + case Builtin::BI__builtin_acoshl: { + assert(Call.getNumArgs() == 1); + SVal V = Call.getArgSVal(0); + llvm::APFloat From = BVF.getValue( + 1, Ctx.getFloatTypeSemantics(Call.getArgExpr(0)->getType())); + DefinedOrUnknownSVal SV = SVB.makeFloatVal(From); + + SVal notNaN = SVB.evalBinOp(State, BO_EQ, V, V, SVB.getConditionType()); + if (notNaN.isUnknown() || notNaN.isZeroConstant()) { + return; + } + + SVal isGE = SVB.evalBinOp(State, BO_GE, V, SV, SVB.getConditionType()); + ProgramStateRef StT, StF; + std::tie(StT, StF) = CM.assumeDual(State, isGE.castAs()); + return handleAssumption(StT, StF, State, C); + } + + // atanh(x): -1 < x < 1 + case Builtin::BIatanh: + case Builtin::BIatanhf: + case Builtin::BIatanhl: + case Builtin::BI__builtin_atanh: + case Builtin::BI__builtin_atanhf: + case Builtin::BI__builtin_atanhl: { + assert(Call.getNumArgs() == 1); + SVal V = Call.getArgSVal(0); + llvm::APFloat From = BVF.getValue( + -1, Ctx.getFloatTypeSemantics(Call.getArgExpr(0)->getType())); + llvm::APFloat To = BVF.getValue( + 1, Ctx.getFloatTypeSemantics(Call.getArgExpr(0)->getType())); + + SVal notNaN = SVB.evalBinOp(State, BO_EQ, V, V, SVB.getConditionType()); + if (notNaN.isUnknown() || notNaN.isZeroConstant()) { + return; + } + + DefinedOrUnknownSVal SFrom = SVB.makeFloatVal(From); + SVal isGT = SVB.evalBinOp(State, BO_GT, V, SFrom, SVB.getConditionType()); + if (isGT.isZeroConstant()) + return reportError(State, C); + + DefinedOrUnknownSVal STo = SVB.makeFloatVal(To); + SVal isLT = SVB.evalBinOp(State, BO_LT, V, STo, SVB.getConditionType()); + if (isGT.isConstant(1) && isLT.isZeroConstant()) + return reportError(State, C); + + // TODO: FIXME + // This should be BO_LAnd, but logical operations are handled much earlier + // during ExplodedGraph generation. However, since both sides are + // Boolean/Int1Ty, we can use bitwise and. + // If/when this is fixed, also remove the explicit short-circuits above. + SVal isIR = + SVB.evalBinOp(State, BO_And, isGT, isLT, SVB.getConditionType()); + ProgramStateRef StIR, StOR; + std::tie(StIR, StOR) = CM.assumeDual(State, isIR.castAs()); + return handleAssumption(StIR, StOR, State, C); + } + + // log(x): x >= 0 + case Builtin::BIlog: + case Builtin::BIlogf: + case Builtin::BIlogl: + case Builtin::BIlog2: + case Builtin::BIlog2f: + case Builtin::BIlog2l: + case Builtin::BIlog10: + case Builtin::BIlog10f: + case Builtin::BIlog10l: + case Builtin::BIsqrt: + case Builtin::BIsqrtf: + case Builtin::BIsqrtl: + case Builtin::BI__builtin_log: + case Builtin::BI__builtin_logf: + case Builtin::BI__builtin_logl: + case Builtin::BI__builtin_log2: + case Builtin::BI__builtin_log2f: + case Builtin::BI__builtin_log2l: + case Builtin::BI__builtin_log10: + case Builtin::BI__builtin_log10f: + case Builtin::BI__builtin_log10l: + case Builtin::BI__builtin_sqrt: + case Builtin::BI__builtin_sqrtf: + case Builtin::BI__builtin_sqrtl: { + assert(Call.getNumArgs() == 1); + SVal V = Call.getArgSVal(0); + llvm::APFloat From = BVF.getValue( + 0, Ctx.getFloatTypeSemantics(Call.getArgExpr(0)->getType())); + DefinedOrUnknownSVal SV = SVB.makeFloatVal(From); + + SVal notNaN = SVB.evalBinOp(State, BO_EQ, V, V, SVB.getConditionType()); + if (notNaN.isUnknown() || notNaN.isZeroConstant()) { + return; + } + + SVal isGE = SVB.evalBinOp(State, BO_GE, V, SV, SVB.getConditionType()); + ProgramStateRef StT, StF; + std::tie(StT, StF) = CM.assumeDual(State, isGE.castAs()); + return handleAssumption(StT, StF, State, C); + } + + // log1p(x): x >= -1 + case Builtin::BIlog1p: + case Builtin::BIlog1pf: + case Builtin::BIlog1pl: + case Builtin::BI__builtin_log1p: + case Builtin::BI__builtin_log1pf: + case Builtin::BI__builtin_log1pl: { + assert(Call.getNumArgs() == 1); + SVal V = Call.getArgSVal(0); + llvm::APFloat From = BVF.getValue( + -1, Ctx.getFloatTypeSemantics(Call.getArgExpr(0)->getType())); + DefinedOrUnknownSVal SV = SVB.makeFloatVal(From); + + SVal notNaN = SVB.evalBinOp(State, BO_EQ, V, V, SVB.getConditionType()); + if (notNaN.isUnknown() || notNaN.isZeroConstant()) { + return; + } + + SVal isGE = SVB.evalBinOp(State, BO_GE, V, SV, SVB.getConditionType()); + ProgramStateRef StT, StF; + std::tie(StT, StF) = CM.assumeDual(State, isGE.castAs()); + return handleAssumption(StT, StF, State, C); + } + + // logb(x): x != 0 + case Builtin::BIlogb: + case Builtin::BIlogbf: + case Builtin::BIlogbl: + case Builtin::BI__builtin_logb: + case Builtin::BI__builtin_logbf: + case Builtin::BI__builtin_logbl: { + assert(Call.getNumArgs() == 1); + SVal V = Call.getArgSVal(0); + llvm::APFloat From = BVF.getValue( + 0, Ctx.getFloatTypeSemantics(Call.getArgExpr(0)->getType())); + DefinedOrUnknownSVal SV = SVB.makeFloatVal(From); + + SVal isNE = SVB.evalBinOp(State, BO_NE, V, SV, SVB.getConditionType()); + ProgramStateRef StT, StF; + std::tie(StT, StF) = CM.assumeDual(State, isNE.castAs()); + return handleAssumption(StT, StF, State, C); + } + + // TODO: + // pow(x, y) : x > 0 || (x == 0 && y > 0) || (x < 0 && (int) y) + // case Builtin::BIpow: + // case Builtin::BIpowf: + // case Builtin::BIpowl: + // case Builtin::BI__builtin_pow: + // case Builtin::BI__builtin_powf: + // case Builtin::BI__builtin_powl: + + // TODO: + // lgamma(x) : x != 0 && !(x < 0 && (int) x) + // case Builtin::BIlgamma: + // case Builtin::BIlgammaf: + // case Builtin::BIlgammal: + // case Builtin::BItgamma: + // case Builtin::BItgammaf: + // case Builtin::BItgammal: + // case Builtin::BI__builtin_lgamma: + // case Builtin::BI__builtin_lgammaf: + // case Builtin::BI__builtin_lgammal: + // case Builtin::BI__builtin_tgamma: + // case Builtin::BI__builtin_tgammaf: + // case Builtin::BI__builtin_tgammal: + + // fmod(x,y) : y != 0 + case Builtin::BIfmod: + case Builtin::BIfmodf: + case Builtin::BIfmodl: + case Builtin::BIremainder: + case Builtin::BIremainderf: + case Builtin::BIremainderl: + case Builtin::BI__builtin_fmod: + case Builtin::BI__builtin_fmodf: + case Builtin::BI__builtin_fmodl: + case Builtin::BI__builtin_remainder: + case Builtin::BI__builtin_remainderf: + case Builtin::BI__builtin_remainderl: + case Builtin::BI__builtin_remquo: + case Builtin::BI__builtin_remquof: + case Builtin::BI__builtin_remquol: { + assert(Call.getNumArgs() >= 2); + SVal V = Call.getArgSVal(1); + llvm::APFloat From = BVF.getValue( + 0, Ctx.getFloatTypeSemantics(Call.getArgExpr(1)->getType())); + DefinedOrUnknownSVal SV = SVB.makeFloatVal(From); + + SVal isNE = SVB.evalBinOp(State, BO_NE, V, SV, SVB.getConditionType()); + ProgramStateRef StT, StF; + std::tie(StT, StF) = CM.assumeDual(State, isNE.castAs()); + return handleAssumption(StT, StF, State, C); + } + } +} + +void ento::registerFloatingPointMathChecker(CheckerManager &mgr) { + mgr.registerChecker(); +} Index: lib/StaticAnalyzer/Core/BasicValueFactory.cpp =================================================================== --- lib/StaticAnalyzer/Core/BasicValueFactory.cpp +++ lib/StaticAnalyzer/Core/BasicValueFactory.cpp @@ -72,6 +72,9 @@ for (APSIntSetTy::iterator I=APSIntSet.begin(), E=APSIntSet.end(); I!=E; ++I) I->getValue().~APSInt(); + for (APFloatSetTy::iterator I=APFloatSet.begin(), E=APFloatSet.end(); I!=E; ++I) + I->getValue().~APFloat(); + delete (PersistentSValsTy*) PersistentSVals; delete (PersistentSValPairsTy*) PersistentSValPairs; } @@ -111,6 +114,28 @@ return getValue(getAPSIntType(T).getValue(X)); } +const llvm::APFloat &BasicValueFactory::getValue(const llvm::APFloat& X) { + llvm::FoldingSetNodeID ID; + void *InsertPos; + typedef llvm::FoldingSetNodeWrapper FoldNodeTy; + + X.Profile(ID); + FoldNodeTy* P = APFloatSet.FindNodeOrInsertPos(ID, InsertPos); + + if (!P) { + P = (FoldNodeTy*) BPAlloc.Allocate(); + new (P) FoldNodeTy(X); + APFloatSet.InsertNode(P, InsertPos); + } + + return *P; +} + +const llvm::APFloat &BasicValueFactory::getValue(int64_t X, + const llvm::fltSemantics &S) { + return Convert(llvm::APSInt::get(X), S); +} + const CompoundValData* BasicValueFactory::getCompoundValData(QualType T, llvm::ImmutableList Vals) { @@ -286,6 +311,90 @@ } } +const llvm::APFloat* +BasicValueFactory::evalAPFloat(BinaryOperator::Opcode Op, + const llvm::APFloat& V1, const llvm::APFloat& V2) { + llvm::APFloat NewV = V1; + llvm::APFloat::opStatus Status = llvm::APFloat::opOK; + + switch (Op) { + default: + assert (false && "Invalid Opcode."); + + case BO_Mul: + Status = NewV.multiply(V2, llvm::APFloat::rmNearestTiesToEven); + if (Status & llvm::APFloat::opOK) + return &getValue(NewV); + break; + + case BO_Div: + // Divide by zero + if (V1.isFinite() && V2.isInfinity()) + NewV = llvm::APFloat::getZero(V1.getSemantics()); + else + Status = NewV.divide(V2, llvm::APFloat::rmNearestTiesToEven); + if (Status & llvm::APFloat::opOK) + return &getValue(NewV); + break; + + case BO_Rem: + Status = NewV.remainder(V2); + if (Status & llvm::APFloat::opOK) + return &getValue(NewV); + break; + + case BO_Add: + Status = NewV.add(V2, llvm::APFloat::rmNearestTiesToEven); + if (Status & llvm::APFloat::opOK) + return &getValue(NewV); + break; + + case BO_Sub: + Status = NewV.subtract(V2, llvm::APFloat::rmNearestTiesToEven); + if (Status & llvm::APFloat::opOK) + return &getValue(NewV); + break; + } + + // TODO: Fix sign of special results + if (Status & llvm::APFloat::opOverflow) + return &getValue(llvm::APFloat::getInf(NewV.getSemantics())); + else if (Status & llvm::APFloat::opDivByZero) + return &getValue(llvm::APFloat::getInf(NewV.getSemantics())); + else if (Status & llvm::APFloat::opInvalidOp) + return &getValue(llvm::APFloat::getSNaN(NewV.getSemantics())); + return &getValue(NewV); +} + +const llvm::APSInt* +BasicValueFactory::evalAPFloatComparison(BinaryOperator::Opcode Op, + const llvm::APFloat& V1, const llvm::APFloat& V2) { + llvm::APFloat::cmpResult R = V1.compare(V2); + switch (Op) { + default: + assert (false && "Invalid Opcode."); + + case BO_LT: + return &getTruthValue(R == llvm::APFloat::cmpLessThan); + + case BO_GT: + return &getTruthValue(R == llvm::APFloat::cmpGreaterThan); + + case BO_LE: + return &getTruthValue(R == llvm::APFloat::cmpLessThan || + R == llvm::APFloat::cmpEqual); + + case BO_GE: + return &getTruthValue(R == llvm::APFloat::cmpGreaterThan || + R == llvm::APFloat::cmpEqual); + + case BO_EQ: + return &getTruthValue(R == llvm::APFloat::cmpEqual); + + case BO_NE: + return &getTruthValue(R != llvm::APFloat::cmpEqual); + } +} const std::pair& BasicValueFactory::getPersistentSValWithData(const SVal& V, uintptr_t Data) { Index: lib/StaticAnalyzer/Core/Environment.cpp =================================================================== --- lib/StaticAnalyzer/Core/Environment.cpp +++ lib/StaticAnalyzer/Core/Environment.cpp @@ -86,6 +86,7 @@ case Stmt::CXXScalarValueInitExprClass: case Stmt::ImplicitValueInitExprClass: case Stmt::IntegerLiteralClass: + case Stmt::FloatingLiteralClass: case Stmt::ObjCBoolLiteralExprClass: case Stmt::CXXNullPtrLiteralExprClass: case Stmt::ObjCStringLiteralClass: Index: lib/StaticAnalyzer/Core/ProgramState.cpp =================================================================== --- lib/StaticAnalyzer/Core/ProgramState.cpp +++ lib/StaticAnalyzer/Core/ProgramState.cpp @@ -262,29 +262,39 @@ // about). if (!T.isNull()) { if (SymbolRef sym = V.getAsSymbol()) { - if (const llvm::APSInt *Int = getStateManager() - .getConstraintManager() - .getSymVal(this, sym)) { - // FIXME: Because we don't correctly model (yet) sign-extension - // and truncation of symbolic values, we need to convert - // the integer value to the correct signedness and bitwidth. - // - // This shows up in the following: - // - // char foo(); - // unsigned x = foo(); - // if (x == 54) - // ... - // - // The symbolic value stored to 'x' is actually the conjured - // symbol for the call to foo(); the type of that symbol is 'char', - // not unsigned. - const llvm::APSInt &NewV = getBasicVals().Convert(T, *Int); - - if (V.getAs()) - return loc::ConcreteInt(NewV); - else - return nonloc::ConcreteInt(NewV); + ConstraintManager &CM = getStateManager().getConstraintManager(); + + if (sym->getType()->isRealFloatingType()) { + if (const llvm::APFloat *Float = CM.getSymFloatVal(this, sym)) { + // FIXME: Because we don't correctly model (yet) sign-extension + // and truncation of symbolic values, we need to convert + // the integer value to the correct signedness and bitwidth. + // + // This shows up in the following: + // + // char foo(); + // unsigned x = foo(); + // if (x == 54) + // ... + // + // The symbolic value stored to 'x' is actually the conjured + // symbol for the call to foo(); the type of that symbol is 'char', + // not unsigned. + const llvm::APFloat &NewV = getBasicVals().Convert(T, *Float); + + assert(!V.getAs() && "Loc::ConcreteFloat not supported!"); + return nonloc::ConcreteFloat(NewV); + } + } else { + if (const llvm::APSInt *Int = CM.getSymVal(this, sym)) { + // FIXME: Likewise + const llvm::APSInt &NewV = getBasicVals().Convert(T, *Int); + + if (V.getAs()) + return loc::ConcreteInt(NewV); + else + return nonloc::ConcreteInt(NewV); + } } } } Index: lib/StaticAnalyzer/Core/RegionStore.cpp =================================================================== --- lib/StaticAnalyzer/Core/RegionStore.cpp +++ lib/StaticAnalyzer/Core/RegionStore.cpp @@ -2027,7 +2027,7 @@ if (Loc::isLocType(T)) V = svalBuilder.makeNull(); - else if (T->isIntegralOrEnumerationType()) + else if (T->isIntegralOrEnumerationType() || T->isRealFloatingType()) V = svalBuilder.makeZeroVal(T); else if (T->isStructureOrClassType() || T->isArrayType()) { // Set the default value to a zero constant when it is a structure Index: lib/StaticAnalyzer/Core/SValBuilder.cpp =================================================================== --- lib/StaticAnalyzer/Core/SValBuilder.cpp +++ lib/StaticAnalyzer/Core/SValBuilder.cpp @@ -40,12 +40,15 @@ type->isAnyComplexType()) return makeCompoundVal(type, BasicVals.getEmptySValList()); - // FIXME: Handle floats. + if (type->isRealFloatingType()) + return makeFloatVal(0, type); + + // FIXME: Handle structs. return UnknownVal(); } NonLoc SValBuilder::makeNonLoc(const SymExpr *lhs, BinaryOperator::Opcode op, - const llvm::APSInt& rhs, QualType type) { + const llvm::APSInt& rhs, QualType type) { // The Environment ensures we always get a persistent APSInt in // BasicValueFactory, so we don't need to get the APSInt from // BasicValueFactory again. @@ -63,6 +66,24 @@ } NonLoc SValBuilder::makeNonLoc(const SymExpr *lhs, BinaryOperator::Opcode op, + const llvm::APFloat& rhs, QualType type) { + // The Environment ensures we always get a persistent APSInt in + // BasicValueFactory, so we don't need to get the APSInt from + // BasicValueFactory again. + assert(lhs); + assert(!Loc::isLocType(type)); + return nonloc::SymbolVal(SymMgr.getSymFloatExpr(lhs, op, rhs, type)); +} + +NonLoc SValBuilder::makeNonLoc(const llvm::APFloat& lhs, + BinaryOperator::Opcode op, const SymExpr *rhs, + QualType type) { + assert(rhs); + assert(!Loc::isLocType(type)); + return nonloc::SymbolVal(SymMgr.getFloatSymExpr(lhs, op, rhs, type)); +} + +NonLoc SValBuilder::makeNonLoc(const SymExpr *lhs, BinaryOperator::Opcode op, const SymExpr *rhs, QualType type) { assert(lhs && rhs); assert(!Loc::isLocType(type)); @@ -304,6 +325,9 @@ case Stmt::IntegerLiteralClass: return makeIntVal(cast(E)); + case Stmt::FloatingLiteralClass: + return makeFloatVal(cast(E)); + case Stmt::ObjCBoolLiteralExprClass: return makeBoolVal(cast(E)); @@ -316,7 +340,8 @@ default: break; case CK_ArrayToPointerDecay: - case CK_BitCast: { + case CK_BitCast: + case CK_IntegralToFloating: { const Expr *SE = CE->getSubExpr(); Optional Val = getConstantVal(SE); if (!Val) @@ -363,13 +388,19 @@ (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp) return makeNonLoc(symLHS, Op, symRHS, ResultTy); - if (symLHS && symLHS->computeComplexity() < MaxComp) + if (symLHS && symLHS->computeComplexity() < MaxComp) { if (Optional rInt = RHS.getAs()) return makeNonLoc(symLHS, Op, rInt->getValue(), ResultTy); + if (Optional rFloat = RHS.getAs()) + return makeNonLoc(symLHS, Op, rFloat->getValue(), ResultTy); + } - if (symRHS && symRHS->computeComplexity() < MaxComp) + if (symRHS && symRHS->computeComplexity() < MaxComp) { if (Optional lInt = LHS.getAs()) return makeNonLoc(lInt->getValue(), Op, symRHS, ResultTy); + if (Optional lFloat = LHS.getAs()) + return makeNonLoc(lFloat->getValue(), Op, symRHS, ResultTy); + } return UnknownVal(); } Index: lib/StaticAnalyzer/Core/SVals.cpp =================================================================== --- lib/StaticAnalyzer/Core/SVals.cpp +++ lib/StaticAnalyzer/Core/SVals.cpp @@ -19,6 +19,7 @@ #include "clang/AST/DeclCXX.h" using namespace clang; using namespace ento; +using llvm::APFloat; using llvm::APSInt; //===----------------------------------------------------------------------===// @@ -204,8 +205,16 @@ // Useful predicates. //===----------------------------------------------------------------------===// +bool SVal::isFloat() const { + if (Optional SV = getAs()) { + return SV->getSymbol()->getType()->isRealFloatingType(); + } + return getAs().hasValue(); +} + bool SVal::isConstant() const { - return getAs() || getAs(); + return getAs() || getAs() || + getAs(); } bool SVal::isConstant(int I) const { @@ -216,7 +225,15 @@ return false; } +bool SVal::isConstant(APFloat &V) const { + if (Optional NF = getAs()) + return NF->getValue().compare(V) == llvm::APFloat::cmpEqual; + return false; +} + bool SVal::isZeroConstant() const { + if (Optional NF = getAs()) + return NF->getValue().isPosZero() || NF->getValue().isNegZero(); return isConstant(0); } @@ -247,6 +264,31 @@ return svalBuilder.makeIntVal(-getValue()); } +nonloc::ConcreteFloat +nonloc::ConcreteFloat::evalMinus(SValBuilder &svalBuilder) const { + llvm::APFloat Value = getValue(); + Value.changeSign(); + return svalBuilder.makeFloatVal(Value); +} + +SVal nonloc::ConcreteFloat::evalBinOp(SValBuilder &svalBuilder, + BinaryOperator::Opcode Op, + const nonloc::ConcreteFloat& R) const { + if (BinaryOperator::isComparisonOp(Op)) { + const llvm::APSInt *V = svalBuilder.getBasicValueFactory().evalAPFloatComparison( + Op, getValue(), R.getValue()); + if (V) + return nonloc::ConcreteInt(*V); + return UnknownVal(); + } + + const llvm::APFloat *V = svalBuilder.getBasicValueFactory().evalAPFloat( + Op, getValue(), R.getValue()); + if (V) + return nonloc::ConcreteFloat(*V); + return UnknownVal(); +} + //===----------------------------------------------------------------------===// // Transfer function dispatch for Locs. //===----------------------------------------------------------------------===// @@ -300,6 +342,17 @@ << C.getValue().getBitWidth() << 'b'; break; } + case nonloc::ConcreteFloatKind: { + const nonloc::ConcreteFloat& C = castAs(); + SmallString<24> Chars; + + C.getValue().toString(Chars, 0, 0); + os << Chars + << ' ' + << llvm::APFloat::semanticsSizeInBits(C.getValue().getSemantics()) + << 'b'; + break; + } case nonloc::SymbolValKind: { os << castAs().getSymbol(); break; Index: lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp =================================================================== --- lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp +++ lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp @@ -53,9 +53,6 @@ ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef State, NonLoc Cond, bool Assumption) { - - // We cannot reason about SymSymExprs, and can only reason about some - // SymIntExprs. if (!canReasonAbout(Cond)) { // Just add the constraint to the expression without trying to simplify. SymbolRef Sym = Cond.getAsSymExpr(); @@ -74,6 +71,12 @@ return assumeSym(State, Sym, Assumption); } + case nonloc::ConcreteFloatKind: { + bool b = !Cond.castAs().getValue().isZero(); + bool isFeasible = b ? Assumption : !Assumption; + return isFeasible ? State : nullptr; + } + case nonloc::ConcreteIntKind: { bool b = Cond.castAs().getValue() != 0; bool isFeasible = b ? Assumption : !Assumption; @@ -117,7 +120,27 @@ if (SymbolRef Sym = Value.getAsSymbol()) return assumeSymInclusiveRange(State, Sym, From, To, InRange); return State; - } // end switch + } + + case nonloc::ConcreteFloatKind: { + BasicValueFactory &BVF = getBasicVals(); + + const llvm::APFloat &FloatVal = + Value.castAs().getValue(); + llvm::APFloat FromF(FloatVal.getSemantics(), llvm::APFloat::uninitialized); + llvm::APFloat ToF(FloatVal.getSemantics(), llvm::APFloat::uninitialized); + assert(BVF.Convert(FromF, From) && "Integer failed to convert to float!"); + assert(BVF.Convert(ToF, To) && "Integer failed to convert to float!"); + llvm::APFloat::cmpResult CompareFrom = FloatVal.compare(FromF); + llvm::APFloat::cmpResult CompareTo = FloatVal.compare(ToF); + + bool IsInRange = (CompareFrom == llvm::APFloat::cmpGreaterThan || + CompareFrom == llvm::APFloat::cmpEqual) && + (CompareTo == llvm::APFloat::cmpLessThan || + CompareTo == llvm::APFloat::cmpEqual); + bool isFeasible = (IsInRange == InRange); + return isFeasible ? State : nullptr; + } case nonloc::ConcreteIntKind: { const llvm::APSInt &IntVal = Value.castAs().getValue(); Index: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp =================================================================== --- lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp +++ lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp @@ -41,11 +41,18 @@ Loc lhs, NonLoc rhs, QualType resultTy) override; /// getKnownValue - evaluates a given SVal. If the SVal has only one possible - /// (integer) value, that value is returned. Otherwise, returns NULL. + /// integer value, that value is returned. Otherwise, returns NULL. const llvm::APSInt *getKnownValue(ProgramStateRef state, SVal V) override; + /// Evaluates a given SVal. If the SVal has only one possible float value, + /// that value is returned. Otherwise, returns NULL. + const llvm::APFloat *getKnownFloatValue(ProgramStateRef state, SVal val) override; + SVal MakeSymIntVal(const SymExpr *LHS, BinaryOperator::Opcode op, const llvm::APSInt &RHS, QualType resultTy); + + SVal MakeSymFloatVal(const SymExpr *LHS, BinaryOperator::Opcode op, + const llvm::APFloat &RHS, QualType resultTy); }; } // end anonymous namespace @@ -62,7 +69,7 @@ SVal SimpleSValBuilder::dispatchCast(SVal Val, QualType CastTy) { assert(Val.getAs() || Val.getAs()); return Val.getAs() ? evalCastFromLoc(Val.castAs(), CastTy) - : evalCastFromNonLoc(Val.castAs(), CastTy); + : evalCastFromNonLoc(Val.castAs(), CastTy); } SVal SimpleSValBuilder::evalCastFromNonLoc(NonLoc val, QualType castTy) { @@ -100,28 +107,77 @@ return UnknownVal(); } - // If value is a non-integer constant, produce unknown. - if (!val.getAs()) + // If value is an unsupported constant, produce unknown. + if (!val.getAs() && !val.getAs()) return UnknownVal(); // Handle casts to a boolean type. if (castTy->isBooleanType()) { - bool b = val.castAs().getValue().getBoolValue(); - return makeTruthVal(b, castTy); + if (Optional CI = val.getAs()) + return makeTruthVal(CI->getValue().getBoolValue(), castTy); + if (Optional CF = val.getAs()) + return makeTruthVal(!CF->getValue().isZero(), castTy); } - // Only handle casts from integers to integers - if val is an integer constant - // being cast to a non-integer type, produce unknown. - if (!isLocType && !castTy->isIntegralOrEnumerationType()) - return UnknownVal(); + // Handle casts from integer + if (Optional CI = val.getAs()) { + if (castTy->isRealFloatingType()) { + if (isLocType) + return UnknownVal(); - llvm::APSInt i = val.castAs().getValue(); - BasicVals.getAPSIntType(castTy).apply(i); + llvm::APFloat Value(Context.getFloatTypeSemantics(castTy)); + // Cannot be represented in destination type, this is undefined behavior + if (!BasicValueFactory::Convert(Value, CI->getValue())) + return UndefinedVal(); + return makeFloatVal(Value); + } - if (isLocType) - return makeIntLocVal(i); - else - return makeIntVal(i); + // Only handle casts from integers to integers - if val is an integer constant + // being cast to a non-integer type, produce unknown. + if (!isLocType && !castTy->isIntegralOrEnumerationType()) + return UnknownVal(); + + llvm::APSInt Value = CI->getValue(); + BasicVals.getAPSIntType(castTy).apply(Value); + if (isLocType) + return makeIntLocVal(Value); + return makeIntVal(Value); + + } + + // Handle casts from real floating-point + if (Optional CF = val.getAs()) { + bool lossOfPrecision; + + if (castTy->isIntegralOrEnumerationType()) { + llvm::APSInt Value(Context.getTypeSize(castTy), + !castTy->isSignedIntegerOrEnumerationType()); + // Cannot be represented in destination type, this is undefined behavior + if (!BasicValueFactory::Convert(Value, CF->getValue())) + return UndefinedVal(); + if (isLocType) + return makeIntLocVal(Value); + return makeIntVal(Value); + } + + if (castTy->isRealFloatingType()) { + if (isLocType) + return UnknownVal(); + + llvm::APFloat Value = CF->getValue(); + llvm::APFloat::opStatus Status = + Value.convert(Context.getFloatTypeSemantics(castTy), + llvm::APFloat::rmNearestTiesToEven, &lossOfPrecision); + // Cannot be represented in destination type, this is undefined behavior + if (Status & (llvm::APFloat::opOverflow | llvm::APFloat::opInvalidOp)) + return UndefinedVal(); + return makeFloatVal(Value); + } + + return UnknownVal(); + } + + return UnknownVal(); } SVal SimpleSValBuilder::evalCastFromLoc(Loc val, QualType castTy) { @@ -191,6 +247,8 @@ switch (val.getSubKind()) { case nonloc::ConcreteIntKind: return val.castAs().evalMinus(*this); + case nonloc::ConcreteFloatKind: + return val.castAs().evalMinus(*this); default: return UnknownVal(); } @@ -304,6 +362,17 @@ return makeNonLoc(LHS, op, *ConvertedRHS, resultTy); } +SVal SimpleSValBuilder::MakeSymFloatVal(const SymExpr *LHS, + BinaryOperator::Opcode op, + const llvm::APFloat &RHS, + QualType resultTy) { + if (RHS.isNaN()) + return makeTruthVal(op == BO_NE, resultTy); + + const llvm::APFloat *ConvertedRHS = &RHS; + return makeNonLoc(LHS, op, *ConvertedRHS, resultTy); +} + SVal SimpleSValBuilder::evalBinOpNN(ProgramStateRef state, BinaryOperator::Opcode op, NonLoc lhs, NonLoc rhs, @@ -312,7 +381,8 @@ NonLoc InputRHS = rhs; // Handle trivial case where left-side and right-side are the same. - if (lhs == rhs) + // Skip floating-point operations, which are not commutative. + if (lhs == rhs && !lhs.isFloat()) switch (op) { default: break; @@ -440,6 +510,29 @@ return makeSymExprValNN(state, op, InputLHS, InputRHS, resultTy); } } + case nonloc::ConcreteFloatKind: { + llvm::APFloat LHSValue = lhs.castAs().getValue(); + + // If we're dealing with two known constants, just perform the operation. + if (const llvm::APFloat *KnownRHSValue = getKnownFloatValue(state, rhs)) { + llvm::APFloat RHSValue = *KnownRHSValue; + + if (BinaryOperator::isComparisonOp(op)) { + const llvm::APSInt *V = BasicVals.evalAPFloatComparison(op, LHSValue, + RHSValue); + if (V) + return nonloc::ConcreteInt(*V); + return UnknownVal(); + } + + const llvm::APFloat *V = BasicVals.evalAPFloat(op, LHSValue, RHSValue); + if (V) + return nonloc::ConcreteFloat(*V); + return UnknownVal(); + } + + return makeSymExprValNN(state, op, InputLHS, InputRHS, resultTy); + } case nonloc::SymbolValKind: { // We only handle LHS as simple symbols or SymIntExprs. SymbolRef Sym = lhs.castAs().getSymbol(); @@ -535,14 +628,26 @@ // If so, "fold" the constant by setting 'lhs' to a ConcreteInt // and try again. ConstraintManager &CMgr = state->getConstraintManager(); - if (const llvm::APSInt *Constant = CMgr.getSymVal(state, Sym)) { - lhs = nonloc::ConcreteInt(*Constant); - continue; + if (Sym->getType()->isRealFloatingType()) { + if (const llvm::APFloat *Constant = CMgr.getSymFloatVal(state, Sym)) { + lhs = nonloc::ConcreteFloat(*Constant); + continue; + } + } else { + if (const llvm::APSInt *Constant = CMgr.getSymVal(state, Sym)) { + lhs = nonloc::ConcreteInt(*Constant); + continue; + } } // Is the RHS a constant? - if (const llvm::APSInt *RHSValue = getKnownValue(state, rhs)) - return MakeSymIntVal(Sym, op, *RHSValue, resultTy); + if (rhs.isFloat()) { + if (const llvm::APFloat *RHSValue = getKnownFloatValue(state, rhs)) + return MakeSymFloatVal(Sym, op, *RHSValue, resultTy); + } else { + if (const llvm::APSInt *RHSValue = getKnownValue(state, rhs)) + return MakeSymIntVal(Sym, op, *RHSValue, resultTy); + } // Give up -- this is not a symbolic expression we can handle. return makeSymExprValNN(state, op, InputLHS, InputRHS, resultTy); @@ -972,6 +1077,8 @@ if (V.isUnknownOrUndef()) return nullptr; + assert(!V.isFloat()); + if (Optional X = V.getAs()) return &X->getValue(); @@ -987,3 +1094,23 @@ return nullptr; } + +const llvm::APFloat *SimpleSValBuilder::getKnownFloatValue(ProgramStateRef state, + SVal V) { + if (V.isUnknownOrUndef()) + return nullptr; + + assert(V.isFloat()); + + if (Optional X = V.getAs()) + return &X->getValue(); + + if (SymbolRef Sym = V.getAsSymbol()) + return state->getConstraintManager().getSymFloatVal(state, Sym); + + if (Optional NV = V.getAs()) + if (SymbolRef Sym = NV->getAsSymExpr()) + return state->getConstraintManager().getSymFloatVal(state, Sym); + + return nullptr; +} Index: lib/StaticAnalyzer/Core/SymbolManager.cpp =================================================================== --- lib/StaticAnalyzer/Core/SymbolManager.cpp +++ lib/StaticAnalyzer/Core/SymbolManager.cpp @@ -48,6 +48,29 @@ os << ')'; } +void SymFloatExpr::dumpToStream(raw_ostream &os) const { + SmallString<24> Chars; + getRHS().toString(Chars, 0, 0); + + os << '('; + getLHS()->dumpToStream(os); + os << ") " + << BinaryOperator::getOpcodeStr(getOpcode()) << ' ' + << Chars; +} + +void FloatSymExpr::dumpToStream(raw_ostream &os) const { + SmallString<24> Chars; + getLHS().toString(Chars, 0, 0); + + os << Chars + << ' ' + << BinaryOperator::getOpcodeStr(getOpcode()) + << " ("; + getRHS()->dumpToStream(os); + os << ')'; +} + void SymSymExpr::dumpToStream(raw_ostream &os) const { os << '('; getLHS()->dumpToStream(os); @@ -131,6 +154,12 @@ case SymExpr::IntSymExprKind: itr.push_back(cast(SE)->getRHS()); return; + case SymExpr::SymFloatExprKind: + itr.push_back(cast(SE)->getLHS()); + return; + case SymExpr::FloatSymExprKind: + itr.push_back(cast(SE)->getRHS()); + return; case SymExpr::SymSymExprKind: { const SymSymExpr *x = cast(SE); itr.push_back(x->getLHS()); @@ -288,6 +317,42 @@ return cast(data); } +const SymFloatExpr *SymbolManager::getSymFloatExpr(const SymExpr *lhs, + BinaryOperator::Opcode op, + const llvm::APFloat& v, + QualType t) { + llvm::FoldingSetNodeID ID; + SymFloatExpr::Profile(ID, lhs, op, v, t); + void *InsertPos; + SymExpr *data = DataSet.FindNodeOrInsertPos(ID, InsertPos); + + if (!data) { + data = (SymFloatExpr*) BPAlloc.Allocate(); + new (data) SymFloatExpr(lhs, op, v, t); + DataSet.InsertNode(data, InsertPos); + } + + return cast(data); +} + +const FloatSymExpr *SymbolManager::getFloatSymExpr(const llvm::APFloat& lhs, + BinaryOperator::Opcode op, + const SymExpr *rhs, + QualType t) { + llvm::FoldingSetNodeID ID; + FloatSymExpr::Profile(ID, lhs, op, rhs, t); + void *InsertPos; + SymExpr *data = DataSet.FindNodeOrInsertPos(ID, InsertPos); + + if (!data) { + data = (FloatSymExpr*) BPAlloc.Allocate(); + new (data) FloatSymExpr(lhs, op, rhs, t); + DataSet.InsertNode(data, InsertPos); + } + + return cast(data); +} + const SymSymExpr *SymbolManager::getSymSymExpr(const SymExpr *lhs, BinaryOperator::Opcode op, const SymExpr *rhs, @@ -340,6 +405,9 @@ if (T->isIntegralOrEnumerationType()) return true; + if (T->isRealFloatingType()) + return true; + if (T->isRecordType() && !T->isUnionType()) return true; @@ -484,6 +552,12 @@ case SymExpr::IntSymExprKind: KnownLive = isLive(cast(sym)->getRHS()); break; + case SymExpr::SymFloatExprKind: + KnownLive = isLive(cast(sym)->getLHS()); + break; + case SymExpr::FloatSymExprKind: + KnownLive = isLive(cast(sym)->getRHS()); + break; case SymExpr::SymSymExprKind: KnownLive = isLive(cast(sym)->getLHS()) && isLive(cast(sym)->getRHS()); Index: test/Analysis/diagnostics/macros.cpp =================================================================== --- test/Analysis/diagnostics/macros.cpp +++ test/Analysis/diagnostics/macros.cpp @@ -30,8 +30,8 @@ // There are no path notes on the comparison to float types. void testDoubleMacro(double d) { - if (d == DBL_MAX) { // expected-note {{Taking true branch}} - + if (d == DBL_MAX) { // expected-note {{Assuming 'd' is equal to DBL_MAX}} + //expected-note@-1 {{Taking true branch}} char *p = NULL; // expected-note {{'p' initialized to a null pointer value}} *p = 7; // expected-warning {{Dereference of null pointer (loaded from variable 'p')}} // expected-note@-1 {{Dereference of null pointer (loaded from variable 'p')}} Index: test/Analysis/float-rules.c =================================================================== --- /dev/null +++ test/Analysis/float-rules.c @@ -0,0 +1,107 @@ +// RUN: %clang_cc1 %z3_cc1 -analyze -analyzer-checker=core.builtin,alpha.core.FPMath,debug.ExprInspection -verify %s +// REQUIRES: z3 + +double acos(double x); +double asin(double x); +double acosh(double x); +double atanh(double x); +double log(double x); +double log2(double x); +double log10(double x); +double log1p(double x); +double logb(double x); +double sqrt(double x); +double fmod(double x, double y); +double remainder(double x, double y); + +double domain1() { + double nan = __builtin_nan(""); + double z = 0.0; + + // -1 <= x <= 1 + z = acos(-5.0); // expected-warning{{Argument value is out of valid domain}} + z = acos(5.0); // expected-warning{{Argument value is out of valid domain}} + z = acos(0.0); // no-warning + z = acos(nan); // no-warning + z = asin(-5.0); // expected-warning{{Argument value is out of valid domain}} + z = asin(5.0); // expected-warning{{Argument value is out of valid domain}} + z = asin(0.0); // no-warning + z = asin(nan); // no-warning + + // x >= 1 + z = acosh(-5.0); // expected-warning{{Argument value is out of valid domain}} + z = acosh(-1.0); // expected-warning{{Argument value is out of valid domain}} + z = acosh(0.0); // expected-warning{{Argument value is out of valid domain}} + z = acosh(1.0); // no-warning + z = acosh(nan); // no-warning + + // -1 < x < 1 + z = atanh(-1.0); // expected-warning{{Argument value is out of valid domain}} + z = atanh(1.0); // expected-warning{{Argument value is out of valid domain}} + z = atanh(0.0); // no-warning + z = atanh(nan); // no-warning + + // x >= 0 + z = log(-1.0); // expected-warning{{Argument value is out of valid domain}} + z = log(-0.5); // expected-warning{{Argument value is out of valid domain}} + z = log(0.0); // no-warning + z = log(nan); // no-warning + z = log2(-1.0); // expected-warning{{Argument value is out of valid domain}} + z = log2(-0.5); // expected-warning{{Argument value is out of valid domain}} + z = log2(0.0); // no-warning + z = log2(nan); // no-warning + z = log10(-1.0); // expected-warning{{Argument value is out of valid domain}} + z = log10(-0.5); // expected-warning{{Argument value is out of valid domain}} + z = log10(0.0); // no-warning + z = log10(nan); // no-warning + z = sqrt(-1.0); // expected-warning{{Argument value is out of valid domain}} + z = sqrt(-0.5); // expected-warning{{Argument value is out of valid domain}} + z = sqrt(0.0); // no-warning + z = sqrt(nan); // no-warning + + // x >= -1 + z = log1p(-5.0); // expected-warning{{Argument value is out of valid domain}} + z = log1p(-1.0); // no-warning + z = log1p(0.0); // no-warning + z = log1p(nan); // no-warning + + // x != 0 + z = logb(0.0); // expected-warning{{Argument value is out of valid domain}} + z = logb(-1.0); // no-warning + z = logb(1.0); // no-warning + z = logb(nan); // no-warning + + return z; +} + +double domain2(double x) { + double nan = __builtin_nan(""); + double z = 0.0; + + // y != 0 + z = fmod(x, 0.0); // expected-warning{{Argument value is out of valid domain}} + z = fmod(x, 1.0); // no-warning + z = fmod(x, -1.0); // no-warning + z = fmod(x, nan); // no-warning + z = remainder(x, 0.0); // expected-warning{{Argument value is out of valid domain}} + z = remainder(x, 1.0); // no-warning + z = remainder(x, -1.0); // no-warning + z = remainder(x, nan); // no-warning + + return z; +} + +double domain3(double x) { + double z = 0.0; + + if (__builtin_isnan(x) || x < 0) + return z; + + z = acosh(x); // expected-warning{{Argument value is out of valid domain}} + z = asin(x); // expected-warning{{Argument value is out of valid domain}} + z = logb(x); // expected-warning{{Argument value is out of valid domain}} + z = log1p(x); // no-warning + z = log(x); // no-warning + + return z; +} Index: test/Analysis/float.c =================================================================== --- /dev/null +++ test/Analysis/float.c @@ -0,0 +1,83 @@ +// RUN: %clang_cc1 %z3_cc1 -analyze -analyzer-checker=core.builtin,debug.ExprInspection -verify %s +// REQUIRES: z3 + +void clang_analyzer_eval(int); + +void float1() { + float z1 = 0.0, z2 = -0.0; + clang_analyzer_eval(z1 == z2); // expected-warning{{TRUE}} +} + +void float2(float a, float b) { + clang_analyzer_eval(a == b); // expected-warning{{UNKNOWN}} + clang_analyzer_eval(a != b); // expected-warning{{UNKNOWN}} +} + +void float3(float a, float b) { + if (__builtin_isnan(a) || __builtin_isnan(b) || a < b) { + clang_analyzer_eval(a > b); // expected-warning{{FALSE}} + clang_analyzer_eval(a == b); // expected-warning{{FALSE}} + return; + } + clang_analyzer_eval(a >= b); // expected-warning{{TRUE}} + clang_analyzer_eval(a == b); // expected-warning{{UNKNOWN}} +} + +void float4(float a) { + if (__builtin_isnan(a) || a < 0.0f) + return; + clang_analyzer_eval(a >= 0.0Q); // expected-warning{{TRUE}} + clang_analyzer_eval(a >= 0.0F); // expected-warning{{TRUE}} + clang_analyzer_eval(a >= 0.0); // expected-warning{{TRUE}} + clang_analyzer_eval(a >= 0); // expected-warning{{TRUE}} +} + +void float5() { + double value = 1.0; + double pinf = __builtin_inf(); + double ninf = -__builtin_inf(); + double nan = __builtin_nan(""); + + /* NaN */ + clang_analyzer_eval(__builtin_isnan(value)); // expected-warning{{FALSE}} + clang_analyzer_eval(__builtin_isnan(nan)); // expected-warning{{TRUE}} + + clang_analyzer_eval(__builtin_isnan(0.0 / 0.0)); // expected-warning{{TRUE}} + clang_analyzer_eval(__builtin_isnan(pinf / ninf)); // expected-warning{{TRUE}} + clang_analyzer_eval(__builtin_isnan(pinf / pinf)); // expected-warning{{TRUE}} + clang_analyzer_eval(__builtin_isnan(ninf / pinf)); // expected-warning{{TRUE}} + clang_analyzer_eval(__builtin_isnan(ninf / ninf)); // expected-warning{{TRUE}} + + clang_analyzer_eval(__builtin_isnan(0.0 * ninf)); // expected-warning{{TRUE}} + clang_analyzer_eval(__builtin_isnan(0.0 * pinf)); // expected-warning{{TRUE}} + clang_analyzer_eval(__builtin_isnan(ninf * 0.0)); // expected-warning{{TRUE}} + clang_analyzer_eval(__builtin_isnan(pinf * 0.0)); // expected-warning{{TRUE}} + + clang_analyzer_eval(__builtin_isnan(nan + value)); // expected-warning{{TRUE}} + clang_analyzer_eval(__builtin_isnan(value - nan)); // expected-warning{{TRUE}} + clang_analyzer_eval(__builtin_isnan(nan * value)); // expected-warning{{TRUE}} + clang_analyzer_eval(__builtin_isnan(value / nan)); // expected-warning{{TRUE}} + + /* Infinity */ + clang_analyzer_eval(__builtin_isinf(value)); // expected-warning{{FALSE}} + clang_analyzer_eval(__builtin_isinf(pinf)); // expected-warning{{TRUE}} + clang_analyzer_eval(__builtin_isinf(ninf)); // expected-warning{{TRUE}} + clang_analyzer_eval(1.0 / pinf == 0.0); // expected-warning{{TRUE}} + clang_analyzer_eval(1.0 / ninf == 0.0); // expected-warning{{TRUE}} + + /* Zero */ + clang_analyzer_eval(0.0 == -0.0); // expected-warning{{TRUE}} +} + +void mixed() { + clang_analyzer_eval(0.0 * 0 == 0.0); // expected-warning{{TRUE}} + clang_analyzer_eval(1.0 * 0 == 0.0); // expected-warning{{TRUE}} + clang_analyzer_eval(1.0 * 1 == 1.0); // expected-warning{{TRUE}} + clang_analyzer_eval((5 * 5) * 1.0 == 25); // expected-warning{{TRUE}} +} + +void nan1(double a) { + if (a == a) + return; + clang_analyzer_eval(__builtin_isnan(a)); // expected-warning{{TRUE}} +} Index: test/Analysis/inline.cpp =================================================================== --- test/Analysis/inline.cpp +++ test/Analysis/inline.cpp @@ -285,11 +285,11 @@ } void testFloatReference() { - clang_analyzer_eval(defaultFloatReference(1) == -1); // expected-warning{{UNKNOWN}} - clang_analyzer_eval(defaultFloatReference() == -42); // expected-warning{{UNKNOWN}} + clang_analyzer_eval(defaultFloatReference(1) == -1); // expected-warning{{TRUE}} + clang_analyzer_eval(defaultFloatReference() == -42); // expected-warning{{TRUE}} - clang_analyzer_eval(defaultFloatReferenceZero(1) == -1); // expected-warning{{UNKNOWN}} - clang_analyzer_eval(defaultFloatReferenceZero() == 0); // expected-warning{{UNKNOWN}} + clang_analyzer_eval(defaultFloatReferenceZero(1) == -1); // expected-warning{{TRUE}} + clang_analyzer_eval(defaultFloatReferenceZero() == 0); // expected-warning{{TRUE}} } char defaultString(const char *s = "abc") { Index: test/Analysis/operator-calls.cpp =================================================================== --- test/Analysis/operator-calls.cpp +++ test/Analysis/operator-calls.cpp @@ -81,8 +81,8 @@ void test(int coin) { // Force a cache-out when we try to conjure a temporary region for the operator call. // ...then, don't crash. - clang_analyzer_eval(+(coin ? getSmallOpaque() : getSmallOpaque())); // expected-warning{{UNKNOWN}} - clang_analyzer_eval(+(coin ? getLargeOpaque() : getLargeOpaque())); // expected-warning{{UNKNOWN}} + clang_analyzer_eval(+(coin ? getSmallOpaque() : getSmallOpaque())); // expected-warning{{TRUE}} + clang_analyzer_eval(+(coin ? getLargeOpaque() : getLargeOpaque())); // expected-warning{{TRUE}} } } Index: tools/z3-constraint-manager/Z3ConstraintManager.cpp =================================================================== --- tools/z3-constraint-manager/Z3ConstraintManager.cpp +++ tools/z3-constraint-manager/Z3ConstraintManager.cpp @@ -77,6 +77,12 @@ Z3_ast Assign = Z3_model_get_const_interp(Z3Expr::ZC, Model, Func); Z3_sort Sort = Z3_get_sort(Z3Expr::ZC, Assign); + if (Z3_get_sort_kind(Z3Expr::ZC, Sort) == Z3_FLOATING_POINT_SORT) { + llvm::APFloat Float(llvm::APFloat::Bogus()); + if (!Z3Expr::toAPFloat(Sort, Assign, Float, false)) + return false; + return BasicValueFactory::Convert(Int, Float); + } return Z3Expr::toAPSInt(Sort, Assign, Int, true); } @@ -88,6 +94,12 @@ Z3_ast Assign = Z3_model_get_const_interp(Z3Expr::ZC, Model, Func); Z3_sort Sort = Z3_get_sort(Z3Expr::ZC, Assign); + if (Z3_get_sort_kind(Z3Expr::ZC, Sort) != Z3_FLOATING_POINT_SORT) { + llvm::APSInt Int; + if (!Z3Expr::toAPSInt(Sort, Assign, Int, false)) + return false; + return BasicValueFactory::Convert(Float, Int); + } return Z3Expr::toAPFloat(Sort, Assign, Float, true); } @@ -617,8 +629,8 @@ }; // end class Z3Expr void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) { - llvm::report_fatal_error("Z3 error: " + - llvm::Twine(Z3_get_error_msg_ex(Context, Error))); + llvm::report_fatal_error( + "Z3 error: " + llvm::Twine(Z3_get_error_msg_ex(Context, Error))); } Z3_context Z3Expr::ZC; @@ -660,6 +672,9 @@ const llvm::APSInt *getSymVal(ProgramStateRef State, SymbolRef Sym) const override; + const llvm::APFloat *getSymFloatVal(ProgramStateRef State, + SymbolRef Sym) const override; + ProgramStateRef removeDeadBindings(ProgramStateRef St, SymbolReaper &SymReaper) override; @@ -740,6 +755,10 @@ // Helper functions. //===------------------------------------------------------------------===// + // Recover the QualType of an APFloat. + // TODO: Refactor to put elsewhere + QualType getAPFloatType(const llvm::APFloat &Float) const; + // Recover the QualType of an APSInt. // TODO: Refactor to put elsewhere QualType getAPSIntType(const llvm::APSInt &Int) const; @@ -765,6 +784,11 @@ void doFloatTypeConversion(T &LHS, QualType <y, T &RHS, QualType &RTy) const; + // Callback function for doCast parameter on APFloat type. + static llvm::APFloat castAPFloat(const llvm::APFloat &V, QualType ToTy, + uint64_t ToWidth, QualType FromTy, + uint64_t FromWidth); + // Callback function for doCast parameter on APSInt type. static llvm::APSInt castAPSInt(const llvm::APSInt &V, QualType ToTy, uint64_t ToWidth, QualType FromTy, @@ -853,6 +877,10 @@ Sym = SIE->getLHS(); } else if (const IntSymExpr *ISE = dyn_cast(BSE)) { Sym = ISE->getRHS(); + } else if (const SymFloatExpr *SFE = dyn_cast(BSE)) { + Sym = SFE->getLHS(); + } else if (const FloatSymExpr *FSE = dyn_cast(BSE)) { + Sym = FSE->getRHS(); } else if (const SymSymExpr *SSM = dyn_cast(BSE)) { return canReasonAbout(nonloc::SymbolVal(SSM->getLHS())) && canReasonAbout(nonloc::SymbolVal(SSM->getRHS())); @@ -889,6 +917,8 @@ return ConditionTruthVal(); } +// TODO: Merge implementation of getSymVal() and getSymFloatVal() into one +// templated function, to avoid weird corner cases when casting back and forth const llvm::APSInt *Z3ConstraintManager::getSymVal(ProgramStateRef State, SymbolRef Sym) const { BasicValueFactory &BV = getBasicVals(); @@ -922,11 +952,45 @@ if (CastTy->isVoidType()) return nullptr; - const llvm::APSInt *Value; - if (!(Value = getSymVal(State, CastSym))) - return nullptr; - return &BV.Convert(SC->getType(), *Value); + // Call the other getSym*Val() function depending on expression type + if (CastSym->getType()->isRealFloatingType()) { + const llvm::APFloat *Float = getSymFloatVal(State, CastSym); + assert(!CastTy->isRealFloatingType()); + llvm::APSInt Int(Ctx.getTypeSize(CastTy), + !CastTy->isSignedIntegerOrEnumerationType()); + if (!Float || !BasicValueFactory::Convert(Int, *Float)) + return nullptr; + return &BV.getValue(Int); + } else { + const llvm::APSInt *Value; + if (!(Value = getSymVal(State, CastSym))) + return nullptr; + return &BV.Convert(CastTy, *Value); + } } else if (const BinarySymExpr *BSE = dyn_cast(Sym)) { + // Floating-point comparisons produce an integral result + if ((isa(BSE) || isa(BSE)) && + BinaryOperator::isComparisonOp(BSE->getOpcode())) { + const llvm::APFloat *LHS, *RHS; + if (const FloatSymExpr *FSE = dyn_cast(BSE)) { + LHS = &FSE->getLHS(); + RHS = getSymFloatVal(State, FSE->getRHS()); + } else if (const SymFloatExpr *SFE = dyn_cast(BSE)) { + LHS = getSymFloatVal(State, SFE->getLHS()); + RHS = &SFE->getRHS(); + } + + if (!LHS || !RHS) + return nullptr; + + llvm::APFloat ConvertedLHS = *LHS, ConvertedRHS = *RHS; + QualType LTy = getAPFloatType(*LHS), RTy = getAPFloatType(*RHS); + doFloatTypeConversion( + ConvertedLHS, LTy, ConvertedRHS, RTy); + return BV.evalAPFloatComparison(BSE->getOpcode(), ConvertedLHS, + ConvertedRHS); + } + const llvm::APSInt *LHS, *RHS; if (const SymIntExpr *SIE = dyn_cast(BSE)) { LHS = getSymVal(State, SIE->getLHS()); @@ -955,6 +1019,80 @@ llvm_unreachable("Unsupported expression to get symbol value!"); } +const llvm::APFloat *Z3ConstraintManager::getSymFloatVal(ProgramStateRef State, + SymbolRef Sym) const { + BasicValueFactory &BV = getBasicVals(); + ASTContext &Ctx = BV.getContext(); + + if (const SymbolData *SD = dyn_cast(Sym)) { + QualType Ty = Sym->getType(); + assert(Ty->isRealFloatingType()); + llvm::APFloat Value(Ctx.getFloatTypeSemantics(Ty)); + + Z3Expr Exp = getZ3DataExpr(SD->getSymbolID(), Ty); + if (getZ3Model(State, Exp, Value) != Z3_L_TRUE) + return nullptr; + + // A value has been obtained, need to check if it is the only value + Z3Expr NotExpr = + Z3Expr::fromFloatBinOp(Exp, BO_NE, Z3Expr::fromAPFloat(Value)); + if (checkZ3Model(State, NotExpr) == Z3_L_TRUE) + return nullptr; + + // This is the only solution, store it + return &BV.getValue(Value); + } else if (const SymbolCast *SC = dyn_cast(Sym)) { + SymbolRef CastSym = SC->getOperand(); + QualType CastTy = SC->getType(); + // Skip the void type + if (CastTy->isVoidType()) + return nullptr; + + // Call the other getSym*Val() function depending on expression type + if (!CastSym->getType()->isRealFloatingType()) { + const llvm::APSInt *Int = getSymVal(State, CastSym); + assert(CastTy->isRealFloatingType()); + llvm::APFloat Float(Ctx.getFloatTypeSemantics(CastTy)); + if (!Int || !BasicValueFactory::Convert(Float, *Int)) + return nullptr; + return &BV.getValue(Float); + } else { + const llvm::APFloat *Value; + if (!(Value = getSymFloatVal(State, CastSym))) + return nullptr; + return &BV.Convert(CastTy, *Value); + } + } else if (const BinarySymExpr *BSE = dyn_cast(Sym)) { + const llvm::APFloat *LHS, *RHS; + if (const SymFloatExpr *SIE = dyn_cast(BSE)) { + LHS = getSymFloatVal(State, SIE->getLHS()); + RHS = &SIE->getRHS(); + } else if (const FloatSymExpr *ISE = dyn_cast(BSE)) { + LHS = &ISE->getLHS(); + RHS = getSymFloatVal(State, ISE->getRHS()); + } else if (const SymSymExpr *SSM = dyn_cast(BSE)) { + // Early termination to avoid expensive call + LHS = getSymFloatVal(State, SSM->getLHS()); + RHS = LHS ? getSymFloatVal(State, SSM->getRHS()) : nullptr; + } else { + llvm_unreachable("Unsupported binary expression to get symbol value!"); + } + + if (!LHS || !RHS) + return nullptr; + + llvm::APFloat ConvertedLHS = *LHS, ConvertedRHS = *RHS; + QualType LTy = getAPFloatType(*LHS), RTy = getAPFloatType(*RHS); + doFloatTypeConversion( + ConvertedLHS, LTy, ConvertedRHS, RTy); + return BV.evalAPFloat(BSE->getOpcode(), ConvertedLHS, ConvertedRHS); + } else { + llvm_unreachable("Unsupported expression to get symbol value!"); + } + + return nullptr; +} + ProgramStateRef Z3ConstraintManager::removeDeadBindings(ProgramStateRef State, SymbolReaper &SymReaper) { @@ -1136,6 +1274,16 @@ Z3Expr LHS = Z3Expr::fromAPSInt(ISE->getLHS()); Z3Expr RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison); return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy); + } else if (const SymFloatExpr *SFE = dyn_cast(BSE)) { + RTy = getAPFloatType(SFE->getRHS()); + Z3Expr LHS = getZ3SymExpr(SFE->getLHS(), <y, hasComparison); + Z3Expr RHS = Z3Expr::fromAPFloat(SFE->getRHS()); + return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy); + } else if (const FloatSymExpr *FSE = dyn_cast(BSE)) { + LTy = getAPFloatType(FSE->getLHS()); + Z3Expr LHS = Z3Expr::fromAPFloat(FSE->getLHS()); + Z3Expr RHS = getZ3SymExpr(FSE->getRHS(), &RTy, hasComparison); + return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy); } else if (const SymSymExpr *SSM = dyn_cast(BSE)) { Z3Expr LHS = getZ3SymExpr(SSM->getLHS(), <y, hasComparison); Z3Expr RHS = getZ3SymExpr(SSM->getRHS(), &RTy, hasComparison); @@ -1182,6 +1330,12 @@ // Helper functions. //===------------------------------------------------------------------===// +QualType Z3ConstraintManager::getAPFloatType(const llvm::APFloat &Float) const { + ASTContext &Ctx = getBasicVals().getContext(); + return Ctx.getRealTypeForBitwidth( + llvm::APFloat::getSizeInBits(Float.getSemantics())); +} + QualType Z3ConstraintManager::getAPSIntType(const llvm::APSInt &Int) const { ASTContext &Ctx = getBasicVals().getContext(); return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned()); @@ -1355,16 +1509,29 @@ // Note: Safe to skip updating bitwidth because this must terminate int order = Ctx.getFloatingTypeOrder(LTy, RTy); if (order > 0) { - RHS = Z3Expr::fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth); + RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth); RTy = LTy; } else if (order == 0) { - LHS = Z3Expr::fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth); + LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth); LTy = RTy; } else { llvm_unreachable("Unsupported floating-point type cast!"); } } +llvm::APFloat Z3ConstraintManager::castAPFloat(const llvm::APFloat &V, + QualType ToTy, uint64_t ToWidth, + QualType FromTy, + uint64_t FromWidth) { + bool lossOfPrecision; + llvm::APFloat To = V; + llvm::APFloat::opStatus Status = + To.convert(Z3Expr::getFloatSemantics(ToWidth), + llvm::APFloat::rmNearestTiesToEven, &lossOfPrecision); + assert(!(Status & (llvm::APFloat::opOverflow | llvm::APFloat::opInvalidOp))); + return To; +} + llvm::APSInt Z3ConstraintManager::castAPSInt(const llvm::APSInt &V, QualType ToTy, uint64_t ToWidth, QualType FromTy,