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 "Physical Memory Functions" 12 13theory PSpaceFuns_H 14imports 15 ObjectInstances_H 16 FaultMonad_H 17 "Lib.DataMap" 18begin 19 20context begin interpretation Arch . 21requalify_consts 22 fromPPtr 23 PPtr 24 freeMemory 25 storeWord 26 loadWord 27end 28 29definition deleteRange :: "( machine_word , 'a ) DataMap.map \<Rightarrow> machine_word \<Rightarrow> nat \<Rightarrow> ( machine_word , 'a ) DataMap.map" 30where "deleteRange m ptr bits \<equiv> 31 let inRange = (\<lambda> x. x && ((- mask bits) - 1) = fromPPtr ptr) in 32 data_map_filterWithKey (\<lambda> x _. Not (inRange x)) m" 33 34#INCLUDE_HASKELL SEL4/Model/PSpace.lhs decls_only Data.Map=DataMap NOT PSpace ptrBits ptrBitsForSize lookupAround maybeToMonad lookupAround2 typeError alignError alignCheck sizeCheck objBits deleteRange 35 36consts 37lookupAround2 :: "('k :: {linorder,finite}) \<Rightarrow> ( 'k , 'a ) DataMap.map \<Rightarrow> (('k * 'a) option * 'k option)" 38 39#INCLUDE_HASKELL SEL4/Model/PSpace.lhs bodies_only Data.Map=DataMap NOT PSpace ptrBits ptrBitsForSize lookupAround maybeToMonad typeError alignError alignCheck sizeCheck objBits deletionIsSafe cNodePartialOverlap pointerInUserData ksASIDMapSafe deleteRange 40 41end 42