1 /* Tracking equivalence classes and constraints at a point on an execution path.
2 Copyright (C) 2019-2023 Free Software Foundation, Inc.
3 Contributed by David Malcolm <dmalcolm@redhat.com>.
5 This file is part of GCC.
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)
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.
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/>. */
22 #define INCLUDE_MEMORY
24 #include "coretypes.h"
27 #include "basic-block.h"
29 #include "gimple-iterator.h"
30 #include "fold-const.h"
32 #include "diagnostic-core.h"
34 #include "analyzer/analyzer.h"
35 #include "ordered-hash-map.h"
40 #include "analyzer/supergraph.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"
58 compare_constants (tree lhs_const
, enum tree_code op
, tree rhs_const
)
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
);
69 /* Return true iff CST is below the maximum value for its type. */
72 can_plus_one_p (tree cst
)
74 gcc_assert (CONSTANT_CLASS_P (cst
));
75 return tree_int_cst_lt (cst
, TYPE_MAX_VALUE (TREE_TYPE (cst
)));
78 /* Return (CST + 1). */
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
));
91 /* Return true iff CST is above the minimum value for its type. */
94 can_minus_one_p (tree cst
)
96 gcc_assert (CONSTANT_CLASS_P (cst
));
97 return tree_int_cst_lt (TYPE_MIN_VALUE (TREE_TYPE (cst
)), cst
);
100 /* Return (CST - 1). */
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
));
115 /* Ensure that this bound is closed by converting an open bound to a
119 bound::ensure_closed (enum bound_kind bound_kind
)
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 m_constant
= fold_build2 (bound_kind
== BK_UPPER
? MINUS_EXPR
: PLUS_EXPR
,
128 TREE_TYPE (m_constant
),
129 m_constant
, integer_one_node
);
130 gcc_assert (CONSTANT_CLASS_P (m_constant
));
135 /* Get "<=" vs "<" for this bound. */
138 bound::get_relation_as_str () const
148 /* Dump this range to PP, which must support %E for tree. */
151 range::dump_to_pp (pretty_printer
*pp
) const
153 if (m_lower_bound
.m_constant
)
155 if (m_upper_bound
.m_constant
)
156 pp_printf (pp
, "%qE %s x %s %qE",
157 m_lower_bound
.m_constant
,
158 m_lower_bound
.get_relation_as_str (),
159 m_upper_bound
.get_relation_as_str (),
160 m_upper_bound
.m_constant
);
162 pp_printf (pp
, "%qE %s x",
163 m_lower_bound
.m_constant
,
164 m_lower_bound
.get_relation_as_str ());
168 if (m_upper_bound
.m_constant
)
169 pp_printf (pp
, "x %s %qE",
170 m_upper_bound
.get_relation_as_str (),
171 m_upper_bound
.m_constant
);
177 /* Dump this range to stderr. */
183 pp_format_decoder (&pp
) = default_tree_printer
;
184 pp_show_color (&pp
) = pp_show_color (global_dc
->printer
);
185 pp
.buffer
->stream
= stderr
;
191 /* Determine if there is only one possible value for this range.
192 If so, return the constant; otherwise, return NULL_TREE. */
195 range::constrained_to_single_element ()
197 if (m_lower_bound
.m_constant
== NULL_TREE
198 || m_upper_bound
.m_constant
== NULL_TREE
)
201 if (!INTEGRAL_TYPE_P (TREE_TYPE (m_lower_bound
.m_constant
)))
203 if (!INTEGRAL_TYPE_P (TREE_TYPE (m_upper_bound
.m_constant
)))
206 /* Convert any open bounds to closed bounds. */
207 m_lower_bound
.ensure_closed (BK_LOWER
);
208 m_upper_bound
.ensure_closed (BK_UPPER
);
211 tree comparison
= fold_binary (EQ_EXPR
, boolean_type_node
,
212 m_lower_bound
.m_constant
,
213 m_upper_bound
.m_constant
);
214 if (comparison
== boolean_true_node
)
215 return m_lower_bound
.m_constant
;
220 /* Eval the condition "X OP RHS_CONST" for X within the range. */
223 range::eval_condition (enum tree_code op
, tree rhs_const
) const
226 if (tree single_element
= copy
.constrained_to_single_element ())
227 return compare_constants (single_element
, op
, rhs_const
);
232 if (below_lower_bound (rhs_const
))
233 return tristate (tristate::TS_FALSE
);
234 if (above_upper_bound (rhs_const
))
235 return tristate (tristate::TS_FALSE
);
240 /* Qn: "X </<= RHS_CONST". */
241 /* If RHS_CONST > upper bound, then it's true.
242 If RHS_CONST < lower bound, then it's false.
243 Otherwise unknown. */
244 if (above_upper_bound (rhs_const
))
245 return tristate (tristate::TS_TRUE
);
246 if (below_lower_bound (rhs_const
))
247 return tristate (tristate::TS_FALSE
);
251 /* Qn: "X != RHS_CONST". */
252 /* If RHS_CONST < lower bound, then it's true.
253 If RHS_CONST > upper bound, then it's false.
254 Otherwise unknown. */
255 if (below_lower_bound (rhs_const
))
256 return tristate (tristate::TS_TRUE
);
257 if (above_upper_bound (rhs_const
))
258 return tristate (tristate::TS_TRUE
);
263 /* Qn: "X >=/> RHS_CONST". */
264 if (above_upper_bound (rhs_const
))
265 return tristate (tristate::TS_FALSE
);
266 if (below_lower_bound (rhs_const
))
267 return tristate (tristate::TS_TRUE
);
274 return tristate (tristate::TS_UNKNOWN
);
277 /* Return true if RHS_CONST is below the lower bound of this range. */
280 range::below_lower_bound (tree rhs_const
) const
282 if (!m_lower_bound
.m_constant
)
285 return compare_constants (rhs_const
,
286 m_lower_bound
.m_closed
? LT_EXPR
: LE_EXPR
,
287 m_lower_bound
.m_constant
).is_true ();
290 /* Return true if RHS_CONST is above the upper bound of this range. */
293 range::above_upper_bound (tree rhs_const
) const
295 if (!m_upper_bound
.m_constant
)
298 return compare_constants (rhs_const
,
299 m_upper_bound
.m_closed
? GT_EXPR
: GE_EXPR
,
300 m_upper_bound
.m_constant
).is_true ();
303 /* Attempt to add B to the bound of the given kind of this range.
304 Return true if feasible; false if infeasible. */
307 range::add_bound (bound b
, enum bound_kind bound_kind
)
309 b
.ensure_closed (bound_kind
);
316 /* Discard redundant bounds. */
317 if (m_lower_bound
.m_constant
)
319 m_lower_bound
.ensure_closed (BK_LOWER
);
320 if (tree_int_cst_le (b
.m_constant
,
321 m_lower_bound
.m_constant
))
324 if (m_upper_bound
.m_constant
)
326 m_upper_bound
.ensure_closed (BK_UPPER
);
327 /* Reject B <= V <= UPPER when B > UPPER. */
328 if (!tree_int_cst_le (b
.m_constant
,
329 m_upper_bound
.m_constant
))
336 /* Discard redundant bounds. */
337 if (m_upper_bound
.m_constant
)
339 m_upper_bound
.ensure_closed (BK_UPPER
);
340 if (!tree_int_cst_lt (b
.m_constant
,
341 m_upper_bound
.m_constant
))
344 if (m_lower_bound
.m_constant
)
346 m_lower_bound
.ensure_closed (BK_LOWER
);
347 /* Reject LOWER <= V <= B when LOWER > B. */
348 if (!tree_int_cst_le (m_lower_bound
.m_constant
,
359 /* Attempt to add (RANGE OP RHS_CONST) as a bound to this range.
360 Return true if feasible; false if infeasible. */
363 range::add_bound (enum tree_code op
, tree rhs_const
)
370 /* "V < RHS_CONST" */
371 return add_bound (bound (rhs_const
, false), BK_UPPER
);
373 /* "V <= RHS_CONST" */
374 return add_bound (bound (rhs_const
, true), BK_UPPER
);
376 /* "V >= RHS_CONST" */
377 return add_bound (bound (rhs_const
, true), BK_LOWER
);
379 /* "V > RHS_CONST" */
380 return add_bound (bound (rhs_const
, false), BK_LOWER
);
384 /* struct bounded_range. */
386 bounded_range::bounded_range (const_tree lower
, const_tree upper
)
387 : m_lower (const_cast<tree
> (lower
)),
388 m_upper (const_cast<tree
> (upper
))
392 gcc_assert (TREE_CODE (m_lower
) == INTEGER_CST
);
393 gcc_assert (TREE_CODE (m_upper
) == INTEGER_CST
);
394 /* We should have lower <= upper. */
395 gcc_assert (!tree_int_cst_lt (m_upper
, m_lower
));
399 /* Purely for pending on-stack values, for
401 gcc_assert (m_lower
== NULL_TREE
);
402 gcc_assert (m_lower
== NULL_TREE
);
407 dump_cst (pretty_printer
*pp
, tree cst
, bool show_types
)
412 pp_character (pp
, '(');
413 dump_generic_node (pp
, TREE_TYPE (cst
), 0, (dump_flags_t
)0, false);
414 pp_character (pp
, ')');
416 dump_generic_node (pp
, cst
, 0, (dump_flags_t
)0, false);
419 /* Dump this object to PP. */
422 bounded_range::dump_to_pp (pretty_printer
*pp
, bool show_types
) const
425 dump_cst (pp
, m_lower
, show_types
);
428 pp_character (pp
, '[');
429 dump_cst (pp
, m_lower
, show_types
);
430 pp_string (pp
, ", ");
431 dump_cst (pp
, m_upper
, show_types
);
432 pp_character (pp
, ']');
436 /* Dump this object to stderr. */
439 bounded_range::dump (bool show_types
) const
442 pp_format_decoder (&pp
) = default_tree_printer
;
443 pp_show_color (&pp
) = pp_show_color (global_dc
->printer
);
444 pp
.buffer
->stream
= stderr
;
445 dump_to_pp (&pp
, show_types
);
451 bounded_range::to_json () const
453 json::object
*range_obj
= new json::object ();
454 set_json_attr (range_obj
, "lower", m_lower
);
455 set_json_attr (range_obj
, "upper", m_upper
);
459 /* Subroutine of bounded_range::to_json. */
462 bounded_range::set_json_attr (json::object
*obj
, const char *name
, tree value
)
465 pp_format_decoder (&pp
) = default_tree_printer
;
466 pp_printf (&pp
, "%E", value
);
467 obj
->set (name
, new json::string (pp_formatted_text (&pp
)));
471 /* Return true iff CST is within this range. */
474 bounded_range::contains_p (tree cst
) const
476 /* Reject if below lower bound. */
477 if (tree_int_cst_lt (cst
, m_lower
))
479 /* Reject if above lower bound. */
480 if (tree_int_cst_lt (m_upper
, cst
))
485 /* If this range intersects OTHER, return true, writing
486 the intersection to *OUT if OUT is non-NULL.
487 Return false if they do not intersect. */
490 bounded_range::intersects_p (const bounded_range
&other
,
491 bounded_range
*out
) const
494 = (tree_int_cst_le (m_lower
, other
.m_lower
)
495 ? other
.m_lower
: m_lower
);
496 gcc_assert (TREE_CODE (max_lower
) == INTEGER_CST
);
498 = (tree_int_cst_le (m_upper
, other
.m_upper
)
499 ? m_upper
: other
.m_upper
);
500 gcc_assert (TREE_CODE (min_upper
) == INTEGER_CST
);
502 if (tree_int_cst_le (max_lower
, min_upper
))
505 *out
= bounded_range (max_lower
, min_upper
);
513 bounded_range::operator== (const bounded_range
&other
) const
515 return (TREE_TYPE (m_lower
) == TREE_TYPE (other
.m_lower
)
516 && TREE_TYPE (m_upper
) == TREE_TYPE (other
.m_upper
)
517 && tree_int_cst_equal (m_lower
, other
.m_lower
)
518 && tree_int_cst_equal (m_upper
, other
.m_upper
));
522 bounded_range::cmp (const bounded_range
&br1
, const bounded_range
&br2
)
524 if (int cmp_lower
= tree_int_cst_compare (br1
.m_lower
,
527 return tree_int_cst_compare (br1
.m_upper
, br2
.m_upper
);
530 /* struct bounded_ranges. */
532 /* Construct a bounded_ranges instance from a single range. */
534 bounded_ranges::bounded_ranges (const bounded_range
&range
)
537 m_ranges
.quick_push (range
);
542 /* Construct a bounded_ranges instance from multiple ranges. */
544 bounded_ranges::bounded_ranges (const vec
<bounded_range
> &ranges
)
545 : m_ranges (ranges
.length ())
547 m_ranges
.safe_splice (ranges
);
552 /* Construct a bounded_ranges instance for values of LHS for which
553 (LHS OP RHS_CONST) is true (e.g. "(LHS > 3)". */
555 bounded_ranges::bounded_ranges (enum tree_code op
, tree rhs_const
)
558 gcc_assert (TREE_CODE (rhs_const
) == INTEGER_CST
);
559 tree type
= TREE_TYPE (rhs_const
);
565 m_ranges
.safe_push (bounded_range (rhs_const
, rhs_const
));
569 m_ranges
.safe_push (bounded_range (rhs_const
, TYPE_MAX_VALUE (type
)));
573 m_ranges
.safe_push (bounded_range (TYPE_MIN_VALUE (type
), rhs_const
));
577 if (tree_int_cst_lt (TYPE_MIN_VALUE (type
), rhs_const
))
578 m_ranges
.safe_push (bounded_range (TYPE_MIN_VALUE (type
),
579 minus_one (rhs_const
)));
580 if (tree_int_cst_lt (rhs_const
, TYPE_MAX_VALUE (type
)))
581 m_ranges
.safe_push (bounded_range (plus_one (rhs_const
),
582 TYPE_MAX_VALUE (type
)));
585 if (tree_int_cst_lt (rhs_const
, TYPE_MAX_VALUE (type
)))
586 m_ranges
.safe_push (bounded_range (plus_one (rhs_const
),
587 TYPE_MAX_VALUE (type
)));
590 if (tree_int_cst_lt (TYPE_MIN_VALUE (type
), rhs_const
))
591 m_ranges
.safe_push (bounded_range (TYPE_MIN_VALUE (type
),
592 minus_one (rhs_const
)));
599 /* Subroutine of ctors for fixing up m_ranges.
600 Also, initialize m_hash. */
603 bounded_ranges::canonicalize ()
605 /* Sort the ranges. */
606 m_ranges
.qsort ([](const void *p1
, const void *p2
) -> int
608 const bounded_range
&br1
= *(const bounded_range
*)p1
;
609 const bounded_range
&br2
= *(const bounded_range
*)p2
;
610 return bounded_range::cmp (br1
, br2
);
613 /* Merge ranges that are touching or overlapping. */
614 for (unsigned i
= 1; i
< m_ranges
.length (); )
616 bounded_range
*prev
= &m_ranges
[i
- 1];
617 const bounded_range
*next
= &m_ranges
[i
];
618 if (prev
->intersects_p (*next
, NULL
)
619 || (can_plus_one_p (prev
->m_upper
)
620 && tree_int_cst_equal (plus_one (prev
->m_upper
),
623 prev
->m_upper
= next
->m_upper
;
624 m_ranges
.ordered_remove (i
);
630 /* Initialize m_hash. */
631 inchash::hash
hstate (0);
632 for (const auto &iter
: m_ranges
)
634 inchash::add_expr (iter
.m_lower
, hstate
);
635 inchash::add_expr (iter
.m_upper
, hstate
);
637 m_hash
= hstate
.end ();
640 /* Assert that this object is valid. */
643 bounded_ranges::validate () const
645 /* Skip this in a release build. */
650 for (unsigned i
= 1; i
< m_ranges
.length (); i
++)
652 const bounded_range
&prev
= m_ranges
[i
- 1];
653 const bounded_range
&next
= m_ranges
[i
];
655 /* Give up if we somehow have incompatible different types. */
656 if (!types_compatible_p (TREE_TYPE (prev
.m_upper
),
657 TREE_TYPE (next
.m_lower
)))
661 gcc_assert (tree_int_cst_lt (prev
.m_upper
, next
.m_lower
));
663 gcc_assert (can_plus_one_p (prev
.m_upper
));
664 /* otherwise there's no room for "next". */
666 /* Verify no ranges touch each other. */
667 gcc_assert (tree_int_cst_lt (plus_one (prev
.m_upper
), next
.m_lower
));
671 /* bounded_ranges equality operator. */
674 bounded_ranges::operator== (const bounded_ranges
&other
) const
676 if (m_ranges
.length () != other
.m_ranges
.length ())
678 for (unsigned i
= 0; i
< m_ranges
.length (); i
++)
680 if (m_ranges
[i
] != other
.m_ranges
[i
])
686 /* Dump this object to PP. */
689 bounded_ranges::dump_to_pp (pretty_printer
*pp
, bool show_types
) const
691 pp_character (pp
, '{');
692 for (unsigned i
= 0; i
< m_ranges
.length (); ++i
)
695 pp_string (pp
, ", ");
696 m_ranges
[i
].dump_to_pp (pp
, show_types
);
698 pp_character (pp
, '}');
701 /* Dump this object to stderr. */
704 bounded_ranges::dump (bool show_types
) const
707 pp_format_decoder (&pp
) = default_tree_printer
;
708 pp_show_color (&pp
) = pp_show_color (global_dc
->printer
);
709 pp
.buffer
->stream
= stderr
;
710 dump_to_pp (&pp
, show_types
);
716 bounded_ranges::to_json () const
718 json::array
*arr_obj
= new json::array ();
720 for (unsigned i
= 0; i
< m_ranges
.length (); ++i
)
721 arr_obj
->append (m_ranges
[i
].to_json ());
726 /* Determine whether (X OP RHS_CONST) is known to be true or false
727 for all X in the ranges expressed by this object. */
730 bounded_ranges::eval_condition (enum tree_code op
,
732 bounded_ranges_manager
*mgr
) const
734 /* Convert (X OP RHS_CONST) to a bounded_ranges instance and find
735 the intersection of that with this object. */
736 bounded_ranges
other (op
, rhs_const
);
737 const bounded_ranges
*intersection
738 = mgr
->get_or_create_intersection (this, &other
);
740 if (intersection
->m_ranges
.length () > 0)
742 /* We can use pointer equality to check for equality,
743 due to instance consolidation. */
744 if (intersection
== this)
745 return tristate (tristate::TS_TRUE
);
747 return tristate (tristate::TS_UNKNOWN
);
750 /* No intersection. */
751 return tristate (tristate::TS_FALSE
);
754 /* Return true if CST is within any of the ranges. */
757 bounded_ranges::contain_p (tree cst
) const
759 gcc_assert (TREE_CODE (cst
) == INTEGER_CST
);
760 for (const auto &iter
: m_ranges
)
762 /* TODO: should we optimize this based on sorting? */
763 if (iter
.contains_p (cst
))
770 bounded_ranges::cmp (const bounded_ranges
*a
, const bounded_ranges
*b
)
772 if (int cmp_length
= ((int)a
->m_ranges
.length ()
773 - (int)b
->m_ranges
.length ()))
775 for (unsigned i
= 0; i
< a
->m_ranges
.length (); i
++)
777 if (int cmp_range
= bounded_range::cmp (a
->m_ranges
[i
], b
->m_ranges
[i
]))
780 /* They are equal. They ought to have been consolidated, so we should
781 have two pointers to the same object. */
786 /* class bounded_ranges_manager. */
788 /* bounded_ranges_manager's dtor. */
790 bounded_ranges_manager::~bounded_ranges_manager ()
792 /* Delete the managed objects. */
793 for (const auto &iter
: m_map
)
797 /* Get the bounded_ranges instance for the empty set, creating it if
800 const bounded_ranges
*
801 bounded_ranges_manager::get_or_create_empty ()
803 auto_vec
<bounded_range
> empty_vec
;
805 return consolidate (new bounded_ranges (empty_vec
));
808 /* Get the bounded_ranges instance for {CST}, creating it if necessary. */
810 const bounded_ranges
*
811 bounded_ranges_manager::get_or_create_point (const_tree cst
)
813 gcc_assert (TREE_CODE (cst
) == INTEGER_CST
);
815 return get_or_create_range (cst
, cst
);
818 /* Get the bounded_ranges instance for {[LOWER_BOUND..UPPER_BOUND]},
819 creating it if necessary. */
821 const bounded_ranges
*
822 bounded_ranges_manager::get_or_create_range (const_tree lower_bound
,
823 const_tree upper_bound
)
825 gcc_assert (TREE_CODE (lower_bound
) == INTEGER_CST
);
826 gcc_assert (TREE_CODE (upper_bound
) == INTEGER_CST
);
829 (new bounded_ranges (bounded_range (lower_bound
, upper_bound
)));
832 /* Get the bounded_ranges instance for the union of OTHERS,
833 creating it if necessary. */
835 const bounded_ranges
*
836 bounded_ranges_manager::
837 get_or_create_union (const vec
<const bounded_ranges
*> &others
)
839 auto_vec
<bounded_range
> ranges
;
840 for (const auto &r
: others
)
841 ranges
.safe_splice (r
->m_ranges
);
842 return consolidate (new bounded_ranges (ranges
));
845 /* Get the bounded_ranges instance for the intersection of A and B,
846 creating it if necessary. */
848 const bounded_ranges
*
849 bounded_ranges_manager::get_or_create_intersection (const bounded_ranges
*a
,
850 const bounded_ranges
*b
)
852 auto_vec
<bounded_range
> ranges
;
855 while (a_idx
< a
->m_ranges
.length ()
856 && b_idx
< b
->m_ranges
.length ())
858 const bounded_range
&r_a
= a
->m_ranges
[a_idx
];
859 const bounded_range
&r_b
= b
->m_ranges
[b_idx
];
861 bounded_range
intersection (NULL_TREE
, NULL_TREE
);
862 if (r_a
.intersects_p (r_b
, &intersection
))
864 ranges
.safe_push (intersection
);
866 if (tree_int_cst_lt (r_a
.m_lower
, r_b
.m_lower
))
872 if (tree_int_cst_lt (r_a
.m_upper
, r_b
.m_upper
))
879 return consolidate (new bounded_ranges (ranges
));
882 /* Get the bounded_ranges instance for the inverse of OTHER relative
883 to TYPE, creating it if necessary.
884 This is for use when handling "default" in switch statements, where
885 OTHER represents all the other cases. */
887 const bounded_ranges
*
888 bounded_ranges_manager::get_or_create_inverse (const bounded_ranges
*other
,
891 tree min_val
= TYPE_MIN_VALUE (type
);
892 tree max_val
= TYPE_MAX_VALUE (type
);
893 if (other
->m_ranges
.length () == 0)
894 return get_or_create_range (min_val
, max_val
);
895 auto_vec
<bounded_range
> ranges
;
896 tree first_lb
= other
->m_ranges
[0].m_lower
;
897 if (tree_int_cst_lt (min_val
, first_lb
)
898 && can_minus_one_p (first_lb
))
899 ranges
.safe_push (bounded_range (min_val
,
900 minus_one (first_lb
)));
901 for (unsigned i
= 1; i
< other
->m_ranges
.length (); i
++)
903 tree prev_ub
= other
->m_ranges
[i
- 1].m_upper
;
904 tree iter_lb
= other
->m_ranges
[i
].m_lower
;
905 gcc_assert (tree_int_cst_lt (prev_ub
, iter_lb
));
906 if (can_plus_one_p (prev_ub
) && can_minus_one_p (iter_lb
))
907 ranges
.safe_push (bounded_range (plus_one (prev_ub
),
908 minus_one (iter_lb
)));
911 = other
->m_ranges
[other
->m_ranges
.length () - 1].m_upper
;
912 if (tree_int_cst_lt (last_ub
, max_val
)
913 && can_plus_one_p (last_ub
))
914 ranges
.safe_push (bounded_range (plus_one (last_ub
), max_val
));
916 return consolidate (new bounded_ranges (ranges
));
919 /* If an object equal to INST is already present, delete INST and
920 return the existing object.
921 Otherwise add INST and return it. */
923 const bounded_ranges
*
924 bounded_ranges_manager::consolidate (bounded_ranges
*inst
)
926 if (bounded_ranges
**slot
= m_map
.get (inst
))
931 m_map
.put (inst
, inst
);
935 /* Get the bounded_ranges instance for EDGE of SWITCH_STMT,
936 creating it if necessary, and caching it by edge. */
938 const bounded_ranges
*
939 bounded_ranges_manager::
940 get_or_create_ranges_for_switch (const switch_cfg_superedge
*edge
,
941 const gswitch
*switch_stmt
)
943 /* Look in per-edge cache. */
944 if (const bounded_ranges
** slot
= m_edge_cache
.get (edge
))
947 /* Not yet in cache. */
948 const bounded_ranges
*all_cases_ranges
949 = create_ranges_for_switch (*edge
, switch_stmt
);
950 m_edge_cache
.put (edge
, all_cases_ranges
);
951 return all_cases_ranges
;
954 /* Get the bounded_ranges instance for EDGE of SWITCH_STMT,
955 creating it if necessary, for edges for which the per-edge
956 cache has not yet been populated. */
958 const bounded_ranges
*
959 bounded_ranges_manager::
960 create_ranges_for_switch (const switch_cfg_superedge
&edge
,
961 const gswitch
*switch_stmt
)
963 /* Get the ranges for each case label. */
964 auto_vec
<const bounded_ranges
*> case_ranges_vec
965 (gimple_switch_num_labels (switch_stmt
));
967 for (tree case_label
: edge
.get_case_labels ())
969 /* Get the ranges for this case label. */
970 const bounded_ranges
*case_ranges
971 = make_case_label_ranges (switch_stmt
, case_label
);
972 case_ranges_vec
.quick_push (case_ranges
);
975 /* Combine all the ranges for each case label into a single collection
977 const bounded_ranges
*all_cases_ranges
978 = get_or_create_union (case_ranges_vec
);
979 return all_cases_ranges
;
982 /* Get the bounded_ranges instance for CASE_LABEL within
985 const bounded_ranges
*
986 bounded_ranges_manager::
987 make_case_label_ranges (const gswitch
*switch_stmt
,
990 gcc_assert (TREE_CODE (case_label
) == CASE_LABEL_EXPR
);
991 tree lower_bound
= CASE_LOW (case_label
);
992 tree upper_bound
= CASE_HIGH (case_label
);
997 return get_or_create_range (lower_bound
, upper_bound
);
1000 return get_or_create_point (lower_bound
);
1004 /* The default case.
1005 Add exclusions based on the other cases. */
1006 auto_vec
<const bounded_ranges
*> other_case_ranges
1007 (gimple_switch_num_labels (switch_stmt
));
1008 for (unsigned other_idx
= 1;
1009 other_idx
< gimple_switch_num_labels (switch_stmt
);
1012 tree other_label
= gimple_switch_label (switch_stmt
,
1014 const bounded_ranges
*other_ranges
1015 = make_case_label_ranges (switch_stmt
, other_label
);
1016 other_case_ranges
.quick_push (other_ranges
);
1018 const bounded_ranges
*other_cases_ranges
1019 = get_or_create_union (other_case_ranges
);
1020 tree type
= TREE_TYPE (gimple_switch_index (switch_stmt
));
1021 return get_or_create_inverse (other_cases_ranges
, type
);
1025 /* Dump the number of objects of each class that were managed by this
1027 If SHOW_OBJS is true, also dump the objects themselves. */
1030 bounded_ranges_manager::log_stats (logger
*logger
, bool show_objs
) const
1033 logger
->log (" # %s: %li", "ranges", (long)m_map
.elements ());
1037 auto_vec
<const bounded_ranges
*> vec_objs (m_map
.elements ());
1038 for (const auto &iter
: m_map
)
1039 vec_objs
.quick_push (iter
.second
);
1041 ([](const void *p1
, const void *p2
) -> int
1043 const bounded_ranges
*br1
= *(const bounded_ranges
* const *)p1
;
1044 const bounded_ranges
*br2
= *(const bounded_ranges
* const *)p2
;
1045 return bounded_ranges::cmp (br1
, br2
);
1048 for (const auto &iter
: vec_objs
)
1050 logger
->start_log_line ();
1051 pretty_printer
*pp
= logger
->get_printer ();
1052 pp_string (pp
, " ");
1053 iter
->dump_to_pp (pp
, true);
1054 logger
->end_log_line ();
1058 /* class equiv_class. */
1060 /* equiv_class's default ctor. */
1062 equiv_class::equiv_class ()
1063 : m_constant (NULL_TREE
), m_cst_sval (NULL
), m_vars ()
1067 /* equiv_class's copy ctor. */
1069 equiv_class::equiv_class (const equiv_class
&other
)
1070 : m_constant (other
.m_constant
), m_cst_sval (other
.m_cst_sval
),
1071 m_vars (other
.m_vars
.length ())
1073 for (const svalue
*sval
: other
.m_vars
)
1074 m_vars
.quick_push (sval
);
1077 /* Print an all-on-one-line representation of this equiv_class to PP,
1078 which must support %E for trees. */
1081 equiv_class::print (pretty_printer
*pp
) const
1083 pp_character (pp
, '{');
1086 FOR_EACH_VEC_ELT (m_vars
, i
, sval
)
1089 pp_string (pp
, " == ");
1090 sval
->dump_to_pp (pp
, true);
1095 pp_string (pp
, " == ");
1096 pp_printf (pp
, "[m_constant]%qE", m_constant
);
1098 pp_character (pp
, '}');
1101 /* Return a new json::object of the form
1103 "constant" : optional str}. */
1106 equiv_class::to_json () const
1108 json::object
*ec_obj
= new json::object ();
1110 json::array
*sval_arr
= new json::array ();
1111 for (const svalue
*sval
: m_vars
)
1112 sval_arr
->append (sval
->to_json ());
1113 ec_obj
->set ("svals", sval_arr
);
1118 pp_format_decoder (&pp
) = default_tree_printer
;
1119 pp_printf (&pp
, "%qE", m_constant
);
1120 ec_obj
->set ("constant", new json::string (pp_formatted_text (&pp
)));
1126 /* Generate a hash value for this equiv_class.
1127 This relies on the ordering of m_vars, and so this object needs to
1128 have been canonicalized for this to be meaningful. */
1131 equiv_class::hash () const
1133 inchash::hash hstate
;
1135 inchash::add_expr (m_constant
, hstate
);
1136 for (const svalue
* sval
: m_vars
)
1137 hstate
.add_ptr (sval
);
1138 return hstate
.end ();
1141 /* Equality operator for equiv_class.
1142 This relies on the ordering of m_vars, and so this object
1143 and OTHER need to have been canonicalized for this to be
1147 equiv_class::operator== (const equiv_class
&other
)
1149 if (m_constant
!= other
.m_constant
)
1150 return false; // TODO: use tree equality here?
1152 /* FIXME: should we compare m_cst_sval? */
1154 if (m_vars
.length () != other
.m_vars
.length ())
1159 FOR_EACH_VEC_ELT (m_vars
, i
, sval
)
1160 if (sval
!= other
.m_vars
[i
])
1166 /* Add SID to this equiv_class, using CM to check if it's a constant. */
1169 equiv_class::add (const svalue
*sval
)
1172 if (tree cst
= sval
->maybe_get_constant ())
1174 gcc_assert (CONSTANT_CLASS_P (cst
));
1175 /* FIXME: should we canonicalize which svalue is the constant
1176 when there are multiple equal constants? */
1180 m_vars
.safe_push (sval
);
1183 /* Remove SID from this equivalence class.
1184 Return true if SID was the last var in the equivalence class (suggesting
1185 a possible leak). */
1188 equiv_class::del (const svalue
*sval
)
1191 gcc_assert (sval
!= m_cst_sval
);
1195 FOR_EACH_VEC_ELT (m_vars
, i
, iv
)
1199 m_vars
[i
] = m_vars
[m_vars
.length () - 1];
1201 return m_vars
.length () == 0;
1205 /* SVAL must be in the class. */
1210 /* Get a representative member of this class, for handling cases
1211 where the IDs can change mid-traversal. */
1214 equiv_class::get_representative () const
1216 gcc_assert (m_vars
.length () > 0);
1220 /* Sort the svalues within this equiv_class. */
1223 equiv_class::canonicalize ()
1225 m_vars
.qsort (svalue::cmp_ptr_ptr
);
1228 /* Return true if this EC contains a variable, false if it merely
1230 Subroutine of constraint_manager::canonicalize, for removing
1234 equiv_class::contains_non_constant_p () const
1238 for (auto iter
: m_vars
)
1239 if (iter
->maybe_get_constant ())
1242 /* We have {non-constant == constant}. */
1244 /* We only have constants. */
1248 /* Return true if we have {non-constant == non-constant}. */
1249 return m_vars
.length () > 1;
1252 /* Get a debug string for C_OP. */
1255 constraint_op_code (enum constraint_op c_op
)
1261 case CONSTRAINT_NE
: return "!=";
1262 case CONSTRAINT_LT
: return "<";
1263 case CONSTRAINT_LE
: return "<=";
1267 /* Convert C_OP to an enum tree_code. */
1270 constraint_tree_code (enum constraint_op c_op
)
1276 case CONSTRAINT_NE
: return NE_EXPR
;
1277 case CONSTRAINT_LT
: return LT_EXPR
;
1278 case CONSTRAINT_LE
: return LE_EXPR
;
1282 /* Given "lhs C_OP rhs", determine "lhs T_OP rhs".
1284 For example, given "x < y", then "x > y" is false. */
1287 eval_constraint_op_for_op (enum constraint_op c_op
, enum tree_code t_op
)
1294 if (t_op
== EQ_EXPR
)
1295 return tristate (tristate::TS_FALSE
);
1296 if (t_op
== NE_EXPR
)
1297 return tristate (tristate::TS_TRUE
);
1300 if (t_op
== LT_EXPR
|| t_op
== LE_EXPR
|| t_op
== NE_EXPR
)
1301 return tristate (tristate::TS_TRUE
);
1302 if (t_op
== EQ_EXPR
|| t_op
== GT_EXPR
|| t_op
== GE_EXPR
)
1303 return tristate (tristate::TS_FALSE
);
1306 if (t_op
== LE_EXPR
)
1307 return tristate (tristate::TS_TRUE
);
1308 if (t_op
== GT_EXPR
)
1309 return tristate (tristate::TS_FALSE
);
1312 return tristate (tristate::TS_UNKNOWN
);
1315 /* class constraint. */
1317 /* Print this constraint to PP (which must support %E for trees),
1318 using CM to look up equiv_class instances from ids. */
1321 constraint::print (pretty_printer
*pp
, const constraint_manager
&cm
) const
1324 pp_string (pp
, ": ");
1325 m_lhs
.get_obj (cm
).print (pp
);
1326 pp_string (pp
, " ");
1327 pp_string (pp
, constraint_op_code (m_op
));
1328 pp_string (pp
, " ");
1330 pp_string (pp
, ": ");
1331 m_rhs
.get_obj (cm
).print (pp
);
1334 /* Return a new json::object of the form
1335 {"lhs" : int, the EC index
1337 "rhs" : int, the EC index}. */
1340 constraint::to_json () const
1342 json::object
*con_obj
= new json::object ();
1344 con_obj
->set ("lhs", new json::integer_number (m_lhs
.as_int ()));
1345 con_obj
->set ("op", new json::string (constraint_op_code (m_op
)));
1346 con_obj
->set ("rhs", new json::integer_number (m_rhs
.as_int ()));
1351 /* Generate a hash value for this constraint. */
1354 constraint::hash () const
1356 inchash::hash hstate
;
1357 hstate
.add_int (m_lhs
.m_idx
);
1358 hstate
.add_int (m_op
);
1359 hstate
.add_int (m_rhs
.m_idx
);
1360 return hstate
.end ();
1363 /* Equality operator for constraints. */
1366 constraint::operator== (const constraint
&other
) const
1368 if (m_lhs
!= other
.m_lhs
)
1370 if (m_op
!= other
.m_op
)
1372 if (m_rhs
!= other
.m_rhs
)
1377 /* Return true if this constraint is implied by OTHER. */
1380 constraint::implied_by (const constraint
&other
,
1381 const constraint_manager
&cm
) const
1383 if (m_lhs
== other
.m_lhs
)
1384 if (tree rhs_const
= m_rhs
.get_obj (cm
).get_any_constant ())
1385 if (tree other_rhs_const
= other
.m_rhs
.get_obj (cm
).get_any_constant ())
1386 if (m_lhs
.get_obj (cm
).get_any_constant () == NULL_TREE
)
1387 if (m_op
== other
.m_op
)
1394 if (compare_constants (rhs_const
,
1396 other_rhs_const
).is_true ())
1403 /* class bounded_ranges_constraint. */
1406 bounded_ranges_constraint::print (pretty_printer
*pp
,
1407 const constraint_manager
&cm
) const
1410 pp_string (pp
, ": ");
1411 m_ec_id
.get_obj (cm
).print (pp
);
1412 pp_string (pp
, ": ");
1413 m_ranges
->dump_to_pp (pp
, true);
1417 bounded_ranges_constraint::to_json () const
1419 json::object
*con_obj
= new json::object ();
1421 con_obj
->set ("ec", new json::integer_number (m_ec_id
.as_int ()));
1422 con_obj
->set ("ranges", m_ranges
->to_json ());
1428 bounded_ranges_constraint::
1429 operator== (const bounded_ranges_constraint
&other
) const
1431 if (m_ec_id
!= other
.m_ec_id
)
1434 /* We can compare by pointer, since the bounded_ranges_manager
1435 consolidates instances. */
1436 return m_ranges
== other
.m_ranges
;
1440 bounded_ranges_constraint::add_to_hash (inchash::hash
*hstate
) const
1442 hstate
->add_int (m_ec_id
.m_idx
);
1443 hstate
->merge_hash (m_ranges
->get_hash ());
1446 /* class equiv_class_id. */
1448 /* Get the underlying equiv_class for this ID from CM. */
1451 equiv_class_id::get_obj (const constraint_manager
&cm
) const
1453 return cm
.get_equiv_class_by_index (m_idx
);
1456 /* Access the underlying equiv_class for this ID from CM. */
1459 equiv_class_id::get_obj (constraint_manager
&cm
) const
1461 return cm
.get_equiv_class_by_index (m_idx
);
1464 /* Print this equiv_class_id to PP. */
1467 equiv_class_id::print (pretty_printer
*pp
) const
1470 pp_printf (pp
, "null");
1472 pp_printf (pp
, "ec%i", m_idx
);
1475 /* class constraint_manager. */
1477 /* constraint_manager's copy ctor. */
1479 constraint_manager::constraint_manager (const constraint_manager
&other
)
1480 : m_equiv_classes (other
.m_equiv_classes
.length ()),
1481 m_constraints (other
.m_constraints
.length ()),
1482 m_bounded_ranges_constraints (other
.m_bounded_ranges_constraints
.length ()),
1487 FOR_EACH_VEC_ELT (other
.m_equiv_classes
, i
, ec
)
1488 m_equiv_classes
.quick_push (new equiv_class (*ec
));
1490 FOR_EACH_VEC_ELT (other
.m_constraints
, i
, c
)
1491 m_constraints
.quick_push (*c
);
1492 for (const auto &iter
: other
.m_bounded_ranges_constraints
)
1493 m_bounded_ranges_constraints
.quick_push (iter
);
1496 /* constraint_manager's assignment operator. */
1499 constraint_manager::operator= (const constraint_manager
&other
)
1501 gcc_assert (m_equiv_classes
.length () == 0);
1502 gcc_assert (m_constraints
.length () == 0);
1503 gcc_assert (m_bounded_ranges_constraints
.length () == 0);
1507 m_equiv_classes
.reserve (other
.m_equiv_classes
.length ());
1508 FOR_EACH_VEC_ELT (other
.m_equiv_classes
, i
, ec
)
1509 m_equiv_classes
.quick_push (new equiv_class (*ec
));
1511 m_constraints
.reserve (other
.m_constraints
.length ());
1512 FOR_EACH_VEC_ELT (other
.m_constraints
, i
, c
)
1513 m_constraints
.quick_push (*c
);
1514 for (const auto &iter
: other
.m_bounded_ranges_constraints
)
1515 m_bounded_ranges_constraints
.quick_push (iter
);
1520 /* Generate a hash value for this constraint_manager. */
1523 constraint_manager::hash () const
1525 inchash::hash hstate
;
1530 FOR_EACH_VEC_ELT (m_equiv_classes
, i
, ec
)
1531 hstate
.merge_hash (ec
->hash ());
1532 FOR_EACH_VEC_ELT (m_constraints
, i
, c
)
1533 hstate
.merge_hash (c
->hash ());
1534 for (const auto &iter
: m_bounded_ranges_constraints
)
1535 iter
.add_to_hash (&hstate
);
1536 return hstate
.end ();
1539 /* Equality operator for constraint_manager. */
1542 constraint_manager::operator== (const constraint_manager
&other
) const
1544 if (m_equiv_classes
.length () != other
.m_equiv_classes
.length ())
1546 if (m_constraints
.length () != other
.m_constraints
.length ())
1548 if (m_bounded_ranges_constraints
.length ()
1549 != other
.m_bounded_ranges_constraints
.length ())
1555 FOR_EACH_VEC_ELT (m_equiv_classes
, i
, ec
)
1556 if (!(*ec
== *other
.m_equiv_classes
[i
]))
1561 FOR_EACH_VEC_ELT (m_constraints
, i
, c
)
1562 if (!(*c
== other
.m_constraints
[i
]))
1565 for (unsigned i
= 0; i
< m_bounded_ranges_constraints
.length (); i
++)
1567 if (m_bounded_ranges_constraints
[i
]
1568 != other
.m_bounded_ranges_constraints
[i
])
1575 /* Print this constraint_manager to PP (which must support %E for trees). */
1578 constraint_manager::print (pretty_printer
*pp
) const
1580 pp_string (pp
, "{");
1583 FOR_EACH_VEC_ELT (m_equiv_classes
, i
, ec
)
1586 pp_string (pp
, ", ");
1587 equiv_class_id (i
).print (pp
);
1588 pp_string (pp
, ": ");
1591 pp_string (pp
, " | ");
1593 FOR_EACH_VEC_ELT (m_constraints
, i
, c
)
1596 pp_string (pp
, " && ");
1597 c
->print (pp
, *this);
1599 if (m_bounded_ranges_constraints
.length ())
1601 pp_string (pp
, " | ");
1603 for (const auto &iter
: m_bounded_ranges_constraints
)
1606 pp_string (pp
, " && ");
1607 iter
.print (pp
, *this);
1611 pp_printf (pp
, "}");
1614 /* Dump a representation of this constraint_manager to PP
1615 (which must support %E for trees). */
1618 constraint_manager::dump_to_pp (pretty_printer
*pp
, bool multiline
) const
1621 pp_string (pp
, " ");
1622 pp_string (pp
, "equiv classes:");
1626 pp_string (pp
, " {");
1629 FOR_EACH_VEC_ELT (m_equiv_classes
, i
, ec
)
1632 pp_string (pp
, " ");
1634 pp_string (pp
, ", ");
1635 equiv_class_id (i
).print (pp
);
1636 pp_string (pp
, ": ");
1642 pp_string (pp
, " ");
1644 pp_string (pp
, "}");
1645 pp_string (pp
, "constraints:");
1649 pp_string (pp
, "{");
1651 FOR_EACH_VEC_ELT (m_constraints
, i
, c
)
1654 pp_string (pp
, " ");
1655 pp_printf (pp
, "%i: ", i
);
1656 c
->print (pp
, *this);
1661 pp_string (pp
, "}");
1662 if (m_bounded_ranges_constraints
.length ())
1665 pp_string (pp
, " ");
1666 pp_string (pp
, "ranges:");
1670 pp_string (pp
, "{");
1672 for (const auto &iter
: m_bounded_ranges_constraints
)
1675 pp_string (pp
, " ");
1677 pp_string (pp
, " && ");
1678 iter
.print (pp
, *this);
1684 pp_string (pp
, "}");
1688 /* Dump a multiline representation of this constraint_manager to FP. */
1691 constraint_manager::dump (FILE *fp
) const
1694 pp_format_decoder (&pp
) = default_tree_printer
;
1695 pp_show_color (&pp
) = pp_show_color (global_dc
->printer
);
1696 pp
.buffer
->stream
= fp
;
1697 dump_to_pp (&pp
, true);
1701 /* Dump a multiline representation of this constraint_manager to stderr. */
1704 constraint_manager::dump () const
1709 /* Dump a multiline representation of CM to stderr. */
1712 debug (const constraint_manager
&cm
)
1717 /* Return a new json::object of the form
1718 {"ecs" : array of objects, one per equiv_class
1719 "constraints" : array of objects, one per constraint}. */
1722 constraint_manager::to_json () const
1724 json::object
*cm_obj
= new json::object ();
1726 /* Equivalence classes. */
1728 json::array
*ec_arr
= new json::array ();
1729 for (const equiv_class
*ec
: m_equiv_classes
)
1730 ec_arr
->append (ec
->to_json ());
1731 cm_obj
->set ("ecs", ec_arr
);
1736 json::array
*con_arr
= new json::array ();
1737 for (const constraint
&c
: m_constraints
)
1738 con_arr
->append (c
.to_json ());
1739 cm_obj
->set ("constraints", con_arr
);
1742 /* m_bounded_ranges_constraints. */
1744 json::array
*con_arr
= new json::array ();
1745 for (const auto &c
: m_bounded_ranges_constraints
)
1746 con_arr
->append (c
.to_json ());
1747 cm_obj
->set ("bounded_ranges_constraints", con_arr
);
1753 /* Attempt to add the constraint LHS OP RHS to this constraint_manager.
1754 Return true if the constraint could be added (or is already true).
1755 Return false if the constraint contradicts existing knowledge. */
1758 constraint_manager::add_constraint (const svalue
*lhs
,
1762 lhs
= lhs
->unwrap_any_unmergeable ();
1763 rhs
= rhs
->unwrap_any_unmergeable ();
1765 /* Nothing can be known about unknown/poisoned values. */
1766 if (!lhs
->can_have_associated_state_p ()
1767 || !rhs
->can_have_associated_state_p ())
1768 /* Not a contradiction. */
1771 /* Check the conditions on svalues. */
1773 tristate t_cond
= eval_condition (lhs
, op
, rhs
);
1775 /* If we already have the condition, do nothing. */
1776 if (t_cond
.is_true ())
1779 /* Reject a constraint that would contradict existing knowledge, as
1781 if (t_cond
.is_false ())
1785 equiv_class_id lhs_ec_id
= get_or_add_equiv_class (lhs
);
1786 equiv_class_id rhs_ec_id
= get_or_add_equiv_class (rhs
);
1788 /* Check the stronger conditions on ECs. */
1790 tristate t
= eval_condition (lhs_ec_id
, op
, rhs_ec_id
);
1792 /* Discard constraints that are already known. */
1796 /* Reject unsatisfiable constraints. */
1802 (SVAL + OFFSET) > CST,
1803 then that can imply:
1804 SVAL > (CST - OFFSET). */
1805 if (const binop_svalue
*lhs_binop
= lhs
->dyn_cast_binop_svalue ())
1806 if (tree rhs_cst
= rhs
->maybe_get_constant ())
1807 if (tree offset
= lhs_binop
->get_arg1 ()->maybe_get_constant ())
1808 if ((op
== GT_EXPR
|| op
== LT_EXPR
1809 || op
== GE_EXPR
|| op
== LE_EXPR
)
1810 && lhs_binop
->get_op () == PLUS_EXPR
)
1812 tree offset_of_cst
= fold_build2 (MINUS_EXPR
, TREE_TYPE (rhs_cst
),
1814 const svalue
*implied_lhs
= lhs_binop
->get_arg0 ();
1815 enum tree_code implied_op
= op
;
1816 const svalue
*implied_rhs
1817 = m_mgr
->get_or_create_constant_svalue (offset_of_cst
);
1818 if (!add_constraint (implied_lhs
, implied_op
, implied_rhs
))
1820 /* The above add_constraint could lead to EC merger, so we need
1821 to refresh the EC IDs. */
1822 lhs_ec_id
= get_or_add_equiv_class (lhs
);
1823 rhs_ec_id
= get_or_add_equiv_class (rhs
);
1826 add_unknown_constraint (lhs_ec_id
, op
, rhs_ec_id
);
1830 /* Attempt to add the constraint LHS_EC_ID OP RHS_EC_ID to this
1832 Return true if the constraint could be added (or is already true).
1833 Return false if the constraint contradicts existing knowledge. */
1836 constraint_manager::add_constraint (equiv_class_id lhs_ec_id
,
1838 equiv_class_id rhs_ec_id
)
1840 tristate t
= eval_condition (lhs_ec_id
, op
, rhs_ec_id
);
1842 /* Discard constraints that are already known. */
1846 /* Reject unsatisfiable constraints. */
1850 add_unknown_constraint (lhs_ec_id
, op
, rhs_ec_id
);
1854 /* Add the constraint LHS_EC_ID OP RHS_EC_ID to this constraint_manager,
1855 where the constraint has already been checked for being "unknown". */
1858 constraint_manager::add_unknown_constraint (equiv_class_id lhs_ec_id
,
1860 equiv_class_id rhs_ec_id
)
1862 gcc_assert (lhs_ec_id
!= rhs_ec_id
);
1864 /* For now, simply accumulate constraints, without attempting any further
1870 /* Merge rhs_ec into lhs_ec. */
1871 equiv_class
&lhs_ec_obj
= lhs_ec_id
.get_obj (*this);
1872 const equiv_class
&rhs_ec_obj
= rhs_ec_id
.get_obj (*this);
1876 FOR_EACH_VEC_ELT (rhs_ec_obj
.m_vars
, i
, sval
)
1877 lhs_ec_obj
.add (sval
);
1879 if (rhs_ec_obj
.m_constant
)
1881 lhs_ec_obj
.m_constant
= rhs_ec_obj
.m_constant
;
1882 lhs_ec_obj
.m_cst_sval
= rhs_ec_obj
.m_cst_sval
;
1885 /* Drop rhs equivalence class, overwriting it with the
1886 final ec (which might be the same one). */
1887 equiv_class_id final_ec_id
= m_equiv_classes
.length () - 1;
1888 equiv_class
*old_ec
= m_equiv_classes
[rhs_ec_id
.m_idx
];
1889 equiv_class
*final_ec
= m_equiv_classes
.pop ();
1890 if (final_ec
!= old_ec
)
1891 m_equiv_classes
[rhs_ec_id
.m_idx
] = final_ec
;
1893 if (lhs_ec_id
== final_ec_id
)
1894 lhs_ec_id
= rhs_ec_id
;
1896 /* Update the constraints. */
1898 FOR_EACH_VEC_ELT (m_constraints
, i
, c
)
1900 /* Update references to the rhs_ec so that
1901 they refer to the lhs_ec. */
1902 if (c
->m_lhs
== rhs_ec_id
)
1903 c
->m_lhs
= lhs_ec_id
;
1904 if (c
->m_rhs
== rhs_ec_id
)
1905 c
->m_rhs
= lhs_ec_id
;
1907 /* Renumber all constraints that refer to the final rhs_ec
1908 to the old rhs_ec, where the old final_ec now lives. */
1909 if (c
->m_lhs
== final_ec_id
)
1910 c
->m_lhs
= rhs_ec_id
;
1911 if (c
->m_rhs
== final_ec_id
)
1912 c
->m_rhs
= rhs_ec_id
;
1914 bounded_ranges_constraint
*brc
;
1915 FOR_EACH_VEC_ELT (m_bounded_ranges_constraints
, i
, brc
)
1917 if (brc
->m_ec_id
== rhs_ec_id
)
1918 brc
->m_ec_id
= lhs_ec_id
;
1919 if (brc
->m_ec_id
== final_ec_id
)
1920 brc
->m_ec_id
= rhs_ec_id
;
1923 /* We may now have self-comparisons due to the merger; these
1924 constraints should be removed. */
1925 unsigned read_index
, write_index
;
1926 VEC_ORDERED_REMOVE_IF (m_constraints
, read_index
, write_index
, c
,
1927 (c
->m_lhs
== c
->m_rhs
));
1931 add_constraint_internal (rhs_ec_id
, CONSTRAINT_LE
, lhs_ec_id
);
1934 add_constraint_internal (lhs_ec_id
, CONSTRAINT_LE
, rhs_ec_id
);
1937 add_constraint_internal (lhs_ec_id
, CONSTRAINT_NE
, rhs_ec_id
);
1940 add_constraint_internal (rhs_ec_id
, CONSTRAINT_LT
, lhs_ec_id
);
1943 add_constraint_internal (lhs_ec_id
, CONSTRAINT_LT
, rhs_ec_id
);
1952 /* Subroutine of constraint_manager::add_constraint, for handling all
1953 operations other than equality (for which equiv classes are merged). */
1956 constraint_manager::add_constraint_internal (equiv_class_id lhs_id
,
1957 enum constraint_op c_op
,
1958 equiv_class_id rhs_id
)
1960 if (m_constraints
.length () >= (unsigned)param_analyzer_max_constraints
)
1963 constraint
new_c (lhs_id
, c_op
, rhs_id
);
1965 /* Remove existing constraints that would be implied by the
1967 unsigned read_index
, write_index
;
1969 VEC_ORDERED_REMOVE_IF (m_constraints
, read_index
, write_index
, c
,
1970 (c
->implied_by (new_c
, *this)));
1972 /* Add the constraint. */
1973 m_constraints
.safe_push (new_c
);
1975 /* We don't yet update m_bounded_ranges_constraints here yet. */
1977 if (!flag_analyzer_transitivity
)
1980 if (c_op
!= CONSTRAINT_NE
)
1982 /* The following can potentially add EQ_EXPR facts, which could lead
1983 to ECs being merged, which would change the meaning of the EC IDs.
1984 Hence we need to do this via representatives. */
1985 const svalue
*lhs
= lhs_id
.get_obj (*this).get_representative ();
1986 const svalue
*rhs
= rhs_id
.get_obj (*this).get_representative ();
1988 /* We have LHS </<= RHS */
1990 /* Handle transitivity of ordering by adding additional constraints
1991 based on what we already knew.
1993 So if we have already have:
2001 We need to recurse to ensure we also add:
2003 We call the checked add_constraint to avoid adding constraints
2004 that are already present. Doing so also ensures termination
2005 in the case of cycles.
2007 We also check for single-element ranges, adding EQ_EXPR facts
2008 where we discover them. For example 3 < x < 5 implies
2009 that x == 4 (if x is an integer). */
2010 for (unsigned i
= 0; i
< m_constraints
.length (); i
++)
2012 const constraint
*other
= &m_constraints
[i
];
2013 if (other
->is_ordering_p ())
2015 /* Refresh the EC IDs, in case any mergers have happened. */
2016 lhs_id
= get_or_add_equiv_class (lhs
);
2017 rhs_id
= get_or_add_equiv_class (rhs
);
2019 tree lhs_const
= lhs_id
.get_obj (*this).m_constant
;
2020 tree rhs_const
= rhs_id
.get_obj (*this).m_constant
;
2021 tree other_lhs_const
2022 = other
->m_lhs
.get_obj (*this).m_constant
;
2023 tree other_rhs_const
2024 = other
->m_rhs
.get_obj (*this).m_constant
;
2026 /* We have "LHS </<= RHS" and "other.lhs </<= other.rhs". */
2028 /* If we have LHS </<= RHS and RHS </<= LHS, then we have a
2030 if (rhs_id
== other
->m_lhs
2031 && other
->m_rhs
== lhs_id
)
2033 /* We must have equality for this to be possible. */
2034 gcc_assert (c_op
== CONSTRAINT_LE
2035 && other
->m_op
== CONSTRAINT_LE
);
2036 add_constraint (lhs_id
, EQ_EXPR
, rhs_id
);
2037 /* Adding an equality will merge the two ECs and potentially
2038 reorganize the constraints. Stop iterating. */
2041 /* Otherwise, check for transitivity. */
2042 if (rhs_id
== other
->m_lhs
)
2044 /* With RHS == other.lhs, we have:
2045 "LHS </<= (RHS, other.lhs) </<= other.rhs"
2046 and thus this implies "LHS </<= other.rhs". */
2048 /* Do we have a tightly-constrained range? */
2053 range
r (bound (lhs_const
, c_op
== CONSTRAINT_LE
),
2054 bound (other_rhs_const
,
2055 other
->m_op
== CONSTRAINT_LE
));
2056 if (tree constant
= r
.constrained_to_single_element ())
2058 const svalue
*cst_sval
2059 = m_mgr
->get_or_create_constant_svalue (constant
);
2062 get_or_add_equiv_class (cst_sval
));
2067 /* Otherwise, add the constraint implied by transitivity. */
2068 enum tree_code new_op
2069 = ((c_op
== CONSTRAINT_LE
&& other
->m_op
== CONSTRAINT_LE
)
2070 ? LE_EXPR
: LT_EXPR
);
2071 add_constraint (lhs_id
, new_op
, other
->m_rhs
);
2073 else if (other
->m_rhs
== lhs_id
)
2075 /* With other.rhs == LHS, we have:
2076 "other.lhs </<= (other.rhs, LHS) </<= RHS"
2077 and thus this implies "other.lhs </<= RHS". */
2079 /* Do we have a tightly-constrained range? */
2084 range
r (bound (other_lhs_const
,
2085 other
->m_op
== CONSTRAINT_LE
),
2087 c_op
== CONSTRAINT_LE
));
2088 if (tree constant
= r
.constrained_to_single_element ())
2090 const svalue
*cst_sval
2091 = m_mgr
->get_or_create_constant_svalue (constant
);
2094 get_or_add_equiv_class (cst_sval
));
2099 /* Otherwise, add the constraint implied by transitivity. */
2100 enum tree_code new_op
2101 = ((c_op
== CONSTRAINT_LE
&& other
->m_op
== CONSTRAINT_LE
)
2102 ? LE_EXPR
: LT_EXPR
);
2103 add_constraint (other
->m_lhs
, new_op
, rhs_id
);
2110 /* Attempt to add the constraint that SVAL is within RANGES to this
2113 Return true if the constraint was successfully added (or is already
2115 Return false if the constraint contradicts existing knowledge. */
2118 constraint_manager::add_bounded_ranges (const svalue
*sval
,
2119 const bounded_ranges
*ranges
)
2121 /* If RANGES is just a singleton, convert this to adding the constraint:
2122 "SVAL == {the singleton}". */
2123 if (ranges
->get_count () == 1
2124 && ranges
->get_range (0).singleton_p ())
2126 tree range_cst
= ranges
->get_range (0).m_lower
;
2127 const svalue
*range_sval
2128 = m_mgr
->get_or_create_constant_svalue (range_cst
);
2129 return add_constraint (sval
, EQ_EXPR
, range_sval
);
2132 sval
= sval
->unwrap_any_unmergeable ();
2134 /* Nothing can be known about unknown/poisoned values. */
2135 if (!sval
->can_have_associated_state_p ())
2136 /* Not a contradiction. */
2139 /* If SVAL is a constant, then we can look at RANGES directly. */
2140 if (tree cst
= sval
->maybe_get_constant ())
2142 /* If the ranges contain CST, then it's a successful no-op;
2143 otherwise it's a contradiction. */
2144 return ranges
->contain_p (cst
);
2147 equiv_class_id ec_id
= get_or_add_equiv_class (sval
);
2149 /* If the EC has a constant, it's either true or false. */
2150 const equiv_class
&ec
= ec_id
.get_obj (*this);
2151 if (tree ec_cst
= ec
.get_any_constant ())
2153 if (ranges
->contain_p (ec_cst
))
2154 /* We already have SVAL == EC_CST, within RANGES, so
2155 we can discard RANGES and succeed. */
2158 /* We already have SVAL == EC_CST, not within RANGES, so
2159 we can reject RANGES as a contradiction. */
2163 /* We have at most one per ec_id. */
2164 /* Iterate through each range in RANGES. */
2165 for (auto iter
: m_bounded_ranges_constraints
)
2167 if (iter
.m_ec_id
== ec_id
)
2169 /* Update with intersection, or fail if empty. */
2170 bounded_ranges_manager
*mgr
= get_range_manager ();
2171 const bounded_ranges
*intersection
2172 = mgr
->get_or_create_intersection (iter
.m_ranges
, ranges
);
2173 if (intersection
->empty_p ())
2175 /* No intersection; fail. */
2180 /* Update with intersection; succeed. */
2181 iter
.m_ranges
= intersection
;
2187 m_bounded_ranges_constraints
.safe_push
2188 (bounded_ranges_constraint (ec_id
, ranges
));
2195 /* Look for SVAL within the equivalence classes of this constraint_manager;
2196 if found, return true, writing the id to *OUT if OUT is non-NULL,
2197 otherwise return false. */
2200 constraint_manager::get_equiv_class_by_svalue (const svalue
*sval
,
2201 equiv_class_id
*out
) const
2203 /* TODO: should we have a map, rather than these searches? */
2206 FOR_EACH_VEC_ELT (m_equiv_classes
, i
, ec
)
2210 FOR_EACH_VEC_ELT (ec
->m_vars
, j
, iv
)
2214 *out
= equiv_class_id (i
);
2221 /* Tries to find a svalue inside another svalue. */
2223 class sval_finder
: public visitor
2226 sval_finder (const svalue
*query
) : m_query (query
), m_found (false)
2230 bool found_query_p ()
2235 void visit_region_svalue (const region_svalue
*sval
)
2237 m_found
|= m_query
== sval
;
2240 void visit_constant_svalue (const constant_svalue
*sval
)
2242 m_found
|= m_query
== sval
;
2245 void visit_unknown_svalue (const unknown_svalue
*sval
)
2247 m_found
|= m_query
== sval
;
2250 void visit_poisoned_svalue (const poisoned_svalue
*sval
)
2252 m_found
|= m_query
== sval
;
2255 void visit_setjmp_svalue (const setjmp_svalue
*sval
)
2257 m_found
|= m_query
== sval
;
2260 void visit_initial_svalue (const initial_svalue
*sval
)
2262 m_found
|= m_query
== sval
;
2265 void visit_unaryop_svalue (const unaryop_svalue
*sval
)
2267 m_found
|= m_query
== sval
;
2270 void visit_binop_svalue (const binop_svalue
*sval
)
2272 m_found
|= m_query
== sval
;
2275 void visit_sub_svalue (const sub_svalue
*sval
)
2277 m_found
|= m_query
== sval
;
2280 void visit_repeated_svalue (const repeated_svalue
*sval
)
2282 m_found
|= m_query
== sval
;
2285 void visit_bits_within_svalue (const bits_within_svalue
*sval
)
2287 m_found
|= m_query
== sval
;
2290 void visit_unmergeable_svalue (const unmergeable_svalue
*sval
)
2292 m_found
|= m_query
== sval
;
2295 void visit_placeholder_svalue (const placeholder_svalue
*sval
)
2297 m_found
|= m_query
== sval
;
2300 void visit_widening_svalue (const widening_svalue
*sval
)
2302 m_found
|= m_query
== sval
;
2305 void visit_compound_svalue (const compound_svalue
*sval
)
2307 m_found
|= m_query
== sval
;
2310 void visit_conjured_svalue (const conjured_svalue
*sval
)
2312 m_found
|= m_query
== sval
;
2315 void visit_asm_output_svalue (const asm_output_svalue
*sval
)
2317 m_found
|= m_query
== sval
;
2320 void visit_const_fn_result_svalue (const const_fn_result_svalue
*sval
)
2322 m_found
|= m_query
== sval
;
2326 const svalue
*m_query
;
2330 /* Returns true if SVAL is constrained. */
2333 constraint_manager::sval_constrained_p (const svalue
*sval
) const
2337 sval_finder
finder (sval
);
2338 FOR_EACH_VEC_ELT (m_equiv_classes
, i
, ec
)
2342 FOR_EACH_VEC_ELT (ec
->m_vars
, j
, iv
)
2344 iv
->accept (&finder
);
2345 if (finder
.found_query_p ())
2352 /* Ensure that SVAL has an equivalence class within this constraint_manager;
2353 return the ID of the class. */
2356 constraint_manager::get_or_add_equiv_class (const svalue
*sval
)
2358 equiv_class_id
result (-1);
2360 gcc_assert (sval
->can_have_associated_state_p ());
2362 /* Convert all NULL pointers to (void *) to avoid state explosions
2363 involving all of the various (foo *)NULL vs (bar *)NULL. */
2364 if (sval
->get_type ())
2365 if (POINTER_TYPE_P (sval
->get_type ()))
2366 if (tree cst
= sval
->maybe_get_constant ())
2368 sval
= m_mgr
->get_or_create_constant_svalue (null_pointer_node
);
2370 /* Try svalue match. */
2371 if (get_equiv_class_by_svalue (sval
, &result
))
2374 /* Try equality of constants. */
2375 if (tree cst
= sval
->maybe_get_constant ())
2379 FOR_EACH_VEC_ELT (m_equiv_classes
, i
, ec
)
2381 && types_compatible_p (TREE_TYPE (cst
),
2382 TREE_TYPE (ec
->m_constant
)))
2384 tree eq
= fold_binary (EQ_EXPR
, boolean_type_node
,
2385 cst
, ec
->m_constant
);
2386 if (eq
== boolean_true_node
)
2389 return equiv_class_id (i
);
2396 equiv_class
*new_ec
= new equiv_class ();
2398 m_equiv_classes
.safe_push (new_ec
);
2400 equiv_class_id
new_id (m_equiv_classes
.length () - 1);
2405 /* Evaluate the condition LHS_EC OP RHS_EC. */
2408 constraint_manager::eval_condition (equiv_class_id lhs_ec
,
2410 equiv_class_id rhs_ec
) const
2412 if (lhs_ec
== rhs_ec
)
2419 return tristate (tristate::TS_TRUE
);
2424 return tristate (tristate::TS_FALSE
);
2430 tree lhs_const
= lhs_ec
.get_obj (*this).get_any_constant ();
2431 tree rhs_const
= rhs_ec
.get_obj (*this).get_any_constant ();
2432 if (lhs_const
&& rhs_const
)
2434 tristate result_for_constants
2435 = compare_constants (lhs_const
, op
, rhs_const
);
2436 if (result_for_constants
.is_known ())
2437 return result_for_constants
;
2440 enum tree_code swapped_op
= swap_tree_comparison (op
);
2444 FOR_EACH_VEC_ELT (m_constraints
, i
, c
)
2446 if (c
->m_lhs
== lhs_ec
2447 && c
->m_rhs
== rhs_ec
)
2449 tristate result_for_constraint
2450 = eval_constraint_op_for_op (c
->m_op
, op
);
2451 if (result_for_constraint
.is_known ())
2452 return result_for_constraint
;
2454 /* Swapped operands. */
2455 if (c
->m_lhs
== rhs_ec
2456 && c
->m_rhs
== lhs_ec
)
2458 tristate result_for_constraint
2459 = eval_constraint_op_for_op (c
->m_op
, swapped_op
);
2460 if (result_for_constraint
.is_known ())
2461 return result_for_constraint
;
2465 /* We don't use m_bounded_ranges_constraints here yet. */
2467 return tristate (tristate::TS_UNKNOWN
);
2471 constraint_manager::get_ec_bounds (equiv_class_id ec_id
) const
2477 FOR_EACH_VEC_ELT (m_constraints
, i
, c
)
2479 if (c
->m_lhs
== ec_id
)
2481 if (tree other_cst
= c
->m_rhs
.get_obj (*this).get_any_constant ())
2490 /* We have "EC_ID < OTHER_CST". */
2491 result
.add_bound (bound (other_cst
, false), BK_UPPER
);
2495 /* We have "EC_ID <= OTHER_CST". */
2496 result
.add_bound (bound (other_cst
, true), BK_UPPER
);
2500 if (c
->m_rhs
== ec_id
)
2502 if (tree other_cst
= c
->m_lhs
.get_obj (*this).get_any_constant ())
2511 /* We have "OTHER_CST < EC_ID"
2512 i.e. "EC_ID > OTHER_CST". */
2513 result
.add_bound (bound (other_cst
, false), BK_LOWER
);
2517 /* We have "OTHER_CST <= EC_ID"
2518 i.e. "EC_ID >= OTHER_CST". */
2519 result
.add_bound (bound (other_cst
, true), BK_LOWER
);
2528 /* Evaluate the condition LHS_EC OP RHS_CONST, avoiding the creation
2529 of equiv_class instances. */
2532 constraint_manager::eval_condition (equiv_class_id lhs_ec
,
2534 tree rhs_const
) const
2536 gcc_assert (!lhs_ec
.null_p ());
2537 gcc_assert (CONSTANT_CLASS_P (rhs_const
));
2539 if (tree lhs_const
= lhs_ec
.get_obj (*this).get_any_constant ())
2540 return compare_constants (lhs_const
, op
, rhs_const
);
2542 /* Check for known inequalities of the form
2543 (LHS_EC != OTHER_CST) or (OTHER_CST != LHS_EC).
2544 If RHS_CONST == OTHER_CST, then we also know that LHS_EC != OTHER_CST.
2545 For example, we might have the constraint
2547 so we want the condition
2552 FOR_EACH_VEC_ELT (m_constraints
, i
, c
)
2554 if (c
->m_op
== CONSTRAINT_NE
)
2556 if (c
->m_lhs
== lhs_ec
)
2558 if (tree other_cst
= c
->m_rhs
.get_obj (*this).get_any_constant ())
2559 if (compare_constants
2560 (rhs_const
, EQ_EXPR
, other_cst
).is_true ())
2565 return tristate (tristate::TS_FALSE
);
2567 return tristate (tristate::TS_TRUE
);
2573 if (c
->m_rhs
== lhs_ec
)
2575 if (tree other_cst
= c
->m_lhs
.get_obj (*this).get_any_constant ())
2576 if (compare_constants
2577 (rhs_const
, EQ_EXPR
, other_cst
).is_true ())
2582 return tristate (tristate::TS_FALSE
);
2584 return tristate (tristate::TS_TRUE
);
2593 bounded_ranges_manager
*mgr
= get_range_manager ();
2594 for (const auto &iter
: m_bounded_ranges_constraints
)
2595 if (iter
.m_ec_id
== lhs_ec
)
2596 return iter
.m_ranges
->eval_condition (op
, rhs_const
, mgr
);
2598 /* Look at existing bounds on LHS_EC. */
2599 range lhs_bounds
= get_ec_bounds (lhs_ec
);
2600 tristate result
= lhs_bounds
.eval_condition (op
, rhs_const
);
2601 if (result
.is_known ())
2604 /* Also reject if range::add_bound fails. */
2605 if (!lhs_bounds
.add_bound (op
, rhs_const
))
2606 return tristate (false);
2608 return tristate::unknown ();
2611 /* Return true iff "LHS == RHS" is known to be impossible due to
2614 Look for an EC containing an EC_VAL of the form (LHS OP CST).
2615 If found, see if (LHS OP CST) == EC_VAL is false.
2616 If so, we know this condition is false.
2618 For example, if we already know that
2620 and we're evaluating X == Z, we can test to see if
2621 (Z & CST_MASK) == EC_VAL
2624 and reject this if we know that's false. */
2627 constraint_manager::impossible_derived_conditions_p (const svalue
*lhs
,
2628 const svalue
*rhs
) const
2632 FOR_EACH_VEC_ELT (m_equiv_classes
, i
, ec
)
2634 for (const svalue
*ec_sval
: ec
->m_vars
)
2635 switch (ec_sval
->get_kind ())
2641 const binop_svalue
*iter_binop
2642 = as_a
<const binop_svalue
*> (ec_sval
);
2643 if (lhs
== iter_binop
->get_arg0 ()
2644 && iter_binop
->get_type ())
2645 if (iter_binop
->get_arg1 ()->get_kind () == SK_CONSTANT
)
2647 /* Try evalating EC_SVAL with LHS
2648 as the value of EC_SVAL's lhs, and see if it's
2649 consistent with existing knowledge. */
2650 const svalue
*subst_bin_op
2651 = m_mgr
->get_or_create_binop
2652 (iter_binop
->get_type (),
2653 iter_binop
->get_op (),
2655 iter_binop
->get_arg1 ());
2656 tristate t
= eval_condition (subst_bin_op
,
2660 return true; /* Impossible. */
2666 /* Not known to be impossible. */
2671 /* Evaluate the condition LHS OP RHS, without modifying this
2672 constraint_manager (avoiding the creation of equiv_class instances). */
2675 constraint_manager::eval_condition (const svalue
*lhs
,
2677 const svalue
*rhs
) const
2679 lhs
= lhs
->unwrap_any_unmergeable ();
2680 rhs
= rhs
->unwrap_any_unmergeable ();
2682 /* Nothing can be known about unknown or poisoned values. */
2683 if (lhs
->get_kind () == SK_UNKNOWN
2684 || lhs
->get_kind () == SK_POISONED
2685 || rhs
->get_kind () == SK_UNKNOWN
2686 || rhs
->get_kind () == SK_POISONED
)
2687 return tristate (tristate::TS_UNKNOWN
);
2690 && !(FLOAT_TYPE_P (lhs
->get_type ())
2691 || FLOAT_TYPE_P (rhs
->get_type ())))
2698 return tristate (tristate::TS_TRUE
);
2703 return tristate (tristate::TS_FALSE
);
2709 equiv_class_id
lhs_ec (-1);
2710 equiv_class_id
rhs_ec (-1);
2711 get_equiv_class_by_svalue (lhs
, &lhs_ec
);
2712 get_equiv_class_by_svalue (rhs
, &rhs_ec
);
2713 if (!lhs_ec
.null_p () && !rhs_ec
.null_p ())
2715 tristate result_for_ecs
2716 = eval_condition (lhs_ec
, op
, rhs_ec
);
2717 if (result_for_ecs
.is_known ())
2718 return result_for_ecs
;
2722 && impossible_derived_conditions_p (lhs
, rhs
))
2725 /* If at least one is not in an EC, we have no constraints
2726 comparing LHS and RHS yet.
2727 They might still be comparable if one (or both) is a constant.
2729 Alternatively, we can also get here if we had ECs but they weren't
2730 comparable. Again, constant comparisons might give an answer. */
2731 tree lhs_const
= lhs
->maybe_get_constant ();
2732 tree rhs_const
= rhs
->maybe_get_constant ();
2733 if (lhs_const
&& rhs_const
)
2735 tristate result_for_constants
2736 = compare_constants (lhs_const
, op
, rhs_const
);
2737 if (result_for_constants
.is_known ())
2738 return result_for_constants
;
2741 if (!lhs_ec
.null_p ())
2744 return eval_condition (lhs_ec
, op
, rhs_const
);
2746 if (!rhs_ec
.null_p ())
2750 enum tree_code swapped_op
= swap_tree_comparison (op
);
2751 return eval_condition (rhs_ec
, swapped_op
, lhs_const
);
2755 return tristate (tristate::TS_UNKNOWN
);
2758 /* Delete any information about svalues identified by P.
2759 Such instances are removed from equivalence classes, and any
2760 redundant ECs and constraints are also removed.
2761 Accumulate stats into STATS. */
2763 template <typename PurgeCriteria
>
2765 constraint_manager::purge (const PurgeCriteria
&p
, purge_stats
*stats
)
2767 /* Delete any svalues identified by P within the various equivalence
2769 for (unsigned ec_idx
= 0; ec_idx
< m_equiv_classes
.length (); )
2771 equiv_class
*ec
= m_equiv_classes
[ec_idx
];
2775 bool delete_ec
= false;
2776 FOR_EACH_VEC_ELT (ec
->m_vars
, i
, sval
)
2778 if (sval
== ec
->m_cst_sval
)
2780 if (p
.should_purge_p (sval
))
2783 if (!ec
->m_constant
)
2791 m_equiv_classes
.ordered_remove (ec_idx
);
2793 stats
->m_num_equiv_classes
++;
2795 /* Update the constraints, potentially removing some. */
2796 for (unsigned con_idx
= 0; con_idx
< m_constraints
.length (); )
2798 constraint
*c
= &m_constraints
[con_idx
];
2800 /* Remove constraints that refer to the deleted EC. */
2801 if (c
->m_lhs
== ec_idx
2802 || c
->m_rhs
== ec_idx
)
2804 m_constraints
.ordered_remove (con_idx
);
2806 stats
->m_num_constraints
++;
2810 /* Renumber constraints that refer to ECs that have
2811 had their idx changed. */
2812 c
->m_lhs
.update_for_removal (ec_idx
);
2813 c
->m_rhs
.update_for_removal (ec_idx
);
2819 /* Update bounded_ranges_constraint instances. */
2820 for (unsigned r_idx
= 0;
2821 r_idx
< m_bounded_ranges_constraints
.length (); )
2823 bounded_ranges_constraint
*brc
2824 = &m_bounded_ranges_constraints
[r_idx
];
2826 /* Remove if it refers to the deleted EC. */
2827 if (brc
->m_ec_id
== ec_idx
)
2829 m_bounded_ranges_constraints
.ordered_remove (r_idx
);
2831 stats
->m_num_bounded_ranges_constraints
++;
2835 /* Renumber any EC ids that refer to ECs that have
2836 had their idx changed. */
2837 brc
->m_ec_id
.update_for_removal (ec_idx
);
2846 /* Now delete any constraints that are purely between constants. */
2847 for (unsigned con_idx
= 0; con_idx
< m_constraints
.length (); )
2849 constraint
*c
= &m_constraints
[con_idx
];
2850 if (m_equiv_classes
[c
->m_lhs
.m_idx
]->m_vars
.length () == 0
2851 && m_equiv_classes
[c
->m_rhs
.m_idx
]->m_vars
.length () == 0)
2853 m_constraints
.ordered_remove (con_idx
);
2855 stats
->m_num_constraints
++;
2863 /* Finally, delete any ECs that purely contain constants and aren't
2864 referenced by any constraints. */
2865 for (unsigned ec_idx
= 0; ec_idx
< m_equiv_classes
.length (); )
2867 equiv_class
*ec
= m_equiv_classes
[ec_idx
];
2868 if (ec
->m_vars
.length () == 0)
2870 equiv_class_id
ec_id (ec_idx
);
2871 bool has_constraint
= false;
2872 for (unsigned con_idx
= 0; con_idx
< m_constraints
.length ();
2875 constraint
*c
= &m_constraints
[con_idx
];
2876 if (c
->m_lhs
== ec_id
2877 || c
->m_rhs
== ec_id
)
2879 has_constraint
= true;
2883 if (!has_constraint
)
2886 m_equiv_classes
.ordered_remove (ec_idx
);
2888 stats
->m_num_equiv_classes
++;
2890 /* Renumber constraints that refer to ECs that have
2891 had their idx changed. */
2892 for (unsigned con_idx
= 0; con_idx
< m_constraints
.length ();
2895 constraint
*c
= &m_constraints
[con_idx
];
2896 c
->m_lhs
.update_for_removal (ec_idx
);
2897 c
->m_rhs
.update_for_removal (ec_idx
);
2900 /* Likewise for m_bounded_ranges_constraints. */
2901 for (unsigned r_idx
= 0;
2902 r_idx
< m_bounded_ranges_constraints
.length ();
2905 bounded_ranges_constraint
*brc
2906 = &m_bounded_ranges_constraints
[r_idx
];
2907 brc
->m_ec_id
.update_for_removal (ec_idx
);
2919 /* Implementation of PurgeCriteria: purge svalues that are not live
2920 with respect to LIVE_SVALUES and MODEL. */
2922 class dead_svalue_purger
2925 dead_svalue_purger (const svalue_set
&live_svalues
,
2926 const region_model
*model
)
2927 : m_live_svalues (live_svalues
), m_model (model
)
2931 bool should_purge_p (const svalue
*sval
) const
2933 return !sval
->live_p (&m_live_svalues
, m_model
);
2937 const svalue_set
&m_live_svalues
;
2938 const region_model
*m_model
;
2941 /* Purge dead svalues from equivalence classes and update constraints
2945 constraint_manager::
2946 on_liveness_change (const svalue_set
&live_svalues
,
2947 const region_model
*model
)
2949 dead_svalue_purger
p (live_svalues
, model
);
2956 svalue_purger (const svalue
*sval
) : m_sval (sval
) {}
2958 bool should_purge_p (const svalue
*sval
) const
2960 return sval
->involves_p (m_sval
);
2964 const svalue
*m_sval
;
2967 /* Purge any state involving SVAL. */
2970 constraint_manager::purge_state_involving (const svalue
*sval
)
2972 svalue_purger
p (sval
);
2976 /* Comparator for use by constraint_manager::canonicalize.
2977 Sort a pair of equiv_class instances, using the representative
2978 svalue as a sort key. */
2981 equiv_class_cmp (const void *p1
, const void *p2
)
2983 const equiv_class
*ec1
= *(const equiv_class
* const *)p1
;
2984 const equiv_class
*ec2
= *(const equiv_class
* const *)p2
;
2986 const svalue
*rep1
= ec1
->get_representative ();
2987 const svalue
*rep2
= ec2
->get_representative ();
2992 return svalue::cmp_ptr (rep1
, rep2
);
2995 /* Comparator for use by constraint_manager::canonicalize.
2996 Sort a pair of constraint instances. */
2999 constraint_cmp (const void *p1
, const void *p2
)
3001 const constraint
*c1
= (const constraint
*)p1
;
3002 const constraint
*c2
= (const constraint
*)p2
;
3003 int lhs_cmp
= c1
->m_lhs
.as_int () - c2
->m_lhs
.as_int ();
3006 int rhs_cmp
= c1
->m_rhs
.as_int () - c2
->m_rhs
.as_int ();
3009 return c1
->m_op
- c2
->m_op
;
3012 /* Purge redundant equivalence classes and constraints, and reorder them
3013 within this constraint_manager into a canonical order, to increase the
3014 chances of finding equality with another instance. */
3017 constraint_manager::canonicalize ()
3019 /* First, sort svalues within the ECs. */
3022 FOR_EACH_VEC_ELT (m_equiv_classes
, i
, ec
)
3023 ec
->canonicalize ();
3025 /* TODO: remove constraints where both sides have a constant, and are
3026 thus implicit. But does this break transitivity? */
3028 /* We will be purging and reordering ECs.
3029 We will need to remap the equiv_class_ids in the constraints,
3030 so we need to store the original index of each EC.
3031 Build a lookup table, mapping from the representative svalue
3032 to the original equiv_class_id of that svalue. */
3033 hash_map
<const svalue
*, equiv_class_id
> original_ec_id
;
3034 const unsigned orig_num_equiv_classes
= m_equiv_classes
.length ();
3035 FOR_EACH_VEC_ELT (m_equiv_classes
, i
, ec
)
3037 const svalue
*rep
= ec
->get_representative ();
3039 original_ec_id
.put (rep
, i
);
3042 /* Find ECs used by constraints. */
3043 hash_set
<const equiv_class
*> used_ecs
;
3045 FOR_EACH_VEC_ELT (m_constraints
, i
, c
)
3047 used_ecs
.add (m_equiv_classes
[c
->m_lhs
.as_int ()]);
3048 used_ecs
.add (m_equiv_classes
[c
->m_rhs
.as_int ()]);
3051 for (const auto &iter
: m_bounded_ranges_constraints
)
3052 used_ecs
.add (m_equiv_classes
[iter
.m_ec_id
.as_int ()]);
3054 /* Purge unused ECs: those that aren't used by constraints and
3055 that effectively have only one svalue (either in m_constant
3058 /* "unordered remove if" from a vec. */
3060 while (i
< m_equiv_classes
.length ())
3062 equiv_class
*ec
= m_equiv_classes
[i
];
3063 if (!used_ecs
.contains (ec
)
3064 && !ec
->contains_non_constant_p ())
3066 m_equiv_classes
.unordered_remove (i
);
3074 /* Next, sort the surviving ECs into a canonical order. */
3075 m_equiv_classes
.qsort (equiv_class_cmp
);
3077 /* Populate ec_id_map based on the old vs new EC ids. */
3078 one_way_id_map
<equiv_class_id
> ec_id_map (orig_num_equiv_classes
);
3079 FOR_EACH_VEC_ELT (m_equiv_classes
, i
, ec
)
3081 const svalue
*rep
= ec
->get_representative ();
3083 ec_id_map
.put (*original_ec_id
.get (rep
), i
);
3086 /* Use ec_id_map to update the EC ids within the constraints. */
3087 FOR_EACH_VEC_ELT (m_constraints
, i
, c
)
3089 ec_id_map
.update (&c
->m_lhs
);
3090 ec_id_map
.update (&c
->m_rhs
);
3093 for (auto &iter
: m_bounded_ranges_constraints
)
3094 ec_id_map
.update (&iter
.m_ec_id
);
3096 /* Finally, sort the constraints. */
3097 m_constraints
.qsort (constraint_cmp
);
3100 /* Concrete subclass of fact_visitor for use by constraint_manager::merge.
3101 For every fact in CM_A, see if it is also true in *CM_B. Add such
3104 class merger_fact_visitor
: public fact_visitor
3107 merger_fact_visitor (const constraint_manager
*cm_b
,
3108 constraint_manager
*out
)
3109 : m_cm_b (cm_b
), m_out (out
)
3112 void on_fact (const svalue
*lhs
, enum tree_code code
, const svalue
*rhs
)
3115 /* Special-case for widening. */
3116 if (lhs
->get_kind () == SK_WIDENING
)
3117 if (!m_cm_b
->get_equiv_class_by_svalue (lhs
, NULL
))
3119 /* LHS isn't constrained within m_cm_b. */
3120 bool sat
= m_out
->add_constraint (lhs
, code
, rhs
);
3125 if (m_cm_b
->eval_condition (lhs
, code
, rhs
).is_true ())
3127 bool sat
= m_out
->add_constraint (lhs
, code
, rhs
);
3130 /* If -fanalyzer-transitivity is off, we can encounter cases
3131 where at least one of the two constraint_managers being merged
3132 is infeasible, but we only discover that infeasibility
3133 during merging (PR analyzer/96650).
3134 Silently drop such constraints. */
3135 gcc_assert (!flag_analyzer_transitivity
);
3140 void on_ranges (const svalue
*lhs_sval
,
3141 const bounded_ranges
*ranges
) final override
3143 for (const auto &iter
: m_cm_b
->m_bounded_ranges_constraints
)
3145 const equiv_class
&ec_rhs
= iter
.m_ec_id
.get_obj (*m_cm_b
);
3146 for (unsigned i
= 0; i
< ec_rhs
.m_vars
.length (); i
++)
3148 const svalue
*rhs_sval
= ec_rhs
.m_vars
[i
];
3149 if (lhs_sval
== rhs_sval
)
3151 /* Union of the two ranges. */
3152 auto_vec
<const bounded_ranges
*> pair (2);
3153 pair
.quick_push (ranges
);
3154 pair
.quick_push (iter
.m_ranges
);
3155 bounded_ranges_manager
*ranges_mgr
3156 = m_cm_b
->get_range_manager ();
3157 const bounded_ranges
*union_
3158 = ranges_mgr
->get_or_create_union (pair
);
3159 bool sat
= m_out
->add_bounded_ranges (lhs_sval
, union_
);
3167 const constraint_manager
*m_cm_b
;
3168 constraint_manager
*m_out
;
3171 /* Use MERGER to merge CM_A and CM_B into *OUT.
3172 If one thinks of a constraint_manager as a subset of N-dimensional
3173 space, this takes the union of the points of CM_A and CM_B, and
3174 expresses that into *OUT. Alternatively, it can be thought of
3175 as the intersection of the constraints. */
3178 constraint_manager::merge (const constraint_manager
&cm_a
,
3179 const constraint_manager
&cm_b
,
3180 constraint_manager
*out
)
3182 /* Merge the equivalence classes and constraints.
3183 The easiest way to do this seems to be to enumerate all of the facts
3184 in cm_a, see which are also true in cm_b,
3185 and add those to *OUT. */
3186 merger_fact_visitor
v (&cm_b
, out
);
3187 cm_a
.for_each_fact (&v
);
3190 /* Call VISITOR's on_fact vfunc repeatedly to express the various
3191 equivalence classes and constraints.
3192 This is used by constraint_manager::merge to find the common
3193 facts between two input constraint_managers. */
3196 constraint_manager::for_each_fact (fact_visitor
*visitor
) const
3198 /* First, call EQ_EXPR within the various equivalence classes. */
3201 FOR_EACH_VEC_ELT (m_equiv_classes
, ec_idx
, ec
)
3207 FOR_EACH_VEC_ELT (ec
->m_vars
, i
, sval
)
3208 visitor
->on_fact (ec
->m_cst_sval
, EQ_EXPR
, sval
);
3210 for (unsigned i
= 0; i
< ec
->m_vars
.length (); i
++)
3211 for (unsigned j
= i
+ 1; j
< ec
->m_vars
.length (); j
++)
3212 visitor
->on_fact (ec
->m_vars
[i
], EQ_EXPR
, ec
->m_vars
[j
]);
3215 /* Now, express the various constraints. */
3218 FOR_EACH_VEC_ELT (m_constraints
, con_idx
, c
)
3220 const equiv_class
&ec_lhs
= c
->m_lhs
.get_obj (*this);
3221 const equiv_class
&ec_rhs
= c
->m_rhs
.get_obj (*this);
3222 enum tree_code code
= constraint_tree_code (c
->m_op
);
3224 if (ec_lhs
.m_cst_sval
)
3226 for (unsigned j
= 0; j
< ec_rhs
.m_vars
.length (); j
++)
3228 visitor
->on_fact (ec_lhs
.m_cst_sval
, code
, ec_rhs
.m_vars
[j
]);
3231 for (unsigned i
= 0; i
< ec_lhs
.m_vars
.length (); i
++)
3233 if (ec_rhs
.m_cst_sval
)
3234 visitor
->on_fact (ec_lhs
.m_vars
[i
], code
, ec_rhs
.m_cst_sval
);
3235 for (unsigned j
= 0; j
< ec_rhs
.m_vars
.length (); j
++)
3236 visitor
->on_fact (ec_lhs
.m_vars
[i
], code
, ec_rhs
.m_vars
[j
]);
3240 for (const auto &iter
: m_bounded_ranges_constraints
)
3242 const equiv_class
&ec_lhs
= iter
.m_ec_id
.get_obj (*this);
3243 for (unsigned i
= 0; i
< ec_lhs
.m_vars
.length (); i
++)
3245 const svalue
*lhs_sval
= ec_lhs
.m_vars
[i
];
3246 visitor
->on_ranges (lhs_sval
, iter
.m_ranges
);
3251 /* Subclass of fact_visitor for use by
3252 constraint_manager::replay_call_summary. */
3254 class replay_fact_visitor
: public fact_visitor
3257 replay_fact_visitor (call_summary_replay
&r
,
3258 constraint_manager
*out
)
3259 : m_r (r
), m_out (out
), m_feasible (true)
3262 bool feasible_p () const { return m_feasible
; }
3264 void on_fact (const svalue
*lhs
, enum tree_code code
, const svalue
*rhs
)
3267 const svalue
*caller_lhs
= m_r
.convert_svalue_from_summary (lhs
);
3270 const svalue
*caller_rhs
= m_r
.convert_svalue_from_summary (rhs
);
3273 if (!m_out
->add_constraint (caller_lhs
, code
, caller_rhs
))
3277 void on_ranges (const svalue
*lhs_sval
,
3278 const bounded_ranges
*ranges
) final override
3280 const svalue
*caller_lhs
= m_r
.convert_svalue_from_summary (lhs_sval
);
3283 if (!m_out
->add_bounded_ranges (caller_lhs
, ranges
))
3288 call_summary_replay
&m_r
;
3289 constraint_manager
*m_out
;
3293 /* Attempt to use R to replay the constraints from SUMMARY into this object.
3294 Return true if it is feasible. */
3297 constraint_manager::replay_call_summary (call_summary_replay
&r
,
3298 const constraint_manager
&summary
)
3300 replay_fact_visitor
v (r
, this);
3301 summary
.for_each_fact (&v
);
3302 return v
.feasible_p ();
3305 /* Assert that this object is valid. */
3308 constraint_manager::validate () const
3310 /* Skip this in a release build. */
3317 FOR_EACH_VEC_ELT (m_equiv_classes
, i
, ec
)
3323 FOR_EACH_VEC_ELT (ec
->m_vars
, j
, sval
)
3327 gcc_assert (CONSTANT_CLASS_P (ec
->m_constant
));
3328 gcc_assert (ec
->m_cst_sval
);
3332 gcc_assert (ec
->m_vars
.length () > 0);
3337 FOR_EACH_VEC_ELT (m_constraints
, i
, c
)
3339 gcc_assert (!c
->m_lhs
.null_p ());
3340 gcc_assert (c
->m_lhs
.as_int () < (int)m_equiv_classes
.length ());
3341 gcc_assert (!c
->m_rhs
.null_p ());
3342 gcc_assert (c
->m_rhs
.as_int () < (int)m_equiv_classes
.length ());
3345 for (const auto &iter
: m_bounded_ranges_constraints
)
3347 gcc_assert (!iter
.m_ec_id
.null_p ());
3348 gcc_assert (iter
.m_ec_id
.as_int () < (int)m_equiv_classes
.length ());
3352 bounded_ranges_manager
*
3353 constraint_manager::get_range_manager () const
3355 return m_mgr
->get_range_manager ();
3360 namespace selftest
{
3362 /* Various constraint_manager selftests.
3363 These have to be written in terms of a region_model, since
3364 the latter is responsible for managing svalue instances. */
3366 /* Verify that range::add_bound works as expected. */
3371 tree int_0
= build_int_cst (integer_type_node
, 0);
3372 tree int_1
= build_int_cst (integer_type_node
, 1);
3373 tree int_2
= build_int_cst (integer_type_node
, 2);
3374 tree int_5
= build_int_cst (integer_type_node
, 5);
3378 ASSERT_FALSE (r
.constrained_to_single_element ());
3381 ASSERT_TRUE (r
.add_bound (GE_EXPR
, int_1
));
3384 ASSERT_TRUE (r
.add_bound (GE_EXPR
, int_0
));
3385 ASSERT_TRUE (r
.add_bound (GT_EXPR
, int_0
));
3387 ASSERT_FALSE (r
.constrained_to_single_element ());
3389 /* Contradiction. */
3390 ASSERT_FALSE (r
.add_bound (LT_EXPR
, int_1
));
3393 ASSERT_TRUE (r
.add_bound (LT_EXPR
, int_5
));
3394 ASSERT_FALSE (r
.constrained_to_single_element ());
3396 /* Contradiction. */
3397 ASSERT_FALSE (r
.add_bound (GE_EXPR
, int_5
));
3400 ASSERT_TRUE (r
.add_bound (LT_EXPR
, int_2
));
3401 ASSERT_TRUE (r
.constrained_to_single_element ());
3404 ASSERT_TRUE (r
.add_bound (LE_EXPR
, int_1
));
3405 ASSERT_TRUE (r
.constrained_to_single_element ());
3409 /* Verify that setting and getting simple conditions within a region_model
3410 work (thus exercising the underlying constraint_manager). */
3413 test_constraint_conditions ()
3415 tree int_42
= build_int_cst (integer_type_node
, 42);
3416 tree int_0
= build_int_cst (integer_type_node
, 0);
3418 tree x
= build_global_decl ("x", integer_type_node
);
3419 tree y
= build_global_decl ("y", integer_type_node
);
3420 tree z
= build_global_decl ("z", integer_type_node
);
3422 /* Self-comparisons. */
3424 region_model_manager mgr
;
3425 region_model
model (&mgr
);
3426 ASSERT_CONDITION_TRUE (model
, x
, EQ_EXPR
, x
);
3427 ASSERT_CONDITION_TRUE (model
, x
, LE_EXPR
, x
);
3428 ASSERT_CONDITION_TRUE (model
, x
, GE_EXPR
, x
);
3429 ASSERT_CONDITION_FALSE (model
, x
, NE_EXPR
, x
);
3430 ASSERT_CONDITION_FALSE (model
, x
, LT_EXPR
, x
);
3431 ASSERT_CONDITION_FALSE (model
, x
, GT_EXPR
, x
);
3434 /* Adding self-equality shouldn't add equiv classes. */
3436 region_model_manager mgr
;
3437 region_model
model (&mgr
);
3438 ADD_SAT_CONSTRAINT (model
, x
, EQ_EXPR
, x
);
3439 ADD_SAT_CONSTRAINT (model
, int_42
, EQ_EXPR
, int_42
);
3440 /* ...even when done directly via svalues: */
3441 const svalue
*sval_int_42
= model
.get_rvalue (int_42
, NULL
);
3442 bool sat
= model
.get_constraints ()->add_constraint (sval_int_42
,
3446 ASSERT_EQ (model
.get_constraints ()->m_equiv_classes
.length (), 0);
3451 region_model_manager mgr
;
3452 region_model
model (&mgr
);
3453 ASSERT_CONDITION_UNKNOWN (model
, x
, EQ_EXPR
, y
);
3455 ADD_SAT_CONSTRAINT (model
, x
, EQ_EXPR
, y
);
3457 ASSERT_CONDITION_TRUE (model
, x
, EQ_EXPR
, y
);
3458 ASSERT_CONDITION_TRUE (model
, x
, LE_EXPR
, y
);
3459 ASSERT_CONDITION_TRUE (model
, x
, GE_EXPR
, y
);
3460 ASSERT_CONDITION_FALSE (model
, x
, NE_EXPR
, y
);
3461 ASSERT_CONDITION_FALSE (model
, x
, LT_EXPR
, y
);
3462 ASSERT_CONDITION_FALSE (model
, x
, GT_EXPR
, y
);
3464 /* Swapped operands. */
3465 ASSERT_CONDITION_TRUE (model
, y
, EQ_EXPR
, x
);
3466 ASSERT_CONDITION_TRUE (model
, y
, LE_EXPR
, x
);
3467 ASSERT_CONDITION_TRUE (model
, y
, GE_EXPR
, x
);
3468 ASSERT_CONDITION_FALSE (model
, y
, NE_EXPR
, x
);
3469 ASSERT_CONDITION_FALSE (model
, y
, LT_EXPR
, x
);
3470 ASSERT_CONDITION_FALSE (model
, y
, GT_EXPR
, x
);
3472 /* Comparison with other var. */
3473 ASSERT_CONDITION_UNKNOWN (model
, x
, EQ_EXPR
, z
);
3474 ASSERT_CONDITION_UNKNOWN (model
, x
, LE_EXPR
, z
);
3475 ASSERT_CONDITION_UNKNOWN (model
, x
, GE_EXPR
, z
);
3476 ASSERT_CONDITION_UNKNOWN (model
, x
, NE_EXPR
, z
);
3477 ASSERT_CONDITION_UNKNOWN (model
, x
, LT_EXPR
, z
);
3478 ASSERT_CONDITION_UNKNOWN (model
, x
, GT_EXPR
, z
);
3481 /* x == y, then y == z */
3483 region_model_manager mgr
;
3484 region_model
model (&mgr
);
3485 ASSERT_CONDITION_UNKNOWN (model
, x
, EQ_EXPR
, y
);
3487 ADD_SAT_CONSTRAINT (model
, x
, EQ_EXPR
, y
);
3488 ADD_SAT_CONSTRAINT (model
, y
, EQ_EXPR
, z
);
3490 ASSERT_CONDITION_TRUE (model
, x
, EQ_EXPR
, z
);
3491 ASSERT_CONDITION_TRUE (model
, x
, LE_EXPR
, z
);
3492 ASSERT_CONDITION_TRUE (model
, x
, GE_EXPR
, z
);
3493 ASSERT_CONDITION_FALSE (model
, x
, NE_EXPR
, z
);
3494 ASSERT_CONDITION_FALSE (model
, x
, LT_EXPR
, z
);
3495 ASSERT_CONDITION_FALSE (model
, x
, GT_EXPR
, z
);
3500 region_model_manager mgr
;
3501 region_model
model (&mgr
);
3503 ADD_SAT_CONSTRAINT (model
, x
, NE_EXPR
, y
);
3505 ASSERT_CONDITION_TRUE (model
, x
, NE_EXPR
, y
);
3506 ASSERT_CONDITION_FALSE (model
, x
, EQ_EXPR
, y
);
3507 ASSERT_CONDITION_UNKNOWN (model
, x
, LE_EXPR
, y
);
3508 ASSERT_CONDITION_UNKNOWN (model
, x
, GE_EXPR
, y
);
3509 ASSERT_CONDITION_UNKNOWN (model
, x
, LT_EXPR
, y
);
3510 ASSERT_CONDITION_UNKNOWN (model
, x
, GT_EXPR
, y
);
3512 /* Swapped operands. */
3513 ASSERT_CONDITION_TRUE (model
, y
, NE_EXPR
, x
);
3514 ASSERT_CONDITION_FALSE (model
, y
, EQ_EXPR
, x
);
3515 ASSERT_CONDITION_UNKNOWN (model
, y
, LE_EXPR
, x
);
3516 ASSERT_CONDITION_UNKNOWN (model
, y
, GE_EXPR
, x
);
3517 ASSERT_CONDITION_UNKNOWN (model
, y
, LT_EXPR
, x
);
3518 ASSERT_CONDITION_UNKNOWN (model
, y
, GT_EXPR
, x
);
3520 /* Comparison with other var. */
3521 ASSERT_CONDITION_UNKNOWN (model
, x
, EQ_EXPR
, z
);
3522 ASSERT_CONDITION_UNKNOWN (model
, x
, LE_EXPR
, z
);
3523 ASSERT_CONDITION_UNKNOWN (model
, x
, GE_EXPR
, z
);
3524 ASSERT_CONDITION_UNKNOWN (model
, x
, NE_EXPR
, z
);
3525 ASSERT_CONDITION_UNKNOWN (model
, x
, LT_EXPR
, z
);
3526 ASSERT_CONDITION_UNKNOWN (model
, x
, GT_EXPR
, z
);
3531 region_model_manager mgr
;
3532 region_model
model (&mgr
);
3534 ADD_SAT_CONSTRAINT (model
, x
, LT_EXPR
, y
);
3536 ASSERT_CONDITION_TRUE (model
, x
, LT_EXPR
, y
);
3537 ASSERT_CONDITION_TRUE (model
, x
, LE_EXPR
, y
);
3538 ASSERT_CONDITION_TRUE (model
, x
, NE_EXPR
, y
);
3539 ASSERT_CONDITION_FALSE (model
, x
, EQ_EXPR
, y
);
3540 ASSERT_CONDITION_FALSE (model
, x
, GT_EXPR
, y
);
3541 ASSERT_CONDITION_FALSE (model
, x
, GE_EXPR
, y
);
3543 /* Swapped operands. */
3544 ASSERT_CONDITION_FALSE (model
, y
, LT_EXPR
, x
);
3545 ASSERT_CONDITION_FALSE (model
, y
, LE_EXPR
, x
);
3546 ASSERT_CONDITION_TRUE (model
, y
, NE_EXPR
, x
);
3547 ASSERT_CONDITION_FALSE (model
, y
, EQ_EXPR
, x
);
3548 ASSERT_CONDITION_TRUE (model
, y
, GT_EXPR
, x
);
3549 ASSERT_CONDITION_TRUE (model
, y
, GE_EXPR
, x
);
3554 region_model_manager mgr
;
3555 region_model
model (&mgr
);
3557 ADD_SAT_CONSTRAINT (model
, x
, LE_EXPR
, y
);
3559 ASSERT_CONDITION_UNKNOWN (model
, x
, LT_EXPR
, y
);
3560 ASSERT_CONDITION_TRUE (model
, x
, LE_EXPR
, y
);
3561 ASSERT_CONDITION_UNKNOWN (model
, x
, NE_EXPR
, y
);
3562 ASSERT_CONDITION_UNKNOWN (model
, x
, EQ_EXPR
, y
);
3563 ASSERT_CONDITION_FALSE (model
, x
, GT_EXPR
, y
);
3564 ASSERT_CONDITION_UNKNOWN (model
, x
, GE_EXPR
, y
);
3566 /* Swapped operands. */
3567 ASSERT_CONDITION_FALSE (model
, y
, LT_EXPR
, x
);
3568 ASSERT_CONDITION_UNKNOWN (model
, y
, LE_EXPR
, x
);
3569 ASSERT_CONDITION_UNKNOWN (model
, y
, NE_EXPR
, x
);
3570 ASSERT_CONDITION_UNKNOWN (model
, y
, EQ_EXPR
, x
);
3571 ASSERT_CONDITION_UNKNOWN (model
, y
, GT_EXPR
, x
);
3572 ASSERT_CONDITION_TRUE (model
, y
, GE_EXPR
, x
);
3577 region_model_manager mgr
;
3578 region_model
model (&mgr
);
3580 ADD_SAT_CONSTRAINT (model
, x
, GT_EXPR
, y
);
3582 ASSERT_CONDITION_TRUE (model
, x
, GT_EXPR
, y
);
3583 ASSERT_CONDITION_TRUE (model
, x
, GE_EXPR
, y
);
3584 ASSERT_CONDITION_TRUE (model
, x
, NE_EXPR
, y
);
3585 ASSERT_CONDITION_FALSE (model
, x
, EQ_EXPR
, y
);
3586 ASSERT_CONDITION_FALSE (model
, x
, LT_EXPR
, y
);
3587 ASSERT_CONDITION_FALSE (model
, x
, LE_EXPR
, y
);
3589 /* Swapped operands. */
3590 ASSERT_CONDITION_FALSE (model
, y
, GT_EXPR
, x
);
3591 ASSERT_CONDITION_FALSE (model
, y
, GE_EXPR
, x
);
3592 ASSERT_CONDITION_TRUE (model
, y
, NE_EXPR
, x
);
3593 ASSERT_CONDITION_FALSE (model
, y
, EQ_EXPR
, x
);
3594 ASSERT_CONDITION_TRUE (model
, y
, LT_EXPR
, x
);
3595 ASSERT_CONDITION_TRUE (model
, y
, LE_EXPR
, x
);
3600 region_model_manager mgr
;
3601 region_model
model (&mgr
);
3603 ADD_SAT_CONSTRAINT (model
, x
, GE_EXPR
, y
);
3605 ASSERT_CONDITION_UNKNOWN (model
, x
, GT_EXPR
, y
);
3606 ASSERT_CONDITION_TRUE (model
, x
, GE_EXPR
, y
);
3607 ASSERT_CONDITION_UNKNOWN (model
, x
, NE_EXPR
, y
);
3608 ASSERT_CONDITION_UNKNOWN (model
, x
, EQ_EXPR
, y
);
3609 ASSERT_CONDITION_FALSE (model
, x
, LT_EXPR
, y
);
3610 ASSERT_CONDITION_UNKNOWN (model
, x
, LE_EXPR
, y
);
3612 /* Swapped operands. */
3613 ASSERT_CONDITION_FALSE (model
, y
, GT_EXPR
, x
);
3614 ASSERT_CONDITION_UNKNOWN (model
, y
, GE_EXPR
, x
);
3615 ASSERT_CONDITION_UNKNOWN (model
, y
, NE_EXPR
, x
);
3616 ASSERT_CONDITION_UNKNOWN (model
, y
, EQ_EXPR
, x
);
3617 ASSERT_CONDITION_UNKNOWN (model
, y
, LT_EXPR
, x
);
3618 ASSERT_CONDITION_TRUE (model
, y
, LE_EXPR
, x
);
3621 // TODO: implied orderings
3625 region_model_manager mgr
;
3626 region_model
model (&mgr
);
3627 ASSERT_CONDITION_FALSE (model
, int_0
, EQ_EXPR
, int_42
);
3628 ASSERT_CONDITION_TRUE (model
, int_0
, NE_EXPR
, int_42
);
3629 ASSERT_CONDITION_TRUE (model
, int_0
, LT_EXPR
, int_42
);
3630 ASSERT_CONDITION_TRUE (model
, int_0
, LE_EXPR
, int_42
);
3631 ASSERT_CONDITION_FALSE (model
, int_0
, GT_EXPR
, int_42
);
3632 ASSERT_CONDITION_FALSE (model
, int_0
, GE_EXPR
, int_42
);
3635 /* x == 0, y == 42. */
3637 region_model_manager mgr
;
3638 region_model
model (&mgr
);
3639 ADD_SAT_CONSTRAINT (model
, x
, EQ_EXPR
, int_0
);
3640 ADD_SAT_CONSTRAINT (model
, y
, EQ_EXPR
, int_42
);
3642 ASSERT_CONDITION_TRUE (model
, x
, NE_EXPR
, y
);
3643 ASSERT_CONDITION_FALSE (model
, x
, EQ_EXPR
, y
);
3644 ASSERT_CONDITION_TRUE (model
, x
, LE_EXPR
, y
);
3645 ASSERT_CONDITION_FALSE (model
, x
, GE_EXPR
, y
);
3646 ASSERT_CONDITION_TRUE (model
, x
, LT_EXPR
, y
);
3647 ASSERT_CONDITION_FALSE (model
, x
, GT_EXPR
, y
);
3650 /* Unsatisfiable combinations. */
3652 /* x == y && x != y. */
3654 region_model_manager mgr
;
3655 region_model
model (&mgr
);
3656 ADD_SAT_CONSTRAINT (model
, x
, EQ_EXPR
, y
);
3657 ADD_UNSAT_CONSTRAINT (model
, x
, NE_EXPR
, y
);
3660 /* x == 0 then x == 42. */
3662 region_model_manager mgr
;
3663 region_model
model (&mgr
);
3664 ADD_SAT_CONSTRAINT (model
, x
, EQ_EXPR
, int_0
);
3665 ADD_UNSAT_CONSTRAINT (model
, x
, EQ_EXPR
, int_42
);
3668 /* x == 0 then x != 0. */
3670 region_model_manager mgr
;
3671 region_model
model (&mgr
);
3672 ADD_SAT_CONSTRAINT (model
, x
, EQ_EXPR
, int_0
);
3673 ADD_UNSAT_CONSTRAINT (model
, x
, NE_EXPR
, int_0
);
3676 /* x == 0 then x > 0. */
3678 region_model_manager mgr
;
3679 region_model
model (&mgr
);
3680 ADD_SAT_CONSTRAINT (model
, x
, EQ_EXPR
, int_0
);
3681 ADD_UNSAT_CONSTRAINT (model
, x
, GT_EXPR
, int_0
);
3684 /* x != y && x == y. */
3686 region_model_manager mgr
;
3687 region_model
model (&mgr
);
3688 ADD_SAT_CONSTRAINT (model
, x
, NE_EXPR
, y
);
3689 ADD_UNSAT_CONSTRAINT (model
, x
, EQ_EXPR
, y
);
3692 /* x <= y && x > y. */
3694 region_model_manager mgr
;
3695 region_model
model (&mgr
);
3696 ADD_SAT_CONSTRAINT (model
, x
, LE_EXPR
, y
);
3697 ADD_UNSAT_CONSTRAINT (model
, x
, GT_EXPR
, y
);
3703 /* Test transitivity of conditions. */
3706 test_transitivity ()
3708 tree a
= build_global_decl ("a", integer_type_node
);
3709 tree b
= build_global_decl ("b", integer_type_node
);
3710 tree c
= build_global_decl ("c", integer_type_node
);
3711 tree d
= build_global_decl ("d", integer_type_node
);
3713 /* a == b, then c == d, then c == b. */
3715 region_model_manager mgr
;
3716 region_model
model (&mgr
);
3717 ASSERT_CONDITION_UNKNOWN (model
, a
, EQ_EXPR
, b
);
3718 ASSERT_CONDITION_UNKNOWN (model
, b
, EQ_EXPR
, c
);
3719 ASSERT_CONDITION_UNKNOWN (model
, c
, EQ_EXPR
, d
);
3720 ASSERT_CONDITION_UNKNOWN (model
, a
, EQ_EXPR
, d
);
3722 ADD_SAT_CONSTRAINT (model
, a
, EQ_EXPR
, b
);
3723 ASSERT_CONDITION_TRUE (model
, a
, EQ_EXPR
, b
);
3725 ADD_SAT_CONSTRAINT (model
, c
, EQ_EXPR
, d
);
3726 ASSERT_CONDITION_TRUE (model
, c
, EQ_EXPR
, d
);
3727 ASSERT_CONDITION_UNKNOWN (model
, a
, EQ_EXPR
, d
);
3729 ADD_SAT_CONSTRAINT (model
, c
, EQ_EXPR
, b
);
3730 ASSERT_CONDITION_TRUE (model
, c
, EQ_EXPR
, b
);
3731 ASSERT_CONDITION_TRUE (model
, a
, EQ_EXPR
, d
);
3734 /* Transitivity: "a < b", "b < c" should imply "a < c". */
3736 region_model_manager mgr
;
3737 region_model
model (&mgr
);
3738 ADD_SAT_CONSTRAINT (model
, a
, LT_EXPR
, b
);
3739 ADD_SAT_CONSTRAINT (model
, b
, LT_EXPR
, c
);
3741 ASSERT_CONDITION_TRUE (model
, a
, LT_EXPR
, c
);
3742 ASSERT_CONDITION_FALSE (model
, a
, EQ_EXPR
, c
);
3745 /* Transitivity: "a <= b", "b < c" should imply "a < c". */
3747 region_model_manager mgr
;
3748 region_model
model (&mgr
);
3749 ADD_SAT_CONSTRAINT (model
, a
, LE_EXPR
, b
);
3750 ADD_SAT_CONSTRAINT (model
, b
, LT_EXPR
, c
);
3752 ASSERT_CONDITION_TRUE (model
, a
, LT_EXPR
, c
);
3753 ASSERT_CONDITION_FALSE (model
, a
, EQ_EXPR
, c
);
3756 /* Transitivity: "a <= b", "b <= c" should imply "a <= c". */
3758 region_model_manager mgr
;
3759 region_model
model (&mgr
);
3760 ADD_SAT_CONSTRAINT (model
, a
, LE_EXPR
, b
);
3761 ADD_SAT_CONSTRAINT (model
, b
, LE_EXPR
, c
);
3763 ASSERT_CONDITION_TRUE (model
, a
, LE_EXPR
, c
);
3764 ASSERT_CONDITION_UNKNOWN (model
, a
, EQ_EXPR
, c
);
3767 /* Transitivity: "a > b", "b > c" should imply "a > c". */
3769 region_model_manager mgr
;
3770 region_model
model (&mgr
);
3771 ADD_SAT_CONSTRAINT (model
, a
, GT_EXPR
, b
);
3772 ADD_SAT_CONSTRAINT (model
, b
, GT_EXPR
, c
);
3774 ASSERT_CONDITION_TRUE (model
, a
, GT_EXPR
, c
);
3775 ASSERT_CONDITION_FALSE (model
, a
, EQ_EXPR
, c
);
3778 /* Transitivity: "a >= b", "b > c" should imply " a > c". */
3780 region_model_manager mgr
;
3781 region_model
model (&mgr
);
3782 ADD_SAT_CONSTRAINT (model
, a
, GE_EXPR
, b
);
3783 ADD_SAT_CONSTRAINT (model
, b
, GT_EXPR
, c
);
3785 ASSERT_CONDITION_TRUE (model
, a
, GT_EXPR
, c
);
3786 ASSERT_CONDITION_FALSE (model
, a
, EQ_EXPR
, c
);
3789 /* Transitivity: "a >= b", "b >= c" should imply "a >= c". */
3791 region_model_manager mgr
;
3792 region_model
model (&mgr
);
3793 ADD_SAT_CONSTRAINT (model
, a
, GE_EXPR
, b
);
3794 ADD_SAT_CONSTRAINT (model
, b
, GE_EXPR
, c
);
3796 ASSERT_CONDITION_TRUE (model
, a
, GE_EXPR
, c
);
3797 ASSERT_CONDITION_UNKNOWN (model
, a
, EQ_EXPR
, c
);
3800 /* Transitivity: "(a < b)", "(c < d)", "(b < c)" should
3801 imply the easy cases:
3807 region_model_manager mgr
;
3808 region_model
model (&mgr
);
3809 ADD_SAT_CONSTRAINT (model
, a
, LT_EXPR
, b
);
3810 ADD_SAT_CONSTRAINT (model
, c
, LT_EXPR
, d
);
3811 ADD_SAT_CONSTRAINT (model
, b
, LT_EXPR
, c
);
3813 ASSERT_CONDITION_TRUE (model
, a
, LT_EXPR
, c
);
3814 ASSERT_CONDITION_TRUE (model
, b
, LT_EXPR
, d
);
3815 ASSERT_CONDITION_TRUE (model
, a
, LT_EXPR
, d
);
3818 /* Transitivity: "a >= b", "b >= a" should imply that a == b. */
3820 region_model_manager mgr
;
3821 region_model
model (&mgr
);
3822 ADD_SAT_CONSTRAINT (model
, a
, GE_EXPR
, b
);
3823 ADD_SAT_CONSTRAINT (model
, b
, GE_EXPR
, a
);
3826 ASSERT_CONDITION_TRUE (model
, a
, EQ_EXPR
, b
);
3828 /* The ECs for a and b should have merged, and any constraints removed. */
3829 ASSERT_EQ (model
.get_constraints ()->m_equiv_classes
.length (), 1);
3830 ASSERT_EQ (model
.get_constraints ()->m_constraints
.length (), 0);
3833 /* Transitivity: "a >= b", "b > a" should be impossible. */
3835 region_model_manager mgr
;
3836 region_model
model (&mgr
);
3837 ADD_SAT_CONSTRAINT (model
, a
, GE_EXPR
, b
);
3838 ADD_UNSAT_CONSTRAINT (model
, b
, GT_EXPR
, a
);
3841 /* Transitivity: "a >= b", "b >= c", "c >= a" should imply
3842 that a == b == c. */
3844 region_model_manager mgr
;
3845 region_model
model (&mgr
);
3846 ADD_SAT_CONSTRAINT (model
, a
, GE_EXPR
, b
);
3847 ADD_SAT_CONSTRAINT (model
, b
, GE_EXPR
, c
);
3848 ADD_SAT_CONSTRAINT (model
, c
, GE_EXPR
, a
);
3850 ASSERT_CONDITION_TRUE (model
, a
, EQ_EXPR
, c
);
3853 /* Transitivity: "a > b", "b > c", "c > a"
3854 should be impossible. */
3856 region_model_manager mgr
;
3857 region_model
model (&mgr
);
3858 ADD_SAT_CONSTRAINT (model
, a
, GT_EXPR
, b
);
3859 ADD_SAT_CONSTRAINT (model
, b
, GT_EXPR
, c
);
3860 ADD_UNSAT_CONSTRAINT (model
, c
, GT_EXPR
, a
);
3865 /* Test various conditionals involving constants where the results
3866 ought to be implied based on the values of the constants. */
3869 test_constant_comparisons ()
3871 tree int_1
= build_int_cst (integer_type_node
, 1);
3872 tree int_3
= build_int_cst (integer_type_node
, 3);
3873 tree int_4
= build_int_cst (integer_type_node
, 4);
3874 tree int_5
= build_int_cst (integer_type_node
, 5);
3876 tree int_1023
= build_int_cst (integer_type_node
, 1023);
3877 tree int_1024
= build_int_cst (integer_type_node
, 1024);
3879 tree a
= build_global_decl ("a", integer_type_node
);
3880 tree b
= build_global_decl ("b", integer_type_node
);
3882 tree a_plus_one
= build2 (PLUS_EXPR
, integer_type_node
, a
, int_1
);
3884 /* Given a >= 1024, then a <= 1023 should be impossible. */
3886 region_model_manager mgr
;
3887 region_model
model (&mgr
);
3888 ADD_SAT_CONSTRAINT (model
, a
, GE_EXPR
, int_1024
);
3889 ADD_UNSAT_CONSTRAINT (model
, a
, LE_EXPR
, int_1023
);
3894 region_model_manager mgr
;
3895 region_model
model (&mgr
);
3896 ADD_SAT_CONSTRAINT (model
, a
, GT_EXPR
, int_4
);
3897 ASSERT_CONDITION_TRUE (model
, a
, GT_EXPR
, int_4
);
3898 ASSERT_CONDITION_TRUE (model
, a
, NE_EXPR
, int_3
);
3899 ASSERT_CONDITION_UNKNOWN (model
, a
, NE_EXPR
, int_5
);
3904 region_model_manager mgr
;
3905 region_model
model (&mgr
);
3906 ADD_SAT_CONSTRAINT (model
, a
, LE_EXPR
, int_4
);
3907 ASSERT_CONDITION_FALSE (model
, a
, GT_EXPR
, int_4
);
3908 ASSERT_CONDITION_FALSE (model
, a
, GT_EXPR
, int_5
);
3909 ASSERT_CONDITION_UNKNOWN (model
, a
, NE_EXPR
, int_3
);
3912 /* If "a > b" and "a == 3", then "b == 4" ought to be unsatisfiable. */
3914 region_model_manager mgr
;
3915 region_model
model (&mgr
);
3916 ADD_SAT_CONSTRAINT (model
, a
, GT_EXPR
, b
);
3917 ADD_SAT_CONSTRAINT (model
, a
, EQ_EXPR
, int_3
);
3918 ADD_UNSAT_CONSTRAINT (model
, b
, EQ_EXPR
, int_4
);
3921 /* Various tests of int ranges where there is only one possible candidate. */
3923 /* If "a <= 4" && "a > 3", then "a == 4",
3924 assuming a is of integral type. */
3926 region_model_manager mgr
;
3927 region_model
model (&mgr
);
3928 ADD_SAT_CONSTRAINT (model
, a
, LE_EXPR
, int_4
);
3929 ADD_SAT_CONSTRAINT (model
, a
, GT_EXPR
, int_3
);
3930 ASSERT_CONDITION_TRUE (model
, a
, EQ_EXPR
, int_4
);
3933 /* If "a > 3" && "a <= 4", then "a == 4",
3934 assuming a is of integral type. */
3936 region_model_manager mgr
;
3937 region_model
model (&mgr
);
3938 ADD_SAT_CONSTRAINT (model
, a
, GT_EXPR
, int_3
);
3939 ADD_SAT_CONSTRAINT (model
, a
, LE_EXPR
, int_4
);
3940 ASSERT_CONDITION_TRUE (model
, a
, EQ_EXPR
, int_4
);
3942 /* If "a > 3" && "a < 5", then "a == 4",
3943 assuming a is of integral type. */
3945 region_model_manager mgr
;
3946 region_model
model (&mgr
);
3947 ADD_SAT_CONSTRAINT (model
, a
, GT_EXPR
, int_3
);
3948 ADD_SAT_CONSTRAINT (model
, a
, LT_EXPR
, int_5
);
3949 ASSERT_CONDITION_TRUE (model
, a
, EQ_EXPR
, int_4
);
3951 /* If "a >= 4" && "a < 5", then "a == 4",
3952 assuming a is of integral type. */
3954 region_model_manager mgr
;
3955 region_model
model (&mgr
);
3956 ADD_SAT_CONSTRAINT (model
, a
, GE_EXPR
, int_4
);
3957 ADD_SAT_CONSTRAINT (model
, a
, LT_EXPR
, int_5
);
3958 ASSERT_CONDITION_TRUE (model
, a
, EQ_EXPR
, int_4
);
3960 /* If "a >= 4" && "a <= 4", then "a == 4". */
3962 region_model_manager mgr
;
3963 region_model
model (&mgr
);
3964 ADD_SAT_CONSTRAINT (model
, a
, GE_EXPR
, int_4
);
3965 ADD_SAT_CONSTRAINT (model
, a
, LE_EXPR
, int_4
);
3966 ASSERT_CONDITION_TRUE (model
, a
, EQ_EXPR
, int_4
);
3970 /* As above, but for floating-point:
3971 if "f > 3" && "f <= 4" we don't know that f == 4. */
3973 tree f
= build_global_decl ("f", double_type_node
);
3974 tree float_3
= build_real_from_int_cst (double_type_node
, int_3
);
3975 tree float_4
= build_real_from_int_cst (double_type_node
, int_4
);
3977 region_model_manager mgr
;
3978 region_model
model (&mgr
);
3979 ADD_SAT_CONSTRAINT (model
, f
, GT_EXPR
, float_3
);
3980 ADD_SAT_CONSTRAINT (model
, f
, LE_EXPR
, float_4
);
3981 ASSERT_CONDITION_UNKNOWN (model
, f
, EQ_EXPR
, float_4
);
3982 ASSERT_CONDITION_UNKNOWN (model
, f
, EQ_EXPR
, int_4
);
3985 /* "a > 3 && a <= 3" should be impossible. */
3987 region_model_manager mgr
;
3988 region_model
model (&mgr
);
3989 ADD_SAT_CONSTRAINT (model
, a
, GT_EXPR
, int_3
);
3990 ADD_UNSAT_CONSTRAINT (model
, a
, LE_EXPR
, int_3
);
3993 /* "(a + 1) > 3 && a < 3" should be impossible. */
3995 region_model_manager mgr
;
3997 region_model
model (&mgr
);
3998 ADD_SAT_CONSTRAINT (model
, a_plus_one
, GT_EXPR
, int_3
);
3999 ADD_UNSAT_CONSTRAINT (model
, a
, LT_EXPR
, int_3
);
4002 region_model
model (&mgr
);
4003 ADD_SAT_CONSTRAINT (model
, a
, LT_EXPR
, int_3
);
4004 ADD_UNSAT_CONSTRAINT (model
, a_plus_one
, GT_EXPR
, int_3
);
4008 /* "3 < a < 4" should be impossible for integer a. */
4010 region_model_manager mgr
;
4012 region_model
model (&mgr
);
4013 ADD_SAT_CONSTRAINT (model
, int_3
, LT_EXPR
, a
);
4014 ADD_UNSAT_CONSTRAINT (model
, a
, LT_EXPR
, int_4
);
4017 region_model
model (&mgr
);
4018 ADD_SAT_CONSTRAINT (model
, int_1
, LT_EXPR
, a
);
4019 ADD_SAT_CONSTRAINT (model
, int_3
, LT_EXPR
, a
);
4020 ADD_SAT_CONSTRAINT (model
, a
, LT_EXPR
, int_5
);
4021 ADD_UNSAT_CONSTRAINT (model
, a
, LT_EXPR
, int_4
);
4024 region_model
model (&mgr
);
4025 ADD_SAT_CONSTRAINT (model
, int_1
, LT_EXPR
, a
);
4026 ADD_SAT_CONSTRAINT (model
, a
, LT_EXPR
, int_5
);
4027 ADD_SAT_CONSTRAINT (model
, int_3
, LT_EXPR
, a
);
4028 ADD_UNSAT_CONSTRAINT (model
, a
, LT_EXPR
, int_4
);
4031 region_model
model (&mgr
);
4032 ADD_SAT_CONSTRAINT (model
, a
, LT_EXPR
, int_4
);
4033 ADD_UNSAT_CONSTRAINT (model
, int_3
, LT_EXPR
, a
);
4036 region_model
model (&mgr
);
4037 ADD_SAT_CONSTRAINT (model
, a
, GT_EXPR
, int_3
);
4038 ADD_UNSAT_CONSTRAINT (model
, int_4
, GT_EXPR
, a
);
4041 region_model
model (&mgr
);
4042 ADD_SAT_CONSTRAINT (model
, int_4
, GT_EXPR
, a
);
4043 ADD_UNSAT_CONSTRAINT (model
, a
, GT_EXPR
, int_3
);
4048 /* Verify various lower-level implementation details about
4049 constraint_manager. */
4052 test_constraint_impl ()
4054 tree int_42
= build_int_cst (integer_type_node
, 42);
4055 tree int_0
= build_int_cst (integer_type_node
, 0);
4057 tree x
= build_global_decl ("x", integer_type_node
);
4058 tree y
= build_global_decl ("y", integer_type_node
);
4059 tree z
= build_global_decl ("z", integer_type_node
);
4063 region_model_manager mgr
;
4064 region_model
model (&mgr
);
4066 ADD_SAT_CONSTRAINT (model
, x
, EQ_EXPR
, y
);
4068 /* Assert various things about the insides of model. */
4069 constraint_manager
*cm
= model
.get_constraints ();
4070 ASSERT_EQ (cm
->m_constraints
.length (), 0);
4071 ASSERT_EQ (cm
->m_equiv_classes
.length (), 1);
4074 /* y <= z; x == y. */
4076 region_model_manager mgr
;
4077 region_model
model (&mgr
);
4078 ASSERT_CONDITION_UNKNOWN (model
, x
, EQ_EXPR
, y
);
4079 ASSERT_CONDITION_UNKNOWN (model
, x
, GE_EXPR
, z
);
4081 ADD_SAT_CONSTRAINT (model
, y
, GE_EXPR
, z
);
4082 ASSERT_CONDITION_TRUE (model
, y
, GE_EXPR
, z
);
4083 ASSERT_CONDITION_UNKNOWN (model
, x
, GE_EXPR
, z
);
4085 ADD_SAT_CONSTRAINT (model
, x
, EQ_EXPR
, y
);
4087 /* Assert various things about the insides of model. */
4088 constraint_manager
*cm
= model
.get_constraints ();
4089 ASSERT_EQ (cm
->m_constraints
.length (), 1);
4090 ASSERT_EQ (cm
->m_equiv_classes
.length (), 2);
4092 /* Ensure that we merged the constraints. */
4093 ASSERT_CONDITION_TRUE (model
, x
, GE_EXPR
, z
);
4096 /* y <= z; y == x. */
4098 region_model_manager mgr
;
4099 region_model
model (&mgr
);
4100 ASSERT_CONDITION_UNKNOWN (model
, x
, EQ_EXPR
, y
);
4101 ASSERT_CONDITION_UNKNOWN (model
, x
, GE_EXPR
, z
);
4103 ADD_SAT_CONSTRAINT (model
, y
, GE_EXPR
, z
);
4104 ASSERT_CONDITION_TRUE (model
, y
, GE_EXPR
, z
);
4105 ASSERT_CONDITION_UNKNOWN (model
, x
, GE_EXPR
, z
);
4107 ADD_SAT_CONSTRAINT (model
, y
, EQ_EXPR
, x
);
4109 /* Assert various things about the insides of model. */
4110 constraint_manager
*cm
= model
.get_constraints ();
4111 ASSERT_EQ (cm
->m_constraints
.length (), 1);
4112 ASSERT_EQ (cm
->m_equiv_classes
.length (), 2);
4114 /* Ensure that we merged the constraints. */
4115 ASSERT_CONDITION_TRUE (model
, x
, GE_EXPR
, z
);
4118 /* x == 0, then x != 42. */
4120 region_model_manager mgr
;
4121 region_model
model (&mgr
);
4123 ADD_SAT_CONSTRAINT (model
, x
, EQ_EXPR
, int_0
);
4124 ADD_SAT_CONSTRAINT (model
, x
, NE_EXPR
, int_42
);
4126 /* Assert various things about the insides of model. */
4127 constraint_manager
*cm
= model
.get_constraints ();
4128 ASSERT_EQ (cm
->m_constraints
.length (), 0);
4129 ASSERT_EQ (cm
->m_equiv_classes
.length (), 1);
4132 // TODO: selftest for merging ecs "in the middle"
4133 // where a non-final one gets overwritten
4135 // TODO: selftest where there are pre-existing constraints
4138 /* Check that operator== and hashing works as expected for the
4144 tree x
= build_global_decl ("x", integer_type_node
);
4145 tree y
= build_global_decl ("y", integer_type_node
);
4148 region_model_manager mgr
;
4149 region_model
model0 (&mgr
);
4150 region_model
model1 (&mgr
);
4152 constraint_manager
*cm0
= model0
.get_constraints ();
4153 constraint_manager
*cm1
= model1
.get_constraints ();
4155 ASSERT_EQ (cm0
->hash (), cm1
->hash ());
4156 ASSERT_EQ (*cm0
, *cm1
);
4158 ASSERT_EQ (model0
.hash (), model1
.hash ());
4159 ASSERT_EQ (model0
, model1
);
4161 ADD_SAT_CONSTRAINT (model1
, x
, EQ_EXPR
, y
);
4162 ASSERT_NE (cm0
->hash (), cm1
->hash ());
4163 ASSERT_NE (*cm0
, *cm1
);
4165 ASSERT_NE (model0
.hash (), model1
.hash ());
4166 ASSERT_NE (model0
, model1
);
4168 region_model
model2 (&mgr
);
4169 constraint_manager
*cm2
= model2
.get_constraints ();
4170 /* Make the same change to cm2. */
4171 ADD_SAT_CONSTRAINT (model2
, x
, EQ_EXPR
, y
);
4172 ASSERT_EQ (cm1
->hash (), cm2
->hash ());
4173 ASSERT_EQ (*cm1
, *cm2
);
4175 ASSERT_EQ (model1
.hash (), model2
.hash ());
4176 ASSERT_EQ (model1
, model2
);
4180 /* Verify tracking inequality of a variable against many constants. */
4183 test_many_constants ()
4185 region_model_manager mgr
;
4186 program_point
point (program_point::origin (mgr
));
4187 tree a
= build_global_decl ("a", integer_type_node
);
4189 region_model
model (&mgr
);
4190 auto_vec
<tree
> constants
;
4191 for (int i
= 0; i
< 20; i
++)
4193 tree constant
= build_int_cst (integer_type_node
, i
);
4194 constants
.safe_push (constant
);
4195 ADD_SAT_CONSTRAINT (model
, a
, NE_EXPR
, constant
);
4197 /* Merge, and check the result. */
4198 region_model
other (model
);
4200 region_model
merged (&mgr
);
4201 ASSERT_TRUE (model
.can_merge_with_p (other
, point
, &merged
));
4202 model
.canonicalize ();
4203 merged
.canonicalize ();
4204 ASSERT_EQ (model
, merged
);
4206 for (int j
= 0; j
<= i
; j
++)
4207 ASSERT_CONDITION_TRUE (model
, a
, NE_EXPR
, constants
[j
]);
4211 /* Verify that purging state relating to a variable doesn't leave stray
4212 equivalence classes (after canonicalization). */
4217 tree int_0
= build_int_cst (integer_type_node
, 0);
4218 tree a
= build_global_decl ("a", integer_type_node
);
4219 tree b
= build_global_decl ("b", integer_type_node
);
4223 region_model_manager mgr
;
4224 region_model
model (&mgr
);
4225 ADD_SAT_CONSTRAINT (model
, a
, NE_EXPR
, int_0
);
4226 ASSERT_EQ (model
.get_constraints ()->m_equiv_classes
.length (), 2);
4227 ASSERT_EQ (model
.get_constraints ()->m_constraints
.length (), 1);
4229 /* Purge state for "a". */
4230 const svalue
*sval_a
= model
.get_rvalue (a
, NULL
);
4231 model
.purge_state_involving (sval_a
, NULL
);
4232 model
.canonicalize ();
4233 /* We should have an empty constraint_manager. */
4234 ASSERT_EQ (model
.get_constraints ()->m_equiv_classes
.length (), 0);
4235 ASSERT_EQ (model
.get_constraints ()->m_constraints
.length (), 0);
4238 /* "a != 0" && "b != 0". */
4240 region_model_manager mgr
;
4241 region_model
model (&mgr
);
4242 ADD_SAT_CONSTRAINT (model
, a
, NE_EXPR
, int_0
);
4243 ADD_SAT_CONSTRAINT (model
, b
, NE_EXPR
, int_0
);
4244 ASSERT_EQ (model
.get_constraints ()->m_equiv_classes
.length (), 3);
4245 ASSERT_EQ (model
.get_constraints ()->m_constraints
.length (), 2);
4247 /* Purge state for "a". */
4248 const svalue
*sval_a
= model
.get_rvalue (a
, NULL
);
4249 model
.purge_state_involving (sval_a
, NULL
);
4250 model
.canonicalize ();
4251 /* We should just have the constraint/ECs involving b != 0. */
4252 ASSERT_EQ (model
.get_constraints ()->m_equiv_classes
.length (), 2);
4253 ASSERT_EQ (model
.get_constraints ()->m_constraints
.length (), 1);
4254 ASSERT_CONDITION_TRUE (model
, b
, NE_EXPR
, int_0
);
4257 /* "a != 0" && "b == 0". */
4259 region_model_manager mgr
;
4260 region_model
model (&mgr
);
4261 ADD_SAT_CONSTRAINT (model
, a
, NE_EXPR
, int_0
);
4262 ADD_SAT_CONSTRAINT (model
, b
, EQ_EXPR
, int_0
);
4263 ASSERT_EQ (model
.get_constraints ()->m_equiv_classes
.length (), 2);
4264 ASSERT_EQ (model
.get_constraints ()->m_constraints
.length (), 1);
4266 /* Purge state for "a". */
4267 const svalue
*sval_a
= model
.get_rvalue (a
, NULL
);
4268 model
.purge_state_involving (sval_a
, NULL
);
4269 model
.canonicalize ();
4270 /* We should just have the EC involving b == 0. */
4271 ASSERT_EQ (model
.get_constraints ()->m_equiv_classes
.length (), 1);
4272 ASSERT_EQ (model
.get_constraints ()->m_constraints
.length (), 0);
4273 ASSERT_CONDITION_TRUE (model
, b
, EQ_EXPR
, int_0
);
4278 region_model_manager mgr
;
4279 region_model
model (&mgr
);
4280 ADD_SAT_CONSTRAINT (model
, a
, EQ_EXPR
, int_0
);
4281 ASSERT_EQ (model
.get_constraints ()->m_equiv_classes
.length (), 1);
4282 ASSERT_EQ (model
.get_constraints ()->m_constraints
.length (), 0);
4284 /* Purge state for "a". */
4285 const svalue
*sval_a
= model
.get_rvalue (a
, NULL
);
4286 model
.purge_state_involving (sval_a
, NULL
);
4287 model
.canonicalize ();
4288 /* We should have an empty constraint_manager. */
4289 ASSERT_EQ (model
.get_constraints ()->m_equiv_classes
.length (), 0);
4290 ASSERT_EQ (model
.get_constraints ()->m_constraints
.length (), 0);
4293 /* "a == 0" && "b != 0". */
4295 region_model_manager mgr
;
4296 region_model
model (&mgr
);
4297 ADD_SAT_CONSTRAINT (model
, a
, EQ_EXPR
, int_0
);
4298 ADD_SAT_CONSTRAINT (model
, b
, NE_EXPR
, int_0
);
4299 ASSERT_EQ (model
.get_constraints ()->m_equiv_classes
.length (), 2);
4300 ASSERT_EQ (model
.get_constraints ()->m_constraints
.length (), 1);
4302 /* Purge state for "a". */
4303 const svalue
*sval_a
= model
.get_rvalue (a
, NULL
);
4304 model
.purge_state_involving (sval_a
, NULL
);
4305 model
.canonicalize ();
4306 /* We should just have the constraint/ECs involving b != 0. */
4307 ASSERT_EQ (model
.get_constraints ()->m_equiv_classes
.length (), 2);
4308 ASSERT_EQ (model
.get_constraints ()->m_constraints
.length (), 1);
4309 ASSERT_CONDITION_TRUE (model
, b
, NE_EXPR
, int_0
);
4312 /* "a == 0" && "b == 0". */
4314 region_model_manager mgr
;
4315 region_model
model (&mgr
);
4316 ADD_SAT_CONSTRAINT (model
, a
, EQ_EXPR
, int_0
);
4317 ADD_SAT_CONSTRAINT (model
, b
, EQ_EXPR
, int_0
);
4318 ASSERT_EQ (model
.get_constraints ()->m_equiv_classes
.length (), 1);
4319 ASSERT_EQ (model
.get_constraints ()->m_constraints
.length (), 0);
4321 /* Purge state for "a". */
4322 const svalue
*sval_a
= model
.get_rvalue (a
, NULL
);
4323 model
.purge_state_involving (sval_a
, NULL
);
4324 model
.canonicalize ();
4325 /* We should just have the EC involving b == 0. */
4326 ASSERT_EQ (model
.get_constraints ()->m_equiv_classes
.length (), 1);
4327 ASSERT_EQ (model
.get_constraints ()->m_constraints
.length (), 0);
4328 ASSERT_CONDITION_TRUE (model
, b
, EQ_EXPR
, int_0
);
4332 /* Implementation detail of ASSERT_DUMP_BOUNDED_RANGES_EQ. */
4335 assert_dump_bounded_range_eq (const location
&loc
,
4336 const bounded_range
&range
,
4337 const char *expected
)
4339 auto_fix_quotes sentinel
;
4341 pp_format_decoder (&pp
) = default_tree_printer
;
4342 range
.dump_to_pp (&pp
, false);
4343 ASSERT_STREQ_AT (loc
, pp_formatted_text (&pp
), expected
);
4346 /* Assert that BR.dump (false) is EXPECTED. */
4348 #define ASSERT_DUMP_BOUNDED_RANGE_EQ(BR, EXPECTED) \
4349 SELFTEST_BEGIN_STMT \
4350 assert_dump_bounded_range_eq ((SELFTEST_LOCATION), (BR), (EXPECTED)); \
4353 /* Verify that bounded_range works as expected. */
4356 test_bounded_range ()
4358 tree u8_0
= build_int_cst (unsigned_char_type_node
, 0);
4359 tree u8_1
= build_int_cst (unsigned_char_type_node
, 1);
4360 tree u8_64
= build_int_cst (unsigned_char_type_node
, 64);
4361 tree u8_128
= build_int_cst (unsigned_char_type_node
, 128);
4362 tree u8_255
= build_int_cst (unsigned_char_type_node
, 255);
4364 tree s8_0
= build_int_cst (signed_char_type_node
, 0);
4365 tree s8_1
= build_int_cst (signed_char_type_node
, 1);
4366 tree s8_2
= build_int_cst (signed_char_type_node
, 2);
4368 bounded_range
br_u8_0 (u8_0
, u8_0
);
4369 ASSERT_DUMP_BOUNDED_RANGE_EQ (br_u8_0
, "0");
4370 ASSERT_TRUE (br_u8_0
.contains_p (u8_0
));
4371 ASSERT_FALSE (br_u8_0
.contains_p (u8_1
));
4372 ASSERT_TRUE (br_u8_0
.contains_p (s8_0
));
4373 ASSERT_FALSE (br_u8_0
.contains_p (s8_1
));
4375 bounded_range
br_u8_0_1 (u8_0
, u8_1
);
4376 ASSERT_DUMP_BOUNDED_RANGE_EQ (br_u8_0_1
, "[0, 1]");
4378 bounded_range
tmp (NULL_TREE
, NULL_TREE
);
4379 ASSERT_TRUE (br_u8_0
.intersects_p (br_u8_0_1
, &tmp
));
4380 ASSERT_DUMP_BOUNDED_RANGE_EQ (tmp
, "0");
4382 bounded_range
br_u8_64_128 (u8_64
, u8_128
);
4383 ASSERT_DUMP_BOUNDED_RANGE_EQ (br_u8_64_128
, "[64, 128]");
4385 ASSERT_FALSE (br_u8_0
.intersects_p (br_u8_64_128
, NULL
));
4386 ASSERT_FALSE (br_u8_64_128
.intersects_p (br_u8_0
, NULL
));
4388 bounded_range
br_u8_128_255 (u8_128
, u8_255
);
4389 ASSERT_DUMP_BOUNDED_RANGE_EQ (br_u8_128_255
, "[128, 255]");
4390 ASSERT_TRUE (br_u8_128_255
.intersects_p (br_u8_64_128
, &tmp
));
4391 ASSERT_DUMP_BOUNDED_RANGE_EQ (tmp
, "128");
4393 bounded_range
br_s8_2 (s8_2
, s8_2
);
4394 ASSERT_DUMP_BOUNDED_RANGE_EQ (br_s8_2
, "2");
4395 bounded_range
br_s8_2_u8_255 (s8_2
, u8_255
);
4396 ASSERT_DUMP_BOUNDED_RANGE_EQ (br_s8_2_u8_255
, "[2, 255]");
4399 /* Implementation detail of ASSERT_DUMP_BOUNDED_RANGES_EQ. */
4402 assert_dump_bounded_ranges_eq (const location
&loc
,
4403 const bounded_ranges
*ranges
,
4404 const char *expected
)
4406 auto_fix_quotes sentinel
;
4408 pp_format_decoder (&pp
) = default_tree_printer
;
4409 ranges
->dump_to_pp (&pp
, false);
4410 ASSERT_STREQ_AT (loc
, pp_formatted_text (&pp
), expected
);
4413 /* Implementation detail of ASSERT_DUMP_BOUNDED_RANGES_EQ. */
4416 assert_dump_bounded_ranges_eq (const location
&loc
,
4417 const bounded_ranges
&ranges
,
4418 const char *expected
)
4420 auto_fix_quotes sentinel
;
4422 pp_format_decoder (&pp
) = default_tree_printer
;
4423 ranges
.dump_to_pp (&pp
, false);
4424 ASSERT_STREQ_AT (loc
, pp_formatted_text (&pp
), expected
);
4427 /* Assert that BRS.dump (false) is EXPECTED. */
4429 #define ASSERT_DUMP_BOUNDED_RANGES_EQ(BRS, EXPECTED) \
4430 SELFTEST_BEGIN_STMT \
4431 assert_dump_bounded_ranges_eq ((SELFTEST_LOCATION), (BRS), (EXPECTED)); \
4434 /* Verify that the bounded_ranges class works as expected. */
4437 test_bounded_ranges ()
4439 bounded_ranges_manager mgr
;
4441 tree ch0
= build_int_cst (unsigned_char_type_node
, 0);
4442 tree ch1
= build_int_cst (unsigned_char_type_node
, 1);
4443 tree ch2
= build_int_cst (unsigned_char_type_node
, 2);
4444 tree ch3
= build_int_cst (unsigned_char_type_node
, 3);
4445 tree ch128
= build_int_cst (unsigned_char_type_node
, 128);
4446 tree ch129
= build_int_cst (unsigned_char_type_node
, 129);
4447 tree ch254
= build_int_cst (unsigned_char_type_node
, 254);
4448 tree ch255
= build_int_cst (unsigned_char_type_node
, 255);
4450 const bounded_ranges
*empty
= mgr
.get_or_create_empty ();
4451 ASSERT_DUMP_BOUNDED_RANGES_EQ (empty
, "{}");
4453 const bounded_ranges
*point0
= mgr
.get_or_create_point (ch0
);
4454 ASSERT_DUMP_BOUNDED_RANGES_EQ (point0
, "{0}");
4456 const bounded_ranges
*point1
= mgr
.get_or_create_point (ch1
);
4457 ASSERT_DUMP_BOUNDED_RANGES_EQ (point1
, "{1}");
4459 const bounded_ranges
*point2
= mgr
.get_or_create_point (ch2
);
4460 ASSERT_DUMP_BOUNDED_RANGES_EQ (point2
, "{2}");
4462 const bounded_ranges
*range0_128
= mgr
.get_or_create_range (ch0
, ch128
);
4463 ASSERT_DUMP_BOUNDED_RANGES_EQ (range0_128
, "{[0, 128]}");
4465 const bounded_ranges
*range0_255
= mgr
.get_or_create_range (ch0
, ch255
);
4466 ASSERT_DUMP_BOUNDED_RANGES_EQ (range0_255
, "{[0, 255]}");
4468 ASSERT_FALSE (empty
->contain_p (ch0
));
4469 ASSERT_FALSE (empty
->contain_p (ch1
));
4470 ASSERT_FALSE (empty
->contain_p (ch255
));
4472 ASSERT_TRUE (point0
->contain_p (ch0
));
4473 ASSERT_FALSE (point0
->contain_p (ch1
));
4474 ASSERT_FALSE (point0
->contain_p (ch255
));
4476 ASSERT_FALSE (point1
->contain_p (ch0
));
4477 ASSERT_TRUE (point1
->contain_p (ch1
));
4478 ASSERT_FALSE (point0
->contain_p (ch255
));
4480 ASSERT_TRUE (range0_128
->contain_p (ch0
));
4481 ASSERT_TRUE (range0_128
->contain_p (ch1
));
4482 ASSERT_TRUE (range0_128
->contain_p (ch128
));
4483 ASSERT_FALSE (range0_128
->contain_p (ch129
));
4484 ASSERT_FALSE (range0_128
->contain_p (ch254
));
4485 ASSERT_FALSE (range0_128
->contain_p (ch255
));
4487 const bounded_ranges
*inv0_128
4488 = mgr
.get_or_create_inverse (range0_128
, unsigned_char_type_node
);
4489 ASSERT_DUMP_BOUNDED_RANGES_EQ (inv0_128
, "{[129, 255]}");
4491 const bounded_ranges
*range128_129
= mgr
.get_or_create_range (ch128
, ch129
);
4492 ASSERT_DUMP_BOUNDED_RANGES_EQ (range128_129
, "{[128, 129]}");
4494 const bounded_ranges
*inv128_129
4495 = mgr
.get_or_create_inverse (range128_129
, unsigned_char_type_node
);
4496 ASSERT_DUMP_BOUNDED_RANGES_EQ (inv128_129
, "{[0, 127], [130, 255]}");
4500 /* Intersection of disjoint ranges should be empty set. */
4501 const bounded_ranges
*intersect0_1
4502 = mgr
.get_or_create_intersection (point0
, point1
);
4503 ASSERT_DUMP_BOUNDED_RANGES_EQ (intersect0_1
, "{}");
4506 /* Various tests of "union of ranges". */
4509 /* Touching points should be merged into a range. */
4510 auto_vec
<const bounded_ranges
*> v
;
4511 v
.safe_push (point0
);
4512 v
.safe_push (point1
);
4513 const bounded_ranges
*union_0_and_1
= mgr
.get_or_create_union (v
);
4514 ASSERT_DUMP_BOUNDED_RANGES_EQ (union_0_and_1
, "{[0, 1]}");
4518 /* Overlapping and out-of-order. */
4519 auto_vec
<const bounded_ranges
*> v
;
4520 v
.safe_push (inv0_128
); // {[129, 255]}
4521 v
.safe_push (range128_129
);
4522 const bounded_ranges
*union_129_255_and_128_129
4523 = mgr
.get_or_create_union (v
);
4524 ASSERT_DUMP_BOUNDED_RANGES_EQ (union_129_255_and_128_129
, "{[128, 255]}");
4528 /* Union of R and inverse(R) should be full range of type. */
4529 auto_vec
<const bounded_ranges
*> v
;
4530 v
.safe_push (range128_129
);
4531 v
.safe_push (inv128_129
);
4532 const bounded_ranges
*union_
= mgr
.get_or_create_union (v
);
4533 ASSERT_DUMP_BOUNDED_RANGES_EQ (union_
, "{[0, 255]}");
4536 /* Union with an endpoint. */
4538 const bounded_ranges
*range2_to_255
4539 = mgr
.get_or_create_range (ch2
, ch255
);
4540 ASSERT_DUMP_BOUNDED_RANGES_EQ (range2_to_255
, "{[2, 255]}");
4541 auto_vec
<const bounded_ranges
*> v
;
4542 v
.safe_push (point0
);
4543 v
.safe_push (point2
);
4544 v
.safe_push (range2_to_255
);
4545 const bounded_ranges
*union_
= mgr
.get_or_create_union (v
);
4546 ASSERT_DUMP_BOUNDED_RANGES_EQ (union_
, "{0, [2, 255]}");
4549 /* Construct from vector of bounded_range. */
4551 auto_vec
<bounded_range
> v
;
4552 v
.safe_push (bounded_range (ch2
, ch2
));
4553 v
.safe_push (bounded_range (ch0
, ch0
));
4554 v
.safe_push (bounded_range (ch2
, ch255
));
4555 bounded_ranges
br (v
);
4556 ASSERT_DUMP_BOUNDED_RANGES_EQ (&br
, "{0, [2, 255]}");
4560 /* Various tests of "inverse". */
4563 const bounded_ranges
*range_1_to_3
= mgr
.get_or_create_range (ch1
, ch3
);
4564 ASSERT_DUMP_BOUNDED_RANGES_EQ (range_1_to_3
, "{[1, 3]}");
4565 const bounded_ranges
*inv
4566 = mgr
.get_or_create_inverse (range_1_to_3
, unsigned_char_type_node
);
4567 ASSERT_DUMP_BOUNDED_RANGES_EQ (inv
, "{0, [4, 255]}");
4570 const bounded_ranges
*range_1_to_255
4571 = mgr
.get_or_create_range (ch1
, ch255
);
4572 ASSERT_DUMP_BOUNDED_RANGES_EQ (range_1_to_255
, "{[1, 255]}");
4573 const bounded_ranges
*inv
4574 = mgr
.get_or_create_inverse (range_1_to_255
, unsigned_char_type_node
);
4575 ASSERT_DUMP_BOUNDED_RANGES_EQ (inv
, "{0}");
4578 const bounded_ranges
*range_0_to_254
4579 = mgr
.get_or_create_range (ch0
, ch254
);
4580 ASSERT_DUMP_BOUNDED_RANGES_EQ (range_0_to_254
, "{[0, 254]}");
4581 const bounded_ranges
*inv
4582 = mgr
.get_or_create_inverse (range_0_to_254
, unsigned_char_type_node
);
4583 ASSERT_DUMP_BOUNDED_RANGES_EQ (inv
, "{255}");
4587 /* "case 'a'-'z': case 'A-Z':" vs "default:", for ASCII. */
4589 tree ch65
= build_int_cst (unsigned_char_type_node
, 65);
4590 tree ch90
= build_int_cst (unsigned_char_type_node
, 90);
4592 tree ch97
= build_int_cst (unsigned_char_type_node
, 97);
4593 tree ch122
= build_int_cst (unsigned_char_type_node
, 122);
4595 const bounded_ranges
*A_to_Z
= mgr
.get_or_create_range (ch65
, ch90
);
4596 ASSERT_DUMP_BOUNDED_RANGES_EQ (A_to_Z
, "{[65, 90]}");
4597 const bounded_ranges
*a_to_z
= mgr
.get_or_create_range (ch97
, ch122
);
4598 ASSERT_DUMP_BOUNDED_RANGES_EQ (a_to_z
, "{[97, 122]}");
4599 auto_vec
<const bounded_ranges
*> v
;
4600 v
.safe_push (A_to_Z
);
4601 v
.safe_push (a_to_z
);
4602 const bounded_ranges
*label_ranges
= mgr
.get_or_create_union (v
);
4603 ASSERT_DUMP_BOUNDED_RANGES_EQ (label_ranges
, "{[65, 90], [97, 122]}");
4604 const bounded_ranges
*default_ranges
4605 = mgr
.get_or_create_inverse (label_ranges
, unsigned_char_type_node
);
4606 ASSERT_DUMP_BOUNDED_RANGES_EQ (default_ranges
,
4607 "{[0, 64], [91, 96], [123, 255]}");
4610 /* Verify ranges from ops. */
4611 ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (EQ_EXPR
, ch128
),
4613 ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (NE_EXPR
, ch128
),
4614 "{[0, 127], [129, 255]}");
4615 ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (LT_EXPR
, ch128
),
4617 ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (LE_EXPR
, ch128
),
4619 ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (GE_EXPR
, ch128
),
4621 ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (GT_EXPR
, ch128
),
4623 /* Ops at endpoints of type ranges. */
4624 ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (LE_EXPR
, ch0
),
4626 ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (LT_EXPR
, ch0
),
4628 ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (NE_EXPR
, ch0
),
4630 ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (GE_EXPR
, ch255
),
4632 ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (GT_EXPR
, ch255
),
4634 ASSERT_DUMP_BOUNDED_RANGES_EQ (bounded_ranges (NE_EXPR
, ch255
),
4637 /* Verify that instances are consolidated by mgr. */
4638 ASSERT_EQ (mgr
.get_or_create_point (ch0
),
4639 mgr
.get_or_create_point (ch0
));
4640 ASSERT_NE (mgr
.get_or_create_point (ch0
),
4641 mgr
.get_or_create_point (ch1
));
4644 /* Verify that we can handle sufficiently simple bitmasking operations. */
4649 region_model_manager mgr
;
4651 tree int_0
= build_int_cst (integer_type_node
, 0);
4652 tree int_0x80
= build_int_cst (integer_type_node
, 0x80);
4653 tree int_0xff
= build_int_cst (integer_type_node
, 0xff);
4654 tree x
= build_global_decl ("x", integer_type_node
);
4656 tree x_bit_and_0x80
= build2 (BIT_AND_EXPR
, integer_type_node
, x
, int_0x80
);
4657 tree x_bit_and_0xff
= build2 (BIT_AND_EXPR
, integer_type_node
, x
, int_0xff
);
4659 /* "x & 0x80 == 0x80". */
4661 region_model
model (&mgr
);
4662 ADD_SAT_CONSTRAINT (model
, x_bit_and_0x80
, EQ_EXPR
, int_0x80
);
4663 ASSERT_CONDITION_FALSE (model
, x
, EQ_EXPR
, int_0
);
4664 ASSERT_CONDITION_UNKNOWN (model
, x
, EQ_EXPR
, int_0x80
);
4667 /* "x & 0x80 != 0x80". */
4669 region_model
model (&mgr
);
4670 ADD_SAT_CONSTRAINT (model
, x_bit_and_0x80
, NE_EXPR
, int_0x80
);
4671 ASSERT_CONDITION_UNKNOWN (model
, x
, EQ_EXPR
, int_0
);
4672 ASSERT_CONDITION_FALSE (model
, x
, EQ_EXPR
, int_0x80
);
4675 /* "x & 0x80 == 0". */
4677 region_model
model (&mgr
);
4679 ADD_SAT_CONSTRAINT (model
, x_bit_and_0x80
, EQ_EXPR
, int_0
);
4680 ASSERT_CONDITION_UNKNOWN (model
, x
, EQ_EXPR
, int_0
);
4681 ASSERT_CONDITION_FALSE (model
, x
, EQ_EXPR
, int_0x80
);
4684 /* "x & 0x80 != 0". */
4686 region_model
model (&mgr
);
4687 ADD_SAT_CONSTRAINT (model
, x_bit_and_0x80
, NE_EXPR
, int_0
);
4688 ASSERT_CONDITION_FALSE (model
, x
, EQ_EXPR
, int_0
);
4689 ASSERT_CONDITION_UNKNOWN (model
, x
, EQ_EXPR
, int_0x80
);
4692 /* More that one bit in the mask. */
4694 /* "x & 0xff == 0x80". */
4696 region_model
model (&mgr
);
4697 ADD_SAT_CONSTRAINT (model
, x_bit_and_0xff
, EQ_EXPR
, int_0x80
);
4698 ASSERT_CONDITION_FALSE (model
, x
, EQ_EXPR
, int_0
);
4699 ASSERT_CONDITION_UNKNOWN (model
, x
, EQ_EXPR
, int_0x80
);
4700 ASSERT_CONDITION_FALSE (model
, x
, EQ_EXPR
, int_0xff
);
4703 /* "x & 0xff != 0x80". */
4705 region_model
model (&mgr
);
4706 ADD_SAT_CONSTRAINT (model
, x_bit_and_0xff
, NE_EXPR
, int_0x80
);
4707 ASSERT_CONDITION_UNKNOWN (model
, x
, EQ_EXPR
, int_0
);
4708 ASSERT_CONDITION_FALSE (model
, x
, EQ_EXPR
, int_0x80
);
4709 ASSERT_CONDITION_UNKNOWN (model
, x
, EQ_EXPR
, int_0xff
);
4712 /* "x & 0xff == 0". */
4714 region_model
model (&mgr
);
4716 ADD_SAT_CONSTRAINT (model
, x_bit_and_0xff
, EQ_EXPR
, int_0
);
4717 ASSERT_CONDITION_UNKNOWN (model
, x
, EQ_EXPR
, int_0
);
4718 ASSERT_CONDITION_FALSE (model
, x
, EQ_EXPR
, int_0x80
);
4719 ASSERT_CONDITION_FALSE (model
, x
, EQ_EXPR
, int_0xff
);
4722 /* "x & 0xff != 0". */
4724 region_model
model (&mgr
);
4725 ADD_SAT_CONSTRAINT (model
, x_bit_and_0xff
, NE_EXPR
, int_0
);
4726 ASSERT_CONDITION_FALSE (model
, x
, EQ_EXPR
, int_0
);
4727 ASSERT_CONDITION_UNKNOWN (model
, x
, EQ_EXPR
, int_0x80
);
4728 ASSERT_CONDITION_UNKNOWN (model
, x
, EQ_EXPR
, int_0xff
);
4732 /* Run the selftests in this file, temporarily overriding
4733 flag_analyzer_transitivity with TRANSITIVITY. */
4736 run_constraint_manager_tests (bool transitivity
)
4738 int saved_flag_analyzer_transitivity
= flag_analyzer_transitivity
;
4739 flag_analyzer_transitivity
= transitivity
;
4742 test_constraint_conditions ();
4743 if (flag_analyzer_transitivity
)
4745 /* These selftests assume transitivity. */
4746 test_transitivity ();
4748 test_constant_comparisons ();
4749 test_constraint_impl ();
4751 test_many_constants ();
4753 test_bounded_range ();
4754 test_bounded_ranges ();
4757 flag_analyzer_transitivity
= saved_flag_analyzer_transitivity
;
4760 /* Run all of the selftests within this file. */
4763 analyzer_constraint_manager_cc_tests ()
4765 /* Run the tests twice: with and without transitivity. */
4766 run_constraint_manager_tests (true);
4767 run_constraint_manager_tests (false);
4770 } // namespace selftest
4772 #endif /* CHECKING_P */
4776 #endif /* #if ENABLE_ANALYZER */