cprover
|
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.
prop_conv.h
which defines prop_convt
. This is the base class that is used to interface to the decision procedures. The key functions are convert
which takes an exprt
and converts it to the appropriate, solver specific, data structures and dec_solve
(inherited from decision_proceduret
) which invokes the actual decision procedures. Individual decision procedures (named *_dect
) objects can be created but prop_convt
is the preferred interface for code that uses them.floatbv
as necessary. Is implemented as a simple conversion (with caching) and then a post-processing function that adds extra constraints. This is not used by the SMT2 back-ends.smt2_dect
type which converts the formulae to SMTLib 2 and then invokes one of Boolector, CVC3, CVC4, MathSAT, Yices or Z3. Note that the interaction with the solver is batched and uses temporary files rather than using the interactive command supported by SMTLib 2. With the –fpa
option, this output mode will not flatten the floating point arithmetic and instead output the proposed SMTLib floating point standard.To be documented.
To be documented.
To be documented.
In the solvers directory.
Key classes:
In the solvers directory.
Key classes:
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:
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’}`.
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:
string_refinementt::set_to(const exprt &expr, bool value)
: Record the constraints to ensure that the expression is true when the boolean is true and false otherwise.string_refinementt::dec_solve()
: Main decision procedure of the solver.string_refinementt::get(const exprt &expr) const
: Evaluates the given expression in the valuation found by string_refinementt::dec_solve.For each goal given to CProver:
set_to
is called on several equations, roughly one for each step of the symbolic execution that leads to that goal;dec_solve
is called to determine whether the goal is reachable given these equations;get
is called by the interpreter to obtain concrete value to build a trace leading to the goal;set_to
remain valid.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:
char_pointer1 = b ? char_pointer2 : char_pointer3
where char_pointer<i>
variables are of type pointer to characters and b
is a Boolean expression.i = cprover_primitive(args)
where i
is of signed bit vector type. String primitives are listed in the next section.bv_refinementt
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
.
cprover_string_associate_array_to_pointer
: Link with an array of characters of the program.cprover_string_associate_length_to_array
: Link the length of the array with the given integer value.cprover_string_char_at
: Character at a given position. More... cprover_string_length
: Length of a string. More... cprover_string_compare_to
: Lexicographic comparison of two strings. More... cprover_string_contains
: Test whether a string contains another. More... cprover_string_equals
: Equality of the content of two strings. More... cprover_string_equals_ignore_case
: Equality of the content ignoring case of characters. More... cprover_string_hash_code
: Value that is identical for strings with the same content. More... cprover_string_is_prefix
: Test if the target is a prefix of the string. More... cprover_string_index_of
: Index of the first occurence of a target inside the string. More... cprover_string_last_index_of
: Index of the last occurence of a target inside the string. More... cprover_string_char_set
: Set of constraints ensuring that result
is similar to input
where the character at index position
is set to character
. More... cprover_string_concat
: Add axioms enforcing that res
is equal to the concatenation of s1
and s2
. More... cprover_string_delete
: Remove a portion of a string. More... cprover_string_insert
: Insertion of a string in another at a specific index. More... cprover_string_replace
: Replace a character by another in a string. More... cprover_string_set_length
: Reduce or extend a string to have the given length. More... cprover_string_substring
: Substring of a string between two indices. More... cprover_string_to_lower_case
: Set of constraints ensuring result
corresponds to input
in which uppercase characters have been converted to lowercase. More... cprover_string_to_upper_case
: Set of constraints ensuring result
corresponds to input
in which lowercase characters of Basic Latin and Latin-1 supplement of unicode have been converted to uppercase. More... cprover_string_trim
: Remove leading and trailing whitespaces. More... cprover_string_format
: Formatted string using a format string and list of arguments. More... cprover_string_from_literal
: String corresponding to an internal cprover string. More... cprover_string_of_int
: Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String.valueOf(J) Java functions applied on the integer expression. More... cprover_string_of_float
: Add axioms corresponding to the integer part of m, in decimal form with no leading zeroes, followed by '. More... cprover_string_of_float_scientific_notation
: Representation of a float value in scientific notation. More... cprover_string_of_char
: Conversion from char to string. More... cprover_string_parse_int
: Integer value represented by a string. More... cprover_string_concat_code_point
, cprover_string_code_point_at
, cprover_string_code_point_before
, cprover_string_code_point_count
: Java specific, should be part of Java models.cprover_string_offset_by_code_point
, cprover_string_concat_char
, cprover_string_concat_int
, cprover_string_concat_long
, cprover_string_concat_bool
, cprover_string_concat_double
, cprover_string_concat_float
, cprover_string_insert_int
, cprover_string_insert_long
, cprover_string_insert_bool
, cprover_string_insert_char
, cprover_string_insert_double
, cprover_string_insert_float
: Should be done in two steps: conversion from primitive type and call to the string primitive.cprover_string_array_of_char_pointer
, cprover_string_to_char_array
: Pointer to char array association is now handled by string_constraint_generatort
, there is no need for explicit conversion.cprover_string_intern
: Never tested.cprover_string_is_empty
: Should use cprover_string_length(s) == 0
instead.cprover_string_is_suffix
: Should use cprover_string_is_prefix
with an offset argument.cprover_string_empty_string
: Can use literal of empty string instead.cprover_string_of_long
: Should be the same as cprover_string_of_int
.cprover_string_delete_char_at
: A call to cprover_string_delete_char_at(s, i)
would be the same thing as cprover_string_delete(s, i, i+1)
.cprover_string_of_bool
: Language dependent, should be implemented in the models.cprover_string_copy
: Same as cprover_string_substring(s, 0)
.cprover_string_of_int_hex
: Same as cprover_string_of_int(s, 16)
.cprover_string_of_double
: Same as cprover_string_of_float
.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.
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> &)
.
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.
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:
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.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> ¬_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:
str
appears in P
indexed by some f(x)
and val
is in the index set of str
we find y
such that f(y)=val
and add lemma P(y)
. (See instantiate(messaget::mstreamt&,const string_constraintt&,const exprt &,const exprt&)
for details)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)
For each string_constraint a
:
a
is an existential formula b
;b
by their values found in get
;b
is simplified and array accesses are replaced by expressions without arrays;b
to a fresh solver;b
is found, this means the constraint a
is satisfied by the valuation given by get. true
if the current model satisfies all the axioms, false
otherwise with a list of lemmas which are obtained by instantiating constraints at indexes given by counter-examples.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.