Add and use a new compilation API

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

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

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
 

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