blob: a4d59bec887381ecc6b880ef0b56b798fd1d7f54 [file] [log] [blame]
Ted Kremenek45021952009-02-14 17:08:39 +00001//== 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/Analysis/PathSensitive/GRExprEngine.h"
17#include "clang/Analysis/PathSensitive/GRState.h"
18
19namespace clang {
20
21SimpleConstraintManager::~SimpleConstraintManager() {}
22
Ted Kremenek66b52712009-03-11 02:22:59 +000023bool SimpleConstraintManager::canReasonAbout(SVal X) const {
Ted Kremenek7de20fe2009-03-11 02:29:48 +000024 if (nonloc::SymIntConstraintVal *Y = dyn_cast<nonloc::SymIntConstraintVal>(&X)) {
25 const SymIntConstraint& C = Y->getConstraint();
26 switch (C.getOpcode()) {
27 // We don't reason yet about bitwise-constraints on symbolic values.
28 case BinaryOperator::And:
29 case BinaryOperator::Or:
30 case BinaryOperator::Xor:
31 return false;
32 default:
33 return true;
34 }
35 }
36
Ted Kremenek66b52712009-03-11 02:22:59 +000037 return true;
38}
39
Ted Kremenek45021952009-02-14 17:08:39 +000040const GRState*
41SimpleConstraintManager::Assume(const GRState* St, SVal Cond, bool Assumption,
42 bool& isFeasible) {
43 if (Cond.isUnknown()) {
44 isFeasible = true;
45 return St;
46 }
47
48 if (isa<NonLoc>(Cond))
49 return Assume(St, cast<NonLoc>(Cond), Assumption, isFeasible);
50 else
51 return Assume(St, cast<Loc>(Cond), Assumption, isFeasible);
52}
53
54const GRState*
55SimpleConstraintManager::Assume(const GRState* St, Loc Cond, bool Assumption,
56 bool& isFeasible) {
57 St = AssumeAux(St, Cond, Assumption, isFeasible);
58
59 if (!isFeasible)
60 return St;
61
62 // EvalAssume is used to call into the GRTransferFunction object to perform
63 // any checker-specific update of the state based on this assumption being
64 // true or false.
65 return StateMgr.getTransferFuncs().EvalAssume(StateMgr, St, Cond, Assumption,
66 isFeasible);
67}
68
69const GRState*
70SimpleConstraintManager::AssumeAux(const GRState* St, Loc Cond, bool Assumption,
71 bool& isFeasible) {
72 BasicValueFactory& BasicVals = StateMgr.getBasicVals();
73
74 switch (Cond.getSubKind()) {
75 default:
76 assert (false && "'Assume' not implemented for this Loc.");
77 return St;
78
79 case loc::SymbolValKind:
80 if (Assumption)
81 return AssumeSymNE(St, cast<loc::SymbolVal>(Cond).getSymbol(),
82 BasicVals.getZeroWithPtrWidth(), isFeasible);
83 else
84 return AssumeSymEQ(St, cast<loc::SymbolVal>(Cond).getSymbol(),
85 BasicVals.getZeroWithPtrWidth(), isFeasible);
86
87 case loc::MemRegionKind: {
88 // FIXME: Should this go into the storemanager?
89
90 const MemRegion* R = cast<loc::MemRegionVal>(Cond).getRegion();
91 const SubRegion* SubR = dyn_cast<SubRegion>(R);
92
93 while (SubR) {
94 // FIXME: now we only find the first symbolic region.
95 if (const SymbolicRegion* SymR = dyn_cast<SymbolicRegion>(SubR))
96 return AssumeAux(St, loc::SymbolVal(SymR->getSymbol()), Assumption,
97 isFeasible);
98 SubR = dyn_cast<SubRegion>(SubR->getSuperRegion());
99 }
100
101 // FALL-THROUGH.
102 }
103
104 case loc::FuncValKind:
105 case loc::GotoLabelKind:
106 isFeasible = Assumption;
107 return St;
108
109 case loc::ConcreteIntKind: {
110 bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0;
111 isFeasible = b ? Assumption : !Assumption;
112 return St;
113 }
114 } // end switch
115}
116
117const GRState*
118SimpleConstraintManager::Assume(const GRState* St, NonLoc Cond, bool Assumption,
119 bool& isFeasible) {
120 St = AssumeAux(St, Cond, Assumption, isFeasible);
121
122 if (!isFeasible)
123 return St;
124
125 // EvalAssume is used to call into the GRTransferFunction object to perform
126 // any checker-specific update of the state based on this assumption being
127 // true or false.
128 return StateMgr.getTransferFuncs().EvalAssume(StateMgr, St, Cond, Assumption,
129 isFeasible);
130}
131
132const GRState*
133SimpleConstraintManager::AssumeAux(const GRState* St,NonLoc Cond,
134 bool Assumption, bool& isFeasible) {
135 BasicValueFactory& BasicVals = StateMgr.getBasicVals();
136 SymbolManager& SymMgr = StateMgr.getSymbolManager();
137
138 switch (Cond.getSubKind()) {
139 default:
140 assert(false && "'Assume' not implemented for this NonLoc");
141
142 case nonloc::SymbolValKind: {
143 nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond);
144 SymbolRef sym = SV.getSymbol();
145 QualType T = SymMgr.getType(sym);
146
147 if (Assumption)
148 return AssumeSymNE(St, sym, BasicVals.getValue(0, T), isFeasible);
149 else
150 return AssumeSymEQ(St, sym, BasicVals.getValue(0, T), isFeasible);
151 }
152
153 case nonloc::SymIntConstraintValKind:
154 return
155 AssumeSymInt(St, Assumption,
156 cast<nonloc::SymIntConstraintVal>(Cond).getConstraint(),
157 isFeasible);
158
159 case nonloc::ConcreteIntKind: {
160 bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0;
161 isFeasible = b ? Assumption : !Assumption;
162 return St;
163 }
164
165 case nonloc::LocAsIntegerKind:
166 return AssumeAux(St, cast<nonloc::LocAsInteger>(Cond).getLoc(),
167 Assumption, isFeasible);
168 } // end switch
169}
170
171const GRState*
172SimpleConstraintManager::AssumeSymInt(const GRState* St, bool Assumption,
173 const SymIntConstraint& C,
174 bool& isFeasible) {
175
176 switch (C.getOpcode()) {
177 default:
178 // No logic yet for other operators.
179 isFeasible = true;
180 return St;
181
182 case BinaryOperator::EQ:
183 if (Assumption)
184 return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
185 else
186 return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
187
188 case BinaryOperator::NE:
189 if (Assumption)
190 return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
191 else
192 return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
193
194 case BinaryOperator::GT:
195 if (Assumption)
196 return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible);
197 else
198 return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
199
200 case BinaryOperator::GE:
201 if (Assumption)
202 return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
203 else
204 return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
205
206 case BinaryOperator::LT:
207 if (Assumption)
208 return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
209 else
210 return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
211
212 case BinaryOperator::LE:
213 if (Assumption)
214 return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
215 else
216 return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible);
217 } // end switch
218}
219
220const GRState*
221SimpleConstraintManager::AssumeInBound(const GRState* St, SVal Idx,
222 SVal UpperBound, bool Assumption,
223 bool& isFeasible) {
224 // Only support ConcreteInt for now.
225 if (!(isa<nonloc::ConcreteInt>(Idx) && isa<nonloc::ConcreteInt>(UpperBound))){
226 isFeasible = true;
227 return St;
228 }
229
230 const llvm::APSInt& Zero = getBasicVals().getZeroWithPtrWidth(false);
231 llvm::APSInt IdxV = cast<nonloc::ConcreteInt>(Idx).getValue();
232 // IdxV might be too narrow.
233 if (IdxV.getBitWidth() < Zero.getBitWidth())
234 IdxV.extend(Zero.getBitWidth());
235 // UBV might be too narrow, too.
236 llvm::APSInt UBV = cast<nonloc::ConcreteInt>(UpperBound).getValue();
237 if (UBV.getBitWidth() < Zero.getBitWidth())
238 UBV.extend(Zero.getBitWidth());
239
240 bool InBound = (Zero <= IdxV) && (IdxV < UBV);
241
242 isFeasible = Assumption ? InBound : !InBound;
243
244 return St;
245}
246
247} // end of namespace clang