From e05c57dec451270a2326a129e18009d28ebda98f Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 26 Jul 2019 14:50:14 +0100 Subject: [PATCH 1/9] Move escape_non_alnum() to util/string_utils.{h,cpp} The function is generally useful for obtaining strings that contain only alphanumeric characters. --- .../java_bytecode/java_string_literals.cpp | 24 +------------------ src/util/string_utils.cpp | 19 ++++++++++++++- src/util/string_utils.h | 6 +++++ 3 files changed, 25 insertions(+), 24 deletions(-) diff --git a/jbmc/src/java_bytecode/java_string_literals.cpp b/jbmc/src/java_bytecode/java_string_literals.cpp index 0a95e7d19ac..f4595e89d76 100644 --- a/jbmc/src/java_bytecode/java_string_literals.cpp +++ b/jbmc/src/java_bytecode/java_string_literals.cpp @@ -15,34 +15,12 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include #include +#include #include #include #include -/// Replace non-alphanumeric characters with `_xx` escapes, where xx are hex -/// digits. Underscores are replaced by `__`. -/// \param to_escape: string to escape -/// \return string with non-alphanumeric characters escaped -static std::string escape_non_alnum(const std::string &to_escape) -{ - std::ostringstream escaped; - for(auto &ch : to_escape) - { - if(ch=='_') - escaped << "__"; - else if(isalnum(ch)) - escaped << ch; - else - escaped << '_' - << std::hex - << std::setfill('0') - << std::setw(2) - << (unsigned int)ch; - } - return escaped.str(); -} - /// Convert UCS-2 or UTF-16 to an array expression. /// \par parameters: `in`: wide string to convert /// \return Returns a Java char array containing the same wchars. diff --git a/src/util/string_utils.cpp b/src/util/string_utils.cpp index 68333a414a6..c76ce9820db 100644 --- a/src/util/string_utils.cpp +++ b/src/util/string_utils.cpp @@ -10,9 +10,10 @@ Author: Daniel Poetzl #include "exception_utils.h" #include "invariant.h" +#include #include #include -#include +#include /// Remove all whitespace characters from either end of a string. Whitespace /// in the middle of the string is left unchanged @@ -159,3 +160,19 @@ std::string escape(const std::string &s) return result; } + +std::string escape_non_alnum(const std::string &to_escape) +{ + std::ostringstream escaped; + for(auto &ch : to_escape) + { + if(ch == '_') + escaped << "__"; + else if(isalnum(ch)) + escaped << ch; + else + escaped << '_' << std::hex << std::setfill('0') << std::setw(2) + << (unsigned int)ch; + } + return escaped.str(); +} diff --git a/src/util/string_utils.h b/src/util/string_utils.h index 504c2f3f2b0..278e48b2c71 100644 --- a/src/util/string_utils.h +++ b/src/util/string_utils.h @@ -96,4 +96,10 @@ join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter) /// programming language. std::string escape(const std::string &); +/// Replace non-alphanumeric characters with `_xx` escapes, where xx are hex +/// digits. Underscores are replaced by `__`. +/// \param to_escape: string to escape +/// \return string with non-alphanumeric characters escaped +std::string escape_non_alnum(const std::string &to_escape); + #endif From 36b60efe00a1bc06dbd950ed4a35f5e664b7e302 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Sun, 28 Jul 2019 15:31:06 +0100 Subject: [PATCH 2/9] Make try_get_string_data_array() non-static This is so the function can be called outside of simplify_expr.cpp. --- src/util/simplify_expr.cpp | 23 ++--------------------- src/util/simplify_expr.h | 19 +++++++++++++++++++ 2 files changed, 21 insertions(+), 21 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 7c35a624052..f90e29b983e 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -64,11 +64,6 @@ struct simplify_expr_cachet simplify_expr_cachet simplify_expr_cache; #endif -static optionalt> -try_get_string_data_array( - const refined_string_exprt &s, - const namespacet &ns); - simplify_exprt::resultt<> simplify_exprt::simplify_abs(const abs_exprt &expr) { if(expr.op().is_constant()) @@ -1670,22 +1665,8 @@ optionalt simplify_exprt::expr2bits( return {}; } -/// Get char sequence from refined string expression -/// -/// If `s.content()` is of the form `&id[e]`, where `id` is an array-typed -/// symbol expression (and `e` is any expression), return the value of the -/// symbol `id` (as given by the `value` field of the symbol in the namespace -/// `ns`); otherwise return an empty optional. -/// -/// \param s: refined string expression -/// \param ns: namespace -/// \return array expression representing the char sequence which forms the -/// content of the refined string expression, empty optional if the content -/// cannot be determined -static optionalt> - try_get_string_data_array( - const refined_string_exprt &s, - const namespacet &ns) +optionalt> +try_get_string_data_array(const refined_string_exprt &s, const namespacet &ns) { if(s.content().id() != ID_address_of) { diff --git a/src/util/simplify_expr.h b/src/util/simplify_expr.h index 3f34c0486dd..22cb796abb6 100644 --- a/src/util/simplify_expr.h +++ b/src/util/simplify_expr.h @@ -10,8 +10,12 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_SIMPLIFY_EXPR_H #define CPROVER_UTIL_SIMPLIFY_EXPR_H +class array_exprt; class exprt; class namespacet; +class refined_string_exprt; + +#include // // simplify an expression @@ -27,4 +31,19 @@ bool simplify( // this is the preferred interface exprt simplify_expr(exprt src, const namespacet &ns); +/// Get char sequence from refined string expression +/// +/// If `s.content()` is of the form `&id[e]`, where `id` is an array-typed +/// symbol expression (and `e` is any expression), return the value of the +/// symbol `id` (as given by the `value` field of the symbol in the namespace +/// `ns`); otherwise return an empty optional. +/// +/// \param s: refined string expression +/// \param ns: namespace +/// \return array expression representing the char sequence which forms the +/// content of the refined string expression, empty optional if the content +/// cannot be determined +optionalt> +try_get_string_data_array(const refined_string_exprt &s, const namespacet &ns); + #endif // CPROVER_UTIL_SIMPLIFY_EXPR_H From f3c5c373ca438107a50f3d9dec7bb446675001b8 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 29 Jul 2019 12:59:55 +0100 Subject: [PATCH 3/9] Change interface of try_get_string_data_array() Take the content field of a refined string expression instead of taking the whole refined string expression. This will allow it to be used from the string mutators constant propagation code in goto_symex.cpp. --- src/util/simplify_expr.cpp | 30 ++++++++++++++++-------------- src/util/simplify_expr.h | 14 +++++++------- 2 files changed, 23 insertions(+), 21 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index f90e29b983e..d94c3565a8a 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -158,14 +158,14 @@ static simplify_exprt::resultt<> simplify_string_endswith( const namespacet &ns) { const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0)); - const auto s1_data_opt = try_get_string_data_array(s1, ns); + const auto s1_data_opt = try_get_string_data_array(s1.content(), ns); if(!s1_data_opt) return simplify_exprt::unchanged(expr); const array_exprt &s1_data = s1_data_opt->get(); const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1)); - const auto s2_data_opt = try_get_string_data_array(s2, ns); + const auto s2_data_opt = try_get_string_data_array(s2.content(), ns); if(!s2_data_opt) return simplify_exprt::unchanged(expr); @@ -214,13 +214,13 @@ static simplify_exprt::resultt<> simplify_string_compare_to( const namespacet &ns) { const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0)); - const auto s1_data_opt = try_get_string_data_array(s1, ns); + const auto s1_data_opt = try_get_string_data_array(s1.content(), ns); if(!s1_data_opt) return simplify_exprt::unchanged(expr); const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1)); - const auto s2_data_opt = try_get_string_data_array(s2, ns); + const auto s2_data_opt = try_get_string_data_array(s2.content(), ns); if(!s2_data_opt) return simplify_exprt::unchanged(expr); @@ -285,7 +285,7 @@ static simplify_exprt::resultt<> simplify_string_index_of( const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0)); - const auto s1_data_opt = try_get_string_data_array(s1, ns); + const auto s1_data_opt = try_get_string_data_array(s1.content(), ns); if(!s1_data_opt) { @@ -310,7 +310,7 @@ static simplify_exprt::resultt<> simplify_string_index_of( const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1)); - const auto s2_data_opt = try_get_string_data_array(s2, ns); + const auto s2_data_opt = try_get_string_data_array(s2.content(), ns); if(!s2_data_opt) { @@ -379,7 +379,7 @@ static simplify_exprt::resultt<> simplify_string_char_at( const refined_string_exprt &s = to_string_expr(expr.arguments().at(0)); - const auto char_seq_opt = try_get_string_data_array(s, ns); + const auto char_seq_opt = try_get_string_data_array(s.content(), ns); if(!char_seq_opt) { @@ -420,7 +420,8 @@ static simplify_exprt::resultt<> simplify_string_startswith( auto &first_argument = to_string_expr(expr.arguments().at(0)); auto &second_argument = to_string_expr(expr.arguments().at(1)); - const auto first_value_opt = try_get_string_data_array(first_argument, ns); + const auto first_value_opt = + try_get_string_data_array(first_argument.content(), ns); if(!first_value_opt) { @@ -429,7 +430,8 @@ static simplify_exprt::resultt<> simplify_string_startswith( const array_exprt &first_value = first_value_opt->get(); - const auto second_value_opt = try_get_string_data_array(second_argument, ns); + const auto second_value_opt = + try_get_string_data_array(second_argument.content(), ns); if(!second_value_opt) { @@ -1666,21 +1668,21 @@ optionalt simplify_exprt::expr2bits( } optionalt> -try_get_string_data_array(const refined_string_exprt &s, const namespacet &ns) +try_get_string_data_array(const exprt &content, const namespacet &ns) { - if(s.content().id() != ID_address_of) + if(content.id() != ID_address_of) { return {}; } - const auto &content = to_address_of_expr(s.content()); + const auto &array_pointer = to_address_of_expr(content); - if(content.object().id() != ID_index) + if(array_pointer.object().id() != ID_index) { return {}; } - const auto &array_start = to_index_expr(content.object()); + const auto &array_start = to_index_expr(array_pointer.object()); if(array_start.array().id() != ID_symbol || array_start.array().type().id() != ID_array) diff --git a/src/util/simplify_expr.h b/src/util/simplify_expr.h index 22cb796abb6..7035720ab21 100644 --- a/src/util/simplify_expr.h +++ b/src/util/simplify_expr.h @@ -31,19 +31,19 @@ bool simplify( // this is the preferred interface exprt simplify_expr(exprt src, const namespacet &ns); -/// Get char sequence from refined string expression +/// Get char sequence from content field of a refined string expression /// -/// If `s.content()` is of the form `&id[e]`, where `id` is an array-typed -/// symbol expression (and `e` is any expression), return the value of the -/// symbol `id` (as given by the `value` field of the symbol in the namespace -/// `ns`); otherwise return an empty optional. +/// If `content` is of the form `&id[e]`, where `id` is an array-typed symbol +/// expression (and `e` is any expression), return the value of the symbol `id` +/// (as given by the `value` field of the symbol in the namespace `ns`); +/// otherwise return an empty optional. /// -/// \param s: refined string expression +/// \param content: content field of a refined string expression /// \param ns: namespace /// \return array expression representing the char sequence which forms the /// content of the refined string expression, empty optional if the content /// cannot be determined optionalt> -try_get_string_data_array(const refined_string_exprt &s, const namespacet &ns); +try_get_string_data_array(const exprt &content, const namespacet &ns); #endif // CPROVER_UTIL_SIMPLIFY_EXPR_H From b0ec24e22acf5e53cec96c242c5d3a0ca885b4ef Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Sun, 28 Jul 2019 15:30:06 +0100 Subject: [PATCH 4/9] Check that `array_expr` is not in `length_of_array` map in array_pool.cpp Previously the string solver returned an error when constant propagation of strings was used as `array_poolt::insert()` might be called for array expressions for which there is already a mapping in the `length_of_array` map. --- src/solvers/strings/array_pool.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/solvers/strings/array_pool.cpp b/src/solvers/strings/array_pool.cpp index e454175e555..5289a5f8f9c 100644 --- a/src/solvers/strings/array_pool.cpp +++ b/src/solvers/strings/array_pool.cpp @@ -162,7 +162,10 @@ void array_poolt::insert( INVARIANT( it_bool.second, "should not associate two arrays to the same pointer"); - attempt_assign_length_from_type(array_expr, length_of_array, fresh_symbol); + if(length_of_array.find(array_expr) == length_of_array.end()) + { + attempt_assign_length_from_type(array_expr, length_of_array, fresh_symbol); + } } /// Return a map mapping all array_string_exprt of the array_pool to their From b9d5f4b3574dfdf86d530779e2394ec6f6d5df8d Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Sun, 28 Jul 2019 15:31:25 +0100 Subject: [PATCH 5/9] Implement constant propagation of string concatenation This implements constant propagation of ID_cprover_string_concat_func and ID_cprover_string_empty_string_func which are the primitives used by StringBuilder.append(), which in turn is used to implement String concatenation using +. --- .../Main.class | Bin 0 -> 872 bytes .../Main.java | 9 + .../test.desc | 9 + .../Main.class | Bin 0 -> 1155 bytes .../Main.java | 25 ++ .../test1.desc | 9 + .../test2.desc | 9 + .../test3.desc | 9 + .../Main.class | Bin 0 -> 702 bytes .../Main.java | 8 + .../test.desc | 9 + .../Main.class | Bin 0 -> 846 bytes .../Main.java | 9 + .../test.desc | 9 + .../Main.class | Bin 0 -> 1146 bytes .../Main.java | 25 ++ .../test1.desc | 9 + .../test2.desc | 9 + .../test3.desc | 9 + .../Main.class | Bin 0 -> 977 bytes .../Main.java | 10 + .../test1.desc | 11 + .../test2.desc | 11 + .../test3.desc | 11 + .../Main.class | Bin 0 -> 644 bytes .../Main.java | 7 + .../test.desc | 9 + src/goto-symex/goto_symex.cpp | 297 +++++++++++++++++- src/goto-symex/goto_symex.h | 99 ++++++ 29 files changed, 611 insertions(+), 1 deletion(-) create mode 100644 jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/Main.class create mode 100644 jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/Main.java create mode 100644 jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/test.desc create mode 100644 jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/Main.class create mode 100644 jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/Main.java create mode 100644 jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test1.desc create mode 100644 jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test2.desc create mode 100644 jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test3.desc create mode 100644 jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/Main.class create mode 100644 jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/Main.java create mode 100644 jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/test.desc create mode 100644 jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/Main.class create mode 100644 jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/Main.java create mode 100644 jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/test.desc create mode 100644 jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/Main.class create mode 100644 jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/Main.java create mode 100644 jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test1.desc create mode 100644 jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test2.desc create mode 100644 jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test3.desc create mode 100644 jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/Main.class create mode 100644 jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/Main.java create mode 100644 jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/test1.desc create mode 100644 jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/test2.desc create mode 100644 jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/test3.desc create mode 100644 jbmc/regression/jbmc-strings/StringDefaultConstructorConstantEvaluation/Main.class create mode 100644 jbmc/regression/jbmc-strings/StringDefaultConstructorConstantEvaluation/Main.java create mode 100644 jbmc/regression/jbmc-strings/StringDefaultConstructorConstantEvaluation/test.desc diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/Main.class b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..9e0e12cde7bb199bece0a85a91f85954cc61cc98 GIT binary patch literal 872 zcmZuvOK%cU6#g!cnPECDlv0Y-R;yK^l;Q)QCC1v;!~}GKv1xY$+~BR_KxQsR-TE)s zxOA;1kk~}`{wIy+PN8GcZtmkd-#OZ^Fc~fr9$4=_s05M@h#9!`!Ov``nYF>-sywx0?=cGq3{&ttwn0A2CGp zg;xx*?QWYhBx}Ou&--ti+G7JmqU3P4@Q*KC4xSc0`;k3C&>Fs7qk#5lQ{fCbhZsL}O+o)KW zMVhi$xP!Y4xiG@kq@-QX>rx1fLIke&aGwOL+&Uguc!*7gROt7jdB|H-%YV?Z7>4k*|XRJYz6@X?xP&6AC(0 z4h=0CirjW+vJBZa_l3vXCq1D#$vzoqtOr=3ElJTfu~bfVlU`BKQXoU;JpGpFW^~8b zMqpnR5m`F5092-h6Y3{&jgoEm2$B7Cbc9%~n2ryj?G=a6>)&7ukXauhkImlk z2vfhtaM~JTdJw`YRU}BYNXe8c6ERX4Crm>LI(A?nM-~f_KWdlH=~&DXcK$?AB@hYB hre}so4xq=rAQt@&BMd&NLj{T>Vm($RT?le7{R7?9voZhx literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/Main.java b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/Main.java new file mode 100644 index 00000000000..4a6ea40f518 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/Main.java @@ -0,0 +1,9 @@ +public class Main { + public void test() { + StringBuilder sb = new StringBuilder("abc"); + sb.append("xyz"); + String s = sb.toString(); + assert s.length() == 6; + assert s.startsWith("abcxyz"); + } +} diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/test.desc b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/test.desc new file mode 100644 index 00000000000..936f1a33c06 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/test.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/Main.class b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..0385c410ad700400c8689e096f49b943f17a098e GIT binary patch literal 1155 zcmb`HO>YuG7{~v!yeuqBf#s#8T5Giy=o_|HtJ0X#RudD@1IDJkEil2YxRBk&tHy63 z7muFR1QMI*-S4FF8A^BCwDDv}c4nT}-~68mzy5sx0bmm)1#!&ExE{is0tq)lxGC28 zFeY$I>=tC?6ofG=4tWJx6vU2l78NXES;h)Oa$dJ>ZaGHBwD$~KueW)VfgLggw+z#8 z9x?dxg_jKe-AGXxxNJ8KNlnxi*fSM~15E@O47(!c( z_PD50>-4M!e`1Id;i_(!t4I1)urVDg8N?~_mNy0AQb$B$T7kP zLnuE-)=9EPG~WPf-}8u0(x}rk^#avZ;763;l5{RW#x6pbB998`HwrQ&8QCoHOuIbq zse<6y5j;agE1K^=(L|`XiU{!}NWL6mD3gdTP0pja;?leu)0ADBbJ}P^n~$CVXQT=I zTbd-nqzEQWFc~b+K(-0Rg`xj|6KO)Y>cVV{#s?&{i2-7L$o|jp`@TW;bU&T2C=`IC MZi`{h&_Tkrzk|TrP5=M^ literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/Main.java b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/Main.java new file mode 100644 index 00000000000..9f86462847a --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/Main.java @@ -0,0 +1,25 @@ +public class Main { + public void test1() { + StringBuilder sb1 = new StringBuilder("abc"); + String s2 = ""; + sb1.append(s2); + assert sb1.length() == 3; + assert sb1.toString().startsWith("abc"); + } + + public void test2() { + StringBuilder sb1 = new StringBuilder(); + String s2 = "abc"; + sb1.append(s2); + assert sb1.length() == 3; + assert sb1.toString().startsWith("abc"); + } + + public void test3() { + StringBuilder sb1 = new StringBuilder(); + String s2 = ""; + sb1.append(s2); + assert sb1.length() == 0; + assert sb1.toString().startsWith(""); + } +} diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test1.desc b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test1.desc new file mode 100644 index 00000000000..5d4cb5560c8 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test1.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test1 --property "java::Main.test1:()V.assertion.1" --property "java::Main.test1:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test2.desc b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test2.desc new file mode 100644 index 00000000000..92d3a8b0dab --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test2.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test2 --property "java::Main.test2:()V.assertion.1" --property "java::Main.test2:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test3.desc b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test3.desc new file mode 100644 index 00000000000..1b80407d635 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test3.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test3 --property "java::Main.test3:()V.assertion.1" --property "java::Main.test3:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/Main.class b/jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..4c786819c8c6be349c5b5af6e4024c60746992fd GIT binary patch literal 702 zcmYjP(M}UV6g{)s?X=4vrPNYUP%3H*NMA@akr)**F)8{`V*+p6?xYSbyJU81;-}aj z@L5etB8k5HPa5wmw(HBxopaAU_spI7_2>H!0K4e;5Ln^3?!&=~U2c@&W7WqRZgSl6 z!7aRob&jTw+t}c^!?3gwq^Zw*Q^Ls9FwFN%FnE6$oMkZi;JC|B+8adwWc*$-(gXQI*`o4cpyHjA;6os= zfC|I1jXO~g4?8`hRXlt)Qc)>b$xHSl z8Y)9Ql&R7(oSCE%nNf;$dKW>D#wrbaF^XJJJu0*=(rJ};M!UCp4)(@GDo4FWjOAJX-OLlPSoJ5E8-o`R literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/Main.java b/jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/Main.java new file mode 100644 index 00000000000..f5f01c587fd --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/Main.java @@ -0,0 +1,8 @@ +public class Main { + public void test() { + StringBuilder sb = new StringBuilder(); + String s = sb.toString(); + assert s.isEmpty(); + assert s.length() == 0; + } +} diff --git a/jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/test.desc b/jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/test.desc new file mode 100644 index 00000000000..27a6bb0db9b --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/test.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/Main.class b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..971beaf6f323eba7b9a3a428c566a54d43c77019 GIT binary patch literal 846 zcmZuv%Wl&^6g`uN?YM4}rfHfM0u%})ZPNrOFSSC@0xeQf7C|7obCOY*Vw}jHAm9)9 zg=|=|2BcJ?672b?iaXB3NJX;m*yrAR&V9_E)1SWpY~sF&6!Hcx7`Uk8l8G4d$}B5$ zIe{5mF|mTHI8RpfQ`U(iuBv5GYv>kM-%w(oOKijM0)7QWqZc#DA@GHBbv74iW? zv`~D>5ZmpvI76~3Tz=4d*Wlg@6-*AveaSFgmv-}Q&F%)UjuL~h-E>AAX1&w%n*6Cy z8Ht)L+>Imqy=`F*8B(wtO|l<8eqvZqc-gVtcDXJ+;kI{r!fA2O!UoC~D!5@`7HJZ& za1*x}a$&-waVt+euj5e*#7m?W4eK@)s$_NCv2Yjn7*b*0^TrWxQV;(?Lv2OT?Q)k! zQYuu#grRqPDW>Z^%(4%3PhHy z7J$mNFbVyP2;D1SKOL#2qqP&nULPaAHh{KH?*RJ2cNl$SN&_TP+80cnz@&(&-y=9} z4KUpgVWk!c)Rst36&59a4RI`ztw6^f4CKg@MC23|9gD*!OYqX9tj(ZQU^YE7K(Y@# a_7$<{4;Uf;xEsY4N5p!l8ao%rpZ^Qj=&SPp literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/Main.java b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/Main.java new file mode 100644 index 00000000000..09e47b60040 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/Main.java @@ -0,0 +1,9 @@ +public class Main { + public void test() { + String s1 = "abc"; + String s2 = "xyz"; + String s3 = s1 + s2; + assert s3.length() == 6; + assert s3.startsWith("abcxyz"); + } +} diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/test.desc b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/test.desc new file mode 100644 index 00000000000..936f1a33c06 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/test.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/Main.class b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..f08a81099b2c1e872e8ddb5aa5db09a0a83b322f GIT binary patch literal 1146 zcmb_b%Wl(95Ixs<*m0aDb)GG>P-r1(n}n9|QY!?M1|cP75d@+;C%FnP!HH~#Uw~gA z8Xu_(+H zVXj6H!?KDMT$6EKg(_kz$jd0GSjC!*b%x}!;W*rO&7S2vHXWncF&tG9>);XUzlNa{qFjK#~+jzt1hw zrI@ez8&0BIg;TCE$1N(@?M==|hUqm9( zWW%0Qgfi3A50GfGfG4_C(*yM*1YaE@v^GL`ot_coy{}M)NESzkgg+sA1eFq^KRs`% zs7oVgL*FgHBoAz!;D7*KL3#^ej%*n+s!))nNF35J$}(~%cZOKaoxv(l)208;DoU(0 z;u9mt8DbSDR*Cai%}-gqA8S?BiPia9=|ZcIz9ti?0{@mONu*LlDovy^^fzR&i=0oY t^oLXmE=);Pyru%PdTfN5A>`m^1Owlo_^p`qUC17Sq&*NLaMA13!f(Z$*0%rv literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/Main.java b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/Main.java new file mode 100644 index 00000000000..2085a053a50 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/Main.java @@ -0,0 +1,25 @@ +public class Main { + public void test1() { + String s1 = "abc"; + String s2 = ""; + String s3 = s1 + s2; + assert s3.length() == 3; + assert s3.startsWith("abc"); + } + + public void test2() { + String s1 = ""; + String s2 = "abc"; + String s3 = s1 + s2; + assert s3.length() == 3; + assert s3.startsWith("abc"); + } + + public void test3() { + String s1 = ""; + String s2 = ""; + String s3 = s1 + s2; + assert s3.length() == 0; + assert s3.startsWith(""); + } +} diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test1.desc b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test1.desc new file mode 100644 index 00000000000..5d4cb5560c8 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test1.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test1 --property "java::Main.test1:()V.assertion.1" --property "java::Main.test1:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test2.desc b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test2.desc new file mode 100644 index 00000000000..92d3a8b0dab --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test2.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test2 --property "java::Main.test2:()V.assertion.1" --property "java::Main.test2:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test3.desc b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test3.desc new file mode 100644 index 00000000000..1b80407d635 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test3.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test3 --property "java::Main.test3:()V.assertion.1" --property "java::Main.test3:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/Main.class b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..2e4b51f8205deb5d677a58b6fe4f690a0781242e GIT binary patch literal 977 zcma)4%Wl&^6g^`*apJm3n!duLg+g2MYC~zurWFE8SwI7eAQ0J2l2MrwoXDQ=G5G=3 zfRsv9f_=XUA?~9kqmgFEm{n$&Jf?1o>cc3%zWV`gLTkp z35N8M^u)8?yN2*zXfQ)ei9l^J%;%3z_f;n&Qp3Ro)HpHpG@6ZSZeBIl}m3^v$~i;mPX-?ri(N(42!>uJ?zPLOZYA}u<4?L z+a%>;3#5}9V;>CN9{PUAX8<|VDmJ!V%5s+>GX_6zoQS6S<-8yOr2*n)x(Bec#sG;vrp}P0j`K}38X;pU+-p*`P@*9gsgnTvj*^WWDO?)q zJf$55b&H|MdL)vaA_cAVPnCQ_+VS2)s?(2@IAknVFjSSNaEh zR+ExQqVN1BW4yCU%gfB2bM8I&+`D`C=f_U~JJ^g6qsp-u!9%rx2um({%u$OFqMFAO z_g?0B8sQmMI93^E*Mu=rTh&j^zA~cSlU)XO#t`nRRN2=Ie!X$b5bX84lA+jCseCuM zYD@jWB@@&K#B~Of3x@n|r}tkYYV`-YBM+6UC>#luzPJ>hM2sRz3?&zD z_e6TW-LhJx=P{=7D8?F|GgKzz+k2}ATK6>r&AW~bvfuM-2<#t zan337LG>unIYX}+-DDTJ%^R? +#include #include +#include +#include +#include #include #include +#include +#include + +#include unsigned goto_symext::dynamic_counter=0; @@ -87,8 +96,294 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code) if(state.source.pc->source_location.get_hide()) assignment_type = symex_targett::assignment_typet::HIDDEN; + symex_assignt symex_assign{ + state, assignment_type, ns, symex_config, target}; + + // Try to constant propagate potential side effects of the assignment, when + // simplification is turned on and there is one thread only. Constant + // propagation is only sound for sequential code as here we do not take into + // account potential writes from other threads when propagating the values. + if(symex_config.simplify_opt && state.threads.size() <= 1) + { + if(constant_propagate_assignment_with_side_effects( + state, symex_assign, lhs, rhs)) + return; + } + exprt::operandst lhs_if_then_else_conditions; - symex_assignt{state, assignment_type, ns, symex_config, target}.assign_rec( + symex_assign.assign_rec( lhs, expr_skeletont{}, rhs, lhs_if_then_else_conditions); } } + +/// Maps the given array expression containing constant characters to a string +/// containing only alphanumeric characters +/// +/// \param char_array: array_exprt containing characters represented by +/// expressions of kind constant_exprt and type unsignedbv_typet or +/// signedbv_typet +/// \return a string containing only alphanumeric characters +static std::string get_alnum_string(const array_exprt &char_array) +{ + const auto &ibv_type = + to_integer_bitvector_type(to_array_type(char_array.type()).subtype()); + + const std::size_t n_bits = ibv_type.get_width(); + CHECK_RETURN(n_bits % 8 == 0); + + static_assert(CHAR_BIT == 8, "bitwidth of char assumed to be 8"); + + const std::size_t n_chars = n_bits / 8; + + INVARIANT( + sizeof(std::size_t) >= n_chars, + "size_t shall be large enough to represent a character"); + + std::string result; + + for(const auto &c : char_array.operands()) + { + const std::size_t c_val = numeric_cast_v(to_constant_expr(c)); + + for(std::size_t i = 0; i < n_chars; i++) + { + const char c_chunk = static_cast((c_val >> (i * 8)) & 0xff); + result.push_back(c_chunk); + } + } + + return escape_non_alnum(result); +} + +bool goto_symext::constant_propagate_assignment_with_side_effects( + statet &state, + symex_assignt &symex_assign, + const exprt &lhs, + const exprt &rhs) +{ + if(rhs.id() == ID_function_application) + { + const function_application_exprt &f_l1 = to_function_application_expr(rhs); + + if(f_l1.function().id() == ID_symbol) + { + const irep_idt &func_id = + to_symbol_expr(f_l1.function()).get_identifier(); + + if(func_id == ID_cprover_string_concat_func) + { + return constant_propagate_string_concat(state, symex_assign, f_l1); + } + else if(func_id == ID_cprover_string_empty_string_func) + { + // constant propagating the empty string always succeeds as it does + // not depend on potentially non-constant inputs + constant_propagate_empty_string(state, symex_assign, f_l1); + return true; + } + } + } + + return false; +} + +void goto_symext::assign_string_constant( + statet &state, + symex_assignt &symex_assign, + const ssa_exprt &length, + const constant_exprt &new_length, + const ssa_exprt &char_array, + const array_exprt &new_char_array) +{ + // assign length of string + symex_assign.assign_symbol(length, expr_skeletont{}, new_length, {}); + + const std::string aux_symbol_name = + get_alnum_string(new_char_array) + "_constant_char_array"; + + const bool string_constant_exists = + state.symbol_table.has_symbol(aux_symbol_name); + + const symbolt &aux_symbol = + string_constant_exists + ? state.symbol_table.lookup_ref(aux_symbol_name) + : get_new_string_data_symbol( + state, symex_assign, aux_symbol_name, char_array, new_char_array); + + INVARIANT( + aux_symbol.value == new_char_array, + "symbol shall have value derived from char array content"); + + const address_of_exprt string_data( + index_exprt(aux_symbol.symbol_expr(), from_integer(0, index_type()))); + + symex_assign.assign_symbol(char_array, expr_skeletont{}, string_data, {}); + + if(!string_constant_exists) + { + associate_array_to_pointer( + state, symex_assign, new_char_array, string_data); + } +} + +const symbolt &goto_symext::get_new_string_data_symbol( + statet &state, + symex_assignt &symex_assign, + const std::string &aux_symbol_name, + const ssa_exprt &char_array, + const array_exprt &new_char_array) +{ + array_typet new_char_array_type = new_char_array.type(); + new_char_array_type.set(ID_C_constant, true); + + symbolt &new_aux_symbol = get_fresh_aux_symbol( + new_char_array_type, + "", + aux_symbol_name, + source_locationt(), + ns.lookup(to_symbol_expr(char_array.get_original_expr())).mode, + ns, + state.symbol_table); + + CHECK_RETURN(new_aux_symbol.is_state_var); + CHECK_RETURN(new_aux_symbol.is_lvalue); + + new_aux_symbol.is_static_lifetime = true; + new_aux_symbol.is_file_local = false; + new_aux_symbol.is_thread_local = false; + + new_aux_symbol.value = new_char_array; + + const exprt arr = state.rename(new_aux_symbol.symbol_expr(), ns).get(); + + symex_assign.assign_symbol( + to_ssa_expr(arr).get_l1_object(), expr_skeletont{}, new_char_array, {}); + + return new_aux_symbol; +} + +void goto_symext::associate_array_to_pointer( + statet &state, + symex_assignt &symex_assign, + const array_exprt &new_char_array, + const address_of_exprt &string_data) +{ + const symbolt &function_symbol = + ns.lookup(ID_cprover_associate_array_to_pointer_func); + + const function_application_exprt array_to_pointer_app{ + function_symbol.symbol_expr(), {new_char_array, string_data}}; + + const symbolt &return_symbol = get_fresh_aux_symbol( + to_mathematical_function_type(function_symbol.type).codomain(), + "", + "return_value", + source_locationt(), + function_symbol.mode, + ns, + state.symbol_table); + + const ssa_exprt ssa_expr(return_symbol.symbol_expr()); + + symex_assign.assign_symbol( + ssa_expr, expr_skeletont{}, array_to_pointer_app, {}); +} + +optionalt> +goto_symext::try_evaluate_constant_string( + const statet &state, + const exprt &content) +{ + if(content.id() != ID_symbol) + { + return {}; + } + + const auto s_pointer_opt = + state.propagation.find(to_symbol_expr(content).get_identifier()); + + if(!s_pointer_opt) + { + return {}; + } + + return try_get_string_data_array(s_pointer_opt->get(), ns); +} + +void goto_symext::constant_propagate_empty_string( + statet &state, + symex_assignt &symex_assign, + const function_application_exprt &f_l1) +{ + const auto &f_type = to_mathematical_function_type(f_l1.function().type()); + const auto &length_type = f_type.domain().at(0); + const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype(); + + const constant_exprt length = from_integer(0, length_type); + + const array_typet char_array_type(char_type, length); + + DATA_INVARIANT( + f_l1.arguments().size() == 2, + "empty string primitive takes two output arguments"); + + const array_exprt char_array({}, char_array_type); + + assign_string_constant( + state, + symex_assign, + to_ssa_expr(f_l1.arguments().at(0)), + length, + to_ssa_expr(f_l1.arguments().at(1)), + char_array); +} + +bool goto_symext::constant_propagate_string_concat( + statet &state, + symex_assignt &symex_assign, + const function_application_exprt &f_l1) +{ + const auto &f_type = to_mathematical_function_type(f_l1.function().type()); + const auto &length_type = f_type.domain().at(0); + const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype(); + + const refined_string_exprt &s1 = to_string_expr(f_l1.arguments().at(2)); + const auto s1_data_opt = try_evaluate_constant_string(state, s1.content()); + + if(!s1_data_opt) + return false; + + const array_exprt &s1_data = s1_data_opt->get(); + + const refined_string_exprt &s2 = to_string_expr(f_l1.arguments().at(3)); + const auto s2_data_opt = try_evaluate_constant_string(state, s2.content()); + + if(!s2_data_opt) + return false; + + const array_exprt &s2_data = s2_data_opt->get(); + + const std::size_t new_size = + s1_data.operands().size() + s2_data.operands().size(); + + const constant_exprt new_char_array_length = + from_integer(new_size, length_type); + + const array_typet new_char_array_type(char_type, new_char_array_length); + + exprt::operandst operands(s1_data.operands()); + operands.insert( + operands.end(), s2_data.operands().begin(), s2_data.operands().end()); + + const array_exprt new_char_array(std::move(operands), new_char_array_type); + + assign_string_constant( + state, + symex_assign, + to_ssa_expr(f_l1.arguments().at(0)), + new_char_array_length, + to_ssa_expr(f_l1.arguments().at(1)), + new_char_array); + + return true; +} diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 2896720c127..de1942a02cb 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "path_storage.h" class byte_extract_exprt; +class function_application_exprt; class typet; class code_typet; class symbol_tablet; @@ -33,6 +34,7 @@ class symbol_exprt; class member_exprt; class namespacet; class side_effect_exprt; +class symex_assignt; class typecast_exprt; /// Configuration used for a symbolic execution @@ -528,6 +530,103 @@ class goto_symext /// \param code: The assignment to execute void symex_assign(statet &state, const code_assignt &code); + /// Attempt to constant propagate side effects of the assignment (if any) + /// + /// \param state: goto symex state + /// \param symex_assign: object handling symbol assignments + /// \param lhs: lhs of the assignment + /// \param rhs: rhs of the assignment + /// \return true if the operation could be evaluated to a constant string, + /// false otherwise + bool constant_propagate_assignment_with_side_effects( + statet &state, + symex_assignt &symex_assign, + const exprt &lhs, + const exprt &rhs); + + /// Create an empty string constant + /// + /// \param state: goto symex state + /// \param symex_assign: object handling symbol assignments + /// \param f_l1: application of function ID_cprover_string_empty_string_func + /// with l1 renaming applied + void constant_propagate_empty_string( + statet &state, + symex_assignt &symex_assign, + const function_application_exprt &f_l1); + + /// Attempt to constant propagate string concatenation + /// + /// \param state: goto symex state + /// \param symex_assign: object handling symbol assignments + /// \param f_l1: application of function ID_cprover_string_concat_func with + /// l1 renaming applied + /// \return true if the operation could be evaluated to a constant string, + /// false otherwise + bool constant_propagate_string_concat( + statet &state, + symex_assignt &symex_assign, + const function_application_exprt &f_l1); + + /// Assign constant string length and string data given by a char array to + /// given ssa variables + /// + /// A new symbol is created (if not yet existing) in the symbol table to hold + /// the string data given by `new_char_array`. The name of the symbol is + /// derived from the contents of `new_char_array` (e.g., if the array contains + /// "abc", the symbol will be named "abc_constant_char_array"). Then, the + /// expression `&sym[0]` is assigned to `char_array` (assuming `sym` denotes + /// the symbol holding the string data given by `new_char_array`. + /// + /// \param state: goto symex state + /// \param symex_assign: object handling symbol assignments + /// \param length: ssa variable to assign the constant string length to + /// \param new_length: value to assign to `length` + /// \param char_array: ssa variable to assign the constant string data to + /// \param new_char_array: constant char array which gives the string data to + /// assign to `char_array` + void assign_string_constant( + statet &state, + symex_assignt &symex_assign, + const ssa_exprt &length, + const constant_exprt &new_length, + const ssa_exprt &char_array, + const array_exprt &new_char_array); + + /// Installs a new symbol in the symbol table to represent the given + /// character array, and assigns the character array to the symbol + /// + /// \param state: goto symex state + /// \param symex_assign: object handling symbol assignments + /// \param aux_symbol_name: name of the symbol to create + /// \param char_array: ssa variable to which to assign a pointer to the symbol + /// \param new_char_array: new character array to assign to the symbol + const symbolt &get_new_string_data_symbol( + statet &state, + symex_assignt &symex_assign, + const std::string &aux_symbol_name, + const ssa_exprt &char_array, + const array_exprt &new_char_array); + + /// Generate array to pointer association primitive + /// + /// Executes an assignment `return_value = f(new_char_array, string_data)`, + /// with `new_char_array` being the character array to associate with pointer + /// `string_data` + /// + /// \param state: goto symex state + /// \param symex_assign: object handling symbol assignments + /// \param new_char_array: character array to associate with pointer + /// \param string_data: pointer to associate with character array + void associate_array_to_pointer( + statet &state, + symex_assignt &symex_assign, + const array_exprt &new_char_array, + const address_of_exprt &string_data); + + optionalt> + try_evaluate_constant_string(const statet &state, const exprt &content); + // havocs the given object void havoc_rec(statet &state, const guardt &guard, const exprt &dest); From aff73bdac000752f8d4a0a31e2b2544654064ca9 Mon Sep 17 00:00:00 2001 From: Yumi Bagge Date: Fri, 26 Jul 2019 17:08:51 +0100 Subject: [PATCH 6/9] Add regression test that uses models-library --- .../Main.class | Bin 0 -> 789 bytes .../Main.java | 8 ++++++++ .../test.desc | 9 +++++++++ 3 files changed, 17 insertions(+) create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/Main.class create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/Main.java create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/test.desc diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..2564e1c2fa864dfa152e7ea38782a67d0ce87273 GIT binary patch literal 789 zcmZWnO>fgc5PcilvEw*R>ZWOc6lf`sv`v#jIHf{Bfm2crK}hY*u~(Ig>jZxw;HTsd za0aAQq7vNsQ5CaJQ&*~N&#q_Q%zHbt|1N(20nouS9YxeMtZKNc;+_r}HDT@xvz9{v z>lz;D*uX;-k96cwQ}I|w9Ss$m3`-kU81f);M}GL)4XvTa9R_y9klk~AH+s$>)f*oe z--~ZVjTq^^af0uIKQ;z&4r&cF;0V!XoLTB+4Kr z18wXwRMX6t^E15(f>A&k1*3{52A-nBP)d>Sh9}%6`PW=CT0t-#bDz4=toPD{S+v`@ z;kwk>rE^E4d5v=YCXf(W{wcP+kYV|H>6w;pgPLDV3HLpk5JSb`p&M}L>S)yOD5e07 z=Ll;w=ptPRR;r5b&`tsq%_Uo=zg1cpt;*&Z*bf23GTCh66rsu$^b{GoI>4@(>6udh z9P;5Al&vYU+w@JL9{hwhLAhz>rqCzIpCeBQ2Ny=8B&|acPCJF_&$hM(kg}e)3 v7ig=f&R%E~ovZ95a)3p%FvY?Is{9?Y^b1;AdahWMQjjrT2=TWQ<~#oZ>S~{Y literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/Main.java new file mode 100644 index 00000000000..9c25e16e1d8 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/Main.java @@ -0,0 +1,8 @@ +public class Main { + public void test() { + String s1 = "abc"; + String s2 = "xyz"; + String s3 = s1 + s2; + assert s3.equals("abcxyz"); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/test.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/test.desc new file mode 100644 index 00000000000..b945ed1593a --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/test.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test --property "java::Main.test:()V.assertion.1" --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- From 6a2684813c668321b48a5175ef9fa4a40fcbf30f Mon Sep 17 00:00:00 2001 From: Yumi Bagge Date: Fri, 26 Jul 2019 17:09:14 +0100 Subject: [PATCH 7/9] Add regression test to check verification failure --- .../Main.class | Bin 0 -> 951 bytes .../Main.java | 15 +++++++++++++++ .../test1.desc | 8 ++++++++ .../test2.desc | 8 ++++++++ 4 files changed, 31 insertions(+) create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/Main.class create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/Main.java create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/test1.desc create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/test2.desc diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..a8de14739ad10f76cc44cd9d99fbe4eb87b0e971 GIT binary patch literal 951 zcmb7?-*3`T6vw|83b&N Date: Fri, 26 Jul 2019 17:09:46 +0100 Subject: [PATCH 8/9] Add regression test for 2byte char --- .../Main.class | Bin 0 -> 870 bytes .../Main.java | 9 +++++++++ .../test.desc | 9 +++++++++ 3 files changed, 18 insertions(+) create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/Main.class create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/Main.java create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/test.desc diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..db71618d67d96a799e5c27779ead0c43d33f9dd4 GIT binary patch literal 870 zcmZuv%Wl&^6g`uN?YM4}x@npg0u%})ZPNrOFSSC@@|2RY2m;ZalZ=9kaVp#41IPmL z0kFu11q&9e04bFyf<3?C|ERd*Jd9K%`_9a{XYRT8&i!-r;}?K++*FZ5PQfV!r)8W` z5kpRxMPbe+Fokm}mT+Fi1r@4bUKHoNjDm_~tjJhpm{~Ghmph)>w%xm?Yt${?WMI1t z(xz#f-Yte`zVMVGw%u-WhGfOG`A+9mojXqinH(N>J%-7eXEa_`jr{kFMpg|tg9bq70cPcTI;k$91^vvkVQ%4m%*AAo%oL}bWH0VrH^W9mCZXx@N_dZeO9tA~g^KR|q?4{4SD zKIENmPTd=3#2C!i&A_Eamp`l(v_92GvIjZ#8L{YhC}I3jH6m6V5$(1p>_i}c@-O@-zb60y literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/Main.java new file mode 100644 index 00000000000..28ea730c884 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/Main.java @@ -0,0 +1,9 @@ +public class Main { + public void test() { + String s1 = "ディフ"; + String s2 = "ブルー"; + String s3 = s1 + s2; + assert s3.length() == 6; + assert s3.startsWith("ディフブルー"); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/test.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/test.desc new file mode 100644 index 00000000000..936f1a33c06 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/test.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- From d9f75eb459feee99ee53921418b7ed94f2ad5b2f Mon Sep 17 00:00:00 2001 From: Yumi Bagge Date: Fri, 26 Jul 2019 17:10:11 +0100 Subject: [PATCH 9/9] Add regression test for non printable character --- .../Main.class | Bin 0 -> 837 bytes .../Main.java | 9 +++++++++ .../test.desc | 9 +++++++++ 3 files changed, 18 insertions(+) create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/Main.class create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/Main.java create mode 100644 jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/test.desc diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/Main.class new file mode 100644 index 0000000000000000000000000000000000000000..9a004221735a5adbc7cbe65618a872bc0ecd03b5 GIT binary patch literal 837 zcmZuvTTc@~6#iy=*$WFTZ7Btpq8;Hr*m7UC!>v!u** z6EnDBVHr1d+_GRP=52K@=_p%R!K#imhU~Hv1l*UR>jlq6;51#{W?%;l$!*~Y`Gg@> zD!*lj?{?dqAypF|-|v5Fa{rAYlSA@AGE6t5)B0FK@GG6$8*JseoLz|lPfD%-4IyP-Q#3P1ubmw*Rh_@*Bf1r^rRqynA+@n@hO10?1 z$h%d(0G%hgMMcZ*I7Y5?kw}cB%e{{L5H|J|gB3`}m%%%spt=94(J)d`4!bT*j3M9V zf$({IQaANq_Q^rxI=~W5KTWTMr3S}hZ+pCJDJ7>U&(l54bv(D#497$932!c2U{)CnviO#KegTqR=~N3!^Vj@Zuz^jWAPSHZwCsY5+a{4e{7d V7*YIjF)CI9n*CJObt#m;{1