flux_refineck/
checker.rs

1use std::{collections::hash_map::Entry, iter, vec};
2
3use flux_common::{
4    bug, dbg, index::IndexVec, iter::IterExt, span_bug, tracked_span_bug,
5    tracked_span_dbg_assert_eq,
6};
7use flux_config::{self as config, InferOpts};
8use flux_infer::{
9    infer::{
10        ConstrReason, GlobalEnvExt as _, InferCtxt, InferCtxtRoot, InferResult, SubtypeReason,
11    },
12    projections::NormalizeExt as _,
13    refine_tree::{Marker, RefineCtxtTrace},
14};
15use flux_middle::{
16    global_env::GlobalEnv,
17    queries::{QueryResult, try_query},
18    query_bug,
19    rty::{
20        self, AdtDef, BaseTy, Binder, Bool, Clause, CoroutineObligPredicate, EarlyBinder, Expr,
21        FnOutput, FnTraitPredicate, GenericArg, GenericArgsExt as _, Int, IntTy, InternalFuncKind,
22        Mutability, Path, PolyFnSig, PtrKind, RefineArgs, RefineArgsExt,
23        Region::ReStatic,
24        Ty, TyKind, Uint, UintTy, VariantIdx,
25        fold::{TypeFoldable, TypeFolder, TypeSuperFoldable},
26        refining::{Refine, Refiner},
27    },
28};
29use flux_rustc_bridge::{
30    self, ToRustc,
31    mir::{
32        self, AggregateKind, AssertKind, BasicBlock, Body, BorrowKind, CastKind, Constant,
33        Location, NonDivergingIntrinsic, Operand, Place, Rvalue, START_BLOCK, Statement,
34        StatementKind, Terminator, TerminatorKind, UnOp,
35    },
36    ty::{self, GenericArgsExt as _},
37};
38use itertools::{Itertools, izip};
39use rustc_data_structures::{graph::dominators::Dominators, unord::UnordMap};
40use rustc_hash::{FxHashMap, FxHashSet};
41use rustc_hir::{
42    LangItem,
43    def_id::{DefId, LocalDefId},
44};
45use rustc_index::bit_set::DenseBitSet;
46use rustc_infer::infer::TyCtxtInferExt;
47use rustc_middle::{
48    mir::SwitchTargets,
49    ty::{TyCtxt, TypeSuperVisitable as _, TypeVisitable as _, TypingMode},
50};
51use rustc_span::{Span, sym};
52
53use self::errors::{CheckerError, ResultExt};
54use crate::{
55    ghost_statements::{GhostStatement, GhostStatements, Point},
56    primops,
57    queue::WorkQueue,
58    rty::Char,
59    type_env::{
60        BasicBlockEnv, BasicBlockEnvShape, PtrToRefBound, SpanTrace, TypeEnv, TypeEnvTrace,
61    },
62};
63
64type Result<T = ()> = std::result::Result<T, CheckerError>;
65
66pub(crate) struct Checker<'ck, 'genv, 'tcx, M> {
67    genv: GlobalEnv<'genv, 'tcx>,
68    /// [`LocalDefId`] of the function-like item being checked.
69    def_id: LocalDefId,
70    inherited: Inherited<'ck, M>,
71    body: &'ck Body<'tcx>,
72    /// The type used for the `resume` argument if we are checking a generator.
73    resume_ty: Option<Ty>,
74    output: Binder<FnOutput>,
75    /// A marker to the node in the refinement tree at the end of the basic block after applying
76    /// the effects of the terminator.
77    markers: IndexVec<BasicBlock, Option<Marker>>,
78    visited: DenseBitSet<BasicBlock>,
79    queue: WorkQueue<'ck>,
80    default_refiner: Refiner<'genv, 'tcx>,
81}
82
83/// Fields shared by the top-level function and its nested closure/generators
84struct Inherited<'ck, M> {
85    /// [`Expr`]s used to instantiate the early bound refinement parameters of the top-level function
86    /// signature
87    ghost_stmts: &'ck UnordMap<LocalDefId, GhostStatements>,
88    mode: &'ck mut M,
89
90    /// This map has the "templates" generated for the closures constructed (in [`Checker::check_rvalue_closure`]).
91    /// The `PolyFnSig`` can have free variables (inside the scope of kvars) in the template, so we
92    /// we need to be careful and only use it in the correct scope.
93    closures: &'ck mut UnordMap<DefId, PolyFnSig>,
94}
95
96#[derive(Debug)]
97struct ResolvedCall {
98    output: Ty,
99    /// The refine arguments given to the call
100    _early_args: Vec<Expr>,
101    /// The refine arguments given to the call
102    _late_args: Vec<Expr>,
103}
104
105impl<'ck, M: Mode> Inherited<'ck, M> {
106    fn new(
107        mode: &'ck mut M,
108        ghost_stmts: &'ck UnordMap<LocalDefId, GhostStatements>,
109        closures: &'ck mut UnordMap<DefId, PolyFnSig>,
110    ) -> Result<Self> {
111        Ok(Self { ghost_stmts, mode, closures })
112    }
113
114    fn reborrow(&mut self) -> Inherited<'_, M> {
115        Inherited { ghost_stmts: self.ghost_stmts, mode: &mut *self.mode, closures: self.closures }
116    }
117}
118
119pub(crate) trait Mode: Sized {
120    #[expect(dead_code)]
121    const NAME: &str;
122
123    fn enter_basic_block<'ck, 'genv, 'tcx>(
124        ck: &mut Checker<'ck, 'genv, 'tcx, Self>,
125        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
126        bb: BasicBlock,
127    ) -> TypeEnv<'ck>;
128
129    fn check_goto_join_point<'genv, 'tcx>(
130        ck: &mut Checker<'_, 'genv, 'tcx, Self>,
131        infcx: InferCtxt<'_, 'genv, 'tcx>,
132        env: TypeEnv,
133        terminator_span: Span,
134        target: BasicBlock,
135    ) -> Result<bool>;
136
137    fn clear(ck: &mut Checker<Self>, bb: BasicBlock);
138}
139
140pub(crate) struct ShapeMode {
141    bb_envs: FxHashMap<LocalDefId, FxHashMap<BasicBlock, BasicBlockEnvShape>>,
142}
143
144pub(crate) struct RefineMode {
145    bb_envs: FxHashMap<LocalDefId, FxHashMap<BasicBlock, BasicBlockEnv>>,
146}
147
148/// The result of running the shape phase.
149pub(crate) struct ShapeResult(FxHashMap<LocalDefId, FxHashMap<BasicBlock, BasicBlockEnvShape>>);
150
151/// A `Guard` describes extra "control" information that holds at the start of a successor basic block
152#[derive(Debug)]
153enum Guard {
154    /// No extra information holds, e.g., for a plain goto.
155    None,
156    /// A predicate that can be assumed, e.g., in the branches of an if-then-else.
157    Pred(Expr),
158    /// The corresponding place was found to be of a particular variant.
159    Match(Place, VariantIdx),
160}
161
162impl<'ck, 'genv, 'tcx> Checker<'ck, 'genv, 'tcx, ShapeMode> {
163    pub(crate) fn run_in_shape_mode(
164        genv: GlobalEnv<'genv, 'tcx>,
165        local_id: LocalDefId,
166        ghost_stmts: &'ck UnordMap<LocalDefId, GhostStatements>,
167        closures: &'ck mut UnordMap<DefId, PolyFnSig>,
168        opts: InferOpts,
169    ) -> Result<ShapeResult> {
170        let def_id = local_id.to_def_id();
171        dbg::shape_mode_span!(genv.tcx(), local_id).in_scope(|| {
172            let span = genv.tcx().def_span(local_id);
173            let mut mode = ShapeMode { bb_envs: FxHashMap::default() };
174
175            let body = genv.mir(local_id).with_span(span)?;
176
177            // In shape mode we don't care about kvars
178            let mut root_ctxt = try_query(|| {
179                genv.infcx_root(&body.infcx, opts)
180                    .with_dummy_kvars()
181                    .identity_for_item(def_id)?
182                    .build()
183            })
184            .with_span(span)?;
185
186            let inherited = Inherited::new(&mut mode, ghost_stmts, closures)?;
187
188            let infcx = root_ctxt.infcx(def_id, &body.infcx);
189            let poly_sig = genv
190                .fn_sig(local_id)
191                .with_span(span)?
192                .instantiate_identity();
193            Checker::run(infcx, local_id, inherited, poly_sig)?;
194
195            Ok(ShapeResult(mode.bb_envs))
196        })
197    }
198}
199
200impl<'ck, 'genv, 'tcx> Checker<'ck, 'genv, 'tcx, RefineMode> {
201    pub(crate) fn run_in_refine_mode(
202        genv: GlobalEnv<'genv, 'tcx>,
203        local_id: LocalDefId,
204        ghost_stmts: &'ck UnordMap<LocalDefId, GhostStatements>,
205        closures: &'ck mut UnordMap<DefId, PolyFnSig>,
206        bb_env_shapes: ShapeResult,
207        opts: InferOpts,
208    ) -> Result<InferCtxtRoot<'genv, 'tcx>> {
209        let def_id = local_id.to_def_id();
210        let span = genv.tcx().def_span(def_id);
211
212        let body = genv.mir(local_id).with_span(span)?;
213        let mut root_ctxt = try_query(|| {
214            genv.infcx_root(&body.infcx, opts)
215                .identity_for_item(def_id)?
216                .build()
217        })
218        .with_span(span)?;
219        let bb_envs = bb_env_shapes.into_bb_envs(&mut root_ctxt);
220
221        dbg::refine_mode_span!(genv.tcx(), def_id, bb_envs).in_scope(|| {
222            // Check the body of the function def_id against its signature
223            let mut mode = RefineMode { bb_envs };
224            let inherited = Inherited::new(&mut mode, ghost_stmts, closures)?;
225            let infcx = root_ctxt.infcx(def_id, &body.infcx);
226            let poly_sig = genv.fn_sig(def_id).with_span(span)?;
227            let poly_sig = poly_sig.instantiate_identity();
228            Checker::run(infcx, local_id, inherited, poly_sig)?;
229
230            Ok(root_ctxt)
231        })
232    }
233}
234
235/// `SubFn` lets us reuse _most_ of the same code for `check_fn_subtyping` for both the case where
236/// we have an early-bound function signature (e.g., for a trait method???) and versions without,
237/// e.g. a plain closure against its FnTraitPredicate obligation.
238#[derive(Debug)]
239pub enum SubFn {
240    Poly(DefId, EarlyBinder<rty::PolyFnSig>, rty::GenericArgs),
241    Mono(rty::PolyFnSig),
242}
243
244impl SubFn {
245    pub fn as_ref(&self) -> &rty::PolyFnSig {
246        match self {
247            SubFn::Poly(_, sig, _) => sig.skip_binder_ref(),
248            SubFn::Mono(sig) => sig,
249        }
250    }
251}
252
253/// The function `check_fn_subtyping` does a function subtyping check between
254/// the sub-type (T_f) corresponding to the type of `def_id` @ `args` and the
255/// super-type (T_g) corresponding to the `oblig_sig`. This subtyping is handled
256/// as akin to the code
257///
258///   T_f := (S1,...,Sn) -> S
259///   T_g := (T1,...,Tn) -> T
260///   T_f <: T_g
261///
262///  fn g(x1:T1,...,xn:Tn) -> T {
263///      f(x1,...,xn)
264///  }
265fn check_fn_subtyping(
266    infcx: &mut InferCtxt,
267    sub_sig: SubFn,
268    super_sig: &rty::PolyFnSig,
269    span: Span,
270) -> InferResult {
271    let mut infcx = infcx.branch();
272    let mut infcx = infcx.at(span);
273    let tcx = infcx.genv.tcx();
274
275    let super_sig = super_sig
276        .replace_bound_vars(|_| rty::ReErased, |sort, _| Expr::fvar(infcx.define_var(sort)))
277        .normalize_projections(&mut infcx)?;
278
279    // 1. Unpack `T_g` input types
280    let actuals = super_sig
281        .inputs()
282        .iter()
283        .map(|ty| infcx.unpack(ty))
284        .collect_vec();
285
286    let mut env = TypeEnv::empty();
287    let actuals = unfold_local_ptrs(&mut infcx, &mut env, sub_sig.as_ref(), &actuals)?;
288    let actuals = infer_under_mut_ref_hack(&mut infcx, &actuals[..], sub_sig.as_ref());
289
290    let output = infcx.ensure_resolved_evars(|infcx| {
291        // 2. Fresh names for `T_f` refine-params / Instantiate fn_def_sig and normalize it
292        // in subtyping_mono, skip next two steps...
293        let sub_sig = match sub_sig {
294            SubFn::Poly(def_id, early_sig, sub_args) => {
295                let refine_args = infcx.instantiate_refine_args(def_id, &sub_args)?;
296                early_sig.instantiate(tcx, &sub_args, &refine_args)
297            }
298            SubFn::Mono(sig) => sig,
299        };
300        // ... jump right here.
301        let sub_sig = sub_sig
302            .replace_bound_vars(|_| rty::ReErased, |sort, mode| infcx.fresh_infer_var(sort, mode))
303            .normalize_projections(infcx)?;
304
305        // 3. INPUT subtyping (g-input <: f-input)
306        for requires in super_sig.requires() {
307            infcx.assume_pred(requires);
308        }
309        for (actual, formal) in iter::zip(actuals, sub_sig.inputs()) {
310            let reason = ConstrReason::Subtype(SubtypeReason::Input);
311            infcx.subtyping_with_env(&mut env, &actual, formal, reason)?;
312        }
313        // we check the requires AFTER the actual-formal subtyping as the above may unfold stuff in
314        // the actuals
315        for requires in sub_sig.requires() {
316            let reason = ConstrReason::Subtype(SubtypeReason::Requires);
317            infcx.check_pred(requires, reason);
318        }
319
320        Ok(sub_sig.output())
321    })?;
322
323    let output = infcx
324        .fully_resolve_evars(&output)
325        .replace_bound_refts_with(|sort, _, _| Expr::fvar(infcx.define_var(sort)));
326
327    // 4. OUTPUT subtyping (f_out <: g_out)
328    infcx.ensure_resolved_evars(|infcx| {
329        let super_output = super_sig
330            .output()
331            .replace_bound_refts_with(|sort, mode, _| infcx.fresh_infer_var(sort, mode));
332        let reason = ConstrReason::Subtype(SubtypeReason::Output);
333        infcx.subtyping(&output.ret, &super_output.ret, reason)?;
334
335        // 6. Update state with Output "ensures" and check super ensures
336        env.assume_ensures(infcx, &output.ensures, span);
337        fold_local_ptrs(infcx, &mut env, span)?;
338        env.check_ensures(
339            infcx,
340            &super_output.ensures,
341            ConstrReason::Subtype(SubtypeReason::Ensures),
342        )
343    })
344}
345
346/// Trait subtyping check, which makes sure that the type for an impl method (def_id)
347/// is a subtype of the corresponding trait method.
348pub(crate) fn trait_impl_subtyping<'genv, 'tcx>(
349    genv: GlobalEnv<'genv, 'tcx>,
350    def_id: LocalDefId,
351    opts: InferOpts,
352    span: Span,
353) -> InferResult<Option<InferCtxtRoot<'genv, 'tcx>>> {
354    let tcx = genv.tcx();
355
356    // Skip the check if this is not an impl method
357    let Some((impl_trait_ref, trait_method_id)) = find_trait_item(genv, def_id)? else {
358        return Ok(None);
359    };
360    let impl_method_id = def_id.to_def_id();
361    // Skip the check if either the trait-method or the impl-method are marked as `trusted_impl`
362    if genv.has_trusted_impl(trait_method_id) || genv.has_trusted_impl(impl_method_id) {
363        return Ok(None);
364    }
365
366    let impl_id = tcx.impl_of_method(impl_method_id).unwrap();
367    let impl_method_args = GenericArg::identity_for_item(genv, impl_method_id)?;
368    let trait_method_args = impl_method_args.rebase_onto(&tcx, impl_id, &impl_trait_ref.args);
369    let trait_refine_args = RefineArgs::identity_for_item(genv, trait_method_id)?;
370
371    let rustc_infcx = genv
372        .tcx()
373        .infer_ctxt()
374        .with_next_trait_solver(true)
375        .build(TypingMode::non_body_analysis());
376
377    let mut root_ctxt = genv
378        .infcx_root(&rustc_infcx, opts)
379        .with_const_generics(impl_id)?
380        .with_refinement_generics(trait_method_id, &trait_method_args)?
381        .build()?;
382
383    let mut infcx = root_ctxt.infcx(impl_method_id, &rustc_infcx);
384
385    let trait_fn_sig =
386        genv.fn_sig(trait_method_id)?
387            .instantiate(tcx, &trait_method_args, &trait_refine_args);
388    let impl_sig = genv.fn_sig(impl_method_id)?;
389    let sub_sig = SubFn::Poly(impl_method_id, impl_sig, impl_method_args);
390
391    check_fn_subtyping(&mut infcx, sub_sig, &trait_fn_sig, span)?;
392    Ok(Some(root_ctxt))
393}
394
395fn find_trait_item(
396    genv: GlobalEnv<'_, '_>,
397    def_id: LocalDefId,
398) -> QueryResult<Option<(rty::TraitRef, DefId)>> {
399    let tcx = genv.tcx();
400    let def_id = def_id.to_def_id();
401    if let Some(impl_id) = tcx.impl_of_method(def_id)
402        && let Some(impl_trait_ref) = genv.impl_trait_ref(impl_id)?
403    {
404        let impl_trait_ref = impl_trait_ref.instantiate_identity();
405        let trait_item_id = tcx.associated_item(def_id).trait_item_def_id.unwrap();
406        return Ok(Some((impl_trait_ref, trait_item_id)));
407    }
408    Ok(None)
409}
410
411/// Temporarily (around a function call) convert an `&mut` to an `&strg` to allow for the call to be
412/// checked. This is done by unfolding the `&mut` into a local pointer at the call-site and then
413/// folding the pointer back into the `&mut` upon return.
414/// See also [`fold_local_ptrs`].
415///
416/// ```text
417///             unpack(T) = T'
418/// ---------------------------------------[local-unfold]
419/// Γ ; &mut T => Γ, l:[<: T] T' ; ptr(l)
420/// ```
421fn unfold_local_ptrs(
422    infcx: &mut InferCtxt,
423    env: &mut TypeEnv,
424    fn_sig: &PolyFnSig,
425    actuals: &[Ty],
426) -> InferResult<Vec<Ty>> {
427    // We *only* need to know whether each input is a &strg or not
428    let fn_sig = fn_sig.skip_binder_ref();
429    let mut tys = vec![];
430    for (actual, input) in izip!(actuals, fn_sig.inputs()) {
431        let actual = if let (
432            TyKind::Indexed(BaseTy::Ref(re, bound, Mutability::Mut), _),
433            TyKind::StrgRef(_, _, _),
434        ) = (actual.kind(), input.kind())
435        {
436            let loc = env.unfold_local_ptr(infcx, bound)?;
437            let path1 = Path::new(loc, rty::List::empty());
438            Ty::ptr(PtrKind::Mut(*re), path1)
439        } else {
440            actual.clone()
441        };
442        tys.push(actual);
443    }
444    Ok(tys)
445}
446
447/// Fold local pointers implements roughly a rule like the following (for all local pointers)
448/// that converts the local pointers created via [`unfold_local_ptrs`] back into `&mut`.
449///
450/// ```text
451///       T1 <: T2
452/// --------------------- [local-fold]
453/// Γ, l:[<: T2] T1 => Γ
454/// ```
455fn fold_local_ptrs(infcx: &mut InferCtxt, env: &mut TypeEnv, span: Span) -> InferResult {
456    let mut at = infcx.at(span);
457    env.fold_local_ptrs(&mut at)
458}
459
460impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> {
461    fn run(
462        mut infcx: InferCtxt<'_, 'genv, 'tcx>,
463        def_id: LocalDefId,
464        inherited: Inherited<'ck, M>,
465        poly_sig: PolyFnSig,
466    ) -> Result {
467        let genv = infcx.genv;
468        let span = genv.tcx().def_span(def_id);
469
470        let body = genv.mir(def_id).with_span(span)?;
471
472        let fn_sig = poly_sig
473            .replace_bound_vars(|_| rty::ReErased, |sort, _| Expr::fvar(infcx.define_var(sort)))
474            .normalize_projections(&mut infcx.at(span))
475            .with_span(span)?;
476
477        let mut env = TypeEnv::new(&mut infcx, &body, &fn_sig);
478
479        // (NOTE:YIELD) per https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.TerminatorKind.html#variant.Yield
480        //   "execution of THIS function continues at the `resume` basic block, with THE SECOND ARGUMENT WRITTEN
481        //    to the `resume_arg` place..."
482        let resume_ty = if genv.tcx().is_coroutine(def_id.to_def_id()) {
483            Some(fn_sig.inputs()[1].clone())
484        } else {
485            None
486        };
487        let mut ck = Checker {
488            def_id,
489            genv,
490            inherited,
491            body: &body,
492            resume_ty,
493            visited: DenseBitSet::new_empty(body.basic_blocks.len()),
494            output: fn_sig.output().clone(),
495            markers: IndexVec::from_fn_n(|_| None, body.basic_blocks.len()),
496            queue: WorkQueue::empty(body.basic_blocks.len(), &body.dominator_order_rank),
497            default_refiner: Refiner::default_for_item(genv, def_id.to_def_id()).with_span(span)?,
498        };
499        ck.check_ghost_statements_at(&mut infcx, &mut env, Point::FunEntry, body.span())?;
500
501        ck.check_goto(infcx.branch(), env, body.span(), START_BLOCK)?;
502
503        while let Some(bb) = ck.queue.pop() {
504            let visited = ck.visited.contains(bb);
505
506            if visited {
507                M::clear(&mut ck, bb);
508            }
509
510            let marker = ck.marker_at_dominator(bb);
511            let mut infcx = infcx.move_to(marker, visited);
512            let mut env = M::enter_basic_block(&mut ck, &mut infcx, bb);
513            env.unpack(&mut infcx);
514            ck.check_basic_block(infcx, env, bb)?;
515        }
516
517        Ok(())
518    }
519
520    fn check_basic_block(
521        &mut self,
522        mut infcx: InferCtxt<'_, 'genv, 'tcx>,
523        mut env: TypeEnv,
524        bb: BasicBlock,
525    ) -> Result {
526        dbg::basic_block_start!(bb, infcx, env);
527
528        self.visited.insert(bb);
529        let data = &self.body.basic_blocks[bb];
530        let mut last_stmt_span = None;
531        let mut location = Location { block: bb, statement_index: 0 };
532        for stmt in &data.statements {
533            let span = stmt.source_info.span;
534            self.check_ghost_statements_at(
535                &mut infcx,
536                &mut env,
537                Point::BeforeLocation(location),
538                span,
539            )?;
540            bug::track_span(span, || {
541                dbg::statement!("start", stmt, &infcx, &env, span, &self);
542                self.check_statement(&mut infcx, &mut env, stmt)?;
543                dbg::statement!("end", stmt, &infcx, &env, span, &self);
544                Ok(())
545            })?;
546            if !stmt.is_nop() {
547                last_stmt_span = Some(span);
548            }
549            location = location.successor_within_block();
550        }
551
552        if let Some(terminator) = &data.terminator {
553            let span = terminator.source_info.span;
554            self.check_ghost_statements_at(
555                &mut infcx,
556                &mut env,
557                Point::BeforeLocation(location),
558                span,
559            )?;
560
561            bug::track_span(span, || {
562                dbg::terminator!("start", terminator, infcx, env);
563
564                let successors =
565                    self.check_terminator(&mut infcx, &mut env, terminator, last_stmt_span)?;
566                dbg::terminator!("end", terminator, infcx, env);
567
568                self.markers[bb] = Some(infcx.marker());
569                let term_span = last_stmt_span.unwrap_or(span);
570                self.check_successors(infcx, env, bb, term_span, successors)
571            })?;
572        }
573        Ok(())
574    }
575
576    fn check_assign_ty(
577        &mut self,
578        infcx: &mut InferCtxt,
579        env: &mut TypeEnv,
580        place: &Place,
581        ty: Ty,
582        span: Span,
583    ) -> InferResult {
584        let ty = infcx.hoister(true).hoist(&ty);
585        env.assign(&mut infcx.at(span), place, ty)
586    }
587
588    fn check_statement(
589        &mut self,
590        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
591        env: &mut TypeEnv,
592        stmt: &Statement,
593    ) -> Result {
594        let stmt_span = stmt.source_info.span;
595        match &stmt.kind {
596            StatementKind::Assign(place, rvalue) => {
597                let ty = self.check_rvalue(infcx, env, stmt_span, rvalue)?;
598                self.check_assign_ty(infcx, env, place, ty, stmt_span)
599                    .with_span(stmt_span)?;
600            }
601            StatementKind::SetDiscriminant { .. } => {
602                // TODO(nilehmann) double check here that the place is unfolded to
603                // the correct variant. This should be guaranteed by rustc
604            }
605            StatementKind::FakeRead(_) => {
606                // TODO(nilehmann) fake reads should be folding points
607            }
608            StatementKind::AscribeUserType(_, _) => {
609                // User ascriptions affect nll, but no refinement type checking.
610                // Maybe we can use this to associate refinement type to locals.
611            }
612            StatementKind::PlaceMention(_) => {
613                // Place mentions are a no-op used to detect uses of unsafe that would
614                // otherwise be optimized away.
615            }
616            StatementKind::Nop => {}
617            StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(op)) => {
618                // Currently, we only have the `assume` intrinsic, which if we're to trust rustc should be a NOP.
619                // TODO: There may be a use-case to actually "assume" the bool index associated with the operand,
620                // i.e. to strengthen the `rcx` / `env` with the assumption that the bool-index is in fact `true`...
621                let _ = self
622                    .check_operand(infcx, env, stmt_span, op)
623                    .with_span(stmt_span)?;
624            }
625        }
626        Ok(())
627    }
628
629    fn is_exit_block(&self, bb: BasicBlock) -> bool {
630        let data = &self.body.basic_blocks[bb];
631        let is_no_op = data.statements.iter().all(Statement::is_nop);
632        let is_ret = match &data.terminator {
633            None => false,
634            Some(term) => term.is_return(),
635        };
636        is_no_op && is_ret
637    }
638
639    /// For `check_terminator`, the output `Vec<BasicBlock, Guard>` denotes,
640    /// - `BasicBlock` "successors" of the current terminator, and
641    /// - `Guard` are extra control information from, e.g. the `SwitchInt` (or `Assert`) you can assume when checking the corresponding successor.
642    fn check_terminator(
643        &mut self,
644        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
645        env: &mut TypeEnv,
646        terminator: &Terminator<'tcx>,
647        last_stmt_span: Option<Span>,
648    ) -> Result<Vec<(BasicBlock, Guard)>> {
649        let source_info = terminator.source_info;
650        let terminator_span = source_info.span;
651        match &terminator.kind {
652            TerminatorKind::Return => {
653                self.check_ret(infcx, env, last_stmt_span.unwrap_or(terminator_span))?;
654                Ok(vec![])
655            }
656            TerminatorKind::Unreachable => Ok(vec![]),
657            TerminatorKind::CoroutineDrop => Ok(vec![]),
658            TerminatorKind::Goto { target } => Ok(vec![(*target, Guard::None)]),
659            TerminatorKind::Yield { resume, resume_arg, .. } => {
660                if let Some(resume_ty) = self.resume_ty.clone() {
661                    self.check_assign_ty(infcx, env, resume_arg, resume_ty, terminator_span)
662                        .with_span(terminator_span)?;
663                } else {
664                    bug!("yield in non-generator function");
665                }
666                Ok(vec![(*resume, Guard::None)])
667            }
668            TerminatorKind::SwitchInt { discr, targets } => {
669                let discr_ty = self
670                    .check_operand(infcx, env, terminator_span, discr)
671                    .with_span(terminator_span)?;
672                if discr_ty.is_integral() || discr_ty.is_bool() || discr_ty.is_char() {
673                    Ok(Self::check_if(&discr_ty, targets))
674                } else {
675                    Ok(Self::check_match(&discr_ty, targets))
676                }
677            }
678            TerminatorKind::Call { kind, args, destination, target, .. } => {
679                let actuals = self
680                    .check_operands(infcx, env, terminator_span, args)
681                    .with_span(terminator_span)?;
682                let ret = match kind {
683                    mir::CallKind::FnDef { resolved_id, resolved_args, .. } => {
684                        let fn_sig = self.genv.fn_sig(*resolved_id).with_span(terminator_span)?;
685                        let generic_args = instantiate_args_for_fun_call(
686                            self.genv,
687                            self.def_id.to_def_id(),
688                            *resolved_id,
689                            &resolved_args.lowered,
690                        )
691                        .with_span(terminator_span)?;
692                        self.check_call(
693                            infcx,
694                            env,
695                            terminator_span,
696                            Some(*resolved_id),
697                            fn_sig,
698                            &generic_args,
699                            &actuals,
700                        )?
701                        .output
702                    }
703                    mir::CallKind::FnPtr { operand, .. } => {
704                        let ty = self
705                            .check_operand(infcx, env, terminator_span, operand)
706                            .with_span(terminator_span)?;
707                        if let TyKind::Indexed(BaseTy::FnPtr(fn_sig), _) = infcx.unpack(&ty).kind()
708                        {
709                            self.check_call(
710                                infcx,
711                                env,
712                                terminator_span,
713                                None,
714                                EarlyBinder(fn_sig.clone()),
715                                &[],
716                                &actuals,
717                            )?
718                            .output
719                        } else {
720                            bug!("TODO: fnptr call {ty:?}")
721                        }
722                    }
723                };
724
725                let ret = infcx.unpack(&ret);
726                infcx.assume_invariants(&ret);
727
728                env.assign(&mut infcx.at(terminator_span), destination, ret)
729                    .with_span(terminator_span)?;
730
731                if let Some(target) = target {
732                    Ok(vec![(*target, Guard::None)])
733                } else {
734                    Ok(vec![])
735                }
736            }
737            TerminatorKind::Assert { cond, expected, target, msg } => {
738                Ok(vec![(
739                    *target,
740                    self.check_assert(infcx, env, terminator_span, cond, *expected, msg)
741                        .with_span(terminator_span)?,
742                )])
743            }
744            TerminatorKind::Drop { place, target, .. } => {
745                let _ = env.move_place(&mut infcx.at(terminator_span), place);
746                Ok(vec![(*target, Guard::None)])
747            }
748            TerminatorKind::FalseEdge { real_target, .. } => Ok(vec![(*real_target, Guard::None)]),
749            TerminatorKind::FalseUnwind { real_target, .. } => {
750                Ok(vec![(*real_target, Guard::None)])
751            }
752            TerminatorKind::UnwindResume => bug!("TODO: implement checking of cleanup code"),
753        }
754    }
755
756    fn check_ret(
757        &mut self,
758        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
759        env: &mut TypeEnv,
760        span: Span,
761    ) -> Result {
762        let obligations = infcx
763            .at(span)
764            .ensure_resolved_evars(|infcx| {
765                let ret_place_ty = env.lookup_place(infcx, Place::RETURN)?;
766                let output = self
767                    .output
768                    .replace_bound_refts_with(|sort, mode, _| infcx.fresh_infer_var(sort, mode));
769                let obligations = infcx.subtyping(&ret_place_ty, &output.ret, ConstrReason::Ret)?;
770
771                env.check_ensures(infcx, &output.ensures, ConstrReason::Ret)?;
772
773                Ok(obligations)
774            })
775            .with_span(span)?;
776
777        self.check_coroutine_obligations(infcx, obligations)
778    }
779
780    #[expect(clippy::too_many_arguments)]
781    fn check_call(
782        &mut self,
783        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
784        env: &mut TypeEnv,
785        span: Span,
786        callee_def_id: Option<DefId>,
787        fn_sig: EarlyBinder<PolyFnSig>,
788        generic_args: &[GenericArg],
789        actuals: &[Ty],
790    ) -> Result<ResolvedCall> {
791        let genv = self.genv;
792        let tcx = genv.tcx();
793
794        let actuals =
795            unfold_local_ptrs(infcx, env, fn_sig.skip_binder_ref(), actuals).with_span(span)?;
796        let actuals = infer_under_mut_ref_hack(infcx, &actuals, fn_sig.skip_binder_ref());
797        infcx.push_evar_scope();
798
799        // Replace holes in generic arguments with fresh inference variables
800        let generic_args = infcx.instantiate_generic_args(generic_args);
801
802        // Generate fresh inference variables for refinement arguments
803        let early_refine_args = match callee_def_id {
804            Some(callee_def_id) => {
805                infcx
806                    .instantiate_refine_args(callee_def_id, &generic_args)
807                    .with_span(span)?
808            }
809            None => rty::List::empty(),
810        };
811
812        let clauses = match callee_def_id {
813            Some(callee_def_id) => {
814                genv.predicates_of(callee_def_id)
815                    .with_span(span)?
816                    .predicates()
817                    .instantiate(tcx, &generic_args, &early_refine_args)
818            }
819            None => crate::rty::List::empty(),
820        };
821
822        let (clauses, fn_clauses) = Clause::split_off_fn_trait_clauses(self.genv, &clauses);
823        infcx
824            .at(span)
825            .check_non_closure_clauses(&clauses, ConstrReason::Call)
826            .with_span(span)?;
827
828        for fn_trait_pred in fn_clauses {
829            self.check_fn_trait_clause(infcx, &fn_trait_pred, span)?;
830        }
831
832        // Instantiate function signature and normalize it
833        let late_refine_args = vec![];
834        let fn_sig = fn_sig
835            .instantiate(tcx, &generic_args, &early_refine_args)
836            .replace_bound_vars(|_| rty::ReErased, |sort, mode| infcx.fresh_infer_var(sort, mode));
837
838        let fn_sig = fn_sig
839            .normalize_projections(&mut infcx.at(span))
840            .with_span(span)?;
841
842        let mut at = infcx.at(span);
843
844        // Check requires predicates
845        for requires in fn_sig.requires() {
846            at.check_pred(requires, ConstrReason::Call);
847        }
848
849        // Check arguments
850        for (actual, formal) in iter::zip(actuals, fn_sig.inputs()) {
851            at.subtyping_with_env(env, &actual, formal, ConstrReason::Call)
852                .with_span(span)?;
853        }
854
855        infcx.pop_evar_scope().with_span(span)?;
856        env.fully_resolve_evars(infcx);
857
858        let output = infcx
859            .fully_resolve_evars(&fn_sig.output)
860            .replace_bound_refts_with(|sort, _, _| Expr::fvar(infcx.define_var(sort)));
861
862        env.assume_ensures(infcx, &output.ensures, span);
863        fold_local_ptrs(infcx, env, span).with_span(span)?;
864
865        Ok(ResolvedCall {
866            output: output.ret,
867            _early_args: early_refine_args
868                .into_iter()
869                .map(|arg| infcx.fully_resolve_evars(arg))
870                .collect(),
871            _late_args: late_refine_args
872                .into_iter()
873                .map(|arg| infcx.fully_resolve_evars(&arg))
874                .collect(),
875        })
876    }
877
878    fn check_coroutine_obligations(
879        &mut self,
880        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
881        obligs: Vec<Binder<CoroutineObligPredicate>>,
882    ) -> Result {
883        for oblig in obligs {
884            // FIXME(nilehmann) we shouldn't be skipping this binder
885            let oblig = oblig.skip_binder();
886
887            #[expect(clippy::disallowed_methods, reason = "coroutines cannot be extern speced")]
888            let def_id = oblig.def_id.expect_local();
889            let span = self.genv.tcx().def_span(def_id);
890            let body = self.genv.mir(def_id).with_span(span)?;
891            Checker::run(
892                infcx.change_item(def_id, &body.infcx),
893                def_id,
894                self.inherited.reborrow(),
895                oblig.to_poly_fn_sig(),
896            )?;
897        }
898        Ok(())
899    }
900
901    fn find_self_ty_fn_sig(
902        &self,
903        self_ty: rustc_middle::ty::Ty<'tcx>,
904        span: Span,
905    ) -> Result<PolyFnSig> {
906        let tcx = self.genv.tcx();
907        let mut def_id = Some(self.def_id.to_def_id());
908        while let Some(did) = def_id {
909            let generic_predicates = self
910                .genv
911                .predicates_of(did)
912                .with_span(span)?
913                .instantiate_identity();
914            let predicates = generic_predicates.predicates;
915
916            for poly_fn_trait_pred in Clause::split_off_fn_trait_clauses(self.genv, &predicates).1 {
917                if poly_fn_trait_pred.skip_binder_ref().self_ty.to_rustc(tcx) == self_ty {
918                    return Ok(poly_fn_trait_pred.map(|fn_trait_pred| fn_trait_pred.fndef_sig()));
919                }
920            }
921            // Continue to the parent if we didn't find a match
922            def_id = generic_predicates.parent;
923        }
924
925        span_bug!(
926            span,
927            "cannot find self_ty_fn_sig for {:?} with self_ty = {self_ty:?}",
928            self.def_id
929        );
930    }
931
932    fn check_fn_trait_clause(
933        &mut self,
934        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
935        poly_fn_trait_pred: &Binder<FnTraitPredicate>,
936        span: Span,
937    ) -> Result {
938        let self_ty = poly_fn_trait_pred
939            .skip_binder_ref()
940            .self_ty
941            .as_bty_skipping_existentials();
942        let oblig_sig = poly_fn_trait_pred.map_ref(|fn_trait_pred| fn_trait_pred.fndef_sig());
943        match self_ty {
944            Some(BaseTy::Closure(def_id, _, _)) => {
945                let Some(poly_sig) = self.inherited.closures.get(def_id).cloned() else {
946                    span_bug!(span, "missing template for closure {def_id:?}");
947                };
948                check_fn_subtyping(infcx, SubFn::Mono(poly_sig.clone()), &oblig_sig, span)
949                    .with_span(span)?;
950            }
951            Some(BaseTy::FnDef(def_id, args)) => {
952                // Generates "function subtyping" obligations between the (super-type) `oblig_sig` in the `fn_trait_pred`
953                // and the (sub-type) corresponding to the signature of `def_id + args`.
954                // See `tests/neg/surface/fndef00.rs`
955                let sub_sig = self.genv.fn_sig(def_id).with_span(span)?;
956                check_fn_subtyping(
957                    infcx,
958                    SubFn::Poly(*def_id, sub_sig, args.clone()),
959                    &oblig_sig,
960                    span,
961                )
962                .with_span(span)?;
963            }
964            Some(BaseTy::FnPtr(sub_sig)) => {
965                check_fn_subtyping(infcx, SubFn::Mono(sub_sig.clone()), &oblig_sig, span)
966                    .with_span(span)?;
967            }
968
969            // Some(self_ty) => {
970            Some(self_ty @ BaseTy::Param(_)) => {
971                // Step 1. Find matching clause and turn it into a FnSig
972                let tcx = self.genv.tcx();
973                let self_ty = self_ty.to_rustc(tcx);
974                let sub_sig = self.find_self_ty_fn_sig(self_ty, span)?;
975                // Step 2. Issue the subtyping
976                check_fn_subtyping(infcx, SubFn::Mono(sub_sig), &oblig_sig, span)
977                    .with_span(span)?;
978            }
979            _ => {}
980        }
981        Ok(())
982    }
983
984    fn check_assert(
985        &mut self,
986        infcx: &mut InferCtxt,
987        env: &mut TypeEnv,
988        terminator_span: Span,
989        cond: &Operand,
990        expected: bool,
991        msg: &AssertKind,
992    ) -> InferResult<Guard> {
993        let ty = self.check_operand(infcx, env, terminator_span, cond)?;
994        let TyKind::Indexed(BaseTy::Bool, idx) = ty.kind() else {
995            tracked_span_bug!("unexpected ty `{ty:?}`");
996        };
997        let pred = if expected { idx.clone() } else { idx.not() };
998
999        let msg = match msg {
1000            AssertKind::DivisionByZero => "possible division by zero",
1001            AssertKind::BoundsCheck => "possible out-of-bounds access",
1002            AssertKind::RemainderByZero => "possible remainder with a divisor of zero",
1003            AssertKind::Overflow(mir::BinOp::Div) => "possible division with overflow",
1004            AssertKind::Overflow(mir::BinOp::Rem) => "possible reminder with overflow",
1005            AssertKind::Overflow(_) => return Ok(Guard::Pred(pred)),
1006        };
1007        infcx
1008            .at(terminator_span)
1009            .check_pred(&pred, ConstrReason::Assert(msg));
1010        Ok(Guard::Pred(pred))
1011    }
1012
1013    /// 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.
1014    /// See <https://github.com/flux-rs/flux/pull/840#discussion_r1786543174>
1015    fn check_if(discr_ty: &Ty, targets: &SwitchTargets) -> Vec<(BasicBlock, Guard)> {
1016        let mk = |bits| {
1017            match discr_ty.kind() {
1018                TyKind::Indexed(BaseTy::Bool, idx) => {
1019                    if bits == 0 {
1020                        idx.not()
1021                    } else {
1022                        idx.clone()
1023                    }
1024                }
1025                TyKind::Indexed(bty @ (BaseTy::Int(_) | BaseTy::Uint(_) | BaseTy::Char), idx) => {
1026                    Expr::eq(idx.clone(), Expr::from_bits(bty, bits))
1027                }
1028                _ => tracked_span_bug!("unexpected discr_ty {:?}", discr_ty),
1029            }
1030        };
1031
1032        let mut successors = vec![];
1033
1034        for (bits, bb) in targets.iter() {
1035            successors.push((bb, Guard::Pred(mk(bits))));
1036        }
1037        let otherwise = Expr::and_from_iter(targets.iter().map(|(bits, _)| mk(bits).not()));
1038        successors.push((targets.otherwise(), Guard::Pred(otherwise)));
1039
1040        successors
1041    }
1042
1043    fn check_match(discr_ty: &Ty, targets: &SwitchTargets) -> Vec<(BasicBlock, Guard)> {
1044        let (adt_def, place) = discr_ty.expect_discr();
1045
1046        let mut successors = vec![];
1047        let mut remaining: FxHashMap<u128, VariantIdx> = adt_def
1048            .discriminants()
1049            .map(|(idx, discr)| (discr, idx))
1050            .collect();
1051        for (bits, bb) in targets.iter() {
1052            let variant_idx = remaining
1053                .remove(&bits)
1054                .expect("value doesn't correspond to any variant");
1055            successors.push((bb, Guard::Match(place.clone(), variant_idx)));
1056        }
1057
1058        if remaining.len() == 1 {
1059            let (_, variant_idx) = remaining
1060                .into_iter()
1061                .next()
1062                .unwrap_or_else(|| tracked_span_bug!());
1063            successors.push((targets.otherwise(), Guard::Match(place.clone(), variant_idx)));
1064        } else {
1065            successors.push((targets.otherwise(), Guard::None));
1066        }
1067
1068        successors
1069    }
1070
1071    fn check_successors(
1072        &mut self,
1073        mut infcx: InferCtxt<'_, 'genv, 'tcx>,
1074        env: TypeEnv,
1075        from: BasicBlock,
1076        terminator_span: Span,
1077        successors: Vec<(BasicBlock, Guard)>,
1078    ) -> Result {
1079        for (target, guard) in successors {
1080            let mut infcx = infcx.branch();
1081            let mut env = env.clone();
1082            match guard {
1083                Guard::None => {}
1084                Guard::Pred(expr) => {
1085                    infcx.assume_pred(&expr);
1086                }
1087                Guard::Match(place, variant_idx) => {
1088                    env.downcast(&mut infcx.at(terminator_span), &place, variant_idx)
1089                        .with_span(terminator_span)?;
1090                }
1091            }
1092            self.check_ghost_statements_at(
1093                &mut infcx,
1094                &mut env,
1095                Point::Edge(from, target),
1096                terminator_span,
1097            )?;
1098            self.check_goto(infcx, env, terminator_span, target)?;
1099        }
1100        Ok(())
1101    }
1102
1103    fn check_goto(
1104        &mut self,
1105        mut infcx: InferCtxt<'_, 'genv, 'tcx>,
1106        mut env: TypeEnv,
1107        span: Span,
1108        target: BasicBlock,
1109    ) -> Result {
1110        if self.is_exit_block(target) {
1111            let location = self.body.terminator_loc(target);
1112            self.check_ghost_statements_at(
1113                &mut infcx,
1114                &mut env,
1115                Point::BeforeLocation(location),
1116                span,
1117            )?;
1118            self.check_ret(&mut infcx, &mut env, span)
1119        } else if self.body.is_join_point(target) {
1120            if M::check_goto_join_point(self, infcx, env, span, target)? {
1121                self.queue.insert(target);
1122            }
1123            Ok(())
1124        } else {
1125            self.check_basic_block(infcx, env, target)
1126        }
1127    }
1128
1129    fn closure_template(
1130        &mut self,
1131        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
1132        env: &mut TypeEnv,
1133        stmt_span: Span,
1134        args: &flux_rustc_bridge::ty::GenericArgs,
1135        operands: &[Operand],
1136    ) -> InferResult<(Vec<Ty>, PolyFnSig)> {
1137        let upvar_tys = self
1138            .check_operands(infcx, env, stmt_span, operands)?
1139            .into_iter()
1140            .map(|ty| {
1141                if let TyKind::Ptr(PtrKind::Mut(re), path) = ty.kind() {
1142                    env.ptr_to_ref(
1143                        &mut infcx.at(stmt_span),
1144                        ConstrReason::Other,
1145                        *re,
1146                        path,
1147                        PtrToRefBound::Infer,
1148                    )
1149                } else {
1150                    Ok(ty.clone())
1151                }
1152            })
1153            .try_collect_vec()?;
1154
1155        let closure_args = args.as_closure();
1156        let ty = closure_args.sig_as_fn_ptr_ty();
1157
1158        if let flux_rustc_bridge::ty::TyKind::FnPtr(poly_sig) = ty.kind() {
1159            let poly_sig = poly_sig.unpack_closure_sig();
1160            let poly_sig = self.refine_with_holes(&poly_sig)?;
1161            let poly_sig = poly_sig.hoist_input_binders();
1162            let poly_sig = poly_sig
1163                .replace_holes(|binders, kind| infcx.fresh_infer_var_for_hole(binders, kind));
1164
1165            Ok((upvar_tys, poly_sig))
1166        } else {
1167            bug!("check_rvalue: closure: expected fn_ptr ty, found {ty:?} in {args:?}");
1168        }
1169    }
1170
1171    fn check_closure_body(
1172        &mut self,
1173        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
1174        did: &DefId,
1175        upvar_tys: &[Ty],
1176        args: &flux_rustc_bridge::ty::GenericArgs,
1177        poly_sig: &PolyFnSig,
1178    ) -> Result {
1179        let genv = self.genv;
1180        let tcx = genv.tcx();
1181        #[expect(clippy::disallowed_methods, reason = "closures cannot be extern speced")]
1182        let closure_id = did.expect_local();
1183        let span = tcx.def_span(closure_id);
1184        let body = genv.mir(closure_id).with_span(span)?;
1185        let closure_sig = rty::to_closure_sig(tcx, closure_id, upvar_tys, args, poly_sig);
1186        Checker::run(
1187            infcx.change_item(closure_id, &body.infcx),
1188            closure_id,
1189            self.inherited.reborrow(),
1190            closure_sig,
1191        )
1192    }
1193
1194    fn check_rvalue_closure(
1195        &mut self,
1196        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
1197        env: &mut TypeEnv,
1198        stmt_span: Span,
1199        did: &DefId,
1200        args: &flux_rustc_bridge::ty::GenericArgs,
1201        operands: &[Operand],
1202    ) -> Result<Ty> {
1203        // (1) Create the closure template
1204        let (upvar_tys, poly_sig) = self
1205            .closure_template(infcx, env, stmt_span, args, operands)
1206            .with_span(stmt_span)?;
1207        // (2) Check the closure body against the template
1208        self.check_closure_body(infcx, did, &upvar_tys, args, &poly_sig)?;
1209        // (3) "Save" the closure type in the `closures` map
1210        self.inherited.closures.insert(*did, poly_sig);
1211        // (4) Return the closure type
1212        Ok(Ty::closure(*did, upvar_tys, args))
1213    }
1214
1215    fn check_rvalue(
1216        &mut self,
1217        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
1218        env: &mut TypeEnv,
1219        stmt_span: Span,
1220        rvalue: &Rvalue,
1221    ) -> Result<Ty> {
1222        let genv = self.genv;
1223        match rvalue {
1224            Rvalue::Use(operand) => {
1225                self.check_operand(infcx, env, stmt_span, operand)
1226                    .with_span(stmt_span)
1227            }
1228            Rvalue::Repeat(operand, c) => {
1229                let ty = self
1230                    .check_operand(infcx, env, stmt_span, operand)
1231                    .with_span(stmt_span)?;
1232                Ok(Ty::array(ty, c.clone()))
1233            }
1234            Rvalue::Ref(r, BorrowKind::Mut { .. }, place) => {
1235                env.borrow(&mut infcx.at(stmt_span), *r, Mutability::Mut, place)
1236                    .with_span(stmt_span)
1237            }
1238            Rvalue::Ref(r, BorrowKind::Shared | BorrowKind::Fake(..), place) => {
1239                env.borrow(&mut infcx.at(stmt_span), *r, Mutability::Not, place)
1240                    .with_span(stmt_span)
1241            }
1242
1243            Rvalue::RawPtr(mir::RawPtrKind::FakeForPtrMetadata, place) => {
1244                // see tests/tests/neg/surface/slice02.rs for what happens without unfolding here.
1245                env.unfold(infcx, place, stmt_span).with_span(stmt_span)?;
1246                let ty = env
1247                    .lookup_place(&mut infcx.at(stmt_span), place)
1248                    .with_span(stmt_span)?;
1249                let ty = BaseTy::RawPtrMetadata(ty).to_ty();
1250                Ok(ty)
1251            }
1252            Rvalue::RawPtr(kind, place) => {
1253                // ignore any refinements on the type stored at place
1254                let ty = &env.lookup_rust_ty(genv, place).with_span(stmt_span)?;
1255                let ty = self.refine_default(ty).with_span(stmt_span)?;
1256                let ty = BaseTy::RawPtr(ty, kind.to_mutbl_lossy()).to_ty();
1257                Ok(ty)
1258            }
1259            Rvalue::Cast(kind, op, to) => {
1260                let from = self
1261                    .check_operand(infcx, env, stmt_span, op)
1262                    .with_span(stmt_span)?;
1263                self.check_cast(infcx, env, stmt_span, *kind, &from, to)
1264                    .with_span(stmt_span)
1265            }
1266            Rvalue::BinaryOp(bin_op, op1, op2) => {
1267                self.check_binary_op(infcx, env, stmt_span, *bin_op, op1, op2)
1268                    .with_span(stmt_span)
1269            }
1270            Rvalue::NullaryOp(null_op, ty) => Ok(self.check_nullary_op(*null_op, ty)),
1271            Rvalue::Len(place) => self.check_len(infcx, env, stmt_span, place),
1272            Rvalue::UnaryOp(UnOp::PtrMetadata, Operand::Copy(place))
1273            | Rvalue::UnaryOp(UnOp::PtrMetadata, Operand::Move(place)) => {
1274                self.check_raw_ptr_metadata(infcx, env, stmt_span, place)
1275            }
1276            Rvalue::UnaryOp(un_op, op) => {
1277                self.check_unary_op(infcx, env, stmt_span, *un_op, op)
1278                    .with_span(stmt_span)
1279            }
1280            Rvalue::Discriminant(place) => {
1281                let ty = env
1282                    .lookup_place(&mut infcx.at(stmt_span), place)
1283                    .with_span(stmt_span)?;
1284                // HACK(nilehmann, mut-ref-unfolding) place should be unfolded here.
1285                let (adt_def, ..) = ty
1286                    .as_bty_skipping_existentials()
1287                    .unwrap_or_else(|| tracked_span_bug!())
1288                    .expect_adt();
1289                Ok(Ty::discr(adt_def.clone(), place.clone()))
1290            }
1291            Rvalue::Aggregate(
1292                AggregateKind::Adt(def_id, variant_idx, args, _, field_idx),
1293                operands,
1294            ) => {
1295                let actuals = self
1296                    .check_operands(infcx, env, stmt_span, operands)
1297                    .with_span(stmt_span)?;
1298                let sig = genv
1299                    .variant_sig(*def_id, *variant_idx)
1300                    .with_span(stmt_span)?
1301                    .ok_or_query_err(*def_id)
1302                    .with_span(stmt_span)?
1303                    .to_poly_fn_sig(*field_idx);
1304
1305                let args =
1306                    instantiate_args_for_constructor(genv, self.def_id.to_def_id(), *def_id, args)
1307                        .with_span(stmt_span)?;
1308                self.check_call(infcx, env, stmt_span, Some(*def_id), sig, &args, &actuals)
1309                    .map(|resolved_call| resolved_call.output)
1310            }
1311            Rvalue::Aggregate(AggregateKind::Array(arr_ty), operands) => {
1312                let args = self
1313                    .check_operands(infcx, env, stmt_span, operands)
1314                    .with_span(stmt_span)?;
1315                let arr_ty = self.refine_with_holes(arr_ty).with_span(stmt_span)?;
1316                self.check_mk_array(infcx, env, stmt_span, &args, arr_ty)
1317                    .with_span(stmt_span)
1318            }
1319            Rvalue::Aggregate(AggregateKind::Tuple, args) => {
1320                let tys = self
1321                    .check_operands(infcx, env, stmt_span, args)
1322                    .with_span(stmt_span)?;
1323                Ok(Ty::tuple(tys))
1324            }
1325            Rvalue::Aggregate(AggregateKind::Closure(did, args), operands) => {
1326                self.check_rvalue_closure(infcx, env, stmt_span, did, args, operands)
1327            }
1328            Rvalue::Aggregate(AggregateKind::Coroutine(did, args), ops) => {
1329                let args = args.as_coroutine();
1330                let resume_ty = self.refine_default(args.resume_ty()).with_span(stmt_span)?;
1331                let upvar_tys = self
1332                    .check_operands(infcx, env, stmt_span, ops)
1333                    .with_span(stmt_span)?;
1334                Ok(Ty::coroutine(*did, resume_ty, upvar_tys.into()))
1335            }
1336            Rvalue::ShallowInitBox(operand, _) => {
1337                self.check_operand(infcx, env, stmt_span, operand)
1338                    .with_span(stmt_span)?;
1339                Ty::mk_box_with_default_alloc(self.genv, Ty::uninit()).with_span(stmt_span)
1340            }
1341        }
1342    }
1343
1344    fn check_raw_ptr_metadata(
1345        &mut self,
1346        infcx: &mut InferCtxt,
1347        env: &mut TypeEnv,
1348        stmt_span: Span,
1349        place: &Place,
1350    ) -> Result<Ty> {
1351        let ty = env
1352            .lookup_place(&mut infcx.at(stmt_span), place)
1353            .with_span(stmt_span)?;
1354        let ty = match ty.kind() {
1355            TyKind::Indexed(BaseTy::RawPtrMetadata(ty), _)
1356            | TyKind::Indexed(BaseTy::Ref(_, ty, _), _) => ty,
1357            _ => tracked_span_bug!("check_metadata: bug! unexpected type `{ty:?}`"),
1358        };
1359        match ty.kind() {
1360            TyKind::Indexed(BaseTy::Array(_, len), _) => {
1361                let idx = Expr::from_const(self.genv.tcx(), len);
1362                Ok(Ty::indexed(BaseTy::Uint(UintTy::Usize), idx))
1363            }
1364            TyKind::Indexed(BaseTy::Slice(_), len) => {
1365                Ok(Ty::indexed(BaseTy::Uint(UintTy::Usize), len.clone()))
1366            }
1367            _ => Ok(Ty::unit()),
1368        }
1369    }
1370
1371    fn check_len(
1372        &mut self,
1373        infcx: &mut InferCtxt,
1374        env: &mut TypeEnv,
1375        stmt_span: Span,
1376        place: &Place,
1377    ) -> Result<Ty> {
1378        let ty = env
1379            .lookup_place(&mut infcx.at(stmt_span), place)
1380            .with_span(stmt_span)?;
1381
1382        let idx = match ty.kind() {
1383            TyKind::Indexed(BaseTy::Array(_, len), _) => Expr::from_const(self.genv.tcx(), len),
1384            TyKind::Indexed(BaseTy::Slice(_), idx) => idx.clone(),
1385            _ => tracked_span_bug!("check_len: expected array or slice type found  `{ty:?}`"),
1386        };
1387
1388        Ok(Ty::indexed(BaseTy::Uint(UintTy::Usize), idx))
1389    }
1390
1391    fn check_binary_op(
1392        &mut self,
1393        infcx: &mut InferCtxt,
1394        env: &mut TypeEnv,
1395        stmt_span: Span,
1396        bin_op: mir::BinOp,
1397        op1: &Operand,
1398        op2: &Operand,
1399    ) -> InferResult<Ty> {
1400        let ty1 = self.check_operand(infcx, env, stmt_span, op1)?;
1401        let ty2 = self.check_operand(infcx, env, stmt_span, op2)?;
1402
1403        match (ty1.kind(), ty2.kind()) {
1404            (TyKind::Indexed(bty1, idx1), TyKind::Indexed(bty2, idx2)) => {
1405                let rule =
1406                    primops::match_bin_op(bin_op, bty1, idx1, bty2, idx2, infcx.check_overflow);
1407                if let Some(pre) = rule.precondition {
1408                    infcx.at(stmt_span).check_pred(pre.pred, pre.reason);
1409                }
1410
1411                Ok(rule.output_type)
1412            }
1413            _ => tracked_span_bug!("incompatible types: `{ty1:?}` `{ty2:?}`"),
1414        }
1415    }
1416
1417    fn check_nullary_op(&self, null_op: mir::NullOp, _ty: &ty::Ty) -> Ty {
1418        match null_op {
1419            mir::NullOp::SizeOf | mir::NullOp::AlignOf => {
1420                // We could try to get the layout of type to index this with the actual value, but
1421                // this enough for now. Revisit if we ever need the precision.
1422                Ty::uint(UintTy::Usize)
1423            }
1424        }
1425    }
1426
1427    fn check_unary_op(
1428        &mut self,
1429        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
1430        env: &mut TypeEnv,
1431        stmt_span: Span,
1432        un_op: mir::UnOp,
1433        op: &Operand,
1434    ) -> InferResult<Ty> {
1435        let ty = self.check_operand(infcx, env, stmt_span, op)?;
1436        match ty.kind() {
1437            TyKind::Indexed(bty, idx) => {
1438                let rule = primops::match_un_op(un_op, bty, idx, infcx.check_overflow);
1439                if let Some(pre) = rule.precondition {
1440                    infcx.at(stmt_span).check_pred(pre.pred, pre.reason);
1441                }
1442                Ok(rule.output_type)
1443            }
1444            _ => tracked_span_bug!("invalid type for unary operator `{un_op:?}` `{ty:?}`"),
1445        }
1446    }
1447
1448    fn check_mk_array(
1449        &mut self,
1450        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
1451        env: &mut TypeEnv,
1452        stmt_span: Span,
1453        args: &[Ty],
1454        arr_ty: Ty,
1455    ) -> InferResult<Ty> {
1456        let arr_ty = infcx.ensure_resolved_evars(|infcx| {
1457            let arr_ty =
1458                arr_ty.replace_holes(|binders, kind| infcx.fresh_infer_var_for_hole(binders, kind));
1459
1460            let (arr_ty, pred) = arr_ty.unconstr();
1461            let mut at = infcx.at(stmt_span);
1462            at.check_pred(&pred, ConstrReason::Other);
1463            for ty in args {
1464                at.subtyping_with_env(env, ty, &arr_ty, ConstrReason::Other)?;
1465            }
1466            Ok(arr_ty)
1467        })?;
1468        let arr_ty = infcx.fully_resolve_evars(&arr_ty);
1469
1470        Ok(Ty::array(arr_ty, rty::Const::from_usize(self.genv.tcx(), args.len())))
1471    }
1472
1473    fn check_cast(
1474        &self,
1475        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
1476        env: &mut TypeEnv,
1477        stmt_span: Span,
1478        kind: CastKind,
1479        from: &Ty,
1480        to: &ty::Ty,
1481    ) -> InferResult<Ty> {
1482        use ty::TyKind as RustTy;
1483        let ty = match kind {
1484            CastKind::PointerExposeProvenance => {
1485                match to.kind() {
1486                    RustTy::Int(int_ty) => Ty::int(*int_ty),
1487                    RustTy::Uint(uint_ty) => Ty::uint(*uint_ty),
1488                    _ => tracked_span_bug!("unsupported PointerExposeProvenance cast"),
1489                }
1490            }
1491            CastKind::IntToInt => {
1492                match (from.kind(), to.kind()) {
1493                    (Bool!(idx), RustTy::Int(int_ty)) => bool_int_cast(idx, *int_ty),
1494                    (Bool!(idx), RustTy::Uint(uint_ty)) => bool_uint_cast(idx, *uint_ty),
1495                    (Int!(int_ty1, idx), RustTy::Int(int_ty2)) => {
1496                        int_int_cast(idx, *int_ty1, *int_ty2)
1497                    }
1498                    (Uint!(uint_ty1, idx), RustTy::Uint(uint_ty2)) => {
1499                        uint_uint_cast(idx, *uint_ty1, *uint_ty2)
1500                    }
1501                    (Uint!(uint_ty, idx), RustTy::Int(int_ty)) => {
1502                        uint_int_cast(idx, *uint_ty, *int_ty)
1503                    }
1504                    (Int!(_, _), RustTy::Uint(uint_ty)) => Ty::uint(*uint_ty),
1505                    (TyKind::Discr(adt_def, _), RustTy::Int(int_ty)) => {
1506                        Self::discr_to_int_cast(adt_def, BaseTy::Int(*int_ty))
1507                    }
1508                    (TyKind::Discr(adt_def, _place), RustTy::Uint(uint_ty)) => {
1509                        Self::discr_to_int_cast(adt_def, BaseTy::Uint(*uint_ty))
1510                    }
1511                    (Char!(idx), RustTy::Uint(uint_ty)) => char_uint_cast(idx, *uint_ty),
1512                    (Uint!(_, idx), RustTy::Char) => uint_char_cast(idx),
1513                    _ => {
1514                        tracked_span_bug!("invalid int to int cast {from:?} --> {to:?}")
1515                    }
1516                }
1517            }
1518            CastKind::PointerCoercion(mir::PointerCast::Unsize) => {
1519                self.check_unsize_cast(infcx, env, stmt_span, from, to)?
1520            }
1521            CastKind::FloatToInt
1522            | CastKind::IntToFloat
1523            | CastKind::PtrToPtr
1524            | CastKind::PointerCoercion(mir::PointerCast::MutToConstPointer)
1525            | CastKind::PointerCoercion(mir::PointerCast::ClosureFnPointer)
1526            | CastKind::PointerWithExposedProvenance => self.refine_default(to)?,
1527            CastKind::PointerCoercion(mir::PointerCast::ReifyFnPointer) => {
1528                let to = self.refine_default(to)?;
1529                if let TyKind::Indexed(rty::BaseTy::FnDef(def_id, args), _) = from.kind()
1530                    && let TyKind::Indexed(BaseTy::FnPtr(super_sig), _) = to.kind()
1531                {
1532                    let current_did = infcx.def_id;
1533                    let sub_sig =
1534                        SubFn::Poly(current_did, infcx.genv.fn_sig(*def_id)?, args.clone());
1535                    // TODO:CLOSURE:2 TODO(RJ) dicey maneuver? assumes that sig_b is unrefined?
1536                    check_fn_subtyping(infcx, sub_sig, super_sig, stmt_span)?;
1537                    to
1538                } else {
1539                    tracked_span_bug!("invalid cast from `{from:?}` to `{to:?}`")
1540                }
1541            }
1542        };
1543        Ok(ty)
1544    }
1545
1546    fn discr_to_int_cast(adt_def: &AdtDef, bty: BaseTy) -> Ty {
1547        // TODO: This could be a giant disjunction, maybe better (if less precise) to use the interval?
1548        let vals = adt_def
1549            .discriminants()
1550            .map(|(_, idx)| Expr::eq(Expr::nu(), Expr::from_bits(&bty, idx)))
1551            .collect_vec();
1552        Ty::exists_with_constr(bty, Expr::or_from_iter(vals))
1553    }
1554
1555    fn check_unsize_cast(
1556        &self,
1557        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
1558        env: &mut TypeEnv,
1559        span: Span,
1560        src: &Ty,
1561        dst: &ty::Ty,
1562    ) -> InferResult<Ty> {
1563        // Convert `ptr` to `&mut`
1564        let src = if let TyKind::Ptr(PtrKind::Mut(re), path) = src.kind() {
1565            env.ptr_to_ref(
1566                &mut infcx.at(span),
1567                ConstrReason::Other,
1568                *re,
1569                path,
1570                PtrToRefBound::Identity,
1571            )?
1572        } else {
1573            src.clone()
1574        };
1575
1576        if let ty::TyKind::Ref(_, deref_ty, _) = dst.kind()
1577            && let ty::TyKind::Dynamic(..) = deref_ty.kind()
1578        {
1579            return Ok(self.refine_default(dst)?);
1580        }
1581
1582        // `&mut [T; n] -> &mut [T]` or `&[T; n] -> &[T]`
1583        if let TyKind::Indexed(BaseTy::Ref(_, deref_ty, _), _) = src.kind()
1584            && let TyKind::Indexed(BaseTy::Array(arr_ty, arr_len), _) = deref_ty.kind()
1585            && let ty::TyKind::Ref(re, _, mutbl) = dst.kind()
1586        {
1587            let idx = Expr::from_const(self.genv.tcx(), arr_len);
1588            Ok(Ty::mk_ref(*re, Ty::indexed(BaseTy::Slice(arr_ty.clone()), idx), *mutbl))
1589
1590        // `Box<[T; n]> -> Box<[T]>`
1591        } else if let TyKind::Indexed(BaseTy::Adt(adt_def, args), _) = src.kind()
1592            && adt_def.is_box()
1593            && let (deref_ty, alloc_ty) = args.box_args()
1594            && let TyKind::Indexed(BaseTy::Array(arr_ty, arr_len), _) = deref_ty.kind()
1595        {
1596            let idx = Expr::from_const(self.genv.tcx(), arr_len);
1597            Ok(Ty::mk_box(
1598                self.genv,
1599                Ty::indexed(BaseTy::Slice(arr_ty.clone()), idx),
1600                alloc_ty.clone(),
1601            )?)
1602        } else {
1603            Err(query_bug!("unsupported unsize cast from `{src:?}` to `{dst:?}`"))?
1604        }
1605    }
1606
1607    fn check_operands(
1608        &mut self,
1609        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
1610        env: &mut TypeEnv,
1611        span: Span,
1612        operands: &[Operand],
1613    ) -> InferResult<Vec<Ty>> {
1614        operands
1615            .iter()
1616            .map(|op| self.check_operand(infcx, env, span, op))
1617            .try_collect()
1618    }
1619
1620    fn check_operand(
1621        &mut self,
1622        infcx: &mut InferCtxt,
1623        env: &mut TypeEnv,
1624        span: Span,
1625        operand: &Operand,
1626    ) -> InferResult<Ty> {
1627        let ty = match operand {
1628            Operand::Copy(p) => env.lookup_place(&mut infcx.at(span), p)?,
1629            Operand::Move(p) => env.move_place(&mut infcx.at(span), p)?,
1630            Operand::Constant(c) => self.check_constant(c)?,
1631        };
1632        Ok(infcx.hoister(true).hoist(&ty))
1633    }
1634
1635    fn check_constant(&mut self, c: &Constant) -> QueryResult<Ty> {
1636        match c {
1637            Constant::Int(n, int_ty) => {
1638                let idx = Expr::constant(rty::Constant::from(*n));
1639                Ok(Ty::indexed(BaseTy::Int(*int_ty), idx))
1640            }
1641            Constant::Uint(n, uint_ty) => {
1642                let idx = Expr::constant(rty::Constant::from(*n));
1643                Ok(Ty::indexed(BaseTy::Uint(*uint_ty), idx))
1644            }
1645            Constant::Bool(b) => {
1646                let idx = Expr::constant(rty::Constant::from(*b));
1647                Ok(Ty::indexed(BaseTy::Bool, idx))
1648            }
1649            Constant::Float(_, float_ty) => Ok(Ty::float(*float_ty)),
1650            Constant::Unit => Ok(Ty::unit()),
1651            Constant::Str(s) => {
1652                let idx = Expr::constant(rty::Constant::from(*s));
1653                Ok(Ty::mk_ref(ReStatic, Ty::indexed(BaseTy::Str, idx), Mutability::Not))
1654            }
1655            Constant::Char(c) => {
1656                let idx = Expr::constant(rty::Constant::from(*c));
1657                Ok(Ty::indexed(BaseTy::Char, idx))
1658            }
1659            Constant::Param(param_const, ty) => {
1660                let idx = Expr::const_generic(*param_const);
1661                let ctor = self.default_refiner.refine_ty_or_base(ty)?.expect_base();
1662                Ok(ctor.replace_bound_reft(&idx).to_ty())
1663            }
1664            Constant::Opaque(ty) => self.refine_default(ty),
1665            Constant::Unevaluated(ty, def_id) => {
1666                let ty = self.refine_default(ty)?;
1667                let info = self.genv.constant_info(def_id)?;
1668                if let Some(bty) = ty.as_bty_skipping_existentials()
1669                    && let rty::ConstantInfo::Interpreted(idx, _) = info
1670                {
1671                    Ok(Ty::indexed(bty.clone(), idx))
1672                } else {
1673                    Ok(ty)
1674                }
1675            }
1676        }
1677    }
1678
1679    fn check_ghost_statements_at(
1680        &mut self,
1681        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
1682        env: &mut TypeEnv,
1683        point: Point,
1684        span: Span,
1685    ) -> Result {
1686        bug::track_span(span, || {
1687            for stmt in self.ghost_stmts().statements_at(point) {
1688                self.check_ghost_statement(infcx, env, stmt, span)
1689                    .with_span(span)?;
1690            }
1691            Ok(())
1692        })
1693    }
1694
1695    fn check_ghost_statement(
1696        &mut self,
1697        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
1698        env: &mut TypeEnv,
1699        stmt: &GhostStatement,
1700        span: Span,
1701    ) -> InferResult {
1702        dbg::statement!("start", stmt, infcx, env, span, &self);
1703        match stmt {
1704            GhostStatement::Fold(place) => {
1705                env.fold(&mut infcx.at(span), place)?;
1706            }
1707            GhostStatement::Unfold(place) => {
1708                env.unfold(infcx, place, span)?;
1709            }
1710            GhostStatement::Unblock(place) => env.unblock(infcx, place),
1711            GhostStatement::PtrToRef(place) => {
1712                env.ptr_to_ref_at_place(&mut infcx.at(span), place)?;
1713            }
1714        }
1715        dbg::statement!("end", stmt, infcx, env, span, &self);
1716        Ok(())
1717    }
1718
1719    #[track_caller]
1720    fn marker_at_dominator(&self, bb: BasicBlock) -> &Marker {
1721        marker_at_dominator(self.body, &self.markers, bb)
1722    }
1723
1724    fn dominators(&self) -> &'ck Dominators<BasicBlock> {
1725        self.body.dominators()
1726    }
1727
1728    fn ghost_stmts(&self) -> &'ck GhostStatements {
1729        &self.inherited.ghost_stmts[&self.def_id]
1730    }
1731
1732    fn refine_default<T: Refine>(&self, ty: &T) -> QueryResult<T::Output> {
1733        ty.refine(&self.default_refiner)
1734    }
1735
1736    fn refine_with_holes<T: Refine>(&self, ty: &T) -> QueryResult<<T as Refine>::Output> {
1737        ty.refine(&Refiner::with_holes(self.genv, self.def_id.to_def_id())?)
1738    }
1739}
1740
1741fn instantiate_args_for_fun_call(
1742    genv: GlobalEnv,
1743    caller_id: DefId,
1744    callee_id: DefId,
1745    args: &ty::GenericArgs,
1746) -> QueryResult<Vec<rty::GenericArg>> {
1747    let params_in_clauses = collect_params_in_clauses(genv, callee_id);
1748
1749    let hole_refiner = Refiner::new_for_item(genv, caller_id, |bty| {
1750        let sort = bty.sort();
1751        let bty = bty.shift_in_escaping(1);
1752        let constr = if !sort.is_unit() {
1753            rty::SubsetTy::new(bty, Expr::nu(), Expr::hole(rty::HoleKind::Pred))
1754        } else {
1755            rty::SubsetTy::trivial(bty, Expr::nu())
1756        };
1757        Binder::bind_with_sort(constr, sort)
1758    })?;
1759    let default_refiner = Refiner::default_for_item(genv, caller_id)?;
1760
1761    let callee_generics = genv.generics_of(callee_id)?;
1762    args.iter()
1763        .enumerate()
1764        .map(|(idx, arg)| {
1765            let param = callee_generics.param_at(idx, genv)?;
1766            let refiner =
1767                if params_in_clauses.contains(&idx) { &default_refiner } else { &hole_refiner };
1768            refiner.refine_generic_arg(&param, arg)
1769        })
1770        .collect()
1771}
1772
1773fn instantiate_args_for_constructor(
1774    genv: GlobalEnv,
1775    caller_id: DefId,
1776    adt_id: DefId,
1777    args: &ty::GenericArgs,
1778) -> QueryResult<Vec<rty::GenericArg>> {
1779    let params_in_clauses = collect_params_in_clauses(genv, adt_id);
1780
1781    let adt_generics = genv.generics_of(adt_id)?;
1782    let hole_refiner = Refiner::with_holes(genv, caller_id)?;
1783    let default_refiner = Refiner::default_for_item(genv, caller_id)?;
1784    args.iter()
1785        .enumerate()
1786        .map(|(idx, arg)| {
1787            let param = adt_generics.param_at(idx, genv)?;
1788            let refiner =
1789                if params_in_clauses.contains(&idx) { &default_refiner } else { &hole_refiner };
1790            refiner.refine_generic_arg(&param, arg)
1791        })
1792        .collect()
1793}
1794
1795fn collect_params_in_clauses(genv: GlobalEnv, def_id: DefId) -> FxHashSet<usize> {
1796    let tcx = genv.tcx();
1797    struct Collector {
1798        params: FxHashSet<usize>,
1799    }
1800
1801    impl rustc_middle::ty::TypeVisitor<TyCtxt<'_>> for Collector {
1802        fn visit_ty(&mut self, t: rustc_middle::ty::Ty) {
1803            if let rustc_middle::ty::Param(param_ty) = t.kind() {
1804                self.params.insert(param_ty.index as usize);
1805            }
1806            t.super_visit_with(self);
1807        }
1808    }
1809    let mut vis = Collector { params: Default::default() };
1810
1811    let span = genv.tcx().def_span(def_id);
1812    for (clause, _) in all_predicates_of(tcx, def_id) {
1813        if let Some(trait_pred) = clause.as_trait_clause() {
1814            let trait_id = trait_pred.def_id();
1815            if tcx.require_lang_item(LangItem::Sized, span) == trait_id {
1816                continue;
1817            }
1818            if tcx.require_lang_item(LangItem::Tuple, span) == trait_id {
1819                continue;
1820            }
1821            if tcx.require_lang_item(LangItem::Copy, span) == trait_id {
1822                continue;
1823            }
1824
1825            if tcx.fn_trait_kind_from_def_id(trait_id).is_some() {
1826                continue;
1827            }
1828            if tcx.get_diagnostic_item(sym::Hash) == Some(trait_id) {
1829                continue;
1830            }
1831            if tcx.get_diagnostic_item(sym::Eq) == Some(trait_id) {
1832                continue;
1833            }
1834        }
1835        if let Some(proj_pred) = clause.as_projection_clause() {
1836            let assoc_id = proj_pred.item_def_id();
1837            if genv.is_fn_output(assoc_id) {
1838                continue;
1839            }
1840        }
1841        if let Some(outlives_pred) = clause.as_type_outlives_clause() {
1842            // We skip outlives bounds if they are not 'static. A 'static bound means the type
1843            // implements `Any` which makes it unsound to instantiate the argument with refinements.
1844            if outlives_pred.skip_binder().1 != tcx.lifetimes.re_static {
1845                continue;
1846            }
1847        }
1848        clause.visit_with(&mut vis);
1849    }
1850    vis.params
1851}
1852
1853fn all_predicates_of(
1854    tcx: TyCtxt<'_>,
1855    id: DefId,
1856) -> impl Iterator<Item = &(rustc_middle::ty::Clause<'_>, Span)> {
1857    let mut next_id = Some(id);
1858    iter::from_fn(move || {
1859        next_id.take().map(|id| {
1860            let preds = tcx.predicates_of(id);
1861            next_id = preds.parent;
1862            preds.predicates.iter()
1863        })
1864    })
1865    .flatten()
1866}
1867
1868struct SkipConstr;
1869
1870impl TypeFolder for SkipConstr {
1871    fn fold_ty(&mut self, ty: &rty::Ty) -> rty::Ty {
1872        if let rty::TyKind::Constr(_, inner_ty) = ty.kind() {
1873            inner_ty.fold_with(self)
1874        } else {
1875            ty.super_fold_with(self)
1876        }
1877    }
1878}
1879
1880fn is_indexed_mut_skipping_constr(ty: &Ty) -> bool {
1881    let ty = SkipConstr.fold_ty(ty);
1882    if let rty::Ref!(_, inner_ty, Mutability::Mut) = ty.kind()
1883        && let TyKind::Indexed(..) = inner_ty.kind()
1884    {
1885        true
1886    } else {
1887        false
1888    }
1889}
1890
1891/// HACK(nilehmann) This let us infer parameters under mutable references for the simple case
1892/// where the formal argument is of the form `&mut B[@n]`, e.g., the type of the first argument
1893/// to `RVec::get_mut` is `&mut RVec<T>[@n]`. We should remove this after we implement opening of
1894/// mutable references.
1895fn infer_under_mut_ref_hack(rcx: &mut InferCtxt, actuals: &[Ty], fn_sig: &PolyFnSig) -> Vec<Ty> {
1896    iter::zip(actuals, fn_sig.skip_binder_ref().inputs())
1897        .map(|(actual, formal)| {
1898            if let rty::Ref!(re, deref_ty, Mutability::Mut) = actual.kind()
1899                && is_indexed_mut_skipping_constr(formal)
1900            {
1901                rty::Ty::mk_ref(*re, rcx.unpack(deref_ty), Mutability::Mut)
1902            } else {
1903                actual.clone()
1904            }
1905        })
1906        .collect()
1907}
1908
1909impl Mode for ShapeMode {
1910    const NAME: &str = "shape";
1911
1912    fn enter_basic_block<'ck, 'genv, 'tcx>(
1913        ck: &mut Checker<'ck, 'genv, 'tcx, ShapeMode>,
1914        _infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
1915        bb: BasicBlock,
1916    ) -> TypeEnv<'ck> {
1917        ck.inherited.mode.bb_envs[&ck.def_id][&bb].enter(&ck.body.local_decls)
1918    }
1919
1920    fn check_goto_join_point<'genv, 'tcx>(
1921        ck: &mut Checker<'_, 'genv, 'tcx, ShapeMode>,
1922        _: InferCtxt<'_, 'genv, 'tcx>,
1923        env: TypeEnv,
1924        span: Span,
1925        target: BasicBlock,
1926    ) -> Result<bool> {
1927        let bb_envs = &mut ck.inherited.mode.bb_envs;
1928        let target_bb_env = bb_envs.entry(ck.def_id).or_default().get(&target);
1929        dbg::shape_goto_enter!(target, env, target_bb_env);
1930
1931        let modified = match bb_envs.entry(ck.def_id).or_default().entry(target) {
1932            Entry::Occupied(mut entry) => entry.get_mut().join(env, span),
1933            Entry::Vacant(entry) => {
1934                let scope = marker_at_dominator(ck.body, &ck.markers, target)
1935                    .scope()
1936                    .unwrap_or_else(|| tracked_span_bug!());
1937                entry.insert(env.into_infer(scope));
1938                true
1939            }
1940        };
1941
1942        dbg::shape_goto_exit!(target, bb_envs[&ck.def_id].get(&target));
1943        Ok(modified)
1944    }
1945
1946    fn clear(ck: &mut Checker<ShapeMode>, root: BasicBlock) {
1947        ck.visited.remove(root);
1948        for bb in ck.body.basic_blocks.indices() {
1949            if bb != root && ck.dominators().dominates(root, bb) {
1950                ck.inherited
1951                    .mode
1952                    .bb_envs
1953                    .entry(ck.def_id)
1954                    .or_default()
1955                    .remove(&bb);
1956                ck.visited.remove(bb);
1957            }
1958        }
1959    }
1960}
1961
1962impl Mode for RefineMode {
1963    const NAME: &str = "refine";
1964
1965    fn enter_basic_block<'ck, 'genv, 'tcx>(
1966        ck: &mut Checker<'ck, 'genv, 'tcx, RefineMode>,
1967        infcx: &mut InferCtxt<'_, 'genv, 'tcx>,
1968        bb: BasicBlock,
1969    ) -> TypeEnv<'ck> {
1970        ck.inherited.mode.bb_envs[&ck.def_id][&bb].enter(infcx, &ck.body.local_decls)
1971    }
1972
1973    fn check_goto_join_point(
1974        ck: &mut Checker<RefineMode>,
1975        mut infcx: InferCtxt,
1976        env: TypeEnv,
1977        terminator_span: Span,
1978        target: BasicBlock,
1979    ) -> Result<bool> {
1980        let bb_env = &ck.inherited.mode.bb_envs[&ck.def_id][&target];
1981        tracked_span_dbg_assert_eq!(
1982            &ck.marker_at_dominator(target)
1983                .scope()
1984                .unwrap_or_else(|| tracked_span_bug!()),
1985            bb_env.scope()
1986        );
1987
1988        dbg::refine_goto!(target, infcx, env, bb_env);
1989
1990        env.check_goto(&mut infcx.at(terminator_span), bb_env, target)
1991            .with_span(terminator_span)?;
1992
1993        Ok(!ck.visited.contains(target))
1994    }
1995
1996    fn clear(_ck: &mut Checker<RefineMode>, _bb: BasicBlock) {
1997        bug!();
1998    }
1999}
2000
2001fn bool_int_cast(b: &Expr, int_ty: IntTy) -> Ty {
2002    let idx = Expr::ite(b, 1, 0);
2003    Ty::indexed(BaseTy::Int(int_ty), idx)
2004}
2005
2006fn uint_char_cast(idx: &Expr) -> Ty {
2007    let idx = Expr::app(
2008        rty::Expr::internal_func(InternalFuncKind::IntToChar),
2009        rty::List::singleton(idx.clone()),
2010    );
2011    Ty::indexed(BaseTy::Char, idx)
2012}
2013
2014fn char_uint_cast(idx: &Expr, uint_ty: UintTy) -> Ty {
2015    let idx = Expr::app(
2016        Expr::internal_func(InternalFuncKind::IntToChar),
2017        rty::List::singleton(idx.clone()),
2018    );
2019    Ty::indexed(BaseTy::Uint(uint_ty), idx)
2020}
2021
2022fn bool_uint_cast(b: &Expr, uint_ty: UintTy) -> Ty {
2023    let idx = Expr::ite(b, 1, 0);
2024    Ty::indexed(BaseTy::Uint(uint_ty), idx)
2025}
2026
2027fn int_int_cast(idx: &Expr, int_ty1: IntTy, int_ty2: IntTy) -> Ty {
2028    if int_bit_width(int_ty1) <= int_bit_width(int_ty2) {
2029        Ty::indexed(BaseTy::Int(int_ty2), idx.clone())
2030    } else {
2031        Ty::int(int_ty2)
2032    }
2033}
2034
2035fn uint_int_cast(idx: &Expr, uint_ty: UintTy, int_ty: IntTy) -> Ty {
2036    if uint_bit_width(uint_ty) < int_bit_width(int_ty) {
2037        Ty::indexed(BaseTy::Int(int_ty), idx.clone())
2038    } else {
2039        Ty::int(int_ty)
2040    }
2041}
2042
2043fn uint_uint_cast(idx: &Expr, uint_ty1: UintTy, uint_ty2: UintTy) -> Ty {
2044    if uint_bit_width(uint_ty1) <= uint_bit_width(uint_ty2) {
2045        Ty::indexed(BaseTy::Uint(uint_ty2), idx.clone())
2046    } else {
2047        Ty::uint(uint_ty2)
2048    }
2049}
2050
2051fn uint_bit_width(uint_ty: UintTy) -> u64 {
2052    uint_ty
2053        .bit_width()
2054        .unwrap_or(config::pointer_width().bits())
2055}
2056
2057fn int_bit_width(int_ty: IntTy) -> u64 {
2058    int_ty.bit_width().unwrap_or(config::pointer_width().bits())
2059}
2060
2061impl ShapeResult {
2062    fn into_bb_envs(
2063        self,
2064        infcx: &mut InferCtxtRoot,
2065    ) -> FxHashMap<LocalDefId, FxHashMap<BasicBlock, BasicBlockEnv>> {
2066        self.0
2067            .into_iter()
2068            .map(|(def_id, shapes)| {
2069                let bb_envs = shapes
2070                    .into_iter()
2071                    .map(|(bb, shape)| (bb, shape.into_bb_env(infcx)))
2072                    .collect();
2073                (def_id, bb_envs)
2074            })
2075            .collect()
2076    }
2077}
2078
2079fn marker_at_dominator<'a>(
2080    body: &Body,
2081    markers: &'a IndexVec<BasicBlock, Option<Marker>>,
2082    bb: BasicBlock,
2083) -> &'a Marker {
2084    let dominator = body
2085        .dominators()
2086        .immediate_dominator(bb)
2087        .unwrap_or_else(|| tracked_span_bug!());
2088    markers[dominator]
2089        .as_ref()
2090        .unwrap_or_else(|| tracked_span_bug!())
2091}
2092
2093pub(crate) mod errors {
2094    use flux_errors::{E0999, ErrorGuaranteed};
2095    use flux_infer::infer::InferErr;
2096    use flux_middle::{global_env::GlobalEnv, queries::ErrCtxt};
2097    use rustc_errors::Diagnostic;
2098    use rustc_hir::def_id::LocalDefId;
2099    use rustc_span::Span;
2100
2101    use crate::fluent_generated as fluent;
2102
2103    #[derive(Debug)]
2104    pub struct CheckerError {
2105        kind: InferErr,
2106        span: Span,
2107    }
2108
2109    impl CheckerError {
2110        pub fn emit(self, genv: GlobalEnv, fn_def_id: LocalDefId) -> ErrorGuaranteed {
2111            let dcx = genv.sess().dcx().handle();
2112            match self.kind {
2113                InferErr::UnsolvedEvar(_) => {
2114                    let mut diag =
2115                        dcx.struct_span_err(self.span, fluent::refineck_param_inference_error);
2116                    diag.code(E0999);
2117                    diag.emit()
2118                }
2119                InferErr::Query(err) => {
2120                    let level = rustc_errors::Level::Error;
2121                    err.at(ErrCtxt::FnCheck(self.span, fn_def_id))
2122                        .into_diag(dcx, level)
2123                        .emit()
2124                }
2125            }
2126        }
2127    }
2128
2129    pub trait ResultExt<T> {
2130        fn with_span(self, span: Span) -> Result<T, CheckerError>;
2131    }
2132
2133    impl<T, E> ResultExt<T> for Result<T, E>
2134    where
2135        E: Into<InferErr>,
2136    {
2137        fn with_span(self, span: Span) -> Result<T, CheckerError> {
2138            self.map_err(|err| CheckerError { kind: err.into(), span })
2139        }
2140    }
2141}