gma config: Make Config.CPU and Config.CPU_Var variable
Introduce CONFIG_GFX_GMA_DYN_CPU that, if set to `y`, makes `Config.CPU`
and `Config.CPU_Var` variables. All other config values derived from
these are turned into expression functions.
Change-Id: If409b5afbd975f3a42e28ff191a092f89ece5ae2
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/27068
Reviewed-by: Angel Pons <th3fanbus@gmail.com>
Reviewed-by: Patrick Georgi <pgeorgi@google.com>
diff --git a/common/Makefile.inc b/common/Makefile.inc
index 11ca2c3..ba48f85 100644
--- a/common/Makefile.inc
+++ b/common/Makefile.inc
@@ -51,8 +51,36 @@
CONFIG_GFX_GMA_INTERNAL_PORT := $(call strip_quotes,$(CONFIG_GFX_GMA_INTERNAL_PORT))
CONFIG_GFX_GMA_ANALOG_I2C_PORT := $(call strip_quotes,$(CONFIG_GFX_GMA_ANALOG_I2C_PORT))
+_GEN_NONCONST := $(strip \
+ $(if $(filter Ironlake,$(CONFIG_GFX_GMA_GENERATION)),ilk, \
+ $(if $(filter Haswell,$(CONFIG_GFX_GMA_GENERATION)),hsw, \
+ $(if $(filter Skylake,$(CONFIG_GFX_GMA_GENERATION)),skl))))
+# GNATprove (GPL 2017) doesn't realize when a boolean expression
+# that depends both on static values and variables can be evalu-
+# ated at compile time (e.g. `False and then Variable` is always
+# `False` and GNAT acts appropriately). So for now, we generate
+# functions instead of constant expressions for these mixed ex-
+# pressions.
+_GEN_CONST_TARGET := <cpufunc> # set to `constant` to generate constants.
+
hw-gfx-gma-config-ads := $(subst //,/,$(call src-to-obj,,$(dir)/hw-gfx-gma-config).ads)
+ifeq ($(CONFIG_GFX_GMA_DYN_CPU),y)
+$(hw-gfx-gma-config-ads): $(dir)/hw-gfx-gma-config.ads.template $(cnf)
+ printf " GENERATE $(patsubst /%,%,$(subst $(obj)/,,$@))\n"
+ sed -e's/<<GEN>>/$(CONFIG_GFX_GMA_GENERATION)/' \
+ -e's/<<INTERNAL_PORT>>/$(CONFIG_GFX_GMA_INTERNAL_PORT)/' \
+ -e's/<<ANALOG_I2C_PORT>>/$(CONFIG_GFX_GMA_ANALOG_I2C_PORT)/' \
+ -e's/<<DEFAULT_MMIO_BASE>>/$(CONFIG_GFX_GMA_DEFAULT_MMIO)/' \
+ -e'/constant Gen_CPU\(_Var\)\?/d' \
+ -e's/<genbool>/constant Boolean/' \
+ -e's/<\(\(ilk\|hsw\|skl\)\(...\)\?\)bool>/<\1var> Boolean/' \
+ $(if $(_GEN_NONCONST),-e's/<\(...\)\?$(_GEN_NONCONST)\(...\)\?var>/<cpufunc>/') \
+ -e's/<\(ilk\|hsw\|skl\)\(...\)\?var>/$(_GEN_CONST_TARGET)/' \
+ -e's/\(.*: *<cpufunc>.*:=\) *\(.*\);/\1\n (\2);/' \
+ -e's/\([^ ]\+\) *: *<cpufunc> \+\([^ ]*\) *:=/function \1 return \2 is/' \
+ $< >$@
+else
$(hw-gfx-gma-config-ads): $(dir)/hw-gfx-gma-config.ads.template $(cnf)
printf " GENERATE $(patsubst /%,%,$(subst $(obj)/,,$@))\n"
sed -e's/<<GEN>>/$(CONFIG_GFX_GMA_GENERATION)/' \
@@ -61,9 +89,12 @@
-e's/<<INTERNAL_PORT>>/$(CONFIG_GFX_GMA_INTERNAL_PORT)/' \
-e's/<<ANALOG_I2C_PORT>>/$(CONFIG_GFX_GMA_ANALOG_I2C_PORT)/' \
-e's/<<DEFAULT_MMIO_BASE>>/$(CONFIG_GFX_GMA_DEFAULT_MMIO)/' \
+ -e":s$$(printf '\n ')/,$$/{N;s/,\n.*Dyn_CPU\(_Var\)\?[^,)]*//;ts$$(printf '\n ')P;D;}" \
+ -e'/Dyn_CPU\(_Var\)\?/d' \
-e's/<\(gen\|\(ilk\|hsw\|skl\)\(...\)\?\)bool>/constant Boolean/' \
-e's/<\(\(ilk\|hsw\|skl\)\(...\)\?\)var>/constant/' \
$< >$@
+endif
gfxinit-gen-y += $(hw-gfx-gma-config-ads)
ifneq ($(filter G45,$(CONFIG_GFX_GMA_CPU)),)
diff --git a/common/hw-gfx-gma-config.ads.template b/common/hw-gfx-gma-config.ads.template
index 87126d5..044036e 100644
--- a/common/hw-gfx-gma-config.ads.template
+++ b/common/hw-gfx-gma-config.ads.template
@@ -59,16 +59,22 @@
type Variable_Config is record
Valid_Port : Valid_Port_Array;
Raw_Clock : Frequency_Type;
+ Dyn_CPU : Gen_CPU_Type;
+ Dyn_CPU_Var : Gen_CPU_Variant;
end record;
Initial_Settings : constant Variable_Config :=
(Valid_Port => (others => False),
- Raw_Clock => Frequency_Type'First);
+ Raw_Clock => Frequency_Type'First,
+ Dyn_CPU => Gen_CPU_Type'First,
+ Dyn_CPU_Var => Gen_CPU_Variant'First);
Variable : Variable_Config with Part_Of => GMA.Config_State;
Valid_Port : Valid_Port_Array renames Variable.Valid_Port;
Raw_Clock : Frequency_Type renames Variable.Raw_Clock;
+ CPU : Gen_CPU_Type renames Variable.Dyn_CPU;
+ CPU_Var : Gen_CPU_Variant renames Variable.Dyn_CPU_Var;
----------------------------------------------------------------------------
@@ -303,12 +309,12 @@
----------------------------------------------------------------------------
- GTT_PTE_Size : <hswvar> := (if Has_64bit_GTT then 8 else 4);
+ GTT_PTE_Size : <hswvar> Natural := (if Has_64bit_GTT then 8 else 4);
- Fence_Base : <ilkvar> :=
+ Fence_Base : <ilkvar> Natural :=
(if not Sandybridge_On then 16#0000_3000# else 16#0010_0000#);
- Fence_Count : <ilkvar> :=
+ Fence_Count : <ilkvar> Natural :=
(if not Ivybridge_On then 16 else 32);
----------------------------------------------------------------------------
diff --git a/common/hw-gfx-gma-registers.adb b/common/hw-gfx-gma-registers.adb
index 838afed..380bced 100644
--- a/common/hw-gfx-gma-registers.adb
+++ b/common/hw-gfx-gma-registers.adb
@@ -16,8 +16,6 @@
with HW.MMIO_Range;
pragma Elaborate_All (HW.MMIO_Range);
-with HW.GFX.GMA.Config;
-
with HW.Debug;
with GNAT.Source_Info;
diff --git a/common/hw-gfx-gma-registers.ads b/common/hw-gfx-gma-registers.ads
index 3be2ec7..ac0f023 100644
--- a/common/hw-gfx-gma-registers.ads
+++ b/common/hw-gfx-gma-registers.ads
@@ -14,6 +14,7 @@
with System;
with HW.GFX.GMA;
+with HW.GFX.GMA.Config;
private package HW.GFX.GMA.Registers
with
@@ -1720,21 +1721,39 @@
procedure Remove_Fence (First_Page, Last_Page : GTT_Range);
+ pragma Warnings (GNATprove, Off, "no check message justified by this",
+ Reason => "see Annotate aspects.");
procedure Write_GTT
(GTT_Page : GTT_Range;
Device_Address : GTT_Address_Type;
Valid : Boolean)
with
- Global => (In_Out => GTT_State),
- Depends => (GTT_State =>+ (GTT_Page, Device_Address, Valid));
+ Global =>
+ (Input => Config.Variable,
+ In_Out => GTT_State),
+ Depends =>
+ (GTT_State =>+ (Config.Variable, GTT_Page, Device_Address, Valid)),
+ Annotate =>
+ (GNATprove, Intentional,
+ """GMA.Config_State"" of ""Write_GTT"" not read",
+ "Reading of Config_State depends on the platform configuration.");
procedure Read_GTT
(Device_Address : out GTT_Address_Type;
Valid : out Boolean;
GTT_Page : in GTT_Range)
with
- Global => (In_Out => GTT_State),
- Depends => ((Device_Address, Valid, GTT_State) => (GTT_State, GTT_Page));
+ Global =>
+ (Input => Config.Variable,
+ In_Out => GTT_State),
+ Depends =>
+ ((Device_Address, Valid, GTT_State) =>
+ (Config.Variable, GTT_State, GTT_Page)),
+ Annotate =>
+ (GNATprove, Intentional,
+ """GMA.Config_State"" of ""Read_GTT"" not read",
+ "Reading of Config_State depends on the platform configuration.");
+ pragma Warnings (GNATprove, On, "no check message justified by this");
procedure Set_Register_Base (Base : Word64; GTT_Base : Word64 := 0)
with
diff --git a/common/hw-gfx-gma.adb b/common/hw-gfx-gma.adb
index 1d97adb..885072c 100644
--- a/common/hw-gfx-gma.adb
+++ b/common/hw-gfx-gma.adb
@@ -528,11 +528,11 @@
pragma Warnings
(GNATprove, Off, """Registers.Register_State"" * is not modified*",
- Reason => "Power_Up_VGA is only effective on certain generations.");
+ Reason => "Power_Up_VGA is only effective in certain configurations.");
procedure Power_Up_VGA
with
Refined_Global =>
- (Input => (Cur_Configs, Time.State),
+ (Input => (Cur_Configs, Config.Variable, Time.State),
In_Out => (Registers.Register_State),
Proof_In => (Initialized))
is
@@ -554,7 +554,7 @@
(GNATprove, Off, "no check message justified*", Reason => "see below");
pragma Annotate
(GNATprove, Intentional, "unused global",
- "Power_Up_VGA is only effective on certain generations.");
+ "Power_Up_VGA is only effective in certain configurations.");
pragma Warnings (GNATprove, On, "no check message justified*");
pragma Warnings
(GNATprove, On, """Registers.Register_State"" * is not modified*");
diff --git a/common/hw-gfx-gma.ads b/common/hw-gfx-gma.ads
index 7c40dd9..3804cd4 100644
--- a/common/hw-gfx-gma.ads
+++ b/common/hw-gfx-gma.ads
@@ -111,7 +111,7 @@
procedure Power_Up_VGA
with
Global =>
- (Input => (State, Time.State),
+ (Input => (State, Config_State, Time.State),
In_Out => (Device_State),
Proof_In => (Init_State)),
Pre => Is_Initialized;
@@ -160,7 +160,9 @@
Device_Address : GTT_Address_Type;
Valid : Boolean)
with
- Global => (In_Out => Device_State, Proof_In => Init_State),
+ Global =>
+ (Input => Config_State,
+ In_Out => Device_State, Proof_In => Init_State),
Pre => Is_Initialized;
procedure Read_GTT
@@ -168,7 +170,9 @@
Valid : out Boolean;
GTT_Page : in GTT_Range)
with
- Global => (In_Out => Device_State, Proof_In => Init_State),
+ Global =>
+ (Input => Config_State,
+ In_Out => Device_State, Proof_In => Init_State),
Pre => Is_Initialized;
procedure Setup_Default_FB
@@ -177,18 +181,27 @@
Success : out Boolean)
with
Global =>
- (In_Out =>
+ (Input => Config_State,
+ In_Out =>
(State, Device_State,
Framebuffer_Filler.State, Framebuffer_Filler.Base_Address),
Proof_In => (Init_State)),
Pre => Is_Initialized and HW.Config.Dynamic_MMIO;
+ pragma Warnings (GNATprove, Off, "no check message justified by this",
+ Reason => "see Annotate aspects.");
procedure Map_Linear_FB (Linear_FB : out Word64; FB : in Framebuffer_Type)
with
Global =>
- (In_Out => (State, Device_State),
+ (Input => Config_State,
+ In_Out => (State, Device_State),
Proof_In => (Init_State)),
- Pre => Is_Initialized and HW.Config.Dynamic_MMIO;
+ Pre => Is_Initialized and HW.Config.Dynamic_MMIO,
+ Annotate =>
+ (GNATprove, Intentional,
+ "global input ""GMA.Config_State"" of ""Map_Linear_FB"" not read",
+ "Reading of Config_State depends on the platform configuration.");
+ pragma Warnings (GNATprove, On, "no check message justified by this");
----------------------------------------------------------------------------