1 //== RangedConstraintManager.cpp --------------------------------*- C++ -*--==//
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
7 //===----------------------------------------------------------------------===//
9 // This file defines RangedConstraintManager, a class that provides a
10 // range-based constraint manager interface.
12 //===----------------------------------------------------------------------===//
14 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
15 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
21 RangedConstraintManager::~RangedConstraintManager() {}
23 ProgramStateRef
RangedConstraintManager::assumeSym(ProgramStateRef State
,
26 Sym
= simplify(State
, Sym
);
29 if (isa
<SymbolData
>(Sym
))
30 return assumeSymUnsupported(State
, Sym
, Assumption
);
32 // Handle symbolic expression.
33 if (const SymIntExpr
*SIE
= dyn_cast
<SymIntExpr
>(Sym
)) {
34 // We can only simplify expressions whose RHS is an integer.
36 BinaryOperator::Opcode op
= SIE
->getOpcode();
37 if (BinaryOperator::isComparisonOp(op
) && op
!= BO_Cmp
) {
39 op
= BinaryOperator::negateComparisonOp(op
);
41 return assumeSymRel(State
, SIE
->getLHS(), op
, SIE
->getRHS());
44 // Handle adjustment with non-comparison ops.
45 const llvm::APSInt
&Zero
= getBasicVals().getValue(0, SIE
->getType());
46 return assumeSymRel(State
, SIE
, (Assumption
? BO_NE
: BO_EQ
), Zero
);
49 if (const auto *SSE
= dyn_cast
<SymSymExpr
>(Sym
)) {
50 BinaryOperator::Opcode Op
= SSE
->getOpcode();
51 if (BinaryOperator::isComparisonOp(Op
)) {
53 // We convert equality operations for pointers only.
54 if (Loc::isLocType(SSE
->getLHS()->getType()) &&
55 Loc::isLocType(SSE
->getRHS()->getType())) {
56 // Translate "a != b" to "(b - a) != 0".
57 // We invert the order of the operands as a heuristic for how loop
58 // conditions are usually written ("begin != end") as compared to length
59 // calculations ("end - begin"). The more correct thing to do would be
60 // to canonicalize "a - b" and "b - a", which would allow us to treat
61 // "a != b" and "b != a" the same.
63 SymbolManager
&SymMgr
= getSymbolManager();
64 QualType DiffTy
= SymMgr
.getContext().getPointerDiffType();
65 SymbolRef Subtraction
=
66 SymMgr
.getSymSymExpr(SSE
->getRHS(), BO_Sub
, SSE
->getLHS(), DiffTy
);
68 const llvm::APSInt
&Zero
= getBasicVals().getValue(0, DiffTy
);
69 Op
= BinaryOperator::reverseComparisonOp(Op
);
71 Op
= BinaryOperator::negateComparisonOp(Op
);
72 return assumeSymRel(State
, Subtraction
, Op
, Zero
);
75 if (BinaryOperator::isEqualityOp(Op
)) {
76 SymbolManager
&SymMgr
= getSymbolManager();
78 QualType ExprType
= SSE
->getType();
79 SymbolRef CanonicalEquality
=
80 SymMgr
.getSymSymExpr(SSE
->getLHS(), BO_EQ
, SSE
->getRHS(), ExprType
);
82 bool WasEqual
= SSE
->getOpcode() == BO_EQ
;
83 bool IsExpectedEqual
= WasEqual
== Assumption
;
85 const llvm::APSInt
&Zero
= getBasicVals().getValue(0, ExprType
);
87 if (IsExpectedEqual
) {
88 return assumeSymNE(State
, CanonicalEquality
, Zero
, Zero
);
91 return assumeSymEQ(State
, CanonicalEquality
, Zero
, Zero
);
96 // If we get here, there's nothing else we can do but treat the symbol as
98 return assumeSymUnsupported(State
, Sym
, Assumption
);
101 ProgramStateRef
RangedConstraintManager::assumeSymInclusiveRange(
102 ProgramStateRef State
, SymbolRef Sym
, const llvm::APSInt
&From
,
103 const llvm::APSInt
&To
, bool InRange
) {
105 Sym
= simplify(State
, Sym
);
107 // Get the type used for calculating wraparound.
108 BasicValueFactory
&BVF
= getBasicVals();
109 APSIntType WraparoundType
= BVF
.getAPSIntType(Sym
->getType());
111 llvm::APSInt Adjustment
= WraparoundType
.getZeroValue();
112 SymbolRef AdjustedSym
= Sym
;
113 computeAdjustment(AdjustedSym
, Adjustment
);
115 // Convert the right-hand side integer as necessary.
116 APSIntType ComparisonType
= std::max(WraparoundType
, APSIntType(From
));
117 llvm::APSInt ConvertedFrom
= ComparisonType
.convert(From
);
118 llvm::APSInt ConvertedTo
= ComparisonType
.convert(To
);
120 // Prefer unsigned comparisons.
121 if (ComparisonType
.getBitWidth() == WraparoundType
.getBitWidth() &&
122 ComparisonType
.isUnsigned() && !WraparoundType
.isUnsigned())
123 Adjustment
.setIsSigned(false);
126 return assumeSymWithinInclusiveRange(State
, AdjustedSym
, ConvertedFrom
,
127 ConvertedTo
, Adjustment
);
128 return assumeSymOutsideInclusiveRange(State
, AdjustedSym
, ConvertedFrom
,
129 ConvertedTo
, Adjustment
);
133 RangedConstraintManager::assumeSymUnsupported(ProgramStateRef State
,
134 SymbolRef Sym
, bool Assumption
) {
135 Sym
= simplify(State
, Sym
);
137 BasicValueFactory
&BVF
= getBasicVals();
138 QualType T
= Sym
->getType();
140 // Non-integer types are not supported.
141 if (!T
->isIntegralOrEnumerationType())
144 // Reverse the operation and add directly to state.
145 const llvm::APSInt
&Zero
= BVF
.getValue(0, T
);
147 return assumeSymNE(State
, Sym
, Zero
, Zero
);
149 return assumeSymEQ(State
, Sym
, Zero
, Zero
);
152 ProgramStateRef
RangedConstraintManager::assumeSymRel(ProgramStateRef State
,
154 BinaryOperator::Opcode Op
,
155 const llvm::APSInt
&Int
) {
156 assert(BinaryOperator::isComparisonOp(Op
) &&
157 "Non-comparison ops should be rewritten as comparisons to zero.");
159 // Simplification: translate an assume of a constraint of the form
160 // "(exp comparison_op expr) != 0" to true into an assume of
161 // "exp comparison_op expr" to true. (And similarly, an assume of the form
162 // "(exp comparison_op expr) == 0" to true into an assume of
163 // "exp comparison_op expr" to false.)
164 if (Int
== 0 && (Op
== BO_EQ
|| Op
== BO_NE
)) {
165 if (const BinarySymExpr
*SE
= dyn_cast
<BinarySymExpr
>(Sym
))
166 if (BinaryOperator::isComparisonOp(SE
->getOpcode()))
167 return assumeSym(State
, Sym
, (Op
== BO_NE
? true : false));
170 // Get the type used for calculating wraparound.
171 BasicValueFactory
&BVF
= getBasicVals();
172 APSIntType WraparoundType
= BVF
.getAPSIntType(Sym
->getType());
174 // We only handle simple comparisons of the form "$sym == constant"
175 // or "($sym+constant1) == constant2".
176 // The adjustment is "constant1" in the above expression. It's used to
177 // "slide" the solution range around for modular arithmetic. For example,
178 // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
179 // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
180 // the subclasses of SimpleConstraintManager to handle the adjustment.
181 llvm::APSInt Adjustment
= WraparoundType
.getZeroValue();
182 computeAdjustment(Sym
, Adjustment
);
184 // Convert the right-hand side integer as necessary.
185 APSIntType ComparisonType
= std::max(WraparoundType
, APSIntType(Int
));
186 llvm::APSInt ConvertedInt
= ComparisonType
.convert(Int
);
188 // Prefer unsigned comparisons.
189 if (ComparisonType
.getBitWidth() == WraparoundType
.getBitWidth() &&
190 ComparisonType
.isUnsigned() && !WraparoundType
.isUnsigned())
191 Adjustment
.setIsSigned(false);
195 llvm_unreachable("invalid operation not caught by assertion above");
198 return assumeSymEQ(State
, Sym
, ConvertedInt
, Adjustment
);
201 return assumeSymNE(State
, Sym
, ConvertedInt
, Adjustment
);
204 return assumeSymGT(State
, Sym
, ConvertedInt
, Adjustment
);
207 return assumeSymGE(State
, Sym
, ConvertedInt
, Adjustment
);
210 return assumeSymLT(State
, Sym
, ConvertedInt
, Adjustment
);
213 return assumeSymLE(State
, Sym
, ConvertedInt
, Adjustment
);
217 void RangedConstraintManager::computeAdjustment(SymbolRef
&Sym
,
218 llvm::APSInt
&Adjustment
) {
219 // Is it a "($sym+constant1)" expression?
220 if (const SymIntExpr
*SE
= dyn_cast
<SymIntExpr
>(Sym
)) {
221 BinaryOperator::Opcode Op
= SE
->getOpcode();
222 if (Op
== BO_Add
|| Op
== BO_Sub
) {
224 Adjustment
= APSIntType(Adjustment
).convert(SE
->getRHS());
226 // Don't forget to negate the adjustment if it's being subtracted.
227 // This should happen /after/ promotion, in case the value being
228 // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
230 Adjustment
= -Adjustment
;
235 SVal
simplifyToSVal(ProgramStateRef State
, SymbolRef Sym
) {
236 SValBuilder
&SVB
= State
->getStateManager().getSValBuilder();
237 return SVB
.simplifySVal(State
, SVB
.makeSymbolVal(Sym
));
240 SymbolRef
simplify(ProgramStateRef State
, SymbolRef Sym
) {
241 SVal SimplifiedVal
= simplifyToSVal(State
, Sym
);
242 if (SymbolRef SimplifiedSym
= SimplifiedVal
.getAsSymbol())
243 return SimplifiedSym
;
247 } // end of namespace ento
248 } // end of namespace clang