Struct aquascope::analysis::permissions::PermissionsCtxt

pub struct PermissionsCtxt<'a, 'tcx> {
    pub tcx: TyCtxt<'tcx>,
    pub polonius_input_facts: &'a AllFacts<RustcFacts>,
    pub polonius_output: Output<RustcFacts>,
    pub permissions_output: Output<AquascopeFacts>,
    pub body_id: BodyId,
    pub def_id: DefId,
    pub body_with_facts: &'a BodyWithBorrowckFacts<'tcx>,
    pub borrow_set: BorrowSet<'tcx>,
    pub move_data: MoveData<'tcx>,
    pub loan_regions: Option<FxHashMap<Loan, (Point, Point)>>,
    pub locals_are_invalidated_at_exit: bool,
    /* private fields */
}

Fields

tcx: TyCtxt<'tcx>

polonius_input_facts: &'a AllFacts<RustcFacts>

polonius_output: Output<RustcFacts>

permissions_output: Output<AquascopeFacts>

Program facts unique to Aquascope.

These are generated by the Output builder and overlap quite a bit with the [rustc_borrowck::consumers::RustcFacts], however, unlike rustc we maintain data about all Places in a body (plus some other things). Conversion functions between the two sets of facts are provided by the PermissionsCtxt.

body_id: BodyId

def_id: DefId

body_with_facts: &'a BodyWithBorrowckFacts<'tcx>

borrow_set: BorrowSet<'tcx>

move_data: MoveData<'tcx>

loan_regions: Option<FxHashMap<Loan, (Point, Point)>>

locals_are_invalidated_at_exit: bool

Implementations

impl<'a, 'tcx> PermissionsCtxt<'a, 'tcx>

pub fn new_path(&mut self, place: Place<'tcx>) -> Path

pub fn region_flows(&self) -> &RegionFlows

pub fn place_to_path(&self, p: &Place<'tcx>) -> Path

Convert and normalize a rustc Place into a Path understood by Aquascope.

pub fn path_to_place(&self, p: Path) -> Place<'tcx>

pub fn location_to_point(&self, l: Location) -> Point

pub fn location_to_points(&self, l: Location) -> SmallVec<[Point; 2]>

pub fn point_to_location(&self, p: Point) -> Location

pub fn path_to_moveable_path(&self, p: Path) -> <RustcFacts as FactTypes>::Path

pub fn moveable_path_to_path(&self, mp: <RustcFacts as FactTypes>::Path) -> Path

pub fn path_to_variable(&self, path: Path) -> Variable

pub fn location_to_span(&self, l: Location) -> Span

pub fn move_to_moveable_path(&self, mv: Move) -> <RustcFacts as FactTypes>::Path

pub fn move_to_path(&self, mv: Move) -> Path

pub fn loan_to_borrow(&self, l: Loan) -> &BorrowData<'tcx>

pub fn is_universal_subset(&self, (from, to): (Origin, Origin)) -> bool

pub fn is_location_operational(&self, loc: Location) -> bool

pub fn is_point_operational(&self, point: Point) -> bool

pub fn is_mutable_borrow(&self, brw: &BorrowData<'tcx>) -> bool

pub fn is_mutable_loan(&self, loan: Loan) -> bool

pub fn is_declared_readonly(&self, place: &Place<'tcx>) -> bool

pub fn is_path_live_at(&self, path: Path, point: Point) -> bool

pub fn is_path_copyable(&self, path: Path) -> bool

On use would the given path be copied?

pub fn is_path_write_enabled(&self, path: Path) -> bool

Can this path be written to?

pub fn is_path_drop_enabled(&self, path: Path) -> bool

Does a Path’s type allow it to be dropped? NOTE: the utility is the negation of the datalog rule.

.decl never_drop(Path)

never_drop(Path) :- !is_direct(Path), !is_index(Path), has_adt_prefix_with_dtor(Path).

This logic follows from Rust’s [MoveData::gather_moves] builder, the core logic is found here: https://doc.rust-lang.org/nightly/nightly-rustc/src/rustc_mir_dataflow/move_paths/builder.rs.html#100

pub fn max_permissions(&self, path: Path) -> Permissions

The maximum set of permissions a given Path could have at any point.

pub fn permissions_for_const_ty(&self, ty: Ty<'tcx>) -> PermissionsData

pub fn permissions_data_at_point( &self, path: Path, point: Point ) -> PermissionsData

Compute the PermissionsData for the Path at Point.

The PermissionsData holds destructured permissions info about a Place. This info remains desugared to help with visual marks but the set of existing Permissions is computed. Permissions are given by the following rules:

decl read(Path, Point)
decl write(Path, Point)
decl drop(Path, Point)
decl memory_uninitialized(Path, Point)

memory_uninitialized(Path, Point) :-
  path_moved(Path, Point).
memory_uninitialized(Path, Point) :-
  path_uninitialized(Path, Point).

read(Path, Point) :-
  !memory_uninitialized(Point),
  !loan_read_refined(Path, Point).

write(Path, Point) :-
  path_ty_allows_write(Path),
  read(Path, Point),
  !loan_write_refined(Path, Point).


drop(Path, Point) :-
  path_ty_allows_drop(Path),
  read(Path, Point),
  !loan_drop_refined(Path, Point).

Queries not defined in the

pub fn domain_places(&self) -> HashSet<Place<'tcx>>

pub fn domain_bottom(&self) -> PermissionsDomain<'tcx>

pub fn permissions_domain_at_point( &self, point: Point ) -> PermissionsDomain<'tcx>