arm-hyp haskell: changes from meeting
This commit is contained in:
Rafal Kolanski
Alejandro Gomez-Londono
parent
a35ec59857
commit
298d4ea6fe
|
|
@ -0,0 +1,136 @@
|
|||
(*
|
||||
* Copyright 2014, General Dynamics C4 Systems
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_GPLv2.txt" for details.
|
||||
*
|
||||
* @TAG(GD_GPL)
|
||||
*)
|
||||
|
||||
theory ArchBCorres2_AI
|
||||
imports
|
||||
"../BCorres2_AI"
|
||||
begin
|
||||
|
||||
context Arch begin global_naming ARM
|
||||
|
||||
named_theorems BCorres2_AI_assms
|
||||
|
||||
crunch (bcorres)bcorres[wp, BCorres2_AI_assms]: invoke_cnode truncate_state
|
||||
(simp: swp_def ignore: clearMemory without_preemption filterM ethread_set recycle_cap_ext)
|
||||
|
||||
crunch (bcorres)bcorres[wp]: create_cap,init_arch_objects,retype_region,delete_objects truncate_state
|
||||
(ignore: freeMemory clearMemory retype_region_ext)
|
||||
|
||||
crunch (bcorres)bcorres[wp]: set_extra_badge,derive_cap truncate_state (ignore: storeWord)
|
||||
|
||||
crunch (bcorres)bcorres[wp]: invoke_untyped truncate_state
|
||||
(ignore: sequence_x)
|
||||
|
||||
crunch (bcorres)bcorres[wp]: set_mcpriority truncate_state
|
||||
|
||||
lemma invoke_tcb_bcorres[wp]:
|
||||
fixes a
|
||||
shows "bcorres (invoke_tcb a) (invoke_tcb a)"
|
||||
apply (cases a)
|
||||
apply (wp | wpc | simp)+
|
||||
apply (rename_tac option)
|
||||
apply (case_tac option)
|
||||
apply (wp | wpc | simp)+
|
||||
done
|
||||
|
||||
lemma transfer_caps_loop_bcorres[wp]:
|
||||
"bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi)"
|
||||
apply (induct caps arbitrary: slots n mi ep)
|
||||
apply simp
|
||||
apply wp
|
||||
apply (case_tac a)
|
||||
apply simp
|
||||
apply (intro impI conjI)
|
||||
apply (wp | simp)+
|
||||
done
|
||||
|
||||
lemma invoke_irq_control_bcorres[wp]: "bcorres (invoke_irq_control a) (invoke_irq_control a)"
|
||||
apply (cases a)
|
||||
apply (wp | simp add: arch_invoke_irq_control_def)+
|
||||
done
|
||||
|
||||
lemma invoke_irq_handler_bcorres[wp]: "bcorres (invoke_irq_handler a) (invoke_irq_handler a)"
|
||||
apply (cases a)
|
||||
apply (wp | simp)+
|
||||
done
|
||||
|
||||
crunch (bcorres)bcorres[wp]: send_ipc,send_signal,do_reply_transfer,arch_perform_invocation truncate_state
|
||||
(simp: gets_the_def swp_def ignore: freeMemory clearMemory get_register loadWord cap_fault_on_failure
|
||||
set_register storeWord lookup_error_on_failure getRestartPC getRegister mapME)
|
||||
|
||||
lemma perform_invocation_bcorres[wp]: "bcorres (perform_invocation a b c) (perform_invocation a b c)"
|
||||
apply (cases c)
|
||||
apply (wp | wpc | simp)+
|
||||
done
|
||||
|
||||
lemma decode_cnode_invocation[wp]: "bcorres (decode_cnode_invocation a b c d) (decode_cnode_invocation a b c d)"
|
||||
apply (simp add: decode_cnode_invocation_def)
|
||||
apply (wp | wpc | simp add: split_def | intro impI conjI)+
|
||||
done
|
||||
|
||||
crunch (bcorres)bcorres[wp]:
|
||||
decode_set_ipc_buffer,decode_set_space,decode_set_priority,decode_set_mcpriority,
|
||||
decode_bind_notification,decode_unbind_notification truncate_state
|
||||
|
||||
lemma decode_tcb_configure_bcorres[wp]: "bcorres (decode_tcb_configure b (cap.ThreadCap c) d e)
|
||||
(decode_tcb_configure b (cap.ThreadCap c) d e)"
|
||||
apply (simp add: decode_tcb_configure_def | wp)+
|
||||
done
|
||||
|
||||
lemma decode_tcb_invocation_bcorres[wp]:"bcorres (decode_tcb_invocation a b (cap.ThreadCap c) d e) (decode_tcb_invocation a b (cap.ThreadCap c) d e)"
|
||||
apply (simp add: decode_tcb_invocation_def)
|
||||
apply (wp | wpc | simp)+
|
||||
done
|
||||
|
||||
lemma create_mapping_entries_bcorres[wp]: "bcorres (create_mapping_entries a b c d e f) (create_mapping_entries a b c d e f)"
|
||||
apply (cases c)
|
||||
apply (wp | simp)+
|
||||
done
|
||||
|
||||
lemma ensure_safe_mapping_bcorres[wp]: "bcorres (ensure_safe_mapping a) (ensure_safe_mapping a)"
|
||||
apply (induct rule: ensure_safe_mapping.induct)
|
||||
apply (wp | wpc | simp)+
|
||||
done
|
||||
|
||||
crunch (bcorres)bcorres[wp]: handle_invocation truncate_state
|
||||
(simp: syscall_def Let_def gets_the_def ignore: get_register syscall cap_fault_on_failure
|
||||
set_register without_preemption const_on_failure)
|
||||
|
||||
crunch (bcorres)bcorres[wp]: receive_ipc,receive_signal,delete_caller_cap truncate_state
|
||||
|
||||
lemma handle_vm_fault_bcorres[wp]: "bcorres (handle_vm_fault a b) (handle_vm_fault a b)"
|
||||
apply (cases b)
|
||||
apply (simp | wp)+
|
||||
done
|
||||
|
||||
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)+
|
||||
done
|
||||
|
||||
crunch (bcorres)bcorres[wp]: guarded_switch_to,switch_to_idle_thread truncate_state (ignore: storeWord clearExMonitor)
|
||||
|
||||
lemma choose_switch_or_idle:
|
||||
"((), s') \<in> fst (choose_thread s) \<Longrightarrow>
|
||||
(\<exists>word. ((),s') \<in> fst (guarded_switch_to word s)) \<or>
|
||||
((),s') \<in> fst (switch_to_idle_thread s)"
|
||||
apply (simp add: choose_thread_def)
|
||||
apply (clarsimp simp add: switch_to_idle_thread_def bind_def gets_def
|
||||
arch_switch_to_idle_thread_def in_monad
|
||||
return_def get_def modify_def put_def
|
||||
get_thread_state_def
|
||||
thread_get_def
|
||||
split: split_if_asm)
|
||||
apply force
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
end
|
||||
|
|
@ -0,0 +1,277 @@
|
|||
(*
|
||||
* Copyright 2014, General Dynamics C4 Systems
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_GPLv2.txt" for details.
|
||||
*
|
||||
* @TAG(GD_GPL)
|
||||
*)
|
||||
|
||||
(*
|
||||
ARM-specific CSpace invariants
|
||||
*)
|
||||
|
||||
theory ArchCSpacePre_AI
|
||||
imports "../CSpacePre_AI"
|
||||
begin
|
||||
|
||||
context Arch begin global_naming ARM
|
||||
|
||||
lemmas typ_at_eq_kheap_obj = typ_at_eq_kheap_obj atyp_at_eq_kheap_obj
|
||||
|
||||
lemmas set_cap_atyp_ats[wp] = abs_atyp_at_lifts[OF set_cap_typ_at]
|
||||
|
||||
lemmas cap_master_cap_def = cap_master_cap_def[simplified cap_master_arch_cap_def]
|
||||
|
||||
definition
|
||||
"final_matters_arch ac \<equiv>
|
||||
(case ac of
|
||||
ASIDPoolCap r as \<Rightarrow> True
|
||||
| ASIDControlCap \<Rightarrow> False
|
||||
| PageCap dev r rghts sz mapdata \<Rightarrow> False
|
||||
| PageTableCap r mapdata \<Rightarrow> True
|
||||
| PageDirectoryCap r mapdata \<Rightarrow> True)"
|
||||
|
||||
definition
|
||||
"cap_vptr_arch acap \<equiv> case acap of
|
||||
(PageCap _ _ _ _ (Some (_, vptr))) \<Rightarrow> Some vptr
|
||||
| (PageTableCap _ (Some (_, vptr))) \<Rightarrow> Some vptr
|
||||
| _ \<Rightarrow> None"
|
||||
|
||||
definition
|
||||
"cap_vptr cap \<equiv> arch_cap_fun_lift cap_vptr_arch None cap"
|
||||
|
||||
declare cap_vptr_arch_def[abs_def, simp]
|
||||
|
||||
lemmas cap_vptr_simps [simp] =
|
||||
cap_vptr_def [simplified, split_simps cap.split arch_cap.split option.split prod.split]
|
||||
|
||||
definition
|
||||
"is_derived_arch cap cap' \<equiv>
|
||||
((is_pt_cap cap \<or> is_pd_cap cap) \<longrightarrow>
|
||||
cap_asid cap = cap_asid cap' \<and> cap_asid cap \<noteq> None) \<and>
|
||||
(vs_cap_ref cap = vs_cap_ref cap' \<or> is_pg_cap cap')"
|
||||
|
||||
lemma is_derived_arch_non_arch:
|
||||
"\<not>is_arch_cap cap \<Longrightarrow> \<not> is_arch_cap cap' \<Longrightarrow>
|
||||
is_derived_arch cap cap'"
|
||||
unfolding is_derived_arch_def is_pg_cap_def is_pt_cap_def is_pd_cap_def
|
||||
vs_cap_ref_def is_arch_cap_def
|
||||
by (auto split: cap.splits)
|
||||
|
||||
lemma is_derived_cap_arch_asid:
|
||||
"is_derived_arch cap cap' \<Longrightarrow> cap_master_cap cap = cap_master_cap cap' \<Longrightarrow>
|
||||
is_pt_cap cap' \<or> is_pd_cap cap' \<Longrightarrow> cap_asid cap = cap_asid cap'"
|
||||
unfolding is_derived_arch_def
|
||||
apply (cases cap; cases cap'; simp)
|
||||
by (auto simp: is_cap_simps cap_master_cap_def split: arch_cap.splits)
|
||||
|
||||
|
||||
|
||||
lemma is_page_cap_PageCap[simp]:
|
||||
"is_page_cap (PageCap dev ref rghts pgsiz mapdata)"
|
||||
by (simp add: is_page_cap_def)
|
||||
|
||||
lemma pageBitsForSize_eq[simp]:
|
||||
"(pageBitsForSize sz = pageBitsForSize sz') = (sz = sz')"
|
||||
by (case_tac sz) (case_tac sz', simp+)+
|
||||
|
||||
|
||||
lemma
|
||||
cap_master_cap_arch_simps:
|
||||
"cap_master_arch_cap ((arch_cap.PageCap dev ref rghts sz mapdata)) =
|
||||
(arch_cap.PageCap dev ref UNIV sz None)"
|
||||
"cap_master_arch_cap ( (arch_cap.ASIDPoolCap pool asid)) =
|
||||
(arch_cap.ASIDPoolCap pool 0)"
|
||||
"cap_master_arch_cap ( (arch_cap.PageTableCap ptr x)) =
|
||||
(arch_cap.PageTableCap ptr None)"
|
||||
"cap_master_arch_cap ( (arch_cap.PageDirectoryCap ptr y)) =
|
||||
(arch_cap.PageDirectoryCap ptr None)"
|
||||
"cap_master_arch_cap ( arch_cap.ASIDControlCap) =
|
||||
arch_cap.ASIDControlCap"
|
||||
by (simp add: cap_master_arch_cap_def)+
|
||||
|
||||
lemma aobj_ref_cases':
|
||||
"aobj_ref acap = (case acap of arch_cap.ASIDControlCap \<Rightarrow> aobj_ref acap
|
||||
| _ \<Rightarrow> aobj_ref acap)"
|
||||
by (simp split: arch_cap.split)
|
||||
|
||||
|
||||
lemma aobj_ref_cases:
|
||||
"aobj_ref acap =
|
||||
(case acap of
|
||||
arch_cap.ASIDPoolCap w1 w2 \<Rightarrow> Some w1
|
||||
| arch_cap.ASIDControlCap \<Rightarrow> None
|
||||
| arch_cap.PageCap _ w s sz opt \<Rightarrow> Some w
|
||||
| arch_cap.PageTableCap w opt \<Rightarrow> Some w
|
||||
| arch_cap.PageDirectoryCap w opt \<Rightarrow> Some w)"
|
||||
apply (subst aobj_ref_cases')
|
||||
apply (clarsimp cong: arch_cap.case_cong)
|
||||
done
|
||||
|
||||
definition
|
||||
"cap_asid_base_arch cap \<equiv> case cap of
|
||||
(arch_cap.ASIDPoolCap _ asid) \<Rightarrow> Some asid
|
||||
| _ \<Rightarrow> None"
|
||||
|
||||
declare cap_asid_base_arch_def[abs_def, simp]
|
||||
|
||||
definition
|
||||
"cap_asid_base cap \<equiv> arch_cap_fun_lift cap_asid_base_arch None cap"
|
||||
|
||||
lemmas cap_asid_base_simps [simp] =
|
||||
cap_asid_base_def [simplified, split_simps cap.split arch_cap.split]
|
||||
|
||||
definition
|
||||
"ups_of_heap h \<equiv> \<lambda>p.
|
||||
case h p of Some (ArchObj (DataPage dev sz)) \<Rightarrow> Some sz | _ \<Rightarrow> None"
|
||||
|
||||
lemma ups_of_heap_typ_at:
|
||||
"ups_of_heap (kheap s) p = Some sz \<longleftrightarrow> data_at sz p s"
|
||||
apply (simp add: typ_at_eq_kheap_obj ups_of_heap_def data_at_def
|
||||
split: option.splits Structures_A.kernel_object.splits
|
||||
arch_kernel_obj.splits)
|
||||
by force
|
||||
|
||||
lemma ups_of_heap_typ_at_def:
|
||||
"ups_of_heap (kheap s) \<equiv> \<lambda>p.
|
||||
if \<exists>!sz. data_at sz p s
|
||||
then Some (THE sz. data_at sz p s)
|
||||
else None"
|
||||
apply (rule eq_reflection)
|
||||
apply (rule ext)
|
||||
apply (clarsimp simp: ups_of_heap_typ_at)
|
||||
apply (intro conjI impI)
|
||||
apply (frule (1) theI')
|
||||
apply safe
|
||||
apply (fastforce simp: ups_of_heap_typ_at)
|
||||
apply (clarsimp simp add: obj_at_def data_at_def)
|
||||
apply force
|
||||
done
|
||||
|
||||
lemma ups_of_heap_non_arch_upd:
|
||||
"h x = Some ko \<Longrightarrow> non_arch_obj ko \<Longrightarrow> non_arch_obj ko' \<Longrightarrow> ups_of_heap (h(x \<mapsto> ko')) = ups_of_heap h"
|
||||
by (rule ext) (auto simp add: ups_of_heap_def non_arch_obj_def split: kernel_object.splits)
|
||||
|
||||
definition
|
||||
"is_simple_cap_arch cap \<equiv> \<not>is_pt_cap cap \<and> \<not> is_pd_cap cap"
|
||||
|
||||
declare is_simple_cap_arch_def[simp]
|
||||
|
||||
lemma is_simple_cap_arch:
|
||||
"\<not>is_arch_cap cap \<Longrightarrow> is_simple_cap_arch cap"
|
||||
by (simp add: is_cap_simps)
|
||||
|
||||
crunch inv[wp]: lookup_ipc_buffer "I"
|
||||
|
||||
|
||||
lemma vs_cap_ref_to_table_cap_ref:
|
||||
"\<not> is_pg_cap cap \<Longrightarrow> vs_cap_ref cap = table_cap_ref cap"
|
||||
by (simp add: is_pg_cap_def table_cap_ref_def vs_cap_ref_simps
|
||||
split: cap.splits arch_cap.splits)
|
||||
|
||||
|
||||
lemma cap_master_cap_pg_cap:
|
||||
"\<lbrakk>cap_master_cap cap = cap_master_cap capa\<rbrakk>
|
||||
\<Longrightarrow> is_pg_cap cap = is_pg_cap capa"
|
||||
by (clarsimp simp:cap_master_cap_def is_cap_simps
|
||||
split:cap.splits arch_cap.splits dest!:cap_master_cap_eqDs)
|
||||
|
||||
lemma master_arch_cap_obj_refs:
|
||||
"cap_master_arch_cap c = cap_master_arch_cap c' \<Longrightarrow> aobj_ref c = aobj_ref c'"
|
||||
by (simp add: cap_master_arch_cap_def split: arch_cap.splits)
|
||||
|
||||
lemma master_arch_cap_cap_class:
|
||||
"cap_master_arch_cap c = cap_master_arch_cap c' \<Longrightarrow> acap_class c = acap_class c'"
|
||||
by (simp add: cap_master_arch_cap_def split: arch_cap.splits)
|
||||
|
||||
lemma is_cap_free_index_update[simp]:
|
||||
"is_pd_cap (src_cap\<lparr>free_index := a\<rparr>) = is_pd_cap src_cap"
|
||||
"is_pt_cap (src_cap\<lparr>free_index := a\<rparr>) = is_pt_cap src_cap"
|
||||
by (simp add:is_cap_simps free_index_update_def split:cap.splits)+
|
||||
|
||||
lemma masked_as_full_test_function_stuff[simp]:
|
||||
"is_pd_cap (masked_as_full a cap ) = is_pd_cap a"
|
||||
"is_pt_cap (masked_as_full a cap ) = is_pt_cap a"
|
||||
"vs_cap_ref (masked_as_full a cap ) = vs_cap_ref a"
|
||||
by (auto simp:masked_as_full_def)
|
||||
|
||||
lemma same_aobject_as_commute:
|
||||
"same_aobject_as x y \<Longrightarrow> same_aobject_as y x"
|
||||
by (cases x; cases y; clarsimp)
|
||||
|
||||
lemmas wellformed_cap_simps = wellformed_cap_simps[simplified wellformed_acap_def, split_simps arch_cap.split]
|
||||
|
||||
lemma same_master_cap_same_types:
|
||||
"cap_master_cap cap = cap_master_cap cap' \<Longrightarrow>
|
||||
(is_pt_cap cap = is_pt_cap cap') \<and> (is_pd_cap cap = is_pd_cap cap')"
|
||||
by (clarsimp simp: cap_master_cap_def is_cap_simps
|
||||
split: cap.splits arch_cap.splits)
|
||||
|
||||
lemma is_derived_cap_arch_asid_issues:
|
||||
"is_derived_arch cap cap' \<Longrightarrow>
|
||||
cap_master_cap cap = cap_master_cap cap'
|
||||
\<Longrightarrow> ((is_pt_cap cap \<or> is_pd_cap cap) \<longrightarrow> cap_asid cap \<noteq> None)
|
||||
\<and> (is_pg_cap cap \<or> (vs_cap_ref cap = vs_cap_ref cap'))"
|
||||
apply (simp add: is_derived_arch_def)
|
||||
by (auto simp: cap_master_cap_def is_cap_simps
|
||||
cap_asid_def
|
||||
split: cap.splits arch_cap.splits option.splits)
|
||||
|
||||
lemma is_pt_pd_Null[simp]:
|
||||
"\<not> is_pt_cap cap.NullCap \<and> \<not> is_pd_cap cap.NullCap"
|
||||
by (simp add: is_pt_cap_def is_pd_cap_def)
|
||||
|
||||
lemma unique_table_caps_upd_eqD:
|
||||
"\<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b';
|
||||
is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'\<rbrakk>
|
||||
\<Longrightarrow> unique_table_caps (ms (a \<mapsto> b')) = unique_table_caps (ms)"
|
||||
unfolding unique_table_caps_def
|
||||
apply (rule iffI)
|
||||
apply (intro allI impI,elim allE)
|
||||
apply (erule impE)
|
||||
apply (rule_tac p = p in fun_upd_Some)
|
||||
apply assumption
|
||||
apply (erule impE)
|
||||
apply (rule_tac p = p' in fun_upd_Some)
|
||||
apply simp
|
||||
apply (simp add: if_distrib split:if_splits)
|
||||
apply (intro allI impI,elim allE)
|
||||
apply (erule impE)
|
||||
apply (rule_tac p = p in fun_upd_Some_rev)
|
||||
apply simp+
|
||||
apply (erule impE)
|
||||
apply (rule_tac p = p' in fun_upd_Some_rev)
|
||||
apply simp+
|
||||
apply (simp add: if_distrib split:if_splits)
|
||||
done
|
||||
|
||||
lemma set_untyped_cap_as_full_not_final_not_pg_cap:
|
||||
"\<lbrace>\<lambda>s. (\<exists>a b. (a, b) \<noteq> dest \<and> \<not> is_pg_cap cap'
|
||||
\<and> cte_wp_at (\<lambda>cap. obj_irq_refs cap = obj_irq_refs cap' \<and> \<not> is_pg_cap cap) (a, b) s)
|
||||
\<and> cte_wp_at (op = src_cap) src s\<rbrace>
|
||||
set_untyped_cap_as_full src_cap cap src
|
||||
\<lbrace>\<lambda>_ s.(\<exists>a b. (a, b) \<noteq> dest \<and> \<not> is_pg_cap cap'
|
||||
\<and> cte_wp_at (\<lambda>cap. obj_irq_refs cap = obj_irq_refs cap' \<and> \<not> is_pg_cap cap) (a, b) s)\<rbrace>"
|
||||
apply (rule hoare_pre)
|
||||
apply (wp hoare_vcg_ex_lift)
|
||||
apply (rule_tac Q = "cte_wp_at Q slot"
|
||||
and Q'="cte_wp_at (op = src_cap) src" for Q slot in P_bool_lift' )
|
||||
apply (wp set_untyped_cap_as_full_cte_wp_at)
|
||||
subgoal by (auto simp: cte_wp_at_caps_of_state is_cap_simps masked_as_full_def cap_bits_untyped_def)
|
||||
apply (wp set_untyped_cap_as_full_cte_wp_at_neg)
|
||||
apply (auto simp: cte_wp_at_caps_of_state is_cap_simps masked_as_full_def cap_bits_untyped_def)
|
||||
done
|
||||
|
||||
lemma arch_derived_is_device:
|
||||
"\<lbrakk>cap_master_arch_cap c = cap_master_arch_cap c';
|
||||
is_derived_arch (ArchObjectCap c) (ArchObjectCap c')\<rbrakk>
|
||||
\<Longrightarrow> arch_cap_is_device c' = arch_cap_is_device c"
|
||||
apply (case_tac c)
|
||||
apply (clarsimp simp: is_derived_arch_def
|
||||
cap_range_def is_cap_simps cap_master_cap_def cap_master_arch_cap_def
|
||||
split: split_if_asm cap.splits arch_cap.splits)+
|
||||
done
|
||||
end
|
||||
end
|
||||
|
|
@ -0,0 +1,184 @@
|
|||
(*
|
||||
* Copyright 2014, General Dynamics C4 Systems
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_GPLv2.txt" for details.
|
||||
*
|
||||
* @TAG(GD_GPL)
|
||||
*)
|
||||
|
||||
theory ArchEmptyFail_AI
|
||||
imports "../EmptyFail_AI"
|
||||
begin
|
||||
|
||||
context Arch begin global_naming ARM
|
||||
|
||||
named_theorems EmptyFail_AI_assms
|
||||
|
||||
crunch_ignore (empty_fail)
|
||||
(add: invalidateTLB_ASID_impl invalidateTLB_VAASID_impl cleanByVA_impl
|
||||
cleanByVA_PoU_impl invalidateByVA_impl invalidateByVA_I_impl
|
||||
invalidate_I_PoU_impl cleanInvalByVA_impl branchFlush_impl
|
||||
clean_D_PoU_impl cleanInvalidate_D_PoC_impl cleanInvalidateL2Range_impl
|
||||
invalidateL2Range_impl cleanL2Range_impl flushBTAC_impl
|
||||
writeContextID_impl isb_impl dsb_impl dmb_impl setHardwareASID_impl
|
||||
writeTTBR0_impl cacheRangeOp)
|
||||
|
||||
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]:
|
||||
loadWord, load_word_offs, storeWord, getRestartPC, get_mrs
|
||||
|
||||
end
|
||||
|
||||
global_interpretation EmptyFail_AI_load_word?: EmptyFail_AI_load_word
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?)
|
||||
qed
|
||||
|
||||
context Arch begin global_naming ARM
|
||||
|
||||
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault
|
||||
(simp: kernel_object.splits option.splits arch_cap.splits cap.splits endpoint.splits
|
||||
bool.splits list.splits thread_state.splits split_def catch_def sum.splits
|
||||
Let_def wp: zipWithM_x_empty_fail)
|
||||
|
||||
crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notification, decode_unbind_notification
|
||||
(simp: cap.splits arch_cap.splits split_def)
|
||||
|
||||
lemma decode_tcb_invocation_empty_fail[wp]:
|
||||
"empty_fail (decode_tcb_invocation a b (ThreadCap p) d e)"
|
||||
by (simp add: decode_tcb_invocation_def split: invocation_label.splits | wp | intro conjI impI)+
|
||||
|
||||
crunch (empty_fail) empty_fail[wp]: find_pd_for_asid, get_master_pde, check_vp_alignment,
|
||||
create_mapping_entries, ensure_safe_mapping, get_asid_pool, resolve_vaddr
|
||||
(simp: kernel_object.splits arch_kernel_obj.splits option.splits pde.splits pte.splits)
|
||||
|
||||
lemma arch_decode_ARMASIDControlMakePool_empty_fail:
|
||||
"invocation_type label = ArchInvocationLabel ARMASIDControlMakePool
|
||||
\<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)"
|
||||
apply (simp add: arch_decode_invocation_def Let_def)
|
||||
apply (intro impI conjI allI)
|
||||
apply (simp add: isPageFlushLabel_def isPDFlushLabel_def split: arch_cap.splits)+
|
||||
apply (rule impI)
|
||||
apply (simp add: split_def)
|
||||
apply wp
|
||||
apply simp
|
||||
apply (subst bindE_assoc[symmetric])
|
||||
apply (rule empty_fail_bindE)
|
||||
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def bind_def return_def returnOk_def lift_def liftE_def fail_def gets_def get_def assert_def select_def split: split_if_asm)
|
||||
by (simp add: Let_def split: cap.splits arch_cap.splits option.splits bool.splits | wp | intro conjI impI allI)+
|
||||
|
||||
lemma arch_decode_ARMASIDPoolAssign_empty_fail:
|
||||
"invocation_type label = ArchInvocationLabel ARMASIDPoolAssign
|
||||
\<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)"
|
||||
apply (simp add: arch_decode_invocation_def split_def Let_def isPageFlushLabel_def isPDFlushLabel_def
|
||||
split: arch_cap.splits cap.splits option.splits | intro impI allI)+
|
||||
apply (rule empty_fail_bindE)
|
||||
apply simp
|
||||
apply (rule empty_fail_bindE)
|
||||
apply ((simp | wp)+)[1]
|
||||
apply (rule empty_fail_bindE)
|
||||
apply ((simp | wp)+)[1]
|
||||
apply (rule empty_fail_bindE)
|
||||
apply ((simp | wp)+)[1]
|
||||
apply (subst bindE_assoc[symmetric])
|
||||
apply (rule empty_fail_bindE)
|
||||
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_def bindE_def
|
||||
bind_def return_def returnOk_def lift_def liftE_def select_ext_def
|
||||
gets_def get_def assert_def fail_def)
|
||||
apply wp
|
||||
done
|
||||
|
||||
lemma arch_decode_invocation_empty_fail[wp]:
|
||||
"empty_fail (arch_decode_invocation label b c d e f)"
|
||||
apply (case_tac "invocation_type label")
|
||||
apply (find_goal \<open>match premises in "_ = ArchInvocationLabel _" \<Rightarrow> \<open>-\<close>\<close>)
|
||||
apply (rename_tac alabel)
|
||||
apply (case_tac alabel; simp)
|
||||
apply (find_goal \<open>succeeds \<open>erule arch_decode_ARMASIDControlMakePool_empty_fail\<close>\<close>)
|
||||
apply (find_goal \<open>succeeds \<open>erule arch_decode_ARMASIDPoolAssign_empty_fail\<close>\<close>)
|
||||
apply ((simp add: arch_decode_ARMASIDControlMakePool_empty_fail arch_decode_ARMASIDPoolAssign_empty_fail)+)[2]
|
||||
by ((simp add: arch_decode_invocation_def Let_def split: arch_cap.splits cap.splits option.splits | wp | intro conjI impI allI)+)
|
||||
|
||||
end
|
||||
|
||||
global_interpretation EmptyFail_AI_derive_cap?: EmptyFail_AI_derive_cap
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?)
|
||||
qed
|
||||
|
||||
context Arch begin global_naming ARM
|
||||
|
||||
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: maskInterrupt, empty_slot,
|
||||
setHardwareASID, setCurrentPD, finalise_cap, preemption_point,
|
||||
cap_swap_for_delete, decode_invocation
|
||||
(simp: Let_def catch_def split_def OR_choiceE_def mk_ef_def option.splits endpoint.splits
|
||||
notification.splits thread_state.splits sum.splits cap.splits arch_cap.splits
|
||||
kernel_object.splits vmpage_size.splits pde.splits bool.splits list.splits)
|
||||
|
||||
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: setRegister, setNextPC
|
||||
|
||||
end
|
||||
|
||||
global_interpretation EmptyFail_AI_rec_del?: EmptyFail_AI_rec_del
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?)
|
||||
qed
|
||||
|
||||
context Arch begin global_naming ARM
|
||||
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]:
|
||||
cap_delete, choose_thread
|
||||
end
|
||||
|
||||
global_interpretation EmptyFail_AI_schedule_unit?: EmptyFail_AI_schedule_unit
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?)
|
||||
qed
|
||||
|
||||
global_interpretation EmptyFail_AI_schedule_det?: EmptyFail_AI_schedule_det
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?)
|
||||
qed
|
||||
|
||||
global_interpretation EmptyFail_AI_schedule?: EmptyFail_AI_schedule
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?)
|
||||
qed
|
||||
|
||||
context Arch begin global_naming ARM
|
||||
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_event, activate_thread
|
||||
(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
|
||||
thread_state.splits endpoint.splits catch_def sum.splits cnode_invocation.splits
|
||||
page_table_invocation.splits page_invocation.splits asid_control_invocation.splits
|
||||
asid_pool_invocation.splits arch_invocation.splits irq_state.splits syscall.splits
|
||||
flush_type.splits page_directory_invocation.splits
|
||||
ignore: resetTimer_impl ackInterrupt_impl)
|
||||
end
|
||||
|
||||
global_interpretation EmptyFail_AI_call_kernel_unit?: EmptyFail_AI_call_kernel_unit
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?)
|
||||
qed
|
||||
|
||||
global_interpretation EmptyFail_AI_call_kernel_det?: EmptyFail_AI_call_kernel_det
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?)
|
||||
qed
|
||||
|
||||
global_interpretation EmptyFail_AI_call_kernel?: EmptyFail_AI_call_kernel
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?)
|
||||
qed
|
||||
|
||||
end
|
||||
|
|
@ -0,0 +1,40 @@
|
|||
(*
|
||||
* Copyright 2014, General Dynamics C4 Systems
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_GPLv2.txt" for details.
|
||||
*
|
||||
* @TAG(GD_GPL)
|
||||
*)
|
||||
|
||||
(*
|
||||
Arch-specific retype invariants
|
||||
*)
|
||||
|
||||
theory ArchInterruptAcc_AI
|
||||
imports "../InterruptAcc_AI"
|
||||
begin
|
||||
|
||||
context Arch begin global_naming ARM
|
||||
|
||||
named_theorems InterruptAcc_AI_assms
|
||||
|
||||
lemma dmo_maskInterrupt_invs [InterruptAcc_AI_assms]:
|
||||
"\<lbrace>all_invs_but_valid_irq_states_for irq and (\<lambda>s. state = interrupt_states s irq)\<rbrace>
|
||||
do_machine_op (maskInterrupt (state = IRQInactive) irq)
|
||||
\<lbrace>\<lambda>rv. invs\<rbrace>"
|
||||
apply (simp add: do_machine_op_def split_def maskInterrupt_def)
|
||||
apply wp
|
||||
apply (clarsimp simp: in_monad invs_def valid_state_def all_invs_but_valid_irq_states_for_def valid_irq_states_but_def valid_irq_masks_but_def valid_machine_state_def cur_tcb_def valid_irq_states_def valid_irq_masks_def)
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
global_interpretation InterruptAcc_AI?: InterruptAcc_AI
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case by (unfold_locales; fact InterruptAcc_AI_assms)
|
||||
qed
|
||||
|
||||
end
|
||||
|
|
@ -154,8 +154,8 @@ With hypervisor extensions, kernel and user MMUs are completely independent. How
|
|||
> copyGlobalMappings newPD = do
|
||||
> globalPT <- gets (armUSGlobalPT . ksArchState)
|
||||
> let pde = PageTablePDE (addrFromPPtr globalPT)
|
||||
> let pdSize = bit (pdBits - pdeBits)
|
||||
> let offset = (pdSize - 1) `shiftL` pdeBits -- FIXME ARMHYP yuck
|
||||
> let pdSize = bit (pdBits)
|
||||
> let offset = pdSize - bit pdeBits
|
||||
> storePDE (newPD + offset) pde
|
||||
|
||||
\subsection{Creating and Updating Mappings}
|
||||
|
|
@ -862,8 +862,8 @@ Note that these capabilities cannot be copied until they have been mapped, so an
|
|||
> throw $ InvalidArgument 0
|
||||
> pdCheck <- lookupErrorOnFailure False $ findPDForASID asid
|
||||
> when (pdCheck /= pd) $ throw $ InvalidCapability 1
|
||||
> let pdIndex = vaddr `shiftR` (ptBits - pdeBits + ptBits - pteBits) -- FIXME ARMHYP is this right? replacing magic numbers
|
||||
> let vaddr' = pdIndex `shiftL` (ptBits - pdeBits + ptBits - pteBits)
|
||||
> let pdIndex = vaddr `shiftR` (pageBits + ptBits - pteBits)
|
||||
> let vaddr' = pdIndex `shiftL` (pageBits + ptBits - pteBits)
|
||||
> let pdSlot = pd + (PPtr $ pdIndex `shiftL` pdeBits)
|
||||
> oldpde <- withoutFailure $ getObject pdSlot
|
||||
> unless (oldpde == InvalidPDE) $ throw DeleteFirst
|
||||
|
|
|
|||
|
|
@ -649,11 +649,13 @@ With hypervisor extensions enabled, page table and page directory entries occupy
|
|||
#else /* CONFIG_ARM_HYPERVISOR_SUPPORT */
|
||||
|
||||
ARM page directories and page tables occupy four frames and one quarter of a frame, respectively.
|
||||
FIXME ARMHYP define pteBits and pdeBits in terms of objBits of the right kind of object
|
||||
FIXME ARMHYP in C, we might want to call them PD\_INDEX\_BITS instead of PD\_BITS - tell Adrian
|
||||
|
||||
> pteBits = (2 :: Int)
|
||||
> pdeBits = (2 :: Int)
|
||||
> pdBits = (12 :: Int) `shiftL` pdeBits
|
||||
> ptBits = (8 :: Int) `shiftL` pteBits
|
||||
> pdBits = (12 :: Int) + pdeBits
|
||||
> ptBits = (8 :: Int) + pteBits
|
||||
|
||||
FIXME ARMHYP this is a bit silly: in the C code we have pdBits be 12 and ptBits 8,
|
||||
not the size of the whole thing. In fact, in the haskell we often have to shift pdBits right by the size of the PDE, which get by calling objBits on a new PDE...
|
||||
|
|
@ -668,14 +670,14 @@ FIXME ARMHYP therefore pdeBits and pteBits are not used much outside of here
|
|||
|
||||
\subsubsection{IO Page Table Structure}
|
||||
|
||||
FIXME ARMHYP ptBits is not the total size of a page table, so this is at best confusing, at worst wrong
|
||||
|
||||
> ioptBits :: Int
|
||||
> ioptBits = pageBits
|
||||
|
||||
FIXME ARMHYP this is really platform code (TK1), move there
|
||||
FIXME ARMHYP this is so very very verbose, but there is no way to know if we will care about the differences between a page table IOPDE entry and a 4M section one.
|
||||
|
||||
FIXME ARMHYP TODO we want to have invalid PDE and PTEs
|
||||
|
||||
> data IOPDE -- FIXME ARMHYP where is InvalidIOPDE?
|
||||
> = PageTableIOPDE {
|
||||
> iopdeFrame :: PAddr,
|
||||
|
|
@ -727,6 +729,3 @@ FIXME ARMHYP this is so very very verbose, but there is no way to know if we wil
|
|||
> kernelBase :: VPtr
|
||||
> kernelBase = Platform.kernelBase
|
||||
|
||||
FIXME ARMHYP MOVE extra machine ops
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -49,6 +49,8 @@ There are three ARM-specific global data elements:
|
|||
\end{itemize}
|
||||
|
||||
FIXME ARMHYP there is no sign of armKSASIDMap - what is it??
|
||||
it is the representation in ghost state of storing hwasids into the last invalid entry of a PD
|
||||
|
||||
FIXME ARMHYP there is no sign of armKSKernelVSpace - ghost state
|
||||
|
||||
FIXME ARMHYP has no global PD and PTs, but the more complicated stage 1 translation for its own address space set up at boot time and then never used again ... it is unclear if we should model this at this time... see arm/32/model/statedata.c ... it is only set up during kernel boot. ARM_HYP doesn't really have a global PD that gets copied everywhere
|
||||
|
|
|
|||
|
|
@ -45,3 +45,5 @@ This module defines instances of "PSpaceStorable" for ARM-specific kernel object
|
|||
|
||||
FIXME ARMHYP not looked at these at all, assuming type error will happen when we try store/load an object type we haven't indicated is PSpaceStorable
|
||||
|
||||
FIXME ARMHYP we want these for IOPTE IOPDE and maybe VCPU
|
||||
|
||||
|
|
|
|||
|
|
@ -62,7 +62,7 @@ FIXME ARMHYP frame caps in C have an isIOSpace property - add this here, or add
|
|||
> capIOSpaceClientID :: Word16 }
|
||||
> | IOPageDirectoryCap {
|
||||
> capIOPDBasePtr :: PPtr IOPDE,
|
||||
> capIOPDMappedAddress :: Maybe (ASID) } -- FIXME ARMHYP where is mapped address?
|
||||
> capIOPDMappedAddress :: Maybe (ASID) } -- FIXME ARMHYP where is mapped address? note that this ASID is in a different namespace (IOMMU not MMU) - stable, deviceID by convention
|
||||
> | IOPageTableCap {
|
||||
> capIOPTBasePtr :: PPtr IOPTE,
|
||||
> capIOPTMappedAddress :: Maybe (ASID, VPtr) } -- FIXME ARMHYP Vptr or PAddr?
|
||||
|
|
@ -73,9 +73,9 @@ FIXME ARMHYP frame caps in C have an isIOSpace property - add this here, or add
|
|||
|
||||
The ARM kernel stores one ARM-specific type of object in the PSpace: ASID pools, which are second level nodes in the global ASID table.
|
||||
|
||||
FIXME ARMHYP how does the above comment possibly relate to the ArchKernelObject datatype?
|
||||
FIXME ARMHYP how does the above comment possibly relate to the ArchKernelObject datatype? fix comment
|
||||
|
||||
FIXME ARMHYP TODO IOPT needs to go here for sure, but what about VCPU? if it was clear what these did, one could decide
|
||||
FIXME ARMHYP TODO IOPTE needs to go here for sure, but what about VCPU? if it was clear what these did, one could decide
|
||||
|
||||
> data ArchKernelObject
|
||||
> = KOASIDPool ASIDPool
|
||||
|
|
@ -83,7 +83,7 @@ FIXME ARMHYP TODO IOPT needs to go here for sure, but what about VCPU? if it was
|
|||
> | KOPDE PDE
|
||||
> deriving Show
|
||||
|
||||
FIXME ARMHYP add IOPTE and IOPDE to ArchKernelObject?
|
||||
FIXME ARMHYP add IOPTE and IOPDE to ArchKernelObject? - YES VCPU - MAYBE
|
||||
|
||||
> archObjSize :: ArchKernelObject -> Int
|
||||
> archObjSize a = case a of
|
||||
|
|
@ -110,7 +110,7 @@ An ASID is an unsigned word. Note that it is a \emph{virtual} address space iden
|
|||
|
||||
ASIDs are mapped to address space roots by a global two-level table. The actual ASID values are opaque to the user, as are the sizes of the levels of the tables; ASID allocation calls will simply return an error once the available ASIDs are exhausted.
|
||||
|
||||
FIXME ARMHYP unclear if bit manipulation still correct
|
||||
FIXME ARMHYP unclear if bit manipulation still correct - we lose one bit down to 7 for isIOSpace, and then 6 after deviceUntyped patch - make it 7/6 (with/without IOMMU)
|
||||
|
||||
> asidHighBits :: Int
|
||||
> asidHighBits = 8
|
||||
|
|
|
|||
|
|
@ -74,7 +74,7 @@ then
|
|||
(cd $L4CAP && git status --short) >> $SPEC/version
|
||||
fi
|
||||
|
||||
ARCHES=("ARM" "X64")
|
||||
ARCHES=("ARM" "X64" "ARM_HYP")
|
||||
|
||||
NAMES=`cd $SKEL; ls *.thy`
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue