runtimeverification / wasm-semantics

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

Lost stack values when entering a loop #678

Open gtrepta opened 1 month ago

gtrepta commented 1 month ago
(module
  ;; Iterative factorial without locals.
  (func $pick0 (param i64) (result i64 i64)
    (local.get 0) (local.get 0)
  )
  (func $pick1 (param i64 i64) (result i64 i64 i64)
    (local.get 0) (local.get 1) (local.get 0)
  )
  (func (export "fac-ssa") (param i64) (result i64)
    (i64.const 1) (local.get 0)
    (loop $l (param i64 i64) (result i64)
      (call $pick1) (call $pick1) (i64.mul)
      (call $pick1) (i64.const 1) (i64.sub)
      (call $pick0) (i64.const 0) (i64.gt_u)
      (br_if $l)
      (drop) (return)
    )
  )
)

(assert_return (invoke "fac-ssa" (i64.const 25)) (i64.const 7034535277573963776))

After fac-ssa gets invoked and the loop instruction is reached, the two values that have been pushed onto the stack disappear when we enter the loop, so then the subsequent call to $pick1 doesn't have any parameters to use.

The spec

Our rule:

https://github.com/runtimeverification/wasm-semantics/blob/ad238ca2f73ea866b54b31308326ac2a56e64159/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md?plain=1#L549-L552

It looks like the spec states that the stack values are prepended to the instructions when entering the block, but we aren't doing that here.