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/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
17 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
23 SimpleConstraintManager::~SimpleConstraintManager() {}
25 bool SimpleConstraintManager::canReasonAbout(SVal X) const {
26 if (nonloc::SymExprVal *SymVal = dyn_cast<nonloc::SymExprVal>(&X)) {
27 const SymExpr *SE = SymVal->getSymbolicExpression();
29 if (isa<SymbolData>(SE))
32 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
33 switch (SIE->getOpcode()) {
34 // We don't reason yet about bitwise-constraints on symbolic values.
39 // We don't reason yet about these arithmetic constraints on
59 const ProgramState *SimpleConstraintManager::assume(const ProgramState *state,
62 if (isa<NonLoc>(Cond))
63 return assume(state, cast<NonLoc>(Cond), Assumption);
65 return assume(state, cast<Loc>(Cond), Assumption);
68 const ProgramState *SimpleConstraintManager::assume(const ProgramState *state, Loc cond,
70 state = assumeAux(state, cond, assumption);
71 return SU.processAssume(state, cond, assumption);
74 const ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *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)) {
93 const llvm::APSInt &zero = BasicVals.getZeroWithPtrWidth();
95 return assumeSymNE(state, SymR->getSymbol(), zero, zero);
97 return assumeSymEQ(state, SymR->getSymbol(), zero, zero);
99 SubR = dyn_cast<SubRegion>(SubR->getSuperRegion());
105 case loc::GotoLabelKind:
106 return Assumption ? state : NULL;
108 case loc::ConcreteIntKind: {
109 bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0;
110 bool isFeasible = b ? Assumption : !Assumption;
111 return isFeasible ? state : NULL;
116 const ProgramState *SimpleConstraintManager::assume(const ProgramState *state,
119 state = assumeAux(state, cond, assumption);
120 return SU.processAssume(state, cond, assumption);
123 static BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) {
124 // FIXME: This should probably be part of BinaryOperator, since this isn't
125 // the only place it's used. (This code was copied from SimpleSValBuilder.cpp.)
128 llvm_unreachable("Invalid opcode.");
129 case BO_LT: return BO_GE;
130 case BO_GT: return BO_LE;
131 case BO_LE: return BO_GT;
132 case BO_GE: return BO_LT;
133 case BO_EQ: return BO_NE;
134 case BO_NE: return BO_EQ;
138 const ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *state,
142 // We cannot reason about SymSymExprs,
143 // and can only reason about some SymIntExprs.
144 if (!canReasonAbout(Cond)) {
145 // Just return the current state indicating that the path is feasible.
146 // This may be an over-approximation of what is possible.
150 BasicValueFactory &BasicVals = state->getBasicVals();
151 SymbolManager &SymMgr = state->getSymbolManager();
153 switch (Cond.getSubKind()) {
155 llvm_unreachable("'Assume' not implemented for this NonLoc");
157 case nonloc::SymbolValKind: {
158 nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond);
159 SymbolRef sym = SV.getSymbol();
160 QualType T = SymMgr.getType(sym);
161 const llvm::APSInt &zero = BasicVals.getValue(0, T);
163 return assumeSymNE(state, sym, zero, zero);
165 return assumeSymEQ(state, sym, zero, zero);
168 case nonloc::SymExprValKind: {
169 nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond);
171 // For now, we only handle expressions whose RHS is an integer.
172 // All other expressions are assumed to be feasible.
173 const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression());
177 BinaryOperator::Opcode op = SE->getOpcode();
178 // Implicitly compare non-comparison expressions to 0.
179 if (!BinaryOperator::isComparisonOp(op)) {
180 QualType T = SymMgr.getType(SE);
181 const llvm::APSInt &zero = BasicVals.getValue(0, T);
182 op = (Assumption ? BO_NE : BO_EQ);
183 return assumeSymRel(state, SE, op, zero);
186 // From here on out, op is the real comparison we'll be testing.
188 op = NegateComparison(op);
190 return assumeSymRel(state, SE->getLHS(), op, SE->getRHS());
193 case nonloc::ConcreteIntKind: {
194 bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0;
195 bool isFeasible = b ? Assumption : !Assumption;
196 return isFeasible ? state : NULL;
199 case nonloc::LocAsIntegerKind:
200 return assumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(),
205 const ProgramState *SimpleConstraintManager::assumeSymRel(const ProgramState *state,
207 BinaryOperator::Opcode op,
208 const llvm::APSInt& Int) {
209 assert(BinaryOperator::isComparisonOp(op) &&
210 "Non-comparison ops should be rewritten as comparisons to zero.");
212 // We only handle simple comparisons of the form "$sym == constant"
213 // or "($sym+constant1) == constant2".
214 // The adjustment is "constant1" in the above expression. It's used to
215 // "slide" the solution range around for modular arithmetic. For example,
216 // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
217 // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
218 // the subclasses of SimpleConstraintManager to handle the adjustment.
219 llvm::APSInt Adjustment;
221 // First check if the LHS is a simple symbol reference.
222 SymbolRef Sym = dyn_cast<SymbolData>(LHS);
226 // Next, see if it's a "($sym+constant1)" expression.
227 const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS);
229 // We don't handle "($sym1+$sym2)".
230 // Give up and assume the constraint is feasible.
234 // We don't handle "(<expr>+constant1)".
235 // Give up and assume the constraint is feasible.
236 Sym = dyn_cast<SymbolData>(SE->getLHS());
240 // Get the constant out of the expression "($sym+constant1)".
241 switch (SE->getOpcode()) {
243 Adjustment = SE->getRHS();
246 Adjustment = -SE->getRHS();
249 // We don't handle non-additive operators.
250 // Give up and assume the constraint is feasible.
255 // FIXME: This next section is a hack. It silently converts the integers to
256 // be of the same type as the symbol, which is not always correct. Really the
257 // comparisons should be performed using the Int's type, then mapped back to
258 // the symbol's range of values.
259 ProgramStateManager &StateMgr = state->getStateManager();
260 ASTContext &Ctx = StateMgr.getContext();
262 QualType T = Sym->getType(Ctx);
263 assert(T->isIntegerType() || Loc::isLocType(T));
264 unsigned bitwidth = Ctx.getTypeSize(T);
266 = T->isUnsignedIntegerOrEnumerationType() || Loc::isLocType(T);
268 // Convert the adjustment.
269 Adjustment.setIsUnsigned(isSymUnsigned);
270 Adjustment = Adjustment.extOrTrunc(bitwidth);
272 // Convert the right-hand side integer.
273 llvm::APSInt ConvertedInt(Int, isSymUnsigned);
274 ConvertedInt = ConvertedInt.extOrTrunc(bitwidth);
278 // No logic yet for other operators. assume the constraint is feasible.
282 return assumeSymEQ(state, Sym, ConvertedInt, Adjustment);
285 return assumeSymNE(state, Sym, ConvertedInt, Adjustment);
288 return assumeSymGT(state, Sym, ConvertedInt, Adjustment);
291 return assumeSymGE(state, Sym, ConvertedInt, Adjustment);
294 return assumeSymLT(state, Sym, ConvertedInt, Adjustment);
297 return assumeSymLE(state, Sym, ConvertedInt, Adjustment);
301 } // end of namespace ento
303 } // end of namespace clang