 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
78.8% |
67 / 85 |
| Generated: |
2010-02-10 01:31 |
|
Branches Executed: |
95.3% |
81 / 85 |
| |
|
Line Coverage: |
89.9% |
80 / 89 |
| |
 |
|
 |
1 : //== SimpleConstraintManager.cpp --------------------------------*- C++ -*--==//
2 : //
3 : // The LLVM Compiler Infrastructure
4 : //
5 : // This file is distributed under the University of Illinois Open Source
6 : // License. See LICENSE.TXT for details.
7 : //
8 : //===----------------------------------------------------------------------===//
9 : //
10 : // This file defines SimpleConstraintManager, a class that holds code shared
11 : // between BasicConstraintManager and RangeConstraintManager.
12 : //
13 : //===----------------------------------------------------------------------===//
14 :
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"
19 :
20 : namespace clang {
21 :
0: branch 1 not taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
0: branch 9 not taken
2138: branch 10 taken
22 2138: SimpleConstraintManager::~SimpleConstraintManager() {}
23 :
24 7850: bool SimpleConstraintManager::canReasonAbout(SVal X) const {
2046: branch 1 taken
5804: branch 2 taken
25 7850: if (nonloc::SymExprVal *SymVal = dyn_cast<nonloc::SymExprVal>(&X)) {
26 2046: const SymExpr *SE = SymVal->getSymbolicExpression();
27 :
0: branch 1 not taken
2046: branch 2 taken
28 2046: if (isa<SymbolData>(SE))
29 0: return true;
30 :
2046: branch 1 taken
0: branch 2 not taken
31 2046: if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
10: branch 1 taken
30: branch 2 taken
2006: branch 3 taken
32 2046: 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:
37 10: return false;
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:
46 30: return false;
47 : // All other cases.
48 : default:
49 2006: return true;
50 : }
51 : }
52 :
53 0: return false;
54 : }
55 :
56 5804: return true;
57 : }
58 :
59 : const GRState *SimpleConstraintManager::Assume(const GRState *state,
60 : DefinedSVal Cond,
61 27280: bool Assumption) {
4297: branch 1 taken
22983: branch 2 taken
62 27280: if (isa<NonLoc>(Cond))
63 4297: return Assume(state, cast<NonLoc>(Cond), Assumption);
64 : else
65 22983: return Assume(state, cast<Loc>(Cond), Assumption);
66 : }
67 :
68 : const GRState *SimpleConstraintManager::Assume(const GRState *state, Loc cond,
69 22983: bool assumption) {
70 22983: state = AssumeAux(state, cond, assumption);
71 22983: return SU.ProcessAssume(state, cond, assumption);
72 : }
73 :
74 : const GRState *SimpleConstraintManager::AssumeAux(const GRState *state,
75 23007: Loc Cond, bool Assumption) {
76 :
77 23007: BasicValueFactory &BasicVals = state->getBasicVals();
78 :
0: branch 1 not taken
22811: branch 2 taken
0: branch 3 not taken
196: branch 4 taken
79 23007: switch (Cond.getSubKind()) {
80 : default:
81 0: assert (false && "'Assume' not implemented for this Loc.");
82 : return state;
83 :
84 : case loc::MemRegionKind: {
85 : // FIXME: Should this go into the storemanager?
86 :
87 22811: const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion();
88 22811: const SubRegion *SubR = dyn_cast<SubRegion>(R);
89 :
25231: branch 0 taken
18528: branch 1 taken
90 66570: while (SubR) {
91 : // FIXME: now we only find the first symbolic region.
4283: branch 1 taken
20948: branch 2 taken
92 25231: if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) {
2413: branch 0 taken
1870: branch 1 taken
93 4283: if (Assumption)
94 : return AssumeSymNE(state, SymR->getSymbol(),
95 2413: BasicVals.getZeroWithPtrWidth());
96 : else
97 : return AssumeSymEQ(state, SymR->getSymbol(),
98 1870: BasicVals.getZeroWithPtrWidth());
99 : }
100 20948: SubR = dyn_cast<SubRegion>(SubR->getSuperRegion());
101 : }
102 :
103 : // FALL-THROUGH.
104 : }
105 :
106 : case loc::GotoLabelKind:
9264: branch 0 taken
9264: branch 1 taken
107 18528: return Assumption ? state : NULL;
108 :
109 : case loc::ConcreteIntKind: {
110 196: bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0;
4: branch 0 taken
192: branch 1 taken
111 196: bool isFeasible = b ? Assumption : !Assumption;
98: branch 0 taken
98: branch 1 taken
112 196: return isFeasible ? state : NULL;
113 : }
114 : } // end switch
115 : }
116 :
117 : const GRState *SimpleConstraintManager::Assume(const GRState *state,
118 : NonLoc cond,
119 4297: bool assumption) {
120 4297: state = AssumeAux(state, cond, assumption);
121 4297: return SU.ProcessAssume(state, cond, assumption);
122 : }
123 :
124 : const GRState *SimpleConstraintManager::AssumeAux(const GRState *state,
125 : NonLoc Cond,
126 4297: bool Assumption) {
127 :
128 : // We cannot reason about SymIntExpr and SymSymExpr.
0: branch 2 not taken
4297: branch 3 taken
129 4297: 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.
132 0: return state;
133 : }
134 :
135 4297: BasicValueFactory &BasicVals = state->getBasicVals();
136 4297: SymbolManager &SymMgr = state->getSymbolManager();
137 :
0: branch 1 not taken
476: branch 2 taken
1936: branch 3 taken
1861: branch 4 taken
24: branch 5 taken
138 4297: switch (Cond.getSubKind()) {
139 : default:
140 0: assert(false && "'Assume' not implemented for this NonLoc");
141 :
142 : case nonloc::SymbolValKind: {
143 476: nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond);
144 476: SymbolRef sym = SV.getSymbol();
145 476: QualType T = SymMgr.getType(sym);
146 476: const llvm::APSInt &zero = BasicVals.getValue(0, T);
147 :
148 : return Assumption ? AssumeSymNE(state, sym, zero)
238: branch 0 taken
238: branch 1 taken
149 476: : AssumeSymEQ(state, sym, zero);
150 : }
151 :
152 : case nonloc::SymExprValKind: {
153 1936: nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond);
1936: branch 2 taken
0: branch 3 not taken
154 1936: 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 1936: GRStateManager &StateMgr = state->getStateManager();
159 1936: ASTContext &Ctx = StateMgr.getContext();
160 1936: QualType LHSType = SE->getLHS()->getType(Ctx);
161 1936: BasicValueFactory &BasicVals = StateMgr.getBasicVals();
162 1936: const llvm::APSInt &RHS = BasicVals.Convert(LHSType, SE->getRHS());
163 1936: SymIntExpr SENew(SE->getLHS(), SE->getOpcode(), RHS, SE->getType(Ctx));
164 :
165 1936: return AssumeSymInt(state, Assumption, &SENew);
166 : }
167 :
168 : // For all other symbolic expressions, over-approximate and consider
169 : // the constraint feasible.
170 0: return state;
171 : }
172 :
173 : case nonloc::ConcreteIntKind: {
174 1861: bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0;
1100: branch 0 taken
761: branch 1 taken
175 1861: bool isFeasible = b ? Assumption : !Assumption;
1034: branch 0 taken
827: branch 1 taken
176 1861: return isFeasible ? state : NULL;
177 : }
178 :
179 : case nonloc::LocAsIntegerKind:
180 : return AssumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(),
181 24: Assumption);
182 : } // end switch
183 : }
184 :
185 : const GRState *SimpleConstraintManager::AssumeSymInt(const GRState *state,
186 : bool Assumption,
187 1936: const SymIntExpr *SE) {
188 :
189 :
190 : // Here we assume that LHS is a symbol. This is consistent with the
191 : // rest of the constraint manager logic.
192 1936: SymbolRef Sym = cast<SymbolData>(SE->getLHS());
193 1936: const llvm::APSInt &Int = SE->getRHS();
194 :
0: branch 1 not taken
1243: branch 2 taken
242: branch 3 taken
395: branch 4 taken
8: branch 5 taken
36: branch 6 taken
12: branch 7 taken
195 1936: switch (SE->getOpcode()) {
196 : default:
197 : // No logic yet for other operators. Assume the constraint is feasible.
198 0: return state;
199 :
200 : case BinaryOperator::EQ:
201 : return Assumption ? AssumeSymEQ(state, Sym, Int)
644: branch 0 taken
599: branch 1 taken
202 1243: : AssumeSymNE(state, Sym, Int);
203 :
204 : case BinaryOperator::NE:
205 : return Assumption ? AssumeSymNE(state, Sym, Int)
121: branch 0 taken
121: branch 1 taken
206 242: : AssumeSymEQ(state, Sym, Int);
207 : case BinaryOperator::GT:
208 : return Assumption ? AssumeSymGT(state, Sym, Int)
202: branch 0 taken
193: branch 1 taken
209 395: : AssumeSymLE(state, Sym, Int);
210 :
211 : case BinaryOperator::GE:
212 : return Assumption ? AssumeSymGE(state, Sym, Int)
4: branch 0 taken
4: branch 1 taken
213 8: : AssumeSymLT(state, Sym, Int);
214 :
215 : case BinaryOperator::LT:
216 : return Assumption ? AssumeSymLT(state, Sym, Int)
18: branch 0 taken
18: branch 1 taken
217 36: : AssumeSymGE(state, Sym, Int);
218 :
219 : case BinaryOperator::LE:
220 : return Assumption ? AssumeSymLE(state, Sym, Int)
6: branch 0 taken
6: branch 1 taken
221 12: : AssumeSymGT(state, Sym, Int);
222 : } // end switch
223 : }
224 :
225 : const GRState *SimpleConstraintManager::AssumeInBound(const GRState *state,
226 : DefinedSVal Idx,
227 : DefinedSVal UpperBound,
228 136: bool Assumption) {
229 :
230 : // Only support ConcreteInt for now.
136: branch 1 taken
0: branch 2 not taken
0: branch 4 not taken
136: branch 5 taken
0: branch 6 not taken
136: branch 7 taken
231 136: if (!(isa<nonloc::ConcreteInt>(Idx) && isa<nonloc::ConcreteInt>(UpperBound)))
232 0: return state;
233 :
234 136: const llvm::APSInt& Zero = state->getBasicVals().getZeroWithPtrWidth(false);
235 136: llvm::APSInt IdxV = cast<nonloc::ConcreteInt>(Idx).getValue();
236 : // IdxV might be too narrow.
56: branch 2 taken
80: branch 3 taken
237 136: if (IdxV.getBitWidth() < Zero.getBitWidth())
238 56: IdxV.extend(Zero.getBitWidth());
239 : // UBV might be too narrow, too.
240 136: llvm::APSInt UBV = cast<nonloc::ConcreteInt>(UpperBound).getValue();
0: branch 2 not taken
136: branch 3 taken
241 136: if (UBV.getBitWidth() < Zero.getBitWidth())
242 0: UBV.extend(Zero.getBitWidth());
243 :
136: branch 1 taken
0: branch 2 not taken
122: branch 4 taken
14: branch 5 taken
244 136: bool InBound = (Zero <= IdxV) && (IdxV < UBV);
68: branch 0 taken
68: branch 1 taken
245 136: bool isFeasible = Assumption ? InBound : !InBound;
68: branch 0 taken
68: branch 1 taken
246 136: return isFeasible ? state : NULL;
247 : }
248 :
249 : } // end of namespace clang
Generated: 2010-02-10 01:31 by zcov