1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(NICTA_GPL)
9 *)
10
11theory Decode_D
12imports
13  Asid_D
14  CNode_D
15  Interrupt_D
16  PageTable_D
17  Tcb_D
18  Untyped_D
19begin
20
21definition
22  get_cnode_intent :: "cdl_intent \<Rightarrow> cdl_cnode_intent option"
23where
24  "get_cnode_intent intent \<equiv>
25    case intent of
26        CNodeIntent x \<Rightarrow> Some x
27      | _ \<Rightarrow> None"
28
29definition
30  get_tcb_intent :: "cdl_intent \<Rightarrow> cdl_tcb_intent option"
31where
32  "get_tcb_intent intent \<equiv>
33    case intent of
34        TcbIntent x \<Rightarrow> Some x
35      | _ \<Rightarrow> None"
36
37definition
38  get_irq_control_intent :: "cdl_intent \<Rightarrow> cdl_irq_control_intent option"
39where
40  "get_irq_control_intent intent \<equiv>
41    case intent of
42        IrqControlIntent x \<Rightarrow> Some x
43      | _ \<Rightarrow> None"
44
45definition
46  get_irq_handler_intent :: "cdl_intent \<Rightarrow> cdl_irq_handler_intent option"
47where
48  "get_irq_handler_intent intent \<equiv>
49    case intent of
50        IrqHandlerIntent x \<Rightarrow> Some x
51      | _ \<Rightarrow> None"
52
53definition
54  get_asid_pool_intent :: "cdl_intent \<Rightarrow> cdl_asid_pool_intent option"
55where
56  "get_asid_pool_intent intent \<equiv>
57    case intent of
58        AsidPoolIntent x \<Rightarrow> Some x
59      | _ \<Rightarrow> None"
60
61
62definition
63  get_asid_control_intent :: "cdl_intent \<Rightarrow> cdl_asid_control_intent option"
64where
65  "get_asid_control_intent intent \<equiv>
66    case intent of
67        AsidControlIntent x \<Rightarrow> Some x
68      | _ \<Rightarrow> None"
69
70definition
71  get_page_intent :: "cdl_intent \<Rightarrow> cdl_page_intent option"
72where
73  "get_page_intent intent \<equiv>
74    case intent of
75        PageIntent x \<Rightarrow> Some x
76      | _ \<Rightarrow> None"
77
78definition
79  get_page_table_intent :: "cdl_intent \<Rightarrow> cdl_page_table_intent option"
80where
81  "get_page_table_intent intent \<equiv>
82    case intent of
83        PageTableIntent x \<Rightarrow> Some x
84      | _ \<Rightarrow> None"
85
86definition
87  get_page_directory_intent :: "cdl_intent \<Rightarrow> cdl_page_directory_intent option"
88where
89  "get_page_directory_intent intent \<equiv>
90    case intent of
91        PageDirectoryIntent x \<Rightarrow> Some x
92      | _ \<Rightarrow> None"
93
94definition
95  get_untyped_intent :: "cdl_intent \<Rightarrow> cdl_untyped_intent option"
96where
97  "get_untyped_intent intent \<equiv>
98    case intent of
99        UntypedIntent x \<Rightarrow> Some x
100      | _ \<Rightarrow> None"
101
102definition
103  get_domain_intent :: "cdl_intent \<Rightarrow> cdl_domain_intent option"
104where
105  "get_domain_intent intent \<equiv>
106     case intent of
107         DomainIntent x \<Rightarrow> Some x
108       | _ \<Rightarrow> None"
109
110(*
111 * Decode and validate the given intent, turning it into an
112 * invocation.
113 *)
114definition
115  decode_invocation :: "cdl_cap \<Rightarrow> cdl_cap_ref \<Rightarrow> (cdl_cap \<times> cdl_cap_ref) list \<Rightarrow> cdl_intent \<Rightarrow> cdl_invocation except_monad"
116where
117  "decode_invocation invoked_cap invoked_cap_ref caps intent \<equiv>
118    case invoked_cap of
119       (* For endpoint-like caps, we always perform an operation,
120        * regardless of the user's actual intent. *)
121         EndpointCap o_id badge rights \<Rightarrow>
122           (if Write \<in> rights then
123             returnOk $ InvokeEndpoint (SyncMessage badge (Grant \<in> rights) o_id)
124           else
125             throw)
126       | NotificationCap o_id badge rights \<Rightarrow>
127           (if Write \<in> rights then
128             returnOk $ InvokeNotification (Signal badge o_id)
129           else
130             throw)
131       | ReplyCap o_id\<Rightarrow>
132           returnOk $ InvokeReply (ReplyMessage o_id invoked_cap_ref)
133
134       (*
135        * For other operations, we only perform the user's intent
136        * if it matches up with the cap.
137        *
138        * Note that this does not currently match the current
139        * implementation: instead, the user's message will be
140        * decoded into a new (undefined) intent for what the
141        * cap happened to be. I propose modifying labels used to
142        * avoid overlaps between different items so that we can
143        * recognise when the user is invoking the wrong item.
144        *)
145       | CNodeCap _ _ _ _ \<Rightarrow>
146           doE
147             cnode_intent \<leftarrow> throw_opt undefined $ get_cnode_intent intent;
148             liftME InvokeCNode $ decode_cnode_invocation invoked_cap invoked_cap_ref caps cnode_intent
149           odE
150       | TcbCap _ \<Rightarrow>
151           doE
152             tcb_intent \<leftarrow> throw_opt undefined $ get_tcb_intent intent;
153             liftME InvokeTcb $ decode_tcb_invocation invoked_cap invoked_cap_ref caps tcb_intent
154           odE
155       | IrqControlCap \<Rightarrow>
156           doE
157             irq_control_intent \<leftarrow> throw_opt undefined $ get_irq_control_intent intent;
158             liftME InvokeIrqControl $ decode_irq_control_invocation
159                 invoked_cap invoked_cap_ref caps irq_control_intent
160           odE
161       | IrqHandlerCap _ \<Rightarrow>
162           doE
163             irq_handler_intent \<leftarrow> throw_opt undefined $ get_irq_handler_intent intent;
164             liftME InvokeIrqHandler $ decode_irq_handler_invocation
165                 invoked_cap invoked_cap_ref caps irq_handler_intent
166           odE
167       | AsidPoolCap _ _\<Rightarrow>
168           doE
169             asid_pool_intent \<leftarrow> throw_opt undefined $ get_asid_pool_intent intent;
170             liftME InvokeAsidPool $ decode_asid_pool_invocation
171                 invoked_cap invoked_cap_ref caps asid_pool_intent
172           odE
173       | AsidControlCap \<Rightarrow>
174           doE
175             asid_control_intent \<leftarrow> throw_opt undefined $ get_asid_control_intent intent;
176             liftME InvokeAsidControl $ decode_asid_control_invocation
177                 invoked_cap invoked_cap_ref caps asid_control_intent
178           odE
179       | UntypedCap _ _ _ \<Rightarrow>
180           doE
181             untyped_intent \<leftarrow> throw_opt undefined $ get_untyped_intent intent;
182             liftME InvokeUntyped $ decode_untyped_invocation
183                 invoked_cap invoked_cap_ref caps untyped_intent
184           odE
185       | FrameCap _ _ _ _ _ _ \<Rightarrow>
186           doE
187             page_intent \<leftarrow> throw_opt undefined $ get_page_intent intent;
188             liftME InvokePage $ decode_page_invocation
189                 invoked_cap invoked_cap_ref caps page_intent
190           odE
191       | PageTableCap _ _ _ \<Rightarrow>
192           doE
193             page_table_intent \<leftarrow> throw_opt undefined $ get_page_table_intent intent;
194             liftME InvokePageTable $ decode_page_table_invocation
195                 invoked_cap invoked_cap_ref caps page_table_intent
196           odE
197       | PageDirectoryCap _ _ _ \<Rightarrow>
198          doE
199             page_directory_intent \<leftarrow> throw_opt undefined $ get_page_directory_intent intent;
200             liftME InvokePageDirectory $ decode_page_directory_invocation
201                 invoked_cap invoked_cap_ref caps page_directory_intent
202           odE
203       | DomainCap \<Rightarrow>
204          doE
205            domain_intent \<leftarrow> throw_opt undefined $ get_domain_intent intent;
206            liftME InvokeDomain $ decode_domain_invocation caps domain_intent
207          odE
208
209       (* Don't support operations on other types of caps. *)
210       | _ \<Rightarrow> throw"
211
212end
213