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/GR/PathSensitive/GRExprEngine.h"
17 #include "clang/GR/PathSensitive/GRState.h"
18 #include "clang/GR/PathSensitive/Checker.h"
24 SimpleConstraintManager::~SimpleConstraintManager() {}
26 bool SimpleConstraintManager::canReasonAbout(SVal X
) const {
27 if (nonloc::SymExprVal
*SymVal
= dyn_cast
<nonloc::SymExprVal
>(&X
)) {
28 const SymExpr
*SE
= SymVal
->getSymbolicExpression();
30 if (isa
<SymbolData
>(SE
))
33 if (const SymIntExpr
*SIE
= dyn_cast
<SymIntExpr
>(SE
)) {
34 switch (SIE
->getOpcode()) {
35 // We don't reason yet about bitwise-constraints on symbolic values.
40 // We don't reason yet about these arithmetic constraints on
60 const GRState
*SimpleConstraintManager::assume(const GRState
*state
,
63 if (isa
<NonLoc
>(Cond
))
64 return assume(state
, cast
<NonLoc
>(Cond
), Assumption
);
66 return assume(state
, cast
<Loc
>(Cond
), Assumption
);
69 const GRState
*SimpleConstraintManager::assume(const GRState
*state
, Loc cond
,
71 state
= assumeAux(state
, cond
, assumption
);
72 return SU
.ProcessAssume(state
, cond
, assumption
);
75 const GRState
*SimpleConstraintManager::assumeAux(const GRState
*state
,
76 Loc Cond
, bool Assumption
) {
78 BasicValueFactory
&BasicVals
= state
->getBasicVals();
80 switch (Cond
.getSubKind()) {
82 assert (false && "'Assume' not implemented for this Loc.");
85 case loc::MemRegionKind
: {
86 // FIXME: Should this go into the storemanager?
88 const MemRegion
*R
= cast
<loc::MemRegionVal
>(Cond
).getRegion();
89 const SubRegion
*SubR
= dyn_cast
<SubRegion
>(R
);
92 // FIXME: now we only find the first symbolic region.
93 if (const SymbolicRegion
*SymR
= dyn_cast
<SymbolicRegion
>(SubR
)) {
94 const llvm::APSInt
&zero
= BasicVals
.getZeroWithPtrWidth();
96 return assumeSymNE(state
, SymR
->getSymbol(), zero
, zero
);
98 return assumeSymEQ(state
, SymR
->getSymbol(), zero
, zero
);
100 SubR
= dyn_cast
<SubRegion
>(SubR
->getSuperRegion());
106 case loc::GotoLabelKind
:
107 return Assumption
? state
: NULL
;
109 case loc::ConcreteIntKind
: {
110 bool b
= cast
<loc::ConcreteInt
>(Cond
).getValue() != 0;
111 bool isFeasible
= b
? Assumption
: !Assumption
;
112 return isFeasible
? state
: NULL
;
117 const GRState
*SimpleConstraintManager::assume(const GRState
*state
,
120 state
= assumeAux(state
, cond
, assumption
);
121 return SU
.ProcessAssume(state
, cond
, assumption
);
124 static BinaryOperator::Opcode
NegateComparison(BinaryOperator::Opcode op
) {
125 // FIXME: This should probably be part of BinaryOperator, since this isn't
126 // the only place it's used. (This code was copied from SimpleSValBuilder.cpp.)
129 assert(false && "Invalid opcode.");
130 case BO_LT
: return BO_GE
;
131 case BO_GT
: return BO_LE
;
132 case BO_LE
: return BO_GT
;
133 case BO_GE
: return BO_LT
;
134 case BO_EQ
: return BO_NE
;
135 case BO_NE
: return BO_EQ
;
139 const GRState
*SimpleConstraintManager::assumeAux(const GRState
*state
,
143 // We cannot reason about SymSymExprs,
144 // and can only reason about some SymIntExprs.
145 if (!canReasonAbout(Cond
)) {
146 // Just return the current state indicating that the path is feasible.
147 // This may be an over-approximation of what is possible.
151 BasicValueFactory
&BasicVals
= state
->getBasicVals();
152 SymbolManager
&SymMgr
= state
->getSymbolManager();
154 switch (Cond
.getSubKind()) {
156 assert(false && "'Assume' not implemented for this NonLoc");
158 case nonloc::SymbolValKind
: {
159 nonloc::SymbolVal
& SV
= cast
<nonloc::SymbolVal
>(Cond
);
160 SymbolRef sym
= SV
.getSymbol();
161 QualType T
= SymMgr
.getType(sym
);
162 const llvm::APSInt
&zero
= BasicVals
.getValue(0, T
);
164 return assumeSymNE(state
, sym
, zero
, zero
);
166 return assumeSymEQ(state
, sym
, zero
, zero
);
169 case nonloc::SymExprValKind
: {
170 nonloc::SymExprVal V
= cast
<nonloc::SymExprVal
>(Cond
);
172 // For now, we only handle expressions whose RHS is an integer.
173 // All other expressions are assumed to be feasible.
174 const SymIntExpr
*SE
= dyn_cast
<SymIntExpr
>(V
.getSymbolicExpression());
178 BinaryOperator::Opcode op
= SE
->getOpcode();
179 // Implicitly compare non-comparison expressions to 0.
180 if (!BinaryOperator::isComparisonOp(op
)) {
181 QualType T
= SymMgr
.getType(SE
);
182 const llvm::APSInt
&zero
= BasicVals
.getValue(0, T
);
183 op
= (Assumption
? BO_NE
: BO_EQ
);
184 return assumeSymRel(state
, SE
, op
, zero
);
187 // From here on out, op is the real comparison we'll be testing.
189 op
= NegateComparison(op
);
191 return assumeSymRel(state
, SE
->getLHS(), op
, SE
->getRHS());
194 case nonloc::ConcreteIntKind
: {
195 bool b
= cast
<nonloc::ConcreteInt
>(Cond
).getValue() != 0;
196 bool isFeasible
= b
? Assumption
: !Assumption
;
197 return isFeasible
? state
: NULL
;
200 case nonloc::LocAsIntegerKind
:
201 return assumeAux(state
, cast
<nonloc::LocAsInteger
>(Cond
).getLoc(),
206 const GRState
*SimpleConstraintManager::assumeSymRel(const GRState
*state
,
208 BinaryOperator::Opcode op
,
209 const llvm::APSInt
& Int
) {
210 assert(BinaryOperator::isComparisonOp(op
) &&
211 "Non-comparison ops should be rewritten as comparisons to zero.");
213 // We only handle simple comparisons of the form "$sym == constant"
214 // or "($sym+constant1) == constant2".
215 // The adjustment is "constant1" in the above expression. It's used to
216 // "slide" the solution range around for modular arithmetic. For example,
217 // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
218 // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
219 // the subclasses of SimpleConstraintManager to handle the adjustment.
220 llvm::APSInt Adjustment
;
222 // First check if the LHS is a simple symbol reference.
223 SymbolRef Sym
= dyn_cast
<SymbolData
>(LHS
);
227 // Next, see if it's a "($sym+constant1)" expression.
228 const SymIntExpr
*SE
= dyn_cast
<SymIntExpr
>(LHS
);
230 // We don't handle "($sym1+$sym2)".
231 // Give up and assume the constraint is feasible.
235 // We don't handle "(<expr>+constant1)".
236 // Give up and assume the constraint is feasible.
237 Sym
= dyn_cast
<SymbolData
>(SE
->getLHS());
241 // Get the constant out of the expression "($sym+constant1)".
242 switch (SE
->getOpcode()) {
244 Adjustment
= SE
->getRHS();
247 Adjustment
= -SE
->getRHS();
250 // We don't handle non-additive operators.
251 // Give up and assume the constraint is feasible.
256 // FIXME: This next section is a hack. It silently converts the integers to
257 // be of the same type as the symbol, which is not always correct. Really the
258 // comparisons should be performed using the Int's type, then mapped back to
259 // the symbol's range of values.
260 GRStateManager
&StateMgr
= state
->getStateManager();
261 ASTContext
&Ctx
= StateMgr
.getContext();
263 QualType T
= Sym
->getType(Ctx
);
264 assert(T
->isIntegerType() || Loc::IsLocType(T
));
265 unsigned bitwidth
= Ctx
.getTypeSize(T
);
266 bool isSymUnsigned
= T
->isUnsignedIntegerType() || 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 GR
303 } // end of namespace clang