rapx/analysis/senryx/contracts/
property.rs

1use crate::{
2    analysis::utils::fn_info::{
3        access_ident_recursive, match_ty_with_ident, parse_expr_into_local_and_ty,
4        parse_expr_into_number,
5    },
6    rap_error,
7};
8use rustc_hir::def_id::DefId;
9use rustc_middle::mir::BinOp;
10use rustc_middle::ty::Ty;
11use rustc_middle::ty::TyCtxt;
12use safety_parser::{
13    property_attr::property::{Kind, PropertyName},
14    syn::Expr,
15};
16
17#[derive(Clone, Debug)]
18pub enum CisRangeItem {
19    Var(usize, Vec<usize>),
20    Value(usize),
21    Unknown,
22}
23
24impl CisRangeItem {
25    pub fn get_var_base(&self) -> Option<usize> {
26        match self {
27            Self::Var(base, _) => Some(*base),
28            _ => None,
29        }
30    }
31
32    pub fn new_var(base: usize) -> Self {
33        Self::Var(base, Vec::new())
34    }
35
36    pub fn new_value(value: usize) -> Self {
37        Self::Value(value)
38    }
39
40    pub fn new_unknown() -> Self {
41        Self::Unknown
42    }
43}
44
45#[derive(Clone, Debug)]
46pub struct CisRange {
47    pub bin_op: BinOp,
48    pub range: CisRangeItem,
49}
50
51impl CisRange {
52    pub fn new(bin_op: BinOp, range: CisRangeItem) -> Self {
53        Self { bin_op, range }
54    }
55}
56
57#[derive(Clone, Debug)]
58pub enum PropertyContract<'tcx> {
59    // Align (ty)
60    Align(Ty<'tcx>),
61    Size(Kind),
62    NoPadding,
63    NonNull,
64    // Allocated( ty, length)
65    Allocated(Ty<'tcx>, CisRangeItem),
66    // InBound( ty, length)
67    InBound(Ty<'tcx>, CisRangeItem),
68    NonOverlap,
69    ValidNum(CisRange),
70    ValidString,
71    ValidCStr,
72    // Init( ty, length)
73    Init(Ty<'tcx>, CisRangeItem),
74    Unwrap,
75    Typed(Ty<'tcx>),
76    Owning,
77    Alias,
78    Alive,
79    Pinned,
80    NonVolatile,
81    Opened,
82    Trait,
83    Unreachable,
84    ValidPtr(Ty<'tcx>, CisRangeItem),
85    Deref,
86    Ptr2Ref,
87    Layout,
88    Unknown,
89}
90
91impl<'tcx> PropertyContract<'tcx> {
92    pub fn new(
93        tcx: TyCtxt<'tcx>,
94        def_id: DefId,
95        kind: Kind,
96        name: PropertyName,
97        exprs: &Vec<Expr>,
98    ) -> Self {
99        match name {
100            PropertyName::Align => {
101                Self::check_arg_length(exprs.len(), 2, "Align");
102                let ty = Self::parse_type(tcx, def_id, &exprs[1], "Align");
103                Self::Align(ty)
104            }
105            PropertyName::Size => Self::Size(kind),
106            PropertyName::NoPadding => Self::NoPadding,
107            PropertyName::NonNull => Self::NonNull,
108            PropertyName::Allocated => {
109                Self::check_arg_length(exprs.len(), 3, "Allocated");
110                let ty = Self::parse_type(tcx, def_id, &exprs[1], "Allocated");
111                let length = Self::parse_length(tcx, def_id, &exprs[2], "Allocated");
112                Self::Allocated(ty, length)
113            }
114            PropertyName::InBound => {
115                Self::check_arg_length(exprs.len(), 3, "InBound");
116                let ty = Self::parse_type(tcx, def_id, &exprs[1], "InBound");
117                let length = Self::parse_length(tcx, def_id, &exprs[2], "InBound");
118                Self::InBound(ty, length)
119            }
120            PropertyName::NonOverlap => Self::NonOverlap,
121            PropertyName::ValidNum => {
122                Self::check_arg_length(exprs.len(), 1, "ValidNum");
123                let bin_op = BinOp::Ne;
124                let length = Self::parse_length(tcx, def_id, &exprs[0], "ValidNum");
125                return Self::ValidNum(CisRange::new(bin_op, length));
126            }
127            PropertyName::ValidString => Self::ValidString,
128            PropertyName::ValidCStr => Self::ValidCStr,
129            PropertyName::Init => {
130                Self::check_arg_length(exprs.len(), 3, "Init");
131                let ty = Self::parse_type(tcx, def_id, &exprs[1], "Init");
132                let length = Self::parse_length(tcx, def_id, &exprs[2], "Init");
133                Self::Init(ty, length)
134            }
135            PropertyName::Unwrap => Self::Unwrap,
136            PropertyName::Typed => {
137                Self::check_arg_length(exprs.len(), 2, "Typed");
138                let ty = Self::parse_type(tcx, def_id, &exprs[1], "Typed");
139                Self::Typed(ty)
140            }
141            PropertyName::Owning => Self::Owning,
142            PropertyName::Alias => Self::Alias,
143            PropertyName::Alive => Self::Alive,
144            PropertyName::Pinned => Self::Pinned,
145            PropertyName::NonVolatile => Self::NonVolatile,
146            PropertyName::Opened => Self::Opened,
147            PropertyName::Trait => Self::Trait,
148            PropertyName::Unreachable => Self::Unreachable,
149            PropertyName::ValidPtr => {
150                Self::check_arg_length(exprs.len(), 3, "ValidPtr");
151                let ty = Self::parse_type(tcx, def_id, &exprs[1], "ValidPtr");
152                let length = Self::parse_length(tcx, def_id, &exprs[2], "ValidPtr");
153                Self::ValidPtr(ty, length)
154            }
155            PropertyName::Deref => Self::Deref,
156            PropertyName::Ptr2Ref => Self::Ptr2Ref,
157            PropertyName::Layout => Self::Layout,
158            PropertyName::Unknown => Self::Unknown,
159        }
160    }
161
162    pub fn new_patial_order(p: usize, op: BinOp) -> Self {
163        Self::ValidNum(CisRange::new(op, CisRangeItem::Var(p, Vec::new())))
164    }
165
166    pub fn new_obj_boundary(ty: Ty<'tcx>, len: CisRangeItem) -> Self {
167        Self::InBound(ty, len)
168    }
169
170    // -------- length checker ----------
171    fn check_arg_length(expr_len: usize, required_len: usize, sp: &str) -> bool {
172        if expr_len != required_len {
173            panic!("Wrong args length for {:?} Tag!", sp);
174        }
175        true
176    }
177
178    // -------- type parser ----------
179    fn parse_type(tcx: TyCtxt<'tcx>, def_id: DefId, expr: &Expr, sp: &str) -> Ty<'tcx> {
180        let ty_ident_full = access_ident_recursive(expr);
181        if ty_ident_full.is_none() {
182            rap_error!("Incorrect expression for the type of {:?} Tag!", sp);
183        }
184        let ty_ident = ty_ident_full.unwrap().0;
185        let ty = match_ty_with_ident(tcx, def_id, ty_ident);
186        if ty.is_none() {
187            rap_error!("Cannot get type in {:?} Tag!", sp);
188        }
189        return ty.unwrap();
190    }
191
192    // -------- cis range parser ----------
193    fn parse_length(tcx: TyCtxt<'tcx>, def_id: DefId, expr: &Expr, sp: &str) -> CisRangeItem {
194        if let Some(var_len) = parse_expr_into_local_and_ty(tcx, def_id, expr) {
195            CisRangeItem::Var(var_len.0, var_len.1.iter().map(|(x, _)| *x).collect())
196        } else if parse_expr_into_number(expr).is_some() {
197            CisRangeItem::Value(parse_expr_into_number(expr).unwrap())
198        } else {
199            rap_error!("Range length error in {:?} Tag!", sp);
200            CisRangeItem::Unknown
201        }
202    }
203}
204
205#[derive(Debug, Clone)]
206pub struct ContractualInvariantState<'tcx> {
207    pub contracts: Vec<PropertyContract<'tcx>>,
208}
209
210impl<'tcx> ContractualInvariantState<'tcx> {
211    pub fn new_default() -> Self {
212        Self {
213            contracts: Vec::new(),
214        }
215    }
216
217    pub fn add_contract(&mut self, contract: PropertyContract<'tcx>) {
218        self.contracts.push(contract);
219    }
220
221    pub fn get_contracts_length(&self) -> usize {
222        self.contracts.len()
223    }
224}
rapx/analysis/senryx/contracts/property.rs

rapx/analysis/senryx/contracts/
property.rs
