1//== RangedConstraintManager.cpp --------------------------------*- C++ -*--==//
2//
3// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4// See https://llvm.org/LICENSE.txt for license information.
5// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6//
7//===----------------------------------------------------------------------===//
8//
9// This file defines RangedConstraintManager, a class that provides a
10// range-based constraint manager interface.
11//
12//===----------------------------------------------------------------------===//
13
14#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
15#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
16
17namespace clang {
18
19namespace ento {
20
21RangedConstraintManager::~RangedConstraintManager() {}
22
23/// Is \p Assumption (i.e. "the condition is non-zero") inconsistent with a
24/// symbol that simplified to the concrete integer \p V?
25static bool isConcreteInfeasible(const llvm::APSInt &V, bool Assumption) {
26 return (V != 0) ? !Assumption : Assumption;
27}
28
29ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
30 SymbolRef Sym,
31 bool Assumption) {
32 SVal SimplifiedVal = simplifyToSVal(State, Sym);
33 if (const auto *CI = SimplifiedVal.getAsInteger()) {
34 // The assumption might be incompatible with the concrete integer after the
35 // simplification.
36 if (isConcreteInfeasible(V: *CI, Assumption))
37 return nullptr;
38 // When the fold is feasible we deliberately do NOT return early: we fall
39 // through and record the constraint on the *original* symbol. That is not a
40 // no-op -- it is how the symbol-simplification fixpoint migrates a
41 // constraint onto a just-simplified symbol. See an example in
42 // symbol-simplification-fixpoint-two-iterations.cpp.
43 } else if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol()) {
44 Sym = SimplifiedSym;
45 }
46
47 // Handle SymbolData.
48 if (isa<SymbolData>(Val: Sym))
49 return assumeSymUnsupported(State, Sym, Assumption);
50
51 // Handle symbolic expression.
52 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Val: Sym)) {
53 // We can only simplify expressions whose RHS is an integer.
54
55 BinaryOperator::Opcode op = SIE->getOpcode();
56 if (BinaryOperator::isComparisonOp(Opc: op) && op != BO_Cmp) {
57 if (!Assumption)
58 op = BinaryOperator::negateComparisonOp(Opc: op);
59
60 return assumeSymRel(State, Sym: SIE->getLHS(), op, Int: SIE->getRHS());
61 }
62
63 // Handle adjustment with non-comparison ops.
64 const llvm::APSInt &Zero = getBasicVals().getValue(X: 0, T: SIE->getType());
65 return assumeSymRel(State, Sym: SIE, op: (Assumption ? BO_NE : BO_EQ), Int: Zero);
66 }
67
68 if (const auto *SSE = dyn_cast<SymSymExpr>(Val: Sym)) {
69 BinaryOperator::Opcode Op = SSE->getOpcode();
70 if (BinaryOperator::isComparisonOp(Opc: Op)) {
71
72 // We convert equality operations for pointers only.
73 if (Loc::isLocType(T: SSE->getLHS()->getType()) &&
74 Loc::isLocType(T: SSE->getRHS()->getType())) {
75 // Translate "a != b" to "(b - a) != 0".
76 // We invert the order of the operands as a heuristic for how loop
77 // conditions are usually written ("begin != end") as compared to length
78 // calculations ("end - begin"). The more correct thing to do would be
79 // to canonicalize "a - b" and "b - a", which would allow us to treat
80 // "a != b" and "b != a" the same.
81
82 SymbolManager &SymMgr = getSymbolManager();
83 QualType DiffTy = SymMgr.getContext().getPointerDiffType();
84 SymbolRef Subtraction = SymMgr.acquire<SymSymExpr>(
85 args: SSE->getRHS(), args: BO_Sub, args: SSE->getLHS(), args&: DiffTy);
86
87 const llvm::APSInt &Zero = getBasicVals().getValue(X: 0, T: DiffTy);
88 Op = BinaryOperator::reverseComparisonOp(Opc: Op);
89 if (!Assumption)
90 Op = BinaryOperator::negateComparisonOp(Opc: Op);
91 return assumeSymRel(State, Sym: Subtraction, op: Op, Int: Zero);
92 }
93
94 if (BinaryOperator::isEqualityOp(Opc: Op)) {
95 SymbolManager &SymMgr = getSymbolManager();
96
97 QualType ExprType = SSE->getType();
98 SymbolRef CanonicalEquality = SymMgr.acquire<SymSymExpr>(
99 args: SSE->getLHS(), args: BO_EQ, args: SSE->getRHS(), args&: ExprType);
100
101 bool WasEqual = SSE->getOpcode() == BO_EQ;
102 bool IsExpectedEqual = WasEqual == Assumption;
103
104 const llvm::APSInt &Zero = getBasicVals().getValue(X: 0, T: ExprType);
105
106 if (IsExpectedEqual) {
107 return assumeSymNE(State, Sym: CanonicalEquality, V: Zero, Adjustment: Zero);
108 }
109
110 return assumeSymEQ(State, Sym: CanonicalEquality, V: Zero, Adjustment: Zero);
111 }
112 }
113 }
114
115 // If we get here, there's nothing else we can do but treat the symbol as
116 // opaque.
117 return assumeSymUnsupported(State, Sym, Assumption);
118}
119
120ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(
121 ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
122 const llvm::APSInt &To, bool InRange) {
123
124 SVal SimplifiedVal = simplifyToSVal(State, Sym);
125 if (const auto *CI = SimplifiedVal.getAsInteger()) {
126 // The symbol folds to a concrete integer. Prune the path only when the
127 // concrete value proves it infeasible (mirroring
128 // SimpleConstraintManager::assumeInclusiveRangeInternal). If it is
129 // consistent, fall through so the existing machinery still runs it might
130 // trigger further simplification even if this assumption is trivial.
131 bool IsInRange = llvm::APSInt::compareValues(I1: *CI, I2: From) >= 0 &&
132 llvm::APSInt::compareValues(I1: *CI, I2: To) <= 0;
133 if (IsInRange != InRange)
134 return nullptr;
135 } else if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol()) {
136 Sym = SimplifiedSym;
137 }
138
139 // Get the type used for calculating wraparound.
140 BasicValueFactory &BVF = getBasicVals();
141 APSIntType WraparoundType = BVF.getAPSIntType(T: Sym->getType());
142
143 llvm::APSInt Adjustment = WraparoundType.getZeroValue();
144 SymbolRef AdjustedSym = Sym;
145 computeAdjustment(Sym&: AdjustedSym, Adjustment);
146
147 // Convert the right-hand side integer as necessary.
148 APSIntType ComparisonType = std::max(a: WraparoundType, b: APSIntType(From));
149 llvm::APSInt ConvertedFrom = ComparisonType.convert(Value: From);
150 llvm::APSInt ConvertedTo = ComparisonType.convert(Value: To);
151
152 // Prefer unsigned comparisons.
153 if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
154 ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
155 Adjustment.setIsSigned(false);
156
157 if (InRange)
158 return assumeSymWithinInclusiveRange(State, Sym: AdjustedSym, From: ConvertedFrom,
159 To: ConvertedTo, Adjustment);
160 return assumeSymOutsideInclusiveRange(State, Sym: AdjustedSym, From: ConvertedFrom,
161 To: ConvertedTo, Adjustment);
162}
163
164ProgramStateRef
165RangedConstraintManager::assumeSymUnsupported(ProgramStateRef State,
166 SymbolRef Sym, bool Assumption) {
167 SVal SimplifiedVal = simplifyToSVal(State, Sym);
168 if (const auto *CI = SimplifiedVal.getAsInteger()) {
169 // Prune only when the concrete fold contradicts the assumption. When it is
170 // consistent we fall through and record the constraint on the original
171 // symbol (assumeSymNE/EQ below) rather than returning early to continue
172 // constraint simplification.
173 if (isConcreteInfeasible(V: *CI, Assumption))
174 return nullptr;
175 } else if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol()) {
176 Sym = SimplifiedSym;
177 }
178
179 BasicValueFactory &BVF = getBasicVals();
180 QualType T = Sym->getType();
181
182 // Non-integer types are not supported.
183 if (!T->isIntegralOrEnumerationType())
184 return State;
185
186 // Reverse the operation and add directly to state.
187 const llvm::APSInt &Zero = BVF.getValue(X: 0, T);
188 if (Assumption)
189 return assumeSymNE(State, Sym, V: Zero, Adjustment: Zero);
190 else
191 return assumeSymEQ(State, Sym, V: Zero, Adjustment: Zero);
192}
193
194ProgramStateRef RangedConstraintManager::assumeSymRel(ProgramStateRef State,
195 SymbolRef Sym,
196 BinaryOperator::Opcode Op,
197 const llvm::APSInt &Int) {
198 assert(BinaryOperator::isComparisonOp(Op) &&
199 "Non-comparison ops should be rewritten as comparisons to zero.");
200
201 // Simplification: translate an assume of a constraint of the form
202 // "(exp comparison_op expr) != 0" to true into an assume of
203 // "exp comparison_op expr" to true. (And similarly, an assume of the form
204 // "(exp comparison_op expr) == 0" to true into an assume of
205 // "exp comparison_op expr" to false.)
206 if (Int == 0 && (Op == BO_EQ || Op == BO_NE)) {
207 if (const BinarySymExpr *SE = dyn_cast<BinarySymExpr>(Val: Sym))
208 if (BinaryOperator::isComparisonOp(Opc: SE->getOpcode()))
209 return assumeSym(State, Sym, Assumption: (Op == BO_NE ? true : false));
210 }
211
212 // Get the type used for calculating wraparound.
213 BasicValueFactory &BVF = getBasicVals();
214 APSIntType WraparoundType = BVF.getAPSIntType(T: Sym->getType());
215
216 // We only handle simple comparisons of the form "$sym == constant"
217 // or "($sym+constant1) == constant2".
218 // The adjustment is "constant1" in the above expression. It's used to
219 // "slide" the solution range around for modular arithmetic. For example,
220 // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
221 // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
222 // the subclasses of SimpleConstraintManager to handle the adjustment.
223 llvm::APSInt Adjustment = WraparoundType.getZeroValue();
224 computeAdjustment(Sym, Adjustment);
225
226 // Convert the right-hand side integer as necessary.
227 APSIntType ComparisonType = std::max(a: WraparoundType, b: APSIntType(Int));
228 llvm::APSInt ConvertedInt = ComparisonType.convert(Value: Int);
229
230 // Prefer unsigned comparisons.
231 if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
232 ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
233 Adjustment.setIsSigned(false);
234
235 switch (Op) {
236 default:
237 llvm_unreachable("invalid operation not caught by assertion above");
238
239 case BO_EQ:
240 return assumeSymEQ(State, Sym, V: ConvertedInt, Adjustment);
241
242 case BO_NE:
243 return assumeSymNE(State, Sym, V: ConvertedInt, Adjustment);
244
245 case BO_GT:
246 return assumeSymGT(State, Sym, V: ConvertedInt, Adjustment);
247
248 case BO_GE:
249 return assumeSymGE(State, Sym, V: ConvertedInt, Adjustment);
250
251 case BO_LT:
252 return assumeSymLT(State, Sym, V: ConvertedInt, Adjustment);
253
254 case BO_LE:
255 return assumeSymLE(State, Sym, V: ConvertedInt, Adjustment);
256 } // end switch
257}
258
259void RangedConstraintManager::computeAdjustment(SymbolRef &Sym,
260 llvm::APSInt &Adjustment) {
261 // Is it a "($sym+constant1)" expression?
262 if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Val: Sym)) {
263 BinaryOperator::Opcode Op = SE->getOpcode();
264 if (Op == BO_Add || Op == BO_Sub) {
265 Sym = SE->getLHS();
266 Adjustment = APSIntType(Adjustment).convert(Value: SE->getRHS());
267
268 // Don't forget to negate the adjustment if it's being subtracted.
269 // This should happen /after/ promotion, in case the value being
270 // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
271 if (Op == BO_Sub)
272 Adjustment = -Adjustment;
273 }
274 }
275}
276
277SVal simplifyToSVal(ProgramStateRef State, SymbolRef Sym) {
278 SValBuilder &SVB = State->getStateManager().getSValBuilder();
279 return SVB.simplifySVal(State, Val: SVB.makeSymbolVal(Sym));
280}
281
282} // end of namespace ento
283} // end of namespace clang
284