1 //== RangeConstraintManager.cpp - Manage range constraints.------*- 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 RangeConstraintManager, a class that tracks simple
10 // equality and inequality constraints on symbolic values of ProgramState.
11 //
12 //===----------------------------------------------------------------------===//
13
14 #include "clang/Basic/JsonSupport.h"
15 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
16 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
17 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
18 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
19 #include "clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h"
20 #include "llvm/ADT/FoldingSet.h"
21 #include "llvm/ADT/ImmutableSet.h"
22 #include "llvm/ADT/STLExtras.h"
23 #include "llvm/ADT/StringExtras.h"
24 #include "llvm/ADT/SmallSet.h"
25 #include "llvm/Support/Compiler.h"
26 #include "llvm/Support/raw_ostream.h"
27 #include <algorithm>
28 #include <iterator>
29
30 using namespace clang;
31 using namespace ento;
32
33 // This class can be extended with other tables which will help to reason
34 // about ranges more precisely.
35 class OperatorRelationsTable {
36 static_assert(BO_LT < BO_GT && BO_GT < BO_LE && BO_LE < BO_GE &&
37 BO_GE < BO_EQ && BO_EQ < BO_NE,
38 "This class relies on operators order. Rework it otherwise.");
39
40 public:
41 enum TriStateKind {
42 False = 0,
43 True,
44 Unknown,
45 };
46
47 private:
48 // CmpOpTable holds states which represent the corresponding range for
49 // branching an exploded graph. We can reason about the branch if there is
50 // a previously known fact of the existence of a comparison expression with
51 // operands used in the current expression.
52 // E.g. assuming (x < y) is true that means (x != y) is surely true.
53 // if (x previous_operation y) // < | != | >
54 // if (x operation y) // != | > | <
55 // tristate // True | Unknown | False
56 //
57 // CmpOpTable represents next:
58 // __|< |> |<=|>=|==|!=|UnknownX2|
59 // < |1 |0 |* |0 |0 |* |1 |
60 // > |0 |1 |0 |* |0 |* |1 |
61 // <=|1 |0 |1 |* |1 |* |0 |
62 // >=|0 |1 |* |1 |1 |* |0 |
63 // ==|0 |0 |* |* |1 |0 |1 |
64 // !=|1 |1 |* |* |0 |1 |0 |
65 //
66 // Columns stands for a previous operator.
67 // Rows stands for a current operator.
68 // Each row has exactly two `Unknown` cases.
69 // UnknownX2 means that both `Unknown` previous operators are met in code,
70 // and there is a special column for that, for example:
71 // if (x >= y)
72 // if (x != y)
73 // if (x <= y)
74 // False only
75 static constexpr size_t CmpOpCount = BO_NE - BO_LT + 1;
76 const TriStateKind CmpOpTable[CmpOpCount][CmpOpCount + 1] = {
77 // < > <= >= == != UnknownX2
78 {True, False, Unknown, False, False, Unknown, True}, // <
79 {False, True, False, Unknown, False, Unknown, True}, // >
80 {True, False, True, Unknown, True, Unknown, False}, // <=
81 {False, True, Unknown, True, True, Unknown, False}, // >=
82 {False, False, Unknown, Unknown, True, False, True}, // ==
83 {True, True, Unknown, Unknown, False, True, False}, // !=
84 };
85
getIndexFromOp(BinaryOperatorKind OP)86 static size_t getIndexFromOp(BinaryOperatorKind OP) {
87 return static_cast<size_t>(OP - BO_LT);
88 }
89
90 public:
getCmpOpCount() const91 constexpr size_t getCmpOpCount() const { return CmpOpCount; }
92
getOpFromIndex(size_t Index)93 static BinaryOperatorKind getOpFromIndex(size_t Index) {
94 return static_cast<BinaryOperatorKind>(Index + BO_LT);
95 }
96
getCmpOpState(BinaryOperatorKind CurrentOP,BinaryOperatorKind QueriedOP) const97 TriStateKind getCmpOpState(BinaryOperatorKind CurrentOP,
98 BinaryOperatorKind QueriedOP) const {
99 return CmpOpTable[getIndexFromOp(CurrentOP)][getIndexFromOp(QueriedOP)];
100 }
101
getCmpOpStateForUnknownX2(BinaryOperatorKind CurrentOP) const102 TriStateKind getCmpOpStateForUnknownX2(BinaryOperatorKind CurrentOP) const {
103 return CmpOpTable[getIndexFromOp(CurrentOP)][CmpOpCount];
104 }
105 };
106
107 //===----------------------------------------------------------------------===//
108 // RangeSet implementation
109 //===----------------------------------------------------------------------===//
110
111 RangeSet::ContainerType RangeSet::Factory::EmptySet{};
112
add(RangeSet Original,Range Element)113 RangeSet RangeSet::Factory::add(RangeSet Original, Range Element) {
114 ContainerType Result;
115 Result.reserve(Original.size() + 1);
116
117 const_iterator Lower = llvm::lower_bound(Original, Element);
118 Result.insert(Result.end(), Original.begin(), Lower);
119 Result.push_back(Element);
120 Result.insert(Result.end(), Lower, Original.end());
121
122 return makePersistent(std::move(Result));
123 }
124
add(RangeSet Original,const llvm::APSInt & Point)125 RangeSet RangeSet::Factory::add(RangeSet Original, const llvm::APSInt &Point) {
126 return add(Original, Range(Point));
127 }
128
getRangeSet(Range From)129 RangeSet RangeSet::Factory::getRangeSet(Range From) {
130 ContainerType Result;
131 Result.push_back(From);
132 return makePersistent(std::move(Result));
133 }
134
makePersistent(ContainerType && From)135 RangeSet RangeSet::Factory::makePersistent(ContainerType &&From) {
136 llvm::FoldingSetNodeID ID;
137 void *InsertPos;
138
139 From.Profile(ID);
140 ContainerType *Result = Cache.FindNodeOrInsertPos(ID, InsertPos);
141
142 if (!Result) {
143 // It is cheaper to fully construct the resulting range on stack
144 // and move it to the freshly allocated buffer if we don't have
145 // a set like this already.
146 Result = construct(std::move(From));
147 Cache.InsertNode(Result, InsertPos);
148 }
149
150 return Result;
151 }
152
construct(ContainerType && From)153 RangeSet::ContainerType *RangeSet::Factory::construct(ContainerType &&From) {
154 void *Buffer = Arena.Allocate();
155 return new (Buffer) ContainerType(std::move(From));
156 }
157
add(RangeSet LHS,RangeSet RHS)158 RangeSet RangeSet::Factory::add(RangeSet LHS, RangeSet RHS) {
159 ContainerType Result;
160 std::merge(LHS.begin(), LHS.end(), RHS.begin(), RHS.end(),
161 std::back_inserter(Result));
162 return makePersistent(std::move(Result));
163 }
164
getMinValue() const165 const llvm::APSInt &RangeSet::getMinValue() const {
166 assert(!isEmpty());
167 return begin()->From();
168 }
169
getMaxValue() const170 const llvm::APSInt &RangeSet::getMaxValue() const {
171 assert(!isEmpty());
172 return std::prev(end())->To();
173 }
174
containsImpl(llvm::APSInt & Point) const175 bool RangeSet::containsImpl(llvm::APSInt &Point) const {
176 if (isEmpty() || !pin(Point))
177 return false;
178
179 Range Dummy(Point);
180 const_iterator It = llvm::upper_bound(*this, Dummy);
181 if (It == begin())
182 return false;
183
184 return std::prev(It)->Includes(Point);
185 }
186
pin(llvm::APSInt & Point) const187 bool RangeSet::pin(llvm::APSInt &Point) const {
188 APSIntType Type(getMinValue());
189 if (Type.testInRange(Point, true) != APSIntType::RTR_Within)
190 return false;
191
192 Type.apply(Point);
193 return true;
194 }
195
pin(llvm::APSInt & Lower,llvm::APSInt & Upper) const196 bool RangeSet::pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const {
197 // This function has nine cases, the cartesian product of range-testing
198 // both the upper and lower bounds against the symbol's type.
199 // Each case requires a different pinning operation.
200 // The function returns false if the described range is entirely outside
201 // the range of values for the associated symbol.
202 APSIntType Type(getMinValue());
203 APSIntType::RangeTestResultKind LowerTest = Type.testInRange(Lower, true);
204 APSIntType::RangeTestResultKind UpperTest = Type.testInRange(Upper, true);
205
206 switch (LowerTest) {
207 case APSIntType::RTR_Below:
208 switch (UpperTest) {
209 case APSIntType::RTR_Below:
210 // The entire range is outside the symbol's set of possible values.
211 // If this is a conventionally-ordered range, the state is infeasible.
212 if (Lower <= Upper)
213 return false;
214
215 // However, if the range wraps around, it spans all possible values.
216 Lower = Type.getMinValue();
217 Upper = Type.getMaxValue();
218 break;
219 case APSIntType::RTR_Within:
220 // The range starts below what's possible but ends within it. Pin.
221 Lower = Type.getMinValue();
222 Type.apply(Upper);
223 break;
224 case APSIntType::RTR_Above:
225 // The range spans all possible values for the symbol. Pin.
226 Lower = Type.getMinValue();
227 Upper = Type.getMaxValue();
228 break;
229 }
230 break;
231 case APSIntType::RTR_Within:
232 switch (UpperTest) {
233 case APSIntType::RTR_Below:
234 // The range wraps around, but all lower values are not possible.
235 Type.apply(Lower);
236 Upper = Type.getMaxValue();
237 break;
238 case APSIntType::RTR_Within:
239 // The range may or may not wrap around, but both limits are valid.
240 Type.apply(Lower);
241 Type.apply(Upper);
242 break;
243 case APSIntType::RTR_Above:
244 // The range starts within what's possible but ends above it. Pin.
245 Type.apply(Lower);
246 Upper = Type.getMaxValue();
247 break;
248 }
249 break;
250 case APSIntType::RTR_Above:
251 switch (UpperTest) {
252 case APSIntType::RTR_Below:
253 // The range wraps but is outside the symbol's set of possible values.
254 return false;
255 case APSIntType::RTR_Within:
256 // The range starts above what's possible but ends within it (wrap).
257 Lower = Type.getMinValue();
258 Type.apply(Upper);
259 break;
260 case APSIntType::RTR_Above:
261 // The entire range is outside the symbol's set of possible values.
262 // If this is a conventionally-ordered range, the state is infeasible.
263 if (Lower <= Upper)
264 return false;
265
266 // However, if the range wraps around, it spans all possible values.
267 Lower = Type.getMinValue();
268 Upper = Type.getMaxValue();
269 break;
270 }
271 break;
272 }
273
274 return true;
275 }
276
intersect(RangeSet What,llvm::APSInt Lower,llvm::APSInt Upper)277 RangeSet RangeSet::Factory::intersect(RangeSet What, llvm::APSInt Lower,
278 llvm::APSInt Upper) {
279 if (What.isEmpty() || !What.pin(Lower, Upper))
280 return getEmptySet();
281
282 ContainerType DummyContainer;
283
284 if (Lower <= Upper) {
285 // [Lower, Upper] is a regular range.
286 //
287 // Shortcut: check that there is even a possibility of the intersection
288 // by checking the two following situations:
289 //
290 // <---[ What ]---[------]------>
291 // Lower Upper
292 // -or-
293 // <----[------]----[ What ]---->
294 // Lower Upper
295 if (What.getMaxValue() < Lower || Upper < What.getMinValue())
296 return getEmptySet();
297
298 DummyContainer.push_back(
299 Range(ValueFactory.getValue(Lower), ValueFactory.getValue(Upper)));
300 } else {
301 // [Lower, Upper] is an inverted range, i.e. [MIN, Upper] U [Lower, MAX]
302 //
303 // Shortcut: check that there is even a possibility of the intersection
304 // by checking the following situation:
305 //
306 // <------]---[ What ]---[------>
307 // Upper Lower
308 if (What.getMaxValue() < Lower && Upper < What.getMinValue())
309 return getEmptySet();
310
311 DummyContainer.push_back(
312 Range(ValueFactory.getMinValue(Upper), ValueFactory.getValue(Upper)));
313 DummyContainer.push_back(
314 Range(ValueFactory.getValue(Lower), ValueFactory.getMaxValue(Lower)));
315 }
316
317 return intersect(*What.Impl, DummyContainer);
318 }
319
intersect(const RangeSet::ContainerType & LHS,const RangeSet::ContainerType & RHS)320 RangeSet RangeSet::Factory::intersect(const RangeSet::ContainerType &LHS,
321 const RangeSet::ContainerType &RHS) {
322 ContainerType Result;
323 Result.reserve(std::max(LHS.size(), RHS.size()));
324
325 const_iterator First = LHS.begin(), Second = RHS.begin(),
326 FirstEnd = LHS.end(), SecondEnd = RHS.end();
327
328 const auto SwapIterators = [&First, &FirstEnd, &Second, &SecondEnd]() {
329 std::swap(First, Second);
330 std::swap(FirstEnd, SecondEnd);
331 };
332
333 // If we ran out of ranges in one set, but not in the other,
334 // it means that those elements are definitely not in the
335 // intersection.
336 while (First != FirstEnd && Second != SecondEnd) {
337 // We want to keep the following invariant at all times:
338 //
339 // ----[ First ---------------------->
340 // --------[ Second ----------------->
341 if (Second->From() < First->From())
342 SwapIterators();
343
344 // Loop where the invariant holds:
345 do {
346 // Check for the following situation:
347 //
348 // ----[ First ]--------------------->
349 // ---------------[ Second ]--------->
350 //
351 // which means that...
352 if (Second->From() > First->To()) {
353 // ...First is not in the intersection.
354 //
355 // We should move on to the next range after First and break out of the
356 // loop because the invariant might not be true.
357 ++First;
358 break;
359 }
360
361 // We have a guaranteed intersection at this point!
362 // And this is the current situation:
363 //
364 // ----[ First ]----------------->
365 // -------[ Second ------------------>
366 //
367 // Additionally, it definitely starts with Second->From().
368 const llvm::APSInt &IntersectionStart = Second->From();
369
370 // It is important to know which of the two ranges' ends
371 // is greater. That "longer" range might have some other
372 // intersections, while the "shorter" range might not.
373 if (Second->To() > First->To()) {
374 // Here we make a decision to keep First as the "longer"
375 // range.
376 SwapIterators();
377 }
378
379 // At this point, we have the following situation:
380 //
381 // ---- First ]-------------------->
382 // ---- Second ]--[ Second+1 ---------->
383 //
384 // We don't know the relationship between First->From and
385 // Second->From and we don't know whether Second+1 intersects
386 // with First.
387 //
388 // However, we know that [IntersectionStart, Second->To] is
389 // a part of the intersection...
390 Result.push_back(Range(IntersectionStart, Second->To()));
391 ++Second;
392 // ...and that the invariant will hold for a valid Second+1
393 // because First->From <= Second->To < (Second+1)->From.
394 } while (Second != SecondEnd);
395 }
396
397 if (Result.empty())
398 return getEmptySet();
399
400 return makePersistent(std::move(Result));
401 }
402
intersect(RangeSet LHS,RangeSet RHS)403 RangeSet RangeSet::Factory::intersect(RangeSet LHS, RangeSet RHS) {
404 // Shortcut: let's see if the intersection is even possible.
405 if (LHS.isEmpty() || RHS.isEmpty() || LHS.getMaxValue() < RHS.getMinValue() ||
406 RHS.getMaxValue() < LHS.getMinValue())
407 return getEmptySet();
408
409 return intersect(*LHS.Impl, *RHS.Impl);
410 }
411
intersect(RangeSet LHS,llvm::APSInt Point)412 RangeSet RangeSet::Factory::intersect(RangeSet LHS, llvm::APSInt Point) {
413 if (LHS.containsImpl(Point))
414 return getRangeSet(ValueFactory.getValue(Point));
415
416 return getEmptySet();
417 }
418
negate(RangeSet What)419 RangeSet RangeSet::Factory::negate(RangeSet What) {
420 if (What.isEmpty())
421 return getEmptySet();
422
423 const llvm::APSInt SampleValue = What.getMinValue();
424 const llvm::APSInt &MIN = ValueFactory.getMinValue(SampleValue);
425 const llvm::APSInt &MAX = ValueFactory.getMaxValue(SampleValue);
426
427 ContainerType Result;
428 Result.reserve(What.size() + (SampleValue == MIN));
429
430 // Handle a special case for MIN value.
431 const_iterator It = What.begin();
432 const_iterator End = What.end();
433
434 const llvm::APSInt &From = It->From();
435 const llvm::APSInt &To = It->To();
436
437 if (From == MIN) {
438 // If the range [From, To] is [MIN, MAX], then result is also [MIN, MAX].
439 if (To == MAX) {
440 return What;
441 }
442
443 const_iterator Last = std::prev(End);
444
445 // Try to find and unite the following ranges:
446 // [MIN, MIN] & [MIN + 1, N] => [MIN, N].
447 if (Last->To() == MAX) {
448 // It means that in the original range we have ranges
449 // [MIN, A], ... , [B, MAX]
450 // And the result should be [MIN, -B], ..., [-A, MAX]
451 Result.emplace_back(MIN, ValueFactory.getValue(-Last->From()));
452 // We already negated Last, so we can skip it.
453 End = Last;
454 } else {
455 // Add a separate range for the lowest value.
456 Result.emplace_back(MIN, MIN);
457 }
458
459 // Skip adding the second range in case when [From, To] are [MIN, MIN].
460 if (To != MIN) {
461 Result.emplace_back(ValueFactory.getValue(-To), MAX);
462 }
463
464 // Skip the first range in the loop.
465 ++It;
466 }
467
468 // Negate all other ranges.
469 for (; It != End; ++It) {
470 // Negate int values.
471 const llvm::APSInt &NewFrom = ValueFactory.getValue(-It->To());
472 const llvm::APSInt &NewTo = ValueFactory.getValue(-It->From());
473
474 // Add a negated range.
475 Result.emplace_back(NewFrom, NewTo);
476 }
477
478 llvm::sort(Result);
479 return makePersistent(std::move(Result));
480 }
481
deletePoint(RangeSet From,const llvm::APSInt & Point)482 RangeSet RangeSet::Factory::deletePoint(RangeSet From,
483 const llvm::APSInt &Point) {
484 if (!From.contains(Point))
485 return From;
486
487 llvm::APSInt Upper = Point;
488 llvm::APSInt Lower = Point;
489
490 ++Upper;
491 --Lower;
492
493 // Notice that the lower bound is greater than the upper bound.
494 return intersect(From, Upper, Lower);
495 }
496
dump(raw_ostream & OS) const497 void Range::dump(raw_ostream &OS) const {
498 OS << '[' << toString(From(), 10) << ", " << toString(To(), 10) << ']';
499 }
500
dump(raw_ostream & OS) const501 void RangeSet::dump(raw_ostream &OS) const {
502 OS << "{ ";
503 llvm::interleaveComma(*this, OS, [&OS](const Range &R) { R.dump(OS); });
504 OS << " }";
505 }
506
507 REGISTER_SET_FACTORY_WITH_PROGRAMSTATE(SymbolSet, SymbolRef)
508
509 namespace {
510 class EquivalenceClass;
511 } // end anonymous namespace
512
513 REGISTER_MAP_WITH_PROGRAMSTATE(ClassMap, SymbolRef, EquivalenceClass)
514 REGISTER_MAP_WITH_PROGRAMSTATE(ClassMembers, EquivalenceClass, SymbolSet)
515 REGISTER_MAP_WITH_PROGRAMSTATE(ConstraintRange, EquivalenceClass, RangeSet)
516
517 REGISTER_SET_FACTORY_WITH_PROGRAMSTATE(ClassSet, EquivalenceClass)
518 REGISTER_MAP_WITH_PROGRAMSTATE(DisequalityMap, EquivalenceClass, ClassSet)
519
520 namespace {
521 /// This class encapsulates a set of symbols equal to each other.
522 ///
523 /// The main idea of the approach requiring such classes is in narrowing
524 /// and sharing constraints between symbols within the class. Also we can
525 /// conclude that there is no practical need in storing constraints for
526 /// every member of the class separately.
527 ///
528 /// Main terminology:
529 ///
530 /// * "Equivalence class" is an object of this class, which can be efficiently
531 /// compared to other classes. It represents the whole class without
532 /// storing the actual in it. The members of the class however can be
533 /// retrieved from the state.
534 ///
535 /// * "Class members" are the symbols corresponding to the class. This means
536 /// that A == B for every member symbols A and B from the class. Members of
537 /// each class are stored in the state.
538 ///
539 /// * "Trivial class" is a class that has and ever had only one same symbol.
540 ///
541 /// * "Merge operation" merges two classes into one. It is the main operation
542 /// to produce non-trivial classes.
543 /// If, at some point, we can assume that two symbols from two distinct
544 /// classes are equal, we can merge these classes.
545 class EquivalenceClass : public llvm::FoldingSetNode {
546 public:
547 /// Find equivalence class for the given symbol in the given state.
548 LLVM_NODISCARD static inline EquivalenceClass find(ProgramStateRef State,
549 SymbolRef Sym);
550
551 /// Merge classes for the given symbols and return a new state.
552 LLVM_NODISCARD static inline ProgramStateRef merge(RangeSet::Factory &F,
553 ProgramStateRef State,
554 SymbolRef First,
555 SymbolRef Second);
556 // Merge this class with the given class and return a new state.
557 LLVM_NODISCARD inline ProgramStateRef
558 merge(RangeSet::Factory &F, ProgramStateRef State, EquivalenceClass Other);
559
560 /// Return a set of class members for the given state.
561 LLVM_NODISCARD inline SymbolSet getClassMembers(ProgramStateRef State) const;
562
563 /// Return true if the current class is trivial in the given state.
564 /// A class is trivial if and only if there is not any member relations stored
565 /// to it in State/ClassMembers.
566 /// An equivalence class with one member might seem as it does not hold any
567 /// meaningful information, i.e. that is a tautology. However, during the
568 /// removal of dead symbols we do not remove classes with one member for
569 /// resource and performance reasons. Consequently, a class with one member is
570 /// not necessarily trivial. It could happen that we have a class with two
571 /// members and then during the removal of dead symbols we remove one of its
572 /// members. In this case, the class is still non-trivial (it still has the
573 /// mappings in ClassMembers), even though it has only one member.
574 LLVM_NODISCARD inline bool isTrivial(ProgramStateRef State) const;
575
576 /// Return true if the current class is trivial and its only member is dead.
577 LLVM_NODISCARD inline bool isTriviallyDead(ProgramStateRef State,
578 SymbolReaper &Reaper) const;
579
580 LLVM_NODISCARD static inline ProgramStateRef
581 markDisequal(RangeSet::Factory &F, ProgramStateRef State, SymbolRef First,
582 SymbolRef Second);
583 LLVM_NODISCARD static inline ProgramStateRef
584 markDisequal(RangeSet::Factory &F, ProgramStateRef State,
585 EquivalenceClass First, EquivalenceClass Second);
586 LLVM_NODISCARD inline ProgramStateRef
587 markDisequal(RangeSet::Factory &F, ProgramStateRef State,
588 EquivalenceClass Other) const;
589 LLVM_NODISCARD static inline ClassSet
590 getDisequalClasses(ProgramStateRef State, SymbolRef Sym);
591 LLVM_NODISCARD inline ClassSet
592 getDisequalClasses(ProgramStateRef State) const;
593 LLVM_NODISCARD inline ClassSet
594 getDisequalClasses(DisequalityMapTy Map, ClassSet::Factory &Factory) const;
595
596 LLVM_NODISCARD static inline Optional<bool> areEqual(ProgramStateRef State,
597 EquivalenceClass First,
598 EquivalenceClass Second);
599 LLVM_NODISCARD static inline Optional<bool>
600 areEqual(ProgramStateRef State, SymbolRef First, SymbolRef Second);
601
602 /// Iterate over all symbols and try to simplify them.
603 LLVM_NODISCARD static inline ProgramStateRef simplify(SValBuilder &SVB,
604 RangeSet::Factory &F,
605 ProgramStateRef State,
606 EquivalenceClass Class);
607
608 void dumpToStream(ProgramStateRef State, raw_ostream &os) const;
dump(ProgramStateRef State) const609 LLVM_DUMP_METHOD void dump(ProgramStateRef State) const {
610 dumpToStream(State, llvm::errs());
611 }
612
613 /// Check equivalence data for consistency.
614 LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED static bool
615 isClassDataConsistent(ProgramStateRef State);
616
getType() const617 LLVM_NODISCARD QualType getType() const {
618 return getRepresentativeSymbol()->getType();
619 }
620
621 EquivalenceClass() = delete;
622 EquivalenceClass(const EquivalenceClass &) = default;
623 EquivalenceClass &operator=(const EquivalenceClass &) = delete;
624 EquivalenceClass(EquivalenceClass &&) = default;
625 EquivalenceClass &operator=(EquivalenceClass &&) = delete;
626
operator ==(const EquivalenceClass & Other) const627 bool operator==(const EquivalenceClass &Other) const {
628 return ID == Other.ID;
629 }
operator <(const EquivalenceClass & Other) const630 bool operator<(const EquivalenceClass &Other) const { return ID < Other.ID; }
operator !=(const EquivalenceClass & Other) const631 bool operator!=(const EquivalenceClass &Other) const {
632 return !operator==(Other);
633 }
634
Profile(llvm::FoldingSetNodeID & ID,uintptr_t CID)635 static void Profile(llvm::FoldingSetNodeID &ID, uintptr_t CID) {
636 ID.AddInteger(CID);
637 }
638
Profile(llvm::FoldingSetNodeID & ID) const639 void Profile(llvm::FoldingSetNodeID &ID) const { Profile(ID, this->ID); }
640
641 private:
EquivalenceClass(SymbolRef Sym)642 /* implicit */ EquivalenceClass(SymbolRef Sym)
643 : ID(reinterpret_cast<uintptr_t>(Sym)) {}
644
645 /// This function is intended to be used ONLY within the class.
646 /// The fact that ID is a pointer to a symbol is an implementation detail
647 /// and should stay that way.
648 /// In the current implementation, we use it to retrieve the only member
649 /// of the trivial class.
getRepresentativeSymbol() const650 SymbolRef getRepresentativeSymbol() const {
651 return reinterpret_cast<SymbolRef>(ID);
652 }
653 static inline SymbolSet::Factory &getMembersFactory(ProgramStateRef State);
654
655 inline ProgramStateRef mergeImpl(RangeSet::Factory &F, ProgramStateRef State,
656 SymbolSet Members, EquivalenceClass Other,
657 SymbolSet OtherMembers);
658 static inline bool
659 addToDisequalityInfo(DisequalityMapTy &Info, ConstraintRangeTy &Constraints,
660 RangeSet::Factory &F, ProgramStateRef State,
661 EquivalenceClass First, EquivalenceClass Second);
662
663 /// This is a unique identifier of the class.
664 uintptr_t ID;
665 };
666
667 //===----------------------------------------------------------------------===//
668 // Constraint functions
669 //===----------------------------------------------------------------------===//
670
671 LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED bool
areFeasible(ConstraintRangeTy Constraints)672 areFeasible(ConstraintRangeTy Constraints) {
673 return llvm::none_of(
674 Constraints,
675 [](const std::pair<EquivalenceClass, RangeSet> &ClassConstraint) {
676 return ClassConstraint.second.isEmpty();
677 });
678 }
679
getConstraint(ProgramStateRef State,EquivalenceClass Class)680 LLVM_NODISCARD inline const RangeSet *getConstraint(ProgramStateRef State,
681 EquivalenceClass Class) {
682 return State->get<ConstraintRange>(Class);
683 }
684
getConstraint(ProgramStateRef State,SymbolRef Sym)685 LLVM_NODISCARD inline const RangeSet *getConstraint(ProgramStateRef State,
686 SymbolRef Sym) {
687 return getConstraint(State, EquivalenceClass::find(State, Sym));
688 }
689
setConstraint(ProgramStateRef State,EquivalenceClass Class,RangeSet Constraint)690 LLVM_NODISCARD ProgramStateRef setConstraint(ProgramStateRef State,
691 EquivalenceClass Class,
692 RangeSet Constraint) {
693 return State->set<ConstraintRange>(Class, Constraint);
694 }
695
setConstraints(ProgramStateRef State,ConstraintRangeTy Constraints)696 LLVM_NODISCARD ProgramStateRef setConstraints(ProgramStateRef State,
697 ConstraintRangeTy Constraints) {
698 return State->set<ConstraintRange>(Constraints);
699 }
700
701 //===----------------------------------------------------------------------===//
702 // Equality/diseqiality abstraction
703 //===----------------------------------------------------------------------===//
704
705 /// A small helper function for detecting symbolic (dis)equality.
706 ///
707 /// Equality check can have different forms (like a == b or a - b) and this
708 /// class encapsulates those away if the only thing the user wants to check -
709 /// whether it's equality/diseqiality or not.
710 ///
711 /// \returns true if assuming this Sym to be true means equality of operands
712 /// false if it means disequality of operands
713 /// None otherwise
meansEquality(const SymSymExpr * Sym)714 Optional<bool> meansEquality(const SymSymExpr *Sym) {
715 switch (Sym->getOpcode()) {
716 case BO_Sub:
717 // This case is: A - B != 0 -> disequality check.
718 return false;
719 case BO_EQ:
720 // This case is: A == B != 0 -> equality check.
721 return true;
722 case BO_NE:
723 // This case is: A != B != 0 -> diseqiality check.
724 return false;
725 default:
726 return llvm::None;
727 }
728 }
729
730 //===----------------------------------------------------------------------===//
731 // Intersection functions
732 //===----------------------------------------------------------------------===//
733
734 template <class SecondTy, class... RestTy>
735 LLVM_NODISCARD inline RangeSet intersect(RangeSet::Factory &F, RangeSet Head,
736 SecondTy Second, RestTy... Tail);
737
738 template <class... RangeTy> struct IntersectionTraits;
739
740 template <class... TailTy> struct IntersectionTraits<RangeSet, TailTy...> {
741 // Found RangeSet, no need to check any further
742 using Type = RangeSet;
743 };
744
745 template <> struct IntersectionTraits<> {
746 // We ran out of types, and we didn't find any RangeSet, so the result should
747 // be optional.
748 using Type = Optional<RangeSet>;
749 };
750
751 template <class OptionalOrPointer, class... TailTy>
752 struct IntersectionTraits<OptionalOrPointer, TailTy...> {
753 // If current type is Optional or a raw pointer, we should keep looking.
754 using Type = typename IntersectionTraits<TailTy...>::Type;
755 };
756
757 template <class EndTy>
intersect(RangeSet::Factory & F,EndTy End)758 LLVM_NODISCARD inline EndTy intersect(RangeSet::Factory &F, EndTy End) {
759 // If the list contains only RangeSet or Optional<RangeSet>, simply return
760 // that range set.
761 return End;
762 }
763
764 LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED inline Optional<RangeSet>
intersect(RangeSet::Factory & F,const RangeSet * End)765 intersect(RangeSet::Factory &F, const RangeSet *End) {
766 // This is an extraneous conversion from a raw pointer into Optional<RangeSet>
767 if (End) {
768 return *End;
769 }
770 return llvm::None;
771 }
772
773 template <class... RestTy>
intersect(RangeSet::Factory & F,RangeSet Head,RangeSet Second,RestTy...Tail)774 LLVM_NODISCARD inline RangeSet intersect(RangeSet::Factory &F, RangeSet Head,
775 RangeSet Second, RestTy... Tail) {
776 // Here we call either the <RangeSet,RangeSet,...> or <RangeSet,...> version
777 // of the function and can be sure that the result is RangeSet.
778 return intersect(F, F.intersect(Head, Second), Tail...);
779 }
780
781 template <class SecondTy, class... RestTy>
intersect(RangeSet::Factory & F,RangeSet Head,SecondTy Second,RestTy...Tail)782 LLVM_NODISCARD inline RangeSet intersect(RangeSet::Factory &F, RangeSet Head,
783 SecondTy Second, RestTy... Tail) {
784 if (Second) {
785 // Here we call the <RangeSet,RangeSet,...> version of the function...
786 return intersect(F, Head, *Second, Tail...);
787 }
788 // ...and here it is either <RangeSet,RangeSet,...> or <RangeSet,...>, which
789 // means that the result is definitely RangeSet.
790 return intersect(F, Head, Tail...);
791 }
792
793 /// Main generic intersect function.
794 /// It intersects all of the given range sets. If some of the given arguments
795 /// don't hold a range set (nullptr or llvm::None), the function will skip them.
796 ///
797 /// Available representations for the arguments are:
798 /// * RangeSet
799 /// * Optional<RangeSet>
800 /// * RangeSet *
801 /// Pointer to a RangeSet is automatically assumed to be nullable and will get
802 /// checked as well as the optional version. If this behaviour is undesired,
803 /// please dereference the pointer in the call.
804 ///
805 /// Return type depends on the arguments' types. If we can be sure in compile
806 /// time that there will be a range set as a result, the returning type is
807 /// simply RangeSet, in other cases we have to back off to Optional<RangeSet>.
808 ///
809 /// Please, prefer optional range sets to raw pointers. If the last argument is
810 /// a raw pointer and all previous arguments are None, it will cost one
811 /// additional check to convert RangeSet * into Optional<RangeSet>.
812 template <class HeadTy, class SecondTy, class... RestTy>
813 LLVM_NODISCARD inline
814 typename IntersectionTraits<HeadTy, SecondTy, RestTy...>::Type
intersect(RangeSet::Factory & F,HeadTy Head,SecondTy Second,RestTy...Tail)815 intersect(RangeSet::Factory &F, HeadTy Head, SecondTy Second,
816 RestTy... Tail) {
817 if (Head) {
818 return intersect(F, *Head, Second, Tail...);
819 }
820 return intersect(F, Second, Tail...);
821 }
822
823 //===----------------------------------------------------------------------===//
824 // Symbolic reasoning logic
825 //===----------------------------------------------------------------------===//
826
827 /// A little component aggregating all of the reasoning we have about
828 /// the ranges of symbolic expressions.
829 ///
830 /// Even when we don't know the exact values of the operands, we still
831 /// can get a pretty good estimate of the result's range.
832 class SymbolicRangeInferrer
833 : public SymExprVisitor<SymbolicRangeInferrer, RangeSet> {
834 public:
835 template <class SourceType>
inferRange(RangeSet::Factory & F,ProgramStateRef State,SourceType Origin)836 static RangeSet inferRange(RangeSet::Factory &F, ProgramStateRef State,
837 SourceType Origin) {
838 SymbolicRangeInferrer Inferrer(F, State);
839 return Inferrer.infer(Origin);
840 }
841
VisitSymExpr(SymbolRef Sym)842 RangeSet VisitSymExpr(SymbolRef Sym) {
843 // If we got to this function, the actual type of the symbolic
844 // expression is not supported for advanced inference.
845 // In this case, we simply backoff to the default "let's simply
846 // infer the range from the expression's type".
847 return infer(Sym->getType());
848 }
849
VisitSymIntExpr(const SymIntExpr * Sym)850 RangeSet VisitSymIntExpr(const SymIntExpr *Sym) {
851 return VisitBinaryOperator(Sym);
852 }
853
VisitIntSymExpr(const IntSymExpr * Sym)854 RangeSet VisitIntSymExpr(const IntSymExpr *Sym) {
855 return VisitBinaryOperator(Sym);
856 }
857
VisitSymSymExpr(const SymSymExpr * Sym)858 RangeSet VisitSymSymExpr(const SymSymExpr *Sym) {
859 return intersect(
860 RangeFactory,
861 // If Sym is (dis)equality, we might have some information
862 // on that in our equality classes data structure.
863 getRangeForEqualities(Sym),
864 // And we should always check what we can get from the operands.
865 VisitBinaryOperator(Sym));
866 }
867
868 private:
SymbolicRangeInferrer(RangeSet::Factory & F,ProgramStateRef S)869 SymbolicRangeInferrer(RangeSet::Factory &F, ProgramStateRef S)
870 : ValueFactory(F.getValueFactory()), RangeFactory(F), State(S) {}
871
872 /// Infer range information from the given integer constant.
873 ///
874 /// It's not a real "inference", but is here for operating with
875 /// sub-expressions in a more polymorphic manner.
inferAs(const llvm::APSInt & Val,QualType)876 RangeSet inferAs(const llvm::APSInt &Val, QualType) {
877 return {RangeFactory, Val};
878 }
879
880 /// Infer range information from symbol in the context of the given type.
inferAs(SymbolRef Sym,QualType DestType)881 RangeSet inferAs(SymbolRef Sym, QualType DestType) {
882 QualType ActualType = Sym->getType();
883 // Check that we can reason about the symbol at all.
884 if (ActualType->isIntegralOrEnumerationType() ||
885 Loc::isLocType(ActualType)) {
886 return infer(Sym);
887 }
888 // Otherwise, let's simply infer from the destination type.
889 // We couldn't figure out nothing else about that expression.
890 return infer(DestType);
891 }
892
infer(SymbolRef Sym)893 RangeSet infer(SymbolRef Sym) {
894 return intersect(
895 RangeFactory,
896 // Of course, we should take the constraint directly associated with
897 // this symbol into consideration.
898 getConstraint(State, Sym),
899 // If Sym is a difference of symbols A - B, then maybe we have range
900 // set stored for B - A.
901 //
902 // If we have range set stored for both A - B and B - A then
903 // calculate the effective range set by intersecting the range set
904 // for A - B and the negated range set of B - A.
905 getRangeForNegatedSub(Sym),
906 // If Sym is a comparison expression (except <=>),
907 // find any other comparisons with the same operands.
908 // See function description.
909 getRangeForComparisonSymbol(Sym),
910 // Apart from the Sym itself, we can infer quite a lot if we look
911 // into subexpressions of Sym.
912 Visit(Sym));
913 }
914
infer(EquivalenceClass Class)915 RangeSet infer(EquivalenceClass Class) {
916 if (const RangeSet *AssociatedConstraint = getConstraint(State, Class))
917 return *AssociatedConstraint;
918
919 return infer(Class.getType());
920 }
921
922 /// Infer range information solely from the type.
infer(QualType T)923 RangeSet infer(QualType T) {
924 // Lazily generate a new RangeSet representing all possible values for the
925 // given symbol type.
926 RangeSet Result(RangeFactory, ValueFactory.getMinValue(T),
927 ValueFactory.getMaxValue(T));
928
929 // References are known to be non-zero.
930 if (T->isReferenceType())
931 return assumeNonZero(Result, T);
932
933 return Result;
934 }
935
936 template <class BinarySymExprTy>
VisitBinaryOperator(const BinarySymExprTy * Sym)937 RangeSet VisitBinaryOperator(const BinarySymExprTy *Sym) {
938 // TODO #1: VisitBinaryOperator implementation might not make a good
939 // use of the inferred ranges. In this case, we might be calculating
940 // everything for nothing. This being said, we should introduce some
941 // sort of laziness mechanism here.
942 //
943 // TODO #2: We didn't go into the nested expressions before, so it
944 // might cause us spending much more time doing the inference.
945 // This can be a problem for deeply nested expressions that are
946 // involved in conditions and get tested continuously. We definitely
947 // need to address this issue and introduce some sort of caching
948 // in here.
949 QualType ResultType = Sym->getType();
950 return VisitBinaryOperator(inferAs(Sym->getLHS(), ResultType),
951 Sym->getOpcode(),
952 inferAs(Sym->getRHS(), ResultType), ResultType);
953 }
954
VisitBinaryOperator(RangeSet LHS,BinaryOperator::Opcode Op,RangeSet RHS,QualType T)955 RangeSet VisitBinaryOperator(RangeSet LHS, BinaryOperator::Opcode Op,
956 RangeSet RHS, QualType T) {
957 switch (Op) {
958 case BO_Or:
959 return VisitBinaryOperator<BO_Or>(LHS, RHS, T);
960 case BO_And:
961 return VisitBinaryOperator<BO_And>(LHS, RHS, T);
962 case BO_Rem:
963 return VisitBinaryOperator<BO_Rem>(LHS, RHS, T);
964 default:
965 return infer(T);
966 }
967 }
968
969 //===----------------------------------------------------------------------===//
970 // Ranges and operators
971 //===----------------------------------------------------------------------===//
972
973 /// Return a rough approximation of the given range set.
974 ///
975 /// For the range set:
976 /// { [x_0, y_0], [x_1, y_1], ... , [x_N, y_N] }
977 /// it will return the range [x_0, y_N].
fillGaps(RangeSet Origin)978 static Range fillGaps(RangeSet Origin) {
979 assert(!Origin.isEmpty());
980 return {Origin.getMinValue(), Origin.getMaxValue()};
981 }
982
983 /// Try to convert given range into the given type.
984 ///
985 /// It will return llvm::None only when the trivial conversion is possible.
convert(const Range & Origin,APSIntType To)986 llvm::Optional<Range> convert(const Range &Origin, APSIntType To) {
987 if (To.testInRange(Origin.From(), false) != APSIntType::RTR_Within ||
988 To.testInRange(Origin.To(), false) != APSIntType::RTR_Within) {
989 return llvm::None;
990 }
991 return Range(ValueFactory.Convert(To, Origin.From()),
992 ValueFactory.Convert(To, Origin.To()));
993 }
994
995 template <BinaryOperator::Opcode Op>
VisitBinaryOperator(RangeSet LHS,RangeSet RHS,QualType T)996 RangeSet VisitBinaryOperator(RangeSet LHS, RangeSet RHS, QualType T) {
997 // We should propagate information about unfeasbility of one of the
998 // operands to the resulting range.
999 if (LHS.isEmpty() || RHS.isEmpty()) {
1000 return RangeFactory.getEmptySet();
1001 }
1002
1003 Range CoarseLHS = fillGaps(LHS);
1004 Range CoarseRHS = fillGaps(RHS);
1005
1006 APSIntType ResultType = ValueFactory.getAPSIntType(T);
1007
1008 // We need to convert ranges to the resulting type, so we can compare values
1009 // and combine them in a meaningful (in terms of the given operation) way.
1010 auto ConvertedCoarseLHS = convert(CoarseLHS, ResultType);
1011 auto ConvertedCoarseRHS = convert(CoarseRHS, ResultType);
1012
1013 // It is hard to reason about ranges when conversion changes
1014 // borders of the ranges.
1015 if (!ConvertedCoarseLHS || !ConvertedCoarseRHS) {
1016 return infer(T);
1017 }
1018
1019 return VisitBinaryOperator<Op>(*ConvertedCoarseLHS, *ConvertedCoarseRHS, T);
1020 }
1021
1022 template <BinaryOperator::Opcode Op>
VisitBinaryOperator(Range LHS,Range RHS,QualType T)1023 RangeSet VisitBinaryOperator(Range LHS, Range RHS, QualType T) {
1024 return infer(T);
1025 }
1026
1027 /// Return a symmetrical range for the given range and type.
1028 ///
1029 /// If T is signed, return the smallest range [-x..x] that covers the original
1030 /// range, or [-min(T), max(T)] if the aforementioned symmetric range doesn't
1031 /// exist due to original range covering min(T)).
1032 ///
1033 /// If T is unsigned, return the smallest range [0..x] that covers the
1034 /// original range.
getSymmetricalRange(Range Origin,QualType T)1035 Range getSymmetricalRange(Range Origin, QualType T) {
1036 APSIntType RangeType = ValueFactory.getAPSIntType(T);
1037
1038 if (RangeType.isUnsigned()) {
1039 return Range(ValueFactory.getMinValue(RangeType), Origin.To());
1040 }
1041
1042 if (Origin.From().isMinSignedValue()) {
1043 // If mini is a minimal signed value, absolute value of it is greater
1044 // than the maximal signed value. In order to avoid these
1045 // complications, we simply return the whole range.
1046 return {ValueFactory.getMinValue(RangeType),
1047 ValueFactory.getMaxValue(RangeType)};
1048 }
1049
1050 // At this point, we are sure that the type is signed and we can safely
1051 // use unary - operator.
1052 //
1053 // While calculating absolute maximum, we can use the following formula
1054 // because of these reasons:
1055 // * If From >= 0 then To >= From and To >= -From.
1056 // AbsMax == To == max(To, -From)
1057 // * If To <= 0 then -From >= -To and -From >= From.
1058 // AbsMax == -From == max(-From, To)
1059 // * Otherwise, From <= 0, To >= 0, and
1060 // AbsMax == max(abs(From), abs(To))
1061 llvm::APSInt AbsMax = std::max(-Origin.From(), Origin.To());
1062
1063 // Intersection is guaranteed to be non-empty.
1064 return {ValueFactory.getValue(-AbsMax), ValueFactory.getValue(AbsMax)};
1065 }
1066
1067 /// Return a range set subtracting zero from \p Domain.
assumeNonZero(RangeSet Domain,QualType T)1068 RangeSet assumeNonZero(RangeSet Domain, QualType T) {
1069 APSIntType IntType = ValueFactory.getAPSIntType(T);
1070 return RangeFactory.deletePoint(Domain, IntType.getZeroValue());
1071 }
1072
1073 // FIXME: Once SValBuilder supports unary minus, we should use SValBuilder to
1074 // obtain the negated symbolic expression instead of constructing the
1075 // symbol manually. This will allow us to support finding ranges of not
1076 // only negated SymSymExpr-type expressions, but also of other, simpler
1077 // expressions which we currently do not know how to negate.
getRangeForNegatedSub(SymbolRef Sym)1078 Optional<RangeSet> getRangeForNegatedSub(SymbolRef Sym) {
1079 if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) {
1080 if (SSE->getOpcode() == BO_Sub) {
1081 QualType T = Sym->getType();
1082
1083 // Do not negate unsigned ranges
1084 if (!T->isUnsignedIntegerOrEnumerationType() &&
1085 !T->isSignedIntegerOrEnumerationType())
1086 return llvm::None;
1087
1088 SymbolManager &SymMgr = State->getSymbolManager();
1089 SymbolRef NegatedSym =
1090 SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), T);
1091
1092 if (const RangeSet *NegatedRange = getConstraint(State, NegatedSym)) {
1093 return RangeFactory.negate(*NegatedRange);
1094 }
1095 }
1096 }
1097 return llvm::None;
1098 }
1099
1100 // Returns ranges only for binary comparison operators (except <=>)
1101 // when left and right operands are symbolic values.
1102 // Finds any other comparisons with the same operands.
1103 // Then do logical calculations and refuse impossible branches.
1104 // E.g. (x < y) and (x > y) at the same time are impossible.
1105 // E.g. (x >= y) and (x != y) at the same time makes (x > y) true only.
1106 // E.g. (x == y) and (y == x) are just reversed but the same.
1107 // It covers all possible combinations (see CmpOpTable description).
1108 // Note that `x` and `y` can also stand for subexpressions,
1109 // not only for actual symbols.
getRangeForComparisonSymbol(SymbolRef Sym)1110 Optional<RangeSet> getRangeForComparisonSymbol(SymbolRef Sym) {
1111 const auto *SSE = dyn_cast<SymSymExpr>(Sym);
1112 if (!SSE)
1113 return llvm::None;
1114
1115 BinaryOperatorKind CurrentOP = SSE->getOpcode();
1116
1117 // We currently do not support <=> (C++20).
1118 if (!BinaryOperator::isComparisonOp(CurrentOP) || (CurrentOP == BO_Cmp))
1119 return llvm::None;
1120
1121 static const OperatorRelationsTable CmpOpTable{};
1122
1123 const SymExpr *LHS = SSE->getLHS();
1124 const SymExpr *RHS = SSE->getRHS();
1125 QualType T = SSE->getType();
1126
1127 SymbolManager &SymMgr = State->getSymbolManager();
1128
1129 int UnknownStates = 0;
1130
1131 // Loop goes through all of the columns exept the last one ('UnknownX2').
1132 // We treat `UnknownX2` column separately at the end of the loop body.
1133 for (size_t i = 0; i < CmpOpTable.getCmpOpCount(); ++i) {
1134
1135 // Let's find an expression e.g. (x < y).
1136 BinaryOperatorKind QueriedOP = OperatorRelationsTable::getOpFromIndex(i);
1137 const SymSymExpr *SymSym = SymMgr.getSymSymExpr(LHS, QueriedOP, RHS, T);
1138 const RangeSet *QueriedRangeSet = getConstraint(State, SymSym);
1139
1140 // If ranges were not previously found,
1141 // try to find a reversed expression (y > x).
1142 if (!QueriedRangeSet) {
1143 const BinaryOperatorKind ROP =
1144 BinaryOperator::reverseComparisonOp(QueriedOP);
1145 SymSym = SymMgr.getSymSymExpr(RHS, ROP, LHS, T);
1146 QueriedRangeSet = getConstraint(State, SymSym);
1147 }
1148
1149 if (!QueriedRangeSet || QueriedRangeSet->isEmpty())
1150 continue;
1151
1152 const llvm::APSInt *ConcreteValue = QueriedRangeSet->getConcreteValue();
1153 const bool isInFalseBranch =
1154 ConcreteValue ? (*ConcreteValue == 0) : false;
1155
1156 // If it is a false branch, we shall be guided by opposite operator,
1157 // because the table is made assuming we are in the true branch.
1158 // E.g. when (x <= y) is false, then (x > y) is true.
1159 if (isInFalseBranch)
1160 QueriedOP = BinaryOperator::negateComparisonOp(QueriedOP);
1161
1162 OperatorRelationsTable::TriStateKind BranchState =
1163 CmpOpTable.getCmpOpState(CurrentOP, QueriedOP);
1164
1165 if (BranchState == OperatorRelationsTable::Unknown) {
1166 if (++UnknownStates == 2)
1167 // If we met both Unknown states.
1168 // if (x <= y) // assume true
1169 // if (x != y) // assume true
1170 // if (x < y) // would be also true
1171 // Get a state from `UnknownX2` column.
1172 BranchState = CmpOpTable.getCmpOpStateForUnknownX2(CurrentOP);
1173 else
1174 continue;
1175 }
1176
1177 return (BranchState == OperatorRelationsTable::True) ? getTrueRange(T)
1178 : getFalseRange(T);
1179 }
1180
1181 return llvm::None;
1182 }
1183
getRangeForEqualities(const SymSymExpr * Sym)1184 Optional<RangeSet> getRangeForEqualities(const SymSymExpr *Sym) {
1185 Optional<bool> Equality = meansEquality(Sym);
1186
1187 if (!Equality)
1188 return llvm::None;
1189
1190 if (Optional<bool> AreEqual =
1191 EquivalenceClass::areEqual(State, Sym->getLHS(), Sym->getRHS())) {
1192 // Here we cover two cases at once:
1193 // * if Sym is equality and its operands are known to be equal -> true
1194 // * if Sym is disequality and its operands are disequal -> true
1195 if (*AreEqual == *Equality) {
1196 return getTrueRange(Sym->getType());
1197 }
1198 // Opposite combinations result in false.
1199 return getFalseRange(Sym->getType());
1200 }
1201
1202 return llvm::None;
1203 }
1204
getTrueRange(QualType T)1205 RangeSet getTrueRange(QualType T) {
1206 RangeSet TypeRange = infer(T);
1207 return assumeNonZero(TypeRange, T);
1208 }
1209
getFalseRange(QualType T)1210 RangeSet getFalseRange(QualType T) {
1211 const llvm::APSInt &Zero = ValueFactory.getValue(0, T);
1212 return RangeSet(RangeFactory, Zero);
1213 }
1214
1215 BasicValueFactory &ValueFactory;
1216 RangeSet::Factory &RangeFactory;
1217 ProgramStateRef State;
1218 };
1219
1220 //===----------------------------------------------------------------------===//
1221 // Range-based reasoning about symbolic operations
1222 //===----------------------------------------------------------------------===//
1223
1224 template <>
VisitBinaryOperator(Range LHS,Range RHS,QualType T)1225 RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Or>(Range LHS, Range RHS,
1226 QualType T) {
1227 APSIntType ResultType = ValueFactory.getAPSIntType(T);
1228 llvm::APSInt Zero = ResultType.getZeroValue();
1229
1230 bool IsLHSPositiveOrZero = LHS.From() >= Zero;
1231 bool IsRHSPositiveOrZero = RHS.From() >= Zero;
1232
1233 bool IsLHSNegative = LHS.To() < Zero;
1234 bool IsRHSNegative = RHS.To() < Zero;
1235
1236 // Check if both ranges have the same sign.
1237 if ((IsLHSPositiveOrZero && IsRHSPositiveOrZero) ||
1238 (IsLHSNegative && IsRHSNegative)) {
1239 // The result is definitely greater or equal than any of the operands.
1240 const llvm::APSInt &Min = std::max(LHS.From(), RHS.From());
1241
1242 // We estimate maximal value for positives as the maximal value for the
1243 // given type. For negatives, we estimate it with -1 (e.g. 0x11111111).
1244 //
1245 // TODO: We basically, limit the resulting range from below, but don't do
1246 // anything with the upper bound.
1247 //
1248 // For positive operands, it can be done as follows: for the upper
1249 // bound of LHS and RHS we calculate the most significant bit set.
1250 // Let's call it the N-th bit. Then we can estimate the maximal
1251 // number to be 2^(N+1)-1, i.e. the number with all the bits up to
1252 // the N-th bit set.
1253 const llvm::APSInt &Max = IsLHSNegative
1254 ? ValueFactory.getValue(--Zero)
1255 : ValueFactory.getMaxValue(ResultType);
1256
1257 return {RangeFactory, ValueFactory.getValue(Min), Max};
1258 }
1259
1260 // Otherwise, let's check if at least one of the operands is negative.
1261 if (IsLHSNegative || IsRHSNegative) {
1262 // This means that the result is definitely negative as well.
1263 return {RangeFactory, ValueFactory.getMinValue(ResultType),
1264 ValueFactory.getValue(--Zero)};
1265 }
1266
1267 RangeSet DefaultRange = infer(T);
1268
1269 // It is pretty hard to reason about operands with different signs
1270 // (and especially with possibly different signs). We simply check if it
1271 // can be zero. In order to conclude that the result could not be zero,
1272 // at least one of the operands should be definitely not zero itself.
1273 if (!LHS.Includes(Zero) || !RHS.Includes(Zero)) {
1274 return assumeNonZero(DefaultRange, T);
1275 }
1276
1277 // Nothing much else to do here.
1278 return DefaultRange;
1279 }
1280
1281 template <>
VisitBinaryOperator(Range LHS,Range RHS,QualType T)1282 RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_And>(Range LHS,
1283 Range RHS,
1284 QualType T) {
1285 APSIntType ResultType = ValueFactory.getAPSIntType(T);
1286 llvm::APSInt Zero = ResultType.getZeroValue();
1287
1288 bool IsLHSPositiveOrZero = LHS.From() >= Zero;
1289 bool IsRHSPositiveOrZero = RHS.From() >= Zero;
1290
1291 bool IsLHSNegative = LHS.To() < Zero;
1292 bool IsRHSNegative = RHS.To() < Zero;
1293
1294 // Check if both ranges have the same sign.
1295 if ((IsLHSPositiveOrZero && IsRHSPositiveOrZero) ||
1296 (IsLHSNegative && IsRHSNegative)) {
1297 // The result is definitely less or equal than any of the operands.
1298 const llvm::APSInt &Max = std::min(LHS.To(), RHS.To());
1299
1300 // We conservatively estimate lower bound to be the smallest positive
1301 // or negative value corresponding to the sign of the operands.
1302 const llvm::APSInt &Min = IsLHSNegative
1303 ? ValueFactory.getMinValue(ResultType)
1304 : ValueFactory.getValue(Zero);
1305
1306 return {RangeFactory, Min, Max};
1307 }
1308
1309 // Otherwise, let's check if at least one of the operands is positive.
1310 if (IsLHSPositiveOrZero || IsRHSPositiveOrZero) {
1311 // This makes result definitely positive.
1312 //
1313 // We can also reason about a maximal value by finding the maximal
1314 // value of the positive operand.
1315 const llvm::APSInt &Max = IsLHSPositiveOrZero ? LHS.To() : RHS.To();
1316
1317 // The minimal value on the other hand is much harder to reason about.
1318 // The only thing we know for sure is that the result is positive.
1319 return {RangeFactory, ValueFactory.getValue(Zero),
1320 ValueFactory.getValue(Max)};
1321 }
1322
1323 // Nothing much else to do here.
1324 return infer(T);
1325 }
1326
1327 template <>
VisitBinaryOperator(Range LHS,Range RHS,QualType T)1328 RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Rem>(Range LHS,
1329 Range RHS,
1330 QualType T) {
1331 llvm::APSInt Zero = ValueFactory.getAPSIntType(T).getZeroValue();
1332
1333 Range ConservativeRange = getSymmetricalRange(RHS, T);
1334
1335 llvm::APSInt Max = ConservativeRange.To();
1336 llvm::APSInt Min = ConservativeRange.From();
1337
1338 if (Max == Zero) {
1339 // It's an undefined behaviour to divide by 0 and it seems like we know
1340 // for sure that RHS is 0. Let's say that the resulting range is
1341 // simply infeasible for that matter.
1342 return RangeFactory.getEmptySet();
1343 }
1344
1345 // At this point, our conservative range is closed. The result, however,
1346 // couldn't be greater than the RHS' maximal absolute value. Because of
1347 // this reason, we turn the range into open (or half-open in case of
1348 // unsigned integers).
1349 //
1350 // While we operate on integer values, an open interval (a, b) can be easily
1351 // represented by the closed interval [a + 1, b - 1]. And this is exactly
1352 // what we do next.
1353 //
1354 // If we are dealing with unsigned case, we shouldn't move the lower bound.
1355 if (Min.isSigned()) {
1356 ++Min;
1357 }
1358 --Max;
1359
1360 bool IsLHSPositiveOrZero = LHS.From() >= Zero;
1361 bool IsRHSPositiveOrZero = RHS.From() >= Zero;
1362
1363 // Remainder operator results with negative operands is implementation
1364 // defined. Positive cases are much easier to reason about though.
1365 if (IsLHSPositiveOrZero && IsRHSPositiveOrZero) {
1366 // If maximal value of LHS is less than maximal value of RHS,
1367 // the result won't get greater than LHS.To().
1368 Max = std::min(LHS.To(), Max);
1369 // We want to check if it is a situation similar to the following:
1370 //
1371 // <------------|---[ LHS ]--------[ RHS ]----->
1372 // -INF 0 +INF
1373 //
1374 // In this situation, we can conclude that (LHS / RHS) == 0 and
1375 // (LHS % RHS) == LHS.
1376 Min = LHS.To() < RHS.From() ? LHS.From() : Zero;
1377 }
1378
1379 // Nevertheless, the symmetrical range for RHS is a conservative estimate
1380 // for any sign of either LHS, or RHS.
1381 return {RangeFactory, ValueFactory.getValue(Min), ValueFactory.getValue(Max)};
1382 }
1383
1384 //===----------------------------------------------------------------------===//
1385 // Constraint assignment logic
1386 //===----------------------------------------------------------------------===//
1387
1388 /// ConstraintAssignorBase is a small utility class that unifies visitor
1389 /// for ranges with a visitor for constraints (rangeset/range/constant).
1390 ///
1391 /// It is designed to have one derived class, but generally it can have more.
1392 /// Derived class can control which types we handle by defining methods of the
1393 /// following form:
1394 ///
1395 /// bool handle${SYMBOL}To${CONSTRAINT}(const SYMBOL *Sym,
1396 /// CONSTRAINT Constraint);
1397 ///
1398 /// where SYMBOL is the type of the symbol (e.g. SymSymExpr, SymbolCast, etc.)
1399 /// CONSTRAINT is the type of constraint (RangeSet/Range/Const)
1400 /// return value signifies whether we should try other handle methods
1401 /// (i.e. false would mean to stop right after calling this method)
1402 template <class Derived> class ConstraintAssignorBase {
1403 public:
1404 using Const = const llvm::APSInt &;
1405
1406 #define DISPATCH(CLASS) return assign##CLASS##Impl(cast<CLASS>(Sym), Constraint)
1407
1408 #define ASSIGN(CLASS, TO, SYM, CONSTRAINT) \
1409 if (!static_cast<Derived *>(this)->assign##CLASS##To##TO(SYM, CONSTRAINT)) \
1410 return false
1411
assign(SymbolRef Sym,RangeSet Constraint)1412 void assign(SymbolRef Sym, RangeSet Constraint) {
1413 assignImpl(Sym, Constraint);
1414 }
1415
assignImpl(SymbolRef Sym,RangeSet Constraint)1416 bool assignImpl(SymbolRef Sym, RangeSet Constraint) {
1417 switch (Sym->getKind()) {
1418 #define SYMBOL(Id, Parent) \
1419 case SymExpr::Id##Kind: \
1420 DISPATCH(Id);
1421 #include "clang/StaticAnalyzer/Core/PathSensitive/Symbols.def"
1422 }
1423 llvm_unreachable("Unknown SymExpr kind!");
1424 }
1425
1426 #define DEFAULT_ASSIGN(Id) \
1427 bool assign##Id##To##RangeSet(const Id *Sym, RangeSet Constraint) { \
1428 return true; \
1429 } \
1430 bool assign##Id##To##Range(const Id *Sym, Range Constraint) { return true; } \
1431 bool assign##Id##To##Const(const Id *Sym, Const Constraint) { return true; }
1432
1433 // When we dispatch for constraint types, we first try to check
1434 // if the new constraint is the constant and try the corresponding
1435 // assignor methods. If it didn't interrupt, we can proceed to the
1436 // range, and finally to the range set.
1437 #define CONSTRAINT_DISPATCH(Id) \
1438 if (const llvm::APSInt *Const = Constraint.getConcreteValue()) { \
1439 ASSIGN(Id, Const, Sym, *Const); \
1440 } \
1441 if (Constraint.size() == 1) { \
1442 ASSIGN(Id, Range, Sym, *Constraint.begin()); \
1443 } \
1444 ASSIGN(Id, RangeSet, Sym, Constraint)
1445
1446 // Our internal assign method first tries to call assignor methods for all
1447 // constraint types that apply. And if not interrupted, continues with its
1448 // parent class.
1449 #define SYMBOL(Id, Parent) \
1450 bool assign##Id##Impl(const Id *Sym, RangeSet Constraint) { \
1451 CONSTRAINT_DISPATCH(Id); \
1452 DISPATCH(Parent); \
1453 } \
1454 DEFAULT_ASSIGN(Id)
1455 #define ABSTRACT_SYMBOL(Id, Parent) SYMBOL(Id, Parent)
1456 #include "clang/StaticAnalyzer/Core/PathSensitive/Symbols.def"
1457
1458 // Default implementations for the top class that doesn't have parents.
assignSymExprImpl(const SymExpr * Sym,RangeSet Constraint)1459 bool assignSymExprImpl(const SymExpr *Sym, RangeSet Constraint) {
1460 CONSTRAINT_DISPATCH(SymExpr);
1461 return true;
1462 }
1463 DEFAULT_ASSIGN(SymExpr);
1464
1465 #undef DISPATCH
1466 #undef CONSTRAINT_DISPATCH
1467 #undef DEFAULT_ASSIGN
1468 #undef ASSIGN
1469 };
1470
1471 /// A little component aggregating all of the reasoning we have about
1472 /// assigning new constraints to symbols.
1473 ///
1474 /// The main purpose of this class is to associate constraints to symbols,
1475 /// and impose additional constraints on other symbols, when we can imply
1476 /// them.
1477 ///
1478 /// It has a nice symmetry with SymbolicRangeInferrer. When the latter
1479 /// can provide more precise ranges by looking into the operands of the
1480 /// expression in question, ConstraintAssignor looks into the operands
1481 /// to see if we can imply more from the new constraint.
1482 class ConstraintAssignor : public ConstraintAssignorBase<ConstraintAssignor> {
1483 public:
1484 template <class ClassOrSymbol>
1485 LLVM_NODISCARD static ProgramStateRef
assign(ProgramStateRef State,SValBuilder & Builder,RangeSet::Factory & F,ClassOrSymbol CoS,RangeSet NewConstraint)1486 assign(ProgramStateRef State, SValBuilder &Builder, RangeSet::Factory &F,
1487 ClassOrSymbol CoS, RangeSet NewConstraint) {
1488 if (!State || NewConstraint.isEmpty())
1489 return nullptr;
1490
1491 ConstraintAssignor Assignor{State, Builder, F};
1492 return Assignor.assign(CoS, NewConstraint);
1493 }
1494
1495 inline bool assignSymExprToConst(const SymExpr *Sym, Const Constraint);
1496 inline bool assignSymSymExprToRangeSet(const SymSymExpr *Sym,
1497 RangeSet Constraint);
1498
1499 private:
ConstraintAssignor(ProgramStateRef State,SValBuilder & Builder,RangeSet::Factory & F)1500 ConstraintAssignor(ProgramStateRef State, SValBuilder &Builder,
1501 RangeSet::Factory &F)
1502 : State(State), Builder(Builder), RangeFactory(F) {}
1503 using Base = ConstraintAssignorBase<ConstraintAssignor>;
1504
1505 /// Base method for handling new constraints for symbols.
assign(SymbolRef Sym,RangeSet NewConstraint)1506 LLVM_NODISCARD ProgramStateRef assign(SymbolRef Sym, RangeSet NewConstraint) {
1507 // All constraints are actually associated with equivalence classes, and
1508 // that's what we are going to do first.
1509 State = assign(EquivalenceClass::find(State, Sym), NewConstraint);
1510 if (!State)
1511 return nullptr;
1512
1513 // And after that we can check what other things we can get from this
1514 // constraint.
1515 Base::assign(Sym, NewConstraint);
1516 return State;
1517 }
1518
1519 /// Base method for handling new constraints for classes.
assign(EquivalenceClass Class,RangeSet NewConstraint)1520 LLVM_NODISCARD ProgramStateRef assign(EquivalenceClass Class,
1521 RangeSet NewConstraint) {
1522 // There is a chance that we might need to update constraints for the
1523 // classes that are known to be disequal to Class.
1524 //
1525 // In order for this to be even possible, the new constraint should
1526 // be simply a constant because we can't reason about range disequalities.
1527 if (const llvm::APSInt *Point = NewConstraint.getConcreteValue()) {
1528
1529 ConstraintRangeTy Constraints = State->get<ConstraintRange>();
1530 ConstraintRangeTy::Factory &CF = State->get_context<ConstraintRange>();
1531
1532 // Add new constraint.
1533 Constraints = CF.add(Constraints, Class, NewConstraint);
1534
1535 for (EquivalenceClass DisequalClass : Class.getDisequalClasses(State)) {
1536 RangeSet UpdatedConstraint = SymbolicRangeInferrer::inferRange(
1537 RangeFactory, State, DisequalClass);
1538
1539 UpdatedConstraint = RangeFactory.deletePoint(UpdatedConstraint, *Point);
1540
1541 // If we end up with at least one of the disequal classes to be
1542 // constrained with an empty range-set, the state is infeasible.
1543 if (UpdatedConstraint.isEmpty())
1544 return nullptr;
1545
1546 Constraints = CF.add(Constraints, DisequalClass, UpdatedConstraint);
1547 }
1548 assert(areFeasible(Constraints) && "Constraint manager shouldn't produce "
1549 "a state with infeasible constraints");
1550
1551 return setConstraints(State, Constraints);
1552 }
1553
1554 return setConstraint(State, Class, NewConstraint);
1555 }
1556
trackDisequality(ProgramStateRef State,SymbolRef LHS,SymbolRef RHS)1557 ProgramStateRef trackDisequality(ProgramStateRef State, SymbolRef LHS,
1558 SymbolRef RHS) {
1559 return EquivalenceClass::markDisequal(RangeFactory, State, LHS, RHS);
1560 }
1561
trackEquality(ProgramStateRef State,SymbolRef LHS,SymbolRef RHS)1562 ProgramStateRef trackEquality(ProgramStateRef State, SymbolRef LHS,
1563 SymbolRef RHS) {
1564 return EquivalenceClass::merge(RangeFactory, State, LHS, RHS);
1565 }
1566
interpreteAsBool(RangeSet Constraint)1567 LLVM_NODISCARD Optional<bool> interpreteAsBool(RangeSet Constraint) {
1568 assert(!Constraint.isEmpty() && "Empty ranges shouldn't get here");
1569
1570 if (Constraint.getConcreteValue())
1571 return !Constraint.getConcreteValue()->isNullValue();
1572
1573 APSIntType T{Constraint.getMinValue()};
1574 Const Zero = T.getZeroValue();
1575 if (!Constraint.contains(Zero))
1576 return true;
1577
1578 return llvm::None;
1579 }
1580
1581 ProgramStateRef State;
1582 SValBuilder &Builder;
1583 RangeSet::Factory &RangeFactory;
1584 };
1585
1586 //===----------------------------------------------------------------------===//
1587 // Constraint manager implementation details
1588 //===----------------------------------------------------------------------===//
1589
1590 class RangeConstraintManager : public RangedConstraintManager {
1591 public:
RangeConstraintManager(ExprEngine * EE,SValBuilder & SVB)1592 RangeConstraintManager(ExprEngine *EE, SValBuilder &SVB)
1593 : RangedConstraintManager(EE, SVB), F(getBasicVals()) {}
1594
1595 //===------------------------------------------------------------------===//
1596 // Implementation for interface from ConstraintManager.
1597 //===------------------------------------------------------------------===//
1598
haveEqualConstraints(ProgramStateRef S1,ProgramStateRef S2) const1599 bool haveEqualConstraints(ProgramStateRef S1,
1600 ProgramStateRef S2) const override {
1601 // NOTE: ClassMembers are as simple as back pointers for ClassMap,
1602 // so comparing constraint ranges and class maps should be
1603 // sufficient.
1604 return S1->get<ConstraintRange>() == S2->get<ConstraintRange>() &&
1605 S1->get<ClassMap>() == S2->get<ClassMap>();
1606 }
1607
1608 bool canReasonAbout(SVal X) const override;
1609
1610 ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
1611
1612 const llvm::APSInt *getSymVal(ProgramStateRef State,
1613 SymbolRef Sym) const override;
1614
1615 ProgramStateRef removeDeadBindings(ProgramStateRef State,
1616 SymbolReaper &SymReaper) override;
1617
1618 void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL = "\n",
1619 unsigned int Space = 0, bool IsDot = false) const override;
1620 void printConstraints(raw_ostream &Out, ProgramStateRef State,
1621 const char *NL = "\n", unsigned int Space = 0,
1622 bool IsDot = false) const;
1623 void printEquivalenceClasses(raw_ostream &Out, ProgramStateRef State,
1624 const char *NL = "\n", unsigned int Space = 0,
1625 bool IsDot = false) const;
1626 void printDisequalities(raw_ostream &Out, ProgramStateRef State,
1627 const char *NL = "\n", unsigned int Space = 0,
1628 bool IsDot = false) const;
1629
1630 //===------------------------------------------------------------------===//
1631 // Implementation for interface from RangedConstraintManager.
1632 //===------------------------------------------------------------------===//
1633
1634 ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,
1635 const llvm::APSInt &V,
1636 const llvm::APSInt &Adjustment) override;
1637
1638 ProgramStateRef assumeSymEQ(ProgramStateRef State, SymbolRef Sym,
1639 const llvm::APSInt &V,
1640 const llvm::APSInt &Adjustment) override;
1641
1642 ProgramStateRef assumeSymLT(ProgramStateRef State, SymbolRef Sym,
1643 const llvm::APSInt &V,
1644 const llvm::APSInt &Adjustment) override;
1645
1646 ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym,
1647 const llvm::APSInt &V,
1648 const llvm::APSInt &Adjustment) override;
1649
1650 ProgramStateRef assumeSymLE(ProgramStateRef State, SymbolRef Sym,
1651 const llvm::APSInt &V,
1652 const llvm::APSInt &Adjustment) override;
1653
1654 ProgramStateRef assumeSymGE(ProgramStateRef State, SymbolRef Sym,
1655 const llvm::APSInt &V,
1656 const llvm::APSInt &Adjustment) override;
1657
1658 ProgramStateRef assumeSymWithinInclusiveRange(
1659 ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
1660 const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
1661
1662 ProgramStateRef assumeSymOutsideInclusiveRange(
1663 ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
1664 const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
1665
1666 private:
1667 RangeSet::Factory F;
1668
1669 RangeSet getRange(ProgramStateRef State, SymbolRef Sym);
1670 RangeSet getRange(ProgramStateRef State, EquivalenceClass Class);
1671 ProgramStateRef setRange(ProgramStateRef State, SymbolRef Sym,
1672 RangeSet Range);
1673 ProgramStateRef setRange(ProgramStateRef State, EquivalenceClass Class,
1674 RangeSet Range);
1675
1676 RangeSet getSymLTRange(ProgramStateRef St, SymbolRef Sym,
1677 const llvm::APSInt &Int,
1678 const llvm::APSInt &Adjustment);
1679 RangeSet getSymGTRange(ProgramStateRef St, SymbolRef Sym,
1680 const llvm::APSInt &Int,
1681 const llvm::APSInt &Adjustment);
1682 RangeSet getSymLERange(ProgramStateRef St, SymbolRef Sym,
1683 const llvm::APSInt &Int,
1684 const llvm::APSInt &Adjustment);
1685 RangeSet getSymLERange(llvm::function_ref<RangeSet()> RS,
1686 const llvm::APSInt &Int,
1687 const llvm::APSInt &Adjustment);
1688 RangeSet getSymGERange(ProgramStateRef St, SymbolRef Sym,
1689 const llvm::APSInt &Int,
1690 const llvm::APSInt &Adjustment);
1691 };
1692
assignSymExprToConst(const SymExpr * Sym,const llvm::APSInt & Constraint)1693 bool ConstraintAssignor::assignSymExprToConst(const SymExpr *Sym,
1694 const llvm::APSInt &Constraint) {
1695 llvm::SmallSet<EquivalenceClass, 4> SimplifiedClasses;
1696 // Iterate over all equivalence classes and try to simplify them.
1697 ClassMembersTy Members = State->get<ClassMembers>();
1698 for (std::pair<EquivalenceClass, SymbolSet> ClassToSymbolSet : Members) {
1699 EquivalenceClass Class = ClassToSymbolSet.first;
1700 State = EquivalenceClass::simplify(Builder, RangeFactory, State, Class);
1701 if (!State)
1702 return false;
1703 SimplifiedClasses.insert(Class);
1704 }
1705
1706 // Trivial equivalence classes (those that have only one symbol member) are
1707 // not stored in the State. Thus, we must skim through the constraints as
1708 // well. And we try to simplify symbols in the constraints.
1709 ConstraintRangeTy Constraints = State->get<ConstraintRange>();
1710 for (std::pair<EquivalenceClass, RangeSet> ClassConstraint : Constraints) {
1711 EquivalenceClass Class = ClassConstraint.first;
1712 if (SimplifiedClasses.count(Class)) // Already simplified.
1713 continue;
1714 State = EquivalenceClass::simplify(Builder, RangeFactory, State, Class);
1715 if (!State)
1716 return false;
1717 }
1718
1719 return true;
1720 }
1721
assignSymSymExprToRangeSet(const SymSymExpr * Sym,RangeSet Constraint)1722 bool ConstraintAssignor::assignSymSymExprToRangeSet(const SymSymExpr *Sym,
1723 RangeSet Constraint) {
1724 Optional<bool> ConstraintAsBool = interpreteAsBool(Constraint);
1725
1726 if (!ConstraintAsBool)
1727 return true;
1728
1729 if (Optional<bool> Equality = meansEquality(Sym)) {
1730 // Here we cover two cases:
1731 // * if Sym is equality and the new constraint is true -> Sym's operands
1732 // should be marked as equal
1733 // * if Sym is disequality and the new constraint is false -> Sym's
1734 // operands should be also marked as equal
1735 if (*Equality == *ConstraintAsBool) {
1736 State = trackEquality(State, Sym->getLHS(), Sym->getRHS());
1737 } else {
1738 // Other combinations leave as with disequal operands.
1739 State = trackDisequality(State, Sym->getLHS(), Sym->getRHS());
1740 }
1741
1742 if (!State)
1743 return false;
1744 }
1745
1746 return true;
1747 }
1748
1749 } // end anonymous namespace
1750
1751 std::unique_ptr<ConstraintManager>
CreateRangeConstraintManager(ProgramStateManager & StMgr,ExprEngine * Eng)1752 ento::CreateRangeConstraintManager(ProgramStateManager &StMgr,
1753 ExprEngine *Eng) {
1754 return std::make_unique<RangeConstraintManager>(Eng, StMgr.getSValBuilder());
1755 }
1756
getConstraintMap(ProgramStateRef State)1757 ConstraintMap ento::getConstraintMap(ProgramStateRef State) {
1758 ConstraintMap::Factory &F = State->get_context<ConstraintMap>();
1759 ConstraintMap Result = F.getEmptyMap();
1760
1761 ConstraintRangeTy Constraints = State->get<ConstraintRange>();
1762 for (std::pair<EquivalenceClass, RangeSet> ClassConstraint : Constraints) {
1763 EquivalenceClass Class = ClassConstraint.first;
1764 SymbolSet ClassMembers = Class.getClassMembers(State);
1765 assert(!ClassMembers.isEmpty() &&
1766 "Class must always have at least one member!");
1767
1768 SymbolRef Representative = *ClassMembers.begin();
1769 Result = F.add(Result, Representative, ClassConstraint.second);
1770 }
1771
1772 return Result;
1773 }
1774
1775 //===----------------------------------------------------------------------===//
1776 // EqualityClass implementation details
1777 //===----------------------------------------------------------------------===//
1778
dumpToStream(ProgramStateRef State,raw_ostream & os) const1779 LLVM_DUMP_METHOD void EquivalenceClass::dumpToStream(ProgramStateRef State,
1780 raw_ostream &os) const {
1781 SymbolSet ClassMembers = getClassMembers(State);
1782 for (const SymbolRef &MemberSym : ClassMembers) {
1783 MemberSym->dump();
1784 os << "\n";
1785 }
1786 }
1787
find(ProgramStateRef State,SymbolRef Sym)1788 inline EquivalenceClass EquivalenceClass::find(ProgramStateRef State,
1789 SymbolRef Sym) {
1790 assert(State && "State should not be null");
1791 assert(Sym && "Symbol should not be null");
1792 // We store far from all Symbol -> Class mappings
1793 if (const EquivalenceClass *NontrivialClass = State->get<ClassMap>(Sym))
1794 return *NontrivialClass;
1795
1796 // This is a trivial class of Sym.
1797 return Sym;
1798 }
1799
merge(RangeSet::Factory & F,ProgramStateRef State,SymbolRef First,SymbolRef Second)1800 inline ProgramStateRef EquivalenceClass::merge(RangeSet::Factory &F,
1801 ProgramStateRef State,
1802 SymbolRef First,
1803 SymbolRef Second) {
1804 EquivalenceClass FirstClass = find(State, First);
1805 EquivalenceClass SecondClass = find(State, Second);
1806
1807 return FirstClass.merge(F, State, SecondClass);
1808 }
1809
merge(RangeSet::Factory & F,ProgramStateRef State,EquivalenceClass Other)1810 inline ProgramStateRef EquivalenceClass::merge(RangeSet::Factory &F,
1811 ProgramStateRef State,
1812 EquivalenceClass Other) {
1813 // It is already the same class.
1814 if (*this == Other)
1815 return State;
1816
1817 // FIXME: As of now, we support only equivalence classes of the same type.
1818 // This limitation is connected to the lack of explicit casts in
1819 // our symbolic expression model.
1820 //
1821 // That means that for `int x` and `char y` we don't distinguish
1822 // between these two very different cases:
1823 // * `x == y`
1824 // * `(char)x == y`
1825 //
1826 // The moment we introduce symbolic casts, this restriction can be
1827 // lifted.
1828 if (getType() != Other.getType())
1829 return State;
1830
1831 SymbolSet Members = getClassMembers(State);
1832 SymbolSet OtherMembers = Other.getClassMembers(State);
1833
1834 // We estimate the size of the class by the height of tree containing
1835 // its members. Merging is not a trivial operation, so it's easier to
1836 // merge the smaller class into the bigger one.
1837 if (Members.getHeight() >= OtherMembers.getHeight()) {
1838 return mergeImpl(F, State, Members, Other, OtherMembers);
1839 } else {
1840 return Other.mergeImpl(F, State, OtherMembers, *this, Members);
1841 }
1842 }
1843
1844 inline ProgramStateRef
mergeImpl(RangeSet::Factory & RangeFactory,ProgramStateRef State,SymbolSet MyMembers,EquivalenceClass Other,SymbolSet OtherMembers)1845 EquivalenceClass::mergeImpl(RangeSet::Factory &RangeFactory,
1846 ProgramStateRef State, SymbolSet MyMembers,
1847 EquivalenceClass Other, SymbolSet OtherMembers) {
1848 // Essentially what we try to recreate here is some kind of union-find
1849 // data structure. It does have certain limitations due to persistence
1850 // and the need to remove elements from classes.
1851 //
1852 // In this setting, EquialityClass object is the representative of the class
1853 // or the parent element. ClassMap is a mapping of class members to their
1854 // parent. Unlike the union-find structure, they all point directly to the
1855 // class representative because we don't have an opportunity to actually do
1856 // path compression when dealing with immutability. This means that we
1857 // compress paths every time we do merges. It also means that we lose
1858 // the main amortized complexity benefit from the original data structure.
1859 ConstraintRangeTy Constraints = State->get<ConstraintRange>();
1860 ConstraintRangeTy::Factory &CRF = State->get_context<ConstraintRange>();
1861
1862 // 1. If the merged classes have any constraints associated with them, we
1863 // need to transfer them to the class we have left.
1864 //
1865 // Intersection here makes perfect sense because both of these constraints
1866 // must hold for the whole new class.
1867 if (Optional<RangeSet> NewClassConstraint =
1868 intersect(RangeFactory, getConstraint(State, *this),
1869 getConstraint(State, Other))) {
1870 // NOTE: Essentially, NewClassConstraint should NEVER be infeasible because
1871 // range inferrer shouldn't generate ranges incompatible with
1872 // equivalence classes. However, at the moment, due to imperfections
1873 // in the solver, it is possible and the merge function can also
1874 // return infeasible states aka null states.
1875 if (NewClassConstraint->isEmpty())
1876 // Infeasible state
1877 return nullptr;
1878
1879 // No need in tracking constraints of a now-dissolved class.
1880 Constraints = CRF.remove(Constraints, Other);
1881 // Assign new constraints for this class.
1882 Constraints = CRF.add(Constraints, *this, *NewClassConstraint);
1883
1884 assert(areFeasible(Constraints) && "Constraint manager shouldn't produce "
1885 "a state with infeasible constraints");
1886
1887 State = State->set<ConstraintRange>(Constraints);
1888 }
1889
1890 // 2. Get ALL equivalence-related maps
1891 ClassMapTy Classes = State->get<ClassMap>();
1892 ClassMapTy::Factory &CMF = State->get_context<ClassMap>();
1893
1894 ClassMembersTy Members = State->get<ClassMembers>();
1895 ClassMembersTy::Factory &MF = State->get_context<ClassMembers>();
1896
1897 DisequalityMapTy DisequalityInfo = State->get<DisequalityMap>();
1898 DisequalityMapTy::Factory &DF = State->get_context<DisequalityMap>();
1899
1900 ClassSet::Factory &CF = State->get_context<ClassSet>();
1901 SymbolSet::Factory &F = getMembersFactory(State);
1902
1903 // 2. Merge members of the Other class into the current class.
1904 SymbolSet NewClassMembers = MyMembers;
1905 for (SymbolRef Sym : OtherMembers) {
1906 NewClassMembers = F.add(NewClassMembers, Sym);
1907 // *this is now the class for all these new symbols.
1908 Classes = CMF.add(Classes, Sym, *this);
1909 }
1910
1911 // 3. Adjust member mapping.
1912 //
1913 // No need in tracking members of a now-dissolved class.
1914 Members = MF.remove(Members, Other);
1915 // Now only the current class is mapped to all the symbols.
1916 Members = MF.add(Members, *this, NewClassMembers);
1917
1918 // 4. Update disequality relations
1919 ClassSet DisequalToOther = Other.getDisequalClasses(DisequalityInfo, CF);
1920 // We are about to merge two classes but they are already known to be
1921 // non-equal. This is a contradiction.
1922 if (DisequalToOther.contains(*this))
1923 return nullptr;
1924
1925 if (!DisequalToOther.isEmpty()) {
1926 ClassSet DisequalToThis = getDisequalClasses(DisequalityInfo, CF);
1927 DisequalityInfo = DF.remove(DisequalityInfo, Other);
1928
1929 for (EquivalenceClass DisequalClass : DisequalToOther) {
1930 DisequalToThis = CF.add(DisequalToThis, DisequalClass);
1931
1932 // Disequality is a symmetric relation meaning that if
1933 // DisequalToOther not null then the set for DisequalClass is not
1934 // empty and has at least Other.
1935 ClassSet OriginalSetLinkedToOther =
1936 *DisequalityInfo.lookup(DisequalClass);
1937
1938 // Other will be eliminated and we should replace it with the bigger
1939 // united class.
1940 ClassSet NewSet = CF.remove(OriginalSetLinkedToOther, Other);
1941 NewSet = CF.add(NewSet, *this);
1942
1943 DisequalityInfo = DF.add(DisequalityInfo, DisequalClass, NewSet);
1944 }
1945
1946 DisequalityInfo = DF.add(DisequalityInfo, *this, DisequalToThis);
1947 State = State->set<DisequalityMap>(DisequalityInfo);
1948 }
1949
1950 // 5. Update the state
1951 State = State->set<ClassMap>(Classes);
1952 State = State->set<ClassMembers>(Members);
1953
1954 return State;
1955 }
1956
1957 inline SymbolSet::Factory &
getMembersFactory(ProgramStateRef State)1958 EquivalenceClass::getMembersFactory(ProgramStateRef State) {
1959 return State->get_context<SymbolSet>();
1960 }
1961
getClassMembers(ProgramStateRef State) const1962 SymbolSet EquivalenceClass::getClassMembers(ProgramStateRef State) const {
1963 if (const SymbolSet *Members = State->get<ClassMembers>(*this))
1964 return *Members;
1965
1966 // This class is trivial, so we need to construct a set
1967 // with just that one symbol from the class.
1968 SymbolSet::Factory &F = getMembersFactory(State);
1969 return F.add(F.getEmptySet(), getRepresentativeSymbol());
1970 }
1971
isTrivial(ProgramStateRef State) const1972 bool EquivalenceClass::isTrivial(ProgramStateRef State) const {
1973 return State->get<ClassMembers>(*this) == nullptr;
1974 }
1975
isTriviallyDead(ProgramStateRef State,SymbolReaper & Reaper) const1976 bool EquivalenceClass::isTriviallyDead(ProgramStateRef State,
1977 SymbolReaper &Reaper) const {
1978 return isTrivial(State) && Reaper.isDead(getRepresentativeSymbol());
1979 }
1980
markDisequal(RangeSet::Factory & RF,ProgramStateRef State,SymbolRef First,SymbolRef Second)1981 inline ProgramStateRef EquivalenceClass::markDisequal(RangeSet::Factory &RF,
1982 ProgramStateRef State,
1983 SymbolRef First,
1984 SymbolRef Second) {
1985 return markDisequal(RF, State, find(State, First), find(State, Second));
1986 }
1987
markDisequal(RangeSet::Factory & RF,ProgramStateRef State,EquivalenceClass First,EquivalenceClass Second)1988 inline ProgramStateRef EquivalenceClass::markDisequal(RangeSet::Factory &RF,
1989 ProgramStateRef State,
1990 EquivalenceClass First,
1991 EquivalenceClass Second) {
1992 return First.markDisequal(RF, State, Second);
1993 }
1994
1995 inline ProgramStateRef
markDisequal(RangeSet::Factory & RF,ProgramStateRef State,EquivalenceClass Other) const1996 EquivalenceClass::markDisequal(RangeSet::Factory &RF, ProgramStateRef State,
1997 EquivalenceClass Other) const {
1998 // If we know that two classes are equal, we can only produce an infeasible
1999 // state.
2000 if (*this == Other) {
2001 return nullptr;
2002 }
2003
2004 DisequalityMapTy DisequalityInfo = State->get<DisequalityMap>();
2005 ConstraintRangeTy Constraints = State->get<ConstraintRange>();
2006
2007 // Disequality is a symmetric relation, so if we mark A as disequal to B,
2008 // we should also mark B as disequalt to A.
2009 if (!addToDisequalityInfo(DisequalityInfo, Constraints, RF, State, *this,
2010 Other) ||
2011 !addToDisequalityInfo(DisequalityInfo, Constraints, RF, State, Other,
2012 *this))
2013 return nullptr;
2014
2015 assert(areFeasible(Constraints) && "Constraint manager shouldn't produce "
2016 "a state with infeasible constraints");
2017
2018 State = State->set<DisequalityMap>(DisequalityInfo);
2019 State = State->set<ConstraintRange>(Constraints);
2020
2021 return State;
2022 }
2023
addToDisequalityInfo(DisequalityMapTy & Info,ConstraintRangeTy & Constraints,RangeSet::Factory & RF,ProgramStateRef State,EquivalenceClass First,EquivalenceClass Second)2024 inline bool EquivalenceClass::addToDisequalityInfo(
2025 DisequalityMapTy &Info, ConstraintRangeTy &Constraints,
2026 RangeSet::Factory &RF, ProgramStateRef State, EquivalenceClass First,
2027 EquivalenceClass Second) {
2028
2029 // 1. Get all of the required factories.
2030 DisequalityMapTy::Factory &F = State->get_context<DisequalityMap>();
2031 ClassSet::Factory &CF = State->get_context<ClassSet>();
2032 ConstraintRangeTy::Factory &CRF = State->get_context<ConstraintRange>();
2033
2034 // 2. Add Second to the set of classes disequal to First.
2035 const ClassSet *CurrentSet = Info.lookup(First);
2036 ClassSet NewSet = CurrentSet ? *CurrentSet : CF.getEmptySet();
2037 NewSet = CF.add(NewSet, Second);
2038
2039 Info = F.add(Info, First, NewSet);
2040
2041 // 3. If Second is known to be a constant, we can delete this point
2042 // from the constraint asociated with First.
2043 //
2044 // So, if Second == 10, it means that First != 10.
2045 // At the same time, the same logic does not apply to ranges.
2046 if (const RangeSet *SecondConstraint = Constraints.lookup(Second))
2047 if (const llvm::APSInt *Point = SecondConstraint->getConcreteValue()) {
2048
2049 RangeSet FirstConstraint = SymbolicRangeInferrer::inferRange(
2050 RF, State, First.getRepresentativeSymbol());
2051
2052 FirstConstraint = RF.deletePoint(FirstConstraint, *Point);
2053
2054 // If the First class is about to be constrained with an empty
2055 // range-set, the state is infeasible.
2056 if (FirstConstraint.isEmpty())
2057 return false;
2058
2059 Constraints = CRF.add(Constraints, First, FirstConstraint);
2060 }
2061
2062 return true;
2063 }
2064
areEqual(ProgramStateRef State,SymbolRef FirstSym,SymbolRef SecondSym)2065 inline Optional<bool> EquivalenceClass::areEqual(ProgramStateRef State,
2066 SymbolRef FirstSym,
2067 SymbolRef SecondSym) {
2068 return EquivalenceClass::areEqual(State, find(State, FirstSym),
2069 find(State, SecondSym));
2070 }
2071
areEqual(ProgramStateRef State,EquivalenceClass First,EquivalenceClass Second)2072 inline Optional<bool> EquivalenceClass::areEqual(ProgramStateRef State,
2073 EquivalenceClass First,
2074 EquivalenceClass Second) {
2075 // The same equivalence class => symbols are equal.
2076 if (First == Second)
2077 return true;
2078
2079 // Let's check if we know anything about these two classes being not equal to
2080 // each other.
2081 ClassSet DisequalToFirst = First.getDisequalClasses(State);
2082 if (DisequalToFirst.contains(Second))
2083 return false;
2084
2085 // It is not clear.
2086 return llvm::None;
2087 }
2088
2089 // Iterate over all symbols and try to simplify them. Once a symbol is
2090 // simplified then we check if we can merge the simplified symbol's equivalence
2091 // class to this class. This way, we simplify not just the symbols but the
2092 // classes as well: we strive to keep the number of the classes to be the
2093 // absolute minimum.
2094 LLVM_NODISCARD ProgramStateRef
simplify(SValBuilder & SVB,RangeSet::Factory & F,ProgramStateRef State,EquivalenceClass Class)2095 EquivalenceClass::simplify(SValBuilder &SVB, RangeSet::Factory &F,
2096 ProgramStateRef State, EquivalenceClass Class) {
2097 SymbolSet ClassMembers = Class.getClassMembers(State);
2098 for (const SymbolRef &MemberSym : ClassMembers) {
2099 SymbolRef SimplifiedMemberSym = ento::simplify(State, MemberSym);
2100 if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) {
2101 // The simplified symbol should be the member of the original Class,
2102 // however, it might be in another existing class at the moment. We
2103 // have to merge these classes.
2104 State = merge(F, State, MemberSym, SimplifiedMemberSym);
2105 if (!State)
2106 return nullptr;
2107 }
2108 }
2109 return State;
2110 }
2111
getDisequalClasses(ProgramStateRef State,SymbolRef Sym)2112 inline ClassSet EquivalenceClass::getDisequalClasses(ProgramStateRef State,
2113 SymbolRef Sym) {
2114 return find(State, Sym).getDisequalClasses(State);
2115 }
2116
2117 inline ClassSet
getDisequalClasses(ProgramStateRef State) const2118 EquivalenceClass::getDisequalClasses(ProgramStateRef State) const {
2119 return getDisequalClasses(State->get<DisequalityMap>(),
2120 State->get_context<ClassSet>());
2121 }
2122
2123 inline ClassSet
getDisequalClasses(DisequalityMapTy Map,ClassSet::Factory & Factory) const2124 EquivalenceClass::getDisequalClasses(DisequalityMapTy Map,
2125 ClassSet::Factory &Factory) const {
2126 if (const ClassSet *DisequalClasses = Map.lookup(*this))
2127 return *DisequalClasses;
2128
2129 return Factory.getEmptySet();
2130 }
2131
isClassDataConsistent(ProgramStateRef State)2132 bool EquivalenceClass::isClassDataConsistent(ProgramStateRef State) {
2133 ClassMembersTy Members = State->get<ClassMembers>();
2134
2135 for (std::pair<EquivalenceClass, SymbolSet> ClassMembersPair : Members) {
2136 for (SymbolRef Member : ClassMembersPair.second) {
2137 // Every member of the class should have a mapping back to the class.
2138 if (find(State, Member) == ClassMembersPair.first) {
2139 continue;
2140 }
2141
2142 return false;
2143 }
2144 }
2145
2146 DisequalityMapTy Disequalities = State->get<DisequalityMap>();
2147 for (std::pair<EquivalenceClass, ClassSet> DisequalityInfo : Disequalities) {
2148 EquivalenceClass Class = DisequalityInfo.first;
2149 ClassSet DisequalClasses = DisequalityInfo.second;
2150
2151 // There is no use in keeping empty sets in the map.
2152 if (DisequalClasses.isEmpty())
2153 return false;
2154
2155 // Disequality is symmetrical, i.e. for every Class A and B that A != B,
2156 // B != A should also be true.
2157 for (EquivalenceClass DisequalClass : DisequalClasses) {
2158 const ClassSet *DisequalToDisequalClasses =
2159 Disequalities.lookup(DisequalClass);
2160
2161 // It should be a set of at least one element: Class
2162 if (!DisequalToDisequalClasses ||
2163 !DisequalToDisequalClasses->contains(Class))
2164 return false;
2165 }
2166 }
2167
2168 return true;
2169 }
2170
2171 //===----------------------------------------------------------------------===//
2172 // RangeConstraintManager implementation
2173 //===----------------------------------------------------------------------===//
2174
canReasonAbout(SVal X) const2175 bool RangeConstraintManager::canReasonAbout(SVal X) const {
2176 Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
2177 if (SymVal && SymVal->isExpression()) {
2178 const SymExpr *SE = SymVal->getSymbol();
2179
2180 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
2181 switch (SIE->getOpcode()) {
2182 // We don't reason yet about bitwise-constraints on symbolic values.
2183 case BO_And:
2184 case BO_Or:
2185 case BO_Xor:
2186 return false;
2187 // We don't reason yet about these arithmetic constraints on
2188 // symbolic values.
2189 case BO_Mul:
2190 case BO_Div:
2191 case BO_Rem:
2192 case BO_Shl:
2193 case BO_Shr:
2194 return false;
2195 // All other cases.
2196 default:
2197 return true;
2198 }
2199 }
2200
2201 if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
2202 // FIXME: Handle <=> here.
2203 if (BinaryOperator::isEqualityOp(SSE->getOpcode()) ||
2204 BinaryOperator::isRelationalOp(SSE->getOpcode())) {
2205 // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
2206 // We've recently started producing Loc <> NonLoc comparisons (that
2207 // result from casts of one of the operands between eg. intptr_t and
2208 // void *), but we can't reason about them yet.
2209 if (Loc::isLocType(SSE->getLHS()->getType())) {
2210 return Loc::isLocType(SSE->getRHS()->getType());
2211 }
2212 }
2213 }
2214
2215 return false;
2216 }
2217
2218 return true;
2219 }
2220
checkNull(ProgramStateRef State,SymbolRef Sym)2221 ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State,
2222 SymbolRef Sym) {
2223 const RangeSet *Ranges = getConstraint(State, Sym);
2224
2225 // If we don't have any information about this symbol, it's underconstrained.
2226 if (!Ranges)
2227 return ConditionTruthVal();
2228
2229 // If we have a concrete value, see if it's zero.
2230 if (const llvm::APSInt *Value = Ranges->getConcreteValue())
2231 return *Value == 0;
2232
2233 BasicValueFactory &BV = getBasicVals();
2234 APSIntType IntType = BV.getAPSIntType(Sym->getType());
2235 llvm::APSInt Zero = IntType.getZeroValue();
2236
2237 // Check if zero is in the set of possible values.
2238 if (!Ranges->contains(Zero))
2239 return false;
2240
2241 // Zero is a possible value, but it is not the /only/ possible value.
2242 return ConditionTruthVal();
2243 }
2244
getSymVal(ProgramStateRef St,SymbolRef Sym) const2245 const llvm::APSInt *RangeConstraintManager::getSymVal(ProgramStateRef St,
2246 SymbolRef Sym) const {
2247 const RangeSet *T = getConstraint(St, Sym);
2248 return T ? T->getConcreteValue() : nullptr;
2249 }
2250
2251 //===----------------------------------------------------------------------===//
2252 // Remove dead symbols from existing constraints
2253 //===----------------------------------------------------------------------===//
2254
2255 /// Scan all symbols referenced by the constraints. If the symbol is not alive
2256 /// as marked in LSymbols, mark it as dead in DSymbols.
2257 ProgramStateRef
removeDeadBindings(ProgramStateRef State,SymbolReaper & SymReaper)2258 RangeConstraintManager::removeDeadBindings(ProgramStateRef State,
2259 SymbolReaper &SymReaper) {
2260 ClassMembersTy ClassMembersMap = State->get<ClassMembers>();
2261 ClassMembersTy NewClassMembersMap = ClassMembersMap;
2262 ClassMembersTy::Factory &EMFactory = State->get_context<ClassMembers>();
2263 SymbolSet::Factory &SetFactory = State->get_context<SymbolSet>();
2264
2265 ConstraintRangeTy Constraints = State->get<ConstraintRange>();
2266 ConstraintRangeTy NewConstraints = Constraints;
2267 ConstraintRangeTy::Factory &ConstraintFactory =
2268 State->get_context<ConstraintRange>();
2269
2270 ClassMapTy Map = State->get<ClassMap>();
2271 ClassMapTy NewMap = Map;
2272 ClassMapTy::Factory &ClassFactory = State->get_context<ClassMap>();
2273
2274 DisequalityMapTy Disequalities = State->get<DisequalityMap>();
2275 DisequalityMapTy::Factory &DisequalityFactory =
2276 State->get_context<DisequalityMap>();
2277 ClassSet::Factory &ClassSetFactory = State->get_context<ClassSet>();
2278
2279 bool ClassMapChanged = false;
2280 bool MembersMapChanged = false;
2281 bool ConstraintMapChanged = false;
2282 bool DisequalitiesChanged = false;
2283
2284 auto removeDeadClass = [&](EquivalenceClass Class) {
2285 // Remove associated constraint ranges.
2286 Constraints = ConstraintFactory.remove(Constraints, Class);
2287 ConstraintMapChanged = true;
2288
2289 // Update disequality information to not hold any information on the
2290 // removed class.
2291 ClassSet DisequalClasses =
2292 Class.getDisequalClasses(Disequalities, ClassSetFactory);
2293 if (!DisequalClasses.isEmpty()) {
2294 for (EquivalenceClass DisequalClass : DisequalClasses) {
2295 ClassSet DisequalToDisequalSet =
2296 DisequalClass.getDisequalClasses(Disequalities, ClassSetFactory);
2297 // DisequalToDisequalSet is guaranteed to be non-empty for consistent
2298 // disequality info.
2299 assert(!DisequalToDisequalSet.isEmpty());
2300 ClassSet NewSet = ClassSetFactory.remove(DisequalToDisequalSet, Class);
2301
2302 // No need in keeping an empty set.
2303 if (NewSet.isEmpty()) {
2304 Disequalities =
2305 DisequalityFactory.remove(Disequalities, DisequalClass);
2306 } else {
2307 Disequalities =
2308 DisequalityFactory.add(Disequalities, DisequalClass, NewSet);
2309 }
2310 }
2311 // Remove the data for the class
2312 Disequalities = DisequalityFactory.remove(Disequalities, Class);
2313 DisequalitiesChanged = true;
2314 }
2315 };
2316
2317 // 1. Let's see if dead symbols are trivial and have associated constraints.
2318 for (std::pair<EquivalenceClass, RangeSet> ClassConstraintPair :
2319 Constraints) {
2320 EquivalenceClass Class = ClassConstraintPair.first;
2321 if (Class.isTriviallyDead(State, SymReaper)) {
2322 // If this class is trivial, we can remove its constraints right away.
2323 removeDeadClass(Class);
2324 }
2325 }
2326
2327 // 2. We don't need to track classes for dead symbols.
2328 for (std::pair<SymbolRef, EquivalenceClass> SymbolClassPair : Map) {
2329 SymbolRef Sym = SymbolClassPair.first;
2330
2331 if (SymReaper.isDead(Sym)) {
2332 ClassMapChanged = true;
2333 NewMap = ClassFactory.remove(NewMap, Sym);
2334 }
2335 }
2336
2337 // 3. Remove dead members from classes and remove dead non-trivial classes
2338 // and their constraints.
2339 for (std::pair<EquivalenceClass, SymbolSet> ClassMembersPair :
2340 ClassMembersMap) {
2341 EquivalenceClass Class = ClassMembersPair.first;
2342 SymbolSet LiveMembers = ClassMembersPair.second;
2343 bool MembersChanged = false;
2344
2345 for (SymbolRef Member : ClassMembersPair.second) {
2346 if (SymReaper.isDead(Member)) {
2347 MembersChanged = true;
2348 LiveMembers = SetFactory.remove(LiveMembers, Member);
2349 }
2350 }
2351
2352 // Check if the class changed.
2353 if (!MembersChanged)
2354 continue;
2355
2356 MembersMapChanged = true;
2357
2358 if (LiveMembers.isEmpty()) {
2359 // The class is dead now, we need to wipe it out of the members map...
2360 NewClassMembersMap = EMFactory.remove(NewClassMembersMap, Class);
2361
2362 // ...and remove all of its constraints.
2363 removeDeadClass(Class);
2364 } else {
2365 // We need to change the members associated with the class.
2366 NewClassMembersMap =
2367 EMFactory.add(NewClassMembersMap, Class, LiveMembers);
2368 }
2369 }
2370
2371 // 4. Update the state with new maps.
2372 //
2373 // Here we try to be humble and update a map only if it really changed.
2374 if (ClassMapChanged)
2375 State = State->set<ClassMap>(NewMap);
2376
2377 if (MembersMapChanged)
2378 State = State->set<ClassMembers>(NewClassMembersMap);
2379
2380 if (ConstraintMapChanged)
2381 State = State->set<ConstraintRange>(Constraints);
2382
2383 if (DisequalitiesChanged)
2384 State = State->set<DisequalityMap>(Disequalities);
2385
2386 assert(EquivalenceClass::isClassDataConsistent(State));
2387
2388 return State;
2389 }
2390
getRange(ProgramStateRef State,SymbolRef Sym)2391 RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
2392 SymbolRef Sym) {
2393 return SymbolicRangeInferrer::inferRange(F, State, Sym);
2394 }
2395
setRange(ProgramStateRef State,SymbolRef Sym,RangeSet Range)2396 ProgramStateRef RangeConstraintManager::setRange(ProgramStateRef State,
2397 SymbolRef Sym,
2398 RangeSet Range) {
2399 return ConstraintAssignor::assign(State, getSValBuilder(), F, Sym, Range);
2400 }
2401
2402 //===------------------------------------------------------------------------===
2403 // assumeSymX methods: protected interface for RangeConstraintManager.
2404 //===------------------------------------------------------------------------===/
2405
2406 // The syntax for ranges below is mathematical, using [x, y] for closed ranges
2407 // and (x, y) for open ranges. These ranges are modular, corresponding with
2408 // a common treatment of C integer overflow. This means that these methods
2409 // do not have to worry about overflow; RangeSet::Intersect can handle such a
2410 // "wraparound" range.
2411 // As an example, the range [UINT_MAX-1, 3) contains five values: UINT_MAX-1,
2412 // UINT_MAX, 0, 1, and 2.
2413
2414 ProgramStateRef
assumeSymNE(ProgramStateRef St,SymbolRef Sym,const llvm::APSInt & Int,const llvm::APSInt & Adjustment)2415 RangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym,
2416 const llvm::APSInt &Int,
2417 const llvm::APSInt &Adjustment) {
2418 // Before we do any real work, see if the value can even show up.
2419 APSIntType AdjustmentType(Adjustment);
2420 if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within)
2421 return St;
2422
2423 llvm::APSInt Point = AdjustmentType.convert(Int) - Adjustment;
2424 RangeSet New = getRange(St, Sym);
2425 New = F.deletePoint(New, Point);
2426
2427 return setRange(St, Sym, New);
2428 }
2429
2430 ProgramStateRef
assumeSymEQ(ProgramStateRef St,SymbolRef Sym,const llvm::APSInt & Int,const llvm::APSInt & Adjustment)2431 RangeConstraintManager::assumeSymEQ(ProgramStateRef St, SymbolRef Sym,
2432 const llvm::APSInt &Int,
2433 const llvm::APSInt &Adjustment) {
2434 // Before we do any real work, see if the value can even show up.
2435 APSIntType AdjustmentType(Adjustment);
2436 if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within)
2437 return nullptr;
2438
2439 // [Int-Adjustment, Int-Adjustment]
2440 llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment;
2441 RangeSet New = getRange(St, Sym);
2442 New = F.intersect(New, AdjInt);
2443
2444 return setRange(St, Sym, New);
2445 }
2446
getSymLTRange(ProgramStateRef St,SymbolRef Sym,const llvm::APSInt & Int,const llvm::APSInt & Adjustment)2447 RangeSet RangeConstraintManager::getSymLTRange(ProgramStateRef St,
2448 SymbolRef Sym,
2449 const llvm::APSInt &Int,
2450 const llvm::APSInt &Adjustment) {
2451 // Before we do any real work, see if the value can even show up.
2452 APSIntType AdjustmentType(Adjustment);
2453 switch (AdjustmentType.testInRange(Int, true)) {
2454 case APSIntType::RTR_Below:
2455 return F.getEmptySet();
2456 case APSIntType::RTR_Within:
2457 break;
2458 case APSIntType::RTR_Above:
2459 return getRange(St, Sym);
2460 }
2461
2462 // Special case for Int == Min. This is always false.
2463 llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
2464 llvm::APSInt Min = AdjustmentType.getMinValue();
2465 if (ComparisonVal == Min)
2466 return F.getEmptySet();
2467
2468 llvm::APSInt Lower = Min - Adjustment;
2469 llvm::APSInt Upper = ComparisonVal - Adjustment;
2470 --Upper;
2471
2472 RangeSet Result = getRange(St, Sym);
2473 return F.intersect(Result, Lower, Upper);
2474 }
2475
2476 ProgramStateRef
assumeSymLT(ProgramStateRef St,SymbolRef Sym,const llvm::APSInt & Int,const llvm::APSInt & Adjustment)2477 RangeConstraintManager::assumeSymLT(ProgramStateRef St, SymbolRef Sym,
2478 const llvm::APSInt &Int,
2479 const llvm::APSInt &Adjustment) {
2480 RangeSet New = getSymLTRange(St, Sym, Int, Adjustment);
2481 return setRange(St, Sym, New);
2482 }
2483
getSymGTRange(ProgramStateRef St,SymbolRef Sym,const llvm::APSInt & Int,const llvm::APSInt & Adjustment)2484 RangeSet RangeConstraintManager::getSymGTRange(ProgramStateRef St,
2485 SymbolRef Sym,
2486 const llvm::APSInt &Int,
2487 const llvm::APSInt &Adjustment) {
2488 // Before we do any real work, see if the value can even show up.
2489 APSIntType AdjustmentType(Adjustment);
2490 switch (AdjustmentType.testInRange(Int, true)) {
2491 case APSIntType::RTR_Below:
2492 return getRange(St, Sym);
2493 case APSIntType::RTR_Within:
2494 break;
2495 case APSIntType::RTR_Above:
2496 return F.getEmptySet();
2497 }
2498
2499 // Special case for Int == Max. This is always false.
2500 llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
2501 llvm::APSInt Max = AdjustmentType.getMaxValue();
2502 if (ComparisonVal == Max)
2503 return F.getEmptySet();
2504
2505 llvm::APSInt Lower = ComparisonVal - Adjustment;
2506 llvm::APSInt Upper = Max - Adjustment;
2507 ++Lower;
2508
2509 RangeSet SymRange = getRange(St, Sym);
2510 return F.intersect(SymRange, Lower, Upper);
2511 }
2512
2513 ProgramStateRef
assumeSymGT(ProgramStateRef St,SymbolRef Sym,const llvm::APSInt & Int,const llvm::APSInt & Adjustment)2514 RangeConstraintManager::assumeSymGT(ProgramStateRef St, SymbolRef Sym,
2515 const llvm::APSInt &Int,
2516 const llvm::APSInt &Adjustment) {
2517 RangeSet New = getSymGTRange(St, Sym, Int, Adjustment);
2518 return setRange(St, Sym, New);
2519 }
2520
getSymGERange(ProgramStateRef St,SymbolRef Sym,const llvm::APSInt & Int,const llvm::APSInt & Adjustment)2521 RangeSet RangeConstraintManager::getSymGERange(ProgramStateRef St,
2522 SymbolRef Sym,
2523 const llvm::APSInt &Int,
2524 const llvm::APSInt &Adjustment) {
2525 // Before we do any real work, see if the value can even show up.
2526 APSIntType AdjustmentType(Adjustment);
2527 switch (AdjustmentType.testInRange(Int, true)) {
2528 case APSIntType::RTR_Below:
2529 return getRange(St, Sym);
2530 case APSIntType::RTR_Within:
2531 break;
2532 case APSIntType::RTR_Above:
2533 return F.getEmptySet();
2534 }
2535
2536 // Special case for Int == Min. This is always feasible.
2537 llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
2538 llvm::APSInt Min = AdjustmentType.getMinValue();
2539 if (ComparisonVal == Min)
2540 return getRange(St, Sym);
2541
2542 llvm::APSInt Max = AdjustmentType.getMaxValue();
2543 llvm::APSInt Lower = ComparisonVal - Adjustment;
2544 llvm::APSInt Upper = Max - Adjustment;
2545
2546 RangeSet SymRange = getRange(St, Sym);
2547 return F.intersect(SymRange, Lower, Upper);
2548 }
2549
2550 ProgramStateRef
assumeSymGE(ProgramStateRef St,SymbolRef Sym,const llvm::APSInt & Int,const llvm::APSInt & Adjustment)2551 RangeConstraintManager::assumeSymGE(ProgramStateRef St, SymbolRef Sym,
2552 const llvm::APSInt &Int,
2553 const llvm::APSInt &Adjustment) {
2554 RangeSet New = getSymGERange(St, Sym, Int, Adjustment);
2555 return setRange(St, Sym, New);
2556 }
2557
2558 RangeSet
getSymLERange(llvm::function_ref<RangeSet ()> RS,const llvm::APSInt & Int,const llvm::APSInt & Adjustment)2559 RangeConstraintManager::getSymLERange(llvm::function_ref<RangeSet()> RS,
2560 const llvm::APSInt &Int,
2561 const llvm::APSInt &Adjustment) {
2562 // Before we do any real work, see if the value can even show up.
2563 APSIntType AdjustmentType(Adjustment);
2564 switch (AdjustmentType.testInRange(Int, true)) {
2565 case APSIntType::RTR_Below:
2566 return F.getEmptySet();
2567 case APSIntType::RTR_Within:
2568 break;
2569 case APSIntType::RTR_Above:
2570 return RS();
2571 }
2572
2573 // Special case for Int == Max. This is always feasible.
2574 llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
2575 llvm::APSInt Max = AdjustmentType.getMaxValue();
2576 if (ComparisonVal == Max)
2577 return RS();
2578
2579 llvm::APSInt Min = AdjustmentType.getMinValue();
2580 llvm::APSInt Lower = Min - Adjustment;
2581 llvm::APSInt Upper = ComparisonVal - Adjustment;
2582
2583 RangeSet Default = RS();
2584 return F.intersect(Default, Lower, Upper);
2585 }
2586
getSymLERange(ProgramStateRef St,SymbolRef Sym,const llvm::APSInt & Int,const llvm::APSInt & Adjustment)2587 RangeSet RangeConstraintManager::getSymLERange(ProgramStateRef St,
2588 SymbolRef Sym,
2589 const llvm::APSInt &Int,
2590 const llvm::APSInt &Adjustment) {
2591 return getSymLERange([&] { return getRange(St, Sym); }, Int, Adjustment);
2592 }
2593
2594 ProgramStateRef
assumeSymLE(ProgramStateRef St,SymbolRef Sym,const llvm::APSInt & Int,const llvm::APSInt & Adjustment)2595 RangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym,
2596 const llvm::APSInt &Int,
2597 const llvm::APSInt &Adjustment) {
2598 RangeSet New = getSymLERange(St, Sym, Int, Adjustment);
2599 return setRange(St, Sym, New);
2600 }
2601
assumeSymWithinInclusiveRange(ProgramStateRef State,SymbolRef Sym,const llvm::APSInt & From,const llvm::APSInt & To,const llvm::APSInt & Adjustment)2602 ProgramStateRef RangeConstraintManager::assumeSymWithinInclusiveRange(
2603 ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
2604 const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
2605 RangeSet New = getSymGERange(State, Sym, From, Adjustment);
2606 if (New.isEmpty())
2607 return nullptr;
2608 RangeSet Out = getSymLERange([&] { return New; }, To, Adjustment);
2609 return setRange(State, Sym, Out);
2610 }
2611
assumeSymOutsideInclusiveRange(ProgramStateRef State,SymbolRef Sym,const llvm::APSInt & From,const llvm::APSInt & To,const llvm::APSInt & Adjustment)2612 ProgramStateRef RangeConstraintManager::assumeSymOutsideInclusiveRange(
2613 ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
2614 const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
2615 RangeSet RangeLT = getSymLTRange(State, Sym, From, Adjustment);
2616 RangeSet RangeGT = getSymGTRange(State, Sym, To, Adjustment);
2617 RangeSet New(F.add(RangeLT, RangeGT));
2618 return setRange(State, Sym, New);
2619 }
2620
2621 //===----------------------------------------------------------------------===//
2622 // Pretty-printing.
2623 //===----------------------------------------------------------------------===//
2624
printJson(raw_ostream & Out,ProgramStateRef State,const char * NL,unsigned int Space,bool IsDot) const2625 void RangeConstraintManager::printJson(raw_ostream &Out, ProgramStateRef State,
2626 const char *NL, unsigned int Space,
2627 bool IsDot) const {
2628 printConstraints(Out, State, NL, Space, IsDot);
2629 printEquivalenceClasses(Out, State, NL, Space, IsDot);
2630 printDisequalities(Out, State, NL, Space, IsDot);
2631 }
2632
toString(const SymbolRef & Sym)2633 static std::string toString(const SymbolRef &Sym) {
2634 std::string S;
2635 llvm::raw_string_ostream O(S);
2636 Sym->dumpToStream(O);
2637 return O.str();
2638 }
2639
printConstraints(raw_ostream & Out,ProgramStateRef State,const char * NL,unsigned int Space,bool IsDot) const2640 void RangeConstraintManager::printConstraints(raw_ostream &Out,
2641 ProgramStateRef State,
2642 const char *NL,
2643 unsigned int Space,
2644 bool IsDot) const {
2645 ConstraintRangeTy Constraints = State->get<ConstraintRange>();
2646
2647 Indent(Out, Space, IsDot) << "\"constraints\": ";
2648 if (Constraints.isEmpty()) {
2649 Out << "null," << NL;
2650 return;
2651 }
2652
2653 std::map<std::string, RangeSet> OrderedConstraints;
2654 for (std::pair<EquivalenceClass, RangeSet> P : Constraints) {
2655 SymbolSet ClassMembers = P.first.getClassMembers(State);
2656 for (const SymbolRef &ClassMember : ClassMembers) {
2657 bool insertion_took_place;
2658 std::tie(std::ignore, insertion_took_place) =
2659 OrderedConstraints.insert({toString(ClassMember), P.second});
2660 assert(insertion_took_place &&
2661 "two symbols should not have the same dump");
2662 }
2663 }
2664
2665 ++Space;
2666 Out << '[' << NL;
2667 bool First = true;
2668 for (std::pair<std::string, RangeSet> P : OrderedConstraints) {
2669 if (First) {
2670 First = false;
2671 } else {
2672 Out << ',';
2673 Out << NL;
2674 }
2675 Indent(Out, Space, IsDot)
2676 << "{ \"symbol\": \"" << P.first << "\", \"range\": \"";
2677 P.second.dump(Out);
2678 Out << "\" }";
2679 }
2680 Out << NL;
2681
2682 --Space;
2683 Indent(Out, Space, IsDot) << "]," << NL;
2684 }
2685
toString(ProgramStateRef State,EquivalenceClass Class)2686 static std::string toString(ProgramStateRef State, EquivalenceClass Class) {
2687 SymbolSet ClassMembers = Class.getClassMembers(State);
2688 llvm::SmallVector<SymbolRef, 8> ClassMembersSorted(ClassMembers.begin(),
2689 ClassMembers.end());
2690 llvm::sort(ClassMembersSorted,
2691 [](const SymbolRef &LHS, const SymbolRef &RHS) {
2692 return toString(LHS) < toString(RHS);
2693 });
2694
2695 bool FirstMember = true;
2696
2697 std::string Str;
2698 llvm::raw_string_ostream Out(Str);
2699 Out << "[ ";
2700 for (SymbolRef ClassMember : ClassMembersSorted) {
2701 if (FirstMember)
2702 FirstMember = false;
2703 else
2704 Out << ", ";
2705 Out << "\"" << ClassMember << "\"";
2706 }
2707 Out << " ]";
2708 return Out.str();
2709 }
2710
printEquivalenceClasses(raw_ostream & Out,ProgramStateRef State,const char * NL,unsigned int Space,bool IsDot) const2711 void RangeConstraintManager::printEquivalenceClasses(raw_ostream &Out,
2712 ProgramStateRef State,
2713 const char *NL,
2714 unsigned int Space,
2715 bool IsDot) const {
2716 ClassMembersTy Members = State->get<ClassMembers>();
2717
2718 Indent(Out, Space, IsDot) << "\"equivalence_classes\": ";
2719 if (Members.isEmpty()) {
2720 Out << "null," << NL;
2721 return;
2722 }
2723
2724 std::set<std::string> MembersStr;
2725 for (std::pair<EquivalenceClass, SymbolSet> ClassToSymbolSet : Members)
2726 MembersStr.insert(toString(State, ClassToSymbolSet.first));
2727
2728 ++Space;
2729 Out << '[' << NL;
2730 bool FirstClass = true;
2731 for (const std::string &Str : MembersStr) {
2732 if (FirstClass) {
2733 FirstClass = false;
2734 } else {
2735 Out << ',';
2736 Out << NL;
2737 }
2738 Indent(Out, Space, IsDot);
2739 Out << Str;
2740 }
2741 Out << NL;
2742
2743 --Space;
2744 Indent(Out, Space, IsDot) << "]," << NL;
2745 }
2746
printDisequalities(raw_ostream & Out,ProgramStateRef State,const char * NL,unsigned int Space,bool IsDot) const2747 void RangeConstraintManager::printDisequalities(raw_ostream &Out,
2748 ProgramStateRef State,
2749 const char *NL,
2750 unsigned int Space,
2751 bool IsDot) const {
2752 DisequalityMapTy Disequalities = State->get<DisequalityMap>();
2753
2754 Indent(Out, Space, IsDot) << "\"disequality_info\": ";
2755 if (Disequalities.isEmpty()) {
2756 Out << "null," << NL;
2757 return;
2758 }
2759
2760 // Transform the disequality info to an ordered map of
2761 // [string -> (ordered set of strings)]
2762 using EqClassesStrTy = std::set<std::string>;
2763 using DisequalityInfoStrTy = std::map<std::string, EqClassesStrTy>;
2764 DisequalityInfoStrTy DisequalityInfoStr;
2765 for (std::pair<EquivalenceClass, ClassSet> ClassToDisEqSet : Disequalities) {
2766 EquivalenceClass Class = ClassToDisEqSet.first;
2767 ClassSet DisequalClasses = ClassToDisEqSet.second;
2768 EqClassesStrTy MembersStr;
2769 for (EquivalenceClass DisEqClass : DisequalClasses)
2770 MembersStr.insert(toString(State, DisEqClass));
2771 DisequalityInfoStr.insert({toString(State, Class), MembersStr});
2772 }
2773
2774 ++Space;
2775 Out << '[' << NL;
2776 bool FirstClass = true;
2777 for (std::pair<std::string, EqClassesStrTy> ClassToDisEqSet :
2778 DisequalityInfoStr) {
2779 const std::string &Class = ClassToDisEqSet.first;
2780 if (FirstClass) {
2781 FirstClass = false;
2782 } else {
2783 Out << ',';
2784 Out << NL;
2785 }
2786 Indent(Out, Space, IsDot) << "{" << NL;
2787 unsigned int DisEqSpace = Space + 1;
2788 Indent(Out, DisEqSpace, IsDot) << "\"class\": ";
2789 Out << Class;
2790 const EqClassesStrTy &DisequalClasses = ClassToDisEqSet.second;
2791 if (!DisequalClasses.empty()) {
2792 Out << "," << NL;
2793 Indent(Out, DisEqSpace, IsDot) << "\"disequal_to\": [" << NL;
2794 unsigned int DisEqClassSpace = DisEqSpace + 1;
2795 Indent(Out, DisEqClassSpace, IsDot);
2796 bool FirstDisEqClass = true;
2797 for (const std::string &DisEqClass : DisequalClasses) {
2798 if (FirstDisEqClass) {
2799 FirstDisEqClass = false;
2800 } else {
2801 Out << ',' << NL;
2802 Indent(Out, DisEqClassSpace, IsDot);
2803 }
2804 Out << DisEqClass;
2805 }
2806 Out << "]" << NL;
2807 }
2808 Indent(Out, Space, IsDot) << "}";
2809 }
2810 Out << NL;
2811
2812 --Space;
2813 Indent(Out, Space, IsDot) << "]," << NL;
2814 }
2815