cprover
solvers

Folder solvers

Authors
Romain Brenguier, Kareem Khazem, Martin Brain

Overview

The basic role of solvers is to answer whether the set of equations given is satisfiable. One example usage, is to determine whether an assertion in a program can be violated. We refer to goto-symex for how CBMC and JBMC convert a input program and property to a set of equations.

The secondary role of solvers is to provide a satisfying assignment of the variables of the equations, this can for instance be used to construct a trace.

The solvers/ directory contains interfaces to a number of different decision procedures, roughly one per directory.

Flattening

To be documented.

Solver APIs

SMT solving API

To be documented.

SAT solving API

To be documented.

SAT/SMT Encoding

In the solvers directory.

Key classes:


Decision Procedure

In the solvers directory.

Key classes:

String Solver Interface

The string solver is particularly aimed at string logic, but since it inherits from bv_refinementt it is also capable of handling arithmetic, array logic, floating point operations etc. The backend uses the flattening of boolbvt to convert expressions to boolean formula.

An example of a problem given to string solver could look like this:

return_code == cprover_string_concat_func(
length1, array1,
{ .length=length2, .content=content2 },
{ .length=length3, .content=content3 })
length3 == length2
content3 == content2
is_equal == cprover_string_equals_func(length1, array1, 2, {'a', 'a'})
is_equal == 1

Details about the meaning of the primitives cprover_string_concat_func and cprover_string_equals_func are given in section String Primitives.

The first equality means that the string represented by {length1, array1} is the concatanation of the string represented by {length2, array2} and {length3, array3}. The second and third mean that {length2, array2} and {length3, array3} represent the same string. The fourth means that is_equal is 1 if and only if {length1, array1} is the string "aa". The last equation ensures that is_equal has to be equal to 1 in the solution.

For this system of equations the string solver should answer that it is satisfiable. It is then possible to recover which assignments make all equation true, in that case length2 = length3 = 1 and ‘content2 = content3 = {'a’}`.

General interface

The common interface for solvers in CProver is inherited from decision_proceduret and is the common interface for all solvers. It is essentially composed of these three functions:

For each goal given to CProver:

Specificity of the string solver

The specificity of the solver is in what kind of expressions set_to accepts and understands. string_refinementt::set_to accepts all constraints that are normally accepted by bv_refinementt.

string_refinementt::set_to also understands constraints of the form:

Note
In the implementation, equations that are not of these forms are passed to an embedded bv_refinementt solver.

String representation in the solver

String primitives can have arguments which are pointers to characters. These pointers represent strings. To each of these pointers the string solver associate a char array which represents the content of the string. If the pointer is the address of an actual array in the program they should be linked by using the primitive cprover_string_associate_array_to_pointer. The length of the array can also be linked to a variable of the program using cprover_string_associate_length_to_array.

Warning
The solver assumes the memory pointed by the arguments is immutable which is not something that is true in general for C pointers for instance. Therefore for each transformation on a string, it is assumed the program allocates a new string before calling a primitive.

String primitives

Basic access:

Comparisons:

Transformations:

Conversions:

Deprecated primitives:

Decision algorithm

Looks for a valuation of variables compatible with the constraints that have been given to set_to so far.

The decision procedure initiated by string_refinementt::dec_solve is composed of several steps detailed below.

Symbol resolution

Pointer symbols which are set to be equal by constraints, are replaced by an single symbol in the solver. The symbol_solvert object used for this substitution is constructed by generate_symbol_resolution_from_equations(const std::vector<equal_exprt>&,const namespacet&,messaget::mstreamt&). All these symbols are then replaced using replace_symbols_in_equations(const union_find_replacet &, std::vector<equal_exprt> &).

Conversion to first order formulas:

Each string primitive is converted to a list of first order formulas by the function substitute_function_applications_in_equations(std::vector<equal_exprt>&,string_constraint_generatort&). These formulas should be unquantified or be either a string_constraintt or a string_not_contains_constraintt. The constraints corresponding to each primitive can be found by following the links in section String primitives.

Since only arrays appear in the string constraints, during the conversion to first order formulas, pointers are associated to arrays. The string_constraint_generatort object keeps track of this association. It can either be set manually using the primitives cprover_associate_array_to_pointer or a fresh array is created.

Refinement loop

We use super_dec_solve and super_get to denote the methods of the underlying solver (bv_refinementt by default). The refinement loop relies on functions string_refinementt::check_axioms which returns true when the set of quantified constraints q is satisfied by the valuation given bysuper_get and string_refinementt::instantiate which gives propositional formulas implied by a string constraint. If the following algorithm returns SAT or UNSAT, the given constraints are SAT or UNSAT respectively:

is_SAT(unquantified_constraints uq, quantified_constraints q)
{
cur <- uq;
while(limit--) > 0
{
if(super_dec_solve(cur)==SAT)
{
if(check_axioms(q, super_get))
else
for(axiom in q)
cur.add(instantiate(axiom));
return SAT;
}
else
return UNSAT;
}
return ERROR;
}
Returns
resultt::D_SATISFIABLE if the constraints are satisfiable, resultt::D_UNSATISFIABLE if they are unsatisfiable, resultt::D_ERROR if the limit of iteration was reached.

Instantiation

This is done by generate_instantiations(const index_set_pairt &index_set, const string_axiomst &axioms, const std::unordered_map<string_not_contains_constraintt, symbol_exprt> &not_contain_witnesses). The string refinement decision procedure works with two types of quantified axioms, which are of the form \(\forall x.\ P(x)\) (string_constraintt) or of the form \(\forall x. P(x) \Rightarrow \exists y .s_0[x+y] \ne s_1[y] \) (string_not_contains_constraintt). They are instantiated in a way which depends on their form:

For formulas of the form \(\forall x. P(x) \Rightarrow \exists y .s_0[x+y] \ne s_1[y]) \) we need to look at the index set of both s_0 and s_1. (See instantiate(const string_not_contains_constraintt&,const index_set_pairt&,const std::map<string_not_contains_constraintt, symbol_exprt>&) for details)

Axiom check

For each string_constraint a:

Floatbv Directory

This library contains the code that is used to convert floating point variables (floatbv) to bit vectors (bv). This is referred to as ‘bit-blasting’ and is called in the solver code during conversion to SAT or SMT. It also contains the abstraction code described in the FMCAD09 paper.