-
Notifications
You must be signed in to change notification settings - Fork 13.3k
hang in fulfill due to exponential blowup #110544
New issue
Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? # to your account
Comments
matthiaskrgr
added a commit
to matthiaskrgr/rust
that referenced
this issue
Apr 27, 2023
…w-response, r=lcnr Clear response values for overflow in new solver When we have an overflow, return a trivial query response. This fixes an ICE with the code described in rust-lang#110544: ```rust trait Trait {} struct W<T>(T); impl<T, U> Trait for W<(W<T>, W<U>)> where W<T>: Trait, W<U>: Trait, {} fn impls<T: Trait>() {} fn main() { impls::<W<_>>() } ``` Where, while proving `W<?0>: Trait`, we overflow but still apply the query response of `?0 = (W<?1>, W<?2>)`. Then while re-processing the query to validate that our evaluation result was stable, we get a different query response that looks like `?1 = (W<?3>, W<?4>), ?2 = (W<?5>, W<?6>)`, and so we trigger the ICE. Also, by returning a trivial query response we also avoid the infinite-loop/OOM behavior of the old solver. r? `@lcnr`
GuillaumeGomez
added a commit
to GuillaumeGomez/rust
that referenced
this issue
Apr 28, 2023
…w-response, r=lcnr Clear response values for overflow in new solver When we have an overflow, return a trivial query response. This fixes an ICE with the code described in rust-lang#110544: ```rust trait Trait {} struct W<T>(T); impl<T, U> Trait for W<(W<T>, W<U>)> where W<T>: Trait, W<U>: Trait, {} fn impls<T: Trait>() {} fn main() { impls::<W<_>>() } ``` Where, while proving `W<?0>: Trait`, we overflow but still apply the query response of `?0 = (W<?1>, W<?2>)`. Then while re-processing the query to validate that our evaluation result was stable, we get a different query response that looks like `?1 = (W<?3>, W<?4>), ?2 = (W<?5>, W<?6>)`, and so we trigger the ICE. Also, by returning a trivial query response we also avoid the infinite-loop/OOM behavior of the old solver. r? ``@lcnr``
matthiaskrgr
added a commit
to matthiaskrgr/rust
that referenced
this issue
Apr 29, 2023
…w-response, r=lcnr Clear response values for overflow in new solver When we have an overflow, return a trivial query response. This fixes an ICE with the code described in rust-lang#110544: ```rust trait Trait {} struct W<T>(T); impl<T, U> Trait for W<(W<T>, W<U>)> where W<T>: Trait, W<U>: Trait, {} fn impls<T: Trait>() {} fn main() { impls::<W<_>>() } ``` Where, while proving `W<?0>: Trait`, we overflow but still apply the query response of `?0 = (W<?1>, W<?2>)`. Then while re-processing the query to validate that our evaluation result was stable, we get a different query response that looks like `?1 = (W<?3>, W<?4>), ?2 = (W<?5>, W<?6>)`, and so we trigger the ICE. Also, by returning a trivial query response we also avoid the infinite-loop/OOM behavior of the old solver. r? `@lcnr`
Dylan-DPC
added a commit
to Dylan-DPC/rust
that referenced
this issue
Apr 29, 2023
…w-response, r=lcnr Clear response values for overflow in new solver When we have an overflow, return a trivial query response. This fixes an ICE with the code described in rust-lang#110544: ```rust trait Trait {} struct W<T>(T); impl<T, U> Trait for W<(W<T>, W<U>)> where W<T>: Trait, W<U>: Trait, {} fn impls<T: Trait>() {} fn main() { impls::<W<_>>() } ``` Where, while proving `W<?0>: Trait`, we overflow but still apply the query response of `?0 = (W<?1>, W<?2>)`. Then while re-processing the query to validate that our evaluation result was stable, we get a different query response that looks like `?1 = (W<?3>, W<?4>), ?2 = (W<?5>, W<?6>)`, and so we trigger the ICE. Also, by returning a trivial query response we also avoid the infinite-loop/OOM behavior of the old solver. r? ``@lcnr``
# for free
to join this conversation on GitHub.
Already have an account?
# to comment
this program results in a hang in both rustc (fulfill) and in r-a (causing my PC to freeze).
if we prove this using a breadth first approach we try to prove
O(2^recursion_limit)
goalsThe text was updated successfully, but these errors were encountered: