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, 133 insertions, 128 deletions

diff --git a/src/value.ml b/src/value.ml
index 71d9ffe6..751c10d7 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -620,131 +620,136 @@ let value_decimal_string_of_bits = function
   | [v] -> V_string (Sail_lib.decimal_string_of_bits (coerce_bv v))
   | _ -> failwith "value decimal_string_of_bits"
 
-let primops =
-  List.fold_left
-    (fun r (x, y) -> StringMap.add x y r)
-    StringMap.empty
-    [ ("and_bool", and_bool);
-      ("or_bool", or_bool);
-      ("print", value_print);
-      ("prerr", fun vs -> (prerr_string (string_of_value (List.hd vs)); V_unit));
-      ("dec_str", fun _ -> V_string "X");
-      ("print_endline", value_print_endline);
-      ("prerr_endline", fun vs -> (prerr_endline (string_of_value (List.hd vs)); V_unit));
-      ("putchar", value_putchar);
-      ("string_of_int", fun vs -> V_string (string_of_value (List.hd vs)));
-      ("string_of_bits", fun vs -> V_string (string_of_value (List.hd vs)));
-      ("decimal_string_of_bits", value_decimal_string_of_bits);
-      ("print_bits", value_print_bits);
-      ("print_int", value_print_int);
-      ("print_string", value_print_string);
-      ("prerr_bits", value_print_bits);
-      ("prerr_int", value_print_int);
-      ("prerr_string", value_prerr_string);
-      ("concat_str", value_concat_str);
-      ("eq_int", value_eq_int);
-      ("lteq", value_lteq);
-      ("gteq", value_gteq);
-      ("lt", value_lt);
-      ("gt", value_gt);
-      ("eq_list", value_eq_list);
-      ("eq_bool", value_eq_bool);
-      ("eq_string", value_eq_string);
-      ("string_startswith", value_string_startswith);
-      ("string_drop", value_string_drop);
-      ("string_take", value_string_take);
-      ("string_length", value_string_length);
-      ("eq_bit", value_eq_bit);
-      ("eq_anything", value_eq_anything);
-      ("length", value_length);
-      ("subrange", value_subrange);
-      ("access", value_access);
-      ("update", value_update);
-      ("update_subrange", value_update_subrange);
-      ("slice", value_slice);
-      ("append", value_append);
-      ("append_list", value_append_list);
-      ("not", value_not);
-      ("not_vec", value_not_vec);
-      ("and_vec", value_and_vec);
-      ("or_vec", value_or_vec);
-      ("xor_vec", value_xor_vec);
-      ("uint", value_uint);
-      ("sint", value_sint);
-      ("get_slice_int", value_get_slice_int);
-      ("set_slice_int", value_set_slice_int);
-      ("set_slice", value_set_slice);
-      ("hex_slice", value_hex_slice);
-      ("zero_extend", value_zero_extend);
-      ("sign_extend", value_sign_extend);
-      ("zeros", value_zeros);
-      ("ones", value_ones);
-      ("shiftr", value_shiftr);
-      ("shiftl", value_shiftl);
-      ("shift_bits_left", value_shift_bits_left);
-      ("shift_bits_right", value_shift_bits_right);
-      ("add_int", value_add_int);
-      ("sub_int", value_sub_int);
-      ("sub_nat", value_sub_nat);
-      ("div_int", value_quotient);
-      ("mult_int", value_mult);
-      ("mult", value_mult);
-      ("quotient", value_quotient);
-      ("modulus", value_modulus);
-      ("negate", value_negate);
-      ("pow2", value_pow2);
-      ("int_power", value_int_power);
-      ("shr_int", value_shr_int);
-      ("shl_int", value_shl_int);
-      ("max_int", value_max_int);
-      ("min_int", value_min_int);
-      ("abs_int", value_abs_int);
-      ("add_vec_int", value_add_vec_int);
-      ("sub_vec_int", value_sub_vec_int);
-      ("add_vec", value_add_vec);
-      ("sub_vec", value_sub_vec);
-      ("vector_truncate", value_vector_truncate);
-      ("vector_truncateLSB", value_vector_truncateLSB);
-      ("read_ram", value_read_ram);
-      ("write_ram", value_write_ram);
-      ("trace_memory_read", fun _ -> V_unit);
-      ("trace_memory_write", fun _ -> V_unit);
-      ("get_time_ns", fun _ -> V_int (Sail_lib.get_time_ns()));
-      ("load_raw", value_load_raw);
-      ("to_real", value_to_real);
-      ("eq_real", value_eq_real);
-      ("lt_real", value_lt_real);
-      ("gt_real", value_gt_real);
-      ("lteq_real", value_lteq_real);
-      ("gteq_real", value_gteq_real);
-      ("add_real", value_add_real);
-      ("sub_real", value_sub_real);
-      ("mult_real", value_mult_real);
-      ("round_up", value_round_up);
-      ("round_down", value_round_down);
-      ("quot_round_zero", value_quot_round_zero);
-      ("rem_round_zero", value_rem_round_zero);
-      ("quotient_real", value_quotient_real);
-      ("abs_real", value_abs_real);
-      ("div_real", value_div_real);
-      ("sqrt_real", value_sqrt_real);
-      ("print_real", value_print_real);
-      ("random_real", value_random_real);
-      ("undefined_unit", fun _ -> V_unit);
-      ("undefined_bit", fun _ -> V_bit Sail_lib.B0);
-      ("undefined_int", fun _ -> V_int Big_int.zero);
-      ("undefined_nat", fun _ -> V_int Big_int.zero);
-      ("undefined_bool", fun _ -> V_bool false);
-      ("undefined_bitvector", value_undefined_bitvector);
-      ("undefined_vector", value_undefined_vector);
-      ("undefined_string", fun _ -> V_string "");
-      ("internal_pick", value_internal_pick);
-      ("replicate_bits", value_replicate_bits);
-      ("Elf_loader.elf_entry", fun _ -> V_int (!Elf_loader.opt_elf_entry));
-      ("Elf_loader.elf_tohost", fun _ -> V_int (!Elf_loader.opt_elf_tohost));
-      ("string_append", value_string_append);
-      ("string_length", value_string_length);
-      ("string_startswith", value_string_startswith);
-      ("string_drop", value_string_drop);
-      ("skip", fun _ -> V_unit);
-    ]
+let primops = ref
+  (List.fold_left
+     (fun r (x, y) -> StringMap.add x y r)
+     StringMap.empty
+     [ ("and_bool", and_bool);
+       ("or_bool", or_bool);
+       ("print", value_print);
+       ("prerr", fun vs -> (prerr_string (string_of_value (List.hd vs)); V_unit));
+       ("dec_str", fun _ -> V_string "X");
+       ("print_endline", value_print_endline);
+       ("prerr_endline", fun vs -> (prerr_endline (string_of_value (List.hd vs)); V_unit));
+       ("putchar", value_putchar);
+       ("string_of_int", fun vs -> V_string (string_of_value (List.hd vs)));
+       ("string_of_bits", fun vs -> V_string (string_of_value (List.hd vs)));
+       ("decimal_string_of_bits", value_decimal_string_of_bits);
+       ("print_bits", value_print_bits);
+       ("print_int", value_print_int);
+       ("print_string", value_print_string);
+       ("prerr_bits", value_print_bits);
+       ("prerr_int", value_print_int);
+       ("prerr_string", value_prerr_string);
+       ("concat_str", value_concat_str);
+       ("eq_int", value_eq_int);
+       ("lteq", value_lteq);
+       ("gteq", value_gteq);
+       ("lt", value_lt);
+       ("gt", value_gt);
+       ("eq_list", value_eq_list);
+       ("eq_bool", value_eq_bool);
+       ("eq_string", value_eq_string);
+       ("string_startswith", value_string_startswith);
+       ("string_drop", value_string_drop);
+       ("string_take", value_string_take);
+       ("string_length", value_string_length);
+       ("eq_bit", value_eq_bit);
+       ("eq_anything", value_eq_anything);
+       ("length", value_length);
+       ("subrange", value_subrange);
+       ("access", value_access);
+       ("update", value_update);
+       ("update_subrange", value_update_subrange);
+       ("slice", value_slice);
+       ("append", value_append);
+       ("append_list", value_append_list);
+       ("not", value_not);
+       ("not_vec", value_not_vec);
+       ("and_vec", value_and_vec);
+       ("or_vec", value_or_vec);
+       ("xor_vec", value_xor_vec);
+       ("uint", value_uint);
+       ("sint", value_sint);
+       ("get_slice_int", value_get_slice_int);
+       ("set_slice_int", value_set_slice_int);
+       ("set_slice", value_set_slice);
+       ("hex_slice", value_hex_slice);
+       ("zero_extend", value_zero_extend);
+       ("sign_extend", value_sign_extend);
+       ("zeros", value_zeros);
+       ("ones", value_ones);
+       ("shiftr", value_shiftr);
+       ("shiftl", value_shiftl);
+       ("shift_bits_left", value_shift_bits_left);
+       ("shift_bits_right", value_shift_bits_right);
+       ("add_int", value_add_int);
+       ("sub_int", value_sub_int);
+       ("sub_nat", value_sub_nat);
+       ("div_int", value_quotient);
+       ("mult_int", value_mult);
+       ("mult", value_mult);
+       ("quotient", value_quotient);
+       ("modulus", value_modulus);
+       ("negate", value_negate);
+       ("pow2", value_pow2);
+       ("int_power", value_int_power);
+       ("shr_int", value_shr_int);
+       ("shl_int", value_shl_int);
+       ("max_int", value_max_int);
+       ("min_int", value_min_int);
+       ("abs_int", value_abs_int);
+       ("add_vec_int", value_add_vec_int);
+       ("sub_vec_int", value_sub_vec_int);
+       ("add_vec", value_add_vec);
+       ("sub_vec", value_sub_vec);
+       ("vector_truncate", value_vector_truncate);
+       ("vector_truncateLSB", value_vector_truncateLSB);
+       ("read_ram", value_read_ram);
+       ("write_ram", value_write_ram);
+       ("trace_memory_read", fun _ -> V_unit);
+       ("trace_memory_write", fun _ -> V_unit);
+       ("get_time_ns", fun _ -> V_int (Sail_lib.get_time_ns()));
+       ("load_raw", value_load_raw);
+       ("to_real", value_to_real);
+       ("eq_real", value_eq_real);
+       ("lt_real", value_lt_real);
+       ("gt_real", value_gt_real);
+       ("lteq_real", value_lteq_real);
+       ("gteq_real", value_gteq_real);
+       ("add_real", value_add_real);
+       ("sub_real", value_sub_real);
+       ("mult_real", value_mult_real);
+       ("round_up", value_round_up);
+       ("round_down", value_round_down);
+       ("quot_round_zero", value_quot_round_zero);
+       ("rem_round_zero", value_rem_round_zero);
+       ("quotient_real", value_quotient_real);
+       ("abs_real", value_abs_real);
+       ("div_real", value_div_real);
+       ("sqrt_real", value_sqrt_real);
+       ("print_real", value_print_real);
+       ("random_real", value_random_real);
+       ("undefined_unit", fun _ -> V_unit);
+       ("undefined_bit", fun _ -> V_bit Sail_lib.B0);
+       ("undefined_int", fun _ -> V_int Big_int.zero);
+       ("undefined_nat", fun _ -> V_int Big_int.zero);
+       ("undefined_bool", fun _ -> V_bool false);
+       ("undefined_bitvector", value_undefined_bitvector);
+       ("undefined_vector", value_undefined_vector);
+       ("undefined_string", fun _ -> V_string "");
+       ("internal_pick", value_internal_pick);
+       ("replicate_bits", value_replicate_bits);
+       ("Elf_loader.elf_entry", fun _ -> V_int (!Elf_loader.opt_elf_entry));
+       ("Elf_loader.elf_tohost", fun _ -> V_int (!Elf_loader.opt_elf_tohost));
+       ("string_append", value_string_append);
+       ("string_length", value_string_length);
+       ("string_startswith", value_string_startswith);
+       ("string_drop", value_string_drop);
+       ("skip", fun _ -> V_unit);
+     ])
+
+let add_primop name impl =
+  primops := StringMap.add name impl !primops
+  
+