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 MIR body and builds symbolic and pointer chains. Holds analysis state such as type mappings, value domains and constraints.

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 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, AAResult>, ) -> 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, AAResult>, )

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, AAResult>, )

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, AAResult>, 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, AAResult>, args: &Box<[Spanned<Operand<'_>>]>, )

Merge function-level alias results into internal chains and value domains. Uses cached alias analysis (AAResult) 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.

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, AAResult>, fn_span: Span, fn_result: UnsafeApi, generic_mapping: FxHashMap<String, Ty<'tcx>>, )

Entry point for handling standard library unsafe API calls and verifying their contracts.

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

Dispatcher function that validates a specific contract type.

fn is_base_determined(&self, base_local: usize) -> bool

Taint Analysis: Check if the base pointer comes from a determined/aligned source. Sources considered determined/aligned:

1. References (Stack allocation) -> &x
2. AddressOf (Stack allocation) -> &raw x
3. Known aligned API calls -> as_ptr, as_mut_ptr, alloc

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

pub fn show_error_info(&self, arg: usize)

impl<'tcx> BodyVisitor<'tcx>

Impl block for Align check Align checking functions

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

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

First check for Align. If this var has contextual invariant state (cis), like: #[rapx::proof::Align::(x, usize)] pub fn test(x: *const usize) { … } CIS will record ‘x: Align(usize)’ information for align check

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

Second check for Align. If no offset, check the type of ptr an its pointed object’s type directly

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

Third check for Align. If ptr has Offset, use Z3 to solve constraints. Assuming offset_op is the accumulated offset from base_local.

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

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

Updates the alignment state of the given local variable. is_aligned = true -> Aligned is_aligned = false -> Unaligned

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

Checks if the argument satisfies the alignment requirements of the contract. Retrieves the pre-computed state from the graph and compares types.

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

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

Attempts to prove a stricter alignment for the base pointer using Z3 and path constraints.

fn check_offset_is_aligned( &self, _base_local: usize, offset: &AnaOperand, align: u64, ) -> bool

Checks if the offset is a multiple of the required alignment using Z3.

fn check_cumulative_offset_aligned( &self, _base_local: usize, acc_def: &SymbolicDef<'_>, curr_op: &AnaOperand, align: u64, ) -> bool

Checks if (AccumulatedDef + CurrentOp) % Align == 0 using Z3.

fn operand_to_symbolic_def(&self, op: AnaOperand) -> SymbolicDef<'tcx>

fn combine_offsets( &self, def: SymbolicDef<'tcx>, op: AnaOperand, ) -> SymbolicDef<'tcx>

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