From b6d0b74d49efe8e7344291e3f9aa2ca402c40192 Mon Sep 17 00:00:00 2001 From: zapashcanon Date: Sat, 7 Dec 2024 13:58:25 +0100 Subject: [PATCH] some code cleaning --- example/c/README.md | 6 +-- example/conc/README.md | 6 +-- example/sym/README.md | 6 +-- src/bin/owi.ml | 70 +++++++++++++++++---------------- src/cmd/cmd_c.ml | 1 - src/cmd/cmd_c.mli | 2 +- src/symbolic/symbolic_global.ml | 6 +-- 7 files changed, 47 insertions(+), 50 deletions(-) diff --git a/example/c/README.md b/example/c/README.md index e086f31b1..e009535bd 100644 --- a/example/c/README.md +++ b/example/c/README.md @@ -473,12 +473,12 @@ OPTIONS --no-value do not display a value for each symbol - -o VAL, --output=VAL (absent=owi-out) - write results to dir - -O VAL (absent=3) specify which optimization level to use + -o VAL, --outpt=VAL (absent=owi-out) + write results to dir + --optimize optimize mode diff --git a/example/conc/README.md b/example/conc/README.md index 17818c498..2db55b1e0 100644 --- a/example/conc/README.md +++ b/example/conc/README.md @@ -68,6 +68,9 @@ OPTIONS --no-value do not display a value for each symbol + -o VAL, --outpt=VAL (absent=owi-out) + write results to dir + --optimize optimize mode @@ -90,9 +93,6 @@ OPTIONS number of workers for symbolic execution. Defaults to the number of physical cores. - --workspace=VAL (absent=owi-out) - path to the workspace directory - COMMON OPTIONS --help[=FMT] (default=auto) Show this help in format FMT. The value FMT must be one of auto, diff --git a/example/sym/README.md b/example/sym/README.md index 6d3b716ab..a35bde1fc 100644 --- a/example/sym/README.md +++ b/example/sym/README.md @@ -68,6 +68,9 @@ OPTIONS --no-value do not display a value for each symbol + -o VAL, --outpt=VAL (absent=owi-out) + write results to dir + --optimize optimize mode @@ -90,9 +93,6 @@ OPTIONS number of workers for symbolic execution. Defaults to the number of physical cores. - --workspace=VAL (absent=owi-out) - path to the workspace directory - COMMON OPTIONS --help[=FMT] (default=auto) Show this help in format FMT. The value FMT must be one of auto, diff --git a/src/bin/owi.ml b/src/bin/owi.ml index ef8ef52ee..4d19898c7 100644 --- a/src/bin/owi.ml +++ b/src/bin/owi.ml @@ -7,19 +7,33 @@ open Cmdliner (* Helpers *) -let existing_non_dir_file = +let existing_file_conv = let parse s = - let path = Fpath.v s in - match Bos.OS.File.exists path with - | Ok true -> `Ok path - | Ok false -> `Error (Fmt.str "no file '%a'" Fpath.pp path) - | Error (`Msg s) -> `Error s + match Fpath.of_string s with + | Error _ as e -> e + | Ok path -> begin + match Bos.OS.File.exists path with + | Ok true -> Ok path + | Ok false -> Fmt.error_msg "no file '%a'" Fpath.pp path + | Error _ as e -> e + end + in + Arg.conv (parse, Fpath.pp) + +let existing_dir_conv = + let parse s = + match Fpath.of_string s with + | Error _ as e -> e + | Ok path -> begin + match Bos.OS.Dir.exists path with + | Ok true -> Ok path + | Ok false -> Fmt.error_msg "no directory '%a'" Fpath.pp path + | Error _ as e -> e + end in - (parse, Fpath.pp) + Arg.conv (parse, Fpath.pp) -let dir_file = - let parse s = `Ok (Fpath.v s) in - (parse, Fpath.pp) +let path_conv = Arg.conv (Fpath.of_string, Fpath.pp) let solver_conv = Arg.conv @@ -53,20 +67,16 @@ let deterministic_result_order = let files = let doc = "source files" in - let f = existing_non_dir_file in - Arg.(value & pos_all f [] (info [] ~doc)) + Arg.(value & pos_all existing_file_conv [] (info [] ~doc)) let source_file = let doc = "source file" in - Arg.(required & pos 0 (some existing_non_dir_file) None (info [] ~doc)) + Arg.(required & pos 0 (some existing_file_conv) None (info [] ~doc)) let out_file = let doc = "Write output to a file." in - let string_to_path = Arg.conv ~docv:"FILE" (Fpath.of_string, Fpath.pp) in Arg.( - value - & opt (some string_to_path) None - & info [ "o"; "output" ] ~docv:"FILE" ~doc ) + value & opt (some path_conv) None & info [ "o"; "output" ] ~docv:"FILE" ~doc ) let no_stop_at_failure = let doc = "do not stop when a program failure is encountered" in @@ -128,8 +138,8 @@ let workers = & info [ "workers"; "w" ] ~doc ~absent:"n" ) let workspace = - let doc = "path to the workspace directory" in - Arg.(value & opt dir_file (Fpath.v "owi-out") & info [ "workspace" ] ~doc) + let doc = "write results to dir" in + Arg.(value & opt path_conv (Fpath.v "owi-out") & info [ "outpt"; "o" ] ~doc) (* owi c *) @@ -144,20 +154,17 @@ let c_cmd = Arg.(value & opt int 32 & info [ "arch"; "m" ] ~doc) and+ property = let doc = "property file" in - Arg.( - value & opt (some existing_non_dir_file) None & info [ "property" ] ~doc ) + Arg.(value & opt (some existing_file_conv) None & info [ "property" ] ~doc) and+ includes = let doc = "headers path" in - Arg.(value & opt_all dir_file [] & info [ "I" ] ~doc) + Arg.(value & opt_all existing_dir_conv [] & info [ "I" ] ~doc) and+ opt_lvl = let doc = "specify which optimization level to use" in Arg.(value & opt string "3" & info [ "O" ] ~doc) and+ testcomp = let doc = "test-comp mode" in Arg.(value & flag & info [ "testcomp" ] ~doc) - and+ workspace = - let doc = "write results to dir" in - Arg.(value & opt string "owi-out" & info [ "output"; "o" ] ~doc) + and+ workspace and+ concolic = let doc = "concolic mode" in Arg.(value & flag & info [ "concolic" ] ~doc) @@ -323,16 +330,11 @@ let replay_cmd = and+ unsafe and+ optimize and+ replay_file = - let parse s = - let path = Fpath.v s in - match Bos.OS.File.exists path with - | Ok true -> Ok path - | Ok false -> Error (`Msg (Fmt.str "no file '%a'" Fpath.pp path)) - | Error _e as e -> e - in - let replay_file = Cmdliner.Arg.conv (parse, Fpath.pp) in let doc = "Which replay file to use" in - Arg.(required & opt (some replay_file) None & info [ "replay-file" ] ~doc) + Arg.( + required + & opt (some existing_file_conv) None + & info [ "replay-file" ] ~doc ) and+ source_file in Cmd_replay.cmd ~profiling ~debug ~unsafe ~optimize ~replay_file ~source_file diff --git a/src/cmd/cmd_c.ml b/src/cmd/cmd_c.ml index 55992eb76..d631b5f76 100644 --- a/src/cmd/cmd_c.ml +++ b/src/cmd/cmd_c.ml @@ -187,7 +187,6 @@ let cmd ~debug ~arch ~property ~testcomp:_ ~workspace ~workers ~opt_lvl ~includes ~files ~profiling ~unsafe ~optimize ~no_stop_at_failure ~no_value ~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 let* files = eacsl_instrument eacsl debug ~includes files in diff --git a/src/cmd/cmd_c.mli b/src/cmd/cmd_c.mli index d22bd6d68..b10645b18 100644 --- a/src/cmd/cmd_c.mli +++ b/src/cmd/cmd_c.mli @@ -7,7 +7,7 @@ val cmd : -> arch:int -> property:Fpath.t option -> testcomp:bool - -> workspace:string + -> workspace:Fpath.t -> workers:int -> opt_lvl:string -> includes:Fpath.t list diff --git a/src/symbolic/symbolic_global.ml b/src/symbolic/symbolic_global.ml index 81df35c67..31564cd55 100644 --- a/src/symbolic/symbolic_global.ml +++ b/src/symbolic/symbolic_global.ml @@ -2,11 +2,7 @@ (* Copyright © 2021-2024 OCamlPro *) (* Written by the Owi programmers *) -module ITbl = Hashtbl.Make (struct - include Int - - let hash x = x -end) +module ITbl = Hashtbl.Make (Int) type t = { mutable value : Symbolic_value.t