Skip to main content

oxilean_std/static_analysis/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::functions::*;
6use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet, VecDeque};
7
8/// Eraser algorithm state for a single memory location.
9#[derive(Debug, Clone)]
10pub struct EraserState {
11    /// Current candidate lock set C(v): intersection of all observed lock sets.
12    pub candidate_set: Option<BTreeSet<usize>>,
13    /// Whether a data race has been reported.
14    pub race_reported: bool,
15    /// Last writer thread.
16    pub last_writer: Option<usize>,
17    /// Last access was a write.
18    pub has_write: bool,
19}
20impl EraserState {
21    pub fn new() -> Self {
22        Self {
23            candidate_set: None,
24            race_reported: false,
25            last_writer: None,
26            has_write: false,
27        }
28    }
29    /// Record an access from `thread` holding `locks`.
30    /// `is_write` is true if this is a write access.
31    pub fn observe_access(&mut self, thread: usize, locks: &BTreeSet<usize>, is_write: bool) {
32        self.candidate_set = Some(match &self.candidate_set {
33            None => locks.clone(),
34            Some(prev) => prev.intersection(locks).copied().collect(),
35        });
36        if let Some(ref cs) = self.candidate_set {
37            if cs.is_empty() && (is_write || self.has_write) {
38                if self.last_writer.is_some_and(|w| w != thread) || is_write {
39                    self.race_reported = true;
40                }
41            }
42        }
43        if is_write {
44            self.has_write = true;
45            self.last_writer = Some(thread);
46        }
47    }
48    /// Has a potential race been detected?
49    pub fn has_race(&self) -> bool {
50        self.race_reported
51    }
52}
53/// A generic monotone framework fixpoint solver.
54/// Each node in the program has an associated abstract value.
55pub struct FixpointSolver<V: Clone + PartialEq> {
56    /// Number of program points.
57    pub num_nodes: usize,
58    /// Current abstract values.
59    pub values: Vec<V>,
60    /// CFG edges: edges[n] = successors of n.
61    pub edges: Vec<Vec<usize>>,
62    /// Bottom element.
63    pub bottom: V,
64    /// Join function.
65    pub join: fn(&V, &V) -> V,
66    /// Transfer function: transfer(node, value_in) -> value_out.
67    pub transfer: fn(usize, &V) -> V,
68}
69impl<V: Clone + PartialEq> FixpointSolver<V> {
70    pub fn new(
71        num_nodes: usize,
72        edges: Vec<Vec<usize>>,
73        bottom: V,
74        join: fn(&V, &V) -> V,
75        transfer: fn(usize, &V) -> V,
76    ) -> Self {
77        let values = vec![bottom.clone(); num_nodes];
78        Self {
79            num_nodes,
80            values,
81            edges,
82            bottom,
83            join,
84            transfer,
85        }
86    }
87    /// Run worklist fixpoint iteration.
88    pub fn solve(&mut self) {
89        let mut worklist: VecDeque<usize> = (0..self.num_nodes).collect();
90        while let Some(n) = worklist.pop_front() {
91            let out = (self.transfer)(n, &self.values[n]);
92            for &succ in &self.edges[n].clone() {
93                let new_val = (self.join)(&self.values[succ], &out);
94                if new_val != self.values[succ] {
95                    self.values[succ] = new_val;
96                    worklist.push_back(succ);
97                }
98            }
99        }
100    }
101}
102/// Security label for two-point lattice: Low < High.
103#[allow(dead_code)]
104#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
105pub enum SecurityLevel {
106    Low,
107    High,
108}
109impl SecurityLevel {
110    /// Join in the security lattice.
111    pub fn join(&self, other: &SecurityLevel) -> SecurityLevel {
112        if *self == SecurityLevel::High || *other == SecurityLevel::High {
113            SecurityLevel::High
114        } else {
115            SecurityLevel::Low
116        }
117    }
118    /// Check if `self` can flow to `other` (self ⊑ other).
119    pub fn can_flow_to(&self, other: &SecurityLevel) -> bool {
120        *self <= *other
121    }
122}
123/// Tracks information flow labels for a set of variables.
124#[allow(dead_code)]
125#[derive(Debug, Clone, Default)]
126pub struct IFCTracker {
127    /// Security label for each variable.
128    pub labels: std::collections::HashMap<String, SecurityLevel>,
129    /// Recorded violations: (var, expected_label).
130    pub violations: Vec<(String, SecurityLevel)>,
131}
132impl IFCTracker {
133    /// Create a new tracker.
134    pub fn new() -> Self {
135        Self::default()
136    }
137    /// Assign a security label to a variable.
138    pub fn assign(&mut self, var: impl Into<String>, level: SecurityLevel) {
139        self.labels.insert(var.into(), level);
140    }
141    /// Get the label of a variable (defaults to Low if unknown).
142    pub fn label_of(&self, var: &str) -> SecurityLevel {
143        self.labels.get(var).cloned().unwrap_or(SecurityLevel::Low)
144    }
145    /// Propagate: `dst` gets the join of all source labels.
146    pub fn propagate(&mut self, dst: impl Into<String>, srcs: &[&str]) {
147        let joined = srcs
148            .iter()
149            .fold(SecurityLevel::Low, |acc, &s| acc.join(&self.label_of(s)));
150        let dst = dst.into();
151        self.labels.insert(dst, joined);
152    }
153    /// Check a flow: assert that `var`'s label ⊑ `required`.
154    pub fn check_flow(&mut self, var: &str, required: &SecurityLevel) {
155        let lbl = self.label_of(var);
156        if !lbl.can_flow_to(required) {
157            self.violations.push((var.to_string(), required.clone()));
158        }
159    }
160    /// Returns true if any information flow violation was detected.
161    pub fn has_violation(&self) -> bool {
162        !self.violations.is_empty()
163    }
164}
165/// A simple constant propagation state: maps variables to known constant values
166/// or marks them as non-constant (⊤).
167#[allow(dead_code)]
168#[derive(Debug, Clone, Default)]
169pub struct ConstPropState {
170    /// None = unknown/non-constant (⊤); Some(v) = definitely v.
171    pub values: std::collections::HashMap<String, Option<i64>>,
172}
173impl ConstPropState {
174    /// Create a new state.
175    pub fn new() -> Self {
176        Self::default()
177    }
178    /// Define a variable as a known constant.
179    pub fn set_const(&mut self, var: impl Into<String>, val: i64) {
180        self.values.insert(var.into(), Some(val));
181    }
182    /// Mark a variable as non-constant.
183    pub fn set_top(&mut self, var: impl Into<String>) {
184        self.values.insert(var.into(), None);
185    }
186    /// Get the constant value of a variable, if known.
187    pub fn get(&self, var: &str) -> Option<i64> {
188        self.values.get(var).copied().flatten()
189    }
190    /// Join two states (meet of constant info: agree ⇒ keep, disagree ⇒ top).
191    pub fn join(&self, other: &ConstPropState) -> ConstPropState {
192        let mut result = ConstPropState::new();
193        for (var, &val) in &self.values {
194            let merged = match (val, other.values.get(var).copied().flatten()) {
195                (Some(a), Some(b)) if a == b => Some(a),
196                _ => None,
197            };
198            result.values.insert(var.clone(), merged);
199        }
200        for var in other.values.keys() {
201            if !result.values.contains_key(var) {
202                result.values.insert(var.clone(), None);
203            }
204        }
205        result
206    }
207    /// Attempt constant folding of a binary add expression.
208    pub fn fold_add(&self, lhs: &str, rhs: &str) -> Option<i64> {
209        self.get(lhs)?.checked_add(self.get(rhs)?)
210    }
211}
212/// An abstract interval element: either `[lo, hi]` or ⊥ (empty).
213#[derive(Debug, Clone, PartialEq, Eq)]
214pub enum Interval {
215    Bottom,
216    Range(i64, i64),
217}
218impl Interval {
219    /// Bottom element ⊥.
220    pub fn bot() -> Self {
221        Interval::Bottom
222    }
223    /// Top element ⊤ = [-∞, +∞] (represented with i64 extremes).
224    pub fn top() -> Self {
225        Interval::Range(i64::MIN, i64::MAX)
226    }
227    /// A single value.
228    pub fn single(v: i64) -> Self {
229        Interval::Range(v, v)
230    }
231    /// Partial order: `self ⊑ other`.
232    pub fn leq(&self, other: &Self) -> bool {
233        match (self, other) {
234            (Interval::Bottom, _) => true,
235            (_, Interval::Bottom) => false,
236            (Interval::Range(a, b), Interval::Range(c, d)) => *a >= *c && *b <= *d,
237        }
238    }
239    /// Join operator ⊔.
240    pub fn join(&self, other: &Self) -> Self {
241        match (self, other) {
242            (Interval::Bottom, x) | (x, Interval::Bottom) => x.clone(),
243            (Interval::Range(a, b), Interval::Range(c, d)) => {
244                Interval::Range((*a).min(*c), (*b).max(*d))
245            }
246        }
247    }
248    /// Meet operator ⊓.
249    pub fn meet(&self, other: &Self) -> Self {
250        match (self, other) {
251            (Interval::Bottom, _) | (_, Interval::Bottom) => Interval::Bottom,
252            (Interval::Range(a, b), Interval::Range(c, d)) => {
253                let lo = (*a).max(*c);
254                let hi = (*b).min(*d);
255                if lo > hi {
256                    Interval::Bottom
257                } else {
258                    Interval::Range(lo, hi)
259                }
260            }
261        }
262    }
263    /// Widening operator â–½.
264    pub fn widen(&self, other: &Self) -> Self {
265        match (self, other) {
266            (Interval::Bottom, x) => x.clone(),
267            (x, Interval::Bottom) => x.clone(),
268            (Interval::Range(a, b), Interval::Range(c, d)) => {
269                let lo = if *c < *a { i64::MIN } else { *a };
270                let hi = if *d > *b { i64::MAX } else { *b };
271                Interval::Range(lo, hi)
272            }
273        }
274    }
275    /// Narrowing operator â–³.
276    pub fn narrow(&self, other: &Self) -> Self {
277        match (self, other) {
278            (Interval::Bottom, _) => Interval::Bottom,
279            (x, Interval::Bottom) => x.clone(),
280            (Interval::Range(a, b), Interval::Range(c, d)) => {
281                let lo = if *a == i64::MIN { *c } else { *a };
282                let hi = if *b == i64::MAX { *d } else { *b };
283                if lo > hi {
284                    Interval::Bottom
285                } else {
286                    Interval::Range(lo, hi)
287                }
288            }
289        }
290    }
291    /// Arithmetic add abstraction.
292    pub fn add(&self, other: &Self) -> Self {
293        match (self, other) {
294            (Interval::Bottom, _) | (_, Interval::Bottom) => Interval::Bottom,
295            (Interval::Range(a, b), Interval::Range(c, d)) => {
296                Interval::Range(a.saturating_add(*c), b.saturating_add(*d))
297            }
298        }
299    }
300    /// Contains a concrete value.
301    pub fn contains(&self, v: i64) -> bool {
302        match self {
303            Interval::Bottom => false,
304            Interval::Range(lo, hi) => *lo <= v && v <= *hi,
305        }
306    }
307}
308/// A simple variable-level taint tracking state.
309#[derive(Debug, Clone, Default)]
310pub struct TaintState {
311    /// Tainted variables.
312    pub tainted: HashSet<String>,
313    /// Sanitized variables (explicitly cleaned).
314    pub sanitized: HashSet<String>,
315}
316impl TaintState {
317    pub fn new() -> Self {
318        Self::default()
319    }
320    /// Mark a variable as a taint source.
321    pub fn add_source(&mut self, var: impl Into<String>) {
322        let v = var.into();
323        self.sanitized.remove(&v);
324        self.tainted.insert(v);
325    }
326    /// Mark a variable as sanitized.
327    pub fn sanitize(&mut self, var: &str) {
328        self.tainted.remove(var);
329        self.sanitized.insert(var.to_string());
330    }
331    /// Propagate taint: `dst` is tainted if any of `srcs` is tainted.
332    pub fn propagate(&mut self, dst: impl Into<String>, srcs: &[&str]) {
333        let dst = dst.into();
334        let tainted = srcs.iter().any(|&s| self.tainted.contains(s));
335        if tainted {
336            self.sanitized.remove(&dst);
337            self.tainted.insert(dst);
338        } else {
339            self.tainted.remove(&dst);
340        }
341    }
342    /// Check for a taint violation: `var` is tainted and reaches a sink.
343    pub fn violates(&self, var: &str) -> bool {
344        self.tainted.contains(var) && !self.sanitized.contains(var)
345    }
346    /// Join two taint states (union of tainted sets).
347    pub fn join(&self, other: &TaintState) -> TaintState {
348        TaintState {
349            tainted: self.tainted.union(&other.tainted).cloned().collect(),
350            sanitized: self
351                .sanitized
352                .intersection(&other.sanitized)
353                .cloned()
354                .collect(),
355        }
356    }
357}
358/// Represents a finite-state automaton for resource protocol checking.
359/// States are `usize` indices; transitions are labeled by operation names.
360#[allow(dead_code)]
361#[derive(Debug, Clone)]
362pub struct TypestateAutomaton {
363    /// Number of states.
364    pub num_states: usize,
365    /// Initial state.
366    pub initial: usize,
367    /// Accepting (final) states.
368    pub accepting: BTreeSet<usize>,
369    /// Transition table: transitions[state][op_name] = next_state.
370    pub transitions: Vec<std::collections::BTreeMap<String, usize>>,
371    /// Error states (invalid transitions recorded here).
372    pub error_states: BTreeSet<usize>,
373}
374impl TypestateAutomaton {
375    /// Construct an automaton with `n` states.
376    pub fn new(num_states: usize, initial: usize) -> Self {
377        Self {
378            num_states,
379            initial,
380            accepting: BTreeSet::new(),
381            transitions: vec![std::collections::BTreeMap::new(); num_states],
382            error_states: BTreeSet::new(),
383        }
384    }
385    /// Add a transition: from `from` via `op` to `to`.
386    pub fn add_transition(&mut self, from: usize, op: &str, to: usize) {
387        self.transitions[from].insert(op.to_string(), to);
388    }
389    /// Mark a state as accepting.
390    pub fn set_accepting(&mut self, state: usize) {
391        self.accepting.insert(state);
392    }
393    /// Simulate an operation sequence; return the final state or `None` on invalid transition.
394    pub fn simulate(&self, ops: &[&str]) -> Option<usize> {
395        let mut state = self.initial;
396        for &op in ops {
397            match self.transitions[state].get(op) {
398                Some(&next) => state = next,
399                None => return None,
400            }
401        }
402        Some(state)
403    }
404    /// Check whether an operation sequence is accepted (ends in accepting state).
405    pub fn accepts(&self, ops: &[&str]) -> bool {
406        self.simulate(ops)
407            .map_or(false, |s| self.accepting.contains(&s))
408    }
409    /// Check whether an operation sequence violates the protocol.
410    pub fn violates(&self, ops: &[&str]) -> bool {
411        self.simulate(ops).is_none()
412    }
413}
414/// A simplified Andersen points-to analysis using a constraint worklist.
415#[derive(Debug, Clone, Default)]
416pub struct AndersenPTA {
417    /// Number of variables.
418    pub num_vars: usize,
419    /// Points-to sets: pts[v] = set of allocation sites.
420    pub pts: Vec<BTreeSet<usize>>,
421    /// Copy constraints: copy_edges[a] = {b | pts(a) ⊆ pts(b)}.
422    pub copy_edges: Vec<BTreeSet<usize>>,
423    /// Store constraints: store[a] = set of (src, field).
424    pub store: Vec<Vec<(usize, usize)>>,
425    /// Load constraints: load[a] = set of (dst, field).
426    pub load: Vec<Vec<(usize, usize)>>,
427}
428impl AndersenPTA {
429    pub fn new(num_vars: usize) -> Self {
430        Self {
431            num_vars,
432            pts: vec![BTreeSet::new(); num_vars],
433            copy_edges: vec![BTreeSet::new(); num_vars],
434            store: vec![vec![]; num_vars],
435            load: vec![vec![]; num_vars],
436        }
437    }
438    /// Add: `a = alloc()` — variable `a` points to allocation site `site`.
439    pub fn add_alloc(&mut self, a: usize, site: usize) {
440        self.pts[a].insert(site);
441    }
442    /// Add copy constraint: `b = a` (pts(a) ⊆ pts(b)).
443    pub fn add_copy(&mut self, src: usize, dst: usize) {
444        self.copy_edges[src].insert(dst);
445    }
446    /// Solve: propagate points-to sets to a fixpoint.
447    pub fn solve(&mut self) {
448        let mut worklist: VecDeque<usize> = (0..self.num_vars).collect();
449        while let Some(v) = worklist.pop_front() {
450            let pts_v: Vec<usize> = self.pts[v].iter().copied().collect();
451            for &dst in &self.copy_edges[v].clone() {
452                let added: Vec<usize> = pts_v
453                    .iter()
454                    .filter(|&&s| self.pts[dst].insert(s))
455                    .copied()
456                    .collect();
457                if !added.is_empty() {
458                    worklist.push_back(dst);
459                }
460            }
461        }
462    }
463    /// Query: may `a` and `b` alias?
464    pub fn may_alias(&self, a: usize, b: usize) -> bool {
465        !self.pts[a].is_disjoint(&self.pts[b])
466    }
467}
468/// A simplified program dependence graph over statement indices.
469#[allow(dead_code)]
470#[derive(Debug, Clone, Default)]
471pub struct PDGraph {
472    /// Number of statements.
473    pub num_stmts: usize,
474    /// Data dependence edges: data_edges[s] = set of statements s flows data to.
475    pub data_edges: Vec<BTreeSet<usize>>,
476    /// Control dependence edges: ctrl_edges[s] = statements s controls.
477    pub ctrl_edges: Vec<BTreeSet<usize>>,
478}
479impl PDGraph {
480    /// Create a PDG for `n` statements.
481    pub fn new(num_stmts: usize) -> Self {
482        Self {
483            num_stmts,
484            data_edges: vec![BTreeSet::new(); num_stmts],
485            ctrl_edges: vec![BTreeSet::new(); num_stmts],
486        }
487    }
488    /// Add a data dependence edge from `src` to `dst`.
489    pub fn add_data_edge(&mut self, src: usize, dst: usize) {
490        self.data_edges[src].insert(dst);
491    }
492    /// Add a control dependence edge from `src` to `dst`.
493    pub fn add_ctrl_edge(&mut self, src: usize, dst: usize) {
494        self.ctrl_edges[src].insert(dst);
495    }
496    /// Compute backward slice from a criterion statement.
497    /// Returns the set of statement indices that can affect `criterion`.
498    pub fn backward_slice(&self, criterion: usize) -> BTreeSet<usize> {
499        let mut slice = BTreeSet::new();
500        let mut worklist: VecDeque<usize> = VecDeque::new();
501        worklist.push_back(criterion);
502        while let Some(s) = worklist.pop_front() {
503            if slice.insert(s) {
504                for src in 0..self.num_stmts {
505                    if self.data_edges[src].contains(&s) || self.ctrl_edges[src].contains(&s) {
506                        if !slice.contains(&src) {
507                            worklist.push_back(src);
508                        }
509                    }
510                }
511            }
512        }
513        slice
514    }
515    /// Compute forward slice from a criterion statement.
516    pub fn forward_slice(&self, criterion: usize) -> BTreeSet<usize> {
517        let mut slice = BTreeSet::new();
518        let mut worklist: VecDeque<usize> = VecDeque::new();
519        worklist.push_back(criterion);
520        while let Some(s) = worklist.pop_front() {
521            if slice.insert(s) {
522                for &dst in &self.data_edges[s] {
523                    if !slice.contains(&dst) {
524                        worklist.push_back(dst);
525                    }
526                }
527                for &dst in &self.ctrl_edges[s] {
528                    if !slice.contains(&dst) {
529                        worklist.push_back(dst);
530                    }
531                }
532            }
533        }
534        slice
535    }
536}
537/// Three-valued nullability: definitely null, definitely non-null, or unknown.
538#[allow(dead_code)]
539#[derive(Debug, Clone, PartialEq, Eq)]
540pub enum Nullability {
541    /// Definitely null.
542    Null,
543    /// Definitely non-null.
544    NonNull,
545    /// Unknown / may be null.
546    MaybeNull,
547}
548/// Tracks nullability for program variables.
549#[allow(dead_code)]
550#[derive(Debug, Clone, Default)]
551pub struct NullTracker {
552    /// Nullability status per variable.
553    pub status: std::collections::HashMap<String, Nullability>,
554    /// Variables that caused a null dereference alarm.
555    pub alarms: Vec<String>,
556}
557impl NullTracker {
558    /// Create a new null tracker.
559    pub fn new() -> Self {
560        Self::default()
561    }
562    /// Declare a variable as definitely non-null (e.g. just allocated).
563    pub fn declare_non_null(&mut self, var: impl Into<String>) {
564        self.status.insert(var.into(), Nullability::NonNull);
565    }
566    /// Declare a variable as potentially null (e.g. result of nullable function).
567    pub fn declare_maybe_null(&mut self, var: impl Into<String>) {
568        self.status.insert(var.into(), Nullability::MaybeNull);
569    }
570    /// Declare a variable as definitely null.
571    pub fn declare_null(&mut self, var: impl Into<String>) {
572        self.status.insert(var.into(), Nullability::Null);
573    }
574    /// Get the nullability of a variable (defaults to MaybeNull if unknown).
575    pub fn get(&self, var: &str) -> &Nullability {
576        self.status.get(var).unwrap_or(&Nullability::MaybeNull)
577    }
578    /// Simulate a dereference: raises an alarm if var may be null.
579    pub fn dereference(&mut self, var: &str) {
580        match self.get(var) {
581            Nullability::Null | Nullability::MaybeNull => self.alarms.push(var.to_string()),
582            Nullability::NonNull => {}
583        }
584    }
585    /// Join two null-tracker states at a merge point.
586    pub fn join(&self, other: &NullTracker) -> NullTracker {
587        let mut result = NullTracker::new();
588        for (var, lhs) in &self.status {
589            let rhs = other.get(var);
590            let merged = match (lhs, rhs) {
591                (Nullability::NonNull, Nullability::NonNull) => Nullability::NonNull,
592                (Nullability::Null, Nullability::Null) => Nullability::Null,
593                _ => Nullability::MaybeNull,
594            };
595            result.status.insert(var.clone(), merged);
596        }
597        for var in other.status.keys() {
598            if !result.status.contains_key(var) {
599                result.status.insert(var.clone(), Nullability::MaybeNull);
600            }
601        }
602        result
603    }
604    /// Returns true if any null-dereference alarm was raised.
605    pub fn has_alarm(&self) -> bool {
606        !self.alarms.is_empty()
607    }
608}
609/// Abstract sign: {⊥, Neg, Zero, Pos, ⊤}.
610#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
611pub enum Sign {
612    Bottom,
613    Neg,
614    Zero,
615    Pos,
616    Top,
617}
618impl Sign {
619    pub fn of(v: i64) -> Self {
620        if v < 0 {
621            Sign::Neg
622        } else if v == 0 {
623            Sign::Zero
624        } else {
625            Sign::Pos
626        }
627    }
628    pub fn join(&self, other: &Self) -> Self {
629        if self == other {
630            return self.clone();
631        }
632        match (self, other) {
633            (Sign::Bottom, x) | (x, Sign::Bottom) => x.clone(),
634            _ => Sign::Top,
635        }
636    }
637    pub fn leq(&self, other: &Self) -> bool {
638        self == &Sign::Bottom || other == &Sign::Top || self == other
639    }
640    pub fn add(&self, other: &Self) -> Self {
641        match (self, other) {
642            (Sign::Bottom, _) | (_, Sign::Bottom) => Sign::Bottom,
643            (Sign::Zero, x) | (x, Sign::Zero) => x.clone(),
644            (Sign::Pos, Sign::Pos) => Sign::Pos,
645            (Sign::Neg, Sign::Neg) => Sign::Neg,
646            _ => Sign::Top,
647        }
648    }
649    pub fn neg(&self) -> Self {
650        match self {
651            Sign::Pos => Sign::Neg,
652            Sign::Neg => Sign::Pos,
653            x => x.clone(),
654        }
655    }
656}