On Tue, 2025-03-11 at 20:13 -0700, Eduard Zingerman wrote:
> Suppose the verifier state exploration graph looks as follows:
>
> .-> A --. Suppose:
> | | | - state A is at iterator 'next';
> | v v - path A -> B -> A is verified first;
> '-- B C - path A -> C is verified next;
> - B does not impose a read mark for register R1;
> - C imposes a read mark for register R1;
>
> Under such conditions:
> - when B is explored and A is identified as its loop entry, the read
> marks are copied from A to B by propagate_liveness(), but these
> marks do not include R1;
> - when C is explored, the read mark for R1 is propagated to A,
> but not to B.
> - at this point, state A has its branch count at zero, but state
> B has incomplete read marks.
>
> The same logic applies to precision marks.
> This means that states with a loop entry can have incomplete read and
> precision marks, regardless of whether the loop entry itself has
> branches.
Which makes me wonder.
If read/precision marks for B are not final and some state D outside
of the loop becomes equal to B, the read/precision marks for that
state would be incomplete as well:
D------. // as some read/precision marks are missing from C
| // propagate_liveness() won't copy all necessary
.-> A --. | // marks to D.
| | | |
| v v |
'-- B C |
^ |
'------'
This makes comparison with 'loop_entry' states contagious,
propagating incomplete read/precision mark flag up to the root state.
This will have verification performance implications.
Alternatively read/precision marks need to be propagated in the state
graph until fixed point is reached. Like with DFA analysis.
Решето.
> The current verification logic does not account for this. An example
> of an unsafe program accepted by the verifier is the selftest included
> in the next patch.
[...]
