1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(GD_GPL)
9 *)
10
11chapter "Intermediate"
12
13theory ArchIntermediate_H
14imports "../Intermediate_H"
15begin
16
17context Arch begin
18context begin
19
20private abbreviation (input)
21  "createNewPageCaps regionBase numObjects dev gSize pSize \<equiv>
22    let Data = (if dev then KOUserDataDevice else KOUserData) in
23    (do addrs \<leftarrow> createObjects regionBase numObjects Data gSize;
24        modify (\<lambda>ks. ks \<lparr> gsUserPages := (\<lambda> addr.
25          if addr `~elem~` map fromPPtr addrs then Just pSize
26          else gsUserPages ks addr)\<rparr>);
27        return $ map (\<lambda>n. PageCap (PPtr (fromPPtr n)) VMReadWrite VMNoMap pSize dev Nothing) addrs
28     od)"
29
30private abbreviation (input)
31  "createNewTableCaps regionBase numObjects tableBits objectProto cap initialiseMappings \<equiv> (do
32      tableSize \<leftarrow> return (tableBits - objBits objectProto);
33      addrs \<leftarrow> createObjects regionBase numObjects (injectKO objectProto) tableSize;
34      pts \<leftarrow> return (map (PPtr \<circ> fromPPtr) addrs);
35      initialiseMappings pts;
36      return $ map (\<lambda>pt. cap pt Nothing) pts
37    od)"
38
39defs Arch_createNewCaps_def:
40"Arch_createNewCaps t regionBase numObjects userSize dev \<equiv>
41    let pointerCast = PPtr \<circ> fromPPtr
42    in (case t of
43          APIObjectType apiObject \<Rightarrow> haskell_fail []
44        | SmallPageObject \<Rightarrow>
45            createNewPageCaps regionBase numObjects dev 0 X64SmallPage
46        | LargePageObject \<Rightarrow>
47            createNewPageCaps regionBase numObjects dev ptTranslationBits X64LargePage
48        | HugePageObject \<Rightarrow>
49            createNewPageCaps regionBase numObjects dev (ptTranslationBits + ptTranslationBits) X64HugePage
50        | PageTableObject \<Rightarrow>
51            createNewTableCaps regionBase numObjects ptBits (makeObject::pte) PageTableCap
52              (\<lambda>pts. return ())
53        | PageDirectoryObject \<Rightarrow>
54            createNewTableCaps regionBase numObjects pdBits (makeObject::pde) PageDirectoryCap
55              (\<lambda>pts. return ())
56        | PDPointerTableObject \<Rightarrow>
57            createNewTableCaps regionBase numObjects pdptBits (makeObject::pdpte) PDPointerTableCap
58              (\<lambda>pts. return ())
59        | PML4Object \<Rightarrow>
60            createNewTableCaps regionBase numObjects pml4Bits (makeObject::pml4e) PML4Cap
61              (\<lambda>pms. mapM_x copyGlobalMappings pms)
62        )"
63
64end
65end
66
67end
68