SpecTec can interpret any given WebAssembly (Wasm) program with respect to an input specification. It achieves this by directly interpreting the prose specification as if the specification itself were a program, effectively indirectly interpreting the Wasm program.
Internally, SpecTec represents the WebAssembly prose specification using an intermediate language called AL (Algorithmic Language). It treats the specification as an executable program composed of multiple algorithms. There are two entry algorithms: the module instantiation, and the function invocation. A Wasm module or function is provided as input to these algorithms, and the computed result is returned as output. SpecTec's AL interpreter takes the specification (represented as an AL program) as input, along with a Wasm module or function (encoded as AL runtime values). The AL interpreter then executes the specification, ultimately producing a return value that corresponds to the execution result of the given Wasm module or function.
Instantiate a Wasm module The following command instantiates the Wasm module sample.wasm using the input specification located in spec/wasm-3.0 and prints the instantiation result to stdout:
./spectec spec/wasm-3.0/*.spectec --interpreter sample.wasm
Backend_interpreter.Exception.Trap is printed.Run a Wasm test script The following command executes the test script sample.wast:
./spectec spec/wasm-3.0/*.spectec --interpreter sample.wast
Run all Wasm tests in a directory The following command runs all Wasm tests located in test-interpreter/wasm-3.0:
./spectec spec/wasm-3.0/*.spectec --interpreter test-interpreter/wasm-3.0
The prose interpreter executes the prose specification step by step, interpreting each line sequentially. Its behavior is mostly straightforward. (TODO: Formally describe the behavior of each step.)
The interpreter follows the computation model assumed in the prose specification:
z is maintained, consisting of a store s, and a current frame f (the most recently pushed frame)Trap, Throw, or Fail step is encountered, execution is immediately aborted, and no further modifications to the store are made.Some parts of the indirect interpreter still rely on the official Wasm reference interpreter:
To execute actual Wasm programs, SpecTec currently borrows the parser from the reference interpreter. The reference interpreter can parse both textual and binary representations of Wasm modules and convert them into an AST.
SpecTec includes a manual translation layer that converts between the reference interpreter’s AST representation and AL values. Whenever new syntax is added to the reference interpreter, corresponding translation logic must also be implemented manually.
One of our future goals is to automate this process by extracting the parser directly from the specification. This would allow SpecTec to parse Wasm programs using the input grammar without relying on the reference interpreter.
Some validation algorithms are hardcoded in src/backend-interpreter/manual.ml. These implementations call the validation functions of the reference interpreter. Further efforts may be needed to make this validation independent.
Some numeric functions, such as $fadd_, are declared but not defined in the specification. For these functions, SpecTec's interpreter currently relies on the implementation from the reference interpreter. Our goal is to eventually implement these numeric functions directly within the specification.
TODO