ping ping (Apr 14 2025 at 08:28): ping ping (Apr 14 2025 at 08:28):Hi, I'm new to Cranelift and currently exploring the ISLE language. While examining inst.isle, I encountered the spec keyword in patterns like this:
(decl x64_movrm (Type SyntheticAmode Gpr) SideEffectNoResult)
(spec (x64_movrm ty addr data)
(provide (= result (store_effect (extract 79 64 addr) ty (conv_to ty data) (extract 63 0 addr)))))
(rule (x64_movrm ty addr data)
(let ((size OperandSize (raw_operand_size_of_type ty)))
(SideEffectNoResult.Inst (MInst.MovRM size data addr))))
I searched the ISLE language documentation but couldn't find any explanation of the spec keyword. Could someone clarify:
What role does spec play here?
Is there documentation available for such keywords, or could the existing docs be updated to include them?
Any guidance or references would be greatly appreciated!
bjorn3 (Apr 14 2025 at 11:15):These were introduced by https://github.com/bytecodealliance/wasmtime/pull/9178
ping ping (Apr 14 2025 at 13:01):Thank you for your response and for sharing the reference to PR #9178. I was able to find an approximate explanation of the spec keyword through that context.
Would it be possible to include this reference in the ISLE language documentation? I believe this would greatly benefit other newcomers to ISLE who might encounter similar questions about the spec.
Chris Fallin (Apr 14 2025 at 19:56):Hi @ping ping -- the specification features are the subject of recent work by @Alexa VanHattum and currently carried on by @Michael McLoughlin -- the best overview we have is actually the paper we published on the work (https://cs.wellesley.edu/~avh/veri-isle-preprint.pdf). It's not yet at the point where it has a full set of documentation ready for third-party users; hopefully we'll reach that point eventually.
ping ping (Apr 15 2025 at 11:31):Thanks for sharing the paper! Looking forward to the completed documentation.
Chris Fallin (Apr 15 2025 at 15:46):Can you say more what you're trying to use it for? That might be interesting to us (me and Alexa, Michael, and the rest of our collaborators)
ping ping (Apr 15 2025 at 17:45):Thank you for your response! I'm a PhD student currently learning compiler technologies, and I'm exploring Cranelift as a case study to understand modern code generation techniques. Along the way, I'm also looking for potential research opportunities.
Last updated: Dec 06 2025 at 07:03 UTC