diff options
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/ROOT | 4 | ||||
| -rw-r--r-- | riscv/main.sail | 1 | ||||
| -rw-r--r-- | riscv/prelude.sail | 10 | ||||
| -rw-r--r-- | riscv/riscv.sail | 3 | ||||
| -rw-r--r-- | riscv/riscv_types.sail | 1 | ||||
| -rw-r--r-- | riscv/riscv_vmem.sail | 24 |
6 files changed, 23 insertions, 20 deletions
diff --git a/riscv/ROOT b/riscv/ROOT new file mode 100644 index 00000000..cfc7f5bd --- /dev/null +++ b/riscv/ROOT @@ -0,0 +1,4 @@ +session "Sail-RISC-V" = "Sail" + + options [document = false] + theories + Riscv_lemmas diff --git a/riscv/main.sail b/riscv/main.sail index 8accaf5b..e108c3dc 100644 --- a/riscv/main.sail +++ b/riscv/main.sail @@ -51,7 +51,6 @@ function main () = { loop () } catch { Error_not_implemented(s) => print_string("Error: Not implemented: ", s), - Error_EBREAK() => print("EBREAK"), Error_internal_error() => print("Error: internal error") }*/ } diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 7ce12d79..7ac0066a 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -401,11 +401,11 @@ infix 4 <_u infix 4 >=_u infix 4 <=_u -val operator <_s = {lem: "slt_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val operator >=_s = {lem: "sgteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val operator <_u = {lem: "ult_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val operator >=_u = {lem: "ugteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val operator <=_u = {lem: "ulteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool +val operator <_s : forall 'n. (bits('n), bits('n)) -> bool +val operator >=_s : forall 'n. (bits('n), bits('n)) -> bool +val operator <_u : forall 'n. (bits('n), bits('n)) -> bool +val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool +val operator <=_u : forall 'n. (bits('n), bits('n)) -> bool function operator <_s (x, y) = signed(x) < signed(y) function operator >=_s (x, y) = signed(x) >= signed(y) diff --git a/riscv/riscv.sail b/riscv/riscv.sail index 84f0f279..9c5e196c 100644 --- a/riscv/riscv.sail +++ b/riscv/riscv.sail @@ -697,7 +697,8 @@ union clause ast = EBREAK : unit function clause decode 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(EBREAK()) -function clause execute EBREAK() = { throw Error_EBREAK() } +function clause execute EBREAK() = + handle_mem_exception(PC, E_Breakpoint) function clause print_insn (EBREAK()) = "ebreak" diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail index 8eefd9d6..07802524 100644 --- a/riscv/riscv_types.sail +++ b/riscv/riscv_types.sail @@ -259,7 +259,6 @@ function trapVectorMode_of_bits (m) = { union exception = { Error_not_implemented : string, - Error_EBREAK : unit, Error_internal_error : unit } diff --git a/riscv/riscv_vmem.sail b/riscv/riscv_vmem.sail index 7fddb047..4fb7b5d5 100644 --- a/riscv/riscv_vmem.sail +++ b/riscv/riscv_vmem.sail @@ -27,16 +27,16 @@ function isInvalidPTE(p : pteAttribs) -> bool = { a.V() == false | (a.W() == true & a.R() == false) } -function checkPTEPermission(ac : AccessType, priv : Privilege, mxr : bool, sum : bool, p : PTE_Bits) -> bool = { +function checkPTEPermission(ac : AccessType, priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits) -> bool = { match (ac, priv) { (Read, User) => p.U() == true & (p.R() == true | (p.X() == true & mxr)), (Write, User) => p.U() == true & p.W() == true, (ReadWrite, User) => p.U() == true & p.W() == true & (p.R() == true | (p.X() == true & mxr)), (Execute, User) => p.U() == true & p.X() == true, - (Read, Supervisor) => (p.U() == false | sum) & (p.R() == true | (p.X() == true & mxr)), - (Write, Supervisor) => (p.U() == false | sum) & p.W() == true, - (ReadWrite, Supervisor) => (p.U() == false | sum) & p.W() == true & (p.R() == true | (p.X() == true & mxr)), + (Read, Supervisor) => (p.U() == false | do_sum) & (p.R() == true | (p.X() == true & mxr)), + (Write, Supervisor) => (p.U() == false | do_sum) & p.W() == true, + (ReadWrite, Supervisor) => (p.U() == false | do_sum) & p.W() == true & (p.R() == true | (p.X() == true & mxr)), (Execute, Supervisor) => p.U() == false & p.X() == true, (_, Machine) => internal_error("m-mode mem perm check") @@ -126,7 +126,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 = { +function walk39(vaddr, ac, priv, mxr, do_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 - 1) .. 0]), PTE39_LOG_SIZE); @@ -147,10 +147,10 @@ function walk39(vaddr, ac, priv, mxr, sum, ptb, level, global) -> PTW_Result = { 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) + walk39(vaddr, ac, priv, mxr, do_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, do_sum, pattr)) then { PTW_Failure(PTW_No_Permission) } else { if level > 0 then { /* superpage */ @@ -259,12 +259,12 @@ union TR39_Result = { let enable_dirty_update = false val translate39 : (vaddr39, AccessType, Privilege, bool, bool, nat) -> TR39_Result effect {rreg, wreg, wmv, escape, rmem} -function translate39(vAddr, ac, priv, mxr, sum, level) = { +function translate39(vAddr, ac, priv, mxr, do_sum, level) = { let asid = curAsid64(); match lookupTLB39(asid, vAddr) { Some(idx, ent) => { let pteBits = Mk_PTE_Bits(ent.pte.BITS()); - if ~ (checkPTEPermission(ac, priv, mxr, sum, pteBits)) + if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pteBits)) then TR39_Failure(PTW_No_Permission) else { match update_PTE_Bits(pteBits, ac) { @@ -291,7 +291,7 @@ function translate39(vAddr, ac, priv, mxr, sum, level) = { } }, None() => { - match walk39(vAddr, ac, priv, mxr, sum, curPTB39(), level, false) { + match walk39(vAddr, ac, priv, mxr, do_sum, curPTB39(), level, false) { PTW_Failure(f) => TR39_Failure(f), PTW_Success(pAddr, pte, pteAddr, level, global) => { match update_PTE_Bits(Mk_PTE_Bits(pte.BITS()), ac) { @@ -360,11 +360,11 @@ function translateAddr(vAddr, ac, rt) = { else cur_privilege }; let mxr : bool = mstatus.MXR() == true; - let sum : bool = mstatus.SUM() == true; + let do_sum : bool = mstatus.SUM() == true; let mode : SATPMode = translationMode(effPriv); match mode { Sbare => TR_Address(vAddr), - SV39 => match translate39(vAddr[38 .. 0], ac, effPriv, mxr, sum, SV39_LEVELS - 1) { + SV39 => match translate39(vAddr[38 .. 0], ac, effPriv, mxr, do_sum, SV39_LEVELS - 1) { TR39_Address(pa) => TR_Address(EXTZ(pa)), TR39_Failure(f) => TR_Failure(translationException(ac, f)) }, |