Skip to content

Use result type for TR_Result instead of union #875

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 1 commit into
base: master
Choose a base branch
from
Open

Use result type for TR_Result instead of union #875

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
12 changes: 6 additions & 6 deletions model/riscv_fetch.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,9 +22,9 @@ function fetch() -> FetchResult =
let use_pc_bits = bits_of(use_pc);
if (use_pc_bits[0] != bitzero | (use_pc_bits[1] != bitzero & not(currentlyEnabled(Ext_Zca))))
then F_Error(E_Fetch_Addr_Align(), PC)
else match translateAddr(use_pc, InstructionFetch()) {
TR_Failure(e, _) => F_Error(e, PC),
TR_Address(ppclo, _) => {
else match translateAddr(use_pc, Execute()) {
Err(e, _) => F_Error(e, PC),
Ok(ppclo, _) => {
/* split instruction fetch into 16-bit granules to handle RVC, as
* well as to generate precise fault addresses in any fetch
* exceptions.
Expand All @@ -41,9 +41,9 @@ function fetch() -> FetchResult =
Ext_FetchAddr_Error(e) => F_Ext_Error(e),
Ext_FetchAddr_OK(use_pc_hi) => {
match translateAddr(use_pc_hi, InstructionFetch()) {
TR_Failure(e, _) => F_Error(e, PC_hi),
TR_Address(ppchi, _) => {
match mem_read(InstructionFetch(), ppchi, 2, false, false, false) {
Err(e, _) => F_Error(e, PC_hi),
Ok(ppchi, _) => {
match mem_read(Execute(), ppchi, 2, false, false, false) {
Err(e) => F_Error(e, PC_hi),
Ok(ihi) => F_Base(append(ihi, ilo))
}
Expand Down
8 changes: 4 additions & 4 deletions model/riscv_fetch_rvfi.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,8 @@ function fetch() -> FetchResult = {
if (use_pc_bits[0] != bitzero | (use_pc_bits[1] != bitzero & not(currentlyEnabled(Ext_Zca))))
then F_Error(E_Fetch_Addr_Align(), PC)
else match translateAddr(use_pc, InstructionFetch()) {
TR_Failure(e, _) => F_Error(e, PC),
TR_Address(_, _) => {
Err(e, _) => F_Error(e, PC),
Ok(_, _) => {
let i = rvfi_instruction[rvfi_insn];
rvfi_inst_data[rvfi_insn] = zero_extend(i);
if (i[1 .. 0] != 0b11)
Expand All @@ -34,8 +34,8 @@ function fetch() -> FetchResult = {
Ext_FetchAddr_Error(e) => F_Ext_Error(e),
Ext_FetchAddr_OK(use_pc_hi) =>
match translateAddr(use_pc_hi, InstructionFetch()) {
TR_Failure(e, _) => F_Error(e, PC),
TR_Address(_, _) => F_Base(i)
Err(e, _) => F_Error(e, PC),
Ok(_, _) => F_Base(i)
}
}
}
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_zicbom.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ function process_clean_inval(rs1, cbop) = {
Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
Ext_DataAddr_OK(vaddr) => {
let res : option(ExceptionType) = match translateAddr(vaddr, Read(Data)) {
TR_Address(paddr, _) => {
Ok(paddr, _) => {
// "A cache-block management instruction is permitted to access the
// specified cache block whenever a load instruction or store instruction
// is permitted to access the corresponding physical addresses. If
Expand All @@ -105,7 +105,7 @@ function process_clean_inval(rs1, cbop) = {
_ => None(),
}
},
TR_Failure(e, _) => Some(e)
Err(e, _) => Some(e)
};
// "If access to the cache block is not permitted, a cache-block management
// instruction raises a store page fault or store guest-page fault exception
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_zicboz.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,8 +44,8 @@ function clause execute(ZICBOZ(rs1)) = {
// was encoded in the instruction. We subtract the negative offset
// (add the positive offset) to get it. Normally this will be
// equal to rs1, but pointer masking can change that.
TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr - negative_offset, e)),
TR_Address(paddr, _) => {
Err(e, _) => RETIRE_FAIL(Memory_Exception(vaddr - negative_offset, e)),
Ok(paddr, _) => {
match mem_write_ea(paddr, cache_block_size, false, false, false) {
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr - negative_offset, e)),
Ok(_) => {
Expand Down
35 changes: 16 additions & 19 deletions model/riscv_vmem.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -209,10 +209,7 @@ function translationMode(priv : Privilege) -> SATPMode = {
// Result of address translation

// PUBLIC
union TR_Result('paddr : Type, 'failure : Type) = {
TR_Address : ('paddr, ext_ptw),
TR_Failure : ('failure, ext_ptw)
}
type TR_Result('paddr : Type, 'failure : Type) = result(('paddr, ext_ptw), ('failure, ext_ptw))

// This function can be ignored on first reading since TLBs are not
// part of RISC-V architecture spec (see TLB NOTE above).
Expand All @@ -239,15 +236,15 @@ function translate_TLB_hit forall 'v, is_sv_mode('v) . (

match pte_check {
PTE_Check_Failure(ext_ptw, ext_ptw_fail) =>
TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw),
Err(ext_get_ptw_error(ext_ptw_fail), ext_ptw),
PTE_Check_Success(ext_ptw) =>
match update_PTE_Bits(pte, ac) {
None() => TR_Address(tlb_get_ppn(sv_width, ent, vpn), ext_ptw),
None() => Ok(tlb_get_ppn(sv_width, ent, vpn), ext_ptw),
Some(pte') =>
// Step 9 of VATP. See riscv_platform.sail.
if not(plat_enable_dirty_update()) then
// pte needs dirty/accessed update but that is not enabled
TR_Failure(PTW_PTE_Update(), ext_ptw)
Err(PTW_PTE_Update(), ext_ptw)
else {
// Writeback the PTE (which has new A/D bits)
write_TLB(tlb_index, tlb_set_pte(ent, pte'));
Expand All @@ -256,7 +253,7 @@ function translate_TLB_hit forall 'v, is_sv_mode('v) . (
Err(e) => internal_error(__FILE__, __LINE__,
"invalid physical address in TLB")
};
TR_Address(tlb_get_ppn(sv_width, ent, vpn), ext_ptw)
Ok(tlb_get_ppn(sv_width, ent, vpn), ext_ptw)
}
}
}
Expand All @@ -281,30 +278,30 @@ function translate_TLB_miss forall 'v, is_sv_mode('v) . (
let ptw_result = pt_walk(sv_width, vpn, ac, priv, mxr, do_sum,
base_ppn, initial_level, false, ext_ptw);
match ptw_result {
Err(f, ext_ptw) => TR_Failure(f, ext_ptw),
Err(f, ext_ptw) => Err(f, ext_ptw),
Ok(struct {ppn, pte, pteAddr, level, global}, ext_ptw) => {
let ext_pte = ext_bits_of_PTE(pte);
// Without TLBs, this 'match' expression can be replaced simply
// by: 'TR_Address(ppn, ext_ptw)' (see TLB NOTE above)
// by: 'Ok(ppn, ext_ptw)' (see TLB NOTE above)
match update_PTE_Bits(pte, ac) {
None() => {
add_to_TLB(sv_width, asid, vpn, ppn, pte, pteAddr, level, global);
TR_Address(ppn, ext_ptw)
Ok(ppn, ext_ptw)
},
Some(pte) =>
// Step 9 of VATP. See riscv_platform.sail.
if not(plat_enable_dirty_update()) then
// pte needs dirty/accessed update but that is not enabled
TR_Failure(PTW_PTE_Update(), ext_ptw)
Err(PTW_PTE_Update(), ext_ptw)
else {
// Writeback the PTE (which has new A/D bits)
match write_pte(pteAddr, pte_width, pte) {
Ok(_) => {
add_to_TLB(sv_width, asid, vpn, ppn, pte, pteAddr, level, global);
TR_Address(ppn, ext_ptw)
Ok(ppn, ext_ptw)
},
Err(e) =>
TR_Failure(PTW_Access(), ext_ptw)
Err(PTW_Access(), ext_ptw)
}
}
}
Expand Down Expand Up @@ -367,7 +364,7 @@ function translateAddr(

let mode = translationMode(effPriv);

if mode == Bare then return TR_Address(Physaddr(zero_extend(bits_of(vAddr))), init_ext_ptw);
if mode == Bare then return Ok(Physaddr(zero_extend(bits_of(vAddr))), init_ext_ptw);

// Sv39 -> 39, etc.
let sv_width = satp_mode_width(mode);
Expand All @@ -380,7 +377,7 @@ function translateAddr(

let svAddr = bits_of(vAddr)[sv_width - 1 .. 0];
if bits_of(vAddr) != sign_extend(svAddr) then {
TR_Failure(translationException(ac, PTW_Invalid_Addr()), init_ext_ptw)
Err(translationException(ac, PTW_Invalid_Addr()), init_ext_ptw)
} else {
let mxr = mstatus[MXR] == 0b1;
let do_sum = mstatus[SUM] == 0b1;
Expand All @@ -397,17 +394,17 @@ function translateAddr(
init_ext_ptw);
// Fixup result PA or exception
match res {
TR_Address(ppn, ext_ptw) => {
Ok(ppn, ext_ptw) => {
// Step 10 of VATP.
// Append the page offset. This is now a 34 or 56 bit address.
let paddr = ppn @ bits_of(vAddr)[pagesize_bits - 1 .. 0];

// On RV64 paddr can be 34 or 56 bits, so we zero extend to 64.
// On RV32 paddr can only be 34 bits. Sail knows this due to
// the assertion above.
TR_Address(Physaddr(zero_extend(paddr)), ext_ptw)
Ok(Physaddr(zero_extend(paddr)), ext_ptw)
},
TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw)
Err(f, ext_ptw) => Err(translationException(ac, f), ext_ptw)
}
}
}
Expand Down
Loading