Implementing callbacks in sail-riscv for state-changing events

1. Added callback functions for XRegs, FRegs, VRegs, PC, CSR, memory writes and CSR, memory reads. 2. Added implementation of callbacks for RVFI records in riscv_rvfi_callbacks.c. 3. Added default callback OCaml-implementations in the file platform.ml.
riscv · Jul 24, 2024 · 5adc0bd · 5adc0bd
1 parent 3ad92a4
commit 5adc0bd
Show file tree

Hide file tree

Showing 20 changed files with 231 additions and 126 deletions.
diff --git a/Makefile b/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)
@@ -313,6 +313,35 @@ generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main
 c_emulator/riscv_rvfi_$(ARCH): generated_definitions/c/riscv_rvfi_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile
  $(CC) -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@
 
+# Note: We have to add -c_preserve since the functions might be optimized out otherwise
+rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \
+ -c_preserve rvfi_get_cmd \
+ -c_preserve rvfi_get_insn \
+ -c_preserve rvfi_get_v2_trace_size \
+ -c_preserve rvfi_get_v2_support_packet \
+ -c_preserve rvfi_get_exec_packet_v1 \
+ -c_preserve rvfi_get_exec_packet_v2 \
+ -c_preserve rvfi_get_mem_data \
+ -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_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) -c_include riscv_rvfi_callbacks.c model/main.sail -o $(basename $@)
+ sed -e '/^[[:space:]]*$$/d' $@ > $@.new
+ mv $@.new $@
+
+c_emulator/riscv_rvfi_$(ARCH): generated_definitions/c/riscv_rvfi_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile
+ gcc -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@
+
 latex: $(SAIL_SRCS) Makefile
  mkdir -p generated_definitions/latex
  $(SAIL) -latex -latex_prefix sail -o generated_definitions/latex $(SAIL_SRCS)

diff --git a/c_emulator/riscv_default_callbacks.c b/c_emulator/riscv_default_callbacks.c
@@ -0,0 +1,16 @@
+/* The model assumes that these functions do not change the state of the model.
+ */
+int mem_update_callback(uint64_t addr, uint64_t width, lbits value,
+ bool is_exception)
+{
+}
+int mem_read_callback(uint64_t addr, uint64_t width, lbits value,
+ bool is_exception)
+{
+}
+int xreg_update_callback(unsigned reg, uint64_t value) { }
+int freg_update_callback(unsigned reg, uint64_t value) { }
+int csr_update_callback(const char *reg_name, uint64_t value) { }
+int csr_read_callback(const char *reg_name, uint64_t value) { }
+int vreg_update_callback(unsigned reg, lbits value) { }
+int pc_update_callback(uint64_t value) { }
diff --git a/c_emulator/riscv_rvfi_callbacks.c b/c_emulator/riscv_rvfi_callbacks.c
@@ -0,0 +1,27 @@
+int zrvfi_write(uint64_t addr, int64_t width, lbits value, bool is_exception);
+int zrvfi_read(uint64_t addr, sail_int width, lbits value, bool is_exception);
+int zrvfi_wX(int64_t reg, uint64_t value);
+
+int mem_update_callback(uint64_t addr, uint64_t width, lbits value,
+ bool is_exception)
+{
+ zrvfi_write(addr, width, value, is_exception);
+}
+int mem_read_callback(uint64_t addr, uint64_t width, lbits value,
+ bool is_exception)
+{
+ sail_int len;
+ CREATE(sail_int)(&len);
+ CONVERT_OF(sail_int, mach_int)(&len, width);
+ zrvfi_read(addr, len, value, is_exception);
+ KILL(sail_int)(&len);
+}
+int xreg_update_callback(unsigned reg, uint64_t value)
+{
+ zrvfi_wX(reg, value);
+}
+int freg_update_callback(unsigned reg, uint64_t value) { }
+int csr_update_callback(const char *reg_name, uint64_t value) { }
+int csr_read_callback(const char *reg_name, uint64_t value) { }
+int vreg_update_callback(unsigned reg, lbits value) { }
+int pc_update_callback(uint64_t value) { }
diff --git a/c_emulator/riscv_sail.h b/c_emulator/riscv_sail.h
@@ -50,6 +50,22 @@ extern bool zhtif_done;
 extern mach_bits zhtif_exit_code;
 extern bool have_exception;
 
+/* Callbacks for state-changing events */
+
+/* Whether need to call the callback functions */
+extern bool zrv_enable_callbacks;
+/* The model assumes that these functions do not change the state of the model.
+ */
+int mem_update_callback(uint64_t addr, uint64_t width, lbits value,
+ bool is_exception);
+int mem_read_callback(uint64_t addr, uint64_t width, lbits value,
+ bool is_exception);
+int xreg_update_callback(unsigned reg, uint64_t value);
+int freg_update_callback(unsigned reg, uint64_t value);
+int csr_update_callback(const char *reg_name, uint64_t value);
+int vreg_update_callback(unsigned reg, lbits value);
+int pc_update_callback(uint64_t value);
+
 /* machine state */
 
 extern uint32_t zcur_privilege;

diff --git a/model/prelude.sail b/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
 

diff --git a/model/riscv_csr_ext.sail b/model/riscv_csr_ext.sail
@@ -22,3 +22,18 @@ end ext_read_CSR
 
 function clause ext_write_CSR (_, _) = None()
 end ext_write_CSR
+
+function ext_notification_read_CSR (csr : csreg) -> option(xlenbits) = {
+ let res = ext_read_CSR(csr);
+ if rv_enable_callbacks then
+ match res {
+ Some(value) => csr_read_callback(csr_name_map(csr), value),
+ None() => (),
+ };
+ res
+}
+
+function ext_notification_write_CSR (csr : csreg, value : xlenbits) -> unit = {
+ let res = ext_write_CSR(csr, value);
+ if rv_enable_callbacks then csr_update_callback(csr_name_map(csr), value)
+}
diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail
@@ -155,6 +155,7 @@ function rF (r : regno) -> flenbits = {
 
 function wF (r : regno, in_v : flenbits) -> unit = {
  assert(sys_enable_fdext());
+ if rv_enable_callbacks then freg_update_callback(regno_to_regidx(r), in_v);
  let v = fregval_into_freg(in_v);
  match r {
  0 => f0 = v,
@@ -193,11 +194,6 @@ 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));
 }
 
 function rF_bits(i: regidx) -> flenbits = rF(unsigned(i))

diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail
@@ -153,25 +153,22 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
  Ext_DataAddr_Error(e) => {
  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));
+ ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i));
  trimmed = true
  }
  },
  Ext_DataAddr_OK(vaddr) => {
  if check_misaligned(vaddr, width_type) then {
  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));
+ ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i));
  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));
+ ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i));
  trimmed = true
  }
  },
@@ -181,8 +178,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
  MemException(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));
+ ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i));
  trimmed = true
  }
  }

diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail
@@ -49,10 +49,10 @@ function handle_illegal_vtype() = {
  /* Note: Implementations can set vill or trap if the vtype setting is not supported.
  * TODO: configuration support for both solutions
  */
- 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))
+ let new_vtype = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
+
+ ext_notification_write_CSR(csr_name_map("vtype"), new_vtype);
+ ext_notification_write_CSR(csr_name_map("vl"), zeros())
 }
 
 val calculate_new_vl : (int, int) -> xlenbits
@@ -77,7 +77,8 @@ function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = {
  let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori;
 
  /* set vtype */
- vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul;
+ let new_vtype = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul;
+ ext_notification_write_CSR(csr_name_map("vtype"), new_vtype);
 
  /* check new SEW and LMUL are legal and calculate VLMAX */
  let VLEN_pow = get_vlen_pow();
@@ -91,11 +92,11 @@ function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = {
  if (rs1 != 0b00000) then { /* normal stripmining */
  let rs1_val = X(rs1);
  let AVL = unsigned(rs1_val);
- vl = calculate_new_vl(AVL, VLMAX);
+ ext_notification_write_CSR(csr_name_map("vl"), calculate_new_vl(AVL, VLMAX));
  X(rd) = vl;
  } else if (rd != 0b00000) then { /* set vl to VLMAX */
  let AVL = unsigned(ones(sizeof(xlen)));
- vl = to_bits(sizeof(xlen), VLMAX);
+ ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), VLMAX));
  X(rd) = vl;
  } else { /* keep existing vl */
  let AVL = unsigned(vl);
@@ -104,11 +105,7 @@ 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));
+ ext_notification_write_CSR(csr_name_map("vstart"), zeros());
 
  RETIRE_SUCCESS
 }
@@ -128,7 +125,8 @@ function clause execute VSETVL(rs2, rs1, rd) = {
  let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori;
 
  /* set vtype */
- vtype.bits = X(rs2);
+ let new_vtype = X(rs2);
+ ext_notification_write_CSR(csr_name_map("vtype"), new_vtype);
 
  /* check new SEW and LMUL are legal and calculate VLMAX */
  let VLEN_pow = get_vlen_pow();
@@ -142,11 +140,11 @@ function clause execute VSETVL(rs2, rs1, rd) = {
  if (rs1 != 0b00000) then { /* normal stripmining */
  let rs1_val = X(rs1);
  let AVL = unsigned(rs1_val);
- vl = calculate_new_vl(AVL, VLMAX);
+ ext_notification_write_CSR(csr_name_map("vl"), calculate_new_vl(AVL, VLMAX));
  X(rd) = vl;
  } else if (rd != 0b00000) then { /* set vl to VLMAX */
  let AVL = unsigned(ones(sizeof(xlen)));
- vl = to_bits(sizeof(xlen), VLMAX);
+ ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), VLMAX));
  X(rd) = vl;
  } else { /* keep existing vl */
  let AVL = unsigned(vl);
@@ -155,11 +153,7 @@ 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));
+ ext_notification_write_CSR(csr_name_map("vstart"), zeros());
 
  RETIRE_SUCCESS
 }
@@ -175,7 +169,8 @@ mapping clause encdec = VSETIVLI(ma, ta, sew, lmul, uimm, rd) if extensionEnable
 
 function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = {
  /* set vtype */
- vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul;
+ let new_vtype = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul;
+ ext_notification_write_CSR(csr_name_map("vtype"), new_vtype);
 
  /* check new SEW and LMUL are legal and calculate VLMAX */
  let VLEN_pow = get_vlen_pow();
@@ -187,15 +182,11 @@ function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = {
 
  /* set vl according to VLMAX and AVL */
  let AVL = unsigned(uimm); /* AVL is encoded as 5-bit zero-extended imm in the rs1 field */
- vl = calculate_new_vl(AVL, VLMAX);
+ ext_notification_write_CSR(csr_name_map("vl"), calculate_new_vl(AVL, VLMAX));
  X(rd) = vl;
 
  /* 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));
+ ext_notification_write_CSR(csr_name_map("vstart"), zeros());
 
  RETIRE_SUCCESS
 }

diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
@@ -101,18 +101,17 @@ function readCSR csr : csreg -> xlenbits = {
  (0x015, _) => read_seed_csr(),
 
  _ => /* check extensions */
- match ext_read_CSR(csr) {
+ match ext_notification_read_CSR(csr) {
  Some(res) => res,
  None() => { print_bits("unhandled read to CSR ", csr);
  zero_extend(0x0) }
  }
  };
- if get_config_print_reg()
- then print_reg("CSR " ^ to_str(csr) ^ " -> " ^ BitStr(res));
  res
 }
 
 function writeCSR (csr : csreg, value : xlenbits) -> unit = {
+ if rv_enable_callbacks then csr_update_callback(csr_name_map(csr), value);
  let res : option(xlenbits) =
  match (csr, sizeof(xlen)) {
  /* machine mode */
@@ -184,11 +183,6 @@ 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) ^ ")"),
- None() => print_bits("unhandled write to CSR ", csr)
- }
 }
 
 function clause execute CSR(csr, rs1, rd, is_imm, op) = {