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 11(* 12 * Operations on interrupt objects. 13 *) 14 15theory Interrupt_D 16imports Endpoint_D "ExecSpec.Platform" 17begin 18 19context begin interpretation Arch . 20requalify_types 21 irq 22 23requalify_consts 24 maxIRQ 25end 26 27(* Return the currently pending IRQ. *) 28definition 29 get_active_irq :: "(cdl_irq option) k_monad" 30where 31 "get_active_irq \<equiv> 32 do 33 irq \<leftarrow> select UNIV; 34 return $ Some irq 35 od \<sqinter> (return None) 36 " 37 38definition 39 arch_decode_irq_control_invocation :: "cdl_cap \<Rightarrow> cdl_cap_ref \<Rightarrow> (cdl_cap \<times> cdl_cap_ref) list \<Rightarrow> 40 cdl_arch_irq_control_intent \<Rightarrow> cdl_irq_control_invocation except_monad" 41where 42 "arch_decode_irq_control_invocation target target_ref caps intent \<equiv> case intent of 43 ARMIrqControlIssueIrqHandlerIntent irq index depth \<Rightarrow> 44 doE 45 root \<leftarrow> throw_on_none $ get_index caps 0; 46 cnode_cap \<leftarrow> returnOk $ fst root; 47 dest_slot_cap_ref \<leftarrow> lookup_slot_for_cnode_op cnode_cap index (unat depth); 48 returnOk $ IssueIrqHandler irq target_ref dest_slot_cap_ref 49 odE \<sqinter> throw" 50 51definition 52 decode_irq_control_invocation :: "cdl_cap \<Rightarrow> cdl_cap_ref \<Rightarrow> (cdl_cap \<times> cdl_cap_ref) list \<Rightarrow> 53 cdl_irq_control_intent \<Rightarrow> cdl_irq_control_invocation except_monad" 54where 55 "decode_irq_control_invocation target target_ref caps intent \<equiv> case intent of 56 (* Create an IRQ handler cap for the given IRQ, placing it 57 * in the specified CNode slot. *) 58 IrqControlIssueIrqHandlerIntent irq index depth \<Rightarrow> 59 doE 60 root \<leftarrow> throw_on_none $ get_index caps 0; 61 cnode_cap \<leftarrow> returnOk $ fst root; 62 dest_slot_cap_ref \<leftarrow> lookup_slot_for_cnode_op cnode_cap index (unat depth); 63 returnOk $ IssueIrqHandler irq target_ref dest_slot_cap_ref 64 odE \<sqinter> throw 65 | ArchIrqControlIssueIrqHandlerIntent arch_intent \<Rightarrow> arch_decode_irq_control_invocation target target_ref caps arch_intent" 66 67definition 68 decode_irq_handler_invocation :: "cdl_cap \<Rightarrow> cdl_cap_ref \<Rightarrow> (cdl_cap \<times> cdl_cap_ref) list \<Rightarrow> 69 cdl_irq_handler_intent \<Rightarrow> cdl_irq_handler_invocation except_monad" 70where 71 "decode_irq_handler_invocation target target_ref caps intent \<equiv> case intent of 72 (* Acknowledge an IRQ. *) 73 IrqHandlerAckIntent \<Rightarrow> 74 doE 75 irq \<leftarrow> liftE $ assert_opt $ cdl_cap_irq target; 76 returnOk $ AckIrq irq 77 odE \<sqinter> throw 78 79 (* Modify the IRQ so that it no longer sends to an endpoint. *) 80 | IrqHandlerClearIntent \<Rightarrow> 81 doE 82 irq \<leftarrow> liftE $ assert_opt $ cdl_cap_irq target; 83 returnOk $ ClearIrqHandler irq 84 odE \<sqinter> throw 85 86 (* Setup an IRQ to cause an endpoint to be sent to. *) 87 | IrqHandlerSetEndpointIntent \<Rightarrow> 88 doE 89 endpoint \<leftarrow> throw_on_none $ get_index caps 0; 90 endpoint_cap \<leftarrow> returnOk $ fst endpoint; 91 endpoint_cap_ref \<leftarrow> returnOk $ snd endpoint; 92 irq \<leftarrow> liftE $ assert_opt $ cdl_cap_irq target; 93 case endpoint_cap of 94 NotificationCap x _ _ \<Rightarrow> returnOk () 95 | _ \<Rightarrow> throw; 96 returnOk $ SetIrqHandler irq endpoint_cap endpoint_cap_ref 97 odE \<sqinter> throw 98 " 99 100definition 101 arch_invoke_irq_control :: "arch_cdl_irq_control_invocation \<Rightarrow> unit k_monad" 102where 103 "arch_invoke_irq_control params \<equiv> case params of 104 (* Create a new IRQ handler cap. *) 105 ARMIssueIrqHandler irq control_slot dest_slot trigger \<Rightarrow> 106 insert_cap_child (IrqHandlerCap irq) control_slot dest_slot 107 " 108 109definition 110 invoke_irq_control :: "cdl_irq_control_invocation \<Rightarrow> unit k_monad" 111where 112 "invoke_irq_control params \<equiv> case params of 113 (* Create a new IRQ handler cap. *) 114 IssueIrqHandler irq control_slot dest_slot \<Rightarrow> 115 insert_cap_child (IrqHandlerCap irq) control_slot dest_slot 116 | ArchIssueIrqHandler arch_inv \<Rightarrow> 117 arch_invoke_irq_control arch_inv" 118 119definition 120 invoke_irq_handler :: "cdl_irq_handler_invocation \<Rightarrow> unit k_monad" 121where 122 "invoke_irq_handler params \<equiv> case params of 123 (* Acknowledge and unmask an IRQ. *) 124 AckIrq irq \<Rightarrow> return () 125 126 (* Attach an IRQ handler to write to an endpoint. *) 127 | SetIrqHandler irq cap slot \<Rightarrow> 128 do 129 irqslot \<leftarrow> gets (get_irq_slot irq); 130 delete_cap_simple irqslot; 131 insert_cap_child cap slot irqslot \<sqinter> insert_cap_sibling cap slot irqslot 132 od 133 134 (* Deassociate this handler with all endpoints. *) 135 | ClearIrqHandler irq \<Rightarrow> 136 do 137 irqslot \<leftarrow> gets (get_irq_slot irq); 138 delete_cap_simple irqslot 139 od 140 " 141 142(* Handle an interrupt. *) 143definition 144 handle_interrupt :: "cdl_irq \<Rightarrow> unit k_monad" 145where 146 "handle_interrupt irq \<equiv> if (irq > maxIRQ) then return () else 147 do 148 irq_slot \<leftarrow> gets $ get_irq_slot irq; 149 c \<leftarrow> gets $ opt_cap irq_slot; 150 case c of 151 None \<Rightarrow> return () 152 | Some cap \<Rightarrow> ( 153 case cap of 154 (NotificationCap obj _ rights) \<Rightarrow> 155 if (Write \<in> rights) then send_signal obj else return () 156 | _ \<Rightarrow> return () 157 ) 158 od 159 " 160 161definition 162 handle_pending_interrupts :: "unit k_monad" 163where 164 "handle_pending_interrupts \<equiv> 165 do 166 active \<leftarrow> get_active_irq; 167 case active of 168 Some irq \<Rightarrow> handle_interrupt irq 169 | None \<Rightarrow> return () 170 od" 171 172end 173