Implementing callbacks in sail-riscv for state-changing events

Makefile

@@ -267,11 +267,11 @@ c_preserve_fns=-c_preserve _set_Misa_C
 
 generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile
  mkdir -p generated_definitions/c
- $(SAIL) $(SAIL_FLAGS) $(c_preserve_fns) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@)
+ $(SAIL) $(SAIL_FLAGS) $(c_preserve_fns) -O -Oconstant_fold -memo_z3 -c -c_include riscv_default_callbacks.c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@)
 
 generated_definitions/c2/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile
  mkdir -p generated_definitions/c2
- $(SAIL) $(SAIL_FLAGS) -no_warn -memo_z3 -config c_emulator/config.json -c2 $(SAIL_SRCS) -o $(basename $@)
+ $(SAIL) $(SAIL_FLAGS) -no_warn -memo_z3 -config c_emulator/config.json -c2 -c_include riscv_default_callbacks.c $(SAIL_SRCS) -o $(basename $@)
 
 $(SOFTFLOAT_LIBS):
  $(MAKE) SPECIALIZE_TYPE=$(SOFTFLOAT_SPECIALIZE_TYPE) -C $(SOFTFLOAT_LIBDIR)
@@ -299,14 +299,18 @@ rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \
  -c_preserve rvfi_get_int_data \
  -c_preserve rvfi_zero_exec_packet \
  -c_preserve rvfi_halt_exec_packet \
+ -c_preserve rvfi_write \
+ -c_preserve rvfi_read \
+ -c_preserve rvfi_mem_exception \
+ -c_preserve rvfi_wX \
  -c_preserve print_rvfi_exec \
  -c_preserve print_instr_packet \
  -c_preserve print_rvfi_exec
 
 # sed -i isn't posix compliant, unfortunately
 generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main.sail Makefile
  mkdir -p generated_definitions/c
- $(SAIL) $(c_preserve_fns) $(rvfi_preserve_fns) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@)
+ $(SAIL) $(c_preserve_fns) $(rvfi_preserve_fns) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) -c_include riscv_rvfi_callbacks.c model/main.sail -o $(basename $@)
  sed -e '/^[[:space:]]*$$/d' $@ > $@.new
  mv $@.new $@
 

c_emulator/riscv_config.h

@@ -5,3 +5,4 @@ extern bool config_print_instr;
 extern bool config_print_reg;
 extern bool config_print_mem_access;
 extern bool config_print_platform;
+extern bool rv_enable_callbacks;

c_emulator/riscv_default_callbacks.c

@@ -0,0 +1,11 @@
+/* The model assumes that these functions do not change the state of the model.
+ */
+int mem_write_callback(uint64_t addr, uint64_t width, lbits value) { }
+int mem_read_callback(uint64_t addr, uint64_t width, lbits value) { }
+int mem_exception_callback(uint64_t addr, uint64_t num_of_exception) { }
+int xreg_write_callback(unsigned reg, uint64_t value) { }
+int freg_write_callback(unsigned reg, uint64_t value) { }
+int csr_write_callback(unsigned reg, uint64_t value) { }
+int csr_read_callback(unsigned reg, uint64_t value) { }
+int vreg_write_callback(unsigned reg, lbits value) { }
+int pc_write_callback(uint64_t value) { }

c_emulator/riscv_rvfi_callbacks.c

@@ -0,0 +1,37 @@
+#include "riscv_config.h"
+
+int zrvfi_write(uint64_t addr, int64_t width, lbits value);
+int zrvfi_read(uint64_t addr, sail_int width, lbits value);
+int zrvfi_mem_exception(uint64_t addr);
+int zrvfi_wX(int64_t reg, uint64_t value);
+
+int mem_write_callback(uint64_t addr, uint64_t width, lbits value)
+{
+ if (rv_enable_callbacks)
+ zrvfi_write(addr, width, value);
+}
+int mem_read_callback(uint64_t addr, uint64_t width, lbits value)
+{
+ if (rv_enable_callbacks) {
+ sail_int len;
+ CREATE(sail_int)(&len);
+ CONVERT_OF(sail_int, mach_int)(&len, width);
+ zrvfi_read(addr, len, value);
+ KILL(sail_int)(&len);
+ }
+}
+int mem_exception_callback(uint64_t addr, uint64_t num_of_exception)
+{
+ if (rv_enable_callbacks)
+ zrvfi_mem_exception(addr);
+}
+int xreg_write_callback(unsigned reg, uint64_t value)
+{
+ if (rv_enable_callbacks)
+ zrvfi_wX(reg, value);
+}
+int freg_write_callback(unsigned reg, uint64_t value) { }
+int csr_write_callback(unsigned reg, uint64_t value) { }
+int csr_read_callback(unsigned reg, uint64_t value) { }
+int vreg_write_callback(unsigned reg, lbits value) { }
+int pc_write_callback(uint64_t value) { }

c_emulator/riscv_sail.h

@@ -50,6 +50,20 @@ extern bool zhtif_done;
 extern mach_bits zhtif_exit_code;
 extern bool have_exception;
 
+/* Callbacks for state-changing events */
+
+/* The model assumes that these functions do not change the state of the model.
+ */
+int mem_write_callback(uint64_t addr, uint64_t width, lbits value);
+int mem_read_callback(uint64_t addr, uint64_t width, lbits value);
+int mem_exception_callback(uint64_t addr, uint64_t num_of_exception);
+int xreg_write_callback(unsigned reg, uint64_t value);
+int freg_write_callback(unsigned reg, uint64_t value);
+int csr_write_callback(unsigned reg, uint64_t value);
+int csr_read_callback(unsigned reg, uint64_t value);
+int vreg_write_callback(unsigned reg, lbits value);
+int pc_write_callback(uint64_t value);
+
 /* machine state */
 
 extern uint32_t zcur_privilege;

c_emulator/riscv_sim.c

@@ -89,6 +89,7 @@ bool config_print_reg = true;
 bool config_print_mem_access = true;
 bool config_print_platform = true;
 bool config_print_rvfi = false;
+bool rv_enable_callbacks = true;
 
 void set_config_print(char *var, bool val)
 {
@@ -98,6 +99,7 @@ void set_config_print(char *var, bool val)
  config_print_reg = val;
  config_print_platform = val;
  config_print_rvfi = val;
+ rv_enable_callbacks = val;
  } else if (strcmp("instr", var) == 0) {
  config_print_instr = val;
  } else if (strcmp("reg", var) == 0) {

model/prelude.sail

@@ -71,18 +71,15 @@ val print = "print_endline" : string -> unit
 val print_string = "print_string" : (string, string) -> unit
 
 val print_instr = {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit
-val print_reg = {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit
 val print_mem = {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit
 val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit
 
 val get_config_print_instr = {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool
-val get_config_print_reg = {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool
 val get_config_print_mem = {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool
 
 val get_config_print_platform = {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool
 // defaults for other backends
 function get_config_print_instr () = false
-function get_config_print_reg () = false
 function get_config_print_mem () = false
 function get_config_print_platform () = false
 

model/riscv_fdext_regs.sail

@@ -193,11 +193,8 @@ function wF (r : regno, in_v : flenbits) -> unit = {
  };
 
  dirty_fd_context();
-
- if get_config_print_reg()
- then
- /* TODO: will only print bits; should we print in floating point format? */
- print_reg("f" ^ dec_str(r) ^ " <- " ^ FRegStr(v));
+
+ freg_write_callback(regno_to_regidx(r), in_v);
 }
 
 function rF_bits(i: regidx) -> flenbits = rF(unsigned(i))

model/riscv_insts_vext_mem.sail

@@ -154,7 +154,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
  if i == 0 then { ext_handle_data_check_error(e); return RETIRE_FAIL }
  else {
  vl = to_bits(sizeof(xlen), i);
- print_reg("CSR vl <- " ^ BitStr(vl));
+ csr_write_callback(csr_name_map("vl"), vl);
  trimmed = true
  }
  },
@@ -163,15 +163,15 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
  if i == 0 then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL }
  else {
  vl = to_bits(sizeof(xlen), i);
- print_reg("CSR vl <- " ^ BitStr(vl));
+ csr_write_callback(csr_name_map("vl"), vl);
  trimmed = true
  }
  } else match translateAddr(vaddr, Read(Data)) {
  TR_Failure(e, _) => {
  if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
  else {
  vl = to_bits(sizeof(xlen), i);
- print_reg("CSR vl <- " ^ BitStr(vl));
+ csr_write_callback(csr_name_map("vl"), vl);
  trimmed = true
  }
  },
@@ -182,7 +182,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
  if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
  else {
  vl = to_bits(sizeof(xlen), i);
- print_reg("CSR vl <- " ^ BitStr(vl));
+ csr_write_callback(csr_name_map("vl"), vl);
  trimmed = true
  }
  }

model/riscv_insts_vext_vset.sail

@@ -51,8 +51,8 @@ function handle_illegal_vtype() = {
  */
  vtype.bits = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
  vl = zeros();
- print_reg("CSR vtype <- " ^ BitStr(vtype.bits));
- print_reg("CSR vl <- " ^ BitStr(vl))
+ csr_write_callback(csr_name_map("vtype"), vtype.bits);
+ csr_write_callback(csr_name_map("vl"), vl);
 }
 
 val calculate_new_vl : (int, int) -> xlenbits
@@ -106,9 +106,9 @@ function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = {
  /* reset vstart to 0 */
  vstart = zeros();
 
- print_reg("CSR vtype <- " ^ BitStr(vtype.bits));
- print_reg("CSR vl <- " ^ BitStr(vl));
- print_reg("CSR vstart <- " ^ BitStr(vstart));
+ csr_write_callback(csr_name_map("vtype"), vtype.bits);
+ csr_write_callback(csr_name_map("vl"), vl);
+ csr_write_callback(csr_name_map("vstart"), zero_extend(vstart));
 
  RETIRE_SUCCESS
 }
@@ -157,9 +157,9 @@ function clause execute VSETVL(rs2, rs1, rd) = {
  /* reset vstart to 0 */
  vstart = zeros();
 
- print_reg("CSR vtype <- " ^ BitStr(vtype.bits));
- print_reg("CSR vl <- " ^ BitStr(vl));
- print_reg("CSR vstart <- " ^ BitStr(vstart));
+ csr_write_callback(csr_name_map("vtype"), vtype.bits);
+ csr_write_callback(csr_name_map("vl"), vl);
+ csr_write_callback(csr_name_map("vstart"), zero_extend(vstart));
 
  RETIRE_SUCCESS
 }
@@ -193,9 +193,9 @@ function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = {
  /* reset vstart to 0 */
  vstart = zeros();
 
- print_reg("CSR vtype <- " ^ BitStr(vtype.bits));
- print_reg("CSR vl <- " ^ BitStr(vl));
- print_reg("CSR vstart <- " ^ BitStr(vstart));
+ csr_write_callback(csr_name_map("vtype"), vtype.bits);
+ csr_write_callback(csr_name_map("vl"), vl);
+ csr_write_callback(csr_name_map("vstart"), zero_extend(vstart));
 
  RETIRE_SUCCESS
 }

model/riscv_insts_zicsr.sail

@@ -107,8 +107,7 @@ function readCSR csr : csreg -> xlenbits = {
  zero_extend(0x0) }
  }
  };
- if get_config_print_reg()
- then print_reg("CSR " ^ to_str(csr) ^ " -> " ^ BitStr(res));
+ csr_read_callback(csr, res);
  res
 }
 
@@ -185,8 +184,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
  _ => ext_write_CSR(csr, value)
  };
  match res {
- Some(v) => if get_config_print_reg()
- then print_reg("CSR " ^ to_str(csr) ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")"),
+ Some(v) => csr_write_callback(csr, v),
  None() => print_bits("unhandled write to CSR ", csr)
  }
 }

model/riscv_mem.sail

@@ -117,25 +117,6 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (
 
 /* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */
 
-$ifdef RVFI_DII
-val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit
-function rvfi_read (addr, width, result) = {
- rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr);
- rvfi_mem_data_present = true;
- match result {
- /* TODO: report tag bit for capability writes and extend mask by one bit. */
- MemValue(v, _) => if width <= 16
- then { rvfi_mem_data[rvfi_mem_rdata] = sail_zero_extend(v, 256);
- rvfi_mem_data[rvfi_mem_rmask] = rvfi_encode_width_mask(width) }
- else { internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!") },
- MemException(_) => ()
- };
-}
-$else
-val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit
-function rvfi_read (addr, width, result) = ()
-$endif
-
 val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n))
 val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n))
 val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, int('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta))
@@ -151,7 +132,10 @@ function mem_read_priv_meta (typ, priv, paddr, width, aq, rl, res, meta) = {
  (false, true, true) => throw(Error_not_implemented("lr.rl")),
  (_, _, _) => checked_mem_read(typ, priv, paddr, width, aq, rl, res, meta)
  };
- rvfi_read(paddr, width, result);
+ match result {
+ MemValue(value, _) => mem_read_callback(paddr, width, value),
+ MemException(e) => mem_exception_callback(paddr, num_of_ExceptionType(e))
+ };
  result
 }
 
@@ -172,28 +156,6 @@ function mem_write_ea (addr, width, aq, rl, con) =
  then MemException(E_SAMO_Addr_Align())
  else MemValue(write_ram_ea(write_kind_of_flags(aq, rl, con), addr, width))
 
-$ifdef RVFI_DII
-val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit
-function rvfi_write (addr, width, value, meta, result) = {
- rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr);
- rvfi_mem_data_present = true;
- match result {
- /* Log only the memory address (without the value) if the write fails. */
- MemValue(_) => if width <= 16 then {
- /* TODO: report tag bit for capability writes and extend mask by one bit. */
- rvfi_mem_data[rvfi_mem_wdata] = sail_zero_extend(value,256);
- rvfi_mem_data[rvfi_mem_wmask] = rvfi_encode_width_mask(width);
- } else {
- internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!");
- },
- MemException(_) => ()
- }
-}
-$else
-val rvfi_write : forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit
-function rvfi_write (addr, width, value, meta, result) = ()
-$endif
-
 // only used for actual memory regions, to avoid MMIO effects
 function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : int('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = {
  let result = MemValue(write_ram(wk, paddr, width, data, meta));
@@ -243,7 +205,10 @@ function mem_write_value_priv_meta (paddr, width, value, typ, priv, meta, aq, rl
  then MemException(E_SAMO_Addr_Align())
  else {
  let result = checked_mem_write(paddr, width, value, typ, priv, meta, aq, rl, con);
- rvfi_write(paddr, width, value, meta, result);
+ match result {
+ MemValue(_) => mem_write_callback(paddr, width, value),
+ MemException(e) => mem_exception_callback(paddr, num_of_ExceptionType(e))
+ };
  result
  }
 }

model/riscv_pc_access.sail

@@ -28,5 +28,6 @@ function set_next_pc(pc) = {
 
 val tick_pc : unit -> unit
 function tick_pc() = {
+ pc_write_callback(PC);
  PC = nextPC
 }

model/riscv_regs.sail

@@ -88,16 +88,6 @@ function rX (r : regno) -> xlenbits = {
  regval_from_reg(v)
 }
 
-$ifdef RVFI_DII
-function rvfi_wX (r : regno, v : xlenbits) -> unit = {
- rvfi_int_data[rvfi_rd_wdata] = zero_extend(v);
- rvfi_int_data[rvfi_rd_addr] = to_bits(8,r);
- rvfi_int_data_present = true;
-}
-$else
-function rvfi_wX (r : regno, v : xlenbits) -> unit = ()
-$endif
-
 function wX (r : regno, in_v : xlenbits) -> unit = {
  let v = regval_into_reg(in_v);
  match r {
@@ -136,9 +126,7 @@ function wX (r : regno, in_v : xlenbits) -> unit = {
  _ => assert(false, "invalid register number")
  };
  if (r != 0) then {
- rvfi_wX(r, in_v);
- if get_config_print_reg()
- then print_reg("x" ^ dec_str(r) ^ " <- " ^ RegStr(v));
+ xreg_write_callback(regno_to_regidx(r), in_v);
  }
 }