about summary refs log tree commit diff
diff options
context:
space:
mode:
authorlcnr <rust@lcnr.de>2023-12-09 09:47:14 +0000
committerlcnr <rust@lcnr.de>2023-12-09 10:35:07 +0000
commitef796db5f0d4eecce0dd2ae9fff224542fb88f5b (patch)
tree7b9b8e48d10011e1d366659cdc6740e509eb150a
parent608f32435afd5b61f61c593e70df1a2b8ada6a79 (diff)
downloadrust-ef796db5f0d4eecce0dd2ae9fff224542fb88f5b.tar.gz
rust-ef796db5f0d4eecce0dd2ae9fff224542fb88f5b.zip
add test for inductive cycle hangs
-rw-r--r--tests/ui/traits/new-solver/cycles/coinduction/fixpoint-exponential-growth.rs8
-rw-r--r--tests/ui/traits/new-solver/cycles/coinduction/fixpoint-exponential-growth.stderr4
-rw-r--r--tests/ui/traits/new-solver/cycles/inductive-fixpoint-hang.rs33
-rw-r--r--tests/ui/traits/new-solver/cycles/inductive-fixpoint-hang.stderr16
4 files changed, 57 insertions, 4 deletions
diff --git a/tests/ui/traits/new-solver/cycles/coinduction/fixpoint-exponential-growth.rs b/tests/ui/traits/new-solver/cycles/coinduction/fixpoint-exponential-growth.rs
index 44e763ef990..07c7d4fb29c 100644
--- a/tests/ui/traits/new-solver/cycles/coinduction/fixpoint-exponential-growth.rs
+++ b/tests/ui/traits/new-solver/cycles/coinduction/fixpoint-exponential-growth.rs
@@ -3,8 +3,12 @@
 // Proving `W<?0>: Trait` instantiates `?0` with `(W<?1>, W<?2>)` and then
 // proves `W<?1>: Trait` and `W<?2>: Trait`, resulting in a coinductive cycle.
 //
-// Proving coinductive cycles runs until we reach a fixpoint. This fixpoint is
-// never reached here and each step doubles the amount of nested obligations.
+// Proving coinductive cycles runs until we reach a fixpoint. However, after
+// computing `try_evaluate_added_goals` in the second fixpoint iteration, the
+// self type already has a depth equal to the number of steps. This results
+// in enormous constraints, causing the canonicalizer to hang without ever
+// reaching the recursion limit. We currently avoid that by erasing the constraints
+// from overflow.
 //
 // This previously caused a hang in the trait solver, see
 // https://github.com/rust-lang/trait-system-refactor-initiative/issues/13.
diff --git a/tests/ui/traits/new-solver/cycles/coinduction/fixpoint-exponential-growth.stderr b/tests/ui/traits/new-solver/cycles/coinduction/fixpoint-exponential-growth.stderr
index 05aaf6108f1..150100f2c53 100644
--- a/tests/ui/traits/new-solver/cycles/coinduction/fixpoint-exponential-growth.stderr
+++ b/tests/ui/traits/new-solver/cycles/coinduction/fixpoint-exponential-growth.stderr
@@ -1,12 +1,12 @@
 error[E0275]: overflow evaluating the requirement `W<_>: Trait`
-  --> $DIR/fixpoint-exponential-growth.rs:29:13
+  --> $DIR/fixpoint-exponential-growth.rs:33:13
    |
 LL |     impls::<W<_>>();
    |             ^^^^
    |
    = help: consider increasing the recursion limit by adding a `#![recursion_limit = "256"]` attribute to your crate (`fixpoint_exponential_growth`)
 note: required by a bound in `impls`
-  --> $DIR/fixpoint-exponential-growth.rs:26:13
+  --> $DIR/fixpoint-exponential-growth.rs:30:13
    |
 LL | fn impls<T: Trait>() {}
    |             ^^^^^ required by this bound in `impls`
diff --git a/tests/ui/traits/new-solver/cycles/inductive-fixpoint-hang.rs b/tests/ui/traits/new-solver/cycles/inductive-fixpoint-hang.rs
new file mode 100644
index 00000000000..062c6ae98d5
--- /dev/null
+++ b/tests/ui/traits/new-solver/cycles/inductive-fixpoint-hang.rs
@@ -0,0 +1,33 @@
+// compile-flags: -Ztrait-solver=next
+
+// This currently hangs if we do not erase constraints from
+// overflow.
+//
+// We set the provisional result of `W<?0>` to `?0 := W<_>`.
+// The next iteration does not simply result in a `?0 := W<W<_>` constraint as
+// one might expect, but instead each time we evaluate the nested `W<T>` goal we
+// apply the previously returned constraints: the first fixpoint iteration goes
+// as follows: `W<?1>: Trait` constrains `?1` to `W<?2>`, we then evaluate
+// `W<W<?2>>: Trait` the next time we try to prove the nested goal. This results
+// inn `W<W<W<?3>>>` and so on. This goes on until we reach overflow in
+// `try_evaluate_added_goals`.  This means the provisional result after the
+// second fixpoint iteration is already `W<W<W<...>>>` with a size proportional
+// to the number of steps in `try_evaluate_added_goals`. The size then continues
+// to grow. The exponential blowup from having 2 nested goals per impl causes
+// the solver to hang without hitting the recursion limit.
+trait Trait {}
+
+struct W<T: ?Sized>(*const T);
+
+impl<T: ?Sized> Trait for W<W<T>>
+where
+    W<T>: Trait,
+    W<T>: Trait,
+{}
+
+fn impls_trait<T: Trait>() {}
+
+fn main() {
+    impls_trait::<W<_>>();
+    //~^ ERROR overflow evaluating the requirement
+}
diff --git a/tests/ui/traits/new-solver/cycles/inductive-fixpoint-hang.stderr b/tests/ui/traits/new-solver/cycles/inductive-fixpoint-hang.stderr
new file mode 100644
index 00000000000..42451920744
--- /dev/null
+++ b/tests/ui/traits/new-solver/cycles/inductive-fixpoint-hang.stderr
@@ -0,0 +1,16 @@
+error[E0275]: overflow evaluating the requirement `W<_>: Trait`
+  --> $DIR/inductive-fixpoint-hang.rs:31:19
+   |
+LL |     impls_trait::<W<_>>();
+   |                   ^^^^
+   |
+   = help: consider increasing the recursion limit by adding a `#![recursion_limit = "256"]` attribute to your crate (`inductive_fixpoint_hang`)
+note: required by a bound in `impls_trait`
+  --> $DIR/inductive-fixpoint-hang.rs:28:19
+   |
+LL | fn impls_trait<T: Trait>() {}
+   |                   ^^^^^ required by this bound in `impls_trait`
+
+error: aborting due to 1 previous error
+
+For more information about this error, try `rustc --explain E0275`.