Nico Huber has submitted this change and it was merged. ( https://review.coreboot.org/c/libgfxinit/+/26866 )
Change subject: gma: Provide `Global` contracts for public procedures ......................................................................
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 --- M common/hw-gfx-framebuffer_filler.adb M common/hw-gfx-framebuffer_filler.ads M common/hw-gfx-gma.adb M common/hw-gfx-gma.ads 4 files changed, 74 insertions(+), 12 deletions(-)
Approvals: Nico Huber: Verified Arthur Heymans: Looks good to me, approved
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,