Nico Huber submitted this change.
gma: Merge `Config_State` into `State`
Treating `Config_State` separately was merely cosmetic and caused
lots of trouble. Its usage depends heavily on the selected plat-
form. Hence, `Global` contracts were not stable across different
configurations.
Let's avoid the annotation mess that it brought us and merge it
into `State`.
Change-Id: Ie28ccfc7ffbe08e0b3fe343d9e6df2420611834e
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/35713
Reviewed-by: Arthur Heymans <arthur@aheymans.xyz>
---
M common/hw-gfx-gma-config.ads.template
M common/hw-gfx-gma-registers.ads
M common/hw-gfx-gma.adb
M common/hw-gfx-gma.ads
4 files changed, 19 insertions(+), 44 deletions(-)
diff --git a/common/hw-gfx-gma-config.ads.template b/common/hw-gfx-gma-config.ads.template
index 1f6fea6..d5bd2ba 100644
--- a/common/hw-gfx-gma-config.ads.template
+++ b/common/hw-gfx-gma-config.ads.template
@@ -71,7 +71,7 @@
Dyn_CPU => Gen_CPU_Type'First,
Dyn_CPU_Var => Gen_CPU_Variant'First);
- Variable : Variable_Config with Part_Of => GMA.Config_State;
+ Variable : Variable_Config with Part_Of => GMA.State;
Valid_Port : Valid_Port_Array renames Variable.Valid_Port;
Raw_Clock : Frequency_Type renames Variable.Raw_Clock;
diff --git a/common/hw-gfx-gma-registers.ads b/common/hw-gfx-gma-registers.ads
index e9c8ab4..81fb219 100644
--- a/common/hw-gfx-gma-registers.ads
+++ b/common/hw-gfx-gma-registers.ads
@@ -1763,7 +1763,7 @@
(GTT_State =>+ (Config.Variable, GTT_Page, Device_Address, Valid)),
Annotate =>
(GNATprove, Intentional,
- """GMA.Config_State"" of ""Write_GTT"" not read",
+ """GMA.State"" of ""Write_GTT"" not read",
"Reading of Config_State depends on the platform configuration.");
procedure Read_GTT
@@ -1779,7 +1779,7 @@
(Config.Variable, GTT_State, GTT_Page)),
Annotate =>
(GNATprove, Intentional,
- """GMA.Config_State"" of ""Read_GTT"" not read",
+ """GMA.State"" of ""Read_GTT"" not read",
"Reading of Config_State depends on the platform configuration.");
pragma Warnings (GNATprove, On, "no check message justified by this");
diff --git a/common/hw-gfx-gma.adb b/common/hw-gfx-gma.adb
index 8352e1c..3221e3e 100644
--- a/common/hw-gfx-gma.adb
+++ b/common/hw-gfx-gma.adb
@@ -38,7 +38,8 @@
package body HW.GFX.GMA
with Refined_State =>
(State =>
- (PCI_Usable,
+ (Config.Variable,
+ PCI_Usable,
Dev.Address_State,
Registers.Address_State,
PCode.Mailbox_Ready,
@@ -47,7 +48,6 @@
HPD_Delay, Wait_For_HPD,
Linear_FB_Base),
Init_State => Initialized,
- Config_State => (Config.Variable),
Device_State =>
(Dev.PCI_State, Registers.Register_State, Registers.GTT_State))
is
diff --git a/common/hw-gfx-gma.ads b/common/hw-gfx-gma.ads
index 3a4580e..bdc4704 100644
--- a/common/hw-gfx-gma.ads
+++ b/common/hw-gfx-gma.ads
@@ -24,7 +24,6 @@
Abstract_State =>
(State,
Init_State,
- Config_State,
(Device_State with External)),
Initializes => Init_State
is
@@ -105,7 +104,7 @@
with
Global =>
(In_Out => (Device_State, Port_IO.State),
- Output => (State, Init_State, Config_State),
+ Output => (State, Init_State),
Input => (Time.State)),
Post => Success = Is_Initialized;
function Is_Initialized return Boolean
@@ -116,7 +115,7 @@
procedure Power_Up_VGA
with
Global =>
- (Input => (State, Config_State, Time.State),
+ (Input => (State, Time.State),
In_Out => (Device_State),
Proof_In => (Init_State)),
Pre => Is_Initialized;
@@ -126,24 +125,17 @@
procedure Update_Outputs (Configs : Pipe_Configs)
with
Global =>
- (Input => (Config_State, Time.State),
+ (Input => (Time.State),
In_Out => (State, Device_State, Port_IO.State),
Proof_In => (Init_State)),
Pre => Is_Initialized;
- pragma Warnings (GNATprove, Off, "no check message justified by this",
- Reason => "see Annotate aspects.");
procedure Update_Cursor (Pipe : Pipe_Index; Cursor : Cursor_Type)
with
Global =>
- (Input => (Config_State),
- In_Out => (State, Device_State),
+ (In_Out => (State, Device_State),
Proof_In => (Init_State)),
- Pre => Is_Initialized,
- Annotate =>
- (GNATprove, Intentional,
- "global input ""GMA.Config_State"" of ""Update_Cursor"" not read",
- "Reading of Config_State depends on the platform configuration.");
+ Pre => Is_Initialized;
procedure Place_Cursor
(Pipe : Pipe_Index;
@@ -151,14 +143,9 @@
Y : Cursor_Pos)
with
Global =>
- (Input => (Config_State),
- In_Out => (State, Device_State),
+ (In_Out => (State, Device_State),
Proof_In => (Init_State)),
- Pre => Is_Initialized,
- Annotate =>
- (GNATprove, Intentional,
- "global input ""GMA.Config_State"" of ""Place_Cursor"" not read",
- "Reading of Config_State depends on the platform configuration.");
+ Pre => Is_Initialized;
procedure Move_Cursor
(Pipe : Pipe_Index;
@@ -166,14 +153,9 @@
Y : Cursor_Pos)
with
Global =>
- (Input => (Config_State),
- In_Out => (State, Device_State),
+ (In_Out => (State, Device_State),
Proof_In => (Init_State)),
- Pre => Is_Initialized,
- Annotate =>
- (GNATprove, Intentional,
- "global input ""GMA.Config_State"" of ""Move_Cursor"" not read",
- "Reading of Config_State depends on the platform configuration.");
+ Pre => Is_Initialized;
----------------------------------------------------------------------------
@@ -183,7 +165,7 @@
Valid : Boolean)
with
Global =>
- (Input => Config_State,
+ (Input => State,
In_Out => Device_State, Proof_In => Init_State),
Pre => Is_Initialized;
@@ -193,7 +175,7 @@
GTT_Page : in GTT_Range)
with
Global =>
- (Input => Config_State,
+ (Input => State,
In_Out => Device_State, Proof_In => Init_State),
Pre => Is_Initialized;
@@ -203,8 +185,7 @@
Success : out Boolean)
with
Global =>
- (Input => Config_State,
- In_Out =>
+ (In_Out =>
(State, Device_State,
Framebuffer_Filler.State, Framebuffer_Filler.Base_Address),
Proof_In => (Init_State)),
@@ -213,15 +194,9 @@
procedure Map_Linear_FB (Linear_FB : out Word64; FB : in Framebuffer_Type)
with
Global =>
- (Input => Config_State,
- In_Out => (State, Device_State),
+ (In_Out => (State, Device_State),
Proof_In => (Init_State)),
- Pre => Is_Initialized and HW.Config.Dynamic_MMIO,
- Annotate =>
- (GNATprove, Intentional,
- "global input ""GMA.Config_State"" of ""Map_Linear_FB"" not read",
- "Reading of Config_State depends on the platform configuration.");
- pragma Warnings (GNATprove, On, "no check message justified by this");
+ Pre => Is_Initialized and HW.Config.Dynamic_MMIO;
----------------------------------------------------------------------------
To view, visit change 35713. To unsubscribe, or for help writing mail filters, visit settings.