Major Components Overview

This page provides a high-level component inventory across Lotus. Each section links to the dedicated documentation page for deeper usage guides and configuration details.

Alias Analysis

See Alias Analysis Components for detailed instructions and command examples.

  • AllocAA – Lightweight alias analysis built from simple heuristics for allocation tracking.

  • DyckAA – Unification-based exhaustive alias analysis (lib/Alias/UnificationBased/DyckAA).

  • CFL (via LLVM) – Context-Free Language alias analysis from LLVM (used by the alias wrapper).

  • Sea-DSA – Context-sensitive and field-sensitive analysis with Sea-DSA (lib/Alias/UnificationBased/seadsa). Does not require Boost.

  • SparrowAA – Inclusion-based pointer analysis without on-the-fly call-graph construction (lib/Alias/InclusionBased/SparrowAA).

  • FPA – Function Pointer Analysis toolbox (FLTA, MLTA, MLTADF, KELP) under lib/Analysis/CallGraph/FPA for resolving indirect calls.

  • DynAA – Dynamic checker living in tools/alias/dynaa that validates static alias analyses against runtime traces.

  • AserPTA – Constraint-based pointer analysis with multiple context sensitivities, including k-callsite and k-origin (thread-creation) sensitivity (lib/Alias/InclusionBased/AserPTA).

  • BootstrapAA – Flow- and context-sensitive inclusion analysis using Steensgaard partitioning, thresholded Andersen refinement, dependency slicing, and input-state-tabulated summaries (lib/Alias/InclusionBased/BootstrapAA). See BootstrapAA.

  • LotusAA – Native alias analysis engine with interprocedural, flow-sensitive, and field-sensitive reasoning (lib/Alias/InclusionBased/LotusAA). See LotusAA — Lotus AA Engine.

  • FlowSensitivePTA – Flow-sensitive inclusion-based pointer analyses with conventional sparse, object-versioned, and direct value-flow solvers (lib/Alias/InclusionBased/FlowSensitive). Includes ValueFlowPTA. See Flow-Sensitive Pointer Analysis and Value-Flow-Based Pointer Analysis.

  • DDA – Demand-driven alias-analysis infrastructure that refines alias information on demand instead of materializing a full global solution (lib/Alias/DemandDriven/DDA). See DDA.

  • SRAA – Strict Relations Alias Analysis that proves pointers cannot alias by establishing strict relations between symbolic expressions (lib/Alias/Specialized/SRAA). See Strict Relations Alias Analysis — Algorithm.

  • TPA – Inclusion-based, flow- and context-sensitive pointer analysis with k-limiting support and a semi-sparse program representation (lib/Alias/InclusionBased/TPA). See TPA: Flow- and Context-Sensitive Pointer Analysis.

  • Spec – Alias specification manager that loads and serves per-function specifications for library routines (lib/Alias/Infrastructure/Spec). See Alias Specification Manager.

  • Metrics – Pointer analysis metrics for measuring precision and soundness-related properties (lib/Alias/Infrastructure/Metrics). See Pointer Analysis Metrics.

Bug Detection and Checkers

See Bug Detection with Lotus and Checker Framework for engine details and selection guides.

  • KINT – Numerical bug detection (integer overflow, division by zero, bad shift, array bounds).

  • AE – Abstract execution for memory safety (buffer overflow, null dereference, use-after-free).

  • Pulse – Witness-oriented biabductive memory-safety analysis.

  • Saber – Source-sink resource checking over sparse value-flow graphs (leaks, double frees).

  • FiTx – Fast typestate-based feedback for routine development.

  • Concurrency – Thread safety, data races, deadlocks, OpenMP, and MPI protocol verification.

  • Taint – Interprocedural IFDS-based information flow and injection checking.

  • GSAF – Path-sensitive checks over guarded value-flow graphs.

  • SymEx – Symbolic-execution bug checks backed by the SymbolicExecution engine.

  • TypeQualifier – Qualifier-based analysis infrastructure modeling qualifier-style properties over program values (lib/Checker/TypeQualifier). See TypeQualifier.

Intermediate Representations

See Intermediate Representations for builder APIs and code snippets.

  • Program Dependence Graph (PDG) – Captures fine-grained data/control dependencies.

  • Static Single Information (SSI) – Extension of SSA with sigma (σ) functions at control splits to encode predicate information (lib/IR/SSI). See SSI — Static Single Information.

  • DyckVFG – Value Flow Graph variant designed for Dyck-based alias analyses (lib/Alias/UnificationBased/DyckAA/DyckVFG.cpp).

  • SVFG – Sparse Value-Flow Graph combining SSA with MemorySSA for efficient interprocedural value-flow analysis (lib/IR/SVFG). See SVFG — Sparse Value-Flow Graph.

  • GVFG – Guarded Value-Flow Graph, a per-function IR for value flow, memory flow, and path-sensitive dependencies (lib/IR/GVFG). See GVFG.

  • ICFG – Interprocedural Control Flow Graph extending the CFG with call and return edges (lib/IR/ICFG). See ICFG — Interprocedural Control Flow Graph.

  • ShadowMemSSA – Query layer for SSA-like shadow memory instructions inserted by the Sea-DSA ShadowMem pass (lib/IR/ShadowMemSSA). See ShadowMem SSA — Sea-DSA Shadow Memory Queries.

  • GSA – Gated SSA, a read-only view of the control flow guarding SSA values at join points (lib/IR/GSA). See GSA — Gated SSA.

  • vSSA – Variable Static Single Assignment, an SSI variant designed for precise symbolic range analysis (lib/IR/vSSA). See vSSA — Variable Static Single Assignment.

  • UFG – Universal Flow Graph, an object-expanded use-flow graph baseline for resource defect detection (lib/IR/UFG). See UFG — Universal Flow Graph.

Machine Learning Features

See Machine Learning Features (CanaryML) for ML feature extraction APIs.

  • CanaryML – Memory-related feature extraction using Sea-DSA for ML applications (lib/Analysis/FeatureExtraction/). Provides MemoryMLFeaturesPass for extracting memory access patterns and structural features from call sites, useful for training memory safety predictors.

Abstract Interpretation

See CLAM – Abstract Interpretation Framework for CLAM and SymAbsAI – Symbolic Abstraction + Abstract Interpretation for higher-level abstractions.

  • CLAM – Modular AI-driven static analyzer with multiple abstract domains (tools/verifier/clam and third-party/verification/clam).

  • SymAbsAI – Configurable abstract interpretation framework with domain composition (lib/Verification/SymAbsAI and include/Verification/SymAbsAI).

Symbolic Automata

See Seal — Symbolic Automata for Stateful Systems for details.

  • Seal (vendored, opt-in) — Symbolic automata lifter for stateful software systems. Builds finite-state-machine models from LLVM IR by combining loop summary analysis, symbolic execution, and abstract interpretation. Published at CAV 2026.

Symbolic Execution

The SymbolicExecution subsystem is a top-level engine under lib/SymbolicExecution and include/SymbolicExecution. It performs path-sensitive symbolic execution over the guarded value-flow graph, tracks symbolic scalar and memory facts, and uses SMT-backed path-condition checks for feasibility. The lotus-check --engine=symex frontend invokes this engine for symbolic-execution bug checks. See Symbolic Execution for the engine documentation.

Utilities and Reachability

See Utilities and Context-Free Language Analysis for extended guides.

  • cJSON – Lightweight JSON parser (include/Utils/Formats/cJSON.h).

  • Transform – LLVM bitcode transformation passes housed in lib/Transform.

  • CFL Reachability – General-purpose CFL reachability utilities and tooling (tools/cfl)