Simplify code

Signed-off-by: Dave Thaler <[email protected]>
vbpf · Oct 11, 2024 · 8aaff6a · 8aaff6a
1 parent de750bb
commit 8aaff6a
Showing 1 changed file with 5 additions and 9 deletions.
diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp
@@ -927,15 +927,13 @@ 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);
-    if (r10_interval.is_singleton()) {
-        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);
-        }
+    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 (const data_kind_t kind : iterate_kinds()) {
             const variable_t src_var = variable_t::stack_frame_var(kind, r, prefix);
@@ -2232,8 +2230,6 @@ void ebpf_domain_t::operator()(const CallLocal& call) {
     }
     save_callee_saved_registers(call.stack_frame_prefix);
 
-    // Lower r10.stack_offset to be the minimum stack area
-    // already initialized.
     const auto r10 = reg_pack(R10_STACK_POINTER);
     sub(r10.stack_offset, EBPF_SUBPROGRAM_STACK_SIZE);
 }