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
31	using namespace clang;
32	using namespace ento;
33
34	// This class can be extended with other tables which will help to reason
35	// about ranges more precisely.
36	class 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
41	public:
42	enum TriStateKind {
43	False = 0,
44	True,
45	Unknown,
46	};
47
48	private:
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
91	public:
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
112	RangeSet::ContainerType RangeSet::Factory::EmptySet{};
113
114	RangeSet 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
122	RangeSet 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
134	RangeSet RangeSet::Factory::add(RangeSet Original, const llvm::APSInt &Point) {
135	return add(Original, Element: Range(Point));
136	}
137
138	RangeSet 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
143	RangeSet 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
150	RangeSet RangeSet::Factory::unite(RangeSet Original, llvm::APSInt Point) {
151	return unite(Original, R: Range(ValueFactory.getValue(X: Point)));
152	}
153
154	RangeSet 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
160	template <typename T>
161	static void swapIterators(T &First, T &FirstEnd, T &Second, T &SecondEnd) {
162	std::swap(First, Second);
163	std::swap(FirstEnd, SecondEnd);
164	}
165
166	RangeSet::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
318	RangeSet RangeSet::Factory::getRangeSet(Range From) {
319	ContainerType Result;
320	Result.push_back(Elt: From);
321	return makePersistent(From: std::move(Result));
322	}
323
324	RangeSet 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
342	RangeSet::ContainerType *RangeSet::Factory::construct(ContainerType &&From) {
343	void *Buffer = Arena.Allocate();
344	return new (Buffer) ContainerType(std::move(From));
345	}
346
347	const llvm::APSInt &RangeSet::getMinValue() const {
348	assert(!isEmpty());
349	return begin()->From();
350	}
351
352	const llvm::APSInt &RangeSet::getMaxValue() const {
353	assert(!isEmpty());
354	return std::prev(x: end())->To();
355	}
356
357	bool clang::ento::RangeSet::isUnsigned() const {
358	assert(!isEmpty());
359	return begin()->From().isUnsigned();
360	}
361
362	uint32_t clang::ento::RangeSet::getBitWidth() const {
363	assert(!isEmpty());
364	return begin()->From().getBitWidth();
365	}
366
367	APSIntType clang::ento::RangeSet::getAPSIntType() const {
368	assert(!isEmpty());
369	return APSIntType(begin()->From());
370	}
371
372	bool 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
384	bool 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
393	bool 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
474	RangeSet 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
517	RangeSet 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
595	RangeSet 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
604	RangeSet 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
611	RangeSet 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.
676	RangeSet 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
707	RangeSet 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
712	RangeSet::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)
778	RangeSet::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.
827	RangeSet::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
849	RangeSet 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
864	LLVM_DUMP_METHOD void Range::dump(raw_ostream &OS) const {
865	OS << '[' << toString(I: From(), Radix: 10) << ", " << toString(I: To(), Radix: 10) << ']';
866	}
867	LLVM_DUMP_METHOD void Range::dump() const { dump(OS&: llvm::errs()); }
868
869	LLVM_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	}
874	LLVM_DUMP_METHOD void RangeSet::dump() const { dump(OS&: llvm::errs()); }
875
876	REGISTER_SET_FACTORY_WITH_PROGRAMSTATE(SymbolSet, SymbolRef)
877
878	namespace {
879	class EquivalenceClass;
880	} // end anonymous namespace
881
882	REGISTER_MAP_WITH_PROGRAMSTATE(ClassMap, SymbolRef, EquivalenceClass)
883	REGISTER_MAP_WITH_PROGRAMSTATE(ClassMembers, EquivalenceClass, SymbolSet)
884	REGISTER_MAP_WITH_PROGRAMSTATE(ConstraintRange, EquivalenceClass, RangeSet)
885
886	REGISTER_SET_FACTORY_WITH_PROGRAMSTATE(ClassSet, EquivalenceClass)
887	REGISTER_MAP_WITH_PROGRAMSTATE(DisequalityMap, EquivalenceClass, ClassSet)
888
889	namespace {
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.
914	class EquivalenceClass : public llvm::FoldingSetNode {
915	public:
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
1013	private:
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
1045	areFeasible(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
1087	std::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
1107	template <class SecondTy, class... RestTy>
1108	[[nodiscard]] inline RangeSet intersect(RangeSet::Factory &F, RangeSet Head,
1109	SecondTy Second, RestTy... Tail);
1110
1111	template <class... RangeTy> struct IntersectionTraits;
1112
1113	template <class... TailTy> struct IntersectionTraits<RangeSet, TailTy...> {
1114	// Found RangeSet, no need to check any further
1115	using Type = RangeSet;
1116	};
1117
1118	template <> 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
1124	template <class OptionalOrPointer, class... TailTy>
1125	struct 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
1130	template <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>
1138	intersect(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
1147	template <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
1155	template <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>.
1188	template <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.
1208	class SymbolicRangeInferrer
1209	: public SymExprVisitor<SymbolicRangeInferrer, RangeSet> {
1210	public:
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
1265	private:
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	[SSE, State = this->State]() -> SymbolRef {
1473	if (SSE->getOpcode() == BO_Sub)
1474	return State->getSymbolManager().acquire<SymSymExpr>(
1475	SSE->getRHS(), BO_Sub, SSE->getLHS(), SSE->getType());
1476	return nullptr;
1477	},
1478	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	{BO_EQ, BO_NE, BO_Or, BO_And, BO_Add, BO_Mul, BO_Xor}, Op);
1495	if (!IsCommutative)
1496	return std::nullopt;
1497
1498	SymbolRef Commuted = State->getSymbolManager().acquire<SymSymExpr>(
1499	SSE->getRHS(), Op, SSE->getLHS(), 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, 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, 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
1634	template <>
1635	RangeSet 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
1685	template <>
1686	RangeSet 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
1742	template <>
1743	RangeSet 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
1788	template <>
1789	RangeSet 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
1845	RangeSet 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
1872	class RangeConstraintManager : public RangedConstraintManager {
1873	public:
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
1956	private:
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)
1998	template <class Derived> class ConstraintAssignorBase {
1999	public:
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.
2078	class ConstraintAssignor : public ConstraintAssignorBase<ConstraintAssignor> {
2079	public:
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
2116	private:
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
2201	bool 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
2242	bool 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
2274	std::unique_ptr<ConstraintManager>
2275	ento::CreateRangeConstraintManager(ProgramStateManager &StMgr,
2276	ExprEngine *Eng) {
2277	return std::make_unique<RangeConstraintManager>(args&: Eng, args&: StMgr.getSValBuilder());
2278	}
2279
2280	ConstraintMap 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
2302	LLVM_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
2311	inline 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
2323	inline 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
2333	inline 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
2368	inline ProgramStateRef
2369	EquivalenceClass::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
2481	inline SymbolSet::Factory &
2482	EquivalenceClass::getMembersFactory(ProgramStateRef State) {
2483	return State->get_context<SymbolSet>();
2484	}
2485
2486	SymbolSet 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
2496	bool EquivalenceClass::isTrivial(ProgramStateRef State) const {
2497	return State->get<ClassMembers>(key: *this) == nullptr;
2498	}
2499
2500	bool EquivalenceClass::isTriviallyDead(ProgramStateRef State,
2501	SymbolReaper &Reaper) const {
2502	return isTrivial(State) && Reaper.isDead(sym: getRepresentativeSymbol());
2503	}
2504
2505	inline 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
2512	inline 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
2519	inline ProgramStateRef
2520	EquivalenceClass::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
2548	inline 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
2589	inline 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
2596	inline 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
2614	EquivalenceClass::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
2643	reAssume(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
2673	EquivalenceClass::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
2749	inline ClassSet EquivalenceClass::getDisequalClasses(ProgramStateRef State,
2750	SymbolRef Sym) {
2751	return find(State, Sym).getDisequalClasses(State);
2752	}
2753
2754	inline ClassSet
2755	EquivalenceClass::getDisequalClasses(ProgramStateRef State) const {
2756	return getDisequalClasses(Map: State->get<DisequalityMap>(),
2757	Factory&: State->get_context<ClassSet>());
2758	}
2759
2760	inline ClassSet
2761	EquivalenceClass::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
2769	bool 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
2812	bool 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(SSE->getOpcode()) ||
2841	BinaryOperator::isRelationalOp(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
2858	ConditionTruthVal 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
2882	const llvm::APSInt *RangeConstraintManager::getSymVal(ProgramStateRef St,
2883	SymbolRef Sym) const {
2884	return getRange(State: St, Sym).getConcreteValue();
2885	}
2886
2887	const 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
2893	const 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.
2905	ProgramStateRef
2906	RangeConstraintManager::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
3039	RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
3040	SymbolRef Sym) const {
3041	return SymbolicRangeInferrer::inferRange(F, State, Origin: Sym);
3042	}
3043
3044	ProgramStateRef 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
3062	ProgramStateRef
3063	RangeConstraintManager::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
3078	ProgramStateRef
3079	RangeConstraintManager::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
3095	RangeSet
3096	RangeConstraintManager::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
3124	ProgramStateRef
3125	RangeConstraintManager::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
3132	RangeSet
3133	RangeConstraintManager::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
3161	ProgramStateRef
3162	RangeConstraintManager::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
3169	RangeSet
3170	RangeConstraintManager::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
3198	ProgramStateRef
3199	RangeConstraintManager::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
3206	RangeSet
3207	RangeConstraintManager::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
3235	RangeSet
3236	RangeConstraintManager::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
3242	ProgramStateRef
3243	RangeConstraintManager::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
3250	ProgramStateRef 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
3260	ProgramStateRef 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
3273	void 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
3281	void 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
3292	static 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
3299	void 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
3345	static 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
3370	void 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
3406	void 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