Lotus: Program Analysis Framework
Lotus is a comprehensive program analysis, verification, and optimization framework built on LLVM. It provides multiple toolkits that can be used individually or in combination for various static analysis tasks.
User Guide
- Major Components Overview
- Architecture Overview
- Quick Start Guide
- Installation Guide
- Tutorials and Examples
- Tutorial 1: Basic Alias Analysis
- Tutorial 2: Detecting Integer Overflow
- Tutorial 3: Null Pointer Detection
- Tutorial 4: Taint Analysis
- Tutorial 5: Abstract Interpretation with CLAM
- Tutorial 6: Program Dependence Graph Queries
- Tutorial 7: Dynamic Validation with DynAA
- Tutorial 8: Interprocedural Analysis
- Tutorial 9: Concurrency Analysis
- Best Practices
- Next Steps
- Bug Detection with Lotus
- PDG Query Language (Cypher)
- Property-Based Slicing
- Verification Backend Abstraction
- Instrumentation Passes
- Troubleshooting and FAQ
- Command-Line Tools
Core Components
- Alias Analysis
- Alias Analysis Components
- AllocAA — Allocation-Based AA
- Sparrow Pointer Analysis — Inclusion AA
- AserPTA — Pointer Analysis
- CclyzerAA
- DDA
- DFPA
- DyckAA — Dyck-CFL Analysis
- Sea-DSA — Memory Graph AA
- FPA — Function Pointer Analyses (FLTA/MLTA/MLTADF/KELP)
- LotusAA — Lotus AA Engine
- UnderApproxAA — Must-Alias Analysis
- DynAA — Dynamic Alias AA
- Strict Relations Alias Analysis — Algorithm
- 1. vSSA / SSI Transformation
- 2. Symbolic Range Analysis
- 3. Strict-Inequality Construction
- 4. Constraint Propagation Solver
- 5. Alias Disambiguation (Final Decision)
- 6. PDG Memory-Node Reduction (Applicability)
- Summary of Properties
- End of document.
- Pointer Analysis Metrics
- Points-To Set Backends
- Alias Specification Manager
- TPA: Flow- and Contex-Sensitive Pointer Analysis
- TypeQualifier
- Analysis Framework
- Annotations
- Applications
- Context-Free Language Analysis
- Data Flow Analysis
- Algebraic Program Analysis (APA)
- Control Flow Support
- Monotone Dataflow Engine
- Overview
- Core Idea
- Example Analyses
- IFDS / IDE Engine
- Overview
- IFDS: Set-Valued Problems
- IDE: Value-Enriched Problems
- Usage
- Command-Line Tool: lotus-taint
- WPDS Dataflow Engine
- Overview
- Core Idea
- Example Analyses
- Newtonian Program Analysis (NPA)
- Overview
- Conceptual Background
- Mathematical Foundation
- Examples and Applications
- Distributive vs. Non-Distributive Analyses
- Core Implementation (include/Dataflow/NPA/Core)
- Usage Notes
- Practical notes for numeric domains
- References
- Intermediate Representations
- ICFG — Interprocedural Control Flow Graph
- Overview
- Key Features
- Components
- Usage
- Integration
- PDG — Program Dependence Graph
- Overview
- Core Passes
- Unified Query API
- High-Level Usage
- pdg-query Analysis Mode
- SSI — Static Single Information
- Overview
- Key Features
- SSI Formalism
- Components
- SSI Instructions
- Algorithm
- Usage
- Integration
- vSSA — Variable Static Single Assignment
- Overview
- Key Features
- vSSA Instructions
- Algorithm
- Components
- Usage
- Integration with SRAA
- Example
- References
- SVFG — Sparse Value-Flow Graph
- Overview
- Key Features
- Node Types
- Edge Types
- Architecture
- Usage
- Integration
- Components
- References
- GVFG
- GSA — Gated SSA
- Overview
- Key Features
- Core Types
- Passes
- Usage
- Command-Line Options
- Behavior Notes
- MemorySSA — Memory Static Single Assignment
- Overview
- Key Features
- Shadow Memory Instructions
- Components
- Usage
- Integration
- Overview
- MemoryMLFeaturesPass
- Features Extracted
- Feature Output
- Analysis Dependencies
- Integration Notes
- Related Components
- Optimization
- Solvers
- Transforms
- Utilities
- Verification
- Checker Framework
Developer Documentation
Features
Multiple Alias Analysis Algorithms: DyckAA, Sea-DSA, SparrowAA, AserPTA, FPA, OriginAA (CFL via LLVM)
Dynamic Analysis Validation: DynAA for validating static analysis results
Intermediate Representations: PDG, SVFG, DyckVFG
Constraint Solving: SMT (Z3), BDD (CUDD), WPDS
Data Flow Analysis: IFDS/IDE framework, taint analysis
Bug Detection: Integer overflow, null pointer, buffer overflow detection
LLVM Integration: Built on LLVM 14 with comprehensive IR support
Supported Platforms
x86 Linux
ARM Mac
LLVM 14.0.0
Z3 4.11
Publications
ISSTA 2025: Program Analysis Combining Generalized Bit-Level and Word-Level Abstractions Guangsheng Fan, Liqian Chen, Banghu Yin, Wenyu Zhang, Peisen Yao, and Ji Wang. The ACM SIGSOFT International Symposium on Software Testing and Analysis.
S&P 2024: Titan: Efficient Multi-target Directed Greybox Fuzzing Heqing Huang, Peisen Yao, Hung-Chun Chiu, Yiyuan Guo, and Charles Zhang.
USENIX Security 2024: Unleashing the Power of Type-Based Call Graph Construction by Using Regional Pointer Information Yuandao Cai, Yibo Jin, and Charles Zhang.
TSE 2024: Fast and Precise Static Null Exception Analysis with Synergistic Preprocessing Yi Sun, Chengpeng Wang, Gang Fan, Qingkai Shi, and Xiangyu Zhang.
OOPSLA 2022: Indexing the Extended Dyck-CFL Reachability for Context-Sensitive Program Analysis Qingkai Shi, Yongchao Wang, Peisen Yao, and Charles Zhang.