Baby WASM interpreter, UTF8 specification

Author: karthiknukala

pvs2c-demos/Makefile

@@ -1,4 +1,4 @@
-.PHONY: run-aes run-hmac run-sha256 run-utf8_decoder run-crypto ci-pvs2c-tests ci clean-aes clean-hmac clean-sha256 clean-utf8_decoder clean
+.PHONY: run-aes run-hmac run-sha256 run-utf8_decoder run-bytecode-wasm run-crypto ci-pvs2c-tests ci clean-aes clean-hmac clean-sha256 clean-utf8_decoder clean-bytecode-wasm clean
 
 run-aes:
 	$(MAKE) -C aes run
@@ -12,6 +12,9 @@ run-sha256:
 run-utf8_decoder:
 	$(MAKE) -C utf8_decoder run
 
+run-bytecode-wasm:
+	$(MAKE) -C bytecode/wasm run
+
 run-crypto: run-aes run-hmac run-sha256
 
 ci-pvs2c-tests:
@@ -21,6 +24,7 @@ ci:
 	python3 ../scripts/ci/run_pvs2c_tests.py --repo-root .. --demo-root pvs2c-demos
 	$(MAKE) run-crypto
 	$(MAKE) run-utf8_decoder
+	$(MAKE) run-bytecode-wasm
 
 clean-aes:
 	$(MAKE) -C aes clean
@@ -34,4 +38,7 @@ clean-sha256:
 clean-utf8_decoder:
 	$(MAKE) -C utf8_decoder clean
 
-clean: clean-aes clean-hmac clean-sha256 clean-utf8_decoder
+clean-bytecode-wasm:
+	$(MAKE) -C bytecode/wasm clean
+
+clean: clean-aes clean-hmac clean-sha256 clean-utf8_decoder clean-bytecode-wasm

pvs2c-demos/bytecode/wasm/README.md

@@ -0,0 +1,92 @@
+# Wasm i32 Bytecode Interpreter PVS2C Demo
+
+This demo implements a small WebAssembly Core interpreter in executable PVS and
+runs the generated C against real Wasm function-body bytecode.
+
+The supported subset is intentionally small:
+
+- i32 values only
+- one-byte immediates
+- i32 locals
+- empty-result `block` and `loop`
+- `br`, `br_if`, `return`, `end`
+- `local.get`, `local.set`, `local.tee`
+- `i32.const`, `i32.eqz`, `i32.eq`, `i32.ne`, `i32.add`, `i32.sub`, `i32.mul`
+
+The PVS model uses predicate subtyping for the stack/control discipline:
+
+- `push` only accepts stacks whose height is below `max_stack`
+- `pop` only accepts nonempty stacks, and its result type records that the
+  returned stack height is one smaller
+- machine states are indexed by the byte string being executed, so the program
+  counter type is bounded by the current body length
+- control frames track `block`/`loop` bodies and matching `end` offsets
+- branch depth selection is checked against the current control depth
+- execution is total by construction through a fuel-bound runner
+
+Run the demo with:
+
+```sh
+make -C pvs2c-demos/bytecode/wasm run
+```
+
+The checked-in examples are:
+
+- `add.wat`: `add(40, 2) = 42`
+- `affine.wat`: `affine(5, 9) = 5 * 7 + 9 * 3 + 11 = 73`
+- `factorial.wat`: an iterative loop using `block`, `loop`, `br_if`, and `br`
+
+Each `.body.hex` file is the WebAssembly function-body payload: the local
+declaration vector followed by instruction bytes.  That is the payload inside a
+standard `.wasm` code-section function body after the body-size LEB128 wrapper.
+
+To rebuild body hex from WAT, install WABT and run:
+
+```sh
+make -C pvs2c-demos/bytecode/wasm compile-examples
+```
+
+Or manually:
+
+```sh
+wat2wasm examples/factorial.wat -o build/factorial.wasm
+python3 tools/extract_wasm_body.py build/factorial.wasm --body 0
+```
+
+The `examples/*.c` files are equivalent source examples.  Toolchains vary in
+which opcodes they emit, so the demo executes the WAT-derived bytecode by
+default; C-compiled modules can be inspected with `tools/extract_wasm_body.py`
+when the emitted body stays inside this demo's subset.
+
+## Running Your Own Body Hex
+
+The current C harness is table-driven.  To run another extracted function body,
+put the hex payload in `examples/` and add a row to the `cases[]` table in
+`driver.c`:
+
+```c
+{"my_example", "examples/my_example.body.hex", 2, {10, 20}, 128, 30},
+```
+
+The fields are:
+
+- `name`: label printed in the PASS/FAIL output
+- `path`: `.body.hex` file containing the extracted Wasm function-body payload
+- `arity`: number of i32 arguments to pass, currently `0`, `1`, or `2`
+- `args`: argument values; in the example, `arg0 = 10` and `arg1 = 20`
+- `fuel`: maximum interpreter steps before the runner returns `fuel_status`
+- `expected`: expected i32 return value
+
+That row runs `my_example(10, 20)` with at most `128` interpreter steps and
+expects the function to return `30`.  For arity `2`, the harness calls the
+generated PVS2C entry point:
+
+```c
+wasm_i32__invoke2(pvs_body, 128, 10, 20)
+```
+
+After editing the table, run:
+
+```sh
+make -C pvs2c-demos/bytecode/wasm run PVS_LOCATION=/path/to/PVS
+```

pvs2c-demos/bytecode/wasm/driver.c

@@ -0,0 +1,154 @@
+#include "wasm_i32_c.h"
+#include "../../cavp_driver.h"
+
+#include <errno.h>
+
+typedef struct {
+  const char *name;
+  const char *path;
+  unsigned arity;
+  uint32_t args[2];
+  uint32_t fuel;
+  uint32_t expected;
+} wasm_case_t;
+
+static int hex_value(int ch) {
+  if (ch >= '0' && ch <= '9') {
+    return ch - '0';
+  }
+  if (ch >= 'a' && ch <= 'f') {
+    return ch - 'a' + 10;
+  }
+  if (ch >= 'A' && ch <= 'F') {
+    return ch - 'A' + 10;
+  }
+  return -1;
+}
+
+static uint8_t *read_hex_body(const char *path, uint32_t *length) {
+  FILE *file = fopen(path, "r");
+  if (file == NULL) {
+    fprintf(stderr, "FAIL open %s: %s\n", path, strerror(errno));
+    exit(2);
+  }
+
+  size_t capacity = 64;
+  size_t used = 0;
+  uint8_t *bytes = malloc(capacity);
+  if (bytes == NULL) {
+    fprintf(stderr, "FAIL allocate hex buffer\n");
+    exit(2);
+  }
+
+  int high = -1;
+  int in_comment = 0;
+  for (;;) {
+    int ch = fgetc(file);
+    if (ch == EOF) {
+      break;
+    }
+    if (in_comment) {
+      if (ch == '\n') {
+        in_comment = 0;
+      }
+      continue;
+    }
+    if (ch == '#') {
+      in_comment = 1;
+      continue;
+    }
+    if (isspace((unsigned char)ch)) {
+      continue;
+    }
+
+    int nibble = hex_value(ch);
+    if (nibble < 0) {
+      fprintf(stderr, "FAIL invalid hex character %c in %s\n", ch, path);
+      exit(2);
+    }
+    if (high < 0) {
+      high = nibble;
+      continue;
+    }
+    if (used == capacity) {
+      capacity *= 2;
+      uint8_t *grown = realloc(bytes, capacity);
+      if (grown == NULL) {
+        fprintf(stderr, "FAIL grow hex buffer\n");
+        exit(2);
+      }
+      bytes = grown;
+    }
+    bytes[used++] = (uint8_t)((high << 4) | nibble);
+    high = -1;
+  }
+  fclose(file);
+
+  if (high >= 0) {
+    fprintf(stderr, "FAIL odd number of hex digits in %s\n", path);
+    exit(2);
+  }
+  if (used > UINT32_MAX) {
+    fprintf(stderr, "FAIL %s too large for PVS bytestring\n", path);
+    exit(2);
+  }
+  *length = (uint32_t)used;
+  return bytes;
+}
+
+static wasm_i32__exec_result_t run_case_body(const wasm_case_t *test,
+                                             const uint8_t *body,
+                                             uint32_t length) {
+  bytestrings__bytestring_t pvs_body = cavp_make_bytestring(body, length);
+  if (test->arity == 1) {
+    return wasm_i32__invoke1(pvs_body, test->fuel, test->args[0]);
+  }
+  if (test->arity == 2) {
+    return wasm_i32__invoke2(pvs_body, test->fuel, test->args[0], test->args[1]);
+  }
+  return wasm_i32__invoke0(pvs_body, test->fuel);
+}
+
+static int run_case(const wasm_case_t *test) {
+  uint32_t length = 0;
+  uint8_t *body = read_hex_body(test->path, &length);
+  wasm_i32__exec_result_t result = run_case_body(test, body, length);
+  free(body);
+
+  uint8_t halt = wasm_i32__halt_status();
+  int ok = result->status == halt && result->value == test->expected;
+  printf("%s wasm %s", ok ? "PASS" : "FAIL", test->name);
+  if (test->arity == 1) {
+    printf("(%u)", test->args[0]);
+  } else if (test->arity == 2) {
+    printf("(%u, %u)", test->args[0], test->args[1]);
+  } else {
+    printf("()");
+  }
+  printf(" => %u\n", result->value);
+  if (!ok) {
+    printf("  expected status=%u value=%u\n", halt, test->expected);
+    printf("  actual   status=%u value=%u pc=%u stack=%u\n",
+           result->status,
+           result->value,
+           result->final_pc,
+           result->final_stack_height);
+  }
+  release_wasm_i32__exec_result(result);
+  return ok ? 0 : 1;
+}
+
+int main(void) {
+  static const wasm_case_t cases[] = {
+      {"add", "examples/add.body.hex", 2, {40, 2}, 32, 42},
+      {"affine", "examples/affine.body.hex", 2, {5, 9}, 64, 73},
+      {"factorial", "examples/factorial.body.hex", 1, {0, 0}, 128, 1},
+      {"factorial", "examples/factorial.body.hex", 1, {5, 0}, 512, 120},
+  };
+
+  int failures = 0;
+  for (size_t i = 0; i < sizeof(cases) / sizeof(cases[0]); i++) {
+    failures += run_case(&cases[i]);
+  }
+  return failures == 0 ? 0 : 1;
+}

pvs2c-demos/bytecode/wasm/examples/add.body.hex

@@ -0,0 +1,4 @@
+# WebAssembly function body payload for examples/add.wat.
+# Local declaration vector: 00
+# Code: local.get 0; local.get 1; i32.add; end
+00 20 00 20 01 6A 0B

pvs2c-demos/bytecode/wasm/examples/add.c

@@ -0,0 +1,4 @@
+__attribute__((export_name("add")))
+int add(int a, int b) {
+  return a + b;
+}

pvs2c-demos/bytecode/wasm/examples/add.wat

@@ -0,0 +1,5 @@
+(module
+  (func $add (export "add") (param i32 i32) (result i32)
+    local.get 0
+    local.get 1
+    i32.add))

pvs2c-demos/bytecode/wasm/examples/affine.body.hex

@@ -0,0 +1,3 @@
+# WebAssembly function body payload for examples/affine.wat.
+# Computes x * 7 + y * 3 + 11.
+00 20 00 41 07 6C 20 01 41 03 6C 6A 41 0B 6A 0B

pvs2c-demos/bytecode/wasm/examples/affine.c

@@ -0,0 +1,4 @@
+__attribute__((export_name("affine")))
+int affine(int x, int y) {
+  return x * 7 + y * 3 + 11;
+}

pvs2c-demos/bytecode/wasm/examples/affine.wat

@@ -0,0 +1,11 @@
+(module
+  (func $affine (export "affine") (param i32 i32) (result i32)
+    local.get 0
+    i32.const 7
+    i32.mul
+    local.get 1
+    i32.const 3
+    i32.mul
+    i32.add
+    i32.const 11
+    i32.add))

pvs2c-demos/bytecode/wasm/examples/factorial.body.hex

@@ -0,0 +1,23 @@
+# WebAssembly function body payload for examples/factorial.wat.
+# Local declaration vector: one group, one i32 local.
+01 01 7F
+41 01
+21 01
+02 40
+03 40
+20 00
+45
+0D 01
+20 01
+20 00
+6C
+21 01
+20 00
+41 01
+6B
+21 00
+0C 00
+0B
+0B
+20 01
+0B