Module graph 

Structs

BlockConstantInfo

Per-block info collected during construction for path reachability analysis. Each block’s assignments, constants, and copy chains are stored together so they can be read with a single index lookup.

ComparisonSource

Records the origin of a boolean temporary produced by a binary comparison during guard-clause evaluation.

ConstraintHash

Hash of the constraint state accumulated along a path prefix.

DiscriminantInfo

Enum discriminant metadata used by [check_switch_transition].

PathEnumerator

Builds a PathTree by depth-first enumeration of whole-CFG paths.

PathGraph

CFG augmented with per-block constant info and discriminant metadata for path reachability analysis.

SccKey

Key for PathEnumerator::scc_paths and PathEnumerator::visited_sccs and PathEnumerator::visited_sccs: which SCC entry block, with what constraint state, and how many additional postfix repeats are allowed.

SccPath

A single enumerated acyclic path through an SCC region.

Constants

AGGREGATE_FIELD_MULT 🔒

Encode a (local, field_index) pair into a single usize.

AGGREGATE_FIELD_SENTINEL 🔒

SCC_MAX_DEPTH 🔒

Maximum DFS depth for intra-SCC path enumeration.

SCC_MAX_PATH_LEN 🔒

Maximum path length within an SCC traversal.

SCC_MAX_SEEN_PATHS 🔒

Maximum number of distinct paths collected per SCC.

SCC_PATH_CACHE_LIMIT 🔒

Bounded cache size for SCC path enumeration.

WHOLE_CFG_PATH_DEPTH_LIMIT 🔒

Maximum DFS depth for whole-CFG path enumeration.

WHOLE_CFG_PATH_LIMIT 🔒

Maximum number of whole-CFG paths collected before stopping enumeration.

Functions

check_postfix_segment 🔒

Check whether the current entry→entry sub-path introduces a new block sequence (not just new blocks). Different branch choices inside the SCC produce different sequences even when all block IDs have already been seen, e.g. if i % 2 == 0 { A } else { B } alternates between two paths through the same set of blocks on successive loop iterations.

decode_aggregate_field 🔒

encode_aggregate_field 🔒

extract_segment 🔒

first_field_projection 🔒

resolve_switch_target 🔒

Resolve a concrete discriminant value to the corresponding SwitchInt successor block index.