Nico Huber has posted comments on this change. ( https://review.coreboot.org/c/libgfxinit/+/35869 )
Change subject: dp_info: read eDP 1.4+ DPCD link rates ......................................................................
Patch Set 1:
(12 comments)
Hi Greg, thanks for your patch. I wasn't sure if I should expect any :D
As you might have noticed, libgfxinit is written in SPARK, which requires a tool (GNATprove) to be run over the source to check for certain errors. If you mind, I can do that for you and report back any problem. But that might be the slow road. If you want to try for yourself, you can follow the README.md instructions for a standalone build of libgfxinit. Alas, I haven't documented these further steps: o Install GNATprove (or download the prebuilt package from libre.adacore.com, e.g. spark-discovery-gpl-2017-x86_64-linux-bin.tar.gz) Haven't tried anything newish lately, because it was borked in 2018 :-/ o Run it for one config, e.g. make cnf=configs/skylake full or all of them make -j proof-allconfigs
https://review.coreboot.org/c/libgfxinit/+/35869/1//COMMIT_MSG Commit Message:
https://review.coreboot.org/c/libgfxinit/+/35869/1//COMMIT_MSG@12 PS1, Line 12: (And higher rate is required because the panel is high res.) The high resolution is actually unrelated. libgfxinit could as well bail out on the 0x00.
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb File common/hw-gfx-dp_info.adb:
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 102: Success : out Boolean) What's the intended meaning of `Success` here? The result seems to be ignored later...
As the whole part is optional, I think we could live without it. Or, at least, only report a failure if we could read the eDP revision, it is >= 1.4, and then failed to read the rates. i.e. `Success = failed_to_read_0x700 or < 3 or succeeded to read 0x10`
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 106: Max_Rate : Word32; An Integer type, e.g. `Natural`, would be preferred. GNATprove could check that we don't overflow any calculation.
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 109: Rates_Size : constant := 8; Linux's i915 reads up to 8 rates, thus 16 bytes.
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 120: Success := Success and Length = Caps_Size; I guess I understand now how you interpret `Success`. You think it's kind the summed up result of all steps?
However, as `Success` is usually an `out` parameter, the next call to Aux_Read() will overwrite any previous value, i.e. if reading 0x700 fails, but reading at 0x10 works, `Success` would be true.
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 122: 16#03# We might want to give this a name, e.g. `eDP_Rev_1_4 : constant := 3;`, it's not obvious that it's the eDP revision that is checked.
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 122: Length = Caps_Size Better check `Success` here instead of repeating `Length = Caps_Size`.
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 132: Length = Rates_Size Same here, better check `Success`.
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 142: end if; I would prefer a loop, especially considering the 8 rates.
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 146: 540000 Nit, numbers could be written as `540_000` etc., makes it easier to review :)
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 152: end if; Please leave a comment here, that this actually needs support for individual (instead of a maximum) rates in libgfxinit. Just using the maximum should cover 99% of the use cases, so I'm ok with the current solution.
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-gma-connect... File common/hw-gfx-gma-connector_info.adb:
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-gma-connect... PS1, Line 57: Success => Success); Could we make the call part of Read_Caps() instead?