gcc/ada/libgnat/s-veboop.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                 GNAT RUN-TIME LIBRARY (GNARL) COMPONENTS                 --
   4 --                                                                          --
   5 --    S Y S T E M . V E C T O R S . B O O L E A N _ O P E R A T I O N S     --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 --          Copyright (C) 2002-2023, Free Software Foundation, Inc.         --
  10 --                                                                          --
  11 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
  12 -- terms of the  GNU General Public License as published  by the Free Soft- --
  13 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
  14 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
  15 -- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
  16 -- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
  17 --                                                                          --
  18 -- As a special exception under Section 7 of GPL version 3, you are granted --
  19 -- additional permissions described in the GCC Runtime Library Exception,   --
  20 -- version 3.1, as published by the Free Software Foundation.               --
  21 --                                                                          --
  22 -- You should have received a copy of the GNU General Public License and    --
  23 -- a copy of the GCC Runtime Library Exception along with this program;     --
  24 -- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
  25 -- <http://www.gnu.org/licenses/>.                                          --
  26 --                                                                          --
  27 -- GNAT was originally developed  by the GNAT team at  New York University. --
  28 -- Extensive contributions were provided by Ada Core Technologies Inc.      --
  29 --                                                                          --
  30 ------------------------------------------------------------------------------
  31
  32 --  This package contains functions for runtime operations on boolean vectors
  33
  34 --  Preconditions in this unit are meant for analysis only, not for run-time
  35 --  checking, so that the expected exceptions are raised. This is enforced by
  36 --  setting the corresponding assertion policy to Ignore. Postconditions and
  37 --  contract cases should not be executed at runtime as well, in order not to
  38 --  slow down the execution of these functions.
  39
  40 pragma Assertion_Policy (Pre            => Ignore,
  41                          Post           => Ignore,
  42                          Contract_Cases => Ignore,
  43                          Ghost          => Ignore);
  44
  45 package System.Vectors.Boolean_Operations
  46   with Pure, SPARK_Mode
  47 is
  48    pragma Warnings (Off, "aspect ""Pre"" not enforced on inlined subprogram",
  49                     Reason => "Pre only used in proof");
  50    pragma Warnings (Off, "aspect ""Post"" not enforced on inlined subprogram",
  51                     Reason => "Post only used in proof");
  52
  53    --  Type Vectors.Vector represents an array of Boolean, each of which
  54    --  takes 8 bits of the representation, with the 7 msb set to zero. Express
  55    --  in contracts the constraint on valid vectors and the model that they
  56    --  represent, and the relationship between input models and output model.
  57
  58    Vector_Boolean_Size : constant Positive :=
  59      System.Word_Size / System.Storage_Unit
  60    with Ghost;
  61
  62    type Vector_Element is mod 2 ** System.Storage_Unit with Ghost;
  63
  64    type Vector_Boolean_Array is array (1 .. Vector_Boolean_Size) of Boolean
  65    with Ghost;
  66
  67    function Shift_Right (V : Vectors.Vector; N : Natural) return Vectors.Vector
  68    with Ghost, Import, Convention => Intrinsic;
  69
  70    function Element (V : Vectors.Vector; N : Positive) return Vector_Element is
  71      (Vector_Element (Shift_Right (V, (N - 1) * System.Storage_Unit)
  72                         and (2 ** System.Storage_Unit - 1)))
  73    with
  74      Ghost,
  75      Pre => N <= Vector_Boolean_Size;
  76    --  Return the Nth element represented by the vector
  77
  78    function Valid (V : Vectors.Vector) return Boolean is
  79      (for all J in 1 .. Vector_Boolean_Size =>
  80         Element (V, J) in 0 .. 1)
  81    with Ghost;
  82    --  A valid vector is one for which all elements are 0 (representing False)
  83    --  or 1 (representing True).
  84
  85    function Model (V : Vectors.Vector) return Vector_Boolean_Array
  86    with
  87      Ghost,
  88      Pre => Valid (V);
  89
  90    function Model (V : Vectors.Vector) return Vector_Boolean_Array is
  91      (for J in 1 .. Vector_Boolean_Size => Element (V, J) = 1);
  92    --  The model of a valid vector is the corresponding array of Boolean values
  93
  94    --  Although in general the boolean operations on arrays of booleans are
  95    --  identical to operations on arrays of unsigned words of the same size,
  96    --  for the "not" operator this is not the case as False is typically
  97    --  represented by 0 and true by 1.
  98
  99    function "not" (Item : Vectors.Vector) return Vectors.Vector
 100    with
 101      Pre  => Valid (Item),
 102      Post => Valid ("not"'Result)
 103        and then (for all J in 1 .. Vector_Boolean_Size =>
 104                    Model ("not"'Result) (J) = not Model (Item) (J));
 105
 106    --  The three boolean operations "nand", "nor" and "nxor" are needed
 107    --  for cases where the compiler moves boolean array operations into
 108    --  the body of the loop that iterates over the array elements.
 109
 110    --  Note the following equivalences:
 111    --    (not X) or  (not Y)  =  not (X and Y)  =  Nand (X, Y)
 112    --    (not X) and (not Y)  =  not (X or Y)   =  Nor  (X, Y)
 113    --    (not X) xor (not Y)  =  X xor Y
 114    --    X       xor (not Y)  =  not (X xor Y)  =  Nxor (X, Y)
 115
 116    function Nand (Left, Right : Boolean) return Boolean
 117    with
 118      Post => Nand'Result = not (Left and Right);
 119
 120    function Nor  (Left, Right : Boolean) return Boolean
 121    with
 122      Post => Nor'Result = not (Left or Right);
 123
 124    function Nxor (Left, Right : Boolean) return Boolean
 125    with
 126      Post => Nxor'Result = not (Left xor Right);
 127
 128    function Nand (Left, Right : Vectors.Vector) return Vectors.Vector
 129    with
 130      Pre  => Valid (Left)
 131        and then Valid (Right),
 132      Post => Valid (Nand'Result)
 133        and then (for all J in 1 .. Vector_Boolean_Size =>
 134                    Model (Nand'Result) (J) =
 135                      Nand (Model (Left) (J), Model (Right) (J)));
 136
 137    function Nor (Left, Right : Vectors.Vector) return Vectors.Vector
 138    with
 139      Pre  => Valid (Left)
 140        and then Valid (Right),
 141      Post => Valid (Nor'Result)
 142        and then (for all J in 1 .. Vector_Boolean_Size =>
 143                    Model (Nor'Result) (J) =
 144                      Nor (Model (Left) (J), Model (Right) (J)));
 145
 146    function Nxor (Left, Right : Vectors.Vector) return Vectors.Vector
 147    with
 148      Pre  => Valid (Left)
 149        and then Valid (Right),
 150      Post => Valid (Nxor'Result)
 151        and then (for all J in 1 .. Vector_Boolean_Size =>
 152                    Model (Nxor'Result) (J) =
 153                      Nxor (Model (Left) (J), Model (Right) (J)));
 154
 155    pragma Inline_Always ("not");
 156    pragma Inline_Always (Nand);
 157    pragma Inline_Always (Nor);
 158    pragma Inline_Always (Nxor);
 159 end System.Vectors.Boolean_Operations;