diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/Test.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/Test.class new file mode 100644 index 00000000000..b91b6eaff34 Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/Test.class differ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/Test.java b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/Test.java new file mode 100644 index 00000000000..e7e5f9b591b --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/Test.java @@ -0,0 +1,30 @@ +public class Test +{ + public void testSuccess() + { + StringBuffer sb = new StringBuffer("abc"); + sb.deleteCharAt(1); + assert sb.toString().equals("ac"); + } + + public void testNoPropagation(int index) + { + StringBuffer sb = new StringBuffer("abc"); + sb.deleteCharAt(index); + assert sb.toString().equals("ac"); + } + + public void testIndexOutOfBounds1() + { + StringBuffer sb = new StringBuffer("abc"); + sb.deleteCharAt(-1); + assert sb.toString().equals("ac"); + } + + public void testIndexOutOfBounds2() + { + StringBuffer sb = new StringBuffer("abc"); + sb.deleteCharAt(3); + assert sb.toString().equals("ac"); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/test_index_out_of_bounds1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/test_index_out_of_bounds1.desc new file mode 100644 index 00000000000..b8c4ebf0e05 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/test_index_out_of_bounds1.desc @@ -0,0 +1,8 @@ +CORE +Test.class +--function Test.testIndexOutOfBounds1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/test_index_out_of_bounds2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/test_index_out_of_bounds2.desc new file mode 100644 index 00000000000..8b853aa4027 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/test_index_out_of_bounds2.desc @@ -0,0 +1,8 @@ +CORE +Test.class +--function Test.testIndexOutOfBounds2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/test_no_propagation.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/test_no_propagation.desc new file mode 100644 index 00000000000..3d80a6238e0 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/test_no_propagation.desc @@ -0,0 +1,9 @@ +CORE symex-driven-lazy-loading-expected-failure +Test.class +--function Test.testNoPropagation --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testNoPropagation:(I)V.assertion.1' +^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/test_success.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/test_success.desc new file mode 100644 index 00000000000..8d1b5b06f48 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/test_success.desc @@ -0,0 +1,9 @@ +CORE +Test.class +--function Test.testSuccess --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/ConstantEvaluationStringBuilderDeleteCharAt/Test.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/Test.class new file mode 100644 index 00000000000..e6d24c4c57e Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/Test.class differ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/Test.java b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/Test.java new file mode 100644 index 00000000000..3b2078054d2 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/Test.java @@ -0,0 +1,30 @@ +public class Test +{ + public void testSuccess() + { + StringBuilder sb = new StringBuilder("abc"); + sb.deleteCharAt(1); + assert sb.toString().equals("ac"); + } + + public void testNoPropagation(int index) + { + StringBuilder sb = new StringBuilder("abc"); + sb.deleteCharAt(index); + assert sb.toString().equals("ac"); + } + + public void testIndexOutOfBounds1() + { + StringBuilder sb = new StringBuilder("abc"); + sb.deleteCharAt(-1); + assert sb.toString().equals("ac"); + } + + public void testIndexOutOfBounds2() + { + StringBuilder sb = new StringBuilder("abc"); + sb.deleteCharAt(3); + assert sb.toString().equals("ac"); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/test_index_out_of_bounds1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/test_index_out_of_bounds1.desc new file mode 100644 index 00000000000..b8c4ebf0e05 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/test_index_out_of_bounds1.desc @@ -0,0 +1,8 @@ +CORE +Test.class +--function Test.testIndexOutOfBounds1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/test_index_out_of_bounds2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/test_index_out_of_bounds2.desc new file mode 100644 index 00000000000..8b853aa4027 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/test_index_out_of_bounds2.desc @@ -0,0 +1,8 @@ +CORE +Test.class +--function Test.testIndexOutOfBounds2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/test_no_propagation.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/test_no_propagation.desc new file mode 100644 index 00000000000..3d80a6238e0 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/test_no_propagation.desc @@ -0,0 +1,9 @@ +CORE symex-driven-lazy-loading-expected-failure +Test.class +--function Test.testNoPropagation --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testNoPropagation:(I)V.assertion.1' +^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/test_success.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/test_success.desc new file mode 100644 index 00000000000..8d1b5b06f48 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/test_success.desc @@ -0,0 +1,9 @@ +CORE +Test.class +--function Test.testSuccess --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/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index ceb7a726d1e..ba95025accf 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -191,6 +191,10 @@ bool goto_symext::constant_propagate_assignment_with_side_effects( { return constant_propagate_integer_to_string(state, symex_assign, f_l1); } + else if(func_id == ID_cprover_string_delete_char_at_func) + { + return constant_propagate_delete_char_at(state, symex_assign, f_l1); + } } } @@ -588,3 +592,76 @@ bool goto_symext::constant_propagate_integer_to_string( return true; } + +bool goto_symext::constant_propagate_delete_char_at( + statet &state, + symex_assignt &symex_assign, + const function_application_exprt &f_l1) +{ + // The function application expression f_l1 takes the following arguments: + // - result string length (output parameter) + // - result string data array (output parameter) + // - string to delete char from + // - index of char to delete + PRECONDITION(f_l1.arguments().size() == 4); + + 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(); + + const auto &index_opt = try_evaluate_constant(state, f_l1.arguments().at(3)); + + if(!index_opt) + { + return false; + } + + const mp_integer index = numeric_cast_v(index_opt->get()); + + if(index < 0 || index >= s_data.operands().size()) + { + return false; + } + + const constant_exprt new_char_array_length = + from_integer(s_data.operands().size() - 1, length_type); + + const array_typet new_char_array_type(char_type, new_char_array_length); + + exprt::operandst operands; + operands.reserve(s_data.operands().size() - 1); + + const std::size_t i = numeric_cast_v(index); + + operands.insert( + operands.end(), + s_data.operands().begin(), + std::next(s_data.operands().begin(), i)); + + operands.insert( + operands.end(), + std::next(s_data.operands().begin(), i + 1), + s_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 31762d5133d..4b37e1659a2 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -597,6 +597,19 @@ class goto_symext symex_assignt &symex_assign, const function_application_exprt &f_l1); + /// Attempt to constant propagate deleting a character from a string + /// + /// \param state: goto symex state + /// \param symex_assign: object handling symbol assignments + /// \param f_l1: application of function ID_cprover_string_delete_char_at_func + /// with l1 renaming applied + /// \return true if the operation could be evaluated to a constant string, + /// false otherwise + bool constant_propagate_delete_char_at( + 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 ///