Implement '--timeout' and '--timeout-instr' options, only in 'owi run' for now

See #155

Author: gasche

src/ast/compile.ml

@@ -38,11 +38,11 @@ module Text = struct
     let* m = until_optimize ~unsafe ~rac ~srac ~optimize m in
     Link.modul link_state ~name m
 
-  let until_interpret ~unsafe ~rac ~srac ~optimize ~name link_state 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 link_state.envs m in
+    let+ () = Interpret.Concrete.modul ~timeout ~timeout_instr link_state.envs m in
     link_state
 end
 
@@ -61,9 +61,9 @@ module Binary = struct
     let* m = until_optimize ~unsafe ~optimize m in
     Link.modul link_state ~name m
 
-  let until_interpret ~unsafe ~optimize ~name link_state 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 link_state.envs m in
+    let+ () = Interpret.Concrete.modul ~timeout ~timeout_instr link_state.envs m in
     link_state
 end
 
@@ -84,10 +84,10 @@ module Any = struct
     | Wasm m -> Binary.until_link ~unsafe ~optimize ~name link_state m
     | Wast _ | Ocaml _ -> assert false
 
-  let until_interpret ~unsafe ~rac ~srac ~optimize ~name link_state = function
+  let until_interpret ~unsafe ~timeout ~timeout_instr ~rac ~srac ~optimize ~name link_state = function
     | Kind.Wat m ->
-      Text.until_interpret ~unsafe ~rac ~srac ~optimize ~name link_state m
-    | Wasm m -> Binary.until_interpret ~unsafe ~optimize ~name link_state 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
 
@@ -114,11 +114,11 @@ module File = struct
     | Wasm m -> Binary.until_link ~unsafe ~optimize ~name link_state m
     | Wast _ | Ocaml _ -> assert false
 
-  let until_interpret ~unsafe ~rac ~srac ~optimize ~name link_state filename =
+  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 ~rac ~srac ~optimize ~name link_state m
-    | Wasm m -> Binary.until_interpret ~unsafe ~optimize ~name link_state 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

@@ -36,6 +36,8 @@ module Any : sig
       link state *)
   val until_interpret :
        unsafe:bool
+    -> timeout:float option
+    -> timeout_instr:int option
     -> rac:bool
     -> srac:bool
     -> optimize:bool
@@ -73,6 +75,8 @@ module File : sig
       link state *)
   val until_interpret :
        unsafe:bool
+    -> timeout:float option
+    -> timeout_instr:int option
     -> rac:bool
     -> srac:bool
     -> optimize:bool
@@ -123,6 +127,8 @@ module Text : sig
       link state *)
   val until_interpret :
        unsafe:bool
+    -> timeout:float option
+    -> timeout_instr:int option
     -> rac:bool
     -> srac:bool
     -> optimize:bool
@@ -153,6 +159,8 @@ module Binary : sig
       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

src/bin/owi.ml

@@ -180,6 +180,24 @@ let srac =
   let doc = "symbolic runtime assertion checking mode" in
   Arg.(value & flag & info [ "srac" ] ~doc)
 
+let timeout =
+  let doc =
+    "Stop execution after S seconds."
+  in
+  Arg.(
+    value
+    & opt (some float) None
+    & info [ "timeout" ] ~doc ~docv:"S" )
+
+let timeout_instr =
+  let doc =
+    "Stop execution after running I instructions."
+  in
+  Arg.(
+    value
+    & opt (some int) None
+    & info [ "timeout-instr" ] ~doc ~docv:"I" )
+
 let unsafe =
   let doc = "skip typechecking pass" in
   Arg.(value & flag & info [ "unsafe"; "u" ] ~doc)
@@ -249,8 +267,8 @@ let c_cmd =
   and+ with_breadcrumbs
   and+ entry_point in
   Cmd_c.cmd ~arch ~property ~testcomp ~workspace ~workers ~opt_lvl ~includes
-    ~files ~unsafe ~optimize ~no_stop_at_failure ~no_value
-    ~no_assert_failure_expression_printing ~deterministic_result_order
+    ~files ~unsafe ~optimize ~no_stop_at_failure
+    ~no_value ~no_assert_failure_expression_printing ~deterministic_result_order
     ~fail_mode ~concolic ~eacsl ~solver ~model_format ~entry_point
     ~invoke_with_symbols ~out_file ~model_out_file ~with_breadcrumbs
 (* owi cpp *)
@@ -438,11 +456,13 @@ let run_info =
 
 let run_cmd =
   let+ unsafe
+  and+ timeout
+  and+ timeout_instr
   and+ rac
   and+ optimize
   and+ () = setup_log
   and+ files in
-  Cmd_run.cmd ~unsafe ~rac ~optimize ~files
+  Cmd_run.cmd ~unsafe ~timeout ~timeout_instr ~rac ~optimize ~files
 
 (* owi rust *)
 

src/cmd/cmd_conc.ml

@@ -57,7 +57,7 @@ let run_modules_to_run (link_state : _ Link.state) modules_to_run =
   List.fold_left
     (fun (acc : unit Choice.t) to_run ->
       Choice.bind acc (fun () ->
-        (Interpret.Concolic.modul link_state.envs) to_run ) )
+        (Interpret.Concolic.modul ~timeout:None ~timeout_instr:None link_state.envs) to_run ) )
     (Choice.return ()) modules_to_run
 
 type end_of_trace =

src/cmd/cmd_iso.ml

@@ -329,7 +329,7 @@ let check_iso ~unsafe export_name export_type module1 module2 =
   in
   let m = Symbolic.convert_module_to_run m in
 
-  Interpret.Symbolic.modul link_state.envs m
+  Interpret.Symbolic.modul ~timeout:None ~timeout_instr:None link_state.envs m
 
 module String_set = Set.Make (String)
 

src/cmd/cmd_replay.ml

@@ -212,7 +212,7 @@ let run_file ~unsafe ~optimize ~entry_point ~invoke_with_symbols filename model
   let* m, link_state =
     Compile.Binary.until_link ~unsafe link_state ~optimize ~name:None m
   in
-  let* () = Interpret.Concrete.modul link_state.envs m in
+  let* () = Interpret.Concrete.modul ~timeout:None ~timeout_instr:None link_state.envs m in
   Ok ()
 
 let cmd ~unsafe ~optimize ~replay_file ~source_file ~entry_point

src/cmd/cmd_run.ml

@@ -22,14 +22,14 @@ let extern_module : Concrete_extern_func.extern_func Link.extern_module =
 let link_state =
   Link.extern_module Link.empty_state ~name:"symbolic" extern_module
 
-let run_file ~unsafe ~rac ~optimize filename =
+let run_file ~unsafe ~timeout ~timeout_instr ~rac ~optimize filename =
   let name = None in
   let link_state = if rac then link_state else Link.empty_state in
   let+ (_ : _ Link.state) =
-    Compile.File.until_interpret ~unsafe ~rac ~srac:false ~optimize ~name
+    Compile.File.until_interpret ~unsafe ~timeout ~timeout_instr ~rac ~srac:false ~optimize ~name
       link_state filename
   in
   ()
 
-let cmd ~unsafe ~rac ~optimize ~files =
-  list_iter (run_file ~unsafe ~rac ~optimize) files
+let cmd ~unsafe ~timeout ~timeout_instr ~rac ~optimize ~files =
+  list_iter (run_file ~unsafe ~timeout ~timeout_instr ~rac ~optimize) files

src/cmd/cmd_run.mli

@@ -4,6 +4,8 @@
 
 val cmd :
      unsafe:bool
+  -> timeout:float option
+  -> timeout_instr:int option
   -> rac:bool
   -> optimize:bool
   -> files:Fpath.t list

src/cmd/cmd_sym.ml

@@ -31,7 +31,7 @@ let run_file ~entry_point ~unsafe ~rac ~srac ~optimize ~invoke_with_symbols _pc
     Compile.Binary.until_link ~unsafe ~optimize ~name:None link_state m
   in
   let m = Symbolic.convert_module_to_run m in
-  Interpret.Symbolic.modul link_state.envs m
+  Interpret.Symbolic.modul ~timeout:None ~timeout_instr:None link_state.envs m
 
 let print_bug ~model_format ~labels ~model_out_file ~id ~no_value
   ~no_stop_at_failure ~no_assert_failure_expression_printing ~breadcrumbs

src/interpret/interpret.ml

@@ -1433,21 +1433,25 @@ module Make (P : Interpret_intf.P) :
         m "unimplemented instruction: %a" (Types.pp_instr ~short:false) i );
       assert false
 
-  let rec loop (state : State.exec_state) =
+  let rec loop ~heartbeat (state : State.exec_state) =
+    let* () =
+      match heartbeat with
+        | None -> Choice.return ()
+        | Some f -> f () in
     match state.pc with
     | instr :: pc -> begin
       let* state = exec_instr instr { state with pc } in
       match state with
-      | State.Continue state -> loop state
+      | State.Continue state -> loop ~heartbeat state
       | State.Return res -> Choice.return res
     end
     | [] -> (
       let* next_state = State.end_block state in
       match next_state with
-      | State.Continue state -> loop state
+      | State.Continue state -> loop ~heartbeat state
       | State.Return res -> Choice.return res )
 
-  let exec_expr envs env locals stack expr bt =
+  let exec_expr ~heartbeat envs env locals stack expr bt =
     let state : State.exec_state =
       let func_rt = match bt with None -> [] | Some rt -> rt in
       { stack
@@ -1461,12 +1465,40 @@ module Make (P : Interpret_intf.P) :
       }
     in
 
-    let+ state = loop state in
+    let+ state = loop ~heartbeat state in
     state
 
-  let modul envs (modul : Module_to_run.t) : unit P.Choice.t =
+  let make_heartbeat ~timeout ~timeout_instr () =
+    match timeout, timeout_instr with
+      | None, None -> None
+      | Some _, _ | _, Some _ ->
+         Some (
+           let fuel = Atomic.make (
+             match timeout_instr with
+               | Some i -> i
+               | None -> max_int
+           ) in
+           let start_time = Unix.gettimeofday () in
+           fun () ->
+           let fuel_left = Atomic.fetch_and_add fuel (-1) in
+           if fuel_left mod 1024 = 0 then begin
+             let at_timeout = match timeout with
+                 | None -> false
+                 | Some s -> Float.compare (Unix.gettimeofday () -. start_time) s > 0
+             in
+             let at_timeout_instr = match timeout_instr with
+                 | None -> false
+                 | Some _ -> fuel_left <= 0
+             in
+             if at_timeout || at_timeout_instr
+             then Choice.trap (`Msg "timeout")
+             else Choice.return ()
+           end else Choice.return ()
+         )
+
+  let modul ~timeout ~timeout_instr envs (modul : Module_to_run.t) : unit P.Choice.t =
+    let heartbeat = make_heartbeat ~timeout ~timeout_instr () in
     Logs.info (fun m -> m "interpreting ...");
-
     try
       begin
         let* () =
@@ -1475,7 +1507,7 @@ module Make (P : Interpret_intf.P) :
               let* () = u in
               let+ _end_stack =
                 let env = Module_to_run.env modul in
-                exec_expr envs env (State.Locals.of_list []) Stack.empty to_run
+                exec_expr ~heartbeat envs env (State.Locals.of_list []) Stack.empty to_run
                   None
               in
               () )
@@ -1508,7 +1540,7 @@ module Make (P : Interpret_intf.P) :
         match state with
         | State.Return res -> Choice.return res
         | State.Continue state ->
-          let+ res = loop state in
+          let+ res = loop ~heartbeat:None state in
           res
       end
     with Stack_overflow -> Choice.trap `Call_stack_exhausted

src/interpret/interpret.mli

@@ -4,7 +4,9 @@
 
 module Concrete : sig
   val modul :
-       Concrete.Env.t Env_id.collection
+       timeout:float option
+    -> timeout_instr:int option
+    -> Concrete.Env.t Env_id.collection
     -> Concrete.Module_to_run.t
     -> unit Concrete_choice.t
 
@@ -44,21 +46,27 @@ end
 
 module Symbolic : sig
   val modul :
-       Symbolic.Env.t Env_id.collection
+       timeout:float option
+    -> timeout_instr:int option
+    -> Symbolic.Env.t Env_id.collection
     -> Symbolic.Module_to_run.t
     -> unit Symbolic.Choice.t
 end
 
 module Minimalist_symbolic : sig
   val modul :
-       Minimalist_symbolic.Env.t Env_id.collection
+       timeout:float option
+    -> timeout_instr:int option
+    -> Minimalist_symbolic.Env.t Env_id.collection
     -> Minimalist_symbolic.Module_to_run.t
     -> unit Minimalist_symbolic.Choice.t
 end
 
 module Concolic : sig
   val modul :
-       Concolic.Env.t Env_id.collection
+       timeout:float option
+    -> timeout_instr:int option
+    -> Concolic.Env.t Env_id.collection
     -> Concolic.Module_to_run.t
     -> unit Concolic.Choice.t
 end

src/intf/interpret_intf.ml

@@ -159,7 +159,10 @@ module type S = sig
   type module_to_run
 
   (** interpret a module *)
-  val modul : env Env_id.collection -> module_to_run -> unit choice
+  val modul :
+    timeout:float option ->
+    timeout_instr:int option ->
+    env Env_id.collection -> module_to_run -> unit choice
 
   type value
 

src/script/script.ml

@@ -160,7 +160,7 @@ let run ~no_exhaustion ~optimize script =
         Logs.info (fun m -> m "*** module");
         incr curr_module;
         let+ link_state =
-          Compile.Text.until_interpret link_state ~unsafe ~rac:false ~srac:false
+          Compile.Text.until_interpret ~timeout:None ~timeout_instr:None link_state ~unsafe ~rac:false ~srac:false
             ~optimize ~name:None m
         in
         (* TODO: enable printing again! *)
@@ -170,7 +170,9 @@ let run ~no_exhaustion ~optimize script =
         incr curr_module;
         let* m = Parse.Text.Inline_module.from_string m in
         let+ link_state =
-          Compile.Text.until_interpret link_state ~unsafe ~rac:false ~srac:false
+          Compile.Text.until_interpret link_state
+            ~unsafe ~rac:false ~srac:false
+            ~timeout:None ~timeout_instr:None
             ~optimize ~name:None m
         in
         link_state
@@ -180,7 +182,7 @@ let run ~no_exhaustion ~optimize script =
         let* m = Parse.Binary.Module.from_string m in
         let m = { m with id } in
         let+ link_state =
-          Compile.Binary.until_interpret link_state ~unsafe ~optimize ~name:None
+          Compile.Binary.until_interpret link_state ~timeout:None ~timeout_instr:None ~unsafe ~optimize ~name:None
             m
         in
         link_state
@@ -191,7 +193,7 @@ let run ~no_exhaustion ~optimize script =
           Compile.Text.until_link link_state ~unsafe ~rac:false ~srac:false
             ~optimize ~name:None m
         in
-        let got = Interpret.Concrete.modul link_state.envs m in
+        let got = Interpret.Concrete.modul ~timeout:None ~timeout_instr:None link_state.envs m in
         let+ () = check_error_result expected got in
         link_state
       | Assert (Assert_malformed_binary (m, expected)) ->

test/run/dune

@@ -1,5 +1,7 @@
 (cram
  (deps
   %{bin:owi}
+  (file ./loop.wat)
+  (file ./fibo.wat)
   (file ./binary_loop.wasm)
   (file ./overflow.wat)))