Add test to verify that call local preserves R6-R9 types

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

src/asm_cfg.cpp

@@ -111,7 +111,7 @@ static void add_cfg_nodes(cfg_t& cfg, label_t caller_label, label_t entry_label)
     const int MAX_CALL_STACK_FRAMES = 8;
     for (auto& macro_label : macro_labels) {
         const label_t label(macro_label.from, macro_label.to, caller_label_str);
-        for (const auto inst : cfg.get_node(label)) {
+        for (const auto& inst : cfg.get_node(label)) {
             if (std::holds_alternative<CallLocal>(inst)) {
                 if (stack_frame_depth >= MAX_CALL_STACK_FRAMES)
                     throw std::runtime_error{"too many call stack frames"};

src/crab/cfg.hpp

@@ -315,8 +315,6 @@ class cfg_t final {
 
     [[nodiscard]] size_t size() const { return static_cast<size_t>(std::distance(begin(), end())); }
 
-    void dump_cfg(std::string str);
-
     void simplify() {
         std::set<label_t> worklist(this->label_begin(), this->label_end());
         while (!worklist.empty()) {

src/crab/ebpf_domain.cpp

@@ -995,6 +995,33 @@ 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 r9.
+    for (int r = R6; r <= R9; r++) {
+        for (data_kind_t kind = data_kind_t::types; kind <= data_kind_t::stack_numeric_sizes;
+             kind = (data_kind_t)((int)kind + 1)) {
+            variable_t src_var = variable_t::reg(kind, r);
+            if (!m_inv[src_var].is_top())
+                assign(variable_t::stack_frame_var(kind, r, prefix), src_var);
+        }
+    }
+}
+
+void ebpf_domain_t::restore_callee_saved_registers(const std::string& prefix) {
+    for (int r = R6; r <= R9; r++) {
+        for (data_kind_t kind = data_kind_t::types; kind <= data_kind_t::stack_numeric_sizes;
+             kind = (data_kind_t)((int)kind + 1)) {
+            variable_t src_var = variable_t::stack_frame_var(kind, r, prefix);
+            if (!m_inv[src_var].is_top())
+                assign(variable_t::reg(kind, r), src_var);
+            else
+                havoc(variable_t::reg(kind, r));
+            havoc(src_var);
+        }
+    }
+}
+
 void ebpf_domain_t::forget_packet_pointers() {
     using namespace crab::dsl_syntax;
 
@@ -1546,15 +1573,7 @@ void ebpf_domain_t::operator()(const Exit& a) {
     std::string prefix = a.stack_frame_prefix;
     if (prefix.empty())
         return;
-    for (int r = R6; r <= R9; r++) {
-        for (data_kind_t kind = data_kind_t::types; kind <= data_kind_t::stack_numeric_sizes;
-             kind = (data_kind_t)((int)kind + 1)) {
-            variable_t src_var = variable_t::stack_frame_var(kind, r, prefix);
-            if (!m_inv[src_var].is_top())
-                assign(variable_t::reg(kind, r), src_var);
-            havoc(src_var);
-        }
-    }
+    restore_callee_saved_registers(prefix);
 }
 
 void ebpf_domain_t::operator()(const Jmp& a) {}
@@ -2380,16 +2399,7 @@ void ebpf_domain_t::operator()(const CallLocal& call) {
     using namespace crab::dsl_syntax;
     if (m_inv.is_bottom())
         return;
-
-    // Create variables specific to the new call stack frame that store
-    // copies of the states of r6 through r9.
-    for (int r = R6; r <= R9; r++) {
-        for (data_kind_t kind = data_kind_t::types; kind <= data_kind_t::stack_numeric_sizes; kind = (data_kind_t)((int)kind + 1)) {
-            variable_t src_var = variable_t::reg(kind, r);
-            if (!m_inv[src_var].is_top())
-                assign(variable_t::stack_frame_var(kind, r, call.stack_frame_prefix), src_var);
-        }
-    }
+    save_callee_saved_registers(call.stack_frame_prefix);
 }
 
 void ebpf_domain_t::operator()(const Callx& callx) {

src/crab/ebpf_domain.hpp

@@ -159,6 +159,8 @@ class ebpf_domain_t final {
     [[nodiscard]] std::optional<variable_t> get_type_offset_variable(const Reg& reg) const;
 
     void scratch_caller_saved_registers();
+    void save_callee_saved_registers(const std::string& prefix);
+    void restore_callee_saved_registers(const std::string& prefix);
     [[nodiscard]] std::optional<uint32_t> get_map_type(const Reg& map_fd_reg) const;
     [[nodiscard]] std::optional<uint32_t> get_map_inner_map_fd(const Reg& map_fd_reg) const;
     [[nodiscard]] crab::interval_t get_map_key_size(const Reg& map_fd_reg) const;

test-data/calllocal.yaml

@@ -227,3 +227,22 @@ post: ["r0.type=number"]
 
 messages:
   - "0/2: tail call not supported in subprogram (valid call(tail_call))"
+---
+test-case: call local must preserve R6-R9 types
+
+pre: ["r6.type=packet"]
+
+code:
+  <start>: |
+    call <sub>
+    r0 = 0
+    exit
+  <sub>: |
+    r6 = 1
+    exit
+
+post:
+  - r0.type=number
+  - r0.svalue=0
+  - r0.uvalue=0
+  - r6.type=packet