Nico Huber has uploaded this change for review.
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
To view, visit change 35527. To unsubscribe, or for help writing mail filters, visit settings.