From 1e567fbe4c87db82b2864f5cb24a1a4d18763714 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 30 May 2017 11:56:49 +0100 Subject: [PATCH 1/4] Add an add_axioms_for_concat_substr function Implements the concatenation of a substring of the second argument. This will make the encoding of StringBuilder.append(CharSequence s, int start, int end) more efficient. Part of test-gen/#256 --- .../refinement/string_constraint_generator.h | 5 ++ .../string_constraint_generator_concat.cpp | 78 +++++++++++++------ 2 files changed, 60 insertions(+), 23 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 533e41a4212..447bfd5f6f0 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -145,6 +145,11 @@ class string_constraint_generatort string_exprt add_axioms_for_copy(const function_application_exprt &f); string_exprt add_axioms_for_concat( const string_exprt &s1, const string_exprt &s2); + string_exprt add_axioms_for_concat_substr( + const string_exprt &s1, + const string_exprt &s2, + const exprt &start_index, + const exprt &end_index); string_exprt add_axioms_for_concat(const function_application_exprt &f); string_exprt add_axioms_for_concat_int(const function_application_exprt &f); string_exprt add_axioms_for_concat_long(const function_application_exprt &f); diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp index 311427ec771..e14cbcc58ad 100644 --- a/src/solvers/refinement/string_constraint_generator_concat.cpp +++ b/src/solvers/refinement/string_constraint_generator_concat.cpp @@ -14,53 +14,85 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include /// add axioms to say that the returned string expression is equal to the -/// concatenation of the two string expressions given as input -/// \par parameters: two string expressions +/// concatenation of s1 with the substring of s2 starting at index start_index +/// and ending at index end_index. If start_index >= end_index, the value +/// returned is s1. If end_index > |s2| and/or start_index < 0, the appended +/// string will be of length end_index - start_index and padded with non- +/// deterministic values. +/// \param s1: string expression +/// \param s2: string expression +/// \param start_index: expression representing an integer +/// \param end_index: expression representing an integer /// \return a new string expression -string_exprt string_constraint_generatort::add_axioms_for_concat( - const string_exprt &s1, const string_exprt &s2) +string_exprt string_constraint_generatort::add_axioms_for_concat_substr( + const string_exprt &s1, + const string_exprt &s2, + const exprt &start_index, + const exprt &end_index) { const refined_string_typet &ref_type=to_refined_string_type(s1.type()); string_exprt res=fresh_string(ref_type); // We add axioms: - // a1 : |res|=|s1|+|s2| - // a2 : |s1| <= |res| (to avoid overflow with very long strings) - // a3 : |s2| <= |res| (to avoid overflow with very long strings) - // a4 : forall i<|s1|. res[i]=s1[i] - // a5 : forall i<|s2|. res[i+|s1|]=s2[i] - - equal_exprt a1( - res.length(), plus_exprt_with_overflow_check(s1.length(), s2.length())); + // a1 : end_index > start_index => |res|=|s1|+ end_index - start_index + // a2 : end_index <= start_index => res = s1 + // a3 : forall i<|s1|. res[i]=s1[i] + // a4 : forall i< end_index - start_index. res[i+|s1|]=s2[start_index+i] + + binary_relation_exprt prem(end_index, ID_gt, start_index); + + exprt res_length=plus_exprt_with_overflow_check( + s1.length(), minus_exprt(end_index, start_index)); + implies_exprt a1(prem, equal_exprt(res.length(), res_length)); axioms.push_back(a1); - axioms.push_back(s1.axiom_for_is_shorter_than(res)); - axioms.push_back(s2.axiom_for_is_shorter_than(res)); + + implies_exprt a2(not_exprt(prem), equal_exprt(res.length(), s1.length())); + axioms.push_back(a2); symbol_exprt idx=fresh_univ_index("QA_index_concat", res.length().type()); - string_constraintt a4(idx, s1.length(), equal_exprt(s1[idx], res[idx])); - axioms.push_back(a4); + string_constraintt a3(idx, s1.length(), equal_exprt(s1[idx], res[idx])); + axioms.push_back(a3); symbol_exprt idx2=fresh_univ_index("QA_index_concat2", res.length().type()); - equal_exprt res_eq(s2[idx2], res[plus_exprt(idx2, s1.length())]); - string_constraintt a5(idx2, s2.length(), res_eq); - axioms.push_back(a5); + equal_exprt res_eq( + res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start_index, idx2)]); + string_constraintt a4(idx2, minus_exprt(end_index, start_index), res_eq); + axioms.push_back(a4); return res; } /// add axioms to say that the returned string expression is equal to the -/// concatenation of the two string arguments of the function application +/// concatenation of the two string expressions given as input +/// \par parameters: two string expressions +/// \return a new string expression +string_exprt string_constraint_generatort::add_axioms_for_concat( + const string_exprt &s1, const string_exprt &s2) +{ + exprt index_zero=from_integer(0, s2.length().type()); + return add_axioms_for_concat_substr(s1, s2, index_zero, s2.length()); +} + +/// add axioms to say that the returned string expression is equal to the +/// concatenation of the two string arguments of the function application. In +/// case 4 arguments instead of 2 are given the last two arguments are +/// intepreted as a start index and last index from which we extract a substring +/// of the second argument: this is similar to the Java +/// StringBuiledr.append(CharSequence s, int start, int end) method. /// \par parameters: function application with two arguments which are strings /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_for_concat( const function_application_exprt &f) { const function_application_exprt::argumentst &args=f.arguments(); - assert(args.size()==2); - + assert(args.size()>=2); string_exprt s1=get_string_expr(args[0]); string_exprt s2=get_string_expr(args[1]); - + if(args.size()!=2) + { + assert(args.size()==4); + return add_axioms_for_concat_substr(s1, s2, args[2], args[3]); + } return add_axioms_for_concat(s1, s2); } From 334ab00b9b2276b9020810fdf565d8ee300bd08a Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Fri, 9 Jun 2017 15:01:31 +0100 Subject: [PATCH 2/4] Comment in description of test for String.replace() --- regression/strings-smoke-tests/java_replace/test.desc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/regression/strings-smoke-tests/java_replace/test.desc b/regression/strings-smoke-tests/java_replace/test.desc index d86aae6b5a9..542ed1630b5 100644 --- a/regression/strings-smoke-tests/java_replace/test.desc +++ b/regression/strings-smoke-tests/java_replace/test.desc @@ -6,3 +6,5 @@ test_replace.class ^VERIFICATION SUCCESSFUL$ -- diffblue/test-gen#256 +This test is only effective with a model of +java.lang.String.replace(LCharSequence; LCharSequence). From ef5bd4dbf4fdf41b09c8c939c21346f3534215b3 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Thu, 15 Jun 2017 11:40:56 +0100 Subject: [PATCH 3/4] Modifications to doxygen --- .../string_constraint_generator_concat.cpp | 64 ++++++++++--------- 1 file changed, 33 insertions(+), 31 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp index e14cbcc58ad..f3ffa7c9394 100644 --- a/src/solvers/refinement/string_constraint_generator_concat.cpp +++ b/src/solvers/refinement/string_constraint_generator_concat.cpp @@ -13,12 +13,14 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include -/// add axioms to say that the returned string expression is equal to the +/// Add axioms to say that the returned string expression is equal to the /// concatenation of s1 with the substring of s2 starting at index start_index -/// and ending at index end_index. If start_index >= end_index, the value -/// returned is s1. If end_index > |s2| and/or start_index < 0, the appended -/// string will be of length end_index - start_index and padded with non- -/// deterministic values. +/// and ending at index end_index. +/// +/// If start_index >= end_index, the value returned is s1. +/// If end_index > |s2| and/or start_index < 0, the appended string will be of +/// length end_index - start_index and padded with non-deterministic values. +/// /// \param s1: string expression /// \param s2: string expression /// \param start_index: expression representing an integer @@ -62,9 +64,11 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_substr( return res; } -/// add axioms to say that the returned string expression is equal to the -/// concatenation of the two string expressions given as input -/// \par parameters: two string expressions +/// Add axioms to say that the returned string expression is equal to the +/// concatenation of the two string expressions given as input. +/// +/// \param s1: the string expression to append to +/// \param s2: the string expression to append to the first one /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_for_concat( const string_exprt &s1, const string_exprt &s2) @@ -73,13 +77,15 @@ string_exprt string_constraint_generatort::add_axioms_for_concat( return add_axioms_for_concat_substr(s1, s2, index_zero, s2.length()); } -/// add axioms to say that the returned string expression is equal to the -/// concatenation of the two string arguments of the function application. In -/// case 4 arguments instead of 2 are given the last two arguments are +/// Add axioms to say that the returned string expression is equal to the +/// concatenation of the two string arguments of the function application. +/// +/// In case 4 arguments instead of 2 are given the last two arguments are /// intepreted as a start index and last index from which we extract a substring /// of the second argument: this is similar to the Java -/// StringBuiledr.append(CharSequence s, int start, int end) method. -/// \par parameters: function application with two arguments which are strings +/// StringBuilder.append(CharSequence s, int start, int end) method. +/// +/// \param f: function application with two arguments which are strings /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_for_concat( const function_application_exprt &f) @@ -96,9 +102,9 @@ string_exprt string_constraint_generatort::add_axioms_for_concat( return add_axioms_for_concat(s1, s2); } -/// add axioms corresponding to the StringBuilder.append(I) java function -/// \par parameters: function application with two arguments: a string and an -/// integer +/// Add axioms corresponding to the StringBuilder.append(I) java function +/// \param f: function application with two arguments: a string and an +/// integer /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_for_concat_int( const function_application_exprt &f) @@ -111,8 +117,8 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_int( } /// Add axioms corresponding to the StringBuilder.append(J) java function -/// \par parameters: function application with two arguments: a string and a -/// integer of type long +/// \param f: function application with two arguments: a string and an +/// integer of type long /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_for_concat_long( const function_application_exprt &f) @@ -123,8 +129,8 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_long( return add_axioms_for_concat(s1, s2); } -/// add axioms corresponding to the StringBuilder.append(Z) java function -/// \par parameters: function application two arguments: a string and a bool +/// Add axioms corresponding to the StringBuilder.append(Z) java function +/// \param f: function application two arguments: a string and a bool /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_for_concat_bool( const function_application_exprt &f) @@ -135,9 +141,8 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_bool( return add_axioms_for_concat(s1, s2); } -/// add axioms corresponding to the StringBuilder.append(C) java function -/// \par parameters: function application with two arguments: a string and a -/// char +/// Add axioms corresponding to the StringBuilder.append(C) java function +/// \param f: function application with two arguments: a string and a char /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_for_concat_char( const function_application_exprt &f) @@ -148,9 +153,8 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_char( return add_axioms_for_concat(s1, s2); } -/// add axioms corresponding to the StringBuilder.append(D) java function -/// \par parameters: function application with two arguments: a string and a -/// double +/// Add axioms corresponding to the StringBuilder.append(D) java function +/// \param f: function application with two arguments: a string and a double /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_for_concat_double( const function_application_exprt &f) @@ -162,9 +166,8 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_double( return add_axioms_for_concat(s1, s2); } -/// add axioms corresponding to the StringBuilder.append(F) java function -/// \par parameters: function application with two arguments: a string and a -/// float +/// Add axioms corresponding to the StringBuilder.append(F) java function +/// \param f: function application with two arguments: a string and a float /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_for_concat_float( const function_application_exprt &f) @@ -177,8 +180,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_float( } /// Add axioms corresponding to the StringBuilder.appendCodePoint(I) function -/// \par parameters: function application with two arguments: a string and a -/// code point +/// \param f: function application with two arguments: a string and a code point /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_for_concat_code_point( const function_application_exprt &f) From cf39c2994254fe1f83462d6ca409b724bbdea2d7 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Wed, 21 Jun 2017 09:17:28 +0100 Subject: [PATCH 4/4] Replace asserts asserts are to be replaced by INVARIANT, PRECONDITION, CHECK_RETURN, etc. --- .../refinement/string_constraint_generator_concat.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp index f3ffa7c9394..b2c9a418055 100644 --- a/src/solvers/refinement/string_constraint_generator_concat.cpp +++ b/src/solvers/refinement/string_constraint_generator_concat.cpp @@ -91,12 +91,12 @@ string_exprt string_constraint_generatort::add_axioms_for_concat( const function_application_exprt &f) { const function_application_exprt::argumentst &args=f.arguments(); - assert(args.size()>=2); + PRECONDITION(args.size()>=2); string_exprt s1=get_string_expr(args[0]); string_exprt s2=get_string_expr(args[1]); if(args.size()!=2) { - assert(args.size()==4); + PRECONDITION(args.size()==4); return add_axioms_for_concat_substr(s1, s2, args[2], args[3]); } return add_axioms_for_concat(s1, s2); @@ -160,7 +160,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_double( const function_application_exprt &f) { string_exprt s1=get_string_expr(args(f, 2)[0]); - assert(refined_string_typet::is_refined_string_type(f.type())); + PRECONDITION(refined_string_typet::is_refined_string_type(f.type())); refined_string_typet ref_type=to_refined_string_type(f.type()); string_exprt s2=add_axioms_from_float(args(f, 2)[1], ref_type, true); return add_axioms_for_concat(s1, s2); @@ -173,7 +173,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_float( const function_application_exprt &f) { string_exprt s1=get_string_expr(args(f, 2)[0]); - assert(refined_string_typet::is_refined_string_type(f.type())); + PRECONDITION(refined_string_typet::is_refined_string_type(f.type())); refined_string_typet ref_type=to_refined_string_type(f.type()); string_exprt s2=add_axioms_from_float(args(f, 2)[1], ref_type, false); return add_axioms_for_concat(s1, s2);