1 /* Derivation and subsumption rules for constraints.
2 Copyright (C) 2013-2020 Free Software Foundation, Inc.
3 Contributed by Andrew Sutton (andrew.n.sutton@gmail.com)
5 This file is part of GCC.
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)
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.
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/>. */
24 #include "coretypes.h"
30 #include "double-int.h"
37 #include "stringpool.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"
48 #include "type-utils.h"
50 /* Hash functions for atomic constrains. */
52 struct constraint_hash
: default_hash_traits
<tree
>
54 static hashval_t
hash (tree t
)
56 return hash_atomic_constraint (t
);
59 static bool equal (tree t1
, tree t2
)
61 return atomic_constraints_identical_p (t1
, t2
);
65 /* A conjunctive or disjunctive clause.
67 Each clause maintains an iterator that refers to the current
68 term, which is used in the linear decomposition of a formula
73 typedef std::list
<tree
>::iterator iterator
;
74 typedef std::list
<tree
>::const_iterator const_iterator
;
76 /* Initialize a clause with an initial term. */
80 m_terms
.push_back (t
);
81 if (TREE_CODE (t
) == ATOMIC_CONSTR
)
84 m_current
= m_terms
.begin ();
87 /* Create a copy of the current term. The current
88 iterator is set to point to the same position in the
89 copied list of terms. */
91 clause (clause
const& c
)
92 : m_terms (c
.m_terms
), m_set (c
.m_set
), m_current (m_terms
.begin ())
94 std::advance (m_current
, std::distance (c
.begin (), c
.current ()));
97 /* Returns true when all terms are atoms. */
101 return m_current
== end ();
104 /* Advance to the next term. */
108 gcc_assert (!done ());
112 /* Replaces the current term at position ITER with T. If
113 T is an atomic constraint that already appears in the
114 clause, remove but do not replace ITER. Returns a pair
115 containing an iterator to the replace object or past
116 the erased object and a boolean value which is true if
117 an object was erased. */
119 std::pair
<iterator
, bool> replace (iterator iter
, tree t
)
121 gcc_assert (TREE_CODE (*iter
) != ATOMIC_CONSTR
);
122 if (TREE_CODE (t
) == ATOMIC_CONSTR
)
125 return std::make_pair (m_terms
.erase (iter
), true);
128 return std::make_pair (iter
, false);
131 /* Inserts T before ITER in the list of terms. If T has
132 already is an atomic constraint that already appears in
133 the clause, no action is taken, and the current iterator
134 is returned. Returns a pair of an iterator to the inserted
135 object or ITER if no insertion occurred and a boolean
136 value which is true if an object was inserted. */
138 std::pair
<iterator
, bool> insert (iterator iter
, tree t
)
140 if (TREE_CODE (t
) == ATOMIC_CONSTR
)
143 return std::make_pair (iter
, false);
145 return std::make_pair (m_terms
.insert (iter
, t
), true);
148 /* Replaces the current term with T. In the case where the
149 current term is erased (because T is redundant), update
150 the position of the current term to the next term. */
152 void replace (tree t
)
154 m_current
= replace (m_current
, t
).first
;
157 /* Replace the current term with T1 and T2, in that order. */
159 void replace (tree t1
, tree t2
)
161 /* Replace the current term with t1. Ensure that iter points
162 to the term before which t2 will be inserted. Update the
163 current term as needed. */
164 std::pair
<iterator
, bool> rep
= replace (m_current
, t1
);
166 m_current
= rep
.first
;
170 /* Insert the t2. Make this the current term if we erased
172 std::pair
<iterator
, bool> ins
= insert (rep
.first
, t2
);
173 if (rep
.second
&& ins
.second
)
174 m_current
= ins
.first
;
177 /* Returns true if the clause contains the term T. */
179 bool contains (tree t
)
181 gcc_assert (TREE_CODE (t
) == ATOMIC_CONSTR
);
182 return m_set
.contains (t
);
186 /* Returns an iterator to the first clause in the formula. */
190 return m_terms
.begin ();
193 /* Returns an iterator to the first clause in the formula. */
195 const_iterator
begin () const
197 return m_terms
.begin ();
200 /* Returns an iterator past the last clause in the formula. */
204 return m_terms
.end ();
207 /* Returns an iterator past the last clause in the formula. */
209 const_iterator
end () const
211 return m_terms
.end ();
214 /* Returns the current iterator. */
216 const_iterator
current () const
221 std::list
<tree
> m_terms
; /* The list of terms. */
222 hash_set
<tree
, false, constraint_hash
> m_set
; /* The set of atomic constraints. */
223 iterator m_current
; /* The current term. */
227 /* A proof state owns a list of goals and tracks the
228 current sub-goal. The class also provides facilities
229 for managing subgoals and constructing term lists. */
233 typedef std::list
<clause
>::iterator iterator
;
234 typedef std::list
<clause
>::const_iterator const_iterator
;
236 /* Construct a formula with an initial formula in a
241 /* This should call emplace_back(). There's an extra copy being
242 invoked by using push_back(). */
243 m_clauses
.push_back (t
);
244 m_current
= m_clauses
.begin ();
247 /* Returns true when all clauses are atomic. */
250 return m_current
== end ();
253 /* Advance to the next term. */
256 gcc_assert (!done ());
260 /* Insert a copy of clause into the formula. This corresponds
261 to a distribution of one logical operation over the other. */
265 gcc_assert (!done ());
266 m_clauses
.push_back (*m_current
);
267 return m_clauses
.back ();
270 /* Returns the position of the current clause. */
277 /* Returns an iterator to the first clause in the formula. */
281 return m_clauses
.begin ();
284 /* Returns an iterator to the first clause in the formula. */
286 const_iterator
begin () const
288 return m_clauses
.begin ();
291 /* Returns an iterator past the last clause in the formula. */
295 return m_clauses
.end ();
298 /* Returns an iterator past the last clause in the formula. */
300 const_iterator
end () const
302 return m_clauses
.end ();
305 std::list
<clause
> m_clauses
; /* The list of clauses. */
306 iterator m_current
; /* The current clause. */
312 for (clause::iterator i
= c
.begin(); i
!= c
.end(); ++i
)
313 verbatim (" # %E", *i
);
319 for (formula::iterator i
= f
.begin(); i
!= f
.end(); ++i
)
327 /* The logical rules used to analyze a logical formula. The
328 "left" and "right" refer to the position of formula in a
329 sequent (as in sequent calculus). */
336 /* Distribution counting. */
339 disjunction_p (tree t
)
341 return TREE_CODE (t
) == DISJ_CONSTR
;
345 conjunction_p (tree t
)
347 return TREE_CODE (t
) == CONJ_CONSTR
;
353 return TREE_CODE (t
) == ATOMIC_CONSTR
;
356 /* Recursively count the number of clauses produced when converting T
357 to DNF. Returns a pair containing the number of clauses and a bool
358 value signifying that the tree would be rewritten as a result of
359 distributing. In general, a conjunction for which this flag is set
360 is considered a disjunction for the purpose of counting. */
362 static std::pair
<int, bool>
366 /* Atomic constraints produce no clauses. */
367 return std::make_pair (0, false);
369 /* For compound constraints, recursively count clauses and unpack
371 tree lhs
= TREE_OPERAND (t
, 0);
372 tree rhs
= TREE_OPERAND (t
, 1);
373 std::pair
<int, bool> p1
= dnf_size_r (lhs
);
374 std::pair
<int, bool> p2
= dnf_size_r (rhs
);
375 int n1
= p1
.first
, n2
= p2
.first
;
376 bool d1
= p1
.second
, d2
= p2
.second
;
378 if (disjunction_p (t
))
380 /* Matches constraints of the form P \/ Q. Disjunctions contribute
381 linearly to the number of constraints. When both P and Q are
382 disjunctions, clauses are added. When only one of P and Q
383 is a disjunction, an additional clause is produced. When neither
384 P nor Q are disjunctions, two clauses are produced. */
385 if (disjunction_p (lhs
))
387 if (disjunction_p (rhs
) || (conjunction_p (rhs
) && d2
))
388 /* Both P and Q are disjunctions. */
389 return std::make_pair (n1
+ n2
, d1
| d2
);
391 /* Only LHS is a disjunction. */
392 return std::make_pair (1 + n1
+ n2
, d1
| d2
);
395 if (conjunction_p (lhs
))
397 if ((disjunction_p (rhs
) && d1
) || (conjunction_p (rhs
) && d1
&& d2
))
398 /* Both P and Q are disjunctions. */
399 return std::make_pair (n1
+ n2
, d1
| d2
);
400 if (disjunction_p (rhs
)
401 || (conjunction_p (rhs
) && d1
!= d2
)
402 || (atomic_p (rhs
) && d1
))
403 /* Either LHS or RHS is a disjunction. */
404 return std::make_pair (1 + n1
+ n2
, d1
| d2
);
406 /* Neither LHS nor RHS is a disjunction. */
407 return std::make_pair (2, false);
411 if (disjunction_p (rhs
) || (conjunction_p (rhs
) && d2
))
412 /* Only RHS is a disjunction. */
413 return std::make_pair (1 + n1
+ n2
, d1
| d2
);
415 /* Neither LHS nor RHS is a disjunction. */
416 return std::make_pair (2, false);
419 else /* conjunction_p (t) */
421 /* Matches constraints of the form P /\ Q, possibly resulting
422 in the distribution of one side over the other. When both
423 P and Q are disjunctions, the number of clauses are multiplied.
424 When only one of P and Q is a disjunction, the number of
425 clauses are added. Otherwise, neither side is a disjunction and
426 no clauses are created. */
427 if (disjunction_p (lhs
))
429 if (disjunction_p (rhs
) || (conjunction_p (rhs
) && d2
))
430 /* Both P and Q are disjunctions. */
431 return std::make_pair (n1
* n2
, true);
433 /* Only LHS is a disjunction. */
434 return std::make_pair (n1
+ n2
, true);
437 if (conjunction_p (lhs
))
439 if ((disjunction_p (rhs
) && d1
) || (conjunction_p (rhs
) && d1
&& d2
))
440 /* Both P and Q are disjunctions. */
441 return std::make_pair (n1
* n2
, true);
442 if (disjunction_p (rhs
)
443 || (conjunction_p (rhs
) && d1
!= d2
)
444 || (atomic_p (rhs
) && d1
))
445 /* Either LHS or RHS is a disjunction. */
446 return std::make_pair (n1
+ n2
, true);
448 /* Neither LHS nor RHS is a disjunction. */
449 return std::make_pair (0, false);
453 if (disjunction_p (rhs
) || (conjunction_p (rhs
) && d2
))
454 /* Only RHS is a disjunction. */
455 return std::make_pair (n1
+ n2
, true);
457 /* Neither LHS nor RHS is a disjunction. */
458 return std::make_pair (0, false);
464 /* Recursively count the number of clauses produced when converting T
465 to CNF. Returns a pair containing the number of clauses and a bool
466 value signifying that the tree would be rewritten as a result of
467 distributing. In general, a disjunction for which this flag is set
468 is considered a conjunction for the purpose of counting. */
470 static std::pair
<int, bool>
474 /* Atomic constraints produce no clauses. */
475 return std::make_pair (0, false);
477 /* For compound constraints, recursively count clauses and unpack
479 tree lhs
= TREE_OPERAND (t
, 0);
480 tree rhs
= TREE_OPERAND (t
, 1);
481 std::pair
<int, bool> p1
= cnf_size_r (lhs
);
482 std::pair
<int, bool> p2
= cnf_size_r (rhs
);
483 int n1
= p1
.first
, n2
= p2
.first
;
484 bool d1
= p1
.second
, d2
= p2
.second
;
486 if (disjunction_p (t
))
488 /* Matches constraints of the form P \/ Q, possibly resulting
489 in the distribution of one side over the other. When both
490 P and Q are conjunctions, the number of clauses are multiplied.
491 When only one of P and Q is a conjunction, the number of
492 clauses are added. Otherwise, neither side is a conjunction and
493 no clauses are created. */
494 if (disjunction_p (lhs
))
496 if ((disjunction_p (rhs
) && d1
&& d2
) || (conjunction_p (rhs
) && d1
))
497 /* Both P and Q are conjunctions. */
498 return std::make_pair (n1
* n2
, true);
499 if ((disjunction_p (rhs
) && d1
!= d2
)
500 || conjunction_p (rhs
)
501 || (atomic_p (rhs
) && d1
))
502 /* Either LHS or RHS is a conjunction. */
503 return std::make_pair (n1
+ n2
, true);
505 /* Neither LHS nor RHS is a conjunction. */
506 return std::make_pair (0, false);
509 if (conjunction_p (lhs
))
511 if ((disjunction_p (rhs
) && d2
) || conjunction_p (rhs
))
512 /* Both LHS and RHS are conjunctions. */
513 return std::make_pair (n1
* n2
, true);
515 /* Only LHS is a conjunction. */
516 return std::make_pair (n1
+ n2
, true);
520 if ((disjunction_p (rhs
) && d2
) || conjunction_p (rhs
))
521 /* Only RHS is a disjunction. */
522 return std::make_pair (n1
+ n2
, true);
524 /* Neither LHS nor RHS is a disjunction. */
525 return std::make_pair (0, false);
528 else /* conjunction_p (t) */
530 /* Matches constraints of the form P /\ Q. Conjunctions contribute
531 linearly to the number of constraints. When both P and Q are
532 conjunctions, clauses are added. When only one of P and Q
533 is a conjunction, an additional clause is produced. When neither
534 P nor Q are conjunctions, two clauses are produced. */
535 if (disjunction_p (lhs
))
537 if ((disjunction_p (rhs
) && d1
&& d2
) || (conjunction_p (rhs
) && d1
))
538 /* Both P and Q are conjunctions. */
539 return std::make_pair (n1
+ n2
, d1
| d2
);
540 if ((disjunction_p (rhs
) && d1
!= d2
)
541 || conjunction_p (rhs
)
542 || (atomic_p (rhs
) && d1
))
543 /* Either LHS or RHS is a conjunction. */
544 return std::make_pair (1 + n1
+ n2
, d1
| d2
);
546 /* Neither LHS nor RHS is a conjunction. */
547 return std::make_pair (2, false);
550 if (conjunction_p (lhs
))
552 if ((disjunction_p (rhs
) && d2
) || conjunction_p (rhs
))
553 /* Both LHS and RHS are conjunctions. */
554 return std::make_pair (n1
+ n2
, d1
| d2
);
556 /* Only LHS is a conjunction. */
557 return std::make_pair (1 + n1
+ n2
, d1
| d2
);
561 if ((disjunction_p (rhs
) && d2
) || conjunction_p (rhs
))
562 /* Only RHS is a disjunction. */
563 return std::make_pair (1 + n1
+ n2
, d1
| d2
);
565 /* Neither LHS nor RHS is a disjunction. */
566 return std::make_pair (2, false);
572 /* Count the number conjunctive clauses that would be created
573 when rewriting T to DNF. */
578 std::pair
<int, bool> result
= dnf_size_r (t
);
579 return result
.first
== 0 ? 1 : result
.first
;
583 /* Count the number disjunctive clauses that would be created
584 when rewriting T to CNF. */
589 std::pair
<int, bool> result
= cnf_size_r (t
);
590 return result
.first
== 0 ? 1 : result
.first
;
594 /* A left-conjunction is replaced by its operands. */
597 replace_term (clause
& c
, tree t
)
599 tree t1
= TREE_OPERAND (t
, 0);
600 tree t2
= TREE_OPERAND (t
, 1);
601 return c
.replace (t1
, t2
);
604 /* Create a new clause in the formula by copying the current
605 clause. In the current clause, the term at CI is replaced
606 by the first operand, and in the new clause, it is replaced
610 branch_clause (formula
& f
, clause
& c1
, tree t
)
612 tree t1
= TREE_OPERAND (t
, 0);
613 tree t2
= TREE_OPERAND (t
, 1);
614 clause
& c2
= f
.branch ();
619 /* Decompose t1 /\ t2 according to the rules R. */
622 decompose_conjuntion (formula
& f
, clause
& c
, tree t
, rules r
)
627 branch_clause (f
, c
, t
);
630 /* Decompose t1 \/ t2 according to the rules R. */
633 decompose_disjunction (formula
& f
, clause
& c
, tree t
, rules r
)
638 branch_clause (f
, c
, t
);
641 /* An atomic constraint is already decomposed. */
643 decompose_atom (clause
& c
)
648 /* Decompose a term of clause C (in formula F) according to the
652 decompose_term (formula
& f
, clause
& c
, tree t
, rules r
)
654 switch (TREE_CODE (t
))
657 return decompose_conjuntion (f
, c
, t
, r
);
659 return decompose_disjunction (f
, c
, t
, r
);
661 return decompose_atom (c
);
665 /* Decompose C (in F) using the logical rules R until it
666 is comprised of only atomic constraints. */
669 decompose_clause (formula
& f
, clause
& c
, rules r
)
672 decompose_term (f
, c
, *c
.current (), r
);
676 /* Decompose the logical formula F according to the logical
677 rules determined by R. The result is a formula containing
678 clauses that contain only atomic terms. */
681 decompose_formula (formula
& f
, rules r
)
684 decompose_clause (f
, *f
.current (), r
);
687 /* Fully decomposing T into a list of sequents, each comprised of
688 a list of atomic constraints, as if T were an antecedent. */
691 decompose_antecedents (tree t
)
694 decompose_formula (f
, left
);
698 /* Fully decomposing T into a list of sequents, each comprised of
699 a list of atomic constraints, as if T were a consequent. */
702 decompose_consequents (tree t
)
705 decompose_formula (f
, right
);
709 static bool derive_proof (clause
&, tree
, rules
);
711 /* Derive a proof of both operands of T. */
714 derive_proof_for_both_operands (clause
& c
, tree t
, rules r
)
716 if (!derive_proof (c
, TREE_OPERAND (t
, 0), r
))
718 return derive_proof (c
, TREE_OPERAND (t
, 1), r
);
721 /* Derive a proof of either operand of T. */
724 derive_proof_for_either_operand (clause
& c
, tree t
, rules r
)
726 if (derive_proof (c
, TREE_OPERAND (t
, 0), r
))
728 return derive_proof (c
, TREE_OPERAND (t
, 1), r
);
731 /* Derive a proof of the atomic constraint T in clause C. */
734 derive_atomic_proof (clause
& c
, tree t
)
736 return c
.contains (t
);
739 /* Derive a proof of T from the terms in C. */
742 derive_proof (clause
& c
, tree t
, rules r
)
744 switch (TREE_CODE (t
))
748 return derive_proof_for_both_operands (c
, t
, r
);
750 return derive_proof_for_either_operand (c
, t
, r
);
753 return derive_proof_for_either_operand (c
, t
, r
);
755 return derive_proof_for_both_operands (c
, t
, r
);
757 return derive_atomic_proof (c
, t
);
761 /* Derive a proof of T from disjunctive clauses in F. */
764 derive_proofs (formula
& f
, tree t
, rules r
)
766 for (formula::iterator i
= f
.begin(); i
!= f
.end(); ++i
)
767 if (!derive_proof (*i
, t
, r
))
772 /* The largest number of clauses in CNF or DNF we accept as input
773 for subsumption. This an upper bound of 2^16 expressions. */
774 static int max_problem_size
= 16;
777 diagnose_constraint_size (tree t
)
779 error_at (input_location
, "%qE exceeds the maximum constraint complexity", t
);
783 /* Key/value pair for caching subsumption results. This associates a pair of
784 constraints with a boolean value indicating the result. */
786 struct GTY((for_user
)) subsumption_entry
793 /* Hashing function and equality for constraint entries. */
795 struct subsumption_hasher
: ggc_ptr_hash
<subsumption_entry
>
797 static hashval_t
hash (subsumption_entry
*e
)
800 val
= iterative_hash_constraint (e
->lhs
, val
);
801 val
= iterative_hash_constraint (e
->rhs
, val
);
805 static bool equal (subsumption_entry
*e1
, subsumption_entry
*e2
)
807 if (!constraints_equivalent_p (e1
->lhs
, e2
->lhs
))
809 if (!constraints_equivalent_p (e1
->rhs
, e2
->rhs
))
815 /* Caches the results of subsumes_non_null(t1, t1). */
817 static GTY ((deletable
)) hash_table
<subsumption_hasher
> *subsumption_cache
;
819 /* Search for a previously cached subsumption result. */
822 lookup_subsumption (tree t1
, tree t2
)
824 if (!subsumption_cache
)
826 subsumption_entry elt
= { t1
, t2
, false };
827 subsumption_entry
* found
= subsumption_cache
->find (&elt
);
829 return &found
->result
;
834 /* Save a subsumption result. */
837 save_subsumption (tree t1
, tree t2
, bool result
)
839 if (!subsumption_cache
)
840 subsumption_cache
= hash_table
<subsumption_hasher
>::create_ggc(31);
841 subsumption_entry elt
= {t1
, t2
, result
};
842 subsumption_entry
** slot
= subsumption_cache
->find_slot (&elt
, INSERT
);
843 subsumption_entry
* entry
= ggc_alloc
<subsumption_entry
> ();
850 /* Returns true if the LEFT constraint subsume the RIGHT constraints.
851 This is done by deriving a proof of the conclusions on the RIGHT
852 from the assumptions on the LEFT assumptions. */
855 subsumes_constraints_nonnull (tree lhs
, tree rhs
)
857 auto_timevar
time (TV_CONSTRAINT_SUB
);
859 if (bool *b
= lookup_subsumption(lhs
, rhs
))
862 int n1
= dnf_size (lhs
);
863 int n2
= cnf_size (rhs
);
865 /* Make sure we haven't exceeded the largest acceptable problem. */
866 if (std::min (n1
, n2
) >= max_problem_size
)
869 diagnose_constraint_size (lhs
);
871 diagnose_constraint_size (rhs
);
875 /* Decompose the smaller of the two formulas, and recursively
876 check for implication of the larger. */
880 formula dnf
= decompose_antecedents (lhs
);
881 result
= derive_proofs (dnf
, rhs
, left
);
885 formula cnf
= decompose_consequents (rhs
);
886 result
= derive_proofs (cnf
, lhs
, right
);
889 return save_subsumption (lhs
, rhs
, result
);
892 /* Returns true if the LEFT constraints subsume the RIGHT
896 subsumes (tree lhs
, tree rhs
)
900 if (!lhs
|| lhs
== error_mark_node
)
902 if (!rhs
|| rhs
== error_mark_node
)
904 return subsumes_constraints_nonnull (lhs
, rhs
);
907 #include "gt-cp-logic.h"