ebpf/

verifier.rs

// Copyright 2024 The Fuchsia Authors. All rights reserved.
// Use of this source code is governed by a BSD-style license that can be
// found in the LICENSE file.

#![allow(unused_variables)]

use crate::scalar_value::{ScalarValueData, U32Range, U32ScalarValueData, U64Range};
use crate::visitor::{BpfVisitor, ProgramCounter, Register, Source};
use crate::{
    BPF_ATOMIC, BPF_CALL, BPF_CLS_MASK, BPF_CMPXCHG, BPF_DW, BPF_EXIT, BPF_JA, BPF_JMP, BPF_JMP32,
    BPF_LDDW, BPF_MAX_INSTS, BPF_PSEUDO_MAP_IDX, BPF_PSEUDO_MAP_IDX_VALUE, BPF_STACK_SIZE, BPF_STX,
    BPF_SUB_OP_MASK, BPF_W, DataWidth, EbpfInstruction, GENERAL_REGISTER_COUNT, MapFlags,
    MapSchema, REGISTER_COUNT, VerifierError, VerifierErrorKind,
};
use byteorder::{BigEndian, ByteOrder, LittleEndian, NativeEndian};
use linux_uapi::{bpf_map_type, bpf_map_type_BPF_MAP_TYPE_ARRAY};
#[cfg(target_os = "fuchsia")]
use starnix_sync::{EbpfVerifierDependenciesLock, LockDepMutex};
use std::cmp::Ordering;
use std::collections::{BTreeMap, HashMap, HashSet};
use std::sync::Arc;
use zerocopy::IntoBytes;

const U32_MAX: u64 = u32::MAX as u64;

/// A trait to receive the log from the verifier.
pub trait VerifierLogger {
    /// Returns whether logging is currently enabled and can accept output.
    ///
    /// Verifiers check this before evaluating log messages or formatting strings.
    fn is_enabled(&self) -> bool {
        true
    }

    /// Log a line. The line is always a correct encoded ASCII string.
    fn log(&mut self, line: &[u8]);
}

/// A `VerifierLogger` that drops all its content.
pub struct NullVerifierLogger;

impl VerifierLogger for NullVerifierLogger {
    fn is_enabled(&self) -> bool {
        false
    }

    fn log(&mut self, line: &[u8]) {
        debug_assert!(line.is_ascii());
    }
}

/// An identifier for a memory buffer accessible by an ebpf program. The identifiers are built as a
/// chain of unique identifier so that a buffer can contain multiple pointers to the same type and
/// the verifier can distinguish between the different instances.
/// The namespace of a `MemoryId`, used to prevent collisions between different
/// sources of identifiers.
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug, Ord, PartialOrd)]
pub enum Namespace {
    /// For static structure identifiers (e.g., `SkBuff`, `BpfSock`) defined in `program_type.rs`.
    Hardcoded,
    /// For IDs generated by `MemoryId::new()` using the global counter.
    Generated,
    /// For IDs generated by `VerificationContext::next_id()` using the local counter.
    Verification,
}

#[derive(Clone, Debug, PartialEq, Eq, Hash, Ord, PartialOrd)]
pub struct MemoryId {
    namespace: Namespace,
    id: u64,
    parent: Option<Box<MemoryId>>,
}

impl MemoryId {
    pub fn id(&self) -> u64 {
        self.id
    }
}

impl From<u64> for MemoryId {
    fn from(id: u64) -> Self {
        Self { namespace: Namespace::Hardcoded, id, parent: None }
    }
}

/// A counter that allows to generate new ids for parameters. The namespace is the same as for id
/// generated for types while verifying an ebpf program. Because different sources of identifiers
/// use different namespaces, this counter can start at 0.
static BPF_TYPE_IDENTIFIER_COUNTER: std::sync::atomic::AtomicU64 =
    std::sync::atomic::AtomicU64::new(0);

impl MemoryId {
    /// Build a `MemoryId` from a raw u64.
    ///
    /// This is supposed to be used by the `ebpf_api` crate to build static identifiers (e.g.
    /// for hardcoded program contexts like `SkBuff`), but not elsewhere.
    pub const fn from_raw(id: u64) -> MemoryId {
        Self { namespace: Namespace::Hardcoded, id, parent: None }
    }

    pub fn new() -> MemoryId {
        Self {
            namespace: Namespace::Generated,
            id: BPF_TYPE_IDENTIFIER_COUNTER.fetch_add(1, std::sync::atomic::Ordering::Relaxed),
            parent: None,
        }
    }

    /// Build a new id such that `other` is prepended to the chain of parent of `self`.
    fn prepended(&self, other: MemoryId) -> Self {
        match &self.parent {
            None => {
                MemoryId { namespace: self.namespace, id: self.id, parent: Some(Box::new(other)) }
            }
            Some(parent) => MemoryId {
                namespace: self.namespace,
                id: self.id,
                parent: Some(Box::new(parent.prepended(other))),
            },
        }
    }

    /// Returns whether the parent of `self` is `parent`
    fn has_parent(&self, parent: &MemoryId) -> bool {
        match &self.parent {
            None => false,
            Some(p) => p.as_ref() == parent,
        }
    }

    /// Returns whether `self` and `other` represent the same type. This is true if both have the
    /// same id and if they both have parent, parents must also match.
    fn matches(&self, other: &MemoryId) -> bool {
        if self.namespace != other.namespace || self.id != other.id {
            return false;
        };
        match (&self.parent, &other.parent) {
            (Some(p1), Some(p2)) => p1.matches(p2.as_ref()),
            _ => true,
        }
    }
}

/// The type of a field in a struct pointed by `Type::PtrToStruct`.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum FieldType {
    /// Read-only scalar value.
    Scalar { size: usize },

    /// Mutable scalar value.
    MutableScalar { size: usize },

    /// A pointer to the kernel memory. The full buffer is `buffer_size` bytes long.
    PtrToMemory { is_32_bit: bool, id: MemoryId, buffer_size: usize },

    /// A nullable pointer to the kernel memory. The full buffer is `buffer_size` bytes long.
    NullablePtrToMemory { is_32_bit: bool, id: MemoryId, buffer_size: usize },

    /// A pointer to the kernel memory. The full buffer size is determined by an instance of
    /// `PtrToEndArray` with the same `id`.
    PtrToArray { is_32_bit: bool, id: MemoryId },

    /// A pointer to the kernel memory that represents the first non accessible byte of a
    /// `PtrToArray` with the same `id`.
    PtrToEndArray { is_32_bit: bool, id: MemoryId },
}

/// Definition of a field in a `Type::PtrToStruct`.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct FieldDescriptor {
    /// The offset at which the field is located.
    pub offset: usize,

    /// The type of the pointed memory. Currently the verifier supports only `PtrToArray`,
    /// `PtrToStruct`, `PtrToEndArray` and `ScalarValue`.
    pub field_type: FieldType,
}

impl FieldDescriptor {
    fn size(&self) -> usize {
        match self.field_type {
            FieldType::Scalar { size } | FieldType::MutableScalar { size } => size,
            FieldType::PtrToMemory { is_32_bit, .. }
            | FieldType::NullablePtrToMemory { is_32_bit, .. }
            | FieldType::PtrToArray { is_32_bit, .. }
            | FieldType::PtrToEndArray { is_32_bit, .. } => {
                if is_32_bit {
                    4
                } else {
                    8
                }
            }
        }
    }
}

/// The offset and width of a field in a struct.
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
struct Field {
    offset: i16,
    width: DataWidth,
}

impl Field {
    fn new(offset: i16, width: DataWidth) -> Self {
        Self { offset, width }
    }
}

/// Defines field layout in a struct pointed by `Type::PtrToStruct`.
#[derive(Debug, PartialEq, Eq, Default)]
pub struct StructDescriptor {
    /// The list of fields.
    pub fields: Vec<FieldDescriptor>,
}

impl StructDescriptor {
    /// Return true if `self` is a subtype of `super_struct`.
    fn is_subtype(&self, super_struct: &StructDescriptor) -> bool {
        // Check that `super_struct.fields` is a subset of `fields`.
        for super_field in super_struct.fields.iter() {
            if self.fields.iter().find(|field| *field == super_field).is_none() {
                return false;
            }
        }
        true
    }

    /// Finds the field type for load/store at the specified location. None is returned if the
    /// access is invalid and the program must be rejected.
    fn find_field(&self, base_offset: ScalarValueData, field: Field) -> Option<&FieldDescriptor> {
        let offset = base_offset + field.offset;
        let field_desc = self.fields.iter().find(|f| {
            f.offset <= offset.min() as usize && (offset.max() as usize) < f.offset + f.size()
        })?;
        let is_valid_load = match field_desc.field_type {
            FieldType::Scalar { size } | FieldType::MutableScalar { size } => {
                // For scalars check that the access is within the bounds of the field.
                ((offset + field.width.bytes()).max() as usize) <= field_desc.offset + size
            }
            FieldType::PtrToMemory { is_32_bit, .. }
            | FieldType::NullablePtrToMemory { is_32_bit, .. }
            | FieldType::PtrToArray { is_32_bit, .. }
            | FieldType::PtrToEndArray { is_32_bit, .. } => {
                let expected_width = if is_32_bit { DataWidth::U32 } else { DataWidth::U64 };
                // Pointer loads are expected to load the whole field.
                offset.is_known()
                    && offset.value as usize == field_desc.offset
                    && field.width == expected_width
            }
        };

        is_valid_load.then_some(field_desc)
    }
}

#[derive(Clone, Debug, PartialEq, Eq)]
pub enum MemoryParameterSize {
    /// The memory buffer have the given size.
    Value(u64),
    /// The memory buffer size is given by the parameter in the given index.
    Reference { index: u8 },
}

impl MemoryParameterSize {
    fn size(&self, context: &ComputationContext) -> Result<u64, VerifierErrorKind> {
        match self {
            Self::Value(size) => Ok(*size),
            Self::Reference { index } => {
                let size_type = context.reg(index + 1)?;
                match size_type {
                    Type::ScalarValue(data) if data.is_known() => Ok(data.value),
                    _ => Err(VerifierErrorKind::NonConstantBufferSize),
                }
            }
        }
    }
}

#[derive(Clone, Debug, PartialEq, Eq)]
pub enum MapTypeFilter {
    AllowList(&'static [bpf_map_type]),
    DenyList(&'static [bpf_map_type]),
}

impl MapTypeFilter {
    pub fn is_allowed(&self, map_type: bpf_map_type) -> bool {
        match self {
            MapTypeFilter::AllowList(types) => types.contains(&map_type),
            MapTypeFilter::DenyList(types) => !types.contains(&map_type),
        }
    }
}

/// Indicates the origin and mutability of a memory buffer referenced by
/// `Type::PtrToMemory`.
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub enum PointerOrigin {
    /// A pointer to a value in a read-only eBPF map (`BPF_F_RDONLY_PROG`).
    MapReadOnly,
    /// A pointer to a value in a writable eBPF map.
    MapWritable,
    /// A read-only pointer to kernel memory (e.g., packet payload in
    /// `sk_buff`).
    KernelReadOnly,
    /// A writable pointer to kernel memory.
    KernelWritable,
}

impl PointerOrigin {
    /// Returns true if the memory referenced by this pointer can be written to.
    pub fn is_writable(self) -> bool {
        match self {
            Self::MapWritable | Self::KernelWritable => true,
            Self::MapReadOnly | Self::KernelReadOnly => false,
        }
    }

    /// Returns true if the pointer points to an eBPF map value.
    pub fn is_map_value(self) -> bool {
        match self {
            Self::MapReadOnly | Self::MapWritable => true,
            Self::KernelReadOnly | Self::KernelWritable => false,
        }
    }
}

#[derive(Clone, Debug, PartialEq, Eq)]
pub enum Type {
    /// A number.
    ScalarValue(ScalarValueData),
    /// A pointer to a map object.
    ConstPtrToMap { id: u64, schema: MapSchema },
    /// A pointer into the stack.
    PtrToStack { offset: StackOffset },
    /// A pointer to the kernel memory. The full buffer is `buffer_size` bytes long. The pointer is
    /// situated at `offset` from the start of the buffer.
    PtrToMemory { id: MemoryId, offset: ScalarValueData, buffer_size: u64, origin: PointerOrigin },
    /// A pointer to a struct with the specified `StructDescriptor`.
    PtrToStruct { id: MemoryId, offset: ScalarValueData, descriptor: Arc<StructDescriptor> },
    /// A pointer to the kernel memory. The full buffer size is determined by an instance of
    /// `PtrToEndArray` with the same `id`. The pointer is situadted at `offset` from the start of
    /// the buffer.
    PtrToArray { id: MemoryId, offset: ScalarValueData },
    /// A pointer to the kernel memory that represents the first non accessible byte of a
    /// `PtrToArray` with the same `id`.
    PtrToEndArray { id: MemoryId },
    /// A pointer that might be null and must be validated before being referenced.
    NullOr { id: MemoryId, inner: Box<Type> },
    /// An object that must be passed to a method with an associated `ReleaseParameter` before the
    /// end of the program.
    Releasable { id: MemoryId, inner: Box<Type> },
    /// A function parameter that must be a `ScalarValue` when called.
    ScalarValueParameter,
    /// A function parameter that must be a `ConstPtrToMap` when called.
    ConstPtrToMapParameter { filter: MapTypeFilter, must_be_writable: bool },
    /// A function parameter that must be a key of a map.
    MapKeyParameter {
        /// The index in the arguments list that contains a `ConstPtrToMap` for the map this key is
        /// associated with.
        map_ptr_index: u8,
    },
    /// A function parameter that must be a value of a map.
    MapValueParameter {
        /// The index in the arguments list that contains a `ConstPtrToMap` for the map this key is
        /// associated with.
        map_ptr_index: u8,
    },
    /// A function parameter that must be a pointer to memory.
    MemoryParameter {
        /// The index in the arguments list that contains a scalar value containing the size of the
        /// memory.
        size: MemoryParameterSize,
        /// Whether this memory is read by the function.
        input: bool,
        /// Whether this memory is written by the function.
        output: bool,
    },
    /// A function return value that is the same type as a parameter.
    AliasParameter {
        /// The index in the argument list of the parameter that has the type of this return value.
        parameter_index: u8,
    },
    /// A function return value that is either null, or the given type.
    NullOrParameter(Box<Type>),
    /// A function parameter that must be a pointer to memory with the given id.
    StructParameter { id: MemoryId },
    /// The parameter should be the same as the specified argument passed to the program.
    ContextParameter { parameter_index: u8 },
    /// A function return value that must be passed to a method with an associated
    /// `ReleaseParameter` before the end of the program.
    ReleasableParameter { id: MemoryId, inner: Box<Type> },
    /// A function parameter that will release the value.
    ReleaseParameter { id: MemoryId },
    /// A function parameter that is not checked.
    AnyParameter,
}

/// Defines a partial ordering on `Type` instances, capturing the notion of how "broad"
/// a type is in terms of the set of potential values it represents.
///
/// The ordering is defined such that `t1 > t2` if a proof that an eBPF program terminates
/// in a state where a register or memory location has type `t1` is also a proof that
/// the program terminates in a state where that location has type `t2`.
///
/// In other words, a "broader" type represents a larger set of possible values, and
/// proving termination with a broader type implies termination with any narrower type.
///
/// Examples:
/// * `Type::ScalarValue(ScalarValueData({ unknown_mask: 0, .. }))` (a known scalar value) is less than
///   `Type::ScalarValue(ScalarValueData({ unknown_mask: u64::MAX, .. }))` (an unknown scalar value).
impl PartialOrd for Type {
    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
        // UNINITIALIZED is treated as the Top element (Greater than all other types).
        // If a path is proven safe when a register is UNINITIALIZED, it means the path
        // does not read that register. Consequently, it is safe to prune any state
        // that has a more specific type (like a pointer) in that register, because
        // the program will still not read it.
        match (self, other) {
            (Self::ScalarValue(data1), Self::ScalarValue(data2)) => data1.partial_cmp(data2),
            (Self::ScalarValue(data), _) => {
                (*data == ScalarValueData::UNINITIALIZED).then_some(Ordering::Greater)
            }
            (_, Self::ScalarValue(data)) => {
                (*data == ScalarValueData::UNINITIALIZED).then_some(Ordering::Less)
            }
            // If the values are equal, return the known result.
            _ if self == other => Some(Ordering::Equal),
            _ => None,
        }
    }
}

impl From<ScalarValueData> for Type {
    fn from(value: ScalarValueData) -> Self {
        Self::ScalarValue(value)
    }
}

impl From<u64> for Type {
    fn from(value: u64) -> Self {
        Self::ScalarValue(value.into())
    }
}

impl Default for Type {
    /// A new instance of `Type` where no bit has been written yet.
    fn default() -> Self {
        Self::UNINITIALIZED.clone()
    }
}

impl Type {
    /// An uninitialized value.
    pub const UNINITIALIZED: Self = Self::ScalarValue(ScalarValueData::UNINITIALIZED);

    /// A `Type` where the data is usable by userspace, but the value is not known by the verifier.
    pub const UNKNOWN_SCALAR: Self = Self::ScalarValue(ScalarValueData::UNKNOWN_WRITTEN);

    /// The mask associated with a data of size `width`.
    fn mask(width: DataWidth) -> u64 {
        if width == DataWidth::U64 { u64::MAX } else { (1 << width.bits()) - 1 }
    }

    /// Return true if `self` is a scalar with all bytes initialized.
    fn is_written_scalar(&self) -> bool {
        match self {
            Self::ScalarValue(data) if data.is_fully_initialized() => true,
            _ => false,
        }
    }

    /// Return true if `self` has all bytes initialized.
    fn is_initialized(&self) -> bool {
        match self {
            Self::ScalarValue(data) => data.is_fully_initialized(),
            _ => true,
        }
    }

    /// Return true if `self` is a subtype of `super_type`.
    pub fn is_subtype(&self, super_type: &Type) -> bool {
        match (self, super_type) {
            // Anything can be used in place of an uninitialized value.
            (_, Self::ScalarValue(data)) if data.is_uninitialized() => true,

            (
                Self::PtrToStruct { id: id1, offset: offset1, descriptor: descriptor1 },
                Self::PtrToStruct { id: id2, offset: offset2, descriptor: descriptor2 },
            ) => id1 == id2 && offset1 <= offset2 && descriptor1.is_subtype(descriptor2),

            // Every type is a subtype of itself.
            (self_type, super_type) if self_type == super_type => true,

            _ => false,
        }
    }

    /// Return true is `self` is guaranteed to be non-zero
    pub fn is_non_zero(&self) -> bool {
        match self {
            Self::ScalarValue(d) => d.min() > 0,
            Self::NullOr { .. } => false,
            _ => true,
        }
    }

    fn inner(&self, context: &ComputationContext) -> Result<&Type, VerifierErrorKind> {
        match self {
            Self::Releasable { id, inner } => {
                if context.resources.contains(id) {
                    Ok(&inner)
                } else {
                    Err(VerifierErrorKind::UseAfterRelease)
                }
            }
            _ => Ok(self),
        }
    }

    /// Constraints `type1` and `type2` for a conditional jump with the specified `jump_type` and
    /// `jump_width`.
    fn constraint(
        context: &mut ComputationContext,
        jump_type: JumpType,
        jump_width: JumpWidth,
        type1: Self,
        type2: Self,
    ) -> Result<(Self, Self), VerifierErrorKind> {
        let result = match (jump_width, jump_type, type1.inner(context)?, type2.inner(context)?) {
            (JumpWidth::W64, JumpType::Eq, Type::ScalarValue(data1), Type::ScalarValue(data2))
                if data1.is_fully_initialized() && data2.is_fully_initialized() =>
            {
                let umin = std::cmp::max(data1.min(), data2.min());
                let umax = std::cmp::min(data1.max(), data2.max());
                let v = Type::ScalarValue(ScalarValueData::new(
                    data1.value | data2.value,
                    data1.unknown_mask & data2.unknown_mask,
                    0,
                    U64Range::new(umin, umax),
                ));
                (v.clone(), v)
            }
            (JumpWidth::W32, JumpType::Eq, Type::ScalarValue(data1), Type::ScalarValue(data2))
                if data1.is_fully_initialized() && data2.is_fully_initialized() =>
            {
                // Refine ranges only when both operands fit in 32 bits; a range
                // straddling 2^32 can have low bits below its min, so refining would
                // drop reachable values.
                let both_fit_u32 = data1.max() <= U32_MAX && data2.max() <= U32_MAX;
                let (urange1, urange2) = if both_fit_u32 {
                    let umin = std::cmp::max(data1.min(), data2.min());
                    let umax = std::cmp::min(data1.max(), data2.max());
                    let urange = U64Range::new(umin, umax);
                    (urange, urange)
                } else {
                    (data1.urange, data2.urange)
                };
                let v1 = Type::ScalarValue(ScalarValueData::new(
                    data1.value | (data2.value & U32_MAX),
                    data1.unknown_mask & (data2.unknown_mask | (U32_MAX << 32)),
                    0,
                    urange1,
                ));
                let v2 = Type::ScalarValue(ScalarValueData::new(
                    data2.value | (data1.value & U32_MAX),
                    data2.unknown_mask & (data1.unknown_mask | (U32_MAX << 32)),
                    0,
                    urange2,
                ));
                (v1, v2)
            }
            (JumpWidth::W64, JumpType::Eq, Type::ScalarValue(data), Type::NullOr { id, .. })
            | (JumpWidth::W64, JumpType::Eq, Type::NullOr { id, .. }, Type::ScalarValue(data))
                if data.is_zero() =>
            {
                context.set_null(id, true);
                let zero = Type::from(0);
                (zero.clone(), zero)
            }
            (JumpWidth::W64, jump_type, Type::NullOr { id, inner }, Type::ScalarValue(data))
                if jump_type.is_strict() && data.is_zero() =>
            {
                context.set_null(id, false);
                let inner = *inner.clone();
                inner.register_resource(context);
                (inner, type2)
            }
            (JumpWidth::W64, jump_type, Type::ScalarValue(data), Type::NullOr { id, inner })
                if jump_type.is_strict() && data.is_zero() =>
            {
                context.set_null(id, false);
                let inner = *inner.clone();
                inner.register_resource(context);
                (type1, inner)
            }

            (JumpWidth::W64, JumpType::Lt, Type::ScalarValue(lhs), Type::ScalarValue(rhs)) => {
                debug_assert!(lhs.min() < u64::MAX);
                debug_assert!(rhs.max() > 0);
                let new_max_lhs = std::cmp::min(lhs.max(), rhs.max() - 1);
                debug_assert!(lhs.min() <= new_max_lhs);
                let new_min_rhs = std::cmp::max(rhs.min(), lhs.min() + 1);
                debug_assert!(new_min_rhs <= rhs.max());
                let new_range_lhs = U64Range::new(lhs.min(), new_max_lhs);
                let new_range_rhs = U64Range::new(new_min_rhs, rhs.max());
                (lhs.update_range(new_range_lhs).into(), rhs.update_range(new_range_rhs).into())
            }
            (JumpWidth::W64, JumpType::Gt, Type::ScalarValue(lhs), Type::ScalarValue(rhs)) => {
                debug_assert!(rhs.min() < u64::MAX);
                debug_assert!(lhs.max() > 0);
                let new_min_lhs = std::cmp::max(lhs.min(), rhs.min() + 1);
                debug_assert!(new_min_lhs <= lhs.max());
                let new_max_rhs = std::cmp::min(rhs.max(), lhs.max() - 1);
                debug_assert!(rhs.min() <= new_max_rhs);
                let new_range_lhs = U64Range::new(new_min_lhs, lhs.max());
                let new_range_rhs = U64Range::new(rhs.min(), new_max_rhs);
                (lhs.update_range(new_range_lhs).into(), rhs.update_range(new_range_rhs).into())
            }

            (JumpWidth::W64, JumpType::Le, Type::ScalarValue(lhs), Type::ScalarValue(rhs)) => {
                let new_max_lhs = std::cmp::min(lhs.max(), rhs.max());
                debug_assert!(lhs.min() <= new_max_lhs);
                let new_min_rhs = std::cmp::max(rhs.min(), lhs.min());
                debug_assert!(new_min_rhs <= rhs.max());
                let new_range_lhs = U64Range::new(lhs.min(), new_max_lhs);
                let new_range_rhs = U64Range::new(new_min_rhs, rhs.max());
                (lhs.update_range(new_range_lhs).into(), rhs.update_range(new_range_rhs).into())
            }
            (JumpWidth::W64, JumpType::Ge, Type::ScalarValue(lhs), Type::ScalarValue(rhs)) => {
                let new_min_lhs = std::cmp::max(lhs.min(), rhs.min());
                debug_assert!(new_min_lhs <= lhs.max());
                let new_max_rhs = std::cmp::min(rhs.max(), lhs.max());
                debug_assert!(rhs.min() <= new_max_rhs);
                let new_range_lhs = U64Range::new(new_min_lhs, lhs.max());
                let new_range_rhs = U64Range::new(rhs.min(), new_max_rhs);
                (lhs.update_range(new_range_lhs).into(), rhs.update_range(new_range_rhs).into())
            }

            (
                JumpWidth::W64,
                JumpType::Eq,
                Type::PtrToArray { id: id1, offset },
                Type::PtrToEndArray { id: id2 },
            )
            | (
                JumpWidth::W64,
                JumpType::Le,
                Type::PtrToArray { id: id1, offset },
                Type::PtrToEndArray { id: id2 },
            )
            | (
                JumpWidth::W64,
                JumpType::Ge,
                Type::PtrToEndArray { id: id1 },
                Type::PtrToArray { id: id2, offset },
            ) if id1 == id2 => {
                context.update_array_bounds(id1.clone(), *offset);
                (type1, type2)
            }
            (
                JumpWidth::W64,
                JumpType::Lt,
                Type::PtrToArray { id: id1, offset },
                Type::PtrToEndArray { id: id2 },
            )
            | (
                JumpWidth::W64,
                JumpType::Gt,
                Type::PtrToEndArray { id: id1 },
                Type::PtrToArray { id: id2, offset },
            ) if id1 == id2 => {
                context.update_array_bounds(id1.clone(), *offset + 1);
                (type1, type2)
            }
            (JumpWidth::W64, JumpType::Eq, _, _) => (type1.clone(), type1),
            _ => (type1, type2),
        };
        Ok(result)
    }

    fn match_parameter_type(
        &self,
        verification_context: &VerificationContext<'_>,
        context: &ComputationContext,
        helper_name: &str,
        parameter_type: &Type,
        index: usize,
        next: &mut ComputationContext,
    ) -> Result<(), VerifierErrorKind> {
        match (parameter_type, self) {
            (Type::NullOrParameter(t), Type::ScalarValue(data))
                if data.is_known() && data.value == 0 =>
            {
                Ok(())
            }
            (Type::NullOrParameter(t), _) => self.match_parameter_type(
                verification_context,
                context,
                helper_name,
                t,
                index,
                next,
            ),
            (Type::ScalarValueParameter, Type::ScalarValue(data))
                if data.is_fully_initialized() =>
            {
                Ok(())
            }
            (
                Type::ConstPtrToMapParameter { filter, must_be_writable },
                Type::ConstPtrToMap { schema, .. },
            ) => {
                if *must_be_writable && schema.flags.contains(MapFlags::ProgReadOnly) {
                    return Err(VerifierErrorKind::WriteToReadOnlyMap);
                }
                let map_type = schema.map_type;
                if !filter.is_allowed(map_type) {
                    return Err(VerifierErrorKind::InvalidMapTypeForHelper(map_type));
                }
                Ok(())
            }
            (
                Type::MapKeyParameter { map_ptr_index },
                Type::PtrToMemory { offset, buffer_size, .. },
            ) => {
                let schema = context.get_map_schema(*map_ptr_index)?;
                context.check_memory_access(*offset, *buffer_size, 0, schema.key_size as usize)
            }
            (Type::MapKeyParameter { map_ptr_index }, Type::PtrToStack { offset }) => {
                let schema = context.get_map_schema(*map_ptr_index)?;
                context.stack.read_data_ptr(*offset, schema.key_size as u64)
            }
            (
                Type::MapValueParameter { map_ptr_index },
                Type::PtrToMemory { offset, buffer_size, .. },
            ) => {
                let schema = context.get_map_schema(*map_ptr_index)?;
                context.check_memory_access(*offset, *buffer_size, 0, schema.value_size as usize)
            }
            (Type::MapValueParameter { map_ptr_index }, Type::PtrToStack { offset }) => {
                let schema = context.get_map_schema(*map_ptr_index)?;
                context.stack.read_data_ptr(*offset, schema.value_size as u64)
            }
            (
                Type::MemoryParameter { size, output, .. },
                Type::PtrToMemory { offset, buffer_size, origin, .. },
            ) => {
                if *output && !origin.is_writable() {
                    return Err(VerifierErrorKind::WriteToReadOnlyMemory);
                }
                let expected_size = size.size(context)?;
                let offset_max = offset.max();
                if offset_max > *buffer_size {
                    return Err(VerifierErrorKind::OutOfBoundsMemoryAccess);
                }
                let size_left = *buffer_size - offset_max;
                if expected_size > size_left {
                    return Err(VerifierErrorKind::OutOfBoundsMemoryAccess);
                }
                Ok(())
            }

            (Type::MemoryParameter { size, input, output }, Type::PtrToStack { offset }) => {
                let size = size.size(context)?;
                let buffer_end = offset.add(size);
                if !buffer_end.is_within_stack() {
                    Err(VerifierErrorKind::OutOfBoundsMemoryAccess)
                } else {
                    if *output {
                        next.stack.write_data_ptr(*offset, size)?;
                    }
                    if *input {
                        context.stack.read_data_ptr(*offset, size)?;
                    }
                    Ok(())
                }
            }
            (
                Type::StructParameter { id: id1 },
                Type::PtrToMemory { id: id2, offset, .. }
                | Type::PtrToStruct { id: id2, offset, .. },
            ) if offset.is_zero() && id1.matches(id2) => Ok(()),
            (
                Type::ReleasableParameter { id: id1, inner: inner1 },
                Type::Releasable { id: id2, inner: inner2 },
            ) if id2.has_parent(id1) => {
                if next.resources.contains(id2) {
                    inner2.match_parameter_type(
                        verification_context,
                        context,
                        helper_name,
                        inner1,
                        index,
                        next,
                    )
                } else {
                    Err(VerifierErrorKind::UseAfterRelease)
                }
            }
            (Type::ContextParameter { parameter_index }, arg_type) => {
                if verification_context.calling_context.args.get(*parameter_index as usize)
                    == Some(arg_type)
                {
                    Ok(())
                } else {
                    Err(VerifierErrorKind::ExpectedProgramArgument(*parameter_index))
                }
            }
            (Type::ReleaseParameter { id: id1 }, Type::Releasable { id: id2, .. })
                if id2.has_parent(id1) =>
            {
                if next.resources.remove(id2) {
                    Ok(())
                } else {
                    Err(VerifierErrorKind::DoubleRelease)
                }
            }
            (_, Type::Releasable { id, inner }) => {
                if !next.resources.contains(id) {
                    return Err(VerifierErrorKind::UseAfterRelease);
                }
                inner.match_parameter_type(
                    verification_context,
                    context,
                    helper_name,
                    parameter_type,
                    index,
                    next,
                )
            }
            (Type::AnyParameter, _) => Ok(()),

            _ => Err(VerifierErrorKind::HelperArgumentTypeMismatch(index)),
        }
    }

    /// If this `Type` is an instance of NullOr with the given `null_id`, replace it wither either
    /// 0 or the subtype depending on `is_null`
    fn set_null(&mut self, null_id: &MemoryId, is_null: bool) {
        match self {
            Type::NullOr { id, inner } if id == null_id => {
                if is_null {
                    *self = Type::from(0);
                } else {
                    *self = *inner.clone();
                }
            }
            _ => {}
        }
    }

    fn register_resource(&self, context: &mut ComputationContext) {
        match self {
            Type::Releasable { id, .. } => {
                context.resources.insert(id.clone());
            }
            _ => {}
        }
    }

    /// Partially Compares two iterators of comparable items.
    ///
    /// This function iterates through both input iterators simultaneously and compares the corresponding elements.
    /// The comparison continues until:
    /// 1. Both iterators are exhausted and all elements were considered equal, in which case it returns `Some(Ordering::Equal)`.
    /// 2. All pairs of corresponding elements that are not equal have the same ordering (`Ordering::Less` or `Ordering::Greater`), in which case it returns `Some(Ordering)` reflecting that consistent ordering.
    /// 3. One iterator is exhausted before the other, or any comparison between elements yields `None`, or not all non-equal pairs have the same ordering, in which case it returns `None`.
    fn compare_list<'a>(
        mut l1: impl Iterator<Item = &'a Self>,
        mut l2: impl Iterator<Item = &'a Self>,
    ) -> Option<Ordering> {
        let mut result = Ordering::Equal;
        loop {
            match (l1.next(), l2.next()) {
                (None, None) => return Some(result),
                (_, None) | (None, _) => return None,
                (Some(v1), Some(v2)) => {
                    result = associate_orderings(result, v1.partial_cmp(v2)?)?;
                }
            }
        }
    }
}

#[derive(Clone, Debug)]
pub struct FunctionSignature {
    pub args: Vec<Type>,
    pub return_value: Type,
    pub invalidate_array_bounds: bool,
}

#[derive(Clone, Debug)]
pub struct HelperDefinition {
    pub index: u32,
    pub name: &'static str,
    pub signature: FunctionSignature,
}

#[derive(Debug, Default)]
pub struct CallingContext {
    /// List of map schemas of the associated map. The maps can be accessed using LDDW instruction
    /// with `src_reg=BPF_PSEUDO_MAP_IDX`.
    pub maps: Vec<MapSchema>,
    /// The registered external functions.
    pub helpers: HashMap<u32, &'static HelperDefinition>,
    /// The args of the program.
    pub args: Vec<Type>,
    /// Packet type. Normally it should be either `None` or `args[0]`.
    pub packet_type: Option<Type>,
}

impl CallingContext {
    pub fn register_map(&mut self, schema: MapSchema) -> usize {
        let index = self.maps.len();
        self.maps.push(schema);
        index
    }
}

#[derive(Debug, PartialEq, Eq, Clone)]
pub struct StructAccess {
    pub pc: ProgramCounter,

    // Memory Id of the struct being accessed.
    pub memory_id: MemoryId,

    // Offset of the field being loaded.
    pub field_offset: usize,

    // Indicates that this is a 32-bit pointer load. These instructions must be remapped.
    pub is_32_bit_ptr_load: bool,
}

#[derive(Debug, Clone)]
pub struct VerifiedEbpfProgram {
    pub(crate) code: Vec<EbpfInstruction>,
    pub(crate) args: Vec<Type>,
    pub(crate) struct_access_instructions: Vec<StructAccess>,
    pub(crate) maps: Vec<MapSchema>,
}

impl VerifiedEbpfProgram {
    pub fn code(&self) -> &[EbpfInstruction] {
        &self.code
    }

    pub fn struct_access_instructions(&self) -> &[StructAccess] {
        &self.struct_access_instructions
    }

    pub fn from_verified_code(
        code: Vec<EbpfInstruction>,
        args: Vec<Type>,
        struct_access_instructions: Vec<StructAccess>,
        maps: Vec<MapSchema>,
    ) -> Self {
        Self { code, args, struct_access_instructions, maps }
    }

    pub fn maps(&self) -> &[MapSchema] {
        &self.maps
    }
}

/// Verify the given code depending on the type of the parameters and the registered external
/// functions. Returned `VerifiedEbpfProgram` should be linked in order to execute it.
pub fn verify_program(
    code: Vec<EbpfInstruction>,
    calling_context: CallingContext,
    logger: &mut dyn VerifierLogger,
) -> Result<VerifiedEbpfProgram, VerifierError> {
    if code.len() > BPF_MAX_INSTS {
        return error_and_log(
            logger,
            VerifierError { kind: VerifierErrorKind::ProgramTooLarge, pc: None },
        );
    }
    // Pre-scan the program to ensure all LDDW instructions are structurally well-formed,
    // even if they are in unreachable code. This is necessary because:
    // 1. The linker may rewrite LDDW instructions (e.g., to resolve map pointers) and
    //    expects them to be well-formed.
    // 2. It ensures that the second part of every LDDW has a `code` of 0 (invalid opcode).
    //    This guarantees that any attempt to jump directly into the second part of an
    //    LDDW will be rejected during verification as an invalid instruction.
    //
    // It also computes the prune points: the targets of the jumps and the instructions following
    // a conditional jump or a `cmpxchg` (which also branches into two states). Every loop and
    // every join of two branches goes through one of them, and the states are only compared with
    // and recorded as terminating contexts at these points.
    let mut terminating_contexts: Vec<Option<TerminatingContexts>> =
        (0..code.len()).map(|_| None).collect();
    let mut scan_pc = 0;
    while scan_pc < code.len() {
        let inst = &code[scan_pc];
        if inst.code() == BPF_LDDW {
            let Some(next_instruction) = code.get(scan_pc + 1) else {
                return error_and_log(
                    logger,
                    VerifierError { kind: VerifierErrorKind::IncompleteLddw, pc: Some(scan_pc) },
                );
            };
            if next_instruction.code() != 0
                || next_instruction.offset() != 0
                || next_instruction.src_reg() != 0
                || next_instruction.dst_reg() != 0
            {
                return error_and_log(
                    logger,
                    VerifierError { kind: VerifierErrorKind::MalformedLddw, pc: Some(scan_pc) },
                );
            }
            scan_pc += 2;
        } else {
            let class = inst.code() & BPF_CLS_MASK;
            let op = inst.code() & BPF_SUB_OP_MASK;
            let is_cmpxchg = (inst.code() == (BPF_STX | BPF_ATOMIC | BPF_W)
                || inst.code() == (BPF_STX | BPF_ATOMIC | BPF_DW))
                && inst.imm() as u8 == BPF_CMPXCHG;
            if (class == BPF_JMP || class == BPF_JMP32) && op != BPF_CALL && op != BPF_EXIT {
                // Invalid targets are ignored here, and rejected if they are reached.
                let target = scan_pc.checked_add_signed(isize::from(inst.offset()) + 1);
                if let Some(entry) = target.and_then(|pc| terminating_contexts.get_mut(pc)) {
                    *entry = Some(Default::default());
                }
                if op != BPF_JA {
                    if let Some(entry) = terminating_contexts.get_mut(scan_pc + 1) {
                        *entry = Some(Default::default());
                    }
                }
            } else if is_cmpxchg {
                if let Some(entry) = terminating_contexts.get_mut(scan_pc + 1) {
                    *entry = Some(Default::default());
                }
            }
            scan_pc += 1;
        }
    }

    let mut context = ComputationContext::default();
    for (i, t) in calling_context.args.iter().enumerate() {
        // The parameter registers are r1 to r5.
        context
            .set_reg((i + 1) as u8, t.clone())
            .map_err(|kind| VerifierError { kind, pc: None })?;
    }
    let states = vec![context];
    let mut verification_context =
        VerificationContext::new(calling_context, logger, &code, states, terminating_contexts);
    while let Some(mut context) = verification_context.states.pop() {
        if let Some(Some(terminating_contexts)) =
            verification_context.terminating_contexts.get(context.pc)
        {
            // Check whether there exist a context that terminate and prove that this context does
            // also terminate.
            if let Some(ending_context) = terminating_contexts.find_greater_or_equal(&context) {
                // One such context has been found, this proves the current context terminates.
                // If the context has a parent, register the data dependencies and try to terminate
                // it.
                if let Some(parent) = context.parent.take() {
                    parent.dependencies.lock().merge(ending_context.dependencies);
                    if let Some(parent) = Arc::into_inner(parent) {
                        parent.terminate(&mut verification_context)?;
                    }
                }
                continue;
            }
        }
        if verification_context.iteration > 10 * BPF_MAX_INSTS {
            return error_and_log(
                verification_context.logger,
                VerifierError { kind: VerifierErrorKind::ComplexityLimitExceeded, pc: None },
            );
        }
        if context.pc >= code.len() {
            return error_and_log(
                verification_context.logger,
                VerifierError { kind: VerifierErrorKind::FellOffProgramEnd, pc: Some(context.pc) },
            );
        }
        if let Err(kind) = context.visit(&mut verification_context, code[context.pc]) {
            return error_and_log(
                verification_context.logger,
                VerifierError { kind, pc: Some(context.pc) },
            );
        }
        if context.terminated {
            context.terminate(&mut verification_context)?;
        }
        verification_context.iteration += 1;
    }

    let struct_access_instructions =
        verification_context.struct_access_instructions.into_values().collect::<Vec<_>>();
    let CallingContext { maps, args, .. } = verification_context.calling_context;
    Ok(VerifiedEbpfProgram { code, struct_access_instructions, maps, args })
}

struct VerificationContext<'a> {
    /// The type information for the program arguments and the registered functions.
    calling_context: CallingContext,
    /// The logger to use.
    logger: &'a mut dyn VerifierLogger,
    /// The `ComputationContext` yet to be validated.
    states: Vec<ComputationContext>,
    /// The program being analyzed.
    code: &'a [EbpfInstruction],
    /// A counter used to generated unique ids for memory buffers and maps.
    counter: u64,
    /// The current iteration of the verifier. Used to ensure termination by limiting the number of
    /// iteration before bailing out.
    iteration: usize,
    /// Keep track of the context that terminates at a given pc. The list of context will all be
    /// incomparables as each time a bigger context is computed, the smaller ones are removed from
    /// the list. Indexed directly by `ProgramCounter` (`0..code.len()`) for O(1) lookup, and
    /// `None` if the pc is not a prune point.
    terminating_contexts: Vec<Option<TerminatingContexts>>,
    /// The current set of struct access instructions that will need to be updated when the
    /// program is linked. This is also used to ensure that a given instruction always loads the
    /// same field. If this is not the case, the verifier will reject the program.
    struct_access_instructions: HashMap<ProgramCounter, StructAccess>,
}

impl<'a> VerificationContext<'a> {
    fn new(
        calling_context: CallingContext,
        logger: &'a mut dyn VerifierLogger,
        code: &'a [EbpfInstruction],
        states: Vec<ComputationContext>,
        terminating_contexts: Vec<Option<TerminatingContexts>>,
    ) -> Self {
        debug_assert_eq!(code.len(), terminating_contexts.len());
        Self {
            calling_context,
            logger,
            states,
            code,
            counter: 0,
            iteration: 0,
            terminating_contexts,
            struct_access_instructions: Default::default(),
        }
    }

    fn next_id(&mut self) -> MemoryId {
        let id = self.counter;
        self.counter += 1;
        MemoryId { namespace: Namespace::Verification, id, parent: None }
    }

    /// Register an instruction that loads or stores a struct field. These instructions will need
    /// to updated later when the program is linked.
    fn register_struct_access(
        &mut self,
        struct_access: StructAccess,
    ) -> Result<(), VerifierErrorKind> {
        match self.struct_access_instructions.entry(struct_access.pc) {
            std::collections::hash_map::Entry::Vacant(entry) => {
                entry.insert(struct_access);
            }
            std::collections::hash_map::Entry::Occupied(entry) => {
                if *entry.get() != struct_access {
                    return Err(VerifierErrorKind::InconsistentStructFieldAccess);
                }
            }
        }
        Ok(())
    }
}

const STACK_ELEMENT_SIZE: usize = std::mem::size_of::<u64>();

/// An offset inside the stack. The offset is from the end of the stack.
/// downward.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct StackOffset(ScalarValueData);

impl Default for StackOffset {
    fn default() -> Self {
        Self(BPF_STACK_SIZE.into())
    }
}

impl StackOffset {
    /// Returns an error if the current offset is not valid for element access, distinguishing
    /// variable offsets from out of bounds ones.
    fn check_valid_offset(&self) -> Result<(), VerifierErrorKind> {
        if !self.0.is_known() {
            return Err(VerifierErrorKind::VariableStackOffset);
        }
        if self.0.value >= (BPF_STACK_SIZE as u64) {
            return Err(VerifierErrorKind::StackAccessOutOfBounds);
        }
        Ok(())
    }

    /// Whether the current offset is within the stack bounds, inclusive of `BPF_STACK_SIZE`.
    fn is_within_stack(&self) -> bool {
        self.0.is_known() && self.0.value <= (BPF_STACK_SIZE as u64)
    }

    /// The value of the register.
    fn reg(&self) -> ScalarValueData {
        self.0
    }

    /// The index into the stack array this offset points to. Can be called only if
    /// `is_within_stack()` is true.
    fn array_index(&self) -> usize {
        debug_assert!(self.is_within_stack());
        usize::try_from(self.0.value).unwrap() / STACK_ELEMENT_SIZE
    }

    /// The offset inside the aligned u64 in the stack.
    fn sub_index(&self) -> usize {
        debug_assert!(self.is_within_stack());
        usize::try_from(self.0.value).unwrap() % STACK_ELEMENT_SIZE
    }

    fn add<T: Into<ScalarValueData>>(self, rhs: T) -> Self {
        Self(self.0 + rhs)
    }
}

// The initialized elements of the stack are tracked in a `u64` bitmask.
const _: () = assert!(BPF_STACK_SIZE / STACK_ELEMENT_SIZE <= u64::BITS as usize);

/// Returns an iterator over the indices of the bits set in `mask`, in increasing order.
fn bit_indices(mut mask: u64) -> impl Iterator<Item = usize> {
    std::iter::from_fn(move || {
        if mask == 0 {
            return None;
        }
        let index = mask.trailing_zeros() as usize;
        mask &= mask - 1;
        Some(index)
    })
}

/// The state of the stack
///
/// Only the initialized elements are stored, densely and in increasing index order. The storage is
/// shared between the clones made for each verified instruction and copied on write. This makes
/// cloning cheap and comparing two stacks, the hot path of state pruning, a linear scan.
#[derive(Clone, Debug, Default, PartialEq, Eq)]
struct Stack {
    /// Bit `i` is set iff element `i` is initialized.
    mask: u64,
    /// The initialized elements, in increasing index order.
    data: Arc<Vec<Type>>,
}

impl Stack {
    fn bit(index: usize) -> u64 {
        assert!(index < u64::BITS as usize);
        1 << index
    }

    /// Returns the position of the element at `index` in `data`, or the position where it must be
    /// inserted if it is not initialized.
    fn position(&self, index: usize) -> usize {
        (self.mask & (Self::bit(index) - 1)).count_ones() as usize
    }

    /// Replace all instances of the NullOr type with the given `null_id` to either 0 or the
    /// subtype depending on `is_null`
    fn set_null(&mut self, null_id: &MemoryId, is_null: bool) {
        if !self.data.iter().any(|t| matches!(t, Type::NullOr { id, .. } if id == null_id)) {
            return;
        }
        for t in Arc::make_mut(&mut self.data).iter_mut() {
            t.set_null(null_id, is_null);
        }
    }

    fn get(&self, index: usize) -> &Type {
        if self.mask & Self::bit(index) == 0 {
            &Type::UNINITIALIZED
        } else {
            &self.data[self.position(index)]
        }
    }

    fn set(&mut self, index: usize, t: Type) {
        let bit = Self::bit(index);
        let position = self.position(index);
        let is_set = self.mask & bit != 0;
        if t == Type::UNINITIALIZED {
            if is_set {
                Arc::make_mut(&mut self.data).remove(position);
                self.mask &= !bit;
            }
        } else if is_set {
            if self.data[position] != t {
                Arc::make_mut(&mut self.data)[position] = t;
            }
        } else {
            Arc::make_mut(&mut self.data).insert(position, t);
            self.mask |= bit;
        }
    }

    /// Uninitializes all the elements whose bit is not set in `mask`.
    fn retain(&mut self, mask: u64) {
        if self.mask & !mask == 0 {
            return;
        }
        if mask == 0 {
            match Arc::get_mut(&mut self.data) {
                Some(data) => data.clear(),
                None => self.data = Default::default(),
            }
            self.mask = 0;
            return;
        }

        let mut indices = bit_indices(self.mask);
        Arc::make_mut(&mut self.data).retain(|_| mask & Self::bit(indices.next().unwrap()) != 0);
        self.mask &= mask;
    }

    fn extract_sub_value(value: u64, offset: usize, byte_count: usize) -> u64 {
        NativeEndian::read_uint(&value.as_bytes()[offset..], byte_count)
    }

    fn insert_sub_value(mut original: u64, value: u64, width: DataWidth, offset: usize) -> u64 {
        let byte_count = width.bytes();
        let original_buf = original.as_mut_bytes();
        let value_buf = value.as_bytes();
        original_buf[offset..(byte_count + offset)].copy_from_slice(&value_buf[..byte_count]);
        original
    }

    fn write_data_ptr(
        &mut self,
        mut offset: StackOffset,
        bytes: u64,
    ) -> Result<(), VerifierErrorKind> {
        for i in 0..bytes {
            self.store(offset, Type::UNKNOWN_SCALAR, DataWidth::U8)?;
            offset = offset.add(1);
        }
        Ok(())
    }

    fn read_data_ptr(&self, offset: StackOffset, bytes: u64) -> Result<(), VerifierErrorKind> {
        let read_element = |index: usize,
                            start_offset: usize,
                            end_offset: usize|
         -> Result<(), VerifierErrorKind> {
            match self.get(index) {
                Type::ScalarValue(data) => {
                    debug_assert!(end_offset > start_offset);
                    let unwritten_bits = Self::extract_sub_value(
                        data.unwritten_mask,
                        start_offset,
                        end_offset - start_offset,
                    );
                    if unwritten_bits == 0 {
                        Ok(())
                    } else {
                        Err(VerifierErrorKind::UninitializedStackRead)
                    }
                }
                _ => Err(VerifierErrorKind::NonScalarStackRead),
            }
        };
        if bytes == 0 {
            return Ok(());
        }

        if bytes as usize > BPF_STACK_SIZE {
            return Err(VerifierErrorKind::StackAccessOutOfBounds);
        }

        offset.check_valid_offset()?;

        let end_offset = offset.add(bytes);
        if !end_offset.is_within_stack() {
            return Err(VerifierErrorKind::StackAccessOutOfBounds);
        }

        // Handle the case where all the data is contained in a single element excluding the last
        // byte (the case when the read ends at an element edge, i.e. `end_offset.sub_index()==0`,
        // is covered by the default path below).
        if offset.array_index() == end_offset.array_index() {
            return read_element(offset.array_index(), offset.sub_index(), end_offset.sub_index());
        }

        // Handle the first element, that might be partial.
        read_element(offset.array_index(), offset.sub_index(), STACK_ELEMENT_SIZE)?;

        // Handle the last element, that might be partial.
        if end_offset.sub_index() != 0 {
            read_element(end_offset.array_index(), 0, end_offset.sub_index())?;
        }

        // Handle the any full type between beginning and end.
        for i in (offset.array_index() + 1)..end_offset.array_index() {
            read_element(i, 0, STACK_ELEMENT_SIZE)?;
        }

        Ok(())
    }

    fn store(
        &mut self,
        offset: StackOffset,
        value: Type,
        width: DataWidth,
    ) -> Result<(), VerifierErrorKind> {
        offset.check_valid_offset()?;
        if offset.sub_index() % width.bytes() != 0 {
            return Err(VerifierErrorKind::MisalignedStackAccess);
        }

        let index = offset.array_index();
        if width == DataWidth::U64 {
            self.set(index, value);
        } else {
            match value {
                Type::ScalarValue(data) => {
                    let old_data = match self.get(index) {
                        Type::ScalarValue(data) => *data,
                        _ => {
                            // The value in the stack is not a scalar. Let consider it an scalar
                            // value with no written bits.
                            ScalarValueData::UNINITIALIZED
                        }
                    };
                    let sub_index = offset.sub_index();
                    let value =
                        Self::insert_sub_value(old_data.value, data.value, width, sub_index);
                    let unknown_mask = Self::insert_sub_value(
                        old_data.unknown_mask,
                        data.unknown_mask,
                        width,
                        sub_index,
                    );
                    let unwritten_mask = Self::insert_sub_value(
                        old_data.unwritten_mask,
                        data.unwritten_mask,
                        width,
                        sub_index,
                    );
                    let urange = U64Range::compute_range_for_bytes_swap(
                        old_data.urange,
                        data.urange,
                        sub_index,
                        0,
                        width.bytes(),
                    );
                    self.set(
                        index,
                        Type::ScalarValue(ScalarValueData::new(
                            value,
                            unknown_mask,
                            unwritten_mask,
                            urange,
                        )),
                    );
                }
                _ => {
                    return Err(VerifierErrorKind::PartialNonScalarStackStore);
                }
            }
        }
        Ok(())
    }

    fn load(&self, offset: StackOffset, width: DataWidth) -> Result<Type, VerifierErrorKind> {
        offset.check_valid_offset()?;
        if offset.sub_index() % width.bytes() != 0 {
            return Err(VerifierErrorKind::MisalignedStackAccess);
        }

        let index = offset.array_index();
        let loaded_type = self.get(index).clone();
        let result = if width == DataWidth::U64 {
            loaded_type
        } else {
            match loaded_type {
                Type::ScalarValue(data) => {
                    let sub_index = offset.sub_index();
                    let value = Self::extract_sub_value(data.value, sub_index, width.bytes());
                    let unknown_mask =
                        Self::extract_sub_value(data.unknown_mask, sub_index, width.bytes());
                    let unwritten_mask =
                        Self::extract_sub_value(data.unwritten_mask, sub_index, width.bytes());
                    let urange = U64Range::compute_range_for_bytes_swap(
                        0.into(),
                        data.urange,
                        0,
                        sub_index,
                        width.bytes(),
                    );
                    Type::ScalarValue(ScalarValueData::new(
                        value,
                        unknown_mask,
                        unwritten_mask,
                        urange,
                    ))
                }
                _ => {
                    return Err(VerifierErrorKind::PartialNonScalarStackLoad);
                }
            }
        };
        if !result.is_initialized() {
            return Err(VerifierErrorKind::UninitializedStackRead);
        }
        Ok(result)
    }
}

/// Two types are ordered with `t1` > `t2` if a proof that a program in a state `t1` finish is also
/// a proof that a program in a state `t2` finish.
impl PartialOrd for Stack {
    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
        if self.mask == other.mask && Arc::ptr_eq(&self.data, &other.data) {
            return Some(Ordering::Equal);
        }
        let mut result = match (self.mask & !other.mask != 0, !self.mask & other.mask != 0) {
            (true, true) => return None,
            (true, false) => Ordering::Less,
            (false, true) => Ordering::Greater,
            (false, false) => Ordering::Equal,
        };
        for index in bit_indices(self.mask & other.mask) {
            result = associate_orderings(result, self.get(index).partial_cmp(other.get(index))?)?;
        }
        Some(result)
    }
}

macro_rules! bpf_log {
    ($context:ident, $verification_context:ident, $($msg:tt)*) => {
        if $verification_context.logger.is_enabled() {
            let line = format!(
                "{}: ({:02x}) {}",
                $context.pc,
                $verification_context.code[$context.pc].code(),
                format_args!($($msg)*)
            );
            $verification_context.logger.log(line.as_bytes());
        }
    };
}

#[cfg(target_os = "fuchsia")]
type DependenciesMutex = LockDepMutex<DataDependencies, EbpfVerifierDependenciesLock>;

#[cfg(not(target_os = "fuchsia"))]
#[derive(Debug, Default)]
struct DependenciesMutex(std::sync::Mutex<DataDependencies>);

#[cfg(not(target_os = "fuchsia"))]
impl DependenciesMutex {
    fn lock(&self) -> std::sync::MutexGuard<'_, DataDependencies> {
        self.0.lock().unwrap()
    }

    fn get_mut(&mut self) -> &mut DataDependencies {
        self.0.get_mut().unwrap()
    }
}

/// The state of the computation as known by the verifier at a given point in time.
#[derive(Debug, Default)]
struct ComputationContext {
    /// The program counter.
    pc: ProgramCounter,
    /// Register 0 to 9.
    registers: [Type; GENERAL_REGISTER_COUNT as usize],
    /// The state of the stack.
    stack: Stack,
    /// The dynamically known bounds of buffers indexed by their ids.
    array_bounds: BTreeMap<MemoryId, u64>,
    /// The currently allocated resources.
    resources: HashSet<MemoryId>,
    /// The previous context in the computation.
    parent: Option<Arc<ComputationContext>>,
    /// The data dependencies of this context. This is used to broaden a known ending context to
    /// help cutting computation branches.
    dependencies: DependenciesMutex,
    /// Whether this context has reached an exit instruction. The main loop uses this flag to
    /// call terminate() on the owned context, avoiding the extra Arc reference that would be
    /// created by cloning self in the exit handler.
    terminated: bool,
}

impl Clone for ComputationContext {
    fn clone(&self) -> Self {
        Self {
            pc: self.pc,
            registers: self.registers.clone(),
            stack: self.stack.clone(),
            array_bounds: self.array_bounds.clone(),
            resources: self.resources.clone(),
            parent: self.parent.clone(),
            // dependencies are erased as they must always be used on the same instance of the
            // context.
            dependencies: Default::default(),
            terminated: false,
        }
    }
}

/// parent and dependencies are ignored for the comparison, as they do not matter for termination.
impl PartialEq for ComputationContext {
    fn eq(&self, other: &Self) -> bool {
        self.pc == other.pc
            && self.registers == other.registers
            && self.stack == other.stack
            && self.array_bounds == other.array_bounds
    }
}

impl ComputationContext {
    /// Replace all instances of the NullOr type with the given `null_id` to either 0 or the
    /// subtype depending on `is_null`
    fn set_null(&mut self, null_id: &MemoryId, is_null: bool) {
        for i in 0..self.registers.len() {
            self.registers[i].set_null(null_id, is_null);
        }
        self.stack.set_null(null_id, is_null);
    }

    fn reg(&self, index: Register) -> Result<Type, VerifierErrorKind> {
        if index >= REGISTER_COUNT {
            return Err(VerifierErrorKind::InvalidRegister(index));
        }
        if index < GENERAL_REGISTER_COUNT {
            Ok(self.registers[index as usize].clone())
        } else {
            Ok(Type::PtrToStack { offset: StackOffset::default() })
        }
    }

    fn set_reg(&mut self, index: Register, reg_type: Type) -> Result<(), VerifierErrorKind> {
        if index >= REGISTER_COUNT {
            return Err(VerifierErrorKind::InvalidRegister(index));
        }
        if index >= GENERAL_REGISTER_COUNT {
            return Err(VerifierErrorKind::WriteToReadOnlyRegister(index));
        }
        self.registers[index as usize] = reg_type;
        Ok(())
    }

    fn update_array_bounds(&mut self, id: MemoryId, new_bound: ScalarValueData) {
        let new_bound_min = new_bound.min();
        self.array_bounds
            .entry(id)
            .and_modify(|v| *v = std::cmp::max(*v, new_bound_min))
            .or_insert(new_bound_min);
    }

    fn get_map_schema(&self, argument: u8) -> Result<MapSchema, VerifierErrorKind> {
        match self.reg(argument + 1)? {
            Type::ConstPtrToMap { schema, .. } => Ok(schema),
            _ => Err(VerifierErrorKind::HelperArgumentNotMap(argument)),
        }
    }

    fn next(&self) -> Result<Self, VerifierErrorKind> {
        self.jump_with_offset(0, Arc::new(self.clone()))
    }

    /// Returns a new `ComputationContext` where the pc has jump by `offset + 1`. In particular,
    /// the next instruction is reached with `jump_with_offset(0)`.
    ///
    /// This does not check that the target is inside the program: falling off the end of the
    /// program is reported by the main verification loop. Use `checked_jump_with_offset` for
    /// explicit jumps.
    fn jump_with_offset(&self, offset: i16, parent: Arc<Self>) -> Result<Self, VerifierErrorKind> {
        let pc = self
            .pc
            .checked_add_signed(offset.into())
            .and_then(|v| v.checked_add_signed(1))
            .ok_or(VerifierErrorKind::JumpOutOfBounds)?;
        let result = Self {
            pc,
            registers: self.registers.clone(),
            stack: self.stack.clone(),
            array_bounds: self.array_bounds.clone(),
            resources: self.resources.clone(),
            parent: Some(parent),
            dependencies: Default::default(),
            terminated: false,
        };
        Ok(result)
    }

    /// Same as `jump_with_offset`, but also fails if the target of the jump is outside of the
    /// program.
    fn checked_jump_with_offset(
        &self,
        verification_context: &VerificationContext<'_>,
        offset: i16,
        parent: Arc<Self>,
    ) -> Result<Self, VerifierErrorKind> {
        let result = self.jump_with_offset(offset, parent)?;
        if result.pc >= verification_context.code.len() {
            return Err(VerifierErrorKind::JumpOutOfBounds);
        }
        Ok(result)
    }

    fn check_memory_access(
        &self,
        dst_offset: ScalarValueData,
        dst_buffer_size: u64,
        instruction_offset: i16,
        width: usize,
    ) -> Result<(), VerifierErrorKind> {
        let memory_range = dst_offset.urange + instruction_offset + U64Range::new(0, width as u64);
        if memory_range.max > dst_buffer_size {
            return Err(VerifierErrorKind::OutOfBoundsMemoryAccess);
        }
        Ok(())
    }

    /// Checks that the atomic access to `addr + field.offset` is allowed: it
    /// must target either the stack or a map value, and it must be naturally
    /// aligned for `field.width`.
    ///
    /// The stack and map values are at least 8-byte aligned, so it is
    /// sufficient to check the offset of the access relative to the start of
    /// the buffer. The offset is tracked as a `ScalarValueData`, so the check
    /// requires the low bits of the offset to be known and zero.
    fn check_atomic_access(&self, addr: &Type, field: Field) -> Result<(), VerifierErrorKind> {
        let addr = addr.inner(self)?;
        let base_offset = match *addr {
            Type::PtrToStack { offset } => offset.reg(),
            Type::PtrToMemory { offset, origin, .. } if origin.is_map_value() => offset,
            _ => return Err(VerifierErrorKind::AtomicAccessNotAllowed),
        };
        let alignment_mask = (field.width.bytes() as u64) - 1;
        // Adding a constant preserves the low bits of the result only if the
        // low bits of the other operand are known.
        if base_offset.unknown_mask & alignment_mask != 0
            || base_offset.value.wrapping_add_signed(field.offset.into()) & alignment_mask != 0
        {
            return Err(VerifierErrorKind::MisalignedAtomicAccess);
        }
        Ok(())
    }

    fn store_memory(
        &mut self,
        context: &mut VerificationContext<'_>,
        addr: &Type,
        field: Field,
        value: Type,
    ) -> Result<(), VerifierErrorKind> {
        let addr = addr.inner(self)?;
        match *addr {
            Type::PtrToStack { offset } => {
                let offset_sum = offset.add(field.offset);
                return self.stack.store(offset_sum, value, field.width);
            }
            Type::PtrToMemory { offset, buffer_size, origin, .. } if origin.is_writable() => {
                self.check_memory_access(offset, buffer_size, field.offset, field.width.bytes())?;
            }
            Type::PtrToMemory { .. } => {
                return Err(VerifierErrorKind::WriteToReadOnlyMemory);
            }
            Type::PtrToStruct { ref id, offset, ref descriptor, .. } => {
                let field_desc = descriptor
                    .find_field(offset, field)
                    .ok_or(VerifierErrorKind::InvalidStructFieldAccess)?;

                if !matches!(field_desc.field_type, FieldType::MutableScalar { .. }) {
                    return Err(VerifierErrorKind::WriteToReadOnlyField);
                }

                context.register_struct_access(StructAccess {
                    pc: self.pc,
                    memory_id: id.clone(),
                    field_offset: field_desc.offset,
                    is_32_bit_ptr_load: false,
                })?;
            }
            Type::PtrToArray { ref id, offset } => {
                self.check_memory_access(
                    offset,
                    *self.array_bounds.get(&id).unwrap_or(&0),
                    field.offset,
                    field.width.bytes(),
                )?;
            }
            _ => return Err(VerifierErrorKind::StoreToNonPointer),
        }

        match value {
            Type::ScalarValue(data) if data.is_fully_initialized() => {}
            // Private data should not be leaked.
            _ => return Err(VerifierErrorKind::InvalidStoredValue),
        }
        Ok(())
    }

    fn load_memory(
        &self,
        context: &mut VerificationContext<'_>,
        addr: &Type,
        field: Field,
    ) -> Result<Type, VerifierErrorKind> {
        let addr = addr.inner(self)?;
        match *addr {
            Type::PtrToStack { offset } => {
                let offset_sum = offset.add(field.offset);
                self.stack.load(offset_sum, field.width)
            }
            Type::PtrToMemory { ref id, offset, buffer_size, .. } => {
                self.check_memory_access(offset, buffer_size, field.offset, field.width.bytes())?;
                Ok(Type::UNKNOWN_SCALAR)
            }
            Type::PtrToStruct { ref id, offset, ref descriptor, .. } => {
                let field_desc = descriptor
                    .find_field(offset, field)
                    .ok_or(VerifierErrorKind::InvalidStructFieldAccess)?;

                let (return_type, is_32_bit_ptr_load) = match &field_desc.field_type {
                    FieldType::Scalar { .. } | FieldType::MutableScalar { .. } => {
                        (Type::UNKNOWN_SCALAR, false)
                    }
                    FieldType::PtrToArray { id: array_id, is_32_bit } => (
                        Type::PtrToArray { id: array_id.prepended(id.clone()), offset: 0.into() },
                        *is_32_bit,
                    ),
                    FieldType::PtrToEndArray { id: array_id, is_32_bit } => {
                        (Type::PtrToEndArray { id: array_id.prepended(id.clone()) }, *is_32_bit)
                    }
                    FieldType::PtrToMemory { id: memory_id, buffer_size, is_32_bit } => (
                        Type::PtrToMemory {
                            id: memory_id.prepended(id.clone()),
                            offset: 0.into(),
                            buffer_size: *buffer_size as u64,
                            origin: PointerOrigin::KernelReadOnly,
                        },
                        *is_32_bit,
                    ),
                    FieldType::NullablePtrToMemory { id: memory_id, buffer_size, is_32_bit } => {
                        let id = memory_id.prepended(id.clone());
                        (
                            Type::NullOr {
                                id: id.clone(),
                                inner: Box::new(Type::PtrToMemory {
                                    id,
                                    offset: 0.into(),
                                    buffer_size: *buffer_size as u64,
                                    origin: PointerOrigin::KernelReadOnly,
                                }),
                            },
                            *is_32_bit,
                        )
                    }
                };

                context.register_struct_access(StructAccess {
                    pc: self.pc,
                    memory_id: id.clone(),
                    field_offset: field_desc.offset,
                    is_32_bit_ptr_load,
                })?;

                Ok(return_type)
            }
            Type::PtrToArray { ref id, offset } => {
                self.check_memory_access(
                    offset,
                    *self.array_bounds.get(&id).unwrap_or(&0),
                    field.offset,
                    field.width.bytes(),
                )?;
                Ok(Type::UNKNOWN_SCALAR)
            }
            _ => Err(VerifierErrorKind::LoadFromNonPointer),
        }
    }

    /**
     * Given the given `return_value` in a method signature, return the concrete type to use,
     * updating the `next` context is needed.
     *
     * `maybe_null` is true is the computed value will be a descendant of a `NullOr` type.
     */
    fn resolve_return_value(
        &self,
        verification_context: &mut VerificationContext<'_>,
        return_value: &Type,
        next: &mut ComputationContext,
        maybe_null: bool,
    ) -> Result<Type, VerifierErrorKind> {
        match return_value {
            Type::AliasParameter { parameter_index } => self.reg(parameter_index + 1),
            Type::ReleasableParameter { id, inner } => {
                let id = verification_context.next_id().prepended(id.clone());
                if !maybe_null {
                    next.resources.insert(id.clone());
                }
                Ok(Type::Releasable {
                    id,
                    inner: Box::new(self.resolve_return_value(
                        verification_context,
                        inner,
                        next,
                        maybe_null,
                    )?),
                })
            }
            Type::NullOrParameter(t) => {
                let id = verification_context.next_id();
                Ok(Type::NullOr {
                    id,
                    inner: Box::new(self.resolve_return_value(
                        verification_context,
                        t,
                        next,
                        true,
                    )?),
                })
            }
            Type::MapValueParameter { map_ptr_index } => {
                let schema = self.get_map_schema(*map_ptr_index)?;
                let id = verification_context.next_id();
                let origin = if schema.flags.contains(MapFlags::ProgReadOnly) {
                    PointerOrigin::MapReadOnly
                } else {
                    PointerOrigin::MapWritable
                };
                Ok(Type::PtrToMemory {
                    id,
                    offset: 0.into(),
                    buffer_size: schema.value_size as u64,
                    origin,
                })
            }
            Type::MemoryParameter { size, .. } => {
                let buffer_size = size.size(self)?;
                let id = verification_context.next_id();
                Ok(Type::PtrToMemory {
                    id,
                    offset: 0.into(),
                    buffer_size,
                    origin: PointerOrigin::MapWritable,
                })
            }
            Type::PtrToMemory { id, offset, buffer_size, origin } => {
                let id = id.prepended(verification_context.next_id());
                Ok(Type::PtrToMemory {
                    id,
                    offset: *offset,
                    buffer_size: *buffer_size,
                    origin: *origin,
                })
            }
            Type::PtrToStruct { id, offset, descriptor } => {
                let id = id.prepended(verification_context.next_id());
                Ok(Type::PtrToStruct { id, offset: *offset, descriptor: descriptor.clone() })
            }
            t => Ok(t.clone()),
        }
    }

    fn compute_source(&self, src: Source) -> Result<Type, VerifierErrorKind> {
        match src {
            Source::Reg(reg) => self.reg(reg),
            Source::Value(v) => Ok(v.into()),
        }
    }

    fn apply_computation(
        context: &ComputationContext,
        op1: Type,
        op2: Type,
        alu_type: AluType,
        op: impl Fn(ScalarValueData, ScalarValueData) -> ScalarValueData,
    ) -> Result<Type, VerifierErrorKind> {
        let result: Type = match (alu_type, op1.inner(context)?, op2.inner(context)?) {
            (_, Type::ScalarValue(data1), Type::ScalarValue(data2)) => op(*data1, *data2).into(),
            (
                AluType::Add,
                Type::ScalarValue(_),
                Type::PtrToStack { .. }
                | Type::PtrToMemory { .. }
                | Type::PtrToStruct { .. }
                | Type::PtrToArray { .. },
            ) => {
                return Self::apply_computation(context, op2, op1, alu_type, op);
            }
            // Pointer arithmetic with a scalar that is not fully initialized (either never
            // written, or derived from a pointer value) is prohibited: it would allow the
            // pointer value to leak through the resulting offset.
            (
                alu_type,
                Type::PtrToStack { .. }
                | Type::PtrToMemory { .. }
                | Type::PtrToStruct { .. }
                | Type::PtrToArray { .. },
                Type::ScalarValue(data),
            ) if alu_type.is_ptr_compatible() && !data.is_fully_initialized() => {
                return Err(VerifierErrorKind::UninitializedPointerArithmetic);
            }
            (alu_type, Type::PtrToStack { offset: x }, Type::ScalarValue(data))
                if alu_type.is_ptr_compatible() =>
            {
                Type::PtrToStack { offset: run_on_stack_offset(*x, |x| op(x, *data)) }
            }
            (
                alu_type,
                Type::PtrToMemory { id, offset: x, buffer_size, origin },
                Type::ScalarValue(data),
            ) if alu_type.is_ptr_compatible() => {
                let offset = op(*x, *data);
                Type::PtrToMemory {
                    id: id.clone(),
                    offset,
                    buffer_size: *buffer_size,
                    origin: *origin,
                }
            }
            (
                alu_type,
                Type::PtrToStruct { id, offset: x, descriptor },
                Type::ScalarValue(data),
            ) if alu_type.is_ptr_compatible() => {
                let offset = op(*x, *data);
                Type::PtrToStruct { id: id.clone(), offset, descriptor: descriptor.clone() }
            }
            (AluType::Add, Type::PtrToArray { id, offset: x }, Type::ScalarValue(data)) => {
                let offset =
                    x.checked_add(*data).ok_or(VerifierErrorKind::PointerOffsetOverflow)?;
                Type::PtrToArray { id: id.clone(), offset }
            }
            (AluType::Sub, Type::PtrToArray { id, offset: x }, Type::ScalarValue(data)) => {
                let offset =
                    x.checked_sub(*data).ok_or(VerifierErrorKind::PointerOffsetOverflow)?;
                Type::PtrToArray { id: id.clone(), offset }
            }
            (
                AluType::Sub,
                Type::PtrToMemory { id: id1, offset: x1, .. },
                Type::PtrToMemory { id: id2, offset: x2, .. },
            )
            | (
                AluType::Sub,
                Type::PtrToStruct { id: id1, offset: x1, .. },
                Type::PtrToStruct { id: id2, offset: x2, .. },
            )
            | (
                AluType::Sub,
                Type::PtrToArray { id: id1, offset: x1 },
                Type::PtrToArray { id: id2, offset: x2 },
            ) if id1 == id2 => Type::from(op(*x1, *x2)),
            (AluType::Sub, Type::PtrToStack { offset: x1 }, Type::PtrToStack { offset: x2 }) => {
                Type::from(op(x1.reg(), x2.reg()))
            }
            (
                AluType::Sub,
                Type::PtrToArray { id: id1, .. },
                Type::PtrToEndArray { id: id2, .. },
            )
            | (
                AluType::Sub,
                Type::PtrToEndArray { id: id1, .. },
                Type::PtrToArray { id: id2, .. },
            ) if id1 == id2 => Type::UNKNOWN_SCALAR,
            _ => Type::default(),
        };
        Ok(result)
    }

    fn alu(
        &mut self,
        op_name: Option<&str>,
        verification_context: &mut VerificationContext<'_>,
        dst: Register,
        src: Source,
        alu_type: AluType,
        op: impl Fn(ScalarValueData, ScalarValueData) -> ScalarValueData,
    ) -> Result<(), VerifierErrorKind> {
        if let Some(op_name) = op_name {
            bpf_log!(
                self,
                verification_context,
                "{op_name} {}, {}",
                display_register(dst),
                display_source(src)
            );
        }
        let op1 = self.reg(dst)?;
        let op2 = self.compute_source(src)?;
        let result = Self::apply_computation(self, op1, op2, alu_type, op)?;
        let mut next = self.next()?;
        next.set_reg(dst, result)?;
        verification_context.states.push(next);
        Ok(())
    }

    fn log_atomic_operation(
        &mut self,
        op_name: &str,
        verification_context: &mut VerificationContext<'_>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) {
        bpf_log!(
            self,
            verification_context,
            "lock {}{} [{}{}], {}",
            if fetch { "fetch " } else { "" },
            op_name,
            display_register(dst),
            print_offset(offset),
            display_register(src),
        );
    }

    fn raw_atomic_operation(
        &mut self,
        op_name: &str,
        verification_context: &mut VerificationContext<'_>,
        width: DataWidth,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
        op: impl FnOnce(&ComputationContext, Type, Type) -> Result<Type, VerifierErrorKind>,
    ) -> Result<(), VerifierErrorKind> {
        self.log_atomic_operation(op_name, verification_context, fetch, dst, offset, src);
        let addr = self.reg(dst)?;
        let value = self.reg(src)?;
        let field = Field::new(offset, width);
        self.check_atomic_access(&addr, field)?;
        let loaded_type = self.load_memory(verification_context, &addr, field)?;
        let result = op(self, loaded_type.clone(), value)?;
        let mut next = self.next()?;
        next.store_memory(verification_context, &addr, field, result)?;
        if fetch {
            next.set_reg(src, loaded_type)?;
        }
        verification_context.states.push(next);
        Ok(())
    }

    fn atomic_operation(
        &mut self,
        op_name: &str,
        verification_context: &mut VerificationContext<'_>,
        width: DataWidth,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
        alu_type: AluType,
        op: impl Fn(ScalarValueData, ScalarValueData) -> ScalarValueData,
    ) -> Result<(), VerifierErrorKind> {
        self.raw_atomic_operation(
            op_name,
            verification_context,
            width,
            fetch,
            dst,
            offset,
            src,
            |context: &ComputationContext, v1: Type, v2: Type| {
                Self::apply_computation(context, v1, v2, alu_type, op)
            },
        )
    }

    fn raw_atomic_cmpxchg(
        &mut self,
        op_name: &str,
        verification_context: &mut VerificationContext<'_>,
        dst: Register,
        offset: i16,
        src: Register,
        jump_width: JumpWidth,
        op: impl Fn(ScalarValueData, ScalarValueData) -> Result<Option<bool>, ()>,
    ) -> Result<(), VerifierErrorKind> {
        self.log_atomic_operation(op_name, verification_context, true, dst, offset, src);
        let width = match jump_width {
            JumpWidth::W32 => DataWidth::U32,
            JumpWidth::W64 => DataWidth::U64,
        };
        let addr = self.reg(dst)?;
        let field = Field::new(offset, width);
        self.check_atomic_access(&addr, field)?;
        let dst = self.load_memory(verification_context, &addr, field)?;
        let value = self.reg(src)?;
        let r0 = self.reg(0)?;
        let branch = self.compute_branch(jump_width, &dst, &r0, op)?;
        // r0 = dst
        if branch.unwrap_or(true) {
            let mut next = self.next()?;
            let (dst, r0) =
                Type::constraint(&mut next, JumpType::Eq, jump_width, dst.clone(), r0.clone())?;
            next.set_reg(0, dst)?;
            next.store_memory(verification_context, &addr, field, value)?;
            verification_context.states.push(next);
        }
        // r0 != dst
        if !branch.unwrap_or(false) {
            let mut next = self.next()?;
            let (dst, r0) = Type::constraint(&mut next, JumpType::Ne, jump_width, dst, r0)?;
            next.set_reg(0, dst.clone())?;
            next.store_memory(verification_context, &addr, field, dst)?;
            verification_context.states.push(next);
        }

        Ok(())
    }
    fn endianness<BO: ByteOrder>(
        &mut self,
        op_name: &str,
        verification_context: &mut VerificationContext<'_>,
        dst: Register,
        width: DataWidth,
    ) -> Result<(), VerifierErrorKind> {
        bpf_log!(self, verification_context, "{op_name}{} {}", width.bits(), display_register(dst),);
        let bit_op = |value: u64| match width {
            DataWidth::U16 => BO::read_u16((value as u16).as_bytes()) as u64,
            DataWidth::U32 => BO::read_u32((value as u32).as_bytes()) as u64,
            DataWidth::U64 => BO::read_u64(value.as_bytes()),
            _ => {
                panic!("Unexpected bit width for endianness operation");
            }
        };
        let value = self.reg(dst)?;
        let new_value = match value {
            Type::ScalarValue(data) => Type::ScalarValue(ScalarValueData::new(
                bit_op(data.value),
                bit_op(data.unknown_mask),
                bit_op(data.unwritten_mask),
                U64Range::max(),
            )),
            _ => Type::default(),
        };
        let mut next = self.next()?;
        next.set_reg(dst, new_value)?;
        verification_context.states.push(next);
        Ok(())
    }

    fn compute_branch(
        &self,
        jump_width: JumpWidth,
        op1: &Type,
        op2: &Type,
        op: impl Fn(ScalarValueData, ScalarValueData) -> Result<Option<bool>, ()>,
    ) -> Result<Option<bool>, VerifierErrorKind> {
        match (jump_width, op1, op2) {
            (_, Type::ScalarValue(data1), Type::ScalarValue(data2)) => op(*data1, *data2),
            (JumpWidth::W64, Type::ScalarValue(data), Type::NullOr { .. })
            | (JumpWidth::W64, Type::NullOr { .. }, Type::ScalarValue(data))
                if data.is_zero() =>
            {
                Ok(None)
            }

            (JumpWidth::W64, Type::ScalarValue(data), t) if data.is_zero() && t.is_non_zero() => {
                let non_zero =
                    ScalarValueData::UNKNOWN_WRITTEN.update_range(U64Range::new(1, u64::MAX));
                op(0.into(), non_zero)
            }

            (JumpWidth::W64, t, Type::ScalarValue(data)) if data.is_zero() && t.is_non_zero() => {
                let non_zero =
                    ScalarValueData::UNKNOWN_WRITTEN.update_range(U64Range::new(1, u64::MAX));
                op(non_zero, 0.into())
            }

            (JumpWidth::W64, Type::PtrToStack { offset: x }, Type::PtrToStack { offset: y }) => {
                op(x.reg(), y.reg())
            }

            (
                JumpWidth::W64,
                Type::PtrToMemory { id: id1, offset: x, .. },
                Type::PtrToMemory { id: id2, offset: y, .. },
            )
            | (
                JumpWidth::W64,
                Type::PtrToStruct { id: id1, offset: x, .. },
                Type::PtrToStruct { id: id2, offset: y, .. },
            )
            | (
                JumpWidth::W64,
                Type::PtrToArray { id: id1, offset: x, .. },
                Type::PtrToArray { id: id2, offset: y, .. },
            ) if *id1 == *id2 => op(*x, *y),

            (JumpWidth::W64, Type::PtrToArray { id: id1, .. }, Type::PtrToEndArray { id: id2 })
            | (JumpWidth::W64, Type::PtrToEndArray { id: id1 }, Type::PtrToArray { id: id2, .. })
                if *id1 == *id2 =>
            {
                Ok(None)
            }

            _ => Err(()),
        }
        .map_err(|_| VerifierErrorKind::InvalidComparison)
    }

    fn conditional_jump(
        &mut self,
        op_name: &str,
        verification_context: &mut VerificationContext<'_>,
        dst: Register,
        src: Source,
        offset: i16,
        jump_type: JumpType,
        jump_width: JumpWidth,
        op: impl Fn(ScalarValueData, ScalarValueData) -> Result<Option<bool>, ()>,
    ) -> Result<(), VerifierErrorKind> {
        bpf_log!(
            self,
            verification_context,
            "{op_name} {}, {}, {}",
            display_register(dst),
            display_source(src),
            if offset == 0 { format!("0") } else { print_offset(offset) },
        );
        let op1 = self.reg(dst)?;
        let op2 = self.compute_source(src.clone())?;
        let apply_constraints_and_register = |mut next: Self,
                                              jump_type: JumpType|
         -> Result<Self, VerifierErrorKind> {
            if jump_type != JumpType::Unknown {
                let (new_op1, new_op2) =
                    Type::constraint(&mut next, jump_type, jump_width, op1.clone(), op2.clone())?;
                if dst < REGISTER_COUNT {
                    next.set_reg(dst, new_op1)?;
                }
                match src {
                    Source::Reg(r) => {
                        next.set_reg(r, new_op2)?;
                    }
                    _ => {
                        // Nothing to do
                    }
                }
            }
            Ok(next)
        };
        let branch = self.compute_branch(jump_width, &op1, &op2, op)?;
        let parent = Arc::new(self.clone());
        if branch.unwrap_or(true) {
            // Do the jump
            verification_context.states.push(apply_constraints_and_register(
                self.checked_jump_with_offset(verification_context, offset, parent.clone())?,
                jump_type,
            )?);
        }
        if !branch.unwrap_or(false) {
            // Skip the jump
            verification_context.states.push(apply_constraints_and_register(
                self.jump_with_offset(0, parent)?,
                jump_type.invert(),
            )?);
        }
        Ok(())
    }

    /// Handles the termination of a `ComputationContext`, performing branch cutting optimization.
    ///
    /// This method is called when it has been proven that the current context terminates (e.g.,
    /// reaches an `exit` instruction).
    ///
    /// The following steps are performed:
    /// 1. **Dependency Calculation:** The data dependencies of the context are computed based on
    ///    the dependencies of its terminated children and the instruction at the current PC.
    /// 2. **Context Broadening:** At a prune point, the context's state is broadened by clearing
    ///    registers and stack slots that are *not* in the calculated data dependencies. This
    ///    optimization assumes that data not used by the terminated branch is irrelevant for
    ///    future execution paths.
    /// 3. **Termination Registration:** At a prune point, the broadened context is added to the
    ///    set of terminating contexts if it is not less than any existing terminating context at
    ///    the same PC.
    /// 4. **Parent Termination:** If all the children of the current context have terminated,
    ///    its parent context is recursively terminated.
    fn terminate(
        self,
        verification_context: &mut VerificationContext<'_>,
    ) -> Result<(), VerifierError> {
        let mut next = Some(self);
        // Because of the potential length of the parent chain, do not use recursion.
        while let Some(mut current) = next.take() {
            // Take the parent to process it at the end and not keep it in the terminating
            // contexts.
            let parent = current.parent.take();

            // 1. Compute the dependencies of the context using the dependencies of its children
            //    and the actual operation.
            let mut dependencies = *current.dependencies.get_mut();

            dependencies
                .visit(
                    &mut DataDependenciesVisitorContext {
                        calling_context: &verification_context.calling_context,
                        computation_context: &current,
                    },
                    verification_context.code[current.pc],
                )
                .map_err(|kind| VerifierError { kind, pc: Some(current.pc) })?;

            if let Some(terminating_contexts) =
                &mut verification_context.terminating_contexts[current.pc]
            {
                // 2. Clear the state depending on the dependencies states
                for register in 0..GENERAL_REGISTER_COUNT {
                    if !dependencies.has_reg(register) {
                        current
                            .set_reg(register, Default::default())
                            .map_err(|kind| VerifierError { kind, pc: Some(current.pc) })?;
                    }
                }
                current.stack.retain(dependencies.stack);

                // 3. Add the cleared state to the set of `terminating_contexts`
                terminating_contexts.insert(current, dependencies);
            }

            // 4. Register the computed dependencies in our parent, and terminate it if all
            //    dependencies has been computed.
            if let Some(parent) = parent {
                parent.dependencies.lock().merge(dependencies);
                // To check whether all dependencies have been computed, rely on the fact that the
                // Arc count of the parent keep track of how many dependencies are left.
                next = Arc::into_inner(parent);
            }
        }
        Ok(())
    }
}

impl Drop for ComputationContext {
    fn drop(&mut self) {
        let mut next = self.parent.take().and_then(Arc::into_inner);
        // Because of the potential length of the parent chain, do not use recursion.
        while let Some(mut current) = next {
            next = current.parent.take().and_then(Arc::into_inner);
        }
    }
}

/// Two types are ordered with `t1` > `t2` if a proof that a program in a state `t1` finish is also
/// a proof that a program in a state `t2` finish.
impl PartialOrd for ComputationContext {
    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
        if self.pc != other.pc || self.resources.len() != other.resources.len() {
            return None;
        }
        let mut result = Type::compare_list(self.registers.iter(), other.registers.iter())?;
        result = associate_orderings(result, self.stack.partial_cmp(&other.stack)?)?;
        if self.resources != other.resources {
            return None;
        }
        let mut array_bound_iter1 = self.array_bounds.iter().peekable();
        let mut array_bound_iter2 = other.array_bounds.iter().peekable();
        let result = loop {
            match (array_bound_iter1.peek().cloned(), array_bound_iter2.peek().cloned()) {
                (None, None) => break result,
                (None, _) => break associate_orderings(result, Ordering::Greater)?,
                (_, None) => break associate_orderings(result, Ordering::Less)?,
                (Some((k1, v1)), Some((k2, v2))) => match k1.cmp(k2) {
                    Ordering::Equal => {
                        array_bound_iter1.next();
                        array_bound_iter2.next();
                        // The comparison is intentionally reversed (v2.cmp(v1) instead of
                        // v1.cmp(v2)). `v1` is the bound of the explored state (`self`) and `v2` is
                        // the bound of the current state (`other`). A smaller bound value
                        // represents a stronger safety guarantee (fewer assumed valid bytes,
                        // meaning a more restricted program). Therefore, a state with a smaller
                        // bound dominates (is "Greater" than) a state with a larger bound.
                        result = associate_orderings(result, v2.cmp(v1))?;
                    }
                    v @ Ordering::Less => {
                        array_bound_iter1.next();
                        result = associate_orderings(result, v)?;
                    }
                    v @ Ordering::Greater => {
                        array_bound_iter2.next();
                        result = associate_orderings(result, v)?;
                    }
                },
            }
        };
        Some(result)
    }
}

/// Represents the read data dependencies of an eBPF program branch.
///
/// This struct tracks which registers and stack positions are *read* by the
/// instructions within a branch of the eBPF program.  This information is used
/// during branch cutting optimization to broaden terminating contexts.
///
/// The verifier assumes that data not read by a terminated branch is irrelevant
/// for future execution paths and can be safely cleared.
#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
struct DataDependencies {
    /// A bitset of registers read by the children of a context.
    registers: u16,
    /// A bitset of stack positions read by the children of a context.
    stack: u64,
}

impl DataDependencies {
    #[inline]
    fn has_reg(&self, reg: Register) -> bool {
        (self.registers & (1_u16 << reg)) != 0
    }

    #[inline]
    fn add_reg(&mut self, reg: Register) {
        self.registers |= 1_u16 << reg;
    }

    #[inline]
    fn remove_reg(&mut self, reg: Register) -> bool {
        let mask = 1_u16 << reg;
        let was_set = (self.registers & mask) != 0;
        self.registers &= !mask;
        was_set
    }

    #[inline]
    fn has_stack(&self, slot: usize) -> bool {
        (self.stack & (1_u64 << slot)) != 0
    }

    #[inline]
    fn add_stack(&mut self, slot: usize) {
        self.stack |= 1_u64 << slot;
    }

    #[inline]
    fn remove_stack(&mut self, slot: usize) -> bool {
        let mask = 1_u64 << slot;
        let was_set = (self.stack & mask) != 0;
        self.stack &= !mask;
        was_set
    }

    #[inline]
    fn add_stack_range(&mut self, start: usize, end: usize) {
        if end > start {
            let count = end - start;
            let mask = if count >= 64 { !0 } else { ((1_u64 << count) - 1) << start };
            self.stack |= mask;
        }
    }

    fn merge(&mut self, other: Self) {
        self.registers |= other.registers;
        self.stack |= other.stack;
    }

    fn alu(&mut self, dst: Register, src: Source) -> Result<(), VerifierErrorKind> {
        // Only do something if the dst is read, otherwise the computation doesn't matter.
        if self.has_reg(dst) {
            if let Source::Reg(src) = src {
                self.add_reg(src);
            }
        }
        Ok(())
    }

    fn jmp(&mut self, dst: Register, src: Source) -> Result<(), VerifierErrorKind> {
        self.add_reg(dst);
        if let Source::Reg(src) = src {
            self.add_reg(src);
        }
        Ok(())
    }

    fn atomic(
        &mut self,
        context: &ComputationContext,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
        width: DataWidth,
        is_cmpxchg: bool,
    ) -> Result<(), VerifierErrorKind> {
        let mut is_read = false;
        if is_cmpxchg && self.has_reg(0) {
            is_read = true;
        }
        if fetch && self.has_reg(src) {
            is_read = true;
        }
        let addr = context.reg(dst)?;
        if let Type::PtrToStack { offset: stack_offset } = addr {
            let stack_offset = stack_offset.add(offset);
            stack_offset.check_valid_offset()?;
            let slot = stack_offset.array_index();
            if is_read || self.has_stack(slot) {
                is_read = true;
                self.add_stack(slot);
            }
        }
        if is_read {
            self.add_reg(0);
            self.add_reg(src);
        }
        self.add_reg(dst);
        Ok(())
    }
}

struct DataDependenciesVisitorContext<'a> {
    calling_context: &'a CallingContext,
    computation_context: &'a ComputationContext,
}

impl BpfVisitor for DataDependencies {
    type Context<'a> = DataDependenciesVisitorContext<'a>;
    type Error = VerifierErrorKind;

    fn add<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn add64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn and<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn and64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn arsh<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn arsh64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn div<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn div64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn lsh<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn lsh64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn r#mod<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn mod64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn mul<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn mul64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn or<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn or64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn rsh<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn rsh64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn sub<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn sub64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn xor<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }
    fn xor64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(dst, src)
    }

    fn mov<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        if src == Source::Reg(dst) || !self.has_reg(dst) {
            return Ok(());
        }
        if let Source::Reg(src) = src {
            self.add_reg(src);
        }
        self.remove_reg(dst);
        Ok(())
    }
    fn mov64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.mov(context, dst, src)
    }

    fn neg<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        _dst: Register,
    ) -> Result<(), VerifierErrorKind> {
        // This is reading and writing the same value. This induces no change in dependencies.
        Ok(())
    }
    fn neg64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        _dst: Register,
    ) -> Result<(), VerifierErrorKind> {
        // This is reading and writing the same value. This induces no change in dependencies.
        Ok(())
    }

    fn be<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        _dst: Register,
        _width: DataWidth,
    ) -> Result<(), VerifierErrorKind> {
        // This is reading and writing the same value. This induces no change in dependencies.
        Ok(())
    }
    fn le<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        _dst: Register,
        _width: DataWidth,
    ) -> Result<(), VerifierErrorKind> {
        // This is reading and writing the same value. This induces no change in dependencies.
        Ok(())
    }

    fn call_external<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        index: u32,
    ) -> Result<(), VerifierErrorKind> {
        let Some(helper) = context.calling_context.helpers.get(&index).cloned() else {
            return Err(VerifierErrorKind::UnknownHelper(index));
        };
        // A helper reads the stack region each `input` memory-parameter argument
        // points at, so those stack slots are data dependencies, like load/store.
        let comp = &context.computation_context;
        for (arg_index, arg) in helper.signature.args.iter().enumerate() {
            if let Type::MemoryParameter { size, input: true, .. } = arg {
                if let Type::PtrToStack { offset } = comp.reg((arg_index + 1) as Register)? {
                    let end = offset.add(size.size(comp)?);
                    if offset.check_valid_offset().is_ok() && end.is_within_stack() {
                        let start_idx = offset.array_index();
                        let end_idx = end.array_index();
                        self.add_stack_range(start_idx, end_idx);
                        if end.sub_index() != 0 {
                            self.add_stack(end_idx);
                        }
                    }
                }
            }
        }
        // 0 is overwritten and 1 to 5 are scratch registers
        self.registers &= !0b0011_1111;
        // 1 to k are parameters.
        let num_args = helper.signature.args.len();
        self.registers |= ((1_u16 << num_args) - 1) << 1;
        Ok(())
    }

    fn exit<'a>(&mut self, _context: &mut Self::Context<'a>) -> Result<(), VerifierErrorKind> {
        // This read r0 unconditionally.
        self.add_reg(0);
        Ok(())
    }

    fn jump<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        _offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        // This doesn't do anything with values.
        Ok(())
    }

    fn jeq<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jeq64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jne<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jne64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jge<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jge64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jgt<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jgt64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jle<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jle64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jlt<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jlt64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jsge<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jsge64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jsgt<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jsgt64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jsle<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jsle64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jslt<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jslt64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jset<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }
    fn jset64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.jmp(dst, src)
    }

    fn atomic_add<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic(&context.computation_context, fetch, dst, offset, src, DataWidth::U32, false)
    }

    fn atomic_add64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic(&context.computation_context, fetch, dst, offset, src, DataWidth::U64, false)
    }

    fn atomic_and<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic(&context.computation_context, fetch, dst, offset, src, DataWidth::U32, false)
    }

    fn atomic_and64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic(&context.computation_context, fetch, dst, offset, src, DataWidth::U64, false)
    }

    fn atomic_or<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic(&context.computation_context, fetch, dst, offset, src, DataWidth::U32, false)
    }

    fn atomic_or64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic(&context.computation_context, fetch, dst, offset, src, DataWidth::U64, false)
    }

    fn atomic_xor<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic(&context.computation_context, fetch, dst, offset, src, DataWidth::U32, false)
    }

    fn atomic_xor64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic(&context.computation_context, fetch, dst, offset, src, DataWidth::U64, false)
    }

    fn atomic_xchg<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic(&context.computation_context, fetch, dst, offset, src, DataWidth::U32, false)
    }

    fn atomic_xchg64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic(&context.computation_context, fetch, dst, offset, src, DataWidth::U64, false)
    }

    fn atomic_cmpxchg<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic(&context.computation_context, true, dst, offset, src, DataWidth::U32, true)
    }

    fn atomic_cmpxchg64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic(&context.computation_context, true, dst, offset, src, DataWidth::U64, true)
    }

    fn load<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        offset: i16,
        src: Register,
        width: DataWidth,
    ) -> Result<(), VerifierErrorKind> {
        let context = &context.computation_context;
        if self.has_reg(dst) {
            let addr = context.reg(src)?;
            if let Type::PtrToStack { offset: stack_offset } = addr {
                let stack_offset = stack_offset.add(offset);
                stack_offset.check_valid_offset()?;
                self.add_stack(stack_offset.array_index());
            }
        }
        self.add_reg(src);
        Ok(())
    }

    fn load64<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        _src: u8,
        _lower: u32,
    ) -> Result<(), VerifierErrorKind> {
        self.remove_reg(dst);
        Ok(())
    }

    fn load_from_packet<'a>(
        &mut self,
        _context: &mut Self::Context<'a>,
        dst: Register,
        src: Register,
        _offset: i32,
        register_offset: Option<Register>,
        _width: DataWidth,
    ) -> Result<(), VerifierErrorKind> {
        // 1 to 5 are scratch registers (bits 1..=5)
        self.registers &= !0b0011_1110;
        self.remove_reg(dst);
        // The types of the packet and of the offset are always checked, and r0 is checked to be a
        // written scalar on the exit path taken when the load fails.
        self.add_reg(src);
        if let Some(reg) = register_offset {
            self.add_reg(reg);
        }
        self.add_reg(0);
        Ok(())
    }

    fn store<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        offset: i16,
        src: Source,
        width: DataWidth,
    ) -> Result<(), VerifierErrorKind> {
        let context = &context.computation_context;
        let addr = context.reg(dst)?;
        if let Type::PtrToStack { offset: stack_offset } = addr {
            let stack_offset = stack_offset.add(offset);
            stack_offset.check_valid_offset()?;
            if self.remove_stack(stack_offset.array_index()) {
                if let Source::Reg(src) = src {
                    self.add_reg(src);
                }
            }
        } else {
            if let Source::Reg(src) = src {
                self.add_reg(src);
            }
            self.add_reg(dst);
        }

        Ok(())
    }
}

#[derive(Debug)]
struct TerminatingContext {
    computation_context: ComputationContext,
    dependencies: DataDependencies,
    /// Known scalar register values of `computation_context`, cached to filter comparisons.
    known_scalars: KnownScalars,
}

/// The contexts known to terminate at a given pc. The contexts are pairwise incomparable: each
/// time a bigger context is inserted, the smaller ones are removed.
#[derive(Debug, Default)]
struct TerminatingContexts {
    contexts: Vec<TerminatingContext>,
}

impl TerminatingContexts {
    /// Returns the most recently inserted context that is greater than or equal to `context`.
    fn find_greater_or_equal(&self, context: &ComputationContext) -> Option<&TerminatingContext> {
        if self.contexts.is_empty() {
            return None;
        }
        let known_scalars = KnownScalars::new(context);
        self.contexts
            .iter()
            .rev()
            .find(|c| c.known_scalars >= known_scalars && c.computation_context >= *context)
    }

    /// Inserts `context` unless a context greater than or equal to it is already present, and
    /// removes the contexts smaller than it.
    fn insert(&mut self, context: ComputationContext, dependencies: DataDependencies) {
        let known_scalars = KnownScalars::new(&context);
        let mut is_dominated = false;
        self.contexts.retain(|c| {
            // Skip the full comparison if the contexts are known to be incomparable. This does not
            // change the result: the full comparison would return `None`.
            if c.known_scalars.partial_cmp(&known_scalars).is_none() {
                return true;
            }
            match c.computation_context.partial_cmp(&context) {
                Some(Ordering::Less) => false,
                Some(Ordering::Equal) | Some(Ordering::Greater) => {
                    // If the list contains a context greater or equal to the current one, it
                    // should not be added.
                    is_dominated = true;
                    true
                }
                None => true,
            }
        });
        if !is_dominated {
            self.contexts.push(TerminatingContext {
                computation_context: context,
                dependencies,
                known_scalars,
            });
        }
    }
}

/// Tracks which general registers of a `ComputationContext` are constrained to a single known
/// constant scalar.
///
/// Used as a fast pre-filter before `ComputationContext::partial_cmp`: if `c1` has a known
/// constant `v` in register `i`, then `c1 >= c2` requires `c2` to also have `v` in register `i`.
#[derive(Clone, Copy, Debug, Default, Eq, PartialEq)]
struct KnownScalars {
    /// Bitmask of the registers holding a known scalar.
    mask: u16,
    /// The value of the registers in `mask`. The other values are 0.
    values: [u64; GENERAL_REGISTER_COUNT as usize],
}

impl KnownScalars {
    fn new(context: &ComputationContext) -> Self {
        let mut result = Self::default();
        for (i, reg) in context.registers.iter().enumerate() {
            if let Type::ScalarValue(data) = reg {
                if data.is_known() {
                    result.mask |= 1 << i;
                    result.values[i] = data.value;
                }
            }
        }
        result
    }
}

impl PartialOrd for KnownScalars {
    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
        let result = match (self.mask & !other.mask != 0, !self.mask & other.mask != 0) {
            (true, true) => return None,
            (true, false) => Ordering::Less,
            (false, true) => Ordering::Greater,
            (false, false) => Ordering::Equal,
        };
        bit_indices((self.mask & other.mask).into())
            .all(|i| self.values[i] == other.values[i])
            .then_some(result)
    }
}

#[derive(Clone, Copy, Debug, Eq, PartialEq)]
enum AluType {
    Plain,
    Sub,
    Add,
}

impl AluType {
    /// Can this operation be done one a pointer and a scalar.
    fn is_ptr_compatible(&self) -> bool {
        match self {
            Self::Sub | Self::Add => true,
            _ => false,
        }
    }
}

#[derive(Clone, Copy, Debug, Eq, PartialEq)]
enum JumpWidth {
    W32,
    W64,
}

#[derive(Clone, Copy, Debug, Eq, PartialEq)]
enum JumpType {
    Eq,
    Ge,
    Gt,
    Le,
    LooseComparaison,
    Lt,
    Ne,
    StrictComparaison,
    Unknown,
}

impl JumpType {
    fn invert(&self) -> Self {
        match self {
            Self::Eq => Self::Ne,
            Self::Ge => Self::Lt,
            Self::Gt => Self::Le,
            Self::Le => Self::Gt,
            Self::LooseComparaison => Self::StrictComparaison,
            Self::Lt => Self::Ge,
            Self::Ne => Self::Eq,
            Self::StrictComparaison => Self::LooseComparaison,
            Self::Unknown => Self::Unknown,
        }
    }

    fn is_strict(&self) -> bool {
        match self {
            Self::Gt | Self::Lt | Self::Ne | Self::StrictComparaison => true,
            _ => false,
        }
    }
}

fn display_register(register: Register) -> String {
    format!("%r{register}")
}

fn display_source(src: Source) -> String {
    match src {
        Source::Reg(r) => display_register(r),
        Source::Value(v) => format!("0x{v:x}"),
    }
}

impl BpfVisitor for ComputationContext {
    type Context<'a> = VerificationContext<'a>;
    type Error = VerifierErrorKind;

    fn add<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("add32"), context, dst, src, AluType::Plain, |x, y| alu32(x, y, |x, y| x + y))
    }
    fn add64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("add"), context, dst, src, AluType::Add, |x, y| x + y)
    }
    fn and<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("and32"), context, dst, src, AluType::Plain, |x, y| alu32(x, y, |x, y| x & y))
    }
    fn and64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("and"), context, dst, src, AluType::Plain, |x, y| x & y)
    }
    fn arsh<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("arsh32"), context, dst, src, AluType::Plain, |x, y| {
            alu32(x, y, |x, y| x.ashr(y))
        })
    }
    fn arsh64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("arsh"), context, dst, src, AluType::Plain, |x, y| x.ashr(y))
    }
    fn div<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("div32"), context, dst, src, AluType::Plain, |x, y| alu32(x, y, |x, y| x / y))
    }
    fn div64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("div"), context, dst, src, AluType::Plain, |x, y| x / y)
    }
    fn lsh<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("lsh32"), context, dst, src, AluType::Plain, |x, y| {
            alu32(x, y, |x, y| x << y)
        })
    }
    fn lsh64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("lsh"), context, dst, src, AluType::Plain, |x, y| x << y)
    }
    fn r#mod<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("mod32"), context, dst, src, AluType::Plain, |x, y| alu32(x, y, |x, y| x % y))
    }
    fn mod64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("mod"), context, dst, src, AluType::Plain, |x, y| x % y)
    }
    fn mov<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        bpf_log!(self, context, "mov32 {}, {}", display_register(dst), display_source(src));
        let src = self.compute_source(src)?;
        let value = match src {
            Type::ScalarValue(data) => {
                let value = (data.value as u32) as u64;
                let unknown_mask = (data.unknown_mask as u32) as u64;
                let unwritten_mask = (data.unwritten_mask as u32) as u64;
                let urange = U64Range::compute_range_for_bytes_swap(0.into(), data.urange, 0, 0, 4);
                Type::ScalarValue(ScalarValueData::new(value, unknown_mask, unwritten_mask, urange))
            }
            _ => Type::default(),
        };
        let mut next = self.next()?;
        next.set_reg(dst, value)?;
        context.states.push(next);
        Ok(())
    }
    fn mov64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        bpf_log!(self, context, "mov {}, {}", display_register(dst), display_source(src));
        let src = self.compute_source(src)?;
        let mut next = self.next()?;
        next.set_reg(dst, src)?;
        context.states.push(next);
        Ok(())
    }
    fn mul<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("mul32"), context, dst, src, AluType::Plain, |x, y| alu32(x, y, |x, y| x * y))
    }
    fn mul64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("mul"), context, dst, src, AluType::Plain, |x, y| x * y)
    }
    fn or<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("or32"), context, dst, src, AluType::Plain, |x, y| alu32(x, y, |x, y| x | y))
    }
    fn or64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("or"), context, dst, src, AluType::Plain, |x, y| x | y)
    }
    fn rsh<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("rsh32"), context, dst, src, AluType::Plain, |x, y| {
            alu32(x, y, |x, y| x >> y)
        })
    }
    fn rsh64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("rsh"), context, dst, src, AluType::Plain, |x, y| x >> y)
    }
    fn sub<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("sub32"), context, dst, src, AluType::Plain, |x, y| alu32(x, y, |x, y| x - y))
    }
    fn sub64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("sub"), context, dst, src, AluType::Sub, |x, y| x - y)
    }
    fn xor<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("xor32"), context, dst, src, AluType::Plain, |x, y| alu32(x, y, |x, y| x ^ y))
    }
    fn xor64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
    ) -> Result<(), VerifierErrorKind> {
        self.alu(Some("xor"), context, dst, src, AluType::Plain, |x, y| x ^ y)
    }

    fn neg<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
    ) -> Result<(), VerifierErrorKind> {
        bpf_log!(self, context, "neg32 {}", display_register(dst));
        self.alu(None, context, dst, Source::Value(0), AluType::Plain, |x, y| {
            alu32(x, y, |x, _y| -x)
        })
    }
    fn neg64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
    ) -> Result<(), VerifierErrorKind> {
        bpf_log!(self, context, "neg {}", display_register(dst));
        self.alu(None, context, dst, Source::Value(0), AluType::Plain, |x, _y| -x)
    }

    fn be<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        width: DataWidth,
    ) -> Result<(), VerifierErrorKind> {
        self.endianness::<BigEndian>("be", context, dst, width)
    }

    fn le<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        width: DataWidth,
    ) -> Result<(), VerifierErrorKind> {
        self.endianness::<LittleEndian>("le", context, dst, width)
    }

    fn call_external<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        index: u32,
    ) -> Result<(), VerifierErrorKind> {
        bpf_log!(self, context, "call 0x{:x}", index);
        let Some(helper) = context.calling_context.helpers.get(&index).cloned() else {
            return Err(VerifierErrorKind::UnknownHelper(index));
        };
        let HelperDefinition { signature, name, .. } = helper;
        debug_assert!(signature.args.len() <= 5);
        let mut next = self.next()?;
        for (arg_index, arg) in signature.args.iter().enumerate() {
            let reg = (arg_index + 1) as u8;
            self.reg(reg)?.match_parameter_type(context, self, name, arg, arg_index, &mut next)?
        }
        // Parameters have been validated, specify the return value on return.
        if signature.invalidate_array_bounds {
            next.array_bounds.clear();
        }
        let value =
            self.resolve_return_value(context, &signature.return_value, &mut next, false)?;
        next.set_reg(0, value)?;
        for i in 1..=5 {
            next.set_reg(i, Type::default())?;
        }
        context.states.push(next);
        Ok(())
    }

    fn exit<'a>(&mut self, context: &mut Self::Context<'a>) -> Result<(), VerifierErrorKind> {
        bpf_log!(self, context, "exit");
        if !self.reg(0)?.is_written_scalar() {
            return Err(VerifierErrorKind::InvalidReturnValue);
        }
        if !self.resources.is_empty() {
            return Err(VerifierErrorKind::ResourceLeak);
        }
        self.terminated = true;
        Ok(())
    }

    fn jump<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        bpf_log!(self, context, "ja {}", offset);
        let parent = Arc::new(self.clone());
        let next = self.checked_jump_with_offset(context, offset, parent)?;
        context.states.push(next);
        Ok(())
    }

    fn jeq<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jeq32",
            context,
            dst,
            src,
            offset,
            JumpType::Eq,
            JumpWidth::W32,
            |x, y| {
                comp32(x, y, |x, y| {
                    // x == y
                    if x.min == x.max && x.min == y.min && x.min == y.max {
                        return Some(true);
                    }
                    if x.max < y.min || y.max < x.min {
                        return Some(false);
                    }
                    None
                })
            },
        )
    }
    fn jeq64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jeq",
            context,
            dst,
            src,
            offset,
            JumpType::Eq,
            JumpWidth::W64,
            |x, y| {
                comp64(x, y, |x, y| {
                    // x == y
                    if x.min == x.max && x.min == y.min && x.min == y.max {
                        return Some(true);
                    }
                    if x.max < y.min || y.max < x.min {
                        return Some(false);
                    }
                    None
                })
            },
        )
    }
    fn jne<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jne32",
            context,
            dst,
            src,
            offset,
            JumpType::Ne,
            JumpWidth::W32,
            |x, y| {
                comp32(x, y, |x, y| {
                    // x != y
                    if x.min == x.max && x.min == y.min && x.min == y.max {
                        return Some(false);
                    }
                    if x.max < y.min || y.max < x.min {
                        return Some(true);
                    }
                    None
                })
            },
        )
    }
    fn jne64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jne",
            context,
            dst,
            src,
            offset,
            JumpType::Ne,
            JumpWidth::W64,
            |x, y| {
                comp64(x, y, |x, y| {
                    // x != y
                    if x.min == x.max && x.min == y.min && x.min == y.max {
                        return Some(false);
                    }
                    if x.max < y.min || y.max < x.min {
                        return Some(true);
                    }
                    None
                })
            },
        )
    }
    fn jge<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jge32",
            context,
            dst,
            src,
            offset,
            JumpType::Ge,
            JumpWidth::W32,
            |x, y| {
                comp32(x, y, |x, y| {
                    // x >= y
                    if x.min >= y.max {
                        return Some(true);
                    }
                    if y.min > x.max {
                        return Some(false);
                    }
                    None
                })
            },
        )
    }
    fn jge64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jge",
            context,
            dst,
            src,
            offset,
            JumpType::Ge,
            JumpWidth::W64,
            |x, y| {
                comp64(x, y, |x, y| {
                    // x >= y
                    if x.min >= y.max {
                        return Some(true);
                    }
                    if y.min > x.max {
                        return Some(false);
                    }
                    None
                })
            },
        )
    }
    fn jgt<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jgt32",
            context,
            dst,
            src,
            offset,
            JumpType::Gt,
            JumpWidth::W32,
            |x, y| {
                comp32(x, y, |x, y| {
                    // x > y
                    if x.min > y.max {
                        return Some(true);
                    }
                    if y.min >= x.max {
                        return Some(false);
                    }
                    None
                })
            },
        )
    }
    fn jgt64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jgt",
            context,
            dst,
            src,
            offset,
            JumpType::Gt,
            JumpWidth::W64,
            |x, y| {
                comp64(x, y, |x, y| {
                    // x > y
                    if x.min > y.max {
                        return Some(true);
                    }
                    if y.min >= x.max {
                        return Some(false);
                    }
                    None
                })
            },
        )
    }
    fn jle<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jle32",
            context,
            dst,
            src,
            offset,
            JumpType::Le,
            JumpWidth::W32,
            |x, y| {
                comp32(x, y, |x, y| {
                    // x <= y
                    if x.max <= y.min {
                        return Some(true);
                    }
                    if y.max < x.min {
                        return Some(false);
                    }
                    None
                })
            },
        )
    }
    fn jle64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jle",
            context,
            dst,
            src,
            offset,
            JumpType::Le,
            JumpWidth::W64,
            |x, y| {
                comp64(x, y, |x, y| {
                    // x <= y
                    if x.max <= y.min {
                        return Some(true);
                    }
                    if y.max < x.min {
                        return Some(false);
                    }
                    None
                })
            },
        )
    }
    fn jlt<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jlt32",
            context,
            dst,
            src,
            offset,
            JumpType::Lt,
            JumpWidth::W32,
            |x, y| {
                comp32(x, y, |x, y| {
                    // x < y
                    if x.max < y.min {
                        return Some(true);
                    }
                    if y.max <= x.min {
                        return Some(false);
                    }
                    None
                })
            },
        )
    }
    fn jlt64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jlt",
            context,
            dst,
            src,
            offset,
            JumpType::Lt,
            JumpWidth::W64,
            |x, y| {
                comp64(x, y, |x, y| {
                    // x < y
                    if x.max < y.min {
                        return Some(true);
                    }
                    if y.max <= x.min {
                        return Some(false);
                    }
                    None
                })
            },
        )
    }
    fn jsge<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jsge32",
            context,
            dst,
            src,
            offset,
            JumpType::LooseComparaison,
            JumpWidth::W32,
            |x, y| scomp32(x, y, |x, y| x >= y),
        )
    }
    fn jsge64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jsge",
            context,
            dst,
            src,
            offset,
            JumpType::LooseComparaison,
            JumpWidth::W64,
            |x, y| scomp64(x, y, |x, y| x >= y),
        )
    }
    fn jsgt<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jsgt32",
            context,
            dst,
            src,
            offset,
            JumpType::StrictComparaison,
            JumpWidth::W32,
            |x, y| scomp32(x, y, |x, y| x > y),
        )
    }
    fn jsgt64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jsgt",
            context,
            dst,
            src,
            offset,
            JumpType::StrictComparaison,
            JumpWidth::W64,
            |x, y| scomp64(x, y, |x, y| x > y),
        )
    }
    fn jsle<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jsle32",
            context,
            dst,
            src,
            offset,
            JumpType::LooseComparaison,
            JumpWidth::W32,
            |x, y| scomp32(x, y, |x, y| x <= y),
        )
    }
    fn jsle64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jsle",
            context,
            dst,
            src,
            offset,
            JumpType::LooseComparaison,
            JumpWidth::W64,
            |x, y| scomp64(x, y, |x, y| x <= y),
        )
    }
    fn jslt<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jslt32",
            context,
            dst,
            src,
            offset,
            JumpType::StrictComparaison,
            JumpWidth::W32,
            |x, y| scomp32(x, y, |x, y| x < y),
        )
    }
    fn jslt64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jslt",
            context,
            dst,
            src,
            offset,
            JumpType::StrictComparaison,
            JumpWidth::W64,
            |x, y| scomp64(x, y, |x, y| x < y),
        )
    }
    fn jset<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jset32",
            context,
            dst,
            src,
            offset,
            JumpType::Unknown,
            JumpWidth::W32,
            |x, y| {
                comp32(x, y, |x, y| {
                    // x & y != 0
                    if x.min != x.max || y.min != y.max {
                        return None;
                    }
                    Some(x.min & y.min != 0)
                })
            },
        )
    }
    fn jset64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Source,
        offset: i16,
    ) -> Result<(), VerifierErrorKind> {
        self.conditional_jump(
            "jset",
            context,
            dst,
            src,
            offset,
            JumpType::Unknown,
            JumpWidth::W64,
            |x, y| {
                comp64(x, y, |x, y| {
                    // x & y != 0
                    if x.min != x.max || y.min != y.max {
                        return None;
                    }
                    Some(x.min & y.min != 0)
                })
            },
        )
    }

    fn atomic_add<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic_operation(
            "add32",
            context,
            DataWidth::U32,
            fetch,
            dst,
            offset,
            src,
            AluType::Add,
            |x, y| alu32(x, y, |x, y| x + y),
        )
    }

    fn atomic_add64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic_operation(
            "add",
            context,
            DataWidth::U64,
            fetch,
            dst,
            offset,
            src,
            AluType::Add,
            |x, y| x + y,
        )
    }

    fn atomic_and<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic_operation(
            "and32",
            context,
            DataWidth::U32,
            fetch,
            dst,
            offset,
            src,
            AluType::Plain,
            |x, y| alu32(x, y, |x, y| x & y),
        )
    }

    fn atomic_and64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic_operation(
            "and",
            context,
            DataWidth::U64,
            fetch,
            dst,
            offset,
            src,
            AluType::Plain,
            |x, y| x & y,
        )
    }

    fn atomic_or<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic_operation(
            "or32",
            context,
            DataWidth::U32,
            fetch,
            dst,
            offset,
            src,
            AluType::Plain,
            |x, y| alu32(x, y, |x, y| x | y),
        )
    }

    fn atomic_or64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic_operation(
            "or",
            context,
            DataWidth::U64,
            fetch,
            dst,
            offset,
            src,
            AluType::Plain,
            |x, y| x | y,
        )
    }

    fn atomic_xor<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic_operation(
            "xor32",
            context,
            DataWidth::U32,
            fetch,
            dst,
            offset,
            src,
            AluType::Plain,
            |x, y| alu32(x, y, |x, y| x ^ y),
        )
    }

    fn atomic_xor64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic_operation(
            "xor",
            context,
            DataWidth::U64,
            fetch,
            dst,
            offset,
            src,
            AluType::Plain,
            |x, y| x ^ y,
        )
    }

    fn atomic_xchg<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.atomic_operation(
            "xchg32",
            context,
            DataWidth::U32,
            fetch,
            dst,
            offset,
            src,
            AluType::Plain,
            |_, x| x,
        )
    }

    fn atomic_xchg64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        fetch: bool,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.raw_atomic_operation(
            "xchg",
            context,
            DataWidth::U64,
            fetch,
            dst,
            offset,
            src,
            |_, _, x| Ok(x),
        )
    }

    fn atomic_cmpxchg<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.raw_atomic_cmpxchg("cmpxchg32", context, dst, offset, src, JumpWidth::W32, |x, y| {
            comp32(x, y, |x, y| {
                // x == y
                if x.min == x.max && x.min == y.min && x.min == y.max {
                    return Some(true);
                }
                if x.max < y.min || y.max < x.min {
                    return Some(false);
                }
                None
            })
        })
    }

    fn atomic_cmpxchg64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        offset: i16,
        src: Register,
    ) -> Result<(), VerifierErrorKind> {
        self.raw_atomic_cmpxchg("cmpxchg", context, dst, offset, src, JumpWidth::W64, |x, y| {
            comp64(x, y, |x, y| {
                // x == y
                if x.min == x.max && x.min == y.min && x.min == y.max {
                    return Some(true);
                }
                if x.max < y.min || y.max < x.min {
                    return Some(false);
                }
                None
            })
        })
    }

    fn load<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        offset: i16,
        src: Register,
        width: DataWidth,
    ) -> Result<(), VerifierErrorKind> {
        bpf_log!(
            self,
            context,
            "ldx{} {}, [{}{}]",
            width.str(),
            display_register(dst),
            display_register(src),
            print_offset(offset)
        );
        let addr = self.reg(src)?;
        let loaded_type = self.load_memory(context, &addr, Field::new(offset, width))?;
        let mut next = self.next()?;
        next.set_reg(dst, loaded_type)?;
        context.states.push(next);
        Ok(())
    }

    fn load64<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: u8,
        lower: u32,
    ) -> Result<(), VerifierErrorKind> {
        // The pre-scan has already guaranteed that `pc + 1` is valid and structurally well-formed.
        let next_instruction = &context.code[self.pc + 1];

        let value = match src {
            0 => {
                let value = (lower as u64) | (((next_instruction.imm() as u32) as u64) << 32);
                bpf_log!(self, context, "lddw {}, 0x{:x}", display_register(dst), value);
                Type::from(value)
            }
            BPF_PSEUDO_MAP_IDX => {
                let map_index = lower;
                bpf_log!(
                    self,
                    context,
                    "lddw {}, map_by_index({:x})",
                    display_register(dst),
                    map_index
                );
                context
                    .calling_context
                    .maps
                    .get(usize::try_from(map_index).unwrap())
                    .map(|schema| Type::ConstPtrToMap { id: map_index.into(), schema: *schema })
                    .ok_or(VerifierErrorKind::InvalidMapIndex(map_index))?
            }
            BPF_PSEUDO_MAP_IDX_VALUE => {
                let map_index = lower;
                let offset = next_instruction.imm();
                bpf_log!(
                    self,
                    context,
                    "lddw {}, map_value_by_index({:x})+{offset}",
                    display_register(dst),
                    map_index
                );
                let id = context.next_id();
                let map_schema = context
                    .calling_context
                    .maps
                    .get(usize::try_from(map_index).unwrap())
                    .ok_or(VerifierErrorKind::InvalidMapIndex(map_index))?;

                if map_schema.map_type != bpf_map_type_BPF_MAP_TYPE_ARRAY {
                    return Err(VerifierErrorKind::LddwMapValueNotArray(
                        map_index,
                        map_schema.map_type,
                    ));
                }
                if map_schema.max_entries == 0 {
                    return Err(VerifierErrorKind::EmptyArrayMap);
                }

                let origin = if map_schema.flags.contains(MapFlags::ProgReadOnly) {
                    PointerOrigin::MapReadOnly
                } else {
                    PointerOrigin::MapWritable
                };
                Type::PtrToMemory {
                    id: MemoryId::from(id),
                    offset: offset.into(),
                    buffer_size: map_schema.value_size.into(),
                    origin,
                }
            }
            _ => {
                return Err(VerifierErrorKind::UnsupportedLddwSource(src));
            }
        };

        let parent = Arc::new(self.clone());
        let mut next = self.jump_with_offset(1, parent)?;
        next.set_reg(dst, value.into())?;

        context.states.push(next);
        Ok(())
    }

    fn load_from_packet<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        src: Register,
        offset: i32,
        register_offset: Option<Register>,
        width: DataWidth,
    ) -> Result<(), VerifierErrorKind> {
        bpf_log!(
            self,
            context,
            "ldp{} {}{}",
            width.str(),
            register_offset.map(display_register).unwrap_or_else(Default::default),
            print_offset(offset)
        );

        // Verify that `src` refers to a packet.
        let src_type = self.reg(src)?;
        let src_is_packet = match &context.calling_context.packet_type {
            Some(packet_type) => src_type == *packet_type,
            None => false,
        };
        if !src_is_packet {
            return Err(VerifierErrorKind::RegisterNotPacket(src));
        }

        if let Some(reg) = register_offset {
            let reg = self.reg(reg)?;
            if !reg.is_written_scalar() {
                return Err(VerifierErrorKind::UninitializedPacketOffset);
            }
        }
        // Handle the case where the load fails.
        if !self.reg(0)?.is_written_scalar() {
            return Err(VerifierErrorKind::InvalidReturnValue);
        }
        if !self.resources.is_empty() {
            return Err(VerifierErrorKind::ResourceLeak);
        }
        // `self` is not terminated here: a copy of it is the parent of `next`, and terminates with
        // the dependencies of both paths once `next` terminates. Terminating `self` would record
        // it as a terminating context with the dependencies of the exit path only.

        // Handle the case where the load succeed.
        let mut next = self.next()?;
        next.set_reg(dst, Type::UNKNOWN_SCALAR)?;
        for i in 1..=5 {
            next.set_reg(i, Type::default())?;
        }
        context.states.push(next);
        Ok(())
    }

    fn store<'a>(
        &mut self,
        context: &mut Self::Context<'a>,
        dst: Register,
        offset: i16,
        src: Source,
        width: DataWidth,
    ) -> Result<(), VerifierErrorKind> {
        let value = match src {
            Source::Reg(r) => {
                bpf_log!(
                    self,
                    context,
                    "stx{} [{}{}], {}",
                    width.str(),
                    display_register(dst),
                    print_offset(offset),
                    display_register(r),
                );
                self.reg(r)?
            }
            Source::Value(v) => {
                bpf_log!(
                    self,
                    context,
                    "st{} [{}{}], 0x{:x}",
                    width.str(),
                    display_register(dst),
                    print_offset(offset),
                    v,
                );
                Type::from(v & Type::mask(width))
            }
        };
        let mut next = self.next()?;
        let addr = self.reg(dst)?;
        next.store_memory(context, &addr, Field::new(offset, width), value)?;
        context.states.push(next);
        Ok(())
    }
}

fn alu32(
    x: ScalarValueData,
    y: ScalarValueData,
    op: impl FnOnce(U32ScalarValueData, U32ScalarValueData) -> U32ScalarValueData,
) -> ScalarValueData {
    op(U32ScalarValueData::from(x), U32ScalarValueData::from(y)).into()
}

fn comp64(
    x: ScalarValueData,
    y: ScalarValueData,
    op: impl FnOnce(U64Range, U64Range) -> Option<bool>,
) -> Result<Option<bool>, ()> {
    if !x.is_fully_initialized() || !y.is_fully_initialized() {
        return Err(());
    }
    Ok(op(x.urange, y.urange))
}

fn comp32(
    x: ScalarValueData,
    y: ScalarValueData,
    op: impl FnOnce(U32Range, U32Range) -> Option<bool>,
) -> Result<Option<bool>, ()> {
    let x = U32ScalarValueData::from(x);
    let y = U32ScalarValueData::from(y);
    if !x.is_fully_initialized() || !y.is_fully_initialized() {
        return Err(());
    }
    Ok(op(x.urange, y.urange))
}

fn scomp64(
    x: ScalarValueData,
    y: ScalarValueData,
    op: impl FnOnce(i64, i64) -> bool,
) -> Result<Option<bool>, ()> {
    if !x.is_fully_initialized() || !y.is_fully_initialized() {
        return Err(());
    }
    if !x.is_known() || !y.is_known() {
        return Ok(None);
    }
    Ok(Some(op(x.value as i64, y.value as i64)))
}

fn scomp32(
    x: ScalarValueData,
    y: ScalarValueData,
    op: impl FnOnce(i32, i32) -> bool,
) -> Result<Option<bool>, ()> {
    let x = U32ScalarValueData::from(x);
    let y = U32ScalarValueData::from(y);
    if !x.is_fully_initialized() || !y.is_fully_initialized() {
        return Err(());
    }
    if !x.is_known() || !y.is_known() {
        return Ok(None);
    }
    Ok(Some(op(x.value as i32, y.value as i32)))
}

fn print_offset<T: Into<i32>>(offset: T) -> String {
    let offset: i32 = offset.into();
    if offset == 0 {
        String::new()
    } else if offset > 0 {
        format!("+{offset}")
    } else {
        format!("{offset}")
    }
}

fn run_on_stack_offset<F>(v: StackOffset, f: F) -> StackOffset
where
    F: FnOnce(ScalarValueData) -> ScalarValueData,
{
    StackOffset(f(v.reg()))
}

fn error_and_log<T>(
    logger: &mut dyn VerifierLogger,
    err: VerifierError,
) -> Result<T, VerifierError> {
    logger.log(err.to_string().as_bytes());
    Err(err)
}

fn associate_orderings(o1: Ordering, o2: Ordering) -> Option<Ordering> {
    match (o1, o2) {
        (o1, o2) if o1 == o2 => Some(o1),
        (o, Ordering::Equal) | (Ordering::Equal, o) => Some(o),
        _ => None,
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::{BPF_ADD, BPF_ALU64, BPF_K, BPF_MOV};
    use std::collections::BTreeSet;
    use test_util::{assert_geq, assert_leq};

    #[test]
    fn test_type_ordering() {
        let t0 = Type::from(0);
        let t1 = Type::from(1);
        let random = Type::AliasParameter { parameter_index: 8 };
        let unknown_written = Type::UNKNOWN_SCALAR;
        let unwritten = Type::default();

        assert_eq!(t0.partial_cmp(&t0), Some(Ordering::Equal));
        assert_eq!(t0.partial_cmp(&t1), None);
        assert_eq!(t0.partial_cmp(&random), None);
        assert_eq!(t0.partial_cmp(&unknown_written), Some(Ordering::Less));
        assert_eq!(t0.partial_cmp(&unwritten), Some(Ordering::Less));

        assert_eq!(t1.partial_cmp(&t0), None);
        assert_eq!(t1.partial_cmp(&t1), Some(Ordering::Equal));
        assert_eq!(t1.partial_cmp(&random), None);
        assert_eq!(t1.partial_cmp(&unknown_written), Some(Ordering::Less));
        assert_eq!(t1.partial_cmp(&unwritten), Some(Ordering::Less));

        assert_eq!(random.partial_cmp(&t0), None);
        assert_eq!(random.partial_cmp(&t1), None);
        assert_eq!(random.partial_cmp(&random), Some(Ordering::Equal));
        assert_eq!(random.partial_cmp(&unknown_written), None);
        assert_eq!(random.partial_cmp(&unwritten), Some(Ordering::Less));

        assert_eq!(unknown_written.partial_cmp(&t0), Some(Ordering::Greater));
        assert_eq!(unknown_written.partial_cmp(&t1), Some(Ordering::Greater));
        assert_eq!(unknown_written.partial_cmp(&random), None);
        assert_eq!(unknown_written.partial_cmp(&unknown_written), Some(Ordering::Equal));
        assert_eq!(unknown_written.partial_cmp(&unwritten), Some(Ordering::Less));

        assert_eq!(unwritten.partial_cmp(&t0), Some(Ordering::Greater));
        assert_eq!(unwritten.partial_cmp(&t1), Some(Ordering::Greater));
        assert_eq!(unwritten.partial_cmp(&random), Some(Ordering::Greater));
        assert_eq!(unwritten.partial_cmp(&unknown_written), Some(Ordering::Greater));
        assert_eq!(unwritten.partial_cmp(&unwritten), Some(Ordering::Equal));
    }

    #[test]
    fn test_stack_ordering() {
        let mut s1 = Stack::default();
        let mut s2 = Stack::default();

        assert_eq!(s1.partial_cmp(&s2), Some(Ordering::Equal));
        s1.set(0, 0.into());
        assert_eq!(s1.partial_cmp(&s1.clone()), Some(Ordering::Equal));
        assert_eq!(s1.partial_cmp(&s2), Some(Ordering::Less));
        assert_eq!(s2.partial_cmp(&s1), Some(Ordering::Greater));
        s2.set(0, Type::UNKNOWN_SCALAR);
        assert_eq!(s1.partial_cmp(&s2), Some(Ordering::Less));
        assert_eq!(s2.partial_cmp(&s1), Some(Ordering::Greater));
        s1.set(1, 1.into());
        assert_eq!(s1.partial_cmp(&s2), Some(Ordering::Less));
        assert_eq!(s2.partial_cmp(&s1), Some(Ordering::Greater));
        s2.set(2, 1.into());
        assert_eq!(s1.partial_cmp(&s2), None);
        assert_eq!(s2.partial_cmp(&s1), None);
    }

    #[test]
    fn test_stack_set_and_retain() {
        let mut s = Stack::default();
        for index in [5, 63, 0, 9] {
            s.set(index, (index as u64).into());
        }
        let mut copy = s.clone();
        s.set(5, 5.into());
        assert!(Arc::ptr_eq(&s.data, &copy.data));
        s.set_null(&MemoryId::new(), true);
        assert!(Arc::ptr_eq(&s.data, &copy.data));
        let mut copy_to_clear = copy.clone();
        assert_eq!(Arc::strong_count(&copy.data), 3);
        copy_to_clear.retain(0);
        assert_eq!(copy_to_clear.mask, 0);
        assert!(copy_to_clear.data.is_empty());
        assert_eq!(Arc::strong_count(&copy.data), 2);
        s.set(9, Type::UNINITIALIZED);
        s.set(10, Type::UNINITIALIZED);
        s.set(63, 1.into());
        assert_eq!(copy.get(9), &Type::from(9));
        assert_eq!(copy.get(63), &Type::from(63));
        let id = MemoryId::new();
        copy.set(5, Type::NullOr { id: id.clone(), inner: Type::from(42).into() });
        copy.set_null(&id, false);
        assert_eq!(copy.get(5), &Type::from(42));
        s.retain(!(1 << 5));
        assert_eq!(s.mask, 1 | (1 << 63));
        assert_eq!(*s.data, vec![Type::from(0), Type::from(1)]);
        for index in [5, 9, 10] {
            assert_eq!(s.get(index), &Type::UNINITIALIZED);
        }
        s.retain(0);
        assert_eq!(s.mask, 0);
        assert!(s.data.is_empty());
        assert_eq!(copy.mask, 1 | (1 << 5) | (1 << 9) | (1 << 63));
    }

    #[test]
    fn test_context_ordering() {
        let mut c1 = ComputationContext::default();
        let mut c2 = ComputationContext::default();

        assert_eq!(c1.partial_cmp(&c2), Some(Ordering::Equal));

        c1.array_bounds.insert(1.into(), 5);
        assert_eq!(c1.partial_cmp(&c2), Some(Ordering::Less));
        assert_eq!(c2.partial_cmp(&c1), Some(Ordering::Greater));

        c2.array_bounds.insert(1.into(), 7);
        assert_eq!(c1.partial_cmp(&c2), Some(Ordering::Greater));
        assert_eq!(c2.partial_cmp(&c1), Some(Ordering::Less));

        c1.array_bounds.insert(2.into(), 9);
        assert_eq!(c1.partial_cmp(&c2), None);
        assert_eq!(c2.partial_cmp(&c1), None);

        c2.array_bounds.insert(2.into(), 9);
        assert_eq!(c1.partial_cmp(&c2), Some(Ordering::Greater));
        assert_eq!(c2.partial_cmp(&c1), Some(Ordering::Less));

        c2.array_bounds.insert(3.into(), 12);
        assert_eq!(c1.partial_cmp(&c2), Some(Ordering::Greater));
        assert_eq!(c2.partial_cmp(&c1), Some(Ordering::Less));

        c1.pc = 8;
        assert_eq!(c1.partial_cmp(&c2), None);
        assert_eq!(c2.partial_cmp(&c1), None);
    }

    /// A sample of types covering the cases distinguished by `Type::partial_cmp`.
    fn sample_types() -> Vec<Type> {
        let id = MemoryId::from(1);
        vec![
            Type::UNINITIALIZED,
            Type::UNKNOWN_SCALAR,
            Type::from(0),
            Type::from(1),
            Type::from(u64::MAX),
            Type::ScalarValue(ScalarValueData::new(0, 0xff, 0, U64Range::new(0, 0xff))),
            Type::ScalarValue(ScalarValueData::new(0, 0xff, 0, U64Range::new(0, 1))),
            Type::ScalarValue(ScalarValueData::new(0, 0xff, 0xff, U64Range::new(0, 0xff))),
            Type::ScalarValue(ScalarValueData::new(0x100, 0xff, 0, U64Range::new(0x100, 0x1ff))),
            Type::PtrToMemory {
                id: id.clone(),
                offset: 0.into(),
                buffer_size: 8,
                origin: PointerOrigin::MapWritable,
            },
            Type::PtrToArray { id, offset: 1.into() },
        ]
    }

    #[test]
    fn test_known_scalars_is_necessary_for_greater_or_equal() {
        let types = sample_types();
        // Check every pair of types in r0, and in r1 with a known scalar in r0.
        for t1 in types.iter() {
            for t2 in types.iter() {
                for r0 in [None, Some(Type::from(3))] {
                    let mut c1 = ComputationContext::default();
                    let mut c2 = ComputationContext::default();
                    let index = if r0.is_some() { 1 } else { 0 };
                    if let Some(r0) = r0 {
                        c1.set_reg(0, r0.clone()).unwrap();
                        c2.set_reg(0, r0).unwrap();
                    }
                    c1.set_reg(index, t1.clone()).unwrap();
                    c2.set_reg(index, t2.clone()).unwrap();
                    let k1 = KnownScalars::new(&c1);
                    let k2 = KnownScalars::new(&c2);
                    if matches!(c1.partial_cmp(&c2), Some(Ordering::Greater | Ordering::Equal)) {
                        assert!(k1 >= k2, "{t1:?} >= {t2:?}");
                    }
                    if matches!(c1.partial_cmp(&c2), Some(Ordering::Less | Ordering::Equal)) {
                        assert!(k1 <= k2, "{t1:?} <= {t2:?}");
                    }
                }
            }
        }
    }

    #[test]
    fn test_known_scalars_filters_distinct_constants() {
        let mut c1 = ComputationContext::default();
        let mut c2 = ComputationContext::default();
        c1.set_reg(7, Type::from(1)).unwrap();
        c2.set_reg(7, Type::from(2)).unwrap();
        let k1 = KnownScalars::new(&c1);
        let k2 = KnownScalars::new(&c2);
        assert_eq!(k1.partial_cmp(&k2), None);
        assert_eq!(k2.partial_cmp(&k1), None);

        // An unknown or uninitialized register may be greater than a known one, but not less.
        c2.set_reg(7, Type::UNKNOWN_SCALAR).unwrap();
        let k2 = KnownScalars::new(&c2);
        assert!(k1 < k2);
        assert!(k1 < KnownScalars::default());
    }

    #[test]
    fn test_terminating_contexts_matches_unfiltered_search() {
        // Insert contexts in a fixed pseudo random order and check that the filtered search and
        // insertion behave exactly like a plain linear search over the full comparison.
        let types = sample_types();
        let mut contexts = TerminatingContexts::default();
        let mut reference: Vec<ComputationContext> = vec![];
        let mut seed = 17usize;
        for _ in 0..200 {
            let mut context = ComputationContext::default();
            for reg in 0..3 {
                seed = seed.wrapping_mul(1103515245).wrapping_add(12345);
                context.set_reg(reg, types[(seed >> 16) % types.len()].clone()).unwrap();
            }

            let expected = reference.iter().rposition(|c| *c >= context);
            let found = contexts.find_greater_or_equal(&context).map(|found| {
                contexts.contexts.iter().position(|c| std::ptr::eq(c, found)).unwrap()
            });
            assert_eq!(found, expected);

            let dominated = reference.iter().any(|c| *c >= context);
            reference.retain(|c| c.partial_cmp(&context) != Some(Ordering::Less));
            if !dominated {
                reference.push(context.clone());
            }
            contexts.insert(context, DataDependencies::default());
            assert_eq!(contexts.contexts.len(), reference.len());
            for (c, r) in contexts.contexts.iter().zip(reference.iter()) {
                assert_eq!(&c.computation_context, r);
            }
        }
    }

    #[test]
    fn test_stack_access() {
        let mut s = Stack::default();

        // Store data in the range [8, 26) and verify that `read_data_ptr()` fails for any
        // reads outside of that range.
        assert!(s.store(StackOffset(8.into()), Type::UNKNOWN_SCALAR, DataWidth::U64).is_ok());
        assert!(s.store(StackOffset(16.into()), Type::UNKNOWN_SCALAR, DataWidth::U64).is_ok());
        assert!(s.store(StackOffset(24.into()), Type::UNKNOWN_SCALAR, DataWidth::U16).is_ok());

        for offset in 0..32 {
            for end in (offset + 1)..32 {
                assert_eq!(
                    s.read_data_ptr(StackOffset(offset.into()), (end - offset) as u64).is_ok(),
                    offset >= 8 && end <= 26
                );
            }
        }

        // Verify that overflows are handled properly.
        assert!(s.read_data_ptr(StackOffset(12.into()), u64::MAX - 2).is_err());
    }

    #[test]
    fn test_compute_range_for_bytes_swap() {
        // Build a list of interesting values. Interesting values are all possible combination of
        // bytes being either 0, max value, or an intermediary value.
        let mut values = BTreeSet::<u64>::default();
        for v1 in &[0x00, 0x1, u64::MAX] {
            for v2 in &[0x00, 0x1, u64::MAX] {
                for v3 in &[0x00, 0x1, u64::MAX] {
                    values.insert(U64Range::assemble_slices((*v1, *v2, *v3), 1, 1));
                }
            }
        }
        // Replace the second byte of old by the first byte of new and return the result.
        let store = |old: u64, new: u64| (old & !0xff00) | ((new & 0xff) << 8);

        for old in &values {
            for new in &values {
                let s = store(*old, *new);
                for min_old in values.iter().filter(|v| *v <= old) {
                    for min_new in values.iter().filter(|v| *v <= new) {
                        for max_old in values.iter().filter(|v| *v >= old) {
                            for max_new in values.iter().filter(|v| *v >= new) {
                                let range = U64Range::compute_range_for_bytes_swap(
                                    U64Range::new(*min_old, *max_old),
                                    U64Range::new(*min_new, *max_new),
                                    1,
                                    0,
                                    1,
                                );
                                assert_leq!(range.min, s);
                                assert_geq!(range.max, s);
                            }
                        }
                    }
                }
            }
        }
    }

    #[test]
    fn test_type_constraint_ge_gt() {
        let mut context = ComputationContext::default();
        let (new_lhs, new_rhs) = Type::constraint(
            &mut context,
            JumpType::Ge,
            JumpWidth::W64,
            Type::UNKNOWN_SCALAR,
            Type::from(10),
        )
        .unwrap();

        if let Type::ScalarValue(data1) = new_lhs {
            assert_eq!(data1.min(), 10);
            assert_eq!(data1.max(), u64::MAX);
        } else {
            panic!("Expected ScalarValue");
        }

        if let Type::ScalarValue(data2) = new_rhs {
            assert_eq!(data2.min(), 10);
            assert_eq!(data2.max(), 10);
        } else {
            panic!("Expected ScalarValue");
        }

        let (new_lhs, _) = Type::constraint(
            &mut context,
            JumpType::Gt,
            JumpWidth::W64,
            Type::UNKNOWN_SCALAR,
            Type::from(10),
        )
        .unwrap();

        if let Type::ScalarValue(data1) = new_lhs {
            assert_eq!(data1.min(), 11);
            assert_eq!(data1.max(), u64::MAX);
        } else {
            panic!("Expected ScalarValue");
        }
    }

    #[test]
    fn test_type_constraint_lt_le() {
        let mut context = ComputationContext::default();
        let (new_lhs, _) = Type::constraint(
            &mut context,
            JumpType::Lt,
            JumpWidth::W64,
            Type::UNKNOWN_SCALAR,
            Type::from(10),
        )
        .unwrap();

        if let Type::ScalarValue(data1) = new_lhs {
            assert_eq!(data1.min(), 0);
            assert_eq!(data1.max(), 9);
        } else {
            panic!("Expected ScalarValue");
        }

        let (new_lhs, _) = Type::constraint(
            &mut context,
            JumpType::Le,
            JumpWidth::W64,
            Type::UNKNOWN_SCALAR,
            Type::from(10),
        )
        .unwrap();

        if let Type::ScalarValue(data1) = new_lhs {
            assert_eq!(data1.min(), 0);
            assert_eq!(data1.max(), 10);
        } else {
            panic!("Expected ScalarValue");
        }
    }

    #[test]
    fn test_type_constraint_w32() {
        let mut context = ComputationContext::default();
        let (new_lhs, _) = Type::constraint(
            &mut context,
            JumpType::Eq,
            JumpWidth::W32,
            Type::ScalarValue(ScalarValueData::UNKNOWN_WRITTEN),
            Type::from(10),
        )
        .unwrap();
        if let Type::ScalarValue(data1) = new_lhs {
            assert_eq!(data1.min(), 10);
            assert_eq!(data1.max(), 0xffff_ffff_0000_000a);
        } else {
            panic!("Expected ScalarValue");
        }
    }

    #[test]
    fn test_type_constraint_w32_straddling_min() {
        // A 32-bit equality only constrains the low 32 bits. When the comparison
        // partner's range straddles 2^32 (min <= U32_MAX < max), its low 32 bits
        // can be smaller than its minimum, so the other register's minimum must
        // not be raised. `data1` is in [0, 0x40]; `data2` is in [0x30, u64::MAX].
        // On the equal branch `data1` can still be 0 (e.g. when `data2 == 2^32`,
        // whose low 32 bits are 0), so its minimum must remain 0.
        let mut context = ComputationContext::default();
        let data1 = ScalarValueData::new(0, u64::MAX, 0, U64Range::new(0, 0x40));
        let data2 = ScalarValueData::new(0, u64::MAX, 0, U64Range::new(0x30, u64::MAX));
        let (new_lhs, _) = Type::constraint(
            &mut context,
            JumpType::Eq,
            JumpWidth::W32,
            Type::ScalarValue(data1),
            Type::ScalarValue(data2),
        )
        .unwrap();
        if let Type::ScalarValue(data) = new_lhs {
            assert_eq!(data.min(), 0);
            assert_eq!(data.max(), 0x40);
        } else {
            panic!("Expected ScalarValue");
        }
    }

    #[test]
    fn test_type_constraint_null_or() {
        let mut context = ComputationContext::default();
        let id = MemoryId::new();
        let null_or = Type::NullOr { id: id.clone(), inner: Box::new(Type::UNKNOWN_SCALAR) };
        let (new_lhs, _) =
            Type::constraint(&mut context, JumpType::Eq, JumpWidth::W64, null_or, Type::from(0))
                .unwrap();
        if let Type::ScalarValue(data) = new_lhs {
            assert_eq!(data.value, 0);
        } else {
            panic!("Expected zero ScalarValue");
        }
    }

    #[test]
    fn test_type_constraint_array_bounds() {
        let mut context = ComputationContext::default();
        let id = MemoryId::new();
        let _ = Type::constraint(
            &mut context,
            JumpType::Le,
            JumpWidth::W64,
            Type::PtrToArray { id: id.clone(), offset: 22.into() },
            Type::PtrToEndArray { id: id.clone() },
        )
        .unwrap();
        assert_eq!(context.array_bounds.get(&id), Some(&22));
    }

    fn make_verification_context<'a>(
        logger: &'a mut dyn VerifierLogger,
    ) -> VerificationContext<'a> {
        VerificationContext::new(CallingContext::default(), logger, &[], vec![], vec![])
    }

    /// Verifies that multiple invocations returning PtrToMemory receive
    /// distinct MemoryIds to prevent ASLR pointer arithmetic between separate
    /// allocations, while still matching the static parameter templates.
    #[test]
    fn test_resolve_return_value_unique_ids() {
        let mut logger = NullVerifierLogger;
        let mut verification_context = make_verification_context(&mut logger);
        let comp_ctx = ComputationContext::default();

        let static_id = MemoryId::from_raw(42);
        let ret_template = Type::PtrToMemory {
            id: static_id.clone(),
            offset: 0.into(),
            buffer_size: 64,
            origin: PointerOrigin::KernelReadOnly,
        };

        let mut next1 = ComputationContext::default();
        let t1 = comp_ctx
            .resolve_return_value(&mut verification_context, &ret_template, &mut next1, false)
            .unwrap();
        let mut next2 = ComputationContext::default();
        let t2 = comp_ctx
            .resolve_return_value(&mut verification_context, &ret_template, &mut next2, false)
            .unwrap();

        assert_ne!(t1, t2);
        let (Type::PtrToMemory { id: id1, .. }, Type::PtrToMemory { id: id2, .. }) = (&t1, &t2)
        else {
            panic!("Expected PtrToMemory");
        };
        assert_ne!(id1, id2);
        assert!(static_id.matches(id1));
        assert!(static_id.matches(id2));
    }

    /// Verifies that multiple releasable allocations are tracked individually
    /// in resources, releasing one does not remove the other, and passing a
    /// released resource to a helper parameter is rejected.
    #[test]
    fn test_resolve_return_value_releasable_resource_tracking() {
        let mut logger = NullVerifierLogger;
        let mut verification_context = make_verification_context(&mut logger);
        let comp_ctx = ComputationContext::default();

        let static_id = MemoryId::from_raw(99);
        let releasable_template = Type::ReleasableParameter {
            id: static_id.clone(),
            inner: Box::new(Type::PtrToMemory {
                id: static_id.clone(),
                offset: 0.into(),
                buffer_size: 64,
                origin: PointerOrigin::KernelReadOnly,
            }),
        };

        let mut next = ComputationContext::default();
        let t1 = comp_ctx
            .resolve_return_value(&mut verification_context, &releasable_template, &mut next, false)
            .unwrap();
        let t2 = comp_ctx
            .resolve_return_value(&mut verification_context, &releasable_template, &mut next, false)
            .unwrap();

        assert_eq!(next.resources.len(), 2);
        let (Type::Releasable { id: id1, .. }, Type::Releasable { id: id2, .. }) = (&t1, &t2)
        else {
            panic!("Expected Releasable");
        };
        assert_ne!(id1, id2);
        assert!(next.resources.contains(id1));
        assert!(next.resources.contains(id2));

        // Release one
        let mut next_after_free = next.clone();
        t1.match_parameter_type(
            &verification_context,
            &comp_ctx,
            "test_free",
            &Type::ReleaseParameter { id: static_id.clone() },
            0,
            &mut next_after_free,
        )
        .unwrap();
        assert_eq!(next_after_free.resources.len(), 1);
        assert!(!next_after_free.resources.contains(id1));
        assert!(next_after_free.resources.contains(id2));

        // Passing released t1 to general helper must fail
        let mut next_uaf = next_after_free.clone();
        let err = t1.match_parameter_type(
            &verification_context,
            &comp_ctx,
            "test_helper",
            &Type::MemoryParameter {
                size: MemoryParameterSize::Value(64),
                input: true,
                output: false,
            },
            0,
            &mut next_uaf,
        );
        assert!(err.is_err());
        assert_eq!(err.unwrap_err(), VerifierErrorKind::UseAfterRelease);
    }

    #[test]
    fn ptr_to_struct_ordering() {
        let desc1 = Arc::new(StructDescriptor {
            fields: vec![
                FieldDescriptor { offset: 0, field_type: FieldType::Scalar { size: 4 } },
                FieldDescriptor { offset: 4, field_type: FieldType::MutableScalar { size: 4 } },
            ],
        });
        let desc1_same_contents = Arc::new(StructDescriptor {
            fields: vec![
                FieldDescriptor { offset: 0, field_type: FieldType::Scalar { size: 4 } },
                FieldDescriptor { offset: 4, field_type: FieldType::MutableScalar { size: 4 } },
            ],
        });
        let desc_other = Arc::new(StructDescriptor {
            fields: vec![FieldDescriptor { offset: 0, field_type: FieldType::Scalar { size: 4 } }],
        });

        let id = MemoryId::from_raw(1);
        let ptr_a =
            Type::PtrToStruct { id: id.clone(), offset: 0.into(), descriptor: Arc::clone(&desc1) };
        let ptr_b_shared_arc =
            Type::PtrToStruct { id: id.clone(), offset: 0.into(), descriptor: Arc::clone(&desc1) };
        let ptr_c_distinct_arc = Type::PtrToStruct {
            id: id.clone(),
            offset: 0.into(),
            descriptor: Arc::clone(&desc1_same_contents),
        };
        let ptr_different_offset =
            Type::PtrToStruct { id: id.clone(), offset: 4.into(), descriptor: Arc::clone(&desc1) };
        let ptr_other_desc =
            Type::PtrToStruct { id, offset: 0.into(), descriptor: Arc::clone(&desc_other) };

        // Shared Arc (pointer-equal fast path) and distinct Arc with equal fields both compare
        // Equal.
        assert_eq!(ptr_a.partial_cmp(&ptr_b_shared_arc), Some(Ordering::Equal));
        assert_eq!(ptr_a.partial_cmp(&ptr_c_distinct_arc), Some(Ordering::Equal));
        assert_eq!(ptr_a.partial_cmp(&ptr_different_offset), None);
        assert_eq!(ptr_a.partial_cmp(&ptr_other_desc), None);

        // Non-scalars are strictly narrower than UNINITIALIZED and incomparable with initialized
        // or narrowed uninitialized scalars.
        let narrowed_uninit = Type::ScalarValue(ScalarValueData::UNINITIALIZED & 7.into());
        assert_eq!(ptr_a.partial_cmp(&Type::UNINITIALIZED), Some(Ordering::Less));
        assert_eq!(Type::UNINITIALIZED.partial_cmp(&ptr_a), Some(Ordering::Greater));
        assert_eq!(ptr_a.partial_cmp(&Type::UNKNOWN_SCALAR), None);
        assert_eq!(Type::UNKNOWN_SCALAR.partial_cmp(&ptr_a), None);
        assert_eq!(ptr_a.partial_cmp(&narrowed_uninit), None);
        assert_eq!(narrowed_uninit.partial_cmp(&ptr_a), None);

        // Narrowed uninitialized scalar (`unwritten_mask == u64::MAX`, `urange == [0, 7]`) is
        // strictly narrower than `Type::UNINITIALIZED`, broader than `5`, and incomparable with
        // out-of-range `1000`.
        assert_eq!(Type::UNINITIALIZED.partial_cmp(&narrowed_uninit), Some(Ordering::Greater));
        assert_eq!(narrowed_uninit.partial_cmp(&Type::UNINITIALIZED), Some(Ordering::Less));
        assert_eq!(narrowed_uninit.partial_cmp(&Type::from(5)), Some(Ordering::Greater));
        assert_eq!(Type::from(5).partial_cmp(&narrowed_uninit), Some(Ordering::Less));
        assert_eq!(narrowed_uninit.partial_cmp(&Type::from(1000)), None);
        assert_eq!(Type::from(1000).partial_cmp(&narrowed_uninit), None);
    }

    #[test]
    fn stack_ordering_disjoint_and_overlapping_keys() {
        let mut s_broad = Stack::default();
        let mut s_narrow = Stack::default();

        // Populate s_narrow at keys 1, 3, 5; keep s_broad empty (all UNINITIALIZED).
        s_narrow.set(1, Type::from(10));
        s_narrow.set(3, Type::from(20));
        s_narrow.set(5, Type::from(30));
        assert_eq!(s_broad.partial_cmp(&s_narrow), Some(Ordering::Greater));
        assert_eq!(s_narrow.partial_cmp(&s_broad), Some(Ordering::Less));

        // Add middle key 3 to s_broad with a broader type (UNKNOWN_SCALAR > 20).
        // s_narrow has an earlier key (1 < 3) and a later key (5 > 3), exercising both
        // `Ordering::Greater` on `k1.cmp(k2)` and `(None, Some(_))` after `s_broad` is exhausted.
        s_broad.set(3, Type::UNKNOWN_SCALAR);
        assert_eq!(s_broad.partial_cmp(&s_narrow), Some(Ordering::Greater));
        assert_eq!(s_narrow.partial_cmp(&s_broad), Some(Ordering::Less));

        // Setting a slot to UNINITIALIZED removes it from the map and preserves the ordering,
        // whereas a narrowed uninitialized scalar stays in the map and is strictly narrower than
        // an empty (all UNINITIALIZED) stack.
        s_broad.set(3, Type::UNINITIALIZED);
        assert!(s_broad.data.is_empty());
        assert_eq!(s_broad.partial_cmp(&s_narrow), Some(Ordering::Greater));
        let mut s_narrowed_uninit = Stack::default();
        s_narrowed_uninit.set(0, Type::ScalarValue(ScalarValueData::UNINITIALIZED & 7.into()));
        assert_eq!(s_broad.partial_cmp(&s_narrowed_uninit), Some(Ordering::Greater));
        assert_eq!(s_narrowed_uninit.partial_cmp(&s_broad), Some(Ordering::Less));

        // Conflicting orderings at overlapping keys must return None.
        s_broad.set(1, Type::from(10));
        s_broad.set(3, Type::UNKNOWN_SCALAR);
        s_broad.set(5, Type::from(99));
        assert_eq!(s_broad.partial_cmp(&s_narrow), None);
        assert_eq!(s_narrow.partial_cmp(&s_broad), None);
    }

    #[test]
    fn test_verifier_logger_is_enabled() {
        struct LimitedLogger {
            max_lines: usize,
            lines: Vec<String>,
        }

        impl VerifierLogger for LimitedLogger {
            fn is_enabled(&self) -> bool {
                self.lines.len() < self.max_lines
            }

            fn log(&mut self, line: &[u8]) {
                assert!(line.is_ascii());
                self.lines.push(std::str::from_utf8(line).unwrap().to_string());
            }
        }

        let code = vec![
            EbpfInstruction::new(BPF_ALU64 | BPF_MOV | BPF_K, 0, 0, 0, 0),
            EbpfInstruction::new(BPF_ALU64 | BPF_ADD | BPF_K, 0, 0, 0, 1),
            EbpfInstruction::new(BPF_JMP | BPF_EXIT, 0, 0, 0, 0),
        ];

        let mut full_logger = LimitedLogger { max_lines: usize::MAX, lines: vec![] };
        verify_program(code.clone(), CallingContext::default(), &mut full_logger).unwrap();
        assert_eq!(
            full_logger.lines,
            vec!["0: (b7) mov %r0, 0x0", "1: (07) add %r0, 0x1", "2: (95) exit"]
        );

        let mut capped_logger = LimitedLogger { max_lines: 2, lines: vec![] };
        verify_program(code, CallingContext::default(), &mut capped_logger).unwrap();
        assert_eq!(capped_logger.lines, vec!["0: (b7) mov %r0, 0x0", "1: (07) add %r0, 0x1"]);
    }

    /// Verifies that memory store instructions to read-only memory pointers are
    /// rejected, while stores to writable pointers succeed.
    #[test]
    fn test_read_only_map_value_store() {
        let mut logger = NullVerifierLogger;
        let mut context = make_verification_context(&mut logger);
        let mut next = ComputationContext::default();

        let ptr_with_origin = |origin| Type::PtrToMemory {
            id: MemoryId::new(),
            offset: 0.into(),
            buffer_size: 4,
            origin,
        };

        let u32_field = Field::new(0, DataWidth::U32);

        // Store to read-only memory must fail.
        let ro_map_ptr = ptr_with_origin(PointerOrigin::MapReadOnly);
        let err = next.store_memory(&mut context, &ro_map_ptr, u32_field, Type::from(42));
        assert_eq!(err, Err(VerifierErrorKind::WriteToReadOnlyMemory));

        let ro_kernel_ptr = ptr_with_origin(PointerOrigin::KernelReadOnly);
        let err = next.store_memory(&mut context, &ro_kernel_ptr, u32_field, Type::from(42));
        assert_eq!(err, Err(VerifierErrorKind::WriteToReadOnlyMemory));

        // Store to writable memory must succeed.
        let rw_map_ptr = ptr_with_origin(PointerOrigin::MapWritable);
        let res = next.store_memory(&mut context, &rw_map_ptr, u32_field, Type::from(42));
        assert!(res.is_ok());

        let rw_kernel_ptr = ptr_with_origin(PointerOrigin::KernelWritable);
        let res = next.store_memory(&mut context, &rw_kernel_ptr, u32_field, Type::from(42));
        assert!(res.is_ok());
    }

    /// Verifies that atomic operations are only allowed on naturally aligned
    /// addresses within the stack or a map value.
    #[test]
    fn test_atomic_access_checks() {
        let context = ComputationContext::default();

        let ptr_to_memory = |offset: ScalarValueData, origin| Type::PtrToMemory {
            id: MemoryId::new(),
            offset,
            buffer_size: 64,
            origin,
        };
        let ptr_to_stack =
            |offset: i16| Type::PtrToStack { offset: StackOffset::default().add(offset) };
        // An offset that is either 0 or 1: its low bit is unknown.
        let unknown_low_bit = ScalarValueData::new(0, 1, 0, U64Range::new(0, 1));
        // An offset that is either 0 or 8: its low 3 bits are known to be 0.
        let unknown_high_bits = ScalarValueData::new(0, 8, 0, U64Range::new(0, 8));

        let u32_field = |offset| Field::new(offset, DataWidth::U32);
        let u64_field = |offset| Field::new(offset, DataWidth::U64);

        // Aligned accesses to map values and the stack are allowed.
        for origin in [PointerOrigin::MapWritable, PointerOrigin::MapReadOnly] {
            let ptr = ptr_to_memory(0.into(), origin);
            assert_eq!(context.check_atomic_access(&ptr, u64_field(8)), Ok(()));
            assert_eq!(context.check_atomic_access(&ptr, u32_field(4)), Ok(()));
            let ptr = ptr_to_memory(4.into(), origin);
            assert_eq!(context.check_atomic_access(&ptr, u64_field(4)), Ok(()));
            assert_eq!(context.check_atomic_access(&ptr, u32_field(-4)), Ok(()));
            let ptr = ptr_to_memory(unknown_high_bits, origin);
            assert_eq!(context.check_atomic_access(&ptr, u64_field(16)), Ok(()));
        }
        assert_eq!(context.check_atomic_access(&ptr_to_stack(-8), u64_field(0)), Ok(()));
        assert_eq!(context.check_atomic_access(&ptr_to_stack(-4), u32_field(-4)), Ok(()));

        // Misaligned accesses are rejected, including when the alignment cannot
        // be proven because the low bits of the offset are unknown.
        let map_ptr = ptr_to_memory(0.into(), PointerOrigin::MapWritable);
        assert_eq!(
            context.check_atomic_access(&map_ptr, u64_field(4)),
            Err(VerifierErrorKind::MisalignedAtomicAccess)
        );
        assert_eq!(
            context.check_atomic_access(&map_ptr, u32_field(2)),
            Err(VerifierErrorKind::MisalignedAtomicAccess)
        );
        let map_ptr = ptr_to_memory(4.into(), PointerOrigin::MapWritable);
        assert_eq!(
            context.check_atomic_access(&map_ptr, u64_field(0)),
            Err(VerifierErrorKind::MisalignedAtomicAccess)
        );
        let map_ptr = ptr_to_memory(unknown_low_bit, PointerOrigin::MapWritable);
        assert_eq!(
            context.check_atomic_access(&map_ptr, u64_field(0)),
            Err(VerifierErrorKind::MisalignedAtomicAccess)
        );
        assert_eq!(
            context.check_atomic_access(&ptr_to_stack(-6), u32_field(0)),
            Err(VerifierErrorKind::MisalignedAtomicAccess)
        );
        assert_eq!(
            context.check_atomic_access(&ptr_to_stack(-8), u64_field(4)),
            Err(VerifierErrorKind::MisalignedAtomicAccess)
        );

        // Atomic accesses to other kinds of memory are rejected, even when
        // aligned.
        for origin in [PointerOrigin::KernelWritable, PointerOrigin::KernelReadOnly] {
            let ptr = ptr_to_memory(0.into(), origin);
            assert_eq!(
                context.check_atomic_access(&ptr, u64_field(8)),
                Err(VerifierErrorKind::AtomicAccessNotAllowed)
            );
        }
        assert_eq!(
            context.check_atomic_access(&Type::from(0), u64_field(0)),
            Err(VerifierErrorKind::AtomicAccessNotAllowed)
        );
    }
}