commit 9e96a45649a8e7c8d945220bbaa0e37ff1af8adf
author Nico Huber <nico.h@gmx.de> Sun Sep 22 20:25:17 2019 +0200
committer Nico Huber <nico.h@gmx.de> Fri Oct 04 21:34:46 2019 +0000
tree 9b8552aad49ed267cca4a352c7c19017d7a7d0fa
parent 312433cd3d90ebd5ee44bc1795b10e3846c1f96c

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>

common/hw-gfx-gma-config_helpers.ads

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;

common/hw-gfx-gma-pipe_setup.ads

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;