[PATCH bpf-next v4 0/3] Improve stack depth verification stats output

[PATCH bpf-next v4 0/3] Improve stack depth verification stats output

[Kumar Kartikeya Dwivedi]

Some improvements for more clarity in the stack depth verification
statistics output. See commit logs for details.

Changelog:
----------
v3 -> v4
v3: https://lore.kernel.org/bpf/20260803031457.3115812-1-memxor@gmail.com

 * Read names from subprog_info directly to avoid an out-of-bounds access
   when func_info validation fails. (BPF CI Bot)

v2 -> v3
v2: https://lore.kernel.org/bpf/20260802225209.2511758-1-memxor@gmail.com

 * Reuse subprog_name() to fetch subprogram names. (BPF CI Bot)

v1 -> v2
v1: https://lore.kernel.org/bpf/20260801230400.850271-1-memxor@gmail.com

 * Use multi-line format. (Eduard)
 * Adjust veristat to work with old and new format.
 * Adjust selftest log_level without new option. (Eduard)

Kumar Kartikeya Dwivedi (3):
  bpf: Show more useful info in stack depth stats
  selftests/bpf: Adjust veristat stack depth parsing
  selftests/bpf: Test stack depth stats without BTF subprog names

 kernel/bpf/verifier.c                         | 13 +++++++----
 .../bpf/progs/verifier_basic_stack.c          |  4 ++--
 .../bpf/progs/verifier_bpf_fastcall.c         | 23 ++++++++++++-------
 .../bpf/progs/verifier_private_stack.c        | 15 +++++++++---
 .../selftests/bpf/progs/verifier_var_off.c    |  4 ++--
 tools/testing/selftests/bpf/test_verifier.c   |  2 +-
 tools/testing/selftests/bpf/verifier/calls.c  |  6 ++++-
 tools/testing/selftests/bpf/veristat.c        | 16 +++++++++----
 8 files changed, 58 insertions(+), 25 deletions(-)


base-commit: 8f876c773b79ed66dadc9507f50dbff39c6a9ec7
-- 
2.53.0

[PATCH bpf-next v4 1/3] bpf: Show more useful info in stack depth stats

[Kumar Kartikeya Dwivedi]

Currently, stack depth statistics are too crude, listing captured depths in
subprogram-number order. Since libbpf determines those numbers, it is hard to
associate each depth with its subprogram name.

Print the maximum stack depth and each subprogram on separate lines:

stack depth max <depth>
stack depth subprog <number> <name> <depth>

When no subprogram name is available, print <unknown>.

Suggested-by: Andrii Nakryiko <andrii@kernel.org>
Signed-off-by: Kumar Kartikeya Dwivedi <memxor@gmail.com>
---
 kernel/bpf/verifier.c                         | 13 +++++++----
 .../bpf/progs/verifier_basic_stack.c          |  4 ++--
 .../bpf/progs/verifier_bpf_fastcall.c         | 23 ++++++++++++-------
 .../bpf/progs/verifier_private_stack.c        | 15 +++++++++---
 .../selftests/bpf/progs/verifier_var_off.c    |  4 ++--
 5 files changed, 40 insertions(+), 19 deletions(-)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index b274004fccfd..3b61897ed0d2 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -18777,10 +18777,15 @@ static void print_verification_stats(struct bpf_verifier_env *env)
 	if (env->log.level & BPF_LOG_STATS) {
 		verbose(env, "verification time %lld usec\n",
 			div_u64(env->verification_time, 1000));
-		verbose(env, "stack depth %d", env->subprog_info[0].stack_depth);
-		for (i = 1; i < subprog_cnt; i++)
-			verbose(env, "+%d", env->subprog_info[i].stack_depth);
-		verbose(env, " max %d\n", env->max_stack_depth);
+		verbose(env, "stack depth max %d\n", env->max_stack_depth);
+		for (i = 0; i < subprog_cnt; i++) {
+			const char *name = env->subprog_info[i].name;
+
+			if (!name || !name[0])
+				name = "<unknown>";
+			verbose(env, "stack depth subprog %d %s %d\n", i, name,
+				env->subprog_info[i].stack_depth);
+		}
 		verbose(env, "insns processed %d", env->subprog_info[0].insn_processed);
 		for (i = 1; i < subprog_cnt; i++)
 			if (bpf_subprog_is_global(env, i))
diff --git a/tools/testing/selftests/bpf/progs/verifier_basic_stack.c b/tools/testing/selftests/bpf/progs/verifier_basic_stack.c
index fb62e09f2114..61ec8790fd21 100644
--- a/tools/testing/selftests/bpf/progs/verifier_basic_stack.c
+++ b/tools/testing/selftests/bpf/progs/verifier_basic_stack.c
@@ -27,7 +27,7 @@ __naked void stack_out_of_bounds(void)
 
 SEC("socket")
 __description("uninitialized stack1")
-__success __log_level(4) __msg("stack depth 8")
+__success __log_level(4) __msg("stack depth subprog 0 uninitialized_stack1 8")
 __failure_unpriv __msg_unpriv("invalid read from stack")
 __naked void uninitialized_stack1(void)
 {
@@ -45,7 +45,7 @@ __naked void uninitialized_stack1(void)
 
 SEC("socket")
 __description("uninitialized stack2")
-__success __log_level(4) __msg("stack depth 8")
+__success __log_level(4) __msg("stack depth subprog 0 uninitialized_stack2 8")
 __failure_unpriv __msg_unpriv("invalid read from stack")
 __naked void uninitialized_stack2(void)
 {
diff --git a/tools/testing/selftests/bpf/progs/verifier_bpf_fastcall.c b/tools/testing/selftests/bpf/progs/verifier_bpf_fastcall.c
index 83707faea049..cb36866bfed3 100644
--- a/tools/testing/selftests/bpf/progs/verifier_bpf_fastcall.c
+++ b/tools/testing/selftests/bpf/progs/verifier_bpf_fastcall.c
@@ -10,7 +10,7 @@
 
 SEC("raw_tp")
 __arch_x86_64
-__log_level(4) __msg("stack depth 8")
+__log_level(4) __msg("stack depth subprog 0 simple 8")
 __xlated("4: r5 = 5")
 __xlated("5: r0 = ")
 __xlated("6: r0 = &(void __percpu *)(r0)")
@@ -96,7 +96,7 @@ __naked void canary_zero_spills(void)
 
 SEC("raw_tp")
 __arch_x86_64
-__log_level(4) __msg("stack depth 16")
+__log_level(4) __msg("stack depth subprog 0 wrong_reg_in_pattern1 16")
 __xlated("1: *(u64 *)(r10 -16) = r1")
 __xlated("...")
 __xlated("3: r0 = &(void __percpu *)(r0)")
@@ -598,7 +598,7 @@ __naked static void subprogs_use_independent_offsets_aux(void)
 
 SEC("raw_tp")
 __arch_x86_64
-__log_level(4) __msg("stack depth 8")
+__log_level(4) __msg("stack depth subprog 0 helper_call_does_not_prevent_bpf_fastcall 8")
 __xlated("2: r0 = &(void __percpu *)(r0)")
 __success
 __naked void helper_call_does_not_prevent_bpf_fastcall(void)
@@ -620,7 +620,7 @@ __naked void helper_call_does_not_prevent_bpf_fastcall(void)
 
 SEC("raw_tp")
 __arch_x86_64
-__log_level(4) __msg("stack depth 24")
+__log_level(4) __msg("stack depth subprog 0 may_goto_interaction_x86_64 24")
 /* may_goto counter at -24 */
 __xlated("0: *(u64 *)(r10 -24) =")
 /* may_goto timestamp at -16 */
@@ -661,7 +661,7 @@ __naked void may_goto_interaction_x86_64(void)
 SEC("raw_tp")
 __arch_arm64
 __arch_riscv64
-__log_level(4) __msg("stack depth 24")
+__log_level(4) __msg("stack depth subprog 0 may_goto_interaction 24")
 /* may_goto counter at -24 */
 __xlated("0: *(u64 *)(r10 -24) =")
 /* may_goto timestamp at -16 */
@@ -708,7 +708,9 @@ __naked static void dummy_loop_callback(void)
 
 SEC("raw_tp")
 __arch_x86_64
-__log_level(4) __msg("stack depth 32+0")
+__log_level(4)
+__msg("stack depth subprog 0 bpf_loop_interaction1 32")
+__msg("stack depth subprog 1 dummy_loop_callback 0")
 __xlated("2: r1 = 1")
 __xlated("3: r0 =")
 __xlated("4: r0 = &(void __percpu *)(r0)")
@@ -756,7 +758,9 @@ __naked int bpf_loop_interaction1(void)
 
 SEC("raw_tp")
 __arch_x86_64
-__log_level(4) __msg("stack depth 40+0")
+__log_level(4)
+__msg("stack depth subprog 0 bpf_loop_interaction2 40")
+__msg("stack depth subprog 1 dummy_loop_callback 0")
 /* call bpf_get_smp_processor_id */
 __xlated("2: r1 = 42")
 __xlated("3: r0 =")
@@ -800,7 +804,10 @@ __naked int bpf_loop_interaction2(void)
 
 SEC("raw_tp")
 __arch_x86_64
-__log_level(4) __msg("stack depth 512+0 max 512")
+__log_level(4)
+__msg("stack depth max 512")
+__msg("stack depth subprog 0 cumulative_stack_depth 512")
+__msg("stack depth subprog 1 cumulative_stack_depth_subprog 0")
 /* just to print xlated version when debugging */
 __xlated("r0 = &(void __percpu *)(r0)")
 __success
diff --git a/tools/testing/selftests/bpf/progs/verifier_private_stack.c b/tools/testing/selftests/bpf/progs/verifier_private_stack.c
index bb8206e10880..c818898836c1 100644
--- a/tools/testing/selftests/bpf/progs/verifier_private_stack.c
+++ b/tools/testing/selftests/bpf/progs/verifier_private_stack.c
@@ -86,7 +86,9 @@ __naked static void cumulative_stack_depth_subprog(void)
 SEC("kprobe")
 __description("Private stack, subtree > MAX_BPF_STACK")
 __success
-__log_level(4) __msg("stack depth 512+32 max 512")
+__log_level(4) __msg("stack depth max 512")
+__msg("stack depth subprog 0 private_stack_nested_1 512")
+__msg("stack depth subprog 1 cumulative_stack_depth_subprog 32")
 __arch_x86_64
 /* private stack fp for the main prog */
 __jited("	movabsq	$0x{{.*}}, %r9")
@@ -331,7 +333,11 @@ SEC("fentry/bpf_fentry_test9")
 __description("Private stack, async callback, potential nesting")
 __success __retval(0)
 __load_if_JITed()
-__log_level(4) __msg("stack depth 8+0+256+0 max 272")
+__log_level(4) __msg("stack depth max 272")
+__msg("stack depth subprog 0 private_stack_async_callback_2 8")
+__msg("stack depth subprog 1 timer_cb1 0")
+__msg("stack depth subprog 2 subprog1 256")
+__msg("stack depth subprog 3 subprog2 0")
 __arch_x86_64
 __jited("	subq	$0x100, %rsp")
 __arch_arm64
@@ -355,7 +361,10 @@ int private_stack_async_callback_2(void)
 SEC("fentry/bpf_fentry_test9")
 __description("private stack, max stack depth is private stack")
 __success
-__log_level(4) __msg("stack depth 8+256+0 max 256")
+__log_level(4) __msg("stack depth max 256")
+__msg("stack depth subprog 0 private_stack_max_depth 8")
+__msg("stack depth subprog 1 subprog1 256")
+__msg("stack depth subprog 2 subprog2 0")
 int private_stack_max_depth(void)
 {
 	int x = 0;
diff --git a/tools/testing/selftests/bpf/progs/verifier_var_off.c b/tools/testing/selftests/bpf/progs/verifier_var_off.c
index 24cd0a763673..df436bbc9ecf 100644
--- a/tools/testing/selftests/bpf/progs/verifier_var_off.c
+++ b/tools/testing/selftests/bpf/progs/verifier_var_off.c
@@ -198,7 +198,7 @@ __success
 /* Check that the maximum stack depth is correctly maintained according to the
  * maximum possible variable offset.
  */
-__log_level(4) __msg("stack depth 16")
+__log_level(4) __msg("stack depth subprog 0 stack_write_priv_vs_unpriv 16")
 __failure_unpriv
 /* Variable stack access is rejected for unprivileged.
  */
@@ -238,7 +238,7 @@ __success
 /* Check that the maximum stack depth is correctly maintained according to the
  * maximum possible variable offset.
  */
-__log_level(4) __msg("stack depth 16")
+__log_level(4) __msg("stack depth subprog 0 stack_write_followed_by_read 16")
 __failure_unpriv
 __msg_unpriv("R2 variable stack access prohibited for !root")
 __retval(0)
-- 
2.53.0

[PATCH bpf-next v4 2/3] selftests/bpf: Adjust veristat stack depth parsing

[Kumar Kartikeya Dwivedi]

The verifier now reports stack depth statistics using one record per line.
Teach veristat to parse the new maximum and per-subprogram records while
retaining support for the legacy one-line format used by older kernels.

Increase the bounded backward scan so it can include all 256 per-subprogram
records.

Signed-off-by: Kumar Kartikeya Dwivedi <memxor@gmail.com>
---
 tools/testing/selftests/bpf/veristat.c | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/tools/testing/selftests/bpf/veristat.c b/tools/testing/selftests/bpf/veristat.c
index c9c257784ee3..97397b97745d 100644
--- a/tools/testing/selftests/bpf/veristat.c
+++ b/tools/testing/selftests/bpf/veristat.c
@@ -993,13 +993,15 @@ static void free_verif_stats(struct verif_stats *stats, size_t stat_cnt)
 
 static char verif_log_buf[64 * 1024];
 
-#define MAX_PARSED_LOG_LINES 100
+/* Keep room for all 256 subprogram records and trailing statistics. */
+#define MAX_PARSED_LOG_LINES 300
 
 static int parse_verif_log(char * const buf, size_t buf_sz, struct verif_stats *s)
 {
 	const char *cur;
-	int pos, lines, sub_stack, cnt = 0;
-	char *state = NULL, *token, stack[512];
+	long sub_stack;
+	int pos, lines, cnt = 0;
+	char *state = NULL, *token, stack[512] = {};
 
 	buf[buf_sz - 1] = '\0';
 
@@ -1025,11 +1027,17 @@ static int parse_verif_log(char * const buf, size_t buf_sz, struct verif_stats *
 				&s->stats[MARK_READ_MAX_LEN]))
 			continue;
 
+		if (1 == sscanf(cur, "stack depth max %ld", &s->stats[MAX_STACK]))
+			continue;
+		if (1 == sscanf(cur, "stack depth subprog %*d %*s %ld", &sub_stack)) {
+			s->stats[STACK] += sub_stack;
+			continue;
+		}
 		if (2 == sscanf(cur, "stack depth %511s max %ld", stack, &s->stats[MAX_STACK]))
 			continue;
 	}
 	while ((token = strtok_r(cnt++ ? NULL : stack, "+", &state))) {
-		if (sscanf(token, "%d", &sub_stack) == 0)
+		if (sscanf(token, "%ld", &sub_stack) == 0)
 			break;
 		s->stats[STACK] += sub_stack;
 	}
-- 
2.53.0

[PATCH bpf-next v4 3/3] selftests/bpf: Test stack depth stats without BTF subprog names

[Kumar Kartikeya Dwivedi]

Test the stack depth statistics emitted when BTF function info does not
provide subprogram names.

Make VERBOSE_ACCEPT request verifier statistics so the raw-insn test can
validate the <unknown> output without a test-specific log level.

Signed-off-by: Kumar Kartikeya Dwivedi <memxor@gmail.com>
---
 tools/testing/selftests/bpf/test_verifier.c  | 2 +-
 tools/testing/selftests/bpf/verifier/calls.c | 6 +++++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/tools/testing/selftests/bpf/test_verifier.c b/tools/testing/selftests/bpf/test_verifier.c
index a8ae03c57bba..bffb7360434c 100644
--- a/tools/testing/selftests/bpf/test_verifier.c
+++ b/tools/testing/selftests/bpf/test_verifier.c
@@ -1560,7 +1560,7 @@ static void do_test_single(struct bpf_test *test, bool unpriv,
 
 	opts.expected_attach_type = test->expected_attach_type;
 	if (expected_ret == VERBOSE_ACCEPT)
-		opts.log_level = 2;
+		opts.log_level = 2 | 4;
 	else if (verbose)
 		opts.log_level = verif_log_level | 4; /* force stats */
 	else
diff --git a/tools/testing/selftests/bpf/verifier/calls.c b/tools/testing/selftests/bpf/verifier/calls.c
index 8cd626e04551..14f6f260b88b 100644
--- a/tools/testing/selftests/bpf/verifier/calls.c
+++ b/tools/testing/selftests/bpf/verifier/calls.c
@@ -1091,7 +1091,11 @@
 	/* stack_main=32, stack_A=256, stack_B=64
 	 * and max(main+A, main+A+B) < 512
 	 */
-	.result = ACCEPT,
+	.result = VERBOSE_ACCEPT,
+	.errstr = "stack depth max 352\t"
+		  "stack depth subprog 0 <unknown> 32\t"
+		  "stack depth subprog 1 <unknown> 256\t"
+		  "stack depth subprog 2 <unknown> 64",
 },
 {
 	"calls: stack depth check using three frames. test2",
-- 
2.53.0

Re: [PATCH bpf-next v4 1/3] bpf: Show more useful info in stack depth stats

[sashiko-bot]

Thank you for your contribution! Sashiko AI review found 1 potential issue(s) to consider:
- [Medium] The patch changes the verifier stack depth log format but misses updating tools/testing/selftests/bpf/veristat.c, breaking its ability to report stack depth statistics.
--

--- Patch [1]: [PATCH bpf-next v4 1/3] bpf: Show more useful info in stack depth stats ---
commit 5ac25e38dad528d9d2648231f63d507a8cd63820
Author: Kumar Kartikeya Dwivedi <memxor@gmail.com>

bpf: Show more useful info in stack depth stats

This commit changes the format of the verifier's stack depth statistics
to display the maximum depth and each subprogram's depth on separate lines
with their names, instead of a single string of depths.

> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -18777,10 +18777,15 @@ static void print_verification_stats(struct bpf_verifier_env *env)
>  	if (env->log.level & BPF_LOG_STATS) {
>  		verbose(env, "verification time %lld usec\n",
>  			div_u64(env->verification_time, 1000));
> -		verbose(env, "stack depth %d", env->subprog_info[0].stack_depth);
> -		for (i = 1; i < subprog_cnt; i++)
> -			verbose(env, "+%d", env->subprog_info[i].stack_depth);
> -		verbose(env, " max %d\n", env->max_stack_depth);
> +		verbose(env, "stack depth max %d\n", env->max_stack_depth);

[Severity: Medium]
Does this change in the verifier log output also require an update to the
veristat tool?

Looking at tools/testing/selftests/bpf/veristat.c in parse_verif_log(), it
currently parses the log like this:

	if (2 == sscanf(cur, "stack depth %511s max %ld", stack, &s->stats[MAX_STACK])) {

Since the patch removes the "stack depth %d...+%d max %d" format and splits
it into multiple lines ("stack depth max %d" and "stack depth subprog ..."),
it looks like veristat's sscanf will no longer match.

Could this cause veristat to silently fail to parse the statistics and report 0
for both the MAX_STACK and STACK metrics?

-- 
Sashiko AI review · https://sashiko.dev/#/patchset/20260803072733.191502-1-memxor@gmail.com?part=1

Re: [PATCH bpf-next v4 2/3] selftests/bpf: Adjust veristat stack depth parsing

[bot+bpf-ci]

[-- Attachment #1: Type: text/plain, Size: 1046 bytes --]

> selftests/bpf: Adjust veristat stack depth parsing
>
> The verifier now reports stack depth statistics using one record per line.
> Teach veristat to parse the new maximum and per-subprogram records while
> retaining support for the legacy one-line format used by older kernels.
>
> Increase the bounded backward scan so it can include all 256 per-subprogram
> records.
>
> Signed-off-by: Kumar Kartikeya Dwivedi <memxor@gmail.com>

This isn't a bug, but would it be worth a sentence on the `stack[512] = {}`
initializer? With the new one-record-per-line format the legacy
`stack depth %511s max %ld` branch never fires, so the trailing strtok_r()
loop would otherwise run over an uninitialized buffer - that seems worth
calling out in the changelog rather than leaving it to be inferred from the
diff.


---
AI reviewed your patch. Please fix the bug or email reply why it's not a bug.
See: https://github.com/kernel-patches/vmtest/blob/master/ci/claude/README.md

CI run summary: https://github.com/kernel-patches/bpf/actions/runs/30794340667

Re: [PATCH bpf-next v4 1/3] bpf: Show more useful info in stack depth stats

[Andrii Nakryiko]

On Mon, Aug 3, 2026 at 12:27 AM Kumar Kartikeya Dwivedi
<memxor@gmail.com> wrote:
>
> Currently, stack depth statistics are too crude, listing captured depths in
> subprogram-number order. Since libbpf determines those numbers, it is hard to
> associate each depth with its subprogram name.
>
> Print the maximum stack depth and each subprogram on separate lines:
>
> stack depth max <depth>
> stack depth subprog <number> <name> <depth>
>
> When no subprogram name is available, print <unknown>.
>
> Suggested-by: Andrii Nakryiko <andrii@kernel.org>
> Signed-off-by: Kumar Kartikeya Dwivedi <memxor@gmail.com>
> ---
>  kernel/bpf/verifier.c                         | 13 +++++++----
>  .../bpf/progs/verifier_basic_stack.c          |  4 ++--
>  .../bpf/progs/verifier_bpf_fastcall.c         | 23 ++++++++++++-------
>  .../bpf/progs/verifier_private_stack.c        | 15 +++++++++---
>  .../selftests/bpf/progs/verifier_var_off.c    |  4 ++--
>  5 files changed, 40 insertions(+), 19 deletions(-)
>

given we are going for quite verbose one line per prog/subprog format
anyways, let's make it actually even more useful and emit
insns_processed as well? I'd probably keep total line (processed N
insns (limit 1000000) ...) for backwards compat, but also have
per-subprog + main prog line with insns stat and stack depth,
something like

subprog 1 (sub1) insns 123 stack 16
subprog 2 (sub2) insns 345 stack 32
prog (main_one) insns 643 stack 64
processed 9999 insns (limit 1000000) max_states_per_insn 0
total_states 1 peak_states 1 mark_read 0

wdyt?

this will give better and more targeted information on where you
should look for w.r.t. verification optimization opportunities

and we can later add some other useful stats per-subprog/main prog as
necessary without any major breakage (tool just need to assume there
might be more stuff after "stack N" eventually

[...]

Re: [PATCH bpf-next v4 1/3] bpf: Show more useful info in stack depth stats

[Kumar Kartikeya Dwivedi]

On Mon Aug 3, 2026 at 9:48 PM CEST, Andrii Nakryiko wrote:
> On Mon, Aug 3, 2026 at 12:27 AM Kumar Kartikeya Dwivedi
> <memxor@gmail.com> wrote:
>>
>> Currently, stack depth statistics are too crude, listing captured depths in
>> subprogram-number order. Since libbpf determines those numbers, it is hard to
>> associate each depth with its subprogram name.
>>
>> Print the maximum stack depth and each subprogram on separate lines:
>>
>> stack depth max <depth>
>> stack depth subprog <number> <name> <depth>
>>
>> When no subprogram name is available, print <unknown>.
>>
>> Suggested-by: Andrii Nakryiko <andrii@kernel.org>
>> Signed-off-by: Kumar Kartikeya Dwivedi <memxor@gmail.com>
>> ---
>>  kernel/bpf/verifier.c                         | 13 +++++++----
>>  .../bpf/progs/verifier_basic_stack.c          |  4 ++--
>>  .../bpf/progs/verifier_bpf_fastcall.c         | 23 ++++++++++++-------
>>  .../bpf/progs/verifier_private_stack.c        | 15 +++++++++---
>>  .../selftests/bpf/progs/verifier_var_off.c    |  4 ++--
>>  5 files changed, 40 insertions(+), 19 deletions(-)
>>
>
> given we are going for quite verbose one line per prog/subprog format
> anyways, let's make it actually even more useful and emit
> insns_processed as well? I'd probably keep total line (processed N
> insns (limit 1000000) ...) for backwards compat, but also have
> per-subprog + main prog line with insns stat and stack depth,
> something like
>
> subprog 1 (sub1) insns 123 stack 16
> subprog 2 (sub2) insns 345 stack 32
> prog (main_one) insns 643 stack 64
> processed 9999 insns (limit 1000000) max_states_per_insn 0
> total_states 1 peak_states 1 mark_read 0
>
> wdyt?
>
> this will give better and more targeted information on where you
> should look for w.r.t. verification optimization opportunities
>
> and we can later add some other useful stats per-subprog/main prog as
> necessary without any major breakage (tool just need to assume there
> might be more stuff after "stack N" eventually
>

The format makes sense, let me rework the output and parsing and repost a v5.

> [...]