WPDS Dataflow Engine
====================

Overview
========

The **WPDS engine** in ``lib/Dataflow/WPDS`` solves distributive
interprocedural data-flow problems by encoding them as
**Weighted Pushdown Systems (WPDS)**.
It leverages the WALi library (``lib/Solvers/WPDS``) to compute
post*/pre* reachability over a pushdown system that models both
control-flow and call/return behavior.

* **Location**: ``lib/Dataflow/WPDS``
* **Core classes**: ``InterProceduralDataFlowEngine``,
  ``GenKillTransformer``, ``DataFlowFacts``

Core Idea
=========

Instead of building an exploded super-graph (as IFDS/IDE do), the WPDS
engine:

* constructs a pushdown system whose rules correspond to CFG edges and
  call/return transitions,
* attaches **weights** that model GEN/KILL behavior on a set of facts,
* runs a standard WPDS algorithm (post* or pre*) to compute the least
  fixed point.

Clients typically provide a function
``GenKillTransformer *createTransformer(Instruction *I)`` which
captures the effect of each instruction on the fact set.

Example Analyses
================

Constant Propagation
--------------------

``WPDSConstantPropagation`` demonstrates a forward **constant
propagation** analysis:

* facts track variables that currently hold constant values,
* GEN adds variables whose values are known to be constant at a point,
* KILL removes variables whose values become non-constant,
* the interprocedural engine propagates these facts across calls.

Liveness
--------

``WPDSLivenessAnalysis`` performs a backward **liveness analysis**:

* GEN collects variables used at an instruction (including loads and
  uses in stores),
* KILL records variables defined (or overwritten) at that point,
* the WPDS formulation makes the analysis naturally interprocedural.

Taint Analysis
--------------

``WPDSTaintAnalysis`` is a WPDS-based **taint analysis**:

* facts represent tainted values,
* GEN introduces taint at configurable source calls,
* KILL removes taint at sanitizers,
* the engine reports flows of tainted data into dangerous sinks
  (e.g., ``system``, ``exec``, ``strcpy``).

Uninitialized Variables
-----------------------

``WPDSUninitializedVariables`` shows a forward analysis for detecting
reads from **possibly uninitialized memory**:

* GEN marks newly allocated locals (``alloca``) as uninitialized,
* KILL removes a location when it is definitely initialized by a store,
* any load whose pointer appears in the ``IN`` set is reported as a
  potential use of uninitialized data.

Compared to IFDS/IDE, the explicit pushdown-system encoding makes the
call stack and recursion behavior more visible and can be advantageous
for certain classes of interprocedural problems.