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