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 <[email protected]>
seL4 · Jul 19, 2022 · cbd44c9 · cbd44c9
1 parent 8144e11
commit cbd44c9
Showing 1 changed file with 32 additions and 15 deletions.
diff --git a/spec/abstract/Decode_A.thy b/spec/abstract/Decode_A.thy
@@ -258,12 +258,31 @@ definition has_handler_rights :: "cap \<Rightarrow> bool" where
 definition valid_fault_handler :: "cap \<Rightarrow> bool" where
   "valid_fault_handler \<equiv> is_ep_cap and has_handler_rights or (=) NullCap"
 
-definition
-  check_handler_ep :: "nat \<Rightarrow> (cap \<times> cslot_ptr) \<Rightarrow> ((cap \<times> cslot_ptr),'z::state_ext) se_monad"
-where
+definition check_handler_ep ::
+  "nat \<Rightarrow> (cap \<times> cslot_ptr) \<Rightarrow> ((cap \<times> cslot_ptr),'z::state_ext) se_monad"
+  where
   "check_handler_ep pos h_cap_h_slot \<equiv> doE
     unlessE (valid_fault_handler $ fst h_cap_h_slot) $ throwError $ InvalidCapability pos;
     returnOk h_cap_h_slot
+   odE"
+
+definition update_handler_ep :: "data \<Rightarrow> data \<Rightarrow> cap \<Rightarrow> cap" where
+  "update_handler_ep data rights cap \<equiv>
+     if data \<noteq> 0 \<or> rights \<noteq> 0
+     then mask_cap (data_to_rights rights) (update_cap_data False data cap)
+     else cap"
+
+definition update_and_check_handler_ep ::
+  "data list \<Rightarrow> nat \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow> ((cap \<times> cslot_ptr),'z::state_ext) se_monad"
+  where
+  "update_and_check_handler_ep args pos excaps \<equiv> doE
+    fh_data  \<leftarrow> returnOk $ args ! 0;
+    fh_rights  \<leftarrow> returnOk $ args ! 1;
+    fh_arg  \<leftarrow> returnOk $ excaps ! 0;
+    fh_cap  \<leftarrow> returnOk $ fst fh_arg;
+    fh_slot \<leftarrow> returnOk $ snd fh_arg;
+    fh_cap \<leftarrow> 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 \<Rightarrow> cap \<Rightarrow> cslot_ptr \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow> (tcb_invocation,'z::state_ext) se_monad"
 where
   "decode_set_space args cap slot excaps \<equiv> doE
-    whenE (length args < 2 \<or> length excaps < 3) $ throwError TruncatedMessage;
-    space \<leftarrow> decode_cv_space (take 2 args) cap slot (take 2 (drop 1 excaps));
-    fh_arg  \<leftarrow> returnOk $ excaps ! 0;
-    fault_handler \<leftarrow> check_handler_ep 1 fh_arg;
+    whenE (length args < 4 \<or> length excaps < 3) $ throwError TruncatedMessage;
+    space \<leftarrow> decode_cv_space (take 2 (drop 2 args)) cap slot (take 2 (drop 1 excaps));
+    fault_handler \<leftarrow> 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 \<Rightarrow> cslot_ptr \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow> (tcb_invocation,'z::state_ext) se_monad"
+  "data list \<Rightarrow> cap \<Rightarrow> cslot_ptr \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow> (tcb_invocation,'z::state_ext) se_monad"
 where
-  "decode_set_timeout_ep cap slot extra_caps \<equiv> doE
+  "decode_set_timeout_ep args cap slot extra_caps \<equiv> doE
+     whenE (length args < 2) $ throwError TruncatedMessage;
      whenE (length extra_caps < 1) $ throwError TruncatedMessage;
-     th_arg \<leftarrow> returnOk $ extra_caps ! 0;
-     handler \<leftarrow> check_handler_ep 1 th_arg;
+     handler \<leftarrow> 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 \<Rightarrow> cap \<Rightarrow> cslot_ptr \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow> (tcb_invocation,'z::state_ext) se_monad"
 where
   "decode_set_sched_params args cap slot extra_caps \<equiv> doE
-     whenE (length args < 2) $ throwError TruncatedMessage;
+     whenE (length args < 4) $ throwError TruncatedMessage;
      whenE (length extra_caps < 3) $ throwError TruncatedMessage;
      new_mcp \<leftarrow> returnOk $ ucast $ args ! 0;
      new_prio \<leftarrow> returnOk $ ucast $ args ! 1;
      auth_cap \<leftarrow> returnOk $ fst $ extra_caps ! 0;
      sc_cap \<leftarrow> returnOk $ fst $ extra_caps ! 1;
-     fh_arg \<leftarrow> returnOk $ extra_caps ! 2;
      auth_tcb \<leftarrow> case auth_cap of
          ThreadCap tcb_ptr \<Rightarrow> returnOk tcb_ptr
        | _ \<Rightarrow> throwError (InvalidCapability 1);
      check_prio (args ! 0) auth_tcb;
      check_prio (args ! 1) auth_tcb;
      sc \<leftarrow> decode_update_sc cap slot sc_cap;
-     fh \<leftarrow> check_handler_ep 3 fh_arg;
+     fh \<leftarrow> 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 \<Rightarrow> decode_set_priority args cap slot excs
     | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args cap slot excs
     | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args cap slot excs
-    | TCBSetTimeoutEndpoint \<Rightarrow> decode_set_timeout_ep cap slot excs
+    | TCBSetTimeoutEndpoint \<Rightarrow> decode_set_timeout_ep args cap slot excs
     | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args cap slot excs
     | TCBSetSpace \<Rightarrow> decode_set_space args cap slot excs
     | TCBBindNotification \<Rightarrow> decode_bind_notification cap excs