Update constants in spec/ebpf_base.rs to be statics

src/crab/array_domain.rs

@@ -87,7 +87,7 @@ pub struct OffsetMap {
 
 impl Default for OffsetMap {
     fn default() -> Self {
-        let n = EBPF_TOTAL_STACK_SIZE as usize;
+        let n = *EBPF_TOTAL_STACK_SIZE as usize;
         OffsetMap {
             sizes: vec![Vec::new(); n],
         }
@@ -241,8 +241,8 @@ fn clamped_bounds(interval: &Interval) -> (i32, i32) {
         .ub()
         .number()
         .and_then(|n| n.to_i64())
-        .map(|n| n.min(EBPF_TOTAL_STACK_SIZE as i64) as i32)
-        .unwrap_or(EBPF_TOTAL_STACK_SIZE);
+        .map(|n| n.min(*EBPF_TOTAL_STACK_SIZE as i64) as i32)
+        .unwrap_or(*EBPF_TOTAL_STACK_SIZE);
     (lb, ub)
 }
 
@@ -412,7 +412,7 @@ impl ArrayDomain {
     }
 
     pub fn to_set(&self) -> StringInvariant {
-        self.num_bytes.to_set()
+        self.num_bytes.clone().to_set()
     }
 
     // ========================================================================
@@ -770,7 +770,7 @@ impl ArrayDomain {
         };
         let idx_i = idx_n.to_i64().unwrap_or(0);
         let width_i = width_n.to_i64().unwrap_or(0);
-        if idx_i + width_i > EBPF_TOTAL_STACK_SIZE as i64 {
+        if idx_i + width_i > *EBPF_TOTAL_STACK_SIZE as i64 {
             return;
         }
         self.num_bytes.reset(idx_i as usize, width_i as i32);

src/crab/bitset_domain.rs

@@ -7,40 +7,44 @@
 //! Each bit represents whether a stack byte is "non-numerical" (bit=1) or
 //! "numerical" (bit=0). Default is all non-numerical (top).
 
+use crate::spec::ebpf_base::EBPF_TOTAL_STACK_SIZE;
 use std::collections::BTreeSet;
 use std::fmt;
-
-use crate::spec::ebpf_base::EBPF_TOTAL_STACK_SIZE;
+use std::sync::LazyLock;
 
 use super::string_constraints::StringInvariant;
 
-const STACK_SIZE: usize = EBPF_TOTAL_STACK_SIZE as usize;
-const NUM_WORDS: usize = STACK_SIZE / 64;
-const _: () = assert!(
-    STACK_SIZE.is_multiple_of(64),
-    "STACK_SIZE must be a multiple of 64"
-);
+static STACK_SIZE: LazyLock<usize> = LazyLock::new(|| {
+    let stack_size = *EBPF_TOTAL_STACK_SIZE as usize;
+    assert!(
+        stack_size.is_multiple_of(64),
+        "STACK_SIZE must be a multiple of 64"
+    );
+    stack_size
+});
+
+static NUM_WORDS: LazyLock<usize> = LazyLock::new(|| *STACK_SIZE / 64);
 
 /// A bitset domain tracking which stack bytes are numerical.
 ///
 /// Each bit `i` indicates whether byte `i` of the stack is non-numerical (1)
 /// or numerical (0).
 /// Top = all non-numerical (all bits set).
 /// Bottom concept is not used (is_bottom always returns false).
-#[derive(Clone, Copy, Debug)]
+#[derive(Clone, Debug)]
 pub struct BitsetDomain {
     /// Bit i is 1 if byte i is non-numerical.
-    bits: [u64; NUM_WORDS],
+    bits: Vec<u64>,
 }
 
-impl BitsetDomain {
-    const ALL_SET: [u64; NUM_WORDS] = [u64::MAX; NUM_WORDS];
-    const ALL_CLEAR: [u64; NUM_WORDS] = [0; NUM_WORDS];
+static ALL_SET: LazyLock<Vec<u64>> = LazyLock::new(|| vec![u64::MAX; *NUM_WORDS]);
+static ALL_CLEAR: LazyLock<Vec<u64>> = LazyLock::new(|| vec![0; *NUM_WORDS]);
 
+impl BitsetDomain {
     /// Create a new BitsetDomain with all bytes non-numerical (top).
     pub fn new() -> Self {
         BitsetDomain {
-            bits: Self::ALL_SET,
+            bits: ALL_SET.clone(),
         }
     }
 
@@ -66,15 +70,15 @@ impl BitsetDomain {
     }
 
     pub fn set_to_top(&mut self) {
-        self.bits = Self::ALL_SET;
+        self.bits.copy_from_slice(&ALL_SET);
     }
 
     pub fn set_to_bottom(&mut self) {
-        self.bits = Self::ALL_CLEAR;
+        self.bits.copy_from_slice(&ALL_CLEAR);
     }
 
     pub fn is_top(&self) -> bool {
-        self.bits == Self::ALL_SET
+        self.bits == *ALL_SET
     }
 
     /// Always false for BitsetDomain (matching C++ semantics).
@@ -104,7 +108,7 @@ impl BitsetDomain {
 
     /// Inclusion: self <= other iff every non-numerical bit in self is also set in other.
     pub fn is_included_in(&self, other: &BitsetDomain) -> bool {
-        for i in 0..NUM_WORDS {
+        for i in 0..*NUM_WORDS {
             // If self has a bit set that other doesn't, not included.
             if self.bits[i] & !other.bits[i] != 0 {
                 return false;
@@ -115,7 +119,7 @@ impl BitsetDomain {
 
     /// Join: bitwise OR (union of non-numerical bytes).
     pub fn join(&self, other: &BitsetDomain) -> BitsetDomain {
-        let mut bits = self.bits;
+        let mut bits = self.bits.clone();
         for (a, b) in bits.iter_mut().zip(&other.bits) {
             *a |= b;
         }
@@ -124,14 +128,14 @@ impl BitsetDomain {
 
     /// Join in place.
     pub fn join_assign(&mut self, other: &BitsetDomain) {
-        for i in 0..NUM_WORDS {
+        for i in 0..*NUM_WORDS {
             self.bits[i] |= other.bits[i];
         }
     }
 
     /// Meet: bitwise AND (intersection of non-numerical bytes).
     pub fn meet(&self, other: &BitsetDomain) -> BitsetDomain {
-        let mut bits = self.bits;
+        let mut bits = self.bits.clone();
         for (a, b) in bits.iter_mut().zip(&other.bits) {
             *a &= b;
         }
@@ -151,10 +155,10 @@ impl BitsetDomain {
     /// Check uniformity of a range [lb, lb+width).
     /// Returns (all_num, all_non_num).
     pub fn uniformity(&self, lb: usize, width: i32) -> (bool, bool) {
-        if lb >= STACK_SIZE {
+        if lb >= *STACK_SIZE {
             return (true, true);
         }
-        let width = width.min((STACK_SIZE - lb) as i32);
+        let width = width.min((*STACK_SIZE - lb) as i32);
         let mut only_num = true;
         let mut only_non_num = true;
         for j in 0..width {
@@ -167,33 +171,33 @@ impl BitsetDomain {
 
     /// Get the number of contiguous numerical bytes starting at lb.
     pub fn all_num_width(&self, lb: usize) -> i32 {
-        if lb >= STACK_SIZE {
+        if lb >= *STACK_SIZE {
             return 0;
         }
         let mut ub = lb;
-        while ub < STACK_SIZE && !self.get_bit(ub) {
+        while ub < *STACK_SIZE && !self.get_bit(ub) {
             ub += 1;
         }
         (ub - lb) as i32
     }
 
     /// Mark bytes [lb, lb+n) as numerical (clear non-numerical bits).
     pub fn reset(&mut self, lb: usize, n: i32) {
-        if lb >= STACK_SIZE {
+        if lb >= *STACK_SIZE {
             return;
         }
-        let n = n.min((STACK_SIZE - lb) as i32);
+        let n = n.min((*STACK_SIZE - lb) as i32);
         for i in 0..n {
             self.clear_bit(lb + i as usize);
         }
     }
 
     /// Mark bytes [lb, lb+width) as non-numerical (set bits).
     pub fn havoc(&mut self, lb: usize, width: i32) {
-        if lb >= STACK_SIZE {
+        if lb >= *STACK_SIZE {
             return;
         }
-        let width = width.min((STACK_SIZE - lb) as i32);
+        let width = width.min((*STACK_SIZE - lb) as i32);
         for i in 0..width {
             self.set_bit(lb + i as usize);
         }
@@ -205,23 +209,23 @@ impl BitsetDomain {
     /// `[start..=end]` where no bit is set (i.e., all bytes are numerical).
     fn numerical_ranges(&self) -> Vec<(usize, usize)> {
         let mut ranges = Vec::new();
-        let mut i: i32 = -(STACK_SIZE as i32);
+        let mut i: i32 = -(*STACK_SIZE as i32);
         while i < 0 {
-            let idx = (STACK_SIZE as i32 + i) as usize;
+            let idx = (*STACK_SIZE as i32 + i) as usize;
             if self.get_bit(idx) {
                 i += 1;
                 continue;
             }
             let start = idx;
             let mut j = i + 1;
             while j < 0 {
-                let jdx = (STACK_SIZE as i32 + j) as usize;
+                let jdx = (*STACK_SIZE as i32 + j) as usize;
                 if self.get_bit(jdx) {
                     break;
                 }
                 j += 1;
             }
-            let end = (STACK_SIZE as i32 + j - 1) as usize;
+            let end = (*STACK_SIZE as i32 + j - 1) as usize;
             ranges.push((start, end));
             i = j;
         }
@@ -234,7 +238,7 @@ impl BitsetDomain {
             return true;
         }
         let lb = lb.max(0);
-        let ub = ub.min(STACK_SIZE as i32);
+        let ub = ub.min(*STACK_SIZE as i32);
         assert!(lb <= ub);
         for i in lb..ub {
             if self.get_bit(i as usize) {
@@ -360,7 +364,7 @@ mod tests {
     fn test_copy_semantics() {
         let mut a = BitsetDomain::new();
         a.reset(0, 8);
-        let b = a; // Copy, not move
+        let b = a.clone(); // Copy, not move
         assert!(!b.get_bit(0));
         a.set_to_top(); // Doesn't affect b
         assert!(!b.get_bit(0));

src/crab/ebpf_checker.rs

@@ -26,7 +26,7 @@ use crate::ir::syntax::{
 };
 use crate::ir::unmarshal::make_call;
 use crate::spec::ebpf_base::{
-    EBPF_SUBPROGRAM_STACK_SIZE, EBPF_TOTAL_STACK_SIZE, MAX_CALL_STACK_FRAMES,
+    EBPF_TOTAL_STACK_SIZE, ebpf_subprogram_stack_size, max_call_stack_frames,
 };
 use crate::spec::vm_isa::R10_STACK_POINTER;
 
@@ -123,14 +123,14 @@ impl<'a> EbpfChecker<'a> {
         // var - expr is not impl?
         // Use full LinearExpression arithmetic
         let lhs = LinearExpression::from(r10.stack_offset)
-            - LinearExpression::from(EBPF_SUBPROGRAM_STACK_SIZE as i64);
+            - LinearExpression::from(ebpf_subprogram_stack_size() as i64);
 
         self.require_value(
             leq(lhs, lb),
             "Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE",
         )?;
         self.require_value(
-            leq(ub, LinearExpression::from(EBPF_TOTAL_STACK_SIZE as i64)),
+            leq(ub, LinearExpression::from(*EBPF_TOTAL_STACK_SIZE as i64)),
             "Upper bound must be at most EBPF_TOTAL_STACK_SIZE",
         )
     }
@@ -255,7 +255,7 @@ impl<'a> EbpfChecker<'a> {
             }
             // And, to avoid wraparound errors, they must be within bounds.
             let va1 = ValidAccess {
-                call_stack_depth: MAX_CALL_STACK_FRAMES,
+                call_stack_depth: max_call_stack_frames(),
                 reg: s.r1,
                 offset: 0,
                 width: Value::Imm(Imm { v: 0 }),
@@ -264,7 +264,7 @@ impl<'a> EbpfChecker<'a> {
             };
             self.check_valid_access(&va1)?;
             let va2 = ValidAccess {
-                call_stack_depth: MAX_CALL_STACK_FRAMES,
+                call_stack_depth: max_call_stack_frames(),
                 reg: s.r2,
                 offset: 0,
                 width: Value::Imm(Imm { v: 0 }),

src/crab/ebpf_domain.rs

@@ -455,7 +455,10 @@ impl EbpfDomain {
             inv.add_value_constraint(&leq(r.uvalue.into(), (u32::MAX as i64).into()), registry);
             inv.add_value_constraint(&geq(r.uvalue.into(), 0i64.into()), registry);
             inv.add_value_constraint(
-                &leq(r.stack_offset.into(), (EBPF_TOTAL_STACK_SIZE as i64).into()),
+                &leq(
+                    r.stack_offset.into(),
+                    (*EBPF_TOTAL_STACK_SIZE as i64).into(),
+                ),
                 registry,
             );
             inv.add_value_constraint(&geq(r.stack_offset.into(), 0i64.into()), registry);
@@ -526,13 +529,13 @@ impl EbpfDomain {
 
         let r10 = reg_pack(&R10_STACK_POINTER, registry);
         inv.add_value_constraint(
-            &leq((EBPF_TOTAL_STACK_SIZE as i64).into(), r10.svalue.into()),
+            &leq((*EBPF_TOTAL_STACK_SIZE as i64).into(), r10.svalue.into()),
             registry,
         );
         inv.add_value_constraint(&leq(r10.svalue.into(), PTR_MAX.into()), registry);
         inv.state
             .values
-            .assign_i64(r10.stack_offset, EBPF_TOTAL_STACK_SIZE as i64, registry);
+            .assign_i64(r10.stack_offset, *EBPF_TOTAL_STACK_SIZE as i64, registry);
         inv.state
             .assign_type_encoding(&R10_STACK_POINTER, T_STACK, registry);
 

src/crab/ebpf_transformer.rs

@@ -257,9 +257,10 @@ fn havoc_subprogram_stack(
     if !intv.is_singleton() {
         return;
     }
-    let stack_start = intv.singleton().unwrap().narrow_to_i64() - EBPF_SUBPROGRAM_STACK_SIZE as i64;
+    let stack_start =
+        intv.singleton().unwrap().narrow_to_i64() - ebpf_subprogram_stack_size() as i64;
     let idx = Interval::from_i64(stack_start);
-    let width = Interval::from_i64(EBPF_SUBPROGRAM_STACK_SIZE as i64);
+    let width = Interval::from_i64(ebpf_subprogram_stack_size() as i64);
     dom.stack.havoc_type(
         &mut dom.state.types,
         &idx,
@@ -1426,7 +1427,7 @@ fn transform_exit(
     add_to_reg(
         dom,
         &R10_STACK_POINTER,
-        EBPF_SUBPROGRAM_STACK_SIZE,
+        ebpf_subprogram_stack_size(),
         64,
         registry,
     );
@@ -1808,7 +1809,7 @@ fn transform_call_local(
     add_to_reg(
         dom,
         &R10_STACK_POINTER,
-        -EBPF_SUBPROGRAM_STACK_SIZE,
+        -ebpf_subprogram_stack_size(),
         64,
         registry,
     );

src/ir/assertions.rs

@@ -9,7 +9,7 @@
 
 use crate::cfg::label::Label;
 use crate::crab::type_encoding::TypeGroup;
-use crate::spec::ebpf_base::EBPF_SUBPROGRAM_STACK_SIZE;
+use crate::spec::ebpf_base::ebpf_subprogram_stack_size;
 use crate::spec::type_descriptors::ProgramInfo;
 use crate::spec::vm_isa::{R0_RETURN_VALUE, R6, R10_STACK_POINTER};
 
@@ -419,7 +419,7 @@ fn assertions_mem(ins: &Mem, info: &ProgramInfo, label: &Option<Label>) -> Vec<A
 
     if basereg == R10_STACK_POINTER {
         // We know we are accessing the stack.
-        if offset < -EBPF_SUBPROGRAM_STACK_SIZE || offset + (width.v as i32) > 0 {
+        if offset < -ebpf_subprogram_stack_size() || offset + (width.v as i32) > 0 {
             // This assertion will fail.
             res.push(Assertion::ValidAccess(make_valid_access(
                 label,

src/ir/program.rs

@@ -21,7 +21,7 @@ use crate::ir::syntax::{
 use crate::ir::unmarshal::conformance_groups;
 use crate::platform::EbpfPlatform;
 use crate::spec::config::EbpfVerifierOptions;
-use crate::spec::ebpf_base::MAX_CALL_STACK_FRAMES;
+use crate::spec::ebpf_base::max_call_stack_frames;
 use crate::spec::type_descriptors::ProgramInfo;
 
 /// Delimiter used between stack frame components in labels.
@@ -1086,7 +1086,7 @@ fn add_cfg_nodes(
         if builder.prog.cfg.contains(&label)
             && let Instruction::CallLocal(cl) = builder.prog.instruction_at(&label)
         {
-            if stack_frame_depth >= MAX_CALL_STACK_FRAMES {
+            if stack_frame_depth >= max_call_stack_frames() {
                 return Err(InvalidControlFlow {
                     message: "too many call stack frames".to_string(),
                 });

src/ir/unmarshal.rs

@@ -471,7 +471,7 @@ impl<'a> Unmarshaller<'a> {
                 }
                 if inst.src() == R10_STACK_POINTER
                     && (inst.offset + width.bytes() as i16 > 0
-                        || inst.offset < -EBPF_TOTAL_STACK_SIZE as i16)
+                        || inst.offset < -*EBPF_TOTAL_STACK_SIZE as i16)
                 {
                     self.note("Stack access out of bounds".to_string());
                 }