add symbolic binop tests

OCamlPro · Jan 9, 2024 · ac117e4 · ac117e4
1 parent 842bffa
commit ac117e4
Show file tree

Hide file tree

Showing 5 changed files with 42 additions and 2 deletions.
diff --git a/test/sym/binop.t b/test/sym/binop.t
@@ -46,6 +46,9 @@ binop i64:
   Reached 5 problems!
 binop f32:
   $ dune exec owi -- sym binop_f32.wast --no-stop-at-failure
+  owi: internal error, uncaught exception:
+       File "src/symbolic_value.ml", line 436, characters 24-30: Assertion failed
+
   Trap: unreachable
   Model:
     (model
@@ -62,9 +65,12 @@ binop f32:
   Model:
     (model
       (symbol_0 f32 (f32 -0.000000)))
-  Reached 4 problems!
+  [125]
 binop f64:
   $ dune exec owi -- sym binop_f64.wast --no-stop-at-failure
+  owi: internal error, uncaught exception:
+       File "src/symbolic_value.ml", line 508, characters 24-30: Assertion failed
+
   Trap: unreachable
   Model:
     (model
@@ -81,4 +87,4 @@ binop f64:
   Model:
     (model
       (symbol_0 f64 (f64 -0.000000)))
-  Reached 4 problems!
+  [125]
diff --git a/test/sym/binop_f32.wast b/test/sym/binop_f32.wast
@@ -16,6 +16,15 @@
     (if (then unreachable))
 
     (f32.eq (f32.div (local.get $x) (f32.const 42)) (f32.const 0))
+    (if (then unreachable))
+
+    (f32.eq (f32.min (local.get $x) (f32.const 42)) (f32.const 0))
+    (if (then unreachable))
+
+    (f32.eq (f32.max (local.get $x) (f32.const 42)) (f32.const 0))
+    (if (then unreachable))
+
+    (f32.eq (f32.copysign (local.get $x) (f32.const 42)) (f32.const 0))
     (if (then unreachable)))
 
   (start $start)

diff --git a/test/sym/binop_f64.wast b/test/sym/binop_f64.wast
@@ -16,6 +16,15 @@
     (if (then unreachable))
 
     (f64.eq (f64.div (local.get $x) (f64.const 42)) (f64.const 0))
+    (if (then unreachable))
+
+    (f64.eq (f64.min (local.get $x) (f64.const 42)) (f64.const 0))
+    (if (then unreachable))
+
+    (f64.eq (f64.max (local.get $x) (f64.const 42)) (f64.const 0))
+    (if (then unreachable))
+
+    (f64.eq (f64.copysign (local.get $x) (f64.const 42)) (f64.const 0))
     (if (then unreachable)))
 
   (start $start)

diff --git a/test/sym/binop_i32.wast b/test/sym/binop_i32.wast
@@ -22,8 +22,16 @@
     i32.eqz
     (if (then unreachable))
 
+    (i32.rem_u (i32.const 42) (local.get $x))
+    i32.eqz
+    (if (then unreachable))
+
     (i32.div_s (local.get $x) (i32.const 42))
     i32.eqz
+    (if (then unreachable))
+
+    (i32.rem_s (i32.const 42) (local.get $x))
+    i32.eqz
     (if (then unreachable)))
 
   (start $start)

diff --git a/test/sym/binop_i64.wast b/test/sym/binop_i64.wast
@@ -22,8 +22,16 @@
     i64.eqz
     (if (then unreachable))
 
+    (i64.rem_u (i64.const 42) (local.get $x))
+    i64.eqz
+    (if (then unreachable))
+
     (i64.div_s (local.get $x) (i64.const 42))
     i64.eqz
+    (if (then unreachable))
+
+    (i64.rem_s (i64.const 42) (local.get $x))
+    i64.eqz
     (if (then unreachable)))
 
   (start $start)