From e3624bd61d44c632d348b78ca47dc20455a5801c Mon Sep 17 00:00:00 2001
From: epatrizio <epatrizio@mpns.fr>
Date: Tue, 9 Jan 2024 18:00:19 +0100
Subject: [PATCH] init symbolic unop tests

---
 test/sym/dune          |  4 ++++
 test/sym/unop.t        | 36 ++++++++++++++++++++++++++++++++++++
 test/sym/unop_f32.wast | 23 +++++++++++++++++++++++
 test/sym/unop_f64.wast | 17 +++++++++++++++++
 test/sym/unop_i32.wast | 26 ++++++++++++++++++++++++++
 test/sym/unop_i64.wast | 14 ++++++++++++++
 6 files changed, 120 insertions(+)
 create mode 100644 test/sym/unop.t
 create mode 100644 test/sym/unop_f32.wast
 create mode 100644 test/sym/unop_f64.wast
 create mode 100644 test/sym/unop_i32.wast
 create mode 100644 test/sym/unop_i64.wast

diff --git a/test/sym/dune b/test/sym/dune
index 4c760c758..a45baac7b 100644
--- a/test/sym/dune
+++ b/test/sym/dune
@@ -7,4 +7,8 @@
   binop_i64.wast
   binop_f32.wast
   binop_f64.wast
+  unop_i32.wast
+  unop_i64.wast
+  unop_f32.wast
+  unop_f64.wast
  ))
diff --git a/test/sym/unop.t b/test/sym/unop.t
new file mode 100644
index 000000000..f5d0d56f4
--- /dev/null
+++ b/test/sym/unop.t
@@ -0,0 +1,36 @@
+unop i32:
+  $ dune exec owi -- sym unop_i32.wast --no-stop-at-failure
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 0)))
+  Reached 1 problems!
+unop i64:
+  $ dune exec owi -- sym unop_i64.wast --no-stop-at-failure
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i64 (i64 0)))
+  Reached 1 problems!
+unop f32:
+  $ dune exec owi -- sym unop_f32.wast --no-stop-at-failure
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f32 (f32 42.000000)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f32 (f32 -0.000000)))
+  Reached 2 problems!
+unop f64:
+  $ dune exec owi -- sym unop_f64.wast --no-stop-at-failure
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f64 (f64 42.000000)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f64 (f64 -0.000000)))
+  Reached 2 problems!
diff --git a/test/sym/unop_f32.wast b/test/sym/unop_f32.wast
new file mode 100644
index 000000000..54b1867f8
--- /dev/null
+++ b/test/sym/unop_f32.wast
@@ -0,0 +1,23 @@
+(module
+  (import "symbolic" "f32_symbol" (func $f32_symbol (result f32)))
+
+  (func $start
+    (local $x f32)
+
+    (local.set $x (call $f32_symbol))
+
+    (f32.ge (f32.abs (local.get $x)) (f32.const 42))
+    (if (then unreachable))
+
+    (f32.le (f32.neg (local.get $x)) (f32.const 42))
+    (if (then unreachable))
+
+    ;; File "lib/z3_mappings.ml", line 408, characters 32-38: Assertion failed
+    ;; (f32.ge (f32.ceil (local.get $x)) (f32.const 42))
+    ;; (if (then unreachable))
+    ;; (f32.le (f32.floor (local.get $x)) (f32.const 42))
+    ;; (if (then unreachable))
+  )
+
+  (start $start)
+)
diff --git a/test/sym/unop_f64.wast b/test/sym/unop_f64.wast
new file mode 100644
index 000000000..bff0a7eec
--- /dev/null
+++ b/test/sym/unop_f64.wast
@@ -0,0 +1,17 @@
+(module
+  (import "symbolic" "f64_symbol" (func $f64_symbol (result f64)))
+
+  (func $start
+    (local $x f64)
+
+    (local.set $x (call $f64_symbol))
+
+    (f64.ge (f64.abs (local.get $x)) (f64.const 42))
+    (if (then unreachable))
+
+    (f64.le (f64.neg (local.get $x)) (f64.const 42))
+    (if (then unreachable))
+  )
+
+  (start $start)
+)
diff --git a/test/sym/unop_i32.wast b/test/sym/unop_i32.wast
new file mode 100644
index 000000000..55d65a6c1
--- /dev/null
+++ b/test/sym/unop_i32.wast
@@ -0,0 +1,26 @@
+(module
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+
+  (func $start
+    (local $x i32)
+
+    (local.set $x (call $i32_symbol))
+
+    (i32.eqz (local.get $x))
+    (if (then unreachable))
+
+    ;; Memo "lib/z3_mappings.ml" (to be implemented)
+    ;; Clz not supported yet
+    ;; (i32.ge_s (i32.const 2) (i32.clz (local.get $x)) )
+    ;; (if (then unreachable))
+    ;; Ctz: TODO
+    ;; (i32.ge_s (i32.const 2) (i32.ctz (local.get $x)) )
+    ;; (if (then unreachable))
+    ;; Popcnt: TODO
+    ;; (i32.ge_s (i32.const 2) (i32.popcnt (local.get $x)) )
+    ;; (if (then unreachable))
+
+  )
+
+  (start $start)
+)
diff --git a/test/sym/unop_i64.wast b/test/sym/unop_i64.wast
new file mode 100644
index 000000000..20e007ea9
--- /dev/null
+++ b/test/sym/unop_i64.wast
@@ -0,0 +1,14 @@
+(module
+  (import "symbolic" "i64_symbol" (func $i64_symbol (result i64)))
+
+  (func $start
+    (local $x i64)
+
+    (local.set $x (call $i64_symbol))
+
+    (i64.eqz (local.get $x))
+    (if (then unreachable))
+  )
+
+  (start $start)
+)