1 /* Derivation and subsumption rules for constraints.
2 Copyright (C) 2013-2024 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 /* A conjunctive or disjunctive clause.
52 Each clause maintains an iterator that refers to the current
53 term, which is used in the linear decomposition of a formula
58 typedef std::list
<tree
>::iterator iterator
;
59 typedef std::list
<tree
>::const_iterator const_iterator
;
61 /* Initialize a clause with an initial term. */
65 m_terms
.push_back (t
);
66 if (TREE_CODE (t
) == ATOMIC_CONSTR
)
69 m_current
= m_terms
.begin ();
72 /* Create a copy of the current term. The current
73 iterator is set to point to the same position in the
74 copied list of terms. */
76 clause (clause
const& c
)
77 : m_terms (c
.m_terms
), m_set (c
.m_set
), m_current (m_terms
.begin ())
79 std::advance (m_current
, std::distance (c
.begin (), c
.current ()));
82 /* Returns true when all terms are atoms. */
86 return m_current
== end ();
89 /* Advance to the next term. */
93 gcc_assert (!done ());
97 /* Replaces the current term at position ITER with T. If
98 T is an atomic constraint that already appears in the
99 clause, remove but do not replace ITER. Returns a pair
100 containing an iterator to the replace object or past
101 the erased object and a boolean value which is true if
102 an object was erased. */
104 std::pair
<iterator
, bool> replace (iterator iter
, tree t
)
106 gcc_assert (TREE_CODE (*iter
) != ATOMIC_CONSTR
);
107 if (TREE_CODE (t
) == ATOMIC_CONSTR
)
110 return std::make_pair (m_terms
.erase (iter
), true);
113 return std::make_pair (iter
, false);
116 /* Inserts T before ITER in the list of terms. If T is an atomic
117 constraint that already appears in the clause, no action is taken,
118 and the current iterator is returned. Returns a pair of an iterator
119 to the inserted object or ITER if no insertion occurred and a boolean
120 value which is true if an object was inserted. */
122 std::pair
<iterator
, bool> insert (iterator iter
, tree t
)
124 if (TREE_CODE (t
) == ATOMIC_CONSTR
)
127 return std::make_pair (iter
, false);
129 return std::make_pair (m_terms
.insert (iter
, t
), true);
132 /* Replaces the current term with T. In the case where the
133 current term is erased (because T is redundant), update
134 the position of the current term to the next term. */
136 void replace (tree t
)
138 m_current
= replace (m_current
, t
).first
;
141 /* Replace the current term with T1 and T2, in that order. */
143 void replace (tree t1
, tree t2
)
145 /* Replace the current term with t1. Ensure that iter points
146 to the term before which t2 will be inserted. Update the
147 current term as needed. */
148 std::pair
<iterator
, bool> rep
= replace (m_current
, t1
);
150 m_current
= rep
.first
;
154 /* Insert the t2. Make this the current term if we erased
156 std::pair
<iterator
, bool> ins
= insert (rep
.first
, t2
);
157 if (rep
.second
&& ins
.second
)
158 m_current
= ins
.first
;
161 /* Returns true if the clause contains the term T. */
163 bool contains (tree t
)
165 gcc_assert (TREE_CODE (t
) == ATOMIC_CONSTR
);
166 return m_set
.contains (t
);
170 /* Returns an iterator to the first clause in the formula. */
174 return m_terms
.begin ();
177 /* Returns an iterator to the first clause in the formula. */
179 const_iterator
begin () const
181 return m_terms
.begin ();
184 /* Returns an iterator past the last clause in the formula. */
188 return m_terms
.end ();
191 /* Returns an iterator past the last clause in the formula. */
193 const_iterator
end () const
195 return m_terms
.end ();
198 /* Returns the current iterator. */
200 const_iterator
current () const
205 std::list
<tree
> m_terms
; /* The list of terms. */
206 hash_set
<tree
, false, atom_hasher
> m_set
; /* The set of atomic constraints. */
207 iterator m_current
; /* The current term. */
211 /* A proof state owns a list of goals and tracks the
212 current sub-goal. The class also provides facilities
213 for managing subgoals and constructing term lists. */
217 typedef std::list
<clause
>::iterator iterator
;
218 typedef std::list
<clause
>::const_iterator const_iterator
;
220 /* Construct a formula with an initial formula in a
225 m_clauses
.emplace_back (t
);
226 m_current
= m_clauses
.begin ();
229 /* Returns true when all clauses are atomic. */
232 return m_current
== end ();
235 /* Advance to the next term. */
238 gcc_assert (!done ());
242 /* Insert a copy of clause into the formula. This corresponds
243 to a distribution of one logical operation over the other. */
247 gcc_assert (!done ());
248 return *m_clauses
.insert (std::next (m_current
), *m_current
);
251 /* Returns the position of the current clause. */
258 /* Returns an iterator to the first clause in the formula. */
262 return m_clauses
.begin ();
265 /* Returns an iterator to the first clause in the formula. */
267 const_iterator
begin () const
269 return m_clauses
.begin ();
272 /* Returns an iterator past the last clause in the formula. */
276 return m_clauses
.end ();
279 /* Returns an iterator past the last clause in the formula. */
281 const_iterator
end () const
283 return m_clauses
.end ();
286 /* Remove the specified clause from the formula. */
288 void erase (iterator i
)
290 gcc_assert (i
!= m_current
);
294 std::list
<clause
> m_clauses
; /* The list of clauses. */
295 iterator m_current
; /* The current clause. */
301 for (clause::iterator i
= c
.begin (); i
!= c
.end (); ++i
)
302 verbatim (" # %E", *i
);
308 for (formula::iterator i
= f
.begin (); i
!= f
.end (); ++i
)
310 /* Format punctuators via %s to avoid -Wformat-diag. */
311 verbatim ("%s", "(((");
313 verbatim ("%s", ")))");
317 /* The logical rules used to analyze a logical formula. The
318 "left" and "right" refer to the position of formula in a
319 sequent (as in sequent calculus). */
326 /* Distribution counting. */
329 disjunction_p (tree t
)
331 return TREE_CODE (t
) == DISJ_CONSTR
;
335 conjunction_p (tree t
)
337 return TREE_CODE (t
) == CONJ_CONSTR
;
343 return TREE_CODE (t
) == ATOMIC_CONSTR
;
346 /* Recursively count the number of clauses produced when converting T
347 to DNF. Returns a pair containing the number of clauses and a bool
348 value signifying that the tree would be rewritten as a result of
349 distributing. In general, a conjunction for which this flag is set
350 is considered a disjunction for the purpose of counting. */
352 static std::pair
<int, bool>
356 /* Atomic constraints produce no clauses. */
357 return std::make_pair (0, false);
359 /* For compound constraints, recursively count clauses and unpack
361 tree lhs
= TREE_OPERAND (t
, 0);
362 tree rhs
= TREE_OPERAND (t
, 1);
363 std::pair
<int, bool> p1
= dnf_size_r (lhs
);
364 std::pair
<int, bool> p2
= dnf_size_r (rhs
);
365 int n1
= p1
.first
, n2
= p2
.first
;
366 bool d1
= p1
.second
, d2
= p2
.second
;
368 if (disjunction_p (t
))
370 /* Matches constraints of the form P \/ Q. Disjunctions contribute
371 linearly to the number of constraints. When both P and Q are
372 disjunctions, clauses are added. When only one of P and Q
373 is a disjunction, an additional clause is produced. When neither
374 P nor Q are disjunctions, two clauses are produced. */
375 if (disjunction_p (lhs
))
377 if (disjunction_p (rhs
) || (conjunction_p (rhs
) && d2
))
378 /* Both P and Q are disjunctions. */
379 return std::make_pair (n1
+ n2
, d1
| d2
);
381 /* Only LHS is a disjunction. */
382 return std::make_pair (1 + n1
+ n2
, d1
| d2
);
385 if (conjunction_p (lhs
))
387 if ((disjunction_p (rhs
) && d1
) || (conjunction_p (rhs
) && d1
&& d2
))
388 /* Both P and Q are disjunctions. */
389 return std::make_pair (n1
+ n2
, d1
| d2
);
390 if (disjunction_p (rhs
)
391 || (conjunction_p (rhs
) && d1
!= d2
)
392 || (atomic_p (rhs
) && d1
))
393 /* Either LHS or RHS is a disjunction. */
394 return std::make_pair (1 + n1
+ n2
, d1
| d2
);
396 /* Neither LHS nor RHS is a disjunction. */
397 return std::make_pair (2, false);
401 if (disjunction_p (rhs
) || (conjunction_p (rhs
) && d2
))
402 /* Only RHS is a disjunction. */
403 return std::make_pair (1 + n1
+ n2
, d1
| d2
);
405 /* Neither LHS nor RHS is a disjunction. */
406 return std::make_pair (2, false);
409 else /* conjunction_p (t) */
411 /* Matches constraints of the form P /\ Q, possibly resulting
412 in the distribution of one side over the other. When both
413 P and Q are disjunctions, the number of clauses are multiplied.
414 When only one of P and Q is a disjunction, the number of
415 clauses are added. Otherwise, neither side is a disjunction and
416 no clauses are created. */
417 if (disjunction_p (lhs
))
419 if (disjunction_p (rhs
) || (conjunction_p (rhs
) && d2
))
420 /* Both P and Q are disjunctions. */
421 return std::make_pair (n1
* n2
, true);
423 /* Only LHS is a disjunction. */
424 return std::make_pair (n1
+ n2
, true);
427 if (conjunction_p (lhs
))
429 if ((disjunction_p (rhs
) && d1
) || (conjunction_p (rhs
) && d1
&& d2
))
430 /* Both P and Q are disjunctions. */
431 return std::make_pair (n1
* n2
, true);
432 if (disjunction_p (rhs
)
433 || (conjunction_p (rhs
) && d1
!= d2
)
434 || (atomic_p (rhs
) && d1
))
435 /* Either LHS or RHS is a disjunction. */
436 return std::make_pair (n1
+ n2
, true);
438 /* Neither LHS nor RHS is a disjunction. */
439 return std::make_pair (0, false);
443 if (disjunction_p (rhs
) || (conjunction_p (rhs
) && d2
))
444 /* Only RHS is a disjunction. */
445 return std::make_pair (n1
+ n2
, true);
447 /* Neither LHS nor RHS is a disjunction. */
448 return std::make_pair (0, false);
454 /* Recursively count the number of clauses produced when converting T
455 to CNF. Returns a pair containing the number of clauses and a bool
456 value signifying that the tree would be rewritten as a result of
457 distributing. In general, a disjunction for which this flag is set
458 is considered a conjunction for the purpose of counting. */
460 static std::pair
<int, bool>
464 /* Atomic constraints produce no clauses. */
465 return std::make_pair (0, false);
467 /* For compound constraints, recursively count clauses and unpack
469 tree lhs
= TREE_OPERAND (t
, 0);
470 tree rhs
= TREE_OPERAND (t
, 1);
471 std::pair
<int, bool> p1
= cnf_size_r (lhs
);
472 std::pair
<int, bool> p2
= cnf_size_r (rhs
);
473 int n1
= p1
.first
, n2
= p2
.first
;
474 bool d1
= p1
.second
, d2
= p2
.second
;
476 if (disjunction_p (t
))
478 /* Matches constraints of the form P \/ Q, possibly resulting
479 in the distribution of one side over the other. When both
480 P and Q are conjunctions, the number of clauses are multiplied.
481 When only one of P and Q is a conjunction, the number of
482 clauses are added. Otherwise, neither side is a conjunction and
483 no clauses are created. */
484 if (disjunction_p (lhs
))
486 if ((disjunction_p (rhs
) && d1
&& d2
) || (conjunction_p (rhs
) && d1
))
487 /* Both P and Q are conjunctions. */
488 return std::make_pair (n1
* n2
, true);
489 if ((disjunction_p (rhs
) && d1
!= d2
)
490 || conjunction_p (rhs
)
491 || (atomic_p (rhs
) && d1
))
492 /* Either LHS or RHS is a conjunction. */
493 return std::make_pair (n1
+ n2
, true);
495 /* Neither LHS nor RHS is a conjunction. */
496 return std::make_pair (0, false);
498 if (conjunction_p (lhs
))
500 if ((disjunction_p (rhs
) && d2
) || conjunction_p (rhs
))
501 /* Both LHS and RHS are conjunctions. */
502 return std::make_pair (n1
* n2
, true);
504 /* Only LHS is a conjunction. */
505 return std::make_pair (n1
+ n2
, true);
509 if ((disjunction_p (rhs
) && d2
) || conjunction_p (rhs
))
510 /* Only RHS is a disjunction. */
511 return std::make_pair (n1
+ n2
, true);
513 /* Neither LHS nor RHS is a disjunction. */
514 return std::make_pair (0, false);
517 else /* conjunction_p (t) */
519 /* Matches constraints of the form P /\ Q. Conjunctions contribute
520 linearly to the number of constraints. When both P and Q are
521 conjunctions, clauses are added. When only one of P and Q
522 is a conjunction, an additional clause is produced. When neither
523 P nor Q are conjunctions, two clauses are produced. */
524 if (disjunction_p (lhs
))
526 if ((disjunction_p (rhs
) && d1
&& d2
) || (conjunction_p (rhs
) && d1
))
527 /* Both P and Q are conjunctions. */
528 return std::make_pair (n1
+ n2
, d1
| d2
);
529 if ((disjunction_p (rhs
) && d1
!= d2
)
530 || conjunction_p (rhs
)
531 || (atomic_p (rhs
) && d1
))
532 /* Either LHS or RHS is a conjunction. */
533 return std::make_pair (1 + n1
+ n2
, d1
| d2
);
535 /* Neither LHS nor RHS is a conjunction. */
536 return std::make_pair (2, false);
538 if (conjunction_p (lhs
))
540 if ((disjunction_p (rhs
) && d2
) || conjunction_p (rhs
))
541 /* Both LHS and RHS are conjunctions. */
542 return std::make_pair (n1
+ n2
, d1
| d2
);
544 /* Only LHS is a conjunction. */
545 return std::make_pair (1 + n1
+ n2
, d1
| d2
);
549 if ((disjunction_p (rhs
) && d2
) || conjunction_p (rhs
))
550 /* Only RHS is a disjunction. */
551 return std::make_pair (1 + n1
+ n2
, d1
| d2
);
553 /* Neither LHS nor RHS is a disjunction. */
554 return std::make_pair (2, false);
560 /* Count the number conjunctive clauses that would be created
561 when rewriting T to DNF. */
566 std::pair
<int, bool> result
= dnf_size_r (t
);
567 return result
.first
== 0 ? 1 : result
.first
;
571 /* Count the number disjunctive clauses that would be created
572 when rewriting T to CNF. */
577 std::pair
<int, bool> result
= cnf_size_r (t
);
578 return result
.first
== 0 ? 1 : result
.first
;
582 /* A left-conjunction is replaced by its operands. */
585 replace_term (clause
& c
, tree t
)
587 tree t1
= TREE_OPERAND (t
, 0);
588 tree t2
= TREE_OPERAND (t
, 1);
589 return c
.replace (t1
, t2
);
592 /* Create a new clause in the formula by copying the current
593 clause. In the current clause, the term at CI is replaced
594 by the first operand, and in the new clause, it is replaced
598 branch_clause (formula
& f
, clause
& c1
, tree t
)
600 tree t1
= TREE_OPERAND (t
, 0);
601 tree t2
= TREE_OPERAND (t
, 1);
602 clause
& c2
= f
.branch ();
607 /* Decompose t1 /\ t2 according to the rules R. */
610 decompose_conjuntion (formula
& f
, clause
& c
, tree t
, rules r
)
615 branch_clause (f
, c
, t
);
618 /* Decompose t1 \/ t2 according to the rules R. */
621 decompose_disjunction (formula
& f
, clause
& c
, tree t
, rules r
)
626 branch_clause (f
, c
, t
);
629 /* An atomic constraint is already decomposed. */
631 decompose_atom (clause
& c
)
636 /* Decompose a term of clause C (in formula F) according to the
640 decompose_term (formula
& f
, clause
& c
, tree t
, rules r
)
642 switch (TREE_CODE (t
))
645 return decompose_conjuntion (f
, c
, t
, r
);
647 return decompose_disjunction (f
, c
, t
, r
);
649 return decompose_atom (c
);
653 /* Decompose C (in F) using the logical rules R until it
654 is comprised of only atomic constraints. */
657 decompose_clause (formula
& f
, clause
& c
, rules r
)
660 decompose_term (f
, c
, *c
.current (), r
);
664 static bool derive_proof (clause
&, tree
, rules
);
666 /* Derive a proof of both operands of T. */
669 derive_proof_for_both_operands (clause
& c
, tree t
, rules r
)
671 if (!derive_proof (c
, TREE_OPERAND (t
, 0), r
))
673 return derive_proof (c
, TREE_OPERAND (t
, 1), r
);
676 /* Derive a proof of either operand of T. */
679 derive_proof_for_either_operand (clause
& c
, tree t
, rules r
)
681 if (derive_proof (c
, TREE_OPERAND (t
, 0), r
))
683 return derive_proof (c
, TREE_OPERAND (t
, 1), r
);
686 /* Derive a proof of the atomic constraint T in clause C. */
689 derive_atomic_proof (clause
& c
, tree t
)
691 return c
.contains (t
);
694 /* Derive a proof of T from the terms in C. */
697 derive_proof (clause
& c
, tree t
, rules r
)
699 switch (TREE_CODE (t
))
703 return derive_proof_for_both_operands (c
, t
, r
);
705 return derive_proof_for_either_operand (c
, t
, r
);
708 return derive_proof_for_either_operand (c
, t
, r
);
710 return derive_proof_for_both_operands (c
, t
, r
);
712 return derive_atomic_proof (c
, t
);
716 /* Key/value pair for caching subsumption results. This associates a pair of
717 constraints with a boolean value indicating the result. */
719 struct GTY((for_user
)) subsumption_entry
726 /* Hashing function and equality for constraint entries. */
728 struct subsumption_hasher
: ggc_ptr_hash
<subsumption_entry
>
730 static hashval_t
hash (subsumption_entry
*e
)
733 val
= iterative_hash_constraint (e
->lhs
, val
);
734 val
= iterative_hash_constraint (e
->rhs
, val
);
738 static bool equal (subsumption_entry
*e1
, subsumption_entry
*e2
)
740 if (!constraints_equivalent_p (e1
->lhs
, e2
->lhs
))
742 if (!constraints_equivalent_p (e1
->rhs
, e2
->rhs
))
748 /* Caches the results of subsumes_constraints_nonnull (t1, t1). */
750 static GTY ((deletable
)) hash_table
<subsumption_hasher
> *subsumption_cache
;
752 /* Search for a previously cached subsumption result. */
755 lookup_subsumption (tree t1
, tree t2
)
757 if (!subsumption_cache
)
759 subsumption_entry elt
= { t1
, t2
, false };
760 subsumption_entry
* found
= subsumption_cache
->find (&elt
);
762 return &found
->result
;
767 /* Save a subsumption result. */
770 save_subsumption (tree t1
, tree t2
, bool result
)
772 if (!subsumption_cache
)
773 subsumption_cache
= hash_table
<subsumption_hasher
>::create_ggc (31);
774 subsumption_entry elt
= {t1
, t2
, result
};
775 subsumption_entry
** slot
= subsumption_cache
->find_slot (&elt
, INSERT
);
776 subsumption_entry
* entry
= ggc_alloc
<subsumption_entry
> ();
783 /* Returns true if the LEFT constraint subsume the RIGHT constraints.
784 This is done by deriving a proof of the conclusions on the RIGHT
785 from the assumptions on the LEFT assumptions. */
788 subsumes_constraints_nonnull (tree lhs
, tree rhs
)
790 auto_timevar
time (TV_CONSTRAINT_SUB
);
792 if (bool *b
= lookup_subsumption (lhs
, rhs
))
797 if (dnf_size (lhs
) <= cnf_size (rhs
))
798 /* When LHS looks simpler than RHS, we'll determine subsumption by
799 decomposing LHS into its disjunctive normal form and checking that
800 each (conjunctive) clause in the decomposed LHS implies RHS. */
801 x
= lhs
, y
= rhs
, r
= left
;
803 /* Otherwise, we'll determine subsumption by decomposing RHS into its
804 conjunctive normal form and checking that each (disjunctive) clause
805 in the decomposed RHS implies LHS. */
806 x
= rhs
, y
= lhs
, r
= right
;
808 /* Decompose X into a list of sequents according to R, and recursively
809 check for implication of Y. */
814 auto i
= f
.current ();
815 decompose_clause (f
, *i
, r
);
816 if (!derive_proof (*i
, y
, r
))
824 return save_subsumption (lhs
, rhs
, result
);
827 /* Returns true if the LEFT constraints subsume the RIGHT
831 subsumes (tree lhs
, tree rhs
)
835 if (!lhs
|| lhs
== error_mark_node
)
837 if (!rhs
|| rhs
== error_mark_node
)
839 return subsumes_constraints_nonnull (lhs
, rhs
);
842 #include "gt-cp-logic.h"