1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7(*
8Retyping and untyped invocation
9*)
10
11chapter "Retyping and Untyped Invocations"
12
13theory Retype_A
14imports
15  CSpaceAcc_A
16  ArchVSpaceAcc_A
17  Invocations_A
18  ArchRetype_A
19begin
20
21context begin interpretation Arch .
22
23requalify_consts
24  arch_default_cap
25  default_arch_object
26  init_arch_objects
27
28end
29
30
31section "Creating Caps"
32
33text \<open>The original capability created when an object of a given type is
34created with a particular address and size.\<close>
35primrec
36  default_cap :: "apiobject_type  \<Rightarrow> obj_ref \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> cap"
37where
38  "default_cap CapTableObject oref s _ = CNodeCap oref s []"
39| "default_cap Untyped oref s dev = UntypedCap dev oref s 0"
40| "default_cap TCBObject oref s _ = ThreadCap oref"
41| "default_cap EndpointObject oref s _ = EndpointCap oref 0 UNIV"
42| "default_cap NotificationObject oref s _ =
43     NotificationCap oref 0 {AllowRead, AllowWrite}"
44| "default_cap (ArchObject aobj) oref s dev = ArchObjectCap (arch_default_cap aobj oref s dev)"
45
46text \<open>Create and install a new capability to a newly created object.\<close>
47definition
48  create_cap ::
49  "apiobject_type \<Rightarrow> nat \<Rightarrow> cslot_ptr \<Rightarrow> bool \<Rightarrow> cslot_ptr \<times> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
50where
51  "create_cap type bits untyped is_device \<equiv> \<lambda>(dest,oref). do
52    dest_p \<leftarrow> gets (\<lambda>s. cdt s dest);
53    cdt \<leftarrow> gets cdt;
54    set_cdt (cdt (dest \<mapsto> untyped));
55    do_extended_op (create_cap_ext untyped dest dest_p);
56    set_original dest True;
57    set_cap (default_cap type oref bits is_device) dest
58   od"
59
60section "Creating Objects"
61
62text \<open>Properties of an empty CNode object.\<close>
63definition
64  empty_cnode :: "nat \<Rightarrow> cnode_contents" where
65  "empty_cnode bits \<equiv> \<lambda>x. if length x = bits then Some NullCap else None"
66
67
68text \<open>The initial state objects of various types are in when created.\<close>
69definition
70  default_object :: "apiobject_type \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> kernel_object" where
71  "default_object api dev n \<equiv> case api of
72           Untyped \<Rightarrow> undefined
73         | CapTableObject \<Rightarrow> CNode n (empty_cnode n)
74         | TCBObject \<Rightarrow> TCB default_tcb
75         | EndpointObject \<Rightarrow> Endpoint default_ep
76         | NotificationObject \<Rightarrow> Notification default_notification
77         | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev n)"
78
79text \<open>The size in bits of the objects that will be created when a given type
80and size is requested.\<close>
81definition
82  obj_bits_api :: "apiobject_type \<Rightarrow> nat \<Rightarrow> nat" where
83  "obj_bits_api type obj_size_bits \<equiv> case type of
84           Untyped \<Rightarrow> obj_size_bits
85         | CapTableObject \<Rightarrow> obj_size_bits + slot_bits
86         | TCBObject \<Rightarrow> obj_bits (TCB default_tcb)
87         | EndpointObject \<Rightarrow> obj_bits (Endpoint undefined)
88         | NotificationObject \<Rightarrow> obj_bits (Notification undefined)
89         | ArchObject aobj \<Rightarrow> obj_bits $ ArchObj $ default_arch_object aobj False obj_size_bits"
90
91section "Main Retype Implementation"
92
93text \<open>
94Create @{text "numObjects"} objects, starting from
95@{text obj_ref}, return of list pointers to them. For some types, each
96returned pointer points to a group of objects.
97\<close>
98
99definition
100  retype_region :: "obj_ref \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> apiobject_type \<Rightarrow> bool \<Rightarrow> (obj_ref list,'z::state_ext) s_monad"
101where
102  "retype_region ptr numObjects o_bits type dev \<equiv> do
103    obj_size \<leftarrow> return $ 2 ^ obj_bits_api type o_bits;
104    ptrs \<leftarrow> return $ map (\<lambda>p. ptr_add ptr (p * obj_size)) [0..< numObjects];
105    when (type \<noteq> Untyped) (do
106      kh \<leftarrow> gets kheap;
107      kh' \<leftarrow> return $ foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits)) ptrs kh;
108      do_extended_op (retype_region_ext ptrs type);
109      modify $ kheap_update (K kh')
110    od);
111    return $ ptrs
112  od"
113
114section "Invoking Untyped Capabilities"
115
116abbreviation (input) "extended_state_update \<equiv> trans_state"
117
118text \<open>Remove objects from a region of the heap.\<close>
119definition
120  detype :: "(obj_ref set) \<Rightarrow> 'z::state_ext state \<Rightarrow> 'z::state_ext state" where
121 "detype S s \<equiv> s \<lparr> kheap := (\<lambda>x. if x \<in> S then None else kheap s x), extended_state := detype_ext S (exst s)\<rparr>"
122
123text \<open>Delete objects within a specified region.\<close>
124definition
125  delete_objects :: "machine_word \<Rightarrow> nat \<Rightarrow> (unit,'z::state_ext) s_monad" where
126 "delete_objects ptr bits = do
127     do_machine_op (freeMemory ptr bits);
128     modify (detype {ptr..ptr + 2 ^ bits - 1})
129  od"
130
131(* FIXME: we need a sensible place for these configurable constants. *)
132definition
133  reset_chunk_bits :: nat where
134  "reset_chunk_bits = 8"
135
136definition
137  get_free_ref :: "obj_ref \<Rightarrow> nat \<Rightarrow> obj_ref" where
138  "get_free_ref base free_index \<equiv> base +  (of_nat free_index)"
139
140definition
141  get_free_index :: "obj_ref \<Rightarrow> obj_ref \<Rightarrow> nat" where
142  "get_free_index base free \<equiv> unat $ (free - base)"
143
144primrec(nonexhaustive) is_device_untyped_cap
145where
146  "is_device_untyped_cap (UntypedCap isdev _ _ _) = isdev"
147
148text \<open>Untyped capabilities note a currently free region. Sometimes this
149region is reset during a Retype operation. This progressively clears the
150underlying memory and also the object level representation, moving the free
151region pointer back to the start of the newly cleared region each time.\<close>
152definition
153  reset_untyped_cap :: "cslot_ptr \<Rightarrow> (unit,'z::state_ext) p_monad"
154where
155  "reset_untyped_cap src_slot = doE
156  cap \<leftarrow> liftE $ get_cap src_slot;
157  sz \<leftarrow> returnOk $ bits_of cap;
158  base \<leftarrow> returnOk $ obj_ref_of cap;
159  if free_index_of cap = 0
160    then returnOk ()
161  else doE
162    liftE $ delete_objects base sz;
163  dev \<leftarrow> returnOk $ is_device_untyped_cap cap;
164
165  if dev \<or> sz < reset_chunk_bits
166      then liftE $ do
167        unless dev $ do_machine_op $ clearMemory base (2 ^ sz);
168        set_cap (UntypedCap dev base sz 0) src_slot
169      od
170    else mapME_x (\<lambda>i. doE
171          liftE $ do_machine_op $ clearMemory (base + (of_nat i << reset_chunk_bits))
172              (2 ^ reset_chunk_bits);
173          liftE $ set_cap (UntypedCap dev base sz
174              (i * 2 ^ reset_chunk_bits)) src_slot;
175          preemption_point
176        odE) (rev [i \<leftarrow> [0 ..< 2 ^ (sz - reset_chunk_bits)].
177            i * 2 ^ reset_chunk_bits < free_index_of cap])
178    odE
179  odE"
180
181text \<open>Untyped capabilities confer authority to the Retype method. This
182clears existing objects from a region, creates new objects of the requested type,
183initialises them and installs new capabilities to them.\<close>
184definition
185  invoke_untyped :: "untyped_invocation \<Rightarrow> (unit,'z::state_ext) p_monad"
186where
187"invoke_untyped ui \<equiv> case ui
188    of Retype src_slot reset base retype_base new_type obj_sz slots is_device \<Rightarrow>
189doE
190  whenE reset $ reset_untyped_cap src_slot;
191  liftE $ do
192
193  cap \<leftarrow> get_cap src_slot;
194
195  \<comment> \<open>Update the untyped cap to track the amount of space used.\<close>
196  total_object_size \<leftarrow> return $ (of_nat (length slots) << (obj_bits_api new_type obj_sz));
197  free_ref \<leftarrow> return $ retype_base + total_object_size;
198  set_cap (UntypedCap is_device base (bits_of cap) (unat (free_ref - base))) src_slot;
199
200  \<comment> \<open>Create new objects.\<close>
201  orefs \<leftarrow> retype_region retype_base (length slots) obj_sz new_type is_device;
202  init_arch_objects new_type retype_base (length slots) obj_sz orefs;
203  sequence_x (map (create_cap new_type obj_sz src_slot is_device) (zip slots orefs))
204od odE"
205
206end
207