From 1bd4fa63b21b2a37a3357bb4f0a6fef5482074f2 Mon Sep 17 00:00:00 2001 From: Peter Rugg Date: Wed, 19 Jul 2023 15:42:57 +0100 Subject: [PATCH] Allow compressed hints to be expanded This leads to different values in RVFI. The RISC-V spec allows this behaviour: "simple implementations can ... execute a HINT as a regular computational instruction". Without this feature, such implementations cannot be verified using RVFI. --- c_emulator/riscv_platform.c | 5 ++++ c_emulator/riscv_platform.h | 1 + c_emulator/riscv_platform_impl.c | 1 + c_emulator/riscv_platform_impl.h | 1 + c_emulator/riscv_sim.c | 6 +++++ model/riscv_insts_hints.sail | 40 ++++++++++++++++++++++++------- model/riscv_platform.sail | 6 +++++ ocaml_emulator/platform.ml | 2 ++ ocaml_emulator/riscv_ocaml_sim.ml | 3 +++ 9 files changed, 57 insertions(+), 8 deletions(-) diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 917a36a95..f42bbf44d 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -57,6 +57,11 @@ bool plat_mtval_has_illegal_inst_bits(unit u) return rv_mtval_has_illegal_inst_bits; } +bool plat_c_hints_expand(unit u) +{ + return rv_c_hints_expand; +} + bool plat_enable_pmp(unit u) { return rv_enable_pmp; diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index aec59d017..a5c00fb85 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -10,6 +10,7 @@ bool sys_enable_writable_misa(unit); bool plat_enable_dirty_update(unit); bool plat_enable_misaligned_access(unit); bool plat_mtval_has_illegal_inst_bits(unit); +bool plat_c_hints_expand(unit); bool plat_enable_pmp(unit); mach_bits plat_ram_base(unit); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index 148c72bd4..4b81b8823 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -13,6 +13,7 @@ bool rv_enable_fdext = true; bool rv_enable_dirty_update = false; bool rv_enable_misaligned = false; bool rv_mtval_has_illegal_inst_bits = false; +bool rv_c_hints_expand = false; uint64_t rv_ram_base = UINT64_C(0x80000000); uint64_t rv_ram_size = UINT64_C(0x4000000); diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h index d24ecc8fb..c47455553 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -16,6 +16,7 @@ extern bool rv_enable_writable_misa; extern bool rv_enable_dirty_update; extern bool rv_enable_misaligned; extern bool rv_mtval_has_illegal_inst_bits; +extern bool rv_c_hints_expand; extern uint64_t rv_ram_base; extern uint64_t rv_ram_size; diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index fdb9ce01d..52129daf9 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -120,6 +120,7 @@ static struct option options[] = { {"disable-writable-misa", no_argument, 0, 'I'}, {"disable-fdext", no_argument, 0, 'F'}, {"mtval-has-illegal-inst-bits", no_argument, 0, 'i'}, + {"c_hints_expand", no_argument, 0, 'H'}, {"device-tree-blob", required_argument, 0, 'b'}, {"terminal-log", required_argument, 0, 't'}, {"show-times", required_argument, 0, 'p'}, @@ -232,6 +233,7 @@ char *process_args(int argc, char **argv) "I" "F" "i" + "H" "s" "p" "z:" @@ -289,6 +291,10 @@ char *process_args(int argc, char **argv) fprintf(stderr, "enabling storing illegal instruction bits in mtval.\n"); rv_mtval_has_illegal_inst_bits = true; break; + case 'H': + fprintf(stderr, "enabling expanding of compressed hints.\n"); + rv_c_hints_expand = true; + break; case 's': do_dump_dts = true; break; diff --git a/model/riscv_insts_hints.sail b/model/riscv_insts_hints.sail index bc803fae5..0c427ef6c 100644 --- a/model/riscv_insts_hints.sail +++ b/model/riscv_insts_hints.sail @@ -92,7 +92,9 @@ mapping clause encdec_compressed = C_ADDI_HINT(rsd) <-> 0b000 @ 0b0 @ rsd : regidx @ 0b00000 @ 0b01 if rsd != zreg -function clause execute (C_ADDI_HINT(rsd)) = RETIRE_SUCCESS +function clause execute (C_ADDI_HINT(rsd)) = + if plat_c_hints_expand() then execute(ITYPE(0b000000000000, rsd, rsd, RISCV_ADDI)) + else RETIRE_SUCCESS mapping clause assembly = C_ADDI_HINT(rsd) if rsd != zreg @@ -105,7 +107,11 @@ union clause ast = C_LI_HINT : (bits(6)) mapping clause encdec_compressed = C_LI_HINT(imm5 @ imm40) <-> 0b010 @ imm5 : bits(1) @ 0b00000 @ imm40 : bits(5) @ 0b01 -function clause execute (C_LI_HINT(imm)) = RETIRE_SUCCESS +function clause execute (C_LI_HINT(imm)) = + if plat_c_hints_expand() then { + let imm : bits(12) = EXTS(imm); + execute(ITYPE(imm, zreg, zreg, RISCV_ADDI)) + } else RETIRE_SUCCESS mapping clause assembly = C_LI_HINT(imm) <-> "c.li.hint." ^ hex_bits_6(imm) @@ -118,7 +124,11 @@ mapping clause encdec_compressed = C_LUI_HINT(imm17 @ imm1612) <-> 0b011 @ imm17 : bits(1) @ 0b00000 @ imm1612 : bits(5) @ 0b01 if imm17 @ imm1612 != 0b000000 -function clause execute (C_LUI_HINT(imm)) = RETIRE_SUCCESS +function clause execute (C_LUI_HINT(imm)) = + if plat_c_hints_expand() then { + let res : bits(20) = EXTS(imm); + execute(UTYPE(res, zreg, RISCV_LUI)); + } else RETIRE_SUCCESS mapping clause assembly = C_LUI_HINT(imm) if imm != 0b000000 @@ -133,7 +143,9 @@ mapping clause encdec_compressed = C_MV_HINT(rs2) <-> 0b100 @ 0b0 @ 0b00000 @ rs2 : regidx @ 0b10 if rs2 != zreg -function clause execute (C_MV_HINT(rs2)) = RETIRE_SUCCESS +function clause execute (C_MV_HINT(rs2)) = + if plat_c_hints_expand() then execute(RTYPE(rs2, zreg, zreg, RISCV_ADD)) + else RETIRE_SUCCESS mapping clause assembly = C_MV_HINT(rs2) if rs2 != zreg @@ -148,7 +160,9 @@ mapping clause encdec_compressed = C_ADD_HINT(rs2) <-> 0b100 @ 0b1 @ 0b00000 @ rs2 : regidx @ 0b10 if rs2 != zreg -function clause execute (C_ADD_HINT(rs2)) = RETIRE_SUCCESS +function clause execute (C_ADD_HINT(rs2)) = + if plat_c_hints_expand() then execute(RTYPE(rs2, zreg, zreg, RISCV_ADD)) + else RETIRE_SUCCESS mapping clause assembly = C_ADD_HINT(rs2) if rs2 != zreg @@ -163,7 +177,9 @@ mapping clause encdec_compressed = C_SLLI_HINT(nzui5 @ nzui40, rsd) <-> 0b000 @ nzui5 : bits(1) @ rsd : regidx @ nzui40 : bits(5) @ 0b10 if (nzui5 @ nzui40 == 0b000000 | rsd == zreg) & (sizeof(xlen) == 64 | nzui5 == 0b0) -function clause execute (C_SLLI_HINT(shamt, rsd)) = RETIRE_SUCCESS +function clause execute (C_SLLI_HINT(shamt, rsd)) = + if plat_c_hints_expand() then execute(SHIFTIOP(shamt, rsd, rsd, RISCV_SLLI)) + else RETIRE_SUCCESS mapping clause assembly = C_SLLI_HINT(shamt, rsd) if shamt == 0b000000 | rsd == zreg @@ -176,7 +192,11 @@ union clause ast = C_SRLI_HINT : (cregidx) mapping clause encdec_compressed = C_SRLI_HINT(rsd) <-> 0b100 @ 0b0 @ 0b00 @ rsd : cregidx @ 0b00000 @ 0b01 -function clause execute (C_SRLI_HINT(rsd)) = RETIRE_SUCCESS +function clause execute (C_SRLI_HINT(rsd)) = + if plat_c_hints_expand() then { + let rsd = creg2reg_idx(rsd); + execute(SHIFTIOP(0b000000, rsd, rsd, RISCV_SRLI)) + } else RETIRE_SUCCESS mapping clause assembly = C_SRLI_HINT(rsd) <-> "c.srli.hint." ^ creg_name(rsd) @@ -187,7 +207,11 @@ union clause ast = C_SRAI_HINT : (cregidx) mapping clause encdec_compressed = C_SRAI_HINT(rsd) <-> 0b100 @ 0b0 @ 0b01 @ rsd : cregidx @ 0b00000 @ 0b01 -function clause execute (C_SRAI_HINT(rsd)) = RETIRE_SUCCESS +function clause execute (C_SRAI_HINT(rsd)) = + if plat_c_hints_expand() then { + let rsd = creg2reg_idx(rsd); + execute(SHIFTIOP(0b000000, rsd, rsd, RISCV_SRAI)) + } else RETIRE_SUCCESS mapping clause assembly = C_SRAI_HINT(rsd) <-> "c.srai.hint." ^ creg_name(rsd) diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index aed996626..5b2939b77 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -118,6 +118,12 @@ val plat_mtval_has_illegal_inst_bits = {ocaml: "Platform.mtval_has_illegal_inst_ c: "plat_mtval_has_illegal_inst_bits", lem: "plat_mtval_has_illegal_inst_bits"} : unit -> bool +/* whether compressed hint instructions are executed as their 32-bit nop encoding */ +val plat_c_hints_expand = {ocaml: "Platform.c_hints_expand", + interpreter: "Platform.c_hints_expand", + c: "plat_c_hints_expand", + lem: "plat_c_hints_expand"} : unit -> bool + /* ROM holding reset vector and device-tree DTB */ val plat_rom_base = {ocaml: "Platform.rom_base", interpreter: "Platform.rom_base", c: "plat_rom_base", lem: "plat_rom_base"} : unit -> xlenbits val plat_rom_size = {ocaml: "Platform.rom_size", interpreter: "Platform.rom_size", c: "plat_rom_size", lem: "plat_rom_size"} : unit -> xlenbits diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index ccf487589..552882a18 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -10,6 +10,7 @@ let config_enable_writable_misa = ref true let config_enable_dirty_update = ref false let config_enable_misaligned_access = ref false let config_mtval_has_illegal_inst_bits = ref false +let config_c_hints_expand = ref false let config_enable_pmp = ref false let platform_arch = ref P.RV64 @@ -81,6 +82,7 @@ let enable_fdext () = false let enable_dirty_update () = !config_enable_dirty_update let enable_misaligned_access () = !config_enable_misaligned_access let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits +let c_hints_expand () = !config_c_hints_expand let enable_pmp () = !config_enable_pmp let enable_zfinx () = false diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml index 6e612ad26..8639bfd88 100644 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ b/ocaml_emulator/riscv_ocaml_sim.ml @@ -50,6 +50,9 @@ let options = Arg.align ([("-dump-dts", ("-mtval-has-illegal-inst-bits", Arg.Set P.config_mtval_has_illegal_inst_bits, " mtval stores instruction bits on an illegal instruction exception"); + ("-c-hints-expand", + Arg.Set P.config_c_hints_expand, + " compressed hint instructions expand to full instructions"); ("-disable-rvc", Arg.Clear P.config_enable_rvc, " disable the RVC extension on boot");