symbolic tests reviews

test/sym/add.t

@@ -6,10 +6,28 @@ add binop:
       (symbol_0 (i32 1073741825))
       (symbol_1 (i32 1073741824)))
   Reached problem!
+  [1]
   $ dune exec owi -- sym add_i64.wat
   Assert failure: (i64.le (i64 0) (i64.add symbol_0 symbol_1))
   Model:
     (model
       (symbol_0 (i64 4611686018427387905))
       (symbol_1 (i64 4611686018427387904)))
   Reached problem!
+  [1]
+  $ dune exec owi -- sym add_f32.wat
+  Assert failure: (f32.eq (f32.add symbol_0 symbol_1) (f32.add symbol_0 symbol_1))
+  Model:
+    (model
+      (symbol_0 (f32 nan))
+      (symbol_1 (f32 10.)))
+  Reached problem!
+  [1]
+  $ dune exec owi -- sym add_f64.wat
+  Assert failure: (f64.eq (f64.add symbol_0 symbol_1) (f64.add symbol_0 symbol_1))
+  Model:
+    (model
+      (symbol_0 (f64 neg_infinity))
+      (symbol_1 (f64 infinity)))
+  Reached problem!
+  [1]

test/sym/add_f32.wat

@@ -0,0 +1,18 @@
+(module
+  (import "symbolic" "f32_symbol" (func $f32_symbol (result f32)))
+  (import "symbolic" "assert" (func $assert_i32 (param i32)))
+
+  (func $start
+    (local $x f32)
+    (local $y f32)
+
+    (local.set $x (call $f32_symbol))
+    (local.set $y (call $f32_symbol))
+
+    (call $assert_i32 (f32.eq ;; False when x+y is NaN (because NaN != Nan)
+      (f32.add (local.get $x) (local.get $y))
+      (f32.add (local.get $x) (local.get $y))))
+  )
+
+  (start $start)
+)

test/sym/add_f64.wat

@@ -0,0 +1,18 @@
+(module
+  (import "symbolic" "f64_symbol" (func $f64_symbol (result f64)))
+  (import "symbolic" "assert" (func $assert_i32 (param i32)))
+
+  (func $start
+    (local $x f64)
+    (local $y f64)
+
+    (local.set $x (call $f64_symbol))
+    (local.set $y (call $f64_symbol))
+
+    (call $assert_i32 (f64.eq ;; False when x+y is NaN (because NaN != Nan)
+      (f64.add (local.get $x) (local.get $y))
+      (f64.add (local.get $x) (local.get $y))))
+  )
+
+  (start $start)
+)

test/sym/add_i32.wat

@@ -10,9 +10,9 @@
     (local.set $x (call $i32_symbol))
     (local.set $y (call $i32_symbol))
 
-    (call $assume_positive_i32 (local.get $x))  ;; x >= 0
-    (call $assume_positive_i32 (local.get $y))  ;; y >= 0
-    (call $assert_i32                           ;; x + y >= 0 (== 0 =< x + y)
+    (call $assume_positive_i32 (local.get $x))  ;; 0 <= x
+    (call $assume_positive_i32 (local.get $y))  ;; 0 <= y
+    (call $assert_i32                           ;; 0 <= x + y (false when overflow)
       (i32.le_s (i32.const 0) (i32.add (local.get $x) (local.get $y))))
   )
 

test/sym/add_i64.wat

@@ -11,10 +11,10 @@
     (local.set $y (call $i64_symbol))
 
     (call $assume_i32
-      (i64.ge_s (local.get $x) (i64.const 0)))    ;; x >= 0
+      (i64.le_s (i64.const 0) (local.get $x)))    ;; 0 <= x
     (call $assume_i32
-      (i64.ge_s (local.get $y) (i64.const 0)))    ;; y >= 0
-    (call $assert_i32                             ;; x + y >= 0 (== 0 =< x + y)
+      (i64.le_s (i64.const 0) (local.get $y)))    ;; 0 <= y
+    (call $assert_i32                             ;; 0 <= x + y (false when overflow)
       (i64.le_s (i64.const 0) (i64.add (local.get $x) (local.get $y))))
   )
 

test/sym/div.t

@@ -6,17 +6,28 @@ div binop:
       (symbol_0 (i32 -2147483648))
       (symbol_1 (i32 -1)))
   Reached problem!
+  [1]
   $ dune exec owi -- sym div_i64.wat
   Trap: integer overflow
   Model:
     (model
       (symbol_0 (i64 -9223372036854775808))
       (symbol_1 (i64 -1)))
   Reached problem!
+  [1]
   $ dune exec owi -- sym div_f32.wat
-  Assert failure: (f32.eq (f32.div (f32 1.) symbol_0) (f32.div (f32 1.) symbol_1))
+  Assert failure: (f32.eq (f32.div symbol_0 symbol_1) (f32.div symbol_0 symbol_1))
   Model:
     (model
-      (symbol_0 (f32 0.))
-      (symbol_1 (f32 -0.)))
+      (symbol_0 (f32 5.74330863654e-39))
+      (symbol_1 (f32 nan)))
   Reached problem!
+  [1]
+  $ dune exec owi -- sym div_f64.wat
+  Assert failure: (f64.eq (f64.div symbol_0 symbol_1) (f64.div symbol_0 symbol_1))
+  Model:
+    (model
+      (symbol_0 (f64 1.0061050058))
+      (symbol_1 (f64 nan)))
+  Reached problem!
+  [1]

test/sym/div_f32.wat

@@ -1,6 +1,5 @@
 (module
   (import "symbolic" "f32_symbol" (func $f32_symbol (result f32)))
-  (import "symbolic" "assume" (func $assume_i32 (param i32)))
   (import "symbolic" "assert" (func $assert_i32 (param i32)))
 
   (func $start
@@ -10,12 +9,9 @@
     (local.set $x (call $f32_symbol))
     (local.set $y (call $f32_symbol))
 
-    ;; x = y
-    (call $assume_i32 (f32.eq (local.get $x) (local.get $y)))
-    ;; 1/x = 1/y
-    (call $assert_i32 (f32.eq
-      (f32.div (f32.const 1) (local.get $x))
-      (f32.div (f32.const 1) (local.get $y))))
+    (call $assert_i32 (f32.eq   ;; False when x/y is NaN (because NaN != Nan)
+      (f32.div (local.get $x) (local.get $y))
+      (f32.div (local.get $x) (local.get $y))))
   )
 
   (start $start)

test/sym/div_f64.wat

@@ -0,0 +1,18 @@
+(module
+  (import "symbolic" "f64_symbol" (func $f64_symbol (result f64)))
+  (import "symbolic" "assert" (func $assert_i32 (param i32)))
+
+  (func $start
+    (local $x f64)
+    (local $y f64)
+
+    (local.set $x (call $f64_symbol))
+    (local.set $y (call $f64_symbol))
+
+    (call $assert_i32 (f64.eq   ;; False when x/y is NaN (because NaN != Nan)
+      (f64.div (local.get $x) (local.get $y))
+      (f64.div (local.get $x) (local.get $y))))
+  )
+
+  (start $start)
+)

test/sym/dune

@@ -3,6 +3,8 @@
   %{bin:owi}
   add_i32.wat
   add_i64.wat
+  add_f32.wat
+  add_f64.wat
   assume.wat
   ; binop_i32.wat
   ; binop_i32-2.wat
@@ -13,18 +15,23 @@
   div_i32.wat
   div_i64.wat
   div_f32.wat
+  div_f64.wat
   global.wat
   grow.wat
   memory.wat
   mini_test.wat
   mul_i32.wat
   mul_i64.wat
+  mul_f32.wat
+  mul_f64.wat
   store.wat
   sub_i32.wat
   sub_i64.wat
+  sub_f32.wat
+  sub_f64.wat
   table.wat
   ; unop_i32.wat
   ; unop_i64.wat
   ; unop_f32.wat
   ; unop_f64.wat
- ))
+  ))

test/sym/global.t

@@ -1,25 +1,3 @@
 global vars stuff:
   $ dune exec owi -- sym global.wat --no-stop-at-failure
-  Trap: unreachable
-  Model:
-    (model
-      (symbol_0 (i32 0)))
-  Trap: unreachable
-  Model:
-    (model
-      (symbol_0 (i32 1))
-      (symbol_1 (i64 0)))
-  Trap: unreachable
-  Model:
-    (model
-      (symbol_0 (i32 1))
-      (symbol_1 (i64 1))
-      (symbol_2 (f32 -0.)))
-  Trap: unreachable
-  Model:
-    (model
-      (symbol_0 (i32 1))
-      (symbol_1 (i64 1))
-      (symbol_2 (f32 -2.35098926216e-38))
-      (symbol_3 (f64 -0.)))
-  Reached 4 problems!
+  All OK

test/sym/global.wat

@@ -3,46 +3,47 @@
   (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)))
+  (import "symbolic" "assume" (func $assume_i32 (param i32)))
+  (import "symbolic" "assert" (func $assert_i32 (param i32)))
 
-  (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))
-
-  (func $i32 (param $a i32)
-    (if (i32.eqz (local.get $a))
-      (then unreachable))
-  )
-
-  (func $i64 (param $a i64)
-    (if (i64.eqz (local.get $a))
-      (then unreachable))
-  )
-
-  (func $f32 (param $a f32)
-    (if (f32.eq (local.get $a) (f32.const 0))
-      (then unreachable))
-  )
-
-  (func $f64 (param $a f64)
-    (if (f64.eq (local.get $a) (f64.const 0))
-      (then unreachable))
-  )
+  (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
-    ;; 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
+    ;; Objective: storing something in a global and then reading it should give the same value
+
+    (local $x i32)
+    (local $y i64)
+    (local $i f32)
+    (local $j f64)
+
+    (local.set $x (call $i32_symbol))
+    (local.set $y (call $i64_symbol))
+    (local.set $i (call $f32_symbol))
+    (local.set $j (call $f64_symbol))
+
+    (global.set $x (local.get $x))
+    (global.set $y (local.get $y))
+    (call $assert_i32 (i32.eq (global.get $x) (local.get $x)))
+    (call $assert_i32 (i64.eq (global.get $y) (local.get $y)))
+
+    ;; In float numbers context, avoid Nan
+
+    (call $assume_i32   ;; 0 < i < 42
+      (i32.and
+        (f32.gt (local.get $i) (f32.const 0))
+        (f32.lt (local.get $i) (f32.const 42))))
+    (global.set $i (local.get $i))
+    (call $assert_i32 (f32.eq (global.get $i) (local.get $i)))
+
+    (call $assume_i32   ;; 0 < j < 42
+      (i32.and
+        (f64.gt (local.get $j) (f64.const 0))
+        (f64.lt (local.get $j) (f64.const 42))))
+    (global.set $j (local.get $j))
+    (call $assert_i32 (f64.eq (global.get $j) (local.get $j)))
   )
 
   (start $start)