Analysis Framework

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

Lotus provides several reusable analysis utilities and frameworks under lib/Analysis. 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/Analysis/Concurrency): Thread-aware analyses for multi-threaded code (MHP, lock sets, thread modeling). See Concurrency Analysis.

  • Crypto (lib/Analysis/Crypto): Constant-time programming analysis for cryptographic code. See Constant-Time Cryptographic 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.

  • Spectre (lib/Analysis/Spectre): Cache speculation analysis for detecting Spectre vulnerabilities. See Spectre Cache Analysis.

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

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.