Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

clean code and improve code coverage #403

Merged
merged 1 commit into from
Aug 3, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions example/define_host_function/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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` *)
Expand All @@ -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 () -> ()
```

Expand Down Expand Up @@ -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` *)
Expand All @@ -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 () -> ()
```

Expand Down
6 changes: 3 additions & 3 deletions example/define_host_function/extern.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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` *)
Expand All @@ -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 () -> ()
6 changes: 3 additions & 3 deletions example/define_host_function/extern_mem.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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` *)
Expand All @@ -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 () -> ()
12 changes: 6 additions & 6 deletions example/define_host_function/life_game/life_console.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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` *)
Expand All @@ -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 *)
Expand All @@ -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 () -> ()
12 changes: 6 additions & 6 deletions example/define_host_function/life_game/life_graphics.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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` *)
Expand All @@ -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 *)
Expand All @@ -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 () -> ()
4 changes: 2 additions & 2 deletions example/lib/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -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
Expand Down
4 changes: 2 additions & 2 deletions src/ast/text.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
3 changes: 2 additions & 1 deletion src/bin/owi.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 4 additions & 6 deletions src/cmd/cmd_c.ml
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ open Syntax

type metadata =
{ arch : int
; property : string option
; property : Fpath.t option
; files : Fpath.t list
}

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/cmd/cmd_c.mli
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
val cmd :
bool
-> int
-> string option
-> Fpath.t option
-> bool
-> string
-> int
Expand Down
28 changes: 14 additions & 14 deletions src/cmd/cmd_conc.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand Down Expand Up @@ -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;
Expand All @@ -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

Expand All @@ -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";
Expand Down
12 changes: 3 additions & 9 deletions src/cmd/cmd_fmt.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 ()
2 changes: 0 additions & 2 deletions src/cmd/cmd_fmt.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
6 changes: 0 additions & 6 deletions src/data_structures/indexed.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 0 additions & 4 deletions src/data_structures/indexed.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
Loading
Loading