diff --git a/proof/crefine/ARM/ADT_C.thy b/proof/crefine/ARM/ADT_C.thy index b45a62fcd7..4129a5181e 100644 --- a/proof/crefine/ARM/ADT_C.thy +++ b/proof/crefine/ARM/ADT_C.thy @@ -118,26 +118,29 @@ end definition "register_to_H \ inv register_from_H" +context state_rel begin + definition to_user_context_C :: "user_context \ user_context_C" where - "to_user_context_C uc \ user_context_C (FCP (\r. uc (register_to_H (of_nat r))))" - -context kernel_m begin - -lemma ccontext_rel_to_C: - "ccontext_relation uc (to_user_context_C uc)" - apply (clarsimp simp: ccontext_relation_def to_user_context_C_def) - apply (rule arg_cong [where f=uc]) - apply (simp add: register_to_H_def inv_def) - done - -end + "to_user_context_C uc \ + user_context_C (ARRAY r. user_regs uc (register_to_H (of_nat r))) + (user_fpu_state_C ((ARRAY r. fpuRegs (fpu_state uc) (finite_index r))) + (fpuExc (fpu_state uc)) (fpuScr (fpu_state uc)))" definition from_user_context_C :: "user_context_C \ user_context" where - "from_user_context_C uc \ \r. index (registers_C uc) (unat (register_from_H r))" + "from_user_context_C uc \ + UserContext (FPUState (Rep_array (fpregs_C (fpuState_C uc))) + (fpexc_C (fpuState_C uc)) + (fpscr_C (fpuState_C uc))) + (\r. (registers_C uc).[unat (register_from_H r)])" + +lemma (in kernel_m) ccontext_rel_to_C: + "ccontext_relation uc (to_user_context_C uc)" + unfolding ccontext_relation_def to_user_context_C_def cregs_relation_def fpu_relation_def + by (clarsimp simp: register_to_H_def inv_def split: fpu_state.splits) definition getContext_C :: "tcb_C ptr \ cstate \ user_context" @@ -145,9 +148,23 @@ where "getContext_C thread \ \s. from_user_context_C (tcbContext_C (the (clift (t_hrs_' (globals s)) (Ptr &(thread\[''tcbArch_C''])))))" +lemma fpu_relation_Rep: + "fpu_relation fH fC \ Rep_array (fpregs_C fC) = fpuRegs fH" + unfolding fpu_relation_def index_def + apply (clarsimp split: fpu_state.splits) + apply (subst (asm) forall_finite_index[where 'a=fpu_regs, symmetric, simplified]) + by auto + lemma from_user_context_C: "ccontext_relation uc uc' \ from_user_context_C uc' = uc" - by (auto simp: ccontext_relation_def from_user_context_C_def) + unfolding ccontext_relation_def cregs_relation_def + apply clarsimp + apply (frule fpu_relation_Rep) + apply (cases uc) + apply (auto simp: from_user_context_C_def fpu_relation_def split: fpu_state.splits) + done + +end context kernel_m begin @@ -688,9 +705,23 @@ lemma cpspace_cte_relation_unique: lemma inj_tcb_ptr_to_ctcb_ptr: "inj tcb_ptr_to_ctcb_ptr" by (simp add: inj_on_def tcb_ptr_to_ctcb_ptr_def) +lemma cregs_relation_imp_eq: + "cregs_relation f x \ cregs_relation g x \ f=g" + by (auto simp: cregs_relation_def) + +lemma fpu_relation_imp_eq: + "fpu_relation f x \ fpu_relation g x \ f=g" + unfolding fpu_relation_def index_def + apply (clarsimp split: fpu_state.splits) + apply (subst (asm) forall_finite_index[where 'a=fpu_regs, symmetric, simplified])+ + by auto + lemma ccontext_relation_imp_eq: "ccontext_relation f x \ ccontext_relation g x \ f=g" - by (rule ext) (simp add: ccontext_relation_def) + unfolding ccontext_relation_def + apply (cases f, cases g) + apply (auto dest: fpu_relation_imp_eq cregs_relation_imp_eq) + done lemma carch_tcb_relation_imp_eq: "carch_tcb_relation f x \ carch_tcb_relation g x \ f = g" @@ -724,7 +755,7 @@ lemma map_to_ctes_tcb_ctes: apply (frule_tac s1=s' in ps_clear_def3[THEN iffD1,rotated 2], assumption, simp add: objBits_simps') apply (drule (1) ps_clear_16)+ - apply (simp add: is_aligned_add_helper[of _ 9 "0x10", simplified] + apply (simp add: is_aligned_add_helper[of _ 10 "0x10", simplified] split_def objBits_simps') apply (rule conjI) apply (clarsimp simp: map_to_ctes_def Let_def fun_eq_iff) @@ -734,7 +765,7 @@ lemma map_to_ctes_tcb_ctes: apply (frule_tac s1=s' in ps_clear_def3[THEN iffD1,rotated 2], assumption, simp add: objBits_simps') apply (drule (1) ps_clear_is_aligned_ctes_None(1))+ - apply (simp add: is_aligned_add_helper[of _ 9 "0x20", simplified] + apply (simp add: is_aligned_add_helper[of _ 10 "0x20", simplified] split_def objBits_simps') apply (rule conjI) apply (clarsimp simp: map_to_ctes_def Let_def fun_eq_iff) @@ -744,7 +775,7 @@ lemma map_to_ctes_tcb_ctes: apply (frule_tac s1=s' in ps_clear_def3[THEN iffD1,rotated 2], assumption, simp add: objBits_simps') apply (drule (1) ps_clear_is_aligned_ctes_None(2))+ - apply (simp add: is_aligned_add_helper[of _ 9 "0x30", simplified] + apply (simp add: is_aligned_add_helper[of _ 10 "0x30", simplified] split_def objBits_simps') apply (clarsimp simp: map_to_ctes_def Let_def fun_eq_iff) apply (drule_tac x="p+0x40" in spec, simp add: objBitsKO_def) @@ -753,7 +784,7 @@ lemma map_to_ctes_tcb_ctes: apply (frule_tac s1=s' in ps_clear_def3[THEN iffD1,rotated 2], assumption, simp add: objBits_simps') apply (drule (1) ps_clear_is_aligned_ctes_None(3))+ - apply (simp add: is_aligned_add_helper[of _ 9 "0x40", simplified] + apply (simp add: is_aligned_add_helper[of _ 10 "0x40", simplified] split_def objBits_simps') done @@ -804,7 +835,7 @@ lemma cpspace_tcb_relation_unique: apply (frule ksPSpace_valid_objs_tcbBoundNotification_nonzero[OF vs]) apply (frule ksPSpace_valid_objs_tcbBoundNotification_nonzero[OF vs']) apply (thin_tac "map_to_tcbs x y = Some z" for x y z)+ - apply (case_tac x, case_tac y, case_tac "the (clift ch (tcb_Ptr (p+0x100)))") + apply (case_tac x, case_tac y, case_tac "the (clift ch (tcb_Ptr (p+0x200)))") apply (clarsimp simp: ctcb_relation_def ran_tcb_cte_cases) apply (clarsimp simp: option_to_ptr_def option_to_0_def split: option.splits) apply (auto simp: cfault_rel_imp_eq cthread_state_rel_imp_eq carch_tcb_relation_imp_eq diff --git a/proof/crefine/ARM/ArchMove_C.thy b/proof/crefine/ARM/ArchMove_C.thy index 938d1c8f2f..be730921eb 100644 --- a/proof/crefine/ARM/ArchMove_C.thy +++ b/proof/crefine/ARM/ArchMove_C.thy @@ -223,7 +223,9 @@ proof - qed lemma user_getreg_rv: - "\obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb r)) t\ asUser t (getRegister r) \\rv s. P rv\" + "\obj_at' (\tcb. P ((user_regs \ atcbContextGet \ tcbArch) tcb r)) t\ + asUser t (getRegister r) + \\rv s. P rv\" apply (simp add: asUser_def split_def) apply (wp threadGet_wp) apply (clarsimp simp: obj_at'_def projectKOs getRegister_def in_monad atcbContextGet_def) diff --git a/proof/crefine/ARM/Arch_C.thy b/proof/crefine/ARM/Arch_C.thy index 516e609e78..3bd32b36a3 100644 --- a/proof/crefine/ARM/Arch_C.thy +++ b/proof/crefine/ARM/Arch_C.thy @@ -1433,6 +1433,10 @@ lemma valid_pde_slots_lift2: apply (wp hoare_vcg_ex_lift hoare_vcg_conj_lift | assumption)+ done +lemma addrFromPPtr_mask_6: + "addrFromPPtr ptr && mask (6::nat) = ptr && mask (6::nat)" + by (rule addrFromPPtr_mask[where n=6, simplified]) + lemma pteCheckIfMapped_ccorres: "ccorres (\rv rv'. rv = to_bool rv') ret__unsigned_long_' \ (UNIV \ {s. pte___ptr_to_struct_pte_C_' s = Ptr slot}) [] @@ -1596,7 +1600,7 @@ lemma performPageInvocationMapPTE_ccorres: apply (subst add_diff_eq [symmetric], subst is_aligned_no_wrap', assumption, fastforce) apply (simp add:addrFromPPtr_mask_5) apply (clarsimp simp:pte_range_relation_def ptr_add_def ptr_range_to_list_def - addrFromPPtr_mask_5) + addrFromPPtr_mask_6) apply (auto simp: valid_pte_slots'2_def upt_conv_Cons[where i=0])[1] apply (clarsimp simp: guard_is_UNIV_def hd_conv_nth last_conv_nth ucast_minus) apply (clarsimp simp: pte_range_relation_def ptr_range_to_list_def objBits_simps archObjSize_def) @@ -1856,7 +1860,7 @@ lemma performPageInvocationMapPDE_ccorres: apply (subst is_aligned_no_wrap', assumption, fastforce) apply (simp add:addrFromPPtr_mask_5) apply (clarsimp simp: pde_range_relation_def ptr_range_to_list_def CTypesDefs.ptr_add_def - valid_pde_slots'2_def addrFromPPtr_mask_5) + valid_pde_slots'2_def addrFromPPtr_mask_6) apply (auto simp: upt_conv_Cons[where i=0])[1] apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem hd_conv_nth last_conv_nth) apply (clarsimp simp: pde_range_relation_def ptr_range_to_list_def pdeBits_def) @@ -3141,7 +3145,7 @@ lemma decodeARMPageDirectoryInvocation_ccorres: apply (simp add:linorder_not_le) apply (erule word_less_sub_1) apply (simp add:mask_add_aligned mask_twice) - apply (subgoal_tac "5 \ pageBitsForSize a") + apply (subgoal_tac "6 \ pageBitsForSize a") apply (frule(1) is_aligned_weaken) apply (simp add:mask_add_aligned mask_twice) apply (erule order_trans[rotated]) diff --git a/proof/crefine/ARM/CLevityCatch.thy b/proof/crefine/ARM/CLevityCatch.thy index 2b822d91c2..fbff4b2e49 100644 --- a/proof/crefine/ARM/CLevityCatch.thy +++ b/proof/crefine/ARM/CLevityCatch.thy @@ -62,7 +62,7 @@ declare empty_fail_doMachineOp [simp] lemma asUser_get_registers: "\tcb_at' target\ asUser target (mapM getRegister xs) - \\rv s. obj_at' (\tcb. map ((atcbContextGet o tcbArch) tcb) xs = rv) target s\" + \\rv s. obj_at' (\tcb. map ((user_regs \ atcbContextGet \ tcbArch) tcb) xs = rv) target s\" apply (induct xs) apply (simp add: mapM_empty asUser_return) apply wp diff --git a/proof/crefine/ARM/CSpace_C.thy b/proof/crefine/ARM/CSpace_C.thy index 607f475755..6ce7f65f0a 100644 --- a/proof/crefine/ARM/CSpace_C.thy +++ b/proof/crefine/ARM/CSpace_C.thy @@ -2554,7 +2554,7 @@ definition | Some (Cap_endpoint_cap c) \ 4 | Some (Cap_notification_cap c) \ 4 | Some (Cap_cnode_cap c) \ unat (capCNodeRadix_CL c) + 4 - | Some (Cap_thread_cap c) \ 9 + | Some (Cap_thread_cap c) \ 10 | Some (Cap_small_frame_cap c) \ 12 | Some (Cap_frame_cap c) \ pageBitsForSize (gen_framesize_to_H $ generic_frame_cap_get_capFSize_CL cap) | Some (Cap_page_table_cap c) \ 10 @@ -2562,7 +2562,7 @@ definition | Some (Cap_asid_pool_cap c) \ asidLowBits + 2 | Some (Cap_zombie_cap c) \ let type = cap_zombie_cap_CL.capZombieType_CL c in - if isZombieTCB_C type then 9 else unat (type && mask 5) + 4 + if isZombieTCB_C type then 10 else unat (type && mask 5) + 4 | _ \ 0" lemma generic_frame_cap_size[simp]: diff --git a/proof/crefine/ARM/Fastpath_C.thy b/proof/crefine/ARM/Fastpath_C.thy index 79948463ae..1fadb8d09e 100644 --- a/proof/crefine/ARM/Fastpath_C.thy +++ b/proof/crefine/ARM/Fastpath_C.thy @@ -1574,7 +1574,7 @@ lemma ctes_of_Some_cte_wp_at: by (clarsimp simp: cte_wp_at_ctes_of) lemma user_getreg_wp: - "\\s. tcb_at' t s \ (\rv. obj_at' (\tcb. (atcbContextGet o tcbArch) tcb r = rv) t s \ Q rv s)\ + "\\s. tcb_at' t s \ (\rv. obj_at' (\tcb. (user_regs o atcbContextGet o tcbArch) tcb r = rv) t s \ Q rv s)\ asUser t (getRegister r) \Q\" apply (rule_tac Q="\rv s. \rv'. rv' = rv \ Q rv' s" in hoare_post_imp) apply simp @@ -1698,8 +1698,8 @@ lemma fastpath_call_ccorres: notes hoare_TrueI[simp] shows "ccorres dc xfdc (\s. invs' s \ ct_in_state' ((=) Running) s - \ obj_at' (\tcb. (atcbContextGet o tcbArch) tcb ARM_H.capRegister = cptr - \ (atcbContextGet o tcbArch) tcb ARM_H.msgInfoRegister = msginfo) + \ obj_at' (\tcb. (user_regs o atcbContextGet o tcbArch) tcb ARM_H.capRegister = cptr + \ (user_regs o atcbContextGet o tcbArch) tcb ARM_H.msgInfoRegister = msginfo) (ksCurThread s) s) (UNIV \ {s. cptr_' s = cptr} \ {s. msgInfo_' s = msginfo}) [] (fastpaths SysCall) (Call fastpath_call_'proc)" @@ -2514,8 +2514,8 @@ lemma fastpath_reply_recv_ccorres: notes hoare_TrueI[simp] shows "ccorres dc xfdc (\s. invs' s \ ct_in_state' ((=) Running) s - \ obj_at' (\tcb. (atcbContextGet o tcbArch) tcb capRegister = cptr - \ (atcbContextGet o tcbArch) tcb msgInfoRegister = msginfo) + \ obj_at' (\tcb. (user_regs o atcbContextGet o tcbArch) tcb capRegister = cptr + \ (user_regs o atcbContextGet o tcbArch) tcb msgInfoRegister = msginfo) (ksCurThread s) s) (UNIV \ {s. cptr_' s = cptr} \ {s. msgInfo_' s = msginfo}) [] (fastpaths SysReplyRecv) (Call fastpath_reply_recv_'proc)" diff --git a/proof/crefine/ARM/Fastpath_Equiv.thy b/proof/crefine/ARM/Fastpath_Equiv.thy index fcb1e1e8e7..ce77586fe9 100644 --- a/proof/crefine/ARM/Fastpath_Equiv.thy +++ b/proof/crefine/ARM/Fastpath_Equiv.thy @@ -248,7 +248,7 @@ lemma ctes_of_Some_cte_wp_at: by (clarsimp simp: cte_wp_at_ctes_of) lemma user_getreg_wp: - "\\s. tcb_at' t s \ (\rv. obj_at' (\tcb. (atcbContextGet o tcbArch) tcb r = rv) t s \ Q rv s)\ + "\\s. tcb_at' t s \ (\rv. obj_at' (\tcb. (user_regs \ atcbContextGet \ tcbArch) tcb r = rv) t s \ Q rv s)\ asUser t (getRegister r) \Q\" apply (rule_tac Q="\rv s. \rv'. rv' = rv \ Q rv' s" in hoare_post_imp) apply simp @@ -1069,7 +1069,7 @@ lemma setEndpoint_setCTE_pivot[unfolded K_bind_def]: setEndpoint_typ_at'[where T="koType TYPE(cte)", unfolded typ_at_to_obj_at'] | simp)+ apply (rule_tac P="\s. epat = ep_at' p s \ cteat = real_cte_at' slot s - \ tcbat = (tcb_at' (slot && ~~ mask 9) and (%y. slot && mask 9 : dom tcb_cte_cases)) s" + \ tcbat = (tcb_at' (slot && ~~ mask 10) and (%y. slot && mask 10 : dom tcb_cte_cases)) s" in monadic_rewrite_pre_imp_eq) apply (simp add: setEndpoint_def setObject_modify_assert bind_assoc exec_gets assert_def exec_modify @@ -1159,7 +1159,7 @@ lemma set_setCTE[unfolded K_bind_def]: apply (rule monadic_rewrite_transverse, rule monadic_rewrite_add_gets, rule monadic_rewrite_bind_tail) apply (rule monadic_rewrite_trans, - rule_tac f="tcb_at' (p && ~~ mask 9) and K (p && mask 9 \ dom tcb_cte_cases)" + rule_tac f="tcb_at' (p && ~~ mask 10) and K (p && mask 10 \ dom tcb_cte_cases)" in monadic_rewrite_add_gets) apply (rule monadic_rewrite_transverse, rule monadic_rewrite_add_gets, rule monadic_rewrite_bind_tail) @@ -1176,7 +1176,7 @@ lemma set_setCTE[unfolded K_bind_def]: apply (rule monadic_rewrite_bind_tail)+ apply (rule_tac P="c = cteat \ t = tcbat \ (tcbat \ - (\ getF setF. tcb_cte_cases (p && mask 9) = Some (getF, setF) + (\ getF setF. tcb_cte_cases (p && mask 10) = Some (getF, setF) \ (\ f g tcb. setF f (setF g tcb) = setF (f o g) tcb)))" in monadic_rewrite_gen_asm) apply (rule monadic_rewrite_is_refl[OF ext]) diff --git a/proof/crefine/ARM/Finalise_C.thy b/proof/crefine/ARM/Finalise_C.thy index b72f830bd7..39bc97b553 100644 --- a/proof/crefine/ARM/Finalise_C.thy +++ b/proof/crefine/ARM/Finalise_C.thy @@ -2003,13 +2003,32 @@ lemma ccap_relation_IRQHandler_mask: apply (simp add: c_valid_cap_def cap_irq_handler_cap_lift cl_valid_cap_def) done -lemma prepare_thread_delete_ccorres: - "ccorres dc xfdc \ UNIV [] +lemma fpuThreadDelete_ccorres: + "ccorres dc xfdc + (invs' and tcb_at' thread) + (UNIV \ {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}) hs + (fpuThreadDelete thread) (Call fpuThreadDelete_'proc)" + supply Collect_const[simp del] dc_simp[simp del] + apply (cinit lift: thread_') + apply clarsimp + apply (ctac (no_vcg) add: nativeThreadUsingFPU_ccorres) + apply clarsimp + apply (rule ccorres_when[where R=\]) + apply fastforce + apply (ctac add: switchFpuOwner_ccorres) + apply wpsimp + apply fastforce + done + +lemma prepareThreadDelete_ccorres: + "ccorres dc xfdc + (invs' and tcb_at' thread) + (UNIV \ {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}) hs (prepareThreadDelete thread) (Call Arch_prepareThreadDelete_'proc)" - unfolding prepareThreadDelete_def - apply (rule ccorres_Call) - apply (rule Arch_prepareThreadDelete_impl[unfolded Arch_prepareThreadDelete_body_def]) - apply (rule ccorres_return_Skip) + supply dc_simp[simp del] + apply (cinit lift: thread_', rename_tac cthread) + apply (ctac add: fpuThreadDelete_ccorres) + apply fastforce done lemma finaliseCap_ccorres: @@ -2112,7 +2131,7 @@ lemma finaliseCap_ccorres: apply csymbr apply (ctac(no_vcg) add: unbindNotification_ccorres) apply (ctac(no_vcg) add: suspend_ccorres[OF cteDeleteOne_ccorres]) - apply (ctac(no_vcg) add: prepare_thread_delete_ccorres) + apply (ctac(no_vcg) add: prepareThreadDelete_ccorres) apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: word_sle_def return_def) @@ -2182,14 +2201,15 @@ lemma finaliseCap_ccorres: apply (simp add: guard_is_UNIV_def) apply (clarsimp simp: cap_get_tag_isCap word_sle_def Collect_const_mem) apply (intro impI conjI) - apply (clarsimp split: bool.splits) - apply (clarsimp split: bool.splits) - apply (clarsimp simp: valid_cap'_def isCap_simps) + apply (clarsimp split: bool.splits) + apply (clarsimp split: bool.splits) + apply (clarsimp simp: valid_cap'_def isCap_simps) + apply (clarsimp simp: isCap_simps capRange_def capAligned_def) + apply (clarsimp simp: isCap_simps valid_cap'_def) apply (clarsimp simp: isCap_simps capRange_def capAligned_def) - apply (clarsimp simp: isCap_simps valid_cap'_def) - apply (clarsimp simp: isCap_simps valid_cap'_def) - apply (clarsimp simp: isCap_simps valid_cap'_def) - apply (clarsimp simp: isCap_simps valid_cap'_def ) + apply (clarsimp simp: isCap_simps valid_cap'_def ) + apply clarsimp + apply (clarsimp simp: isCap_simps valid_cap'_def ) apply (clarsimp simp: tcb_ptr_to_ctcb_ptr_def ccap_relation_def isCap_simps c_valid_cap_def cap_thread_cap_lift_def cap_to_H_def ctcb_ptr_to_tcb_ptr_def Let_def diff --git a/proof/crefine/ARM/Interrupt_C.thy b/proof/crefine/ARM/Interrupt_C.thy index c5b5d8d1e0..5282a97b05 100644 --- a/proof/crefine/ARM/Interrupt_C.thy +++ b/proof/crefine/ARM/Interrupt_C.thy @@ -371,7 +371,7 @@ lemma isIRQActive_ccorres: (isIRQActive irq) (Call isIRQActive_'proc)" apply (cinit lift: irq_') apply (simp add: getIRQState_def getInterruptState_def) - apply (rule_tac P="irq \ ucast Kernel_C.maxIRQ \ unat irq < (160::nat)" in ccorres_gen_asm) + apply (rule_tac P="irq \ ucast Kernel_C.maxIRQ \ unat irq < (161::nat)" in ccorres_gen_asm) apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: simpler_gets_def word_sless_msb_less maxIRQ_def diff --git a/proof/crefine/ARM/Invoke_C.thy b/proof/crefine/ARM/Invoke_C.thy index 95d9a658ca..0ffbc22449 100644 --- a/proof/crefine/ARM/Invoke_C.thy +++ b/proof/crefine/ARM/Invoke_C.thy @@ -1949,7 +1949,7 @@ lemma resetUntypedCap_ccorres: apply (simp add: is_aligned_def addr_card_def card_word) apply clarsimp - apply (rule conseqPre, vcg exspec=cleanCacheRange_RAM_preserves_bytes + apply (rule conseqPre, vcg exspec=cleanCacheRange_PoC_preserves_bytes exspec=cleanCacheRange_RAM_preserves_bytes exspec=preemptionPoint_modifies) apply (clarsimp simp: in_set_conv_nth isCap_simps length_upto_enum_step upto_enum_step_nth @@ -1972,7 +1972,6 @@ lemma resetUntypedCap_ccorres: is_aligned_add_multI conj_comms region_actually_is_bytes_def) apply (simp add: Kernel_Config.resetChunkBits_def is_aligned_def) - apply (rule hoare_pre) apply (wp updateFreeIndex_cte_wp_at updateFreeIndex_clear_invs' updateFreeIndex_pspace_no_overlap' diff --git a/proof/crefine/ARM/Ipc_C.thy b/proof/crefine/ARM/Ipc_C.thy index 4ec3ea85ef..b156086e9d 100644 --- a/proof/crefine/ARM/Ipc_C.thy +++ b/proof/crefine/ARM/Ipc_C.thy @@ -1268,6 +1268,13 @@ lemma ccorres_add_getRegister: apply fastforce done +lemma user_getreg_rv: + "\obj_at' (\tcb. P ((user_regs o atcbContextGet o tcbArch) tcb r)) t\ asUser t (getRegister r) \\rv s. P rv\" + apply (simp add: asUser_def split_def) + apply (wp threadGet_wp) + apply (clarsimp simp: obj_at'_def projectKOs getRegister_def in_monad atcbContextGet_def) + done + lemma exceptionMessage_ccorres: "n < unat n_exceptionMessage \ register_from_H (ARM_H.exceptionMessage ! n) @@ -1293,7 +1300,7 @@ lemma exceptionMessage_length_aux : lemma copyMRsFault_ccorres_exception: "ccorres dc xfdc (valid_pspace' - and obj_at' (\tcb. map (atcbContext (tcbArch tcb)) ARM_H.exceptionMessage = msg) sender + and obj_at' (\tcb. map (user_regs (atcbContext (tcbArch tcb))) ARM_H.exceptionMessage = msg) sender and K (length msg = 3) and K (recvBuffer \ Some 0) and K (sender \ receiver)) @@ -1315,7 +1322,7 @@ lemma copyMRsFault_ccorres_exception: for as bs, simplified] bind_assoc) apply (rule ccorres_rhs_assoc2, rule ccorres_split_nothrow_novcg) - apply (rule_tac F="K $ obj_at' (\tcb. map ((atcbContext o tcbArch) tcb) ARM_H.exceptionMessage = msg) sender" + apply (rule_tac F="K $ obj_at' (\tcb. map ((user_regs o atcbContext o tcbArch) tcb) ARM_H.exceptionMessage = msg) sender" in ccorres_mapM_x_while) apply (clarsimp simp: n_msgRegisters_def) apply (rule ccorres_guard_imp2) @@ -1361,7 +1368,7 @@ lemma mapM_cong: "\ \x. elem x xs \ f x = g x \< lemma copyMRsFault_ccorres_syscall: "ccorres dc xfdc (valid_pspace' - and obj_at' (\tcb. map (atcbContext (tcbArch tcb)) ARM_H.syscallMessage = msg) sender + and obj_at' (\tcb. map (user_regs (atcbContext (tcbArch tcb))) ARM_H.syscallMessage = msg) sender and (case recvBuffer of Some x \ valid_ipc_buffer_ptr' x | None \ \) and K (length msg = 12) and K (recvBuffer \ Some 0) @@ -1400,7 +1407,7 @@ proof - and ys="drop (unat n_msgRegisters) (zip as bs)" for as bs, simplified] bind_assoc) apply (rule ccorres_rhs_assoc2, rule ccorres_split_nothrow_novcg) - apply (rule_tac F="K $ obj_at' (\tcb. map ((atcbContext o tcbArch) tcb) ARM_H.syscallMessage = msg) sender" + apply (rule_tac F="K $ obj_at' (\tcb. map ((user_regs o atcbContext o tcbArch) tcb) ARM_H.syscallMessage = msg) sender" in ccorres_mapM_x_while) apply (clarsimp simp: n_msgRegisters_def) apply (rule ccorres_guard_imp2) @@ -1429,7 +1436,7 @@ proof - apply (rule ccorres_Cond_rhs) apply (simp del: Collect_const) apply (rule ccorres_rel_imp) - apply (rule_tac F="\_. obj_at' (\tcb. map ((atcbContext o tcbArch) tcb) ARM_H.syscallMessage = msg) + apply (rule_tac F="\_. obj_at' (\tcb. map ((user_regs o atcbContext o tcbArch) tcb) ARM_H.syscallMessage = msg) sender and valid_pspace' and (case recvBuffer of Some x \ valid_ipc_buffer_ptr' x | None \ \)" in ccorres_mapM_x_while'[where i="unat n_msgRegisters"]) diff --git a/proof/crefine/ARM/IsolatedThreadAction.thy b/proof/crefine/ARM/IsolatedThreadAction.thy index a4326bc4da..5e3be0ab6c 100644 --- a/proof/crefine/ARM/IsolatedThreadAction.thy +++ b/proof/crefine/ARM/IsolatedThreadAction.thy @@ -9,6 +9,8 @@ theory IsolatedThreadAction imports ArchMove_C begin +context begin interpretation Arch . + datatype tcb_state_regs = TCBStateRegs (tsrState : thread_state) (tsrContext : "MachineTypes.register \ machine_word") @@ -16,13 +18,16 @@ definition get_tcb_state_regs :: "kernel_object option \ tcb_state_regs" where "get_tcb_state_regs oko \ case oko of - Some (KOTCB tcb) \ TCBStateRegs (tcbState tcb) ((atcbContextGet o tcbArch) tcb)" + Some (KOTCB tcb) \ TCBStateRegs (tcbState tcb) ((user_regs o atcbContextGet o tcbArch) tcb)" definition put_tcb_state_regs_tcb :: "tcb_state_regs \ tcb \ tcb" where "put_tcb_state_regs_tcb tsr tcb \ case tsr of - TCBStateRegs st regs \ tcb \ tcbState := st, tcbArch := atcbContextSet regs (tcbArch tcb) \" + TCBStateRegs st regs \ + tcb \ tcbState := st, + tcbArch := atcbContextSet (UserContext (fpu_state (atcbContext (tcbArch tcb))) regs) + (tcbArch tcb) \" definition put_tcb_state_regs :: "tcb_state_regs \ kernel_object option \ kernel_object option" @@ -54,15 +59,20 @@ definition return rv od" +lemma UserContextGet[simp]: + "UserContext (fpu_state (atcbContext t)) (user_regs (atcbContextGet t)) = atcbContextGet t" + by (cases t, simp add: atcbContextGet_def) + lemma put_tcb_state_regs_twice[simp]: "put_tcb_state_regs tsr (put_tcb_state_regs tsr' tcb) = put_tcb_state_regs tsr tcb" apply (simp add: put_tcb_state_regs_def put_tcb_state_regs_tcb_def - makeObject_tcb + atcbContextSet_def + makeObject_tcb newArchTCB_def newContext_def initContext_def split: tcb_state_regs.split option.split Structures_H.kernel_object.split) apply (intro all_tcbI impI allI) - apply simp + apply (case_tac q, simp) done lemma partial_overwrite_twice[simp]: @@ -103,8 +113,6 @@ lemmas setEndpoint_obj_at_tcb' = setEndpoint_obj_at'_tcb lemmas setNotification_tcb = set_ntfn_tcb_obj_at' -context begin interpretation Arch . (*FIXME: arch_split*) - lemma setObject_modify: fixes v :: "'a :: pspace_storable" shows "\ obj_at' (P :: 'a \ bool) p s; updateObject v = updateObject_default v; @@ -136,8 +144,6 @@ lemma getObject_return: apply (simp add: magnitudeCheck_assert in_monad) done -end - lemmas getObject_return_tcb = getObject_return[OF meta_eq_to_obj_eq, OF loadObject_tcb, unfolded objBits_simps', simplified] @@ -156,13 +162,13 @@ lemma partial_overwrite_fun_upd: lemma get_tcb_state_regs_ko_at': "ko_at' ko p s \ get_tcb_state_regs (ksPSpace s p) - = TCBStateRegs (tcbState ko) ((atcbContextGet o tcbArch) ko)" + = TCBStateRegs (tcbState ko) ((user_regs o atcbContextGet o tcbArch) ko)" by (clarsimp simp: obj_at'_def projectKOs get_tcb_state_regs_def) lemma put_tcb_state_regs_ko_at': "ko_at' ko p s \ put_tcb_state_regs tsr (ksPSpace s p) = Some (KOTCB (ko \ tcbState := tsrState tsr - , tcbArch := atcbContextSet (tsrContext tsr) (tcbArch ko)\))" + , tcbArch := atcbContextSet (UserContext (fpu_state (atcbContext (tcbArch ko))) (tsrContext tsr)) (tcbArch ko)\))" by (clarsimp simp: obj_at'_def projectKOs put_tcb_state_regs_def put_tcb_state_regs_tcb_def split: tcb_state_regs.split) @@ -193,7 +199,7 @@ lemma ksPSpace_update_partial_id: done lemma isolate_thread_actions_asUser: - "\ idx t' = t; inj idx; f = (\s. ({(v, g s)}, False)) \ \ + "\ idx t' = t; inj idx; f = (\s. ({(v, UserContext (fpu_state s) (g (user_regs s)))}, False)) \ \ monadic_rewrite False True (\s. \x. tcb_at' (idx x) s) (asUser t f) (isolate_thread_actions idx (return v) @@ -214,17 +220,33 @@ lemma isolate_thread_actions_asUser: apply (clarsimp simp: partial_overwrite_get_tcb_state_regs put_tcb_state_regs_ko_at') apply (case_tac ko, simp) + apply (rename_tac uc) + apply (case_tac uc, simp add: modify_registers_def atcbContextGet_def atcbContextSet_def) + done + +lemma getRegister_simple: + "getRegister r = (\con. ({(user_regs con r, con)}, False))" + by (simp add: getRegister_def simpler_gets_def) + +lemma mapM_getRegister_simple: + "mapM getRegister rs = (\con. ({(map (user_regs con) rs, con)}, False))" + apply (induct rs) + apply (simp add: mapM_Nil return_def) + apply (simp add: mapM_Cons getRegister_def simpler_gets_def + bind_def return_def) done context begin interpretation Arch . (*FIXME: arch_split*) lemma setRegister_simple: - "setRegister r v = (\con. ({((), con (r := v))}, False))" + "setRegister r v = (\con. ({((), UserContext (fpu_state con) ((user_regs con)(r := v)))}, False))" by (simp add: setRegister_def simpler_modify_def) lemma zipWithM_setRegister_simple: "zipWithM_x setRegister rs vs - = (\con. ({((), foldl (\con (r, v). con (r := v)) con (zip rs vs))}, False))" + = (\con. ({((), + UserContext (fpu_state con) + (foldl (\regs (r, v). ((regs)(r := v))) (user_regs con) (zip rs vs)))}, False))" supply if_split[split del] apply (simp add: zipWithM_x_mapM_x) apply (induct ("zip rs vs")) @@ -273,7 +295,7 @@ lemma map_to_ctes_partial_overwrite: cong: if_cong option.case_cong) apply (case_tac obj, simp split: tcb_state_regs.split if_split) apply (intro impI allI) - apply (subgoal_tac "x - idx xa = x && mask 9") + apply (subgoal_tac "x - idx xa = x && mask 10") apply (clarsimp simp: tcb_cte_cases_def split: if_split) apply (drule_tac t = "idx xa" in sym) apply simp @@ -616,7 +638,6 @@ lemma findPDForASID_isolatable: lemma getHWASID_isolatable: "thread_actions_isolatable idx (getHWASID asid)" apply (simp add: getHWASID_def loadHWASID_def - findFreeHWASID_def case_option_If2 findPDForASIDAssert_def checkPDAt_def checkPDUniqueToASID_def checkPDASIDMapMembership_def @@ -697,6 +718,13 @@ lemma lookupIPC_inv: "\P\ lookupIPCBuffer f t \\ (* FIXME move *) lemmas empty_fail_user_getreg[intro!, wp, simp] = empty_fail_asUser[OF empty_fail_getRegister] +lemma user_getreg_rv: + "\obj_at' (\tcb. P ((user_regs o atcbContextGet o tcbArch) tcb r)) t\ asUser t (getRegister r) \\rv s. P rv\" + apply (simp add: asUser_def split_def) + apply (wp threadGet_wp) + apply (clarsimp simp: obj_at'_def projectKOs getRegister_def in_monad atcbContextGet_def) + done + lemma copyMRs_simple: "msglen \ of_nat (length msgRegisters) \ copyMRs sender sbuf receiver rbuf msglen @@ -718,7 +746,7 @@ lemma doIPCTransfer_simple_rewrite: \ msgLength (messageInfoFromWord msgInfo) \ of_nat (length msgRegisters)) and obj_at' (\tcb. tcbFault tcb = None - \ (atcbContextGet o tcbArch) tcb msgInfoRegister = msgInfo) sender) + \ (user_regs o atcbContextGet o tcbArch) tcb msgInfoRegister = msgInfo) sender) (doIPCTransfer sender ep badge grant rcvr) (do rv \ mapM_x (\r. do v \ asUser sender (getRegister r); asUser rcvr (setRegister r v) @@ -881,17 +909,6 @@ lemma activateThread_simple_rewrite: end -lemma setCTE_obj_at_prio[wp]: - "\obj_at' (\tcb. P (tcbPriority tcb)) t\ setCTE p v \\rv. obj_at' (\tcb. P (tcbPriority tcb)) t\" - unfolding setCTE_def - by (rule setObject_cte_obj_at_tcb', simp+) - -crunch obj_at_prio[wp]: cteInsert "obj_at' (\tcb. P (tcbPriority tcb)) t" - (wp: crunch_wps) - -crunch ctes_of[wp]: asUser "\s. P (ctes_of s)" - (wp: crunch_wps) - lemma tcbSchedEnqueue_tcbPriority[wp]: "\obj_at' (\tcb. P (tcbPriority tcb)) t\ tcbSchedEnqueue t' @@ -1021,8 +1038,7 @@ lemma setCTE_assert_modify: apply (subst updateObject_cte_tcb) apply (fastforce simp add: subtract_mask) apply (simp add: assert_opt_def alignCheck_assert bind_assoc - magnitudeCheck_assert - is_aligned_neg_mask2 objBits_def) + magnitudeCheck_assert objBits_def) apply (rule ps_clear_lookupAround2, assumption+) apply (rule word_and_le2) apply (simp add: objBits_simps mask_def field_simps) @@ -1060,13 +1076,19 @@ lemma partial_overwrite_fun_upd2: else y)" by (simp add: fun_eq_iff partial_overwrite_def split: if_split) +lemma atcbContextSetSetGet_eq[simp]: + "atcbContextSet (UserContext (fpu_state (atcbContext + (atcbContextSet (UserContext (fpu_state (atcbContext t)) r) t))) + (user_regs (atcbContextGet t))) t = t" + by (cases t, simp add: atcbContextSet_def atcbContextGet_def) + lemma setCTE_isolatable: "thread_actions_isolatable idx (setCTE p v)" supply if_split[split del] apply (simp add: setCTE_assert_modify) apply (clarsimp simp: thread_actions_isolatable_def monadic_rewrite_def fun_eq_iff - liftM_def exec_gets + liftM_def isolate_thread_actions_def bind_assoc exec_gets getSchedulerAction_def bind_select_f_bind[symmetric] @@ -1313,6 +1335,7 @@ lemma copy_register_isolate: apply (case_tac obj, case_tac obja) apply (simp add: projectKO_opt_tcb put_tcb_state_regs_def put_tcb_state_regs_tcb_def get_tcb_state_regs_def + atcbContextGet_def cong: if_cong) apply (auto simp: fun_eq_iff split: if_split) done @@ -1431,7 +1454,8 @@ lemmas fastpath_isolatables thread_actions_isolatable_returns lemmas fastpath_isolate_rewrites - = isolate_thread_actions_threadSet_tcbState isolate_thread_actions_asUser + = isolate_thread_actions_threadSet_tcbState + isolate_thread_actions_asUser copy_registers_isolate setSchedulerAction_isolate fastpath_isolatables[THEN thread_actions_isolatableD] @@ -1475,3 +1499,5 @@ lemma setThreadState_rewrite_simple: end end + +end diff --git a/proof/crefine/ARM/Machine_C.thy b/proof/crefine/ARM/Machine_C.thy index edd276229a..eceac99f0a 100644 --- a/proof/crefine/ARM/Machine_C.thy +++ b/proof/crefine/ARM/Machine_C.thy @@ -20,8 +20,28 @@ assumes resetTimer_ccorres: (doMachineOp resetTimer) (Call resetTimer_'proc)" +(* ARM: Lazy FPU switching takes place outside of verified code. The remaining invocation within + verified code only clears out some global FPU state. We therefore do not verify the lazy FPU + switching at this time, as it would require a number of C changes, same as for X64 (see VER-951) + *) +assumes nativeThreadUsingFPU_ccorres: + "ccorres (\rv rv'. rv' = from_bool rv) ret__unsigned_long_' + (tcb_at' thread) + (UNIV \ \\thread = tcb_ptr_to_ctcb_ptr thread\) + [] + (doMachineOp (nativeThreadUsingFPU thread)) + (Call nativeThreadUsingFPU_'proc)" + +assumes switchFpuOwner_ccorres: + "ccorres dc xfdc \ + (UNIV \ \\new_owner = Ptr new_owner\ + \ \\cpu = cpu\) + [] + (doMachineOp (switchFpuOwner new_owner cpu)) + (Call switchFpuOwner_'proc)" + assumes writeTTBR0_ccorres: - "ccorres dc xfdc \ (\\val = pd\) [] + "ccorres dc xfdc \ (\\val___unsigned_long = pd\) [] (doMachineOp (writeTTBR0 pd)) (Call writeTTBR0_'proc)" @@ -263,7 +283,7 @@ lemma lineStart_le_mono: by (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1 neg_mask_mono_le) lemma lineStart_sub: - "\ x && mask 5 = y && mask 5\ \ lineStart (x - y) = lineStart x - lineStart y" + "\ x && mask 6 = y && mask 6\ \ lineStart (x - y) = lineStart x - lineStart y" apply (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1) apply (clarsimp simp: mask_out_sub_mask) apply (clarsimp simp: mask_eqs(8)[symmetric]) @@ -271,22 +291,22 @@ lemma lineStart_sub: lemma lineStart_mask: - "lineStart x && mask 5 = 0" + "lineStart x && mask 6 = 0" by (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1 mask_AND_NOT_mask) lemma cachRangeOp_corres_helper: - "\w1 \ w2; w3 \ w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\ - \ unat (lineStart w2 - lineStart w1) div 32 = - unat (lineStart (w3 + (w2 - w1)) - lineStart w3) div 32" + "\w1 \ w2; w3 \ w3 + (w2 - w1); w1 && mask 6 = w3 && mask 6\ + \ unat (lineStart w2 - lineStart w1) div 64 = + unat (lineStart (w3 + (w2 - w1)) - lineStart w3) div 64" apply (subst dvd_div_div_eq_mult, simp) - apply (clarsimp simp: and_mask_dvd_nat[where n=5, simplified]) + apply (clarsimp simp: and_mask_dvd_nat[where n=6, simplified]) apply (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1) apply (subst mask_eqs(8)[symmetric]) apply (clarsimp simp: mask_AND_NOT_mask) - apply (clarsimp simp: and_mask_dvd_nat[where n=5, simplified]) + apply (clarsimp simp: and_mask_dvd_nat[where n=6, simplified]) apply (subst mask_eqs(8)[symmetric]) apply (clarsimp simp: lineStart_mask) - apply (subgoal_tac "w3 + (w2 - w1) && mask 5 = w2 && mask 5") + apply (subgoal_tac "w3 + (w2 - w1) && mask 6 = w2 && mask 6") apply clarsimp apply (rule_tac x=w1 and y=w3 in linorder_le_cases) apply (subgoal_tac "lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1") @@ -335,8 +355,8 @@ lemma lineIndex_le_mono: by (clarsimp simp: lineIndex_def2 cacheLineBits_def le_shiftr) lemma lineIndex_lineStart_diff: - "w1 \ w2 \ (unat (lineStart w2 - lineStart w1) div 32) = unat (lineIndex w2 - lineIndex w1)" - apply (subst shiftr_div_2n'[symmetric, where n=5, simplified]) + "w1 \ w2 \ (unat (lineStart w2 - lineStart w1) div 64) = unat (lineIndex w2 - lineIndex w1)" + apply (subst shiftr_div_2n'[symmetric, where n=6, simplified]) apply (drule lineStart_le_mono) apply (drule sub_right_shift[OF lineStart_mask lineStart_mask]) apply (simp add: lineIndex_def cacheLineBits_def) @@ -345,15 +365,15 @@ lemma lineIndex_lineStart_diff: lemma cacheRangeOp_ccorres: "\\x y. empty_fail (oper x y); \n. ccorres dc xfdc \ (\\index = lineIndex w1 + of_nat n\) hs - (doMachineOp (oper (lineStart w1 + of_nat n * 0x20) - (lineStart w3 + of_nat n * 0x20))) + (doMachineOp (oper (lineStart w1 + of_nat n * 0x40) + (lineStart w3 + of_nat n * 0x40))) f; \s. \\\<^bsub>/UNIV\<^esub> {s} f ({t. index_' t = index_' s}) \ \ ccorres dc xfdc (\_. w1 \ w2 \ w3 \ w3 + (w2 - w1) - \ w1 && mask 5 = w3 && mask 5) - (\\index = w1 >> 5\) hs + \ w1 && mask 6 = w3 && mask 6) + (\\index = w1 >> 6\) hs (doMachineOp (cacheRangeOp oper w1 w2 w3)) - (While \\index < (w2 >> 5) + 1\ + (While \\index < (w2 >> 6) + 1\ (f;; \index :== \index + 1))" apply (clarsimp simp: cacheRangeOp_def doMachineOp_mapM_x split_def cacheLine_def cacheLineBits_def) @@ -387,7 +407,7 @@ lemma cacheRangeOp_ccorres: lemma lineStart_eq_minus_mask: - "lineStart w1 = w1 - (w1 && mask 5)" + "lineStart w1 = w1 - (w1 && mask 6)" by (simp add: lineStart_def cacheLineBits_def mask_out_sub_mask[symmetric] and_not_mask) lemma lineStart_idem[simp]: @@ -396,7 +416,7 @@ lemma lineStart_idem[simp]: lemma cache_range_lineIndex_helper: - "lineIndex w1 + of_nat n << 5 = w1 - (w1 && mask 5) + of_nat n * 0x20" + "lineIndex w1 + of_nat n << 6 = w1 - (w1 && mask 6) + of_nat n * 0x40" apply (clarsimp simp: lineIndex_def cacheLineBits_def word_shiftl_add_distrib lineStart_def[symmetric, unfolded cacheLineBits_def] lineStart_eq_minus_mask[symmetric]) apply (simp add: shiftl_t2n) done @@ -404,7 +424,7 @@ lemma cache_range_lineIndex_helper: lemma cleanCacheRange_PoC_ccorres: "ccorres dc xfdc (\_. w1 \ w2 \ w3 \ w3 + (w2 - w1) - \ w1 && mask 5 = w3 && mask 5) + \ w1 && mask 6 = w3 && mask 6) (\\start = w1\ \ \\end = w2\ \ \\pstart = w3\) [] (doMachineOp (cleanCacheRange_PoC w1 w2 w3)) (Call cleanCacheRange_PoC_'proc)" @@ -422,7 +442,7 @@ lemma cleanCacheRange_PoC_ccorres: apply (ctac add: cleanByVA_ccorres) apply (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1 mask_out_sub_mask) - apply (drule_tac s="w1 && mask 5" in sym, simp add: cache_range_lineIndex_helper) + apply (drule_tac s="w1 && mask 6" in sym, simp add: cache_range_lineIndex_helper) apply (vcg exspec=cleanByVA_modifies) apply clarsimp done @@ -430,7 +450,7 @@ lemma cleanCacheRange_PoC_ccorres: lemma cleanInvalidateCacheRange_RAM_ccorres: "ccorres dc xfdc ((\s. unat (w2 - w1) \ gsMaxObjectSize s) and (\_. w1 \ w2 \ w3 \ w3 + (w2 - w1) - \ w1 && mask 5 = w3 && mask 5 \ unat (w2 - w2) \ gsMaxObjectSize s)) + \ w1 && mask 6 = w3 && mask 6 \ unat (w2 - w2) \ gsMaxObjectSize s)) (\\start = w1\ \ \\end = w2\ \ \\pstart = w3\) [] (doMachineOp (cleanInvalidateCacheRange_RAM w1 w2 w3)) (Call cleanInvalidateCacheRange_RAM_'proc)" @@ -457,7 +477,7 @@ lemma cleanInvalidateCacheRange_RAM_ccorres: apply (ctac add: cleanInvalByVA_ccorres) apply (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1 mask_out_sub_mask) - apply (drule_tac s="w1 && mask 5" in sym, simp add: cache_range_lineIndex_helper) + apply (drule_tac s="w1 && mask 6" in sym, simp add: cache_range_lineIndex_helper) apply (vcg exspec=cleanInvalByVA_modifies) apply (rule ceqv_refl) apply (ctac (no_vcg) add: dsb_ccorres) @@ -468,7 +488,7 @@ lemma cleanInvalidateCacheRange_RAM_ccorres: lemma cleanCacheRange_RAM_ccorres: "ccorres dc xfdc (\s. w1 \ w2 \ w3 \ w3 + (w2 - w1) - \ w1 && mask 5 = w3 && mask 5 + \ w1 && mask 6 = w3 && mask 6 \ unat (w2 - w1) \ gsMaxObjectSize s) (\\start = w1\ \ \\end = w2\ \ \\pstart = w3\) [] (doMachineOp (cleanCacheRange_RAM w1 w2 w3)) @@ -493,7 +513,7 @@ lemma cleanCacheRange_RAM_ccorres: lemma cleanCacheRange_PoU_ccorres: "ccorres dc xfdc ((\s. unat (w2 - w1) \ gsMaxObjectSize s) and (\_. w1 \ w2 \ w3 \ w3 + (w2 - w1) - \ w1 && mask 5 = w3 && mask 5)) + \ w1 && mask 6 = w3 && mask 6)) (\\start = w1\ \ \\end = w2\ \ \\pstart = w3\) [] (doMachineOp (cleanCacheRange_PoU w1 w2 w3)) (Call cleanCacheRange_PoU_'proc)" @@ -514,7 +534,7 @@ lemma cleanCacheRange_PoU_ccorres: apply (ctac add: cleanByVA_PoU_ccorres) apply (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1 mask_out_sub_mask) - apply (drule_tac s="w1 && mask 5" in sym, simp add: cache_range_lineIndex_helper) + apply (drule_tac s="w1 && mask 6" in sym, simp add: cache_range_lineIndex_helper) apply (vcg exspec=cleanByVA_PoU_modifies) apply clarsimp apply (frule(1) ghost_assertion_size_logic) @@ -528,7 +548,7 @@ lemma dmo_if: lemma invalidateCacheRange_RAM_ccorres: "ccorres dc xfdc ((\s. unat (w2 - w1) \ gsMaxObjectSize s) and (\_. w1 \ w2 \ w3 \ w3 + (w2 - w1) - \ w1 && mask 5 = w3 && mask 5)) + \ w1 && mask 6 = w3 && mask 6)) (\\start = w1\ \ \\end = w2\ \ \\pstart = w3\) [] (doMachineOp (invalidateCacheRange_RAM w1 w2 w3)) (Call invalidateCacheRange_RAM_'proc)" @@ -571,7 +591,7 @@ lemma invalidateCacheRange_RAM_ccorres: apply (ctac add: invalidateByVA_ccorres) apply (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1 mask_out_sub_mask) - apply (drule_tac s="w1 && mask 5" in sym, simp add: cache_range_lineIndex_helper) + apply (drule_tac s="w1 && mask 6" in sym, simp add: cache_range_lineIndex_helper) apply (vcg exspec=invalidateByVA_modifies) apply ceqv apply (ctac add: dsb_ccorres) @@ -592,7 +612,7 @@ lemma invalidateCacheRange_RAM_ccorres: lemma invalidateCacheRange_I_ccorres: "ccorres dc xfdc (\_. w1 \ w2 \ w3 \ w3 + (w2 - w1) - \ w1 && mask 5 = w3 && mask 5) + \ w1 && mask 6 = w3 && mask 6) (\\start = w1\ \ \\end = w2\ \ \\pstart = w3\) [] (doMachineOp (invalidateCacheRange_I w1 w2 w3)) (Call invalidateCacheRange_I_'proc)" @@ -611,14 +631,14 @@ lemma invalidateCacheRange_I_ccorres: apply (ctac add: invalidateByVA_I_ccorres) apply (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1 mask_out_sub_mask) - apply (drule_tac s="w1 && mask 5" in sym, simp add: cache_range_lineIndex_helper) + apply (drule_tac s="w1 && mask 6" in sym, simp add: cache_range_lineIndex_helper) apply (vcg exspec=invalidateByVA_I_modifies) apply clarsimp done lemma branchFlushRange_ccorres: "ccorres dc xfdc (\_. w1 \ w2 \ w3 \ w3 + (w2 - w1) - \ w1 && mask 5 = w3 && mask 5) + \ w1 && mask 6 = w3 && mask 6) (\\start = w1\ \ \\end = w2\ \ \\pstart = w3\) [] (doMachineOp (branchFlushRange w1 w2 w3)) (Call branchFlushRange_'proc)" @@ -637,7 +657,7 @@ lemma branchFlushRange_ccorres: apply (ctac add: branchFlush_ccorres) apply (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1 mask_out_sub_mask) - apply (drule_tac s="w1 && mask 5" in sym, simp add: cache_range_lineIndex_helper) + apply (drule_tac s="w1 && mask 6" in sym, simp add: cache_range_lineIndex_helper) apply (vcg exspec=branchFlush_modifies) apply clarsimp done diff --git a/proof/crefine/ARM/Refine_C.thy b/proof/crefine/ARM/Refine_C.thy index bc01eeafb9..529c746c6c 100644 --- a/proof/crefine/ARM/Refine_C.thy +++ b/proof/crefine/ARM/Refine_C.thy @@ -591,8 +591,8 @@ lemma ccorres_add_gets: lemma ccorres_get_registers: "\ \cptr msgInfo. ccorres dc xfdc ((\s. P s \ Q s \ - obj_at' (\tcb. (atcbContextGet o tcbArch) tcb ARM_H.capRegister = cptr - \ (atcbContextGet o tcbArch) tcb ARM_H.msgInfoRegister = msgInfo) + obj_at' (\tcb. (user_regs o atcbContextGet o tcbArch) tcb ARM_H.capRegister = cptr + \ (user_regs o atcbContextGet o tcbArch) tcb ARM_H.msgInfoRegister = msgInfo) (ksCurThread s) s) and R) (UNIV \ \\cptr = cptr\ \ \\msgInfo = msgInfo\) [] m c \ \ @@ -605,12 +605,12 @@ lemma ccorres_get_registers: apply (rule ccorres_assume_pre) apply (clarsimp simp: ct_in_state'_def st_tcb_at'_def) apply (drule obj_at_ko_at', clarsimp) - apply (erule_tac x="(atcbContextGet o tcbArch) ko ARM_H.capRegister" in meta_allE) - apply (erule_tac x="(atcbContextGet o tcbArch) ko ARM_H.msgInfoRegister" in meta_allE) + apply (erule_tac x="(user_regs o atcbContextGet o tcbArch) ko ARM_H.capRegister" in meta_allE) + apply (erule_tac x="(user_regs o atcbContextGet o tcbArch) ko ARM_H.msgInfoRegister" in meta_allE) apply (erule ccorres_guard_imp2) apply (clarsimp simp: rf_sr_ksCurThread) apply (drule(1) obj_at_cslift_tcb, clarsimp simp: obj_at'_def projectKOs) - apply (clarsimp simp: ctcb_relation_def ccontext_relation_def + apply (clarsimp simp: ctcb_relation_def ccontext_relation_def cregs_relation_def ARM_H.msgInfoRegister_def ARM_H.capRegister_def ARM.msgInfoRegister_def ARM.capRegister_def carch_tcb_relation_def diff --git a/proof/crefine/ARM/Retype_C.thy b/proof/crefine/ARM/Retype_C.thy index baaeaa0efb..6f670ccade 100644 --- a/proof/crefine/ARM/Retype_C.thy +++ b/proof/crefine/ARM/Retype_C.thy @@ -844,6 +844,34 @@ lemma update_ti_t_word32_0s: "word_rcat [0, 0, 0, (0 :: word8)] = (0 :: word32)" by (simp_all add: typ_info_word word_rcat_def bin_rcat_def) +lemma update_ti_t_word64_0s: + "update_ti_t (typ_info_t TYPE(word64)) [0,0,0,0,0,0,0,0] X = 0" + "word_rcat [0,0,0,0, 0,0,0,(0 :: word8)] = (0 :: word64)" + by (simp_all add: typ_info_word word_rcat_def bin_rcat_def) + +lemma is_aligned_ptr_aligned: + fixes p :: "'a :: c_type ptr" + assumes al: "is_aligned (ptr_val p) n" + and alignof: "align_of TYPE('a) = 2 ^ n" + shows "ptr_aligned p" + using al unfolding is_aligned_def ptr_aligned_def + by (simp add: alignof) + +lemma is_aligned_c_guard: + "is_aligned (ptr_val p) n + \ ptr_val p \ 0 + \ align_of TYPE('a) = 2 ^ m + \ size_of TYPE('a) \ 2 ^ n + \ m \ n + \ c_guard (p :: ('a :: c_type) ptr)" + apply (clarsimp simp: c_guard_def c_null_guard_def) + apply (rule conjI) + apply (rule is_aligned_ptr_aligned, erule(1) is_aligned_weaken, simp) + apply (erule is_aligned_get_word_bits, simp_all) + apply (rule intvl_nowrap[where x=0, simplified], simp) + apply (erule is_aligned_no_wrap_le, simp+) + done + lemma retype_guard_helper: assumes cover: "range_cover p sz (objBitsKO ko) n" and ptr0: "p \ 0" @@ -2533,6 +2561,16 @@ lemma update_ti_t_array_rep_word0: apply (simp add: update_ti_t_word32_0s) done +lemma update_ti_t_array_rep_word64_0: + "bs = replicate ((card (UNIV :: 'b :: finite set)) * 8) 0 \ + update_ti_t (typ_info_t TYPE(word64['b :: finite])) bs x = + foldr (\n arr. Arrays.update arr n 0) + [0..<(card (UNIV :: 'b :: finite set))] x" + apply (subst update_ti_t_array_rep) + apply simp + apply (simp add: update_ti_t_word64_0s) + done + lemma tcb_queue_update_other: "\ ctcb_ptr_to_tcb_ptr p \ set tcbs \ \ tcb_queue_relation next prev (mp(p \ v)) tcbs qe qh = @@ -2561,7 +2599,8 @@ lemma c_guard_tcb: proof (rule conjI) show "ptr_aligned p" using al apply - - apply (rule is_aligned_ptr_aligned [where n = word_size_bits]) + (* TCB starts with 64-bit FPU registers *) + apply (rule is_aligned_ptr_aligned [where n="word_size_bits + 1"]) apply (rule is_aligned_weaken) apply (erule ctcb_ptr_to_tcb_ptr_aligned) by (auto simp: align_of_def word_size_bits_def ctcb_size_bits_def) @@ -2578,7 +2617,7 @@ qed lemma tcb_ptr_orth_cte_ptrs': - "ptr_span (tcb_Ptr (regionBase + 0x100)) \ ptr_span (Ptr regionBase :: (cte_C[5]) ptr) = {}" + "ptr_span (tcb_Ptr (regionBase + 0x200)) \ ptr_span (Ptr regionBase :: (cte_C[5]) ptr) = {}" apply (rule disjointI) apply (clarsimp simp: ctcb_ptr_to_tcb_ptr_def size_td_array intvl_def field_simps size_of_def ctcb_offset_def) @@ -2867,9 +2906,16 @@ proof - let ?tcb = "undefined \tcbArch_C := tcbArch_C undefined \tcbContext_C := tcbContext_C (tcbArch_C undefined) - \registers_C := + \fpuState_C := fpuState_C (tcbContext_C (tcbArch_C undefined)) + \ fpregs_C := foldr (\n arr. Arrays.update arr n 0) [0..<32] + (fpregs_C (fpuState_C (tcbContext_C (tcbArch_C undefined)))), + fpexc_C := 0, + fpscr_C := 0 + \, + registers_C := foldr (\n arr. Arrays.update arr n 0) [0..<20] - (registers_C (tcbContext_C (tcbArch_C undefined)))\\, + (registers_C (tcbContext_C (tcbArch_C undefined)))\ + \, tcbState_C := thread_state_C.words_C_update (\_. foldr (\n arr. Arrays.update arr n 0) [0..<3] @@ -2890,20 +2936,22 @@ proof - tcbSchedNext_C := tcb_Ptr 0, tcbSchedPrev_C := tcb_Ptr 0, tcbEPNext_C := tcb_Ptr 0, tcbEPPrev_C := tcb_Ptr 0, tcbBoundNotification_C := ntfn_Ptr 0\" + have fbtcb: "from_bytes (replicate (size_of TYPE(tcb_C)) 0) = ?tcb" apply (simp add: from_bytes_def) apply (simp add: typ_info_simps tcb_C_tag_def) apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def)(* takes ages *) - apply (simp add: update_ti_adjust_ti update_ti_t_word32_0s + apply (simp add: update_ti_adjust_ti update_ti_t_word32_0s update_ti_t_word64_0s typ_info_simps user_context_C_tag_def thread_state_C_tag_def seL4_Fault_C_tag_def lookup_fault_C_tag_def update_ti_t_ptr_0s arch_tcb_C_tag_def ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td - align_of_def padup_def + ti_typ_combine_empty_ti ti_typ_combine_td + align_of_def padup_def user_fpu_state_C_tag_def user_context_C_tag_def final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def align_td_array' size_td_array) - apply (simp add: update_ti_t_array_rep_word0) + apply (simp add: update_ti_t_array_rep_word0 update_ti_t_array_rep_word64_0) done have tcb_rel: @@ -2911,21 +2959,27 @@ proof - unfolding ctcb_relation_def makeObject_tcb apply (simp add: fbtcb minBound_word) apply (intro conjI) - apply (simp add: cthread_state_relation_def thread_state_lift_def - eval_nat_numeral ThreadState_Inactive_def) - apply (simp add: ccontext_relation_def carch_tcb_relation_def) - apply (rule allI) - subgoal for r - by (case_tac r; - simp add: "StrictC'_register_defs" eval_nat_numeral atcbContext_def atcbContextGet_def - newArchTCB_def newContext_def initContext_def take_bit_Suc - del: unsigned_numeral) - apply (simp add: thread_state_lift_def eval_nat_numeral atcbContextGet_def)+ - apply (simp add: Kernel_Config.timeSlice_def) - apply (simp add: cfault_rel_def seL4_Fault_lift_def seL4_Fault_get_tag_def Let_def - lookup_fault_lift_def lookup_fault_get_tag_def lookup_fault_invalid_root_def - eval_nat_numeral seL4_Fault_NullFault_def option_to_ptr_def option_to_0_def - split: if_split)+ + apply (simp add: cthread_state_relation_def thread_state_lift_def + eval_nat_numeral ThreadState_Inactive_def) + apply (clarsimp simp: ccontext_relation_def carch_tcb_relation_def) + apply (rule conjI) + (* C regs relation *) + apply (clarsimp simp: cregs_relation_def) + subgoal for r + by (case_tac r; + simp add: "StrictC'_register_defs" eval_nat_numeral atcbContext_def atcbContextGet_def + newArchTCB_def newContext_def initContext_def take_bit_Suc + del: unsigned_numeral) + (* FPU state relation *) + apply (clarsimp simp: ccontext_relation_def carch_tcb_relation_def + newArchTCB_def atcbContextGet_def fpu_relation_def + newContext_def newFPUState_def index_foldr_update) + apply (simp add: thread_state_lift_def eval_nat_numeral atcbContextGet_def)+ + apply (simp add: Kernel_Config.timeSlice_def) + apply (simp add: cfault_rel_def seL4_Fault_lift_def seL4_Fault_get_tag_def Let_def + lookup_fault_lift_def lookup_fault_get_tag_def lookup_fault_invalid_root_def + eval_nat_numeral seL4_Fault_NullFault_def option_to_ptr_def option_to_0_def + split: if_split)+ done have pks: "ks (ctcb_ptr_to_tcb_ptr p) = None" @@ -3986,7 +4040,7 @@ lemma ccorres_placeNewObject_tcb: ({s. region_actually_is_zero_bytes regionBase (2^tcbBlockSizeBits) s}) hs (placeNewObject regionBase (makeObject :: tcb) 0) - (\tcb :== tcb_Ptr (regionBase + 0x100);; + (\tcb :== tcb_Ptr (regionBase + 0x200);; (global_htd_update (\s. ptr_retyp (Ptr (ptr_val (tcb_' s) - ctcb_offset) :: (cte_C[5]) ptr) \ ptr_retyp (tcb_' s)));; (Guard C_Guard \hrs_htd \t_hrs \\<^sub>t \tcb\ @@ -3999,10 +4053,10 @@ lemma ccorres_placeNewObject_tcb: apply (rule conseqPre) apply vcg apply (clarsimp simp: rf_sr_htd_safe ctcb_offset_defs) - apply (subgoal_tac "c_guard (tcb_Ptr (regionBase + 0x100))") + apply (subgoal_tac "c_guard (tcb_Ptr (regionBase + 0x200))") apply (subgoal_tac "hrs_htd (hrs_htd_update (ptr_retyp (Ptr regionBase :: (cte_C[5]) ptr) - \ ptr_retyp (tcb_Ptr (regionBase + 0x100))) - (t_hrs_' (globals x))) \\<^sub>t tcb_Ptr (regionBase + 0x100)") + \ ptr_retyp (tcb_Ptr (regionBase + 0x200))) + (t_hrs_' (globals x))) \\<^sub>t tcb_Ptr (regionBase + 0x200)") prefer 2 apply (clarsimp simp: hrs_htd_update) apply (rule h_t_valid_ptr_retyps_gen_disjoint[where n=1 and arr=False, @@ -4027,7 +4081,7 @@ lemma ccorres_placeNewObject_tcb: apply (rule bexI [OF _ placeNewObject_eq]) apply (clarsimp simp: split_def new_cap_addrs_def) apply (cut_tac \=\ and x=x - and ks="ksPSpace \" and p="tcb_Ptr (regionBase + 0x100)" in cnc_tcb_helper) + and ks="ksPSpace \" and p="tcb_Ptr (regionBase + 0x200)" in cnc_tcb_helper) apply clarsimp apply (clarsimp simp: ctcb_ptr_to_tcb_ptr_def ctcb_offset_defs objBitsKO_def range_cover.aligned) diff --git a/proof/crefine/ARM/StateRelation_C.thy b/proof/crefine/ARM/StateRelation_C.thy index 1f68d18a5b..73f59171ab 100644 --- a/proof/crefine/ARM/StateRelation_C.thy +++ b/proof/crefine/ARM/StateRelation_C.thy @@ -237,9 +237,24 @@ fun | "register_from_H ARM.FaultIP = scast Kernel_C.FaultIP" definition - ccontext_relation :: "(MachineTypes.register \ word32) \ user_context_C \ bool" + cregs_relation :: "(MachineTypes.register \ machine_word) \ machine_word[20] \ bool" where - "ccontext_relation regs uc \ \r. regs r = index (registers_C uc) (unat (register_from_H r))" + "cregs_relation Hregs Cregs \ \r. Hregs r = Cregs.[unat (register_from_H r)]" + +definition + fpu_relation :: "fpu_state \ user_fpu_state_C \ bool" +where + "fpu_relation fpu_H fpu_C \ + case fpu_H of FPUState fpregs exc scr \ + (\r < CARD(fpu_regs). fpregs (finite_index r) = (fpregs_C fpu_C).[r]) + \ exc = fpexc_C fpu_C + \ scr = fpscr_C fpu_C" + +definition + ccontext_relation :: "user_context \ user_context_C \ bool" +where + "ccontext_relation uc_H uc_C \ cregs_relation (user_regs uc_H) (registers_C uc_C) \ + fpu_relation (fpu_state uc_H) (fpuState_C uc_C)" primrec cthread_state_relation_lifted :: "Structures_H.thread_state \ @@ -598,7 +613,7 @@ fun | "irqstate_to_C irqstate.IRQReserved = scast Kernel_C.IRQReserved" definition - cinterrupt_relation :: "interrupt_state \ 'a ptr \ (word32[160]) \ bool" + cinterrupt_relation :: "interrupt_state \ 'a ptr \ (word32[161]) \ bool" where "cinterrupt_relation airqs cnode cirqs \ cnode = Ptr (intStateIRQNode airqs) \ diff --git a/proof/crefine/ARM/SyscallArgs_C.thy b/proof/crefine/ARM/SyscallArgs_C.thy index ac977cc863..f8704a8d83 100644 --- a/proof/crefine/ARM/SyscallArgs_C.thy +++ b/proof/crefine/ARM/SyscallArgs_C.thy @@ -623,7 +623,8 @@ lemma asUser_const_rv: lemma getMRs_tcbContext: "\\s. n < unat n_msgRegisters \ n < unat (msgLength info) \ thread = ksCurThread s \ cur_tcb' s\ getMRs thread buffer info - \\rv s. obj_at' (\tcb. atcbContextGet (tcbArch tcb) (ARM_H.msgRegisters ! n) = rv ! n) (ksCurThread s) s\" + \\rv s. obj_at' (\tcb. user_regs (atcbContextGet (tcbArch tcb)) (ARM_H.msgRegisters ! n) = rv ! n) + (ksCurThread s) s\" apply (rule hoare_assume_pre) apply (elim conjE) apply (thin_tac "thread = t" for t) @@ -1179,7 +1180,9 @@ lemma getSyscallArg_ccorres_foo: apply (simp add: word_less_nat_alt split: if_split) apply (rule ccorres_add_return2) apply (rule ccorres_symb_exec_l) - apply (rule_tac P="\s. n < unat (scast n_msgRegisters :: word32) \ obj_at' (\tcb. atcbContextGet (tcbArch tcb) (ARM_H.msgRegisters!n) = x!n) (ksCurThread s) s" + apply (rule_tac P="\s. n < unat (scast n_msgRegisters :: word32) + \ obj_at' (\tcb. user_regs (atcbContextGet (tcbArch tcb)) + (ARM_H.msgRegisters!n) = x!n) (ksCurThread s) s" and P' = UNIV in ccorres_from_vcg_split_throws) apply vcg @@ -1190,7 +1193,7 @@ lemma getSyscallArg_ccorres_foo: apply (clarsimp simp: typ_heap_simps') apply (clarsimp simp: ctcb_relation_def ccontext_relation_def msgRegisters_ccorres atcbContextGet_def - carch_tcb_relation_def) + carch_tcb_relation_def cregs_relation_def) apply (subst (asm) msgRegisters_ccorres) apply (clarsimp simp: n_msgRegisters_def) apply (simp add: n_msgRegisters_def word_less_nat_alt) diff --git a/proof/crefine/ARM/Syscall_C.thy b/proof/crefine/ARM/Syscall_C.thy index cdd7f8c900..6b45a06101 100644 --- a/proof/crefine/ARM/Syscall_C.thy +++ b/proof/crefine/ARM/Syscall_C.thy @@ -1485,7 +1485,7 @@ lemma ucast_maxIRQ_is_less: "SCAST(32 signed \ 32) Kernel_C.maxIRQ < UCAST(10 \ 32) irq \ scast Kernel_C.maxIRQ < irq" apply (clarsimp simp: scast_def Kernel_C.maxIRQ_def) apply (subgoal_tac "LENGTH(10) \ LENGTH(32)") - apply (drule less_ucast_ucast_less[where x= "0x9F" and y="irq"]) + apply (drule less_ucast_ucast_less[where x= "0xA0" and y="irq"]) by (simp)+ lemma scast_maxIRQ_is_not_less: "(\ (Kernel_C.maxIRQ) (ucast :: irq \ 16 word)) b) \ \ (scast Kernel_C.maxIRQ < b)" diff --git a/proof/crefine/ARM/TcbAcc_C.thy b/proof/crefine/ARM/TcbAcc_C.thy index c9e9e58920..e5a3425ea9 100644 --- a/proof/crefine/ARM/TcbAcc_C.thy +++ b/proof/crefine/ARM/TcbAcc_C.thy @@ -76,13 +76,14 @@ lemma getRegister_ccorres [corres]: apply (drule (1) obj_at_cslift_tcb) apply (clarsimp simp: typ_heap_simps register_from_H_less) apply (clarsimp simp: getRegister_def typ_heap_simps) - apply (rule_tac x = "((atcbContextGet o tcbArch) ko reg, \)" in bexI [rotated]) + apply (rule_tac x = "((user_regs o atcbContextGet o tcbArch) ko reg, \)" in bexI [rotated]) apply (simp add: in_monad' asUser_def select_f_def split_def) apply (subst arg_cong2 [where f = "(\)"]) defer apply (rule refl) apply (erule threadSet_eq) - apply (clarsimp simp: ctcb_relation_def ccontext_relation_def carch_tcb_relation_def) + apply (clarsimp simp: ctcb_relation_def ccontext_relation_def cregs_relation_def + carch_tcb_relation_def) apply (wp threadGet_obj_at2)+ apply simp apply simp diff --git a/proof/crefine/ARM/Tcb_C.thy b/proof/crefine/ARM/Tcb_C.thy index 8a515d6123..d2506daafd 100644 --- a/proof/crefine/ARM/Tcb_C.thy +++ b/proof/crefine/ARM/Tcb_C.thy @@ -507,7 +507,7 @@ lemma invokeTCB_ThreadControl_ccorres: del: Collect_const cong: call_ignore_cong if_cong) apply (rule_tac P="ptr_val (tcb_ptr_to_ctcb_ptr target) && ~~ mask 4 = ptr_val (tcb_ptr_to_ctcb_ptr target) - \ ptr_val (tcb_ptr_to_ctcb_ptr target) && 0xFFFFFE00 = target" + \ ptr_val (tcb_ptr_to_ctcb_ptr target) && 0xFFFFFC00 = target" in ccorres_gen_asm) apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow_novcg) apply (rule ccorres_cond_both'[where Q=\ and Q'=\]) @@ -1730,7 +1730,7 @@ shows = min (unat n) (unat n_frameRegisters + unat n_gpRegisters)" in ccorres_gen_asm) apply (rule ccorres_split_nothrow_novcg) - apply (rule_tac F="\m s. obj_at' (\tcb. map ((atcbContextGet o tcbArch) tcb) (genericTake n + apply (rule_tac F="\m s. obj_at' (\tcb. map ((user_regs o atcbContextGet o tcbArch) tcb) (genericTake n (ARM_H.frameRegisters @ ARM_H.gpRegisters)) = reply) target s" in ccorres_mapM_x_while) @@ -1796,7 +1796,7 @@ shows in ccorres_split_nothrow_novcg) apply (rule ccorres_Cond_rhs) apply (rule ccorres_rel_imp, - rule_tac F="\m s. obj_at' (\tcb. map ((atcbContextGet o tcbArch) tcb) (genericTake n + rule_tac F="\m s. obj_at' (\tcb. map ((user_regs o atcbContextGet o tcbArch) tcb) (genericTake n (ARM_H.frameRegisters @ ARM_H.gpRegisters)) = reply) target s \ valid_ipc_buffer_ptr' (the destIPCBuffer) s @@ -1909,7 +1909,7 @@ shows apply (rename_tac i_c, rule_tac P="i_c = 0" in ccorres_gen_asm2) apply (simp add: drop_zip del: Collect_const) apply (rule ccorres_Cond_rhs) - apply (rule_tac F="\m s. obj_at' (\tcb. map ((atcbContextGet o tcbArch) tcb) (genericTake n + apply (rule_tac F="\m s. obj_at' (\tcb. map ((user_regs o atcbContextGet o tcbArch) tcb) (genericTake n (ARM_H.frameRegisters @ ARM_H.gpRegisters)) = reply) target s \ valid_ipc_buffer_ptr' (the destIPCBuffer) s \ valid_pspace' s" diff --git a/proof/crefine/ARM/VSpace_C.thy b/proof/crefine/ARM/VSpace_C.thy index 725ae72eea..00f497171b 100644 --- a/proof/crefine/ARM/VSpace_C.thy +++ b/proof/crefine/ARM/VSpace_C.thy @@ -1563,7 +1563,7 @@ definition | ARM_H.flush_type.Unify \ (label = Kernel_C.ARMPageUnify_Instruction \ label = Kernel_C.ARMPDUnify_Instruction)" lemma doFlush_ccorres: - "ccorres dc xfdc (\s. vs \ ve \ ps \ ps + (ve - vs) \ vs && mask 5 = ps && mask 5 + "ccorres dc xfdc (\s. vs \ ve \ ps \ ps + (ve - vs) \ vs && mask 6 = ps && mask 6 \ unat (ve - vs) \ gsMaxObjectSize s) (\flushtype_relation t \invLabel___int\ \ \\start = vs\ \ \\end = ve\ \ \\pstart = ps\) [] (doMachineOp (doFlush t vs ve ps)) (Call doFlush_'proc)" @@ -1625,7 +1625,7 @@ context kernel_m begin lemma performPageFlush_ccorres: "ccorres (K (K \) \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and K (asid \ mask asid_bits) - and (\s. ps \ ps + (ve - vs) \ vs && mask 5 = ps && mask 5 + and (\s. ps \ ps + (ve - vs) \ vs && mask 6 = ps && mask 6 \ unat (ve - vs) \ gsMaxObjectSize s)) (\\pd = Ptr pd\ \ \\asid = asid\ \ \\start = vs\ \ \\end = ve\ \ \\pstart = ps\ \ \flushtype_relation typ \invLabel___int \) @@ -1701,7 +1701,7 @@ lemma setRegister_ccorres: apply (rule ball_tcb_cte_casesI, simp+) apply (clarsimp simp: ctcb_relation_def ccontext_relation_def atcbContextSet_def atcbContextGet_def - carch_tcb_relation_def + carch_tcb_relation_def cregs_relation_def split: if_split) apply (clarsimp simp: Collect_const_mem register_from_H_less) @@ -1756,7 +1756,7 @@ lemma setMessageInfo_ccorres: lemma performPageDirectoryInvocationFlush_ccorres: "ccorres (K (K \) \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and K (asid \ mask asid_bits) - and (\s. ps \ ps + (ve - vs) \ vs && mask 5 = ps && mask 5 + and (\s. ps \ ps + (ve - vs) \ vs && mask 6 = ps && mask 6 \ unat (ve - vs) \ gsMaxObjectSize s)) (\\pd = Ptr pd\ \ \\asid = asid\ \ \\start = vs\ \ \\end = ve\ \ \\pstart = ps\ \ \flushtype_relation typ \invLabel___int \) @@ -1947,7 +1947,7 @@ lemma ccorres_return_void_C': lemma is_aligned_cache_preconds: "\is_aligned rva n; n \ 6\ \ rva \ rva + 0x3F \ - addrFromPPtr rva \ addrFromPPtr rva + 0x3F \ rva && mask 5 = addrFromPPtr rva && mask 5" + addrFromPPtr rva \ addrFromPPtr rva + 0x3F \ rva && mask 6 = addrFromPPtr rva && mask 6" supply if_cong[cong] apply (drule is_aligned_weaken, simp) apply (rule conjI) @@ -1956,7 +1956,6 @@ lemma is_aligned_cache_preconds: apply (drule is_aligned_addrFromPPtr_n, simp) apply (drule is_aligned_no_overflow, unat_arith) apply (frule is_aligned_addrFromPPtr_n, simp) - apply (drule_tac x=6 and y=5 in is_aligned_weaken, simp)+ apply (simp add: is_aligned_mask) done diff --git a/spec/cspec/ARM/Kernel_C.thy b/spec/cspec/ARM/Kernel_C.thy index 89042169be..ac73812b5e 100644 --- a/spec/cspec/ARM/Kernel_C.thy +++ b/spec/cspec/ARM/Kernel_C.thy @@ -79,7 +79,7 @@ end definition ctcb_size_bits :: nat where - "ctcb_size_bits \ 8" + "ctcb_size_bits \ 9" definition ctcb_offset :: "32 word"