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/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
17 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
18
19 namespace clang {
20
21 namespace ento {
22
~SimpleConstraintManager()23 SimpleConstraintManager::~SimpleConstraintManager() {}
24
canReasonAbout(SVal X) const25 bool SimpleConstraintManager::canReasonAbout(SVal X) const {
26 nonloc::SymbolVal *SymVal = dyn_cast<nonloc::SymbolVal>(&X);
27 if (SymVal && SymVal->isExpression()) {
28 const SymExpr *SE = SymVal->getSymbol();
29
30 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
31 switch (SIE->getOpcode()) {
32 // We don't reason yet about bitwise-constraints on symbolic values.
33 case BO_And:
34 case BO_Or:
35 case BO_Xor:
36 return false;
37 // We don't reason yet about these arithmetic constraints on
38 // symbolic values.
39 case BO_Mul:
40 case BO_Div:
41 case BO_Rem:
42 case BO_Shl:
43 case BO_Shr:
44 return false;
45 // All other cases.
46 default:
47 return true;
48 }
49 }
50
51 return false;
52 }
53
54 return true;
55 }
56
assume(ProgramStateRef state,DefinedSVal Cond,bool Assumption)57 ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
58 DefinedSVal Cond,
59 bool Assumption) {
60 if (isa<NonLoc>(Cond))
61 return assume(state, cast<NonLoc>(Cond), Assumption);
62 else
63 return assume(state, cast<Loc>(Cond), Assumption);
64 }
65
assume(ProgramStateRef state,Loc cond,bool assumption)66 ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, Loc cond,
67 bool assumption) {
68 state = assumeAux(state, cond, assumption);
69 return SU.processAssume(state, cond, assumption);
70 }
71
assumeAux(ProgramStateRef state,Loc Cond,bool Assumption)72 ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
73 Loc Cond, bool Assumption) {
74
75 BasicValueFactory &BasicVals = state->getBasicVals();
76
77 switch (Cond.getSubKind()) {
78 default:
79 assert (false && "'Assume' not implemented for this Loc.");
80 return state;
81
82 case loc::MemRegionKind: {
83 // FIXME: Should this go into the storemanager?
84
85 const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion();
86 const SubRegion *SubR = dyn_cast<SubRegion>(R);
87
88 while (SubR) {
89 // FIXME: now we only find the first symbolic region.
90 if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) {
91 const llvm::APSInt &zero = BasicVals.getZeroWithPtrWidth();
92 if (Assumption)
93 return assumeSymNE(state, SymR->getSymbol(), zero, zero);
94 else
95 return assumeSymEQ(state, SymR->getSymbol(), zero, zero);
96 }
97 SubR = dyn_cast<SubRegion>(SubR->getSuperRegion());
98 }
99
100 // FALL-THROUGH.
101 }
102
103 case loc::GotoLabelKind:
104 return Assumption ? state : NULL;
105
106 case loc::ConcreteIntKind: {
107 bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0;
108 bool isFeasible = b ? Assumption : !Assumption;
109 return isFeasible ? state : NULL;
110 }
111 } // end switch
112 }
113
assume(ProgramStateRef state,NonLoc cond,bool assumption)114 ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
115 NonLoc cond,
116 bool assumption) {
117 state = assumeAux(state, cond, assumption);
118 return SU.processAssume(state, cond, assumption);
119 }
120
NegateComparison(BinaryOperator::Opcode op)121 static BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) {
122 // FIXME: This should probably be part of BinaryOperator, since this isn't
123 // the only place it's used. (This code was copied from SimpleSValBuilder.cpp.)
124 switch (op) {
125 default:
126 llvm_unreachable("Invalid opcode.");
127 case BO_LT: return BO_GE;
128 case BO_GT: return BO_LE;
129 case BO_LE: return BO_GT;
130 case BO_GE: return BO_LT;
131 case BO_EQ: return BO_NE;
132 case BO_NE: return BO_EQ;
133 }
134 }
135
136
assumeAuxForSymbol(ProgramStateRef State,SymbolRef Sym,bool Assumption)137 ProgramStateRef SimpleConstraintManager::assumeAuxForSymbol(
138 ProgramStateRef State,
139 SymbolRef Sym,
140 bool Assumption) {
141 QualType T = State->getSymbolManager().getType(Sym);
142 const llvm::APSInt &zero = State->getBasicVals().getValue(0, T);
143 if (Assumption)
144 return assumeSymNE(State, Sym, zero, zero);
145 else
146 return assumeSymEQ(State, Sym, zero, zero);
147 }
148
assumeAux(ProgramStateRef state,NonLoc Cond,bool Assumption)149 ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
150 NonLoc Cond,
151 bool Assumption) {
152
153 // We cannot reason about SymSymExprs, and can only reason about some
154 // SymIntExprs.
155 if (!canReasonAbout(Cond)) {
156 // Just add the constraint to the expression without trying to simplify.
157 SymbolRef sym = Cond.getAsSymExpr();
158 return assumeAuxForSymbol(state, sym, Assumption);
159 }
160
161 BasicValueFactory &BasicVals = state->getBasicVals();
162 SymbolManager &SymMgr = state->getSymbolManager();
163
164 switch (Cond.getSubKind()) {
165 default:
166 llvm_unreachable("'Assume' not implemented for this NonLoc");
167
168 case nonloc::SymbolValKind: {
169 nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond);
170 SymbolRef sym = SV.getSymbol();
171 assert(sym);
172
173 // Handle SymbolData.
174 if (!SV.isExpression()) {
175 return assumeAuxForSymbol(state, sym, Assumption);
176
177 // Handle symbolic expression.
178 } else {
179 // We can only simplify expressions whose RHS is an integer.
180 const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym);
181 if (!SE)
182 return assumeAuxForSymbol(state, sym, Assumption);
183
184 BinaryOperator::Opcode op = SE->getOpcode();
185 // Implicitly compare non-comparison expressions to 0.
186 if (!BinaryOperator::isComparisonOp(op)) {
187 QualType T = SymMgr.getType(SE);
188 const llvm::APSInt &zero = BasicVals.getValue(0, T);
189 op = (Assumption ? BO_NE : BO_EQ);
190 return assumeSymRel(state, SE, op, zero);
191 }
192 // From here on out, op is the real comparison we'll be testing.
193 if (!Assumption)
194 op = NegateComparison(op);
195
196 return assumeSymRel(state, SE->getLHS(), op, SE->getRHS());
197 }
198 }
199
200 case nonloc::ConcreteIntKind: {
201 bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0;
202 bool isFeasible = b ? Assumption : !Assumption;
203 return isFeasible ? state : NULL;
204 }
205
206 case nonloc::LocAsIntegerKind:
207 return assumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(),
208 Assumption);
209 } // end switch
210 }
211
computeAdjustment(const SymExpr * LHS,SymbolRef & Sym)212 static llvm::APSInt computeAdjustment(const SymExpr *LHS,
213 SymbolRef &Sym) {
214 llvm::APSInt DefaultAdjustment;
215 DefaultAdjustment = 0;
216
217 // First check if the LHS is a simple symbol reference.
218 if (isa<SymbolData>(LHS))
219 return DefaultAdjustment;
220
221 // Next, see if it's a "($sym+constant1)" expression.
222 const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS);
223
224 // We cannot simplify "($sym1+$sym2)".
225 if (!SE)
226 return DefaultAdjustment;
227
228 // Get the constant out of the expression "($sym+constant1)" or
229 // "<expr>+constant1".
230 Sym = SE->getLHS();
231 switch (SE->getOpcode()) {
232 case BO_Add:
233 return SE->getRHS();
234 case BO_Sub:
235 return -SE->getRHS();
236 default:
237 // We cannot simplify non-additive operators.
238 return DefaultAdjustment;
239 }
240 }
241
assumeSymRel(ProgramStateRef state,const SymExpr * LHS,BinaryOperator::Opcode op,const llvm::APSInt & Int)242 ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state,
243 const SymExpr *LHS,
244 BinaryOperator::Opcode op,
245 const llvm::APSInt& Int) {
246 assert(BinaryOperator::isComparisonOp(op) &&
247 "Non-comparison ops should be rewritten as comparisons to zero.");
248
249 // We only handle simple comparisons of the form "$sym == constant"
250 // or "($sym+constant1) == constant2".
251 // The adjustment is "constant1" in the above expression. It's used to
252 // "slide" the solution range around for modular arithmetic. For example,
253 // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
254 // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
255 // the subclasses of SimpleConstraintManager to handle the adjustment.
256 SymbolRef Sym = LHS;
257 llvm::APSInt Adjustment = computeAdjustment(LHS, Sym);
258
259 // FIXME: This next section is a hack. It silently converts the integers to
260 // be of the same type as the symbol, which is not always correct. Really the
261 // comparisons should be performed using the Int's type, then mapped back to
262 // the symbol's range of values.
263 ProgramStateManager &StateMgr = state->getStateManager();
264 ASTContext &Ctx = StateMgr.getContext();
265
266 QualType T = Sym->getType(Ctx);
267 assert(T->isIntegerType() || Loc::isLocType(T));
268 unsigned bitwidth = Ctx.getTypeSize(T);
269 bool isSymUnsigned
270 = T->isUnsignedIntegerOrEnumerationType() || Loc::isLocType(T);
271
272 // Convert the adjustment.
273 Adjustment.setIsUnsigned(isSymUnsigned);
274 Adjustment = Adjustment.extOrTrunc(bitwidth);
275
276 // Convert the right-hand side integer.
277 llvm::APSInt ConvertedInt(Int, isSymUnsigned);
278 ConvertedInt = ConvertedInt.extOrTrunc(bitwidth);
279
280 switch (op) {
281 default:
282 // No logic yet for other operators. assume the constraint is feasible.
283 return state;
284
285 case BO_EQ:
286 return assumeSymEQ(state, Sym, ConvertedInt, Adjustment);
287
288 case BO_NE:
289 return assumeSymNE(state, Sym, ConvertedInt, Adjustment);
290
291 case BO_GT:
292 return assumeSymGT(state, Sym, ConvertedInt, Adjustment);
293
294 case BO_GE:
295 return assumeSymGE(state, Sym, ConvertedInt, Adjustment);
296
297 case BO_LT:
298 return assumeSymLT(state, Sym, ConvertedInt, Adjustment);
299
300 case BO_LE:
301 return assumeSymLE(state, Sym, ConvertedInt, Adjustment);
302 } // end switch
303 }
304
305 } // end of namespace ento
306
307 } // end of namespace clang
308