On Tue, Dec 17, 2024 at 10:43:49AM -0500, 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.
>
> -- >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.
Sorry for a silly question, but is there a reason to prefer
unsigned HOST_WIDE_INT over uint64_t?
Patch seems fine, though, thanks.
> 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;
> }
>
> --
> 2.48.0.rc0
>
Marek
