Make max packet size a runtime parameter

src/config.hpp

@@ -61,8 +61,12 @@ struct ebpf_verifier_options_t {
     // Maximum number of nested function calls.
     int max_call_stack_frames = 8;
 
+    // Maximum packet size in bytes (upper bound on packet_size).
+    int max_packet_size = 0xffff;
+
     static constexpr int MAX_SUBPROGRAM_STACK_SIZE = 1024 * 1024;
     static constexpr int MAX_CALL_STACK_FRAMES_LIMIT = 128;
+    static constexpr int MAX_PACKET_SIZE_LIMIT = (1 << 30);
 
     [[nodiscard]]
     int total_stack_size() const noexcept {
@@ -80,6 +84,10 @@ struct ebpf_verifier_options_t {
                                         std::to_string(MAX_CALL_STACK_FRAMES_LIMIT) + "], got " +
                                         std::to_string(max_call_stack_frames));
         }
+        if (max_packet_size <= 0 || max_packet_size > MAX_PACKET_SIZE_LIMIT) {
+            throw std::invalid_argument("max_packet_size must be in [1, " + std::to_string(MAX_PACKET_SIZE_LIMIT) +
+                                        "], got " + std::to_string(max_packet_size));
+        }
     }
 
     verbosity_options_t verbosity_opts;

src/crab/ebpf_checker.cpp

@@ -102,8 +102,8 @@ void EbpfChecker::check_access_packet(const LinearExpression& lb, const LinearEx
     if (packet_size) {
         require_value(dom.state, ub <= *packet_size, "Upper bound must be at most packet_size");
     } else {
-        require_value(dom.state, ub <= MAX_PACKET_SIZE,
-                      std::string{"Upper bound must be at most "} + std::to_string(MAX_PACKET_SIZE));
+        require_value(dom.state, ub <= max_packet_size(),
+                      std::string{"Upper bound must be at most "} + std::to_string(max_packet_size()));
     }
 }
 

src/crab/ebpf_domain.cpp

@@ -350,7 +350,7 @@ void EbpfDomain::initialize_packet() {
     inv.havoc(variable_registry->meta_offset());
 
     inv.add_value_constraint(0 <= variable_registry->packet_size());
-    inv.add_value_constraint(variable_registry->packet_size() < MAX_PACKET_SIZE);
+    inv.add_value_constraint(variable_registry->packet_size() < max_packet_size());
     const auto info = *thread_local_program_info;
     if (info.type.context_descriptor->meta >= 0) {
         inv.add_value_constraint(variable_registry->meta_offset() <= 0);
@@ -408,7 +408,7 @@ EbpfDomain EbpfDomain::setup_entry(const bool init_r1) {
     constexpr Reg r10_reg{R10_STACK_POINTER};
     const auto total_stack = thread_local_options.total_stack_size();
     inv.state.values.add_constraint(total_stack <= r10.svalue);
-    inv.state.values.add_constraint(r10.svalue <= PTR_MAX);
+    inv.state.values.add_constraint(r10.svalue <= ptr_max());
     inv.state.values.assign(r10.stack_offset, total_stack);
     // stack_numeric_size would be 0, but TOP has the same result
     // so no need to assign it.
@@ -418,7 +418,7 @@ EbpfDomain EbpfDomain::setup_entry(const bool init_r1) {
         const auto r1 = reg_pack(R1_ARG);
         constexpr Reg r1_reg{R1_ARG};
         inv.state.values.add_constraint(1 <= r1.svalue);
-        inv.state.values.add_constraint(r1.svalue <= PTR_MAX);
+        inv.state.values.add_constraint(r1.svalue <= ptr_max());
         inv.state.values.assign(r1.ctx_offset, 0);
         inv.state.assign_type(r1_reg, T_CTX);
     }

src/crab/ebpf_domain.hpp

@@ -4,9 +4,11 @@
 
 // This file is eBPF-specific, not derived from CRAB.
 
+#include <limits>
 #include <optional>
 
 #include "arith/variable.hpp"
+#include "config.hpp"
 #include "crab/array_domain.hpp"
 #include "crab/type_to_num.hpp"
 #include "string_constraints.hpp"
@@ -19,8 +21,8 @@ namespace prevail {
 // the offsets get replaced with 64-bit address pointers.  However, we currently
 // need to do pointer arithmetic on 64-bit numbers so for now we cap the interval
 // to 32 bits.
-constexpr int MAX_PACKET_SIZE = 0xffff;
-constexpr int64_t PTR_MAX = std::numeric_limits<int32_t>::max() - MAX_PACKET_SIZE;
+inline int max_packet_size() noexcept { return thread_local_options.max_packet_size; }
+inline int64_t ptr_max() noexcept { return std::numeric_limits<int32_t>::max() - thread_local_options.max_packet_size; }
 
 class EbpfDomain;
 

src/crab/ebpf_transformer.cpp

@@ -518,7 +518,7 @@ static void do_load_ctx(TypeToNumDomain& state, const Reg& target_reg, const Lin
             // EXPERIMENTAL: Explicit upper bound since packet_size is min_only.
             // This preserves the relational constraint (packet_offset <= packet_size)
             // while ensuring comparison checks have a concrete upper bound.
-            state.values.add_constraint(target.packet_offset < MAX_PACKET_SIZE);
+            state.values.add_constraint(target.packet_offset < max_packet_size());
         }
     } else if (addr == desc->meta) {
         if (width == offset_width) {
@@ -535,7 +535,7 @@ static void do_load_ctx(TypeToNumDomain& state, const Reg& target_reg, const Lin
     if (width == offset_width) {
         state.assign_type(target_reg, T_PACKET);
         state.values.add_constraint(4098 <= target.svalue);
-        state.values.add_constraint(target.svalue <= PTR_MAX);
+        state.values.add_constraint(target.svalue <= ptr_max());
     }
 }
 
@@ -1049,7 +1049,7 @@ void EbpfTransformer::assign_valid_ptr(const Reg& dst_reg, const bool maybe_null
     } else {
         dom.state.values.add_constraint(0 < reg.svalue);
     }
-    dom.state.values.add_constraint(reg.svalue <= PTR_MAX);
+    dom.state.values.add_constraint(reg.svalue <= ptr_max());
     dom.state.values.assign(reg.uvalue, reg.svalue);
 }
 

src/main.cpp

@@ -97,6 +97,11 @@ int main(int argc, char** argv) {
         ->group("Features")
         ->check(CLI::Range(1, ebpf_verifier_options_t::MAX_CALL_STACK_FRAMES_LIMIT));
 
+    app.add_option("--max-packet-size", ebpf_verifier_options.max_packet_size,
+                   "Maximum packet size in bytes (default: 65535)")
+        ->group("Features")
+        ->check(CLI::Range(1, ebpf_verifier_options_t::MAX_PACKET_SIZE_LIMIT));
+
     std::set<std::string> include_groups = get_conformance_group_names();
     app.add_option("--include_groups", include_groups, "Include conformance groups")
         ->group("Features")