Struct TypeEnv

pub struct TypeEnv<'a> {
    bindings: PlacesTree,
    local_decls: &'a LocalDecls,
}

Fields

bindings: PlacesTree

local_decls: &'a LocalDecls

Implementations

impl<'a> TypeEnv<'a>

pub fn new( infcx: &mut InferCtxt<'_, '_, '_>, body: &'a Body<'_>, fn_sig: &FnSig, check_overflow: bool, ) -> TypeEnv<'a>

pub fn empty() -> TypeEnv<'a>

fn alloc_with_ty(&mut self, local: Local, ty: Ty)

fn alloc(&mut self, local: Local)

pub(crate) fn into_infer( self, scope: Scope, ) -> Result<BasicBlockEnvShape, CheckerErrKind>

pub(crate) fn lookup_rust_ty( &self, genv: GlobalEnv<'_, '_>, place: &Place, ) -> QueryResult<Ty>

pub(crate) fn lookup_place( &mut self, infcx: &mut InferCtxtAt<'_, '_, '_, '_>, place: &Place, ) -> Result<Ty, CheckerErrKind>

pub(crate) fn get(&self, path: &Path) -> Ty

pub fn update_path(&mut self, path: &Path, new_ty: Ty)

pub(crate) fn borrow( &mut self, infcx: &mut InferCtxtAt<'_, '_, '_, '_>, re: Region, mutbl: Mutability, place: &Place, ) -> Result<Ty, CheckerErrKind>

When checking a borrow in the right hand side of an assignment x = &'?n p, we use the annotated region '?n in the type of the result. This region will only be used temporarily and then replaced by the region in the type of x after the assignment. See TypeEnv::assign

pub(crate) fn ptr_to_ref_at_place( &mut self, infcx: &mut InferCtxtAt<'_, '_, '_, '_>, place: &Place, ) -> Result<(), CheckerErrKind>

pub(crate) fn ptr_to_ref( &mut self, infcx: &mut InferCtxtAt<'_, '_, '_, '_>, reason: ConstrReason, re: Region, path: &Path, bound: PtrToRefBound, ) -> InferResult<Ty>

Convert a (strong) pointer to a mutable reference.

This roughly implements the following inference rule:

                  t₁ <: t₂
-------------------------------------------------
Γ₁,ℓ:t1,Γ₂ ; ptr(mut, ℓ) => Γ₁,ℓ:†t₂,Γ₂ ; &mut t2

That’s it, we first get the current type t₁ at location ℓ and check it is a subtype of t₂. Then, we update the type of ℓ to t₂ and block the place.

The bound t₂ can be either inferred (PtrToRefBound::Infer), explicitly provided (PtrToRefBound::Ty), or made equal to t₁ (PtrToRefBound::Identity).

As an example, consider the environment x: i32[a] and the pointer ptr(mut, x). Converting the pointer to a mutable reference with an inferred bound produces the following derivation (roughly):

                   i32[a] <: i32{v: $k(v)}
----------------------------------------------------------------
x: i32[a] ; ptr(mut, x) => x:†i32{v: $k(v)} ; &mut i32{v: $k(v)}

pub(crate) fn fold_local_ptrs( &mut self, infcx: &mut InferCtxtAt<'_, '_, '_, '_>, ) -> InferResult<()>

pub(crate) fn assign( &mut self, infcx: &mut InferCtxtAt<'_, '_, '_, '_>, place: &Place, new_ty: Ty, ) -> Result<(), CheckerErrKind>

Updates the type of place to new_ty. This may involve a strong update if we have ownership of place or a weak update if it’s behind a reference (which fires a subtyping constraint)

When strong updating, the process involves recovering the original regions (lifetimes) used in the (unrefined) Rust type of place and then substituting these regions in new_ty. For instance, if we are assigning a value of type S<&'?10 i32{v: v > 0}> to a variable x, and the (unrefined) Rust type of x is S<&'?5 i32>, before the assignment, we identify a substitution that maps the region '?10 to '?5. After applying this substitution, the type of the place x is updated accordingly. This ensures that the lifetimes in the assigned type are consistent with those expected by the place’s original type definition.

pub(crate) fn move_place( &mut self, infcx: &mut InferCtxtAt<'_, '_, '_, '_>, place: &Place, ) -> Result<Ty, CheckerErrKind>

pub(crate) fn unpack( &mut self, infcx: &mut InferCtxt<'_, '_, '_>, check_overflow: bool, )

pub(crate) fn unblock( &mut self, rcx: &mut RefineCtxt<'_>, place: &Place, check_overflow: bool, )

pub(crate) fn check_goto( self, infcx: &mut InferCtxtAt<'_, '_, '_, '_>, bb_env: &BasicBlockEnv, target: BasicBlock, ) -> Result<(), CheckerErrKind>

pub(crate) fn fold( &mut self, infcx: &mut InferCtxtAt<'_, '_, '_, '_>, place: &Place, ) -> Result<(), CheckerErrKind>

pub(crate) fn unfold_local_ptr( &mut self, infcx: &mut InferCtxt<'_, '_, '_>, bound: &Ty, ) -> InferResult<Loc>

pub(crate) fn unfold_strg_ref( &mut self, infcx: &mut InferCtxt<'_, '_, '_>, path: &Path, ty: &Ty, ) -> InferResult<Loc>

-----------------------------------
Γ ; &strg <ℓ: t> => Γ,ℓ: t ; ptr(ℓ)

pub(crate) fn unfold( &mut self, infcx: &mut InferCtxt<'_, '_, '_>, place: &Place, checker_conf: CheckerConfig, ) -> Result<(), CheckerErrKind>

pub(crate) fn downcast( &mut self, infcx: &mut InferCtxtAt<'_, '_, '_, '_>, place: &Place, variant_idx: VariantIdx, checker_config: CheckerConfig, ) -> Result<(), CheckerErrKind>

pub fn replace_evars(&mut self, evars: &EVarSol)

pub(crate) fn update_ensures( &mut self, infcx: &mut InferCtxt<'_, '_, '_>, output: &FnOutput, overflow_checking: bool, )

pub(crate) fn check_ensures( &mut self, at: &mut InferCtxtAt<'_, '_, '_, '_>, output: &FnOutput, reason: ConstrReason, ) -> InferResult

Trait Implementations

impl<'a> Clone for TypeEnv<'a>

fn clone(&self) -> TypeEnv<'a>

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for TypeEnv<'_>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'a> Default for TypeEnv<'a>

fn default() -> TypeEnv<'a>

Returns the “default value” for a type.

impl LocEnv for TypeEnv<'_>

fn ptr_to_ref( &mut self, infcx: &mut InferCtxtAt<'_, '_, '_, '_>, reason: ConstrReason, re: Region, path: &Path, bound: Ty, ) -> InferResult<Ty>

fn get(&self, path: &Path) -> Ty

fn unfold_strg_ref( &mut self, infcx: &mut InferCtxt<'_, '_, '_>, path: &Path, ty: &Ty, ) -> InferResult<Loc>

impl Pretty for TypeEnv<'_>

fn fmt(&self, cx: &PrettyCx<'_>, f: &mut Formatter<'_>) -> Result

fn default_cx(tcx: TyCtxt<'_>) -> PrettyCx<'_>