CLAM – Abstract Interpretation Framework

CLAM is a static analysis framework based on abstract interpretation over numerical abstract domains. It provides invariant generation and property checking for LLVM bitcode.

Location: third-party/verification/clam/src/

Headers: third-party/verification/clam/include/Verification/clam/

Tools: tools/verifier/clam/ (command-line frontends)

Overview

CLAM computes sound over-approximations of program behaviors by interpreting programs over different numerical abstract domains. It integrates with Lotus’s alias analysis and memory modeling infrastructure.

Key Features:

  • Multiple abstract domains: intervals, zones, octagons, polyhedra

  • Memory safety checking: null pointer, buffer bounds, use-after-free

  • Assertion checking and invariant generation

  • Integration with Sea-DSA for precise heap abstraction

  • Interprocedural and intraprocedural analysis modes

Components

Core Library (third-party/verification/clam/src/):

  • Clam.cc – Main analysis engine and pass registration

  • CfgBuilder.cc – LLVM IR to CRAB IR translation

  • CfgBuilderMemRegions.cc – Memory region abstraction

  • SeaDsaHeapAbstraction.cc – Sea-DSA integration

  • ClamQueryCache.cc – Query result caching

Abstract Domains (third-party/verification/clam/src/crab/domains/):

  • Intervals, zones, octagons, polyhedra

  • Disjunctive domains and term domains

  • Domain-specific optimizations

Property Checkers (third-party/verification/clam/src/Properties/):

  • NullCheck.cc – Null pointer dereference detection

  • BndCheck.cc – Buffer bounds checking

  • UafCheck.cc – Use-after-free detection

  • MemoryCheckUtils.cc – Memory safety utilities

Transforms (third-party/verification/clam/src/Transforms/):

  • DevirtFunctions.cc – Function devirtualization

  • LowerSelect.cc – Select instruction lowering

  • LowerUnsignedICmp.cc – Unsigned comparison lowering

  • PromoteMalloc.cc – Malloc promotion

  • NondetInit.cc – Non-deterministic initialization

Command-Line Tools (tools/verifier/clam/):

  • clam – Main analyzer

  • clam-pp – Preprocessing tool

  • clam-diff – Differential analysis

Build Targets

  • ClamAnalysis – Core library (third-party/verification/clam/src/)

  • clam – Command-line analyzer

  • clam-pp – Preprocessor

  • clam-diff – Differential analyzer

Usage

Basic Analysis:

./build/bin/clam program.bc

With Domain Selection:

./build/bin/clam --crab-dom=zones program.bc
./build/bin/clam --crab-dom=pk program.bc  # Polyhedra

Property Checking:

./build/bin/clam --crab-check program.bc
./build/bin/clam --crab-check --crab-null-check program.bc
./build/bin/clam --crab-check --crab-bounds-check program.bc

Interprocedural Analysis:

./build/bin/clam --crab-inter program.bc

Preprocessing:

./build/bin/clam-pp --clam-lower-unsigned-icmp \
                    --clam-lower-select \
                    input.bc -o prep.bc
./build/bin/clam prep.bc

Programmatic Usage

#include "Verification/clam/Clam.hh"
#include "Verification/clam/CfgBuilder.hh"

// Create a crab CFG builder manager
CrabBuilderParams cparams;
auto tli = &getAnalysis<TargetLibraryInfoWrapperPass>().getTLI();
std::unique_ptr<HeapAbstraction> mem(new DummyHeapAbstraction());
CrabBuilderManager builder(cparams, tli, std::move(mem));

// Create CLAM analysis (use IntraGlobalClam for a non-interprocedural run)
InterGlobalClam ga(module, builder);

// Run analysis
AnalysisParams params;
params.run_inter = true;
ClamGlobalAnalysis::abs_dom_map_t assumptions;
ga.analyze(params, assumptions);

// Query invariants
auto pre = ga.getPre(&bb);
auto post = ga.getPost(&bb);

Abstract Domains

  • Intervals (int): Fast, value ranges [l, u]

  • Zones: Difference constraints x - y ≤ c

  • Octagons (oct): Diagonal constraints ±x ± y ≤ c

  • Polyhedra (pk): Most precise, linear inequalities

  • Disjunctive domains: Union of abstract values

See CLAM – Numerical Abstract Interpretation for detailed domain documentation and usage examples.

Integration Points

  • Sea-DSA: Supplies the HeapAbstraction handed to CrabBuilderManager

  • Lotus Alias Analysis: Provides alias facts used when the CFG builder models memory

  • CRAB Library: Implements the abstract domains and fixpoint engines

  • LLVM Pass Infrastructure: clam/clam-pp register as LLVM passes

See Also