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 def_id: LocalDefId,
70 inherited: Inherited<'ck, M>,
71 body: &'ck Body<'tcx>,
72 resume_ty: Option<Ty>,
74 output: Binder<FnOutput>,
75 markers: IndexVec<BasicBlock, Option<Marker>>,
78 visited: DenseBitSet<BasicBlock>,
79 queue: WorkQueue<'ck>,
80 default_refiner: Refiner<'genv, 'tcx>,
81}
82
83struct Inherited<'ck, M> {
85 ghost_stmts: &'ck UnordMap<LocalDefId, GhostStatements>,
88 mode: &'ck mut M,
89
90 closures: &'ck mut UnordMap<DefId, PolyFnSig>,
94}
95
96#[derive(Debug)]
97struct ResolvedCall {
98 output: Ty,
99 _early_args: Vec<Expr>,
101 _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
148pub(crate) struct ShapeResult(FxHashMap<LocalDefId, FxHashMap<BasicBlock, BasicBlockEnvShape>>);
150
151#[derive(Debug)]
153enum Guard {
154 None,
156 Pred(Expr),
158 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 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 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#[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
253fn 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 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 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 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 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 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 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 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
346pub(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 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 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
411fn unfold_local_ptrs(
422 infcx: &mut InferCtxt,
423 env: &mut TypeEnv,
424 fn_sig: &PolyFnSig,
425 actuals: &[Ty],
426) -> InferResult<Vec<Ty>> {
427 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
447fn 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 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 }
605 StatementKind::FakeRead(_) => {
606 }
608 StatementKind::AscribeUserType(_, _) => {
609 }
612 StatementKind::PlaceMention(_) => {
613 }
616 StatementKind::Nop => {}
617 StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(op)) => {
618 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 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 let generic_args = infcx.instantiate_generic_args(generic_args);
801
802 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 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 for requires in fn_sig.requires() {
846 at.check_pred(requires, ConstrReason::Call);
847 }
848
849 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 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 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 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 @ BaseTy::Param(_)) => {
971 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 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 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 let (upvar_tys, poly_sig) = self
1205 .closure_template(infcx, env, stmt_span, args, operands)
1206 .with_span(stmt_span)?;
1207 self.check_closure_body(infcx, did, &upvar_tys, args, &poly_sig)?;
1209 self.inherited.closures.insert(*did, poly_sig);
1211 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 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 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 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 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 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 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 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 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 } 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(¶m, 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(¶m, 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 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
1891fn 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}