|
145
|
1 /* Tracking equivalence classes and constraints at a point on an execution path.
|
|
|
2 Copyright (C) 2019-2020 Free Software Foundation, Inc.
|
|
|
3 Contributed by David Malcolm <dmalcolm@redhat.com>.
|
|
|
4
|
|
|
5 This file is part of GCC.
|
|
|
6
|
|
|
7 GCC is free software; you can redistribute it and/or modify it
|
|
|
8 under the terms of the GNU General Public License as published by
|
|
|
9 the Free Software Foundation; either version 3, or (at your option)
|
|
|
10 any later version.
|
|
|
11
|
|
|
12 GCC is distributed in the hope that it will be useful, but
|
|
|
13 WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
|
14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
|
|
|
15 General Public License for more details.
|
|
|
16
|
|
|
17 You should have received a copy of the GNU General Public License
|
|
|
18 along with GCC; see the file COPYING3. If not see
|
|
|
19 <http://www.gnu.org/licenses/>. */
|
|
|
20
|
|
|
21 #include "config.h"
|
|
|
22 #include "system.h"
|
|
|
23 #include "coretypes.h"
|
|
|
24 #include "tree.h"
|
|
|
25 #include "function.h"
|
|
|
26 #include "basic-block.h"
|
|
|
27 #include "gimple.h"
|
|
|
28 #include "gimple-iterator.h"
|
|
|
29 #include "fold-const.h"
|
|
|
30 #include "selftest.h"
|
|
|
31 #include "diagnostic-core.h"
|
|
|
32 #include "graphviz.h"
|
|
|
33 #include "function.h"
|
|
|
34 #include "analyzer/analyzer.h"
|
|
|
35 #include "ordered-hash-map.h"
|
|
|
36 #include "options.h"
|
|
|
37 #include "cgraph.h"
|
|
|
38 #include "cfg.h"
|
|
|
39 #include "digraph.h"
|
|
|
40 #include "analyzer/supergraph.h"
|
|
|
41 #include "sbitmap.h"
|
|
|
42 #include "tristate.h"
|
|
|
43 #include "analyzer/region-model.h"
|
|
|
44 #include "analyzer/constraint-manager.h"
|
|
|
45 #include "analyzer/analyzer-selftests.h"
|
|
|
46
|
|
|
47 #if ENABLE_ANALYZER
|
|
|
48
|
|
|
49 namespace ana {
|
|
|
50
|
|
|
51 /* One of the end-points of a range. */
|
|
|
52
|
|
|
53 struct bound
|
|
|
54 {
|
|
|
55 bound () : m_constant (NULL_TREE), m_closed (false) {}
|
|
|
56 bound (tree constant, bool closed)
|
|
|
57 : m_constant (constant), m_closed (closed) {}
|
|
|
58
|
|
|
59 void ensure_closed (bool is_upper);
|
|
|
60
|
|
|
61 const char * get_relation_as_str () const;
|
|
|
62
|
|
|
63 tree m_constant;
|
|
|
64 bool m_closed;
|
|
|
65 };
|
|
|
66
|
|
|
67 /* A range of values, used for determining if a value has been
|
|
|
68 constrained to just one possible constant value. */
|
|
|
69
|
|
|
70 struct range
|
|
|
71 {
|
|
|
72 range () : m_lower_bound (), m_upper_bound () {}
|
|
|
73 range (const bound &lower, const bound &upper)
|
|
|
74 : m_lower_bound (lower), m_upper_bound (upper) {}
|
|
|
75
|
|
|
76 void dump (pretty_printer *pp) const;
|
|
|
77
|
|
|
78 bool constrained_to_single_element (tree *out);
|
|
|
79
|
|
|
80 bound m_lower_bound;
|
|
|
81 bound m_upper_bound;
|
|
|
82 };
|
|
|
83
|
|
|
84 /* struct bound. */
|
|
|
85
|
|
|
86 /* Ensure that this bound is closed by converting an open bound to a
|
|
|
87 closed one. */
|
|
|
88
|
|
|
89 void
|
|
|
90 bound::ensure_closed (bool is_upper)
|
|
|
91 {
|
|
|
92 if (!m_closed)
|
|
|
93 {
|
|
|
94 /* Offset by 1 in the appropriate direction.
|
|
|
95 For example, convert 3 < x into 4 <= x,
|
|
|
96 and convert x < 5 into x <= 4. */
|
|
|
97 gcc_assert (CONSTANT_CLASS_P (m_constant));
|
|
|
98 m_constant = fold_build2 (is_upper ? MINUS_EXPR : PLUS_EXPR,
|
|
|
99 TREE_TYPE (m_constant),
|
|
|
100 m_constant, integer_one_node);
|
|
|
101 gcc_assert (CONSTANT_CLASS_P (m_constant));
|
|
|
102 m_closed = true;
|
|
|
103 }
|
|
|
104 }
|
|
|
105
|
|
|
106 /* Get "<=" vs "<" for this bound. */
|
|
|
107
|
|
|
108 const char *
|
|
|
109 bound::get_relation_as_str () const
|
|
|
110 {
|
|
|
111 if (m_closed)
|
|
|
112 return "<=";
|
|
|
113 else
|
|
|
114 return "<";
|
|
|
115 }
|
|
|
116
|
|
|
117 /* struct range. */
|
|
|
118
|
|
|
119 /* Dump this range to PP, which must support %E for tree. */
|
|
|
120
|
|
|
121 void
|
|
|
122 range::dump (pretty_printer *pp) const
|
|
|
123 {
|
|
|
124 pp_printf (pp, "%qE %s x %s %qE",
|
|
|
125 m_lower_bound.m_constant,
|
|
|
126 m_lower_bound.get_relation_as_str (),
|
|
|
127 m_upper_bound.get_relation_as_str (),
|
|
|
128 m_upper_bound.m_constant);
|
|
|
129 }
|
|
|
130
|
|
|
131 /* Determine if there is only one possible value for this range.
|
|
|
132 If so, return true and write the constant to *OUT.
|
|
|
133 Otherwise, return false. */
|
|
|
134
|
|
|
135 bool
|
|
|
136 range::constrained_to_single_element (tree *out)
|
|
|
137 {
|
|
|
138 if (!INTEGRAL_TYPE_P (TREE_TYPE (m_lower_bound.m_constant)))
|
|
|
139 return false;
|
|
|
140 if (!INTEGRAL_TYPE_P (TREE_TYPE (m_upper_bound.m_constant)))
|
|
|
141 return false;
|
|
|
142
|
|
|
143 /* Convert any open bounds to closed bounds. */
|
|
|
144 m_lower_bound.ensure_closed (false);
|
|
|
145 m_upper_bound.ensure_closed (true);
|
|
|
146
|
|
|
147 // Are they equal?
|
|
|
148 tree comparison = fold_binary (EQ_EXPR, boolean_type_node,
|
|
|
149 m_lower_bound.m_constant,
|
|
|
150 m_upper_bound.m_constant);
|
|
|
151 if (comparison == boolean_true_node)
|
|
|
152 {
|
|
|
153 *out = m_lower_bound.m_constant;
|
|
|
154 return true;
|
|
|
155 }
|
|
|
156 else
|
|
|
157 return false;
|
|
|
158 }
|
|
|
159
|
|
|
160 /* class equiv_class. */
|
|
|
161
|
|
|
162 /* equiv_class's default ctor. */
|
|
|
163
|
|
|
164 equiv_class::equiv_class ()
|
|
|
165 : m_constant (NULL_TREE), m_cst_sid (svalue_id::null ()),
|
|
|
166 m_vars ()
|
|
|
167 {
|
|
|
168 }
|
|
|
169
|
|
|
170 /* equiv_class's copy ctor. */
|
|
|
171
|
|
|
172 equiv_class::equiv_class (const equiv_class &other)
|
|
|
173 : m_constant (other.m_constant), m_cst_sid (other.m_cst_sid),
|
|
|
174 m_vars (other.m_vars.length ())
|
|
|
175 {
|
|
|
176 int i;
|
|
|
177 svalue_id *sid;
|
|
|
178 FOR_EACH_VEC_ELT (other.m_vars, i, sid)
|
|
|
179 m_vars.quick_push (*sid);
|
|
|
180 }
|
|
|
181
|
|
|
182 /* Print an all-on-one-line representation of this equiv_class to PP,
|
|
|
183 which must support %E for trees. */
|
|
|
184
|
|
|
185 void
|
|
|
186 equiv_class::print (pretty_printer *pp) const
|
|
|
187 {
|
|
|
188 pp_character (pp, '{');
|
|
|
189 int i;
|
|
|
190 svalue_id *sid;
|
|
|
191 FOR_EACH_VEC_ELT (m_vars, i, sid)
|
|
|
192 {
|
|
|
193 if (i > 0)
|
|
|
194 pp_string (pp, " == ");
|
|
|
195 sid->print (pp);
|
|
|
196 }
|
|
|
197 if (m_constant)
|
|
|
198 {
|
|
|
199 if (i > 0)
|
|
|
200 pp_string (pp, " == ");
|
|
|
201 pp_printf (pp, "%qE", m_constant);
|
|
|
202 }
|
|
|
203 pp_character (pp, '}');
|
|
|
204 }
|
|
|
205
|
|
|
206 /* Generate a hash value for this equiv_class. */
|
|
|
207
|
|
|
208 hashval_t
|
|
|
209 equiv_class::hash () const
|
|
|
210 {
|
|
|
211 inchash::hash hstate;
|
|
|
212 int i;
|
|
|
213 svalue_id *sid;
|
|
|
214
|
|
|
215 inchash::add_expr (m_constant, hstate);
|
|
|
216 FOR_EACH_VEC_ELT (m_vars, i, sid)
|
|
|
217 inchash::add (*sid, hstate);
|
|
|
218 return hstate.end ();
|
|
|
219 }
|
|
|
220
|
|
|
221 /* Equality operator for equiv_class. */
|
|
|
222
|
|
|
223 bool
|
|
|
224 equiv_class::operator== (const equiv_class &other)
|
|
|
225 {
|
|
|
226 if (m_constant != other.m_constant)
|
|
|
227 return false; // TODO: use tree equality here?
|
|
|
228
|
|
|
229 /* FIXME: should we compare m_cst_sid? */
|
|
|
230
|
|
|
231 if (m_vars.length () != other.m_vars.length ())
|
|
|
232 return false;
|
|
|
233
|
|
|
234 int i;
|
|
|
235 svalue_id *sid;
|
|
|
236 FOR_EACH_VEC_ELT (m_vars, i, sid)
|
|
|
237 if (! (*sid == other.m_vars[i]))
|
|
|
238 return false;
|
|
|
239
|
|
|
240 return true;
|
|
|
241 }
|
|
|
242
|
|
|
243 /* Add SID to this equiv_class, using CM to check if it's a constant. */
|
|
|
244
|
|
|
245 void
|
|
|
246 equiv_class::add (svalue_id sid, const constraint_manager &cm)
|
|
|
247 {
|
|
|
248 gcc_assert (!sid.null_p ());
|
|
|
249 if (tree cst = cm.maybe_get_constant (sid))
|
|
|
250 {
|
|
|
251 gcc_assert (CONSTANT_CLASS_P (cst));
|
|
|
252 /* FIXME: should we canonicalize which svalue is the constant
|
|
|
253 when there are multiple equal constants? */
|
|
|
254 m_constant = cst;
|
|
|
255 m_cst_sid = sid;
|
|
|
256 }
|
|
|
257 m_vars.safe_push (sid);
|
|
|
258 }
|
|
|
259
|
|
|
260 /* Remove SID from this equivalence class.
|
|
|
261 Return true if SID was the last var in the equivalence class (suggesting
|
|
|
262 a possible leak). */
|
|
|
263
|
|
|
264 bool
|
|
|
265 equiv_class::del (svalue_id sid)
|
|
|
266 {
|
|
|
267 gcc_assert (!sid.null_p ());
|
|
|
268 gcc_assert (sid != m_cst_sid);
|
|
|
269
|
|
|
270 int i;
|
|
|
271 svalue_id *iv;
|
|
|
272 FOR_EACH_VEC_ELT (m_vars, i, iv)
|
|
|
273 {
|
|
|
274 if (*iv == sid)
|
|
|
275 {
|
|
|
276 m_vars[i] = m_vars[m_vars.length () - 1];
|
|
|
277 m_vars.pop ();
|
|
|
278 return m_vars.length () == 0;
|
|
|
279 }
|
|
|
280 }
|
|
|
281
|
|
|
282 /* SID must be in the class. */
|
|
|
283 gcc_unreachable ();
|
|
|
284 return false;
|
|
|
285 }
|
|
|
286
|
|
|
287 /* Get a representative member of this class, for handling cases
|
|
|
288 where the IDs can change mid-traversal. */
|
|
|
289
|
|
|
290 svalue_id
|
|
|
291 equiv_class::get_representative () const
|
|
|
292 {
|
|
|
293 if (!m_cst_sid.null_p ())
|
|
|
294 return m_cst_sid;
|
|
|
295 else
|
|
|
296 {
|
|
|
297 gcc_assert (m_vars.length () > 0);
|
|
|
298 return m_vars[0];
|
|
|
299 }
|
|
|
300 }
|
|
|
301
|
|
|
302 /* Remap all svalue_ids within this equiv_class using MAP. */
|
|
|
303
|
|
|
304 void
|
|
|
305 equiv_class::remap_svalue_ids (const svalue_id_map &map)
|
|
|
306 {
|
|
|
307 int i;
|
|
|
308 svalue_id *iv;
|
|
|
309 FOR_EACH_VEC_ELT (m_vars, i, iv)
|
|
|
310 map.update (iv);
|
|
|
311 map.update (&m_cst_sid);
|
|
|
312 }
|
|
|
313
|
|
|
314 /* Comparator for use by equiv_class::canonicalize. */
|
|
|
315
|
|
|
316 static int
|
|
|
317 svalue_id_cmp_by_id (const void *p1, const void *p2)
|
|
|
318 {
|
|
|
319 const svalue_id *sid1 = (const svalue_id *)p1;
|
|
|
320 const svalue_id *sid2 = (const svalue_id *)p2;
|
|
|
321 return sid1->as_int () - sid2->as_int ();
|
|
|
322 }
|
|
|
323
|
|
|
324 /* Sort the svalues_ids within this equiv_class. */
|
|
|
325
|
|
|
326 void
|
|
|
327 equiv_class::canonicalize ()
|
|
|
328 {
|
|
|
329 m_vars.qsort (svalue_id_cmp_by_id);
|
|
|
330 }
|
|
|
331
|
|
|
332 /* Get a debug string for C_OP. */
|
|
|
333
|
|
|
334 const char *
|
|
|
335 constraint_op_code (enum constraint_op c_op)
|
|
|
336 {
|
|
|
337 switch (c_op)
|
|
|
338 {
|
|
|
339 default:
|
|
|
340 gcc_unreachable ();
|
|
|
341 case CONSTRAINT_NE: return "!=";
|
|
|
342 case CONSTRAINT_LT: return "<";
|
|
|
343 case CONSTRAINT_LE: return "<=";
|
|
|
344 }
|
|
|
345 }
|
|
|
346
|
|
|
347 /* Convert C_OP to an enum tree_code. */
|
|
|
348
|
|
|
349 enum tree_code
|
|
|
350 constraint_tree_code (enum constraint_op c_op)
|
|
|
351 {
|
|
|
352 switch (c_op)
|
|
|
353 {
|
|
|
354 default:
|
|
|
355 gcc_unreachable ();
|
|
|
356 case CONSTRAINT_NE: return NE_EXPR;
|
|
|
357 case CONSTRAINT_LT: return LT_EXPR;
|
|
|
358 case CONSTRAINT_LE: return LE_EXPR;
|
|
|
359 }
|
|
|
360 }
|
|
|
361
|
|
|
362 /* Given "lhs C_OP rhs", determine "lhs T_OP rhs".
|
|
|
363
|
|
|
364 For example, given "x < y", then "x > y" is false. */
|
|
|
365
|
|
|
366 static tristate
|
|
|
367 eval_constraint_op_for_op (enum constraint_op c_op, enum tree_code t_op)
|
|
|
368 {
|
|
|
369 switch (c_op)
|
|
|
370 {
|
|
|
371 default:
|
|
|
372 gcc_unreachable ();
|
|
|
373 case CONSTRAINT_NE:
|
|
|
374 if (t_op == EQ_EXPR)
|
|
|
375 return tristate (tristate::TS_FALSE);
|
|
|
376 if (t_op == NE_EXPR)
|
|
|
377 return tristate (tristate::TS_TRUE);
|
|
|
378 break;
|
|
|
379 case CONSTRAINT_LT:
|
|
|
380 if (t_op == LT_EXPR || t_op == LE_EXPR || t_op == NE_EXPR)
|
|
|
381 return tristate (tristate::TS_TRUE);
|
|
|
382 if (t_op == EQ_EXPR || t_op == GT_EXPR || t_op == GE_EXPR)
|
|
|
383 return tristate (tristate::TS_FALSE);
|
|
|
384 break;
|
|
|
385 case CONSTRAINT_LE:
|
|
|
386 if (t_op == LE_EXPR)
|
|
|
387 return tristate (tristate::TS_TRUE);
|
|
|
388 if (t_op == GT_EXPR)
|
|
|
389 return tristate (tristate::TS_FALSE);
|
|
|
390 break;
|
|
|
391 }
|
|
|
392 return tristate (tristate::TS_UNKNOWN);
|
|
|
393 }
|
|
|
394
|
|
|
395 /* class constraint. */
|
|
|
396
|
|
|
397 /* Print this constraint to PP (which must support %E for trees),
|
|
|
398 using CM to look up equiv_class instances from ids. */
|
|
|
399
|
|
|
400 void
|
|
|
401 constraint::print (pretty_printer *pp, const constraint_manager &cm) const
|
|
|
402 {
|
|
|
403 m_lhs.print (pp);
|
|
|
404 pp_string (pp, ": ");
|
|
|
405 m_lhs.get_obj (cm).print (pp);
|
|
|
406 pp_string (pp, " ");
|
|
|
407 pp_string (pp, constraint_op_code (m_op));
|
|
|
408 pp_string (pp, " ");
|
|
|
409 m_rhs.print (pp);
|
|
|
410 pp_string (pp, ": ");
|
|
|
411 m_rhs.get_obj (cm).print (pp);
|
|
|
412 }
|
|
|
413
|
|
|
414 /* Generate a hash value for this constraint. */
|
|
|
415
|
|
|
416 hashval_t
|
|
|
417 constraint::hash () const
|
|
|
418 {
|
|
|
419 inchash::hash hstate;
|
|
|
420 hstate.add_int (m_lhs.m_idx);
|
|
|
421 hstate.add_int (m_op);
|
|
|
422 hstate.add_int (m_rhs.m_idx);
|
|
|
423 return hstate.end ();
|
|
|
424 }
|
|
|
425
|
|
|
426 /* Equality operator for constraints. */
|
|
|
427
|
|
|
428 bool
|
|
|
429 constraint::operator== (const constraint &other) const
|
|
|
430 {
|
|
|
431 if (m_lhs != other.m_lhs)
|
|
|
432 return false;
|
|
|
433 if (m_op != other.m_op)
|
|
|
434 return false;
|
|
|
435 if (m_rhs != other.m_rhs)
|
|
|
436 return false;
|
|
|
437 return true;
|
|
|
438 }
|
|
|
439
|
|
|
440 /* class equiv_class_id. */
|
|
|
441
|
|
|
442 /* Get the underlying equiv_class for this ID from CM. */
|
|
|
443
|
|
|
444 const equiv_class &
|
|
|
445 equiv_class_id::get_obj (const constraint_manager &cm) const
|
|
|
446 {
|
|
|
447 return cm.get_equiv_class_by_index (m_idx);
|
|
|
448 }
|
|
|
449
|
|
|
450 /* Access the underlying equiv_class for this ID from CM. */
|
|
|
451
|
|
|
452 equiv_class &
|
|
|
453 equiv_class_id::get_obj (constraint_manager &cm) const
|
|
|
454 {
|
|
|
455 return cm.get_equiv_class_by_index (m_idx);
|
|
|
456 }
|
|
|
457
|
|
|
458 /* Print this equiv_class_id to PP. */
|
|
|
459
|
|
|
460 void
|
|
|
461 equiv_class_id::print (pretty_printer *pp) const
|
|
|
462 {
|
|
|
463 if (null_p ())
|
|
|
464 pp_printf (pp, "null");
|
|
|
465 else
|
|
|
466 pp_printf (pp, "ec%i", m_idx);
|
|
|
467 }
|
|
|
468
|
|
|
469 /* class constraint_manager. */
|
|
|
470
|
|
|
471 /* constraint_manager's copy ctor. */
|
|
|
472
|
|
|
473 constraint_manager::constraint_manager (const constraint_manager &other)
|
|
|
474 : m_equiv_classes (other.m_equiv_classes.length ()),
|
|
|
475 m_constraints (other.m_constraints.length ())
|
|
|
476 {
|
|
|
477 int i;
|
|
|
478 equiv_class *ec;
|
|
|
479 FOR_EACH_VEC_ELT (other.m_equiv_classes, i, ec)
|
|
|
480 m_equiv_classes.quick_push (new equiv_class (*ec));
|
|
|
481 constraint *c;
|
|
|
482 FOR_EACH_VEC_ELT (other.m_constraints, i, c)
|
|
|
483 m_constraints.quick_push (*c);
|
|
|
484 }
|
|
|
485
|
|
|
486 /* constraint_manager's assignment operator. */
|
|
|
487
|
|
|
488 constraint_manager&
|
|
|
489 constraint_manager::operator= (const constraint_manager &other)
|
|
|
490 {
|
|
|
491 gcc_assert (m_equiv_classes.length () == 0);
|
|
|
492 gcc_assert (m_constraints.length () == 0);
|
|
|
493
|
|
|
494 int i;
|
|
|
495 equiv_class *ec;
|
|
|
496 m_equiv_classes.reserve (other.m_equiv_classes.length ());
|
|
|
497 FOR_EACH_VEC_ELT (other.m_equiv_classes, i, ec)
|
|
|
498 m_equiv_classes.quick_push (new equiv_class (*ec));
|
|
|
499 constraint *c;
|
|
|
500 m_constraints.reserve (other.m_constraints.length ());
|
|
|
501 FOR_EACH_VEC_ELT (other.m_constraints, i, c)
|
|
|
502 m_constraints.quick_push (*c);
|
|
|
503
|
|
|
504 return *this;
|
|
|
505 }
|
|
|
506
|
|
|
507 /* Generate a hash value for this constraint_manager. */
|
|
|
508
|
|
|
509 hashval_t
|
|
|
510 constraint_manager::hash () const
|
|
|
511 {
|
|
|
512 inchash::hash hstate;
|
|
|
513 int i;
|
|
|
514 equiv_class *ec;
|
|
|
515 constraint *c;
|
|
|
516
|
|
|
517 FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
|
|
|
518 hstate.merge_hash (ec->hash ());
|
|
|
519 FOR_EACH_VEC_ELT (m_constraints, i, c)
|
|
|
520 hstate.merge_hash (c->hash ());
|
|
|
521 return hstate.end ();
|
|
|
522 }
|
|
|
523
|
|
|
524 /* Equality operator for constraint_manager. */
|
|
|
525
|
|
|
526 bool
|
|
|
527 constraint_manager::operator== (const constraint_manager &other) const
|
|
|
528 {
|
|
|
529 if (m_equiv_classes.length () != other.m_equiv_classes.length ())
|
|
|
530 return false;
|
|
|
531 if (m_constraints.length () != other.m_constraints.length ())
|
|
|
532 return false;
|
|
|
533
|
|
|
534 int i;
|
|
|
535 equiv_class *ec;
|
|
|
536
|
|
|
537 FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
|
|
|
538 if (!(*ec == *other.m_equiv_classes[i]))
|
|
|
539 return false;
|
|
|
540
|
|
|
541 constraint *c;
|
|
|
542
|
|
|
543 FOR_EACH_VEC_ELT (m_constraints, i, c)
|
|
|
544 if (!(*c == other.m_constraints[i]))
|
|
|
545 return false;
|
|
|
546
|
|
|
547 return true;
|
|
|
548 }
|
|
|
549
|
|
|
550 /* Print this constraint_manager to PP (which must support %E for trees). */
|
|
|
551
|
|
|
552 void
|
|
|
553 constraint_manager::print (pretty_printer *pp) const
|
|
|
554 {
|
|
|
555 pp_string (pp, "{");
|
|
|
556 int i;
|
|
|
557 equiv_class *ec;
|
|
|
558 FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
|
|
|
559 {
|
|
|
560 if (i > 0)
|
|
|
561 pp_string (pp, ", ");
|
|
|
562 equiv_class_id (i).print (pp);
|
|
|
563 pp_string (pp, ": ");
|
|
|
564 ec->print (pp);
|
|
|
565 }
|
|
|
566 pp_string (pp, " | ");
|
|
|
567 constraint *c;
|
|
|
568 FOR_EACH_VEC_ELT (m_constraints, i, c)
|
|
|
569 {
|
|
|
570 if (i > 0)
|
|
|
571 pp_string (pp, " && ");
|
|
|
572 c->print (pp, *this);
|
|
|
573 }
|
|
|
574 pp_printf (pp, "}");
|
|
|
575 }
|
|
|
576
|
|
|
577 /* Dump a multiline representation of this constraint_manager to PP
|
|
|
578 (which must support %E for trees). */
|
|
|
579
|
|
|
580 void
|
|
|
581 constraint_manager::dump_to_pp (pretty_printer *pp) const
|
|
|
582 {
|
|
|
583 // TODO
|
|
|
584 pp_string (pp, " equiv classes:");
|
|
|
585 pp_newline (pp);
|
|
|
586 int i;
|
|
|
587 equiv_class *ec;
|
|
|
588 FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
|
|
|
589 {
|
|
|
590 pp_string (pp, " ");
|
|
|
591 equiv_class_id (i).print (pp);
|
|
|
592 pp_string (pp, ": ");
|
|
|
593 ec->print (pp);
|
|
|
594 pp_newline (pp);
|
|
|
595 }
|
|
|
596 pp_string (pp, " constraints:");
|
|
|
597 pp_newline (pp);
|
|
|
598 constraint *c;
|
|
|
599 FOR_EACH_VEC_ELT (m_constraints, i, c)
|
|
|
600 {
|
|
|
601 pp_printf (pp, " %i: ", i);
|
|
|
602 c->print (pp, *this);
|
|
|
603 pp_newline (pp);
|
|
|
604 }
|
|
|
605 }
|
|
|
606
|
|
|
607 /* Dump a multiline representation of this constraint_manager to FP. */
|
|
|
608
|
|
|
609 void
|
|
|
610 constraint_manager::dump (FILE *fp) const
|
|
|
611 {
|
|
|
612 pretty_printer pp;
|
|
|
613 pp_format_decoder (&pp) = default_tree_printer;
|
|
|
614 pp_show_color (&pp) = pp_show_color (global_dc->printer);
|
|
|
615 pp.buffer->stream = fp;
|
|
|
616 dump_to_pp (&pp);
|
|
|
617 pp_flush (&pp);
|
|
|
618 }
|
|
|
619
|
|
|
620 /* Dump a multiline representation of this constraint_manager to stderr. */
|
|
|
621
|
|
|
622 DEBUG_FUNCTION void
|
|
|
623 constraint_manager::dump () const
|
|
|
624 {
|
|
|
625 dump (stderr);
|
|
|
626 }
|
|
|
627
|
|
|
628 /* Dump a multiline representation of CM to stderr. */
|
|
|
629
|
|
|
630 DEBUG_FUNCTION void
|
|
|
631 debug (const constraint_manager &cm)
|
|
|
632 {
|
|
|
633 cm.dump ();
|
|
|
634 }
|
|
|
635
|
|
|
636 /* Attempt to add the constraint LHS OP RHS to this constraint_manager.
|
|
|
637 Return true if the constraint could be added (or is already true).
|
|
|
638 Return false if the constraint contradicts existing knowledge. */
|
|
|
639
|
|
|
640 bool
|
|
|
641 constraint_manager::add_constraint (svalue_id lhs,
|
|
|
642 enum tree_code op,
|
|
|
643 svalue_id rhs)
|
|
|
644 {
|
|
|
645 equiv_class_id lhs_ec_id = get_or_add_equiv_class (lhs);
|
|
|
646 equiv_class_id rhs_ec_id = get_or_add_equiv_class (rhs);
|
|
|
647 return add_constraint (lhs_ec_id, op,rhs_ec_id);
|
|
|
648 }
|
|
|
649
|
|
|
650 /* Attempt to add the constraint LHS_EC_ID OP RHS_EC_ID to this
|
|
|
651 constraint_manager.
|
|
|
652 Return true if the constraint could be added (or is already true).
|
|
|
653 Return false if the constraint contradicts existing knowledge. */
|
|
|
654
|
|
|
655 bool
|
|
|
656 constraint_manager::add_constraint (equiv_class_id lhs_ec_id,
|
|
|
657 enum tree_code op,
|
|
|
658 equiv_class_id rhs_ec_id)
|
|
|
659 {
|
|
|
660 tristate t = eval_condition (lhs_ec_id, op, rhs_ec_id);
|
|
|
661
|
|
|
662 /* Discard constraints that are already known. */
|
|
|
663 if (t.is_true ())
|
|
|
664 return true;
|
|
|
665
|
|
|
666 /* Reject unsatisfiable constraints. */
|
|
|
667 if (t.is_false ())
|
|
|
668 return false;
|
|
|
669
|
|
|
670 gcc_assert (lhs_ec_id != rhs_ec_id);
|
|
|
671
|
|
|
672 /* For now, simply accumulate constraints, without attempting any further
|
|
|
673 optimization. */
|
|
|
674 switch (op)
|
|
|
675 {
|
|
|
676 case EQ_EXPR:
|
|
|
677 {
|
|
|
678 /* Merge rhs_ec into lhs_ec. */
|
|
|
679 equiv_class &lhs_ec_obj = lhs_ec_id.get_obj (*this);
|
|
|
680 const equiv_class &rhs_ec_obj = rhs_ec_id.get_obj (*this);
|
|
|
681
|
|
|
682 int i;
|
|
|
683 svalue_id *sid;
|
|
|
684 FOR_EACH_VEC_ELT (rhs_ec_obj.m_vars, i, sid)
|
|
|
685 lhs_ec_obj.add (*sid, *this);
|
|
|
686
|
|
|
687 if (rhs_ec_obj.m_constant)
|
|
|
688 {
|
|
|
689 lhs_ec_obj.m_constant = rhs_ec_obj.m_constant;
|
|
|
690 lhs_ec_obj.m_cst_sid = rhs_ec_obj.m_cst_sid;
|
|
|
691 }
|
|
|
692
|
|
|
693 /* Drop rhs equivalence class, overwriting it with the
|
|
|
694 final ec (which might be the same one). */
|
|
|
695 equiv_class_id final_ec_id = m_equiv_classes.length () - 1;
|
|
|
696 equiv_class *old_ec = m_equiv_classes[rhs_ec_id.m_idx];
|
|
|
697 equiv_class *final_ec = m_equiv_classes.pop ();
|
|
|
698 if (final_ec != old_ec)
|
|
|
699 m_equiv_classes[rhs_ec_id.m_idx] = final_ec;
|
|
|
700 delete old_ec;
|
|
|
701
|
|
|
702 /* Update the constraints. */
|
|
|
703 constraint *c;
|
|
|
704 FOR_EACH_VEC_ELT (m_constraints, i, c)
|
|
|
705 {
|
|
|
706 /* Update references to the rhs_ec so that
|
|
|
707 they refer to the lhs_ec. */
|
|
|
708 if (c->m_lhs == rhs_ec_id)
|
|
|
709 c->m_lhs = lhs_ec_id;
|
|
|
710 if (c->m_rhs == rhs_ec_id)
|
|
|
711 c->m_rhs = lhs_ec_id;
|
|
|
712
|
|
|
713 /* Renumber all constraints that refer to the final rhs_ec
|
|
|
714 to the old rhs_ec, where the old final_ec now lives. */
|
|
|
715 if (c->m_lhs == final_ec_id)
|
|
|
716 c->m_lhs = rhs_ec_id;
|
|
|
717 if (c->m_rhs == final_ec_id)
|
|
|
718 c->m_rhs = rhs_ec_id;
|
|
|
719 }
|
|
|
720 }
|
|
|
721 break;
|
|
|
722 case GE_EXPR:
|
|
|
723 add_constraint_internal (rhs_ec_id, CONSTRAINT_LE, lhs_ec_id);
|
|
|
724 break;
|
|
|
725 case LE_EXPR:
|
|
|
726 add_constraint_internal (lhs_ec_id, CONSTRAINT_LE, rhs_ec_id);
|
|
|
727 break;
|
|
|
728 case NE_EXPR:
|
|
|
729 add_constraint_internal (lhs_ec_id, CONSTRAINT_NE, rhs_ec_id);
|
|
|
730 break;
|
|
|
731 case GT_EXPR:
|
|
|
732 add_constraint_internal (rhs_ec_id, CONSTRAINT_LT, lhs_ec_id);
|
|
|
733 break;
|
|
|
734 case LT_EXPR:
|
|
|
735 add_constraint_internal (lhs_ec_id, CONSTRAINT_LT, rhs_ec_id);
|
|
|
736 break;
|
|
|
737 default:
|
|
|
738 /* do nothing. */
|
|
|
739 break;
|
|
|
740 }
|
|
|
741 validate ();
|
|
|
742 return true;
|
|
|
743 }
|
|
|
744
|
|
|
745 /* Subroutine of constraint_manager::add_constraint, for handling all
|
|
|
746 operations other than equality (for which equiv classes are merged). */
|
|
|
747
|
|
|
748 void
|
|
|
749 constraint_manager::add_constraint_internal (equiv_class_id lhs_id,
|
|
|
750 enum constraint_op c_op,
|
|
|
751 equiv_class_id rhs_id)
|
|
|
752 {
|
|
|
753 /* Add the constraint. */
|
|
|
754 m_constraints.safe_push (constraint (lhs_id, c_op, rhs_id));
|
|
|
755
|
|
|
756 if (!flag_analyzer_transitivity)
|
|
|
757 return;
|
|
|
758
|
|
|
759 if (c_op != CONSTRAINT_NE)
|
|
|
760 {
|
|
|
761 /* The following can potentially add EQ_EXPR facts, which could lead
|
|
|
762 to ECs being merged, which would change the meaning of the EC IDs.
|
|
|
763 Hence we need to do this via representatives. */
|
|
|
764 svalue_id lhs = lhs_id.get_obj (*this).get_representative ();
|
|
|
765 svalue_id rhs = rhs_id.get_obj (*this).get_representative ();
|
|
|
766
|
|
|
767 /* We have LHS </<= RHS */
|
|
|
768
|
|
|
769 /* Handle transitivity of ordering by adding additional constraints
|
|
|
770 based on what we already knew.
|
|
|
771
|
|
|
772 So if we have already have:
|
|
|
773 (a < b)
|
|
|
774 (c < d)
|
|
|
775 Then adding:
|
|
|
776 (b < c)
|
|
|
777 will also add:
|
|
|
778 (a < c)
|
|
|
779 (b < d)
|
|
|
780 We need to recurse to ensure we also add:
|
|
|
781 (a < d).
|
|
|
782 We call the checked add_constraint to avoid adding constraints
|
|
|
783 that are already present. Doing so also ensures termination
|
|
|
784 in the case of cycles.
|
|
|
785
|
|
|
786 We also check for single-element ranges, adding EQ_EXPR facts
|
|
|
787 where we discover them. For example 3 < x < 5 implies
|
|
|
788 that x == 4 (if x is an integer). */
|
|
|
789 for (unsigned i = 0; i < m_constraints.length (); i++)
|
|
|
790 {
|
|
|
791 const constraint *other = &m_constraints[i];
|
|
|
792 if (other->is_ordering_p ())
|
|
|
793 {
|
|
|
794 /* Refresh the EC IDs, in case any mergers have happened. */
|
|
|
795 lhs_id = get_or_add_equiv_class (lhs);
|
|
|
796 rhs_id = get_or_add_equiv_class (rhs);
|
|
|
797
|
|
|
798 tree lhs_const = lhs_id.get_obj (*this).m_constant;
|
|
|
799 tree rhs_const = rhs_id.get_obj (*this).m_constant;
|
|
|
800 tree other_lhs_const
|
|
|
801 = other->m_lhs.get_obj (*this).m_constant;
|
|
|
802 tree other_rhs_const
|
|
|
803 = other->m_rhs.get_obj (*this).m_constant;
|
|
|
804
|
|
|
805 /* We have "LHS </<= RHS" and "other.lhs </<= other.rhs". */
|
|
|
806
|
|
|
807 /* If we have LHS </<= RHS and RHS </<= LHS, then we have a
|
|
|
808 cycle. */
|
|
|
809 if (rhs_id == other->m_lhs
|
|
|
810 && other->m_rhs == lhs_id)
|
|
|
811 {
|
|
|
812 /* We must have equality for this to be possible. */
|
|
|
813 gcc_assert (c_op == CONSTRAINT_LE
|
|
|
814 && other->m_op == CONSTRAINT_LE);
|
|
|
815 add_constraint (lhs_id, EQ_EXPR, rhs_id);
|
|
|
816 /* Adding an equality will merge the two ECs and potentially
|
|
|
817 reorganize the constraints. Stop iterating. */
|
|
|
818 return;
|
|
|
819 }
|
|
|
820 /* Otherwise, check for transitivity. */
|
|
|
821 if (rhs_id == other->m_lhs)
|
|
|
822 {
|
|
|
823 /* With RHS == other.lhs, we have:
|
|
|
824 "LHS </<= (RHS, other.lhs) </<= other.rhs"
|
|
|
825 and thus this implies "LHS </<= other.rhs". */
|
|
|
826
|
|
|
827 /* Do we have a tightly-constrained range? */
|
|
|
828 if (lhs_const
|
|
|
829 && !rhs_const
|
|
|
830 && other_rhs_const)
|
|
|
831 {
|
|
|
832 range r (bound (lhs_const, c_op == CONSTRAINT_LE),
|
|
|
833 bound (other_rhs_const,
|
|
|
834 other->m_op == CONSTRAINT_LE));
|
|
|
835 tree constant;
|
|
|
836 if (r.constrained_to_single_element (&constant))
|
|
|
837 {
|
|
|
838 svalue_id cst_sid = get_sid_for_constant (constant);
|
|
|
839 add_constraint
|
|
|
840 (rhs_id, EQ_EXPR,
|
|
|
841 get_or_add_equiv_class (cst_sid));
|
|
|
842 return;
|
|
|
843 }
|
|
|
844 }
|
|
|
845
|
|
|
846 /* Otherwise, add the constraint implied by transitivity. */
|
|
|
847 enum tree_code new_op
|
|
|
848 = ((c_op == CONSTRAINT_LE && other->m_op == CONSTRAINT_LE)
|
|
|
849 ? LE_EXPR : LT_EXPR);
|
|
|
850 add_constraint (lhs_id, new_op, other->m_rhs);
|
|
|
851 }
|
|
|
852 else if (other->m_rhs == lhs_id)
|
|
|
853 {
|
|
|
854 /* With other.rhs == LHS, we have:
|
|
|
855 "other.lhs </<= (other.rhs, LHS) </<= RHS"
|
|
|
856 and thus this implies "other.lhs </<= RHS". */
|
|
|
857
|
|
|
858 /* Do we have a tightly-constrained range? */
|
|
|
859 if (other_lhs_const
|
|
|
860 && !lhs_const
|
|
|
861 && rhs_const)
|
|
|
862 {
|
|
|
863 range r (bound (other_lhs_const,
|
|
|
864 other->m_op == CONSTRAINT_LE),
|
|
|
865 bound (rhs_const,
|
|
|
866 c_op == CONSTRAINT_LE));
|
|
|
867 tree constant;
|
|
|
868 if (r.constrained_to_single_element (&constant))
|
|
|
869 {
|
|
|
870 svalue_id cst_sid = get_sid_for_constant (constant);
|
|
|
871 add_constraint
|
|
|
872 (lhs_id, EQ_EXPR,
|
|
|
873 get_or_add_equiv_class (cst_sid));
|
|
|
874 return;
|
|
|
875 }
|
|
|
876 }
|
|
|
877
|
|
|
878 /* Otherwise, add the constraint implied by transitivity. */
|
|
|
879 enum tree_code new_op
|
|
|
880 = ((c_op == CONSTRAINT_LE && other->m_op == CONSTRAINT_LE)
|
|
|
881 ? LE_EXPR : LT_EXPR);
|
|
|
882 add_constraint (other->m_lhs, new_op, rhs_id);
|
|
|
883 }
|
|
|
884 }
|
|
|
885 }
|
|
|
886 }
|
|
|
887 }
|
|
|
888
|
|
|
889 /* Look for SID within the equivalence classes of this constraint_manager;
|
|
|
890 if found, write the id to *OUT and return true, otherwise return false. */
|
|
|
891
|
|
|
892 bool
|
|
|
893 constraint_manager::get_equiv_class_by_sid (svalue_id sid, equiv_class_id *out) const
|
|
|
894 {
|
|
|
895 /* TODO: should we have a map, rather than these searches? */
|
|
|
896 int i;
|
|
|
897 equiv_class *ec;
|
|
|
898 FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
|
|
|
899 {
|
|
|
900 int j;
|
|
|
901 svalue_id *iv;
|
|
|
902 FOR_EACH_VEC_ELT (ec->m_vars, j, iv)
|
|
|
903 if (*iv == sid)
|
|
|
904 {
|
|
|
905 *out = equiv_class_id (i);
|
|
|
906 return true;
|
|
|
907 }
|
|
|
908 }
|
|
|
909 return false;
|
|
|
910 }
|
|
|
911
|
|
|
912 /* Ensure that SID has an equivalence class within this constraint_manager;
|
|
|
913 return the ID of the class. */
|
|
|
914
|
|
|
915 equiv_class_id
|
|
|
916 constraint_manager::get_or_add_equiv_class (svalue_id sid)
|
|
|
917 {
|
|
|
918 equiv_class_id result (-1);
|
|
|
919
|
|
|
920 /* Try svalue_id match. */
|
|
|
921 if (get_equiv_class_by_sid (sid, &result))
|
|
|
922 return result;
|
|
|
923
|
|
|
924 /* Try equality of constants. */
|
|
|
925 if (tree cst = maybe_get_constant (sid))
|
|
|
926 {
|
|
|
927 int i;
|
|
|
928 equiv_class *ec;
|
|
|
929 FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
|
|
|
930 if (ec->m_constant
|
|
|
931 && types_compatible_p (TREE_TYPE (cst),
|
|
|
932 TREE_TYPE (ec->m_constant)))
|
|
|
933 {
|
|
|
934 tree eq = fold_binary (EQ_EXPR, boolean_type_node,
|
|
|
935 cst, ec->m_constant);
|
|
|
936 if (eq == boolean_true_node)
|
|
|
937 {
|
|
|
938 ec->add (sid, *this);
|
|
|
939 return equiv_class_id (i);
|
|
|
940 }
|
|
|
941 }
|
|
|
942 }
|
|
|
943
|
|
|
944
|
|
|
945 /* Not found. */
|
|
|
946 equiv_class *new_ec = new equiv_class ();
|
|
|
947 new_ec->add (sid, *this);
|
|
|
948 m_equiv_classes.safe_push (new_ec);
|
|
|
949
|
|
|
950 equiv_class_id new_id (m_equiv_classes.length () - 1);
|
|
|
951
|
|
|
952 if (maybe_get_constant (sid))
|
|
|
953 {
|
|
|
954 /* If we have a new EC for a constant, add constraints comparing this
|
|
|
955 to other constants we may have (so that we accumulate the transitive
|
|
|
956 closure of all constraints on constants as the constants are
|
|
|
957 added). */
|
|
|
958 for (equiv_class_id other_id (0); other_id.m_idx < new_id.m_idx;
|
|
|
959 other_id.m_idx++)
|
|
|
960 {
|
|
|
961 const equiv_class &other_ec = other_id.get_obj (*this);
|
|
|
962 if (other_ec.m_constant
|
|
|
963 && types_compatible_p (TREE_TYPE (new_ec->m_constant),
|
|
|
964 TREE_TYPE (other_ec.m_constant)))
|
|
|
965 {
|
|
|
966 /* If we have two ECs, both with constants, the constants must be
|
|
|
967 non-equal (or they would be in the same EC).
|
|
|
968 Determine the direction of the inequality, and record that
|
|
|
969 fact. */
|
|
|
970 tree lt
|
|
|
971 = fold_binary (LT_EXPR, boolean_type_node,
|
|
|
972 new_ec->m_constant, other_ec.m_constant);
|
|
|
973 if (lt == boolean_true_node)
|
|
|
974 add_constraint_internal (new_id, CONSTRAINT_LT, other_id);
|
|
|
975 else if (lt == boolean_false_node)
|
|
|
976 add_constraint_internal (other_id, CONSTRAINT_LT, new_id);
|
|
|
977 /* Refresh new_id, in case ECs were merged. SID should always
|
|
|
978 be present by now, so this should never lead to a
|
|
|
979 recursion. */
|
|
|
980 new_id = get_or_add_equiv_class (sid);
|
|
|
981 }
|
|
|
982 }
|
|
|
983 }
|
|
|
984
|
|
|
985 return new_id;
|
|
|
986 }
|
|
|
987
|
|
|
988 /* Evaluate the condition LHS_EC OP RHS_EC. */
|
|
|
989
|
|
|
990 tristate
|
|
|
991 constraint_manager::eval_condition (equiv_class_id lhs_ec,
|
|
|
992 enum tree_code op,
|
|
|
993 equiv_class_id rhs_ec)
|
|
|
994 {
|
|
|
995 if (lhs_ec == rhs_ec)
|
|
|
996 {
|
|
|
997 switch (op)
|
|
|
998 {
|
|
|
999 case EQ_EXPR:
|
|
|
1000 case GE_EXPR:
|
|
|
1001 case LE_EXPR:
|
|
|
1002 return tristate (tristate::TS_TRUE);
|
|
|
1003
|
|
|
1004 case NE_EXPR:
|
|
|
1005 case GT_EXPR:
|
|
|
1006 case LT_EXPR:
|
|
|
1007 return tristate (tristate::TS_FALSE);
|
|
|
1008 default:
|
|
|
1009 break;
|
|
|
1010 }
|
|
|
1011 }
|
|
|
1012
|
|
|
1013 tree lhs_const = lhs_ec.get_obj (*this).get_any_constant ();
|
|
|
1014 tree rhs_const = rhs_ec.get_obj (*this).get_any_constant ();
|
|
|
1015 if (lhs_const && rhs_const)
|
|
|
1016 {
|
|
|
1017 tree comparison
|
|
|
1018 = fold_binary (op, boolean_type_node, lhs_const, rhs_const);
|
|
|
1019 if (comparison == boolean_true_node)
|
|
|
1020 return tristate (tristate::TS_TRUE);
|
|
|
1021 if (comparison == boolean_false_node)
|
|
|
1022 return tristate (tristate::TS_FALSE);
|
|
|
1023 }
|
|
|
1024
|
|
|
1025 enum tree_code swapped_op = swap_tree_comparison (op);
|
|
|
1026
|
|
|
1027 int i;
|
|
|
1028 constraint *c;
|
|
|
1029 FOR_EACH_VEC_ELT (m_constraints, i, c)
|
|
|
1030 {
|
|
|
1031 if (c->m_lhs == lhs_ec
|
|
|
1032 && c->m_rhs == rhs_ec)
|
|
|
1033 {
|
|
|
1034 tristate result_for_constraint
|
|
|
1035 = eval_constraint_op_for_op (c->m_op, op);
|
|
|
1036 if (result_for_constraint.is_known ())
|
|
|
1037 return result_for_constraint;
|
|
|
1038 }
|
|
|
1039 /* Swapped operands. */
|
|
|
1040 if (c->m_lhs == rhs_ec
|
|
|
1041 && c->m_rhs == lhs_ec)
|
|
|
1042 {
|
|
|
1043 tristate result_for_constraint
|
|
|
1044 = eval_constraint_op_for_op (c->m_op, swapped_op);
|
|
|
1045 if (result_for_constraint.is_known ())
|
|
|
1046 return result_for_constraint;
|
|
|
1047 }
|
|
|
1048 }
|
|
|
1049
|
|
|
1050 return tristate (tristate::TS_UNKNOWN);
|
|
|
1051 }
|
|
|
1052
|
|
|
1053 /* Evaluate the condition LHS OP RHS, creating equiv_class instances for
|
|
|
1054 LHS and RHS if they aren't already in equiv_classes. */
|
|
|
1055
|
|
|
1056 tristate
|
|
|
1057 constraint_manager::eval_condition (svalue_id lhs,
|
|
|
1058 enum tree_code op,
|
|
|
1059 svalue_id rhs)
|
|
|
1060 {
|
|
|
1061 return eval_condition (get_or_add_equiv_class (lhs),
|
|
|
1062 op,
|
|
|
1063 get_or_add_equiv_class (rhs));
|
|
|
1064 }
|
|
|
1065
|
|
|
1066 /* Delete any information about svalue_id instances identified by P.
|
|
|
1067 Such instances are removed from equivalence classes, and any
|
|
|
1068 redundant ECs and constraints are also removed.
|
|
|
1069 Accumulate stats into STATS. */
|
|
|
1070
|
|
|
1071 void
|
|
|
1072 constraint_manager::purge (const purge_criteria &p, purge_stats *stats)
|
|
|
1073 {
|
|
|
1074 /* Delete any svalue_ids identified by P within the various equivalence
|
|
|
1075 classes. */
|
|
|
1076 for (unsigned ec_idx = 0; ec_idx < m_equiv_classes.length (); )
|
|
|
1077 {
|
|
|
1078 equiv_class *ec = m_equiv_classes[ec_idx];
|
|
|
1079
|
|
|
1080 int i;
|
|
|
1081 svalue_id *pv;
|
|
|
1082 bool delete_ec = false;
|
|
|
1083 FOR_EACH_VEC_ELT (ec->m_vars, i, pv)
|
|
|
1084 {
|
|
|
1085 if (*pv == ec->m_cst_sid)
|
|
|
1086 continue;
|
|
|
1087 if (p.should_purge_p (*pv))
|
|
|
1088 {
|
|
|
1089 if (ec->del (*pv))
|
|
|
1090 if (!ec->m_constant)
|
|
|
1091 delete_ec = true;
|
|
|
1092 }
|
|
|
1093 }
|
|
|
1094
|
|
|
1095 if (delete_ec)
|
|
|
1096 {
|
|
|
1097 delete ec;
|
|
|
1098 m_equiv_classes.ordered_remove (ec_idx);
|
|
|
1099 if (stats)
|
|
|
1100 stats->m_num_equiv_classes++;
|
|
|
1101
|
|
|
1102 /* Update the constraints, potentially removing some. */
|
|
|
1103 for (unsigned con_idx = 0; con_idx < m_constraints.length (); )
|
|
|
1104 {
|
|
|
1105 constraint *c = &m_constraints[con_idx];
|
|
|
1106
|
|
|
1107 /* Remove constraints that refer to the deleted EC. */
|
|
|
1108 if (c->m_lhs == ec_idx
|
|
|
1109 || c->m_rhs == ec_idx)
|
|
|
1110 {
|
|
|
1111 m_constraints.ordered_remove (con_idx);
|
|
|
1112 if (stats)
|
|
|
1113 stats->m_num_constraints++;
|
|
|
1114 }
|
|
|
1115 else
|
|
|
1116 {
|
|
|
1117 /* Renumber constraints that refer to ECs that have
|
|
|
1118 had their idx changed. */
|
|
|
1119 c->m_lhs.update_for_removal (ec_idx);
|
|
|
1120 c->m_rhs.update_for_removal (ec_idx);
|
|
|
1121
|
|
|
1122 con_idx++;
|
|
|
1123 }
|
|
|
1124 }
|
|
|
1125 }
|
|
|
1126 else
|
|
|
1127 ec_idx++;
|
|
|
1128 }
|
|
|
1129
|
|
|
1130 /* Now delete any constraints that are purely between constants. */
|
|
|
1131 for (unsigned con_idx = 0; con_idx < m_constraints.length (); )
|
|
|
1132 {
|
|
|
1133 constraint *c = &m_constraints[con_idx];
|
|
|
1134 if (m_equiv_classes[c->m_lhs.m_idx]->m_vars.length () == 0
|
|
|
1135 && m_equiv_classes[c->m_rhs.m_idx]->m_vars.length () == 0)
|
|
|
1136 {
|
|
|
1137 m_constraints.ordered_remove (con_idx);
|
|
|
1138 if (stats)
|
|
|
1139 stats->m_num_constraints++;
|
|
|
1140 }
|
|
|
1141 else
|
|
|
1142 {
|
|
|
1143 con_idx++;
|
|
|
1144 }
|
|
|
1145 }
|
|
|
1146
|
|
|
1147 /* Finally, delete any ECs that purely contain constants and aren't
|
|
|
1148 referenced by any constraints. */
|
|
|
1149 for (unsigned ec_idx = 0; ec_idx < m_equiv_classes.length (); )
|
|
|
1150 {
|
|
|
1151 equiv_class *ec = m_equiv_classes[ec_idx];
|
|
|
1152 if (ec->m_vars.length () == 0)
|
|
|
1153 {
|
|
|
1154 equiv_class_id ec_id (ec_idx);
|
|
|
1155 bool has_constraint = false;
|
|
|
1156 for (unsigned con_idx = 0; con_idx < m_constraints.length ();
|
|
|
1157 con_idx++)
|
|
|
1158 {
|
|
|
1159 constraint *c = &m_constraints[con_idx];
|
|
|
1160 if (c->m_lhs == ec_id
|
|
|
1161 || c->m_rhs == ec_id)
|
|
|
1162 {
|
|
|
1163 has_constraint = true;
|
|
|
1164 break;
|
|
|
1165 }
|
|
|
1166 }
|
|
|
1167 if (!has_constraint)
|
|
|
1168 {
|
|
|
1169 delete ec;
|
|
|
1170 m_equiv_classes.ordered_remove (ec_idx);
|
|
|
1171 if (stats)
|
|
|
1172 stats->m_num_equiv_classes++;
|
|
|
1173
|
|
|
1174 /* Renumber constraints that refer to ECs that have
|
|
|
1175 had their idx changed. */
|
|
|
1176 for (unsigned con_idx = 0; con_idx < m_constraints.length ();
|
|
|
1177 con_idx++)
|
|
|
1178 {
|
|
|
1179 constraint *c = &m_constraints[con_idx];
|
|
|
1180 c->m_lhs.update_for_removal (ec_idx);
|
|
|
1181 c->m_rhs.update_for_removal (ec_idx);
|
|
|
1182 }
|
|
|
1183 continue;
|
|
|
1184 }
|
|
|
1185 }
|
|
|
1186 ec_idx++;
|
|
|
1187 }
|
|
|
1188
|
|
|
1189 validate ();
|
|
|
1190 }
|
|
|
1191
|
|
|
1192 /* Remap all svalue_ids within this constraint_manager using MAP. */
|
|
|
1193
|
|
|
1194 void
|
|
|
1195 constraint_manager::remap_svalue_ids (const svalue_id_map &map)
|
|
|
1196 {
|
|
|
1197 int i;
|
|
|
1198 equiv_class *ec;
|
|
|
1199 FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
|
|
|
1200 ec->remap_svalue_ids (map);
|
|
|
1201 }
|
|
|
1202
|
|
|
1203 /* Comparator for use by constraint_manager::canonicalize.
|
|
|
1204 Sort a pair of equiv_class instances, using the representative
|
|
|
1205 svalue_id as a sort key. */
|
|
|
1206
|
|
|
1207 static int
|
|
|
1208 equiv_class_cmp (const void *p1, const void *p2)
|
|
|
1209 {
|
|
|
1210 const equiv_class *ec1 = *(const equiv_class * const *)p1;
|
|
|
1211 const equiv_class *ec2 = *(const equiv_class * const *)p2;
|
|
|
1212
|
|
|
1213 svalue_id rep1 = ec1->get_representative ();
|
|
|
1214 svalue_id rep2 = ec2->get_representative ();
|
|
|
1215
|
|
|
1216 return rep1.as_int () - rep2.as_int ();
|
|
|
1217 }
|
|
|
1218
|
|
|
1219 /* Comparator for use by constraint_manager::canonicalize.
|
|
|
1220 Sort a pair of constraint instances. */
|
|
|
1221
|
|
|
1222 static int
|
|
|
1223 constraint_cmp (const void *p1, const void *p2)
|
|
|
1224 {
|
|
|
1225 const constraint *c1 = (const constraint *)p1;
|
|
|
1226 const constraint *c2 = (const constraint *)p2;
|
|
|
1227 int lhs_cmp = c1->m_lhs.as_int () - c2->m_lhs.as_int ();
|
|
|
1228 if (lhs_cmp)
|
|
|
1229 return lhs_cmp;
|
|
|
1230 int rhs_cmp = c1->m_rhs.as_int () - c2->m_rhs.as_int ();
|
|
|
1231 if (rhs_cmp)
|
|
|
1232 return rhs_cmp;
|
|
|
1233 return c1->m_op - c2->m_op;
|
|
|
1234 }
|
|
|
1235
|
|
|
1236 /* Reorder the equivalence classes and constraints within this
|
|
|
1237 constraint_manager into a canonical order, to increase the
|
|
|
1238 chances of finding equality with another instance. */
|
|
|
1239
|
|
|
1240 void
|
|
|
1241 constraint_manager::canonicalize (unsigned num_svalue_ids)
|
|
|
1242 {
|
|
|
1243 /* First, sort svalue_ids within the ECs. */
|
|
|
1244 unsigned i;
|
|
|
1245 equiv_class *ec;
|
|
|
1246 FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
|
|
|
1247 ec->canonicalize ();
|
|
|
1248
|
|
|
1249 /* Next, sort the ECs into a canonical order. */
|
|
|
1250
|
|
|
1251 /* We will need to remap the equiv_class_ids in the constraints,
|
|
|
1252 so we need to store the original index of each EC.
|
|
|
1253 Build a lookup table, mapping from representative svalue_id
|
|
|
1254 to the original equiv_class_id of that svalue_id. */
|
|
|
1255 auto_vec<equiv_class_id> original_ec_id (num_svalue_ids);
|
|
|
1256 for (i = 0; i < num_svalue_ids; i++)
|
|
|
1257 original_ec_id.quick_push (equiv_class_id::null ());
|
|
|
1258 FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
|
|
|
1259 {
|
|
|
1260 svalue_id rep = ec->get_representative ();
|
|
|
1261 gcc_assert (!rep.null_p ());
|
|
|
1262 original_ec_id[rep.as_int ()] = i;
|
|
|
1263 }
|
|
|
1264
|
|
|
1265 /* Sort the equivalence classes. */
|
|
|
1266 m_equiv_classes.qsort (equiv_class_cmp);
|
|
|
1267
|
|
|
1268 /* Populate ec_id_map based on the old vs new EC ids. */
|
|
|
1269 one_way_id_map<equiv_class_id> ec_id_map (m_equiv_classes.length ());
|
|
|
1270 FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
|
|
|
1271 {
|
|
|
1272 svalue_id rep = ec->get_representative ();
|
|
|
1273 ec_id_map.put (original_ec_id[rep.as_int ()], i);
|
|
|
1274 }
|
|
|
1275
|
|
|
1276 /* Update the EC ids within the constraints. */
|
|
|
1277 constraint *c;
|
|
|
1278 FOR_EACH_VEC_ELT (m_constraints, i, c)
|
|
|
1279 {
|
|
|
1280 ec_id_map.update (&c->m_lhs);
|
|
|
1281 ec_id_map.update (&c->m_rhs);
|
|
|
1282 }
|
|
|
1283
|
|
|
1284 /* Finally, sort the constraints. */
|
|
|
1285 m_constraints.qsort (constraint_cmp);
|
|
|
1286 }
|
|
|
1287
|
|
|
1288 /* A concrete subclass of constraint_manager for use when
|
|
|
1289 merging two constraint_manager into a third constraint_manager,
|
|
|
1290 each of which has its own region_model.
|
|
|
1291 Calls are delegated to the constraint_manager for the merged model,
|
|
|
1292 and thus affect its region_model. */
|
|
|
1293
|
|
|
1294 class cleaned_constraint_manager : public constraint_manager
|
|
|
1295 {
|
|
|
1296 public:
|
|
|
1297 cleaned_constraint_manager (constraint_manager *merged) : m_merged (merged) {}
|
|
|
1298
|
|
|
1299 constraint_manager *clone (region_model *) const FINAL OVERRIDE
|
|
|
1300 {
|
|
|
1301 gcc_unreachable ();
|
|
|
1302 }
|
|
|
1303 tree maybe_get_constant (svalue_id sid) const FINAL OVERRIDE
|
|
|
1304 {
|
|
|
1305 return m_merged->maybe_get_constant (sid);
|
|
|
1306 }
|
|
|
1307 svalue_id get_sid_for_constant (tree cst) const FINAL OVERRIDE
|
|
|
1308 {
|
|
|
1309 return m_merged->get_sid_for_constant (cst);
|
|
|
1310 }
|
|
|
1311 virtual int get_num_svalues () const FINAL OVERRIDE
|
|
|
1312 {
|
|
|
1313 return m_merged->get_num_svalues ();
|
|
|
1314 }
|
|
|
1315 private:
|
|
|
1316 constraint_manager *m_merged;
|
|
|
1317 };
|
|
|
1318
|
|
|
1319 /* Concrete subclass of fact_visitor for use by constraint_manager::merge.
|
|
|
1320 For every fact in CM_A, see if it is also true in *CM_B. Add such
|
|
|
1321 facts to *OUT. */
|
|
|
1322
|
|
|
1323 class merger_fact_visitor : public fact_visitor
|
|
|
1324 {
|
|
|
1325 public:
|
|
|
1326 merger_fact_visitor (constraint_manager *cm_b,
|
|
|
1327 constraint_manager *out)
|
|
|
1328 : m_cm_b (cm_b), m_out (out)
|
|
|
1329 {}
|
|
|
1330
|
|
|
1331 void on_fact (svalue_id lhs, enum tree_code code, svalue_id rhs)
|
|
|
1332 FINAL OVERRIDE
|
|
|
1333 {
|
|
|
1334 if (m_cm_b->eval_condition (lhs, code, rhs).is_true ())
|
|
|
1335 {
|
|
|
1336 bool sat = m_out->add_constraint (lhs, code, rhs);
|
|
|
1337 gcc_assert (sat);
|
|
|
1338 }
|
|
|
1339 }
|
|
|
1340
|
|
|
1341 private:
|
|
|
1342 constraint_manager *m_cm_b;
|
|
|
1343 constraint_manager *m_out;
|
|
|
1344 };
|
|
|
1345
|
|
|
1346 /* Use MERGER to merge CM_A and CM_B into *OUT.
|
|
|
1347 If one thinks of a constraint_manager as a subset of N-dimensional
|
|
|
1348 space, this takes the union of the points of CM_A and CM_B, and
|
|
|
1349 expresses that into *OUT. Alternatively, it can be thought of
|
|
|
1350 as the intersection of the constraints. */
|
|
|
1351
|
|
|
1352 void
|
|
|
1353 constraint_manager::merge (const constraint_manager &cm_a,
|
|
|
1354 const constraint_manager &cm_b,
|
|
|
1355 constraint_manager *out,
|
|
|
1356 const model_merger &merger)
|
|
|
1357 {
|
|
|
1358 gcc_assert (merger.m_sid_mapping);
|
|
|
1359
|
|
|
1360 /* Map svalue_ids in each equiv class from both sources
|
|
|
1361 to the merged region_model, dropping ids that don't survive merger,
|
|
|
1362 and potentially creating svalues in *OUT for constants. */
|
|
|
1363 cleaned_constraint_manager cleaned_cm_a (out);
|
|
|
1364 const one_way_svalue_id_map &map_a_to_m
|
|
|
1365 = merger.m_sid_mapping->m_map_from_a_to_m;
|
|
|
1366 clean_merger_input (cm_a, map_a_to_m, &cleaned_cm_a);
|
|
|
1367
|
|
|
1368 cleaned_constraint_manager cleaned_cm_b (out);
|
|
|
1369 const one_way_svalue_id_map &map_b_to_m
|
|
|
1370 = merger.m_sid_mapping->m_map_from_b_to_m;
|
|
|
1371 clean_merger_input (cm_b, map_b_to_m, &cleaned_cm_b);
|
|
|
1372
|
|
|
1373 /* At this point, the two cleaned CMs have ECs and constraints referring
|
|
|
1374 to svalues in the merged region model, but both of them have separate
|
|
|
1375 ECs. */
|
|
|
1376
|
|
|
1377 /* Merge the equivalence classes and constraints.
|
|
|
1378 The easiest way to do this seems to be to enumerate all of the facts
|
|
|
1379 in cleaned_cm_a, see which are also true in cleaned_cm_b,
|
|
|
1380 and add those to *OUT. */
|
|
|
1381 merger_fact_visitor v (&cleaned_cm_b, out);
|
|
|
1382 cleaned_cm_a.for_each_fact (&v);
|
|
|
1383 }
|
|
|
1384
|
|
|
1385 /* A subroutine of constraint_manager::merge.
|
|
|
1386 Use MAP_SID_TO_M to map equivalence classes and constraints from
|
|
|
1387 SM_IN to *OUT. Purge any non-constant svalue_id that don't appear
|
|
|
1388 in the result of MAP_SID_TO_M, purging any ECs and their constraints
|
|
|
1389 that become empty as a result. Potentially create svalues in
|
|
|
1390 the merged region_model for constants that weren't already in use there. */
|
|
|
1391
|
|
|
1392 void
|
|
|
1393 constraint_manager::
|
|
|
1394 clean_merger_input (const constraint_manager &cm_in,
|
|
|
1395 const one_way_svalue_id_map &map_sid_to_m,
|
|
|
1396 constraint_manager *out)
|
|
|
1397 {
|
|
|
1398 one_way_id_map<equiv_class_id> map_ec_to_m
|
|
|
1399 (cm_in.m_equiv_classes.length ());
|
|
|
1400 unsigned ec_idx;
|
|
|
1401 equiv_class *ec;
|
|
|
1402 FOR_EACH_VEC_ELT (cm_in.m_equiv_classes, ec_idx, ec)
|
|
|
1403 {
|
|
|
1404 equiv_class cleaned_ec;
|
|
|
1405 if (tree cst = ec->get_any_constant ())
|
|
|
1406 {
|
|
|
1407 cleaned_ec.m_constant = cst;
|
|
|
1408 /* Lazily create the constant in the out region_model. */
|
|
|
1409 cleaned_ec.m_cst_sid = out->get_sid_for_constant (cst);
|
|
|
1410 }
|
|
|
1411 unsigned var_idx;
|
|
|
1412 svalue_id *var_in_sid;
|
|
|
1413 FOR_EACH_VEC_ELT (ec->m_vars, var_idx, var_in_sid)
|
|
|
1414 {
|
|
|
1415 svalue_id var_m_sid = map_sid_to_m.get_dst_for_src (*var_in_sid);
|
|
|
1416 if (!var_m_sid.null_p ())
|
|
|
1417 cleaned_ec.m_vars.safe_push (var_m_sid);
|
|
|
1418 }
|
|
|
1419 if (cleaned_ec.get_any_constant () || !cleaned_ec.m_vars.is_empty ())
|
|
|
1420 {
|
|
|
1421 map_ec_to_m.put (ec_idx, out->m_equiv_classes.length ());
|
|
|
1422 out->m_equiv_classes.safe_push (new equiv_class (cleaned_ec));
|
|
|
1423 }
|
|
|
1424 }
|
|
|
1425
|
|
|
1426 /* Write out to *OUT any constraints for which both sides survived
|
|
|
1427 cleaning, using the new EC IDs. */
|
|
|
1428 unsigned con_idx;
|
|
|
1429 constraint *c;
|
|
|
1430 FOR_EACH_VEC_ELT (cm_in.m_constraints, con_idx, c)
|
|
|
1431 {
|
|
|
1432 equiv_class_id new_lhs = map_ec_to_m.get_dst_for_src (c->m_lhs);
|
|
|
1433 if (new_lhs.null_p ())
|
|
|
1434 continue;
|
|
|
1435 equiv_class_id new_rhs = map_ec_to_m.get_dst_for_src (c->m_rhs);
|
|
|
1436 if (new_rhs.null_p ())
|
|
|
1437 continue;
|
|
|
1438 out->m_constraints.safe_push (constraint (new_lhs,
|
|
|
1439 c->m_op,
|
|
|
1440 new_rhs));
|
|
|
1441 }
|
|
|
1442 }
|
|
|
1443
|
|
|
1444 /* Call VISITOR's on_fact vfunc repeatedly to express the various
|
|
|
1445 equivalence classes and constraints.
|
|
|
1446 This is used by constraint_manager::merge to find the common
|
|
|
1447 facts between two input constraint_managers. */
|
|
|
1448
|
|
|
1449 void
|
|
|
1450 constraint_manager::for_each_fact (fact_visitor *visitor) const
|
|
|
1451 {
|
|
|
1452 /* First, call EQ_EXPR within the various equivalence classes. */
|
|
|
1453 unsigned ec_idx;
|
|
|
1454 equiv_class *ec;
|
|
|
1455 FOR_EACH_VEC_ELT (m_equiv_classes, ec_idx, ec)
|
|
|
1456 {
|
|
|
1457 if (!ec->m_cst_sid.null_p ())
|
|
|
1458 {
|
|
|
1459 unsigned i;
|
|
|
1460 svalue_id *sid;
|
|
|
1461 FOR_EACH_VEC_ELT (ec->m_vars, i, sid)
|
|
|
1462 visitor->on_fact (ec->m_cst_sid, EQ_EXPR, *sid);
|
|
|
1463 }
|
|
|
1464 for (unsigned i = 0; i < ec->m_vars.length (); i++)
|
|
|
1465 for (unsigned j = i + 1; j < ec->m_vars.length (); j++)
|
|
|
1466 visitor->on_fact (ec->m_vars[i], EQ_EXPR, ec->m_vars[j]);
|
|
|
1467 }
|
|
|
1468
|
|
|
1469 /* Now, express the various constraints. */
|
|
|
1470 unsigned con_idx;
|
|
|
1471 constraint *c;
|
|
|
1472 FOR_EACH_VEC_ELT (m_constraints, con_idx, c)
|
|
|
1473 {
|
|
|
1474 const equiv_class &ec_lhs = c->m_lhs.get_obj (*this);
|
|
|
1475 const equiv_class &ec_rhs = c->m_rhs.get_obj (*this);
|
|
|
1476 enum tree_code code = constraint_tree_code (c->m_op);
|
|
|
1477
|
|
|
1478 if (!ec_lhs.m_cst_sid.null_p ())
|
|
|
1479 {
|
|
|
1480 for (unsigned j = 0; j < ec_rhs.m_vars.length (); j++)
|
|
|
1481 {
|
|
|
1482 visitor->on_fact (ec_lhs.m_cst_sid, code, ec_rhs.m_vars[j]);
|
|
|
1483 }
|
|
|
1484 }
|
|
|
1485 for (unsigned i = 0; i < ec_lhs.m_vars.length (); i++)
|
|
|
1486 {
|
|
|
1487 if (!ec_rhs.m_cst_sid.null_p ())
|
|
|
1488 visitor->on_fact (ec_lhs.m_vars[i], code, ec_rhs.m_cst_sid);
|
|
|
1489 for (unsigned j = 0; j < ec_rhs.m_vars.length (); j++)
|
|
|
1490 visitor->on_fact (ec_lhs.m_vars[i], code, ec_rhs.m_vars[j]);
|
|
|
1491 }
|
|
|
1492 }
|
|
|
1493 }
|
|
|
1494
|
|
|
1495 /* Assert that this object is valid. */
|
|
|
1496
|
|
|
1497 void
|
|
|
1498 constraint_manager::validate () const
|
|
|
1499 {
|
|
|
1500 /* Skip this in a release build. */
|
|
|
1501 #if !CHECKING_P
|
|
|
1502 return;
|
|
|
1503 #endif
|
|
|
1504
|
|
|
1505 int i;
|
|
|
1506 equiv_class *ec;
|
|
|
1507 FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
|
|
|
1508 {
|
|
|
1509 gcc_assert (ec);
|
|
|
1510
|
|
|
1511 int j;
|
|
|
1512 svalue_id *sid;
|
|
|
1513 FOR_EACH_VEC_ELT (ec->m_vars, j, sid)
|
|
|
1514 {
|
|
|
1515 gcc_assert (!sid->null_p ());
|
|
|
1516 gcc_assert (sid->as_int () < get_num_svalues ());
|
|
|
1517 }
|
|
|
1518 if (ec->m_constant)
|
|
|
1519 {
|
|
|
1520 gcc_assert (CONSTANT_CLASS_P (ec->m_constant));
|
|
|
1521 gcc_assert (!ec->m_cst_sid.null_p ());
|
|
|
1522 gcc_assert (ec->m_cst_sid.as_int () < get_num_svalues ());
|
|
|
1523 }
|
|
|
1524 #if 0
|
|
|
1525 else
|
|
|
1526 gcc_assert (ec->m_vars.length () > 0);
|
|
|
1527 #endif
|
|
|
1528 }
|
|
|
1529
|
|
|
1530 constraint *c;
|
|
|
1531 FOR_EACH_VEC_ELT (m_constraints, i, c)
|
|
|
1532 {
|
|
|
1533 gcc_assert (!c->m_lhs.null_p ());
|
|
|
1534 gcc_assert (c->m_lhs.as_int () <= (int)m_equiv_classes.length ());
|
|
|
1535 gcc_assert (!c->m_rhs.null_p ());
|
|
|
1536 gcc_assert (c->m_rhs.as_int () <= (int)m_equiv_classes.length ());
|
|
|
1537 }
|
|
|
1538 }
|
|
|
1539
|
|
|
1540 #if CHECKING_P
|
|
|
1541
|
|
|
1542 namespace selftest {
|
|
|
1543
|
|
|
1544 /* Various constraint_manager selftests.
|
|
|
1545 These have to be written in terms of a region_model, since
|
|
|
1546 the latter is responsible for managing svalue and svalue_id
|
|
|
1547 instances. */
|
|
|
1548
|
|
|
1549 /* Verify that setting and getting simple conditions within a region_model
|
|
|
1550 work (thus exercising the underlying constraint_manager). */
|
|
|
1551
|
|
|
1552 static void
|
|
|
1553 test_constraint_conditions ()
|
|
|
1554 {
|
|
|
1555 tree int_42 = build_int_cst (integer_type_node, 42);
|
|
|
1556 tree int_0 = build_int_cst (integer_type_node, 0);
|
|
|
1557
|
|
|
1558 tree x = build_global_decl ("x", integer_type_node);
|
|
|
1559 tree y = build_global_decl ("y", integer_type_node);
|
|
|
1560 tree z = build_global_decl ("z", integer_type_node);
|
|
|
1561
|
|
|
1562 /* Self-comparisons. */
|
|
|
1563 {
|
|
|
1564 region_model model;
|
|
|
1565 ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, x);
|
|
|
1566 ASSERT_CONDITION_TRUE (model, x, LE_EXPR, x);
|
|
|
1567 ASSERT_CONDITION_TRUE (model, x, GE_EXPR, x);
|
|
|
1568 ASSERT_CONDITION_FALSE (model, x, NE_EXPR, x);
|
|
|
1569 ASSERT_CONDITION_FALSE (model, x, LT_EXPR, x);
|
|
|
1570 ASSERT_CONDITION_FALSE (model, x, GT_EXPR, x);
|
|
|
1571 }
|
|
|
1572
|
|
|
1573 /* x == y. */
|
|
|
1574 {
|
|
|
1575 region_model model;
|
|
|
1576 ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
|
|
|
1577
|
|
|
1578 ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
|
|
|
1579
|
|
|
1580 ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, y);
|
|
|
1581 ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
|
|
|
1582 ASSERT_CONDITION_TRUE (model, x, GE_EXPR, y);
|
|
|
1583 ASSERT_CONDITION_FALSE (model, x, NE_EXPR, y);
|
|
|
1584 ASSERT_CONDITION_FALSE (model, x, LT_EXPR, y);
|
|
|
1585 ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
|
|
|
1586
|
|
|
1587 /* Swapped operands. */
|
|
|
1588 ASSERT_CONDITION_TRUE (model, y, EQ_EXPR, x);
|
|
|
1589 ASSERT_CONDITION_TRUE (model, y, LE_EXPR, x);
|
|
|
1590 ASSERT_CONDITION_TRUE (model, y, GE_EXPR, x);
|
|
|
1591 ASSERT_CONDITION_FALSE (model, y, NE_EXPR, x);
|
|
|
1592 ASSERT_CONDITION_FALSE (model, y, LT_EXPR, x);
|
|
|
1593 ASSERT_CONDITION_FALSE (model, y, GT_EXPR, x);
|
|
|
1594
|
|
|
1595 /* Comparison with other var. */
|
|
|
1596 ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, z);
|
|
|
1597 ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, z);
|
|
|
1598 ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
|
|
|
1599 ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, z);
|
|
|
1600 ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, z);
|
|
|
1601 ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, z);
|
|
|
1602 }
|
|
|
1603
|
|
|
1604 /* x == y, then y == z */
|
|
|
1605 {
|
|
|
1606 region_model model;
|
|
|
1607 ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
|
|
|
1608
|
|
|
1609 ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
|
|
|
1610 ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, z);
|
|
|
1611
|
|
|
1612 ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, z);
|
|
|
1613 ASSERT_CONDITION_TRUE (model, x, LE_EXPR, z);
|
|
|
1614 ASSERT_CONDITION_TRUE (model, x, GE_EXPR, z);
|
|
|
1615 ASSERT_CONDITION_FALSE (model, x, NE_EXPR, z);
|
|
|
1616 ASSERT_CONDITION_FALSE (model, x, LT_EXPR, z);
|
|
|
1617 ASSERT_CONDITION_FALSE (model, x, GT_EXPR, z);
|
|
|
1618 }
|
|
|
1619
|
|
|
1620 /* x != y. */
|
|
|
1621 {
|
|
|
1622 region_model model;
|
|
|
1623
|
|
|
1624 ADD_SAT_CONSTRAINT (model, x, NE_EXPR, y);
|
|
|
1625
|
|
|
1626 ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
|
|
|
1627 ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
|
|
|
1628 ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, y);
|
|
|
1629 ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, y);
|
|
|
1630 ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, y);
|
|
|
1631 ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, y);
|
|
|
1632
|
|
|
1633 /* Swapped operands. */
|
|
|
1634 ASSERT_CONDITION_TRUE (model, y, NE_EXPR, x);
|
|
|
1635 ASSERT_CONDITION_FALSE (model, y, EQ_EXPR, x);
|
|
|
1636 ASSERT_CONDITION_UNKNOWN (model, y, LE_EXPR, x);
|
|
|
1637 ASSERT_CONDITION_UNKNOWN (model, y, GE_EXPR, x);
|
|
|
1638 ASSERT_CONDITION_UNKNOWN (model, y, LT_EXPR, x);
|
|
|
1639 ASSERT_CONDITION_UNKNOWN (model, y, GT_EXPR, x);
|
|
|
1640
|
|
|
1641 /* Comparison with other var. */
|
|
|
1642 ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, z);
|
|
|
1643 ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, z);
|
|
|
1644 ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
|
|
|
1645 ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, z);
|
|
|
1646 ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, z);
|
|
|
1647 ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, z);
|
|
|
1648 }
|
|
|
1649
|
|
|
1650 /* x < y. */
|
|
|
1651 {
|
|
|
1652 region_model model;
|
|
|
1653
|
|
|
1654 ADD_SAT_CONSTRAINT (model, x, LT_EXPR, y);
|
|
|
1655
|
|
|
1656 ASSERT_CONDITION_TRUE (model, x, LT_EXPR, y);
|
|
|
1657 ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
|
|
|
1658 ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
|
|
|
1659 ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
|
|
|
1660 ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
|
|
|
1661 ASSERT_CONDITION_FALSE (model, x, GE_EXPR, y);
|
|
|
1662
|
|
|
1663 /* Swapped operands. */
|
|
|
1664 ASSERT_CONDITION_FALSE (model, y, LT_EXPR, x);
|
|
|
1665 ASSERT_CONDITION_FALSE (model, y, LE_EXPR, x);
|
|
|
1666 ASSERT_CONDITION_TRUE (model, y, NE_EXPR, x);
|
|
|
1667 ASSERT_CONDITION_FALSE (model, y, EQ_EXPR, x);
|
|
|
1668 ASSERT_CONDITION_TRUE (model, y, GT_EXPR, x);
|
|
|
1669 ASSERT_CONDITION_TRUE (model, y, GE_EXPR, x);
|
|
|
1670 }
|
|
|
1671
|
|
|
1672 /* x <= y. */
|
|
|
1673 {
|
|
|
1674 region_model model;
|
|
|
1675
|
|
|
1676 ADD_SAT_CONSTRAINT (model, x, LE_EXPR, y);
|
|
|
1677
|
|
|
1678 ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, y);
|
|
|
1679 ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
|
|
|
1680 ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, y);
|
|
|
1681 ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
|
|
|
1682 ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
|
|
|
1683 ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, y);
|
|
|
1684
|
|
|
1685 /* Swapped operands. */
|
|
|
1686 ASSERT_CONDITION_FALSE (model, y, LT_EXPR, x);
|
|
|
1687 ASSERT_CONDITION_UNKNOWN (model, y, LE_EXPR, x);
|
|
|
1688 ASSERT_CONDITION_UNKNOWN (model, y, NE_EXPR, x);
|
|
|
1689 ASSERT_CONDITION_UNKNOWN (model, y, EQ_EXPR, x);
|
|
|
1690 ASSERT_CONDITION_UNKNOWN (model, y, GT_EXPR, x);
|
|
|
1691 ASSERT_CONDITION_TRUE (model, y, GE_EXPR, x);
|
|
|
1692 }
|
|
|
1693
|
|
|
1694 /* x > y. */
|
|
|
1695 {
|
|
|
1696 region_model model;
|
|
|
1697
|
|
|
1698 ADD_SAT_CONSTRAINT (model, x, GT_EXPR, y);
|
|
|
1699
|
|
|
1700 ASSERT_CONDITION_TRUE (model, x, GT_EXPR, y);
|
|
|
1701 ASSERT_CONDITION_TRUE (model, x, GE_EXPR, y);
|
|
|
1702 ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
|
|
|
1703 ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
|
|
|
1704 ASSERT_CONDITION_FALSE (model, x, LT_EXPR, y);
|
|
|
1705 ASSERT_CONDITION_FALSE (model, x, LE_EXPR, y);
|
|
|
1706
|
|
|
1707 /* Swapped operands. */
|
|
|
1708 ASSERT_CONDITION_FALSE (model, y, GT_EXPR, x);
|
|
|
1709 ASSERT_CONDITION_FALSE (model, y, GE_EXPR, x);
|
|
|
1710 ASSERT_CONDITION_TRUE (model, y, NE_EXPR, x);
|
|
|
1711 ASSERT_CONDITION_FALSE (model, y, EQ_EXPR, x);
|
|
|
1712 ASSERT_CONDITION_TRUE (model, y, LT_EXPR, x);
|
|
|
1713 ASSERT_CONDITION_TRUE (model, y, LE_EXPR, x);
|
|
|
1714 }
|
|
|
1715
|
|
|
1716 /* x >= y. */
|
|
|
1717 {
|
|
|
1718 region_model model;
|
|
|
1719
|
|
|
1720 ADD_SAT_CONSTRAINT (model, x, GE_EXPR, y);
|
|
|
1721
|
|
|
1722 ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, y);
|
|
|
1723 ASSERT_CONDITION_TRUE (model, x, GE_EXPR, y);
|
|
|
1724 ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, y);
|
|
|
1725 ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
|
|
|
1726 ASSERT_CONDITION_FALSE (model, x, LT_EXPR, y);
|
|
|
1727 ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, y);
|
|
|
1728
|
|
|
1729 /* Swapped operands. */
|
|
|
1730 ASSERT_CONDITION_FALSE (model, y, GT_EXPR, x);
|
|
|
1731 ASSERT_CONDITION_UNKNOWN (model, y, GE_EXPR, x);
|
|
|
1732 ASSERT_CONDITION_UNKNOWN (model, y, NE_EXPR, x);
|
|
|
1733 ASSERT_CONDITION_UNKNOWN (model, y, EQ_EXPR, x);
|
|
|
1734 ASSERT_CONDITION_UNKNOWN (model, y, LT_EXPR, x);
|
|
|
1735 ASSERT_CONDITION_TRUE (model, y, LE_EXPR, x);
|
|
|
1736 }
|
|
|
1737
|
|
|
1738 // TODO: implied orderings
|
|
|
1739
|
|
|
1740 /* Constants. */
|
|
|
1741 {
|
|
|
1742 region_model model;
|
|
|
1743 ASSERT_CONDITION_FALSE (model, int_0, EQ_EXPR, int_42);
|
|
|
1744 ASSERT_CONDITION_TRUE (model, int_0, NE_EXPR, int_42);
|
|
|
1745 ASSERT_CONDITION_TRUE (model, int_0, LT_EXPR, int_42);
|
|
|
1746 ASSERT_CONDITION_TRUE (model, int_0, LE_EXPR, int_42);
|
|
|
1747 ASSERT_CONDITION_FALSE (model, int_0, GT_EXPR, int_42);
|
|
|
1748 ASSERT_CONDITION_FALSE (model, int_0, GE_EXPR, int_42);
|
|
|
1749 }
|
|
|
1750
|
|
|
1751 /* x == 0, y == 42. */
|
|
|
1752 {
|
|
|
1753 region_model model;
|
|
|
1754 ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
|
|
|
1755 ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, int_42);
|
|
|
1756
|
|
|
1757 ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
|
|
|
1758 ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
|
|
|
1759 ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
|
|
|
1760 ASSERT_CONDITION_FALSE (model, x, GE_EXPR, y);
|
|
|
1761 ASSERT_CONDITION_TRUE (model, x, LT_EXPR, y);
|
|
|
1762 ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
|
|
|
1763 }
|
|
|
1764
|
|
|
1765 /* Unsatisfiable combinations. */
|
|
|
1766
|
|
|
1767 /* x == y && x != y. */
|
|
|
1768 {
|
|
|
1769 region_model model;
|
|
|
1770 ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
|
|
|
1771 ADD_UNSAT_CONSTRAINT (model, x, NE_EXPR, y);
|
|
|
1772 }
|
|
|
1773
|
|
|
1774 /* x == 0 then x == 42. */
|
|
|
1775 {
|
|
|
1776 region_model model;
|
|
|
1777 ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
|
|
|
1778 ADD_UNSAT_CONSTRAINT (model, x, EQ_EXPR, int_42);
|
|
|
1779 }
|
|
|
1780
|
|
|
1781 /* x == 0 then x != 0. */
|
|
|
1782 {
|
|
|
1783 region_model model;
|
|
|
1784 ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
|
|
|
1785 ADD_UNSAT_CONSTRAINT (model, x, NE_EXPR, int_0);
|
|
|
1786 }
|
|
|
1787
|
|
|
1788 /* x == 0 then x > 0. */
|
|
|
1789 {
|
|
|
1790 region_model model;
|
|
|
1791 ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
|
|
|
1792 ADD_UNSAT_CONSTRAINT (model, x, GT_EXPR, int_0);
|
|
|
1793 }
|
|
|
1794
|
|
|
1795 /* x != y && x == y. */
|
|
|
1796 {
|
|
|
1797 region_model model;
|
|
|
1798 ADD_SAT_CONSTRAINT (model, x, NE_EXPR, y);
|
|
|
1799 ADD_UNSAT_CONSTRAINT (model, x, EQ_EXPR, y);
|
|
|
1800 }
|
|
|
1801
|
|
|
1802 /* x <= y && x > y. */
|
|
|
1803 {
|
|
|
1804 region_model model;
|
|
|
1805 ADD_SAT_CONSTRAINT (model, x, LE_EXPR, y);
|
|
|
1806 ADD_UNSAT_CONSTRAINT (model, x, GT_EXPR, y);
|
|
|
1807 }
|
|
|
1808
|
|
|
1809 // etc
|
|
|
1810 }
|
|
|
1811
|
|
|
1812 /* Test transitivity of conditions. */
|
|
|
1813
|
|
|
1814 static void
|
|
|
1815 test_transitivity ()
|
|
|
1816 {
|
|
|
1817 tree a = build_global_decl ("a", integer_type_node);
|
|
|
1818 tree b = build_global_decl ("b", integer_type_node);
|
|
|
1819 tree c = build_global_decl ("c", integer_type_node);
|
|
|
1820 tree d = build_global_decl ("d", integer_type_node);
|
|
|
1821
|
|
|
1822 /* a == b, then c == d, then c == b. */
|
|
|
1823 {
|
|
|
1824 region_model model;
|
|
|
1825 ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, b);
|
|
|
1826 ASSERT_CONDITION_UNKNOWN (model, b, EQ_EXPR, c);
|
|
|
1827 ASSERT_CONDITION_UNKNOWN (model, c, EQ_EXPR, d);
|
|
|
1828 ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, d);
|
|
|
1829
|
|
|
1830 ADD_SAT_CONSTRAINT (model, a, EQ_EXPR, b);
|
|
|
1831 ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, b);
|
|
|
1832
|
|
|
1833 ADD_SAT_CONSTRAINT (model, c, EQ_EXPR, d);
|
|
|
1834 ASSERT_CONDITION_TRUE (model, c, EQ_EXPR, d);
|
|
|
1835 ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, d);
|
|
|
1836
|
|
|
1837 ADD_SAT_CONSTRAINT (model, c, EQ_EXPR, b);
|
|
|
1838 ASSERT_CONDITION_TRUE (model, c, EQ_EXPR, b);
|
|
|
1839 ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, d);
|
|
|
1840 }
|
|
|
1841
|
|
|
1842 /* Transitivity: "a < b", "b < c" should imply "a < c". */
|
|
|
1843 {
|
|
|
1844 region_model model;
|
|
|
1845 ADD_SAT_CONSTRAINT (model, a, LT_EXPR, b);
|
|
|
1846 ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c);
|
|
|
1847
|
|
|
1848 ASSERT_CONDITION_TRUE (model, a, LT_EXPR, c);
|
|
|
1849 ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
|
|
|
1850 }
|
|
|
1851
|
|
|
1852 /* Transitivity: "a <= b", "b < c" should imply "a < c". */
|
|
|
1853 {
|
|
|
1854 region_model model;
|
|
|
1855 ADD_SAT_CONSTRAINT (model, a, LE_EXPR, b);
|
|
|
1856 ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c);
|
|
|
1857
|
|
|
1858 ASSERT_CONDITION_TRUE (model, a, LT_EXPR, c);
|
|
|
1859 ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
|
|
|
1860 }
|
|
|
1861
|
|
|
1862 /* Transitivity: "a <= b", "b <= c" should imply "a <= c". */
|
|
|
1863 {
|
|
|
1864 region_model model;
|
|
|
1865 ADD_SAT_CONSTRAINT (model, a, LE_EXPR, b);
|
|
|
1866 ADD_SAT_CONSTRAINT (model, b, LE_EXPR, c);
|
|
|
1867
|
|
|
1868 ASSERT_CONDITION_TRUE (model, a, LE_EXPR, c);
|
|
|
1869 ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, c);
|
|
|
1870 }
|
|
|
1871
|
|
|
1872 /* Transitivity: "a > b", "b > c" should imply "a > c". */
|
|
|
1873 {
|
|
|
1874 region_model model;
|
|
|
1875 ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b);
|
|
|
1876 ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c);
|
|
|
1877
|
|
|
1878 ASSERT_CONDITION_TRUE (model, a, GT_EXPR, c);
|
|
|
1879 ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
|
|
|
1880 }
|
|
|
1881
|
|
|
1882 /* Transitivity: "a >= b", "b > c" should imply " a > c". */
|
|
|
1883 {
|
|
|
1884 region_model model;
|
|
|
1885 ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
|
|
|
1886 ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c);
|
|
|
1887
|
|
|
1888 ASSERT_CONDITION_TRUE (model, a, GT_EXPR, c);
|
|
|
1889 ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
|
|
|
1890 }
|
|
|
1891
|
|
|
1892 /* Transitivity: "a >= b", "b >= c" should imply "a >= c". */
|
|
|
1893 {
|
|
|
1894 region_model model;
|
|
|
1895 ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
|
|
|
1896 ADD_SAT_CONSTRAINT (model, b, GE_EXPR, c);
|
|
|
1897
|
|
|
1898 ASSERT_CONDITION_TRUE (model, a, GE_EXPR, c);
|
|
|
1899 ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, c);
|
|
|
1900 }
|
|
|
1901
|
|
|
1902 /* Transitivity: "(a < b)", "(c < d)", "(b < c)" should
|
|
|
1903 imply the easy cases:
|
|
|
1904 (a < c)
|
|
|
1905 (b < d)
|
|
|
1906 but also that:
|
|
|
1907 (a < d). */
|
|
|
1908 {
|
|
|
1909 region_model model;
|
|
|
1910 ADD_SAT_CONSTRAINT (model, a, LT_EXPR, b);
|
|
|
1911 ADD_SAT_CONSTRAINT (model, c, LT_EXPR, d);
|
|
|
1912 ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c);
|
|
|
1913
|
|
|
1914 ASSERT_CONDITION_TRUE (model, a, LT_EXPR, c);
|
|
|
1915 ASSERT_CONDITION_TRUE (model, b, LT_EXPR, d);
|
|
|
1916 ASSERT_CONDITION_TRUE (model, a, LT_EXPR, d);
|
|
|
1917 }
|
|
|
1918
|
|
|
1919 /* Transitivity: "a >= b", "b >= a" should imply that a == b. */
|
|
|
1920 {
|
|
|
1921 region_model model;
|
|
|
1922 ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
|
|
|
1923 ADD_SAT_CONSTRAINT (model, b, GE_EXPR, a);
|
|
|
1924
|
|
|
1925 // TODO:
|
|
|
1926 ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, b);
|
|
|
1927 }
|
|
|
1928
|
|
|
1929 /* Transitivity: "a >= b", "b > a" should be impossible. */
|
|
|
1930 {
|
|
|
1931 region_model model;
|
|
|
1932 ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
|
|
|
1933 ADD_UNSAT_CONSTRAINT (model, b, GT_EXPR, a);
|
|
|
1934 }
|
|
|
1935
|
|
|
1936 /* Transitivity: "a >= b", "b >= c", "c >= a" should imply
|
|
|
1937 that a == b == c. */
|
|
|
1938 {
|
|
|
1939 region_model model;
|
|
|
1940 ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
|
|
|
1941 ADD_SAT_CONSTRAINT (model, b, GE_EXPR, c);
|
|
|
1942 ADD_SAT_CONSTRAINT (model, c, GE_EXPR, a);
|
|
|
1943
|
|
|
1944 ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, c);
|
|
|
1945 }
|
|
|
1946
|
|
|
1947 /* Transitivity: "a > b", "b > c", "c > a"
|
|
|
1948 should be impossible. */
|
|
|
1949 {
|
|
|
1950 region_model model;
|
|
|
1951 ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b);
|
|
|
1952 ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c);
|
|
|
1953 ADD_UNSAT_CONSTRAINT (model, c, GT_EXPR, a);
|
|
|
1954 }
|
|
|
1955
|
|
|
1956 }
|
|
|
1957
|
|
|
1958 /* Test various conditionals involving constants where the results
|
|
|
1959 ought to be implied based on the values of the constants. */
|
|
|
1960
|
|
|
1961 static void
|
|
|
1962 test_constant_comparisons ()
|
|
|
1963 {
|
|
|
1964 tree int_3 = build_int_cst (integer_type_node, 3);
|
|
|
1965 tree int_4 = build_int_cst (integer_type_node, 4);
|
|
|
1966 tree int_5 = build_int_cst (integer_type_node, 5);
|
|
|
1967
|
|
|
1968 tree int_1023 = build_int_cst (integer_type_node, 1023);
|
|
|
1969 tree int_1024 = build_int_cst (integer_type_node, 1024);
|
|
|
1970
|
|
|
1971 tree a = build_global_decl ("a", integer_type_node);
|
|
|
1972 tree b = build_global_decl ("b", integer_type_node);
|
|
|
1973
|
|
|
1974 /* Given a >= 1024, then a <= 1023 should be impossible. */
|
|
|
1975 {
|
|
|
1976 region_model model;
|
|
|
1977 ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_1024);
|
|
|
1978 ADD_UNSAT_CONSTRAINT (model, a, LE_EXPR, int_1023);
|
|
|
1979 }
|
|
|
1980
|
|
|
1981 /* a > 4. */
|
|
|
1982 {
|
|
|
1983 region_model model;
|
|
|
1984 ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_4);
|
|
|
1985 ASSERT_CONDITION_TRUE (model, a, GT_EXPR, int_4);
|
|
|
1986 ASSERT_CONDITION_TRUE (model, a, NE_EXPR, int_3);
|
|
|
1987 ASSERT_CONDITION_UNKNOWN (model, a, NE_EXPR, int_5);
|
|
|
1988 }
|
|
|
1989
|
|
|
1990 /* a <= 4. */
|
|
|
1991 {
|
|
|
1992 region_model model;
|
|
|
1993 ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
|
|
|
1994 ASSERT_CONDITION_FALSE (model, a, GT_EXPR, int_4);
|
|
|
1995 ASSERT_CONDITION_FALSE (model, a, GT_EXPR, int_5);
|
|
|
1996 ASSERT_CONDITION_UNKNOWN (model, a, NE_EXPR, int_3);
|
|
|
1997 }
|
|
|
1998
|
|
|
1999 /* If "a > b" and "a == 3", then "b == 4" ought to be unsatisfiable. */
|
|
|
2000 {
|
|
|
2001 region_model model;
|
|
|
2002 ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b);
|
|
|
2003 ADD_SAT_CONSTRAINT (model, a, EQ_EXPR, int_3);
|
|
|
2004 ADD_UNSAT_CONSTRAINT (model, b, EQ_EXPR, int_4);
|
|
|
2005 }
|
|
|
2006
|
|
|
2007 /* Various tests of int ranges where there is only one possible candidate. */
|
|
|
2008 {
|
|
|
2009 /* If "a <= 4" && "a > 3", then "a == 4",
|
|
|
2010 assuming a is of integral type. */
|
|
|
2011 {
|
|
|
2012 region_model model;
|
|
|
2013 ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
|
|
|
2014 ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
|
|
|
2015 ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
|
|
|
2016 }
|
|
|
2017
|
|
|
2018 /* If "a > 3" && "a <= 4", then "a == 4",
|
|
|
2019 assuming a is of integral type. */
|
|
|
2020 {
|
|
|
2021 region_model model;
|
|
|
2022 ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
|
|
|
2023 ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
|
|
|
2024 ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
|
|
|
2025 }
|
|
|
2026 /* If "a > 3" && "a < 5", then "a == 4",
|
|
|
2027 assuming a is of integral type. */
|
|
|
2028 {
|
|
|
2029 region_model model;
|
|
|
2030 ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
|
|
|
2031 ADD_SAT_CONSTRAINT (model, a, LT_EXPR, int_5);
|
|
|
2032 ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
|
|
|
2033 }
|
|
|
2034 /* If "a >= 4" && "a < 5", then "a == 4",
|
|
|
2035 assuming a is of integral type. */
|
|
|
2036 {
|
|
|
2037 region_model model;
|
|
|
2038 ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_4);
|
|
|
2039 ADD_SAT_CONSTRAINT (model, a, LT_EXPR, int_5);
|
|
|
2040 ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
|
|
|
2041 }
|
|
|
2042 /* If "a >= 4" && "a <= 4", then "a == 4". */
|
|
|
2043 {
|
|
|
2044 region_model model;
|
|
|
2045 ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_4);
|
|
|
2046 ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
|
|
|
2047 ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
|
|
|
2048 }
|
|
|
2049 }
|
|
|
2050
|
|
|
2051 /* As above, but for floating-point:
|
|
|
2052 if "f > 3" && "f <= 4" we don't know that f == 4. */
|
|
|
2053 {
|
|
|
2054 tree f = build_global_decl ("f", double_type_node);
|
|
|
2055 tree float_3 = build_real_from_int_cst (double_type_node, int_3);
|
|
|
2056 tree float_4 = build_real_from_int_cst (double_type_node, int_4);
|
|
|
2057
|
|
|
2058 region_model model;
|
|
|
2059 ADD_SAT_CONSTRAINT (model, f, GT_EXPR, float_3);
|
|
|
2060 ADD_SAT_CONSTRAINT (model, f, LE_EXPR, float_4);
|
|
|
2061 ASSERT_CONDITION_UNKNOWN (model, f, EQ_EXPR, float_4);
|
|
|
2062 ASSERT_CONDITION_UNKNOWN (model, f, EQ_EXPR, int_4);
|
|
|
2063 }
|
|
|
2064 }
|
|
|
2065
|
|
|
2066 /* Verify various lower-level implementation details about
|
|
|
2067 constraint_manager. */
|
|
|
2068
|
|
|
2069 static void
|
|
|
2070 test_constraint_impl ()
|
|
|
2071 {
|
|
|
2072 tree int_42 = build_int_cst (integer_type_node, 42);
|
|
|
2073 tree int_0 = build_int_cst (integer_type_node, 0);
|
|
|
2074
|
|
|
2075 tree x = build_global_decl ("x", integer_type_node);
|
|
|
2076 tree y = build_global_decl ("y", integer_type_node);
|
|
|
2077 tree z = build_global_decl ("z", integer_type_node);
|
|
|
2078
|
|
|
2079 /* x == y. */
|
|
|
2080 {
|
|
|
2081 region_model model;
|
|
|
2082
|
|
|
2083 ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
|
|
|
2084
|
|
|
2085 /* Assert various things about the insides of model. */
|
|
|
2086 constraint_manager *cm = model.get_constraints ();
|
|
|
2087 ASSERT_EQ (cm->m_constraints.length (), 0);
|
|
|
2088 ASSERT_EQ (cm->m_equiv_classes.length (), 1);
|
|
|
2089 }
|
|
|
2090
|
|
|
2091 /* y <= z; x == y. */
|
|
|
2092 {
|
|
|
2093 region_model model;
|
|
|
2094 ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
|
|
|
2095 ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
|
|
|
2096
|
|
|
2097 ADD_SAT_CONSTRAINT (model, y, GE_EXPR, z);
|
|
|
2098 ASSERT_CONDITION_TRUE (model, y, GE_EXPR, z);
|
|
|
2099 ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
|
|
|
2100
|
|
|
2101 ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
|
|
|
2102
|
|
|
2103 /* Assert various things about the insides of model. */
|
|
|
2104 constraint_manager *cm = model.get_constraints ();
|
|
|
2105 ASSERT_EQ (cm->m_constraints.length (), 1);
|
|
|
2106 ASSERT_EQ (cm->m_equiv_classes.length (), 2);
|
|
|
2107
|
|
|
2108 /* Ensure that we merged the constraints. */
|
|
|
2109 ASSERT_CONDITION_TRUE (model, x, GE_EXPR, z);
|
|
|
2110 }
|
|
|
2111
|
|
|
2112 /* y <= z; y == x. */
|
|
|
2113 {
|
|
|
2114 region_model model;
|
|
|
2115 ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
|
|
|
2116 ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
|
|
|
2117
|
|
|
2118 ADD_SAT_CONSTRAINT (model, y, GE_EXPR, z);
|
|
|
2119 ASSERT_CONDITION_TRUE (model, y, GE_EXPR, z);
|
|
|
2120 ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
|
|
|
2121
|
|
|
2122 ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, x);
|
|
|
2123
|
|
|
2124 /* Assert various things about the insides of model. */
|
|
|
2125 constraint_manager *cm = model.get_constraints ();
|
|
|
2126 ASSERT_EQ (cm->m_constraints.length (), 1);
|
|
|
2127 ASSERT_EQ (cm->m_equiv_classes.length (), 2);
|
|
|
2128
|
|
|
2129 /* Ensure that we merged the constraints. */
|
|
|
2130 ASSERT_CONDITION_TRUE (model, x, GE_EXPR, z);
|
|
|
2131 }
|
|
|
2132
|
|
|
2133 /* x == 0, then x != 42. */
|
|
|
2134 {
|
|
|
2135 region_model model;
|
|
|
2136
|
|
|
2137 ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
|
|
|
2138 ADD_SAT_CONSTRAINT (model, x, NE_EXPR, int_42);
|
|
|
2139
|
|
|
2140 /* Assert various things about the insides of model. */
|
|
|
2141 constraint_manager *cm = model.get_constraints ();
|
|
|
2142 ASSERT_EQ (cm->m_constraints.length (), 1);
|
|
|
2143 ASSERT_EQ (cm->m_equiv_classes.length (), 2);
|
|
|
2144 ASSERT_EQ (cm->m_constraints[0].m_lhs,
|
|
|
2145 cm->get_or_add_equiv_class (model.get_rvalue (int_0, NULL)));
|
|
|
2146 ASSERT_EQ (cm->m_constraints[0].m_rhs,
|
|
|
2147 cm->get_or_add_equiv_class (model.get_rvalue (int_42, NULL)));
|
|
|
2148 ASSERT_EQ (cm->m_constraints[0].m_op, CONSTRAINT_LT);
|
|
|
2149 }
|
|
|
2150
|
|
|
2151 // TODO: selftest for merging ecs "in the middle"
|
|
|
2152 // where a non-final one gets overwritten
|
|
|
2153
|
|
|
2154 // TODO: selftest where there are pre-existing constraints
|
|
|
2155 }
|
|
|
2156
|
|
|
2157 /* Check that operator== and hashing works as expected for the
|
|
|
2158 various types. */
|
|
|
2159
|
|
|
2160 static void
|
|
|
2161 test_equality ()
|
|
|
2162 {
|
|
|
2163 tree x = build_global_decl ("x", integer_type_node);
|
|
|
2164 tree y = build_global_decl ("y", integer_type_node);
|
|
|
2165
|
|
|
2166 {
|
|
|
2167 region_model model0;
|
|
|
2168 region_model model1;
|
|
|
2169
|
|
|
2170 constraint_manager *cm0 = model0.get_constraints ();
|
|
|
2171 constraint_manager *cm1 = model1.get_constraints ();
|
|
|
2172
|
|
|
2173 ASSERT_EQ (cm0->hash (), cm1->hash ());
|
|
|
2174 ASSERT_EQ (*cm0, *cm1);
|
|
|
2175
|
|
|
2176 ASSERT_EQ (model0.hash (), model1.hash ());
|
|
|
2177 ASSERT_EQ (model0, model1);
|
|
|
2178
|
|
|
2179 ADD_SAT_CONSTRAINT (model1, x, EQ_EXPR, y);
|
|
|
2180 ASSERT_NE (cm0->hash (), cm1->hash ());
|
|
|
2181 ASSERT_NE (*cm0, *cm1);
|
|
|
2182
|
|
|
2183 ASSERT_NE (model0.hash (), model1.hash ());
|
|
|
2184 ASSERT_NE (model0, model1);
|
|
|
2185
|
|
|
2186 region_model model2;
|
|
|
2187 constraint_manager *cm2 = model2.get_constraints ();
|
|
|
2188 /* Make the same change to cm2. */
|
|
|
2189 ADD_SAT_CONSTRAINT (model2, x, EQ_EXPR, y);
|
|
|
2190 ASSERT_EQ (cm1->hash (), cm2->hash ());
|
|
|
2191 ASSERT_EQ (*cm1, *cm2);
|
|
|
2192
|
|
|
2193 ASSERT_EQ (model1.hash (), model2.hash ());
|
|
|
2194 ASSERT_EQ (model1, model2);
|
|
|
2195 }
|
|
|
2196 }
|
|
|
2197
|
|
|
2198 /* Verify tracking inequality of a variable against many constants. */
|
|
|
2199
|
|
|
2200 static void
|
|
|
2201 test_many_constants ()
|
|
|
2202 {
|
|
|
2203 tree a = build_global_decl ("a", integer_type_node);
|
|
|
2204
|
|
|
2205 region_model model;
|
|
|
2206 auto_vec<tree> constants;
|
|
|
2207 for (int i = 0; i < 20; i++)
|
|
|
2208 {
|
|
|
2209 tree constant = build_int_cst (integer_type_node, i);
|
|
|
2210 constants.safe_push (constant);
|
|
|
2211 ADD_SAT_CONSTRAINT (model, a, NE_EXPR, constant);
|
|
|
2212
|
|
|
2213 /* Merge, and check the result. */
|
|
|
2214 region_model other (model);
|
|
|
2215
|
|
|
2216 region_model merged;
|
|
|
2217 ASSERT_TRUE (model.can_merge_with_p (other, &merged));
|
|
|
2218 model.canonicalize (NULL);
|
|
|
2219 merged.canonicalize (NULL);
|
|
|
2220 ASSERT_EQ (model, merged);
|
|
|
2221
|
|
|
2222 for (int j = 0; j <= i; j++)
|
|
|
2223 ASSERT_CONDITION_TRUE (model, a, NE_EXPR, constants[j]);
|
|
|
2224 }
|
|
|
2225 }
|
|
|
2226
|
|
|
2227 /* Run the selftests in this file, temporarily overriding
|
|
|
2228 flag_analyzer_transitivity with TRANSITIVITY. */
|
|
|
2229
|
|
|
2230 static void
|
|
|
2231 run_constraint_manager_tests (bool transitivity)
|
|
|
2232 {
|
|
|
2233 int saved_flag_analyzer_transitivity = flag_analyzer_transitivity;
|
|
|
2234 flag_analyzer_transitivity = transitivity;
|
|
|
2235
|
|
|
2236 test_constraint_conditions ();
|
|
|
2237 if (flag_analyzer_transitivity)
|
|
|
2238 {
|
|
|
2239 /* These selftests assume transitivity. */
|
|
|
2240 test_transitivity ();
|
|
|
2241 test_constant_comparisons ();
|
|
|
2242 }
|
|
|
2243 test_constraint_impl ();
|
|
|
2244 test_equality ();
|
|
|
2245 test_many_constants ();
|
|
|
2246
|
|
|
2247 flag_analyzer_transitivity = saved_flag_analyzer_transitivity;
|
|
|
2248 }
|
|
|
2249
|
|
|
2250 /* Run all of the selftests within this file. */
|
|
|
2251
|
|
|
2252 void
|
|
|
2253 analyzer_constraint_manager_cc_tests ()
|
|
|
2254 {
|
|
|
2255 /* Run the tests twice: with and without transitivity. */
|
|
|
2256 run_constraint_manager_tests (true);
|
|
|
2257 run_constraint_manager_tests (false);
|
|
|
2258 }
|
|
|
2259
|
|
|
2260 } // namespace selftest
|
|
|
2261
|
|
|
2262 #endif /* CHECKING_P */
|
|
|
2263
|
|
|
2264 } // namespace ana
|
|
|
2265
|
|
|
2266 #endif /* #if ENABLE_ANALYZER */
|
