| //== SimpleConstraintManager.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 SimpleConstraintManager, a class that holds code shared |
| // between BasicConstraintManager and RangeConstraintManager. |
| // |
| //===----------------------------------------------------------------------===// |
| |
| #include "SimpleConstraintManager.h" |
| #include "clang/Checker/PathSensitive/GRExprEngine.h" |
| #include "clang/Checker/PathSensitive/GRState.h" |
| #include "clang/Checker/PathSensitive/Checker.h" |
| |
| namespace clang { |
| |
| 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; |
| |
| if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) { |
| switch (SIE->getOpcode()) { |
| // We don't reason yet about bitwise-constraints on symbolic values. |
| case BinaryOperator::And: |
| case BinaryOperator::Or: |
| case BinaryOperator::Xor: |
| return false; |
| // We don't reason yet about these arithmetic constraints on |
| // symbolic values. |
| case BinaryOperator::Mul: |
| case BinaryOperator::Div: |
| case BinaryOperator::Rem: |
| case BinaryOperator::Shl: |
| case BinaryOperator::Shr: |
| return false; |
| // All other cases. |
| default: |
| return true; |
| } |
| } |
| |
| return false; |
| } |
| |
| return true; |
| } |
| |
| const GRState *SimpleConstraintManager::Assume(const GRState *state, |
| DefinedSVal Cond, |
| bool Assumption) { |
| if (isa<NonLoc>(Cond)) |
| return Assume(state, cast<NonLoc>(Cond), Assumption); |
| else |
| return Assume(state, cast<Loc>(Cond), Assumption); |
| } |
| |
| const GRState *SimpleConstraintManager::Assume(const GRState *state, Loc cond, |
| bool assumption) { |
| state = AssumeAux(state, cond, assumption); |
| return SU.ProcessAssume(state, cond, assumption); |
| } |
| |
| const GRState *SimpleConstraintManager::AssumeAux(const GRState *state, |
| Loc Cond, bool Assumption) { |
| |
| BasicValueFactory &BasicVals = state->getBasicVals(); |
| |
| switch (Cond.getSubKind()) { |
| default: |
| assert (false && "'Assume' not implemented for this Loc."); |
| return state; |
| |
| case loc::MemRegionKind: { |
| // FIXME: Should this go into the storemanager? |
| |
| const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion(); |
| const SubRegion *SubR = dyn_cast<SubRegion>(R); |
| |
| while (SubR) { |
| // FIXME: now we only find the first symbolic region. |
| if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) { |
| const llvm::APSInt &zero = BasicVals.getZeroWithPtrWidth(); |
| if (Assumption) |
| return AssumeSymNE(state, SymR->getSymbol(), zero, zero); |
| else |
| return AssumeSymEQ(state, SymR->getSymbol(), zero, zero); |
| } |
| SubR = dyn_cast<SubRegion>(SubR->getSuperRegion()); |
| } |
| |
| // FALL-THROUGH. |
| } |
| |
| case loc::GotoLabelKind: |
| return Assumption ? state : NULL; |
| |
| case loc::ConcreteIntKind: { |
| bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0; |
| bool isFeasible = b ? Assumption : !Assumption; |
| return isFeasible ? state : NULL; |
| } |
| } // end switch |
| } |
| |
| const GRState *SimpleConstraintManager::Assume(const GRState *state, |
| NonLoc cond, |
| bool assumption) { |
| state = AssumeAux(state, cond, assumption); |
| return SU.ProcessAssume(state, cond, assumption); |
| } |
| |
| static BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) { |
| // FIXME: This should probably be part of BinaryOperator, since this isn't |
| // the only place it's used. (This code was copied from SimpleSValuator.cpp.) |
| switch (op) { |
| default: |
| assert(false && "Invalid opcode."); |
| case BinaryOperator::LT: return BinaryOperator::GE; |
| case BinaryOperator::GT: return BinaryOperator::LE; |
| case BinaryOperator::LE: return BinaryOperator::GT; |
| case BinaryOperator::GE: return BinaryOperator::LT; |
| case BinaryOperator::EQ: return BinaryOperator::NE; |
| case BinaryOperator::NE: return BinaryOperator::EQ; |
| } |
| } |
| |
| const GRState *SimpleConstraintManager::AssumeAux(const GRState *state, |
| NonLoc Cond, |
| bool Assumption) { |
| |
| // 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; |
| } |
| |
| BasicValueFactory &BasicVals = state->getBasicVals(); |
| SymbolManager &SymMgr = state->getSymbolManager(); |
| |
| switch (Cond.getSubKind()) { |
| default: |
| assert(false && "'Assume' not implemented for this NonLoc"); |
| |
| 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); |
| } |
| |
| 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; |
| |
| GRStateManager &StateMgr = state->getStateManager(); |
| ASTContext &Ctx = StateMgr.getContext(); |
| BasicValueFactory &BasicVals = StateMgr.getBasicVals(); |
| |
| // FIXME: This is a hack. It silently converts the RHS integer to be |
| // of the same type as on the left side. This should be removed once |
| // we support truncation/extension of symbolic values. |
| const SymExpr *LHS = SE->getLHS(); |
| QualType LHSType = LHS->getType(Ctx); |
| const llvm::APSInt &RHS = BasicVals.Convert(LHSType, SE->getRHS()); |
| |
| BinaryOperator::Opcode op = SE->getOpcode(); |
| // FIXME: We should implicitly compare non-comparison expressions to 0. |
| if (!BinaryOperator::isComparisonOp(op)) |
| return state; |
| |
| // From here on out, op is the real comparison we'll be testing. |
| if (!Assumption) |
| op = NegateComparison(op); |
| |
| return AssumeSymRel(state, LHS, op, RHS); |
| } |
| |
| case nonloc::ConcreteIntKind: { |
| bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0; |
| bool isFeasible = b ? Assumption : !Assumption; |
| return isFeasible ? state : NULL; |
| } |
| |
| case nonloc::LocAsIntegerKind: |
| return AssumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(), |
| Assumption); |
| } // end switch |
| } |
| |
| const GRState *SimpleConstraintManager::AssumeSymRel(const GRState *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(Int.getBitWidth(), Int.isUnsigned()); |
| |
| // First check if the LHS is a simple symbol reference. |
| SymbolRef Sym = dyn_cast<SymbolData>(LHS); |
| if (!Sym) { |
| // 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 BinaryOperator::Add: |
| Adjustment = SE->getRHS(); |
| break; |
| case BinaryOperator::Sub: |
| Adjustment = -SE->getRHS(); |
| break; |
| default: |
| // We don't handle non-additive operators. |
| // Give up and assume the constraint is feasible. |
| return state; |
| } |
| } |
| |
| switch (op) { |
| default: |
| // No logic yet for other operators. Assume the constraint is feasible. |
| return state; |
| |
| case BinaryOperator::EQ: |
| return AssumeSymEQ(state, Sym, Int, Adjustment); |
| |
| case BinaryOperator::NE: |
| return AssumeSymNE(state, Sym, Int, Adjustment); |
| |
| case BinaryOperator::GT: |
| return AssumeSymGT(state, Sym, Int, Adjustment); |
| |
| case BinaryOperator::GE: |
| return AssumeSymGE(state, Sym, Int, Adjustment); |
| |
| case BinaryOperator::LT: |
| return AssumeSymLT(state, Sym, Int, Adjustment); |
| |
| case BinaryOperator::LE: |
| return AssumeSymLE(state, Sym, Int, Adjustment); |
| } // end switch |
| } |
| |
| const GRState *SimpleConstraintManager::AssumeInBound(const GRState *state, |
| DefinedSVal Idx, |
| DefinedSVal UpperBound, |
| bool Assumption) { |
| |
| // Only support ConcreteInt for now. |
| if (!(isa<nonloc::ConcreteInt>(Idx) && isa<nonloc::ConcreteInt>(UpperBound))) |
| return state; |
| |
| const llvm::APSInt& Zero = state->getBasicVals().getZeroWithPtrWidth(false); |
| llvm::APSInt IdxV = cast<nonloc::ConcreteInt>(Idx).getValue(); |
| // IdxV might be too narrow. |
| if (IdxV.getBitWidth() < Zero.getBitWidth()) |
| IdxV.extend(Zero.getBitWidth()); |
| // UBV might be too narrow, too. |
| llvm::APSInt UBV = cast<nonloc::ConcreteInt>(UpperBound).getValue(); |
| if (UBV.getBitWidth() < Zero.getBitWidth()) |
| UBV.extend(Zero.getBitWidth()); |
| |
| bool InBound = (Zero <= IdxV) && (IdxV < UBV); |
| bool isFeasible = Assumption ? InBound : !InBound; |
| return isFeasible ? state : NULL; |
| } |
| |
| } // end of namespace clang |