Struct BodyVisitor 

pub struct BodyVisitor<'tcx> {
    pub tcx: TyCtxt<'tcx>,
    pub def_id: DefId,
    pub safedrop_graph: SafeDropGraph<'tcx>,
    pub local_ty: HashMap<usize, PlaceTy<'tcx>>,
    pub visit_time: usize,
    pub check_results: Vec<CheckResult>,
    pub generic_map: HashMap<String, HashSet<Ty<'tcx>>>,
    pub proj_ty: HashMap<usize, Ty<'tcx>>,
    pub chains: DominatedGraph<'tcx>,
    pub value_domains: HashMap<usize, ValueDomain<'tcx>>,
    pub path_constraints: Vec<SymbolicDef<'tcx>>,
}

Visitor that traverses one MIR body and builds symbolic and pointer state.

Fields

tcx: TyCtxt<'tcx>

def_id: DefId

safedrop_graph: SafeDropGraph<'tcx>

local_ty: HashMap<usize, PlaceTy<'tcx>>

visit_time: usize

check_results: Vec<CheckResult>

generic_map: HashMap<String, HashSet<Ty<'tcx>>>

proj_ty: HashMap<usize, Ty<'tcx>>

chains: DominatedGraph<'tcx>

value_domains: HashMap<usize, ValueDomain<'tcx>>

path_constraints: Vec<SymbolicDef<'tcx>>

Implementations

impl<'tcx> BodyVisitor<'tcx>

pub fn handle_std_unsafe_call( &mut self, _dst_place: &Place<'_>, def_id: &DefId, args: &[Spanned<Operand<'_>>], _path_index: usize, _fn_map: &FxHashMap<DefId, FnAliasPairs>, fn_span: Span, generic_mapping: FxHashMap<String, Ty<'tcx>>, )

Instantiate and verify contracts at a standard-library unsafe API callsite.

pub fn check_contract( &mut self, arg: usize, _args: &[Spanned<Operand<'_>>], contract: PropertyContract<'tcx>, generic_mapping: &FxHashMap<String, Ty<'tcx>>, func_name: String, fn_span: Span, idx: usize, ) -> bool

Dispatch one instantiated contract to the checker for that safety tag.

impl<'tcx> BodyVisitor<'tcx>

pub fn insert_checking_result( &mut self, sp: &str, is_passed: bool, func_name: String, fn_span: Span, idx: usize, )

Record one property-checking result for the current unsafe callsite.

pub fn insert_failed_check_result( &mut self, func_name: String, fn_span: Span, idx: usize, sp: &str, )

Record one failed safety-property check for an unsafe callsite.

pub fn insert_successful_check_result( &mut self, func_name: String, fn_span: Span, idx: usize, sp: &str, )

Record one successful safety-property check for an unsafe callsite.

pub fn show_error_info(&self, arg: usize)

Print graph context when a checker cannot locate a requested node.

impl<'tcx> BodyVisitor<'tcx>

pub fn check_align(&self, arg: usize, contract_required_ty: Ty<'tcx>) -> bool

Prove that arg satisfies the contract Align(arg, contract_required_ty).

The proof order is contract facts, then symbolic offset proof, then direct graph/OTS alignment. The offset proof is tried before the direct check because derived pointers normally carry their key alignment evidence in offset_from rather than in the immediate pointee type alone.

fn check_align_from_facts( &self, arg: usize, required_layout: &PlaceTy<'tcx>, ) -> bool

Check alignment facts that came directly from caller annotations.

fn check_align_directly( &self, pointer_id: usize, required_ty: PlaceTy<'tcx>, ) -> bool

Check alignment from the current graph state and pointed object type.

fn check_offset_align_with_z3( &self, op: BinOp, base_local: usize, offset_op: AnaOperand, stride_layout: PlaceTy<'tcx>, contract_required_ty: Ty<'tcx>, ) -> bool

Use Z3 to prove that pointer arithmetic preserves required alignment.

The formula models result = base +/- index * stride and proves that whenever the base address is aligned for each possible base alignment, the result address is aligned for every required alignment.

fn get_ptr_offset_info( &self, arg: usize, ) -> Option<(BinOp, usize, AnaOperand, PlaceTy<'tcx>)>

Return the pointer-offset summary attached to a graph node, if present.

pub fn update_align_state(&mut self, ptr_local: usize, is_aligned: bool)

Refine the alignment state after a branch such as ptr.is_aligned().

is_aligned == true records an Aligned(pointee_ty) fact; false records Unaligned(pointee_ty). The visitor calls this on both the condition operand and, when traceable, the source pointer.

pub fn check_align_by_pre_computed_state( &self, arg: usize, contract_required_ty: Ty<'tcx>, ) -> bool

Check a previously computed alignment state without re-running offset proof.

fn two_types_cast_check(src: PlaceTy<'tcx>, dest: PlaceTy<'tcx>) -> bool

Return true when every possible source alignment implies the destination alignment.

fn _try_refine_alignment(&self, base_local: usize, current_align: u64) -> u64

Try to strengthen a base pointer’s alignment with numeric constraints.

fn _check_offset_is_aligned(&self, offset: &AnaOperand, align: u64) -> bool

Prove that a symbolic offset is a multiple of align.

fn _check_cumulative_offset_aligned( &self, acc_def: &SymbolicDef<'tcx>, curr_op: &AnaOperand, align: u64, ) -> bool

Prove that an accumulated symbolic offset plus one current operand is aligned.

fn symbolic_def_to_bv<'a>( &self, ctx: &'a Context, vars: &HashMap<usize, BV<'a>>, def: &SymbolicDef<'tcx>, ) -> BV<'a>

Convert a local symbolic definition to a Z3 bit-vector expression.

impl<'tcx> BodyVisitor<'tcx>

pub fn check_non_zst(&self, arg: usize) -> bool

Return true when the modeled object reached by arg is zero-sized.

The API name is kept for compatibility with existing call sites, but the current implementation returns true for ZST objects.

pub fn check_inbound( &self, _arg: usize, _length_arg: ContractExpr<'tcx>, _contract_ty: Ty<'tcx>, ) -> bool

Check the in-bounds contract for a pointer and element count.

This is intentionally conservative until length constraints from contract facts and symbolic values are connected into one proof procedure.

impl<'tcx> BodyVisitor<'tcx>

pub fn check_init(&self, arg: usize) -> bool

Check each field’s init state in the graph tree, or the node itself for leaves.

impl<'tcx> BodyVisitor<'tcx>

pub fn check_allocator_consistency( &self, _func_name: String, _arg: usize, ) -> bool

Placeholder for allocator-consistency checking.

pub fn check_valid_string(&self, _arg: usize) -> bool

Placeholder for UTF-8 string validity checking.

pub fn check_valid_cstr(&self, _arg: usize) -> bool

Placeholder for nul-terminated C string validity checking.

pub fn check_valid_num(&self, predicates: &[NumericPredicate<'tcx>]) -> bool

Check numeric predicates that are already fully constant.

Non-constant predicates currently return true to preserve the previous placeholder behavior; a later NumericProver should discharge them with symbolic values and path constraints.

fn check_constant_numeric_predicate( &self, predicate: &NumericPredicate<'tcx>, ) -> bool

Evaluate one numeric predicate when both sides are constants.

fn eval_constant_contract_expr(expr: &ContractExpr<'tcx>) -> Option<u128>

Evaluate a contract expression when it is a literal-only expression.

pub fn check_alias(&self, _arg: usize) -> bool

Placeholder for aliasing constraints.

impl<'tcx> BodyVisitor<'tcx>

pub fn check_non_null(&self, arg: usize) -> bool

Check that a pointer’s modeled target is non-null.

impl<'tcx> BodyVisitor<'tcx>

pub fn check_allocated(&self, _arg: usize) -> bool

Placeholder for allocation provenance checking.

pub fn check_valid_ptr( &self, arg: usize, length_arg: ContractExpr<'tcx>, contract_ty: Ty<'tcx>, ) -> bool

Check the composite ValidPtr contract.

pub fn check_deref( &self, arg: usize, length_arg: ContractExpr<'tcx>, contract_ty: Ty<'tcx>, ) -> bool

Check that a pointer can be dereferenced for the requested extent.

pub fn check_ref_to_ptr( &self, arg: usize, length_arg: ContractExpr<'tcx>, contract_ty: Ty<'tcx>, ) -> bool

Check the composite pointer-to-reference conversion contract.

impl<'tcx> BodyVisitor<'tcx>

pub fn check_typed(&self, arg: usize) -> bool

Check whether the value the pointer reaches is valid for its tracked type.

impl<'tcx> BodyVisitor<'tcx>

pub fn new(tcx: TyCtxt<'tcx>, def_id: DefId, visit_time: usize) -> Self

Construct a new BodyVisitor for def_id. Initializes helper structures and generic type map.

impl<'tcx> BodyVisitor<'tcx>

=== Partition: Path-sensitive analysis driver === Compute and iterate control-flow paths and merge results.

pub fn path_forward_check( &mut self, fn_map: &FxHashMap<DefId, FnAliasPairs>, ) -> InterResultNode<'tcx>

Perform path-sensitive forward analysis. Uses Tarjan-produced paths and performs per-path symbolic and pointer analysis. Returns an InterResultNode merging all path results.

pub fn path_analyze_block( &mut self, block: &BasicBlockData<'tcx>, path_index: usize, bb_index: usize, next_block: Option<usize>, fn_map: &FxHashMap<DefId, FnAliasPairs>, )

Analyze one basic block: process statements then its terminator for the current path.

pub fn get_all_paths( &mut self, ) -> HashMap<Vec<usize>, Vec<(Place<'tcx>, Place<'tcx>, BinOp)>>

Retrieve all paths and optional range-based constraints for this function. Falls back to safedrop graph paths if range analysis did not produce constraints.

impl<'tcx> BodyVisitor<'tcx>

pub fn path_analyze_statement( &mut self, statement: &Statement<'tcx>, _path_index: usize, )

Dispatch analysis for a single MIR statement (assignments, intrinsics, etc.).

pub fn path_analyze_assign( &mut self, lplace: &Place<'tcx>, rvalue: &Rvalue<'tcx>, path_index: usize, )

Handle assignment rvalues: record symbolic defs and update pointer/alias chains.

pub fn get_ptr_pointee_layout(&self, ptr_local: usize) -> PlaceTy<'tcx>

Get the layout of the pointee type of a pointer or reference.

impl<'tcx> BodyVisitor<'tcx>

=== Partition: Terminator handling === Terminator handling: calls, drops and branch-switch translation into constraints.

pub fn path_analyze_terminator( &mut self, terminator: &Terminator<'tcx>, path_index: usize, bb_index: usize, next_block: Option<usize>, fn_map: &FxHashMap<DefId, FnAliasPairs>, )

Analyze a MIR terminator (calls, drops, switches, etc.) for a path. Updates chains/value domains based on call, drop and switch semantics.

pub fn get_ty_by_place(&self, p: usize) -> Ty<'tcx>

Return the MIR type of a local given its numeric p index.

pub fn update_fields_states(&mut self, inter_result: InterResultNode<'tcx>)

Update field state graph from an inter-procedural result node.

fn get_generic_mapping( &self, raw_list: &[GenericArg<'tcx>], def_id: &DefId, generic_mapping: &mut FxHashMap<String, Ty<'tcx>>, )

Get the generic name to an actual type mapping when used for a def_id. If current def_id doesn’t have generic, then search its parent. The generic set include type and allocator. Example: generic_mapping (T -> u32, A -> std::alloc::Global)

pub fn handle_call( &mut self, dst_place: &Place<'tcx>, def_id: &DefId, args: &Box<[Spanned<Operand<'tcx>>]>, path_index: usize, fn_map: &FxHashMap<DefId, FnAliasPairs>, fn_span: Span, generic_mapping: FxHashMap<String, Ty<'tcx>>, )

Handle a function call: record symbolic Call, check unsafe contracts, and merge aliases.

fn set_bound( &mut self, def_id: &DefId, dst_place: &Place<'tcx>, args: &Box<[Spanned<Operand<'_>>]>, )

For certain library calls (e.g. slice::len), bind computed values into object contracts.

pub fn handle_ret_alias( &mut self, dst_place: &Place<'tcx>, def_id: &DefId, fn_map: &FxHashMap<DefId, FnAliasPairs>, args: &Box<[Spanned<Operand<'_>>]>, )

Merge function-level alias results into internal chains and value domains. Uses cached alias analysis (FnAliasPairs) to connect return/arg relationships.

pub fn compute_function_summary(&self) -> FunctionSummary<'tcx>

Compute a compact FunctionSummary for this function based on the return local (_0). If the return resolves to a param or const expression, include it in the summary.

fn resolve_symbolic_def( &self, def: &SymbolicDef<'tcx>, depth: usize, ) -> Option<SymbolicDef<'tcx>>

Resolve a SymbolicDef into a simplified form referencing params or constants. For example, given _1 = add(_2, _3), attempt to express the result in terms of params.

fn resolve_local( &self, local_idx: usize, depth: usize, ) -> Option<SymbolicDef<'tcx>>

Resolve a local’s symbolic definition by consulting the value_domains map.

pub fn handle_offset_call( &mut self, dst_place: &Place<'tcx>, def_id: &DefId, args: &Box<[Spanned<Operand<'tcx>>]>, )

Handle calls to pointer offset functions (e.g., ptr::add, ptr::sub).

fn handle_switch_int( &mut self, discr: &Operand<'tcx>, targets: &SwitchTargets, next_bb: usize, )

Handle SwitchInt: Convert branch selections into constraints AND refine abstract states. Convert a SwitchInt terminator into path constraints and refine state when possible.

The function maps the branch target taken into a concrete equality/inequality constraint on the discriminator local and attempts to refine abstract states (e.g. alignment) when the condition corresponds to recognized helper calls.

fn refine_state_by_condition(&mut self, cond_local: usize, matched_val: u128)

Entry point for refining states based on a condition variable’s value.

fn apply_condition_refinement( &mut self, func_name: &str, args: &Vec<AnaOperand>, matched_val: u128, )

Dispatcher: Applies specific state updates based on function name and return value.

pub fn find_source_var(&self, start_local: usize) -> usize

Helper: Trace back through Use/Cast/Copy to find the definitive source local.

pub fn apply_function_summary( &mut self, dst_local: usize, summary: &FunctionSummary<'tcx>, args: &Vec<usize>, )

Apply function summary to update Visitor state and Graph

fn resolve_summary_def( &self, def: &SymbolicDef<'tcx>, args: &Vec<usize>, ) -> Option<SymbolicDef<'tcx>>

Resolve a definition from Function Summary (using Param indices) into a concrete SymbolicDef (using Caller’s Locals).

pub fn set_constraint( &mut self, constraint: &Vec<(Place<'tcx>, Place<'tcx>, BinOp)>, )

Apply path constraints into chains and propagate simple constant equalities into value_domains for later symbolic checks.

pub fn get_layout_by_place_usize(&self, place: usize) -> PlaceTy<'tcx>

Return layout information (align, size) or Unknown for a place via chain-derived type.

pub fn visit_ty_and_get_layout(&self, ty: Ty<'tcx>) -> PlaceTy<'tcx>

Determine layout info (align,size) for a type. For generics, collect possible concrete layouts.

pub fn handle_binary_op( &mut self, first_op: &Operand<'_>, bin_op: &BinOp, second_op: &Operand<'_>, path_index: usize, )

Handle special binary operations (e.g., pointer offset) and extract operand places.

pub fn handle_proj(&mut self, is_right: bool, place: Place<'tcx>) -> usize

Convert a MIR Place (with projections) into an internal numeric node id. Handles deref and field projections by consulting/creating chain nodes.

fn record_value_def(&mut self, local_idx: usize, def: SymbolicDef<'tcx>)

Record or overwrite the symbolic definition for a local in value_domains.

fn lift_operand(&mut self, op: &Operand<'tcx>) -> Option<AnaOperand>

Convert a MIR Operand into an AnaOperand (local node id or constant) when possible.

pub fn trace_base_ptr(&self, local: usize) -> Option<(usize, u64)>

Trace a pointer value back to its base local and accumulate byte offsets. Returns (base_local, total_offset) when traceable.

Example: p3 = p2.byte_offset(v2), p2 = p1.byte_offset(v1) returns (p1, v1 + v2) for trace_base_ptr(p3).

impl<'tcx> BodyVisitor<'tcx>

pub fn display_combined_debug_info(&self)

Display a combined debug table merging DominatedGraph and ValueDomain info. Handles different lengths of variables in graph (includes heap nodes) vs domains.

pub fn display_path_constraints(&self)

Pretty-print the collected path constraints for debugging. Display the true conditions in all branches.

pub fn display_value_domains(&self)

Display all variables’ symbolic definitions and value constraints. Pretty-print value domains (symbolic definitions and constraints) for debug.

fn safe_truncate(&self, s: &str, max_width: usize) -> String

Truncate a string to max_width preserving character boundaries. Returns a shortened string with “..” appended when truncation occurs.

fn format_symbolic_def(&self, def: Option<&SymbolicDef<'tcx>>) -> String

Convert a SymbolicDef into a short human-readable string for display.

fn binop_to_symbol(&self, op: &BinOp) -> &'static str

Map MIR BinOp to a human-friendly operator string.

pub fn display_path_dot(&self, path: &[usize])

Display the path in DOT format.