Struct flux_refineck::checker::Checker

pub(crate) struct Checker<'ck, 'genv, 'tcx, M> {
    genv: GlobalEnv<'genv, 'tcx>,
    def_id: LocalDefId,
    inherited: Inherited<'ck, M>,
    body: &'ck Body<'tcx>,
    resume_ty: Option<Ty>,
    output: Binder<FnOutput>,
    snapshots: IndexVec<BasicBlock, Option<Snapshot>>,
    visited: BitSet<BasicBlock>,
    queue: WorkQueue<'ck>,
}

Fields

genv: GlobalEnv<'genv, 'tcx>

def_id: LocalDefId

LocalDefId 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>

snapshots: IndexVec<BasicBlock, Option<Snapshot>>

A snapshot of the refinement context at the end of the basic block after applying the effects of the terminator.

visited: BitSet<BasicBlock>

queue: WorkQueue<'ck>

Implementations

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

pub(crate) fn run_in_shape_mode( genv: GlobalEnv<'genv, 'tcx>, def_id: LocalDefId, ghost_stmts: &'ck UnordMap<LocalDefId, GhostStatements>, config: CheckerConfig, ) -> Result<ShapeResult, CheckerError>

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

pub(crate) fn run_in_refine_mode( genv: GlobalEnv<'genv, 'tcx>, def_id: LocalDefId, ghost_stmts: &'ck UnordMap<LocalDefId, GhostStatements>, bb_env_shapes: ShapeResult, config: CheckerConfig, ) -> Result<(RefineTree, KVarGen), CheckerError>

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

fn run( infcx: InferCtxt<'_, 'genv, 'tcx>, def_id: LocalDefId, inherited: Inherited<'ck, 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, source_info: SourceInfo, ) -> Result<(), CheckerError>

fn check_statement( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, stmt: &Statement, ) -> 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<Ty, CheckerError>

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

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

fn check_closure_clauses( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, clauses: &[Binder<FnTraitPredicate>], span: Span, ) -> Result<(), CheckerError>

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

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

Checks conditional branching as in a match statement. SwitchTargets (https://doc.rust-lang.org/nightly/nightly-rustc/stable_mir/mir/struct.SwitchTargets.html) 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( discr_ty: &Ty, targets: &SwitchTargets, ) -> 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 check_rvalue( &mut self, infcx: &mut InferCtxt<'_, 'genv, 'tcx>, env: &mut TypeEnv<'_>, stmt_span: Span, rvalue: &Rvalue, ) -> Result<Ty, CheckerError>

fn check_len( &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<'_, '_, '_>, env: &mut TypeEnv<'_>, stmt_span: Span, bin_op: BinOp, op1: &Operand, op2: &Operand, ) -> Result<Ty, CheckerError>

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, ) -> Result<Ty, CheckerError>

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

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

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, ) -> Result<Ty, CheckerError>

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

fn check_operand( &mut self, infcx: &mut InferCtxt<'_, '_, '_>, env: &mut TypeEnv<'_>, source_span: Span, operand: &Operand, ) -> Result<Ty, CheckerError>

fn check_constant(&mut self, c: &Constant) -> Result<Ty, CheckerError>

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, ) -> Result<(), CheckerError>

fn snapshot_at_dominator(&self, bb: BasicBlock) -> &Snapshot

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

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

fn config(&self) -> CheckerConfig

fn check_overflow(&self) -> bool

fn default_refiner(&self) -> QueryResult<Refiner<'genv, 'tcx>>

fn refine_default(&self, ty: &Ty) -> QueryResult<Ty>

fn refine_with_holes(&self, ty: &Ty) -> QueryResult<Ty>