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: lib/Verification/clam/

Headers: include/Apps/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 (lib/Verification/clam/):

  • 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 (lib/Verification/clam/crab/domains/):

  • Intervals, zones, octagons, polyhedra

  • Disjunctive domains and term domains

  • Domain-specific optimizations

Property Checkers (lib/Verification/clam/Properties/):

  • NullCheck.cc – Null pointer dereference detection

  • BndCheck.cc – Buffer bounds checking

  • UafCheck.cc – Use-after-free detection

  • MemoryCheckUtils.cc – Memory safety utilities

Transforms (lib/Verification/clam/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 (lib/Verification/clam/)

  • 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=assert program.bc
./build/bin/clam --crab-check=null program.bc
./build/bin/clam --crab-check=bounds program.bc

Interprocedural Analysis:

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

Preprocessing:

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

Programmatic Usage

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

// Create CFG builder
CrabBuilderManager builder(module);

// Create CLAM analysis
GlobalClam ga(module, builder);

// Run analysis
AnalysisParams params;
params.run_inter = true;
ga.analyze(params);

// 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: Heap abstraction for memory modeling

  • Lotus Alias Analysis: Pointer analysis integration

  • CRAB Library: Abstract domain implementations

  • LLVM Pass Infrastructure: Standard pass registration

See Also