Struct Checker 

pub(crate) struct Checker<'ck, 'genv, 'tcx, M> {
    genv: GlobalEnv<'genv, 'tcx>,
    checker_id: CheckerId,
    inherited: Inherited<'ck, M>,
    body: &'ck Body<'tcx>,
    resume_ty: Option<Ty>,
    output: Binder<FnOutput>,
    markers: IndexVec<BasicBlock, Option<Marker>>,
    visited: DenseBitSet<BasicBlock>,
    queue: WorkQueue<'ck>,
    default_refiner: Refiner<'genv, 'tcx>,
    promoted: &'ck IndexSlice<Promoted, Ty>,
}

Fields

genv: GlobalEnv<'genv, 'tcx>

checker_id: CheckerId

CheckerId of the function-like item being checked.

inherited: Inherited<'ck, M>

body: &'ck Body<'tcx>

resume_ty: Option<Ty>

The type used for the resume argument if we are checking a generator.

output: Binder<FnOutput>

markers: IndexVec<BasicBlock, Option<Marker>>

A marker to the node in the refinement tree at the end of the basic block after applying the effects of the terminator.

visited: DenseBitSet<BasicBlock>

queue: WorkQueue<'ck>

default_refiner: Refiner<'genv, 'tcx>

promoted: &'ck IndexSlice<Promoted, Ty>

The templates for the promoted bodies of the current function

Implementations

impl<'genv, 'tcx> Checker<'_, 'genv, 'tcx, ShapeMode>

pub(crate) fn run_in_shape_mode<'ck>( genv: GlobalEnv<'genv, 'tcx>, local_id: LocalDefId, ghost_stmts: &'ck UnordMap<CheckerId, GhostStatements>, closures: &'ck mut UnordMap<DefId, PolyFnSig>, opts: InferOpts, ) -> Result<ShapeResult, CheckerError>

impl<'genv, 'tcx> Checker<'_, 'genv, 'tcx, RefineMode>

pub(crate) fn run_in_refine_mode<'ck>( genv: GlobalEnv<'genv, 'tcx>, local_id: LocalDefId, ghost_stmts: &'ck UnordMap<CheckerId, GhostStatements>, closures: &'ck mut UnordMap<DefId, PolyFnSig>, bb_env_shapes: ShapeResult, opts: InferOpts, ) -> Result<InferCtxtRoot<'genv, 'tcx>, CheckerError>

impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M>

fn new( genv: GlobalEnv<'genv, 'tcx>, checker_id: CheckerId, inherited: Inherited<'ck, M>, body: &'ck Body<'tcx>, fn_sig: FnSig, promoted: &'ck IndexSlice<Promoted, Ty>, ) -> QueryResult<Self>

fn check_body( infcx: &mut InferCtxt<'_, 'genv, 'tcx>, checker_id: CheckerId, inherited: Inherited<'ck, M>, body: &'ck Body<'tcx>, poly_sig: PolyFnSig, promoted: &'ck IndexSlice<Promoted, Ty>, ) -> Result<(), CheckerError>

fn promoted_tys( infcx: &mut InferCtxt<'_, 'genv, 'tcx>, def_id: LocalDefId, body_root: &BodyRoot<'tcx>, ) -> QueryResult<IndexVec<Promoted, Ty>>

Assign a template with fresh kvars to each promoted constant in body_root.

fn run( infcx: InferCtxt<'_, 'genv, 'tcx>, def_id: LocalDefId, inherited: Inherited<'_, M>, poly_sig: PolyFnSig, ) -> Result<(), CheckerError>

fn check_basic_block( &mut self, infcx: InferCtxt<'_, 'genv, 'tcx>, env: TypeEnv<'_>, bb: BasicBlock, ) -> Result<(), CheckerError>

fn check_assign_ty( &mut self, infcx: &mut InferCtxt<'_, '_, '_>, env: &mut TypeEnv<'_>, place: &Place, ty: Ty, span: Span, ) -> InferResult

fn check_statement( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, stmt: &Statement<'tcx>, ) -> Result<(), CheckerError>

fn is_exit_block(&self, bb: BasicBlock) -> bool

fn check_terminator( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, terminator: &Terminator<'tcx>, last_stmt_span: Option<Span>, ) -> Result<Vec<(BasicBlock, Guard)>, CheckerError>

For check_terminator, the output Vec<BasicBlock, Guard> denotes,

• BasicBlock “successors” of the current terminator, and
• Guard are extra control information from, e.g. the SwitchInt (or Assert) you can assume when checking the corresponding successor.

fn check_ret( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, span: Span, ) -> Result<(), CheckerError>

fn check_call( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, span: Span, callee_def_id: Option<DefId>, fn_sig: EarlyBinder<PolyFnSig>, generic_args: &[GenericArg], actuals: &[Ty], ) -> Result<ResolvedCall, CheckerError>

fn check_coroutine_obligations( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, obligs: Vec<Binder<CoroutineObligPredicate>>, ) -> Result<(), CheckerError>

fn find_self_ty_fn_sig( &self, self_ty: Ty<'tcx>, span: Span, ) -> Result<PolyFnSig, CheckerError>

fn check_fn_trait_clause( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, poly_fn_trait_pred: &Binder<FnTraitPredicate>, span: Span, ) -> Result<(), CheckerError>

fn check_assert( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, terminator_span: Span, cond: &Operand<'tcx>, expected: bool, msg: &AssertKind, ) -> InferResult<Guard>

fn check_if(discr_ty: &Ty, targets: &SwitchTargets) -> Vec<(BasicBlock, Guard)>

Checks conditional branching as in a match statement. SwitchTargets contains a list of branches - the exact bit value which is being compared and the block to jump to. Using the conditionals, each branch can be checked using the new control flow information. See https://github.com/flux-rs/flux/pull/840#discussion_r1786543174

fn check_match( infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, discr_ty: &Ty, targets: &SwitchTargets, span: Span, ) -> Vec<(BasicBlock, Guard)>

fn check_successors( &mut self, infcx: InferCtxt<'_, 'genv, 'tcx>, env: TypeEnv<'_>, from: BasicBlock, terminator_span: Span, successors: Vec<(BasicBlock, Guard)>, ) -> Result<(), CheckerError>

fn check_goto( &mut self, infcx: InferCtxt<'_, 'genv, 'tcx>, env: TypeEnv<'_>, span: Span, target: BasicBlock, ) -> Result<(), CheckerError>

fn closure_template( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, stmt_span: Span, args: &GenericArgs, operands: &[Operand<'tcx>], ) -> InferResult<(Vec<Ty>, PolyFnSig)>

fn check_closure_body( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, did: &DefId, upvar_tys: &[Ty], args: &GenericArgs, poly_sig: &PolyFnSig, ) -> Result<(), CheckerError>

fn check_rvalue_closure( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, stmt_span: Span, did: &DefId, args: &GenericArgs, operands: &[Operand<'tcx>], ) -> Result<Ty, CheckerError>

fn check_rvalue( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, stmt_span: Span, rvalue: &Rvalue<'tcx>, ) -> Result<Ty, CheckerError>

fn check_raw_ptr_metadata( &mut self, infcx: &mut InferCtxt<'_, '_, '_>, env: &mut TypeEnv<'_>, stmt_span: Span, place: &Place, ) -> Result<Ty, CheckerError>

fn check_binary_op( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, stmt_span: Span, bin_op: BinOp, op1: &Operand<'tcx>, op2: &Operand<'tcx>, ) -> InferResult<Ty>

fn check_nullary_op(&self, null_op: NullOp, _ty: &Ty) -> Ty

fn check_unary_op( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, stmt_span: Span, un_op: UnOp, op: &Operand<'tcx>, ) -> InferResult<Ty>

fn check_mk_array( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, stmt_span: Span, args: &[Ty], arr_ty: Ty, ) -> InferResult<Ty>

fn check_cast( &self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, stmt_span: Span, kind: CastKind, from: &Ty, to: &Ty, ) -> InferResult<Ty>

fn discr_to_int_cast(adt_def: &AdtDef, bty: BaseTy) -> Ty

fn check_unsize_cast( &self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, span: Span, src: &Ty, dst: &Ty, ) -> InferResult<Ty>

fn check_operands( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, span: Span, operands: &[Operand<'tcx>], ) -> InferResult<Vec<Ty>>

fn check_operand( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, span: Span, operand: &Operand<'tcx>, ) -> InferResult<Ty>

fn check_constant( &mut self, infcx: &InferCtxt<'_, 'genv, 'tcx>, constant: &ConstOperand<'tcx>, ) -> QueryResult<Ty>

fn check_ty_const( &mut self, constant: &ConstOperand<'tcx>, cst: Const<'tcx>, ty: Ty<'tcx>, ) -> QueryResult<Option<Ty>>

fn check_const_val(&mut self, val: ConstValue, ty: Ty<'tcx>) -> Option<Ty>

fn check_uneval_const( &mut self, infcx: &InferCtxt<'_, 'genv, 'tcx>, constant: &ConstOperand<'tcx>, uneval: UnevaluatedConst<'tcx>, ty: Ty<'tcx>, ) -> QueryResult<Option<Ty>>

fn check_scalar(&mut self, scalar: Scalar, ty: Ty<'tcx>) -> Option<Ty>

fn check_scalar_int(&mut self, scalar: ScalarInt, ty: Ty<'tcx>) -> Option<Ty>

fn check_ghost_statements_at( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, point: Point, span: Span, ) -> Result<(), CheckerError>

fn check_ghost_statement( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, stmt: &GhostStatement, span: Span, ) -> InferResult

fn marker_at_dominator(&self, bb: BasicBlock) -> &Marker

fn dominators(&self) -> &'ck Dominators<BasicBlock>

fn ghost_stmts(&self) -> &'ck GhostStatements

fn refine_default<T: Refine>(&self, ty: &T) -> QueryResult<T::Output>

fn refine_with_holes<T: Refine>( &self, ty: &T, ) -> QueryResult<<T as Refine>::Output>