diff --git a/src/bin/owi.ml b/src/bin/owi.ml index 329f5ce4..940c75fe 100644 --- a/src/bin/owi.ml +++ b/src/bin/owi.ml @@ -69,14 +69,6 @@ let outfile = & opt (some string_to_path) None & info [ "o"; "output" ] ~docv:"FILE" ~doc ) -let emit_file = - let doc = "Emit (.wat) files from corresponding (.wasm) files." in - Arg.(value & flag & info [ "emit-file" ] ~doc) - -let no_exhaustion = - let doc = "no exhaustion tests" in - Arg.(value & flag & info [ "no-exhaustion" ] ~doc) - let no_stop_at_failure = let doc = "do not stop when a program failure is encountered" in Arg.(value & flag & info [ "no-stop-at-failure" ] ~doc) @@ -115,14 +107,6 @@ let srac = let doc = "symbolic runtime assertion checking mode" in Arg.(value & flag & info [ "srac" ] ~doc) -let eacsl = - let doc = - "e-acsl mode, refer to \ - https://frama-c.com/download/e-acsl/e-acsl-implementation.pdf for \ - Frama-C's current language feature implementations" - in - Arg.(value & flag & info [ "e-acsl" ] ~doc) - let solver = let doc = "SMT solver to use" in Arg.( @@ -130,10 +114,6 @@ let solver = & opt solver_conv Smtml.Solver_dispatcher.Z3_solver & info [ "solver"; "s" ] ~doc ) -let symbolic = - let doc = "generate instrumented module that depends on symbolic execution" in - Arg.(value & flag & info [ "symbolic" ] ~doc) - let unsafe = let doc = "skip typechecking pass" in Arg.(value & flag & info [ "unsafe"; "u" ] ~doc) @@ -176,7 +156,7 @@ let c_cmd = and+ testcomp = let doc = "test-comp mode" in Arg.(value & flag & info [ "testcomp" ] ~doc) - and+ output = + and+ workspace = let doc = "write results to dir" in Arg.(value & opt string "owi-out" & info [ "output"; "o" ] ~doc) and+ concolic = @@ -193,12 +173,18 @@ let c_cmd = and+ no_assert_failure_expression_printing and+ deterministic_result_order and+ fail_mode - and+ eacsl + and+ eacsl = + let doc = + "e-acsl mode, refer to \ + https://frama-c.com/download/e-acsl/e-acsl-implementation.pdf for \ + Frama-C's current language feature implementations" + in + Arg.(value & flag & info [ "e-acsl" ] ~doc) and+ solver in - Cmd_c.cmd debug arch property testcomp output workers opt_lvl includes files - profiling unsafe optimize no_stop_at_failure no_values - no_assert_failure_expression_printing deterministic_result_order fail_mode - concolic eacsl solver + Cmd_c.cmd ~debug ~arch ~property ~testcomp ~workspace ~workers ~opt_lvl + ~includes ~files ~profiling ~unsafe ~optimize ~no_stop_at_failure ~no_values + ~no_assert_failure_expression_printing ~deterministic_result_order + ~fail_mode ~concolic ~eacsl ~solver (* owi fmt *) @@ -212,7 +198,7 @@ let fmt_cmd = let doc = "Format in-place, overwriting input file" in Arg.(value & flag & info [ "inplace"; "i" ] ~doc) and+ files in - Cmd_fmt.cmd inplace files + Cmd_fmt.cmd ~inplace ~files (* owi opt *) @@ -226,7 +212,7 @@ let opt_cmd = and+ unsafe and+ sourcefile and+ outfile in - Cmd_opt.cmd debug unsafe sourcefile outfile + Cmd_opt.cmd ~debug ~unsafe ~file:sourcefile ~outfile (* owi instrument *) @@ -241,9 +227,13 @@ let instrument_info = let instrument_cmd = let+ debug and+ unsafe - and+ symbolic + and+ symbolic = + let doc = + "generate instrumented module that depends on symbolic execution" + in + Arg.(value & flag & info [ "symbolic" ] ~doc) and+ files in - Cmd_instrument.cmd debug unsafe symbolic files + Cmd_instrument.cmd ~debug ~unsafe ~symbolic ~files (* owi run *) @@ -259,7 +249,7 @@ let run_cmd = and+ rac and+ optimize and+ files in - Cmd_run.cmd profiling debug unsafe rac optimize files + Cmd_run.cmd ~profiling ~debug ~unsafe ~rac ~optimize ~files (* owi validate *) @@ -271,7 +261,7 @@ let validate_info = let validate_cmd = let+ debug and+ files in - Cmd_validate.cmd debug files + Cmd_validate.cmd ~debug ~files (* owi script *) @@ -285,8 +275,11 @@ let script_cmd = and+ debug and+ optimize and+ files - and+ no_exhaustion in - Cmd_script.cmd profiling debug optimize files no_exhaustion + and+ no_exhaustion = + let doc = "no exhaustion tests" in + Arg.(value & flag & info [ "no-exhaustion" ] ~doc) + in + Cmd_script.cmd ~profiling ~debug ~optimize ~files ~no_exhaustion (* owi sym *) @@ -311,9 +304,9 @@ let sym_cmd = and+ workspace and+ solver and+ files in - Cmd_sym.cmd profiling debug unsafe rac srac optimize workers - no_stop_at_failure no_values no_assert_failure_expression_printing - deterministic_result_order fail_mode workspace solver files + Cmd_sym.cmd ~profiling ~debug ~unsafe ~rac ~srac ~optimize ~workers + ~no_stop_at_failure ~no_values ~no_assert_failure_expression_printing + ~deterministic_result_order ~fail_mode ~workspace ~solver ~files (* owi conc *) @@ -338,9 +331,9 @@ let conc_cmd = and+ workspace and+ solver and+ files in - Cmd_conc.cmd profiling debug unsafe rac srac optimize workers - no_stop_at_failure no_values no_assert_failure_expression_printing - deterministic_result_order fail_mode workspace solver files + Cmd_conc.cmd ~profiling ~debug ~unsafe ~rac ~srac ~optimize ~workers + ~no_stop_at_failure ~no_values ~no_assert_failure_expression_printing + ~deterministic_result_order ~fail_mode ~workspace ~solver ~files (* owi wasm2wat *) @@ -353,9 +346,11 @@ let wasm2wat_info = let wasm2wat_cmd = let+ sourcefile - and+ emit_file + and+ emit_file = + let doc = "Emit (.wat) files from corresponding (.wasm) files." in + Arg.(value & flag & info [ "emit-file" ] ~doc) and+ outfile in - Cmd_wasm2wat.cmd sourcefile emit_file outfile + Cmd_wasm2wat.cmd ~file:sourcefile ~emit_file ~outfile (* owi wat2wasm *) @@ -373,7 +368,7 @@ let wat2wasm_cmd = and+ optimize and+ outfile and+ sourcefile in - Cmd_wat2wasm.cmd profiling debug unsafe optimize outfile sourcefile + Cmd_wat2wasm.cmd ~profiling ~debug ~unsafe ~optimize ~outfile ~file:sourcefile (* owi *) diff --git a/src/cmd/cmd_c.ml b/src/cmd/cmd_c.ml index b63549c6..3c71a72d 100644 --- a/src/cmd/cmd_c.ml +++ b/src/cmd/cmd_c.ml @@ -183,10 +183,10 @@ let metadata ~workspace arch property files : unit Result.t = let* res = OS.File.with_oc fpath out_metadata { arch; property; files } in res -let cmd debug arch property _testcomp workspace workers opt_lvl includes files - profiling unsafe optimize no_stop_at_failure no_values - no_assert_failure_expression_printing deterministic_result_order fail_mode - concolic eacsl solver : unit Result.t = +let cmd ~debug ~arch ~property ~testcomp:_ ~workspace ~workers ~opt_lvl + ~includes ~files ~profiling ~unsafe ~optimize ~no_stop_at_failure ~no_values + ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode + ~concolic ~eacsl ~solver : unit Result.t = let workspace = Fpath.v workspace in let includes = libc_location @ includes in let* (_exists : bool) = OS.Dir.create ~path:true workspace in @@ -196,6 +196,6 @@ let cmd debug arch property _testcomp workspace workers opt_lvl includes files let workspace = Fpath.(workspace / "test-suite") in let files = [ modul ] in (if concolic then Cmd_conc.cmd else Cmd_sym.cmd) - profiling debug unsafe false false optimize workers no_stop_at_failure - no_values no_assert_failure_expression_printing deterministic_result_order - fail_mode workspace solver files + ~profiling ~debug ~unsafe ~rac:false ~srac:false ~optimize ~workers + ~no_stop_at_failure ~no_values ~no_assert_failure_expression_printing + ~deterministic_result_order ~fail_mode ~workspace ~solver ~files diff --git a/src/cmd/cmd_c.mli b/src/cmd/cmd_c.mli index bc860bb8..f3eff669 100644 --- a/src/cmd/cmd_c.mli +++ b/src/cmd/cmd_c.mli @@ -3,24 +3,24 @@ (* Written by the Owi programmers *) val cmd : - bool - -> int - -> Fpath.t option - -> bool - -> string - -> int - -> string - -> Fpath.t list - -> Fpath.t list - -> bool - -> bool - -> bool - -> bool - -> bool - -> bool - -> bool - -> Cmd_sym.fail_mode - -> bool - -> bool - -> Smtml.Solver_dispatcher.solver_type + debug:bool + -> arch:int + -> property:Fpath.t option + -> testcomp:bool + -> workspace:string + -> workers:int + -> opt_lvl:string + -> includes:Fpath.t list + -> files:Fpath.t list + -> profiling:bool + -> unsafe:bool + -> optimize:bool + -> no_stop_at_failure:bool + -> no_values:bool + -> no_assert_failure_expression_printing:bool + -> deterministic_result_order:bool + -> fail_mode:Cmd_sym.fail_mode + -> concolic:bool + -> eacsl:bool + -> solver:Smtml.Solver_dispatcher.solver_type -> unit Result.t diff --git a/src/cmd/cmd_conc.ml b/src/cmd/cmd_conc.ml index 87a022ee..f8f08284 100644 --- a/src/cmd/cmd_conc.ml +++ b/src/cmd/cmd_conc.ml @@ -415,9 +415,10 @@ let run solver tree link_state modules_to_run = during evaluation (OS, syntax error, etc.), except for Trap and Assert, which are handled here. Most of the computations are done in the Result monad, hence the let*. *) -let cmd profiling debug unsafe rac srac optimize _workers _no_stop_at_failure - no_values no_assert_failure_expression_printing _deterministic_result_order - _fail_mode (workspace : Fpath.t) solver files = +let cmd ~profiling ~debug ~unsafe ~rac ~srac ~optimize ~workers:_ + ~no_stop_at_failure:_ ~no_values ~no_assert_failure_expression_printing + ~deterministic_result_order:_ ~fail_mode:_ ~(workspace : Fpath.t) ~solver + ~files = if profiling then Log.profiling_on := true; if debug then Log.debug_on := true; (* deterministic_result_order implies no_stop_at_failure *) diff --git a/src/cmd/cmd_conc.mli b/src/cmd/cmd_conc.mli index 0a27652a..94c1a6b7 100644 --- a/src/cmd/cmd_conc.mli +++ b/src/cmd/cmd_conc.mli @@ -3,19 +3,19 @@ (* Written by the Owi programmers *) val cmd : - bool - -> bool - -> bool - -> bool - -> bool - -> bool - -> int - -> bool - -> bool - -> bool - -> bool - -> Cmd_sym.fail_mode - -> Fpath.t - -> Smtml.Solver_dispatcher.solver_type - -> Fpath.t list + profiling:bool + -> debug:bool + -> unsafe:bool + -> rac:bool + -> srac:bool + -> optimize:bool + -> workers:int + -> no_stop_at_failure:bool + -> no_values:bool + -> no_assert_failure_expression_printing:bool + -> deterministic_result_order:bool + -> fail_mode:Cmd_sym.fail_mode + -> workspace:Fpath.t + -> solver:Smtml.Solver_dispatcher.solver_type + -> files:Fpath.t list -> unit Result.t diff --git a/src/cmd/cmd_fmt.ml b/src/cmd/cmd_fmt.ml index 9a846026..93814aae 100644 --- a/src/cmd/cmd_fmt.ml +++ b/src/cmd/cmd_fmt.ml @@ -20,4 +20,4 @@ let cmd_one inplace file = 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 cmd ~inplace ~files = list_iter (cmd_one inplace) files diff --git a/src/cmd/cmd_fmt.mli b/src/cmd/cmd_fmt.mli index 433a9547..483add9a 100644 --- a/src/cmd/cmd_fmt.mli +++ b/src/cmd/cmd_fmt.mli @@ -2,4 +2,4 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -val cmd : bool -> Fpath.t list -> unit Result.t +val cmd : inplace:bool -> files:Fpath.t list -> unit Result.t diff --git a/src/cmd/cmd_instrument.ml b/src/cmd/cmd_instrument.ml index 26f19eb2..e8d27d3b 100644 --- a/src/cmd/cmd_instrument.ml +++ b/src/cmd/cmd_instrument.ml @@ -25,6 +25,6 @@ let cmd_one unsafe symbolic file = Bos.OS.File.writef filename "%a" Text.pp_modul instrumented_text_modul | ext -> Error (`Unsupported_file_extension ext) -let cmd debug unsafe symbolic files = +let cmd ~debug ~unsafe ~symbolic ~files = if debug then Log.debug_on := true; list_iter (cmd_one unsafe symbolic) files diff --git a/src/cmd/cmd_instrument.mli b/src/cmd/cmd_instrument.mli index 96aaaceb..70b4138f 100644 --- a/src/cmd/cmd_instrument.mli +++ b/src/cmd/cmd_instrument.mli @@ -2,4 +2,9 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -val cmd : bool -> bool -> bool -> Fpath.t list -> unit Result.t +val cmd : + debug:bool + -> unsafe:bool + -> symbolic:bool + -> files:Fpath.t list + -> unit Result.t diff --git a/src/cmd/cmd_opt.ml b/src/cmd/cmd_opt.ml index df5ea111..bc3dc53a 100644 --- a/src/cmd/cmd_opt.ml +++ b/src/cmd/cmd_opt.ml @@ -15,6 +15,6 @@ let print_or_emit ~unsafe file outfile = | Some name -> Bos.OS.File.writef name "%a@\n" Text.pp_modul m | None -> Ok (Fmt.pr "%a@\n" Text.pp_modul m) -let cmd debug unsafe file outfile = +let cmd ~debug ~unsafe ~file ~outfile = if debug then Log.debug_on := true; print_or_emit ~unsafe file outfile diff --git a/src/cmd/cmd_opt.mli b/src/cmd/cmd_opt.mli index 74ce0a34..965f9cb4 100644 --- a/src/cmd/cmd_opt.mli +++ b/src/cmd/cmd_opt.mli @@ -2,4 +2,9 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -val cmd : bool -> bool -> Fpath.t -> Fpath.t option -> unit Result.t +val cmd : + debug:bool + -> unsafe:bool + -> file:Fpath.t + -> outfile:Fpath.t option + -> unit Result.t diff --git a/src/cmd/cmd_run.ml b/src/cmd/cmd_run.ml index d3e949f1..5bbc495a 100644 --- a/src/cmd/cmd_run.ml +++ b/src/cmd/cmd_run.ml @@ -27,7 +27,7 @@ let run_file ~unsafe ~rac ~optimize filename = in () -let cmd profiling debug unsafe rac optimize files = +let cmd ~profiling ~debug ~unsafe ~rac ~optimize ~files = if profiling then Log.profiling_on := true; if debug then Log.debug_on := true; list_iter (run_file ~unsafe ~rac ~optimize) files diff --git a/src/cmd/cmd_run.mli b/src/cmd/cmd_run.mli index 63aec0ac..5d8bd595 100644 --- a/src/cmd/cmd_run.mli +++ b/src/cmd/cmd_run.mli @@ -2,4 +2,11 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -val cmd : bool -> bool -> bool -> bool -> bool -> Fpath.t list -> unit Result.t +val cmd : + profiling:bool + -> debug:bool + -> unsafe:bool + -> rac:bool + -> optimize:bool + -> files:Fpath.t list + -> unit Result.t diff --git a/src/cmd/cmd_script.ml b/src/cmd/cmd_script.ml index 30048a92..3878cb3a 100644 --- a/src/cmd/cmd_script.ml +++ b/src/cmd/cmd_script.ml @@ -8,7 +8,7 @@ let run_file exec filename = let* script = Parse.Text.Script.from_file filename in exec script -let cmd profiling debug optimize files no_exhaustion = +let cmd ~profiling ~debug ~optimize ~files ~no_exhaustion = let exec = Script.exec ~no_exhaustion ~optimize in if profiling then Log.profiling_on := true; if debug then Log.debug_on := true; diff --git a/src/cmd/cmd_script.mli b/src/cmd/cmd_script.mli index fe2dd105..d5850ede 100644 --- a/src/cmd/cmd_script.mli +++ b/src/cmd/cmd_script.mli @@ -2,4 +2,10 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -val cmd : bool -> bool -> bool -> Fpath.t list -> bool -> unit Result.t +val cmd : + profiling:bool + -> debug:bool + -> optimize:bool + -> files:Fpath.t list + -> no_exhaustion:bool + -> unit Result.t diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml index f06f2665..fa489f92 100644 --- a/src/cmd/cmd_sym.ml +++ b/src/cmd/cmd_sym.ml @@ -46,9 +46,9 @@ let run_file ~unsafe ~rac ~srac ~optimize pc filename = during evaluation (OS, syntax error, etc.), except for Trap and Assert, which are handled here. Most of the computations are done in the Result monad, hence the let*. *) -let cmd profiling debug unsafe rac srac optimize workers no_stop_at_failure - no_values no_assert_failure_expression_printing deterministic_result_order - fail_mode (workspace : Fpath.t) solver files = +let cmd ~profiling ~debug ~unsafe ~rac ~srac ~optimize ~workers + ~no_stop_at_failure ~no_values ~no_assert_failure_expression_printing + ~deterministic_result_order ~fail_mode ~workspace ~solver ~files = if profiling then Log.profiling_on := true; if debug then Log.debug_on := true; (* deterministic_result_order implies no_stop_at_failure *) diff --git a/src/cmd/cmd_sym.mli b/src/cmd/cmd_sym.mli index cef78983..005960bf 100644 --- a/src/cmd/cmd_sym.mli +++ b/src/cmd/cmd_sym.mli @@ -9,19 +9,19 @@ type fail_mode = ] val cmd : - bool - -> bool - -> bool - -> bool - -> bool - -> bool - -> int - -> bool - -> bool - -> bool - -> bool - -> fail_mode - -> Fpath.t - -> Smtml.Solver_dispatcher.solver_type - -> Fpath.t list + profiling:bool + -> debug:bool + -> unsafe:bool + -> rac:bool + -> srac:bool + -> optimize:bool + -> workers:int + -> no_stop_at_failure:bool + -> no_values:bool + -> no_assert_failure_expression_printing:bool + -> deterministic_result_order:bool + -> fail_mode:fail_mode + -> workspace:Fpath.t + -> solver:Smtml.Solver_dispatcher.solver_type + -> files:Fpath.t list -> unit Result.t diff --git a/src/cmd/cmd_validate.ml b/src/cmd/cmd_validate.ml index f5c12a61..17474af5 100644 --- a/src/cmd/cmd_validate.ml +++ b/src/cmd/cmd_validate.ml @@ -11,6 +11,6 @@ let validate filename = in () -let cmd debug files = +let cmd ~debug ~files = if debug then Log.debug_on := true; list_iter validate files diff --git a/src/cmd/cmd_validate.mli b/src/cmd/cmd_validate.mli index 433a9547..f8db7978 100644 --- a/src/cmd/cmd_validate.mli +++ b/src/cmd/cmd_validate.mli @@ -2,4 +2,4 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -val cmd : bool -> Fpath.t list -> unit Result.t +val cmd : debug:bool -> files:Fpath.t list -> unit Result.t diff --git a/src/cmd/cmd_wasm2wat.ml b/src/cmd/cmd_wasm2wat.ml index 379eedc0..4407f19e 100644 --- a/src/cmd/cmd_wasm2wat.ml +++ b/src/cmd/cmd_wasm2wat.ml @@ -5,13 +5,12 @@ open Syntax (** Utility function to handle writing to a file or printing to stdout *) -let cmd_one emitfile outfile file = +let cmd ~file ~emit_file ~outfile = let ext = Fpath.get_ext file in - let _dir, wat_file = Fpath.split_base file in - let wat_file = Fpath.set_ext "wat" wat_file in - match ext with | ".wasm" -> + let _dir, wat_file = Fpath.split_base file in + let wat_file = Fpath.set_ext "wat" wat_file in let* m = Parse.Binary.Module.from_file file in let m = Binary_to_text.modul m in let outname, output = @@ -21,9 +20,7 @@ let cmd_one emitfile outfile file = | None -> (wat_file, false) end in - if emitfile || output then + if emit_file || output then Bos.OS.File.writef outname "%a@\n" Text.pp_modul m else Ok (Fmt.pr "%a@\n" Text.pp_modul m) | ext -> Error (`Unsupported_file_extension ext) - -let cmd file emitfile outfile = cmd_one emitfile outfile file diff --git a/src/cmd/cmd_wasm2wat.mli b/src/cmd/cmd_wasm2wat.mli index 220d9b19..b8b0f96f 100644 --- a/src/cmd/cmd_wasm2wat.mli +++ b/src/cmd/cmd_wasm2wat.mli @@ -2,4 +2,5 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -val cmd : Fpath.t -> bool -> Fpath.t option -> unit Result.t +val cmd : + file:Fpath.t -> emit_file:bool -> outfile:Fpath.t option -> unit Result.t diff --git a/src/cmd/cmd_wat2wasm.ml b/src/cmd/cmd_wat2wasm.ml index e820eadb..4b9c65c5 100644 --- a/src/cmd/cmd_wat2wasm.ml +++ b/src/cmd/cmd_wat2wasm.ml @@ -12,7 +12,7 @@ let cmd_one ~unsafe ~optimize outfile file = Binary_encoder.convert outfile file ~unsafe ~optimize modul | ext -> Error (`Unsupported_file_extension ext) -let cmd profiling debug unsafe optimize outfile file = +let cmd ~profiling ~debug ~unsafe ~optimize ~outfile ~file = if profiling then Log.profiling_on := true; if debug then Log.debug_on := true; cmd_one ~unsafe ~optimize outfile file diff --git a/src/cmd/cmd_wat2wasm.mli b/src/cmd/cmd_wat2wasm.mli index 43a9d5c2..a491c20e 100644 --- a/src/cmd/cmd_wat2wasm.mli +++ b/src/cmd/cmd_wat2wasm.mli @@ -3,4 +3,10 @@ (* Written by the Owi programmers *) val cmd : - bool -> bool -> bool -> bool -> Fpath.t option -> Fpath.t -> unit Result.t + profiling:bool + -> debug:bool + -> unsafe:bool + -> optimize:bool + -> outfile:Fpath.t option + -> file:Fpath.t + -> unit Result.t