2 ms·
I think WebAssembly is too low level, making symbolic execution and specialization of a WebAssembly interpreter intractable or at least ineffective for all but
by wahern 4y ago
I think WebAssembly is too low level, making symbolic execution and specialization of a WebAssembly interpreter intractable or at least ineffective for all but the simplest of cases. WebAssembly doesn't even have arrays or structures--just integers, combined with a handful of "types" for global and external objects. Symbolically executing a WebAssembly interpreter (written in any language) over any non-trivial WASM code will be a parade of worst cases for such an approach. Perhaps it can be done, but I doubt it could be done in a manner that makes it a better approach (in developer time or runtime performance) than explicit compilation.
I'm not that familiar with this area, but tried to reacquaint myself by skimming through http://www.itu.dk/people/sestoft/pebook/jonesgomardsestoft-letter.pdf http://www.itu.dk/people/sestoft/pebook/jonesgomardsestoft-l... (via http://www.itu.dk/people/sestoft/pebook/ http://www.itu.dk/people/sestoft/pebook/), especially Chapter 11, "Partial Evaluation for the C Language", which I figured would highlight some the biggest potential roadblocks, even if it's not directly pertinent (i.e. in our case we might be symbolically executing a strongly typed functional language implementation of a WASM interpreter).
- UncleEntity 4y agoNot making a wasm interpreter but using it as the output of $whatever_language you choose abstract interpreter — written in $whatever_ language if you want the “free” jit compiler. It doesn’t need fancy stuff like arrays or objects since it just operates on the sandboxed wasm memory. Probably need some runtime system to deal with memory management &etc but that’s just some extra code tacked onto the module. If one wanted to get all fancy it would be: code -> ast -> ir -> optimizer -> partial eval -> wasm Or just a simple: code -> ast -> tree walker -> wasm There’s some pretty good algorithms for the first case where you get pretty close to optimal code without having to leave SSA form I’ve been reading about recently. In fact, I totally forgot about the Futamura transformations until I was reading TFA and was wondering why it wouldn’t work. —edit— I guess the first case is just a traditional compiler and it would probably not benefit from partial evaluation because there’s also an efficient algorithm that’s part of the mentioned reading to transform SSA -> AST which could be adapted to wasm output quite easily…which is on my laptop and I’m on my phone so…