------------------------------------------------------------------------------ -- -- -- 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-2022, 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 -- -- . -- -- -- -- 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;