On 5/10/24 15:57, Eduard Zingerman wrote:
On Fri, 2024-05-10 at 15:53 -0700, Kui-Feng Lee wrote:
[...]
Do you mean checking index in the way like the following code?
if (array[0] != ref0 || array[1] != ref1 || array[2] != ref2 ....)
return err;
Probably, but I'd need your help here.
There goal is to verify that offsets of __kptr's in the 'info' array
had been set correctly. Where is this information is used later on?
E.g. I'd like to trigger some action that "touches" __kptr at index N
and verify that all others had not been "touched".
But this "touch" action has to use offset stored in the 'info'.
They are used for verifying the offset of instructions.
Let's assume we have an array of size 10.
Then, we have 10 infos with 10 different offsets.
And, we have a program includes one instruction for each element, 10 in
total, to access the corresponding element.
Each instruction has an offset different from others, generated by the
compiler. That means the verifier will fail to find an info for some of
instructions if there is one or more info having wrong offset.
That's a bit depressing, as there would be no way to check if e.g. all
10 refer to the same offset. Is it possible to trigger printing of the
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
How can that happen? Do you mean the compiler does it wrong?
No, suppose that 'info.offset' is computed incorrectly because of some
bug in arrays handling. E.g. all .off fields in the infos have the
same value.
What is the shape of the test that could catch such bug?
I am not sure if I read you question correctly.
For example, we have 3 correct info.
[info(offset=0x8), info(offset=0x10), info(offset=0x18)]
And We have program that includes 3 instructions to access the offset
0x8, 0x10, and 0x18. (let's assume these load instructions would be
checked against infos)
load r1, [0x8]
load r1, [0x10]
load r1, [0x18]
If everything works as expected, the verifier would accept the program.
Otherwise, like you said, all 3 info are pointing to the same offset.
[info(0offset=0x8), info(offset=0x8), info(offset=0x8)]
Then, the later two instructions should fail the check.
'info.offset' to verifier log? E.g. via some 'illegal' action.
Yes if necessary!
