1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7(*
8Arch-specific functions for the abstract model of CSpace.
9*)
10
11chapter "ArchCSpace"
12
13theory ArchCSpace_A
14imports
15  ArchVSpace_A
16begin
17
18context Arch begin global_naming ARM_A
19
20definition cnode_guard_size_bits :: "nat"
21where
22  cnode_guard_size_bits_def [simp]: "cnode_guard_size_bits \<equiv> 5"
23
24definition cnode_padding_bits :: "nat"
25where
26  cnode_padding_bits_def [simp]: "cnode_padding_bits \<equiv> 3"
27
28text \<open>On a user request to modify a cnode capability, extract new guard bits and guard.\<close>
29definition
30  update_cnode_cap_data :: "data \<Rightarrow> nat \<times> data" where
31 "update_cnode_cap_data w \<equiv>
32    let
33      guard_bits = 18;
34      guard_size' = unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits);
35      guard'' = (w >> (cnode_padding_bits + cnode_guard_size_bits)) && mask guard_bits
36    in (guard_size', guard'')"
37
38text \<open>For some purposes capabilities to physical objects are treated
39differently to others.\<close>
40definition
41  arch_is_physical :: "arch_cap \<Rightarrow> bool" where
42  "arch_is_physical cap \<equiv> case cap of ASIDControlCap \<Rightarrow> False | _ \<Rightarrow> True"
43
44text \<open>Check whether the second capability is to the same object or an object
45contained in the region of the first one.\<close>
46fun
47  arch_same_region_as :: "arch_cap \<Rightarrow> arch_cap \<Rightarrow> bool"
48where
49  "arch_same_region_as (PageCap dev r R s x) (PageCap dev' r' R' s' x') =
50   (let
51     topA = r + (1 << pageBitsForSize s) - 1;
52     topB = r' + (1 << pageBitsForSize s') - 1
53   in r \<le> r' \<and> topA \<ge> topB \<and> r' \<le> topB)"
54| "arch_same_region_as (PageTableCap r x) (PageTableCap r' x') = (r' = r)"
55| "arch_same_region_as (PageDirectoryCap r x) (PageDirectoryCap r' x') = (r' = r)"
56| "arch_same_region_as ASIDControlCap ASIDControlCap = True"
57| "arch_same_region_as (ASIDPoolCap r a) (ASIDPoolCap r' a') = (r' = r)"
58| "arch_same_region_as _ _ = False"
59
60
61text \<open>Check whether two arch capabilities are to the same object.\<close>
62definition
63  same_aobject_as :: "arch_cap \<Rightarrow> arch_cap \<Rightarrow> bool" where
64 "same_aobject_as cp cp' \<equiv>
65   (case (cp, cp') of
66      (PageCap dev ref _ pgsz _,PageCap dev' ref' _ pgsz' _)
67          \<Rightarrow> (dev, ref, pgsz) = (dev', ref', pgsz')
68              \<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1
69    | _ \<Rightarrow> arch_same_region_as cp cp')"
70
71(* Proofs don't want to see this definition *)
72declare same_aobject_as_def[simp]
73
74definition
75  arch_is_cap_revocable :: "cap \<Rightarrow> cap \<Rightarrow> bool"
76where
77  "arch_is_cap_revocable c c' \<equiv> False"
78
79end
80end
81