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, 3 insertions, 10 deletions

diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 13438208..bec4ce75 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -257,8 +257,7 @@ let rec instr_rename from_id to_id (I_aux (instr, aux)) =
 (* 1. Instruction pretty printer                                          *)
 (**************************************************************************)
 
-
-let string_of_name ?deref_current_exception:(dce=true) ?zencode:(zencode=true) =
+let string_of_name ?deref_current_exception:(dce=false) ?zencode:(zencode=true) =
   let ssa_num n = if n = -1 then "" else ("/" ^ string_of_int n) in
   function
   | Name (id, n) ->
@@ -377,16 +376,10 @@ let rec string_of_cval = function
      Printf.sprintf "%s.%s" (string_of_cval f) (string_of_uid field)
   | V_tuple_member (f, _, n) ->
      Printf.sprintf "%s.ztup%d" (string_of_cval f) n
-  | V_ctor_kind (f, ctor, [], _) ->
-     string_of_cval f ^ " is " ^ Util.zencode_string (string_of_id ctor)
   | V_ctor_kind (f, ctor, unifiers, _) ->
-     string_of_cval f ^ " is " ^ Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)
-  | V_ctor_unwrap (ctor, f, [], _) ->
-     Printf.sprintf "%s as %s" (string_of_cval f) (string_of_id ctor)
+     string_of_cval f ^ " is " ^ string_of_uid (ctor, unifiers)
   | V_ctor_unwrap (ctor, f, unifiers, _) ->
-     Printf.sprintf "%s as %s"
-       (string_of_cval f)
-       (Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers))
+     string_of_cval f ^ " as " ^ string_of_uid (ctor, unifiers)
   | V_struct (fields, _) ->
      Printf.sprintf "{%s}"
        (Util.string_of_list ", " (fun (field, cval) -> string_of_uid field ^ " = " ^ string_of_cval cval) fields)