arch_split: InfoFlowC checking
This commit is contained in:
parent
56b226a608
commit
b16496e7cf
|
@ -13,6 +13,7 @@ imports
|
||||||
"ADT_IF" "../refine/Refine" "../refine/EmptyFail_H"
|
"ADT_IF" "../refine/Refine" "../refine/EmptyFail_H"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
||||||
definition
|
definition
|
||||||
kernelEntry_if
|
kernelEntry_if
|
||||||
|
@ -403,7 +404,7 @@ lemma do_user_op_if_corres':
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
apply (rule corres_machine_op')
|
apply (rule corres_machine_op')
|
||||||
apply (rule corres_underlying_trivial)
|
apply (rule corres_underlying_trivial)
|
||||||
apply wp
|
apply (wp do_machine_op_domain_list)
|
||||||
apply (clarsimp simp: addrFromPPtr_def)
|
apply (clarsimp simp: addrFromPPtr_def)
|
||||||
apply (rule corres_machine_op')
|
apply (rule corres_machine_op')
|
||||||
apply (rule corres_underlying_trivial)
|
apply (rule corres_underlying_trivial)
|
||||||
|
@ -489,7 +490,7 @@ lemma check_active_irq_if_corres:
|
||||||
apply (simp add: checkActiveIRQ_if_def check_active_irq_if_def)
|
apply (simp add: checkActiveIRQ_if_def check_active_irq_if_def)
|
||||||
apply (rule corres_underlying_split[where r'="op ="])
|
apply (rule corres_underlying_split[where r'="op ="])
|
||||||
apply (rule dmo_getActiveIRQ_corres)
|
apply (rule dmo_getActiveIRQ_corres)
|
||||||
apply wp
|
apply (wp do_machine_op_domain_list)
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
done
|
done
|
||||||
|
|
||||||
|
@ -854,9 +855,7 @@ lemma step_corresE:
|
||||||
apply simp+
|
apply simp+
|
||||||
done
|
done
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
locale global_automaton_invs =
|
locale global_automaton_invs =
|
||||||
fixes check_active_irq
|
fixes check_active_irq
|
||||||
|
|
|
@ -13,6 +13,7 @@ imports
|
||||||
"ADT_IF_Refine" "../crefine/Refine_C"
|
"ADT_IF_Refine" "../crefine/Refine_C"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
||||||
definition handleInterruptEntry_C_body_if (*:: "(globals myvars, int, l4c_errortype) com"*) where
|
definition handleInterruptEntry_C_body_if (*:: "(globals myvars, int, l4c_errortype) com"*) where
|
||||||
"handleInterruptEntry_C_body_if \<equiv> (
|
"handleInterruptEntry_C_body_if \<equiv> (
|
||||||
|
@ -96,7 +97,7 @@ definition handleVMFaultEvent_C_body_if
|
||||||
FI;;
|
FI;;
|
||||||
\<acute>ret__unsigned_long :== scast EXCEPTION_NONE))"
|
\<acute>ret__unsigned_long :== scast EXCEPTION_NONE))"
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
context kernel_m begin
|
context kernel_m begin
|
||||||
|
|
||||||
|
@ -161,9 +162,9 @@ proof -
|
||||||
apply (rule allI, rule conseqPre, vcg)
|
apply (rule allI, rule conseqPre, vcg)
|
||||||
apply (clarsimp simp: return_def)
|
apply (clarsimp simp: return_def)
|
||||||
apply wp
|
apply wp
|
||||||
apply (rule_tac Q="\<lambda>rv s. invs' s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> Platform.maxIRQ)
|
apply (rule_tac Q="\<lambda>rv s. invs' s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ)
|
||||||
\<and> rv \<noteq> Some 0xFFFF" in hoare_post_imp)
|
\<and> rv \<noteq> Some 0xFFFF" in hoare_post_imp)
|
||||||
apply (clarsimp simp: Kernel_C.maxIRQ_def Platform.maxIRQ_def)
|
apply (clarsimp simp: Kernel_C.maxIRQ_def ARM.maxIRQ_def)
|
||||||
apply (wp getActiveIRQ_le_maxIRQ getActiveIRQ_neq_Some0xFF | simp)+
|
apply (wp getActiveIRQ_le_maxIRQ getActiveIRQ_neq_Some0xFF | simp)+
|
||||||
apply (clarsimp simp: invs'_def valid_state'_def)
|
apply (clarsimp simp: invs'_def valid_state'_def)
|
||||||
done
|
done
|
||||||
|
|
|
@ -14,6 +14,8 @@ imports
|
||||||
ADT_IF_Refine
|
ADT_IF_Refine
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
||||||
section {* Haskell state *}
|
section {* Haskell state *}
|
||||||
|
|
||||||
text {* One invariant we need on s0 is that there exists
|
text {* One invariant we need on s0 is that there exists
|
||||||
|
@ -44,7 +46,7 @@ where
|
||||||
(the_nat_to_bl_10 2)
|
(the_nat_to_bl_10 2)
|
||||||
\<mapsto> (Structures_H.CNodeCap Low_cnode_ptr 10 2 10, MDB 0 Low_tcb_ptr False False),
|
\<mapsto> (Structures_H.CNodeCap Low_cnode_ptr 10 2 10, MDB 0 Low_tcb_ptr False False),
|
||||||
(the_nat_to_bl_10 3)
|
(the_nat_to_bl_10 3)
|
||||||
\<mapsto> (Structures_H.ArchObjectCap (ArchStructures_H.PageDirectoryCap Low_pd_ptr
|
\<mapsto> (Structures_H.ArchObjectCap (ARM_H.PageDirectoryCap Low_pd_ptr
|
||||||
(Some Low_asid)), MDB 0 (Low_tcb_ptr + 0x10) False False),
|
(Some Low_asid)), MDB 0 (Low_tcb_ptr + 0x10) False False),
|
||||||
(the_nat_to_bl_10 318)
|
(the_nat_to_bl_10 318)
|
||||||
\<mapsto> (Structures_H.NotificationCap ntfn_ptr 0 True False,
|
\<mapsto> (Structures_H.NotificationCap ntfn_ptr 0 True False,
|
||||||
|
@ -74,7 +76,7 @@ where
|
||||||
(the_nat_to_bl_10 2)
|
(the_nat_to_bl_10 2)
|
||||||
\<mapsto> (Structures_H.CNodeCap High_cnode_ptr 10 2 10, MDB 0 High_tcb_ptr False False),
|
\<mapsto> (Structures_H.CNodeCap High_cnode_ptr 10 2 10, MDB 0 High_tcb_ptr False False),
|
||||||
(the_nat_to_bl_10 3)
|
(the_nat_to_bl_10 3)
|
||||||
\<mapsto> (Structures_H.ArchObjectCap (ArchStructures_H.PageDirectoryCap High_pd_ptr
|
\<mapsto> (Structures_H.ArchObjectCap (ARM_H.PageDirectoryCap High_pd_ptr
|
||||||
(Some High_asid)), MDB 0 (High_tcb_ptr + 0x10) False False),
|
(Some High_asid)), MDB 0 (High_tcb_ptr + 0x10) False False),
|
||||||
(the_nat_to_bl_10 318)
|
(the_nat_to_bl_10 318)
|
||||||
\<mapsto> (Structures_H.NotificationCap ntfn_ptr 0 False True,
|
\<mapsto> (Structures_H.NotificationCap ntfn_ptr 0 False True,
|
||||||
|
@ -127,33 +129,33 @@ where
|
||||||
text {* Low's VSpace (PageDirectory)*}
|
text {* Low's VSpace (PageDirectory)*}
|
||||||
|
|
||||||
definition
|
definition
|
||||||
Low_pt'H :: "word8 \<Rightarrow> Hardware_H.pte "
|
Low_pt'H :: "word8 \<Rightarrow> ARM_H.pte "
|
||||||
where
|
where
|
||||||
"Low_pt'H \<equiv> (\<lambda>_. Hardware_H.InvalidPTE)
|
"Low_pt'H \<equiv> (\<lambda>_. ARM_H.InvalidPTE)
|
||||||
(0 := Hardware_H.SmallPagePTE shared_page_ptr (PageCacheable \<in> {}) (Global \<in> {}) (XNever \<in> {}) (vmrights_map vm_read_write))"
|
(0 := ARM_H.SmallPagePTE shared_page_ptr (PageCacheable \<in> {}) (Global \<in> {}) (XNever \<in> {}) (vmrights_map vm_read_write))"
|
||||||
|
|
||||||
definition
|
definition
|
||||||
Low_ptH :: "word32 \<Rightarrow> word32 \<Rightarrow> Structures_H.kernel_object option"
|
Low_ptH :: "word32 \<Rightarrow> word32 \<Rightarrow> Structures_H.kernel_object option"
|
||||||
where
|
where
|
||||||
"Low_ptH \<equiv>
|
"Low_ptH \<equiv>
|
||||||
\<lambda>base. (map_option (\<lambda>x. Structures_H.KOArch (ArchStructures_H.KOPTE (Low_pt'H x)))) \<circ>
|
\<lambda>base. (map_option (\<lambda>x. Structures_H.KOArch (ARM_H.KOPTE (Low_pt'H x)))) \<circ>
|
||||||
(\<lambda>offs. if is_aligned offs 2 \<and> base \<le> offs \<and> offs \<le> base + 2 ^ 10 - 1
|
(\<lambda>offs. if is_aligned offs 2 \<and> base \<le> offs \<and> offs \<le> base + 2 ^ 10 - 1
|
||||||
then Some (ucast (offs - base >> 2)) else None)"
|
then Some (ucast (offs - base >> 2)) else None)"
|
||||||
|
|
||||||
definition
|
definition
|
||||||
[simp]:
|
[simp]:
|
||||||
"global_pdH \<equiv> (\<lambda>_. Hardware_H.InvalidPDE)( ucast (kernel_base >> 20) :=
|
"global_pdH \<equiv> (\<lambda>_. ARM_H.InvalidPDE)( ucast (kernel_base >> 20) :=
|
||||||
Hardware_H.SectionPDE (addrFromPPtr kernel_base) (ParityEnabled \<in> {}) 0
|
ARM_H.SectionPDE (addrFromPPtr kernel_base) (ParityEnabled \<in> {}) 0
|
||||||
(PageCacheable \<in> {}) (Global \<in> {}) (XNever \<in> {}) (vmrights_map {}))"
|
(PageCacheable \<in> {}) (Global \<in> {}) (XNever \<in> {}) (vmrights_map {}))"
|
||||||
|
|
||||||
|
|
||||||
definition
|
definition
|
||||||
Low_pd'H :: "12 word \<Rightarrow> Hardware_H.pde "
|
Low_pd'H :: "12 word \<Rightarrow> ARM_H.pde "
|
||||||
where
|
where
|
||||||
"Low_pd'H \<equiv>
|
"Low_pd'H \<equiv>
|
||||||
global_pdH
|
global_pdH
|
||||||
(0 := Hardware_H.PageTablePDE
|
(0 := ARM_H.PageTablePDE
|
||||||
(Platform.addrFromPPtr Low_pt_ptr)
|
(addrFromPPtr Low_pt_ptr)
|
||||||
(ParityEnabled \<in> {})
|
(ParityEnabled \<in> {})
|
||||||
undefined)"
|
undefined)"
|
||||||
|
|
||||||
|
@ -164,7 +166,7 @@ definition
|
||||||
Low_pdH :: "word32 \<Rightarrow> word32 \<Rightarrow> Structures_H.kernel_object option"
|
Low_pdH :: "word32 \<Rightarrow> word32 \<Rightarrow> Structures_H.kernel_object option"
|
||||||
where
|
where
|
||||||
"Low_pdH \<equiv>
|
"Low_pdH \<equiv>
|
||||||
\<lambda>base. (map_option (\<lambda>x. Structures_H.KOArch (ArchStructures_H.KOPDE (Low_pd'H x)))) \<circ>
|
\<lambda>base. (map_option (\<lambda>x. Structures_H.KOArch (ARM_H.KOPDE (Low_pd'H x)))) \<circ>
|
||||||
(\<lambda>offs. if is_aligned offs 2 \<and> base \<le> offs \<and> offs \<le> base + 2 ^ 14 - 1
|
(\<lambda>offs. if is_aligned offs 2 \<and> base \<le> offs \<and> offs \<le> base + 2 ^ 14 - 1
|
||||||
then Some (ucast (offs - base >> 2)) else None)"
|
then Some (ucast (offs - base >> 2)) else None)"
|
||||||
|
|
||||||
|
@ -173,11 +175,11 @@ text {* High's VSpace (PageDirectory)*}
|
||||||
|
|
||||||
|
|
||||||
definition
|
definition
|
||||||
High_pt'H :: "word8 \<Rightarrow> Hardware_H.pte "
|
High_pt'H :: "word8 \<Rightarrow> ARM_H.pte "
|
||||||
where
|
where
|
||||||
"High_pt'H \<equiv>
|
"High_pt'H \<equiv>
|
||||||
(\<lambda>_. Hardware_H.InvalidPTE)
|
(\<lambda>_. ARM_H.InvalidPTE)
|
||||||
(0 := Hardware_H.SmallPagePTE shared_page_ptr (PageCacheable \<in> {}) (Global \<in> {}) (XNever \<in> {})
|
(0 := ARM_H.SmallPagePTE shared_page_ptr (PageCacheable \<in> {}) (Global \<in> {}) (XNever \<in> {})
|
||||||
(vmrights_map vm_read_only))"
|
(vmrights_map vm_read_only))"
|
||||||
|
|
||||||
|
|
||||||
|
@ -185,18 +187,18 @@ definition
|
||||||
High_ptH :: "word32 \<Rightarrow> word32 \<Rightarrow> Structures_H.kernel_object option"
|
High_ptH :: "word32 \<Rightarrow> word32 \<Rightarrow> Structures_H.kernel_object option"
|
||||||
where
|
where
|
||||||
"High_ptH \<equiv>
|
"High_ptH \<equiv>
|
||||||
\<lambda>base. (map_option (\<lambda>x. Structures_H.KOArch (ArchStructures_H.KOPTE (High_pt'H x)))) \<circ>
|
\<lambda>base. (map_option (\<lambda>x. Structures_H.KOArch (ARM_H.KOPTE (High_pt'H x)))) \<circ>
|
||||||
(\<lambda>offs. if is_aligned offs 2 \<and> base \<le> offs \<and> offs \<le> base + 2 ^ 10 - 1
|
(\<lambda>offs. if is_aligned offs 2 \<and> base \<le> offs \<and> offs \<le> base + 2 ^ 10 - 1
|
||||||
then Some (ucast (offs - base >> 2)) else None)"
|
then Some (ucast (offs - base >> 2)) else None)"
|
||||||
|
|
||||||
|
|
||||||
definition
|
definition
|
||||||
High_pd'H :: "12 word \<Rightarrow> Hardware_H.pde "
|
High_pd'H :: "12 word \<Rightarrow> ARM_H.pde "
|
||||||
where
|
where
|
||||||
"High_pd'H \<equiv>
|
"High_pd'H \<equiv>
|
||||||
global_pdH
|
global_pdH
|
||||||
(0 := Hardware_H.PageTablePDE
|
(0 := ARM_H.PageTablePDE
|
||||||
(Platform.addrFromPPtr High_pt_ptr)
|
(addrFromPPtr High_pt_ptr)
|
||||||
(ParityEnabled \<in> {})
|
(ParityEnabled \<in> {})
|
||||||
undefined )"
|
undefined )"
|
||||||
|
|
||||||
|
@ -207,7 +209,7 @@ definition
|
||||||
High_pdH :: "word32 \<Rightarrow> word32 \<Rightarrow> Structures_H.kernel_object option"
|
High_pdH :: "word32 \<Rightarrow> word32 \<Rightarrow> Structures_H.kernel_object option"
|
||||||
where
|
where
|
||||||
"High_pdH \<equiv>
|
"High_pdH \<equiv>
|
||||||
\<lambda>base. (map_option (\<lambda>x. Structures_H.KOArch (ArchStructures_H.KOPDE (High_pd'H x)))) \<circ>
|
\<lambda>base. (map_option (\<lambda>x. Structures_H.KOArch (ARM_H.KOPDE (High_pd'H x)))) \<circ>
|
||||||
(\<lambda>offs. if is_aligned offs 2 \<and> base \<le> offs \<and> offs \<le> base + 2 ^ 14 - 1
|
(\<lambda>offs. if is_aligned offs 2 \<and> base \<le> offs \<and> offs \<le> base + 2 ^ 14 - 1
|
||||||
then Some (ucast (offs - base >> 2)) else None)"
|
then Some (ucast (offs - base >> 2)) else None)"
|
||||||
|
|
||||||
|
@ -296,7 +298,7 @@ definition
|
||||||
global_pdH' :: "word32 \<Rightarrow> word32 \<Rightarrow> Structures_H.kernel_object option"
|
global_pdH' :: "word32 \<Rightarrow> word32 \<Rightarrow> Structures_H.kernel_object option"
|
||||||
where
|
where
|
||||||
"global_pdH' \<equiv> \<lambda>base.
|
"global_pdH' \<equiv> \<lambda>base.
|
||||||
(map_option (\<lambda>x. Structures_H.KOArch (ArchStructures_H.KOPDE (global_pdH (x::12 word))))) \<circ>
|
(map_option (\<lambda>x. Structures_H.KOArch (ARM_H.KOPDE (global_pdH (x::12 word))))) \<circ>
|
||||||
(\<lambda>offs. if is_aligned offs 2 \<and> base \<le> offs \<and> offs \<le> base + 2 ^ 14 - 1
|
(\<lambda>offs. if is_aligned offs 2 \<and> base \<le> offs \<and> offs \<le> base + 2 ^ 14 - 1
|
||||||
then Some (ucast (offs - base >> 2)) else None)"
|
then Some (ucast (offs - base >> 2)) else None)"
|
||||||
|
|
||||||
|
@ -1077,7 +1079,7 @@ lemma kh0H_SomeD:
|
||||||
apply (clarsimp | frule offs_range_correct)+
|
apply (clarsimp | frule offs_range_correct)+
|
||||||
done
|
done
|
||||||
|
|
||||||
definition arch_state0H :: ArchStateData_H.kernel_state where
|
definition arch_state0H :: Arch.kernel_state where
|
||||||
"arch_state0H \<equiv> ARMKernelState
|
"arch_state0H \<equiv> ARMKernelState
|
||||||
(* armKSGlobalsFrame = *) init_globals_frame
|
(* armKSGlobalsFrame = *) init_globals_frame
|
||||||
(* armKSASIDTable = *) Map.empty
|
(* armKSASIDTable = *) Map.empty
|
||||||
|
@ -2176,17 +2178,17 @@ lemma s0H_valid_objs':
|
||||||
apply (clarsimp simp: valid_obj'_def Low_cte_def Low_cte'_def Low_capsH_def empty_cte_def valid_cte'_def split: split_if_asm)
|
apply (clarsimp simp: valid_obj'_def Low_cte_def Low_cte'_def Low_capsH_def empty_cte_def valid_cte'_def split: split_if_asm)
|
||||||
apply (clarsimp simp: valid_obj'_def High_cte_def High_cte'_def High_capsH_def empty_cte_def valid_cte'_def split: split_if_asm)
|
apply (clarsimp simp: valid_obj'_def High_cte_def High_cte'_def High_capsH_def empty_cte_def valid_cte'_def split: split_if_asm)
|
||||||
apply (clarsimp simp: valid_obj'_def Silc_cte_def Silc_cte'_def Silc_capsH_def empty_cte_def valid_cte'_def split: split_if_asm)
|
apply (clarsimp simp: valid_obj'_def Silc_cte_def Silc_cte'_def Silc_capsH_def empty_cte_def valid_cte'_def split: split_if_asm)
|
||||||
apply (clarsimp simp: valid_obj'_def global_pdH'_def valid_mapping'_def s0_ptr_defs is_aligned_def Platform.addrFromPPtr_def Platform.ptrFromPAddr_def
|
apply (clarsimp simp: valid_obj'_def global_pdH'_def valid_mapping'_def s0_ptr_defs is_aligned_def ARM.addrFromPPtr_def ARM.ptrFromPAddr_def
|
||||||
physMappingOffset_def Platform.kernelBase_def Platform.physBase_def
|
physMappingOffset_def ARM.kernelBase_def ARM.physBase_def
|
||||||
kernelBase_addr_def physBase_def split: split_if_asm)
|
kernelBase_addr_def physBase_def split: split_if_asm)
|
||||||
apply (clarsimp simp: valid_obj'_def High_pdH_def High_pd'H_def valid_pde'_def valid_mapping'_def s0_ptr_defs is_aligned_def Platform.addrFromPPtr_def
|
apply (clarsimp simp: valid_obj'_def High_pdH_def High_pd'H_def valid_pde'_def valid_mapping'_def s0_ptr_defs is_aligned_def ARM.addrFromPPtr_def
|
||||||
Platform.kernelBase_def Platform.physBase_def Platform.ptrFromPAddr_def ptBits_def pageBits_def physMappingOffset_def kernelBase_addr_def physBase_def split: split_if_asm)
|
ARM.kernelBase_def ARM.physBase_def ARM.ptrFromPAddr_def ptBits_def pageBits_def physMappingOffset_def kernelBase_addr_def physBase_def split: split_if_asm)
|
||||||
apply (clarsimp simp: valid_obj'_def Low_pdH_def Low_pd'H_def valid_pde'_def valid_mapping'_def s0_ptr_defs is_aligned_def Platform.addrFromPPtr_def
|
apply (clarsimp simp: valid_obj'_def Low_pdH_def Low_pd'H_def valid_pde'_def valid_mapping'_def s0_ptr_defs is_aligned_def ARM.addrFromPPtr_def
|
||||||
Platform.ptrFromPAddr_def Platform.physBase_def ptBits_def pageBits_def physMappingOffset_def kernelBase_addr_def physBase_def split: split_if_asm)
|
ARM.ptrFromPAddr_def ARM.physBase_def ptBits_def pageBits_def physMappingOffset_def kernelBase_addr_def physBase_def split: split_if_asm)
|
||||||
apply (clarsimp simp: valid_obj'_def High_ptH_def High_pt'H_def valid_mapping'_def s0_ptr_defs is_aligned_def Platform.addrFromPPtr_def
|
apply (clarsimp simp: valid_obj'_def High_ptH_def High_pt'H_def valid_mapping'_def s0_ptr_defs is_aligned_def ARM.addrFromPPtr_def
|
||||||
Platform.ptrFromPAddr_def Platform.kernelBase_def Platform.physBase_def physMappingOffset_def kernelBase_addr_def physBase_def split: split_if_asm)
|
ARM.ptrFromPAddr_def ARM.kernelBase_def ARM.physBase_def physMappingOffset_def kernelBase_addr_def physBase_def split: split_if_asm)
|
||||||
apply (clarsimp simp: valid_obj'_def Low_ptH_def Low_pt'H_def valid_mapping'_def s0_ptr_defs is_aligned_def Platform.addrFromPPtr_def
|
apply (clarsimp simp: valid_obj'_def Low_ptH_def Low_pt'H_def valid_mapping'_def s0_ptr_defs is_aligned_def ARM.addrFromPPtr_def
|
||||||
Platform.physBase_def Platform.ptrFromPAddr_def physMappingOffset_def kernelBase_addr_def physBase_def split: split_if_asm)
|
ARM.physBase_def ARM.ptrFromPAddr_def physMappingOffset_def kernelBase_addr_def physBase_def split: split_if_asm)
|
||||||
done
|
done
|
||||||
|
|
||||||
lemmas the_nat_to_bl_simps =
|
lemmas the_nat_to_bl_simps =
|
||||||
|
@ -2426,10 +2428,10 @@ lemma sameRegionAs_s0H:
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' s0_ptr_defs split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' s0_ptr_defs split: split_if_asm)
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_2 s0_ptrs_aligned split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_2 s0_ptrs_aligned split: split_if_asm)
|
||||||
apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD)
|
apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD)
|
||||||
apply (elim disjE, simp_all add: sameRegionAs_def ArchRetype_H.sameRegionAs_def isCap_simps)[1]
|
apply (elim disjE, simp_all add: sameRegionAs_def ARM_H.sameRegionAs_def isCap_simps)[1]
|
||||||
apply (simp add: s0_ptr_defs)
|
apply (simp add: s0_ptr_defs)
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' s0_ptr_defs split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' s0_ptr_defs split: split_if_asm)
|
||||||
apply (clarsimp simp: ArchRetype_H.sameRegionAs_def isCap_simps kh0H_all_obj_def' s0_ptr_defs split: split_if_asm)
|
apply (clarsimp simp: ARM_H.sameRegionAs_def isCap_simps kh0H_all_obj_def' s0_ptr_defs split: split_if_asm)
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 s0_ptrs_aligned split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 s0_ptrs_aligned split: split_if_asm)
|
||||||
apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD)
|
apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD)
|
||||||
apply (elim disjE, simp_all add: sameRegionAs_def isCap_simps)[1]
|
apply (elim disjE, simp_all add: sameRegionAs_def isCap_simps)[1]
|
||||||
|
@ -2443,11 +2445,11 @@ lemma sameRegionAs_s0H:
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_2 s0_ptrs_aligned split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_2 s0_ptrs_aligned split: split_if_asm)
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' s0_ptr_defs split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' s0_ptr_defs split: split_if_asm)
|
||||||
apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD)
|
apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD)
|
||||||
apply (elim disjE, simp_all add: sameRegionAs_def ArchRetype_H.sameRegionAs_def isCap_simps)[1]
|
apply (elim disjE, simp_all add: sameRegionAs_def ARM_H.sameRegionAs_def isCap_simps)[1]
|
||||||
apply (simp add: s0_ptr_defs)
|
apply (simp add: s0_ptr_defs)
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' s0_ptr_defs split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' s0_ptr_defs split: split_if_asm)
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 s0_ptrs_aligned split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 s0_ptrs_aligned split: split_if_asm)
|
||||||
apply (clarsimp simp: ArchRetype_H.sameRegionAs_def isCap_simps kh0H_all_obj_def' s0_ptr_defs split: split_if_asm)
|
apply (clarsimp simp: ARM_H.sameRegionAs_def isCap_simps kh0H_all_obj_def' s0_ptr_defs split: split_if_asm)
|
||||||
apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD)
|
apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD)
|
||||||
apply (elim disjE, simp_all add: sameRegionAs_def isCap_simps)[1]
|
apply (elim disjE, simp_all add: sameRegionAs_def isCap_simps)[1]
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' s0_ptr_defs split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' s0_ptr_defs split: split_if_asm)
|
||||||
|
@ -2492,7 +2494,7 @@ lemma sameRegionAs_s0H:
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_13E s0_ptrs_aligned split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_13E s0_ptrs_aligned split: split_if_asm)
|
||||||
apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD)
|
apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD)
|
||||||
apply (elim disjE, simp_all add: sameRegionAs_def ArchRetype_H.sameRegionAs_def isCap_simps)[1]
|
apply (elim disjE, simp_all add: sameRegionAs_def ARM_H.sameRegionAs_def isCap_simps)[1]
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 s0_ptrs_aligned split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 s0_ptrs_aligned split: split_if_asm)
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' s0_ptr_defs split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' s0_ptr_defs split: split_if_asm)
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps split: split_if_asm)
|
||||||
|
@ -2510,7 +2512,7 @@ lemma sameRegionAs_s0H:
|
||||||
apply (drule(2) ucast_shiftr_3)
|
apply (drule(2) ucast_shiftr_3)
|
||||||
apply (rule s0_ptrs_aligned)
|
apply (rule s0_ptrs_aligned)
|
||||||
apply simp
|
apply simp
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps s0_ptrs_aligned ArchRetype_H.sameRegionAs_def isCap_simps split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps s0_ptrs_aligned ARM_H.sameRegionAs_def isCap_simps split: split_if_asm)
|
||||||
apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD)
|
apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD)
|
||||||
apply (elim disjE, simp_all add: sameRegionAs_def isCap_simps)[1]
|
apply (elim disjE, simp_all add: sameRegionAs_def isCap_simps)[1]
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_2 s0_ptrs_aligned split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_2 s0_ptrs_aligned split: split_if_asm)
|
||||||
|
@ -2550,11 +2552,11 @@ lemma sameRegionAs_s0H:
|
||||||
apply simp
|
apply simp
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD)
|
apply (frule_tac x=p' in map_to_ctes_kh0H_SomeD)
|
||||||
apply (elim disjE, simp_all add: sameRegionAs_def ArchRetype_H.sameRegionAs_def isCap_simps)[1]
|
apply (elim disjE, simp_all add: sameRegionAs_def ARM_H.sameRegionAs_def isCap_simps)[1]
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 s0_ptrs_aligned split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 s0_ptrs_aligned split: split_if_asm)
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' s0_ptr_defs split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' s0_ptr_defs split: split_if_asm)
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 s0_ptrs_aligned split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 s0_ptrs_aligned split: split_if_asm)
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 s0_ptrs_aligned ArchRetype_H.sameRegionAs_def isCap_simps split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 s0_ptrs_aligned ARM_H.sameRegionAs_def isCap_simps split: split_if_asm)
|
||||||
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 s0_ptrs_aligned split: split_if_asm)
|
apply (clarsimp simp: kh0H_all_obj_def' cte_level_bits_def to_bl_use_of_bl the_nat_to_bl_simps ucast_shiftr_3 s0_ptrs_aligned split: split_if_asm)
|
||||||
apply (drule(2) ucast_shiftr_3)
|
apply (drule(2) ucast_shiftr_3)
|
||||||
apply (rule s0_ptrs_aligned)
|
apply (rule s0_ptrs_aligned)
|
||||||
|
@ -2752,6 +2754,8 @@ lemma s0H_valid_pspace':
|
||||||
apply ((clarsimp split: split_if_asm)+)[3]
|
apply ((clarsimp split: split_if_asm)+)[3]
|
||||||
done
|
done
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
(* Instantiate the current, abstract domain scheduler into the
|
(* Instantiate the current, abstract domain scheduler into the
|
||||||
concrete scheduler required for this example *)
|
concrete scheduler required for this example *)
|
||||||
axiomatization newKSDomSchedInst where
|
axiomatization newKSDomSchedInst where
|
||||||
|
@ -2764,6 +2768,8 @@ axiomatization kernel_data_refs_valid where
|
||||||
kdr_valid_global_refs': "valid_global_refs' s0H_internal" and
|
kdr_valid_global_refs': "valid_global_refs' s0H_internal" and
|
||||||
kdr_pspace_domain_valid: "pspace_domain_valid s0H_internal"
|
kdr_pspace_domain_valid: "pspace_domain_valid s0H_internal"
|
||||||
|
|
||||||
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
||||||
lemma s0H_invs:
|
lemma s0H_invs:
|
||||||
"invs' s0H_internal"
|
"invs' s0H_internal"
|
||||||
apply (clarsimp simp: invs'_def valid_state'_def s0H_valid_pspace')
|
apply (clarsimp simp: invs'_def valid_state'_def s0H_valid_pspace')
|
||||||
|
@ -3368,3 +3374,5 @@ lemma Sys1_valid_initial_state_noenabled:
|
||||||
by (rule Sys1_valid_initial_state_noenabled[OF step_restrict_s0 utf_det utf_non_empty utf_non_interrupt det_inv_invariant det_inv_s0])
|
by (rule Sys1_valid_initial_state_noenabled[OF step_restrict_s0 utf_det utf_non_empty utf_non_interrupt det_inv_invariant det_inv_s0])
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
||||||
|
end
|
||||||
|
|
|
@ -15,6 +15,8 @@ begin
|
||||||
(* FIXME: fp is currently ignored by ADT_C_if *)
|
(* FIXME: fp is currently ignored by ADT_C_if *)
|
||||||
consts fp :: bool
|
consts fp :: bool
|
||||||
|
|
||||||
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
||||||
lemma internal_R_ADT_A_if:
|
lemma internal_R_ADT_A_if:
|
||||||
"internal_R (ADT_A_if uop) R = R"
|
"internal_R (ADT_A_if uop) R = R"
|
||||||
apply (rule ext, rule ext)
|
apply (rule ext, rule ext)
|
||||||
|
@ -45,6 +47,8 @@ lemma LI_trans:
|
||||||
apply simp
|
apply simp
|
||||||
done
|
done
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
context kernel_m begin
|
context kernel_m begin
|
||||||
|
|
||||||
definition big_step_ADT_C_if where
|
definition big_step_ADT_C_if where
|
||||||
|
@ -65,6 +69,8 @@ lemma big_step_ADT_C_if_big_step_ADT_A_if_refines:
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
||||||
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
||||||
lemma LI_sub_big_steps':
|
lemma LI_sub_big_steps':
|
||||||
"\<lbrakk>(s',as) \<in> sub_big_steps C (internal_R C R) s;
|
"\<lbrakk>(s',as) \<in> sub_big_steps C (internal_R C R) s;
|
||||||
LI A C S (Ia \<times> Ic); A [> Ia; C [> Ic;
|
LI A C S (Ia \<times> Ic); A [> Ia; C [> Ic;
|
||||||
|
@ -186,6 +192,8 @@ lemma LI_rel_terminate:
|
||||||
apply simp
|
apply simp
|
||||||
done
|
done
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
locale valid_initial_state_C = valid_initial_state + kernel_m +
|
locale valid_initial_state_C = valid_initial_state + kernel_m +
|
||||||
assumes ADT_C_if_serial:
|
assumes ADT_C_if_serial:
|
||||||
"\<forall>s' a. (\<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if')
|
"\<forall>s' a. (\<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if')
|
||||||
|
|
|
@ -18,7 +18,14 @@ lemma wpc_helper_empty_fail:
|
||||||
|
|
||||||
wpc_setup "\<lambda>m. empty_fail m" wpc_helper_empty_fail
|
wpc_setup "\<lambda>m. empty_fail m" wpc_helper_empty_fail
|
||||||
|
|
||||||
crunch_ignore (empty_fail) (add: handleE' getCTE getObject updateObject)
|
crunch_ignore (empty_fail)
|
||||||
|
(add: handleE' getCTE getObject updateObject
|
||||||
|
CSpaceDecls_H.resolveAddressBits
|
||||||
|
doMachineOp
|
||||||
|
suspend restart
|
||||||
|
schedule)
|
||||||
|
|
||||||
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
||||||
lemmas forM_empty_fail[intro!, wp, simp] = empty_fail_mapM[simplified forM_def[symmetric]]
|
lemmas forM_empty_fail[intro!, wp, simp] = empty_fail_mapM[simplified forM_def[symmetric]]
|
||||||
lemmas forM_x_empty_fail[intro!, wp, simp] = empty_fail_mapM_x[simplified forM_x_def[symmetric]]
|
lemmas forM_x_empty_fail[intro!, wp, simp] = empty_fail_mapM_x[simplified forM_x_def[symmetric]]
|
||||||
|
@ -90,12 +97,10 @@ proof (induct arbitrary: s rule: resolveAddressBits.induct)
|
||||||
|
|
||||||
lemmas resolveAddressBits_empty_fail[intro!, wp, simp] =
|
lemmas resolveAddressBits_empty_fail[intro!, wp, simp] =
|
||||||
resolveAddressBits_spec_empty_fail[THEN use_spec_empty_fail]
|
resolveAddressBits_spec_empty_fail[THEN use_spec_empty_fail]
|
||||||
crunch_ignore (empty_fail) (add: CSpaceDecls_H.resolveAddressBits)
|
|
||||||
|
|
||||||
crunch (empty_fail) empty_fail[intro!, wp, simp]: lookupIPCBuffer
|
crunch (empty_fail) empty_fail[intro!, wp, simp]: lookupIPCBuffer
|
||||||
(simp:Let_def)
|
(simp:Let_def)
|
||||||
|
|
||||||
crunch_ignore (empty_fail) (add: doMachineOp)
|
|
||||||
declare ef_dmo'[intro!, wp, simp]
|
declare ef_dmo'[intro!, wp, simp]
|
||||||
|
|
||||||
lemma empty_fail_getObject_ep [intro!, wp, simp]:
|
lemma empty_fail_getObject_ep [intro!, wp, simp]:
|
||||||
|
@ -113,8 +118,8 @@ lemma constOnFailure_empty_fail[intro!, wp, simp]:
|
||||||
lemma ArchRetypeDecls_H_deriveCap_empty_fail[intro!, wp, simp]:
|
lemma ArchRetypeDecls_H_deriveCap_empty_fail[intro!, wp, simp]:
|
||||||
"isPageTableCap y \<or> isPageDirectoryCap y \<or> isPageCap y
|
"isPageTableCap y \<or> isPageDirectoryCap y \<or> isPageCap y
|
||||||
\<or> isASIDControlCap y \<or> isASIDPoolCap y
|
\<or> isASIDControlCap y \<or> isASIDPoolCap y
|
||||||
\<Longrightarrow> empty_fail (ArchRetypeDecls_H.deriveCap x y)"
|
\<Longrightarrow> empty_fail (Arch.deriveCap x y)"
|
||||||
apply (simp add: ArchRetype_H.deriveCap_def)
|
apply (simp add: ARM_H.deriveCap_def)
|
||||||
by auto
|
by auto
|
||||||
|
|
||||||
crunch (empty_fail) empty_fail[intro!, wp, simp]: ensureNoChildren
|
crunch (empty_fail) empty_fail[intro!, wp, simp]: ensureNoChildren
|
||||||
|
@ -181,8 +186,6 @@ lemma ThreadDecls_H_restart_empty_fail[intro!, wp, simp]:
|
||||||
"empty_fail (ThreadDecls_H.restart target)"
|
"empty_fail (ThreadDecls_H.restart target)"
|
||||||
by (simp add:restart_def)
|
by (simp add:restart_def)
|
||||||
|
|
||||||
crunch_ignore (empty_fail) (add: suspend restart)
|
|
||||||
|
|
||||||
crunch (empty_fail) empty_fail[intro!, wp, simp]: finaliseCap, preemptionPoint, capSwapForDelete
|
crunch (empty_fail) empty_fail[intro!, wp, simp]: finaliseCap, preemptionPoint, capSwapForDelete
|
||||||
(wp: empty_fail_catch simp: Let_def ignore: cacheRangeOp)
|
(wp: empty_fail_catch simp: Let_def ignore: cacheRangeOp)
|
||||||
|
|
||||||
|
@ -305,18 +308,12 @@ lemma ThreadDecls_H_schedule_empty_fail[intro!, wp, simp]:
|
||||||
apply (simp | wp | wpc)+
|
apply (simp | wp | wpc)+
|
||||||
done
|
done
|
||||||
|
|
||||||
crunch_ignore (empty_fail) (add: schedule)
|
|
||||||
|
|
||||||
|
|
||||||
lemma empty_fail_resetTimer[wp]: "empty_fail resetTimer"
|
lemma empty_fail_resetTimer[wp]: "empty_fail resetTimer"
|
||||||
by (simp add: resetTimer_def)
|
by (simp add: resetTimer_def)
|
||||||
|
|
||||||
crunch (empty_fail) empty_fail: callKernel
|
crunch (empty_fail) empty_fail: callKernel
|
||||||
(wp: empty_fail_catch simp: const_def Let_def ignore: cacheRangeOp)
|
(wp: empty_fail_catch simp: const_def Let_def ignore: cacheRangeOp)
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
lemma call_kernel_serial:
|
lemma call_kernel_serial:
|
||||||
" \<lbrakk> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and
|
" \<lbrakk> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and
|
||||||
(\<lambda>s. scheduler_action s = resume_cur_thread)) s;
|
(\<lambda>s. scheduler_action s = resume_cur_thread)) s;
|
||||||
|
@ -332,3 +329,5 @@ lemma call_kernel_serial:
|
||||||
done
|
done
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
||||||
|
end
|
||||||
|
|
Loading…
Reference in New Issue