[coreboot-gerrit] Patch set updated for coreboot: WIP: SPARK: Add building blocks for HW access
Nico Huber (nico.h@gmx.de)
gerrit at coreboot.org
Thu Jun 16 06:14:55 CEST 2016
Nico Huber (nico.h at gmx.de) just uploaded a new patch set to gerrit, which you can find at https://review.coreboot.org/11867
-gerrit
commit 22e8fbfe0c580742f8d467939aeb96dd50f48cc2
Author: Nico Huber <nico.huber at secunet.com>
Date: Sun Oct 11 14:40:01 2015 +0200
WIP: SPARK: Add building blocks for HW access
Some basic support for i/o access, debugging, timers. Just what I put
around our code, to make it build stand-alone. Very open for discussion.
Currently the Kconfig option WITH_SPARK_HW has to be selected to include
it into a build. It's integrated to be build for ramstage only. We'll
see to it if we need it somewhere else.
Change-Id: I8c4bb90c3e925af7c19f35c8aa6aafe844f42e1f
Signed-off-by: Nico Huber <nico.huber at secunet.com>
---
src/Kconfig | 31 +++
src/cpu/x86/tsc/Makefile.inc | 2 +
src/cpu/x86/tsc/hw-time-timer.adb | 56 +++++
src/lib/Makefile.inc | 10 +
src/lib/ada/hw-mmio_range.adb | 47 ++++
src/lib/debug/Makefile.inc | 27 +++
src/lib/debug/cb_console/ada/hw-debug_sink.adb | 59 +++++
src/lib/debug/cb_console/ada/hw-debug_sink.ads | 24 +++
src/lib/debug/hw-debug.adb | 284 +++++++++++++++++++++++++
src/lib/debug/hw-debug.ads | 44 ++++
src/lib/debug/null/hw-debug_sink.ads | 24 +++
src/lib/debug/text_io/ada/hw-debug_sink.ads | 25 +++
src/lib/hw-mmio_range.ads | 41 ++++
src/lib/hw-port_io.adb | 73 +++++++
src/lib/hw-port_io.ads | 63 ++++++
src/lib/hw-time.adb | 136 ++++++++++++
src/lib/hw-time.ads | 66 ++++++
src/lib/hw.ads | 58 +++++
src/lib/proof/hw-mmio_range.adb | 46 ++++
src/lib/timer/Makefile.inc | 15 ++
src/lib/timer/hw-time-timer.ads | 39 ++++
src/lib/timer/null/hw-time-timer.adb | 37 ++++
22 files changed, 1207 insertions(+)
diff --git a/src/Kconfig b/src/Kconfig
index 7f13b62..6c87a6a 100644
--- a/src/Kconfig
+++ b/src/Kconfig
@@ -1073,6 +1073,14 @@ config DEBUG_COVERAGE
If enabled, the code coverage hooks in coreboot will output some
information about the coverage data that is dumped.
+config DEBUG_SPARK
+ bool "Debug SPARK code"
+ depends on WITH_SPARK_HW
+ default n
+ help
+ Enable debugging of SPARK code. The debug code won't be proved
+ currently.
+
endmenu
# These probably belong somewhere else, but they are needed somewhere.
@@ -1157,3 +1165,26 @@ config CBFS_SIZE
This is the part of the ROM actually managed by CBFS. Set it to be
equal to the full rom size if that hasn't been overridden by the
chipset or mainboard.
+
+config WITH_SPARK_HW
+ bool
+ default n
+ help
+ Internal option that activates build of SPARK code. Disabled by default
+ to save build time. If we come to the point where we build it for the
+ majority of boards we might just drop it.
+
+config HAVE_SPARK_PORT_IO
+ bool
+ depends on WITH_SPARK_HW && (ARCH_RAMSTAGE_X86_32 || ARCH_RAMSTAGE_X86_64)
+ default y
+
+config SPARK_TIMER_INTEL_TSC
+ bool
+ depends on WITH_SPARK_HW && TSC_CONSTANT_RATE
+ default y
+
+config SPARK_TIMER_NULL
+ bool
+ depends on WITH_SPARK_HW && !SPARK_TIMER_INTEL_TSC
+ default y
diff --git a/src/cpu/x86/tsc/Makefile.inc b/src/cpu/x86/tsc/Makefile.inc
index bbebda9..fd081dc 100644
--- a/src/cpu/x86/tsc/Makefile.inc
+++ b/src/cpu/x86/tsc/Makefile.inc
@@ -4,3 +4,5 @@ verstage-$(CONFIG_TSC_CONSTANT_RATE) += delay_tsc.c
ifeq ($(CONFIG_HAVE_SMI_HANDLER),y)
smm-$(CONFIG_TSC_CONSTANT_RATE) += delay_tsc.c
endif
+
+ramstage-$(CONFIG_SPARK_TIMER_INTEL_TSC) += hw-time-timer.adb
diff --git a/src/cpu/x86/tsc/hw-time-timer.adb b/src/cpu/x86/tsc/hw-time-timer.adb
new file mode 100644
index 0000000..d8ded4c
--- /dev/null
+++ b/src/cpu/x86/tsc/hw-time-timer.adb
@@ -0,0 +1,56 @@
+--
+-- This file is part of the coreboot project.
+--
+-- 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.Machine_Code;
+with Interfaces.C;
+
+use type Interfaces.C.unsigned_long;
+
+package body HW.Time.Timer
+ with Refined_State => (Timer_State => Cached_Hz,
+ Abstract_Time => null)
+is
+
+ Cached_Hz : T;
+
+ function TSC_Freq_MHz return Interfaces.C.unsigned_long;
+ pragma Import (C, TSC_Freq_MHz, "tsc_freq_mhz");
+
+ procedure Raw_Value (Value : out T)
+ with
+ SPARK_Mode => Off
+ is
+ TSC_Low, TSC_High : Word32;
+ begin
+ System.Machine_Code.Asm
+ (Template => "rdtsc",
+ Outputs => (Word32'Asm_Output ("=d", TSC_High),
+ Word32'Asm_Output ("=a", TSC_Low)),
+ Volatile => True);
+ Value := Shift_Left (T (TSC_High), 32) or T (TSC_Low);
+ end Raw_Value;
+
+ function Hz return T
+ with
+ Refined_Global => (Input => Cached_Hz)
+ is
+ begin
+ return Cached_Hz;
+ end Hz;
+
+begin
+ pragma SPARK_Mode (Off);
+ Cached_Hz := T (TSC_Freq_MHz) * 1_000_000;
+end HW.Time.Timer;
diff --git a/src/lib/Makefile.inc b/src/lib/Makefile.inc
index fa65f7c..c4c31f6 100644
--- a/src/lib/Makefile.inc
+++ b/src/lib/Makefile.inc
@@ -14,8 +14,18 @@
#
subdirs-y += loaders
subdirs-y += gnat
+subdirs-y += debug
+subdirs-y += timer
+ramstage-$(CONFIG_WITH_SPARK_HW) += hw.ads
+ramstage-$(CONFIG_WITH_SPARK_HW) += hw-mmio_range.ads
+ramstage-$(CONFIG_WITH_SPARK_HW) += ada/hw-mmio_range.adb
+ramstage-$(CONFIG_WITH_SPARK_HW) += hw-time.adb
+ramstage-$(CONFIG_WITH_SPARK_HW) += hw-time.ads
+ramstage-$(CONFIG_HAVE_SPARK_PORT_IO) += hw-port_io.adb
+ramstage-$(CONFIG_HAVE_SPARK_PORT_IO) += hw-port_io.ads
+
ifneq ($(CONFIG_BOOTBLOCK_CUSTOM),y)
bootblock-y += bootblock.c
endif
diff --git a/src/lib/ada/hw-mmio_range.adb b/src/lib/ada/hw-mmio_range.adb
new file mode 100644
index 0000000..75bb53e
--- /dev/null
+++ b/src/lib/ada/hw-mmio_range.adb
@@ -0,0 +1,47 @@
+--
+-- This file is part of the coreboot project.
+--
+-- 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.Address_To_Access_Conversions;
+
+package body HW.MMIO_Range
+with
+ Refined_State =>
+ (State => Range_A, -- the contents accessed
+ Base_Address => null) -- the address, so actually Range_A too
+is
+ pragma Warnings (Off, "implicit dereference",
+ Reason => "This is what this package is about.");
+
+ type Range_Access is access all Range_T;
+ package Conv_Range is new System.Address_To_Access_Conversions (Range_T);
+
+ Range_A : Range_Access with Volatile;
+
+ procedure Read (Value : out Element_T; Index : in Index_T) is
+ begin
+ Value := Range_A (Index);
+ end Read;
+
+ procedure Write (Index : in Index_T; Value: in Element_T) is
+ begin
+ Range_A (Index) := Value;
+ end Write;
+
+ procedure Set_Base_Address (Base : System.Address) is
+ begin
+ Range_A := Range_Access (Conv_Range.To_Pointer (Base));
+ end Set_Base_Address;
+
+end HW.MMIO_Range;
diff --git a/src/lib/debug/Makefile.inc b/src/lib/debug/Makefile.inc
new file mode 100644
index 0000000..00348f4
--- /dev/null
+++ b/src/lib/debug/Makefile.inc
@@ -0,0 +1,27 @@
+##
+## This file is part of the coreboot project.
+##
+## 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.
+##
+
+ramstage-y += hw-debug.adb
+
+ifeq ($(CONFIG_DEBUG_SPARK),y)
+
+ramstage-y += cb_console/ada/hw-debug_sink.adb
+ramstage-y += cb_console/ada/hw-debug_sink.ads
+
+else
+
+ramstage-y += null/hw-debug_sink.ads
+
+endif
diff --git a/src/lib/debug/cb_console/ada/hw-debug_sink.adb b/src/lib/debug/cb_console/ada/hw-debug_sink.adb
new file mode 100644
index 0000000..9d4ee4c
--- /dev/null
+++ b/src/lib/debug/cb_console/ada/hw-debug_sink.adb
@@ -0,0 +1,59 @@
+--
+-- This file is part of the coreboot project.
+--
+-- 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.C;
+
+use type Interfaces.C.int;
+
+package body HW.Debug_Sink is
+
+ Sink_Enabled : Boolean;
+
+ procedure console_tx_byte (chr : Interfaces.C.char);
+ pragma Import (C, console_tx_byte, "console_tx_byte");
+
+ procedure Put (Item : String) is
+ begin
+ if Sink_Enabled then
+ for Idx in Item'Range loop
+ console_tx_byte (Interfaces.C.To_C (Item (Idx)));
+ end loop;
+ end if;
+ end Put;
+
+ procedure Put_Char (Item : Character) is
+ begin
+ if Sink_Enabled then
+ console_tx_byte (Interfaces.C.To_C (Item));
+ end if;
+ end Put_Char;
+
+ procedure New_Line is
+ begin
+ Put_Char (Character'Val (16#0a#));
+ end New_Line;
+
+ ----------------------------------------------------------------------------
+
+ function console_log_level
+ (msg_level : Interfaces.C.int)
+ return Interfaces.C.int;
+ pragma Import (C, console_log_level, "console_log_level");
+
+ Msg_Level_BIOS_DEBUG : constant := 7;
+
+begin
+ Sink_Enabled := console_log_level (Msg_Level_BIOS_DEBUG) /= 0;
+end HW.Debug_Sink;
diff --git a/src/lib/debug/cb_console/ada/hw-debug_sink.ads b/src/lib/debug/cb_console/ada/hw-debug_sink.ads
new file mode 100644
index 0000000..322249e
--- /dev/null
+++ b/src/lib/debug/cb_console/ada/hw-debug_sink.ads
@@ -0,0 +1,24 @@
+--
+-- This file is part of the coreboot project.
+--
+-- 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.Debug_Sink is
+
+ procedure Put (Item : String);
+
+ procedure Put_Char (Item : Character);
+
+ procedure New_Line;
+
+end HW.Debug_Sink;
diff --git a/src/lib/debug/hw-debug.adb b/src/lib/debug/hw-debug.adb
new file mode 100644
index 0000000..2d18524
--- /dev/null
+++ b/src/lib/debug/hw-debug.adb
@@ -0,0 +1,284 @@
+--
+-- This file is part of the coreboot project.
+--
+-- 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 HW;
+with HW.Time;
+with HW.Debug_Sink;
+
+use type HW.Word64;
+use type HW.Int64;
+
+package body HW.Debug is
+ pragma SPARK_Mode (Off);
+
+ Start_Of_Line : Boolean := True;
+ Register_Write_Delay_Nanoseconds : Word64 := 0;
+
+ type Base_Range is new Positive range 2 .. 16;
+ type Width_Range is new Natural range 0 .. 64;
+
+ procedure Put_By_Base
+ (Item : Word64;
+ Min_Width : Width_Range;
+ Base : Base_Range);
+
+ procedure Do_Put_Int64
+ (Item : Int64);
+
+ ----------------------------------------------------------------------------
+
+ procedure Put_Time
+ is
+ Now_US : Int64;
+ begin
+ if Start_Of_Line then
+ Start_Of_Line := False;
+ Time.Now_US (Now_US);
+ Debug_Sink.Put_Char ('[');
+ Do_Put_Int64 (Now_US / 1_000_000);
+ Debug_Sink.Put_Char ('.');
+ Put_By_Base (Word64 (Now_US mod 1_000_000), 6, 10);
+ Debug_Sink.Put ("] ");
+ end if;
+ end Put_Time;
+
+ ----------------------------------------------------------------------------
+
+ procedure Put (Item : String) is
+ begin
+ Put_Time;
+ HW.Debug_Sink.Put (Item);
+ end Put;
+
+ procedure Put_Line (Item : String) is
+ begin
+ Put (Item);
+ New_Line;
+ end Put_Line;
+
+ procedure New_Line is
+ begin
+ HW.Debug_Sink.New_Line;
+ Start_Of_Line := True;
+ end New_Line;
+
+ ----------------------------------------------------------------------------
+
+ procedure Put_By_Base
+ (Item : Word64;
+ Min_Width : Width_Range;
+ Base : Base_Range)
+ is
+ Temp : Word64 := Item;
+
+ subtype Chars_Range is Width_Range range 0 .. 63;
+ Index : Width_Range := 0;
+
+ type Chars_Array is array (Chars_Range) of Character;
+ Chars : Chars_Array := (others => '0');
+
+ Digit : Natural;
+ begin
+ while Temp > 0 loop
+ Digit := Natural (Temp rem Word64 (Base));
+ if Digit < 10 then
+ Chars (Index) := Character'Val (Character'Pos ('0') + Digit);
+ else
+ Chars (Index) := Character'Val (Character'Pos ('a') + Digit - 10);
+ end if;
+ Temp := Temp / Word64 (Base);
+ Index := Index + 1;
+ end loop;
+ if Index < Min_Width then
+ Index := Min_Width;
+ end if;
+ for I in reverse Width_Range range 0 .. Index - 1 loop
+ HW.Debug_Sink.Put_Char (Chars (I));
+ end loop;
+ end Put_By_Base;
+
+ ----------------------------------------------------------------------------
+
+ procedure Put_Word
+ (Item : Word64;
+ Min_Width : Width_Range;
+ Print_Ox : Boolean := True) is
+ begin
+ Put_Time;
+ if Print_Ox then
+ Put ("0x");
+ end if;
+ Put_By_Base (Item, Min_Width, 16);
+ end Put_Word;
+
+ procedure Put_Word8 (Item : Word8) is
+ begin
+ Put_Word (Word64 (Item), 2);
+ end Put_Word8;
+
+ procedure Put_Word16 (Item : Word16) is
+ begin
+ Put_Word (Word64 (Item), 4);
+ end Put_Word16;
+
+ procedure Put_Word32 (Item : Word32) is
+ begin
+ Put_Word (Word64 (Item), 8);
+ end Put_Word32;
+
+ procedure Put_Word64 (Item : Word64) is
+ begin
+ Put_Word (Item, 16);
+ end Put_Word64;
+
+ ----------------------------------------------------------------------------
+
+ procedure Do_Put_Int64 (Item : Int64)
+ is
+ Temp : Word64;
+ begin
+ if Item < 0 then
+ Debug_Sink.Put_Char ('-');
+ Temp := Word64 (-Item);
+ else
+ Temp := Word64 (Item);
+ end if;
+ Put_By_Base (Temp, 1, 10);
+ end Do_Put_Int64;
+
+ procedure Put_Int64 (Item : Int64)
+ is
+ begin
+ Put_Time;
+ Do_Put_Int64 (Item);
+ end Put_Int64;
+
+ procedure Put_Int8 (Item : Int8) is
+ begin
+ Put_Int64 (Int64 (Item));
+ end Put_Int8;
+
+ procedure Put_Int16 (Item : Int16) is
+ begin
+ Put_Int64 (Int64 (Item));
+ end Put_Int16;
+
+ procedure Put_Int32 (Item : Int32) is
+ begin
+ Put_Int64 (Int64 (Item));
+ end Put_Int32;
+
+ ----------------------------------------------------------------------------
+
+ procedure Put_Reg8 (Name : String; Item : Word8) is
+ begin
+ Put (Name);
+ Put (": ");
+ Put_Word8 (Item);
+ New_Line;
+ end Put_Reg8;
+
+ procedure Put_Reg16 (Name : String; Item : Word16)
+ is
+ begin
+ Put (Name);
+ Put (": ");
+ Put_Word16 (Item);
+ New_Line;
+ end Put_Reg16;
+
+ procedure Put_Reg32 (Name : String; Item : Word32)
+ is
+ begin
+ Put (Name);
+ Put (": ");
+ Put_Word32 (Item);
+ New_Line;
+ end Put_Reg32;
+
+ procedure Put_Reg64 (Name : String; Item : Word64)
+ is
+ begin
+ Put (Name);
+ Put (": ");
+ Put_Word64 (Item);
+ New_Line;
+ end Put_Reg64;
+
+ ----------------------------------------------------------------------------
+
+ procedure Put_Buffer
+ (Name : String;
+ Buf : Buffer;
+ Len : Buffer_Range)
+ is
+ Line_Start, Left : Natural;
+ begin
+ if Len = 0 then
+ if Name'Length > 0 then
+ Put (Name);
+ Put_Line ("+0x00:");
+ end if;
+ else
+ Line_Start := 0;
+ Left := Len - 1;
+ for I in Natural range 1 .. ((Len + 15) / 16) loop
+ if Name'Length > 0 then
+ Put (Name);
+ Debug_Sink.Put_Char ('+');
+ Put_Word16 (Word16 (Line_Start));
+ Put (": ");
+ end if;
+ for J in Natural range 0 .. Natural'Min (7, Left)
+ loop
+ Put_Word (Word64 (Buf (Line_Start + J)), 2, False);
+ Debug_Sink.Put_Char (' ');
+ end loop;
+
+ Debug_Sink.Put_Char (' ');
+ for J in Natural range 8 .. Natural'Min (15, Left)
+ loop
+ Put_Word (Word64(Buf (Line_Start + J)), 2, False);
+ Debug_Sink.Put_Char (' ');
+ end loop;
+ New_Line;
+
+ Line_Start := Line_Start + 16;
+ Left := Left - Natural'Min (Left, 16);
+ end loop;
+ end if;
+ end Put_Buffer;
+
+ ----------------------------------------------------------------------------
+
+ procedure Set_Register_Write_Delay (Value : Word64)
+ is
+ begin
+ Register_Write_Delay_Nanoseconds := Value;
+ end Set_Register_Write_Delay;
+
+ ----------------------------------------------------------------------------
+
+ Procedure Register_Write_Wait
+ is
+ begin
+ if Register_Write_Delay_Nanoseconds > 0 then
+ Time.U_Delay (Natural ((Register_Write_Delay_Nanoseconds + 999) / 1000));
+ end if;
+ end Register_Write_Wait;
+
+end HW.Debug;
+
+-- vim: set ts=8 sts=3 sw=3 et:
diff --git a/src/lib/debug/hw-debug.ads b/src/lib/debug/hw-debug.ads
new file mode 100644
index 0000000..83309e6
--- /dev/null
+++ b/src/lib/debug/hw-debug.ads
@@ -0,0 +1,44 @@
+--
+-- This file is part of the coreboot project.
+--
+-- 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.Debug is
+
+ procedure Put (Item : String);
+ procedure Put_Line (Item : String);
+ procedure New_Line;
+
+ procedure Put_Word8 (Item : Word8);
+ procedure Put_Word16 (Item : Word16);
+ procedure Put_Word32 (Item : Word32);
+ procedure Put_Word64 (Item : Word64);
+
+ procedure Put_Int8 (Item : Int8);
+ procedure Put_Int16 (Item : Int16);
+ procedure Put_Int32 (Item : Int32);
+ procedure Put_Int64 (Item : Int64);
+
+ procedure Put_Reg8 (Name : String; Item : Word8);
+ procedure Put_Reg16 (Name : String; Item : Word16);
+ procedure Put_Reg32 (Name : String; Item : Word32);
+ procedure Put_Reg64 (Name : String; Item : Word64);
+
+ procedure Put_Buffer (Name : String; Buf : in Buffer; Len : in Buffer_Range);
+
+ procedure Set_Register_Write_Delay (Value : Word64);
+ Procedure Register_Write_Wait;
+end HW.Debug;
+
+-- vim: set ts=8 sts=3 sw=3 et:
diff --git a/src/lib/debug/null/hw-debug_sink.ads b/src/lib/debug/null/hw-debug_sink.ads
new file mode 100644
index 0000000..fc84ff6
--- /dev/null
+++ b/src/lib/debug/null/hw-debug_sink.ads
@@ -0,0 +1,24 @@
+--
+-- This file is part of the coreboot project.
+--
+-- 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.Debug_Sink is
+
+ procedure Put (Item : String) is null;
+
+ procedure Put_Char (Item : Character) is null;
+
+ procedure New_Line is null;
+
+end HW.Debug_Sink;
diff --git a/src/lib/debug/text_io/ada/hw-debug_sink.ads b/src/lib/debug/text_io/ada/hw-debug_sink.ads
new file mode 100644
index 0000000..590ad1c
--- /dev/null
+++ b/src/lib/debug/text_io/ada/hw-debug_sink.ads
@@ -0,0 +1,25 @@
+--
+-- This file is part of the coreboot project.
+--
+-- 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 Ada.Text_IO;
+
+package HW.Debug_Sink is
+
+ procedure Put (Item : String) renames Ada.Text_IO.Put;
+ procedure Put_Char (Item : Character) renames Ada.Text_IO.Put;
+ procedure New_Line (Spacing : Ada.Text_IO.Positive_Count := 1)
+ renames Ada.Text_IO.New_Line;
+
+end HW.Debug_Sink;
diff --git a/src/lib/hw-mmio_range.ads b/src/lib/hw-mmio_range.ads
new file mode 100644
index 0000000..579b27d
--- /dev/null
+++ b/src/lib/hw-mmio_range.ads
@@ -0,0 +1,41 @@
+--
+-- This file is part of the coreboot project.
+--
+-- 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;
+
+generic
+ type Element_T is private;
+ type Index_T is (<>);
+ type Range_T is array (Index_T) of Element_T;
+package HW.MMIO_Range
+with
+ Abstract_State =>
+ ((State with External),
+ Base_Address)
+is
+
+ procedure Read (Value : out Element_T; Index : in Index_T)
+ with
+ Global => (In_Out => State);
+
+ procedure Write (Index : in Index_T; Value: in Element_T)
+ with
+ Global => (In_Out => State);
+
+ procedure Set_Base_Address (Base : System.Address)
+ with
+ Global => (Output => Base_Address);
+
+end HW.MMIO_Range;
diff --git a/src/lib/hw-port_io.adb b/src/lib/hw-port_io.adb
new file mode 100644
index 0000000..52777e2
--- /dev/null
+++ b/src/lib/hw-port_io.adb
@@ -0,0 +1,73 @@
+--
+-- This file is part of the coreboot project.
+--
+-- 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/src/lib/hw-port_io.ads b/src/lib/hw-port_io.ads
new file mode 100644
index 0000000..d5dbc10
--- /dev/null
+++ b/src/lib/hw-port_io.ads
@@ -0,0 +1,63 @@
+--
+-- This file is part of the coreboot project.
+--
+-- 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/src/lib/hw-time.adb b/src/lib/hw-time.adb
new file mode 100644
index 0000000..88408f6
--- /dev/null
+++ b/src/lib/hw-time.adb
@@ -0,0 +1,136 @@
+--
+-- This file is part of the coreboot project.
+--
+-- 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 HW;
+with HW.Time.Timer;
+
+use type HW.Word64;
+
+package body HW.Time
+ with Refined_State => (State => (Timer.Timer_State, Timer.Abstract_Time))
+is
+
+ procedure Now_US (US : out Int64)
+ is
+ Current, MHz : T;
+ begin
+ MHz := Timer.Hz / 1_000_000;
+ if MHz < 2 then
+ MHz := 2;
+ end if;
+
+ Timer.Raw_Value (Current);
+ US := Int64 (Current / MHz);
+ end Now_US;
+
+ pragma Warnings
+ (GNATprove, Off,
+ """Timer.Abstract_Time"" constituent of ""Time.State"" is not modified, could be INPUT",
+ Reason => "Time passes by itself");
+ procedure Delay_Until (Deadline : T)
+ with
+ Refined_Global => (In_Out => Timer.Abstract_Time),
+ Refined_Depends => (Timer.Abstract_Time => Timer.Abstract_Time,
+ null => Deadline)
+ is
+ Current : T;
+ begin
+ pragma Warnings (GNATprove, Off, "statement has no effect",
+ Reason => "It effects passing of time");
+ pragma Warnings (GNATprove, Off, "unused assignment to ""Current""",
+ Reason => "Um, well, first, it's not unused?");
+ loop
+ Timer.Raw_Value (Current);
+ exit when Current > Deadline;
+ end loop;
+ pragma Warnings (GNATprove, On, "statement has no effect");
+ pragma Warnings (GNATprove, On, "unused assignment to ""Current""");
+ end Delay_Until;
+ pragma Warnings
+ (GNATprove, On,
+ """Timer.Abstract_Time"" constituent of ""Time.State"" is not modified, could be INPUT");
+
+ procedure U_Delay (US : Natural) is
+ Timeout : T;
+ begin
+ New_Timeout_US (US, Timeout);
+ Delay_Until (Timeout);
+ end U_Delay;
+
+ procedure M_Delay (MS : Natural) is
+ Timeout : T;
+ begin
+ New_Timeout_MS (MS, Timeout);
+ Delay_Until (Timeout);
+ end M_Delay;
+
+ procedure New_Timeout_US (US : Natural; Timeout : out T)
+ is
+ Current : T;
+ begin
+ Timer.Raw_Value (Current);
+ Timeout := Current + (T (US) * Timer.Hz + 999_999) / 1_000_000;
+ end New_Timeout_US;
+
+ procedure New_Timeout_MS (MS : Natural; Timeout : out T)
+ is
+ Current : T;
+ begin
+ Timer.Raw_Value (Current);
+ Timeout := Current + (T (MS) * Timer.Hz + 999) / 1_000;
+ end New_Timeout_MS;
+
+ procedure Timed_Out (Deadline : T; T_Out : out Boolean)
+ with
+ Refined_Global => (Input => Timer.Abstract_Time),
+ Refined_Depends => (T_Out => (Deadline, Timer.Abstract_Time))
+ is
+ Current : T;
+ begin
+ Timer.Raw_Value (Current);
+ T_Out := Current >= Deadline;
+ end Timed_Out;
+
+ procedure Timeout_Delay (Deadline, Delay_End : T; T_Out : out Boolean) is
+ begin
+ Timed_Out (Deadline, T_Out);
+ if not T_Out then
+ if Deadline < Delay_End then
+ Delay_Until (Deadline);
+ else
+ Delay_Until (Delay_End);
+ end if;
+ end if;
+ end Timeout_Delay;
+
+ procedure Timeout_U_Delay (Deadline : T; US : Natural; T_Out : out Boolean)
+ is
+ Timeout : T;
+ begin
+ New_Timeout_US (US, Timeout);
+ Timeout_Delay (Deadline, Timeout, T_Out);
+ end Timeout_U_Delay;
+
+ procedure Timeout_M_Delay (Deadline : T; MS : Natural; T_Out : out Boolean)
+ is
+ Timeout : T;
+ begin
+ New_Timeout_MS (MS, Timeout);
+ Timeout_Delay (Deadline, Timeout, T_Out);
+ end Timeout_M_Delay;
+
+end HW.Time;
+
+-- vim: set ts=8 sts=3 sw=3 et:
diff --git a/src/lib/hw-time.ads b/src/lib/hw-time.ads
new file mode 100644
index 0000000..444e181
--- /dev/null
+++ b/src/lib/hw-time.ads
@@ -0,0 +1,66 @@
+--
+-- This file is part of the coreboot project.
+--
+-- 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.Time
+ with Abstract_State => (State with External => Async_Writers)
+is
+
+ type T is private;
+
+ procedure Now_US (US : out Int64);
+ -- avoid volatile functions until attribute is generally available
+
+ -- Delay execution until Deadline has been reached.
+ procedure Delay_Until (Deadline : T)
+ with
+ Global => (In_Out => State),
+ Depends => (State => State,
+ null => Deadline);
+
+ procedure U_Delay (US : Natural);
+
+ procedure M_Delay (MS : Natural);
+
+ procedure New_Timeout_US (US : Natural; Timeout : out T);
+ -- avoid volatile functions until attribute is generally available
+
+ procedure New_Timeout_MS (MS : Natural; Timeout : out T);
+ -- avoid volatile functions until attribute is generally available
+
+ -- procedure as workaround until Volatile_Function works
+ procedure Timed_Out (Deadline : T; T_Out : out Boolean)
+ with
+ Global => (Input => State),
+ Depends => (T_Out => (Deadline, State));
+ --function Timed_Out (Deadline : T) return Boolean
+ -- with
+ -- Volatile_Function,
+ -- Global => (Input => State);
+
+ -- Delay execution for given number of Microseconds but stop if Deadline
+ -- has been reached. Set T_Out if Dealine had already expired.
+ procedure Timeout_U_Delay (Deadline : T; US : Natural; T_Out : out Boolean);
+
+ -- Delay execution for given number of Milliseconds but stop if Deadline
+ -- has been reached. Set T_Out if Dealine had already expired.
+ procedure Timeout_M_Delay (Deadline : T; MS : Natural; T_Out : out Boolean);
+
+private
+
+ type T is new Word64;
+
+end HW.Time;
+
+-- vim: set ts=8 sts=3 sw=3 et:
diff --git a/src/lib/hw.ads b/src/lib/hw.ads
new file mode 100644
index 0000000..f26dbf4
--- /dev/null
+++ b/src/lib/hw.ads
@@ -0,0 +1,58 @@
+--
+-- This file is part of the coreboot project.
+--
+-- 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
+
+ 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;
diff --git a/src/lib/proof/hw-mmio_range.adb b/src/lib/proof/hw-mmio_range.adb
new file mode 100644
index 0000000..2336138
--- /dev/null
+++ b/src/lib/proof/hw-mmio_range.adb
@@ -0,0 +1,46 @@
+--
+-- This file is part of the coreboot project.
+--
+-- 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 body HW.MMIO_Range
+with
+ Refined_State =>
+ (State => Range_A,
+ Base_Address => Address)
+is
+
+ Range_A : Range_T
+ with
+ Volatile,
+ Async_Readers, Async_Writers, Effective_Reads, Effective_Writes,
+ Import;
+
+ Address : System.Address;
+
+ procedure Read (Value : out Element_T; Index : in Index_T) is
+ begin
+ Value := Range_A (Index);
+ end Read;
+
+ procedure Write (Index : in Index_T; Value: in Element_T) is
+ begin
+ Range_A (Index) := Value;
+ end Write;
+
+ procedure Set_Base_Address (Base : System.Address) is
+ begin
+ Address := Base;
+ end Set_Base_Address;
+
+end HW.MMIO_Range;
diff --git a/src/lib/timer/Makefile.inc b/src/lib/timer/Makefile.inc
new file mode 100644
index 0000000..9e7ef18
--- /dev/null
+++ b/src/lib/timer/Makefile.inc
@@ -0,0 +1,15 @@
+##
+## 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.
+##
+
+ramstage-$(CONFIG_WITH_SPARK_HW) += hw-time-timer.ads
+ramstage-$(CONFIG_SPARK_TIMER_NULL) += null/hw-time-timer.adb
diff --git a/src/lib/timer/hw-time-timer.ads b/src/lib/timer/hw-time-timer.ads
new file mode 100644
index 0000000..e4638e7
--- /dev/null
+++ b/src/lib/timer/hw-time-timer.ads
@@ -0,0 +1,39 @@
+--
+-- This file is part of the coreboot project.
+--
+-- 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.
+--
+
+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
+
+ -- procedure as workaround until Volatile_Function works
+ procedure Raw_Value (Value : out T)
+ with
+ Global => (Input => Abstract_Time),
+ Depends => (Value => Abstract_Time);
+ --function Raw_Value return T
+ -- with
+ -- Volatile_Function,
+ -- Global => (Input => Abstract_Time);
+
+ function Hz return T
+ with
+ Global => (Input => Timer_State);
+
+end HW.Time.Timer;
diff --git a/src/lib/timer/null/hw-time-timer.adb b/src/lib/timer/null/hw-time-timer.adb
new file mode 100644
index 0000000..8d54131
--- /dev/null
+++ b/src/lib/timer/null/hw-time-timer.adb
@@ -0,0 +1,37 @@
+--
+-- This file is part of the coreboot project.
+--
+-- Copyright (C) 2016 Nico Huber <nico.h at gmx.de>
+--
+-- 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.Time.Timer
+ with Refined_State => (Timer_State => null,
+ Abstract_Time => null)
+is
+
+ procedure Raw_Value (Value : out T)
+ with
+ SPARK_Mode => Off
+ is
+ begin
+ Value := 0;
+ end Raw_Value;
+
+ function Hz return T
+ with
+ SPARK_Mode => Off
+ is
+ begin
+ return 1;
+ end Hz;
+
+end HW.Time.Timer;
More information about the coreboot-gerrit
mailing list