Commit d9439c21 authored by Andrii Nakryiko's avatar Andrii Nakryiko Committed by Alexei Starovoitov
Browse files

bpf: improve precision backtrack logging 



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: default avatarAndrii Nakryiko <andrii@kernel.org>
Link: https://lore.kernel.org/r/20230505043317.3629845-5-andrii@kernel.org


Signed-off-by: default avatarAlexei Starovoitov <ast@kernel.org>
parent 407958a0

include/linux/bpf_verifier.h

+9 −4
Original line number Diff line number Diff line
@@ -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
@@ -620,8 +623,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,

kernel/bpf/verifier.c

+65 −7
Original line number Diff line number Diff line
@@ -605,9 +605,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[] = {








@@ -3308,6 +3308,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.








@@ -3331,7 +3370,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=%s ",









			bt->frame, env->tmp_str_buf);









		fmt_stack_mask(env->tmp_str_buf, TMP_STR_BUF_LEN, bt_stack_mask(bt));









		verbose(env, "stack=%s before ", env->tmp_str_buf);









		verbose(env, "%d: ", idx);









		print_bpf_insn(&cbs, insn, env->allow_ptr_leaks);









	}








@@ -3531,6 +3574,11 @@ static void mark_all_scalars_precise(struct bpf_verifier_env *env,







	struct bpf_reg_state *reg;









	int i, j;

















	if (env->log.level & BPF_LOG_LEVEL2) {









		verbose(env, "mark_precise: frame%d: falling back to forcing all scalars precise\n",









			st->curframe);









	}

















	/* big hammer: mark all scalars precise in this path.









	 * pop_stack may still get !precise scalars.









	 * We also skip current state and go straight to first parent state,








@@ -3542,17 +3590,25 @@ static void mark_all_scalars_precise(struct bpf_verifier_env *env,







			func = st->frame[i];









			for (j = 0; j < BPF_REG_FP; j++) {









				reg = &func->regs[j];









				if (reg->type != SCALAR_VALUE)









				if (reg->type != SCALAR_VALUE || reg->precise)









					continue;









				reg->precise = true;









				if (env->log.level & BPF_LOG_LEVEL2) {









					verbose(env, "force_precise: frame%d: forcing r%d to be precise\n",









						i, j);









				}









			}









			for (j = 0; j < func->allocated_stack / BPF_REG_SIZE; j++) {









				if (!is_spilled_reg(&func->stack[j]))









					continue;









				reg = &func->stack[j].spilled_ptr;









				if (reg->type != SCALAR_VALUE)









				if (reg->type != SCALAR_VALUE || reg->precise)









					continue;









				reg->precise = true;









				if (env->log.level & BPF_LOG_LEVEL2) {









					verbose(env, "force_precise: frame%d: forcing fp%d to be precise\n",









						i, -(j + 1) * 8);









				}









			}









		}









	}








@@ -3716,8 +3772,10 @@ static int __mark_chain_precision(struct bpf_verifier_env *env, int frame, int r







		DECLARE_BITMAP(mask, 64);









		u32 history = st->jmp_history_cnt;

















		if (env->log.level & BPF_LOG_LEVEL2)









			verbose(env, "last_idx %d first_idx %d\n", last_idx, first_idx);









		if (env->log.level & BPF_LOG_LEVEL2) {









			verbose(env, "mark_precise: frame%d: last_idx %d first_idx %d\n",









				bt->frame, last_idx, first_idx);









		}

















		if (last_idx < 0) {









			/* we are at the entry into subprog, which
































tools/testing/selftests/bpf/verifier/precise.c



+54
−52






























Original line number
Diff line number
Diff line







@@ -38,25 +38,24 @@







	.fixup_map_array_48b = { 1 },









	.result = VERBOSE_ACCEPT,









	.errstr =









	"26: (85) call bpf_probe_read_kernel#113\









	last_idx 26 first_idx 20\









	regs=4 stack=0 before 25\









	regs=4 stack=0 before 24\









	regs=4 stack=0 before 23\









	regs=4 stack=0 before 22\









	regs=4 stack=0 before 20\









	parent didn't have regs=4 stack=0 marks\









	last_idx 19 first_idx 10\









	regs=4 stack=0 before 19\









	regs=200 stack=0 before 18\









	regs=300 stack=0 before 17\









	regs=201 stack=0 before 15\









	regs=201 stack=0 before 14\









	regs=200 stack=0 before 13\









	regs=200 stack=0 before 12\









	regs=200 stack=0 before 11\









	regs=200 stack=0 before 10\









	parent already had regs=0 stack=0 marks",









	"mark_precise: frame0: last_idx 26 first_idx 20\









	mark_precise: frame0: regs=r2 stack= before 25\









	mark_precise: frame0: regs=r2 stack= before 24\









	mark_precise: frame0: regs=r2 stack= before 23\









	mark_precise: frame0: regs=r2 stack= before 22\









	mark_precise: frame0: regs=r2 stack= before 20\









	parent didn't have regs=4 stack=0 marks:\









	mark_precise: frame0: last_idx 19 first_idx 10\









	mark_precise: frame0: regs=r2 stack= before 19\









	mark_precise: frame0: regs=r9 stack= before 18\









	mark_precise: frame0: regs=r8,r9 stack= before 17\









	mark_precise: frame0: regs=r0,r9 stack= before 15\









	mark_precise: frame0: regs=r0,r9 stack= before 14\









	mark_precise: frame0: regs=r9 stack= before 13\









	mark_precise: frame0: regs=r9 stack= before 12\









	mark_precise: frame0: regs=r9 stack= before 11\









	mark_precise: frame0: regs=r9 stack= before 10\









	parent already had regs=0 stack=0 marks:",









},









{









	"precise: test 2",








@@ -100,20 +99,20 @@







	.flags = BPF_F_TEST_STATE_FREQ,









	.errstr =









	"26: (85) call bpf_probe_read_kernel#113\









	last_idx 26 first_idx 22\









	regs=4 stack=0 before 25\









	regs=4 stack=0 before 24\









	regs=4 stack=0 before 23\









	regs=4 stack=0 before 22\









	parent didn't have regs=4 stack=0 marks\









	last_idx 20 first_idx 20\









	regs=4 stack=0 before 20\









	parent didn't have regs=4 stack=0 marks\









	last_idx 19 first_idx 17\









	regs=4 stack=0 before 19\









	regs=200 stack=0 before 18\









	regs=300 stack=0 before 17\









	parent already had regs=0 stack=0 marks",









	mark_precise: frame0: last_idx 26 first_idx 22\









	mark_precise: frame0: regs=r2 stack= before 25\









	mark_precise: frame0: regs=r2 stack= before 24\









	mark_precise: frame0: regs=r2 stack= before 23\









	mark_precise: frame0: regs=r2 stack= before 22\









	parent didn't have regs=4 stack=0 marks:\









	mark_precise: frame0: last_idx 20 first_idx 20\









	mark_precise: frame0: regs=r2 stack= before 20\









	parent didn't have regs=4 stack=0 marks:\









	mark_precise: frame0: last_idx 19 first_idx 17\









	mark_precise: frame0: regs=r2 stack= before 19\









	mark_precise: frame0: regs=r9 stack= before 18\









	mark_precise: frame0: regs=r8,r9 stack= before 17\









	parent already had regs=0 stack=0 marks:",









},









{









	"precise: cross frame pruning",








@@ -153,15 +152,15 @@







	},









	.prog_type = BPF_PROG_TYPE_XDP,









	.flags = BPF_F_TEST_STATE_FREQ,









	.errstr = "5: (2d) if r4 > r0 goto pc+0\









	last_idx 5 first_idx 5\









	parent didn't have regs=10 stack=0 marks\









	last_idx 4 first_idx 2\









	regs=10 stack=0 before 4\









	regs=10 stack=0 before 3\









	regs=0 stack=1 before 2\









	last_idx 5 first_idx 5\









	parent didn't have regs=1 stack=0 marks",









	.errstr = "mark_precise: frame0: last_idx 5 first_idx 5\









	parent didn't have regs=10 stack=0 marks:\









	mark_precise: frame0: last_idx 4 first_idx 2\









	mark_precise: frame0: regs=r4 stack= before 4\









	mark_precise: frame0: regs=r4 stack= before 3\









	mark_precise: frame0: regs= stack=-8 before 2\









	mark_precise: frame0: falling back to forcing all scalars precise\









	mark_precise: frame0: last_idx 5 first_idx 5\









	parent didn't have regs=1 stack=0 marks:",









	.result = VERBOSE_ACCEPT,









	.retval = -1,









},








@@ -179,16 +178,19 @@







	},









	.prog_type = BPF_PROG_TYPE_XDP,









	.flags = BPF_F_TEST_STATE_FREQ,









	.errstr = "last_idx 6 first_idx 6\









	parent didn't have regs=10 stack=0 marks\









	last_idx 5 first_idx 3\









	regs=10 stack=0 before 5\









	regs=10 stack=0 before 4\









	regs=0 stack=1 before 3\









	last_idx 6 first_idx 6\









	parent didn't have regs=1 stack=0 marks\









	last_idx 5 first_idx 3\









	regs=1 stack=0 before 5",









	.errstr = "mark_precise: frame0: last_idx 6 first_idx 6\









	parent didn't have regs=10 stack=0 marks:\









	mark_precise: frame0: last_idx 5 first_idx 3\









	mark_precise: frame0: regs=r4 stack= before 5\









	mark_precise: frame0: regs=r4 stack= before 4\









	mark_precise: frame0: regs= stack=-8 before 3\









	mark_precise: frame0: falling back to forcing all scalars precise\









	force_precise: frame0: forcing r0 to be precise\









	force_precise: frame0: forcing r0 to be precise\









	mark_precise: frame0: last_idx 6 first_idx 6\









	parent didn't have regs=1 stack=0 marks:\









	mark_precise: frame0: last_idx 5 first_idx 3\









	mark_precise: frame0: regs=r0 stack= before 5",









	.result = VERBOSE_ACCEPT,









	.retval = -1,









},