From ddc3a161a453a622f0342677c754e9ad086daccd Mon Sep 17 00:00:00 2001 From: Venus Xeon-Blonde Date: Mon, 6 Apr 2026 15:24:59 -0400 Subject: [PATCH 1/4] Update constants in spec/ebpf_base.rs to be statics, using OnceLock and LazyLock where appropriate. Rust does not support build-time definitions in the same way used in https://github.com/vbpf/prevail/pull/1060, so we instead make those constants into global statics, which may be initialized once before any other library functions are called (otherwise they'll use the existing defaults). All references to those constants have been updated to use the statics, which unfortunately means that the implementation of crab/bitset_domain.rs is no longer constant size, and now uses `Vec`s. Signed-off-by: Venus Xeon-Blonde --- src/crab/array_domain.rs | 10 +++--- src/crab/bitset_domain.rs | 67 ++++++++++++++++++------------------ src/crab/ebpf_checker.rs | 12 +++---- src/crab/ebpf_domain.rs | 6 ++-- src/crab/ebpf_transformer.rs | 8 ++--- src/ir/assertions.rs | 4 +-- src/ir/program.rs | 4 +-- src/ir/unmarshal.rs | 2 +- src/result.rs | 8 ++--- src/spec/ebpf_base.rs | 23 +++++++++++-- tests/conformance_tests.rs | 10 +++--- 11 files changed, 85 insertions(+), 69 deletions(-) diff --git a/src/crab/array_domain.rs b/src/crab/array_domain.rs index 75ee520..8e2a5e0 100644 --- a/src/crab/array_domain.rs +++ b/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); diff --git a/src/crab/bitset_domain.rs b/src/crab/bitset_domain.rs index 5017ec7..3e0f649 100644 --- a/src/crab/bitset_domain.rs +++ b/src/crab/bitset_domain.rs @@ -9,17 +9,18 @@ use std::collections::BTreeSet; use std::fmt; - +use std::sync::LazyLock; use crate::spec::ebpf_base::EBPF_TOTAL_STACK_SIZE; 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" -); +const STACK_SIZE: LazyLock = 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 +}); + +const NUM_WORDS: LazyLock = LazyLock::new(|| *STACK_SIZE / 64); /// A bitset domain tracking which stack bytes are numerical. /// @@ -27,20 +28,20 @@ const _: () = assert!( /// 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, } impl BitsetDomain { - const ALL_SET: [u64; NUM_WORDS] = [u64::MAX; NUM_WORDS]; - const ALL_CLEAR: [u64; NUM_WORDS] = [0; NUM_WORDS]; + const ALL_SET: LazyLock> = LazyLock::new(|| vec![u64::MAX; *NUM_WORDS]); + const ALL_CLEAR: LazyLock> = LazyLock::new(|| vec![0; *NUM_WORDS]); /// Create a new BitsetDomain with all bytes non-numerical (top). pub fn new() -> Self { BitsetDomain { - bits: Self::ALL_SET, + bits: Self::ALL_SET.clone(), } } @@ -66,15 +67,15 @@ impl BitsetDomain { } pub fn set_to_top(&mut self) { - self.bits = Self::ALL_SET; + self.bits.copy_from_slice(&*Self::ALL_SET); } pub fn set_to_bottom(&mut self) { - self.bits = Self::ALL_CLEAR; + self.bits.copy_from_slice(&*Self::ALL_CLEAR); } pub fn is_top(&self) -> bool { - self.bits == Self::ALL_SET + self.bits == *Self::ALL_SET } /// Always false for BitsetDomain (matching C++ semantics). @@ -104,7 +105,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 +116,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 +125,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 +152,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,11 +168,11 @@ 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 @@ -179,10 +180,10 @@ impl BitsetDomain { /// 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); } @@ -190,10 +191,10 @@ impl BitsetDomain { /// 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,9 +206,9 @@ 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; @@ -215,13 +216,13 @@ impl BitsetDomain { 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 +235,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 +361,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)); diff --git a/src/crab/ebpf_checker.rs b/src/crab/ebpf_checker.rs index 1849178..a78fce5 100644 --- a/src/crab/ebpf_checker.rs +++ b/src/crab/ebpf_checker.rs @@ -25,9 +25,7 @@ use crate::ir::syntax::{ ValidStore, Value, ZeroCtxOffset, }; use crate::ir::unmarshal::make_call; -use crate::spec::ebpf_base::{ - EBPF_SUBPROGRAM_STACK_SIZE, EBPF_TOTAL_STACK_SIZE, MAX_CALL_STACK_FRAMES, -}; +use crate::spec::ebpf_base::{ebpf_subprogram_stack_size, max_call_stack_frames, EBPF_TOTAL_STACK_SIZE}; use crate::spec::vm_isa::R10_STACK_POINTER; pub fn ebpf_domain_check( @@ -123,14 +121,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 +253,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 +262,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 }), diff --git a/src/crab/ebpf_domain.rs b/src/crab/ebpf_domain.rs index 2555823..d672a25 100644 --- a/src/crab/ebpf_domain.rs +++ b/src/crab/ebpf_domain.rs @@ -455,7 +455,7 @@ 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 +526,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); diff --git a/src/crab/ebpf_transformer.rs b/src/crab/ebpf_transformer.rs index 34ca608..786cfcb 100644 --- a/src/crab/ebpf_transformer.rs +++ b/src/crab/ebpf_transformer.rs @@ -257,9 +257,9 @@ 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 +1426,7 @@ fn transform_exit( add_to_reg( dom, &R10_STACK_POINTER, - EBPF_SUBPROGRAM_STACK_SIZE, + ebpf_subprogram_stack_size(), 64, registry, ); @@ -1808,7 +1808,7 @@ fn transform_call_local( add_to_reg( dom, &R10_STACK_POINTER, - -EBPF_SUBPROGRAM_STACK_SIZE, + -ebpf_subprogram_stack_size(), 64, registry, ); diff --git a/src/ir/assertions.rs b/src/ir/assertions.rs index 1d1d1d8..3da3b74 100644 --- a/src/ir/assertions.rs +++ b/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