Nico Huber has uploaded this change for review. ( https://review.coreboot.org/26848
Change subject: gfx, gma pipe_setup: Rewrite Scale_Keep_Aspect ......................................................................
gfx, gma pipe_setup: Rewrite Scale_Keep_Aspect
Use Scaling_Type() to organize the different scaling cases. Looks better and helps GNATprove on bad days.
Change-Id: I14af765c6f17aeccff3f9274ccec3756493670d7 Signed-off-by: Nico Huber nico.h@gmx.de --- M common/hw-gfx-gma-pipe_setup.adb M common/hw-gfx.ads 2 files changed, 28 insertions(+), 19 deletions(-)
git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/48/26848/1
diff --git a/common/hw-gfx-gma-pipe_setup.adb b/common/hw-gfx-gma-pipe_setup.adb index a45dfb2..e0be5fb 100644 --- a/common/hw-gfx-gma-pipe_setup.adb +++ b/common/hw-gfx-gma-pipe_setup.adb @@ -411,14 +411,18 @@ 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 := (Max_Width * Src_Height) / Src_Width; + when Pillarbox => + pragma Assert ((Max_Height * Src_Width) / Src_Height <= Max_Width); + Width := (Max_Height * Src_Width) / Src_Height; + Height := Max_Height; + when Uniform => + Width := Max_Width; + Height := Max_Height; + end case; end Scale_Keep_Aspect;
procedure Setup_Skylake_Pipe_Scaler 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;