You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
Those invariants are ciritcal to the safety and working 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
All registers of all instructions of a translated function are valid.
In particular register in the preservation space are properly defragmented.
All function, table, memory and global indices are valid for the given ModuleHeader and Engine.
If consume_fuel is enabled, no BranchOffset[16]s may be 0.
If consume_fuel is enabled, all BranchOffset[16]s that jump backwards must target a ConsumeFuel instruction.
All ConsumeFuel instructions must consume at least 1 fuel.
All BranchOffset[16]s must have valid jump destinations within the same function.
All (conditional) return instructions must return the same number as the number of results of the translated function.
The text was updated successfully, but these errors were encountered:
Robbepop
changed the title
A debug post-conditions for Wasmi translation
Add debug post-conditions for Wasmi translation
Sep 30, 2024
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.Those invariants are ciritcal to the safety and working 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
ModuleHeader
andEngine
.consume_fuel
is enabled, noBranchOffset[16]
s may be 0.consume_fuel
is enabled, allBranchOffset[16]
s that jump backwards must target aConsumeFuel
instruction.ConsumeFuel
instructions must consume at least 1 fuel.BranchOffset[16]
s must have valid jump destinations within the same function.The text was updated successfully, but these errors were encountered: