[coreboot-gerrit] Change in libgfxinit[master]: gma config_helpers: Introduce Valid_FB()

[Nico Huber (Code Review)]

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 
Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/35527
Reviewed-by: Arthur Heymans 
Reviewed-by: Angel Pons 
---
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;