From 4799f996fc5b27f53a93a521db7ff2f54a5d3558 Mon Sep 17 00:00:00 2001 From: Prashanth Mundkur Date: Fri, 24 May 2019 14:22:18 -0700 Subject: Make xret hooks differentiate between just reading xret target values and getting the value when transferring control to the xret target. --- model/riscv_sys_control.sail | 6 +++--- model/riscv_sys_exceptions.sail | 12 +++++++++++- 2 files changed, 14 insertions(+), 4 deletions(-) (limited to 'model') diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 6bee610..e866986 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -366,7 +366,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, print_platform("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege); cancel_reservation(); - get_xret_target(Machine) & pc_alignment_mask() + prepare_xret_target(Machine) & pc_alignment_mask() }, (_, CTL_SRET()) => { let prev_priv = cur_privilege; @@ -380,7 +380,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, print_platform("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege); cancel_reservation(); - get_xret_target(Supervisor) & pc_alignment_mask() + prepare_xret_target(Supervisor) & pc_alignment_mask() }, (_, CTL_URET()) => { let prev_priv = cur_privilege; @@ -392,7 +392,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, print_platform("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege); cancel_reservation(); - get_xret_target(User) & pc_alignment_mask() + prepare_xret_target(User) & pc_alignment_mask() } } } diff --git a/model/riscv_sys_exceptions.sail b/model/riscv_sys_exceptions.sail index d2be25f..94d869e 100644 --- a/model/riscv_sys_exceptions.sail +++ b/model/riscv_sys_exceptions.sail @@ -17,7 +17,13 @@ function prepare_trap_vector(p : Privilege, cause : Mcause) -> xlenbits = { } } -/* used for xRET */ +/* xRET handling involves three functions: + * + * get_xret_target: used to read the value of the xret target (no control flow transfer) + * set_xret_target: used to write a value of the xret target (no control flow transfer) + * prepare_xret_target: used to get the value for control transfer to the xret target + */ + val get_xret_target : Privilege -> xlenbits effect {rreg} function get_xret_target(p) = match p { @@ -37,6 +43,10 @@ function set_xret_target(p, value) = { target } +val prepare_xret_target : (Privilege) -> xlenbits effect {rreg, wreg} +function prepare_xret_target(p) = + get_xret_target(p) + /* other trap-related CSRs */ function get_mtvec() -> xlenbits = -- cgit v1.1