|
111
|
1 /* Derivation and subsumption rules for constraints.
|
|
|
2 Copyright (C) 2013-2017 Free Software Foundation, Inc.
|
|
|
3 Contributed by Andrew Sutton (andrew.n.sutton@gmail.com)
|
|
|
4
|
|
|
5 This file is part of GCC.
|
|
|
6
|
|
|
7 GCC is free software; you can redistribute it and/or modify
|
|
|
8 it 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,
|
|
|
13 but WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
|
14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
|
|
15 GNU General Public License for more details.
|
|
|
16
|
|
|
17 You should have received a copy of the GNU General Public License
|
|
|
18 along with GCC; see the file COPYING3. If not see
|
|
|
19 <http://www.gnu.org/licenses/>. */
|
|
|
20
|
|
|
21 #include "config.h"
|
|
|
22 #define INCLUDE_LIST
|
|
|
23 #include "system.h"
|
|
|
24 #include "coretypes.h"
|
|
|
25 #include "tm.h"
|
|
|
26 #include "timevar.h"
|
|
|
27 #include "hash-set.h"
|
|
|
28 #include "machmode.h"
|
|
|
29 #include "vec.h"
|
|
|
30 #include "double-int.h"
|
|
|
31 #include "input.h"
|
|
|
32 #include "alias.h"
|
|
|
33 #include "symtab.h"
|
|
|
34 #include "wide-int.h"
|
|
|
35 #include "inchash.h"
|
|
|
36 #include "tree.h"
|
|
|
37 #include "stringpool.h"
|
|
|
38 #include "attribs.h"
|
|
|
39 #include "intl.h"
|
|
|
40 #include "flags.h"
|
|
|
41 #include "cp-tree.h"
|
|
|
42 #include "c-family/c-common.h"
|
|
|
43 #include "c-family/c-objc.h"
|
|
|
44 #include "cp-objcp-common.h"
|
|
|
45 #include "tree-inline.h"
|
|
|
46 #include "decl.h"
|
|
|
47 #include "toplev.h"
|
|
|
48 #include "type-utils.h"
|
|
|
49
|
|
|
50 namespace {
|
|
|
51
|
|
|
52 // Helper algorithms
|
|
|
53
|
|
|
54 template<typename I>
|
|
|
55 inline I
|
|
|
56 next (I iter)
|
|
|
57 {
|
|
|
58 return ++iter;
|
|
|
59 }
|
|
|
60
|
|
|
61 template<typename I, typename P>
|
|
|
62 inline bool
|
|
|
63 any_p (I first, I last, P pred)
|
|
|
64 {
|
|
|
65 while (first != last)
|
|
|
66 {
|
|
|
67 if (pred(*first))
|
|
|
68 return true;
|
|
|
69 ++first;
|
|
|
70 }
|
|
|
71 return false;
|
|
|
72 }
|
|
|
73
|
|
|
74 bool prove_implication (tree, tree);
|
|
|
75
|
|
|
76 /*---------------------------------------------------------------------------
|
|
|
77 Proof state
|
|
|
78 ---------------------------------------------------------------------------*/
|
|
|
79
|
|
|
80 struct term_entry
|
|
|
81 {
|
|
|
82 tree t;
|
|
|
83 };
|
|
|
84
|
|
|
85 /* Hashing function and equality for constraint entries. */
|
|
|
86
|
|
|
87 struct term_hasher : ggc_ptr_hash<term_entry>
|
|
|
88 {
|
|
|
89 static hashval_t hash (term_entry *e)
|
|
|
90 {
|
|
|
91 return iterative_hash_template_arg (e->t, 0);
|
|
|
92 }
|
|
|
93
|
|
|
94 static bool equal (term_entry *e1, term_entry *e2)
|
|
|
95 {
|
|
|
96 return cp_tree_equal (e1->t, e2->t);
|
|
|
97 }
|
|
|
98 };
|
|
|
99
|
|
|
100 /* A term list is a list of atomic constraints. It is used
|
|
|
101 to maintain the lists of assumptions and conclusions in a
|
|
|
102 proof goal.
|
|
|
103
|
|
|
104 Each term list maintains an iterator that refers to the current
|
|
|
105 term. This can be used by various tactics to support iteration
|
|
|
106 and stateful manipulation of the list. */
|
|
|
107 struct term_list
|
|
|
108 {
|
|
|
109 typedef std::list<tree>::iterator iterator;
|
|
|
110
|
|
|
111 term_list ();
|
|
|
112 term_list (tree);
|
|
|
113
|
|
|
114 bool includes (tree);
|
|
|
115 iterator insert (iterator, tree);
|
|
|
116 iterator push_back (tree);
|
|
|
117 iterator erase (iterator);
|
|
|
118 iterator replace (iterator, tree);
|
|
|
119 iterator replace (iterator, tree, tree);
|
|
|
120
|
|
|
121 iterator begin() { return seq.begin(); }
|
|
|
122 iterator end() { return seq.end(); }
|
|
|
123
|
|
|
124 std::list<tree> seq;
|
|
|
125 hash_table<term_hasher> tab;
|
|
|
126 };
|
|
|
127
|
|
|
128 inline
|
|
|
129 term_list::term_list ()
|
|
|
130 : seq(), tab (11)
|
|
|
131 {
|
|
|
132 }
|
|
|
133
|
|
|
134 /* Initialize a term list with an initial term. */
|
|
|
135
|
|
|
136 inline
|
|
|
137 term_list::term_list (tree t)
|
|
|
138 : seq (), tab (11)
|
|
|
139 {
|
|
|
140 push_back (t);
|
|
|
141 }
|
|
|
142
|
|
|
143 /* Returns true if T is the in the tree. */
|
|
|
144
|
|
|
145 inline bool
|
|
|
146 term_list::includes (tree t)
|
|
|
147 {
|
|
|
148 term_entry ent = {t};
|
|
|
149 return tab.find (&ent);
|
|
|
150 }
|
|
|
151
|
|
|
152 /* Append a term to the list. */
|
|
|
153 inline term_list::iterator
|
|
|
154 term_list::push_back (tree t)
|
|
|
155 {
|
|
|
156 return insert (end(), t);
|
|
|
157 }
|
|
|
158
|
|
|
159 /* Insert a new (unseen) term T into the list before the proposition
|
|
|
160 indicated by ITER. Returns the iterator to the newly inserted
|
|
|
161 element. */
|
|
|
162
|
|
|
163 term_list::iterator
|
|
|
164 term_list::insert (iterator iter, tree t)
|
|
|
165 {
|
|
|
166 gcc_assert (!includes (t));
|
|
|
167 iter = seq.insert (iter, t);
|
|
|
168 term_entry ent = {t};
|
|
|
169 term_entry** slot = tab.find_slot (&ent, INSERT);
|
|
|
170 term_entry* ptr = ggc_alloc<term_entry> ();
|
|
|
171 *ptr = ent;
|
|
|
172 *slot = ptr;
|
|
|
173 return iter;
|
|
|
174 }
|
|
|
175
|
|
|
176 /* Remove an existing term from the list. Returns an iterator referring
|
|
|
177 to the element after the removed term. This may be end(). */
|
|
|
178
|
|
|
179 term_list::iterator
|
|
|
180 term_list::erase (iterator iter)
|
|
|
181 {
|
|
|
182 gcc_assert (includes (*iter));
|
|
|
183 term_entry ent = {*iter};
|
|
|
184 tab.remove_elt (&ent);
|
|
|
185 iter = seq.erase (iter);
|
|
|
186 return iter;
|
|
|
187 }
|
|
|
188
|
|
|
189 /* Replace the given term with that specified. If the term has
|
|
|
190 been previously seen, do not insert the term. Returns the
|
|
|
191 first iterator past the current term. */
|
|
|
192
|
|
|
193 term_list::iterator
|
|
|
194 term_list::replace (iterator iter, tree t)
|
|
|
195 {
|
|
|
196 iter = erase (iter);
|
|
|
197 if (!includes (t))
|
|
|
198 insert (iter, t);
|
|
|
199 return iter;
|
|
|
200 }
|
|
|
201
|
|
|
202
|
|
|
203 /* Replace the term at the given position by the supplied T1
|
|
|
204 followed by t2. This is used in certain logical operators to
|
|
|
205 load a list of assumptions or conclusions. */
|
|
|
206
|
|
|
207 term_list::iterator
|
|
|
208 term_list::replace (iterator iter, tree t1, tree t2)
|
|
|
209 {
|
|
|
210 iter = erase (iter);
|
|
|
211 if (!includes (t1))
|
|
|
212 insert (iter, t1);
|
|
|
213 if (!includes (t2))
|
|
|
214 insert (iter, t2);
|
|
|
215 return iter;
|
|
|
216 }
|
|
|
217
|
|
|
218 /* A goal (or subgoal) models a sequent of the form
|
|
|
219 'A |- C' where A and C are lists of assumptions and
|
|
|
220 conclusions written as propositions in the constraint
|
|
|
221 language (i.e., lists of trees). */
|
|
|
222
|
|
|
223 struct proof_goal
|
|
|
224 {
|
|
|
225 term_list assumptions;
|
|
|
226 term_list conclusions;
|
|
|
227 };
|
|
|
228
|
|
|
229 /* A proof state owns a list of goals and tracks the
|
|
|
230 current sub-goal. The class also provides facilities
|
|
|
231 for managing subgoals and constructing term lists. */
|
|
|
232
|
|
|
233 struct proof_state : std::list<proof_goal>
|
|
|
234 {
|
|
|
235 proof_state ();
|
|
|
236
|
|
|
237 iterator branch (iterator i);
|
|
|
238 iterator discharge (iterator i);
|
|
|
239 };
|
|
|
240
|
|
|
241 /* Initialize the state with a single empty goal, and set that goal
|
|
|
242 as the current subgoal. */
|
|
|
243
|
|
|
244 inline
|
|
|
245 proof_state::proof_state ()
|
|
|
246 : std::list<proof_goal> (1)
|
|
|
247 { }
|
|
|
248
|
|
|
249
|
|
|
250 /* Branch the current goal by creating a new subgoal, returning a
|
|
|
251 reference to the new object. This does not update the current goal. */
|
|
|
252
|
|
|
253 inline proof_state::iterator
|
|
|
254 proof_state::branch (iterator i)
|
|
|
255 {
|
|
|
256 gcc_assert (i != end());
|
|
|
257 proof_goal& g = *i;
|
|
|
258 return insert (++i, g);
|
|
|
259 }
|
|
|
260
|
|
|
261 /* Discharge the current goal, setting it equal to the
|
|
|
262 next non-satisfied goal. */
|
|
|
263
|
|
|
264 inline proof_state::iterator
|
|
|
265 proof_state::discharge (iterator i)
|
|
|
266 {
|
|
|
267 gcc_assert (i != end());
|
|
|
268 return erase (i);
|
|
|
269 }
|
|
|
270
|
|
|
271
|
|
|
272 /*---------------------------------------------------------------------------
|
|
|
273 Debugging
|
|
|
274 ---------------------------------------------------------------------------*/
|
|
|
275
|
|
|
276 // void
|
|
|
277 // debug (term_list& ts)
|
|
|
278 // {
|
|
|
279 // for (term_list::iterator i = ts.begin(); i != ts.end(); ++i)
|
|
|
280 // verbatim (" # %E", *i);
|
|
|
281 // }
|
|
|
282 //
|
|
|
283 // void
|
|
|
284 // debug (proof_goal& g)
|
|
|
285 // {
|
|
|
286 // debug (g.assumptions);
|
|
|
287 // verbatim (" |-");
|
|
|
288 // debug (g.conclusions);
|
|
|
289 // }
|
|
|
290
|
|
|
291 /*---------------------------------------------------------------------------
|
|
|
292 Atomicity of constraints
|
|
|
293 ---------------------------------------------------------------------------*/
|
|
|
294
|
|
|
295 /* Returns true if T is not an atomic constraint. */
|
|
|
296
|
|
|
297 bool
|
|
|
298 non_atomic_constraint_p (tree t)
|
|
|
299 {
|
|
|
300 switch (TREE_CODE (t))
|
|
|
301 {
|
|
|
302 case PRED_CONSTR:
|
|
|
303 case EXPR_CONSTR:
|
|
|
304 case TYPE_CONSTR:
|
|
|
305 case ICONV_CONSTR:
|
|
|
306 case DEDUCT_CONSTR:
|
|
|
307 case EXCEPT_CONSTR:
|
|
|
308 /* A pack expansion isn't atomic, but it can't decompose to prove an
|
|
|
309 atom, so it shouldn't cause analyze_atom to return undecided. */
|
|
|
310 case EXPR_PACK_EXPANSION:
|
|
|
311 return false;
|
|
|
312 case CHECK_CONSTR:
|
|
|
313 case PARM_CONSTR:
|
|
|
314 case CONJ_CONSTR:
|
|
|
315 case DISJ_CONSTR:
|
|
|
316 return true;
|
|
|
317 default:
|
|
|
318 gcc_unreachable ();
|
|
|
319 }
|
|
|
320 }
|
|
|
321
|
|
|
322 /* Returns true if any constraints in T are not atomic. */
|
|
|
323
|
|
|
324 bool
|
|
|
325 any_non_atomic_constraints_p (term_list& t)
|
|
|
326 {
|
|
|
327 return any_p (t.begin(), t.end(), non_atomic_constraint_p);
|
|
|
328 }
|
|
|
329
|
|
|
330 /*---------------------------------------------------------------------------
|
|
|
331 Proof validations
|
|
|
332 ---------------------------------------------------------------------------*/
|
|
|
333
|
|
|
334 enum proof_result
|
|
|
335 {
|
|
|
336 invalid,
|
|
|
337 valid,
|
|
|
338 undecided
|
|
|
339 };
|
|
|
340
|
|
|
341 proof_result check_term (term_list&, tree);
|
|
|
342
|
|
|
343
|
|
|
344 proof_result
|
|
|
345 analyze_atom (term_list& ts, tree t)
|
|
|
346 {
|
|
|
347 /* FIXME: Hook into special cases, if any. */
|
|
|
348 /*
|
|
|
349 term_list::iterator iter = ts.begin();
|
|
|
350 term_list::iterator end = ts.end();
|
|
|
351 while (iter != end)
|
|
|
352 {
|
|
|
353 ++iter;
|
|
|
354 }
|
|
|
355 */
|
|
|
356
|
|
|
357 if (non_atomic_constraint_p (t))
|
|
|
358 return undecided;
|
|
|
359 if (any_non_atomic_constraints_p (ts))
|
|
|
360 return undecided;
|
|
|
361 return invalid;
|
|
|
362 }
|
|
|
363
|
|
|
364 /* Search for a pack expansion in the list of assumptions that would
|
|
|
365 make this expansion valid. */
|
|
|
366
|
|
|
367 proof_result
|
|
|
368 analyze_pack (term_list& ts, tree t)
|
|
|
369 {
|
|
|
370 tree c1 = normalize_expression (PACK_EXPANSION_PATTERN (t));
|
|
|
371 term_list::iterator iter = ts.begin();
|
|
|
372 term_list::iterator end = ts.end();
|
|
|
373 while (iter != end)
|
|
|
374 {
|
|
|
375 if (TREE_CODE (*iter) == TREE_CODE (t))
|
|
|
376 {
|
|
|
377 tree c2 = normalize_expression (PACK_EXPANSION_PATTERN (*iter));
|
|
|
378 if (prove_implication (c2, c1))
|
|
|
379 return valid;
|
|
|
380 else
|
|
|
381 return invalid;
|
|
|
382 }
|
|
|
383 ++iter;
|
|
|
384 }
|
|
|
385 return invalid;
|
|
|
386 }
|
|
|
387
|
|
|
388 /* Search for concept checks in TS that we know subsume T. */
|
|
|
389
|
|
|
390 proof_result
|
|
|
391 search_known_subsumptions (term_list& ts, tree t)
|
|
|
392 {
|
|
|
393 for (term_list::iterator i = ts.begin(); i != ts.end(); ++i)
|
|
|
394 if (TREE_CODE (*i) == CHECK_CONSTR)
|
|
|
395 {
|
|
|
396 if (bool* b = lookup_subsumption_result (*i, t))
|
|
|
397 return *b ? valid : invalid;
|
|
|
398 }
|
|
|
399 return undecided;
|
|
|
400 }
|
|
|
401
|
|
|
402 /* Determine if the terms in TS provide sufficient support for proving
|
|
|
403 the proposition T. If any term in TS is a concept check that is known
|
|
|
404 to subsume T, then the proof is valid. Otherwise, we have to expand T
|
|
|
405 and continue searching for support. */
|
|
|
406
|
|
|
407 proof_result
|
|
|
408 analyze_check (term_list& ts, tree t)
|
|
|
409 {
|
|
|
410 proof_result r = search_known_subsumptions (ts, t);
|
|
|
411 if (r != undecided)
|
|
|
412 return r;
|
|
|
413
|
|
|
414 tree tmpl = CHECK_CONSTR_CONCEPT (t);
|
|
|
415 tree args = CHECK_CONSTR_ARGS (t);
|
|
|
416 tree c = expand_concept (tmpl, args);
|
|
|
417 return check_term (ts, c);
|
|
|
418 }
|
|
|
419
|
|
|
420 /* Recursively check constraints of the parameterized constraint. */
|
|
|
421
|
|
|
422 proof_result
|
|
|
423 analyze_parameterized (term_list& ts, tree t)
|
|
|
424 {
|
|
|
425 return check_term (ts, PARM_CONSTR_OPERAND (t));
|
|
|
426 }
|
|
|
427
|
|
|
428 proof_result
|
|
|
429 analyze_conjunction (term_list& ts, tree t)
|
|
|
430 {
|
|
|
431 proof_result r = check_term (ts, TREE_OPERAND (t, 0));
|
|
|
432 if (r == invalid || r == undecided)
|
|
|
433 return r;
|
|
|
434 return check_term (ts, TREE_OPERAND (t, 1));
|
|
|
435 }
|
|
|
436
|
|
|
437 proof_result
|
|
|
438 analyze_disjunction (term_list& ts, tree t)
|
|
|
439 {
|
|
|
440 proof_result r = check_term (ts, TREE_OPERAND (t, 0));
|
|
|
441 if (r == valid)
|
|
|
442 return r;
|
|
|
443 return check_term (ts, TREE_OPERAND (t, 1));
|
|
|
444 }
|
|
|
445
|
|
|
446 proof_result
|
|
|
447 analyze_term (term_list& ts, tree t)
|
|
|
448 {
|
|
|
449 switch (TREE_CODE (t))
|
|
|
450 {
|
|
|
451 case CHECK_CONSTR:
|
|
|
452 return analyze_check (ts, t);
|
|
|
453
|
|
|
454 case PARM_CONSTR:
|
|
|
455 return analyze_parameterized (ts, t);
|
|
|
456
|
|
|
457 case CONJ_CONSTR:
|
|
|
458 return analyze_conjunction (ts, t);
|
|
|
459 case DISJ_CONSTR:
|
|
|
460 return analyze_disjunction (ts, t);
|
|
|
461
|
|
|
462 case PRED_CONSTR:
|
|
|
463 case EXPR_CONSTR:
|
|
|
464 case TYPE_CONSTR:
|
|
|
465 case ICONV_CONSTR:
|
|
|
466 case DEDUCT_CONSTR:
|
|
|
467 case EXCEPT_CONSTR:
|
|
|
468 return analyze_atom (ts, t);
|
|
|
469
|
|
|
470 case EXPR_PACK_EXPANSION:
|
|
|
471 return analyze_pack (ts, t);
|
|
|
472
|
|
|
473 case ERROR_MARK:
|
|
|
474 /* Encountering an error anywhere in a constraint invalidates
|
|
|
475 the proof, since the constraint is ill-formed. */
|
|
|
476 return invalid;
|
|
|
477 default:
|
|
|
478 gcc_unreachable ();
|
|
|
479 }
|
|
|
480 }
|
|
|
481
|
|
|
482 /* Check if a single term can be proven from a set of assumptions.
|
|
|
483 If the proof is not valid, then it is incomplete when either
|
|
|
484 the given term is non-atomic or any term in the list of assumptions
|
|
|
485 is not-atomic. */
|
|
|
486
|
|
|
487 proof_result
|
|
|
488 check_term (term_list& ts, tree t)
|
|
|
489 {
|
|
|
490 /* Try the easy way; search for an equivalent term. */
|
|
|
491 if (ts.includes (t))
|
|
|
492 return valid;
|
|
|
493
|
|
|
494 /* The hard way; actually consider what the term means. */
|
|
|
495 return analyze_term (ts, t);
|
|
|
496 }
|
|
|
497
|
|
|
498 /* Check to see if any term is proven by the assumptions in the
|
|
|
499 proof goal. The proof is valid if the proof of any term is valid.
|
|
|
500 If validity cannot be determined, but any particular
|
|
|
501 check was undecided, then this goal is undecided. */
|
|
|
502
|
|
|
503 proof_result
|
|
|
504 check_goal (proof_goal& g)
|
|
|
505 {
|
|
|
506 term_list::iterator iter = g.conclusions.begin ();
|
|
|
507 term_list::iterator end = g.conclusions.end ();
|
|
|
508 bool incomplete = false;
|
|
|
509 while (iter != end)
|
|
|
510 {
|
|
|
511 proof_result r = check_term (g.assumptions, *iter);
|
|
|
512 if (r == valid)
|
|
|
513 return r;
|
|
|
514 if (r == undecided)
|
|
|
515 incomplete = true;
|
|
|
516 ++iter;
|
|
|
517 }
|
|
|
518
|
|
|
519 /* Was the proof complete? */
|
|
|
520 if (incomplete)
|
|
|
521 return undecided;
|
|
|
522 else
|
|
|
523 return invalid;
|
|
|
524 }
|
|
|
525
|
|
|
526 /* Check if the the proof is valid. This is the case when all
|
|
|
527 goals can be discharged. If any goal is invalid, then the
|
|
|
528 entire proof is invalid. Otherwise, the proof is undecided. */
|
|
|
529
|
|
|
530 proof_result
|
|
|
531 check_proof (proof_state& p)
|
|
|
532 {
|
|
|
533 proof_state::iterator iter = p.begin();
|
|
|
534 proof_state::iterator end = p.end();
|
|
|
535 while (iter != end)
|
|
|
536 {
|
|
|
537 proof_result r = check_goal (*iter);
|
|
|
538 if (r == invalid)
|
|
|
539 return r;
|
|
|
540 if (r == valid)
|
|
|
541 iter = p.discharge (iter);
|
|
|
542 else
|
|
|
543 ++iter;
|
|
|
544 }
|
|
|
545
|
|
|
546 /* If all goals are discharged, then the proof is valid. */
|
|
|
547 if (p.empty())
|
|
|
548 return valid;
|
|
|
549 else
|
|
|
550 return undecided;
|
|
|
551 }
|
|
|
552
|
|
|
553 /*---------------------------------------------------------------------------
|
|
|
554 Left logical rules
|
|
|
555 ---------------------------------------------------------------------------*/
|
|
|
556
|
|
|
557 term_list::iterator
|
|
|
558 load_check_assumption (term_list& ts, term_list::iterator i)
|
|
|
559 {
|
|
|
560 tree decl = CHECK_CONSTR_CONCEPT (*i);
|
|
|
561 tree tmpl = DECL_TI_TEMPLATE (decl);
|
|
|
562 tree args = CHECK_CONSTR_ARGS (*i);
|
|
|
563 return ts.replace(i, expand_concept (tmpl, args));
|
|
|
564 }
|
|
|
565
|
|
|
566 term_list::iterator
|
|
|
567 load_parameterized_assumption (term_list& ts, term_list::iterator i)
|
|
|
568 {
|
|
|
569 return ts.replace(i, PARM_CONSTR_OPERAND(*i));
|
|
|
570 }
|
|
|
571
|
|
|
572 term_list::iterator
|
|
|
573 load_conjunction_assumption (term_list& ts, term_list::iterator i)
|
|
|
574 {
|
|
|
575 tree t1 = TREE_OPERAND (*i, 0);
|
|
|
576 tree t2 = TREE_OPERAND (*i, 1);
|
|
|
577 return ts.replace(i, t1, t2);
|
|
|
578 }
|
|
|
579
|
|
|
580 /* Examine the terms in the list, and apply left-logical rules to move
|
|
|
581 terms into the set of assumptions. */
|
|
|
582
|
|
|
583 void
|
|
|
584 load_assumptions (proof_goal& g)
|
|
|
585 {
|
|
|
586 term_list::iterator iter = g.assumptions.begin();
|
|
|
587 term_list::iterator end = g.assumptions.end();
|
|
|
588 while (iter != end)
|
|
|
589 {
|
|
|
590 switch (TREE_CODE (*iter))
|
|
|
591 {
|
|
|
592 case CHECK_CONSTR:
|
|
|
593 iter = load_check_assumption (g.assumptions, iter);
|
|
|
594 break;
|
|
|
595 case PARM_CONSTR:
|
|
|
596 iter = load_parameterized_assumption (g.assumptions, iter);
|
|
|
597 break;
|
|
|
598 case CONJ_CONSTR:
|
|
|
599 iter = load_conjunction_assumption (g.assumptions, iter);
|
|
|
600 break;
|
|
|
601 default:
|
|
|
602 ++iter;
|
|
|
603 break;
|
|
|
604 }
|
|
|
605 }
|
|
|
606 }
|
|
|
607
|
|
|
608 /* In each subgoal, load constraints into the assumption set. */
|
|
|
609
|
|
|
610 void
|
|
|
611 load_assumptions(proof_state& p)
|
|
|
612 {
|
|
|
613 proof_state::iterator iter = p.begin();
|
|
|
614 while (iter != p.end())
|
|
|
615 {
|
|
|
616 load_assumptions (*iter);
|
|
|
617 ++iter;
|
|
|
618 }
|
|
|
619 }
|
|
|
620
|
|
|
621 void
|
|
|
622 explode_disjunction (proof_state& p, proof_state::iterator gi, term_list::iterator ti1)
|
|
|
623 {
|
|
|
624 tree t1 = TREE_OPERAND (*ti1, 0);
|
|
|
625 tree t2 = TREE_OPERAND (*ti1, 1);
|
|
|
626
|
|
|
627 /* Erase the current term from the goal. */
|
|
|
628 proof_goal& g1 = *gi;
|
|
|
629 proof_goal& g2 = *p.branch (gi);
|
|
|
630
|
|
|
631 /* Get an iterator to the equivalent position in th enew goal. */
|
|
|
632 int n = std::distance (g1.assumptions.begin (), ti1);
|
|
|
633 term_list::iterator ti2 = g2.assumptions.begin ();
|
|
|
634 std::advance (ti2, n);
|
|
|
635
|
|
|
636 /* Replace the disjunction in both branches. */
|
|
|
637 g1.assumptions.replace (ti1, t1);
|
|
|
638 g2.assumptions.replace (ti2, t2);
|
|
|
639 }
|
|
|
640
|
|
|
641
|
|
|
642 /* Search the assumptions of the goal for the first disjunction. */
|
|
|
643
|
|
|
644 bool
|
|
|
645 explode_goal (proof_state& p, proof_state::iterator gi)
|
|
|
646 {
|
|
|
647 term_list& ts = gi->assumptions;
|
|
|
648 term_list::iterator ti = ts.begin();
|
|
|
649 term_list::iterator end = ts.end();
|
|
|
650 while (ti != end)
|
|
|
651 {
|
|
|
652 if (TREE_CODE (*ti) == DISJ_CONSTR)
|
|
|
653 {
|
|
|
654 explode_disjunction (p, gi, ti);
|
|
|
655 return true;
|
|
|
656 }
|
|
|
657 else ++ti;
|
|
|
658 }
|
|
|
659 return false;
|
|
|
660 }
|
|
|
661
|
|
|
662 /* Search for the first goal with a disjunction, and then branch
|
|
|
663 creating a clone of that subgoal. */
|
|
|
664
|
|
|
665 void
|
|
|
666 explode_assumptions (proof_state& p)
|
|
|
667 {
|
|
|
668 proof_state::iterator iter = p.begin();
|
|
|
669 proof_state::iterator end = p.end();
|
|
|
670 while (iter != end)
|
|
|
671 {
|
|
|
672 if (explode_goal (p, iter))
|
|
|
673 return;
|
|
|
674 ++iter;
|
|
|
675 }
|
|
|
676 }
|
|
|
677
|
|
|
678
|
|
|
679 /*---------------------------------------------------------------------------
|
|
|
680 Right logical rules
|
|
|
681 ---------------------------------------------------------------------------*/
|
|
|
682
|
|
|
683 term_list::iterator
|
|
|
684 load_disjunction_conclusion (term_list& g, term_list::iterator i)
|
|
|
685 {
|
|
|
686 tree t1 = TREE_OPERAND (*i, 0);
|
|
|
687 tree t2 = TREE_OPERAND (*i, 1);
|
|
|
688 return g.replace(i, t1, t2);
|
|
|
689 }
|
|
|
690
|
|
|
691 /* Apply logical rules to the right hand side. This will load the
|
|
|
692 conclusion set with all tpp-level disjunctions. */
|
|
|
693
|
|
|
694 void
|
|
|
695 load_conclusions (proof_goal& g)
|
|
|
696 {
|
|
|
697 term_list::iterator iter = g.conclusions.begin();
|
|
|
698 term_list::iterator end = g.conclusions.end();
|
|
|
699 while (iter != end)
|
|
|
700 {
|
|
|
701 if (TREE_CODE (*iter) == DISJ_CONSTR)
|
|
|
702 iter = load_disjunction_conclusion (g.conclusions, iter);
|
|
|
703 else
|
|
|
704 ++iter;
|
|
|
705 }
|
|
|
706 }
|
|
|
707
|
|
|
708 void
|
|
|
709 load_conclusions (proof_state& p)
|
|
|
710 {
|
|
|
711 proof_state::iterator iter = p.begin();
|
|
|
712 while (iter != p.end())
|
|
|
713 {
|
|
|
714 load_conclusions (*iter);
|
|
|
715 ++iter;
|
|
|
716 }
|
|
|
717 }
|
|
|
718
|
|
|
719
|
|
|
720 /*---------------------------------------------------------------------------
|
|
|
721 High-level proof tactics
|
|
|
722 ---------------------------------------------------------------------------*/
|
|
|
723
|
|
|
724 /* Given two constraints A and C, try to derive a proof that
|
|
|
725 A implies C. */
|
|
|
726
|
|
|
727 bool
|
|
|
728 prove_implication (tree a, tree c)
|
|
|
729 {
|
|
|
730 /* Quick accept. */
|
|
|
731 if (cp_tree_equal (a, c))
|
|
|
732 return true;
|
|
|
733
|
|
|
734 /* Build the initial proof state. */
|
|
|
735 proof_state proof;
|
|
|
736 proof_goal& goal = proof.front();
|
|
|
737 goal.assumptions.push_back(a);
|
|
|
738 goal.conclusions.push_back(c);
|
|
|
739
|
|
|
740 /* Perform an initial right-expansion in the off-chance that the right
|
|
|
741 hand side contains disjunctions. */
|
|
|
742 load_conclusions (proof);
|
|
|
743
|
|
|
744 int step_max = 1 << 10;
|
|
|
745 int step_count = 0; /* FIXME: We shouldn't have this. */
|
|
|
746 std::size_t branch_limit = 1024; /* FIXME: This needs to be configurable. */
|
|
|
747 while (step_count < step_max && proof.size() < branch_limit)
|
|
|
748 {
|
|
|
749 /* Determine if we can prove that the assumptions entail the
|
|
|
750 conclusions. If so, we're done. */
|
|
|
751 load_assumptions (proof);
|
|
|
752
|
|
|
753 /* Can we solve the proof based on this? */
|
|
|
754 proof_result r = check_proof (proof);
|
|
|
755 if (r != undecided)
|
|
|
756 return r == valid;
|
|
|
757
|
|
|
758 /* If not, then we need to dig into disjunctions. */
|
|
|
759 explode_assumptions (proof);
|
|
|
760
|
|
|
761 ++step_count;
|
|
|
762 }
|
|
|
763
|
|
|
764 if (step_count == step_max)
|
|
|
765 error ("subsumption failed to resolve");
|
|
|
766
|
|
|
767 if (proof.size() == branch_limit)
|
|
|
768 error ("exceeded maximum number of branches");
|
|
|
769
|
|
|
770 return false;
|
|
|
771 }
|
|
|
772
|
|
|
773 /* Returns true if the LEFT constraint subsume the RIGHT constraints.
|
|
|
774 This is done by deriving a proof of the conclusions on the RIGHT
|
|
|
775 from the assumptions on the LEFT assumptions. */
|
|
|
776
|
|
|
777 bool
|
|
|
778 subsumes_constraints_nonnull (tree left, tree right)
|
|
|
779 {
|
|
|
780 gcc_assert (check_constraint_info (left));
|
|
|
781 gcc_assert (check_constraint_info (right));
|
|
|
782
|
|
|
783 auto_timevar time (TV_CONSTRAINT_SUB);
|
|
|
784 tree a = CI_ASSOCIATED_CONSTRAINTS (left);
|
|
|
785 tree c = CI_ASSOCIATED_CONSTRAINTS (right);
|
|
|
786 return prove_implication (a, c);
|
|
|
787 }
|
|
|
788
|
|
|
789 } /* namespace */
|
|
|
790
|
|
|
791 /* Returns true if the LEFT constraints subsume the RIGHT
|
|
|
792 constraints. */
|
|
|
793
|
|
|
794 bool
|
|
|
795 subsumes (tree left, tree right)
|
|
|
796 {
|
|
|
797 if (left == right)
|
|
|
798 return true;
|
|
|
799 if (!left)
|
|
|
800 return false;
|
|
|
801 if (!right)
|
|
|
802 return true;
|
|
|
803 return subsumes_constraints_nonnull (left, right);
|
|
|
804 }
|
