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 def_id: LocalDefId,
68 inherited: Inherited<'ck, M>,
69 body: &'ck Body<'tcx>,
70 resume_ty: Option<Ty>,
72 output: Binder<FnOutput>,
73 markers: IndexVec<BasicBlock, Option<Marker>>,
76 visited: DenseBitSet<BasicBlock>,
77 queue: WorkQueue<'ck>,
78 default_refiner: Refiner<'genv, 'tcx>,
79}
80
81struct Inherited<'ck, M> {
83 ghost_stmts: &'ck UnordMap<LocalDefId, GhostStatements>,
86 mode: &'ck mut M,
87
88 closures: &'ck mut UnordMap<DefId, PolyFnSig>,
92}
93
94#[derive(Debug)]
95struct ResolvedCall {
96 output: Ty,
97 _early_args: Vec<Expr>,
99 _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
146pub(crate) struct ShapeResult(FxHashMap<LocalDefId, FxHashMap<BasicBlock, BasicBlockEnvShape>>);
148
149#[derive(Debug)]
151enum Guard {
152 None,
154 Pred(Expr),
156 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 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 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#[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
251fn 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 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 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 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 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 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 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 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
344pub(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 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 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
409fn unfold_local_ptrs(
420 infcx: &mut InferCtxt,
421 env: &mut TypeEnv,
422 fn_sig: &PolyFnSig,
423 actuals: &[Ty],
424) -> InferResult<Vec<Ty>> {
425 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
445fn 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 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 }
603 StatementKind::FakeRead(_) => {
604 }
606 StatementKind::AscribeUserType(_, _) => {
607 }
610 StatementKind::PlaceMention(_) => {
611 }
614 StatementKind::Nop => {}
615 StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(op)) => {
616 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 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 let generic_args = infcx.instantiate_generic_args(generic_args);
799
800 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 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 for requires in fn_sig.requires() {
844 at.check_pred(requires, ConstrReason::Call);
845 }
846
847 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 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 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 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 @ BaseTy::Param(_)) => {
969 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 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 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 let (upvar_tys, poly_sig) = self
1203 .closure_template(infcx, env, stmt_span, args, operands)
1204 .with_span(stmt_span)?;
1205 self.check_closure_body(infcx, did, &upvar_tys, args, &poly_sig)?;
1207 self.inherited.closures.insert(*did, poly_sig);
1209 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 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 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 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 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 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 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 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 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 } 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(¶m, 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(¶m, 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 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
1893fn 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 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}