rapx/analysis/senryx/contracts/
state_lattice.rs

1//use crate::rap_info;
2use super::abstract_state::*;
3
4pub trait Lattice {
5    fn join(&self, other: Self) -> Self;
6    fn meet(&self, other: Self) -> Self;
7    fn less_than(&self, other: Self) -> bool;
8    fn equal(&self, other: Self) -> bool;
9    fn check(&self) -> bool;
10}
11
12impl<'tcx> Lattice for StateType<'tcx> {
13    fn join(&self, other: Self) -> Self {
14        match &self {
15            &StateType::AllocatedState(a) => match other {
16                StateType::AllocatedState(b) => StateType::AllocatedState(a.join(b)),
17                _ => panic!("Incompatible types"),
18            },
19            &StateType::AlignState(a) => match other {
20                StateType::AlignState(b) => StateType::AlignState(a.join(b)),
21                _ => panic!("Incompatible types"),
22            },
23        }
24    }
25
26    fn meet(&self, other: Self) -> Self {
27        match &self {
28            &StateType::AllocatedState(a) => match other {
29                StateType::AllocatedState(b) => StateType::AllocatedState(a.meet(b)),
30                _ => panic!("Incompatible types"),
31            },
32            &StateType::AlignState(a) => match other {
33                StateType::AlignState(b) => StateType::AlignState(a.meet(b)),
34                _ => panic!("Incompatible types"),
35            },
36        }
37    }
38
39    fn less_than(&self, other: Self) -> bool {
40        match &self {
41            &StateType::AllocatedState(a) => match other {
42                StateType::AllocatedState(b) => a.less_than(b),
43                _ => panic!("Incompatible types"),
44            },
45            &StateType::AlignState(a) => match other {
46                StateType::AlignState(b) => a.less_than(b),
47                _ => panic!("Incompatible types"),
48            },
49        }
50    }
51
52    fn equal(&self, other: Self) -> bool {
53        match &self {
54            &StateType::AllocatedState(a) => match other {
55                StateType::AllocatedState(b) => a.equal(b),
56                _ => panic!("Incompatible types"),
57            },
58            &StateType::AlignState(a) => match other {
59                StateType::AlignState(b) => a.equal(b),
60                _ => panic!("Incompatible types"),
61            },
62        }
63    }
64
65    fn check(&self) -> bool {
66        match &self {
67            &StateType::AllocatedState(a) => a.check(),
68            &StateType::AlignState(a) => a.check(),
69        }
70    }
71}
72
73impl Lattice for AllocatedState {
74    fn join(&self, other: Self) -> Self {
75        match (*self, other) {
76            (AllocatedState::Bottom, _) => other,
77            (_, AllocatedState::Bottom) => *self,
78            (AllocatedState::Top, _) | (_, AllocatedState::Top) => AllocatedState::Top,
79            (AllocatedState::Borrowed, AllocatedState::Moved)
80            | (AllocatedState::Moved, AllocatedState::Borrowed) => AllocatedState::Top,
81            (AllocatedState::Alloc, AllocatedState::SpecificAlloc)
82            | (AllocatedState::SpecificAlloc, AllocatedState::Alloc) => {
83                AllocatedState::SpecificAlloc
84            }
85            (state1, state2) if state1 == state2 => state1,
86            (AllocatedState::Alloc, AllocatedState::Borrowed)
87            | (AllocatedState::Borrowed, AllocatedState::Alloc) => AllocatedState::Borrowed,
88            (AllocatedState::Alloc, AllocatedState::Moved)
89            | (AllocatedState::Moved, AllocatedState::Alloc) => AllocatedState::Moved,
90            (AllocatedState::SpecificAlloc, AllocatedState::Borrowed)
91            | (AllocatedState::Borrowed, AllocatedState::SpecificAlloc) => AllocatedState::Borrowed,
92            (AllocatedState::Moved, AllocatedState::SpecificAlloc)
93            | (AllocatedState::SpecificAlloc, AllocatedState::Moved) => AllocatedState::Moved,
94            _ => AllocatedState::Top,
95        }
96    }
97
98    fn meet(&self, other: Self) -> Self {
99        match (*self, other) {
100            (AllocatedState::Top, _) => other,
101            (_, AllocatedState::Top) => *self,
102            (AllocatedState::Bottom, _) | (_, AllocatedState::Bottom) => AllocatedState::Bottom,
103            (AllocatedState::Borrowed, AllocatedState::Moved)
104            | (AllocatedState::Moved, AllocatedState::Borrowed) => AllocatedState::Bottom,
105            (AllocatedState::Alloc, AllocatedState::SpecificAlloc)
106            | (AllocatedState::SpecificAlloc, AllocatedState::Alloc) => AllocatedState::Alloc,
107            (state1, state2) if state1 == state2 => state1,
108            (AllocatedState::Alloc, AllocatedState::Borrowed)
109            | (AllocatedState::Borrowed, AllocatedState::Alloc) => AllocatedState::Alloc,
110            (AllocatedState::SpecificAlloc, AllocatedState::Borrowed)
111            | (AllocatedState::Borrowed, AllocatedState::SpecificAlloc) => {
112                AllocatedState::SpecificAlloc
113            }
114            (AllocatedState::Moved, AllocatedState::SpecificAlloc)
115            | (AllocatedState::SpecificAlloc, AllocatedState::Moved) => {
116                AllocatedState::SpecificAlloc
117            }
118            _ => AllocatedState::Bottom,
119        }
120    }
121
122    fn less_than(&self, other: Self) -> bool {
123        match (*self, other) {
124            (AllocatedState::Bottom, _) | (_, AllocatedState::Top) => true,
125            (AllocatedState::Alloc, AllocatedState::Borrowed) => true,
126            (AllocatedState::Alloc, AllocatedState::SpecificAlloc) => true,
127            (AllocatedState::Alloc, AllocatedState::Moved) => true,
128            (AllocatedState::SpecificAlloc, AllocatedState::Borrowed) => true,
129            (AllocatedState::SpecificAlloc, AllocatedState::Moved) => true,
130            _ => false,
131        }
132    }
133
134    fn equal(&self, other: Self) -> bool {
135        *self == other
136    }
137
138    fn check(&self) -> bool {
139        true
140    }
141}
142
143impl<'tcx> Lattice for AlignState<'tcx> {
144    fn join(&self, other: Self) -> Self {
145        match (self, other.clone()) {
146            (AlignState::Aligned, _) => AlignState::Aligned,
147            (AlignState::Cast(_, _), AlignState::Cast(_, _)) => AlignState::Unaligned,
148            (AlignState::Unaligned, _) => AlignState::Unaligned,
149            (_, AlignState::Unaligned) => AlignState::Unaligned,
150            _ => other.clone(),
151        }
152    }
153
154    fn meet(&self, other: Self) -> Self {
155        other
156        // match (self, other) {
157        //     (AlignState::Aligned, _) => other,
158        //     (AlignState::Big2SmallCast(_,_), AlignState::Big2SmallCast(_,_)) => AlignState::Aligned,
159        //     (AlignState::Big2SmallCast(_,_), AlignState::Small2BigCast(_,_)) => AlignState::Unaligned,
160        //     (AlignState::Big2SmallCast(_,_), AlignState::Aligned) => AlignState::Big2SmallCast(_,_),
161        //     (AlignState::Small2BigCast, _) => AlignState::Small2BigCast,
162        // }
163    }
164
165    fn less_than(&self, other: Self) -> bool {
166        match (self, other) {
167            (_, AlignState::Aligned) => true,
168            (AlignState::Cast(_, _), AlignState::Cast(_, _)) => true,
169            _ => false,
170        }
171    }
172
173    fn equal(&self, other: Self) -> bool {
174        *self == other
175    }
176
177    fn check(&self) -> bool {
178        match self {
179            AlignState::Aligned => true,
180            AlignState::Unaligned => false,
181            AlignState::Cast(src, dest) => {
182                // rap_info!("src ty {:?}, dst ty {:?}",src, dest);
183                let src_aligns = src.possible_aligns();
184                let dest_aligns = dest.possible_aligns();
185                if dest_aligns.len() == 0 && src != dest {
186                    // dst ty could be arbitrary type && src and dst are different types
187                    return false;
188                }
189
190                for &d_align in &dest_aligns {
191                    if d_align != 1 && src_aligns.len() == 0 {
192                        // src ty could be arbitrary type
193                        return false;
194                    }
195                    for &s_align in &src_aligns {
196                        if s_align < d_align {
197                            return false;
198                        }
199                    }
200                }
201                true
202            }
203        }
204    }
205}
206
207impl Lattice for InitState {
208    fn join(&self, other: Self) -> Self {
209        match (self, other) {
210            (InitState::FullyInitialized, _) => InitState::FullyInitialized,
211            (_, InitState::FullyInitialized) => InitState::FullyInitialized,
212            _ => InitState::PartlyInitialized,
213        }
214    }
215
216    fn meet(&self, other: Self) -> Self {
217        match (self, other) {
218            (InitState::FullyInitialized, _) => other,
219            (_, InitState::FullyInitialized) => *self,
220            _ => InitState::PartlyInitialized,
221        }
222    }
223
224    fn less_than(&self, other: Self) -> bool {
225        match (self, other) {
226            (InitState::FullyInitialized, InitState::FullyInitialized) => true,
227            (InitState::PartlyInitialized, _) => true,
228            _ => false,
229        }
230    }
231
232    fn equal(&self, other: Self) -> bool {
233        *self == other
234    }
235
236    fn check(&self) -> bool {
237        true
238    }
239}
rapx/analysis/senryx/contracts/state_lattice.rs

rapx/analysis/senryx/contracts/
state_lattice.rs
