[Bug c++/100828] New: Arbitrary limit on constraint complexity

[Bug c++/100828] New: Arbitrary limit on constraint complexity

[matthewjbarichello at gmail dot com]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=100828

            Bug ID: 100828
           Summary: Arbitrary limit on constraint complexity
           Product: gcc
           Version: 11.1.0
            Status: UNCONFIRMED
          Severity: normal
          Priority: P3
         Component: c++
          Assignee: unassigned at gcc dot gnu.org
          Reporter: matthewjbarichello at gmail dot com
  Target Milestone: ---

Created attachment 50889
  --> https://gcc.gnu.org/bugzilla/attachment.cgi?id=50889&action=edit
Patch to remove the constraint complexity limit from gcc-11.1.0

It would seem that there is an arbitrary limit on the complexity of constraints
in gcc 11.

    #define a (0 || 0 && 0)

    namespace e {
     template<typename>
     struct f;
    }
    template<typename g>
    concept f = e::f<g>::h && true && a;

    template<typename>
    concept i = a && a;

    template <typename, typename j>
    requires(i<j> || f<j>)
    struct k;

    template<typename g, typename j>
    requires(i<j> && i<g>)
    struct k<g, j>;

This example, reduced with c-reduce, yields:

    <source>:19:8: error: ‘0 \/ 0 /\ 0 /\ 0 \/ 0 /\ 0 \/ e::f<
<template-parameter-1-1> >::h [with g = j] /\ true /\ 0 \/ 0 /\ 0’ exceeds the
maximum constraint complexity
       19 | struct k<g, j>;
          |        ^~~~~~~

Attached is a patch for gcc, as of the releases/gcc-11.1.0 tag, which allows
gcc to compile the example without an issue.

Clang does not seem to have this limitation and has no problem compiling the
example. Is there a reason for this limit?

[Bug c++/100828] Arbitrary limit on constraint complexity

[ppalka at gcc dot gnu.org]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=100828

Patrick Palka <ppalka at gcc dot gnu.org> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|UNCONFIRMED                 |ASSIGNED
                 CC|                            |ppalka at gcc dot gnu.org
     Ever confirmed|0                           |1
   Last reconfirmed|                            |2021-07-19
           Assignee|unassigned at gcc dot gnu.org      |ppalka at gcc dot gnu.org
   Target Milestone|---                         |11.2

--- Comment #1 from Patrick Palka <ppalka at gcc dot gnu.org> ---
Confirmed.  This complexity limit is probably there because the subsumption
algorithm (namely the conversion to DNF/CNF) can use an exponential amount of
space, but I think we can improve this and avoid the exponential memory usage
in the first place.  Then we could safely remove the complexity limit.

[Bug c++/100828] Arbitrary limit on constraint complexity

[rguenth at gcc dot gnu.org]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=100828

Richard Biener <rguenth at gcc dot gnu.org> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
   Target Milestone|11.2                        |11.3

--- Comment #2 from Richard Biener <rguenth at gcc dot gnu.org> ---
GCC 11.2 is being released, retargeting bugs to GCC 11.3

[Bug c++/100828] Arbitrary limit on constraint complexity

[cvs-commit at gcc dot gnu.org]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=100828

--- Comment #3 from CVS Commits <cvs-commit at gcc dot gnu.org> ---
The master branch has been updated by Patrick Palka <ppalka@gcc.gnu.org>:

https://gcc.gnu.org/g:f48c3cd2e3f9cd9e3c329eb2d3185bd26e7c7607

commit r12-2658-gf48c3cd2e3f9cd9e3c329eb2d3185bd26e7c7607
Author: Patrick Palka <ppalka@redhat.com>
Date:   Mon Aug 2 09:59:56 2021 -0400

    c++: Improve memory usage of subsumption [PR100828]

    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 DNF/CNF
    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
    the 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 to make formula::branch() insert 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.

            PR c++/100828

    gcc/cp/ChangeLog:

            * logic.cc (formula::formula): Use emplace_back instead of
            push_back.
            (formula::branch): Insert a copy of m_current directly after
            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.  Remove limit on constraint complexity.
            Use formula::erase to free the current clause before moving on to
            the next one.

[Bug c++/100828] Arbitrary limit on constraint complexity

[cvs-commit at gcc dot gnu.org]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=100828

--- Comment #4 from CVS Commits <cvs-commit at gcc dot gnu.org> ---
The releases/gcc-11 branch has been updated by Patrick Palka
<ppalka@gcc.gnu.org>:

https://gcc.gnu.org/g:90f3dd128bc709a76c52b5ae29b40903acb26f20

commit r11-8851-g90f3dd128bc709a76c52b5ae29b40903acb26f20
Author: Patrick Palka <ppalka@redhat.com>
Date:   Mon Aug 2 09:59:56 2021 -0400

    c++: Improve memory usage of subsumption [PR100828]

    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 DNF/CNF
    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
    the 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 to make formula::branch() insert 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.

            PR c++/100828

    gcc/cp/ChangeLog:

            * logic.cc (formula::formula): Use emplace_back instead of
            push_back.
            (formula::branch): Insert a copy of m_current directly after
            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.  Remove limit on constraint complexity.
            Use formula::erase to free the current clause before moving on to
            the next one.

    (cherry picked from commit f48c3cd2e3f9cd9e3c329eb2d3185bd26e7c7607)

[Bug c++/100828] Arbitrary limit on constraint complexity

[ppalka at gcc dot gnu.org]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=100828

Patrick Palka <ppalka at gcc dot gnu.org> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|ASSIGNED                    |RESOLVED
         Resolution|---                         |FIXED

--- Comment #5 from Patrick Palka <ppalka at gcc dot gnu.org> ---
Fixed for GCC 11.3 and 12, thanks for the bug report!