Skip to content

[spectec] Wasm 1.0: $growmemory does not enforce the page limit #2219

Description

@lzy0505

The Wasm 1.0 execution rule for memory.grow succeeds only if the resulting memory size is no greater than 2^16 pages.

The official WebAssembly Specification, Release 1.0 PDF states:

“If len is larger than 2¹⁶, then fail.”

growmem includes:

len ≤ 2¹⁶

Currently the spectec rule is:

def $growmemory(mi, n) = mi'
  -- if mi = { TYPE `[i .. j?], BYTES b* }
  -- if i' = $(|b*| / (64 * $Ki) + n)
  -- if mi' = { TYPE `[i' .. j?], BYTES b* 0^(n * $($(64 * $Ki))) }
  -- (if i' <= j)?

It is missing the condition -- if $(i' <= 65536)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions