Re: [PATCH 1/2] c++: subsumption of complex constraints [PR118069]

[Jason Merrill]

On 12/17/24 10:43 AM, Patrick Palka wrote:
Bootstrapped and regtested on x86_64-pc-linux-gnu, does this look
OK for trunk?  Shall we also backport this to release branches?
It's not a regression but seems like a safe fix for an inconvenient
issue.

OK for trunk and 14.

I wonder about using __builtin_mul_overflow et al (wrapped in a 
"non-overflow integer" class template?) to fail better on an even more 
extreme testcase.

-- >8 --

For the testcase in the PR we hang during constraint normalization
ultimately because one of the constraints is complex enough that its
conjunctive normal form is calculated to have more than 2^31 clauses,
which causes the size calculation (through an int) to overflow and so
the optimization in subsumes_constraints_nonnull

   if (dnf_size (lhs) <= cnf_size (rhs))
     // iterate over DNF of LHS
   else
     // iterate over CNF of RHS

incorrectly decides to loop over the CNF (billions of clauses) instead
of the DNF (thousands of clauses).

I haven't verified that the result of cnf_size is correct for the
problematic constraint but integer overflow is definitely plausible
given that CNF/DNF can be exponentially larger than the original
constraint in the worst case.

This patch fixes this by using a 64-bit unsigned int during DNF/CNF size
calculation which is enough to avoid overflow in the testcase, and we now
compile it in ~3 seconds.

In theory doubling the precision will only let us handle a ~2x bigger
constraint before risking overflow in the worst case given the
exponential-ness, but I suppose it should suffice for now.

        PR c++/118069

gcc/cp/ChangeLog:

        * logic.cc (dnf_size_r): Use unsigned HOST_WIDE_INT instead of int.
        (cnf_size_r): Likewise.
        (dnf_size): Likewise.
        (cnf_size): Likewise.
---
  gcc/cp/logic.cc | 24 ++++++++++++------------
  1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/gcc/cp/logic.cc b/gcc/cp/logic.cc
index fab2c357dc4..e46ea0ebb78 100644
--- a/gcc/cp/logic.cc
+++ b/gcc/cp/logic.cc
@@ -349,7 +349,7 @@ atomic_p (tree t)
     distributing.  In general, a conjunction for which this flag is set
     is considered a disjunction for the purpose of counting.  */
  
-static std::pair<int, bool>
+static std::pair<unsigned HOST_WIDE_INT, bool>
  dnf_size_r (tree t)
  {
    if (atomic_p (t))
@@ -360,9 +360,9 @@ dnf_size_r (tree t)
       the results.  */
    tree lhs = TREE_OPERAND (t, 0);
    tree rhs = TREE_OPERAND (t, 1);
-  std::pair<int, bool> p1 = dnf_size_r (lhs);
-  std::pair<int, bool> p2 = dnf_size_r (rhs);
-  int n1 = p1.first, n2 = p2.first;
+  auto p1 = dnf_size_r (lhs);
+  auto p2 = dnf_size_r (rhs);
+  unsigned HOST_WIDE_INT n1 = p1.first, n2 = p2.first;
    bool d1 = p1.second, d2 = p2.second;
  
    if (disjunction_p (t))
@@ -457,7 +457,7 @@ dnf_size_r (tree t)
     distributing.  In general, a disjunction for which this flag is set
     is considered a conjunction for the purpose of counting.  */
  
-static std::pair<int, bool>
+static std::pair<unsigned HOST_WIDE_INT, bool>
  cnf_size_r (tree t)
  {
    if (atomic_p (t))
@@ -468,9 +468,9 @@ cnf_size_r (tree t)
       the results.  */
    tree lhs = TREE_OPERAND (t, 0);
    tree rhs = TREE_OPERAND (t, 1);
-  std::pair<int, bool> p1 = cnf_size_r (lhs);
-  std::pair<int, bool> p2 = cnf_size_r (rhs);
-  int n1 = p1.first, n2 = p2.first;
+  auto p1 = cnf_size_r (lhs);
+  auto p2 = cnf_size_r (rhs);
+  unsigned HOST_WIDE_INT n1 = p1.first, n2 = p2.first;
    bool d1 = p1.second, d2 = p2.second;
  
    if (disjunction_p (t))
@@ -560,10 +560,10 @@ cnf_size_r (tree t)
  /* Count the number conjunctive clauses that would be created
     when rewriting T to DNF.  */
  
-static int
+static unsigned HOST_WIDE_INT
  dnf_size (tree t)
  {
-  std::pair<int, bool> result = dnf_size_r (t);
+  auto result = dnf_size_r (t);
    return result.first == 0 ? 1 : result.first;
  }
  
@@ -571,10 +571,10 @@ dnf_size (tree t)
  /* Count the number disjunctive clauses that would be created
     when rewriting T to CNF.  */
  
-static int
+static unsigned HOST_WIDE_INT
  cnf_size (tree t)
  {
-  std::pair<int, bool> result = cnf_size_r (t);
+  auto result = cnf_size_r (t);
    return result.first == 0 ? 1 : result.first;
  }