Mercurial > hg > CbC > CbC_gcc
comparison gcc/cp/logic.cc @ 111:04ced10e8804
gcc 7
author | kono |
---|---|
date | Fri, 27 Oct 2017 22:46:09 +0900 |
parents | |
children | 84e7813d76e9 |
comparison
equal
deleted
inserted
replaced
68:561a7518be6b | 111:04ced10e8804 |
---|---|
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 } |