Analysis Framework

This section covers the core analysis components and frameworks in Lotus.

Lotus provides several reusable analysis utilities and frameworks under lib/Analysis and adjacent subsystem modules such as lib/Concurrency. These components complement the alias analyses and high-level analyzers such as CLAM (numerical abstract interpretation) and SymAbsAI (symbolic abstraction + abstract interpretation) built in lib/Verification.

Overview

At a glance:

• CFG (lib/Analysis/CFG): Control Flow Graph utilities for reachability, dominance, and structural reasoning. See CFG Analysis.

• Concurrency (lib/Concurrency): Thread-aware analyses for multi-threaded code (MHP, lock sets, thread modeling). Now documented in its own section: see Concurrency Analysis.

• DebugInfo (lib/Analysis/DebugInfo): Source-location and metadata extraction support. See Debug Info.

• Loop (lib/Analysis/Loop): Loop-dependence, iteration-space, and transformation-oriented loop analyses. See Loop Analysis Framework.

• NullPointer (lib/Analysis/NullPointer): A family of nullness and null-flow analyses. See Null Pointer Analysis.

• TypeHierarchy (lib/Analysis/TypeHierarchy): Type-hierarchy and vtable recovery for object-oriented code. See Type Hierarchy.

• SCCP (lib/Analysis/SCCP): Sparse conditional constant propagation using a three-valued lattice (Top/Constant/Bottom) to discover constants and dead code. See SCCP — Sparse Conditional Constant Propagation.

• ParameterSummary (lib/Analysis/ParameterSummary): Per-function parameter effect summaries tracking freed, dereferenced, and allocated parameters, with transitive call-graph composition. See ParameterSummary — Parameter Effect Summary Analysis.

• Multiplicity (lib/Analysis/Multiplicity): Allocation multiplicity classification — classifies global, stack, and heap allocations as Unique or Summary. See Multiplicity — Allocation Multiplicity Classification.

Higher-level analyzers such as CLAM and SymAbsAI build on these components; see CLAM – Abstract Interpretation Framework and SymAbsAI – Symbolic Abstraction + Abstract Interpretation for details.

• CFG Analysis
• Debug Info
  • Overview
  • Main components
  • Typical use cases
  • See also
• Loop Analysis Framework
• Null Pointer Analysis
• Type Hierarchy
  • Overview
  • Main components
  • Typical use cases
• SCCP — Sparse Conditional Constant Propagation
  • Overview
  • Supported Instructions
  • Read-Only Globals
  • Results
  • Example
• ParameterSummary — Parameter Effect Summary Analysis
  • Overview
  • Resource Table
  • Transitive Composition
  • Usage
• Multiplicity — Allocation Multiplicity Classification
  • Overview
  • Heap Allocation Detection
  • Usage