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

ainvs: adjust generic theories for ARM fix

This commit is contained in:
Miki Tanaka 2017-05-16 21:27:26 +10:00 committed by Alejandro Gomez-Londono
parent 35f714addf
commit 5e4df460e2
11 changed files with 112 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
proof/invariant-abstract/CNodeInv_AI.thy
View File

@ -1860,11 +1860,10 @@ lemma cap_swap_irq_handlers[wp]:
crunch vspace_objs [wp]: cap_swap "valid_vspace_objs"
crunch valid_global_objs [wp]: cap_swap "valid_global_objs"
crunch valid_global_vspace_mappings [wp]: cap_swap "valid_global_vspace_mappings"
(*
crunch arch_objs [wp]: cap_swap "valid_arch_objs"
crunch arch_objs [wp]: cap_move "valid_arch_objs"
crunch arch_objs [wp]: empty_slot "valid_arch_objs"
*)
@ -1983,7 +1982,7 @@ lemma cap_swap_invs[wp]:
cte_wp_at_caps_of_state
simp del: split_paired_Ex split_paired_All
| rule conjI
| fastforce dest!: valid_reply_caps_of_stateD)+
| clarsimp dest!: valid_reply_caps_of_stateD)+
done
lemma cap_swap_fd_invs[wp]:

10
proof/invariant-abstract/CSpace_AI.thy
View File

@ -3954,6 +3954,12 @@ crunch empty_table_at[wp]: cap_insert "obj_at (empty_table S) p"
simp: empty_table_caps_of)
crunch valid_global_objs[wp]: cap_insert "valid_global_objs"
(wp: crunch_wps)
crunch global_vspace_mappings[wp]: cap_insert "valid_global_vspace_mappings"
(wp: crunch_wps)
crunch v_ker_map[wp]: cap_insert "valid_kernel_mappings"
(wp: crunch_wps)
@ -4637,6 +4643,10 @@ lemmas setup_reply_master_valid_vso_at[wp]
= valid_vso_at_lift [OF setup_reply_master_typ_at setup_reply_master_arch_ko_at]
crunch valid_global_objs[wp]: setup_reply_master "valid_global_objs"
crunch global_vspace_mappings[wp]: setup_reply_master "valid_global_vspace_mappings"
crunch v_ker_map[wp]: setup_reply_master "valid_kernel_mappings"
crunch eq_ker_map[wp]: setup_reply_master "equal_kernel_mappings"

12
proof/invariant-abstract/Detype_AI.thy
View File

@ -416,11 +416,13 @@ lemma unique_table_refs:
split: if_split)
apply blast
done
lemma valid_pspace: "valid_pspace s" using invs
by (simp add: invs_def valid_state_def)
lemma valid_global_objs: "valid_global_objs s"
using invs by (clarsimp simp: invs_def valid_state_def)
lemma cap_is_valid: "valid_cap cap s"
by (rule cte_wp_valid_cap[OF cap invs_valid_objs[OF invs]])
@ -465,8 +467,10 @@ locale detype_locale_gen_2 = detype_locale_gen_1 cap ptr s
"valid_vspace_objs (detype (untyped_range cap) s)"
"valid_arch_caps (detype (untyped_range cap) s)"
"valid_kernel_mappings (detype (untyped_range cap) s)"
"valid_global_objs (detype (untyped_range cap) s)"
"valid_asid_map (detype (untyped_range cap) s)"
"equal_kernel_mappings (detype (untyped_range cap) s)"
"valid_global_vspace_mappings (detype (untyped_range cap) s)"
"equal_kernel_mappings (detype (untyped_range cap) s)"
"pspace_in_kernel_window (detype (untyped_range cap) s)"
"valid_machine_state (clear_um (untyped_range cap) (detype (untyped_range cap) s))"
"pspace_respects_device_region (clear_um (untyped_range cap) (detype (untyped_range cap) s))"

4
proof/invariant-abstract/Finalise_AI.thy
View File

@ -692,12 +692,12 @@ lemma tcb_cap_valid_imp_NullCap:
apply (clarsimp simp: ran_tcb_cap_cases valid_ipc_buffer_cap_def
split: Structures_A.thread_state.split_asm)
done
(* moved to Invariants_AI
lemma a_type_arch_live:
"a_type ko = AArch tp \<Longrightarrow> \<not> live0 ko"
by (simp add: a_type_def
split: Structures_A.kernel_object.split_asm)
*)
lemma pred_tcb_at_def2:
"pred_tcb_at proj P t \<equiv> \<lambda>s. \<exists>tcb. ko_at (TCB tcb) t s \<and> P (proj (tcb_to_itcb tcb))"
by (rule eq_reflection, rule ext) (fastforce simp: pred_tcb_at_def obj_at_def)

2
proof/invariant-abstract/InterruptAcc_AI.thy
View File

@ -53,6 +53,8 @@ definition all_invs_but_valid_irq_states_for where
valid_kernel_mappings and
equal_kernel_mappings and
valid_asid_map and
valid_global_objs and
valid_global_vspace_mappings and
pspace_in_kernel_window and
cap_refs_in_kernel_window and
pspace_respects_device_region and

26
proof/invariant-abstract/Invariants_AI.thy
View File

@ -26,7 +26,6 @@ requalify_consts
is_nondevice_page_cap
state_hyp_refs_of
hyp_refs_of
arch_live
hyp_live
wellformed_acap
@ -45,8 +44,10 @@ requalify_consts
valid_arch_objs
valid_vspace_objs
valid_arch_caps
valid_global_objs
valid_kernel_mappings
equal_kernel_mappings
valid_global_vspace_mappings
pspace_in_kernel_window
ASIDPoolObj
@ -84,6 +85,7 @@ requalify_facts
physical_arch_cap_has_ref
wellformed_arch_default
valid_arch_obj_default'
valid_vspace_obj_default'
vs_lookup1_stateI2
vs_lookup_pages1_stateI2
typ_at_pg
@ -624,6 +626,11 @@ where
| Notification ntfn => live0 ko
| ArchObj ao => hyp_live ko"
lemma a_type_arch_live:
"a_type ko = AArch tp \<Longrightarrow> \<not> live0 ko"
by (simp add: a_type_def
split: Structures_A.kernel_object.split_asm)
fun
zobj_refs :: "cap \<Rightarrow> obj_ref set"
where
@ -895,9 +902,11 @@ where
(* and valid_arch_objs *)
and valid_vspace_objs
and valid_arch_caps
and valid_global_objs
and valid_kernel_mappings
and equal_kernel_mappings
and valid_asid_map
and valid_global_vspace_mappings
and pspace_in_kernel_window
and cap_refs_in_kernel_window
and pspace_respects_device_region
@ -975,8 +984,9 @@ abbreviation(input)
and valid_reply_caps and valid_reply_masters and valid_global_refs
and valid_arch_state and valid_machine_state and valid_irq_states
and valid_irq_node and valid_irq_handlers and valid_vspace_objs (* and valid_arch_objs *)
and valid_arch_caps and valid_kernel_mappings
and valid_arch_caps and valid_global_objs and valid_kernel_mappings
and equal_kernel_mappings and valid_asid_map
and valid_global_vspace_mappings
and pspace_in_kernel_window and cap_refs_in_kernel_window
and pspace_respects_device_region and cap_refs_respects_device_region
and cur_tcb"
@ -2539,6 +2549,14 @@ lemma valid_arch_cap_update [iff]:
"valid_arch_caps (f s) = valid_arch_caps s"
by (simp add: valid_arch_caps_def)
lemma valid_global_objs_update [iff]:
"valid_global_objs (f s) = valid_global_objs s"
by (simp add: valid_global_objs_def arch)
lemma valid_global_vspace_mappings_update [iff]:
"valid_global_vspace_mappings (f s) = valid_global_vspace_mappings s"
by (simp add: valid_global_vspace_mappings_def arch)
lemma pspace_in_kernel_window_update [iff]:
"pspace_in_kernel_window (f s) = pspace_in_kernel_window s"
by (simp add: pspace_in_kernel_window_def arch pspace)
@ -3183,6 +3201,10 @@ lemma cur_tcb_arch [iff]:
"cur_tcb (arch_state_update f s) = cur_tcb s"
by (simp add: cur_tcb_def)
lemma invs_valid_global_objs[elim!]:
"invs s \<Longrightarrow> valid_global_objs s"
by (clarsimp simp: invs_def valid_state_def)
lemma get_irq_slot_real_cte:
"\<lbrace>invs\<rbrace> get_irq_slot irq \<lbrace>real_cte_at\<rbrace>"
apply (simp add: get_irq_slot_def)

43
proof/invariant-abstract/Ipc_AI.thy
View File

@ -235,6 +235,10 @@ locale Ipc_AI =
"\<And> ft t. make_arch_fault_msg ft t \<lbrace>cap_refs_in_kernel_window :: 'state_ext state \<Rightarrow> bool\<rbrace>"
assumes make_arch_fault_msg_valid_objs[wp]:
"\<And> ft t. make_arch_fault_msg ft t \<lbrace>valid_objs :: 'state_ext state \<Rightarrow> bool\<rbrace>"
assumes make_arch_fault_msg_valid_global_objs[wp]:
"\<And> ft t. make_arch_fault_msg ft t \<lbrace>valid_global_objs :: 'state_ext state \<Rightarrow> bool\<rbrace>"
assumes make_arch_fault_msg_valid_global_vspace_mappings[wp]:
"\<And> ft t. make_arch_fault_msg ft t \<lbrace>valid_global_vspace_mappings :: 'state_ext state \<Rightarrow> bool\<rbrace>"
assumes make_arch_fault_msg_valid_ioc[wp]:
"\<And> ft t. make_arch_fault_msg ft t \<lbrace>valid_ioc :: 'state_ext state \<Rightarrow> bool\<rbrace>"
assumes make_arch_fault_msg_vms[wp]:
@ -273,6 +277,11 @@ locale Ipc_AI =
\<lbrace>valid_objs and cte_wp_at P (t, ref) and tcb_at t :: 'state_ext state \<Rightarrow> bool\<rbrace>
do_ipc_transfer st ep b gr rt
\<lbrace>\<lambda>rv. cte_wp_at P (t, ref)\<rbrace>"
assumes setup_caller_cap_valid_global_objs[wp]:
"\<And>send recv.
\<lbrace>valid_global_objs :: 'state_ext state \<Rightarrow> bool\<rbrace>
setup_caller_cap send recv
\<lbrace>\<lambda>rv. valid_global_objs\<rbrace>"
assumes handle_arch_fault_reply_typ_at[wp]:
"\<And> P T p x4 t label msg.
\<lbrace>\<lambda>s::'state_ext state. P (typ_at T p s)\<rbrace>
@ -970,8 +979,16 @@ lemma transfer_caps_loop_valid_arch_caps[wp]:
apply clarsimp
done
crunch valid_global_objs [wp]: set_extra_badge valid_global_objs
lemma transfer_caps_loop_valid_global_objs[wp]:
"\<And>ep buffer n caps slots mi.
\<lbrace>valid_global_objs :: 'state_ext state \<Rightarrow> bool\<rbrace>
transfer_caps_loop ep buffer n caps slots mi
\<lbrace>\<lambda>rv. valid_global_objs\<rbrace>"
by (wp transfer_caps_loop_pres cap_insert_valid_global_objs)
crunch valid_kernel_mappings [wp]: set_extra_badge valid_kernel_mappings
@ -1015,6 +1032,16 @@ lemma transfer_caps_loop_only_idle[wp]:
\<lbrace>\<lambda>rv. only_idle\<rbrace>"
by (wp transfer_caps_loop_pres | simp)+
crunch valid_global_vspace_mappings [wp]: set_extra_badge valid_global_vspace_mappings
lemma transfer_caps_loop_valid_global_pd_mappings[wp]:
"\<And>ep buffer n caps slots mi.
\<lbrace>valid_global_vspace_mappings :: 'state_ext state \<Rightarrow> bool\<rbrace>
transfer_caps_loop ep buffer n caps slots mi
\<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>"
by (wp transfer_caps_loop_pres)
crunch pspace_in_kernel_window [wp]: set_extra_badge pspace_in_kernel_window
@ -1121,7 +1148,8 @@ lemma transfer_caps_loop_invs[wp]:
\<and> transfer_caps_srcs caps s\<rbrace>
transfer_caps_loop ep buffer n caps slots mi
\<lbrace>\<lambda>rv. invs\<rbrace>"
unfolding invs_def valid_state_def valid_pspace_def by (wpsimp wp: valid_irq_node_typ transfer_caps_loop_valid_vspace_objs)
unfolding invs_def valid_state_def valid_pspace_def
by (wpsimp wp: valid_irq_node_typ transfer_caps_loop_valid_vspace_objs)
end
@ -1672,14 +1700,17 @@ lemma copy_mrs_irq_handlers[wp]:
context Ipc_AI begin
crunch irq_handlers[wp]: do_ipc_transfer "valid_irq_handlers :: 'state_ext state \<Rightarrow> bool"
(wp: crunch_wps hoare_vcg_const_Ball_lift simp: zipWithM_x_mapM crunch_simps ball_conj_distrib )
(wp: crunch_wps hoare_vcg_const_Ball_lift simp: zipWithM_x_mapM crunch_simps ball_conj_distrib)
crunch vspace_objs[wp]: transfer_caps_loop "valid_vspace_objs :: 'state_ext state \<Rightarrow> bool"
(wp: crunch_wps transfer_caps_loop_valid_vspace_objs simp: zipWithM_x_mapM crunch_simps)
crunch valid_global_objs[wp]: do_ipc_transfer "valid_global_objs :: 'state_ext state \<Rightarrow> bool"
(wp: crunch_wps simp: zipWithM_x_mapM ignore: make_arch_fault_msg)
crunch vspace_objs[wp]: do_ipc_transfer "valid_vspace_objs :: 'state_ext state \<Rightarrow> bool"
(wp: crunch_wps transfer_caps_loop_valid_vspace_objs simp: zipWithM_x_mapM crunch_simps)
crunch valid_global_vspace_mappings[wp]: do_ipc_transfer "valid_global_vspace_mappings :: 'state_ext state \<Rightarrow> bool"
(wp: crunch_wps transfer_caps_loop_valid_vspace_objs simp: zipWithM_x_mapM crunch_simps)
crunch arch_caps[wp]: do_ipc_transfer "valid_arch_caps :: 'state_ext state \<Rightarrow> bool"
(wp: crunch_wps hoare_vcg_const_Ball_lift transfer_caps_loop_valid_arch_caps
simp: zipWithM_x_mapM crunch_simps ball_conj_distrib )
@ -1718,6 +1749,8 @@ context Ipc_AI begin
crunch only_idle [wp]: do_ipc_transfer "only_idle :: 'state_ext state \<Rightarrow> bool"
(wp: crunch_wps simp: crunch_simps)
crunch valid_global_vspace_mappings [wp]: set_extra_badge valid_global_vspace_mappings
crunch pspace_in_kernel_window[wp]: do_ipc_transfer "pspace_in_kernel_window :: 'state_ext state \<Rightarrow> bool"
(wp: crunch_wps simp: crunch_simps)
@ -2448,6 +2481,8 @@ crunch eq_ker_map[wp]: setup_caller_cap "equal_kernel_mappings"
crunch asid_map [wp]: setup_caller_cap "valid_asid_map"
crunch global_pd_mappings[wp]: setup_caller_cap "valid_global_vspace_mappings"
crunch pspace_in_kernel_window[wp]: setup_caller_cap "pspace_in_kernel_window"
lemma setup_caller_cap_cap_refs_in_window[wp]:

18
proof/invariant-abstract/KHeapPre_AI.thy
View File

@ -73,7 +73,7 @@ lemma arch_obj_pred_a_type[intro, simp]: "arch_obj_pred (\<lambda>ko. a_type ko
lemma
arch_obj_pred_arch_obj_l[intro, simp]: "arch_obj_pred (\<lambda>ko. ArchObj ako = ko)" and
arch_obj_pred_arch_obj_r[intro, simp]: "arch_obj_pred (\<lambda>ko. ko = ArchObj ako)"
arch_obj_pred_arch_obj_r[intro, simp]: "arch_obj_pred (\<lambda>ko. ko = ArchObj ako)"
by (auto simp add: arch_obj_pred_defs)
lemma arch_obj_pred_fun_lift: "arch_obj_pred (\<lambda>ko. F (arch_obj_fun_lift P N ko))"
@ -109,27 +109,15 @@ declare
locale arch_only_obj_pred =
fixes P :: "kernel_object \<Rightarrow> bool"
assumes arch_only: "arch_obj_pred P"
(**)
(*
lemma "arch_obj_pred P \<Longrightarrow> vspace_obj_pred P"
apply (clarsimp simp add: arch_obj_pred_def vspace_obj_pred_def)
apply (erule_tac x=ko in allE)
apply (simp add: non_vspace_obj_def)
apply
*)
assumes arch_only: "arch_obj_pred P"
locale vspace_only_obj_pred =
fixes P :: "kernel_object \<Rightarrow> bool"
fixes vspace_obj_pred :: "(kernel_object \<Rightarrow> bool) \<Rightarrow> bool"
assumes vspace_only: "vspace_obj_pred P"
(**)
lemma set_object_typ_at:
"\<lbrace>\<lambda>s. typ_at (a_type ko) p s \<and> P (typ_at T p' s)\<rbrace>
"\<lbrace>\<lambda>s. typ_at (a_type ko) p s \<and> P (typ_at T p' s)\<rbrace>
set_object p ko \<lbrace>\<lambda>rv s. P (typ_at T p' s)\<rbrace>"
apply (simp add: set_object_def)
apply wp

17
proof/invariant-abstract/KHeap_AI.thy
View File

@ -27,9 +27,11 @@ requalify_facts
vs_lookup_vspace_obj_at_lift
vs_lookup_pages_vspace_obj_at_lift
valid_arch_caps_lift_weak
valid_global_objs_lift_weak
valid_asid_map_lift
valid_kernel_mappings_lift
equal_kernel_mappings_lift
valid_global_vspace_mappings_lift
valid_machine_state_lift
valid_vso_at_lift
valid_vso_at_lift_aobj_at
@ -1253,7 +1255,7 @@ lemma set_object_non_pagetable:
apply (clarsimp simp: obj_at_def)
by (rule vspace_obj_predE)
(*
lemma set_object_vspace_objs_non_pagetable:
"\<lbrace>valid_vspace_objs and K (non_vspace_obj ko) and obj_at non_vspace_obj p\<rbrace>
set_object p ko
@ -1262,7 +1264,7 @@ lemma set_object_vspace_objs_non_pagetable:
apply (rule hoare_pre)
apply (rule valid_vspace_objs_lift_weak)
apply (wpsimp wp: set_object_non_pagetable)+
done
done*)
lemma set_object_memory[wp]:
"\<lbrace>\<lambda>s. P (underlying_memory (machine_state s))\<rbrace>
@ -1311,6 +1313,13 @@ by (rule vs_lookup_vspace_obj_at_lift; wp vsobj_at; simp)
lemma vs_lookup_pages[wp]: "\<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace> f \<lbrace>\<lambda>_ s. P (vs_lookup_pages s)\<rbrace>"
by (rule vs_lookup_pages_vspace_obj_at_lift; wp vsobj_at; simp)
lemma valid_global_objs[wp]: "\<lbrace>valid_global_objs\<rbrace> f \<lbrace>\<lambda>_. valid_global_objs\<rbrace>"
by (rule valid_global_objs_lift_weak, (wp vsobj_at)+)
lemma valid_global_vspace_mappings[wp]:
"\<lbrace>valid_global_vspace_mappings\<rbrace> f \<lbrace>\<lambda>_. valid_global_vspace_mappings\<rbrace>"
by (rule valid_global_vspace_mappings_lift, (wp vsobj_at)+)
lemma valid_asid_map[wp]: "\<lbrace>valid_asid_map\<rbrace> f \<lbrace>\<lambda>_. valid_asid_map\<rbrace>"
by (rule valid_asid_map_lift, (wp vsobj_at)+)
@ -1692,6 +1701,10 @@ crunch reply_masters[wp]: do_machine_op "valid_reply_masters"
crunch valid_irq_handlers[wp]: do_machine_op "valid_irq_handlers"
crunch valid_global_objs[wp]: do_machine_op "valid_global_objs"
crunch valid_global_vspace_mappings[wp]: do_machine_op "valid_global_vspace_mappings"
crunch valid_arch_caps[wp]: do_machine_op "valid_arch_caps"

7
proof/invariant-abstract/Retype_AI.thy
View File

@ -22,7 +22,6 @@ abbreviation "down_aligned_area ptr sz \<equiv> {(ptr && ~~ mask sz) + (2 ^ sz -
context begin interpretation Arch .
requalify_facts
global_refs_kheap
valid_vspace_obj_default' (* move to invariants_AI? *)
requalify_consts
clearMemory
clearMemoryVM
@ -1123,9 +1122,9 @@ abbreviation(input)
and if_unsafe_then_cap and valid_reply_caps
and valid_reply_masters and valid_global_refs and valid_arch_state
and valid_irq_node and valid_irq_handlers and valid_vspace_objs
and valid_irq_states
and valid_irq_states and valid_global_objs
and valid_arch_caps and valid_kernel_mappings
and valid_asid_map
and valid_asid_map and valid_global_vspace_mappings
and pspace_in_kernel_window and cap_refs_in_kernel_window
and pspace_respects_device_region and cap_refs_respects_device_region
and cur_tcb and valid_ioc and valid_machine_state"
@ -1150,6 +1149,7 @@ locale Retype_AI_dmo_eq_kernel_restricted =
crunch only_idle[wp]: do_machine_op "only_idle"
crunch valid_global_refs[wp]: do_machine_op "valid_global_refs"
crunch global_mappings[wp]: do_machine_op "valid_global_vspace_mappings"
crunch valid_kernel_mappings[wp]: do_machine_op "valid_kernel_mappings"
crunch cap_refs_in_kernel_window[wp]: do_machine_op "cap_refs_in_kernel_window"
@ -1627,7 +1627,6 @@ lemma valid_obj_default_object:
apply (clarsimp simp add: wellformed_arch_default)
done
lemma valid_vspace_obj_default:
assumes tyunt: "ty \<noteq> Structures_A.apiobject_type.Untyped"
shows "ArchObj ao = default_object ty dev us \<Longrightarrow> valid_vspace_obj ao s'"

4
proof/invariant-abstract/VSpacePre_AI.thy
View File

@ -103,8 +103,8 @@ lemma hoare_name_pre_state2:
by (auto simp: valid_def intro: hoare_name_pre_state)
lemma pd_casting_shifting:
"size x + 3 < len_of TYPE('a) \<Longrightarrow>
ucast (ucast x << 3 >> 3 :: ('a :: len) word) = x"
"size x + n < len_of TYPE('a) \<Longrightarrow>
ucast (ucast x << n >> n :: ('a :: len) word) = x"
apply (rule word_eqI)
apply (simp add: nth_ucast nth_shiftr nth_shiftl word_size)
done