walker (Oct 31 2022 at 09:25): walker (Oct 31 2022 at 09:25):I am looking for formal model in Coq in particular,
Last I had this kind of discussion, I was informed that there are active efforts to formally verify cranelift.
I wonder if there any work regarding gettting formal semantics for cranelift IR ?
Why would I need that ?
I am experimenting with designing formal languages in Coq, eventually those languages will generate IR (I am exploring options now), It will be nice to show that this translation from high level IR to cranelift IR is preserving semantics. But that might not be possible without precise model of cranelift's semantics to start with
bjorn3 (Oct 31 2022 at 10:16):There is no Coq model for clif ir. There is work being done on verifying lowering of clir if to machine code using an SMT solver, but that is for individual instructions and doesn't give operational semantics for the entirety of clif ir I believe.
walker (Oct 31 2022 at 14:26):alright, another question:
How often does cranelift IR change, it is something super stable that is no longer going to change in the near future, or do we expect breaking change on regular basis ?
bjorn3 (Oct 31 2022 at 15:46):Breaking changes happen every other release or so. They are almost always not that large though. It is mostly adding new features or cleaning up old unused instructions.
Chris Fallin (Oct 31 2022 at 17:04):Yeah the periodic updates are mostly removals at this point. We've been in the process of deleting bits of the opcode and type space that were never very clearly specified or otherwise hard to work with / model (bools, iflags)
Chris Fallin (Oct 31 2022 at 17:05):the specs that @Alexa VanHattum et al are writing are in the form of a custom assertion annotation language in the ISLE, but with some work could probably be translated to some other formal language
Chris Fallin (Oct 31 2022 at 17:05):they might be interested in collaborating if you also are wanting to work toward a formal model!
walker (Oct 31 2022 at 19:32):that is interesting, I am not expert of ISLE, but I wonder how hard will it be to rewrite those specs in SAIL for example
walker (Oct 31 2022 at 19:33):also can you point me to where those specs are ? I found the ISLE directory for clift but couldn't locate clift's specs.
Chris Fallin (Oct 31 2022 at 19:43):They are working in a different repo for now (though we eventually hope to merge their work); cc @Alexa VanHattum for more details
Alexa VanHattum (Oct 31 2022 at 19:43):Hi @walker !
The current annotations (which are still a work in progress) can be found inline here: https://github.com/avanhatt/wasmtime/blob/oct-3-rebase/cranelift/codegen/src/clif.isle.
We lower these to SMT expressions relating the inputs and outputs of the corresponding ISLE terms, the code for that lowering can be found under cranelift/isle/veri/ on that same branch.
walker (Oct 31 2022 at 19:44):thank you so much, I will have to learn about ISLE and sail first in the near future, and see if translation from one to the other is easy.
thank you so much.
Alexa VanHattum (Oct 31 2022 at 19:45):It would certainly be possible to translate these to SAIL, though we are not using quite the same sort of model for values/registers as the SAIL ISA semantics I have looked at before. That difference is probably where most of the work would be.
walker (Oct 31 2022 at 21:09):notated thanks, I bookmarked this conversation for my future reference.
Last updated: Dec 23 2024 at 12:05 UTC