From 7bbe8d75fdb6c76079d584da9ff5b15ab98a0e56 Mon Sep 17 00:00:00 2001 From: Arthur Carcano Date: Wed, 10 Jul 2024 14:26:54 +0200 Subject: [PATCH] Add and use a new compilation API --- src/ast/compile.ml | 42 +++++++++++++++++++++++++++++++++ src/ast/compile.mli | 27 +++++++++++++++++++++ src/cmd/cmd_conc.ml | 57 ++++++++++----------------------------------- src/cmd/cmd_sym.ml | 54 +++++++++++++----------------------------- 4 files changed, 97 insertions(+), 83 deletions(-) diff --git a/src/ast/compile.ml b/src/ast/compile.ml index 682678b40..f4bc2f59a 100644 --- a/src/ast/compile.ml +++ b/src/ast/compile.ml @@ -67,3 +67,45 @@ module Binary = struct let+ () = Interpret.Concrete.modul link_state.envs m in link_state end + +module ApiV2 = struct + type 'a t = + 'a Link.module_to_run list * 'a Link.state + -> ('a Link.module_to_run list * 'a Link.state) Result.t + + let start_compilation = Ok ([], Link.empty_state) + + let extern_module ~func_typ ~name ~module_impl (modules_to_run, state) = + let state = Link.extern_module' state ~name ~func_typ module_impl in + Ok (modules_to_run, state) + + let file ~filename ~unsafe ~optimize ~add_main_as_start (modules_to_run, state) + = + let* m = Parse.guess_from_file filename in + let* m = + match m with + | Either.Left (Either.Left text_module) -> + Text.until_binary ~unsafe text_module + | Either.Left (Either.Right _text_scrpt) -> + Error (`Msg "Wasm script is not supported by this API.") + | Either.Right binary_module -> Ok binary_module + in + let* m = + if add_main_as_start then Cmd_utils.add_main_as_start m else Ok m + in + let name = filename |> Fpath.rem_ext |> Fpath.filename |> Option.some in + let+ m_to_run, state = Binary.until_link ~unsafe ~name ~optimize state m in + (m_to_run :: modules_to_run, state) + + let files ~filenames ~unsafe ~optimize ~add_main_as_start init = + List.fold_left + (fun acc filename -> + Result.bind acc (file ~filename ~unsafe ~optimize ~add_main_as_start) ) + (Ok init) filenames + + let finish (modules_to_run, state) = Ok (List.rev modules_to_run, state) + + let compile l = + let* x = List.fold_left Result.bind start_compilation l in + finish x +end diff --git a/src/ast/compile.mli b/src/ast/compile.mli index b16e6ddb1..7505f65b0 100644 --- a/src/ast/compile.mli +++ b/src/ast/compile.mli @@ -61,3 +61,30 @@ module Binary : sig -> Binary.modul -> Concrete_value.Func.extern_func Link.state Result.t end + +module ApiV2 : sig + type 'a t + + val extern_module : + func_typ:('a -> Types.binary Types.func_type) + -> name:string + -> module_impl:'a Link.extern_module + -> 'a t + + val file : + filename:Fpath.t + -> unsafe:bool + -> optimize:bool + -> add_main_as_start:bool + -> 'a t + + val files : + filenames:Fpath.t list + -> unsafe:bool + -> optimize:bool + -> add_main_as_start:bool + -> 'a t + + val compile : + 'a t list -> ('a Link.module_to_run list * 'a Link.state) Result.t +end diff --git a/src/cmd/cmd_conc.ml b/src/cmd/cmd_conc.ml index 0b2867bff..0b19d6273 100644 --- a/src/cmd/cmd_conc.ml +++ b/src/cmd/cmd_conc.ml @@ -15,48 +15,6 @@ let ( let** ) (t : 'a Result.t Choice.t) (f : 'a -> 'b Result.t Choice.t) : Choice.bind t (fun t -> match t with Error e -> Choice.return (Error e) | Ok x -> f x ) -let simplify_then_link ~unsafe ~optimize link_state m = - let* m = - match m with - | Either.Left (Either.Left text_module) -> - Compile.Text.until_binary ~unsafe text_module - | Either.Left (Either.Right _text_scrpt) -> - Error (`Msg "can't run concolic interpreter on a script") - | Either.Right binary_module -> Ok binary_module - in - let* m = Cmd_utils.add_main_as_start m in - let+ m, link_state = - Compile.Binary.until_link ~unsafe link_state ~optimize ~name:None m - in - let module_to_run = Concolic.convert_module_to_run m in - (link_state, module_to_run) - -let simplify_then_link_files ~unsafe ~optimize filenames = - let link_state = Link.empty_state in - let link_state = - Link.extern_module' link_state ~name:"symbolic" - ~func_typ:Concolic.P.Extern_func.extern_type - Concolic_wasm_ffi.symbolic_extern_module - in - let link_state = - Link.extern_module' link_state ~name:"summaries" - ~func_typ:Concolic.P.Extern_func.extern_type - Concolic_wasm_ffi.summaries_extern_module - in - let+ link_state, modules_to_run = - List.fold_left - (fun (acc : (_ * _) Result.t) filename -> - let* link_state, modules_to_run = acc in - let* m0dule = Parse.guess_from_file filename in - let+ link_state, module_to_run = - simplify_then_link ~unsafe ~optimize link_state m0dule - in - (link_state, module_to_run :: modules_to_run) ) - (Ok (link_state, [])) - filenames - in - (link_state, List.rev modules_to_run) - let run_modules_to_run (link_state : _ Link.state) modules_to_run = List.fold_left (fun (acc : unit Result.t Concolic.P.Choice.t) to_run -> @@ -403,7 +361,7 @@ let launch solver tree link_state modules_to_run = which are handled here. Most of the computations are done in the Result monad, hence the let*. *) let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values - deterministic_result_order (workspace : Fpath.t) solver files = + deterministic_result_order (workspace : Fpath.t) solver filenames = ignore (workers, no_stop_at_failure, deterministic_result_order, workspace); if profiling then Log.profiling_on := true; @@ -413,9 +371,18 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values (* let no_stop_at_failure = deterministic_result_order || no_stop_at_failure in *) let* _created_dir = Bos.OS.Dir.create ~path:true ~mode:0o755 workspace in let solver = Solver.fresh solver () in - let* link_state, modules_to_run = - simplify_then_link_files ~unsafe ~optimize files + let func_typ = Concolic.P.Extern_func.extern_type in + let* modules_to_run, link_state = + Compile.ApiV2.( + compile + [ extern_module ~name:"symbolic" ~func_typ + ~module_impl:Concolic_wasm_ffi.symbolic_extern_module + ; extern_module ~name:"summaries" ~func_typ + ~module_impl:Concolic_wasm_ffi.summaries_extern_module + ; files ~filenames ~unsafe ~optimize ~add_main_as_start:true + ] ) in + let modules_to_run = List.map Concolic.convert_module_to_run modules_to_run in let tree = fresh_tree [] in let result = launch solver tree link_state modules_to_run in diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml index 1c916a308..e0a5c219d 100644 --- a/src/cmd/cmd_sym.ml +++ b/src/cmd/cmd_sym.ml @@ -6,58 +6,36 @@ open Syntax module Expr = Smtml.Expr module Choice = Symbolic.P.Choice -let ( let*/ ) (t : 'a Result.t) (f : 'a -> 'b Result.t Choice.t) : - 'b Result.t Choice.t = - match t with Error e -> Choice.return (Error e) | Ok x -> f x - -let link_state = - lazy - (let func_typ = Symbolic.P.Extern_func.extern_type in - let link_state = - Link.extern_module' Link.empty_state ~name:"symbolic" ~func_typ - Symbolic_wasm_ffi.symbolic_extern_module - in - Link.extern_module' link_state ~name:"summaries" ~func_typ - Symbolic_wasm_ffi.summaries_extern_module ) - -let run_binary_modul ~unsafe ~optimize (pc : unit Result.t Choice.t) - (m : Binary.modul) = - let*/ m = Cmd_utils.add_main_as_start m in - let link_state = Lazy.force link_state in - - let*/ m, link_state = - Compile.Binary.until_link ~unsafe link_state ~optimize ~name:None m - in - let m = Symbolic.convert_module_to_run m in - let c = Interpret.SymbolicP.modul link_state.envs m in +let run_modul link_output (pc : unit Result.t Choice.t) module_to_run = + let m = Symbolic.convert_module_to_run module_to_run in + let c = Interpret.SymbolicP.modul link_output.Link.envs m in Choice.bind pc (fun r -> match r with Error _ -> Choice.return r | Ok () -> c ) -let run_file ~unsafe ~optimize pc filename = - let*/ m = Parse.guess_from_file filename in - let*/ m = - match m with - | Either.Left (Either.Left text_module) -> - Compile.Text.until_binary ~unsafe text_module - | Either.Left (Either.Right _text_scrpt) -> - Error (`Msg "can't run symbolic interpreter on a script") - | Either.Right binary_module -> Ok binary_module - in - run_binary_modul ~unsafe ~optimize pc m - (* 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 optimize workers no_stop_at_failure no_values - deterministic_result_order (workspace : Fpath.t) solver files = + deterministic_result_order (workspace : Fpath.t) solver filenames = if profiling then Log.profiling_on := true; if debug then Log.debug_on := true; (* deterministic_result_order implies no_stop_at_failure *) let no_stop_at_failure = deterministic_result_order || no_stop_at_failure in let* _created_dir = Bos.OS.Dir.create ~path:true ~mode:0o755 workspace in + let func_typ = Symbolic.P.Extern_func.extern_type in + let* modules_to_run, link_output = + Compile.ApiV2.( + compile + [ extern_module ~name:"symbolic" ~func_typ + ~module_impl:Symbolic_wasm_ffi.symbolic_extern_module + ; extern_module ~name:"summaries" ~func_typ + ~module_impl:Symbolic_wasm_ffi.summaries_extern_module + ; files ~filenames ~unsafe ~optimize ~add_main_as_start:true + ] ) + in let pc = Choice.return (Ok ()) in - let result = List.fold_left (run_file ~unsafe ~optimize) pc files in + let result = List.fold_left (run_modul link_output) pc modules_to_run in let thread : Thread.t = Thread.create () in let res_queue = Wq.init () in let callback = function