flux_refineck/
checker.rs

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