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 2:
(6 comments)
Now using early returns with the success thing.
Thanks for the update :)
As for SPARK, the 'full' make target with spark-discovery-gpl-2017 spews a ton of warnings from all around the project. For new code, it says
hw-gfx-dp_info.adb:147:58: medium: range check might fail, in instantiation at hw-gfx-gma-dp_info.ads:19 hw-gfx-dp_info.adb:147:58: medium: overflow check might fail, in instantiation at hw-gfx-gma-dp_info.ads:19 hw-gfx-dp_info.adb:163:28: medium: range check might fail, in instantiation at hw-gfx-gma-dp_info.ads:19 hw-gfx-dp_info.adb:163:28: medium: overflow check might fail, in instantiation at hw-gfx-gma-dp_info.ads:19which seems silly, it can't prove that the constants from the 0..7 range multiplied by 2 fit into the Aux_Payload_Index.
That's silly indeed. I assume the other ton of warnings is too, there shouldn't be any. Maybe GNATprove has trouble finding the theorem prover. We currently have `z3` hardcoded. Maybe it can't find it or something is wrong with its installation *shrug*
I left comments on the three lines it spat out for me. That's quite impressive btw. only 3 for nearly 100 new lines \o/
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.)
But it didn't, it read this as the minimum speed..
Yes, well, that it tries the lower rate at all is libgfxinit specific. Reading the above just made me wonder: max link rate is 0x00 and it needs something higher? ofc, it needs something higher than 0.
Anyway, it just made me stumble a little, when I read it.
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... […]
Thinking about this again. I would just make it a local variable. Return early on errors, but don't propagate the error.
Also, currently we have:
hw-gfx-gma-connector_info.adb:57:28: warning: unused assignment to "Success"
Because we ignore the result anyway.
https://review.coreboot.org/c/libgfxinit/+/35869/2/common/hw-gfx-dp_info.adb File common/hw-gfx-dp_info.adb:
https://review.coreboot.org/c/libgfxinit/+/35869/2/common/hw-gfx-dp_info.adb... PS2, Line 93: return Word16 We should add a precondition here for `Offset`. As we read 2 bytes, we'll need some margin at the end:
with Pre => Offset < DP_Defs.Aux_Payload_Index'Last
Without this, we get for the `Offset + 1` below:
hw-gfx-dp_info.adb:96:54: medium: array index check might fail, in instantiation at hw-gfx-gma-dp_info.ads:19
https://review.coreboot.org/c/libgfxinit/+/35869/2/common/hw-gfx-dp_info.adb... PS2, Line 134: Success := Success and Length = Rates_Size; Alternatively, we can use the resulting `Length` to limit the loop below...
https://review.coreboot.org/c/libgfxinit/+/35869/2/common/hw-gfx-dp_info.adb... PS2, Line 145: for I in 0 .. 7 loop e.g.
for I in 0 .. Length / 2 - 1 loop
https://review.coreboot.org/c/libgfxinit/+/35869/2/common/hw-gfx-dp_info.adb... PS2, Line 158: end; You were correct that loops are a little special. GNATprove doesn't track all available information across the iterations. But we need to know that `Max_Rate` doesn't get to big:
pragma Loop_Invariant (Max_Rate <= Natural (Word16'Last));
Otherwise, we can't prove that the `Max_Rate * 20` below doesn't overflow:
hw-gfx-dp_info.adb:163:28: medium: overflow check might fail, in instantiation at hw-gfx-gma-dp_info.ads:19