add global and memory sym test

OCamlPro · Jan 16, 2024 · 24740ac · 24740ac
1 parent d62cfec
commit 24740ac
Show file tree

Hide file tree

Showing 5 changed files with 266 additions and 0 deletions.
diff --git a/test/sym/dune b/test/sym/dune
@@ -7,6 +7,8 @@
   binop_i64.wast
   binop_f32.wast
   binop_f64.wast
+  global.wast
+  memory.wast
   unop_i32.wast
   unop_i64.wast
   unop_f32.wast

diff --git a/test/sym/global.t b/test/sym/global.t
@@ -0,0 +1,25 @@
+global vars stuff:
+  $ dune exec owi -- sym global.wast --no-stop-at-failure
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 6)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 -2147483642))
+      (symbol_1 i64 (i64 0)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 -2147483642))
+      (symbol_1 i64 (i64 4611686018427387904))
+      (symbol_2 f32 (f32 14.000002)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 -2147483642))
+      (symbol_1 i64 (i64 4611686018427387904))
+      (symbol_2 f32 (f32 0.000000))
+      (symbol_3 f64 (f64 0.000000)))
+  Reached 4 problems!
diff --git a/test/sym/global.wast b/test/sym/global.wast
@@ -0,0 +1,31 @@
+(module
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+  (import "symbolic" "i64_symbol" (func $i64_symbol (result i64)))
+  (import "symbolic" "f32_symbol" (func $f32_symbol (result f32)))
+  (import "symbolic" "f64_symbol" (func $f64_symbol (result f64)))
+
+  (global $x (mut i32) (i32.const 0))
+  (global $y (mut i64) (i64.const 0))
+  (global $i (mut f32) (f32.const 0))
+  (global $j (mut f64) (f64.const 0))
+
+  (func $start
+    (global.set $x (call $i32_symbol))
+    (global.set $y (call $i64_symbol))
+    (global.set $i (call $f32_symbol))
+    (global.set $j (call $f64_symbol))
+
+    (if (i32.lt_s (i32.const 5) (global.get $x))
+      (then unreachable))
+
+    (if (i64.gt_s (i64.const 5) (global.get $y))
+      (then unreachable))
+
+    (if (f32.lt (f32.const 5) (global.get $i))
+      (then unreachable))
+
+    (if (f64.gt (f64.const 5) (global.get $j))
+      (then unreachable)))
+
+  (start $start)
+)
diff --git a/test/sym/memory.t b/test/sym/memory.t
@@ -0,0 +1,84 @@
+memory stuff:
+  $ dune exec owi -- sym memory.wast --no-stop-at-failure
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 6)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 134)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 0))
+      (symbol_1 i32 (i32 8)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 0))
+      (symbol_1 i32 (i32 32774)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 0))
+      (symbol_2 i32 (i32 6))
+      (symbol_1 i32 (i32 0)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 0))
+      (symbol_2 i32 (i32 -2147483642))
+      (symbol_1 i32 (i32 0))
+      (symbol_3 i64 (i64 0)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_4 i64 (i64 0))
+      (symbol_0 i32 (i32 0))
+      (symbol_2 i32 (i32 -2147483642))
+      (symbol_1 i32 (i32 0))
+      (symbol_3 i64 (i64 64)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_4 i64 (i64 16384))
+      (symbol_0 i32 (i32 0))
+      (symbol_2 i32 (i32 -2147483642))
+      (symbol_1 i32 (i32 0))
+      (symbol_5 i64 (i64 0))
+      (symbol_3 i64 (i64 64)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_4 i64 (i64 16384))
+      (symbol_0 i32 (i32 0))
+      (symbol_2 i32 (i32 -2147483642))
+      (symbol_1 i32 (i32 0))
+      (symbol_6 i64 (i64 0))
+      (symbol_5 i64 (i64 1073741824))
+      (symbol_3 i64 (i64 64)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_4 i64 (i64 16384))
+      (symbol_0 i32 (i32 0))
+      (symbol_2 i32 (i32 -2147483642))
+      (symbol_1 i32 (i32 0))
+      (symbol_6 i64 (i64 4611686018427387904))
+      (symbol_7 f32 (f32 12.000000))
+      (symbol_5 i64 (i64 1073741824))
+      (symbol_3 i64 (i64 64)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_4 i64 (i64 16384))
+      (symbol_0 i32 (i32 0))
+      (symbol_2 i32 (i32 -2147483642))
+      (symbol_1 i32 (i32 0))
+      (symbol_8 f64 (f64 0.000000))
+      (symbol_6 i64 (i64 4611686018427387904))
+      (symbol_7 f32 (f32 0.000000))
+      (symbol_5 i64 (i64 1073741824))
+      (symbol_3 i64 (i64 64)))
+  Reached 11 problems!
diff --git a/test/sym/memory.wast b/test/sym/memory.wast
@@ -0,0 +1,124 @@
+(module
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+  (import "symbolic" "i64_symbol" (func $i64_symbol (result i64)))
+  (import "symbolic" "f32_symbol" (func $f32_symbol (result f32)))
+  (import "symbolic" "f64_symbol" (func $f64_symbol (result f64)))
+
+  (memory 1)
+
+  (func $mem_set_i32_8 (param $idx i32) (param $val i32)
+    local.get $idx
+    local.get $val
+    i32.store8
+  )
+
+  (func $mem_set_i32_16 (param $idx i32) (param $val i32)
+    local.get $idx
+    local.get $val
+    i32.store16
+  )
+
+  (func $mem_set_i32 (param $idx i32) (param $val i32)
+    local.get $idx
+    local.get $val
+    i32.store
+  )
+
+  (func $mem_set_i64_8 (param $idx i32) (param $val i64)
+    local.get $idx
+    local.get $val
+    i64.store8
+  )
+
+  (func $mem_set_i64_16 (param $idx i32) (param $val i64)
+    local.get $idx
+    local.get $val
+    i64.store16
+  )
+
+  (func $mem_set_i64_32 (param $idx i32) (param $val i64)
+    local.get $idx
+    local.get $val
+    i64.store32
+  )
+
+  (func $mem_set_i64 (param $idx i32) (param $val i64)
+    local.get $idx
+    local.get $val
+    i64.store
+  )
+
+  (func $mem_set_f32 (param $idx i32) (param $val f32)
+    local.get $idx
+    local.get $val
+    f32.store
+  )
+
+  (func $mem_set_f64 (param $idx i32) (param $val f64)
+    local.get $idx
+    local.get $val
+    f64.store
+  )
+
+  (func $start
+    (call $mem_set_i32_8 (i32.const 0) (call $i32_symbol))
+    (call $mem_set_i32_16 (i32.const 4) (call $i32_symbol))
+    (call $mem_set_i32 (i32.const 8) (call $i32_symbol))
+
+    (call $mem_set_i64_8 (i32.const 12) (call $i64_symbol))
+    (call $mem_set_i64_16 (i32.const 20) (call $i64_symbol))
+    (call $mem_set_i64_32 (i32.const 28) (call $i64_symbol))
+    (call $mem_set_i64 (i32.const 36) (call $i64_symbol))
+
+    (call $mem_set_f32 (i32.const 44) (call $f32_symbol))
+
+    (call $mem_set_f64 (i32.const 48) (call $f64_symbol))
+
+
+    (if (i32.lt_s (i32.const 5) (i32.load8_s (i32.const 0)))
+      (then unreachable))
+
+    (if (i32.lt_u (i32.const 5) (i32.load8_u (i32.const 0)))
+      (then unreachable))
+
+    (if (i32.lt_s (i32.const 5) (i32.load16_s (i32.const 4)))
+      (then unreachable))
+
+    (if (i32.lt_u (i32.const 5) (i32.load16_u (i32.const 4)))
+      (then unreachable))
+
+    (if (i32.lt_s (i32.const 5) (i32.load (i32.const 8)))
+      (then unreachable))
+
+
+    (if (i64.gt_s (i64.const 5) (i64.load8_s (i32.const 12)))
+      (then unreachable))
+
+    (if (i64.gt_u (i64.const 5) (i64.load8_u (i32.const 12)))
+      (then unreachable))
+
+    (if (i64.gt_s (i64.const 5) (i64.load16_s (i32.const 20)))
+      (then unreachable))
+
+    (if (i64.gt_u (i64.const 5) (i64.load16_u (i32.const 20)))
+      (then unreachable))
+
+    (if (i64.gt_s (i64.const 5) (i64.load32_s (i32.const 28)))
+      (then unreachable))
+
+    (if (i64.gt_u (i64.const 5) (i64.load32_u (i32.const 28)))
+      (then unreachable))
+
+    (if (i64.gt_s (i64.const 5) (i64.load (i32.const 36)))
+      (then unreachable))
+
+
+    (if (f32.lt (f32.const 5) (f32.load (i32.const 44)))
+      (then unreachable))
+
+
+    (if (f64.gt (f64.const 5) (f64.load (i32.const 48)))
+      (then unreachable)))
+
+  (start $start)
+)