On Wed, May 3, 2023 at 7:55 PM Alexei Starovoitov
<alexei.starovoitov@xxxxxxxxx> wrote:
>
> On Tue, Apr 25, 2023 at 04:49:05PM -0700, Andrii Nakryiko wrote:
> > Add helper to format register and stack masks in more human-readable
> > format. Adjust logging a bit during backtrack propagation and especially
> > during forcing precision fallback logic to make it clearer what's going
> > on (with log_level=2, of course), and also start reporting affected
> > frame depth. This is in preparation for having more than one active
> > frame later when precision propagation between subprog calls is added.
> >
> > Signed-off-by: Andrii Nakryiko <andrii@xxxxxxxxxx>
> > ---
> > include/linux/bpf_verifier.h | 13 ++-
> > kernel/bpf/verifier.c | 72 ++++++++++--
> > .../testing/selftests/bpf/verifier/precise.c | 106 +++++++++---------
> > 3 files changed, 128 insertions(+), 63 deletions(-)
> >
> > diff --git a/include/linux/bpf_verifier.h b/include/linux/bpf_verifier.h
> > index 185bfaf0ec6b..0ca367e13dd8 100644
> > --- a/include/linux/bpf_verifier.h
> > +++ b/include/linux/bpf_verifier.h
> > @@ -18,8 +18,11 @@
> > * that converting umax_value to int cannot overflow.
> > */
> > #define BPF_MAX_VAR_SIZ (1 << 29)
> > -/* size of type_str_buf in bpf_verifier. */
> > -#define TYPE_STR_BUF_LEN 128
> > +/* size of tmp_str_buf in bpf_verifier.
> > + * we need at least 306 bytes to fit full stack mask representation
> > + * (in the "-8,-16,...,-512" form)
> > + */
> > +#define TMP_STR_BUF_LEN 320
> >
> > /* Liveness marks, used for registers and spilled-regs (in stack slots).
> > * Read marks propagate upwards until they find a write mark; they record that
> > @@ -621,8 +624,10 @@ struct bpf_verifier_env {
> > /* Same as scratched_regs but for stack slots */
> > u64 scratched_stack_slots;
> > u64 prev_log_pos, prev_insn_print_pos;
> > - /* buffer used in reg_type_str() to generate reg_type string */
> > - char type_str_buf[TYPE_STR_BUF_LEN];
> > + /* buffer used to generate temporary string representations,
> > + * e.g., in reg_type_str() to generate reg_type string
> > + */
> > + char tmp_str_buf[TMP_STR_BUF_LEN];
> > };
> >
> > __printf(2, 0) void bpf_verifier_vlog(struct bpf_verifier_log *log,
> > diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> > index 1cb89fe00507..8faf9170acf0 100644
> > --- a/kernel/bpf/verifier.c
> > +++ b/kernel/bpf/verifier.c
> > @@ -604,9 +604,9 @@ static const char *reg_type_str(struct bpf_verifier_env *env,
> > type & PTR_TRUSTED ? "trusted_" : ""
> > );
> >
> > - snprintf(env->type_str_buf, TYPE_STR_BUF_LEN, "%s%s%s",
> > + snprintf(env->tmp_str_buf, TMP_STR_BUF_LEN, "%s%s%s",
> > prefix, str[base_type(type)], postfix);
> > - return env->type_str_buf;
> > + return env->tmp_str_buf;
> > }
> >
> > static char slot_type_char[] = {
> > @@ -3275,6 +3275,45 @@ static inline bool bt_is_slot_set(struct backtrack_state *bt, u32 slot)
> > return bt->stack_masks[bt->frame] & (1ull << slot);
> > }
> >
> > +/* format registers bitmask, e.g., "r0,r2,r4" for 0x15 mask */
> > +static void fmt_reg_mask(char *buf, ssize_t buf_sz, u32 reg_mask)
> > +{
> > + DECLARE_BITMAP(mask, 64);
> > + bool first = true;
> > + int i, n;
> > +
> > + buf[0] = '\0';
> > +
> > + bitmap_from_u64(mask, reg_mask);
> > + for_each_set_bit(i, mask, 32) {
> > + n = snprintf(buf, buf_sz, "%sr%d", first ? "" : ",", i);
> > + first = false;
> > + buf += n;
> > + buf_sz -= n;
> > + if (buf_sz < 0)
> > + break;
> > + }
> > +}
> > +/* format stack slots bitmask, e.g., "-8,-24,-40" for 0x15 mask */
> > +static void fmt_stack_mask(char *buf, ssize_t buf_sz, u64 stack_mask)
> > +{
> > + DECLARE_BITMAP(mask, 64);
> > + bool first = true;
> > + int i, n;
> > +
> > + buf[0] = '\0';
> > +
> > + bitmap_from_u64(mask, stack_mask);
> > + for_each_set_bit(i, mask, 64) {
> > + n = snprintf(buf, buf_sz, "%s%d", first ? "" : ",", -(i + 1) * 8);
> > + first = false;
> > + buf += n;
> > + buf_sz -= n;
> > + if (buf_sz < 0)
> > + break;
> > + }
> > +}
> > +
> > /* For given verifier state backtrack_insn() is called from the last insn to
> > * the first insn. Its purpose is to compute a bitmask of registers and
> > * stack slots that needs precision in the parent verifier state.
> > @@ -3298,7 +3337,11 @@ static int backtrack_insn(struct bpf_verifier_env *env, int idx,
> > if (insn->code == 0)
> > return 0;
> > if (env->log.level & BPF_LOG_LEVEL2) {
> > - verbose(env, "regs=%x stack=%llx before ", bt_reg_mask(bt), bt_stack_mask(bt));
> > + fmt_reg_mask(env->tmp_str_buf, TMP_STR_BUF_LEN, bt_reg_mask(bt));
> > + verbose(env, "mark_precise: frame%d: regs(0x%x)=%s ",
> > + bt->frame, bt_reg_mask(bt), env->tmp_str_buf);
> > + fmt_stack_mask(env->tmp_str_buf, TMP_STR_BUF_LEN, bt_stack_mask(bt));
> > + verbose(env, "stack(0x%llx)=%s before ", bt_stack_mask(bt), env->tmp_str_buf);
>
> Let's drop (0x%llx) part from regs and stack.
> With nice human readable addition no one will be reading the hex anymore.
> It's just wasting screen real estate.
ack, will drop
>
> > + "mark_precise: frame0: last_idx 26 first_idx 20\
> > + mark_precise: frame0: regs(0x4)=r2 stack(0x0)= before 25\
> > + mark_precise: frame0: regs(0x4)=r2 stack(0x0)= before 24\
> > + mark_precise: frame0: regs(0x4)=r2 stack(0x0)= before 23\
> > + mark_precise: frame0: regs(0x4)=r2 stack(0x0)= before 22\
> > + mark_precise: frame0: regs(0x4)=r2 stack(0x0)= before 20\
> > + parent didn't have regs=4 stack=0 marks:\
> > + mark_precise: frame0: last_idx 19 first_idx 10\
> > + mark_precise: frame0: regs(0x4)=r2 stack(0x0)= before 19\
> > + mark_precise: frame0: regs(0x200)=r9 stack(0x0)= before 18\
> > + mark_precise: frame0: regs(0x300)=r8,r9 stack(0x0)= before 17\
> > + mark_precise: frame0: regs(0x201)=r0,r9 stack(0x0)= before 15\
> > + mark_precise: frame0: regs(0x201)=r0,r9 stack(0x0)= before 14\
> > + mark_precise: frame0: regs(0x200)=r9 stack(0x0)= before 13\
> > + mark_precise: frame0: regs(0x200)=r9 stack(0x0)= before 12\
> > + mark_precise: frame0: regs(0x200)=r9 stack(0x0)= before 11\
> > + mark_precise: frame0: regs(0x200)=r9 stack(0x0)= before 10\
> > + parent already had regs=0 stack=0 marks:",
>
> This part would be much cleaner without (0x...)
