WebAssembly support for crucible #594
Conversation
|
Since the initial comment, I've added support for:
Finishing indirect function call support for symbolic arguments will probably require the same work as a fix for #10, which is support for truly symbolic function handles. |
robdockins
force-pushed
the
wasm
branch
2 times, most recently
from
1a17379
to
65e24af
Compare
|
I'd like to get some resolution to SPY/haskell-wasm#10 before we merge this, but I think this is otherwise ready to merge. I don't want this to get too out of date before merging, even though it is incomplete. |
There was a problem hiding this comment.
This looks really clear and clean!
I realize it was a "pencils down" situation that stopped your work, so apologies for the comments on the todo-ish portions, but it would be good to get those into an actionable form.
Most of the rest of the comments are stylistic or suggestions, so feel free to ignore if you don't like them.
I'm looking forward to seeing this merged into crucible master!
| return ss | ||
|
|
||
| execCommand c ss = | ||
| do liftIO $ putStrLn $ unwords ["Command not implemented", show c] |
There was a problem hiding this comment.
That's a good question. I'm coming around to the idea that we should perhaps make a distinction between panic and unimplemented. In my mind, panic means the programmer has thought about this and believes that various explicit or implicit invariants mean that the situation cannot occur, and it is a programming mistake bug if the situation occurs. Whereas, unimplemented or unsupported is explicitly an acknowledgement that valid inputs can drive the program into this situation, but we just haven't written the necessary code to deal with it.
Operationally, I think unimplemented should probably raise an appropriate (potentially non-fatal) exception instead of printing the panic message and immediately exiting.
There was a problem hiding this comment.
I agree that there's definitely a semantic differentiation, but is there a runtime distinction (i.e. can it be a non-fatal/recoverable exception if it's truly unimplemented)? If so, then yes, let's make an unimplemented, otherwise we can just make sure the panic message clarifies the distinction (or I guess we can make an unimplemented that does the latter).
There was a problem hiding this comment.
Well... for something like SAW, I guess I'd rather see some useful "unimplemented" message and end up back at the SAW prompt rather than baling out of the executable altogether like panic does.
There was a problem hiding this comment.
My overall thinking relative to all the panic notes below is leaving the right breadcrumbs for both the user and the developer to know who to tell and where to fix it when these unimplemented/todo/whatever things get encountered.
As context: Comments in the code, print statements that might get lost or don't suggest there needs to be a report, or error calls that might simply result in alternatives or quietly unsatisfiable branches are mostly passive and could result in invalid analyses or a lot of debugging to figure out why something isn't working right, which is why I tend to default to a fairly agressive reaction like panic.
This package currently is capable of loading WebAssembly modules and simulating a subset of concrte programs that use integer values, control flow and memory. There is a very basic `crux` driver layer that loads scripts from the `haskell-wasm` test suite and executes them (only a subset of the assertions in those scripts are supported, however). There is plenty of work still to be done, but the existing subset will allow some nontrivial programs to be simulated, and a bit more crux infrastructure support would allow serious symbolic simulation testing to begin.
This PR implements a rough first cut at providing WebAssembly translation support for Crucible. Support is currently incomplete in a variety of ways. For reference, I have been following the WebAssembly 1.0 specification, which may be found here:
https://www.w3.org/TR/2019/REC-wasm-core-1-20191205 (there is a newer 1.1 spec, but it doesn't seem to have much uptake yet, and the changes seem relatively small).
What works:
haskell-wasmpackageassert_returnclauses of thehaskell-wasmtest suiteWhat doesn't work yet:
Other rough edges:
haskell-wasm. I have not yet tried to get these changes incorporated upstreamerrorcalls should be converted topanic, as they should be ruled out by module verification, and others should be reported in more appropriate ways.