rapx/analysis/senryx/contracts/
abstract_state.rs

1use std::{
2    collections::{HashMap, HashSet},
3    hash::Hash,
4};
5
6use crate::analysis::senryx::symbolic_analysis::{AnaOperand, SymbolicDef};
7use crate::analysis::senryx::visitor::PlaceTy;
8use rustc_middle::ty::Ty;
9
10/// Tracks pointer alignment status in the abstract domain.
11#[derive(Debug, Clone, PartialEq, Eq)]
12pub enum AlignState<'tcx> {
13    Aligned(Ty<'tcx>),
14    /// Misaligned relative to `u64` by offset `SymbolicDef`.
15    Unaligned(Ty<'tcx>),
16    /// Alignment cannot be statically determined (Top).
17    Unknown,
18}
19
20impl<'tcx> AlignState<'tcx> {
21    /// Merges two states (Lattice Join). Returns the conservative lower bound.
22    pub fn merge(&self, other: &Self) -> Self {
23        if self == other {
24            return other.clone();
25        }
26        match (self, other) {
27            // If both are aligned for the same type, keep the weaker alignment.
28            (AlignState::Aligned(t1), AlignState::Aligned(t2)) => {
29                if t1 == t2 {
30                    AlignState::Aligned(*t1)
31                } else {
32                    AlignState::Unknown
33                }
34            }
35            // Merging unaligned states is complex; default to Unknown for checking soundness.
36            (AlignState::Unaligned(t1), AlignState::Unaligned(t2)) => AlignState::Unknown,
37            _ => AlignState::Unknown,
38        }
39    }
40}
rapx/analysis/senryx/contracts/abstract_state.rs

rapx/analysis/senryx/contracts/
abstract_state.rs
