Initial upstream commit
The history contained unlicensed code so everything got squashed, sorry.
Change-Id: Ie1335ecfcee7f740bb6de2e9887606be30a2deff
Signed-off-by: Nico Huber <nico.huber@secunet.com>
diff --git a/common/Makefile.inc b/common/Makefile.inc
new file mode 100644
index 0000000..b8e4f35
--- /dev/null
+++ b/common/Makefile.inc
@@ -0,0 +1,10 @@
+hw-y += hw.ads
+hw-y += hw-mmio_range.ads
+hw-y += hw-mmio_regs.adb
+hw-y += hw-mmio_regs.ads
+hw-y += hw-port_io.adb
+hw-y += hw-port_io.ads
+hw-y += hw-sub_regs.ads
+hw-y += hw-time.ads
+hw-y += hw-time.adb
+hw-y += hw-time-timer.ads
diff --git a/common/hw-mmio_range.ads b/common/hw-mmio_range.ads
new file mode 100644
index 0000000..1b33630
--- /dev/null
+++ b/common/hw-mmio_range.ads
@@ -0,0 +1,35 @@
+--
+-- Copyright (C) 2015-2016 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- This program is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+-- GNU General Public License for more details.
+--
+
+with System;
+
+generic
+ Base_Addr : Word64;
+ type Element_T is mod <>;
+ type Index_T is range <>;
+ type Array_T is array (Index_T) of Element_T;
+package HW.MMIO_Range
+with
+ Abstract_State =>
+ ((State with External),
+ Base_Address),
+ Initializes => Base_Address
+is
+
+ procedure Read (Value : out Element_T; Index : in Index_T);
+
+ procedure Write (Index : in Index_T; Value : in Element_T);
+
+ procedure Set_Base_Address (Base : Word64);
+
+end HW.MMIO_Range;
diff --git a/common/hw-mmio_regs.adb b/common/hw-mmio_regs.adb
new file mode 100644
index 0000000..5eea563
--- /dev/null
+++ b/common/hw-mmio_regs.adb
@@ -0,0 +1,92 @@
+--
+-- Copyright (C) 2016 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- This program is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+-- GNU General Public License for more details.
+--
+
+package body HW.MMIO_Regs
+is
+
+ generic
+ type Word_T is mod <>;
+ procedure Read_G (Value : out Word_T; Idx : Subs_P.Index_T);
+
+ procedure Read_G (Value : out Word_T; Idx : Subs_P.Index_T)
+ is
+ Off : constant Range_P.Index_T := Range_P.Index_T
+ ((Byte_Offset + Regs (Idx).Byte_Offset) / (Range_P.Element_T'Size / 8));
+ pragma Warnings
+ (GNAT, Off, """Mask"" is not modified, could be declared constant",
+ Reason => "Ada RM forbids making it constant.");
+ Mask : Word64 := Shift_Left (1, Regs (Idx).MSB + 1 - Regs (Idx).LSB) - 1;
+ pragma Warnings
+ (GNAT, On, """Mask"" is not modified, could be declared constant");
+ Temp : Range_P.Element_T;
+ begin
+ Range_P.Read (Temp, Off);
+ Value := Word_T (Shift_Right (Word64 (Temp), Regs (Idx).LSB) and Mask);
+ end Read_G;
+
+ procedure Read_I is new Read_G (Word8);
+ procedure Read (Value : out Word8; Idx : Subs_P.Index_T) renames Read_I;
+
+ procedure Read_I is new Read_G (Word16);
+ procedure Read (Value : out Word16; Idx : Subs_P.Index_T) renames Read_I;
+
+ procedure Read_I is new Read_G (Word32);
+ procedure Read (Value : out Word32; Idx : Subs_P.Index_T) renames Read_I;
+
+ procedure Read_I is new Read_G (Word64);
+ procedure Read (Value : out Word64; Idx : Subs_P.Index_T) renames Read_I;
+
+ ----------------------------------------------------------------------------
+
+ generic
+ type Word_T is mod <>;
+ procedure Write_G (Idx : Subs_P.Index_T; Value : Word_T);
+
+ procedure Write_G (Idx : Subs_P.Index_T; Value : Word_T)
+ is
+ Off : constant Range_P.Index_T := Range_P.Index_T
+ ((Byte_Offset + Regs (Idx).Byte_Offset) / (Range_P.Element_T'Size / 8));
+ pragma Warnings
+ (GNAT, Off, """Mask"" is not modified, could be declared constant",
+ Reason => "Ada RM forbids making it constant.");
+ Mask : Word64 :=
+ Shift_Left (1, Regs (Idx).MSB + 1) - Shift_Left (1, Regs (Idx).LSB);
+ pragma Warnings
+ (GNAT, On, """Mask"" is not modified, could be declared constant");
+ Temp : Range_P.Element_T;
+ begin
+ if Regs (Idx).MSB - Regs (Idx).LSB + 1 = Range_P.Element_T'Size then
+ Range_P.Write (Off, Range_P.Element_T (Value));
+ else
+ -- read/modify/write
+ Range_P.Read (Temp, Off);
+ Temp := Range_P.Element_T
+ ((Word64 (Temp) and not Mask) or
+ (Shift_Left (Word64 (Value), Regs (Idx).LSB)));
+ Range_P.Write (Off, Temp);
+ end if;
+ end Write_G;
+
+ procedure Write_I is new Write_G (Word8);
+ procedure Write (Idx : Subs_P.Index_T; Value : Word8) renames Write_I;
+
+ procedure Write_I is new Write_G (Word16);
+ procedure Write (Idx : Subs_P.Index_T; Value : Word16) renames Write_I;
+
+ procedure Write_I is new Write_G (Word32);
+ procedure Write (Idx : Subs_P.Index_T; Value : Word32) renames Write_I;
+
+ procedure Write_I is new Write_G (Word64);
+ procedure Write (Idx : Subs_P.Index_T; Value : Word64) renames Write_I;
+
+end HW.MMIO_Regs;
diff --git a/common/hw-mmio_regs.ads b/common/hw-mmio_regs.ads
new file mode 100644
index 0000000..9aafed9
--- /dev/null
+++ b/common/hw-mmio_regs.ads
@@ -0,0 +1,127 @@
+--
+-- Copyright (C) 2016 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- This program is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+-- GNU General Public License for more details.
+--
+
+with HW.Sub_Regs;
+with HW.MMIO_Range;
+
+use type HW.Word64;
+
+generic
+ with package Range_P is new MMIO_Range (<>);
+ Byte_Offset_O : Natural := 0;
+
+ with package Subs_P is new Sub_Regs (<>);
+ Regs : Subs_P.Array_T;
+
+package HW.MMIO_Regs
+is
+
+ Byte_Offset : Natural := Byte_Offset_O;
+
+ ----------------------------------------------------------------------------
+
+ procedure Read (Value : out Word8; Idx : Subs_P.Index_T)
+ with
+ Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+ ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+ Range_P.Element_T'Size <= Word64'Size and
+ Regs (Idx).MSB < Range_P.Element_T'Size and
+ Regs (Idx).MSB >= Regs (Idx).LSB and
+ Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word8'Size;
+
+ procedure Read (Value : out Word16; Idx : Subs_P.Index_T)
+ with
+ Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+ ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+ Range_P.Element_T'Size <= Word64'Size and
+ Regs (Idx).MSB < Range_P.Element_T'Size and
+ Regs (Idx).MSB >= Regs (Idx).LSB and
+ Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word16'Size;
+
+ procedure Read (Value : out Word32; Idx : Subs_P.Index_T)
+ with
+ Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+ ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+ Range_P.Element_T'Size <= Word64'Size and
+ Regs (Idx).MSB < Range_P.Element_T'Size and
+ Regs (Idx).MSB >= Regs (Idx).LSB and
+ Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word32'Size;
+
+ procedure Read (Value : out Word64; Idx : Subs_P.Index_T)
+ with
+ Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+ ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+ Range_P.Element_T'Size <= Word64'Size and
+ Regs (Idx).MSB < Range_P.Element_T'Size and
+ Regs (Idx).MSB >= Regs (Idx).LSB and
+ Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word64'Size;
+
+ ----------------------------------------------------------------------------
+
+ procedure Write (Idx : Subs_P.Index_T; Value : Word8)
+ with
+ Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+ ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+ Range_P.Element_T'Size <= Word64'Size and
+ Regs (Idx).MSB < Range_P.Element_T'Size and
+ Regs (Idx).MSB >= Regs (Idx).LSB and
+ Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
+ Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
+
+ procedure Write (Idx : Subs_P.Index_T; Value : Word16)
+ with
+ Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+ ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+ Range_P.Element_T'Size <= Word64'Size and
+ Regs (Idx).MSB < Range_P.Element_T'Size and
+ Regs (Idx).MSB >= Regs (Idx).LSB and
+ Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
+ Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
+
+ procedure Write (Idx : Subs_P.Index_T; Value : Word32)
+ with
+ Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+ ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+ Range_P.Element_T'Size <= Word64'Size and
+ Regs (Idx).MSB < Range_P.Element_T'Size and
+ Regs (Idx).MSB >= Regs (Idx).LSB and
+ Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
+ Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
+
+ procedure Write (Idx : Subs_P.Index_T; Value : Word64)
+ with
+ Pre => ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+ ((Byte_Offset + Regs (Idx).Byte_Offset) /
+ (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+ Range_P.Element_T'Size <= Word64'Size and
+ Regs (Idx).MSB < Range_P.Element_T'Size and
+ Regs (Idx).MSB >= Regs (Idx).LSB and
+ Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
+ Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
+
+end HW.MMIO_Regs;
diff --git a/common/hw-port_io.adb b/common/hw-port_io.adb
new file mode 100644
index 0000000..e8adfc2
--- /dev/null
+++ b/common/hw-port_io.adb
@@ -0,0 +1,71 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- This program is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+-- GNU General Public License for more details.
+--
+
+with System;
+with System.Machine_Code;
+
+package body HW.Port_IO
+with
+ Refined_State => (State => null),
+ SPARK_Mode => Off
+is
+
+ generic
+ type Word is private;
+ procedure Port_In (Value : out Word; Port : Port_Type);
+
+ procedure Port_In (Value : out Word; Port : Port_Type) is
+ begin
+ System.Machine_Code.Asm
+ ("in %1, %0",
+ Inputs => (Port_Type'Asm_Input ("Nd", Port)),
+ Outputs => (Word'Asm_Output ("=a", Value)),
+ Volatile => True);
+ end Port_In;
+
+ procedure InB_Body is new Port_In (Word => Word8);
+ procedure InB (Value : out Word8; Port : Port_Type) renames InB_Body;
+
+ procedure InW_Body is new Port_In (Word => Word16);
+ procedure InW (Value : out Word16; Port : Port_Type) renames InW_Body;
+
+ procedure InL_Body is new Port_In (Word => Word32);
+ procedure InL (Value : out Word32; Port : Port_Type) renames InL_Body;
+
+ ----------------------------------------------------------------------------
+
+ generic
+ type Word is private;
+ procedure Port_Out (Port : Port_Type; Value : Word);
+
+ procedure Port_Out (Port : Port_Type; Value : Word) is
+ begin
+ System.Machine_Code.Asm
+ ("out %1, %0",
+ Inputs => (Port_Type'Asm_Input ("Nd", Port),
+ Word'Asm_Input ("a", Value)),
+ Volatile => True);
+ end Port_Out;
+
+ procedure OutB_Body is new Port_Out (Word => Word8);
+ procedure OutB (Port : Port_Type; Value : Word8) renames OutB_Body;
+
+ procedure OutW_Body is new Port_Out (Word => Word16);
+ procedure OutW (Port : Port_Type; Value : Word16) renames OutW_Body;
+
+ procedure OutL_Body is new Port_Out (Word => Word32);
+ procedure OutL (Port : Port_Type; Value : Word32) renames OutL_Body;
+
+end HW.Port_IO;
+
+-- vim: set ts=8 sts=3 sw=3 et:
diff --git a/common/hw-port_io.ads b/common/hw-port_io.ads
new file mode 100644
index 0000000..a5d0e9e
--- /dev/null
+++ b/common/hw-port_io.ads
@@ -0,0 +1,61 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- This program is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+-- GNU General Public License for more details.
+--
+
+package HW.Port_IO
+with
+ Abstract_State => (State with External => (Async_Readers, Async_Writers))
+is
+
+ type Port_Type is mod 2**16;
+
+ procedure InB (Value : out Word8; Port : Port_Type)
+ with
+ Global => (In_Out => State),
+ Depends => ((Value, State) => (Port, State)),
+ Inline_Always;
+
+ procedure InW (Value : out Word16; Port : Port_Type)
+ with
+ Global => (In_Out => State),
+ Depends => ((Value, State) => (Port, State)),
+ Pre => Port mod 2 = 0,
+ Inline_Always;
+
+ procedure InL (Value : out Word32; Port : Port_Type)
+ with
+ Global => (In_Out => State),
+ Depends => ((Value, State) => (Port, State)),
+ Pre => Port mod 4 = 0,
+ Inline_Always;
+
+ procedure OutB (Port : Port_Type; Value : Word8)
+ with
+ Global => (In_Out => State),
+ Depends => (State =>+ (Port, Value)),
+ Inline_Always;
+
+ procedure OutW (Port : Port_Type; Value : Word16)
+ with
+ Global => (In_Out => State),
+ Depends => (State =>+ (Port, Value)),
+ Pre => Port mod 2 = 0,
+ Inline_Always;
+
+ procedure OutL (Port : Port_Type; Value : Word32)
+ with
+ Global => (In_Out => State),
+ Depends => (State =>+ (Port, Value)),
+ Pre => Port mod 4 = 0,
+ Inline_Always;
+
+end HW.Port_IO;
diff --git a/common/hw-sub_regs.ads b/common/hw-sub_regs.ads
new file mode 100644
index 0000000..ca04c1d
--- /dev/null
+++ b/common/hw-sub_regs.ads
@@ -0,0 +1,26 @@
+--
+-- Copyright (C) 2016 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- This program is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+-- GNU General Public License for more details.
+--
+
+generic
+ type Index_T is (<>);
+package HW.Sub_Regs is
+
+ type T is record
+ Byte_Offset : Natural;
+ MSB : Natural;
+ LSB : Natural;
+ end record;
+
+ type Array_T is array (Index_T) of T;
+
+end HW.Sub_Regs;
diff --git a/common/hw-time-timer.ads b/common/hw-time-timer.ads
new file mode 100644
index 0000000..4676815
--- /dev/null
+++ b/common/hw-time-timer.ads
@@ -0,0 +1,41 @@
+--
+-- Copyright (C) 2015-2016 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- This program is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+-- GNU General Public License for more details.
+--
+
+private package HW.Time.Timer
+ with
+ Abstract_State => ((Timer_State with Part_Of => HW.Time.State),
+ (Abstract_Time with
+ Part_Of => HW.Time.State,
+ External => Async_Writers)),
+ Initializes => (Timer_State)
+is
+
+ -- Returns the highest point in time that has definitely passed.
+ function Raw_Value_Min return T
+ with
+ Volatile_Function,
+ Global => (Input => Abstract_Time),
+ Depends => (Raw_Value_Min'Result => Abstract_Time);
+
+ -- Returns the highest point in time that might have been reached yet.
+ function Raw_Value_Max return T
+ with
+ Volatile_Function,
+ Global => (Input => Abstract_Time),
+ Depends => (Raw_Value_Max'Result => Abstract_Time);
+
+ function Hz return T
+ with
+ Global => (Input => Timer_State);
+
+end HW.Time.Timer;
diff --git a/common/hw-time.adb b/common/hw-time.adb
new file mode 100644
index 0000000..3162de1
--- /dev/null
+++ b/common/hw-time.adb
@@ -0,0 +1,105 @@
+--
+-- Copyright (C) 2015-2016 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- This program is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+-- GNU General Public License for more details.
+--
+
+with HW;
+with HW.Time.Timer;
+
+use type HW.Word64;
+
+package body HW.Time
+ with Refined_State => (State => (Timer.Timer_State, Timer.Abstract_Time))
+is
+
+ function Now return T
+ with
+ Refined_Global => (Input => Timer.Abstract_Time)
+ is
+ Current : constant T := Timer.Raw_Value_Min;
+ begin
+ return Current;
+ end Now;
+
+ function US_From_Now (US : Natural) return T
+ with
+ Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+ is
+ Current : constant T := Timer.Raw_Value_Max;
+ begin
+ return Current + (T (US) * Timer.Hz + 999_999) / 1_000_000;
+ end US_From_Now;
+
+ function MS_From_Now (MS : Natural) return T
+ with
+ Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+ is
+ Current : constant T := Timer.Raw_Value_Max;
+ begin
+ return Current + (T (MS) * Timer.Hz + 999) / 1_000;
+ end MS_From_Now;
+
+ function Now_US return Int64
+ with
+ Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+ is
+ MHz : constant T := Timer.Hz / 1_000_000;
+ Current : constant T := Timer.Raw_Value_Min;
+ begin
+ return Int64 ((Current and (2 ** 63 - 1)) / (if MHz = 0 then 1 else MHz));
+ end Now_US;
+
+ ----------------------------------------------------------------------------
+
+ procedure Delay_Until (Deadline : T)
+ with
+ Refined_Global => (Input => (Timer.Abstract_Time))
+ is
+ Current: T;
+ begin
+ loop
+ Current := Timer.Raw_Value_Min;
+ exit when Current >= Deadline;
+ end loop;
+ end Delay_Until;
+
+ procedure U_Delay (US : Natural)
+ with
+ Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+ is
+ Deadline : constant T := US_From_Now (US);
+ begin
+ Delay_Until (Deadline);
+ end U_Delay;
+
+ procedure M_Delay (MS : Natural)
+ with
+ Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+ is
+ Deadline : constant T := MS_From_Now (MS);
+ begin
+ Delay_Until (Deadline);
+ end M_Delay;
+
+ ----------------------------------------------------------------------------
+
+ function Timed_Out (Deadline : T) return Boolean
+ with
+ Refined_Global => (Input => (Timer.Abstract_Time))
+ is
+ Current : constant T := Timer.Raw_Value_Min;
+ begin
+ return Current >= Deadline;
+ end Timed_Out;
+
+end HW.Time;
+
+-- vim: set ts=8 sts=3 sw=3 et:
diff --git a/common/hw-time.ads b/common/hw-time.ads
new file mode 100644
index 0000000..743279b
--- /dev/null
+++ b/common/hw-time.ads
@@ -0,0 +1,75 @@
+--
+-- Copyright (C) 2015-2016 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- This program is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+-- GNU General Public License for more details.
+--
+
+package HW.Time
+ with Abstract_State => (State with External => Async_Writers)
+is
+
+ type T is private;
+
+ function Now return T
+ with
+ Volatile_Function,
+ Global => (Input => State);
+
+ function US_From_Now (US : Natural) return T
+ with
+ Volatile_Function,
+ Global => (Input => State);
+
+ function MS_From_Now (MS : Natural) return T
+ with
+ Volatile_Function,
+ Global => (Input => State);
+
+ function Now_US return Int64
+ with
+ Volatile_Function,
+ Global => (Input => State);
+
+ ----------------------------------------------------------------------------
+
+ pragma Warnings
+ (GNATprove, Off, "subprogram ""*Delay*"" has no effect",
+ Reason => "No effect on dataflow but time always passes.");
+
+ -- Delay execution until Deadline has been reached.
+ procedure Delay_Until (Deadline : T)
+ with
+ Global => (Input => State);
+
+ procedure U_Delay (US : Natural)
+ with
+ Global => (Input => State);
+
+ procedure M_Delay (MS : Natural)
+ with
+ Global => (Input => State);
+
+ pragma Warnings
+ (GNATprove, On, "subprogram ""*Delay*"" has no effect");
+
+ ----------------------------------------------------------------------------
+
+ function Timed_Out (Deadline : T) return Boolean
+ with
+ Volatile_Function,
+ Global => (Input => State);
+
+private
+
+ type T is new Word64;
+
+end HW.Time;
+
+-- vim: set ts=8 sts=3 sw=3 et:
diff --git a/common/hw.ads b/common/hw.ads
new file mode 100644
index 0000000..6bfca91
--- /dev/null
+++ b/common/hw.ads
@@ -0,0 +1,58 @@
+--
+-- Copyright (C) 2015 secunet Security Networks AG
+--
+-- This program is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; version 2 of the License.
+--
+-- This program is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+-- GNU General Public License for more details.
+--
+
+with Interfaces;
+
+package HW is
+
+ type Bit is mod 2 ** 1;
+
+ subtype Byte is Interfaces.Unsigned_8;
+ subtype Word8 is Byte;
+ function Shift_Left (Value : Word8; Amount : Natural) return Word8
+ renames Interfaces.Shift_Left;
+ function Shift_Right (Value : Word8; Amount : Natural) return Word8
+ renames Interfaces.Shift_Right;
+
+ subtype Word16 is Interfaces.Unsigned_16;
+ function Shift_Left (Value : Word16; Amount : Natural) return Word16
+ renames Interfaces.Shift_Left;
+ function Shift_Right (Value : Word16; Amount : Natural) return Word16
+ renames Interfaces.Shift_Right;
+
+ subtype Word32 is Interfaces.Unsigned_32;
+ function Shift_Left (Value : Word32; Amount : Natural) return Word32
+ renames Interfaces.Shift_Left;
+ function Shift_Right (Value : Word32; Amount : Natural) return Word32
+ renames Interfaces.Shift_Right;
+
+ subtype Word64 is Interfaces.Unsigned_64;
+ function Shift_Left (Value : Word64; Amount : Natural) return Word64
+ renames Interfaces.Shift_Left;
+ function Shift_Right (Value : Word64; Amount : Natural) return Word64
+ renames Interfaces.Shift_Right;
+
+ subtype Int8 is Interfaces.Integer_8;
+ subtype Int16 is Interfaces.Integer_16;
+ subtype Int32 is Interfaces.Integer_32;
+ subtype Int64 is Interfaces.Integer_64;
+
+ subtype Pos8 is Interfaces.Integer_8 range 1 .. Interfaces.Integer_8'Last;
+ subtype Pos16 is Interfaces.Integer_16 range 1 .. Interfaces.Integer_16'Last;
+ subtype Pos32 is Interfaces.Integer_32 range 1 .. Interfaces.Integer_32'Last;
+ subtype Pos64 is Interfaces.Integer_64 range 1 .. Interfaces.Integer_64'Last;
+
+ subtype Buffer_Range is Natural range 0 .. Natural'Last - 1;
+ type Buffer is array (Buffer_Range range <>) of Byte;
+
+end HW;