refacto 2 global sym tests

OCamlPro · Jan 25, 2024 · cd7142b · cd7142b
1 parent eb5f4bf
commit cd7142b
Show file tree

Hide file tree

Showing 3 changed files with 36 additions and 57 deletions.
diff --git a/test/sym/dune b/test/sym/dune
@@ -12,7 +12,7 @@
   ; binop_f64.wat
   div_i32.wat
   div_i64.wat
-  ; global.wat
+  global.wat
   ; grow.wat
   ; memory.wat
   mini_test.wat

diff --git a/test/sym/global.t b/test/sym/global.t
@@ -3,33 +3,23 @@ global vars stuff:
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 0))
-      (symbol_1 (i32 1)))
+      (symbol_0 (i32 0)))
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 0))
-      (symbol_1 (i32 -2147483647))
-      (symbol_2 (i64 1))
-      (symbol_3 (i64 0)))
+      (symbol_0 (i32 1))
+      (symbol_1 (i64 0)))
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 0))
-      (symbol_1 (i32 -2147483647))
-      (symbol_2 (i64 -9223372036854775807))
-      (symbol_3 (i64 0))
-      (symbol_4 (f32 -2.03125))
-      (symbol_5 (f32 1.19386159018e-38)))
+      (symbol_0 (i32 1))
+      (symbol_1 (i64 1))
+      (symbol_2 (f32 -0.)))
   Trap: unreachable
   Model:
     (model
-      (symbol_0 (i32 0))
-      (symbol_1 (i32 -2147483647))
-      (symbol_2 (i64 -9223372036854775807))
-      (symbol_3 (i64 0))
-      (symbol_4 (f32 2.12513160706))
-      (symbol_5 (f32 1.24904037968e-38))
-      (symbol_6 (f64 2.98443202363e-154))
-      (symbol_7 (f64 -3.69206570797e+19)))
+      (symbol_0 (i32 1))
+      (symbol_1 (i64 1))
+      (symbol_2 (f32 -2.35098926216e-38))
+      (symbol_3 (f64 -0.)))
   Reached 4 problems!
diff --git a/test/sym/global.wat b/test/sym/global.wat
@@ -4,56 +4,45 @@
   (import "symbolic" "f32_symbol" (func $f32_symbol (result f32)))
   (import "symbolic" "f64_symbol" (func $f64_symbol (result f64)))
 
-  (global $x1 (mut i32) (i32.const 0))
-  (global $x2 (mut i32) (i32.const 0))
+  (global $w (mut i32) (i32.const 0))
+  (global $x (mut i64) (i64.const 0))
+  (global $y (mut f32) (f32.const 0))
+  (global $z (mut f64) (f64.const 0))
 
-  (global $y1 (mut i64) (i64.const 0))
-  (global $y2 (mut i64) (i64.const 0))
-
-  (global $i1 (mut f32) (f32.const 0))
-  (global $i2 (mut f32) (f32.const 0))
-
-  (global $j1 (mut f64) (f64.const 0))
-  (global $j2 (mut f64) (f64.const 0))
-
-  (func $i32 (param $x i32) (param $y i32)
-    (if (i32.lt_s (local.get $x) (local.get $y))
+  (func $i32 (param $a i32)
+    (if (i32.eqz (local.get $a))
       (then unreachable))
   )
 
-  (func $i64 (param $x i64) (param $y i64)
-    (if (i64.gt_s (local.get $x) (local.get $y))
+  (func $i64 (param $a i64)
+    (if (i64.eqz (local.get $a))
       (then unreachable))
   )
 
-  (func $f32 (param $x f32) (param $y f32)
-    (if (f32.lt (local.get $x) (local.get $y))
+  (func $f32 (param $a f32)
+    (if (f32.eq (local.get $a) (f32.const 0))
       (then unreachable))
   )
 
-  (func $f64 (param $x f64) (param $y f64)
-    (if (f64.gt (local.get $x) (local.get $y))
+  (func $f64 (param $a f64)
+    (if (f64.eq (local.get $a) (f64.const 0))
       (then unreachable))
   )
 
   (func $start
-    (global.set $x1 (call $i32_symbol))
-    (global.set $x2 (call $i32_symbol))
-    (call $i32 (global.get $x1) (global.get $x2))
-    ;; (call $i32 (global.get $x1) (i32.const 0))
-    ;; (call $i32 (i32.const 0) (global.get $x2))
-
-    (global.set $y1 (call $i64_symbol))
-    (global.set $y2 (call $i64_symbol))
-    (call $i64 (global.get $y1) (global.get $y2))
-
-    (global.set $i1 (call $f32_symbol))
-    (global.set $i2 (call $f32_symbol))
-    (call $f32 (global.get $i1) (global.get $i2))
-
-    (global.set $j1 (call $f64_symbol))
-    (global.set $j2 (call $f64_symbol))
-    (call $f64 (global.get $j1) (global.get $j2))
+    ;; objective: check that interactions with globals are ok
+
+    (global.set $w (call $i32_symbol))
+    (global.set $x (call $i64_symbol))
+    (global.set $y (call $f32_symbol))
+    (global.set $z (call $f64_symbol))
+
+    ;; 'unreachable' when argument is equal to 0
+    ;; in global.t, only one model symbol is equal to 0
+    (call $i32 (global.get $w))
+    (call $i64 (global.get $x)) ;; (symbol_0) w != 0
+    (call $f32 (global.get $y)) ;; (symbol_0) w != 0 AND (symbol_1) x != 0
+    (call $f64 (global.get $z)) ;; (symbol_0) w != 0 AND (symbol_1) x != 0 AND (symbol_2) y != 0
   )
 
   (start $start)