Change in ...libgfxinit[master]: gma config: Make Config.CPU and Config.CPU_Var variable

[Nico Huber (Code Review)]

Nico Huber has submitted this change and it was merged. ( https://review.coreboot.org/c/libgfxinit/+/27068 )

Change subject: gma config: Make Config.CPU and Config.CPU_Var variable
......................................................................

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 
Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/27068
Reviewed-by: Angel Pons 
Reviewed-by: Patrick Georgi 
---
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.adb
M common/hw-gfx-gma.ads
6 files changed, 86 insertions(+), 19 deletions(-)

Approvals:
  Nico Huber: Verified
  Patrick Georgi: Looks good to me, approved
  Angel Pons: Looks good to me, but someone else must approve

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");

----------------------------------------------------------------------------