Andrii Nakryiko wrote:
> Currently the way that verifier prints SCALAR_VALUE register state (and
> PTR_TO_PACKET, which can have var_off and ranges info as well) is very
> ambiguous.
>
> In the name of brevity we are trying to eliminate "unnecessary" output
> of umin/umax, smin/smax, u32_min/u32_max, and s32_min/s32_max values, if
> possible. Current rules are that if any of those have their default
> value (which for mins is the minimal value of its respective types: 0,
> S32_MIN, or S64_MIN, while for maxs it's U32_MAX, S32_MAX, S64_MAX, or
> U64_MAX) *OR* if there is another min/max value that as matching value.
> E.g., if smin=100 and umin=100, we'll emit only umin=10, omitting smin
> altogether. This approach has a few problems, being both ambiguous and
> sort-of incorrect in some cases.
>
> Ambiguity is due to missing value could be either default value or value
> of umin/umax or smin/smax. This is especially confusing when we mix
> signed and unsigned ranges. Quite often, umin=0 and smin=0, and so we'll
> have only `umin=0` leaving anyone reading verifier log to guess whether
> smin is actually 0 or it's actually -9223372036854775808 (S64_MIN). And
> often times it's important to know, especially when debugging tricky
> issues.
+1
>
> "Sort-of incorrectness" comes from mixing negative and positive values.
> E.g., if umin is some large positive number, it can be equal to smin
> which is, interpreted as signed value, is actually some negative value.
> Currently, that smin will be omitted and only umin will be emitted with
> a large positive value, giving an impression that smin is also positive.
>
> Anyway, ambiguity is the biggest issue making it impossible to have an
> exact understanding of register state, preventing any sort of automated
> testing of verifier state based on verifier log. This patch is
> attempting to rectify the situation by removing ambiguity, while
> minimizing the verboseness of register state output.
>
> The rules are straightforward:
> - if some of the values are missing, then it definitely has a default
> value. I.e., `umin=0` means that umin is zero, but smin is actually
> S64_MIN;
> - all the various boundaries that happen to have the same value are
> emitted in one equality separated sequence. E.g., if umin and smin are
> both 100, we'll emit `smin=umin=100`, making this explicit;
> - we do not mix negative and positive values together, and even if
> they happen to have the same bit-level value, they will be emitted
> separately with proper sign. I.e., if both umax and smax happen to be
> 0xffffffffffffffff, we'll emit them both separately as
> `smax=-1,umax=18446744073709551615`;
> - in the name of a bit more uniformity and consistency,
> {u32,s32}_{min,max} are renamed to {s,u}{min,max}32, which seems to
> improve readability.
agree.
>
> The above means that in case of all 4 ranges being, say, [50, 100] range,
> we'd previously see hugely ambiguous:
>
> R1=scalar(umin=50,umax=100)
>
> Now, we'll be more explicit:
>
> R1=scalar(smin=umin=smin32=umin32=50,smax=umax=smax32=umax32=100)
>
> This is slightly more verbose, but distinct from the case when we don't
> know anything about signed boundaries and 32-bit boundaries, which under
> new rules will match the old case:
>
> R1=scalar(umin=50,umax=100)
Did you consider perhaps just always printing the entire set? Its overly
verbose I guess but I find it easier to track state across multiple
steps this way.
Otherwise patch LGTM.
