SELFOUR-444: Haskell implementation, begin refine.
First attempt at a haskell implementation of preemptible retyping and the refinement proof to abstract.
This commit is contained in:
Thomas Sewell
parent
63888fa98d
commit
d765a64b81
|
|
@ -42,9 +42,10 @@ session BaseRefine = AInvs +
|
|||
"refine/Include"
|
||||
|
||||
session AInvs = ASpec +
|
||||
theories [condition = "SKIP_INVS_PROOFS", quick_and_dirty, skip_proofs]
|
||||
"invariant-abstract/AInvs"
|
||||
theories
|
||||
"invariant-abstract/AInvs"
|
||||
"invariant-abstract/EmptyFail_AI"
|
||||
"invariant-abstract/KernelInit_AI"
|
||||
"invariant-abstract/DetSchedSchedule_AI"
|
||||
|
||||
|
|
|
|||
|
|
@ -21,6 +21,44 @@ crunch ct[wp]: init_arch_objects "\<lambda>s. P (cur_thread s)" (wp: crunch_wps
|
|||
crunch st_tcb_at[wp]: init_arch_objects "st_tcb_at Q t" (wp: mapM_x_wp' hoare_unless_wp)
|
||||
crunch valid_etcbs[wp, DetSchedAux_AI_assms]: init_arch_objects valid_etcbs (wp: valid_etcbs_lift)
|
||||
|
||||
crunch ct[wp, DetSchedAux_AI_assms]: invoke_untyped "\<lambda>s. P (cur_thread s)"
|
||||
(wp: crunch_wps dxo_wp_weak preemption_point_inv mapME_x_inv_wp
|
||||
simp: crunch_simps do_machine_op_def detype_def mapM_x_defsym unless_def
|
||||
ignore: freeMemory ignore: retype_region_ext)
|
||||
crunch ready_queues[wp, DetSchedAux_AI_assms]: invoke_untyped "\<lambda>s. P (ready_queues s)"
|
||||
(wp: crunch_wps mapME_x_inv_wp preemption_point_inv'
|
||||
simp: detype_def detype_ext_def whenE_def unless_def
|
||||
wrap_ext_det_ext_ext_def mapM_x_defsym
|
||||
ignore: freeMemory)
|
||||
crunch scheduler_action[wp, DetSchedAux_AI_assms]: invoke_untyped "\<lambda>s. P (scheduler_action s)"
|
||||
(wp: crunch_wps mapME_x_inv_wp preemption_point_inv'
|
||||
simp: detype_def detype_ext_def whenE_def unless_def
|
||||
wrap_ext_det_ext_ext_def mapM_x_defsym
|
||||
ignore: freeMemory)
|
||||
crunch cur_domain[wp, DetSchedAux_AI_assms]: invoke_untyped "\<lambda>s. P (cur_domain s)"
|
||||
(wp: crunch_wps mapME_x_inv_wp preemption_point_inv'
|
||||
simp: detype_def detype_ext_def whenE_def unless_def
|
||||
wrap_ext_det_ext_ext_def mapM_x_defsym
|
||||
ignore: freeMemory)
|
||||
crunch idle_thread[wp, DetSchedAux_AI_assms]: invoke_untyped "\<lambda>s. P (idle_thread s)"
|
||||
(wp: crunch_wps mapME_x_inv_wp preemption_point_inv dxo_wp_weak
|
||||
simp: detype_def detype_ext_def whenE_def unless_def
|
||||
wrap_ext_det_ext_ext_def mapM_x_defsym
|
||||
ignore: freeMemory retype_region_ext)
|
||||
|
||||
crunch inv[wp]: get_tcb_queue, ethread_get "\<lambda>s. P s"
|
||||
|
||||
lemma tcb_sched_action_valid_idle_etcb:
|
||||
"\<lbrace>valid_idle_etcb\<rbrace>
|
||||
tcb_sched_action foo thread
|
||||
\<lbrace>\<lambda>_. valid_idle_etcb\<rbrace>"
|
||||
apply (rule valid_idle_etcb_lift)
|
||||
apply (simp add: tcb_sched_action_def set_tcb_queue_def)
|
||||
apply (wp | simp)+
|
||||
done
|
||||
|
||||
crunch ekheap[wp]: do_machine_op "\<lambda>s. P (ekheap s)"
|
||||
|
||||
lemma delete_objects_etcb_at[wp, DetSchedAux_AI_assms]:
|
||||
"\<lbrace>\<lambda>s::det_ext state. etcb_at P t s\<rbrace> delete_objects a b \<lbrace>\<lambda>r s. etcb_at P t s\<rbrace>"
|
||||
apply (simp add: delete_objects_def)
|
||||
|
|
@ -28,16 +66,29 @@ lemma delete_objects_etcb_at[wp, DetSchedAux_AI_assms]:
|
|||
apply (simp add: detype_def detype_ext_def wrap_ext_det_ext_ext_def etcb_at_def|wp)+
|
||||
done
|
||||
|
||||
crunch etcb_at[wp]: reset_untyped_cap "etcb_at P t"
|
||||
(wp: preemption_point_inv' mapME_x_inv_wp crunch_wps
|
||||
simp: unless_def)
|
||||
|
||||
crunch valid_etcbs[wp]: reset_untyped_cap "valid_etcbs"
|
||||
(wp: preemption_point_inv' mapME_x_inv_wp crunch_wps
|
||||
simp: unless_def)
|
||||
|
||||
lemma invoke_untyped_etcb_at [DetSchedAux_AI_assms]:
|
||||
"\<lbrace>(\<lambda>s :: det_ext state. etcb_at P t s) and valid_etcbs\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. st_tcb_at (Not o inactive) t s \<longrightarrow> etcb_at P t s\<rbrace> "
|
||||
"\<lbrace>(\<lambda>s :: det_ext state. etcb_at P t s) and valid_etcbs\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. st_tcb_at (Not o inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>"
|
||||
apply (cases ui)
|
||||
apply (simp add: mapM_x_def[symmetric])
|
||||
apply wp
|
||||
apply (wp retype_region_etcb_at mapM_x_wp' create_cap_no_pred_tcb_at
|
||||
hoare_convert_imp typ_at_pred_tcb_at_lift )
|
||||
apply simp
|
||||
apply (simp add: mapM_x_def[symmetric] invoke_untyped_def whenE_def
|
||||
split del: split_if)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp retype_region_etcb_at mapM_x_wp'
|
||||
create_cap_no_pred_tcb_at typ_at_pred_tcb_at_lift
|
||||
hoare_convert_imp[OF create_cap_no_pred_tcb_at]
|
||||
hoare_convert_imp[OF _ init_arch_objects_exst]
|
||||
| simp
|
||||
| (wp_once hoare_drop_impE_E))+
|
||||
done
|
||||
|
||||
|
||||
crunch valid_blocked[wp, DetSchedAux_AI_assms]: init_arch_objects valid_blocked
|
||||
(wp: valid_blocked_lift set_cap_typ_at)
|
||||
|
||||
|
|
@ -119,6 +170,9 @@ crunch valid_sched[wp]: init_arch_objects valid_sched (wp: valid_sched_lift)
|
|||
|
||||
end
|
||||
|
||||
lemmas tcb_sched_action_valid_idle_etcb
|
||||
= ARM.tcb_sched_action_valid_idle_etcb
|
||||
|
||||
global_interpretation DetSchedAux_AI_det_ext?: DetSchedAux_AI_det_ext
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
|
|
|
|||
|
|
@ -34,7 +34,9 @@ crunch valid_list[wp, Deterministic_AI_assms]: cap_recycle valid_list
|
|||
ignore: without_preemption filterM recycle_cap_ext)
|
||||
|
||||
crunch valid_list[wp]: invoke_untyped valid_list
|
||||
(wp: crunch_wps hoare_unless_wp simp: mapM_x_def_bak)
|
||||
(wp: crunch_wps preemption_point_inv' hoare_unless_wp mapME_x_wp'
|
||||
simp: mapM_x_def_bak crunch_simps
|
||||
ignore: Deterministic_A.OR_choiceE)
|
||||
|
||||
crunch valid_list[wp]: invoke_irq_control valid_list
|
||||
|
||||
|
|
|
|||
|
|
@ -743,7 +743,7 @@ lemma delete_objects_valid_pdpt:
|
|||
by (rule delete_objects_reduct) (wp detype_valid_pdpt)
|
||||
|
||||
crunch valid_pdpt[wp]: reset_untyped_cap "valid_pdpt_objs"
|
||||
(wp: mapME_x_inv_wp)
|
||||
(wp: mapME_x_inv_wp crunch_wps simp: crunch_simps unless_def)
|
||||
|
||||
lemma invoke_untyped_valid_pdpt[wp]:
|
||||
"\<lbrace>valid_pdpt_objs and invs and ct_active
|
||||
|
|
|
|||
|
|
@ -149,9 +149,9 @@ locale DetSchedAux_AI_det_ext = DetSchedAux_AI "TYPE(det_ext)" +
|
|||
invoke_untyped ui
|
||||
\<lbrace>\<lambda>r s. st_tcb_at (Not o inactive) t s \<longrightarrow> etcb_at P t s\<rbrace> "
|
||||
assumes init_arch_objects_valid_etcbs[wp]:
|
||||
"\<And>t r n sz refs dev. \<lbrace>valid_etcbs\<rbrace> init_arch_objects t r n sz refs dev\<lbrace>\<lambda>_. valid_etcbs\<rbrace>"
|
||||
"\<And>t r n sz refs. \<lbrace>valid_etcbs\<rbrace> init_arch_objects t r n sz refs \<lbrace>\<lambda>_. valid_etcbs\<rbrace>"
|
||||
assumes init_arch_objects_valid_blocked[wp]:
|
||||
"\<And>t r n sz refs dev. \<lbrace>valid_blocked\<rbrace> init_arch_objects t r n sz refs dev \<lbrace>\<lambda>_. valid_blocked\<rbrace>"
|
||||
"\<And>t r n sz refs. \<lbrace>valid_blocked\<rbrace> init_arch_objects t r n sz refs \<lbrace>\<lambda>_. valid_blocked\<rbrace>"
|
||||
assumes invoke_untyped_cur_domain[wp]:
|
||||
"\<And>P i. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> invoke_untyped i \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>"
|
||||
assumes invoke_untyped_ready_queues[wp]:
|
||||
|
|
@ -175,7 +175,7 @@ context DetSchedAux_AI_det_ext begin
|
|||
|
||||
crunch valid_etcbs[wp]: invoke_untyped "valid_etcbs"
|
||||
(wp: preemption_point_inv' mapME_x_inv_wp crunch_wps whenE_inv
|
||||
simp: mapM_x_defsym)
|
||||
simp: mapM_x_defsym crunch_simps unless_def)
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -220,7 +220,7 @@ context DetSchedAux_AI_det_ext begin
|
|||
|
||||
crunch valid_blocked[wp]: invoke_untyped "valid_blocked"
|
||||
(wp: preemption_point_inv' mapME_x_inv_wp crunch_wps whenE_inv
|
||||
simp: mapM_x_defsym)
|
||||
simp: mapM_x_defsym crunch_simps unless_def)
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -317,30 +317,6 @@ lemma valid_sched_tcb_state_preservation:
|
|||
apply(fastforce simp: valid_idle_def pred_tcb_at_def obj_at_def)
|
||||
done
|
||||
|
||||
crunch ct[wp]: invoke_untyped "\<lambda>s. P (cur_thread s)"
|
||||
(wp: crunch_wps dxo_wp_weak preemption_point_inv mapME_x_inv_wp
|
||||
simp: crunch_simps do_machine_op_def detype_def mapM_x_defsym
|
||||
ignore: freeMemory ignore: retype_region_ext)
|
||||
crunch ready_queues[wp]: invoke_untyped "\<lambda>s. P (ready_queues s)"
|
||||
(wp: crunch_wps mapME_x_inv_wp preemption_point_inv'
|
||||
simp: detype_def detype_ext_def whenE_def
|
||||
wrap_ext_det_ext_ext_def mapM_x_defsym
|
||||
ignore: freeMemory)
|
||||
crunch scheduler_action[wp]: invoke_untyped "\<lambda>s. P (scheduler_action s)"
|
||||
(wp: crunch_wps mapME_x_inv_wp preemption_point_inv'
|
||||
simp: detype_def detype_ext_def whenE_def
|
||||
wrap_ext_det_ext_ext_def mapM_x_defsym
|
||||
ignore: freeMemory)
|
||||
crunch cur_domain[wp]: invoke_untyped "\<lambda>s. P (cur_domain s)"
|
||||
(wp: crunch_wps mapME_x_inv_wp preemption_point_inv'
|
||||
simp: detype_def detype_ext_def whenE_def
|
||||
wrap_ext_det_ext_ext_def mapM_x_defsym
|
||||
ignore: freeMemory)
|
||||
crunch idle_thread[wp]: invoke_untyped "\<lambda>s. P (idle_thread s)"
|
||||
(wp: crunch_wps mapME_x_inv_wp preemption_point_inv dxo_wp_weak
|
||||
simp: detype_def detype_ext_def whenE_def
|
||||
wrap_ext_det_ext_ext_def mapM_x_defsym
|
||||
ignore: freeMemory retype_region_ext)
|
||||
lemma valid_idle_etcb_lift:
|
||||
assumes "\<And>P t. \<lbrace>\<lambda>s. etcb_at P t s\<rbrace> f \<lbrace>\<lambda>r s. etcb_at P t s\<rbrace>"
|
||||
shows "\<lbrace>valid_idle_etcb\<rbrace> f \<lbrace>\<lambda>r. valid_idle_etcb\<rbrace>"
|
||||
|
|
@ -348,23 +324,6 @@ lemma valid_idle_etcb_lift:
|
|||
apply(wp assms)
|
||||
done
|
||||
|
||||
crunch etcb_at[wp]: reset_untyped_cap "etcb_at P t"
|
||||
(wp: preemption_point_inv' mapME_x_inv_wp)
|
||||
|
||||
lemma invoke_untyped_etcb_at:
|
||||
"\<lbrace>(\<lambda>s :: det_ext state. etcb_at P t s) and valid_etcbs\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. st_tcb_at (Not o inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>"
|
||||
apply (cases ui)
|
||||
apply (simp add: mapM_x_def[symmetric] invoke_untyped_def whenE_def
|
||||
split del: split_if)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp retype_region_etcb_at mapM_x_wp'
|
||||
create_cap_no_pred_tcb_at typ_at_pred_tcb_at_lift
|
||||
hoare_convert_imp[OF create_cap_no_pred_tcb_at]
|
||||
hoare_convert_imp[OF _ init_arch_objects_exst]
|
||||
| simp
|
||||
| (wp_once hoare_drop_impE_E))+
|
||||
done
|
||||
|
||||
context DetSchedAux_AI_det_ext begin
|
||||
|
||||
lemma invoke_untyped_valid_sched:
|
||||
|
|
|
|||
|
|
@ -4085,9 +4085,6 @@ global_interpretation retype_region_ext_extended: is_extended "retype_region_ext
|
|||
apply wp
|
||||
done
|
||||
|
||||
crunch valid_list[wp]: invoke_untyped valid_list
|
||||
(wp: crunch_wps preemption_point_inv' mapME_x_inv_wp
|
||||
simp: mapM_x_def_bak whenE_def)
|
||||
crunch valid_list[wp]: invoke_irq_handler valid_list
|
||||
|
||||
crunch valid_list[wp]: attempt_switch_to "valid_list"
|
||||
|
|
|
|||
|
|
@ -2872,8 +2872,8 @@ lemma reset_untyped_cap_invs_etc:
|
|||
(simp add: cte_wp_at_caps_of_state descendants_range_def)+)
|
||||
apply (drule caps_of_state_valid_cap | clarify)+
|
||||
apply (intro conjI; clarify?; blast)[1]
|
||||
apply (cases "sz < reset_chunk_bits")
|
||||
apply simp
|
||||
apply (cases "dev \<or> sz < reset_chunk_bits")
|
||||
apply (simp add: unless_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp set_untyped_cap_invs_simple set_cap_cte_wp_at set_cap_no_overlap
|
||||
hoare_vcg_const_Ball_lift set_cap_cte_cap_wp_to
|
||||
|
|
@ -2882,7 +2882,8 @@ lemma reset_untyped_cap_invs_etc:
|
|||
apply (rule hoare_lift_Pf2 [where f="interrupt_irq_node"])
|
||||
apply (wp hoare_vcg_const_Ball_lift hoare_vcg_const_imp_lift
|
||||
hoare_vcg_ex_lift ct_in_state_thread_state_lift)
|
||||
apply (clarsimp simp add: bits_of_def field_simps cte_wp_at_caps_of_state)
|
||||
apply (clarsimp simp add: bits_of_def field_simps cte_wp_at_caps_of_state
|
||||
empty_descendants_range_in)
|
||||
apply (cut_tac a=sz and b=reset_chunk_bits and n=idx in upt_mult_lt_prop)
|
||||
apply (frule caps_of_state_valid_cap, clarsimp+)
|
||||
apply (simp add: valid_cap_def)
|
||||
|
|
@ -2929,11 +2930,11 @@ lemma reset_untyped_cap_st_tcb_at:
|
|||
\<lbrace>\<lambda>_. st_tcb_at P t\<rbrace>, \<lbrace>\<lambda>_. st_tcb_at P t\<rbrace>"
|
||||
apply (simp add: reset_untyped_cap_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp mapME_x_inv_wp preemption_point_inv | simp)+
|
||||
apply (wp mapME_x_inv_wp preemption_point_inv | simp add: unless_def)+
|
||||
apply (simp add: delete_objects_def)
|
||||
apply (wp get_cap_wp | simp)+
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state cap_range_def
|
||||
bits_of_def split: cap.split_asm)
|
||||
apply (wp get_cap_wp hoare_vcg_const_imp_lift | simp)+
|
||||
apply (auto simp: cte_wp_at_caps_of_state cap_range_def
|
||||
bits_of_def split: cap.split_asm)
|
||||
done
|
||||
|
||||
lemma create_cap_iflive[wp]:
|
||||
|
|
|
|||
|
|
@ -1653,5 +1653,39 @@ lemma loadWordUser_inv :
|
|||
unfolding loadWordUser_def
|
||||
by (wp dmo_inv' loadWord_inv stateAssert_wp | simp)+
|
||||
|
||||
lemma clearMemory_vms':
|
||||
"valid_machine_state' s \<Longrightarrow>
|
||||
\<forall>x\<in>fst (clearMemory ptr bits (ksMachineState s)).
|
||||
valid_machine_state' (s\<lparr>ksMachineState := snd x\<rparr>)"
|
||||
apply (clarsimp simp: valid_machine_state'_def
|
||||
disj_commute[of "pointerInUserData p s" for p s])
|
||||
apply (drule_tac x=p in spec, simp)
|
||||
apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = 0"
|
||||
in use_valid[where P=P and Q="\<lambda>_. P" for P], simp_all)
|
||||
apply (rule clearMemory_um_eq_0)
|
||||
done
|
||||
|
||||
lemma ct_not_inQ_ksMachineState_update[simp]:
|
||||
"ct_not_inQ (s\<lparr>ksMachineState := v\<rparr>) = ct_not_inQ s"
|
||||
by (simp add: ct_not_inQ_def)
|
||||
|
||||
lemma ct_in_current_domain_ksMachineState_update[simp]:
|
||||
"ct_idle_or_in_cur_domain' (s\<lparr>ksMachineState := v\<rparr>) = ct_idle_or_in_cur_domain' s"
|
||||
by (simp add: ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
|
||||
|
||||
lemma dmo_clearMemory_invs'[wp]:
|
||||
"\<lbrace>invs'\<rbrace> doMachineOp (clearMemory w sz) \<lbrace>\<lambda>_. invs'\<rbrace>"
|
||||
apply (simp add: doMachineOp_def split_def)
|
||||
apply wp
|
||||
apply (clarsimp simp: invs'_def valid_state'_def)
|
||||
apply (rule conjI)
|
||||
apply (simp add: valid_irq_masks'_def, elim allEI, clarsimp)
|
||||
apply (drule use_valid)
|
||||
apply (rule no_irq_clearMemory[simplified no_irq_def, rule_format])
|
||||
apply simp_all
|
||||
apply (drule clearMemory_vms')
|
||||
apply fastforce
|
||||
done
|
||||
|
||||
end
|
||||
end
|
||||
|
|
|
|||
|
|
@ -221,7 +221,7 @@ lemma pac_corres:
|
|||
apply (wp set_untyped_cap_invs_simple[where sz = pageBits]
|
||||
set_cap_cte_wp_at
|
||||
set_cap_caps_no_overlap[where sz = pageBits]
|
||||
set_cap_no_overlap[where sz = pageBits]
|
||||
set_cap_no_overlap
|
||||
set_cap_device_and_range_aligned[where dev = False,simplified]
|
||||
set_untyped_cap_caps_overlap_reserved[where sz = pageBits] | assumption)+
|
||||
apply (clarsimp simp: conj_comms obj_bits_api_def arch_kobj_size_def
|
||||
|
|
@ -252,7 +252,8 @@ lemma pac_corres:
|
|||
apply (clarsimp simp: conj_comms ex_disj_distrib
|
||||
| strengthen invs_valid_pspace' invs_pspace_aligned'
|
||||
invs_pspace_distinct')+
|
||||
apply (wp deleteObjects_invs' deleteObjects_cte_wp_at')
|
||||
apply (wp deleteObjects_invs' deleteObjects_cte_wp_at'
|
||||
deleteObjects_descendants)
|
||||
apply (rule_tac Q= "\<lambda>r s. ct_active' s \<and>
|
||||
(\<exists>x. (x = capability.UntypedCap False word1 pageBits idx \<and> F r s x))" for F
|
||||
in hoare_strengthen_post)
|
||||
|
|
@ -271,6 +272,7 @@ lemma pac_corres:
|
|||
deleteObject_no_overlap deleteObjects_ct_active')
|
||||
apply (clarsimp simp: is_simple_cap_def valid_cap'_def max_free_index_def is_cap_simps
|
||||
cong: conj_cong)
|
||||
apply (strengthen empty_descendants_range_in')
|
||||
apply (wp deleteObjects_descendants deleteObjects_cte_wp_at' deleteObjects_null_filter)
|
||||
apply (clarsimp simp:invs_mdb max_free_index_def invs_untyped_children)
|
||||
apply (subgoal_tac "detype_locale x y sa" for x y)
|
||||
|
|
@ -311,8 +313,6 @@ lemma pac_corres:
|
|||
apply clarsimp
|
||||
apply (rule conjI,clarsimp simp:clear_um_def)
|
||||
apply (simp add:detype_clear_um_independent)
|
||||
apply (rule conjI,rule pspace_no_overlap_detype[OF caps_of_state_valid])
|
||||
apply (simp add:invs_psp_aligned invs_valid_objs)+
|
||||
apply (rule conjI,erule caps_no_overlap_detype[OF descendants_range_caps_no_overlapI])
|
||||
apply (clarsimp simp:is_aligned_neg_mask_eq cte_wp_at_caps_of_state)
|
||||
apply (simp add:empty_descendants_range_in)+
|
||||
|
|
@ -322,6 +322,9 @@ lemma pac_corres:
|
|||
apply fastforce
|
||||
apply (clarsimp simp: region_in_kernel_window_def valid_cap_def
|
||||
cap_aligned_def is_aligned_neg_mask_eq detype_def clear_um_def)
|
||||
apply (rule conjI, rule pspace_no_overlap_subset,
|
||||
rule pspace_no_overlap_detype[OF caps_of_state_valid])
|
||||
apply (simp add:invs_psp_aligned invs_valid_objs is_aligned_neg_mask_eq)+
|
||||
apply (clarsimp simp: detype_def clear_um_def detype_ext_def valid_sched_def valid_etcbs_def
|
||||
st_tcb_at_kh_def obj_at_kh_def st_tcb_at_def obj_at_def is_etcb_at_def)
|
||||
apply (simp add: detype_def clear_um_def)
|
||||
|
|
@ -2247,6 +2250,7 @@ lemma performASIDControlInvocation_invs' [wp]:
|
|||
apply (clarsimp simp:isCap_simps)
|
||||
apply assumption
|
||||
apply (clarsimp split del:if_splits simp:valid_cap'_def max_free_index_def)
|
||||
apply (strengthen empty_descendants_range_in')
|
||||
apply (wp hoare_vcg_ex_lift deleteObjects_caps_no_overlap''
|
||||
deleteObjects_cte_wp_at'[where d=False] deleteObjects_null_filter[where d=False]
|
||||
deleteObject_no_overlap[where d=False] deleteObjects_descendants[where d=False])
|
||||
|
|
|
|||
|
|
@ -574,16 +574,6 @@ declare split_if [split]
|
|||
|
||||
text {* Proving desired properties about rec_del/cap_delete *}
|
||||
|
||||
lemma preemptionPoint_inv:
|
||||
assumes "(\<And>f s. P (ksWorkUnitsCompleted_update f s) = P s)"
|
||||
"irq_state_independent_H P"
|
||||
shows "\<lbrace>P\<rbrace> preemptionPoint \<lbrace>\<lambda>_. P\<rbrace>" using assms
|
||||
apply (simp add: preemptionPoint_def setWorkUnits_def getWorkUnits_def modifyWorkUnits_def)
|
||||
apply (wpc
|
||||
| wp hoare_whenE_wp hoare_seq_ext [OF _ select_inv] alternative_valid hoare_drop_imps
|
||||
| simp)+
|
||||
done
|
||||
|
||||
declare of_nat_power [simp del]
|
||||
|
||||
(* FIXME: pull up *)
|
||||
|
|
@ -754,47 +744,6 @@ lemma not_recursive_ctes_irq_state_independent[simp, intro!]:
|
|||
"not_recursive_ctes (s \<lparr> ksMachineState := ksMachineState s \<lparr> irq_state := x \<rparr>\<rparr>) = not_recursive_ctes s"
|
||||
by (simp add: not_recursive_ctes_def)
|
||||
|
||||
lemma ps_clear_irq_state_independent [simp, intro!]:
|
||||
"ps_clear a b (s\<lparr>ksMachineState := ksMachineState s
|
||||
\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) =
|
||||
ps_clear a b s"
|
||||
by (simp add: ps_clear_def)
|
||||
|
||||
lemma ct_in_state'_irq_state_independent [simp, intro!]:
|
||||
"ct_in_state' x (s\<lparr>ksMachineState := ksMachineState s
|
||||
\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) =
|
||||
ct_in_state' x s"
|
||||
by (simp add: ct_in_state'_def irq_state_independent_H_def)+
|
||||
|
||||
lemma ex_cte_cap_wp_to'_irq_state_independent [simp, intro!]:
|
||||
"ex_cte_cap_wp_to' x y (s\<lparr>ksMachineState := ksMachineState s
|
||||
\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) =
|
||||
ex_cte_cap_wp_to' x y s"
|
||||
by (simp add: ex_cte_cap_wp_to'_def irq_state_independent_H_def)+
|
||||
|
||||
lemma invs'_irq_state_independent [simp, intro!]:
|
||||
"invs' (s\<lparr>ksMachineState := ksMachineState s
|
||||
\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) =
|
||||
invs' s"
|
||||
apply (clarsimp simp: irq_state_independent_H_def invs'_def valid_state'_def
|
||||
valid_pspace'_def sch_act_wf_def
|
||||
valid_queues_def sym_refs_def state_refs_of'_def
|
||||
if_live_then_nonz_cap'_def if_unsafe_then_cap'_def
|
||||
valid_idle'_def valid_global_refs'_def
|
||||
valid_arch_state'_def valid_irq_node'_def
|
||||
valid_irq_handlers'_def valid_irq_states'_def
|
||||
irqs_masked'_def bitmapQ_defs valid_queues_no_bitmap_def
|
||||
valid_queues'_def valid_pde_mappings'_def
|
||||
pspace_domain_valid_def cur_tcb'_def
|
||||
valid_machine_state'_def tcb_in_cur_domain'_def
|
||||
cong: if_cong option.case_cong)
|
||||
apply (rule iffI)
|
||||
apply (clarsimp)
|
||||
apply (case_tac "ksSchedulerAction s", simp_all)
|
||||
apply clarsimp
|
||||
apply (case_tac "ksSchedulerAction s", simp_all)
|
||||
done
|
||||
|
||||
lemma typ_at'_irq_state_independent[simp, intro!]:
|
||||
"P (typ_at' T p (s \<lparr>ksMachineState := ksMachineState s \<lparr> irq_state := f (irq_state (ksMachineState s)) \<rparr>\<rparr>))
|
||||
= P (typ_at' T p s)"
|
||||
|
|
@ -6532,18 +6481,6 @@ lemma reduceZombie_invs'':
|
|||
apply (auto elim: ex_Zombie_to2)
|
||||
done
|
||||
|
||||
lemma invs'_wu [simp, intro!]:
|
||||
"invs' (ksWorkUnitsCompleted_update f s) = invs' s"
|
||||
apply (simp add: invs'_def cur_tcb'_def valid_state'_def Invariants_H.valid_queues_def
|
||||
valid_queues'_def valid_irq_node'_def valid_machine_state'_def
|
||||
ct_not_inQ_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def
|
||||
bitmapQ_defs valid_queues_no_bitmap_def)
|
||||
done
|
||||
|
||||
lemma preemptionPoint_invs [wp]:
|
||||
"\<lbrace>invs'\<rbrace> preemptionPoint \<lbrace>\<lambda>_. invs'\<rbrace>"
|
||||
by (wp preemptionPoint_inv | clarsimp)+
|
||||
|
||||
lemma preemptionPoint_no_cte_prop [wp]:
|
||||
"\<lbrace>no_cte_prop P and K (finalise_prop_stuff P)\<rbrace> preemptionPoint \<lbrace>\<lambda>_. no_cte_prop P\<rbrace>"
|
||||
apply (rule hoare_gen_asm)
|
||||
|
|
@ -7256,34 +7193,6 @@ lemma spec_corres_get_known_cap:
|
|||
apply (clarsimp dest!: singleton_eqD get_cap_det)
|
||||
done
|
||||
|
||||
lemma work_units_updated_state_relationI[intro!]:
|
||||
"(s,s') \<in> state_relation \<Longrightarrow>
|
||||
(work_units_completed_update (\<lambda>_. work_units_completed s + 1) s, s'\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s' + 1\<rparr>) \<in> state_relation"
|
||||
apply (simp add: state_relation_def)
|
||||
done
|
||||
|
||||
lemma work_units_and_irq_state_state_relationI [intro!]:
|
||||
"(s, s') \<in> state_relation \<Longrightarrow>
|
||||
(s \<lparr> work_units_completed := n, machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr>\<rparr>,
|
||||
s' \<lparr> ksWorkUnitsCompleted := n, ksMachineState := ksMachineState s' \<lparr> irq_state := f (irq_state (ksMachineState s')) \<rparr>\<rparr>)
|
||||
\<in> state_relation"
|
||||
by (simp add: state_relation_def swp_def)
|
||||
|
||||
lemma preemption_corres:
|
||||
"corres (intr \<oplus> dc) \<top> \<top> preemption_point preemptionPoint"
|
||||
apply (simp add: preemption_point_def preemptionPoint_def)
|
||||
by (auto simp: preemption_point_def preemptionPoint_def o_def gets_def liftE_def whenE_def getActiveIRQ_def
|
||||
corres_underlying_def select_def bind_def get_def bindE_def select_f_def modify_def
|
||||
alternative_def throwError_def returnOk_def return_def lift_def doMachineOp_def split_def
|
||||
put_def getWorkUnits_def setWorkUnits_def modifyWorkUnits_def do_machine_op_def
|
||||
|
||||
update_work_units_def wrap_ext_bool_det_ext_ext_def work_units_limit_def workUnitsLimit_def
|
||||
work_units_limit_reached_def OR_choiceE_def reset_work_units_def mk_ef_def
|
||||
elim: state_relationE)
|
||||
(* what? *)
|
||||
(* who says our proofs are not automatic.. *)
|
||||
|
||||
|
||||
lemma cte_map_not_in_cte_wp_at:
|
||||
"\<lbrakk> \<forall>p\<in>set'. \<exists>a b. p = cte_map (a, b) \<and> cte_wp_at (P a b) (a, b) s; cte_wp_at (op = c) p s;
|
||||
invs s; \<not> P (fst p) (snd p) c \<rbrakk> \<Longrightarrow> cte_map p \<notin> set'"
|
||||
|
|
|
|||
|
|
@ -3561,15 +3561,20 @@ lemma lsfc_corres:
|
|||
apply clarsimp
|
||||
done
|
||||
|
||||
(* this helper characterisation of ctes_of
|
||||
is needed in CNodeInv and Untyped *)
|
||||
|
||||
lemma ensureNoChildren_wp:
|
||||
"\<lbrace>\<lambda>s. Q s \<and> (descendants_of' p (ctes_of s) = {} \<longrightarrow> P () s)\<rbrace> ensureNoChildren p \<lbrace>P\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>"
|
||||
"\<lbrace>\<lambda>s. (descendants_of' p (ctes_of s) \<noteq> {} \<longrightarrow> Q s)
|
||||
\<and> (descendants_of' p (ctes_of s) = {} \<longrightarrow> P () s)\<rbrace>
|
||||
ensureNoChildren p
|
||||
\<lbrace>P\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>"
|
||||
apply (simp add: ensureNoChildren_def whenE_def)
|
||||
apply (wp getCTE_wp')
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def descendants_of'_def)
|
||||
apply (rule conjI)
|
||||
apply (intro conjI impI allI)
|
||||
apply clarsimp
|
||||
apply (drule spec, erule notE, rule subtree.direct_parent)
|
||||
apply (simp add:mdb_next_rel_def mdb_next_def)
|
||||
apply simp
|
||||
apply (simp add: parentOf_def)
|
||||
apply clarsimp
|
||||
apply (erule (4) subtree_no_parent)
|
||||
apply clarsimp
|
||||
|
|
@ -6351,5 +6356,11 @@ lemma updateFreeIndex_invs':
|
|||
apply (clarsimp simp:isCap_simps cte_wp_at_ctes_of)+
|
||||
done
|
||||
|
||||
lemma no_fail_getSlotCap:
|
||||
"no_fail (cte_at' p) (getSlotCap p)"
|
||||
apply (rule no_fail_pre)
|
||||
apply (simp add: getSlotCap_def | wp)+
|
||||
done
|
||||
|
||||
end
|
||||
end
|
||||
|
|
|
|||
|
|
@ -2303,12 +2303,11 @@ lemma createObject_cte_wp_at':
|
|||
apply (simp add:createObject_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wpc
|
||||
| wp createWordObjects_orig_cte_wp_at[where sz = "(Types_H.getObjectSize ty us)"]
|
||||
createObjects_orig_cte_wp_at'[where sz = "(Types_H.getObjectSize ty us)"]
|
||||
| wp createObjects_orig_cte_wp_at'[where sz = "(Types_H.getObjectSize ty us)"]
|
||||
threadSet_cte_wp_at'
|
||||
| simp add: ARM_H.createObject_def createPageObject_def
|
||||
| simp add: ARM_H.createObject_def placeNewDataObject_def
|
||||
unless_def placeNewObject_def2 objBitsKO_simps range_cover_full
|
||||
createPageObject_def curDomain_def pageBits_def ptBits_def
|
||||
curDomain_def pageBits_def ptBits_def
|
||||
pdBits_def getObjSize_simps archObjSize_def
|
||||
apiGetObjectSize_def tcbBlockSizeBits_def
|
||||
epSizeBits_def ntfnSizeBits_def
|
||||
|
|
@ -3547,7 +3546,7 @@ lemma createObject_setCTE_commute:
|
|||
apply ((rule monad_commute_guard_imp[OF commute_commute]
|
||||
, rule monad_commute_split[OF commute_commute[OF return_commute]]
|
||||
, clarsimp simp: ARM_H.createObject_def
|
||||
createPageObject_def bind_assoc split
|
||||
placeNewDataObject_def bind_assoc split
|
||||
del: if_splits
|
||||
,(rule monad_commute_split return_commute[THEN commute_commute]
|
||||
setCTE_modify_gsUserPages_commute[of \<top>]
|
||||
|
|
@ -3831,7 +3830,7 @@ lemma createNewCaps_not_nc:
|
|||
apply (rule hoare_pre)
|
||||
apply wpc
|
||||
apply wp
|
||||
apply (simp add:Arch_createNewCaps_def)
|
||||
apply (simp add:Arch_createNewCaps_def split del: split_if)
|
||||
apply (wpc|wp|clarsimp)+
|
||||
done
|
||||
|
||||
|
|
@ -3988,14 +3987,14 @@ lemma createNewCaps_pspace_no_overlap':
|
|||
ARM_H.toAPIType_def tcbBlockSizeBits_def
|
||||
ARM_H.getObjectSize_def objBits_simps epSizeBits_def ntfnSizeBits_def
|
||||
cteSizeBits_def pageBits_def ptBits_def archObjSize_def pdBits_def
|
||||
createObjects_def createWordObjects_def)
|
||||
createObjects_def)
|
||||
apply (rule hoare_pre)
|
||||
apply wpc
|
||||
apply (clarsimp simp: apiGetObjectSize_def curDomain_def
|
||||
ARM_H.toAPIType_def tcbBlockSizeBits_def
|
||||
ARM_H.getObjectSize_def objBits_simps epSizeBits_def ntfnSizeBits_def
|
||||
cteSizeBits_def pageBits_def ptBits_def archObjSize_def pdBits_def
|
||||
createObjects_def createWordObjects_def Arch_createNewCaps_def
|
||||
createObjects_def Arch_createNewCaps_def
|
||||
split: apiobject_type.splits
|
||||
| wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap[where sz = sz]
|
||||
createObjects'_psp_aligned[where sz = sz] createObjects'_psp_distinct[where sz = sz]
|
||||
|
|
@ -4007,7 +4006,7 @@ lemma createNewCaps_pspace_no_overlap':
|
|||
ARM_H.toAPIType_def tcbBlockSizeBits_def
|
||||
ARM_H.getObjectSize_def objBits_simps epSizeBits_def ntfnSizeBits_def
|
||||
cteSizeBits_def pageBits_def ptBits_def archObjSize_def pdBits_def
|
||||
createObjects_def createWordObjects_def Arch_createNewCaps_def
|
||||
createObjects_def Arch_createNewCaps_def
|
||||
unless_def
|
||||
split: apiobject_type.splits
|
||||
| wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap
|
||||
|
|
@ -4040,11 +4039,11 @@ lemma createNewCaps_ret_len:
|
|||
apply wpc
|
||||
apply (wp|simp add:Arch_createNewCaps_def ARM_H.toAPIType_def
|
||||
unat_of_nat_minus_1
|
||||
[where 'a=32, folded word_bits_def] createWordObjects_def |
|
||||
[where 'a=32, folded word_bits_def] |
|
||||
erule hoare_strengthen_post[OF createObjects_ret],clarsimp+ | intro conjI impI)+
|
||||
apply (rule hoare_pre,
|
||||
(wp | simp add: Arch_createNewCaps_def toAPIType_def
|
||||
ARM_H.toAPIType_def unat_of_nat_minus_1 createWordObjects_def
|
||||
ARM_H.toAPIType_def unat_of_nat_minus_1
|
||||
| erule hoare_strengthen_post[OF createObjects_ret],clarsimp+
|
||||
| intro conjI impI)+)+
|
||||
done
|
||||
|
|
@ -4679,18 +4678,16 @@ lemma createObjects_setDomains_commute:
|
|||
qed
|
||||
|
||||
lemma createObjects'_pspace_no_overlap2:
|
||||
"gz = (objBitsKO val) + us
|
||||
\<Longrightarrow> \<lbrace>pspace_no_overlap' (ptr + (1 + of_nat n << gz)) sz and
|
||||
K (range_cover ptr sz gz (Suc (Suc n)) \<and> ptr \<noteq> 0)\<rbrace>
|
||||
createObjects' ptr (Suc n) val us
|
||||
\<lbrace>\<lambda>addrs s. pspace_no_overlap' (ptr + (1 + of_nat n << gz)) sz s\<rbrace>"
|
||||
"\<lbrace>pspace_no_overlap' (ptr + (1 + of_nat n << gz)) sz
|
||||
and K (gz = (objBitsKO val) + us)
|
||||
and K (range_cover ptr sz gz (Suc (Suc n)) \<and> ptr \<noteq> 0)\<rbrace>
|
||||
createObjects' ptr (Suc n) val us
|
||||
\<lbrace>\<lambda>addrs s. pspace_no_overlap' (ptr + (1 + of_nat n << gz)) sz s\<rbrace>"
|
||||
proof -
|
||||
note blah[simp del] = untyped_range.simps usable_untyped_range.simps atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
|
||||
Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
|
||||
assume "gz = (objBitsKO val) + us"
|
||||
thus ?thesis using assms
|
||||
apply -
|
||||
apply (rule hoare_gen_asm)
|
||||
show ?thesis
|
||||
apply (rule hoare_gen_asm)+
|
||||
apply (clarsimp simp:createObjects'_def split_def new_cap_addrs_fold')
|
||||
apply (subst new_cap_addrs_fold')
|
||||
apply clarsimp
|
||||
|
|
@ -4880,8 +4877,7 @@ proof -
|
|||
mapM_def sequence_def Retype_H.createObject_def
|
||||
ARM_H.toAPIType_def
|
||||
createObjects_def ARM_H.createObject_def
|
||||
createPageObject_def Arch_createNewCaps_def
|
||||
createWordObjects_def comp_def
|
||||
Arch_createNewCaps_def comp_def
|
||||
apiGetObjectSize_def shiftl_t2n field_simps
|
||||
shiftL_nat mapM_x_def sequence_x_def append
|
||||
fromIntegral_def integral_inv[unfolded Fun.comp_def])
|
||||
|
|
@ -4892,8 +4888,7 @@ proof -
|
|||
sequence_def Retype_H.createObject_def
|
||||
ARM_H.toAPIType_def
|
||||
createObjects_def ARM_H.createObject_def
|
||||
createPageObject_def Arch_createNewCaps_def
|
||||
createWordObjects_def comp_def
|
||||
Arch_createNewCaps_def comp_def
|
||||
apiGetObjectSize_def shiftl_t2n field_simps
|
||||
shiftL_nat append mapM_x_append2
|
||||
fromIntegral_def integral_inv[unfolded Fun.comp_def])+
|
||||
|
|
@ -4965,8 +4960,7 @@ proof -
|
|||
mapM_def sequence_def Retype_H.createObject_def
|
||||
ARM_H.toAPIType_def
|
||||
createObjects_def ARM_H.createObject_def
|
||||
createPageObject_def Arch_createNewCaps_def
|
||||
createWordObjects_def comp_def
|
||||
Arch_createNewCaps_def comp_def
|
||||
apiGetObjectSize_def shiftl_t2n field_simps
|
||||
shiftL_nat mapM_x_def sequence_x_def append
|
||||
fromIntegral_def integral_inv[unfolded Fun.comp_def])+
|
||||
|
|
@ -4980,8 +4974,7 @@ proof -
|
|||
mapM_def sequence_def Retype_H.createObject_def
|
||||
ARM_H.toAPIType_def
|
||||
createObjects_def ARM_H.createObject_def
|
||||
createPageObject_def Arch_createNewCaps_def
|
||||
createWordObjects_def comp_def
|
||||
Arch_createNewCaps_def comp_def
|
||||
apiGetObjectSize_def shiftl_t2n field_simps
|
||||
shiftL_nat mapM_x_def sequence_x_def append
|
||||
fromIntegral_def integral_inv[unfolded Fun.comp_def])+
|
||||
|
|
@ -4999,10 +4992,10 @@ proof -
|
|||
apply simp
|
||||
|
||||
-- "SmallPageObject"
|
||||
apply (simp add: Arch_createNewCaps_def createWordObjects_def
|
||||
apply (simp add: Arch_createNewCaps_def
|
||||
Retype_H.createObject_def createObjects_def bind_assoc
|
||||
ARM_H.toAPIType_def ARM_H.toAPIType_def
|
||||
ARM_H.createObject_def createPageObject_def)
|
||||
ARM_H.createObject_def placeNewDataObject_def)
|
||||
apply (intro conjI impI)
|
||||
apply (subst monad_eq, rule createObjects_Cons)
|
||||
apply (simp_all add: field_simps shiftl_t2n pageBits_def
|
||||
|
|
@ -5030,18 +5023,11 @@ proof -
|
|||
unless_dmo'_createObjects'_comm
|
||||
dmo'_createObjects'_comm dmo'_gsUserPages_upd_comm
|
||||
| simp add: modify_modify_bind o_def)+
|
||||
apply (rule fun_cong[where x=s])
|
||||
apply (rule arg_cong2[where f=bind, OF refl ext])+
|
||||
apply (simp add: bind_assoc[symmetric])
|
||||
apply (rule arg_cong2[where f=bind, OF _ ext])
|
||||
apply (simp add: append mapM_x_append mapM_x_singleton)
|
||||
apply (subst doMachineOp_bind)
|
||||
apply ((simp add: add.commute unless_def when_def if_bind split del: if_splits)+)[4]
|
||||
-- "LargePageObject"
|
||||
apply (simp add: Arch_createNewCaps_def createWordObjects_def
|
||||
apply (simp add: Arch_createNewCaps_def
|
||||
Retype_H.createObject_def createObjects_def bind_assoc
|
||||
ARM_H.toAPIType_def ARM_H.toAPIType_def
|
||||
ARM_H.createObject_def createPageObject_def)
|
||||
ARM_H.createObject_def placeNewDataObject_def)
|
||||
apply (intro conjI impI)
|
||||
apply (subst monad_eq, rule createObjects_Cons)
|
||||
apply (simp_all add: field_simps shiftl_t2n pageBits_def
|
||||
|
|
@ -5069,18 +5055,11 @@ proof -
|
|||
unless_dmo'_createObjects'_comm
|
||||
dmo'_createObjects'_comm dmo'_gsUserPages_upd_comm
|
||||
| simp add: modify_modify_bind o_def)+
|
||||
apply (rule fun_cong[where x=s])
|
||||
apply (rule arg_cong2[where f=bind, OF refl ext])+
|
||||
apply (simp add: bind_assoc[symmetric])
|
||||
apply (rule arg_cong2[where f=bind, OF _ ext])
|
||||
apply (simp add: append mapM_x_append mapM_x_singleton)
|
||||
apply (subst doMachineOp_bind)
|
||||
apply ((simp add: add.commute unless_def when_def if_bind)+)[4]
|
||||
-- "SectionObject"
|
||||
apply (simp add: Arch_createNewCaps_def createWordObjects_def
|
||||
apply (simp add: Arch_createNewCaps_def
|
||||
Retype_H.createObject_def createObjects_def bind_assoc
|
||||
toAPIType_def ARM_H.toAPIType_def
|
||||
ARM_H.createObject_def createPageObject_def)
|
||||
ARM_H.createObject_def placeNewDataObject_def)
|
||||
apply (intro conjI impI)
|
||||
apply (subst monad_eq, rule createObjects_Cons)
|
||||
apply (simp_all add: field_simps shiftl_t2n pageBits_def
|
||||
|
|
@ -5108,18 +5087,11 @@ proof -
|
|||
unless_dmo'_createObjects'_comm
|
||||
dmo'_createObjects'_comm dmo'_gsUserPages_upd_comm
|
||||
| simp add: modify_modify_bind o_def)+
|
||||
apply (rule fun_cong[where x=s])
|
||||
apply (rule arg_cong2[where f=bind, OF refl ext])+
|
||||
apply (simp add: bind_assoc[symmetric])
|
||||
apply (rule arg_cong2[where f=bind, OF _ ext])
|
||||
apply (simp add: append mapM_x_append mapM_x_singleton)
|
||||
apply (subst doMachineOp_bind)
|
||||
apply ((simp add: add.commute unless_def if_bind when_def)+)[4]
|
||||
-- "SuperSectionObject"
|
||||
apply (simp add: Arch_createNewCaps_def createWordObjects_def
|
||||
apply (simp add: Arch_createNewCaps_def
|
||||
Retype_H.createObject_def createObjects_def bind_assoc
|
||||
toAPIType_def ARM_H.toAPIType_def
|
||||
ARM_H.createObject_def createPageObject_def)
|
||||
ARM_H.createObject_def placeNewDataObject_def)
|
||||
apply (intro conjI impI)
|
||||
apply (subst monad_eq, rule createObjects_Cons)
|
||||
apply (simp_all add: field_simps shiftl_t2n pageBits_def
|
||||
|
|
@ -5147,56 +5119,24 @@ proof -
|
|||
unless_dmo'_createObjects'_comm
|
||||
dmo'_createObjects'_comm dmo'_gsUserPages_upd_comm
|
||||
| simp add: modify_modify_bind o_def)+
|
||||
apply (rule fun_cong[where x=s])
|
||||
apply (rule arg_cong2[where f=bind, OF refl ext])+
|
||||
apply (simp add: bind_assoc[symmetric])
|
||||
apply (rule arg_cong2[where f=bind, OF _ ext])
|
||||
apply (simp add: append mapM_x_append mapM_x_singleton)
|
||||
apply (subst doMachineOp_bind)
|
||||
apply ((simp add: add.commute if_bind unless_def when_def)+)[4]
|
||||
-- "PageTableObject"
|
||||
apply (simp add:Arch_createNewCaps_def createWordObjects_def Retype_H.createObject_def
|
||||
apply (simp add:Arch_createNewCaps_def Retype_H.createObject_def
|
||||
createObjects_def bind_assoc ARM_H.toAPIType_def
|
||||
ARM_H.createObject_def createPageObject_def)
|
||||
ARM_H.createObject_def)
|
||||
apply (subst monad_eq,rule createObjects_Cons)
|
||||
apply ((simp add: field_simps shiftl_t2n pageBits_def archObjSize_def
|
||||
getObjectSize_def ARM_H.getObjectSize_def
|
||||
objBits_simps ptBits_def)+)[6]
|
||||
apply (simp add:bind_assoc)
|
||||
apply (rule monad_eq_split)
|
||||
apply (rule sym)
|
||||
apply (subst monad_commute_simple)
|
||||
apply (rule commute_commute[OF placeNewObject_doMachineOp_commute])
|
||||
apply assumption
|
||||
apply (rule monad_eq_split2[where Q = "\<lambda>r. \<top>"])
|
||||
apply (simp add: cteSizeBits_def pageBits_def field_simps
|
||||
tcbBlockSizeBits_def epSizeBits_def ntfnSizeBits_def pdBits_def
|
||||
apply (simp add:bind_assoc placeNewObject_def2)
|
||||
apply (simp add: pageBits_def field_simps
|
||||
getObjectSize_def ptBits_def archObjSize_def
|
||||
ARM_H.getObjectSize_def placeNewObject_def2
|
||||
objBits_simps mapM_x_def sequence_x_def append)
|
||||
apply (simp add:append mapM_x_append mapM_x_singleton )
|
||||
apply (subst doMachineOp_bind)
|
||||
apply (wp empty_fail_mapM_x empty_fail_cleanCacheRange_PoU)
|
||||
apply (simp add: cteSizeBits_def pageBits_def field_simps
|
||||
tcbBlockSizeBits_def epSizeBits_def ntfnSizeBits_def
|
||||
pdBits_def archObjSize_def ptBits_def shiftL_nat
|
||||
getObjectSize_def ARM_H.getObjectSize_def
|
||||
placeNewObject_def2 objBits_simps bind_assoc)
|
||||
apply (wp createObjects'_psp_aligned[where sz = sz]
|
||||
createObjects'_psp_distinct[where sz = sz]
|
||||
createObjects'_pspace_no_overlap[where sz =sz]
|
||||
| clarsimp simp:field_simps
|
||||
objBits_simps cteSizeBits_def pageBits_def ptBits_def archObjSize_def
|
||||
tcbBlockSizeBits_def epSizeBits_def ntfnSizeBits_def pdBits_def
|
||||
getObjectSize_def ARM_H.getObjectSize_def)+
|
||||
apply (frule range_cover_le[where n = "Suc n" ],simp)
|
||||
apply (simp add:word_bits_def)
|
||||
apply (erule aligned_add_aligned)
|
||||
apply ((simp add:is_aligned_shiftl_self word_bits_def)+)[3]
|
||||
objBits_simps append)
|
||||
|
||||
-- "PageDirectoryObject"
|
||||
apply (simp add:Arch_createNewCaps_def createWordObjects_def Retype_H.createObject_def
|
||||
apply (simp add:Arch_createNewCaps_def Retype_H.createObject_def
|
||||
createObjects_def bind_assoc ARM_H.toAPIType_def
|
||||
ARM_H.createObject_def createPageObject_def)
|
||||
ARM_H.createObject_def)
|
||||
apply (subgoal_tac "distinct (map (\<lambda>n. ptr + (n << 14)) [0.e.((of_nat n)::word32)])")
|
||||
prefer 2
|
||||
apply (clarsimp simp:objBits_simps archObjSize_def pdBits_def pageBits_def
|
||||
|
|
@ -5317,6 +5257,30 @@ proof -
|
|||
done
|
||||
qed
|
||||
|
||||
lemma createObject_def2:
|
||||
"(RetypeDecls_H.createObject ty ptr us dev >>= (\<lambda>x. return [x])) =
|
||||
createNewCaps ty ptr (Suc 0) us dev"
|
||||
apply (clarsimp simp:createObject_def createNewCaps_def placeNewObject_def2)
|
||||
apply (case_tac ty)
|
||||
apply (simp_all add: toAPIType_def)
|
||||
defer
|
||||
apply ((clarsimp simp: Arch_createNewCaps_def
|
||||
createObjects_def shiftL_nat
|
||||
ARM_H.createObject_def placeNewDataObject_def
|
||||
placeNewObject_def2 objBits_simps bind_assoc
|
||||
clearMemory_def clearMemoryVM_def fun_upd_def[symmetric]
|
||||
word_size mapM_x_singleton storeWordVM_def)+)[6]
|
||||
apply (rename_tac apiobject_type)
|
||||
apply (case_tac apiobject_type)
|
||||
apply (clarsimp simp: Arch_createNewCaps_def
|
||||
createObjects_def shiftL_nat
|
||||
ARM_H.createObject_def
|
||||
placeNewObject_def2 objBits_simps bind_assoc
|
||||
clearMemory_def clearMemoryVM_def
|
||||
word_size mapM_x_singleton storeWordVM_def)+
|
||||
done
|
||||
|
||||
|
||||
lemma createNewObjects_def2:
|
||||
"\<lbrakk>dslots \<noteq> []; length ( dslots ) < 2^word_bits;
|
||||
cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s;
|
||||
|
|
@ -5514,41 +5478,18 @@ lemma ArchCreateObject_pspace_no_overlap':
|
|||
apply (rule hoare_pre)
|
||||
apply (clarsimp simp:ARM_H.createObject_def)
|
||||
apply wpc
|
||||
apply ((wp doMachineOp_psp_no_overlap unless_doMachineOp_psp_no_overlap[simplified]
|
||||
apply (wp doMachineOp_psp_no_overlap unless_doMachineOp_psp_no_overlap[simplified]
|
||||
createObjects'_pspace_no_overlap2 hoare_when_weak_wp
|
||||
| simp add: createPageObject_def placeNewObject_def2 word_shiftl_add_distrib
|
||||
copyGlobalMappings_pspace_no_overlap'
|
||||
createObjects'_psp_aligned[where sz = sz]
|
||||
createObjects'_psp_distinct[where sz = sz]
|
||||
| simp add: placeNewObject_def2 word_shiftl_add_distrib
|
||||
| simp add: placeNewObject_def2 word_shiftl_add_distrib
|
||||
| simp add: placeNewDataObject_def placeNewObject_def2 word_shiftl_add_distrib
|
||||
field_simps split del: if_splits
|
||||
| clarsimp simp add: add.assoc[symmetric],wp createObjects'_pspace_no_overlap2[where n =0 and sz = sz,simplified]
|
||||
| clarsimp simp add: APIType_capBits_def objBits_simps pageBits_def)+
|
||||
,(wp createObjects'_psp_aligned[where sz = sz]
|
||||
createObjects'_psp_distinct[where sz = sz]))+
|
||||
apply (wp doMachineOp_psp_no_overlap[where sz =sz]
|
||||
createObjects'_psp_aligned[where sz = sz]
|
||||
createObjects'_psp_distinct[where sz = sz]
|
||||
createObjects'_pspace_no_overlap2 copyGlobalMappings_pspace_no_overlap'
|
||||
| simp add:createPageObject_def placeNewObject_def2 word_shiftl_add_distrib
|
||||
field_simps)+
|
||||
apply (rule_tac P="ptSize = 8" in hoare_gen_asm)
|
||||
apply (simp add:add.assoc[symmetric])
|
||||
apply (wp createObjects'_pspace_no_overlap2
|
||||
[where n =0 and sz = sz ,simplified])
|
||||
apply (simp add:APIType_capBits_def objBits_simps pageBits_def
|
||||
archObjSize_def ptBits_def)
|
||||
apply (wp doMachineOp_psp_no_overlap[where sz =sz]
|
||||
createObjects'_psp_aligned[where sz = sz]
|
||||
createObjects'_psp_distinct[where sz = sz]
|
||||
createObjects'_pspace_no_overlap2 copyGlobalMappings_pspace_no_overlap'
|
||||
| simp add:createPageObject_def placeNewObject_def2 word_shiftl_add_distrib
|
||||
field_simps)+
|
||||
apply (simp add:add.assoc[symmetric])
|
||||
apply (rule_tac P="pdSize = 12" in hoare_gen_asm)
|
||||
apply (wp createObjects'_pspace_no_overlap2
|
||||
[where n =0 and sz = sz,simplified])
|
||||
apply (simp add: APIType_capBits_def objBits_simps pageBits_def
|
||||
archObjSize_def ptBits_def pdBits_def)
|
||||
apply (wp createObjects'_psp_aligned[where sz = sz]
|
||||
createObjects'_psp_distinct[where sz = sz])[1]
|
||||
apply wp
|
||||
|
||||
apply (clarsimp simp: conj_comms)
|
||||
apply (frule(1) range_cover_no_0[where p = n])
|
||||
apply simp
|
||||
|
|
@ -5556,7 +5497,8 @@ lemma ArchCreateObject_pspace_no_overlap':
|
|||
(APIType_capBits ty userSize) ")
|
||||
prefer 2
|
||||
apply (rule aligned_add_aligned[OF range_cover.aligned],assumption)
|
||||
apply (simp add:is_aligned_shiftl_self range_cover_sz')+
|
||||
apply (simp add:is_aligned_shiftl_self range_cover_sz')
|
||||
apply (simp add: APIType_capBits_def)
|
||||
apply (frule range_cover_offset[rotated,where p = n])
|
||||
apply simp+
|
||||
apply (frule range_cover_le[where n = "Suc (Suc 0)"])
|
||||
|
|
@ -5581,6 +5523,10 @@ lemma ArchCreateObject_pspace_no_overlap':
|
|||
| rule conjI | erule range_cover_le,simp)+
|
||||
done
|
||||
|
||||
lemma to_from_apiTypeD: "toAPIType ty = Some x \<Longrightarrow> ty = fromAPIType x"
|
||||
by (cases ty) (auto simp add: fromAPIType_def
|
||||
toAPIType_def)
|
||||
|
||||
lemma createObject_pspace_no_overlap':
|
||||
"\<lbrace>\<lambda>s. pspace_no_overlap'
|
||||
(ptr + (of_nat n << APIType_capBits ty userSize)) sz s \<and>
|
||||
|
|
@ -5598,44 +5544,32 @@ lemma createObject_pspace_no_overlap':
|
|||
apply wp
|
||||
apply (simp add:placeNewObject_def2)
|
||||
apply (wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap2 unless_doMachineOp_psp_no_overlap[simplified]
|
||||
| simp add:createPageObject_def placeNewObject_def2 curDomain_def word_shiftl_add_distrib
|
||||
| simp add: placeNewObject_def2 curDomain_def word_shiftl_add_distrib
|
||||
field_simps)+
|
||||
apply (simp add:add.assoc[symmetric])
|
||||
apply (wp createObjects'_pspace_no_overlap2
|
||||
[where n =0 and sz = sz,simplified])
|
||||
apply (simp add:APIType_capBits_def objBits_simps
|
||||
pageBits_def ARM_H.toAPIType_def
|
||||
split:ARM_H.object_type.splits)
|
||||
apply (simp add:placeNewObject_def2)
|
||||
apply (wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap2 unless_doMachineOp_psp_no_overlap[simplified]
|
||||
| simp add:createPageObject_def placeNewObject_def2 word_shiftl_add_distrib
|
||||
| simp add: placeNewObject_def2 word_shiftl_add_distrib
|
||||
field_simps)+
|
||||
apply (simp add:add.assoc[symmetric])
|
||||
apply (wp createObjects'_pspace_no_overlap2
|
||||
[where n =0 and sz = sz,simplified])
|
||||
apply (simp add:APIType_capBits_def objBits_simps
|
||||
pageBits_def ARM_H.toAPIType_def
|
||||
split:ARM_H.object_type.splits)
|
||||
apply (simp add:placeNewObject_def2)
|
||||
apply (wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap2 unless_doMachineOp_psp_no_overlap[simplified]
|
||||
| simp add:createPageObject_def placeNewObject_def2 word_shiftl_add_distrib
|
||||
| simp add: placeNewObject_def2 word_shiftl_add_distrib
|
||||
field_simps)+
|
||||
apply (simp add:add.assoc[symmetric])
|
||||
apply (wp createObjects'_pspace_no_overlap2
|
||||
[where n =0 and sz = sz,simplified])
|
||||
apply (simp add:APIType_capBits_def objBits_simps
|
||||
pageBits_def ARM_H.toAPIType_def
|
||||
split:ARM_H.object_type.splits)
|
||||
apply (simp add:placeNewObject_def2)
|
||||
apply (wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap2 unless_doMachineOp_psp_no_overlap[simplified]
|
||||
| simp add:createPageObject_def placeNewObject_def2 word_shiftl_add_distrib
|
||||
| simp add: placeNewObject_def2 word_shiftl_add_distrib
|
||||
field_simps)+
|
||||
apply (simp add:add.assoc[symmetric])
|
||||
apply (wp createObjects'_pspace_no_overlap2
|
||||
[where n =0 and sz = sz,simplified])
|
||||
apply (simp add:APIType_capBits_def objBits_simps
|
||||
pageBits_def ARM_H.toAPIType_def
|
||||
split:ARM_H.object_type.splits)
|
||||
apply clarsimp
|
||||
apply (frule(1) range_cover_no_0[where p = n])
|
||||
apply simp
|
||||
|
|
@ -5653,9 +5587,9 @@ lemma createObject_pspace_no_overlap':
|
|||
apply (simp add:shiftl_t2n field_simps)
|
||||
apply (frule range_cover_offset[rotated,where p = n])
|
||||
apply simp+
|
||||
apply (intro conjI)
|
||||
apply (clarsimp simp:word_shiftl_add_distrib)+
|
||||
apply (clarsimp simp:field_simps shiftl_t2n | erule range_cover_le)+
|
||||
apply (auto simp: word_shiftl_add_distrib field_simps shiftl_t2n elim: range_cover_le,
|
||||
auto simp add: APIType_capBits_def fromAPIType_def objBits_def
|
||||
dest!: to_from_apiTypeD)
|
||||
done
|
||||
|
||||
lemma createObject_pspace_aligned_distinct':
|
||||
|
|
@ -5669,11 +5603,11 @@ lemma createObject_pspace_aligned_distinct':
|
|||
placeNewObject_pspace_distinct'
|
||||
| simp add:ARM_H.createObject_def
|
||||
Retype_H.createObject_def objBits_simps
|
||||
createPageObject_def curDomain_def
|
||||
curDomain_def placeNewDataObject_def
|
||||
split del: split_if
|
||||
| wpc | intro conjI impI)+
|
||||
apply (auto simp:APIType_capBits_def pdBits_def objBits_simps
|
||||
pageBits_def word_bits_def archObjSize_def ptBits_def ARM_H.toAPIType_def
|
||||
|
||||
split:ARM_H.object_type.splits apiobject_type.splits)
|
||||
done
|
||||
|
||||
|
|
|
|||
|
|
@ -3735,40 +3735,6 @@ lemma dmo'_bind_return:
|
|||
by (clarsimp simp: doMachineOp_def bind_def return_def valid_def select_f_def
|
||||
split_def)
|
||||
|
||||
lemma clearMemory_vms':
|
||||
"valid_machine_state' s \<Longrightarrow>
|
||||
\<forall>x\<in>fst (clearMemory ptr bits (ksMachineState s)).
|
||||
valid_machine_state' (s\<lparr>ksMachineState := snd x\<rparr>)"
|
||||
apply (clarsimp simp: valid_machine_state'_def
|
||||
disj_commute[of "pointerInUserData p s" for p s])
|
||||
apply (drule_tac x=p in spec, simp)
|
||||
apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = 0"
|
||||
in use_valid[where P=P and Q="\<lambda>_. P" for P], simp_all)
|
||||
apply (rule clearMemory_um_eq_0)
|
||||
done
|
||||
|
||||
lemma ct_not_inQ_ksMachineState_update[simp]:
|
||||
"ct_not_inQ (s\<lparr>ksMachineState := v\<rparr>) = ct_not_inQ s"
|
||||
by (simp add: ct_not_inQ_def)
|
||||
|
||||
lemma ct_in_current_domain_ksMachineState_update[simp]:
|
||||
"ct_idle_or_in_cur_domain' (s\<lparr>ksMachineState := v\<rparr>) = ct_idle_or_in_cur_domain' s"
|
||||
by (simp add: ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
|
||||
|
||||
lemma dmo_clearMemory_invs'[wp]:
|
||||
"\<lbrace>invs'\<rbrace> doMachineOp (clearMemory w sz) \<lbrace>\<lambda>_. invs'\<rbrace>"
|
||||
apply (simp add: doMachineOp_def split_def)
|
||||
apply wp
|
||||
apply (clarsimp simp: invs'_def valid_state'_def)
|
||||
apply (rule conjI)
|
||||
apply (simp add: valid_irq_masks'_def, elim allEI, clarsimp)
|
||||
apply (drule use_valid)
|
||||
apply (rule no_irq_clearMemory[simplified no_irq_def, rule_format])
|
||||
apply simp_all
|
||||
apply (drule clearMemory_vms')
|
||||
apply fastforce
|
||||
done
|
||||
|
||||
lemma ct_in_current_domain_ArchState_update[simp]:
|
||||
"ct_idle_or_in_cur_domain' (s\<lparr>ksArchState := v\<rparr>) = ct_idle_or_in_cur_domain' s"
|
||||
by (simp add: ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
|
||||
|
|
@ -4457,12 +4423,6 @@ crunch typ_at'[wp]: recycleCap "\<lambda>s. P (typ_at' T p s)"
|
|||
lemmas recycleCap_typ_at_lifts[wp]
|
||||
= typ_at_lifts [OF recycleCap_typ_at']
|
||||
|
||||
lemma no_fail_getSlotCap:
|
||||
"no_fail (cte_at' p) (getSlotCap p)"
|
||||
apply (rule no_fail_pre)
|
||||
apply (simp add: getSlotCap_def | wp)+
|
||||
done
|
||||
|
||||
crunch idle_thread[wp]: deleteCallerCap "\<lambda>s. P (ksIdleThread s)"
|
||||
(wp: crunch_wps)
|
||||
crunch sch_act_simple: deleteCallerCap sch_act_simple
|
||||
|
|
|
|||
|
|
@ -85,5 +85,96 @@ lemma getIRQSlot_cte_at[wp]:
|
|||
apply (clarsimp simp: real_cte_at')
|
||||
done
|
||||
|
||||
lemma work_units_updated_state_relationI[intro!]:
|
||||
"(s,s') \<in> state_relation \<Longrightarrow>
|
||||
(work_units_completed_update (\<lambda>_. work_units_completed s + 1) s, s'\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s' + 1\<rparr>) \<in> state_relation"
|
||||
apply (simp add: state_relation_def)
|
||||
done
|
||||
|
||||
lemma work_units_and_irq_state_state_relationI [intro!]:
|
||||
"(s, s') \<in> state_relation \<Longrightarrow>
|
||||
(s \<lparr> work_units_completed := n, machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr>\<rparr>,
|
||||
s' \<lparr> ksWorkUnitsCompleted := n, ksMachineState := ksMachineState s' \<lparr> irq_state := f (irq_state (ksMachineState s')) \<rparr>\<rparr>)
|
||||
\<in> state_relation"
|
||||
by (simp add: state_relation_def swp_def)
|
||||
|
||||
lemma preemption_corres:
|
||||
"corres (intr \<oplus> dc) \<top> \<top> preemption_point preemptionPoint"
|
||||
apply (simp add: preemption_point_def preemptionPoint_def)
|
||||
by (auto simp: preemption_point_def preemptionPoint_def o_def gets_def liftE_def whenE_def getActiveIRQ_def
|
||||
corres_underlying_def select_def bind_def get_def bindE_def select_f_def modify_def
|
||||
alternative_def throwError_def returnOk_def return_def lift_def doMachineOp_def split_def
|
||||
put_def getWorkUnits_def setWorkUnits_def modifyWorkUnits_def do_machine_op_def
|
||||
|
||||
update_work_units_def wrap_ext_bool_det_ext_ext_def work_units_limit_def workUnitsLimit_def
|
||||
work_units_limit_reached_def OR_choiceE_def reset_work_units_def mk_ef_def
|
||||
elim: state_relationE)
|
||||
(* what? *)
|
||||
(* who says our proofs are not automatic.. *)
|
||||
|
||||
lemma preemptionPoint_inv:
|
||||
assumes "(\<And>f s. P (ksWorkUnitsCompleted_update f s) = P s)"
|
||||
"irq_state_independent_H P"
|
||||
shows "\<lbrace>P\<rbrace> preemptionPoint \<lbrace>\<lambda>_. P\<rbrace>" using assms
|
||||
apply (simp add: preemptionPoint_def setWorkUnits_def getWorkUnits_def modifyWorkUnits_def)
|
||||
apply (wpc
|
||||
| wp hoare_whenE_wp hoare_seq_ext [OF _ select_inv] alternative_valid hoare_drop_imps
|
||||
| simp)+
|
||||
done
|
||||
|
||||
lemma invs'_wu [simp, intro!]:
|
||||
"invs' (ksWorkUnitsCompleted_update f s) = invs' s"
|
||||
apply (simp add: invs'_def cur_tcb'_def valid_state'_def Invariants_H.valid_queues_def
|
||||
valid_queues'_def valid_irq_node'_def valid_machine_state'_def
|
||||
ct_not_inQ_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def
|
||||
bitmapQ_defs valid_queues_no_bitmap_def)
|
||||
done
|
||||
|
||||
lemma ct_in_state'_irq_state_independent [simp, intro!]:
|
||||
"ct_in_state' x (s\<lparr>ksMachineState := ksMachineState s
|
||||
\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) =
|
||||
ct_in_state' x s"
|
||||
by (simp add: ct_in_state'_def irq_state_independent_H_def)+
|
||||
|
||||
lemma ex_cte_cap_wp_to'_irq_state_independent [simp, intro!]:
|
||||
"ex_cte_cap_wp_to' x y (s\<lparr>ksMachineState := ksMachineState s
|
||||
\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) =
|
||||
ex_cte_cap_wp_to' x y s"
|
||||
by (simp add: ex_cte_cap_wp_to'_def irq_state_independent_H_def)+
|
||||
|
||||
lemma ps_clear_irq_state_independent [simp, intro!]:
|
||||
"ps_clear a b (s\<lparr>ksMachineState := ksMachineState s
|
||||
\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) =
|
||||
ps_clear a b s"
|
||||
by (simp add: ps_clear_def)
|
||||
|
||||
lemma invs'_irq_state_independent [simp, intro!]:
|
||||
"invs' (s\<lparr>ksMachineState := ksMachineState s
|
||||
\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) =
|
||||
invs' s"
|
||||
apply (clarsimp simp: irq_state_independent_H_def invs'_def valid_state'_def
|
||||
valid_pspace'_def sch_act_wf_def
|
||||
valid_queues_def sym_refs_def state_refs_of'_def
|
||||
if_live_then_nonz_cap'_def if_unsafe_then_cap'_def
|
||||
valid_idle'_def valid_global_refs'_def
|
||||
valid_arch_state'_def valid_irq_node'_def
|
||||
valid_irq_handlers'_def valid_irq_states'_def
|
||||
irqs_masked'_def bitmapQ_defs valid_queues_no_bitmap_def
|
||||
valid_queues'_def valid_pde_mappings'_def
|
||||
pspace_domain_valid_def cur_tcb'_def
|
||||
valid_machine_state'_def tcb_in_cur_domain'_def
|
||||
ct_not_inQ_def ct_idle_or_in_cur_domain'_def
|
||||
cong: if_cong option.case_cong)
|
||||
apply (rule iffI[rotated])
|
||||
apply (clarsimp)
|
||||
apply (case_tac "ksSchedulerAction s", simp_all)
|
||||
apply clarsimp
|
||||
apply (case_tac "ksSchedulerAction s", simp_all)
|
||||
done
|
||||
|
||||
lemma preemptionPoint_invs [wp]:
|
||||
"\<lbrace>invs'\<rbrace> preemptionPoint \<lbrace>\<lambda>_. invs'\<rbrace>"
|
||||
by (wp preemptionPoint_inv | clarsimp)+
|
||||
|
||||
end
|
||||
end
|
||||
|
|
|
|||
|
|
@ -1135,16 +1135,6 @@ lemma createObjects_no_orphans [wp]:
|
|||
apply simp
|
||||
done
|
||||
|
||||
lemma createWordObjects_no_orphans [wp]:
|
||||
"\<lbrace> \<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s
|
||||
\<and> pspace_no_overlap' ptr sz s \<and> n \<noteq> 0 \<and> range_cover ptr sz (pageBits + us) n\<rbrace>
|
||||
createWordObjects ptr n us d
|
||||
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
|
||||
unfolding createWordObjects_def
|
||||
apply (wp hoare_unless_wp | clarsimp simp: projectKO_opt_tcb split del: split_if)+
|
||||
apply (intro conjI | simp add: objBits_simps)+
|
||||
done
|
||||
|
||||
lemma copyGlobalMappings_no_orphans [wp]:
|
||||
"\<lbrace> \<lambda>s. no_orphans s \<rbrace>
|
||||
copyGlobalMappings newPD
|
||||
|
|
@ -1178,7 +1168,10 @@ lemma createNewCaps_no_orphans:
|
|||
apply (wp mapM_x_wp' threadSet_no_orphans
|
||||
| clarsimp simp: is_active_thread_state_def makeObject_tcb
|
||||
projectKO_opt_tcb isRunning_def isRestart_def
|
||||
APIType_capBits_def objBits_simps Arch_createNewCaps_def
|
||||
APIType_capBits_def Arch_createNewCaps_def
|
||||
objBits_if_dev
|
||||
split del: split_if
|
||||
| simp add: objBits_simps
|
||||
| fastforce simp:pageBits_def archObjSize_def ptBits_def pdBits_def)+
|
||||
done
|
||||
|
||||
|
|
@ -1192,7 +1185,7 @@ lemma createObject_no_orphans:
|
|||
apply (simp_all add: createObject_def ARM_H.createObject_def split del: split_if)
|
||||
apply (rename_tac apiobject_type)
|
||||
apply (case_tac apiobject_type)
|
||||
apply (simp_all add: ARM_H.createObject_def createPageObject_def placeNewObject_def2
|
||||
apply (simp_all add: ARM_H.createObject_def placeNewObject_def2
|
||||
toAPIType_def split del: split_if)+
|
||||
apply (wp threadSet_no_orphans | clarsimp)+
|
||||
apply ((wp createObjects'_wp_subst
|
||||
|
|
@ -1222,7 +1215,7 @@ lemma createObject_no_orphans:
|
|||
split: option.splits split del: split_if)+)[1]
|
||||
apply ((wp createObjects'_wp_subst hoare_if
|
||||
createObjects_no_orphans[where sz = sz] |
|
||||
clarsimp simp: placeNewObject_def2
|
||||
clarsimp simp: placeNewObject_def2 placeNewDataObject_def
|
||||
projectKO_opt_tcb cte_wp_at_ctes_of projectKO_opt_ep
|
||||
is_active_thread_state_def makeObject_tcb pageBits_def unless_def
|
||||
projectKO_opt_tcb isRunning_def isRestart_def
|
||||
|
|
@ -1244,7 +1237,7 @@ lemma createObject_no_orphans:
|
|||
split: option.splits))+
|
||||
done
|
||||
|
||||
lemma createNewObjects_no_orphans :
|
||||
lemma createNewObjects_no_orphans:
|
||||
"\<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> pspace_no_overlap' ptr sz s
|
||||
\<and> (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s)
|
||||
\<and> cte_wp_at' (\<lambda>cte. cteCap cte = UntypedCap d (ptr && ~~ mask sz) sz idx) cref s
|
||||
|
|
@ -1296,134 +1289,45 @@ lemma deleteObjects_no_orphans [wp]:
|
|||
cong: if_cong)
|
||||
done
|
||||
|
||||
lemma invokeUntyped_no_orphans' [wp]:
|
||||
"ui = Retype cref ptr_base ptr tp us slots d \<Longrightarrow>
|
||||
\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> valid_untyped_inv' ui s \<and> ct_active' s \<rbrace>
|
||||
invokeUntyped ui
|
||||
\<lbrace> \<lambda>reply s. no_orphans s \<rbrace>"
|
||||
apply (rule hoare_name_pre_state)
|
||||
apply clarsimp
|
||||
apply (subgoal_tac "invokeUntyped_proofs s cref ptr tp us slots sz idx d")
|
||||
prefer 2
|
||||
apply (simp add:invokeUntyped_proofs_def)
|
||||
proof -
|
||||
fix s sz idx d
|
||||
assume no_orph: "no_orphans s"
|
||||
assume misc : " (tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us)"
|
||||
" tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> 4 \<le> us \<and> us \<le> 29"
|
||||
" sch_act_simple s " "ct_active' s"
|
||||
assume ivk_pf: "invokeUntyped_proofs s cref ptr tp us slots sz idx d"
|
||||
note blah[simp del] =
|
||||
atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
|
||||
Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex usableUntypedRange.simps
|
||||
|
||||
have capBits_low_bound[simp]:
|
||||
"4 \<le> APIType_capBits tp us"
|
||||
using misc
|
||||
apply (case_tac tp)
|
||||
apply (simp_all add:APIType_capBits_def objBits_simps ArchTypes_H.apiobject_type.splits)
|
||||
done
|
||||
|
||||
have us_align[simp]:"is_aligned (of_nat (length slots) * 2 ^ APIType_capBits tp us) 4"
|
||||
apply (rule is_aligned_weaken)
|
||||
apply (subst mult.commute)
|
||||
apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n])
|
||||
apply simp
|
||||
done
|
||||
|
||||
show "\<lbrace>op = s\<rbrace> invokeUntyped (Invocations_H.untyped_invocation.Retype cref (ptr && ~~ mask sz) ptr tp us slots d)
|
||||
\<lbrace>\<lambda>reply. no_orphans\<rbrace>"
|
||||
apply (simp add: invokeUntyped_def insertNewCaps_def
|
||||
split_def bind_assoc zipWithM_x_mapM
|
||||
cong: capability.case_cong)
|
||||
apply (case_tac "ptr && ~~ mask sz \<noteq> ptr")
|
||||
apply (rule hoare_pre)
|
||||
apply (wp createNewObjects_no_orphans[where sz = sz] getSlotCap_wp
|
||||
updateFreeIndex_invs' updateFreeIndex_pspace_no_overlap'
|
||||
hoare_vcg_ball_lift updateCap_weak_cte_wp_at
|
||||
updateFreeIndex_caps_no_overlap''
|
||||
updateFreeIndex_caps_overlap_reserved' | clarsimp)+
|
||||
apply (intro exI)
|
||||
apply (rule conjI)
|
||||
apply (rule invokeUntyped_proofs.cte_wp_at'[OF ivk_pf])
|
||||
using ivk_pf
|
||||
apply (clarsimp simp:conj_comms invs_valid_pspace'
|
||||
invokeUntyped_proofs_def no_orph misc)
|
||||
apply (simp add:getFreeIndex_def add_minus_neg_mask field_simps shiftL_nat
|
||||
invokeUntyped_proofs.ps_no_overlap'[OF ivk_pf]
|
||||
invokeUntyped_proofs.not_0_ptr[OF ivk_pf]
|
||||
invokeUntyped_proofs.usableRange_disjoint[OF ivk_pf]
|
||||
invokeUntyped_proofs.descendants_range[OF ivk_pf]
|
||||
invokeUntyped_proofs.slots_invD[OF ivk_pf]
|
||||
invokeUntyped_proofs.caps_no_overlap'[OF ivk_pf])
|
||||
apply (intro conjI)
|
||||
apply (simp add: range_cover_unat range_cover.unat_of_nat_shift field_simps)
|
||||
apply (rule aligned_add_aligned[OF aligned_after_mask])
|
||||
apply (erule range_cover.aligned)
|
||||
apply simp
|
||||
apply simp
|
||||
apply (simp add: range_cover_unat range_cover.unat_of_nat_shift field_simps)
|
||||
apply (drule range_cover.range_cover_compare_bound)
|
||||
apply simp
|
||||
apply simp+
|
||||
apply (rule subset_trans[OF invokeUntyped_proofs.subset_stuff[OF ivk_pf]])
|
||||
apply (clarsimp simp:blah word_and_le2)
|
||||
using ivk_pf
|
||||
apply clarsimp
|
||||
apply (wp createNewObjects_no_orphans[where sz = sz] getSlotCap_wp
|
||||
updateFreeIndex_invs_simple' updateFreeIndex_pspace_no_overlap'
|
||||
hoare_vcg_ball_lift updateCap_weak_cte_wp_at
|
||||
updateFreeIndex_caps_no_overlap''
|
||||
updateFreeIndex_caps_overlap_reserved' | clarsimp)+
|
||||
apply (strengthen invs_pspace_aligned' invs_valid_pspace'
|
||||
invs_pspace_distinct' invs_arch_state invs_psp_aligned)
|
||||
apply (clarsimp simp:conj_comms invokeUntyped_proofs.slots_invD[OF ivk_pf])
|
||||
apply (rule_tac P = "cap = capability.UntypedCap d (ptr && ~~ mask sz) sz idx"
|
||||
in hoare_gen_asm)
|
||||
apply (clarsimp simp:misc)
|
||||
apply (wp deleteObjects_invs'[where idx = idx and p = "cref" and d=d]
|
||||
deleteObjects_caps_no_overlap''[where idx = idx and slot = "cref" and d=d]
|
||||
deleteObject_no_overlap[where idx = idx and d=d]
|
||||
deleteObjects_cte_wp_at'[where idx = idx and ptr = ptr and bits = sz and d=d]
|
||||
deleteObjects_caps_overlap_reserved'[where idx = idx and slot = "cref" and d=d]
|
||||
deleteObjects_descendants[where idx = idx and p = "cref" and d=d]
|
||||
hoare_vcg_ball_lift hoare_drop_imp hoare_vcg_ex_lift
|
||||
deleteObjects_st_tcb_at'[where p = cref and d=d]
|
||||
deleteObjects_cte_wp_at'[where idx = idx and ptr = ptr and bits = sz and d=d]
|
||||
deleteObjects_ct_active'[where idx = idx and cref = cref and d=d])
|
||||
apply (clarsimp simp: conj_comms)
|
||||
apply (wp getSlotCap_wp)
|
||||
using invokeUntyped_proofs.usableRange_disjoint[OF ivk_pf]
|
||||
invokeUntyped_proofs.descendants_range[OF ivk_pf]
|
||||
invokeUntyped_proofs.slots_invD[OF ivk_pf]
|
||||
invokeUntyped_proofs.vc'[OF ivk_pf]
|
||||
invokeUntyped_proofs.cref_inv[OF ivk_pf]
|
||||
apply (clarsimp simp:invs_valid_pspace' invokeUntyped_proofs_def
|
||||
is_aligned_neg_mask_eq' range_cover.aligned
|
||||
no_orph getFreeIndex_def misc range_cover.sz )
|
||||
apply (simp add: getFreeIndex_def add_minus_neg_mask field_simps shiftL_nat
|
||||
invokeUntyped_proofs.not_0_ptr[OF ivk_pf]
|
||||
descendants_range'_def2 shiftL_nat
|
||||
range_cover_unat range_cover.unat_of_nat_shift
|
||||
invokeUntyped_proofs.caps_no_overlap'[OF ivk_pf]
|
||||
is_aligned_mask[unfolded is_aligned_neg_mask_eq']
|
||||
invs_pspace_distinct')
|
||||
apply (intro conjI)
|
||||
apply (simp add: range_cover_def word_bits_def)
|
||||
apply simp
|
||||
apply (simp add:is_aligned_mask[symmetric])
|
||||
apply (drule range_cover.range_cover_compare_bound)
|
||||
apply (simp add:is_aligned_mask[unfolded is_aligned_neg_mask_eq'])
|
||||
apply (rule subset_trans[OF invokeUntyped_proofs.subset_stuff[OF ivk_pf]])
|
||||
apply (simp add:is_aligned_mask[unfolded is_aligned_neg_mask_eq',symmetric])
|
||||
lemma no_orphans_ksWorkUnits [simp]:
|
||||
"no_orphans (ksWorkUnitsCompleted_update f s) = no_orphans s"
|
||||
unfolding no_orphans_def all_active_tcb_ptrs_def all_queued_tcb_ptrs_def is_active_tcb_ptr_def
|
||||
apply auto
|
||||
done
|
||||
|
||||
lemma no_orphans_irq_state_independent[intro!, simp]:
|
||||
"no_orphans (s \<lparr>ksMachineState := ksMachineState s \<lparr> irq_state := f (irq_state (ksMachineState s)) \<rparr> \<rparr>)
|
||||
= no_orphans s"
|
||||
by (simp add: no_orphans_def all_active_tcb_ptrs_def
|
||||
all_queued_tcb_ptrs_def is_active_tcb_ptr_def)
|
||||
|
||||
lemma resetUntypedCap_no_orphans [wp]:
|
||||
"\<lbrace> (\<lambda>s. no_orphans s \<and> pspace_distinct' s \<and> valid_objs' s)
|
||||
and cte_wp_at' (isUntypedCap o cteCap) slot\<rbrace>
|
||||
resetUntypedCap slot
|
||||
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
|
||||
apply (simp add: resetUntypedCap_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp mapME_x_inv_wp preemptionPoint_inv getSlotCap_wp
|
||||
| simp add: getSlotCap_def unless_def
|
||||
| wp_once hoare_drop_imps)+
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of)
|
||||
apply (frule(1) cte_wp_at_valid_objs_valid_cap'[OF ctes_of_cte_wpD])
|
||||
apply (clarsimp simp: isCap_simps valid_cap_simps' capAligned_def)
|
||||
done
|
||||
qed
|
||||
|
||||
lemma invokeUntyped_no_orphans [wp]:
|
||||
"\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> valid_untyped_inv' ui s \<and> ct_active' s \<rbrace>
|
||||
invokeUntyped ui
|
||||
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
|
||||
by (cases ui, erule invokeUntyped_no_orphans')
|
||||
invokeUntyped ui
|
||||
\<lbrace> \<lambda>reply s. no_orphans s \<rbrace>"
|
||||
apply (rule hoare_pre, rule hoare_strengthen_post)
|
||||
apply (rule invokeUntyped_invs''[where Q=no_orphans])
|
||||
apply (wp createNewCaps_no_orphans)
|
||||
apply (clarsimp simp: valid_pspace'_def)
|
||||
apply (intro conjI, simp_all)[1]
|
||||
apply (wp | simp)+
|
||||
apply (cases ui, auto simp: cte_wp_at_ctes_of)[1]
|
||||
done
|
||||
|
||||
lemma setInterruptState_no_orphans [wp]:
|
||||
"\<lbrace> \<lambda>s. no_orphans s \<rbrace>
|
||||
|
|
@ -1714,12 +1618,6 @@ lemma finaliseCap_no_orphans [wp]:
|
|||
apply (auto simp: valid_cap'_def dest!: isCapDs)
|
||||
done
|
||||
|
||||
lemma no_orphans_ksWorkUnits [simp]:
|
||||
"no_orphans (ksWorkUnitsCompleted_update f s) = no_orphans s"
|
||||
unfolding no_orphans_def all_active_tcb_ptrs_def all_queued_tcb_ptrs_def is_active_tcb_ptr_def
|
||||
apply auto
|
||||
done
|
||||
|
||||
crunch no_orphans [wp]: cteSwap "no_orphans"
|
||||
|
||||
crunch no_orphans [wp]: capSwapForDelete "no_orphans"
|
||||
|
|
@ -1760,12 +1658,6 @@ lemma cteDelete_no_orphans [wp]:
|
|||
crunch no_orphans [wp]: cteMove "no_orphans"
|
||||
(wp: crunch_wps)
|
||||
|
||||
lemma no_orphans_irq_state_independent[intro!, simp]:
|
||||
"no_orphans (s \<lparr>ksMachineState := ksMachineState s \<lparr> irq_state := f (irq_state (ksMachineState s)) \<rparr> \<rparr>)
|
||||
= no_orphans s"
|
||||
by (simp add: no_orphans_def all_active_tcb_ptrs_def
|
||||
all_queued_tcb_ptrs_def is_active_tcb_ptr_def)
|
||||
|
||||
lemma cteRevoke_no_orphans [wp]:
|
||||
"\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<rbrace>
|
||||
cteRevoke ptr
|
||||
|
|
|
|||
|
|
@ -400,7 +400,7 @@ lemma page_table_at_pte_atD':
|
|||
apply simp
|
||||
apply simp
|
||||
apply (subst (asm) is_aligned_neg_mask_eq[where n = 2])
|
||||
apply (simp add:aligned_after_mask)
|
||||
apply (simp add: is_aligned_andI1)
|
||||
apply (simp add:mask_out_sub_mask)
|
||||
done
|
||||
|
||||
|
|
@ -489,7 +489,7 @@ lemma page_directory_at_pde_atD':
|
|||
apply simp
|
||||
apply simp
|
||||
apply (subst (asm) is_aligned_neg_mask_eq[where n = 2])
|
||||
apply (simp add:aligned_after_mask)
|
||||
apply (simp add: is_aligned_andI1)
|
||||
apply (simp add:mask_out_sub_mask)
|
||||
done
|
||||
|
||||
|
|
@ -1154,7 +1154,7 @@ lemma createObject_valid_duplicates'[wp]:
|
|||
apply (simp add:createObject_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wpc | wp| simp add: ARM_H.createObject_def split del: split_if)+
|
||||
apply (simp add: createPageObject_def placeNewObject_def
|
||||
apply (simp add: placeNewObject_def placeNewDataObject_def
|
||||
placeNewObject'_def split_def split del: split_if
|
||||
| wp hoare_unless_wp[where P="d"] hoare_unless_wp[where Q=\<top>]
|
||||
| wpc | simp add: alignError_def split del: split_if)+
|
||||
|
|
@ -1430,71 +1430,74 @@ lemma deleteObjects_valid_duplicates'[wp]:
|
|||
apply simp
|
||||
done
|
||||
|
||||
crunch arch_inv[wp]: deleteObjects "\<lambda>s. P (ksArchState s)"
|
||||
(simp: crunch_simps wp: hoare_drop_imps hoare_unless_wp ignore:freeMemory)
|
||||
crunch arch_inv[wp]: resetUntypedCap "\<lambda>s. P (ksArchState s)"
|
||||
(simp: crunch_simps wp: hoare_drop_imps hoare_unless_wp mapME_x_inv_wp
|
||||
preemptionPoint_inv
|
||||
ignore:freeMemory forME_x)
|
||||
|
||||
lemma resetUntypedCap_valid_duplicates'[wp]:
|
||||
"\<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s))
|
||||
and valid_objs' and cte_wp_at' (isUntypedCap o cteCap) slot\<rbrace>
|
||||
resetUntypedCap slot
|
||||
\<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
|
||||
(is "\<lbrace>?P\<rbrace> ?f \<lbrace>\<lambda>_. ?Q\<rbrace>")
|
||||
apply (clarsimp simp: resetUntypedCap_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp | simp add: unless_def)+
|
||||
apply (wp mapME_x_inv_wp preemptionPoint_inv | simp | wp_once hoare_drop_imps)+
|
||||
apply (wp getSlotCap_wp)
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of)
|
||||
apply (frule cte_wp_at_valid_objs_valid_cap'[OF ctes_of_cte_wpD], clarsimp+)
|
||||
apply (clarsimp simp add: isCap_simps valid_cap_simps' capAligned_def)
|
||||
done
|
||||
|
||||
lemma is_aligned_armKSGlobalPD:
|
||||
"valid_arch_state' s
|
||||
\<Longrightarrow> is_aligned (armKSGlobalPD (ksArchState s)) pdBits"
|
||||
by (clarsimp simp: valid_arch_state'_def page_directory_at'_def)
|
||||
|
||||
lemma new_CapTable_bound:
|
||||
"range_cover (ptr :: obj_ref) sz (APIType_capBits tp us) n
|
||||
\<Longrightarrow> tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28"
|
||||
apply (frule range_cover.sz)
|
||||
apply (drule range_cover.sz(2))
|
||||
apply (clarsimp simp:APIType_capBits_def objBits_simps word_bits_def)
|
||||
done
|
||||
|
||||
lemma invokeUntyped_valid_duplicates[wp]:
|
||||
"\<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))
|
||||
and valid_untyped_inv' ui and ct_active'\<rbrace>
|
||||
invokeUntyped ui
|
||||
\<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s) \<rbrace>"
|
||||
apply (simp only: invokeUntyped_def updateCap_def)
|
||||
apply (rule hoare_name_pre_state)
|
||||
apply (cases ui)
|
||||
apply (clarsimp)
|
||||
apply (rename_tac s cref ptr tp us slots sz idx)
|
||||
proof -
|
||||
fix s cref ptr tp us slots sz idx d
|
||||
assume cte_wp_at': "cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s"
|
||||
assume cover : "range_cover ptr sz (APIType_capBits tp us) (length (slots::word32 list))"
|
||||
assume misc : "distinct slots" "idx \<le> unat (ptr && mask sz) \<or> ptr = ptr && ~~ mask sz"
|
||||
"invs' s" "slots \<noteq> []" "sch_act_simple s" "vs_valid_duplicates' (ksPSpace s)"
|
||||
"\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s"
|
||||
"\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s" "ct_active' s"
|
||||
"tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> 4 \<le> us \<and> us \<le> 29"
|
||||
assume desc_range: "ptr = ptr && ~~ mask sz \<longrightarrow> descendants_range_in' {ptr..ptr + 2 ^ sz - 1} (cref) (ctes_of s)"
|
||||
|
||||
have pf: "invokeUntyped_proofs s cref ptr tp us slots sz idx d"
|
||||
using cte_wp_at' cover misc desc_range
|
||||
by (simp add:invokeUntyped_proofs_def)
|
||||
have bound[simp]: "tp = APIObjectType apiobject_type.CapTableObject \<longrightarrow> us < 28"
|
||||
using cover
|
||||
apply -
|
||||
apply (frule range_cover.sz)
|
||||
apply (drule range_cover.sz(2))
|
||||
apply (clarsimp simp:APIType_capBits_def objBits_simps word_bits_def)
|
||||
done
|
||||
have pd_aligned[simp]:
|
||||
"armKSGlobalPD (ksArchState s) && ~~ mask pdBits = armKSGlobalPD (ksArchState s)"
|
||||
using misc
|
||||
apply -
|
||||
apply (clarsimp dest!:invs_arch_state' simp:valid_arch_state'_def
|
||||
page_directory_at'_def is_aligned_neg_mask_eq')
|
||||
done
|
||||
show
|
||||
"\<lbrace>op = s\<rbrace>
|
||||
invokeUntyped
|
||||
(Invocations_H.untyped_invocation.Retype cref (ptr && ~~ mask sz) ptr tp us slots d)
|
||||
\<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
|
||||
apply (clarsimp simp:invokeUntyped_def updateCap_def)
|
||||
apply (clarsimp simp only: pred_conj_def valid_untyped_inv_wcap'
|
||||
Invocations_H.untyped_invocation.simps)
|
||||
apply (frule(2) invokeUntyped_proofs.intro)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp setCTE_pspace_no_overlap'[where sz = sz ]
|
||||
deleteObjects_invs_derivatives[where idx = idx and p = cref and d=d])
|
||||
apply (rule_tac P = "cap = capability.UntypedCap d (ptr && ~~ mask sz) sz idx"
|
||||
in hoare_gen_asm)
|
||||
apply simp
|
||||
apply (wp setCTE_pspace_no_overlap')
|
||||
apply (rule hoare_post_impErr)
|
||||
apply (rule combine_validE)
|
||||
apply (rule_tac ui=ui in whenE_reset_resetUntypedCap_invs_etc)
|
||||
apply (rule hoare_whenE_wp)
|
||||
apply (rule valid_validE)
|
||||
apply (rule resetUntypedCap_valid_duplicates')
|
||||
defer
|
||||
apply simp
|
||||
apply (wp getSlotCap_wp hoare_drop_imps
|
||||
deleteObject_no_overlap deleteObjects_invs_derivatives[where idx = idx and p = cref and d=d])
|
||||
using cte_wp_at' misc cover desc_range
|
||||
invokeUntyped_proofs.not_0_ptr[OF pf] invokeUntyped_proofs.vc'[OF pf]
|
||||
apply (clarsimp simp:cte_wp_at_ctes_of)
|
||||
apply (rule_tac x = "capability.UntypedCap d (ptr && ~~ mask sz) sz idx" in exI)
|
||||
apply (clarsimp simp: is_aligned_neg_mask_eq' conj_comms invs_valid_pspace'
|
||||
invs_pspace_aligned' invs_pspace_distinct'
|
||||
range_cover.sz[where 'a=32, folded word_bits_def]
|
||||
invokeUntyped_proofs.ps_no_overlap'[OF pf])
|
||||
apply (simp add:descendants_range'_def2)
|
||||
apply (clarsimp simp del: valid_untyped_inv_wcap'.simps
|
||||
split del: split_if)
|
||||
apply (rule conjI, assumption)
|
||||
apply (auto simp: cte_wp_at_ctes_of isCap_simps)[1]
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of)
|
||||
apply (frule new_CapTable_bound)
|
||||
apply (frule invokeUntyped_proofs.not_0_ptr)
|
||||
apply (strengthen is_aligned_armKSGlobalPD)
|
||||
apply (frule cte_wp_at_valid_objs_valid_cap'[OF ctes_of_cte_wpD], clarsimp+)
|
||||
apply (clarsimp simp add: isCap_simps valid_cap_simps' capAligned_def)
|
||||
apply (auto split: split_if_asm)
|
||||
done
|
||||
qed
|
||||
|
||||
crunch valid_duplicates'[wp]:
|
||||
doReplyTransfer "\<lambda>s. vs_valid_duplicates' (ksPSpace s)"
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -497,15 +497,16 @@ lemma pinv_corres:
|
|||
(perform_invocation block call i) (performInvocation block call i')"
|
||||
apply (simp add: performInvocation_def)
|
||||
apply (case_tac i)
|
||||
apply (clarsimp simp: o_def liftE_bindE)
|
||||
apply (clarsimp simp: o_def liftE_bindE)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split_norE[OF corres_returnOkTT])
|
||||
apply simp
|
||||
apply (rule corres_rel_imp, rule inv_untyped_corres)
|
||||
apply simp
|
||||
apply (case_tac x, simp_all)[1]
|
||||
apply wp
|
||||
apply simp+
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split[OF corres_returnOkTT])
|
||||
apply simp
|
||||
apply (erule corres_guard_imp [OF inv_untyped_corres])
|
||||
apply assumption+
|
||||
apply wp
|
||||
apply simp+
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split [OF _ gct_corres])
|
||||
apply simp
|
||||
apply (rule corres_split [OF _ send_ipc_corres])
|
||||
|
|
@ -2443,7 +2444,7 @@ lemma retype_pi_IRQInactive:
|
|||
apply (rule hoare_pre)
|
||||
apply (wpc |
|
||||
wp inv_tcb_IRQInactive inv_cnode_IRQInactive inv_irq_IRQInactive
|
||||
inv_arch_IRQInactive |
|
||||
inv_untyped_IRQInactive inv_arch_IRQInactive |
|
||||
simp)+
|
||||
done
|
||||
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -145,9 +145,9 @@ definition
|
|||
get_free_index :: "obj_ref \<Rightarrow> obj_ref \<Rightarrow> nat" where
|
||||
"get_free_index base free \<equiv> unat $ (free - base)"
|
||||
|
||||
primrec(nonexhaustive) is_device_ut_cap
|
||||
primrec(nonexhaustive) is_device_untyped_cap
|
||||
where
|
||||
"is_device_ut_cap (UntypedCap isd _ _ _) = isd"
|
||||
"is_device_untyped_cap (UntypedCap isdev _ _ _) = isdev"
|
||||
|
||||
text {* Untyped capabilities note a currently free region. Sometimes this
|
||||
region is reset during a Retype operation. This progressively clears the
|
||||
|
|
@ -161,18 +161,17 @@ where
|
|||
sz \<leftarrow> returnOk $ bits_of cap;
|
||||
base \<leftarrow> returnOk $ obj_ref_of cap;
|
||||
liftE $ delete_objects base sz;
|
||||
dev \<leftarrow> returnOk $ is_device_untyped_cap cap;
|
||||
|
||||
if sz < reset_chunk_bits
|
||||
if dev \<or> sz < reset_chunk_bits
|
||||
then liftE $ do
|
||||
do_machine_op $ clearMemory base (2 ^ sz);
|
||||
set_cap (UntypedCap (is_device_ut_cap cap)
|
||||
(obj_ref_of cap) (bits_of cap) 0) src_slot
|
||||
unless dev $ do_machine_op $ clearMemory base (2 ^ sz);
|
||||
set_cap (UntypedCap dev base sz 0) src_slot
|
||||
od
|
||||
else mapME_x (\<lambda>i. doE
|
||||
liftE $ do_machine_op $ clearMemory (base + (of_nat i << reset_chunk_bits))
|
||||
(2 ^ reset_chunk_bits);
|
||||
liftE $ set_cap (UntypedCap (is_device_ut_cap cap)
|
||||
(obj_ref_of cap) (bits_of cap)
|
||||
liftE $ set_cap (UntypedCap dev base sz
|
||||
(i * 2 ^ reset_chunk_bits)) src_slot;
|
||||
preemption_point
|
||||
odE) (rev [i \<leftarrow> [0 ..< 2 ^ (sz - reset_chunk_bits)].
|
||||
|
|
|
|||
|
|
@ -648,6 +648,9 @@ isPhysicalCap :: "arch_capability \<Rightarrow> bool"
|
|||
consts'
|
||||
sameObjectAs :: "arch_capability \<Rightarrow> arch_capability \<Rightarrow> bool"
|
||||
|
||||
consts'
|
||||
placeNewDataObject :: "machine_word \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
createObject :: "object_type \<Rightarrow> machine_word \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> arch_capability kernel"
|
||||
|
||||
|
|
|
|||
|
|
@ -205,17 +205,10 @@ defs sameObjectAs_def:
|
|||
else sameRegionAs a b
|
||||
)"
|
||||
|
||||
definition
|
||||
"createPageObject ptr numPages isDevice \<equiv>
|
||||
if isDevice then (do
|
||||
addrs \<leftarrow> placeNewObject ptr UserDataDevice numPages;
|
||||
return addrs
|
||||
od)
|
||||
else (do
|
||||
addrs \<leftarrow> placeNewObject ptr UserData numPages;
|
||||
doMachineOp $ initMemory (PPtr $ fromPPtr ptr) (1 `~shiftL~` (pageBits + numPages) );
|
||||
return addrs
|
||||
od)"
|
||||
defs placeNewDataObject_def:
|
||||
"placeNewDataObject regionBase sz isDevice \<equiv> if isDevice
|
||||
then placeNewObject regionBase UserDataDevice sz
|
||||
else placeNewObject regionBase UserData sz"
|
||||
|
||||
defs createObject_def:
|
||||
"createObject t regionBase arg3 isDevice \<equiv>
|
||||
|
|
@ -225,7 +218,7 @@ defs createObject_def:
|
|||
APIObjectType v2 \<Rightarrow>
|
||||
haskell_fail []
|
||||
| SmallPageObject \<Rightarrow> (do
|
||||
createPageObject regionBase 0 isDevice;
|
||||
placeNewDataObject regionBase 0 isDevice;
|
||||
modify (\<lambda> ks. ks \<lparr> gsUserPages :=
|
||||
funupd (gsUserPages ks)
|
||||
(fromPPtr regionBase) (Just ARMSmallPage)\<rparr>);
|
||||
|
|
@ -233,7 +226,7 @@ defs createObject_def:
|
|||
VMReadWrite ARMSmallPage Nothing
|
||||
od)
|
||||
| LargePageObject \<Rightarrow> (do
|
||||
createPageObject regionBase 4 isDevice;
|
||||
placeNewDataObject regionBase 4 isDevice;
|
||||
modify (\<lambda> ks. ks \<lparr> gsUserPages :=
|
||||
funupd (gsUserPages ks)
|
||||
(fromPPtr regionBase) (Just ARMLargePage)\<rparr>);
|
||||
|
|
@ -241,7 +234,7 @@ defs createObject_def:
|
|||
VMReadWrite ARMLargePage Nothing
|
||||
od)
|
||||
| SectionObject \<Rightarrow> (do
|
||||
createPageObject regionBase 8 isDevice;
|
||||
placeNewDataObject regionBase 8 isDevice;
|
||||
modify (\<lambda> ks. ks \<lparr> gsUserPages :=
|
||||
funupd (gsUserPages ks)
|
||||
(fromPPtr regionBase) (Just ARMSection)\<rparr>);
|
||||
|
|
@ -249,7 +242,7 @@ defs createObject_def:
|
|||
VMReadWrite ARMSection Nothing
|
||||
od)
|
||||
| SuperSectionObject \<Rightarrow> (do
|
||||
createPageObject regionBase 12 isDevice;
|
||||
placeNewDataObject regionBase 12 isDevice;
|
||||
modify (\<lambda> ks. ks \<lparr> gsUserPages :=
|
||||
funupd (gsUserPages ks)
|
||||
(fromPPtr regionBase) (Just ARMSuperSection)\<rparr>);
|
||||
|
|
@ -258,12 +251,7 @@ defs createObject_def:
|
|||
od)
|
||||
| PageTableObject \<Rightarrow> (do
|
||||
ptSize \<leftarrow> return ( ptBits - objBits (makeObject ::pte));
|
||||
regionSize \<leftarrow> return ( (1 `~shiftL~` ptBits));
|
||||
placeNewObject regionBase (makeObject ::pte) ptSize;
|
||||
doMachineOp $
|
||||
cleanCacheRange_PoU (VPtr $ fromPPtr regionBase)
|
||||
(VPtr $ fromPPtr regionBase + regionSize - 1)
|
||||
(addrFromPPtr regionBase);
|
||||
return $ PageTableCap (pointerCast regionBase) Nothing
|
||||
od)
|
||||
| PageDirectoryObject \<Rightarrow> (do
|
||||
|
|
|
|||
|
|
@ -45,14 +45,6 @@ createNewCaps :: "object_type \<Rightarrow> machine_word \<Rightarrow> nat \<Rig
|
|||
consts
|
||||
Arch_createNewCaps :: "object_type \<Rightarrow> machine_word \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> arch_capability list kernel"
|
||||
thm injectKO_defs
|
||||
definition
|
||||
"createWordObjects ptr numObjects gs dev\<equiv> (do
|
||||
gbits \<leftarrow> return (pageBits + gs);
|
||||
addrs \<leftarrow> createObjects ptr numObjects (if dev then KOUserDataDevice else KOUserData) gs;
|
||||
unless dev $ doMachineOp $ mapM_x (\<lambda>x. clearMemory (PPtr $ fromPPtr x) ((1::nat) `~shiftL~` gbits)) addrs;
|
||||
return addrs
|
||||
od)"
|
||||
|
||||
defs insertNewCaps_def:
|
||||
"insertNewCaps newType srcSlot destSlots regionBase magnitudeBits dev \<equiv> (do
|
||||
caps \<leftarrow> createNewCaps newType regionBase (length destSlots) magnitudeBits dev ;
|
||||
|
|
@ -61,12 +53,13 @@ od)"
|
|||
|
||||
defs (in Arch) Arch_createNewCaps_def:
|
||||
"Arch_createNewCaps t regionBase numObjects arg4 dev \<equiv>
|
||||
let pointerCast = PPtr \<circ> fromPPtr
|
||||
let pointerCast = PPtr \<circ> fromPPtr;
|
||||
Data = (if dev then KOUserDataDevice else KOUserData)
|
||||
in (case t of
|
||||
APIObjectType v5 \<Rightarrow>
|
||||
haskell_fail []
|
||||
| SmallPageObject \<Rightarrow> (do
|
||||
addrs \<leftarrow> createWordObjects regionBase numObjects 0 dev;
|
||||
addrs \<leftarrow> createObjects regionBase numObjects Data 0;
|
||||
modify (\<lambda> ks. ks \<lparr> gsUserPages := (\<lambda> addr.
|
||||
if addr `~elem~` map fromPPtr addrs then Just ARMSmallPage
|
||||
else gsUserPages ks addr)\<rparr>);
|
||||
|
|
@ -74,7 +67,7 @@ defs (in Arch) Arch_createNewCaps_def:
|
|||
ARMSmallPage Nothing) addrs
|
||||
od)
|
||||
| LargePageObject \<Rightarrow> (do
|
||||
addrs \<leftarrow> createWordObjects regionBase numObjects 4 dev;
|
||||
addrs \<leftarrow> createObjects regionBase numObjects Data 4;
|
||||
modify (\<lambda> ks. ks \<lparr> gsUserPages := (\<lambda> addr.
|
||||
if addr `~elem~` map fromPPtr addrs then Just ARMLargePage
|
||||
else gsUserPages ks addr)\<rparr>);
|
||||
|
|
@ -82,7 +75,7 @@ defs (in Arch) Arch_createNewCaps_def:
|
|||
ARMLargePage Nothing) addrs
|
||||
od)
|
||||
| SectionObject \<Rightarrow> (do
|
||||
addrs \<leftarrow> createWordObjects regionBase numObjects 8 dev;
|
||||
addrs \<leftarrow> createObjects regionBase numObjects Data 8;
|
||||
modify (\<lambda> ks. ks \<lparr> gsUserPages := (\<lambda> addr.
|
||||
if addr `~elem~` map fromPPtr addrs then Just ARMSection
|
||||
else gsUserPages ks addr)\<rparr>);
|
||||
|
|
@ -90,7 +83,7 @@ defs (in Arch) Arch_createNewCaps_def:
|
|||
ARMSection Nothing) addrs
|
||||
od)
|
||||
| SuperSectionObject \<Rightarrow> (do
|
||||
addrs \<leftarrow> createWordObjects regionBase numObjects 12 dev;
|
||||
addrs \<leftarrow> createObjects regionBase numObjects Data 12;
|
||||
modify (\<lambda> ks. ks \<lparr> gsUserPages := (\<lambda> addr.
|
||||
if addr `~elem~` map fromPPtr addrs then Just ARMSuperSection
|
||||
else gsUserPages ks addr)\<rparr>);
|
||||
|
|
@ -102,9 +95,6 @@ defs (in Arch) Arch_createNewCaps_def:
|
|||
addrs \<leftarrow> createObjects regionBase numObjects (injectKO (makeObject ::pte)) ptSize;
|
||||
objSize \<leftarrow> return (((1::nat) `~shiftL~` ptBits));
|
||||
pts \<leftarrow> return ( map pointerCast addrs);
|
||||
doMachineOp $ mapM_x (flip clearMemoryVM ptBits) pts;
|
||||
doMachineOp $ mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + (fromIntegral objSize) - 1)
|
||||
(addrFromPPtr x)) pts;
|
||||
return $ map (\<lambda> pt. PageTableCap pt Nothing) pts
|
||||
od)
|
||||
| PageDirectoryObject \<Rightarrow> (do
|
||||
|
|
@ -112,7 +102,6 @@ defs (in Arch) Arch_createNewCaps_def:
|
|||
addrs \<leftarrow> createObjects regionBase numObjects (injectKO (makeObject ::pde)) pdSize;
|
||||
objSize \<leftarrow> return ( ((1::nat) `~shiftL~` pdBits));
|
||||
pds \<leftarrow> return ( map pointerCast addrs);
|
||||
doMachineOp $ mapM_x (flip clearMemoryVM pdBits) pds;
|
||||
mapM_x copyGlobalMappings pds;
|
||||
doMachineOp $ mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + (fromIntegral objSize) - 1)
|
||||
(addrFromPPtr x)) pds;
|
||||
|
|
|
|||
|
|
@ -49,5 +49,10 @@ retypeFanOutLimit :: "machine_word"
|
|||
where
|
||||
"retypeFanOutLimit \<equiv> 256"
|
||||
|
||||
definition
|
||||
resetChunkBits :: "nat"
|
||||
where
|
||||
"resetChunkBits \<equiv> 8"
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -563,82 +563,92 @@ where
|
|||
| _ \<Rightarrow> False"
|
||||
|
||||
datatype untyped_invocation =
|
||||
Retype machine_word machine_word machine_word object_type nat "machine_word list" bool
|
||||
Retype machine_word bool machine_word machine_word object_type nat "machine_word list" bool
|
||||
|
||||
primrec
|
||||
retypeSource :: "untyped_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"retypeSource (Retype v0 v1 v2 v3 v4 v5 v6) = v0"
|
||||
"retypeSource (Retype v0 v1 v2 v3 v4 v5 v6 v7) = v0"
|
||||
|
||||
primrec
|
||||
retypeNewType :: "untyped_invocation \<Rightarrow> object_type"
|
||||
where
|
||||
"retypeNewType (Retype v0 v1 v2 v3 v4 v5 v6) = v3"
|
||||
"retypeNewType (Retype v0 v1 v2 v3 v4 v5 v6 v7) = v4"
|
||||
|
||||
primrec
|
||||
retypeIsDevice :: "untyped_invocation \<Rightarrow> bool"
|
||||
where
|
||||
"retypeIsDevice (Retype v0 v1 v2 v3 v4 v5 v6) = v6"
|
||||
"retypeIsDevice (Retype v0 v1 v2 v3 v4 v5 v6 v7) = v7"
|
||||
|
||||
primrec
|
||||
retypeRegionBase :: "untyped_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"retypeRegionBase (Retype v0 v1 v2 v3 v4 v5 v6) = v1"
|
||||
"retypeRegionBase (Retype v0 v1 v2 v3 v4 v5 v6 v7) = v2"
|
||||
|
||||
primrec
|
||||
retypeSlots :: "untyped_invocation \<Rightarrow> machine_word list"
|
||||
where
|
||||
"retypeSlots (Retype v0 v1 v2 v3 v4 v5 v6) = v5"
|
||||
"retypeSlots (Retype v0 v1 v2 v3 v4 v5 v6 v7) = v6"
|
||||
|
||||
primrec
|
||||
retypeResetUntyped :: "untyped_invocation \<Rightarrow> bool"
|
||||
where
|
||||
"retypeResetUntyped (Retype v0 v1 v2 v3 v4 v5 v6 v7) = v1"
|
||||
|
||||
primrec
|
||||
retypeFreeRegionBase :: "untyped_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"retypeFreeRegionBase (Retype v0 v1 v2 v3 v4 v5 v6) = v2"
|
||||
"retypeFreeRegionBase (Retype v0 v1 v2 v3 v4 v5 v6 v7) = v3"
|
||||
|
||||
primrec
|
||||
retypeNewSizeBits :: "untyped_invocation \<Rightarrow> nat"
|
||||
where
|
||||
"retypeNewSizeBits (Retype v0 v1 v2 v3 v4 v5 v6) = v4"
|
||||
"retypeNewSizeBits (Retype v0 v1 v2 v3 v4 v5 v6 v7) = v5"
|
||||
|
||||
primrec
|
||||
retypeSource_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> untyped_invocation \<Rightarrow> untyped_invocation"
|
||||
where
|
||||
"retypeSource_update f (Retype v0 v1 v2 v3 v4 v5 v6) = Retype (f v0) v1 v2 v3 v4 v5 v6"
|
||||
"retypeSource_update f (Retype v0 v1 v2 v3 v4 v5 v6 v7) = Retype (f v0) v1 v2 v3 v4 v5 v6 v7"
|
||||
|
||||
primrec
|
||||
retypeNewType_update :: "(object_type \<Rightarrow> object_type) \<Rightarrow> untyped_invocation \<Rightarrow> untyped_invocation"
|
||||
where
|
||||
"retypeNewType_update f (Retype v0 v1 v2 v3 v4 v5 v6) = Retype v0 v1 v2 (f v3) v4 v5 v6"
|
||||
"retypeNewType_update f (Retype v0 v1 v2 v3 v4 v5 v6 v7) = Retype v0 v1 v2 v3 (f v4) v5 v6 v7"
|
||||
|
||||
primrec
|
||||
retypeIsDevice_update :: "(bool \<Rightarrow> bool) \<Rightarrow> untyped_invocation \<Rightarrow> untyped_invocation"
|
||||
where
|
||||
"retypeIsDevice_update f (Retype v0 v1 v2 v3 v4 v5 v6) = Retype v0 v1 v2 v3 v4 v5 (f v6)"
|
||||
"retypeIsDevice_update f (Retype v0 v1 v2 v3 v4 v5 v6 v7) = Retype v0 v1 v2 v3 v4 v5 v6 (f v7)"
|
||||
|
||||
primrec
|
||||
retypeRegionBase_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> untyped_invocation \<Rightarrow> untyped_invocation"
|
||||
where
|
||||
"retypeRegionBase_update f (Retype v0 v1 v2 v3 v4 v5 v6) = Retype v0 (f v1) v2 v3 v4 v5 v6"
|
||||
"retypeRegionBase_update f (Retype v0 v1 v2 v3 v4 v5 v6 v7) = Retype v0 v1 (f v2) v3 v4 v5 v6 v7"
|
||||
|
||||
primrec
|
||||
retypeSlots_update :: "((machine_word list) \<Rightarrow> (machine_word list)) \<Rightarrow> untyped_invocation \<Rightarrow> untyped_invocation"
|
||||
where
|
||||
"retypeSlots_update f (Retype v0 v1 v2 v3 v4 v5 v6) = Retype v0 v1 v2 v3 v4 (f v5) v6"
|
||||
"retypeSlots_update f (Retype v0 v1 v2 v3 v4 v5 v6 v7) = Retype v0 v1 v2 v3 v4 v5 (f v6) v7"
|
||||
|
||||
primrec
|
||||
retypeResetUntyped_update :: "(bool \<Rightarrow> bool) \<Rightarrow> untyped_invocation \<Rightarrow> untyped_invocation"
|
||||
where
|
||||
"retypeResetUntyped_update f (Retype v0 v1 v2 v3 v4 v5 v6 v7) = Retype v0 (f v1) v2 v3 v4 v5 v6 v7"
|
||||
|
||||
primrec
|
||||
retypeFreeRegionBase_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> untyped_invocation \<Rightarrow> untyped_invocation"
|
||||
where
|
||||
"retypeFreeRegionBase_update f (Retype v0 v1 v2 v3 v4 v5 v6) = Retype v0 v1 (f v2) v3 v4 v5 v6"
|
||||
"retypeFreeRegionBase_update f (Retype v0 v1 v2 v3 v4 v5 v6 v7) = Retype v0 v1 v2 (f v3) v4 v5 v6 v7"
|
||||
|
||||
primrec
|
||||
retypeNewSizeBits_update :: "(nat \<Rightarrow> nat) \<Rightarrow> untyped_invocation \<Rightarrow> untyped_invocation"
|
||||
where
|
||||
"retypeNewSizeBits_update f (Retype v0 v1 v2 v3 v4 v5 v6) = Retype v0 v1 v2 v3 (f v4) v5 v6"
|
||||
"retypeNewSizeBits_update f (Retype v0 v1 v2 v3 v4 v5 v6 v7) = Retype v0 v1 v2 v3 v4 (f v5) v6 v7"
|
||||
|
||||
abbreviation (input)
|
||||
Retype_trans :: "(machine_word) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> (object_type) \<Rightarrow> (nat) \<Rightarrow> (machine_word list) \<Rightarrow> (bool) \<Rightarrow> untyped_invocation" ("Retype'_ \<lparr> retypeSource= _, retypeRegionBase= _, retypeFreeRegionBase= _, retypeNewType= _, retypeNewSizeBits= _, retypeSlots= _, retypeIsDevice= _ \<rparr>")
|
||||
Retype_trans :: "(machine_word) \<Rightarrow> (bool) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> (object_type) \<Rightarrow> (nat) \<Rightarrow> (machine_word list) \<Rightarrow> (bool) \<Rightarrow> untyped_invocation" ("Retype'_ \<lparr> retypeSource= _, retypeResetUntyped= _, retypeRegionBase= _, retypeFreeRegionBase= _, retypeNewType= _, retypeNewSizeBits= _, retypeSlots= _, retypeIsDevice= _ \<rparr>")
|
||||
where
|
||||
"Retype_ \<lparr> retypeSource= v0, retypeRegionBase= v1, retypeFreeRegionBase= v2, retypeNewType= v3, retypeNewSizeBits= v4, retypeSlots= v5, retypeIsDevice= v6 \<rparr> == Retype v0 v1 v2 v3 v4 v5 v6"
|
||||
"Retype_ \<lparr> retypeSource= v0, retypeResetUntyped= v1, retypeRegionBase= v2, retypeFreeRegionBase= v3, retypeNewType= v4, retypeNewSizeBits= v5, retypeSlots= v6, retypeIsDevice= v7 \<rparr> == Retype v0 v1 v2 v3 v4 v5 v6 v7"
|
||||
|
||||
lemma retypeSource_retypeSource_update [simp]:
|
||||
"retypeSource (retypeSource_update f v) = f (retypeSource v)"
|
||||
|
|
@ -660,6 +670,10 @@ lemma retypeSource_retypeSlots_update [simp]:
|
|||
"retypeSource (retypeSlots_update f v) = retypeSource v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeSource_retypeResetUntyped_update [simp]:
|
||||
"retypeSource (retypeResetUntyped_update f v) = retypeSource v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeSource_retypeFreeRegionBase_update [simp]:
|
||||
"retypeSource (retypeFreeRegionBase_update f v) = retypeSource v"
|
||||
by (cases v) simp
|
||||
|
|
@ -688,6 +702,10 @@ lemma retypeNewType_retypeSlots_update [simp]:
|
|||
"retypeNewType (retypeSlots_update f v) = retypeNewType v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeNewType_retypeResetUntyped_update [simp]:
|
||||
"retypeNewType (retypeResetUntyped_update f v) = retypeNewType v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeNewType_retypeFreeRegionBase_update [simp]:
|
||||
"retypeNewType (retypeFreeRegionBase_update f v) = retypeNewType v"
|
||||
by (cases v) simp
|
||||
|
|
@ -716,6 +734,10 @@ lemma retypeIsDevice_retypeSlots_update [simp]:
|
|||
"retypeIsDevice (retypeSlots_update f v) = retypeIsDevice v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeIsDevice_retypeResetUntyped_update [simp]:
|
||||
"retypeIsDevice (retypeResetUntyped_update f v) = retypeIsDevice v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeIsDevice_retypeFreeRegionBase_update [simp]:
|
||||
"retypeIsDevice (retypeFreeRegionBase_update f v) = retypeIsDevice v"
|
||||
by (cases v) simp
|
||||
|
|
@ -744,6 +766,10 @@ lemma retypeRegionBase_retypeSlots_update [simp]:
|
|||
"retypeRegionBase (retypeSlots_update f v) = retypeRegionBase v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeRegionBase_retypeResetUntyped_update [simp]:
|
||||
"retypeRegionBase (retypeResetUntyped_update f v) = retypeRegionBase v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeRegionBase_retypeFreeRegionBase_update [simp]:
|
||||
"retypeRegionBase (retypeFreeRegionBase_update f v) = retypeRegionBase v"
|
||||
by (cases v) simp
|
||||
|
|
@ -772,6 +798,10 @@ lemma retypeSlots_retypeSlots_update [simp]:
|
|||
"retypeSlots (retypeSlots_update f v) = f (retypeSlots v)"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeSlots_retypeResetUntyped_update [simp]:
|
||||
"retypeSlots (retypeResetUntyped_update f v) = retypeSlots v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeSlots_retypeFreeRegionBase_update [simp]:
|
||||
"retypeSlots (retypeFreeRegionBase_update f v) = retypeSlots v"
|
||||
by (cases v) simp
|
||||
|
|
@ -780,6 +810,38 @@ lemma retypeSlots_retypeNewSizeBits_update [simp]:
|
|||
"retypeSlots (retypeNewSizeBits_update f v) = retypeSlots v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeResetUntyped_retypeSource_update [simp]:
|
||||
"retypeResetUntyped (retypeSource_update f v) = retypeResetUntyped v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeResetUntyped_retypeNewType_update [simp]:
|
||||
"retypeResetUntyped (retypeNewType_update f v) = retypeResetUntyped v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeResetUntyped_retypeIsDevice_update [simp]:
|
||||
"retypeResetUntyped (retypeIsDevice_update f v) = retypeResetUntyped v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeResetUntyped_retypeRegionBase_update [simp]:
|
||||
"retypeResetUntyped (retypeRegionBase_update f v) = retypeResetUntyped v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeResetUntyped_retypeSlots_update [simp]:
|
||||
"retypeResetUntyped (retypeSlots_update f v) = retypeResetUntyped v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeResetUntyped_retypeResetUntyped_update [simp]:
|
||||
"retypeResetUntyped (retypeResetUntyped_update f v) = f (retypeResetUntyped v)"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeResetUntyped_retypeFreeRegionBase_update [simp]:
|
||||
"retypeResetUntyped (retypeFreeRegionBase_update f v) = retypeResetUntyped v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeResetUntyped_retypeNewSizeBits_update [simp]:
|
||||
"retypeResetUntyped (retypeNewSizeBits_update f v) = retypeResetUntyped v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeFreeRegionBase_retypeSource_update [simp]:
|
||||
"retypeFreeRegionBase (retypeSource_update f v) = retypeFreeRegionBase v"
|
||||
by (cases v) simp
|
||||
|
|
@ -800,6 +862,10 @@ lemma retypeFreeRegionBase_retypeSlots_update [simp]:
|
|||
"retypeFreeRegionBase (retypeSlots_update f v) = retypeFreeRegionBase v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeFreeRegionBase_retypeResetUntyped_update [simp]:
|
||||
"retypeFreeRegionBase (retypeResetUntyped_update f v) = retypeFreeRegionBase v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeFreeRegionBase_retypeFreeRegionBase_update [simp]:
|
||||
"retypeFreeRegionBase (retypeFreeRegionBase_update f v) = f (retypeFreeRegionBase v)"
|
||||
by (cases v) simp
|
||||
|
|
@ -828,6 +894,10 @@ lemma retypeNewSizeBits_retypeSlots_update [simp]:
|
|||
"retypeNewSizeBits (retypeSlots_update f v) = retypeNewSizeBits v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeNewSizeBits_retypeResetUntyped_update [simp]:
|
||||
"retypeNewSizeBits (retypeResetUntyped_update f v) = retypeNewSizeBits v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma retypeNewSizeBits_retypeFreeRegionBase_update [simp]:
|
||||
"retypeNewSizeBits (retypeFreeRegionBase_update f v) = retypeNewSizeBits v"
|
||||
by (cases v) simp
|
||||
|
|
|
|||
|
|
@ -410,7 +410,7 @@ defs decodeInvocation_def:
|
|||
defs performInvocation_def:
|
||||
"performInvocation block call x2\<equiv> (case x2 of
|
||||
(InvokeUntyped invok) \<Rightarrow> (doE
|
||||
withoutPreemption $ invokeUntyped invok;
|
||||
invokeUntyped invok;
|
||||
returnOk $ []
|
||||
odE)
|
||||
| (InvokeEndpoint ep badge canGrant) \<Rightarrow>
|
||||
|
|
|
|||
|
|
@ -20,6 +20,7 @@ imports
|
|||
Invocations_H
|
||||
InvocationLabels_H
|
||||
Config_H
|
||||
"../machine/MachineExports"
|
||||
begin
|
||||
|
||||
consts
|
||||
|
|
@ -78,10 +79,11 @@ where
|
|||
mapM (locateSlotCap nodeCap)
|
||||
[nodeOffset .e. nodeOffset+nodeWindow - 1];
|
||||
mapME_x ensureEmptySlot slots;
|
||||
freeIndex \<leftarrow> withoutFailure $ constOnFailure (capFreeIndex cap) $ (doE
|
||||
reset \<leftarrow> withoutFailure $ constOnFailure False $ (doE
|
||||
ensureNoChildren slot;
|
||||
returnOk 0
|
||||
returnOk True
|
||||
odE);
|
||||
freeIndex \<leftarrow> returnOk ( if reset then 0 else capFreeIndex cap);
|
||||
freeRef \<leftarrow> returnOk ( getFreeRef (capPtr cap) freeIndex);
|
||||
objectSize \<leftarrow> returnOk ( getObjectSize newType userObjSize);
|
||||
untypedFreeBytes \<leftarrow> returnOk ( (bit (capBlockSize cap)) - freeIndex);
|
||||
|
|
@ -95,6 +97,7 @@ where
|
|||
alignedFreeRef \<leftarrow> returnOk ( PPtr $ alignUp (fromPPtr freeRef) objectSize);
|
||||
returnOk $ Retype_ \<lparr>
|
||||
retypeSource= slot,
|
||||
retypeResetUntyped= reset,
|
||||
retypeRegionBase= capPtr cap,
|
||||
retypeFreeRegionBase= alignedFreeRef,
|
||||
retypeNewType= newType,
|
||||
|
|
@ -109,22 +112,50 @@ where
|
|||
)"
|
||||
|
||||
definition
|
||||
invokeUntyped :: "untyped_invocation \<Rightarrow> unit kernel"
|
||||
resetUntypedCap :: "machine_word \<Rightarrow> unit kernel_p"
|
||||
where
|
||||
"resetUntypedCap slot\<equiv> (doE
|
||||
cap \<leftarrow> withoutPreemption $ getSlotCap slot;
|
||||
sz \<leftarrow> returnOk ( capBlockSize cap);
|
||||
withoutPreemption $ deleteObjects (capPtr cap) sz;
|
||||
if (capIsDevice cap \<or> sz < resetChunkBits)
|
||||
then withoutPreemption $ (do
|
||||
unless (capIsDevice cap) $ doMachineOp $
|
||||
clearMemory (PPtr (fromPPtr (capPtr cap))) (1 `~shiftL~` sz);
|
||||
updateCap slot (cap \<lparr>capFreeIndex := 0\<rparr>)
|
||||
od)
|
||||
else (
|
||||
forME_x (reverse [capPtr cap, capPtr cap + (1 `~shiftL~` resetChunkBits) .e.
|
||||
getFreeRef (capPtr cap) (capFreeIndex cap) - 1])
|
||||
(\<lambda> addr. (doE
|
||||
withoutPreemption $ doMachineOp $ clearMemory
|
||||
(PPtr (fromPPtr addr)) (1 `~shiftL~` resetChunkBits);
|
||||
withoutPreemption $ updateCap slot (cap \<lparr>capFreeIndex
|
||||
:= getFreeIndex (capPtr cap) addr\<rparr>);
|
||||
preemptionPoint
|
||||
odE))
|
||||
)
|
||||
odE)"
|
||||
|
||||
definition
|
||||
invokeUntyped :: "untyped_invocation \<Rightarrow> unit kernel_p"
|
||||
where
|
||||
"invokeUntyped x0\<equiv> (case x0 of
|
||||
(Retype srcSlot base freeRegionBase newType userSize destSlots isDevice) \<Rightarrow> (do
|
||||
cap \<leftarrow> getSlotCap srcSlot;
|
||||
when (base = freeRegionBase) $
|
||||
deleteObjects base (capBlockSize cap);
|
||||
totalObjectSize \<leftarrow> return ( (length destSlots) `~shiftL~` (getObjectSize newType userSize));
|
||||
stateAssert (\<lambda> x. Not (cNodeOverlap (gsCNodes x)
|
||||
(\<lambda> x. fromPPtr freeRegionBase \<le> x
|
||||
\<and> x \<le> fromPPtr freeRegionBase + fromIntegral totalObjectSize - 1)))
|
||||
[];
|
||||
freeRef \<leftarrow> return ( freeRegionBase + PPtr (fromIntegral totalObjectSize));
|
||||
updateCap srcSlot (cap \<lparr>capFreeIndex := getFreeIndex base freeRef\<rparr>);
|
||||
createNewObjects newType srcSlot destSlots freeRegionBase userSize isDevice
|
||||
(Retype srcSlot reset base retypeBase newType userSize destSlots isDev) \<Rightarrow> (doE
|
||||
whenE reset $ resetUntypedCap srcSlot;
|
||||
withoutPreemption $ (do
|
||||
cap \<leftarrow> getSlotCap srcSlot;
|
||||
totalObjectSize \<leftarrow> return ( (length destSlots) `~shiftL~` (getObjectSize newType userSize));
|
||||
stateAssert (\<lambda> x. Not (cNodeOverlap (gsCNodes x)
|
||||
(\<lambda> x. fromPPtr retypeBase \<le> x
|
||||
\<and> x \<le> fromPPtr retypeBase + fromIntegral totalObjectSize - 1)))
|
||||
[];
|
||||
freeRef \<leftarrow> return ( retypeBase + PPtr (fromIntegral totalObjectSize));
|
||||
updateCap srcSlot
|
||||
(cap \<lparr>capFreeIndex := getFreeIndex base freeRef\<rparr>);
|
||||
createNewObjects newType srcSlot destSlots retypeBase userSize isDev
|
||||
od)
|
||||
odE)
|
||||
)"
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -18,6 +18,7 @@ imports
|
|||
Invocations_H
|
||||
InvocationLabels_H
|
||||
Config_H
|
||||
"../machine/MachineExports"
|
||||
begin
|
||||
|
||||
consts
|
||||
|
|
|
|||
|
|
@ -1,5 +1,95 @@
|
|||
Built from git repo at /home/matthewb/verification/patch/l4v/spec/haskell by matthewb
|
||||
Built from git repo at /home/tsewell/dev/verification2/l4v/spec/haskell by tsewell
|
||||
|
||||
Generated from changeset:
|
||||
1c569f1 SELFOUR-276: reworked haskell
|
||||
af80ffc Invariants proven for preemptible retype.
|
||||
|
||||
|
||||
Warning - uncomitted changes used:
|
||||
M ../../proof/ROOT
|
||||
M ../../proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy
|
||||
M ../../proof/invariant-abstract/ARM/ArchDeterministic_AI.thy
|
||||
M ../../proof/invariant-abstract/DetSchedAux_AI.thy
|
||||
M ../../proof/invariant-abstract/Deterministic_AI.thy
|
||||
M ../../proof/invariant-abstract/Untyped_AI.thy
|
||||
M ../../proof/refine/ArchAcc_R.thy
|
||||
M ../../proof/refine/Arch_R.thy
|
||||
M ../../proof/refine/CNodeInv_R.thy
|
||||
M ../../proof/refine/CSpace_R.thy
|
||||
MM ../../proof/refine/Detype_R.thy
|
||||
M ../../proof/refine/Finalise_R.thy
|
||||
M ../../proof/refine/InterruptAcc_R.thy
|
||||
M ../../proof/refine/Orphanage.thy
|
||||
M ../../proof/refine/PageTableDuplicates.thy
|
||||
MM ../../proof/refine/Retype_R.thy
|
||||
M ../../proof/refine/Syscall_R.thy
|
||||
MM ../../proof/refine/Untyped_R.thy
|
||||
M ../abstract/Retype_A.thy
|
||||
M ../design/ARM/ArchRetypeDecls_H.thy
|
||||
MM ../design/ARM/ArchRetype_H.thy
|
||||
MM ../design/ARM/Intermediate_H.thy
|
||||
M ../design/Config_H.thy
|
||||
MM ../design/Invocations_H.thy
|
||||
M ../design/Retype_H.thy
|
||||
MM ../design/Untyped_H.thy
|
||||
M ../design/skel/Untyped_H.thy
|
||||
MM ../design/version
|
||||
M src/SEL4/API/Invocation.lhs
|
||||
M src/SEL4/Config.lhs
|
||||
M src/SEL4/Object/ObjectType.lhs
|
||||
M src/SEL4/Object/ObjectType/ARM.lhs
|
||||
M src/SEL4/Object/Untyped.lhs
|
||||
?? ../../Test.thy
|
||||
?? ../../camkes/glue-proofs/umm_types.txt
|
||||
?? ../../lib/Test.thy
|
||||
?? ../../lib/foo.c
|
||||
?? ../../patch
|
||||
?? ../../proof/Ctac.thy
|
||||
?? ../../proof/Old_Arch.thy
|
||||
?? ../../proof/Old_Retype_R.thy
|
||||
?? ../../proof/Old_Untyped_AI.thy
|
||||
?? ../../proof/Test.thy
|
||||
?? ../../proof/asmrefine/CFunDump.txt
|
||||
?? ../../proof/crefine/Test.thy
|
||||
?? ../../proof/foo
|
||||
?? ../../proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy.orig
|
||||
?? ../../proof/invariant-abstract/Arch_AI.thy.orig
|
||||
?? ../../proof/invariant-abstract/BCorres2_AI.thy.orig
|
||||
?? ../../proof/invariant-abstract/CNodeInv_AI.thy.orig
|
||||
?? ../../proof/invariant-abstract/CSpace_AI.thy.orig
|
||||
?? ../../proof/invariant-abstract/DetSchedAux_AI.thy.orig
|
||||
?? ../../proof/invariant-abstract/Deterministic_AI.thy.orig
|
||||
?? ../../proof/invariant-abstract/Finalise_AI.thy.orig
|
||||
?? ../../proof/invariant-abstract/Retype_AI.thy.orig
|
||||
?? ../../proof/invariant-abstract/Untyped_AI.thy.orig
|
||||
?? ../../proof/lhs_pars.py
|
||||
?? ../../proof/refine/.Untyped_R.thy.marks
|
||||
?? ../../proof/refine/Arch_R.thy.orig
|
||||
?? ../../proof/refine/Detype_R.thy.orig
|
||||
?? ../../proof/refine/Orphanage.thy.orig
|
||||
?? ../../proof/refine/PageTableDuplicates.thy.orig
|
||||
?? ../../proof/refine/Retype_R.thy.orig
|
||||
?? ../../proof/refine/Untyped_R.thy.orig
|
||||
?? ../../proof/switch_glob.c
|
||||
?? ../../proof/switch_glob.thy
|
||||
?? ../../proof/untyped.c
|
||||
?? ../abstract/ARM/ArchRetype_A.thy.orig
|
||||
?? ../abstract/Decode_A.thy.orig
|
||||
?? ../abstract/Invocations_A.thy.orig
|
||||
?? ../abstract/Retype_A.thy.orig
|
||||
?? ../cspec/c/foo.c
|
||||
?? ../cspec/c/foo.s
|
||||
?? ../design/ARM/ArchRetype_H.thy.orig
|
||||
?? ../design/ARM/Intermediate_H.thy.orig
|
||||
?? ../design/Invocations_H.thy.orig
|
||||
?? ../design/Untyped_H.thy.orig
|
||||
?? ../design/version.orig
|
||||
?? ../foo.c
|
||||
?? src/SEL4/API/Invocation.lhs.orig
|
||||
?? src/SEL4/Object/ObjectType/ARM.lhs.orig
|
||||
?? src/SEL4/Object/ObjectType/ARM.lhs.rej
|
||||
?? src/SEL4/Object/Untyped.lhs.orig
|
||||
?? src/SEL4/Object/Untyped.lhs.rej
|
||||
?? ../patch
|
||||
?? ../../tools/autocorres/doc/quickstart/umm_types.txt
|
||||
?? ../../tools/autocorres/tests/umm_types.txt
|
||||
?? ../../use-this-isabelle
|
||||
|
|
|
|||
|
|
@ -113,6 +113,7 @@ The following data type defines the parameters expected for invocations of Untyp
|
|||
> data UntypedInvocation
|
||||
> = Retype {
|
||||
> retypeSource :: PPtr CTE,
|
||||
> retypeResetUntyped :: Bool,
|
||||
> retypeRegionBase :: PPtr (),
|
||||
> retypeFreeRegionBase :: PPtr (),
|
||||
> retypeNewType :: ObjectType,
|
||||
|
|
|
|||
|
|
@ -53,3 +53,8 @@ To limit the impact of "Retype" calls on interrupt latency, there is a fixed max
|
|||
> retypeFanOutLimit :: Word
|
||||
> retypeFanOutLimit = 256
|
||||
|
||||
Also related to interrupt latency, clearing of memory before "Retype" is done one chunk at a time, with a configurable chunk size. The chunk size must be a power of two, and is represented by a number of bits.
|
||||
|
||||
> resetChunkBits :: Int
|
||||
> resetChunkBits = 8
|
||||
|
||||
|
|
|
|||
|
|
@ -470,7 +470,7 @@ This function just dispatches invocations to the type-specific invocation functi
|
|||
> performInvocation :: Bool -> Bool -> Invocation -> KernelP [Word]
|
||||
>
|
||||
> performInvocation _ _ (InvokeUntyped invok) = do
|
||||
> withoutPreemption $ invokeUntyped invok
|
||||
> invokeUntyped invok
|
||||
> return $! []
|
||||
>
|
||||
> performInvocation block call (InvokeEndpoint ep badge canGrant) =
|
||||
|
|
|
|||
|
|
@ -208,19 +208,13 @@ All other capabilities need no finalisation action.
|
|||
|
||||
\subsection{Creating New Capabilities}
|
||||
|
||||
Creates a page-sized object that consists of plain words observable to the user.
|
||||
|
||||
> createPageObject ptr numPages isDevice =
|
||||
> if isDevice then do
|
||||
> addrs <- placeNewObject ptr UserDataDevice numPages
|
||||
> return addrs
|
||||
> else do
|
||||
> addrs <- placeNewObject ptr UserData numPages
|
||||
> doMachineOp $ initMemory (PPtr $ fromPPtr ptr) (1 `shiftL` (pageBits + numPages) ) -- only write to non-device pages
|
||||
> return addrs
|
||||
|
||||
Create an architecture-specific object.
|
||||
|
||||
> placeNewDataObject :: PPtr () -> Int -> Bool -> Kernel ()
|
||||
> placeNewDataObject regionBase sz isDevice = if isDevice
|
||||
> then placeNewObject regionBase UserDataDevice sz
|
||||
> else placeNewObject regionBase UserData sz
|
||||
|
||||
> createObject :: ObjectType -> PPtr () -> Int -> Bool -> Kernel ArchCapability
|
||||
> createObject t regionBase _ isDevice =
|
||||
> let funupd = (\f x v y -> if y == x then v else f y) in
|
||||
|
|
@ -229,28 +223,28 @@ Create an architecture-specific object.
|
|||
> Arch.Types.APIObjectType _ ->
|
||||
> fail "Arch.createObject got an API type"
|
||||
> Arch.Types.SmallPageObject -> do
|
||||
> createPageObject regionBase 0 isDevice
|
||||
> placeNewDataObject regionBase 0 isDevice
|
||||
> modify (\ks -> ks { gsUserPages =
|
||||
> funupd (gsUserPages ks)
|
||||
> (fromPPtr regionBase) (Just ARMSmallPage)})
|
||||
> return $! PageCap isDevice (pointerCast regionBase)
|
||||
> VMReadWrite ARMSmallPage Nothing
|
||||
> Arch.Types.LargePageObject -> do
|
||||
> createPageObject regionBase 4 isDevice
|
||||
> placeNewDataObject regionBase 4 isDevice
|
||||
> modify (\ks -> ks { gsUserPages =
|
||||
> funupd (gsUserPages ks)
|
||||
> (fromPPtr regionBase) (Just ARMLargePage)})
|
||||
> return $! PageCap isDevice (pointerCast regionBase)
|
||||
> VMReadWrite ARMLargePage Nothing
|
||||
> Arch.Types.SectionObject -> do
|
||||
> createPageObject regionBase 8 isDevice
|
||||
> placeNewDataObject regionBase 8 isDevice
|
||||
> modify (\ks -> ks { gsUserPages =
|
||||
> funupd (gsUserPages ks)
|
||||
> (fromPPtr regionBase) (Just ARMSection)})
|
||||
> return $! PageCap isDevice (pointerCast regionBase)
|
||||
> VMReadWrite ARMSection Nothing
|
||||
> Arch.Types.SuperSectionObject -> do
|
||||
> createPageObject regionBase 12 isDevice
|
||||
> placeNewDataObject regionBase 12 isDevice
|
||||
> modify (\ks -> ks { gsUserPages =
|
||||
> funupd (gsUserPages ks)
|
||||
> (fromPPtr regionBase) (Just ARMSuperSection)})
|
||||
|
|
@ -258,12 +252,7 @@ Create an architecture-specific object.
|
|||
> VMReadWrite ARMSuperSection Nothing
|
||||
> Arch.Types.PageTableObject -> do
|
||||
> let ptSize = ptBits - objBits (makeObject :: PTE)
|
||||
> let regionSize = (1 `shiftL` ptBits)
|
||||
> placeNewObject regionBase (makeObject :: PTE) ptSize
|
||||
> doMachineOp $
|
||||
> cleanCacheRange_PoU (VPtr $ fromPPtr regionBase)
|
||||
> (VPtr $ fromPPtr regionBase + regionSize - 1)
|
||||
> (addrFromPPtr regionBase)
|
||||
> return $! PageTableCap (pointerCast regionBase) Nothing
|
||||
> Arch.Types.PageDirectoryObject -> do
|
||||
> let pdSize = pdBits - objBits (makeObject :: PDE)
|
||||
|
|
|
|||
|
|
@ -128,11 +128,15 @@ The destination slots must all be empty. If any of them contains a capability, t
|
|||
|
||||
> mapM_ ensureEmptySlot slots
|
||||
|
||||
Find out how much free room is available in the Untyped. If we discover that we don't have any children (for instance, they have all been manually deleted), we can just start allocating from the beginning of region again.
|
||||
If we discover we don't have any children (for instance, they have all been manually deleted), we reset the untyped region, clearing any memory that had been used.
|
||||
|
||||
> freeIndex <- withoutFailure $ constOnFailure (capFreeIndex cap) $ do
|
||||
> reset <- withoutFailure $ constOnFailure False $ do
|
||||
> ensureNoChildren slot
|
||||
> return 0
|
||||
> return True
|
||||
|
||||
The memory free for use begins at the current free pointer, unless we are performing a reset, in which case it begins at the start of the region.
|
||||
|
||||
> let freeIndex = if reset then 0 else capFreeIndex cap
|
||||
> let freeRef = getFreeRef (capPtr cap) freeIndex
|
||||
|
||||
Ensure that sufficient space is available in the region of memory.
|
||||
|
|
@ -157,6 +161,7 @@ Align up the free region pointer to ensure that created objects are aligned to t
|
|||
|
||||
> return $! Retype {
|
||||
> retypeSource = slot,
|
||||
> retypeResetUntyped = reset,
|
||||
> retypeRegionBase = capPtr cap,
|
||||
> retypeFreeRegionBase = alignedFreeRef,
|
||||
> retypeNewType = newType,
|
||||
|
|
@ -169,35 +174,57 @@ Align up the free region pointer to ensure that created objects are aligned to t
|
|||
> then TruncatedMessage
|
||||
> else IllegalOperation
|
||||
|
||||
> invokeUntyped :: UntypedInvocation -> Kernel ()
|
||||
> invokeUntyped (Retype srcSlot base freeRegionBase newType userSize destSlots isDevice) = do
|
||||
A Retype operation may begin with a reset of an Untyped cap. This returns the free space pointer to the start of the Untyped region. For large regions this is done preemptibly, one chunk at a time.
|
||||
|
||||
> cap <- getSlotCap srcSlot
|
||||
> resetUntypedCap :: PPtr CTE -> KernelP ()
|
||||
> resetUntypedCap slot = do
|
||||
> cap <- withoutPreemption $ getSlotCap slot
|
||||
> let sz = capBlockSize cap
|
||||
|
||||
\begin{impdetails}
|
||||
The following code removes any existing objects in the physical memory region. This operation is specific to the Haskell physical memory model, in which memory objects are typed; it is not necessary (or possible) when running on real hardware.
|
||||
|
||||
> when (base == freeRegionBase) $
|
||||
> deleteObjects base (capBlockSize cap)
|
||||
The objects in the Haskell model are removed at this time. This operation is specific to the Haskell physical memory model, in which memory objects are typed; it is not necessary (or possible) when running on real hardware.
|
||||
|
||||
> withoutPreemption $ deleteObjects (capPtr cap) sz
|
||||
|
||||
\end{impdetails}
|
||||
|
||||
Update the untyped capability we are using to create these objects to record that this space now has objects in it.
|
||||
> if (capIsDevice cap || sz < resetChunkBits)
|
||||
> then withoutPreemption $ do
|
||||
> unless (capIsDevice cap) $ doMachineOp $
|
||||
> clearMemory (PPtr (fromPPtr (capPtr cap))) (1 `shiftL` sz)
|
||||
> updateCap slot (cap {capFreeIndex = 0})
|
||||
> else do
|
||||
> forM_ (reverse [capPtr cap, capPtr cap + (1 `shiftL` resetChunkBits) ..
|
||||
> getFreeRef (capPtr cap) (capFreeIndex cap) - 1])
|
||||
> $ \addr -> do
|
||||
> withoutPreemption $ doMachineOp $ clearMemory
|
||||
> (PPtr (fromPPtr addr)) (1 `shiftL` resetChunkBits)
|
||||
> withoutPreemption $ updateCap slot (cap {capFreeIndex
|
||||
> = getFreeIndex (capPtr cap) addr})
|
||||
> preemptionPoint
|
||||
|
||||
> invokeUntyped :: UntypedInvocation -> KernelP ()
|
||||
> invokeUntyped (Retype srcSlot reset base retypeBase newType userSize destSlots isDev) = do
|
||||
|
||||
> when reset $ resetUntypedCap srcSlot
|
||||
> withoutPreemption $ do
|
||||
> cap <- getSlotCap srcSlot
|
||||
|
||||
For verification purposes a check is made that the region the objects are created in does not overlap with any existing CNodes.
|
||||
|
||||
> let totalObjectSize = (length destSlots) `shiftL` (getObjectSize newType userSize)
|
||||
> stateAssert (\x -> not (cNodeOverlap (gsCNodes x)
|
||||
> (\x -> fromPPtr freeRegionBase <= x
|
||||
> && x <= fromPPtr freeRegionBase + fromIntegral totalObjectSize - 1)))
|
||||
> "CNodes present in region to be retyped."
|
||||
> let freeRef = freeRegionBase + PPtr (fromIntegral totalObjectSize)
|
||||
> updateCap srcSlot (cap {capFreeIndex = getFreeIndex base freeRef})
|
||||
> let totalObjectSize = (length destSlots) `shiftL` (getObjectSize newType userSize)
|
||||
> stateAssert (\x -> not (cNodeOverlap (gsCNodes x)
|
||||
> (\x -> fromPPtr retypeBase <= x
|
||||
> && x <= fromPPtr retypeBase + fromIntegral totalObjectSize - 1)))
|
||||
> "CNodes present in region to be retyped."
|
||||
> let freeRef = retypeBase + PPtr (fromIntegral totalObjectSize)
|
||||
> updateCap srcSlot
|
||||
> (cap {capFreeIndex = getFreeIndex base freeRef})
|
||||
|
||||
Create the new objects and insert caps to these objects into the destination slots.
|
||||
|
||||
> createNewObjects newType srcSlot destSlots freeRegionBase userSize isDevice
|
||||
|
||||
|
||||
> createNewObjects newType srcSlot destSlots retypeBase userSize isDev
|
||||
|
||||
This function performs the check that CNodes do not overlap with the retyping region. Its actual definition is provided in the Isabelle translation.
|
||||
|
||||
> cNodeOverlap :: (Word -> Maybe Int) -> (Word -> Bool) -> Bool
|
||||
|
|
|
|||
Loading…
Reference in New Issue