commit da1185eea1dad41b9b15685cbe5eaaf352158d16
author Nico Huber <nico.h@gmx.de> Sun Jun 03 01:07:46 2018 +0200
committer Nico Huber <nico.h@gmx.de> Wed Jun 13 09:15:50 2018 +0000
tree 05d31280a43fc3865db4c0ee9dd4d92fcdad214d
parent db68441c979d4f3623a0fb6b906683955ff95c66

gfx, gma pipe_setup: Rewrite Scale_Keep_Aspect

Use Scaling_Type() to organize the different scaling cases. Looks better
and outlining the calculation helps GNATprove on bad days.

Change-Id: I14af765c6f17aeccff3f9274ccec3756493670d7
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.coreboot.org/26848
Reviewed-by: Arthur Heymans <arthur@aheymans.xyz>

common/hw-gfx-gma-pipe_setup.adb

diff --git a/common/hw-gfx-gma-pipe_setup.adb b/common/hw-gfx-gma-pipe_setup.adb
index a45dfb2..68cc98e 100644
--- a/common/hw-gfx-gma-pipe_setup.adb
+++ b/common/hw-gfx-gma-pipe_setup.adb
@@ -393,6 +393,14 @@
 
    ----------------------------------------------------------------------------
 
+   function Scale (Val, Max, Num, Denom : Pos32)
+      return Pos32 is ((Val * Num) / Denom)
+   with
+      Pre =>
+         Val * Num <= Int32'Last and Denom <= Num and
+         Val * Num < Max * Denom,
+      Post => Scale'Result < Max;
+
    procedure Scale_Keep_Aspect
      (Width       :    out Pos32;
       Height      :    out Pos32;
@@ -411,14 +419,17 @@
       Src_Width : constant Pos32 := Pos32 (Rotated_Width (Framebuffer));
       Src_Height : constant Pos32 := Pos32 (Rotated_Height (Framebuffer));
    begin
-      if (Max_Width * Src_Height) / Src_Width <= Max_Height then
-         Width  := Max_Width;
-         Height := (Max_Width * Src_Height) / Src_Width;
-      else
-         Height := Max_Height;
-         Width  := Pos32'Min (Max_Width,  -- could prove, it's <= Max_Width
-            (Max_Height * Src_Width) / Src_Height);
-      end if;
+      case Scaling_Type (Src_Width, Src_Height, Max_Width, Max_Height) is
+         when Letterbox =>
+            Width  := Max_Width;
+            Height := Scale (Src_Height, Max_Height, Max_Width, Src_Width);
+         when Pillarbox =>
+            Width  := Scale (Src_Width, Max_Width, Max_Height, Src_Height);
+            Height := Max_Height;
+         when Uniform =>
+            Width  := Max_Width;
+            Height := Max_Height;
+      end case;
    end Scale_Keep_Aspect;
 
    procedure Setup_Skylake_Pipe_Scaler

common/hw-gfx.ads

diff --git a/common/hw-gfx.ads b/common/hw-gfx.ads
index 86ef51b..beb111f 100644
--- a/common/hw-gfx.ads
+++ b/common/hw-gfx.ads
@@ -198,17 +198,22 @@
       Rotated_Height (FB) /= Mode.V_Visible);
 
    type Scaling_Aspect is (Uniform, Letterbox, Pillarbox);
-   function Scaling_Type (FB : Framebuffer_Type; Mode : Mode_Type)
+   function Scaling_Type (Width, Height, Scaled_Width, Scaled_Height : Pos32)
       return Scaling_Aspect is
-     (if Pos32 (Mode.H_Visible) * Pos32 (Rotated_Height (FB)) <
-         Pos32 (Mode.V_Visible) * Pos32 (Rotated_Width (FB))
-      then
-         Letterbox
-      elsif Pos32 (Mode.H_Visible) * Pos32 (Rotated_Height (FB)) >
-            Pos32 (Mode.V_Visible) * Pos32 (Rotated_Width (FB))
-      then
-         Pillarbox
-      else
-         Uniform);
+     (if    Scaled_Width * Height < Scaled_Height * Width   then Letterbox
+      elsif Scaled_Width * Height > Scaled_Height * Width   then Pillarbox
+      else                                                       Uniform)
+   with
+      Pre =>
+         Width <= Pos32 (Pos16'Last) and
+         Height <= Pos32 (Pos16'Last) and
+         Scaled_Width <= Pos32 (Pos16'Last) and
+         Scaled_Height <= Pos32 (Pos16'Last);
+   function Scaling_Type (FB : Framebuffer_Type; Mode : Mode_Type)
+      return Scaling_Aspect is (Scaling_Type
+     (Width          => Pos32 (Rotated_Width (FB)),
+      Height         => Pos32 (Rotated_Height (FB)),
+      Scaled_Width   => Pos32 (Mode.H_Visible),
+      Scaled_Height  => Pos32 (Mode.V_Visible)));
 
 end HW.GFX;