diff --git a/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp b/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp index 2b2014dfaea..f7c310d1109 100644 --- a/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp +++ b/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp @@ -10,7 +10,7 @@ Author: Diffblue Ltd. #include #include -#include +#include #include #include #include diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 02fc6453e16..4f777a1849e 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -162,6 +162,7 @@ SRC = $(BOOLEFORCE_SRC) \ strings/array_pool.cpp \ strings/equation_symbol_mapping.cpp \ strings/string_builtin_function.cpp \ + strings/string_dependencies.cpp \ strings/string_refinement.cpp \ strings/string_refinement_util.cpp \ strings/string_constraint.cpp \ diff --git a/src/solvers/strings/string_dependencies.cpp b/src/solvers/strings/string_dependencies.cpp new file mode 100644 index 00000000000..fb72a5959aa --- /dev/null +++ b/src/solvers/strings/string_dependencies.cpp @@ -0,0 +1,355 @@ +/*******************************************************************\ + +Module: String solver + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#include "string_dependencies.h" +#include +#include +#include +#include +#include + +/// Applies `f` on all strings contained in `e` that are not if-expressions. +/// For instance on input `cond1?s1:cond2?s2:s3` we apply `f` on s1, s2 and s3. +static void for_each_atomic_string( + const array_string_exprt &e, + const std::function f); + +/// Construct a string_builtin_functiont object from a function application +/// \return a unique pointer to the created object +static std::unique_ptr to_string_builtin_function( + const function_application_exprt &fun_app, + const exprt &return_code, + array_poolt &array_pool) +{ + const auto name = expr_checked_cast(fun_app.function()); + PRECONDITION(!is_ssa_expr(name)); + + const irep_idt &id = name.get_identifier(); + + if(id == ID_cprover_string_insert_func) + return util_make_unique( + return_code, fun_app.arguments(), array_pool); + + if(id == ID_cprover_string_concat_func) + return util_make_unique( + return_code, fun_app.arguments(), array_pool); + + if(id == ID_cprover_string_concat_char_func) + return util_make_unique( + return_code, fun_app.arguments(), array_pool); + + if(id == ID_cprover_string_of_int_func) + return util_make_unique( + return_code, fun_app.arguments(), array_pool); + + if(id == ID_cprover_string_char_set_func) + return util_make_unique( + return_code, fun_app.arguments(), array_pool); + + if(id == ID_cprover_string_to_lower_case_func) + return util_make_unique( + return_code, fun_app.arguments(), array_pool); + + if(id == ID_cprover_string_to_upper_case_func) + return util_make_unique( + return_code, fun_app.arguments(), array_pool); + + return util_make_unique( + return_code, fun_app, array_pool); +} + +string_dependenciest::string_nodet & +string_dependenciest::get_node(const array_string_exprt &e) +{ + auto entry_inserted = node_index_pool.emplace(e, string_nodes.size()); + if(!entry_inserted.second) + return string_nodes[entry_inserted.first->second]; + + string_nodes.emplace_back(e, entry_inserted.first->second); + return string_nodes.back(); +} + +std::unique_ptr +string_dependenciest::node_at(const array_string_exprt &e) const +{ + const auto &it = node_index_pool.find(e); + if(it != node_index_pool.end()) + return util_make_unique(string_nodes.at(it->second)); + return {}; +} + +string_dependenciest::builtin_function_nodet &string_dependenciest::make_node( + std::unique_ptr &builtin_function) +{ + builtin_function_nodes.emplace_back( + std::move(builtin_function), builtin_function_nodes.size()); + return builtin_function_nodes.back(); +} + +const string_builtin_functiont &string_dependenciest::get_builtin_function( + const builtin_function_nodet &node) const +{ + return *node.data; +} + +static void for_each_atomic_string( + const array_string_exprt &e, + const std::function f) +{ + if(e.id() != ID_if) + return f(e); + + const auto if_expr = to_if_expr(e); + for_each_atomic_string(to_array_string_expr(if_expr.true_case()), f); + for_each_atomic_string(to_array_string_expr(if_expr.false_case()), f); +} + +void string_dependenciest::add_dependency( + const array_string_exprt &e, + const builtin_function_nodet &builtin_function_node) +{ + for_each_atomic_string(e, [&](const array_string_exprt &s) { //NOLINT + string_nodet &string_node = get_node(s); + string_node.dependencies.push_back(builtin_function_node.index); + }); +} + +void string_dependenciest::clear() +{ + builtin_function_nodes.clear(); + string_nodes.clear(); + node_index_pool.clear(); + clean_cache(); +} + +static void add_dependency_to_string_subexprs( + string_dependenciest &dependencies, + const function_application_exprt &fun_app, + const string_dependenciest::builtin_function_nodet &builtin_function_node, + array_poolt &array_pool) +{ + PRECONDITION(fun_app.arguments()[0].type().id() != ID_pointer); + if( + fun_app.arguments().size() > 1 && + fun_app.arguments()[1].type().id() == ID_pointer) + { + // Case where the result is given as a pointer argument + const array_string_exprt string = + array_pool.find(fun_app.arguments()[1], fun_app.arguments()[0]); + dependencies.add_dependency(string, builtin_function_node); + } + + for(const auto &expr : fun_app.arguments()) + { + std::for_each( + expr.depth_begin(), + expr.depth_end(), + [&](const exprt &e) { // NOLINT + if(is_refined_string_type(e.type())) + { + const auto string_struct = expr_checked_cast(e); + const auto string = of_argument(array_pool, string_struct); + dependencies.add_dependency(string, builtin_function_node); + } + }); + } +} + +optionalt string_dependenciest::eval( + const array_string_exprt &s, + const std::function &get_value) const +{ + const auto &it = node_index_pool.find(s); + if(it == node_index_pool.end()) + return {}; + + if(eval_string_cache[it->second]) + return eval_string_cache[it->second]; + + const auto node = string_nodes[it->second]; + const auto &f = node.result_from; + if(f && node.dependencies.size() == 1) + { + const auto value_opt = builtin_function_nodes[*f].data->eval(get_value); + eval_string_cache[it->second] = value_opt; + return value_opt; + } + return {}; +} + +void string_dependenciest::clean_cache() +{ + eval_string_cache.resize(string_nodes.size()); + for(auto &e : eval_string_cache) + e.reset(); +} + +bool add_node( + string_dependenciest &dependencies, + const equal_exprt &equation, + array_poolt &array_pool) +{ + const auto fun_app = + expr_try_dynamic_cast(equation.rhs()); + if(!fun_app) + return false; + + auto builtin_function = + to_string_builtin_function(*fun_app, equation.lhs(), array_pool); + + CHECK_RETURN(builtin_function != nullptr); + const auto &builtin_function_node = dependencies.make_node(builtin_function); + // Warning: `builtin_function` has been emptied and should not be used anymore + + if( + const auto &string_result = + dependencies.get_builtin_function(builtin_function_node).string_result()) + { + dependencies.add_dependency(*string_result, builtin_function_node); + auto &node = dependencies.get_node(*string_result); + node.result_from = builtin_function_node.index; + + // Ensure all atomic strings in the argument have an associated node + for(const auto arg : builtin_function_node.data->string_arguments()) + { + for_each_atomic_string( + arg, [&](const array_string_exprt &atomic) { // NOLINT + (void)dependencies.get_node(atomic); + }); + } + } + else + add_dependency_to_string_subexprs( + dependencies, *fun_app, builtin_function_node, array_pool); + + return true; +} + +void string_dependenciest::for_each_dependency( + const builtin_function_nodet &node, + const std::function &f) const +{ + for(const auto &s : node.data->string_arguments()) + { + std::vector> stack({s}); + while(!stack.empty()) + { + const auto current = stack.back(); + stack.pop_back(); + if(const auto if_expr = expr_try_dynamic_cast(current.get())) + { + stack.emplace_back(if_expr->true_case()); + stack.emplace_back(if_expr->false_case()); + } + else + { + const auto string_node = node_at(to_array_string_expr(current)); + INVARIANT( + string_node, + "dependencies of the node should have been added to the graph at " + "node creation " + + current.get().pretty()); + f(*string_node); + } + } + } +} + +void string_dependenciest::for_each_dependency( + const string_nodet &node, + const std::function &f) const +{ + for(const std::size_t &index : node.dependencies) + f(builtin_function_nodes[index]); +} + +void string_dependenciest::for_each_successor( + const nodet &node, + const std::function &f) const +{ + switch(node.kind) + { + case nodet::BUILTIN: + for_each_dependency( + builtin_function_nodes[node.index], + [&](const string_nodet &n) { return f(nodet(n)); }); + break; + + case nodet::STRING: + for_each_dependency( + string_nodes[node.index], + [&](const builtin_function_nodet &n) { return f(nodet(n)); }); + break; + } +} + +void string_dependenciest::for_each_node( + const std::function &f) const +{ + for(const auto string_node : string_nodes) + f(nodet(string_node)); + for(std::size_t i = 0; i < builtin_function_nodes.size(); ++i) + f(nodet(builtin_function_nodes[i])); +} + +void string_dependenciest::output_dot(std::ostream &stream) const +{ + const auto for_each = + [&](const std::function &f) { // NOLINT + for_each_node(f); + }; + const auto for_each_succ = + [&](const nodet &n, const std::function &f) { // NOLINT + for_each_successor(n, f); + }; + const auto node_to_string = [&](const nodet &n) { // NOLINT + std::stringstream ostream; + if(n.kind == nodet::BUILTIN) + ostream << '"' << builtin_function_nodes[n.index].data->name() << '_' + << n.index << '"'; + else + ostream << '"' << format(string_nodes[n.index].expr) << '"'; + return ostream.str(); + }; + stream << "digraph dependencies {\n"; + output_dot_generic( + stream, for_each, for_each_succ, node_to_string, node_to_string); + stream << '}' << std::endl; +} + +void string_dependenciest::add_constraints( + string_constraint_generatort &generator) +{ + std::unordered_set test_dependencies; + for(const auto &builtin : builtin_function_nodes) + { + if(builtin.data->maybe_testing_function()) + test_dependencies.insert(nodet(builtin)); + } + + get_reachable( + test_dependencies, + [&]( + const nodet &n, + const std::function &f) { // NOLINT + for_each_successor(n, f); + }); + + for(const auto &node : builtin_function_nodes) + { + if(test_dependencies.count(nodet(node))) + { + const auto &builtin = builtin_function_nodes[node.index]; + string_constraintst constraints = builtin.data->constraints(generator); + merge(generator.constraints, std::move(constraints)); + } + else + generator.constraints.existential.push_back( + node.data->length_constraint()); + } +} diff --git a/src/solvers/strings/string_dependencies.h b/src/solvers/strings/string_dependencies.h new file mode 100644 index 00000000000..46c96127859 --- /dev/null +++ b/src/solvers/strings/string_dependencies.h @@ -0,0 +1,201 @@ +/*******************************************************************\ + +Module: String solver + +Author: Diffblue Ltd. + +\*******************************************************************/ + +/// \file +/// Keeps track of dependencies between strings. + +#ifndef CPROVER_SOLVERS_STRINGS_STRING_DEPENDENCIES_H +#define CPROVER_SOLVERS_STRINGS_STRING_DEPENDENCIES_H + +#include + +#include "string_builtin_function.h" + +/// Keep track of dependencies between strings. +/// Each string points to the builtin_function calls on which it depends. +/// Each builtin_function points to the strings on which the result depends. +class string_dependenciest +{ +public: + /// A builtin function node contains a builtin function call + class builtin_function_nodet + { + public: + // index in the `builtin_function_nodes` vector + std::size_t index; + // pointer to the builtin function + std::unique_ptr data; + + explicit builtin_function_nodet( + std::unique_ptr d, + std::size_t i) + : index(i), data(std::move(d)) + { + } + + builtin_function_nodet(builtin_function_nodet &&other) + : index(other.index), data(std::move(other.data)) + { + } + + builtin_function_nodet &operator=(builtin_function_nodet &&other) + { + index = other.index; + data = std::move(other.data); + return *this; + } + }; + + /// A string node points to builtin_function on which it depends + class string_nodet + { + public: + // expression the node corresponds to + array_string_exprt expr; + // index in the string_nodes vector + std::size_t index; + // builtin functions on which it depends, refered by there index in + // builtin_function node vector. + // \todo should these we shared pointers? + std::vector dependencies; + // builtin function of which it is the result + optionalt result_from; + + explicit string_nodet(array_string_exprt e, const std::size_t index) + : expr(std::move(e)), index(index) + { + } + }; + + string_nodet &get_node(const array_string_exprt &e); + + std::unique_ptr + node_at(const array_string_exprt &e) const; + + /// `builtin_function` is reset to an empty pointer after the node is created + builtin_function_nodet & + make_node(std::unique_ptr &builtin_function); + const string_builtin_functiont & + get_builtin_function(const builtin_function_nodet &node) const; + + /// Add edge from node for `e` to node for `builtin_function` if `e` is a + /// simple array expression. If it is an `if_exprt` we add the sub-expressions + /// that are not `if_exprt`s instead. + void add_dependency( + const array_string_exprt &e, + const builtin_function_nodet &builtin_function); + + /// Applies `f` to each node on which `node` depends + void for_each_dependency( + const string_nodet &node, + const std::function &f) const; + void for_each_dependency( + const builtin_function_nodet &node, + const std::function &f) const; + + /// Attempt to evaluate the given string from the dependencies and valuation + /// of strings on which it depends + /// Warning: eval uses a cache which must be cleaned everytime the valuations + /// given by get_value can change. + optionalt eval( + const array_string_exprt &s, + const std::function &get_value) const; + + /// Clean the cache used by `eval` + void clean_cache(); + + void output_dot(std::ostream &stream) const; + + /// For all builtin call on which a test (or an unsupported buitin) + /// result depends, add the corresponding constraints. For the other builtin + /// only add constraints on the length. + void add_constraints(string_constraint_generatort &generatort); + + /// Clear the content of the dependency graph + void clear(); + +private: + /// Set of nodes representing builtin_functions + std::vector builtin_function_nodes; + + /// Set of nodes representing strings + std::vector string_nodes; + + /// Nodes describing dependencies of a string: values of the map correspond + /// to indexes in the vector `string_nodes`. + std::unordered_map + node_index_pool; + + class nodet + { + public: + enum + { + BUILTIN, + STRING + } kind; + std::size_t index; + + explicit nodet(const builtin_function_nodet &builtin) + : kind(BUILTIN), index(builtin.index) + { + } + + explicit nodet(const string_nodet &string_node) + : kind(STRING), index(string_node.index) + { + } + + bool operator==(const nodet &n) const + { + return n.kind == kind && n.index == index; + } + }; + + /// Hash function for nodes + // NOLINTNEXTLINE(readability/identifiers) + struct node_hash + { + size_t + operator()(const string_dependenciest::nodet &node) const optional_noexcept + { + return 2 * node.index + + (node.kind == string_dependenciest::nodet::STRING ? 0 : 1); + } + }; + + mutable std::vector> eval_string_cache; + + /// Applies `f` on all nodes + void for_each_node(const std::function &f) const; + + /// Applies `f` on all successors of the node n + void for_each_successor( + const nodet &i, + const std::function &f) const; +}; + +/// When right hand side of equation is a builtin_function add +/// a "string_builtin_function" node to the graph and connect it to the strings +/// on which it depends and which depends on it. +/// If the string builtin_function is not a supported one, mark all the string +/// arguments as depending on an unknown builtin_function. +/// \param dependencies: graph to which we add the node +/// \param equation: an equation whose right hand side is possibly a call to a +/// string builtin_function. +/// \param array_pool: array pool containing arrays corresponding to the string +/// exprt arguments of the builtin_function call +/// \return true if a node was added, if false is returned it either means that +/// the right hand side is not a function application +/// \todo there should be a class with just the three functions we require here +bool add_node( + string_dependenciest &dependencies, + const equal_exprt &equation, + array_poolt &array_pool); + +#endif // CPROVER_SOLVERS_STRINGS_STRING_DEPENDENCIES_H diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index fd2db24e300..884427409ef 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -31,6 +31,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #include "equation_symbol_mapping.h" #include "string_constraint_instantiation.h" +#include "string_dependencies.h" static bool is_valid_string_constraint( messaget::mstreamt &stream, diff --git a/src/solvers/strings/string_refinement.h b/src/solvers/strings/string_refinement.h index 22616d63b51..80021207b7b 100644 --- a/src/solvers/strings/string_refinement.h +++ b/src/solvers/strings/string_refinement.h @@ -27,6 +27,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #include "string_constraint.h" #include "string_constraint_generator.h" +#include "string_dependencies.h" #include "string_refinement_invariant.h" #include "string_refinement_util.h" diff --git a/src/solvers/strings/string_refinement_util.cpp b/src/solvers/strings/string_refinement_util.cpp index e0d366b6d41..c56d3335101 100644 --- a/src/solvers/strings/string_refinement_util.cpp +++ b/src/solvers/strings/string_refinement_util.cpp @@ -21,12 +21,6 @@ Author: Diffblue Ltd. #include #include -/// Applies `f` on all strings contained in `e` that are not if-expressions. -/// For instance on input `cond1?s1:cond2?s2:s3` we apply `f` on s1, s2 and s3. -static void for_each_atomic_string( - const array_string_exprt &e, - const std::function f); - bool is_char_type(const typet &type) { return type.id() == ID_unsignedbv && to_unsignedbv_type(type).get_width() <= @@ -182,338 +176,3 @@ array_exprt interval_sparse_arrayt::concretize( size, it == entries.end() ? default_value : it->second); return array; } - -/// Construct a string_builtin_functiont object from a function application -/// \return a unique pointer to the created object -static std::unique_ptr to_string_builtin_function( - const function_application_exprt &fun_app, - const exprt &return_code, - array_poolt &array_pool) -{ - const auto name = expr_checked_cast(fun_app.function()); - PRECONDITION(!is_ssa_expr(name)); - - const irep_idt &id = name.get_identifier(); - - if(id == ID_cprover_string_insert_func) - return util_make_unique( - return_code, fun_app.arguments(), array_pool); - - if(id == ID_cprover_string_concat_func) - return util_make_unique( - return_code, fun_app.arguments(), array_pool); - - if(id == ID_cprover_string_concat_char_func) - return util_make_unique( - return_code, fun_app.arguments(), array_pool); - - if(id == ID_cprover_string_of_int_func) - return util_make_unique( - return_code, fun_app.arguments(), array_pool); - - if(id == ID_cprover_string_char_set_func) - return util_make_unique( - return_code, fun_app.arguments(), array_pool); - - if(id == ID_cprover_string_to_lower_case_func) - return util_make_unique( - return_code, fun_app.arguments(), array_pool); - - if(id == ID_cprover_string_to_upper_case_func) - return util_make_unique( - return_code, fun_app.arguments(), array_pool); - - return util_make_unique( - return_code, fun_app, array_pool); -} - -string_dependenciest::string_nodet & -string_dependenciest::get_node(const array_string_exprt &e) -{ - auto entry_inserted = node_index_pool.emplace(e, string_nodes.size()); - if(!entry_inserted.second) - return string_nodes[entry_inserted.first->second]; - - string_nodes.emplace_back(e, entry_inserted.first->second); - return string_nodes.back(); -} - -std::unique_ptr -string_dependenciest::node_at(const array_string_exprt &e) const -{ - const auto &it = node_index_pool.find(e); - if(it != node_index_pool.end()) - return util_make_unique(string_nodes.at(it->second)); - return {}; -} - -string_dependenciest::builtin_function_nodet &string_dependenciest::make_node( - std::unique_ptr &builtin_function) -{ - builtin_function_nodes.emplace_back( - std::move(builtin_function), builtin_function_nodes.size()); - return builtin_function_nodes.back(); -} - -const string_builtin_functiont &string_dependenciest::get_builtin_function( - const builtin_function_nodet &node) const -{ - return *node.data; -} - -static void for_each_atomic_string( - const array_string_exprt &e, - const std::function f) -{ - if(e.id() != ID_if) - return f(e); - - const auto if_expr = to_if_expr(e); - for_each_atomic_string(to_array_string_expr(if_expr.true_case()), f); - for_each_atomic_string(to_array_string_expr(if_expr.false_case()), f); -} - -void string_dependenciest::add_dependency( - const array_string_exprt &e, - const builtin_function_nodet &builtin_function_node) -{ - for_each_atomic_string(e, [&](const array_string_exprt &s) { //NOLINT - string_nodet &string_node = get_node(s); - string_node.dependencies.push_back(builtin_function_node.index); - }); -} - -void string_dependenciest::clear() -{ - builtin_function_nodes.clear(); - string_nodes.clear(); - node_index_pool.clear(); - clean_cache(); -} - -static void add_dependency_to_string_subexprs( - string_dependenciest &dependencies, - const function_application_exprt &fun_app, - const string_dependenciest::builtin_function_nodet &builtin_function_node, - array_poolt &array_pool) -{ - PRECONDITION(fun_app.arguments()[0].type().id() != ID_pointer); - if( - fun_app.arguments().size() > 1 && - fun_app.arguments()[1].type().id() == ID_pointer) - { - // Case where the result is given as a pointer argument - const array_string_exprt string = - array_pool.find(fun_app.arguments()[1], fun_app.arguments()[0]); - dependencies.add_dependency(string, builtin_function_node); - } - - for(const auto &expr : fun_app.arguments()) - { - std::for_each( - expr.depth_begin(), - expr.depth_end(), - [&](const exprt &e) { // NOLINT - if(is_refined_string_type(e.type())) - { - const auto string_struct = expr_checked_cast(e); - const auto string = of_argument(array_pool, string_struct); - dependencies.add_dependency(string, builtin_function_node); - } - }); - } -} - -optionalt string_dependenciest::eval( - const array_string_exprt &s, - const std::function &get_value) const -{ - const auto &it = node_index_pool.find(s); - if(it == node_index_pool.end()) - return {}; - - if(eval_string_cache[it->second]) - return eval_string_cache[it->second]; - - const auto node = string_nodes[it->second]; - const auto &f = node.result_from; - if(f && node.dependencies.size() == 1) - { - const auto value_opt = builtin_function_nodes[*f].data->eval(get_value); - eval_string_cache[it->second] = value_opt; - return value_opt; - } - return {}; -} - -void string_dependenciest::clean_cache() -{ - eval_string_cache.resize(string_nodes.size()); - for(auto &e : eval_string_cache) - e.reset(); -} - -bool add_node( - string_dependenciest &dependencies, - const equal_exprt &equation, - array_poolt &array_pool) -{ - const auto fun_app = - expr_try_dynamic_cast(equation.rhs()); - if(!fun_app) - return false; - - auto builtin_function = - to_string_builtin_function(*fun_app, equation.lhs(), array_pool); - - CHECK_RETURN(builtin_function != nullptr); - const auto &builtin_function_node = dependencies.make_node(builtin_function); - // Warning: `builtin_function` has been emptied and should not be used anymore - - if( - const auto &string_result = - dependencies.get_builtin_function(builtin_function_node).string_result()) - { - dependencies.add_dependency(*string_result, builtin_function_node); - auto &node = dependencies.get_node(*string_result); - node.result_from = builtin_function_node.index; - - // Ensure all atomic strings in the argument have an associated node - for(const auto arg : builtin_function_node.data->string_arguments()) - { - for_each_atomic_string( - arg, [&](const array_string_exprt &atomic) { // NOLINT - (void)dependencies.get_node(atomic); - }); - } - } - else - add_dependency_to_string_subexprs( - dependencies, *fun_app, builtin_function_node, array_pool); - - return true; -} - -void string_dependenciest::for_each_dependency( - const builtin_function_nodet &node, - const std::function &f) const -{ - for(const auto &s : node.data->string_arguments()) - { - std::vector> stack({s}); - while(!stack.empty()) - { - const auto current = stack.back(); - stack.pop_back(); - if(const auto if_expr = expr_try_dynamic_cast(current.get())) - { - stack.emplace_back(if_expr->true_case()); - stack.emplace_back(if_expr->false_case()); - } - else - { - const auto string_node = node_at(to_array_string_expr(current)); - INVARIANT( - string_node, - "dependencies of the node should have been added to the graph at " - "node creation " + - current.get().pretty()); - f(*string_node); - } - } - } -} - -void string_dependenciest::for_each_dependency( - const string_nodet &node, - const std::function &f) const -{ - for(const std::size_t &index : node.dependencies) - f(builtin_function_nodes[index]); -} - -void string_dependenciest::for_each_successor( - const nodet &node, - const std::function &f) const -{ - switch(node.kind) - { - case nodet::BUILTIN: - for_each_dependency( - builtin_function_nodes[node.index], - [&](const string_nodet &n) { return f(nodet(n)); }); - break; - - case nodet::STRING: - for_each_dependency( - string_nodes[node.index], - [&](const builtin_function_nodet &n) { return f(nodet(n)); }); - break; - } -} - -void string_dependenciest::for_each_node( - const std::function &f) const -{ - for(const auto string_node : string_nodes) - f(nodet(string_node)); - for(std::size_t i = 0; i < builtin_function_nodes.size(); ++i) - f(nodet(builtin_function_nodes[i])); -} - -void string_dependenciest::output_dot(std::ostream &stream) const -{ - const auto for_each = - [&](const std::function &f) { // NOLINT - for_each_node(f); - }; - const auto for_each_succ = - [&](const nodet &n, const std::function &f) { // NOLINT - for_each_successor(n, f); - }; - const auto node_to_string = [&](const nodet &n) { // NOLINT - std::stringstream ostream; - if(n.kind == nodet::BUILTIN) - ostream << '"' << builtin_function_nodes[n.index].data->name() << '_' - << n.index << '"'; - else - ostream << '"' << format(string_nodes[n.index].expr) << '"'; - return ostream.str(); - }; - stream << "digraph dependencies {\n"; - output_dot_generic( - stream, for_each, for_each_succ, node_to_string, node_to_string); - stream << '}' << std::endl; -} - -void string_dependenciest::add_constraints( - string_constraint_generatort &generator) -{ - std::unordered_set test_dependencies; - for(const auto &builtin : builtin_function_nodes) - { - if(builtin.data->maybe_testing_function()) - test_dependencies.insert(nodet(builtin)); - } - - get_reachable( - test_dependencies, - [&]( - const nodet &n, - const std::function &f) { // NOLINT - for_each_successor(n, f); - }); - - for(const auto &node : builtin_function_nodes) - { - if(test_dependencies.count(nodet(node))) - { - const auto &builtin = builtin_function_nodes[node.index]; - string_constraintst constraints = builtin.data->constraints(generator); - merge(generator.constraints, std::move(constraints)); - } - else - generator.constraints.existential.push_back( - node.data->length_constraint()); - } -} diff --git a/src/solvers/strings/string_refinement_util.h b/src/solvers/strings/string_refinement_util.h index 678ebc34a99..0bacc9fdae8 100644 --- a/src/solvers/strings/string_refinement_util.h +++ b/src/solvers/strings/string_refinement_util.h @@ -132,186 +132,4 @@ class interval_sparse_arrayt final : public sparse_arrayt } }; -/// Keep track of dependencies between strings. -/// Each string points to the builtin_function calls on which it depends. -/// Each builtin_function points to the strings on which the result depends. -class string_dependenciest -{ -public: - /// A builtin function node contains a builtin function call - class builtin_function_nodet - { - public: - // index in the `builtin_function_nodes` vector - std::size_t index; - // pointer to the builtin function - std::unique_ptr data; - - explicit builtin_function_nodet( - std::unique_ptr d, - std::size_t i) - : index(i), data(std::move(d)) - { - } - - builtin_function_nodet(builtin_function_nodet &&other) - : index(other.index), data(std::move(other.data)) - { - } - - builtin_function_nodet &operator=(builtin_function_nodet &&other) - { - index = other.index; - data = std::move(other.data); - return *this; - } - }; - - /// A string node points to builtin_function on which it depends - class string_nodet - { - public: - // expression the node corresponds to - array_string_exprt expr; - // index in the string_nodes vector - std::size_t index; - // builtin functions on which it depends, refered by there index in - // builtin_function node vector. - // \todo should these we shared pointers? - std::vector dependencies; - // builtin function of which it is the result - optionalt result_from; - - explicit string_nodet(array_string_exprt e, const std::size_t index) - : expr(std::move(e)), index(index) - { - } - }; - - string_nodet &get_node(const array_string_exprt &e); - - std::unique_ptr - node_at(const array_string_exprt &e) const; - - /// `builtin_function` is reset to an empty pointer after the node is created - builtin_function_nodet & - make_node(std::unique_ptr &builtin_function); - const string_builtin_functiont & - get_builtin_function(const builtin_function_nodet &node) const; - - /// Add edge from node for `e` to node for `builtin_function` if `e` is a - /// simple array expression. If it is an `if_exprt` we add the sub-expressions - /// that are not `if_exprt`s instead. - void add_dependency( - const array_string_exprt &e, - const builtin_function_nodet &builtin_function); - - /// Applies `f` to each node on which `node` depends - void for_each_dependency( - const string_nodet &node, - const std::function &f) const; - void for_each_dependency( - const builtin_function_nodet &node, - const std::function &f) const; - - /// Attempt to evaluate the given string from the dependencies and valuation - /// of strings on which it depends - /// Warning: eval uses a cache which must be cleaned everytime the valuations - /// given by get_value can change. - optionalt eval( - const array_string_exprt &s, - const std::function &get_value) const; - - /// Clean the cache used by `eval` - void clean_cache(); - - void output_dot(std::ostream &stream) const; - - /// For all builtin call on which a test (or an unsupported buitin) - /// result depends, add the corresponding constraints. For the other builtin - /// only add constraints on the length. - void add_constraints(string_constraint_generatort &generatort); - - /// Clear the content of the dependency graph - void clear(); - -private: - /// Set of nodes representing builtin_functions - std::vector builtin_function_nodes; - - /// Set of nodes representing strings - std::vector string_nodes; - - /// Nodes describing dependencies of a string: values of the map correspond - /// to indexes in the vector `string_nodes`. - std::unordered_map - node_index_pool; - - class nodet - { - public: - enum - { - BUILTIN, - STRING - } kind; - std::size_t index; - - explicit nodet(const builtin_function_nodet &builtin) - : kind(BUILTIN), index(builtin.index) - { - } - - explicit nodet(const string_nodet &string_node) - : kind(STRING), index(string_node.index) - { - } - - bool operator==(const nodet &n) const - { - return n.kind == kind && n.index == index; - } - }; - - /// Hash function for nodes - // NOLINTNEXTLINE(readability/identifiers) - struct node_hash - { - size_t - operator()(const string_dependenciest::nodet &node) const optional_noexcept - { - return 2 * node.index + - (node.kind == string_dependenciest::nodet::STRING ? 0 : 1); - } - }; - - mutable std::vector> eval_string_cache; - - /// Applies `f` on all nodes - void for_each_node(const std::function &f) const; - - /// Applies `f` on all successors of the node n - void for_each_successor( - const nodet &i, - const std::function &f) const; -}; - -/// When right hand side of equation is a builtin_function add -/// a "string_builtin_function" node to the graph and connect it to the strings -/// on which it depends and which depends on it. -/// If the string builtin_function is not a supported one, mark all the string -/// arguments as depending on an unknown builtin_function. -/// \param dependencies: graph to which we add the node -/// \param equation: an equation whose right hand side is possibly a call to a -/// string builtin_function. -/// \param array_pool: array pool containing arrays corresponding to the string -/// exprt arguments of the builtin_function call -/// \return true if a node was added, if false is returned it either means that -/// the right hand side is not a function application -/// \todo there should be a class with just the three functions we require here -bool add_node( - string_dependenciest &dependencies, - const equal_exprt &equation, - array_poolt &array_pool); - #endif // CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H