Fix bpf2bpf local function calls with stack usage (#784)

Signed-off-by: Dave Thaler <[email protected]>
vbpf · Nov 9, 2024 · 41fbd5a · 41fbd5a
1 parent 71a34c7
commit 41fbd5a
Show file tree

Hide file tree

Showing 8 changed files with 24 additions and 22 deletions.
diff --git a/ebpf-samples b/ebpf-samples
diff --git a/src/asm_ostream.hpp b/src/asm_ostream.hpp
@@ -17,7 +17,7 @@ inline std::function<int16_t(label_t)> label_to_offset16(const pc_t pc) {
         const int64_t offset = label.from - gsl::narrow<int64_t>(pc) - 1;
         const bool is16 =
             std::numeric_limits<int16_t>::min() <= offset && offset <= std::numeric_limits<int16_t>::max();
-        return is16 ? gsl::narrow<int16_t>(offset) : 0;
+        return gsl::narrow<int16_t>(is16 ? offset : 0);
     };
 }
 

diff --git a/src/asm_syntax.hpp b/src/asm_syntax.hpp
@@ -59,7 +59,7 @@ struct label_t {
         if (stack_frame_prefix.empty()) {
             return 1;
         }
-        return 2 + std::ranges::count(stack_frame_prefix, STACK_FRAME_DELIMITER);
+        return gsl::narrow<int>(2 + std::ranges::count(stack_frame_prefix, STACK_FRAME_DELIMITER));
     }
 
     friend std::ostream& operator<<(std::ostream& os, const label_t& label) {

diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp
@@ -938,18 +938,12 @@ 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 2 + the number of
-    // '/' separators because we need to account for the current frame and the root frame.
-    const int call_stack_depth = 2 + std::ranges::count(prefix, STACK_FRAME_DELIMITER);
-
     const variable_t r10_stack_offset = reg_pack(R10_STACK_POINTER).stack_offset;
     const auto intv = m_inv.eval_interval(r10_stack_offset);
     if (!intv.is_singleton()) {
         return;
     }
-    const int64_t stack_offset = intv.singleton()->cast_to<int64_t>();
-    const int32_t stack_start = stack_offset - EBPF_SUBPROGRAM_STACK_SIZE * call_stack_depth;
+    const int64_t stack_start = intv.singleton()->cast_to<int64_t>() - EBPF_SUBPROGRAM_STACK_SIZE;
     for (const data_kind_t kind : iterate_kinds()) {
         stack.havoc(m_inv, kind, stack_start, EBPF_SUBPROGRAM_STACK_SIZE);
     }
@@ -1212,15 +1206,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 int call_stack_depth) const {
+void ebpf_domain_t::check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb,
+                                       const linear_expression_t& ub) const {
     using namespace crab::dsl_syntax;
     const variable_t r10_stack_offset = reg_pack(R10_STACK_POINTER).stack_offset;
     const auto interval = inv.eval_interval(r10_stack_offset);
     if (interval.is_singleton()) {
         const 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, lb >= stack_offset - EBPF_SUBPROGRAM_STACK_SIZE,
+                "Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE");
     }
     require(inv, ub <= EBPF_TOTAL_STACK_SIZE, "Upper bound must be at most EBPF_TOTAL_STACK_SIZE");
 }
@@ -1391,6 +1385,10 @@ void ebpf_domain_t::operator()(const Exit& a) {
     }
     havoc_subprogram_stack(prefix);
     restore_callee_saved_registers(prefix);
+
+    // Restore r10.
+    constexpr Reg r10_reg{R10_STACK_POINTER};
+    add(r10_reg, EBPF_SUBPROGRAM_STACK_SIZE, 64);
 }
 
 void ebpf_domain_t::operator()(const Jmp&) const {
@@ -1709,7 +1707,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, s.call_stack_depth);
+            check_access_stack(inv, lb, ub);
             // if within bounds, it can never be null
             if (s.access_type == AccessType::read) {
                 // Require that the stack range contains numbers.
@@ -2258,6 +2256,10 @@ void ebpf_domain_t::operator()(const CallLocal& call) {
         return;
     }
     save_callee_saved_registers(call.stack_frame_prefix);
+
+    // Update r10.
+    constexpr Reg r10_reg{R10_STACK_POINTER};
+    add(r10_reg, -EBPF_SUBPROGRAM_STACK_SIZE, 64);
 }
 
 void ebpf_domain_t::operator()(const Callx& callx) {

diff --git a/src/crab/ebpf_domain.hpp b/src/crab/ebpf_domain.hpp
@@ -171,8 +171,7 @@ class ebpf_domain_t final {
     void require(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,
-                            int call_stack_depth) const;
+    void check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub) 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;

diff --git a/test-data/calllocal.yaml b/test-data/calllocal.yaml
@@ -347,14 +347,14 @@ code:
     r0 += r1              ; r0 = 1 + 2 + 3 = 6
     exit
   <sub1>: |
-    *(u8 *)(r10 - 513) = 2
+    *(u8 *)(r10 - 1) = 2
     call <sub2>
-    r1 = *(u8 *)(r10 - 513)
+    r1 = *(u8 *)(r10 - 1)
     r0 += r1              ; r0 = 2 + 3 = 5
     exit
   <sub2>: |
-    *(u8 *)(r10 - 1025) = 3
-    r0 = *(u8 *)(r10 - 1025)
+    *(u8 *)(r10 - 1) = 3
+    r0 = *(u8 *)(r10 - 1)
     exit
 
 post:

diff --git a/test-data/stack.yaml b/test-data/stack.yaml
@@ -594,4 +594,4 @@ post:
   - s[511].uvalue=0
 
 messages:
-  - "0: Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE * call_stack_depth (valid_access(r10.offset-513, width=1) for write)"
+  - "0: Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE (valid_access(r10.offset-513, width=1) for write)"
diff --git a/test-data/subtract.yaml b/test-data/subtract.yaml
@@ -159,3 +159,4 @@ post:
   - r10.stack_offset=4096
 messages:
   - "0: Upper bound must be at most EBPF_TOTAL_STACK_SIZE (r2.type == number or r1.type == r2.type in {ctx, stack, packet})"
+  - "0: Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE (r2.type == number or r1.type == r2.type in {ctx, stack, packet})"