1	/* Tracking equivalence classes and constraints at a point on an execution path.
2	Copyright (C) 2019-2024 Free Software Foundation, Inc.
3	Contributed by David Malcolm <dmalcolm@redhat.com>.
4
5	This file is part of GCC.
6
7	GCC is free software; you can redistribute it and/or modify it
8	under the terms of the GNU General Public License as published by
9	the Free Software Foundation; either version 3, or (at your option)
10	any later version.
11
12	GCC is distributed in the hope that it will be useful, but
13	WITHOUT ANY WARRANTY; without even the implied warranty of
14	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
15	General Public License for more details.
16
17	You should have received a copy of the GNU General Public License
18	along with GCC; see the file COPYING3. If not see
19	<http://www.gnu.org/licenses/>. */
20
21	#include "config.h"
22	#define INCLUDE_MEMORY
23	#include "system.h"
24	#include "coretypes.h"
25	#include "tree.h"
26	#include "function.h"
27	#include "basic-block.h"
28	#include "gimple.h"
29	#include "gimple-iterator.h"
30	#include "fold-const.h"
31	#include "selftest.h"
32	#include "diagnostic-core.h"
33	#include "graphviz.h"
34	#include "analyzer/analyzer.h"
35	#include "ordered-hash-map.h"
36	#include "options.h"
37	#include "cgraph.h"
38	#include "cfg.h"
39	#include "digraph.h"
40	#include "analyzer/supergraph.h"
41	#include "sbitmap.h"
42	#include "bitmap.h"
43	#include "analyzer/analyzer-logging.h"
44	#include "analyzer/call-string.h"
45	#include "analyzer/program-point.h"
46	#include "analyzer/store.h"
47	#include "analyzer/region-model.h"
48	#include "analyzer/constraint-manager.h"
49	#include "analyzer/call-summary.h"
50	#include "analyzer/analyzer-selftests.h"
51	#include "tree-pretty-print.h"
52
53	#if ENABLE_ANALYZER
54
55	namespace ana {
56
57	tristate
58	compare_constants (tree lhs_const, enum tree_code op, tree rhs_const)
59	{
60	tree comparison
61	= fold_binary (op, boolean_type_node, lhs_const, rhs_const);
62	if (comparison == boolean_true_node)
63	return tristate (tristate::TS_TRUE);
64	if (comparison == boolean_false_node)
65	return tristate (tristate::TS_FALSE);
66	return tristate (tristate::TS_UNKNOWN);
67	}
68
69	/* Return true iff CST is below the maximum value for its type. */
70
71	static bool
72	can_plus_one_p (tree cst)
73	{
74	gcc_assert (CONSTANT_CLASS_P (cst));
75	return tree_int_cst_lt (t1: cst, TYPE_MAX_VALUE (TREE_TYPE (cst)));
76	}
77
78	/* Return (CST + 1). */
79
80	static tree
81	plus_one (tree cst)
82	{
83	gcc_assert (CONSTANT_CLASS_P (cst));
84	gcc_assert (can_plus_one_p (cst));
85	tree result = fold_build2 (PLUS_EXPR, TREE_TYPE (cst),
86	cst, integer_one_node);
87	gcc_assert (CONSTANT_CLASS_P (result));
88	return result;
89	}
90
91	/* Return true iff CST is above the minimum value for its type. */
92
93	static bool
94	can_minus_one_p (tree cst)
95	{
96	gcc_assert (CONSTANT_CLASS_P (cst));
97	return tree_int_cst_lt (TYPE_MIN_VALUE (TREE_TYPE (cst)), t2: cst);
98	}
99
100	/* Return (CST - 1). */
101
102	static tree
103	minus_one (tree cst)
104	{
105	gcc_assert (CONSTANT_CLASS_P (cst));
106	gcc_assert (can_minus_one_p (cst));
107	tree result = fold_build2 (MINUS_EXPR, TREE_TYPE (cst),
108	cst, integer_one_node);
109	gcc_assert (CONSTANT_CLASS_P (result));
110	return result;
111	}
112
113	/* struct bound. */
114
115	/* Ensure that this bound is closed by converting an open bound to a
116	closed one. */
117
118	void
119	bound::ensure_closed (enum bound_kind bound_kind)
120	{
121	if (!m_closed)
122	{
123	/* Offset by 1 in the appropriate direction.
124	For example, convert 3 < x into 4 <= x,
125	and convert x < 5 into x <= 4. */
126	gcc_assert (CONSTANT_CLASS_P (m_constant));
127	gcc_assert (INTEGRAL_TYPE_P (TREE_TYPE (m_constant)));
128	m_constant = fold_build2 (bound_kind == BK_UPPER ? MINUS_EXPR : PLUS_EXPR,
129	TREE_TYPE (m_constant),
130	m_constant, integer_one_node);
131	gcc_assert (CONSTANT_CLASS_P (m_constant));
132	gcc_assert (INTEGRAL_TYPE_P (TREE_TYPE (m_constant)));
133	m_closed = true;
134	}
135	}
136
137	/* Get "<=" vs "<" for this bound. */
138
139	const char *
140	bound::get_relation_as_str () const
141	{
142	if (m_closed)
143	return "<=";
144	else
145	return "<";
146	}
147
148	/* struct range. */
149
150	/* Dump this range to PP, which must support %E for tree. */
151
152	void
153	range::dump_to_pp (pretty_printer *pp) const
154	{
155	if (m_lower_bound.m_constant)
156	{
157	if (m_upper_bound.m_constant)
158	pp_printf (pp, "%qE %s x %s %qE",
159	m_lower_bound.m_constant,
160	m_lower_bound.get_relation_as_str (),
161	m_upper_bound.get_relation_as_str (),
162	m_upper_bound.m_constant);
163	else
164	pp_printf (pp, "%qE %s x",
165	m_lower_bound.m_constant,
166	m_lower_bound.get_relation_as_str ());
167	}
168	else
169	{
170	if (m_upper_bound.m_constant)
171	pp_printf (pp, "x %s %qE",
172	m_upper_bound.get_relation_as_str (),
173	m_upper_bound.m_constant);
174	else
175	pp_string (pp, "x");
176	}
177	}
178
179	/* Dump this range to stderr. */
180
181	DEBUG_FUNCTION void
182	range::dump () const
183	{
184	pretty_printer pp;
185	pp_format_decoder (&pp) = default_tree_printer;
186	pp_show_color (&pp) = pp_show_color (global_dc->printer);
187	pp.buffer->stream = stderr;
188	dump_to_pp (pp: &pp);
189	pp_newline (&pp);
190	pp_flush (&pp);
191	}
192
193	/* Determine if there is only one possible value for this range.
194	If so, return the constant; otherwise, return NULL_TREE. */
195
196	tree
197	range::constrained_to_single_element ()
198	{
199	if (m_lower_bound.m_constant == NULL_TREE
200	|| m_upper_bound.m_constant == NULL_TREE)
201	return NULL_TREE;
202
203	if (!INTEGRAL_TYPE_P (TREE_TYPE (m_lower_bound.m_constant)))
204	return NULL_TREE;
205	if (!INTEGRAL_TYPE_P (TREE_TYPE (m_upper_bound.m_constant)))
206	return NULL_TREE;
207
208	/* Convert any open bounds to closed bounds. */
209	m_lower_bound.ensure_closed (bound_kind: BK_LOWER);
210	m_upper_bound.ensure_closed (bound_kind: BK_UPPER);
211
212	// Are they equal?
213	tree comparison = fold_binary (EQ_EXPR, boolean_type_node,
214	m_lower_bound.m_constant,
215	m_upper_bound.m_constant);
216	if (comparison == boolean_true_node)
217	return m_lower_bound.m_constant;
218	else
219	return NULL_TREE;
220	}
221
222	/* Eval the condition "X OP RHS_CONST" for X within the range. */
223
224	tristate
225	range::eval_condition (enum tree_code op, tree rhs_const) const
226	{
227	range copy (*this);
228	if (tree single_element = copy.constrained_to_single_element ())
229	return compare_constants (lhs_const: single_element, op, rhs_const);
230
231	switch (op)
232	{
233	case EQ_EXPR:
234	if (below_lower_bound (rhs_const))
235	return tristate (tristate::TS_FALSE);
236	if (above_upper_bound (rhs_const))
237	return tristate (tristate::TS_FALSE);
238	break;
239
240	case LT_EXPR:
241	case LE_EXPR:
242	/* Qn: "X </<= RHS_CONST". */
243	/* If RHS_CONST > upper bound, then it's true.
244	If RHS_CONST < lower bound, then it's false.
245	Otherwise unknown. */
246	if (above_upper_bound (rhs_const))
247	return tristate (tristate::TS_TRUE);
248	if (below_lower_bound (rhs_const))
249	return tristate (tristate::TS_FALSE);
250	break;
251
252	case NE_EXPR:
253	/* Qn: "X != RHS_CONST". */
254	/* If RHS_CONST < lower bound, then it's true.
255	If RHS_CONST > upper bound, then it's false.
256	Otherwise unknown. */
257	if (below_lower_bound (rhs_const))
258	return tristate (tristate::TS_TRUE);
259	if (above_upper_bound (rhs_const))
260	return tristate (tristate::TS_TRUE);
261	break;
262
263	case GE_EXPR:
264	case GT_EXPR:
265	/* Qn: "X >=/> RHS_CONST". */
266	if (above_upper_bound (rhs_const))
267	return tristate (tristate::TS_FALSE);
268	if (below_lower_bound (rhs_const))
269	return tristate (tristate::TS_TRUE);
270	break;
271
272	default:
273	gcc_unreachable ();
274	break;
275	}
276	return tristate (tristate::TS_UNKNOWN);
277	}
278
279	/* Return true if RHS_CONST is below the lower bound of this range. */
280
281	bool
282	range::below_lower_bound (tree rhs_const) const
283	{
284	if (!m_lower_bound.m_constant)
285	return false;
286
287	return compare_constants (lhs_const: rhs_const,
288	op: m_lower_bound.m_closed ? LT_EXPR : LE_EXPR,
289	rhs_const: m_lower_bound.m_constant).is_true ();
290	}
291
292	/* Return true if RHS_CONST is above the upper bound of this range. */
293
294	bool
295	range::above_upper_bound (tree rhs_const) const
296	{
297	if (!m_upper_bound.m_constant)
298	return false;
299
300	return compare_constants (lhs_const: rhs_const,
301	op: m_upper_bound.m_closed ? GT_EXPR : GE_EXPR,
302	rhs_const: m_upper_bound.m_constant).is_true ();
303	}
304
305	/* Attempt to add B to the bound of the given kind of this range.
306	Return true if feasible; false if infeasible. */
307
308	bool
309	range::add_bound (bound b, enum bound_kind bound_kind)
310	{
311	/* Bail out on floating point constants. */
312	if (!INTEGRAL_TYPE_P (TREE_TYPE (b.m_constant)))
313	return true;
314
315	b.ensure_closed (bound_kind);
316
317	switch (bound_kind)
318	{
319	default:
320	gcc_unreachable ();
321	case BK_LOWER:
322	/* Discard redundant bounds. */
323	if (m_lower_bound.m_constant)
324	{
325	m_lower_bound.ensure_closed (bound_kind: BK_LOWER);
326	if (tree_int_cst_le (t1: b.m_constant,
327	t2: m_lower_bound.m_constant))
328	return true;
329	}
330	if (m_upper_bound.m_constant)
331	{
332	m_upper_bound.ensure_closed (bound_kind: BK_UPPER);
333	/* Reject B <= V <= UPPER when B > UPPER. */
334	if (!tree_int_cst_le (t1: b.m_constant,
335	t2: m_upper_bound.m_constant))
336	return false;
337	}
338	m_lower_bound = b;
339	break;
340
341	case BK_UPPER:
342	/* Discard redundant bounds. */
343	if (m_upper_bound.m_constant)
344	{
345	m_upper_bound.ensure_closed (bound_kind: BK_UPPER);
346	if (!tree_int_cst_lt (t1: b.m_constant,
347	t2: m_upper_bound.m_constant))
348	return true;
349	}
350	if (m_lower_bound.m_constant)
351	{
352	m_lower_bound.ensure_closed (bound_kind: BK_LOWER);
353	/* Reject LOWER <= V <= B when LOWER > B. */
354	if (!tree_int_cst_le (t1: m_lower_bound.m_constant,
355	t2: b.m_constant))
356	return false;
357	}
358	m_upper_bound = b;
359	break;
360	}
361
362	return true;
363	}
364
365	/* Attempt to add (RANGE OP RHS_CONST) as a bound to this range.
366	Return true if feasible; false if infeasible. */
367
368	bool
369	range::add_bound (enum tree_code op, tree rhs_const)
370	{
371	switch (op)
372	{
373	default:
374	return true;
375	case LT_EXPR:
376	/* "V < RHS_CONST" */
377	return add_bound (b: bound (rhs_const, false), bound_kind: BK_UPPER);
378	case LE_EXPR:
379	/* "V <= RHS_CONST" */
380	return add_bound (b: bound (rhs_const, true), bound_kind: BK_UPPER);
381	case GE_EXPR:
382	/* "V >= RHS_CONST" */
383	return add_bound (b: bound (rhs_const, true), bound_kind: BK_LOWER);
384	case GT_EXPR:
385	/* "V > RHS_CONST" */
386	return add_bound (b: bound (rhs_const, false), bound_kind: BK_LOWER);
387	}
388	}
389
390	/* struct bounded_range. */
391
392	bounded_range::bounded_range (const_tree lower, const_tree upper)
393	: m_lower (const_cast<tree> (lower)),
394	m_upper (const_cast<tree> (upper))
395	{
396	if (lower && upper)
397	{
398	gcc_assert (TREE_CODE (m_lower) == INTEGER_CST);
399	gcc_assert (TREE_CODE (m_upper) == INTEGER_CST);
400	/* We should have lower <= upper. */
401	gcc_assert (!tree_int_cst_lt (m_upper, m_lower));
402	}
403	else
404	{
405	/* Purely for pending on-stack values, for
406	writing back to. */
407	gcc_assert (m_lower == NULL_TREE);
408	gcc_assert (m_lower == NULL_TREE);
409	}
410	}
411
412	static void
413	dump_cst (pretty_printer *pp, tree cst, bool show_types)
414	{
415	gcc_assert (cst);
416	if (show_types)
417	{
418	pp_character (pp, '(');
419	dump_generic_node (pp, TREE_TYPE (cst), 0, (dump_flags_t)0, false);
420	pp_character (pp, ')');
421	}
422	dump_generic_node (pp, cst, 0, (dump_flags_t)0, false);
423	}
424
425	/* Dump this object to PP. */
426
427	void
428	bounded_range::dump_to_pp (pretty_printer *pp, bool show_types) const
429	{
430	if (singleton_p ())
431	dump_cst (pp, cst: m_lower, show_types);
432	else
433	{
434	pp_character (pp, '[');
435	dump_cst (pp, cst: m_lower, show_types);
436	pp_string (pp, ", ");
437	dump_cst (pp, cst: m_upper, show_types);
438	pp_character (pp, ']');
439	}
440	}
441
442	/* Dump this object to stderr. */
443
444	void
445	bounded_range::dump (bool show_types) const
446	{
447	pretty_printer pp;
448	pp_format_decoder (&pp) = default_tree_printer;
449	pp_show_color (&pp) = pp_show_color (global_dc->printer);
450	pp.buffer->stream = stderr;
451	dump_to_pp (pp: &pp, show_types);
452	pp_newline (&pp);
453	pp_flush (&pp);
454	}
455
456	json::object *
457	bounded_range::to_json () const
458	{
459	json::object *range_obj = new json::object ();
460	set_json_attr (obj: range_obj, name: "lower", value: m_lower);
461	set_json_attr (obj: range_obj, name: "upper", value: m_upper);
462	return range_obj;
463	}
464
465	/* Subroutine of bounded_range::to_json. */
466
467	void
468	bounded_range::set_json_attr (json::object *obj, const char *name, tree value)
469	{
470	pretty_printer pp;
471	pp_format_decoder (&pp) = default_tree_printer;
472	pp_printf (&pp, "%E", value);
473	obj->set (key: name, v: new json::string (pp_formatted_text (&pp)));
474	}
475
476
477	/* Return true iff CST is within this range. */
478
479	bool
480	bounded_range::contains_p (tree cst) const
481	{
482	/* Reject if below lower bound. */
483	if (tree_int_cst_lt (t1: cst, t2: m_lower))
484	return false;
485	/* Reject if above lower bound. */
486	if (tree_int_cst_lt (t1: m_upper, t2: cst))
487	return false;
488	return true;
489	}
490
491	/* If this range intersects OTHER, return true, writing
492	the intersection to *OUT if OUT is non-NULL.
493	Return false if they do not intersect. */
494
495	bool
496	bounded_range::intersects_p (const bounded_range &other,
497	bounded_range *out) const
498	{
499	const tree max_lower
500	= (tree_int_cst_le (t1: m_lower, t2: other.m_lower)
501	? other.m_lower : m_lower);
502	gcc_assert (TREE_CODE (max_lower) == INTEGER_CST);
503	const tree min_upper
504	= (tree_int_cst_le (t1: m_upper, t2: other.m_upper)
505	? m_upper : other.m_upper);
506	gcc_assert (TREE_CODE (min_upper) == INTEGER_CST);
507
508	if (tree_int_cst_le (t1: max_lower, t2: min_upper))
509	{
510	if (out)
511	*out = bounded_range (max_lower, min_upper);
512	return true;
513	}
514	else
515	return false;
516	}
517
518	bool
519	bounded_range::operator== (const bounded_range &other) const
520	{
521	return (TREE_TYPE (m_lower) == TREE_TYPE (other.m_lower)
522	&& TREE_TYPE (m_upper) == TREE_TYPE (other.m_upper)
523	&& tree_int_cst_equal (m_lower, other.m_lower)
524	&& tree_int_cst_equal (m_upper, other.m_upper));
525	}
526
527	int
528	bounded_range::cmp (const bounded_range &br1, const bounded_range &br2)
529	{
530	if (int cmp_lower = tree_int_cst_compare (t1: br1.m_lower,
531	t2: br2.m_lower))
532	return cmp_lower;
533	return tree_int_cst_compare (t1: br1.m_upper, t2: br2.m_upper);
534	}
535
536	/* struct bounded_ranges. */
537
538	/* Construct a bounded_ranges instance from a single range. */
539
540	bounded_ranges::bounded_ranges (const bounded_range &range)
541	: m_ranges (1)
542	{
543	m_ranges.quick_push (obj: range);
544	canonicalize ();
545	validate ();
546	}
547
548	/* Construct a bounded_ranges instance from multiple ranges. */
549
550	bounded_ranges::bounded_ranges (const vec<bounded_range> &ranges)
551	: m_ranges (ranges.length ())
552	{
553	m_ranges.safe_splice (src: ranges);
554	canonicalize ();
555	validate ();
556	}
557
558	/* Construct a bounded_ranges instance for values of LHS for which
559	(LHS OP RHS_CONST) is true (e.g. "(LHS > 3)". */
560
561	bounded_ranges::bounded_ranges (enum tree_code op, tree rhs_const)
562	: m_ranges ()
563	{
564	gcc_assert (TREE_CODE (rhs_const) == INTEGER_CST);
565	tree type = TREE_TYPE (rhs_const);
566	switch (op)
567	{
568	default:
569	gcc_unreachable ();
570	case EQ_EXPR:
571	m_ranges.safe_push (obj: bounded_range (rhs_const, rhs_const));
572	break;
573
574	case GE_EXPR:
575	m_ranges.safe_push (obj: bounded_range (rhs_const, TYPE_MAX_VALUE (type)));
576	break;
577
578	case LE_EXPR:
579	m_ranges.safe_push (obj: bounded_range (TYPE_MIN_VALUE (type), rhs_const));
580	break;
581
582	case NE_EXPR:
583	if (tree_int_cst_lt (TYPE_MIN_VALUE (type), t2: rhs_const))
584	m_ranges.safe_push (obj: bounded_range (TYPE_MIN_VALUE (type),
585	minus_one (cst: rhs_const)));
586	if (tree_int_cst_lt (t1: rhs_const, TYPE_MAX_VALUE (type)))
587	m_ranges.safe_push (obj: bounded_range (plus_one (cst: rhs_const),
588	TYPE_MAX_VALUE (type)));
589	break;
590	case GT_EXPR:
591	if (tree_int_cst_lt (t1: rhs_const, TYPE_MAX_VALUE (type)))
592	m_ranges.safe_push (obj: bounded_range (plus_one (cst: rhs_const),
593	TYPE_MAX_VALUE (type)));
594	break;
595	case LT_EXPR:
596	if (tree_int_cst_lt (TYPE_MIN_VALUE (type), t2: rhs_const))
597	m_ranges.safe_push (obj: bounded_range (TYPE_MIN_VALUE (type),
598	minus_one (cst: rhs_const)));
599	break;
600	}
601	canonicalize ();
602	validate ();
603	}
604
605	/* Subroutine of ctors for fixing up m_ranges.
606	Also, initialize m_hash. */
607
608	void
609	bounded_ranges::canonicalize ()
610	{
611	/* Sort the ranges. */
612	m_ranges.qsort ([](const void *p1, const void *p2) -> int
613	{
614	const bounded_range &br1 = *(const bounded_range *)p1;
615	const bounded_range &br2 = *(const bounded_range *)p2;
616	return bounded_range::cmp (br1, br2);
617	});
618
619	/* Merge ranges that are touching or overlapping. */
620	for (unsigned i = 1; i < m_ranges.length (); )
621	{
622	bounded_range *prev = &m_ranges[i - 1];
623	const bounded_range *next = &m_ranges[i];
624	if (prev->intersects_p (other: *next, NULL)
625	|| (can_plus_one_p (cst: prev->m_upper)
626	&& tree_int_cst_equal (plus_one (cst: prev->m_upper),
627	next->m_lower)))
628	{
629	prev->m_upper = next->m_upper;
630	m_ranges.ordered_remove (ix: i);
631	}
632	else
633	i++;
634	}
635
636	/* Initialize m_hash. */
637	inchash::hash hstate (0);
638	for (const auto &iter : m_ranges)
639	{
640	inchash::add_expr (iter.m_lower, hstate);
641	inchash::add_expr (iter.m_upper, hstate);
642	}
643	m_hash = hstate.end ();
644	}
645
646	/* Assert that this object is valid. */
647
648	void
649	bounded_ranges::validate () const
650	{
651	/* Skip this in a release build. */
652	#if !CHECKING_P
653	return;
654	#endif
655
656	for (unsigned i = 1; i < m_ranges.length (); i++)
657	{
658	const bounded_range &prev = m_ranges[i - 1];
659	const bounded_range &next = m_ranges[i];
660
661	/* Give up if we somehow have incompatible different types. */
662	if (!types_compatible_p (TREE_TYPE (prev.m_upper),
663	TREE_TYPE (next.m_lower)))
664	continue;
665
666	/* Verify sorted. */
667	gcc_assert (tree_int_cst_lt (prev.m_upper, next.m_lower));
668
669	gcc_assert (can_plus_one_p (prev.m_upper));
670	/* otherwise there's no room for "next". */
671
672	/* Verify no ranges touch each other. */
673	gcc_assert (tree_int_cst_lt (plus_one (prev.m_upper), next.m_lower));
674	}
675	}
676
677	/* bounded_ranges equality operator. */
678
679	bool
680	bounded_ranges::operator== (const bounded_ranges &other) const
681	{
682	if (m_ranges.length () != other.m_ranges.length ())
683	return false;
684	for (unsigned i = 0; i < m_ranges.length (); i++)
685	{
686	if (m_ranges[i] != other.m_ranges[i])
687	return false;
688	}
689	return true;
690	}
691
692	/* Dump this object to PP. */
693
694	void
695	bounded_ranges::dump_to_pp (pretty_printer *pp, bool show_types) const
696	{
697	pp_character (pp, '{');
698	for (unsigned i = 0; i < m_ranges.length (); ++i)
699	{
700	if (i > 0)
701	pp_string (pp, ", ");
702	m_ranges[i].dump_to_pp (pp, show_types);
703	}
704	pp_character (pp, '}');
705	}
706
707	/* Dump this object to stderr. */
708
709	DEBUG_FUNCTION void
710	bounded_ranges::dump (bool show_types) const
711	{
712	pretty_printer pp;
713	pp_format_decoder (&pp) = default_tree_printer;
714	pp_show_color (&pp) = pp_show_color (global_dc->printer);
715	pp.buffer->stream = stderr;
716	dump_to_pp (pp: &pp, show_types);
717	pp_newline (&pp);
718	pp_flush (&pp);
719	}
720
721	json::value *
722	bounded_ranges::to_json () const
723	{
724	json::array *arr_obj = new json::array ();
725
726	for (unsigned i = 0; i < m_ranges.length (); ++i)
727	arr_obj->append (v: m_ranges[i].to_json ());
728
729	return arr_obj;
730	}
731
732	/* Determine whether (X OP RHS_CONST) is known to be true or false
733	for all X in the ranges expressed by this object. */
734
735	tristate
736	bounded_ranges::eval_condition (enum tree_code op,
737	tree rhs_const,
738	bounded_ranges_manager *mgr) const
739	{
740	/* Convert (X OP RHS_CONST) to a bounded_ranges instance and find
741	the intersection of that with this object. */
742	bounded_ranges other (op, rhs_const);
743	const bounded_ranges *intersection
744	= mgr->get_or_create_intersection (a: this, b: &other);
745
746	if (intersection->m_ranges.length () > 0)
747	{
748	/* We can use pointer equality to check for equality,
749	due to instance consolidation. */
750	if (intersection == this)
751	return tristate (tristate::TS_TRUE);
752	else
753	return tristate (tristate::TS_UNKNOWN);
754	}
755	else
756	/* No intersection. */
757	return tristate (tristate::TS_FALSE);
758	}
759
760	/* Return true if CST is within any of the ranges. */
761
762	bool
763	bounded_ranges::contain_p (tree cst) const
764	{
765	gcc_assert (TREE_CODE (cst) == INTEGER_CST);
766	for (const auto &iter : m_ranges)
767	{
768	/* TODO: should we optimize this based on sorting? */
769	if (iter.contains_p (cst))
770	return true;
771	}
772	return false;
773	}
774
775	int
776	bounded_ranges::cmp (const bounded_ranges *a, const bounded_ranges *b)
777	{
778	if (int cmp_length = ((int)a->m_ranges.length ()
779	- (int)b->m_ranges.length ()))
780	return cmp_length;
781	for (unsigned i = 0; i < a->m_ranges.length (); i++)
782	{
783	if (int cmp_range = bounded_range::cmp (br1: a->m_ranges[i], br2: b->m_ranges[i]))
784	return cmp_range;
785	}
786	/* They are equal. They ought to have been consolidated, so we should
787	have two pointers to the same object. */
788	gcc_assert (a == b);
789	return 0;
790	}
791
792	/* class bounded_ranges_manager. */
793
794	/* bounded_ranges_manager's dtor. */
795
796	bounded_ranges_manager::~bounded_ranges_manager ()
797	{
798	/* Delete the managed objects. */
799	for (const auto &iter : m_map)
800	delete iter.second;
801	}
802
803	/* Get the bounded_ranges instance for the empty set, creating it if
804	necessary. */
805
806	const bounded_ranges *
807	bounded_ranges_manager::get_or_create_empty ()
808	{
809	auto_vec<bounded_range> empty_vec;
810
811	return consolidate (new bounded_ranges (empty_vec));
812	}
813
814	/* Get the bounded_ranges instance for {CST}, creating it if necessary. */
815
816	const bounded_ranges *
817	bounded_ranges_manager::get_or_create_point (const_tree cst)
818	{
819	gcc_assert (TREE_CODE (cst) == INTEGER_CST);
820
821	return get_or_create_range (lower_bound: cst, upper_bound: cst);
822	}
823
824	/* Get the bounded_ranges instance for {[LOWER_BOUND..UPPER_BOUND]},
825	creating it if necessary. */
826
827	const bounded_ranges *
828	bounded_ranges_manager::get_or_create_range (const_tree lower_bound,
829	const_tree upper_bound)
830	{
831	gcc_assert (TREE_CODE (lower_bound) == INTEGER_CST);
832	gcc_assert (TREE_CODE (upper_bound) == INTEGER_CST);
833
834	return consolidate
835	(new bounded_ranges (bounded_range (lower_bound, upper_bound)));
836	}
837
838	/* Get the bounded_ranges instance for the union of OTHERS,
839	creating it if necessary. */
840
841	const bounded_ranges *
842	bounded_ranges_manager::
843	get_or_create_union (const vec <const bounded_ranges *> &others)
844	{
845	auto_vec<bounded_range> ranges;
846	for (const auto &r : others)
847	ranges.safe_splice (src: r->m_ranges);
848	return consolidate (new bounded_ranges (ranges));
849	}
850
851	/* Get the bounded_ranges instance for the intersection of A and B,
852	creating it if necessary. */
853
854	const bounded_ranges *
855	bounded_ranges_manager::get_or_create_intersection (const bounded_ranges *a,
856	const bounded_ranges *b)
857	{
858	auto_vec<bounded_range> ranges;
859	unsigned a_idx = 0;
860	unsigned b_idx = 0;
861	while (a_idx < a->m_ranges.length ()
862	&& b_idx < b->m_ranges.length ())
863	{
864	const bounded_range &r_a = a->m_ranges[a_idx];
865	const bounded_range &r_b = b->m_ranges[b_idx];
866
867	bounded_range intersection (NULL_TREE, NULL_TREE);
868	if (r_a.intersects_p (other: r_b, out: &intersection))
869	{
870	ranges.safe_push (obj: intersection);
871	}
872	if (tree_int_cst_lt (t1: r_a.m_lower, t2: r_b.m_lower))
873	{
874	a_idx++;
875	}
876	else
877	{
878	if (tree_int_cst_lt (t1: r_a.m_upper, t2: r_b.m_upper))
879	a_idx++;
880	else
881	b_idx++;
882	}
883	}
884
885	return consolidate (new bounded_ranges (ranges));
886	}
887
888	/* Get the bounded_ranges instance for the inverse of OTHER relative
889	to TYPE, creating it if necessary.
890	This is for use when handling "default" in switch statements, where
891	OTHER represents all the other cases. */
892
893	const bounded_ranges *
894	bounded_ranges_manager::get_or_create_inverse (const bounded_ranges *other,
895	tree type)
896	{
897	tree min_val = TYPE_MIN_VALUE (type);
898	tree max_val = TYPE_MAX_VALUE (type);
899	if (other->m_ranges.length () == 0)
900	return get_or_create_range (lower_bound: min_val, upper_bound: max_val);
901	auto_vec<bounded_range> ranges;
902	tree first_lb = other->m_ranges[0].m_lower;
903	if (tree_int_cst_lt (t1: min_val, t2: first_lb)
904	&& can_minus_one_p (cst: first_lb))
905	ranges.safe_push (obj: bounded_range (min_val,
906	minus_one (cst: first_lb)));
907	for (unsigned i = 1; i < other->m_ranges.length (); i++)
908	{
909	tree prev_ub = other->m_ranges[i - 1].m_upper;
910	tree iter_lb = other->m_ranges[i].m_lower;
911	gcc_assert (tree_int_cst_lt (prev_ub, iter_lb));
912	if (can_plus_one_p (cst: prev_ub) && can_minus_one_p (cst: iter_lb))
913	ranges.safe_push (obj: bounded_range (plus_one (cst: prev_ub),
914	minus_one (cst: iter_lb)));
915	}
916	tree last_ub
917	= other->m_ranges[other->m_ranges.length () - 1].m_upper;
918	if (tree_int_cst_lt (t1: last_ub, t2: max_val)
919	&& can_plus_one_p (cst: last_ub))
920	ranges.safe_push (obj: bounded_range (plus_one (cst: last_ub), max_val));
921
922	return consolidate (new bounded_ranges (ranges));
923	}
924
925	/* If an object equal to INST is already present, delete INST and
926	return the existing object.
927	Otherwise add INST and return it. */
928
929	const bounded_ranges *
930	bounded_ranges_manager::consolidate (bounded_ranges *inst)
931	{
932	if (bounded_ranges **slot = m_map.get (k: inst))
933	{
934	delete inst;
935	return *slot;
936	}
937	m_map.put (k: inst, v: inst);
938	return inst;
939	}
940
941	/* Get the bounded_ranges instance for EDGE of SWITCH_STMT,
942	creating it if necessary, and caching it by edge. */
943
944	const bounded_ranges *
945	bounded_ranges_manager::
946	get_or_create_ranges_for_switch (const switch_cfg_superedge *edge,
947	const gswitch *switch_stmt)
948	{
949	/* Look in per-edge cache. */
950	if (const bounded_ranges ** slot = m_edge_cache.get (k: edge))
951	return *slot;
952
953	/* Not yet in cache. */
954	const bounded_ranges *all_cases_ranges
955	= create_ranges_for_switch (edge: *edge, switch_stmt);
956	m_edge_cache.put (k: edge, v: all_cases_ranges);
957	return all_cases_ranges;
958	}
959
960	/* Get the bounded_ranges instance for EDGE of SWITCH_STMT,
961	creating it if necessary, for edges for which the per-edge
962	cache has not yet been populated. */
963
964	const bounded_ranges *
965	bounded_ranges_manager::
966	create_ranges_for_switch (const switch_cfg_superedge &edge,
967	const gswitch *switch_stmt)
968	{
969	/* Get the ranges for each case label. */
970	auto_vec <const bounded_ranges *> case_ranges_vec
971	(gimple_switch_num_labels (gs: switch_stmt));
972
973	for (tree case_label : edge.get_case_labels ())
974	{
975	/* Get the ranges for this case label. */
976	const bounded_ranges *case_ranges
977	= make_case_label_ranges (switch_stmt, case_label);
978	case_ranges_vec.quick_push (obj: case_ranges);
979	}
980
981	/* Combine all the ranges for each case label into a single collection
982	of ranges. */
983	const bounded_ranges *all_cases_ranges
984	= get_or_create_union (others: case_ranges_vec);
985	return all_cases_ranges;
986	}
987
988	/* Get the bounded_ranges instance for CASE_LABEL within
989	SWITCH_STMT. */
990
991	const bounded_ranges *
992	bounded_ranges_manager::
993	make_case_label_ranges (const gswitch *switch_stmt,
994	tree case_label)
995	{
996	gcc_assert (TREE_CODE (case_label) == CASE_LABEL_EXPR);
997	tree lower_bound = CASE_LOW (case_label);
998	tree upper_bound = CASE_HIGH (case_label);
999	if (lower_bound)
1000	{
1001	if (upper_bound)
1002	/* Range. */
1003	return get_or_create_range (lower_bound, upper_bound);
1004	else
1005	/* Single-value. */
1006	return get_or_create_point (cst: lower_bound);
1007	}
1008	else
1009	{
1010	/* The default case.
1011	Add exclusions based on the other cases. */
1012	auto_vec <const bounded_ranges *> other_case_ranges
1013	(gimple_switch_num_labels (gs: switch_stmt));
1014	for (unsigned other_idx = 1;
1015	other_idx < gimple_switch_num_labels (gs: switch_stmt);
1016	other_idx++)
1017	{
1018	tree other_label = gimple_switch_label (gs: switch_stmt,
1019	index: other_idx);
1020	const bounded_ranges *other_ranges
1021	= make_case_label_ranges (switch_stmt, case_label: other_label);
1022	other_case_ranges.quick_push (obj: other_ranges);
1023	}
1024	const bounded_ranges *other_cases_ranges
1025	= get_or_create_union (others: other_case_ranges);
1026	tree type = TREE_TYPE (gimple_switch_index (switch_stmt));
1027	return get_or_create_inverse (other: other_cases_ranges, type);
1028	}
1029	}
1030
1031	/* Dump the number of objects of each class that were managed by this
1032	manager to LOGGER.
1033	If SHOW_OBJS is true, also dump the objects themselves. */
1034
1035	void
1036	bounded_ranges_manager::log_stats (logger *logger, bool show_objs) const
1037	{
1038	LOG_SCOPE (logger);
1039	logger->log (fmt: " # %s: %li", "ranges", (long)m_map.elements ());
1040	if (!show_objs)
1041	return;
1042
1043	auto_vec<const bounded_ranges *> vec_objs (m_map.elements ());
1044	for (const auto &iter : m_map)
1045	vec_objs.quick_push (obj: iter.second);
1046	vec_objs.qsort
1047	([](const void *p1, const void *p2) -> int
1048	{
1049	const bounded_ranges *br1 = *(const bounded_ranges * const *)p1;
1050	const bounded_ranges *br2 = *(const bounded_ranges * const *)p2;
1051	return bounded_ranges::cmp (br1, br2);
1052	});
1053
1054	for (const auto &iter : vec_objs)
1055	{
1056	logger->start_log_line ();
1057	pretty_printer *pp = logger->get_printer ();
1058	pp_string (pp, " ");
1059	iter->dump_to_pp (pp, show_types: true);
1060	logger->end_log_line ();
1061	}
1062	}
1063
1064	/* class equiv_class. */
1065
1066	/* equiv_class's default ctor. */
1067
1068	equiv_class::equiv_class ()
1069	: m_constant (NULL_TREE), m_cst_sval (NULL), m_vars ()
1070	{
1071	}
1072
1073	/* equiv_class's copy ctor. */
1074
1075	equiv_class::equiv_class (const equiv_class &other)
1076	: m_constant (other.m_constant), m_cst_sval (other.m_cst_sval),
1077	m_vars (other.m_vars.length ())
1078	{
1079	for (const svalue *sval : other.m_vars)
1080	m_vars.quick_push (obj: sval);
1081	}
1082
1083	/* Print an all-on-one-line representation of this equiv_class to PP,
1084	which must support %E for trees. */
1085
1086	void
1087	equiv_class::print (pretty_printer *pp) const
1088	{
1089	pp_character (pp, '{');
1090	int i;
1091	const svalue *sval;
1092	FOR_EACH_VEC_ELT (m_vars, i, sval)
1093	{
1094	if (i > 0)
1095	pp_string (pp, " == ");
1096	sval->dump_to_pp (pp, simple: true);
1097	}
1098	if (m_constant)
1099	{
1100	if (i > 0)
1101	pp_string (pp, " == ");
1102	pp_printf (pp, "[m_constant]%qE", m_constant);
1103	}
1104	pp_character (pp, '}');
1105	}
1106
1107	/* Return a new json::object of the form
1108	{"svals" : [str],
1109	"constant" : optional str}. */
1110
1111	json::object *
1112	equiv_class::to_json () const
1113	{
1114	json::object *ec_obj = new json::object ();
1115
1116	json::array *sval_arr = new json::array ();
1117	for (const svalue *sval : m_vars)
1118	sval_arr->append (v: sval->to_json ());
1119	ec_obj->set (key: "svals", v: sval_arr);
1120
1121	if (m_constant)
1122	{
1123	pretty_printer pp;
1124	pp_format_decoder (&pp) = default_tree_printer;
1125	pp_printf (&pp, "%qE", m_constant);
1126	ec_obj->set (key: "constant", v: new json::string (pp_formatted_text (&pp)));
1127	}
1128
1129	return ec_obj;
1130	}
1131
1132	/* Generate a hash value for this equiv_class.
1133	This relies on the ordering of m_vars, and so this object needs to
1134	have been canonicalized for this to be meaningful. */
1135
1136	hashval_t
1137	equiv_class::hash () const
1138	{
1139	inchash::hash hstate;
1140
1141	inchash::add_expr (m_constant, hstate);
1142	for (const svalue * sval : m_vars)
1143	hstate.add_ptr (ptr: sval);
1144	return hstate.end ();
1145	}
1146
1147	/* Equality operator for equiv_class.
1148	This relies on the ordering of m_vars, and so this object
1149	and OTHER need to have been canonicalized for this to be
1150	meaningful. */
1151
1152	bool
1153	equiv_class::operator== (const equiv_class &other)
1154	{
1155	if (m_constant != other.m_constant)
1156	return false; // TODO: use tree equality here?
1157
1158	/* FIXME: should we compare m_cst_sval? */
1159
1160	if (m_vars.length () != other.m_vars.length ())
1161	return false;
1162
1163	int i;
1164	const svalue *sval;
1165	FOR_EACH_VEC_ELT (m_vars, i, sval)
1166	if (sval != other.m_vars[i])
1167	return false;
1168
1169	return true;
1170	}
1171
1172	/* Add SID to this equiv_class, using CM to check if it's a constant. */
1173
1174	void
1175	equiv_class::add (const svalue *sval)
1176	{
1177	gcc_assert (sval);
1178	if (tree cst = sval->maybe_get_constant ())
1179	{
1180	gcc_assert (CONSTANT_CLASS_P (cst));
1181	/* FIXME: should we canonicalize which svalue is the constant
1182	when there are multiple equal constants? */
1183	m_constant = cst;
1184	m_cst_sval = sval;
1185	}
1186	m_vars.safe_push (obj: sval);
1187	}
1188
1189	/* Remove SID from this equivalence class.
1190	Return true if SID was the last var in the equivalence class (suggesting
1191	a possible leak). */
1192
1193	bool
1194	equiv_class::del (const svalue *sval)
1195	{
1196	gcc_assert (sval);
1197	gcc_assert (sval != m_cst_sval);
1198
1199	int i;
1200	const svalue *iv;
1201	FOR_EACH_VEC_ELT (m_vars, i, iv)
1202	{
1203	if (iv == sval)
1204	{
1205	m_vars[i] = m_vars[m_vars.length () - 1];
1206	m_vars.pop ();
1207	return m_vars.length () == 0;
1208	}
1209	}
1210
1211	/* SVAL must be in the class. */
1212	gcc_unreachable ();
1213	return false;
1214	}
1215
1216	/* Get a representative member of this class, for handling cases
1217	where the IDs can change mid-traversal. */
1218
1219	const svalue *
1220	equiv_class::get_representative () const
1221	{
1222	gcc_assert (m_vars.length () > 0);
1223	return m_vars[0];
1224	}
1225
1226	/* Sort the svalues within this equiv_class. */
1227
1228	void
1229	equiv_class::canonicalize ()
1230	{
1231	m_vars.qsort (svalue::cmp_ptr_ptr);
1232	}
1233
1234	/* Return true if this EC contains a variable, false if it merely
1235	contains constants.
1236	Subroutine of constraint_manager::canonicalize, for removing
1237	redundant ECs. */
1238
1239	bool
1240	equiv_class::contains_non_constant_p () const
1241	{
1242	if (m_constant)
1243	{
1244	for (auto iter : m_vars)
1245	if (iter->maybe_get_constant ())
1246	continue;
1247	else
1248	/* We have {non-constant == constant}. */
1249	return true;
1250	/* We only have constants. */
1251	return false;
1252	}
1253	else
1254	/* Return true if we have {non-constant == non-constant}. */
1255	return m_vars.length () > 1;
1256	}
1257
1258	/* Get a debug string for C_OP. */
1259
1260	const char *
1261	constraint_op_code (enum constraint_op c_op)
1262	{
1263	switch (c_op)
1264	{
1265	default:
1266	gcc_unreachable ();
1267	case CONSTRAINT_NE: return "!=";
1268	case CONSTRAINT_LT: return "<";
1269	case CONSTRAINT_LE: return "<=";
1270	}
1271	}
1272
1273	/* Convert C_OP to an enum tree_code. */
1274
1275	enum tree_code
1276	constraint_tree_code (enum constraint_op c_op)
1277	{
1278	switch (c_op)
1279	{
1280	default:
1281	gcc_unreachable ();
1282	case CONSTRAINT_NE: return NE_EXPR;
1283	case CONSTRAINT_LT: return LT_EXPR;
1284	case CONSTRAINT_LE: return LE_EXPR;
1285	}
1286	}
1287
1288	/* Given "lhs C_OP rhs", determine "lhs T_OP rhs".
1289
1290	For example, given "x < y", then "x > y" is false. */
1291
1292	static tristate
1293	eval_constraint_op_for_op (enum constraint_op c_op, enum tree_code t_op)
1294	{
1295	switch (c_op)
1296	{
1297	default:
1298	gcc_unreachable ();
1299	case CONSTRAINT_NE:
1300	if (t_op == EQ_EXPR)
1301	return tristate (tristate::TS_FALSE);
1302	if (t_op == NE_EXPR)
1303	return tristate (tristate::TS_TRUE);
1304	break;
1305	case CONSTRAINT_LT:
1306	if (t_op == LT_EXPR || t_op == LE_EXPR || t_op == NE_EXPR)
1307	return tristate (tristate::TS_TRUE);
1308	if (t_op == EQ_EXPR || t_op == GT_EXPR || t_op == GE_EXPR)
1309	return tristate (tristate::TS_FALSE);
1310	break;
1311	case CONSTRAINT_LE:
1312	if (t_op == LE_EXPR)
1313	return tristate (tristate::TS_TRUE);
1314	if (t_op == GT_EXPR)
1315	return tristate (tristate::TS_FALSE);
1316	break;
1317	}
1318	return tristate (tristate::TS_UNKNOWN);
1319	}
1320
1321	/* class constraint. */
1322
1323	/* Print this constraint to PP (which must support %E for trees),
1324	using CM to look up equiv_class instances from ids. */
1325
1326	void
1327	constraint::print (pretty_printer *pp, const constraint_manager &cm) const
1328	{
1329	m_lhs.print (pp);
1330	pp_string (pp, ": ");
1331	m_lhs.get_obj (cm).print (pp);
1332	pp_string (pp, " ");
1333	pp_string (pp, constraint_op_code (c_op: m_op));
1334	pp_string (pp, " ");
1335	m_rhs.print (pp);
1336	pp_string (pp, ": ");
1337	m_rhs.get_obj (cm).print (pp);
1338	}
1339
1340	/* Return a new json::object of the form
1341	{"lhs" : int, the EC index
1342	"op" : str,
1343	"rhs" : int, the EC index}. */
1344
1345	json::object *
1346	constraint::to_json () const
1347	{
1348	json::object *con_obj = new json::object ();
1349
1350	con_obj->set (key: "lhs", v: new json::integer_number (m_lhs.as_int ()));
1351	con_obj->set (key: "op", v: new json::string (constraint_op_code (c_op: m_op)));
1352	con_obj->set (key: "rhs", v: new json::integer_number (m_rhs.as_int ()));
1353
1354	return con_obj;
1355	}
1356
1357	/* Generate a hash value for this constraint. */
1358
1359	hashval_t
1360	constraint::hash () const
1361	{
1362	inchash::hash hstate;
1363	hstate.add_int (v: m_lhs.m_idx);
1364	hstate.add_int (v: m_op);
1365	hstate.add_int (v: m_rhs.m_idx);
1366	return hstate.end ();
1367	}
1368
1369	/* Equality operator for constraints. */
1370
1371	bool
1372	constraint::operator== (const constraint &other) const
1373	{
1374	if (m_lhs != other.m_lhs)
1375	return false;
1376	if (m_op != other.m_op)
1377	return false;
1378	if (m_rhs != other.m_rhs)
1379	return false;
1380	return true;
1381	}
1382
1383	/* Return true if this constraint is implied by OTHER. */
1384
1385	bool
1386	constraint::implied_by (const constraint &other,
1387	const constraint_manager &cm) const
1388	{
1389	if (m_lhs == other.m_lhs)
1390	if (tree rhs_const = m_rhs.get_obj (cm).get_any_constant ())
1391	if (tree other_rhs_const = other.m_rhs.get_obj (cm).get_any_constant ())
1392	if (m_lhs.get_obj (cm).get_any_constant () == NULL_TREE)
1393	if (m_op == other.m_op)
1394	switch (m_op)
1395	{
1396	default:
1397	break;
1398	case CONSTRAINT_LE:
1399	case CONSTRAINT_LT:
1400	if (compare_constants (lhs_const: rhs_const,
1401	op: GE_EXPR,
1402	rhs_const: other_rhs_const).is_true ())
1403	return true;
1404	break;
1405	}
1406	return false;
1407	}
1408
1409	/* class bounded_ranges_constraint. */
1410
1411	void
1412	bounded_ranges_constraint::print (pretty_printer *pp,
1413	const constraint_manager &cm) const
1414	{
1415	m_ec_id.print (pp);
1416	pp_string (pp, ": ");
1417	m_ec_id.get_obj (cm).print (pp);
1418	pp_string (pp, ": ");
1419	m_ranges->dump_to_pp (pp, show_types: true);
1420	}
1421
1422	json::object *
1423	bounded_ranges_constraint::to_json () const
1424	{
1425	json::object *con_obj = new json::object ();
1426
1427	con_obj->set (key: "ec", v: new json::integer_number (m_ec_id.as_int ()));
1428	con_obj->set (key: "ranges", v: m_ranges->to_json ());
1429
1430	return con_obj;
1431	}
1432
1433	bool
1434	bounded_ranges_constraint::
1435	operator== (const bounded_ranges_constraint &other) const
1436	{
1437	if (m_ec_id != other.m_ec_id)
1438	return false;
1439
1440	/* We can compare by pointer, since the bounded_ranges_manager
1441	consolidates instances. */
1442	return m_ranges == other.m_ranges;
1443	}
1444
1445	void
1446	bounded_ranges_constraint::add_to_hash (inchash::hash *hstate) const
1447	{
1448	hstate->add_int (v: m_ec_id.m_idx);
1449	hstate->merge_hash (other: m_ranges->get_hash ());
1450	}
1451
1452	/* class equiv_class_id. */
1453
1454	/* Get the underlying equiv_class for this ID from CM. */
1455
1456	const equiv_class &
1457	equiv_class_id::get_obj (const constraint_manager &cm) const
1458	{
1459	return cm.get_equiv_class_by_index (idx: m_idx);
1460	}
1461
1462	/* Access the underlying equiv_class for this ID from CM. */
1463
1464	equiv_class &
1465	equiv_class_id::get_obj (constraint_manager &cm) const
1466	{
1467	return cm.get_equiv_class_by_index (idx: m_idx);
1468	}
1469
1470	/* Print this equiv_class_id to PP. */
1471
1472	void
1473	equiv_class_id::print (pretty_printer *pp) const
1474	{
1475	if (null_p ())
1476	pp_printf (pp, "null");
1477	else
1478	pp_printf (pp, "ec%i", m_idx);
1479	}
1480
1481	/* class constraint_manager. */
1482
1483	/* constraint_manager's copy ctor. */
1484
1485	constraint_manager::constraint_manager (const constraint_manager &other)
1486	: m_equiv_classes (other.m_equiv_classes.length ()),
1487	m_constraints (other.m_constraints.length ()),
1488	m_bounded_ranges_constraints (other.m_bounded_ranges_constraints.length ()),
1489	m_mgr (other.m_mgr)
1490	{
1491	int i;
1492	equiv_class *ec;
1493	FOR_EACH_VEC_ELT (other.m_equiv_classes, i, ec)
1494	m_equiv_classes.quick_push (obj: new equiv_class (*ec));
1495	constraint *c;
1496	FOR_EACH_VEC_ELT (other.m_constraints, i, c)
1497	m_constraints.quick_push (obj: *c);
1498	for (const auto &iter : other.m_bounded_ranges_constraints)
1499	m_bounded_ranges_constraints.quick_push (obj: iter);
1500	}
1501
1502	/* constraint_manager's assignment operator. */
1503
1504	constraint_manager&
1505	constraint_manager::operator= (const constraint_manager &other)
1506	{
1507	gcc_assert (m_equiv_classes.length () == 0);
1508	gcc_assert (m_constraints.length () == 0);
1509	gcc_assert (m_bounded_ranges_constraints.length () == 0);
1510
1511	int i;
1512	equiv_class *ec;
1513	m_equiv_classes.reserve (nelems: other.m_equiv_classes.length ());
1514	FOR_EACH_VEC_ELT (other.m_equiv_classes, i, ec)
1515	m_equiv_classes.quick_push (obj: new equiv_class (*ec));
1516	constraint *c;
1517	m_constraints.reserve (nelems: other.m_constraints.length ());
1518	FOR_EACH_VEC_ELT (other.m_constraints, i, c)
1519	m_constraints.quick_push (obj: *c);
1520	for (const auto &iter : other.m_bounded_ranges_constraints)
1521	m_bounded_ranges_constraints.quick_push (obj: iter);
1522
1523	return *this;
1524	}
1525
1526	/* Generate a hash value for this constraint_manager. */
1527
1528	hashval_t
1529	constraint_manager::hash () const
1530	{
1531	inchash::hash hstate;
1532	int i;
1533	equiv_class *ec;
1534	constraint *c;
1535
1536	FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
1537	hstate.merge_hash (other: ec->hash ());
1538	FOR_EACH_VEC_ELT (m_constraints, i, c)
1539	hstate.merge_hash (other: c->hash ());
1540	for (const auto &iter : m_bounded_ranges_constraints)
1541	iter.add_to_hash (hstate: &hstate);
1542	return hstate.end ();
1543	}
1544
1545	/* Equality operator for constraint_manager. */
1546
1547	bool
1548	constraint_manager::operator== (const constraint_manager &other) const
1549	{
1550	if (m_equiv_classes.length () != other.m_equiv_classes.length ())
1551	return false;
1552	if (m_constraints.length () != other.m_constraints.length ())
1553	return false;
1554	if (m_bounded_ranges_constraints.length ()
1555	!= other.m_bounded_ranges_constraints.length ())
1556	return false;
1557
1558	int i;
1559	equiv_class *ec;
1560
1561	FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
1562	if (!(*ec == *other.m_equiv_classes[i]))
1563	return false;
1564
1565	constraint *c;
1566
1567	FOR_EACH_VEC_ELT (m_constraints, i, c)
1568	if (!(*c == other.m_constraints[i]))
1569	return false;
1570
1571	for (unsigned i = 0; i < m_bounded_ranges_constraints.length (); i++)
1572	{
1573	if (m_bounded_ranges_constraints[i]
1574	!= other.m_bounded_ranges_constraints[i])
1575	return false;
1576	}
1577
1578	return true;
1579	}
1580
1581	/* Print this constraint_manager to PP (which must support %E for trees). */
1582
1583	void
1584	constraint_manager::print (pretty_printer *pp) const
1585	{
1586	pp_string (pp, "{");
1587	int i;
1588	equiv_class *ec;
1589	FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
1590	{
1591	if (i > 0)
1592	pp_string (pp, ", ");
1593	equiv_class_id (i).print (pp);
1594	pp_string (pp, ": ");
1595	ec->print (pp);
1596	}
1597	pp_string (pp, " | ");
1598	constraint *c;
1599	FOR_EACH_VEC_ELT (m_constraints, i, c)
1600	{
1601	if (i > 0)
1602	pp_string (pp, " && ");
1603	c->print (pp, cm: *this);
1604	}
1605	if (m_bounded_ranges_constraints.length ())
1606	{
1607	pp_string (pp, " | ");
1608	i = 0;
1609	for (const auto &iter : m_bounded_ranges_constraints)
1610	{
1611	if (i > 0)
1612	pp_string (pp, " && ");
1613	iter.print (pp, cm: *this);
1614	i++;
1615	}
1616	}
1617	pp_printf (pp, "}");
1618	}
1619
1620	/* Dump a representation of this constraint_manager to PP
1621	(which must support %E for trees). */
1622
1623	void
1624	constraint_manager::dump_to_pp (pretty_printer *pp, bool multiline) const
1625	{
1626	if (multiline)
1627	pp_string (pp, " ");
1628	pp_string (pp, "equiv classes:");
1629	if (multiline)
1630	pp_newline (pp);
1631	else
1632	pp_string (pp, " {");
1633	int i;
1634	equiv_class *ec;
1635	FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
1636	{
1637	if (multiline)
1638	pp_string (pp, " ");
1639	else if (i > 0)
1640	pp_string (pp, ", ");
1641	equiv_class_id (i).print (pp);
1642	pp_string (pp, ": ");
1643	ec->print (pp);
1644	if (multiline)
1645	pp_newline (pp);
1646	}
1647	if (multiline)
1648	pp_string (pp, " ");
1649	else
1650	pp_string (pp, "}");
1651	pp_string (pp, "constraints:");
1652	if (multiline)
1653	pp_newline (pp);
1654	else
1655	pp_string (pp, "{");
1656	constraint *c;
1657	FOR_EACH_VEC_ELT (m_constraints, i, c)
1658	{
1659	if (multiline)
1660	pp_string (pp, " ");
1661	pp_printf (pp, "%i: ", i);
1662	c->print (pp, cm: *this);
1663	if (multiline)
1664	pp_newline (pp);
1665	}
1666	if (!multiline)
1667	pp_string (pp, "}");
1668	if (m_bounded_ranges_constraints.length ())
1669	{
1670	if (multiline)
1671	pp_string (pp, " ");
1672	pp_string (pp, "ranges:");
1673	if (multiline)
1674	pp_newline (pp);
1675	else
1676	pp_string (pp, "{");
1677	i = 0;
1678	for (const auto &iter : m_bounded_ranges_constraints)
1679	{
1680	if (multiline)
1681	pp_string (pp, " ");
1682	else if (i > 0)
1683	pp_string (pp, " && ");
1684	iter.print (pp, cm: *this);
1685	if (multiline)
1686	pp_newline (pp);
1687	i++;
1688	}
1689	if (!multiline)
1690	pp_string (pp, "}");
1691	}
1692	}
1693
1694	/* Dump a multiline representation of this constraint_manager to FP. */
1695
1696	void
1697	constraint_manager::dump (FILE *fp) const
1698	{
1699	pretty_printer pp;
1700	pp_format_decoder (&pp) = default_tree_printer;
1701	pp_show_color (&pp) = pp_show_color (global_dc->printer);
1702	pp.buffer->stream = fp;
1703	dump_to_pp (pp: &pp, multiline: true);
1704	pp_flush (&pp);
1705	}
1706
1707	/* Dump a multiline representation of this constraint_manager to stderr. */
1708
1709	DEBUG_FUNCTION void
1710	constraint_manager::dump () const
1711	{
1712	dump (stderr);
1713	}
1714
1715	/* Dump a multiline representation of CM to stderr. */
1716
1717	DEBUG_FUNCTION void
1718	debug (const constraint_manager &cm)
1719	{
1720	cm.dump ();
1721	}
1722
1723	/* Return a new json::object of the form
1724	{"ecs" : array of objects, one per equiv_class
1725	"constraints" : array of objects, one per constraint}. */
1726
1727	json::object *
1728	constraint_manager::to_json () const
1729	{
1730	json::object *cm_obj = new json::object ();
1731
1732	/* Equivalence classes. */
1733	{
1734	json::array *ec_arr = new json::array ();
1735	for (const equiv_class *ec : m_equiv_classes)
1736	ec_arr->append (v: ec->to_json ());
1737	cm_obj->set (key: "ecs", v: ec_arr);
1738	}
1739
1740	/* Constraints. */
1741	{
1742	json::array *con_arr = new json::array ();
1743	for (const constraint &c : m_constraints)
1744	con_arr->append (v: c.to_json ());
1745	cm_obj->set (key: "constraints", v: con_arr);
1746	}
1747
1748	/* m_bounded_ranges_constraints. */
1749	{
1750	json::array *con_arr = new json::array ();
1751	for (const auto &c : m_bounded_ranges_constraints)
1752	con_arr->append (v: c.to_json ());
1753	cm_obj->set (key: "bounded_ranges_constraints", v: con_arr);
1754	}
1755
1756	return cm_obj;
1757	}
1758
1759	/* Attempt to add the constraint LHS OP RHS to this constraint_manager.
1760	Return true if the constraint could be added (or is already true).
1761	Return false if the constraint contradicts existing knowledge. */
1762
1763	bool
1764	constraint_manager::add_constraint (const svalue *lhs,
1765	enum tree_code op,
1766	const svalue *rhs)
1767	{
1768	lhs = lhs->unwrap_any_unmergeable ();
1769	rhs = rhs->unwrap_any_unmergeable ();
1770
1771	/* Nothing can be known about unknown/poisoned values. */
1772	if (!lhs->can_have_associated_state_p ()
1773	|| !rhs->can_have_associated_state_p ())
1774	/* Not a contradiction. */
1775	return true;
1776
1777	/* Check the conditions on svalues. */
1778	{
1779	tristate t_cond = eval_condition (lhs, op, rhs);
1780
1781	/* If we already have the condition, do nothing. */
1782	if (t_cond.is_true ())
1783	return true;
1784
1785	/* Reject a constraint that would contradict existing knowledge, as
1786	unsatisfiable. */
1787	if (t_cond.is_false ())
1788	return false;
1789	}
1790
1791	equiv_class_id lhs_ec_id = get_or_add_equiv_class (sval: lhs);
1792	equiv_class_id rhs_ec_id = get_or_add_equiv_class (sval: rhs);
1793
1794	/* Check the stronger conditions on ECs. */
1795	{
1796	tristate t = eval_condition (lhs: lhs_ec_id, op, rhs: rhs_ec_id);
1797
1798	/* Discard constraints that are already known. */
1799	if (t.is_true ())
1800	return true;
1801
1802	/* Reject unsatisfiable constraints. */
1803	if (t.is_false ())
1804	return false;
1805	}
1806
1807	/* If adding
1808	(SVAL + OFFSET) > CST,
1809	then that can imply:
1810	SVAL > (CST - OFFSET). */
1811	if (const binop_svalue *lhs_binop = lhs->dyn_cast_binop_svalue ())
1812	if (tree rhs_cst = rhs->maybe_get_constant ())
1813	if (tree offset = lhs_binop->get_arg1 ()->maybe_get_constant ())
1814	if ((op == GT_EXPR || op == LT_EXPR
1815	|| op == GE_EXPR || op == LE_EXPR)
1816	&& lhs_binop->get_op () == PLUS_EXPR)
1817	{
1818	tree offset_of_cst = fold_build2 (MINUS_EXPR, TREE_TYPE (rhs_cst),
1819	rhs_cst, offset);
1820	const svalue *implied_lhs = lhs_binop->get_arg0 ();
1821	enum tree_code implied_op = op;
1822	const svalue *implied_rhs
1823	= m_mgr->get_or_create_constant_svalue (cst_expr: offset_of_cst);
1824	if (!add_constraint (lhs: implied_lhs, op: implied_op, rhs: implied_rhs))
1825	return false;
1826	/* The above add_constraint could lead to EC merger, so we need
1827	to refresh the EC IDs. */
1828	lhs_ec_id = get_or_add_equiv_class (sval: lhs);
1829	rhs_ec_id = get_or_add_equiv_class (sval: rhs);
1830	}
1831
1832	add_unknown_constraint (lhs_ec_id, op, rhs_ec_id);
1833	return true;
1834	}
1835
1836	/* Attempt to add the constraint LHS_EC_ID OP RHS_EC_ID to this
1837	constraint_manager.
1838	Return true if the constraint could be added (or is already true).
1839	Return false if the constraint contradicts existing knowledge. */
1840
1841	bool
1842	constraint_manager::add_constraint (equiv_class_id lhs_ec_id,
1843	enum tree_code op,
1844	equiv_class_id rhs_ec_id)
1845	{
1846	tristate t = eval_condition (lhs: lhs_ec_id, op, rhs: rhs_ec_id);
1847
1848	/* Discard constraints that are already known. */
1849	if (t.is_true ())
1850	return true;
1851
1852	/* Reject unsatisfiable constraints. */
1853	if (t.is_false ())
1854	return false;
1855
1856	add_unknown_constraint (lhs_ec_id, op, rhs_ec_id);
1857	return true;
1858	}
1859
1860	/* Add the constraint LHS_EC_ID OP RHS_EC_ID to this constraint_manager,
1861	where the constraint has already been checked for being "unknown". */
1862
1863	void
1864	constraint_manager::add_unknown_constraint (equiv_class_id lhs_ec_id,
1865	enum tree_code op,
1866	equiv_class_id rhs_ec_id)
1867	{
1868	gcc_assert (lhs_ec_id != rhs_ec_id);
1869
1870	/* For now, simply accumulate constraints, without attempting any further
1871	optimization. */
1872	switch (op)
1873	{
1874	case EQ_EXPR:
1875	{
1876	/* Merge rhs_ec into lhs_ec. */
1877	equiv_class &lhs_ec_obj = lhs_ec_id.get_obj (cm&: *this);
1878	const equiv_class &rhs_ec_obj = rhs_ec_id.get_obj (cm&: *this);
1879
1880	int i;
1881	const svalue *sval;
1882	FOR_EACH_VEC_ELT (rhs_ec_obj.m_vars, i, sval)
1883	lhs_ec_obj.add (sval);
1884
1885	if (rhs_ec_obj.m_constant)
1886	{
1887	lhs_ec_obj.m_constant = rhs_ec_obj.m_constant;
1888	lhs_ec_obj.m_cst_sval = rhs_ec_obj.m_cst_sval;
1889	}
1890
1891	/* Drop rhs equivalence class, overwriting it with the
1892	final ec (which might be the same one). */
1893	equiv_class_id final_ec_id = m_equiv_classes.length () - 1;
1894	equiv_class *old_ec = m_equiv_classes[rhs_ec_id.m_idx];
1895	equiv_class *final_ec = m_equiv_classes.pop ();
1896	if (final_ec != old_ec)
1897	m_equiv_classes[rhs_ec_id.m_idx] = final_ec;
1898	delete old_ec;
1899	if (lhs_ec_id == final_ec_id)
1900	lhs_ec_id = rhs_ec_id;
1901
1902	/* Update the constraints. */
1903	constraint *c;
1904	FOR_EACH_VEC_ELT (m_constraints, i, c)
1905	{
1906	/* Update references to the rhs_ec so that
1907	they refer to the lhs_ec. */
1908	if (c->m_lhs == rhs_ec_id)
1909	c->m_lhs = lhs_ec_id;
1910	if (c->m_rhs == rhs_ec_id)
1911	c->m_rhs = lhs_ec_id;
1912
1913	/* Renumber all constraints that refer to the final rhs_ec
1914	to the old rhs_ec, where the old final_ec now lives. */
1915	if (c->m_lhs == final_ec_id)
1916	c->m_lhs = rhs_ec_id;
1917	if (c->m_rhs == final_ec_id)
1918	c->m_rhs = rhs_ec_id;
1919	}
1920	bounded_ranges_constraint *brc;
1921	FOR_EACH_VEC_ELT (m_bounded_ranges_constraints, i, brc)
1922	{
1923	if (brc->m_ec_id == rhs_ec_id)
1924	brc->m_ec_id = lhs_ec_id;
1925	if (brc->m_ec_id == final_ec_id)
1926	brc->m_ec_id = rhs_ec_id;
1927	}
1928
1929	/* We may now have self-comparisons due to the merger; these
1930	constraints should be removed. */
1931	unsigned read_index, write_index;
1932	VEC_ORDERED_REMOVE_IF (m_constraints, read_index, write_index, c,
1933	(c->m_lhs == c->m_rhs));
1934	}
1935	break;
1936	case GE_EXPR:
1937	add_constraint_internal (lhs_id: rhs_ec_id, c_op: CONSTRAINT_LE, rhs_id: lhs_ec_id);
1938	break;
1939	case LE_EXPR:
1940	add_constraint_internal (lhs_id: lhs_ec_id, c_op: CONSTRAINT_LE, rhs_id: rhs_ec_id);
1941	break;
1942	case NE_EXPR:
1943	add_constraint_internal (lhs_id: lhs_ec_id, c_op: CONSTRAINT_NE, rhs_id: rhs_ec_id);
1944	break;
1945	case GT_EXPR:
1946	add_constraint_internal (lhs_id: rhs_ec_id, c_op: CONSTRAINT_LT, rhs_id: lhs_ec_id);
1947	break;
1948	case LT_EXPR:
1949	add_constraint_internal (lhs_id: lhs_ec_id, c_op: CONSTRAINT_LT, rhs_id: rhs_ec_id);
1950	break;
1951	default:
1952	/* do nothing. */
1953	break;
1954	}
1955	validate ();
1956	}
1957
1958	/* Subroutine of constraint_manager::add_constraint, for handling all
1959	operations other than equality (for which equiv classes are merged). */
1960
1961	void
1962	constraint_manager::add_constraint_internal (equiv_class_id lhs_id,
1963	enum constraint_op c_op,
1964	equiv_class_id rhs_id)
1965	{
1966	if (m_constraints.length () >= (unsigned)param_analyzer_max_constraints)
1967	return;
1968
1969	constraint new_c (lhs_id, c_op, rhs_id);
1970
1971	/* Remove existing constraints that would be implied by the
1972	new constraint. */
1973	unsigned read_index, write_index;
1974	constraint *c;
1975	VEC_ORDERED_REMOVE_IF (m_constraints, read_index, write_index, c,
1976	(c->implied_by (new_c, *this)));
1977
1978	/* Add the constraint. */
1979	m_constraints.safe_push (obj: new_c);
1980
1981	/* We don't yet update m_bounded_ranges_constraints here yet. */
1982
1983	if (!flag_analyzer_transitivity)
1984	return;
1985
1986	if (c_op != CONSTRAINT_NE)
1987	{
1988	/* The following can potentially add EQ_EXPR facts, which could lead
1989	to ECs being merged, which would change the meaning of the EC IDs.
1990	Hence we need to do this via representatives. */
1991	const svalue *lhs = lhs_id.get_obj (cm&: *this).get_representative ();
1992	const svalue *rhs = rhs_id.get_obj (cm&: *this).get_representative ();
1993
1994	/* We have LHS </<= RHS */
1995
1996	/* Handle transitivity of ordering by adding additional constraints
1997	based on what we already knew.
1998
1999	So if we have already have:
2000	(a < b)
2001	(c < d)
2002	Then adding:
2003	(b < c)
2004	will also add:
2005	(a < c)
2006	(b < d)
2007	We need to recurse to ensure we also add:
2008	(a < d).
2009	We call the checked add_constraint to avoid adding constraints
2010	that are already present. Doing so also ensures termination
2011	in the case of cycles.
2012
2013	We also check for single-element ranges, adding EQ_EXPR facts
2014	where we discover them. For example 3 < x < 5 implies
2015	that x == 4 (if x is an integer). */
2016	for (unsigned i = 0; i < m_constraints.length (); i++)
2017	{
2018	const constraint *other = &m_constraints[i];
2019	if (other->is_ordering_p ())
2020	{
2021	/* Refresh the EC IDs, in case any mergers have happened. */
2022	lhs_id = get_or_add_equiv_class (sval: lhs);
2023	rhs_id = get_or_add_equiv_class (sval: rhs);
2024
2025	tree lhs_const = lhs_id.get_obj (cm&: *this).m_constant;
2026	tree rhs_const = rhs_id.get_obj (cm&: *this).m_constant;
2027	tree other_lhs_const
2028	= other->m_lhs.get_obj (cm&: *this).m_constant;
2029	tree other_rhs_const
2030	= other->m_rhs.get_obj (cm&: *this).m_constant;
2031
2032	/* We have "LHS </<= RHS" and "other.lhs </<= other.rhs". */
2033
2034	/* If we have LHS </<= RHS and RHS </<= LHS, then we have a
2035	cycle. */
2036	if (rhs_id == other->m_lhs
2037	&& other->m_rhs == lhs_id)
2038	{
2039	/* We must have equality for this to be possible. */
2040	gcc_assert (c_op == CONSTRAINT_LE
2041	&& other->m_op == CONSTRAINT_LE);
2042	add_constraint (lhs_ec_id: lhs_id, op: EQ_EXPR, rhs_ec_id: rhs_id);
2043	/* Adding an equality will merge the two ECs and potentially
2044	reorganize the constraints. Stop iterating. */
2045	return;
2046	}
2047	/* Otherwise, check for transitivity. */
2048	if (rhs_id == other->m_lhs)
2049	{
2050	/* With RHS == other.lhs, we have:
2051	"LHS </<= (RHS, other.lhs) </<= other.rhs"
2052	and thus this implies "LHS </<= other.rhs". */
2053
2054	/* Do we have a tightly-constrained range? */
2055	if (lhs_const
2056	&& !rhs_const
2057	&& other_rhs_const)
2058	{
2059	range r (bound (lhs_const, c_op == CONSTRAINT_LE),
2060	bound (other_rhs_const,
2061	other->m_op == CONSTRAINT_LE));
2062	if (tree constant = r.constrained_to_single_element ())
2063	{
2064	const svalue *cst_sval
2065	= m_mgr->get_or_create_constant_svalue (cst_expr: constant);
2066	add_constraint
2067	(lhs_ec_id: rhs_id, op: EQ_EXPR,
2068	rhs_ec_id: get_or_add_equiv_class (sval: cst_sval));
2069	return;
2070	}
2071	}
2072
2073	/* Otherwise, add the constraint implied by transitivity. */
2074	enum tree_code new_op
2075	= ((c_op == CONSTRAINT_LE && other->m_op == CONSTRAINT_LE)
2076	? LE_EXPR : LT_EXPR);
2077	add_constraint (lhs_ec_id: lhs_id, op: new_op, rhs_ec_id: other->m_rhs);
2078	}
2079	else if (other->m_rhs == lhs_id)
2080	{
2081	/* With other.rhs == LHS, we have:
2082	"other.lhs </<= (other.rhs, LHS) </<= RHS"
2083	and thus this implies "other.lhs </<= RHS". */
2084
2085	/* Do we have a tightly-constrained range? */
2086	if (other_lhs_const
2087	&& !lhs_const
2088	&& rhs_const)
2089	{
2090	range r (bound (other_lhs_const,
2091	other->m_op == CONSTRAINT_LE),
2092	bound (rhs_const,
2093	c_op == CONSTRAINT_LE));
2094	if (tree constant = r.constrained_to_single_element ())
2095	{
2096	const svalue *cst_sval
2097	= m_mgr->get_or_create_constant_svalue (cst_expr: constant);
2098	add_constraint
2099	(lhs_ec_id: lhs_id, op: EQ_EXPR,
2100	rhs_ec_id: get_or_add_equiv_class (sval: cst_sval));
2101	return;
2102	}
2103	}
2104
2105	/* Otherwise, add the constraint implied by transitivity. */
2106	enum tree_code new_op
2107	= ((c_op == CONSTRAINT_LE && other->m_op == CONSTRAINT_LE)
2108	? LE_EXPR : LT_EXPR);
2109	add_constraint (lhs_ec_id: other->m_lhs, op: new_op, rhs_ec_id: rhs_id);
2110	}
2111	}
2112	}
2113	}
2114	}
2115
2116	/* Attempt to add the constraint that SVAL is within RANGES to this
2117	constraint_manager.
2118
2119	Return true if the constraint was successfully added (or is already
2120	known to be true).
2121	Return false if the constraint contradicts existing knowledge. */
2122
2123	bool
2124	constraint_manager::add_bounded_ranges (const svalue *sval,
2125	const bounded_ranges *ranges)
2126	{
2127	/* If RANGES is just a singleton, convert this to adding the constraint:
2128	"SVAL == {the singleton}". */
2129	if (ranges->get_count () == 1
2130	&& ranges->get_range (idx: 0).singleton_p ())
2131	{
2132	tree range_cst = ranges->get_range (idx: 0).m_lower;
2133	const svalue *range_sval
2134	= m_mgr->get_or_create_constant_svalue (cst_expr: range_cst);
2135	return add_constraint (lhs: sval, op: EQ_EXPR, rhs: range_sval);
2136	}
2137
2138	sval = sval->unwrap_any_unmergeable ();
2139
2140	/* Nothing can be known about unknown/poisoned values. */
2141	if (!sval->can_have_associated_state_p ())
2142	/* Not a contradiction. */
2143	return true;
2144
2145	/* If SVAL is a constant, then we can look at RANGES directly. */
2146	if (tree cst = sval->maybe_get_constant ())
2147	{
2148	/* If the ranges contain CST, then it's a successful no-op;
2149	otherwise it's a contradiction. */
2150	return ranges->contain_p (cst);
2151	}
2152
2153	equiv_class_id ec_id = get_or_add_equiv_class (sval);
2154
2155	/* If the EC has a constant, it's either true or false. */
2156	const equiv_class &ec = ec_id.get_obj (cm&: *this);
2157	if (tree ec_cst = ec.get_any_constant ())
2158	{
2159	if (ranges->contain_p (cst: ec_cst))
2160	/* We already have SVAL == EC_CST, within RANGES, so
2161	we can discard RANGES and succeed. */
2162	return true;
2163	else
2164	/* We already have SVAL == EC_CST, not within RANGES, so
2165	we can reject RANGES as a contradiction. */
2166	return false;
2167	}
2168
2169	/* We have at most one per ec_id. */
2170	/* Iterate through each range in RANGES. */
2171	for (auto iter : m_bounded_ranges_constraints)
2172	{
2173	if (iter.m_ec_id == ec_id)
2174	{
2175	/* Update with intersection, or fail if empty. */
2176	bounded_ranges_manager *mgr = get_range_manager ();
2177	const bounded_ranges *intersection
2178	= mgr->get_or_create_intersection (a: iter.m_ranges, b: ranges);
2179	if (intersection->empty_p ())
2180	{
2181	/* No intersection; fail. */
2182	return false;
2183	}
2184	else
2185	{
2186	/* Update with intersection; succeed. */
2187	iter.m_ranges = intersection;
2188	validate ();
2189	return true;
2190	}
2191	}
2192	}
2193	m_bounded_ranges_constraints.safe_push
2194	(obj: bounded_ranges_constraint (ec_id, ranges));
2195
2196	validate ();
2197
2198	return true;
2199	}
2200
2201	/* Look for SVAL within the equivalence classes of this constraint_manager;
2202	if found, return true, writing the id to *OUT if OUT is non-NULL,
2203	otherwise return false. */
2204
2205	bool
2206	constraint_manager::get_equiv_class_by_svalue (const svalue *sval,
2207	equiv_class_id *out) const
2208	{
2209	/* TODO: should we have a map, rather than these searches? */
2210	int i;
2211	equiv_class *ec;
2212	FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
2213	{
2214	int j;
2215	const svalue *iv;
2216	FOR_EACH_VEC_ELT (ec->m_vars, j, iv)
2217	if (iv == sval)
2218	{
2219	if (out)
2220	*out = equiv_class_id (i);
2221	return true;
2222	}
2223	}
2224	return false;
2225	}
2226
2227	/* Tries to find a svalue inside another svalue. */
2228
2229	class sval_finder : public visitor
2230	{
2231	public:
2232	sval_finder (const svalue *query) : m_query (query), m_found (false)
2233	{
2234	}
2235
2236	bool found_query_p ()
2237	{
2238	return m_found;
2239	}
2240
2241	void visit_region_svalue (const region_svalue *sval)
2242	{
2243	m_found |= m_query == sval;
2244	}
2245
2246	void visit_constant_svalue (const constant_svalue *sval)
2247	{
2248	m_found |= m_query == sval;
2249	}
2250
2251	void visit_unknown_svalue (const unknown_svalue *sval)
2252	{
2253	m_found |= m_query == sval;
2254	}
2255
2256	void visit_poisoned_svalue (const poisoned_svalue *sval)
2257	{
2258	m_found |= m_query == sval;
2259	}
2260
2261	void visit_setjmp_svalue (const setjmp_svalue *sval)
2262	{
2263	m_found |= m_query == sval;
2264	}
2265
2266	void visit_initial_svalue (const initial_svalue *sval)
2267	{
2268	m_found |= m_query == sval;
2269	}
2270
2271	void visit_unaryop_svalue (const unaryop_svalue *sval)
2272	{
2273	m_found |= m_query == sval;
2274	}
2275
2276	void visit_binop_svalue (const binop_svalue *sval)
2277	{
2278	m_found |= m_query == sval;
2279	}
2280
2281	void visit_sub_svalue (const sub_svalue *sval)
2282	{
2283	m_found |= m_query == sval;
2284	}
2285
2286	void visit_repeated_svalue (const repeated_svalue *sval)
2287	{
2288	m_found |= m_query == sval;
2289	}
2290
2291	void visit_bits_within_svalue (const bits_within_svalue *sval)
2292	{
2293	m_found |= m_query == sval;
2294	}
2295
2296	void visit_unmergeable_svalue (const unmergeable_svalue *sval)
2297	{
2298	m_found |= m_query == sval;
2299	}
2300
2301	void visit_placeholder_svalue (const placeholder_svalue *sval)
2302	{
2303	m_found |= m_query == sval;
2304	}
2305
2306	void visit_widening_svalue (const widening_svalue *sval)
2307	{
2308	m_found |= m_query == sval;
2309	}
2310
2311	void visit_compound_svalue (const compound_svalue *sval)
2312	{
2313	m_found |= m_query == sval;
2314	}
2315
2316	void visit_conjured_svalue (const conjured_svalue *sval)
2317	{
2318	m_found |= m_query == sval;
2319	}
2320
2321	void visit_asm_output_svalue (const asm_output_svalue *sval)
2322	{
2323	m_found |= m_query == sval;
2324	}
2325
2326	void visit_const_fn_result_svalue (const const_fn_result_svalue *sval)
2327	{
2328	m_found |= m_query == sval;
2329	}
2330
2331	private:
2332	const svalue *m_query;
2333	bool m_found;
2334	};
2335
2336	/* Returns true if SVAL is constrained. */
2337
2338	bool
2339	constraint_manager::sval_constrained_p (const svalue *sval) const
2340	{
2341	int i;
2342	equiv_class *ec;
2343	sval_finder finder (sval);
2344	FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
2345	{
2346	int j;
2347	const svalue *iv;
2348	FOR_EACH_VEC_ELT (ec->m_vars, j, iv)
2349	{
2350	iv->accept (v: &finder);
2351	if (finder.found_query_p ())
2352	return true;
2353	}
2354	}
2355	return false;
2356	}
2357
2358	/* Ensure that SVAL has an equivalence class within this constraint_manager;
2359	return the ID of the class. */
2360
2361	equiv_class_id
2362	constraint_manager::get_or_add_equiv_class (const svalue *sval)
2363	{
2364	equiv_class_id result (-1);
2365
2366	gcc_assert (sval->can_have_associated_state_p ());
2367
2368	/* Convert all NULL pointers to (void *) to avoid state explosions
2369	involving all of the various (foo *)NULL vs (bar *)NULL. */
2370	if (sval->get_type ())
2371	if (POINTER_TYPE_P (sval->get_type ()))
2372	if (tree cst = sval->maybe_get_constant ())
2373	if (zerop (cst))
2374	sval = m_mgr->get_or_create_constant_svalue (null_pointer_node);
2375
2376	/* Try svalue match. */
2377	if (get_equiv_class_by_svalue (sval, out: &result))
2378	return result;
2379
2380	/* Try equality of constants. */
2381	if (tree cst = sval->maybe_get_constant ())
2382	{
2383	int i;
2384	equiv_class *ec;
2385	FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
2386	if (ec->m_constant
2387	&& types_compatible_p (TREE_TYPE (cst),
2388	TREE_TYPE (ec->m_constant)))
2389	{
2390	tree eq = fold_binary (EQ_EXPR, boolean_type_node,
2391	cst, ec->m_constant);
2392	if (eq == boolean_true_node)
2393	{
2394	ec->add (sval);
2395	return equiv_class_id (i);
2396	}
2397	}
2398	}
2399
2400
2401	/* Not found. */
2402	equiv_class *new_ec = new equiv_class ();
2403	new_ec->add (sval);
2404	m_equiv_classes.safe_push (obj: new_ec);
2405
2406	equiv_class_id new_id (m_equiv_classes.length () - 1);
2407
2408	return new_id;
2409	}
2410
2411	/* Evaluate the condition LHS_EC OP RHS_EC. */
2412
2413	tristate
2414	constraint_manager::eval_condition (equiv_class_id lhs_ec,
2415	enum tree_code op,
2416	equiv_class_id rhs_ec) const
2417	{
2418	if (lhs_ec == rhs_ec)
2419	{
2420	switch (op)
2421	{
2422	case EQ_EXPR:
2423	case GE_EXPR:
2424	case LE_EXPR:
2425	return tristate (tristate::TS_TRUE);
2426
2427	case NE_EXPR:
2428	case GT_EXPR:
2429	case LT_EXPR:
2430	return tristate (tristate::TS_FALSE);
2431	default:
2432	break;
2433	}
2434	}
2435
2436	tree lhs_const = lhs_ec.get_obj (cm: *this).get_any_constant ();
2437	tree rhs_const = rhs_ec.get_obj (cm: *this).get_any_constant ();
2438	if (lhs_const && rhs_const)
2439	{
2440	tristate result_for_constants
2441	= compare_constants (lhs_const, op, rhs_const);
2442	if (result_for_constants.is_known ())
2443	return result_for_constants;
2444	}
2445
2446	enum tree_code swapped_op = swap_tree_comparison (op);
2447
2448	int i;
2449	constraint *c;
2450	FOR_EACH_VEC_ELT (m_constraints, i, c)
2451	{
2452	if (c->m_lhs == lhs_ec
2453	&& c->m_rhs == rhs_ec)
2454	{
2455	tristate result_for_constraint
2456	= eval_constraint_op_for_op (c_op: c->m_op, t_op: op);
2457	if (result_for_constraint.is_known ())
2458	return result_for_constraint;
2459	}
2460	/* Swapped operands. */
2461	if (c->m_lhs == rhs_ec
2462	&& c->m_rhs == lhs_ec)
2463	{
2464	tristate result_for_constraint
2465	= eval_constraint_op_for_op (c_op: c->m_op, t_op: swapped_op);
2466	if (result_for_constraint.is_known ())
2467	return result_for_constraint;
2468	}
2469	}
2470
2471	/* We don't use m_bounded_ranges_constraints here yet. */
2472
2473	return tristate (tristate::TS_UNKNOWN);
2474	}
2475
2476	range
2477	constraint_manager::get_ec_bounds (equiv_class_id ec_id) const
2478	{
2479	range result;
2480
2481	int i;
2482	constraint *c;
2483	FOR_EACH_VEC_ELT (m_constraints, i, c)
2484	{
2485	if (c->m_lhs == ec_id)
2486	{
2487	if (tree other_cst = c->m_rhs.get_obj (cm: *this).get_any_constant ())
2488	switch (c->m_op)
2489	{
2490	default:
2491	gcc_unreachable ();
2492	case CONSTRAINT_NE:
2493	continue;
2494
2495	case CONSTRAINT_LT:
2496	/* We have "EC_ID < OTHER_CST". */
2497	result.add_bound (b: bound (other_cst, false), bound_kind: BK_UPPER);
2498	break;
2499
2500	case CONSTRAINT_LE:
2501	/* We have "EC_ID <= OTHER_CST". */
2502	result.add_bound (b: bound (other_cst, true), bound_kind: BK_UPPER);
2503	break;
2504	}
2505	}
2506	if (c->m_rhs == ec_id)
2507	{
2508	if (tree other_cst = c->m_lhs.get_obj (cm: *this).get_any_constant ())
2509	switch (c->m_op)
2510	{
2511	default:
2512	gcc_unreachable ();
2513	case CONSTRAINT_NE:
2514	continue;
2515
2516	case CONSTRAINT_LT:
2517	/* We have "OTHER_CST < EC_ID"
2518	i.e. "EC_ID > OTHER_CST". */
2519	result.add_bound (b: bound (other_cst, false), bound_kind: BK_LOWER);
2520	break;
2521
2522	case CONSTRAINT_LE:
2523	/* We have "OTHER_CST <= EC_ID"
2524	i.e. "EC_ID >= OTHER_CST". */
2525	result.add_bound (b: bound (other_cst, true), bound_kind: BK_LOWER);
2526	break;
2527	}
2528	}
2529	}
2530
2531	return result;
2532	}
2533
2534	/* Evaluate the condition LHS_EC OP RHS_CONST, avoiding the creation
2535	of equiv_class instances. */
2536
2537	tristate
2538	constraint_manager::eval_condition (equiv_class_id lhs_ec,
2539	enum tree_code op,
2540	tree rhs_const) const
2541	{
2542	gcc_assert (!lhs_ec.null_p ());
2543	gcc_assert (CONSTANT_CLASS_P (rhs_const));
2544
2545	if (tree lhs_const = lhs_ec.get_obj (cm: *this).get_any_constant ())
2546	return compare_constants (lhs_const, op, rhs_const);
2547
2548	/* Check for known inequalities of the form
2549	(LHS_EC != OTHER_CST) or (OTHER_CST != LHS_EC).
2550	If RHS_CONST == OTHER_CST, then we also know that LHS_EC != OTHER_CST.
2551	For example, we might have the constraint
2552	ptr != (void *)0
2553	so we want the condition
2554	ptr == (foo *)0
2555	to be false. */
2556	int i;
2557	constraint *c;
2558	FOR_EACH_VEC_ELT (m_constraints, i, c)
2559	{
2560	if (c->m_op == CONSTRAINT_NE)
2561	{
2562	if (c->m_lhs == lhs_ec)
2563	{
2564	if (tree other_cst = c->m_rhs.get_obj (cm: *this).get_any_constant ())
2565	if (compare_constants
2566	(lhs_const: rhs_const, op: EQ_EXPR, rhs_const: other_cst).is_true ())
2567	{
2568	switch (op)
2569	{
2570	case EQ_EXPR:
2571	return tristate (tristate::TS_FALSE);
2572	case NE_EXPR:
2573	return tristate (tristate::TS_TRUE);
2574	default:
2575	break;
2576	}
2577	}
2578	}
2579	if (c->m_rhs == lhs_ec)
2580	{
2581	if (tree other_cst = c->m_lhs.get_obj (cm: *this).get_any_constant ())
2582	if (compare_constants
2583	(lhs_const: rhs_const, op: EQ_EXPR, rhs_const: other_cst).is_true ())
2584	{
2585	switch (op)
2586	{
2587	case EQ_EXPR:
2588	return tristate (tristate::TS_FALSE);
2589	case NE_EXPR:
2590	return tristate (tristate::TS_TRUE);
2591	default:
2592	break;
2593	}
2594	}
2595	}
2596	}
2597	}
2598
2599	bounded_ranges_manager *mgr = get_range_manager ();
2600	for (const auto &iter : m_bounded_ranges_constraints)
2601	if (iter.m_ec_id == lhs_ec)
2602	return iter.m_ranges->eval_condition (op, rhs_const, mgr);
2603
2604	/* Look at existing bounds on LHS_EC. */
2605	range lhs_bounds = get_ec_bounds (ec_id: lhs_ec);
2606	tristate result = lhs_bounds.eval_condition (op, rhs_const);
2607	if (result.is_known ())
2608	return result;
2609
2610	/* Also reject if range::add_bound fails. */
2611	if (!lhs_bounds.add_bound (op, rhs_const))
2612	return tristate (false);
2613
2614	return tristate::unknown ();
2615	}
2616
2617	/* Return true iff "LHS == RHS" is known to be impossible due to
2618	derived conditions.
2619
2620	Look for an EC containing an EC_VAL of the form (LHS OP CST).
2621	If found, see if (LHS OP CST) == EC_VAL is false.
2622	If so, we know this condition is false.
2623
2624	For example, if we already know that
2625	(X & CST_MASK) == Y
2626	and we're evaluating X == Z, we can test to see if
2627	(Z & CST_MASK) == EC_VAL
2628	and thus if:
2629	(Z & CST_MASK) == Y
2630	and reject this if we know that's false. */
2631
2632	bool
2633	constraint_manager::impossible_derived_conditions_p (const svalue *lhs,
2634	const svalue *rhs) const
2635	{
2636	int i;
2637	equiv_class *ec;
2638	FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
2639	{
2640	for (const svalue *ec_sval : ec->m_vars)
2641	switch (ec_sval->get_kind ())
2642	{
2643	default:
2644	break;
2645	case SK_BINOP:
2646	{
2647	const binop_svalue *iter_binop
2648	= as_a <const binop_svalue *> (p: ec_sval);
2649	if (lhs == iter_binop->get_arg0 ()
2650	&& iter_binop->get_type ())
2651	if (iter_binop->get_arg1 ()->get_kind () == SK_CONSTANT)
2652	{
2653	/* Try evalating EC_SVAL with LHS
2654	as the value of EC_SVAL's lhs, and see if it's
2655	consistent with existing knowledge. */
2656	const svalue *subst_bin_op
2657	= m_mgr->get_or_create_binop
2658	(type: iter_binop->get_type (),
2659	op: iter_binop->get_op (),
2660	arg0: rhs,
2661	arg1: iter_binop->get_arg1 ());
2662	tristate t = eval_condition (lhs: subst_bin_op,
2663	op: EQ_EXPR,
2664	rhs: ec_sval);
2665	if (t.is_false ())
2666	return true; /* Impossible. */
2667	}
2668	}
2669	break;
2670	}
2671	}
2672	/* Not known to be impossible. */
2673	return false;
2674	}
2675
2676
2677	/* Evaluate the condition LHS OP RHS, without modifying this
2678	constraint_manager (avoiding the creation of equiv_class instances). */
2679
2680	tristate
2681	constraint_manager::eval_condition (const svalue *lhs,
2682	enum tree_code op,
2683	const svalue *rhs) const
2684	{
2685	lhs = lhs->unwrap_any_unmergeable ();
2686	rhs = rhs->unwrap_any_unmergeable ();
2687
2688	/* Nothing can be known about unknown or poisoned values. */
2689	if (lhs->get_kind () == SK_UNKNOWN
2690	|| lhs->get_kind () == SK_POISONED
2691	|| rhs->get_kind () == SK_UNKNOWN
2692	|| rhs->get_kind () == SK_POISONED)
2693	return tristate (tristate::TS_UNKNOWN);
2694
2695	if (lhs == rhs
2696	&& !(FLOAT_TYPE_P (lhs->get_type ())
2697	|| FLOAT_TYPE_P (rhs->get_type ())))
2698	{
2699	switch (op)
2700	{
2701	case EQ_EXPR:
2702	case GE_EXPR:
2703	case LE_EXPR:
2704	return tristate (tristate::TS_TRUE);
2705
2706	case NE_EXPR:
2707	case GT_EXPR:
2708	case LT_EXPR:
2709	return tristate (tristate::TS_FALSE);
2710	default:
2711	break;
2712	}
2713	}
2714
2715	equiv_class_id lhs_ec (-1);
2716	equiv_class_id rhs_ec (-1);
2717	get_equiv_class_by_svalue (sval: lhs, out: &lhs_ec);
2718	get_equiv_class_by_svalue (sval: rhs, out: &rhs_ec);
2719	if (!lhs_ec.null_p () && !rhs_ec.null_p ())
2720	{
2721	tristate result_for_ecs
2722	= eval_condition (lhs_ec, op, rhs_ec);
2723	if (result_for_ecs.is_known ())
2724	return result_for_ecs;
2725	}
2726
2727	if (op == EQ_EXPR
2728	&& impossible_derived_conditions_p (lhs, rhs))
2729	return false;
2730
2731	/* If at least one is not in an EC, we have no constraints
2732	comparing LHS and RHS yet.
2733	They might still be comparable if one (or both) is a constant.
2734
2735	Alternatively, we can also get here if we had ECs but they weren't
2736	comparable. Again, constant comparisons might give an answer. */
2737	tree lhs_const = lhs->maybe_get_constant ();
2738	tree rhs_const = rhs->maybe_get_constant ();
2739	if (lhs_const && rhs_const)
2740	{
2741	tristate result_for_constants
2742	= compare_constants (lhs_const, op, rhs_const);
2743	if (result_for_constants.is_known ())
2744	return result_for_constants;
2745	}
2746
2747	if (!lhs_ec.null_p ())
2748	{
2749	if (rhs_const)
2750	return eval_condition (lhs_ec, op, rhs_const);
2751	}
2752	if (!rhs_ec.null_p ())
2753	{
2754	if (lhs_const)
2755	{
2756	enum tree_code swapped_op = swap_tree_comparison (op);
2757	return eval_condition (lhs_ec: rhs_ec, op: swapped_op, rhs_const: lhs_const);
2758	}
2759	}
2760
2761	return tristate (tristate::TS_UNKNOWN);
2762	}
2763
2764	/* Delete any information about svalues identified by P.
2765	Such instances are removed from equivalence classes, and any
2766	redundant ECs and constraints are also removed.
2767	Accumulate stats into STATS. */
2768
2769	template <typename PurgeCriteria>
2770	void
2771	constraint_manager::purge (const PurgeCriteria &p, purge_stats *stats)
2772	{
2773	/* Delete any svalues identified by P within the various equivalence
2774	classes. */
2775	for (unsigned ec_idx = 0; ec_idx < m_equiv_classes.length (); )
2776	{
2777	equiv_class *ec = m_equiv_classes[ec_idx];
2778
2779	int i;
2780	const svalue *sval;
2781	bool delete_ec = false;
2782	FOR_EACH_VEC_ELT (ec->m_vars, i, sval)
2783	{
2784	if (sval == ec->m_cst_sval)
2785	continue;
2786	if (p.should_purge_p (sval))
2787	{
2788	if (ec->del (sval))
2789	if (!ec->m_constant)
2790	delete_ec = true;
2791	}
2792	}
2793
2794	if (delete_ec)
2795	{
2796	delete ec;
2797	m_equiv_classes.ordered_remove (ix: ec_idx);
2798	if (stats)
2799	stats->m_num_equiv_classes++;
2800
2801	/* Update the constraints, potentially removing some. */
2802	for (unsigned con_idx = 0; con_idx < m_constraints.length (); )
2803	{
2804	constraint *c = &m_constraints[con_idx];
2805
2806	/* Remove constraints that refer to the deleted EC. */
2807	if (c->m_lhs == ec_idx
2808	|| c->m_rhs == ec_idx)
2809	{
2810	m_constraints.ordered_remove (ix: con_idx);
2811	if (stats)
2812	stats->m_num_constraints++;
2813	}
2814	else
2815	{
2816	/* Renumber constraints that refer to ECs that have
2817	had their idx changed. */
2818	c->m_lhs.update_for_removal (other: ec_idx);
2819	c->m_rhs.update_for_removal (other: ec_idx);
2820
2821	con_idx++;
2822	}
2823	}
2824
2825	/* Update bounded_ranges_constraint instances. */
2826	for (unsigned r_idx = 0;
2827	r_idx < m_bounded_ranges_constraints.length (); )
2828	{
2829	bounded_ranges_constraint *brc
2830	= &m_bounded_ranges_constraints[r_idx];
2831
2832	/* Remove if it refers to the deleted EC. */
2833	if (brc->m_ec_id == ec_idx)
2834	{
2835	m_bounded_ranges_constraints.ordered_remove (ix: r_idx);
2836	if (stats)
2837	stats->m_num_bounded_ranges_constraints++;
2838	}
2839	else
2840	{
2841	/* Renumber any EC ids that refer to ECs that have
2842	had their idx changed. */
2843	brc->m_ec_id.update_for_removal (other: ec_idx);
2844	r_idx++;
2845	}
2846	}
2847	}
2848	else
2849	ec_idx++;
2850	}
2851
2852	/* Now delete any constraints that are purely between constants. */
2853	for (unsigned con_idx = 0; con_idx < m_constraints.length (); )
2854	{
2855	constraint *c = &m_constraints[con_idx];
2856	if (m_equiv_classes[c->m_lhs.m_idx]->m_vars.length () == 0
2857	&& m_equiv_classes[c->m_rhs.m_idx]->m_vars.length () == 0)
2858	{
2859	m_constraints.ordered_remove (ix: con_idx);
2860	if (stats)
2861	stats->m_num_constraints++;
2862	}
2863	else
2864	{
2865	con_idx++;
2866	}
2867	}
2868
2869	/* Finally, delete any ECs that purely contain constants and aren't
2870	referenced by any constraints. */
2871	for (unsigned ec_idx = 0; ec_idx < m_equiv_classes.length (); )
2872	{
2873	equiv_class *ec = m_equiv_classes[ec_idx];
2874	if (ec->m_vars.length () == 0)
2875	{
2876	equiv_class_id ec_id (ec_idx);
2877	bool has_constraint = false;
2878	for (unsigned con_idx = 0; con_idx < m_constraints.length ();
2879	con_idx++)
2880	{
2881	constraint *c = &m_constraints[con_idx];
2882	if (c->m_lhs == ec_id
2883	|| c->m_rhs == ec_id)
2884	{
2885	has_constraint = true;
2886	break;
2887	}
2888	}
2889	if (!has_constraint)
2890	{
2891	delete ec;
2892	m_equiv_classes.ordered_remove (ix: ec_idx);
2893	if (stats)
2894	stats->m_num_equiv_classes++;
2895
2896	/* Renumber constraints that refer to ECs that have
2897	had their idx changed. */
2898	for (unsigned con_idx = 0; con_idx < m_constraints.length ();
2899	con_idx++)
2900	{
2901	constraint *c = &m_constraints[con_idx];
2902	c->m_lhs.update_for_removal (other: ec_idx);
2903	c->m_rhs.update_for_removal (other: ec_idx);
2904	}
2905
2906	/* Likewise for m_bounded_ranges_constraints. */
2907	for (unsigned r_idx = 0;
2908	r_idx < m_bounded_ranges_constraints.length ();
2909	r_idx++)
2910	{
2911	bounded_ranges_constraint *brc
2912	= &m_bounded_ranges_constraints[r_idx];
2913	brc->m_ec_id.update_for_removal (other: ec_idx);
2914	}
2915
2916	continue;
2917	}
2918	}
2919	ec_idx++;
2920	}
2921
2922	validate ();
2923	}
2924
2925	/* Implementation of PurgeCriteria: purge svalues that are not live
2926	with respect to LIVE_SVALUES and MODEL. */
2927
2928	class dead_svalue_purger
2929	{
2930	public:
2931	dead_svalue_purger (const svalue_set &live_svalues,
2932	const region_model *model)
2933	: m_live_svalues (live_svalues), m_model (model)
2934	{
2935	}
2936
2937	bool should_purge_p (const svalue *sval) const
2938	{
2939	return !sval->live_p (live_svalues: &m_live_svalues, model: m_model);
2940	}
2941
2942	private:
2943	const svalue_set &m_live_svalues;
2944	const region_model *m_model;
2945	};
2946
2947	/* Purge dead svalues from equivalence classes and update constraints
2948	accordingly. */
2949
2950	void
2951	constraint_manager::
2952	on_liveness_change (const svalue_set &live_svalues,
2953	const region_model *model)
2954	{
2955	dead_svalue_purger p (live_svalues, model);
2956	purge (p, NULL);
2957	}
2958
2959	class svalue_purger
2960	{
2961	public:
2962	svalue_purger (const svalue *sval) : m_sval (sval) {}
2963
2964	bool should_purge_p (const svalue *sval) const
2965	{
2966	return sval->involves_p (other: m_sval);
2967	}
2968
2969	private:
2970	const svalue *m_sval;
2971	};
2972
2973	/* Purge any state involving SVAL. */
2974
2975	void
2976	constraint_manager::purge_state_involving (const svalue *sval)
2977	{
2978	svalue_purger p (sval);
2979	purge (p, NULL);
2980	}
2981
2982	/* Comparator for use by constraint_manager::canonicalize.
2983	Sort a pair of equiv_class instances, using the representative
2984	svalue as a sort key. */
2985
2986	static int
2987	equiv_class_cmp (const void *p1, const void *p2)
2988	{
2989	const equiv_class *ec1 = *(const equiv_class * const *)p1;
2990	const equiv_class *ec2 = *(const equiv_class * const *)p2;
2991
2992	const svalue *rep1 = ec1->get_representative ();
2993	const svalue *rep2 = ec2->get_representative ();
2994
2995	gcc_assert (rep1);
2996	gcc_assert (rep2);
2997
2998	return svalue::cmp_ptr (rep1, rep2);
2999	}
3000
3001	/* Comparator for use by constraint_manager::canonicalize.
3002	Sort a pair of constraint instances. */
3003
3004	static int
3005	constraint_cmp (const void *p1, const void *p2)
3006	{
3007	const constraint *c1 = (const constraint *)p1;
3008	const constraint *c2 = (const constraint *)p2;
3009	int lhs_cmp = c1->m_lhs.as_int () - c2->m_lhs.as_int ();
3010	if (lhs_cmp)
3011	return lhs_cmp;
3012	int rhs_cmp = c1->m_rhs.as_int () - c2->m_rhs.as_int ();
3013	if (rhs_cmp)
3014	return rhs_cmp;
3015	return c1->m_op - c2->m_op;
3016	}
3017
3018	/* Purge redundant equivalence classes and constraints, and reorder them
3019	within this constraint_manager into a canonical order, to increase the
3020	chances of finding equality with another instance. */
3021
3022	void
3023	constraint_manager::canonicalize ()
3024	{
3025	/* First, sort svalues within the ECs. */
3026	unsigned i;
3027	equiv_class *ec;
3028	FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
3029	ec->canonicalize ();
3030
3031	/* TODO: remove constraints where both sides have a constant, and are
3032	thus implicit. But does this break transitivity? */
3033
3034	/* We will be purging and reordering ECs.
3035	We will need to remap the equiv_class_ids in the constraints,
3036	so we need to store the original index of each EC.
3037	Build a lookup table, mapping from the representative svalue
3038	to the original equiv_class_id of that svalue. */
3039	hash_map<const svalue *, equiv_class_id> original_ec_id;
3040	const unsigned orig_num_equiv_classes = m_equiv_classes.length ();
3041	FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
3042	{
3043	const svalue *rep = ec->get_representative ();
3044	gcc_assert (rep);
3045	original_ec_id.put (k: rep, v: i);
3046	}
3047
3048	/* Find ECs used by constraints. */
3049	hash_set<const equiv_class *> used_ecs;
3050	constraint *c;
3051	FOR_EACH_VEC_ELT (m_constraints, i, c)
3052	{
3053	used_ecs.add (k: m_equiv_classes[c->m_lhs.as_int ()]);
3054	used_ecs.add (k: m_equiv_classes[c->m_rhs.as_int ()]);
3055	}
3056
3057	for (const auto &iter : m_bounded_ranges_constraints)
3058	used_ecs.add (k: m_equiv_classes[iter.m_ec_id.as_int ()]);
3059
3060	/* Purge unused ECs: those that aren't used by constraints and
3061	that effectively have only one svalue (either in m_constant
3062	or in m_vars). */
3063	{
3064	/* "unordered remove if" from a vec. */
3065	unsigned i = 0;
3066	while (i < m_equiv_classes.length ())
3067	{
3068	equiv_class *ec = m_equiv_classes[i];
3069	if (!used_ecs.contains (k: ec)
3070	&& !ec->contains_non_constant_p ())
3071	{
3072	m_equiv_classes.unordered_remove (ix: i);
3073	delete ec;
3074	}
3075	else
3076	i++;
3077	}
3078	}
3079
3080	/* Next, sort the surviving ECs into a canonical order. */
3081	m_equiv_classes.qsort (equiv_class_cmp);
3082
3083	/* Populate ec_id_map based on the old vs new EC ids. */
3084	one_way_id_map<equiv_class_id> ec_id_map (orig_num_equiv_classes);
3085	FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
3086	{
3087	const svalue *rep = ec->get_representative ();
3088	gcc_assert (rep);
3089	ec_id_map.put (src: *original_ec_id.get (k: rep), dst: i);
3090	}
3091
3092	/* Use ec_id_map to update the EC ids within the constraints. */
3093	FOR_EACH_VEC_ELT (m_constraints, i, c)
3094	{
3095	ec_id_map.update (id: &c->m_lhs);
3096	ec_id_map.update (id: &c->m_rhs);
3097	}
3098
3099	for (auto &iter : m_bounded_ranges_constraints)
3100	ec_id_map.update (id: &iter.m_ec_id);
3101
3102	/* Finally, sort the constraints. */
3103	m_constraints.qsort (constraint_cmp);
3104	}
3105
3106	/* Concrete subclass of fact_visitor for use by constraint_manager::merge.
3107	For every fact in CM_A, see if it is also true in *CM_B. Add such
3108	facts to *OUT. */
3109
3110	class merger_fact_visitor : public fact_visitor
3111	{
3112	public:
3113	merger_fact_visitor (const constraint_manager *cm_b,
3114	constraint_manager *out)
3115	: m_cm_b (cm_b), m_out (out)
3116	{}
3117
3118	void on_fact (const svalue *lhs, enum tree_code code, const svalue *rhs)
3119	final override
3120	{
3121	/* Special-case for widening. */
3122	if (lhs->get_kind () == SK_WIDENING)
3123	if (!m_cm_b->get_equiv_class_by_svalue (sval: lhs, NULL))
3124	{
3125	/* LHS isn't constrained within m_cm_b. */
3126	bool sat = m_out->add_constraint (lhs, op: code, rhs);
3127	gcc_assert (sat);
3128	return;
3129	}
3130
3131	if (m_cm_b->eval_condition (lhs, op: code, rhs).is_true ())
3132	{
3133	bool sat = m_out->add_constraint (lhs, op: code, rhs);
3134	if (!sat)
3135	{
3136	/* If -fanalyzer-transitivity is off, we can encounter cases
3137	where at least one of the two constraint_managers being merged
3138	is infeasible, but we only discover that infeasibility
3139	during merging (PR analyzer/96650).
3140	Silently drop such constraints. */
3141	gcc_assert (!flag_analyzer_transitivity);
3142	}
3143	}
3144	}
3145
3146	void on_ranges (const svalue *lhs_sval,
3147	const bounded_ranges *ranges) final override
3148	{
3149	for (const auto &iter : m_cm_b->m_bounded_ranges_constraints)
3150	{
3151	const equiv_class &ec_rhs = iter.m_ec_id.get_obj (cm: *m_cm_b);
3152	for (unsigned i = 0; i < ec_rhs.m_vars.length (); i++)
3153	{
3154	const svalue *rhs_sval = ec_rhs.m_vars[i];
3155	if (lhs_sval == rhs_sval)
3156	{
3157	/* Union of the two ranges. */
3158	auto_vec <const bounded_ranges *> pair (2);
3159	pair.quick_push (obj: ranges);
3160	pair.quick_push (obj: iter.m_ranges);
3161	bounded_ranges_manager *ranges_mgr
3162	= m_cm_b->get_range_manager ();
3163	const bounded_ranges *union_
3164	= ranges_mgr->get_or_create_union (others: pair);
3165	bool sat = m_out->add_bounded_ranges (sval: lhs_sval, ranges: union_);
3166	gcc_assert (sat);
3167	}
3168	}
3169	}
3170	}
3171
3172	private:
3173	const constraint_manager *m_cm_b;
3174	constraint_manager *m_out;
3175	};
3176
3177	/* Use MERGER to merge CM_A and CM_B into *OUT.
3178	If one thinks of a constraint_manager as a subset of N-dimensional
3179	space, this takes the union of the points of CM_A and CM_B, and
3180	expresses that into *OUT. Alternatively, it can be thought of
3181	as the intersection of the constraints. */
3182
3183	void
3184	constraint_manager::merge (const constraint_manager &cm_a,
3185	const constraint_manager &cm_b,
3186	constraint_manager *out)
3187	{
3188	/* Merge the equivalence classes and constraints.
3189	The easiest way to do this seems to be to enumerate all of the facts
3190	in cm_a, see which are also true in cm_b,
3191	and add those to *OUT. */
3192	merger_fact_visitor v (&cm_b, out);
3193	cm_a.for_each_fact (&v);
3194	}
3195
3196	/* Call VISITOR's on_fact vfunc repeatedly to express the various
3197	equivalence classes and constraints.
3198	This is used by constraint_manager::merge to find the common
3199	facts between two input constraint_managers. */
3200
3201	void
3202	constraint_manager::for_each_fact (fact_visitor *visitor) const
3203	{
3204	/* First, call EQ_EXPR within the various equivalence classes. */
3205	unsigned ec_idx;
3206	equiv_class *ec;
3207	FOR_EACH_VEC_ELT (m_equiv_classes, ec_idx, ec)
3208	{
3209	if (ec->m_cst_sval)
3210	{
3211	unsigned i;
3212	const svalue *sval;
3213	FOR_EACH_VEC_ELT (ec->m_vars, i, sval)
3214	visitor->on_fact (lhs: ec->m_cst_sval, EQ_EXPR, rhs: sval);
3215	}
3216	for (unsigned i = 0; i < ec->m_vars.length (); i++)
3217	for (unsigned j = i + 1; j < ec->m_vars.length (); j++)
3218	visitor->on_fact (lhs: ec->m_vars[i], EQ_EXPR, rhs: ec->m_vars[j]);
3219	}
3220
3221	/* Now, express the various constraints. */
3222	unsigned con_idx;
3223	constraint *c;
3224	FOR_EACH_VEC_ELT (m_constraints, con_idx, c)
3225	{
3226	const equiv_class &ec_lhs = c->m_lhs.get_obj (cm: *this);
3227	const equiv_class &ec_rhs = c->m_rhs.get_obj (cm: *this);
3228	enum tree_code code = constraint_tree_code (c_op: c->m_op);
3229
3230	if (ec_lhs.m_cst_sval)
3231	{
3232	for (unsigned j = 0; j < ec_rhs.m_vars.length (); j++)
3233	{
3234	visitor->on_fact (lhs: ec_lhs.m_cst_sval, code, rhs: ec_rhs.m_vars[j]);
3235	}
3236	}
3237	for (unsigned i = 0; i < ec_lhs.m_vars.length (); i++)
3238	{
3239	if (ec_rhs.m_cst_sval)
3240	visitor->on_fact (lhs: ec_lhs.m_vars[i], code, rhs: ec_rhs.m_cst_sval);
3241	for (unsigned j = 0; j < ec_rhs.m_vars.length (); j++)
3242	visitor->on_fact (lhs: ec_lhs.m_vars[i], code, rhs: ec_rhs.m_vars[j]);
3243	}
3244	}
3245
3246	for (const auto &iter : m_bounded_ranges_constraints)
3247	{
3248	const equiv_class &ec_lhs = iter.m_ec_id.get_obj (cm: *this);
3249	for (unsigned i = 0; i < ec_lhs.m_vars.length (); i++)
3250	{
3251	const svalue *lhs_sval = ec_lhs.m_vars[i];
3252	visitor->on_ranges (lhs: lhs_sval, ranges: iter.m_ranges);
3253	}
3254	}
3255	}
3256
3257	/* Subclass of fact_visitor for use by
3258	constraint_manager::replay_call_summary. */
3259
3260	class replay_fact_visitor : public fact_visitor
3261	{
3262	public:
3263	replay_fact_visitor (call_summary_replay &r,
3264	constraint_manager *out)
3265	: m_r (r), m_out (out), m_feasible (true)
3266	{}
3267
3268	bool feasible_p () const { return m_feasible; }
3269
3270	void on_fact (const svalue *lhs, enum tree_code code, const svalue *rhs)
3271	final override
3272	{
3273	const svalue *caller_lhs = m_r.convert_svalue_from_summary (lhs);
3274	if (!caller_lhs)
3275	return;
3276	const svalue *caller_rhs = m_r.convert_svalue_from_summary (rhs);
3277	if (!caller_rhs)
3278	return;
3279	if (!m_out->add_constraint (lhs: caller_lhs, op: code, rhs: caller_rhs))
3280	m_feasible = false;
3281	}
3282
3283	void on_ranges (const svalue *lhs_sval,
3284	const bounded_ranges *ranges) final override
3285	{
3286	const svalue *caller_lhs = m_r.convert_svalue_from_summary (lhs_sval);
3287	if (!caller_lhs)
3288	return;
3289	if (!m_out->add_bounded_ranges (sval: caller_lhs, ranges))
3290	m_feasible = false;
3291	}
3292
3293	private:
3294	call_summary_replay &m_r;
3295	constraint_manager *m_out;
3296	bool m_feasible;
3297	};
3298
3299	/* Attempt to use R to replay the constraints from SUMMARY into this object.
3300	Return true if it is feasible. */
3301
3302	bool
3303	constraint_manager::replay_call_summary (call_summary_replay &r,
3304	const constraint_manager &summary)
3305	{
3306	replay_fact_visitor v (r, this);
3307	summary.for_each_fact (visitor: &v);
3308	return v.feasible_p ();
3309	}
3310
3311	/* Assert that this object is valid. */
3312
3313	void
3314	constraint_manager::validate () const
3315	{
3316	/* Skip this in a release build. */
3317	#if !CHECKING_P
3318	return;
3319	#endif
3320
3321	int i;
3322	equiv_class *ec;
3323	FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
3324	{
3325	gcc_assert (ec);
3326
3327	int j;
3328	const svalue *sval;
3329	FOR_EACH_VEC_ELT (ec->m_vars, j, sval)
3330	gcc_assert (sval);
3331	if (ec->m_constant)
3332	{
3333	gcc_assert (CONSTANT_CLASS_P (ec->m_constant));
3334	gcc_assert (ec->m_cst_sval);
3335	}
3336	#if 0
3337	else
3338	gcc_assert (ec->m_vars.length () > 0);
3339	#endif
3340	}
3341
3342	constraint *c;
3343	FOR_EACH_VEC_ELT (m_constraints, i, c)
3344	{
3345	gcc_assert (!c->m_lhs.null_p ());
3346	gcc_assert (c->m_lhs.as_int () < (int)m_equiv_classes.length ());
3347	gcc_assert (!c->m_rhs.null_p ());
3348	gcc_assert (c->m_rhs.as_int () < (int)m_equiv_classes.length ());
3349	}
3350
3351	for (const auto &iter : m_bounded_ranges_constraints)
3352	{
3353	gcc_assert (!iter.m_ec_id.null_p ());
3354	gcc_assert (iter.m_ec_id.as_int () < (int)m_equiv_classes.length ());
3355	}
3356	}
3357
3358	bounded_ranges_manager *
3359	constraint_manager::get_range_manager () const
3360	{
3361	return m_mgr->get_range_manager ();
3362	}
3363
3364	#if CHECKING_P
3365
3366	namespace selftest {
3367
3368	/* Various constraint_manager selftests.
3369	These have to be written in terms of a region_model, since
3370	the latter is responsible for managing svalue instances. */
3371
3372	/* Verify that range::add_bound works as expected. */
3373
3374	static void
3375	test_range ()
3376	{
3377	tree int_0 = integer_zero_node;
3378	tree int_1 = integer_one_node;
3379	tree int_2 = build_int_cst (integer_type_node, 2);
3380	tree int_5 = build_int_cst (integer_type_node, 5);
3381
3382	{
3383	range r;
3384	ASSERT_FALSE (r.constrained_to_single_element ());
3385
3386	/* (r >= 1). */
3387	ASSERT_TRUE (r.add_bound (GE_EXPR, int_1));
3388
3389	/* Redundant. */
3390	ASSERT_TRUE (r.add_bound (GE_EXPR, int_0));
3391	ASSERT_TRUE (r.add_bound (GT_EXPR, int_0));
3392
3393	ASSERT_FALSE (r.constrained_to_single_element ());
3394
3395	/* Contradiction. */
3396	ASSERT_FALSE (r.add_bound (LT_EXPR, int_1));
3397
3398	/* (r < 5). */
3399	ASSERT_TRUE (r.add_bound (LT_EXPR, int_5));
3400	ASSERT_FALSE (r.constrained_to_single_element ());
3401
3402	/* Contradiction. */
3403	ASSERT_FALSE (r.add_bound (GE_EXPR, int_5));
3404
3405	/* (r < 2). */
3406	ASSERT_TRUE (r.add_bound (LT_EXPR, int_2));
3407	ASSERT_TRUE (r.constrained_to_single_element ());
3408
3409	/* Redundant. */
3410	ASSERT_TRUE (r.add_bound (LE_EXPR, int_1));
3411	ASSERT_TRUE (r.constrained_to_single_element ());
3412	}
3413	}
3414
3415	/* Verify that setting and getting simple conditions within a region_model
3416	work (thus exercising the underlying constraint_manager). */
3417
3418	static void
3419	test_constraint_conditions ()
3420	{
3421	tree int_42 = build_int_cst (integer_type_node, 42);
3422	tree int_0 = integer_zero_node;
3423
3424	tree x = build_global_decl (name: "x", integer_type_node);
3425	tree y = build_global_decl (name: "y", integer_type_node);
3426	tree z = build_global_decl (name: "z", integer_type_node);
3427
3428	/* Self-comparisons. */
3429	{
3430	region_model_manager mgr;
3431	region_model model (&mgr);
3432	ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, x);
3433	ASSERT_CONDITION_TRUE (model, x, LE_EXPR, x);
3434	ASSERT_CONDITION_TRUE (model, x, GE_EXPR, x);
3435	ASSERT_CONDITION_FALSE (model, x, NE_EXPR, x);
3436	ASSERT_CONDITION_FALSE (model, x, LT_EXPR, x);
3437	ASSERT_CONDITION_FALSE (model, x, GT_EXPR, x);
3438	}
3439
3440	/* Adding self-equality shouldn't add equiv classes. */
3441	{
3442	region_model_manager mgr;
3443	region_model model (&mgr);
3444	ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, x);
3445	ADD_SAT_CONSTRAINT (model, int_42, EQ_EXPR, int_42);
3446	/* ...even when done directly via svalues: */
3447	const svalue *sval_int_42 = model.get_rvalue (expr: int_42, NULL);
3448	bool sat = model.get_constraints ()->add_constraint (lhs: sval_int_42,
3449	op: EQ_EXPR,
3450	rhs: sval_int_42);
3451	ASSERT_TRUE (sat);
3452	ASSERT_EQ (model.get_constraints ()->m_equiv_classes.length (), 0);
3453	}
3454
3455	/* x == y. */
3456	{
3457	region_model_manager mgr;
3458	region_model model (&mgr);
3459	ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
3460
3461	ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
3462
3463	ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, y);
3464	ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
3465	ASSERT_CONDITION_TRUE (model, x, GE_EXPR, y);
3466	ASSERT_CONDITION_FALSE (model, x, NE_EXPR, y);
3467	ASSERT_CONDITION_FALSE (model, x, LT_EXPR, y);
3468	ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
3469
3470	/* Swapped operands. */
3471	ASSERT_CONDITION_TRUE (model, y, EQ_EXPR, x);
3472	ASSERT_CONDITION_TRUE (model, y, LE_EXPR, x);
3473	ASSERT_CONDITION_TRUE (model, y, GE_EXPR, x);
3474	ASSERT_CONDITION_FALSE (model, y, NE_EXPR, x);
3475	ASSERT_CONDITION_FALSE (model, y, LT_EXPR, x);
3476	ASSERT_CONDITION_FALSE (model, y, GT_EXPR, x);
3477
3478	/* Comparison with other var. */
3479	ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, z);
3480	ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, z);
3481	ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
3482	ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, z);
3483	ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, z);
3484	ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, z);
3485	}
3486
3487	/* x == y, then y == z */
3488	{
3489	region_model_manager mgr;
3490	region_model model (&mgr);
3491	ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
3492
3493	ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
3494	ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, z);
3495
3496	ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, z);
3497	ASSERT_CONDITION_TRUE (model, x, LE_EXPR, z);
3498	ASSERT_CONDITION_TRUE (model, x, GE_EXPR, z);
3499	ASSERT_CONDITION_FALSE (model, x, NE_EXPR, z);
3500	ASSERT_CONDITION_FALSE (model, x, LT_EXPR, z);
3501	ASSERT_CONDITION_FALSE (model, x, GT_EXPR, z);
3502	}
3503
3504	/* x != y. */
3505	{
3506	region_model_manager mgr;
3507	region_model model (&mgr);
3508
3509	ADD_SAT_CONSTRAINT (model, x, NE_EXPR, y);
3510
3511	ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
3512	ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
3513	ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, y);
3514	ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, y);
3515	ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, y);
3516	ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, y);
3517
3518	/* Swapped operands. */
3519	ASSERT_CONDITION_TRUE (model, y, NE_EXPR, x);
3520	ASSERT_CONDITION_FALSE (model, y, EQ_EXPR, x);
3521	ASSERT_CONDITION_UNKNOWN (model, y, LE_EXPR, x);
3522	ASSERT_CONDITION_UNKNOWN (model, y, GE_EXPR, x);
3523	ASSERT_CONDITION_UNKNOWN (model, y, LT_EXPR, x);
3524	ASSERT_CONDITION_UNKNOWN (model, y, GT_EXPR, x);
3525
3526	/* Comparison with other var. */
3527	ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, z);
3528	ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, z);
3529	ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
3530	ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, z);
3531	ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, z);
3532	ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, z);
3533	}
3534
3535	/* x < y. */
3536	{
3537	region_model_manager mgr;
3538	region_model model (&mgr);
3539
3540	ADD_SAT_CONSTRAINT (model, x, LT_EXPR, y);
3541
3542	ASSERT_CONDITION_TRUE (model, x, LT_EXPR, y);
3543	ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
3544	ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
3545	ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
3546	ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
3547	ASSERT_CONDITION_FALSE (model, x, GE_EXPR, y);
3548
3549	/* Swapped operands. */
3550	ASSERT_CONDITION_FALSE (model, y, LT_EXPR, x);
3551	ASSERT_CONDITION_FALSE (model, y, LE_EXPR, x);
3552	ASSERT_CONDITION_TRUE (model, y, NE_EXPR, x);
3553	ASSERT_CONDITION_FALSE (model, y, EQ_EXPR, x);
3554	ASSERT_CONDITION_TRUE (model, y, GT_EXPR, x);
3555	ASSERT_CONDITION_TRUE (model, y, GE_EXPR, x);
3556	}
3557
3558	/* x <= y. */
3559	{
3560	region_model_manager mgr;
3561	region_model model (&mgr);
3562
3563	ADD_SAT_CONSTRAINT (model, x, LE_EXPR, y);
3564
3565	ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, y);
3566	ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
3567	ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, y);
3568	ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
3569	ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
3570	ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, y);
3571
3572	/* Swapped operands. */
3573	ASSERT_CONDITION_FALSE (model, y, LT_EXPR, x);
3574	ASSERT_CONDITION_UNKNOWN (model, y, LE_EXPR, x);
3575	ASSERT_CONDITION_UNKNOWN (model, y, NE_EXPR, x);
3576	ASSERT_CONDITION_UNKNOWN (model, y, EQ_EXPR, x);
3577	ASSERT_CONDITION_UNKNOWN (model, y, GT_EXPR, x);
3578	ASSERT_CONDITION_TRUE (model, y, GE_EXPR, x);
3579	}
3580
3581	/* x > y. */
3582	{
3583	region_model_manager mgr;
3584	region_model model (&mgr);
3585
3586	ADD_SAT_CONSTRAINT (model, x, GT_EXPR, y);
3587
3588	ASSERT_CONDITION_TRUE (model, x, GT_EXPR, y);
3589	ASSERT_CONDITION_TRUE (model, x, GE_EXPR, y);
3590	ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
3591	ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
3592	ASSERT_CONDITION_FALSE (model, x, LT_EXPR, y);
3593	ASSERT_CONDITION_FALSE (model, x, LE_EXPR, y);
3594
3595	/* Swapped operands. */
3596	ASSERT_CONDITION_FALSE (model, y, GT_EXPR, x);
3597	ASSERT_CONDITION_FALSE (model, y, GE_EXPR, x);
3598	ASSERT_CONDITION_TRUE (model, y, NE_EXPR, x);
3599	ASSERT_CONDITION_FALSE (model, y, EQ_EXPR, x);
3600	ASSERT_CONDITION_TRUE (model, y, LT_EXPR, x);
3601	ASSERT_CONDITION_TRUE (model, y, LE_EXPR, x);
3602	}
3603
3604	/* x >= y. */
3605	{
3606	region_model_manager mgr;
3607	region_model model (&mgr);
3608
3609	ADD_SAT_CONSTRAINT (model, x, GE_EXPR, y);
3610
3611	ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, y);
3612	ASSERT_CONDITION_TRUE (model, x, GE_EXPR, y);
3613	ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, y);
3614	ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
3615	ASSERT_CONDITION_FALSE (model, x, LT_EXPR, y);
3616	ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, y);
3617
3618	/* Swapped operands. */
3619	ASSERT_CONDITION_FALSE (model, y, GT_EXPR, x);
3620	ASSERT_CONDITION_UNKNOWN (model, y, GE_EXPR, x);
3621	ASSERT_CONDITION_UNKNOWN (model, y, NE_EXPR, x);
3622	ASSERT_CONDITION_UNKNOWN (model, y, EQ_EXPR, x);
3623	ASSERT_CONDITION_UNKNOWN (model, y, LT_EXPR, x);
3624	ASSERT_CONDITION_TRUE (model, y, LE_EXPR, x);
3625	}
3626
3627	// TODO: implied orderings
3628
3629	/* Constants. */
3630	{
3631	region_model_manager mgr;
3632	region_model model (&mgr);
3633	ASSERT_CONDITION_FALSE (model, int_0, EQ_EXPR, int_42);
3634	ASSERT_CONDITION_TRUE (model, int_0, NE_EXPR, int_42);
3635	ASSERT_CONDITION_TRUE (model, int_0, LT_EXPR, int_42);
3636	ASSERT_CONDITION_TRUE (model, int_0, LE_EXPR, int_42);
3637	ASSERT_CONDITION_FALSE (model, int_0, GT_EXPR, int_42);
3638	ASSERT_CONDITION_FALSE (model, int_0, GE_EXPR, int_42);
3639	}
3640
3641	/* x == 0, y == 42. */
3642	{
3643	region_model_manager mgr;
3644	region_model model (&mgr);
3645	ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
3646	ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, int_42);
3647
3648	ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
3649	ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
3650	ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
3651	ASSERT_CONDITION_FALSE (model, x, GE_EXPR, y);
3652	ASSERT_CONDITION_TRUE (model, x, LT_EXPR, y);
3653	ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
3654	}
3655
3656	/* Unsatisfiable combinations. */
3657
3658	/* x == y && x != y. */
3659	{
3660	region_model_manager mgr;
3661	region_model model (&mgr);
3662	ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
3663	ADD_UNSAT_CONSTRAINT (model, x, NE_EXPR, y);
3664	}
3665
3666	/* x == 0 then x == 42. */
3667	{
3668	region_model_manager mgr;
3669	region_model model (&mgr);
3670	ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
3671	ADD_UNSAT_CONSTRAINT (model, x, EQ_EXPR, int_42);
3672	}
3673
3674	/* x == 0 then x != 0. */
3675	{
3676	region_model_manager mgr;
3677	region_model model (&mgr);
3678	ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
3679	ADD_UNSAT_CONSTRAINT (model, x, NE_EXPR, int_0);
3680	}
3681
3682	/* x == 0 then x > 0. */
3683	{
3684	region_model_manager mgr;
3685	region_model model (&mgr);
3686	ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
3687	ADD_UNSAT_CONSTRAINT (model, x, GT_EXPR, int_0);
3688	}
3689
3690	/* x != y && x == y. */
3691	{
3692	region_model_manager mgr;
3693	region_model model (&mgr);
3694	ADD_SAT_CONSTRAINT (model, x, NE_EXPR, y);
3695	ADD_UNSAT_CONSTRAINT (model, x, EQ_EXPR, y);
3696	}
3697
3698	/* x <= y && x > y. */
3699	{
3700	region_model_manager mgr;
3701	region_model model (&mgr);
3702	ADD_SAT_CONSTRAINT (model, x, LE_EXPR, y);
3703	ADD_UNSAT_CONSTRAINT (model, x, GT_EXPR, y);
3704	}
3705
3706	// etc
3707	}
3708
3709	/* Test transitivity of conditions. */
3710
3711	static void
3712	test_transitivity ()
3713	{
3714	tree a = build_global_decl (name: "a", integer_type_node);
3715	tree b = build_global_decl (name: "b", integer_type_node);
3716	tree c = build_global_decl (name: "c", integer_type_node);
3717	tree d = build_global_decl (name: "d", integer_type_node);
3718
3719	/* a == b, then c == d, then c == b. */
3720	{
3721	region_model_manager mgr;
3722	region_model model (&mgr);
3723	ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, b);
3724	ASSERT_CONDITION_UNKNOWN (model, b, EQ_EXPR, c);
3725	ASSERT_CONDITION_UNKNOWN (model, c, EQ_EXPR, d);
3726	ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, d);
3727
3728	ADD_SAT_CONSTRAINT (model, a, EQ_EXPR, b);
3729	ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, b);
3730
3731	ADD_SAT_CONSTRAINT (model, c, EQ_EXPR, d);
3732	ASSERT_CONDITION_TRUE (model, c, EQ_EXPR, d);
3733	ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, d);
3734
3735	ADD_SAT_CONSTRAINT (model, c, EQ_EXPR, b);
3736	ASSERT_CONDITION_TRUE (model, c, EQ_EXPR, b);
3737	ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, d);
3738	}
3739
3740	/* Transitivity: "a < b", "b < c" should imply "a < c". */
3741	{
3742	region_model_manager mgr;
3743	region_model model (&mgr);
3744	ADD_SAT_CONSTRAINT (model, a, LT_EXPR, b);
3745	ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c);
3746
3747	ASSERT_CONDITION_TRUE (model, a, LT_EXPR, c);
3748	ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
3749	}
3750
3751	/* Transitivity: "a <= b", "b < c" should imply "a < c". */
3752	{
3753	region_model_manager mgr;
3754	region_model model (&mgr);
3755	ADD_SAT_CONSTRAINT (model, a, LE_EXPR, b);
3756	ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c);
3757
3758	ASSERT_CONDITION_TRUE (model, a, LT_EXPR, c);
3759	ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
3760	}
3761
3762	/* Transitivity: "a <= b", "b <= c" should imply "a <= c". */
3763	{
3764	region_model_manager mgr;
3765	region_model model (&mgr);
3766	ADD_SAT_CONSTRAINT (model, a, LE_EXPR, b);
3767	ADD_SAT_CONSTRAINT (model, b, LE_EXPR, c);
3768
3769	ASSERT_CONDITION_TRUE (model, a, LE_EXPR, c);
3770	ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, c);
3771	}
3772
3773	/* Transitivity: "a > b", "b > c" should imply "a > c". */
3774	{
3775	region_model_manager mgr;
3776	region_model model (&mgr);
3777	ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b);
3778	ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c);
3779
3780	ASSERT_CONDITION_TRUE (model, a, GT_EXPR, c);
3781	ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
3782	}
3783
3784	/* Transitivity: "a >= b", "b > c" should imply " a > c". */
3785	{
3786	region_model_manager mgr;
3787	region_model model (&mgr);
3788	ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
3789	ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c);
3790
3791	ASSERT_CONDITION_TRUE (model, a, GT_EXPR, c);
3792	ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
3793	}
3794
3795	/* Transitivity: "a >= b", "b >= c" should imply "a >= c". */
3796	{
3797	region_model_manager mgr;
3798	region_model model (&mgr);
3799	ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
3800	ADD_SAT_CONSTRAINT (model, b, GE_EXPR, c);
3801
3802	ASSERT_CONDITION_TRUE (model, a, GE_EXPR, c);
3803	ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, c);
3804	}
3805
3806	/* Transitivity: "(a < b)", "(c < d)", "(b < c)" should
3807	imply the easy cases:
3808	(a < c)
3809	(b < d)
3810	but also that:
3811	(a < d). */
3812	{
3813	region_model_manager mgr;
3814	region_model model (&mgr);
3815	ADD_SAT_CONSTRAINT (model, a, LT_EXPR, b);
3816	ADD_SAT_CONSTRAINT (model, c, LT_EXPR, d);
3817	ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c);
3818
3819	ASSERT_CONDITION_TRUE (model, a, LT_EXPR, c);
3820	ASSERT_CONDITION_TRUE (model, b, LT_EXPR, d);
3821	ASSERT_CONDITION_TRUE (model, a, LT_EXPR, d);
3822	}
3823
3824	/* Transitivity: "a >= b", "b >= a" should imply that a == b. */
3825	{
3826	region_model_manager mgr;
3827	region_model model (&mgr);
3828	ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
3829	ADD_SAT_CONSTRAINT (model, b, GE_EXPR, a);
3830
3831	// TODO:
3832	ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, b);
3833
3834	/* The ECs for a and b should have merged, and any constraints removed. */
3835	ASSERT_EQ (model.get_constraints ()->m_equiv_classes.length (), 1);
3836	ASSERT_EQ (model.get_constraints ()->m_constraints.length (), 0);
3837	}
3838
3839	/* Transitivity: "a >= b", "b > a" should be impossible. */
3840	{
3841	region_model_manager mgr;
3842	region_model model (&mgr);
3843	ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
3844	ADD_UNSAT_CONSTRAINT (model, b, GT_EXPR, a);
3845	}
3846
3847	/* Transitivity: "a >= b", "b >= c", "c >= a" should imply
3848	that a == b == c. */
3849	{
3850	region_model_manager mgr;
3851	region_model model (&mgr);
3852	ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
3853	ADD_SAT_CONSTRAINT (model, b, GE_EXPR, c);
3854	ADD_SAT_CONSTRAINT (model, c, GE_EXPR, a);
3855
3856	ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, c);
3857	}
3858
3859	/* Transitivity: "a > b", "b > c", "c > a"
3860	should be impossible. */
3861	{
3862	region_model_manager mgr;
3863	region_model model (&mgr);
3864	ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b);
3865	ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c);
3866	ADD_UNSAT_CONSTRAINT (model, c, GT_EXPR, a);
3867	}
3868
3869	}
3870
3871	/* Test various conditionals involving constants where the results
3872	ought to be implied based on the values of the constants. */
3873
3874	static void
3875	test_constant_comparisons ()
3876	{
3877	tree int_1 = integer_one_node;
3878	tree int_3 = build_int_cst (integer_type_node, 3);
3879	tree int_4 = build_int_cst (integer_type_node, 4);
3880	tree int_5 = build_int_cst (integer_type_node, 5);
3881
3882	tree int_1023 = build_int_cst (integer_type_node, 1023);
3883	tree int_1024 = build_int_cst (integer_type_node, 1024);
3884
3885	tree a = build_global_decl (name: "a", integer_type_node);
3886	tree b = build_global_decl (name: "b", integer_type_node);
3887
3888	tree a_plus_one = build2 (PLUS_EXPR, integer_type_node, a, int_1);
3889
3890	/* Given a >= 1024, then a <= 1023 should be impossible. */
3891	{
3892	region_model_manager mgr;
3893	region_model model (&mgr);
3894	ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_1024);
3895	ADD_UNSAT_CONSTRAINT (model, a, LE_EXPR, int_1023);
3896	}
3897
3898	/* a > 4. */
3899	{
3900	region_model_manager mgr;
3901	region_model model (&mgr);
3902	ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_4);
3903	ASSERT_CONDITION_TRUE (model, a, GT_EXPR, int_4);
3904	ASSERT_CONDITION_TRUE (model, a, NE_EXPR, int_3);
3905	ASSERT_CONDITION_UNKNOWN (model, a, NE_EXPR, int_5);
3906	}
3907
3908	/* a <= 4. */
3909	{
3910	region_model_manager mgr;
3911	region_model model (&mgr);
3912	ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
3913	ASSERT_CONDITION_FALSE (model, a, GT_EXPR, int_4);
3914	ASSERT_CONDITION_FALSE (model, a, GT_EXPR, int_5);
3915	ASSERT_CONDITION_UNKNOWN (model, a, NE_EXPR, int_3);
3916	}
3917
3918	/* If "a > b" and "a == 3", then "b == 4" ought to be unsatisfiable. */
3919	{
3920	region_model_manager mgr;
3921	region_model model (&mgr);
3922	ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b);
3923	ADD_SAT_CONSTRAINT (model, a, EQ_EXPR, int_3);
3924	ADD_UNSAT_CONSTRAINT (model, b, EQ_EXPR, int_4);
3925	}
3926
3927	/* Various tests of int ranges where there is only one possible candidate. */
3928	{
3929	/* If "a <= 4" && "a > 3", then "a == 4",
3930	assuming a is of integral type. */
3931	{
3932	region_model_manager mgr;
3933	region_model model (&mgr);
3934	ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
3935	ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
3936	ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
3937	}
3938
3939	/* If "a > 3" && "a <= 4", then "a == 4",
3940	assuming a is of integral type. */
3941	{
3942	region_model_manager mgr;
3943	region_model model (&mgr);
3944	ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
3945	ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
3946	ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
3947	}
3948	/* If "a > 3" && "a < 5", then "a == 4",
3949	assuming a is of integral type. */
3950	{
3951	region_model_manager mgr;
3952	region_model model (&mgr);
3953	ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
3954	ADD_SAT_CONSTRAINT (model, a, LT_EXPR, int_5);
3955	ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
3956	}
3957	/* If "a >= 4" && "a < 5", then "a == 4",
3958	assuming a is of integral type. */
3959	{
3960	region_model_manager mgr;
3961	region_model model (&mgr);
3962	ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_4);
3963	ADD_SAT_CONSTRAINT (model, a, LT_EXPR, int_5);
3964	ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
3965	}
3966	/* If "a >= 4" && "a <= 4", then "a == 4". */
3967	{
3968	region_model_manager mgr;
3969	region_model model (&mgr);
3970	ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_4);
3971	ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
3972	ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
3973	}
3974	}
3975
3976	/* As above, but for floating-point:
3977	if "f > 3" && "f <= 4" we don't know that f == 4. */
3978	{
3979	tree f = build_global_decl (name: "f", double_type_node);
3980	tree float_3 = build_real_from_int_cst (double_type_node, int_3);
3981	tree float_4 = build_real_from_int_cst (double_type_node, int_4);
3982
3983	region_model_manager mgr;
3984	region_model model (&mgr);
3985	ADD_SAT_CONSTRAINT (model, f, GT_EXPR, float_3);
3986	ADD_SAT_CONSTRAINT (model, f, LE_EXPR, float_4);
3987	ASSERT_CONDITION_UNKNOWN (model, f, EQ_EXPR, float_4);
3988	ASSERT_CONDITION_UNKNOWN (model, f, EQ_EXPR, int_4);
3989	}
3990
3991	/* "a > 3 && a <= 3" should be impossible. */
3992	{
3993	region_model_manager mgr;
3994	region_model model (&mgr);
3995	ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
3996	ADD_UNSAT_CONSTRAINT (model, a, LE_EXPR, int_3);
3997	}
3998
3999	/* "(a + 1) > 3 && a < 3" should be impossible. */
4000	{
4001	region_model_manager mgr;
4002	{
4003	region_model model (&mgr);
4004	ADD_SAT_CONSTRAINT (model, a_plus_one, GT_EXPR, int_3);
4005	ADD_UNSAT_CONSTRAINT (model, a, LT_EXPR, int_3);
4006	}
4007	{
4008	region_model model (&mgr);
4009	ADD_SAT_CONSTRAINT (model, a, LT_EXPR, int_3);
4010	ADD_UNSAT_CONSTRAINT (model, a_plus_one, GT_EXPR, int_3);
4011	}
4012	}
4013
4014	/* "3 < a < 4" should be impossible for integer a. */
4015	{
4016	region_model_manager mgr;
4017	{
4018	region_model model (&mgr);
4019	ADD_SAT_CONSTRAINT (model, int_3, LT_EXPR, a);
4020	ADD_UNSAT_CONSTRAINT (model, a, LT_EXPR, int_4);
4021	}
4022	{
4023	region_model model (&mgr);
4024	ADD_SAT_CONSTRAINT (model, int_1, LT_EXPR, a);
4025	ADD_SAT_CONSTRAINT (model, int_3, LT_EXPR, a);
4026	ADD_SAT_CONSTRAINT (model, a, LT_EXPR, int_5);
4027	ADD_UNSAT_CONSTRAINT (model, a, LT_EXPR, int_4);
4028	}
4029	{
4030	region_model model (&mgr);
4031	ADD_SAT_CONSTRAINT (model, int_1, LT_EXPR, a);
4032	ADD_SAT_CONSTRAINT (model, a, LT_EXPR, int_5);
4033	ADD_SAT_CONSTRAINT (model, int_3, LT_EXPR, a);
4034	ADD_UNSAT_CONSTRAINT (model, a, LT_EXPR, int_4);
4035	}
4036	{
4037	region_model model (&mgr);
4038	ADD_SAT_CONSTRAINT (model, a, LT_EXPR, int_4);
4039	ADD_UNSAT_CONSTRAINT (model, int_3, LT_EXPR, a);
4040	}
4041	{
4042	region_model model (&mgr);
4043	ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
4044	ADD_UNSAT_CONSTRAINT (model, int_4, GT_EXPR, a);
4045	}
4046	{
4047	region_model model (&mgr);
4048	ADD_SAT_CONSTRAINT (model, int_4, GT_EXPR, a);
4049	ADD_UNSAT_CONSTRAINT (model, a, GT_EXPR, int_3);
4050	}
4051	}
4052	}
4053
4054	/* Verify various lower-level implementation details about
4055	constraint_manager. */
4056
4057	static void
4058	test_constraint_impl ()
4059	{
4060	tree int_42 = build_int_cst (integer_type_node, 42);
4061	tree int_0 = integer_zero_node;
4062
4063	tree x = build_global_decl (name: "x", integer_type_node);
4064	tree y = build_global_decl (name: "y", integer_type_node);
4065	tree z = build_global_decl (name: "z", integer_type_node);
4066
4067	/* x == y. */
4068	{
4069	region_model_manager mgr;
4070	region_model model (&mgr);
4071
4072	ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
4073
4074	/* Assert various things about the insides of model. */
4075	constraint_manager *cm = model.get_constraints ();
4076	ASSERT_EQ (cm->m_constraints.length (), 0);
4077	ASSERT_EQ (cm->m_equiv_classes.length (), 1);
4078	}
4079
4080	/* y <= z; x == y. */
4081	{
4082	region_model_manager mgr;
4083	region_model model (&mgr);
4084	ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
4085	ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
4086
4087	ADD_SAT_CONSTRAINT (model, y, GE_EXPR, z);
4088	ASSERT_CONDITION_TRUE (model, y, GE_EXPR, z);
4089	ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
4090
4091	ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
4092
4093	/* Assert various things about the insides of model. */
4094	constraint_manager *cm = model.get_constraints ();
4095	ASSERT_EQ (cm->m_constraints.length (), 1);
4096	ASSERT_EQ (cm->m_equiv_classes.length (), 2);
4097
4098	/* Ensure that we merged the constraints. */
4099	ASSERT_CONDITION_TRUE (model, x, GE_EXPR, z);
4100	}
4101
4102	/* y <= z; y == x. */
4103	{
4104	region_model_manager mgr;
4105	region_model model (&mgr);
4106	ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
4107	ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
4108
4109	ADD_SAT_CONSTRAINT (model, y, GE_EXPR, z);
4110	ASSERT_CONDITION_TRUE (model, y, GE_EXPR, z);
4111	ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
4112
4113	ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, x);
4114
4115	/* Assert various things about the insides of model. */
4116	constraint_manager *cm = model.get_constraints ();
4117	ASSERT_EQ (cm->m_constraints.length (), 1);
4118	ASSERT_EQ (cm->m_equiv_classes.length (), 2);
4119
4120	/* Ensure that we merged the constraints. */
4121	ASSERT_CONDITION_TRUE (model, x, GE_EXPR, z);
4122	}
4123
4124	/* x == 0, then x != 42. */
4125	{
4126	region_model_manager mgr;
4127	region_model model (&mgr);
4128
4129	ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
4130	ADD_SAT_CONSTRAINT (model, x, NE_EXPR, int_42);
4131
4132	/* Assert various things about the insides of model. */
4133	constraint_manager *cm = model.get_constraints ();
4134	ASSERT_EQ (cm->m_constraints.length (), 0);
4135	ASSERT_EQ (cm->m_equiv_classes.length (), 1);
4136	}
4137
4138	// TODO: selftest for merging ecs "in the middle"
4139	// where a non-final one gets overwritten
4140
4141	// TODO: selftest where there are pre-existing constraints
4142	}
4143
4144	/* Check that operator== and hashing works as expected for the
4145	various types. */
4146
4147	static void
4148	test_equality ()
4149	{
4150	tree x = build_global_decl (name: "x", integer_type_node);
4151	tree y = build_global_decl (name: "y", integer_type_node);
4152
4153	{
4154	region_model_manager mgr;
4155	region_model model0 (&mgr);
4156	region_model model1 (&mgr);
4157
4158	constraint_manager *cm0 = model0.get_constraints ();
4159	constraint_manager *cm1 = model1.get_constraints ();
4160
4161	ASSERT_EQ (cm0->hash (), cm1->hash ());
4162	ASSERT_EQ (*cm0, *cm1);
4163
4164	ASSERT_EQ (model0.hash (), model1.hash ());
4165	ASSERT_EQ (model0, model1);
4166
4167	ADD_SAT_CONSTRAINT (model1, x, EQ_EXPR, y);
4168	ASSERT_NE (cm0->hash (), cm1->hash ());
4169	ASSERT_NE (*cm0, *cm1);
4170
4171	ASSERT_NE (model0.hash (), model1.hash ());
4172	ASSERT_NE (model0, model1);
4173
4174	region_model model2 (&mgr);
4175	constraint_manager *cm2 = model2.get_constraints ();
4176	/* Make the same change to cm2. */
4177	ADD_SAT_CONSTRAINT (model2, x, EQ_EXPR, y);
4178	ASSERT_EQ (cm1->hash (), cm2->hash ());
4179	ASSERT_EQ (*cm1, *cm2);
4180
4181	ASSERT_EQ (model1.hash (), model2.hash ());
4182	ASSERT_EQ (model1, model2);
4183	}
4184	}
4185
4186	/* Verify tracking inequality of a variable against many constants. */
4187
4188	static void
4189	test_many_constants ()
4190	{
4191	region_model_manager mgr;
4192	program_point point (program_point::origin (mgr));
4193	tree a = build_global_decl (name: "a", integer_type_node);
4194
4195	region_model model (&mgr);
4196	auto_vec<tree> constants;
4197	for (int i = 0; i < 20; i++)
4198	{
4199	tree constant = build_int_cst (integer_type_node, i);
4200	constants.safe_push (obj: constant);
4201	ADD_SAT_CONSTRAINT (model, a, NE_EXPR, constant);
4202
4203	/* Merge, and check the result. */
4204	region_model other (model);
4205
4206	region_model merged (&mgr);
4207	ASSERT_TRUE (model.can_merge_with_p (other, point, &merged));
4208	model.canonicalize ();
4209	merged.canonicalize ();
4210	ASSERT_EQ (model, merged);
4211
4212	for (int j = 0; j <= i; j++)
4213	ASSERT_CONDITION_TRUE (model, a, NE_EXPR, constants[j]);
4214	}
4215	}
4216
4217	/* Verify that purging state relating to a variable doesn't leave stray
4218	equivalence classes (after canonicalization). */
4219
4220	static void
4221	test_purging (void)
4222	{
4223	tree int_0 = integer_zero_node;
4224	tree a = build_global_decl (name: "a", integer_type_node);
4225	tree b = build_global_decl (name: "b", integer_type_node);
4226
4227	/* "a != 0". */
4228	{
4229	region_model_manager mgr;
4230	region_model model (&mgr);
4231	ADD_SAT_CONSTRAINT (model, a, NE_EXPR, int_0);
4232	ASSERT_EQ (model.get_constraints ()->m_equiv_classes.length (), 2);
4233	ASSERT_EQ (model.get_constraints ()->m_constraints.length (), 1);
4234
4235	/* Purge state for "a". */
4236	const svalue *sval_a = model.get_rvalue (expr: a, NULL);
4237	model.purge_state_involving (sval: sval_a, NULL);
4238	model.canonicalize ();
4239	/* We should have an empty constraint_manager. */
4240	ASSERT_EQ (model.get_constraints ()->m_equiv_classes.length (), 0);
4241	ASSERT_EQ (model.get_constraints ()->m_constraints.length (), 0);
4242	}
4243
4244	/* "a != 0" && "b != 0". */
4245	{
4246	region_model_manager mgr;
4247	region_model model (&mgr);
4248	ADD_SAT_CONSTRAINT (model, a, NE_EXPR, int_0);
4249	ADD_SAT_CONSTRAINT (model, b, NE_EXPR, int_0);
4250	ASSERT_EQ (model.get_constraints ()->m_equiv_classes.length (), 3);
4251	ASSERT_EQ (model.get_constraints ()->m_constraints.length (), 2);
4252
4253	/* Purge state for "a". */
4254	const svalue *sval_a = model.get_rvalue (expr: a, NULL);
4255	model.purge_state_involving (sval: sval_a, NULL);
4256	model.canonicalize ();
4257	/* We should just have the constraint/ECs involving b != 0. */
4258	ASSERT_EQ (model.get_constraints ()->m_equiv_classes.length (), 2);
4259	ASSERT_EQ (model.get_constraints ()->m_constraints.length (), 1);
4260	ASSERT_CONDITION_TRUE (model, b, NE_EXPR, int_0);
4261	}
4262
4263	/* "a != 0" && "b == 0". */
4264	{
4265	region_model_manager mgr;
4266	region_model model (&mgr);
4267	ADD_SAT_CONSTRAINT (model, a, NE_EXPR, int_0);
4268	ADD_SAT_CONSTRAINT (model, b, EQ_EXPR, int_0);
4269	ASSERT_EQ (model.get_constraints ()->m_equiv_classes.length (), 2);
4270	ASSERT_EQ (model.get_constraints ()->m_constraints.length (), 1);
4271
4272	/* Purge state for "a". */
4273	const svalue *sval_a = model.get_rvalue (expr: a, NULL);
4274	model.purge_state_involving (sval: sval_a, NULL);
4275	model.canonicalize ();
4276	/* We should just have the EC involving b == 0. */
4277	ASSERT_EQ (model.get_constraints ()->m_equiv_classes.length (), 1);
4278	ASSERT_EQ (model.get_constraints ()->m_constraints.length (), 0);
4279	ASSERT_CONDITION_TRUE (model, b, EQ_EXPR, int_0);
4280	}
4281
4282	/* "a == 0". */
4283	{
4284	region_model_manager mgr;
4285	region_model model (&mgr);
4286	ADD_SAT_CONSTRAINT (model, a, EQ_EXPR, int_0);
4287	ASSERT_EQ (model.get_constraints ()->m_equiv_classes.length (), 1);
4288	ASSERT_EQ (model.get_constraints ()->m_constraints.length (), 0);
4289
4290	/* Purge state for "a". */
4291	const svalue *sval_a = model.get_rvalue (expr: a, NULL);
4292	model.purge_state_involving (sval: sval_a, NULL);
4293	model.canonicalize ();
4294	/* We should have an empty constraint_manager. */
4295	ASSERT_EQ (model.get_constraints ()->m_equiv_classes.length (), 0);
4296	ASSERT_EQ (model.get_constraints ()->m_constraints.length (), 0);
4297	}
4298
4299	/* "a == 0" && "b != 0". */
4300	{
4301	region_model_manager mgr;
4302	region_model model (&mgr);
4303	ADD_SAT_CONSTRAINT (model, a, EQ_EXPR, int_0);
4304	ADD_SAT_CONSTRAINT (model, b, NE_EXPR, int_0);
4305	ASSERT_EQ (model.get_constraints ()->m_equiv_classes.length (), 2);
4306	ASSERT_EQ (model.get_constraints ()->m_constraints.length (), 1);
4307
4308	/* Purge state for "a". */
4309	const svalue *sval_a = model.get_rvalue (expr: a, NULL);
4310	model.purge_state_involving (sval: sval_a, NULL);
4311	model.canonicalize ();
4312	/* We should just have the constraint/ECs involving b != 0. */
4313	ASSERT_EQ (model.get_constraints ()->m_equiv_classes.length (), 2);
4314	ASSERT_EQ (model.get_constraints ()->m_constraints.length (), 1);
4315	ASSERT_CONDITION_TRUE (model, b, NE_EXPR, int_0);
4316	}
4317
4318	/* "a == 0" && "b == 0". */
4319	{
4320	region_model_manager mgr;
4321	region_model model (&mgr);
4322	ADD_SAT_CONSTRAINT (model, a, EQ_EXPR, int_0);
4323	ADD_SAT_CONSTRAINT (model, b, EQ_EXPR, int_0);
4324	ASSERT_EQ (model.get_constraints ()->m_equiv_classes.length (), 1);
4325	ASSERT_EQ (model.get_constraints ()->m_constraints.length (), 0);
4326
4327	/* Purge state for "a". */
4328	const svalue *sval_a = model.get_rvalue (expr: a, NULL);
4329	model.purge_state_involving (sval: sval_a, NULL);
4330	model.canonicalize ();
4331	/* We should just have the EC involving b == 0. */
4332	ASSERT_EQ (model.get_constraints ()->m_equiv_classes.length (), 1);
4333	ASSERT_EQ (model.get_constraints ()->m_constraints.length (), 0);
4334	ASSERT_CONDITION_TRUE (model, b, EQ_EXPR, int_0);
4335	}
4336	}
4337
4338	/* Implementation detail of ASSERT_DUMP_BOUNDED_RANGES_EQ. */
4339
4340	static void
4341	assert_dump_bounded_range_eq (const location &loc,
4342	const bounded_range &range,
4343	const char *expected)
4344	{
4345	auto_fix_quotes sentinel;
4346	pretty_printer pp;
4347	pp_format_decoder (&pp) = default_tree_printer;
4348	range.dump_to_pp (pp: &pp, show_types: false);
4349	ASSERT_STREQ_AT (loc, pp_formatted_text (&pp), expected);
4350	}
4351
4352	/* Assert that BR.dump (false) is EXPECTED. */
4353
4354	#define ASSERT_DUMP_BOUNDED_RANGE_EQ(BR, EXPECTED) \
4355	SELFTEST_BEGIN_STMT \
4356	assert_dump_bounded_range_eq ((SELFTEST_LOCATION), (BR), (EXPECTED)); \
4357	SELFTEST_END_STMT
4358
4359	/* Verify that bounded_range works as expected. */
4360
4361	static void
4362	test_bounded_range ()
4363	{
4364	tree u8_0 = build_int_cst (unsigned_char_type_node, 0);
4365	tree u8_1 = build_int_cst (unsigned_char_type_node, 1);
4366	tree u8_64 = build_int_cst (unsigned_char_type_node, 64);
4367	tree u8_128 = build_int_cst (unsigned_char_type_node, 128);
4368	tree u8_255 = build_int_cst (unsigned_char_type_node, 255);
4369
4370	tree s8_0 = build_int_cst (signed_char_type_node, 0);
4371	tree s8_1 = build_int_cst (signed_char_type_node, 1);
4372	tree s8_2 = build_int_cst (signed_char_type_node, 2);
4373
4374	bounded_range br_u8_0 (u8_0, u8_0);
4375	ASSERT_DUMP_BOUNDED_RANGE_EQ (br_u8_0, "0");
4376	ASSERT_TRUE (br_u8_0.contains_p (u8_0));
4377	ASSERT_FALSE (br_u8_0.contains_p (u8_1));
4378	ASSERT_TRUE (br_u8_0.contains_p (s8_0));
4379	ASSERT_FALSE (br_u8_0.contains_p (s8_1));
4380
4381	bounded_range br_u8_0_1 (u8_0, u8_1);
4382	ASSERT_DUMP_BOUNDED_RANGE_EQ (br_u8_0_1, "[0, 1]");
4383
4384	bounded_range tmp (NULL_TREE, NULL_TREE);
4385	ASSERT_TRUE (br_u8_0.intersects_p (br_u8_0_1, &tmp));
4386	ASSERT_DUMP_BOUNDED_RANGE_EQ (tmp, "0");
4387
4388	bounded_range br_u8_64_128 (u8_64, u8_128);
4389	ASSERT_DUMP_BOUNDED_RANGE_EQ (br_u8_64_128, "[64, 128]");
4390
4391	ASSERT_FALSE (br_u8_0.intersects_p (br_u8_64_128, NULL));
4392	ASSERT_FALSE (br_u8_64_128.intersects_p (br_u8_0, NULL));
4393
4394	bounded_range br_u8_128_255 (u8_128, u8_255);
4395	ASSERT_DUMP_BOUNDED_RANGE_EQ (br_u8_128_255, "[128, 255]");
4396	ASSERT_TRUE (br_u8_128_255.intersects_p (br_u8_64_128, &tmp));
4397	ASSERT_DUMP_BOUNDED_RANGE_EQ (tmp, "128");
4398
4399	bounded_range br_s8_2 (s8_2, s8_2);
4400	ASSERT_DUMP_BOUNDED_RANGE_EQ (br_s8_2, "2");
4401	bounded_range br_s8_2_u8_255 (s8_2, u8_255);
4402	ASSERT_DUMP_BOUNDED_RANGE_EQ (br_s8_2_u8_255, "[2, 255]");
4403	}
4404
4405	/* Implementation detail of ASSERT_DUMP_BOUNDED_RANGES_EQ. */
4406
4407	static void
4408	assert_dump_bounded_ranges_eq (const location &loc,
4409	const bounded_ranges *ranges,
4410	const char *expected)
4411	{
4412	auto_fix_quotes sentinel;
4413	pretty_printer pp;
4414	pp_format_decoder (&pp) = default_tree_printer;
4415	ranges->dump_to_pp (pp: &pp, show_types: false);
4416	ASSERT_STREQ_AT (loc, pp_formatted_text (&pp), expected);
4417	}
4418
4419	/* Implementation detail of ASSERT_DUMP_BOUNDED_RANGES_EQ. */
4420
4421	static void
4422	assert_dump_bounded_ranges_eq (const location &loc,
4423	const bounded_ranges &ranges,
4424	const char *expected)
4425	{
4426	auto_fix_quotes sentinel;
4427	pretty_printer pp;
4428	pp_format_decoder (&pp) = default_tree_printer;
4429	ranges.dump_to_pp (pp: &pp, show_types: false);
4430	ASSERT_STREQ_AT (loc, pp_formatted_text (&pp), expected);
4431	}
4432
4433	/* Assert that BRS.dump (false) is EXPECTED. */
4434
4435	#define ASSERT_DUMP_BOUNDED_RANGES_EQ(BRS, EXPECTED) \
4436	SELFTEST_BEGIN_STMT \
4437	assert_dump_bounded_ranges_eq ((SELFTEST_LOCATION), (BRS), (EXPECTED)); \
4438	SELFTEST_END_STMT
4439
4440	/* Verify that the bounded_ranges class works as expected. */
4441
4442	static void
4443	test_bounded_ranges ()
4444	{
4445	bounded_ranges_manager mgr;
4446
4447	tree ch0 = build_int_cst (unsigned_char_type_node, 0);
4448	tree ch1 = build_int_cst (unsigned_char_type_node, 1);
4449	tree ch2 = build_int_cst (unsigned_char_type_node, 2);
4450	tree ch3 = build_int_cst (unsigned_char_type_node, 3);
4451	tree ch128 = build_int_cst (unsigned_char_type_node, 128);
4452	tree ch129 = build_int_cst (unsigned_char_type_node, 129);
4453	tree ch254 = build_int_cst (unsigned_char_type_node, 254);
4454	tree ch255 = build_int_cst (unsigned_char_type_node, 255);
4455
4456	const bounded_ranges *empty = mgr.get_or_create_empty ();
4457	ASSERT_DUMP_BOUNDED_RANGES_EQ (empty, "{}");
4458
4459	const bounded_ranges *point0 = mgr.get_or_create_point (cst: ch0);
4460	ASSERT_DUMP_BOUNDED_RANGES_EQ (point0, "{0}");
4461
4462	const bounded_ranges *point1 = mgr.get_or_create_point (cst: ch1);
4463	ASSERT_DUMP_BOUNDED_RANGES_EQ (point1, "{1}");
4464
4465	const bounded_ranges *point2 = mgr.get_or_create_point (cst: ch2);
4466	ASSERT_DUMP_BOUNDED_RANGES_EQ (point2, "{2}");
4467
4468	const bounded_ranges *range0_128 = mgr.get_or_create_range (lower_bound: ch0, upper_bound: ch128);
4469	ASSERT_DUMP_BOUNDED_RANGES_EQ (range0_128, "{[0, 128]}");
4470
4471	const bounded_ranges *range0_255 = mgr.get_or_create_range (lower_bound: ch0, upper_bound: ch255);
4472	ASSERT_DUMP_BOUNDED_RANGES_EQ (range0_255, "{[0, 255]}");
4473
4474	ASSERT_FALSE (empty->contain_p (ch0));
4475	ASSERT_FALSE (empty->contain_p (ch1));
4476	ASSERT_FALSE (empty->contain_p (ch255));
4477
4478	ASSERT_TRUE (point0->contain_p (ch0));
4479	ASSERT_FALSE (point0->contain_p (ch1));
4480	ASSERT_FALSE (point0->contain_p (ch255));
4481
4482	ASSERT_FALSE (point1->contain_p (ch0));
4483	ASSERT_TRUE (point1->contain_p (ch1));
4484	ASSERT_FALSE (point0->contain_p (ch255));
4485
4486	ASSERT_TRUE (range0_128->contain_p (ch0));
4487	ASSERT_TRUE (range0_128->contain_p (ch1));
4488	ASSERT_TRUE (range0_128->contain_p (ch128));
4489	ASSERT_FALSE (range0_128->contain_p (ch129));
4490	ASSERT_FALSE (range0_128->contain_p (ch254));
4491	ASSERT_FALSE (range0_128->contain_p (ch255));
4492
4493	const bounded_ranges *inv0_128
4494	= mgr.get_or_create_inverse (other: range0_128, unsigned_char_type_node);
4495	ASSERT_DUMP_BOUNDED_RANGES_EQ (inv0_128, "{[129, 255]}");
4496
4497	const bounded_ranges *range128_129 = mgr.get_or_create_range (lower_bound: ch128, upper_bound: ch129);
4498	ASSERT_DUMP_BOUNDED_RANGES_EQ (range128_129, "{[128, 129]}");
4499
4500	const bounded_ranges *inv128_129
4501	= mgr.get_or_create_inverse (other: range128_129, unsigned_char_type_node);
4502	ASSERT_DUMP_BOUNDED_RANGES_EQ (inv128_129, "{[0, 127], [130, 255]}");
4503
4504	/* Intersection. */
4505	{
4506	/* Intersection of disjoint ranges should be empty set. */
4507	const bounded_ranges *intersect0_1
4508	= mgr.get_or_create_intersection (a: point0, b: point1);
4509	ASSERT_DUMP_BOUNDED_RANGES_EQ (intersect0_1, "{}");
4510	}
4511
4512	/* Various tests of "union of ranges". */
4513	{
4514	{
4515	/* Touching points should be merged into a range. */
4516	auto_vec <const bounded_ranges *> v;
4517	v.safe_push (obj: point0);
4518	v.safe_push (obj: point1);
4519	const bounded_ranges *union_0_and_1 = mgr.get_or_create_union (others: v);
4520	ASSERT_DUMP_BOUNDED_RANGES_EQ (union_0_and_1, "{[0, 1]}");
4521	}
4522
4523	{
4524	/* Overlapping and out-of-order. */
4525	auto_vec <const bounded_ranges *> v;
4526	v.safe_push (obj: inv0_128); // {[129, 255]}
4527	v.safe_push (obj: range128_129);
4528	const bounded_ranges *union_129_255_and_128_129
4529	= mgr.get_or_create_union (others: v);
4530	ASSERT_DUMP_BOUNDED_RANGES_EQ (union_129_255_and_128_129, "{[128, 255]}");
4531	}
4532
4533	{
4534	/* Union of R and inverse(R) should be full range of type. */
4535	auto_vec <const bounded_ranges *> v;
4536	v.safe_push (obj: range128_129);
4537	v.safe_push (obj: inv128_129);
4538	const bounded_ranges *union_ = mgr.get_or_create_union (others: v);
4539	ASSERT_DUMP_BOUNDED_RANGES_EQ (union_, "{[0, 255]}");
4540	}
4541
4542	/* Union with an endpoint. */
4543	{
4544	const bounded_ranges *range2_to_255
4545	= mgr.get_or_create_range (lower_bound: ch2, upper_bound: ch255);
4546	ASSERT_DUMP_BOUNDED_RANGES_EQ (range2_to_255, "{[2, 255]}");
4547	auto_vec <const bounded_ranges *> v;
4548	v.safe_push (obj: point0);
4549	v.safe_push (obj: point2);
4550	v.safe_push (obj: range2_to_255);
4551	const bounded_ranges *union_ = mgr.get_or_create_union (others: v);
4552	ASSERT_DUMP_BOUNDED_RANGES_EQ (union_, "{0, [2, 255]}");
4553	}
4554
4555	/* Construct from vector of bounded_range. */
4556	{
4557	auto_vec<bounded_range> v;
4558	v.safe_push (obj: bounded_range (ch2, ch2));
4559	v.safe_push (obj: bounded_range (ch0, ch0));
4560	v.safe_push (obj: bounded_range (ch2, ch255));
4561	bounded_ranges br (v);
4562	ASSERT_DUMP_BOUNDED_RANGES_EQ (&br, "{0, [2, 255]}");
4563	}
4564	}
4565
4566	/* Various tests of "inverse". */
4567	{
4568	{
4569	const bounded_ranges *range_1_to_3 = mgr.get_or_create_range (lower_bound: ch1, upper_bound: ch3);
4570	ASSERT_DUMP_BOUNDED_RANGES_EQ (range_1_to_3, "{[1, 3]}");
4571	const bounded_ranges *inv
4572	= mgr.get_or_create_inverse (other: range_1_to_3, unsigned_char_type_node);
4573	ASSERT_DUMP_BOUNDED_RANGES_EQ (inv, "{0, [4, 255]}");
4574	}
4575	{
4576	const bounded_ranges *range_1_to_255
4577	= mgr.get_or_create_range (lower_bound: ch1, upper_bound: ch255);
4578	ASSERT_DUMP_BOUNDED_RANGES_EQ (range_1_to_255, "{[1, 255]}");
4579	const bounded_ranges *inv
4580	= mgr.get_or_create_inverse (other: range_1_to_255, unsigned_char_type_node);
4581	ASSERT_DUMP_BOUNDED_RANGES_EQ (inv, "{0}");
4582	}
4583	{
4584	const bounded_ranges *range_0_to_254
4585	= mgr.get_or_create_range (lower_bound: ch0, upper_bound: ch254);
4586	ASSERT_DUMP_BOUNDED_RANGES_EQ (range_0_to_254, "{[0, 254]}");
4587	const bounded_ranges *inv
4588	= mgr.get_or_create_inverse (other: range_0_to_254, unsigned_char_type_node);
4589	ASSERT_DUMP_BOUNDED_RANGES_EQ (inv, "{255}");
4590	}
4591	}
4592
4593	/* "case 'a'-'z': case 'A-Z':" vs "default:", for ASCII. */
4594	{
4595	tree ch65 = build_int_cst (unsigned_char_type_node, 65);
4596	tree ch90 = build_int_cst (unsigned_char_type_node, 90);
4597
4598	tree ch97 = build_int_cst (unsigned_char_type_node, 97);
4599	tree ch122 = build_int_cst (unsigned_char_type_node, 122);
4600
4601	const bounded_ranges *A_to_Z = mgr.get_or_create_range (lower_bound: ch65, upper_bound: ch90);
4602	ASSERT_DUMP_BOUNDED_RANGES_EQ (A_to_Z, "{[65, 90]}");
4603	const bounded_ranges *a_to_z = mgr.get_or_create_range (lower_bound: ch97, upper_bound: ch122);
4604	ASSERT_DUMP_BOUNDED_RANGES_EQ (a_to_z, "{[97, 122]}");
4605	auto_vec <const bounded_ranges *> v;
4606	v.safe_push (obj: A_to_Z);
4607	v.safe_push (obj: a_to_z);
4608	const bounded_ranges *label_ranges = mgr.get_or_create_union (others: v);
4609	ASSERT_DUMP_BOUNDED_RANGES_EQ (label_ranges, "{[65, 90], [97, 122]}");
4610	const bounded_ranges *default_ranges
4611	= mgr.get_or_create_inverse (other: label_ranges, unsigned_char_type_node);
4612	ASSERT_DUMP_BOUNDED_RANGES_EQ (default_ranges,
4613	"{[0, 64], [91, 96], [123, 255]}");
4614	}
4615
4616	/* Verify ranges from ops. */
4617	ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (EQ_EXPR, ch128),
4618	"{128}");
4619	ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (NE_EXPR, ch128),
4620	"{[0, 127], [129, 255]}");
4621	ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (LT_EXPR, ch128),
4622	"{[0, 127]}");
4623	ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (LE_EXPR, ch128),
4624	"{[0, 128]}");
4625	ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (GE_EXPR, ch128),
4626	"{[128, 255]}");
4627	ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (GT_EXPR, ch128),
4628	"{[129, 255]}");
4629	/* Ops at endpoints of type ranges. */
4630	ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (LE_EXPR, ch0),
4631	"{0}");
4632	ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (LT_EXPR, ch0),
4633	"{}");
4634	ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (NE_EXPR, ch0),
4635	"{[1, 255]}");
4636	ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (GE_EXPR, ch255),
4637	"{255}");
4638	ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (GT_EXPR, ch255),
4639	"{}");
4640	ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (NE_EXPR, ch255),
4641	"{[0, 254]}");
4642
4643	/* Verify that instances are consolidated by mgr. */
4644	ASSERT_EQ (mgr.get_or_create_point (ch0),
4645	mgr.get_or_create_point (ch0));
4646	ASSERT_NE (mgr.get_or_create_point (ch0),
4647	mgr.get_or_create_point (ch1));
4648	}
4649
4650	/* Verify that we can handle sufficiently simple bitmasking operations. */
4651
4652	static void
4653	test_bits (void)
4654	{
4655	region_model_manager mgr;
4656
4657	tree int_0 = integer_zero_node;
4658	tree int_0x80 = build_int_cst (integer_type_node, 0x80);
4659	tree int_0xff = build_int_cst (integer_type_node, 0xff);
4660	tree x = build_global_decl (name: "x", integer_type_node);
4661
4662	tree x_bit_and_0x80 = build2 (BIT_AND_EXPR, integer_type_node, x, int_0x80);
4663	tree x_bit_and_0xff = build2 (BIT_AND_EXPR, integer_type_node, x, int_0xff);
4664
4665	/* "x & 0x80 == 0x80". */
4666	{
4667	region_model model (&mgr);
4668	ADD_SAT_CONSTRAINT (model, x_bit_and_0x80, EQ_EXPR, int_0x80);
4669	ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, int_0);
4670	ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, int_0x80);
4671	}
4672
4673	/* "x & 0x80 != 0x80". */
4674	{
4675	region_model model (&mgr);
4676	ADD_SAT_CONSTRAINT (model, x_bit_and_0x80, NE_EXPR, int_0x80);
4677	ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, int_0);
4678	ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, int_0x80);
4679	}
4680
4681	/* "x & 0x80 == 0". */
4682	{
4683	region_model model (&mgr);
4684
4685	ADD_SAT_CONSTRAINT (model, x_bit_and_0x80, EQ_EXPR, int_0);
4686	ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, int_0);
4687	ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, int_0x80);
4688	}
4689
4690	/* "x & 0x80 != 0". */
4691	{
4692	region_model model (&mgr);
4693	ADD_SAT_CONSTRAINT (model, x_bit_and_0x80, NE_EXPR, int_0);
4694	ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, int_0);
4695	ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, int_0x80);
4696	}
4697
4698	/* More that one bit in the mask. */
4699
4700	/* "x & 0xff == 0x80". */
4701	{
4702	region_model model (&mgr);
4703	ADD_SAT_CONSTRAINT (model, x_bit_and_0xff, EQ_EXPR, int_0x80);
4704	ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, int_0);
4705	ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, int_0x80);
4706	ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, int_0xff);
4707	}
4708
4709	/* "x & 0xff != 0x80". */
4710	{
4711	region_model model (&mgr);
4712	ADD_SAT_CONSTRAINT (model, x_bit_and_0xff, NE_EXPR, int_0x80);
4713	ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, int_0);
4714	ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, int_0x80);
4715	ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, int_0xff);
4716	}
4717
4718	/* "x & 0xff == 0". */
4719	{
4720	region_model model (&mgr);
4721
4722	ADD_SAT_CONSTRAINT (model, x_bit_and_0xff, EQ_EXPR, int_0);
4723	ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, int_0);
4724	ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, int_0x80);
4725	ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, int_0xff);
4726	}
4727
4728	/* "x & 0xff != 0". */
4729	{
4730	region_model model (&mgr);
4731	ADD_SAT_CONSTRAINT (model, x_bit_and_0xff, NE_EXPR, int_0);
4732	ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, int_0);
4733	ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, int_0x80);
4734	ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, int_0xff);
4735	}
4736	}
4737
4738	/* Run the selftests in this file, temporarily overriding
4739	flag_analyzer_transitivity with TRANSITIVITY. */
4740
4741	static void
4742	run_constraint_manager_tests (bool transitivity)
4743	{
4744	int saved_flag_analyzer_transitivity = flag_analyzer_transitivity;
4745	flag_analyzer_transitivity = transitivity;
4746
4747	test_range ();
4748	test_constraint_conditions ();
4749	if (flag_analyzer_transitivity)
4750	{
4751	/* These selftests assume transitivity. */
4752	test_transitivity ();
4753	}
4754	test_constant_comparisons ();
4755	test_constraint_impl ();
4756	test_equality ();
4757	test_many_constants ();
4758	test_purging ();
4759	test_bounded_range ();
4760	test_bounded_ranges ();
4761	test_bits ();
4762
4763	flag_analyzer_transitivity = saved_flag_analyzer_transitivity;
4764	}
4765
4766	/* Run all of the selftests within this file. */
4767
4768	void
4769	analyzer_constraint_manager_cc_tests ()
4770	{
4771	/* Run the tests twice: with and without transitivity. */
4772	run_constraint_manager_tests (transitivity: true);
4773	run_constraint_manager_tests (transitivity: false);
4774	}
4775
4776	} // namespace selftest
4777
4778	#endif /* CHECKING_P */
4779
4780	} // namespace ana
4781
4782	#endif /* #if ENABLE_ANALYZER */
4783