rapx/analysis/senryx/contracts/
abstract_state.rs

1use std::{
2    collections::{HashMap, HashSet},
3    hash::Hash,
4};
5
6use crate::analysis::senryx::visitor::PlaceTy;
7
8use super::state_lattice::Lattice;
9
10#[derive(Debug, PartialEq, PartialOrd, Copy, Clone)]
11pub enum Value {
12    Usize(usize),
13    Isize(isize),
14    U32(u32),
15    Custom(),
16    None,
17    // ...
18}
19
20#[derive(Debug, PartialEq, Eq, Clone, Hash)]
21pub enum StateType<'tcx> {
22    AllocatedState(AllocatedState),
23    AlignState(AlignState<'tcx>),
24    // ...
25}
26
27#[derive(Debug, PartialEq, Copy, Clone)]
28pub enum Op {
29    EQ,
30    NE,
31    LT,
32    GT,
33    LE,
34    GE,
35}
36
37#[derive(Debug, PartialEq, Eq, Hash, Copy, Clone)]
38pub enum AllocatedState {
39    Top,
40    Borrowed,
41    Moved,
42    Alloc,
43    SpecificAlloc,
44    Bottom,
45}
46
47#[derive(Debug, PartialEq, Eq, Clone, Hash)]
48pub enum AlignState<'tcx> {
49    Aligned,
50    Cast(PlaceTy<'tcx>, PlaceTy<'tcx>),
51    Unaligned,
52}
53
54#[derive(Debug, PartialEq, Eq, Hash, Copy, Clone)]
55pub enum InitState {
56    FullyInitialized,
57    PartlyInitialized,
58}
59
60#[derive(Debug, PartialEq, Eq, Hash, Clone)]
61pub enum VType<'tcx> {
62    Pointer(PlaceTy<'tcx>),
63    None,
64    // todo
65}
66
67#[derive(Debug, Clone, PartialEq)]
68pub struct AbstractStateItem<'tcx> {
69    pub value: (Value, Value),
70    pub vtype: VType<'tcx>,
71    pub state: HashSet<StateType<'tcx>>,
72}
73
74impl<'tcx> AbstractStateItem<'tcx> {
75    pub fn new(value: (Value, Value), vtype: VType<'tcx>, state: HashSet<StateType<'tcx>>) -> Self {
76        Self {
77            value,
78            vtype,
79            state,
80        }
81    }
82
83    pub fn new_default() -> Self {
84        Self {
85            value: (Value::None, Value::None),
86            vtype: VType::None,
87            state: HashSet::new(),
88        }
89    }
90
91    pub fn meet_state_item(&mut self, other_state: &AbstractStateItem<'tcx>) {
92        let mut new_state: HashSet<StateType<'tcx>> = HashSet::new();
93
94        // visit 'self.state' and 'other_state.state'，matching states and calling meet method
95        for state_self in &self.state {
96            // if find the same state type in 'other_state', then meet it;
97            if let Some(matching_state) = other_state.state.iter().find(|state_other| {
98                std::mem::discriminant(*state_other) == std::mem::discriminant(state_self)
99            }) {
100                let merged_state = match (state_self, matching_state) {
101                    (StateType::AllocatedState(s1), StateType::AllocatedState(s2)) => {
102                        StateType::AllocatedState(s1.meet(*s2))
103                    }
104                    (StateType::AlignState(s1), StateType::AlignState(s2)) => {
105                        StateType::AlignState(s1.meet(s2.clone()))
106                    }
107                    _ => continue,
108                };
109                new_state.insert(merged_state);
110            } else {
111                // if 'other_state' does not have the same state，then reserve the current state
112                new_state.insert(state_self.clone());
113            }
114        }
115
116        // 更新 self 的状态
117        self.state = new_state;
118    }
119}
120
121#[derive(PartialEq)]
122pub struct PathInfo<'tcx> {
123    pub state_map: HashMap<usize, AbstractStateItem<'tcx>>,
124}
125
126impl<'tcx> PathInfo<'tcx> {
127    pub fn new() -> Self {
128        Self {
129            state_map: HashMap::new(),
130        }
131    }
132
133    pub fn insert_abstate(&mut self, place: usize, place_state_item: AbstractStateItem<'tcx>) {
134        self.state_map.insert(place, place_state_item);
135    }
136}
rapx/analysis/senryx/contracts/abstract_state.rs

rapx/analysis/senryx/contracts/
abstract_state.rs
