- Generated by
1.15.0
|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Directories | |
| bitwuzla | |
| bitwuzllob | |
| boolector | |
| cvc4 | |
| cvc5 | |
| mathsat | |
| minisat | |
| neurosym | |
| prop | |
| sat | |
| smt | |
| smtlib | |
| yices | |
| z3 | |
Files | |
| solve.cpp | |
| solve.h | |
This document is intended for developers extending ESBMC with new SMT backends or new SMT encodings. If you are just trying to use an existing solver, the project README.md and the setup docs on the website are the right starting points.
This directory reduces SSA programs produced by ESBMC's symbolic execution engine into SMT formulae, hands them to a back-end solver, and reads the resulting model back out. Backends are pluggable: each lives in its own subdirectory and implements a small set of abstract interfaces defined in smt/.
The cleanest reference backend is bitwuzla/ (~1 kLoC, modern Bitwuzla C API). The most thorough in-source documentation is the file-level Doxygen comment at the top of smt/smt_conv.h — start there if you want a deep dive.
If you are new to ESBMC, read the top-level ARCHITECTURE.md first — it has the diagram and prose overview of the full verification pipeline. The short version:
source → AST → GOTO program → symex / SSA → SMT formula → solver → model
└────────── src/solvers/ ──────────┘
This directory owns the last two stages. Its inputs are SSA-form expressions in ESBMC's typed internal representation; its outputs are SMT terms in a back-end solver's API and, on SAT, a model that is decoded back into ESBMC values.
Neighbouring layers that this module collaborates with — read these when something in smt_convt is not behaving the way you expect:
User-facing theory and developer docs on the website mirror parts of this pipeline and are worth a skim:
| Path | Contents |
|---|---|
| smt/ | Solver-agnostic core: smt_convt, smt_ast, smt_sort, byte ops, casts, memory model, overflow encoding |
| smt/tuple/ | Tuple flattening for solvers that lack native tuples (node-based and symbol-based variants) |
| smt/fp/ | Floating-point flattening (fp_convt) for solvers without native FP |
| prop/ | Shared with SAT backends: literal.h, pointer_logic.{cpp,h} |
| bitwuzla/, z3/, boolector/, cvc4/, cvc5/, mathsat/, yices/, smtlib/, minisat/, sat/ | Per-backend subclasses |
| solve.{cpp,h} | Factory that picks and instantiates a backend |
| solver_config.h.in | Compile-time configuration (#cmakedefine per solver) |
Three abstract classes carry the design:
smt_convt flattens, for every backend: the C memory address space, pointer representation, casts, byte extract/update, fixed-bv float encoding, unions, and overflow detection. Three optional interfaces let a backend opt in to native handling where the solver supports it:
| Interface | If implemented | Fallback |
|---|---|---|
| array_iface | Solver's native arrays | array_conv (Kroening's decision procedure) |
| tuple_iface | Solver's native tuples / datatypes | smt_tuple_node or smt_tuple_sym |
| fp_convt (subclassed) | Solver's native FP theory | IEEE 754 bit-vector encoding |
If you find yourself flattening anything more than the items above — for instance, anything that touches pointer dereferencing, control-flow guards, or dynamic allocation — that work belongs in symbolic execution, not here.
Symex hands smt_convt an SSA program one expression at a time and later asks for a verdict. The sequence of calls is:
smt_convt::assert_expr(expr2tc)
└─> convert_ast(expr2tc) // defined in smt_conv.cpp
└─> mk_* family // your overrides build native terms
└─> assert_ast(smt_astt) // your override hands term to solver
... repeat for every SSA assertion ...
dec_solve() // your override invokes the solver
└─> returns SAT / UNSAT / UNKNOWN
if SAT:
get_bool / get_bv / get_array_elem // your overrides read the model
push_ctx / pop_ctx bracket incremental queries. This is the only temporal contract a backend must honour: terms produced by mk_* are asserted via assert_ast, the solver is invoked exactly once per verdict via dec_solve, and model values are extracted only after a SAT result.
The canonical small reference is bitwuzla/. There is also a longer narrative on the wiki: Integrate a new SMT solver into the ESBMC backend. That page is written against z3/ as the template and some of its line-number citations have drifted; treat bitwuzla/ as the up-to-date reference and the wiki as background.
From a clean rebuild, smoke-test with a one-line C program:
The first command exercises the full lifecycle (convert_ast → assert_ast → dec_solve → no model needed); the second dumps the formula your backend would receive — invaluable when a real query misbehaves. Once that works, run the regression suite filtered by -L esbmc with your --<name> flag wired in.
If the first command does not return VERIFICATION SUCCESSFUL, the cause is almost always in Stage 1: a missing literal builder (mk_smt_bool / mk_smt_bv / mk_smt_symbol) or equality (mk_eq), or a broken solver hand-off (assert_ast / dec_solve). Start by implementing dump_smt and re-running with --smt-formula-only to see exactly what your backend produced.
Implement the overrides. The base class declares ~50 virtual methods; build them up in this order — each stage produces a backend that can run progressively richer programs.
Stage 1 — Core (minimum to compile and solve a trivial query). These methods are pure-virtual in smt_convt, or their defaults abort(). Without them the class will not instantiate, or will die on the first call.
At this point a trivial program with --<name> should reach VERIFICATION SUCCESSFUL / FAILED cleanly. This is your first milestone — the backend is correctly wired end-to-end and every subsequent stage is additive.
Stage 2 — Common (any non-trivial C program needs these).
After Stage 2, most of the regression/esbmc suite should run.
Stage 3 — Advanced and optional.
Out-of-tree (elsewhere in the repo):
Extending ESBMC with a new encoding — for example, a real-arithmetic fragment, an integer-encoded bit-vector lowering, or a new logic — is a different axis from adding a solver and touches different files. The wiki has a narrative walkthrough: Implement a new SMT theory into ESBMC.
The in-tree exemplar is the --ir-ieee real-arithmetic FP mode (summarised below); its entry point is smt_convt::apply_ieee754_semantics in smt/smt_conv.cpp. Touch-points to expect:
Intuition. Floating-point operations are approximated using real-arithmetic constraints with sound, symmetric error bounds: every FP result is bracketed by [r − ε, r + ε] where r is the exact real value and ε envelops the round-to-nearest rounding error. The encoding is cheaper for solvers without native FP, and never reports a false UNSAT.
When --ir-ieee is set, floating-point operations are encoded in real arithmetic rather than bit-precise FP. smt_convt::apply_ieee754_semantics (in smt/smt_conv.cpp) wraps each real-valued FP result in a sound symmetric error enclosure derived from the round-to-nearest model:
|fl(r) - r| <= eps_rel * |r| + eps_abs
where eps_rel is half the machine epsilon (2⁻⁵³ double, 2⁻²⁴ single) and eps_abs is the minimum positive subnormal (2⁻¹⁰⁷⁴ double, 2⁻¹⁴⁹ single), covering the underflow region. The enclosure asserts r - (eps_rel * |r| + eps_abs) <= result <= r + (eps_rel * |r| + eps_abs) together with a sanity bound lo <= hi. Bidirectional inequalities are used rather than equalities so the bounds survive Z3's solve-eqs tactic.
Epsilon constants come from four helpers in smt_conv.cpp (get_double_eps_rel, get_single_eps_rel, get_double_min_subnormal, get_single_min_subnormal), each rounded upward at the last decimal digit so the parsed value is >= the true power of two — preserving soundness of the enclosure. Non-standard FP formats currently fall back to an unconstrained (weak) enclosure.
A few habits will save hours when bringing up a new backend or encoding:
Dump the formula and read it. Even when your backend is selected, point ESBMC at the text backend to inspect what was produced:
Cross-check the dumped term shape against what your backend's mk_* overrides produce. See the website page SMT Formula Generation for the supported dump options.
In-tree, in this directory:
In-tree, neighbouring layers:
On the wiki:
1.15.0