c++: integer overflow during constraint subsumption [PR118069]

For the testcase in the PR we hang during constraint subsumption
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 64-bit saturating arithmetic during
these size calculations (via new add/mul_sat_hwi functions) so that
overflow is less likely and if it does occur we handle it gracefully.
It should be highly unlikely that both the DNF and CNF sizes overflow,
and if they do then it doesn't matter which form we select, subsumption
will take forever either way.  The testcase now compiles in ~3 seconds
on my machine after this change.

	PR c++/118069

gcc/ChangeLog:

	* hwint.h (add_sat_hwi): New function.
	(mul_sat_hwi): Likewise.

gcc/cp/ChangeLog:

	* logic.cc (dnf_size_r): Use HOST_WIDE_INT instead of int, and
	handle overflow gracefully via add_sat_hwi and mul_sat_hwi.
	(cnf_size_r): Likewise.
	(dnf_size): Use HOST_WIDE_INT instead of int.
	(cnf_size): Likewise.

Reviewed-by: Jason Merrill <jason@redhat.com>

diff --git a/gcc/cp/logic.cc b/gcc/cp/logic.cc
index fab2c357dc4eb0e5f94e84333441a44f0336572a..a385fb719ecaa8c9176bff6e0168ea639bbe94ac 100644 (file)
--- 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<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);
+  HOST_WIDE_INT n1 = p1.first, n2 = p2.first;
   bool d1 = p1.second, d2 = p2.second;
 
   if (disjunction_p (t))
@@ -376,22 +376,24 @@ dnf_size_r (tree t)
        {
          if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
            /* Both P and Q are disjunctions.  */
-           return std::make_pair (n1 + n2, d1 | d2);
+           return std::make_pair (add_sat_hwi (n1, n2), d1 | d2);
          else
            /* Only LHS is a disjunction.  */
-           return std::make_pair (1 + n1 + n2, d1 | d2);
+           return std::make_pair (add_sat_hwi (1, add_sat_hwi (n1, n2)),
+                                  d1 | d2);
          gcc_unreachable ();
        }
       if (conjunction_p (lhs))
        {
          if ((disjunction_p (rhs) && d1) || (conjunction_p (rhs) && d1 && d2))
            /* Both P and Q are disjunctions.  */
-           return std::make_pair (n1 + n2, d1 | d2);
+           return std::make_pair (add_sat_hwi (n1, n2), d1 | d2);
          if (disjunction_p (rhs)
              || (conjunction_p (rhs) && d1 != d2)
              || (atomic_p (rhs) && d1))
            /* Either LHS or RHS is a disjunction.  */
-           return std::make_pair (1 + n1 + n2, d1 | d2);
+           return std::make_pair (add_sat_hwi (1, add_sat_hwi (n1, n2)),
+                                  d1 | d2);
          else
            /* Neither LHS nor RHS is a disjunction.  */
            return std::make_pair (2, false);
@@ -400,7 +402,8 @@ dnf_size_r (tree t)
        {
          if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
            /* Only RHS is a disjunction.  */
-           return std::make_pair (1 + n1 + n2, d1 | d2);
+           return std::make_pair (add_sat_hwi (1, add_sat_hwi (n1, n2)),
+                                  d1 | d2);
          else
            /* Neither LHS nor RHS is a disjunction.  */
            return std::make_pair (2, false);
@@ -418,22 +421,22 @@ dnf_size_r (tree t)
        {
          if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
            /* Both P and Q are disjunctions.  */
-           return std::make_pair (n1 * n2, true);
+           return std::make_pair (mul_sat_hwi (n1, n2), true);
          else
            /* Only LHS is a disjunction.  */
-           return std::make_pair (n1 + n2, true);
+           return std::make_pair (add_sat_hwi (n1, n2), true);
          gcc_unreachable ();
        }
       if (conjunction_p (lhs))
        {
          if ((disjunction_p (rhs) && d1) || (conjunction_p (rhs) && d1 && d2))
            /* Both P and Q are disjunctions.  */
-           return std::make_pair (n1 * n2, true);
+           return std::make_pair (mul_sat_hwi (n1, n2), true);
          if (disjunction_p (rhs)
              || (conjunction_p (rhs) && d1 != d2)
              || (atomic_p (rhs) && d1))
            /* Either LHS or RHS is a disjunction.  */
-           return std::make_pair (n1 + n2, true);
+           return std::make_pair (add_sat_hwi (n1, n2), true);
          else
            /* Neither LHS nor RHS is a disjunction.  */
            return std::make_pair (0, false);
@@ -457,7 +460,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<HOST_WIDE_INT, bool>
 cnf_size_r (tree t)
 {
   if (atomic_p (t))
@@ -468,9 +471,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);
+  HOST_WIDE_INT n1 = p1.first, n2 = p2.first;
   bool d1 = p1.second, d2 = p2.second;
 
   if (disjunction_p (t))
@@ -485,12 +488,12 @@ cnf_size_r (tree t)
        {
          if ((disjunction_p (rhs) && d1 && d2) || (conjunction_p (rhs) && d1))
            /* Both P and Q are conjunctions.  */
-           return std::make_pair (n1 * n2, true);
+           return std::make_pair (mul_sat_hwi (n1, n2), true);
          if ((disjunction_p (rhs) && d1 != d2)
              || conjunction_p (rhs)
              || (atomic_p (rhs) && d1))
            /* Either LHS or RHS is a conjunction.  */
-           return std::make_pair (n1 + n2, true);
+           return std::make_pair (add_sat_hwi (n1, n2), true);
          else
            /* Neither LHS nor RHS is a conjunction.  */
            return std::make_pair (0, false);
@@ -499,16 +502,16 @@ cnf_size_r (tree t)
        {
          if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
            /* Both LHS and RHS are conjunctions.  */
-           return std::make_pair (n1 * n2, true);
+           return std::make_pair (mul_sat_hwi (n1, n2), true);
          else
            /* Only LHS is a conjunction.  */
-           return std::make_pair (n1 + n2, true);
+           return std::make_pair (add_sat_hwi (n1, n2), true);
        }
       if (atomic_p (lhs))
        {
          if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
            /* Only RHS is a disjunction.  */
-           return std::make_pair (n1 + n2, true);
+           return std::make_pair (add_sat_hwi (n1, n2), true);
          else
            /* Neither LHS nor RHS is a disjunction.  */
            return std::make_pair (0, false);
@@ -525,12 +528,13 @@ cnf_size_r (tree t)
        {
          if ((disjunction_p (rhs) && d1 && d2) || (conjunction_p (rhs) && d1))
            /* Both P and Q are conjunctions.  */
-           return std::make_pair (n1 + n2, d1 | d2);
+           return std::make_pair (add_sat_hwi (n1, n2), d1 | d2);
          if ((disjunction_p (rhs) && d1 != d2)
              || conjunction_p (rhs)
              || (atomic_p (rhs) && d1))
            /* Either LHS or RHS is a conjunction.  */
-           return std::make_pair (1 + n1 + n2, d1 | d2);
+           return std::make_pair (add_sat_hwi (1, add_sat_hwi (n1, n2)),
+                                  d1 | d2);
          else
            /* Neither LHS nor RHS is a conjunction.  */
            return std::make_pair (2, false);
@@ -539,16 +543,18 @@ cnf_size_r (tree t)
        {
          if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
            /* Both LHS and RHS are conjunctions.  */
-           return std::make_pair (n1 + n2, d1 | d2);
+           return std::make_pair (add_sat_hwi (n1, n2), d1 | d2);
          else
            /* Only LHS is a conjunction.  */
-           return std::make_pair (1 + n1 + n2, d1 | d2);
+           return std::make_pair (add_sat_hwi (1, add_sat_hwi (n1, n2)),
+                                  d1 | d2);
        }
       if (atomic_p (lhs))
        {
          if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
            /* Only RHS is a disjunction.  */
-           return std::make_pair (1 + n1 + n2, d1 | d2);
+           return std::make_pair (add_sat_hwi (1, add_sat_hwi (n1, n2)),
+                                  d1 | d2);
          else
            /* Neither LHS nor RHS is a disjunction.  */
            return std::make_pair (2, false);
@@ -560,10 +566,10 @@ cnf_size_r (tree t)
 /* Count the number conjunctive clauses that would be created
    when rewriting T to DNF.  */
 
-static int
+static 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 +577,10 @@ dnf_size (tree t)
 /* Count the number disjunctive clauses that would be created
    when rewriting T to CNF.  */
 
-static int
+static 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;
 }
 

diff --git a/gcc/hwint.h b/gcc/hwint.h
index f69b61db9cc632b5a69d92fa8e997f361fd5e442..e07a12a4097f84709e1090fee40ea6692c0cbc5c 100644 (file)
--- a/gcc/hwint.h
+++ b/gcc/hwint.h
@@ -397,4 +397,30 @@ mul_hwi (HOST_WIDE_INT a, HOST_WIDE_INT b, bool *overflow)
 #endif
 }
 
+/* Compute the saturated sum of signed A and B, i.e. upon overflow clamp
+   the result to the corresponding extremum.  */
+
+inline HOST_WIDE_INT
+add_sat_hwi (HOST_WIDE_INT a, HOST_WIDE_INT b)
+{
+  bool overflow;
+  HOST_WIDE_INT result = add_hwi (a, b, &overflow);
+  if (!overflow)
+    return result;
+  return (a < 0) ? HOST_WIDE_INT_MIN : HOST_WIDE_INT_MAX;
+}
+
+/* Compute the saturated product of signed A and B, i.e. upon overflow clamp
+   the result to the corresponding extremum.  */
+
+inline HOST_WIDE_INT
+mul_sat_hwi (HOST_WIDE_INT a, HOST_WIDE_INT b)
+{
+  bool overflow;
+  HOST_WIDE_INT result = mul_hwi (a, b, &overflow);
+  if (!overflow)
+    return result;
+  return ((a < 0) != (b < 0)) ? HOST_WIDE_INT_MIN : HOST_WIDE_INT_MAX;
+}
+
 #endif /* ! GCC_HWINT_H */