On Mar 20, 2024, at 7:46 AM, Shung-Hsi Yu <shung-hsi.yu@xxxxxxxx> wrote: > >> following assumptions: we only consider parts of the verifier concerned with >> range analysis (that is, the part that updates u/smin, u/smax, and tnums in >> bpf_reg_state), we only consider scalar types (SCALAR_VALUE) in bpf registers, >> we assume Agni's translation of the verifier's C code to logic (SMT) is correct. > > Q: looking at README in Agni's repo both the 64-bit and 32-bit u/smin > u/smax gets verified, is that right? Yes, that’s correct. Agni verifies the range tracking in u32/s32 min/max, u64/s64 min/max, and tnums.
