From 77a657004d230edec70b0c0756fc6ce7f518bd08 Mon Sep 17 00:00:00 2001 From: Joel Beeren Date: Tue, 17 Jan 2017 14:04:55 +1100 Subject: [PATCH] x64: Interrupt_AI, ArchInterrupt_AI done --- proof/invariant-abstract/Interrupt_AI.thy | 11 ++- .../X64/ArchInterrupt_AI.thy | 89 +++++++++++++++++-- spec/abstract/X64/Arch_A.thy | 4 +- spec/machine/X64/MachineOps.thy | 4 +- 4 files changed, 91 insertions(+), 17 deletions(-) diff --git a/proof/invariant-abstract/Interrupt_AI.thy b/proof/invariant-abstract/Interrupt_AI.thy index 97a0922fb..ae27b7fed 100644 --- a/proof/invariant-abstract/Interrupt_AI.thy +++ b/proof/invariant-abstract/Interrupt_AI.thy @@ -39,18 +39,21 @@ where \ cte_wp_at (interrupt_derived cap) cte_ptr s \ s \ cap \ is_ntfn_cap cap)" +consts + arch_irq_control_inv_valid :: "arch_irq_control_invocation \ ('a :: state_ext) state \ bool" primrec - irq_control_inv_valid :: "irq_control_invocation \ 'z::state_ext state \ bool" + irq_control_inv_valid :: "irq_control_invocation \ 'a::state_ext state \ bool" where - "irq_control_inv_valid (Invocations_A.ArchIRQControl ivk) = \" + "irq_control_inv_valid (Invocations_A.ArchIRQControl ivk) = (arch_irq_control_inv_valid 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' and ex_cte_cap_wp_to is_cnode_cap ptr and real_cte_at ptr and K (irq \ maxIRQ))" -locale Interrupt_AI = + +locale Interrupt_AI = fixes state_ext_type1 :: "('a :: state_ext) itself" assumes decode_irq_control_invocation_inv[wp]: "\(P :: 'a state \ bool) args slot label caps. @@ -108,7 +111,7 @@ locale Interrupt_AI = "\ f irq. empty_fail (maskInterrupt f irq)" assumes handle_interrupt_invs [wp]: "\ irq. \invs :: 'a state \ bool\ handle_interrupt irq \\_. invs\" - + crunch inv[wp]: decode_irq_handler_invocation "P" (simp: crunch_simps) diff --git a/proof/invariant-abstract/X64/ArchInterrupt_AI.thy b/proof/invariant-abstract/X64/ArchInterrupt_AI.thy index 951d48721..134b2de22 100644 --- a/proof/invariant-abstract/X64/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/X64/ArchInterrupt_AI.thy @@ -12,7 +12,29 @@ theory ArchInterrupt_AI imports "../Interrupt_AI" begin -context Arch begin +context Arch begin global_naming X64 + +thm irq_control_inv_valid.simps arch_decode_irq_control_invocation_def +primrec arch_irq_control_inv_valid_real :: "arch_irq_control_invocation \ 'a::state_ext state \ bool" +where + "arch_irq_control_inv_valid_real (IssueIRQHandlerIOAPIC irq dest_slot src_slot + ioapic pin level polarity vector) = + (cte_wp_at (op = NullCap) dest_slot and + cte_wp_at (op = IRQControlCap) src_slot and + ex_cte_cap_wp_to is_cnode_cap dest_slot and + real_cte_at dest_slot and + K (irq \ maxIRQ \ ioapic < numIOAPICs \ + pin < ioapicIRQLines \ level < 2 \ + polarity < 2))" +| "arch_irq_control_inv_valid_real (IssueIRQHandlerMSI irq dest_slot src_slot bus dev func handle) + = (cte_wp_at (op = NullCap) dest_slot and + cte_wp_at (op = IRQControlCap) src_slot and + ex_cte_cap_wp_to is_cnode_cap dest_slot and + real_cte_at dest_slot and + K (irq \ maxIRQ \ bus \ maxPCIBus \ dev \ maxPCIDev \ func \ maxPCIFunc))" + +defs arch_irq_control_inv_valid_def: + "arch_irq_control_inv_valid \ arch_irq_control_inv_valid_real" named_theorems Interrupt_AI_asms @@ -23,6 +45,40 @@ lemma (* decode_irq_control_invocation_inv *)[Interrupt_AI_asms]: apply (rule hoare_pre) apply (wp | simp split del: split_if)+ done + +lemma irq_control_inv_valid_ArchIRQControl[simp]: + "irq_control_inv_valid \ ArchIRQControl = arch_irq_control_inv_valid" + by auto + +context begin + +private method cap_hammer = (((drule_tac x="caps ! 0" in bspec)+, (rule nth_mem, fastforce)+), + solves \(clarsimp simp: cte_wp_at_eq_simp)\) + +private method word_hammer = solves \(clarsimp simp: not_less maxIRQ_def numIOAPICs_def ioapicIRQLines_def + maxPCIDev_def maxPCIBus_def maxPCIFunc_def, + (word_bitwise, auto?)?)[1]\ + + +lemma arch_decode_irq_control_valid[wp]: + "\\s. invs s \ (\cap \ set caps. s \ cap) + \ (\cap \ set caps. is_cnode_cap cap \ + (\r \ cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) + \ cte_wp_at (op = cap.IRQControlCap) slot s\ + arch_decode_irq_control_invocation label args slot caps + \arch_irq_control_inv_valid\,-" + apply (simp add: arch_decode_irq_control_invocation_def Let_def whenE_def + arch_irq_control_inv_valid_def + split del: split_if + cong: if_cong) + apply (rule hoare_pre) + apply (wp ensure_empty_stronger hoare_vcg_const_imp_lift_R hoare_vcg_const_imp_lift + | simp add: cte_wp_at_eq_simp split del: split_if + | wpc | wp_once hoare_drop_imps)+ + apply clarsimp + by (safe; (cap_hammer | word_hammer)) + +end lemma (* decode_irq_control_valid *)[Interrupt_AI_asms]: "\\s. invs s \ (\cap \ set caps. s \ cap) @@ -32,8 +88,7 @@ lemma (* decode_irq_control_valid *)[Interrupt_AI_asms]: decode_irq_control_invocation label args slot caps \irq_control_inv_valid\,-" apply (simp add: decode_irq_control_invocation_def Let_def split_def - whenE_def arch_check_irq_def - arch_decode_irq_control_invocation_def + whenE_def arch_check_irq_def split del: split_if cong: if_cong) apply (rule hoare_pre) apply (wp ensure_empty_stronger | simp add: cte_wp_at_eq_simp @@ -150,6 +205,18 @@ lemma invoke_irq_handler_invs'[Interrupt_AI_asms]: done qed +lemma arch_invoke_irq_control_invs[wp]: + "\invs and arch_irq_control_inv_valid i\ arch_invoke_irq_control i \\rv. invs\" + apply (simp add: arch_invoke_irq_control_def) + apply (rule hoare_pre) + apply (wp cap_insert_simple_invs | wpc + | simp add: IRQHandler_valid is_cap_simps no_cap_to_obj_with_diff_IRQHandler_ARCH + | strengthen real_cte_tcb_valid)+ + by (auto simp: cte_wp_at_caps_of_state IRQ_def arch_irq_control_inv_valid_def + is_simple_cap_def is_cap_simps is_pt_cap_def + safe_parent_for_def + ex_cte_cap_to_cnode_always_appropriate_strg) + lemma (* invoke_irq_control_invs *) [Interrupt_AI_asms]: "\invs and irq_control_inv_valid i\ invoke_irq_control i \\rv. invs\" apply (cases i, simp_all) @@ -157,12 +224,14 @@ lemma (* invoke_irq_control_invs *) [Interrupt_AI_asms]: apply (wp cap_insert_simple_invs | simp add: IRQHandler_valid is_cap_simps no_cap_to_obj_with_diff_IRQHandler_ARCH | strengthen real_cte_tcb_valid)+ - apply (clarsimp simp: cte_wp_at_caps_of_state - is_simple_cap_def is_cap_simps is_pt_cap_def - safe_parent_for_def - ex_cte_cap_to_cnode_always_appropriate_strg) - done + apply (clarsimp simp: cte_wp_at_caps_of_state + is_simple_cap_def is_cap_simps is_pt_cap_def + safe_parent_for_def + ex_cte_cap_to_cnode_always_appropriate_strg) + by wp +crunch device_state_inv[wp]: resetTimer "\ms. P (device_state ms)" + lemma resetTimer_invs_ARCH[Interrupt_AI_asms]: "\invs\ do_machine_op resetTimer \\_. invs\" apply (wp dmo_invs) @@ -200,7 +269,9 @@ lemma (* handle_interrupt_invs *) [Interrupt_AI_asms]: end -interpretation Interrupt_AI?: Interrupt_AI + + +interpretation Interrupt_AI?: Interrupt_AI proof goal_cases interpret Arch . case 1 show ?case by (intro_locales; (unfold_locales, simp_all add: Interrupt_AI_asms)?) diff --git a/spec/abstract/X64/Arch_A.thy b/spec/abstract/X64/Arch_A.thy index 0fff89754..7a959b6ba 100644 --- a/spec/abstract/X64/Arch_A.thy +++ b/spec/abstract/X64/Arch_A.thy @@ -30,13 +30,13 @@ definition irq_state \ return $ IRQIOAPIC ioapic pin level polarity True; do_machine_op $ updateIRQState irq irq_state; set_irq_state IRQSignal (IRQ irq); - cap_insert (IRQHandlerCap (IRQ irq)) dest src + cap_insert (IRQHandlerCap (IRQ irq)) src dest od) | IssueIRQHandlerMSI irq dest src bus dev func handle \ without_preemption (do irq_state \ return $ IRQMSI bus dev func handle; do_machine_op $ updateIRQState irq irq_state; set_irq_state IRQSignal (IRQ irq); - cap_insert (IRQHandlerCap (IRQ irq)) dest src + cap_insert (IRQHandlerCap (IRQ irq)) src dest od) )" diff --git a/spec/machine/X64/MachineOps.thy b/spec/machine/X64/MachineOps.thy index f75a31dec..b63545d67 100644 --- a/spec/machine/X64/MachineOps.thy +++ b/spec/machine/X64/MachineOps.thy @@ -331,12 +331,12 @@ where definition numIOAPICs :: "machine_word" where -"numIOAPICs \ error []" +"numIOAPICs \ 1" (* FIXME x64: bc adrian said so *) definition ioapicIRQLines :: "machine_word" where -"ioapicIRQLines \ error []" +"ioapicIRQLines \ 24" (* FIXME x64: technically this is defined in c and should be here *) consts'