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 11theory PSpaceStorable_H 12imports 13 Structures_H 14 KernelStateData_H 15 "Lib.DataMap" 16begin 17 18context begin interpretation Arch . 19requalify_types 20 arch_kernel_object_type 21 22requalify_consts 23 archTypeOf 24end 25 26lemma UserData_singleton [simp]: 27 "(v = UserData) = True" "(UserData = v) = True" 28 by (cases v, simp)+ 29 30lemma UserDataDevice_singleton [simp]: 31 "(v = UserDataDevice) = True" "(UserDataDevice = v) = True" 32 by (cases v, simp)+ 33 34datatype 35 kernel_object_type = 36 EndpointT 37 | NotificationT 38 | CTET 39 | TCBT 40 | UserDataT 41 | UserDataDeviceT 42 | KernelDataT 43 | ArchT arch_kernel_object_type 44 45primrec 46 koTypeOf :: "kernel_object \<Rightarrow> kernel_object_type" 47where 48 "koTypeOf (KOEndpoint e) = EndpointT" 49| "koTypeOf (KONotification e) = NotificationT" 50| "koTypeOf (KOCTE e) = CTET" 51| "koTypeOf (KOTCB e) = TCBT" 52| "koTypeOf (KOUserData) = UserDataT" 53| "koTypeOf (KOUserDataDevice) = UserDataDeviceT" 54| "koTypeOf (KOKernelData) = KernelDataT" 55| "koTypeOf (KOArch e) = ArchT (archTypeOf e)" 56 57definition 58 typeError :: "unit list \<Rightarrow> kernel_object \<Rightarrow> 'a kernel" where 59 "typeError t1 t2 \<equiv> fail" 60 61definition 62 alignError :: "nat \<Rightarrow> 'a kernel" where 63 "alignError n \<equiv> fail" 64 65definition 66 alignCheck :: "machine_word \<Rightarrow> nat \<Rightarrow> unit kernel" where 67 "alignCheck x n \<equiv> unless ((x && mask n) = 0) $ alignError n" 68 69definition 70 magnitudeCheck :: "machine_word \<Rightarrow> machine_word option \<Rightarrow> nat \<Rightarrow> unit kernel" 71where 72 "magnitudeCheck x y n \<equiv> case y of None \<Rightarrow> return () 73 | Some z \<Rightarrow> when (z - x < 1 << n) fail" 74 75class pre_storable = 76 fixes injectKO :: "'a \<Rightarrow> kernel_object" 77 fixes projectKO_opt :: "kernel_object \<Rightarrow> 'a option" 78 fixes koType :: "'a itself \<Rightarrow> kernel_object_type" 79 80 assumes project_inject: "(projectKO_opt ko = Some v) = (injectKO v = ko)" 81 assumes project_koType: "(\<exists>v. projectKO_opt ko = Some (v::'a)) = (koTypeOf ko = koType TYPE('a))" 82begin 83 84definition 85 projectKO :: "kernel_object \<Rightarrow> 'a kernel" 86where 87 "projectKO e \<equiv> 88 case projectKO_opt e of None \<Rightarrow> fail | Some k \<Rightarrow> return k" 89 90definition 91 objBits :: "'a \<Rightarrow> nat" 92where 93 "objBits v \<equiv> objBitsKO (injectKO v)" 94 95definition 96 loadObject_default :: "machine_word \<Rightarrow> machine_word \<Rightarrow> machine_word option \<Rightarrow> kernel_object \<Rightarrow> 'a kernel" 97where 98 "loadObject_default ptr ptr' next obj \<equiv> do 99 assert (ptr = ptr'); 100 val \<leftarrow> projectKO obj; 101 alignCheck ptr (objBits val); 102 magnitudeCheck ptr next (objBits val); 103 return val 104 od" 105 106definition 107 updateObject_default :: "'a \<Rightarrow> kernel_object \<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow> machine_word option \<Rightarrow> kernel_object kernel" 108where 109 "updateObject_default val oldObj ptr ptr' next \<equiv> do 110 assert (ptr = ptr'); 111 (_ :: 'a) \<leftarrow> projectKO oldObj; 112 alignCheck ptr (objBits val); 113 magnitudeCheck ptr next (objBits val); 114 return (injectKO val) 115 od" 116 117end 118 119class pspace_storable = pre_storable + 120 fixes makeObject :: 'a 121 fixes loadObject :: "machine_word \<Rightarrow> machine_word \<Rightarrow> machine_word option \<Rightarrow> kernel_object \<Rightarrow> 'a kernel" 122 fixes updateObject :: "'a \<Rightarrow> kernel_object \<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow> 123 machine_word option \<Rightarrow> kernel_object kernel" 124 assumes updateObject_type: 125 "(ko', s') \<in> fst (updateObject v ko p p' p'' s) \<Longrightarrow> koTypeOf ko' = koTypeOf ko" 126 127end 128