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