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.
riscv · Jul 19, 2023 · 1bd4fa6 · 1bd4fa6
1 parent ae905fb
commit 1bd4fa6
Show file tree

Hide file tree

Showing 9 changed files with 57 additions and 8 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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");