Lotus: Program Analysis Framework
Lotus is a comprehensive toolkit for performing static program analysis, bug detection, verification, and optimization on C/C++ code through the LLVM intermediate representation. The framework provides multiple analysis engines and bug detection tools that can be used individually or in combination to analyze programs for correctness, security vulnerabilities, and optimization opportunities.
The framework is designed with modularity and extensibility in mind, allowing researchers and practitioners to:
Perform various forms of dataflow analysis (distributive, monotone, pushdown, elimination-based)
Detect concurrency bugs (data races, deadlocks, atomicity violations)
Identify memory safety issues (buffer overflows, null pointer dereferences, use-after-free)
Track information flow through taint analysis
Verify program properties using abstract interpretation
User Guide
- Architecture & Major Components
- Getting Started
- Major Components Overview
- 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 Driver Abstraction
- Instrumentation Passes
- Troubleshooting and FAQ
- Command-Line Tools Reference
Core Components
- Alias Analysis
- Alias Analysis Components
- AllocAA — Allocation-Based AA
- Sparrow Pointer Analysis — Inclusion AA
- AserPTA — Pointer Analysis
- BootstrapAA
- CclyzerAA
- DDA
- DyckAA — Dyck-CFL Analysis
- Sea-DSA — Memory Graph AA
- Flow-Sensitive Pointer Analysis
- Value-Flow-Based Pointer Analysis
- Overview
- Public API
- Entry points
- Algorithm
- Memory model and limitations
- Command line
- 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
- Pointer Analysis Metrics
- Points-To Set Backends
- Alias Specification Manager
- TPA: Flow- and Context-Sensitive Pointer Analysis
- Analysis Framework
- Annotations
- Applications
- Context-Free Language Analysis
- Concurrency Analysis
- Data Flow Analysis Frameworks
- 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
- lotus-ir-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
- UseTraceSSA — Ordered Use-History Overlay
- Overview
- Representation and Core Abstractions
- Query Engine
- Bug Detection
- Tools and Integration
- Performance and Deferred Reports
- GVFG
- GSA — Gated SSA
- Overview
- Key Features
- Core Types
- Passes
- Usage
- Command-Line Options
- Behavior Notes
- ShadowMem SSA — Sea-DSA Shadow Memory Queries
- Overview
- Key Features
- Shadow Memory Instructions
- Components
- Usage
- Integration
- Path Program
- UFG — Universal Flow Graph
- Overview
- Architecture and Construction
- Search Engine and Defect Detection
- Context Sensitivity and Budgets
- Machine Learning Features (CanaryML)
- Optimization
- Security Components
- Solvers
- CUDD (Binary Decision Diagrams)
- SMT (Satisfiability Modulo Theories)
- WPDS (Weighted Pushdown Systems)
- SMT Samplers
- SMTStabilizer: SMT-LIB2 Normalization Library
- SMT Formula Abstraction (SymAbs)
- SMT Theory Arbitrage (STAUB)
- TUNA
- Stingx — String Constraint Solver
- Lotus EGraph: Equality Saturation Engine
- E-Graph Quantifier Simplification (EGraphsSimp)
- FPsolve — Fixed-Point Equation Solver
- LIBSMT — SMT Solver Abstraction Layer
- Native C++ Datalog
- Third-Party Libraries
- Symbolic Execution
- Transforms
- Utilities
- Verification
- Verification Support Analyses
- Nested Word Automata
- Trace Abstraction
- Verification Backend API
- CRAB - Abstract Interpretation Library
- CLAM – Abstract Interpretation Framework
- Mosaic
- SMACK Verification Frontend
- Sifa
- Seal — Symbolic Automata for Stateful Systems
- SymAbsAI – Symbolic Abstraction + Abstract Interpretation
- SeaHorn Verification Framework
- Failure-Directed Trimming
- Verification Frontend
- Verification Transformation Passes
- Checker Framework
Developer Documentation
Features
Multiple Pointer Analysis Algorithms: DyckAA, Sea-DSA, SparrowAA, AserPTA, TPA, FPA, CFL (via LLVM)
Dynamic Analysis Validation: DynAA for validating static analysis results
Intermediate Representations: PDG, SVFG and its sparse MemorySSA, GVFG, ICFG, ShadowMemSSA, and Gated SSA (GSA)
Constraint Solving: SMT (Z3), BDD (CUDD), WPDS, string constraints (Stingx)
Data Flow Analysis Frameworks: IFDS/IDE framework, Monotone framework, WPDS, and APA (Elimination-based)
Bug Detection Checkers: Integer overflow (Kint), memory safety (AE, Pulse, Saber), concurrency bugs, taint tracking
Symbolic Execution: Path-sensitive engine for bug checking
Symbolic Automata: Seal — FSM model lifting for stateful systems (CAV 2026)
LLVM Integration: Built on LLVM 14 with IR and graph abstractions
Supported Platforms
x86/ARM Linux
ARM macOS
LLVM 14.x
Z3 4.8.1+ (4.11 tested)
CMake 3.18+
C++17
Publications
Papers utilizing the Lotus framework (kept in sync with the repository
README.md):
PPoPP 2027: Cactus: GPU-Accelerated Alias Query Processing over Persistent Points-to Information. Zinan Gu, Zhaoyang Tan, Peisen Yao, and Kui Ren.
SPLASH/ISSTA 2026 Demo: Phoenix: A Modular and Versatile Framework for C/C++ Pointer Analysis. Peisen Yao, Zinan Gu, and Qingkai Shi.
ASE 2026: SIMD-Accelerated Sparse Bit-Vectors for Pointer Analysis. Zhaoyang Tan, Peisen Yao, and Kui Ren.
FM 2026: EUF-based Solving Dyck-Reachability with Applications to Static Analysis. Yide Du, Zhenbang Chen, Kunlin Liu, Guofeng Zhang, Xudong Wang, Ke Ma, Wei Dong, and Ji Wang.
CAV 2026: Sound and Precise Symbolic Automata Model for Stateful Software Systems. Xinlong Wu, Ruiyu Zhou, Peisen Yao, and Qingkai Shi. International Conference on Computer Aided Verification.
TOSEM 2026: Compiler Optimizations-Based SMT Simplifications: An In-Depth Study. Hanyun Jiang, Peisen Yao, Jiachen Lu, Yongwang Zhao, and Kui Ren.
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.