Test coverage improvement

test/sym/binop.t

@@ -37,6 +37,39 @@ binop i32:
     (model
       (symbol_0 i32 (i32 -46)))
   Reached 9 problems!
+binop i32 (2):
+  $ dune exec owi -- sym binop_i32-2.wast --no-stop-at-failure
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_2 i32 (i32 -65))
+      (symbol_1 i32 (i32 -65)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_2 i32 (i32 0))
+      (symbol_1 i32 (i32 1)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_2 i32 (i32 0))
+      (symbol_1 i32 (i32 0))
+      (symbol_3 i32 (i32 0)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 2))
+      (symbol_2 i32 (i32 0))
+      (symbol_1 i32 (i32 0))
+      (symbol_3 i32 (i32 2)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 -2147483618))
+      (symbol_2 i32 (i32 0))
+      (symbol_1 i32 (i32 0))
+      (symbol_3 i32 (i32 -2147483648)))
+  Reached 5 problems!
 binop i64:
   $ dune exec owi -- sym binop_i64.wast --no-stop-at-failure
   Trap: unreachable
@@ -76,6 +109,39 @@ binop i64:
     (model
       (symbol_0 i64 (i64 -99)))
   Reached 9 problems!
+binop i64 (2):
+  $ dune exec owi -- sym binop_i64-2.wast --no-stop-at-failure
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_1 i64 (i64 0))
+      (symbol_2 i64 (i64 0)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_1 i64 (i64 -1))
+      (symbol_2 i64 (i64 -1)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_1 i64 (i64 -1))
+      (symbol_2 i64 (i64 -2))
+      (symbol_3 i64 (i64 0)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_1 i64 (i64 -2))
+      (symbol_0 i64 (i64 -9223372036854775808))
+      (symbol_2 i64 (i64 -1))
+      (symbol_3 i64 (i64 4611686018427387904)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_1 i64 (i64 -2))
+      (symbol_0 i64 (i64 -9223372036854775804))
+      (symbol_2 i64 (i64 -1))
+      (symbol_3 i64 (i64 -4611686018427387904)))
+  Reached 5 problems!
 binop f32:
   $ dune exec owi -- sym binop_f32.wast --no-stop-at-failure
   Trap: unreachable

test/sym/binop_i32-2.wast

@@ -0,0 +1,42 @@
+(module
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+
+  (func $start
+    (local $w i32)
+    (local $x i32)
+    (local $y i32)
+    (local $z i32)
+
+    (local.set $w (call $i32_symbol))
+    (local.set $x (call $i32_symbol))
+    (local.set $y (call $i32_symbol))
+    (local.set $z (call $i32_symbol))
+
+    (i32.and (local.get $x) (local.get $y))
+    (if (then unreachable))
+
+    (i32.or (local.get $x) (local.get $y))
+    (if (then unreachable))
+
+    (i32.xor (local.get $x) (local.get $y))
+    (if (then unreachable))
+
+    (i32.eqz (i32.shl (local.get $z) (i32.const 0)))
+    (if (then unreachable))
+
+    (i32.eqz (i32.shr_s (local.get $z) (local.get $w)))
+    (if (then unreachable))
+
+    (i32.eqz (i32.shr_u (local.get $z) (local.get $w)))
+    (if (then unreachable))
+
+    ;; owi: internal error, uncaught exception:
+    ;;  Failure("z3_mappings: rotl|rotr not implemented!")
+    ;; (i32.eqz (i32.rotl (local.get $z) (local.get $w)))
+    ;; (if (then unreachable))
+    ;; (i32.eqz (i32.rotr (local.get $z) (local.get $w)))
+    ;; (if (then unreachable))
+  )
+
+  (start $start)
+)

test/sym/binop_i64-2.wast

@@ -0,0 +1,42 @@
+(module
+  (import "symbolic" "i64_symbol" (func $i64_symbol (result i64)))
+
+  (func $start
+    (local $w i64)
+    (local $x i64)
+    (local $y i64)
+    (local $z i64)
+
+    (local.set $w (call $i64_symbol))
+    (local.set $x (call $i64_symbol))
+    (local.set $y (call $i64_symbol))
+    (local.set $z (call $i64_symbol))
+
+    (i64.eqz (i64.and (local.get $x) (local.get $y)))
+    (if (then unreachable))
+
+    (i64.eqz (i64.or (local.get $x) (local.get $y)))
+    (if (then unreachable))
+
+    (i64.eqz (i64.xor (local.get $x) (local.get $y)))
+    (if (then unreachable))
+
+    (i64.eqz (i64.shl (local.get $z) (i64.const 0)))
+    (if (then unreachable))
+
+    (i64.eqz (i64.shr_s (local.get $z) (local.get $w)))
+    (if (then unreachable))
+
+    (i64.eqz (i64.shr_u (local.get $z) (local.get $w)))
+    (if (then unreachable))
+
+    ;; owi: internal error, uncaught exception:
+    ;;  Failure("z3_mappings: rotl|rotr not implemented!")
+    ;; (i64.eqz (i64.rotl (local.get $z) (local.get $w)))
+    ;; (if (then unreachable))
+    ;; (i64.eqz (i64.rotr (local.get $z) (local.get $w)))
+    ;; (if (then unreachable))
+  )
+
+  (start $start)
+)

test/sym/dune

@@ -4,7 +4,9 @@
   mini_test.wast
   assume.wast
   binop_i32.wast
+  binop_i32-2.wast
   binop_i64.wast
+  binop_i64-2.wast
   binop_f32.wast
   binop_f64.wast
   global.wast

test/sym/memory.wast

@@ -4,8 +4,6 @@
   (import "symbolic" "f32_symbol" (func $f32_symbol (result f32)))
   (import "symbolic" "f64_symbol" (func $f64_symbol (result f64)))
 
-  (import "symbolic" "assume_positive_i32" (func $positive_i32 (param i32)))
-
   (memory $m 1)
   (data $d (memory $m) (offset i32.const 99) "str_data")
 

test/sym/unop_f64.wast

@@ -30,6 +30,15 @@
     (f64.le (f64.neg (local.get $x)) (f64.const 42))
     (if (then unreachable))
 
+    ;; owi: internal error, uncaught exception:
+    ;;  File "src/symbolic_value.ml", line 420, characters 18-24: Assertion failed
+    ;; (f64.eq (f64.trunc (local.get $x)) (f64.const 123))
+    ;; (if (then unreachable))
+
+    ;; very long computation
+    ;; (f64.eq (f64.sqrt (local.get $x)) (f64.const 0))
+    ;; (if (then unreachable))
+
     (f64.eq (f64.nearest (local.get $x)) (f64.const 123))
     (if (then unreachable))