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

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"

using namespace z3;
using namespace SymAbs;

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

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

// Compute abstraction
auto zone = OctagonAbstraction::create(phi);

// Query abstract domain
auto max_x = zone.maximum(x);
auto bounds = zone.getBounds(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