Merge pull request #1709 from romainbrenguier/doc/string-solver-intro

Add introduction to string solver documentation TG-838

Author: romainbrenguier

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.

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<i>` 
+  * `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.
 
-\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<exprt(const exprt &)> &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<exprt(const exprt &)> &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<exprt(const exprt &)> &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