1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7(* 8Retyping and untyped invocation 9*) 10 11chapter "Retyping and Untyped Invocations" 12 13theory Retype_A 14imports 15 CSpaceAcc_A 16 ArchVSpaceAcc_A 17 Invocations_A 18 ArchRetype_A 19begin 20 21context begin interpretation Arch . 22 23requalify_consts 24 arch_default_cap 25 default_arch_object 26 init_arch_objects 27 28end 29 30 31section "Creating Caps" 32 33text \<open>The original capability created when an object of a given type is 34created with a particular address and size.\<close> 35primrec 36 default_cap :: "apiobject_type \<Rightarrow> obj_ref \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> cap" 37where 38 "default_cap CapTableObject oref s _ = CNodeCap oref s []" 39| "default_cap Untyped oref s dev = UntypedCap dev oref s 0" 40| "default_cap TCBObject oref s _ = ThreadCap oref" 41| "default_cap EndpointObject oref s _ = EndpointCap oref 0 UNIV" 42| "default_cap NotificationObject oref s _ = 43 NotificationCap oref 0 {AllowRead, AllowWrite}" 44| "default_cap (ArchObject aobj) oref s dev = ArchObjectCap (arch_default_cap aobj oref s dev)" 45 46text \<open>Create and install a new capability to a newly created object.\<close> 47definition 48 create_cap :: 49 "apiobject_type \<Rightarrow> nat \<Rightarrow> cslot_ptr \<Rightarrow> bool \<Rightarrow> cslot_ptr \<times> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" 50where 51 "create_cap type bits untyped is_device \<equiv> \<lambda>(dest,oref). do 52 dest_p \<leftarrow> gets (\<lambda>s. cdt s dest); 53 cdt \<leftarrow> gets cdt; 54 set_cdt (cdt (dest \<mapsto> untyped)); 55 do_extended_op (create_cap_ext untyped dest dest_p); 56 set_original dest True; 57 set_cap (default_cap type oref bits is_device) dest 58 od" 59 60section "Creating Objects" 61 62text \<open>Properties of an empty CNode object.\<close> 63definition 64 empty_cnode :: "nat \<Rightarrow> cnode_contents" where 65 "empty_cnode bits \<equiv> \<lambda>x. if length x = bits then Some NullCap else None" 66 67 68text \<open>The initial state objects of various types are in when created.\<close> 69definition 70 default_object :: "apiobject_type \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> kernel_object" where 71 "default_object api dev n \<equiv> case api of 72 Untyped \<Rightarrow> undefined 73 | CapTableObject \<Rightarrow> CNode n (empty_cnode n) 74 | TCBObject \<Rightarrow> TCB default_tcb 75 | EndpointObject \<Rightarrow> Endpoint default_ep 76 | NotificationObject \<Rightarrow> Notification default_notification 77 | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev n)" 78 79text \<open>The size in bits of the objects that will be created when a given type 80and size is requested.\<close> 81definition 82 obj_bits_api :: "apiobject_type \<Rightarrow> nat \<Rightarrow> nat" where 83 "obj_bits_api type obj_size_bits \<equiv> case type of 84 Untyped \<Rightarrow> obj_size_bits 85 | CapTableObject \<Rightarrow> obj_size_bits + slot_bits 86 | TCBObject \<Rightarrow> obj_bits (TCB default_tcb) 87 | EndpointObject \<Rightarrow> obj_bits (Endpoint undefined) 88 | NotificationObject \<Rightarrow> obj_bits (Notification undefined) 89 | ArchObject aobj \<Rightarrow> obj_bits $ ArchObj $ default_arch_object aobj False obj_size_bits" 90 91section "Main Retype Implementation" 92 93text \<open> 94Create @{text "numObjects"} objects, starting from 95@{text obj_ref}, return of list pointers to them. For some types, each 96returned pointer points to a group of objects. 97\<close> 98 99definition 100 retype_region :: "obj_ref \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> apiobject_type \<Rightarrow> bool \<Rightarrow> (obj_ref list,'z::state_ext) s_monad" 101where 102 "retype_region ptr numObjects o_bits type dev \<equiv> do 103 obj_size \<leftarrow> return $ 2 ^ obj_bits_api type o_bits; 104 ptrs \<leftarrow> return $ map (\<lambda>p. ptr_add ptr (p * obj_size)) [0..< numObjects]; 105 when (type \<noteq> Untyped) (do 106 kh \<leftarrow> gets kheap; 107 kh' \<leftarrow> return $ foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits)) ptrs kh; 108 do_extended_op (retype_region_ext ptrs type); 109 modify $ kheap_update (K kh') 110 od); 111 return $ ptrs 112 od" 113 114section "Invoking Untyped Capabilities" 115 116abbreviation (input) "extended_state_update \<equiv> trans_state" 117 118text \<open>Remove objects from a region of the heap.\<close> 119definition 120 detype :: "(obj_ref set) \<Rightarrow> 'z::state_ext state \<Rightarrow> 'z::state_ext state" where 121 "detype S s \<equiv> s \<lparr> kheap := (\<lambda>x. if x \<in> S then None else kheap s x), extended_state := detype_ext S (exst s)\<rparr>" 122 123text \<open>Delete objects within a specified region.\<close> 124definition 125 delete_objects :: "machine_word \<Rightarrow> nat \<Rightarrow> (unit,'z::state_ext) s_monad" where 126 "delete_objects ptr bits = do 127 do_machine_op (freeMemory ptr bits); 128 modify (detype {ptr..ptr + 2 ^ bits - 1}) 129 od" 130 131(* FIXME: we need a sensible place for these configurable constants. *) 132definition 133 reset_chunk_bits :: nat where 134 "reset_chunk_bits = 8" 135 136definition 137 get_free_ref :: "obj_ref \<Rightarrow> nat \<Rightarrow> obj_ref" where 138 "get_free_ref base free_index \<equiv> base + (of_nat free_index)" 139 140definition 141 get_free_index :: "obj_ref \<Rightarrow> obj_ref \<Rightarrow> nat" where 142 "get_free_index base free \<equiv> unat $ (free - base)" 143 144primrec(nonexhaustive) is_device_untyped_cap 145where 146 "is_device_untyped_cap (UntypedCap isdev _ _ _) = isdev" 147 148text \<open>Untyped capabilities note a currently free region. Sometimes this 149region is reset during a Retype operation. This progressively clears the 150underlying memory and also the object level representation, moving the free 151region pointer back to the start of the newly cleared region each time.\<close> 152definition 153 reset_untyped_cap :: "cslot_ptr \<Rightarrow> (unit,'z::state_ext) p_monad" 154where 155 "reset_untyped_cap src_slot = doE 156 cap \<leftarrow> liftE $ get_cap src_slot; 157 sz \<leftarrow> returnOk $ bits_of cap; 158 base \<leftarrow> returnOk $ obj_ref_of cap; 159 if free_index_of cap = 0 160 then returnOk () 161 else doE 162 liftE $ delete_objects base sz; 163 dev \<leftarrow> returnOk $ is_device_untyped_cap cap; 164 165 if dev \<or> sz < reset_chunk_bits 166 then liftE $ do 167 unless dev $ do_machine_op $ clearMemory base (2 ^ sz); 168 set_cap (UntypedCap dev base sz 0) src_slot 169 od 170 else mapME_x (\<lambda>i. doE 171 liftE $ do_machine_op $ clearMemory (base + (of_nat i << reset_chunk_bits)) 172 (2 ^ reset_chunk_bits); 173 liftE $ set_cap (UntypedCap dev base sz 174 (i * 2 ^ reset_chunk_bits)) src_slot; 175 preemption_point 176 odE) (rev [i \<leftarrow> [0 ..< 2 ^ (sz - reset_chunk_bits)]. 177 i * 2 ^ reset_chunk_bits < free_index_of cap]) 178 odE 179 odE" 180 181text \<open>Untyped capabilities confer authority to the Retype method. This 182clears existing objects from a region, creates new objects of the requested type, 183initialises them and installs new capabilities to them.\<close> 184definition 185 invoke_untyped :: "untyped_invocation \<Rightarrow> (unit,'z::state_ext) p_monad" 186where 187"invoke_untyped ui \<equiv> case ui 188 of Retype src_slot reset base retype_base new_type obj_sz slots is_device \<Rightarrow> 189doE 190 whenE reset $ reset_untyped_cap src_slot; 191 liftE $ do 192 193 cap \<leftarrow> get_cap src_slot; 194 195 \<comment> \<open>Update the untyped cap to track the amount of space used.\<close> 196 total_object_size \<leftarrow> return $ (of_nat (length slots) << (obj_bits_api new_type obj_sz)); 197 free_ref \<leftarrow> return $ retype_base + total_object_size; 198 set_cap (UntypedCap is_device base (bits_of cap) (unat (free_ref - base))) src_slot; 199 200 \<comment> \<open>Create new objects.\<close> 201 orefs \<leftarrow> retype_region retype_base (length slots) obj_sz new_type is_device; 202 init_arch_objects new_type retype_base (length slots) obj_sz orefs; 203 sequence_x (map (create_cap new_type obj_sz src_slot is_device) (zip slots orefs)) 204od odE" 205 206end 207