diff --git a/src/solvers/refinement/README.md b/src/solvers/refinement/README.md new file mode 100644 index 00000000000..b3914fb1ded --- /dev/null +++ b/src/solvers/refinement/README.md @@ -0,0 +1,211 @@ +\page string-solver String solver + +\author Romain Brenguier + +\tableofcontents + +\section string_solver_interface String solver interface + +\subsection general_interface 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: + + - `string_refinementt::set_to(const exprt &expr, bool value)`: + \copybrief string_refinementt::set_to + - `string_refinementt::dec_solve()`: + \copybrief string_refinementt::dec_solve + - `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 + 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 + 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 +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` + 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 + 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 +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. + +\section primitives String primitives + +\subsection basic-primitives Basic access: + + * `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` : + \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` : + \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 + +\subsection comparisons Comparisons: + + * `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` : + \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` : + \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` : + \copybrief string_constraint_generatort::add_axioms_for_equals_ignore_case(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_equals_ignore_case(const function_application_exprt &f) More... \endlink + * `cprover_string_hash_code` : + \copybrief string_constraint_generatort::add_axioms_for_hash_code + \link string_constraint_generatort::add_axioms_for_hash_code More... \endlink + * `cprover_string_is_prefix` : + \copybrief string_constraint_generatort::add_axioms_for_is_prefix + \link string_constraint_generatort::add_axioms_for_is_prefix More... \endlink + * `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` : + \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: + + * `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` : + \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` : + \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` : + \copybrief string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f) More... \endlink + * `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` : + \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` : + \copybrief string_constraint_generatort::add_axioms_for_to_lower_case(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_to_lower_case(const function_application_exprt &f) More... \endlink + * `cprover_string_to_upper_case` : + \copybrief string_constraint_generatort::add_axioms_for_to_upper_case(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_to_upper_case(const function_application_exprt &f) More... \endlink + * `cprover_string_trim` : + \copybrief string_constraint_generatort::add_axioms_for_trim(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_trim(const function_application_exprt &f) More... \endlink + +\subsection conversions Conversions: + + * `cprover_string_format` : + \copybrief string_constraint_generatort::add_axioms_for_format(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_format(const function_application_exprt &f) More... \endlink + * `cprover_string_from_literal` : + \copybrief string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f) More... \endlink + * `cprover_string_of_int` : + \copybrief string_constraint_generatort::add_axioms_from_int(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_from_int(const function_application_exprt &f) More... \endlink + * `cprover_string_of_float` : + \copybrief string_constraint_generatort::add_axioms_for_string_of_float(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_string_of_float(const function_application_exprt &f) More... \endlink + * `cprover_string_of_float_scientific_notation` : + \copybrief string_constraint_generatort::add_axioms_from_float_scientific_notation(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_from_float_scientific_notation(const function_application_exprt &f) More... \endlink + * `cprover_string_of_char` : + \copybrief string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f) More... \endlink + * `cprover_string_parse_int` : + \copybrief string_constraint_generatort::add_axioms_for_parse_int(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_parse_int(const function_application_exprt &f) More... \endlink + +\subsection deprecated Deprecated primitives: + + * `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_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`. + +\section algorithm Decision algorithm + +\copydetails string_refinementt::dec_solve + +\subsection instantiation Instantiation + +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) + (See function documentation...) \endlink diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h index 5172c277d1b..1066235b61e 100644 --- a/src/solvers/refinement/string_constraint.h +++ b/src/solvers/refinement/string_constraint.h @@ -26,29 +26,32 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include -/*! \brief Universally quantified string constraint - - This represents a universally quantified string constraint as laid out in - DOI: 10.1007/978-3-319-03077-7. The paper seems to specify a universal - constraint as follows. - - A universal constraint is of the form \f$\forall n. L(n) \rightarrow - P(n, s_0,\ldots, s_k)\f$ where - - 1. \f$L(n)\f$ does not contain string indices [possibly not required, but - implied by examples] - 2. \f$\forall n. L(n) \rightarrow P'\left(s_0[f_0(n)],\ldots, s_k[f_k(n)] - \right)\f$, i.e. when focusing on one specific string, all indices are - the same [stated in a roundabout manner] - 3. Each \f$f\f$ is linear and therefore has an inverse [explicitly stated] - 4. \f$L(n)\f$ and \f$P(n, s_0,\ldots, s_k)\f$ may contain other (free) - variables, but in \f$P\f$, \f$n\f$ can only occur as an argument to an - \f$f\f$ [explicitly stated, implied] - - We extend this slightly by restricting n to be in a specific range, but this - is another implication which can be pushed in to \f$L(n)\f$. -*/ - +/// ### Universally quantified string constraint +/// +/// This represents a universally quantified string constraint as laid out in +/// DOI: 10.1007/978-3-319-03077-7. The paper seems to specify a universal +/// constraint as follows. +/// +/// A universal constraint is of the form +/// \f$ \forall i.\ PI(i) \Rightarrow PV(i)\f$ +/// where \f$PI\f$ and \f$PV\f$ satisfies the following conditions: +/// +/// * The predicate `PI` , called the index guard, must follow the grammar +/// * \f$iguard : iguard \land iguard \mid iguard \lor iguard \mid +/// iterm \le iterm \mid iterm = iterm \f$ +/// * \f$iterm : integer\_constant1 \times i + integer\_constant2 \f$ +/// +/// * The predicate `PV` is called the value constraint. +/// The index variable `i` can only be used in array read expressions of +/// the form `a[i]`. +/// ie. `PV` is of the form \f$P'(s_0[f_0(i)],\ldots, s_k[f_k(i)] +/// )\f$, moreover when focusing on one specific string, all indices are +/// the same [stated in a roundabout manner]. +/// \f$L(n)\f$ and \f$P(n, s_0,\ldots, s_k)\f$ may contain other (free) +/// variables, but in \f$P\f$, \f$n\f$ can only occur as an argument to an +/// \f$f\f$ [explicitly stated, implied]. +/// +/// \todo The fact that we follow this grammar is not enforced at the moment. class string_constraintt: public exprt { public: @@ -155,6 +158,7 @@ inline std::string from_expr( from_expr(ns, identifier, expr.body()); } +/// Constraints to encode non containement of strings. class string_not_contains_constraintt: public exprt { public: diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 8d1c9c75546..2ca6347dd9b 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -211,36 +211,27 @@ class string_constraint_generatort final const array_string_exprt &str, const exprt &c, const exprt &from_index); - - // Add axioms corresponding to the String.indexOf:(String;I) java function exprt add_axioms_for_index_of_string( const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index); - - // Add axioms corresponding to the String.indexOf java functions exprt add_axioms_for_index_of(const function_application_exprt &f); - - // Add axioms corresponding to the String.lastIndexOf:(String;I) java function exprt add_axioms_for_last_index_of_string( const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index); - - // Add axioms corresponding to the String.lastIndexOf:(CI) java function exprt add_axioms_for_last_index_of( const array_string_exprt &str, const exprt &c, const exprt &from_index); - // Add axioms corresponding to the String.lastIndexOf java functions exprt add_axioms_for_last_index_of(const function_application_exprt &f); - // TODO: the specifications of these functions is only partial - // We currently only specify that the string for NaN is "NaN", for infinity - // and minus infinity the string are "Infinity" and "-Infinity respectively - // otherwise the string contains only characters in [0123456789.] and '-' at - // the start for negative number + /// \todo The specifications of these functions is only partial. + /// We currently only specify that the string for NaN is "NaN", for infinity + /// and minus infinity the string are "Infinity" and "-Infinity respectively + /// otherwise the string contains only characters in [0123456789.] and '-' at + /// the start for negative number exprt add_axioms_for_string_of_float(const function_application_exprt &f); exprt add_axioms_for_string_of_float(const array_string_exprt &res, const exprt &f); @@ -254,16 +245,16 @@ class string_constraint_generatort final exprt add_axioms_from_float_scientific_notation( const function_application_exprt &f); - // Add axioms corresponding to the String.valueOf(D) java function - // TODO: the specifications is only partial + /// Add axioms corresponding to the String.valueOf(D) java function + /// \todo The specifications is only partial. exprt add_axioms_from_double(const function_application_exprt &f); exprt add_axioms_for_replace(const function_application_exprt &f); exprt add_axioms_for_set_length(const function_application_exprt &f); - // TODO: the specification may not be correct for the case where the - // string is shorter than end. An actual java program should throw an - // exception in that case + /// \todo The specification may not be correct for the case where the + /// string is shorter than end. An actual java program should throw an + /// exception in that case. exprt add_axioms_for_substring( const array_string_exprt &res, const array_string_exprt &str, @@ -282,16 +273,18 @@ class string_constraint_generatort final const exprt &code_point); exprt add_axioms_for_char_literal(const function_application_exprt &f); - // Add axioms corresponding the String.codePointCount java function - // TODO: this function is underspecified, we do not compute the exact value - // but over approximate it. + /// Add axioms corresponding the String.codePointCount java function + /// \todo This function is underspecified, we do not compute the exact value + /// but over approximate it. + /// \deprecated This is Java specific and should be implemented in Java. exprt add_axioms_for_code_point_count(const function_application_exprt &f); - // Add axioms corresponding the String.offsetByCodePointCount java function - // TODO: this function is underspecified, it should return the index within - // this String that is offset from the given first argument by second argument - // code points and we approximate this by saying the result is - // between index + offset and index + 2 * offset + /// Add axioms corresponding the String.offsetByCodePointCount java function + /// \todo This function is underspecified, it should return the index within + /// this String that is offset from the given first argument by second + /// argument code points and we approximate this by saying the result is + /// between index + offset and index + 2 * offset. + /// \deprecated This is Java specific and should be implemented in Java. exprt add_axioms_for_offset_by_code_point( const function_application_exprt &f); @@ -313,9 +306,10 @@ class string_constraint_generatort final exprt add_axioms_for_parse_int(const function_application_exprt &f); exprt add_axioms_for_compare_to(const function_application_exprt &f); - // Add axioms corresponding to the String.intern java function - // TODO: this does not work at the moment because of the way we treat - // string pointers + /// Add axioms corresponding to the String.intern java function + /// \todo This does not work at the moment because of the way we treat + /// string pointers. + /// \deprecated Not tested. symbol_exprt add_axioms_for_intern(const function_application_exprt &f); exprt associate_array_to_pointer(const function_application_exprt &f); diff --git a/src/solvers/refinement/string_constraint_generator_comparison.cpp b/src/solvers/refinement/string_constraint_generator_comparison.cpp index 22f73351317..e59e8ef4ba7 100644 --- a/src/solvers/refinement/string_constraint_generator_comparison.cpp +++ b/src/solvers/refinement/string_constraint_generator_comparison.cpp @@ -13,12 +13,18 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include -/// add axioms stating that the result is true exactly when the strings -/// represented by the arguments are equal. the variable ending in -/// `witness_unequal` is -1 if the length differs or an index at which the -/// strings are different -/// \par parameters: function application with two string arguments -/// \return a expression of Boolean type +/// Equality of the content of two strings +/// +/// Add axioms stating that the result is true exactly when the strings +/// represented by the arguments are equal. +/// These axioms are: +/// 1. \f$ eq \Rightarrow |s_1|=|s_2|\f$ +/// 2. \f$ \forall i<|s_1|.\ eq \Rightarrow s_1[i]=s_2[i] \f$ +/// 3. \f$ \lnot eq \Rightarrow (|s_1| \ne |s_2| \land witness=-1) +/// \lor (0 \le witness<|s_1| \land s_1[witness] \ne s_2[witness]) \f$ +/// \param f: function application with arguments refined_string `s1` and +/// refined_string `s2` +/// \return Boolean expression `eq` exprt string_constraint_generatort::add_axioms_for_equals( const function_application_exprt &f) { @@ -32,13 +38,6 @@ exprt string_constraint_generatort::add_axioms_for_equals( typet index_type=s1.length().type(); - // We want to write: - // eq <=> (s1.length=s2.length &&forall i s1.length=s2.length - // a2 : forall i s1[i]=s2[i] - // a3 : !eq => (s1.length!=s2.length && witness=-1) - // || (0<=witness |s1|=|s2| - // a2 : forall qvar, 0<=qvar<|s1|, - // eq => char_equal_ignore_case(s1[qvar],s2[qvar]); - // a3 : !eq => |s1|!=s2 || (0 <=witness<|s1| &&!char_equal_ignore_case) - const implies_exprt a1(eq, equal_exprt(s1.length(), s2.length())); axioms.push_back(a1); @@ -146,10 +152,15 @@ exprt string_constraint_generatort::add_axioms_for_equals_ignore_case( return typecast_exprt(eq, f.type()); } -/// add axioms stating that if two strings are equal then their hash codes are -/// equals -/// \par parameters: function application with a string argument -/// \return a integer expression corresponding to the hash code of the string +/// Value that is identical for strings with the same content +/// +/// Add axioms stating that if two strings are equal then the values +/// returned by this function are equal. +/// These axioms are, for each string `s` on which hash was called: +/// * \f$ hash(str)=hash(s) \lor |str| \ne |s| +/// \lor (|str|=|s| \land \exists i<|s|.\ s[i]\ne str[i]) \f$ +/// \param f: function application with argument refined_string `str` +/// \return integer expression `hash(str)` exprt string_constraint_generatort::add_axioms_for_hash_code( const function_application_exprt &f) { @@ -162,12 +173,6 @@ exprt string_constraint_generatort::add_axioms_for_hash_code( std::make_pair(str, fresh_symbol("hash", return_type))); const exprt hash = pair.first->second; - // for each string s. either: - // c1: hash(str)=hash(s) - // c2: |str|!=|s| - // c3: (|str|==|s| && exists i<|s|. s[i]!=str[i]) - - // WARNING: the specification may be incomplete for(auto it : hash_code_of_string) { const symbol_exprt i = fresh_exist_index("index_hash", index_type); @@ -183,9 +188,25 @@ exprt string_constraint_generatort::add_axioms_for_hash_code( return hash; } -/// add axioms corresponding to the String.compareTo java function -/// \par parameters: function application with two string arguments -/// \return a integer expression +/// Lexicographic comparison of two strings +/// +/// Add axioms ensuring the result corresponds to that of the `String.compareTo` +/// Java function. +/// In the lexicographic comparison, `x` representing the first point where the +/// two strings differ, we add axioms: +/// * \f$ res=0 \Rightarrow |s1|=|s2|\f$ +/// * \f$ \forall i<|s1|. s1[i]=s2[i] \f$ +/// * \f$ \exists x.\ res\ne 0 \Rightarrow x > 0 +/// \land ((|s1| \ge |s2| \land x<|s1|) +/// \lor (|s1| \ge |s2| \land x<|s2|) +/// \land res=s1[x]-s2[x] ) +/// \lor cond2: +/// (|s1|<|s2| \land x=|s1|) \lor (|s1| > |s2| \land x=|s2|) +/// \land res=|s1|-|s2|) \f$ +/// * \f$ \forall i' |s1|=|s2| - // a2 : forall i<|s1|. s1[i]==s2[i] - // a3 : exists x. - // res!=0 ==> x > 0 - // && ((|s1| <= |s2| && x<|s1|) || (|s1| >= |s2| &&x<|s2|) - // && res=s1[x]-s2[x] ) - // || cond2: - // (|s1|<|s2| &&x=|s1|) || (|s1| > |s2| &&x=|s2|) &&res=|s1|-|s2|) - // a4 : forall i' s1[i]=s2[i] - const equal_exprt res_null(res, from_integer(0, return_type)); const implies_exprt a1(res_null, equal_exprt(s1.length(), s2.length())); axioms.push_back(a1); @@ -253,9 +261,10 @@ exprt string_constraint_generatort::add_axioms_for_compare_to( return res; } -/// add axioms stating that the return value for two equal string should be the +/// Add axioms stating that the return value for two equal string should be the /// same -/// \par parameters: function application with one string argument +/// \deprecated never tested +/// \param f: function application with one string argument /// \return a string expression symbol_exprt string_constraint_generatort::add_axioms_for_intern( const function_application_exprt &f) diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp index 8a85267e803..1c002590ef2 100644 --- a/src/solvers/refinement/string_constraint_generator_concat.cpp +++ b/src/solvers/refinement/string_constraint_generator_concat.cpp @@ -21,12 +21,22 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// If `end_index > |s2|` and/or `start_index < 0`, the appended string will /// be of length `end_index - start_index` and padded with non-deterministic /// values. -/// \param res: an array of character -/// \param s1: string expression -/// \param s2: string expression -/// \param start_index: expression representing an integer -/// \param end_index: expression representing an integer -/// \return a new string expression +/// +/// These axioms are: +/// 1. \f$end\_index > start\_index \Rightarrow |res| = |s_1| + end\_index - +/// start\_index +/// \f$ +/// 2. \f$end\_index \le start\_index \Rightarrow res = s_1 \f$ +/// 3. \f$\forall i<|s_1|. res[i]=s_1[i] \f$ +/// 4. \f$\forall i< end\_index - start\_index.\ res[i+|s_1|] +/// = s_2[start\_index+i]\f$ +/// +/// \param res: an array of characters expression +/// \param s1: an array of characters expression +/// \param s2: an array of characters expression +/// \param start_index: integer expression +/// \param end_index: integer expression +/// \return integer expression `0` exprt string_constraint_generatort::add_axioms_for_concat_substr( const array_string_exprt &res, const array_string_exprt &s1, @@ -34,12 +44,6 @@ exprt string_constraint_generatort::add_axioms_for_concat_substr( const exprt &start_index, const exprt &end_index) { - // We add axioms: - // a1 : end_index > start_index => |res|=|s1|+ end_index - start_index - // a2 : end_index <= start_index => res = s1 - // a3 : forall i<|s1|. res[i]=s1[i] - // a4 : forall i< end_index - start_index. res[i+|s1|]=s2[start_index+i] - binary_relation_exprt prem(end_index, ID_gt, start_index); exprt res_length=plus_exprt_with_overflow_check( @@ -66,6 +70,11 @@ exprt string_constraint_generatort::add_axioms_for_concat_substr( /// Add axioms enforcing that `res` is the concatenation of `s1` with /// character `c`. +/// These axioms are : +/// * \f$ |res|=|s1|+1 \f$ +/// * \f$ \forall i<|s1|. res[i]=s1[i] \f$ +/// * \f$ res[|s1|]=c \f$ +/// /// \param res: string expression /// \param s1: string expression /// \param c: character expression @@ -75,11 +84,6 @@ exprt string_constraint_generatort::add_axioms_for_concat_char( const array_string_exprt &s1, const exprt &c) { - // We add axioms: - // a1 : |res|=|s1|+1 - // a2 : forall i<|s1|. res[i]=s1[i] - // a3 : res[|s1|]=c - const typet &index_type = res.length().type(); const equal_exprt a1( res.length(), plus_exprt(s1.length(), from_integer(1, index_type))); @@ -96,7 +100,10 @@ exprt string_constraint_generatort::add_axioms_for_concat_char( return from_integer(0, get_return_code_type()); } -/// Add axioms to say that `res` is equal to the concatenation of `s1` and `s2`. +/// Add axioms enforcing that `res` is equal to the concatenation of `s1` and +/// `s2`. +/// +/// \deprecated should use concat_substr instead /// \param res: string_expression corresponding to the result /// \param s1: the string expression to append to /// \param s2: the string expression to append to the first one @@ -110,16 +117,17 @@ exprt string_constraint_generatort::add_axioms_for_concat( return add_axioms_for_concat_substr(res, s1, s2, index_zero, s2.length()); } -/// Add axioms enforcing that the returned string expression is equal to the -/// concatenation of the two string arguments of the function application. +/// String concatenation /// -/// In case 4 arguments instead of 2 are given the last two arguments are -/// intepreted as a start index and last index from which we extract a substring -/// of the second argument: this is similar to the Java -/// StringBuilder.append(CharSequence s, int start, int end) method. +/// This primitive accepts 4 or 6 arguments. +/// \copybrief string_constraint_generatort::add_axioms_for_concat_substr +/// \link string_constraint_generatort::add_axioms_for_concat_substr +/// (More...) \endlink /// -/// \param f: function application with two string arguments -/// \return a new string expression +/// \param f: function application with arguments integer `|res|`, character +/// pointer `&res[0]`, refined_string `s1`, refined_string `s2`, +/// optional integer `start_index`, optional integer `end_index` +/// \return an integer expression exprt string_constraint_generatort::add_axioms_for_concat( const function_application_exprt &f) { @@ -137,6 +145,7 @@ exprt string_constraint_generatort::add_axioms_for_concat( /// Add axioms enforcing that the string represented by the two first /// expressions is equal to the concatenation of the string argument and /// the character argument of the function application. +/// \todo This should be merged with add_axioms_for_concat. /// \param f: function application with a length, pointer, string and character /// argument. /// \return code 0 on success @@ -152,6 +161,7 @@ exprt string_constraint_generatort::add_axioms_for_concat_char( } /// Add axioms corresponding to the StringBuilder.appendCodePoint(I) function +/// \deprecated java specific /// \param f: function application with two arguments: a string and a code point /// \return an expression exprt string_constraint_generatort::add_axioms_for_concat_code_point( diff --git a/src/solvers/refinement/string_constraint_generator_constants.cpp b/src/solvers/refinement/string_constraint_generator_constants.cpp index 18fbb876e4e..d5d6d4eeb0c 100644 --- a/src/solvers/refinement/string_constraint_generator_constants.cpp +++ b/src/solvers/refinement/string_constraint_generator_constants.cpp @@ -15,8 +15,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include -/// add axioms saying the returned string expression should be equal to the -/// string constant +/// Add axioms ensuring that the provided string expression and constant are +/// equal. /// \param res: array of characters for the result /// \param sval: a string constant /// \return integer expression equal to zero @@ -29,8 +29,8 @@ exprt string_constraint_generatort::add_axioms_for_constant( std::string c_str=id2string(sval); std::wstring str; - // TODO: we should have a special treatment for java strings when the - // conversion function is available: +/// \todo We should have a special treatment for java strings when the +/// conversion function is available: #if 0 if(mode==ID_java) str=utf8_to_utf16_little_endian(c_str); @@ -52,7 +52,7 @@ exprt string_constraint_generatort::add_axioms_for_constant( return from_integer(0, get_return_code_type()); } -/// add axioms to say that the returned string expression is empty +/// Add axioms to say that the returned string expression is empty /// \param f: function application with arguments integer `length` and character /// pointer `ptr`. /// \return integer expression equal to zero @@ -65,8 +65,11 @@ exprt string_constraint_generatort::add_axioms_for_empty_string( return from_integer(0, get_return_code_type()); } -/// add axioms to say that the returned string expression is equal to the string -/// literal +/// String corresponding to an internal cprover string +/// +/// Add axioms ensuring that the returned string expression is equal to the +/// string literal. +/// \todo The name of the function should be changed to reflect what it does. /// \param f: function application with an argument which is a string literal /// that is a constant with a string value. /// \return string expression diff --git a/src/solvers/refinement/string_constraint_generator_float.cpp b/src/solvers/refinement/string_constraint_generator_float.cpp index 7bd3533c6fb..cd1518b5dd9 100644 --- a/src/solvers/refinement/string_constraint_generator_float.cpp +++ b/src/solvers/refinement/string_constraint_generator_float.cpp @@ -18,7 +18,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// Gets the unbiased exponent in a floating-point bit-vector /// -/// TODO: factorize with float_bv.cpp float_utils.h +/// \todo Refactor with float_bv.cpp float_utils.h /// \param src: a floating point expression /// \param spec: specification for floating points /// \return A new 32 bit integer expression representing the exponent. @@ -147,6 +147,8 @@ exprt estimate_decimal_exponent(const exprt &f, const ieee_float_spect &spec) return round_expr_to_zero(adjust_for_neg); } +/// String representation of a float value +/// /// Add axioms corresponding to the String.valueOf(F) java function /// \param f: function application with one float argument /// \return an integer expression @@ -174,8 +176,8 @@ exprt string_constraint_generatort::add_axioms_from_double( /// This specification is correct for inputs that do not exceed 100000 and the /// function is unspecified for other values. /// -/// \todo: this specification is not correct for negative numbers and -/// double precision +/// \todo This specification is not correct for negative numbers and +/// double precision. /// \param res: string expression corresponding to the result /// \param f: expression representing a float /// \return an integer expression, different from zero if an error should be @@ -306,7 +308,7 @@ exprt string_constraint_generatort::add_axioms_for_fractional_part( /// Then \f$n\f$ can be expressed by the equation: /// \f$log_10(n) = log_10(m) + log_10(2) * e - d\f$ /// \f$n = f / 10^d = m * 2^e / 10^d = m * 2^e / 10^(floor(log_10(2) * e))\f$ -/// TODO: For now we only consider single precision. +/// \todo For now we only consider single precision. /// \param res: string expression representing the float in scientific notation /// \param f: a float expression, which is positive /// \return a integer expression different from 0 to signal an exception @@ -471,6 +473,8 @@ exprt string_constraint_generatort::add_axioms_from_float_scientific_notation( return add_axioms_for_concat(res, string_expr_with_E, exponent_string); } +/// Representation of a float value in scientific notation +/// /// Add axioms corresponding to the scientific representation of floating point /// values /// \param f: a function application expression diff --git a/src/solvers/refinement/string_constraint_generator_format.cpp b/src/solvers/refinement/string_constraint_generator_format.cpp index 85f738182af..7a5902f7e70 100644 --- a/src/solvers/refinement/string_constraint_generator_format.cpp +++ b/src/solvers/refinement/string_constraint_generator_format.cpp @@ -320,13 +320,13 @@ string_constraint_generatort::add_axioms_for_format_specifier( return res; } case format_specifiert::OCTAL_INTEGER: - // TODO: conversion of octal not implemented + /// \todo Conversion of octal is not implemented. case format_specifiert::GENERAL: - // TODO: general not implemented + /// \todo Conversion for format specifier general is not implemented. case format_specifiert::HEXADECIMAL_FLOAT: - // TODO: hexadecimal float not implemented + /// \todo Conversion of hexadecimal float is not implemented. case format_specifiert::DATE_TIME: - // TODO: DateTime not implemented + /// \todo Conversion of date-time is not implemented // For all these unimplemented cases we return a non-deterministic string message.warning() << "unimplemented format specifier: " << fs.conversion << message.eom; @@ -433,9 +433,10 @@ std::string utf16_constant_array_to_java( return utf16_little_endian_to_java(out); } -/// Add axioms to specify the Java String.format function. +/// Formatted string using a format string and list of arguments /// -/// TODO: This is correct only if the first argument (ie the format string) is +/// Add axioms to specify the Java String.format function. +/// \todo This is correct only if the first argument (ie the format string) is /// constant or does not contain format specifiers. /// \param f: a function application /// \return A string expression representing the return value of the diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp index a0cea95abdd..edf532751d1 100644 --- a/src/solvers/refinement/string_constraint_generator_indexof.cpp +++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp @@ -14,13 +14,26 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include -/// Add axioms stating that the returned value is the index within str of the -/// first occurrence of c starting the search at from_index, or -1 if no such -/// character occurs at or after position from_index. -/// \param str: a string expression -/// \param c: an expression representing a character -/// \param from_index: an expression representing an index in the string -/// \return a integer expression +/// Add axioms stating that the returned value is the index within `haystack` +/// (`str`) of the first occurrence of `needle` (`c`) starting the search at +/// `from_index`, or is `-1` if no such character occurs at or after position +/// `from_index`. +/// \todo Make argument names match whose of add_axioms_for_index_of_string +/// +/// These axioms are: +/// 1. \f$-1 \le {\tt index} < |{\tt haystack}| \f$ +/// 2. \f$ \lnot contains \Leftrightarrow {\tt index} = -1 \f$ +/// 3. \f$ contains \Rightarrow {\tt from\_index} \le {\tt index} +/// \land {\tt haystack}[{\tt index}] = {\tt needle} \f$ +/// 4. \f$ \forall i \in [{\tt from\_index}, {\tt index}).\ contains +/// \Rightarrow {\tt haystack}[i] \ne {\tt needle} \f$ +/// 5. \f$ \forall m, n \in [{\tt from\_index}, |{\tt haystack}|) +/// .\ \lnot contains \Rightarrow {\tt haystack}[m] \ne {\tt needle} +/// \f$ +/// \param str: an array of characters expression +/// \param c: a character expression +/// \param from_index: an integer expression +/// \return integer expression `index` exprt string_constraint_generatort::add_axioms_for_index_of( const array_string_exprt &str, const exprt &c, @@ -30,13 +43,6 @@ exprt string_constraint_generatort::add_axioms_for_index_of( symbol_exprt index=fresh_exist_index("index_of", index_type); symbol_exprt contains=fresh_boolean("contains_in_index_of"); - // We add axioms: - // a1 : -1 <= index < |str| - // a2 : !contains <=> index=-1 - // a3 : contains ==> from_index <= index && str[index] = c - // a4 : forall n, n:[from_index,index[. contains ==> str[n] != c - // a5 : forall m, n:[from_index,|str|[. !contains ==> str[m] != c - exprt minus1=from_integer(-1, index_type); and_exprt a1( binary_relation_exprt(index, ID_ge, minus1), @@ -70,14 +76,28 @@ exprt string_constraint_generatort::add_axioms_for_index_of( return index; } -/// Add axioms stating that the returned value is the index within haystack of -/// the first occurrence of needle starting the search at from_index, or -1 if -/// needle does not occur at or after position from_index. -/// \param haystack: a string expression -/// \param needle: a string expression -/// \param from_index: an expression representing an index in strings -/// \return an integer expression representing the first index of needle in -/// haystack after from_index, or -1 if there is none +/// Add axioms stating that the returned value `index` is the index within +/// `haystack` of the first occurrence of `needle` starting the search at +/// `from_index`, or `-1` if needle does not occur at or after position +/// `from_index`. +/// +/// These axioms are: +/// 1. \f$ contains \Rightarrow {\tt from\_index} \le \tt{index} +/// \le |{\tt haystack}|-|{\tt needle} | \f$ +/// 2. \f$ \lnot contains \Leftrightarrow {\tt index} = -1 \f$ +/// 3. \f$ \forall n \in [0,|{\tt needle}|).\ contains +/// \Rightarrow {\tt haystack}[n + {\tt index}] = {\tt needle}[n] \f$ +/// 4. \f$ \forall n \in [{\tt from\_index}, {\tt index}).\ contains +/// \Rightarrow (\exists m \in [0,|{\tt needle}|).\ {\tt haystack}[m+n] +/// \ne {\tt needle}[m]]) \f$ +/// 5. \f$ \forall n \in [{\tt from\_index},|{\tt haystack}|-|{\tt needle}|] +/// .\ \lnot contains \Rightarrow (\exists m \in [0,|{\tt needle}|) +/// .\ {\tt haystack}[m+n] \ne {\tt needle}[m]) \f$ +/// \param haystack: an array of character expression +/// \param needle: an array of character expression +/// \param from_index: an integer expression +/// \return integer expression `index` representing the first index of `needle` +/// in `haystack` exprt string_constraint_generatort::add_axioms_for_index_of_string( const array_string_exprt &haystack, const array_string_exprt &needle, @@ -87,16 +107,6 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string( symbol_exprt offset=fresh_exist_index("index_of", index_type); symbol_exprt contains=fresh_boolean("contains_substring"); - // We add axioms: - // a1 : contains ==> from_index <= offset <= |haystack|-|needle| - // a2 : !contains <=> offset=-1 - // a3 : forall n:[0,|needle|[. - // contains ==> haystack[n+offset]=needle[n] - // a4 : forall n:[from_index,offset[. - // contains ==> (exists m:[0,|needle|[. haystack[m+n] != needle[m]]) - // a5: forall n:[from_index,|haystack|-|needle|]. - // !contains ==> (exists m:[0,|needle|[. haystack[m+n] != needle[m]) - implies_exprt a1( contains, and_exprt( @@ -149,11 +159,30 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string( /// the last occurrence of needle starting the search backward at from_index (ie /// the index is smaller or equal to from_index), or -1 if needle does not occur /// before from_index. -/// \param haystack: a string expression -/// \param needle: a string expression -/// \param from_index: an expression representing an index in strings -/// \return an integer expression representing the last index of needle in -/// haystack before or at from_index, or -1 if there is none +/// +/// These axioms are: +/// 1. \f$ contains \Rightarrow -1 \le {\tt index} +/// \land {\tt index} \le {\tt from\_index} +/// \land {\tt index} \le |{\tt haystack}| - |{\tt needle}| \f$ +/// 2. \f$ \lnot contains \Leftrightarrow {\tt index}= -1 \f$ +/// 3. \f$ \forall n \in [0, |{\tt needle}|).\ contains +/// \Rightarrow {\tt haystack}[n+{\tt index}] = {\tt needle}[n] \f$ +/// 4. \f$ \forall n \in [{\tt index}+1, +/// min({\tt from\_index}, +/// |{\tt haystack}| - |{\tt needle}|)] +/// .\ contains \Rightarrow +/// (\exists m \in [0,|{\tt needle}|) +/// .\ {\tt haystack}[m+n] \ne {\tt needle}[m]]) \f$ +/// 5. \f$ \forall n \in +/// [0, min({\tt from\_index}, |{\tt haystack}| - |{\tt needle}|)] +/// .\ \lnot contains \Rightarrow +/// (\exists m \in [0,|{\tt needle}|) +/// .\ {\tt haystack}[m+n] \ne {\tt needle}[m]) \f$ +/// \param haystack: an array of characters expression +/// \param needle: an array of characters expression +/// \param from_index: integer expression +/// \return integer expression `index` representing the last index of `needle` +/// in `haystack` before or at `from_index`, or -1 if there is none exprt string_constraint_generatort::add_axioms_for_last_index_of_string( const array_string_exprt &haystack, const array_string_exprt &needle, @@ -163,19 +192,6 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string( symbol_exprt offset=fresh_exist_index("index_of", index_type); symbol_exprt contains=fresh_boolean("contains_substring"); - // We add axioms: - // a1 : contains ==> -1 <= offset && offset <= from_index - // && offset <= |haystack| - |needle| - // a2 : !contains <=> offset = -1 - // a3 : forall n:[0, |needle|[, - // contains ==> haystack[n+offset] = needle[n] - // a4 : forall n:[offset+1, min(from_index, |haystack| - |needle|)]. - // contains ==> - // (exists m:[0,|needle|[. haystack[m+n] != needle[m]]) - // a5: forall n:[0, min(from_index, |haystack| - |needle|)]. - // !contains ==> - // (exists m:[0,|needle|[. haystack[m+n] != needle[m]) - implies_exprt a1( contains, and_exprt( @@ -225,10 +241,24 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string( return offset; } -/// add axioms corresponding to the String.indexOf:(C), String.indexOf:(CI), -/// String.indexOf:(String), and String.indexOf:(String,I) java functions -/// \par parameters: function application with 2 or 3 arguments -/// \return a integer expression +/// Index of the first occurence of a target inside the string +/// +/// If the target is a character: +// NOLINTNEXTLINE +/// \copybrief add_axioms_for_index_of(const array_string_exprt&,const exprt&,const exprt&) +/// \link +/// add_axioms_for_index_of(const array_string_exprt&,const exprt&,const exprt&) +/// (More...) \endlink +/// +/// If the target is a refined_string: +/// \copybrief string_constraint_generatort::add_axioms_for_index_of_string +/// \link string_constraint_generatort::add_axioms_for_index_of_string (More...) +/// \endlink +/// \warning slow for string targets +/// \param f: function application with arguments refined_string `haystack`, +/// refined_string or character `needle`, and optional integer +/// `from_index` with default value `0` +/// \return integer expression exprt string_constraint_generatort::add_axioms_for_index_of( const function_application_exprt &f) { @@ -258,14 +288,26 @@ exprt string_constraint_generatort::add_axioms_for_index_of( } } -/// Add axioms stating that the returned value is the index within str of the -/// last occurrence of c starting the search backward at from_index, or -1 if no -/// such character occurs at or before position from_index. -/// \param str: a string expression -/// \param c: an expression representing a character -/// \param from_index: an expression representing an index in the string -/// \return an integer expression representing the last index of c in str before -/// or at from_index, or -1 if there is none +/// Add axioms stating that the returned value is the index within `haystack` +/// (`str`) of the last occurrence of `needle` (`c`) starting the search +/// backward at `from_index`, or `-1` if no such character occurs at or before +/// position `from_index`. +/// \todo Change argument names to match add_axioms_for_last_index_of_string +/// +/// These axioms are : +/// 1. \f$ -1 \le {\tt index} \le {\tt from\_index} \f$ +/// 2. \f$ {\tt index} = -1 \Leftrightarrow \lnot contains\f$ +/// 3. \f$ contains \Rightarrow ({\tt index} \le {\tt from\_index} \land +/// {\tt haystack}[i] = {\tt needle} )\f$ +/// 4. \f$ \forall n \in [{\tt index} +1, {\tt from\_index}+1) +/// .\ contains \Rightarrow {\tt haystack}[n] \ne {\tt needle} \f$ +/// 5. \f$ \forall m \in [0, {\tt from\_index}+1) +/// .\ \lnot contains \Rightarrow {\tt haystack}[m] \ne {\tt needle}\f$ +/// \param str: an array of characters expression +/// \param c: a character expression +/// \param from_index: an integer expression +/// \return integer expression `index` representing the last index of `needle` +/// in `haystack` before or at `from_index`, or `-1` if there is none exprt string_constraint_generatort::add_axioms_for_last_index_of( const array_string_exprt &str, const exprt &c, @@ -275,13 +317,6 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of( symbol_exprt index=fresh_exist_index("last_index_of", index_type); symbol_exprt contains=fresh_boolean("contains_in_last_index_of"); - // We add axioms: - // a1 : -1 <= i <= from_index - // a2 : i = -1 <=> !contains - // a3 : contains ==> (i <= from_index && s[i] = c) - // a4 : forall n:[i+1, from_index+1[ && contains ==> s[n] != c - // a5 : forall m:[0, from_index+1[ && !contains ==> s[m] != c - exprt index1=from_integer(1, index_type); exprt minus1=from_integer(-1, index_type); exprt from_index_plus_one=plus_exprt_with_overflow_check(from_index, index1); @@ -320,11 +355,24 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of( return index; } -/// add axioms corresponding to the String.lastIndexOf:(C), -/// String.lastIndexOf:(CI), String.lastIndexOf:(String), and -/// String.lastIndexOf:(String,I) java functions -/// \par parameters: function application with 2 or 3 arguments -/// \return a integer expression +/// Index of the last occurence of a target inside the string +/// +/// If the target is a character: +// NOLINTNEXTLINE +/// \copybrief add_axioms_for_last_index_of(const array_string_exprt&,const exprt&,const exprt&) +// NOLINTNEXTLINE +/// \link add_axioms_for_last_index_of(const array_string_exprt&,const exprt&,const exprt&) +/// (More...) \endlink +/// +/// If the target is a refined_string: +/// \copybrief string_constraint_generatort::add_axioms_for_last_index_of_string +/// \link string_constraint_generatort::add_axioms_for_last_index_of_string +/// (More...) \endlink +/// \warning slow for string targets +/// \param f: function application with arguments refined_string `haystack`, +/// refined_string or character `needle`, and optional integer +/// `from_index` with default value `|haystack|-1` +/// \return an integer expression exprt string_constraint_generatort::add_axioms_for_last_index_of( const function_application_exprt &f) { diff --git a/src/solvers/refinement/string_constraint_generator_insert.cpp b/src/solvers/refinement/string_constraint_generator_insert.cpp index e0fa0db911e..c5c975ffbff 100644 --- a/src/solvers/refinement/string_constraint_generator_insert.cpp +++ b/src/solvers/refinement/string_constraint_generator_insert.cpp @@ -12,11 +12,16 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include -/// add axioms stating that the result correspond to the first string where we -/// inserted the second one at position offset -/// \par parameters: two string expression and an integer offset -/// \return an expression whose value would be different from zero if there is -/// an exception to signal +/// Add axioms ensuring the result `res` corresponds to `s1` where we +/// inserted `s2` at position `offset`. +/// This is equivalent to +/// `res=concat(substring(s1, 0, offset), concat(s2, substring(s1, offset)))`. +/// \param res: array of characters expression +/// \param s1: array of characters expression +/// \param s2: array of characters expression +/// \param offset: integer expression +/// \return an expression expression which is different from zero if there is +/// an exception to signal exprt string_constraint_generatort::add_axioms_for_insert( const array_string_exprt &res, const array_string_exprt &s1, @@ -46,12 +51,23 @@ exprt string_constraint_generatort::add_axioms_for_insert( return_code1); } -/// add axioms corresponding to the StringBuilder.insert(int, CharSequence) and -/// StringBuilder.insert(int, CharSequence, int, int) java functions -/// \param f: function application with arguments integer `|res|`, char pointer -/// `&res[0]`, refined string `s1`, refined string `s2`, -/// integer `offset` -/// \return a new string expression +/// Insertion of a string in another at a specific index +/// +/// \copybrief string_constraint_generatort::add_axioms_for_insert( +/// const array_string_exprt &, const array_string_exprt &, +/// const array_string_exprt &, const exprt &) +// NOLINTNEXTLINE +/// \link add_axioms_for_insert(const array_string_exprt&,const array_string_exprt&,const array_string_exprt&,const exprt&) +/// (More...) \endlink +/// +/// If `start` and `end` arguments are given then `substring(s2, start, end)` +/// is considered instead of `s2`. +/// \param f: function application with arguments integer `|res|`, character +/// pointer `&res[0]`, refined_string `s1`, refined_string`s2`, +/// integer `offset`, optional integer `start` and optional integer +/// `end` +/// \return an integer expression which is different from zero if there is +/// an exception to signal exprt string_constraint_generatort::add_axioms_for_insert( const function_application_exprt &f) { @@ -80,7 +96,9 @@ exprt string_constraint_generatort::add_axioms_for_insert( return add_axioms_for_insert(res, s1, s2, offset); } } + /// add axioms corresponding to the StringBuilder.insert(I) java function +/// \deprecated /// \param f: function application with three arguments: a string, an /// integer offset, and an integer /// \return an expression @@ -100,6 +118,7 @@ exprt string_constraint_generatort::add_axioms_for_insert_int( } /// add axioms corresponding to the StringBuilder.insert(Z) java function +/// \deprecated should convert the value to string and call insert /// \param f: function application with three arguments: a string, an /// integer offset, and a Boolean /// \return a new string expression @@ -118,7 +137,8 @@ exprt string_constraint_generatort::add_axioms_for_insert_bool( return add_axioms_for_insert(res, s1, s2, offset); } -/// add axioms corresponding to the StringBuilder.insert(C) java function +/// Add axioms corresponding to the StringBuilder.insert(C) java function +/// \todo This should be merged with add_axioms_for_insert. /// \param f: function application with three arguments: a string, an /// integer offset, and a character /// \return an expression @@ -138,6 +158,7 @@ exprt string_constraint_generatort::add_axioms_for_insert_char( } /// add axioms corresponding to the StringBuilder.insert(D) java function +/// \deprecated should convert the value to string and call insert /// \param f: function application with three arguments: a string, an /// integer offset, and a double /// \return a string expression @@ -157,7 +178,8 @@ exprt string_constraint_generatort::add_axioms_for_insert_double( return add_axioms_for_insert(res, s1, s2, offset); } -/// add axioms corresponding to the StringBuilder.insert(F) java function +/// Add axioms corresponding to the StringBuilder.insert(F) java function +/// \deprecated should convert the value to string and call insert /// \param f: function application with three arguments: a string, an /// integer offset, and a float /// \return a new string expression diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index d7ff6d98c86..6d889be9412 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -222,7 +222,7 @@ string_constraint_generatort::associate_char_array_to_char_pointer( char_pointer.id() == ID_constant && to_constant_expr(char_pointer).get_value() == ID_NULL) { - // TODO: is this useful? + /// \todo Check if the case char_array_null occurs. array_typet array_type( char_array_type.subtype(), from_integer(0, to_array_type(char_array_type).size().type())); @@ -269,9 +269,9 @@ exprt string_constraint_generatort::associate_array_to_pointer( array_expr.length() = pair.first->second; } - // TODO should use a function for that + /// \todo We should use a function for inserting the correspondance + /// between array and pointers. arrays_of_pointers_.insert(std::make_pair(pointer_expr, array_expr)); - // TODO should go inside function add_default_axioms(to_array_string_expr(array_expr)); return from_integer(0, f.type()); } @@ -337,7 +337,7 @@ void string_constraint_generatort::add_default_axioms( } /// Adds creates a new array if it does not already exists -/// TODO: This should be replaced by associate_char_array_to_char_pointer +/// \todo This should be replaced by associate_char_array_to_char_pointer array_string_exprt string_constraint_generatort::char_array_of_pointer( const exprt &pointer, const exprt &length) @@ -484,7 +484,8 @@ exprt string_constraint_generatort::add_axioms_for_function_application( /// add axioms to say that the returned string expression is equal to the /// argument of the function application -/// \par parameters: function application with one argument, which is a string, +/// \deprecated should use substring instead +/// \param f: function application with one argument, which is a string, /// or three arguments: string, integer offset and count /// \return a new string expression exprt string_constraint_generatort::add_axioms_for_copy( @@ -500,10 +501,11 @@ exprt string_constraint_generatort::add_axioms_for_copy( return add_axioms_for_substring(res, str, offset, plus_exprt(offset, count)); } - -/// add axioms corresponding to the String.length java function -/// \par parameters: function application with one string argument -/// \return a string expression of index type +/// Length of a string +/// +/// Returns the length of the string argument of the given function application +/// \param f: function application with argument string `str` +/// \return expression `|str|` exprt string_constraint_generatort::add_axioms_for_length( const function_application_exprt &f) { @@ -513,7 +515,7 @@ exprt string_constraint_generatort::add_axioms_for_length( } /// expression true exactly when the index is positive -/// \par parameters: an index expression +/// \param x: an index expression /// \return a Boolean expression exprt string_constraint_generatort::axiom_for_is_positive_index(const exprt &x) { @@ -521,7 +523,7 @@ exprt string_constraint_generatort::axiom_for_is_positive_index(const exprt &x) } /// add axioms stating that the returned value is equal to the argument -/// \par parameters: function application with one character argument +/// \param f: function application with one character argument /// \return a new character expression exprt string_constraint_generatort::add_axioms_for_char_literal( const function_application_exprt &f) @@ -551,11 +553,13 @@ exprt string_constraint_generatort::add_axioms_for_char_literal( } } -/// add axioms stating that the character of the string at the given position is -/// equal to the returned value -/// \par parameters: function application with two arguments: a string and an -/// integer -/// \return a character expression +/// Character at a given position +/// +/// Add axioms stating that the character of the string at position given by +/// second argument is equal to the returned value. +/// This axiom is \f$ char = str[i] \f$. +/// \param f: function application with arguments string `str` and integer `i` +/// \return character expression `char` exprt string_constraint_generatort::add_axioms_for_char_at( const function_application_exprt &f) { diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/refinement/string_constraint_generator_testing.cpp index 2c6b68fdc0b..3186451e32e 100644 --- a/src/solvers/refinement/string_constraint_generator_testing.cpp +++ b/src/solvers/refinement/string_constraint_generator_testing.cpp @@ -13,10 +13,21 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include -/// add axioms stating that the returned expression is true exactly when the -/// first string is a prefix of the second one, starting at position offset -/// \par parameters: a prefix string, a string and an integer offset -/// \return a Boolean expression +/// Add axioms stating that the returned expression is true exactly when the +/// first string is a prefix of the second one, starting at position offset. +/// +/// These axioms are: +/// 1. \f$ {\tt isprefix} \Rightarrow |str| \ge |{\tt prefix}|+offset \f$ +/// 2. \f$ \forall 0 \le qvar<|{\tt prefix}|.\ {\tt isprefix} +/// \Rightarrow s0[witness+{\tt offset}]=s2[witness] \f$ +/// 3. \f$ !{\tt isprefix} \Rightarrow |{\tt str}|<|{\tt prefix}|+{\tt offset} +/// \lor (0 \le witness<|{\tt prefix}| +/// \land {\tt str}[witness+{\tt offset}] \ne {\tt prefix}[witness])\f$ +/// +/// \param prefix: an array of characters +/// \param str: an array of characters +/// \param offset: an integer +/// \return Boolean expression `isprefix` exprt string_constraint_generatort::add_axioms_for_is_prefix( const array_string_exprt &prefix, const array_string_exprt &str, @@ -25,13 +36,6 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix( symbol_exprt isprefix=fresh_boolean("isprefix"); const typet &index_type=str.length().type(); - // We add axioms: - // a1 : isprefix => |str| >= |prefix|+offset - // a2 : forall 0<=qvar<|prefix|. isprefix => s0[witness+offset]=s2[witness] - // a3 : !isprefix => - // |str|<|prefix|+offset || - // (0<=witness<|prefix| && str[witness+offset]!=prefix[witness]) - implies_exprt a1( isprefix, str.axiom_for_length_ge(plus_exprt_with_overflow_check( @@ -61,12 +65,21 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix( return isprefix; } -/// add axioms corresponding to the String.isPrefix java function -/// \par parameters: a function application with 2 or 3 arguments and a Boolean -/// telling -/// whether the prefix is the second argument (when swap_arguments is -/// true) or the first argument -/// \return a Boolean expression +/// Test if the target is a prefix of the string +/// +/// Add axioms ensuring the return value is true when the string starts with the +/// given target. +/// These axioms are detailed here: +// NOLINTNEXTLINE +/// string_constraint_generatort::add_axioms_for_is_prefix(const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset) +/// \todo The primitive should be renamed to `starts_with`. +/// \todo Get rid of the boolean flag. +/// \param f: a function application with arguments refined_string `s0`, +/// refined string `s1` and optional integer argument `offset` +/// whose default value is 0 +/// \param swap_arguments: a Boolean telling whether the prefix is the second +/// argument or the first argument +/// \return boolean expression `isprefix` exprt string_constraint_generatort::add_axioms_for_is_prefix( const function_application_exprt &f, bool swap_arguments) { @@ -80,9 +93,10 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix( return typecast_exprt(add_axioms_for_is_prefix(s0, s1, offset), f.type()); } -/// add axioms stating that the returned value is true exactly when the argument -/// string is empty -/// \par parameters: function application with a string argument +/// Add axioms stating that the returned value is true exactly when the argument +/// string is empty. +/// \deprecated should use `string_length(s)==0` instead +/// \param f: function application with a string argument /// \return a Boolean expression exprt string_constraint_generatort::add_axioms_for_is_empty( const function_application_exprt &f) @@ -100,12 +114,26 @@ exprt string_constraint_generatort::add_axioms_for_is_empty( return typecast_exprt(is_empty, f.type()); } -/// add axioms corresponding to the String.isSuffix java function -/// \par parameters: a function application with 2 or 3 arguments and a Boolean -/// telling -/// whether the suffix is the second argument (when swap_arguments is -/// true) or the first argument -/// \return a Boolean expression +/// Test if the target is a suffix of the string +/// +/// Add axioms ensuring the return value is true when the first string ends with +/// the given target. +/// These axioms are: +/// 1. \f$ \texttt{issuffix} \Rightarrow |s_0| \ge |s_1| \f$ +/// 2. \f$ \forall i <|s_1|.\ {\tt issuffix} +/// \Rightarrow s_1[i] = s_0[i + |s_0| - |s_1|] +/// \f$ +/// 3. \f$ \lnot {\tt issuffix} \Rightarrow +/// (|s_1| > |s_0| \land {\tt witness}=-1) +/// \lor (|s_1| > {witness} \ge 0 +/// \land s_1[{witness}] \ne s_0[{witness} + |s_0| - |s_1|] \f$ +/// +/// \todo The primitive should be renamed `ends_with`. +/// \param f: a function application with arguments refined_string `s0` +/// and refined_string `s1` +/// \param swap_arguments: boolean flag telling whether the suffix is the second +/// argument or the first argument +/// \return Boolean expression `issuffix` exprt string_constraint_generatort::add_axioms_for_is_suffix( const function_application_exprt &f, bool swap_arguments) { @@ -119,15 +147,6 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix( const array_string_exprt &s1 = get_string_expr(args[swap_arguments ? 0 : 1]); const typet &index_type=s0.length().type(); - // We add axioms: - // a1 : issufix => s0.length >= s1.length - // a2 : forall witness s1[witness]=s0[witness + s0.length-s1.length] - // a3 : !issuffix => - // (s1.length > s0.length && witness=-1) - // || (s1.length > witness>=0 - // &&s1[witness]!=s0[witness + s0.length-s1.length] - implies_exprt a1(issuffix, s1.axiom_for_length_ge(s0.length())); axioms.push_back(a1); @@ -156,9 +175,24 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix( return tc_issuffix; } -/// add axioms corresponding to the String.contains java function -/// \par parameters: function application with two string arguments -/// \return a Boolean expression +/// Test whether a string contains another +/// +/// Add axioms ensuring the returned value is true when the first string +/// contains the second. +/// These axioms are: +/// 1. \f$ contains \Rightarrow |s_0| \ge |s_1| \f$ +/// 2. \f$ contains \Rightarrow 0 \le startpos \le |s_0|-|s_1| \f$ +/// 3. \f$ !contains \Rightarrow startpos = -1 \f$ +/// 4. \f$ \forall qvar < |s_1|.\ contains +/// \Rightarrow s_1[qvar] = s_0[startpos + qvar] \f$ +/// 5. \f$ \forall startpos \le |s_0|-|s_1|. +/// \ (!contains \land |s_0| \ge |s_1|) +/// \Rightarrow \exists witness < |s_1|. +/// \ s_1[witness] \ne s_0[startpos+witness] \f$ +/// \warning slow for target longer than one character +/// \param f: function application with arguments refined_string `s0` +/// refined_string `s1` +/// \return Boolean expression `contains` exprt string_constraint_generatort::add_axioms_for_contains( const function_application_exprt &f) { @@ -171,15 +205,6 @@ exprt string_constraint_generatort::add_axioms_for_contains( const symbol_exprt startpos = fresh_exist_index("startpos_contains", index_type); - // We add axioms: - // a1 : contains ==> |s0| >= |s1| - // a2 : contains ==> 0 <= startpos <= |s0|-|s1| - // a3 : !contains ==> startpos = -1 - // a4 : forall qvar < |s1|. contains ==> s1[qvar] = s0[startpos + qvar] - // a5 : !contains ==> |s1| > |s0| || - // (forall startpos <= |s0| - |s1|. - // exists witness < |s1|. s1[witness] != s0[witness + startpos]) - const implies_exprt a1(contains, s0.axiom_for_length_ge(s1.length())); axioms.push_back(a1); @@ -201,9 +226,6 @@ exprt string_constraint_generatort::add_axioms_for_contains( qvar, s1.length(), contains, equal_exprt(s1[qvar], s0[qvar_shifted])); axioms.push_back(a4); - // We rewrite axiom a4 as: - // forall startpos <= |s0|-|s1|. (!contains && |s0| >= |s1|) - // ==> exists witness < |s1|. s1[witness] != s0[startpos+witness] string_not_contains_constraintt a5( from_integer(0, index_type), plus_exprt(from_integer(1, index_type), length_diff), diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp index 0f6d5f624a1..355cd29598d 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp @@ -15,14 +15,23 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include "expr_cast.h" -/// add axioms to say that the returned string expression `res` has length `k` +/// Reduce or extend a string to have the given length +/// +/// Add axioms ensuring the returned string expression `res` has length `k` /// and characters at position `i` in `res` are equal to the character at /// position `i` in `s1` if `i` is smaller that the length of `s1`, otherwise /// it is the null character `\u0000`. -/// \param f: function application with two arguments, the first of which -/// is a string `s1` and the second an integer `k` which should have -/// same type as the string length -/// \return a new string expression `res` +/// +/// These axioms are: +/// 1. \f$ |{\tt res}|={\tt k} \f$ +/// 2. \f$ \forall i<|{\tt res}|.\ i < |s_1| +/// \Rightarrow {\tt res}[i] = s_1[i] \f$ +/// 3. \f$ \forall i<|{\tt res}|.\ i \ge |s_1| +/// \Rightarrow {\tt res}[i] = 0 \f$ +/// \todo We can reduce the number of constraints by merging 2 and 3. +/// \param f: function application with arguments integer `|res|`, character +/// pointer `&res[0]`, refined_string `s1`, integer `k` +/// \return integer expressino equal to `0` exprt string_constraint_generatort::add_axioms_for_set_length( const function_application_exprt &f) { @@ -60,13 +69,25 @@ exprt string_constraint_generatort::add_axioms_for_set_length( return from_integer(0, signedbv_typet(32)); } -/// add axioms corresponding to the String.substring java function Warning: the -/// specification may not be correct for the case where the string is shorter -/// than the end index -/// \par parameters: function application with one string argument, one start -/// index -/// argument and an optional end index argument -/// \return a new string expression +/// Substring of a string between two indices +/// +/// \copybrief string_constraint_generatort::add_axioms_for_substring( +/// const array_string_exprt &res, +/// const array_string_exprt &str, +/// const exprt &start, +/// const exprt &end) +// NOLINTNEXTLINE +/// \link string_constraint_generatort::add_axioms_for_substring(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end) +/// (More...) \endlink +/// \warning The specification may not be correct for the case where the string +/// is shorter than the end index +/// \todo Should return a integer different from zero when the string is shorter +/// tan the end index. +/// \param f: function application with arguments integer `|res|`, character +/// pointer `&res[0]`, refined_string `str`, integer `start`, +/// optional integer `end` with default value `|str|`. +/// \return integer expression which is different from 0 when there is an +/// exception to signal exprt string_constraint_generatort::add_axioms_for_substring( const function_application_exprt &f) { @@ -79,12 +100,22 @@ exprt string_constraint_generatort::add_axioms_for_substring( return add_axioms_for_substring(res, str, i, j); } -/// add axioms stating that the returned string expression is equal to the input -/// one starting at `start` and ending before `end` -/// \par parameters: a string expression, an expression for the start index, and -/// an -/// expression for the end index -/// \return a new string expression +/// Add axioms ensuring that `res` corresponds to the substring of `str` +/// between indexes `start` and `end`. +/// +/// These axioms are: +/// 1. \f$ {\tt start} < {\tt end} \Rightarrow +/// |{\tt res}| = {\tt end} - {\tt start} \f$ +/// 2. \f$ {\tt start} \ge {\tt end} \Rightarrow |{\tt res}| = 0 \f$ +/// 3. \f$ |{\tt str}| > {\tt end} \f$ +/// 4. \f$ \forall i<|{\tt str}|.\ {\tt res}[i]={\tt str}[{\tt start}+i] \f$ +/// \todo Should return code different from 0 if `|str| <= |end|` instead of +/// adding constraint 3. +/// \param res: array of characters expression +/// \param str: array of characters expression +/// \param start: integer expression +/// \param end: integer expression +/// \return integer expression equal to zero exprt string_constraint_generatort::add_axioms_for_substring( const array_string_exprt &res, const array_string_exprt &str, @@ -96,10 +127,6 @@ exprt string_constraint_generatort::add_axioms_for_substring( PRECONDITION(end.type()==index_type); // We add axioms: - // a1 : start < end => |res| = end - start - // a2 : start >= end => |res| = 0 - // a3 : |str| > end - // a4 : forall idx{\tt \lq~\rq} \land s[m+|{\tt res}|-1]>{\tt \lq~\rq}) +/// \lor m=|{\tt res}| \f$ +/// \note Some of the constraints among 1, 2, 3, 4 and 5 seems to be redundant +/// \param f: function application with arguments integer `|res|`, character +/// pointer `&res[0]`, refined_string `str`. +/// \return integer expression which is different from 0 when there is an +/// exception to signal exprt string_constraint_generatort::add_axioms_for_trim( const function_application_exprt &f) { @@ -137,18 +187,6 @@ exprt string_constraint_generatort::add_axioms_for_trim( const symbol_exprt idx = fresh_exist_index("index_trim", index_type); const exprt space_char = from_integer(' ', char_type); - // We add axioms: - // a1 : m + |s1| <= |str| - // a2 : idx >= 0 - // a3 : str >= idx - // a4 : |res|>= 0 - // a5 : |res|<=|str| - // (this is necessary to prevent exceeding the biggest integer) - // a6 : forall n' ' &&s[m+|s1|-1]>' ') || m=|s| - exprt a1=str.axiom_for_length_ge( plus_exprt_with_overflow_check(idx, res.length())); axioms.push_back(a1); @@ -200,9 +238,22 @@ exprt string_constraint_generatort::add_axioms_for_trim( return from_integer(0, f.type()); } -/// add axioms corresponding to the String.toLowerCase java function -/// \par parameters: function application with one string argument -/// \return a new string expression +/// Conversion of a string to lower case +/// +/// Add axioms ensuring `res` corresponds to `str` in which uppercase characters +/// have been converted to lowercase. +/// These axioms are: +/// 1. \f$ |{\tt res}| = |{\tt str}| \f$ +/// 2. \f$ \forall i<|{\tt str}|.\ {\tt is\_upper\_case}({\tt str}[i])? +/// {\tt res}[i]={\tt str}[i]+diff : {\tt res}[i]={\tt str}[i] +/// \land {\tt str}[i]<{\tt 0x100} \f$ +/// where `diff` is the difference between lower case and upper case +/// characters: `diff = 'a'-'A' = 0x20`. +/// +/// \param f: function application with arguments integer `|res|`, character +/// pointer `&res[0]`, refined_string `str` +/// \return integer expression which is different from `0` when there is an +/// exception to signal exprt string_constraint_generatort::add_axioms_for_to_lower_case( const function_application_exprt &f) { @@ -217,18 +268,10 @@ exprt string_constraint_generatort::add_axioms_for_to_lower_case( const exprt char_A=constant_char('A', char_type); const exprt char_Z=constant_char('Z', char_type); - // TODO: for now, only characters in Basic Latin and Latin-1 supplement + // \todo for now, only characters in Basic Latin and Latin-1 supplement // are supported (up to 0x100), we should add others using case mapping // information from the UnicodeData file. - // We add axioms: - // a1 : |res| = |str| - // a2 : forall idx - // res[idx1]=str[idx1]+'A'-'a' - // a3 : forall idx2 res[idx2]=str[idx2] - // Note that index expressions are only allowed in the body of universal - // axioms, so we use a trivial premise and push our premise into the body. - equal_exprt a1(res.length(), str.length()); axioms.push_back(a1); @@ -316,9 +366,17 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case( return from_integer(0, signedbv_typet(32)); } -/// add axioms corresponding to the String.toUpperCase java function -/// \param f: function application with one string argument -/// \return a new string expression +/// Conversion of a string to upper case +/// +// NOLINTNEXTLINE +/// \copybrief string_constraint_generatort::add_axioms_for_to_upper_case(const array_string_exprt&, const array_string_exprt&) +// NOLINTNEXTLINE +/// \link string_constraint_generatort::add_axioms_for_to_upper_case(const array_string_exprt &res, const array_string_exprt &str) +/// (More...) \endlink +/// \param f: function application with arguments integer `|res|`, character +/// pointer `&res[0]`, refined_string `str` +/// \return integer expression which is different from `0` when there is an +/// exception to signal exprt string_constraint_generatort::add_axioms_for_to_upper_case( const function_application_exprt &f) { @@ -329,12 +387,20 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case( return add_axioms_for_to_upper_case(res, str); } -/// add axioms corresponding stating that the result is similar to that of the -/// StringBuilder.setCharAt java function Warning: this may be underspecified in -/// the case wher the index exceed the length of the string -/// \param f: function application with three arguments, the first is a -/// string, the second an index and the third a character -/// \return a new string expression +/// Set a character to a specific value at an index of the string +/// +/// Add axioms ensuring that the result `res` is similar to input string `str` +/// where the character at index `pos` is set to `char`. +/// These axioms are: +/// 1. \f$ |{\tt res}| = |{\tt str}|\f$ +/// 2. \f$ {\tt res}[{\tt pos}]={\tt char}\f$ +/// 3. \f$ \forall i<|{\tt res}|.\ i \ne {\tt pos} +/// \Rightarrow {\tt res}[i] = {\tt str}[i]\f$ +/// \param f: function application with arguments integer `|res|`, character +/// pointer `&res[0]`, refined_string `str`, integer `pos`, +/// and character `char` +/// \return an integer expression which is `1` when `pos` is out of bounds and +/// `0` otherwise exprt string_constraint_generatort::add_axioms_for_char_set( const function_application_exprt &f) { @@ -345,11 +411,6 @@ exprt string_constraint_generatort::add_axioms_for_char_set( const exprt &position = f.arguments()[3]; const exprt &character = f.arguments()[4]; - // We add axioms: - // a1 : |res| = |str| - // a2 : res[pos]=char - // a3 : forall i<|res|. i != pos => res[i] = str[i] - const binary_relation_exprt out_of_bounds(position, ID_ge, str.length()); axioms.push_back(equal_exprt(res.length(), str.length())); axioms.push_back(equal_exprt(res[position], character)); @@ -386,15 +447,25 @@ static optionalt> to_char_pair( return { }; } -/// Add axioms corresponding to the String.replace java function +/// Replace a character by another in a string +/// +/// Add axioms ensuring that `res` corresponds to `str` where occurences of +/// `old_char` have been replaced by `new_char`. +/// These axioms are: +/// 1. \f$ |{\tt res}| = |{\tt str}| \f$ +/// 2. \f$ \forall i \in 0, |{\tt res}|) +/// .\ {\tt str}[i]={\tt old\_char} +/// \Rightarrow {\tt res}[i]={\tt new\_char} +/// \land {\tt str}[i]\ne {\tt old\_char} +/// \Rightarrow {\tt res}[i]={\tt str}[i] \f$ /// Only supports String.replace(char, char) and /// String.replace(String, String) for single-character strings /// Returns original string in every other case (that behaviour is to /// be fixed in the future) -/// \param f function application with three arguments, the first is a -/// string, the second and the third are either pair of characters or -/// a pair of strings -/// \return a new string expression +/// \param f: function application with arguments integer `|res|`, character +/// pointer `&res[0]`, refined_string `str`, character `old_char` and +/// character `new_char` +/// \return an integer expression equal to 0 exprt string_constraint_generatort::add_axioms_for_replace( const function_application_exprt &f) { @@ -411,12 +482,6 @@ exprt string_constraint_generatort::add_axioms_for_replace( const auto old_char=maybe_chars->first; const auto new_char=maybe_chars->second; - // We add axioms: - // a1 : |res| = |str| - // a2 : forall qvar, 0<=qvar<|res|, - // str[qvar]=oldChar => res[qvar]=newChar - // !str[qvar]=oldChar => res[qvar]=str[qvar] - axioms.push_back(equal_exprt(res.length(), str.length())); symbol_exprt qvar = fresh_univ_index("QA_replace", str.length().type()); @@ -452,14 +517,20 @@ exprt string_constraint_generatort::add_axioms_for_delete_char_at( plus_exprt_with_overflow_check(f.arguments()[3], index_one)); } -/// add axioms stating that `res` corresponds to the input `str` -/// where we removed characters between the positions start (included) and end -/// (not included) -/// \param res: a string expression -/// \param str: a string expression -/// \param start: a start index -/// \param end: an end index -/// \return a expression different from zero to signal an exception +/// Add axioms stating that `res` corresponds to the input `str` +/// where we removed characters between the positions `start` (included) and +/// `end` (not included). +/// +/// These axioms are the same as would be generated for: +/// `concat(substring(str, 0, start), substring(end, |str|))` +/// (see \ref add_axioms_for_substring and \ref add_axioms_for_concat_substr). +/// \todo Should use add_axioms_for_concat_substr instead +/// of add_axioms_for_concat +/// \param res: array of characters expression +/// \param str: array of characters expression +/// \param start: integer expression +/// \param end: integer expression +/// \return integer expression different from zero to signal an exception exprt string_constraint_generatort::add_axioms_for_delete( const array_string_exprt &res, const array_string_exprt &str, @@ -480,9 +551,16 @@ exprt string_constraint_generatort::add_axioms_for_delete( return bitor_exprt(return_code1, bitor_exprt(return_code2, return_code3)); } -/// add axioms corresponding to the StringBuilder.delete java function -/// \param f: function application with three arguments: a string -/// expression, a start index and an end index +/// Remove a portion of a string +/// +// NOLINTNEXTLINE +/// \copybrief string_constraint_generatort::add_axioms_for_delete(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end) +// NOLINTNEXTLINE +/// \link string_constraint_generatort::add_axioms_for_delete(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end) +/// (More...) \endlink +/// \param f: function application with arguments integer `|res|`, character +/// pointer `&res[0]`, refined_string `str`, integer `start` +/// and integer `end` /// \return an integer expression whose value is different from 0 to signal /// an exception exprt string_constraint_generatort::add_axioms_for_delete( diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index dd1c80a7341..45c8799fca1 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -18,6 +18,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include +/// Convert an integer to a string +/// /// Add axioms corresponding to the String.valueOf(I) java function. /// \param f: function application with one integer argument /// \return a new string expression @@ -35,6 +37,7 @@ exprt string_constraint_generatort::add_axioms_from_int( } /// Add axioms corresponding to the String.valueOf(J) java function. +/// \deprecated should use add_axioms_from_int instead /// \param f: function application with one long argument /// \return a new string expression exprt string_constraint_generatort::add_axioms_from_long( @@ -51,6 +54,7 @@ exprt string_constraint_generatort::add_axioms_from_long( } /// Add axioms corresponding to the String.valueOf(Z) java function. +/// \deprecated this is specific to Java /// \param f: function application with a Boolean argument /// \return a new string expression exprt string_constraint_generatort::add_axioms_from_bool( @@ -64,6 +68,7 @@ exprt string_constraint_generatort::add_axioms_from_bool( /// Add axioms stating that the returned string equals "true" when the Boolean /// expression is true and "false" when it is false. +/// \deprecated This is language dependent /// \param res: string expression for the result /// \param b: Boolean expression /// \return code 0 on success @@ -191,6 +196,7 @@ exprt string_constraint_generatort::int_of_hex_char(const exprt &chr) /// Add axioms stating that the string `res` corresponds to the integer /// argument written in hexadecimal. +/// \deprecated use add_axioms_from_int which takes a radix argument instead /// \param res: string expression for the result /// \param i: an integer argument /// \return code 0 on success @@ -247,7 +253,7 @@ exprt string_constraint_generatort::add_axioms_from_int_hex( return from_integer(0, get_return_code_type()); } -/// add axioms corresponding to the Integer.toHexString(I) java function +/// Add axioms corresponding to the Integer.toHexString(I) java function /// \param f: function application with an integer argument /// \return code 0 on success exprt string_constraint_generatort::add_axioms_from_int_hex( @@ -259,8 +265,15 @@ exprt string_constraint_generatort::add_axioms_from_int_hex( return add_axioms_from_int_hex(res, f.arguments()[2]); } -/// Add axioms corresponding to the String.valueOf(C) java function. -/// \param f: function application one char argument +/// Conversion from char to string +/// +/// \copybrief string_constraint_generatort::add_axioms_from_char( +/// const array_string_exprt &res, const exprt &c) +// NOLINTNEXTLINE +/// \link string_constraint_generatort::add_axioms_from_char(const array_string_exprt &res, const exprt &c) +/// (More...) \endlink +/// \param f: function application with arguments integer `|res|`, character +/// pointer `&res[0]` and character `c` /// \return code 0 on success exprt string_constraint_generatort::add_axioms_from_char( const function_application_exprt &f) @@ -271,10 +284,12 @@ exprt string_constraint_generatort::add_axioms_from_char( return add_axioms_from_char(res, f.arguments()[2]); } -/// Add axioms stating that the returned string has length 1 and the character -/// it contains corresponds to the input expression. -/// \param res: string expression for the result -/// \param c: one expression of type char +/// Add axiom stating that string `res` has length 1 and the character +/// it contains equals `c`. +/// +/// This axiom is: \f$ |{\tt res}| = 1 \land {\tt res}[0] = {\tt c} \f$. +/// \param res: array of characters expression +/// \param c: character expression /// \return code 0 on success exprt string_constraint_generatort::add_axioms_from_char( const array_string_exprt &res, @@ -462,10 +477,13 @@ void string_constraint_generatort::add_axioms_for_characters_in_integer_string( } } -/// add axioms corresponding to the Integer.parseInt java function -/// \param f: a function application with either one string expression or one -/// string expression and an integer expression for the radix -/// \return an integer expression +/// Integer value represented by a string +/// +/// Add axioms ensuring the value of the returned integer corresponds +/// to the value represented by `str` +/// \param f: a function application with arguments refined_string `str` and +/// an optional integer for the radix +/// \return integer expression equal to the value represented by `str` exprt string_constraint_generatort::add_axioms_for_parse_int( const function_application_exprt &f) { @@ -476,8 +494,8 @@ exprt string_constraint_generatort::add_axioms_for_parse_int( const exprt radix=f.arguments().size()==1? static_cast(from_integer(10, type)): static_cast(typecast_exprt(f.arguments()[1], type)); - /// Most of the time we can evaluate radix as an integer. The value 0 is used - /// to indicate when we can't tell what the radix is. + // Most of the time we can evaluate radix as an integer. The value 0 is used + // to indicate when we can't tell what the radix is. const unsigned long radix_ul=to_integer_or_default(radix, 0); PRECONDITION((radix_ul>=2 && radix_ul<=36) || radix_ul==0); @@ -488,8 +506,9 @@ exprt string_constraint_generatort::add_axioms_for_parse_int( const std::size_t max_string_length=max_printed_string_length(type, radix_ul); - /// TODO: we should throw an exception when this does not hold: - /// Note that the only thing stopping us from taking longer strings with many + /// \todo We should throw an exception when constraints added in + /// add_axioms_for_correct_number_format do not hold. + /// \note the only thing stopping us from taking longer strings with many /// leading zeros is the axioms for correct number format add_axioms_for_correct_number_format( input_int, diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index e70ea613c5c..5b7ec9c4490 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -42,6 +42,22 @@ static optionalt find_counter_example( const exprt &axiom, const symbol_exprt &var); +/// Check axioms takes the model given by the underlying solver and answers +/// whether it satisfies the string constraints. +/// +/// For each string_constraint `a`: +/// * the negation of `a` is an existential formula `b`; +/// * we substituted symbols in `b` by their values found in `get`; +/// * arrays are concretized, meaning we attribute a value for characters that +/// are unknown to get, for details see concretize_arrays_in_expression; +/// * `b` is simplified and array accesses are replaced by expressions +/// without arrays; +/// * we give lemma `b` to a fresh solver; +/// * if no counter-example to `b` is found, this means the constraint `a` +/// is satisfied by the valuation given by get. +/// \return `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. static std::pair> check_axioms( const string_axiomst &axioms, string_constraint_generatort &generator, @@ -80,6 +96,16 @@ static void update_index_set( const namespacet &ns, const exprt &formula); +/// Substitute `qvar` the universally quantified variable of `axiom`, by +/// an index `val`, in `axiom`, so that the index used for `str` equals `val`. +/// For instance, if `axiom` corresponds to \f$\forall q.\ s[q+x]='a' \land +/// t[q]='b'\f$, `instantiate(axiom,s,v)` would return an expression for +/// \f$s[v]='a' \land t[v-x]='b'\f$. +/// \param stream: output stream +/// \param axiom: a universally quantified formula +/// \param str: an array of char variable +/// \param val: an index expression +/// \return `axiom` with substitued `qvar` static exprt instantiate( messaget::mstreamt &stream, const string_constraintt &axiom, @@ -100,7 +126,8 @@ static optionalt get_array( /// Convert index-value map to a vector of values. If a value for an /// index is not defined, set it to the value referenced by the next higher -/// index. The length of the resulting vector is the key of the map's +/// index. +/// The length of the resulting vector is the key of the map's /// last element + 1 /// \param index_value: map containing values of specific vector cells /// \return Vector containing values as described in the map @@ -128,7 +155,6 @@ static std::vector fill_in_map_as_vector( return result; } - static bool validate(const string_refinementt::infot &info) { PRECONDITION(info.ns); @@ -176,6 +202,27 @@ static void display_index_set( << " newly added)" << eom; } +/// Instantiation of all constraints +/// +/// The string refinement decision procedure works with two types of quantified +/// axioms, which are of the form \f$\forall x.\ P(x)\f$ (`string_constraintt`) +/// or of the form +/// \f$\forall x. P(x) \Rightarrow \exists y .s_0[x+y] \ne s_1[y] \f$ +/// (`string_not_contains_constraintt`). +/// They are instantiated in a way which depends on their form: +/// * For formulas of the form \f$\forall x.\ P(x)\f$ if string `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 +// NOLINTNEXTLINE +/// `instantiate(messaget::mstreamt&,const string_constraintt&,const exprt &,const exprt&)` +/// for details) +/// * For formulas of the form +/// \f$\forall x. P(x) \Rightarrow \exists y .s_0[x+y] \ne s_1[y]) \f$ we +/// need to look at the index set of both `s_0` and `s_1`. +/// (See `instantiate(const string_not_contains_constraintt &axiom)` +/// for details) static std::vector generate_instantiations( messaget::mstreamt &stream, const namespacet &ns, @@ -309,9 +356,10 @@ void replace_symbols_in_equations( symbol_resolve.replace_expr(eq); } -/// Add equation to `m_equation_list` or give them to `supert::set_to` -/// \param expr: an expression -/// \param value: the value to set it to +/// Record the constraints to ensure that the expression is true when +/// the boolean is true and false otherwise. +/// \param expr: an expression of type `bool` +/// \param value: the boolean value to set it to void string_refinementt::set_to(const exprt &expr, bool value) { PRECONDITION(expr.type().id()==ID_bool); @@ -410,9 +458,70 @@ void output_equations( << " == " << from_expr(ns, "", eq.rhs()) << std::endl; } -/// use a refinement loop to instantiate universal axioms, call the sat solver, -/// and instantiate more indexes if needed. -/// \return result of the decision procedure +/// Main decision procedure of the solver. 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 +// NOLINTNEXTLINE +/// `generate_symbol_resolution_from_equations(const std::vector&,const namespacet&,messaget::mstreamt&)`. +/// All these symbols are then replaced using +// NOLINTNEXTLINE +/// `replace_symbols_in_equations(const union_find_replacet &, std::vector &)`. +/// +/// ## Conversion to first order formulas: +/// Each string primitive is converted to a list of first order formulas by the +// NOLINTNEXTLINE +/// function `substitute_function_applications_in_equations(std::vector&,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 \ref 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 by`super_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; +/// } +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// \return `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. decision_proceduret::resultt string_refinementt::dec_solve() { #ifdef DEBUG @@ -1403,7 +1512,7 @@ static std::pair> check_axioms( return { false, std::vector() }; } -/// \par parameters: an expression with only addition and subtraction +/// \param f: an expression with only addition and subtraction /// \return a map where each leaf of the input is mapped to the number of times /// it is added. For instance, expression $x + x - y$ would give the map x -> /// 2, y -> -1. @@ -1445,7 +1554,9 @@ static std::map map_representation_of_sum(const exprt &f) return elems; } -/// \par parameters: a map from expressions to integers +/// \param m: a map from expressions to integers +/// \param type: type for the returned expression +/// \param negated: optinal Boolean asking to negates the sum /// \return a expression for the sum of each element in the map a number of /// times given by the corresponding integer in the map. For a map x -> 2, y /// -> -1 would give an expression $x + x - y$. @@ -1520,7 +1631,7 @@ static exprt sum_over_map( return index_const; } -/// \par parameters: an expression with only plus and minus expr +/// \param f: an expression with only plus and minus expr /// \return an equivalent expression in a canonical form exprt simplify_sum(const exprt &f) { @@ -1528,13 +1639,16 @@ exprt simplify_sum(const exprt &f) return sum_over_map(map, f.type()); } -/// \par parameters: a symbol qvar, an expression val, an expression f -/// containing + and − -/// operations in which qvar should appear exactly once. -/// \return an expression corresponding of $f^{−1}(val)$ where $f$ is seen as -/// a function of $qvar$, i.e. the value that is necessary for qvar for f to -/// be equal to val. For instance, if `f` corresponds to the expression $q + -/// x$, `compute_inverse_function(q,v,f)` returns an expression for $v - x$. +/// \param stream: an output stream +/// \param qvar: a symbol representing a universally quantified variable +/// \param val: an expression +/// \param f: an expression containing `+` and `-` +/// operations in which `qvar` should appear exactly once. +/// \return an expression corresponding of $f^{-1}(val)$ where $f$ is seen as +/// a function of $qvar$, i.e. the value that is necessary for `qvar` for `f` +/// to be equal to `val`. For instance, if `f` corresponds to the expression +/// $q + x$, `compute_inverse_function(q,v,f)` returns an expression +/// for $v - x$. static exprt compute_inverse_function( messaget::mstreamt &stream, const exprt &qvar, @@ -1593,7 +1707,8 @@ class find_qvar_visitort: public const_expr_visitort }; /// look for the symbol and return true if it is found -/// \par parameters: an index expression and a symbol qvar +/// \param index: an index expression +/// \param qvar: a symbol expression /// \return a Boolean static bool find_qvar(const exprt &index, const symbol_exprt &qvar) { @@ -1602,9 +1717,11 @@ static bool find_qvar(const exprt &index, const symbol_exprt &qvar) return v2.found; } -/// add to the index set all the indices that appear in the formulas and the -/// upper bound minus one -/// \par parameters: a list of string constraints +/// Add to the index set all the indices that appear in the formulas and the +/// upper bound minus one. +/// \param index_set: set of indexes to update +/// \param ns: namespace +/// \param axioms: a list of string axioms static void initial_index_set( index_set_pairt &index_set, const namespacet &ns, @@ -1616,8 +1733,10 @@ static void initial_index_set( initial_index_set(index_set, ns, axiom); } -/// add to the index set all the indices that appear in the formulas -/// \par parameters: a list of string constraints +/// Add to the index set all the indices that appear in the formulas. +/// \param index_set: set of indexes to update +/// \param ns: namespace +/// \param current_constraints: a vector of string constraints static void update_index_set( index_set_pairt &index_set, const namespacet &ns, @@ -1655,9 +1774,11 @@ static void get_sub_arrays(const exprt &array_expr, std::vector &accu) } } -/// add to the index set all the indices that appear in the formula and the -/// upper bound minus one -/// \par parameters: a string constraint +/// Add `i` to the index set all the indices that appear in the formula. +/// \param index_set: set of indexes +/// \param ns: namespace +/// \param s: an expression containing strings +/// \param i: an expression representing an index static void add_to_index_set( index_set_pairt &index_set, const namespacet &ns, @@ -1755,8 +1876,10 @@ static void initial_index_set( add_to_index_set(index_set, ns, axiom.s1().content(), kminus1); } -/// add to the index set all the indices that appear in the formula -/// \par parameters: a string constraint +/// Add to the index set all the indices that appear in the formula +/// \param index_set: set of indexes +/// \param ns: namespace +/// \param formula: a string constraint static void update_index_set( index_set_pairt &index_set, const namespacet &ns, @@ -1813,13 +1936,18 @@ static exprt find_index( :to_index_expr(*it).index(); } -/// \par parameters: a universally quantified formula `axiom`, an array of char -/// variable `str`, and an index expression `val`. -/// \return substitute `qvar` the universally quantified variable of `axiom`, by -/// an index `val`, in `axiom`, so that the index used for `str` equals `val`. -/// For instance, if `axiom` corresponds to \f$\forall q. s[q+x]='a' && -/// t[q]='b'\f$, `instantiate(axiom,s,v)` would return an expression for -/// \f$s[v]='a' && t[v-x]='b'\f$. +/// Instantiates a string constraint by substituting the quantifiers. +/// For a string constraint of the form \f$\forall q. P(x)\f$, +/// substitute `qvar` the universally quantified variable of `axiom`, by +/// an index `val`, in `axiom`, so that the index used for `str` equals `val`. +/// For instance, if `axiom` corresponds to \f$\forall q. s[q+x]={\tt 'a'} \land +/// t[q]={\tt 'b'} \f$, `instantiate(axiom,s,v)` would return an expression for +/// \f$s[v]={\tt 'a'} \land t[v-x]={\tt 'b'}\f$. +/// \param stream: a message stream +/// \param axiom: a universally quantified formula `axiom` +/// \param str: an array of characters +/// \param val: an index expression +/// \return instantiated formula static exprt instantiate( messaget::mstreamt &stream, const string_constraintt &axiom, @@ -1844,9 +1972,20 @@ static exprt instantiate( /// Instantiates a quantified formula representing `not_contains` by /// substituting the quantifiers and generating axioms. +/// +/// For a formula of the form +/// \f$\phi = \forall x. P(x) \Rightarrow Q(x, f(x))\f$ +/// let \f$instantiate\_not\_contains(\phi) = ( (f(t) = u) \land +/// P(t) ) \Rightarrow Q(t, u)\f$. +/// Then \f$\forall x.\ P(x) \Rightarrow Q(x, f(x)) \models \f$ +/// Axioms of the form \f$\forall x. P(x) \Rightarrow \exists y .Q(x, y) \f$ +/// can be transformed into the the equisatisfiable +/// formula \f$\forall x. P(x) \Rightarrow Q(x, f(x))\f$ for a new function +/// symbol `f`. Hence, after transforming axioms of the second type and +/// by the above lemmas, we can create quantifier free formulas that are +/// entailed by a (transformed) axiom. /// \param [in] axiom: the axiom to instantiate /// \param index_set: set of indexes -/// \param current_index_set: set of indexes that have been newly added /// \param generator: constraint generator object /// \return the lemmas produced through instantiation static std::vector instantiate( @@ -1919,9 +2058,13 @@ exprt substitute_array_lists(exprt expr, size_t string_max_length) return expr; } -/// evaluation of the expression in the current model -/// \par parameters: an expression -/// \return an expression +/// Evaluates the given expression in the valuation found by +/// string_refinementt::dec_solve. +/// +/// The difference with supert::get is that arrays of characters need to be +/// concretized. See concretize_arrays_in_expression for how it is done. +/// \param expr: an expression +/// \return evaluated expression exprt string_refinementt::get(const exprt &expr) const { const auto super_get = [this](const exprt &expr) { // NOLINT @@ -2033,7 +2176,7 @@ static array_index_mapt gather_indices(const exprt &expr) /// \param expr: an expression /// \param var: a symbol /// \return Boolean telling whether `expr` is a linear function of `var`. -/// TODO: add unit test +/// \todo Add unit tests /// \related string_constraintt static bool is_linear_arithmetic_expr(const exprt &expr, const symbol_exprt &var)