From 24740ac327475db71e6c4d3ef85c09aae0485f8e Mon Sep 17 00:00:00 2001 From: epatrizio Date: Tue, 16 Jan 2024 14:49:16 +0100 Subject: [PATCH] add global and memory sym test --- test/sym/dune | 2 + test/sym/global.t | 25 +++++++++ test/sym/global.wast | 31 +++++++++++ test/sym/memory.t | 84 +++++++++++++++++++++++++++++ test/sym/memory.wast | 124 +++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 266 insertions(+) create mode 100644 test/sym/global.t create mode 100644 test/sym/global.wast create mode 100644 test/sym/memory.t create mode 100644 test/sym/memory.wast diff --git a/test/sym/dune b/test/sym/dune index a45baac7b..5116f371e 100644 --- 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 new file mode 100644 index 000000000..8f247d50d --- /dev/null +++ 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 new file mode 100644 index 000000000..f85513abb --- /dev/null +++ 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 new file mode 100644 index 000000000..5bb456744 --- /dev/null +++ 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 new file mode 100644 index 000000000..428c59c68 --- /dev/null +++ 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) +)