SMT Formula Abstraction (SymAbs)

This section documents the SMT Formula Abstraction library (SymAbs), which implements algorithms for computing symbolic abstractions of SMT bit-vector formulas.

Overview

Location: lib/Solvers/SMT/SymAbs/

Important: This library is distinct from lib/Verification/SymAbsAI. SymAbs operates on SMT formulas, while the verification module operates on LLVM IR programs.

Key Differences

Aspect

lib/Solvers/SMT/SymAbs

lib/Verification/SymAbsAI

Input

SMT bit-vector formulas (Z3 expressions)

LLVM IR (program code)

Output

Abstract constraints (intervals, octagons, etc.)

Abstract domain values for LLVM values

Approximation

Converts bit-vectors to linear integer formulas

Works directly with program semantics

Level

Formula-level abstraction algorithms

Program-level abstract interpretation

Integration

Standalone SMT formula processing

Integrated LLVM pass with fixpoint engine

Use Case

Abstracting SMT formulas for constraint solving

Static analysis and optimization of programs

Why Linear Integer Approximation?

SymAbs uses linear integer formulas to approximate bit-vector formulas because:

  • Bit-vector arithmetic is complex (wrap-around, modular arithmetic)

  • Linear integer arithmetic is more tractable for SMT solvers

  • Allows reuse of efficient integer constraint algorithms

  • Trade-off: May lose precision due to the approximation

The conversion uses bv_signed_to_int() which interprets bit-vectors in two’s complement to avoid wrap-around during arithmetic.

Abstract Domains

SymAbs implements several abstract domains for symbolic abstraction:

Zone Domain (Difference Bound Matrices)

  • Files: Zone.cpp, Zone.h

  • Constraints: x - y ≤ c and x ≤ c

  • Description: The zone domain tracks difference constraints between variables. More restrictive than octagons but computationally more efficient.

  • Use cases: Timing analysis, scheduling, real-time systems verification

Octagon Domain

  • Files: Octagon.cpp, Octagon.h

  • Constraints: ±x ± y ≤ c

  • Description: Relational numerical domain expressing constraints with linear combinations of at most two variables with coefficients in {-1, 0, 1}.

  • Use cases: General numerical analysis, overflow detection

Other Domains

  • Intervals: Unary constraints representing value ranges

  • Polyhedra: General convex constraints

  • Affine Equalities: Linear equality relations

  • Congruences: Modular arithmetic constraints

  • Polynomials: Non-linear polynomial constraints

Key Algorithms

  • Algorithm 7: α_lin-exp - Linear expression maximization

  • Algorithm 8: α_oct^V - Octagonal abstraction

  • α_zone^V: Zone abstraction (Difference Bound Matrices)

  • Algorithm 9: α_conv^V - Convex polyhedral abstraction

  • Algorithm 10: relax-conv - Relaxing convex polyhedra

  • Algorithm 11: α_a-cong - Arithmetical congruence abstraction

  • Algorithm 12: α_aff^V - Affine equality abstraction

  • Algorithm 13: α_poly^V - Polynomial abstraction

C++ API Usage

#include "Solvers/SMT/SymAbs/SymbolicAbstraction.h"
#include <z3++.h>

z3::context ctx;
z3::expr x = ctx.bv_const("x", 8);
z3::expr y = ctx.bv_const("y", 8);

// Build a formula
z3::expr phi = (x >= 0) && (x <= 10) && (y >= 0) && (y <= 20);

// Compute octagonal abstraction constraints
auto oct_constraints = SymAbs::alpha_oct_V(phi, {x, y});

// Compute bounds via linear expression maximization/minimization
auto max_x = SymAbs::maximum(phi, x);
auto min_x = SymAbs::minimum(phi, x);

When to Use SymAbs

Use lib/Solvers/SMT/SymAbs when:

  • You have SMT formulas (bit-vectors) that need abstraction

  • You need to approximate bit-vector constraints with linear integer constraints

  • You’re working at the formula/solver level, not the program level

Use lib/Verification/SymAbsAI when:

  • You’re analyzing LLVM IR programs

  • You need a complete abstract interpretation framework

  • You want to integrate analysis into LLVM optimization passes