rapx/check/rcanary/ranalyzer/
ownership.rs

1use std::{collections::HashSet, fmt::Debug};
2use z3::ast;
3
4use rustc_middle::ty::Ty;
5
6use crate::analysis::heap_ownership::default::TyWithIndex;
7
8#[derive(Clone, Debug)]
9pub struct Taint<'tcx> {
10    set: HashSet<TyWithIndex<'tcx>>,
11}
12
13impl<'tcx> Default for Taint<'tcx> {
14    fn default() -> Self {
15        Self {
16            set: HashSet::default(),
17        }
18    }
19}
20
21impl<'tcx> Taint<'tcx> {
22    pub fn is_untainted(&self) -> bool {
23        self.set.is_empty()
24    }
25
26    pub fn is_tainted(&self) -> bool {
27        !self.set.is_empty()
28    }
29
30    pub fn contains(&self, k: &TyWithIndex<'tcx>) -> bool {
31        self.set.contains(k)
32    }
33
34    pub fn insert(&mut self, k: TyWithIndex<'tcx>) {
35        self.set.insert(k);
36    }
37
38    pub fn set(&self) -> &HashSet<TyWithIndex<'tcx>> {
39        &self.set
40    }
41}
42
43#[derive(Clone, Debug, Eq, PartialEq, Hash)]
44pub enum IntraVar<'z3> {
45    Declared,
46    Init(ast::BV<'z3>),
47    Unsupported,
48}
49
50impl<'z3> Default for IntraVar<'z3> {
51    fn default() -> Self {
52        Self::Declared
53    }
54}
55
56impl<'z3> IntraVar<'z3> {
57    pub fn is_declared(&self) -> bool {
58        matches!(self, IntraVar::Declared)
59    }
60
61    pub fn is_init(&self) -> bool {
62        matches!(self, IntraVar::Init(_))
63    }
64
65    pub fn is_unsupported(&self) -> bool {
66        matches!(self, IntraVar::Unsupported)
67    }
68
69    pub fn extract(&self) -> ast::BV<'z3> {
70        match self {
71            IntraVar::Init(ast) => ast.clone(),
72            _ => unreachable!(),
73        }
74    }
75}
76
77#[derive(Copy, Clone, Debug, Eq, PartialEq, Hash)]
78pub enum ContextTypeOwner<'tcx> {
79    Owned { kind: OwnerKind, ty: Ty<'tcx> },
80    Unowned,
81}
82
83#[derive(Copy, Clone, Debug, Eq, PartialEq, Hash)]
84pub enum OwnerKind {
85    Instance,
86    Reference,
87    Pointer,
88}
89
90impl<'tcx> Default for ContextTypeOwner<'tcx> {
91    fn default() -> Self {
92        Self::Unowned
93    }
94}
95
96impl<'tcx> ContextTypeOwner<'tcx> {
97    pub fn is_owned(&self) -> bool {
98        match self {
99            ContextTypeOwner::Owned { .. } => true,
100            ContextTypeOwner::Unowned => false,
101        }
102    }
103}
rapx/check/rcanary/ranalyzer/ownership.rs

rapx/check/rcanary/ranalyzer/
ownership.rs
