aspec/haskell/machine: refactor user_context interface
- remove separate abstract set_/get_register implementation, directly use machine op - make interface aware that user_context does not always need to equal (register => machine_word) - introduce FPU state on x64
This commit is contained in:
Gerwin Klein
parent
ba97e55d1f
commit
d9c08fc73f
|
|
@ -23,7 +23,7 @@ context Arch begin global_naming ARM_A
|
|||
definition
|
||||
arch_tcb_set_ipc_buffer :: "machine_word \<Rightarrow> vspace_ref \<Rightarrow> (unit, 'a::state_ext) s_monad"
|
||||
where
|
||||
"arch_tcb_set_ipc_buffer target ptr \<equiv> as_user target $ set_register TPIDRURW ptr"
|
||||
"arch_tcb_set_ipc_buffer target ptr \<equiv> as_user target $ setRegister TPIDRURW ptr"
|
||||
|
||||
(* Allow most pre-existing proofs to continue to work. *)
|
||||
declare arch_tcb_set_ipc_buffer_def [simp]
|
||||
|
|
|
|||
|
|
@ -315,6 +315,16 @@ definition
|
|||
where
|
||||
"arch_tcb_context_get a_tcb \<equiv> tcb_context a_tcb"
|
||||
|
||||
definition
|
||||
arch_tcb_set_registers :: "(register \<Rightarrow> machine_word) \<Rightarrow> arch_tcb \<Rightarrow> arch_tcb"
|
||||
where
|
||||
"arch_tcb_set_registers \<equiv> arch_tcb_context_set"
|
||||
|
||||
definition
|
||||
arch_tcb_get_registers :: "arch_tcb \<Rightarrow> register \<Rightarrow> machine_word"
|
||||
where
|
||||
"arch_tcb_get_registers \<equiv> arch_tcb_context_get"
|
||||
|
||||
end
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ context Arch begin global_naming ARM_A
|
|||
definition
|
||||
arch_tcb_set_ipc_buffer :: "machine_word \<Rightarrow> vspace_ref \<Rightarrow> (unit, 'a::state_ext) s_monad"
|
||||
where
|
||||
"arch_tcb_set_ipc_buffer target ptr \<equiv> as_user target $ set_register TPIDRURW ptr"
|
||||
"arch_tcb_set_ipc_buffer target ptr \<equiv> as_user target $ setRegister TPIDRURW ptr"
|
||||
|
||||
(* Allow most pre-existing proofs to continue to work. *)
|
||||
declare arch_tcb_set_ipc_buffer_def [simp]
|
||||
|
|
|
|||
|
|
@ -410,6 +410,16 @@ definition
|
|||
where
|
||||
"arch_tcb_context_get a_tcb \<equiv> tcb_context a_tcb"
|
||||
|
||||
definition
|
||||
arch_tcb_set_registers :: "(register \<Rightarrow> machine_word) \<Rightarrow> arch_tcb \<Rightarrow> arch_tcb"
|
||||
where
|
||||
"arch_tcb_set_registers \<equiv> arch_tcb_context_set"
|
||||
|
||||
definition
|
||||
arch_tcb_get_registers :: "arch_tcb \<Rightarrow> register \<Rightarrow> machine_word"
|
||||
where
|
||||
"arch_tcb_get_registers \<equiv> arch_tcb_context_get"
|
||||
|
||||
end
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -32,7 +32,7 @@ definition
|
|||
get_message_info :: "obj_ref \<Rightarrow> (message_info,'z::state_ext) s_monad"
|
||||
where
|
||||
"get_message_info thread \<equiv> do
|
||||
x \<leftarrow> as_user thread $ get_register msg_info_register;
|
||||
x \<leftarrow> as_user thread $ getRegister msg_info_register;
|
||||
return $ data_to_message_info x
|
||||
od"
|
||||
|
||||
|
|
@ -173,14 +173,14 @@ where
|
|||
| "handle_fault_reply (UnknownSyscallException n) thread label msg = do
|
||||
t \<leftarrow> arch_get_sanitise_register_info thread;
|
||||
as_user thread $ zipWithM_x
|
||||
(\<lambda>r v. set_register r $ sanitise_register t r v)
|
||||
(\<lambda>r v. setRegister r $ sanitise_register t r v)
|
||||
syscallMessage msg;
|
||||
return (label = 0)
|
||||
od"
|
||||
| "handle_fault_reply (UserException exception code) thread label msg = do
|
||||
t \<leftarrow> arch_get_sanitise_register_info thread;
|
||||
as_user thread $ zipWithM_x
|
||||
(\<lambda>r v. set_register r $ sanitise_register t r v)
|
||||
(\<lambda>r v. setRegister r $ sanitise_register t r v)
|
||||
exceptionMessage msg;
|
||||
return (label = 0)
|
||||
od"
|
||||
|
|
@ -200,7 +200,7 @@ where
|
|||
(label, msg) \<leftarrow> make_fault_msg f sender;
|
||||
sent \<leftarrow> set_mrs receiver buf msg;
|
||||
set_message_info receiver $ MI sent 0 0 label;
|
||||
as_user receiver $ set_register badge_register badge
|
||||
as_user receiver $ setRegister badge_register badge
|
||||
od"
|
||||
|
||||
section {* Synchronous Message Transfers *}
|
||||
|
|
@ -222,7 +222,7 @@ where
|
|||
mi' \<leftarrow> transfer_caps mi caps endpoint receiver rbuf;
|
||||
set_message_info receiver $ MI mrs_transferred (mi_extra_caps mi')
|
||||
(mi_caps_unwrapped mi') (mi_label mi);
|
||||
as_user receiver $ set_register badge_register badge
|
||||
as_user receiver $ setRegister badge_register badge
|
||||
od"
|
||||
|
||||
text {* Transfer a message either involving a fault or not. *}
|
||||
|
|
@ -281,7 +281,7 @@ where
|
|||
"reply_from_kernel thread x \<equiv> do
|
||||
(label, msg) \<leftarrow> return x;
|
||||
buf \<leftarrow> lookup_ipc_buffer True thread;
|
||||
as_user thread $ set_register badge_register 0;
|
||||
as_user thread $ setRegister badge_register 0;
|
||||
len \<leftarrow> set_mrs thread buf msg;
|
||||
set_message_info thread $ MI len 0 0 label
|
||||
od"
|
||||
|
|
@ -363,7 +363,7 @@ where
|
|||
ntfn \<leftarrow> get_notification ntfnptr;
|
||||
case ntfn_obj ntfn of
|
||||
ActiveNtfn badge \<Rightarrow> do
|
||||
as_user tcb $ set_register badge_register badge;
|
||||
as_user tcb $ setRegister badge_register badge;
|
||||
set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn
|
||||
od
|
||||
| _ \<Rightarrow> fail
|
||||
|
|
@ -372,7 +372,7 @@ where
|
|||
definition
|
||||
do_nbrecv_failed_transfer :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
|
||||
where
|
||||
"do_nbrecv_failed_transfer thread = do as_user thread $ set_register badge_register 0; return () od"
|
||||
"do_nbrecv_failed_transfer thread = do as_user thread $ setRegister badge_register 0; return () od"
|
||||
|
||||
definition
|
||||
receive_ipc :: "obj_ref \<Rightarrow> cap \<Rightarrow> bool \<Rightarrow> (unit,'z::state_ext) s_monad"
|
||||
|
|
@ -442,7 +442,7 @@ where
|
|||
ntfn_obj = (case rest of [] \<Rightarrow> IdleNtfn | _ \<Rightarrow> WaitingNtfn rest),
|
||||
ntfn_bound_tcb = bound_tcb \<rparr>;
|
||||
set_thread_state dest Running;
|
||||
as_user dest $ set_register badge_register badge;
|
||||
as_user dest $ setRegister badge_register badge;
|
||||
do_extended_op (possible_switch_to dest)
|
||||
|
||||
od"
|
||||
|
|
@ -471,7 +471,7 @@ where
|
|||
then do
|
||||
cancel_ipc tcb;
|
||||
set_thread_state tcb Running;
|
||||
as_user tcb $ set_register badge_register badge;
|
||||
as_user tcb $ setRegister badge_register badge;
|
||||
do_extended_op (possible_switch_to tcb)
|
||||
od
|
||||
else set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge)
|
||||
|
|
@ -512,7 +512,7 @@ where
|
|||
od
|
||||
| False \<Rightarrow> do_nbrecv_failed_transfer thread)
|
||||
| ActiveNtfn badge \<Rightarrow> do
|
||||
as_user thread $ set_register badge_register badge;
|
||||
as_user thread $ setRegister badge_register badge;
|
||||
set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn
|
||||
od
|
||||
od"
|
||||
|
|
|
|||
|
|
@ -22,6 +22,7 @@ context begin interpretation Arch .
|
|||
|
||||
requalify_types
|
||||
user_context
|
||||
user_monad
|
||||
register
|
||||
data
|
||||
obj_ref
|
||||
|
|
@ -56,23 +57,10 @@ requalify_consts
|
|||
data_offset_to_nat
|
||||
combine_ntfn_badges
|
||||
|
||||
|
||||
end
|
||||
|
||||
|
||||
type_synonym 'a user_monad = "(user_context, 'a) nondet_monad"
|
||||
|
||||
definition
|
||||
get_register :: "register \<Rightarrow> data user_monad" where
|
||||
"get_register r \<equiv> gets (\<lambda>uc. uc r)"
|
||||
|
||||
definition
|
||||
set_registers :: "(register \<Rightarrow> data) \<Rightarrow> unit user_monad" where
|
||||
"set_registers \<equiv> put"
|
||||
|
||||
definition
|
||||
set_register :: "register \<Rightarrow> data \<Rightarrow> unit user_monad" where
|
||||
"set_register r v \<equiv> modify (\<lambda>uc. uc (r := v))"
|
||||
|
||||
(* Needs to be done here after plain type names are exported *)
|
||||
translations
|
||||
(type) "'a user_monad" <= (type) "user_context \<Rightarrow> ('a \<times> user_context) set \<times> bool"
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -46,6 +46,8 @@ requalify_consts
|
|||
default_arch_tcb
|
||||
arch_tcb_context_get
|
||||
arch_tcb_context_set
|
||||
arch_tcb_set_registers
|
||||
arch_tcb_get_registers
|
||||
cte_level_bits
|
||||
tcb_bits
|
||||
endpoint_bits
|
||||
|
|
|
|||
|
|
@ -219,7 +219,7 @@ where
|
|||
thread \<leftarrow> liftE $ gets cur_thread;
|
||||
info \<leftarrow> without_preemption $ get_message_info thread;
|
||||
ptr \<leftarrow> without_preemption $ liftM data_to_cptr $
|
||||
as_user thread $ get_register cap_register;
|
||||
as_user thread $ getRegister cap_register;
|
||||
syscall
|
||||
(doE
|
||||
(cap, slot) \<leftarrow> cap_fault_on_failure (of_bl ptr) False $
|
||||
|
|
@ -279,7 +279,7 @@ definition
|
|||
thread \<leftarrow> gets cur_thread;
|
||||
|
||||
ep_cptr \<leftarrow> liftM data_to_cptr $ as_user thread $
|
||||
get_register cap_register;
|
||||
getRegister cap_register;
|
||||
|
||||
(cap_fault_on_failure (of_bl ep_cptr) True $ doE
|
||||
ep_cap \<leftarrow> lookup_cap thread ep_cptr;
|
||||
|
|
|
|||
|
|
@ -40,7 +40,7 @@ definition
|
|||
set_message_info :: "obj_ref \<Rightarrow> message_info \<Rightarrow> (unit,'z::state_ext) s_monad"
|
||||
where
|
||||
"set_message_info thread info \<equiv>
|
||||
as_user thread $ set_register msg_info_register $
|
||||
as_user thread $ setRegister msg_info_register $
|
||||
message_info_to_data info"
|
||||
|
||||
|
||||
|
|
@ -49,11 +49,11 @@ definition
|
|||
"set_mrs thread buf msgs \<equiv>
|
||||
do
|
||||
tcb \<leftarrow> gets_the $ get_tcb thread;
|
||||
context \<leftarrow> return (arch_tcb_context_get (tcb_arch tcb));
|
||||
context \<leftarrow> return (arch_tcb_get_registers (tcb_arch tcb));
|
||||
new_regs \<leftarrow> return (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers)
|
||||
then msgs ! (the_index msg_registers reg)
|
||||
else context reg);
|
||||
set_object thread (TCB (tcb \<lparr> tcb_arch := arch_tcb_context_set new_regs (tcb_arch tcb) \<rparr>));
|
||||
set_object thread (TCB (tcb \<lparr> tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb) \<rparr>));
|
||||
remaining_msgs \<leftarrow> return (drop (length msg_registers) msgs);
|
||||
case buf of
|
||||
None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length msgs))
|
||||
|
|
|
|||
|
|
@ -97,8 +97,8 @@ definition
|
|||
do
|
||||
hardware_mrs \<leftarrow> return $ take (unat n) msg_registers;
|
||||
mapM (\<lambda>r. do
|
||||
v \<leftarrow> as_user sender $ get_register r;
|
||||
as_user receiver $ set_register r v
|
||||
v \<leftarrow> as_user sender $ getRegister r;
|
||||
as_user receiver $ setRegister r v
|
||||
od) hardware_mrs;
|
||||
buf_mrs \<leftarrow> case (sbuf, rbuf) of
|
||||
(Some sb_ptr, Some rb_ptr) \<Rightarrow> mapM (\<lambda>x. do
|
||||
|
|
@ -274,7 +274,7 @@ definition
|
|||
get_mrs :: "obj_ref \<Rightarrow> obj_ref option \<Rightarrow> message_info \<Rightarrow>
|
||||
(message list,'z::state_ext) s_monad" where
|
||||
"get_mrs thread buf info \<equiv> do
|
||||
context \<leftarrow> thread_get (arch_tcb_context_get o tcb_arch) thread;
|
||||
context \<leftarrow> thread_get (arch_tcb_get_registers o tcb_arch) thread;
|
||||
cpu_mrs \<leftarrow> return (map context msg_registers);
|
||||
buf_mrs \<leftarrow> case buf
|
||||
of None \<Rightarrow> return []
|
||||
|
|
|
|||
|
|
@ -39,7 +39,7 @@ where
|
|||
|
||||
definition
|
||||
empty_context :: user_context where
|
||||
"empty_context \<equiv> \<lambda>_. 0"
|
||||
"empty_context \<equiv> UserContext (\<lambda>_. 0) (\<lambda>_. 0)"
|
||||
|
||||
definition init_arch_tcb :: arch_tcb where
|
||||
"init_arch_tcb \<equiv> \<lparr> tcb_context = empty_context \<rparr>"
|
||||
|
|
|
|||
|
|
@ -57,7 +57,7 @@ where
|
|||
definition
|
||||
arch_post_modify_registers :: "obj_ref \<Rightarrow> obj_ref \<Rightarrow> (unit, 'a::state_ext) s_monad"
|
||||
where
|
||||
"arch_post_modify_registers cur t \<equiv> when (t \<noteq> cur) $ as_user t $ set_register ErrorRegister 0"
|
||||
"arch_post_modify_registers cur t \<equiv> when (t \<noteq> cur) $ as_user t $ setRegister ErrorRegister 0"
|
||||
|
||||
end
|
||||
end
|
||||
|
|
|
|||
|
|
@ -401,9 +401,9 @@ section "Arch-specific TCB"
|
|||
|
||||
qualify X64_A (in Arch)
|
||||
|
||||
(* arch specific part of tcb: this must have a field for user context *)
|
||||
text \<open> Arch-specific part of a TCB: this must have at least a field for user context. \<close>
|
||||
record arch_tcb =
|
||||
tcb_context :: user_context
|
||||
tcb_context :: user_context
|
||||
|
||||
end_qualify
|
||||
|
||||
|
|
@ -413,7 +413,9 @@ definition
|
|||
default_arch_tcb :: arch_tcb where
|
||||
"default_arch_tcb \<equiv> \<lparr>tcb_context = new_context\<rparr>"
|
||||
|
||||
text {* accesors for @{text "tcb_context"} inside @{text "arch_tcb"} *}
|
||||
text \<open> Accessors for @{text "tcb_context"} inside @{text "arch_tcb"}.
|
||||
These are later used to implement @{text as_user}, i.e.\ need to be
|
||||
compatible with @{text user_monad}.\<close>
|
||||
definition
|
||||
arch_tcb_context_set :: "user_context \<Rightarrow> arch_tcb \<Rightarrow> arch_tcb"
|
||||
where
|
||||
|
|
@ -424,6 +426,23 @@ definition
|
|||
where
|
||||
"arch_tcb_context_get a_tcb \<equiv> tcb_context a_tcb"
|
||||
|
||||
(* FIXME: the following means that we break the set/getRegister abstraction
|
||||
and should move some of this into the machine interface *)
|
||||
text \<open>
|
||||
Accessors for the user register part of the @{text "arch_tcb"}.
|
||||
(Because @{typ "register \<Rightarrow> machine_word"} may not be equal to @{typ user_context}).
|
||||
\<close>
|
||||
definition
|
||||
arch_tcb_set_registers :: "(register \<Rightarrow> machine_word) \<Rightarrow> arch_tcb \<Rightarrow> arch_tcb"
|
||||
where
|
||||
"arch_tcb_set_registers regs a_tcb \<equiv>
|
||||
a_tcb \<lparr> tcb_context := UserContext (fpu_state (tcb_context a_tcb)) regs \<rparr>"
|
||||
|
||||
definition
|
||||
arch_tcb_get_registers :: "arch_tcb \<Rightarrow> register \<Rightarrow> machine_word"
|
||||
where
|
||||
"arch_tcb_get_registers a_tcb \<equiv> user_regs (tcb_context a_tcb)"
|
||||
|
||||
end
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -30,7 +30,7 @@ text {*
|
|||
references, user pointers, word-based data, cap references, and so
|
||||
on. This theory provides an instantiation of these names to concrete
|
||||
types for the x64 architecture. Other architectures may have slightly
|
||||
different instantations.
|
||||
different instantiations.
|
||||
*}
|
||||
type_synonym obj_ref = machine_word
|
||||
type_synonym vspace_ref = machine_word
|
||||
|
|
@ -106,11 +106,9 @@ definition
|
|||
slot_bits :: nat where
|
||||
"slot_bits \<equiv> 5"
|
||||
|
||||
type_synonym user_context = "register \<Rightarrow> data"
|
||||
|
||||
definition
|
||||
new_context :: "user_context" where
|
||||
"new_context \<equiv> (\<lambda>r. 0) aLU initContext"
|
||||
"new_context \<equiv> UserContext (\<lambda>r. 0) ((\<lambda>r. 0)(CS := selCS3, SS := selDS3, FLAGS := 0x202))"
|
||||
|
||||
definition
|
||||
pptr_base :: "machine_word" where
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@ text {*
|
|||
|
||||
section "Types"
|
||||
|
||||
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/ARM.lhs CONTEXT ARM decls_only
|
||||
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/ARM.lhs CONTEXT ARM decls_only NOT UserContext UserMonad getRegister setRegister newContext
|
||||
(*<*)
|
||||
|
||||
section "Machine Words"
|
||||
|
|
@ -48,7 +48,7 @@ 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
|
||||
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/ARM.lhs CONTEXT ARM bodies_only NOT getRegister setRegister newContext
|
||||
|
||||
section "Machine State"
|
||||
|
||||
|
|
|
|||
|
|
@ -27,7 +27,7 @@ text {*
|
|||
|
||||
section "Types"
|
||||
|
||||
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/ARM.lhs CONTEXT ARM_HYP decls_only
|
||||
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/ARM.lhs CONTEXT ARM_HYP decls_only NOT UserContext UserMonad getRegister setRegister newContext
|
||||
(*<*)
|
||||
|
||||
type_synonym machine_word_len = 32
|
||||
|
|
@ -48,7 +48,7 @@ context Arch begin global_naming ARM_HYP
|
|||
|
||||
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/ARM.lhs CONTEXT ARM_HYP instanceproofs
|
||||
(*>*)
|
||||
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/ARM.lhs CONTEXT ARM_HYP bodies_only
|
||||
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/ARM.lhs CONTEXT ARM_HYP bodies_only NOT getRegister setRegister newContext
|
||||
|
||||
section "Machine State"
|
||||
|
||||
|
|
|
|||
|
|
@ -28,7 +28,7 @@ text {*
|
|||
|
||||
section "Types"
|
||||
|
||||
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/X64.lhs CONTEXT X64 decls_only
|
||||
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/X64.lhs CONTEXT X64 decls_only NOT UserContext UserMonad getRegister setRegister newContext
|
||||
(*<*)
|
||||
|
||||
section "Machine Words"
|
||||
|
|
@ -50,7 +50,7 @@ context Arch begin global_naming X64
|
|||
|
||||
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/X64.lhs CONTEXT X64 instanceproofs
|
||||
(*>*)
|
||||
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/X64.lhs CONTEXT X64 bodies_only
|
||||
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/X64.lhs CONTEXT X64 bodies_only NOT getRegister setRegister newContext
|
||||
|
||||
section "Machine State"
|
||||
|
||||
|
|
|
|||
|
|
@ -13,14 +13,14 @@ chapter "Register Set"
|
|||
theory RegisterSet_H
|
||||
imports
|
||||
"../../../lib/HaskellLib_H"
|
||||
"../../machine/X64/MachineTypes"
|
||||
"../../machine/X64/MachineOps"
|
||||
begin
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
definition
|
||||
newContext :: "register => machine_word"
|
||||
newContext :: "user_context"
|
||||
where
|
||||
"newContext \<equiv> (K 0) aLU initContext"
|
||||
"newContext \<equiv> UserContext (\<lambda>w. 0) ((K 0) aLU initContext)"
|
||||
|
||||
end
|
||||
end
|
||||
|
|
|
|||
|
|
@ -16,9 +16,7 @@ chapter "Machine State"
|
|||
|
||||
theory State_H
|
||||
imports
|
||||
"../../../lib/HaskellLib_H"
|
||||
RegisterSet_H
|
||||
"../../machine/X64/MachineOps"
|
||||
begin
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@ This module contains the architecture-specific thread switch code for the ARM.
|
|||
\begin{impdetails}
|
||||
|
||||
> import SEL4.Machine
|
||||
> import SEL4.Machine.RegisterSet.ARM
|
||||
> import SEL4.Machine.RegisterSet.ARM (Register(..))
|
||||
> import SEL4.Model.StateData
|
||||
> import SEL4.Object.Structures
|
||||
> import SEL4.Object.TCB
|
||||
|
|
|
|||
|
|
@ -27,7 +27,7 @@ We use the C preprocessor to select a target architecture. Also, this file makes
|
|||
> import Data.Helpers
|
||||
> import Foreign.Storable
|
||||
|
||||
> import Control.Monad.State(State, gets, modify)
|
||||
> import Control.Monad.State(State,liftM)
|
||||
|
||||
\end{impdetails}
|
||||
|
||||
|
|
@ -76,17 +76,11 @@ The types defined here are used for kernel and user pointers. Depending on the a
|
|||
> newtype VPtr = VPtr { fromVPtr :: Word }
|
||||
> deriving (Show, Eq, Num, Bits, FiniteBits, Ord, Enum, Bounded)
|
||||
|
||||
\subsubsection{User-level Context}
|
||||
|
||||
The representation of the user-level context of a thread is an array of machine words, indexed by register name.
|
||||
|
||||
> newtype UserContext = UC { fromUC :: Array Register Word }
|
||||
> deriving Show
|
||||
|
||||
\subsection{Monads}
|
||||
|
||||
"UserMonad" is a specialisation of "Control.Monad.State", used to execute functions that have access only to the user-level context of a single thread.
|
||||
|
||||
> type UserContext = Arch.UserContext
|
||||
> type UserMonad = State UserContext
|
||||
|
||||
\subsection{Functions and Constants}
|
||||
|
|
@ -140,21 +134,20 @@ This list may be empty, though it should contain as many registers as possible.
|
|||
|
||||
\end{description}
|
||||
|
||||
\subsubsection{User-level Context}
|
||||
|
||||
A new user-level context is a list of values for the machine's registers. Registers are generally initialised to 0, but there may be machine-specific initial values for certain registers.
|
||||
|
||||
> newContext :: UserContext
|
||||
> newContext = UC $ (funArray $ const 0)//initContext
|
||||
> where initContext = map (\(r,v) -> (Register r, Word v)) Arch.initContext
|
||||
|
||||
Functions are provided to get and set a single register.
|
||||
Functions for getting and setting registers.
|
||||
|
||||
> getRegister :: Register -> UserMonad Word
|
||||
> getRegister r = gets $ (!r) . fromUC
|
||||
> getRegister (Register r) = do
|
||||
> w <- Arch.getRegister r
|
||||
> return (Word w)
|
||||
|
||||
> setRegister :: Register -> Word -> UserMonad ()
|
||||
> setRegister r v = modify $ UC . (//[(r, v)]) . fromUC
|
||||
> setRegister (Register r) (Word v)= Arch.setRegister r v
|
||||
|
||||
> newContext :: UserContext
|
||||
> newContext = Arch.newContext
|
||||
|
||||
|
||||
\subsubsection{Miscellaneous}
|
||||
|
||||
|
|
|
|||
|
|
@ -22,6 +22,8 @@ This module defines the ARM register set.
|
|||
|
||||
> import qualified Data.Word
|
||||
> import Data.Array
|
||||
> import Data.Helpers
|
||||
> import Control.Monad.State(State, gets, modify)
|
||||
|
||||
\end{impdetails}
|
||||
|
||||
|
|
@ -70,3 +72,21 @@ This module defines the ARM register set.
|
|||
> initContext :: [(Register, Word)]
|
||||
> initContext = [(CPSR,0x150)] -- User mode
|
||||
|
||||
\subsubsection{User-level Context}
|
||||
|
||||
The representation of the user-level context of a thread is an array of machine words, indexed by register name.
|
||||
|
||||
> newtype UserContext = UC { fromUC :: Array Register Word }
|
||||
> deriving Show
|
||||
|
||||
A new user-level context is a list of values for the machine's registers. Registers are generally initialised to 0, but there may be machine-specific initial values for certain registers.
|
||||
|
||||
> newContext :: UserContext
|
||||
> newContext = UC $ (funArray $ const 0)//initContext
|
||||
|
||||
Functions are provided to get and set a single register.
|
||||
|
||||
> getRegister r = gets $ (!r) . fromUC
|
||||
|
||||
> setRegister r v = modify $ UC . (//[(r, v)]) . fromUC
|
||||
|
||||
|
|
|
|||
|
|
@ -16,6 +16,9 @@ This module defines the x86 64-bit register set.
|
|||
> import qualified Data.Word
|
||||
> import Data.Array
|
||||
> import Data.Bits
|
||||
> import Data.Helpers
|
||||
|
||||
> import Control.Monad.State(State, gets, modify)
|
||||
|
||||
\end{impdetails}
|
||||
|
||||
|
|
@ -71,3 +74,30 @@ This module defines the x86 64-bit register set.
|
|||
> , (FLAGS, bit 9 .|. bit 1) -- User mode
|
||||
> ]
|
||||
|
||||
\subsubsection{User-level Context}
|
||||
|
||||
On X64 the representation of the user-level context of a thread is an array
|
||||
of machine words, indexed by register name for the user registers, plus the
|
||||
state of the FPU, which we represent as a function from machine word to bytes
|
||||
with the convention that all unused entries map to 0. There are no operations
|
||||
on the FPU state apart from save and restore at kernel entry and exit.
|
||||
|
||||
> data UserContext = UC { fromUC :: Array Register Word,
|
||||
> fpuState :: Array Word Data.Word.Word8 }
|
||||
> deriving Show
|
||||
|
||||
|
||||
A new user-level context is a list of values for the machine's registers.
|
||||
Registers are generally initialised to 0, but there may be machine-specific
|
||||
initial values for certain registers. The FPU state contains 576 bytes,
|
||||
initialised to 0.
|
||||
|
||||
> newContext :: UserContext
|
||||
> newContext = UC ((funArray $ const 0)//initContext) (funPartialArray (const 0) (0,575))
|
||||
|
||||
Functions are provided to get and set a single register.
|
||||
|
||||
> getRegister r = gets $ (!r) . fromUC
|
||||
|
||||
> setRegister r v = modify (\ uc -> UC (fromUC uc //[(r, v)]) (fpuState uc))
|
||||
|
||||
|
|
|
|||
|
|
@ -223,19 +223,30 @@ definition
|
|||
|
||||
section "User Monad"
|
||||
|
||||
type_synonym user_context = "register \<Rightarrow> machine_word"
|
||||
|
||||
text \<open> There are 576 bytes of FPU state. Since there are no operations on this state apart from bulk
|
||||
save/restore, we abstract from names and just say how many bytes there are. \<close>
|
||||
type_synonym fpu_bytes = 576
|
||||
type_synonym fpu_state = "fpu_bytes \<Rightarrow> 8 word"
|
||||
|
||||
type_synonym user_regs = "register \<Rightarrow> machine_word"
|
||||
|
||||
datatype user_context = UserContext (fpu_state : fpu_state) (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>uc. uc r)"
|
||||
"getRegister r \<equiv> gets (\<lambda>s. user_regs s r)"
|
||||
|
||||
definition
|
||||
"modify_registers f uc \<equiv> UserContext (fpu_state uc) (f (user_regs uc))"
|
||||
|
||||
definition
|
||||
setRegister :: "register \<Rightarrow> machine_word \<Rightarrow> unit user_monad"
|
||||
where
|
||||
"setRegister r v \<equiv> modify (\<lambda>uc. uc (r := v))"
|
||||
"setRegister r v \<equiv> modify (\<lambda>s. UserContext (fpu_state s) ((user_regs s) (r := v)))"
|
||||
|
||||
definition
|
||||
"getRestartPC \<equiv> getRegister FaultIP"
|
||||
|
|
@ -243,6 +254,18 @@ definition
|
|||
definition
|
||||
"setNextPC \<equiv> setRegister NextIP"
|
||||
|
||||
|
||||
definition
|
||||
getFPUState :: "fpu_state user_monad"
|
||||
where
|
||||
"getFPUState \<equiv> gets fpu_state"
|
||||
|
||||
definition
|
||||
setFPUState :: "fpu_state \<Rightarrow> unit user_monad"
|
||||
where
|
||||
"setFPUState fc \<equiv> modify (\<lambda>s. UserContext fc (user_regs s))"
|
||||
|
||||
|
||||
consts'
|
||||
initL2Cache_impl :: "unit machine_rest_monad"
|
||||
definition
|
||||
|
|
@ -437,8 +460,4 @@ where
|
|||
end
|
||||
|
||||
|
||||
translations
|
||||
(type) "'a X64.user_monad" <= (type) "(X64.register \<Rightarrow> X64.machine_word, 'a) nondet_monad"
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in New Issue