Skip to content

Commit 3bdcf27

Browse files
kseniadobrovolskayajordancarlinTim Hutt
authored
Implement callbacks for state-changing events (#494)
Add a callback API for register, PC and CSR updates, memory writes and traps. This is used for logging and RVFI instead of embedding that code in the model itself. Co-authored-by: Jordan Carlin <jordanmcarlin@gmail.com> Co-authored-by: Tim Hutt <timothy.hutt@codasip.com>
1 parent 3759ebb commit 3bdcf27

20 files changed

+346
-157
lines changed

c_emulator/CMakeLists.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
11
set(EMULATOR_COMMON_SRCS
2+
riscv_callbacks.cpp
3+
riscv_callbacks.h
24
riscv_config.h
35
riscv_platform.cpp
46
riscv_platform.h

c_emulator/riscv_callbacks.cpp

Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
1+
#include "riscv_callbacks.h"
2+
#include "riscv_config.h"
3+
#include "riscv_platform_impl.h"
4+
#include <stdlib.h>
5+
#include <vector>
6+
#include <inttypes.h>
7+
8+
bool config_enable_rvfi = true; // Only used if RVFI_DII is defined
9+
10+
void print_lbits_hex(lbits val, int length = 0)
11+
{
12+
if (length == 0) {
13+
length = val.len;
14+
}
15+
std::vector<uint8_t> data(length);
16+
mpz_export(data.data(), nullptr, -1, 1, 0, 0, *val.bits);
17+
for (int i = length - 1; i >= 0; --i) {
18+
fprintf(trace_log, "%02" PRIX8, data[i]);
19+
}
20+
fprintf(trace_log, "\n");
21+
}
22+
23+
// Implementations of default callbacks for trace printing and RVFI.
24+
// The model assumes that these functions do not change the state of the model.
25+
unit mem_write_callback(uint64_t paddr, uint64_t width, lbits value)
26+
{
27+
if (config_print_mem_access) {
28+
fprintf(trace_log, "mem[0x%016" PRIX64 "] <- 0x", paddr);
29+
print_lbits_hex(value, width);
30+
}
31+
#ifdef RVFI_DII
32+
if (config_enable_rvfi) {
33+
zrvfi_write(paddr, width, value);
34+
}
35+
#endif
36+
return UNIT;
37+
}
38+
39+
unit mem_read_callback(const char *type, uint64_t paddr, uint64_t width,
40+
lbits value)
41+
{
42+
if (config_print_mem_access) {
43+
fprintf(trace_log, "mem[%s,0x%016" PRIX64 "] -> 0x", type, paddr);
44+
print_lbits_hex(value, width);
45+
}
46+
#ifdef RVFI_DII
47+
if (config_enable_rvfi) {
48+
sail_int len;
49+
CREATE(sail_int)(&len);
50+
CONVERT_OF(sail_int, mach_int)(&len, width);
51+
zrvfi_read(paddr, len, value);
52+
KILL(sail_int)(&len);
53+
}
54+
#endif
55+
return UNIT;
56+
}
57+
58+
unit mem_exception_callback(uint64_t paddr, uint64_t num_of_exception)
59+
{
60+
(void)num_of_exception;
61+
#ifdef RVFI_DII
62+
if (config_enable_rvfi) {
63+
zrvfi_mem_exception(paddr);
64+
}
65+
#else
66+
(void)paddr;
67+
#endif
68+
return UNIT;
69+
}
70+
71+
unit xreg_write_callback(unsigned reg, uint64_t value)
72+
{
73+
if (config_print_reg) {
74+
fprintf(trace_log, "x%d <- 0x%016" PRIX64 "\n", reg, value);
75+
}
76+
#ifdef RVFI_DII
77+
if (config_enable_rvfi) {
78+
zrvfi_wX(reg, value);
79+
}
80+
#endif
81+
return UNIT;
82+
}
83+
84+
unit freg_write_callback(unsigned reg, uint64_t value)
85+
{
86+
// TODO: will only print bits; should we print in floating point format?
87+
if (config_print_reg) {
88+
fprintf(trace_log, "f%d <- 0x%016" PRIX64 "\n", reg, value);
89+
}
90+
return UNIT;
91+
}
92+
93+
unit csr_full_write_callback(const_sail_string csr_name, unsigned reg,
94+
uint64_t value)
95+
{
96+
if (config_print_reg) {
97+
fprintf(trace_log, "CSR %s (0x%03X) <- 0x%016" PRIX64 "\n", csr_name, reg,
98+
value);
99+
}
100+
return UNIT;
101+
}
102+
103+
unit csr_full_read_callback(const_sail_string csr_name, unsigned reg,
104+
uint64_t value)
105+
{
106+
if (config_print_reg) {
107+
fprintf(trace_log, "CSR %s (0x%03X) -> 0x%016" PRIX64 "\n", csr_name, reg,
108+
value);
109+
}
110+
return UNIT;
111+
}
112+
113+
unit vreg_write_callback(unsigned reg, lbits value)
114+
{
115+
if (config_print_reg) {
116+
fprintf(trace_log, "v%d <- ", reg);
117+
print_lbits_hex(value);
118+
}
119+
return UNIT;
120+
}
121+
122+
unit pc_write_callback(uint64_t value)
123+
{
124+
(void)value;
125+
return UNIT;
126+
}
127+
128+
unit trap_callback(unit)
129+
{
130+
#ifdef RVFI_DII
131+
if (config_enable_rvfi) {
132+
zrvfi_trap();
133+
}
134+
#endif
135+
return UNIT;
136+
}

c_emulator/riscv_callbacks.h

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
#pragma once
2+
#include "sail.h"
3+
4+
#ifdef __cplusplus
5+
extern "C" {
6+
#endif
7+
8+
unit mem_write_callback(uint64_t paddr, uint64_t width, lbits value);
9+
unit mem_read_callback(const char *type, uint64_t paddr, uint64_t width,
10+
lbits value);
11+
unit mem_exception_callback(uint64_t paddr, uint64_t num_of_exception);
12+
unit xreg_write_callback(unsigned reg, uint64_t value);
13+
unit freg_write_callback(unsigned reg, uint64_t value);
14+
// `full` indicates that the name and index of the CSR are provided.
15+
// 64 bit CSRs use a long_csr_write_callback Sail function that automatically
16+
// makes two csr_full_write_callback calls on RV32.
17+
unit csr_full_write_callback(const_sail_string csr_name, unsigned reg,
18+
uint64_t value);
19+
unit csr_full_read_callback(const_sail_string csr_name, unsigned reg,
20+
uint64_t value);
21+
unit vreg_write_callback(unsigned reg, lbits value);
22+
unit pc_write_callback(uint64_t value);
23+
unit trap_callback(unit);
24+
25+
#ifdef RVFI_DII
26+
// TODO: Move these implementations to C.
27+
unit zrvfi_write(uint64_t paddr, int64_t width, lbits value);
28+
unit zrvfi_read(uint64_t paddr, sail_int width, lbits value);
29+
unit zrvfi_mem_exception(uint64_t paddr);
30+
unit zrvfi_wX(int64_t reg, uint64_t value);
31+
unit zrvfi_trap();
32+
#endif
33+
34+
#ifdef __cplusplus
35+
}
36+
#endif

c_emulator/riscv_prelude.cpp

Lines changed: 2 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -22,20 +22,6 @@ unit print_step(unit)
2222
return UNIT;
2323
}
2424

25-
unit print_reg(sail_string s)
26-
{
27-
if (config_print_reg)
28-
fprintf(trace_log, "%s\n", s);
29-
return UNIT;
30-
}
31-
32-
unit print_mem_access(sail_string s)
33-
{
34-
if (config_print_mem_access)
35-
fprintf(trace_log, "%s\n", s);
36-
return UNIT;
37-
}
38-
3925
unit print_platform(sail_string s)
4026
{
4127
if (config_print_platform)
@@ -45,20 +31,10 @@ unit print_platform(sail_string s)
4531

4632
bool get_config_print_instr(unit)
4733
{
48-
return (config_print_instr) ? true : false;
49-
}
50-
51-
bool get_config_print_reg(unit)
52-
{
53-
return (config_print_reg) ? true : false;
54-
}
55-
56-
bool get_config_print_mem(unit)
57-
{
58-
return (config_print_mem_access) ? true : false;
34+
return config_print_instr;
5935
}
6036

6137
bool get_config_print_platform(unit)
6238
{
63-
return (config_print_platform) ? true : false;
39+
return config_print_platform;
6440
}

c_emulator/riscv_prelude.h

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -11,13 +11,9 @@ unit print_string(sail_string prefix, sail_string msg);
1111

1212
unit print_instr(sail_string s);
1313
unit print_step(unit);
14-
unit print_reg(sail_string s);
15-
unit print_mem_access(sail_string s);
1614
unit print_platform(sail_string s);
1715

1816
bool get_config_print_instr(unit);
19-
bool get_config_print_reg(unit);
20-
bool get_config_print_mem(unit);
2117
bool get_config_print_platform(unit);
2218

2319
#ifdef __cplusplus

model/CMakeLists.txt

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -155,6 +155,7 @@ foreach (xlen IN ITEMS 32 64)
155155

156156
set(sail_regs_srcs
157157
"riscv_csr_begin.sail"
158+
"riscv_callbacks.sail"
158159
"riscv_reg_type.sail"
159160
"riscv_freg_type.sail"
160161
"riscv_regs.sail"
@@ -263,6 +264,7 @@ foreach (xlen IN ITEMS 32 64)
263264
# Extra #include's.
264265
--c-include riscv_prelude.h
265266
--c-include riscv_platform.h
267+
--c-include riscv_callbacks.h
266268
# Don't dead-code eliminate these functions. These should match the
267269
# ones used from riscv_sail.h
268270
--c-preserve init_model
@@ -283,6 +285,11 @@ foreach (xlen IN ITEMS 32 64)
283285
--c-preserve rvfi_halt_exec_packet
284286
--c-preserve print_instr_packet
285287
--c-preserve print_rvfi_exec
288+
--c-preserve rvfi_write
289+
--c-preserve rvfi_read
290+
--c-preserve rvfi_mem_exception
291+
--c-preserve rvfi_wX
292+
--c-preserve rvfi_trap
286293
# Input files.
287294
${sail_srcs}
288295
)

model/prelude.sail

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -62,23 +62,16 @@ overload max = {max_int}
6262
val print_string = pure "print_string" : (string, string) -> unit
6363

6464
val print_instr = pure {interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit
65-
val print_reg = pure {interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit
66-
val print_mem = pure {interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit
6765
val print_platform = pure {interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit
6866

6967
val print_step = pure {c: "print_step"} : unit -> unit
7068

7169
function print_step() = ()
7270

7371
val get_config_print_instr = pure {c:"get_config_print_instr"} : unit -> bool
74-
val get_config_print_reg = pure {c:"get_config_print_reg"} : unit -> bool
75-
val get_config_print_mem = pure {c:"get_config_print_mem"} : unit -> bool
76-
7772
val get_config_print_platform = pure {c:"get_config_print_platform"} : unit -> bool
7873
// defaults for other backends
7974
function get_config_print_instr () = false
80-
function get_config_print_reg () = false
81-
function get_config_print_mem () = false
8275
function get_config_print_platform () = false
8376

8477
val sign_extend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)

model/riscv_callbacks.sail

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
/*=======================================================================================*/
2+
/* This Sail RISC-V architecture model, comprising all files and */
3+
/* directories except where otherwise noted is subject the BSD */
4+
/* two-clause license in the LICENSE file. */
5+
/* */
6+
/* SPDX-License-Identifier: BSD-2-Clause */
7+
/*=======================================================================================*/
8+
9+
// Callbacks for state-changing events
10+
val mem_write_callback = pure {c: "mem_write_callback"} : forall 'n, 0 < 'n <= max_mem_access . (/* addr */ physaddrbits, /* width */ int('n), /* value */ bits(8 * 'n)) -> unit
11+
val mem_read_callback = pure {c: "mem_read_callback"} : forall 'n, 0 < 'n <= max_mem_access . (/* access type */ string, /* addr */ physaddrbits, /* width */ int('n), /* value */ bits(8 * 'n)) -> unit
12+
val mem_exception_callback = pure {c: "mem_exception_callback"} : forall 'n, 0 <= 'n < xlen . (/* addr */ physaddrbits, /* num_of_ExceptionType */ int('n)) -> unit
13+
val pc_write_callback = pure {c: "pc_write_callback"} : xlenbits -> unit
14+
val xreg_write_callback = pure {c: "xreg_write_callback"} : (regidx, xlenbits) -> unit
15+
val csr_full_write_callback = pure {c: "csr_full_write_callback"} : (string, csreg, xlenbits) -> unit
16+
val csr_full_read_callback = pure {c: "csr_full_read_callback"} : (string, csreg, xlenbits) -> unit
17+
val trap_callback = pure {c: "trap_callback"} : unit -> unit
18+
19+
// Overloads for easier use of callbacks
20+
function csr_name_write_callback(name : string, value : xlenbits) -> unit = {
21+
let csr = csr_name_map(name);
22+
csr_full_write_callback(name, csr, value);
23+
}
24+
function csr_id_write_callback(csr : csreg, value : xlenbits) -> unit = {
25+
let name = csr_name_map(csr);
26+
csr_full_write_callback(name, csr, value);
27+
}
28+
function csr_name_read_callback(name : string, value : xlenbits) -> unit = {
29+
let csr = csr_name_map(name);
30+
csr_full_read_callback(name, csr, value);
31+
}
32+
function csr_id_read_callback(csr : csreg, value : xlenbits) -> unit = {
33+
let name = csr_name_map(csr);
34+
csr_full_read_callback(name, csr, value);
35+
}
36+
37+
overload csr_write_callback = {csr_name_write_callback, csr_id_write_callback, csr_full_write_callback}
38+
overload csr_read_callback = {csr_name_read_callback, csr_id_read_callback, csr_full_read_callback}
39+
40+
function long_csr_write_callback(name : string, name_high : string, value : bits(64)) -> unit = {
41+
csr_write_callback(name, value[xlen - 1 .. 0]);
42+
if xlen == 32
43+
then csr_write_callback(name_high, value[63 .. 32]);
44+
}

model/riscv_fdext_regs.sail

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,7 @@ function nan_unbox(m, x) = if 'n == 'm then x else (
5555
newtype fregidx = Fregidx : bits(5)
5656
newtype fregno = Fregno : range(0, 31)
5757
function fregidx_to_fregno (Fregidx(b) : fregidx) -> fregno = Fregno(unsigned(b))
58+
function fregno_to_fregidx (Fregno(b) : fregno) -> fregidx = Fregidx(to_bits(5, b))
5859
function fregidx_offset(Fregidx(r) : fregidx, o : bits(5)) -> fregidx = Fregidx(r + o)
5960
function fregidx_bits(Fregidx(r) : fregidx) -> bits(5) = r
6061

@@ -69,6 +70,8 @@ function fregidx_to_regidx (Fregidx(b) : fregidx) -> regidx =
6970

7071
mapping encdec_freg : fregidx <-> bits(5) = { Fregidx(r) <-> r }
7172

73+
val freg_write_callback = pure {c: "freg_write_callback"} : (fregidx, flenbits) -> unit
74+
7275
register f0 : fregtype
7376
register f1 : fregtype
7477
register f2 : fregtype
@@ -106,6 +109,7 @@ function dirty_fd_context() -> unit = {
106109
assert(hartSupports(Ext_F));
107110
mstatus[FS] = extStatus_to_bits(Dirty);
108111
mstatus[SD] = 0b1;
112+
long_csr_write_callback("mstatus", "mstatush", mstatus.bits);
109113
}
110114

111115
function dirty_fd_context_if_present() -> unit = {
@@ -193,12 +197,8 @@ function wF (Fregno(r) : fregno, in_v : flenbits) -> unit = {
193197
_ => assert(false, "invalid floating point register number")
194198
};
195199

200+
freg_write_callback(fregno_to_fregidx(Fregno(r)), in_v);
196201
dirty_fd_context();
197-
198-
if get_config_print_reg()
199-
then
200-
/* TODO: will only print bits; should we print in floating point format? */
201-
print_reg("f" ^ dec_str(r) ^ " <- " ^ FRegStr(v));
202202
}
203203

204204
function rF_bits(i: fregidx) -> flenbits = rF(fregidx_to_fregno(i))

0 commit comments

Comments
 (0)