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/smtlib.ml b/src/smtlib.ml
index b90f33a7..06386f61 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -529,7 +529,7 @@ let check_counterexample ast env fname function_id args arg_ctyps arg_smt_names
      prerr_endline (sprintf "Solver found counterexample: %s" Util.("ok" |> green |> clear));
      let counterexample = build_counterexample args arg_ctyps arg_smt_names model in
      List.iter (fun (id, v) -> prerr_endline ("  " ^ string_of_id id ^ " -> " ^ string_of_value v)) counterexample;
-     let istate = initial_state ast env primops in
+     let istate = initial_state ast env !primops in
      let annot = (Parse_ast.Unknown, Type_check.mk_tannot env bool_typ no_effect) in
      let call = E_aux (E_app (function_id, List.map (fun (_, v) -> E_aux (E_internal_value v, (Parse_ast.Unknown, Type_check.empty_tannot))) counterexample), annot) in
      let result = run (Step (lazy "", istate, return call, [])) in