On Wed, 11 Aug 2021, Jason Merrill wrote:
> On 8/9/21 5:07 PM, Patrick Palka wrote:
> > On Wed, Jul 28, 2021 at 4:42 PM Jason Merrill <ja...@redhat.com> wrote:
> > >
> > > On 7/19/21 6:05 PM, Patrick Palka wrote:
> > > > Constraint subsumption is implemented in two steps. The first step
> > > > computes the disjunctive (or conjunctive) normal form of one of the
> > > > constraints, and the second step verifies that each clause in the
> > > > decomposed form implies the other constraint. Performing these two
> > > > steps separately is problematic because in the first step the
> > > > disjunctive normal form can be exponentially larger than the original
> > > > constraint, and by computing it ahead of time we'd have to keep all of
> > > > it in memory.
> > > >
> > > > This patch fixes this exponential blowup in memory usage by interleaving
> > > > these two steps, so that as soon as we decompose one clause we check
> > > > implication for it. In turn, memory usage during subsumption is now
> > > > worst case linear in the size of the constraints rather than
> > > > exponential, and so we can safely remove the hard limit of 16 clauses
> > > > without introducing runaway memory usage on some inputs. (Note the
> > > > _time_ complexity of subsumption is still exponential in the worst
> > > > case.)
> > > >
> > > > In order for this to work we need formula::branch to prepend the copy
> > > > of the current clause directly after the current clause rather than
> > > > at the end of the list, so that we fully decompose a clause shortly
> > > > after creating it. Otherwise we'd end up accumulating exponentially
> > > > many (partially decomposed) clauses in memory anyway.
> > > >
> > > > Bootstrapped and regtested on x86_64-pc-linux-gnu, and also tested on
> > > > range-v3 and cmcstl2. Does this look OK for trunk and perhaps 11?
> > >
> > > OK for trunk.
> >
> > Thanks a lot, patch committed to trunk as r12-2658. Since this low
> > complexity limit was introduced in GCC 10, what do you think about
> > increasing the limit from 16 to say 128 in the 10/11 release branches
> > as a relatively safe stopgap?
>
> Now that 11.2 is out, go ahead and apply this patch to the 11 branch.
Ah great, will do.
>
> Won't a limit of 128 in GCC 10 lead to extremely long compile times for
> affected code? Is that more desirable than an error?
Potentially, though I think that'd be the case only if the original
(normalized) constraint is huge to begin with. The comment for
max_problem_size says
/* The largest number of clauses in CNF or DNF we accept as input
for subsumption. This an upper bound of 2^16 expressions. */
static int max_problem_size = 16;
which implies increasing it to 128 would allow for at most 2^128
expressions (clearly unacceptable), but I'm not sure how this upper
bound was obtained.
FWIW I think another upper bound for the number of expressions in the
CNF/DNF is roughly 'max_problem_size * size_of_original_constraint',
since we allow at most 'max_problem_size' clauses in the decomposed form
and each clause is definitely no larger than the original constraint.
So according to this upper bound the dependence on max_problem_size as
it relates to worst-case compile time/memory usage of subsumption is
linear rather than exponential, contrary to the comment. In that case
increasing the limit from 16 to 128 doesn't seem to be too bad.
>
> > > > PR c++/100828
> > > >
> > > > gcc/cp/ChangeLog:
> > > >
> > > > * logic.cc (formula::formula): Use emplace_back.
> > > > (formula::branch): Insert a copy of m_current in front of
> > > > m_current instead of at the end of the list.
> > > > (formula::erase): Define.
> > > > (decompose_formula): Remove.
> > > > (decompose_antecedents): Remove.
> > > > (decompose_consequents): Remove.
> > > > (derive_proofs): Remove.
> > > > (max_problem_size): Remove.
> > > > (diagnose_constraint_size): Remove.
> > > > (subsumes_constraints_nonnull): Rewrite directly in terms of
> > > > decompose_clause and derive_proof, interleaving decomposition
> > > > with implication checking. Use formula::erase to free the
> > > > current clause before moving on to the next one.
> > > > ---
> > > > gcc/cp/logic.cc | 118
> > > > ++++++++++++++----------------------------------
> > > > 1 file changed, 35 insertions(+), 83 deletions(-)
> > > >
> > > > diff --git a/gcc/cp/logic.cc b/gcc/cp/logic.cc
> > > > index 142457e408a..3f872c11fe2 100644
> > > > --- a/gcc/cp/logic.cc
> > > > +++ b/gcc/cp/logic.cc
> > > > @@ -223,9 +223,7 @@ struct formula
> > > >
> > > > formula (tree t)
> > > > {
> > > > - /* This should call emplace_back(). There's an extra copy being
> > > > - invoked by using push_back(). */
> > > > - m_clauses.push_back (t);
> > > > + m_clauses.emplace_back (t);
> > > > m_current = m_clauses.begin ();
> > > > }
> > > >
> > > > @@ -248,8 +246,7 @@ struct formula
> > > > clause& branch ()
> > > > {
> > > > gcc_assert (!done ());
> > > > - m_clauses.push_back (*m_current);
> > > > - return m_clauses.back ();
> > > > + return *m_clauses.insert (std::next (m_current), *m_current);
> > > > }
> > > >
> > > > /* Returns the position of the current clause. */
> > > > @@ -287,6 +284,14 @@ struct formula
> > > > return m_clauses.end ();
> > > > }
> > > >
> > > > + /* Remove the specified clause. */
> > > > +
> > > > + void erase (iterator i)
> > > > + {
> > > > + gcc_assert (i != m_current);
> > > > + m_clauses.erase (i);
> > > > + }
> > > > +
> > > > std::list<clause> m_clauses; /* The list of clauses. */
> > > > iterator m_current; /* The current clause. */
> > > > };
> > > > @@ -659,39 +664,6 @@ decompose_clause (formula& f, clause& c, rules r)
> > > > f.advance ();
> > > > }
> > > >
> > > > -/* Decompose the logical formula F according to the logical
> > > > - rules determined by R. The result is a formula containing
> > > > - clauses that contain only atomic terms. */
> > > > -
> > > > -void
> > > > -decompose_formula (formula& f, rules r)
> > > > -{
> > > > - while (!f.done ())
> > > > - decompose_clause (f, *f.current (), r);
> > > > -}
> > > > -
> > > > -/* Fully decomposing T into a list of sequents, each comprised of
> > > > - a list of atomic constraints, as if T were an antecedent. */
> > > > -
> > > > -static formula
> > > > -decompose_antecedents (tree t)
> > > > -{
> > > > - formula f (t);
> > > > - decompose_formula (f, left);
> > > > - return f;
> > > > -}
> > > > -
> > > > -/* Fully decomposing T into a list of sequents, each comprised of
> > > > - a list of atomic constraints, as if T were a consequent. */
> > > > -
> > > > -static formula
> > > > -decompose_consequents (tree t)
> > > > -{
> > > > - formula f (t);
> > > > - decompose_formula (f, right);
> > > > - return f;
> > > > -}
> > > > -
> > > > static bool derive_proof (clause&, tree, rules);
> > > >
> > > > /* Derive a proof of both operands of T. */
> > > > @@ -744,28 +716,6 @@ derive_proof (clause& c, tree t, rules r)
> > > > }
> > > > }
> > > >
> > > > -/* Derive a proof of T from disjunctive clauses in F. */
> > > > -
> > > > -static bool
> > > > -derive_proofs (formula& f, tree t, rules r)
> > > > -{
> > > > - for (formula::iterator i = f.begin(); i != f.end(); ++i)
> > > > - if (!derive_proof (*i, t, r))
> > > > - return false;
> > > > - return true;
> > > > -}
> > > > -
> > > > -/* The largest number of clauses in CNF or DNF we accept as input
> > > > - for subsumption. This an upper bound of 2^16 expressions. */
> > > > -static int max_problem_size = 16;
> > > > -
> > > > -static inline bool
> > > > -diagnose_constraint_size (tree t)
> > > > -{
> > > > - error_at (input_location, "%qE exceeds the maximum constraint
> > > > complexity", t);
> > > > - return false;
> > > > -}
> > > > -
> > > > /* Key/value pair for caching subsumption results. This associates a
> > > > pair of
> > > > constraints with a boolean value indicating the result. */
> > > >
> > > > @@ -845,31 +795,33 @@ subsumes_constraints_nonnull (tree lhs, tree rhs)
> > > > if (bool *b = lookup_subsumption(lhs, rhs))
> > > > return *b;
> > > >
> > > > - int n1 = dnf_size (lhs);
> > > > - int n2 = cnf_size (rhs);
> > > > -
> > > > - /* Make sure we haven't exceeded the largest acceptable problem. */
> > > > - if (std::min (n1, n2) >= max_problem_size)
> > > > - {
> > > > - if (n1 < n2)
> > > > - diagnose_constraint_size (lhs);
> > > > - else
> > > > - diagnose_constraint_size (rhs);
> > > > - return false;
> > > > - }
> > > > -
> > > > - /* Decompose the smaller of the two formulas, and recursively
> > > > - check for implication of the larger. */
> > > > - bool result;
> > > > - if (n1 <= n2)
> > > > - {
> > > > - formula dnf = decompose_antecedents (lhs);
> > > > - result = derive_proofs (dnf, rhs, left);
> > > > - }
> > > > + tree x, y;
> > > > + rules r;
> > > > + if (dnf_size (lhs) <= cnf_size (rhs))
> > > > + /* When LHS looks simpler than RHS, we'll determine subsumption by
> > > > + decomposing LHS into its disjunctive normal form and checking
> > > > that
> > > > + each (conjunctive) clause implies RHS. */
> > > > + x = lhs, y = rhs, r = left;
> > > > else
> > > > + /* Otherwise, we'll determine subsumption by decomposing RHS into
> > > > its
> > > > + conjunctive normal form and checking that each (disjunctive)
> > > > clause
> > > > + implies LHS. */
> > > > + x = rhs, y = lhs, r = right;
> > > > +
> > > > + /* Decompose X into a list of sequents according to R, and
> > > > recursively
> > > > + check for implication of Y. */
> > > > + bool result = true;
> > > > + formula f (x);
> > > > + while (!f.done ())
> > > > {
> > > > - formula cnf = decompose_consequents (rhs);
> > > > - result = derive_proofs (cnf, lhs, right);
> > > > + auto i = f.current ();
> > > > + decompose_clause (f, *i, r);
> > > > + if (!derive_proof (*i, y, r))
> > > > + {
> > > > + result = false;
> > > > + break;
> > > > + }
> > > > + f.erase (i);
> > > > }
> > > >
> > > > return save_subsumption (lhs, rhs, result);
> > > >
> > >
> >
>
>
