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? > > 'info.offset' to verifier log? E.g. via some 'illegal' action. > Yes if necessary!
