diff options
Diffstat (limited to 'lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp')
| -rw-r--r-- | lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp | 178 |
1 files changed, 91 insertions, 87 deletions
diff --git a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp index 79d8b8b..a76a2da 100644 --- a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp +++ b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp @@ -23,11 +23,9 @@ namespace ento { SimpleConstraintManager::~SimpleConstraintManager() {} bool SimpleConstraintManager::canReasonAbout(SVal X) const { - if (nonloc::SymExprVal *SymVal = dyn_cast<nonloc::SymExprVal>(&X)) { - const SymExpr *SE = SymVal->getSymbolicExpression(); - - if (isa<SymbolData>(SE)) - return true; + nonloc::SymbolVal *SymVal = dyn_cast<nonloc::SymbolVal>(&X); + if (SymVal && SymVal->isExpression()) { + const SymExpr *SE = SymVal->getSymbol(); if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) { switch (SIE->getOpcode()) { @@ -56,7 +54,7 @@ bool SimpleConstraintManager::canReasonAbout(SVal X) const { return true; } -const ProgramState *SimpleConstraintManager::assume(const ProgramState *state, +ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, DefinedSVal Cond, bool Assumption) { if (isa<NonLoc>(Cond)) @@ -65,13 +63,13 @@ const ProgramState *SimpleConstraintManager::assume(const ProgramState *state, return assume(state, cast<Loc>(Cond), Assumption); } -const ProgramState *SimpleConstraintManager::assume(const ProgramState *state, Loc cond, +ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, Loc cond, bool assumption) { state = assumeAux(state, cond, assumption); return SU.processAssume(state, cond, assumption); } -const ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *state, +ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, Loc Cond, bool Assumption) { BasicValueFactory &BasicVals = state->getBasicVals(); @@ -113,7 +111,7 @@ const ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *state } // end switch } -const ProgramState *SimpleConstraintManager::assume(const ProgramState *state, +ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, NonLoc cond, bool assumption) { state = assumeAux(state, cond, assumption); @@ -135,16 +133,29 @@ static BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) { } } -const ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *state, + +ProgramStateRef SimpleConstraintManager::assumeAuxForSymbol( + ProgramStateRef State, + SymbolRef Sym, + bool Assumption) { + QualType T = State->getSymbolManager().getType(Sym); + const llvm::APSInt &zero = State->getBasicVals().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) { - // We cannot reason about SymSymExprs, - // and can only reason about some SymIntExprs. + // We cannot reason about SymSymExprs, and can only reason about some + // SymIntExprs. if (!canReasonAbout(Cond)) { - // Just return the current state indicating that the path is feasible. - // This may be an over-approximation of what is possible. - return state; + // Just add the constraint to the expression without trying to simplify. + SymbolRef sym = Cond.getAsSymExpr(); + return assumeAuxForSymbol(state, sym, Assumption); } BasicValueFactory &BasicVals = state->getBasicVals(); @@ -157,37 +168,33 @@ const ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *state case nonloc::SymbolValKind: { nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond); SymbolRef sym = SV.getSymbol(); - QualType T = SymMgr.getType(sym); - const llvm::APSInt &zero = BasicVals.getValue(0, T); - if (Assumption) - return assumeSymNE(state, sym, zero, zero); - else - return assumeSymEQ(state, sym, zero, zero); - } + assert(sym); + + // Handle SymbolData. + if (!SV.isExpression()) { + return assumeAuxForSymbol(state, sym, Assumption); + + // Handle symbolic expression. + } else { + // We can only simplify expressions whose RHS is an integer. + const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym); + if (!SE) + return assumeAuxForSymbol(state, sym, Assumption); + + BinaryOperator::Opcode op = SE->getOpcode(); + // Implicitly compare non-comparison expressions to 0. + if (!BinaryOperator::isComparisonOp(op)) { + QualType T = SymMgr.getType(SE); + const llvm::APSInt &zero = BasicVals.getValue(0, T); + op = (Assumption ? BO_NE : BO_EQ); + return assumeSymRel(state, SE, op, zero); + } + // From here on out, op is the real comparison we'll be testing. + if (!Assumption) + op = NegateComparison(op); - case nonloc::SymExprValKind: { - nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond); - - // For now, we only handle expressions whose RHS is an integer. - // All other expressions are assumed to be feasible. - const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression()); - if (!SE) - return state; - - BinaryOperator::Opcode op = SE->getOpcode(); - // Implicitly compare non-comparison expressions to 0. - if (!BinaryOperator::isComparisonOp(op)) { - QualType T = SymMgr.getType(SE); - const llvm::APSInt &zero = BasicVals.getValue(0, T); - op = (Assumption ? BO_NE : BO_EQ); - return assumeSymRel(state, SE, op, zero); + return assumeSymRel(state, SE->getLHS(), op, SE->getRHS()); } - - // From here on out, op is the real comparison we'll be testing. - if (!Assumption) - op = NegateComparison(op); - - return assumeSymRel(state, SE->getLHS(), op, SE->getRHS()); } case nonloc::ConcreteIntKind: { @@ -202,55 +209,52 @@ const ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *state } // end switch } -const ProgramState *SimpleConstraintManager::assumeSymRel(const ProgramState *state, +static llvm::APSInt computeAdjustment(const SymExpr *LHS, + SymbolRef &Sym) { + llvm::APSInt DefaultAdjustment; + DefaultAdjustment = 0; + + // First check if the LHS is a simple symbol reference. + if (isa<SymbolData>(LHS)) + return DefaultAdjustment; + + // Next, see if it's a "($sym+constant1)" expression. + const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS); + + // We cannot simplify "($sym1+$sym2)". + if (!SE) + return DefaultAdjustment; + + // Get the constant out of the expression "($sym+constant1)" or + // "<expr>+constant1". + Sym = SE->getLHS(); + switch (SE->getOpcode()) { + case BO_Add: + return SE->getRHS(); + case BO_Sub: + return -SE->getRHS(); + default: + // We cannot simplify non-additive operators. + return DefaultAdjustment; + } +} + +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."); - // 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; - - // First check if the LHS is a simple symbol reference. - SymbolRef Sym = dyn_cast<SymbolData>(LHS); - if (Sym) { - Adjustment = 0; - } else { - // Next, see if it's a "($sym+constant1)" expression. - const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS); - - // We don't handle "($sym1+$sym2)". - // Give up and assume the constraint is feasible. - if (!SE) - return state; - - // We don't handle "(<expr>+constant1)". - // Give up and assume the constraint is feasible. - Sym = dyn_cast<SymbolData>(SE->getLHS()); - if (!Sym) - return state; - - // Get the constant out of the expression "($sym+constant1)". - switch (SE->getOpcode()) { - case BO_Add: - Adjustment = SE->getRHS(); - break; - case BO_Sub: - Adjustment = -SE->getRHS(); - break; - default: - // We don't handle non-additive operators. - // Give up and assume the constraint is feasible. - return state; - } - } + // 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. + SymbolRef Sym = LHS; + llvm::APSInt Adjustment = computeAdjustment(LHS, Sym); // FIXME: This next section is a hack. It silently converts the integers to // be of the same type as the symbol, which is not always correct. Really the |
