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

rapx/analysis/senryx/contracts/
property.rs
