Bug 100828 - Arbitrary limit on constraint complexity
Summary: Arbitrary limit on constraint complexity
Status: RESOLVED FIXED
Alias: None
Product: gcc
Classification: Unclassified
Component: c++ (show other bugs)
Version: 11.1.0
: P3 normal
Target Milestone: 11.3
Assignee: Patrick Palka
URL:
Keywords: rejects-valid
Depends on:
Blocks: concepts
  Show dependency treegraph
 
Reported: 2021-05-30 00:15 UTC by Matthew Barichello
Modified: 2021-08-11 15:59 UTC (History)
3 users (show)

See Also:
Host:
Target:
Build:
Known to work:
Known to fail:
Last reconfirmed: 2021-07-19 00:00:00


Attachments
Patch to remove the constraint complexity limit from gcc-11.1.0 (498 bytes, patch)
2021-05-30 00:15 UTC, Matthew Barichello
Details | Diff

Note You need to log in before you can comment on or make changes to this bug.
Description Matthew Barichello 2021-05-30 00:15:49 UTC
Created attachment 50889 [details]
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?
Comment 1 Patrick Palka 2021-07-19 18:56:45 UTC
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.
Comment 2 Richard Biener 2021-07-28 07:07:15 UTC
GCC 11.2 is being released, retargeting bugs to GCC 11.3
Comment 3 GCC Commits 2021-08-02 14:05:17 UTC
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.
Comment 4 GCC Commits 2021-08-11 15:55:54 UTC
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)
Comment 5 Patrick Palka 2021-08-11 15:59:14 UTC
Fixed for GCC 11.3 and 12, thanks for the bug report!