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

doc/src/manpages/owi-run.md

@@ -25,6 +25,12 @@ OPTIONS
        --rac
            runtime assertion checking mode
 
+       --timeout=S
+           Stop execution after S seconds.
+
+       --timeout-instr=I
+           Stop execution after running I instructions.
+
        -u, --unsafe
            skip typechecking pass
 

doc/src/ocaml-api/custom-functions.md

@@ -99,8 +99,11 @@ let module_to_run, link_state =
 
 (* let's run it ! it will print the values as defined in the print_i32 function *)
 let () =
-  match Interpret.Concrete.modul link_state.envs module_to_run with
-  | Error _ -> assert false
+  match
+    Interpret.Concrete.modul ~timeout:None ~timeout_instr:None link_state.envs
+      module_to_run
+  with
+  | Error _o -> assert false
   | Ok () -> ()
 ```
 
@@ -222,7 +225,10 @@ let module_to_run, link_state =
 
 (* let's run it ! it will print the values as defined in the print_i64 function *)
 let () =
-  match Interpret.Concrete.modul link_state.envs module_to_run with
+  match
+    Interpret.Concrete.modul ~timeout:None ~timeout_instr:None link_state.envs
+      module_to_run
+  with
   | Error _ -> assert false
   | Ok () -> ()
 ```

doc/src/ocaml-api/extern.ml

@@ -53,6 +53,9 @@ let module_to_run, link_state =
 
 (* let's run it ! it will print the values as defined in the print_i32 function *)
 let () =
-  match Interpret.Concrete.modul link_state.envs module_to_run with
-  | Error _ -> assert false
+  match
+    Interpret.Concrete.modul ~timeout:None ~timeout_instr:None link_state.envs
+      module_to_run
+  with
+  | Error _o -> assert false
   | Ok () -> ()

doc/src/ocaml-api/extern_mem.ml

@@ -51,6 +51,9 @@ let module_to_run, link_state =
 
 (* let's run it ! it will print the values as defined in the print_i64 function *)
 let () =
-  match Interpret.Concrete.modul link_state.envs module_to_run with
+  match
+    Interpret.Concrete.modul ~timeout:None ~timeout_instr:None link_state.envs
+      module_to_run
+  with
   | Error _ -> assert false
   | Ok () -> ()

doc/src/ocaml-api/game-of-life/life_console.ml

@@ -80,7 +80,10 @@ let module_to_run, link_state =
 
 (* let's run it ! First module to be interpreted *)
 let () =
-  match Interpret.Concrete.modul link_state.envs module_to_run with
+  match
+    Interpret.Concrete.modul ~timeout:None ~timeout_instr:None link_state.envs
+      module_to_run
+  with
   | Error _ -> assert false
   | Ok () -> ()
 
@@ -101,6 +104,9 @@ let module_to_run, link_state =
 
 (* let's run it ! it will animate the game of life in console *)
 let () =
-  match Interpret.Concrete.modul link_state.envs module_to_run with
+  match
+    Interpret.Concrete.modul ~timeout:None ~timeout_instr:None link_state.envs
+      module_to_run
+  with
   | Error _ -> assert false
   | Ok () -> ()

doc/src/ocaml-api/overview.md

@@ -29,7 +29,7 @@ mdx_gen.bc.exe: [INFO] typechecking ...
 mdx_gen.bc.exe: [INFO] linking      ...
 ...
 # let () =
-    match Interpret.Concrete.modul link_state.envs module_to_run with
+    match Interpret.Concrete.modul ~timeout:None ~timeout_instr:None link_state.envs module_to_run with
     | Ok () -> ()
     | Error _ -> assert false;;
 mdx_gen.bc.exe: [INFO] interpreting ...

src/ast/compile.ml

@@ -38,11 +38,14 @@ 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 +64,12 @@ 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 +90,14 @@ 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 +124,15 @@ 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,14 @@ 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)
@@ -438,11 +446,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,9 @@ 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,9 @@ 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
-      link_state filename
+    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,24 @@ 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 +1464,49 @@ 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 after_time =
+           let start_time = Unix.gettimeofday () in
+           fun timeout_s ->
+             Float.compare (Unix.gettimeofday () -. start_time) timeout_s > 0
+         in
+         fun () ->
+           let fuel_left = Atomic.fetch_and_add fuel (-1) in
+           (* If we only use [timeout_instr], we want to stop all as
+              soon as [fuel_left <= 0]. But if we only use [timeout],
+              we don't want to run into the slow path below on each
+              instruction after [fuel_left] becomes negative. We avoid
+              this repeated slow path by bumping [fuel] to [max_int]
+              again in this case. *)
+           if fuel_left mod 1024 = 0 || fuel_left < 0 then begin
+             let stop =
+               match (timeout, timeout_instr) with
+               | None, None -> assert false
+               | None, Some _instr -> fuel_left <= 0
+               | Some s, Some _instr -> after_time s || fuel_left <= 0
+               | Some s, None ->
+                 let stop = after_time s in
+                 if (not stop) && fuel_left < 0 then Atomic.set fuel max_int;
+                 stop
+             in
+             if stop 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,8 +1515,8 @@ 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
-                  None
+                exec_expr ~heartbeat envs env (State.Locals.of_list [])
+                  Stack.empty to_run None
               in
               () )
             (Choice.return ())
@@ -1508,7 +1548,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