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