riscv design: initial RISCV64 setup
This commit is contained in:
Gerwin Klein
parent
52b9f958aa
commit
05925b889d
|
|
@ -21,6 +21,7 @@
|
|||
/spec/design/*.thy
|
||||
/spec/design/ARM/*.thy
|
||||
/spec/design/ARM_HYP/*.thy
|
||||
/spec/design/RISCV64/*.thy
|
||||
/spec/design/X64/*.thy
|
||||
|
||||
/spec/machine/*/MachineTypes.thy
|
||||
|
|
|
|||
|
|
@ -23,9 +23,10 @@ SKEL_FILES := $(shell find ${SKEL_PATH} -name "*.thy")
|
|||
MSKEL_FILES := $(shell find ${MSKEL_PATH} -name "*.thy")
|
||||
HASKELL_FILES := $(shell find ${HASKELL_PATH} -regex ".*\.l?hs") # FIXME: add .hs
|
||||
HASKELL_TRANS := ${L4V_REPO_PATH}/tools/haskell-translator/make_spec.sh
|
||||
ARCH_DIRS += ARM ARM_HYP X64
|
||||
ARCH_DIRS += ARM ARM_HYP RISCV64 X64
|
||||
MACHINE_FILES += ${MACHINE_PATH}/ARM/MachineTypes.thy \
|
||||
${MACHINE_PATH}/ARM_HYP/MachineTypes.thy \
|
||||
${MACHINE_PATH}/RISCV64/MachineTypes.thy \
|
||||
${MACHINE_PATH}/X64/MachineTypes.thy
|
||||
|
||||
design : version
|
||||
|
|
|
|||
|
|
@ -0,0 +1,134 @@
|
|||
(*
|
||||
* 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 "RISCV 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 RISCV64
|
||||
|
||||
text {*
|
||||
An implementation of the machine's types, defining register set
|
||||
and some observable machine state.
|
||||
*}
|
||||
|
||||
section "Types"
|
||||
|
||||
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/RISCV64.hs CONTEXT RISCV64 decls_only NOT UserContext UserMonad getRegister setRegister newContext
|
||||
(*<*)
|
||||
|
||||
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
|
||||
end
|
||||
|
||||
context Arch begin global_naming RISCV64
|
||||
|
||||
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/RISCV64.hs CONTEXT RISCV64 instanceproofs
|
||||
(*>*)
|
||||
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/RISCV64.hs CONTEXT RISCV64 bodies_only NOT getRegister setRegister newContext
|
||||
|
||||
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 RISCV64 (in Arch)
|
||||
|
||||
record
|
||||
machine_state =
|
||||
irq_masks :: "RISCV64.irq \<Rightarrow> bool"
|
||||
irq_state :: nat
|
||||
underlying_memory :: "word64 \<Rightarrow> word8"
|
||||
device_state :: "word64 \<Rightarrow> word8 option"
|
||||
machine_state_rest :: RISCV64.machine_state_rest
|
||||
|
||||
consts irq_oracle :: "nat \<Rightarrow> word8"
|
||||
|
||||
end_qualify
|
||||
|
||||
context Arch begin global_naming RISCV64
|
||||
|
||||
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 RISCV64.machine_monad" <= (type) "(RISCV64.machine_state, 'c) nondet_monad"
|
||||
|
||||
context Arch begin global_naming RISCV64
|
||||
|
||||
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>"
|
||||
|
||||
#INCLUDE_HASKELL SEL4/Machine/Hardware/RISCV64.hs CONTEXT RISCV64 ONLY VMFaultType HypFaultType VMPageSize pageBits ptTranslationBits pageBitsForSize
|
||||
|
||||
end
|
||||
|
||||
context begin interpretation Arch .
|
||||
requalify_types vmpage_size
|
||||
end
|
||||
|
||||
context Arch begin global_naming RISCV64
|
||||
|
||||
#INCLUDE_HASKELL SEL4/Machine/Hardware/RISCV64.hs CONTEXT RISCV64 instanceproofs ONLY VMFaultType HypFaultType VMPageSize
|
||||
|
||||
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 "Fault Handlers"
|
||||
|
||||
theory ArchFaultHandler_H
|
||||
imports "../TCB_H" "../Structures_H"
|
||||
begin
|
||||
|
||||
context Arch begin global_naming RISCV64_H
|
||||
|
||||
#INCLUDE_HASKELL_PREPARSE SEL4/API/Failures/RISCV64.hs
|
||||
|
||||
#INCLUDE_HASKELL SEL4/API/Faults/RISCV64.hs decls_only
|
||||
#INCLUDE_HASKELL SEL4/API/Faults/RISCV64.hs bodies_only
|
||||
|
||||
end
|
||||
|
||||
end
|
||||
|
|
@ -0,0 +1,244 @@
|
|||
(*
|
||||
* Copyright 2014, General Dynamics C4 Systems
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_GPLv2.txt" for details.
|
||||
*
|
||||
* @TAG(GD_GPL)
|
||||
*)
|
||||
|
||||
chapter "Machine Operations"
|
||||
|
||||
theory MachineOps
|
||||
imports
|
||||
"../../../lib/$L4V_ARCH/WordSetup"
|
||||
"../../../lib/Monad_WP/NonDetMonad"
|
||||
"../MachineMonad"
|
||||
begin
|
||||
|
||||
section "Wrapping and Lifting Machine Operations"
|
||||
|
||||
text {*
|
||||
Most of the machine operations below work on the underspecified
|
||||
part of the machine state @{typ machine_state_rest} and cannot fail.
|
||||
We could express the latter by type (leaving out the failure flag),
|
||||
but if we later wanted to implement them,
|
||||
we'd have to set up a new hoare-logic
|
||||
framework for that type. So instead, we provide a wrapper for these
|
||||
operations that explicitly ignores the fail flag and sets it to
|
||||
False. Similarly, these operations never return an empty set of
|
||||
follow-on states, which would require the operation to fail.
|
||||
So we explicitly make this (non-existing) case a null operation.
|
||||
|
||||
All this is done only to avoid a large number of axioms (2 for each operation).
|
||||
*}
|
||||
|
||||
context Arch begin global_naming RISCV64
|
||||
|
||||
section "The Operations"
|
||||
|
||||
definition
|
||||
loadWord :: "machine_word \<Rightarrow> machine_word machine_monad"
|
||||
where "loadWord p \<equiv> do m \<leftarrow> gets underlying_memory;
|
||||
assert (p && mask 3 = 0);
|
||||
return (word_rcat (map (\<lambda>i. m (p + (7 - of_int i))) [0 .. 7]))
|
||||
od"
|
||||
|
||||
definition
|
||||
storeWord :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
|
||||
where "storeWord p w \<equiv> do
|
||||
assert (p && mask 3 = 0);
|
||||
modify (underlying_memory_update (
|
||||
fold (\<lambda>i m. m((p + (of_int i)) := word_rsplit w ! (7 - nat i))) [0 .. 7]))
|
||||
od"
|
||||
|
||||
lemma upto0_7_def:
|
||||
"[0..7] = [0,1,2,3,4,5,6,7]" by eval
|
||||
|
||||
lemma loadWord_storeWord_is_return:
|
||||
"p && mask 3 = 0 \<Longrightarrow> (do w \<leftarrow> loadWord p; storeWord p w od) = return ()"
|
||||
apply (rule ext)
|
||||
by (simp add: loadWord_def storeWord_def bind_def assert_def return_def
|
||||
modify_def gets_def get_def eval_nat_numeral put_def upto0_7_def
|
||||
word_rsplit_rcat_size word_size)
|
||||
|
||||
|
||||
text {* This instruction is required in the simulator, only. *}
|
||||
definition
|
||||
storeWordVM :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
|
||||
where "storeWordVM w p \<equiv> return ()"
|
||||
|
||||
consts'
|
||||
configureTimer_impl :: "unit machine_rest_monad"
|
||||
configureTimer_val :: "machine_state \<Rightarrow> irq"
|
||||
|
||||
definition
|
||||
configureTimer :: "irq machine_monad"
|
||||
where
|
||||
"configureTimer \<equiv> do
|
||||
machine_op_lift configureTimer_impl;
|
||||
gets configureTimer_val
|
||||
od"
|
||||
|
||||
consts' (* XXX: replaces configureTimer in new boot code
|
||||
TODO: remove configureTimer when haskell updated *)
|
||||
initTimer_impl :: "unit machine_rest_monad"
|
||||
definition
|
||||
initTimer :: "unit machine_monad"
|
||||
where "initTimer \<equiv> machine_op_lift initTimer_impl"
|
||||
|
||||
consts'
|
||||
resetTimer_impl :: "unit machine_rest_monad"
|
||||
|
||||
definition
|
||||
resetTimer :: "unit machine_monad"
|
||||
where "resetTimer \<equiv> machine_op_lift resetTimer_impl"
|
||||
|
||||
consts'
|
||||
invalidateTLB_impl :: "unit machine_rest_monad"
|
||||
definition
|
||||
invalidateTLB :: "unit machine_monad"
|
||||
where "invalidateTLB \<equiv> machine_op_lift invalidateTLB_impl"
|
||||
|
||||
lemmas cache_machine_op_defs = invalidateTLB_def
|
||||
|
||||
definition
|
||||
debugPrint :: "unit list \<Rightarrow> unit machine_monad"
|
||||
where
|
||||
debugPrint_def[simp]:
|
||||
"debugPrint \<equiv> \<lambda>message. return ()"
|
||||
|
||||
|
||||
-- "Interrupt controller operations"
|
||||
|
||||
text {*
|
||||
Interrupts that cannot occur while the kernel is running (e.g. at preemption points),
|
||||
but that can occur from user mode. Empty on plain x86-64.
|
||||
*}
|
||||
definition
|
||||
"non_kernel_IRQs = {}"
|
||||
|
||||
text {*
|
||||
@{term getActiveIRQ} is now derministic.
|
||||
It 'updates' the irq state to the reflect the passage of
|
||||
time since last the irq was gotten, then it gets the active
|
||||
IRQ (if there is one).
|
||||
*}
|
||||
definition
|
||||
getActiveIRQ :: "bool \<Rightarrow> (irq option) machine_monad"
|
||||
where
|
||||
"getActiveIRQ in_kernel \<equiv> do
|
||||
is_masked \<leftarrow> gets $ irq_masks;
|
||||
modify (\<lambda>s. s \<lparr> irq_state := irq_state s + 1 \<rparr>);
|
||||
active_irq \<leftarrow> gets $ irq_oracle \<circ> irq_state;
|
||||
if is_masked active_irq \<or> active_irq = 0xFF \<or> (in_kernel \<and> active_irq \<in> non_kernel_IRQs)
|
||||
then return None
|
||||
else return ((Some active_irq) :: irq option)
|
||||
od"
|
||||
|
||||
definition
|
||||
maskInterrupt :: "bool \<Rightarrow> irq \<Rightarrow> unit machine_monad"
|
||||
where
|
||||
"maskInterrupt m irq \<equiv>
|
||||
modify (\<lambda>s. s \<lparr> irq_masks := (irq_masks s) (irq := m) \<rparr>)"
|
||||
|
||||
definition
|
||||
ackInterrupt :: "irq \<Rightarrow> unit machine_monad"
|
||||
where
|
||||
"ackInterrupt \<equiv> \<lambda>irq. return ()"
|
||||
|
||||
definition
|
||||
setInterruptMode :: "irq \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> unit machine_monad"
|
||||
where
|
||||
"setInterruptMode \<equiv> \<lambda>irq levelTrigger polarityLow. return ()"
|
||||
|
||||
section "Memory Clearance"
|
||||
|
||||
text {* Clear memory contents to recycle it as user memory *}
|
||||
definition
|
||||
clearMemory :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
|
||||
where
|
||||
"clearMemory ptr bytelength \<equiv> mapM_x (\<lambda>p. storeWord p 0) [ptr, ptr + word_size .e. ptr + (of_nat bytelength) - 1]"
|
||||
|
||||
definition
|
||||
clearMemoryVM :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
|
||||
where
|
||||
"clearMemoryVM ptr bits \<equiv> return ()"
|
||||
|
||||
text {*
|
||||
Initialize memory to be used as user memory.
|
||||
Note that zeroing out the memory is redundant in the specifications.
|
||||
In any case, we cannot abstract from the call to cleanCacheRange,
|
||||
which appears in the implementation.
|
||||
*}
|
||||
abbreviation (input) "initMemory == clearMemory"
|
||||
|
||||
text {*
|
||||
Free memory that had been initialized as user memory.
|
||||
While freeing memory is a no-op in the implementation,
|
||||
we zero out the underlying memory in the specifications to avoid garbage.
|
||||
If we know that there is no garbage,
|
||||
we can compute from the implementation state
|
||||
what the exact memory content in the specifications is.
|
||||
*}
|
||||
definition
|
||||
freeMemory :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
|
||||
where
|
||||
"freeMemory ptr bits \<equiv>
|
||||
mapM_x (\<lambda>p. storeWord p 0) [ptr, ptr + word_size .e. ptr + 2 ^ bits - 1]"
|
||||
|
||||
|
||||
section "User Monad"
|
||||
|
||||
type_synonym user_regs = "register \<Rightarrow> machine_word"
|
||||
|
||||
datatype user_context = UserContext (user_regs : user_regs)
|
||||
|
||||
type_synonym 'a user_monad = "(user_context, 'a) nondet_monad"
|
||||
|
||||
definition
|
||||
getRegister :: "register \<Rightarrow> machine_word user_monad"
|
||||
where
|
||||
"getRegister r \<equiv> gets (\<lambda>s. user_regs s r)"
|
||||
|
||||
definition
|
||||
"modify_registers f uc \<equiv> UserContext (f (user_regs uc))"
|
||||
|
||||
definition
|
||||
setRegister :: "register \<Rightarrow> machine_word \<Rightarrow> unit user_monad"
|
||||
where
|
||||
"setRegister r v \<equiv> modify (\<lambda>s. UserContext ((user_regs s) (r := v)))"
|
||||
|
||||
definition
|
||||
"getRestartPC \<equiv> getRegister FaultIP"
|
||||
|
||||
definition
|
||||
"setNextPC \<equiv> setRegister NextIP"
|
||||
|
||||
|
||||
consts'
|
||||
hwASIDFlush_impl :: "machine_word \<Rightarrow> unit machine_rest_monad"
|
||||
definition
|
||||
hwASIDFlush :: "machine_word \<Rightarrow> unit machine_monad"
|
||||
where
|
||||
"hwASIDFlush asid \<equiv> machine_op_lift (hwASIDFlush_impl asid)"
|
||||
|
||||
consts'
|
||||
sFence_impl :: "unit machine_rest_monad"
|
||||
definition
|
||||
sFence :: "unit machine_monad"
|
||||
where
|
||||
"sFence \<equiv> machine_op_lift sFence_impl"
|
||||
|
||||
consts'
|
||||
sBadAddr_val :: "machine_state \<Rightarrow> machine_word"
|
||||
definition
|
||||
readSBADAddr :: "machine_word machine_monad"
|
||||
where
|
||||
"readSBADAddr = gets sBadAddr_val"
|
||||
|
||||
end
|
||||
|
||||
|
||||
end
|
||||
|
|
@ -0,0 +1,67 @@
|
|||
(*
|
||||
* Copyright 2014, General Dynamics C4 Systems
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_GPLv2.txt" for details.
|
||||
*
|
||||
* @TAG(GD_GPL)
|
||||
*)
|
||||
|
||||
chapter "Platform Definitions"
|
||||
|
||||
theory Platform
|
||||
imports
|
||||
"../../../lib/Lib"
|
||||
"../../../lib/Word_Lib/Word_Enum"
|
||||
"../../../lib/Defs"
|
||||
"../Setup_Locale"
|
||||
begin
|
||||
|
||||
context Arch begin global_naming RISCV64
|
||||
|
||||
type_synonym irq = word32
|
||||
type_synonym paddr = word64
|
||||
|
||||
|
||||
abbreviation (input) "toPAddr \<equiv> id"
|
||||
abbreviation (input) "fromPAddr \<equiv> id"
|
||||
|
||||
definition
|
||||
kernelBase :: word64 where
|
||||
"kernelBase = 0xFFFFFFFF80000000"
|
||||
|
||||
definition
|
||||
paddrLoad :: word64 where
|
||||
"paddrLoad = 0xC0000000"
|
||||
|
||||
definition
|
||||
kernelBaseOffset :: word64 where
|
||||
"kernelBaseOffset = kernelBase - paddrLoad"
|
||||
|
||||
definition
|
||||
pptrBase :: word64 where
|
||||
"pptrBase = 0xFFFFFFC000000000"
|
||||
|
||||
definition
|
||||
ptrFromPAddr :: "paddr \<Rightarrow> word64" where
|
||||
"ptrFromPAddr paddr \<equiv> paddr + pptrBase"
|
||||
|
||||
definition
|
||||
addrFromPPtr :: "word64 \<Rightarrow> paddr" where
|
||||
"addrFromPPtr pptr \<equiv> pptr - pptrBase"
|
||||
|
||||
definition
|
||||
addrFromKPPtr :: "word64 \<Rightarrow> paddr" where
|
||||
"addrFromKPPtr pptr \<equiv> pptr - kernelBaseOffset"
|
||||
|
||||
definition
|
||||
minIRQ :: "irq" where
|
||||
"minIRQ \<equiv> 0"
|
||||
|
||||
definition
|
||||
maxIRQ :: "irq" where
|
||||
"maxIRQ \<equiv> 5"
|
||||
|
||||
end
|
||||
end
|
||||
Loading…
Reference in New Issue