Nico Huber submitted this change.

View Change

gma: Work around GNATprove issue with nested loops

Add some explicit `Loop_Invariant (True)` to work around
odd check messages. These show up since about the spark-
community-2019 release and still with newer versions,
which almost seem to hang (takes some minutes longer than
expected). Example messages are provided below. Given that
the values are in the ranges as stated by the `for` loops,
they can't be out of range.

hw-gfx-gma-plls.adb:323:14: medium: range check might fail
  323 |         for M1 in reverse M1_Range range Limits.M1_Lower .. Limits.M1_Upper
      |             ^~

hw-gfx-gma-plls.adb:325:17: medium: range check might fail
  325 |            for M2 in reverse M2_Range range Limits.M2_Lower .. Int64'Min (Limits.M2_Upper, M1)
      |                ^~

hw-gfx-gma-plls.adb:327:20: medium: range check might fail
  327 |               for P1 in reverse P1_Range range Limits.P1_Lower .. Limits.P1_Upper
      |                   ^~

hw-gfx-gma-plls.adb:332:41: medium: range check might fail
  332 |                     M2              => M2,
      |                                        ^~
  reason for check: input value must fit in parameter type

Change-Id: I5430081767c760b85401300e0db4d26fd78270d7
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/68112
Reviewed-by: Angel Pons <th3fanbus@gmail.com>
---
M common/g45/hw-gfx-gma-plls.adb
M common/ironlake/hw-gfx-gma-plls.adb
2 files changed, 4 insertions(+), 0 deletions(-)

diff --git a/common/g45/hw-gfx-gma-plls.adb b/common/g45/hw-gfx-gma-plls.adb
index 67242f2..5db76d6 100644
--- a/common/g45/hw-gfx-gma-plls.adb
+++ b/common/g45/hw-gfx-gma-plls.adb
@@ -322,8 +322,10 @@
          -- reverse loops as hardware prefers higher values
          for M1 in reverse M1_Range range Limits.M1_Lower .. Limits.M1_Upper
          loop
+            pragma Loop_Invariant (True);
             for M2 in reverse M2_Range range Limits.M2_Lower .. Int64'Min (Limits.M2_Upper, M1)
             loop
+               pragma Loop_Invariant (True);
                for P1 in reverse P1_Range range Limits.P1_Lower .. Limits.P1_Upper
                loop
                   Verify_Parameters
diff --git a/common/ironlake/hw-gfx-gma-plls.adb b/common/ironlake/hw-gfx-gma-plls.adb
index 10e9ff2..8b6ca36 100644
--- a/common/ironlake/hw-gfx-gma-plls.adb
+++ b/common/ironlake/hw-gfx-gma-plls.adb
@@ -291,8 +291,10 @@
          -- reverse loops as hardware prefers higher values
          for M1 in reverse M1_Range range Limits.M1_Lower .. Limits.M1_Upper
          loop
+            pragma Loop_Invariant (True);
             for M2 in reverse M2_Range range Limits.M2_Lower .. Limits.M2_Upper
             loop
+               pragma Loop_Invariant (True);
                for P1 in reverse P1_Range range Limits.P1_Lower .. Limits.P1_Upper
                loop
                   Verify_Parameters

To view, visit change 68112. To unsubscribe, or for help writing mail filters, visit settings.