weir

GPU-resident dataflow primitives over Vyre IR.

Weir 0.1.0 is the standalone dataflow crate in the Vyre 0.4.2 release train. The release package token is weir@0.1.0.

cargo add weir

The default feature set is empty (default = []), library consumers that only need program builders get a minimal compile. Enable serde for release-facing witness and soundness evidence types: cargo add weir --features serde. The standalone serde_evidence example declares required-features = ["serde"] so feature-minimal builds do not accidentally compile serialization evidence against a disabled feature. Enable cpu-parity to pull in the host reference oracles used by the df_* integration tests and parity bench gates.

Stats at a glance

Feature flags

Weir is the dataflow layer that sits above vyre. It builds compiler-analysis and security-analysis primitives as composable vyre::Programs: SSA, reaching definitions, IFDS, points-to, range checks, slicing, callgraph queries, and proof witness extraction.

What Weir is

Weir turns graph/fact buffers into dataflow results.

frontend graph buffers -> weir primitive -> vyre::Program -> CUDA/WGPU backend
                                             |
                                             +-> CPU oracle for parity

Frontends own source-language parsing. Weir owns the dataflow computation after the program has been lowered into graph and fact buffers.

CPU reference routines live under weir::oracle and are for parity, conformance, fuzzing, and release evidence only. Production consumers should build weir::* Programs and dispatch them through a concrete Vyre GPU backend; direct cpu_ref / solve_cpu / compute_cpu helpers are not part of the production surface. Any remaining crate-private helpers with those names are deprecated reference oracles and are gated by tests so they cannot become fallback hooks.

What Weir is not

Weir is not a C parser, rule language, scanner, or raw shader library. It does not emit CUDA, WGSL, or PTX directly. Every GPU path is expressed through Vyre IR so backends and conformance stay centralized.

Current release surface

Core modules include:

Analysis families

Weir's four bitset fixed-point analysis families (reaching, live, points_to, slice) share a single generic driver ladder. The AnalysisFamily trait (see src/analysis_family.rs) captures the invariant machinery:

• KIND: analysis discriminant for plan/graph kind checking.
• NAME: human-readable prefix for error messages.
• build_program: constructs the Vyre transfer-step Program for one iteration.
• prepare_graph / prepare_graph_with_scratch: builds invariant CSR graph buffers.
• closure_labels / resident_labels: label bundles for telemetry and diagnostics.

New families are added with the define_analysis_family! declarative macro:

crate::define_analysis_family! {
    family: MyFamily,
    kind: FixedPointAnalysisKind::MyAnalysis,
    name: "my_analysis_closure",
    program_builder: my_analysis_step,
    graph_prep: prepare_my_graph,
    graph_prep_scratch: prepare_my_graph_with_scratch,
    input_buffer: "fin",
    output_buffer: "fout",
    closure_prefix: my_analysis_closure,
    resident_prefix: my_analysis_closure_resident,
    word_capacity: "my_analysis_closure",
    frontier_output: "frontier",
    resident_capacity: "my_analysis_closure resident",
    resident_output: "frontier",
    visibility: pub,
}

The macro generates the full suite of closure_* and resident_* wrapper functions so call sites stay stable during migration. See TESTING.md for the full guide on adding a family.

IFDS to witness flow

The full proof path is:

1. Build or receive an exploded IFDS supergraph.
2. Dispatch the Weir GPU step to produce reached nodes; use weir::oracle only for parity evidence.
3. Convert exploded (proc, block, fact) nodes into statement reachability with exploded_reachability_to_statement_mask.
4. Prepare the proof graph once with prepare_witness_graph.
5. Extract one or many source-to-sink witnesses with extract_path_prepared.

The prepared graph path avoids rebuilding reverse CSR state for every finding.

Soundness

Every primitive soundness contract is explicit:

Compositions must join soundness conservatively. Use PrecisionContract and PrimitiveSoundness to reject pipelines whose primitive soundness cannot satisfy the consumer contract.

use weir::soundness::{validate_pipeline, PrecisionContract, PrimitiveSoundness, Soundness};

let joined = validate_pipeline(
    PrecisionContract::ZeroFalsePositive,
    &[PrimitiveSoundness::new("weir::ssa", Soundness::Exact)],
)?;
assert_eq!(joined, Soundness::Exact);
# Ok::<(), weir::soundness::SoundnessViolation>(())

Minimal example

use weir::reachability_witness::{
    exploded_reachability_to_statement_mask, extract_path_prepared,
    prepare_witness_graph, NodeAttr, PathSeed,
};

fn main() -> Result<(), Box<dyn std::error::Error>> {
    let reached = vec![
        vyre_primitives::graph::exploded::encode_node(0, 0, 0)?,
        vyre_primitives::graph::exploded::encode_node(0, 1, 0)?,
    ];
    let block_to_statement = vec![0, 1];
    let source_reach =
        exploded_reachability_to_statement_mask(&reached, 2, &block_to_statement, Some(0), 2)?;

    let attrs = vec![
        NodeAttr { byte_start: 0, byte_end: 4, file_idx: 0 },
        NodeAttr { byte_start: 5, byte_end: 9, file_idx: 0 },
    ];
    let files = vec!["example.c".to_string()];
    let descriptions = vec!["source".to_string(), "sink".to_string()];
    let edge_offsets = vec![0, 1, 1];
    let edge_targets = vec![1];
    let edge_kind_mask = vec![vyre_primitives::predicate::edge_kind::ASSIGNMENT];
    let graph = prepare_witness_graph(
        &edge_offsets,
        &edge_targets,
        &edge_kind_mask,
        &attrs,
        &files,
        &descriptions,
        "c-c11",
    );
    let seed = PathSeed {
        source_file: "example.c".to_string(),
        source_node: 0,
        sink_file: "example.c".to_string(),
        sink_node: 1,
    };
    let path = extract_path_prepared(&seed, &source_reach, &[], &graph)?;
    assert_eq!(path.statements.len(), 2);
    Ok(())
}

Release status

For this release, Weir's critical path is IFDS reachability plus witness extraction. Source parsing and full frontend integration live outside this crate.

Release evidence:

• release/evidence/weir/weir-analysis-api-matrix.json
• release/evidence/weir/weir-vyre-integration-tests.json
• release/evidence/weir/weir-readme-contracts.json
• release/evidence/weir/weir-flow-release-contracts.json

Release evidence

Release readiness for this document is proven through the Vyre/Weir evidence manifest and generated artifacts under release/evidence/. Claims here must map to concrete gate output, benchmark output, conformance output, parser corpus output, or documentation proof files before the release requirement can be closed.

Weir release claims also depend on the Vyre backend release path: dataflow programs must remain backend-neutral Vyre IR while the release train proves CUDA as the NVIDIA fast path through vyre-driver-cuda@0.4.2 and WGPU as the secondary portable GPU backend through vyre-driver-wgpu@0.4.2.

Performance budget (host micro-LO)

Regression gates live in benches/primitive_micro.rs. Re-baseline with:

cargo bench -p weir --bench primitive_micro

Document median time per iteration; CI should compare against the constants below multiplied by the regression factor.

Hot-path rules enforced in code:

• No format!() on GPU decode success paths; cold diagnostics use error_format + write!.
• Dense u32 domains use dense_domain::DenseU32Slots instead of HashMap where ids are bounded (SSA dominator postorder index).
• dispatch_decode::unpack_exact_u32_into reuses caller Vec<u32> and uses bytemuck on little-endian hosts.
• CSR layout hashing uses word-slice FNV mixing without per-word to_le_bytes allocation on LE hosts.

Testing

Quick-start commands:

# Fastest check, lib-only unit tests (~1,400 tests, ~20 s)
cargo test --lib

# Full host check including doc tests and examples
cargo test --lib && cargo test --doc && cargo test --examples

# Full parity gate (requires CUDA-capable host + `cpu-parity`)
cargo test --features cpu-parity

Weir's testing strategy is documented in TESTING.md, covering:

• The 4-vector strategy (Test Density, Performance & Innovation, Deduplication & Legoblock, Corpus & Fuzz).
• How to use FakeResidentBackend, CsrFactory, IfdsProblemBuilder, and DominatorFixture.
• Test categories: unit, integration, property-based, contract, doc, example, adversarial.
• How to run the full test suite and how to add a new analysis family.

Performance

Detailed optimization decisions, benchmark methodology, and profiling instructions live in PERF.md. Key decisions include:

• GPU telemetry threshold at 64 words.
• bitset::equal for unified host/device convergence.
• ScratchPool for zero-allocation staging.
• SIMD oracle feature-gated and performance-neutral.
• Dominator GPU threshold at 1,000 nodes.

See INVENTORY.md for full crate layout and test coverage.