1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7(* 8Decoding system calls 9*) 10 11chapter "Decoding Architecture-specific System Calls" 12 13theory ArchDecode_A 14imports 15 Interrupt_A 16 InvocationLabels_A 17begin 18context Arch begin global_naming ARM_A 19 20section "Helper definitions" 21 22text \<open>This definition ensures that the given pointer is aligned 23to the given page size.\<close> 24 25definition 26 check_vp_alignment :: "vmpage_size \<Rightarrow> word32 \<Rightarrow> (unit,'z::state_ext) se_monad" where 27 "check_vp_alignment sz vptr \<equiv> 28 unlessE (is_aligned vptr (pageBitsForSize sz)) $ 29 throwError AlignmentError" 30 31text \<open>This definition converts a user-supplied argument into an 32invocation label, used to determine the method to invoke. 33\<close> 34 35definition 36 label_to_flush_type :: "invocation_label \<Rightarrow> flush_type" 37where 38 "label_to_flush_type label \<equiv> case label of 39 ArchInvocationLabel ARMPDClean_Data \<Rightarrow> Clean 40 | ArchInvocationLabel ARMPageClean_Data \<Rightarrow> Clean 41 | ArchInvocationLabel ARMPDInvalidate_Data \<Rightarrow> Invalidate 42 | ArchInvocationLabel ARMPageInvalidate_Data \<Rightarrow> Invalidate 43 | ArchInvocationLabel ARMPDCleanInvalidate_Data \<Rightarrow> CleanInvalidate 44 | ArchInvocationLabel ARMPageCleanInvalidate_Data \<Rightarrow> CleanInvalidate 45 | ArchInvocationLabel ARMPDUnify_Instruction \<Rightarrow> Unify 46 | ArchInvocationLabel ARMPageUnify_Instruction \<Rightarrow> Unify" 47 48section "Architecture calls" 49 50text \<open>This definition decodes architecture-specific invocations. 51\<close> 52 53definition 54 page_base :: "vspace_ref \<Rightarrow> vmpage_size \<Rightarrow> vspace_ref" 55where 56 "page_base vaddr vmsize \<equiv> vaddr && ~~ mask (pageBitsForSize vmsize)" 57 58 59definition 60 arch_decode_invocation :: 61 "data \<Rightarrow> data list \<Rightarrow> cap_ref \<Rightarrow> cslot_ptr \<Rightarrow> arch_cap \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow> 62 (arch_invocation,'z::state_ext) se_monad" 63where 64"arch_decode_invocation label args x_slot cte cap extra_caps \<equiv> case cap of 65 66 PageDirectoryCap _ _ \<Rightarrow> 67 if isPDFlushLabel (invocation_type label) then 68 if length args > 1 69 then let start = args ! 0; 70 end = args ! 1 71 in doE 72 whenE (end \<le> start) $ throwError $ InvalidArgument 1; 73 whenE (start \<ge> kernel_base \<or> end > kernel_base) $ throwError IllegalOperation; 74 (pd,asid) \<leftarrow> (case cap of 75 PageDirectoryCap pd (Some asid) \<Rightarrow> returnOk (pd,asid) 76 | _ \<Rightarrow> throwError $ InvalidCapability 0); 77 pd' \<leftarrow> lookup_error_on_failure False $ find_pd_for_asid asid; 78 whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 0; 79 frame_info \<leftarrow> liftE $ resolve_vaddr pd start; 80 case frame_info of 81 None \<Rightarrow> returnOk $ InvokePageDirectory PageDirectoryNothing 82 | Some (frame_size, frame_base) \<Rightarrow> 83 let base_start = page_base start frame_size; 84 base_end = page_base (end - 1) frame_size; 85 offset = start && mask (pageBitsForSize frame_size); 86 pstart = frame_base + offset 87 in doE 88 whenE (base_start \<noteq> base_end) $ throwError $ 89 RangeError start (base_start + mask (pageBitsForSize frame_size)); 90 returnOk $ InvokePageDirectory $ 91 PageDirectoryFlush (label_to_flush_type (invocation_type label)) 92 start (end - 1) pstart pd asid 93 odE 94 odE 95 else throwError TruncatedMessage 96 else throwError IllegalOperation 97 98| PageTableCap p mapped_address \<Rightarrow> 99 if invocation_type label = ArchInvocationLabel ARMPageTableMap then 100 if length args > 1 \<and> length extra_caps > 0 101 then let vaddr = args ! 0; 102 attr = args ! 1; 103 pd_cap = fst (extra_caps ! 0) 104 in doE 105 whenE (mapped_address \<noteq> None) $ throwError $ InvalidCapability 0; 106 (pd,asid) \<leftarrow> (case pd_cap of 107 ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> 108 returnOk (pd,asid) 109 | _ \<Rightarrow> throwError $ InvalidCapability 1); 110 whenE (vaddr \<ge> kernel_base) $ throwError $ InvalidArgument 0; 111 pd' \<leftarrow> lookup_error_on_failure False $ find_pd_for_asid asid; 112 whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 1; 113 pd_index \<leftarrow> returnOk (shiftr vaddr 20); 114 vaddr' \<leftarrow> returnOk (vaddr && ~~ mask 20); 115 pd_slot \<leftarrow> returnOk (pd + (pd_index << 2)); 116 oldpde \<leftarrow> liftE $ get_master_pde pd_slot; 117 unlessE (oldpde = InvalidPDE) $ throwError DeleteFirst; 118 pde \<leftarrow> returnOk (PageTablePDE (addrFromPPtr p) 119 (attribs_from_word attr \<inter> {ParityEnabled}) 0); 120 returnOk $ InvokePageTable $ 121 PageTableMap 122 (ArchObjectCap $ PageTableCap p (Some (asid, vaddr'))) 123 cte pde pd_slot 124 odE 125 else throwError TruncatedMessage 126 else if invocation_type label = ArchInvocationLabel ARMPageTableUnmap 127 then doE 128 final \<leftarrow> liftE $ is_final_cap (ArchObjectCap cap); 129 unlessE final $ throwError RevokeFirst; 130 returnOk $ InvokePageTable $ PageTableUnmap (ArchObjectCap cap) cte 131 odE 132 else throwError IllegalOperation 133 134| PageCap dev p R pgsz mapped_address \<Rightarrow> 135 if invocation_type label = ArchInvocationLabel ARMPageMap then 136 if length args > 2 \<and> length extra_caps > 0 137 then let vaddr = args ! 0; 138 rights_mask = args ! 1; 139 attr = args ! 2; 140 pd_cap = fst (extra_caps ! 0) 141 in doE 142 (pd,asid) \<leftarrow> (case pd_cap of 143 ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> 144 returnOk (pd,asid) 145 | _ \<Rightarrow> throwError $ InvalidCapability 1); 146 case mapped_address of 147 Some (asid', vaddr') \<Rightarrow> doE 148 whenE (asid' \<noteq> asid) (throwError $ InvalidCapability 1); 149 whenE (vaddr' \<noteq> vaddr) (throwError $ InvalidArgument 0) 150 odE 151 | None \<Rightarrow> doE 152 vtop \<leftarrow> returnOk (vaddr + (1 << (pageBitsForSize pgsz)) - 1); 153 whenE (vtop \<ge> kernel_base) $ throwError $ InvalidArgument 0 154 odE; 155 pd' \<leftarrow> lookup_error_on_failure False $ find_pd_for_asid asid; 156 whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 1; 157 vm_rights \<leftarrow> returnOk (mask_vm_rights R (data_to_rights rights_mask)); 158 check_vp_alignment pgsz vaddr; 159 entries \<leftarrow> create_mapping_entries (addrFromPPtr p) 160 vaddr pgsz vm_rights 161 (attribs_from_word attr) pd; 162 ensure_safe_mapping entries; 163 returnOk $ InvokePage $ PageMap asid 164 (ArchObjectCap $ PageCap dev p R pgsz (Some (asid, vaddr))) 165 cte entries 166 odE 167 else throwError TruncatedMessage 168 else if invocation_type label = ArchInvocationLabel ARMPageUnmap 169 then returnOk $ InvokePage $ PageUnmap cap cte 170 else if isPageFlushLabel (invocation_type label) then 171 if length args > 1 172 then let start = args ! 0; 173 end = args ! 1 174 in doE 175 (asid, vaddr) \<leftarrow> (case mapped_address of 176 Some a \<Rightarrow> returnOk a 177 | _ \<Rightarrow> throwError IllegalOperation); 178 pd \<leftarrow> lookup_error_on_failure False $ find_pd_for_asid asid; 179 whenE (end \<le> start) $ throwError $ InvalidArgument 1; 180 page_size \<leftarrow> returnOk $ 1 << pageBitsForSize pgsz; 181 whenE (start \<ge> page_size \<or> end > page_size) $ throwError $ InvalidArgument 0; 182 returnOk $ InvokePage $ PageFlush 183 (label_to_flush_type (invocation_type label)) (start + vaddr) 184 (end + vaddr - 1) (addrFromPPtr p + start) pd asid 185 odE 186 else throwError TruncatedMessage 187 else if invocation_type label = ArchInvocationLabel ARMPageGetAddress 188 then returnOk $ InvokePage $ PageGetAddr p 189 else throwError IllegalOperation 190 191| ASIDControlCap \<Rightarrow> 192 if invocation_type label = ArchInvocationLabel ARMASIDControlMakePool then 193 if length args > 1 \<and> length extra_caps > 1 194 then let index = args ! 0; 195 depth = args ! 1; 196 (untyped, parent_slot) = extra_caps ! 0; 197 root = fst (extra_caps ! 1) 198 in doE 199 asid_table \<leftarrow> liftE $ gets (arm_asid_table \<circ> arch_state); 200 free_set \<leftarrow> returnOk (- dom asid_table \<inter> {x. x \<le> 2 ^ asid_high_bits - 1}); 201 whenE (free_set = {}) $ throwError DeleteFirst; 202 free \<leftarrow> liftE $ select_ext (\<lambda>_. free_asid_select asid_table) free_set; 203 base \<leftarrow> returnOk (ucast free << asid_low_bits); 204 (p,n) \<leftarrow> (case untyped of UntypedCap False p n f \<Rightarrow> returnOk (p,n) 205 | _ \<Rightarrow> throwError $ InvalidCapability 1); 206 frame \<leftarrow> (if n = pageBits 207 then doE 208 ensure_no_children parent_slot; 209 returnOk p 210 odE 211 else throwError $ InvalidCapability 1); 212 dest_slot \<leftarrow> lookup_target_slot root (to_bl index) (unat depth); 213 ensure_empty dest_slot; 214 returnOk $ InvokeASIDControl $ MakePool frame dest_slot parent_slot base 215 odE 216 else throwError TruncatedMessage 217 else throwError IllegalOperation 218 219| ASIDPoolCap p base \<Rightarrow> 220 if invocation_type label = ArchInvocationLabel ARMASIDPoolAssign then 221 if length extra_caps > 0 222 then 223 let (pd_cap, pd_cap_slot) = extra_caps ! 0 224 in case pd_cap of 225 ArchObjectCap (PageDirectoryCap _ None) \<Rightarrow> doE 226 asid_table \<leftarrow> liftE $ gets (arm_asid_table \<circ> arch_state); 227 pool_ptr \<leftarrow> returnOk (asid_table (asid_high_bits_of base)); 228 whenE (pool_ptr = None) $ throwError $ FailedLookup False InvalidRoot; 229 whenE (p \<noteq> the pool_ptr) $ throwError $ InvalidCapability 0; 230 pool \<leftarrow> liftE $ get_asid_pool p; 231 free_set \<leftarrow> returnOk (- dom pool \<inter> {x. ucast x + base \<noteq> 0}); 232 whenE (free_set = {}) $ throwError DeleteFirst; 233 offset \<leftarrow> liftE $ select_ext (\<lambda>_. free_asid_pool_select pool base) free_set; 234 returnOk $ InvokeASIDPool $ Assign (ucast offset + base) p pd_cap_slot 235 odE 236 | _ \<Rightarrow> throwError $ InvalidCapability 1 237 else throwError TruncatedMessage 238 else throwError IllegalOperation" 239 240 241definition 242 arch_data_to_obj_type :: "nat \<Rightarrow> aobject_type option" where 243 "arch_data_to_obj_type n \<equiv> 244 if n = 0 then Some SmallPageObj 245 else if n = 1 then Some LargePageObj 246 else if n = 2 then Some SectionObj 247 else if n = 3 then Some SuperSectionObj 248 else if n = 4 then Some PageTableObj 249 else if n = 5 then Some PageDirectoryObj 250 else None" 251 252definition 253 arch_check_irq :: "data \<Rightarrow> (unit,'z::state_ext) se_monad" 254where 255 "arch_check_irq irq \<equiv> whenE (irq > ucast maxIRQ) $ throwError (RangeError 0 (ucast maxIRQ))" 256 257definition arch_decode_irq_control_invocation :: 258 "data \<Rightarrow> data list \<Rightarrow> cslot_ptr \<Rightarrow> cap list \<Rightarrow> (arch_irq_control_invocation,'z::state_ext) se_monad" 259 where 260 "arch_decode_irq_control_invocation label args src_slot cps \<equiv> 261 (if invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler 262 then if length args \<ge> 4 \<and> length cps \<ge> 1 263 then let irq_word = args ! 0; 264 trigger = args ! 1; 265 index = args ! 2; 266 depth = args ! 3; 267 cnode = cps ! 0; 268 irq = ucast irq_word 269 in doE 270 arch_check_irq irq_word; 271 irq_active \<leftarrow> liftE $ is_irq_active irq; 272 whenE irq_active $ throwError RevokeFirst; 273 274 dest_slot \<leftarrow> lookup_target_slot cnode (data_to_cptr index) (unat depth); 275 ensure_empty dest_slot; 276 277 returnOk $ ArchIRQControlIssue irq dest_slot src_slot (trigger \<noteq> 0) 278 odE 279 else throwError TruncatedMessage 280 else throwError IllegalOperation)" 281 282end 283 284end 285