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>
This commit is contained in:
Nico Huber
2018-06-03 01:07:46 +02:00
parent db68441c97
commit da1185eea1
2 changed files with 35 additions and 19 deletions

View File

@@ -393,6 +393,14 @@ package body HW.GFX.GMA.Pipe_Setup is
----------------------------------------------------------------------------
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 @@ package body HW.GFX.GMA.Pipe_Setup is
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

View File

@@ -198,17 +198,22 @@ private
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;