From 7d2cc21e3f85bfeecd3f9679e17ed7c21483303a Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 26 Feb 2024 11:24:16 +0100 Subject: [PATCH] x64 crefine: ioapic_nirqs updates Signed-off-by: Gerwin Klein --- proof/crefine/X64/ADT_C.thy | 12 ++- proof/crefine/X64/Interrupt_C.thy | 121 ++++++++++++++++++++------ proof/crefine/X64/SR_lemmas_C.thy | 9 +- proof/crefine/X64/StateRelation_C.thy | 1 + 4 files changed, 113 insertions(+), 30 deletions(-) diff --git a/proof/crefine/X64/ADT_C.thy b/proof/crefine/X64/ADT_C.thy index d113aa6f15..b4f53402db 100644 --- a/proof/crefine/X64/ADT_C.thy +++ b/proof/crefine/X64/ADT_C.thy @@ -541,6 +541,10 @@ end context state_rel begin +definition + "ioapic_nirqs_from_to_H cstate \ + \x. if x \ of_nat maxNumIOAPIC then ioapic_nirqs_' cstate.[unat x] else 0" + definition "carch_state_to_H cstate \ X64KernelState @@ -555,6 +559,7 @@ definition x64KSKernelVSpace_C (cioport_bitmap_to_H (the (clift (t_hrs_' cstate) (Ptr (symbol_table ''x86KSAllocatedIOPorts''))))) (ucast (num_ioapics_' cstate)) + (ioapic_nirqs_from_to_H cstate) \ \Map IRQ states to their Haskell equivalent, and out-of-bounds entries to X64IRQFree\ (case_option X64IRQFree id \ (array_map_conv @@ -584,6 +589,8 @@ lemma carch_state_to_H_correct: using valid[simplified valid_arch_state'_def] apply (fastforce simp: valid_asid_table'_def) apply (simp add: ccr3_relation_def split: cr3.splits) + apply (rule conjI) + apply (solves \clarsimp simp: global_ioport_bitmap_relation_def\) apply (rule conjI) prefer 2 apply (rule ext) @@ -591,7 +598,10 @@ lemma carch_state_to_H_correct: array_to_map_def) using valid[simplified valid_arch_state'_def valid_x64_irq_state'_def] apply (case_tac "x \ maxIRQ"; fastforce split: option.split) - apply (clarsimp simp: global_ioport_bitmap_relation_def) + apply (clarsimp simp: array_relation_def ioapic_nirqs_from_to_H_def) + apply (rule ext) + using valid[simplified valid_arch_state'_def valid_ioapic_def] + apply (clarsimp simp: not_le) done end diff --git a/proof/crefine/X64/Interrupt_C.thy b/proof/crefine/X64/Interrupt_C.thy index f623cebd71..fc693a6b07 100644 --- a/proof/crefine/X64/Interrupt_C.thy +++ b/proof/crefine/X64/Interrupt_C.thy @@ -530,32 +530,76 @@ lemma ccorres_pre_gets_x64KSNumIOAPICs_ksArchState: apply clarsimp done +lemma ccorres_pre_gets_x64KSIOAPICnIRQs_ksArchState: + assumes cc: "\rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" + shows "ccorres r xf + (\s. (\rv. x64KSIOAPICnIRQs (ksArchState s) = rv \ P rv s)) + {s. \rv. s \ P' rv } + hs (gets (x64KSIOAPICnIRQs \ ksArchState) >>= (\rv. f rv)) c" + apply (rule ccorres_guard_imp) + apply (rule ccorres_symb_exec_l) + defer + apply wp[1] + apply (rule gets_sp) + apply (clarsimp simp: empty_fail_def simpler_gets_def) + apply assumption + apply clarsimp + defer + apply (rule ccorres_guard_imp) + apply (rule cc) + apply clarsimp + apply assumption + apply clarsimp + done + +lemma rf_sr_x64KSIOAPICnIRQs: + "\ (s,s') \ rf_sr; i < of_nat maxNumIOAPIC \ \ + ioapic_nirqs_' (globals s').[unat i] = x64KSIOAPICnIRQs (ksArchState s) i" + by (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def Let_def + array_relation_def) + +lemma uint_less_1_eq: (* FIXME APIC: move to Word_Lib *) + "0 < n \ (uint (n - 1) < m) = (uint n \ m)" + by uint_arith + +lemma scast_ucast_up_minus_1_ucast: (* FIXME APIC: move to Word_Lib *) + assumes "LENGTH('a::len) < LENGTH('b::len)" + assumes "0 < w" + shows "SCAST('b \ 'c) (UCAST('a \ 'b) w - 1) = UCAST('a \ 'c::len) (w - 1)" + using assms + apply (subst scast_eq_ucast; simp) + apply (metis gt0_iff_gem1 msb_less_mono ucast_less_ucast_weak unsigned_0 word_upcast_neg_msb) + apply (smt (verit) lt1_neq0 nat_le_linear scast_ucast_simps(9) ucast_1 ucast_sub_ucast + verit_comp_simplify1(3) word_le_nat_alt) + done + lemma ioapic_decode_map_pin_to_vector_ccorres: "ccorres (intr_and_se_rel \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') - \ - (UNIV - \ {s. ioapic___unsigned_long_' s = ioapic} - \ {s. pin___unsigned_long_' s = pin} - \ {s. level___unsigned_long_' s = level} - \ {s. polarity_' s = polarity}) + valid_ioapic + (\\ioapic___unsigned_long = ioapic\ \ + \\pin___unsigned_long = pin\ \ + \\level___unsigned_long = level\ \ + \\polarity = polarity\) hs (doE numIOAPICs <- liftE (gets (x64KSNumIOAPICs \ ksArchState)); + ioapic_nirqs <- liftE (gets (x64KSIOAPICnIRQs \ ksArchState)); whenE (numIOAPICs = 0) (throwError (Inl IllegalOperation)); whenE (uint (numIOAPICs - 1) < uint ioapic) (throwError (Inl (RangeError 0 (numIOAPICs - 1)))); - whenE (uint (ioapicIRQLines - 1) < uint pin) - (throwError (Inl (RangeError 0 (ioapicIRQLines - 1)))); + whenE (uint (ucast (ioapic_nirqs ioapic - 1) :: machine_word) < uint pin) + (throwError (Inl (RangeError 0 (ucast (ioapic_nirqs ioapic - 1))))); whenE (1 < uint level) (throwError (Inl (RangeError 0 1))); whenE (1 < uint polarity) (throwError (Inl (RangeError 0 1))) odE) (Call ioapic_decode_map_pin_to_vector_'proc)" - supply Collect_const[simp del] + supply Collect_const[simp del] word_less_1[simp del] (* for uniform array guard on ioapic_nirqs *) apply (cinit' lift: ioapic___unsigned_long_' pin___unsigned_long_' level___unsigned_long_' polarity_') apply (simp add: ioapicIRQLines_def cong: StateSpace.state.fold_congs globals.fold_congs) apply (clarsimp simp: liftE_bindE) apply (rule ccorres_pre_gets_x64KSNumIOAPICs_ksArchState) + apply (rule ccorres_pre_gets_x64KSIOAPICnIRQs_ksArchState) apply (rule_tac Q="\s. x64KSNumIOAPICs (ksArchState s) = numIOAPICs" and Q'=\ in ccorres_split_when_throwError_cond) apply (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def Let_def) @@ -573,28 +617,58 @@ lemma ioapic_decode_map_pin_to_vector_ccorres: EXCEPTION_SYSCALL_ERROR_def EXCEPTION_NONE_def syscall_error_rel_def) apply (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def Let_def) apply (subst ucast_sub_ucast; fastforce simp: lt1_neq0) + apply (rule_tac P="numIOAPICs \ of_nat maxNumIOAPIC" in ccorres_gen_asm) + apply (clarsimp simp: not_less word_le_def[symmetric]) + apply (prop_tac "ioapic < of_nat maxNumIOAPIC", + solves \simp add: le_m1_iff_lt[THEN iffD1] word_neq_0_conv\) + apply (simp add: Kernel_Config.maxNumIOAPIC_def) + apply ccorres_rewrite + apply (rename_tac ioapic_nirqs) + apply (rule_tac Q="\s. ioapic_nirqs = x64KSIOAPICnIRQs (ksArchState s) \ + (0 < x64KSIOAPICnIRQs (ksArchState s) ioapic)" and Q'=\ + in ccorres_split_when_throwError_cond) + apply (fastforce simp: word_le_def scast_ucast_up_eq_ucast uint_up_ucast is_up + rf_sr_x64KSIOAPICnIRQs Kernel_Config.maxNumIOAPIC_def + uint_less_1_eq) + (* Need to VCG it as the range error depends on the global state *) + apply (rule_tac P="\s. ioapic_nirqs = x64KSIOAPICnIRQs (ksArchState s) \ + numIOAPICs \ of_nat maxNumIOAPIC \ + 0 < x64KSIOAPICnIRQs (ksArchState s) ioapic \ + x64KSIOAPICnIRQs (ksArchState s) ioapic \ ucast ioapicIRQLines" + and P'="UNIV" in ccorres_from_vcg_throws) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: fst_throwError_returnOk syscall_error_to_H_cases + EXCEPTION_SYSCALL_ERROR_def EXCEPTION_NONE_def syscall_error_rel_def) + apply (simp add: rf_sr_x64KSIOAPICnIRQs Kernel_Config.maxNumIOAPIC_def + scast_ucast_up_eq_ucast ioapicIRQLines_def sint_ucast_eq_uint is_down + scast_ucast_up_minus_1_ucast) + apply uint_arith apply (rule_tac Q=\ and Q'=\ in ccorres_split_when_throwError_cond) - apply (fastforce simp: word_le_def add1_zle_eq[symmetric]) + apply clarsimp + apply (metis arith_special(21) diff_eq_diff_eq uint_1 word_less_def word_less_sub1 + word_neq_0_conv word_sub_less_iff) apply (fastforce simp: syscall_error_to_H_cases intro: syscall_error_throwError_ccorres_n) - apply (rule_tac Q=\ and Q'=\ in ccorres_split_when_throwError_cond) + apply (rule_tac Q=\ and Q'=\ + in ccorres_split_when_throwError_cond[where b="returnOk ()", simplified]) apply clarsimp apply (metis arith_special(21) diff_eq_diff_eq uint_1 word_less_def word_less_sub1 word_neq_0_conv word_sub_less_iff) apply (fastforce simp: syscall_error_to_H_cases intro: syscall_error_throwError_ccorres_n) - apply (rule_tac Q=\ and Q'=\ - in ccorres_split_when_throwError_cond[where b="returnOk ()", simplified]) - apply clarsimp - apply (metis arith_special(21) diff_eq_diff_eq uint_1 word_less_def word_less_sub1 - word_neq_0_conv word_sub_less_iff) - apply (fastforce simp: syscall_error_to_H_cases intro: syscall_error_throwError_ccorres_n) - apply (ctac add: ccorres_return_CE) - apply vcg+ - apply fastforce + apply (ctac add: ccorres_return_CE) + apply vcg+ + apply (clarsimp simp: not_less) + apply (prop_tac "ioapic < x64KSNumIOAPICs (ksArchState s)") + apply (meson word_leq_minus_one_le word_less_eq_iff_unsigned) + apply (fastforce simp: valid_ioapic_def) done (* Bundle of definitions for minIRQ, maxIRQ, minUserIRQ, etc *) lemmas c_irq_const_defs = irq_const_defs irq_user_min_def irq_user_max_def +lemma invs_valid_ioapic[elim!]: (* FIXME APIC: move *) + "invs' s \ valid_ioapic s" + by (simp add: invs'_def valid_state'_def valid_arch_state'_def) + lemma Arch_decodeIRQControlInvocation_ccorres: assumes "interpret_excaps extraCaps' = excaps_map extraCaps" shows "ccorres (intr_and_se_rel \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') @@ -867,11 +941,8 @@ from assms show ?thesis invs_sch_act_wf' ct_in_state'_def cte_wp_at_weakenE' pred_tcb'_weakenE) apply (subst pred_tcb'_weakenE, assumption, fastforce)+ - apply (rule conjI) - apply (rule TrueI) - apply (rule conjI) - apply (rule impI) - apply (rule TrueI) + apply (rule conjI, fastforce) + apply clarsimp apply (rule_tac irq1="yf" in irq64_helper_two) apply (simp only: unat_def) apply (vcg exspec=isIRQActive_modifies) diff --git a/proof/crefine/X64/SR_lemmas_C.thy b/proof/crefine/X64/SR_lemmas_C.thy index d3041b0640..afb7ec4774 100644 --- a/proof/crefine/X64/SR_lemmas_C.thy +++ b/proof/crefine/X64/SR_lemmas_C.thy @@ -1061,7 +1061,6 @@ lemma cstate_relation_only_t_hrs: ksCurThread_' s = ksCurThread_' t; ksIdleThread_' s = ksIdleThread_' t; ksWorkUnitsCompleted_' s = ksWorkUnitsCompleted_' t; - intStateIRQNode_' s = intStateIRQNode_' t; intStateIRQTable_' s = intStateIRQTable_' t; x86KSASIDTable_' s = x86KSASIDTable_' t; x64KSCurrentUserCR3_' s = x64KSCurrentUserCR3_' t; @@ -1071,6 +1070,7 @@ lemma cstate_relation_only_t_hrs: ksCurDomain_' s = ksCurDomain_' t; ksDomainTime_' s = ksDomainTime_' t; num_ioapics_' s = num_ioapics_' t; + ioapic_nirqs_' s = ioapic_nirqs_' t; x86KSIRQState_' s = x86KSIRQState_' t \ \ cstate_relation a s = cstate_relation a t" @@ -1087,7 +1087,6 @@ lemma rf_sr_upd: "(ksCurThread_' (globals x)) = (ksCurThread_' (globals y))" "(ksIdleThread_' (globals x)) = (ksIdleThread_' (globals y))" "(ksWorkUnitsCompleted_' (globals x)) = (ksWorkUnitsCompleted_' (globals y))" - "intStateIRQNode_'(globals x) = intStateIRQNode_' (globals y)" "intStateIRQTable_'(globals x) = intStateIRQTable_' (globals y)" "x86KSASIDTable_' (globals x) = x86KSASIDTable_' (globals y)" "x64KSCurrentUserCR3_' (globals x) = x64KSCurrentUserCR3_' (globals y)" @@ -1097,6 +1096,8 @@ lemma rf_sr_upd: "ksCurDomain_' (globals x) = ksCurDomain_' (globals y)" "ksDomainTime_' (globals x) = ksDomainTime_' (globals y)" "num_ioapics_' (globals x) = num_ioapics_' (globals y)" + "ioapic_nirqs_' (globals x) = ioapic_nirqs_' (globals y)" + "ioapic_nirqs_' (globals x) = ioapic_nirqs_' (globals y)" "x86KSIRQState_' (globals x) = x86KSIRQState_' (globals y)" shows "((a, x) \ rf_sr) = ((a, y) \ rf_sr)" unfolding rf_sr_def using assms @@ -1110,7 +1111,6 @@ lemma rf_sr_upd_safe[simp]: and sa: "(ksSchedulerAction_' (globals (g y))) = (ksSchedulerAction_' (globals y))" and ct: "(ksCurThread_' (globals (g y))) = (ksCurThread_' (globals y))" and it: "(ksIdleThread_' (globals (g y))) = (ksIdleThread_' (globals y))" - and isn: "intStateIRQNode_'(globals (g y)) = intStateIRQNode_' (globals y)" and ist: "intStateIRQTable_'(globals (g y)) = intStateIRQTable_' (globals y)" and dsi: "ksDomScheduleIdx_' (globals (g y)) = ksDomScheduleIdx_' (globals y)" and cdom: "ksCurDomain_' (globals (g y)) = ksCurDomain_' (globals y)" @@ -1120,11 +1120,12 @@ lemma rf_sr_upd_safe[simp]: "x64KSCurrentUserCR3_' (globals (g y)) = x64KSCurrentUserCR3_' (globals y)" "phantom_machine_state_' (globals (g y)) = phantom_machine_state_' (globals y)" "num_ioapics_' (globals (g y)) = num_ioapics_' (globals y)" + "ioapic_nirqs_' (globals (g y)) = ioapic_nirqs_' (globals y)" "x86KSIRQState_' (globals (g y)) = x86KSIRQState_' (globals y)" and gs: "ghost'state_' (globals (g y)) = ghost'state_' (globals y)" and wu: "(ksWorkUnitsCompleted_' (globals (g y))) = (ksWorkUnitsCompleted_' (globals y))" shows "((a, (g y)) \ rf_sr) = ((a, y) \ rf_sr)" - using rl rq rqL1 rqL2 sa ct it isn ist arch wu gs dsi cdom dt by - (rule rf_sr_upd) + using assms by - (rule rf_sr_upd) (* More of a well-formed lemma, but \ *) lemma valid_mdb_cslift_next: diff --git a/proof/crefine/X64/StateRelation_C.thy b/proof/crefine/X64/StateRelation_C.thy index 7f1b6b9949..b7b62ed6e9 100644 --- a/proof/crefine/X64/StateRelation_C.thy +++ b/proof/crefine/X64/StateRelation_C.thy @@ -192,6 +192,7 @@ where global_ioport_bitmap_relation (clift (t_hrs_' cstate)) (x64KSAllocatedIOPorts astate) \ fpu_null_state_relation (t_hrs_' cstate) \ x64KSNumIOAPICs astate = UCAST (32 \ 64) (num_ioapics_' cstate) \ + array_relation (=) (of_nat Kernel_Config.maxNumIOAPIC) (x64KSIOAPICnIRQs astate) (ioapic_nirqs_' cstate) \ array_relation x64_irq_state_relation maxIRQ (x64KSIRQState astate) (x86KSIRQState_' cstate) \ carch_globals astate"