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

aarch64 design: incomplete ArchIntermediate_H.thy skeleton 

Allows building ExecSpec, but is almost certainly wrong due to not
taking top-level pages into account.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski 2022-02-17 22:15:56 +11:00 committed by Gerwin Klein
parent 624ec70eb4
commit 9284d4305f
1 changed files with 14 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
spec/design/skel/AARCH64/ArchIntermediate_H.thy
View File

@ -1,14 +1,13 @@
(*
* Copyright 2014, General Dynamics C4 Systems
* Copyright 2022, Proofcraft Pty Ltd
*
* SPDX-License-Identifier: GPL-2.0-only
*)
chapter "Intermediate"
(* FIXME AARCH64: This file was copied *VERBATIM* from the RISCV64 version,
with minimal text substitution! Remove this comment after updating,
check copyright. *)
(* FIXME AARCH64: This file needs some thinking regarding handling of top-level tables. *)
theory ArchIntermediate_H
imports Intermediate_H
begin
@ -40,15 +39,23 @@ defs Arch_createNewCaps_def:
let pointerCast = PPtr \<circ> fromPPtr
in (case t of
APIObjectType apiObject \<Rightarrow> haskell_fail []
\<comment> \<open>FIXME AARCH64 TODO\<close>
| VSpaceRootObject \<Rightarrow> undefined
| SmallPageObject \<Rightarrow>
createNewFrameCaps regionBase numObjects dev 0 RISCVSmallPage
createNewFrameCaps regionBase numObjects dev 0 ARMSmallPage
| LargePageObject \<Rightarrow>
createNewFrameCaps regionBase numObjects dev ptTranslationBits RISCVLargePage
createNewFrameCaps regionBase numObjects dev (ptTranslationBits False) ARMLargePage
| HugePageObject \<Rightarrow>
createNewFrameCaps regionBase numObjects dev (ptTranslationBits + ptTranslationBits) RISCVHugePage
createNewFrameCaps regionBase numObjects dev (ptTranslationBits False + ptTranslationBits False) ARMHugePage
\<comment> \<open>FIXME AARCH64: does not take into account top-level pages and is almost certainly wrong\<close>
| PageTableObject \<Rightarrow>
createNewTableCaps regionBase numObjects ptBits (makeObject::pte) PageTableCap
createNewTableCaps regionBase numObjects (ptBits False) (makeObject::pte)
(\<lambda>base addr. PageTableCap base False addr)
(\<lambda>pts. return ())
| VCPUObject \<Rightarrow> (do
addrs \<leftarrow> createObjects regionBase numObjects (injectKO (makeObject :: vcpu)) 0;
return $ map (\<lambda> addr. VCPUCap addr) addrs
od)
)"
end