Bongjun Jang (Aug 28 2025 at 07:38): Bongjun Jang (Aug 28 2025 at 07:38):Hi,
just out of curiosity,
I wonder if the termination of the Cranelift optimizer (written in ISLE) is guaranteed.
For example, if we have a simplify rule of commutativity of addition,
(iadd x y) => (iadd y x) => ... can loop forever.
Is such a bug possible in theory, according to the current design of Cranelift?
I'm aware of the directional e-graph approach with code skeleton reconstruction.
But I find it hard to make a conclusion for the question.
Chris Fallin (Aug 28 2025 at 16:15):It's guaranteed for the trivial reason that we bound the rewrite step count (at 5, currently) :-) But you're right, in general, without that one couldn't prove termination with our general ruleset and abstractions
Bongjun Jang (Aug 29 2025 at 01:17):Thanks!
Last updated: Dec 06 2025 at 07:03 UTC