diff options
| author | Robert Norton <rmn30@cam.ac.uk> | 2019-11-05 13:52:05 +0000 |
|---|---|---|
| committer | Robert Norton <rmn30@cam.ac.uk> | 2019-11-05 13:52:05 +0000 |
| commit | 75550b059c957c65b7ee69a83ddfe53afbd147ac (patch) | |
| tree | 980801638a9b780efa43b679e2008e290766eee6 /model | |
| parent | f736870454a8ee8fabaf4a5ad4b3af938cfcb267 (diff) | |
| download | sail-riscv-75550b059c957c65b7ee69a83ddfe53afbd147ac.zip sail-riscv-75550b059c957c65b7ee69a83ddfe53afbd147ac.tar.gz sail-riscv-75550b059c957c65b7ee69a83ddfe53afbd147ac.tar.bz2 | |
Add a hook to allow extensions to veto xret. This will be used by CHERI extension. Note that illegal exception on mode check failure takes precedence over CHERI to allow for virtualisation.xret_ext
Diffstat (limited to 'model')
| -rw-r--r-- | model/riscv_insts_base.sail | 25 | ||||
| -rw-r--r-- | model/riscv_insts_next.sail | 2 | ||||
| -rw-r--r-- | model/riscv_sys_exceptions.sail | 5 |
3 files changed, 21 insertions, 11 deletions
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index d80d34d..bc86859 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -714,9 +714,11 @@ mapping clause encdec = MRET() <-> 0b0011000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 function clause execute MRET() = { - if cur_privilege == Machine - then set_next_pc(exception_handler(cur_privilege, CTL_MRET(), PC)) - else handle_illegal(); + if cur_privilege != Machine + then handle_illegal() + else if ~(ext_check_xret_priv (Machine)) + then ext_fail_xret_priv () + else set_next_pc(exception_handler(cur_privilege, CTL_MRET(), PC)); RETIRE_FAIL } @@ -729,15 +731,16 @@ mapping clause encdec = SRET() <-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 function clause execute SRET() = { - match cur_privilege { - User => handle_illegal(), - Supervisor => if (~ (haveSupMode ())) | mstatus.TSR() == 0b1 - then handle_illegal() - else set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC)), - Machine => if (~ (haveSupMode ())) - then handle_illegal() - else set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC)) + let sret_illegal : bool = match cur_privilege { + User => true, + Supervisor => ~ (haveSupMode ()) | mstatus.TSR() == 0b1, + Machine => ~ (haveSupMode ()) }; + if sret_illegal + then handle_illegal() + else if ~(ext_check_xret_priv (Supervisor)) + then ext_fail_xret_priv () + else set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC)); RETIRE_FAIL } diff --git a/model/riscv_insts_next.sail b/model/riscv_insts_next.sail index 2af2eeb..0d23452 100644 --- a/model/riscv_insts_next.sail +++ b/model/riscv_insts_next.sail @@ -9,6 +9,8 @@ mapping clause encdec = URET() function clause execute URET() = { if (~ (haveUsrMode())) then handle_illegal() + else if ~ (ext_check_xret_priv (User)) + then ext_fail_xret_priv () else set_next_pc(exception_handler(cur_privilege, CTL_URET(), PC)); RETIRE_FAIL } diff --git a/model/riscv_sys_exceptions.sail b/model/riscv_sys_exceptions.sail index 94d869e..fa693e8 100644 --- a/model/riscv_sys_exceptions.sail +++ b/model/riscv_sys_exceptions.sail @@ -2,6 +2,11 @@ type ext_exception = unit +/* Is XRET from given mode permitted by extension? */ +function ext_check_xret_priv (p : Privilege) : Privilege -> bool = true +/* Called if above check fails */ +function ext_fail_xret_priv () : unit -> unit = () + function handle_trap_extension(p : Privilege, pc : xlenbits, u : option(unit)) -> unit = () /* used for traps and ECALL */ |