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