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

aarch64 aspec/haskell: sync attribs_from_word 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2022-03-16 11:27:51 +11:00 committed by Gerwin Klein
parent 29518b9bb0
commit 89815424cf
2 changed files with 3 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
spec/abstract/AARCH64/ArchDecode_A.thy
View File

@ -61,9 +61,8 @@ definition arch_decode_irq_control_invocation ::
else throwError TruncatedMessage
else throwError IllegalOperation)"
definition attribs_from_word :: "machine_word \<Rightarrow> vm_attributes"
where
"attribs_from_word w \<equiv> if \<not> w!!0 then {Execute} else {}"
definition attribs_from_word :: "machine_word \<Rightarrow> vm_attributes" where
"attribs_from_word w \<equiv> {attr. \<not>w!!0 \<and> attr = Execute \<or> \<not>w !! 2 \<and> attr = Device}"
(* FIXME AARCH64: only half updated *)
definition make_user_pte :: "paddr \<Rightarrow> vm_attributes \<Rightarrow> vm_rights \<Rightarrow> pte" where

2
spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs
View File

@ -511,7 +511,7 @@ makeUserPTE baseAddr rights attrs vmSize =
pteSmallPage = vmSize == ARMSmallPage,
pteGlobal = False,
pteExecuteNever = armExecuteNever attrs,
pteDevice = armPageCacheable attrs,
pteDevice = not (armPageCacheable attrs),
pteRights = rights }
checkVPAlignment :: VMPageSize -> VPtr -> KernelF SyscallError ()