SymAbsAI – Symbolic Abstraction + Abstract Interpretation

SymAbsAI is a framework for static program analysis using symbolic abstraction to provide a flexible interface for designing program analyses in a compositional way.

Binary: symabs_ai (also spranalyze) Location: tools/verifier/symabs-ai/

For the underlying framework and API documentation, see SymAbsAI – Symbolic Abstraction + Abstract Interpretation.

Overview

SymAbsAI provides a command-line tool for running abstract interpretation analyses on LLVM bitcode. It supports multiple abstract domains and fragment decomposition strategies for scalable analysis.

Key features:

  • Multiple abstract domains: intervals, numerical relations, constants, memory regions

  • Configurable fragment strategies for balancing precision and performance

  • Configuration file support for reproducible analyses

  • Integration with Z3 for symbolic reasoning

Quick Start

Basic usage:

# Analyze all functions
./build/bin/symabs_ai example.bc

# Analyze specific function
./build/bin/symabs_ai --function=foo example.bc

# Use a configuration file
./build/bin/symabs_ai --config config/symabs-ai/01_const_function.conf example.bc

List available options:

# List available abstract domains
./build/bin/symabs_ai --list-domains

# List available configuration files
./build/bin/symabs_ai --list-configs

# List functions in a module
./build/bin/symabs_ai --list-functions example.bc

Configuration Files

SymAbsAI uses configuration files (.conf) to specify analysis parameters. Configuration files are located in config/symabs-ai/.

Example configuration:

# Fragment decomposition strategy
FragmentDecomposition.Strategy = Edges

# Abstract domains (comma-separated for product domains)
AbstractDomain = SimpleConstProp, Interval

# Memory model variant
MemoryModel.Variant = BlockModel

# Analyzer settings
Analyzer.WideningDelay = 20

# Verbose output
SymAbsAIPass.Verbose = false

Common configurations:

  • 01_const_function.conf – Fast constant propagation (whole function)

  • 03_const_edge.conf – Balanced constant propagation (loop-friendly)

  • 05_const_rel_edge.conf – Constants + numerical relations

  • memsafety_sv16_body.conf – Memory safety analysis (SV-COMP style)

Command-Line Options

Domain selection:

  • --abstract-domain <NAME> – Override domain from config file

  • --list-domains – Show available abstract domains

Function selection:

  • --function <NAME> – Analyze specific function only

  • --list-functions – List all functions in the module

Configuration:

  • --config <FILE> – Use configuration file

  • --list-configs – List available configuration files

  • SYMBOLIC_ABSTRACTION_CONFIG=<FILE> – Environment variable for default config

Output:

  • --verbose – Enable detailed output

  • --dump-cfg – Dump control flow graph

Abstract Domains

Available abstract domains include:

  • SimpleConstProp – Constant propagation

  • Interval – Value range analysis

  • NumRels – Numerical relations (e.g., x <= y + 5)

  • Affine – Affine relationships

  • BitMask – Bit-level tracking

  • MemRange – Memory access bounds

  • MemRegions – Memory region analysis

Multiple domains can be combined using product domains (comma-separated in config).

Fragment Strategies

Fragment decomposition strategies control where abstraction points are placed:

  • Function – Analyze whole function as one fragment (fastest, least precise)

  • Edges – Abstract after every basic block (most precise, slowest)

  • Headers – Abstract at loop headers (good balance)

  • Body – Abstract in loop bodies

  • Backedges – Abstract at loop backedges

For more details on the framework architecture and API, see SymAbsAI – Symbolic Abstraction + Abstract Interpretation.