Monica Pardeshi (Feb 03 2022 at 00:49): Monica Pardeshi (Feb 03 2022 at 00:49):I'm trying to visualize how isle rewrites clif instructions, so I was playing around with isle tries. I was able to pretty print them but I'm wondering if there's a way to map from ir constructs back to easily readable lines of isle.
Chris Fallin (Feb 03 2022 at 01:22):@Monica Pardeshi that's a good question! At the moment, no, but I can see how one might be able to map from the trie back to rules; basically enumerate all paths to leaves, recover the LHS (sequence of PatternInst) and get the RHS (sequence of ExprInst) from the leaf, and then decompile the two sequences to ASTs. The last bit is a little tricky in the presence of sharing; we lose some information while lowering from AST to IR ops
Chris Fallin (Feb 03 2022 at 01:24):At a higher level though, what information are you looking to extract from the ISLE? Just exploring or is this meant to be a frontend to a translation to some other thing (SMT formulae or whatnot)? Happy to talk about what level might be easiest to start from given a target!
Monica Pardeshi (Feb 03 2022 at 02:07):Thanks for the idea, Chris!!
This is just to help us see how the rules are related. Originally we were looking to find the depth so that we would have an idea of how deeply nested our SMT would be. But then we got a little curious about exactly which rules can be substituted at each step. For example, what other rules would be on the path if we try to lower an iadd instruction?
Chris Fallin (Feb 03 2022 at 17:33):Ah, I see. It seems like adding some tracing to the generated Rust code might help with that -- for example, at the top of every generated constructor, add a println with the arguments; and when emitting the code for each leaf node (right-hand side), add a message showing which rule (file, line number) was chosen
Chris Fallin (Feb 03 2022 at 17:34):if you'd like I can point out the places that would need to change for this!
Chris Fallin (Feb 03 2022 at 17:34):(I imagine a more formal trace of term rewrites might be useful for some sort of translation validation approach as well; interesting to think about what such an interface might look like)
Monica Pardeshi (Feb 04 2022 at 00:39):Yes, file and line number would be helpful too! I was thinking about this but couldn't find a way to do it. It would be great if you could point out places to make changes :)
Chris Fallin (Feb 04 2022 at 00:51):Cool, so to instrument the generated code to emit a trace of the lowering logic, you could add a generated println after this line [1], which is the opening fn f(...) { generated for each constructor term, and possibly iterate over and emit args too. Then here [2] you can see where we emit a comment in the generated code saying where an RHS body came from (file and line); you could add a generated println here too, so the lowering code says something like "now at lower.isle line 123".
Also, as a general note, for targeted tracing/modifications, it should be ok to modify the generated code as well. If you regenerate it you'll lose the changes of course, but regeneration is always an explicit opt-in via Cargo feature. So you could e.g. just add a println at the top of lower(), then dig in from there.
[1] https://github.com/bytecodealliance/wasmtime/blob/a519e5ab645899fb29017d78b5174ad249fdcf84/cranelift/isle/isle/src/codegen.rs#L287-L292
[2] https://github.com/bytecodealliance/wasmtime/blob/a519e5ab645899fb29017d78b5174ad249fdcf84/cranelift/isle/isle/src/codegen.rs#L674-L680
Monica Pardeshi (Feb 04 2022 at 01:38):I'll try it! Thanks for the advice!
Last updated: Dec 23 2024 at 13:07 UTC