rapx/analysis/senryx/contracts/
abstract_state.rs1use 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 }
19
20#[derive(Debug, PartialEq, Eq, Clone, Hash)]
21pub enum StateType<'tcx> {
22 AllocatedState(AllocatedState),
23 AlignState(AlignState<'tcx>),
24 }
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 }
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 for state_self in &self.state {
96 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 new_state.insert(state_self.clone());
113 }
114 }
115
116 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}