Allow sail to be scripted using sail

Currently the -is option allows a list of interactive commands to be
passed to the interactive toplevel, however this is only capable of
executing a sequential list of instructions which is quite limiting.

This commit allows sail interactive commands to be invoked from sail
functions running in the interpreter which can be freely interleaved
with ordinary sail code, for example one could test an assertion at each
QEMU/GDB breakpoint like so:

$include <aarch64.sail>

function main() -> unit = {
  sail_gdb_start("target-select remote localhost:1234");
  while true do {
    sail_gdb_continue(); // Run until breakpoint
    sail_gdb_sync();     // Sync register state with QEMU
    if not(my_assertion()) {
      print_endline("Assertion failed")
    }
  }
}

1 files changed, 4 insertions, 4 deletions

diff --git a/src/jib/jib_ir.ml b/src/jib/jib_ir.ml
index c5f2b20a..2fdc4b88 100644
--- a/src/jib/jib_ir.ml
+++ b/src/jib/jib_ir.ml
@@ -244,7 +244,7 @@ let () =
   let open Interactive in
   let open Jib_interactive in
 
-  (fun arg ->
+  ArgString ("(val|register)? identifier", fun arg -> Action (fun () ->
     let is_def id = function
       | CDEF_fundef (id', _, _, _) -> Id.compare id id' = 0
       | CDEF_spec (id', _, _) -> Id.compare id (prepend_id "val " id') = 0
@@ -258,12 +258,12 @@ let () =
        let buf = Buffer.create 256 in
        with_colors (fun () -> Flat_ir_formatter.output_def buf cdef);
        print_endline (Buffer.contents buf)
-  ) |> Interactive.(register_command ~name:"ir" ~help:(sprintf ":ir %s - Print the ir representation of a toplevel definition" (arg "(val|register)? identifier")));
+  )) |> Interactive.register_command ~name:"ir" ~help:"Print the ir representation of a toplevel definition";
 
-  (fun file ->
+  ArgString ("file", fun file -> Action (fun () ->
     let buf = Buffer.create 256 in
     let out_chan = open_out file in
     Flat_ir_formatter.output_defs buf !ir;
     output_string out_chan (Buffer.contents buf);
     close_out out_chan
-  ) |> Interactive.(register_command ~name:"dump_ir" ~help:(sprintf ":dump_ir %s - Dump the ir to a file" (arg "file")))
+  )) |> Interactive.register_command ~name:"dump_ir" ~help:"Dump the ir to a file"