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,8 @@ return nullptr; } + /// Scan all symbols referenced by the constraints. If the symbol is not + /// alive, remove it. virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, SymbolReaper& SymReaper) = 0; Index: include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h =================================================================== --- /dev/null +++ include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h @@ -0,0 +1,92 @@ +//== SimpleConstraintManager.h ----------------------------------*- C++ -*--==// +// +// The LLVM Compiler Infrastructure +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +// +// Simplified constraint manager backend. +// +//===----------------------------------------------------------------------===// + +#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SIMPLECONSTRAINTMANAGER_H +#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SIMPLECONSTRAINTMANAGER_H + +#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" + +namespace clang { + +namespace ento { + +class SimpleConstraintManager : public ConstraintManager { + SubEngine *SU; + SValBuilder &SVB; + +public: + SimpleConstraintManager(SubEngine *subengine, SValBuilder &SB) + : SU(subengine), SVB(SB) {} + + ~SimpleConstraintManager() override; + + //===------------------------------------------------------------------===// + // Implementation for interface from ConstraintManager. + //===------------------------------------------------------------------===// + + /// Ensures that the DefinedSVal conditional is expressed as a NonLoc by + /// creating boolean casts to handle Loc's. + ProgramStateRef assume(ProgramStateRef State, DefinedSVal Cond, + bool Assumption) override; + + ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value, + const llvm::APSInt &From, + const llvm::APSInt &To, + bool InRange) override; + +protected: + //===------------------------------------------------------------------===// + // Interface that subclasses must implement. + //===------------------------------------------------------------------===// + + /// Given a symbolic expression that can be reasoned about, assume that it is + /// true/false and generate the new program state. + virtual ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym, + bool Assumption) = 0; + + /// Given a symbolic expression within the range [From, To], assume that it is + /// true/false and generate the new program state. + /// This function is used to handle case ranges produced by a language + /// extension for switch case statements. + virtual ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, + SymbolRef Sym, + const llvm::APSInt &From, + const llvm::APSInt &To, + bool InRange) = 0; + + /// Given a symbolic expression that cannot be reasoned about, assume that + /// it is zero/nonzero and add it directly to the solver state. + virtual ProgramStateRef assumeSymUnsupported(ProgramStateRef State, + SymbolRef Sym, + bool Assumption) = 0; + + //===------------------------------------------------------------------===// + // Internal implementation. + //===------------------------------------------------------------------===// + + BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); } + SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); } + +private: + ProgramStateRef assume(ProgramStateRef State, NonLoc Cond, bool Assumption); + + ProgramStateRef assumeAux(ProgramStateRef State, NonLoc Cond, + bool Assumption); +}; + +} // end GR namespace + +} // end clang namespace + +#endif Index: lib/StaticAnalyzer/Core/CMakeLists.txt =================================================================== --- lib/StaticAnalyzer/Core/CMakeLists.txt +++ lib/StaticAnalyzer/Core/CMakeLists.txt @@ -34,6 +34,7 @@ PlistDiagnostics.cpp ProgramState.cpp RangeConstraintManager.cpp + RangedConstraintManager.cpp RegionStore.cpp SValBuilder.cpp SVals.cpp Index: lib/StaticAnalyzer/Core/ConstraintManager.cpp =================================================================== --- lib/StaticAnalyzer/Core/ConstraintManager.cpp +++ lib/StaticAnalyzer/Core/ConstraintManager.cpp @@ -20,8 +20,8 @@ static DefinedSVal getLocFromSymbol(const ProgramStateRef &State, SymbolRef Sym) { - const MemRegion *R = State->getStateManager().getRegionManager() - .getSymbolicRegion(Sym); + const MemRegion *R = + State->getStateManager().getRegionManager().getSymbolicRegion(Sym); return loc::MemRegionVal(R); } Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp =================================================================== --- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -12,7 +12,7 @@ // //===----------------------------------------------------------------------===// -#include "SimpleConstraintManager.h" +#include "RangedConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h" @@ -282,12 +282,31 @@ RangeSet)) namespace { -class RangeConstraintManager : public SimpleConstraintManager { - RangeSet getRange(ProgramStateRef State, SymbolRef Sym); - +class RangeConstraintManager : public RangedConstraintManager { public: RangeConstraintManager(SubEngine *SE, SValBuilder &SVB) - : SimpleConstraintManager(SE, SVB) {} + : RangedConstraintManager(SE, SVB) {} + + //===------------------------------------------------------------------===// + // Implementation for interface from ConstraintManager. + //===------------------------------------------------------------------===// + + bool canReasonAbout(SVal X) const override; + + ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override; + + const llvm::APSInt *getSymVal(ProgramStateRef State, + SymbolRef Sym) const override; + + ProgramStateRef removeDeadBindings(ProgramStateRef State, + SymbolReaper &SymReaper) override; + + void print(ProgramStateRef State, raw_ostream &Out, const char *nl, + const char *sep) override; + + //===------------------------------------------------------------------===// + // Implementation for interface from RangedConstraintManager. + //===------------------------------------------------------------------===// ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &V, @@ -313,26 +332,19 @@ const llvm::APSInt &V, const llvm::APSInt &Adjustment) override; - ProgramStateRef assumeSymbolWithinInclusiveRange( + ProgramStateRef assumeSymWithinInclusiveRange( ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, const llvm::APSInt &Adjustment) override; - ProgramStateRef assumeSymbolOutOfInclusiveRange( + ProgramStateRef assumeSymOutsideInclusiveRange( ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, const llvm::APSInt &Adjustment) override; - const llvm::APSInt *getSymVal(ProgramStateRef St, - SymbolRef Sym) const override; - ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override; - - ProgramStateRef removeDeadBindings(ProgramStateRef St, - SymbolReaper &SymReaper) override; - - void print(ProgramStateRef St, raw_ostream &Out, const char *nl, - const char *sep) override; - private: RangeSet::Factory F; + + RangeSet getRange(ProgramStateRef State, SymbolRef Sym); + RangeSet getSymLTRange(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, const llvm::APSInt &Adjustment); @@ -356,10 +368,46 @@ return llvm::make_unique(Eng, StMgr.getSValBuilder()); } -const llvm::APSInt *RangeConstraintManager::getSymVal(ProgramStateRef St, - SymbolRef Sym) const { - const ConstraintRangeTy::data_type *T = St->get(Sym); - return T ? T->getConcreteValue() : nullptr; +bool RangeConstraintManager::canReasonAbout(SVal X) const { + Optional SymVal = X.getAs(); + if (SymVal && SymVal->isExpression()) { + const SymExpr *SE = SymVal->getSymbol(); + + if (const SymIntExpr *SIE = dyn_cast(SE)) { + switch (SIE->getOpcode()) { + // We don't reason yet about bitwise-constraints on symbolic values. + case BO_And: + case BO_Or: + case BO_Xor: + return false; + // We don't reason yet about these arithmetic constraints on + // symbolic values. + case BO_Mul: + case BO_Div: + case BO_Rem: + case BO_Shl: + case BO_Shr: + return false; + // All other cases. + default: + return true; + } + } + + if (const SymSymExpr *SSE = dyn_cast(SE)) { + if (BinaryOperator::isComparisonOp(SSE->getOpcode())) { + // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc. + if (Loc::isLocType(SSE->getLHS()->getType())) { + assert(Loc::isLocType(SSE->getRHS()->getType())); + return true; + } + } + } + + return false; + } + + return true; } ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State, @@ -386,6 +434,12 @@ return ConditionTruthVal(); } +const llvm::APSInt *RangeConstraintManager::getSymVal(ProgramStateRef St, + SymbolRef Sym) const { + const ConstraintRangeTy::data_type *T = St->get(Sym); + return T ? T->getConcreteValue() : nullptr; +} + /// Scan all symbols referenced by the constraints. If the symbol is not alive /// as marked in LSymbols, mark it as dead in DSymbols. ProgramStateRef @@ -429,7 +483,7 @@ } //===------------------------------------------------------------------------=== -// assumeSymX methods: public interface for RangeConstraintManager. +// assumeSymX methods: protected interface for RangeConstraintManager. //===------------------------------------------------------------------------===/ // The syntax for ranges below is mathematical, using [x, y] for closed ranges @@ -646,7 +700,7 @@ return New.isEmpty() ? nullptr : St->set(Sym, New); } -ProgramStateRef RangeConstraintManager::assumeSymbolWithinInclusiveRange( +ProgramStateRef RangeConstraintManager::assumeSymWithinInclusiveRange( ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, const llvm::APSInt &Adjustment) { RangeSet New = getSymGERange(State, Sym, From, Adjustment); @@ -656,7 +710,7 @@ return New.isEmpty() ? nullptr : State->set(Sym, New); } -ProgramStateRef RangeConstraintManager::assumeSymbolOutOfInclusiveRange( +ProgramStateRef RangeConstraintManager::assumeSymOutsideInclusiveRange( ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, const llvm::APSInt &Adjustment) { RangeSet RangeLT = getSymLTRange(State, Sym, From, Adjustment); Index: lib/StaticAnalyzer/Core/RangedConstraintManager.h =================================================================== --- lib/StaticAnalyzer/Core/RangedConstraintManager.h +++ lib/StaticAnalyzer/Core/RangedConstraintManager.h @@ -1,4 +1,4 @@ -//== SimpleConstraintManager.h ----------------------------------*- C++ -*--==// +//== RangedConstraintManager.h ----------------------------------*- C++ -*--==// // // The LLVM Compiler Infrastructure // @@ -7,59 +7,55 @@ // //===----------------------------------------------------------------------===// // -// Code shared between BasicConstraintManager and RangeConstraintManager. +// Ranged constraint manager, built on SimpleConstraintManager. // //===----------------------------------------------------------------------===// -#ifndef LLVM_CLANG_LIB_STATICANALYZER_CORE_SIMPLECONSTRAINTMANAGER_H -#define LLVM_CLANG_LIB_STATICANALYZER_CORE_SIMPLECONSTRAINTMANAGER_H +#ifndef LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H +#define LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H -#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h" namespace clang { namespace ento { -class SimpleConstraintManager : public ConstraintManager { - SubEngine *SU; - SValBuilder &SVB; - +class RangedConstraintManager : public SimpleConstraintManager { public: - SimpleConstraintManager(SubEngine *SE, SValBuilder &SB) : SU(SE), SVB(SB) {} - ~SimpleConstraintManager() override; + RangedConstraintManager(SubEngine *SE, SValBuilder &SB) + : SimpleConstraintManager(SE, SB) {} + + ~RangedConstraintManager() override; //===------------------------------------------------------------------===// - // Common implementation for the interface provided by ConstraintManager. + // Implementation for interface from SimpleConstraintManager. //===------------------------------------------------------------------===// - ProgramStateRef assume(ProgramStateRef State, DefinedSVal Cond, - bool Assumption) override; + ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym, + bool Assumption) override; - ProgramStateRef assume(ProgramStateRef State, NonLoc Cond, bool Assumption); + ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, + const llvm::APSInt &From, + const llvm::APSInt &To, + bool InRange) override; - ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value, - const llvm::APSInt &From, - const llvm::APSInt &To, - bool InRange) override; + ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, + bool Assumption) override; - ProgramStateRef assumeSymRel(ProgramStateRef State, const SymExpr *LHS, - BinaryOperator::Opcode Op, +protected: + /// Assume a constraint between a symbolic expression and a concrete integer. + virtual ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym, + BinaryOperator::Opcode op, const llvm::APSInt &Int); - ProgramStateRef assumeSymWithinInclusiveRange(ProgramStateRef State, - SymbolRef Sym, - const llvm::APSInt &From, - const llvm::APSInt &To, - bool InRange); - -protected: //===------------------------------------------------------------------===// // Interface that subclasses must implement. //===------------------------------------------------------------------===// // Each of these is of the form "$Sym+Adj <> V", where "<>" is the comparison // operation for the method being invoked. + virtual ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &V, const llvm::APSInt &Adjustment) = 0; @@ -84,28 +80,19 @@ const llvm::APSInt &V, const llvm::APSInt &Adjustment) = 0; - virtual ProgramStateRef assumeSymbolWithinInclusiveRange( + virtual ProgramStateRef assumeSymWithinInclusiveRange( ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0; - virtual ProgramStateRef assumeSymbolOutOfInclusiveRange( + virtual ProgramStateRef assumeSymOutsideInclusiveRange( ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0; //===------------------------------------------------------------------===// // Internal implementation. //===------------------------------------------------------------------===// - - BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); } - SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); } - - bool canReasonAbout(SVal X) const override; - - ProgramStateRef assumeAux(ProgramStateRef State, NonLoc Cond, - bool Assumption); - - ProgramStateRef assumeAuxForSymbol(ProgramStateRef State, SymbolRef Sym, - bool Assumption); +private: + static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment); }; } // end GR namespace Index: lib/StaticAnalyzer/Core/RangedConstraintManager.cpp =================================================================== --- /dev/null +++ lib/StaticAnalyzer/Core/RangedConstraintManager.cpp @@ -0,0 +1,204 @@ +//== RangedConstraintManager.cpp --------------------------------*- C++ -*--==// +// +// The LLVM Compiler Infrastructure +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +// +// This file defines RangedConstraintManager, a class that provides a +// range-based constraint manager interface. +// +//===----------------------------------------------------------------------===// + +#include "RangedConstraintManager.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" + +namespace clang { + +namespace ento { + +RangedConstraintManager::~RangedConstraintManager() {} + +ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State, + SymbolRef Sym, + bool Assumption) { + // Handle SymbolData. + if (isa(Sym)) { + return assumeSymUnsupported(State, Sym, Assumption); + + // Handle symbolic expression. + } else if (const SymIntExpr *SIE = dyn_cast(Sym)) { + // We can only simplify expressions whose RHS is an integer. + + BinaryOperator::Opcode op = SIE->getOpcode(); + if (BinaryOperator::isComparisonOp(op)) { + if (!Assumption) + op = BinaryOperator::negateComparisonOp(op); + + return assumeSymRel(State, SIE->getLHS(), op, SIE->getRHS()); + } + + } else if (const SymSymExpr *SSE = dyn_cast(Sym)) { + // Translate "a != b" to "(b - a) != 0". + // We invert the order of the operands as a heuristic for how loop + // conditions are usually written ("begin != end") as compared to length + // calculations ("end - begin"). The more correct thing to do would be to + // canonicalize "a - b" and "b - a", which would allow us to treat + // "a != b" and "b != a" the same. + SymbolManager &SymMgr = getSymbolManager(); + BinaryOperator::Opcode Op = SSE->getOpcode(); + assert(BinaryOperator::isComparisonOp(Op)); + + // For now, we only support comparing pointers. + assert(Loc::isLocType(SSE->getLHS()->getType())); + assert(Loc::isLocType(SSE->getRHS()->getType())); + QualType DiffTy = SymMgr.getContext().getPointerDiffType(); + SymbolRef Subtraction = + SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), DiffTy); + + const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy); + Op = BinaryOperator::reverseComparisonOp(Op); + if (!Assumption) + Op = BinaryOperator::negateComparisonOp(Op); + return assumeSymRel(State, Subtraction, Op, Zero); + } + + // If we get here, there's nothing else we can do but treat the symbol as + // opaque. + return assumeSymUnsupported(State, Sym, Assumption); +} + +ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange( + ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, + const llvm::APSInt &To, bool InRange) { + // Get the type used for calculating wraparound. + BasicValueFactory &BVF = getBasicVals(); + APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType()); + + llvm::APSInt Adjustment = WraparoundType.getZeroValue(); + SymbolRef AdjustedSym = Sym; + computeAdjustment(AdjustedSym, Adjustment); + + // Convert the right-hand side integer as necessary. + APSIntType ComparisonType = std::max(WraparoundType, APSIntType(From)); + llvm::APSInt ConvertedFrom = ComparisonType.convert(From); + llvm::APSInt ConvertedTo = ComparisonType.convert(To); + + // Prefer unsigned comparisons. + if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() && + ComparisonType.isUnsigned() && !WraparoundType.isUnsigned()) + Adjustment.setIsSigned(false); + + if (InRange) + return assumeSymWithinInclusiveRange(State, AdjustedSym, ConvertedFrom, + ConvertedTo, Adjustment); + return assumeSymOutsideInclusiveRange(State, AdjustedSym, ConvertedFrom, + ConvertedTo, Adjustment); +} + +ProgramStateRef +RangedConstraintManager::assumeSymUnsupported(ProgramStateRef State, + SymbolRef Sym, bool Assumption) { + BasicValueFactory &BVF = getBasicVals(); + QualType T = Sym->getType(); + + // Non-integer types are not supported. + if (!T->isIntegralOrEnumerationType()) + return State; + + // Reverse the operation and add directly to state. + const llvm::APSInt &Zero = BVF.getValue(0, T); + if (Assumption) + return assumeSymNE(State, Sym, Zero, Zero); + else + return assumeSymEQ(State, Sym, Zero, Zero); +} + +ProgramStateRef RangedConstraintManager::assumeSymRel(ProgramStateRef State, + SymbolRef Sym, + BinaryOperator::Opcode Op, + const llvm::APSInt &Int) { + assert(BinaryOperator::isComparisonOp(Op) && + "Non-comparison ops should be rewritten as comparisons to zero."); + + // Simplification: translate an assume of a constraint of the form + // "(exp comparison_op expr) != 0" to true into an assume of + // "exp comparison_op expr" to true. (And similarly, an assume of the form + // "(exp comparison_op expr) == 0" to true into an assume of + // "exp comparison_op expr" to false.) + if (Int == 0 && (Op == BO_EQ || Op == BO_NE)) { + if (const BinarySymExpr *SE = dyn_cast(Sym)) + if (BinaryOperator::isComparisonOp(SE->getOpcode())) + return assumeSym(State, Sym, (Op == BO_NE ? true : false)); + } + + // Get the type used for calculating wraparound. + BasicValueFactory &BVF = getBasicVals(); + APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType()); + + // We only handle simple comparisons of the form "$sym == constant" + // or "($sym+constant1) == constant2". + // The adjustment is "constant1" in the above expression. It's used to + // "slide" the solution range around for modular arithmetic. For example, + // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which + // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to + // the subclasses of SimpleConstraintManager to handle the adjustment. + llvm::APSInt Adjustment = WraparoundType.getZeroValue(); + computeAdjustment(Sym, Adjustment); + + // Convert the right-hand side integer as necessary. + APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int)); + llvm::APSInt ConvertedInt = ComparisonType.convert(Int); + + // Prefer unsigned comparisons. + if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() && + ComparisonType.isUnsigned() && !WraparoundType.isUnsigned()) + Adjustment.setIsSigned(false); + + switch (Op) { + default: + llvm_unreachable("invalid operation not caught by assertion above"); + + case BO_EQ: + return assumeSymEQ(State, Sym, ConvertedInt, Adjustment); + + case BO_NE: + return assumeSymNE(State, Sym, ConvertedInt, Adjustment); + + case BO_GT: + return assumeSymGT(State, Sym, ConvertedInt, Adjustment); + + case BO_GE: + return assumeSymGE(State, Sym, ConvertedInt, Adjustment); + + case BO_LT: + return assumeSymLT(State, Sym, ConvertedInt, Adjustment); + + case BO_LE: + return assumeSymLE(State, Sym, ConvertedInt, Adjustment); + } // end switch +} + +void RangedConstraintManager::computeAdjustment(SymbolRef &Sym, + llvm::APSInt &Adjustment) { + // Is it a "($sym+constant1)" expression? + if (const SymIntExpr *SE = dyn_cast(Sym)) { + BinaryOperator::Opcode Op = SE->getOpcode(); + if (Op == BO_Add || Op == BO_Sub) { + Sym = SE->getLHS(); + Adjustment = APSIntType(Adjustment).convert(SE->getRHS()); + + // Don't forget to negate the adjustment if it's being subtracted. + // This should happen /after/ promotion, in case the value being + // subtracted is, say, CHAR_MIN, and the promoted type is 'int'. + if (Op == BO_Sub) + Adjustment = -Adjustment; + } + } +} + +} // end of namespace ento + +} // end of namespace clang Index: lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp =================================================================== --- lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp +++ lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp @@ -7,12 +7,12 @@ // //===----------------------------------------------------------------------===// // -// This file defines SimpleConstraintManager, a class that holds code shared -// between BasicConstraintManager and RangeConstraintManager. +// This file defines SimpleConstraintManager, a class that provides a +// simplified constraint manager interface, compared to ConstraintManager. // //===----------------------------------------------------------------------===// -#include "SimpleConstraintManager.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" @@ -23,48 +23,6 @@ SimpleConstraintManager::~SimpleConstraintManager() {} -bool SimpleConstraintManager::canReasonAbout(SVal X) const { - Optional SymVal = X.getAs(); - if (SymVal && SymVal->isExpression()) { - const SymExpr *SE = SymVal->getSymbol(); - - if (const SymIntExpr *SIE = dyn_cast(SE)) { - switch (SIE->getOpcode()) { - // We don't reason yet about bitwise-constraints on symbolic values. - case BO_And: - case BO_Or: - case BO_Xor: - return false; - // We don't reason yet about these arithmetic constraints on - // symbolic values. - case BO_Mul: - case BO_Div: - case BO_Rem: - case BO_Shl: - case BO_Shr: - return false; - // All other cases. - default: - return true; - } - } - - if (const SymSymExpr *SSE = dyn_cast(SE)) { - if (BinaryOperator::isComparisonOp(SSE->getOpcode())) { - // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc. - if (Loc::isLocType(SSE->getLHS()->getType())) { - assert(Loc::isLocType(SSE->getRHS()->getType())); - return true; - } - } - } - - return false; - } - - return true; -} - ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef State, DefinedSVal Cond, bool Assumption) { @@ -92,23 +50,6 @@ return State; } -ProgramStateRef -SimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State, - SymbolRef Sym, bool Assumption) { - BasicValueFactory &BVF = getBasicVals(); - QualType T = Sym->getType(); - - // None of the constraint solvers currently support non-integer types. - if (!T->isIntegralOrEnumerationType()) - return State; - - const llvm::APSInt &zero = BVF.getValue(0, T); - if (Assumption) - return assumeSymNE(State, Sym, zero, zero); - else - return assumeSymEQ(State, Sym, zero, zero); -} - ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef State, NonLoc Cond, bool Assumption) { @@ -118,7 +59,8 @@ if (!canReasonAbout(Cond)) { // Just add the constraint to the expression without trying to simplify. SymbolRef Sym = Cond.getAsSymExpr(); - return assumeAuxForSymbol(State, Sym, Assumption); + assert(Sym); + return assumeSymUnsupported(State, Sym, Assumption); } switch (Cond.getSubKind()) { @@ -129,51 +71,7 @@ nonloc::SymbolVal SV = Cond.castAs(); SymbolRef Sym = SV.getSymbol(); assert(Sym); - - // Handle SymbolData. - if (!SV.isExpression()) { - return assumeAuxForSymbol(State, Sym, Assumption); - - // Handle symbolic expression. - } else if (const SymIntExpr *SE = dyn_cast(Sym)) { - // We can only simplify expressions whose RHS is an integer. - - BinaryOperator::Opcode Op = SE->getOpcode(); - if (BinaryOperator::isComparisonOp(Op)) { - if (!Assumption) - Op = BinaryOperator::negateComparisonOp(Op); - - return assumeSymRel(State, SE->getLHS(), Op, SE->getRHS()); - } - - } else if (const SymSymExpr *SSE = dyn_cast(Sym)) { - // Translate "a != b" to "(b - a) != 0". - // We invert the order of the operands as a heuristic for how loop - // conditions are usually written ("begin != end") as compared to length - // calculations ("end - begin"). The more correct thing to do would be to - // canonicalize "a - b" and "b - a", which would allow us to treat - // "a != b" and "b != a" the same. - SymbolManager &SymMgr = getSymbolManager(); - BinaryOperator::Opcode Op = SSE->getOpcode(); - assert(BinaryOperator::isComparisonOp(Op)); - - // For now, we only support comparing pointers. - assert(Loc::isLocType(SSE->getLHS()->getType())); - assert(Loc::isLocType(SSE->getRHS()->getType())); - QualType DiffTy = SymMgr.getContext().getPointerDiffType(); - SymbolRef Subtraction = - SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), DiffTy); - - const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy); - Op = BinaryOperator::reverseComparisonOp(Op); - if (!Assumption) - Op = BinaryOperator::negateComparisonOp(Op); - return assumeSymRel(State, Subtraction, Op, Zero); - } - - // If we get here, there's nothing else we can do but treat the symbol as - // opaque. - return assumeAuxForSymbol(State, Sym, Assumption); + return assumeSym(State, Sym, Assumption); } case nonloc::ConcreteIntKind: { @@ -206,7 +104,7 @@ // Just add the constraint to the expression without trying to simplify. SymbolRef Sym = Value.getAsSymExpr(); assert(Sym); - return assumeSymWithinInclusiveRange(State, Sym, From, To, InRange); + return assumeSymInclusiveRange(State, Sym, From, To, InRange); } switch (Value.getSubKind()) { @@ -217,7 +115,7 @@ case nonloc::LocAsIntegerKind: case nonloc::SymbolValKind: { if (SymbolRef Sym = Value.getAsSymbol()) - return assumeSymWithinInclusiveRange(State, Sym, From, To, InRange); + return assumeSymInclusiveRange(State, Sym, From, To, InRange); return State; } // end switch @@ -230,118 +128,6 @@ } // end switch } -static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) { - // Is it a "($sym+constant1)" expression? - if (const SymIntExpr *SE = dyn_cast(Sym)) { - BinaryOperator::Opcode Op = SE->getOpcode(); - if (Op == BO_Add || Op == BO_Sub) { - Sym = SE->getLHS(); - Adjustment = APSIntType(Adjustment).convert(SE->getRHS()); - - // Don't forget to negate the adjustment if it's being subtracted. - // This should happen /after/ promotion, in case the value being - // subtracted is, say, CHAR_MIN, and the promoted type is 'int'. - if (Op == BO_Sub) - Adjustment = -Adjustment; - } - } -} - -ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef State, - const SymExpr *LHS, - BinaryOperator::Opcode Op, - const llvm::APSInt &Int) { - assert(BinaryOperator::isComparisonOp(Op) && - "Non-comparison ops should be rewritten as comparisons to zero."); - - SymbolRef Sym = LHS; - - // Simplification: translate an assume of a constraint of the form - // "(exp comparison_op expr) != 0" to true into an assume of - // "exp comparison_op expr" to true. (And similarly, an assume of the form - // "(exp comparison_op expr) == 0" to true into an assume of - // "exp comparison_op expr" to false.) - if (Int == 0 && (Op == BO_EQ || Op == BO_NE)) { - if (const BinarySymExpr *SE = dyn_cast(Sym)) - if (BinaryOperator::isComparisonOp(SE->getOpcode())) - return assume(State, nonloc::SymbolVal(Sym), (Op == BO_NE ? true : false)); - } - - // Get the type used for calculating wraparound. - BasicValueFactory &BVF = getBasicVals(); - APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType()); - - // We only handle simple comparisons of the form "$sym == constant" - // or "($sym+constant1) == constant2". - // The adjustment is "constant1" in the above expression. It's used to - // "slide" the solution range around for modular arithmetic. For example, - // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which - // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to - // the subclasses of SimpleConstraintManager to handle the adjustment. - llvm::APSInt Adjustment = WraparoundType.getZeroValue(); - computeAdjustment(Sym, Adjustment); - - // Convert the right-hand side integer as necessary. - APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int)); - llvm::APSInt ConvertedInt = ComparisonType.convert(Int); - - // Prefer unsigned comparisons. - if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() && - ComparisonType.isUnsigned() && !WraparoundType.isUnsigned()) - Adjustment.setIsSigned(false); - - switch (Op) { - default: - llvm_unreachable("invalid operation not caught by assertion above"); - - case BO_EQ: - return assumeSymEQ(State, Sym, ConvertedInt, Adjustment); - - case BO_NE: - return assumeSymNE(State, Sym, ConvertedInt, Adjustment); - - case BO_GT: - return assumeSymGT(State, Sym, ConvertedInt, Adjustment); - - case BO_GE: - return assumeSymGE(State, Sym, ConvertedInt, Adjustment); - - case BO_LT: - return assumeSymLT(State, Sym, ConvertedInt, Adjustment); - - case BO_LE: - return assumeSymLE(State, Sym, ConvertedInt, Adjustment); - } // end switch -} - -ProgramStateRef SimpleConstraintManager::assumeSymWithinInclusiveRange( - ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, - const llvm::APSInt &To, bool InRange) { - // Get the type used for calculating wraparound. - BasicValueFactory &BVF = getBasicVals(); - APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType()); - - llvm::APSInt Adjustment = WraparoundType.getZeroValue(); - SymbolRef AdjustedSym = Sym; - computeAdjustment(AdjustedSym, Adjustment); - - // Convert the right-hand side integer as necessary. - APSIntType ComparisonType = std::max(WraparoundType, APSIntType(From)); - llvm::APSInt ConvertedFrom = ComparisonType.convert(From); - llvm::APSInt ConvertedTo = ComparisonType.convert(To); - - // Prefer unsigned comparisons. - if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() && - ComparisonType.isUnsigned() && !WraparoundType.isUnsigned()) - Adjustment.setIsSigned(false); - - if (InRange) - return assumeSymbolWithinInclusiveRange(State, AdjustedSym, ConvertedFrom, - ConvertedTo, Adjustment); - return assumeSymbolOutOfInclusiveRange(State, AdjustedSym, ConvertedFrom, - ConvertedTo, Adjustment); -} - } // end of namespace ento } // end of namespace clang