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!
 ```
 

dune-project

@@ -61,5 +61,5 @@
   (crowbar :with-test)
   (graphics :dev)
   (tiny_httpd :dev)
-  encoding
+  (encoding (>= 0.0.3))
   xmlm))

owi.opam

@@ -30,7 +30,7 @@ depends: [
   "crowbar" {with-test}
   "graphics" {dev}
   "tiny_httpd" {dev}
-  "encoding"
+  "encoding" {>= "0.0.3"}
   "xmlm"
 ]
 build: [

src/bin/owi.ml

@@ -37,7 +37,7 @@ let unsafe =
 
 let workers =
   let doc = "number of workers for symbolic execution" in
-  Cmdliner.Arg.(value & opt int 4 & info [ "workers"; "w" ] ~doc)
+  Cmdliner.Arg.(value & opt int (Domain.recommended_domain_count ()) & info [ "workers"; "w" ] ~doc)
 
 let workspace =
   let doc = "path to the workspace directory" in

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 ? *)
@@ -112,28 +112,25 @@ struct
     let pc = Thread.pc state in
     let sym_int = Expr.simplify sym_int in
     let orig_pc = pc in
-    let pc, sym = fix_symbol sym_int pc in
+    let pc, symbol = fix_symbol sym_int pc in
     match sym_int.e with
     | Val (Num (I32 i)) -> M.return (i, state)
     | _ ->
       let module Solver = (val solver_module) in
       let rec find_values values =
-        let additionnal = M.to_list @@ M.map (not_value sym) values in
+        let additionnal = M.to_list @@ M.map (not_value symbol) values in
         if not (Solver.check solver (additionnal @ pc)) then M.empty
         else begin
-          let model = Solver.model ~symbols:[ sym ] solver in
+          let model = Solver.model ~symbols:[ symbol ] solver in
           match model with
           | None -> assert false (* ? *)
           | Some model -> (
             Format.pp_std "Model:@.%a@." Model.pp model;
-            let v = Model.evaluate model sym in
+            let v = Model.evaluate model symbol in
             match v with
             | None -> assert false (* ? *)
-            | Some (Num (I32 i) as v) -> begin
-              let cond =
-                Expr.(
-                  Relop (Eq, mk_symbol sym, Val v @: Ty_bitv S32) @: Ty_bitv S32 )
-              in
+            | Some (Num (I32 i)) -> begin
+              let cond = Expr.Bitv.I32.(Expr.mk_symbol symbol = v i) in
               let pc = cond :: pc in
               let case = (i, { state with pc }) in
               M.cons case (find_values (M.cons i values))
@@ -570,8 +567,8 @@ module MT = struct
 
   let spawn_producer _i global =
     let module Mapping = Z3_mappings.Fresh.Make () in
-    let module Batch = Batch.Make (Mapping) in
-    let solver = Batch.create () in
+    let module Batch = Solver.Batch (Mapping) in
+    let solver = Batch.create ~logic:QF_BVFP () in
     let solver : Thread.solver = S ((module Batch), solver) in
     let st = { solver; next = None; global } in
     let rec producer (H (thread, t, cont)) =

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

src/symbolic_value.ml

@@ -287,7 +287,7 @@ module S = struct
 
     let wrap_i64 x = cvtop ty WrapI64 x
 
-    let extend_s _ = assert false
+    let extend_s n x = cvtop ty (ExtS n) x
   end
 
   module I64 = struct
@@ -385,7 +385,7 @@ module S = struct
 
     let reinterpret_f64 x = cvtop ty Reinterpret_float x
 
-    let extend_s _ = assert false
+    let extend_s n x = cvtop ty (ExtS n) x
 
     let extend_i32_s x = cvtop ty (ExtS 32) x
 

src/thread.ml

@@ -2,7 +2,7 @@
 (* Copyright © 2021 Léo Andrès *)
 (* Copyright © 2021 Pierre Chambart *)
 
-module Solver = Encoding.Batch.Make (Encoding.Z3_mappings)
+module Solver = Encoding.Solver.Batch (Encoding.Z3_mappings)
 
 type 'a solver_module = (module Encoding.Solver_intf.S with type t = 'a)
 
@@ -29,7 +29,7 @@ let globals t = t.globals
 let solver_mod : Solver.t solver_module = (module Solver)
 
 let create () =
-  let solver = S (solver_mod, Solver.create ()) in
+  let solver = S (solver_mod, Solver.create ~logic:QF_BVFP ()) in
   { solver
   ; pc = []
   ; memories = Symbolic_memory.init ()

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,8 @@
+symbolic extern module (assume and assert test):
+  $ dune exec owi -- sym assume.wast
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 571440828))
+      (symbol_1 i32 (i32 1744863297)))
+  Reached problem!

test/sym/assume.wast

@@ -0,0 +1,21 @@
+(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 $y i32)
+    (local.set $x (call $i32_symbol))
+    (local.set $y (call $i32_symbol))
+    (call $positive_i32 (local.get $x)) ;; x >= 0
+    (call $assume_i32 (i32.gt_s (local.get $y) (i32.const 0))) ;; (y > 0) > 0
+    (if (i32.le_s (i32.add (local.get $x) (local.get $y)) (i32.const 0)) ;; x + y <= 0
+      (then unreachable))   ;; possible if i32 overflow
+    ;; Alternatively (x + y > 0)
+    (call $assert_i32 (i32.gt_s (i32.add (local.get $x) (local.get $y)) (i32.const 0)))
+  )
+
+  (start $start)
+)