| ------------------------------------------------------------------------------ |
| -- -- |
| -- GNAT RUN-TIME LIBRARY (GNARL) COMPONENTS -- |
| -- -- |
| -- 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 -- |
| -- -- |
| -- S p e c -- |
| -- -- |
| -- Copyright (C) 2002-2023, Free Software Foundation, Inc. -- |
| -- -- |
| -- 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 contains functions for runtime operations on boolean vectors |
| |
| -- Preconditions in this unit are meant for analysis only, not for run-time |
| -- checking, so that the expected exceptions are raised. This is enforced by |
| -- setting the corresponding assertion policy to Ignore. Postconditions and |
| -- contract cases should not be executed at runtime as well, in order not to |
| -- slow down the execution of these functions. |
| |
| pragma Assertion_Policy (Pre => Ignore, |
| Post => Ignore, |
| Contract_Cases => Ignore, |
| Ghost => Ignore); |
| |
| package System.Vectors.Boolean_Operations |
| with Pure, SPARK_Mode |
| is |
| pragma Warnings (Off, "aspect ""Pre"" not enforced on inlined subprogram", |
| Reason => "Pre only used in proof"); |
| pragma Warnings (Off, "aspect ""Post"" not enforced on inlined subprogram", |
| Reason => "Post only used in proof"); |
| |
| -- Type Vectors.Vector represents an array of Boolean, each of which |
| -- takes 8 bits of the representation, with the 7 msb set to zero. Express |
| -- in contracts the constraint on valid vectors and the model that they |
| -- represent, and the relationship between input models and output model. |
| |
| Vector_Boolean_Size : constant Positive := |
| System.Word_Size / System.Storage_Unit |
| with Ghost; |
| |
| type Vector_Element is mod 2 ** System.Storage_Unit with Ghost; |
| |
| type Vector_Boolean_Array is array (1 .. Vector_Boolean_Size) of Boolean |
| with Ghost; |
| |
| function Shift_Right (V : Vectors.Vector; N : Natural) return Vectors.Vector |
| with Ghost, Import, Convention => Intrinsic; |
| |
| function Element (V : Vectors.Vector; N : Positive) return Vector_Element is |
| (Vector_Element (Shift_Right (V, (N - 1) * System.Storage_Unit) |
| and (2 ** System.Storage_Unit - 1))) |
| with |
| Ghost, |
| Pre => N <= Vector_Boolean_Size; |
| -- Return the Nth element represented by the vector |
| |
| function Valid (V : Vectors.Vector) return Boolean is |
| (for all J in 1 .. Vector_Boolean_Size => |
| Element (V, J) in 0 .. 1) |
| with Ghost; |
| -- A valid vector is one for which all elements are 0 (representing False) |
| -- or 1 (representing True). |
| |
| function Model (V : Vectors.Vector) return Vector_Boolean_Array |
| with |
| Ghost, |
| Pre => Valid (V); |
| |
| function Model (V : Vectors.Vector) return Vector_Boolean_Array is |
| (for J in 1 .. Vector_Boolean_Size => Element (V, J) = 1); |
| -- The model of a valid vector is the corresponding array of Boolean values |
| |
| -- Although in general the boolean operations on arrays of booleans are |
| -- identical to operations on arrays of unsigned words of the same size, |
| -- for the "not" operator this is not the case as False is typically |
| -- represented by 0 and true by 1. |
| |
| function "not" (Item : Vectors.Vector) return Vectors.Vector |
| with |
| Pre => Valid (Item), |
| Post => Valid ("not"'Result) |
| and then (for all J in 1 .. Vector_Boolean_Size => |
| Model ("not"'Result) (J) = not Model (Item) (J)); |
| |
| -- The three boolean operations "nand", "nor" and "nxor" are needed |
| -- for cases where the compiler moves boolean array operations into |
| -- the body of the loop that iterates over the array elements. |
| |
| -- Note the following equivalences: |
| -- (not X) or (not Y) = not (X and Y) = Nand (X, Y) |
| -- (not X) and (not Y) = not (X or Y) = Nor (X, Y) |
| -- (not X) xor (not Y) = X xor Y |
| -- X xor (not Y) = not (X xor Y) = Nxor (X, Y) |
| |
| function Nand (Left, Right : Boolean) return Boolean |
| with |
| Post => Nand'Result = not (Left and Right); |
| |
| function Nor (Left, Right : Boolean) return Boolean |
| with |
| Post => Nor'Result = not (Left or Right); |
| |
| function Nxor (Left, Right : Boolean) return Boolean |
| with |
| Post => Nxor'Result = not (Left xor Right); |
| |
| function Nand (Left, Right : Vectors.Vector) return Vectors.Vector |
| with |
| Pre => Valid (Left) |
| and then Valid (Right), |
| Post => Valid (Nand'Result) |
| and then (for all J in 1 .. Vector_Boolean_Size => |
| Model (Nand'Result) (J) = |
| Nand (Model (Left) (J), Model (Right) (J))); |
| |
| function Nor (Left, Right : Vectors.Vector) return Vectors.Vector |
| with |
| Pre => Valid (Left) |
| and then Valid (Right), |
| Post => Valid (Nor'Result) |
| and then (for all J in 1 .. Vector_Boolean_Size => |
| Model (Nor'Result) (J) = |
| Nor (Model (Left) (J), Model (Right) (J))); |
| |
| function Nxor (Left, Right : Vectors.Vector) return Vectors.Vector |
| with |
| Pre => Valid (Left) |
| and then Valid (Right), |
| Post => Valid (Nxor'Result) |
| and then (for all J in 1 .. Vector_Boolean_Size => |
| Model (Nxor'Result) (J) = |
| Nxor (Model (Left) (J), Model (Right) (J))); |
| |
| pragma Inline_Always ("not"); |
| pragma Inline_Always (Nand); |
| pragma Inline_Always (Nor); |
| pragma Inline_Always (Nxor); |
| end System.Vectors.Boolean_Operations; |
