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

arm-hyp (abstract/design/machine): add ARM_HYP directories

This commit is contained in:
Miki Tanaka 2016-07-07 14:37:02 +10:00 committed by Alejandro Gomez-Londono
parent f7e451b18a
commit 1f8127c6cc
14 changed files with 2910 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
lib/ARM_HYP/WordSetup.thy Normal file
View File

@ -0,0 +1,44 @@
(*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*)
theory WordSetup
imports
"../Distinct_Prop"
"../Word_Lib/Word_Lemmas_32"
begin
(* Distinct_Prop lemmas that need word lemmas: *)
lemma distinct_prop_enum:
"\<lbrakk> \<And>x y. \<lbrakk> x \<le> stop; y \<le> stop; x \<noteq> y \<rbrakk> \<Longrightarrow> P x y \<rbrakk>
\<Longrightarrow> distinct_prop P [0 :: 'a :: len word .e. stop]"
apply (simp add: upto_enum_def distinct_prop_map del: upt.simps)
apply (rule distinct_prop_distinct)
apply simp
apply (simp add: less_Suc_eq_le del: upt.simps)
apply (erule_tac x="of_nat x" in meta_allE)
apply (erule_tac x="of_nat y" in meta_allE)
apply (frule_tac y=x in unat_le)
apply (frule_tac y=y in unat_le)
apply (erule word_unat.Rep_cases)+
apply (simp add: toEnum_of_nat[OF unat_lt2p]
word_le_nat_alt)
done
lemma distinct_prop_enum_step:
"\<lbrakk> \<And>x y. \<lbrakk> x \<le> stop div step; y \<le> stop div step; x \<noteq> y \<rbrakk> \<Longrightarrow> P (x * step) (y * step) \<rbrakk>
\<Longrightarrow> distinct_prop P [0, step .e. stop]"
apply (simp add: upto_enum_step_def distinct_prop_map)
apply (rule distinct_prop_enum)
apply simp
done
end

67
spec/abstract/ARM_HYP/ArchCSpace_A.thy Normal file
View File

@ -0,0 +1,67 @@
(*
* 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 functions for the abstract model of CSpace.
*)
chapter "ArchCSpace"
theory ArchCSpace_A
imports
ArchVSpace_A
begin
context Arch begin global_naming ARM_A
text {* For some purposes capabilities to physical objects are treated
differently to others. *}
definition
arch_is_physical :: "arch_cap \<Rightarrow> bool" where
"arch_is_physical cap \<equiv> case cap of ASIDControlCap \<Rightarrow> False | _ \<Rightarrow> True"
text {* Check whether the second capability is to the same object or an object
contained in the region of the first one. *}
fun
arch_same_region_as :: "arch_cap \<Rightarrow> arch_cap \<Rightarrow> bool"
where
"arch_same_region_as (PageCap r R s x) (PageCap r' R' s' x') =
(let
topA = r + (1 << pageBitsForSize s) - 1;
topB = r' + (1 << pageBitsForSize s') - 1
in r \<le> r' \<and> topA \<ge> topB \<and> r' \<le> topB)"
| "arch_same_region_as (PageTableCap r x) (PageTableCap r' x') = (r' = r)"
| "arch_same_region_as (PageDirectoryCap r x) (PageDirectoryCap r' x') = (r' = r)"
| "arch_same_region_as ASIDControlCap ASIDControlCap = True"
| "arch_same_region_as (ASIDPoolCap r a) (ASIDPoolCap r' a') = (r' = r)"
| "arch_same_region_as _ _ = False"
text {* Check whether two arch capabilities are to the same object. *}
definition
same_aobject_as :: "arch_cap \<Rightarrow> arch_cap \<Rightarrow> bool" where
"same_aobject_as cp cp' \<equiv>
(case (cp, cp') of
(PageCap ref _ pgsz _,PageCap ref' _ pgsz' _)
\<Rightarrow> (ref, pgsz) = (ref', pgsz')
\<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1
| _ \<Rightarrow> arch_same_region_as cp cp')"
(* Proofs don't want to see this definition *)
declare same_aobject_as_def[simp]
text {* Only caps with sufficient rights can be recycled. *}
definition
arch_has_recycle_rights :: "arch_cap \<Rightarrow> bool" where
"arch_has_recycle_rights cap \<equiv> case cap of
PageCap _ R _ _ \<Rightarrow> {AllowRead,AllowWrite} \<subseteq> R
| _ \<Rightarrow> True"
end
end

283
spec/abstract/ARM_HYP/ArchDecode_A.thy Normal file
View File

@ -0,0 +1,283 @@
(*
* 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)
*)
(*
Decoding system calls
*)
chapter "Decoding Architecture-specific System Calls"
theory ArchDecode_A
imports
"../Interrupt_A"
"../InvocationLabels_A"
begin
context Arch begin global_naming ARM_A
section "Helper definitions"
text {* This definition ensures that the given pointer is aligned
to the given page size. *}
definition
check_vp_alignment :: "vmpage_size \<Rightarrow> word32 \<Rightarrow> (unit,'z::state_ext) se_monad" where
"check_vp_alignment sz vptr \<equiv>
unlessE (is_aligned vptr (pageBitsForSize sz)) $
throwError AlignmentError"
text {* This definition converts a user-supplied argument into an
invocation label, used to determine the method to invoke.
*}
definition
label_to_flush_type :: "invocation_label \<Rightarrow> flush_type"
where
"label_to_flush_type label \<equiv> case label of
ArchInvocationLabel ARMPDClean_Data \<Rightarrow> Clean
| ArchInvocationLabel ARMPageClean_Data \<Rightarrow> Clean
| ArchInvocationLabel ARMPDInvalidate_Data \<Rightarrow> Invalidate
| ArchInvocationLabel ARMPageInvalidate_Data \<Rightarrow> Invalidate
| ArchInvocationLabel ARMPDCleanInvalidate_Data \<Rightarrow> CleanInvalidate
| ArchInvocationLabel ARMPageCleanInvalidate_Data \<Rightarrow> CleanInvalidate
| ArchInvocationLabel ARMPDUnify_Instruction \<Rightarrow> Unify
| ArchInvocationLabel ARMPageUnify_Instruction \<Rightarrow> Unify"
section "Architecture calls"
text {* This definition decodes architecture-specific invocations.
*}
definition
page_base :: "vspace_ref \<Rightarrow> vmpage_size \<Rightarrow> vspace_ref"
where
"page_base vaddr vmsize \<equiv> vaddr && ~~ mask (pageBitsForSize vmsize)"
definition
arch_decode_invocation ::
"data \<Rightarrow> data list \<Rightarrow> cap_ref \<Rightarrow> cslot_ptr \<Rightarrow> arch_cap \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow>
(arch_invocation,'z::state_ext) se_monad"
where
"arch_decode_invocation label args x_slot cte cap extra_caps \<equiv> case cap of
PageDirectoryCap _ _ \<Rightarrow>
if isPDFlushLabel (invocation_type label) then
if length args > 1
then let start = args ! 0;
end = args ! 1
in doE
whenE (end \<le> start) $ throwError $ InvalidArgument 1;
whenE (start \<ge> kernel_base \<or> end > kernel_base) $ throwError IllegalOperation;
(pd,asid) \<leftarrow> (case cap of
PageDirectoryCap pd (Some asid) \<Rightarrow> returnOk (pd,asid)
| _ \<Rightarrow> throwError $ InvalidCapability 0);
pd' \<leftarrow> lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 0;
frame_info \<leftarrow> liftE $ resolve_vaddr pd start;
case frame_info of
None \<Rightarrow> returnOk $ InvokePageDirectory PageDirectoryNothing
| Some (frame_size, frame_base) \<Rightarrow>
let base_start = page_base start frame_size;
base_end = page_base (end - 1) frame_size;
offset = start && mask (pageBitsForSize frame_size);
pstart = frame_base + offset
in doE
whenE (base_start \<noteq> base_end) $ throwError $
RangeError start (base_start + mask (pageBitsForSize frame_size));
returnOk $ InvokePageDirectory $
PageDirectoryFlush (label_to_flush_type (invocation_type label))
start (end - 1) pstart pd asid
odE
odE
else throwError TruncatedMessage
else throwError IllegalOperation
| PageTableCap p mapped_address \<Rightarrow>
if invocation_type label = ArchInvocationLabel ARMPageTableMap then
if length args > 1 \<and> length extra_caps > 0
then let vaddr = args ! 0;
attr = args ! 1;
pd_cap = fst (extra_caps ! 0)
in doE
whenE (mapped_address \<noteq> None) $ throwError $ InvalidCapability 0;
(pd,asid) \<leftarrow> (case pd_cap of
ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow>
returnOk (pd,asid)
| _ \<Rightarrow> throwError $ InvalidCapability 1);
whenE (vaddr \<ge> kernel_base) $ throwError $ InvalidArgument 0;
pd' \<leftarrow> lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 1;
pd_index \<leftarrow> returnOk (shiftr vaddr 20);
vaddr' \<leftarrow> returnOk (vaddr && ~~ mask 20);
pd_slot \<leftarrow> returnOk (pd + (pd_index << 2));
oldpde \<leftarrow> liftE $ get_master_pde pd_slot;
unlessE (oldpde = InvalidPDE) $ throwError DeleteFirst;
pde \<leftarrow> returnOk (PageTablePDE (addrFromPPtr p)
(attribs_from_word attr \<inter> {ParityEnabled}) 0);
returnOk $ InvokePageTable $
PageTableMap
(ArchObjectCap $ PageTableCap p (Some (asid, vaddr')))
cte pde pd_slot
odE
else throwError TruncatedMessage
else if invocation_type label = ArchInvocationLabel ARMPageTableUnmap
then doE
final \<leftarrow> liftE $ is_final_cap (ArchObjectCap cap);
unlessE final $ throwError RevokeFirst;
returnOk $ InvokePageTable $ PageTableUnmap (ArchObjectCap cap) cte
odE
else throwError IllegalOperation
| PageCap p R pgsz mapped_address \<Rightarrow>
if invocation_type label = ArchInvocationLabel ARMPageMap then
if length args > 2 \<and> length extra_caps > 0
then let vaddr = args ! 0;
rights_mask = args ! 1;
attr = args ! 2;
pd_cap = fst (extra_caps ! 0)
in doE
whenE (mapped_address \<noteq> None) $ throwError $ InvalidCapability 0;
(pd,asid) \<leftarrow> (case pd_cap of
ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow>
returnOk (pd,asid)
| _ \<Rightarrow> throwError $ InvalidCapability 1);
pd' \<leftarrow> lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 1;
vtop \<leftarrow> returnOk (vaddr + (1 << (pageBitsForSize pgsz)) - 1);
whenE (vtop \<ge> kernel_base) $ throwError $ InvalidArgument 0;
vm_rights \<leftarrow> returnOk (mask_vm_rights R (data_to_rights rights_mask));
check_vp_alignment pgsz vaddr;
entries \<leftarrow> create_mapping_entries (addrFromPPtr p)
vaddr pgsz vm_rights
(attribs_from_word attr) pd;
ensure_safe_mapping entries;
returnOk $ InvokePage $ PageMap asid
(ArchObjectCap $ PageCap p R pgsz (Some (asid, vaddr)))
cte entries
odE
else throwError TruncatedMessage
else if invocation_type label = ArchInvocationLabel ARMPageRemap then
if length args > 1 \<and> length extra_caps > 0
then let rights_mask = args ! 0;
attr = args ! 1;
pd_cap = fst (extra_caps ! 0)
in doE
(pd,asid) \<leftarrow> (case pd_cap of
ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow>
returnOk (pd,asid)
| _ \<Rightarrow> throwError $ InvalidCapability 1);
(asid', vaddr) \<leftarrow> (case mapped_address of
Some a \<Rightarrow> returnOk a
| _ \<Rightarrow> throwError $ InvalidCapability 0);
pd' \<leftarrow> lookup_error_on_failure False $ find_pd_for_asid asid';
whenE (pd' \<noteq> pd \<or> asid' \<noteq> asid) $ throwError $ InvalidCapability 1;
vm_rights \<leftarrow> returnOk (mask_vm_rights R $ data_to_rights rights_mask);
check_vp_alignment pgsz vaddr;
entries \<leftarrow> create_mapping_entries (addrFromPPtr p)
vaddr pgsz vm_rights
(attribs_from_word attr) pd;
ensure_safe_mapping entries;
returnOk $ InvokePage $ PageRemap asid' entries
odE
else throwError TruncatedMessage
else if invocation_type label = ArchInvocationLabel ARMPageUnmap
then returnOk $ InvokePage $ PageUnmap cap cte
else if isPageFlushLabel (invocation_type label) then
if length args > 1
then let start = args ! 0;
end = args ! 1
in doE
(asid, vaddr) \<leftarrow> (case mapped_address of
Some a \<Rightarrow> returnOk a
| _ \<Rightarrow> throwError IllegalOperation);
pd \<leftarrow> lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (end \<le> start) $ throwError $ InvalidArgument 1;
page_size \<leftarrow> returnOk $ 1 << pageBitsForSize pgsz;
whenE (start \<ge> page_size \<or> end > page_size) $ throwError $ InvalidArgument 0;
returnOk $ InvokePage $ PageFlush
(label_to_flush_type (invocation_type label)) (start + vaddr)
(end + vaddr - 1) (addrFromPPtr p + start) pd asid
odE
else throwError TruncatedMessage
else if invocation_type label = ArchInvocationLabel ARMPageGetAddress
then returnOk $ InvokePage $ PageGetAddr p
else throwError IllegalOperation
| ASIDControlCap \<Rightarrow>
if invocation_type label = ArchInvocationLabel ARMASIDControlMakePool then
if length args > 1 \<and> length extra_caps > 1
then let index = args ! 0;
depth = args ! 1;
(untyped, parent_slot) = extra_caps ! 0;
root = fst (extra_caps ! 1)
in doE
asid_table \<leftarrow> liftE $ gets (arm_asid_table \<circ> arch_state);
free_set \<leftarrow> returnOk (- dom asid_table \<inter> {x. x \<le> 2 ^ asid_high_bits - 1});
whenE (free_set = {}) $ throwError DeleteFirst;
free \<leftarrow> liftE $ select_ext (\<lambda>_. free_asid_select asid_table) free_set;
base \<leftarrow> returnOk (ucast free << asid_low_bits);
(p,n) \<leftarrow> (case untyped of UntypedCap p n f \<Rightarrow> returnOk (p,n)
| _ \<Rightarrow> throwError $ InvalidCapability 1);
frame \<leftarrow> (if n = pageBits
then doE
ensure_no_children parent_slot;
returnOk p
odE
else throwError $ InvalidCapability 1);
dest_slot \<leftarrow> lookup_target_slot root (to_bl index) (unat depth);
ensure_empty dest_slot;
returnOk $ InvokeASIDControl $ MakePool frame dest_slot parent_slot base
odE
else throwError TruncatedMessage
else throwError IllegalOperation
| ASIDPoolCap p base \<Rightarrow>
if invocation_type label = ArchInvocationLabel ARMASIDPoolAssign then
if length extra_caps > 0
then
let (pd_cap, pd_cap_slot) = extra_caps ! 0
in case pd_cap of
ArchObjectCap (PageDirectoryCap _ None) \<Rightarrow> doE
asid_table \<leftarrow> liftE $ gets (arm_asid_table \<circ> arch_state);
pool_ptr \<leftarrow> returnOk (asid_table (asid_high_bits_of base));
whenE (pool_ptr = None) $ throwError $ FailedLookup False InvalidRoot;
whenE (p \<noteq> the pool_ptr) $ throwError $ InvalidCapability 0;
pool \<leftarrow> liftE $ get_asid_pool p;
free_set \<leftarrow> returnOk
(- dom pool \<inter> {x. x \<le> 2 ^ asid_low_bits - 1 \<and> ucast x + base \<noteq> 0});
whenE (free_set = {}) $ throwError DeleteFirst;
offset \<leftarrow> liftE $ select_ext (\<lambda>_. free_asid_pool_select pool base) free_set;
returnOk $ InvokeASIDPool $ Assign (ucast offset + base) p pd_cap_slot
odE
| _ \<Rightarrow> throwError $ InvalidCapability 1
else throwError TruncatedMessage
else throwError IllegalOperation"
text "ARM does not support additional interrupt control operations"
definition
arch_decode_irq_control_invocation ::
"data \<Rightarrow> data list \<Rightarrow> cslot_ptr \<Rightarrow> cap list \<Rightarrow> (arch_irq_control_invocation,'z::state_ext) se_monad" where
"arch_decode_irq_control_invocation label args slot excaps \<equiv> throwError IllegalOperation"
definition
arch_data_to_obj_type :: "nat \<Rightarrow> aobject_type option" where
"arch_data_to_obj_type n \<equiv>
if n = 0 then Some SmallPageObj
else if n = 1 then Some LargePageObj
else if n = 2 then Some SectionObj
else if n = 3 then Some SuperSectionObj
else if n = 4 then Some PageTableObj
else if n = 5 then Some PageDirectoryObj
else None"
end
end

103
spec/abstract/ARM_HYP/ArchInvocation_A.thy Normal file
View File

@ -0,0 +1,103 @@
(*
* 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 object invocations
*)
chapter "ARM Object Invocations"
theory ArchInvocation_A
imports "../Structures_A"
begin
context Arch begin global_naming ARM_A
text {* Message infos are encoded to or decoded from a data word. *}
primrec
message_info_to_data :: "message_info \<Rightarrow> data"
where
"message_info_to_data (MI ln exc unw mlabel) =
(let
extra = exc << 7;
unwrapped = unw << 9;
label = mlabel << 12
in
label || extra || unwrapped || ln)"
text {* Hard-coded to avoid recursive imports? *}
definition
data_to_message_info :: "data \<Rightarrow> message_info"
where
"data_to_message_info w \<equiv>
MI (let v = w && ((1 << 7) - 1) in if v > 120 then 120 else v) ((w >> 7) && ((1 << 2) - 1))
((w >> 9) && ((1 << 3) - 1)) (w >> 12)"
text {* These datatypes encode the arguments to the various possible
ARM-specific system calls. Selectors are defined for various fields
for convenience elsewhere. *}
datatype flush_type = Clean | Invalidate | CleanInvalidate | Unify
datatype page_directory_invocation =
PageDirectoryFlush (pd_flush_type: flush_type) (pd_flush_start: vspace_ref)
(pd_flush_end: vspace_ref) (pd_flush_pstart: word32)
(pd_flush_pd: obj_ref) (pd_flush_asid: asid)
| PageDirectoryNothing
datatype page_table_invocation =
PageTableMap cap cslot_ptr pde obj_ref
| PageTableUnmap cap cslot_ptr
datatype asid_control_invocation =
MakePool obj_ref cslot_ptr cslot_ptr asid
datatype asid_pool_invocation =
Assign asid obj_ref cslot_ptr
datatype page_invocation
= PageMap
(page_map_asid: asid)
(page_map_cap: cap)
(page_map_ct_slot: cslot_ptr)
(page_map_entries: "pte \<times> (obj_ref list) + pde \<times> (obj_ref list)")
| PageRemap
(page_remap_asid: asid)
(page_remap_entries: "pte \<times> (obj_ref list) + pde \<times> (obj_ref list)")
| PageUnmap
(page_unmap_cap: arch_cap)
(page_unmap_cap_slot: cslot_ptr)
| PageFlush
(page_flush_type: flush_type)
(page_flush_start: vspace_ref)
(page_flush_end: vspace_ref)
(page_flush_pstart: word32)
(page_flush_pd: obj_ref)
(page_flush_asid: asid)
| PageGetAddr
(page_get_paddr: obj_ref)
datatype arch_invocation
= InvokePageTable page_table_invocation
| InvokePageDirectory page_directory_invocation
| InvokePage page_invocation
| InvokeASIDControl asid_control_invocation
| InvokeASIDPool asid_pool_invocation
datatype arch_copy_register_sets =
ArchDefaultExtraRegisters
-- "There are no additional interrupt control operations on ARM."
typedecl arch_irq_control_invocation
end
end

66
spec/abstract/ARM_HYP/ArchRetype_A.thy Normal file
View File

@ -0,0 +1,66 @@
(*
* 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)
*)
(*
Retyping and untyped invocation
*)
chapter "Retyping and Untyped Invocations"
theory ArchRetype_A
imports
ArchVSpaceAcc_A
ArchInvocation_A
begin
context Arch begin global_naming ARM_A
text {* This is a placeholder function. We may wish to extend the specification
with explicitly tagging kernel data regions in memory. *}
definition
reserve_region :: "obj_ref \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (unit,'z::state_ext) s_monad" where
"reserve_region ptr byteLength is_kernel \<equiv> return ()"
text {* Create 4096-byte frame objects that can be mapped into memory. These must be
cleared to prevent past contents being revealed. *}
definition
create_word_objects :: "word32 \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (unit,'z::state_ext) s_monad" where
"create_word_objects ptr numObjects sz \<equiv>
do
byteLength \<leftarrow> return $ numObjects * 2 ^ sz;
reserve_region ptr byteLength True;
rst \<leftarrow> return (map (\<lambda> n. (ptr + (n << sz))) [0 .e. (of_nat numObjects) - 1]);
do_machine_op $ mapM_x (\<lambda>x. clearMemory x (2 ^ sz)) rst
od"
text {* Initialise architecture-specific objects. *}
definition
init_arch_objects :: "apiobject_type \<Rightarrow> obj_ref \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> obj_ref list \<Rightarrow> (unit,'z::state_ext) s_monad"
where
"init_arch_objects new_type ptr num_objects obj_sz refs \<equiv> case new_type of
ArchObject SmallPageObj \<Rightarrow> create_word_objects ptr num_objects 12
| ArchObject LargePageObj \<Rightarrow> create_word_objects ptr num_objects 16
| ArchObject SectionObj \<Rightarrow> create_word_objects ptr num_objects 20
| ArchObject SuperSectionObj \<Rightarrow> create_word_objects ptr num_objects 24
| ArchObject PageTableObj \<Rightarrow>
do_machine_op $ mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + ((1::word32) << pt_bits) - 1)
(addrFromPPtr x)) refs
| ArchObject PageDirectoryObj \<Rightarrow> do
mapM_x copy_global_mappings refs;
do_machine_op $ mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + ((1::word32) << pd_bits) - 1)
(addrFromPPtr x)) refs
od
| _ \<Rightarrow> return ()"
end
end

58
spec/abstract/ARM_HYP/ArchVMRights_A.thy Normal file
View File

@ -0,0 +1,58 @@
(*
* 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)
*)
chapter "ARM-Specific Virtual-Memory Rights"
theory ArchVMRights_A
imports "../CapRights_A" "../../machine/Setup_Locale"
begin
context Arch begin global_naming ARM_A
text {*
This theory provides architecture-specific definitions and datatypes
for virtual-memory support.
*}
section {* Architecture-specific virtual memory *}
text {* Page access rights. *}
type_synonym vm_rights = cap_rights
definition
vm_kernel_only :: vm_rights where
"vm_kernel_only \<equiv> {}"
definition
vm_read_only :: vm_rights where
"vm_read_only \<equiv> {AllowRead}"
definition
vm_read_write :: vm_rights where
"vm_read_write \<equiv> {AllowRead,AllowWrite}"
text {*
Note that only the above combinations of virtual-memory rights are permitted.
We introduce the following definitions to reflect this fact:
The predicate @{text valid_vm_rights} holds iff a given set of rights is valid
(i.e., a permitted combination).
The function @{text validate_vm_rights} takes an arbitrary set of rights and
returns the largest permitted subset.
*}
definition
"valid_vm_rights \<equiv> {vm_read_write, vm_read_only, vm_kernel_only}"
definition
"validate_vm_rights rs \<equiv>
(if AllowRead \<in> rs
then (if AllowWrite \<in> rs then vm_read_write else vm_read_only)
else vm_kernel_only)"
end
end

192
spec/abstract/ARM_HYP/ArchVSpaceAcc_A.thy Normal file
View File

@ -0,0 +1,192 @@
(*
* 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)
*)
(*
Accessor functions for architecture specific parts of the specification.
*)
chapter "Accessing the ARM VSpace"
theory ArchVSpaceAcc_A
imports "../KHeap_A"
begin
context Arch begin global_naming ARM_A
text {*
This part of the specification is fairly concrete as the machine architecture
is visible to the user in seL4 and therefore needs to be described.
The abstraction compared to the implementation is in the data types for
kernel objects. The interface which is rich in machine details remains the same.
*}
section "Encodings"
text {* The high bits of a virtual ASID. *}
definition
asid_high_bits_of :: "asid \<Rightarrow> word8" where
"asid_high_bits_of asid \<equiv> ucast (asid >> asid_low_bits)"
section "Kernel Heap Accessors"
text {* Manipulate ASID pools, page directories and page tables in the kernel
heap. *}
definition
get_asid_pool :: "obj_ref \<Rightarrow> (10 word \<rightharpoonup> obj_ref,'z::state_ext) s_monad" where
"get_asid_pool ptr \<equiv> do
kobj \<leftarrow> get_object ptr;
(case kobj of ArchObj (ASIDPool pool) \<Rightarrow> return pool
| _ \<Rightarrow> fail)
od"
definition
set_asid_pool :: "obj_ref \<Rightarrow> (10 word \<rightharpoonup> obj_ref) \<Rightarrow> (unit,'z::state_ext) s_monad" where
"set_asid_pool ptr pool \<equiv> do
v \<leftarrow> get_object ptr;
assert (case v of ArchObj (arch_kernel_obj.ASIDPool p) \<Rightarrow> True | _ \<Rightarrow> False);
set_object ptr (ArchObj (arch_kernel_obj.ASIDPool pool))
od"
definition
get_pd :: "obj_ref \<Rightarrow> (12 word \<Rightarrow> pde,'z::state_ext) s_monad" where
"get_pd ptr \<equiv> do
kobj \<leftarrow> get_object ptr;
(case kobj of ArchObj (PageDirectory pd) \<Rightarrow> return pd
| _ \<Rightarrow> fail)
od"
definition
set_pd :: "obj_ref \<Rightarrow> (12 word \<Rightarrow> pde) \<Rightarrow> (unit,'z::state_ext) s_monad" where
"set_pd ptr pd \<equiv> do
kobj \<leftarrow> get_object ptr;
assert (case kobj of ArchObj (PageDirectory pd) \<Rightarrow> True | _ \<Rightarrow> False);
set_object ptr (ArchObj (PageDirectory pd))
od"
text {* The following function takes a pointer to a PDE in kernel memory
and returns the actual PDE. *}
definition
get_pde :: "obj_ref \<Rightarrow> (pde,'z::state_ext) s_monad" where
"get_pde ptr \<equiv> do
base \<leftarrow> return (ptr && ~~mask pd_bits);
offset \<leftarrow> return ((ptr && mask pd_bits) >> 2);
pd \<leftarrow> get_pd base;
return $ pd (ucast offset)
od"
definition
store_pde :: "obj_ref \<Rightarrow> pde \<Rightarrow> (unit,'z::state_ext) s_monad" where
"store_pde p pde \<equiv> do
base \<leftarrow> return (p && ~~mask pd_bits);
offset \<leftarrow> return ((p && mask pd_bits) >> 2);
pd \<leftarrow> get_pd base;
pd' \<leftarrow> return $ pd (ucast offset := pde);
set_pd base pd'
od"
definition
get_pt :: "obj_ref \<Rightarrow> (word8 \<Rightarrow> pte,'z::state_ext) s_monad" where
"get_pt ptr \<equiv> do
kobj \<leftarrow> get_object ptr;
(case kobj of ArchObj (PageTable pt) \<Rightarrow> return pt
| _ \<Rightarrow> fail)
od"
definition
set_pt :: "obj_ref \<Rightarrow> (word8 \<Rightarrow> pte) \<Rightarrow> (unit,'z::state_ext) s_monad" where
"set_pt ptr pt \<equiv> do
kobj \<leftarrow> get_object ptr;
assert (case kobj of ArchObj (PageTable _) \<Rightarrow> True | _ \<Rightarrow> False);
set_object ptr (ArchObj (PageTable pt))
od"
text {* The following function takes a pointer to a PTE in kernel memory
and returns the actual PTE. *}
definition
get_pte :: "obj_ref \<Rightarrow> (pte,'z::state_ext) s_monad" where
"get_pte ptr \<equiv> do
base \<leftarrow> return (ptr && ~~mask pt_bits);
offset \<leftarrow> return ((ptr && mask pt_bits) >> 2);
pt \<leftarrow> get_pt base;
return $ pt (ucast offset)
od"
definition
store_pte :: "obj_ref \<Rightarrow> pte \<Rightarrow> (unit,'z::state_ext) s_monad" where
"store_pte p pte \<equiv> do
base \<leftarrow> return (p && ~~mask pt_bits);
offset \<leftarrow> return ((p && mask pt_bits) >> 2);
pt \<leftarrow> get_pt base;
pt' \<leftarrow> return $ pt (ucast offset := pte);
set_pt base pt'
od"
section "Basic Operations"
text {* The kernel window is mapped into every virtual address space from the
@{term kernel_base} pointer upwards. This function copies the mappings which
create the kernel window into a new page directory object. *}
definition
copy_global_mappings :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
"copy_global_mappings new_pd \<equiv> do
global_pd \<leftarrow> gets (arm_global_pd \<circ> arch_state);
pde_bits \<leftarrow> return 2;
pd_size \<leftarrow> return (1 << (pd_bits - pde_bits));
mapM_x (\<lambda>index. do
offset \<leftarrow> return (index << pde_bits);
pde \<leftarrow> get_pde (global_pd + offset);
store_pde (new_pd + offset) pde
od) [kernel_base >> 20 .e. pd_size - 1]
od"
text {* Walk the page directories and tables in software. *}
text {* The following function takes a page-directory reference as well as
a virtual address and then computes a pointer to the PDE in kernel memory *}
definition
lookup_pd_slot :: "word32 \<Rightarrow> vspace_ref \<Rightarrow> word32" where
"lookup_pd_slot pd vptr \<equiv>
let pd_index = vptr >> 20
in pd + (pd_index << 2)"
text {* The following function takes a page-directory reference as well as
a virtual address and then computes a pointer to the PTE in kernel memory.
Note that the function fails if the virtual address is mapped on a section or
super section. *}
definition
lookup_pt_slot :: "word32 \<Rightarrow> vspace_ref \<Rightarrow> (word32,'z::state_ext) lf_monad" where
"lookup_pt_slot pd vptr \<equiv> doE
pd_slot \<leftarrow> returnOk (lookup_pd_slot pd vptr);
pde \<leftarrow> liftE $ get_pde pd_slot;
(case pde of
PageTablePDE ptab _ _ \<Rightarrow> (doE
pt \<leftarrow> returnOk (ptrFromPAddr ptab);
pt_index \<leftarrow> returnOk ((vptr >> 12) && 0xff);
pt_slot \<leftarrow> returnOk (pt + (pt_index << 2));
returnOk pt_slot
odE)
| _ \<Rightarrow> throwError $ MissingCapability 20)
odE"
text {* A non-failing version of @{const lookup_pt_slot} when the pd is already known *}
definition
lookup_pt_slot_no_fail :: "word32 \<Rightarrow> vspace_ref \<Rightarrow> word32"
where
"lookup_pt_slot_no_fail pt vptr \<equiv>
let pt_index = ((vptr >> 12) && 0xff)
in pt + (pt_index << 2)"
end
end

755
spec/abstract/ARM_HYP/ArchVSpace_A.thy Normal file
View File

@ -0,0 +1,755 @@
(*
* 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)
*)
(*
Higher level functions for manipulating virtual address spaces
*)
chapter "ARM VSpace Functions"
theory ArchVSpace_A
imports "../Retype_A"
begin
context Arch begin global_naming ARM_A
text {* Save the set of entries that would be inserted into a page table or
page directory to map various different sizes of frame at a given virtual
address. *}
fun create_mapping_entries ::
"paddr \<Rightarrow> vspace_ref \<Rightarrow> vmpage_size \<Rightarrow> vm_rights \<Rightarrow> vm_attributes \<Rightarrow> word32 \<Rightarrow>
((pte * word32 list) + (pde * word32 list),'z::state_ext) se_monad"
where
"create_mapping_entries base vptr ARMSmallPage vm_rights attrib pd =
doE
p \<leftarrow> lookup_error_on_failure False $ lookup_pt_slot pd vptr;
returnOk $ Inl (SmallPagePTE base (attrib - {Global, ParityEnabled})
vm_rights, [p])
odE"
| "create_mapping_entries base vptr ARMLargePage vm_rights attrib pd =
doE
p \<leftarrow> lookup_error_on_failure False $ lookup_pt_slot pd vptr;
returnOk $ Inl (LargePagePTE base (attrib - {Global, ParityEnabled})
vm_rights, [p, p + 4 .e. p + 60])
odE"
| "create_mapping_entries base vptr ARMSection vm_rights attrib pd =
doE
p \<leftarrow> returnOk (lookup_pd_slot pd vptr);
returnOk $ Inr (SectionPDE base (attrib - {Global}) 0 vm_rights, [p])
odE"
| "create_mapping_entries base vptr ARMSuperSection vm_rights attrib pd =
doE
p \<leftarrow> returnOk (lookup_pd_slot pd vptr);
returnOk $ Inr (SuperSectionPDE base (attrib - {Global}) vm_rights, [p, p + 4 .e. p + 60])
odE"
definition get_master_pde :: "word32 \<Rightarrow> (pde,'z::state_ext)s_monad"
where "get_master_pde ptr \<equiv> do
pde \<leftarrow> (get_pde (ptr && ~~ mask 6));
(case pde of SuperSectionPDE _ _ _ \<Rightarrow> return pde
| _ \<Rightarrow> get_pde ptr)
od"
definition get_master_pte :: "word32 \<Rightarrow> (pte, 'z::state_ext)s_monad"
where "get_master_pte ptr \<equiv> do
pte \<leftarrow> (get_pte (ptr && ~~ mask 6));
(case pte of LargePagePTE _ _ _ \<Rightarrow> return pte
| _ \<Rightarrow> get_pte ptr)
od"
text {* Placing an entry which maps a frame within the set of entries that map a
larger frame is unsafe. This function checks that given entries replace either
invalid entries or entries of the same granularity. *}
fun ensure_safe_mapping ::
"(pte * word32 list) + (pde * word32 list) \<Rightarrow> (unit,'z::state_ext) se_monad"
where
"ensure_safe_mapping (Inl (InvalidPTE, _)) = returnOk ()"
|
"ensure_safe_mapping (Inl (SmallPagePTE _ _ _, pt_slots)) =
mapME_x (\<lambda>slot. (doE
pte \<leftarrow> liftE $ get_master_pte slot;
(case pte of
InvalidPTE \<Rightarrow> returnOk ()
| SmallPagePTE _ _ _ \<Rightarrow> returnOk ()
| _ \<Rightarrow> throwError DeleteFirst)
odE)) pt_slots"
|
"ensure_safe_mapping (Inl (LargePagePTE _ _ _, pt_slots)) =
mapME_x (\<lambda> slot. (doE
pte \<leftarrow> liftE $ get_master_pte slot;
(case pte of
InvalidPTE \<Rightarrow> returnOk ()
| LargePagePTE _ _ _ \<Rightarrow> returnOk ()
| _ \<Rightarrow> throwError DeleteFirst
)
odE)) pt_slots"
|
"ensure_safe_mapping (Inr (InvalidPDE, _)) = returnOk ()"
|
"ensure_safe_mapping (Inr (PageTablePDE _ _ _, _)) = fail"
|
"ensure_safe_mapping (Inr (SectionPDE _ _ _ _, pd_slots)) =
mapME_x (\<lambda> slot. (doE
pde \<leftarrow> liftE $ get_master_pde slot;
(case pde of
InvalidPDE \<Rightarrow> returnOk ()
| SectionPDE _ _ _ _ \<Rightarrow> returnOk ()
| _ \<Rightarrow> throwError DeleteFirst
)
odE)) pd_slots"
|
"ensure_safe_mapping (Inr (SuperSectionPDE _ _ _, pd_slots)) =
mapME_x (\<lambda> slot. (doE
pde \<leftarrow> liftE $ get_master_pde slot;
(case pde of
InvalidPDE \<Rightarrow> returnOk ()
| SuperSectionPDE _ _ _ \<Rightarrow> returnOk ()
| _ \<Rightarrow> throwError DeleteFirst
)
odE)) pd_slots"
text {* Look up a thread's IPC buffer and check that the thread has the right
authority to read or (in the receiver case) write to it. *}
definition
lookup_ipc_buffer :: "bool \<Rightarrow> word32 \<Rightarrow> (word32 option,'z::state_ext) s_monad" where
"lookup_ipc_buffer is_receiver thread \<equiv> do
buffer_ptr \<leftarrow> thread_get tcb_ipc_buffer thread;
buffer_frame_slot \<leftarrow> return (thread, tcb_cnode_index 4);
buffer_cap \<leftarrow> get_cap buffer_frame_slot;
(case buffer_cap of
ArchObjectCap (PageCap p R vms _) \<Rightarrow>
if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not>is_receiver
then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms))
else return None
| _ \<Rightarrow> return None)
od"
text {* Locate the page directory associated with a given virtual ASID. *}
definition
find_pd_for_asid :: "asid \<Rightarrow> (word32,'z::state_ext) lf_monad" where
"find_pd_for_asid asid \<equiv> doE
assertE (asid > 0);
asid_table \<leftarrow> liftE $ gets (arm_asid_table \<circ> arch_state);
pool_ptr \<leftarrow> returnOk (asid_table (asid_high_bits_of asid));
pool \<leftarrow> (case pool_ptr of
Some ptr \<Rightarrow> liftE $ get_asid_pool ptr
| None \<Rightarrow> throwError InvalidRoot);
pd \<leftarrow> returnOk (pool (ucast asid));
(case pd of
Some ptr \<Rightarrow> returnOk ptr
| None \<Rightarrow> throwError InvalidRoot)
odE"
text {* Locate the page directory and check that this process succeeds and
returns a pointer to a real page directory. *}
definition
find_pd_for_asid_assert :: "asid \<Rightarrow> (word32,'z::state_ext) s_monad" where
"find_pd_for_asid_assert asid \<equiv> do
pd \<leftarrow> find_pd_for_asid asid <catch> K fail;
get_pde pd;
return pd
od"
text {* Format a VM fault message to be passed to a thread's supervisor after
it encounters a page fault. *}
fun
handle_vm_fault :: "word32 \<Rightarrow> vmfault_type \<Rightarrow> (unit,'z::state_ext) f_monad"
where
"handle_vm_fault thread ARMDataAbort = doE
addr \<leftarrow> liftE $ do_machine_op getFAR;
fault \<leftarrow> liftE $ do_machine_op getDFSR;
throwError $ VMFault addr [0, fault && mask 14]
odE"
|
"handle_vm_fault thread ARMPrefetchAbort = doE
pc \<leftarrow> liftE $ as_user thread $ getRestartPC;
fault \<leftarrow> liftE $ do_machine_op getIFSR;
throwError $ VMFault pc [1, fault && mask 14]
odE"
text {* Load the optional hardware ASID currently associated with this virtual
ASID. *}
definition
load_hw_asid :: "asid \<Rightarrow> (hardware_asid option,'z::state_ext) s_monad" where
"load_hw_asid asid \<equiv> do
asid_map \<leftarrow> gets (arm_asid_map \<circ> arch_state);
return $ option_map fst $ asid_map asid
od"
text {* Associate a hardware ASID with a virtual ASID. *}
definition
store_hw_asid :: "asid \<Rightarrow> hardware_asid \<Rightarrow> (unit,'z::state_ext) s_monad" where
"store_hw_asid asid hw_asid \<equiv> do
pd \<leftarrow> find_pd_for_asid_assert asid;
asid_map \<leftarrow> gets (arm_asid_map \<circ> arch_state);
asid_map' \<leftarrow> return (asid_map (asid \<mapsto> (hw_asid, pd)));
modify (\<lambda>s. s \<lparr> arch_state := (arch_state s) \<lparr> arm_asid_map := asid_map' \<rparr>\<rparr>);
hw_asid_map \<leftarrow> gets (arm_hwasid_table \<circ> arch_state);
hw_asid_map' \<leftarrow> return (hw_asid_map (hw_asid \<mapsto> asid));
modify (\<lambda>s. s \<lparr> arch_state := (arch_state s) \<lparr> arm_hwasid_table := hw_asid_map' \<rparr>\<rparr>)
od"
text {* Clear all TLB mappings associated with this virtual ASID. *}
definition
invalidate_tlb_by_asid :: "asid \<Rightarrow> (unit,'z::state_ext) s_monad" where
"invalidate_tlb_by_asid asid \<equiv> do
maybe_hw_asid \<leftarrow> load_hw_asid asid;
(case maybe_hw_asid of
None \<Rightarrow> return ()
| Some hw_asid \<Rightarrow> do_machine_op $ invalidateTLB_ASID hw_asid)
od"
text {* Flush all cache and TLB entries associated with this virtual ASID. *}
definition
flush_space :: "asid \<Rightarrow> (unit,'z::state_ext) s_monad" where
"flush_space asid \<equiv> do
maybe_hw_asid \<leftarrow> load_hw_asid asid;
do_machine_op cleanCaches_PoU;
(case maybe_hw_asid of
None \<Rightarrow> return ()
| Some hw_asid \<Rightarrow> do_machine_op $ invalidateTLB_ASID hw_asid)
od"
text {* Remove any mapping from this virtual ASID to a hardware ASID. *}
definition
invalidate_asid :: "asid \<Rightarrow> (unit,'z::state_ext) s_monad" where
"invalidate_asid asid \<equiv> do
asid_map \<leftarrow> gets (arm_asid_map \<circ> arch_state);
asid_map' \<leftarrow> return (asid_map (asid:= None));
modify (\<lambda>s. s \<lparr> arch_state := (arch_state s) \<lparr> arm_asid_map := asid_map' \<rparr>\<rparr>)
od"
text {* Remove any mapping from this hardware ASID to a virtual ASID. *}
definition
invalidate_hw_asid_entry :: "hardware_asid \<Rightarrow> (unit,'z::state_ext) s_monad" where
"invalidate_hw_asid_entry hw_asid \<equiv> do
hw_asid_map \<leftarrow> gets (arm_hwasid_table \<circ> arch_state);
hw_asid_map' \<leftarrow> return (hw_asid_map (hw_asid:= None));
modify (\<lambda>s. s \<lparr> arch_state := (arch_state s) \<lparr> arm_hwasid_table := hw_asid_map' \<rparr>\<rparr>)
od"
text {* Remove virtual to physical mappings in either direction involving this
virtual ASID. *}
definition
invalidate_asid_entry :: "asid \<Rightarrow> (unit,'z::state_ext) s_monad" where
"invalidate_asid_entry asid \<equiv> do
maybe_hw_asid \<leftarrow> load_hw_asid asid;
when (maybe_hw_asid \<noteq> None) $ invalidate_hw_asid_entry (the maybe_hw_asid);
invalidate_asid asid
od"
text {* Locate a hardware ASID that is not in use, if necessary by reclaiming
one from another virtual ASID in a round-robin manner. *}
definition
find_free_hw_asid :: "(hardware_asid,'z::state_ext) s_monad" where
"find_free_hw_asid \<equiv> do
hw_asid_table \<leftarrow> gets (arm_hwasid_table \<circ> arch_state);
next_asid \<leftarrow> gets (arm_next_asid \<circ> arch_state);
maybe_asid \<leftarrow> return (find (\<lambda>a. hw_asid_table a = None)
(take (length [minBound :: hardware_asid .e. maxBound])
([next_asid .e. maxBound] @ [minBound .e. next_asid])));
(case maybe_asid of
Some hw_asid \<Rightarrow> return hw_asid
| None \<Rightarrow> do
invalidate_asid $ the $ hw_asid_table next_asid;
do_machine_op $ invalidateTLB_ASID next_asid;
invalidate_hw_asid_entry next_asid;
new_next_asid \<leftarrow> return (next_asid + 1);
modify (\<lambda>s. s \<lparr> arch_state := (arch_state s) \<lparr> arm_next_asid := new_next_asid \<rparr>\<rparr>);
return next_asid
od)
od"
text {* Get the hardware ASID associated with a virtual ASID, assigning one if
none is already assigned. *}
definition
get_hw_asid :: "asid \<Rightarrow> (hardware_asid,'z::state_ext) s_monad" where
"get_hw_asid asid \<equiv> do
maybe_hw_asid \<leftarrow> load_hw_asid asid;
(case maybe_hw_asid of
Some hw_asid \<Rightarrow> return hw_asid
| None \<Rightarrow> do
new_hw_asid \<leftarrow> find_free_hw_asid;
store_hw_asid asid new_hw_asid;
return new_hw_asid
od)
od"
abbreviation
"arm_context_switch_hwasid pd hwasid \<equiv> do
setCurrentPD $ addrFromPPtr pd;
setHardwareASID hwasid
od"
definition
arm_context_switch :: "word32 \<Rightarrow> asid \<Rightarrow> (unit, 'z::state_ext) s_monad"
where
"arm_context_switch pd asid \<equiv> do
hwasid \<leftarrow> get_hw_asid asid;
do_machine_op $ arm_context_switch_hwasid pd hwasid
od"
text {* Switch into the address space of a given thread or the global address
space if none is correctly configured. *}
definition
set_vm_root :: "word32 \<Rightarrow> (unit,'z::state_ext) s_monad" where
"set_vm_root tcb \<equiv> do
thread_root_slot \<leftarrow> return (tcb, tcb_cnode_index 1);
thread_root \<leftarrow> get_cap thread_root_slot;
(case thread_root of
ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> doE
pd' \<leftarrow> find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError InvalidRoot;
liftE $ arm_context_switch pd asid
odE
| _ \<Rightarrow> throwError InvalidRoot) <catch>
(\<lambda>_. do
global_pd \<leftarrow> gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromPPtr global_pd
od)
od"
text {* Before deleting an ASID pool object we must deactivate all page
directories that are installed in it. *}
definition
delete_asid_pool :: "asid \<Rightarrow> word32 \<Rightarrow> (unit,'z::state_ext) s_monad" where
"delete_asid_pool base ptr \<equiv> do
assert (base && mask asid_low_bits = 0);
asid_table \<leftarrow> gets (arm_asid_table \<circ> arch_state);
when (asid_table (asid_high_bits_of base) = Some ptr) $ do
pool \<leftarrow> get_asid_pool ptr;
mapM (\<lambda>offset. (when (pool (ucast offset) \<noteq> None) $ do
flush_space $ base + offset;
invalidate_asid_entry $ base + offset
od)) [0 .e. (1 << asid_low_bits) - 1];
asid_table' \<leftarrow> return (asid_table (asid_high_bits_of base:= None));
modify (\<lambda>s. s \<lparr> arch_state := (arch_state s) \<lparr> arm_asid_table := asid_table' \<rparr>\<rparr>);
tcb \<leftarrow> gets cur_thread;
set_vm_root tcb
od
od"
text {* When deleting a page directory from an ASID pool we must deactivate
it. *}
definition
delete_asid :: "asid \<Rightarrow> word32 \<Rightarrow> (unit,'z::state_ext) s_monad" where
"delete_asid asid pd \<equiv> do
asid_table \<leftarrow> gets (arm_asid_table \<circ> arch_state);
(case asid_table (asid_high_bits_of asid) of
None \<Rightarrow> return ()
| Some pool_ptr \<Rightarrow> do
pool \<leftarrow> get_asid_pool pool_ptr;
when (pool (ucast asid) = Some pd) $ do
flush_space asid;
invalidate_asid_entry asid;
pool' \<leftarrow> return (pool (ucast asid := None));
set_asid_pool pool_ptr pool';
tcb \<leftarrow> gets cur_thread;
set_vm_root tcb
od
od)
od"
text {* Switch to a particular address space in order to perform a flush
operation. *}
definition
set_vm_root_for_flush :: "word32 \<Rightarrow> asid \<Rightarrow> (bool,'z::state_ext) s_monad" where
"set_vm_root_for_flush pd asid \<equiv> do
tcb \<leftarrow> gets cur_thread;
thread_root_slot \<leftarrow> return (tcb, tcb_cnode_index 1);
thread_root \<leftarrow> get_cap thread_root_slot;
not_is_pd \<leftarrow> (case thread_root of
ArchObjectCap (PageDirectoryCap cur_pd (Some _)) \<Rightarrow> return (cur_pd \<noteq> pd)
| _ \<Rightarrow> return True);
(if not_is_pd then do
arm_context_switch pd asid;
return True
od
else return False)
od"
definition
do_flush :: "flush_type \<Rightarrow> vspace_ref \<Rightarrow> vspace_ref \<Rightarrow> paddr \<Rightarrow> unit machine_monad" where
"do_flush flush_type vstart vend pstart \<equiv>
case flush_type of
Clean \<Rightarrow> cleanCacheRange_RAM vstart vend pstart
| Invalidate \<Rightarrow> invalidateCacheRange_RAM vstart vend pstart
| CleanInvalidate \<Rightarrow> cleanInvalidateCacheRange_RAM vstart vend pstart
| Unify \<Rightarrow> do
cleanCacheRange_PoU vstart vend pstart;
dsb;
invalidateCacheRange_I vstart vend pstart;
branchFlushRange vstart vend pstart;
isb
od"
text {* Flush mappings associated with a page table. *}
definition
flush_table :: "word32 \<Rightarrow> asid \<Rightarrow> vspace_ref \<Rightarrow> word32 \<Rightarrow> (unit,'z::state_ext) s_monad" where
"flush_table pd asid vptr pt \<equiv> do
assert (vptr && mask (pageBitsForSize ARMSection) = 0);
root_switched \<leftarrow> set_vm_root_for_flush pd asid;
maybe_hw_asid \<leftarrow> load_hw_asid asid;
when (maybe_hw_asid \<noteq> None) $ do
hw_asid \<leftarrow> return (the maybe_hw_asid);
do_machine_op $ invalidateTLB_ASID hw_asid;
when root_switched $ do
tcb \<leftarrow> gets cur_thread;
set_vm_root tcb
od
od
od"
text {* Flush mappings associated with a given page. *}
definition
flush_page :: "vmpage_size \<Rightarrow> word32 \<Rightarrow> asid \<Rightarrow> vspace_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
"flush_page page_size pd asid vptr\<equiv> do
assert (vptr && mask pageBits = 0);
root_switched \<leftarrow> set_vm_root_for_flush pd asid;
maybe_hw_asid \<leftarrow> load_hw_asid asid;
when (maybe_hw_asid \<noteq> None) $ do
hw_asid \<leftarrow> return (the maybe_hw_asid);
do_machine_op $ invalidateTLB_VAASID (vptr || ucast hw_asid);
when root_switched $ do
tcb \<leftarrow> gets cur_thread;
set_vm_root tcb
od
od
od"
text {* Return the optional page directory a page table is mapped in. *}
definition
page_table_mapped :: "asid \<Rightarrow> vspace_ref \<Rightarrow> obj_ref \<Rightarrow> (obj_ref option,'z::state_ext) s_monad" where
"page_table_mapped asid vaddr pt \<equiv> doE
pd \<leftarrow> find_pd_for_asid asid;
pd_slot \<leftarrow> returnOk $ lookup_pd_slot pd vaddr;
pde \<leftarrow> liftE $ get_pde pd_slot;
case pde of
PageTablePDE addr _ _ \<Rightarrow> returnOk $
if addrFromPPtr pt = addr then Some pd else None
| _ \<Rightarrow> returnOk None
odE <catch> (K $ return None)"
text {* Unmap a page table from its page directory. *}
definition
unmap_page_table :: "asid \<Rightarrow> vspace_ref \<Rightarrow> word32 \<Rightarrow> (unit,'z::state_ext) s_monad" where
"unmap_page_table asid vaddr pt \<equiv> do
pdOpt \<leftarrow> page_table_mapped asid vaddr pt;
case pdOpt of
None \<Rightarrow> return ()
| Some pd \<Rightarrow> do
pd_slot \<leftarrow> return $ lookup_pd_slot pd vaddr;
store_pde pd_slot InvalidPDE;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot);
flush_table pd asid vaddr pt
od
od"
text {* Check that a given frame is mapped by a given mapping entry. *}
definition
check_mapping_pptr :: "obj_ref \<Rightarrow> vmpage_size \<Rightarrow> (obj_ref + obj_ref) \<Rightarrow> (bool,'z::state_ext) s_monad" where
"check_mapping_pptr pptr pgsz tablePtr \<equiv> case tablePtr of
Inl ptePtr \<Rightarrow> do
pte \<leftarrow> get_pte ptePtr;
return $ case pte of
SmallPagePTE x _ _ \<Rightarrow> x = addrFromPPtr pptr \<and> pgsz = ARMSmallPage
| LargePagePTE x _ _ \<Rightarrow> x = addrFromPPtr pptr \<and> pgsz = ARMLargePage
| _ \<Rightarrow> False
od
| Inr pdePtr \<Rightarrow> do
pde \<leftarrow> get_pde pdePtr;
return $ case pde of
SectionPDE x _ _ _ \<Rightarrow> x = addrFromPPtr pptr \<and> pgsz = ARMSection
| SuperSectionPDE x _ _ \<Rightarrow> x = addrFromPPtr pptr \<and> pgsz = ARMSuperSection
| _ \<Rightarrow> False
od"
definition
"last_byte_pte x \<equiv> let pte_bits = 2 in x + ((1 << pte_bits) - 1)"
definition
"last_byte_pde x \<equiv> let pde_bits = 2 in x + ((1 << pde_bits) - 1)"
text {* Unmap a mapped page if the given mapping details are still current. *}
definition
unmap_page :: "vmpage_size \<Rightarrow> asid \<Rightarrow> vspace_ref \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
"unmap_page pgsz asid vptr pptr \<equiv> doE
pd \<leftarrow> find_pd_for_asid asid;
(case pgsz of
ARMSmallPage \<Rightarrow> doE
p \<leftarrow> lookup_pt_slot pd vptr;
throw_on_false undefined $
check_mapping_pptr pptr pgsz (Inl p);
liftE $ do
store_pte p InvalidPTE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE
| ARMLargePage \<Rightarrow> doE
p \<leftarrow> lookup_pt_slot pd vptr;
throw_on_false undefined $
check_mapping_pptr pptr pgsz (Inl p);
liftE $ do
assert $ p && mask 6 = 0;
slots \<leftarrow> return (map (\<lambda>x. x + p) [0, 4 .e. 60]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pte (last slots))
(addrFromPPtr (hd slots))
od
odE
| ARMSection \<Rightarrow> doE
p \<leftarrow> returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $
check_mapping_pptr pptr pgsz (Inr p);
liftE $ do
store_pde p InvalidPDE;
do_machine_op $ cleanByVA_PoU p (addrFromPPtr p)
od
odE
| ARMSuperSection \<Rightarrow> doE
p \<leftarrow> returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined $
check_mapping_pptr pptr pgsz (Inr p);
liftE $ do
assert $ p && mask 6 = 0;
slots \<leftarrow> return (map (\<lambda>x. x + p) [0, 4 .e. 60]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pde (last slots))
(addrFromPPtr (hd slots))
od
odE);
liftE $ flush_page pgsz pd asid vptr
odE <catch> (K $ return ())"
text {* PageDirectory and PageTable capabilities cannot be copied until they
have a virtual ASID and location assigned. This is because page directories
cannot have multiple current virtual ASIDs and page tables cannot be shared
between address spaces or virtual locations. *}
definition
arch_derive_cap :: "arch_cap \<Rightarrow> (arch_cap,'z::state_ext) se_monad"
where
"arch_derive_cap c \<equiv> case c of
PageTableCap _ (Some x) \<Rightarrow> returnOk c
| PageTableCap _ None \<Rightarrow> throwError IllegalOperation
| PageDirectoryCap _ (Some x) \<Rightarrow> returnOk c
| PageDirectoryCap _ None \<Rightarrow> throwError IllegalOperation
| PageCap r R pgs x \<Rightarrow> returnOk (PageCap r R pgs None)
| ASIDControlCap \<Rightarrow> returnOk c
| ASIDPoolCap _ _ \<Rightarrow> returnOk c"
text {* No user-modifiable data is stored in ARM-specific capabilities. *}
definition
arch_update_cap_data :: "data \<Rightarrow> arch_cap \<Rightarrow> cap"
where
"arch_update_cap_data data c \<equiv> ArchObjectCap c"
text {* Actions that must be taken on finalisation of ARM-specific
capabilities. *}
definition
arch_finalise_cap :: "arch_cap \<Rightarrow> bool \<Rightarrow> (cap,'z::state_ext) s_monad"
where
"arch_finalise_cap c x \<equiv> case (c, x) of
(ASIDPoolCap ptr b, True) \<Rightarrow> do
delete_asid_pool b ptr;
return NullCap
od
| (PageDirectoryCap ptr (Some a), True) \<Rightarrow> do
delete_asid a ptr;
return NullCap
od
| (PageTableCap ptr (Some (a, v)), True) \<Rightarrow> do
unmap_page_table a v ptr;
return NullCap
od
| (PageCap ptr _ s (Some (a, v)), _) \<Rightarrow> do
unmap_page s a v ptr;
return NullCap
od
| _ \<Rightarrow> return NullCap"
text {* Remove record of mappings to a page cap, page table cap or page directory cap *}
fun
arch_reset_mem_mapping :: "arch_cap \<Rightarrow> arch_cap"
where
"arch_reset_mem_mapping (PageCap p rts sz mp) = PageCap p rts sz None"
| "arch_reset_mem_mapping (PageTableCap ptr mp) = PageTableCap ptr None"
| "arch_reset_mem_mapping (PageDirectoryCap ptr ma) = PageDirectoryCap ptr None"
| "arch_reset_mem_mapping cap = cap"
text {* Actions that must be taken to recycle ARM-specific capabilities. *}
definition
arch_recycle_cap :: "bool \<Rightarrow> arch_cap \<Rightarrow> (arch_cap,'z::state_ext) s_monad"
where
"arch_recycle_cap is_final cap \<equiv> case cap of
PageCap p _ sz _ \<Rightarrow> do
do_machine_op $ clearMemory p (2 ^ (pageBitsForSize sz));
arch_finalise_cap cap is_final;
return $ arch_reset_mem_mapping cap
od
| PageTableCap ptr mp \<Rightarrow> do
pte_bits \<leftarrow> return 2;
slots \<leftarrow> return [ptr, ptr + (1 << pte_bits) .e. ptr + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU ptr (ptr + (1 << pt_bits) - 1)
(addrFromPPtr ptr);
case mp of None \<Rightarrow> return ()
| Some (a, v) \<Rightarrow> do
pdOpt \<leftarrow> page_table_mapped a v ptr;
when (pdOpt \<noteq> None) $ invalidate_tlb_by_asid a
od;
arch_finalise_cap cap is_final;
return (if is_final then arch_reset_mem_mapping cap else cap)
od
| PageDirectoryCap ptr ma \<Rightarrow> do
pde_bits \<leftarrow> return 2;
indices \<leftarrow> return [0 .e. (kernel_base >> pageBitsForSize ARMSection) - 1];
offsets \<leftarrow> return (map (swp (op <<) pde_bits) indices);
slots \<leftarrow> return (map (\<lambda>x. x + ptr) offsets);
mapM_x (swp store_pde InvalidPDE) slots;
do_machine_op $ cleanCacheRange_PoU ptr (ptr + (1 << pd_bits) - 1)
(addrFromPPtr ptr);
case ma of None \<Rightarrow> return ()
| Some a \<Rightarrow> doE
pd' \<leftarrow> find_pd_for_asid a;
liftE $ when (pd' = ptr) $ invalidate_tlb_by_asid a
odE <catch> K (return ());
arch_finalise_cap cap is_final;
return (if is_final then arch_reset_mem_mapping cap else cap)
od
| ASIDControlCap \<Rightarrow> return ASIDControlCap
| ASIDPoolCap ptr base \<Rightarrow> do
asid_table \<leftarrow> gets (arm_asid_table \<circ> arch_state);
when (asid_table (asid_high_bits_of base) = Some ptr) $ do
delete_asid_pool base ptr;
set_asid_pool ptr empty;
asid_table \<leftarrow> gets (arm_asid_table \<circ> arch_state);
asid_table' \<leftarrow> return (asid_table (asid_high_bits_of base \<mapsto> ptr));
modify (\<lambda>s. s \<lparr> arch_state := (arch_state s) \<lparr> arm_asid_table := asid_table' \<rparr>\<rparr>)
od;
return cap
od"
text {* A thread's virtual address space capability must be to a page directory
to be valid on the ARM architecture. *}
definition
is_valid_vtable_root :: "cap \<Rightarrow> bool" where
"is_valid_vtable_root c \<equiv> \<exists>r a. c = ArchObjectCap (PageDirectoryCap r (Some a))"
text {* A thread's IPC buffer capability must be to a page that is capable of
containing the IPC buffer without the end of the buffer spilling into another
page. *}
definition
cap_transfer_data_size :: nat where
"cap_transfer_data_size \<equiv> 3"
definition
msg_max_length :: nat where
"msg_max_length \<equiv> 120"
definition
msg_max_extra_caps :: nat where
"msg_max_extra_caps \<equiv> 3"
definition
msg_align_bits :: nat
where
"msg_align_bits \<equiv> 2 + (LEAST n. (cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2) \<le> 2 ^ n)"
lemma msg_align_bits:
"msg_align_bits = 9"
proof -
have "(LEAST n. (cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2) \<le> 2 ^ n) = 7"
proof (rule Least_equality)
show "(cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2) \<le> 2 ^ 7"
by (simp add: cap_transfer_data_size_def msg_max_length_def msg_max_extra_caps_def)
next
fix y
assume "(cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2) \<le> 2 ^ y"
hence "(2 :: nat) ^ 7 \<le> 2 ^ y"
by (simp add: cap_transfer_data_size_def msg_max_length_def msg_max_extra_caps_def)
thus "7 \<le> y"
by (rule power_le_imp_le_exp [rotated], simp)
qed
thus ?thesis unfolding msg_align_bits_def by simp
qed
definition
check_valid_ipc_buffer :: "vspace_ref \<Rightarrow> cap \<Rightarrow> (unit,'z::state_ext) se_monad" where
"check_valid_ipc_buffer vptr c \<equiv> case c of
(ArchObjectCap (PageCap _ _ magnitude _)) \<Rightarrow> doE
whenE (\<not> is_aligned vptr msg_align_bits) $ throwError AlignmentError;
returnOk ()
odE
| _ \<Rightarrow> throwError IllegalOperation"
text {* On the abstract level, capability and VM rights share the same type.
Nevertheless, a simple set intersection might lead to an invalid value like
@{term "{AllowWrite}"}. Hence, @{const validate_vm_rights}. *}
definition
mask_vm_rights :: "vm_rights \<Rightarrow> cap_rights \<Rightarrow> vm_rights" where
"mask_vm_rights V R \<equiv> validate_vm_rights (V \<inter> R)"
text {* Decode a user argument word describing the kind of VM attributes a
mapping is to have. *}
definition
attribs_from_word :: "word32 \<Rightarrow> vm_attributes" where
"attribs_from_word w \<equiv>
let V = (if w !!0 then {PageCacheable} else {});
V' = (if w!!1 then insert ParityEnabled V else V)
in if w!!2 then insert XNever V' else V'"
text {* Update the mapping data saved in a page or page table capability. *}
definition
update_map_data :: "arch_cap \<Rightarrow> (word32 \<times> word32) option \<Rightarrow> arch_cap" where
"update_map_data cap m \<equiv> case cap of PageCap p R sz _ \<Rightarrow> PageCap p R sz m
| PageTableCap p _ \<Rightarrow> PageTableCap p m"
text {* Get information about the frame of a given virtual address *}
definition
resolve_vaddr :: "word32 \<Rightarrow> vspace_ref \<Rightarrow> ((vmpage_size \<times> obj_ref) option, 'z::state_ext) s_monad"
where
"resolve_vaddr pd vaddr \<equiv> do
pd_slot \<leftarrow> return $ lookup_pd_slot pd vaddr;
pde \<leftarrow> get_master_pde pd_slot;
case pde of
SectionPDE f _ _ _ \<Rightarrow> return $ Some (ARMSection, f)
| SuperSectionPDE f _ _ \<Rightarrow> return $ Some (ARMSuperSection, f)
| PageTablePDE t _ _ \<Rightarrow> (do
pt \<leftarrow> return $ ptrFromPAddr t;
pte_slot \<leftarrow> return $ lookup_pt_slot_no_fail pt vaddr;
pte \<leftarrow> get_master_pte pte_slot;
case pte of
LargePagePTE f _ _ \<Rightarrow> return $ Some (ARMLargePage, f)
| SmallPagePTE f _ _ \<Rightarrow> return $ Some (ARMSmallPage, f)
| _ \<Rightarrow> return None
od)
| _ \<Rightarrow> return None
od"
text {*
A pointer is inside a user frame if its top bits point to a @{text DataPage}.
*}
definition
in_user_frame :: "word32 \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" where
"in_user_frame p s \<equiv>
\<exists>sz. kheap s (p && ~~ mask (pageBitsForSize sz)) =
Some (ArchObj (DataPage sz))"
end
end

233
spec/abstract/ARM_HYP/Arch_A.thy Normal file
View File

@ -0,0 +1,233 @@
(*
* 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)
*)
(*
Entry point for architecture dependent definitions.
*)
chapter "Toplevel ARM Definitions"
theory Arch_A
imports "../TcbAcc_A"
begin
context Arch begin global_naming ARM_A
definition "page_bits \<equiv> pageBits"
text {* The ARM architecture does not provide any additional operations on its
interrupt controller. *}
definition
arch_invoke_irq_control :: "arch_irq_control_invocation \<Rightarrow> (unit,'z::state_ext) p_monad" where
"arch_invoke_irq_control aic \<equiv> fail"
text {* Switch to a thread's virtual address space context and write its IPC
buffer pointer into the globals frame. Clear the load-exclusive monitor. *}
definition
arch_switch_to_thread :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
"arch_switch_to_thread t \<equiv> do
set_vm_root t;
globals \<leftarrow> gets (arm_globals_frame \<circ> arch_state);
buffer_ptr \<leftarrow> thread_get tcb_ipc_buffer t;
do_machine_op $ storeWord globals buffer_ptr;
do_machine_op $ clearExMonitor
od"
text {* The idle thread does not need to be handled specially on ARM. *}
(* Clear the globals frame when switching to the idle thread. This is
specificially to ease infoflow reasoning VER-207 *)
definition
arch_switch_to_idle_thread :: "(unit,'z::state_ext) s_monad" where
"arch_switch_to_idle_thread \<equiv> do
globals \<leftarrow> gets (arm_globals_frame \<circ> arch_state);
do_machine_op $ storeWord globals 0
od"
definition
arch_activate_idle_thread :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
"arch_activate_idle_thread t \<equiv> return ()"
text {* The ASIDControl capability confers the authority to create a new ASID
pool object. This operation creates the new ASID pool, provides a capability
to it and connects it to the global virtual ASID table. *}
definition
perform_asid_control_invocation :: "asid_control_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where
"perform_asid_control_invocation iv \<equiv> case iv of
MakePool frame slot parent base \<Rightarrow> do
delete_objects frame page_bits;
pcap \<leftarrow> get_cap parent;
set_cap (max_free_index_update pcap) parent;
retype_region frame 1 0 (ArchObject ASIDPoolObj);
cap_insert (ArchObjectCap $ ASIDPoolCap frame base) parent slot;
assert (base && mask asid_low_bits = 0);
asid_table \<leftarrow> gets (arm_asid_table \<circ> arch_state);
asid_table' \<leftarrow> return (asid_table (asid_high_bits_of base \<mapsto> frame));
modify (\<lambda>s. s \<lparr>arch_state := (arch_state s) \<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od"
text {* The ASIDPool capability confers the authority to assign a virtual ASID
to a page directory. *}
definition
perform_asid_pool_invocation :: "asid_pool_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where
"perform_asid_pool_invocation iv \<equiv> case iv of Assign asid pool_ptr ct_slot \<Rightarrow>
do
pd_cap \<leftarrow> get_cap ct_slot;
case pd_cap of
ArchObjectCap (PageDirectoryCap pd_base _) \<Rightarrow> do
pool \<leftarrow> get_asid_pool pool_ptr;
pool' \<leftarrow> return (pool (ucast asid \<mapsto> pd_base));
set_cap (ArchObjectCap $ PageDirectoryCap pd_base (Some asid)) ct_slot;
set_asid_pool pool_ptr pool'
od
| _ \<Rightarrow> fail
od"
text {* The PageDirectory capability confers the authority to flush cache entries
associated with that PD *}
definition
perform_page_directory_invocation :: "page_directory_invocation \<Rightarrow> (unit,'z::state_ext) s_monad"
where
"perform_page_directory_invocation iv \<equiv> case iv of
PageDirectoryFlush typ start end pstart pd asid \<Rightarrow>
when (start < end) $ do
root_switched \<leftarrow> set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ do
tcb \<leftarrow> gets cur_thread;
set_vm_root tcb
od
od
| PageDirectoryNothing \<Rightarrow> return ()"
definition
pte_check_if_mapped :: "32 word \<Rightarrow> (bool, 'z::state_ext) s_monad"
where
"pte_check_if_mapped slot \<equiv> do
pt \<leftarrow> get_master_pte slot;
return (pt \<noteq> InvalidPTE)
od"
definition
pde_check_if_mapped :: "32 word \<Rightarrow> (bool, 'z::state_ext) s_monad"
where
"pde_check_if_mapped slot \<equiv> do
pd \<leftarrow> get_master_pde slot;
return (pd \<noteq> InvalidPDE)
od"
text {* The Page capability confers the authority to map, unmap and flush the
memory page. The remap system call is a convenience operation that ensures the
page is mapped in the same location as this cap was previously used to map it
in. *}
definition
perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where
"perform_page_invocation iv \<equiv> case iv of
PageMap asid cap ct_slot entries \<Rightarrow> do
set_cap cap ct_slot;
case entries of
Inl (pte, slots) \<Rightarrow> do
flush \<leftarrow> pte_check_if_mapped (hd slots);
store_pte (hd slots) pte;
mapM (swp store_pte InvalidPTE) (tl slots);
do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pte (last slots))
(addrFromPPtr (hd slots));
if flush then (invalidate_tlb_by_asid asid) else return ()
od
| Inr (pde, slots) \<Rightarrow> do
flush \<leftarrow> pde_check_if_mapped (hd slots);
store_pde (hd slots) pde;
mapM (swp store_pde InvalidPDE) (tl slots);
do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pde (last slots))
(addrFromPPtr (hd slots));
if flush then (invalidate_tlb_by_asid asid) else return ()
od
od
| PageRemap asid (Inl (pte, slots)) \<Rightarrow> do
flush \<leftarrow> pte_check_if_mapped (hd slots);
store_pte (hd slots) pte;
mapM_x (swp store_pte InvalidPTE) (tl slots);
do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pte (last slots))
(addrFromPPtr (hd slots));
if flush then (invalidate_tlb_by_asid asid) else return ()
od
| PageRemap asid (Inr (pde, slots)) \<Rightarrow> do
flush \<leftarrow> pde_check_if_mapped (hd slots);
store_pde (hd slots) pde;
mapM_x (swp store_pde InvalidPDE) (tl slots);
do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pde (last slots))
(addrFromPPtr (hd slots));
if flush then (invalidate_tlb_by_asid asid) else return ()
od
| PageUnmap cap ct_slot \<Rightarrow>
(case cap of
PageCap p R vp_size vp_mapped_addr \<Rightarrow> do
case vp_mapped_addr of
Some (asid, vaddr) \<Rightarrow> unmap_page vp_size asid vaddr p
| None \<Rightarrow> return ();
cap \<leftarrow> liftM the_arch_cap $ get_cap ct_slot;
set_cap (ArchObjectCap $ update_map_data cap None) ct_slot
od
| _ \<Rightarrow> fail)
| PageFlush typ start end pstart pd asid \<Rightarrow>
when (start < end) $ do
root_switched \<leftarrow> set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ do
tcb \<leftarrow> gets cur_thread;
set_vm_root tcb
od
od
| PageGetAddr ptr \<Rightarrow> do
ct \<leftarrow> gets cur_thread;
n_msg \<leftarrow> set_mrs ct None [addrFromPPtr ptr];
set_message_info ct $ MI n_msg 0 0 0
od"
text {* PageTable capabilities confer the authority to map and unmap page
tables. *}
definition
perform_page_table_invocation :: "page_table_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where
"perform_page_table_invocation iv \<equiv>
case iv of PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do
set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od
| PageTableUnmap (ArchObjectCap (PageTableCap p mapped_address)) ct_slot \<Rightarrow> do
case mapped_address of Some (asid, vaddr) \<Rightarrow> do
unmap_page_table asid vaddr p;
pte_bits \<leftarrow> return 2;
slots \<leftarrow> return [p, p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1)
(addrFromPPtr p)
od | None \<Rightarrow> return ();
cap \<leftarrow> liftM the_arch_cap $ get_cap ct_slot;
set_cap (ArchObjectCap $ update_map_data cap None) ct_slot
od
| _ \<Rightarrow> fail"
text {* Top level system call despatcher for all ARM-specific system calls. *}
definition
arch_perform_invocation :: "arch_invocation \<Rightarrow> (data list,'z::state_ext) p_monad" where
"arch_perform_invocation i \<equiv> liftE $ do
case i of
InvokePageTable oper \<Rightarrow> perform_page_table_invocation oper
| InvokePageDirectory oper \<Rightarrow> perform_page_directory_invocation oper
| InvokePage oper \<Rightarrow> perform_page_invocation oper
| InvokeASIDControl oper \<Rightarrow> perform_asid_control_invocation oper
| InvokeASIDPool oper \<Rightarrow> perform_asid_pool_invocation oper;
return $ []
od"
end
end

246
spec/abstract/ARM_HYP/Arch_Structs_A.thy Normal file
View File

@ -0,0 +1,246 @@
(*
* 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 data types
*)
chapter "ARM-Specific Data Types"
theory Arch_Structs_A
imports
"../../design/$L4V_ARCH/Arch_Structs_B"
"../ExceptionTypes_A"
ArchVMRights_A
begin
context Arch begin global_naming ARM_A
text {*
This theory provides architecture-specific definitions and datatypes
including architecture-specific capabilities and objects.
*}
section {* Architecture-specific virtual memory *}
text {* An ASID is simply a word. *}
type_synonym asid = "word32"
datatype vm_attribute = ParityEnabled | PageCacheable | Global | XNever
type_synonym vm_attributes = "vm_attribute set"
section {* Architecture-specific capabilities *}
text {* The ARM kernel supports capabilities for ASID pools and an ASID controller capability,
along with capabilities for page directories, page tables, and page mappings. *}
datatype arch_cap =
ASIDPoolCap obj_ref asid
| ASIDControlCap
| PageCap obj_ref cap_rights vmpage_size "(asid * vspace_ref) option"
| PageTableCap obj_ref "(asid * vspace_ref) option"
| PageDirectoryCap obj_ref "asid option"
lemmas arch_cap_cases =
arch_cap.induct[where arch_cap=x and P="\<lambda>x'. x = x' \<longrightarrow> P x'" for x P, simplified, rule_format]
lemmas arch_cap_cases_asm =
arch_cap.induct[where arch_cap=x and P="\<lambda>x'. x = x' \<longrightarrow> P x' \<longrightarrow> R" for P R x,
simplified, rule_format, rotated -1]
definition
is_page_cap :: "arch_cap \<Rightarrow> bool" where
"is_page_cap c \<equiv> \<exists>x0 x1 x2 x3. c = PageCap x0 x1 x2 x3"
definition
asid_high_bits :: nat where
"asid_high_bits \<equiv> 8"
definition
asid_low_bits :: nat where
"asid_low_bits \<equiv> 10 :: nat"
definition
asid_bits :: nat where
"asid_bits \<equiv> 18 :: nat"
section {* Architecture-specific objects *}
text {* This section gives the types and auxiliary definitions for the
architecture-specific objects: a page directory entry (@{text "pde"})
contains either an invalid entry, a page table reference, a section
reference, or a super-section reference; a page table entry contains
either an invalid entry, a large page, or a small page mapping;
finally, an architecture-specific object is either an ASID pool, a
page table, a page directory, or a data page used to model user
memory.
*}
datatype pde =
InvalidPDE
| PageTablePDE obj_ref vm_attributes machine_word
| SectionPDE obj_ref vm_attributes machine_word cap_rights
| SuperSectionPDE obj_ref vm_attributes cap_rights
datatype pte =
InvalidPTE
| LargePagePTE obj_ref vm_attributes cap_rights
| SmallPagePTE obj_ref vm_attributes cap_rights
datatype arch_kernel_obj =
ASIDPool "10 word \<rightharpoonup> obj_ref"
| PageTable "word8 \<Rightarrow> pte"
| PageDirectory "12 word \<Rightarrow> pde"
| DataPage vmpage_size
lemmas arch_kernel_obj_cases =
arch_kernel_obj.induct[where arch_kernel_obj=x and P="\<lambda>x'. x = x' \<longrightarrow> P x'" for x P, simplified, rule_format]
lemmas arch_kernel_obj_cases_asm =
arch_kernel_obj.induct[where arch_kernel_obj=x and P="\<lambda>x'. x = x' \<longrightarrow> P x' \<longrightarrow> R" for P R x,
simplified, rule_format, rotated -1]
primrec
arch_obj_size :: "arch_cap \<Rightarrow> nat"
where
"arch_obj_size (ASIDPoolCap p as) = pageBits"
| "arch_obj_size ASIDControlCap = 0"
| "arch_obj_size (PageCap x rs sz as4) = pageBitsForSize sz"
| "arch_obj_size (PageDirectoryCap x as2) = 14"
| "arch_obj_size (PageTableCap x as3) = 10"
primrec
arch_kobj_size :: "arch_kernel_obj \<Rightarrow> nat"
where
"arch_kobj_size (ASIDPool p) = pageBits"
| "arch_kobj_size (PageTable pte) = 10"
| "arch_kobj_size (PageDirectory pde) = 14"
| "arch_kobj_size (DataPage sz) = pageBitsForSize sz"
primrec
aobj_ref :: "arch_cap \<rightharpoonup> obj_ref"
where
"aobj_ref (ASIDPoolCap p as) = Some p"
| "aobj_ref ASIDControlCap = None"
| "aobj_ref (PageCap x rs sz as4) = Some x"
| "aobj_ref (PageDirectoryCap x as2) = Some x"
| "aobj_ref (PageTableCap x as3) = Some x"
primrec (nonexhaustive)
acap_rights :: "arch_cap \<Rightarrow> cap_rights"
where
"acap_rights (PageCap x rs sz as) = rs"
definition
acap_rights_update :: "cap_rights \<Rightarrow> arch_cap \<Rightarrow> arch_cap" where
"acap_rights_update rs ac \<equiv> case ac of
PageCap x rs' sz as \<Rightarrow> PageCap x (validate_vm_rights rs) sz as
| _ \<Rightarrow> ac"
section {* Architecture-specific object types and default objects *}
datatype
aobject_type =
SmallPageObj
| LargePageObj
| SectionObj
| SuperSectionObj
| PageTableObj
| PageDirectoryObj
| ASIDPoolObj
definition
arch_default_cap :: "aobject_type \<Rightarrow> obj_ref \<Rightarrow> nat \<Rightarrow> arch_cap" where
"arch_default_cap tp r n \<equiv> case tp of
SmallPageObj \<Rightarrow> PageCap r vm_read_write ARMSmallPage None
| LargePageObj \<Rightarrow> PageCap r vm_read_write ARMLargePage None
| SectionObj \<Rightarrow> PageCap r vm_read_write ARMSection None
| SuperSectionObj \<Rightarrow> PageCap r vm_read_write ARMSuperSection None
| PageTableObj \<Rightarrow> PageTableCap r None
| PageDirectoryObj \<Rightarrow> PageDirectoryCap r None
| ASIDPoolObj \<Rightarrow> ASIDPoolCap r 0" (* unused *)
definition
default_arch_object :: "aobject_type \<Rightarrow> nat \<Rightarrow> arch_kernel_obj" where
"default_arch_object tp n \<equiv> case tp of
SmallPageObj \<Rightarrow> DataPage ARMSmallPage
| LargePageObj \<Rightarrow> DataPage ARMLargePage
| SectionObj \<Rightarrow> DataPage ARMSection
| SuperSectionObj \<Rightarrow> DataPage ARMSuperSection
| PageTableObj \<Rightarrow> PageTable (\<lambda>x. InvalidPTE)
| PageDirectoryObj \<Rightarrow> PageDirectory (\<lambda>x. InvalidPDE)
| ASIDPoolObj \<Rightarrow> ASIDPool (\<lambda>_. None)"
type_synonym hw_asid = word8
type_synonym arm_vspace_region_uses = "vspace_ref \<Rightarrow> arm_vspace_region_use"
section {* Architecture-specific state *}
text {* The architecture-specific state for the ARM model
consists of a reference to the globals page (@{text "arm_globals_frame"}),
the first level of the ASID table (@{text "arm_asid_table"}), a
map from hardware ASIDs to seL4 ASIDs (@{text "arm_hwasid_table"}),
the next hardware ASID to preempt (@{text "arm_next_asid"}), the
inverse map from seL4 ASIDs to hardware ASIDs (first component of
@{text "arm_asid_map"}), and the address of the page directory and
page tables mapping the shared address space, along with a description
of this space (@{text "arm_global_pd"}, @{text "arm_global_pts"}, and
@{text "arm_kernel_vspace"} respectively).
Hardware ASIDs are only ever associated with seL4 ASIDs that have a
currently active page directory. The second component of
@{text "arm_asid_map"} values is the address of that page directory.
*}
end
qualify ARM_A (in Arch)
record arch_state =
arm_globals_frame :: obj_ref
arm_asid_table :: "word8 \<rightharpoonup> obj_ref"
arm_hwasid_table :: "ARM_A.hw_asid \<rightharpoonup> ARM_A.asid"
arm_next_asid :: ARM_A.hw_asid
arm_asid_map :: "ARM_A.asid \<rightharpoonup> (ARM_A.hw_asid \<times> obj_ref)"
arm_global_pd :: obj_ref
arm_global_pts :: "obj_ref list"
arm_kernel_vspace :: ARM_A.arm_vspace_region_uses
end_qualify
context Arch begin global_naming ARM_A
definition
pd_bits :: "nat" where
"pd_bits \<equiv> pageBits + 2"
definition
pt_bits :: "nat" where
"pt_bits \<equiv> pageBits - 2"
section "Type declarations for invariant definitions"
datatype aa_type =
AASIDPool
| APageTable
| APageDirectory
| AIntData vmpage_size
definition aa_type :: "arch_kernel_obj \<Rightarrow> aa_type"
where
"aa_type ao \<equiv> (case ao of
PageTable pt \<Rightarrow> APageTable
| PageDirectory pd \<Rightarrow> APageDirectory
| DataPage sz \<Rightarrow> AIntData sz
| ASIDPool f \<Rightarrow> AASIDPool)"
end
end

120
spec/abstract/ARM_HYP/Init_A.thy Normal file
View File

@ -0,0 +1,120 @@
(*
* 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)
*)
(*
Dummy initial kernel state. Real kernel boot up is more complex.
*)
chapter "An Initial Kernel State"
theory Init_A
imports "../Retype_A"
begin
context Arch begin global_naming ARM_A
text {*
This is not a specification of true kernel
initialisation. This theory describes a dummy initial state only, to
show that the invariants and refinement relation are consistent.
*}
(* Moved to Deterministic_A
definition
idle_thread_ptr :: word32 where
"idle_thread_ptr = kernel_base + 0x1000"
*)
definition
init_tcb_ptr :: word32 where
"init_tcb_ptr = kernel_base + 0x2000"
definition
init_irq_node_ptr :: word32 where
"init_irq_node_ptr = kernel_base + 0x8000"
definition
init_globals_frame :: word32 where
"init_globals_frame = kernel_base + 0x5000"
definition
init_global_pd :: word32 where
"init_global_pd = kernel_base + 0x60000"
definition
"init_arch_state \<equiv> \<lparr>
arm_globals_frame = init_globals_frame,
arm_asid_table = empty,
arm_hwasid_table = empty,
arm_next_asid = 0,
arm_asid_map = empty,
arm_global_pd = init_global_pd,
arm_global_pts = [],
arm_kernel_vspace = \<lambda>ref.
if ref \<in> {kernel_base .. kernel_base + mask 20}
then ArmVSpaceKernelWindow
else ArmVSpaceInvalidRegion
\<rparr>"
definition
empty_context :: user_context where
"empty_context \<equiv> \<lambda>_. 0"
definition
[simp]:
"global_pd \<equiv> (\<lambda>_. InvalidPDE)( ucast (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})"
definition
"init_kheap \<equiv>
(\<lambda>x. if \<exists>irq :: irq. init_irq_node_ptr + (ucast irq << cte_level_bits) = x
then Some (CNode 0 (empty_cnode 0)) else None)
(idle_thread_ptr \<mapsto> TCB \<lparr>
tcb_ctable = NullCap,
tcb_vtable = NullCap,
tcb_reply = NullCap,
tcb_caller = NullCap,
tcb_ipcframe = NullCap,
tcb_state = IdleThreadState,
tcb_fault_handler = replicate word_bits False,
tcb_ipc_buffer = 0,
tcb_context = empty_context,
tcb_fault = None,
tcb_bound_notification = None
\<rparr>,
init_globals_frame \<mapsto> ArchObj (DataPage ARMSmallPage),
init_global_pd \<mapsto> ArchObj (PageDirectory global_pd)
)"
definition
"init_cdt \<equiv> empty"
definition
"init_ioc \<equiv>
\<lambda>(a,b). (\<exists>obj. init_kheap a = Some obj \<and>
(\<exists>cap. cap_of obj b = Some cap \<and> cap \<noteq> cap.NullCap))"
definition
"init_A_st \<equiv> \<lparr>
kheap = init_kheap,
cdt = init_cdt,
is_original_cap = init_ioc,
cur_thread = idle_thread_ptr,
idle_thread = idle_thread_ptr,
machine_state = init_machine_state,
interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (ucast irq << cte_level_bits),
interrupt_states = \<lambda>_. Structures_A.IRQInactive,
arch_state = init_arch_state,
exst = ext_init
\<rparr>"
end
end

140
spec/abstract/ARM_HYP/Machine_A.thy Normal file
View File

@ -0,0 +1,140 @@
(*
* 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)
*)
(*
Types and operations to access the underlying machine, instantiated
for ARM.
*)
chapter "ARM Machine Instantiation"
theory Machine_A
imports
"../../machine/$L4V_ARCH/MachineTypes"
begin
context Arch begin global_naming ARM_A
text {*
The specification is written with abstract type names for object
references, user pointers, word-based data, cap references, and so
on. This theory provides an instantiation of these names to concrete
types for the ARM architecture. Other architectures may have slightly
different instantiations.
*}
type_synonym obj_ref = machine_word
type_synonym vspace_ref = machine_word
type_synonym data_offset = "12 word"
type_synonym data = machine_word
type_synonym cap_ref = "bool list"
type_synonym length_type = machine_word
type_synonym asid_pool_index = "10 word"
type_synonym asid_index = "8 word" (* FIXME: better name? *)
text {* With the definitions above, most conversions between abstract
type names boil down to just the identity function, some convert from
@{text word} to @{typ nat} and others between different word sizes
using @{const ucast}. *}
definition
oref_to_data :: "obj_ref \<Rightarrow> data" where
"oref_to_data \<equiv> id"
definition
data_to_oref :: "data \<Rightarrow> obj_ref" where
"data_to_oref \<equiv> id"
definition
vref_to_data :: "vspace_ref \<Rightarrow> data" where
"vref_to_data \<equiv> id"
definition
data_to_vref :: "data \<Rightarrow> vspace_ref" where
"data_to_vref \<equiv> id"
definition
nat_to_len :: "nat \<Rightarrow> length_type" where
"nat_to_len \<equiv> of_nat"
definition
data_to_nat :: "data \<Rightarrow> nat" where
"data_to_nat \<equiv> unat"
definition
data_to_16 :: "data \<Rightarrow> 16 word" where
"data_to_16 \<equiv> ucast"
definition
data_to_cptr :: "data \<Rightarrow> cap_ref" where
"data_to_cptr \<equiv> to_bl"
definition
data_offset_to_nat :: "data_offset \<Rightarrow> nat" where
"data_offset_to_nat \<equiv> unat"
definition
combine_ntfn_badges :: "data \<Rightarrow> data \<Rightarrow> data" where
"combine_ntfn_badges \<equiv> bitOR"
definition
combine_ntfn_msgs :: "data \<Rightarrow> data \<Rightarrow> data" where
"combine_ntfn_msgs \<equiv> bitOR"
text {* These definitions will be unfolded automatically in proofs. *}
lemmas data_convs [simp] =
oref_to_data_def data_to_oref_def vref_to_data_def data_to_vref_def
nat_to_len_def data_to_nat_def data_to_16_def data_to_cptr_def
data_offset_to_nat_def
text {* The following definitions provide architecture-dependent sizes
such as the standard page size and capability size of the underlying
machine.
*}
definition
slot_bits :: nat where
"slot_bits \<equiv> 4"
type_synonym user_context = "register \<Rightarrow> data"
definition
new_context :: "user_context" where
"new_context \<equiv> (\<lambda>r. 0) (CPSR := 0x150)"
text {* Miscellaneous definitions of constants used in modelling machine
operations. *}
definition
nat_to_cref :: "nat \<Rightarrow> nat \<Rightarrow> cap_ref" where
"nat_to_cref ln n \<equiv> drop (word_bits - ln)
(to_bl (of_nat n :: machine_word))"
definition
"msg_info_register \<equiv> msgInfoRegister"
definition
"msg_registers \<equiv> msgRegisters"
definition
"cap_register \<equiv> capRegister"
definition
"badge_register \<equiv> badgeRegister"
definition
"frame_registers \<equiv> frameRegisters"
definition
"gp_registers \<equiv> gpRegisters"
definition
"exception_message \<equiv> exceptionMessage"
definition
"syscall_message \<equiv> syscallMessage"
end
end

520
spec/machine/ARM_HYP/MachineOps.thy Normal file
View File

@ -0,0 +1,520 @@
(*
* 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)
*)
chapter "Machine Operations"
theory MachineOps
imports
"../MachineMonad"
begin
section "Wrapping and Lifting Machine Operations"
text {*
Most of the machine operations below work on the underspecified
part of the machine state @{typ machine_state_rest} and cannot fail.
We could express the latter by type (leaving out the failure flag),
but if we later wanted to implement them,
we'd have to set up a new hoare-logic
framework for that type. So instead, we provide a wrapper for these
operations that explicitly ignores the fail flag and sets it to
False. Similarly, these operations never return an empty set of
follow-on states, which would require the operation to fail.
So we explicitly make this (non-existing) case a null operation.
All this is done only to avoid a large number of axioms (2 for each operation).
*}
context Arch begin global_naming ARM
section "The Operations"
consts'
memory_regions :: "(paddr \<times> paddr) list" (* avail_p_regs *)
device_regions :: "(paddr \<times> paddr) list" (* dev_p_regs *)
definition
getMemoryRegions :: "(paddr * paddr) list machine_monad"
where "getMemoryRegions \<equiv> return memory_regions"
consts'
getDeviceRegions_impl :: "unit machine_rest_monad"
getDeviceRegions_val :: "machine_state \<Rightarrow> (paddr * paddr) list"
definition
getDeviceRegions :: "(paddr * paddr) list machine_monad"
where
"getDeviceRegions \<equiv> return device_regions"
consts'
getKernelDevices_impl :: "unit machine_rest_monad"
getKernelDevices_val :: "machine_state \<Rightarrow> (paddr * machine_word) list"
definition
getKernelDevices :: "(paddr * machine_word) list machine_monad"
where
"getKernelDevices \<equiv> do
machine_op_lift getKernelDevices_impl;
gets getKernelDevices_val
od"
definition
loadWord :: "machine_word \<Rightarrow> machine_word machine_monad"
where "loadWord p \<equiv> do m \<leftarrow> gets underlying_memory;
assert (p && mask 2 = 0);
return (word_rcat [m (p + 3), m (p + 2), m (p + 1), m p])
od"
definition
storeWord :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
where "storeWord p w \<equiv> do
assert (p && mask 2 = 0);
modify (underlying_memory_update (\<lambda>m.
m(p := word_rsplit w ! 3,
p + 1 := word_rsplit w ! 2,
p + 2 := word_rsplit w ! 1,
p + 3 := word_rsplit w ! 0)))
od"
lemma loadWord_storeWord_is_return:
"p && mask 2 = 0 \<Longrightarrow> (do w \<leftarrow> loadWord p; storeWord p w od) = return ()"
apply (rule ext)
apply (simp add: loadWord_def storeWord_def bind_def assert_def return_def
modify_def gets_def get_def eval_nat_numeral put_def)
apply (simp add: word_rsplit_rcat_size word_size)
done
text {* This instruction is required in the simulator, only. *}
definition
storeWordVM :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
where "storeWordVM w p \<equiv> return ()"
consts'
configureTimer_impl :: "unit machine_rest_monad"
configureTimer_val :: "machine_state \<Rightarrow> irq"
definition
configureTimer :: "irq machine_monad"
where
"configureTimer \<equiv> do
machine_op_lift configureTimer_impl;
gets configureTimer_val
od"
consts' (* XXX: replaces configureTimer in new boot code
TODO: remove configureTimer when haskell updated *)
initTimer_impl :: "unit machine_rest_monad"
definition
initTimer :: "unit machine_monad"
where "initTimer \<equiv> machine_op_lift initTimer_impl"
consts'
resetTimer_impl :: "unit machine_rest_monad"
definition
resetTimer :: "unit machine_monad"
where "resetTimer \<equiv> machine_op_lift resetTimer_impl"
consts'
writeTTBR0_impl :: "paddr \<Rightarrow> unit machine_rest_monad"
definition
writeTTBR0 :: "paddr \<Rightarrow> unit machine_monad"
where "writeTTBR0 pd \<equiv> machine_op_lift (writeTTBR0_impl pd)"
consts'
setHardwareASID_impl :: "hardware_asid \<Rightarrow> unit machine_rest_monad"
definition
setHardwareASID:: "hardware_asid \<Rightarrow> unit machine_monad"
where "setHardwareASID a \<equiv> machine_op_lift (setHardwareASID_impl a)"
(* Memory Barriers *)
consts'
isb_impl :: "unit machine_rest_monad"
definition
isb :: "unit machine_monad"
where "isb \<equiv> machine_op_lift isb_impl"
consts'
dsb_impl :: "unit machine_rest_monad"
definition
dsb :: "unit machine_monad"
where "dsb \<equiv> machine_op_lift dsb_impl"
consts'
dmb_impl :: "unit machine_rest_monad"
definition
dmb :: "unit machine_monad"
where "dmb \<equiv> machine_op_lift dmb_impl"
definition
setCurrentPD :: "paddr \<Rightarrow> unit machine_monad"
where "setCurrentPD pd \<equiv> do
dsb;
writeTTBR0 pd;
isb
od"
consts'
invalidateTLB_impl :: "unit machine_rest_monad"
definition
invalidateTLB :: "unit machine_monad"
where "invalidateTLB \<equiv> machine_op_lift invalidateTLB_impl"
consts'
invalidateTLB_ASID_impl :: "hardware_asid \<Rightarrow> unit machine_rest_monad"
definition
invalidateTLB_ASID :: "hardware_asid \<Rightarrow> unit machine_monad"
where "invalidateTLB_ASID a \<equiv> machine_op_lift (invalidateTLB_ASID_impl a)"
(* C implementation takes one argument, which is w || a *)
consts'
invalidateTLB_VAASID_impl :: "machine_word \<Rightarrow> unit machine_rest_monad"
definition
invalidateTLB_VAASID :: "machine_word \<Rightarrow> unit machine_monad"
where "invalidateTLB_VAASID w \<equiv> machine_op_lift (invalidateTLB_VAASID_impl w)"
consts'
cleanByVA_impl :: "machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_rest_monad"
definition
cleanByVA :: "machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_monad"
where "cleanByVA w p \<equiv> machine_op_lift (cleanByVA_impl w p)"
consts'
cleanByVA_PoU_impl :: "machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_rest_monad"
definition
cleanByVA_PoU :: "machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_monad"
where "cleanByVA_PoU w p \<equiv> machine_op_lift (cleanByVA_PoU_impl w p)"
consts'
invalidateByVA_impl :: "machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_rest_monad"
definition
invalidateByVA :: "machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_monad"
where "invalidateByVA w p \<equiv> machine_op_lift (invalidateByVA_impl w p)"
consts'
invalidateByVA_I_impl :: "machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_rest_monad"
definition
invalidateByVA_I :: "machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_monad"
where "invalidateByVA_I w p \<equiv> machine_op_lift (invalidateByVA_I_impl w p)"
consts'
invalidate_I_PoU_impl :: "unit machine_rest_monad"
definition
invalidate_I_PoU :: "unit machine_monad"
where "invalidate_I_PoU \<equiv> machine_op_lift invalidate_I_PoU_impl"
consts'
cleanInvalByVA_impl :: "machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_rest_monad"
definition
cleanInvalByVA :: "machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_monad"
where "cleanInvalByVA w p \<equiv> machine_op_lift (cleanInvalByVA_impl w p)"
consts'
branchFlush_impl :: "machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_rest_monad"
definition
branchFlush :: "machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_monad"
where "branchFlush w p \<equiv> machine_op_lift (branchFlush_impl w p)"
consts'
clean_D_PoU_impl :: "unit machine_rest_monad"
definition
clean_D_PoU :: "unit machine_monad"
where "clean_D_PoU \<equiv> machine_op_lift clean_D_PoU_impl"
consts'
cleanInvalidate_D_PoC_impl :: "unit machine_rest_monad"
definition
cleanInvalidate_D_PoC :: "unit machine_monad"
where "cleanInvalidate_D_PoC \<equiv> machine_op_lift cleanInvalidate_D_PoC_impl"
consts'
cleanInvalidateL2Range_impl :: "paddr \<Rightarrow> paddr \<Rightarrow> unit machine_rest_monad"
definition
cleanInvalidateL2Range :: "paddr \<Rightarrow> paddr \<Rightarrow> unit machine_monad"
where "cleanInvalidateL2Range w p \<equiv> machine_op_lift (cleanInvalidateL2Range_impl w p)"
consts'
invalidateL2Range_impl :: "paddr \<Rightarrow> paddr \<Rightarrow> unit machine_rest_monad"
definition
invalidateL2Range :: "paddr \<Rightarrow> paddr \<Rightarrow> unit machine_monad"
where "invalidateL2Range w p \<equiv> machine_op_lift (invalidateL2Range_impl w p)"
consts'
cleanL2Range_impl :: "paddr \<Rightarrow> paddr \<Rightarrow> unit machine_rest_monad"
definition
cleanL2Range :: "paddr \<Rightarrow> paddr \<Rightarrow> unit machine_monad"
where "cleanL2Range w p \<equiv> machine_op_lift (cleanL2Range_impl w p)"
consts'
initL2Cache_impl :: "unit machine_rest_monad"
definition
initL2Cache :: "unit machine_monad"
where "initL2Cache \<equiv> machine_op_lift initL2Cache_impl"
definition
clearExMonitor :: "unit machine_monad"
where "clearExMonitor \<equiv> modify (\<lambda>s. s \<lparr> exclusive_state := default_exclusive_state \<rparr>)"
consts'
flushBTAC_impl :: "unit machine_rest_monad"
definition
flushBTAC :: "unit machine_monad"
where "flushBTAC \<equiv> machine_op_lift flushBTAC_impl"
consts'
initIRQController_impl :: "unit machine_rest_monad"
definition
initIRQController :: "unit machine_monad"
where "initIRQController \<equiv> machine_op_lift initIRQController_impl"
consts'
writeContextID_impl :: "unit machine_rest_monad"
definition
writeContextID :: "unit machine_monad"
where "writeContextID \<equiv> machine_op_lift writeContextID_impl"
lemmas cache_machine_op_defs = isb_def dsb_def dmb_def writeContextID_def flushBTAC_def
clearExMonitor_def cleanL2Range_def invalidateL2Range_def
cleanInvalidateL2Range_def cleanInvalidate_D_PoC_def
clean_D_PoU_def branchFlush_def cleanInvalByVA_def
invalidate_I_PoU_def invalidateByVA_I_def invalidateByVA_def
cleanByVA_PoU_def cleanByVA_def invalidateTLB_VAASID_def
invalidateTLB_ASID_def invalidateTLB_def
consts'
IFSR_val :: "machine_state \<Rightarrow> machine_word"
DFSR_val :: "machine_state \<Rightarrow> machine_word"
FAR_val :: "machine_state \<Rightarrow> machine_word"
definition
getIFSR :: "machine_word machine_monad"
where "getIFSR \<equiv> gets IFSR_val"
definition
getDFSR :: "machine_word machine_monad"
where "getDFSR \<equiv> gets DFSR_val"
definition
getFAR :: "machine_word machine_monad"
where "getFAR \<equiv> gets FAR_val"
definition
debugPrint :: "unit list \<Rightarrow> unit machine_monad"
where
debugPrint_def[simp]:
"debugPrint \<equiv> \<lambda>message. return ()"
consts'
ackInterrupt_impl :: "irq \<Rightarrow> unit machine_rest_monad"
definition
ackInterrupt :: "irq \<Rightarrow> unit machine_monad"
where
"ackInterrupt irq \<equiv> machine_op_lift (ackInterrupt_impl irq)"
-- "Interrupt controller operations"
text {*
@{term getActiveIRQ} is now derministic.
It 'updates' the irq state to the reflect the passage of
time since last the irq was gotten, then it gets the active
IRQ (if there is one).
*}
definition
getActiveIRQ :: "(irq option) machine_monad"
where
"getActiveIRQ \<equiv> do
is_masked \<leftarrow> gets $ irq_masks;
modify (\<lambda>s. s \<lparr> irq_state := irq_state s + 1 \<rparr>);
active_irq \<leftarrow> gets $ irq_oracle \<circ> irq_state;
if is_masked active_irq \<or> active_irq = 0x3FF
then return None
else return ((Some active_irq) :: irq option)
od"
definition
maskInterrupt :: "bool \<Rightarrow> irq \<Rightarrow> unit machine_monad"
where
"maskInterrupt m irq \<equiv>
modify (\<lambda>s. s \<lparr> irq_masks := (irq_masks s) (irq := m) \<rparr>)"
definition
lineStart :: "machine_word \<Rightarrow> machine_word"
where
"lineStart addr = (addr >> cacheLineBits) << cacheLineBits"
text {*
Performs the given operation on every cache line that intersects the
supplied range.
*}
definition
cacheRangeOp :: "(machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_monad)
\<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_monad"
where
"cacheRangeOp operation vstart vend pstart \<equiv>
let pend = pstart + (vend - vstart);
vptrs = [lineStart vstart, lineStart vstart + of_nat cacheLine .e. lineStart vend];
pptrs = [lineStart pstart, lineStart pstart + of_nat cacheLine .e. lineStart pend]
in mapM_x (\<lambda>(v, p). operation v p) (zip vptrs pptrs)"
definition
cleanCacheRange_PoC :: "machine_word \<Rightarrow> machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_monad"
where
"cleanCacheRange_PoC vstart vend pstart \<equiv> cacheRangeOp cleanByVA vstart vend pstart"
definition
cleanInvalidateCacheRange_RAM :: "machine_word \<Rightarrow> machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_monad"
where
"cleanInvalidateCacheRange_RAM vstart vend pstart \<equiv> do
cleanCacheRange_PoC vstart vend pstart;
dsb;
cleanInvalidateL2Range pstart (pstart + (vend - vstart));
cacheRangeOp cleanInvalByVA vstart vend pstart;
dsb
od"
definition
cleanCacheRange_RAM :: "machine_word \<Rightarrow> machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_monad"
where
"cleanCacheRange_RAM vstart vend pstart \<equiv> do
cleanCacheRange_PoC vstart vend pstart;
dsb;
cleanL2Range pstart (pstart + (vend - vstart))
od"
definition
cleanCacheRange_PoU :: "machine_word \<Rightarrow> machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_monad"
where
"cleanCacheRange_PoU vstart vend pstart \<equiv> cacheRangeOp cleanByVA_PoU vstart vend pstart"
definition
invalidateCacheRange_RAM :: "machine_word \<Rightarrow> machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_monad"
where
"invalidateCacheRange_RAM vstart vend pstart \<equiv> do
when (vstart \<noteq> lineStart vstart) $
cleanCacheRange_RAM vstart vstart pstart;
when (vend + 1 \<noteq> lineStart (vend + 1)) $
cleanCacheRange_RAM (lineStart vend) (lineStart vend)
(pstart + ((lineStart vend) - vstart));
invalidateL2Range pstart (pstart + (vend - vstart));
cacheRangeOp invalidateByVA vstart vend pstart;
dsb
od"
definition
invalidateCacheRange_I :: "machine_word \<Rightarrow> machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_monad"
where
"invalidateCacheRange_I vstart vend pstart \<equiv> cacheRangeOp invalidateByVA_I vstart vend pstart"
definition
branchFlushRange :: "machine_word \<Rightarrow> machine_word \<Rightarrow> paddr \<Rightarrow> unit machine_monad"
where
"branchFlushRange vstart vend pstart \<equiv> cacheRangeOp branchFlush vstart vend pstart"
definition
cleanCaches_PoU :: "unit machine_monad"
where
"cleanCaches_PoU \<equiv> do
dsb;
clean_D_PoU;
dsb;
invalidate_I_PoU;
dsb
od"
definition
cleanInvalidateL1Caches :: "unit machine_monad"
where
"cleanInvalidateL1Caches \<equiv> do
dsb;
cleanInvalidate_D_PoC;
dsb;
invalidate_I_PoU;
dsb
od"
section "Memory Clearance"
text {* Clear memory contents to recycle it as user memory *}
definition
clearMemory :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
where
"clearMemory ptr bytelength \<equiv>
do mapM_x (\<lambda>p. storeWord p 0) [ptr, ptr + word_size .e. ptr + (of_nat bytelength) - 1];
cleanCacheRange_PoU ptr (ptr + of_nat bytelength - 1) (addrFromPPtr ptr)
od"
definition
clearMemoryVM :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
where
"clearMemoryVM ptr bits \<equiv> return ()"
text {*
Initialize memory to be used as user memory.
Note that zeroing out the memory is redundant in the specifications.
In any case, we cannot abstract from the call to cleanCacheRange,
which appears in the implementation.
*}
abbreviation (input) "initMemory == clearMemory"
text {*
Free memory that had been initialized as user memory.
While freeing memory is a no-op in the implementation,
we zero out the underlying memory in the specifications to avoid garbage.
If we know that there is no garbage,
we can compute from the implementation state
what the exact memory content in the specifications is.
*}
definition
freeMemory :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
where
"freeMemory ptr bits \<equiv>
mapM_x (\<lambda>p. storeWord p 0) [ptr, ptr + word_size .e. ptr + 2 ^ bits - 1]"
section "User Monad"
type_synonym user_context = "register \<Rightarrow> machine_word"
type_synonym 'a user_monad = "(user_context, 'a) nondet_monad"
definition
getRegister :: "register \<Rightarrow> machine_word user_monad"
where
"getRegister r \<equiv> gets (\<lambda>uc. uc r)"
definition
setRegister :: "register \<Rightarrow> machine_word \<Rightarrow> unit user_monad"
where
"setRegister r v \<equiv> modify (\<lambda>uc. uc (r := v))"
definition
"getRestartPC \<equiv> getRegister FaultInstruction"
definition
"setNextPC \<equiv> setRegister LR_svc"
end
translations
(type) "'a ARM.user_monad" <= (type) "(ARM.register \<Rightarrow> ARM.machine_word, 'a) nondet_monad"
end

83
spec/machine/ARM_HYP/Platform.thy Normal file
View File

@ -0,0 +1,83 @@
(*
* 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)
*)
chapter "Platform Definitions"
theory Platform
imports
"../../../lib/Defs"
"../../../lib/Lib"
"../../../lib/$L4V_ARCH/WordSetup"
"../Setup_Locale"
begin
context Arch begin global_naming ARM
text {*
This theory lists platform-specific types and basic constants, in particular
the types of interrupts and physical addresses, constants for the
kernel location, the offsets between physical and virtual kernel
addresses, as well as the range of IRQs on the platform.
*}
type_synonym irq = "10 word"
type_synonym paddr = word32
abbreviation (input) "toPAddr \<equiv> id"
abbreviation (input) "fromPAddr \<equiv> id"
definition
pageColourBits :: nat where
"pageColourBits \<equiv> 2"
definition
cacheLineBits :: nat where
"cacheLineBits = 5"
definition
cacheLine :: nat where
"cacheLine = 2^cacheLineBits"
definition
kernelBase_addr :: word32 where
"kernelBase_addr \<equiv> 0xe0000000"
(* Arch specific kernel base address used for haskell spec *)
definition
kernelBase :: word32 where
"kernelBase \<equiv> 0xe0000000"
definition
physBase :: word32 where
"physBase \<equiv> 0x10000000"
definition
physMappingOffset :: word32 where
"physMappingOffset \<equiv> kernelBase_addr - physBase"
definition
ptrFromPAddr :: "paddr \<Rightarrow> word32" where
"ptrFromPAddr paddr \<equiv> paddr + physMappingOffset"
definition
addrFromPPtr :: "word32 \<Rightarrow> paddr" where
"addrFromPPtr pptr \<equiv> pptr - physMappingOffset"
definition
minIRQ :: "irq" where
"minIRQ \<equiv> 0"
definition
maxIRQ :: "irq" where
"maxIRQ \<equiv> 0x9F"
end
end