CRAB - Abstract Interpretation Library

CRAB is the abstract interpretation library vendored in Lotus under third-party/crab/. It provides the core abstract domains, fixpoint engines, and CrabIR infrastructure that CLAM builds on.

Location: third-party/crab/

Overview

CRAB is a reusable C++ library for building static analyses over a CFG-based intermediate representation called CrabIR. In Lotus, it is primarily consumed through CLAM, but the library itself is worth documenting because it contains the underlying domain implementations, analyzers, and solver machinery.

Key Features:

  • Numerical abstract domains such as intervals, congruences, zones, octagons, polyhedra, disjunctive intervals, and reduced products

  • Forward, backward, and interprocedural analyses

  • WTO-based fixpoint iteration with widening heuristics and thresholds

  • CrabIR, a strongly typed three-address IR with assumptions and assertions

  • Optional integration with Apron, Elina, LDD/Boxes, and PPLite

Repository Structure

Headers (third-party/crab/include/crab/):

  • cfg/ - CrabIR CFG definitions and utilities

  • domains/ - Abstract domains and supporting data structures

  • analysis/ - Forward, backward, dataflow, and interprocedural analyzers

  • fixpoint/ - Fixpoint iterators, WTO support, and thresholds

  • transforms/ - IR-level transformations

  • support/ - Statistics, debugging, and OS helpers

Sources (third-party/crab/lib/):

  • Core numeric and domain implementations such as intervals, congruences, wrapped intervals, symbolic terms, and region information

Build Configuration

CRAB is built with CMake and can be compiled standalone or as an embedded dependency.

Common options:

  • CRAB_ENABLE_TESTS - Build CRAB’s standalone test programs

  • CRAB_BUILD_LIBS_SHARED - Build shared libraries instead of static ones

  • CRAB_USE_APRON - Enable Apron-backed domains

  • CRAB_USE_ELINA - Enable Elina-backed domains

  • CRAB_USE_LDD - Enable Boxes/LDD domains

  • CRAB_USE_PPLITE - Enable PPLite-backed domains

Standalone build:

mkdir build && cd build
cmake .. -DCRAB_ENABLE_TESTS=ON
cmake --build .

Integration With Lotus

  • CLAM uses CRAB for abstract domains, fixpoint solving, and its internal IR

  • Lotus documents CLAM as the primary user-facing verifier, while CRAB is the lower-level analysis library underneath it

  • CRAB’s domain choices surface in CLAM flags such as --crab-dom

If you are interested in running analyses directly from Lotus, start with CLAM – Abstract Interpretation Framework. If you need to understand where the domains and abstract interpretation machinery come from, CRAB is the relevant component.

See Also