Handle address translation for misaligned loads and stores better

Refactor the LOAD and STORE instruction so they split misaligned
accesses into multiple sub-accesses and perform address translation
separately. This means we should handle the case where a misaligned
access straddles a page boundary in a sensible way, even if we don't
yet cover the full range of possibilities allowed for any RISC-V
implementation.

In addition tidy up the implementation in a few ways:

- Very long lines on the LOAD encdec were fixed by adding a helper

- Add some linebreaks in the code so it reads as less claustrophobic

- Ensure we use the same names for arguments in encdec/execute/assembly.
  Previously we used 'size' and 'width'. I opted for 'width' consistently.

Makefile

@@ -90,6 +90,7 @@ SAIL_VM_SRCS += riscv_vmem_pte.sail
 SAIL_VM_SRCS += riscv_vmem_ptw.sail
 SAIL_VM_SRCS += riscv_vmem_tlb.sail
 SAIL_VM_SRCS += riscv_vmem.sail
+SAIL_VM_SRCS += riscv_vmem_utils.sail
 
 # Non-instruction sources
 PRELUDE = prelude.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail

c_emulator/riscv_platform.c

@@ -57,6 +57,16 @@ bool sys_enable_vext(unit u)
  return rv_enable_vext;
 }
 
+bool sys_misaligned_order_decreasing(unit u)
+{
+ return rv_misaligned_order_decreasing;
+}
+
+bool sys_misaligned_to_byte(unit u)
+{
+ return rv_misaligned_to_byte;
+}
+
 uint64_t sys_pmp_count(unit u)
 {
  return rv_pmp_count;
@@ -108,7 +118,7 @@ mach_bits plat_rom_size(unit u)
 }
 
 // Provides entropy for the scalar cryptography extension.
-mach_bits plat_get_16_random_bits()
+mach_bits plat_get_16_random_bits(unit u)
 {
  return rv_16_random_bits();
 }

c_emulator/riscv_platform.h

@@ -11,6 +11,9 @@ bool sys_enable_writable_misa(unit);
 bool sys_enable_writable_fiom(unit);
 bool sys_enable_vext(unit);
 
+bool sys_misaligned_order_decreasing(unit);
+bool sys_misaligned_to_byte(unit);
+
 uint64_t sys_pmp_count(unit);
 uint64_t sys_pmp_grain(unit);
 
@@ -26,7 +29,7 @@ mach_bits plat_rom_base(unit);
 mach_bits plat_rom_size(unit);
 
 // Provides entropy for the scalar cryptography extension.
-mach_bits plat_get_16_random_bits();
+mach_bits plat_get_16_random_bits(unit);
 
 mach_bits plat_clint_base(unit);
 mach_bits plat_clint_size(unit);

c_emulator/riscv_platform_impl.c

@@ -6,6 +6,10 @@
 uint64_t rv_pmp_count = 0;
 uint64_t rv_pmp_grain = 0;
 
+/* Defaults for misaligned access behavior in the generated simulator */
+bool rv_misaligned_order_decreasing = false;
+bool rv_misaligned_to_byte = false;
+
 bool rv_enable_svinval = false;
 bool rv_enable_zcb = false;
 bool rv_enable_zfinx = false;

c_emulator/riscv_platform_impl.h

@@ -11,6 +11,9 @@
 extern uint64_t rv_pmp_count;
 extern uint64_t rv_pmp_grain;
 
+extern bool rv_misaligned_order_decreasing;
+extern bool rv_misaligned_to_byte;
+
 extern bool rv_enable_svinval;
 extern bool rv_enable_zcb;
 extern bool rv_enable_zfinx;

c_emulator/riscv_sim.c

@@ -54,6 +54,8 @@ const char *RV32ISA = "RV32IMAC";
 #define OPT_PMP_COUNT 1002
 #define OPT_PMP_GRAIN 1003
 #define OPT_ENABLE_SVINVAL 1004
+#define OPT_MISALIGNED_ORDER_DEC 1005
+#define OPT_MISALIGNED_TO_BYTE 1006
 #define OPT_ENABLE_ZCB 10014
 
 static bool do_dump_dts = false;
@@ -125,6 +127,8 @@ static struct option options[] = {
  {"enable-misaligned", no_argument, 0, 'm' },
  {"pmp-count", required_argument, 0, OPT_PMP_COUNT },
  {"pmp-grain", required_argument, 0, OPT_PMP_GRAIN },
+ {"misaligned-order-decreasing", no_argument, 0, OPT_MISALIGNED_ORDER_DEC},
+ {"misaligned-to-byte", no_argument, 0, OPT_MISALIGNED_TO_BYTE },
  {"enable-next", no_argument, 0, 'N' },
  {"ram-size", required_argument, 0, 'z' },
  {"disable-compressed", no_argument, 0, 'C' },
@@ -308,6 +312,18 @@ static int process_args(int argc, char **argv)
  }
  rv_pmp_grain = pmp_grain;
  break;
+ case OPT_MISALIGNED_ORDER_DEC:
+ fprintf(stderr,
+ "misaligned access virtual addresses will be translated in "
+ "decreasing order.\n");
+ rv_misaligned_order_decreasing = true;
+ break;
+ case OPT_MISALIGNED_TO_BYTE:
+ fprintf(stderr,
+ "misaligned accesses will be split into individual "
+ "byte operations.\n");
+ rv_misaligned_to_byte = true;
+ break;
  case 'C':
  fprintf(stderr, "disabling RVC compressed instructions.\n");
  rv_enable_rvc = false;

model/prelude.sail

@@ -10,6 +10,7 @@ default Order dec
 
 $include <smt.sail>
 $include <option.sail>
+$include <result.sail>
 $include <arith.sail>
 $include <string.sail>
 $include "mapping.sail"

model/riscv_insts_aext.sail

@@ -40,6 +40,12 @@ function amo_width_valid(size : word_width) -> bool = {
  }
 }
 
+val extend_value : forall 'n, 0 < 'n <= xlen_bytes. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits)
+function extend_value(is_unsigned, value) = match (value) {
+ MemValue(v) => MemValue(if is_unsigned then zero_extend(v) else sign_extend(v) : xlenbits),
+ MemException(e) => MemException(e)
+}
+
 /* ****************************************************************** */
 union clause ast = LOADRES : (bool, bool, regidx, word_width, regidx)
 

model/riscv_insts_base.sail

@@ -297,55 +297,43 @@ union clause ast = LOAD : (bits(12), regidx, regidx, bool, word_width, bool, boo
 
 /* unsigned loads are only present for widths strictly less than xlen,
  signed loads also present for widths equal to xlen */
-mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (size_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & size_bytes(size) <= sizeof(xlen_bytes))
- <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_enc(size) @ rd @ 0b0000011 if (size_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & size_bytes(size) <= sizeof(xlen_bytes))
+function valid_load_encdec(width : word_width, is_unsigned : bool) -> bool =
+ (size_bytes(width) < sizeof(xlen_bytes)) | (not(is_unsigned) & size_bytes(width) <= sizeof(xlen_bytes))
 
-val extend_value : forall 'n, 0 < 'n <= xlen_bytes. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits)
-function extend_value(is_unsigned, value) = match (value) {
- MemValue(v) => MemValue(if is_unsigned then zero_extend(v) else sign_extend(v) : xlenbits),
- MemException(e) => MemException(e)
-}
-
-val process_load : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired
-function process_load(rd, vaddr, value, is_unsigned) =
- match extend_value(is_unsigned, value) {
- MemValue(result) => { X(rd) = result; RETIRE_SUCCESS },
- MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
- }
-
-function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
- if plat_enable_misaligned_access() then false
- else match width {
- BYTE => false,
- HALF => vaddr[0] == bitone,
- WORD => vaddr[0] == bitone | vaddr[1] == bitone,
- DOUBLE => vaddr[0] == bitone | vaddr[1] == bitone | vaddr[2] == bitone
- }
+mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, width, false, false) if valid_load_encdec(width, is_unsigned)
+ <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_enc(width) @ rd @ 0b0000011 if valid_load_encdec(width, is_unsigned)
 
 function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
  let offset : xlenbits = sign_extend(imm);
  /* Get the address, X(rs1) + offset.
  Some extensions perform additional checks on address validity. */
  match ext_data_get_addr(rs1, offset, Read(Data), width) {
- Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
- Ext_DataAddr_OK(vaddr) =>
- if check_misaligned(vaddr, width)
- then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL }
- else match translateAddr(vaddr, Read(Data)) {
- TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
- TR_Address(paddr, _) =>
- match (width) {
- BYTE =>
- process_load(rd, vaddr, mem_read(Read(Data), paddr, 1, aq, rl, false), is_unsigned),
- HALF =>
- process_load(rd, vaddr, mem_read(Read(Data), paddr, 2, aq, rl, false), is_unsigned),
- WORD =>
- process_load(rd, vaddr, mem_read(Read(Data), paddr, 4, aq, rl, false), is_unsigned),
- DOUBLE if sizeof(xlen) >= 64 =>
- process_load(rd, vaddr, mem_read(Read(Data), paddr, 8, aq, rl, false), is_unsigned),
- _ => report_invalid_width(__FILE__, __LINE__, width, "load")
- }
+ Ext_DataAddr_Error(e) => {
+ ext_handle_data_check_error(e);
+ RETIRE_FAIL
+ },
+
+ Ext_DataAddr_OK(vaddr) => {
+ if check_misaligned(vaddr, width) then {
+ handle_mem_exception(vaddr, E_Load_Addr_Align());
+ return RETIRE_FAIL
+ };
+
+ let bytes = size_bytes(width);
+ if bytes > sizeof(xlen_bytes) then {
+ report_invalid_width(__FILE__, __LINE__, width, "load")
+ } else match vmem_read(vaddr, bytes, aq, rl, false) {
+ Err(vaddr, e) => {
+ handle_mem_exception(vaddr, e);
+ RETIRE_FAIL
+ },
+
+ Ok(data) => {
+ X(rd) = if is_unsigned then zero_extend(data) else sign_extend(data);
+ RETIRE_SUCCESS
+ }
  }
+ }
  }
 }
 
@@ -367,61 +355,47 @@ mapping maybe_u = {
  false <-> ""
 }
 
-mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, size, aq, rl)
- <-> "l" ^ size_mnemonic(size) ^ maybe_u(is_unsigned) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_12(imm) ^ "(" ^ reg_name(rs1) ^ ")"
+mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)
+ <-> "l" ^ size_mnemonic(width) ^ maybe_u(is_unsigned) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_12(imm) ^ "(" ^ reg_name(rs1) ^ ")"
 
 /* ****************************************************************** */
 union clause ast = STORE : (bits(12), regidx, regidx, word_width, bool, bool)
 
-mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false)  if size_bytes(size) <= sizeof(xlen_bytes)
- <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ imm5 : bits(5) @ 0b0100011 if size_bytes(size) <= sizeof(xlen_bytes)
+mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, width, false, false) if size_bytes(width) <= sizeof(xlen_bytes)
+ <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_enc(width) @ imm5 : bits(5) @ 0b0100011 if size_bytes(width) <= sizeof(xlen_bytes)
 
-/* NOTE: Currently, we only EA if address translation is successful.
- This may need revisiting. */
 function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
  let offset : xlenbits = sign_extend(imm);
  /* Get the address, X(rs1) + offset.
  Some extensions perform additional checks on address validity. */
  match ext_data_get_addr(rs1, offset, Write(Data), width) {
- Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
- Ext_DataAddr_OK(vaddr) =>
- if check_misaligned(vaddr, width)
- then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
- else match translateAddr(vaddr, Write(Data)) {
- TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
- TR_Address(paddr, _) => {
- let eares : MemoryOpResult(unit) = match width {
- BYTE => mem_write_ea(paddr, 1, aq, rl, false),
- HALF => mem_write_ea(paddr, 2, aq, rl, false),
- WORD => mem_write_ea(paddr, 4, aq, rl, false),
- DOUBLE => mem_write_ea(paddr, 8, aq, rl, false)
- };
- match (eares) {
- MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
- MemValue(_) => {
- let rs2_val = X(rs2);
- let res : MemoryOpResult(bool) = match (width) {
- BYTE => mem_write_value(paddr, 1, rs2_val[7..0], aq, rl, false),
- HALF => mem_write_value(paddr, 2, rs2_val[15..0], aq, rl, false),
- WORD => mem_write_value(paddr, 4, rs2_val[31..0], aq, rl, false),
- DOUBLE if sizeof(xlen) >= 64
- => mem_write_value(paddr, 8, rs2_val, aq, rl, false),
- _ => report_invalid_width(__FILE__, __LINE__, width, "store"),
- };
- match (res) {
- MemValue(true) => RETIRE_SUCCESS,
- MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
- MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
- }
- }
- }
+ Ext_DataAddr_Error(e) => {
+ ext_handle_data_check_error(e);
+ RETIRE_FAIL
+ },
+
+ Ext_DataAddr_OK(vaddr) => {
+ if check_misaligned(vaddr, width) then {
+ handle_mem_exception(vaddr, E_SAMO_Addr_Align());
+ return RETIRE_FAIL
+ };
+
+ let bytes = size_bytes(width);
+ if bytes > sizeof(xlen_bytes) then {
+ report_invalid_width(__FILE__, __LINE__, width, "store")
+ } else match vmem_write_from_register(vaddr, bytes, unsigned(rs2), aq, rl, false) {
+ Ok() => RETIRE_SUCCESS,
+ Err(vaddr, e) => {
+ handle_mem_exception(vaddr, e);
+ return RETIRE_FAIL
  }
  }
+ }
  }
 }
 
-mapping clause assembly = STORE(imm, rs2, rs1, size, aq, rl)
- <-> "s" ^ size_mnemonic(size) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_12(imm) ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"
+mapping clause assembly = STORE(imm, rs2, rs1, width, aq, rl)
+ <-> "s" ^ size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_12(imm) ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"
 
 /* ****************************************************************** */
 union clause ast = ADDIW : (bits(12), regidx, regidx)

model/riscv_mem.sail

@@ -38,6 +38,14 @@
 function is_aligned_addr forall 'n. (addr : xlenbits, width : int('n)) -> bool =
  unsigned(addr) % width == 0
 
+function check_misaligned(vaddr : xlenbits, width : word_width) -> bool = {
+ if plat_enable_misaligned_access() then {
+ false
+ } else {
+ not(is_aligned_addr(vaddr, size_bytes(width)))
+ }
+}
+
 function read_kind_of_flags (aq : bool, rl : bool, res : bool) -> option(read_kind) =
  match (aq, rl, res) {
  (false, false, false) => Some(Read_plain),