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/APSIntType.h"
17 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
18 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
24 SimpleConstraintManager::~SimpleConstraintManager() {}
26 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();
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.
38 // We don't reason yet about these arithmetic constraints on
52 if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
53 if (BinaryOperator::isComparisonOp(SSE->getOpcode())) {
54 // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
55 if (Loc::isLocType(SSE->getLHS()->getType())) {
56 assert(Loc::isLocType(SSE->getRHS()->getType()));
68 ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
71 if (Optional<NonLoc> NV = Cond.getAs<NonLoc>())
72 return assume(state, *NV, Assumption);
73 return assume(state, Cond.castAs<Loc>(), Assumption);
76 ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, Loc cond,
78 state = assumeAux(state, cond, assumption);
79 if (NotifyAssumeClients && SU)
80 return SU->processAssume(state, cond, assumption);
84 ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
85 Loc Cond, bool Assumption) {
86 switch (Cond.getSubKind()) {
88 assert (false && "'Assume' not implemented for this Loc.");
91 case loc::MemRegionKind: {
92 // FIXME: Should this go into the storemanager?
93 const MemRegion *R = Cond.castAs<loc::MemRegionVal>().getRegion();
95 // FIXME: now we only find the first symbolic region.
96 if (const SymbolicRegion *SymR = R->getSymbolicBase()) {
97 const llvm::APSInt &zero = getBasicVals().getZeroWithPtrWidth();
99 return assumeSymNE(state, SymR->getSymbol(), zero, zero);
101 return assumeSymEQ(state, SymR->getSymbol(), zero, zero);
107 case loc::GotoLabelKind:
108 return Assumption ? state : NULL;
110 case loc::ConcreteIntKind: {
111 bool b = Cond.castAs<loc::ConcreteInt>().getValue() != 0;
112 bool isFeasible = b ? Assumption : !Assumption;
113 return isFeasible ? state : NULL;
118 ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
121 state = assumeAux(state, cond, assumption);
122 if (NotifyAssumeClients && SU)
123 return SU->processAssume(state, cond, assumption);
129 SimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State,
130 SymbolRef Sym, bool Assumption) {
131 BasicValueFactory &BVF = getBasicVals();
132 QualType T = Sym->getType();
134 // None of the constraint solvers currently support non-integer types.
135 if (!T->isIntegralOrEnumerationType())
138 const llvm::APSInt &zero = BVF.getValue(0, T);
140 return assumeSymNE(State, Sym, zero, zero);
142 return assumeSymEQ(State, Sym, zero, zero);
145 ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
149 // We cannot reason about SymSymExprs, and can only reason about some
151 if (!canReasonAbout(Cond)) {
152 // Just add the constraint to the expression without trying to simplify.
153 SymbolRef sym = Cond.getAsSymExpr();
154 return assumeAuxForSymbol(state, sym, Assumption);
157 switch (Cond.getSubKind()) {
159 llvm_unreachable("'Assume' not implemented for this NonLoc");
161 case nonloc::SymbolValKind: {
162 nonloc::SymbolVal SV = Cond.castAs<nonloc::SymbolVal>();
163 SymbolRef sym = SV.getSymbol();
166 // Handle SymbolData.
167 if (!SV.isExpression()) {
168 return assumeAuxForSymbol(state, sym, Assumption);
170 // Handle symbolic expression.
171 } else if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym)) {
172 // We can only simplify expressions whose RHS is an integer.
174 BinaryOperator::Opcode op = SE->getOpcode();
175 if (BinaryOperator::isComparisonOp(op)) {
177 op = BinaryOperator::negateComparisonOp(op);
179 return assumeSymRel(state, SE->getLHS(), op, SE->getRHS());
182 } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(sym)) {
183 // Translate "a != b" to "(b - a) != 0".
184 // We invert the order of the operands as a heuristic for how loop
185 // conditions are usually written ("begin != end") as compared to length
186 // calculations ("end - begin"). The more correct thing to do would be to
187 // canonicalize "a - b" and "b - a", which would allow us to treat
188 // "a != b" and "b != a" the same.
189 SymbolManager &SymMgr = getSymbolManager();
190 BinaryOperator::Opcode Op = SSE->getOpcode();
191 assert(BinaryOperator::isComparisonOp(Op));
193 // For now, we only support comparing pointers.
194 assert(Loc::isLocType(SSE->getLHS()->getType()));
195 assert(Loc::isLocType(SSE->getRHS()->getType()));
196 QualType DiffTy = SymMgr.getContext().getPointerDiffType();
197 SymbolRef Subtraction = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub,
198 SSE->getLHS(), DiffTy);
200 const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy);
201 Op = BinaryOperator::reverseComparisonOp(Op);
203 Op = BinaryOperator::negateComparisonOp(Op);
204 return assumeSymRel(state, Subtraction, Op, Zero);
207 // If we get here, there's nothing else we can do but treat the symbol as
209 return assumeAuxForSymbol(state, sym, Assumption);
212 case nonloc::ConcreteIntKind: {
213 bool b = Cond.castAs<nonloc::ConcreteInt>().getValue() != 0;
214 bool isFeasible = b ? Assumption : !Assumption;
215 return isFeasible ? state : NULL;
218 case nonloc::LocAsIntegerKind:
219 return assumeAux(state, Cond.castAs<nonloc::LocAsInteger>().getLoc(),
224 static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) {
225 // Is it a "($sym+constant1)" expression?
226 if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
227 BinaryOperator::Opcode Op = SE->getOpcode();
228 if (Op == BO_Add || Op == BO_Sub) {
230 Adjustment = APSIntType(Adjustment).convert(SE->getRHS());
232 // Don't forget to negate the adjustment if it's being subtracted.
233 // This should happen /after/ promotion, in case the value being
234 // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
236 Adjustment = -Adjustment;
241 ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state,
243 BinaryOperator::Opcode op,
244 const llvm::APSInt& Int) {
245 assert(BinaryOperator::isComparisonOp(op) &&
246 "Non-comparison ops should be rewritten as comparisons to zero.");
248 // Get the type used for calculating wraparound.
249 BasicValueFactory &BVF = getBasicVals();
250 APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType());
252 // We only handle simple comparisons of the form "$sym == constant"
253 // or "($sym+constant1) == constant2".
254 // The adjustment is "constant1" in the above expression. It's used to
255 // "slide" the solution range around for modular arithmetic. For example,
256 // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
257 // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
258 // the subclasses of SimpleConstraintManager to handle the adjustment.
260 llvm::APSInt Adjustment = WraparoundType.getZeroValue();
261 computeAdjustment(Sym, Adjustment);
263 // Convert the right-hand side integer as necessary.
264 APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int));
265 llvm::APSInt ConvertedInt = ComparisonType.convert(Int);
267 // Prefer unsigned comparisons.
268 if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
269 ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
270 Adjustment.setIsSigned(false);
274 llvm_unreachable("invalid operation not caught by assertion above");
277 return assumeSymEQ(state, Sym, ConvertedInt, Adjustment);
280 return assumeSymNE(state, Sym, ConvertedInt, Adjustment);
283 return assumeSymGT(state, Sym, ConvertedInt, Adjustment);
286 return assumeSymGE(state, Sym, ConvertedInt, Adjustment);
289 return assumeSymLT(state, Sym, ConvertedInt, Adjustment);
292 return assumeSymLE(state, Sym, ConvertedInt, Adjustment);
296 } // end of namespace ento
298 } // end of namespace clang