Fix stack access with bpf2bpf calls

src/asm_cfg.cpp

@@ -119,7 +119,6 @@ static void add_cfg_nodes(cfg_t& cfg, const label_t& caller_label, const label_t
     // Finally, recurse to replace any nested function macros.
     string caller_label_str = to_string(caller_label);
     long stack_frame_depth = std::ranges::count(caller_label_str, STACK_FRAME_DELIMITER) + 2;
-    constexpr int MAX_CALL_STACK_FRAMES = 8;
     for (auto& macro_label : seen_labels) {
         for (const label_t label(macro_label.from, macro_label.to, caller_label_str);
              const auto& inst : cfg.get_node(label)) {

src/asm_syntax.hpp

@@ -51,6 +51,17 @@ struct label_t {
         return to != -1;
     }
 
+    [[nodiscard]]
+    int call_stack_depth() const {
+        // The call stack depth is the number of '/' separated components in the label,
+        // which is one more than the number of '/' separated components in the prefix,
+        // hence two more than the number of '/' in the prefix, if any.
+        if (stack_frame_prefix.empty()) {
+            return 1;
+        }
+        return 2 + std::count(stack_frame_prefix.begin(), stack_frame_prefix.end(), STACK_FRAME_DELIMITER);
+    }
+
     friend std::ostream& operator<<(std::ostream& os, const label_t& label) {
         if (label == entry) {
             return os << "entry";
@@ -337,6 +348,7 @@ enum class AccessType {
 };
 
 struct ValidAccess {
+    int call_stack_depth{};
     Reg reg;
     int32_t offset{};
     Value width{Imm{0}};

src/asm_unmarshal.cpp

@@ -338,7 +338,7 @@ struct Unmarshaller {
             const uint8_t basereg = isLoad ? inst.src : inst.dst;
 
             if (basereg == R10_STACK_POINTER &&
-                (inst.offset + opcode_to_width(inst.opcode) > 0 || inst.offset < -EBPF_STACK_SIZE)) {
+                (inst.offset + opcode_to_width(inst.opcode) > 0 || inst.offset < -EBPF_TOTAL_STACK_SIZE)) {
                 note("Stack access out of bounds");
             }
             auto res = Mem{

src/assertions.cpp

@@ -27,6 +27,12 @@ class AssertExtractor {
         return res;
     }
 
+    ValidAccess make_valid_access(Reg reg, int32_t offset = {}, Value width = Imm{0}, bool or_null = {},
+                                  AccessType access_type = {}) const {
+        int depth = current_label.has_value() ? current_label.value().call_stack_depth() : 1;
+        return ValidAccess{ depth, reg, offset, width, or_null, access_type};
+    }
+
   public:
     explicit AssertExtractor(program_info info, std::optional<label_t> label)
         : info{std::move(info)}, current_label(label) {}
@@ -99,17 +105,17 @@ class AssertExtractor {
             switch (arg.kind) {
             case ArgPair::Kind::PTR_TO_READABLE_MEM_OR_NULL:
                 res.emplace_back(TypeConstraint{arg.mem, TypeGroup::mem_or_num});
-                res.emplace_back(ValidAccess{arg.mem, 0, arg.size, true, AccessType::read});
+                res.emplace_back(make_valid_access(arg.mem, 0, arg.size, true, AccessType::read));
                 break;
             case ArgPair::Kind::PTR_TO_READABLE_MEM:
                 /* pointer to valid memory (stack, packet, map value) */
                 res.emplace_back(TypeConstraint{arg.mem, TypeGroup::mem});
-                res.emplace_back(ValidAccess{arg.mem, 0, arg.size, false, AccessType::read});
+                res.emplace_back(make_valid_access(arg.mem, 0, arg.size, false, AccessType::read));
                 break;
             case ArgPair::Kind::PTR_TO_WRITABLE_MEM:
                 // memory may be uninitialized, i.e. write only
                 res.emplace_back(TypeConstraint{arg.mem, TypeGroup::mem});
-                res.emplace_back(ValidAccess{arg.mem, 0, arg.size, false, AccessType::write});
+                res.emplace_back(make_valid_access(arg.mem, 0, arg.size, false, AccessType::write));
                 break;
             }
             // TODO: reg is constant (or maybe it's not important)
@@ -137,14 +143,14 @@ class AssertExtractor {
                 // no need to check for valid access, it must be a number
                 res.emplace_back(TypeConstraint{cond.left, TypeGroup::number});
             } else {
-                res.emplace_back(ValidAccess{cond.left});
+                res.emplace_back(make_valid_access(cond.left));
                 // OK - map_fd is just another pointer
                 // Anything can be compared to 0
             }
         } else {
             const auto reg_right = get<Reg>(cond.right);
-            res.emplace_back(ValidAccess{cond.left});
-            res.emplace_back(ValidAccess{reg_right});
+            res.emplace_back(make_valid_access(cond.left));
+            res.emplace_back(make_valid_access(reg_right));
             if (cond.op != Condition::Op::EQ && cond.op != Condition::Op::NE) {
                 res.emplace_back(TypeConstraint{cond.left, TypeGroup::ptr_or_num});
             }
@@ -169,15 +175,15 @@ class AssertExtractor {
         const int offset = ins.access.offset;
         if (basereg.v == R10_STACK_POINTER) {
             // We know we are accessing the stack.
-            if (offset < -EBPF_STACK_SIZE || offset + static_cast<int>(width.v) >= 0) {
+            if (offset < -EBPF_SUBPROGRAM_STACK_SIZE || offset + static_cast<int>(width.v) >= 0) {
                 // This assertion will fail
-                res.emplace_back(
-                    ValidAccess{basereg, offset, width, false, ins.is_load ? AccessType::read : AccessType::write});
+                res.emplace_back(make_valid_access(basereg, offset, width, false,
+                                                   ins.is_load ? AccessType::read : AccessType::write));
             }
         } else {
             res.emplace_back(TypeConstraint{basereg, TypeGroup::pointer});
-            res.emplace_back(
-                ValidAccess{basereg, offset, width, false, ins.is_load ? AccessType::read : AccessType::write});
+            res.emplace_back(make_valid_access(basereg, offset, width, false,
+                                               ins.is_load ? AccessType::read : AccessType::write));
             if (!info.type.is_privileged && !ins.is_load) {
                 if (const auto preg = std::get_if<Reg>(&ins.value)) {
                     if (width.v != 8) {
@@ -194,8 +200,8 @@ class AssertExtractor {
     vector<Assert> operator()(const Atomic& ins) const {
         vector<Assert> res;
         res.emplace_back(TypeConstraint{ins.access.basereg, TypeGroup::pointer});
-        res.emplace_back(
-            ValidAccess{ins.access.basereg, ins.access.offset, Imm{static_cast<uint32_t>(ins.access.width)}, false});
+        res.emplace_back(make_valid_access(ins.access.basereg, ins.access.offset,
+                                           Imm{static_cast<uint32_t>(ins.access.width)}, false));
         if (ins.op == Atomic::Op::CMPXCHG) {
             // The memory contents pointed to by ins.access will be compared
             // against the value of the ins.valreg register.  Only numbers are

src/crab/array_domain.cpp

@@ -816,7 +816,7 @@ void array_domain_t::havoc(NumAbsDomain& inv, const data_kind_t kind, const line
 void array_domain_t::store_numbers(const NumAbsDomain& inv, const variable_t _idx, const variable_t _width) {
 
     // TODO: this should be an user parameter.
-    const number_t max_num_elems = EBPF_STACK_SIZE;
+    const number_t max_num_elems = EBPF_TOTAL_STACK_SIZE;
 
     if (is_bottom()) {
         return;

src/crab/bitset_domain.cpp

@@ -6,23 +6,23 @@
 std::ostream& operator<<(std::ostream& o, const bitset_domain_t& b) {
     o << "Numbers -> {";
     bool first = true;
-    for (int i = -EBPF_STACK_SIZE; i < 0; i++) {
-        if (b.non_numerical_bytes[EBPF_STACK_SIZE + i]) {
+    for (int i = -EBPF_TOTAL_STACK_SIZE; i < 0; i++) {
+        if (b.non_numerical_bytes[EBPF_TOTAL_STACK_SIZE + i]) {
             continue;
         }
         if (!first) {
             o << ", ";
         }
         first = false;
-        o << "[" << EBPF_STACK_SIZE + i;
+        o << "[" << EBPF_TOTAL_STACK_SIZE + i;
         int j = i + 1;
         for (; j < 0; j++) {
-            if (b.non_numerical_bytes[EBPF_STACK_SIZE + j]) {
+            if (b.non_numerical_bytes[EBPF_TOTAL_STACK_SIZE + j]) {
                 break;
             }
         }
         if (j > i + 1) {
-            o << "..." << EBPF_STACK_SIZE + j - 1;
+            o << "..." << EBPF_TOTAL_STACK_SIZE + j - 1;
         }
         o << "]";
         i = j;
@@ -40,19 +40,19 @@ string_invariant bitset_domain_t::to_set() const {
     }
 
     std::set<std::string> result;
-    for (int i = -EBPF_STACK_SIZE; i < 0; i++) {
-        if (non_numerical_bytes[EBPF_STACK_SIZE + i]) {
+    for (int i = -EBPF_TOTAL_STACK_SIZE; i < 0; i++) {
+        if (non_numerical_bytes[EBPF_TOTAL_STACK_SIZE + i]) {
             continue;
         }
-        std::string value = "s[" + std::to_string(EBPF_STACK_SIZE + i);
+        std::string value = "s[" + std::to_string(EBPF_TOTAL_STACK_SIZE + i);
         int j = i + 1;
         for (; j < 0; j++) {
-            if (non_numerical_bytes[EBPF_STACK_SIZE + j]) {
+            if (non_numerical_bytes[EBPF_TOTAL_STACK_SIZE + j]) {
                 break;
             }
         }
         if (j > i + 1) {
-            value += "..." + std::to_string(EBPF_STACK_SIZE + j - 1);
+            value += "..." + std::to_string(EBPF_TOTAL_STACK_SIZE + j - 1);
         }
         value += "].type=number";
         result.insert(value);

src/crab/bitset_domain.hpp

@@ -4,12 +4,12 @@
 #include <bitset>
 #include <cassert>
 
-#include "spec_type_descriptors.hpp" // for EBPF_STACK_SIZE
+#include "ebpf_base.h" // for EBPF_TOTAL_STACK_SIZE constant
 #include "string_constraints.hpp"
 
 class bitset_domain_t final {
   private:
-    using bits_t = std::bitset<EBPF_STACK_SIZE>;
+    using bits_t = std::bitset<EBPF_TOTAL_STACK_SIZE>;
     bits_t non_numerical_bytes;
 
   public:
@@ -64,7 +64,7 @@ class bitset_domain_t final {
 
     [[nodiscard]]
     std::pair<bool, bool> uniformity(size_t lb, int width) const {
-        width = std::min(width, (int)(EBPF_STACK_SIZE - lb));
+        width = std::min(width, (int)(EBPF_TOTAL_STACK_SIZE - lb));
         bool only_num = true;
         bool only_non_num = true;
         for (int j = 0; j < width; j++) {
@@ -82,21 +82,21 @@ class bitset_domain_t final {
     [[nodiscard]]
     int all_num_width(size_t lb) const {
         size_t ub = lb;
-        while ((ub < EBPF_STACK_SIZE) && !non_numerical_bytes[ub]) {
+        while ((ub < EBPF_TOTAL_STACK_SIZE) && !non_numerical_bytes[ub]) {
             ub++;
         }
         return (int)(ub - lb);
     }
 
     void reset(size_t lb, int n) {
-        n = std::min(n, (int)(EBPF_STACK_SIZE - lb));
+        n = std::min(n, (int)(EBPF_TOTAL_STACK_SIZE - lb));
         for (int i = 0; i < n; i++) {
             non_numerical_bytes.reset(lb + i);
         }
     }
 
     void havoc(size_t lb, int width) {
-        width = std::min(width, (int)(EBPF_STACK_SIZE - lb));
+        width = std::min(width, (int)(EBPF_TOTAL_STACK_SIZE - lb));
         for (int i = 0; i < width; i++) {
             non_numerical_bytes.set(lb + i);
         }
@@ -109,7 +109,7 @@ class bitset_domain_t final {
     bool all_num(int32_t lb, int32_t ub) const {
         assert(lb < ub);
         lb = std::max(lb, 0);
-        ub = std::min(ub, EBPF_STACK_SIZE);
+        ub = std::min(ub, (int)EBPF_TOTAL_STACK_SIZE);
         if (lb < 0 || ub > (int)non_numerical_bytes.size()) {
             return false;
         }

src/crab/ebpf_domain.cpp

@@ -819,7 +819,7 @@ ebpf_domain_t ebpf_domain_t::calculate_constant_limits() {
         inv += r.svalue >= std::numeric_limits<int32_t>::min();
         inv += r.uvalue <= std::numeric_limits<uint32_t>::max();
         inv += r.uvalue >= 0;
-        inv += r.stack_offset <= EBPF_STACK_SIZE;
+        inv += r.stack_offset <= EBPF_TOTAL_STACK_SIZE;
         inv += r.stack_offset >= 0;
         inv += r.shared_offset <= r.shared_region_size;
         inv += r.shared_offset >= 0;
@@ -937,6 +937,24 @@ void ebpf_domain_t::restore_callee_saved_registers(const std::string& prefix) {
     }
 }
 
+void ebpf_domain_t::havoc_subprogram_stack(const std::string& prefix) {
+    // Calculate the call stack depth being returned from.  Since we're returning
+    // *to* the given prefix, the current call stack is 1 + the number of
+    // '/'-separated labels in the prefix, hence 2 plus the number of separators in the prefix.
+    int call_stack_depth = 2 + std::count(prefix.begin(), prefix.end(), STACK_FRAME_DELIMITER);
+
+    variable_t r10_stack_offset = reg_pack(R10_STACK_POINTER).stack_offset;
+    auto intv = m_inv.eval_interval(r10_stack_offset);
+    if (!intv.is_singleton()) {
+        return;
+    }
+    int64_t stack_offset = intv.singleton()->cast_to<int64_t>();
+    int32_t stack_start = stack_offset - EBPF_SUBPROGRAM_STACK_SIZE * call_stack_depth;
+    for (const data_kind_t kind : iterate_kinds()) {
+        stack.havoc(m_inv, kind, stack_start, EBPF_SUBPROGRAM_STACK_SIZE);
+    }
+}
+
 void ebpf_domain_t::forget_packet_pointers() {
     using namespace crab::dsl_syntax;
 
@@ -1184,10 +1202,16 @@ void ebpf_domain_t::operator()(const basic_block_t& bb) {
 }
 
 void ebpf_domain_t::check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb,
-                                       const linear_expression_t& ub) const {
+                                       const linear_expression_t& ub, int call_stack_depth) const {
     using namespace crab::dsl_syntax;
-    require(inv, lb >= 0, "Lower bound must be at least 0");
-    require(inv, ub <= EBPF_STACK_SIZE, "Upper bound must be at most EBPF_STACK_SIZE");
+    variable_t r10_stack_offset = reg_pack(R10_STACK_POINTER).stack_offset;
+    auto interval = inv.eval_interval(r10_stack_offset);
+    if (interval.is_singleton()) {
+        int64_t stack_offset = interval.singleton()->cast_to<int64_t>();
+        require(inv, lb >= stack_offset - EBPF_SUBPROGRAM_STACK_SIZE * call_stack_depth,
+                "Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE * call_stack_depth");
+    }
+    require(inv, ub <= EBPF_TOTAL_STACK_SIZE, "Upper bound must be at most EBPF_TOTAL_STACK_SIZE");
 }
 
 void ebpf_domain_t::check_access_context(NumAbsDomain& inv, const linear_expression_t& lb,
@@ -1354,6 +1378,7 @@ void ebpf_domain_t::operator()(const Exit& a) {
     if (prefix.empty()) {
         return;
     }
+    havoc_subprogram_stack(prefix);
     restore_callee_saved_registers(prefix);
 }
 
@@ -1371,8 +1396,8 @@ void ebpf_domain_t::operator()(const Comparable& s) {
             return;
         }
         // And, to avoid wraparound errors, they must be within bounds.
-        this->operator()(ValidAccess{s.r1, 0, Imm{0}, false});
-        this->operator()(ValidAccess{s.r2, 0, Imm{0}, false});
+        this->operator()(ValidAccess{MAX_CALL_STACK_FRAMES, s.r1, 0, Imm{0}, false});
+        this->operator()(ValidAccess{MAX_CALL_STACK_FRAMES, s.r2, 0, Imm{0}, false});
     } else {
         // _Maybe_ different types, so r2 must be a number.
         // We checked in a previous assertion that r1 is a pointer or a number.
@@ -1663,7 +1688,7 @@ void ebpf_domain_t::operator()(const ValidAccess& s) {
         }
         case T_STACK: {
             auto [lb, ub] = lb_ub_access_pair(s, reg.stack_offset);
-            check_access_stack(inv, lb, ub);
+            check_access_stack(inv, lb, ub, s.call_stack_depth);
             // if within bounds, it can never be null
             if (s.access_type == AccessType::read) {
                 // Require that the stack range contains numbers.
@@ -2029,8 +2054,13 @@ void ebpf_domain_t::do_mem_store(const Mem& b, Type val_type, SValue val_svalue,
     int width = b.access.width;
     const number_t offset{b.access.offset};
     if (b.access.basereg.v == R10_STACK_POINTER) {
-        const number_t base_addr{EBPF_STACK_SIZE};
-        do_store_stack(m_inv, width, base_addr + offset, val_type, val_svalue, val_uvalue, val_reg);
+        auto r10_stack_offset = reg_pack(b.access.basereg).stack_offset;
+        const auto r10_interval = m_inv.eval_interval(r10_stack_offset);
+        if (r10_interval.is_singleton()) {
+            const int32_t stack_offset = r10_interval.singleton()->cast_to<int32_t>();
+            const number_t base_addr{stack_offset};
+            do_store_stack(m_inv, width, base_addr + offset, val_type, val_svalue, val_uvalue, val_reg);
+        }
         return;
     }
     m_inv = type_inv.join_over_types(m_inv, b.access.basereg, [&](NumAbsDomain& inv, const type_encoding_t type) {
@@ -2892,9 +2922,9 @@ ebpf_domain_t ebpf_domain_t::setup_entry(const bool init_r1) {
     ebpf_domain_t inv;
     const auto r10 = reg_pack(R10_STACK_POINTER);
     constexpr Reg r10_reg{R10_STACK_POINTER};
-    inv += EBPF_STACK_SIZE <= r10.svalue;
+    inv += EBPF_TOTAL_STACK_SIZE <= r10.svalue;
     inv += r10.svalue <= PTR_MAX;
-    inv.assign(r10.stack_offset, EBPF_STACK_SIZE);
+    inv.assign(r10.stack_offset, EBPF_TOTAL_STACK_SIZE);
     // stack_numeric_size would be 0, but TOP has the same result
     // so no need to assign it.
     inv.type_inv.assign_type(inv.m_inv, r10_reg, T_STACK);

src/crab/ebpf_domain.hpp

@@ -149,6 +149,7 @@ class ebpf_domain_t final {
     void scratch_caller_saved_registers();
     void save_callee_saved_registers(const std::string& prefix);
     void restore_callee_saved_registers(const std::string& prefix);
+    void havoc_subprogram_stack(const std::string& prefix);
     [[nodiscard]]
     std::optional<uint32_t> get_map_type(const Reg& map_fd_reg) const;
     [[nodiscard]]
@@ -167,7 +168,7 @@ class ebpf_domain_t final {
     void require(domains::NumAbsDomain& inv, const linear_constraint_t& cst, const std::string& s) const;
 
     // memory check / load / store
-    void check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub) const;
+    void check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub, int call_stack_depth) const;
     void check_access_context(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub) const;
     void check_access_packet(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub,
                              std::optional<variable_t> packet_size) const;

src/ebpf_base.h

@@ -37,3 +37,14 @@ typedef struct _ebpf_context_descriptor {
     int end;  // Offset into ctx struct of pointer to end of data.
     int meta; // Offset into ctx struct of pointer to metadata.
 } ebpf_context_descriptor_t;
+
+// Maximum number of nested function calls allowed in eBPF programs.
+// This limit helps prevent stack overflow and ensures predictable behavior.
+constexpr int MAX_CALL_STACK_FRAMES = 8;
+
+// Stack space allocated for each subprogram (in bytes).
+// This ensures each function call has its own dedicated stack space.
+constexpr int EBPF_SUBPROGRAM_STACK_SIZE = 512;
+
+// Total stack space usable with nested subprogram calls.
+constexpr int EBPF_TOTAL_STACK_SIZE = MAX_CALL_STACK_FRAMES * EBPF_SUBPROGRAM_STACK_SIZE;