------------------------------------------------------------------------------ -- -- -- GNAT COMPILER COMPONENTS -- -- -- -- I N T E R F A C E S . C H E R I -- -- -- -- S p e c -- -- -- -- Copyright (C) 2023-2024, AdaCore -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- -- ware Foundation; either version 3, or (at your option) any later ver- -- -- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- -- or FITNESS FOR A PARTICULAR PURPOSE. -- -- -- -- As a special exception under Section 7 of GPL version 3, you are granted -- -- additional permissions described in the GCC Runtime Library Exception, -- -- version 3.1, as published by the Free Software Foundation. -- -- -- -- You should have received a copy of the GNU General Public License and -- -- a copy of the GCC Runtime Library Exception along with this program; -- -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- -- . -- -- -- -- GNAT was originally developed by the GNAT team at New York University. -- -- Extensive contributions were provided by Ada Core Technologies Inc. -- -- -- ------------------------------------------------------------------------------ -- This package provides bindings to CHERI intrinsics and some common -- operations on capabilities. with System; with System.Storage_Elements; package Interfaces.CHERI with Preelaborate, No_Elaboration_Code_All is use type System.Storage_Elements.Integer_Address; subtype Capability is System.Address; type Bounds_Length is range 0 .. System.Memory_Size - 1 with Size => System.Word_Size; ---------------------------- -- Capability Permissions -- ---------------------------- type Permissions_Mask is mod System.Memory_Size with Size => System.Word_Size; Global : constant Permissions_Mask := 16#0001#; Executive : constant Permissions_Mask := 16#0002#; Mutable_Load : constant Permissions_Mask := 16#0040#; Compartment_Id : constant Permissions_Mask := 16#0080#; Branch_Sealed_Pair : constant Permissions_Mask := 16#0100#; Access_System_Registers : constant Permissions_Mask := 16#0200#; Permit_Unseal : constant Permissions_Mask := 16#0400#; Permit_Seal : constant Permissions_Mask := 16#0800#; Permit_Store_Local : constant Permissions_Mask := 16#1000#; Permit_Store_Capability : constant Permissions_Mask := 16#2000#; Permit_Load_Capability : constant Permissions_Mask := 16#4000#; Permit_Execute : constant Permissions_Mask := 16#8000#; Permit_Store : constant Permissions_Mask := 16#1_0000#; Permit_Load : constant Permissions_Mask := 16#2_0000#; function "and" (Cap : Capability; Mask : Permissions_Mask) return Capability with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_perms_and"; -- Perform a bitwise-AND of a capability permissions and the specified -- mask, returning the new capability. function Get_Permissions (Cap : Capability) return Permissions_Mask with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_perms_get"; -- Get the permissions of a capability function Clear_Permissions (Cap : Capability; Mask : Permissions_Mask) return Capability is (Cap and not Mask); -- Clear the specified permissions of a capability, returning the new -- capability. function Has_All_Permissions (Cap : Capability; Permissions : Permissions_Mask) return Boolean is ((Get_Permissions (Cap) and Permissions) = Permissions); -- Query whether all of the specified permission bits are set in a -- capability's permissions flags. ----------------------- -- Common Intrinsics -- ----------------------- function Capability_With_Address (Cap : Capability; Addr : System.Storage_Elements.Integer_Address) return Capability with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_address_set"; -- Return a new capability with the same bounds and permissions as Cap, -- with the address set to Addr. function Get_Address (Cap : Capability) return System.Storage_Elements.Integer_Address with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_address_get"; -- Get the address of a capability procedure Set_Address (Cap : in out Capability; Addr : System.Storage_Elements.Integer_Address) with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_address_set"; -- Set the address of a capability function Get_Base (Cap : Capability) return System.Storage_Elements.Integer_Address with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_base_get"; -- Get the lower bound of a capability function Get_Offset (Cap : Capability) return Bounds_Length with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_offset_get"; -- Get the difference between the address and the lower bound of a -- capability. procedure Set_Offset (Cap : in out Capability; Offset : Bounds_Length) with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_offset_set"; -- Set the address relative to the lower bound of a capability function Capability_With_Offset (Cap : Capability; Value : Bounds_Length) return Capability with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_offset_set"; -- Set the address relative to the lower bound of a capability, returning -- the new capability. function Increment_Offset (Cap : Capability; Value : Bounds_Length) return Capability with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_offset_increment"; -- Increment the address of a capability by the specified amount, -- returning the new capability. function Get_Length (Cap : Capability) return Bounds_Length with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_length_get"; -- Get the length of a capability's bounds function Clear_Tag (Cap : Capability) return Capability with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_tag_clear"; -- Clear the capability validity tag, returning the new capability function Get_Tag (Cap : Capability) return Boolean with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_tag_get"; -- Get the validty tag of a capability function Is_Valid (Cap : Capability) return Boolean is (Get_Tag (Cap)); -- Check whether a capability is valid function Is_Invalid (Cap : Capability) return Boolean is (not Is_Valid (Cap)); -- Check whether a capability is invalid function Is_Equal_Exact (A, B : Capability) return Boolean with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_equal_exact"; -- Check for bit equality between two capabilities function Is_Subset (A, B : Capability) return Boolean with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_subset_test"; -- Returns True if capability A is a subset or equal to capability B -------------------- -- Bounds Setting -- -------------------- function Capability_With_Bounds (Cap : Capability; Length : Bounds_Length) return Capability with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_bounds_set"; -- Narrow the bounds of a capability so that the lower bound is the -- current address and the upper bound is suitable for the Length, -- returning the new capability. -- -- Note that the effective bounds of the returned capability may be wider -- than the range Get_Address (Cap) .. Get_Address (Cap) + Length - 1 due -- to capability compression, but they will always be a subset of the -- original bounds. function Capability_With_Exact_Bounds (Cap : Capability; Length : Bounds_Length) return Capability with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_bounds_set_exact"; -- Narrow the bounds of a capability so that the lower bound is the -- current address and the upper bound is suitable for the Length, -- returning the new capability. -- -- This is similar to Capability_With_Bounds but will clear the capability -- tag in the returned capability if the bounds cannot be set exactly, due -- to capability compression. function Capability_With_Address_And_Bounds (Cap : Capability; Address : System.Storage_Elements.Integer_Address; Length : Bounds_Length) return Capability is (Capability_With_Bounds (Capability_With_Address (Cap, Address), Length)); -- Set the address and narrow the bounds of the capability so that the -- lower bound is Address and the upper bound is Address + Length, -- returning the new capability. -- -- Note that the effective bounds of the returned capability may be wider -- than the range Address .. Address + Length - 1 due to capability -- compression, but they will always be a subset of the original bounds. function Capability_With_Address_And_Exact_Bounds (Cap : Capability; Address : System.Storage_Elements.Integer_Address; Length : Bounds_Length) return Capability is (Capability_With_Exact_Bounds (Capability_With_Address (Cap, Address), Length)); -- Set the address and narrow the bounds of the capability so that the -- lower bound is Address and the upper bound is Address + Length, -- returning the new capability. -- -- This is similar to Capability_With_Address_And_Bounds but will clear the -- capability tag in the returned capability if the bounds cannot be set -- exactly, due to capability compression. procedure Set_Bounds (Cap : in out Capability; Length : Bounds_Length) with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_bounds_set"; -- Narrow the bounds of a capability so that the lower bound is the -- current address and the upper bound is suitable for the Length. -- -- Note that the effective bounds of the output capability may be wider -- than the range Get_Address (Cap) .. Get_Address (Cap) + Length - 1 due -- to capability compression, but they will always be a subset of the -- original bounds. procedure Set_Exact_Bounds (Cap : in out Capability; Length : Bounds_Length) with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_bounds_set_exact"; -- Narrow the bounds of a capability so that the lower bound is the -- current address and the upper bound is suitable for the Length. -- -- This is similar to Set_Bounds but will clear the capability tag if the -- bounds cannot be set exactly, due to capability compression. procedure Set_Address_And_Bounds (Cap : in out Capability; Address : System.Storage_Elements.Integer_Address; Length : Bounds_Length) with Inline_Always; -- Set the address and narrow the bounds of the capability so that the -- lower bound is Address and the upper bound is Address + Length. -- -- Note that the effective bounds of the output capability may be wider -- than the range Address .. Address + Length - 1 due to capability -- compression, but they will always be a subset of the original bounds. procedure Set_Address_And_Exact_Bounds (Cap : in out Capability; Address : System.Storage_Elements.Integer_Address; Length : Bounds_Length) with Inline_Always; -- Set the address and narrow the bounds of the capability so that the -- lower bound is Address and the upper bound is Address + Length. -- -- This is similar to Set_Address_And_Bounds but will clear the capability -- tag if the bounds cannot be set exactly, due to capability compression. function Representable_Length (Length : Bounds_Length) return Bounds_Length with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_round_representable_length"; -- Returns the length that a capability would have after using Set_Bounds -- to set the Length (assuming appropriate alignment of the base). function Representable_Alignment_Mask (Length : Bounds_Length) return System.Storage_Elements.Integer_Address with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_representable_alignment_mask"; -- Returns a bitmask that can be used to align an address downwards such -- that it is sufficiently aligned to create a precisely bounded -- capability. function Align_Address_Down (Address : System.Storage_Elements.Integer_Address; Length : Bounds_Length) return System.Storage_Elements.Integer_Address is (Address and Representable_Alignment_Mask (Length)); -- Align an address such that it is sufficiently aligned to create a -- precisely bounded capability, rounding down if necessary. -- -- Due to capability compression, the upper and lower bounds of a -- capability must be aligned based on the length of the bounds to ensure -- that the capability is representable. This function aligns an address -- down to the next boundary if it is not already aligned. function Capability_With_Address_Aligned_Down (Cap : Capability; Length : Bounds_Length) return Capability is (Capability_With_Address (Cap, Align_Address_Down (Get_Address (Cap), Length))); -- Align a capability's address such that it is sufficiently aligned to -- create a precisely bounded capability, rounding down if necessary. -- -- Due to capability compression, the upper and lower bounds of a -- capability must be aligned based on the length of the bounds to ensure -- that the capability is representable. This function aligns an address -- down to the next boundary if it is not already aligned. function Align_Address_Up (Address : System.Storage_Elements.Integer_Address; Length : Bounds_Length) return System.Storage_Elements.Integer_Address with Inline; -- Align an address such that it is sufficiently aligned to create a -- precisely bounded capability, rounding upwards if necessary. -- -- Due to capability compression, the upper and lower bounds of a -- capability must be aligned based on the length of the bounds to ensure -- that the capability is representable. This function aligns an address up -- to the next boundary if it is not already aligned. function Capability_With_Address_Aligned_Up (Cap : Capability; Length : Bounds_Length) return Capability is (Capability_With_Address (Cap, Align_Address_Up (Get_Address (Cap), Length))); -- Align a capability's address such that it is sufficiently aligned to -- create a precisely bounded capability, rounding upwards if necessary. -- -- Due to capability compression, the upper and lower bounds of a -- capability must be aligned based on the length of the bounds to ensure -- that the capability is representable. This function aligns an address up -- to the next boundary if it is not already aligned. ------------------------------------------ -- Object Types, Sealing, and Unsealing -- ------------------------------------------ type Object_Type is range -2**(System.Word_Size - 1) .. +2**(System.Word_Size - 1) - 1 with Size => System.Word_Size; Type_Unsealed : constant Object_Type := 0; Type_Sentry : constant Object_Type := 1; function Get_Object_Type (Cap : Capability) return Object_Type with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_type_get"; -- Get the object type of a capability function Is_Sealed (Cap : Capability) return Boolean with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_sealed_get"; -- Check whether a capability is sealed function Is_Unsealed (Cap : Capability) return Boolean is (not Is_Sealed (Cap)); -- Check whether a capability is unsealed function Is_Sentry (Cap : Capability) return Boolean is (Get_Object_Type (Cap) = Type_Sentry); -- Check whether a capability is a sealed entry function Create_Sentry (Cap : Capability) return Capability with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_seal_entry"; -- Create a sealed entry and return the new capability. function Seal (Cap : Capability; Sealing_Cap : Capability) return Capability with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_seal"; -- Seal a capability with a sealing capability, by setting the object type -- of the capability to the Sealing_Cap's value, returning the sealed -- capability. function Unseal (Cap : Capability; Unsealing_Cap : Capability) return Capability with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_unseal"; -- Unseal a capability with an unsealing capability, by checking the object -- type of the capability against the Sealing_Cap's value, returning the -- unsealed capability. ----------------------------------- -- Capability Register Accessors -- ----------------------------------- function Get_PCC return System.Address with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_program_counter_get"; -- Get the Program Counter Capablity (PCC) function Get_DDC return System.Address with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_global_data_get"; -- Get the Default Data Capability (DDC) function Get_CSP return System.Address with Import, Convention => Intrinsic, External_Name => "__builtin_cheri_stack_get"; -- Get the Capability Stack Pointer (CSP) --------------------------- -- Capability Exceptions -- --------------------------- Capability_Bound_Error : exception; -- An out-of-bounds access was attempted Capability_Permission_Error : exception; -- An attempted access exceeded the permissions granted by a capability Capability_Sealed_Error : exception; -- A sealed capability was dereferenced Capability_Tag_Error : exception; -- An invalid capability was dereferenced end Interfaces.CHERI;