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