public inbox for gcc-patches@gcc.gnu.org
 help / color / mirror / Atom feed
From: "Marc Poulhiès" <poulhies@adacore.com>
To: gcc-patches@gcc.gnu.org
Cc: Daniel King <dmking@adacore.com>
Subject: [COMMITTED] ada: Add CHERI intrinsic bindings and helper functions.
Date: Tue, 20 Jun 2023 09:47:00 +0200	[thread overview]
Message-ID: <20230620074700.1252872-1-poulhies@adacore.com> (raw)

From: Daniel King <dmking@adacore.com>

The package Interfaces.CHERI provides intrinsic bindings and
helper functions to allow software to query, create, and
manipulate CHERI capabilities.

gcc/ada/

	* libgnat/i-cheri.ads: Add CHERI intrinsics and helper functions.
	* libgnat/i-cheri.adb: Likewise

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/libgnat/i-cheri.adb |  75 ++++++
 gcc/ada/libgnat/i-cheri.ads | 470 ++++++++++++++++++++++++++++++++++++
 2 files changed, 545 insertions(+)
 create mode 100644 gcc/ada/libgnat/i-cheri.adb
 create mode 100644 gcc/ada/libgnat/i-cheri.ads

diff --git a/gcc/ada/libgnat/i-cheri.adb b/gcc/ada/libgnat/i-cheri.adb
new file mode 100644
index 00000000000..174fdcc5b47
--- /dev/null
+++ b/gcc/ada/libgnat/i-cheri.adb
@@ -0,0 +1,75 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         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, 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    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+package body Interfaces.CHERI is
+
+   ----------------------------
+   -- Set_Address_And_Bounds --
+   ----------------------------
+
+   procedure Set_Address_And_Bounds
+     (Cap     : in out Capability;
+      Address :        System.Storage_Elements.Integer_Address;
+      Length  :        Bounds_Length)
+   is
+   begin
+      Cap := Capability_With_Address_And_Bounds (Cap, Address, Length);
+   end Set_Address_And_Bounds;
+
+   ----------------------------------
+   -- Set_Address_And_Exact_Bounds --
+   ----------------------------------
+
+   procedure Set_Address_And_Exact_Bounds
+     (Cap     : in out Capability;
+      Address :        System.Storage_Elements.Integer_Address;
+      Length  :        Bounds_Length)
+   is
+   begin
+      Cap := Capability_With_Address_And_Exact_Bounds (Cap, Address, Length);
+   end Set_Address_And_Exact_Bounds;
+
+   ----------------------
+   -- Align_Address_Up --
+   ----------------------
+
+   function Align_Address_Up
+     (Address : System.Storage_Elements.Integer_Address;
+      Length  : Bounds_Length)
+      return System.Storage_Elements.Integer_Address
+   is
+      Mask : constant System.Storage_Elements.Integer_Address :=
+        Representable_Alignment_Mask (Length);
+   begin
+      return (Address + (not Mask)) and Mask;
+   end Align_Address_Up;
+
+end Interfaces.CHERI;
diff --git a/gcc/ada/libgnat/i-cheri.ads b/gcc/ada/libgnat/i-cheri.ads
new file mode 100644
index 00000000000..547b033dbaf
--- /dev/null
+++ b/gcc/ada/libgnat/i-cheri.ads
@@ -0,0 +1,470 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         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, 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    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+-- 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)
+
+end Interfaces.CHERI;
-- 
2.40.0


             reply	other threads:[~2023-06-20  7:47 UTC|newest]

Thread overview: 5+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2023-06-20  7:47 Marc Poulhiès [this message]
2023-06-20 13:00 ` Alex Coplan
2023-06-20 13:47   ` Marc Poulhiès
2023-06-20 20:21     ` Alex Coplan
2023-06-22  8:18       ` Marc Poulhiès

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20230620074700.1252872-1-poulhies@adacore.com \
    --to=poulhies@adacore.com \
    --cc=dmking@adacore.com \
    --cc=gcc-patches@gcc.gnu.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).