runtimeverification / runtimeverification/wasm-semantics

Function signatures aren't available during `Text2Abstract` on function definitions

Open
#663 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Dominant language
WebAssembly
Stars
106
Forks
24
PR merge metrics
No merged PRs in 30d

Description

Some information about a module doesn't get passed down to one of the text2abstract operations that need it:
https://github.com/runtimeverification/wasm-semantics/blob/b353017e7178731daa12cba75dc81fd69e20a81f/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm-text.md?plain=1#L837-L849

On line 839, t2aDefns is invoked on the functions of the module with the context C. However, this context doesn't contain the signatures for the types in the module, only their ids. So, when t2a goes to calculate the indices of the variables in a function body, it doesn't have the function parameters for named types.

Here's an example from the wasm tests func.wast that fails because of this:

(module
  (type $sig (func (param i32) (result i32)))

  (func (export "f") (type $sig)
    (local $var i32)
    (local.get $var)
  )
)

(assert_return (invoke "f" (i32.const 42)) (i32.const 0))

$var here is assigned index 0. But, it should be 1, as the (param i32) in the function signature is at index 0 already. So, when "f" gets invoked, (local.get 0) is evaluated and returned, which is where the 42 that was passed in is at.

Relevant rules:

https://github.com/runtimeverification/wasm-semantics/blob/b353017e7178731daa12cba75dc81fd69e20a81f/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm-text.md?plain=1#L883-L888

https://github.com/runtimeverification/wasm-semantics/blob/b353017e7178731daa12cba75dc81fd69e20a81f/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm-text.md?plain=1#L1309-L1325

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Start in pykwasm/kdist/wasm-semantics/wasm-text.md at the t2aDefns invocation around lines 837-849, then read the related rules around lines 883-888 and 1309-1325. Use the func.wast example with a named function type and parameter as the regression case. Done means named locals receive indices after the function parameters and the example no longer evaluates the local at index 0.

Written by the indexing model from the issue text.

Assessment

Tech stack
wasm
Domain
compilers
Issue type
Bug
Difficulty
3/5
Estimated time
1-2 days
Activity status
Stale
Clarity
Clearly specified
Newbie friendliness
55/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.