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

arm-hyp execspec: pdates for VER-623 

with correct copy_global_mappings for ARM_HYP
This commit is contained in:
Miki Tanaka 2017-04-10 11:46:20 +10:00 committed by Alejandro Gomez-Londono
parent c32e6552e5
commit c079f39e3b
5 changed files with 21 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
spec/design/m-skel/ARM_HYP/MachineTypes.thy
View File

@ -27,10 +27,16 @@ section "Types"
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/ARM_HYP.lhs CONTEXT ARM_HYP decls_only
(*<*)
type_synonym machine_word_len = 32
end
context begin interpretation Arch .
requalify_types register
end
context Arch begin global_naming ARM_HYP
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/ARM_HYP.lhs CONTEXT ARM_HYP instanceproofs
@ -70,6 +76,7 @@ record
irq_masks :: "ARM_HYP.irq \<Rightarrow> bool"
irq_state :: nat
underlying_memory :: "word32 \<Rightarrow> word8"
device_state :: "word32 \<Rightarrow> word8 option"
exclusive_state :: ARM_HYP.exclusive_monitors
machine_state_rest :: ARM_HYP.machine_state_rest
@ -124,6 +131,7 @@ definition
"init_machine_state \<equiv> \<lparr> irq_masks = init_irq_masks,
irq_state = 0,
underlying_memory = init_underlying_memory,
device_state = empty,
exclusive_state = default_exclusive_state,
machine_state_rest = undefined \<rparr>"

2
spec/design/skel/ARM_HYP/ArchObjInsts_H.thy
View File

@ -126,6 +126,8 @@ lemmas (in Arch) [simp] =
-- --------------------------------------
#INCLUDE_SETTINGS keep_constructor = asidpool
#INCLUDE_HASKELL_PREPARSE SEL4/Object/Structures/ARM_HYP.lhs
#INCLUDE_HASKELL_PREPARSE SEL4/Machine/Hardware/ARM_HYP.lhs
#INCLUDE_HASKELL_PREPARSE SEL4/Object/VCPU/ARM_HYP.lhs

3
spec/design/skel/ARM_HYP/ArchStructures_H.thy
View File

@ -16,6 +16,9 @@ imports
begin
context Arch begin global_naming ARM_HYP_H
#INCLUDE_SETTINGS keep_constructor=asidpool
#INCLUDE_SETTINGS keep_constructor=arch_tcb
#INCLUDE_HASKELL SEL4/Object/Structures/ARM_HYP.lhs CONTEXT ARM_HYP_H decls_only
#INCLUDE_HASKELL SEL4/Object/Structures/ARM_HYP.lhs CONTEXT ARM_HYP_H instanceproofs
#INCLUDE_HASKELL SEL4/Object/Structures/ARM_HYP.lhs CONTEXT ARM_HYP_H bodies_only

2
spec/design/skel/ARM_HYP/ArchTCB_H.thy
View File

@ -15,7 +15,7 @@ context Arch begin global_naming ARM_HYP_H
#INCLUDE_HASKELL SEL4/Object/TCB/ARM_HYP.lhs CONTEXT ARM_HYP_H
#INCLUDE_HASKELL SEL4/Object/TCB.lhs Arch= ONLY archThreadGet archThreadSet asUser
#INCLUDE_HASKELL SEL4/Object/TCB.lhs Arch= ONLY archThreadGet archThreadSet
end

12
tools/haskell-translator/caseconvs
View File

@ -616,11 +616,6 @@ case \x of (0, vaddr:rightsMask:attr:_, (pdCap,_):_) -> (0, _, _) -> (1, rightsM
then ->6
else ->7
case \x of UntypedCap { capIsDevice = False } | capBlockSize untyped == objBits pool -> _ -> ---> let \v0\ = \x in
if isUntypedCap \v0\ \<and> capBlockSize \v0\ == objBits pool \<and> \<not> capIsDevice \v0\
then ->1
else ->2
case \x of (0, index:depth:_, (untyped,parentSlot):(root,_):_) -> (0, _, _) -> _ -> ---> let (\v0\, \v1\, \v2\) = \x in
if \v0\ = 0 then
if length \v1\ > 1 \<and> length \v2\ > 1
@ -1848,4 +1843,11 @@ case \x of cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}
then ->6
else undefined
case \x of UntypedCap { capIsDevice = False } | capBlockSize untyped == objBits pool -> _ -> ---> let \v0\ = \x in
if isUntypedCap \v0\ \<and> capBlockSize \v0\ == objBits pool \<and> \<not> capIsDevice \v0\
then ->1
else ->2
case \x of UntypedCap {capIsDevice = False} | capBlockSize untyped == objBits pool -> _ -> ---> if isUntypedCap \x \<and> (\<not> capIsDevice \x) \<and> (capBlockSize \x = objBits pool)
then ->1
else ->2