x64: remove generated exec spec
This commit is contained in:
Matthew Brecknell
parent
3871575834
commit
f4a220e587
|
|
@ -30,6 +30,7 @@
|
|||
/spec/design/*.thy
|
||||
/spec/design/ARM/*.thy
|
||||
/spec/design/ARM_HYP/*.thy
|
||||
/spec/design/X64/*.thy
|
||||
|
||||
/spec/machine/*/MachineTypes.thy
|
||||
|
||||
|
|
|
|||
|
|
@ -1,44 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file ArchFaultHandler_H.thy *)
|
||||
(*
|
||||
* 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 "Fault Handlers"
|
||||
|
||||
theory ArchFaultHandler_H
|
||||
imports "../TCB_H" "../Structures_H"
|
||||
begin
|
||||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
|
||||
consts'
|
||||
makeArchFaultMessage :: "arch_fault \<Rightarrow> machine_word \<Rightarrow> (machine_word * machine_word list) kernel"
|
||||
|
||||
consts'
|
||||
handleArchFaultReply :: "arch_fault \<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow> machine_word list \<Rightarrow> bool kernel"
|
||||
|
||||
defs makeArchFaultMessage_def:
|
||||
"makeArchFaultMessage x0 thread\<equiv> (case x0 of
|
||||
(VMFault vptr archData) \<Rightarrow> (do
|
||||
pc \<leftarrow> asUser thread getRestartPC;
|
||||
return (5, pc#fromVPtr vptr#archData)
|
||||
od)
|
||||
)"
|
||||
|
||||
defs handleArchFaultReply_def:
|
||||
"handleArchFaultReply x0 x1 x2 x3\<equiv> (case x0 of
|
||||
(VMFault _ _) \<Rightarrow> return True
|
||||
)"
|
||||
|
||||
|
||||
end
|
||||
|
||||
end
|
||||
|
|
@ -1,69 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file ArchFault_H.thy *)
|
||||
(*
|
||||
* 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)
|
||||
*)
|
||||
|
||||
(*
|
||||
VSpace lookup code.
|
||||
*)
|
||||
|
||||
theory ArchFault_H
|
||||
imports "../Types_H"
|
||||
begin
|
||||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
datatype arch_fault =
|
||||
VMFault vptr "machine_word list"
|
||||
|
||||
primrec
|
||||
vmFaultAddress :: "arch_fault \<Rightarrow> vptr"
|
||||
where
|
||||
"vmFaultAddress (VMFault v0 v1) = v0"
|
||||
|
||||
primrec
|
||||
vmFaultArchData :: "arch_fault \<Rightarrow> machine_word list"
|
||||
where
|
||||
"vmFaultArchData (VMFault v0 v1) = v1"
|
||||
|
||||
primrec
|
||||
vmFaultAddress_update :: "(vptr \<Rightarrow> vptr) \<Rightarrow> arch_fault \<Rightarrow> arch_fault"
|
||||
where
|
||||
"vmFaultAddress_update f (VMFault v0 v1) = VMFault (f v0) v1"
|
||||
|
||||
primrec
|
||||
vmFaultArchData_update :: "((machine_word list) \<Rightarrow> (machine_word list)) \<Rightarrow> arch_fault \<Rightarrow> arch_fault"
|
||||
where
|
||||
"vmFaultArchData_update f (VMFault v0 v1) = VMFault v0 (f v1)"
|
||||
|
||||
abbreviation (input)
|
||||
VMFault_trans :: "(vptr) \<Rightarrow> (machine_word list) \<Rightarrow> arch_fault" ("VMFault'_ \<lparr> vmFaultAddress= _, vmFaultArchData= _ \<rparr>")
|
||||
where
|
||||
"VMFault_ \<lparr> vmFaultAddress= v0, vmFaultArchData= v1 \<rparr> == VMFault v0 v1"
|
||||
|
||||
lemma vmFaultAddress_vmFaultAddress_update [simp]:
|
||||
"vmFaultAddress (vmFaultAddress_update f v) = f (vmFaultAddress v)"
|
||||
by (cases v) simp
|
||||
|
||||
lemma vmFaultAddress_vmFaultArchData_update [simp]:
|
||||
"vmFaultAddress (vmFaultArchData_update f v) = vmFaultAddress v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma vmFaultArchData_vmFaultAddress_update [simp]:
|
||||
"vmFaultArchData (vmFaultAddress_update f v) = vmFaultArchData v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma vmFaultArchData_vmFaultArchData_update [simp]:
|
||||
"vmFaultArchData (vmFaultArchData_update f v) = f (vmFaultArchData v)"
|
||||
by (cases v) simp
|
||||
|
||||
|
||||
end
|
||||
end
|
||||
|
|
@ -1,35 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file ArchHypervisor_H.thy *)
|
||||
(*
|
||||
* Copyright 2016, Data61, CSIRO
|
||||
*
|
||||
* 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(DATA61_GPL)
|
||||
*)
|
||||
|
||||
(*
|
||||
Hypervisor stub for X64
|
||||
*)
|
||||
|
||||
theory ArchHypervisor_H
|
||||
imports
|
||||
"../CNode_H"
|
||||
"../KI_Decls_H"
|
||||
begin
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
|
||||
consts'
|
||||
handleHypervisorFault :: "machine_word \<Rightarrow> hyp_fault_type \<Rightarrow> unit kernel"
|
||||
|
||||
defs handleHypervisorFault_def:
|
||||
"handleHypervisorFault x0 x1\<equiv> (let hyp = x1 in
|
||||
case hyp of X64NoHypFaults => return ()
|
||||
)"
|
||||
|
||||
|
||||
end
|
||||
end
|
||||
|
|
@ -1,37 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file ArchInterruptDecls_H.thy *)
|
||||
(*
|
||||
* Copyright 2014, General Dynamics C4 Systems
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_GPLv2.txt" for details.
|
||||
*
|
||||
* @TAG(GD_GPL)
|
||||
*)
|
||||
|
||||
theory ArchInterruptDecls_H
|
||||
imports "../RetypeDecls_H" "../CNode_H"
|
||||
begin
|
||||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
consts'
|
||||
decodeIRQControlInvocation :: "machine_word \<Rightarrow> machine_word list \<Rightarrow> machine_word \<Rightarrow> capability list \<Rightarrow> ( syscall_error , irqcontrol_invocation ) kernel_f"
|
||||
|
||||
consts'
|
||||
performIRQControl :: "irqcontrol_invocation \<Rightarrow> unit kernel_p"
|
||||
|
||||
consts'
|
||||
checkIRQ :: "machine_word \<Rightarrow> ( syscall_error , unit ) kernel_f"
|
||||
|
||||
consts'
|
||||
handleReservedIRQ :: "irq \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
initInterruptController :: "unit kernel"
|
||||
|
||||
|
||||
end (* context X64 *)
|
||||
|
||||
end
|
||||
|
|
@ -1,92 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file ArchInterrupt_H.thy *)
|
||||
(*
|
||||
* Copyright 2014, General Dynamics C4 Systems
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_GPLv2.txt" for details.
|
||||
*
|
||||
* @TAG(GD_GPL)
|
||||
*)
|
||||
|
||||
theory ArchInterrupt_H
|
||||
imports "../RetypeDecls_H" "../CNode_H" "../InterruptDecls_H" ArchInterruptDecls_H
|
||||
begin
|
||||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
defs decodeIRQControlInvocation_def:
|
||||
"decodeIRQControlInvocation label args srcSlot extraCaps \<equiv>
|
||||
(let (label, args, extraCaps) = (invocationType label, args, extraCaps) in
|
||||
case (label, args, extraCaps) of
|
||||
(ArchInvocationLabel X64IRQIssueIRQHandlerIOAPIC,
|
||||
index#depth#ioapic#pin#level#polarity#irqW#_, cnode#_) => (doE
|
||||
rangeCheck irqW (fromEnum minIRQ) (fromEnum maxIRQ);
|
||||
irq \<leftarrow> returnOk ( toEnum (fromIntegral irqW) ::irq);
|
||||
irqActive \<leftarrow> withoutFailure $ isIRQActive irq;
|
||||
whenE irqActive $ throw RevokeFirst;
|
||||
destSlot \<leftarrow> lookupTargetSlot cnode (CPtr index)
|
||||
(fromIntegral depth);
|
||||
ensureEmptySlot destSlot;
|
||||
rangeCheck ioapic 0 (numIOAPICs - 1);
|
||||
rangeCheck pin 0 (ioapicIRQLines - 1);
|
||||
rangeCheck level (0::machine_word) 1;
|
||||
rangeCheck polarity (0::machine_word) 1;
|
||||
vector \<leftarrow> returnOk ( (fromIntegral $ fromEnum irq) + irqIntOffset);
|
||||
returnOk $ IssueIRQHandlerIOAPIC irq destSlot srcSlot ioapic
|
||||
pin level polarity vector
|
||||
odE)
|
||||
| (ArchInvocationLabel X64IRQIssueIRQHandlerIOAPIC, _, _) => throw TruncatedMessage
|
||||
| (ArchInvocationLabel X64IRQIssueIRQHandlerMSI,
|
||||
index#depth#pciBus#pciDev#pciFunc#handle#irqW#_, cnode#_) => (doE
|
||||
rangeCheck irqW (fromEnum minIRQ) (fromEnum maxIRQ);
|
||||
irq \<leftarrow> returnOk ( toEnum (fromIntegral irqW) ::irq);
|
||||
irqActive \<leftarrow> withoutFailure $ isIRQActive irq;
|
||||
whenE irqActive $ throw RevokeFirst;
|
||||
destSlot \<leftarrow> lookupTargetSlot cnode (CPtr index)
|
||||
(fromIntegral depth);
|
||||
ensureEmptySlot destSlot;
|
||||
rangeCheck pciBus 0 maxPCIBus;
|
||||
rangeCheck pciDev 0 maxPCIDev;
|
||||
rangeCheck pciFunc 0 maxPCIFunc;
|
||||
returnOk $ IssueIRQHandlerMSI irq destSlot srcSlot pciBus
|
||||
pciDev pciFunc handle
|
||||
odE)
|
||||
| (ArchInvocationLabel X64IRQIssueIRQHandlerMSI, _, _) => throw TruncatedMessage
|
||||
| _ => throw IllegalOperation
|
||||
)"
|
||||
|
||||
defs performIRQControl_def:
|
||||
"performIRQControl x0\<equiv> (let inv = x0 in
|
||||
case inv of
|
||||
(IssueIRQHandlerIOAPIC irq destSlot srcSlot ioapic pin level polarity vector) => withoutPreemption $ (do
|
||||
doMachineOp $ ioapicMapPinToVector ioapic pin level polarity vector;
|
||||
irqState \<leftarrow> return $ IRQIOAPIC ioapic pin level polarity True;
|
||||
doMachineOp $ updateIRQState irq irqState;
|
||||
setIRQState IRQSignal (IRQ irq);
|
||||
cteInsert (IRQHandlerCap (IRQ irq)) srcSlot destSlot;
|
||||
return ()
|
||||
od)
|
||||
| (IssueIRQHandlerMSI irq destSlot srcSlot pciBus pciDev pciFunc handle) => withoutPreemption $ (do
|
||||
irqState \<leftarrow> return $ IRQMSI pciBus pciDev pciFunc handle;
|
||||
doMachineOp $ updateIRQState irq irqState;
|
||||
setIRQState IRQSignal (IRQ irq);
|
||||
cteInsert (IRQHandlerCap (IRQ irq)) srcSlot destSlot;
|
||||
return ()
|
||||
od)
|
||||
)"
|
||||
|
||||
defs checkIRQ_def:
|
||||
"checkIRQ irq\<equiv> rangeCheck irq (fromEnum minIRQ) (fromEnum maxIRQ)"
|
||||
|
||||
defs handleReservedIRQ_def:
|
||||
"handleReservedIRQ arg1 \<equiv> return ()"
|
||||
|
||||
defs initInterruptController_def:
|
||||
"initInterruptController\<equiv> return ()"
|
||||
|
||||
|
||||
end
|
||||
|
||||
end
|
||||
|
|
@ -1,130 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file ArchInvocationLabels_H.thy *)
|
||||
(*
|
||||
* 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 "Architecture-specific Invocation Labels"
|
||||
|
||||
theory ArchInvocationLabels_H
|
||||
imports
|
||||
"../../../lib/Word_Lib/Enumeration"
|
||||
"../../machine/Setup_Locale"
|
||||
begin
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
text {*
|
||||
An enumeration of arch-specific system call labels.
|
||||
*}
|
||||
|
||||
datatype arch_invocation_label =
|
||||
X64PDPTMap
|
||||
| X64PDPTUnmap
|
||||
| X64PageDirectoryMap
|
||||
| X64PageDirectoryUnmap
|
||||
| X64PageTableMap
|
||||
| X64PageTableUnmap
|
||||
| X64IOPageTableMap
|
||||
| X64IOPageTableUnmap
|
||||
| X64PageMap
|
||||
| X64PageRemap
|
||||
| X64PageUnmap
|
||||
| X64PageMapIO
|
||||
| X64PageGetAddress
|
||||
| X64ASIDControlMakePool
|
||||
| X64ASIDPoolAssign
|
||||
| X64IOPortIn8
|
||||
| X64IOPortIn16
|
||||
| X64IOPortIn32
|
||||
| X64IOPortOut8
|
||||
| X64IOPortOut16
|
||||
| X64IOPortOut32
|
||||
| X64IRQIssueIRQHandlerIOAPIC
|
||||
| X64IRQIssueIRQHandlerMSI
|
||||
|
||||
|
||||
end
|
||||
|
||||
context begin interpretation Arch .
|
||||
requalify_types arch_invocation_label
|
||||
end
|
||||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
end
|
||||
qualify X64_H (in Arch)
|
||||
(* arch_invocation_label instance proofs *)
|
||||
(*<*)
|
||||
instantiation arch_invocation_label :: enum begin
|
||||
interpretation Arch .
|
||||
definition
|
||||
enum_arch_invocation_label: "enum_class.enum \<equiv>
|
||||
[
|
||||
X64PDPTMap,
|
||||
X64PDPTUnmap,
|
||||
X64PageDirectoryMap,
|
||||
X64PageDirectoryUnmap,
|
||||
X64PageTableMap,
|
||||
X64PageTableUnmap,
|
||||
X64IOPageTableMap,
|
||||
X64IOPageTableUnmap,
|
||||
X64PageMap,
|
||||
X64PageRemap,
|
||||
X64PageUnmap,
|
||||
X64PageMapIO,
|
||||
X64PageGetAddress,
|
||||
X64ASIDControlMakePool,
|
||||
X64ASIDPoolAssign,
|
||||
X64IOPortIn8,
|
||||
X64IOPortIn16,
|
||||
X64IOPortIn32,
|
||||
X64IOPortOut8,
|
||||
X64IOPortOut16,
|
||||
X64IOPortOut32,
|
||||
X64IRQIssueIRQHandlerIOAPIC,
|
||||
X64IRQIssueIRQHandlerMSI
|
||||
]"
|
||||
|
||||
|
||||
definition
|
||||
"enum_class.enum_all (P :: arch_invocation_label \<Rightarrow> bool) \<longleftrightarrow> Ball UNIV P"
|
||||
|
||||
definition
|
||||
"enum_class.enum_ex (P :: arch_invocation_label \<Rightarrow> bool) \<longleftrightarrow> Bex UNIV P"
|
||||
|
||||
instance
|
||||
apply intro_classes
|
||||
apply (safe, simp)
|
||||
apply (case_tac x)
|
||||
apply (simp_all add: enum_arch_invocation_label enum_all_arch_invocation_label_def enum_ex_arch_invocation_label_def)
|
||||
by fast+
|
||||
end
|
||||
|
||||
instantiation arch_invocation_label :: enum_alt
|
||||
begin
|
||||
interpretation Arch .
|
||||
definition
|
||||
enum_alt_arch_invocation_label: "enum_alt \<equiv>
|
||||
alt_from_ord (enum :: arch_invocation_label list)"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation arch_invocation_label :: enumeration_both
|
||||
begin
|
||||
interpretation Arch .
|
||||
instance by (intro_classes, simp add: enum_alt_arch_invocation_label)
|
||||
end
|
||||
|
||||
(*>*)
|
||||
end_qualify
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
|
||||
end
|
||||
end
|
||||
|
|
@ -1,25 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file ArchLabelFuns_H.thy *)
|
||||
(*
|
||||
* 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 "Architecture-specific Invocation Label Functions"
|
||||
|
||||
theory ArchLabelFuns_H
|
||||
imports "../InvocationLabels_H"
|
||||
begin
|
||||
|
||||
text {*
|
||||
Arch-specific functions on invocation labels
|
||||
*}
|
||||
|
||||
(* None for x64 *)
|
||||
|
||||
end
|
||||
|
|
@ -1,320 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file ArchObjInsts_H.thy *)
|
||||
(*
|
||||
* 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)
|
||||
*)
|
||||
|
||||
(*
|
||||
Defines the instances of pspace_storable objects.
|
||||
*)
|
||||
|
||||
chapter "Storable Arch Object Instances"
|
||||
|
||||
theory ArchObjInsts_H
|
||||
imports
|
||||
ArchTypes_H
|
||||
"../PSpaceStorable_H"
|
||||
"../ObjectInstances_H"
|
||||
begin
|
||||
qualify X64_H (in Arch)
|
||||
|
||||
instantiation X64_H.pde :: pre_storable
|
||||
begin
|
||||
interpretation Arch .
|
||||
|
||||
definition
|
||||
projectKO_opt_pde:
|
||||
"projectKO_opt e \<equiv> case e of KOArch (KOPDE e) \<Rightarrow> Some e | _ \<Rightarrow> None"
|
||||
|
||||
definition
|
||||
injectKO_pde [simp]:
|
||||
"injectKO e \<equiv> KOArch (KOPDE e)"
|
||||
|
||||
definition
|
||||
koType_pde [simp]:
|
||||
"koType (t::pde itself) \<equiv> ArchT PDET"
|
||||
|
||||
instance
|
||||
by (intro_classes,
|
||||
auto simp: projectKO_opt_pde split: kernel_object.splits arch_kernel_object.splits)
|
||||
|
||||
end
|
||||
|
||||
|
||||
instantiation X64_H.pte :: pre_storable
|
||||
begin
|
||||
interpretation Arch .
|
||||
|
||||
definition
|
||||
projectKO_opt_pte:
|
||||
"projectKO_opt e \<equiv> case e of (KOArch (KOPTE e)) \<Rightarrow> Some e | _ \<Rightarrow> None"
|
||||
|
||||
definition
|
||||
injectKO_pte [simp]:
|
||||
"injectKO e \<equiv> KOArch (KOPTE e)"
|
||||
|
||||
definition
|
||||
koType_pte [simp]:
|
||||
"koType (t::pte itself) \<equiv> ArchT PTET"
|
||||
|
||||
instance
|
||||
by (intro_classes,
|
||||
auto simp: projectKO_opt_pte split: kernel_object.splits arch_kernel_object.splits)
|
||||
|
||||
end
|
||||
|
||||
instantiation X64_H.pdpte :: pre_storable
|
||||
begin
|
||||
interpretation Arch .
|
||||
|
||||
definition
|
||||
projectKO_opt_pdpte:
|
||||
"projectKO_opt e \<equiv> case e of (KOArch (KOPDPTE e)) \<Rightarrow> Some e | _ \<Rightarrow> None"
|
||||
|
||||
definition
|
||||
injectKO_pdpte [simp]:
|
||||
"injectKO e \<equiv> KOArch (KOPDPTE e)"
|
||||
|
||||
definition
|
||||
koType_pdpte [simp]:
|
||||
"koType (t::pdpte itself) \<equiv> ArchT PDPTET"
|
||||
|
||||
instance
|
||||
by (intro_classes,
|
||||
auto simp: projectKO_opt_pdpte split: kernel_object.splits arch_kernel_object.splits)
|
||||
|
||||
end
|
||||
|
||||
instantiation X64_H.pml4e :: pre_storable
|
||||
begin
|
||||
interpretation Arch .
|
||||
|
||||
definition
|
||||
projectKO_opt_pml4e:
|
||||
"projectKO_opt e \<equiv> case e of (KOArch (KOPML4E e)) \<Rightarrow> Some e | _ \<Rightarrow> None"
|
||||
|
||||
definition
|
||||
injectKO_pml4e [simp]:
|
||||
"injectKO e \<equiv> KOArch (KOPML4E e)"
|
||||
|
||||
definition
|
||||
koType_pml4e [simp]:
|
||||
"koType (t::pml4e itself) \<equiv> ArchT PML4ET"
|
||||
|
||||
instance
|
||||
by (intro_classes,
|
||||
auto simp: projectKO_opt_pml4e split: kernel_object.splits arch_kernel_object.splits)
|
||||
|
||||
end
|
||||
|
||||
instantiation X64_H.asidpool :: pre_storable
|
||||
begin
|
||||
interpretation Arch .
|
||||
|
||||
definition
|
||||
injectKO_asidpool [simp]:
|
||||
"injectKO e \<equiv> KOArch (KOASIDPool e)"
|
||||
|
||||
definition
|
||||
koType_asidpool [simp]:
|
||||
"koType (t::asidpool itself) \<equiv> ArchT ASIDPoolT"
|
||||
|
||||
definition
|
||||
projectKO_opt_asidpool:
|
||||
"projectKO_opt e \<equiv> case e of (KOArch (KOASIDPool e)) \<Rightarrow> Some e | _ \<Rightarrow> None"
|
||||
|
||||
instance
|
||||
by (intro_classes,
|
||||
auto simp: projectKO_opt_asidpool split: kernel_object.splits arch_kernel_object.splits)
|
||||
|
||||
end
|
||||
|
||||
lemmas (in Arch) projectKO_opts_defs =
|
||||
projectKO_opt_pte projectKO_opt_pde
|
||||
projectKO_opt_pdpte projectKO_opt_pml4e
|
||||
projectKO_opt_asidpool
|
||||
ObjectInstances_H.projectKO_opts_defs
|
||||
|
||||
lemmas (in Arch) [simp] =
|
||||
injectKO_pte koType_pte
|
||||
injectKO_pde koType_pde
|
||||
injectKO_pdpte koType_pdpte
|
||||
injectKO_pml4e koType_pml4e
|
||||
injectKO_asidpool koType_asidpool
|
||||
|
||||
|
||||
-- --------------------------------------
|
||||
|
||||
|
||||
|
||||
|
||||
instantiation X64_H.pde :: pspace_storable
|
||||
begin
|
||||
interpretation Arch .
|
||||
|
||||
(* pde extra instance defs *)
|
||||
|
||||
|
||||
definition
|
||||
makeObject_pde: "(makeObject :: pde) \<equiv> InvalidPDE"
|
||||
|
||||
definition
|
||||
loadObject_pde[simp]:
|
||||
"(loadObject p q n obj) :: pde kernel \<equiv>
|
||||
loadObject_default p q n obj"
|
||||
|
||||
definition
|
||||
updateObject_pde[simp]:
|
||||
"updateObject (val :: pde) \<equiv>
|
||||
updateObject_default val"
|
||||
|
||||
|
||||
instance
|
||||
apply (intro_classes)
|
||||
apply (clarsimp simp add: updateObject_default_def in_monad projectKO_opts_defs
|
||||
projectKO_eq2
|
||||
split: kernel_object.splits arch_kernel_object.splits)
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
instantiation X64_H.pte :: pspace_storable
|
||||
begin
|
||||
interpretation Arch .
|
||||
|
||||
(* pte extra instance defs *)
|
||||
|
||||
|
||||
definition
|
||||
makeObject_pte: "(makeObject :: pte) \<equiv> InvalidPTE"
|
||||
|
||||
definition
|
||||
loadObject_pte[simp]:
|
||||
"(loadObject p q n obj) :: pte kernel \<equiv>
|
||||
loadObject_default p q n obj"
|
||||
|
||||
definition
|
||||
updateObject_pte[simp]:
|
||||
"updateObject (val :: pte) \<equiv>
|
||||
updateObject_default val"
|
||||
|
||||
|
||||
instance
|
||||
apply (intro_classes)
|
||||
apply (clarsimp simp add: updateObject_default_def in_monad projectKO_opts_defs
|
||||
projectKO_eq2
|
||||
split: kernel_object.splits arch_kernel_object.splits)
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
|
||||
instantiation X64_H.pdpte :: pspace_storable
|
||||
begin
|
||||
interpretation Arch .
|
||||
|
||||
(* pdpte extra instance defs *)
|
||||
|
||||
|
||||
definition
|
||||
makeObject_pdpte: "(makeObject :: pdpte) \<equiv> InvalidPDPTE"
|
||||
|
||||
definition
|
||||
loadObject_pdpte[simp]:
|
||||
"(loadObject p q n obj) :: pdpte kernel \<equiv>
|
||||
loadObject_default p q n obj"
|
||||
|
||||
definition
|
||||
updateObject_pdpte[simp]:
|
||||
"updateObject (val :: pdpte) \<equiv>
|
||||
updateObject_default val"
|
||||
|
||||
|
||||
instance
|
||||
apply (intro_classes)
|
||||
apply (clarsimp simp add: updateObject_default_def in_monad projectKO_opts_defs
|
||||
projectKO_eq2
|
||||
split: kernel_object.splits arch_kernel_object.splits)
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
instantiation X64_H.pml4e :: pspace_storable
|
||||
begin
|
||||
interpretation Arch .
|
||||
|
||||
(* pml4e extra instance defs *)
|
||||
|
||||
|
||||
definition
|
||||
makeObject_pml4e: "(makeObject :: pml4e) \<equiv> InvalidPML4E"
|
||||
|
||||
definition
|
||||
loadObject_pml4e[simp]:
|
||||
"(loadObject p q n obj) :: pml4e kernel \<equiv>
|
||||
loadObject_default p q n obj"
|
||||
|
||||
definition
|
||||
updateObject_pml4e[simp]:
|
||||
"updateObject (val :: pml4e) \<equiv>
|
||||
updateObject_default val"
|
||||
|
||||
|
||||
instance
|
||||
apply (intro_classes)
|
||||
apply (clarsimp simp add: updateObject_default_def in_monad projectKO_opts_defs
|
||||
projectKO_eq2
|
||||
split: kernel_object.splits arch_kernel_object.splits)
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
(* This is hard coded since using funArray in haskell for 2^32 bound is risky *)
|
||||
|
||||
instantiation X64_H.asidpool :: pspace_storable
|
||||
begin
|
||||
interpretation Arch .
|
||||
|
||||
definition
|
||||
makeObject_asidpool: "(makeObject :: asidpool) \<equiv> ASIDPool $
|
||||
funArray (const Nothing)"
|
||||
|
||||
definition
|
||||
loadObject_asidpool[simp]:
|
||||
"(loadObject p q n obj) :: asidpool kernel \<equiv>
|
||||
loadObject_default p q n obj"
|
||||
|
||||
definition
|
||||
updateObject_asidpool[simp]:
|
||||
"updateObject (val :: asidpool) \<equiv>
|
||||
updateObject_default val"
|
||||
|
||||
instance
|
||||
apply (intro_classes)
|
||||
apply (clarsimp simp add: updateObject_default_def in_monad projectKO_opts_defs
|
||||
projectKO_eq2
|
||||
split: kernel_object.splits arch_kernel_object.splits)
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
lemmas load_update_defs =
|
||||
loadObject_pte updateObject_pte
|
||||
loadObject_pde updateObject_pde
|
||||
loadObject_pdpte updateObject_pdpte
|
||||
loadObject_pml4e updateObject_pml4e
|
||||
loadObject_asidpool updateObject_asidpool
|
||||
|
||||
declare load_update_defs[simp del]
|
||||
|
||||
end_qualify
|
||||
|
||||
declare (in Arch) load_update_defs[simp]
|
||||
|
||||
end
|
||||
|
|
@ -1,917 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file ArchRetypeDecls_H.thy *)
|
||||
(*
|
||||
* 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 "Retyping Objects"
|
||||
|
||||
theory ArchRetypeDecls_H
|
||||
imports
|
||||
"../FaultMonad_H"
|
||||
"../EndpointDecls_H"
|
||||
"../KernelInitMonad_H"
|
||||
"../PSpaceFuns_H"
|
||||
ArchObjInsts_H
|
||||
begin
|
||||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
datatype pdptinvocation =
|
||||
PDPTUnmap arch_capability machine_word
|
||||
| PDPTMap capability machine_word pml4e machine_word machine_word
|
||||
|
||||
primrec
|
||||
pdptMapCap :: "pdptinvocation \<Rightarrow> capability"
|
||||
where
|
||||
"pdptMapCap (PDPTMap v0 v1 v2 v3 v4) = v0"
|
||||
|
||||
primrec
|
||||
pdptMapPML4Slot :: "pdptinvocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"pdptMapPML4Slot (PDPTMap v0 v1 v2 v3 v4) = v3"
|
||||
|
||||
primrec
|
||||
pdptUnmapCap :: "pdptinvocation \<Rightarrow> arch_capability"
|
||||
where
|
||||
"pdptUnmapCap (PDPTUnmap v0 v1) = v0"
|
||||
|
||||
primrec
|
||||
pdptMapCTSlot :: "pdptinvocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"pdptMapCTSlot (PDPTMap v0 v1 v2 v3 v4) = v1"
|
||||
|
||||
primrec
|
||||
pdptMapVSpace :: "pdptinvocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"pdptMapVSpace (PDPTMap v0 v1 v2 v3 v4) = v4"
|
||||
|
||||
primrec
|
||||
pdptMapPML4E :: "pdptinvocation \<Rightarrow> pml4e"
|
||||
where
|
||||
"pdptMapPML4E (PDPTMap v0 v1 v2 v3 v4) = v2"
|
||||
|
||||
primrec
|
||||
pdptUnmapCapSlot :: "pdptinvocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"pdptUnmapCapSlot (PDPTUnmap v0 v1) = v1"
|
||||
|
||||
primrec
|
||||
pdptMapCap_update :: "(capability \<Rightarrow> capability) \<Rightarrow> pdptinvocation \<Rightarrow> pdptinvocation"
|
||||
where
|
||||
"pdptMapCap_update f (PDPTMap v0 v1 v2 v3 v4) = PDPTMap (f v0) v1 v2 v3 v4"
|
||||
|
||||
primrec
|
||||
pdptMapPML4Slot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> pdptinvocation \<Rightarrow> pdptinvocation"
|
||||
where
|
||||
"pdptMapPML4Slot_update f (PDPTMap v0 v1 v2 v3 v4) = PDPTMap v0 v1 v2 (f v3) v4"
|
||||
|
||||
primrec
|
||||
pdptUnmapCap_update :: "(arch_capability \<Rightarrow> arch_capability) \<Rightarrow> pdptinvocation \<Rightarrow> pdptinvocation"
|
||||
where
|
||||
"pdptUnmapCap_update f (PDPTUnmap v0 v1) = PDPTUnmap (f v0) v1"
|
||||
|
||||
primrec
|
||||
pdptMapCTSlot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> pdptinvocation \<Rightarrow> pdptinvocation"
|
||||
where
|
||||
"pdptMapCTSlot_update f (PDPTMap v0 v1 v2 v3 v4) = PDPTMap v0 (f v1) v2 v3 v4"
|
||||
|
||||
primrec
|
||||
pdptMapVSpace_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> pdptinvocation \<Rightarrow> pdptinvocation"
|
||||
where
|
||||
"pdptMapVSpace_update f (PDPTMap v0 v1 v2 v3 v4) = PDPTMap v0 v1 v2 v3 (f v4)"
|
||||
|
||||
primrec
|
||||
pdptMapPML4E_update :: "(pml4e \<Rightarrow> pml4e) \<Rightarrow> pdptinvocation \<Rightarrow> pdptinvocation"
|
||||
where
|
||||
"pdptMapPML4E_update f (PDPTMap v0 v1 v2 v3 v4) = PDPTMap v0 v1 (f v2) v3 v4"
|
||||
|
||||
primrec
|
||||
pdptUnmapCapSlot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> pdptinvocation \<Rightarrow> pdptinvocation"
|
||||
where
|
||||
"pdptUnmapCapSlot_update f (PDPTUnmap v0 v1) = PDPTUnmap v0 (f v1)"
|
||||
|
||||
abbreviation (input)
|
||||
PDPTUnmap_trans :: "(arch_capability) \<Rightarrow> (machine_word) \<Rightarrow> pdptinvocation" ("PDPTUnmap'_ \<lparr> pdptUnmapCap= _, pdptUnmapCapSlot= _ \<rparr>")
|
||||
where
|
||||
"PDPTUnmap_ \<lparr> pdptUnmapCap= v0, pdptUnmapCapSlot= v1 \<rparr> == PDPTUnmap v0 v1"
|
||||
|
||||
abbreviation (input)
|
||||
PDPTMap_trans :: "(capability) \<Rightarrow> (machine_word) \<Rightarrow> (pml4e) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> pdptinvocation" ("PDPTMap'_ \<lparr> pdptMapCap= _, pdptMapCTSlot= _, pdptMapPML4E= _, pdptMapPML4Slot= _, pdptMapVSpace= _ \<rparr>")
|
||||
where
|
||||
"PDPTMap_ \<lparr> pdptMapCap= v0, pdptMapCTSlot= v1, pdptMapPML4E= v2, pdptMapPML4Slot= v3, pdptMapVSpace= v4 \<rparr> == PDPTMap v0 v1 v2 v3 v4"
|
||||
|
||||
definition
|
||||
isPDPTUnmap :: "pdptinvocation \<Rightarrow> bool"
|
||||
where
|
||||
"isPDPTUnmap v \<equiv> case v of
|
||||
PDPTUnmap v0 v1 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isPDPTMap :: "pdptinvocation \<Rightarrow> bool"
|
||||
where
|
||||
"isPDPTMap v \<equiv> case v of
|
||||
PDPTMap v0 v1 v2 v3 v4 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
datatype page_directory_invocation =
|
||||
PageDirectoryUnmap arch_capability machine_word
|
||||
| PageDirectoryMap capability machine_word pdpte machine_word machine_word
|
||||
|
||||
primrec
|
||||
pdMapCTSlot :: "page_directory_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"pdMapCTSlot (PageDirectoryMap v0 v1 v2 v3 v4) = v1"
|
||||
|
||||
primrec
|
||||
pdUnmapCap :: "page_directory_invocation \<Rightarrow> arch_capability"
|
||||
where
|
||||
"pdUnmapCap (PageDirectoryUnmap v0 v1) = v0"
|
||||
|
||||
primrec
|
||||
pdMapVSpace :: "page_directory_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"pdMapVSpace (PageDirectoryMap v0 v1 v2 v3 v4) = v4"
|
||||
|
||||
primrec
|
||||
pdMapPDPTE :: "page_directory_invocation \<Rightarrow> pdpte"
|
||||
where
|
||||
"pdMapPDPTE (PageDirectoryMap v0 v1 v2 v3 v4) = v2"
|
||||
|
||||
primrec
|
||||
pdMapCap :: "page_directory_invocation \<Rightarrow> capability"
|
||||
where
|
||||
"pdMapCap (PageDirectoryMap v0 v1 v2 v3 v4) = v0"
|
||||
|
||||
primrec
|
||||
pdMapPDPTSlot :: "page_directory_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"pdMapPDPTSlot (PageDirectoryMap v0 v1 v2 v3 v4) = v3"
|
||||
|
||||
primrec
|
||||
pdUnmapCapSlot :: "page_directory_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"pdUnmapCapSlot (PageDirectoryUnmap v0 v1) = v1"
|
||||
|
||||
primrec
|
||||
pdMapCTSlot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> page_directory_invocation \<Rightarrow> page_directory_invocation"
|
||||
where
|
||||
"pdMapCTSlot_update f (PageDirectoryMap v0 v1 v2 v3 v4) = PageDirectoryMap v0 (f v1) v2 v3 v4"
|
||||
|
||||
primrec
|
||||
pdUnmapCap_update :: "(arch_capability \<Rightarrow> arch_capability) \<Rightarrow> page_directory_invocation \<Rightarrow> page_directory_invocation"
|
||||
where
|
||||
"pdUnmapCap_update f (PageDirectoryUnmap v0 v1) = PageDirectoryUnmap (f v0) v1"
|
||||
|
||||
primrec
|
||||
pdMapVSpace_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> page_directory_invocation \<Rightarrow> page_directory_invocation"
|
||||
where
|
||||
"pdMapVSpace_update f (PageDirectoryMap v0 v1 v2 v3 v4) = PageDirectoryMap v0 v1 v2 v3 (f v4)"
|
||||
|
||||
primrec
|
||||
pdMapPDPTE_update :: "(pdpte \<Rightarrow> pdpte) \<Rightarrow> page_directory_invocation \<Rightarrow> page_directory_invocation"
|
||||
where
|
||||
"pdMapPDPTE_update f (PageDirectoryMap v0 v1 v2 v3 v4) = PageDirectoryMap v0 v1 (f v2) v3 v4"
|
||||
|
||||
primrec
|
||||
pdMapCap_update :: "(capability \<Rightarrow> capability) \<Rightarrow> page_directory_invocation \<Rightarrow> page_directory_invocation"
|
||||
where
|
||||
"pdMapCap_update f (PageDirectoryMap v0 v1 v2 v3 v4) = PageDirectoryMap (f v0) v1 v2 v3 v4"
|
||||
|
||||
primrec
|
||||
pdMapPDPTSlot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> page_directory_invocation \<Rightarrow> page_directory_invocation"
|
||||
where
|
||||
"pdMapPDPTSlot_update f (PageDirectoryMap v0 v1 v2 v3 v4) = PageDirectoryMap v0 v1 v2 (f v3) v4"
|
||||
|
||||
primrec
|
||||
pdUnmapCapSlot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> page_directory_invocation \<Rightarrow> page_directory_invocation"
|
||||
where
|
||||
"pdUnmapCapSlot_update f (PageDirectoryUnmap v0 v1) = PageDirectoryUnmap v0 (f v1)"
|
||||
|
||||
abbreviation (input)
|
||||
PageDirectoryUnmap_trans :: "(arch_capability) \<Rightarrow> (machine_word) \<Rightarrow> page_directory_invocation" ("PageDirectoryUnmap'_ \<lparr> pdUnmapCap= _, pdUnmapCapSlot= _ \<rparr>")
|
||||
where
|
||||
"PageDirectoryUnmap_ \<lparr> pdUnmapCap= v0, pdUnmapCapSlot= v1 \<rparr> == PageDirectoryUnmap v0 v1"
|
||||
|
||||
abbreviation (input)
|
||||
PageDirectoryMap_trans :: "(capability) \<Rightarrow> (machine_word) \<Rightarrow> (pdpte) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> page_directory_invocation" ("PageDirectoryMap'_ \<lparr> pdMapCap= _, pdMapCTSlot= _, pdMapPDPTE= _, pdMapPDPTSlot= _, pdMapVSpace= _ \<rparr>")
|
||||
where
|
||||
"PageDirectoryMap_ \<lparr> pdMapCap= v0, pdMapCTSlot= v1, pdMapPDPTE= v2, pdMapPDPTSlot= v3, pdMapVSpace= v4 \<rparr> == PageDirectoryMap v0 v1 v2 v3 v4"
|
||||
|
||||
definition
|
||||
isPageDirectoryUnmap :: "page_directory_invocation \<Rightarrow> bool"
|
||||
where
|
||||
"isPageDirectoryUnmap v \<equiv> case v of
|
||||
PageDirectoryUnmap v0 v1 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isPageDirectoryMap :: "page_directory_invocation \<Rightarrow> bool"
|
||||
where
|
||||
"isPageDirectoryMap v \<equiv> case v of
|
||||
PageDirectoryMap v0 v1 v2 v3 v4 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
datatype page_table_invocation =
|
||||
PageTableUnmap arch_capability machine_word
|
||||
| PageTableMap capability machine_word pde machine_word machine_word
|
||||
|
||||
primrec
|
||||
ptMapPDSlot :: "page_table_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"ptMapPDSlot (PageTableMap v0 v1 v2 v3 v4) = v3"
|
||||
|
||||
primrec
|
||||
ptUnmapCapSlot :: "page_table_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"ptUnmapCapSlot (PageTableUnmap v0 v1) = v1"
|
||||
|
||||
primrec
|
||||
ptMapCTSlot :: "page_table_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"ptMapCTSlot (PageTableMap v0 v1 v2 v3 v4) = v1"
|
||||
|
||||
primrec
|
||||
ptMapVSpace :: "page_table_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"ptMapVSpace (PageTableMap v0 v1 v2 v3 v4) = v4"
|
||||
|
||||
primrec
|
||||
ptUnmapCap :: "page_table_invocation \<Rightarrow> arch_capability"
|
||||
where
|
||||
"ptUnmapCap (PageTableUnmap v0 v1) = v0"
|
||||
|
||||
primrec
|
||||
ptMapPDE :: "page_table_invocation \<Rightarrow> pde"
|
||||
where
|
||||
"ptMapPDE (PageTableMap v0 v1 v2 v3 v4) = v2"
|
||||
|
||||
primrec
|
||||
ptMapCap :: "page_table_invocation \<Rightarrow> capability"
|
||||
where
|
||||
"ptMapCap (PageTableMap v0 v1 v2 v3 v4) = v0"
|
||||
|
||||
primrec
|
||||
ptMapPDSlot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> page_table_invocation \<Rightarrow> page_table_invocation"
|
||||
where
|
||||
"ptMapPDSlot_update f (PageTableMap v0 v1 v2 v3 v4) = PageTableMap v0 v1 v2 (f v3) v4"
|
||||
|
||||
primrec
|
||||
ptUnmapCapSlot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> page_table_invocation \<Rightarrow> page_table_invocation"
|
||||
where
|
||||
"ptUnmapCapSlot_update f (PageTableUnmap v0 v1) = PageTableUnmap v0 (f v1)"
|
||||
|
||||
primrec
|
||||
ptMapCTSlot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> page_table_invocation \<Rightarrow> page_table_invocation"
|
||||
where
|
||||
"ptMapCTSlot_update f (PageTableMap v0 v1 v2 v3 v4) = PageTableMap v0 (f v1) v2 v3 v4"
|
||||
|
||||
primrec
|
||||
ptMapVSpace_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> page_table_invocation \<Rightarrow> page_table_invocation"
|
||||
where
|
||||
"ptMapVSpace_update f (PageTableMap v0 v1 v2 v3 v4) = PageTableMap v0 v1 v2 v3 (f v4)"
|
||||
|
||||
primrec
|
||||
ptUnmapCap_update :: "(arch_capability \<Rightarrow> arch_capability) \<Rightarrow> page_table_invocation \<Rightarrow> page_table_invocation"
|
||||
where
|
||||
"ptUnmapCap_update f (PageTableUnmap v0 v1) = PageTableUnmap (f v0) v1"
|
||||
|
||||
primrec
|
||||
ptMapPDE_update :: "(pde \<Rightarrow> pde) \<Rightarrow> page_table_invocation \<Rightarrow> page_table_invocation"
|
||||
where
|
||||
"ptMapPDE_update f (PageTableMap v0 v1 v2 v3 v4) = PageTableMap v0 v1 (f v2) v3 v4"
|
||||
|
||||
primrec
|
||||
ptMapCap_update :: "(capability \<Rightarrow> capability) \<Rightarrow> page_table_invocation \<Rightarrow> page_table_invocation"
|
||||
where
|
||||
"ptMapCap_update f (PageTableMap v0 v1 v2 v3 v4) = PageTableMap (f v0) v1 v2 v3 v4"
|
||||
|
||||
abbreviation (input)
|
||||
PageTableUnmap_trans :: "(arch_capability) \<Rightarrow> (machine_word) \<Rightarrow> page_table_invocation" ("PageTableUnmap'_ \<lparr> ptUnmapCap= _, ptUnmapCapSlot= _ \<rparr>")
|
||||
where
|
||||
"PageTableUnmap_ \<lparr> ptUnmapCap= v0, ptUnmapCapSlot= v1 \<rparr> == PageTableUnmap v0 v1"
|
||||
|
||||
abbreviation (input)
|
||||
PageTableMap_trans :: "(capability) \<Rightarrow> (machine_word) \<Rightarrow> (pde) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> page_table_invocation" ("PageTableMap'_ \<lparr> ptMapCap= _, ptMapCTSlot= _, ptMapPDE= _, ptMapPDSlot= _, ptMapVSpace= _ \<rparr>")
|
||||
where
|
||||
"PageTableMap_ \<lparr> ptMapCap= v0, ptMapCTSlot= v1, ptMapPDE= v2, ptMapPDSlot= v3, ptMapVSpace= v4 \<rparr> == PageTableMap v0 v1 v2 v3 v4"
|
||||
|
||||
definition
|
||||
isPageTableUnmap :: "page_table_invocation \<Rightarrow> bool"
|
||||
where
|
||||
"isPageTableUnmap v \<equiv> case v of
|
||||
PageTableUnmap v0 v1 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isPageTableMap :: "page_table_invocation \<Rightarrow> bool"
|
||||
where
|
||||
"isPageTableMap v \<equiv> case v of
|
||||
PageTableMap v0 v1 v2 v3 v4 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
datatype page_invocation =
|
||||
PageGetAddr machine_word
|
||||
| PageRemap "(vmpage_entry * vmpage_entry_ptr)" asid machine_word
|
||||
| PageMap capability machine_word "(vmpage_entry * vmpage_entry_ptr)" machine_word
|
||||
| PageUnmap arch_capability machine_word
|
||||
|
||||
primrec
|
||||
pageMapCap :: "page_invocation \<Rightarrow> capability"
|
||||
where
|
||||
"pageMapCap (PageMap v0 v1 v2 v3) = v0"
|
||||
|
||||
primrec
|
||||
pageUnmapCapSlot :: "page_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"pageUnmapCapSlot (PageUnmap v0 v1) = v1"
|
||||
|
||||
primrec
|
||||
pageUnmapCap :: "page_invocation \<Rightarrow> arch_capability"
|
||||
where
|
||||
"pageUnmapCap (PageUnmap v0 v1) = v0"
|
||||
|
||||
primrec
|
||||
pageMapVSpace :: "page_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"pageMapVSpace (PageMap v0 v1 v2 v3) = v3"
|
||||
|
||||
primrec
|
||||
pageRemapVSpace :: "page_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"pageRemapVSpace (PageRemap v0 v1 v2) = v2"
|
||||
|
||||
primrec
|
||||
pageRemapEntries :: "page_invocation \<Rightarrow> (vmpage_entry * vmpage_entry_ptr)"
|
||||
where
|
||||
"pageRemapEntries (PageRemap v0 v1 v2) = v0"
|
||||
|
||||
primrec
|
||||
pageMapCTSlot :: "page_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"pageMapCTSlot (PageMap v0 v1 v2 v3) = v1"
|
||||
|
||||
primrec
|
||||
pageGetBasePtr :: "page_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"pageGetBasePtr (PageGetAddr v0) = v0"
|
||||
|
||||
primrec
|
||||
pageMapEntries :: "page_invocation \<Rightarrow> (vmpage_entry * vmpage_entry_ptr)"
|
||||
where
|
||||
"pageMapEntries (PageMap v0 v1 v2 v3) = v2"
|
||||
|
||||
primrec
|
||||
pageRemapASID :: "page_invocation \<Rightarrow> asid"
|
||||
where
|
||||
"pageRemapASID (PageRemap v0 v1 v2) = v1"
|
||||
|
||||
primrec
|
||||
pageMapCap_update :: "(capability \<Rightarrow> capability) \<Rightarrow> page_invocation \<Rightarrow> page_invocation"
|
||||
where
|
||||
"pageMapCap_update f (PageMap v0 v1 v2 v3) = PageMap (f v0) v1 v2 v3"
|
||||
|
||||
primrec
|
||||
pageUnmapCapSlot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> page_invocation \<Rightarrow> page_invocation"
|
||||
where
|
||||
"pageUnmapCapSlot_update f (PageUnmap v0 v1) = PageUnmap v0 (f v1)"
|
||||
|
||||
primrec
|
||||
pageUnmapCap_update :: "(arch_capability \<Rightarrow> arch_capability) \<Rightarrow> page_invocation \<Rightarrow> page_invocation"
|
||||
where
|
||||
"pageUnmapCap_update f (PageUnmap v0 v1) = PageUnmap (f v0) v1"
|
||||
|
||||
primrec
|
||||
pageMapVSpace_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> page_invocation \<Rightarrow> page_invocation"
|
||||
where
|
||||
"pageMapVSpace_update f (PageMap v0 v1 v2 v3) = PageMap v0 v1 v2 (f v3)"
|
||||
|
||||
primrec
|
||||
pageRemapVSpace_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> page_invocation \<Rightarrow> page_invocation"
|
||||
where
|
||||
"pageRemapVSpace_update f (PageRemap v0 v1 v2) = PageRemap v0 v1 (f v2)"
|
||||
|
||||
primrec
|
||||
pageRemapEntries_update :: "(((vmpage_entry * vmpage_entry_ptr)) \<Rightarrow> ((vmpage_entry * vmpage_entry_ptr))) \<Rightarrow> page_invocation \<Rightarrow> page_invocation"
|
||||
where
|
||||
"pageRemapEntries_update f (PageRemap v0 v1 v2) = PageRemap (f v0) v1 v2"
|
||||
|
||||
primrec
|
||||
pageMapCTSlot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> page_invocation \<Rightarrow> page_invocation"
|
||||
where
|
||||
"pageMapCTSlot_update f (PageMap v0 v1 v2 v3) = PageMap v0 (f v1) v2 v3"
|
||||
|
||||
primrec
|
||||
pageGetBasePtr_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> page_invocation \<Rightarrow> page_invocation"
|
||||
where
|
||||
"pageGetBasePtr_update f (PageGetAddr v0) = PageGetAddr (f v0)"
|
||||
|
||||
primrec
|
||||
pageMapEntries_update :: "(((vmpage_entry * vmpage_entry_ptr)) \<Rightarrow> ((vmpage_entry * vmpage_entry_ptr))) \<Rightarrow> page_invocation \<Rightarrow> page_invocation"
|
||||
where
|
||||
"pageMapEntries_update f (PageMap v0 v1 v2 v3) = PageMap v0 v1 (f v2) v3"
|
||||
|
||||
primrec
|
||||
pageRemapASID_update :: "(asid \<Rightarrow> asid) \<Rightarrow> page_invocation \<Rightarrow> page_invocation"
|
||||
where
|
||||
"pageRemapASID_update f (PageRemap v0 v1 v2) = PageRemap v0 (f v1) v2"
|
||||
|
||||
abbreviation (input)
|
||||
PageGetAddr_trans :: "(machine_word) \<Rightarrow> page_invocation" ("PageGetAddr'_ \<lparr> pageGetBasePtr= _ \<rparr>")
|
||||
where
|
||||
"PageGetAddr_ \<lparr> pageGetBasePtr= v0 \<rparr> == PageGetAddr v0"
|
||||
|
||||
abbreviation (input)
|
||||
PageRemap_trans :: "((vmpage_entry * vmpage_entry_ptr)) \<Rightarrow> (asid) \<Rightarrow> (machine_word) \<Rightarrow> page_invocation" ("PageRemap'_ \<lparr> pageRemapEntries= _, pageRemapASID= _, pageRemapVSpace= _ \<rparr>")
|
||||
where
|
||||
"PageRemap_ \<lparr> pageRemapEntries= v0, pageRemapASID= v1, pageRemapVSpace= v2 \<rparr> == PageRemap v0 v1 v2"
|
||||
|
||||
abbreviation (input)
|
||||
PageMap_trans :: "(capability) \<Rightarrow> (machine_word) \<Rightarrow> ((vmpage_entry * vmpage_entry_ptr)) \<Rightarrow> (machine_word) \<Rightarrow> page_invocation" ("PageMap'_ \<lparr> pageMapCap= _, pageMapCTSlot= _, pageMapEntries= _, pageMapVSpace= _ \<rparr>")
|
||||
where
|
||||
"PageMap_ \<lparr> pageMapCap= v0, pageMapCTSlot= v1, pageMapEntries= v2, pageMapVSpace= v3 \<rparr> == PageMap v0 v1 v2 v3"
|
||||
|
||||
abbreviation (input)
|
||||
PageUnmap_trans :: "(arch_capability) \<Rightarrow> (machine_word) \<Rightarrow> page_invocation" ("PageUnmap'_ \<lparr> pageUnmapCap= _, pageUnmapCapSlot= _ \<rparr>")
|
||||
where
|
||||
"PageUnmap_ \<lparr> pageUnmapCap= v0, pageUnmapCapSlot= v1 \<rparr> == PageUnmap v0 v1"
|
||||
|
||||
definition
|
||||
isPageGetAddr :: "page_invocation \<Rightarrow> bool"
|
||||
where
|
||||
"isPageGetAddr v \<equiv> case v of
|
||||
PageGetAddr v0 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isPageRemap :: "page_invocation \<Rightarrow> bool"
|
||||
where
|
||||
"isPageRemap v \<equiv> case v of
|
||||
PageRemap v0 v1 v2 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isPageMap :: "page_invocation \<Rightarrow> bool"
|
||||
where
|
||||
"isPageMap v \<equiv> case v of
|
||||
PageMap v0 v1 v2 v3 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isPageUnmap :: "page_invocation \<Rightarrow> bool"
|
||||
where
|
||||
"isPageUnmap v \<equiv> case v of
|
||||
PageUnmap v0 v1 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
datatype asidcontrol_invocation =
|
||||
MakePool machine_word machine_word machine_word asid
|
||||
|
||||
primrec
|
||||
makePoolSlot :: "asidcontrol_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"makePoolSlot (MakePool v0 v1 v2 v3) = v1"
|
||||
|
||||
primrec
|
||||
makePoolFrame :: "asidcontrol_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"makePoolFrame (MakePool v0 v1 v2 v3) = v0"
|
||||
|
||||
primrec
|
||||
makePoolBase :: "asidcontrol_invocation \<Rightarrow> asid"
|
||||
where
|
||||
"makePoolBase (MakePool v0 v1 v2 v3) = v3"
|
||||
|
||||
primrec
|
||||
makePoolParent :: "asidcontrol_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"makePoolParent (MakePool v0 v1 v2 v3) = v2"
|
||||
|
||||
primrec
|
||||
makePoolSlot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> asidcontrol_invocation \<Rightarrow> asidcontrol_invocation"
|
||||
where
|
||||
"makePoolSlot_update f (MakePool v0 v1 v2 v3) = MakePool v0 (f v1) v2 v3"
|
||||
|
||||
primrec
|
||||
makePoolFrame_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> asidcontrol_invocation \<Rightarrow> asidcontrol_invocation"
|
||||
where
|
||||
"makePoolFrame_update f (MakePool v0 v1 v2 v3) = MakePool (f v0) v1 v2 v3"
|
||||
|
||||
primrec
|
||||
makePoolBase_update :: "(asid \<Rightarrow> asid) \<Rightarrow> asidcontrol_invocation \<Rightarrow> asidcontrol_invocation"
|
||||
where
|
||||
"makePoolBase_update f (MakePool v0 v1 v2 v3) = MakePool v0 v1 v2 (f v3)"
|
||||
|
||||
primrec
|
||||
makePoolParent_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> asidcontrol_invocation \<Rightarrow> asidcontrol_invocation"
|
||||
where
|
||||
"makePoolParent_update f (MakePool v0 v1 v2 v3) = MakePool v0 v1 (f v2) v3"
|
||||
|
||||
abbreviation (input)
|
||||
MakePool_trans :: "(machine_word) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> (asid) \<Rightarrow> asidcontrol_invocation" ("MakePool'_ \<lparr> makePoolFrame= _, makePoolSlot= _, makePoolParent= _, makePoolBase= _ \<rparr>")
|
||||
where
|
||||
"MakePool_ \<lparr> makePoolFrame= v0, makePoolSlot= v1, makePoolParent= v2, makePoolBase= v3 \<rparr> == MakePool v0 v1 v2 v3"
|
||||
|
||||
lemma makePoolSlot_makePoolSlot_update [simp]:
|
||||
"makePoolSlot (makePoolSlot_update f v) = f (makePoolSlot v)"
|
||||
by (cases v) simp
|
||||
|
||||
lemma makePoolSlot_makePoolFrame_update [simp]:
|
||||
"makePoolSlot (makePoolFrame_update f v) = makePoolSlot v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma makePoolSlot_makePoolBase_update [simp]:
|
||||
"makePoolSlot (makePoolBase_update f v) = makePoolSlot v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma makePoolSlot_makePoolParent_update [simp]:
|
||||
"makePoolSlot (makePoolParent_update f v) = makePoolSlot v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma makePoolFrame_makePoolSlot_update [simp]:
|
||||
"makePoolFrame (makePoolSlot_update f v) = makePoolFrame v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma makePoolFrame_makePoolFrame_update [simp]:
|
||||
"makePoolFrame (makePoolFrame_update f v) = f (makePoolFrame v)"
|
||||
by (cases v) simp
|
||||
|
||||
lemma makePoolFrame_makePoolBase_update [simp]:
|
||||
"makePoolFrame (makePoolBase_update f v) = makePoolFrame v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma makePoolFrame_makePoolParent_update [simp]:
|
||||
"makePoolFrame (makePoolParent_update f v) = makePoolFrame v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma makePoolBase_makePoolSlot_update [simp]:
|
||||
"makePoolBase (makePoolSlot_update f v) = makePoolBase v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma makePoolBase_makePoolFrame_update [simp]:
|
||||
"makePoolBase (makePoolFrame_update f v) = makePoolBase v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma makePoolBase_makePoolBase_update [simp]:
|
||||
"makePoolBase (makePoolBase_update f v) = f (makePoolBase v)"
|
||||
by (cases v) simp
|
||||
|
||||
lemma makePoolBase_makePoolParent_update [simp]:
|
||||
"makePoolBase (makePoolParent_update f v) = makePoolBase v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma makePoolParent_makePoolSlot_update [simp]:
|
||||
"makePoolParent (makePoolSlot_update f v) = makePoolParent v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma makePoolParent_makePoolFrame_update [simp]:
|
||||
"makePoolParent (makePoolFrame_update f v) = makePoolParent v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma makePoolParent_makePoolBase_update [simp]:
|
||||
"makePoolParent (makePoolBase_update f v) = makePoolParent v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma makePoolParent_makePoolParent_update [simp]:
|
||||
"makePoolParent (makePoolParent_update f v) = f (makePoolParent v)"
|
||||
by (cases v) simp
|
||||
|
||||
datatype asidpool_invocation =
|
||||
Assign asid machine_word machine_word
|
||||
|
||||
primrec
|
||||
assignASIDPool :: "asidpool_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"assignASIDPool (Assign v0 v1 v2) = v1"
|
||||
|
||||
primrec
|
||||
assignASIDCTSlot :: "asidpool_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"assignASIDCTSlot (Assign v0 v1 v2) = v2"
|
||||
|
||||
primrec
|
||||
assignASID :: "asidpool_invocation \<Rightarrow> asid"
|
||||
where
|
||||
"assignASID (Assign v0 v1 v2) = v0"
|
||||
|
||||
primrec
|
||||
assignASIDPool_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> asidpool_invocation \<Rightarrow> asidpool_invocation"
|
||||
where
|
||||
"assignASIDPool_update f (Assign v0 v1 v2) = Assign v0 (f v1) v2"
|
||||
|
||||
primrec
|
||||
assignASIDCTSlot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> asidpool_invocation \<Rightarrow> asidpool_invocation"
|
||||
where
|
||||
"assignASIDCTSlot_update f (Assign v0 v1 v2) = Assign v0 v1 (f v2)"
|
||||
|
||||
primrec
|
||||
assignASID_update :: "(asid \<Rightarrow> asid) \<Rightarrow> asidpool_invocation \<Rightarrow> asidpool_invocation"
|
||||
where
|
||||
"assignASID_update f (Assign v0 v1 v2) = Assign (f v0) v1 v2"
|
||||
|
||||
abbreviation (input)
|
||||
Assign_trans :: "(asid) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> asidpool_invocation" ("Assign'_ \<lparr> assignASID= _, assignASIDPool= _, assignASIDCTSlot= _ \<rparr>")
|
||||
where
|
||||
"Assign_ \<lparr> assignASID= v0, assignASIDPool= v1, assignASIDCTSlot= v2 \<rparr> == Assign v0 v1 v2"
|
||||
|
||||
lemma assignASIDPool_assignASIDPool_update [simp]:
|
||||
"assignASIDPool (assignASIDPool_update f v) = f (assignASIDPool v)"
|
||||
by (cases v) simp
|
||||
|
||||
lemma assignASIDPool_assignASIDCTSlot_update [simp]:
|
||||
"assignASIDPool (assignASIDCTSlot_update f v) = assignASIDPool v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma assignASIDPool_assignASID_update [simp]:
|
||||
"assignASIDPool (assignASID_update f v) = assignASIDPool v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma assignASIDCTSlot_assignASIDPool_update [simp]:
|
||||
"assignASIDCTSlot (assignASIDPool_update f v) = assignASIDCTSlot v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma assignASIDCTSlot_assignASIDCTSlot_update [simp]:
|
||||
"assignASIDCTSlot (assignASIDCTSlot_update f v) = f (assignASIDCTSlot v)"
|
||||
by (cases v) simp
|
||||
|
||||
lemma assignASIDCTSlot_assignASID_update [simp]:
|
||||
"assignASIDCTSlot (assignASID_update f v) = assignASIDCTSlot v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma assignASID_assignASIDPool_update [simp]:
|
||||
"assignASID (assignASIDPool_update f v) = assignASID v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma assignASID_assignASIDCTSlot_update [simp]:
|
||||
"assignASID (assignASIDCTSlot_update f v) = assignASID v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma assignASID_assignASID_update [simp]:
|
||||
"assignASID (assignASID_update f v) = f (assignASID v)"
|
||||
by (cases v) simp
|
||||
|
||||
datatype ioport_invocation_data =
|
||||
IOPortIn8
|
||||
| IOPortIn16
|
||||
| IOPortIn32
|
||||
| IOPortOut8 word8
|
||||
| IOPortOut16 word16
|
||||
| IOPortOut32 word32
|
||||
|
||||
datatype ioport_invocation =
|
||||
IOPortInvocation ioport ioport_invocation_data
|
||||
|
||||
datatype copy_register_sets =
|
||||
X64NoExtraRegisters
|
||||
|
||||
|
||||
datatype invocation =
|
||||
InvokePDPT pdptinvocation
|
||||
| InvokePageDirectory page_directory_invocation
|
||||
| InvokePageTable page_table_invocation
|
||||
| InvokePage page_invocation
|
||||
| InvokeASIDControl asidcontrol_invocation
|
||||
| InvokeASIDPool asidpool_invocation
|
||||
| InvokeIOPort ioport_invocation
|
||||
|
||||
datatype irqcontrol_invocation =
|
||||
IssueIRQHandlerIOAPIC irq machine_word machine_word machine_word machine_word machine_word machine_word machine_word
|
||||
| IssueIRQHandlerMSI irq machine_word machine_word machine_word machine_word machine_word machine_word
|
||||
|
||||
primrec
|
||||
issueHandlerIOAPICPin :: "irqcontrol_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"issueHandlerIOAPICPin (IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 v7) = v4"
|
||||
|
||||
primrec
|
||||
issueHandlerIOAPICSlot :: "irqcontrol_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"issueHandlerIOAPICSlot (IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 v7) = v1"
|
||||
|
||||
primrec
|
||||
issueHandlerMSIPCIFunc :: "irqcontrol_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"issueHandlerMSIPCIFunc (IssueIRQHandlerMSI v0 v1 v2 v3 v4 v5 v6) = v5"
|
||||
|
||||
primrec
|
||||
issueHandlerIOAPICLevel :: "irqcontrol_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"issueHandlerIOAPICLevel (IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 v7) = v5"
|
||||
|
||||
primrec
|
||||
issueHandlerMSISlot :: "irqcontrol_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"issueHandlerMSISlot (IssueIRQHandlerMSI v0 v1 v2 v3 v4 v5 v6) = v1"
|
||||
|
||||
primrec
|
||||
issueHandlerMSIIRQ :: "irqcontrol_invocation \<Rightarrow> irq"
|
||||
where
|
||||
"issueHandlerMSIIRQ (IssueIRQHandlerMSI v0 v1 v2 v3 v4 v5 v6) = v0"
|
||||
|
||||
primrec
|
||||
issueHandlerMSIHandle :: "irqcontrol_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"issueHandlerMSIHandle (IssueIRQHandlerMSI v0 v1 v2 v3 v4 v5 v6) = v6"
|
||||
|
||||
primrec
|
||||
issueHandlerIOAPICControllerSlot :: "irqcontrol_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"issueHandlerIOAPICControllerSlot (IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 v7) = v2"
|
||||
|
||||
primrec
|
||||
issueHandlerIOAPICPolarity :: "irqcontrol_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"issueHandlerIOAPICPolarity (IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 v7) = v6"
|
||||
|
||||
primrec
|
||||
issueHandlerIOAPICIRQ :: "irqcontrol_invocation \<Rightarrow> irq"
|
||||
where
|
||||
"issueHandlerIOAPICIRQ (IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 v7) = v0"
|
||||
|
||||
primrec
|
||||
issueHandlerMSIControllerSlot :: "irqcontrol_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"issueHandlerMSIControllerSlot (IssueIRQHandlerMSI v0 v1 v2 v3 v4 v5 v6) = v2"
|
||||
|
||||
primrec
|
||||
issueHandlerMSIPCIDev :: "irqcontrol_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"issueHandlerMSIPCIDev (IssueIRQHandlerMSI v0 v1 v2 v3 v4 v5 v6) = v4"
|
||||
|
||||
primrec
|
||||
issueHandlerMSIPCIBus :: "irqcontrol_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"issueHandlerMSIPCIBus (IssueIRQHandlerMSI v0 v1 v2 v3 v4 v5 v6) = v3"
|
||||
|
||||
primrec
|
||||
issueHandlerIOAPICVector :: "irqcontrol_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"issueHandlerIOAPICVector (IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 v7) = v7"
|
||||
|
||||
primrec
|
||||
issueHandlerIOAPICIOAPIC :: "irqcontrol_invocation \<Rightarrow> machine_word"
|
||||
where
|
||||
"issueHandlerIOAPICIOAPIC (IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 v7) = v3"
|
||||
|
||||
primrec
|
||||
issueHandlerIOAPICPin_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> irqcontrol_invocation \<Rightarrow> irqcontrol_invocation"
|
||||
where
|
||||
"issueHandlerIOAPICPin_update f (IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 v7) = IssueIRQHandlerIOAPIC v0 v1 v2 v3 (f v4) v5 v6 v7"
|
||||
|
||||
primrec
|
||||
issueHandlerIOAPICSlot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> irqcontrol_invocation \<Rightarrow> irqcontrol_invocation"
|
||||
where
|
||||
"issueHandlerIOAPICSlot_update f (IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 v7) = IssueIRQHandlerIOAPIC v0 (f v1) v2 v3 v4 v5 v6 v7"
|
||||
|
||||
primrec
|
||||
issueHandlerMSIPCIFunc_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> irqcontrol_invocation \<Rightarrow> irqcontrol_invocation"
|
||||
where
|
||||
"issueHandlerMSIPCIFunc_update f (IssueIRQHandlerMSI v0 v1 v2 v3 v4 v5 v6) = IssueIRQHandlerMSI v0 v1 v2 v3 v4 (f v5) v6"
|
||||
|
||||
primrec
|
||||
issueHandlerIOAPICLevel_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> irqcontrol_invocation \<Rightarrow> irqcontrol_invocation"
|
||||
where
|
||||
"issueHandlerIOAPICLevel_update f (IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 v7) = IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 (f v5) v6 v7"
|
||||
|
||||
primrec
|
||||
issueHandlerMSISlot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> irqcontrol_invocation \<Rightarrow> irqcontrol_invocation"
|
||||
where
|
||||
"issueHandlerMSISlot_update f (IssueIRQHandlerMSI v0 v1 v2 v3 v4 v5 v6) = IssueIRQHandlerMSI v0 (f v1) v2 v3 v4 v5 v6"
|
||||
|
||||
primrec
|
||||
issueHandlerMSIIRQ_update :: "(irq \<Rightarrow> irq) \<Rightarrow> irqcontrol_invocation \<Rightarrow> irqcontrol_invocation"
|
||||
where
|
||||
"issueHandlerMSIIRQ_update f (IssueIRQHandlerMSI v0 v1 v2 v3 v4 v5 v6) = IssueIRQHandlerMSI (f v0) v1 v2 v3 v4 v5 v6"
|
||||
|
||||
primrec
|
||||
issueHandlerMSIHandle_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> irqcontrol_invocation \<Rightarrow> irqcontrol_invocation"
|
||||
where
|
||||
"issueHandlerMSIHandle_update f (IssueIRQHandlerMSI v0 v1 v2 v3 v4 v5 v6) = IssueIRQHandlerMSI v0 v1 v2 v3 v4 v5 (f v6)"
|
||||
|
||||
primrec
|
||||
issueHandlerIOAPICControllerSlot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> irqcontrol_invocation \<Rightarrow> irqcontrol_invocation"
|
||||
where
|
||||
"issueHandlerIOAPICControllerSlot_update f (IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 v7) = IssueIRQHandlerIOAPIC v0 v1 (f v2) v3 v4 v5 v6 v7"
|
||||
|
||||
primrec
|
||||
issueHandlerIOAPICPolarity_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> irqcontrol_invocation \<Rightarrow> irqcontrol_invocation"
|
||||
where
|
||||
"issueHandlerIOAPICPolarity_update f (IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 v7) = IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 (f v6) v7"
|
||||
|
||||
primrec
|
||||
issueHandlerIOAPICIRQ_update :: "(irq \<Rightarrow> irq) \<Rightarrow> irqcontrol_invocation \<Rightarrow> irqcontrol_invocation"
|
||||
where
|
||||
"issueHandlerIOAPICIRQ_update f (IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 v7) = IssueIRQHandlerIOAPIC (f v0) v1 v2 v3 v4 v5 v6 v7"
|
||||
|
||||
primrec
|
||||
issueHandlerMSIControllerSlot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> irqcontrol_invocation \<Rightarrow> irqcontrol_invocation"
|
||||
where
|
||||
"issueHandlerMSIControllerSlot_update f (IssueIRQHandlerMSI v0 v1 v2 v3 v4 v5 v6) = IssueIRQHandlerMSI v0 v1 (f v2) v3 v4 v5 v6"
|
||||
|
||||
primrec
|
||||
issueHandlerMSIPCIDev_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> irqcontrol_invocation \<Rightarrow> irqcontrol_invocation"
|
||||
where
|
||||
"issueHandlerMSIPCIDev_update f (IssueIRQHandlerMSI v0 v1 v2 v3 v4 v5 v6) = IssueIRQHandlerMSI v0 v1 v2 v3 (f v4) v5 v6"
|
||||
|
||||
primrec
|
||||
issueHandlerMSIPCIBus_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> irqcontrol_invocation \<Rightarrow> irqcontrol_invocation"
|
||||
where
|
||||
"issueHandlerMSIPCIBus_update f (IssueIRQHandlerMSI v0 v1 v2 v3 v4 v5 v6) = IssueIRQHandlerMSI v0 v1 v2 (f v3) v4 v5 v6"
|
||||
|
||||
primrec
|
||||
issueHandlerIOAPICVector_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> irqcontrol_invocation \<Rightarrow> irqcontrol_invocation"
|
||||
where
|
||||
"issueHandlerIOAPICVector_update f (IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 v7) = IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 (f v7)"
|
||||
|
||||
primrec
|
||||
issueHandlerIOAPICIOAPIC_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> irqcontrol_invocation \<Rightarrow> irqcontrol_invocation"
|
||||
where
|
||||
"issueHandlerIOAPICIOAPIC_update f (IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 v7) = IssueIRQHandlerIOAPIC v0 v1 v2 (f v3) v4 v5 v6 v7"
|
||||
|
||||
abbreviation (input)
|
||||
IssueIRQHandlerIOAPIC_trans :: "(irq) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> irqcontrol_invocation" ("IssueIRQHandlerIOAPIC'_ \<lparr> issueHandlerIOAPICIRQ= _, issueHandlerIOAPICSlot= _, issueHandlerIOAPICControllerSlot= _, issueHandlerIOAPICIOAPIC= _, issueHandlerIOAPICPin= _, issueHandlerIOAPICLevel= _, issueHandlerIOAPICPolarity= _, issueHandlerIOAPICVector= _ \<rparr>")
|
||||
where
|
||||
"IssueIRQHandlerIOAPIC_ \<lparr> issueHandlerIOAPICIRQ= v0, issueHandlerIOAPICSlot= v1, issueHandlerIOAPICControllerSlot= v2, issueHandlerIOAPICIOAPIC= v3, issueHandlerIOAPICPin= v4, issueHandlerIOAPICLevel= v5, issueHandlerIOAPICPolarity= v6, issueHandlerIOAPICVector= v7 \<rparr> == IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 v7"
|
||||
|
||||
abbreviation (input)
|
||||
IssueIRQHandlerMSI_trans :: "(irq) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> irqcontrol_invocation" ("IssueIRQHandlerMSI'_ \<lparr> issueHandlerMSIIRQ= _, issueHandlerMSISlot= _, issueHandlerMSIControllerSlot= _, issueHandlerMSIPCIBus= _, issueHandlerMSIPCIDev= _, issueHandlerMSIPCIFunc= _, issueHandlerMSIHandle= _ \<rparr>")
|
||||
where
|
||||
"IssueIRQHandlerMSI_ \<lparr> issueHandlerMSIIRQ= v0, issueHandlerMSISlot= v1, issueHandlerMSIControllerSlot= v2, issueHandlerMSIPCIBus= v3, issueHandlerMSIPCIDev= v4, issueHandlerMSIPCIFunc= v5, issueHandlerMSIHandle= v6 \<rparr> == IssueIRQHandlerMSI v0 v1 v2 v3 v4 v5 v6"
|
||||
|
||||
definition
|
||||
isIssueIRQHandlerIOAPIC :: "irqcontrol_invocation \<Rightarrow> bool"
|
||||
where
|
||||
"isIssueIRQHandlerIOAPIC v \<equiv> case v of
|
||||
IssueIRQHandlerIOAPIC v0 v1 v2 v3 v4 v5 v6 v7 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isIssueIRQHandlerMSI :: "irqcontrol_invocation \<Rightarrow> bool"
|
||||
where
|
||||
"isIssueIRQHandlerMSI v \<equiv> case v of
|
||||
IssueIRQHandlerMSI v0 v1 v2 v3 v4 v5 v6 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
|
||||
consts'
|
||||
deriveCap :: "machine_word \<Rightarrow> arch_capability \<Rightarrow> ( syscall_error , arch_capability ) kernel_f"
|
||||
|
||||
consts'
|
||||
ioPortGetFirstPort :: "machine_word \<Rightarrow> word16"
|
||||
|
||||
consts'
|
||||
ioPortGetLastPort :: "machine_word \<Rightarrow> word16"
|
||||
|
||||
consts'
|
||||
updateCapData :: "bool \<Rightarrow> machine_word \<Rightarrow> arch_capability \<Rightarrow> capability"
|
||||
|
||||
consts'
|
||||
maskCapRights :: "cap_rights \<Rightarrow> arch_capability \<Rightarrow> capability"
|
||||
|
||||
consts'
|
||||
finaliseCap :: "arch_capability \<Rightarrow> bool \<Rightarrow> capability kernel"
|
||||
|
||||
consts'
|
||||
sameRegionAs :: "arch_capability \<Rightarrow> arch_capability \<Rightarrow> bool"
|
||||
|
||||
consts'
|
||||
isPhysicalCap :: "arch_capability \<Rightarrow> bool"
|
||||
|
||||
consts'
|
||||
sameObjectAs :: "arch_capability \<Rightarrow> arch_capability \<Rightarrow> bool"
|
||||
|
||||
consts'
|
||||
placeNewDataObject :: "machine_word \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
createObject :: "object_type \<Rightarrow> machine_word \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> arch_capability kernel"
|
||||
|
||||
consts'
|
||||
isIOCap :: "arch_capability \<Rightarrow> bool"
|
||||
|
||||
consts'
|
||||
decodeInvocation :: "machine_word \<Rightarrow> machine_word list \<Rightarrow> cptr \<Rightarrow> machine_word \<Rightarrow> arch_capability \<Rightarrow> (capability * machine_word) list \<Rightarrow> ( syscall_error , invocation ) kernel_f"
|
||||
|
||||
consts'
|
||||
performInvocation :: "invocation \<Rightarrow> machine_word list kernel_p"
|
||||
|
||||
consts'
|
||||
capUntypedPtr :: "arch_capability \<Rightarrow> machine_word"
|
||||
|
||||
consts'
|
||||
capUntypedSize :: "arch_capability \<Rightarrow> machine_word"
|
||||
|
||||
consts'
|
||||
prepareThreadDelete :: "machine_word \<Rightarrow> unit kernel"
|
||||
|
||||
|
||||
end (*context X64*)
|
||||
|
||||
end
|
||||
|
|
@ -1,273 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file ArchRetype_H.thy *)
|
||||
(*
|
||||
* 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 "Retyping Objects"
|
||||
|
||||
theory ArchRetype_H
|
||||
imports
|
||||
ArchRetypeDecls_H
|
||||
ArchVSpaceDecls_H
|
||||
Hardware_H
|
||||
"../KI_Decls_H"
|
||||
begin
|
||||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
defs deriveCap_def:
|
||||
"deriveCap x0 x1\<equiv> (let c = x1 in
|
||||
if isPageTableCap c \<and> capPTMappedAddress c \<noteq> None
|
||||
then returnOk c
|
||||
else if isPageTableCap c \<and> capPTMappedAddress c = None
|
||||
then throw IllegalOperation
|
||||
else if isPageDirectoryCap c \<and> capPDMappedAddress c \<noteq> None
|
||||
then returnOk c
|
||||
else if isPageDirectoryCap c \<and> capPDMappedAddress c = None
|
||||
then throw IllegalOperation
|
||||
else if isPDPointerTableCap c \<and> capPDPTMappedAddress c \<noteq> None
|
||||
then returnOk c
|
||||
else if isPDPointerTableCap c \<and> capPDPTMappedAddress c = None
|
||||
then throw IllegalOperation
|
||||
else if isPML4Cap c \<and> capPML4MappedASID c \<noteq> None
|
||||
then returnOk c
|
||||
else if isPML4Cap c \<and> capPML4MappedASID c = None
|
||||
then throw IllegalOperation
|
||||
else if isPageCap c
|
||||
then returnOk $ c \<lparr> capVPMappedAddress := Nothing, capVPMapType := VMNoMap \<rparr>
|
||||
else if isASIDControlCap c
|
||||
then returnOk c
|
||||
else if isASIDPoolCap c
|
||||
then returnOk c
|
||||
else if isIOPortCap c
|
||||
then returnOk c
|
||||
else undefined
|
||||
)"
|
||||
|
||||
defs ioPortGetFirstPort_def:
|
||||
"ioPortGetFirstPort arg1 \<equiv> error []"
|
||||
|
||||
defs ioPortGetLastPort_def:
|
||||
"ioPortGetLastPort arg1 \<equiv> error []"
|
||||
|
||||
defs updateCapData_def:
|
||||
"updateCapData arg1 arg2 c \<equiv> ArchObjectCap c"
|
||||
|
||||
defs maskCapRights_def:
|
||||
"maskCapRights r x1\<equiv> (let c = x1 in
|
||||
if isPageCap c
|
||||
then ArchObjectCap $ c \<lparr>
|
||||
capVPRights := maskVMRights (capVPRights c) r \<rparr>
|
||||
else ArchObjectCap c
|
||||
)"
|
||||
|
||||
defs finaliseCap_def:
|
||||
"finaliseCap x0 x1\<equiv> (case (x0, x1) of
|
||||
((ASIDPoolCap ptr b), True) \<Rightarrow> (do
|
||||
deleteASIDPool b ptr;
|
||||
return NullCap
|
||||
od)
|
||||
| ((PML4Cap ptr (Some a)), True) \<Rightarrow> (do
|
||||
deleteASID a ptr;
|
||||
return NullCap
|
||||
od)
|
||||
| ((PDPointerTableCap ptr (Some (a, v))), True) \<Rightarrow> (do
|
||||
unmapPDPT a v ptr;
|
||||
return NullCap
|
||||
od)
|
||||
| ((PageDirectoryCap ptr (Some (a, v))), True) \<Rightarrow> (do
|
||||
unmapPageDirectory a v ptr;
|
||||
return NullCap
|
||||
od)
|
||||
| ((PageTableCap ptr (Some (a, v))), True) \<Rightarrow> (do
|
||||
unmapPageTable a v ptr;
|
||||
return NullCap
|
||||
od)
|
||||
| ((PageCap ptr _ _ s _ (Some (a, v))), _) \<Rightarrow> (do
|
||||
unmapPage s a v ptr;
|
||||
return NullCap
|
||||
od)
|
||||
| (_, _) \<Rightarrow> return NullCap
|
||||
)"
|
||||
|
||||
defs sameRegionAs_def:
|
||||
"sameRegionAs x0 x1\<equiv> (let (a,b) = (x0, x1) in
|
||||
if isPageCap a \<and> isPageCap b
|
||||
then
|
||||
let
|
||||
botA = capVPBasePtr a;
|
||||
botB = capVPBasePtr b;
|
||||
topA = botA + bit (pageBitsForSize $ capVPSize a) - 1;
|
||||
topB = botB + bit (pageBitsForSize $ capVPSize b) - 1
|
||||
in
|
||||
|
||||
(botA \<le> botB) \<and> (topA \<ge> topB) \<and> (botB \<le> topB)
|
||||
else if isPageTableCap a \<and> isPageTableCap b
|
||||
then
|
||||
capPTBasePtr a = capPTBasePtr b
|
||||
else if isPageDirectoryCap a \<and> isPageDirectoryCap b
|
||||
then
|
||||
capPDBasePtr a = capPDBasePtr b
|
||||
else if isPDPointerTableCap a \<and> isPDPointerTableCap b
|
||||
then
|
||||
capPDPTBasePtr a = capPDPTBasePtr b
|
||||
else if isPML4Cap a \<and> isPML4Cap b
|
||||
then
|
||||
capPML4BasePtr a = capPML4BasePtr b
|
||||
else if isASIDControlCap a \<and> isASIDControlCap b
|
||||
then True
|
||||
else if isASIDPoolCap a \<and> isASIDPoolCap b
|
||||
then
|
||||
capASIDPool a = capASIDPool b
|
||||
else if isIOPortCap a \<and> isIOPortCap b
|
||||
then
|
||||
let
|
||||
fA = capIOPortFirstPort a;
|
||||
fB = capIOPortFirstPort b;
|
||||
lA = capIOPortLastPort a;
|
||||
lB = capIOPortLastPort b
|
||||
in
|
||||
|
||||
(fA \<le> fB) \<and> (lB \<le> lA) \<and> (fB \<le> lB)
|
||||
else False
|
||||
)"
|
||||
|
||||
defs isPhysicalCap_def:
|
||||
"isPhysicalCap x0\<equiv> (case x0 of
|
||||
ASIDControlCap \<Rightarrow> False
|
||||
| (IOPortCap _ _) \<Rightarrow> False
|
||||
| _ \<Rightarrow> True
|
||||
)"
|
||||
|
||||
defs sameObjectAs_def:
|
||||
"sameObjectAs x0 x1\<equiv> (let (a, b) = (x0, x1) in
|
||||
if isPageCap a \<and> isPageCap b
|
||||
then let ptrA = capVPBasePtr a
|
||||
in
|
||||
(ptrA = capVPBasePtr b) \<and> (capVPSize a = capVPSize b)
|
||||
\<and> (ptrA \<le> ptrA + bit (pageBitsForSize $ capVPSize a) - 1)
|
||||
\<and> (capVPIsDevice a = capVPIsDevice b)
|
||||
else if isIOPortCap a \<and> isIOPortCap b
|
||||
then let fA = capIOPortFirstPort a
|
||||
in
|
||||
(fA = capIOPortFirstPort b) \<and> (capIOPortLastPort a = capIOPortLastPort b)
|
||||
\<and> (fA \<le> capIOPortLastPort a)
|
||||
else sameRegionAs a b
|
||||
)"
|
||||
|
||||
defs placeNewDataObject_def:
|
||||
"placeNewDataObject regionBase sz isDevice \<equiv> if isDevice
|
||||
then placeNewObject regionBase UserDataDevice sz
|
||||
else placeNewObject regionBase UserData sz"
|
||||
|
||||
defs createObject_def:
|
||||
"createObject t regionBase arg3 isDevice \<equiv>
|
||||
let funupd = (\<lambda> f x v y. if y = x then v else f y) in
|
||||
let pointerCast = PPtr \<circ> fromPPtr
|
||||
in (let t = t in
|
||||
case t of
|
||||
APIObjectType _ =>
|
||||
haskell_fail []
|
||||
| SmallPageObject => (do
|
||||
placeNewDataObject regionBase 0 isDevice;
|
||||
modify (\<lambda> ks. ks \<lparr> gsUserPages :=
|
||||
funupd (gsUserPages ks)
|
||||
(fromPPtr regionBase) (Just X64SmallPage)\<rparr>);
|
||||
return $ PageCap (pointerCast regionBase)
|
||||
VMReadWrite VMNoMap X64SmallPage isDevice Nothing
|
||||
od)
|
||||
| LargePageObject => (do
|
||||
placeNewDataObject regionBase ptTranslationBits isDevice;
|
||||
modify (\<lambda> ks. ks \<lparr> gsUserPages :=
|
||||
funupd (gsUserPages ks)
|
||||
(fromPPtr regionBase) (Just X64LargePage)\<rparr>);
|
||||
return $ PageCap (pointerCast regionBase)
|
||||
VMReadWrite VMNoMap X64LargePage isDevice Nothing
|
||||
od)
|
||||
| HugePageObject => (do
|
||||
placeNewDataObject regionBase (ptTranslationBits + ptTranslationBits) isDevice;
|
||||
modify (\<lambda> ks. ks \<lparr> gsUserPages :=
|
||||
funupd (gsUserPages ks)
|
||||
(fromPPtr regionBase) (Just X64HugePage)\<rparr>);
|
||||
return $ PageCap (pointerCast regionBase)
|
||||
VMReadWrite VMNoMap X64HugePage isDevice Nothing
|
||||
od)
|
||||
| PageTableObject => (do
|
||||
ptSize \<leftarrow> return ( ptBits - objBits (makeObject ::pte));
|
||||
placeNewObject regionBase (makeObject ::pte) ptSize;
|
||||
return $ PageTableCap (pointerCast regionBase) Nothing
|
||||
od)
|
||||
| PageDirectoryObject => (do
|
||||
pdSize \<leftarrow> return ( pdBits - objBits (makeObject ::pde));
|
||||
placeNewObject regionBase (makeObject ::pde) pdSize;
|
||||
return $ PageDirectoryCap (pointerCast regionBase) Nothing
|
||||
od)
|
||||
| PDPointerTableObject => (do
|
||||
pdptSize \<leftarrow> return ( pdptBits - objBits (makeObject ::pdpte));
|
||||
placeNewObject regionBase (makeObject ::pdpte) pdptSize;
|
||||
return $ PDPointerTableCap (pointerCast regionBase) Nothing
|
||||
od)
|
||||
| PML4Object => (do
|
||||
pml4Size \<leftarrow> return ( pml4Bits - objBits (makeObject ::pml4e));
|
||||
placeNewObject regionBase (makeObject ::pml4e) pml4Size;
|
||||
copyGlobalMappings (pointerCast regionBase);
|
||||
return $ PML4Cap (pointerCast regionBase) Nothing
|
||||
od)
|
||||
)"
|
||||
|
||||
defs isIOCap_def:
|
||||
"isIOCap c\<equiv> (case c of
|
||||
(IOPortCap _ _) \<Rightarrow> True
|
||||
| _ \<Rightarrow> False
|
||||
)"
|
||||
|
||||
defs decodeInvocation_def:
|
||||
"decodeInvocation label args capIndex slot cap extraCaps \<equiv>
|
||||
if isIOCap cap
|
||||
then decodeX64PortInvocation label args cap
|
||||
else decodeX64MMUInvocation label args capIndex slot cap extraCaps"
|
||||
|
||||
defs performInvocation_def:
|
||||
"performInvocation x0\<equiv> (let oper = x0 in
|
||||
case oper of
|
||||
InvokeIOPort _ => performX64PortInvocation oper
|
||||
| _ => performX64MMUInvocation oper
|
||||
)"
|
||||
|
||||
defs capUntypedPtr_def:
|
||||
"capUntypedPtr x0\<equiv> (case x0 of
|
||||
(PageCap ((* PPtr *) p) _ _ _ _ _) \<Rightarrow> PPtr p
|
||||
| (PageTableCap ((* PPtr *) p) _) \<Rightarrow> PPtr p
|
||||
| (PageDirectoryCap ((* PPtr *) p) _) \<Rightarrow> PPtr p
|
||||
| (PDPointerTableCap ((* PPtr *) p) _) \<Rightarrow> PPtr p
|
||||
| (PML4Cap ((* PPtr *) p) _) \<Rightarrow> PPtr p
|
||||
| ASIDControlCap \<Rightarrow> error []
|
||||
| (ASIDPoolCap ((* PPtr *) p) _) \<Rightarrow> PPtr p
|
||||
| (IOPortCap _ _) \<Rightarrow> error []
|
||||
)"
|
||||
|
||||
defs capUntypedSize_def:
|
||||
"capUntypedSize x0\<equiv> (case x0 of
|
||||
(PageCap _ _ _ sz _ _) \<Rightarrow> 1 `~shiftL~` pageBitsForSize sz
|
||||
| (PageTableCap _ _) \<Rightarrow> 1 `~shiftL~` 12
|
||||
| (PageDirectoryCap _ _) \<Rightarrow> 1 `~shiftL~` 12
|
||||
| (PDPointerTableCap _ _) \<Rightarrow> 1 `~shiftL~` 12
|
||||
| (PML4Cap _ _) \<Rightarrow> 1 `~shiftL~` 12
|
||||
| (ASIDControlCap ) \<Rightarrow> 0
|
||||
| (ASIDPoolCap _ _) \<Rightarrow> 1 `~shiftL~` (asidLowBits + 3)
|
||||
| (IOPortCap _ _) \<Rightarrow> 0
|
||||
)"
|
||||
|
||||
defs prepareThreadDelete_def:
|
||||
"prepareThreadDelete arg1 \<equiv> return ()"
|
||||
|
||||
|
||||
end (* context X64 *)
|
||||
end
|
||||
|
|
@ -1,384 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file ArchStateData_H.thy *)
|
||||
(*
|
||||
* 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)
|
||||
*)
|
||||
|
||||
(*
|
||||
Kernel state and kernel monads, imports everything that SEL4.Model needs.
|
||||
*)
|
||||
|
||||
chapter "Architecture Specific Kernel State and Monads"
|
||||
|
||||
theory ArchStateData_H
|
||||
imports
|
||||
Arch_Structs_B
|
||||
ArchTypes_H
|
||||
ArchStructures_H
|
||||
begin
|
||||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
datatype kernel_state =
|
||||
X64KernelState "asid \<Rightarrow> ((machine_word) option)" "asid \<Rightarrow> ((machine_word) option)" machine_word "machine_word list" "machine_word list" "machine_word list" cr3 "machine_word \<Rightarrow> x64vspace_region_use"
|
||||
|
||||
primrec
|
||||
x64KSCurrentCR3 :: "kernel_state \<Rightarrow> cr3"
|
||||
where
|
||||
"x64KSCurrentCR3 (X64KernelState v0 v1 v2 v3 v4 v5 v6 v7) = v6"
|
||||
|
||||
primrec
|
||||
x64KSGlobalPDs :: "kernel_state \<Rightarrow> machine_word list"
|
||||
where
|
||||
"x64KSGlobalPDs (X64KernelState v0 v1 v2 v3 v4 v5 v6 v7) = v4"
|
||||
|
||||
primrec
|
||||
x64KSASIDMap :: "kernel_state \<Rightarrow> asid \<Rightarrow> ((machine_word) option)"
|
||||
where
|
||||
"x64KSASIDMap (X64KernelState v0 v1 v2 v3 v4 v5 v6 v7) = v1"
|
||||
|
||||
primrec
|
||||
x64KSKernelVSpace :: "kernel_state \<Rightarrow> machine_word \<Rightarrow> x64vspace_region_use"
|
||||
where
|
||||
"x64KSKernelVSpace (X64KernelState v0 v1 v2 v3 v4 v5 v6 v7) = v7"
|
||||
|
||||
primrec
|
||||
x64KSASIDTable :: "kernel_state \<Rightarrow> asid \<Rightarrow> ((machine_word) option)"
|
||||
where
|
||||
"x64KSASIDTable (X64KernelState v0 v1 v2 v3 v4 v5 v6 v7) = v0"
|
||||
|
||||
primrec
|
||||
x64KSGlobalPDPTs :: "kernel_state \<Rightarrow> machine_word list"
|
||||
where
|
||||
"x64KSGlobalPDPTs (X64KernelState v0 v1 v2 v3 v4 v5 v6 v7) = v3"
|
||||
|
||||
primrec
|
||||
x64KSGlobalPML4 :: "kernel_state \<Rightarrow> machine_word"
|
||||
where
|
||||
"x64KSGlobalPML4 (X64KernelState v0 v1 v2 v3 v4 v5 v6 v7) = v2"
|
||||
|
||||
primrec
|
||||
x64KSGlobalPTs :: "kernel_state \<Rightarrow> machine_word list"
|
||||
where
|
||||
"x64KSGlobalPTs (X64KernelState v0 v1 v2 v3 v4 v5 v6 v7) = v5"
|
||||
|
||||
primrec
|
||||
x64KSCurrentCR3_update :: "(cr3 \<Rightarrow> cr3) \<Rightarrow> kernel_state \<Rightarrow> kernel_state"
|
||||
where
|
||||
"x64KSCurrentCR3_update f (X64KernelState v0 v1 v2 v3 v4 v5 v6 v7) = X64KernelState v0 v1 v2 v3 v4 v5 (f v6) v7"
|
||||
|
||||
primrec
|
||||
x64KSGlobalPDs_update :: "((machine_word list) \<Rightarrow> (machine_word list)) \<Rightarrow> kernel_state \<Rightarrow> kernel_state"
|
||||
where
|
||||
"x64KSGlobalPDs_update f (X64KernelState v0 v1 v2 v3 v4 v5 v6 v7) = X64KernelState v0 v1 v2 v3 (f v4) v5 v6 v7"
|
||||
|
||||
primrec
|
||||
x64KSASIDMap_update :: "((asid \<Rightarrow> ((machine_word) option)) \<Rightarrow> (asid \<Rightarrow> ((machine_word) option))) \<Rightarrow> kernel_state \<Rightarrow> kernel_state"
|
||||
where
|
||||
"x64KSASIDMap_update f (X64KernelState v0 v1 v2 v3 v4 v5 v6 v7) = X64KernelState v0 (f v1) v2 v3 v4 v5 v6 v7"
|
||||
|
||||
primrec
|
||||
x64KSKernelVSpace_update :: "((machine_word \<Rightarrow> x64vspace_region_use) \<Rightarrow> (machine_word \<Rightarrow> x64vspace_region_use)) \<Rightarrow> kernel_state \<Rightarrow> kernel_state"
|
||||
where
|
||||
"x64KSKernelVSpace_update f (X64KernelState v0 v1 v2 v3 v4 v5 v6 v7) = X64KernelState v0 v1 v2 v3 v4 v5 v6 (f v7)"
|
||||
|
||||
primrec
|
||||
x64KSASIDTable_update :: "((asid \<Rightarrow> ((machine_word) option)) \<Rightarrow> (asid \<Rightarrow> ((machine_word) option))) \<Rightarrow> kernel_state \<Rightarrow> kernel_state"
|
||||
where
|
||||
"x64KSASIDTable_update f (X64KernelState v0 v1 v2 v3 v4 v5 v6 v7) = X64KernelState (f v0) v1 v2 v3 v4 v5 v6 v7"
|
||||
|
||||
primrec
|
||||
x64KSGlobalPDPTs_update :: "((machine_word list) \<Rightarrow> (machine_word list)) \<Rightarrow> kernel_state \<Rightarrow> kernel_state"
|
||||
where
|
||||
"x64KSGlobalPDPTs_update f (X64KernelState v0 v1 v2 v3 v4 v5 v6 v7) = X64KernelState v0 v1 v2 (f v3) v4 v5 v6 v7"
|
||||
|
||||
primrec
|
||||
x64KSGlobalPML4_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> kernel_state \<Rightarrow> kernel_state"
|
||||
where
|
||||
"x64KSGlobalPML4_update f (X64KernelState v0 v1 v2 v3 v4 v5 v6 v7) = X64KernelState v0 v1 (f v2) v3 v4 v5 v6 v7"
|
||||
|
||||
primrec
|
||||
x64KSGlobalPTs_update :: "((machine_word list) \<Rightarrow> (machine_word list)) \<Rightarrow> kernel_state \<Rightarrow> kernel_state"
|
||||
where
|
||||
"x64KSGlobalPTs_update f (X64KernelState v0 v1 v2 v3 v4 v5 v6 v7) = X64KernelState v0 v1 v2 v3 v4 (f v5) v6 v7"
|
||||
|
||||
abbreviation (input)
|
||||
X64KernelState_trans :: "(asid \<Rightarrow> ((machine_word) option)) \<Rightarrow> (asid \<Rightarrow> ((machine_word) option)) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word list) \<Rightarrow> (machine_word list) \<Rightarrow> (machine_word list) \<Rightarrow> (cr3) \<Rightarrow> (machine_word \<Rightarrow> x64vspace_region_use) \<Rightarrow> kernel_state" ("X64KernelState'_ \<lparr> x64KSASIDTable= _, x64KSASIDMap= _, x64KSGlobalPML4= _, x64KSGlobalPDPTs= _, x64KSGlobalPDs= _, x64KSGlobalPTs= _, x64KSCurrentCR3= _, x64KSKernelVSpace= _ \<rparr>")
|
||||
where
|
||||
"X64KernelState_ \<lparr> x64KSASIDTable= v0, x64KSASIDMap= v1, x64KSGlobalPML4= v2, x64KSGlobalPDPTs= v3, x64KSGlobalPDs= v4, x64KSGlobalPTs= v5, x64KSCurrentCR3= v6, x64KSKernelVSpace= v7 \<rparr> == X64KernelState v0 v1 v2 v3 v4 v5 v6 v7"
|
||||
|
||||
lemma x64KSCurrentCR3_x64KSCurrentCR3_update [simp]:
|
||||
"x64KSCurrentCR3 (x64KSCurrentCR3_update f v) = f (x64KSCurrentCR3 v)"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSCurrentCR3_x64KSGlobalPDs_update [simp]:
|
||||
"x64KSCurrentCR3 (x64KSGlobalPDs_update f v) = x64KSCurrentCR3 v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSCurrentCR3_x64KSASIDMap_update [simp]:
|
||||
"x64KSCurrentCR3 (x64KSASIDMap_update f v) = x64KSCurrentCR3 v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSCurrentCR3_x64KSKernelVSpace_update [simp]:
|
||||
"x64KSCurrentCR3 (x64KSKernelVSpace_update f v) = x64KSCurrentCR3 v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSCurrentCR3_x64KSASIDTable_update [simp]:
|
||||
"x64KSCurrentCR3 (x64KSASIDTable_update f v) = x64KSCurrentCR3 v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSCurrentCR3_x64KSGlobalPDPTs_update [simp]:
|
||||
"x64KSCurrentCR3 (x64KSGlobalPDPTs_update f v) = x64KSCurrentCR3 v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSCurrentCR3_x64KSGlobalPML4_update [simp]:
|
||||
"x64KSCurrentCR3 (x64KSGlobalPML4_update f v) = x64KSCurrentCR3 v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSCurrentCR3_x64KSGlobalPTs_update [simp]:
|
||||
"x64KSCurrentCR3 (x64KSGlobalPTs_update f v) = x64KSCurrentCR3 v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPDs_x64KSCurrentCR3_update [simp]:
|
||||
"x64KSGlobalPDs (x64KSCurrentCR3_update f v) = x64KSGlobalPDs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPDs_x64KSGlobalPDs_update [simp]:
|
||||
"x64KSGlobalPDs (x64KSGlobalPDs_update f v) = f (x64KSGlobalPDs v)"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPDs_x64KSASIDMap_update [simp]:
|
||||
"x64KSGlobalPDs (x64KSASIDMap_update f v) = x64KSGlobalPDs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPDs_x64KSKernelVSpace_update [simp]:
|
||||
"x64KSGlobalPDs (x64KSKernelVSpace_update f v) = x64KSGlobalPDs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPDs_x64KSASIDTable_update [simp]:
|
||||
"x64KSGlobalPDs (x64KSASIDTable_update f v) = x64KSGlobalPDs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPDs_x64KSGlobalPDPTs_update [simp]:
|
||||
"x64KSGlobalPDs (x64KSGlobalPDPTs_update f v) = x64KSGlobalPDs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPDs_x64KSGlobalPML4_update [simp]:
|
||||
"x64KSGlobalPDs (x64KSGlobalPML4_update f v) = x64KSGlobalPDs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPDs_x64KSGlobalPTs_update [simp]:
|
||||
"x64KSGlobalPDs (x64KSGlobalPTs_update f v) = x64KSGlobalPDs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSASIDMap_x64KSCurrentCR3_update [simp]:
|
||||
"x64KSASIDMap (x64KSCurrentCR3_update f v) = x64KSASIDMap v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSASIDMap_x64KSGlobalPDs_update [simp]:
|
||||
"x64KSASIDMap (x64KSGlobalPDs_update f v) = x64KSASIDMap v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSASIDMap_x64KSASIDMap_update [simp]:
|
||||
"x64KSASIDMap (x64KSASIDMap_update f v) = f (x64KSASIDMap v)"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSASIDMap_x64KSKernelVSpace_update [simp]:
|
||||
"x64KSASIDMap (x64KSKernelVSpace_update f v) = x64KSASIDMap v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSASIDMap_x64KSASIDTable_update [simp]:
|
||||
"x64KSASIDMap (x64KSASIDTable_update f v) = x64KSASIDMap v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSASIDMap_x64KSGlobalPDPTs_update [simp]:
|
||||
"x64KSASIDMap (x64KSGlobalPDPTs_update f v) = x64KSASIDMap v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSASIDMap_x64KSGlobalPML4_update [simp]:
|
||||
"x64KSASIDMap (x64KSGlobalPML4_update f v) = x64KSASIDMap v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSASIDMap_x64KSGlobalPTs_update [simp]:
|
||||
"x64KSASIDMap (x64KSGlobalPTs_update f v) = x64KSASIDMap v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSKernelVSpace_x64KSCurrentCR3_update [simp]:
|
||||
"x64KSKernelVSpace (x64KSCurrentCR3_update f v) = x64KSKernelVSpace v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSKernelVSpace_x64KSGlobalPDs_update [simp]:
|
||||
"x64KSKernelVSpace (x64KSGlobalPDs_update f v) = x64KSKernelVSpace v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSKernelVSpace_x64KSASIDMap_update [simp]:
|
||||
"x64KSKernelVSpace (x64KSASIDMap_update f v) = x64KSKernelVSpace v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSKernelVSpace_x64KSKernelVSpace_update [simp]:
|
||||
"x64KSKernelVSpace (x64KSKernelVSpace_update f v) = f (x64KSKernelVSpace v)"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSKernelVSpace_x64KSASIDTable_update [simp]:
|
||||
"x64KSKernelVSpace (x64KSASIDTable_update f v) = x64KSKernelVSpace v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSKernelVSpace_x64KSGlobalPDPTs_update [simp]:
|
||||
"x64KSKernelVSpace (x64KSGlobalPDPTs_update f v) = x64KSKernelVSpace v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSKernelVSpace_x64KSGlobalPML4_update [simp]:
|
||||
"x64KSKernelVSpace (x64KSGlobalPML4_update f v) = x64KSKernelVSpace v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSKernelVSpace_x64KSGlobalPTs_update [simp]:
|
||||
"x64KSKernelVSpace (x64KSGlobalPTs_update f v) = x64KSKernelVSpace v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSASIDTable_x64KSCurrentCR3_update [simp]:
|
||||
"x64KSASIDTable (x64KSCurrentCR3_update f v) = x64KSASIDTable v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSASIDTable_x64KSGlobalPDs_update [simp]:
|
||||
"x64KSASIDTable (x64KSGlobalPDs_update f v) = x64KSASIDTable v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSASIDTable_x64KSASIDMap_update [simp]:
|
||||
"x64KSASIDTable (x64KSASIDMap_update f v) = x64KSASIDTable v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSASIDTable_x64KSKernelVSpace_update [simp]:
|
||||
"x64KSASIDTable (x64KSKernelVSpace_update f v) = x64KSASIDTable v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSASIDTable_x64KSASIDTable_update [simp]:
|
||||
"x64KSASIDTable (x64KSASIDTable_update f v) = f (x64KSASIDTable v)"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSASIDTable_x64KSGlobalPDPTs_update [simp]:
|
||||
"x64KSASIDTable (x64KSGlobalPDPTs_update f v) = x64KSASIDTable v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSASIDTable_x64KSGlobalPML4_update [simp]:
|
||||
"x64KSASIDTable (x64KSGlobalPML4_update f v) = x64KSASIDTable v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSASIDTable_x64KSGlobalPTs_update [simp]:
|
||||
"x64KSASIDTable (x64KSGlobalPTs_update f v) = x64KSASIDTable v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPDPTs_x64KSCurrentCR3_update [simp]:
|
||||
"x64KSGlobalPDPTs (x64KSCurrentCR3_update f v) = x64KSGlobalPDPTs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPDPTs_x64KSGlobalPDs_update [simp]:
|
||||
"x64KSGlobalPDPTs (x64KSGlobalPDs_update f v) = x64KSGlobalPDPTs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPDPTs_x64KSASIDMap_update [simp]:
|
||||
"x64KSGlobalPDPTs (x64KSASIDMap_update f v) = x64KSGlobalPDPTs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPDPTs_x64KSKernelVSpace_update [simp]:
|
||||
"x64KSGlobalPDPTs (x64KSKernelVSpace_update f v) = x64KSGlobalPDPTs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPDPTs_x64KSASIDTable_update [simp]:
|
||||
"x64KSGlobalPDPTs (x64KSASIDTable_update f v) = x64KSGlobalPDPTs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPDPTs_x64KSGlobalPDPTs_update [simp]:
|
||||
"x64KSGlobalPDPTs (x64KSGlobalPDPTs_update f v) = f (x64KSGlobalPDPTs v)"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPDPTs_x64KSGlobalPML4_update [simp]:
|
||||
"x64KSGlobalPDPTs (x64KSGlobalPML4_update f v) = x64KSGlobalPDPTs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPDPTs_x64KSGlobalPTs_update [simp]:
|
||||
"x64KSGlobalPDPTs (x64KSGlobalPTs_update f v) = x64KSGlobalPDPTs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPML4_x64KSCurrentCR3_update [simp]:
|
||||
"x64KSGlobalPML4 (x64KSCurrentCR3_update f v) = x64KSGlobalPML4 v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPML4_x64KSGlobalPDs_update [simp]:
|
||||
"x64KSGlobalPML4 (x64KSGlobalPDs_update f v) = x64KSGlobalPML4 v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPML4_x64KSASIDMap_update [simp]:
|
||||
"x64KSGlobalPML4 (x64KSASIDMap_update f v) = x64KSGlobalPML4 v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPML4_x64KSKernelVSpace_update [simp]:
|
||||
"x64KSGlobalPML4 (x64KSKernelVSpace_update f v) = x64KSGlobalPML4 v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPML4_x64KSASIDTable_update [simp]:
|
||||
"x64KSGlobalPML4 (x64KSASIDTable_update f v) = x64KSGlobalPML4 v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPML4_x64KSGlobalPDPTs_update [simp]:
|
||||
"x64KSGlobalPML4 (x64KSGlobalPDPTs_update f v) = x64KSGlobalPML4 v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPML4_x64KSGlobalPML4_update [simp]:
|
||||
"x64KSGlobalPML4 (x64KSGlobalPML4_update f v) = f (x64KSGlobalPML4 v)"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPML4_x64KSGlobalPTs_update [simp]:
|
||||
"x64KSGlobalPML4 (x64KSGlobalPTs_update f v) = x64KSGlobalPML4 v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPTs_x64KSCurrentCR3_update [simp]:
|
||||
"x64KSGlobalPTs (x64KSCurrentCR3_update f v) = x64KSGlobalPTs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPTs_x64KSGlobalPDs_update [simp]:
|
||||
"x64KSGlobalPTs (x64KSGlobalPDs_update f v) = x64KSGlobalPTs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPTs_x64KSASIDMap_update [simp]:
|
||||
"x64KSGlobalPTs (x64KSASIDMap_update f v) = x64KSGlobalPTs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPTs_x64KSKernelVSpace_update [simp]:
|
||||
"x64KSGlobalPTs (x64KSKernelVSpace_update f v) = x64KSGlobalPTs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPTs_x64KSASIDTable_update [simp]:
|
||||
"x64KSGlobalPTs (x64KSASIDTable_update f v) = x64KSGlobalPTs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPTs_x64KSGlobalPDPTs_update [simp]:
|
||||
"x64KSGlobalPTs (x64KSGlobalPDPTs_update f v) = x64KSGlobalPTs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPTs_x64KSGlobalPML4_update [simp]:
|
||||
"x64KSGlobalPTs (x64KSGlobalPML4_update f v) = x64KSGlobalPTs v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64KSGlobalPTs_x64KSGlobalPTs_update [simp]:
|
||||
"x64KSGlobalPTs (x64KSGlobalPTs_update f v) = f (x64KSGlobalPTs v)"
|
||||
by (cases v) simp
|
||||
|
||||
definition
|
||||
gdteBits :: "nat"
|
||||
where
|
||||
"gdteBits \<equiv> 3"
|
||||
|
||||
definition
|
||||
newKernelState :: "paddr \<Rightarrow> (kernel_state * paddr list)"
|
||||
where
|
||||
"newKernelState arg1 \<equiv> error []"
|
||||
|
||||
|
||||
end
|
||||
end
|
||||
|
|
@ -1,479 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file ArchStructures_H.thy *)
|
||||
(*
|
||||
* Copyright 2014, General Dynamics C4 Systems
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_GPLv2.txt" for details.
|
||||
*
|
||||
* @TAG(GD_GPL)
|
||||
*)
|
||||
|
||||
theory ArchStructures_H
|
||||
imports
|
||||
"../../../lib/Lib"
|
||||
"../Types_H"
|
||||
Hardware_H
|
||||
begin
|
||||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
|
||||
type_synonym asid = "word64"
|
||||
|
||||
definition
|
||||
ASID :: "asid \<Rightarrow> asid"
|
||||
where ASID_def[simp]:
|
||||
"ASID \<equiv> id"
|
||||
|
||||
definition
|
||||
fromASID :: "asid \<Rightarrow> asid"
|
||||
where
|
||||
fromASID_def[simp]:
|
||||
"fromASID \<equiv> id"
|
||||
|
||||
definition fromASID_update :: "(asid \<Rightarrow> asid) \<Rightarrow> asid \<Rightarrow> asid"
|
||||
where
|
||||
fromASID_update_def[simp]:
|
||||
"fromASID_update f y \<equiv> f y"
|
||||
|
||||
abbreviation (input)
|
||||
ASID_trans :: "(word64) \<Rightarrow> asid" ("ASID'_ \<lparr> fromASID= _ \<rparr>")
|
||||
where
|
||||
"ASID_ \<lparr> fromASID= v0 \<rparr> == ASID v0"
|
||||
|
||||
datatype arch_capability =
|
||||
ASIDPoolCap machine_word asid
|
||||
| ASIDControlCap
|
||||
| IOPortCap ioport ioport
|
||||
| PageCap machine_word vmrights vmmap_type vmpage_size bool "(asid * vptr) option"
|
||||
| PageTableCap machine_word "(asid * vptr) option"
|
||||
| PageDirectoryCap machine_word "(asid * vptr) option"
|
||||
| PDPointerTableCap machine_word "(asid * vptr) option"
|
||||
| PML4Cap machine_word "asid option"
|
||||
|
||||
primrec
|
||||
capVPIsDevice :: "arch_capability \<Rightarrow> bool"
|
||||
where
|
||||
"capVPIsDevice (PageCap v0 v1 v2 v3 v4 v5) = v4"
|
||||
|
||||
primrec
|
||||
capVPBasePtr :: "arch_capability \<Rightarrow> machine_word"
|
||||
where
|
||||
"capVPBasePtr (PageCap v0 v1 v2 v3 v4 v5) = v0"
|
||||
|
||||
primrec
|
||||
capASIDPool :: "arch_capability \<Rightarrow> machine_word"
|
||||
where
|
||||
"capASIDPool (ASIDPoolCap v0 v1) = v0"
|
||||
|
||||
primrec
|
||||
capPDBasePtr :: "arch_capability \<Rightarrow> machine_word"
|
||||
where
|
||||
"capPDBasePtr (PageDirectoryCap v0 v1) = v0"
|
||||
|
||||
primrec
|
||||
capVPRights :: "arch_capability \<Rightarrow> vmrights"
|
||||
where
|
||||
"capVPRights (PageCap v0 v1 v2 v3 v4 v5) = v1"
|
||||
|
||||
primrec
|
||||
capPTMappedAddress :: "arch_capability \<Rightarrow> (asid * vptr) option"
|
||||
where
|
||||
"capPTMappedAddress (PageTableCap v0 v1) = v1"
|
||||
|
||||
primrec
|
||||
capIOPortFirstPort :: "arch_capability \<Rightarrow> ioport"
|
||||
where
|
||||
"capIOPortFirstPort (IOPortCap v0 v1) = v0"
|
||||
|
||||
primrec
|
||||
capPML4MappedASID :: "arch_capability \<Rightarrow> asid option"
|
||||
where
|
||||
"capPML4MappedASID (PML4Cap v0 v1) = v1"
|
||||
|
||||
primrec
|
||||
capPML4BasePtr :: "arch_capability \<Rightarrow> machine_word"
|
||||
where
|
||||
"capPML4BasePtr (PML4Cap v0 v1) = v0"
|
||||
|
||||
primrec
|
||||
capASIDBase :: "arch_capability \<Rightarrow> asid"
|
||||
where
|
||||
"capASIDBase (ASIDPoolCap v0 v1) = v1"
|
||||
|
||||
primrec
|
||||
capPDPTBasePtr :: "arch_capability \<Rightarrow> machine_word"
|
||||
where
|
||||
"capPDPTBasePtr (PDPointerTableCap v0 v1) = v0"
|
||||
|
||||
primrec
|
||||
capPDPTMappedAddress :: "arch_capability \<Rightarrow> (asid * vptr) option"
|
||||
where
|
||||
"capPDPTMappedAddress (PDPointerTableCap v0 v1) = v1"
|
||||
|
||||
primrec
|
||||
capIOPortLastPort :: "arch_capability \<Rightarrow> ioport"
|
||||
where
|
||||
"capIOPortLastPort (IOPortCap v0 v1) = v1"
|
||||
|
||||
primrec
|
||||
capPTBasePtr :: "arch_capability \<Rightarrow> machine_word"
|
||||
where
|
||||
"capPTBasePtr (PageTableCap v0 v1) = v0"
|
||||
|
||||
primrec
|
||||
capVPMapType :: "arch_capability \<Rightarrow> vmmap_type"
|
||||
where
|
||||
"capVPMapType (PageCap v0 v1 v2 v3 v4 v5) = v2"
|
||||
|
||||
primrec
|
||||
capPDMappedAddress :: "arch_capability \<Rightarrow> (asid * vptr) option"
|
||||
where
|
||||
"capPDMappedAddress (PageDirectoryCap v0 v1) = v1"
|
||||
|
||||
primrec
|
||||
capVPSize :: "arch_capability \<Rightarrow> vmpage_size"
|
||||
where
|
||||
"capVPSize (PageCap v0 v1 v2 v3 v4 v5) = v3"
|
||||
|
||||
primrec
|
||||
capVPMappedAddress :: "arch_capability \<Rightarrow> (asid * vptr) option"
|
||||
where
|
||||
"capVPMappedAddress (PageCap v0 v1 v2 v3 v4 v5) = v5"
|
||||
|
||||
primrec
|
||||
capVPIsDevice_update :: "(bool \<Rightarrow> bool) \<Rightarrow> arch_capability \<Rightarrow> arch_capability"
|
||||
where
|
||||
"capVPIsDevice_update f (PageCap v0 v1 v2 v3 v4 v5) = PageCap v0 v1 v2 v3 (f v4) v5"
|
||||
|
||||
primrec
|
||||
capVPBasePtr_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> arch_capability \<Rightarrow> arch_capability"
|
||||
where
|
||||
"capVPBasePtr_update f (PageCap v0 v1 v2 v3 v4 v5) = PageCap (f v0) v1 v2 v3 v4 v5"
|
||||
|
||||
primrec
|
||||
capASIDPool_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> arch_capability \<Rightarrow> arch_capability"
|
||||
where
|
||||
"capASIDPool_update f (ASIDPoolCap v0 v1) = ASIDPoolCap (f v0) v1"
|
||||
|
||||
primrec
|
||||
capPDBasePtr_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> arch_capability \<Rightarrow> arch_capability"
|
||||
where
|
||||
"capPDBasePtr_update f (PageDirectoryCap v0 v1) = PageDirectoryCap (f v0) v1"
|
||||
|
||||
primrec
|
||||
capVPRights_update :: "(vmrights \<Rightarrow> vmrights) \<Rightarrow> arch_capability \<Rightarrow> arch_capability"
|
||||
where
|
||||
"capVPRights_update f (PageCap v0 v1 v2 v3 v4 v5) = PageCap v0 (f v1) v2 v3 v4 v5"
|
||||
|
||||
primrec
|
||||
capPTMappedAddress_update :: "(((asid * vptr) option) \<Rightarrow> ((asid * vptr) option)) \<Rightarrow> arch_capability \<Rightarrow> arch_capability"
|
||||
where
|
||||
"capPTMappedAddress_update f (PageTableCap v0 v1) = PageTableCap v0 (f v1)"
|
||||
|
||||
primrec
|
||||
capIOPortFirstPort_update :: "(ioport \<Rightarrow> ioport) \<Rightarrow> arch_capability \<Rightarrow> arch_capability"
|
||||
where
|
||||
"capIOPortFirstPort_update f (IOPortCap v0 v1) = IOPortCap (f v0) v1"
|
||||
|
||||
primrec
|
||||
capPML4MappedASID_update :: "((asid option) \<Rightarrow> (asid option)) \<Rightarrow> arch_capability \<Rightarrow> arch_capability"
|
||||
where
|
||||
"capPML4MappedASID_update f (PML4Cap v0 v1) = PML4Cap v0 (f v1)"
|
||||
|
||||
primrec
|
||||
capPML4BasePtr_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> arch_capability \<Rightarrow> arch_capability"
|
||||
where
|
||||
"capPML4BasePtr_update f (PML4Cap v0 v1) = PML4Cap (f v0) v1"
|
||||
|
||||
primrec
|
||||
capASIDBase_update :: "(asid \<Rightarrow> asid) \<Rightarrow> arch_capability \<Rightarrow> arch_capability"
|
||||
where
|
||||
"capASIDBase_update f (ASIDPoolCap v0 v1) = ASIDPoolCap v0 (f v1)"
|
||||
|
||||
primrec
|
||||
capPDPTBasePtr_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> arch_capability \<Rightarrow> arch_capability"
|
||||
where
|
||||
"capPDPTBasePtr_update f (PDPointerTableCap v0 v1) = PDPointerTableCap (f v0) v1"
|
||||
|
||||
primrec
|
||||
capPDPTMappedAddress_update :: "(((asid * vptr) option) \<Rightarrow> ((asid * vptr) option)) \<Rightarrow> arch_capability \<Rightarrow> arch_capability"
|
||||
where
|
||||
"capPDPTMappedAddress_update f (PDPointerTableCap v0 v1) = PDPointerTableCap v0 (f v1)"
|
||||
|
||||
primrec
|
||||
capIOPortLastPort_update :: "(ioport \<Rightarrow> ioport) \<Rightarrow> arch_capability \<Rightarrow> arch_capability"
|
||||
where
|
||||
"capIOPortLastPort_update f (IOPortCap v0 v1) = IOPortCap v0 (f v1)"
|
||||
|
||||
primrec
|
||||
capPTBasePtr_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> arch_capability \<Rightarrow> arch_capability"
|
||||
where
|
||||
"capPTBasePtr_update f (PageTableCap v0 v1) = PageTableCap (f v0) v1"
|
||||
|
||||
primrec
|
||||
capVPMapType_update :: "(vmmap_type \<Rightarrow> vmmap_type) \<Rightarrow> arch_capability \<Rightarrow> arch_capability"
|
||||
where
|
||||
"capVPMapType_update f (PageCap v0 v1 v2 v3 v4 v5) = PageCap v0 v1 (f v2) v3 v4 v5"
|
||||
|
||||
primrec
|
||||
capPDMappedAddress_update :: "(((asid * vptr) option) \<Rightarrow> ((asid * vptr) option)) \<Rightarrow> arch_capability \<Rightarrow> arch_capability"
|
||||
where
|
||||
"capPDMappedAddress_update f (PageDirectoryCap v0 v1) = PageDirectoryCap v0 (f v1)"
|
||||
|
||||
primrec
|
||||
capVPSize_update :: "(vmpage_size \<Rightarrow> vmpage_size) \<Rightarrow> arch_capability \<Rightarrow> arch_capability"
|
||||
where
|
||||
"capVPSize_update f (PageCap v0 v1 v2 v3 v4 v5) = PageCap v0 v1 v2 (f v3) v4 v5"
|
||||
|
||||
primrec
|
||||
capVPMappedAddress_update :: "(((asid * vptr) option) \<Rightarrow> ((asid * vptr) option)) \<Rightarrow> arch_capability \<Rightarrow> arch_capability"
|
||||
where
|
||||
"capVPMappedAddress_update f (PageCap v0 v1 v2 v3 v4 v5) = PageCap v0 v1 v2 v3 v4 (f v5)"
|
||||
|
||||
abbreviation (input)
|
||||
ASIDPoolCap_trans :: "(machine_word) \<Rightarrow> (asid) \<Rightarrow> arch_capability" ("ASIDPoolCap'_ \<lparr> capASIDPool= _, capASIDBase= _ \<rparr>")
|
||||
where
|
||||
"ASIDPoolCap_ \<lparr> capASIDPool= v0, capASIDBase= v1 \<rparr> == ASIDPoolCap v0 v1"
|
||||
|
||||
abbreviation (input)
|
||||
IOPortCap_trans :: "(ioport) \<Rightarrow> (ioport) \<Rightarrow> arch_capability" ("IOPortCap'_ \<lparr> capIOPortFirstPort= _, capIOPortLastPort= _ \<rparr>")
|
||||
where
|
||||
"IOPortCap_ \<lparr> capIOPortFirstPort= v0, capIOPortLastPort= v1 \<rparr> == IOPortCap v0 v1"
|
||||
|
||||
abbreviation (input)
|
||||
PageCap_trans :: "(machine_word) \<Rightarrow> (vmrights) \<Rightarrow> (vmmap_type) \<Rightarrow> (vmpage_size) \<Rightarrow> (bool) \<Rightarrow> ((asid * vptr) option) \<Rightarrow> arch_capability" ("PageCap'_ \<lparr> capVPBasePtr= _, capVPRights= _, capVPMapType= _, capVPSize= _, capVPIsDevice= _, capVPMappedAddress= _ \<rparr>")
|
||||
where
|
||||
"PageCap_ \<lparr> capVPBasePtr= v0, capVPRights= v1, capVPMapType= v2, capVPSize= v3, capVPIsDevice= v4, capVPMappedAddress= v5 \<rparr> == PageCap v0 v1 v2 v3 v4 v5"
|
||||
|
||||
abbreviation (input)
|
||||
PageTableCap_trans :: "(machine_word) \<Rightarrow> ((asid * vptr) option) \<Rightarrow> arch_capability" ("PageTableCap'_ \<lparr> capPTBasePtr= _, capPTMappedAddress= _ \<rparr>")
|
||||
where
|
||||
"PageTableCap_ \<lparr> capPTBasePtr= v0, capPTMappedAddress= v1 \<rparr> == PageTableCap v0 v1"
|
||||
|
||||
abbreviation (input)
|
||||
PageDirectoryCap_trans :: "(machine_word) \<Rightarrow> ((asid * vptr) option) \<Rightarrow> arch_capability" ("PageDirectoryCap'_ \<lparr> capPDBasePtr= _, capPDMappedAddress= _ \<rparr>")
|
||||
where
|
||||
"PageDirectoryCap_ \<lparr> capPDBasePtr= v0, capPDMappedAddress= v1 \<rparr> == PageDirectoryCap v0 v1"
|
||||
|
||||
abbreviation (input)
|
||||
PDPointerTableCap_trans :: "(machine_word) \<Rightarrow> ((asid * vptr) option) \<Rightarrow> arch_capability" ("PDPointerTableCap'_ \<lparr> capPDPTBasePtr= _, capPDPTMappedAddress= _ \<rparr>")
|
||||
where
|
||||
"PDPointerTableCap_ \<lparr> capPDPTBasePtr= v0, capPDPTMappedAddress= v1 \<rparr> == PDPointerTableCap v0 v1"
|
||||
|
||||
abbreviation (input)
|
||||
PML4Cap_trans :: "(machine_word) \<Rightarrow> (asid option) \<Rightarrow> arch_capability" ("PML4Cap'_ \<lparr> capPML4BasePtr= _, capPML4MappedASID= _ \<rparr>")
|
||||
where
|
||||
"PML4Cap_ \<lparr> capPML4BasePtr= v0, capPML4MappedASID= v1 \<rparr> == PML4Cap v0 v1"
|
||||
|
||||
definition
|
||||
isASIDPoolCap :: "arch_capability \<Rightarrow> bool"
|
||||
where
|
||||
"isASIDPoolCap v \<equiv> case v of
|
||||
ASIDPoolCap v0 v1 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isASIDControlCap :: "arch_capability \<Rightarrow> bool"
|
||||
where
|
||||
"isASIDControlCap v \<equiv> case v of
|
||||
ASIDControlCap \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isIOPortCap :: "arch_capability \<Rightarrow> bool"
|
||||
where
|
||||
"isIOPortCap v \<equiv> case v of
|
||||
IOPortCap v0 v1 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isPageCap :: "arch_capability \<Rightarrow> bool"
|
||||
where
|
||||
"isPageCap v \<equiv> case v of
|
||||
PageCap v0 v1 v2 v3 v4 v5 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isPageTableCap :: "arch_capability \<Rightarrow> bool"
|
||||
where
|
||||
"isPageTableCap v \<equiv> case v of
|
||||
PageTableCap v0 v1 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isPageDirectoryCap :: "arch_capability \<Rightarrow> bool"
|
||||
where
|
||||
"isPageDirectoryCap v \<equiv> case v of
|
||||
PageDirectoryCap v0 v1 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isPDPointerTableCap :: "arch_capability \<Rightarrow> bool"
|
||||
where
|
||||
"isPDPointerTableCap v \<equiv> case v of
|
||||
PDPointerTableCap v0 v1 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isPML4Cap :: "arch_capability \<Rightarrow> bool"
|
||||
where
|
||||
"isPML4Cap v \<equiv> case v of
|
||||
PML4Cap v0 v1 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
datatype asidpool =
|
||||
ASIDPool "asid \<Rightarrow> ((machine_word) option)"
|
||||
|
||||
datatype arch_kernel_object =
|
||||
KOASIDPool asidpool
|
||||
| KOPTE pte
|
||||
| KOPDE pde
|
||||
| KOPDPTE pdpte
|
||||
| KOPML4E pml4e
|
||||
|
||||
datatype arch_tcb =
|
||||
ArchThread user_context
|
||||
|
||||
primrec
|
||||
atcbContext :: "arch_tcb \<Rightarrow> user_context"
|
||||
where
|
||||
"atcbContext (ArchThread v0) = v0"
|
||||
|
||||
primrec
|
||||
atcbContext_update :: "(user_context \<Rightarrow> user_context) \<Rightarrow> arch_tcb \<Rightarrow> arch_tcb"
|
||||
where
|
||||
"atcbContext_update f (ArchThread v0) = ArchThread (f v0)"
|
||||
|
||||
abbreviation (input)
|
||||
ArchThread_trans :: "(user_context) \<Rightarrow> arch_tcb" ("ArchThread'_ \<lparr> atcbContext= _ \<rparr>")
|
||||
where
|
||||
"ArchThread_ \<lparr> atcbContext= v0 \<rparr> == ArchThread v0"
|
||||
|
||||
lemma atcbContext_atcbContext_update [simp]:
|
||||
"atcbContext (atcbContext_update f v) = f (atcbContext v)"
|
||||
by (cases v) simp
|
||||
|
||||
datatype cr3 =
|
||||
CR3 paddr asid
|
||||
|
||||
primrec
|
||||
cr3BaseAddress :: "cr3 \<Rightarrow> paddr"
|
||||
where
|
||||
"cr3BaseAddress (CR3 v0 v1) = v0"
|
||||
|
||||
primrec
|
||||
cr3pcid :: "cr3 \<Rightarrow> asid"
|
||||
where
|
||||
"cr3pcid (CR3 v0 v1) = v1"
|
||||
|
||||
primrec
|
||||
cr3BaseAddress_update :: "(paddr \<Rightarrow> paddr) \<Rightarrow> cr3 \<Rightarrow> cr3"
|
||||
where
|
||||
"cr3BaseAddress_update f (CR3 v0 v1) = CR3 (f v0) v1"
|
||||
|
||||
primrec
|
||||
cr3pcid_update :: "(asid \<Rightarrow> asid) \<Rightarrow> cr3 \<Rightarrow> cr3"
|
||||
where
|
||||
"cr3pcid_update f (CR3 v0 v1) = CR3 v0 (f v1)"
|
||||
|
||||
abbreviation (input)
|
||||
CR3_trans :: "(paddr) \<Rightarrow> (asid) \<Rightarrow> cr3" ("CR3'_ \<lparr> cr3BaseAddress= _, cr3pcid= _ \<rparr>")
|
||||
where
|
||||
"CR3_ \<lparr> cr3BaseAddress= v0, cr3pcid= v1 \<rparr> == CR3 v0 v1"
|
||||
|
||||
lemma cr3BaseAddress_cr3BaseAddress_update [simp]:
|
||||
"cr3BaseAddress (cr3BaseAddress_update f v) = f (cr3BaseAddress v)"
|
||||
by (cases v) simp
|
||||
|
||||
lemma cr3BaseAddress_cr3pcid_update [simp]:
|
||||
"cr3BaseAddress (cr3pcid_update f v) = cr3BaseAddress v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma cr3pcid_cr3BaseAddress_update [simp]:
|
||||
"cr3pcid (cr3BaseAddress_update f v) = cr3pcid v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma cr3pcid_cr3pcid_update [simp]:
|
||||
"cr3pcid (cr3pcid_update f v) = f (cr3pcid v)"
|
||||
by (cases v) simp
|
||||
|
||||
consts'
|
||||
archObjSize :: "arch_kernel_object \<Rightarrow> nat"
|
||||
|
||||
consts'
|
||||
atcbContextSet :: "user_context \<Rightarrow> arch_tcb \<Rightarrow> arch_tcb"
|
||||
|
||||
consts'
|
||||
atcbContextGet :: "arch_tcb \<Rightarrow> user_context"
|
||||
|
||||
consts'
|
||||
asidHighBits :: "nat"
|
||||
|
||||
consts'
|
||||
asidLowBits :: "nat"
|
||||
|
||||
consts'
|
||||
asidBits :: "nat"
|
||||
|
||||
consts'
|
||||
asidRange :: "(asid * asid)"
|
||||
|
||||
consts'
|
||||
asidHighBitsOf :: "asid \<Rightarrow> asid"
|
||||
|
||||
defs archObjSize_def:
|
||||
"archObjSize a\<equiv> (case a of
|
||||
KOASIDPool v16 \<Rightarrow> pageBits
|
||||
| KOPTE v17 \<Rightarrow> 3
|
||||
| KOPDE v18 \<Rightarrow> 3
|
||||
| KOPDPTE v19 \<Rightarrow> 3
|
||||
| KOPML4E v20 \<Rightarrow> 3
|
||||
)"
|
||||
|
||||
definition
|
||||
"newArchTCB \<equiv> ArchThread_ \<lparr>
|
||||
atcbContext= newContext \<rparr>"
|
||||
|
||||
defs atcbContextSet_def:
|
||||
"atcbContextSet uc atcb \<equiv> atcb \<lparr> atcbContext := uc \<rparr>"
|
||||
|
||||
defs atcbContextGet_def:
|
||||
"atcbContextGet \<equiv> atcbContext"
|
||||
|
||||
defs asidHighBits_def:
|
||||
"asidHighBits \<equiv> 3"
|
||||
|
||||
defs asidLowBits_def:
|
||||
"asidLowBits \<equiv> 9"
|
||||
|
||||
defs asidBits_def:
|
||||
"asidBits \<equiv> asidHighBits + asidLowBits"
|
||||
|
||||
defs asidRange_def:
|
||||
"asidRange\<equiv> (0, (1 `~shiftL~` asidBits) - 1)"
|
||||
|
||||
defs asidHighBitsOf_def:
|
||||
"asidHighBitsOf asid\<equiv> (asid `~shiftR~` asidLowBits) && mask asidHighBits"
|
||||
|
||||
|
||||
datatype arch_kernel_object_type =
|
||||
PDET
|
||||
| PTET
|
||||
| PDPTET
|
||||
| PML4ET
|
||||
| ASIDPoolT
|
||||
|
||||
primrec
|
||||
archTypeOf :: "arch_kernel_object \<Rightarrow> arch_kernel_object_type"
|
||||
where
|
||||
"archTypeOf (KOPDE e) = PDET"
|
||||
| "archTypeOf (KOPTE e) = PTET"
|
||||
| "archTypeOf (KOPDPTE e) = PDPTET"
|
||||
| "archTypeOf (KOPML4E e) = PML4ET"
|
||||
| "archTypeOf (KOASIDPool e) = ASIDPoolT"
|
||||
|
||||
end
|
||||
end
|
||||
|
|
@ -1,68 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file ArchTCB_H.thy *)
|
||||
(*
|
||||
* Copyright 2014, General Dynamics C4 Systems
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_GPLv2.txt" for details.
|
||||
*
|
||||
* @TAG(GD_GPL)
|
||||
*)
|
||||
|
||||
theory ArchTCB_H
|
||||
imports "../TCBDecls_H"
|
||||
begin
|
||||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
definition
|
||||
decodeTransfer :: "word8 \<Rightarrow> ( syscall_error , copy_register_sets ) kernel_f"
|
||||
where
|
||||
"decodeTransfer arg1 \<equiv> returnOk X64NoExtraRegisters"
|
||||
|
||||
definition
|
||||
performTransfer :: "copy_register_sets \<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow> unit kernel"
|
||||
where
|
||||
"performTransfer arg1 arg2 arg3 \<equiv> return ()"
|
||||
|
||||
definition
|
||||
sanitiseOrFlags :: "machine_word"
|
||||
where
|
||||
"sanitiseOrFlags \<equiv> (1 << 1) || bit 9"
|
||||
|
||||
definition
|
||||
sanitiseAndFlags :: "machine_word"
|
||||
where
|
||||
"sanitiseAndFlags\<equiv> ((1 << 12) - 1) && (complement (bit 3)) && (complement (bit 5)) && (complement (bit 8))"
|
||||
|
||||
definition
|
||||
sanitiseRegister :: "tcb \<Rightarrow> register \<Rightarrow> machine_word \<Rightarrow> machine_word"
|
||||
where
|
||||
"sanitiseRegister arg1 r v \<equiv>
|
||||
let val = if r = FaultIP \<or> r = NextIP then
|
||||
if v > 0x00007fffffffffff \<and> v < 0xffff800000000000 then 0 else v
|
||||
else v;
|
||||
val' = if r = TLS_BASE then if val > 0x00007fffffffffff then 0x00007fffffffffff else val else val
|
||||
in
|
||||
if r = FLAGS then
|
||||
(val' || sanitiseOrFlags) && sanitiseAndFlags
|
||||
else val'"
|
||||
|
||||
|
||||
definition
|
||||
archThreadGet :: "(arch_tcb \<Rightarrow> 'a) \<Rightarrow> machine_word \<Rightarrow> 'a kernel"
|
||||
where
|
||||
"archThreadGet f tptr\<equiv> liftM (f \<circ> tcbArch) $ getObject tptr"
|
||||
|
||||
definition
|
||||
archThreadSet :: "(arch_tcb \<Rightarrow> arch_tcb) \<Rightarrow> machine_word \<Rightarrow> unit kernel"
|
||||
where
|
||||
"archThreadSet f tptr\<equiv> (do
|
||||
tcb \<leftarrow> getObject tptr;
|
||||
setObject tptr $ tcb \<lparr> tcbArch := f (tcbArch tcb) \<rparr>
|
||||
od)"
|
||||
|
||||
|
||||
end
|
||||
end
|
||||
|
|
@ -1,43 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file ArchThreadDecls_H.thy *)
|
||||
(*
|
||||
* 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)
|
||||
*)
|
||||
|
||||
(*
|
||||
Declarations from SEL4.Kernel.Thread.
|
||||
*)
|
||||
|
||||
chapter "Function Declarations for Threads"
|
||||
|
||||
theory ArchThreadDecls_H
|
||||
imports
|
||||
"../Structures_H"
|
||||
"../FaultMonad_H"
|
||||
"../KernelInitMonad_H"
|
||||
begin
|
||||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
consts'
|
||||
switchToThread :: "machine_word \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
configureIdleThread :: "machine_word \<Rightarrow> unit kernel_init"
|
||||
|
||||
consts'
|
||||
switchToIdleThread :: "unit kernel"
|
||||
|
||||
consts'
|
||||
activateIdleThread :: "machine_word \<Rightarrow> unit kernel"
|
||||
|
||||
|
||||
end (* context X64 *)
|
||||
|
||||
end
|
||||
|
|
@ -1,40 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file ArchThread_H.thy *)
|
||||
(*
|
||||
* 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 "Threads"
|
||||
|
||||
theory ArchThread_H
|
||||
imports
|
||||
ArchThreadDecls_H
|
||||
"../TCBDecls_H"
|
||||
ArchVSpaceDecls_H
|
||||
begin
|
||||
|
||||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
defs switchToThread_def:
|
||||
"switchToThread tcb \<equiv> setVMRoot tcb"
|
||||
|
||||
defs configureIdleThread_def:
|
||||
"configureIdleThread arg1 \<equiv> error []"
|
||||
|
||||
defs switchToIdleThread_def:
|
||||
"switchToIdleThread\<equiv> return ()"
|
||||
|
||||
defs activateIdleThread_def:
|
||||
"activateIdleThread arg1 \<equiv> return ()"
|
||||
|
||||
|
||||
end (* context X64 *)
|
||||
|
||||
end
|
||||
|
|
@ -1,213 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file ArchTypes_H.thy *)
|
||||
(*
|
||||
* 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 visible in the API.
|
||||
*)
|
||||
|
||||
chapter "Arch-dependant Types visible in the API"
|
||||
|
||||
theory ArchTypes_H
|
||||
imports
|
||||
State_H
|
||||
Hardware_H
|
||||
"../../../lib/Lib"
|
||||
begin
|
||||
|
||||
datatype apiobject_type =
|
||||
Untyped
|
||||
| TCBObject
|
||||
| EndpointObject
|
||||
| NotificationObject
|
||||
| CapTableObject
|
||||
(* apiobject_type instance proofs *)
|
||||
(*<*)
|
||||
instantiation apiobject_type :: enum begin
|
||||
definition
|
||||
enum_apiobject_type: "enum_class.enum \<equiv>
|
||||
[
|
||||
Untyped,
|
||||
TCBObject,
|
||||
EndpointObject,
|
||||
NotificationObject,
|
||||
CapTableObject
|
||||
]"
|
||||
|
||||
|
||||
definition
|
||||
"enum_class.enum_all (P :: apiobject_type \<Rightarrow> bool) \<longleftrightarrow> Ball UNIV P"
|
||||
|
||||
definition
|
||||
"enum_class.enum_ex (P :: apiobject_type \<Rightarrow> bool) \<longleftrightarrow> Bex UNIV P"
|
||||
|
||||
instance
|
||||
apply intro_classes
|
||||
apply (safe, simp)
|
||||
apply (case_tac x)
|
||||
apply (simp_all add: enum_apiobject_type enum_all_apiobject_type_def enum_ex_apiobject_type_def)
|
||||
by fast+
|
||||
end
|
||||
|
||||
instantiation apiobject_type :: enum_alt
|
||||
begin
|
||||
definition
|
||||
enum_alt_apiobject_type: "enum_alt \<equiv>
|
||||
alt_from_ord (enum :: apiobject_type list)"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation apiobject_type :: enumeration_both
|
||||
begin
|
||||
instance by (intro_classes, simp add: enum_alt_apiobject_type)
|
||||
end
|
||||
|
||||
(*>*)
|
||||
|
||||
|
||||
definition
|
||||
tcbBlockSizeBits :: "nat"
|
||||
where
|
||||
"tcbBlockSizeBits \<equiv> 9"
|
||||
|
||||
definition
|
||||
epSizeBits :: "nat"
|
||||
where
|
||||
"epSizeBits \<equiv> 5"
|
||||
|
||||
definition
|
||||
ntfnSizeBits :: "nat"
|
||||
where
|
||||
"ntfnSizeBits \<equiv> 5"
|
||||
|
||||
definition
|
||||
cteSizeBits :: "nat"
|
||||
where
|
||||
"cteSizeBits \<equiv> 5"
|
||||
|
||||
definition
|
||||
apiGetObjectSize :: "apiobject_type \<Rightarrow> nat \<Rightarrow> nat"
|
||||
where
|
||||
"apiGetObjectSize x0 magnitude\<equiv> (case x0 of
|
||||
Untyped \<Rightarrow> magnitude
|
||||
| TCBObject \<Rightarrow> tcbBlockSizeBits
|
||||
| EndpointObject \<Rightarrow> epSizeBits
|
||||
| NotificationObject \<Rightarrow> ntfnSizeBits
|
||||
| CapTableObject \<Rightarrow> cteSizeBits + magnitude
|
||||
)"
|
||||
|
||||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
datatype object_type =
|
||||
APIObjectType apiobject_type
|
||||
| SmallPageObject
|
||||
| LargePageObject
|
||||
| HugePageObject
|
||||
| PageTableObject
|
||||
| PageDirectoryObject
|
||||
| PDPointerTableObject
|
||||
| PML4Object
|
||||
|
||||
definition
|
||||
"fromAPIType \<equiv> APIObjectType"
|
||||
|
||||
definition
|
||||
"toAPIType x0\<equiv> (case x0 of
|
||||
(APIObjectType a) \<Rightarrow> Just a
|
||||
| _ \<Rightarrow> Nothing
|
||||
)"
|
||||
|
||||
definition
|
||||
"pageType \<equiv> SmallPageObject"
|
||||
|
||||
definition
|
||||
getObjectSize :: "object_type \<Rightarrow> nat \<Rightarrow> nat"
|
||||
where
|
||||
"getObjectSize x0 magnitude\<equiv> (case x0 of
|
||||
SmallPageObject \<Rightarrow> pageBitsForSize X64SmallPage
|
||||
| LargePageObject \<Rightarrow> pageBitsForSize X64LargePage
|
||||
| HugePageObject \<Rightarrow> pageBitsForSize X64HugePage
|
||||
| PageTableObject \<Rightarrow> ptBits
|
||||
| PageDirectoryObject \<Rightarrow> ptBits
|
||||
| PDPointerTableObject \<Rightarrow> ptBits
|
||||
| PML4Object \<Rightarrow> ptBits
|
||||
| (APIObjectType apiObjectType) \<Rightarrow> apiGetObjectSize apiObjectType magnitude
|
||||
)"
|
||||
|
||||
definition
|
||||
isFrameType :: "object_type \<Rightarrow> bool"
|
||||
where
|
||||
"isFrameType x0\<equiv> (case x0 of
|
||||
SmallPageObject \<Rightarrow> True
|
||||
| LargePageObject \<Rightarrow> True
|
||||
| HugePageObject \<Rightarrow> True
|
||||
| _ \<Rightarrow> False
|
||||
)"
|
||||
|
||||
|
||||
end
|
||||
|
||||
text {* object\_type instance proofs *}
|
||||
|
||||
qualify X64_H (in Arch)
|
||||
instantiation X64_H.object_type :: enum
|
||||
begin
|
||||
interpretation Arch .
|
||||
definition
|
||||
enum_object_type: "enum_class.enum \<equiv>
|
||||
map APIObjectType (enum_class.enum :: apiobject_type list) @
|
||||
[SmallPageObject,
|
||||
LargePageObject,
|
||||
HugePageObject,
|
||||
PageTableObject,
|
||||
PageDirectoryObject,
|
||||
PDPointerTableObject,
|
||||
PML4Object
|
||||
]"
|
||||
|
||||
definition
|
||||
"enum_class.enum_all (P :: object_type \<Rightarrow> bool) \<longleftrightarrow> Ball UNIV P"
|
||||
|
||||
definition
|
||||
"enum_class.enum_ex (P :: object_type \<Rightarrow> bool) \<longleftrightarrow> Bex UNIV P"
|
||||
|
||||
instance
|
||||
apply intro_classes
|
||||
apply (safe, simp)
|
||||
apply (case_tac x)
|
||||
apply (simp_all add: enum_object_type)
|
||||
apply (auto intro: distinct_map_enum
|
||||
simp: enum_all_object_type_def enum_ex_object_type_def)
|
||||
done
|
||||
end
|
||||
|
||||
|
||||
instantiation X64_H.object_type :: enum_alt
|
||||
begin
|
||||
interpretation Arch .
|
||||
definition
|
||||
enum_alt_object_type: "enum_alt \<equiv>
|
||||
alt_from_ord (enum :: object_type list)"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation X64_H.object_type :: enumeration_both
|
||||
begin
|
||||
interpretation Arch .
|
||||
instance by (intro_classes, simp add: enum_alt_object_type)
|
||||
end
|
||||
|
||||
context begin interpretation Arch .
|
||||
requalify_types object_type
|
||||
end
|
||||
|
||||
end
|
||||
|
|
@ -1,285 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file ArchVSpaceDecls_H.thy *)
|
||||
(*
|
||||
* 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 "Retyping Objects"
|
||||
|
||||
theory ArchVSpaceDecls_H
|
||||
imports ArchRetypeDecls_H "../InvocationLabels_H"
|
||||
begin
|
||||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
consts'
|
||||
kernelBase :: "vptr"
|
||||
|
||||
consts'
|
||||
globalsBase :: "vptr"
|
||||
|
||||
consts'
|
||||
idleThreadStart :: "vptr"
|
||||
|
||||
consts'
|
||||
copyGlobalMappings :: "machine_word \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
createMappingEntries :: "paddr \<Rightarrow> vptr \<Rightarrow> vmpage_size \<Rightarrow> vmrights \<Rightarrow> vmattributes \<Rightarrow> machine_word \<Rightarrow> ( syscall_error , (vmpage_entry * vmpage_entry_ptr) ) kernel_f"
|
||||
|
||||
consts'
|
||||
ensureSafeMapping :: "(vmpage_entry * vmpage_entry_ptr) \<Rightarrow> ( syscall_error , unit ) kernel_f"
|
||||
|
||||
consts'
|
||||
lookupIPCBuffer :: "bool \<Rightarrow> machine_word \<Rightarrow> ((machine_word) option) kernel"
|
||||
|
||||
consts'
|
||||
findVSpaceForASID :: "asid \<Rightarrow> ( lookup_failure , (machine_word) ) kernel_f"
|
||||
|
||||
consts'
|
||||
findVSpaceForASIDAssert :: "asid \<Rightarrow> (machine_word) kernel"
|
||||
|
||||
consts'
|
||||
checkPML4At :: "machine_word \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
checkPDPTAt :: "machine_word \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
checkPDAt :: "machine_word \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
checkPTAt :: "machine_word \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
checkPML4ASIDMapMembership :: "machine_word \<Rightarrow> asid list \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
checkPML4UniqueToASID :: "machine_word \<Rightarrow> asid \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
checkPML4NotInASIDMap :: "machine_word \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
lookupPTSlot :: "machine_word \<Rightarrow> vptr \<Rightarrow> ( lookup_failure , (machine_word) ) kernel_f"
|
||||
|
||||
consts'
|
||||
lookupPTSlotFromPT :: "machine_word \<Rightarrow> vptr \<Rightarrow> (machine_word) kernel"
|
||||
|
||||
consts'
|
||||
lookupPDSlot :: "machine_word \<Rightarrow> vptr \<Rightarrow> ( lookup_failure , (machine_word) ) kernel_f"
|
||||
|
||||
consts'
|
||||
lookupPDSlotFromPD :: "machine_word \<Rightarrow> vptr \<Rightarrow> (machine_word) kernel"
|
||||
|
||||
consts'
|
||||
lookupPDPTSlot :: "machine_word \<Rightarrow> vptr \<Rightarrow> ( lookup_failure , (machine_word) ) kernel_f"
|
||||
|
||||
consts'
|
||||
lookupPDPTSlotFromPDPT :: "machine_word \<Rightarrow> vptr \<Rightarrow> (machine_word) kernel"
|
||||
|
||||
consts'
|
||||
lookupPML4Slot :: "machine_word \<Rightarrow> vptr \<Rightarrow> machine_word"
|
||||
|
||||
consts'
|
||||
handleVMFault :: "machine_word \<Rightarrow> vmfault_type \<Rightarrow> ( fault , unit ) kernel_f"
|
||||
|
||||
consts'
|
||||
deleteASIDPool :: "asid \<Rightarrow> machine_word \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
deleteASID :: "asid \<Rightarrow> machine_word \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
unmapPDPT :: "asid \<Rightarrow> vptr \<Rightarrow> machine_word \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
unmapPageDirectory :: "asid \<Rightarrow> vptr \<Rightarrow> machine_word \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
unmapPageTable :: "asid \<Rightarrow> vptr \<Rightarrow> machine_word \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
unmapPage :: "vmpage_size \<Rightarrow> asid \<Rightarrow> vptr \<Rightarrow> machine_word \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
checkMappingPPtr :: "machine_word \<Rightarrow> vmpage_entry \<Rightarrow> ( lookup_failure , unit ) kernel_f"
|
||||
|
||||
consts'
|
||||
getCurrentCR3 :: "cr3 kernel"
|
||||
|
||||
consts'
|
||||
setCurrentCR3 :: "cr3 \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
invalidateLocalPageStructureCacheASID :: "paddr \<Rightarrow> asid \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
invalidatePageStructureCacheASID :: "paddr \<Rightarrow> asid \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
getCurrentVSpaceRoot :: "paddr kernel"
|
||||
|
||||
consts'
|
||||
setCurrentVSpaceRoot :: "paddr \<Rightarrow> asid \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
updateASIDMap :: "asid \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
setVMRoot :: "machine_word \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
isValidVTableRoot :: "capability \<Rightarrow> bool"
|
||||
|
||||
consts'
|
||||
checkValidIPCBuffer :: "vptr \<Rightarrow> capability \<Rightarrow> ( syscall_error , unit ) kernel_f"
|
||||
|
||||
consts'
|
||||
maskVMRights :: "vmrights \<Rightarrow> cap_rights \<Rightarrow> vmrights"
|
||||
|
||||
consts'
|
||||
flushAll :: "machine_word \<Rightarrow> asid \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
flushPDPT :: "machine_word \<Rightarrow> asid \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
flushPD :: "machine_word \<Rightarrow> asid \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
flushTable :: "machine_word \<Rightarrow> vptr \<Rightarrow> machine_word \<Rightarrow> asid \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
invalidateASID' :: "asid \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
invalidateASIDEntry :: "asid \<Rightarrow> machine_word \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
attribsFromWord :: "machine_word \<Rightarrow> vmattributes"
|
||||
|
||||
consts'
|
||||
pageBase :: "vptr \<Rightarrow> vmpage_size \<Rightarrow> vptr"
|
||||
|
||||
consts'
|
||||
userVTop :: "machine_word"
|
||||
|
||||
consts'
|
||||
decodeX64FrameInvocation :: "machine_word \<Rightarrow> machine_word list \<Rightarrow> machine_word \<Rightarrow> arch_capability \<Rightarrow> (capability * machine_word) list \<Rightarrow> ( syscall_error , invocation ) kernel_f"
|
||||
|
||||
consts'
|
||||
decodeX64PDPointerTableInvocation :: "machine_word \<Rightarrow> machine_word list \<Rightarrow> machine_word \<Rightarrow> arch_capability \<Rightarrow> (capability * machine_word) list \<Rightarrow> ( syscall_error , invocation ) kernel_f"
|
||||
|
||||
consts'
|
||||
decodeX64PageDirectoryInvocation :: "machine_word \<Rightarrow> machine_word list \<Rightarrow> machine_word \<Rightarrow> arch_capability \<Rightarrow> (capability * machine_word) list \<Rightarrow> ( syscall_error , invocation ) kernel_f"
|
||||
|
||||
consts'
|
||||
decodeX64PageTableInvocation :: "machine_word \<Rightarrow> machine_word list \<Rightarrow> machine_word \<Rightarrow> arch_capability \<Rightarrow> (capability * machine_word) list \<Rightarrow> ( syscall_error , invocation ) kernel_f"
|
||||
|
||||
consts'
|
||||
decodeX64ASIDControlInvocation :: "machine_word \<Rightarrow> machine_word list \<Rightarrow> arch_capability \<Rightarrow> (capability * machine_word) list \<Rightarrow> ( syscall_error , invocation ) kernel_f"
|
||||
|
||||
consts'
|
||||
decodeX64ASIDPoolInvocation :: "machine_word \<Rightarrow> arch_capability \<Rightarrow> (capability * machine_word) list \<Rightarrow> ( syscall_error , invocation ) kernel_f"
|
||||
|
||||
consts'
|
||||
decodeX64MMUInvocation :: "machine_word \<Rightarrow> machine_word list \<Rightarrow> cptr \<Rightarrow> machine_word \<Rightarrow> arch_capability \<Rightarrow> (capability * machine_word) list \<Rightarrow> ( syscall_error , invocation ) kernel_f"
|
||||
|
||||
consts'
|
||||
checkVPAlignment :: "vmpage_size \<Rightarrow> vptr \<Rightarrow> ( syscall_error , unit ) kernel_f"
|
||||
|
||||
consts'
|
||||
checkValidMappingSize :: "vmpage_size \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
performX64MMUInvocation :: "invocation \<Rightarrow> machine_word list kernel_p"
|
||||
|
||||
consts'
|
||||
performPDPTInvocation :: "pdptinvocation \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
performPageDirectoryInvocation :: "page_directory_invocation \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
performPageTableInvocation :: "page_table_invocation \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
pteCheckIfMapped :: "machine_word \<Rightarrow> bool kernel"
|
||||
|
||||
consts'
|
||||
pdeCheckIfMapped :: "machine_word \<Rightarrow> bool kernel"
|
||||
|
||||
consts'
|
||||
performPageInvocation :: "page_invocation \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
performASIDControlInvocation :: "asidcontrol_invocation \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
performASIDPoolInvocation :: "asidpool_invocation \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
storePML4E :: "machine_word \<Rightarrow> pml4e \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
storePDPTE :: "machine_word \<Rightarrow> pdpte \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
storePDE :: "machine_word \<Rightarrow> pde \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
storePTE :: "machine_word \<Rightarrow> pte \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
mapKernelWindow :: "unit kernel"
|
||||
|
||||
consts'
|
||||
activateGlobalVSpace :: "unit kernel"
|
||||
|
||||
consts'
|
||||
createIPCBufferFrame :: "capability \<Rightarrow> vptr \<Rightarrow> capability kernel_init"
|
||||
|
||||
consts'
|
||||
createBIFrame :: "capability \<Rightarrow> vptr \<Rightarrow> word32 \<Rightarrow> word32 \<Rightarrow> capability kernel_init"
|
||||
|
||||
consts'
|
||||
createFramesOfRegion :: "capability \<Rightarrow> region \<Rightarrow> bool \<Rightarrow> unit kernel_init"
|
||||
|
||||
consts'
|
||||
createITPDPTs :: "capability \<Rightarrow> vptr \<Rightarrow> vptr \<Rightarrow> capability kernel_init"
|
||||
|
||||
consts'
|
||||
writeITPDPTs :: "capability \<Rightarrow> capability \<Rightarrow> unit kernel_init"
|
||||
|
||||
consts'
|
||||
createITASIDPool :: "capability \<Rightarrow> capability kernel_init"
|
||||
|
||||
consts'
|
||||
writeITASIDPool :: "capability \<Rightarrow> capability \<Rightarrow> unit kernel"
|
||||
|
||||
consts'
|
||||
createDeviceFrames :: "capability \<Rightarrow> unit kernel_init"
|
||||
|
||||
consts'
|
||||
vptrFromPPtr :: "machine_word \<Rightarrow> vptr kernel_init"
|
||||
|
||||
consts'
|
||||
ensurePortOperationAllowed :: "arch_capability \<Rightarrow> ioport \<Rightarrow> nat \<Rightarrow> ( syscall_error , unit ) kernel_f"
|
||||
|
||||
consts'
|
||||
decodeX64PortInvocation :: "machine_word \<Rightarrow> machine_word list \<Rightarrow> arch_capability \<Rightarrow> ( syscall_error , invocation ) kernel_f"
|
||||
|
||||
consts'
|
||||
performX64PortInvocation :: "invocation \<Rightarrow> machine_word list kernel_p"
|
||||
|
||||
|
||||
end (* context X64 *)
|
||||
|
||||
end
|
||||
File diff suppressed because it is too large
Load Diff
|
|
@ -1,34 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file Arch_Structs_B.thy *)
|
||||
(*
|
||||
* 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)
|
||||
*)
|
||||
|
||||
(* Architecture-specific data types shared by spec and abstract. *)
|
||||
|
||||
chapter "Common, Architecture-Specific Data Types"
|
||||
|
||||
theory Arch_Structs_B
|
||||
imports "~~/src/HOL/Main" "../../../spec/machine/Setup_Locale"
|
||||
begin
|
||||
(* FIXME: Clagged from X64 version *)
|
||||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
(* FIXME: add an underscore after translation of X64 prefix? *)
|
||||
datatype x64vspace_region_use =
|
||||
X64VSpaceUserRegion
|
||||
| X64VSpaceInvalidRegion
|
||||
| X64VSpaceKernelWindow
|
||||
| X64VSpaceDeviceWindow
|
||||
|
||||
|
||||
end (* context X64 *)
|
||||
|
||||
end
|
||||
|
|
@ -1,827 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file Hardware_H.thy *)
|
||||
(*
|
||||
* Copyright 2014, General Dynamics C4 Systems
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_GPLv2.txt" for details.
|
||||
*
|
||||
* @TAG(GD_GPL)
|
||||
*)
|
||||
|
||||
theory Hardware_H
|
||||
imports
|
||||
"../../machine/X64/MachineOps"
|
||||
State_H
|
||||
begin
|
||||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
type_synonym irq = "Platform.X64.irq"
|
||||
|
||||
type_synonym ioport = "word16"
|
||||
|
||||
type_synonym paddr = "Platform.X64.paddr"
|
||||
|
||||
datatype vmrights =
|
||||
VMKernelOnly
|
||||
| VMReadOnly
|
||||
| VMReadWrite
|
||||
|
||||
datatype pml4e =
|
||||
InvalidPML4E
|
||||
| PDPointerTablePML4E paddr bool bool bool bool vmrights
|
||||
|
||||
primrec
|
||||
pml4eWriteThrough :: "pml4e \<Rightarrow> bool"
|
||||
where
|
||||
"pml4eWriteThrough (PDPointerTablePML4E v0 v1 v2 v3 v4 v5) = v3"
|
||||
|
||||
primrec
|
||||
pml4eTable :: "pml4e \<Rightarrow> paddr"
|
||||
where
|
||||
"pml4eTable (PDPointerTablePML4E v0 v1 v2 v3 v4 v5) = v0"
|
||||
|
||||
primrec
|
||||
pml4eExecuteDisable :: "pml4e \<Rightarrow> bool"
|
||||
where
|
||||
"pml4eExecuteDisable (PDPointerTablePML4E v0 v1 v2 v3 v4 v5) = v4"
|
||||
|
||||
primrec
|
||||
pml4eCacheDisabled :: "pml4e \<Rightarrow> bool"
|
||||
where
|
||||
"pml4eCacheDisabled (PDPointerTablePML4E v0 v1 v2 v3 v4 v5) = v2"
|
||||
|
||||
primrec
|
||||
pml4eAccessed :: "pml4e \<Rightarrow> bool"
|
||||
where
|
||||
"pml4eAccessed (PDPointerTablePML4E v0 v1 v2 v3 v4 v5) = v1"
|
||||
|
||||
primrec
|
||||
pml4eRights :: "pml4e \<Rightarrow> vmrights"
|
||||
where
|
||||
"pml4eRights (PDPointerTablePML4E v0 v1 v2 v3 v4 v5) = v5"
|
||||
|
||||
primrec
|
||||
pml4eWriteThrough_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pml4e \<Rightarrow> pml4e"
|
||||
where
|
||||
"pml4eWriteThrough_update f (PDPointerTablePML4E v0 v1 v2 v3 v4 v5) = PDPointerTablePML4E v0 v1 v2 (f v3) v4 v5"
|
||||
|
||||
primrec
|
||||
pml4eTable_update :: "(paddr \<Rightarrow> paddr) \<Rightarrow> pml4e \<Rightarrow> pml4e"
|
||||
where
|
||||
"pml4eTable_update f (PDPointerTablePML4E v0 v1 v2 v3 v4 v5) = PDPointerTablePML4E (f v0) v1 v2 v3 v4 v5"
|
||||
|
||||
primrec
|
||||
pml4eExecuteDisable_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pml4e \<Rightarrow> pml4e"
|
||||
where
|
||||
"pml4eExecuteDisable_update f (PDPointerTablePML4E v0 v1 v2 v3 v4 v5) = PDPointerTablePML4E v0 v1 v2 v3 (f v4) v5"
|
||||
|
||||
primrec
|
||||
pml4eCacheDisabled_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pml4e \<Rightarrow> pml4e"
|
||||
where
|
||||
"pml4eCacheDisabled_update f (PDPointerTablePML4E v0 v1 v2 v3 v4 v5) = PDPointerTablePML4E v0 v1 (f v2) v3 v4 v5"
|
||||
|
||||
primrec
|
||||
pml4eAccessed_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pml4e \<Rightarrow> pml4e"
|
||||
where
|
||||
"pml4eAccessed_update f (PDPointerTablePML4E v0 v1 v2 v3 v4 v5) = PDPointerTablePML4E v0 (f v1) v2 v3 v4 v5"
|
||||
|
||||
primrec
|
||||
pml4eRights_update :: "(vmrights \<Rightarrow> vmrights) \<Rightarrow> pml4e \<Rightarrow> pml4e"
|
||||
where
|
||||
"pml4eRights_update f (PDPointerTablePML4E v0 v1 v2 v3 v4 v5) = PDPointerTablePML4E v0 v1 v2 v3 v4 (f v5)"
|
||||
|
||||
abbreviation (input)
|
||||
PDPointerTablePML4E_trans :: "(paddr) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (vmrights) \<Rightarrow> pml4e" ("PDPointerTablePML4E'_ \<lparr> pml4eTable= _, pml4eAccessed= _, pml4eCacheDisabled= _, pml4eWriteThrough= _, pml4eExecuteDisable= _, pml4eRights= _ \<rparr>")
|
||||
where
|
||||
"PDPointerTablePML4E_ \<lparr> pml4eTable= v0, pml4eAccessed= v1, pml4eCacheDisabled= v2, pml4eWriteThrough= v3, pml4eExecuteDisable= v4, pml4eRights= v5 \<rparr> == PDPointerTablePML4E v0 v1 v2 v3 v4 v5"
|
||||
|
||||
definition
|
||||
isInvalidPML4E :: "pml4e \<Rightarrow> bool"
|
||||
where
|
||||
"isInvalidPML4E v \<equiv> case v of
|
||||
InvalidPML4E \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isPDPointerTablePML4E :: "pml4e \<Rightarrow> bool"
|
||||
where
|
||||
"isPDPointerTablePML4E v \<equiv> case v of
|
||||
PDPointerTablePML4E v0 v1 v2 v3 v4 v5 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
datatype pdpte =
|
||||
InvalidPDPTE
|
||||
| PageDirectoryPDPTE paddr bool bool bool bool vmrights
|
||||
| HugePagePDPTE paddr bool bool bool bool bool bool bool vmrights
|
||||
|
||||
primrec
|
||||
pdpteAccessed :: "pdpte \<Rightarrow> bool"
|
||||
where
|
||||
"pdpteAccessed (HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v4"
|
||||
| "pdpteAccessed (PageDirectoryPDPTE v0 v1 v2 v3 v4 v5) = v1"
|
||||
|
||||
primrec
|
||||
pdpteGlobal :: "pdpte \<Rightarrow> bool"
|
||||
where
|
||||
"pdpteGlobal (HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v1"
|
||||
|
||||
primrec
|
||||
pdpteWriteThrough :: "pdpte \<Rightarrow> bool"
|
||||
where
|
||||
"pdpteWriteThrough (HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v6"
|
||||
| "pdpteWriteThrough (PageDirectoryPDPTE v0 v1 v2 v3 v4 v5) = v3"
|
||||
|
||||
primrec
|
||||
pdpteExecuteDisable :: "pdpte \<Rightarrow> bool"
|
||||
where
|
||||
"pdpteExecuteDisable (HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v7"
|
||||
| "pdpteExecuteDisable (PageDirectoryPDPTE v0 v1 v2 v3 v4 v5) = v4"
|
||||
|
||||
primrec
|
||||
pdpteTable :: "pdpte \<Rightarrow> paddr"
|
||||
where
|
||||
"pdpteTable (PageDirectoryPDPTE v0 v1 v2 v3 v4 v5) = v0"
|
||||
|
||||
primrec
|
||||
pdpteCacheDisabled :: "pdpte \<Rightarrow> bool"
|
||||
where
|
||||
"pdpteCacheDisabled (HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v5"
|
||||
| "pdpteCacheDisabled (PageDirectoryPDPTE v0 v1 v2 v3 v4 v5) = v2"
|
||||
|
||||
primrec
|
||||
pdpteFrame :: "pdpte \<Rightarrow> paddr"
|
||||
where
|
||||
"pdpteFrame (HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v0"
|
||||
|
||||
primrec
|
||||
pdpteRights :: "pdpte \<Rightarrow> vmrights"
|
||||
where
|
||||
"pdpteRights (HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v8"
|
||||
| "pdpteRights (PageDirectoryPDPTE v0 v1 v2 v3 v4 v5) = v5"
|
||||
|
||||
primrec
|
||||
pdptePAT :: "pdpte \<Rightarrow> bool"
|
||||
where
|
||||
"pdptePAT (HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v2"
|
||||
|
||||
primrec
|
||||
pdpteDirty :: "pdpte \<Rightarrow> bool"
|
||||
where
|
||||
"pdpteDirty (HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v3"
|
||||
|
||||
primrec
|
||||
pdpteAccessed_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pdpte \<Rightarrow> pdpte"
|
||||
where
|
||||
"pdpteAccessed_update f (HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = HugePagePDPTE v0 v1 v2 v3 (f v4) v5 v6 v7 v8"
|
||||
| "pdpteAccessed_update f (PageDirectoryPDPTE v0 v1 v2 v3 v4 v5) = PageDirectoryPDPTE v0 (f v1) v2 v3 v4 v5"
|
||||
|
||||
primrec
|
||||
pdpteGlobal_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pdpte \<Rightarrow> pdpte"
|
||||
where
|
||||
"pdpteGlobal_update f (HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = HugePagePDPTE v0 (f v1) v2 v3 v4 v5 v6 v7 v8"
|
||||
|
||||
primrec
|
||||
pdpteWriteThrough_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pdpte \<Rightarrow> pdpte"
|
||||
where
|
||||
"pdpteWriteThrough_update f (HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = HugePagePDPTE v0 v1 v2 v3 v4 v5 (f v6) v7 v8"
|
||||
| "pdpteWriteThrough_update f (PageDirectoryPDPTE v0 v1 v2 v3 v4 v5) = PageDirectoryPDPTE v0 v1 v2 (f v3) v4 v5"
|
||||
|
||||
primrec
|
||||
pdpteExecuteDisable_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pdpte \<Rightarrow> pdpte"
|
||||
where
|
||||
"pdpteExecuteDisable_update f (HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 (f v7) v8"
|
||||
| "pdpteExecuteDisable_update f (PageDirectoryPDPTE v0 v1 v2 v3 v4 v5) = PageDirectoryPDPTE v0 v1 v2 v3 (f v4) v5"
|
||||
|
||||
primrec
|
||||
pdpteTable_update :: "(paddr \<Rightarrow> paddr) \<Rightarrow> pdpte \<Rightarrow> pdpte"
|
||||
where
|
||||
"pdpteTable_update f (PageDirectoryPDPTE v0 v1 v2 v3 v4 v5) = PageDirectoryPDPTE (f v0) v1 v2 v3 v4 v5"
|
||||
|
||||
primrec
|
||||
pdpteCacheDisabled_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pdpte \<Rightarrow> pdpte"
|
||||
where
|
||||
"pdpteCacheDisabled_update f (HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = HugePagePDPTE v0 v1 v2 v3 v4 (f v5) v6 v7 v8"
|
||||
| "pdpteCacheDisabled_update f (PageDirectoryPDPTE v0 v1 v2 v3 v4 v5) = PageDirectoryPDPTE v0 v1 (f v2) v3 v4 v5"
|
||||
|
||||
primrec
|
||||
pdpteFrame_update :: "(paddr \<Rightarrow> paddr) \<Rightarrow> pdpte \<Rightarrow> pdpte"
|
||||
where
|
||||
"pdpteFrame_update f (HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = HugePagePDPTE (f v0) v1 v2 v3 v4 v5 v6 v7 v8"
|
||||
|
||||
primrec
|
||||
pdpteRights_update :: "(vmrights \<Rightarrow> vmrights) \<Rightarrow> pdpte \<Rightarrow> pdpte"
|
||||
where
|
||||
"pdpteRights_update f (HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 (f v8)"
|
||||
| "pdpteRights_update f (PageDirectoryPDPTE v0 v1 v2 v3 v4 v5) = PageDirectoryPDPTE v0 v1 v2 v3 v4 (f v5)"
|
||||
|
||||
primrec
|
||||
pdptePAT_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pdpte \<Rightarrow> pdpte"
|
||||
where
|
||||
"pdptePAT_update f (HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = HugePagePDPTE v0 v1 (f v2) v3 v4 v5 v6 v7 v8"
|
||||
|
||||
primrec
|
||||
pdpteDirty_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pdpte \<Rightarrow> pdpte"
|
||||
where
|
||||
"pdpteDirty_update f (HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = HugePagePDPTE v0 v1 v2 (f v3) v4 v5 v6 v7 v8"
|
||||
|
||||
abbreviation (input)
|
||||
PageDirectoryPDPTE_trans :: "(paddr) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (vmrights) \<Rightarrow> pdpte" ("PageDirectoryPDPTE'_ \<lparr> pdpteTable= _, pdpteAccessed= _, pdpteCacheDisabled= _, pdpteWriteThrough= _, pdpteExecuteDisable= _, pdpteRights= _ \<rparr>")
|
||||
where
|
||||
"PageDirectoryPDPTE_ \<lparr> pdpteTable= v0, pdpteAccessed= v1, pdpteCacheDisabled= v2, pdpteWriteThrough= v3, pdpteExecuteDisable= v4, pdpteRights= v5 \<rparr> == PageDirectoryPDPTE v0 v1 v2 v3 v4 v5"
|
||||
|
||||
abbreviation (input)
|
||||
HugePagePDPTE_trans :: "(paddr) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (vmrights) \<Rightarrow> pdpte" ("HugePagePDPTE'_ \<lparr> pdpteFrame= _, pdpteGlobal= _, pdptePAT= _, pdpteDirty= _, pdpteAccessed= _, pdpteCacheDisabled= _, pdpteWriteThrough= _, pdpteExecuteDisable= _, pdpteRights= _ \<rparr>")
|
||||
where
|
||||
"HugePagePDPTE_ \<lparr> pdpteFrame= v0, pdpteGlobal= v1, pdptePAT= v2, pdpteDirty= v3, pdpteAccessed= v4, pdpteCacheDisabled= v5, pdpteWriteThrough= v6, pdpteExecuteDisable= v7, pdpteRights= v8 \<rparr> == HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8"
|
||||
|
||||
definition
|
||||
isInvalidPDPTE :: "pdpte \<Rightarrow> bool"
|
||||
where
|
||||
"isInvalidPDPTE v \<equiv> case v of
|
||||
InvalidPDPTE \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isPageDirectoryPDPTE :: "pdpte \<Rightarrow> bool"
|
||||
where
|
||||
"isPageDirectoryPDPTE v \<equiv> case v of
|
||||
PageDirectoryPDPTE v0 v1 v2 v3 v4 v5 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isHugePagePDPTE :: "pdpte \<Rightarrow> bool"
|
||||
where
|
||||
"isHugePagePDPTE v \<equiv> case v of
|
||||
HugePagePDPTE v0 v1 v2 v3 v4 v5 v6 v7 v8 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
datatype pde =
|
||||
InvalidPDE
|
||||
| PageTablePDE paddr bool bool bool bool vmrights
|
||||
| LargePagePDE paddr bool bool bool bool bool bool bool vmrights
|
||||
|
||||
primrec
|
||||
pdePAT :: "pde \<Rightarrow> bool"
|
||||
where
|
||||
"pdePAT (LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v2"
|
||||
|
||||
primrec
|
||||
pdeExecuteDisable :: "pde \<Rightarrow> bool"
|
||||
where
|
||||
"pdeExecuteDisable (PageTablePDE v0 v1 v2 v3 v4 v5) = v4"
|
||||
| "pdeExecuteDisable (LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v7"
|
||||
|
||||
primrec
|
||||
pdeRights :: "pde \<Rightarrow> vmrights"
|
||||
where
|
||||
"pdeRights (PageTablePDE v0 v1 v2 v3 v4 v5) = v5"
|
||||
| "pdeRights (LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v8"
|
||||
|
||||
primrec
|
||||
pdeTable :: "pde \<Rightarrow> paddr"
|
||||
where
|
||||
"pdeTable (PageTablePDE v0 v1 v2 v3 v4 v5) = v0"
|
||||
|
||||
primrec
|
||||
pdeFrame :: "pde \<Rightarrow> paddr"
|
||||
where
|
||||
"pdeFrame (LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v0"
|
||||
|
||||
primrec
|
||||
pdeAccessed :: "pde \<Rightarrow> bool"
|
||||
where
|
||||
"pdeAccessed (PageTablePDE v0 v1 v2 v3 v4 v5) = v1"
|
||||
| "pdeAccessed (LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v4"
|
||||
|
||||
primrec
|
||||
pdeCacheDisabled :: "pde \<Rightarrow> bool"
|
||||
where
|
||||
"pdeCacheDisabled (PageTablePDE v0 v1 v2 v3 v4 v5) = v2"
|
||||
| "pdeCacheDisabled (LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v5"
|
||||
|
||||
primrec
|
||||
pdeGlobal :: "pde \<Rightarrow> bool"
|
||||
where
|
||||
"pdeGlobal (LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v1"
|
||||
|
||||
primrec
|
||||
pdeWriteThrough :: "pde \<Rightarrow> bool"
|
||||
where
|
||||
"pdeWriteThrough (PageTablePDE v0 v1 v2 v3 v4 v5) = v3"
|
||||
| "pdeWriteThrough (LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v6"
|
||||
|
||||
primrec
|
||||
pdeDirty :: "pde \<Rightarrow> bool"
|
||||
where
|
||||
"pdeDirty (LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v3"
|
||||
|
||||
primrec
|
||||
pdePAT_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pde \<Rightarrow> pde"
|
||||
where
|
||||
"pdePAT_update f (LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8) = LargePagePDE v0 v1 (f v2) v3 v4 v5 v6 v7 v8"
|
||||
|
||||
primrec
|
||||
pdeExecuteDisable_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pde \<Rightarrow> pde"
|
||||
where
|
||||
"pdeExecuteDisable_update f (PageTablePDE v0 v1 v2 v3 v4 v5) = PageTablePDE v0 v1 v2 v3 (f v4) v5"
|
||||
| "pdeExecuteDisable_update f (LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8) = LargePagePDE v0 v1 v2 v3 v4 v5 v6 (f v7) v8"
|
||||
|
||||
primrec
|
||||
pdeRights_update :: "(vmrights \<Rightarrow> vmrights) \<Rightarrow> pde \<Rightarrow> pde"
|
||||
where
|
||||
"pdeRights_update f (PageTablePDE v0 v1 v2 v3 v4 v5) = PageTablePDE v0 v1 v2 v3 v4 (f v5)"
|
||||
| "pdeRights_update f (LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8) = LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 (f v8)"
|
||||
|
||||
primrec
|
||||
pdeTable_update :: "(paddr \<Rightarrow> paddr) \<Rightarrow> pde \<Rightarrow> pde"
|
||||
where
|
||||
"pdeTable_update f (PageTablePDE v0 v1 v2 v3 v4 v5) = PageTablePDE (f v0) v1 v2 v3 v4 v5"
|
||||
|
||||
primrec
|
||||
pdeFrame_update :: "(paddr \<Rightarrow> paddr) \<Rightarrow> pde \<Rightarrow> pde"
|
||||
where
|
||||
"pdeFrame_update f (LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8) = LargePagePDE (f v0) v1 v2 v3 v4 v5 v6 v7 v8"
|
||||
|
||||
primrec
|
||||
pdeAccessed_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pde \<Rightarrow> pde"
|
||||
where
|
||||
"pdeAccessed_update f (PageTablePDE v0 v1 v2 v3 v4 v5) = PageTablePDE v0 (f v1) v2 v3 v4 v5"
|
||||
| "pdeAccessed_update f (LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8) = LargePagePDE v0 v1 v2 v3 (f v4) v5 v6 v7 v8"
|
||||
|
||||
primrec
|
||||
pdeCacheDisabled_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pde \<Rightarrow> pde"
|
||||
where
|
||||
"pdeCacheDisabled_update f (PageTablePDE v0 v1 v2 v3 v4 v5) = PageTablePDE v0 v1 (f v2) v3 v4 v5"
|
||||
| "pdeCacheDisabled_update f (LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8) = LargePagePDE v0 v1 v2 v3 v4 (f v5) v6 v7 v8"
|
||||
|
||||
primrec
|
||||
pdeGlobal_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pde \<Rightarrow> pde"
|
||||
where
|
||||
"pdeGlobal_update f (LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8) = LargePagePDE v0 (f v1) v2 v3 v4 v5 v6 v7 v8"
|
||||
|
||||
primrec
|
||||
pdeWriteThrough_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pde \<Rightarrow> pde"
|
||||
where
|
||||
"pdeWriteThrough_update f (PageTablePDE v0 v1 v2 v3 v4 v5) = PageTablePDE v0 v1 v2 (f v3) v4 v5"
|
||||
| "pdeWriteThrough_update f (LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8) = LargePagePDE v0 v1 v2 v3 v4 v5 (f v6) v7 v8"
|
||||
|
||||
primrec
|
||||
pdeDirty_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pde \<Rightarrow> pde"
|
||||
where
|
||||
"pdeDirty_update f (LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8) = LargePagePDE v0 v1 v2 (f v3) v4 v5 v6 v7 v8"
|
||||
|
||||
abbreviation (input)
|
||||
PageTablePDE_trans :: "(paddr) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (vmrights) \<Rightarrow> pde" ("PageTablePDE'_ \<lparr> pdeTable= _, pdeAccessed= _, pdeCacheDisabled= _, pdeWriteThrough= _, pdeExecuteDisable= _, pdeRights= _ \<rparr>")
|
||||
where
|
||||
"PageTablePDE_ \<lparr> pdeTable= v0, pdeAccessed= v1, pdeCacheDisabled= v2, pdeWriteThrough= v3, pdeExecuteDisable= v4, pdeRights= v5 \<rparr> == PageTablePDE v0 v1 v2 v3 v4 v5"
|
||||
|
||||
abbreviation (input)
|
||||
LargePagePDE_trans :: "(paddr) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (vmrights) \<Rightarrow> pde" ("LargePagePDE'_ \<lparr> pdeFrame= _, pdeGlobal= _, pdePAT= _, pdeDirty= _, pdeAccessed= _, pdeCacheDisabled= _, pdeWriteThrough= _, pdeExecuteDisable= _, pdeRights= _ \<rparr>")
|
||||
where
|
||||
"LargePagePDE_ \<lparr> pdeFrame= v0, pdeGlobal= v1, pdePAT= v2, pdeDirty= v3, pdeAccessed= v4, pdeCacheDisabled= v5, pdeWriteThrough= v6, pdeExecuteDisable= v7, pdeRights= v8 \<rparr> == LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8"
|
||||
|
||||
definition
|
||||
isInvalidPDE :: "pde \<Rightarrow> bool"
|
||||
where
|
||||
"isInvalidPDE v \<equiv> case v of
|
||||
InvalidPDE \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isPageTablePDE :: "pde \<Rightarrow> bool"
|
||||
where
|
||||
"isPageTablePDE v \<equiv> case v of
|
||||
PageTablePDE v0 v1 v2 v3 v4 v5 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isLargePagePDE :: "pde \<Rightarrow> bool"
|
||||
where
|
||||
"isLargePagePDE v \<equiv> case v of
|
||||
LargePagePDE v0 v1 v2 v3 v4 v5 v6 v7 v8 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
datatype pte =
|
||||
InvalidPTE
|
||||
| SmallPagePTE paddr bool bool bool bool bool bool bool vmrights
|
||||
|
||||
primrec
|
||||
pteAccessed :: "pte \<Rightarrow> bool"
|
||||
where
|
||||
"pteAccessed (SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v4"
|
||||
|
||||
primrec
|
||||
pteCacheDisabled :: "pte \<Rightarrow> bool"
|
||||
where
|
||||
"pteCacheDisabled (SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v5"
|
||||
|
||||
primrec
|
||||
pteGlobal :: "pte \<Rightarrow> bool"
|
||||
where
|
||||
"pteGlobal (SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v1"
|
||||
|
||||
primrec
|
||||
pteWriteThrough :: "pte \<Rightarrow> bool"
|
||||
where
|
||||
"pteWriteThrough (SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v6"
|
||||
|
||||
primrec
|
||||
pteDirty :: "pte \<Rightarrow> bool"
|
||||
where
|
||||
"pteDirty (SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v3"
|
||||
|
||||
primrec
|
||||
ptePAT :: "pte \<Rightarrow> bool"
|
||||
where
|
||||
"ptePAT (SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v2"
|
||||
|
||||
primrec
|
||||
pteExecuteDisable :: "pte \<Rightarrow> bool"
|
||||
where
|
||||
"pteExecuteDisable (SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v7"
|
||||
|
||||
primrec
|
||||
pteRights :: "pte \<Rightarrow> vmrights"
|
||||
where
|
||||
"pteRights (SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v8"
|
||||
|
||||
primrec
|
||||
pteFrame :: "pte \<Rightarrow> paddr"
|
||||
where
|
||||
"pteFrame (SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = v0"
|
||||
|
||||
primrec
|
||||
pteAccessed_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pte \<Rightarrow> pte"
|
||||
where
|
||||
"pteAccessed_update f (SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = SmallPagePTE v0 v1 v2 v3 (f v4) v5 v6 v7 v8"
|
||||
|
||||
primrec
|
||||
pteCacheDisabled_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pte \<Rightarrow> pte"
|
||||
where
|
||||
"pteCacheDisabled_update f (SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = SmallPagePTE v0 v1 v2 v3 v4 (f v5) v6 v7 v8"
|
||||
|
||||
primrec
|
||||
pteGlobal_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pte \<Rightarrow> pte"
|
||||
where
|
||||
"pteGlobal_update f (SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = SmallPagePTE v0 (f v1) v2 v3 v4 v5 v6 v7 v8"
|
||||
|
||||
primrec
|
||||
pteWriteThrough_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pte \<Rightarrow> pte"
|
||||
where
|
||||
"pteWriteThrough_update f (SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = SmallPagePTE v0 v1 v2 v3 v4 v5 (f v6) v7 v8"
|
||||
|
||||
primrec
|
||||
pteDirty_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pte \<Rightarrow> pte"
|
||||
where
|
||||
"pteDirty_update f (SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = SmallPagePTE v0 v1 v2 (f v3) v4 v5 v6 v7 v8"
|
||||
|
||||
primrec
|
||||
ptePAT_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pte \<Rightarrow> pte"
|
||||
where
|
||||
"ptePAT_update f (SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = SmallPagePTE v0 v1 (f v2) v3 v4 v5 v6 v7 v8"
|
||||
|
||||
primrec
|
||||
pteExecuteDisable_update :: "(bool \<Rightarrow> bool) \<Rightarrow> pte \<Rightarrow> pte"
|
||||
where
|
||||
"pteExecuteDisable_update f (SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = SmallPagePTE v0 v1 v2 v3 v4 v5 v6 (f v7) v8"
|
||||
|
||||
primrec
|
||||
pteRights_update :: "(vmrights \<Rightarrow> vmrights) \<Rightarrow> pte \<Rightarrow> pte"
|
||||
where
|
||||
"pteRights_update f (SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 (f v8)"
|
||||
|
||||
primrec
|
||||
pteFrame_update :: "(paddr \<Rightarrow> paddr) \<Rightarrow> pte \<Rightarrow> pte"
|
||||
where
|
||||
"pteFrame_update f (SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8) = SmallPagePTE (f v0) v1 v2 v3 v4 v5 v6 v7 v8"
|
||||
|
||||
abbreviation (input)
|
||||
SmallPagePTE_trans :: "(paddr) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> (vmrights) \<Rightarrow> pte" ("SmallPagePTE'_ \<lparr> pteFrame= _, pteGlobal= _, ptePAT= _, pteDirty= _, pteAccessed= _, pteCacheDisabled= _, pteWriteThrough= _, pteExecuteDisable= _, pteRights= _ \<rparr>")
|
||||
where
|
||||
"SmallPagePTE_ \<lparr> pteFrame= v0, pteGlobal= v1, ptePAT= v2, pteDirty= v3, pteAccessed= v4, pteCacheDisabled= v5, pteWriteThrough= v6, pteExecuteDisable= v7, pteRights= v8 \<rparr> == SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8"
|
||||
|
||||
definition
|
||||
isInvalidPTE :: "pte \<Rightarrow> bool"
|
||||
where
|
||||
"isInvalidPTE v \<equiv> case v of
|
||||
InvalidPTE \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
definition
|
||||
isSmallPagePTE :: "pte \<Rightarrow> bool"
|
||||
where
|
||||
"isSmallPagePTE v \<equiv> case v of
|
||||
SmallPagePTE v0 v1 v2 v3 v4 v5 v6 v7 v8 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
datatype vmpage_entry =
|
||||
VMPTE pte
|
||||
| VMPDE pde
|
||||
| VMPDPTE pdpte
|
||||
|
||||
datatype vmpage_entry_ptr =
|
||||
VMPTEPtr machine_word
|
||||
| VMPDEPtr machine_word
|
||||
| VMPDPTEPtr machine_word
|
||||
|
||||
datatype vmattributes =
|
||||
VMAttributes bool bool bool
|
||||
|
||||
primrec
|
||||
x64CacheDisabled :: "vmattributes \<Rightarrow> bool"
|
||||
where
|
||||
"x64CacheDisabled (VMAttributes v0 v1 v2) = v2"
|
||||
|
||||
primrec
|
||||
x64WriteThrough :: "vmattributes \<Rightarrow> bool"
|
||||
where
|
||||
"x64WriteThrough (VMAttributes v0 v1 v2) = v0"
|
||||
|
||||
primrec
|
||||
x64PAT :: "vmattributes \<Rightarrow> bool"
|
||||
where
|
||||
"x64PAT (VMAttributes v0 v1 v2) = v1"
|
||||
|
||||
primrec
|
||||
x64CacheDisabled_update :: "(bool \<Rightarrow> bool) \<Rightarrow> vmattributes \<Rightarrow> vmattributes"
|
||||
where
|
||||
"x64CacheDisabled_update f (VMAttributes v0 v1 v2) = VMAttributes v0 v1 (f v2)"
|
||||
|
||||
primrec
|
||||
x64WriteThrough_update :: "(bool \<Rightarrow> bool) \<Rightarrow> vmattributes \<Rightarrow> vmattributes"
|
||||
where
|
||||
"x64WriteThrough_update f (VMAttributes v0 v1 v2) = VMAttributes (f v0) v1 v2"
|
||||
|
||||
primrec
|
||||
x64PAT_update :: "(bool \<Rightarrow> bool) \<Rightarrow> vmattributes \<Rightarrow> vmattributes"
|
||||
where
|
||||
"x64PAT_update f (VMAttributes v0 v1 v2) = VMAttributes v0 (f v1) v2"
|
||||
|
||||
abbreviation (input)
|
||||
VMAttributes_trans :: "(bool) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> vmattributes" ("VMAttributes'_ \<lparr> x64WriteThrough= _, x64PAT= _, x64CacheDisabled= _ \<rparr>")
|
||||
where
|
||||
"VMAttributes_ \<lparr> x64WriteThrough= v0, x64PAT= v1, x64CacheDisabled= v2 \<rparr> == VMAttributes v0 v1 v2"
|
||||
|
||||
lemma x64CacheDisabled_x64CacheDisabled_update [simp]:
|
||||
"x64CacheDisabled (x64CacheDisabled_update f v) = f (x64CacheDisabled v)"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64CacheDisabled_x64WriteThrough_update [simp]:
|
||||
"x64CacheDisabled (x64WriteThrough_update f v) = x64CacheDisabled v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64CacheDisabled_x64PAT_update [simp]:
|
||||
"x64CacheDisabled (x64PAT_update f v) = x64CacheDisabled v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64WriteThrough_x64CacheDisabled_update [simp]:
|
||||
"x64WriteThrough (x64CacheDisabled_update f v) = x64WriteThrough v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64WriteThrough_x64WriteThrough_update [simp]:
|
||||
"x64WriteThrough (x64WriteThrough_update f v) = f (x64WriteThrough v)"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64WriteThrough_x64PAT_update [simp]:
|
||||
"x64WriteThrough (x64PAT_update f v) = x64WriteThrough v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64PAT_x64CacheDisabled_update [simp]:
|
||||
"x64PAT (x64CacheDisabled_update f v) = x64PAT v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64PAT_x64WriteThrough_update [simp]:
|
||||
"x64PAT (x64WriteThrough_update f v) = x64PAT v"
|
||||
by (cases v) simp
|
||||
|
||||
lemma x64PAT_x64PAT_update [simp]:
|
||||
"x64PAT (x64PAT_update f v) = f (x64PAT v)"
|
||||
by (cases v) simp
|
||||
|
||||
definition
|
||||
addrFromKPPtr :: "machine_word \<Rightarrow> paddr"
|
||||
where
|
||||
"addrFromKPPtr \<equiv> Platform.X64.addrFromKPPtr"
|
||||
|
||||
definition
|
||||
fromPAddr :: "paddr \<Rightarrow> machine_word"
|
||||
where
|
||||
"fromPAddr \<equiv> Platform.X64.fromPAddr"
|
||||
|
||||
definition
|
||||
ptBits :: "nat"
|
||||
where
|
||||
"ptBits \<equiv> ptTranslationBits + 3"
|
||||
|
||||
definition
|
||||
ptShiftBits :: "nat"
|
||||
where
|
||||
"ptShiftBits \<equiv> pageBits"
|
||||
|
||||
definition
|
||||
pdBits :: "nat"
|
||||
where
|
||||
"pdBits \<equiv> ptTranslationBits + 3"
|
||||
|
||||
definition
|
||||
pdShiftBits :: "nat"
|
||||
where
|
||||
"pdShiftBits \<equiv> pageBits + ptTranslationBits"
|
||||
|
||||
definition
|
||||
pdptBits :: "nat"
|
||||
where
|
||||
"pdptBits \<equiv> ptTranslationBits + 3"
|
||||
|
||||
definition
|
||||
pdptShiftBits :: "nat"
|
||||
where
|
||||
"pdptShiftBits \<equiv> pageBits + ptTranslationBits + ptTranslationBits"
|
||||
|
||||
definition
|
||||
pml4Bits :: "nat"
|
||||
where
|
||||
"pml4Bits \<equiv> ptTranslationBits + 3"
|
||||
|
||||
definition
|
||||
pml4ShiftBits :: "nat"
|
||||
where
|
||||
"pml4ShiftBits \<equiv> pageBits + ptTranslationBits + ptTranslationBits + ptTranslationBits"
|
||||
|
||||
definition
|
||||
pageColourBits :: "nat"
|
||||
where
|
||||
"pageColourBits \<equiv> error []"
|
||||
|
||||
definition
|
||||
setInterruptMode :: "irq \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> unit machine_monad"
|
||||
where
|
||||
"setInterruptMode arg1 arg2 arg3 \<equiv> return ()"
|
||||
|
||||
definition
|
||||
getPTIndex :: "vptr \<Rightarrow> machine_word"
|
||||
where
|
||||
"getPTIndex vptr \<equiv> fromVPtr $ vptr `~shiftR~` ptShiftBits && mask ptTranslationBits"
|
||||
|
||||
definition
|
||||
getPDIndex :: "vptr \<Rightarrow> machine_word"
|
||||
where
|
||||
"getPDIndex vptr \<equiv> fromVPtr $ vptr `~shiftR~` pdShiftBits && mask ptTranslationBits"
|
||||
|
||||
definition
|
||||
getPDPTIndex :: "vptr \<Rightarrow> machine_word"
|
||||
where
|
||||
"getPDPTIndex vptr \<equiv> fromVPtr $ vptr `~shiftR~` pdptShiftBits && mask ptTranslationBits"
|
||||
|
||||
definition
|
||||
getPML4Index :: "vptr \<Rightarrow> machine_word"
|
||||
where
|
||||
"getPML4Index vptr \<equiv> fromVPtr $ vptr `~shiftR~` pml4ShiftBits && mask ptTranslationBits"
|
||||
|
||||
definition
|
||||
vmRightsToBits :: "vmrights \<Rightarrow> machine_word"
|
||||
where
|
||||
"vmRightsToBits x0\<equiv> (case x0 of
|
||||
VMKernelOnly \<Rightarrow> 0x01
|
||||
| VMReadOnly \<Rightarrow> 0x10
|
||||
| VMReadWrite \<Rightarrow> 0x11
|
||||
)"
|
||||
|
||||
definition
|
||||
allowWrite :: "vmrights \<Rightarrow> bool"
|
||||
where
|
||||
"allowWrite x0\<equiv> (case x0 of
|
||||
VMKernelOnly \<Rightarrow> False
|
||||
| VMReadOnly \<Rightarrow> False
|
||||
| VMReadWrite \<Rightarrow> True
|
||||
)"
|
||||
|
||||
definition
|
||||
allowRead :: "vmrights \<Rightarrow> bool"
|
||||
where
|
||||
"allowRead x0\<equiv> (case x0 of
|
||||
VMKernelOnly \<Rightarrow> False
|
||||
| VMReadOnly \<Rightarrow> True
|
||||
| VMReadWrite \<Rightarrow> True
|
||||
)"
|
||||
|
||||
definition
|
||||
getVMRights :: "bool \<Rightarrow> bool \<Rightarrow> vmrights"
|
||||
where
|
||||
"getVMRights x0 x1\<equiv> (case (x0, x1) of
|
||||
(True, True) \<Rightarrow> VMReadWrite
|
||||
| (True, False) \<Rightarrow> VMReadOnly
|
||||
| (_, _) \<Rightarrow> VMKernelOnly
|
||||
)"
|
||||
|
||||
definition
|
||||
vmRightsFromBits :: "machine_word \<Rightarrow> vmrights"
|
||||
where
|
||||
"vmRightsFromBits rw\<equiv> getVMRights (testBit rw 1) (testBit rw 0)"
|
||||
|
||||
definition
|
||||
pptrBase :: "vptr"
|
||||
where
|
||||
"pptrBase \<equiv> Platform.X64.pptrBase"
|
||||
|
||||
definition
|
||||
initIRQController :: "unit machine_monad"
|
||||
where
|
||||
"initIRQController \<equiv> error []"
|
||||
|
||||
|
||||
end
|
||||
|
||||
context begin interpretation Arch .
|
||||
requalify_types vmrights
|
||||
end
|
||||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
|
||||
definition
|
||||
wordFromPML4E :: "pml4e \<Rightarrow> machine_word"
|
||||
where
|
||||
"wordFromPML4E x0\<equiv> (case x0 of
|
||||
InvalidPML4E \<Rightarrow> 0
|
||||
| (PDPointerTablePML4E table accessed cd wt xd rights) \<Rightarrow> 1 ||
|
||||
(if xd then (1 << 63) else 0) ||
|
||||
(fromIntegral table && 0x7fffffffff000) ||
|
||||
(if accessed then (1 << 5) else 0) ||
|
||||
(if cd then (1 << 4) else 0) ||
|
||||
(if wt then (1 << 3) else 0) ||
|
||||
(fromIntegral $ vmRightsToBits rights `~shiftL~` 1)
|
||||
)"
|
||||
|
||||
definition
|
||||
wordFromPDPTE :: "pdpte \<Rightarrow> machine_word"
|
||||
where
|
||||
"wordFromPDPTE x0\<equiv> (case x0 of
|
||||
InvalidPDPTE \<Rightarrow> 0
|
||||
| (PageDirectoryPDPTE table accessed cd wt xd rights) \<Rightarrow> 1 ||
|
||||
(if xd then (1 << 63) else 0) ||
|
||||
(fromIntegral table && 0x7fffffffff000) ||
|
||||
(if accessed then (1 << 5) else 0) ||
|
||||
(if cd then (1 << 4) else 0) ||
|
||||
(if wt then (1 << 3) else 0) ||
|
||||
(fromIntegral $ vmRightsToBits rights `~shiftL~` 1)
|
||||
| (HugePagePDPTE frame global pat dirty accessed cd wt xd rights) \<Rightarrow> 1 || (1 << 7) ||
|
||||
(if xd then (1 << 63) else 0) ||
|
||||
(fromIntegral frame && 0x7ffffc0000000) ||
|
||||
(if global then (1 << 8) else 0) ||
|
||||
(if pat then (1 << 12) else 0) ||
|
||||
(if dirty then (1 << 6) else 0) ||
|
||||
(if accessed then (1 << 5) else 0) ||
|
||||
(if cd then (1 << 4) else 0) ||
|
||||
(if wt then (1 << 3) else 0) ||
|
||||
(fromIntegral $ vmRightsToBits rights `~shiftL~` 1)
|
||||
)"
|
||||
|
||||
definition
|
||||
wordFromPDE :: "pde \<Rightarrow> machine_word"
|
||||
where
|
||||
"wordFromPDE x0\<equiv> (case x0 of
|
||||
InvalidPDE \<Rightarrow> 0
|
||||
| (PageTablePDE table accessed cd wt xd rights) \<Rightarrow> 1 ||
|
||||
(if xd then (1 << 63) else 0) ||
|
||||
(fromIntegral table && 0x7fffffffff000) ||
|
||||
(if accessed then (1 << 5) else 0) ||
|
||||
(if cd then (1 << 4) else 0) ||
|
||||
(if wt then (1 << 3) else 0) ||
|
||||
(fromIntegral $ vmRightsToBits rights `~shiftL~` 1)
|
||||
| (LargePagePDE frame global pat dirty accessed cd wt xd rights) \<Rightarrow> 1 || (1 << 7) ||
|
||||
(if xd then (1 << 63) else 0) ||
|
||||
(fromIntegral frame && 0x7ffffffe00000) ||
|
||||
(if global then (1 << 8) else 0) ||
|
||||
(if pat then (1 << 12) else 0) ||
|
||||
(if dirty then (1 << 6) else 0) ||
|
||||
(if accessed then (1 << 5) else 0) ||
|
||||
(if cd then (1 << 4) else 0) ||
|
||||
(if wt then (1 << 3) else 0) ||
|
||||
(fromIntegral $ vmRightsToBits rights `~shiftL~` 1)
|
||||
)"
|
||||
|
||||
definition
|
||||
wordFromPTE :: "pte \<Rightarrow> machine_word"
|
||||
where
|
||||
"wordFromPTE x0\<equiv> (case x0 of
|
||||
InvalidPTE \<Rightarrow> 0
|
||||
| (SmallPagePTE frame global pat dirty accessed cd wt xd rights) \<Rightarrow> 1 ||
|
||||
(if xd then (1 << 63) else 0) ||
|
||||
(fromIntegral frame && 0x7fffffffffe000) ||
|
||||
(if global then (1 << 8) else 0) ||
|
||||
(if pat then (1 << 7) else 0) ||
|
||||
(if dirty then (1 << 6) else 0) ||
|
||||
(if accessed then (1 << 5) else 0) ||
|
||||
(if cd then (1 << 4) else 0) ||
|
||||
(if wt then (1 << 3) else 0) ||
|
||||
(fromIntegral $ vmRightsToBits rights `~shiftL~` 1)
|
||||
)"
|
||||
|
||||
|
||||
end (* context X64 *)
|
||||
|
||||
end
|
||||
|
|
@ -1,28 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file RegisterSet_H.thy *)
|
||||
(*
|
||||
* 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 "Register Set"
|
||||
|
||||
theory RegisterSet_H
|
||||
imports
|
||||
"../../../lib/HaskellLib_H"
|
||||
"../../machine/X64/MachineTypes"
|
||||
begin
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
definition
|
||||
newContext :: "register => machine_word"
|
||||
where
|
||||
"newContext \<equiv> (K 0) aLU initContext"
|
||||
|
||||
end
|
||||
end
|
||||
|
|
@ -1,122 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file State_H.thy *)
|
||||
(*
|
||||
* 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)
|
||||
*)
|
||||
|
||||
(*
|
||||
Machine and kernel state.
|
||||
*)
|
||||
|
||||
chapter "Machine State"
|
||||
|
||||
theory State_H
|
||||
imports
|
||||
"../../../lib/HaskellLib_H"
|
||||
RegisterSet_H
|
||||
"../../machine/X64/MachineOps"
|
||||
begin
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
definition
|
||||
Word :: "machine_word \<Rightarrow> machine_word"
|
||||
where
|
||||
Word_def[simp]:
|
||||
"Word \<equiv> id"
|
||||
|
||||
type_synonym register = "X64.register"
|
||||
|
||||
definition
|
||||
Register :: "register \<Rightarrow> register"
|
||||
where Register_def[simp]:
|
||||
"Register \<equiv> id"
|
||||
|
||||
type_synonym vptr = "machine_word"
|
||||
|
||||
definition
|
||||
VPtr :: "vptr \<Rightarrow> vptr"
|
||||
where VPtr_def[simp]:
|
||||
"VPtr \<equiv> id"
|
||||
|
||||
definition
|
||||
fromVPtr :: "vptr \<Rightarrow> vptr"
|
||||
where
|
||||
fromVPtr_def[simp]:
|
||||
"fromVPtr \<equiv> id"
|
||||
|
||||
definition fromVPtr_update :: "(vptr \<Rightarrow> vptr) \<Rightarrow> vptr \<Rightarrow> vptr"
|
||||
where
|
||||
fromVPtr_update_def[simp]:
|
||||
"fromVPtr_update f y \<equiv> f y"
|
||||
|
||||
abbreviation (input)
|
||||
VPtr_trans :: "(machine_word) \<Rightarrow> vptr" ("VPtr'_ \<lparr> fromVPtr= _ \<rparr>")
|
||||
where
|
||||
"VPtr_ \<lparr> fromVPtr= v0 \<rparr> == VPtr v0"
|
||||
|
||||
definition
|
||||
msgInfoRegister :: "register"
|
||||
where
|
||||
"msgInfoRegister \<equiv> Register X64.msgInfoRegister"
|
||||
|
||||
definition
|
||||
msgRegisters :: "register list"
|
||||
where
|
||||
"msgRegisters \<equiv> map Register X64.msgRegisters"
|
||||
|
||||
definition
|
||||
capRegister :: "register"
|
||||
where
|
||||
"capRegister \<equiv> Register X64.capRegister"
|
||||
|
||||
definition
|
||||
badgeRegister :: "register"
|
||||
where
|
||||
"badgeRegister \<equiv> Register X64.badgeRegister"
|
||||
|
||||
definition
|
||||
frameRegisters :: "register list"
|
||||
where
|
||||
"frameRegisters \<equiv> map Register X64.frameRegisters"
|
||||
|
||||
definition
|
||||
gpRegisters :: "register list"
|
||||
where
|
||||
"gpRegisters \<equiv> map Register X64.gpRegisters"
|
||||
|
||||
definition
|
||||
exceptionMessage :: "register list"
|
||||
where
|
||||
"exceptionMessage \<equiv> map Register X64.exceptionMessage"
|
||||
|
||||
definition
|
||||
syscallMessage :: "register list"
|
||||
where
|
||||
"syscallMessage \<equiv> map Register X64.syscallMessage"
|
||||
|
||||
|
||||
definition
|
||||
PPtr :: "machine_word \<Rightarrow> machine_word"
|
||||
where
|
||||
PPtr_def[simp]:
|
||||
"PPtr \<equiv> id"
|
||||
|
||||
definition
|
||||
fromPPtr :: "machine_word \<Rightarrow> machine_word"
|
||||
where
|
||||
fromPPtr_def[simp]:
|
||||
"fromPPtr \<equiv> id"
|
||||
|
||||
definition
|
||||
nullPointer :: machine_word
|
||||
where
|
||||
"nullPointer \<equiv> 0"
|
||||
|
||||
end
|
||||
end
|
||||
|
|
@ -39,7 +39,7 @@ private abbreviation (input)
|
|||
defs Arch_createNewCaps_def:
|
||||
"Arch_createNewCaps t regionBase numObjects userSize dev \<equiv>
|
||||
let pointerCast = PPtr \<circ> fromPPtr
|
||||
in (case t of
|
||||
in (case t of
|
||||
APIObjectType apiObject \<Rightarrow> haskell_fail []
|
||||
| SmallPageObject \<Rightarrow>
|
||||
createNewPageCaps regionBase numObjects dev 0 X64SmallPage
|
||||
|
|
@ -1,511 +0,0 @@
|
|||
(* THIS FILE WAS AUTOMATICALLY GENERATED. DO NOT EDIT. *)
|
||||
(* instead, see the skeleton file MachineTypes.thy *)
|
||||
(*
|
||||
* 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 "x86-64bit Machine Types"
|
||||
|
||||
theory MachineTypes
|
||||
imports
|
||||
"../../../lib/Word_Lib/Enumeration"
|
||||
"../../../lib/$L4V_ARCH/WordSetup"
|
||||
"../../../lib/Monad_WP/NonDetMonad"
|
||||
"../../../lib/HaskellLib_H"
|
||||
Platform
|
||||
begin
|
||||
|
||||
context Arch begin global_naming X64
|
||||
|
||||
text {*
|
||||
An implementation of the machine's types, defining register set
|
||||
and some observable machine state.
|
||||
*}
|
||||
|
||||
section "Types"
|
||||
|
||||
datatype register =
|
||||
RAX
|
||||
| RBX
|
||||
| RCX
|
||||
| RDX
|
||||
| RSI
|
||||
| RDI
|
||||
| RBP
|
||||
| R8
|
||||
| R9
|
||||
| R10
|
||||
| R11
|
||||
| R12
|
||||
| R13
|
||||
| R14
|
||||
| R15
|
||||
| DS
|
||||
| ES
|
||||
| FS
|
||||
| GS
|
||||
| FaultIP
|
||||
| TLS_BASE
|
||||
| PADDING_REGISTER
|
||||
| ErrorRegister
|
||||
| NextIP
|
||||
| CS
|
||||
| FLAGS
|
||||
| RSP
|
||||
| SS
|
||||
|
||||
type_synonym machine_word = "word64"
|
||||
|
||||
datatype gdtslot =
|
||||
GDT_NULL
|
||||
| GDT_CS_0
|
||||
| GDT_DS_0
|
||||
| GDT_TSS
|
||||
| GDT_TSS_Padding
|
||||
| GDT_CS_3
|
||||
| GDT_DS_3
|
||||
| GDT_TLS
|
||||
| GDT_IPCBUF
|
||||
| GDT_ENTRIES
|
||||
|
||||
consts'
|
||||
gdtToSel :: "gdtslot \<Rightarrow> machine_word"
|
||||
|
||||
consts'
|
||||
gdtToSel_masked :: "gdtslot \<Rightarrow> machine_word"
|
||||
|
||||
consts'
|
||||
initContext :: "(register * machine_word) list"
|
||||
|
||||
consts'
|
||||
sanitiseRegister :: "register \<Rightarrow> machine_word \<Rightarrow> machine_word"
|
||||
|
||||
(*<*)
|
||||
|
||||
section "Machine Words"
|
||||
|
||||
type_synonym machine_word_len = 64
|
||||
|
||||
definition
|
||||
word_size_bits :: "'a :: numeral"
|
||||
where
|
||||
"word_size_bits \<equiv> 3"
|
||||
|
||||
end
|
||||
|
||||
context begin interpretation Arch .
|
||||
requalify_types register gdtslot
|
||||
end
|
||||
|
||||
context Arch begin global_naming X64
|
||||
|
||||
end
|
||||
qualify X64 (in Arch)
|
||||
(* register instance proofs *)
|
||||
(*<*)
|
||||
instantiation register :: enum begin
|
||||
interpretation Arch .
|
||||
definition
|
||||
enum_register: "enum_class.enum \<equiv>
|
||||
[
|
||||
RAX,
|
||||
RBX,
|
||||
RCX,
|
||||
RDX,
|
||||
RSI,
|
||||
RDI,
|
||||
RBP,
|
||||
R8,
|
||||
R9,
|
||||
R10,
|
||||
R11,
|
||||
R12,
|
||||
R13,
|
||||
R14,
|
||||
R15,
|
||||
DS,
|
||||
ES,
|
||||
FS,
|
||||
GS,
|
||||
FaultIP,
|
||||
TLS_BASE,
|
||||
PADDING_REGISTER,
|
||||
ErrorRegister,
|
||||
NextIP,
|
||||
CS,
|
||||
FLAGS,
|
||||
RSP,
|
||||
SS
|
||||
]"
|
||||
|
||||
|
||||
definition
|
||||
"enum_class.enum_all (P :: register \<Rightarrow> bool) \<longleftrightarrow> Ball UNIV P"
|
||||
|
||||
definition
|
||||
"enum_class.enum_ex (P :: register \<Rightarrow> bool) \<longleftrightarrow> Bex UNIV P"
|
||||
|
||||
instance
|
||||
apply intro_classes
|
||||
apply (safe, simp)
|
||||
apply (case_tac x)
|
||||
apply (simp_all add: enum_register enum_all_register_def enum_ex_register_def)
|
||||
by fast+
|
||||
end
|
||||
|
||||
instantiation register :: enum_alt
|
||||
begin
|
||||
interpretation Arch .
|
||||
definition
|
||||
enum_alt_register: "enum_alt \<equiv>
|
||||
alt_from_ord (enum :: register list)"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation register :: enumeration_both
|
||||
begin
|
||||
interpretation Arch .
|
||||
instance by (intro_classes, simp add: enum_alt_register)
|
||||
end
|
||||
|
||||
(*>*)
|
||||
end_qualify
|
||||
context Arch begin global_naming X64
|
||||
|
||||
end
|
||||
qualify X64 (in Arch)
|
||||
(* gdtslot instance proofs *)
|
||||
(*<*)
|
||||
instantiation gdtslot :: enum begin
|
||||
interpretation Arch .
|
||||
definition
|
||||
enum_gdtslot: "enum_class.enum \<equiv>
|
||||
[
|
||||
GDT_NULL,
|
||||
GDT_CS_0,
|
||||
GDT_DS_0,
|
||||
GDT_TSS,
|
||||
GDT_TSS_Padding,
|
||||
GDT_CS_3,
|
||||
GDT_DS_3,
|
||||
GDT_TLS,
|
||||
GDT_IPCBUF,
|
||||
GDT_ENTRIES
|
||||
]"
|
||||
|
||||
|
||||
definition
|
||||
"enum_class.enum_all (P :: gdtslot \<Rightarrow> bool) \<longleftrightarrow> Ball UNIV P"
|
||||
|
||||
definition
|
||||
"enum_class.enum_ex (P :: gdtslot \<Rightarrow> bool) \<longleftrightarrow> Bex UNIV P"
|
||||
|
||||
instance
|
||||
apply intro_classes
|
||||
apply (safe, simp)
|
||||
apply (case_tac x)
|
||||
apply (simp_all add: enum_gdtslot enum_all_gdtslot_def enum_ex_gdtslot_def)
|
||||
by fast+
|
||||
end
|
||||
|
||||
instantiation gdtslot :: enum_alt
|
||||
begin
|
||||
interpretation Arch .
|
||||
definition
|
||||
enum_alt_gdtslot: "enum_alt \<equiv>
|
||||
alt_from_ord (enum :: gdtslot list)"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation gdtslot :: enumeration_both
|
||||
begin
|
||||
interpretation Arch .
|
||||
instance by (intro_classes, simp add: enum_alt_gdtslot)
|
||||
end
|
||||
|
||||
(*>*)
|
||||
end_qualify
|
||||
context Arch begin global_naming X64
|
||||
|
||||
(*>*)
|
||||
definition
|
||||
"capRegister \<equiv> RBX"
|
||||
|
||||
definition
|
||||
"msgInfoRegister \<equiv> RSI"
|
||||
|
||||
definition
|
||||
"msgRegisters \<equiv> [RDI, RBP]"
|
||||
|
||||
definition
|
||||
"badgeRegister \<equiv> capRegister"
|
||||
|
||||
definition
|
||||
"frameRegisters \<equiv> FaultIP # RSP # FLAGS # [RAX .e. R15]"
|
||||
|
||||
definition
|
||||
"gpRegisters \<equiv> [TLS_BASE, FS, GS]"
|
||||
|
||||
definition
|
||||
"exceptionMessage \<equiv> [FaultIP, RSP, FLAGS]"
|
||||
|
||||
definition
|
||||
"syscallMessage \<equiv> [RAX .e. RBP] @ [NextIP, RSP, FLAGS]"
|
||||
|
||||
defs gdtToSel_def:
|
||||
"gdtToSel g\<equiv> (fromIntegral (fromEnum g) `~shiftL~` 3 ) || 3"
|
||||
|
||||
defs gdtToSel_masked_def:
|
||||
"gdtToSel_masked g \<equiv> gdtToSel g || 3"
|
||||
|
||||
definition
|
||||
"selCS3 \<equiv> gdtToSel_masked GDT_CS_3"
|
||||
|
||||
definition
|
||||
"selDS3 \<equiv> gdtToSel_masked GDT_DS_3"
|
||||
|
||||
definition
|
||||
"selTLS \<equiv> gdtToSel_masked GDT_TLS"
|
||||
|
||||
definition
|
||||
"selIPCBUF \<equiv> gdtToSel_masked GDT_IPCBUF"
|
||||
|
||||
definition
|
||||
"selCS0 \<equiv> gdtToSel_masked GDT_CS_0"
|
||||
|
||||
definition
|
||||
"selDS0 \<equiv> gdtToSel GDT_DS_0"
|
||||
|
||||
defs initContext_def:
|
||||
"initContext\<equiv> [ (CS, selCS3)
|
||||
, (SS, selDS3)
|
||||
, (FLAGS, (1 << 9) || bit 1)
|
||||
]"
|
||||
|
||||
defs sanitiseRegister_def:
|
||||
"sanitiseRegister x0 v\<equiv> (case x0 of
|
||||
FLAGS \<Rightarrow>
|
||||
v || (1 << 1) && (complement (bit 3)) && (complement (bit 5)) || bit 9
|
||||
&& ((1 << 12) - 1)
|
||||
| FS \<Rightarrow> if v \<noteq> selTLS \<and> v \<noteq> selIPCBUF then 0 else v
|
||||
| GS \<Rightarrow> if v \<noteq> selTLS \<and> v \<noteq> selIPCBUF then 0 else v
|
||||
| _ \<Rightarrow> v
|
||||
)"
|
||||
|
||||
|
||||
section "Machine State"
|
||||
|
||||
text {*
|
||||
Most of the machine state is left underspecified at this level.
|
||||
We know it exists, we will declare some interface functions, but
|
||||
at this level we do not have access to how this state is transformed
|
||||
or what effect it has on the machine.
|
||||
*}
|
||||
typedecl machine_state_rest
|
||||
|
||||
end
|
||||
|
||||
qualify X64 (in Arch)
|
||||
|
||||
record
|
||||
machine_state =
|
||||
irq_masks :: "X64.irq \<Rightarrow> bool"
|
||||
irq_state :: nat
|
||||
underlying_memory :: "word64 \<Rightarrow> word8"
|
||||
device_state :: "word64 \<Rightarrow> word8 option"
|
||||
machine_state_rest :: X64.machine_state_rest
|
||||
|
||||
consts irq_oracle :: "nat \<Rightarrow> word8"
|
||||
|
||||
end_qualify
|
||||
|
||||
context Arch begin global_naming X64
|
||||
|
||||
text {*
|
||||
The machine monad is used for operations on the state defined above.
|
||||
*}
|
||||
type_synonym 'a machine_monad = "(machine_state, 'a) nondet_monad"
|
||||
|
||||
end
|
||||
|
||||
translations
|
||||
(type) "'c X64.machine_monad" <= (type) "(X64.machine_state, 'c) nondet_monad"
|
||||
|
||||
context Arch begin global_naming X64
|
||||
|
||||
text {*
|
||||
After kernel initialisation all IRQs are masked.
|
||||
*}
|
||||
definition
|
||||
"init_irq_masks \<equiv> \<lambda>_. True"
|
||||
|
||||
text {*
|
||||
The initial contents of the user-visible memory is 0.
|
||||
*}
|
||||
definition
|
||||
init_underlying_memory :: "word64 \<Rightarrow> word8"
|
||||
where
|
||||
"init_underlying_memory \<equiv> \<lambda>_. 0"
|
||||
|
||||
text {*
|
||||
We leave open the underspecified rest of the machine state in
|
||||
the initial state.
|
||||
*}
|
||||
definition
|
||||
init_machine_state :: machine_state where
|
||||
"init_machine_state \<equiv> \<lparr> irq_masks = init_irq_masks,
|
||||
irq_state = 0,
|
||||
underlying_memory = init_underlying_memory,
|
||||
device_state = empty,
|
||||
machine_state_rest = undefined \<rparr>"
|
||||
|
||||
datatype vmpage_size =
|
||||
X64SmallPage
|
||||
| X64LargePage
|
||||
| X64HugePage
|
||||
|
||||
datatype vmfault_type =
|
||||
X64DataFault
|
||||
| X64InstructionFault
|
||||
|
||||
datatype hyp_fault_type =
|
||||
X64NoHypFaults
|
||||
|
||||
datatype vmmap_type =
|
||||
VMNoMap
|
||||
| VMVSpaceMap
|
||||
| VMIOSpaceMap
|
||||
|
||||
definition
|
||||
pageBits :: "nat"
|
||||
where
|
||||
"pageBits \<equiv> 12"
|
||||
|
||||
definition
|
||||
ptTranslationBits :: "nat"
|
||||
where
|
||||
"ptTranslationBits \<equiv> 9"
|
||||
|
||||
definition
|
||||
pageBitsForSize :: "vmpage_size \<Rightarrow> nat"
|
||||
where
|
||||
"pageBitsForSize x0\<equiv> (case x0 of
|
||||
X64SmallPage \<Rightarrow> pageBits
|
||||
| X64LargePage \<Rightarrow> pageBits + ptTranslationBits
|
||||
| X64HugePage \<Rightarrow> pageBits + ptTranslationBits + ptTranslationBits
|
||||
)"
|
||||
|
||||
|
||||
end
|
||||
|
||||
context begin interpretation Arch .
|
||||
requalify_types vmpage_size vmmap_type
|
||||
end
|
||||
|
||||
context Arch begin global_naming X64
|
||||
|
||||
end
|
||||
qualify X64 (in Arch)
|
||||
(* vmpage_size instance proofs *)
|
||||
(*<*)
|
||||
instantiation vmpage_size :: enum begin
|
||||
interpretation Arch .
|
||||
definition
|
||||
enum_vmpage_size: "enum_class.enum \<equiv>
|
||||
[
|
||||
X64SmallPage,
|
||||
X64LargePage,
|
||||
X64HugePage
|
||||
]"
|
||||
|
||||
|
||||
definition
|
||||
"enum_class.enum_all (P :: vmpage_size \<Rightarrow> bool) \<longleftrightarrow> Ball UNIV P"
|
||||
|
||||
definition
|
||||
"enum_class.enum_ex (P :: vmpage_size \<Rightarrow> bool) \<longleftrightarrow> Bex UNIV P"
|
||||
|
||||
instance
|
||||
apply intro_classes
|
||||
apply (safe, simp)
|
||||
apply (case_tac x)
|
||||
apply (simp_all add: enum_vmpage_size enum_all_vmpage_size_def enum_ex_vmpage_size_def)
|
||||
by fast+
|
||||
end
|
||||
|
||||
instantiation vmpage_size :: enum_alt
|
||||
begin
|
||||
interpretation Arch .
|
||||
definition
|
||||
enum_alt_vmpage_size: "enum_alt \<equiv>
|
||||
alt_from_ord (enum :: vmpage_size list)"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation vmpage_size :: enumeration_both
|
||||
begin
|
||||
interpretation Arch .
|
||||
instance by (intro_classes, simp add: enum_alt_vmpage_size)
|
||||
end
|
||||
|
||||
(*>*)
|
||||
end_qualify
|
||||
context Arch begin global_naming X64
|
||||
|
||||
end
|
||||
qualify X64 (in Arch)
|
||||
(* vmmap_type instance proofs *)
|
||||
(*<*)
|
||||
instantiation vmmap_type :: enum begin
|
||||
interpretation Arch .
|
||||
definition
|
||||
enum_vmmap_type: "enum_class.enum \<equiv>
|
||||
[
|
||||
VMNoMap,
|
||||
VMVSpaceMap,
|
||||
VMIOSpaceMap
|
||||
]"
|
||||
|
||||
|
||||
definition
|
||||
"enum_class.enum_all (P :: vmmap_type \<Rightarrow> bool) \<longleftrightarrow> Ball UNIV P"
|
||||
|
||||
definition
|
||||
"enum_class.enum_ex (P :: vmmap_type \<Rightarrow> bool) \<longleftrightarrow> Bex UNIV P"
|
||||
|
||||
instance
|
||||
apply intro_classes
|
||||
apply (safe, simp)
|
||||
apply (case_tac x)
|
||||
apply (simp_all add: enum_vmmap_type enum_all_vmmap_type_def enum_ex_vmmap_type_def)
|
||||
by fast+
|
||||
end
|
||||
|
||||
instantiation vmmap_type :: enum_alt
|
||||
begin
|
||||
interpretation Arch .
|
||||
definition
|
||||
enum_alt_vmmap_type: "enum_alt \<equiv>
|
||||
alt_from_ord (enum :: vmmap_type list)"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation vmmap_type :: enumeration_both
|
||||
begin
|
||||
interpretation Arch .
|
||||
instance by (intro_classes, simp add: enum_alt_vmmap_type)
|
||||
end
|
||||
|
||||
(*>*)
|
||||
end_qualify
|
||||
context Arch begin global_naming X64
|
||||
|
||||
|
||||
end
|
||||
end
|
||||
Loading…
Reference in New Issue