From bc5a4c0ad2a517274e87ed6bb233083e6860ea0f Mon Sep 17 00:00:00 2001
From: Alan Jowett <alanjo@microsoft.com>
Date: Tue, 18 Aug 2026 08:53:06 -0700
Subject: [PATCH 1/2] Expose BPF call depth from analysis

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Copilot-Session: e25e56a4-6641-4d86-8b3a-2771a6a804c5
Signed-off-by: Alan Jowett <alanjo@microsoft.com>
---
 src/fwd_analyzer.cpp                 | 10 ++++++++++
 src/result.hpp                       |  1 +
 src/test/test_cfg_builder_passes.cpp | 26 ++++++++++++++++++++++++++
 3 files changed, 37 insertions(+)

diff --git a/src/fwd_analyzer.cpp b/src/fwd_analyzer.cpp
index 4ce08cf52..206ee5245 100644
--- a/src/fwd_analyzer.cpp
+++ b/src/fwd_analyzer.cpp
@@ -142,6 +142,15 @@ class InterleavedFwdFixpointIterator final {
         return std::numeric_limits<int>::max();
     }
 
+    int max_call_depth() const {
+        int max_call_depth = 0;
+        for (const Label& label : _prog.labels()) {
+            // Label depth includes the entry frame; callers need only BPF-to-BPF calls.
+            max_call_depth = std::max(max_call_depth, label.call_stack_depth() - 1);
+        }
+        return max_call_depth;
+    }
+
   public:
     void operator()(const Label& node);
 
@@ -223,6 +232,7 @@ AnalysisResult InterleavedFwdFixpointIterator::run(const AnalysisContext& contex
     const Program& prog = context.program;
     AnalysisResult result;
     InterleavedFwdFixpointIterator analyzer(context, result);
+    result.max_call_depth = analyzer.max_call_depth();
     if (context.runtime().check_for_termination) {
         analyzer._wto.for_each_loop_head(
             [&](const Label& label) { ebpf_domain_initialize_loop_counter(entry_inv, label, context); });
diff --git a/src/result.hpp b/src/result.hpp
index 5311904ab..6cc604514 100644
--- a/src/result.hpp
+++ b/src/result.hpp
@@ -144,6 +144,7 @@ struct AnalysisResult {
     std::map<Label, InvariantMapPair> invariants;
     bool failed = false;
     int max_loop_count{};
+    int max_call_depth{};
     Interval exit_value = Interval::top();
 
     [[nodiscard]]
diff --git a/src/test/test_cfg_builder_passes.cpp b/src/test/test_cfg_builder_passes.cpp
index 0b9824114..4818515ac 100644
--- a/src/test/test_cfg_builder_passes.cpp
+++ b/src/test/test_cfg_builder_passes.cpp
@@ -12,6 +12,7 @@
 #include "ir/program.hpp"
 #include "ir/syntax.hpp"
 #include "platform.hpp"
+#include "verifier.hpp"
 
 using namespace prevail;
 
@@ -207,6 +208,31 @@ TEST_CASE("pass_insert_termination_counters is off by default", "[passes]") {
     }
 }
 
+TEST_CASE("AnalysisResult reports maximum nested BPF-to-BPF call depth", "[passes][stats]") {
+    const ProgramInfo info = default_info();
+
+    SECTION("does not count the entry frame") {
+        InstructionSeq seq;
+        seq.push_back(at(0, Exit{}));
+
+        const Program prog = Program::from_sequence(seq, info, {});
+        REQUIRE(analyze(prog, {}).max_call_depth == 0);
+    }
+
+    SECTION("counts nested local calls") {
+        InstructionSeq seq;
+        // entry -> call subprogram 1 -> call subprogram 2 -> exit.
+        seq.push_back(at(0, CallLocal{.target = Label{2}}));
+        seq.push_back(at(1, Exit{}));
+        seq.push_back(at(2, CallLocal{.target = Label{4}}));
+        seq.push_back(at(3, Exit{}));
+        seq.push_back(at(4, Exit{}));
+
+        const Program prog = Program::from_sequence(seq, info, {});
+        REQUIRE(analyze(prog, {}).max_call_depth == 2);
+    }
+}
+
 TEST_CASE("pass_extract_assertions populates assertions for every label in the CFG", "[passes]") {
     const ProgramInfo info = default_info();
     InstructionSeq seq;

From f57dab194dbd3305328d506894d74b342af0e9b8 Mon Sep 17 00:00:00 2001
From: Alan Jowett <alanjo@microsoft.com>
Date: Tue, 18 Aug 2026 12:03:11 -0700
Subject: [PATCH 2/2] Report reachable BPF call depth

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Copilot-Session: e25e56a4-6641-4d86-8b3a-2771a6a804c5
Signed-off-by: Alan Jowett <alanjo@microsoft.com>
---
 src/fwd_analyzer.cpp                 | 16 ++++++++++++-
 src/test/test_cfg_builder_passes.cpp | 34 ++++++++++++++++++++++++++++
 2 files changed, 49 insertions(+), 1 deletion(-)

diff --git a/src/fwd_analyzer.cpp b/src/fwd_analyzer.cpp
index 206ee5245..ebf53917a 100644
--- a/src/fwd_analyzer.cpp
+++ b/src/fwd_analyzer.cpp
@@ -2,8 +2,10 @@
 // SPDX-License-Identifier: Apache-2.0
 #include <cassert>
 #include <ranges>
+#include <set>
 #include <utility>
 #include <variant>
+#include <vector>
 
 #include "analysis_context.hpp"
 #include "cfg/cfg.hpp"
@@ -142,11 +144,23 @@ class InterleavedFwdFixpointIterator final {
         return std::numeric_limits<int>::max();
     }
 
+    [[nodiscard]]
     int max_call_depth() const {
         int max_call_depth = 0;
-        for (const Label& label : _prog.labels()) {
+        std::set<Label> visited;
+        std::vector<Label> worklist{_cfg.entry_label()};
+        while (!worklist.empty()) {
+            const Label label = worklist.back();
+            worklist.pop_back();
+            if (!visited.insert(label).second) {
+                continue;
+            }
+
             // Label depth includes the entry frame; callers need only BPF-to-BPF calls.
             max_call_depth = std::max(max_call_depth, label.call_stack_depth() - 1);
+            for (const Label& child : _cfg.children_of(label)) {
+                worklist.push_back(child);
+            }
         }
         return max_call_depth;
     }
diff --git a/src/test/test_cfg_builder_passes.cpp b/src/test/test_cfg_builder_passes.cpp
index 4818515ac..e366ed2dc 100644
--- a/src/test/test_cfg_builder_passes.cpp
+++ b/src/test/test_cfg_builder_passes.cpp
@@ -231,6 +231,40 @@ TEST_CASE("AnalysisResult reports maximum nested BPF-to-BPF call depth", "[passe
         const Program prog = Program::from_sequence(seq, info, {});
         REQUIRE(analyze(prog, {}).max_call_depth == 2);
     }
+
+    SECTION("excludes unreachable nested local calls") {
+        InstructionSeq seq;
+        seq.push_back(at(0, Exit{}));
+        // These calls are retained and inlined during CFG preparation, but are unreachable from entry.
+        seq.push_back(at(1, CallLocal{.target = Label{3}}));
+        seq.push_back(at(2, Exit{}));
+        seq.push_back(at(3, CallLocal{.target = Label{5}}));
+        seq.push_back(at(4, Exit{}));
+        seq.push_back(at(5, Exit{}));
+
+        const Program prog = Program::from_sequence(seq, info, {});
+        REQUIRE(analyze(prog, {}).max_call_depth == 0);
+    }
+
+    SECTION("preserves call depth after verification failure") {
+        InstructionSeq seq;
+        seq.push_back(at(0, CallLocal{.target = Label{2}}));
+        seq.push_back(at(1, Exit{}));
+        seq.push_back(at(2, CallLocal{.target = Label{4}}));
+        seq.push_back(at(3, Exit{}));
+        // This is one byte below the innermost 512-byte frame.
+        seq.push_back(at(4, Mem{
+                                .access = {.width = 1, .basereg = Reg{R10_STACK_POINTER}, .offset = -513},
+                                .value = Imm{0},
+                                .is_load = false,
+                            }));
+        seq.push_back(at(5, Exit{}));
+
+        const Program prog = Program::from_sequence(seq, info, {});
+        const AnalysisResult result = analyze(prog, {});
+        REQUIRE(result.failed);
+        REQUIRE(result.max_call_depth == 2);
+    }
 }
 
 TEST_CASE("pass_extract_assertions populates assertions for every label in the CFG", "[passes]") {