Skip to content

Commit

Permalink
Misaligned access draft
Browse files Browse the repository at this point in the history 
This is incomplete and does not quite compile (due to dependent changes to `ext_data_get_addr()`). Just making a PR to discuss it.
  • Loading branch information
@Timmmm
Timmmm committed Apr 22, 2024
1 parent 16077e1 commit 614f963
Show file tree
Hide file tree
Showing 7 changed files with 760 additions and 565 deletions.
1 change: 1 addition & 0 deletions Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,7 @@ SAIL_VM_SRCS += riscv_vmem_common.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_translate.sail
SAIL_VM_SRCS += riscv_vmem.sail

# Non-instruction sources
Expand Down
1 change: 1 addition & 0 deletions model/prelude.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_addr_checks.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ type ext_data_addr_error = unit

/* Default data addr is just base register + immediate offset (may be zero).
Extensions might override and add additional checks. */
function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : word_width)
function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : range(0, max_mem_access))
-> Ext_DataAddr_Check(ext_data_addr_error) =
let addr = X(base) + offset in
Ext_DataAddr_OK(addr)
Expand Down
113 changes: 50 additions & 63 deletions model/riscv_insts_base.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -300,52 +300,48 @@ union clause ast = LOAD : (bits(12), regidx, regidx, bool, word_width, bool, boo
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))

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 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)

val process_load : forall 'n, 0 < 'n <= xlen_bytes. (regidx, result(bits(8 * 'n), VMemException), bool) -> Retired
function process_load(rd, value, is_unsigned) =
match value {
Ok(result) => { X(rd) = extend_value(is_unsigned, result); RETIRE_SUCCESS },
Err(vaddr, e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
}

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 is_aligned(vaddr : xlenbits, width : word_width) -> bool =
match width {
BYTE => true,
HALF => vaddr[0..0] == 0b0,
WORD => vaddr[1..0] == 0b00,
DOUBLE => vaddr[2..0] == 0b000
}

// Return true if the address is misaligned and we don't support misaligned access.
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
}
not(plat_enable_misaligned_access()) & not(is_aligned(vaddr, width))

function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
let offset : xlenbits = sign_extend(imm);
let width_bytes = size_bytes(width);

// This is checked during decoding.
assert(width_bytes <= sizeof(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) {
match ext_data_get_addr(rs1, offset, Read(Data), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
Ext_DataAddr_OK(vaddr) => {
match check_and_handle_load_vaddr_for_triggers(vaddr, get_arch_pc()) {
Some(ret) => return ret,
_ => ()
};
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")
}
}
else process_load(rd, vmem_read(Read(Data), vaddr, width_bytes, aq, rl, false), is_unsigned)
}
}
}

Expand Down Expand Up @@ -380,43 +376,34 @@ mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false)
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 <= sizeof(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) {
match ext_data_get_addr(rs1, offset, Write(Data), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
Ext_DataAddr_OK(vaddr) => {
match check_and_handle_store_vaddr_for_triggers(vaddr, get_arch_pc()) {
Some(ret) => return ret,
None() => ()
};
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 }
}
}
else match vmem_write_translate(vaddr, width_bytes, Write(Data), aq, rl, false) {
Err(vaddr, e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
Ok(state) => {
let rs2_val = X(rs2);
match vmem_write_value(state, rs2_val[width_bytes * 8 - 1 .. 0]) {
Ok(true) => RETIRE_SUCCESS,
Ok(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
Err(vaddr, e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
}
}
}
}
}
}

Expand Down
108 changes: 30 additions & 78 deletions model/riscv_insts_fext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -282,60 +282,29 @@ mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE) if haveDExt()

/* Execution semantics ================================ */

val process_fload64 : (regidx, xlenbits, MemoryOpResult(bits(64)))
-> Retired
function process_fload64(rd, addr, value) =
if sizeof(flen) == 64
then match value {
MemValue(result) => { F(rd) = result; RETIRE_SUCCESS },
MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }
}
else {
/* should not get here */
RETIRE_FAIL
}

val process_fload32 : (regidx, xlenbits, MemoryOpResult(bits(32)))
-> Retired
function process_fload32(rd, addr, value) =
match value {
MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS },
MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }
}
function clause execute(LOAD_FP(imm, rs1, rd, width)) = {
let width_bytes = word_width_bytes(width);

val process_fload16 : (regidx, xlenbits, MemoryOpResult(bits(16)))
-> Retired
function process_fload16(rd, addr, value) =
match value {
MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS },
MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }
}
// This is checked during decoding.
assert(width_bytes <= sizeof(xlen_bytes));

function clause execute(LOAD_FP(imm, rs1, rd, width)) = {
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) {
match ext_data_get_addr(rs1, offset, Read(Data), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
Ext_DataAddr_OK(vaddr) => {
match check_and_handle_load_vaddr_for_triggers(vaddr, get_arch_pc()) {
Some(ret) => return ret,
None() => ()
};
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(addr, _) => {
let (aq, rl, res) = (false, false, false);
match (width) {
BYTE => { handle_illegal(); RETIRE_FAIL },
HALF =>
process_fload16(rd, vaddr, mem_read(Read(Data), addr, 2, aq, rl, res)),
WORD =>
process_fload32(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, res)),
DOUBLE if sizeof(flen) >= 64 =>
process_fload64(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, res)),
_ => report_invalid_width(__FILE__, __LINE__, width, "floating point load"),
}
}
else match vmem_read(Read(Data), vaddr, width_bytes, false, false, false) {
Ok(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS },
Err(vaddr, e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
}
}
}
}

Expand Down Expand Up @@ -368,49 +337,32 @@ mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE)

/* Execution semantics ================================ */

val process_fstore : (xlenbits, MemoryOpResult(bool)) -> Retired
function process_fstore(vaddr, value) =
match value {
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 }
}

function clause execute (STORE_FP(imm, rs2, rs1, width)) = {
let width_bytes = word_width_bytes(width);

// This is checked during decoding.
assert(width_bytes <= sizeof(xlen_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) {
match ext_data_get_addr(rs1, offset, Write(Data), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
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(addr, _) => {
let eares : MemoryOpResult(unit) = match width {
BYTE => MemValue () /* bogus placeholder for illegal size */,
HALF => mem_write_ea(addr, 2, aq, rl, false),
WORD => mem_write_ea(addr, 4, aq, rl, false),
DOUBLE => mem_write_ea(addr, 8, aq, rl, false)
};
match (eares) {
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
MemValue(_) => {
let rs2_val = F(rs2);
match (width) {
BYTE => { handle_illegal(); RETIRE_FAIL },
HALF => process_fstore (vaddr, mem_write_value(addr, 2, rs2_val[15..0], aq, rl, con)),
WORD => process_fstore (vaddr, mem_write_value(addr, 4, rs2_val[31..0], aq, rl, con)),
DOUBLE if sizeof(flen) >= 64 =>
process_fstore (vaddr, mem_write_value(addr, 8, rs2_val, aq, rl, con)),
_ => report_invalid_width(__FILE__, __LINE__, width, "floating point store"),
};
}
else match vmem_write_translate(vaddr, width_bytes, Write(Data), false, false, false) {
Err(vaddr, e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
Ok(state) => {
let rs2_val = F(rs2);
match vmem_write_value(state, rs2_val[width_bytes * 8 - 1 .. 0]) {
Ok(true) => { RETIRE_SUCCESS },
Ok(false) => { internal_error(__FILE__, __LINE__, "store got false from mem_write_value") },
Err(vaddr, e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
}
}
}
}
}
}

Expand Down
Loading

0 comments on commit 614f963

Please sign in to comment.