wasmi-labs/wasmi

Add debug post-conditions for Wasmi translation

Robbepop opened this issue · 1 comments

In order to improve fuzzing and Wasmi translation stability we should add more post-condition checks to the Wasmi translator.

The reason is that the Wasmi translator has pre-condition checking in the form of wasmparser's Wasm validation but lacks its own post-conditions to verify for debug builds that the Wasmi bytecode it produced aligns with the invariants that it guarantees to its users, i.e. the Wasmi executor.

Those invariants are ciritcal to the correctness of the Wasmi executor since it fully relies on them.

This issue tracks progress of the implementation and lists the concrete conditions that we plan to implement.

The listed post-conditions are checked after function translation has already finished. So they are used to detect bugs in the Wasmi translator more easily.

Post-Conditions

#1233 (comment)

Started implementation here: #1233