From db3e044944d88337e047004df8540fb99624d5f4 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 8 Jan 2018 12:58:39 +0000 Subject: [PATCH 1/3] Add introduction to string solver documentation --- src/solvers/refinement/README.md | 46 ++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/src/solvers/refinement/README.md b/src/solvers/refinement/README.md index b3914fb1ded..c3ac7ab0daf 100644 --- a/src/solvers/refinement/README.md +++ b/src/solvers/refinement/README.md @@ -6,6 +6,52 @@ \section string_solver_interface String solver interface +The basic role of the solver 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. +For instance, CBMC and JBMC, convert a input program and property to check +about this program to a set of equations. These equations are fed to a solver, +which is one of the last step in CBMC and JBMC, as it tells us whether the +property holds or can fail. + +The secondary role of the solver is to provide a satisfying assignment of +the variables of the equations, this can for instance be used to construct +a trace. + +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 From 549eb57f6af07bac7e1d2dd14237438049621214 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 9 Jan 2018 13:20:18 +0000 Subject: [PATCH 2/3] Delete trailing whitespaces --- src/solvers/refinement/README.md | 74 ++++++++++++++++---------------- 1 file changed, 37 insertions(+), 37 deletions(-) diff --git a/src/solvers/refinement/README.md b/src/solvers/refinement/README.md index c3ac7ab0daf..6adb77e703f 100644 --- a/src/solvers/refinement/README.md +++ b/src/solvers/refinement/README.md @@ -7,14 +7,14 @@ \section string_solver_interface String solver interface The basic role of the solver is to answer whether the set of equations given -is satisfiable. One example usage, is to determine whether an assertion in a +is satisfiable. One example usage, is to determine whether an assertion in a program can be violated. -For instance, CBMC and JBMC, convert a input program and property to check +For instance, CBMC and JBMC, convert a input program and property to check about this program to a set of equations. These equations are fed to a solver, -which is one of the last step in CBMC and JBMC, as it tells us whether the +which is one of the last step in CBMC and JBMC, as it tells us whether the property holds or can fail. -The secondary role of the solver is to provide a satisfying assignment of +The secondary role of the solver is to provide a satisfying assignment of the variables of the equations, this can for instance be used to construct a trace. @@ -54,57 +54,57 @@ equation true, in that case `length2 = length3 = 1` and \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 @@ -118,7 +118,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 @@ -127,10 +127,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` : @@ -145,25 +145,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` : @@ -172,7 +172,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` : @@ -212,18 +212,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. @@ -232,15 +232,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 @@ -249,9 +249,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 From 1d1be4ccceac5cf4888db0730c3f1e39ec8513f6 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 12 Jan 2018 14:45:59 +0000 Subject: [PATCH 3/3] Move non-string-specific part of doc to solvers This is a more appropriate place since it is not at all specific to strings. --- src/solvers/module.md | 13 +++++++++++++ src/solvers/refinement/README.md | 12 ------------ 2 files changed, 13 insertions(+), 12 deletions(-) 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 6adb77e703f..0743a8098df 100644 --- a/src/solvers/refinement/README.md +++ b/src/solvers/refinement/README.md @@ -6,18 +6,6 @@ \section string_solver_interface String solver interface -The basic role of the solver 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. -For instance, CBMC and JBMC, convert a input program and property to check -about this program to a set of equations. These equations are fed to a solver, -which is one of the last step in CBMC and JBMC, as it tells us whether the -property holds or can fail. - -The secondary role of the solver is to provide a satisfying assignment of -the variables of the equations, this can for instance be used to construct -a trace. - 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.