From cbd44c9e318faed49599bf9c3e99f8f4c2e6a283 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Tue, 19 Jul 2022 16:05:24 +1000 Subject: [PATCH] rt aspec: set handler params when configuring TCBs This modifies the tcb_decode functions so that it is possible to set the badge and rights of fault and timeout handler caps. Signed-off-by: Corey Lewis --- spec/abstract/Decode_A.thy | 47 ++++++++++++++++++++++++++------------ 1 file changed, 32 insertions(+), 15 deletions(-) diff --git a/spec/abstract/Decode_A.thy b/spec/abstract/Decode_A.thy index 14bd2708d1..0243f0b238 100644 --- a/spec/abstract/Decode_A.thy +++ b/spec/abstract/Decode_A.thy @@ -258,12 +258,31 @@ definition has_handler_rights :: "cap \ bool" where definition valid_fault_handler :: "cap \ bool" where "valid_fault_handler \ is_ep_cap and has_handler_rights or (=) NullCap" -definition - check_handler_ep :: "nat \ (cap \ cslot_ptr) \ ((cap \ cslot_ptr),'z::state_ext) se_monad" -where +definition check_handler_ep :: + "nat \ (cap \ cslot_ptr) \ ((cap \ cslot_ptr),'z::state_ext) se_monad" + where "check_handler_ep pos h_cap_h_slot \ doE unlessE (valid_fault_handler $ fst h_cap_h_slot) $ throwError $ InvalidCapability pos; returnOk h_cap_h_slot + odE" + +definition update_handler_ep :: "data \ data \ cap \ cap" where + "update_handler_ep data rights cap \ + if data \ 0 \ rights \ 0 + then mask_cap (data_to_rights rights) (update_cap_data False data cap) + else cap" + +definition update_and_check_handler_ep :: + "data list \ nat \ (cap \ cslot_ptr) list \ ((cap \ cslot_ptr),'z::state_ext) se_monad" + where + "update_and_check_handler_ep args pos excaps \ doE + fh_data \ returnOk $ args ! 0; + fh_rights \ returnOk $ args ! 1; + fh_arg \ returnOk $ excaps ! 0; + fh_cap \ returnOk $ fst fh_arg; + fh_slot \ returnOk $ snd fh_arg; + fh_cap \ derive_cap fh_slot (update_handler_ep fh_data fh_rights fh_cap); + check_handler_ep pos (fh_cap, fh_slot) odE" definition @@ -308,10 +327,9 @@ definition :: "data list \ cap \ cslot_ptr \ (cap \ cslot_ptr) list \ (tcb_invocation,'z::state_ext) se_monad" where "decode_set_space args cap slot excaps \ doE - whenE (length args < 2 \ length excaps < 3) $ throwError TruncatedMessage; - space \ decode_cv_space (take 2 args) cap slot (take 2 (drop 1 excaps)); - fh_arg \ returnOk $ excaps ! 0; - fault_handler \ check_handler_ep 1 fh_arg; + whenE (length args < 4 \ length excaps < 3) $ throwError TruncatedMessage; + space \ decode_cv_space (take 2 (drop 2 args)) cap slot (take 2 (drop 1 excaps)); + fault_handler \ update_and_check_handler_ep (take 2 args) 1 (take 1 excaps); returnOk $ ThreadControlCaps (obj_ref_of cap) slot (Some fault_handler) None (tc_new_croot space) (tc_new_vroot space) None odE" @@ -360,12 +378,12 @@ where definition decode_set_timeout_ep :: - "cap \ cslot_ptr \ (cap \ cslot_ptr) list \ (tcb_invocation,'z::state_ext) se_monad" + "data list \ cap \ cslot_ptr \ (cap \ cslot_ptr) list \ (tcb_invocation,'z::state_ext) se_monad" where - "decode_set_timeout_ep cap slot extra_caps \ doE + "decode_set_timeout_ep args cap slot extra_caps \ doE + whenE (length args < 2) $ throwError TruncatedMessage; whenE (length extra_caps < 1) $ throwError TruncatedMessage; - th_arg \ returnOk $ extra_caps ! 0; - handler \ check_handler_ep 1 th_arg; + handler \ update_and_check_handler_ep args 1 extra_caps; returnOk $ ThreadControlCaps (obj_ref_of cap) slot None (Some handler) None None None odE" @@ -420,20 +438,19 @@ definition decode_set_sched_params :: "data list \ cap \ cslot_ptr \ (cap \ cslot_ptr) list \ (tcb_invocation,'z::state_ext) se_monad" where "decode_set_sched_params args cap slot extra_caps \ doE - whenE (length args < 2) $ throwError TruncatedMessage; + whenE (length args < 4) $ throwError TruncatedMessage; whenE (length extra_caps < 3) $ throwError TruncatedMessage; new_mcp \ returnOk $ ucast $ args ! 0; new_prio \ returnOk $ ucast $ args ! 1; auth_cap \ returnOk $ fst $ extra_caps ! 0; sc_cap \ returnOk $ fst $ extra_caps ! 1; - fh_arg \ returnOk $ extra_caps ! 2; auth_tcb \ case auth_cap of ThreadCap tcb_ptr \ returnOk tcb_ptr | _ \ throwError (InvalidCapability 1); check_prio (args ! 0) auth_tcb; check_prio (args ! 1) auth_tcb; sc \ decode_update_sc cap slot sc_cap; - fh \ check_handler_ep 3 fh_arg; + fh \ update_and_check_handler_ep (take 2 (drop 2 args)) 3 (drop 2 extra_caps); returnOk $ ThreadControlSched (obj_ref_of cap) slot (Some fh) (Some (new_mcp, auth_tcb)) (Some (new_prio, auth_tcb)) (Some sc) @@ -455,7 +472,7 @@ where | TCBSetPriority \ decode_set_priority args cap slot excs | TCBSetMCPriority \ decode_set_mcpriority args cap slot excs | TCBSetSchedParams \ decode_set_sched_params args cap slot excs - | TCBSetTimeoutEndpoint \ decode_set_timeout_ep cap slot excs + | TCBSetTimeoutEndpoint \ decode_set_timeout_ep args cap slot excs | TCBSetIPCBuffer \ decode_set_ipc_buffer args cap slot excs | TCBSetSpace \ decode_set_space args cap slot excs | TCBBindNotification \ decode_bind_notification cap excs