From efb4c61816c1e3edbbd1e0f01aa3687e65658b54 Mon Sep 17 00:00:00 2001 From: Joel Beeren Date: Thu, 14 Jan 2016 15:01:46 +1100 Subject: [PATCH] archirq: Remove redundant invocation, renamed arch_decode_interrupt_control. --- proof/crefine/Interrupt_C.thy | 36 +++++++++++------------ proof/drefine/Interrupt_DR.thy | 7 ++--- proof/drefine/StateTranslation_D.thy | 3 -- proof/drefine/Syscall_DR.thy | 6 ++-- proof/infoflow/Decode_IF.thy | 2 +- proof/invariant-abstract/EmptyFail_AI.thy | 4 +-- proof/invariant-abstract/Interrupt_AI.thy | 6 ++-- proof/refine/Interrupt_R.thy | 16 +++++----- proof/refine/Orphanage.thy | 2 +- proof/refine/PageTableDuplicates.thy | 6 ++-- proof/refine/Syscall_R.thy | 2 +- spec/abstract/ArchInvocation_A.thy | 2 +- spec/abstract/Arch_A.thy | 2 +- spec/abstract/Decode_A.thy | 11 +++---- spec/abstract/Interrupt_A.thy | 2 +- spec/abstract/Invocations_A.thy | 2 +- spec/capDL/Intents_D.thy | 2 +- spec/capDL/Interrupt_D.thy | 2 +- spec/design/ArchInterrupt_H.thy | 8 ++--- spec/design/ArchRetypeDecls_H.thy | 2 +- spec/design/Interrupt_H.thy | 8 ++--- spec/design/InvocationLabels_H.thy | 2 -- spec/design/Invocations_H.thy | 28 +++++++++--------- spec/design/skel/ArchInterrupt_H.thy | 2 +- spec/design/version | 4 +-- 25 files changed, 77 insertions(+), 90 deletions(-) diff --git a/proof/crefine/Interrupt_C.thy b/proof/crefine/Interrupt_C.thy index 2f0a0c9fe..b0df68d54 100644 --- a/proof/crefine/Interrupt_C.thy +++ b/proof/crefine/Interrupt_C.thy @@ -367,13 +367,13 @@ lemma Platform_maxIRQ: "Platform.maxIRQ = scast Kernel_C.maxIRQ" by (simp add: Platform.maxIRQ_def Kernel_C.maxIRQ_def) -lemma Arch_decodeInterruptControl_ccorres: +lemma Arch_decodeIRQControlInvocation_ccorres: "ccorres (intr_and_se_rel \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') \ UNIV [] - (decodeInterruptControl args extraCaps - >>= invocationCatch thread isBlocking isCall (InvokeIRQControl o InterruptControl)) - (Call Arch_decodeInterruptControl_'proc)" - apply (cinit' simp: decodeInterruptControl_def) + (ArchInterrupt_H.decodeIRQControlInvocation label args srcSlot extraCaps + >>= invocationCatch thread isBlocking isCall (InvokeIRQControl o ArchIRQControl)) + (Call Arch_decodeIRQControlInvocation_'proc)" + apply (cinit' simp: ArchInterrupt_H.decodeIRQControlInvocation_def) apply (simp add: throwError_bind invocationCatch_def cong: StateSpace.state.fold_congs globals.fold_congs) apply (rule syscall_error_throwError_ccorres_n) @@ -395,6 +395,10 @@ lemma maxIRQ_ucast_scast [simp]: "ucast (scast Kernel_C.maxIRQ :: word8) = scast Kernel_C.maxIRQ" by (clarsimp simp: Kernel_C.maxIRQ_def) +lemma decodeIRQ_arch_helper: "x \ invocation_label.IRQIssueIRQHandler \ + (case x of invocation_label.IRQIssueIRQHandler \ f | _ \ g) = g" + by (clarsimp split: invocation_label.splits) + lemma decodeIRQControlInvocation_ccorres: notes if_cong[cong] tl_drop_1[simp] shows @@ -524,19 +528,15 @@ lemma decodeIRQControlInvocation_ccorres: apply wp apply (simp add: Collect_const_mem all_ex_eq_helper) apply (vcg exspec=getSyscallArg_modifies) - apply (rule ccorres_Cond_rhs) - apply (simp add: liftME_invocationCatch) - apply (rule ccorres_add_returnOk) - apply (ctac add: Arch_decodeInterruptControl_ccorres) - apply (rule ccorres_return_CE, simp+)[1] - apply (rule ccorres_return_C_errorE, simp+)[1] - apply wp - apply vcg - apply (rule ccorres_equals_throwError) - apply (fastforce simp: throwError_bind invocationCatch_def - split: invocation_label.split) - apply (rule syscall_error_throwError_ccorres_n) - apply (simp add: syscall_error_to_H_cases) + apply (clarsimp simp: decodeIRQ_arch_helper) + apply (simp add: liftME_invocationCatch) + apply (rule ccorres_add_returnOk) + apply (ctac add: Arch_decodeIRQControlInvocation_ccorres) + apply (rule ccorres_return_CE, simp+)[1] + apply (rule ccorres_return_C_errorE, simp+)[1] + apply wp + apply vcg + apply (simp add: syscall_error_to_H_cases) apply (clarsimp simp: if_1_0_0 interpret_excaps_test_null excaps_map_def Collect_const_mem word_sless_def word_sle_def ThreadState_Restart_def unat_of_nat mask_def diff --git a/proof/drefine/Interrupt_DR.thy b/proof/drefine/Interrupt_DR.thy index 242e0c8dc..2c94a2a82 100644 --- a/proof/drefine/Interrupt_DR.thy +++ b/proof/drefine/Interrupt_DR.thy @@ -18,9 +18,8 @@ lemma decode_irq_control_error_corres: (throwError e) (Decode_A.decode_irq_control_invocation label args slot (map fst excaps))" apply (unfold decode_irq_control_invocation_def) - apply (cases "invocation_type label", simp_all) + apply (cases "invocation_type label"; simp add: arch_decode_irq_control_invocation_def) apply (simp add: transform_intent_def transform_intent_issue_irq_handler_def split: list.splits) - apply (simp add: transform_intent_def) done (* Interrupt Control Invocations *) @@ -91,9 +90,7 @@ lemma decode_irq_control_corres: apply wp apply (cases excaps', auto)[1] apply wp[1] - apply (cases "invocation_type label' = IRQInterruptControl") - apply (clarsimp simp: arch_decode_interrupt_control_def transform_intent_def) - apply clarsimp + apply (clarsimp simp: arch_decode_irq_control_invocation_def transform_intent_def) apply (rule corres_guard_imp) apply (cases ui) apply (auto simp: dcorres_alternative_throw) diff --git a/proof/drefine/StateTranslation_D.thy b/proof/drefine/StateTranslation_D.thy index 9547de81f..2f218cbbf 100644 --- a/proof/drefine/StateTranslation_D.thy +++ b/proof/drefine/StateTranslation_D.thy @@ -327,8 +327,6 @@ definition | IRQIssueIRQHandler \ map_option IrqControlIntent (transform_intent_issue_irq_handler args) - | IRQInterruptControl \ - Some (IrqControlIntent IrqControlInterruptControlIntent) | IRQAckIRQ \ Some (IrqHandlerIntent IrqHandlerAckIntent) | IRQSetIRQHandler \ Some (IrqHandlerIntent IrqHandlerSetEndpointIntent) | IRQClearIRQHandler \ Some (IrqHandlerIntent IrqHandlerClearIntent) @@ -396,7 +394,6 @@ lemma transform_tcb_intent_invocation: label \ CNodeRotate \ label \ CNodeSaveCaller \ label \ IRQIssueIRQHandler \ - label \ IRQInterruptControl \ label \ IRQAckIRQ \ label \ IRQSetIRQHandler \ label \ IRQClearIRQHandler \ diff --git a/proof/drefine/Syscall_DR.thy b/proof/drefine/Syscall_DR.thy index a16d3afc7..fc0be8c30 100644 --- a/proof/drefine/Syscall_DR.thy +++ b/proof/drefine/Syscall_DR.thy @@ -428,12 +428,12 @@ lemma transform_intent_irq_control_None: \ \op = s\ Decode_A.decode_invocation label args cap_i slot cap excaps \\r. \\, \\x. op = s\" apply (clarsimp simp:Decode_A.decode_invocation_def) apply wp - apply (clarsimp simp:decode_irq_control_invocation_def split del:if_splits) + apply (clarsimp simp:decode_irq_control_invocation_def arch_decode_irq_control_invocation_def split del:if_splits) apply (case_tac "invocation_type label") apply (clarsimp,wp)+ apply (clarsimp simp:transform_intent_issue_irq_handler_def transform_intent_def split:list.split_asm split del:if_splits,wp) - apply (clarsimp simp:arch_decode_interrupt_control_def,wp)+ -done + apply (clarsimp simp:arch_decode_irq_control_invocation_def,wp)+ + done lemma transform_intent_irq_handler_None: "\transform_intent (invocation_type label) args = None; cap = cap.IRQHandlerCap w\ diff --git a/proof/infoflow/Decode_IF.thy b/proof/infoflow/Decode_IF.thy index b33bf0762..489650a3c 100644 --- a/proof/infoflow/Decode_IF.thy +++ b/proof/infoflow/Decode_IF.thy @@ -277,7 +277,7 @@ lemma decode_irq_control_invocation_rev: apply (wp ensure_empty_rev lookup_slot_for_cnode_op_rev is_irq_active_rev whenE_inv | wp_once hoare_drop_imps - | simp add: Let_def arch_decode_interrupt_control_def)+ + | simp add: Let_def arch_decode_irq_control_invocation_def)+ apply safe apply simp+ apply(blast intro: aag_Control_into_owns_irq) diff --git a/proof/invariant-abstract/EmptyFail_AI.thy b/proof/invariant-abstract/EmptyFail_AI.thy index cfbc9af5d..f6d17f700 100644 --- a/proof/invariant-abstract/EmptyFail_AI.thy +++ b/proof/invariant-abstract/EmptyFail_AI.thy @@ -334,8 +334,8 @@ lemma arch_decode_ARMASIDPoolAssign_empty_fail: lemma arch_decode_invocation_empty_fail[wp]: "empty_fail (arch_decode_invocation label b c d e f)" apply (case_tac "invocation_type label") - prefer 44 - prefer 45 + prefer 43 + prefer 44 apply ((simp add: arch_decode_ARMASIDControlMakePool_empty_fail arch_decode_ARMASIDPoolAssign_empty_fail)+)[2] by ((simp add: arch_decode_invocation_def Let_def split: arch_cap.splits cap.splits option.splits | wp | intro conjI impI allI)+) diff --git a/proof/invariant-abstract/Interrupt_AI.thy b/proof/invariant-abstract/Interrupt_AI.thy index cca3b5b16..3dfadfbe9 100644 --- a/proof/invariant-abstract/Interrupt_AI.thy +++ b/proof/invariant-abstract/Interrupt_AI.thy @@ -37,7 +37,7 @@ where primrec irq_control_inv_valid :: "irq_control_invocation \ 'z::state_ext state \ bool" where - "irq_control_inv_valid (Invocations_A.InterruptControl ivk) = \" + "irq_control_inv_valid (Invocations_A.ArchIRQControl ivk) = \" | "irq_control_inv_valid (Invocations_A.IRQControl irq ptr ptr') = (cte_wp_at (op = cap.NullCap) ptr and cte_wp_at (op = cap.IRQControlCap) ptr' @@ -72,7 +72,7 @@ crunch inv[wp]: is_irq_active "P" lemma decode_irq_control_invocation_inv[wp]: "\P\ decode_irq_control_invocation label args slot caps \\rv. P\" apply (simp add: decode_irq_control_invocation_def Let_def - arch_decode_interrupt_control_def whenE_def, safe) + arch_decode_irq_control_invocation_def whenE_def, safe) apply (wp | simp)+ done @@ -85,7 +85,7 @@ lemma decode_irq_control_valid[wp]: \irq_control_inv_valid\,-" apply (simp add: decode_irq_control_invocation_def Let_def split_def lookup_target_slot_def whenE_def - arch_decode_interrupt_control_def + arch_decode_irq_control_invocation_def split del: split_if cong: if_cong) apply (rule hoare_pre) apply (wp ensure_empty_stronger | simp add: cte_wp_at_eq_simp diff --git a/proof/refine/Interrupt_R.thy b/proof/refine/Interrupt_R.thy index fd9f474cd..8b81ee5d1 100644 --- a/proof/refine/Interrupt_R.thy +++ b/proof/refine/Interrupt_R.thy @@ -26,15 +26,15 @@ where | "irq_handler_inv_relation (Invocations_A.SetMode irq trig pol) x = (x = SetMode irq trig pol)" consts - interrupt_control_relation :: "arch_interrupt_control \ interrupt_control \ bool" + interrupt_control_relation :: "arch_irq_control_invocation \ ArchRetypeDecls_H.irqcontrol_invocation \ bool" primrec irq_control_inv_relation :: "irq_control_invocation \ irqcontrol_invocation \ bool" where "irq_control_inv_relation (Invocations_A.IRQControl irq slot slot') x = (x = IssueIRQHandler irq (cte_map slot) (cte_map slot'))" -| "irq_control_inv_relation (Invocations_A.InterruptControl ivk) x - = (\ivk'. x = InterruptControl ivk' \ interrupt_control_relation ivk ivk')" +| "irq_control_inv_relation (Invocations_A.ArchIRQControl ivk) x + = (\ivk'. x = ArchIRQControl ivk' \ interrupt_control_relation ivk ivk')" primrec irq_handler_inv_valid' :: "irqhandler_invocation \ kernel_state \ bool" @@ -52,7 +52,7 @@ where primrec irq_control_inv_valid' :: "irqcontrol_invocation \ kernel_state \ bool" where - "irq_control_inv_valid' (InterruptControl ivk) = \" + "irq_control_inv_valid' (ArchIRQControl ivk) = \" | "irq_control_inv_valid' (IssueIRQHandler irq ptr ptr') = (cte_wp_at' (\cte. cteCap cte = NullCap) ptr and cte_wp_at' (\cte. cteCap cte = IRQControlCap) ptr' and @@ -136,7 +136,7 @@ lemma decode_irq_control_corres: (decode_irq_control_invocation label args slot caps) (decodeIRQControlInvocation label args (cte_map slot) caps')" apply (clarsimp simp: decode_irq_control_invocation_def decodeIRQControlInvocation_def - decodeInterruptControl_def arch_decode_interrupt_control_def + ArchInterrupt_H.decodeIRQControlInvocation_def arch_decode_irq_control_invocation_def split del: split_if cong: if_cong split: invocation_label.split) apply (cases caps, simp split: list.split) @@ -165,7 +165,7 @@ lemma decode_irq_control_corres: done crunch inv[wp]: decodeIRQControlInvocation "P" - (simp: crunch_simps decodeInterruptControl_def) + (simp: crunch_simps ArchInterrupt_H.decodeIRQControlInvocation_def) (* Levity: added (20090201 10:50:27) *) declare ensureEmptySlot_stronger [wp] @@ -197,7 +197,7 @@ lemma decode_irq_control_valid'[wp]: apply (rule hoare_pre) apply (wp ensureEmptySlot_stronger isIRQActive_wp whenE_throwError_wp - | simp add: decodeInterruptControl_def | wpc + | simp add: ArchInterrupt_H.decodeIRQControlInvocation_def | wpc | wp_once hoare_drop_imps)+ apply (clarsimp simp: minIRQ_def maxIRQ_def toEnum_of_nat word_le_nat_alt unat_of_nat) @@ -348,7 +348,7 @@ lemma invoke_irq_control_corres: apply (case_tac ctea) apply (clarsimp simp: isCap_simps sameRegionAs_def3) apply (auto dest: valid_irq_handlers_ctes_ofD)[1] - apply (clarsimp simp: arch_invoke_irq_control_def invokeInterruptControl_def) + apply (clarsimp simp: arch_invoke_irq_control_def ArchInterrupt_H.invokeIRQControl_def) done crunch valid_cap'[wp]: setIRQState "valid_cap' cap" diff --git a/proof/refine/Orphanage.thy b/proof/refine/Orphanage.thy index ceb554db8..e1f032307 100644 --- a/proof/refine/Orphanage.thy +++ b/proof/refine/Orphanage.thy @@ -1968,7 +1968,7 @@ lemma invokeIRQControl_no_orphans [wp]: "\ \s. no_orphans s \ invokeIRQControl i \ \rv s. no_orphans s \" - apply (cases i, simp_all add: invokeIRQControl_def invokeInterruptControl_def) + apply (cases i, simp_all add: invokeIRQControl_def ArchInterrupt_H.invokeIRQControl_def) apply (wp | clarsimp)+ done diff --git a/proof/refine/PageTableDuplicates.thy b/proof/refine/PageTableDuplicates.thy index 6f78c3b29..ef87ba50e 100644 --- a/proof/refine/PageTableDuplicates.thy +++ b/proof/refine/PageTableDuplicates.thy @@ -2041,9 +2041,9 @@ crunch valid_duplicates'[wp]: lemma invokeIRQControl_valid_duplicates'[wp]: "\\s. vs_valid_duplicates' (ksPSpace s) \ invokeIRQControl a \\_ s. vs_valid_duplicates' (ksPSpace s)\" - apply (simp add:invokeIRQControl_def invokeInterruptControl_def) + apply (simp add:invokeIRQControl_def ArchInterrupt_H.invokeIRQControl_def) apply (rule hoare_pre) - apply (wp|wpc | simp add:invokeInterruptControl_def)+ + apply (wp|wpc | simp add:ArchInterrupt_H.invokeIRQControl_def)+ apply fastforce done @@ -2052,7 +2052,7 @@ lemma invokeIRQHandler_valid_duplicates'[wp]: \\_ s. vs_valid_duplicates' (ksPSpace s)\" apply (simp add:invokeIRQHandler_def) apply (rule hoare_pre) - apply (wp|wpc | simp add:invokeInterruptControl_def)+ + apply (wp|wpc | simp add: ArchInterrupt_H.invokeIRQControl_def)+ done lemma invokeCNode_valid_duplicates'[wp]: diff --git a/proof/refine/Syscall_R.thy b/proof/refine/Syscall_R.thy index e07aa04a3..234b6d264 100644 --- a/proof/refine/Syscall_R.thy +++ b/proof/refine/Syscall_R.thy @@ -2397,7 +2397,7 @@ lemma inv_irq_IRQInactive: -, \\rv s. intStateIRQTable (ksInterruptState s) rv \ irqstate.IRQInactive\" apply (simp add: invokeIRQControl_def) apply (rule hoare_pre) - apply (wpc|wp|simp add: invokeInterruptControl_def)+ + apply (wpc|wp|simp add: ArchInterrupt_H.invokeIRQControl_def)+ done lemma inv_arch_IRQInactive: diff --git a/spec/abstract/ArchInvocation_A.thy b/spec/abstract/ArchInvocation_A.thy index b05f3bdd9..3feb78776 100644 --- a/spec/abstract/ArchInvocation_A.thy +++ b/spec/abstract/ArchInvocation_A.thy @@ -70,6 +70,6 @@ datatype arch_invocation | InvokeASIDPool asid_pool_invocation -- "There are no additional interrupt control operations on ARM." -typedecl arch_interrupt_control +typedecl arch_irq_control_invocation end diff --git a/spec/abstract/Arch_A.thy b/spec/abstract/Arch_A.thy index d05f40aa5..124a2a1cf 100644 --- a/spec/abstract/Arch_A.thy +++ b/spec/abstract/Arch_A.thy @@ -23,7 +23,7 @@ definition "page_bits \ pageBits" text {* The ARM architecture does not provide any additional operations on its interrupt controller. *} definition - arch_invoke_irq_control :: "arch_interrupt_control \ (unit,'z::state_ext) p_monad" where + arch_invoke_irq_control :: "arch_irq_control_invocation \ (unit,'z::state_ext) p_monad" where "arch_invoke_irq_control aic \ fail" text {* Switch to a thread's virtual address space context and write its IPC diff --git a/spec/abstract/Decode_A.thy b/spec/abstract/Decode_A.thy index 065ea37bc..450a98e2c 100644 --- a/spec/abstract/Decode_A.thy +++ b/spec/abstract/Decode_A.thy @@ -279,9 +279,9 @@ where text "ARM does not support additional interrupt control operations" definition - arch_decode_interrupt_control :: - "data list \ cap list \ (arch_interrupt_control,'z::state_ext) se_monad" where - "arch_decode_interrupt_control d cs \ throwError IllegalOperation" + arch_decode_irq_control_invocation :: + "data \ data list \ cslot_ptr \ cap list \ (arch_irq_control_invocation,'z::state_ext) se_monad" where + "arch_decode_irq_control_invocation label args slot excaps \ throwError IllegalOperation" section "CNode" @@ -645,10 +645,7 @@ definition returnOk $ IRQControl irqv dest_slot src_slot odE else throwError TruncatedMessage - else if invocation_type label = IRQInterruptControl - then liftME InterruptControl - $ arch_decode_interrupt_control args cps - else throwError IllegalOperation)" + else liftME ArchIRQControl $ arch_decode_irq_control_invocation label args src_slot cps)" definition data_to_bool :: "data \ bool" diff --git a/spec/abstract/Interrupt_A.thy b/spec/abstract/Interrupt_A.thy index 794cfc9b3..0cd1ac082 100644 --- a/spec/abstract/Interrupt_A.thy +++ b/spec/abstract/Interrupt_A.thy @@ -32,7 +32,7 @@ where "invoke_irq_control (IRQControl irq handler_slot control_slot) = liftE (do set_irq_state IRQSignal irq; cap_insert (IRQHandlerCap irq) control_slot handler_slot od)" -| "invoke_irq_control (InterruptControl invok) = +| "invoke_irq_control (ArchIRQControl invok) = arch_invoke_irq_control invok" text {* The IRQHandler capability may be used to configure how interrupts on an diff --git a/spec/abstract/Invocations_A.thy b/spec/abstract/Invocations_A.thy index cb2ce3c65..e81a5f284 100644 --- a/spec/abstract/Invocations_A.thy +++ b/spec/abstract/Invocations_A.thy @@ -49,7 +49,7 @@ datatype tcb_invocation = datatype irq_control_invocation = IRQControl irq cslot_ptr cslot_ptr - | InterruptControl arch_interrupt_control + | ArchIRQControl arch_irq_control_invocation datatype irq_handler_invocation = ACKIrq irq diff --git a/spec/capDL/Intents_D.thy b/spec/capDL/Intents_D.thy index c381e5a0e..c97edd127 100644 --- a/spec/capDL/Intents_D.thy +++ b/spec/capDL/Intents_D.thy @@ -134,7 +134,7 @@ datatype cdl_irq_control_intent = (* IssueIrqHandler: (target), irq, (root), index, depth *) IrqControlIssueIrqHandlerIntent word8 word32 word32 (* InterruptControl *) - | IrqControlInterruptControlIntent + | IrqControlArchIrqControlIntent datatype cdl_page_table_intent = (* Map: (target), (pd), vaddr, attr *) diff --git a/spec/capDL/Interrupt_D.thy b/spec/capDL/Interrupt_D.thy index 345abc87b..6a6165a8c 100644 --- a/spec/capDL/Interrupt_D.thy +++ b/spec/capDL/Interrupt_D.thy @@ -47,7 +47,7 @@ where dest_slot_cap_ref \ lookup_slot_for_cnode_op cnode_cap index (unat depth); returnOk $ IssueIrqHandler irq target_ref dest_slot_cap_ref odE \ throw - | IrqControlInterruptControlIntent \ throw + | IrqControlArchIrqControlIntent \ throw " definition diff --git a/spec/design/ArchInterrupt_H.thy b/spec/design/ArchInterrupt_H.thy index 87492a5a4..b5b32a565 100644 --- a/spec/design/ArchInterrupt_H.thy +++ b/spec/design/ArchInterrupt_H.thy @@ -13,14 +13,14 @@ imports RetypeDecls_H begin definition -decodeInterruptControl :: "machine_word list \ capability list \ ( syscall_error , interrupt_control ) kernel_f" +decodeIRQControlInvocation :: "machine_word \ machine_word list \ machine_word \ capability list \ ( syscall_error , ArchRetypeDecls_H.irqcontrol_invocation ) kernel_f" where -"decodeInterruptControl arg1 arg2 \ throw IllegalOperation" +"decodeIRQControlInvocation arg1 arg2 arg3 arg4 \ throw IllegalOperation" definition -invokeInterruptControl :: "interrupt_control \ unit kernel_p" +invokeIRQControl :: "ArchRetypeDecls_H.irqcontrol_invocation \ unit kernel_p" where -"invokeInterruptControl arg1 \ haskell_fail []" +"invokeIRQControl arg1 \ haskell_fail []" end diff --git a/spec/design/ArchRetypeDecls_H.thy b/spec/design/ArchRetypeDecls_H.thy index 5a9af68e0..dc914c9a1 100644 --- a/spec/design/ArchRetypeDecls_H.thy +++ b/spec/design/ArchRetypeDecls_H.thy @@ -606,7 +606,7 @@ datatype invocation = | InvokeASIDControl asidcontrol_invocation | InvokeASIDPool asidpool_invocation -typedecl interrupt_control +typedecl irqcontrol_invocation datatype copy_register_sets = ARMNoExtraRegisters diff --git a/spec/design/Interrupt_H.thy b/spec/design/Interrupt_H.thy index 9e2ffbc49..19d487eba 100644 --- a/spec/design/Interrupt_H.thy +++ b/spec/design/Interrupt_H.thy @@ -68,9 +68,7 @@ defs decodeIRQControlInvocation_def: returnOk $ IssueIRQHandler irq destSlot srcSlot odE) | (IRQIssueIRQHandler,_,_) \ throw TruncatedMessage - | (IRQInterruptControl,_,_) \ liftME InterruptControl $ - ArchInterrupt_H.decodeInterruptControl args extraCaps - | _ \ throw IllegalOperation + | _ \ liftME ArchIRQControl $ ArchInterrupt_H.decodeIRQControlInvocation label args srcSlot extraCaps )" defs invokeIRQControl_def: @@ -80,8 +78,8 @@ defs invokeIRQControl_def: setIRQState (IRQSignal) irq; cteInsert (IRQHandlerCap irq) controlSlot handlerSlot od) - | (InterruptControl invok) \ - ArchInterrupt_H.invokeInterruptControl invok + | (ArchIRQControl invok) \ + ArchInterrupt_H.invokeIRQControl invok )" defs decodeIRQHandlerInvocation_def: diff --git a/spec/design/InvocationLabels_H.thy b/spec/design/InvocationLabels_H.thy index 318206817..7b3edbb22 100644 --- a/spec/design/InvocationLabels_H.thy +++ b/spec/design/InvocationLabels_H.thy @@ -42,7 +42,6 @@ datatype invocation_label = | CNodeRotate | CNodeSaveCaller | IRQIssueIRQHandler - | IRQInterruptControl | IRQAckIRQ | IRQSetIRQHandler | IRQClearIRQHandler @@ -116,7 +115,6 @@ definition CNodeRotate, CNodeSaveCaller, IRQIssueIRQHandler, - IRQInterruptControl, IRQAckIRQ, IRQSetIRQHandler, IRQClearIRQHandler, diff --git a/spec/design/Invocations_H.thy b/spec/design/Invocations_H.thy index a17f1b88e..511adc050 100644 --- a/spec/design/Invocations_H.thy +++ b/spec/design/Invocations_H.thy @@ -760,14 +760,9 @@ lemma retypeNewSizeBits_retypeNewSizeBits_update [simp]: by (cases v) simp datatype irqcontrol_invocation = - InterruptControl ArchRetypeDecls_H.interrupt_control + ArchIRQControl ArchRetypeDecls_H.irqcontrol_invocation | IssueIRQHandler irq machine_word machine_word -primrec - interruptControlArch :: "irqcontrol_invocation \ ArchRetypeDecls_H.interrupt_control" -where - "interruptControlArch (InterruptControl v0) = v0" - primrec issueHandlerSlot :: "irqcontrol_invocation \ machine_word" where @@ -784,9 +779,9 @@ where "issueHandlerControllerSlot (IssueIRQHandler v0 v1 v2) = v2" primrec - interruptControlArch_update :: "(ArchRetypeDecls_H.interrupt_control \ ArchRetypeDecls_H.interrupt_control) \ irqcontrol_invocation \ irqcontrol_invocation" + archIRQControl :: "irqcontrol_invocation \ ArchRetypeDecls_H.irqcontrol_invocation" where - "interruptControlArch_update f (InterruptControl v0) = InterruptControl (f v0)" + "archIRQControl (ArchIRQControl v0) = v0" primrec issueHandlerSlot_update :: "(machine_word \ machine_word) \ irqcontrol_invocation \ irqcontrol_invocation" @@ -803,10 +798,15 @@ primrec where "issueHandlerControllerSlot_update f (IssueIRQHandler v0 v1 v2) = IssueIRQHandler v0 v1 (f v2)" -abbreviation (input) - InterruptControl_trans :: "(ArchRetypeDecls_H.interrupt_control) \ irqcontrol_invocation" ("InterruptControl'_ \ interruptControlArch= _ \") +primrec + archIRQControl_update :: "(ArchRetypeDecls_H.irqcontrol_invocation \ ArchRetypeDecls_H.irqcontrol_invocation) \ irqcontrol_invocation \ irqcontrol_invocation" where - "InterruptControl_ \ interruptControlArch= v0 \ == InterruptControl v0" + "archIRQControl_update f (ArchIRQControl v0) = ArchIRQControl (f v0)" + +abbreviation (input) + ArchIRQControl_trans :: "(ArchRetypeDecls_H.irqcontrol_invocation) \ irqcontrol_invocation" ("ArchIRQControl'_ \ archIRQControl= _ \") +where + "ArchIRQControl_ \ archIRQControl= v0 \ == ArchIRQControl v0" abbreviation (input) IssueIRQHandler_trans :: "(irq) \ (machine_word) \ (machine_word) \ irqcontrol_invocation" ("IssueIRQHandler'_ \ issueHandlerIRQ= _, issueHandlerSlot= _, issueHandlerControllerSlot= _ \") @@ -814,10 +814,10 @@ where "IssueIRQHandler_ \ issueHandlerIRQ= v0, issueHandlerSlot= v1, issueHandlerControllerSlot= v2 \ == IssueIRQHandler v0 v1 v2" definition - isInterruptControl :: "irqcontrol_invocation \ bool" + isArchIRQControl :: "irqcontrol_invocation \ bool" where - "isInterruptControl v \ case v of - InterruptControl v0 \ True + "isArchIRQControl v \ case v of + ArchIRQControl v0 \ True | _ \ False" definition diff --git a/spec/design/skel/ArchInterrupt_H.thy b/spec/design/skel/ArchInterrupt_H.thy index 8ac3f0d55..6d9e66e16 100644 --- a/spec/design/skel/ArchInterrupt_H.thy +++ b/spec/design/skel/ArchInterrupt_H.thy @@ -12,6 +12,6 @@ theory ArchInterrupt_H imports RetypeDecls_H begin -#INCLUDE_HASKELL SEL4/Object/Interrupt/ARM.lhs +#INCLUDE_HASKELL SEL4/Object/Interrupt/ARM.lhs ArchInv=ArchRetypeDecls_H end diff --git a/spec/design/version b/spec/design/version index 45c1c99e6..4a20d1ceb 100644 --- a/spec/design/version +++ b/spec/design/version @@ -1,5 +1,5 @@ -Built from git repo at /home/tsewell/dev/verification/seL4/haskell by tsewell +Built from git repo at /net/nfshome/export/home/insecure/jbeeren/work/test/seL4/haskell by jbeeren Generated from changeset: -f7b60e9 Final patch to lookupSlot variants. +d59b73d Remove redundant IRQInterruptControl invocation, and replace with a mechanism to actually decode arch specific IRQ invocations