From a2fab1097fb477d0a9e143105b01689556a9e73c Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Mar 2018 14:42:50 +0000 Subject: [PATCH 01/19] Linting corrections in string_refinement --- src/solvers/refinement/string_refinement.cpp | 2 +- src/solvers/refinement/string_refinement.h | 9 +++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 95df34885cc..62a683d6e7a 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -1862,7 +1862,7 @@ static exprt compute_inverse_function( return sum_over_map(elems, f.type(), neg); } -class find_qvar_visitort: public const_expr_visitort +class find_qvar_visitort : public const_expr_visitort { private: const exprt &qvar_; diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 7ee95f8d3a6..a0d2a532d2a 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -44,10 +44,11 @@ class string_refinementt final: public bv_refinementt }; public: /// string_refinementt constructor arguments - struct infot: - public bv_refinementt::infot, - public string_constraint_generatort::infot, - public configt { }; + struct infot : public bv_refinementt::infot, + public string_constraint_generatort::infot, + public configt + { + }; explicit string_refinementt(const infot &); From 5108a72b322fc7584c787643db42f8b4c2d2e2f3 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 8 Mar 2018 15:43:35 +0000 Subject: [PATCH 02/19] Fix string constraints printing --- src/solvers/refinement/string_constraint.h | 8 ++------ src/solvers/refinement/string_refinement.cpp | 8 ++++---- 2 files changed, 6 insertions(+), 10 deletions(-) diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h index 7e804ec6e13..07bf20408dd 100644 --- a/src/solvers/refinement/string_constraint.h +++ b/src/solvers/refinement/string_constraint.h @@ -148,9 +148,7 @@ extern inline string_constraintt &to_string_constraint(exprt &expr) /// \param [in] identifier: identifier for `from_expr` /// \param [in] expr: constraint to render /// \return rendered string -inline std::string from_expr( - const irep_idt &identifier, - const string_constraintt &expr) +inline std::string to_string(const string_constraintt &expr) { std::ostringstream out; out << "forall " << format(expr.univ_var()) << " in [" @@ -222,9 +220,7 @@ class string_not_contains_constraintt: public exprt /// \param [in] identifier: identifier for `from_expr` /// \param [in] expr: constraint to render /// \return rendered string -inline std::string from_expr( - const irep_idt &identifier, - const string_not_contains_constraintt &expr) +inline std::string to_string(const string_not_contains_constraintt &expr) { std::ostringstream out; out << "forall x in [" << format(expr.univ_lower_bound()) << ", " diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 62a683d6e7a..a6f5698ed9e 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -1475,17 +1475,17 @@ static void debug_check_axioms_step( stream << indent2 << "- axiom:\n" << indent2 << indent; if(axiom.id() == ID_string_constraint) - stream << format(to_string_constraint(axiom)); + stream << to_string(to_string_constraint(axiom)); else if(axiom.id() == ID_string_not_contains_constraint) - stream << format(to_string_not_contains_constraint(axiom)); + stream << to_string(to_string_not_contains_constraint(axiom)); else stream << format(axiom); stream << '\n' << indent2 << "- axiom_in_model:\n" << indent2 << indent; if(axiom_in_model.id() == ID_string_constraint) - stream << format(to_string_constraint(axiom_in_model)); + stream << to_string(to_string_constraint(axiom_in_model)); else if(axiom_in_model.id() == ID_string_not_contains_constraint) - stream << format(to_string_not_contains_constraint(axiom_in_model)); + stream << to_string(to_string_not_contains_constraint(axiom_in_model)); else stream << format(axiom_in_model); From 01394249c3f9d2c9979c39fb8222c5be0d21a409 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 8 Mar 2018 15:44:37 +0000 Subject: [PATCH 03/19] Fix linting problem in string_constraint --- src/solvers/refinement/string_constraint.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h index 07bf20408dd..55aacd7f4d5 100644 --- a/src/solvers/refinement/string_constraint.h +++ b/src/solvers/refinement/string_constraint.h @@ -54,7 +54,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// \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 +class string_constraintt : public exprt { public: // String constraints are of the form @@ -158,7 +158,7 @@ inline std::string to_string(const string_constraintt &expr) } /// Constraints to encode non containement of strings. -class string_not_contains_constraintt: public exprt +class string_not_contains_constraintt : public exprt { public: // string_not contains_constraintt are formula of the form: From f6a153eb7800cd2f60957b1da7d1f323e49cbdc6 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Mar 2018 15:12:34 +0000 Subject: [PATCH 04/19] Check type before adding dependencies We check that the type is that of a string before adding the dependence. --- src/solvers/refinement/string_refinement_util.cpp | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index 06c71623ec1..fb141ea8ddc 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -256,11 +256,11 @@ static void add_unknown_dependency_to_string_subexprs( { std::for_each( expr.depth_begin(), expr.depth_end(), [&](const exprt &e) { // NOLINT - const auto &string_struct = expr_try_dynamic_cast(e); - if(string_struct && string_struct->operands().size() == 2) + if(is_refined_string_type(e.type())) { + const auto &string_struct = expr_checked_cast(e); const array_string_exprt string = - array_pool.find(string_struct->op1(), string_struct->op0()); + array_pool.find(string_struct.op1(), string_struct.op0()); dependencies.add_unknown_dependency(string); } }); @@ -290,9 +290,10 @@ static void add_dependency_to_string_subexprs( expr.depth_begin(), expr.depth_end(), [&](const exprt &e) { // NOLINT - if(const auto structure = expr_try_dynamic_cast(e)) + if(is_refined_string_type(e.type())) { - const array_string_exprt string = array_pool.of_argument(*structure); + const auto string_struct = expr_checked_cast(e); + const auto string = array_pool.of_argument(string_struct); dependencies.add_dependency(string, builtin_function_node); } }); From 06dc6b2efb825db13ef918ada7dbcd7fa7e2bb5e Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Mar 2018 13:11:11 +0000 Subject: [PATCH 05/19] Add an evaluation method to builtin functions This will be used to concretize strings by directly computing them from the primitives instead of using the solver, when possible. --- .../refinement/string_refinement_util.cpp | 128 +++++++++++++++++- .../refinement/string_refinement_util.h | 29 ++++ 2 files changed, 155 insertions(+), 2 deletions(-) diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index fb141ea8ddc..b509776a10d 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -16,8 +16,19 @@ #include #include #include +#include #include "string_refinement_util.h" +/// Get the valuation of the string, given a valuation +static optionalt> eval_string( + const array_string_exprt &a, + const std::function &get_value); + +/// Make a string from a constant array +static array_string_exprt make_string( + const std::vector &array, + const array_typet &array_type); + bool is_char_type(const typet &type) { return type.id() == ID_unsignedbv && @@ -175,6 +186,119 @@ string_insertion_builtin_functiont::string_insertion_builtin_functiont( args.insert(args.end(), fun_args.begin() + 4, fun_args.end()); } +optionalt> eval_string( + const array_string_exprt &a, + const std::function &get_value) +{ + if(a.id() == ID_if) + { + const if_exprt &ite = to_if_expr(a); + const exprt cond = get_value(ite.cond()); + if(!cond.is_constant()) + return {}; + return cond.is_true() + ? eval_string(to_array_string_expr(ite.true_case()), get_value) + : eval_string(to_array_string_expr(ite.false_case()), get_value); + } + + const auto size = numeric_cast(get_value(a.length())); + const exprt content = get_value(a.content()); + const auto &array = expr_try_dynamic_cast(content); + if(!size || !array) + return {}; + + const auto &ops = array->operands(); + INVARIANT(*size == ops.size(), "operands size should match string size"); + + std::vector result; + const mp_integer unknown('?'); + const auto &insert = std::back_inserter(result); + std::transform( + ops.begin(), ops.end(), insert, [unknown](const exprt &e) { // NOLINT + if(const auto i = numeric_cast(e)) + return *i; + return unknown; + }); + return result; +} + +array_string_exprt +make_string(const std::vector &array, const array_typet &array_type) +{ + const typet &char_type = array_type.subtype(); + array_exprt array_expr(array_type); + const auto &insert = std::back_inserter(array_expr.operands()); + std::transform( + array.begin(), array.end(), insert, [&](const mp_integer &i) { // NOLINT + return from_integer(i, char_type); + }); + return to_array_string_expr(array_expr); +} + +std::vector string_concatenation_builtin_functiont::eval( + const std::vector &input1_value, + const std::vector &input2_value, + const std::vector &args_value) const +{ + const std::size_t start_index = + args_value.size() > 0 && args_value[0] > 0 ? args_value[0].to_ulong() : 0; + const std::size_t end_index = args_value.size() > 1 && args_value[1] > 0 + ? args_value[1].to_ulong() + : input2_value.size(); + + std::vector result(input1_value); + result.insert( + result.end(), + input2_value.begin() + start_index, + input2_value.begin() + end_index); + return result; +} + +std::vector string_insertion_builtin_functiont::eval( + const std::vector &input1_value, + const std::vector &input2_value, + const std::vector &args_value) const +{ + PRECONDITION(args_value.size() >= 1 || args_value.size() <= 3); + const std::size_t &offset = numeric_cast_v(args_value[0]); + const std::size_t &start = + args_value.size() > 1 ? numeric_cast_v(args_value[1]) : 0; + const std::size_t &end = args_value.size() > 2 + ? numeric_cast_v(args_value[2]) + : input2_value.size(); + + std::vector result(input1_value); + result.insert( + result.begin() + offset, + input2_value.begin() + start, + input2_value.end() + end); + return result; +} + +optionalt string_insertion_builtin_functiont::eval( + const std::function &get_value) const +{ + const auto &input1_value = eval_string(input1, get_value); + const auto &input2_value = eval_string(input2, get_value); + if(!input2_value.has_value() || !input1_value.has_value()) + return {}; + + std::vector arg_values; + const auto &insert = std::back_inserter(arg_values); + const mp_integer unknown('?'); + std::transform( + args.begin(), args.end(), insert, [&](const exprt &e) { // NOLINT + if(const auto val = numeric_cast(get_value(e))) + return *val; + return unknown; + }); + + const auto result_value = eval(*input1_value, *input2_value, arg_values); + const auto length = from_integer(result_value.size(), result.length().type()); + const array_typet type(result.type().subtype(), length); + return make_string(result_value, type); +} + /// Construct a string_builtin_functiont object from a function application /// \return a unique pointer to the created object, this unique pointer is empty /// if the function does not correspond to one of the supported @@ -192,8 +316,8 @@ static std::unique_ptr to_string_builtin_function( new string_insertion_builtin_functiont(fun_app.arguments(), array_pool)); if(id == ID_cprover_string_concat_func) - return std::unique_ptr( - new string_insertion_builtin_functiont(fun_app.arguments(), array_pool)); + return util_make_unique( + fun_app.arguments(), array_pool); return {}; } diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h index 4501cd68ec3..04fb07571f7 100644 --- a/src/solvers/refinement/string_refinement_util.h +++ b/src/solvers/refinement/string_refinement_util.h @@ -157,6 +157,9 @@ class string_builtin_functiont { return {}; } + + virtual optionalt + eval(const std::function &get_value) const = 0; }; /// String builtin_function transforming one string into another @@ -200,6 +203,32 @@ class string_insertion_builtin_functiont : public string_builtin_functiont { return {input1, input2}; } + + /// Evaluate the result from a concrete valuation of the arguments + virtual std::vector eval( + const std::vector &input1_value, + const std::vector &input2_value, + const std::vector &args_value) const; + + optionalt + eval(const std::function &get_value) const override; +}; + +class string_concatenation_builtin_functiont final + : public string_insertion_builtin_functiont +{ +public: + string_concatenation_builtin_functiont( + const std::vector &fun_args, + array_poolt &array_pool) + : string_insertion_builtin_functiont(fun_args, array_pool) + { + } + + std::vector eval( + const std::vector &input1_value, + const std::vector &input2_value, + const std::vector &args_value) const override; }; /// String creation from other types From e308bade515ee511e4da66a0093787893ee00fc8 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 12 Mar 2018 16:20:24 +0000 Subject: [PATCH 06/19] Rename class to string_dependenciest --- src/solvers/refinement/string_refinement.cpp | 6 +-- .../refinement/string_refinement_util.cpp | 48 +++++++++---------- .../refinement/string_refinement_util.h | 8 ++-- .../string_refinement/dependency_graph.cpp | 8 ++-- 4 files changed, 35 insertions(+), 35 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index a6f5698ed9e..51a9fcea714 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -680,12 +680,12 @@ decision_proceduret::resultt string_refinementt::dec_solve() #ifdef DEBUG output_equations(debug(), equations, ns); - string_dependencest dependences; + string_dependenciest dependencies; for(const equal_exprt &eq : equations) - add_node(dependences, eq, generator.array_pool); + add_node(dependencies, eq, generator.array_pool); debug() << "dec_solve: dependence graph:" << eom; - dependences.output_dot(debug()); + dependencies.output_dot(debug()); #endif debug() << "dec_solve: Replace function applications" << eom; diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index b509776a10d..f2ff7b63cd2 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -322,8 +322,8 @@ static std::unique_ptr to_string_builtin_function( return {}; } -string_dependencest::string_nodet & -string_dependencest::get_node(const array_string_exprt &e) +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) @@ -333,7 +333,7 @@ string_dependencest::get_node(const array_string_exprt &e) return string_nodes.back(); } -string_dependencest::builtin_function_nodet string_dependencest::make_node( +string_dependenciest::builtin_function_nodet string_dependenciest::make_node( std::unique_ptr &builtin_function) { const builtin_function_nodet builtin_function_node( @@ -343,21 +343,21 @@ string_dependencest::builtin_function_nodet string_dependencest::make_node( return builtin_function_node; } -const string_builtin_functiont &string_dependencest::get_builtin_function( +const string_builtin_functiont &string_dependenciest::get_builtin_function( const builtin_function_nodet &node) const { PRECONDITION(node.index < builtin_function_nodes.size()); return *(builtin_function_nodes[node.index]); } -const std::vector & -string_dependencest::dependencies( - const string_dependencest::string_nodet &node) const +const std::vector & +string_dependenciest::dependencies( + const string_dependenciest::string_nodet &node) const { return node.dependencies; } -void string_dependencest::add_dependency( +void string_dependenciest::add_dependency( const array_string_exprt &e, const builtin_function_nodet &builtin_function_node) { @@ -365,14 +365,14 @@ void string_dependencest::add_dependency( string_node.dependencies.push_back(builtin_function_node); } -void string_dependencest::add_unknown_dependency(const array_string_exprt &e) +void string_dependenciest::add_unknown_dependency(const array_string_exprt &e) { string_nodet &string_node = get_node(e); string_node.depends_on_unknown_builtin_function = true; } static void add_unknown_dependency_to_string_subexprs( - string_dependencest &dependencies, + string_dependenciest &dependencies, const function_application_exprt &fun_app, array_poolt &array_pool) { @@ -392,9 +392,9 @@ static void add_unknown_dependency_to_string_subexprs( } static void add_dependency_to_string_subexprs( - string_dependencest &dependencies, + string_dependenciest &dependencies, const function_application_exprt &fun_app, - const string_dependencest::builtin_function_nodet &builtin_function_node, + const string_dependenciest::builtin_function_nodet &builtin_function_node, array_poolt &array_pool) { PRECONDITION(fun_app.arguments()[0].type().id() != ID_pointer); @@ -424,7 +424,7 @@ static void add_dependency_to_string_subexprs( } } -string_dependencest::node_indext string_dependencest::size() const +string_dependenciest::node_indext string_dependenciest::size() const { return builtin_function_nodes.size() + string_nodes.size(); } @@ -444,28 +444,28 @@ builtin_function_index_to_node_index(const std::size_t builtin_index) return 2 * builtin_index; } -string_dependencest::node_indext -string_dependencest::node_index(const builtin_function_nodet &n) const +string_dependenciest::node_indext +string_dependenciest::node_index(const builtin_function_nodet &n) const { return builtin_function_index_to_node_index(n.index); } -string_dependencest::node_indext -string_dependencest::node_index(const array_string_exprt &s) const +string_dependenciest::node_indext +string_dependenciest::node_index(const array_string_exprt &s) const { return string_index_to_node_index(node_index_pool.at(s)); } -optionalt -string_dependencest::get_builtin_function_node(node_indext i) const +optionalt +string_dependenciest::get_builtin_function_node(node_indext i) const { if(i % 2 == 0) return builtin_function_nodet(i / 2); return {}; } -optionalt -string_dependencest::get_string_node(node_indext i) const +optionalt +string_dependenciest::get_string_node(node_indext i) const { if(i % 2 == 1 && i / 2 < string_nodes.size()) return string_nodes[i / 2]; @@ -473,7 +473,7 @@ string_dependencest::get_string_node(node_indext i) const } bool add_node( - string_dependencest &dependencies, + string_dependenciest &dependencies, const equal_exprt &equation, array_poolt &array_pool) { @@ -505,7 +505,7 @@ bool add_node( return true; } -void string_dependencest::for_each_successor( +void string_dependenciest::for_each_successor( const std::size_t &i, const std::function &f) const { @@ -529,7 +529,7 @@ void string_dependencest::for_each_successor( UNREACHABLE; } -void string_dependencest::output_dot(std::ostream &stream) const +void string_dependenciest::output_dot(std::ostream &stream) const { const auto for_each_node = [&](const std::function &f) { // NOLINT diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h index 04fb07571f7..395ab4e4b47 100644 --- a/src/solvers/refinement/string_refinement_util.h +++ b/src/solvers/refinement/string_refinement_util.h @@ -259,9 +259,9 @@ class string_test_builtin_functiont : public string_builtin_functiont }; /// Keep track of dependencies between strings. -/// Each string points to builtin_function calls on which it depends, -/// each builtin_function points to the strings on which the result depend. -class string_dependencest +/// 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 is just an index in the `builtin_function_nodes` @@ -365,7 +365,7 @@ class string_dependencest /// 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_dependencest &dependencies, + string_dependenciest &dependencies, const equal_exprt &equation, array_poolt &array_pool); diff --git a/unit/solvers/refinement/string_refinement/dependency_graph.cpp b/unit/solvers/refinement/string_refinement/dependency_graph.cpp index d4e9748badb..09c4b075fb0 100644 --- a/unit/solvers/refinement/string_refinement/dependency_graph.cpp +++ b/unit/solvers/refinement/string_refinement/dependency_graph.cpp @@ -47,7 +47,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]") { GIVEN("dependency graph") { - string_dependencest dependences; + string_dependenciest dependences; refined_string_typet string_type(java_char_type(), java_int_type()); const exprt string1 = make_string_argument("string1"); const exprt string2 = make_string_argument("string2"); @@ -142,7 +142,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]") THEN("string3 depends on primitive0") { const auto &node = dependences.get_node(char_array3); - const std::vector + const std::vector &depends = dependences.dependencies(node); REQUIRE(depends.size() == 1); const auto &primitive0 = dependences.get_builtin_function(depends[0]); @@ -159,7 +159,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]") THEN("string5 depends on primitive1") { const auto &node = dependences.get_node(char_array5); - const std::vector + const std::vector &depends = dependences.dependencies(node); REQUIRE(depends.size() == 1); const auto &primitive1 = dependences.get_builtin_function(depends[0]); @@ -176,7 +176,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]") THEN("string6 depends on primitive2") { const auto &node = dependences.get_node(char_array6); - const std::vector + const std::vector &depends = dependences.dependencies(node); REQUIRE(depends.size() == 1); const auto &primitive2 = dependences.get_builtin_function(depends[0]); From 357cb445634943147c7a2bbf66d47bbd49faee69 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Mar 2018 14:39:04 +0000 Subject: [PATCH 07/19] Add const node_at function in string dependencies This is useful to find a node with the guarantee of node modifying the graph. --- src/solvers/refinement/string_refinement_util.cpp | 9 +++++++++ src/solvers/refinement/string_refinement_util.h | 3 +++ 2 files changed, 12 insertions(+) diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index f2ff7b63cd2..0cffa2b1222 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -333,6 +333,15 @@ string_dependenciest::get_node(const array_string_exprt &e) 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) { diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h index 395ab4e4b47..06a4487da43 100644 --- a/src/solvers/refinement/string_refinement_util.h +++ b/src/solvers/refinement/string_refinement_util.h @@ -287,6 +287,9 @@ class string_dependenciest 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); From 69f31c1a185e1006325f61cdb7e57a622ec69040 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Mar 2018 15:23:23 +0000 Subject: [PATCH 08/19] Add eval function to string_dependenciest --- src/solvers/refinement/string_refinement_util.cpp | 15 +++++++++++++++ src/solvers/refinement/string_refinement_util.h | 6 ++++++ 2 files changed, 21 insertions(+) diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index 0cffa2b1222..cc088c20a5b 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -481,6 +481,21 @@ string_dependenciest::get_string_node(node_indext i) const return {}; } +optionalt string_dependenciest::eval( + const array_string_exprt &s, + const std::function &get_value) const +{ + const auto node = node_at(s); + if(node && node->dependencies.size() == 1) + { + const auto &f = get_builtin_function(node->dependencies[0]); + const auto result = f.string_result(); + if(result && *result == s) + return f.eval(get_value); + } + return {}; +} + bool add_node( string_dependenciest &dependencies, const equal_exprt &equation, diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h index 06a4487da43..007d905734b 100644 --- a/src/solvers/refinement/string_refinement_util.h +++ b/src/solvers/refinement/string_refinement_util.h @@ -306,6 +306,12 @@ class string_dependenciest /// Mark node for `e` as depending on unknown builtin_function void add_unknown_dependency(const array_string_exprt &e); + /// Attempt to evaluate the given string from the dependencies and valuation + /// of strings on which it depends + optionalt eval( + const array_string_exprt &s, + const std::function &get_value) const; + void output_dot(std::ostream &stream) const; private: From 56cb57127f7b60ac7996ff326cda6dc429215447 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Mar 2018 14:41:52 +0000 Subject: [PATCH 09/19] Activate dependency computation in string solver This is computed at the beginning of dec_solve. --- src/solvers/refinement/string_refinement.cpp | 5 +++-- src/solvers/refinement/string_refinement.h | 2 ++ 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 51a9fcea714..15f534f2ec1 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -679,12 +679,13 @@ decision_proceduret::resultt string_refinementt::dec_solve() #ifdef DEBUG output_equations(debug(), equations, ns); +#endif - string_dependenciest dependencies; + debug() << "dec_solve: compute dependency graph:" << eom; for(const equal_exprt &eq : equations) add_node(dependencies, eq, generator.array_pool); - debug() << "dec_solve: dependence graph:" << eom; +#ifdef DEBUG dependencies.output_dot(debug()); #endif diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index a0d2a532d2a..281f004da87 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -85,6 +85,8 @@ class string_refinementt final: public bv_refinementt std::vector equations; + string_dependenciest dependencies; + void add_lemma(const exprt &lemma, bool simplify_lemma = true); }; From 44693e80837b495d6b6d60746a255e16b92930e5 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Mar 2018 14:46:05 +0000 Subject: [PATCH 10/19] Use eval of builtin function in get when available When we can find a string in the string dependencies graph and the corresponding function can be evaluated we return that result instead of using get_array. --- src/solvers/refinement/string_refinement.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 15f534f2ec1..6ac7393eead 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -2254,6 +2254,12 @@ exprt string_refinementt::get(const exprt &expr) const { array_string_exprt &arr = to_array_string_expr(ecopy); arr.length() = generator.array_pool.get_length(arr); + + if( + const auto from_dependencies = + dependencies.eval(arr, [&](const exprt &expr) { return get(expr); })) + return *from_dependencies; + const auto arr_model_opt = get_array(super_get, ns, generator.max_string_length, debug(), arr); // \todo Refactor with get array in model From 095d57b75350da9ffa704d5cf2eca00bd45e6528 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 8 Mar 2018 16:52:50 +0000 Subject: [PATCH 11/19] Add concat_char builtin function for strings --- .../refinement/string_refinement_util.cpp | 52 +++++++++++++++++++ .../refinement/string_refinement_util.h | 31 +++++++++++ 2 files changed, 83 insertions(+) diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index cc088c20a5b..e55e3292a8d 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -173,6 +173,44 @@ equation_symbol_mappingt::find_equations(const exprt &expr) return equations_containing[expr]; } +string_transformation_builtin_functiont:: + string_transformation_builtin_functiont( + const std::vector &fun_args, + array_poolt &array_pool) +{ + PRECONDITION(fun_args.size() > 2); + const auto arg1 = expr_checked_cast(fun_args[2]); + input = array_pool.find(arg1.op1(), arg1.op0()); + result = array_pool.find(fun_args[1], fun_args[0]); + args.insert(args.end(), fun_args.begin() + 3, fun_args.end()); +} + +optionalt string_transformation_builtin_functiont::eval( + const std::function &get_value) const +{ + const auto &input_value = eval_string(input, get_value); + if(!input_value.has_value()) + return {}; + + std::vector arg_values; + const auto &insert = std::back_inserter(arg_values); + const mp_integer unknown('?'); + std::transform( + args.begin(), args.end(), insert, [&](const exprt &e) { // NOLINT + if(const auto val = numeric_cast(get_value(e))) + return *val; + INVARIANT( + get_value(e).id() == ID_unknown, + "array valuation should only contain constants and unknown"); + return unknown; + }); + + const auto result_value = eval(*input_value, arg_values); + const auto length = from_integer(result_value.size(), result.length().type()); + const array_typet type(result.type().subtype(), length); + return make_string(result_value, type); +} + string_insertion_builtin_functiont::string_insertion_builtin_functiont( const std::vector &fun_args, array_poolt &array_pool) @@ -254,6 +292,16 @@ std::vector string_concatenation_builtin_functiont::eval( return result; } +std::vector string_concat_char_builtin_functiont::eval( + const std::vector &input_value, + const std::vector &args_value) const +{ + PRECONDITION(args_value.size() == 1); + std::vector result(input_value); + result.push_back(args_value[0]); + return result; +} + std::vector string_insertion_builtin_functiont::eval( const std::vector &input1_value, const std::vector &input2_value, @@ -319,6 +367,10 @@ static std::unique_ptr to_string_builtin_function( return util_make_unique( fun_app.arguments(), array_pool); + if(id == ID_cprover_string_concat_char_func) + return util_make_unique( + fun_app.arguments(), array_pool); + return {}; } diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h index 007d905734b..d23c03fb690 100644 --- a/src/solvers/refinement/string_refinement_util.h +++ b/src/solvers/refinement/string_refinement_util.h @@ -170,6 +170,12 @@ class string_transformation_builtin_functiont : public string_builtin_functiont array_string_exprt input; std::vector args; exprt return_code; + + /// Constructor from arguments of a function application + string_transformation_builtin_functiont( + const std::vector &fun_args, + array_poolt &array_pool); + optionalt string_result() const override { return result; @@ -178,6 +184,31 @@ class string_transformation_builtin_functiont : public string_builtin_functiont { return {input}; } + + /// Evaluate the result from a concrete valuation of the arguments + virtual std::vector eval( + const std::vector &input_value, + const std::vector &args_value) const = 0; + + optionalt + eval(const std::function &get_value) const override; +}; + +/// Adding a character at the end of a string +class string_concat_char_builtin_functiont + : public string_transformation_builtin_functiont +{ +public: + string_concat_char_builtin_functiont( + const std::vector &fun_args, + array_poolt &array_pool) + : string_transformation_builtin_functiont(fun_args, array_pool) + { + } + + std::vector eval( + const std::vector &input_value, + const std::vector &args_value) const override; }; /// String inserting a string into another one From fb676d54d1c284d8fa93a153237410f7fbf607d6 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 8 Mar 2018 16:54:03 +0000 Subject: [PATCH 12/19] Add a cache for eval in string dependences This improves the performances since the model for one string can depend on the model for two other strings, which model may have already been computed. The cache must be cleared every time the model changes. --- src/solvers/refinement/string_refinement.cpp | 2 ++ .../refinement/string_refinement_util.cpp | 27 ++++++++++++++++--- .../refinement/string_refinement_util.h | 7 +++++ 3 files changed, 32 insertions(+), 4 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 6ac7393eead..b994d73b16c 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -757,6 +757,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() // Initial try without index set const auto get = [this](const exprt &expr) { return this->get(expr); }; + dependencies.clean_cache(); const decision_proceduret::resultt res=supert::dec_solve(); if(res==resultt::D_SATISFIABLE) { @@ -804,6 +805,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() while((loop_bound_--)>0) { + dependencies.clean_cache(); const decision_proceduret::resultt res=supert::dec_solve(); if(res==resultt::D_SATISFIABLE) diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index e55e3292a8d..6cea38e4c19 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -537,17 +537,36 @@ optionalt string_dependenciest::eval( const array_string_exprt &s, const std::function &get_value) const { - const auto node = node_at(s); - if(node && node->dependencies.size() == 1) + 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]; + + if(node.dependencies.size() == 1) { - const auto &f = get_builtin_function(node->dependencies[0]); + const auto &f = get_builtin_function(node.dependencies[0]); const auto result = f.string_result(); if(result && *result == s) - return f.eval(get_value); + { + const auto value_opt = f.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, diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h index d23c03fb690..e8c18ad3cf6 100644 --- a/src/solvers/refinement/string_refinement_util.h +++ b/src/solvers/refinement/string_refinement_util.h @@ -339,10 +339,15 @@ class string_dependenciest /// 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; private: @@ -352,6 +357,8 @@ class string_dependenciest /// Set of nodes representing strings std::vector string_nodes; + mutable std::vector> eval_string_cache; + /// Nodes describing dependencies of a string: values of the map correspond /// to indexes in the vector `string_nodes`. std::unordered_map From 0b3796ebe6584853a9828792e12ee5062a31b1c5 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 9 Mar 2018 15:07:42 +0000 Subject: [PATCH 13/19] Declare a nodet class in string_dependencies This make it more convenient to reuse graph function, rather than using a common index for two tables. --- .../refinement/string_refinement_util.cpp | 118 ++++++------------ .../refinement/string_refinement_util.h | 63 +++++----- 2 files changed, 73 insertions(+), 108 deletions(-) diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index 6cea38e4c19..b4d89996b3b 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -381,7 +381,7 @@ string_dependenciest::get_node(const array_string_exprt &e) if(!entry_inserted.second) return string_nodes[entry_inserted.first->second]; - string_nodes.emplace_back(); + string_nodes.emplace_back(e, entry_inserted.first->second); return string_nodes.back(); } @@ -485,54 +485,6 @@ static void add_dependency_to_string_subexprs( } } -string_dependenciest::node_indext string_dependenciest::size() const -{ - return builtin_function_nodes.size() + string_nodes.size(); -} - -/// Convert an index of a string node in `string_nodes` to the node_indext for -/// the same node -static std::size_t string_index_to_node_index(const std::size_t string_index) -{ - return 2 * string_index + 1; -} - -/// Convert an index of a builtin function node to the node_indext for -/// the same node -static std::size_t -builtin_function_index_to_node_index(const std::size_t builtin_index) -{ - return 2 * builtin_index; -} - -string_dependenciest::node_indext -string_dependenciest::node_index(const builtin_function_nodet &n) const -{ - return builtin_function_index_to_node_index(n.index); -} - -string_dependenciest::node_indext -string_dependenciest::node_index(const array_string_exprt &s) const -{ - return string_index_to_node_index(node_index_pool.at(s)); -} - -optionalt -string_dependenciest::get_builtin_function_node(node_indext i) const -{ - if(i % 2 == 0) - return builtin_function_nodet(i / 2); - return {}; -} - -optionalt -string_dependenciest::get_string_node(node_indext i) const -{ - if(i % 2 == 1 && i / 2 < string_nodes.size()) - return string_nodes[i / 2]; - return {}; -} - optionalt string_dependenciest::eval( const array_string_exprt &s, const std::function &get_value) const @@ -601,50 +553,58 @@ bool add_node( } void string_dependenciest::for_each_successor( - const std::size_t &i, - const std::function &f) const + const nodet &node, + const std::function &f) const { - if(const auto &builtin_function_node = get_builtin_function_node(i)) + if(node.kind == nodet::BUILTIN) { - const string_builtin_functiont &p = - get_builtin_function(*builtin_function_node); - std::for_each( - p.string_arguments().begin(), - p.string_arguments().end(), - [&](const array_string_exprt &s) { f(node_index(s)); }); + const auto &builtin = builtin_function_nodes[node.index]; + for(const auto &s : builtin->string_arguments()) + { + if(const auto node = node_at(s)) + f(nodet(*node)); + } } - else if(const auto &s = get_string_node(i)) + else if(node.kind == nodet::STRING) { + const auto &s_node = string_nodes[node.index]; std::for_each( - s->dependencies.begin(), - s->dependencies.end(), - [&](const builtin_function_nodet &p) { f(node_index(p)); }); + s_node.dependencies.begin(), + s_node.dependencies.end(), + [&](const builtin_function_nodet &p) { f(nodet(p)); }); } else UNREACHABLE; } +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_nodet(i))); +} + void string_dependenciest::output_dot(std::ostream &stream) const { - const auto for_each_node = - [&](const std::function &f) { // NOLINT - for(std::size_t i = 0; i < string_nodes.size(); ++i) - f(string_index_to_node_index(i)); - for(std::size_t i = 0; i < builtin_function_nodes.size(); ++i) - f(builtin_function_index_to_node_index(i)); + const auto for_each = + [&](const std::function &f) { // NOLINT + for_each_node(f); }; - - const auto for_each_succ = [&]( - const std::size_t &i, - const std::function &f) { // NOLINT - for_each_successor(i, f); - }; - - const auto node_to_string = [&](const std::size_t &i) { // NOLINT - return std::to_string(i); + 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_" << n.index; + else + ostream << '"' << format(string_nodes[n.index].expr) << '"'; + return ostream.str(); }; stream << "digraph dependencies {\n"; - output_dot_generic( - stream, for_each_node, for_each_succ, node_to_string); + output_dot_generic(stream, for_each, for_each_succ, node_to_string); stream << '}' << std::endl; } diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h index e8c18ad3cf6..1008d029c04 100644 --- a/src/solvers/refinement/string_refinement_util.h +++ b/src/solvers/refinement/string_refinement_util.h @@ -310,10 +310,19 @@ class string_dependenciest 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 std::vector dependencies; - // In case it depends on a builtin_function we don't support yet bool depends_on_unknown_builtin_function = false; + + 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); @@ -357,45 +366,41 @@ class string_dependenciest /// Set of nodes representing strings std::vector string_nodes; - mutable std::vector> eval_string_cache; - /// Nodes describing dependencies of a string: values of the map correspond /// to indexes in the vector `string_nodes`. std::unordered_map node_index_pool; - /// Common index for all nodes (both strings and builtin_functions) so that we - /// can reuse generic algorithms of util/graph.h - /// Even indexes correspond to builtin_function nodes, odd indexes to string - /// nodes. - typedef std::size_t node_indext; - - /// \return total number of nodes - node_indext size() const; + class nodet + { + public: + enum + { + BUILTIN, + STRING + } kind; + std::size_t index; - /// \param n: builtin function node - /// \return index corresponding to builtin function node `n` - node_indext node_index(const builtin_function_nodet &n) const; + explicit nodet(const builtin_function_nodet &builtin) + : kind(BUILTIN), index(builtin.index) + { + } - /// \param s: array expression representing a string - /// \return index corresponding to an string exprt s - node_indext node_index(const array_string_exprt &s) const; + explicit nodet(const string_nodet &string_node) + : kind(STRING), index(string_node.index) + { + } + }; - /// \param i: index of a node - /// \return corresponding node if the index corresponds to a builtin function - /// node, empty optional otherwise - optionalt - get_builtin_function_node(node_indext i) const; + mutable std::vector> eval_string_cache; - /// \param i: index of a node - /// \return corresponding node if the index corresponds to a string - /// node, empty optional otherwise - optionalt get_string_node(node_indext i) const; + /// Applies `f` on all nodes + void for_each_node(const std::function &f) const; - /// Applies `f` on all successors of the node with index `i` + /// Applies `f` on all successors of the node n void for_each_successor( - const node_indext &i, - const std::function &f) const; + const nodet &i, + const std::function &f) const; }; /// When right hand side of equation is a builtin_function add From a89ceb07d7238bd8913f577c50d8fa9283e12a79 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 8 Mar 2018 09:41:14 +0000 Subject: [PATCH 14/19] Tests for string solver get with new dependencies --- .../jbmc-strings/StringConcat/Test.class | Bin 0 -> 5246 bytes .../jbmc-strings/StringConcat/Test.java | 315 ++++++++++++++++++ .../StringConcat/test_buffer_det.desc | 11 + .../StringConcat/test_buffer_nondet_loop.desc | 14 + .../test_buffer_nondet_loop2.desc | 11 + .../test_buffer_nondet_loop3.desc | 11 + .../test_buffer_nondet_loop4.desc | 14 + .../test_buffer_nondet_loop5.desc | 11 + .../StringConcat/test_char_buffer_det.desc | 11 + .../test_char_buffer_det_loop.desc | 11 + .../test_char_buffer_det_loop2.desc | 11 + .../StringConcat/test_string_det.desc | 11 + .../StringConcat/test_string_nondet.desc | 11 + 13 files changed, 442 insertions(+) create mode 100644 regression/jbmc-strings/StringConcat/Test.class create mode 100644 regression/jbmc-strings/StringConcat/Test.java create mode 100644 regression/jbmc-strings/StringConcat/test_buffer_det.desc create mode 100644 regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc create mode 100644 regression/jbmc-strings/StringConcat/test_buffer_nondet_loop2.desc create mode 100644 regression/jbmc-strings/StringConcat/test_buffer_nondet_loop3.desc create mode 100644 regression/jbmc-strings/StringConcat/test_buffer_nondet_loop4.desc create mode 100644 regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5.desc create mode 100644 regression/jbmc-strings/StringConcat/test_char_buffer_det.desc create mode 100644 regression/jbmc-strings/StringConcat/test_char_buffer_det_loop.desc create mode 100644 regression/jbmc-strings/StringConcat/test_char_buffer_det_loop2.desc create mode 100644 regression/jbmc-strings/StringConcat/test_string_det.desc create mode 100644 regression/jbmc-strings/StringConcat/test_string_nondet.desc diff --git a/regression/jbmc-strings/StringConcat/Test.class b/regression/jbmc-strings/StringConcat/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..7600fbe19d0fec393e7b41d7581e25a5b10474fc GIT binary patch literal 5246 zcmd6rdvH`|8OEPCdplV+u)En!ve_hD3klhf$|YPvQy@Sa8Ym^SDPWP!?j|gRByNJz zQrpq4w%TF5P%nT*2`EyvQnkS;mMU1Cf?7xZu%kn3tJXS7i@m7DP4M~7Ih$mY9U7~D zl*~Ebp7*<+-}}7p_Z`j-JaG!ZT(mkd5p^1_cVLMV7SyTRQVq*gS+8Nah7}rCYPdne zjT#y>tkQ6khDHsmHLS@+DQ;1!{-_tW&pob!*bF-icdrn*+^G+>Q+n zY!u{A3wL+N5h^F)TXmCOQ7g!6>Ip}-uMT(VT^!gXa2dVU zbav<+r?EuEje;zYdEniZ4!7go*O$my9EC7hO9$*N41?TC@62p z-r8+UY%JIqct&}{7+38X*_ktqvds~cbM|*Tu$U zBC(Zm-RbLN-959Et6i9asZ>l@P&m@{%XY@wqp^ew@5dc%(&EBq%;1j*FQqc7M_PHc z@!HBO&TAX5?Y!D~?QmfdCJTy&240$0>xx98GeLh1RT*+K#Gt19fVyoFfP!-&j24Pm zE!%;J3sG=#_fY4XTeig_RPZp9F&+aU+|?E9;CidZBvSLGDSNG_Gd)IVj9rzs*)v#P zKU%WJo3Ym39_wi9AuvW}14DA?E$Z7D&4dz-b;lF2=pZb{U(Zffu){`7X0DjXq$BPk zg_pnbAj*rpPvcW5OHzYv<_XASsv)l7-L4x|)pX3@olPZ-9R5Kp-kiphuxvO1Yh@p7 zUOR7naAerDEVkS%HfI*wxGXkT7F%8x+xRTD30Z9JEH+OTo7c2`7y0`!?j(GCYyVS~ z$B8IM2UUj&{B334wxN*NDk;G0p`i)6XoC~GF%F-G3x~=51jgeW+rI!e-hfw_kWtRw z8YCs+Km|e1(EHnh2&DiEiOP-#i&CN>rjGLD)~;7VGq@Qh)RE) zT7QN*zd)s5qNfHZ^GFs)8I< z@m_6`36NL=Lk#aCBaoa%olQW99IHrf76ZJRmiJ*c{}y5nmhhNz1Lk23=JOb_fXQ_s zB3OiNsKp0y9d?oYy;S-q*m4h+;vv-I0G6W{D{u@eah$zRpaG|_3QyxEoJZpj|ML#c zDx5W)T1NAChx<_6T`o5=qT)@)Wg9Qkh{|1kMS$UjQ{G4gLE|2FcElm9mI-%kGR(P_uWP@$tZM}1#Qu~(xm0eLF9$pdd1NzubaOHJLugrp)u7B6YV-4bb${u#qJ`w zJDEQ3VzS-MFu$7;+D$QigmS%y(!3YT@KMU{V_1v(h&4%sA19{!iR1wy_#}INioYJz zVdTTE^}|gy%4OuIFkReJNJK?}o`Z9$$i>bayf}Cej*^FmqghjBqN%a^tp=Pb6ONT| zUNx($3^-K=oGODsl{*bbbxv9p9<%D`mA?-*(s>RJU^t@2=C=jui1b`G&UGnsE{keY z(u-9iC)J}TXpfG0(xe)_Z}3Ic)Vd0WPd?&BGu=qB40Ge7R5-XBYWNIy#m{p0`y4a) zUS{Wqn2Gk1`sbYJ_E`{%l1&_;k^ogHk z5GP~`ejpWiLgwS7E)ix)EvFwILnFQvkF=f?%BUA_3T~O`xs2iza{25FQZ#d@Lu31% zq#p@@-k^2_Uh27oZgZ+~|Nl)!9IdE1sKy+-Pp{@6BhH>;wEc+j^(*elFe ze_?KViNWz#2Eawi`Bj}>5V?67^a>?~V)49-ixdOtC5oQ zl%Uc^z{-#;YSsh$QszqqtQo;t#)B;II*+k$z=Jm#sBiH|^(OP}Kk2uB=_|{Fr5`>c zG`#A&V!_~A4w??-SAl+_T4c5AX-VY|PkLGUGA_Q0#ZBk3fPeFzqFDQR{!8(!H^BUI zg;`_(3nT|C8Qbc_=Yy>uE@P4Y6mnGPs9#}_Tve_=H<|km ztKwUA@p~w}EPas&`1D^cZiE1B83H`b(+R`@n`qF)36G3JKwQkdd6>zZJ)7kMnSdqY z#*N~^TJd6o1!fN>*^3`X%@im(MY*)IsA;+~ueZeo*tFQYHa>0wT literal 0 HcmV?d00001 diff --git a/regression/jbmc-strings/StringConcat/Test.java b/regression/jbmc-strings/StringConcat/Test.java new file mode 100644 index 00000000000..74f91b81df0 --- /dev/null +++ b/regression/jbmc-strings/StringConcat/Test.java @@ -0,0 +1,315 @@ +public class Test { + + public String stringDet() { + String s = "a"; + s += "b"; + s += "c"; + s += "d"; + s += "e"; + s += "f"; + s += "g"; + s += "h"; + s += "i"; + s += "j"; + s += "k"; + s += "l"; + s += "m"; + + assert(false); + return s; + } + + public String stringNonDet(String arg) { + String s = arg; + s += "b"; + s += "c"; + s += "d"; + s += "e"; + s += "f"; + s += arg; + s += "h"; + s += "i"; + s += "j"; + s += "k"; + s += "l"; + s += arg; + + assert(false); + return s; + } + + public String bufferDet() { + StringBuffer s = new StringBuffer(); + s.append("a"); + s.append("b"); + s.append("c"); + s.append("d"); + s.append("e"); + + s.append("a"); + s.append("b"); + s.append("c"); + s.append("d"); + s.append("e"); + + s.append("a"); + s.append("b"); + s.append("c"); + s.append("d"); + s.append("e"); + + s.append("a"); + s.append("b"); + s.append("c"); + s.append("d"); + s.append("e"); + + s.append("a"); + s.append("b"); + s.append("c"); + s.append("d"); + s.append("e"); + + s.append("a"); + s.append("b"); + assert(false); + return s.toString(); + } + + public String charBufferDet() { + StringBuffer s = new StringBuffer(); + s.append('a'); + s.append('b'); + s.append('c'); + s.append('d'); + s.append('e'); + + s.append('a'); + s.append('b'); + s.append('c'); + s.append('d'); + s.append('e'); + + s.append('a'); + s.append('b'); + s.append('c'); + s.append('d'); + s.append('e'); + + s.append('a'); + s.append('b'); + s.append('c'); + s.append('d'); + s.append('e'); + + s.append('a'); + s.append('b'); + s.append('c'); + s.append('d'); + s.append('e'); + + s.append('a'); + s.append('b'); + + assert(false); + return s.toString(); + } + + public String charBufferDetLoop(int width) { + if(width <= 5) + return ""; + StringBuffer sb = new StringBuffer(); + sb.append('+'); + for(int i=1; i < width-1; ++i) + sb.append('-'); + sb.append('+'); + sb.append('\n'); + sb.append('|'); + + sb.append(' '); + sb.append('c'); + int padding = width - 2; + while(padding-- > 0) + sb.append(' '); + + sb.append(' '); + sb.append('|'); + sb.append('\n'); + assert(false); + return sb.toString(); + } + + public String charBufferDetLoop2(int width, int height) { + if(width <= 0 || height <= 0) + return ""; + StringBuffer sb = new StringBuffer(); + sb.append('+'); + for(int i=1; i < width-1; ++i) + sb.append('-'); + sb.append('+'); + sb.append('\n'); + sb.append('|'); + + sb.append(' '); + sb.append('c'); + int padding = width - 2; + while(padding-- > 0) + sb.append(' '); + sb.append(' '); + sb.append('|'); + sb.append('\n'); + + sb.append('+'); + for(int i=1; i 0) + sb.append(' '); + sb.append(' '); + sb.append('|'); + sb.append('\n'); + } + + sb.append('+'); + for(int i=1; i= width || s.length() == 0) + return ""; + StringBuffer sb = new StringBuffer(); + sb.append('+'); + for(int i=1; i < width-1; ++i) + sb.append('-'); + sb.append('+'); + sb.append('\n'); + sb.append('|'); + + sb.append(' '); + sb.append(s); + int padding = width - s.length(); + while(padding-- > 0) + sb.append(' '); + sb.append(' '); + sb.append('|'); + sb.append('\n'); + + assert(false); + return sb.toString(); + } + + public String bufferNonDetLoop2(int width, String c) { + if(width < 5 || c.length() > width) + return ""; + + StringBuffer sb = new StringBuffer(); + sb.append('+'); + + for(int i=1; i 0) + sb.append(' '); + sb.append(' '); + sb.append('|'); + } + sb.append('\n'); + + assert(false); + return sb.toString(); + } + + public String bufferNonDetLoop3(int cols, int columnWidth, String c) { + StringBuffer sb = new StringBuffer(); + sb.append('-'); + for(int i = 0; i < cols; ++i) + sb.append(c); + + assert(false); + return sb.toString(); + } + public String bufferNonDetLoop4(int cols, int columnWidth, String c) { + StringBuffer sb = new StringBuffer(); + for(int i=1; i < columnWidth-1; ++i) + sb.append('-'); + for(int i = 0; i < cols; ++i) { + sb.append(c); + } + + assert(false); + return sb.toString(); + } + + public String bufferNonDetLoop5(int cols, int columnWidth, String c, String data[]) { + if(cols<1) + return ""; + + StringBuffer sb = new StringBuffer(); + sb.append('+'); + int totalWidth = columnWidth * cols; + for(int i=1; i 0) + sb.append(' '); + sb.append(' '); + sb.append('|'); + } + sb.append('\n'); + + sb.append('+'); + for(int i=1; i 0) + sb.append(' '); + sb.append(' '); + sb.append('|'); + + if(i % cols == 0) + sb.append('\n'); + } + + sb.append('+'); + for(int i=1; i Date: Fri, 9 Mar 2018 17:43:54 +0000 Subject: [PATCH 15/19] Make node point to builtin func they result from This make finding the function the string results from easier. --- .../refinement/string_refinement_util.cpp | 21 ++++++++++--------- .../refinement/string_refinement_util.h | 2 ++ 2 files changed, 13 insertions(+), 10 deletions(-) diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index b4d89996b3b..62254c8aabb 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -497,17 +497,14 @@ optionalt string_dependenciest::eval( return eval_string_cache[it->second]; const auto node = string_nodes[it->second]; - - if(node.dependencies.size() == 1) + const auto &f = node.result_from; + if( + f && node.dependencies.size() == 1 && + !node.depends_on_unknown_builtin_function) { - const auto &f = get_builtin_function(node.dependencies[0]); - const auto result = f.string_result(); - if(result && *result == s) - { - const auto value_opt = f.eval(get_value); - eval_string_cache[it->second] = value_opt; - return value_opt; - } + const auto value_opt = get_builtin_function(*f).eval(get_value); + eval_string_cache[it->second] = value_opt; + return value_opt; } return {}; } @@ -544,7 +541,11 @@ bool add_node( 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; + } else add_dependency_to_string_subexprs( dependencies, *fun_app, builtin_function_node, array_pool); diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h index 1008d029c04..e9ad2988f5f 100644 --- a/src/solvers/refinement/string_refinement_util.h +++ b/src/solvers/refinement/string_refinement_util.h @@ -316,6 +316,8 @@ class string_dependenciest std::size_t index; // builtin functions on which it depends std::vector dependencies; + // builtin function of which it is the result + optionalt result_from; // In case it depends on a builtin_function we don't support yet bool depends_on_unknown_builtin_function = false; From d0a8868825d63839cf57aa22050185f80a49cd1c Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 12 Mar 2018 16:38:47 +0000 Subject: [PATCH 16/19] Constructor and destructor of builtin functions Mark empty constructor as protected and define destructor as virtual default. --- src/solvers/refinement/string_refinement_util.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h index e9ad2988f5f..2e59647f5bb 100644 --- a/src/solvers/refinement/string_refinement_util.h +++ b/src/solvers/refinement/string_refinement_util.h @@ -145,8 +145,8 @@ class equation_symbol_mappingt class string_builtin_functiont { public: - string_builtin_functiont() = default; string_builtin_functiont(const string_builtin_functiont &) = delete; + virtual ~string_builtin_functiont() = default; virtual optionalt string_result() const { @@ -160,6 +160,9 @@ class string_builtin_functiont virtual optionalt eval(const std::function &get_value) const = 0; + +protected: + string_builtin_functiont() = default; }; /// String builtin_function transforming one string into another From cb72bb79a986298e8a8b381c37e3394898f40361 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 12 Mar 2018 17:04:11 +0000 Subject: [PATCH 17/19] Correct insert builtin function construction The arguments were not in the right order. We also need to seperate construction of concatenation since it was using insertion. --- .../refinement/string_refinement_util.cpp | 16 +++++++++++++++- src/solvers/refinement/string_refinement_util.h | 8 ++++---- 2 files changed, 19 insertions(+), 5 deletions(-) diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index 62254c8aabb..faa7e782a7e 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -215,7 +215,21 @@ string_insertion_builtin_functiont::string_insertion_builtin_functiont( const std::vector &fun_args, array_poolt &array_pool) { - PRECONDITION(fun_args.size() > 3); + PRECONDITION(fun_args.size() > 4); + const auto arg1 = expr_checked_cast(fun_args[2]); + input1 = array_pool.find(arg1.op1(), arg1.op0()); + const auto arg2 = expr_checked_cast(fun_args[4]); + input2 = array_pool.find(arg2.op1(), arg2.op0()); + result = array_pool.find(fun_args[1], fun_args[0]); + args.push_back(fun_args[3]); + args.insert(args.end(), fun_args.begin() + 5, fun_args.end()); +} + +string_concatenation_builtin_functiont::string_concatenation_builtin_functiont( + const std::vector &fun_args, + array_poolt &array_pool) +{ + PRECONDITION(fun_args.size() >= 4 && fun_args.size() <= 6); const auto arg1 = expr_checked_cast(fun_args[2]); input1 = array_pool.find(arg1.op1(), arg1.op0()); const auto arg2 = expr_checked_cast(fun_args[3]); diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h index 2e59647f5bb..6d158e77c56 100644 --- a/src/solvers/refinement/string_refinement_util.h +++ b/src/solvers/refinement/string_refinement_util.h @@ -246,6 +246,9 @@ class string_insertion_builtin_functiont : public string_builtin_functiont optionalt eval(const std::function &get_value) const override; + +protected: + string_insertion_builtin_functiont() = default; }; class string_concatenation_builtin_functiont final @@ -254,10 +257,7 @@ class string_concatenation_builtin_functiont final public: string_concatenation_builtin_functiont( const std::vector &fun_args, - array_poolt &array_pool) - : string_insertion_builtin_functiont(fun_args, array_pool) - { - } + array_poolt &array_pool); std::vector eval( const std::vector &input1_value, From 8d4a0573dd814cfc556d2f6108448d7f110ad147 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 13 Mar 2018 08:17:22 +0000 Subject: [PATCH 18/19] Decompose if_expr when adding dependencies We add the dependencies on atomic string expressions, instead of the if_expr directly. --- .../refinement/string_refinement_util.cpp | 18 ++++++++++++++++++ .../refinement/string_refinement_util.h | 4 +++- 2 files changed, 21 insertions(+), 1 deletion(-) diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index faa7e782a7e..1899a9ad7ec 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -436,12 +436,30 @@ void string_dependenciest::add_dependency( const array_string_exprt &e, const builtin_function_nodet &builtin_function_node) { + if(e.id() == ID_if) + { + const auto if_expr = to_if_expr(e); + const auto &true_case = to_array_string_expr(if_expr.true_case()); + const auto &false_case = to_array_string_expr(if_expr.false_case()); + add_dependency(true_case, builtin_function_node); + add_dependency(false_case, builtin_function_node); + return; + } string_nodet &string_node = get_node(e); string_node.dependencies.push_back(builtin_function_node); } void string_dependenciest::add_unknown_dependency(const array_string_exprt &e) { + if(e.id() == ID_if) + { + const auto if_expr = to_if_expr(e); + const auto &true_case = to_array_string_expr(if_expr.true_case()); + const auto &false_case = to_array_string_expr(if_expr.false_case()); + add_unknown_dependency(true_case); + add_unknown_dependency(false_case); + return; + } string_nodet &string_node = get_node(e); string_node.depends_on_unknown_builtin_function = true; } diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h index 6d158e77c56..9497fcf6c8c 100644 --- a/src/solvers/refinement/string_refinement_util.h +++ b/src/solvers/refinement/string_refinement_util.h @@ -343,7 +343,9 @@ class string_dependenciest const string_builtin_functiont & get_builtin_function(const builtin_function_nodet &node) const; - /// Add edge from node for `e` to node for `builtin_function` + /// 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); From 1a874b3cc41b45ec10627545648e7d8cdb169a7e Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 13 Mar 2018 08:21:23 +0000 Subject: [PATCH 19/19] Add name method to builtin functions This is useful to make the dot output more informative. --- .../refinement/string_refinement_util.cpp | 2 +- src/solvers/refinement/string_refinement_util.h | 17 +++++++++++++++++ 2 files changed, 18 insertions(+), 1 deletion(-) diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index 1899a9ad7ec..236847659a0 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -632,7 +632,7 @@ void string_dependenciest::output_dot(std::ostream &stream) const const auto node_to_string = [&](const nodet &n) { // NOLINT std::stringstream ostream; if(n.kind == nodet::BUILTIN) - ostream << "builtin_" << n.index; + ostream << builtin_function_nodes[n.index]->name() << n.index; else ostream << '"' << format(string_nodes[n.index].expr) << '"'; return ostream.str(); diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h index 9497fcf6c8c..b6e7a7880ee 100644 --- a/src/solvers/refinement/string_refinement_util.h +++ b/src/solvers/refinement/string_refinement_util.h @@ -161,6 +161,8 @@ class string_builtin_functiont virtual optionalt eval(const std::function &get_value) const = 0; + virtual std::string name() const = 0; + protected: string_builtin_functiont() = default; }; @@ -212,6 +214,11 @@ class string_concat_char_builtin_functiont std::vector eval( const std::vector &input_value, const std::vector &args_value) const override; + + std::string name() const override + { + return "concat_char"; + } }; /// String inserting a string into another one @@ -247,6 +254,11 @@ class string_insertion_builtin_functiont : public string_builtin_functiont optionalt eval(const std::function &get_value) const override; + std::string name() const override + { + return "insert"; + } + protected: string_insertion_builtin_functiont() = default; }; @@ -263,6 +275,11 @@ class string_concatenation_builtin_functiont final const std::vector &input1_value, const std::vector &input2_value, const std::vector &args_value) const override; + + std::string name() const override + { + return "concat"; + } }; /// String creation from other types