Skip to content

Commit

Permalink
make all cmd argument named
Browse files Browse the repository at this point in the history
  • Loading branch information
zapashcanon committed Dec 4, 2024
1 parent 075ffe6 commit 7fd4b22
Show file tree
Hide file tree
Showing 23 changed files with 151 additions and 128 deletions.
81 changes: 38 additions & 43 deletions src/bin/owi.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -115,25 +107,13 @@ 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.(
value
& 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)
Expand Down Expand Up @@ -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 =
Expand All @@ -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 *)

Expand All @@ -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 *)

Expand All @@ -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 *)

Expand All @@ -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 *)

Expand All @@ -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 *)

Expand All @@ -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 *)

Expand All @@ -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 *)

Expand All @@ -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 *)

Expand All @@ -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 *)

Expand All @@ -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 *)

Expand All @@ -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 *)

Expand Down
14 changes: 7 additions & 7 deletions src/cmd/cmd_c.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
40 changes: 20 additions & 20 deletions src/cmd/cmd_c.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
7 changes: 4 additions & 3 deletions src/cmd/cmd_conc.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down
30 changes: 15 additions & 15 deletions src/cmd/cmd_conc.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion src/cmd/cmd_fmt.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion src/cmd/cmd_fmt.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion src/cmd/cmd_instrument.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
7 changes: 6 additions & 1 deletion src/cmd/cmd_instrument.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion src/cmd/cmd_opt.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
7 changes: 6 additions & 1 deletion src/cmd/cmd_opt.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion src/cmd/cmd_run.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
9 changes: 8 additions & 1 deletion src/cmd/cmd_run.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion src/cmd/cmd_script.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
Loading

0 comments on commit 7fd4b22

Please sign in to comment.