Change in libgfxinit[master]: [WIP]gma config: Make Config.CPU and Config.CPU_Var variable
Nico Huber has uploaded this change for review. ( https://review.coreboot.org/27068
Change subject: [WIP]gma config: Make Config.CPU and Config.CPU_Var variable ......................................................................
[WIP]gma config: Make Config.CPU and Config.CPU_Var variable
Change-Id: If409b5afbd975f3a42e28ff191a092f89ece5ae2 Signed-off-by: Nico Huber nico.h@gmx.de --- M common/Makefile.inc M common/hw-gfx-gma-config.ads.template M common/hw-gfx-gma-registers.adb M common/hw-gfx-gma-registers.ads M common/hw-gfx-gma.ads 5 files changed, 91 insertions(+), 17 deletions(-)
git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/68/27068/1
diff --git a/common/Makefile.inc b/common/Makefile.inc index 5eeba41..b840b1d 100644 --- a/common/Makefile.inc +++ b/common/Makefile.inc @@ -45,13 +45,41 @@ gfxinit-y += hw-gfx-framebuffer_filler.adb gfxinit-y += hw-gfx-framebuffer_filler.ads
+CONFIG_GFX_GMA_GENERATION := $(call strip_quotes,$(CONFIG_GFX_GMA_GENERATION)) CONFIG_GFX_GMA_CPU := $(call strip_quotes,$(CONFIG_GFX_GMA_CPU)) CONFIG_GFX_GMA_CPU_VARIANT := $(call strip_quotes,$(CONFIG_GFX_GMA_CPU_VARIANT)) 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 Variable` is always `False` +# and GNAT acts appropriately). So for now, we generate functions +# instead of constant expressions for these mixed expressions. +_GEN_CONST_TARGET := <cpufunc> # set to <genconst> 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/<((gen|ilk|hsw|skl)(...)?)bool>/<\1const> Boolean/' \ + $(if $(_GEN_NONCONST),-e's/<(...)?$(_GEN_NONCONST)(...)?const>/<cpufunc>/') \ + -e's/<(ilk|hsw|skl)(...)?const>/$(_GEN_CONST_TARGET)/' \ + -e's/<genconst>/constant/' \ + -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)/' \ @@ -60,9 +88,11 @@ -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'/Dyn_CPU(_Var)?/d' \ -e's/<(gen|(ilk|hsw|skl)(...)?)const>/constant/' \ -e's/<(gen|(ilk|hsw|skl)(...)?)bool>/constant Boolean/' \ $< >$@ +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 03f343b..fa62890 100644 --- a/common/hw-gfx-gma-config.ads.template +++ b/common/hw-gfx-gma-config.ads.template @@ -60,15 +60,22 @@ type Settings_T 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 Settings_T := (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 + );
Settings : Settings_T with Part_Of => GMA.Config_State;
Valid_Port : Valid_Port_Array renames Settings.Valid_Port; Raw_Clock : Frequency_Type renames Settings.Raw_Clock; + CPU : Gen_CPU_Type renames Settings.Dyn_CPU; + CPU_Var : Gen_CPU_Variant renames Settings.Dyn_CPU_Var;
----------------------------------------------------------------------------
@@ -288,12 +295,12 @@
----------------------------------------------------------------------------
- GTT_PTE_Size : <hswconst> := (if Has_64bit_GTT then 8 else 4); + GTT_PTE_Size : <hswconst> Natural := (if Has_64bit_GTT then 8 else 4);
- Fence_Base : <ilkconst> := + Fence_Base : <ilkconst> Natural := (if not Sandybridge_Plus then 16#0000_3000# else 16#0010_0000#);
- Fence_Count : <ilkconst> := + Fence_Count : <ilkconst> Natural := (if not Ivybridge_Plus then 16 else 32);
---------------------------------------------------------------------------- diff --git a/common/hw-gfx-gma-registers.adb b/common/hw-gfx-gma-registers.adb index c0187f6..10b02b1 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..c5fa0e7 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.Settings, + In_Out => GTT_State), + Depends => + (GTT_State =>+ (Config.Settings, 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.Settings, + In_Out => GTT_State), + Depends => + ((Device_Address, Valid, GTT_State) => + (Config.Settings, 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.ads b/common/hw-gfx-gma.ads index 7c40dd9..7f717bc 100644 --- a/common/hw-gfx-gma.ads +++ b/common/hw-gfx-gma.ads @@ -108,13 +108,20 @@ Global => (Input => Init_State); pragma Warnings (GNATprove, On, "unused variable ""Write_Delay""");
+ pragma Warnings (GNATprove, Off, "no check message justified by this", + Reason => "see Annotate aspects."); 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; + Pre => Is_Initialized, + Annotate => + (GNATprove, Intentional, + "global input ""GMA.Config_State"" of ""Power_Up_VGA"" not read", + "Reading of Config_State depends on the platform configuration."); + pragma Warnings (GNATprove, On, "no check message justified by this");
----------------------------------------------------------------------------
@@ -160,7 +167,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 +177,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 +188,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");
----------------------------------------------------------------------------
-
Nico Huber (Code Review)