Skip to content

Better handling of misaligned accesses (take 2) #861

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Better handling of misaligned accesses (take 2) #861

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
141ea20
Handle address translation for misaligned loads and stores better
pmundkur Apr 14, 2025
677dab9
Update the F/D and vector loads/stores to use the `vmem_utils` helpers.
pmundkur Apr 18, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 5 additions & 3 deletions Makefile.old
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,7 @@ SAIL_DEFAULT_INST += riscv_insts_zicbom.sail
SAIL_DEFAULT_INST += riscv_insts_zicboz.sail
SAIL_DEFAULT_INST += riscv_insts_zvbb.sail
SAIL_DEFAULT_INST += riscv_insts_zvbc.sail
SAIL_DEFAULT_INST += riscv_insts_zvknhab.sail
SAIL_DEFAULT_INST += riscv_insts_zimop.sail
SAIL_DEFAULT_INST += riscv_insts_zcmop.sail

Expand All @@ -91,11 +92,13 @@ SAIL_SYS_SRCS += riscv_zicntr_control.sail
SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdext_control.sail
SAIL_SYS_SRCS += riscv_sys_control.sail # general exception handling
SAIL_SYS_SRCS += riscv_smcntrpmf.sail
SAIL_SYS_SRCS += riscv_inst_retire.sail

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 riscv_errors.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_addrtype.sail prelude_mem_metadata.sail prelude_mem.sail arithmetic.sail
Expand All @@ -112,8 +115,7 @@ SAIL_ARCH_SRCS += riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv
SAIL_ARCH_SRCS += riscv_sstc.sail
SAIL_ARCH_SRCS += riscv_mem.sail $(SAIL_VM_SRCS)
SAIL_ARCH_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_extensions.sail riscv_types_common.sail riscv_types_ext.sail riscv_types.sail riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail $(SAIL_VM_SRCS) riscv_types_kext.sail riscv_inst_retire.sail
SAIL_ARCH_SRCS += riscv_types_kext.sail # Shared/common code for the cryptography extension.
SAIL_ARCH_SRCS += riscv_inst_retire.sail
SAIL_ARCH_SRCS += riscv_types_kext.sail riscv_zvk_utils.sail # Shared/common code for the cryptography extension.

SAIL_STEP_SRCS = riscv_step_common.sail riscv_step_ext.sail riscv_decode_ext.sail riscv_fetch.sail riscv_step.sail
RVFI_STEP_SRCS = riscv_step_common.sail riscv_step_rvfi.sail riscv_decode_ext.sail riscv_fetch_rvfi.sail riscv_step.sail
Expand Down Expand Up @@ -202,7 +204,7 @@ RISCV_EXTRAS_LEM = $(addprefix handwritten_support/,$(RISCV_EXTRAS_LEM_FILES))
.PHONY:

all: c_emulator/riscv_sim_$(ARCH)
.PHONY: all
.PHONY: all check_properties

# the following ensures empty sail-generated .c files don't hang around and
# break future builds if sail exits badly
Expand Down
5 changes: 4 additions & 1 deletion config/default.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,10 @@
"count": 16
},
"misaligned": {
"supported": true
"supported": true,
"to_byte": false,
"order_decreasing": false,
"allowed_within": 0
},
"translation": {
"dirty_update": false
Expand Down
12 changes: 9 additions & 3 deletions doc/ReadingGuide.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,9 +80,15 @@ such as the platform memory map.
appropriate access fault. This file also contains definitions that
are used in the weak memory concurrency model.

- The `riscv_vmem_*.sail` files describe the S-mode address
translation. See the [Virtual Memory Notes](./notes_Virtual_Memory.adoc)
for details.
- The `riscv_vmem_{types,pte,ptw,tlb}.sail` and `riscv_vmem.sail`
files describe the S-mode address translation.
See the [Virtual Memory Notes](./notes_Virtual_Memory.adoc) for
details.

- The `riscv_vmem_utils.sail` file provides a higher level interface
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Might be worth adding a more detailed description to the notes_Virtual_Memory.adoc file.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure what can go in there in addition to what's already described in comments in riscv_vmem_utils.sail.

to virtual memory for load/store style instructions that handles
address translation and accesses to misaligned addresses taking
platform configuration options into account.

- The `riscv_addr_checks_common.sail` and `riscv_addr_checks.sail`
contain extension hooks to support the checking and transformation
Expand Down
3 changes: 2 additions & 1 deletion model/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -134,6 +134,7 @@ foreach (xlen IN ITEMS 32 64)
"riscv_vmem_ptw.sail"
"riscv_vmem_tlb.sail"
"riscv_vmem.sail"
"riscv_vmem_utils.sail"
)

set(prelude
Expand Down Expand Up @@ -178,11 +179,11 @@ foreach (xlen IN ITEMS 32 64)
${sail_sys_srcs}
"riscv_platform.sail"
"riscv_mem.sail"
"riscv_inst_retire.sail"
${sail_vm_srcs}
# Shared/common code for the cryptography extension.
"riscv_types_kext.sail"
"riscv_zvk_utils.sail"
"riscv_inst_retire.sail"
)

if (variant STREQUAL "rvfi")
Expand Down
89 changes: 25 additions & 64 deletions model/riscv_insts_aext.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,26 +78,12 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
// This is checked during decoding.
assert(width_bytes <= xlen_bytes);

/* Get the address, X(rs1) (no offset).
* Extensions might perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), Read(Data), width_bytes) {
Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
Ext_DataAddr_OK(vaddr) => {
/* "LR faults like a normal load, even though it's in the AMO major opcode space."
* - Andrew Waterman, isa-dev, 10 Jul 2018.
*/
if not(is_aligned(bits_of(vaddr), width))
then RETIRE_FAIL(Memory_Exception(vaddr, E_Load_Addr_Align()))
else match translateAddr(vaddr, Read(Data)) {
TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
TR_Address(addr, _) =>
match mem_read(Read(Data), addr, width_bytes, aq, aq & rl, true) {
Ok(result) => { load_reservation(bits_of(addr)); X(rd) = sign_extend(result); RETIRE_SUCCESS },
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
},
}
}
match vmem_read(rs1, zeros(), width_bytes, aq, aq & rl, true) {
Ok(data) => {
X(rd) = sign_extend(data);
RETIRE_SUCCESS
},
Err(e) => RETIRE_FAIL(e),
}
}

Expand All @@ -118,50 +104,25 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
// This is checked during decoding.
assert(width_bytes <= xlen_bytes);

if speculate_conditional () == false then {
/* should only happen in rmem
* rmem: allow SC to fail very early
if speculate_conditional() == false then {
/* should only happen in RMEM
* RMEM: allow SC to fail very early
*/
X(rd) = zero_extend(0b1); RETIRE_SUCCESS
} else {
/* normal non-rmem case
* rmem: SC is allowed to succeed (but might fail later)
*/
/* Get the address, X(rs1) (no offset).
* Extensions might perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) {
Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
Ext_DataAddr_OK(vaddr) => {
if not(is_aligned(bits_of(vaddr), width))
then RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align()))
else {
match translateAddr(vaddr, Write(Data)) { /* Write and ReadWrite are equivalent here:
* both result in a SAMO exception */
TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
TR_Address(addr, _) => {
// Check reservation with physical address.
if not(match_reservation(bits_of(addr))) then {
/* cannot happen in rmem */
X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS
} else {
match mem_write_ea(addr, width_bytes, aq & rl, rl, true) {
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
Ok(_) => {
let rs2_val = X(rs2);
match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq & rl, rl, true) {
Ok(true) => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS },
Ok(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS },
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
}
}
}
}
}
}
}
}
}
X(rd) = zero_extend(0b1);
return RETIRE_SUCCESS
};

/* normal non-rmem case
* RMEM: SC is allowed to succeed (but might fail later)
*/
let data = X(rs2)[width_bytes * 8 - 1 .. 0];
match vmem_write(rs1, zeros(), width_bytes, data, aq & rl, rl, true) {
Ok(b) => {
X(rd) = zero_extend(if b then 0b0 else 0b1);
cancel_reservation();
RETIRE_SUCCESS
},
Err(e) => return RETIRE_FAIL(e),
}
}

Expand Down Expand Up @@ -203,7 +164,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width_bytes) {
Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
Ext_DataAddr_OK(vaddr) => {
if not(is_aligned(bits_of(vaddr), width))
if not(is_aligned_addr(bits_of(vaddr), width))
then RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align()))
else match translateAddr(vaddr, ReadWrite(Data, Data)) {
TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
Expand Down
82 changes: 21 additions & 61 deletions model/riscv_insts_base.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -276,24 +276,15 @@ 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)
<-> imm @ encdec_reg(rs1) @ bool_bits(is_unsigned) @ size_enc(size) @ encdec_reg(rd) @ 0b0000011
when (size_bytes(size) < xlen_bytes) | (not(is_unsigned) & size_bytes(size) <= xlen_bytes)
function valid_load_encdec(width : word_width, is_unsigned : bool) -> bool =
(size_bytes(width) < xlen_bytes) | (not(is_unsigned) & size_bytes(width) <= xlen_bytes)

val extend_value : forall 'n, 0 < 'n <= xlen. (bool, bits('n)) -> xlenbits
function extend_value(is_unsigned, value) = if is_unsigned then zero_extend(value) else sign_extend(value)

function is_aligned(vaddr : xlenbits, width : word_width) -> bool =
match width {
BYTE => true,
HALF => vaddr[0..0] == zeros(),
WORD => vaddr[1..0] == zeros(),
DOUBLE => vaddr[2..0] == zeros(),
}

// Return true if the address is misaligned and we don't support misaligned access.
function check_misaligned(vaddr : virtaddr, width : word_width) -> bool =
not(plat_enable_misaligned_access()) & not(is_aligned(bits_of(vaddr), width))
mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, width, false, false)
<-> imm @ encdec_reg(rs1) @ bool_bits(is_unsigned) @ size_enc(width) @ encdec_reg(rd) @ 0b0000011
when valid_load_encdec(width, is_unsigned)

function clause execute (LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
let offset : xlenbits = sign_extend(imm);
Expand All @@ -302,22 +293,12 @@ function clause execute (LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
// This is checked during decoding.
assert(width_bytes <= xlen_bytes);

/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Read(Data), width_bytes) {
Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
Ext_DataAddr_OK(vaddr) => {
if check_misaligned(vaddr, width)
then RETIRE_FAIL(Memory_Exception(vaddr, E_Load_Addr_Align()))
else match translateAddr(vaddr, Read(Data)) {
TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
TR_Address(paddr, _) =>
match mem_read(Read(Data), paddr, width_bytes, aq, rl, false) {
Ok(result) => { X(rd) = extend_value(is_unsigned, result); RETIRE_SUCCESS },
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
},
}
match vmem_read(rs1, offset, width_bytes, aq, rl, false) {
Ok(data) => {
X(rd) = extend_value(is_unsigned, data);
RETIRE_SUCCESS
},
Err(e) => RETIRE_FAIL(e),
}
}

Expand All @@ -339,53 +320,32 @@ 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_signed_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_signed_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)
<-> imm7 : bits(7) @ encdec_reg(rs2) @ encdec_reg(rs1) @ 0b0 @ size_enc(size) @ imm5 : bits(5) @ 0b0100011
when size_bytes(size) <= xlen_bytes
mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, width, false, false)
<-> imm7 : bits(7) @ encdec_reg(rs2) @ encdec_reg(rs1) @ 0b0 @ size_enc(width) @ imm5 : bits(5) @ 0b0100011
when size_bytes(width) <= 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);
let width_bytes = size_bytes(width);

// This is checked during decoding.
assert(width_bytes <= xlen_bytes);

/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Write(Data), width_bytes) {
Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
then RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align()))
else match translateAddr(vaddr, Write(Data)) {
TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
TR_Address(paddr, _) => {
match mem_write_ea(paddr, width_bytes, aq, rl, false) {
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
Ok(_) => {
let rs2_val = X(rs2);
match mem_write_value(paddr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq, rl, false) {
Ok(true) => RETIRE_SUCCESS,
Ok(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e))
}
}
}
}
}
let data = X(rs2)[width_bytes * 8 - 1 .. 0];
match vmem_write(rs1, offset, width_bytes, data, aq, rl, false) {
Ok(_) => RETIRE_SUCCESS,
Err(e) => RETIRE_FAIL(e),
}
}

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_signed_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_signed_12(imm) ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"

/* ****************************************************************** */
union clause ast = ADDIW : (bits(12), regidx, regidx)
Expand Down
51 changes: 8 additions & 43 deletions model/riscv_insts_fext.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -295,24 +295,9 @@ function clause execute(LOAD_FP(imm, rs1, rd, width)) = {
assert(width_bytes <= flen_bytes);

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_bytes) {
Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
Ext_DataAddr_OK(vaddr) => {
if check_misaligned(vaddr, width)
then RETIRE_FAIL(Memory_Exception(vaddr, E_Load_Addr_Align()))
else match translateAddr(vaddr, Read(Data)) {
TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
TR_Address(addr, _) => {
let (aq, rl, res) = (false, false, false);
match mem_read(Read(Data), addr, width_bytes, aq, rl, res) {
Ok(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS },
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
}
},
}
}
match vmem_read(rs1, offset, width_bytes, false, false, false) {
Ok(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS },
Err(e) => { RETIRE_FAIL(e) }
}
}

Expand Down Expand Up @@ -355,31 +340,11 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = {
assert(width_bytes <= flen_bytes);

let offset : xlenbits = sign_extend(imm);
let (aq, rl, con) = (false, false, false);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Write(Data), width_bytes) {
Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
Ext_DataAddr_OK(vaddr) => {
if check_misaligned(vaddr, width)
then RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align()))
else match translateAddr(vaddr, Write(Data)) {
TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
TR_Address(addr, _) => {
match mem_write_ea(addr, width_bytes, aq, rl, false) {
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
Ok(_) => {
let rs2_val = F(rs2);
match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq, rl, con) {
Ok(true) => RETIRE_SUCCESS,
Ok(false) => { internal_error(__FILE__, __LINE__, "store got false from mem_write_value") },
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e))
}
},
}
}
}
}
let data = F(rs2)[width_bytes * 8 - 1 .. 0];
match vmem_write(rs1, offset, width_bytes, data, false, false, false) {
Ok(true) => RETIRE_SUCCESS,
Ok(false) => internal_error(__FILE__, __LINE__, "store got false from vmem_write"),
Err(e) => RETIRE_FAIL(e),
}
}

Expand Down
Loading
Loading