clean code and improve code coverage

example/define_host_function/README.md

@@ -79,7 +79,7 @@ let link_state =
 (* a pure wasm module refering to `sausage` *)
 let pure_wasm_module =
   match Parse.Text.Module.from_file (Fpath.v "extern.wat") with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok modul -> modul
 
 (* our pure wasm module, linked with `sausage` *)
@@ -88,13 +88,13 @@ let module_to_run, link_state =
     Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None
       pure_wasm_module
   with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok v -> v
 
 (* let's run it ! it will print the values as defined in the print_i32 function *)
 let () =
   match Interpret.Concrete.modul link_state.envs module_to_run with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok () -> ()
 ```
 
@@ -197,7 +197,7 @@ let link_state =
 (* a pure wasm module refering to `$extern_mem` *)
 let pure_wasm_module =
   match Parse.Text.Module.from_file (Fpath.v "extern_mem.wat") with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok modul -> modul
 
 (* our pure wasm module, linked with `chorizo` *)
@@ -206,13 +206,13 @@ let module_to_run, link_state =
     Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None
       pure_wasm_module
   with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok v -> v
 
 (* let's run it ! it will print the values as defined in the print_i64 function *)
 let () =
   match Interpret.Concrete.modul link_state.envs module_to_run with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok () -> ()
 ```
 

example/define_host_function/extern.ml

@@ -33,7 +33,7 @@ let link_state =
 (* a pure wasm module refering to `sausage` *)
 let pure_wasm_module =
   match Parse.Text.Module.from_file (Fpath.v "extern.wat") with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok modul -> modul
 
 (* our pure wasm module, linked with `sausage` *)
@@ -42,11 +42,11 @@ let module_to_run, link_state =
     Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None
       pure_wasm_module
   with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok v -> v
 
 (* let's run it ! it will print the values as defined in the print_i32 function *)
 let () =
   match Interpret.Concrete.modul link_state.envs module_to_run with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok () -> ()

example/define_host_function/extern_mem.ml

@@ -32,7 +32,7 @@ let link_state =
 (* a pure wasm module refering to `$extern_mem` *)
 let pure_wasm_module =
   match Parse.Text.Module.from_file (Fpath.v "extern_mem.wat") with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok modul -> modul
 
 (* our pure wasm module, linked with `chorizo` *)
@@ -41,11 +41,11 @@ let module_to_run, link_state =
     Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None
       pure_wasm_module
   with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok v -> v
 
 (* let's run it ! it will print the values as defined in the print_i64 function *)
 let () =
   match Interpret.Concrete.modul link_state.envs module_to_run with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok () -> ()

example/define_host_function/life_game/life_console.ml

@@ -58,7 +58,7 @@ let link_state =
 (* first pure wasm module refering to `life_ext` *)
 let pure_wasm_module_1 =
   match Parse.Text.Module.from_file (Fpath.v "life.wat") with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok modul -> modul
 
 (* our first pure wasm module, linked with `life_ext` *)
@@ -67,19 +67,19 @@ let module_to_run, link_state =
     Compile.Text.until_link link_state ~unsafe:false ~optimize:true
       ~name:(Some "life") pure_wasm_module_1
   with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok (m, state) -> (m, state)
 
 (* let's run it ! First module to be interpreted *)
 let () =
   match Interpret.Concrete.modul link_state.envs module_to_run with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok () -> ()
 
 (* second pure wasm module refering to `life_ext` *)
 let pure_wasm_module_2 =
   match Parse.Text.Module.from_file (Fpath.v "life_loop.wat") with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok modul -> modul
 
 (* our second pure wasm module, linked with `life_ext` and `life` interpreted before *)
@@ -88,11 +88,11 @@ let module_to_run, link_state =
     Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None
       pure_wasm_module_2
   with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok (m, state) -> (m, state)
 
 (* let's run it ! it will animate the game of life in console *)
 let () =
   match Interpret.Concrete.modul link_state.envs module_to_run with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok () -> ()

example/define_host_function/life_game/life_graphics.ml

@@ -70,7 +70,7 @@ let link_state =
 (* first pure wasm module refering to `life_ext` *)
 let pure_wasm_module_1 =
   match Parse.Text.Module.from_file (Fpath.v "life.wat") with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok modul -> modul
 
 (* our first pure wasm module, linked with `life_ext` *)
@@ -79,19 +79,19 @@ let module_to_run, link_state =
     Compile.Text.until_link link_state ~unsafe:false ~optimize:true
       ~name:(Some "life") pure_wasm_module_1
   with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok (m, state) -> (m, state)
 
 (* let's run it ! First module to be interpreted *)
 let () =
   match Interpret.Concrete.modul link_state.envs module_to_run with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok () -> ()
 
 (* second pure wasm module refering to `life_ext` *)
 let pure_wasm_module_2 =
   match Parse.Text.Module.from_file (Fpath.v "life_loop.wat") with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok modul -> modul
 
 (* our second pure wasm module, linked with `life_ext` and `life` interpreted before *)
@@ -100,11 +100,11 @@ let module_to_run, link_state =
     Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None
       pure_wasm_module_2
   with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok (m, state) -> (m, state)
 
 (* let's run it ! it will animate the game of life in a graphics window *)
 let () =
   match Interpret.Concrete.modul link_state.envs module_to_run with
-  | Error e -> Result.failwith e
+  | Error _ -> assert false
   | Ok () -> ()

example/lib/README.md

@@ -18,7 +18,7 @@ val m : Text.modul =
 # let module_to_run, link_state =
     match Compile.Text.until_link Link.empty_state ~unsafe:false ~optimize:false ~name:None m with
     | Ok v -> v
-    | Error e -> Result.failwith e;;
+    | Error _ -> assert false;;
 val module_to_run : '_weak1 Link.module_to_run =
 ...
 val link_state : '_weak1 Link.state =
@@ -27,7 +27,7 @@ val link_state : '_weak1 Link.state =
     Log.debug_on := true;
     match Interpret.Concrete.modul link_state.envs module_to_run with
     | Ok () -> ()
-    | Error e -> Result.failwith e;;
+    | Error _ -> assert false;;
 interpreting ...
 stack        : [  ]
 running instr: call 0

src/ast/text.ml

@@ -128,11 +128,11 @@ type result =
 
 let pp_result fmt = function
   | Result_const c -> pf fmt "(%a)" pp_result_const c
-  | Result_func_ref | Result_extern_ref -> Log.err "not yet implemented"
+  | Result_func_ref | Result_extern_ref -> assert false
 
 let pp_result_bis fmt = function
   | Result_const c -> pf fmt "%a" pp_result_const c
-  | Result_extern_ref | Result_func_ref -> Log.err "not yet implemented"
+  | Result_extern_ref | Result_func_ref -> assert false
 
 let pp_results fmt r = list ~sep:sp pp_result_bis fmt r
 

src/bin/owi.ml

@@ -119,7 +119,8 @@ let c_cmd =
   in
   let property =
     let doc = "property file" in
-    Arg.(value & opt (some string) None & info [ "property" ] ~doc)
+    Arg.(
+      value & opt (some existing_non_dir_file) None & info [ "property" ] ~doc )
   in
   let includes =
     let doc = "headers path" in

src/cmd/cmd_c.ml

@@ -7,7 +7,7 @@ open Syntax
 
 type metadata =
   { arch : int
-  ; property : string option
+  ; property : Fpath.t option
   ; files : Fpath.t list
   }
 
@@ -80,15 +80,14 @@ let metadata ~workspace arch property files : unit Result.t =
     let tag n = (("", n), []) in
     let el n d = `El (tag n, [ `Data d ]) in
     let* spec =
-      match property with None -> Ok "" | Some f -> OS.File.read @@ Fpath.v f
+      match property with None -> Ok "" | Some f -> OS.File.read f
     in
     let file = String.concat " " (List.map Fpath.to_string files) in
     let* hash =
       list_fold_left
         (fun context file ->
-          match Bos.OS.File.read file with
-          | Error (`Msg msg) -> Error (`Msg msg)
-          | Ok str -> Ok (Digestif.SHA256.feed_string context str) )
+          let+ str = Bos.OS.File.read file in
+          Digestif.SHA256.feed_string context str )
         Digestif.SHA256.empty files
     in
     let hash = Digestif.SHA256.to_hex (Digestif.SHA256.get hash) in
@@ -121,7 +120,6 @@ let metadata ~workspace arch property files : unit Result.t =
 let cmd debug arch property _testcomp workspace workers opt_lvl includes files
   profiling unsafe optimize no_stop_at_failure no_values
   deterministic_result_order fail_mode concolic solver : unit Result.t =
-  if debug then Logs.set_level (Some Debug);
   let workspace = Fpath.v workspace in
   let includes = libc_location @ includes in
   let* (_exists : bool) = OS.Dir.create ~path:true workspace in

src/cmd/cmd_c.mli

@@ -5,7 +5,7 @@
 val cmd :
      bool
   -> int
-  -> string option
+  -> Fpath.t option
   -> bool
   -> string
   -> int

src/cmd/cmd_conc.ml

@@ -274,13 +274,13 @@ let run_once tree link_state modules_to_run forced_values =
     Choice.run forced_values result
   in
   let () = List.iter2 Concolic.recover backups modules_to_run in
-  let end_of_trace =
+  let+ end_of_trace =
     match result with
-    | Ok (Ok ()) -> Normal
-    | Ok (Error e) -> Result.failwith e
-    | Error (Trap t) -> Trap t
-    | Error Assert_fail -> Assert_fail
-    | Error (Assume_fail _c) -> Assume_fail
+    | Ok (Ok ()) -> Ok Normal
+    | Ok (Error _ as e) -> e
+    | Error (Trap t) -> Ok (Trap t)
+    | Error Assert_fail -> Ok Assert_fail
+    | Error (Assume_fail _c) -> Ok Assume_fail
   in
   let trace =
     { assignments = symbols_value; remaining_pc = List.rev pc; end_of_trace }
@@ -368,16 +368,16 @@ let launch solver tree link_state modules_to_run =
         end;
         Some m
   in
-  let rec loop count =
-    if count <= 0 then None
+  let rec loop count : _ Result.t =
+    if count <= 0 then Ok None
     else
       let model = find_model 20 in
       run_model model count
-  and run_model model count =
-    let r, thread = run_once tree link_state modules_to_run model in
+  and run_model model count : _ Result.t =
+    let* r, thread = run_once tree link_state modules_to_run model in
     match r with
     | Ok (Ok ()) -> loop (count - 1)
-    | Ok (Error e) -> Result.failwith e
+    | Ok (Error _ as e) -> e
     | Error (Assume_fail c) -> begin
       if debug then begin
         Fmt.pr "Assume_fail: %a@\n" Smtml.Expr.pp c;
@@ -391,8 +391,8 @@ let launch solver tree link_state modules_to_run =
         loop (count - 1)
       | Some _model as model -> run_model model (count - 1)
     end
-    | Error (Trap trap) -> Some (`Trap trap, thread)
-    | Error Assert_fail -> Some (`Assert_fail, thread)
+    | Error (Trap trap) -> Ok (Some (`Trap trap, thread))
+    | Error Assert_fail -> Ok (Some (`Assert_fail, thread))
   in
   loop 10
 
@@ -413,7 +413,7 @@ let cmd profiling debug unsafe optimize _workers _no_stop_at_failure no_values
     simplify_then_link_files ~unsafe ~optimize files
   in
   let tree = fresh_tree [] in
-  let result = launch solver tree link_state modules_to_run in
+  let* result = launch solver tree link_state modules_to_run in
 
   let print_pc pc =
     Fmt.pr "PC:@\n";

src/cmd/cmd_fmt.ml

@@ -16,14 +16,8 @@ let get_printer filename =
   | ext -> Error (`Unsupported_file_extension ext)
 
 let cmd_one inplace file =
-  match get_printer file with
-  | Error _e as e -> e
-  | Ok pp ->
-    if inplace then Bos.OS.File.writef file "%a@\n" pp ()
-    else Ok (Fmt.pr "%a@\n" pp ())
+  let* pp = get_printer file in
+  if inplace then Bos.OS.File.writef file "%a@\n" pp ()
+  else Ok (Fmt.pr "%a@\n" pp ())
 
 let cmd inplace files = list_iter (cmd_one inplace) files
-
-let format_file_to_string file =
-  let+ pp = get_printer file in
-  Fmt.str "%a@\n" pp ()

src/cmd/cmd_fmt.mli

@@ -3,5 +3,3 @@
 (* Written by the Owi programmers *)
 
 val cmd : bool -> Fpath.t list -> unit Result.t
-
-val format_file_to_string : Fpath.t -> string Result.t

src/data_structures/indexed.ml

@@ -17,13 +17,7 @@ let return index value = { index; value }
 
 let has_index idx { index; _ } = idx = index
 
-let get_at_exn i values =
-  let { value; _ } = List.find (has_index i) values in
-  value
-
 let get_at i values =
   match List.find_opt (has_index i) values with
   | None -> None
   | Some { value; _ } -> Some value
-
-let pp f fmt v = f fmt v.value

src/data_structures/indexed.mli

@@ -14,8 +14,4 @@ val return : int -> 'a -> 'a t
 
 val get_at : int -> 'a t list -> 'a option
 
-val get_at_exn : int -> 'a t list -> 'a
-
 val has_index : int -> 'a t -> bool
-
-val pp : (Fmt.formatter -> 'a -> unit) -> Fmt.formatter -> 'a t -> unit