gma: Provide `Global` contracts for public procedures
We have to enforce a contract on Power_Up_VGA(), as it has no effect
on older hardware generations.
Change-Id: I13af0d90ff738e1eea5f8992718e00a6a09c4705
Signed-off-by: Nico Huber <nico.huber@secunet.com>
Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/26866
Reviewed-by: Arthur Heymans <arthur@aheymans.xyz>
Tested-by: Nico Huber <nico.h@gmx.de>
diff --git a/common/hw-gfx-framebuffer_filler.adb b/common/hw-gfx-framebuffer_filler.adb
index 250d903..29c7da6 100644
--- a/common/hw-gfx-framebuffer_filler.adb
+++ b/common/hw-gfx-framebuffer_filler.adb
@@ -17,6 +17,8 @@
pragma Elaborate_All (HW.MMIO_Range);
package body HW.GFX.Framebuffer_Filler
+with
+ Refined_State => (State => FB.State, Base_Address => FB.Base_Address)
is
type FB_Index is new Natural range
diff --git a/common/hw-gfx-framebuffer_filler.ads b/common/hw-gfx-framebuffer_filler.ads
index 228d43a..7ad3b79 100644
--- a/common/hw-gfx-framebuffer_filler.ads
+++ b/common/hw-gfx-framebuffer_filler.ads
@@ -19,6 +19,9 @@
use type HW.Int32;
package HW.GFX.Framebuffer_Filler
+with
+ Abstract_State => ((State with External), Base_Address),
+ Initializes => Base_Address
is
procedure Fill (Linear_FB : Word64; Framebuffer : Framebuffer_Type)
diff --git a/common/hw-gfx-gma.adb b/common/hw-gfx-gma.adb
index f135a5e..a443132 100644
--- a/common/hw-gfx-gma.adb
+++ b/common/hw-gfx-gma.adb
@@ -18,8 +18,6 @@
with HW.PCI.Dev;
pragma Elaborate_All (HW.PCI.Dev);
-with HW.GFX.Framebuffer_Filler;
-
with HW.GFX.GMA.Config;
with HW.GFX.GMA.Config_Helpers;
with HW.GFX.GMA.Registers;
@@ -527,7 +525,15 @@
----------------------------------------------------------------------------
+ pragma Warnings
+ (GNATprove, Off, """Registers.Register_State"" * is not modified*",
+ Reason => "Power_Up_VGA is only effective on certain generations.");
procedure Power_Up_VGA
+ with
+ Refined_Global =>
+ (Input => (Cur_Configs, Time.State),
+ In_Out => (Registers.Register_State),
+ Proof_In => (Initialized))
is
Fake_Config : constant Pipe_Configs :=
(Primary =>
@@ -543,6 +549,14 @@
begin
Power_And_Clocks.Power_Up (Cur_Configs, Fake_Config);
end Power_Up_VGA;
+ pragma Warnings
+ (GNATprove, Off, "no check message justified*", Reason => "see below");
+ pragma Annotate
+ (GNATprove, Intentional, "unused global",
+ "Power_Up_VGA is only effective on certain generations.");
+ pragma Warnings (GNATprove, On, "no check message justified*");
+ pragma Warnings
+ (GNATprove, On, """Registers.Register_State"" * is not modified*");
----------------------------------------------------------------------------
diff --git a/common/hw-gfx-gma.ads b/common/hw-gfx-gma.ads
index 1f81ece..7f44a0f 100644
--- a/common/hw-gfx-gma.ads
+++ b/common/hw-gfx-gma.ads
@@ -16,6 +16,7 @@
with HW.Config;
with HW.Time;
with HW.Port_IO;
+with HW.GFX.Framebuffer_Filler;
package HW.GFX.GMA
with
@@ -107,44 +108,86 @@
Global => (Input => Init_State);
pragma Warnings (GNATprove, On, "unused variable ""Write_Delay""");
- pragma Warnings (GNATprove, Off, "subprogram ""Power_Up_VGA"" has no effect",
- Reason => "Effect depends on the platform compiled for");
procedure Power_Up_VGA
with
+ Global =>
+ (Input => (State, Time.State),
+ In_Out => (Device_State),
+ Proof_In => (Init_State)),
Pre => Is_Initialized;
- procedure Update_Outputs (Configs : Pipe_Configs);
+ ----------------------------------------------------------------------------
- procedure Update_Cursor (Pipe : Pipe_Index; Cursor : Cursor_Type);
+ procedure Update_Outputs (Configs : Pipe_Configs)
+ with
+ Global =>
+ (Input => (Config_State, Time.State),
+ In_Out => (State, Device_State, Port_IO.State),
+ Proof_In => (Init_State)),
+ Pre => Is_Initialized;
+
+ procedure Update_Cursor (Pipe : Pipe_Index; Cursor : Cursor_Type)
+ with
+ Global =>
+ (In_Out => (State, Device_State),
+ Proof_In => (Init_State)),
+ Pre => Is_Initialized;
+
procedure Place_Cursor
(Pipe : Pipe_Index;
X : Cursor_Pos;
- Y : Cursor_Pos);
+ Y : Cursor_Pos)
+ with
+ Global =>
+ (In_Out => (State, Device_State),
+ Proof_In => (Init_State)),
+ Pre => Is_Initialized;
+
procedure Move_Cursor
(Pipe : Pipe_Index;
X : Cursor_Pos;
- Y : Cursor_Pos);
+ Y : Cursor_Pos)
+ with
+ Global =>
+ (In_Out => (State, Device_State),
+ Proof_In => (Init_State)),
+ Pre => Is_Initialized;
- pragma Warnings (GNATprove, Off, "subprogram ""Dump_Configs"" has no effect",
- Reason => "It's only used for debugging");
- procedure Dump_Configs (Configs : Pipe_Configs);
+ ----------------------------------------------------------------------------
procedure Write_GTT
(GTT_Page : GTT_Range;
Device_Address : GTT_Address_Type;
- Valid : Boolean);
+ Valid : Boolean)
+ with
+ Global => (In_Out => Device_State, Proof_In => Init_State),
+ Pre => Is_Initialized;
procedure Setup_Default_FB
(FB : in Framebuffer_Type;
Clear : in Boolean := True;
Success : out Boolean)
with
+ Global =>
+ (In_Out =>
+ (State, Device_State,
+ Framebuffer_Filler.State, Framebuffer_Filler.Base_Address),
+ Proof_In => (Init_State)),
Pre => Is_Initialized and HW.Config.Dynamic_MMIO;
procedure Map_Linear_FB (Linear_FB : out Word64; FB : in Framebuffer_Type)
with
+ Global =>
+ (In_Out => (State, Device_State),
+ Proof_In => (Init_State)),
Pre => Is_Initialized and HW.Config.Dynamic_MMIO;
+ ----------------------------------------------------------------------------
+
+ pragma Warnings (GNATprove, Off, "subprogram ""Dump_Configs"" has no effect",
+ Reason => "It's only used for debugging");
+ procedure Dump_Configs (Configs : Pipe_Configs);
+
private
-- For the default framebuffer setup (see below) with 90 degree rotations,
