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.

Makefile

@@ -227,11 +227,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)
@@ -257,13 +257,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

@@ -6,3 +6,4 @@ extern bool config_print_step;
 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

@@ -93,6 +93,7 @@ bool config_print_mem_access = true;
 bool config_print_platform = true;
 bool config_print_rvfi = false;
 bool config_print_step = false;
+bool rv_enable_callbacks = true;
 
 void set_config_print(char *var, bool val)
 {
@@ -102,6 +103,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

@@ -76,7 +76,6 @@ val get_config_print_mem = pure {c:"get_config_print_mem"} : unit -> bool
 val get_config_print_platform = pure {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(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(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(xlen, i);
-                    print_reg("CSR vl <- " ^ BitStr(vl));
+                    csr_write_callback(csr_name_map("vl"), vl);
                     trimmed = true
                   }
                 },
@@ -182,7 +182,8 @@ 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(xlen, i);
-                        print_reg("CSR vl <- " ^ BitStr(vl));
+                        csr_write_callback(csr_name_map("vl"), vl);
+>>>>>>> cb0b429d (Implementing callbacks in sail-riscv for state-changing events)
                         trimmed = true
                       }
                     }

model/riscv_insts_vext_vset.sail

@@ -51,8 +51,8 @@ function handle_illegal_vtype() = {
    */
   vtype.bits = 0b1 @ zeros(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

@@ -197,11 +197,9 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) = {
         CSRRC => csr_val & ~(rs1_val)
       };
       let final_val = write_CSR(csr, new_val);
-      if get_config_print_reg()
-      then print_reg("CSR " ^ to_str(csr) ^ " <- " ^ bits_str(final_val) ^ " (input: " ^ bits_str(new_val) ^ ")")
+      csr_write_callback(csr, final_val);
     } else {
-      if get_config_print_reg()
-      then print_reg("CSR " ^ to_str(csr) ^ " -> " ^ bits_str(csr_val));
+      csr_read_callback(csr, csr_val);
     };
     X(rd) = csr_val;
     RETIRE_SUCCESS

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);
   }
 }