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