Crate weir

Expand description

Weir dataflow analysis crate.

This crate owns dataflow analyses and reusable fixed-point execution scaffolding. CPU functions in module internals are parity oracles only; the production surface builds Vyre programs for GPU dispatch.

§Example: dominators on a diamond CFG

use std::collections::{HashMap, HashSet};
use weir::ssa::{try_compute_dominators, Block, Cfg};

// CFG:  0 → {1, 2} → 3
let mut blocks = HashMap::new();
for (id, preds, succs) in [
    (0u32, vec![],     vec![1, 2]),
    (1,    vec![0],    vec![3]),
    (2,    vec![0],    vec![3]),
    (3,    vec![1, 2], vec![]),
] {
    blocks.insert(id, Block { id, preds, succs, defs: HashSet::new(), uses: HashSet::new() });
}

let idoms = try_compute_dominators(&Cfg { entry: 0, blocks }).unwrap();
assert_eq!(idoms[&1], 0);
assert_eq!(idoms[&2], 0);
assert_eq!(idoms[&3], 0); // merge point is dominated by the diamond head

Re-exports§

pub use soundness::DataflowEvidence;

Modules§

analysis_family: Unifying trait and generic drivers for Weir’s bitset fixed-point families.
callgraph: Call-graph construction with indirect resolution (DF-5).
control_dependence: Control-dependence query (does b execute on every path through a?).
cross_language: Cross-language FFI reachability analysis.
def_use: Def-use chain queries over SSA form (DF-11).
dispatch_decode: Shared GPU dispatch ABI helpers for Weir via paths.
dominators: Dominator-tree construction and query (DF-1).
escape: Escape analysis: does a pointer leave its defining frame? (DF-8).
escapes: Escape-set query over points-to sets.
fixed_point_batch: Batch fixed-point execution over multiple seed sets.
fixed_point_execution_plan: Scale-aware execution planning for fixed-point analyses.
fixed_point_execution_plan_cache: LRU cache for reusable fixed-point execution plans.
fixed_point_graph: Packed forward CSR graph buffers for fixed-point GPU wrappers.
fixed_point_resident: Resident-GPU fixed-point closure drivers.
fixed_point_resident_batch: Batch resident fixed-point execution.
fixed_point_resident_cache: Cache for resident fixed-point graph and plan reuse.
fixed_point_resident_frontier: Reusable resident frontier scratch buffers.
fixed_point_resident_plan: Resident execution plan construction.
fixed_point_scratch: Reusable host-side scratch for fixed-point graph preparation.
graph_layout: Shared graph-layout contracts for CSR normalization.
ifds: IFDS/IDE interprocedural dataflow framework (DF-4).
ifds_gpu: GPU-native IFDS/IDE driver (G3).
ifds_resident_batch: Batch resident IFDS execution.
ifds_resident_cache: Cache for resident IFDS graph reuse.
ifds_resident_direct_batch: Direct-resident IFDS batch facade.
ifds_resident_direct_prepare: Direct resident IFDS CSR preparation.
ifds_resident_direct_prepare_scratch: Reusable host scratch for direct-resident IFDS CSR preparation.
ifds_vyre_resident: Adapter from the common Vyre resident backend contract to Weir IFDS.
live: Live-variable analysis (DF-2 backward variant).
live_at: Liveness query: is variable v live at node n?
loop_sum: Loop summarization with widening+narrowing (DF-10).
may_alias: May-alias query packed as a bitset.
must_init: Must-initialization analysis.
points_to: Andersen points-to analysis (DF-3).
post_dominates: Post-dominator tree query.
range: Interval range propagation (DF-7).
range_check: Interval bound check for VSA results.
reachability_witness: Witness extraction from IFDS reachability results.
reaching: Reaching definitions analysis (DF-2).
reaching_def: Reaching-definitions query packed as a bitset.
reaching_def_summary: Compact reaching-definition summary queries.
relation_interchange: Relation import/export fixtures for IFDS and differential evidence.
resident_cache_identity
scc_query: Strongly-connected-component membership query.
slice: Backward program slicer (DF-6).
soundness: Soundness regime markers and evidence types.
ssa: SSA construction via Cytron’s algorithm (DF-1).
summary: Persistent procedure summaries (DF-9).
test_harness: Test harness for parity and conformance testing.
traversal_step: Forward and backward CFG traversal step builders.
value_set: Constant-value-set reachability query.

Macros§

define_analysis_family: Define a complete analysis family: marker type, AnalysisFamily impl, and all closure_* / resident_* wrapper functions.

Structs§

DynamicPrimitiveSoundness: Serializable soundness evidence for one primitive in a finding or release artifact.
DynamicSoundnessViolation: Mechanical rejection reason for an invalid dynamic soundness composition.
PrimitiveSoundness: Soundness evidence for one primitive in a composed pipeline.
SoundnessViolation: Mechanical rejection reason for an invalid soundness composition.

Enums§

PrecisionContract: Precision contract requested by a consumer pipeline.
Soundness: Soundness regime of a dataflow primitive.

Traits§

SoundnessTagged: Trait for types that carry a soundness marker.

Functions§

validate_dynamic_pipeline: Validate a serializable primitive pipeline against a consumer precision contract, returning the composed soundness marker on success.
validate_dynamic_primitive: Validate one serializable primitive against a consumer precision contract.
validate_pipeline: Validate that a primitive pipeline can satisfy a consumer precision contract, returning the composed soundness marker on success.
validate_primitive: Validate one primitive against a consumer precision contract.

Crate weir

Crate weir Copy item path

§Example: dominators on a diamond CFG

Re-exports§

Modules§

Macros§

Structs§

Enums§

Traits§

Functions§

Crate weir