[coreboot-gerrit] Change in libgfxinit[master]: [WIP]gma config: Make Config.CPU and Config.CPU_Var variable
Nico Huber (Code Review)
gerrit at coreboot.org
Wed Jun 13 01:27:45 CEST 2018
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 at 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");
----------------------------------------------------------------------------
--
To view, visit https://review.coreboot.org/27068
To unsubscribe, or for help writing mail filters, visit https://review.coreboot.org/settings
Gerrit-Project: libgfxinit
Gerrit-Branch: master
Gerrit-MessageType: newchange
Gerrit-Change-Id: If409b5afbd975f3a42e28ff191a092f89ece5ae2
Gerrit-Change-Number: 27068
Gerrit-PatchSet: 1
Gerrit-Owner: Nico Huber <nico.h at gmx.de>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.coreboot.org/pipermail/coreboot-gerrit/attachments/20180612/2c6e0755/attachment-0001.html>
More information about the coreboot-gerrit
mailing list