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