Don't change r10

Signed-off-by: Dave Thaler <[email protected]>

src/asm_syntax.hpp

@@ -51,6 +51,16 @@ 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.
+        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 +347,7 @@ enum class AccessType {
 };
 
 struct ValidAccess {
+    int call_stack_depth{};
     Reg reg;
     int32_t offset{};
     Value width{Imm{0}};

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});
             }
@@ -171,13 +177,13 @@ class AssertExtractor {
             // We know we are accessing the stack.
             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/bitset_domain.hpp

@@ -4,7 +4,7 @@
 #include <bitset>
 #include <cassert>
 
-#include "ebpf_base.h" // for EBPF_TOTAL_STACK_SIZE
+#include "ebpf_base.h" // for EBPF_TOTAL_STACK_SIZE constant
 #include "string_constraints.hpp"
 
 class bitset_domain_t final {
@@ -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_TOTAL_STACK_SIZE);
+        ub = std::min(ub, (int32_t)EBPF_TOTAL_STACK_SIZE);
         if (lb < 0 || ub > (int)non_numerical_bytes.size()) {
             return false;
         }

src/crab/ebpf_domain.cpp

@@ -912,8 +912,8 @@ void ebpf_domain_t::scratch_caller_saved_registers() {
 
 void ebpf_domain_t::save_callee_saved_registers(const std::string& prefix) {
     // Create variables specific to the new call stack frame that store
-    // copies of the states of r6 through r10.
-    for (int r = R6; r <= R10_STACK_POINTER; r++) {
+    // copies of the states of r6 through r9.
+    for (int r = R6; r <= R9; r++) {
         for (const data_kind_t kind : iterate_kinds()) {
             const variable_t src_var = variable_t::reg(kind, r);
             if (!m_inv[src_var].is_top()) {
@@ -924,17 +924,7 @@ void ebpf_domain_t::save_callee_saved_registers(const std::string& prefix) {
 }
 
 void ebpf_domain_t::restore_callee_saved_registers(const std::string& prefix) {
-    // First havoc the subprogram's stack.
-    variable_t r10_stack_offset = variable_t::reg(data_kind_t::stack_offsets, R10_STACK_POINTER);
-    auto r10_interval = m_inv.eval_interval(r10_stack_offset);
-    int32_t stack_offset = r10_interval.singleton()->cast_to<int32_t>();
-    int32_t stack_start = stack_offset - EBPF_SUBPROGRAM_STACK_SIZE;
-    for (const data_kind_t kind : iterate_kinds()) {
-        stack.havoc(m_inv, kind, stack_start, EBPF_SUBPROGRAM_STACK_SIZE);
-    }
-
-    // Now restore registers.
-    for (int r = R6; r <= R10_STACK_POINTER; r++) {
+    for (int r = R6; r <= R9; r++) {
         for (const data_kind_t kind : iterate_kinds()) {
             const variable_t src_var = variable_t::stack_frame_var(kind, r, prefix);
             if (!m_inv[src_var].is_top()) {
@@ -947,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.
+    int call_stack_depth = 2 + std::count(prefix.begin(), prefix.end(), '/');
+
+    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;
 
@@ -1194,12 +1202,15 @@ 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;
     variable_t r10_stack_offset = reg_pack(R10_STACK_POINTER).stack_offset;
-    int64_t stack_offset = m_inv.eval_interval(r10_stack_offset).singleton()->cast_to<int64_t>();
-    require(inv, lb >= stack_offset - EBPF_SUBPROGRAM_STACK_SIZE,
-            "Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE");
+    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");
 }
 
@@ -1367,6 +1378,7 @@ void ebpf_domain_t::operator()(const Exit& a) {
     if (prefix.empty()) {
         return;
     }
+    havoc_subprogram_stack(prefix);
     restore_callee_saved_registers(prefix);
 }
 
@@ -1384,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.
@@ -1676,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.
@@ -2044,6 +2056,7 @@ void ebpf_domain_t::do_mem_store(const Mem& b, Type val_type, SValue val_svalue,
     if (b.access.basereg.v == R10_STACK_POINTER) {
         auto r10_stack_offset = reg_pack(b.access.basereg).stack_offset;
         const auto r10_interval = m_inv.eval_interval(r10_stack_offset);
+        assert(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);
@@ -2229,9 +2242,6 @@ void ebpf_domain_t::operator()(const CallLocal& call) {
         return;
     }
     save_callee_saved_registers(call.stack_frame_prefix);
-
-    const auto r10 = reg_pack(R10_STACK_POINTER);
-    sub(r10.stack_offset, EBPF_SUBPROGRAM_STACK_SIZE);
 }
 
 void ebpf_domain_t::operator()(const Callx& callx) {

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

@@ -38,10 +38,13 @@ typedef struct _ebpf_context_descriptor {
     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 per subprogram.
+// 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);
+constexpr int EBPF_TOTAL_STACK_SIZE = MAX_CALL_STACK_FRAMES * EBPF_SUBPROGRAM_STACK_SIZE;