runtimeverification / wasm-semantics

A Prototype Formal Semantics of WebAssembly in K
Other
78 stars 22 forks source link

Separate core semantics and text format #93

Open hjorthjort opened 5 years ago

hjorthjort commented 5 years ago

It's becoming a bit inconvenient to have all these folded instructions, aliases and syntactic sugars in the main semantics module, wasm.md. I suggest we move all rules that are just intermediate rewrites, such as instruction unfolding, into a module named normalizations.md. That way, wasm.md becomes a close mirror of the "Execution" part of the spec, dealing with the AST and state updates, and normalizations.md deals with the whole world of valid .wast concrete syntax by only rewriting top-level terms in the <k> cell.

Instead of having all these rules in the core syntax, we can keep them in a separate module. This both makes the core semantics smaller, more like the official spec, and a smaller compile target for the binary format.

Update: Here's the suggested tasks

QianyangPeng commented 5 years ago

I am also thinking about doing file splittings because the wasm.md file is getting too long. It is a good idea to split code by its purpose. We may do this after all the current features get merged.

hjorthjort commented 5 years ago

I think it's no rush, really, but it also doesn't have to wait: it should be straightforward in most cases to grab the desugaring rules and move them, and merge conflicts should be simple, since the rules for desugaring are disjoint from the rest (or should be).

We could perhaps put the new module in the same file,we don't actually need a separate file. Perhaps that's the easiest to her an overview of, especially if we want to point people to a single file for getting to see most of our semantics.

hjorthjort commented 5 years ago

Next step is drafted in #183

hjorthjort commented 5 years ago

To avoid hacks like <labeldepth>, we should probably do a pre-pass over the text format and turn it into AST format.