<p>Nico Huber has uploaded this change for <strong>review</strong>.</p><p><a href="https://review.coreboot.org/27068">View Change</a></p><pre style="font-family: monospace,monospace; white-space: pre-wrap;">[WIP]gma config: Make Config.CPU and Config.CPU_Var variable<br><br>Change-Id: If409b5afbd975f3a42e28ff191a092f89ece5ae2<br>Signed-off-by: Nico Huber <nico.h@gmx.de><br>---<br>M common/Makefile.inc<br>M common/hw-gfx-gma-config.ads.template<br>M common/hw-gfx-gma-registers.adb<br>M common/hw-gfx-gma-registers.ads<br>M common/hw-gfx-gma.ads<br>5 files changed, 91 insertions(+), 17 deletions(-)<br><br></pre><pre style="font-family: monospace,monospace; white-space: pre-wrap;">git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/68/27068/1</pre><pre style="font-family: monospace,monospace; white-space: pre-wrap;"><span>diff --git a/common/Makefile.inc b/common/Makefile.inc</span><br><span>index 5eeba41..b840b1d 100644</span><br><span>--- a/common/Makefile.inc</span><br><span>+++ b/common/Makefile.inc</span><br><span>@@ -45,13 +45,41 @@</span><br><span> gfxinit-y += hw-gfx-framebuffer_filler.adb</span><br><span> gfxinit-y += hw-gfx-framebuffer_filler.ads</span><br><span> </span><br><span style="color: hsl(120, 100%, 40%);">+CONFIG_GFX_GMA_GENERATION := $(call strip_quotes,$(CONFIG_GFX_GMA_GENERATION))</span><br><span> CONFIG_GFX_GMA_CPU := $(call strip_quotes,$(CONFIG_GFX_GMA_CPU))</span><br><span> CONFIG_GFX_GMA_CPU_VARIANT := $(call strip_quotes,$(CONFIG_GFX_GMA_CPU_VARIANT))</span><br><span> CONFIG_GFX_GMA_INTERNAL_PORT := $(call strip_quotes,$(CONFIG_GFX_GMA_INTERNAL_PORT))</span><br><span> CONFIG_GFX_GMA_ANALOG_I2C_PORT := $(call strip_quotes,$(CONFIG_GFX_GMA_ANALOG_I2C_PORT))</span><br><span> </span><br><span style="color: hsl(120, 100%, 40%);">+_GEN_NONCONST := $(strip \</span><br><span style="color: hsl(120, 100%, 40%);">+ $(if $(filter Ironlake,$(CONFIG_GFX_GMA_GENERATION)),ilk, \</span><br><span style="color: hsl(120, 100%, 40%);">+ $(if $(filter Haswell,$(CONFIG_GFX_GMA_GENERATION)),hsw, \</span><br><span style="color: hsl(120, 100%, 40%);">+ $(if $(filter Skylake,$(CONFIG_GFX_GMA_GENERATION)),skl))))</span><br><span style="color: hsl(120, 100%, 40%);">+# GNATprove (GPL 2017) doesn't realize when a boolean expression</span><br><span style="color: hsl(120, 100%, 40%);">+# that depends both on static values and variables can be evalu-</span><br><span style="color: hsl(120, 100%, 40%);">+# ated at compile time (e.g. `False and Variable` is always `False`</span><br><span style="color: hsl(120, 100%, 40%);">+# and GNAT acts appropriately). So for now, we generate functions</span><br><span style="color: hsl(120, 100%, 40%);">+# instead of constant expressions for these mixed expressions.</span><br><span style="color: hsl(120, 100%, 40%);">+_GEN_CONST_TARGET := <cpufunc> # set to <genconst> to generate constants.</span><br><span style="color: hsl(120, 100%, 40%);">+</span><br><span> hw-gfx-gma-config-ads := $(subst //,/,$(call src-to-obj,,$(dir)/hw-gfx-gma-config).ads)</span><br><span> </span><br><span style="color: hsl(120, 100%, 40%);">+ifeq ($(CONFIG_GFX_GMA_DYN_CPU),y)</span><br><span style="color: hsl(120, 100%, 40%);">+$(hw-gfx-gma-config-ads): $(dir)/hw-gfx-gma-config.ads.template $(cnf)</span><br><span style="color: hsl(120, 100%, 40%);">+ printf " GENERATE $(patsubst /%,%,$(subst $(obj)/,,$@))\n"</span><br><span style="color: hsl(120, 100%, 40%);">+ sed -e's/<<GEN>>/$(CONFIG_GFX_GMA_GENERATION)/' \</span><br><span style="color: hsl(120, 100%, 40%);">+ -e's/<<INTERNAL_PORT>>/$(CONFIG_GFX_GMA_INTERNAL_PORT)/' \</span><br><span style="color: hsl(120, 100%, 40%);">+ -e's/<<ANALOG_I2C_PORT>>/$(CONFIG_GFX_GMA_ANALOG_I2C_PORT)/' \</span><br><span style="color: hsl(120, 100%, 40%);">+ -e's/<<DEFAULT_MMIO_BASE>>/$(CONFIG_GFX_GMA_DEFAULT_MMIO)/' \</span><br><span style="color: hsl(120, 100%, 40%);">+ -e'/constant Gen_CPU\(_Var\)\?/d' \</span><br><span style="color: hsl(120, 100%, 40%);">+ -e's/<\(\(gen\|ilk\|hsw\|skl\)\(...\)\?\)bool>/<\1const> Boolean/' \</span><br><span style="color: hsl(120, 100%, 40%);">+ $(if $(_GEN_NONCONST),-e's/<\(...\)\?$(_GEN_NONCONST)\(...\)\?const>/<cpufunc>/') \</span><br><span style="color: hsl(120, 100%, 40%);">+ -e's/<\(ilk\|hsw\|skl\)\(...\)\?const>/$(_GEN_CONST_TARGET)/' \</span><br><span style="color: hsl(120, 100%, 40%);">+ -e's/<genconst>/constant/' \</span><br><span style="color: hsl(120, 100%, 40%);">+ -e's/\(.*: *<cpufunc>.*:=\) *\(.*\);/\1\n (\2);/' \</span><br><span style="color: hsl(120, 100%, 40%);">+ -e's/\([^ ]\+\) *: *<cpufunc> \+\([^ ]*\) *:=/function \1 return \2 is/' \</span><br><span style="color: hsl(120, 100%, 40%);">+ $< >$@</span><br><span style="color: hsl(120, 100%, 40%);">+else</span><br><span> $(hw-gfx-gma-config-ads): $(dir)/hw-gfx-gma-config.ads.template $(cnf)</span><br><span> printf " GENERATE $(patsubst /%,%,$(subst $(obj)/,,$@))\n"</span><br><span> sed -e's/<<GEN>>/$(CONFIG_GFX_GMA_GENERATION)/' \</span><br><span>@@ -60,9 +88,11 @@</span><br><span> -e's/<<INTERNAL_PORT>>/$(CONFIG_GFX_GMA_INTERNAL_PORT)/' \</span><br><span> -e's/<<ANALOG_I2C_PORT>>/$(CONFIG_GFX_GMA_ANALOG_I2C_PORT)/' \</span><br><span> -e's/<<DEFAULT_MMIO_BASE>>/$(CONFIG_GFX_GMA_DEFAULT_MMIO)/' \</span><br><span style="color: hsl(120, 100%, 40%);">+ -e'/Dyn_CPU\(_Var\)\?/d' \</span><br><span> -e's/<\(gen\|\(ilk\|hsw\|skl\)\(...\)\?\)const>/constant/' \</span><br><span> -e's/<\(gen\|\(ilk\|hsw\|skl\)\(...\)\?\)bool>/constant Boolean/' \</span><br><span> $< >$@</span><br><span style="color: hsl(120, 100%, 40%);">+endif</span><br><span> gfxinit-gen-y += $(hw-gfx-gma-config-ads)</span><br><span> </span><br><span> ifneq ($(filter G45,$(CONFIG_GFX_GMA_CPU)),)</span><br><span>diff --git a/common/hw-gfx-gma-config.ads.template b/common/hw-gfx-gma-config.ads.template</span><br><span>index 03f343b..fa62890 100644</span><br><span>--- a/common/hw-gfx-gma-config.ads.template</span><br><span>+++ b/common/hw-gfx-gma-config.ads.template</span><br><span>@@ -60,15 +60,22 @@</span><br><span> type Settings_T is record</span><br><span> Valid_Port : Valid_Port_Array;</span><br><span> Raw_Clock : Frequency_Type;</span><br><span style="color: hsl(120, 100%, 40%);">+ Dyn_CPU : Gen_CPU_Type;</span><br><span style="color: hsl(120, 100%, 40%);">+ Dyn_CPU_Var : Gen_CPU_Variant;</span><br><span> end record;</span><br><span> Initial_Settings : constant Settings_T :=</span><br><span> (Valid_Port => (others => False),</span><br><span style="color: hsl(0, 100%, 40%);">- Raw_Clock => Frequency_Type'First);</span><br><span style="color: hsl(120, 100%, 40%);">+ Raw_Clock => Frequency_Type'First</span><br><span style="color: hsl(120, 100%, 40%);">+ ,Dyn_CPU => Gen_CPU_Type'First</span><br><span style="color: hsl(120, 100%, 40%);">+ ,Dyn_CPU_Var => Gen_CPU_Variant'First</span><br><span style="color: hsl(120, 100%, 40%);">+ );</span><br><span> </span><br><span> Settings : Settings_T with Part_Of => GMA.Config_State;</span><br><span> </span><br><span> Valid_Port : Valid_Port_Array renames Settings.Valid_Port;</span><br><span> Raw_Clock : Frequency_Type renames Settings.Raw_Clock;</span><br><span style="color: hsl(120, 100%, 40%);">+ CPU : Gen_CPU_Type renames Settings.Dyn_CPU;</span><br><span style="color: hsl(120, 100%, 40%);">+ CPU_Var : Gen_CPU_Variant renames Settings.Dyn_CPU_Var;</span><br><span> </span><br><span> ----------------------------------------------------------------------------</span><br><span> </span><br><span>@@ -288,12 +295,12 @@</span><br><span> </span><br><span> ----------------------------------------------------------------------------</span><br><span> </span><br><span style="color: hsl(0, 100%, 40%);">- GTT_PTE_Size : <hswconst> := (if Has_64bit_GTT then 8 else 4);</span><br><span style="color: hsl(120, 100%, 40%);">+ GTT_PTE_Size : <hswconst> Natural := (if Has_64bit_GTT then 8 else 4);</span><br><span> </span><br><span style="color: hsl(0, 100%, 40%);">- Fence_Base : <ilkconst> :=</span><br><span style="color: hsl(120, 100%, 40%);">+ Fence_Base : <ilkconst> Natural :=</span><br><span> (if not Sandybridge_Plus then 16#0000_3000# else 16#0010_0000#);</span><br><span> </span><br><span style="color: hsl(0, 100%, 40%);">- Fence_Count : <ilkconst> :=</span><br><span style="color: hsl(120, 100%, 40%);">+ Fence_Count : <ilkconst> Natural :=</span><br><span> (if not Ivybridge_Plus then 16 else 32);</span><br><span> </span><br><span> ----------------------------------------------------------------------------</span><br><span>diff --git a/common/hw-gfx-gma-registers.adb b/common/hw-gfx-gma-registers.adb</span><br><span>index c0187f6..10b02b1 100644</span><br><span>--- a/common/hw-gfx-gma-registers.adb</span><br><span>+++ b/common/hw-gfx-gma-registers.adb</span><br><span>@@ -16,8 +16,6 @@</span><br><span> with HW.MMIO_Range;</span><br><span> pragma Elaborate_All (HW.MMIO_Range);</span><br><span> </span><br><span style="color: hsl(0, 100%, 40%);">-with HW.GFX.GMA.Config;</span><br><span style="color: hsl(0, 100%, 40%);">-</span><br><span> with HW.Debug;</span><br><span> with GNAT.Source_Info;</span><br><span> </span><br><span>diff --git a/common/hw-gfx-gma-registers.ads b/common/hw-gfx-gma-registers.ads</span><br><span>index 3be2ec7..c5fa0e7 100644</span><br><span>--- a/common/hw-gfx-gma-registers.ads</span><br><span>+++ b/common/hw-gfx-gma-registers.ads</span><br><span>@@ -14,6 +14,7 @@</span><br><span> </span><br><span> with System;</span><br><span> with HW.GFX.GMA;</span><br><span style="color: hsl(120, 100%, 40%);">+with HW.GFX.GMA.Config;</span><br><span> </span><br><span> private package HW.GFX.GMA.Registers</span><br><span> with</span><br><span>@@ -1720,21 +1721,39 @@</span><br><span> </span><br><span> procedure Remove_Fence (First_Page, Last_Page : GTT_Range);</span><br><span> </span><br><span style="color: hsl(120, 100%, 40%);">+ pragma Warnings (GNATprove, Off, "no check message justified by this",</span><br><span style="color: hsl(120, 100%, 40%);">+ Reason => "see Annotate aspects.");</span><br><span> procedure Write_GTT</span><br><span> (GTT_Page : GTT_Range;</span><br><span> Device_Address : GTT_Address_Type;</span><br><span> Valid : Boolean)</span><br><span> with</span><br><span style="color: hsl(0, 100%, 40%);">- Global => (In_Out => GTT_State),</span><br><span style="color: hsl(0, 100%, 40%);">- Depends => (GTT_State =>+ (GTT_Page, Device_Address, Valid));</span><br><span style="color: hsl(120, 100%, 40%);">+ Global =></span><br><span style="color: hsl(120, 100%, 40%);">+ (Input => Config.Settings,</span><br><span style="color: hsl(120, 100%, 40%);">+ In_Out => GTT_State),</span><br><span style="color: hsl(120, 100%, 40%);">+ Depends =></span><br><span style="color: hsl(120, 100%, 40%);">+ (GTT_State =>+ (Config.Settings, GTT_Page, Device_Address, Valid)),</span><br><span style="color: hsl(120, 100%, 40%);">+ Annotate =></span><br><span style="color: hsl(120, 100%, 40%);">+ (GNATprove, Intentional,</span><br><span style="color: hsl(120, 100%, 40%);">+ """GMA.Config_State"" of ""Write_GTT"" not read",</span><br><span style="color: hsl(120, 100%, 40%);">+ "Reading of Config_State depends on the platform configuration.");</span><br><span> </span><br><span> procedure Read_GTT</span><br><span> (Device_Address : out GTT_Address_Type;</span><br><span> Valid : out Boolean;</span><br><span> GTT_Page : in GTT_Range)</span><br><span> with</span><br><span style="color: hsl(0, 100%, 40%);">- Global => (In_Out => GTT_State),</span><br><span style="color: hsl(0, 100%, 40%);">- Depends => ((Device_Address, Valid, GTT_State) => (GTT_State, GTT_Page));</span><br><span style="color: hsl(120, 100%, 40%);">+ Global =></span><br><span style="color: hsl(120, 100%, 40%);">+ (Input => Config.Settings,</span><br><span style="color: hsl(120, 100%, 40%);">+ In_Out => GTT_State),</span><br><span style="color: hsl(120, 100%, 40%);">+ Depends =></span><br><span style="color: hsl(120, 100%, 40%);">+ ((Device_Address, Valid, GTT_State) =></span><br><span style="color: hsl(120, 100%, 40%);">+ (Config.Settings, GTT_State, GTT_Page)),</span><br><span style="color: hsl(120, 100%, 40%);">+ Annotate =></span><br><span style="color: hsl(120, 100%, 40%);">+ (GNATprove, Intentional,</span><br><span style="color: hsl(120, 100%, 40%);">+ """GMA.Config_State"" of ""Read_GTT"" not read",</span><br><span style="color: hsl(120, 100%, 40%);">+ "Reading of Config_State depends on the platform configuration.");</span><br><span style="color: hsl(120, 100%, 40%);">+ pragma Warnings (GNATprove, On, "no check message justified by this");</span><br><span> </span><br><span> procedure Set_Register_Base (Base : Word64; GTT_Base : Word64 := 0)</span><br><span> with</span><br><span>diff --git a/common/hw-gfx-gma.ads b/common/hw-gfx-gma.ads</span><br><span>index 7c40dd9..7f717bc 100644</span><br><span>--- a/common/hw-gfx-gma.ads</span><br><span>+++ b/common/hw-gfx-gma.ads</span><br><span>@@ -108,13 +108,20 @@</span><br><span> Global => (Input => Init_State);</span><br><span> pragma Warnings (GNATprove, On, "unused variable ""Write_Delay""");</span><br><span> </span><br><span style="color: hsl(120, 100%, 40%);">+ pragma Warnings (GNATprove, Off, "no check message justified by this",</span><br><span style="color: hsl(120, 100%, 40%);">+ Reason => "see Annotate aspects.");</span><br><span> procedure Power_Up_VGA</span><br><span> with</span><br><span> Global =></span><br><span style="color: hsl(0, 100%, 40%);">- (Input => (State, Time.State),</span><br><span style="color: hsl(120, 100%, 40%);">+ (Input => (State, Config_State, Time.State),</span><br><span> In_Out => (Device_State),</span><br><span> Proof_In => (Init_State)),</span><br><span style="color: hsl(0, 100%, 40%);">- Pre => Is_Initialized;</span><br><span style="color: hsl(120, 100%, 40%);">+ Pre => Is_Initialized,</span><br><span style="color: hsl(120, 100%, 40%);">+ Annotate =></span><br><span style="color: hsl(120, 100%, 40%);">+ (GNATprove, Intentional,</span><br><span style="color: hsl(120, 100%, 40%);">+ "global input ""GMA.Config_State"" of ""Power_Up_VGA"" not read",</span><br><span style="color: hsl(120, 100%, 40%);">+ "Reading of Config_State depends on the platform configuration.");</span><br><span style="color: hsl(120, 100%, 40%);">+ pragma Warnings (GNATprove, On, "no check message justified by this");</span><br><span> </span><br><span> ----------------------------------------------------------------------------</span><br><span> </span><br><span>@@ -160,7 +167,9 @@</span><br><span> Device_Address : GTT_Address_Type;</span><br><span> Valid : Boolean)</span><br><span> with</span><br><span style="color: hsl(0, 100%, 40%);">- Global => (In_Out => Device_State, Proof_In => Init_State),</span><br><span style="color: hsl(120, 100%, 40%);">+ Global =></span><br><span style="color: hsl(120, 100%, 40%);">+ (Input => Config_State,</span><br><span style="color: hsl(120, 100%, 40%);">+ In_Out => Device_State, Proof_In => Init_State),</span><br><span> Pre => Is_Initialized;</span><br><span> </span><br><span> procedure Read_GTT</span><br><span>@@ -168,7 +177,9 @@</span><br><span> Valid : out Boolean;</span><br><span> GTT_Page : in GTT_Range)</span><br><span> with</span><br><span style="color: hsl(0, 100%, 40%);">- Global => (In_Out => Device_State, Proof_In => Init_State),</span><br><span style="color: hsl(120, 100%, 40%);">+ Global =></span><br><span style="color: hsl(120, 100%, 40%);">+ (Input => Config_State,</span><br><span style="color: hsl(120, 100%, 40%);">+ In_Out => Device_State, Proof_In => Init_State),</span><br><span> Pre => Is_Initialized;</span><br><span> </span><br><span> procedure Setup_Default_FB</span><br><span>@@ -177,18 +188,27 @@</span><br><span> Success : out Boolean)</span><br><span> with</span><br><span> Global =></span><br><span style="color: hsl(0, 100%, 40%);">- (In_Out =></span><br><span style="color: hsl(120, 100%, 40%);">+ (Input => Config_State,</span><br><span style="color: hsl(120, 100%, 40%);">+ In_Out =></span><br><span> (State, Device_State,</span><br><span> Framebuffer_Filler.State, Framebuffer_Filler.Base_Address),</span><br><span> Proof_In => (Init_State)),</span><br><span> Pre => Is_Initialized and HW.Config.Dynamic_MMIO;</span><br><span> </span><br><span style="color: hsl(120, 100%, 40%);">+ pragma Warnings (GNATprove, Off, "no check message justified by this",</span><br><span style="color: hsl(120, 100%, 40%);">+ Reason => "see Annotate aspects.");</span><br><span> procedure Map_Linear_FB (Linear_FB : out Word64; FB : in Framebuffer_Type)</span><br><span> with</span><br><span> Global =></span><br><span style="color: hsl(0, 100%, 40%);">- (In_Out => (State, Device_State),</span><br><span style="color: hsl(120, 100%, 40%);">+ (Input => Config_State,</span><br><span style="color: hsl(120, 100%, 40%);">+ In_Out => (State, Device_State),</span><br><span> Proof_In => (Init_State)),</span><br><span style="color: hsl(0, 100%, 40%);">- Pre => Is_Initialized and HW.Config.Dynamic_MMIO;</span><br><span style="color: hsl(120, 100%, 40%);">+ Pre => Is_Initialized and HW.Config.Dynamic_MMIO,</span><br><span style="color: hsl(120, 100%, 40%);">+ Annotate =></span><br><span style="color: hsl(120, 100%, 40%);">+ (GNATprove, Intentional,</span><br><span style="color: hsl(120, 100%, 40%);">+ "global input ""GMA.Config_State"" of ""Map_Linear_FB"" not read",</span><br><span style="color: hsl(120, 100%, 40%);">+ "Reading of Config_State depends on the platform configuration.");</span><br><span style="color: hsl(120, 100%, 40%);">+ pragma Warnings (GNATprove, On, "no check message justified by this");</span><br><span> </span><br><span> ----------------------------------------------------------------------------</span><br><span> </span><br><span></span><br></pre><p>To view, visit <a href="https://review.coreboot.org/27068">change 27068</a>. To unsubscribe, or for help writing mail filters, visit <a href="https://review.coreboot.org/settings">settings</a>.</p><div itemscope itemtype="http://schema.org/EmailMessage"><div itemscope itemprop="action" itemtype="http://schema.org/ViewAction"><link itemprop="url" href="https://review.coreboot.org/27068"/><meta itemprop="name" content="View Change"/></div></div>
<div style="display:none"> Gerrit-Project: libgfxinit </div>
<div style="display:none"> Gerrit-Branch: master </div>
<div style="display:none"> Gerrit-MessageType: newchange </div>
<div style="display:none"> Gerrit-Change-Id: If409b5afbd975f3a42e28ff191a092f89ece5ae2 </div>
<div style="display:none"> Gerrit-Change-Number: 27068 </div>
<div style="display:none"> Gerrit-PatchSet: 1 </div>
<div style="display:none"> Gerrit-Owner: Nico Huber <nico.h@gmx.de> </div>