arm-hyp execspec: add skel/ARM_HYP, m-skel/ARM_HYP, make haskell-translator work for ARM_HYP
(copied from ARM) Per-plaform CPP configuration for spec-check and make-spec. The configuration is still duplicated between the two scripts, but now the translation/check for ARM_HYP will use correct CPP settings.
This commit is contained in:
parent
8bfc2ac68c
commit
81663c978d
|
@ -29,6 +29,7 @@
|
||||||
/spec/design/version
|
/spec/design/version
|
||||||
/spec/design/*.thy
|
/spec/design/*.thy
|
||||||
/spec/design/ARM/*.thy
|
/spec/design/ARM/*.thy
|
||||||
|
/spec/design/ARM_HYP/*.thy
|
||||||
|
|
||||||
/spec/machine/ARM/MachineTypes.thy
|
/spec/machine/ARM/MachineTypes.thy
|
||||||
|
|
||||||
|
|
|
@ -0,0 +1,147 @@
|
||||||
|
(*
|
||||||
|
* Copyright 2014, General Dynamics C4 Systems
|
||||||
|
*
|
||||||
|
* This software may be distributed and modified according to the terms of
|
||||||
|
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||||
|
* See "LICENSE_GPLv2.txt" for details.
|
||||||
|
*
|
||||||
|
* @TAG(GD_GPL)
|
||||||
|
*)
|
||||||
|
|
||||||
|
chapter "ARM Machine Types"
|
||||||
|
|
||||||
|
theory MachineTypes
|
||||||
|
imports
|
||||||
|
"../../../lib/Monad_WP/NonDetMonad"
|
||||||
|
"../Setup_Locale"
|
||||||
|
Platform
|
||||||
|
begin
|
||||||
|
context Arch begin global_naming ARM
|
||||||
|
|
||||||
|
(* !!! Generated File !!! Skeleton in ../../design/skel-m/ARM/MachineTypes.thy *)
|
||||||
|
|
||||||
|
text {*
|
||||||
|
An implementation of the machine's types, defining register set
|
||||||
|
and some observable machine state.
|
||||||
|
*}
|
||||||
|
|
||||||
|
section "Types"
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/ARM.lhs CONTEXT ARM decls_only
|
||||||
|
(*<*)
|
||||||
|
end
|
||||||
|
context begin interpretation Arch .
|
||||||
|
requalify_types register
|
||||||
|
end
|
||||||
|
context Arch begin global_naming ARM
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/ARM.lhs CONTEXT ARM instanceproofs
|
||||||
|
(*>*)
|
||||||
|
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/ARM.lhs CONTEXT ARM bodies_only
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
text {*
|
||||||
|
The exclusive monitors state is observable in user mode.
|
||||||
|
The type for this is the type used in the Cambridge HOL4 ARM model.
|
||||||
|
*}
|
||||||
|
type_synonym exclusive_monitors = "(word32 \<Rightarrow> bool) list \<times> (word32 \<times> nat \<Rightarrow> bool)"
|
||||||
|
|
||||||
|
text {*
|
||||||
|
The full machine state is the state observable by the kernel plus
|
||||||
|
the underspecified rest above. The observable parts are the
|
||||||
|
interrupt controller (which IRQs are masked) and the memory of the
|
||||||
|
machine. The latter is shadow state: kernel memory is kept in a
|
||||||
|
separate, more abstract datatype; user memory is reflected down
|
||||||
|
to the underlying memory of the machine.
|
||||||
|
*}
|
||||||
|
end
|
||||||
|
|
||||||
|
qualify ARM (in Arch)
|
||||||
|
|
||||||
|
record
|
||||||
|
machine_state =
|
||||||
|
irq_masks :: "ARM.irq \<Rightarrow> bool"
|
||||||
|
irq_state :: nat
|
||||||
|
underlying_memory :: "word32 \<Rightarrow> word8"
|
||||||
|
exclusive_state :: ARM.exclusive_monitors
|
||||||
|
machine_state_rest :: ARM.machine_state_rest
|
||||||
|
|
||||||
|
consts irq_oracle :: "nat \<Rightarrow> 10 word"
|
||||||
|
|
||||||
|
axiomatization irq_oracle_max_irqInst where
|
||||||
|
irq_oracle_max_irq: "\<forall> n. (irq_oracle n) <= ARM.maxIRQ"
|
||||||
|
|
||||||
|
end_qualify
|
||||||
|
|
||||||
|
context Arch begin global_naming ARM
|
||||||
|
|
||||||
|
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 ARM.machine_monad" <= (type) "(ARM.machine_state, 'c) nondet_monad"
|
||||||
|
|
||||||
|
context Arch begin global_naming ARM
|
||||||
|
|
||||||
|
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 :: "word32 \<Rightarrow> word8"
|
||||||
|
where
|
||||||
|
"init_underlying_memory \<equiv> \<lambda>_. 0"
|
||||||
|
|
||||||
|
text {*
|
||||||
|
The initial exclusive state is the same constant
|
||||||
|
that clearExMonitor defaults it to.
|
||||||
|
*}
|
||||||
|
|
||||||
|
consts' default_exclusive_state :: exclusive_monitors
|
||||||
|
|
||||||
|
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,
|
||||||
|
exclusive_state = default_exclusive_state,
|
||||||
|
machine_state_rest = undefined \<rparr>"
|
||||||
|
|
||||||
|
|
||||||
|
(* Machine/Hardware/ARM.lhs - hardware_asid, vmfault_type and vmpage_size *)
|
||||||
|
#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.lhs CONTEXT ARM ONLY HardwareASID VMFaultType VMPageSize pageBits pageBitsForSize
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
context begin interpretation Arch .
|
||||||
|
requalify_types vmpage_size
|
||||||
|
end
|
||||||
|
|
||||||
|
context Arch begin global_naming ARM
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.lhs CONTEXT ARM instanceproofs ONLY HardwareASID VMFaultType VMPageSize
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -0,0 +1,21 @@
|
||||||
|
(*
|
||||||
|
* 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 ARM_H
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Object/Interrupt/ARM.lhs CONTEXT Arch decls_only ArchInv=
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
end
|
|
@ -0,0 +1,19 @@
|
||||||
|
(*
|
||||||
|
* 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 ARM_H
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Object/Interrupt/ARM.lhs CONTEXT ARM_H bodies_only ArchInv=ArchRetypeDecls_H
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -0,0 +1,37 @@
|
||||||
|
(*
|
||||||
|
* 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 ARM_H
|
||||||
|
|
||||||
|
text {*
|
||||||
|
An enumeration of arch-specific system call labels.
|
||||||
|
*}
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/API/InvocationLabels/ARM.lhs CONTEXT ARM_H ONLY ArchInvocationLabel
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
context begin interpretation Arch .
|
||||||
|
requalify_types arch_invocation_label
|
||||||
|
end
|
||||||
|
|
||||||
|
context Arch begin global_naming ARM_H
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/API/InvocationLabels/ARM.lhs CONTEXT ARM_H instanceproofs ONLY ArchInvocationLabel
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -0,0 +1,24 @@
|
||||||
|
(*
|
||||||
|
* 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
|
||||||
|
context Arch begin global_naming ARM_H
|
||||||
|
text {*
|
||||||
|
Arch-specific functions on invocation labels
|
||||||
|
*}
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/API/Invocation/ARM.lhs CONTEXT ARM_H ONLY isPDFlushLabel isPageFlushLabel
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -0,0 +1,180 @@
|
||||||
|
(*
|
||||||
|
* 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 ARM_H (in Arch)
|
||||||
|
|
||||||
|
instantiation ARM_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:
|
||||||
|
"injectKO e \<equiv> KOArch (KOPDE e)"
|
||||||
|
|
||||||
|
definition
|
||||||
|
koType_pde:
|
||||||
|
"koType (t::pde itself) \<equiv> ArchT PDET"
|
||||||
|
|
||||||
|
instance
|
||||||
|
by (intro_classes,
|
||||||
|
auto simp: projectKO_opt_pde injectKO_pde koType_pde
|
||||||
|
split: kernel_object.splits arch_kernel_object.splits)
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
instantiation ARM_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:
|
||||||
|
"injectKO e \<equiv> KOArch (KOPTE e)"
|
||||||
|
|
||||||
|
definition
|
||||||
|
koType_pte:
|
||||||
|
"koType (t::pte itself) \<equiv> ArchT PTET"
|
||||||
|
|
||||||
|
instance
|
||||||
|
by (intro_classes,
|
||||||
|
auto simp: projectKO_opt_pte injectKO_pte koType_pte
|
||||||
|
split: kernel_object.splits arch_kernel_object.splits)
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
|
||||||
|
instantiation ARM_H.asidpool :: pre_storable
|
||||||
|
begin
|
||||||
|
interpretation Arch .
|
||||||
|
|
||||||
|
definition
|
||||||
|
injectKO_asidpool:
|
||||||
|
"injectKO e \<equiv> KOArch (KOASIDPool e)"
|
||||||
|
|
||||||
|
definition
|
||||||
|
koType_asidpool:
|
||||||
|
"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 injectKO_asidpool koType_asidpool
|
||||||
|
split: kernel_object.splits arch_kernel_object.splits)
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
lemmas (in Arch) projectKO_opts_defs =
|
||||||
|
projectKO_opt_pde projectKO_opt_pte projectKO_opt_asidpool
|
||||||
|
ObjectInstances_H.projectKO_opts_defs
|
||||||
|
|
||||||
|
lemmas (in Arch) [simp] =
|
||||||
|
injectKO_pde koType_pde
|
||||||
|
injectKO_pte koType_pte
|
||||||
|
injectKO_asidpool koType_asidpool
|
||||||
|
|
||||||
|
-- --------------------------------------
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL_PREPARSE SEL4/Object/Structures/ARM.lhs
|
||||||
|
#INCLUDE_HASKELL_PREPARSE SEL4/Machine/Hardware/ARM.lhs
|
||||||
|
|
||||||
|
|
||||||
|
instantiation ARM_H.pde :: pspace_storable
|
||||||
|
begin
|
||||||
|
interpretation Arch .
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Object/Instances/ARM.lhs instanceproofs bodies_only ONLY PDE
|
||||||
|
|
||||||
|
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 ARM_H.pte :: pspace_storable
|
||||||
|
begin
|
||||||
|
interpretation Arch .
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Object/Instances/ARM.lhs instanceproofs bodies_only ONLY PTE
|
||||||
|
|
||||||
|
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 ARM_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_pde updateObject_pde
|
||||||
|
loadObject_pte updateObject_pte
|
||||||
|
loadObject_asidpool updateObject_asidpool
|
||||||
|
|
||||||
|
declare load_update_defs[simp del]
|
||||||
|
|
||||||
|
end_qualify
|
||||||
|
|
||||||
|
declare (in Arch) load_update_defs[simp]
|
||||||
|
|
||||||
|
end
|
|
@ -0,0 +1,31 @@
|
||||||
|
(*
|
||||||
|
* 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
|
||||||
|
ArchLabelFuns_H
|
||||||
|
"../FaultMonad_H"
|
||||||
|
"../EndpointDecls_H"
|
||||||
|
"../KernelInitMonad_H"
|
||||||
|
"../PSpaceFuns_H"
|
||||||
|
ArchObjInsts_H
|
||||||
|
begin
|
||||||
|
context Arch begin global_naming ARM_H
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/API/Invocation/ARM.lhs CONTEXT ARM_H decls_only NOT isPageFlushLabel isPDFlushLabel Invocation IRQControlInvocation CopyRegisterSets
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/API/Invocation/ARM.lhs CONTEXT ARM_H decls_only ONLY Invocation IRQControlInvocation CopyRegisterSets
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Object/ObjectType/ARM.lhs CONTEXT ARM_H Arch.Types=ArchTypes_H ArchInv= decls_only
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -0,0 +1,26 @@
|
||||||
|
(*
|
||||||
|
* 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 ARM_H
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Object/ObjectType/ARM.lhs CONTEXT ARM_H Arch.Types= ArchInv= bodies_only
|
||||||
|
#INCLUDE_HASKELL SEL4/API/Invocation/ARM.lhs bodies_only CONTEXT ARM_H NOT isPDFlushLabel isPageFlushLabel
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -0,0 +1,29 @@
|
||||||
|
(*
|
||||||
|
* 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 ARM_H
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Model/StateData/ARM.lhs CONTEXT ARM_H NOT ArmVSpaceRegionUse
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
end
|
|
@ -0,0 +1,36 @@
|
||||||
|
(*
|
||||||
|
* 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 ARM_H
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H decls_only
|
||||||
|
#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H instanceproofs
|
||||||
|
#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H bodies_only
|
||||||
|
|
||||||
|
datatype arch_kernel_object_type =
|
||||||
|
PDET
|
||||||
|
| PTET
|
||||||
|
| ASIDPoolT
|
||||||
|
|
||||||
|
primrec
|
||||||
|
archTypeOf :: "arch_kernel_object \<Rightarrow> arch_kernel_object_type"
|
||||||
|
where
|
||||||
|
"archTypeOf (KOPDE e) = PDET"
|
||||||
|
| "archTypeOf (KOPTE e) = PTET"
|
||||||
|
| "archTypeOf (KOASIDPool e) = ASIDPoolT"
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -0,0 +1,19 @@
|
||||||
|
(*
|
||||||
|
* 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 ARM_H
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Object/TCB/ARM.lhs CONTEXT ARM_H
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -0,0 +1,29 @@
|
||||||
|
(*
|
||||||
|
* 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 ARM_H
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Kernel/Thread/ARM.lhs CONTEXT Arch decls_only
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -0,0 +1,24 @@
|
||||||
|
(*
|
||||||
|
* 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 ARM_H
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Kernel/Thread/ARM.lhs CONTEXT ARM_H ARMHardware=ARM bodies_only
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -0,0 +1,85 @@
|
||||||
|
(*
|
||||||
|
* 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
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/API/Types/Universal.lhs all_bits
|
||||||
|
|
||||||
|
context Arch begin global_naming ARM_H
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/API/Types/ARM.lhs CONTEXT ARM_H
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
text {* object\_type instance proofs *}
|
||||||
|
|
||||||
|
qualify ARM_H (in Arch)
|
||||||
|
instantiation ARM_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,
|
||||||
|
SectionObject,
|
||||||
|
SuperSectionObject,
|
||||||
|
PageTableObject,
|
||||||
|
PageDirectoryObject
|
||||||
|
]"
|
||||||
|
|
||||||
|
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 ARM_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 ARM_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
|
|
@ -0,0 +1,22 @@
|
||||||
|
(*
|
||||||
|
* 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 ARM_H
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL_PREPARSE SEL4/Object/Structures.lhs CONTEXT ARM_H
|
||||||
|
#INCLUDE_HASKELL SEL4/Kernel/VSpace/ARM.lhs CONTEXT ARM_H decls_only ArchInv=
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -0,0 +1,31 @@
|
||||||
|
(*
|
||||||
|
* 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 ArchVSpace_H
|
||||||
|
imports
|
||||||
|
"../CNode_H"
|
||||||
|
"../KI_Decls_H"
|
||||||
|
ArchVSpaceDecls_H
|
||||||
|
begin
|
||||||
|
context Arch begin global_naming ARM_H
|
||||||
|
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Kernel/VSpace/ARM.lhs CONTEXT ARM_H bodies_only ArchInv=ArchRetypeDecls_H.ARM ArchLabels=ArchInvocationLabels_H.ARM NOT checkPDAt checkPTAt checkPDASIDMapMembership checkValidMappingSize vptrFromPPtr
|
||||||
|
|
||||||
|
defs checkValidMappingSize_def:
|
||||||
|
"checkValidMappingSize sz \<equiv> stateAssert
|
||||||
|
(\<lambda>s. 2 ^ pageBitsForSize sz <= gsMaxObjectSize s) []"
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -0,0 +1,23 @@
|
||||||
|
(*
|
||||||
|
* 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
|
||||||
|
context Arch begin global_naming ARM_H
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Model/StateData/ARM.lhs CONTEXT ARM_H ONLY ArmVSpaceRegionUse
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -0,0 +1,33 @@
|
||||||
|
(*
|
||||||
|
* 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/ARM/MachineOps"
|
||||||
|
State_H
|
||||||
|
begin
|
||||||
|
context Arch begin global_naming ARM_H
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.lhs Platform=Platform.ARM CONTEXT ARM_H NOT getMemoryRegions getDeviceRegions getKernelDevices loadWord storeWord storeWordVM getActiveIRQ ackInterrupt maskInterrupt configureTimer resetTimer debugPrint getRestartPC setNextPC clearMemory clearMemoryVM initMemory freeMemory writeTTBR0 setCurrentPD setGlobalPD setTTBCR setHardwareASID invalidateTLB invalidateTLB_ASID invalidateTLB_VAASID cleanByVA cleanByVA_PoU invalidateByVA invalidateByVA_I invalidate_I_PoU cleanInvalByVA branchFlush clean_D_PoU cleanInvalidate_D_PoC cleanInvalidate_D_PoU cleanInvalidateL2Range invalidateL2Range cleanL2Range isb dsb dmb getIFSR getDFSR getFAR HardwareASID wordFromPDE wordFromPTE VMFaultType VMPageSize pageBits pageBitsForSize toPAddr cacheLineBits cacheLine lineStart cacheRangeOp cleanCacheRange_PoC cleanInvalidateCacheRange_RAM cleanCacheRange_RAM cleanCacheRange_PoU invalidateCacheRange_RAM invalidateCacheRange_I branchFlushRange cleanCaches_PoU cleanInvalidateL1Caches addrFromPPtr ptrFromPAddr initIRQController MachineData
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
context begin interpretation Arch .
|
||||||
|
requalify_types vmrights
|
||||||
|
end
|
||||||
|
|
||||||
|
context Arch begin global_naming ARM_H
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.lhs CONTEXT ARM_H instanceproofs NOT HardwareASID VMFaultType VMPageSize
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.lhs CONTEXT ARM_H ONLY wordFromPDE wordFromPTE
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -0,0 +1,26 @@
|
||||||
|
(*
|
||||||
|
* 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/ARM/MachineTypes"
|
||||||
|
begin
|
||||||
|
context Arch begin global_naming ARM_H
|
||||||
|
|
||||||
|
definition
|
||||||
|
newContext :: "register => machine_word"
|
||||||
|
where
|
||||||
|
"newContext \<equiv> (K 0) aLU initContext"
|
||||||
|
|
||||||
|
end
|
||||||
|
end
|
|
@ -0,0 +1,51 @@
|
||||||
|
(*
|
||||||
|
* 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/ARM/MachineOps"
|
||||||
|
begin
|
||||||
|
context Arch begin global_naming ARM_H
|
||||||
|
|
||||||
|
definition
|
||||||
|
Word :: "machine_word \<Rightarrow> machine_word"
|
||||||
|
where
|
||||||
|
Word_def[simp]:
|
||||||
|
"Word \<equiv> id"
|
||||||
|
|
||||||
|
#INCLUDE_HASKELL SEL4/Machine/RegisterSet.lhs Arch=ARM CONTEXT ARM_H all_bits NOT UserContext UserMonad getRegister setRegister newContext mask Word PPtr
|
||||||
|
|
||||||
|
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
|
|
@ -74,8 +74,18 @@ then
|
||||||
(cd $L4CAP && git status --short) >> $SPEC/version
|
(cd $L4CAP && git status --short) >> $SPEC/version
|
||||||
fi
|
fi
|
||||||
|
|
||||||
|
# which architectures to process
|
||||||
ARCHES=("ARM" "X64" "ARM_HYP")
|
ARCHES=("ARM" "X64" "ARM_HYP")
|
||||||
|
|
||||||
|
# Match the CPP configuration used by SEL4.cabal and Setup.hs for Haskell build
|
||||||
|
# Note: these should be in sync with both the Haskell .cabal and Setup.hs,
|
||||||
|
# If these are not in sync, expect the unexpected.
|
||||||
|
# spec_check.sh has a copy of these, which should be updated in tandem.
|
||||||
|
# FIXME: move to a common location in haskell-translator (D.R.Y.)
|
||||||
|
declare -A cpp_opts
|
||||||
|
cpp_opts[ARM]="-DPLATFORM=QEmu -DPLATFORM_QEmu -DTARGET=ARM -DTARGET_ARM"
|
||||||
|
cpp_opts[ARM_HYP]="-DPLATFORM=TK1 -DPLATFORM_TK1 -DTARGET=ARM_HYP -DTARGET_ARM_HYP -DCONFIG_ARM_HYPERVISOR_SUPPORT"
|
||||||
|
|
||||||
NAMES=`cd $SKEL; ls *.thy`
|
NAMES=`cd $SKEL; ls *.thy`
|
||||||
|
|
||||||
SPECNONARCH="/tmp/make_spec_temp_nonarch_$$"
|
SPECNONARCH="/tmp/make_spec_temp_nonarch_$$"
|
||||||
|
@ -110,7 +120,7 @@ function send_filenames () {
|
||||||
for ARCH in ${ARCHES[@]}
|
for ARCH in ${ARCHES[@]}
|
||||||
do
|
do
|
||||||
send_filenames $ARCH > $TMPFILE
|
send_filenames $ARCH > $TMPFILE
|
||||||
L4CPP="-DTARGET=$ARCH -DTARGET_$ARCH -DPLATFORM=QEmu -DPLATFORM_QEmu"
|
L4CPP=${cpp_opts[$ARCH]}
|
||||||
export L4CPP
|
export L4CPP
|
||||||
cd $TRANSLATOR
|
cd $TRANSLATOR
|
||||||
python pars_skl.py $TMPFILE
|
python pars_skl.py $TMPFILE
|
||||||
|
|
Loading…
Reference in New Issue