-------------------------------------------------------------------------------
-- Copyright (c) 2019, Daniel King
-- All rights reserved.
--
-- Redistribution and use in source and binary forms, with or without
-- modification, are permitted provided that the following conditions are met:
-- * Redistributions of source code must retain the above copyright
-- notice, this list of conditions and the following disclaimer.
-- * Redistributions in binary form must reproduce the above copyright
-- notice, this list of conditions and the following disclaimer in the
-- documentation and/or other materials provided with the distribution.
-- * The name of the copyright holder may not be used to endorse or promote
-- Products derived from this software without specific prior written
-- permission.
--
-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
-- AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
-- IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
-- ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER BE LIABLE FOR ANY
-- DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
-- (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
-- LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
-- ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
-- (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
-- THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-------------------------------------------------------------------------------
with Ada.Unchecked_Conversion;
with Interfaces; use Interfaces;
-- @brief@
-- Type definitions and subprograms for AVX2 vector instructions.
package Keccak.Arch.AVX2
with SPARK_Mode => On
is
pragma Warnings (GNATprove, Off,
"pragma ""Machine_Attribute"" ignored (not yet supported)");
-------------------------
-- 4x 64-bit vectors --
-------------------------
package V4DI_Vectors
is
type V4DI_Index is range 0 .. 3;
type V4DI is array (V4DI_Index) of Unsigned_64
with Alignment => 32,
Size => 256,
Object_Size => 256;
pragma Machine_Attribute (V4DI, "vector_type");
pragma Machine_Attribute (V4DI, "may_alias");
type V4DI_View is array (V4DI_Index) of Unsigned_64
with Alignment => 32,
Size => 256,
Object_Size => 256;
function Load is new Ada.Unchecked_Conversion
(Source => V4DI_View,
Target => V4DI);
function Store is new Ada.Unchecked_Conversion
(Source => V4DI,
Target => V4DI_View);
function "and" (A, B : in V4DI) return V4DI
with Global => null;
pragma Import (Intrinsic, "and", "__builtin_ia32_andsi256");
function "xor" (A, B : in V4DI) return V4DI
with Global => null;
pragma Import (Intrinsic, "xor", "__builtin_ia32_pxor256");
function And_Not (A, B : in V4DI) return V4DI
with Global => null;
pragma Import (Intrinsic, And_Not, "__builtin_ia32_andnotsi256");
function Shift_Left (A : in V4DI;
Amount : in Natural) return V4DI
with Global => null;
pragma Import (Intrinsic, Shift_Left, "__builtin_ia32_psllqi256");
function Shift_Right (A : in V4DI;
Amount : in Natural) return V4DI
with Global => null;
pragma Import (Intrinsic, Shift_Right, "__builtin_ia32_psrlqi256");
function Rotate_Left (A : in V4DI;
Amount : in Natural) return V4DI
is (Shift_Left (A, Amount) xor Shift_Right (A, 64 - Amount))
with Inline,
Global => null,
Pre => Amount <= 64;
end V4DI_Vectors;
end Keccak.Arch.AVX2;