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, 1 insertions, 1 deletions

diff --git a/src/jib/jib_smt_fuzz.ml b/src/jib/jib_smt_fuzz.ml
index 846d0178..02e70e29 100644
--- a/src/jib/jib_smt_fuzz.ml
+++ b/src/jib/jib_smt_fuzz.ml
@@ -158,7 +158,7 @@ let fuzz_cdef ctx all_cdefs = function
      if Env.is_extern id ctx.tc_env "smt" then (
        let extern = Env.get_extern id ctx.tc_env "smt" in
        let typq, (Typ_aux (aux, _) as typ) = Env.get_val_spec id ctx.tc_env in
-       let istate = initial_state ctx.ast ctx.tc_env Value.primops in
+       let istate = initial_state ctx.ast ctx.tc_env !Value.primops in
        let header = smt_header ctx all_cdefs in
        prerr_endline (Util.("Fuzz: " |> cyan |> clear) ^ string_of_id id ^ " = \"" ^ extern ^ "\" : " ^ string_of_typ typ);