rapx/verify/
verifier.rs

1//! Forward visitor for relevant MIR items.
2//!
3//! This module consumes the MIR items produced by `backward_visit` and visits
4//! them in path order.  The current implementation is a skeleton: it records
5//! simple value/fact summaries and leaves unsupported MIR effects as notes so
6//! later property checkers can be added incrementally.
7
8use std::collections::HashSet;
9
10use crate::compat::FxHashMap;
11use crate::compat::Spanned;
12use rustc_hir::def_id::DefId;
13use rustc_middle::{
14    mir::{
15        AggregateKind, BasicBlock, BinOp, Body, Local, Operand, Place, Rvalue, Statement,
16        StatementKind, Terminator, TerminatorKind, UnOp,
17    },
18    ty::{Ty, TyCtxt, TyKind},
19};
20
21use super::{
22    call_summary::{self, CallEffect, CallEffectSummary},
23    contract::Property,
24    def_use::{PlaceBaseKey, PlaceKey},
25    helpers::CheckpointLocation,
26    path_extractor::{Path, PathStep},
27    slicer::{BackwardItem, ForgetReason, KeepReason, RelevantMirItems},
28};
29
30/// Visits relevant MIR items forward and builds an abstract state.
31pub struct ForwardVerifier<'tcx> {
32    tcx: TyCtxt<'tcx>,
33}
34
35impl<'tcx> ForwardVerifier<'tcx> {
36    /// Create a forward visitor over the current compiler type context.
37    pub fn new(tcx: TyCtxt<'tcx>) -> Self {
38        Self { tcx }
39    }
40
41    /// Visit relevant MIR items in path order and produce an abstract state.
42    pub fn visit(&self, items: &RelevantMirItems<'tcx>) -> ForwardVisitResult<'tcx> {
43        let mut result =
44            ForwardVisitResult::new(items.checkpoint, items.property.clone(), items.path.clone());
45        let body = self.tcx.optimized_mir(items.checkpoint.caller);
46
47        for item in &items.items {
48            match item {
49                BackwardItem::Statement {
50                    block,
51                    statement_index,
52                    kind,
53                } => {
54                    let statement = &body.basic_blocks[*block].statements[*statement_index];
55                    self.visit_statement(
56                        *block,
57                        *statement_index,
58                        *kind,
59                        statement,
60                        body,
61                        &mut result,
62                    );
63                }
64                BackwardItem::Terminator { block, kind } => {
65                    let terminator = body.basic_blocks[*block].terminator();
66                    self.visit_terminator(*block, *kind, terminator, body, &mut result);
67                }
68                BackwardItem::PathStep { step, kind } => {
69                    result.steps.push(ForwardStep::PathStep {
70                        step: step.clone(),
71                        reason: *kind,
72                    });
73                }
74                BackwardItem::ContractFact { property } => {
75                    result.facts.push(StateFact::Contract(property.clone()));
76                }
77                BackwardItem::Forget { reason } => {
78                    result.forgets.push(reason.clone());
79                }
80            }
81        }
82
83        result
84    }
85
86    /// Visit one retained MIR statement.
87    fn visit_statement(
88        &self,
89        block: BasicBlock,
90        statement_index: usize,
91        reason: KeepReason,
92        statement: &Statement<'tcx>,
93        body: &Body<'tcx>,
94        result: &mut ForwardVisitResult<'tcx>,
95    ) {
96        result.steps.push(ForwardStep::Statement {
97            block,
98            statement_index,
99            reason,
100        });
101
102        match &statement.kind {
103            StatementKind::Assign(assign) => {
104                let (place, rvalue) = &**assign;
105                let value = self.value_from_rvalue(rvalue);
106                result.record_value_definition(block, Some(statement_index), place.local, value);
107                self.record_rvalue_facts(block, statement_index, place, rvalue, body, result);
108            }
109            StatementKind::FakeRead(..)
110            | StatementKind::SetDiscriminant { .. }
111            | StatementKind::StorageLive(..)
112            | StatementKind::AscribeUserType(..)
113            | StatementKind::Coverage(..)
114            | StatementKind::PlaceMention(..)
115            | StatementKind::Intrinsic(..)
116            | StatementKind::ConstEvalCounter
117            | StatementKind::Nop => {}
118            #[cfg(not(rapx_rustc_ge_198))]
119            StatementKind::Retag(..) => {}
120            StatementKind::StorageDead(local) => {
121                result.facts.push(StateFact::LocalDead(*local));
122            }
123            _ => result.notes.push(format!(
124                "unsupported statement at bb{}#{statement_index}",
125                block.as_usize()
126            )),
127        }
128    }
129
130    /// Visit one retained MIR terminator.
131    fn visit_terminator(
132        &self,
133        block: BasicBlock,
134        reason: KeepReason,
135        terminator: &Terminator<'tcx>,
136        body: &Body<'tcx>,
137        result: &mut ForwardVisitResult<'tcx>,
138    ) {
139        result.steps.push(ForwardStep::Terminator { block, reason });
140
141        match &terminator.kind {
142            TerminatorKind::Call {
143                func,
144                args,
145                destination,
146                ..
147            } => {
148                let arg_values = args
149                    .iter()
150                    .map(|arg| value_from_operand(&arg.node))
151                    .collect();
152                let effect_summary = call_summary::effect_summary(
153                    self.tcx,
154                    result.checkpoint.caller,
155                    func,
156                    destination.local,
157                );
158                let call = CallSummary {
159                    destination: destination.local,
160                    func: call_summary::call_name(self.tcx, func),
161                    arg_count: args.len(),
162                    args: arg_values,
163                    effects: effect_summary.effects.clone(),
164                    unsupported: effect_summary.unsupported,
165                };
166                result.record_value_definition(
167                    block,
168                    None,
169                    destination.local,
170                    AbstractValue::CallResult(call.clone()),
171                );
172                result.facts.push(StateFact::Call(call));
173                self.apply_call_effects(
174                    block,
175                    &effect_summary,
176                    args,
177                    reason == KeepReason::Checkpoint,
178                    result,
179                );
180                let is_uninit = call_summary::is_maybe_uninit_uninit_call(&call_summary::call_name(self.tcx, func));
181                if is_uninit
182                    && let Some((_elem_ty_name, elements)) =
183                        self.allocated_element_summary(result.checkpoint.caller, Some(destination.local))
184                {
185                    let dest_place = PlaceKey {
186                        base: crate::verify::def_use::PlaceBaseKey::Local(destination.local.as_usize()),
187                        fields: Vec::new(),
188                    };
189                    let actual_ty = self.tcx.optimized_mir(result.checkpoint.caller)
190                        .local_decls[destination.local].ty;
191                    result.facts.push(StateFact::KnownAllocated {
192                        place: dest_place.clone(),
193                        object: dest_place.clone(),
194                        ty_name: format!("{actual_ty:?}"),
195                        elements,
196                        reason: "live local allocation".to_string(),
197                    });
198                }
199            }
200            TerminatorKind::SwitchInt { discr, .. } => {
201                if let Some(equals) = chosen_switch_value(&result.path, block, terminator) {
202                    let value = value_from_operand(discr);
203                    let (cmp_op, cmp_lhs, cmp_rhs) = find_cmp_source(block, discr, body);
204                    result.facts.push(StateFact::BranchEq {
205                        value: value.clone(),
206                        equals,
207                        cmp_op,
208                        cmp_lhs,
209                        cmp_rhs,
210                    });
211                    if let Some((place, align)) = align_guard_value(&value, equals, result) {
212                        result.facts.push(StateFact::KnownAligned {
213                            place,
214                            align,
215                            ty_name: format!("{align}-aligned"),
216                            reason: format!("{align}-byte alignment guard on path"),
217                        });
218                    }
219                } else {
220                    result
221                        .facts
222                        .push(StateFact::PathCondition(format!("{discr:?}")));
223                }
224            }
225            TerminatorKind::Assert { cond, expected, .. } => {
226                let (cmp_op, cmp_lhs, cmp_rhs) = find_cmp_source(block, cond, body);
227                result.facts.push(StateFact::BranchEq {
228                    value: value_from_operand(cond),
229                    equals: u128::from(*expected),
230                    cmp_op,
231                    cmp_lhs,
232                    cmp_rhs,
233                });
234            }
235            TerminatorKind::Drop { place, .. } => {
236                result
237                    .facts
238                    .push(StateFact::Drop(PlaceKey::from_mir_place(place)));
239            }
240            TerminatorKind::Goto { .. }
241            | TerminatorKind::Return
242            | TerminatorKind::Unreachable
243            | TerminatorKind::UnwindResume
244            | TerminatorKind::UnwindTerminate(_)
245            | TerminatorKind::Yield { .. }
246            | TerminatorKind::CoroutineDrop
247            | TerminatorKind::FalseEdge { .. }
248            | TerminatorKind::FalseUnwind { .. }
249            | TerminatorKind::InlineAsm { .. }
250            | TerminatorKind::TailCall { .. } => {}
251        }
252    }
253
254    /// Build an abstract value for a MIR rvalue.
255    fn value_from_rvalue(&self, rvalue: &Rvalue<'tcx>) -> AbstractValue<'tcx> {
256        match rvalue {
257            Rvalue::Use(operand, ..) => value_from_operand(operand),
258            Rvalue::Repeat(operand, _) => {
259                AbstractValue::Repeat(Box::new(value_from_operand(operand)))
260            }
261            Rvalue::Ref(_, _, place) => AbstractValue::Ref(PlaceKey::from_mir_place(place)),
262            Rvalue::RawPtr(_, place) => AbstractValue::RawPtr(PlaceKey::from_mir_place(place)),
263            Rvalue::ThreadLocalRef(def_id) => AbstractValue::ThreadLocal(format!("{def_id:?}")),
264            Rvalue::Cast(_, operand, ty) => {
265                AbstractValue::Cast(Box::new(value_from_operand(operand)), *ty)
266            }
267            Rvalue::BinaryOp(op, pair) => {
268                let (lhs, rhs) = &**pair;
269                AbstractValue::Binary(
270                    *op,
271                    Box::new(value_from_operand(lhs)),
272                    Box::new(value_from_operand(rhs)),
273                )
274            }
275            #[cfg(all(rapx_rustc_ge_193, not(rapx_rustc_ge_196)))]
276            Rvalue::NullaryOp(op) => AbstractValue::Nullary(format!("{op:?}")),
277            #[cfg(all(not(rapx_rustc_ge_193), not(rapx_rustc_ge_196)))]
278            Rvalue::NullaryOp(op, _) => AbstractValue::Nullary(format!("{op:?}")),
279            Rvalue::UnaryOp(op, operand) => {
280                AbstractValue::Unary(*op, Box::new(value_from_operand(operand)))
281            }
282            Rvalue::Discriminant(place) => {
283                AbstractValue::Discriminant(PlaceKey::from_mir_place(place))
284            }
285            Rvalue::Aggregate(kind, operands) => {
286                AbstractValue::Aggregate(aggregate_name(kind), operands.len())
287            }
288            #[cfg(not(rapx_rustc_ge_196))]
289            Rvalue::ShallowInitBox(operand, ty) => {
290                AbstractValue::ShallowInitBox(Box::new(value_from_operand(operand)), *ty)
291            }
292            Rvalue::CopyForDeref(place) => AbstractValue::Place(PlaceKey::from_mir_place(place)),
293            _ => AbstractValue::Unknown(format!("{rvalue:?}")),
294        }
295    }
296
297    /// Record initial facts directly implied by selected rvalues.
298    fn record_rvalue_facts(
299        &self,
300        block: BasicBlock,
301        statement_index: usize,
302        place: &Place<'tcx>,
303        rvalue: &Rvalue<'tcx>,
304        body: &Body<'tcx>,
305        result: &mut ForwardVisitResult<'tcx>,
306    ) {
307        let target = PlaceKey::from_mir_place(place);
308        match rvalue {
309            Rvalue::Ref(_, _, source) => {
310                let source = PlaceKey::from_mir_place(source);
311                let object = allocation_object_for_source(&source, result);
312                result.facts.push(StateFact::PointsTo {
313                    pointer: target.clone(),
314                    source: source.clone(),
315                });
316                if let Some((ty_name, elements)) =
317                    self.allocated_element_summary(result.checkpoint.caller, object.local())
318                {
319                    result.facts.push(StateFact::KnownAllocated {
320                        place: target,
321                        object,
322                        ty_name,
323                        elements,
324                        reason: "derived from live local/reference".to_string(),
325                    });
326                }
327            }
328            Rvalue::RawPtr(_, source) => {
329                let source_key = PlaceKey::from_mir_place(source);
330                if let Some(alias) =
331                    self.deref_pointer_value_for_place(result.checkpoint.caller, source)
332                {
333                    result.record_value_definition(
334                        block,
335                        Some(statement_index),
336                        place.local,
337                        AbstractValue::Place(alias.clone()),
338                    );
339                    let ty = self.tcx.optimized_mir(result.checkpoint.caller).local_decls
340                        [place.local]
341                        .ty;
342                    result.facts.push(StateFact::Cast {
343                        target: target.clone(),
344                        source: AbstractValue::Place(alias),
345                        ty,
346                    });
347                }
348                let object = self
349                    .referenced_object_for_place(result.checkpoint.caller, source)
350                    .unwrap_or_else(|| allocation_object_for_source(&source_key, result));
351                result.facts.push(StateFact::PointsTo {
352                    pointer: target.clone(),
353                    source: source_key,
354                });
355                result.facts.push(StateFact::KnownNonZero {
356                    place: target.clone(),
357                    reason: "created from reference".to_string(),
358                });
359                if let Some((ty_name, elements)) =
360                    self.allocated_element_summary(result.checkpoint.caller, object.local())
361                {
362                    result.facts.push(StateFact::KnownAllocated {
363                        place: target,
364                        object,
365                        ty_name,
366                        elements,
367                        reason: "derived from live local/reference".to_string(),
368                    });
369                }
370            }
371            Rvalue::Aggregate(kind, operands) => {
372                let is_decomposable =
373                    matches!(kind.as_ref(), AggregateKind::Adt(..) | AggregateKind::Tuple);
374                if !is_decomposable {
375                    return;
376                }
377                for (field_index, operand) in operands.iter().enumerate() {
378                    let mut field_place = target.clone();
379                    field_place.fields.push(field_index);
380                    let source_val = value_from_operand(operand);
381                    let op_ty = operand.ty(&body.local_decls, self.tcx);
382                    result.facts.push(StateFact::Cast {
383                        target: field_place,
384                        source: source_val,
385                        ty: op_ty,
386                    });
387                }
388            }
389            Rvalue::Cast(_, operand, ty) => {
390                let source_val = value_from_operand(operand);
391                result.facts.push(StateFact::Cast {
392                    target: target.clone(),
393                    source: source_val.clone(),
394                    ty: *ty,
395                });
396                if let Some(align) = known_alignment_of(&source_val, result) {
397                    result.facts.push(StateFact::KnownAligned {
398                        place: target.clone(),
399                        align,
400                        ty_name: format!("cast-{align}"),
401                        reason: format!("cast preserves {align}-byte alignment"),
402                    });
403                }
404                if let AbstractValue::Place(source_place) = &source_val
405                    && let Some((ty_name, elements)) =
406                        self.box_projection_allocation(result.checkpoint.caller, source_place, *ty)
407                {
408                    result.facts.push(StateFact::KnownAllocated {
409                        place: target,
410                        object: source_place.clone(),
411                        ty_name,
412                        elements,
413                        reason: "cast from Box-owned pointer field".to_string(),
414                    });
415                }
416            }
417            #[cfg(not(rapx_rustc_ge_198))]
418            Rvalue::Use(operand) => {
419                let source_place = match operand {
420                    Operand::Copy(place) | Operand::Move(place) => Some(place),
421                    _ => None,
422                };
423                if let Some(source_place) = source_place {
424                    let has_projection = source_place
425                        .projection
426                        .iter()
427                        .any(|p| {
428                            matches!(p,
429                                rustc_middle::mir::ProjectionElem::Deref |
430                                rustc_middle::mir::ProjectionElem::Field(..)
431                            )
432                        });
433                    if !has_projection {
434                        return;
435                    }
436                    let source_key = PlaceKey::from_mir_place(source_place);
437                    let op_ty = operand.ty(&body.local_decls, self.tcx);
438                    result.facts.push(StateFact::Cast {
439                        target: target.clone(),
440                        source: AbstractValue::Place(source_key),
441                        ty: op_ty,
442                    });
443                }
444            }
445            #[cfg(rapx_rustc_ge_198)]
446            Rvalue::Use(operand, _retag) => {
447                let source_place = match operand {
448                    Operand::Copy(place) | Operand::Move(place) => Some(place),
449                    _ => None,
450                };
451                if let Some(source_place) = source_place {
452                    let has_projection = source_place
453                        .projection
454                        .iter()
455                        .any(|p| {
456                            matches!(p,
457                                rustc_middle::mir::ProjectionElem::Deref |
458                                rustc_middle::mir::ProjectionElem::Field(..)
459                            )
460                        });
461                    if !has_projection {
462                        return;
463                    }
464                    let source_key = PlaceKey::from_mir_place(source_place);
465                    let op_ty = operand.ty(&body.local_decls, self.tcx);
466                    result.facts.push(StateFact::Cast {
467                        target: target.clone(),
468                        source: AbstractValue::Place(source_key),
469                        ty: op_ty,
470                    });
471                }
472            }
473            Rvalue::CopyForDeref(place) => {
474                let source_place = PlaceKey::from_mir_place(place);
475                result.facts.push(StateFact::Cast {
476                    target: target.clone(),
477                    source: AbstractValue::Place(source_place),
478                    ty: self.tcx.types.usize,
479                });
480            }
481            Rvalue::BinaryOp(op, pair) => {
482                let (lhs, rhs) = &**pair;
483                let lhs_val = value_from_operand(lhs);
484                let rhs_val = value_from_operand(rhs);
485                let target_key = target.clone();
486                result.facts.push(StateFact::Binary {
487                    target: target_key.clone(),
488                    op: *op,
489                    lhs: lhs_val.clone(),
490                    rhs: rhs_val.clone(),
491                });
492                // If multiplying by a known constant multiple of an alignment
493                // (e.g. i * 4), the result inherits that alignment property.
494                if *op == BinOp::Mul || *op == BinOp::MulWithOverflow {
495                    let rhs_resolved = resolve_value_chain(&rhs_val, result);
496                    if let Some(divisor) = const_int_value(&rhs_resolved) {
497                        if divisor > 0 && is_power_of_two(divisor) {
498                            result.facts.push(StateFact::KnownAligned {
499                                place: target_key.clone(),
500                                align: divisor as u64,
501                                ty_name: format!("result of mul by {divisor}"),
502                                reason: format!("multiply by {divisor} (power of two)"),
503                            });
504                        }
505                    }
506                }
507                if *op == BinOp::Add || *op == BinOp::AddWithOverflow {
508                    if let Some(a) = known_alignment_of(&lhs_val, result).and_then(|a| {
509                        known_alignment_of(&rhs_val, result)
510                            .filter(|&b| b == a)
511                            .map(|_| a)
512                    }) {
513                        result.facts.push(StateFact::KnownAligned {
514                            place: target_key.clone(),
515                            align: a,
516                            ty_name: format!("sum of {a}-aligned"),
517                            reason: "sum of two aligned values".into(),
518                        });
519                    }
520                }
521                if *op == BinOp::Div {
522                    if let Some(src_align) = known_alignment_of(&lhs_val, result) {
523                        let rhs_resolved = resolve_value_chain(&rhs_val, result);
524                        if let Some(divisor) = const_int_value(&rhs_resolved) {
525                            if divisor > 0 && src_align % divisor as u64 == 0 {
526                                let new_align = src_align / divisor as u64;
527                                result.facts.push(StateFact::KnownAligned {
528                                    place: target_key.clone(),
529                                    align: new_align,
530                                    ty_name: format!("result of div by {divisor}"),
531                                    reason: format!("dividing {src_align}-aligned by {divisor}"),
532                                });
533                            }
534                        }
535                    }
536                }
537            }
538            _ => {}
539        }
540    }
541
542    /// Apply a summarized call effect to the path-local abstract state.
543    fn apply_call_effects(
544        &self,
545        block: BasicBlock,
546        summary: &CallEffectSummary,
547        args: &[Spanned<Operand<'tcx>>],
548        is_target_checkpoint: bool,
549        result: &mut ForwardVisitResult<'tcx>,
550    ) {
551        result.facts.push(StateFact::CallEffect(summary.clone()));
552        let Some(destination) = summary.destination else {
553            return;
554        };
555        let destination_place = PlaceKey {
556            base: super::def_use::PlaceBaseKey::Local(destination.as_usize()),
557            fields: Vec::new(),
558        };
559
560        for effect in &summary.effects {
561            match effect {
562                CallEffect::ReturnAliasArg { arg } | CallEffect::ReturnPointerFromArg { arg } => {
563                    if let Some(source) = args.get(*arg).and_then(|arg| operand_place(&arg.node)) {
564                        let object = allocation_object_for_source(&source, result);
565                        result.facts.push(StateFact::PointsTo {
566                            pointer: destination_place.clone(),
567                            source: source.clone(),
568                        });
569                        if let Some((ty_name, elements)) =
570                            self.allocated_element_summary(result.checkpoint.caller, object.local())
571                        {
572                            result.facts.push(StateFact::KnownAllocated {
573                                place: destination_place.clone(),
574                                object,
575                                ty_name,
576                                elements,
577                                reason: format!("returned by {}", summary.name),
578                            });
579                        }
580                        result.facts.push(StateFact::KnownNonZero {
581                            place: destination_place.clone(),
582                            reason: format!("returned by {}", summary.name),
583                        });
584                    }
585                }
586                CallEffect::ReturnPointerAdd { base_arg, .. }
587                | CallEffect::ReturnPointerSub { base_arg, .. } => {
588                    if let Some(source) =
589                        args.get(*base_arg).and_then(|arg| operand_place(&arg.node))
590                    {
591                        result.facts.push(StateFact::PointsTo {
592                            pointer: destination_place.clone(),
593                            source,
594                        });
595                    }
596                }
597                CallEffect::ReturnNonZero => result.facts.push(StateFact::KnownNonZero {
598                    place: destination_place.clone(),
599                    reason: format!("returned by {}", summary.name),
600                }),
601                CallEffect::ReturnAligned { align, ty_name } => {
602                    result.facts.push(StateFact::KnownAligned {
603                        place: destination_place.clone(),
604                        align: *align,
605                        ty_name: ty_name.clone(),
606                        reason: format!("returned by {}", summary.name),
607                    });
608                }
609                CallEffect::ReturnConst { value, label } => {
610                    result.record_value_definition(
611                        block,
612                        None,
613                        destination,
614                        AbstractValue::ConstInt(u128::from(*value)),
615                    );
616                    result.facts.push(StateFact::KnownConst {
617                        place: destination_place.clone(),
618                        value: *value,
619                        reason: label.clone(),
620                    });
621                }
622                CallEffect::ReadMemory { .. } => {}
623                CallEffect::WriteMemory { pointer_arg } => {
624                    if let Some(pointer) = args
625                        .get(*pointer_arg)
626                        .and_then(|arg| operand_place(&arg.node))
627                    {
628                        let mut init_places = copy_chain_places(&pointer, result);
629                        if init_places.is_empty() {
630                            init_places.push(pointer);
631                        }
632
633                        for place in init_places {
634                            let ty_name =
635                                self.init_write_ty_name(summary, result.checkpoint.caller, &place);
636                            result.facts.push(StateFact::KnownInit {
637                                place,
638                                ty_name,
639                                elements: 1,
640                                reason: format!("written by {}", summary.name),
641                            });
642                        }
643                    }
644                }
645                CallEffect::ReturnLengthOfArg { .. } => {}
646                CallEffect::ReturnTupleFieldLength { .. } => {}
647                CallEffect::ForgetArgFacts { reason, .. } => {
648                    result.forgets.push(reason.clone());
649                }
650            }
651        }
652
653        if summary.unsupported && !is_target_checkpoint {
654            result.forgets.push(ForgetReason::UnknownCall);
655            result
656                .notes
657                .push(format!("unsupported call effect: {}", summary.name));
658        } else if summary.unsupported {
659            result.notes.push(format!(
660                "unsupported target call effect ignored for precondition proof: {}",
661                summary.name
662            ));
663        }
664    }
665
666    /// Return a compact pointee type name for a raw pointer local.
667    fn pointee_ty_name(&self, caller: DefId, place: &PlaceKey) -> Option<String> {
668        if !place.fields.is_empty() {
669            return None;
670        }
671        let local = place.local()?;
672        let ty = self.tcx.optimized_mir(caller).local_decls[local].ty;
673        match ty.kind() {
674            TyKind::RawPtr(ty, _) | TyKind::Ref(_, ty, _) => Some(format!("{ty:?}")),
675            _ => Some(format!("{ty:?}")),
676        }
677    }
678
679    fn init_write_ty_name(
680        &self,
681        summary: &CallEffectSummary,
682        caller: DefId,
683        place: &PlaceKey,
684    ) -> String {
685        let ty_name = self
686            .pointee_ty_name(caller, place)
687            .unwrap_or_else(|| "?".to_string());
688        if summary.name.contains("MaybeUninit") && summary.name.contains("write") {
689            maybe_uninit_inner_ty_name(&ty_name).unwrap_or(ty_name)
690        } else {
691            ty_name
692        }
693    }
694
695    fn allocated_element_summary(
696        &self,
697        caller: DefId,
698        local: Option<Local>,
699    ) -> Option<(String, u64)> {
700        let local = local?;
701        let ty = self.tcx.optimized_mir(caller).local_decls[local].ty;
702        fixed_allocation_elements(self.tcx, caller, ty)
703    }
704
705    fn referenced_object_for_place(&self, caller: DefId, place: &Place<'tcx>) -> Option<PlaceKey> {
706        if !place
707            .projection
708            .iter()
709            .any(|projection| matches!(projection, rustc_middle::mir::ProjectionElem::Deref))
710        {
711            return None;
712        }
713        let body = self.tcx.optimized_mir(caller);
714        for block in body.basic_blocks.iter() {
715            for statement in &block.statements {
716                let StatementKind::Assign(assign) = &statement.kind else {
717                    continue;
718                };
719                let (dest, rvalue) = assign.as_ref();
720                if dest.local != place.local {
721                    continue;
722                }
723                match rvalue {
724                    Rvalue::Ref(_, _, source) | Rvalue::RawPtr(_, source) => {
725                        return Some(PlaceKey::from_mir_place(source));
726                    }
727                    Rvalue::Use(Operand::Copy(source), ..)
728                    | Rvalue::Use(Operand::Move(source), ..) => {
729                        return Some(PlaceKey::from_mir_place(source));
730                    }
731                    _ => {}
732                }
733            }
734        }
735        None
736    }
737
738    fn deref_pointer_value_for_place(
739        &self,
740        caller: DefId,
741        place: &Place<'tcx>,
742    ) -> Option<PlaceKey> {
743        if !place
744            .projection
745            .iter()
746            .any(|projection| matches!(projection, rustc_middle::mir::ProjectionElem::Deref))
747        {
748            return None;
749        }
750
751        let body = self.tcx.optimized_mir(caller);
752        for block in body.basic_blocks.iter() {
753            for statement in &block.statements {
754                let StatementKind::Assign(assign) = &statement.kind else {
755                    continue;
756                };
757                let (dest, rvalue) = assign.as_ref();
758                if dest.local != place.local {
759                    continue;
760                }
761
762                let source = match rvalue {
763                    Rvalue::Ref(_, _, source) | Rvalue::RawPtr(_, source) => source,
764                    Rvalue::Use(Operand::Copy(source), ..)
765                    | Rvalue::Use(Operand::Move(source), ..) => source,
766                    _ => continue,
767                };
768                if source.projection.iter().any(|projection| {
769                    matches!(projection, rustc_middle::mir::ProjectionElem::Deref)
770                }) {
771                    return Some(PlaceKey::from_mir_place(source));
772                }
773            }
774        }
775
776        None
777    }
778
779    fn box_projection_allocation(
780        &self,
781        caller: DefId,
782        source_place: &PlaceKey,
783        cast_ty: Ty<'tcx>,
784    ) -> Option<(String, u64)> {
785        if source_place.fields.is_empty() {
786            return None;
787        }
788        let base = source_place.local()?;
789        let body = self.tcx.optimized_mir(caller);
790        let base_ty = body.local_decls[base].ty;
791        if !format!("{base_ty:?}").contains("Box<") {
792            return None;
793        }
794        let TyKind::RawPtr(pointee, _) = cast_ty.kind() else {
795            return None;
796        };
797        Some((format!("{pointee:?}"), 1))
798    }
799}
800
801/// Result produced by visiting relevant MIR items forward.
802#[derive(Clone, Debug)]
803pub struct ForwardVisitResult<'tcx> {
804    /// Unsafe checkpoint being checked.
805    pub checkpoint: CheckpointLocation,
806    /// Required property checked at the checkpoint.
807    pub property: Property<'tcx>,
808    /// Path whose relevant items were visited.
809    pub path: Path,
810    /// Abstract values currently known for MIR locals.
811    pub values: FxHashMap<Local, AbstractValue<'tcx>>,
812    /// Path-ordered definitions produced while replaying retained MIR items.
813    pub value_definitions: Vec<ValueDefinition<'tcx>>,
814    /// Facts recorded during the forward visit.
815    pub facts: Vec<StateFact<'tcx>>,
816    /// Places whose facts were conservatively forgotten.
817    pub forgets: Vec<ForgetReason>,
818    /// Ordered visit trace.
819    pub steps: Vec<ForwardStep>,
820    /// Unsupported items kept as notes rather than modeled facts.
821    pub notes: Vec<String>,
822}
823
824impl<'tcx> ForwardVisitResult<'tcx> {
825    /// Create an empty forward visit result.
826    pub fn new(checkpoint: CheckpointLocation, property: Property<'tcx>, path: Path) -> Self {
827        Self {
828            checkpoint,
829            property,
830            path,
831            values: FxHashMap::default(),
832            value_definitions: Vec::new(),
833            facts: Vec::new(),
834            forgets: Vec::new(),
835            steps: Vec::new(),
836            notes: Vec::new(),
837        }
838    }
839
840    /// Render a compact diagnostic summary of this forward visit.
841    pub fn describe(&self) -> String {
842        let mut lines = Vec::new();
843        lines.push("      forward visit:".to_string());
844        lines.push(format!(
845            "        |_ values: {}, facts: {}, precision loss: {}",
846            self.values.len(),
847            self.facts.len(),
848            self.forgets.len()
849        ));
850        if !self.facts.is_empty() {
851            lines.push("        |_ facts:".to_string());
852            for fact in &self.facts {
853                lines.push(format!("        |  |_ {fact:?}"));
854            }
855        }
856        if !self.notes.is_empty() {
857            lines.push("        |_ unsupported:".to_string());
858            for note in &self.notes {
859                lines.push(format!("        |  |_ {note}"));
860            }
861        }
862        lines.join("\n")
863    }
864
865    /// Record one path-ordered local definition and update the final snapshot.
866    pub fn record_value_definition(
867        &mut self,
868        block: BasicBlock,
869        statement_index: Option<usize>,
870        local: Local,
871        value: AbstractValue<'tcx>,
872    ) {
873        let value = Self::fold_self_ref(value, local, &self.values);
874        let ordinal = self.value_definitions.len();
875        self.values.insert(local, value.clone());
876        self.value_definitions.push(ValueDefinition {
877            ordinal,
878            block,
879            statement_index,
880            local,
881            value,
882        });
883    }
884
885    /// Replace `Place(local)` inside `value` with the current snapshot from
886    /// `values`.  This prevents self-referencing chains when a local is
887    /// re-assigned using its own previous value (e.g. `i = i + 1` inside a
888    /// loop).
889    fn fold_self_ref(
890        value: AbstractValue<'tcx>,
891        local: Local,
892        snapshot: &FxHashMap<Local, AbstractValue<'tcx>>,
893    ) -> AbstractValue<'tcx> {
894        let local_usize = local.as_usize();
895        match value {
896            AbstractValue::Place(ref p)
897                if p.base == PlaceBaseKey::Local(local_usize) =>
898            {
899                snapshot.get(&local).cloned().unwrap_or(value)
900            }
901            AbstractValue::Binary(op, lhs, rhs) => AbstractValue::Binary(
902                op,
903                Box::new(Self::fold_self_ref(*lhs, local, snapshot)),
904                Box::new(Self::fold_self_ref(*rhs, local, snapshot)),
905            ),
906            AbstractValue::Unary(op, inner) => AbstractValue::Unary(
907                op,
908                Box::new(Self::fold_self_ref(*inner, local, snapshot)),
909            ),
910            AbstractValue::Cast(inner, ty) => AbstractValue::Cast(
911                Box::new(Self::fold_self_ref(*inner, local, snapshot)),
912                ty,
913            ),
914            _ => value,
915        }
916    }
917
918    /// Return the latest definition of `local` before the exclusive cursor.
919    pub fn latest_value_definition_before(
920        &self,
921        local: Local,
922        cursor: usize,
923    ) -> Option<&ValueDefinition<'tcx>> {
924        let end = cursor.min(self.value_definitions.len());
925        self.value_definitions[..end]
926            .iter()
927            .rev()
928            .find(|definition| definition.local == local)
929    }
930}
931
932/// One local definition observed while replaying retained MIR items.
933#[derive(Clone, Debug)]
934pub struct ValueDefinition<'tcx> {
935    pub ordinal: usize,
936    pub block: BasicBlock,
937    pub statement_index: Option<usize>,
938    pub local: Local,
939    pub value: AbstractValue<'tcx>,
940}
941
942/// One step visited by the forward visitor.
943#[derive(Clone, Debug)]
944pub enum ForwardStep {
945    Statement {
946        block: BasicBlock,
947        statement_index: usize,
948        reason: KeepReason,
949    },
950    Terminator {
951        block: BasicBlock,
952        reason: KeepReason,
953    },
954    PathStep {
955        step: PathStep,
956        reason: KeepReason,
957    },
958}
959
960/// Abstract value assigned to a MIR local by the forward visitor.
961#[derive(Clone, Debug)]
962pub enum AbstractValue<'tcx> {
963    Unknown(String),
964    Place(PlaceKey),
965    Ref(PlaceKey),
966    RawPtr(PlaceKey),
967    ThreadLocal(String),
968    ConstInt(u128),
969    Const(String),
970    ConstParam(String),
971    Repeat(Box<AbstractValue<'tcx>>),
972    Cast(Box<AbstractValue<'tcx>>, Ty<'tcx>),
973    Unary(UnOp, Box<AbstractValue<'tcx>>),
974    Binary(BinOp, Box<AbstractValue<'tcx>>, Box<AbstractValue<'tcx>>),
975    Nullary(String),
976    Discriminant(PlaceKey),
977    Aggregate(String, usize),
978    #[cfg(not(rapx_rustc_ge_196))]
979    ShallowInitBox(Box<AbstractValue<'tcx>>, Ty<'tcx>),
980    CallResult(CallSummary<'tcx>),
981}
982
983/// Fact recorded from a relevant MIR item.
984#[derive(Clone, Debug)]
985pub enum StateFact<'tcx> {
986    Contract(Property<'tcx>),
987    PointsTo {
988        pointer: PlaceKey,
989        source: PlaceKey,
990    },
991    Cast {
992        target: PlaceKey,
993        source: AbstractValue<'tcx>,
994        ty: Ty<'tcx>,
995    },
996    Binary {
997        target: PlaceKey,
998        op: BinOp,
999        lhs: AbstractValue<'tcx>,
1000        rhs: AbstractValue<'tcx>,
1001    },
1002    BranchEq {
1003        value: AbstractValue<'tcx>,
1004        equals: u128,
1005        cmp_op: Option<BinOp>,
1006        cmp_lhs: Option<AbstractValue<'tcx>>,
1007        cmp_rhs: Option<AbstractValue<'tcx>>,
1008    },
1009    PathCondition(String),
1010    Drop(PlaceKey),
1011    LocalDead(Local),
1012    Call(CallSummary<'tcx>),
1013    CallEffect(CallEffectSummary),
1014    KnownNonZero {
1015        place: PlaceKey,
1016        reason: String,
1017    },
1018    KnownAligned {
1019        place: PlaceKey,
1020        align: u64,
1021        ty_name: String,
1022        reason: String,
1023    },
1024    KnownInit {
1025        place: PlaceKey,
1026        ty_name: String,
1027        elements: u64,
1028        reason: String,
1029    },
1030    KnownAllocated {
1031        place: PlaceKey,
1032        object: PlaceKey,
1033        ty_name: String,
1034        elements: u64,
1035        reason: String,
1036    },
1037    KnownConst {
1038        place: PlaceKey,
1039        value: u64,
1040        reason: String,
1041    },
1042}
1043
1044/// Summary for a retained call terminator.
1045#[derive(Clone, Debug)]
1046pub struct CallSummary<'tcx> {
1047    pub destination: Local,
1048    pub func: String,
1049    pub arg_count: usize,
1050    pub args: Vec<AbstractValue<'tcx>>,
1051    pub effects: Vec<CallEffect>,
1052    pub unsupported: bool,
1053}
1054
1055fn extract_const_param_name(text: &str) -> Option<String> {
1056    if let Some(start) = text.find("kind: Param(") {
1057        let rest = &text[start + "kind: Param(".len()..];
1058        if let Some(end) = rest.find(')') {
1059            let inner = &rest[..end];
1060            if let Some(name_start) = inner.find("name: ") {
1061                let name_part = &inner[name_start + "name: ".len()..];
1062                if let Some(name_end) = name_part.find(',') {
1063                    return Some(name_part[..name_end].trim().to_string());
1064                }
1065                return Some(name_part.trim().to_string());
1066            }
1067        }
1068    }
1069    None
1070}
1071
1072/// Convert a MIR operand to an abstract value.
1073fn value_from_operand<'tcx>(operand: &Operand<'tcx>) -> AbstractValue<'tcx> {
1074    match operand {
1075        Operand::Copy(place) | Operand::Move(place) => {
1076            AbstractValue::Place(PlaceKey::from_mir_place(place))
1077        }
1078        Operand::Constant(constant) => {
1079            let text = format!("{:?}", constant.const_);
1080            if let Some(name) = extract_const_param_name(&text) {
1081                return AbstractValue::ConstParam(name);
1082            }
1083            const_int_from_debug(&text)
1084                .map(AbstractValue::ConstInt)
1085                .unwrap_or(AbstractValue::Const(text))
1086        }
1087        #[cfg(rapx_rustc_ge_196)]
1088        Operand::RuntimeChecks(_) => AbstractValue::Unknown("RuntimeChecks".to_string()),
1089    }
1090}
1091
1092/// Convert an operand into a place key when it names a MIR place.
1093fn operand_place(operand: &Operand<'_>) -> Option<PlaceKey> {
1094    match operand {
1095        Operand::Copy(place) | Operand::Move(place) => Some(PlaceKey::from_mir_place(place)),
1096        Operand::Constant(_) => None,
1097        #[cfg(rapx_rustc_ge_196)]
1098        Operand::RuntimeChecks(_) => None,
1099    }
1100}
1101
1102/// Extract a small integer constant from rustc's debug representation.
1103fn const_int_from_debug(text: &str) -> Option<u128> {
1104    let text = text.trim();
1105    if text == "const true" {
1106        return Some(1);
1107    }
1108    if text == "const false" {
1109        return Some(0);
1110    }
1111    if let Some(rest) = text.strip_prefix("const ") {
1112        let digits = rest
1113            .chars()
1114            .take_while(|ch| ch.is_ascii_digit())
1115            .collect::<String>();
1116        if digits.is_empty() {
1117            return None;
1118        }
1119        return digits.parse().ok();
1120    }
1121
1122    let scalar = text.strip_prefix("Val(Scalar(0x")?;
1123    let digits = scalar
1124        .chars()
1125        .take_while(|ch| ch.is_ascii_hexdigit())
1126        .collect::<String>();
1127    if digits.is_empty() {
1128        None
1129    } else {
1130        u128::from_str_radix(&digits, 16).ok()
1131    }
1132}
1133
1134/// Return the concrete SwitchInt value that selects the next path block.
1135fn chosen_switch_value(
1136    path: &Path,
1137    block: BasicBlock,
1138    terminator: &Terminator<'_>,
1139) -> Option<u128> {
1140    let TerminatorKind::SwitchInt { targets, .. } = &terminator.kind else {
1141        return None;
1142    };
1143    let chosen = chosen_successor(path, block)?;
1144    let mut explicit_values = Vec::new();
1145    for (value, target) in targets.iter() {
1146        explicit_values.push(value);
1147        if target == chosen {
1148            return Some(value);
1149        }
1150    }
1151
1152    if targets.otherwise() == chosen && explicit_values.len() == 1 {
1153        return match explicit_values[0] {
1154            0 => Some(1),
1155            1 => Some(0),
1156            _ => None,
1157        };
1158    }
1159
1160    None
1161}
1162
1163/// Return the next MIR block after `block` in a finite verification path.
1164fn chosen_successor(path: &Path, block: BasicBlock) -> Option<BasicBlock> {
1165    let mut previous = None;
1166    for step in path.steps.iter() {
1167        match step {
1168            PathStep::Block(current) => {
1169                if previous == Some(block) {
1170                    return Some(*current);
1171                }
1172                previous = Some(*current);
1173            }
1174            PathStep::Checkpoint(_) => return None,
1175        }
1176    }
1177    None
1178}
1179
1180/// Return a compact aggregate kind name.
1181fn aggregate_name<'tcx>(kind: &AggregateKind<'tcx>) -> String {
1182    match kind {
1183        AggregateKind::Array(_) => "array".to_string(),
1184        AggregateKind::Tuple => "tuple".to_string(),
1185        AggregateKind::Adt(def_id, ..) => format!("adt({def_id:?})"),
1186        AggregateKind::Closure(def_id, _) => format!("closure({def_id:?})"),
1187        AggregateKind::Coroutine(def_id, _) => format!("coroutine({def_id:?})"),
1188        AggregateKind::CoroutineClosure(def_id, _) => format!("coroutine_closure({def_id:?})"),
1189        AggregateKind::RawPtr(_, _) => "raw_ptr".to_string(),
1190    }
1191}
1192
1193fn const_int_value(val: &AbstractValue<'_>) -> Option<u128> {
1194    match val {
1195        AbstractValue::ConstInt(v) => Some(*v),
1196        _ => None,
1197    }
1198}
1199
1200fn is_power_of_two(n: u128) -> bool {
1201    n > 0 && (n & (n - 1)) == 0
1202}
1203
1204fn is_const_zero(val: &AbstractValue<'_>) -> bool {
1205    matches!(val, AbstractValue::ConstInt(0))
1206}
1207
1208fn align_guard_value<'tcx>(
1209    value: &AbstractValue<'tcx>,
1210    equals: u128,
1211    result: &ForwardVisitResult<'tcx>,
1212) -> Option<(PlaceKey, u64)> {
1213    let resolved = resolve_value_chain(value, result);
1214    if equals == 0 {
1215        // MIR encodes `value % n == 0` as switchInt(value) -> [0: ...].
1216        match &resolved {
1217            AbstractValue::Binary(BinOp::Rem, rem_l, rem_r) => {
1218                let d = const_int_value(rem_r)?;
1219                if d > 0 && is_power_of_two(d) {
1220                    let place = match resolve_value_chain(rem_l, result) {
1221                        AbstractValue::Place(p) => p,
1222                        AbstractValue::Cast(inner, _) => match inner.as_ref() {
1223                            AbstractValue::Place(p) => p.clone(),
1224                            _ => return None,
1225                        },
1226                        _ => return None,
1227                    };
1228                    return Some((place, d as u64));
1229                }
1230            }
1231            _ => {}
1232        }
1233    }
1234    if equals == 1 {
1235        // Guards expressed as `(value % n) == 0` produce Eq(Rem(place, n), 0).
1236        let AbstractValue::Binary(BinOp::Eq, eq_l, eq_r) = &resolved else {
1237            return None;
1238        };
1239        if !is_const_zero(eq_r) {
1240            return None;
1241        }
1242        let eq_resolved = resolve_value_chain(eq_l, result);
1243        let AbstractValue::Binary(BinOp::Rem, rem_l, rem_r) = &eq_resolved else {
1244            return None;
1245        };
1246        let d = const_int_value(rem_r)?;
1247        if d == 0 || !is_power_of_two(d) {
1248            return None;
1249        }
1250        let place = match resolve_value_chain(rem_l, result) {
1251            AbstractValue::Place(p) => p,
1252            AbstractValue::Cast(inner, _) => match inner.as_ref() {
1253                AbstractValue::Place(p) => p.clone(),
1254                _ => return None,
1255            },
1256            _ => return None,
1257        };
1258        return Some((place, d as u64));
1259    }
1260    None
1261}
1262
1263fn resolve_value_chain<'tcx>(
1264    value: &AbstractValue<'tcx>,
1265    result: &ForwardVisitResult<'tcx>,
1266) -> AbstractValue<'tcx> {
1267    let mut cur = value.clone();
1268    let mut seen = HashSet::new();
1269    loop {
1270        if !seen.insert(format!("{cur:?}")) {
1271            return cur;
1272        }
1273        cur = match &cur {
1274            AbstractValue::Place(p) => {
1275                if let PlaceBaseKey::Local(ix) = &p.base {
1276                    match result.values.get(&Local::from_usize(*ix)) {
1277                        Some(v) => v.clone(),
1278                        None => return cur,
1279                    }
1280                } else {
1281                    return cur;
1282                }
1283            }
1284            _ => return cur,
1285        };
1286    }
1287}
1288
1289fn copy_chain_places<'tcx>(place: &PlaceKey, result: &ForwardVisitResult<'tcx>) -> Vec<PlaceKey> {
1290    let mut places = Vec::new();
1291    let mut cur = place.clone();
1292    let mut seen = HashSet::new();
1293    loop {
1294        if !seen.insert(cur.clone()) {
1295            break;
1296        }
1297        if !places.contains(&cur) {
1298            places.push(cur.clone());
1299        }
1300
1301        let Some(local) = cur.local() else {
1302            break;
1303        };
1304        let Some(value) = result.values.get(&local) else {
1305            break;
1306        };
1307        match value {
1308            AbstractValue::Place(next) => cur = next.clone(),
1309            AbstractValue::Cast(inner, _) => match inner.as_ref() {
1310                AbstractValue::Place(next) => cur = next.clone(),
1311                _ => break,
1312            },
1313            _ => break,
1314        }
1315    }
1316    places
1317}
1318
1319fn allocation_object_for_source<'tcx>(
1320    source: &PlaceKey,
1321    result: &ForwardVisitResult<'tcx>,
1322) -> PlaceKey {
1323    let mut cur = source.clone();
1324    let mut seen = HashSet::new();
1325    loop {
1326        if !seen.insert(cur.clone()) {
1327            return cur;
1328        }
1329        if let Some(local) = cur.local()
1330            && let Some(value) = result.values.get(&local)
1331        {
1332            match value {
1333                AbstractValue::Place(next)
1334                | AbstractValue::Ref(next)
1335                | AbstractValue::RawPtr(next) => {
1336                    cur = next.clone();
1337                    continue;
1338                }
1339                AbstractValue::Cast(inner, _) => {
1340                    if let AbstractValue::Place(next)
1341                    | AbstractValue::Ref(next)
1342                    | AbstractValue::RawPtr(next) = inner.as_ref()
1343                    {
1344                        cur = next.clone();
1345                        continue;
1346                    }
1347                }
1348                _ => {}
1349            }
1350        }
1351        let Some(next) = result.facts.iter().find_map(|fact| match fact {
1352            StateFact::PointsTo { pointer, source } if pointer == &cur => Some(source.clone()),
1353            _ => None,
1354        }) else {
1355            return cur;
1356        };
1357        cur = next;
1358    }
1359}
1360
1361fn fixed_allocation_elements<'tcx>(
1362    tcx: TyCtxt<'tcx>,
1363    caller: DefId,
1364    ty: Ty<'tcx>,
1365) -> Option<(String, u64)> {
1366    match ty.kind() {
1367        TyKind::Array(elem, len) => {
1368            let value = len.try_to_target_usize(tcx)?;
1369            Some((format!("{elem:?}"), value))
1370        }
1371        TyKind::Ref(_, inner, _) => fixed_allocation_elements(tcx, caller, *inner),
1372        TyKind::Slice(elem) => Some((format!("{elem:?}"), 0)),
1373        TyKind::RawPtr(_, _) => None,
1374        TyKind::Adt(_, args) => {
1375            let ty_name = format!("{ty:?}");
1376            if ty_name.contains("MaybeUninit") {
1377                if let Some(first) = args.first()
1378                    && let Some(inner_ty) = first.as_type()
1379                    && let TyKind::Array(elem, len) = inner_ty.kind()
1380                {
1381                    // For const-generic N where length can't be
1382                    // resolved, return 0 (dynamic) — the SMT will
1383                    // use the loop guard (i < N) via guarded_len_for_index
1384                    // to discover the actual bound at each iteration.
1385                    let value = len.try_to_target_usize(tcx).unwrap_or(0);
1386                    return Some((format!("{elem:?}"), value));
1387                }
1388                return Some((ty_name, 1));
1389            }
1390            Some((ty_name, 1))
1391        }
1392        _ => Some((format!("{ty:?}"), 1)),
1393    }
1394}
1395
1396fn maybe_uninit_inner_ty_name(ty_name: &str) -> Option<String> {
1397    let ty_name = ty_name.trim();
1398    for prefix in [
1399        "std::mem::MaybeUninit<",
1400        "core::mem::MaybeUninit<",
1401        "MaybeUninit<",
1402    ] {
1403        if let Some(inner) = ty_name
1404            .strip_prefix(prefix)
1405            .and_then(|s| s.strip_suffix('>'))
1406        {
1407            return Some(inner.trim().to_string());
1408        }
1409    }
1410    None
1411}
1412
1413fn known_alignment_of<'tcx>(
1414    value: &AbstractValue<'tcx>,
1415    result: &ForwardVisitResult<'tcx>,
1416) -> Option<u64> {
1417    let mut best: Option<u64> = None;
1418    let mut cur = value.clone();
1419    let mut seen = HashSet::new();
1420    loop {
1421        if !seen.insert(format!("{cur:?}")) {
1422            break;
1423        }
1424        if let AbstractValue::Place(ref p) = cur {
1425            for f in &result.facts {
1426                if let StateFact::KnownAligned { place, align, .. } = f {
1427                    if place == p {
1428                        best = best.map_or(Some(*align), |b| Some(b.max(*align)));
1429                    }
1430                    if place.fields.is_empty() != p.fields.is_empty() && place.base == p.base {
1431                        best = best.map_or(Some(*align), |b| Some(b.max(*align)));
1432                    }
1433                }
1434            }
1435        }
1436        cur = match &cur {
1437            AbstractValue::Place(p) => {
1438                if let PlaceBaseKey::Local(ix) = &p.base {
1439                    match result.values.get(&Local::from_usize(*ix)) {
1440                        Some(v) => v.clone(),
1441                        None => break,
1442                    }
1443                } else {
1444                    break;
1445                }
1446            }
1447            AbstractValue::Cast(inner, _) => (**inner).clone(),
1448            _ => break,
1449        };
1450    }
1451    best
1452}
1453
1454fn find_cmp_source<'tcx>(
1455    block: BasicBlock,
1456    cond: &Operand<'tcx>,
1457    body: &Body<'tcx>,
1458) -> (
1459    Option<BinOp>,
1460    Option<AbstractValue<'tcx>>,
1461    Option<AbstractValue<'tcx>>,
1462) {
1463    let place = match cond {
1464        Operand::Copy(place) | Operand::Move(place) => place,
1465        _ => return (None, None, None),
1466    };
1467    let bb = &body.basic_blocks[block];
1468    for stmt in &bb.statements {
1469        let StatementKind::Assign(assign) = &stmt.kind else { continue };
1470        if assign.0.local != place.local { continue };
1471        let Rvalue::BinaryOp(op, pair) = &assign.1 else { continue };
1472        if !matches!(op, BinOp::Lt | BinOp::Le | BinOp::Gt | BinOp::Ge | BinOp::Eq | BinOp::Ne) { continue; }
1473        return (Some(*op), Some(value_from_operand(&pair.0)), Some(value_from_operand(&pair.1)));
1474    }
1475    (None, None, None)
1476}
rapx/verify/verifier.rs

rapx/verify/
verifier.rs
