Nico Huber has uploaded this change for review. ( https://review.coreboot.org/c/libgfxinit/+/35527 )
Change subject: gma config_helpers: Revise Validate_Config() ......................................................................
gma config_helpers: Revise Validate_Config()
Split it into Valid_FB() and Valid_Config() and make both expression functions. This will make it easier to use them for proofs.
Change-Id: I0931217658000d3ff6d71515acb45aeb063768d5 Signed-off-by: Nico Huber nico.h@gmx.de --- M common/hw-gfx-gma-config_helpers.adb M common/hw-gfx-gma-config_helpers.ads M common/hw-gfx-gma-pipe_setup.ads M common/hw-gfx-gma.adb 4 files changed, 42 insertions(+), 58 deletions(-)
git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/27/35527/1
diff --git a/common/hw-gfx-gma-config_helpers.adb b/common/hw-gfx-gma-config_helpers.adb index c95bebc..a86af9e 100644 --- a/common/hw-gfx-gma-config_helpers.adb +++ b/common/hw-gfx-gma-config_helpers.adb @@ -12,7 +12,6 @@ -- GNU General Public License for more details. --
-with HW.GFX.GMA.Config; with HW.GFX.GMA.Connector_Info; with HW.GFX.GMA.DP_Info; with HW.GFX.GMA.Registers; @@ -182,40 +181,4 @@ end if; end Fill_Port_Config;
- ---------------------------------------------------------------------------- - - -- Validates that a given configuration should work with - -- a given framebuffer. - function Validate_Config - (FB : Framebuffer_Type; - Mode : Mode_Type; - Pipe : Pipe_Index; - Scaler_Available : Boolean) - return Boolean - is - begin - -- No downscaling - -- Respect maximum scalable width - -- VGA plane is only allowed on the primary pipe - -- Only 32bpp RGB (ignored for VGA plane) - -- Stride must be big enough and a multiple of 64 bytes or the tile size - -- (ignored for VGA plane) - -- Y-Tiling and rotation are only supported on newer generations (with - -- Plane_Control) - -- 90 degree rotations are only supported with Y-tiling - return - ((Rotated_Width (FB) = Mode.H_Visible and - Rotated_Height (FB) = Mode.V_Visible) or - (Scaler_Available and - Rotated_Width (FB) <= Config.Maximum_Scalable_Width (Pipe) and - Rotated_Width (FB) <= Mode.H_Visible and - Rotated_Height (FB) <= Mode.V_Visible)) and - (FB.Offset /= VGA_PLANE_FRAMEBUFFER_OFFSET or Pipe = Primary) and - (FB.Offset = VGA_PLANE_FRAMEBUFFER_OFFSET or - (FB.BPC = 8 and Valid_Stride (FB) and - (Config.Has_Plane_Control or - (FB.Tiling /= Y_Tiled and FB.Rotation = No_Rotation)) and - (FB.Tiling = Y_Tiled or not Rotation_90 (FB)))); - end Validate_Config; - end HW.GFX.GMA.Config_Helpers; diff --git a/common/hw-gfx-gma-config_helpers.ads b/common/hw-gfx-gma-config_helpers.ads index d56be5e..023b3e5 100644 --- a/common/hw-gfx-gma-config_helpers.ads +++ b/common/hw-gfx-gma-config_helpers.ads @@ -14,6 +14,8 @@
with HW;
+with HW.GFX.GMA.Config; + private package HW.GFX.GMA.Config_Helpers is
@@ -39,18 +41,44 @@ Reason => "Needed for older compiler versions"); use type HW.Pos32; pragma Warnings (GNAT, On, """Integer_32"" is already use-visible *"); - function Validate_Config + + -- Validate that a framebuffer is valid for a given mode and pipe. + function Valid_FB + (FB : Framebuffer_Type; + Mode : Mode_Type; + Pipe : Pipe_Index) + return Boolean is + (-- No downscaling + -- Respect maximum scalable width + -- VGA plane is only allowed on the primary pipe + -- Only 32bpp RGB (ignored for VGA plane) + -- Stride must be big enough and a multiple of 64 bytes or the tile size + -- (ignored for VGA plane) + -- Y-Tiling and rotation are only supported on newer generations (with + -- Plane_Control) + -- 90 degree rotations are only supported with Y-tiling + ((Rotated_Width (FB) = Mode.H_Visible and + Rotated_Height (FB) = Mode.V_Visible) or + (Rotated_Width (FB) <= Config.Maximum_Scalable_Width (Pipe) and + Rotated_Width (FB) <= Mode.H_Visible and + Rotated_Height (FB) <= Mode.V_Visible)) and + (FB.Offset /= VGA_PLANE_FRAMEBUFFER_OFFSET or Pipe = Primary) and + (FB.Offset = VGA_PLANE_FRAMEBUFFER_OFFSET or + (FB.BPC = 8 and Valid_Stride (FB) and + (Config.Has_Plane_Control or + (FB.Tiling /= Y_Tiled and FB.Rotation = No_Rotation)) and + (FB.Tiling = Y_Tiled or not Rotation_90 (FB))))); + + -- Also validate that we only scale if a scaler is available. + function Valid_Config (FB : Framebuffer_Type; Mode : Mode_Type; Pipe : Pipe_Index; Scaler_Available : Boolean) - return Boolean - with - Post => - (if Validate_Config'Result then - Rotated_Width (FB) <= Mode.H_Visible and - Rotated_Height (FB) <= Mode.V_Visible and - (FB.Offset = VGA_PLANE_FRAMEBUFFER_OFFSET or - FB.Height + FB.Start_Y <= FB.V_Stride)); + return Boolean is + (Valid_FB (FB, Mode, Pipe) and + ((Rotated_Width (FB) = Mode.H_Visible and + Rotated_Height (FB) = Mode.V_Visible) or + Scaler_Available));
end HW.GFX.GMA.Config_Helpers; diff --git a/common/hw-gfx-gma-pipe_setup.ads b/common/hw-gfx-gma-pipe_setup.ads index 0edb0c9..990f306 100644 --- a/common/hw-gfx-gma-pipe_setup.ads +++ b/common/hw-gfx-gma-pipe_setup.ads @@ -13,6 +13,7 @@ --
with HW.GFX.GMA.Config; +with HW.GFX.GMA.Config_Helpers; with HW.GFX.GMA.Registers;
use type HW.Int32; @@ -26,11 +27,7 @@ Framebuffer : Framebuffer_Type; Cursor : Cursor_Type) with - Pre => - Rotated_Width (Framebuffer) <= Port_Cfg.Mode.H_Visible and - Rotated_Height (Framebuffer) <= Port_Cfg.Mode.V_Visible and - (Framebuffer.Offset = VGA_PLANE_FRAMEBUFFER_OFFSET or - Framebuffer.Height + Framebuffer.Start_Y <= Framebuffer.V_Stride); + Pre => Config_Helpers.Valid_FB (Framebuffer, Port_Cfg.Mode, Pipe);
procedure Off (Pipe : Pipe_Index);
@@ -43,11 +40,7 @@ Mode : Mode_Type; Framebuffer : Framebuffer_Type) with - Pre => - Rotated_Width (Framebuffer) <= Mode.H_Visible and - Rotated_Height (Framebuffer) <= Mode.V_Visible and - (Framebuffer.Offset = VGA_PLANE_FRAMEBUFFER_OFFSET or - Framebuffer.Height + Framebuffer.Start_Y <= Framebuffer.V_Stride); + Pre => Config_Helpers.Valid_FB (Framebuffer, Mode, Pipe);
procedure Update_Cursor (Pipe : Pipe_Index; diff --git a/common/hw-gfx-gma.adb b/common/hw-gfx-gma.adb index 15d234a..de79fd3 100644 --- a/common/hw-gfx-gma.adb +++ b/common/hw-gfx-gma.adb @@ -110,7 +110,7 @@
if Success then Display_Controller.Scaler_Available (Scaler_Available, Pipe); - Success := Config_Helpers.Validate_Config + Success := Config_Helpers.Valid_Config (Pipe_Cfg.Framebuffer, Port_Cfg.Mode, Pipe, Scaler_Available); end if;
@@ -305,7 +305,7 @@ Cur_Config.Framebuffer /= New_Config.Framebuffer then Display_Controller.Scaler_Available (Scaler_Available, Pipe); - if Config_Helpers.Validate_Config + if Config_Helpers.Valid_Config (New_Config.Framebuffer, New_Config.Mode, Pipe, Scaler_Available) then
Hello Arthur Heymans, Matt DeVillier, Thomas Heijligen,
I'd like you to reexamine a change. Please visit
https://review.coreboot.org/c/libgfxinit/+/35527
to look at the new patch set (#2).
Change subject: gma config_helpers: Introduce Valid_FB() ......................................................................
gma config_helpers: Introduce Valid_FB()
Make the post condition of Validate_Config() a separate function, Valid_FB(). This way, we don't have to repeat it everywhere.
Theoretically, we could make Validate_Config() an expression function, too. Alas, all the added conditions seem to distract provers too much.
Change-Id: I0931217658000d3ff6d71515acb45aeb063768d5 Signed-off-by: Nico Huber nico.h@gmx.de --- M common/hw-gfx-gma-config_helpers.ads M common/hw-gfx-gma-pipe_setup.ads 2 files changed, 16 insertions(+), 16 deletions(-)
git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/27/35527/2
Nico Huber has posted comments on this change. ( https://review.coreboot.org/c/libgfxinit/+/35527 )
Change subject: gma config_helpers: Introduce Valid_FB() ......................................................................
Patch Set 2: Verified+1
Arthur Heymans has posted comments on this change. ( https://review.coreboot.org/c/libgfxinit/+/35527 )
Change subject: gma config_helpers: Introduce Valid_FB() ......................................................................
Patch Set 2: Code-Review+2
Angel Pons has posted comments on this change. ( https://review.coreboot.org/c/libgfxinit/+/35527 )
Change subject: gma config_helpers: Introduce Valid_FB() ......................................................................
Patch Set 2: Code-Review+2
Nico Huber has submitted this change. ( https://review.coreboot.org/c/libgfxinit/+/35527 )
Change subject: gma config_helpers: Introduce Valid_FB() ......................................................................
gma config_helpers: Introduce Valid_FB()
Make the post condition of Validate_Config() a separate function, Valid_FB(). This way, we don't have to repeat it everywhere.
Theoretically, we could make Validate_Config() an expression function, too. Alas, all the added conditions seem to distract provers too much.
Change-Id: I0931217658000d3ff6d71515acb45aeb063768d5 Signed-off-by: Nico Huber nico.h@gmx.de Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/35527 Reviewed-by: Arthur Heymans arthur@aheymans.xyz Reviewed-by: Angel Pons th3fanbus@gmail.com --- M common/hw-gfx-gma-config_helpers.ads M common/hw-gfx-gma-pipe_setup.ads 2 files changed, 16 insertions(+), 16 deletions(-)
Approvals: Nico Huber: Verified Arthur Heymans: Looks good to me, approved Angel Pons: Looks good to me, approved
diff --git a/common/hw-gfx-gma-config_helpers.ads b/common/hw-gfx-gma-config_helpers.ads index d56be5e..7bbf423 100644 --- a/common/hw-gfx-gma-config_helpers.ads +++ b/common/hw-gfx-gma-config_helpers.ads @@ -39,6 +39,18 @@ Reason => "Needed for older compiler versions"); use type HW.Pos32; pragma Warnings (GNAT, On, """Integer_32"" is already use-visible *"); + + -- Validate just enough to satisfy Pipe_Setup pre conditions. + function Valid_FB + (FB : Framebuffer_Type; + Mode : Mode_Type) + return Boolean is + (Rotated_Width (FB) <= Mode.H_Visible and + Rotated_Height (FB) <= Mode.V_Visible and + (FB.Offset = VGA_PLANE_FRAMEBUFFER_OFFSET or + FB.Height + FB.Start_Y <= FB.V_Stride)); + + -- Also validate that we only use supported values / features. function Validate_Config (FB : Framebuffer_Type; Mode : Mode_Type; @@ -46,11 +58,6 @@ Scaler_Available : Boolean) return Boolean with - Post => - (if Validate_Config'Result then - Rotated_Width (FB) <= Mode.H_Visible and - Rotated_Height (FB) <= Mode.V_Visible and - (FB.Offset = VGA_PLANE_FRAMEBUFFER_OFFSET or - FB.Height + FB.Start_Y <= FB.V_Stride)); + Post => (if Validate_Config'Result then Valid_FB (FB, Mode));
end HW.GFX.GMA.Config_Helpers; diff --git a/common/hw-gfx-gma-pipe_setup.ads b/common/hw-gfx-gma-pipe_setup.ads index 0edb0c9..3ecb6dd 100644 --- a/common/hw-gfx-gma-pipe_setup.ads +++ b/common/hw-gfx-gma-pipe_setup.ads @@ -13,6 +13,7 @@ --
with HW.GFX.GMA.Config; +with HW.GFX.GMA.Config_Helpers; with HW.GFX.GMA.Registers;
use type HW.Int32; @@ -26,11 +27,7 @@ Framebuffer : Framebuffer_Type; Cursor : Cursor_Type) with - Pre => - Rotated_Width (Framebuffer) <= Port_Cfg.Mode.H_Visible and - Rotated_Height (Framebuffer) <= Port_Cfg.Mode.V_Visible and - (Framebuffer.Offset = VGA_PLANE_FRAMEBUFFER_OFFSET or - Framebuffer.Height + Framebuffer.Start_Y <= Framebuffer.V_Stride); + Pre => Config_Helpers.Valid_FB (Framebuffer, Port_Cfg.Mode);
procedure Off (Pipe : Pipe_Index);
@@ -43,11 +40,7 @@ Mode : Mode_Type; Framebuffer : Framebuffer_Type) with - Pre => - Rotated_Width (Framebuffer) <= Mode.H_Visible and - Rotated_Height (Framebuffer) <= Mode.V_Visible and - (Framebuffer.Offset = VGA_PLANE_FRAMEBUFFER_OFFSET or - Framebuffer.Height + Framebuffer.Start_Y <= Framebuffer.V_Stride); + Pre => Config_Helpers.Valid_FB (Framebuffer, Mode);
procedure Update_Cursor (Pipe : Pipe_Index;
-
Angel Pons (Code Review) -
Arthur Heymans (Code Review)
-
Nico Huber (Code Review)