smt_conv.h File Reference

SMT conversion tools and utilities. More...

#include <memory>
#include <string>
#include <unordered_set>
#include <irep2/irep2.h>
#include <util/base/threeval.h>
#include <solvers/smt/smt_result.h>

Include dependency graph for smt_conv.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	smt_convt
	Slim, frontend-facing SMT interface. More...

Detailed Description

SMT conversion tools and utilities.

smt_solver_baset is the base class for everything that attempts to convert the contents of an SSA program into something else, generally SMT or SAT based.

The class itself does various accounting and structuring of the conversion, however the challenge is that as we convert the SSA program into anything else, we must deal with the fact that expressions in ESBMC are somewhat bespoke, and don't follow any particular formalism or logic. Therefore a lot of translation has to occur to reduce it to the desired logic, a process that Kroening refers to in CBMC as 'Flattenning'.

The conceptual data flow is that an SSA program held by symex_target_equationt is converted into a series of boolean propositions in some kind of solver context, the handle to which are objects of class smt_ast. These are then asserted as appropriate (or conjoined or disjuncted), after which the solver may be asked whether the formula is or not. If it is, the value of symbols in the formula may be retrieved from the solver.

To do that, the user must allocate a solver converter object, which extends the class smt_solver_baset. Currently, create_solver() will do this, in the factory-pattern manner (ish). Each solver converter implements all the abstract methods of smt_solver_baset. When handed an expression to convert, smt_solver_baset deconstructs it into a series of function applications, which it creates by calling various abstract methods implemented by the converter (in particular mk_func_app).

The actual function applications are in smt_ast objects. Following the SMTLIB definition, these are basically a term.

In no particular order, the following expression translation problems exist and are solved at various layers:

For all solvers, the following problems are flattenned:

• The C memory address space
• Representation of pointer types
• Casts
• Byte operations on objects (extract/update)
• FixedBV representation of floats
• Unions -> something else

While these problems are supported by some SMT solvers, but are flattened in others (as SMT doesn't support these):

• Bitvector integer overflow detection
• Tuple representation (and arrays of them)

SAT solvers have the following aspects flattened:

• Arrays (using Kroenings array decision procedure)
• First order logic bitvector calculations to boolean formulas
• Boolean formulas to CNF

If you find yourself having to make the SMT translation translate more than these things, ask yourself whether what you're doing is better handled at a different layer, such as symbolic execution. A nonexhaustive list of these include:

• Anything involving pointer dereferencing at all
• Anything that considers the control flow guard at any point
• Pointer liveness or dynamic allocation consideration

A reasonable amount of SMT conversion complexity comes from the eccentricities of different solvers. This is a necessary part of working in the tar pit.

See also

smt_solver_baset

symex_target_equationt

create_solver

smt_solver_baset::mk_func_app