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
5This file is part of GCC.
6
7GCC is free software; you can redistribute it and/or modify
8it under the terms of the GNU General Public License as published by
9the Free Software Foundation; either version 3, or (at your option)
10any later version.
11
12GCC is distributed in the hope that it will be useful,
13but WITHOUT ANY WARRANTY; without even the implied warranty of
14MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15GNU General Public License for more details.
16
17You should have received a copy of the GNU General Public License
18along 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
50namespace {
51
52// Helper algorithms
53
54template<typename I>
55inline I
56next (I iter)
57{
58 return ++iter;
59}
60
61template<typename I, typename P>
62inline bool
63any_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
74bool prove_implication (tree, tree);
75
76/*---------------------------------------------------------------------------
77 Proof state
78---------------------------------------------------------------------------*/
79
80struct term_entry
81{
82 tree t;
83};
84
85/* Hashing function and equality for constraint entries. */
86
87struct 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. */
107struct 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
128inline
129term_list::term_list ()
130 : seq(), tab (11)
131{
132}
133
134/* Initialize a term list with an initial term. */
135
136inline
137term_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
145inline bool
146term_list::includes (tree t)
147{
148 term_entry ent = {t};
149 return tab.find (&ent);
150}
151
152/* Append a term to the list. */
153inline term_list::iterator
154term_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
163term_list::iterator
164term_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
179term_list::iterator
180term_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
193term_list::iterator
194term_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
207term_list::iterator
208term_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
223struct 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
233struct 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
244inline
245proof_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
253inline proof_state::iterator
254proof_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
264inline proof_state::iterator
265proof_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
297bool
298non_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
324bool
325any_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
334enum proof_result
335{
336 invalid,
337 valid,
338 undecided
339};
340
341proof_result check_term (term_list&, tree);
342
343
344proof_result
345analyze_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
367proof_result
368analyze_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
390proof_result
391search_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
407proof_result
408analyze_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
422proof_result
423analyze_parameterized (term_list& ts, tree t)
424{
425 return check_term (ts, PARM_CONSTR_OPERAND (t));
426}
427
428proof_result
429analyze_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
437proof_result
438analyze_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
446proof_result
447analyze_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
487proof_result
488check_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
503proof_result
504check_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
530proof_result
531check_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
557term_list::iterator
558load_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
566term_list::iterator
567load_parameterized_assumption (term_list& ts, term_list::iterator i)
568{
569 return ts.replace(i, PARM_CONSTR_OPERAND(*i));
570}
571
572term_list::iterator
573load_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
583void
584load_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
610void
611load_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
621void
622explode_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
644bool
645explode_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
665void
666explode_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
683term_list::iterator
684load_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
694void
695load_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
708void
709load_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
727bool
728prove_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
777bool
778subsumes_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
794bool
795subsumes (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}
805