diff options
| -rw-r--r-- | riscv/riscv_vmem.sail | 47 |
1 files changed, 32 insertions, 15 deletions
diff --git a/riscv/riscv_vmem.sail b/riscv/riscv_vmem.sail index 0c1b9949..cc365769 100644 --- a/riscv/riscv_vmem.sail +++ b/riscv/riscv_vmem.sail @@ -128,7 +128,7 @@ union PTW_Result = { val walk39 : (vaddr39, AccessType, Privilege, bool, bool, paddr39, nat, bool) -> PTW_Result effect {rmem, escape} function walk39(vaddr, ac, priv, mxr, sum, ptb, level, global) -> PTW_Result = { let va = Mk_SV39_Vaddr(vaddr); - let pt_ofs : paddr39 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[SV39_LEVEL_BITS .. 0]), + let pt_ofs : paddr39 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]), PTE39_LOG_SIZE); let pte_addr = ptb + pt_ofs; match (checked_mem_read(Data, EXTZ(pte_addr), 8)) { @@ -142,22 +142,32 @@ function walk39(vaddr, ac, priv, mxr, sum, ptb, level, global) -> PTW_Result = { PTW_Failure(PTW_Invalid_PTE) } else { if isPTEPtr(pbits) then { - if level == 0 then PTW_Failure(PTW_Invalid_PTE) - else walk39(vaddr, ac, priv, mxr, sum, EXTZ(pte.PPNi()), level - 1, is_global) + if level == 0 then { + /* last-level PTE contains a pointer instead of a leaf */ + PTW_Failure(PTW_Invalid_PTE) + } else { + /* walk down the pointer to the next level */ + walk39(vaddr, ac, priv, mxr, sum, EXTZ(shiftl(pte.PPNi(), PAGESIZE_BITS)), level - 1, is_global) + } } else { /* leaf PTE */ - if ~ (checkPTEPermission(ac, priv, mxr, sum, pattr)) then + if ~ (checkPTEPermission(ac, priv, mxr, sum, pattr)) then { PTW_Failure(PTW_No_Permission) - else { + } else { if level > 0 then { /* superpage */ - let masked = pte.PPNi() & EXTZ(shiftl(0b1, level * SV39_LEVEL_BITS) - 1); - if masked != EXTZ(0b0) then + /* fixme hack: to get a mask of appropriate size */ + let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV39_LEVEL_BITS) - 1; + if (pte.PPNi() & mask) != EXTZ(0b0) then { + /* misaligned superpage mapping */ PTW_Failure(PTW_Misaligned) - else { - let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & EXTZ(shiftl(0b1, level * SV39_LEVEL_BITS) - 1)); + } else { + /* add the appropriate bits of the VPN to the superpage PPN */ + let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask); PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global) } - } else + } else { + /* normal leaf PTE */ PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global) + } } } } @@ -260,8 +270,10 @@ function translate39(vAddr, ac, priv, mxr, sum, level) = { None() => TR39_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)), Some(pbits) => { if ~ (enable_dirty_update) - then TR39_Failure(PTW_PTE_Update) - else { + then { + /* pte needs dirty/accessed update but that is not enabled */ + TR39_Failure(PTW_PTE_Update) + } else { /* update PTE entry and TLB */ n_ent : TLB39_Entry = ent; n_ent.pte = update_BITS(ent.pte, pbits.bits()); @@ -288,15 +300,20 @@ function translate39(vAddr, ac, priv, mxr, sum, level) = { }, Some(pbits) => if ~ (enable_dirty_update) - then TR39_Failure(PTW_PTE_Update) - else { + then { + /* pte needs dirty/accessed update but that is not enabled */ + TR39_Failure(PTW_PTE_Update) + } else { w_pte : SV39_PTE = update_BITS(pte, pbits.bits()); match checked_mem_write(EXTZ(pteAddr), 8, w_pte.bits()) { MemValue(_) => { addToTLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global); TR39_Address(pAddr) }, - MemException(e) => TR39_Failure(PTW_Access) + MemException(e) => { + /* pte is not in valid memory */ + TR39_Failure(PTW_Access) + } } } } |