diff --git a/src/solvers/module.md b/src/solvers/module.md index 98eeae6719e..0369735e555 100644 --- a/src/solvers/module.md +++ b/src/solvers/module.md @@ -3,6 +3,19 @@ \author Kareem Khazem +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 \ref module_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 most general solver in terms of supported equations is \ref string-solver. + \section sat-smt-encoding SAT/SMT Encoding In the \ref solvers directory. diff --git a/src/solvers/refinement/README.md b/src/solvers/refinement/README.md index b3914fb1ded..0743a8098df 100644 --- a/src/solvers/refinement/README.md +++ b/src/solvers/refinement/README.md @@ -6,59 +6,93 @@ \section string_solver_interface String solver interface +The string solver is particularly aimed at string logic, but since it inherits +from \ref bv_refinementt it is also capable of handling arithmetic, array logic, +floating point operations etc. +The backend uses the flattening of \ref 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 \ref primitives "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'}`. + + \subsection general_interface General interface -The common interface for solvers in CProver is inherited from +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)`: + - `string_refinementt::set_to(const exprt &expr, bool value)`: \copybrief string_refinementt::set_to - - `string_refinementt::dec_solve()`: + - `string_refinementt::dec_solve()`: \copybrief string_refinementt::dec_solve - - `string_refinementt::get(const exprt &expr) const`: + - `string_refinementt::get(const exprt &expr) const`: \copybrief string_refinementt::get - + For each goal given to CProver: - - `set_to` is called on several equations, roughly one for each step of the + - `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; - - The same process can be repeated for further goals, in that case the + - The same process can be repeated for further goals, in that case the constraints added by previous calls to `set_to` remain valid. \subsection specificity Specificity of the string solver -The specificity of the solver is in what kind of expressions `set_to` accepts +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` + * `char_pointer1 = b ? char_pointer2 : char_pointer3` where `char_pointer` 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. -\note In the implementation, equations that are not of these forms are passed +\note In the implementation, equations that are not of these forms are passed to an embedded `bv_refinementt` solver. \subsection string-representation 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 +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 +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 +Therefore for each transformation on a string, it is assumed the program allocates a new string before calling a primitive. \section primitives String primitives @@ -72,7 +106,7 @@ allocates a new string before calling a primitive. * `cprover_string_char_at` : \copybrief string_constraint_generatort::add_axioms_for_char_at(const function_application_exprt &f) \link string_constraint_generatort::add_axioms_for_char_at(const function_application_exprt &f) More... \endlink - * `cprover_string_length` : + * `cprover_string_length` : \copybrief string_constraint_generatort::add_axioms_for_length(const function_application_exprt &f) \link string_constraint_generatort::add_axioms_for_length(const function_application_exprt &f) More... \endlink @@ -81,10 +115,10 @@ allocates a new string before calling a primitive. * `cprover_string_compare_to` : \copybrief string_constraint_generatort::add_axioms_for_compare_to(const function_application_exprt &f) \link string_constraint_generatort::add_axioms_for_compare_to(const function_application_exprt &f) More... \endlink - * `cprover_string_contains` : + * `cprover_string_contains` : \copybrief string_constraint_generatort::add_axioms_for_contains(const function_application_exprt &f) \link string_constraint_generatort::add_axioms_for_contains(const function_application_exprt &f) More... \endlink - * `cprover_string_equals` : + * `cprover_string_equals` : \copybrief string_constraint_generatort::add_axioms_for_equals(const function_application_exprt &f) \link string_constraint_generatort::add_axioms_for_equals(const function_application_exprt &f) More... \endlink * `cprover_string_equals_ignore_case` : @@ -99,25 +133,25 @@ allocates a new string before calling a primitive. * `cprover_string_is_suffix` : \copybrief string_constraint_generatort::add_axioms_for_is_suffix \link string_constraint_generatort::add_axioms_for_is_suffix More... \endlink - * `cprover_string_index_of` : + * `cprover_string_index_of` : \copybrief string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f) \link string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f) More... \endlink * `cprover_string_last_index_of` : \copybrief string_constraint_generatort::add_axioms_for_last_index_of(const function_application_exprt &f) \link string_constraint_generatort::add_axioms_for_last_index_of(const function_application_exprt &f) More... \endlink -\subsection transformations Transformations: +\subsection transformations Transformations: * `cprover_string_char_set` : \copybrief string_constraint_generatort::add_axioms_for_char_set(const function_application_exprt &f) \link string_constraint_generatort::add_axioms_for_char_set(const function_application_exprt &f) More... \endlink - * `cprover_string_concat` : + * `cprover_string_concat` : \copybrief string_constraint_generatort::add_axioms_for_concat(const function_application_exprt &f) \link string_constraint_generatort::add_axioms_for_concat(const function_application_exprt &f) More... \endlink * `cprover_string_delete` : \copybrief string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f) \link string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f) More... \endlink - * `cprover_string_insert` : + * `cprover_string_insert` : \copybrief string_constraint_generatort::add_axioms_for_insert(const function_application_exprt &f) \link string_constraint_generatort::add_axioms_for_insert(const function_application_exprt &f) More... \endlink * `cprover_string_replace` : @@ -126,7 +160,7 @@ allocates a new string before calling a primitive. * `cprover_string_set_length` : \copybrief string_constraint_generatort::add_axioms_for_set_length(const function_application_exprt &f) \link string_constraint_generatort::add_axioms_for_set_length(const function_application_exprt &f) More... \endlink - * `cprover_string_substring` : + * `cprover_string_substring` : \copybrief string_constraint_generatort::add_axioms_for_substring(const function_application_exprt &f) \link string_constraint_generatort::add_axioms_for_substring(const function_application_exprt &f) More... \endlink * `cprover_string_to_lower_case` : @@ -166,18 +200,18 @@ allocates a new string before calling a primitive. \subsection deprecated Deprecated primitives: * `cprover_string_concat_code_point`, `cprover_string_code_point_at`, - `cprover_string_code_point_before`, `cprover_string_code_point_count`: + `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_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_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` : + `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` : + * `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. @@ -186,15 +220,15 @@ allocates a new string before calling a primitive. Should use `cprover_string_length(s) == 0` instead. * `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_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`. - + \section algorithm Decision algorithm \copydetails string_refinementt::dec_solve @@ -203,9 +237,9 @@ allocates a new string before calling a primitive. This is done by generate_instantiations(messaget::mstreamt &stream, const namespacet &ns, const string_constraint_generatort &generator, const index_set_pairt &index_set, const string_axiomst &axioms). \copydetails generate_instantiations(messaget::mstreamt &stream, const namespacet &ns, const string_constraint_generatort &generator, const index_set_pairt &index_set, const string_axiomst &axioms) - + \subsection axiom-check Axiom check \copydetails check_axioms(const string_axiomst &axioms, string_constraint_generatort &generator, const std::function &get, messaget::mstreamt &stream, const namespacet &ns, std::size_t max_string_length, bool use_counter_example, ui_message_handlert::uit ui, const union_find_replacet &symbol_resolve) -\link check_axioms(const string_axiomst &axioms, string_constraint_generatort &generator, const std::function &get, messaget::mstreamt &stream, const namespacet &ns, std::size_t max_string_length, bool use_counter_example, ui_message_handlert::uit ui, const union_find_replacet &symbol_resolve) +\link check_axioms(const string_axiomst &axioms, string_constraint_generatort &generator, const std::function &get, messaget::mstreamt &stream, const namespacet &ns, std::size_t max_string_length, bool use_counter_example, ui_message_handlert::uit ui, const union_find_replacet &symbol_resolve) (See function documentation...) \endlink