1 //== SimpleConstraintManager.cpp --------------------------------*- C++ -*--==//
3 // The LLVM Compiler Infrastructure
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
8 //===----------------------------------------------------------------------===//
10 // This file defines SimpleConstraintManager, a class that holds code shared
11 // between BasicConstraintManager and RangeConstraintManager.
13 //===----------------------------------------------------------------------===//
15 #include "SimpleConstraintManager.h"
16 #include "clang/Checker/PathSensitive/GRExprEngine.h"
17 #include "clang/Checker/PathSensitive/GRState.h"
18 #include "clang/Checker/PathSensitive/Checker.h"
22 SimpleConstraintManager::~SimpleConstraintManager() {}
24 bool SimpleConstraintManager::canReasonAbout(SVal X) const {
25 if (nonloc::SymExprVal *SymVal = dyn_cast<nonloc::SymExprVal>(&X)) {
26 const SymExpr *SE = SymVal->getSymbolicExpression();
28 if (isa<SymbolData>(SE))
31 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
32 switch (SIE->getOpcode()) {
33 // We don't reason yet about bitwise-constraints on symbolic values.
34 case BinaryOperator::And:
35 case BinaryOperator::Or:
36 case BinaryOperator::Xor:
38 // We don't reason yet about arithmetic constraints on symbolic values.
39 case BinaryOperator::Mul:
40 case BinaryOperator::Div:
41 case BinaryOperator::Rem:
42 case BinaryOperator::Add:
43 case BinaryOperator::Sub:
44 case BinaryOperator::Shl:
45 case BinaryOperator::Shr:
59 const GRState *SimpleConstraintManager::Assume(const GRState *state,
62 if (isa<NonLoc>(Cond))
63 return Assume(state, cast<NonLoc>(Cond), Assumption);
65 return Assume(state, cast<Loc>(Cond), Assumption);
68 const GRState *SimpleConstraintManager::Assume(const GRState *state, Loc cond,
70 state = AssumeAux(state, cond, assumption);
71 return SU.ProcessAssume(state, cond, assumption);
74 const GRState *SimpleConstraintManager::AssumeAux(const GRState *state,
75 Loc Cond, bool Assumption) {
77 BasicValueFactory &BasicVals = state->getBasicVals();
79 switch (Cond.getSubKind()) {
81 assert (false && "'Assume' not implemented for this Loc.");
84 case loc::MemRegionKind: {
85 // FIXME: Should this go into the storemanager?
87 const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion();
88 const SubRegion *SubR = dyn_cast<SubRegion>(R);
91 // FIXME: now we only find the first symbolic region.
92 if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) {
94 return AssumeSymNE(state, SymR->getSymbol(),
95 BasicVals.getZeroWithPtrWidth());
97 return AssumeSymEQ(state, SymR->getSymbol(),
98 BasicVals.getZeroWithPtrWidth());
100 SubR = dyn_cast<SubRegion>(SubR->getSuperRegion());
106 case loc::GotoLabelKind:
107 return Assumption ? state : NULL;
109 case loc::ConcreteIntKind: {
110 bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0;
111 bool isFeasible = b ? Assumption : !Assumption;
112 return isFeasible ? state : NULL;
117 const GRState *SimpleConstraintManager::Assume(const GRState *state,
120 state = AssumeAux(state, cond, assumption);
121 return SU.ProcessAssume(state, cond, assumption);
124 const GRState *SimpleConstraintManager::AssumeAux(const GRState *state,
128 // We cannot reason about SymIntExpr and SymSymExpr.
129 if (!canReasonAbout(Cond)) {
130 // Just return the current state indicating that the path is feasible.
131 // This may be an over-approximation of what is possible.
135 BasicValueFactory &BasicVals = state->getBasicVals();
136 SymbolManager &SymMgr = state->getSymbolManager();
138 switch (Cond.getSubKind()) {
140 assert(false && "'Assume' not implemented for this NonLoc");
142 case nonloc::SymbolValKind: {
143 nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond);
144 SymbolRef sym = SV.getSymbol();
145 QualType T = SymMgr.getType(sym);
146 const llvm::APSInt &zero = BasicVals.getValue(0, T);
148 return Assumption ? AssumeSymNE(state, sym, zero)
149 : AssumeSymEQ(state, sym, zero);
152 case nonloc::SymExprValKind: {
153 nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond);
154 if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression())){
155 // FIXME: This is a hack. It silently converts the RHS integer to be
156 // of the same type as on the left side. This should be removed once
157 // we support truncation/extension of symbolic values.
158 GRStateManager &StateMgr = state->getStateManager();
159 ASTContext &Ctx = StateMgr.getContext();
160 QualType LHSType = SE->getLHS()->getType(Ctx);
161 BasicValueFactory &BasicVals = StateMgr.getBasicVals();
162 const llvm::APSInt &RHS = BasicVals.Convert(LHSType, SE->getRHS());
163 SymIntExpr SENew(SE->getLHS(), SE->getOpcode(), RHS, SE->getType(Ctx));
165 return AssumeSymInt(state, Assumption, &SENew);
168 // For all other symbolic expressions, over-approximate and consider
169 // the constraint feasible.
173 case nonloc::ConcreteIntKind: {
174 bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0;
175 bool isFeasible = b ? Assumption : !Assumption;
176 return isFeasible ? state : NULL;
179 case nonloc::LocAsIntegerKind:
180 return AssumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(),
185 const GRState *SimpleConstraintManager::AssumeSymInt(const GRState *state,
187 const SymIntExpr *SE) {
190 // Here we assume that LHS is a symbol. This is consistent with the
191 // rest of the constraint manager logic.
192 SymbolRef Sym = cast<SymbolData>(SE->getLHS());
193 const llvm::APSInt &Int = SE->getRHS();
195 switch (SE->getOpcode()) {
197 // No logic yet for other operators. Assume the constraint is feasible.
200 case BinaryOperator::EQ:
201 return Assumption ? AssumeSymEQ(state, Sym, Int)
202 : AssumeSymNE(state, Sym, Int);
204 case BinaryOperator::NE:
205 return Assumption ? AssumeSymNE(state, Sym, Int)
206 : AssumeSymEQ(state, Sym, Int);
207 case BinaryOperator::GT:
208 return Assumption ? AssumeSymGT(state, Sym, Int)
209 : AssumeSymLE(state, Sym, Int);
211 case BinaryOperator::GE:
212 return Assumption ? AssumeSymGE(state, Sym, Int)
213 : AssumeSymLT(state, Sym, Int);
215 case BinaryOperator::LT:
216 return Assumption ? AssumeSymLT(state, Sym, Int)
217 : AssumeSymGE(state, Sym, Int);
219 case BinaryOperator::LE:
220 return Assumption ? AssumeSymLE(state, Sym, Int)
221 : AssumeSymGT(state, Sym, Int);
225 const GRState *SimpleConstraintManager::AssumeInBound(const GRState *state,
227 DefinedSVal UpperBound,
230 // Only support ConcreteInt for now.
231 if (!(isa<nonloc::ConcreteInt>(Idx) && isa<nonloc::ConcreteInt>(UpperBound)))
234 const llvm::APSInt& Zero = state->getBasicVals().getZeroWithPtrWidth(false);
235 llvm::APSInt IdxV = cast<nonloc::ConcreteInt>(Idx).getValue();
236 // IdxV might be too narrow.
237 if (IdxV.getBitWidth() < Zero.getBitWidth())
238 IdxV.extend(Zero.getBitWidth());
239 // UBV might be too narrow, too.
240 llvm::APSInt UBV = cast<nonloc::ConcreteInt>(UpperBound).getValue();
241 if (UBV.getBitWidth() < Zero.getBitWidth())
242 UBV.extend(Zero.getBitWidth());
244 bool InBound = (Zero <= IdxV) && (IdxV < UBV);
245 bool isFeasible = Assumption ? InBound : !InBound;
246 return isFeasible ? state : NULL;
249 } // end of namespace clang