adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

arm ainvs: update for invoke_irq_handler arch split 

Signed-off-by: Victor Phan <Victor.Phan@data61.csiro.au>
This commit is contained in:
Victor Phan 2020-04-29 13:54:21 +10:00 committed by Gerwin Klein
parent 9ddc7c93c2
commit c297e93154
6 changed files with 25 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
proof/invariant-abstract/ARM/ArchBCorres2_AI.thy
View File

@ -145,7 +145,9 @@ lemma handle_hypervisor_fault_bcorres[wp]: "bcorres (handle_hypervisor_fault a b
lemma handle_event_bcorres[wp]: "bcorres (handle_event e) (handle_event e)"
apply (cases e)
apply (simp add: handle_send_def handle_call_def handle_recv_def handle_reply_def handle_yield_def handle_interrupt_def Let_def | intro impI conjI allI | wp | wpc)+
apply (simp add: handle_send_def handle_call_def handle_recv_def handle_reply_def handle_yield_def
handle_interrupt_def Let_def arch_mask_irq_signal_def
| intro impI conjI allI | wp | wpc)+
done
crunch (bcorres)bcorres[wp]: guarded_switch_to,switch_to_idle_thread truncate_state (ignore: storeWord clearExMonitor)

10
proof/invariant-abstract/ARM/ArchDetSchedDomainTime_AI.thy
View File

@ -20,7 +20,7 @@ crunch domain_list_inv [wp, DetSchedDomainTime_AI_assms]:
handle_arch_fault_reply,
arch_invoke_irq_control, handle_vm_fault, arch_get_sanitise_register_info,
prepare_thread_delete, handle_hypervisor_fault, make_arch_fault_msg,
arch_post_modify_registers, arch_post_cap_deletion
arch_post_modify_registers, arch_post_cap_deletion, arch_invoke_irq_handler
"\<lambda>s. P (domain_list s)"
crunch domain_time_inv [wp, DetSchedDomainTime_AI_assms]: arch_finalise_cap "\<lambda>s. P (domain_time s)"
@ -31,7 +31,7 @@ crunch domain_time_inv [wp, DetSchedDomainTime_AI_assms]:
handle_arch_fault_reply, init_arch_objects,
arch_invoke_irq_control, handle_vm_fault, arch_get_sanitise_register_info,
prepare_thread_delete, handle_hypervisor_fault,
arch_post_modify_registers, arch_post_cap_deletion
arch_post_modify_registers, arch_post_cap_deletion, arch_invoke_irq_handler
"\<lambda>s. P (domain_time s)"
declare init_arch_objects_exst[DetSchedDomainTime_AI_assms]
make_arch_fault_msg_inv[DetSchedDomainTime_AI_assms]
@ -46,6 +46,10 @@ global_interpretation DetSchedDomainTime_AI?: DetSchedDomainTime_AI
context Arch begin global_naming ARM
crunch domain_time_inv [wp, DetSchedDomainTime_AI_assms]: arch_mask_irq_signal "\<lambda>s. P (domain_time s)"
crunch domain_list_inv [wp, DetSchedDomainTime_AI_assms]: arch_mask_irq_signal "\<lambda>s. P (domain_list s)"
crunch domain_time_inv [wp, DetSchedDomainTime_AI_assms]: arch_perform_invocation "\<lambda>s. P (domain_time s)"
(wp: crunch_wps check_cap_inv)
@ -59,7 +63,7 @@ lemma handle_interrupt_valid_domain_time [DetSchedDomainTime_AI_assms]:
apply (case_tac "maxIRQ < i"; simp)
subgoal by (wp hoare_false_imp, simp)
apply (rule hoare_pre)
apply (wp do_machine_op_exst | simp | wpc)+
apply (wp do_machine_op_exst | simp add: arch_mask_irq_signal_def | wpc)+
apply (rule_tac Q="\<lambda>_ s. 0 < domain_time s" in hoare_post_imp, fastforce)
apply wp
apply (rule_tac Q="\<lambda>_ s. 0 < domain_time s" in hoare_post_imp, fastforce)

6
proof/invariant-abstract/ARM/ArchDetSchedSchedule_AI.thy
View File

@ -12,6 +12,8 @@ context Arch begin global_naming ARM
named_theorems DetSchedSchedule_AI_assms
crunch valid_sched[wp, DetSchedSchedule_AI_assms]: arch_mask_irq_signal valid_sched
crunch prepare_thread_delete_idle_thread[wp, DetSchedSchedule_AI_assms]:
prepare_thread_delete "\<lambda>(s:: det_ext state). P (idle_thread s)"
@ -209,8 +211,8 @@ crunch simple_sched_action [wp, DetSchedSchedule_AI_assms]:
(wp: hoare_drop_imps mapM_x_wp mapM_wp select_wp subset_refl
simp: unless_def if_fun_split)
crunch valid_sched [wp, DetSchedSchedule_AI_assms]:
arch_finalise_cap, prepare_thread_delete valid_sched
crunches arch_finalise_cap, prepare_thread_delete, arch_invoke_irq_handler
for valid_sched [wp, DetSchedSchedule_AI_assms]: valid_sched
(ignore: set_object wp: crunch_wps subset_refl simp: if_fun_split)
lemma activate_thread_valid_sched [DetSchedSchedule_AI_assms]:

5
proof/invariant-abstract/ARM/ArchDeterministic_AI.thy
View File

@ -28,6 +28,8 @@ global_interpretation Deterministic_AI_1?: Deterministic_AI_1
context Arch begin global_naming ARM
crunch valid_list[wp, Deterministic_AI_assms]: arch_invoke_irq_handler valid_list
crunch valid_list[wp]: invalidate_tlb_by_asid valid_list
(wp: crunch_wps preemption_point_inv' simp: crunch_simps filterM_mapM)
@ -72,7 +74,7 @@ lemma handle_interrupt_valid_list[wp, Deterministic_AI_assms]:
unfolding handle_interrupt_def ackInterrupt_def
apply (rule hoare_pre)
by (wp get_cap_wp do_machine_op_valid_list
| wpc | simp add: get_irq_slot_def handle_reserved_irq_def
| wpc | simp add: get_irq_slot_def handle_reserved_irq_def arch_mask_irq_signal_def
| wp (once) hoare_drop_imps)+
crunch valid_list[wp, Deterministic_AI_assms]: handle_send,handle_reply valid_list
@ -80,7 +82,6 @@ crunch valid_list[wp, Deterministic_AI_assms]: handle_send,handle_reply valid_li
crunch valid_list[wp, Deterministic_AI_assms]: handle_hypervisor_fault valid_list
end
global_interpretation Deterministic_AI_2?: Deterministic_AI_2
proof goal_cases
interpret Arch .

3
proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy
View File

@ -153,7 +153,8 @@ global_interpretation EmptyFail_AI_schedule?: EmptyFail_AI_schedule
context Arch begin global_naming ARM
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: possible_switch_to, handle_event, activate_thread
crunches possible_switch_to, handle_event, activate_thread
for (empty_fail) empty_fail[wp, EmptyFail_AI_assms]
(simp: cap.splits arch_cap.splits split_def invocation_label.splits Let_def
kernel_object.splits arch_kernel_obj.splits option.splits pde.splits pte.splits
bool.splits apiobject_type.splits aobject_type.splits notification.splits

9
proof/invariant-abstract/ARM/ArchInterrupt_AI.thy
View File

@ -96,6 +96,8 @@ lemma (* set_irq_state_valid_cap *)[Interrupt_AI_asms]:
crunch valid_global_refs[Interrupt_AI_asms]: set_irq_state "valid_global_refs"
crunch typ_at[wp]: arch_invoke_irq_handler "\<lambda>s. P (typ_at T p s)"
lemma invoke_irq_handler_invs'[Interrupt_AI_asms]:
assumes dmo_ex_inv[wp]: "\<And>f. \<lbrace>invs and ex_inv\<rbrace> do_machine_op f \<lbrace>\<lambda>rv::unit. ex_inv\<rbrace>"
assumes cap_insert_ex_inv[wp]: "\<And>cap src dest.
@ -198,11 +200,12 @@ lemma empty_fail_maskInterrupt_ARCH[Interrupt_AI_asms]:
lemma (* handle_interrupt_invs *) [Interrupt_AI_asms]:
"\<lbrace>invs\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: handle_interrupt_def )
apply (simp add: handle_interrupt_def)
apply (rule conjI; rule impI)
apply (simp add: do_machine_op_bind empty_fail_ackInterrupt_ARCH empty_fail_maskInterrupt_ARCH)
apply (wp dmo_maskInterrupt_invs maskInterrupt_invs_ARCH dmo_ackInterrupt send_signal_interrupt_states | wpc | simp)+
apply (wp get_cap_wp send_signal_interrupt_states )
apply (wp dmo_maskInterrupt_invs maskInterrupt_invs_ARCH dmo_ackInterrupt send_signal_interrupt_states
| wpc | simp add: arch_mask_irq_signal_def)+
apply (wp get_cap_wp send_signal_interrupt_states)
apply (rule_tac Q="\<lambda>rv. invs and (\<lambda>s. st = interrupt_states s irq)" in hoare_post_imp)
apply (clarsimp simp: ex_nonz_cap_to_def invs_valid_objs)
apply (intro allI exI, erule cte_wp_at_weakenE)