Skip to content

Commit

Permalink
rt arm ainvs: set handler params when configuring TCBs
Browse files Browse the repository at this point in the history 
Signed-off-by: Corey Lewis <[email protected]>
  • Loading branch information
@corlewis
corlewis committed Sep 2, 2022
1 parent aedba0e commit 646cd15
Show file tree
Hide file tree
Showing 3 changed files with 57 additions and 42 deletions.
2 changes: 1 addition & 1 deletion proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault
crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
decode_set_priority, decode_set_mcpriority, decode_set_sched_params, decode_set_timeout_ep,
decode_set_tls_base, decode_set_space
(simp: cap.splits arch_cap.splits split_def)
(simp: cap.splits arch_cap.splits split_def Let_def)

lemma decode_tcb_invocation_empty_fail[wp]:
"empty_fail (decode_tcb_invocation a b (ThreadCap p) d e)"
Expand Down
41 changes: 22 additions & 19 deletions proof/invariant-abstract/ARM/ArchIpc_AI.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,25 +15,28 @@ named_theorems Ipc_AI_assms
lemma update_cap_data_closedform:
"update_cap_data pres w cap =
(case cap of
cap.EndpointCap r badge rights \<Rightarrow>
if badge = 0 \<and> \<not> pres then (cap.EndpointCap r (w && mask 28) rights) else cap.NullCap
| cap.NotificationCap r badge rights \<Rightarrow>
if badge = 0 \<and> \<not> pres then (cap.NotificationCap r (w && mask 28) rights) else cap.NullCap
| cap.CNodeCap r bits guard \<Rightarrow>
if word_bits < unat ((w >> 3) && mask 5) + bits
then cap.NullCap
else cap.CNodeCap r bits ((\<lambda>g''. drop (size g'' - unat ((w >> 3) && mask 5)) (to_bl g'')) ((w >> 8) && mask 18))
| cap.ThreadCap r \<Rightarrow> cap.ThreadCap r
| cap.DomainCap \<Rightarrow> cap.DomainCap
| cap.UntypedCap d p n idx \<Rightarrow> cap.UntypedCap d p n idx
| cap.NullCap \<Rightarrow> cap.NullCap
| cap.ReplyCap t rights \<Rightarrow> cap.ReplyCap t rights
| cap.SchedContextCap s n \<Rightarrow> cap.SchedContextCap s n
| cap.SchedControlCap \<Rightarrow> cap.SchedControlCap
| cap.IRQControlCap \<Rightarrow> cap.IRQControlCap
| cap.IRQHandlerCap irq \<Rightarrow> cap.IRQHandlerCap irq
| cap.Zombie r b n \<Rightarrow> cap.Zombie r b n
| cap.ArchObjectCap cap \<Rightarrow> cap.ArchObjectCap cap)"
EndpointCap r badge rights \<Rightarrow>
if badge = 0 \<and> \<not> pres then (EndpointCap r (w && mask badge_bits) rights) else NullCap
| NotificationCap r badge rights \<Rightarrow>
if badge = 0 \<and> \<not> pres then (NotificationCap r (w && mask badge_bits) rights) else NullCap
| CNodeCap r bits guard \<Rightarrow>
if word_bits < unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits) + bits
then NullCap
else CNodeCap r bits
((\<lambda>g''. drop (size g'' - unat ((w >> cnode_padding_bits) &&
mask cnode_guard_size_bits)) (to_bl g''))
((w >> cnode_padding_bits + cnode_guard_size_bits) && mask 18))
| ThreadCap r \<Rightarrow> ThreadCap r
| DomainCap \<Rightarrow> DomainCap
| UntypedCap dev p n idx \<Rightarrow> UntypedCap dev p n idx
| NullCap \<Rightarrow> NullCap
| ReplyCap t rights \<Rightarrow> ReplyCap t rights
| SchedContextCap s n \<Rightarrow> SchedContextCap s n
| SchedControlCap \<Rightarrow> SchedControlCap
| IRQControlCap \<Rightarrow> IRQControlCap
| IRQHandlerCap irq \<Rightarrow> IRQHandlerCap irq
| Zombie r b n \<Rightarrow> Zombie r b n
| ArchObjectCap cap \<Rightarrow> ArchObjectCap cap)"
apply (cases cap,
simp_all only: cap.simps update_cap_data_def is_ep_cap.simps if_False if_True
is_ntfn_cap.simps is_cnode_cap.simps is_arch_cap_def word_size
Expand Down
56 changes: 34 additions & 22 deletions proof/invariant-abstract/ARM/ArchTcb_AI.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@ lemma checked_insert_tcb_invs: (* arch specific *)
and valid_cap new_cap
and tcb_cap_valid new_cap (target, ref)
and (\<lambda>s. valid_fault_handler new_cap
\<longrightarrow> cte_wp_at (\<lambda>c. c = new_cap \<or> c = NullCap) src_slot s)
\<longrightarrow> cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s)
and (cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap
\<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and>
pt_pd_asid c = pt_pd_asid new_cap) src_slot)\<rbrace>
Expand Down Expand Up @@ -140,7 +140,7 @@ lemma checked_insert_tcb_invs: (* arch specific *)
apply (rule conjI)
apply (erule disjE)
apply (erule(1) checked_insert_is_derived, simp+)
apply (auto simp: is_cnode_or_valid_arch_def is_derived_def is_cap_simps valid_fault_handler_def)
apply (auto simp: is_cnode_or_valid_arch_def is_derived_def is_cap_simps valid_fault_handler_def)
done

lemma checked_insert_tcb_invs': (* arch specific *)
Expand Down Expand Up @@ -251,26 +251,26 @@ lemma install_tcb_cap_invs:
"\<lbrace>invs and tcb_at target and
(\<lambda>s. \<forall>new_cap src_slot.
slot_opt = Some (new_cap, src_slot)
\<longrightarrow> K (is_cnode_or_valid_arch new_cap \<or>
valid_fault_handler new_cap) s
\<longrightarrow> K (is_cnode_or_valid_arch new_cap \<or> valid_fault_handler new_cap) s
\<and> valid_cap new_cap s
\<and> tcb_cap_valid new_cap (target, tcb_cnode_index n) s
\<and> (valid_fault_handler new_cap
\<longrightarrow> cte_wp_at valid_fault_handler (target, tcb_cnode_index n) s
\<and> cte_wp_at (\<lambda>c. c = new_cap \<or> c = NullCap) src_slot s)
\<longrightarrow> cte_wp_at valid_fault_handler (target, tcb_cnode_index n) s)
\<and> (is_ep_cap new_cap \<longrightarrow> cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s)
\<and> (case tcb_cap_cases (tcb_cnode_index n) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> \<forall>st. restr target st new_cap)
\<and> (tcb_cnode_index n = tcb_cnode_index 2 \<longrightarrow> (\<forall>ptr. valid_ipc_buffer_cap new_cap ptr))
\<and> real_cte_at src_slot s \<and> no_cap_to_obj_dr_emp new_cap s)\<rbrace>
install_tcb_cap target slot n slot_opt
\<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: install_tcb_cap_def)
unfolding install_tcb_cap_def
apply (wpsimp wp: checked_insert_tcb_invs cap_delete_deletes
hoare_vcg_imp_lift_R
| strengthen tcb_cap_always_valid_strg use_no_cap_to_obj_asid_strg
| wpsimp wp: cap_delete_ep)+
| wpsimp wp: cap_delete_is_derived_ep)+
by (auto simp: typ_at_eq_kheap_obj cap_table_at_typ tcb_at_typ
is_cnode_or_valid_arch_def is_cap_simps real_cte_at_cte
elim!: cte_wp_at_weakenE)
valid_fault_handler_def
elim!: notE[OF _ cte_wp_at_weakenE] is_derived_ep_cap)

lemma install_tcb_cap_no_cap_to_obj_dr_emp[wp, Tcb_AI_asms]:
"\<lbrace>no_cap_to_obj_dr_emp cap and
Expand Down Expand Up @@ -306,15 +306,16 @@ lemma install_tcb_frame_cap_invs:
\<comment> \<open>non-exception case\<close>
apply wpsimp
apply (wpsimp wp: checked_insert_tcb_invs[where ref="tcb_cnode_index 2"])
apply (wpsimp wp: hoare_vcg_all_lift static_imp_wp
apply ((wpsimp wp: hoare_vcg_all_lift static_imp_wp
thread_set_tcb_ipc_buffer_cap_cleared_invs
thread_set_cte_wp_at_trivial[where Q="\<lambda>x. x", OF ball_tcb_cap_casesI]
thread_set_ipc_tcb_cap_valid)
thread_set_ipc_tcb_cap_valid
| wps)+)[1]
apply((wpsimp wp: cap_delete_deletes
hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R hoare_vcg_all_lift
static_imp_wp static_imp_conj_wp
| strengthen use_no_cap_to_obj_asid_strg
| wp cap_delete_ep)+)[1]
| wp cap_delete_is_derived_ep)+)[1]
by (clarsimp simp: is_cap_simps' valid_fault_handler_def)

lemma tcc_invs[Tcb_AI_asms]:
Expand All @@ -341,21 +342,21 @@ lemma tcc_invs[Tcb_AI_asms]:
apply ((wpsimp wp: hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R
install_tcb_cap_invs
| strengthen tcb_cap_always_valid_strg
| wp install_tcb_cap_cte_wp_at_ep)+)[1]
| wp install_tcb_cap_cte_wp_at_ep install_tcb_cap_is_derived_ep)+)[1]
\<comment> \<open>install_tcb_cap 4\<close>
apply (simp)
apply (rule hoare_vcg_E_elim, wp install_tcb_cap_invs)
apply ((wpsimp wp: hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R
install_tcb_cap_invs
| strengthen tcb_cap_always_valid_strg
| wp install_tcb_cap_cte_wp_at_ep)+)[1]
| wp install_tcb_cap_cte_wp_at_ep install_tcb_cap_is_derived_ep)+)[1]
\<comment> \<open>install_tcb_cap 3\<close>
apply (simp)
apply (rule hoare_vcg_E_elim, wp install_tcb_cap_invs)
apply ((wpsimp wp: hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R
install_tcb_cap_invs
| strengthen tcb_cap_always_valid_strg
| wp install_tcb_cap_cte_wp_at_ep)+)[1]
| wp install_tcb_cap_cte_wp_at_ep install_tcb_cap_is_derived_ep)+)[1]
\<comment> \<open>cleanup\<close>
apply (simp)
apply (strengthen tcb_cap_always_valid_strg)
Expand All @@ -364,9 +365,10 @@ lemma tcc_invs[Tcb_AI_asms]:
apply (intro conjI impI;
clarsimp simp: is_cnode_or_valid_arch_is_cap_simps tcb_ep_slot_cte_wp_ats real_cte_at_cte
dest!: is_valid_vtable_root_is_arch_cap)
apply (all \<open>clarsimp simp: is_cap_simps cte_wp_at_caps_of_state\<close>)
apply (all \<open>clarsimp simp: is_cap_simps cte_wp_at_caps_of_state\<close>)
apply (all \<open>clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\<close>)
by (auto simp: valid_ipc_buffer_cap valid_fault_handler_def)
by (auto simp: valid_ipc_buffer_cap valid_fault_handler_def is_cap_simps
dest: is_derived_ep_cap)

crunches empty_slot
for sc_tcb_sc_at[wp]: "sc_tcb_sc_at P target"
Expand Down Expand Up @@ -406,7 +408,6 @@ lemma tcs_invs[Tcb_AI_asms]:
apply (intro conjI impI;
(clarsimp simp: is_cnode_or_valid_arch_is_cap_simps tcb_ep_slot_cte_wp_ats real_cte_at_cte
dest!: is_valid_vtable_root_is_arch_cap)?)
apply (erule cte_wp_at_strengthen, simp)
apply (clarsimp simp: obj_at_def is_ep is_tcb)
apply (intro conjI; intro allI impI)
apply (clarsimp simp: pred_tcb_at_def obj_at_def is_tcb)
Expand Down Expand Up @@ -476,10 +477,21 @@ lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]:
= vs_cap_ref c")
apply (simp add: no_cap_to_obj_with_diff_ref_def
update_cap_objrefs)
apply (clarsimp simp: update_cap_data_closedform
table_cap_ref_def
arch_update_cap_data_def
split: cap.split)
apply (clarsimp simp: update_cap_data_closedform table_cap_ref_simps
split: cap.splits)
apply simp
done

lemma no_cap_to_obj_with_diff_ref_mask_cap[Tcb_AI_asms]:
"no_cap_to_obj_with_diff_ref c S s \<longrightarrow>
no_cap_to_obj_with_diff_ref (mask_cap R c) S s"
apply (case_tac "mask_cap R c = NullCap")
apply (simp add: no_cap_to_obj_with_diff_ref_Null del: mask_cap_Null)
apply (subgoal_tac "vs_cap_ref (mask_cap R c) = vs_cap_ref c")
apply (simp add: no_cap_to_obj_with_diff_ref_def)
apply (clarsimp simp: mask_cap_def cap_rights_update_def acap_rights_update_def
table_cap_ref_simps
split: cap.split arch_cap.split)
apply simp
done

Expand Down

0 comments on commit 646cd15

Please sign in to comment.