Test coverage improvement

README.md

@@ -125,10 +125,10 @@ Given a file `test/sym/mini_test.wast` with the following content:
 <!-- $MDX file=test/sym/mini_test.wast -->
 ```wast
 (module
-  (import "symbolic" "i32" (func $gen_i32 (param i32) (result i32)))
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
 
   (func $start (local $x i32)
-    (local.set $x (call $gen_i32 (i32.const 42)))
+    (local.set $x (call $i32_symbol))
     (if (i32.lt_s (i32.const 5) (local.get $x)) (then
       unreachable
     )))
@@ -143,7 +143,7 @@ $ dune exec owi -- sym test/sym/mini_test.wast
 Trap: unreachable
 Model:
   (model
-    (x_0 i32 (i32 6)))
+    (symbol_0 i32 (i32 6)))
 Reached problem!
 ```
 

src/choice_monad.ml

@@ -23,13 +23,13 @@ let check (sym_bool : vbool) (state : Thread.t) : bool =
   | Val False -> true
   | _ ->
     let check = no :: pc in
-    Format.pp_std "CHECK:@.%a"
+    (* Format.pp_std "CHECK:@.%a"
       (Format.pp_list ~pp_sep:Format.pp_newline Expr.pp)
-      check;
+      check; *)
     let module Solver = (val solver_module) in
     let r = Solver.check solver check in
-    let msg = if r then "KO" else "OK" in
-    Format.pp_std "@./CHECK %s@." msg;
+    (* let msg = if r then "KO" else "OK" in
+    Format.pp_std "@./CHECK %s@." msg; *)
     not r
 
 (* TODO: make this a CLI flag ? *)

src/cmd_sym.ml

@@ -9,60 +9,9 @@ let print_solver_time = false
 
 let print_path_condition = false
 
-let print_extern_module : Symbolic.P.extern_func Link.extern_module =
-  let print_i32 (i : Value.int32) : unit Choice.t =
-    Format.pp_std "%s@\n" (Expr.to_string i);
-    Choice.return ()
-  in
-  (* we need to describe their types *)
-  let functions =
-    [ ( "i32"
-      , Symbolic.P.Extern_func.Extern_func (Func (Arg (I32, Res), R0), print_i32)
-      )
-    ]
-  in
-  { functions }
-
-let assert_extern_module : Symbolic.P.extern_func Link.extern_module =
-  let positive_i32 (i : Value.int32) : unit Choice.t =
-    let c = Value.I32.ge i Value.I32.zero in
-    Choice.add_pc c
-  in
-  let assert_i32 (i : Value.int32) : unit Choice.t =
-    let c = Value.I32.to_bool i in
-    Choice.add_pc c
-  in
-  (* we need to describe their types *)
-  let functions =
-    [ ( "positive_i32"
-      , Symbolic.P.Extern_func.Extern_func
-          (Func (Arg (I32, Res), R0), positive_i32) )
-    ; ( "i32"
-      , Symbolic.P.Extern_func.Extern_func
-          (Func (Arg (I32, Res), R0), assert_i32) )
-    ]
-  in
-  { functions }
-
-let names = [| "plop"; "foo"; "bar" |]
-
 let symbolic_extern_module : Symbolic.P.extern_func Link.extern_module =
   let sym_cnt = Atomic.make 0 in
   let mk_symbol = Encoding.Symbol.mk_symbol in
-  let symbolic_i32 (i : Value.int32) : Value.int32 Choice.t =
-    let name =
-      match i.e with
-      | Expr.Val (Num (I32 i)) -> begin
-        match names.(Int32.to_int i) with exception _ -> "x" | name -> name
-      end
-      | _ -> Format.kasprintf failwith "Text name %a" Expr.pp i
-    in
-    let id = Atomic.fetch_and_add sym_cnt 1 in
-    let r =
-      Expr.mk_symbol @@ mk_symbol (Ty_bitv S32) (Format.sprintf "%s_%i" name id)
-    in
-    Choice.return r
-  in
   let symbol ty () : Value.int32 Choice.t =
     let id = Atomic.fetch_and_add sym_cnt 1 in
     let r = Expr.mk_symbol @@ mk_symbol ty (Format.sprintf "symbol_%i" id) in
@@ -74,16 +23,17 @@ let symbolic_extern_module : Symbolic.P.extern_func Link.extern_module =
     let c = Value.I32.to_bool i in
     Choice.add_pc c
   in
+  let assume_positive_i32 (i : Value.int32) : unit Choice.t =
+    let c = Value.I32.ge i Value.I32.zero in
+    Choice.add_pc c
+  in
   let assert_i32 (i : Value.int32) : unit Choice.t =
     let c = Value.I32.to_bool i in
     Choice.assertion c
   in
   (* we need to describe their types *)
   let functions =
-    [ ( "i32"
-      , Symbolic.P.Extern_func.Extern_func
-          (Func (Arg (I32, Res), R1 I32), symbolic_i32) )
-    ; ( "i8_symbol"
+    [ ( "i8_symbol"
       , Symbolic.P.Extern_func.Extern_func
           (Func (UArg Res, R1 I32), symbol (Ty_bitv S8)) )
     ; ( "i32_symbol"
@@ -101,6 +51,9 @@ let symbolic_extern_module : Symbolic.P.extern_func Link.extern_module =
     ; ( "assume"
       , Symbolic.P.Extern_func.Extern_func
           (Func (Arg (I32, Res), R0), assume_i32) )
+    ; ( "assume_positive_i32"
+      , Symbolic.P.Extern_func.Extern_func
+          (Func (Arg (I32, Res), R0), assume_positive_i32) )
     ; ( "assert"
       , Symbolic.P.Extern_func.Extern_func
           (Func (Arg (I32, Res), R0), assert_i32) )
@@ -167,14 +120,6 @@ let ( let*/ ) (t : 'a Result.t) (f : 'a -> 'b Result.t Choice.t) :
 let simplify_then_link_then_run ~unsafe ~optimize (pc : unit Result.t Choice.t)
   file =
   let link_state = Link.empty_state in
-  let link_state =
-    Link.extern_module' link_state ~name:"print"
-      ~func_typ:Symbolic.P.Extern_func.extern_type print_extern_module
-  in
-  let link_state =
-    Link.extern_module' link_state ~name:"assert"
-      ~func_typ:Symbolic.P.Extern_func.extern_type assert_extern_module
-  in
   let link_state =
     Link.extern_module' link_state ~name:"symbolic"
       ~func_typ:Symbolic.P.Extern_func.extern_type symbolic_extern_module

test/optimize/not_exists.t

@@ -0,0 +1,4 @@
+file doesn't exist:
+  $ dune exec -- owi opt not_exists.wast --debug
+  file `not_exists.wast` doesn't exist
+  [1]

test/run/not_exists.t

@@ -0,0 +1,4 @@
+file doesn't exist (run option):
+  $ dune exec -- owi run not_exists.wast --debug --profiling
+  file `not_exists.wast` doesn't exist
+  [1]

test/script/not_exists.t

@@ -0,0 +1,4 @@
+file doesn't exist (script option):
+  $ dune exec -- owi script not_exists.wast --debug --profiling
+  file `not_exists.wast` doesn't exist
+  [1]

test/sym/assume.t

@@ -0,0 +1,3 @@
+symbolic extern module (assume and assert test):
+  $ dune exec owi -- sym assume.wast
+  All OK

test/sym/assume.wast

@@ -0,0 +1,17 @@
+(module
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+  (import "symbolic" "assume" (func $assume_i32 (param i32)))
+  (import "symbolic" "assume_positive_i32" (func $positive_i32 (param i32)))
+  (import "symbolic" "assert" (func $assert_i32 (param i32)))
+
+  (func $start
+    (local $x i32)
+    (local.set $x (call $i32_symbol))
+    (call $assume_i32 (local.get $x))
+    (call $positive_i32 (local.get $x))
+    (call $assert_i32 (local.get $x))
+    (if (i32.gt_s (i32.const 0) (local.get $x))
+      (then unreachable)))
+
+  (start $start)
+)

test/sym/binop.t

@@ -0,0 +1,140 @@
+binop i32:
+  $ dune exec owi -- sym binop_i32.wast --no-stop-at-failure
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 -1073741923)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 2147483549)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 50)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 -42)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 42)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 0)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 30)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 -34)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 -46)))
+  Reached 9 problems!
+binop i64:
+  $ dune exec owi -- sym binop_i64.wast --no-stop-at-failure
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i64 (i64 -9223231299366420579)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i64 (i64 9223372036854775709)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i64 (i64 50)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i64 (i64 -42)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i64 (i64 42)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i64 (i64 0)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i64 (i64 30)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i64 (i64 -34)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i64 (i64 -99)))
+  Reached 9 problems!
+binop f32:
+  $ dune exec owi -- sym binop_f32.wast --no-stop-at-failure
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f32 (f32 -200.000015)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f32 (f32 200.000015)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f32 (f32 -42.000000)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f32 (f32 42.000000)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f32 (f32 0.000000)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f32 (f32 0.000000)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f32 (f32 -64.005882)))
+  Reached 7 problems!
+binop f64:
+  $ dune exec owi -- sym binop_f64.wast --no-stop-at-failure
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f64 (f64 -200.000000)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f64 (f64 200.000000)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f64 (f64 -42.000000)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f64 (f64 42.000000)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f64 (f64 -0.000000)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f64 (f64 0.000000)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f64 (f64 0.000000)))
+  Reached 7 problems!

test/sym/binop_f32.wast

@@ -0,0 +1,47 @@
+(module
+  (import "symbolic" "f32_symbol" (func $f32_symbol (result f32)))
+
+  (func $start
+    (local $x f32)
+
+    (local.set $x (call $f32_symbol))
+
+    (f32.le (local.get $x) (f32.const -100))
+    (if (then unreachable))
+
+    (f32.lt (local.get $x) (f32.const -100))
+    (if (then unreachable))
+
+    (f32.ge (local.get $x) (f32.const 100))
+    (if (then unreachable))
+
+    (f32.gt (local.get $x) (f32.const 100))
+    (if (then unreachable))
+
+    (f32.eq (f32.add (local.get $x) (f32.const 42)) (f32.const 0))
+    (if (then unreachable))
+
+    (f32.eq (f32.sub (local.get $x) (f32.const 42)) (f32.const 0))
+    (if (then unreachable))
+
+    (f32.eq (f32.mul (local.get $x) (f32.const 42)) (f32.const 0))
+    (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))
+
+    ;; File "src/symbolic_value.ml", line 436, characters 24-30: Assertion failed
+    ;; (f32.eq (f32.copysign (local.get $x) (f32.const 42)) (f32.const 0))
+    ;; (if (then unreachable))
+
+    (f32.ne (local.get $x) (f32.const 42))
+    (if (then unreachable)))
+
+  (start $start)
+)