Proper start and entry point handling

src/ast/compile.ml

@@ -23,90 +23,67 @@ module Text = struct
     else if rac then Code_generator.generate false m
     else Ok m
 
-  let until_binary_validate ~unsafe ~rac ~srac m =
+  let until_validate ~unsafe ~rac ~srac m =
     let* m = until_binary ~unsafe ~rac ~srac m in
     if unsafe then Ok m
     else
       let+ () = Binary_validate.modul m in
       m
 
   let until_optimize ~unsafe ~rac ~srac ~optimize m =
-    let+ m = until_binary_validate ~unsafe ~rac ~srac m in
+    let+ m = until_validate ~unsafe ~rac ~srac m in
     if optimize then Optimize.modul m else m
 
   let until_link ~unsafe ~rac ~srac ~optimize ~name link_state m =
     let* m = until_optimize ~unsafe ~rac ~srac ~optimize m in
     Link.modul link_state ~name m
-
-  let until_interpret ~unsafe ~timeout ~timeout_instr ~rac ~srac ~optimize ~name
-    link_state m =
-    let* m, link_state =
-      until_link ~unsafe ~rac ~srac ~optimize ~name link_state m
-    in
-    let+ () =
-      Interpret.Concrete.modul ~timeout ~timeout_instr link_state.envs m
-    in
-    link_state
 end
 
 module Binary = struct
-  let until_binary_validate ~unsafe m =
+  let until_validate ~unsafe m =
     if unsafe then Ok m
     else
       let+ () = Binary_validate.modul m in
       m
 
   let until_optimize ~unsafe ~optimize m =
-    let+ m = until_binary_validate ~unsafe m in
+    let+ m = until_validate ~unsafe m in
     if optimize then Optimize.modul m else m
 
   let until_link ~unsafe ~optimize ~name link_state m =
     let* m = until_optimize ~unsafe ~optimize m in
     Link.modul link_state ~name m
-
-  let until_interpret ~unsafe ~timeout ~timeout_instr ~optimize ~name link_state
-    m =
-    let* m, link_state = until_link ~unsafe ~optimize ~name link_state m in
-    let+ () =
-      Interpret.Concrete.modul ~timeout ~timeout_instr link_state.envs m
-    in
-    link_state
 end
 
 module Any = struct
-  let until_binary_validate ~unsafe ~rac ~srac = function
-    | Kind.Wat m -> Text.until_binary_validate ~unsafe ~rac ~srac m
-    | Wasm m -> Binary.until_binary_validate ~unsafe m
-    | Wast _ | Ocaml _ -> assert false
+  let until_validate ~unsafe ~rac ~srac = function
+    | Kind.Wat m -> Text.until_validate ~unsafe ~rac ~srac m
+    | Wasm m -> Binary.until_validate ~unsafe m
+    | Wast _ -> Fmt.error_msg "can not validate a .wast file"
+    | Ocaml _ -> Fmt.error_msg "can not validate an OCaml module"
 
   let until_optimize ~unsafe ~rac ~srac ~optimize = function
     | Kind.Wat m -> Text.until_optimize ~unsafe ~rac ~srac ~optimize m
     | Wasm m -> Binary.until_optimize ~unsafe ~optimize m
-    | Wast _ | Ocaml _ -> assert false
+    | Wast _ -> Fmt.error_msg "can not optimize a .wast file"
+    | Ocaml _ -> Fmt.error_msg "can not optimize an OCaml module"
 
   let until_link ~unsafe ~rac ~srac ~optimize ~name link_state = function
     | Kind.Wat m ->
       Text.until_link ~unsafe ~rac ~srac ~optimize ~name link_state m
     | Wasm m -> Binary.until_link ~unsafe ~optimize ~name link_state m
-    | Wast _ | Ocaml _ -> assert false
-
-  let until_interpret ~unsafe ~timeout ~timeout_instr ~rac ~srac ~optimize ~name
-    link_state = function
-    | Kind.Wat m ->
-      Text.until_interpret ~unsafe ~timeout ~timeout_instr ~rac ~srac ~optimize
-        ~name link_state m
-    | Wasm m ->
-      Binary.until_interpret ~unsafe ~timeout ~timeout_instr ~optimize ~name
-        link_state m
-    | Wast _ | Ocaml _ -> assert false
+    | Ocaml _m ->
+      (* TODO: we may be able to handle linking here but return an empty runnable module ? *)
+      Fmt.error_msg "can not link an OCaml module"
+    | Wast _ -> Fmt.error_msg "can not link a .wast file"
 end
 
 module File = struct
-  let until_binary_validate ~unsafe ~rac ~srac filename =
+  let until_validate ~unsafe ~rac ~srac filename =
     let* m = Parse.guess_from_file filename in
     match m with
-    | Kind.Wat m -> Text.until_binary_validate ~unsafe ~rac ~srac m
-    | Wasm m -> Binary.until_binary_validate ~unsafe m
+    | Kind.Wat m -> Text.until_validate ~unsafe ~rac ~srac m
+    | Wasm m -> Binary.until_validate ~unsafe m
     | Wast _ | Ocaml _ -> assert false
 
   let until_optimize ~unsafe ~rac ~srac ~optimize filename =
@@ -123,16 +100,4 @@ module File = struct
       Text.until_link ~unsafe ~rac ~srac ~optimize ~name link_state m
     | Wasm m -> Binary.until_link ~unsafe ~optimize ~name link_state m
     | Wast _ | Ocaml _ -> assert false
-
-  let until_interpret ~unsafe ~timeout ~timeout_instr ~rac ~srac ~optimize ~name
-    link_state filename =
-    let* m = Parse.guess_from_file filename in
-    match m with
-    | Kind.Wat m ->
-      Text.until_interpret ~unsafe ~timeout ~timeout_instr ~rac ~srac ~optimize
-        ~name link_state m
-    | Wasm m ->
-      Binary.until_interpret ~unsafe ~timeout ~timeout_instr ~optimize ~name
-        link_state m
-    | Wast _ | Ocaml _ -> assert false
 end

src/ast/compile.mli

@@ -5,7 +5,7 @@
 (** Utility functions to compile a module until a given step. *)
 
 module Any : sig
-  val until_binary_validate :
+  val until_validate :
        unsafe:bool
     -> rac:bool
     -> srac:bool
@@ -31,24 +31,10 @@ module Any : sig
     -> 'extern_func Link.state
     -> 'extern_func Kind.t
     -> ('extern_func Link.module_to_run * 'extern_func Link.state) Result.t
-
-  (** compile and interpret a module with a given link state and produce a new
-      link state *)
-  val until_interpret :
-       unsafe:bool
-    -> timeout:float option
-    -> timeout_instr:int option
-    -> rac:bool
-    -> srac:bool
-    -> optimize:bool
-    -> name:string option
-    -> Concrete_extern_func.extern_func Link.state
-    -> Concrete_extern_func.extern_func Kind.t
-    -> Concrete_extern_func.extern_func Link.state Result.t
 end
 
 module File : sig
-  val until_binary_validate :
+  val until_validate :
     unsafe:bool -> rac:bool -> srac:bool -> Fpath.t -> Binary.Module.t Result.t
 
   val until_optimize :
@@ -70,33 +56,17 @@ module File : sig
     -> 'extern_func Link.state
     -> Fpath.t
     -> ('extern_func Link.module_to_run * 'extern_func Link.state) Result.t
-
-  (** compile and interpret a file with a given link state and produce a new
-      link state *)
-  val until_interpret :
-       unsafe:bool
-    -> timeout:float option
-    -> timeout_instr:int option
-    -> rac:bool
-    -> srac:bool
-    -> optimize:bool
-    -> name:string option
-    -> Concrete_extern_func.extern_func Link.state
-    -> Fpath.t
-    -> Concrete_extern_func.extern_func Link.state Result.t
 end
 
 module Text : sig
-  val until_text_validate : unsafe:bool -> Text.modul -> Text.modul Result.t
-
   val until_binary :
        unsafe:bool
     -> rac:bool
     -> srac:bool
     -> Text.modul
     -> Binary.Module.t Result.t
 
-  val until_binary_validate :
+  val until_validate :
        unsafe:bool
     -> rac:bool
     -> srac:bool
@@ -122,24 +92,10 @@ module Text : sig
     -> 'f Link.state
     -> Text.modul
     -> ('f Link.module_to_run * 'f Link.state) Result.t
-
-  (** compile and interpret a module with a given link state and produce a new
-      link state *)
-  val until_interpret :
-       unsafe:bool
-    -> timeout:float option
-    -> timeout_instr:int option
-    -> rac:bool
-    -> srac:bool
-    -> optimize:bool
-    -> name:string option
-    -> Concrete_extern_func.extern_func Link.state
-    -> Text.modul
-    -> Concrete_extern_func.extern_func Link.state Result.t
 end
 
 module Binary : sig
-  val until_binary_validate :
+  val until_validate :
     unsafe:bool -> Binary.Module.t -> Binary.Module.t Result.t
 
   val until_optimize :
@@ -154,16 +110,4 @@ module Binary : sig
     -> 'f Link.state
     -> Binary.Module.t
     -> ('f Link.module_to_run * 'f Link.state) Result.t
-
-  (** compile and interpret a module with a given link state and produce a new
-      link state *)
-  val until_interpret :
-       unsafe:bool
-    -> timeout:float option
-    -> timeout_instr:int option
-    -> optimize:bool
-    -> name:string option
-    -> Concrete_extern_func.extern_func Link.state
-    -> Binary.Module.t
-    -> Concrete_extern_func.extern_func Link.state Result.t
 end

src/bin/owi.ml

@@ -320,15 +320,15 @@ let conc_cmd =
   and+ workspace
   and+ () = setup_log
   and+ solver
-  and+ files
+  and+ source_file
   and+ model_format
   and+ model_out_file
   and+ invoke_with_symbols
   and+ with_breadcrumbs
   and+ entry_point in
   Cmd_conc.cmd ~unsafe ~rac ~srac ~optimize ~workers ~no_stop_at_failure
     ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order
-    ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point
+    ~fail_mode ~workspace ~solver ~source_file ~model_format ~entry_point
     ~invoke_with_symbols ~model_out_file ~with_breadcrumbs
 
 (* owi fmt *)
@@ -451,8 +451,8 @@ let run_cmd =
   and+ rac
   and+ optimize
   and+ () = setup_log
-  and+ files in
-  Cmd_run.cmd ~unsafe ~timeout ~timeout_instr ~rac ~optimize ~files
+  and+ source_file in
+  Cmd_run.cmd ~unsafe ~timeout ~timeout_instr ~rac ~optimize ~source_file
 
 (* owi rust *)
 
@@ -529,7 +529,7 @@ let sym_cmd =
   and+ fail_mode
   and+ workspace
   and+ solver
-  and+ files
+  and+ source_file
   and+ model_format
   and+ () = setup_log
   and+ entry_point
@@ -538,7 +538,7 @@ let sym_cmd =
   and+ invoke_with_symbols in
   Cmd_sym.cmd ~unsafe ~rac ~srac ~optimize ~workers ~no_stop_at_failure
     ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order
-    ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point
+    ~fail_mode ~workspace ~solver ~source_file ~model_format ~entry_point
     ~invoke_with_symbols ~model_out_file ~with_breadcrumbs
 
 (* owi validate *)

src/cmd/cmd_c.ml

@@ -194,15 +194,14 @@ let cmd ~arch ~property ~testcomp:_ ~workspace ~workers ~opt_lvl ~includes
 
   let includes = Cmd_utils.c_files_location @ includes in
   let* files = eacsl_instrument eacsl ~includes files in
-  let* modul =
+  let* source_file =
     compile ~workspace ~entry_point ~includes ~opt_lvl ~out_file files
   in
   let* () = metadata ~workspace arch property files in
-  let files = [ modul ] in
   let entry_point = Some entry_point in
   let workspace = Some workspace in
   (if concolic then Cmd_conc.cmd else Cmd_sym.cmd)
     ~unsafe ~rac:false ~srac:false ~optimize ~workers ~no_stop_at_failure
     ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order
-    ~fail_mode ~workspace ~solver ~files ~model_format ~entry_point
+    ~fail_mode ~workspace ~solver ~source_file ~model_format ~entry_point
     ~invoke_with_symbols ~model_out_file ~with_breadcrumbs