diff --git a/proof/drefine/CNode_DR.thy b/proof/drefine/CNode_DR.thy index 6e7f59442..7892f232d 100644 --- a/proof/drefine/CNode_DR.thy +++ b/proof/drefine/CNode_DR.thy @@ -332,20 +332,20 @@ lemma insert_cap_child_corres: apply (clarsimp simp: caps_of_state_transform_opt_cap cte_wp_at_caps_of_state transform_cap_def)+ apply (clarsimp simp: valid_mdb_def cte_wp_at_cases dest!:invs_mdb) - apply (case_tac "cdt s' child", safe intro!: mdb_cte_atI) - (* 121 subgoals *) - by (auto dest: mdb_cte_atD is_untyped_cap_eqD - simp: valid_mdb_def swp_def cte_wp_at_caps_of_state not_idle_thread_def) + apply (case_tac "cdt s' child", safe intro!: mdb_cte_atI; + auto dest: mdb_cte_atD is_untyped_cap_eqD + simp: valid_mdb_def swp_def cte_wp_at_caps_of_state not_idle_thread_def) + done lemma reply_cap_insert_corres: "sid \ did\dcorres dc \ (valid_idle and not_idle_thread did and valid_mdb and st_tcb_at (\r. \ inactive r \ \ idle r) sid and valid_etcbs and tcb_at did and tcb_at sid and valid_objs) - (insert_cap_child (cdl_cap.ReplyCap sid) (sid, tcb_replycap_slot) + (insert_cap_child (cdl_cap.ReplyCap sid rights) (sid, tcb_replycap_slot) (did, tcb_caller_slot)) - (cap_insert (cap.ReplyCap sid False) (sid,tcb_cnode_index 2) (did,tcb_cnode_index 3))" + (cap_insert (cap.ReplyCap sid False rights) (sid,tcb_cnode_index 2) (did,tcb_cnode_index 3))" apply (rule corres_guard_imp) - apply (rule insert_cap_child_corres [where cap = "cap.ReplyCap sid False" + apply (rule insert_cap_child_corres [where cap = "cap.ReplyCap sid False rights" and src = "(sid, tcb_cnode_index 2)" and child = "(did, tcb_cnode_index 3)", unfolded transform_cap_def transform_tcb_slot_simp ,simplified]) @@ -493,11 +493,11 @@ crunch idle_thread[wp]: cap_move "\s::'a::state_ext state. P (idle_threa (wp: dxo_wp_weak) lemma cap_null_reply_case_If: - "(case cap of cap.ReplyCap t b \ f t b | cap.NullCap \ g | _ \ h) + "(case cap of cap.ReplyCap t b R \ f t b R | cap.NullCap \ g | _ \ h) = (if cap = cap.NullCap then g else if is_reply_cap cap \ is_master_reply_cap cap - then f (obj_ref_of cap) (is_master_reply_cap cap) - else h)" + then f (obj_ref_of cap) (is_master_reply_cap cap) (cap_rights cap) + else h)" by (simp add: is_reply_cap_def is_master_reply_cap_def split: cap.split) (* FIXME: move *) @@ -2323,7 +2323,7 @@ lemma lsfco_not_idle: done lemma cdl_right_UNIV: - "UNIV = {Read, Write, Grant}" + "UNIV = {Read, Write, Grant, GrantReply}" apply (rule set_eqI) apply (case_tac x, auto) done diff --git a/proof/drefine/Intent_DR.thy b/proof/drefine/Intent_DR.thy index 60f9f9ce0..69c79f911 100644 --- a/proof/drefine/Intent_DR.thy +++ b/proof/drefine/Intent_DR.thy @@ -36,17 +36,19 @@ lemma cte_wp_at_zombie_not_idle: lemmas tcb_slots = Types_D.tcb_caller_slot_def Types_D.tcb_cspace_slot_def Types_D.tcb_ipcbuffer_slot_def Types_D.tcb_pending_op_slot_def Types_D.tcb_replycap_slot_def Types_D.tcb_vspace_slot_def Types_D.tcb_boundntfn_slot_def +(* FIXME: MOVE *) lemma tcb_cap_casesE: assumes cs: "tcb_cap_cases p = Some (gf, sf, restr)" and rules: "\ p = tcb_cnode_index 0; gf = tcb_ctable; sf = tcb_ctable_update; restr = (\_ _. \) \ \ R" - "\ p = tcb_cnode_index 1; gf = tcb_vtable; sf = tcb_vtable_update; restr = (\_ _. \) \ \ R" - "\ p = tcb_cnode_index 2; gf = tcb_reply; sf = tcb_reply_update; restr = - (\t st c. - (is_master_reply_cap c \ obj_ref_of c = t) - \ (halted st \ (c = cap.NullCap))) \ \ R" - "\ p = tcb_cnode_index 3; gf = tcb_caller; sf = tcb_caller_update; restr = - (\_ st. case st of - Structures_A.BlockedOnReceive e \ + "\ p = tcb_cnode_index 1; gf = tcb_vtable; sf = tcb_vtable_update; + restr = (\_ _. is_valid_vtable_root or ((=) cap.NullCap)) \ \ R" + "\ p = tcb_cnode_index 2; gf = tcb_reply; sf = tcb_reply_update; + restr = (\t st c. (is_master_reply_cap c \ obj_ref_of c = t + \ AllowGrant \ cap_rights c) + \ (halted st \ (c = cap.NullCap))) \ \ R" + "\ p = tcb_cnode_index 3; gf = tcb_caller; sf = tcb_caller_update; + restr = (\_ st. case st of + Structures_A.BlockedOnReceive e data \ ((=) cap.NullCap) | _ \ is_reply_cap or ((=) cap.NullCap)) \ \ R" "\ p = tcb_cnode_index 4; gf = tcb_ipcframe; sf = tcb_ipcframe_update; restr = @@ -96,18 +98,20 @@ abbreviation lemma tcb_cap_cases_slot_simps[simp]: "tcb_cap_cases (tcb_cnode_index tcb_cspace_slot) = Some (tcb_ctable, tcb_ctable_update, (\_ _. \))" - "tcb_cap_cases (tcb_cnode_index tcb_vspace_slot) = Some (tcb_vtable, tcb_vtable_update, (\_ _. \))" - "tcb_cap_cases (tcb_cnode_index tcb_replycap_slot) = Some (tcb_reply, tcb_reply_update, - (\t st c. - (is_master_reply_cap c \ obj_ref_of c = t) - \ (halted st \ (c = cap.NullCap))))" - "tcb_cap_cases (tcb_cnode_index tcb_caller_slot) = Some (tcb_caller, tcb_caller_update, - (\_ st. case st of - Structures_A.BlockedOnReceive e \ - ((=) cap.NullCap) - | _ \ is_reply_cap or ((=) cap.NullCap)))" - "tcb_cap_cases (tcb_cnode_index tcb_ipcbuffer_slot) = Some (tcb_ipcframe, tcb_ipcframe_update, - (\_ _. is_nondevice_page_cap or ((=) cap.NullCap)))" + "tcb_cap_cases (tcb_cnode_index tcb_vspace_slot) = + Some (tcb_vtable, tcb_vtable_update, (\_ _. is_valid_vtable_root or ((=) cap.NullCap)))" + "tcb_cap_cases (tcb_cnode_index tcb_replycap_slot) = + Some (tcb_reply, tcb_reply_update, + (\t st c. (is_master_reply_cap c \ obj_ref_of c = t \ AllowGrant \ cap_rights c) + \ (halted st \ (c = cap.NullCap))))" + "tcb_cap_cases (tcb_cnode_index tcb_caller_slot) = + Some (tcb_caller, tcb_caller_update, + (\_ st. case st of + Structures_A.BlockedOnReceive e data \ + ((=) cap.NullCap) + | _ \ is_reply_cap or ((=) cap.NullCap)))" + "tcb_cap_cases (tcb_cnode_index tcb_ipcbuffer_slot) = + Some (tcb_ipcframe, tcb_ipcframe_update, (\_ _. is_nondevice_page_cap or ((=) cap.NullCap)))" by (simp add: tcb_slots)+ lemma opt_cap_tcb: @@ -189,7 +193,7 @@ definition generates_pending :: "Structures_A.thread_state \ bool" where "generates_pending st \ case st of - Structures_A.BlockedOnReceive ptr \ True + Structures_A.BlockedOnReceive ptr payload \ True | Structures_A.BlockedOnSend ptr payload \ True | Structures_A.BlockedOnReply \ True | Structures_A.BlockedOnNotification ptr \ True diff --git a/proof/drefine/Ipc_DR.thy b/proof/drefine/Ipc_DR.thy index c43c1b8f5..74e3e039e 100644 --- a/proof/drefine/Ipc_DR.thy +++ b/proof/drefine/Ipc_DR.thy @@ -400,12 +400,12 @@ lemma sts_gwp: lemma block_thread_on_send_corres: "dcorres dc \ (not_idle_thread thread and valid_etcbs) (KHeap_D.set_cap (thread, tcb_pending_op_slot) - (PendingSyncSendCap epptr badge call can_grant + (PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) (set_thread_state thread (Structures_A.thread_state.BlockedOnSend epptr \sender_badge = badge, sender_can_grant = can_grant, - sender_is_call = call\))" + sender_can_grant_reply = can_grant_reply, sender_is_call = call\))" apply (clarsimp simp:KHeap_D.set_cap_def set_thread_state_def) apply (rule dcorres_gets_the, clarsimp) apply (rule dcorres_rhs_noop_below_True[OF set_thread_state_ext_dcorres]) @@ -428,8 +428,9 @@ lemma block_thread_on_send_corres: lemma block_thread_on_recv_corres: "dcorres dc \ (not_idle_thread thread and valid_etcbs) (KHeap_D.set_cap (thread, tcb_pending_op_slot) - (PendingSyncRecvCap epptr False)) - (set_thread_state thread (Structures_A.thread_state.BlockedOnReceive epptr))" + (PendingSyncRecvCap epptr False can_grant)) + (set_thread_state thread + (Structures_A.thread_state.BlockedOnReceive epptr \receiver_can_grant = can_grant\))" apply (clarsimp simp:KHeap_D.set_cap_def set_thread_state_def) apply (rule dcorres_gets_the, clarsimp) apply (rule dcorres_rhs_noop_below_True[OF set_thread_state_ext_dcorres]) @@ -973,29 +974,32 @@ lemma set_thread_state_block_on_send_corres: "dcorres dc \ (not_idle_thread thread and valid_etcbs) (block_thread_on_ipc thread - (PendingSyncSendCap epptr badge call can_grant False)) + (PendingSyncSendCap epptr badge call can_grant can_grant_reply False)) (set_thread_state thread (Structures_A.thread_state.BlockedOnSend epptr - \sender_badge = badge, sender_can_grant = can_grant, sender_is_call = call\))" + \sender_badge = badge, sender_can_grant = can_grant, + sender_can_grant_reply = can_grant_reply, sender_is_call = call\))" by (simp add:block_thread_on_ipc_def,rule block_thread_on_send_corres) lemma set_thread_state_block_on_receive_corres: "dcorres dc \ (not_idle_thread thread and valid_etcbs) - (block_thread_on_ipc thread (PendingSyncRecvCap epptr False)) - (set_thread_state thread (Structures_A.thread_state.BlockedOnReceive epptr))" + (block_thread_on_ipc thread (PendingSyncRecvCap epptr False can_grant)) + (set_thread_state thread + (Structures_A.thread_state.BlockedOnReceive epptr \receiver_can_grant = can_grant\))" apply (simp add:block_thread_on_ipc_def) apply (rule block_thread_on_recv_corres) done lemma corres_setup_caller_cap: "sender \ receiver \ dcorres dc \ - (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver - and st_tcb_at (Not\ halted) sender and valid_objs and valid_etcbs) - (inject_reply_cap sender receiver) - (setup_caller_cap sender receiver)" + (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver + and tcb_at sender and tcb_at receiver + and st_tcb_at (Not \ halted) sender and valid_objs and valid_etcbs) + (inject_reply_cap sender receiver can_grant) + (setup_caller_cap sender receiver can_grant)" apply (rule dcorres_expand_pfx) apply (rule corres_guard_imp) - apply (simp add: inject_reply_cap_def setup_caller_cap_def) + apply (simp add: inject_reply_cap_def setup_caller_cap_def split del: if_split) apply (rule corres_split[OF _ set_thread_state_corres]) apply (rule reply_cap_insert_corres) apply (simp add:not_idle_thread_def)+ @@ -1159,13 +1163,14 @@ definition "dest_of xs \ case xs of [] \ None | [r] \ Some (transform_cslot_ptr r)" lemma update_cap_rights_cong: - "\ is_ep_cap cap \ is_ntfn_cap cap \ is_arch_page_cap cap \ R = R' \ \ + "\ is_ep_cap cap \ is_ntfn_cap cap \ is_reply_cap cap \ is_arch_page_cap cap \ R = R' \ \ transform_cap (cap_rights_update R' cap) = update_cap_rights R (transform_cap cap)" - by (clarsimp simp: cap_rights_update_def acap_rights_update_def update_cap_rights_def + by (clarsimp simp: is_reply_cap_def + cap_rights_update_def acap_rights_update_def update_cap_rights_def split: cap.splits arch_cap.splits) lemma transform_cap_rights: - "is_ep_cap cap \ is_ntfn_cap cap \ is_arch_page_cap cap + "is_ep_cap cap \ is_ntfn_cap cap \ is_reply_cap cap \ is_arch_page_cap cap \ (Structures_A.cap_rights cap) = Types_D.cap_rights (transform_cap cap)" by (auto simp: is_cap_simps is_arch_page_cap_def Types_D.cap_rights_def transform_cap_def split: arch_cap.splits cap.splits) @@ -1488,6 +1493,7 @@ lemma get_ipc_buffer_words_receive_slots: apply (simp add:word_mod_2p_is_mask[where n = 2,symmetric] word_of_int_hom_syms) done +(* FIXME: MOVE *) lemma dcorres_return: "r a b \ dcorres (r) (\_. True) (\_. True) (return a) (return b)" by (clarsimp simp:return_def corres_underlying_def) @@ -1586,11 +1592,10 @@ lemma get_receive_slot_dcorres: apply (clarsimp simp: word_size word_bits_def)+ apply (rule hoareE_TrueI)+ apply clarsimp - apply (rule hoare_post_impErr[OF hoareE_TrueI]) - apply fastforce + apply (rule hoare_post_impErr[OF hoareE_TrueI TrueI]) apply simp apply (wp lsfco_not_idle | clarsimp)+ - apply fastforce + apply (rule conjI; rule TrueI) apply (clarsimp simp:not_idle_thread_def) apply fastforce apply (wp mapM_wp) @@ -1944,7 +1949,7 @@ lemma corres_complete_ipc_transfer: (valid_objs and pspace_aligned and valid_global_refs and pspace_distinct and valid_mdb and (\s. not_idle_thread (cur_thread s) s) and valid_irq_node and valid_idle and not_idle_thread recv and not_idle_thread send and valid_etcbs) - (Endpoint_D.do_ipc_transfer ep' send recv can_grant) + (Endpoint_D.do_ipc_transfer ep' send recv can_grant) (* FIXME argument order *) (Ipc_A.do_ipc_transfer send ep badge can_grant recv)" apply (clarsimp simp: Endpoint_D.do_ipc_transfer_def Ipc_A.do_ipc_transfer_def) apply (rule dcorres_expand_pfx) @@ -2236,11 +2241,12 @@ lemma do_reply_transfer_corres: shows "slot' = transform_cslot_ptr slot \ dcorres dc \ - (invs and tcb_at recver and tcb_at sender and cte_wp_at ((=) (cap.ReplyCap recver False)) slot + (invs and tcb_at recver and tcb_at sender + and cte_wp_at (\cap. \R. cap = cap.ReplyCap recver False R) slot and (\s. not_idle_thread (cur_thread s) s) and not_idle_thread recver and not_idle_thread sender and valid_etcbs) - (Endpoint_D.do_reply_transfer sender recver slot') - (Ipc_A.do_reply_transfer sender recver slot)" + (Endpoint_D.do_reply_transfer sender recver slot' can_grant) + (Ipc_A.do_reply_transfer sender recver slot can_grant)" apply (clarsimp simp:do_reply_transfer_def Endpoint_D.do_reply_transfer_def) apply (clarsimp simp:get_thread_state_def thread_get_def get_thread_fault_def) apply (rule dcorres_absorb_gets_the) @@ -2296,12 +2302,13 @@ lemma do_reply_transfer_corres: apply (rule conjI) apply (case_tac slot) apply (clarsimp simp:invs_def not_idle_thread_def valid_state_def) + apply (clarsimp simp:cte_wp_at_caps_of_state) apply (drule valid_idle_has_null_cap) apply assumption+ - apply (fastforce simp:valid_state_def cte_wp_at_caps_of_state) - apply simp + apply (fastforce simp:valid_state_def) apply (rule emptyable_cte_wp_atD) - apply (simp add: is_master_reply_cap_def invs_def valid_state_def valid_pspace_def valid_idle_def)+ + apply (fastforce simp:is_master_reply_cap_def invs_def + valid_state_def valid_pspace_def valid_idle_def)+ done lemma set_endpoint_valid_irq_node[wp]: @@ -2334,34 +2341,34 @@ lemma dcorres_if_rhs: (* this is ugly and terrible, but pretty much recreates the old recv_sync_ipc_corres proof to avoid duplication *) lemma dcorres_receive_sync: - "\ ep_at word1 s; ko_at (kernel_object.Endpoint rv) word1 s; not_idle_thread thread s; + "\ ep_at ep s; ko_at (kernel_object.Endpoint rv) ep s; not_idle_thread thread s; not_idle_thread (cur_thread s) s; st_tcb_at active thread s; valid_state s; valid_etcbs s \ \ dcorres dc ((=) (transform s)) ((=) s) - (receive_sync thread word1) + (receive_sync thread ep can_grant) (case rv of Structures_A.endpoint.IdleEP \ (case is_blocking of True \ do set_thread_state thread - (Structures_A.thread_state.BlockedOnReceive word1); - set_endpoint word1 (Structures_A.endpoint.RecvEP [thread]) - od + (Structures_A.thread_state.BlockedOnReceive ep + \receiver_can_grant = can_grant\); + set_endpoint ep (Structures_A.endpoint.RecvEP [thread]) + od | False \ do_nbrecv_failed_transfer thread) | Structures_A.endpoint.SendEP q \ do assert (q \ []); queue \ return $ tl q; sender \ return $ hd q; - set_endpoint word1 $ - case queue of [] \ Structures_A.endpoint.IdleEP - | a # list \ Structures_A.endpoint.SendEP queue; + set_endpoint ep $ + (case queue of [] \ Structures_A.endpoint.IdleEP + | a # list \ Structures_A.endpoint.SendEP queue); sender_state \ get_thread_state sender; - data \ case sender_state of + payload \ case sender_state of Structures_A.thread_state.BlockedOnSend ref x \ return x | _ \ fail; - Ipc_A.do_ipc_transfer sender (Some word1) (sender_badge data) - (sender_can_grant data) thread; - fault \ thread_get tcb_fault sender; - if sender_is_call data \ fault \ None - then if sender_can_grant data - then setup_caller_cap sender thread + Ipc_A.do_ipc_transfer sender (Some ep) (sender_badge payload) + (sender_can_grant payload) thread; + if sender_is_call payload + then if sender_can_grant payload \ sender_can_grant_reply payload + then setup_caller_cap sender thread can_grant else set_thread_state sender Structures_A.thread_state.Inactive else do set_thread_state sender Structures_A.thread_state.Running; do_extended_op (possible_switch_to sender) @@ -2369,8 +2376,9 @@ lemma dcorres_receive_sync: od | Structures_A.endpoint.RecvEP queue \ (case is_blocking of True \ do set_thread_state thread - (Structures_A.thread_state.BlockedOnReceive word1); - set_endpoint word1 (Structures_A.endpoint.RecvEP (queue @ [thread])) + (Structures_A.thread_state.BlockedOnReceive ep + \receiver_can_grant = can_grant\); + set_endpoint ep (Structures_A.endpoint.RecvEP (queue @ [thread])) od | False \ do_nbrecv_failed_transfer thread))" apply (clarsimp simp: receive_sync_def gets_def) @@ -2406,65 +2414,63 @@ lemma dcorres_receive_sync: apply (rename_tac list) apply (drule_tac s = "set list" in sym) apply (rule conjI, clarsimp dest!: not_empty_list_not_empty_set) - apply (clarsimp simp:neq_Nil_conv) - apply (rule_tac P1="\" and P'="(=) s" and x1 = y + apply (clarsimp simp:neq_Nil_conv, rename_tac t ts) + apply (rule_tac P1="\" and P'="(=) s" and x1 = t in dcorres_absorb_pfx[OF select_pick_corres[OF dcorres_expand_pfx],rotated]) apply clarsimp apply clarsimp apply clarsimp - apply (drule_tac x1 = y in iffD2[OF eqset_imp_iff], simp) + apply (drule_tac x1 = t in iffD2[OF eqset_imp_iff], simp) apply (clarsimp simp:ep_waiting_set_send_def get_thread_def bind_assoc gets_the_def gets_def) + apply (rename_tac tcb payload) apply (rule dcorres_absorb_get_l,clarsimp) apply (frule(1) valid_etcbs_tcb_etcb, clarsimp) apply (subst opt_object_tcb) apply (erule get_tcb_rev) apply (fastforce simp: get_etcb_def) - apply (frule_tac a = y and list = "y # ys" in pending_thread_in_send_not_idle) - apply ((simp add: valid_state_def insertI obj_at_def not_idle_thread_def )+)[4] + apply (frule_tac a = t and list = "t # ts" in pending_thread_in_send_not_idle) + apply ((simp add: valid_state_def insertI obj_at_def not_idle_thread_def)+)[4] apply (clarsimp simp: assert_opt_def transform_tcb_def infer_tcb_pending_op_def tcb_slots split del: if_split) apply (rule dcorres_symb_exec_r) apply (rule corres_symb_exec_r) - apply (rule_tac F="sender_state = tcb_state t" in corres_gen_asm2) + apply (rule_tac F="sender_state = tcb_state tcb" in corres_gen_asm2) apply (clarsimp dest!: get_tcb_SomeD simp: dc_def[symmetric] split del: if_split split: if_split_asm) apply (rule corres_guard_imp) apply (rule corres_split[OF _ corres_complete_ipc_transfer]) prefer 2 apply simp - apply (rule corres_symb_exec_r) - apply (rule dcorres_if_rhs) - apply (rule dcorres_if_rhs) - apply (simp add:dc_def[symmetric] when_def) - apply (rule corres_alternate1)+ - apply (rule corres_setup_caller_cap) - apply (clarsimp simp:st_tcb_at_def obj_at_def generates_pending_def) - apply (rule corres_alternate2[OF set_thread_state_corres[unfolded tcb_slots]]) - apply (rule corres_alternate1[OF corres_alternate2]) - apply (rule dcorres_rhs_noop_below_True[OF possible_switch_to_dcorres]) - apply (rule set_thread_state_corres[unfolded tcb_slots]) - apply clarsimp - apply (wp hoare_drop_imps)+ - apply clarsimp - apply (wp gts_st_tcb_at | simp add:not_idle_thread_def )+ - apply (rule_tac Q="\fault. valid_mdb and valid_objs and pspace_aligned - and pspace_distinct and not_idle_thread y and not_idle_thread thread + apply (rule dcorres_if_rhs) + apply (rule dcorres_if_rhs) + apply (simp add:dc_def[symmetric] when_def) + apply (rule corres_alternate1)+ + apply (rule corres_setup_caller_cap) + apply (clarsimp simp:st_tcb_at_def obj_at_def generates_pending_def) + apply (rule corres_alternate2[OF set_thread_state_corres[unfolded tcb_slots]]) + apply (rule corres_alternate1[OF corres_alternate2]) + apply (rule dcorres_rhs_noop_below_True[OF possible_switch_to_dcorres]) + apply (rule set_thread_state_corres[unfolded tcb_slots]) + apply wp + apply (wp hoare_drop_imps gts_st_tcb_at | simp add:not_idle_thread_def)+ + apply (rule_tac Q="\fault. valid_mdb and valid_objs and pspace_aligned + and pspace_distinct and not_idle_thread t and not_idle_thread thread and valid_idle and valid_irq_node and (\s. cur_thread s \ idle_thread s) - and tcb_at y and tcb_at thread - and st_tcb_at (\rv. rv = Structures_A.thread_state.BlockedOnSend word1 payload) y and valid_etcbs" + and tcb_at t and tcb_at thread + and st_tcb_at (\rv. rv = Structures_A.thread_state.BlockedOnSend ep payload) t and valid_etcbs" in hoare_strengthen_post[rotated]) - apply (clarsimp simp:not_idle_thread_def) - apply (clarsimp simp:st_tcb_at_def obj_at_def) - apply ((wp | clarsimp simp:not_idle_thread_def | wps )+)[1] - apply (frule_tac a = y and list = "y # ys" in pending_thread_in_send_not_idle) - apply (clarsimp simp:valid_state_def insertI)+ - apply (simp add:obj_at_def not_idle_thread_def)+ - apply (clarsimp simp:valid_state_def st_tcb_at_def obj_at_def valid_pspace_def) - apply (drule valid_objs_valid_ep_simp) - apply (simp add:is_ep_def) - apply (clarsimp simp: valid_ep_def a_type_def - split: Structures_A.endpoint.splits list.splits) - apply (clarsimp simp:valid_state_def valid_pspace_def a_type_def)+ + apply (clarsimp simp:not_idle_thread_def) + apply (clarsimp simp:st_tcb_at_def obj_at_def) + apply ((wp | clarsimp simp:not_idle_thread_def | wps )+)[1] + apply (frule_tac a = t and list = "t # ts" in pending_thread_in_send_not_idle) + apply (clarsimp simp:valid_state_def insertI)+ + apply (simp add:obj_at_def not_idle_thread_def)+ + apply (clarsimp simp:valid_state_def st_tcb_at_def obj_at_def valid_pspace_def) + apply (drule valid_objs_valid_ep_simp) + apply (simp add:is_ep_def) + apply (clarsimp simp:valid_ep_def valid_simple_obj_def a_type_def + split:Structures_A.endpoint.splits list.splits) + apply (clarsimp simp:valid_state_def valid_pspace_def valid_simple_obj_def a_type_def)+ apply (rule dcorres_to_wp[where Q=\,simplified]) apply (rule corres_dummy_set_sync_ep) (* RecvEP *) @@ -2509,10 +2515,11 @@ lemma recv_sync_ipc_corres: (ep_at epptr and not_idle_thread thread and (\s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) - (Endpoint_D.receive_ipc tcb_id_receiver ep_id ) + (Endpoint_D.receive_ipc tcb_id_receiver ep_id (Grant \ cap_rights ep_cap)) (Ipc_A.receive_ipc thread ep_cap is_blocking)" apply (clarsimp simp:corres_free_fail cap_ep_ptr_def Ipc_A.receive_ipc_def split:cap.splits Structures_A.endpoint.splits) + apply (rename_tac ep_badge ep_rights) apply (rule dcorres_expand_pfx) apply (rule_tac Q'="\ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr" in corres_symb_exec_r) apply (simp add:Endpoint_D.receive_ipc_def get_bound_notification_def thread_get_def gets_the_def gets_def bind_assoc) @@ -2591,6 +2598,34 @@ lemma dcorres_dummy_set_pending_cap_Restart: crunch pred_tcb[wp]: do_ipc_transfer "pred_tcb_at proj P t" (wp: crunch_wps transfer_caps_loop_pres make_fault_message_inv simp: zipWithM_x_mapM) +lemma dcorres_get_thread_state: + "dcorres (\op ts. op = infer_tcb_pending_op t ts) + \ + (valid_etcbs and tcb_at t and not_idle_thread t) + (do tcb <- get_thread t; return (the (cdl_tcb_caps tcb tcb_pending_op_slot)) od) + (get_thread_state t)" + text \Brute force proof. Trying to reuse @{thm thread_get_corres} doesn't + seem to work, because it expects to have concrete tcbs\ + apply (simp add: get_thread_state_def) + apply (monad_eq simp: corres_underlying_def Bex_def + get_thread_def opt_object_def + thread_get_def get_tcb_def + split: option.splits) + apply (rename_tac s ko tcb) + apply (case_tac ko; clarsimp) + text \These two existential vars refer to the same transformed tcb. + We skip the first one and instantiate the second first\ + apply (rule exI) + apply (rule conjI) + apply (rule_tac x="transform_tcb (machine_state s) t tcb (the (get_etcb t s))" in exI) + apply (monad_eq simp: transform_tcb_def) + apply (rule conjI) + apply (fastforce simp: get_etcb_def cdl_objects_tcb not_idle_thread_def + dest: valid_etcbs_tcb_etcb) + apply (rule refl) + apply (clarsimp simp: infer_tcb_pending_op_def tcb_slot_defs) + done + lemma send_sync_ipc_corres: "\ep_id = epptr;tcb_id_sender= thread\ \ dcorres dc @@ -2598,9 +2633,10 @@ lemma send_sync_ipc_corres: (not_idle_thread thread and (\s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) - (Endpoint_D.send_ipc block call badge can_grant tcb_id_sender ep_id) - (Ipc_A.send_ipc block call badge can_grant thread epptr)" - apply (clarsimp simp:gets_def Endpoint_D.send_ipc_def Ipc_A.send_ipc_def split del:if_split) + (Endpoint_D.send_ipc block call badge can_grant can_grant_reply tcb_id_sender ep_id) + (Ipc_A.send_ipc block call badge can_grant can_grant_reply thread epptr)" + apply (clarsimp simp:gets_def Endpoint_D.send_ipc_def Ipc_A.send_ipc_def + split del:if_split) apply (rule dcorres_absorb_get_l) apply (clarsimp split del:if_split) apply (rule_tac Q' = "\r. (=) s' and ko_at (kernel_object.Endpoint r) epptr" in corres_symb_exec_r[rotated]) @@ -2651,36 +2687,36 @@ lemma send_sync_ipc_corres: apply (subst when_def)+ apply (rule corres_guard_imp) apply (rule dcorres_symb_exec_r) - apply (rule corres_symb_exec_r) - apply (case_tac "recv_state"; simp add: corres_free_fail split del: if_split) - apply (rule corres_split[OF _ corres_complete_ipc_transfer]) - apply (rule corres_split[OF _ set_thread_state_corres]) - apply (rule dcorres_rhs_noop_above[OF possible_switch_to_dcorres]) - apply (rule_tac corres_symb_exec_r) - apply (rule dcorres_if_rhs) - apply (rule dcorres_if_rhs) - apply (simp only:if_True) - apply (rule corres_alternate1)+ - apply (rule corres_setup_caller_cap) - apply (clarsimp simp:ep_waiting_set_recv_def pred_tcb_at_def obj_at_def generates_pending_def) - apply (rule corres_alternate1[OF corres_alternate2]) - apply (rule set_thread_state_corres) - apply (rule corres_alternate2) - apply (rule corres_return_trivial ) - apply (clarsimp) - apply (rule_tac Q="\r. valid_mdb and valid_idle and valid_objs + apply (simp only: liftM_def) + apply (rule corres_split[OF _ dcorres_get_thread_state]) + apply (clarsimp, rename_tac recv_state') + apply (case_tac recv_state'; simp add: corres_free_fail split del: if_split) + apply (rule corres_split[OF _ corres_complete_ipc_transfer]) + apply (rule corres_split[OF _ set_thread_state_corres]) + apply (rule dcorres_rhs_noop_above[OF possible_switch_to_dcorres]) + apply (rule dcorres_if_rhs) + apply (rule dcorres_if_rhs) + apply (clarsimp simp only: if_True) + apply (rule corres_alternate1)+ + apply (rule corres_setup_caller_cap) + apply (clarsimp simp:ep_waiting_set_recv_def pred_tcb_at_def obj_at_def generates_pending_def) + apply (rule corres_alternate1[OF corres_alternate2]) + apply (rule set_thread_state_corres) + apply (rule corres_alternate2) + apply (rule corres_return_trivial) + apply wp + apply (rule_tac Q="\r. valid_mdb and valid_idle and valid_objs and not_idle_thread thread and not_idle_thread y and tcb_at thread and tcb_at y - and st_tcb_at runnable thread and valid_etcbs - " in hoare_strengthen_post[rotated]) - apply (clarsimp simp:pred_tcb_at_def obj_at_def, - simp split:Structures_A.thread_state.splits, fastforce) - apply ((wp sts_st_tcb_at' sts_st_tcb_at_neq |clarsimp simp add:not_idle_thread_def)+) + and st_tcb_at runnable thread and valid_etcbs" + in hoare_strengthen_post[rotated]) + apply (clarsimp simp:pred_tcb_at_def obj_at_def, + simp split:Structures_A.thread_state.splits, fastforce) + apply ((wp sts_st_tcb_at' sts_st_tcb_at_neq |clarsimp simp add:not_idle_thread_def)+) apply (wp hoare_vcg_conj_lift) apply (rule hoare_disjI1) apply (wp do_ipc_transfer_pred_tcb | wpc | simp)+ - apply (clarsimp simp:conj_comms not_idle_thread_def)+ - apply wp - apply (wp|wps)+ + apply (clarsimp simp:conj_comms not_idle_thread_def) + apply (wp | wps)+ apply (simp add:not_idle_thread_def) apply (clarsimp simp:ep_waiting_set_recv_def obj_at_def st_tcb_at_def)+ apply (frule_tac a = "y" and list = "y # ys" in pending_thread_in_recv_not_idle) diff --git a/proof/drefine/KHeap_DR.thy b/proof/drefine/KHeap_DR.thy index 8a7c10c25..e70c6e01a 100644 --- a/proof/drefine/KHeap_DR.thy +++ b/proof/drefine/KHeap_DR.thy @@ -1429,13 +1429,13 @@ lemma fast_finalise_not_idle_thread[wp]: lemma block_lift: "\kheap b word = Some (TCB tcb_type); ekheap b word = Some etcb; transform_tcb (machine_state b) word tcb_type etcb = Tcb cdl_tcb_type\ \ is_thread_blocked_on_endpoint cdl_tcb_type ep = (case tcb_state tcb_type of - Structures_A.thread_state.BlockedOnReceive p \ ep = p + Structures_A.thread_state.BlockedOnReceive p _ \ ep = p | Structures_A.thread_state.BlockedOnSend p _ \ ep = p | Structures_A.thread_state.BlockedOnNotification p \ ep = p | _ \ False)" apply (clarsimp simp:is_thread_blocked_on_endpoint_def transform_tcb_def infer_tcb_pending_op_def infer_tcb_bound_notification_def tcb_slots) apply (case_tac "tcb_state tcb_type") - apply (auto) + apply (auto) done (* Before we handle fast_finalise, we need sth form invs that can give us some preconditions of ep and ntfn *) @@ -1451,18 +1451,22 @@ where "ntfn_waiting_set epptr s \ definition none_is_waiting_ntfn :: "obj_ref \ 'z::state_ext state\bool" where "none_is_waiting_ntfn epptr s \ (ntfn_waiting_set epptr s) = {}" -definition ep_waiting_set_send :: "obj_ref\ 'z::state_ext state\obj_ref set" +definition ep_waiting_set_send :: "obj_ref \ 'z::state_ext state \ obj_ref set" where "ep_waiting_set_send epptr s \ - {tcb. \t payload. ((kheap s tcb) = Some (TCB t)) - \ ((tcb_state t) = Structures_A.thread_state.BlockedOnSend epptr payload)}" + {tcb. \t payload can_grant. + kheap s tcb = Some (TCB t) + \ tcb_state t = Structures_A.thread_state.BlockedOnSend epptr payload + \ can_grant = sender_can_grant payload}" definition none_is_sending_ep:: "obj_ref \ 'z::state_ext state \ bool" where "none_is_sending_ep epptr s \ (ep_waiting_set_send epptr s) = {}" -definition ep_waiting_set_recv :: "obj_ref\ 'z::state_ext state\obj_ref set" +definition ep_waiting_set_recv :: "obj_ref \ 'z::state_ext state \ obj_ref set" where "ep_waiting_set_recv epptr s \ - {tcb. \t. ((kheap s tcb) = Some (TCB t)) - \ ((tcb_state t) = Structures_A.thread_state.BlockedOnReceive epptr)}" + {tcb. \t payload can_grant. + kheap s tcb = Some (TCB t) + \ tcb_state t = Structures_A.thread_state.BlockedOnReceive epptr payload + \ can_grant = receiver_can_grant payload}" definition none_is_receiving_ep:: "obj_ref \ 'z::state_ext state \ bool" where "none_is_receiving_ep epptr s \ (ep_waiting_set_recv epptr s) = {}" @@ -1593,25 +1597,27 @@ lemma ntfn_not_waiting_ep_send: "\ valid_objs s;kheap s epptr = Some (kernel_object.Notification ntfn) \ \ ep_waiting_set_send epptr s = {}" apply (rule set_eqI) - apply (clarsimp simp:ep_waiting_set_send_def) - apply (simp add:valid_objs_def) - apply (drule_tac x= x in bspec) - apply (clarsimp simp:dom_def) - apply (clarsimp simp:valid_obj_def valid_tcb_def valid_tcb_state_def obj_at_def is_ep_def - split:Structures_A.kernel_object.splits) -done + apply (clarsimp simp: ep_waiting_set_send_def) + apply (simp add: valid_objs_def) + apply (rename_tac ptr t payload) + apply (drule_tac x=ptr in bspec) + apply (clarsimp simp: dom_def) + apply (clarsimp simp: valid_obj_def valid_tcb_def valid_tcb_state_def obj_at_def is_ep_def + split: Structures_A.kernel_object.splits) + done lemma ntfn_not_waiting_ep_recv: "\ valid_objs s;kheap s epptr = Some (kernel_object.Notification ntfn) \ \ ep_waiting_set_recv epptr s = {}" - apply (rule set_eqI) - apply (clarsimp simp:ep_waiting_set_recv_def) - apply (simp add:valid_objs_def) - apply (drule_tac x= x in bspec) - apply (clarsimp simp:dom_def) - apply (clarsimp simp:valid_obj_def valid_tcb_def valid_tcb_state_def obj_at_def is_ep_def - split:Structures_A.kernel_object.splits) -done + apply (rule set_eqI) + apply (clarsimp simp: ep_waiting_set_recv_def) + apply (simp add: valid_objs_def) + apply (rename_tac ptr t payload) + apply (drule_tac x=ptr in bspec) + apply (clarsimp simp: dom_def) + apply (clarsimp simp: valid_obj_def valid_tcb_def valid_tcb_state_def obj_at_def is_ep_def + split: Structures_A.kernel_object.splits) + done lemma ep_not_waiting_ntfn: "\ valid_objs s;kheap s epptr = Some (kernel_object.Endpoint ep) \ @@ -1624,7 +1630,6 @@ lemma ep_not_waiting_ntfn: by (clarsimp simp:valid_obj_def valid_tcb_def valid_tcb_state_def obj_at_def is_ntfn_def split:Structures_A.kernel_object.splits) - (* Following 2 lemmas is useful, it tells us that under certain condition, we can get valid_ep and valid_ntfn, which helps us ruling out the idle thread and constract a map between the waiting list and waiting set *) @@ -1638,11 +1643,13 @@ lemma get_endpoint_pick: apply (rule conjI) apply (rule set_eqI) apply (clarsimp simp:ep_waiting_set_send_def) - apply (drule_tac x=x in spec) + apply (rename_tac ptr t payload) + apply (drule_tac x=ptr in spec) apply (clarsimp simp: state_refs_of_def) apply (rule set_eqI) apply (clarsimp simp:ep_waiting_set_recv_def) - apply (drule_tac x=x in spec) + apply (rename_tac ptr t payload) + apply (drule_tac x=ptr in spec) apply (clarsimp simp:state_refs_of_def) apply (clarsimp simp:valid_state_def valid_pspace_def valid_objs_def) apply (drule_tac x=epptr in bspec) @@ -1652,7 +1659,8 @@ lemma get_endpoint_pick: apply (rule sym) apply (rule antisym) apply (clarsimp simp:ep_waiting_set_send_def sym_refs_def) - apply (drule_tac x = x in spec) + apply (rename_tac ptr t payload) + apply (drule_tac x=ptr in spec) apply (clarsimp simp:state_refs_of_def) apply (clarsimp simp:ep_waiting_set_send_def sym_refs_def) apply (drule_tac x= epptr in spec) @@ -1663,7 +1671,7 @@ lemma get_endpoint_pick: apply (case_tac y) apply (clarsimp simp:refs_of_def tcb_st_refs_of_def ep_q_refs_of_def ntfn_q_refs_of_def split:Structures_A.kernel_object.splits)+ - apply (clarsimp simp:tcb_bound_refs_def2 split:Structures_A.thread_state.splits) + apply (force simp:tcb_bound_refs_def2 split:Structures_A.thread_state.splits) apply (clarsimp simp:ep_waiting_set_send_def) apply (clarsimp simp:refs_of_def tcb_st_refs_of_def ep_q_refs_of_def ntfn_q_refs_of_def split:Structures_A.kernel_object.splits)+ @@ -1677,7 +1685,8 @@ lemma get_endpoint_pick: apply (clarsimp simp:none_is_receiving_ep_def) apply (rule set_eqI) apply (clarsimp simp: ep_waiting_set_recv_def sym_refs_def) - apply (drule_tac x = x in spec) + apply (rename_tac ptr t payload) + apply (drule_tac x = ptr in spec) apply (clarsimp simp:state_refs_of_def) apply clarsimp defer @@ -1689,7 +1698,8 @@ lemma get_endpoint_pick: apply (rule sym) apply (rule antisym) apply (clarsimp simp:ep_waiting_set_recv_def sym_refs_def) - apply (drule_tac x = x in spec) + apply (rename_tac ptr t payload) + apply (drule_tac x = ptr in spec) apply (clarsimp simp:state_refs_of_def) apply (clarsimp simp:ep_waiting_set_recv_def sym_refs_def) apply (drule_tac x= epptr in spec) @@ -1700,7 +1710,7 @@ lemma get_endpoint_pick: apply (case_tac y) apply (clarsimp simp:refs_of_def tcb_st_refs_of_def ep_q_refs_of_def ntfn_q_refs_of_def split:Structures_A.kernel_object.splits)+ - apply (clarsimp simp: tcb_bound_refs_def2 split:Structures_A.thread_state.splits) + apply (force simp: tcb_bound_refs_def2 split:Structures_A.thread_state.splits) apply (clarsimp simp:ep_waiting_set_recv_def) apply (clarsimp simp:refs_of_def tcb_st_refs_of_def ep_q_refs_of_def ntfn_q_refs_of_def split:Structures_A.kernel_object.splits)+ @@ -1714,7 +1724,8 @@ lemma get_endpoint_pick: apply (clarsimp simp:none_is_sending_ep_def) apply (rule set_eqI) apply (clarsimp simp: ep_waiting_set_send_def sym_refs_def) - apply (drule_tac x = x in spec) + apply (rename_tac ptr t payload) + apply (drule_tac x = ptr in spec) apply (clarsimp simp:state_refs_of_def) apply (rename_tac list) apply clarsimp @@ -1937,12 +1948,12 @@ lemma is_thread_blocked_on_sth: = (get_waiting_sync_recv_threads ep s) \ (get_waiting_sync_send_threads ep s) \ (get_waiting_ntfn_recv_threads ep s)" apply (rule set_eqI) apply (rule iffI) - apply (clarsimp simp:is_thread_blocked_on_endpoint_def split:option.splits) - apply (case_tac y) - apply (simp_all add: get_waiting_sync_recv_threads_def get_waiting_sync_send_threads_def get_waiting_ntfn_recv_threads_def) - apply safe - apply (clarsimp simp:is_thread_blocked_on_endpoint_def)+ -done + apply (clarsimp simp: is_thread_blocked_on_endpoint_def split: option.splits) + apply (case_tac y; simp add: get_waiting_sync_recv_threads_def get_waiting_sync_send_threads_def + get_waiting_ntfn_recv_threads_def) + apply (fastforce simp: is_thread_blocked_on_endpoint_def get_waiting_sync_recv_threads_def + get_waiting_sync_send_threads_def get_waiting_ntfn_recv_threads_def) + done lemma set_ep_exec_wp: (* generalise? *) "\(=) s\ set_endpoint epptr ep \\r s'. s' = update_kheap ((kheap s)(epptr \ Endpoint ep)) s\ " diff --git a/proof/drefine/StateTranslation_D.thy b/proof/drefine/StateTranslation_D.thy index 4fde4f4cb..88cd74ff2 100644 --- a/proof/drefine/StateTranslation_D.thy +++ b/proof/drefine/StateTranslation_D.thy @@ -542,17 +542,17 @@ lemma transform_intent_isnot_TcbIntent: (label \ TCBUnbindNotification) \ (label \ TCBSetTLSBase))" apply(rule iffI) - apply(erule contrapos_np) - apply(clarsimp simp: transform_intent_def) - apply(case_labels label) - apply(simp_all) - apply(fastforce simp: transform_intent_tcb_defs - option_map_def - split: list.split)+ + subgoal + apply(erule contrapos_np) + apply(clarsimp simp: transform_intent_def) + apply(case_labels label; simp) + apply(fastforce simp: transform_intent_tcb_defs option_map_def + split: list.split)+ + done apply(unfold transform_intent_def) apply(case_labels label, simp_all add: option_map_def split: option.split) - apply (auto simp: transform_intent_tcb_defs - split: list.splits arch_invocation_label.splits) + apply(auto simp: transform_intent_tcb_defs + split: list.splits arch_invocation_label.splits) done (* @@ -622,8 +622,8 @@ where Types_D.EndpointCap ptr badge cap_rights_ | Structures_A.NotificationCap ptr badge cap_rights_ \ Types_D.NotificationCap ptr badge cap_rights_ - | Structures_A.ReplyCap ptr is_master \ - if is_master then Types_D.MasterReplyCap ptr else Types_D.ReplyCap ptr + | Structures_A.ReplyCap ptr is_master cap_rights_ \ + if is_master then Types_D.MasterReplyCap ptr else Types_D.ReplyCap ptr cap_rights_ | Structures_A.CNodeCap ptr size_bits guard \ Types_D.CNodeCap ptr (of_bl guard) (length guard) size_bits | Structures_A.ThreadCap ptr \ @@ -707,16 +707,17 @@ definition where "infer_tcb_pending_op ptr t \ case t of - Structures_A.BlockedOnReceive ptr \ - PendingSyncRecvCap ptr False + Structures_A.BlockedOnReceive ptr payload \ + PendingSyncRecvCap ptr False (receiver_can_grant payload) - |Structures_A.BlockedOnReply \ - PendingSyncRecvCap ptr True + | Structures_A.BlockedOnReply \ + PendingSyncRecvCap ptr True False | Structures_A.BlockedOnSend ptr payload \ PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) - (sender_can_grant payload) False + (sender_can_grant payload) (sender_can_grant_reply payload) + False | Structures_A.BlockedOnNotification ptr \ PendingNtfnRecvCap ptr diff --git a/proof/drefine/Syscall_DR.thy b/proof/drefine/Syscall_DR.thy index 8daed895c..46ab281aa 100644 --- a/proof/drefine/Syscall_DR.thy +++ b/proof/drefine/Syscall_DR.thy @@ -30,15 +30,15 @@ where Invocations_A.InvokeUntyped iu \ Invocations_D.InvokeUntyped $ translate_untyped_invocation iu - | Invocations_A.InvokeEndpoint ep bdg grant \ + | Invocations_A.InvokeEndpoint ep bdg grant grant_reply \ Invocations_D.InvokeEndpoint $ - SyncMessage bdg grant ep + SyncMessage bdg grant grant_reply ep | Invocations_A.InvokeNotification ntfn aebdg \ Invocations_D.InvokeNotification $ Signal aebdg ntfn - | Invocations_A.InvokeReply target_tcb reply_slot \ + | Invocations_A.InvokeReply target_tcb reply_slot grant \ Invocations_D.InvokeReply $ - ReplyMessage target_tcb (transform_cslot_ptr reply_slot) + ReplyMessage target_tcb (transform_cslot_ptr reply_slot) grant | Invocations_A.InvokeCNode icn \ Invocations_D.InvokeCNode $ translate_cnode_invocation icn @@ -150,7 +150,7 @@ lemma decode_invocation_replycap_corres: invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = transform_cap invoked_cap'; excaps = transform_cap_list excaps'; - invoked_cap' = cap.ReplyCap a b \ \ + invoked_cap' = cap.ReplyCap a b c \ \ dcorres (dc \ cdl_invocation_relation) \ (cte_wp_at (Not\ is_master_reply_cap) invoked_cap_ref' and cte_wp_at (diminished invoked_cap') invoked_cap_ref') (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')" @@ -702,7 +702,7 @@ lemma perform_invocation_corres: apply (wp | clarsimp)+ (* invoke_reply *) - apply (rename_tac word a b) + apply (rename_tac word a b c) apply (clarsimp simp:invoke_reply_def) apply (rule corres_guard_imp) apply (rule corres_split[OF _ get_cur_thread_corres]) @@ -718,7 +718,7 @@ lemma perform_invocation_corres: apply clarsimp apply (drule (1) valid_reply_capsD) apply (clarsimp simp: valid_idle_def not_idle_thread_def pred_tcb_at_def obj_at_def) - apply (fastforce simp: has_reply_cap_def) + apply (fastforce simp: has_reply_cap_def is_reply_cap_to_def) (* invoke_tcb *) apply (rule corres_guard_imp) @@ -1355,6 +1355,7 @@ crunch cur_thread[wp]: complete_signal "\s. P (cur_thread s)" lemma receive_ipc_cur_thread: notes do_nbrecv_failed_transfer_def[simp] + if_split[split del] shows " \\s. valid_objs s \ P (cur_thread (s :: det_ext state))\ receive_ipc a b c \\xg s. P (cur_thread s)\" apply (simp add:receive_ipc_def bind_assoc) @@ -1362,11 +1363,8 @@ lemma receive_ipc_cur_thread: apply (simp add:setup_caller_cap_def) apply (wp dxo_wp_weak | simp)+ apply (rule_tac Q="\r s. P (cur_thread s)" in hoare_strengthen_post) - apply wp apply clarsimp apply (wp|wpc)+ - apply (rule_tac Q="\r s. P (cur_thread s)" in hoare_strengthen_post) - apply wp apply clarsimp apply (clarsimp simp:neq_Nil_conv) apply (rename_tac list queue sender) @@ -1419,7 +1417,8 @@ lemma handle_recv_corres: apply (rule corres_alternate1) apply clarsimp apply (rule corres_split[where r'=dc]) - apply (rule_tac epptr=word1 in recv_sync_ipc_corres) + apply (rule_tac epptr=word1 in recv_sync_ipc_corres + [where ep_cap="cap.EndpointCap _ _ _", simplified]) apply (simp add: cap_ep_ptr_def delete_caller_cap_def)+ apply (simp add: transform_tcb_slot_simp[symmetric]) apply (rule delete_cap_simple_corres) @@ -1495,7 +1494,7 @@ lemma handle_reply_corres: in corres_split [OF _ get_cap_corres]) apply (simp add: transform_cap_def corres_fail split: cap.split) apply (clarsimp simp: corres_fail dc_def[symmetric] split: bool.split) - apply (rename_tac word) + apply (rename_tac word rights) apply (rule corres_guard_imp) apply (rule do_reply_transfer_corres) apply (simp add: transform_tcb_slot_simp) @@ -1505,8 +1504,10 @@ lemma handle_reply_corres: apply (clarsimp simp:cte_wp_at_caps_of_state) apply (simp add:valid_cap_def)+ apply (clarsimp simp:valid_state_def invs_def valid_reply_caps_def dest!:has_reply_cap_cte_wpD) - apply (drule_tac x = word in spec,simp) - apply (clarsimp simp:not_idle_thread_def pred_tcb_at_def obj_at_def valid_idle_def) + apply (drule_tac x = word in spec, simp add: cte_wp_at_def) + apply (clarsimp simp:not_idle_thread_def pred_tcb_at_def obj_at_def valid_idle_def + cte_wp_at_def has_reply_cap_def is_reply_cap_to_def) + apply blast apply (clarsimp simp: transform_tcb_slot_simp|(wp get_cap_wp)+)+ apply (clarsimp simp:ct_in_state_def invs_def valid_state_def pred_tcb_at_def tcb_at_def obj_at_def) done diff --git a/proof/drefine/Tcb_DR.thy b/proof/drefine/Tcb_DR.thy index dd06e9349..0fee8e7cb 100644 --- a/proof/drefine/Tcb_DR.thy +++ b/proof/drefine/Tcb_DR.thy @@ -481,10 +481,11 @@ lemma dcorres_setup_reply_master: apply (rule TrueI) apply (clarsimp simp: not_idle_thread_def) apply (clarsimp simp:when_def is_master_reply_cap_def split:cap.split_asm) + apply (rename_tac rc_rights) apply (subgoal_tac "opt_cap (obj_id,tcb_replycap_slot) (transform s') = Some (cdl_cap.MasterReplyCap obj_id)") apply (clarsimp simp:corres_underlying_def set_cap_is_noop_opt_cap return_def) - apply (subgoal_tac "cte_wp_at ((=) (cap.ReplyCap obj_id True)) + apply (subgoal_tac "cte_wp_at ((=) (cap.ReplyCap obj_id True rc_rights)) (obj_id,tcb_cnode_index 2) s'") apply (clarsimp dest!:iffD1[OF cte_wp_at_caps_of_state]) apply (drule caps_of_state_transform_opt_cap) diff --git a/spec/capDL/CSpace_D.thy b/spec/capDL/CSpace_D.thy index eb82c29d2..e39a2ebda 100644 --- a/spec/capDL/CSpace_D.thy +++ b/spec/capDL/CSpace_D.thy @@ -151,12 +151,12 @@ definition where "cancel_ipc ptr \ do cap \ KHeap_D.get_cap (ptr,tcb_pending_op_slot); (case cap of - PendingSyncRecvCap _ is_reply \ ( do + PendingSyncRecvCap _ is_reply _ \ ( do when is_reply $ update_thread_fault ptr (\x. False); revoke_cap_simple (ptr,tcb_replycap_slot); when (\ is_reply) $ set_cap (ptr,tcb_pending_op_slot) NullCap od ) - | PendingSyncSendCap _ _ _ _ _ \ (do + | PendingSyncSendCap _ _ _ _ _ _ \ (do revoke_cap_simple (ptr,tcb_replycap_slot); set_cap (ptr,tcb_pending_op_slot) NullCap od) @@ -188,7 +188,7 @@ where unbind_maybe_notification r; cancel_all_ipc r od)" -| "finalise_cap (ReplyCap r) final = return (NullCap, NullCap)" +| "finalise_cap (ReplyCap r R) final = return (NullCap, NullCap)" | "finalise_cap (MasterReplyCap r) final = return (NullCap, NullCap)" | "finalise_cap (CNodeCap r bits g sz) final = (return (if final then ZombieCap r else NullCap, NullCap))" @@ -200,8 +200,8 @@ where prepare_thread_delete r od); return (if final then (ZombieCap r) else NullCap, NullCap) od)" -| "finalise_cap (PendingSyncSendCap r _ _ _ _) final = return (NullCap, NullCap)" -| "finalise_cap (PendingSyncRecvCap r _ ) final = return (NullCap, NullCap)" +| "finalise_cap (PendingSyncSendCap r _ _ _ _ _) final = return (NullCap, NullCap)" +| "finalise_cap (PendingSyncRecvCap r _ _) final = return (NullCap, NullCap)" | "finalise_cap (PendingNtfnRecvCap r) final = return (NullCap, NullCap)" | "finalise_cap IrqControlCap final = return (NullCap, NullCap)" | "finalise_cap (IrqHandlerCap irq) final = ( @@ -436,7 +436,7 @@ definition where "get_tcb_ep_badge t \ case (cdl_tcb_caps t tcb_pending_op_slot) of - Some (PendingSyncSendCap _ badge _ _ _) \ Some badge + Some (PendingSyncSendCap _ badge _ _ _ _) \ Some badge | _ \ None" (* @@ -658,7 +658,7 @@ definition where "derive_cap slot cap \ case cap of UntypedCap _ _ _ \ doE ensure_no_children slot; returnOk cap odE - | ReplyCap _ \ returnOk NullCap + | ReplyCap _ _ \ returnOk NullCap | MasterReplyCap oref \ returnOk NullCap | IrqControlCap \ returnOk NullCap | ZombieCap _ \ returnOk NullCap diff --git a/spec/capDL/Decode_D.thy b/spec/capDL/Decode_D.thy index cebe47f82..f751a1b1c 100644 --- a/spec/capDL/Decode_D.thy +++ b/spec/capDL/Decode_D.thy @@ -120,7 +120,7 @@ where * regardless of the user's actual intent. *) EndpointCap o_id badge rights \ (if Write \ rights then - returnOk $ InvokeEndpoint (SyncMessage badge (Grant \ rights) o_id) + returnOk $ InvokeEndpoint (SyncMessage badge (Grant \ rights) (GrantReply \ rights) o_id) else throw) | NotificationCap o_id badge rights \ @@ -128,8 +128,8 @@ where returnOk $ InvokeNotification (Signal badge o_id) else throw) - | ReplyCap o_id\ - returnOk $ InvokeReply (ReplyMessage o_id invoked_cap_ref) + | ReplyCap o_id rights \ + returnOk $ InvokeReply (ReplyMessage o_id invoked_cap_ref (Grant \ rights)) (* * For other operations, we only perform the user's intent diff --git a/spec/capDL/Endpoint_D.thy b/spec/capDL/Endpoint_D.thy index 950a3eb81..dcd634ae0 100644 --- a/spec/capDL/Endpoint_D.thy +++ b/spec/capDL/Endpoint_D.thy @@ -18,11 +18,14 @@ begin (* Inject the reply cap into the target TCB *) definition - inject_reply_cap :: "cdl_object_id \ cdl_object_id \ unit k_monad" + inject_reply_cap :: "cdl_object_id \ cdl_object_id \ bool \ unit k_monad" where - "inject_reply_cap src_tcb_id dst_tcb_id \ do - set_cap (src_tcb_id,tcb_pending_op_slot) $ cdl_cap.PendingSyncRecvCap src_tcb_id True; - insert_cap_child (ReplyCap src_tcb_id) (src_tcb_id, tcb_replycap_slot) (dst_tcb_id, tcb_caller_slot); + "inject_reply_cap src_tcb_id dst_tcb_id can_grant \ do + set_cap (src_tcb_id, tcb_pending_op_slot) $ + cdl_cap.PendingSyncRecvCap src_tcb_id True False; + insert_cap_child (ReplyCap src_tcb_id (if can_grant then {Grant, Write} else {Write})) + (src_tcb_id, tcb_replycap_slot) + (dst_tcb_id, tcb_caller_slot); return () od" @@ -189,19 +192,19 @@ definition get_waiting_sync_recv_threads :: "cdl_object_id \ cdl_state \ cdl_object_id set" where "get_waiting_sync_recv_threads target state \ - { x. \a. (cdl_objects state) x = Some (Tcb a) \ - (((cdl_tcb_caps a) tcb_pending_op_slot) = Some (PendingSyncRecvCap target False)) }" + {x. \a. (cdl_objects state) x = Some (Tcb a) \ + (\can_grant. (cdl_tcb_caps a) tcb_pending_op_slot = Some (PendingSyncRecvCap target False can_grant)) }" (* * Get the set of threads waiting to send to the given sync endpoint. - * Return a tuple of (thread, is_call, can_grant). *) definition get_waiting_sync_send_threads :: "cdl_object_id \ cdl_state \ cdl_object_id set" where "get_waiting_sync_send_threads target state \ - {x. \ rights grant call a b. (cdl_objects state) x = Some (Tcb a) \ - (((cdl_tcb_caps a) tcb_pending_op_slot) = Some (PendingSyncSendCap target b call grant rights)) }" + {t. \fault a b. (cdl_objects state) t = Some (Tcb a) \ + (\call can_grant can_grant_reply. (cdl_tcb_caps a) tcb_pending_op_slot = + Some (PendingSyncSendCap target b call can_grant can_grant_reply fault)) }" (* * Get the set of threads which are bound to the given ntfn, but are @@ -212,8 +215,8 @@ definition where "get_waiting_sync_bound_ntfn_threads ntfn_id state \ {x. \a ep_id. (cdl_objects state) x = Some (Tcb a) \ - (((cdl_tcb_caps a) tcb_pending_op_slot) = Some (PendingSyncRecvCap ep_id False)) \ - (((cdl_tcb_caps a) tcb_boundntfn_slot) = Some (BoundNotificationCap ntfn_id))}" + (\can_grant. (cdl_tcb_caps a) tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \ + ((cdl_tcb_caps a) tcb_boundntfn_slot = Some (BoundNotificationCap ntfn_id))}" (* * Mark a thread blocked on IPC. @@ -264,30 +267,26 @@ where (* * Transfer a message from "sender" to "receiver" using a reply capability. * - * A reply capability always gives the sender the right to grant caps - * over the channel. As the original sender must have had grant rights - * to establish the reply cap to begin with (and hence could have - * granted the other side a return communication path), this does not - * increase any rights. + * The sender may have the right to grant caps over the channel. * * If a fault is pending in the receiver, the fault is transferred. *) definition - do_reply_transfer :: "cdl_object_id \ cdl_object_id \ cdl_cap_ref \ unit k_monad" + do_reply_transfer :: "cdl_object_id \ cdl_object_id \ cdl_cap_ref \ bool \ unit k_monad" where - "do_reply_transfer sender_id receiver_id reply_cap_slot \ + "do_reply_transfer sender_id receiver_id reply_cap_slot can_grant \ do has_fault \ get_thread_fault receiver_id; - when (\ has_fault) $ do_ipc_transfer None sender_id receiver_id True; + when (\ has_fault) $ do_ipc_transfer None sender_id receiver_id can_grant; (* Clear out any pending operation caps. *) delete_cap_simple reply_cap_slot; when (has_fault) $ (do corrupt_tcb_intent receiver_id; update_thread_fault receiver_id (\_. False) od ); - if ( \ has_fault) then set_cap (receiver_id,tcb_pending_op_slot) RunningCap + if ( \ has_fault) then set_cap (receiver_id, tcb_pending_op_slot) RunningCap else (set_cap (receiver_id,tcb_pending_op_slot) NullCap - \ set_cap (receiver_id,tcb_pending_op_slot) RestartCap ) + \ set_cap (receiver_id,tcb_pending_op_slot) RestartCap) od" (* Wake-up a thread waiting on an notification. *) @@ -349,9 +348,9 @@ where * them up. Otherwise, we put the sender to sleep. *) definition - send_ipc :: "bool \ bool \ cdl_badge \ bool \ cdl_object_id \ cdl_object_id \ unit k_monad" + send_ipc :: "bool \ bool \ cdl_badge \ bool \ bool \ cdl_object_id \ cdl_object_id \ unit k_monad" where - "send_ipc block call badge can_grant tcb_id_sender ep_id \ + "send_ipc block call badge can_grant can_grant_reply tcb_id_sender ep_id \ do waiters \ gets $ get_waiting_sync_recv_threads ep_id; t \ option_select waiters; @@ -359,14 +358,23 @@ where None \ if block then block_thread_on_ipc tcb_id_sender - (PendingSyncSendCap ep_id badge call can_grant False) + (PendingSyncSendCap ep_id badge call can_grant can_grant_reply False) else return () | Some tcb_id_receiver \ do - do_ipc_transfer (Some ep_id) tcb_id_sender tcb_id_receiver can_grant; + \ \liftM instead of bind+return avoids early unfolding in send_ipc_corres\ + recv_state \ liftM (\tcb. the (cdl_tcb_caps tcb tcb_pending_op_slot)) $ + get_thread tcb_id_receiver; + reply_can_grant \ + (case recv_state of + PendingSyncRecvCap target False receiver_grant \ do + do_ipc_transfer (Some ep_id) tcb_id_sender tcb_id_receiver can_grant; + return receiver_grant od + | _ \ fail); set_cap (tcb_id_receiver,tcb_pending_op_slot) RunningCap; - (when (can_grant) $ (inject_reply_cap tcb_id_sender tcb_id_receiver)) \ - set_cap (tcb_id_sender,tcb_pending_op_slot) NullCap \ return () + (when (can_grant \ can_grant_reply) $ + (inject_reply_cap tcb_id_sender tcb_id_receiver reply_can_grant)) + \ set_cap (tcb_id_sender,tcb_pending_op_slot) NullCap \ return () od od" @@ -375,24 +383,25 @@ where * wake them up. Otherwise, we put the receiver to sleep. *) definition - receive_sync :: "cdl_object_id \ cdl_object_id \ unit k_monad" + receive_sync :: "cdl_object_id \ cdl_object_id \ bool \ unit k_monad" where - "receive_sync thread ep_id \ do + "receive_sync thread ep_id receiver_can_grant \ do waiters \ gets $ get_waiting_sync_send_threads ep_id; - t \ option_select waiters; - (case t of + waiter \ option_select waiters; + (case waiter of None \ - block_thread_on_ipc thread (PendingSyncRecvCap ep_id False) \ corrupt_tcb_intent thread + block_thread_on_ipc thread (PendingSyncRecvCap ep_id False receiver_can_grant) + \ corrupt_tcb_intent thread | Some tcb_id_sender \ (do tcb \ get_thread tcb_id_sender; case ((cdl_tcb_caps tcb) tcb_pending_op_slot) of - Some (PendingSyncSendCap target _ call grant rights)\(do - do_ipc_transfer (Some ep_id) tcb_id_sender thread grant; - (when (grant) $ (inject_reply_cap tcb_id_sender thread)) \ - set_cap (tcb_id_sender,tcb_pending_op_slot) RunningCap \ + Some (PendingSyncSendCap target _ call can_grant can_grant_reply fault) \ (do + do_ipc_transfer (Some ep_id) tcb_id_sender thread can_grant; + (when (can_grant \ can_grant_reply) $ + (inject_reply_cap tcb_id_sender thread receiver_can_grant)) \ + set_cap (tcb_id_sender, tcb_pending_op_slot) RunningCap \ set_cap (tcb_id_sender, tcb_pending_op_slot) NullCap od) - od) ) od" @@ -400,17 +409,17 @@ where (* This is more nonderministic than is really required, but it makes the refinement proofs much easier *) definition - receive_ipc :: "cdl_object_id \ cdl_object_id \ unit k_monad" + receive_ipc :: "cdl_object_id \ cdl_object_id \ bool \ unit k_monad" where - "receive_ipc thread ep_id \ corrupt_tcb_intent thread \ receive_sync thread ep_id" + "receive_ipc thread ep_id can_grant \ corrupt_tcb_intent thread \ receive_sync thread ep_id can_grant" definition invoke_endpoint :: "bool \ bool \ cdl_endpoint_invocation \ unit k_monad" where "invoke_endpoint is_call can_block params \ case params of - SyncMessage badge can_grant ep_id \ do + SyncMessage badge can_grant can_grant_reply ep_id \ do thread \ gets_the cdl_current_thread; - send_ipc can_block is_call badge can_grant thread ep_id + send_ipc can_block is_call badge can_grant can_grant_reply thread ep_id od" definition @@ -424,9 +433,9 @@ definition invoke_reply :: "cdl_reply_invocation \ unit k_monad" where "invoke_reply params \ case params of - ReplyMessage recv reply_cap_ref \ do + ReplyMessage recv reply_cap_ref rights \ do send \ gets_the cdl_current_thread; - do_reply_transfer send recv reply_cap_ref + do_reply_transfer send recv reply_cap_ref rights od" @@ -444,10 +453,10 @@ definition handler_cap \ lookup_cap tcb_id target_ep_cptr; (case handler_cap of EndpointCap ref badge rights \ - if Write \ rights \ Grant \ rights then + if Write \ rights \ (Grant \ rights \ GrantReply \ rights) then liftE $ do update_thread_fault tcb_id (\_. True); - send_ipc True False badge True tcb_id ref + send_ipc True True badge (Grant \ rights) True tcb_id ref od else throw diff --git a/spec/capDL/Intents_D.thy b/spec/capDL/Intents_D.thy index a76baa0af..4982470a4 100644 --- a/spec/capDL/Intents_D.thy +++ b/spec/capDL/Intents_D.thy @@ -50,6 +50,9 @@ abbreviation (input) Write::rights abbreviation (input) Grant::rights where "Grant \ AllowGrant" +abbreviation (input) GrantReply::rights + where "GrantReply \ AllowGrantReply" + (* Capability data, such as guard information. *) type_synonym cdl_raw_capdata = word32 @@ -183,6 +186,7 @@ datatype cdl_asid_pool_intent = datatype cdl_notification_intent = SendSignalIntent word32 +(* Also used with reply caps *) datatype cdl_endpoint_intent = SendMessageIntent "cdl_cptr list" diff --git a/spec/capDL/Invocations_D.thy b/spec/capDL/Invocations_D.thy index bd73df4ed..686981874 100644 --- a/spec/capDL/Invocations_D.thy +++ b/spec/capDL/Invocations_D.thy @@ -52,17 +52,17 @@ datatype cdl_irq_handler_invocation = | ClearIrqHandler cdl_irq datatype cdl_endpoint_invocation = - (* badge, grant, ep *) - (* Invoking an endpoint is always a blocking, non-call operation, - * so we need not track the "block" or "call" bits. *) - SyncMessage cdl_badge bool cdl_object_id + (* We need not track the "block" or "call" bits because they + are handled separately in the top-level syscall interface. *) + (* badge, grant, grant reply, ep *) + SyncMessage cdl_badge bool bool cdl_object_id datatype cdl_notification_invocation = (* badge (notification word) and notification object *) Signal cdl_badge cdl_object_id datatype cdl_reply_invocation = - ReplyMessage cdl_object_id cdl_cap_ref + ReplyMessage cdl_object_id cdl_cap_ref bool (* can grant *) datatype cdl_page_table_invocation = (* PageTableMap *) diff --git a/spec/capDL/PageTableUnmap_D.thy b/spec/capDL/PageTableUnmap_D.thy index 3a7f7c7ee..1239d4f7e 100644 --- a/spec/capDL/PageTableUnmap_D.thy +++ b/spec/capDL/PageTableUnmap_D.thy @@ -41,8 +41,8 @@ definition where "is_thread_blocked_on_endpoint t ep \ case (cdl_tcb_caps t tcb_pending_op_slot) of - Some (PendingSyncSendCap p _ _ _ _) \ p = ep - | Some (PendingSyncRecvCap p is_reply ) \ p = ep \ \ is_reply + Some (PendingSyncSendCap p _ _ _ _ _) \ p = ep + | Some (PendingSyncRecvCap p is_reply _) \ p = ep \ \ is_reply | Some (PendingNtfnRecvCap p) \ p = ep | _ \ False" @@ -113,15 +113,15 @@ where definition can_fast_finalise :: "cdl_cap \ bool" where - "can_fast_finalise cap \ case cap of ReplyCap r \ True + "can_fast_finalise cap \ case cap of ReplyCap r R \ True | MasterReplyCap r \ True | EndpointCap r b R \ True | NotificationCap r b R \ True | NullCap \ True | RestartCap \ True | RunningCap \ True - | PendingSyncSendCap r _ _ _ _ \ True - | PendingSyncRecvCap r _ \ True + | PendingSyncSendCap r _ _ _ _ _ \ True + | PendingSyncRecvCap r _ _ \ True | PendingNtfnRecvCap r \ True | DomainCap \ True | PageDirectoryCap _ x _ \ \(x = Real) @@ -139,7 +139,7 @@ where "fast_finalise NullCap final = return ()" | "fast_finalise (RestartCap) final = return ()" | "fast_finalise (RunningCap) final = return ()" -| "fast_finalise (ReplyCap r) final = return ()" +| "fast_finalise (ReplyCap r R) final = return ()" | "fast_finalise (MasterReplyCap r) final = return ()" | "fast_finalise (EndpointCap r b R) final = (when final $ cancel_all_ipc r)" @@ -148,8 +148,8 @@ where unbind_maybe_notification r; cancel_all_ipc r od)" -| "fast_finalise (PendingSyncSendCap r _ _ _ _) final = return()" -| "fast_finalise (PendingSyncRecvCap r _) final = return()" +| "fast_finalise (PendingSyncSendCap r _ _ _ _ _) final = return()" +| "fast_finalise (PendingSyncRecvCap r _ _) final = return()" | "fast_finalise (PendingNtfnRecvCap r) final = return()" | "fast_finalise DomainCap final = return ()" | "fast_finalise (PageDirectoryCap _ x _) _ = (if x = Real then fail else return())" @@ -165,12 +165,12 @@ definition "cap_counts cap \ (case cap of cdl_cap.NullCap \ False | UntypedCap _ _ _ \ False - | ReplyCap _ \ False + | ReplyCap _ _ \ False | MasterReplyCap _ \ False | RestartCap \ False | RunningCap \ False - | PendingSyncSendCap _ _ _ _ _ \ False - | PendingSyncRecvCap _ _ \ False + | PendingSyncSendCap _ _ _ _ _ _ \ False + | PendingSyncRecvCap _ _ _ \ False | PendingNtfnRecvCap _ \ False | DomainCap \ False | BoundNotificationCap _ \ False diff --git a/spec/capDL/Syscall_D.thy b/spec/capDL/Syscall_D.thy index a1e953a88..952ad4b44 100644 --- a/spec/capDL/Syscall_D.thy +++ b/spec/capDL/Syscall_D.thy @@ -87,7 +87,7 @@ definition ep_related_cap :: "cdl_cap \ bool" where "ep_related_cap cap \ case cap of cdl_cap.EndpointCap o_id badge rights \ True | cdl_cap.NotificationCap o_id badge rights \ True -| cdl_cap.ReplyCap o_id \ True +| cdl_cap.ReplyCap o_id rights \ True | _ \ False" definition "has_restart_cap \ \tcb_id. do @@ -163,7 +163,7 @@ where if Read \ rights then (liftE $ do delete_cap_simple (tcb_id, tcb_caller_slot); - receive_ipc tcb_id (cap_object ep_cap) + receive_ipc tcb_id (cap_object ep_cap) (Grant \ rights) od) \ throw else throw @@ -189,7 +189,7 @@ where caller_cap \ get_cap (tcb_id, tcb_caller_slot); case caller_cap of - ReplyCap target \ do_reply_transfer tcb_id target (tcb_id, tcb_caller_slot) + ReplyCap target rights \ do_reply_transfer tcb_id target (tcb_id, tcb_caller_slot) (Grant \ rights) | NullCap \ return () | _ \ fail od diff --git a/spec/capDL/Types_D.thy b/spec/capDL/Types_D.thy index 84b199c62..5be7440a3 100644 --- a/spec/capDL/Types_D.thy +++ b/spec/capDL/Types_D.thy @@ -93,7 +93,7 @@ datatype cdl_cap = | UntypedCap bool cdl_object_set cdl_object_set | EndpointCap cdl_object_id cdl_badge "cdl_right set" | NotificationCap cdl_object_id cdl_badge "cdl_right set" - | ReplyCap cdl_object_id (* The id of the tcb of the target thread *) + | ReplyCap cdl_object_id "cdl_right set" (* The id of the tcb of the target thread *) | MasterReplyCap cdl_object_id | CNodeCap cdl_object_id cdl_cap_guard cdl_cap_guard_size cdl_size_bits | TcbCap cdl_object_id @@ -101,17 +101,11 @@ datatype cdl_cap = (* * Capabilities representing threads waiting in endpoint queues. - * - * The PendingSyncSendCap has booleans indicating if the pending - * send is a call, if it has grant rights, and if the send is a - * fault IPC respectively. *) - | PendingSyncSendCap cdl_object_id cdl_badge bool bool bool - - (* The PendingSyncRecvCap has booleans indicating if - it is waiting for a reply or not - *) - | PendingSyncRecvCap cdl_object_id bool + (* thread, badge, is call, can grant, can grant reply, is fault ipc *) + | PendingSyncSendCap cdl_object_id cdl_badge bool bool bool bool + (* thread, is waiting for reply, can grant *) + | PendingSyncRecvCap cdl_object_id bool bool | PendingNtfnRecvCap cdl_object_id (* Indicate that the thread is ready for Reschedule *) @@ -328,13 +322,13 @@ where | "cap_objects (TcbCap x) = {x}" | "cap_objects (CNodeCap x _ _ _) = {x}" | "cap_objects (MasterReplyCap x) = {x}" - | "cap_objects (ReplyCap x) = {x}" + | "cap_objects (ReplyCap x _) = {x}" | "cap_objects (NotificationCap x _ _) = {x}" | "cap_objects (EndpointCap x _ _) = {x}" | "cap_objects (UntypedCap _ x a) = x" | "cap_objects (ZombieCap x) = {x}" - | "cap_objects (PendingSyncSendCap x _ _ _ _) = {x}" - | "cap_objects (PendingSyncRecvCap x _ ) = {x}" + | "cap_objects (PendingSyncSendCap x _ _ _ _ _) = {x}" + | "cap_objects (PendingSyncRecvCap x _ _) = {x}" | "cap_objects (PendingNtfnRecvCap x) = {x}" | "cap_objects (BoundNotificationCap x) = {x}" @@ -371,12 +365,12 @@ lemma cap_object_simps: "cap_object (TcbCap x) = x" "cap_object (CNodeCap x k l sz) = x" "cap_object (MasterReplyCap x) = x" - "cap_object (ReplyCap x) = x" + "cap_object (ReplyCap x q) = x" "cap_object (NotificationCap x m n) = x" "cap_object (EndpointCap x p q) = x" "cap_object (ZombieCap x) = x" - "cap_object (PendingSyncSendCap x s t u v) = x" - "cap_object (PendingSyncRecvCap x t) = x" + "cap_object (PendingSyncSendCap x s t u v w) = x" + "cap_object (PendingSyncRecvCap x t u) = x" "cap_object (PendingNtfnRecvCap x) = x" "cap_object (BoundNotificationCap x) = x" by (simp_all add:cap_object_def Nitpick.The_psimp cap_has_object_def) @@ -395,7 +389,7 @@ where | _ \ c" definition all_cdl_rights :: "cdl_right set" where - "all_cdl_rights = {Read, Write, Grant}" + "all_cdl_rights = {Read, Write, Grant, GrantReply}" definition cap_rights :: "cdl_cap \ cdl_right set" @@ -404,6 +398,7 @@ where FrameCap _ _ x _ _ _ \ x | NotificationCap _ _ x \ x | EndpointCap _ _ x \ x + | ReplyCap _ x \ x | _ \ all_cdl_rights" definition @@ -411,8 +406,9 @@ definition where "update_cap_rights r c \ case c of FrameCap dev f1 _ f2 f3 f4 \ FrameCap dev f1 (validate_vm_rights r) f2 f3 f4 - | NotificationCap f1 f2 _ \ NotificationCap f1 f2 (r - {Grant}) + | NotificationCap f1 f2 _ \ NotificationCap f1 f2 (r - {Grant, GrantReply}) | EndpointCap f1 f2 _ \ EndpointCap f1 f2 r + | ReplyCap f1 _ \ ReplyCap f1 (r - {Read, GrantReply} \ {Write}) | _ \ c" definition @@ -584,9 +580,9 @@ lemma update_cap_guard_size [simp]: definition is_pending_cap :: "cdl_cap \ bool" where "is_pending_cap c \ case c of - PendingSyncRecvCap _ _ \ True + PendingSyncRecvCap _ _ _ \ True | PendingNtfnRecvCap _ \ True - | PendingSyncSendCap _ _ _ _ _ \ True + | PendingSyncSendCap _ _ _ _ _ _ \ True | _ \ False"