diff --git a/.ocamlformat b/.ocamlformat index f1462252f..c365faf03 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1,4 +1,4 @@ -version=0.26.2 +version=0.27.0 assignment-operator=end-line break-cases=fit break-fun-decl=wrap diff --git a/bench/report/pie_results.ml b/bench/report/pie_results.ml index f53ac596a..8d72667d8 100644 --- a/bench/report/pie_results.ml +++ b/bench/report/pie_results.ml @@ -107,7 +107,7 @@ let make runs output_dir reference_name = , Format.sprintf "Nothing (%d)" count_nothing ) ] |> List.filter_map (fun ((count, _, _, _) as v) -> - if count = 0 then None else Some v ) + if count = 0 then None else Some v ) |> List.sort (fun (c1, _, _, _) (c2, _, _, _) -> compare c2 c1) |> List.map mk_value |> Cmd.of_list in diff --git a/bench/report/runs.ml b/bench/report/runs.ml index 56867b8a1..cfec01f47 100644 --- a/bench/report/runs.ml +++ b/bench/report/runs.ml @@ -83,11 +83,11 @@ let mean_stime runs = sum_stime runs /. (count_all runs |> float_of_int) let to_distribution ~max_time runs = List.init max_time (fun i -> - List.fold_left - (fun count r -> - let clock = Run.clock r |> int_of_float in - if clock = i then count +. 1. else count ) - 0. runs ) + List.fold_left + (fun count r -> + let clock = Run.clock r |> int_of_float in + if clock = i then count +. 1. else count ) + 0. runs ) let pp_quick_results fmt results = let nothing = ref 0 in @@ -118,8 +118,8 @@ let pp_table_results fmt results = Format.fprintf fmt "| Nothing | Reached | Timeout | Other | Killed | Total |@\n\ |:-------:|:-------:|:-------:|:-----:|:------:|:-----:|@\n\ - | %6i | %6i | %6i | %6i | %6i | %6i |" nothing reached timeout other killed - total + | %6i | %6i | %6i | %6i | %6i | %6i |" + nothing reached timeout other killed total let pp_table_statistics fmt results = let total = sum_clock results in diff --git a/bench/report/time_distribution.ml b/bench/report/time_distribution.ml index 643fbc67e..1924cb0a2 100644 --- a/bench/report/time_distribution.ml +++ b/bench/report/time_distribution.ml @@ -49,11 +49,12 @@ let make runs output_dir reference_name = let output = Gnuplot.Output.create (`Png - Fpath.( - output_dir - // v - (Format.sprintf "results_%s_time_distribution.png" reference_name) - |> to_string ) ) + Fpath.( + output_dir + // v + (Format.sprintf "results_%s_time_distribution.png" + reference_name ) + |> to_string ) ) in let range = Gnuplot.Range.X (min_time, float_of_int max_time) in diff --git a/example/define_host_function/life_game/runweb.ml b/example/define_host_function/life_game/runweb.ml index 028c2fcb4..c1e6b91dc 100644 --- a/example/define_host_function/life_game/runweb.ml +++ b/example/define_host_function/life_game/runweb.ml @@ -6,9 +6,9 @@ let asset_loader path = let () = let server = S.create ~port:8000 () in S.add_route_handler ~meth:`GET server S.Route.return (fun _req -> - S.Response.make_string - ~headers:[ ("Content-Type", "text/html") ] - (Ok (asset_loader "index.html")) ); + S.Response.make_string + ~headers:[ ("Content-Type", "text/html") ] + (Ok (asset_loader "index.html")) ); S.add_route_handler ~meth:`GET server S.Route.(exact "life_browser.js" @/ return) diff --git a/src/annot/contract.ml b/src/annot/contract.ml index 9a8b05878..0fb42c6d2 100644 --- a/src/annot/contract.ml +++ b/src/annot/contract.ml @@ -27,7 +27,8 @@ let pp_contract fmt { funcid; preconditions; postconditions } = Preconditions:@;\ <1 2>@[%a@]@,\ Postconditions:@;\ - <1 2>@[%a@]@]" pp_indice funcid + <1 2>@[%a@]@]" + pp_indice funcid (list ~sep:pp_newline pp_prop) preconditions (list ~sep:pp_newline pp_prop) diff --git a/src/ast/binary_encoder.ml b/src/ast/binary_encoder.ml index f029c525b..be4436a2a 100644 --- a/src/ast/binary_encoder.ml +++ b/src/ast/binary_encoder.ml @@ -663,8 +663,8 @@ let encode_imports buf (funcs, tables, memories, globals) = let encode_functions buf (funcs : binary func list) = let idx = ref 0 in encode_vector_list buf funcs (fun buf func -> - write_block_type_idx buf func.type_f; - incr idx ) + write_block_type_idx buf func.type_f; + incr idx ) (* table: section 4 *) let encode_tables buf tables = encode_vector_list buf tables write_table @@ -707,11 +707,11 @@ let encode_datacount buf datas = (* code: section 10 *) let encode_codes buf funcs = encode_vector_list buf funcs (fun buf { locals; body; _ } -> - let code_buf = Buffer.create 16 in - write_locals code_buf locals; - write_expr code_buf body ~end_op_code:None; - write_u32_of_int buf (Buffer.length code_buf); - Buffer.add_buffer buf code_buf ) + let code_buf = Buffer.create 16 in + write_locals code_buf locals; + write_expr code_buf body ~end_op_code:None; + write_u32_of_int buf (Buffer.length code_buf); + Buffer.add_buffer buf code_buf ) (* data: section 11 *) let encode_datas buf datas = encode_vector_array buf datas write_data diff --git a/src/ast/code_generator.ml b/src/ast/code_generator.ml index b2c3ade79..73beb18f5 100644 --- a/src/ast/code_generator.ml +++ b/src/ast/code_generator.ml @@ -573,11 +573,11 @@ let contract_generate (owi_funcs : (string * int) array) (m : modul) List.init (Array.length tenv.param_types) (fun i -> Local_get (Raw i)) @ [ Call (Raw old_index) ] @ List.init (Array.length tenv.result_types) (fun i -> - Local_set (tenv.result i) ) + Local_set (tenv.result i) ) in let return = List.init (Array.length tenv.result_types) (fun i -> - Local_get (tenv.result i) ) + Local_get (tenv.result i) ) in let* tenv, precond_checker = diff --git a/src/bin/owi.ml b/src/bin/owi.ml index 80e91dff1..940c75fe4 100644 --- a/src/bin/owi.ml +++ b/src/bin/owi.ml @@ -3,10 +3,9 @@ (* Written by the Owi programmers *) open Owi +open Cmdliner -let debug = - let doc = "debug mode" in - Cmdliner.Arg.(value & flag & info [ "debug"; "d" ] ~doc) +(* Helpers *) let existing_non_dir_file = let parse s = @@ -23,62 +22,69 @@ let dir_file = (parse, Fpath.pp) let solver_conv = - Cmdliner.Arg.conv + Arg.conv ( Smtml.Solver_dispatcher.solver_type_of_string , Smtml.Solver_dispatcher.pp_solver_type ) +(* Common options *) + +let copts_t = Term.(const []) + +let sdocs = Manpage.s_common_options + +let shared_man = [ `S Manpage.s_bugs; `P "Email them to ." ] + +let version = "%%VERSION%%" + +(* Common terms *) + +open Term.Syntax + +let debug = + let doc = "debug mode" in + Arg.(value & flag & info [ "debug"; "d" ] ~doc) + let deterministic_result_order = let doc = "Guarantee a fixed deterministic order of found failures. This implies \ --no-stop-at-failure." in - Cmdliner.Arg.(value & flag & info [ "deterministic-result-order" ] ~doc) + Arg.(value & flag & info [ "deterministic-result-order" ] ~doc) let files = let doc = "source files" in let f = existing_non_dir_file in - Cmdliner.Arg.(value & pos_all f [] (info [] ~doc)) + Arg.(value & pos_all f [] (info [] ~doc)) let sourcefile = let doc = "source file" in let f = existing_non_dir_file in - Cmdliner.Arg.(required & pos 0 (some f) None (info [] ~doc)) + Arg.(required & pos 0 (some f) None (info [] ~doc)) let outfile = let doc = "Write output to a file." in - let string_to_path = - Cmdliner.Arg.conv ~docv:"FILE" (Fpath.of_string, Fpath.pp) - in - Cmdliner.Arg.( + 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 ) -let emit_file = - let doc = "Emit (.wat) files from corresponding (.wasm) files." in - Cmdliner.Arg.(value & flag & info [ "emit-file" ] ~doc) - -let no_exhaustion = - let doc = "no exhaustion tests" in - Cmdliner.Arg.(value & flag & info [ "no-exhaustion" ] ~doc) - let no_stop_at_failure = let doc = "do not stop when a program failure is encountered" in - Cmdliner.Arg.(value & flag & info [ "no-stop-at-failure" ] ~doc) + Arg.(value & flag & info [ "no-stop-at-failure" ] ~doc) let no_values = let doc = "do not display a value for each symbol" in - Cmdliner.Arg.(value & flag & info [ "no-value" ] ~doc) + Arg.(value & flag & info [ "no-value" ] ~doc) let no_assert_failure_expression_printing = let doc = "do not display the expression in the assert failure" in - Cmdliner.Arg.( - value & flag & info [ "no-assert-failure-expression-printing" ] ~doc ) + Arg.(value & flag & info [ "no-assert-failure-expression-printing" ] ~doc) let fail_mode = let trap_doc = "ignore assertion violations and only report traps" in let assert_doc = "ignore traps and only report assertion violations" in - Cmdliner.Arg.( + Arg.( value & vflag `Both [ (`Trap_only, info [ "fail-on-trap-only" ] ~doc:trap_doc) @@ -87,233 +93,286 @@ let fail_mode = let optimize = let doc = "optimize mode" in - Cmdliner.Arg.(value & flag & info [ "optimize" ] ~doc) + Arg.(value & flag & info [ "optimize" ] ~doc) let profiling = let doc = "profiling mode" in - Cmdliner.Arg.(value & flag & info [ "profiling"; "p" ] ~doc) + Arg.(value & flag & info [ "profiling"; "p" ] ~doc) let rac = let doc = "runtime assertion checking mode" in - Cmdliner.Arg.(value & flag & info [ "rac" ] ~doc) + Arg.(value & flag & info [ "rac" ] ~doc) let srac = let doc = "symbolic runtime assertion checking mode" in - Cmdliner.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 - Cmdliner.Arg.(value & flag & info [ "e-acsl" ] ~doc) + Arg.(value & flag & info [ "srac" ] ~doc) let solver = let doc = "SMT solver to use" in - Cmdliner.Arg.( + 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 - Cmdliner.Arg.(value & flag & info [ "symbolic" ] ~doc) - let unsafe = let doc = "skip typechecking pass" in - Cmdliner.Arg.(value & flag & info [ "unsafe"; "u" ] ~doc) + Arg.(value & flag & info [ "unsafe"; "u" ] ~doc) let workers = let doc = "number of workers for symbolic execution. Defaults to the number of \ physical cores." in - Cmdliner.Arg.( + Arg.( value & opt int Processor.Query.core_count & info [ "workers"; "w" ] ~doc ~absent:"n" ) let workspace = let doc = "path to the workspace directory" in - Cmdliner.Arg.( - value & opt dir_file (Fpath.v "owi-out") & info [ "workspace" ] ~doc ) + Arg.(value & opt dir_file (Fpath.v "owi-out") & info [ "workspace" ] ~doc) -let copts_t = Cmdliner.Term.(const []) +(* owi c *) -let sdocs = Cmdliner.Manpage.s_common_options - -let shared_man = - [ `S Cmdliner.Manpage.s_bugs; `P "Email them to ." ] - -let version = "%%VERSION%%" +let c_info = + let doc = "Compile a C file to Wasm and run the symbolic interpreter on it" in + let man = [] @ shared_man in + Cmd.info "c" ~version ~doc ~sdocs ~man let c_cmd = - let open Cmdliner in - let info = - let doc = - "Compile a C file to Wasm and run the symbolic interpreter on it" - in - let man = [] @ shared_man in - Cmd.info "c" ~version ~doc ~sdocs ~man - in - let arch = + let+ arch = let doc = "data model" in Arg.(value & opt int 32 & info [ "arch"; "m" ] ~doc) - in - let property = + and+ property = let doc = "property file" in Arg.( value & opt (some existing_non_dir_file) None & info [ "property" ] ~doc ) - in - let includes = + and+ includes = let doc = "headers path" in Arg.(value & opt_all dir_file [] & info [ "I" ] ~doc) - in - let opt_lvl = + and+ opt_lvl = let doc = "specify which optimization level to use" in Arg.(value & opt string "3" & info [ "O" ] ~doc) - in - let testcomp = + and+ testcomp = let doc = "test-comp mode" in Arg.(value & flag & info [ "testcomp" ] ~doc) - in - let output = + and+ workspace = let doc = "write results to dir" in Arg.(value & opt string "owi-out" & info [ "output"; "o" ] ~doc) - in - let concolic = + and+ concolic = let doc = "concolic mode" in Arg.(value & flag & info [ "concolic" ] ~doc) - in - Cmd.v info - Term.( - const 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 ) + and+ debug + and+ workers + and+ files + and+ profiling + and+ unsafe + and+ optimize + and+ no_stop_at_failure + and+ no_values + and+ no_assert_failure_expression_printing + and+ deterministic_result_order + and+ fail_mode + 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 ~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 *) + +let fmt_info = + let doc = "Format a .wat or .wast file" in + let man = [] @ shared_man in + Cmd.info "fmt" ~version ~doc ~sdocs ~man let fmt_cmd = - let open Cmdliner in - let info = - let doc = "Format a .wat or .wast file" in - let man = [] @ shared_man in - Cmd.info "fmt" ~version ~doc ~sdocs ~man - in - let inplace = + let+ inplace = let doc = "Format in-place, overwriting input file" in - Cmdliner.Arg.(value & flag & info [ "inplace"; "i" ] ~doc) - in - Cmd.v info Term.(const Cmd_fmt.cmd $ inplace $ files) + Arg.(value & flag & info [ "inplace"; "i" ] ~doc) + and+ files in + Cmd_fmt.cmd ~inplace ~files + +(* owi opt *) + +let opt_info = + let doc = "Optimize a module" in + let man = [] @ shared_man in + Cmd.info "opt" ~version ~doc ~sdocs ~man let opt_cmd = - let open Cmdliner in - let info = - let doc = "Optimize a module" in - let man = [] @ shared_man in - Cmd.info "opt" ~version ~doc ~sdocs ~man + let+ debug + and+ unsafe + and+ sourcefile + and+ outfile in + Cmd_opt.cmd ~debug ~unsafe ~file:sourcefile ~outfile + +(* owi instrument *) + +let instrument_info = + let doc = + "Generate an instrumented file with runtime assertion checking coming from \ + Weasel specifications" in - Cmd.v info Term.(const Cmd_opt.cmd $ debug $ unsafe $ sourcefile $ outfile) + let man = [] @ shared_man in + Cmd.info "instrument" ~version ~doc ~sdocs ~man let instrument_cmd = - let open Cmdliner in - let info = + let+ debug + and+ unsafe + and+ symbolic = let doc = - "Generate an instrumented file with runtime assertion checking coming \ - from Weasel specifications" + "generate instrumented module that depends on symbolic execution" in - let man = [] @ shared_man in - Cmd.info "instrument" ~version ~doc ~sdocs ~man - in - Cmd.v info Term.(const Cmd_instrument.cmd $ debug $ unsafe $ symbolic $ files) + Arg.(value & flag & info [ "symbolic" ] ~doc) + and+ files in + Cmd_instrument.cmd ~debug ~unsafe ~symbolic ~files + +(* owi run *) + +let run_info = + let doc = "Run the concrete interpreter" in + let man = [] @ shared_man in + Cmd.info "run" ~version ~doc ~sdocs ~man let run_cmd = - let open Cmdliner in - let info = - let doc = "Run the concrete interpreter" in - let man = [] @ shared_man in - Cmd.info "run" ~version ~doc ~sdocs ~man - in - Cmd.v info - Term.( - const Cmd_run.cmd $ profiling $ debug $ unsafe $ rac $ optimize $ files ) + let+ profiling + and+ debug + and+ unsafe + and+ rac + and+ optimize + and+ files in + Cmd_run.cmd ~profiling ~debug ~unsafe ~rac ~optimize ~files + +(* owi validate *) + +let validate_info = + let doc = "Validate a module" in + let man = [] @ shared_man in + Cmd.info "validate" ~version ~doc ~sdocs ~man let validate_cmd = - let open Cmdliner in - let info = - let doc = "Validate a module" in - let man = [] @ shared_man in - Cmd.info "validate" ~version ~doc ~sdocs ~man - in - Cmd.v info Term.(const Cmd_validate.cmd $ debug $ files) + let+ debug + and+ files in + Cmd_validate.cmd ~debug ~files + +(* owi script *) + +let script_info = + let doc = "Run a reference test suite script" in + let man = [] @ shared_man in + Cmd.info "script" ~version ~doc ~sdocs ~man let script_cmd = - let open Cmdliner in - let info = - let doc = "Run a reference test suite script" in - let man = [] @ shared_man in - Cmd.info "script" ~version ~doc ~sdocs ~man + let+ profiling + and+ debug + and+ optimize + and+ files + and+ no_exhaustion = + let doc = "no exhaustion tests" in + Arg.(value & flag & info [ "no-exhaustion" ] ~doc) in - Cmd.v info - Term.( - const Cmd_script.cmd $ profiling $ debug $ optimize $ files - $ no_exhaustion ) + Cmd_script.cmd ~profiling ~debug ~optimize ~files ~no_exhaustion + +(* owi sym *) + +let sym_info = + let doc = "Run the symbolic interpreter" in + let man = [] @ shared_man in + Cmd.info "sym" ~version ~doc ~sdocs ~man let sym_cmd = - let open Cmdliner in - let info = - let doc = "Run the symbolic interpreter" in - let man = [] @ shared_man in - Cmd.info "sym" ~version ~doc ~sdocs ~man - in - Cmd.v info - Term.( - const 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 ) + let+ profiling + and+ debug + and+ unsafe + and+ rac + and+ srac + and+ optimize + and+ workers + and+ no_stop_at_failure + and+ no_values + and+ no_assert_failure_expression_printing + and+ deterministic_result_order + and+ fail_mode + 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 + +(* owi conc *) + +let conc_info = + let doc = "Run the concolic interpreter" in + let man = [] @ shared_man in + Cmd.info "conc" ~version ~doc ~sdocs ~man let conc_cmd = - let open Cmdliner in - let info = - let doc = "Run the concolic interpreter" in - let man = [] @ shared_man in - Cmd.info "conc" ~version ~doc ~sdocs ~man + let+ profiling + and+ debug + and+ unsafe + and+ rac + and+ srac + and+ optimize + and+ workers + and+ no_stop_at_failure + and+ no_values + and+ no_assert_failure_expression_printing + and+ deterministic_result_order + and+ fail_mode + 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 + +(* owi wasm2wat *) + +let wasm2wat_info = + let doc = + "Generate a text format file (.wat) from a binary format file (.wasm)" in - Cmd.v info - Term.( - const 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 ) + let man = [] @ shared_man in + Cmd.info "wasm2wat" ~version ~doc ~sdocs ~man let wasm2wat_cmd = - let open Cmdliner in - let info = - let doc = - "Generate a text format file (.wat) from a binary format file (.wasm)" - in - let man = [] @ shared_man in - Cmd.info "wasm2wat" ~version ~doc ~sdocs ~man + let+ sourcefile + 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 ~file:sourcefile ~emit_file ~outfile + +(* owi wat2wasm *) + +let wat2wasm_info = + let doc = + "Generate a binary format file (.wasm) from a text format file (.wat)" in - Cmd.v info Term.(const Cmd_wasm2wat.cmd $ sourcefile $ emit_file $ outfile) + let man = [] @ shared_man in + Cmd.info "wat2wasm" ~version ~doc ~sdocs ~man let wat2wasm_cmd = - let open Cmdliner in - let info = - let doc = - "Generate a binary format file (.wasm) from a text format file (.wat)" - in - let man = [] @ shared_man in - Cmd.info "wat2wasm" ~version ~doc ~sdocs ~man - in - Cmd.v info - Term.( - const Cmd_wat2wasm.cmd $ profiling $ debug $ unsafe $ optimize $ outfile - $ sourcefile ) + let+ profiling + and+ debug + and+ unsafe + and+ optimize + and+ outfile + and+ sourcefile in + Cmd_wat2wasm.cmd ~profiling ~debug ~unsafe ~optimize ~outfile ~file:sourcefile + +(* owi *) let cli = - let open Cmdliner in let info = let doc = "OCaml WebAssembly Interpreter" in let sdocs = Manpage.s_common_options in @@ -324,22 +383,22 @@ let cli = Term.(ret (const (fun (_ : _ list) -> `Help (`Plain, None)) $ copts_t)) in Cmd.group info ~default - [ c_cmd - ; fmt_cmd - ; opt_cmd - ; instrument_cmd - ; run_cmd - ; script_cmd - ; sym_cmd - ; conc_cmd - ; validate_cmd - ; wasm2wat_cmd - ; wat2wasm_cmd + [ Cmd.v c_info c_cmd + ; Cmd.v fmt_info fmt_cmd + ; Cmd.v opt_info opt_cmd + ; Cmd.v instrument_info instrument_cmd + ; Cmd.v run_info run_cmd + ; Cmd.v script_info script_cmd + ; Cmd.v sym_info sym_cmd + ; Cmd.v conc_info conc_cmd + ; Cmd.v validate_info validate_cmd + ; Cmd.v wasm2wat_info wasm2wat_cmd + ; Cmd.v wat2wasm_info wat2wasm_cmd ] let exit_code = - let open Cmdliner.Cmd.Exit in - match Cmdliner.Cmd.eval_value cli with + let open Cmd.Exit in + match Cmd.eval_value cli with | Ok (`Help | `Version) -> ok | Ok (`Ok result) -> begin match result with diff --git a/src/cmd/cmd_c.ml b/src/cmd/cmd_c.ml index b63549c65..1e16b0244 100644 --- a/src/cmd/cmd_c.ml +++ b/src/cmd/cmd_c.ml @@ -80,10 +80,10 @@ let eacsl_instrument eacsl debug ~includes (files : Fpath.t list) : | Error (`Msg e) -> Error (`Msg - (Fmt.str "Frama-C failed: %s" - ( if debug then e - else "run with --debug to get the full error message" ) ) - ) ) + (Fmt.str "Frama-C failed: %s" + ( if debug then e + else "run with --debug to get the full error message" ) ) + ) ) (List.combine files outs) in @@ -128,9 +128,9 @@ let compile ~includes ~opt_lvl debug (files : Fpath.t list) : Fpath.t Result.t = | Error (`Msg e) -> Error (`Msg - (Fmt.str "Clang failed: %s" - ( if debug then e - else "run with --debug to get the full error message" ) ) ) + (Fmt.str "Clang failed: %s" + ( if debug then e + else "run with --debug to get the full error message" ) ) ) in out @@ -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 bc860bb81..f3eff669c 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 87a022ee6..45b51a244 100644 --- a/src/cmd/cmd_conc.ml +++ b/src/cmd/cmd_conc.ml @@ -14,7 +14,7 @@ let print_paths = false let ( let** ) (t : 'a Result.t Choice.t) (f : 'a -> 'b Result.t Choice.t) : 'b Result.t Choice.t = Choice.bind t (fun t -> - match t with Error e -> Choice.return (Error e) | Ok x -> f x ) + match t with Error e -> Choice.return (Error e) | Ok x -> f x ) let simplify_then_link ~unsafe ~rac ~srac ~optimize link_state m = let* m = @@ -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 0a27652af..94c1a6b7a 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 9a846026a..93814aaee 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 433a95470..483add9a7 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 26f19eb26..e8d27d3bd 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 96aaaceb4..70b4138f0 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 df5ea1114..bc3dc53a1 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 74ce0a34d..965f9cb4d 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 d3e949f16..5bbc495a9 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 63aec0acf..5d8bd5959 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 30048a92c..3878cb3aa 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 fe2dd1058..d5850ede3 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 f06f2665f..4a6021ba8 100644 --- a/src/cmd/cmd_sym.ml +++ b/src/cmd/cmd_sym.ml @@ -40,15 +40,15 @@ let run_file ~unsafe ~rac ~srac ~optimize pc filename = let m = Symbolic.convert_module_to_run m in let c = Interpret.SymbolicP.modul link_state.envs m in Choice.bind pc (fun r -> - match r with Error _ -> Choice.return r | Ok () -> c ) + match r with Error _ -> Choice.return r | Ok () -> c ) (* NB: This function propagates potential errors (Result.err) occurring 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 *) @@ -80,7 +80,7 @@ let cmd profiling debug unsafe rac srac optimize workers no_stop_at_failure in let results = Wq.read_as_seq res_queue ~finalizer:(fun () -> - Array.iter Domain.join join_handles ) + Array.iter Domain.join join_handles ) in let print_bug = function | `ETrap (tr, model) -> @@ -123,7 +123,7 @@ let cmd profiling debug unsafe rac srac optimize workers no_stop_at_failure (x, List.rev @@ Thread_with_memory.breadcrumbs thread) ) |> List.of_seq |> List.sort (fun (_, bc1) (_, bc2) -> - List.compare Prelude.Int32.compare bc1 bc2 ) + List.compare Prelude.Int32.compare bc1 bc2 ) |> List.to_seq |> Seq.map fst else results in diff --git a/src/cmd/cmd_sym.mli b/src/cmd/cmd_sym.mli index cef789835..005960bfa 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_utils.ml b/src/cmd/cmd_utils.ml index 9f03d6f6b..bcce9c3c4 100644 --- a/src/cmd/cmd_utils.ml +++ b/src/cmd/cmd_utils.ml @@ -62,8 +62,8 @@ let add_main_as_start (m : Binary.modul) = | Ref_type (Types.No_null, t) -> Error (`Msg - (Fmt.str "can not create default value of type %a" - Types.pp_heap_type t ) ) + (Fmt.str "can not create default value of type %a" + Types.pp_heap_type t ) ) in let+ body = let pt, rt = snd main_type in diff --git a/src/cmd/cmd_validate.ml b/src/cmd/cmd_validate.ml index f5c12a614..17474af51 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 433a95470..f8db79782 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 379eedc04..4407f19e8 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 220d9b19a..b8b0f96f4 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 e820eadb2..4b9c65c50 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 43a9d5c20..a491c20e4 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 diff --git a/src/concolic/concolic_choice.ml b/src/concolic/concolic_choice.ml index a57afbc2f..22e41077b 100644 --- a/src/concolic/concolic_choice.ml +++ b/src/concolic/concolic_choice.ml @@ -91,8 +91,7 @@ let ( let+ ) = map let abort = M (fun st -> - (Ok (), { st with pc = Assume (Symbolic_value.Bool.const false) :: st.pc }) - ) + (Ok (), { st with pc = Assume (Symbolic_value.Bool.const false) :: st.pc }) ) let add_pc (c : Concolic_value.V.vbool) = M (fun st -> (Ok (), { st with pc = Assume c.symbolic :: st.pc })) diff --git a/src/concolic/concolic_wasm_ffi.ml b/src/concolic/concolic_wasm_ffi.ml index 289aaaf8f..b38792bc9 100644 --- a/src/concolic/concolic_wasm_ffi.ml +++ b/src/concolic/concolic_wasm_ffi.ml @@ -20,71 +20,71 @@ module M : let symbol_i32 () : Value.int32 Choice.t = Choice.with_new_symbol (Ty_bitv 32) (fun sym forced_value -> - let n = - match forced_value with - | None -> Random.bits32 () - | Some (Num (I32 n)) -> n - | _ -> assert false - in - (I32 n, Value.pair n (Expr.symbol sym)) ) + let n = + match forced_value with + | None -> Random.bits32 () + | Some (Num (I32 n)) -> n + | _ -> assert false + in + (I32 n, Value.pair n (Expr.symbol sym)) ) let symbol_i8 () : Value.int32 Choice.t = Choice.with_new_symbol (Ty_bitv 32) (fun sym forced_value -> - let n = - match forced_value with - | None -> Int32.logand 0xFFl (Random.bits32 ()) - | Some (Num (I32 n)) -> n - | _ -> assert false - in - let sym_expr = - Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) - in - (I32 n, Value.pair n sym_expr) ) + let n = + match forced_value with + | None -> Int32.logand 0xFFl (Random.bits32 ()) + | Some (Num (I32 n)) -> n + | _ -> assert false + in + let sym_expr = + Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) + in + (I32 n, Value.pair n sym_expr) ) let symbol_char () : Value.int32 Choice.t = Choice.with_new_symbol (Ty_bitv 32) (fun sym forced_value -> - let n = - match forced_value with - | None -> Int32.logand 0xFFl (Random.bits32 ()) - | Some (Num (I32 n)) -> n - | _ -> assert false - in - let sym_expr = - Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) - in - (I32 n, Value.pair n sym_expr) ) + let n = + match forced_value with + | None -> Int32.logand 0xFFl (Random.bits32 ()) + | Some (Num (I32 n)) -> n + | _ -> assert false + in + let sym_expr = + Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) + in + (I32 n, Value.pair n sym_expr) ) let symbol_i64 () : Value.int64 Choice.t = Choice.with_new_symbol (Ty_bitv 64) (fun sym forced_value -> - let n = - match forced_value with - | None -> Random.bits64 () - | Some (Num (I64 n)) -> n - | _ -> assert false - in - (I64 n, Value.pair n (Expr.symbol sym)) ) + let n = + match forced_value with + | None -> Random.bits64 () + | Some (Num (I64 n)) -> n + | _ -> assert false + in + (I64 n, Value.pair n (Expr.symbol sym)) ) let symbol_f32 () : Value.float32 Choice.t = Choice.with_new_symbol (Ty_fp 32) (fun sym forced_value -> - let n = - match forced_value with - | None -> Random.bits32 () - | Some (Num (F32 n)) -> n - | _ -> assert false - in - let n = Float32.of_bits n in - (F32 n, Value.pair n (Expr.symbol sym)) ) + let n = + match forced_value with + | None -> Random.bits32 () + | Some (Num (F32 n)) -> n + | _ -> assert false + in + let n = Float32.of_bits n in + (F32 n, Value.pair n (Expr.symbol sym)) ) let symbol_f64 () : Value.float64 Choice.t = Choice.with_new_symbol (Ty_fp 64) (fun sym forced_value -> - let n = - match forced_value with - | None -> Random.bits64 () - | Some (Num (F64 n)) -> n - | _ -> assert false - in - let n = Float64.of_bits n in - (F64 n, Value.pair n (Expr.symbol sym)) ) + let n = + match forced_value with + | None -> Random.bits64 () + | Some (Num (F64 n)) -> n + | _ -> assert false + in + let n = Float64.of_bits n in + (F64 n, Value.pair n (Expr.symbol sym)) ) let assume_i32 (i : Value.int32) : unit Choice.t = let c = Value.I32.to_bool i in @@ -127,10 +127,10 @@ module M : let alloc _ (base : Value.int32) (_size : Value.int32) : Value.int32 Choice.t = Choice.bind (i32 base) (fun (base : int32) -> - Choice.return - { Concolic_value.concrete = base - ; symbolic = Expr.ptr base (Symbolic_value.const_i32 0l) - } ) + Choice.return + { Concolic_value.concrete = base + ; symbolic = Expr.ptr base (Symbolic_value.const_i32 0l) + } ) let free _ (p : Value.int32) = (* WHAT ???? *) diff --git a/src/data_structures/named.ml b/src/data_structures/named.ml index 0a1b9b988..50e30fb10 100644 --- a/src/data_structures/named.ml +++ b/src/data_structures/named.ml @@ -28,4 +28,4 @@ let to_array v = if Hashtbl.mem tbl i then assert false else Hashtbl.add tbl i v ) v.values; Array.init (List.length v.values) (fun i -> - match Hashtbl.find_opt tbl i with None -> assert false | Some v -> v ) + match Hashtbl.find_opt tbl i with None -> assert false | Some v -> v ) diff --git a/src/interpret/interpret.ml b/src/interpret/interpret.ml index 7cb8efe6d..54bdd8a26 100644 --- a/src/interpret/interpret.ml +++ b/src/interpret/interpret.ml @@ -501,8 +501,8 @@ module Make (P : Interpret_intf.P) : | Type_mismatch -> Choice.trap Trap.Extern_call_arg_type_mismatch | Null -> Choice.trap Trap.Extern_call_null_arg ) in - let rec split_args : - type f r. Stack.t -> (f, r) Extern_func.atype -> Stack.t * Stack.t = + let rec split_args : type f r. + Stack.t -> (f, r) Extern_func.atype -> Stack.t * Stack.t = fun stack ty -> let[@local] split_one_arg args = let elt, stack = Stack.pop stack in @@ -516,8 +516,8 @@ module Make (P : Interpret_intf.P) : | NArg (_, _, args) -> split_one_arg args | Res -> ([], stack) in - let rec apply : - type f r. Stack.t -> (f, r) Extern_func.atype -> f -> r Choice.t = + let rec apply : type f r. + Stack.t -> (f, r) Extern_func.atype -> f -> r Choice.t = fun stack ty f -> match ty with | Mem args -> @@ -635,7 +635,7 @@ module Make (P : Interpret_intf.P) : List.sort (fun ((Raw id1 : binary indice), _) ((Raw id2 : binary indice), _) -> - compare id1 id2 ) + compare id1 id2 ) @@ List.of_seq @@ Hashtbl.to_seq tbl in match l with diff --git a/src/primitives/int64.ml b/src/primitives/int64.ml index e380a036f..b843e1c56 100644 --- a/src/primitives/int64.ml +++ b/src/primitives/int64.ml @@ -42,8 +42,8 @@ let popcnt = (x * h01) lsr 56 (* - * Unsigned comparison in terms of signed comparison. - *) + * Unsigned comparison in terms of signed comparison. + *) let cmp_u x op y = op (add x min_int) (add y min_int) let eq (x : int64) y = equal x y diff --git a/src/symbolic/symbolic.ml b/src/symbolic/symbolic.ml index aab9ecc96..29ee747ae 100644 --- a/src/symbolic/symbolic.ml +++ b/src/symbolic/symbolic.ml @@ -5,9 +5,10 @@ module MakeP (Memory : Symbolic_memory_intf.S) (Thread : Thread.S with type Memory.collection = Memory.collection) - (Choice : Choice_intf.Complete - with module V := Symbolic_value - and type thread := Thread.t) = + (Choice : + Choice_intf.Complete + with module V := Symbolic_value + and type thread := Thread.t) = struct module Value = Symbolic_value module Choice = Choice diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml index 55e81ccf6..18217f6b4 100644 --- a/src/symbolic/symbolic_choice.ml +++ b/src/symbolic/symbolic_choice.ml @@ -102,15 +102,15 @@ module CoreImpl = struct let spawn_worker sched wls_init callback callback_init callback_close = callback_init (); Domain.spawn (fun () -> - Fun.protect - ~finally:(fun () -> callback_close ()) - (fun () -> - let wls = wls_init () in - try work wls sched callback - with e -> - let bt = Printexc.get_raw_backtrace () in - Wq.fail sched.work_queue; - Printexc.raise_with_backtrace e bt ) ) + Fun.protect + ~finally:(fun () -> callback_close ()) + (fun () -> + let wls = wls_init () in + try work wls sched callback + with e -> + let bt = Printexc.get_raw_backtrace () in + Wq.fail sched.work_queue; + Printexc.raise_with_backtrace e bt ) ) end module State = struct @@ -307,8 +307,8 @@ module CoreImpl = struct let sched = init_scheduler () in add_init_task sched (State.run t thread); Array.init workers (fun _i -> - spawn_worker sched (Solver.fresh solver) callback callback_init - callback_end ) + spawn_worker sched (Solver.fresh solver) callback callback_init + callback_end ) let trap t = let* thread in @@ -348,8 +348,8 @@ module Make (Thread : Thread.S) = struct let sym = Fmt.kstr (Smtml.Symbol.make ty) "symbol_%d" n in let+ () = modify_thread (fun thread -> - let thread = Thread.add_symbol thread sym in - Thread.incr_symbols thread ) + let thread = Thread.add_symbol thread sym in + Thread.incr_symbols thread ) in f sym diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml index 26a047bc4..90b08c9e8 100644 --- a/src/symbolic/symbolic_wasm_ffi.ml +++ b/src/symbolic/symbolic_wasm_ffi.ml @@ -29,11 +29,11 @@ module M : let symbol_i8 () = Choice.with_new_symbol (Ty_bitv 8) (fun sym -> - Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) ) + Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) ) let symbol_char () = Choice.with_new_symbol (Ty_bitv 8) (fun sym -> - Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) ) + Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) ) let symbol_i32 () = Choice.with_new_symbol (Ty_bitv 32) Expr.symbol diff --git a/src/text_to_binary/rewrite.ml b/src/text_to_binary/rewrite.ml index c8b871fce..373156a28 100644 --- a/src/text_to_binary/rewrite.ml +++ b/src/text_to_binary/rewrite.ml @@ -28,7 +28,9 @@ let find (named : 'a Named.t) : _ -> binary indice = function let get error (named : 'a Named.t) indice : 'a Indexed.t Result.t = let (Raw i) = find named indice in (* TODO change Named.t structure to make that sensible *) - match List.nth_opt named.values i with None -> Error error | Some v -> Ok v + match List.nth_opt named.values i with + | None -> Error error + | Some v -> Ok v let find_global (modul : Assigned.t) id : binary indice = find modul.global id @@ -92,8 +94,7 @@ let rewrite_expr (typemap : binary indice TypeMap.t) (modul : Assigned.t) | None -> Ok (locals, next_free_int + 1) | Some name -> if String_map.mem name locals then Error (`Duplicate_local name) - else Ok (String_map.add name next_free_int locals, next_free_int + 1) - ) + else Ok (String_map.add name next_free_int locals, next_free_int + 1) ) (String_map.empty, 0) locals in diff --git a/src/utils/syntax.ml b/src/utils/syntax.ml index 82ba5391c..bf5c822de 100644 --- a/src/utils/syntax.ml +++ b/src/utils/syntax.ml @@ -87,12 +87,12 @@ let array_map f a = try ok @@ Array.init (Array.length a) (fun i -> - let v = Array.get a i in - match f v with - | Error _e as e -> - err := Some e; - raise Exit - | Ok v -> v ) + let v = Array.get a i in + match f v with + | Error _e as e -> + err := Some e; + raise Exit + | Ok v -> v ) with Exit -> Option.get !err let array_fold_left f acc l = diff --git a/src/utils/tracing.ml b/src/utils/tracing.ml index 0c6b9fc4c..8ac2ff5b4 100644 --- a/src/utils/tracing.ml +++ b/src/utils/tracing.ml @@ -29,4 +29,4 @@ let model = let with_ev ev f = Runtime_events.User.write ev Runtime_events.Type.Begin; Fun.protect f ~finally:(fun () -> - Runtime_events.User.write ev Runtime_events.Type.End ) + Runtime_events.User.write ev Runtime_events.Type.End ) diff --git a/src/validate/binary_validate.ml b/src/validate/binary_validate.ml index 0c0505f1b..48b9ae1b7 100644 --- a/src/validate/binary_validate.ml +++ b/src/validate/binary_validate.ml @@ -560,8 +560,8 @@ and typecheck_expr env expr ~is_loop (block_type : binary block_type option) | None -> Error (`Type_mismatch - (Fmt.str "expected a prefix of %a but stack has type %a" Stack.pp pt - Stack.pp previous_stack ) ) + (Fmt.str "expected a prefix of %a but stack has type %a" Stack.pp pt + Stack.pp previous_stack ) ) | Some stack_to_push -> Stack.push rt stack_to_push let typecheck_function (modul : modul) func refs = diff --git a/test/fuzz/basic.ml b/test/fuzz/basic.ml index a2fcf0cc7..7cb2247c5 100644 --- a/test/fuzz/basic.ml +++ b/test/fuzz/basic.ml @@ -21,7 +21,10 @@ let heap_type : text heap_type Crowbar.gen = const Func_ht let ref_type = pair nullable heap_type let limits = - let sup = if true then 10 else 100000 (* TODO: fix max size ? *) in + let sup = + if true then 10 else 100000 + (* TODO: fix max size ? *) + in let* min = range sup in let+ max = option (range ~min (sup - min)) in { min; max } @@ -288,8 +291,7 @@ let global ntyp env = let globals = Env.get_globals ntyp env ~only_mut:false in List.map (fun (name, (_, _)) -> - pair (const (Global_get (Text name))) (const [ S.Push (Num_type ntyp) ]) - ) + pair (const (Global_get (Text name))) (const [ S.Push (Num_type ntyp) ]) ) globals let global_i32 env = global I32 env diff --git a/test/fuzz/fuzzer.ml b/test/fuzz/fuzzer.ml index fb16dec53..9b38e360a 100644 --- a/test/fuzz/fuzzer.ml +++ b/test/fuzz/fuzzer.ml @@ -74,13 +74,13 @@ let check (module I1 : Interprets.INTERPRET) (module I2 : Interprets.INTERPRET) let add_test name gen (module I1 : Interprets.INTERPRET) (module I2 : Interprets.INTERPRET) = Crowbar.add_test ~name [ gen ] (fun m -> - incr global_count; - if Param.debug then Fmt.epr "%a@\n" Owi.Text.pp_modul m; - Fmt.epr "test module %d [got %d timeouts...]@\n@[" !global_count - !timeout_count; - Fmt.flush Fmt.stderr (); - Crowbar.check (check (module I1) (module I2) m); - Fmt.epr "@]" ) + incr global_count; + if Param.debug then Fmt.epr "%a@\n" Owi.Text.pp_modul m; + Fmt.epr "test module %d [got %d timeouts...]@\n@[" !global_count + !timeout_count; + Fmt.flush Fmt.stderr (); + Crowbar.check (check (module I1) (module I2) m); + Fmt.epr "@]" ) let gen (conf : Env.conf) = Crowbar.with_printer Owi.Text.pp_modul (Gen.modul conf) diff --git a/test/fuzz/interprets.ml b/test/fuzz/interprets.ml index 06174cfcb..053199670 100644 --- a/test/fuzz/interprets.ml +++ b/test/fuzz/interprets.ml @@ -27,8 +27,8 @@ let set = let timeout_call_run (run : unit -> unit Result.t) : 'a Result.t = try Fun.protect ~finally:unset (fun () -> - set (); - try run () with Timeout -> Error `Timeout ) + set (); + try run () with Timeout -> Error `Timeout ) with Timeout -> Error `Timeout module Owi_unoptimized : INTERPRET = struct @@ -45,7 +45,7 @@ module Owi_unoptimized : INTERPRET = struct Link.modul Link.empty_state ~name:None simplified in timeout_call_run (fun () -> - Interpret.Concrete.modul link_state.envs regular ) + Interpret.Concrete.modul link_state.envs regular ) let name = "owi" end @@ -65,7 +65,7 @@ module Owi_optimized : INTERPRET = struct Link.modul Link.empty_state ~name:None simplified in timeout_call_run (fun () -> - Interpret.Concrete.modul link_state.envs regular ) + Interpret.Concrete.modul link_state.envs regular ) let name = "owi+optimize" end @@ -87,16 +87,16 @@ module Owi_symbolic : INTERPRET = struct in let regular = Symbolic.convert_module_to_run_minimalist regular in timeout_call_run (fun () -> - let c = Interpret.SymbolicM.modul link_state.envs regular in - let init_thread = Thread_with_memory.init () in - let res, _ = - Symbolic_choice_minimalist.run ~workers:dummy_workers_count - Smtml.Solver_dispatcher.Z3_solver c init_thread - in - match res with - | Ok res -> res - | Error (Trap t) -> Error (`Trap t) - | Error Assert_fail -> Error `Assert_failure ) + let c = Interpret.SymbolicM.modul link_state.envs regular in + let init_thread = Thread_with_memory.init () in + let res, _ = + Symbolic_choice_minimalist.run ~workers:dummy_workers_count + Smtml.Solver_dispatcher.Z3_solver c init_thread + in + match res with + | Ok res -> res + | Error (Trap t) -> Error (`Trap t) + | Error Assert_fail -> Error `Assert_failure ) let name = "owi_symbolic" end