runtimeverification / wasm-semantics

A Prototype Formal Semantics of WebAssembly in K
Other
77 stars 19 forks source link

Support `memory.fill` #670

Closed gtrepta closed 1 month ago

gtrepta commented 1 month ago

This adds the semantics for the memory.fill instruction.

In the spec they desugar the instruction into a sequence of i32.store8 instructions. For efficiency, we just use the #setBytesRange function.

https://webassembly.github.io/spec/core/exec/instructions.html#xref-syntax-instructions-syntax-instr-memory-mathsf-memory-fill