Data Flow Analysis Frameworks

Lotus implements several distinct dataflow analysis frameworks, each optimized for different problem classes and precision/performance trade-offs. This page provides an architectural overview of the frameworks, explains when to use each, and documents their core abstractions.

Framework Overview

Lotus provides several compiled libraries under lib/Dataflow/, each implementing a distinct algorithmic approach:

Dataflow Engines

CMake Target	Namespace	Primary Solver Classes	Key Headers	Scope
IFDS	ifds::	IFDSSolver, IDESolver, PathAwareIDESolver	IFDSSolver.h, IDESolver.h	Interprocedural
MONODataFlow	mono::	IntraMonoSolver, InterMonoSolver	IntraSolver.h, InterSolver.h	Intra/Interprocedural
WPDSDataFlow	wpds::	InterProceduralDataFlowEngine	InterProceduralDataFlow.h	Interprocedural
APADataFlow	elimination::	IntraEliminationSolver, InterEliminationSolver	IntraSolver.h	Intra/Interprocedural
NPADataFlow	npa::	BitVectorSolver, ForwardInterEngine, BackwardInterEngine	NPALLVMDriver.h, IntraEngine.h	Intra/Interprocedural
VASCODataFlow	vasco::	ForwardInterProceduralAnalysis, BackwardInterProceduralAnalysis	ForwardInterProceduralAnalysis.h	Interprocedural

When to Use Each Framework

Selecting the right framework depends heavily on the properties of the dataflow problem being solved:

Framework Selection Guide

Framework	Problem Class	Context Sensitivity	Typical Use Cases
IFDS	Distributive (gen-kill, set-union)	Call-string (implicit)	Taint analysis, uninitialized variables, reaching definitions.
IDE	Distributive + value	Tabulation + edge	Linear analysis, type-state.
Mono (Intra)	Arbitrary monotone lattice	None (Intraprocedural)	Simple lattice problems, worklist fixpoint iteration.
Mono (Inter)	Arbitrary monotone lattice	K-call-string	Constant-prop, context-sensitive analyses.
WPDS	Weighted pushdown reachability	CFL-reachability	Stack-aware analyses, demand-driven queries.
APA	Arbitrary meet/transfer	None (Intraprocedural)	Meet-over-all-paths, path expressions, elimination benchmarks.

The lotus-dfa tool (located in tools/dataflow/ and built from lotus-dfa-diff.cpp) can be used to perform differential testing across these different engines for a given problem class.

Detailed Engine Documentation

• Algebraic Program Analysis (APA)
  • Overview
  • Main components
  • Order-aware elimination
  • Interprocedural Forward Summary Solver
  • EAN equality saturation
  • TranslAPA baseline
  • Modular interprocedural summary solver
  • Typical use cases
  • Analysis Tooling & Evaluation
  • See also
• Demand-Driven APA
  • Overview
  • Key Features
  • Dependencies
  • Usage
• Control Flow Support
  • Overview
  • Main components
  • Why it exists
  • Choosing a graph view
  • See also
• Monotone Dataflow Engine
• Overview
• Implementation Layout
• Core Idea
• Abstract Domain Contract
• Example Analyses
  • Live Variables (SSA)
  • Reachable Instructions
• IFDS / IDE Engine
• Overview
• IFDS: Set-Valued Problems
  • Example — Taint Analysis
• IDE: Value-Enriched Problems
  • Example — Linear Constant Propagation
  • Example — Typestate Analysis
• Usage
• Analysis Sessions and Graph Providers
• Sparse Execution
• Command-Line Tool: lotus-check –engine=taint
  • Key Options
  • Examples
• VASCO Value-Context Framework
• Overview
• Why VASCO
• Value Contexts
• Algorithm Sketch
• Core API
  • Generic Interfaces
  • Directional Solvers
• Results
  • Context-sensitive results
  • Merged meet-over-valid-paths results
• LLVM Instantiation in Lotus
• Parallel Context Scheduling
  • Core Idea
  • Versioned Summary Replay
  • Public API
  • Configuration
  • Usage Example
  • Correctness Invariants
  • Design Document
• Current Scope and Caveats
• Relationship to Other Lotus Engines
• WPDS Dataflow Engine
• Overview
• Core Idea
• Backend selection and prepared sessions
• Example Analyses
  • Constant Propagation
  • Liveness
  • Taint Analysis
  • Uninitialized Variables
• Newtonian Program Analysis (NPA)
• Overview
• Conceptual Background
  • Key Insight: Algebraic Generalization
• Mathematical Foundation
  • ω-Continuous Semirings
  • Comparison with Kleene’s Method
• Examples and Applications
  • May-Alias Analysis
  • Average Runtime Analysis
  • LCFL Sub-Problems and Tensor-Product Regularization
  • Other Applications
• Distributive vs. Non-Distributive Analyses
• Implementation Layout
• Usage Notes
• Practical notes for numeric domains
• Boolean Program Analysis
• References