Add a riscv platform parameter to control trapping to M-mode on misaligned access, and a cli option to control it.

5 files changed, 34 insertions, 4 deletions

diff --git a/riscv/platform.ml b/riscv/platform.ml
index 1b3ecf5d..0366e601 100644
--- a/riscv/platform.ml
+++ b/riscv/platform.ml
@@ -53,7 +53,9 @@ module P = Platform_impl;;
 module Elf = Elf_loader;;
 
 (* Platform configuration *)
+
 let config_enable_dirty_update = ref false
+let config_enable_misaligned_access = ref false
 
 (* Mapping to Sail externs *)
 
@@ -79,6 +81,7 @@ let make_rom start_pc =
     rom )
 
 let enable_dirty_update () = !config_enable_dirty_update
+let enable_misaligned_access () = !config_enable_misaligned_access
 
 let rom_base () = bits_of_int64 P.rom_base
 let rom_size () = bits_of_int   !rom_size_ref
diff --git a/riscv/platform_main.ml b/riscv/platform_main.ml
index a087e90c..8dd47547 100644
--- a/riscv/platform_main.ml
+++ b/riscv/platform_main.ml
@@ -69,7 +69,10 @@ let options = Arg.align ([("-dump-dts",
                            " dump the *binary* platform device-tree blob to stdout");
                           ("-enable-dirty-update",
                            Arg.Set P.config_enable_dirty_update,
-                           " enable dirty-bit update during page-table walks")
+                           " enable dirty-bit update during page-table walks");
+                          ("-enable-misaligned-access",
+                           Arg.Set P.config_enable_misaligned_access,
+                           " enable misaligned accesses without M-mode traps")
                          ])
 
 let usage_msg = "RISC-V platform options:"
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index aad6c731..37fefaf1 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -333,9 +333,20 @@ function process_load(rd, addr, value, is_unsigned) =
     MemException(e)  => { handle_mem_exception(addr, e); false }
   }
 
+function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
+  if plat_enable_misaligned_access() then false
+  else match width {
+         BYTE   => false,
+         HALF   => vaddr[0] == true,
+         WORD   => vaddr[0] == true | vaddr[1] == true,
+         DOUBLE => vaddr[0] == true | vaddr[1] == true | vaddr[2] == true
+       }
+
 function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) =
     let vaddr : xlenbits = X(rs1) + EXTS(imm) in
-    match translateAddr(vaddr, Read, Data) {
+    if check_misaligned(vaddr, width)
+    then { handle_mem_exception(vaddr, E_Load_Addr_Align); false }
+    else match translateAddr(vaddr, Read, Data) {
       TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
       TR_Address(addr) =>
         match width {
@@ -393,7 +404,9 @@ mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false) <-> imm
    This may need revisiting. */
 function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) =
     let vaddr : xlenbits = X(rs1) + EXTS(imm) in
-    match translateAddr(vaddr, Write, Data) {
+    if check_misaligned(vaddr, width)
+    then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); false }
+    else match translateAddr(vaddr, Write, Data) {
       TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
       TR_Address(addr) =>
         let eares : MemoryOpResult(unit) = match width {
diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem
index 60d9852a..7c346688 100644
--- a/riscv/riscv_extras.lem
+++ b/riscv/riscv_extras.lem
@@ -72,6 +72,10 @@ val plat_enable_dirty_update : unit -> bool
 let plat_enable_dirty_update () = false
 declare ocaml target_rep function plat_enable_dirty_update = `Platform.enable_dirty_update`
 
+val plat_enable_misaligned_access : unit -> bool
+let plat_enable_misaligned_access () = false
+declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access`
+
 val plat_insns_per_tick : unit -> integer
 let plat_insns_per_tick () = 1
 declare ocaml target_rep function plat_insns_per_tick = `Platform.insns_per_tick`
diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index bfeff01d..bf0e5020 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -11,7 +11,14 @@ val plat_ram_base = {ocaml: "Platform.dram_base", lem: "plat_ram_base"} : unit -
 val plat_ram_size = {ocaml: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits
 
 /* whether the MMU should update dirty bits in PTEs */
-val plat_enable_dirty_update = {ocaml: "Platform.enable_dirty_update", lem: "plat_enable_dirty_update"} : unit -> bool
+val plat_enable_dirty_update = {ocaml: "Platform.enable_dirty_update",
+                                lem: "plat_enable_dirty_update"} : unit -> bool
+
+/* whether the platform supports misaligned accesses without trapping to M-mode. if false,
+ * misaligned loads/stores are trapped to Machine mode.
+ */
+val plat_enable_misaligned_access = {ocaml: "Platform.enable_misaligned_access",
+                                     lem: "plat_enable_misaligned_access"} : unit -> bool
 
 /* ROM holding reset vector and device-tree DTB */
 val plat_rom_base = {ocaml: "Platform.rom_base", lem: "plat_rom_base"} : unit -> xlenbits