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