diff --git a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation1/Main.class b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation1/Main.class new file mode 100644 index 00000000000..6ae3c5981f8 Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation1/Main.class differ diff --git a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation1/Main.java b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation1/Main.java new file mode 100644 index 00000000000..73e77e82028 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation1/Main.java @@ -0,0 +1,25 @@ +public class Main { + public void test() { + StringBuilder sb = new StringBuilder("abc"); + + String s1 = sb.substring(0); + assert s1.length() == 3; + assert s1.startsWith("abc"); + + String s2 = sb.substring(1); + assert s2.length() == 2; + assert s2.startsWith("bc"); + + String s3 = sb.substring(0, 3); + assert s3.length() == 3; + assert s3.startsWith("abc"); + + String s4 = sb.substring(0, 0); + assert s4.length() == 0; + assert s4.startsWith(""); + + String s5 = sb.substring(0, 1); + assert s5.length() == 1; + assert s5.startsWith("a"); + } +} diff --git a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation1/test.desc b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation1/test.desc new file mode 100644 index 00000000000..27a6bb0db9b --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation1/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/StringBuilderSubstringConstantEvaluation2/Main.class b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/Main.class new file mode 100644 index 00000000000..0dc564ae6d0 Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/Main.class differ diff --git a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/Main.java b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/Main.java new file mode 100644 index 00000000000..b646f14e0b7 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/Main.java @@ -0,0 +1,18 @@ +public class Main { + public void test1(StringBuilder sb) { + String s = sb.substring(0); + assert s.startsWith("xyz"); + } + + public void test2(int i) { + StringBuilder sb = new StringBuilder("abc"); + + String s = sb.substring(i); + assert s.startsWith("xyz"); + } + + public void test3(StringBuilder sb, int i) { + String s = sb.substring(i); + assert s.startsWith("xyz"); + } +} diff --git a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test1.desc b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test1.desc new file mode 100644 index 00000000000..77378287522 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test1.desc @@ -0,0 +1,9 @@ +CORE symex-driven-lazy-loading-expected-failure +Main.class +--function Main.test1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test1:(Ljava/lang/StringBuilder;)V.assertion.1" +^Generated 1 VCC\(s\), 1 remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test2.desc b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test2.desc new file mode 100644 index 00000000000..e1bbac2c42c --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test2.desc @@ -0,0 +1,9 @@ +CORE symex-driven-lazy-loading-expected-failure +Main.class +--function Main.test2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test2:(I)V.assertion.1" +^Generated 1 VCC\(s\), 1 remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test3.desc b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test3.desc new file mode 100644 index 00000000000..3556eee536e --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test3.desc @@ -0,0 +1,9 @@ +CORE symex-driven-lazy-loading-expected-failure +Main.class +--function Main.test3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test3:(Ljava/lang/StringBuilder;I)V.assertion.1" +^Generated 1 VCC\(s\), 1 remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation3/Main.class b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation3/Main.class new file mode 100644 index 00000000000..888bc378aa7 Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation3/Main.class differ diff --git a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation3/Main.java b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation3/Main.java new file mode 100644 index 00000000000..c85322865ea --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation3/Main.java @@ -0,0 +1,16 @@ +public class Main { + public void test1() { + StringBuilder sb = new StringBuilder("abc"); + sb.substring(-1); + } + + public void test2() { + StringBuilder sb = new StringBuilder("abc"); + sb.substring(4); + } + + public void test3() { + StringBuilder sb = new StringBuilder("abc"); + sb.substring(-1, 4); + } +} diff --git a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation3/test1.desc b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation3/test1.desc new file mode 100644 index 00000000000..f4496a5678e --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation3/test1.desc @@ -0,0 +1,13 @@ +FUTURE +Main.class +--function Main.test1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9][0-9]* VCC\(s\), 1 remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +no uncaught exception: FAILURE +^VERIFICATION FAILED$ +-- +-- +This test will pass once a model for StringBuilder.substring() exists that +throws an exception when the index is greater or equal to the length of the +string. diff --git a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation3/test2.desc b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation3/test2.desc new file mode 100644 index 00000000000..a6de7f9da9c --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation3/test2.desc @@ -0,0 +1,13 @@ +FUTURE +Main.class +--function Main.test2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9][0-9]* VCC\(s\), 1 remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +no uncaught exception: FAILURE +^VERIFICATION FAILED$ +-- +-- +This test will pass once a model for StringBuilder.substring() exists that +throws an exception when the index is greater or equal to the length of the +string. diff --git a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation3/test3.desc b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation3/test3.desc new file mode 100644 index 00000000000..6d10db559ac --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation3/test3.desc @@ -0,0 +1,13 @@ +FUTURE +Main.class +--function Main.test3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9][0-9]* VCC\(s\), 1 remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +no uncaught exception: FAILURE +^VERIFICATION FAILED$ +-- +-- +This test will pass once a model for StringBuilder.substring() exists that +throws an exception when the index is greater or equal to the length of the +string. diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation1/Main.class b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation1/Main.class new file mode 100644 index 00000000000..03a2bc0f9de Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation1/Main.class differ diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation1/Main.java b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation1/Main.java new file mode 100644 index 00000000000..9f8f3d81c5f --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation1/Main.java @@ -0,0 +1,20 @@ +public class Main { + public void test() { + String s = "abc"; + + String s1 = s.substring(0); + assert s1.equals("abc"); + + String s2 = s.substring(1); + assert s2.equals("bc"); + + String s3 = s.substring(0, 3); + assert s3.equals("abc"); + + String s4 = s.substring(0, 0); + assert s4.equals(""); + + String s5 = s.substring(0, 1); + assert s5.equals("a"); + } +} diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation1/test.desc b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation1/test.desc new file mode 100644 index 00000000000..fb11e5707f3 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation1/test.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test --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$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/Main.class b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/Main.class new file mode 100644 index 00000000000..9f0062e01d4 Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/Main.class differ diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/Main.java b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/Main.java new file mode 100644 index 00000000000..8e7986732bc --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/Main.java @@ -0,0 +1,18 @@ +public class Main { + public void test1(String s1) { + String s2 = s1.substring(0); + assert s2.startsWith("xyz"); + } + + public void test2(int i) { + String s1 = "abc"; + + String s2 = s1.substring(i); + assert s2.startsWith("xyz"); + } + + public void test3(String s1, int i) { + String s2 = s1.substring(i); + assert s2.startsWith("xyz"); + } +} diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test1.desc b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test1.desc new file mode 100644 index 00000000000..cfb19c179e3 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test1.desc @@ -0,0 +1,9 @@ +CORE symex-driven-lazy-loading-expected-failure +Main.class +--function Main.test1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test1:(Ljava/lang/String;)V.assertion.1" +^Generated 1 VCC\(s\), 1 remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test2.desc b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test2.desc new file mode 100644 index 00000000000..e1bbac2c42c --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test2.desc @@ -0,0 +1,9 @@ +CORE symex-driven-lazy-loading-expected-failure +Main.class +--function Main.test2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test2:(I)V.assertion.1" +^Generated 1 VCC\(s\), 1 remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test3.desc b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test3.desc new file mode 100644 index 00000000000..9b08f22a808 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test3.desc @@ -0,0 +1,9 @@ +CORE symex-driven-lazy-loading-expected-failure +Main.class +--function Main.test3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test3:(Ljava/lang/String;I)V.assertion.1" +^Generated 1 VCC\(s\), 1 remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation3/Main.class b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation3/Main.class new file mode 100644 index 00000000000..0bced82999a Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation3/Main.class differ diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation3/Main.java b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation3/Main.java new file mode 100644 index 00000000000..64119b8aa6e --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation3/Main.java @@ -0,0 +1,16 @@ +public class Main { + public void test1() { + String s1 = "abc"; + s1.substring(-1); + } + + public void test2() { + String s1 = "abc"; + s1.substring(4); + } + + public void test3() { + String s1 = "abc"; + s1.substring(-1, 4); + } +} diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation3/test1.desc b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation3/test1.desc new file mode 100644 index 00000000000..ed4f1edd0fd --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation3/test1.desc @@ -0,0 +1,10 @@ +CORE +Main.class +--function Main.test1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9][0-9]* VCC\(s\), 1 remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +no uncaught exception: FAILURE +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation3/test2.desc b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation3/test2.desc new file mode 100644 index 00000000000..50600f75708 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation3/test2.desc @@ -0,0 +1,10 @@ +CORE +Main.class +--function Main.test2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9][0-9]* VCC\(s\), 1 remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +no uncaught exception: FAILURE +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation3/test3.desc b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation3/test3.desc new file mode 100644 index 00000000000..6d6e3889acd --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation3/test3.desc @@ -0,0 +1,10 @@ +CORE +Main.class +--function Main.test3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9][0-9]* VCC\(s\), 1 remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +no uncaught exception: FAILURE +^VERIFICATION FAILED$ +-- +-- diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index 171aca2a2ab..515e89f0656 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -181,6 +181,10 @@ bool goto_symext::constant_propagate_assignment_with_side_effects( constant_propagate_empty_string(state, symex_assign, f_l1); return true; } + else if(func_id == ID_cprover_string_substring_func) + { + return constant_propagate_string_substring(state, symex_assign, f_l1); + } } } @@ -310,6 +314,26 @@ goto_symext::try_evaluate_constant_string( return try_get_string_data_array(s_pointer_opt->get(), ns); } +optionalt> +goto_symext::try_evaluate_constant(const statet &state, const exprt &expr) +{ + if(expr.id() != ID_symbol) + { + return {}; + } + + const auto constant_expr_opt = + state.propagation.find(to_symbol_expr(expr).get_identifier()); + + if(!constant_expr_opt || constant_expr_opt->get().id() != ID_constant) + { + return {}; + } + + return optionalt>( + to_constant_expr(constant_expr_opt->get())); +} + void goto_symext::constant_propagate_empty_string( statet &state, symex_assignt &symex_assign, @@ -387,3 +411,90 @@ bool goto_symext::constant_propagate_string_concat( return true; } + +bool goto_symext::constant_propagate_string_substring( + statet &state, + symex_assignt &symex_assign, + const function_application_exprt &f_l1) +{ + const std::size_t num_operands = f_l1.arguments().size(); + + PRECONDITION(num_operands >= 4); + PRECONDITION(num_operands <= 5); + + 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 &s = to_string_expr(f_l1.arguments().at(2)); + const auto s_data_opt = try_evaluate_constant_string(state, s.content()); + + if(!s_data_opt) + return false; + + const array_exprt &s_data = s_data_opt->get(); + + mp_integer end_index; + + if(num_operands == 5) + { + const auto end_index_expr_opt = + try_evaluate_constant(state, f_l1.arguments().at(4)); + + if(!end_index_expr_opt) + { + return false; + } + + end_index = + numeric_cast_v(to_constant_expr(*end_index_expr_opt)); + + if(end_index < 0 || end_index > s_data.operands().size()) + { + return false; + } + } + else + { + end_index = s_data.operands().size(); + } + + const auto start_index_expr_opt = + try_evaluate_constant(state, f_l1.arguments().at(3)); + + if(!start_index_expr_opt) + { + return false; + } + + const mp_integer start_index = + numeric_cast_v(to_constant_expr(*start_index_expr_opt)); + + if(start_index < 0 || start_index > end_index) + { + return false; + } + + const constant_exprt new_char_array_length = + from_integer(end_index - start_index, length_type); + + const array_typet new_char_array_type(char_type, new_char_array_length); + + exprt::operandst operands( + std::next( + s_data.operands().begin(), numeric_cast_v(start_index)), + std::next( + s_data.operands().begin(), numeric_cast_v(end_index))); + + 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 de1942a02cb..364a83b4376 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -568,6 +568,19 @@ class goto_symext symex_assignt &symex_assign, const function_application_exprt &f_l1); + /// Attempt to constant propagate getting a substring of a string + /// + /// \param state: goto symex state + /// \param symex_assign: object handling symbol assignments + /// \param f_l1: application of function ID_cprover_string_substring_func with + /// l1 renaming applied + /// \return true if the operation could be evaluated to a constant string, + /// false otherwise + bool constant_propagate_string_substring( + 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 /// @@ -627,6 +640,13 @@ class goto_symext optionalt> try_evaluate_constant_string(const statet &state, const exprt &content); + // clang-format off + static optionalt> + try_evaluate_constant( + const statet &state, + const exprt &expr); + // clang-format on + // havocs the given object void havoc_rec(statet &state, const guardt &guard, const exprt &dest);