Cleanup in string preprocessing #2374

romainbrenguier · 2018-06-20T13:16:05Z

This removes broken or unused functions from the preprocessing

allredj

Passed Diffblue compatibility checks (cbmc commit: b00b5f1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77563791

allredj

Passed Diffblue compatibility checks (cbmc commit: abf0bb0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78068569

allredj

Passed Diffblue compatibility checks (cbmc commit: 6968a82).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78384602

allredj

Only formatting issues in the test. Otherwise looks good to me!

allredj · 2018-07-11T10:28:39Z

jbmc/regression/jbmc-strings/java_append_char/test_append_char.java

-      StringBuilder buffer = new StringBuilder();
+    public static String ofCharArray(char value[], int offset, int count) {
+      	org.cprover.CProver.assume(value != null);
+	org.cprover.CProver.assume(value.length - count >= offset


Bad indentation (in many places).

allredj · 2018-07-11T10:51:08Z

jbmc/regression/jbmc-strings/java_append_char/test_append_char.java

+	String s = ofCharArray(diff, 0, diff.length);
+	buffer.append(ofCharArray(diff, 0, diff.length))
+	    .append(ofCharArray(blue, 0, blue.length));
+	String tmp=buffer.toString();


Spaces around =

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 2a3420f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80857319
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

allredj

Passed Diffblue compatibility checks (cbmc commit: d26d482).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/81006696

peterschrammel · 2018-08-06T12:06:12Z

jbmc/regression/jbmc-strings/java_append_char/test_append_char.java

-      char[] blue = {'b', 'l', 'u', 'e'};
-
-      StringBuilder buffer = new StringBuilder();
+    public static String ofCharArray(char value[], int offset, int count) {


char[] value?

Both notations are acceptable.

peterschrammel · 2018-08-06T12:07:22Z

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

    checked_dereference(array_pointer, array_pointer.type().subtype());
  // array_data is array_pointer-> data
  const exprt array_data = get_data(array, symbol_table);
-  symbolt sym_char_array = get_fresh_aux_symbol(
+  const symbolt sym_char_array = get_fresh_aux_symbol(
    array_data.type(), "char_array", "char_array", loc, ID_java, symbol_table);


Must take function_id to prefix the symbol name

I propose to add a function that makes sure it's always the case. @peterschrammel Can you have a look at the last commit?

peterschrammel · 2018-08-06T12:07:46Z

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

-  symbolt sym_content = get_fresh_aux_symbol(
+  const symbol_exprt length_field = sym_length.symbol_expr();
+  const pointer_typet array_type = pointer_type(java_char_type());
+  const symbolt sym_content = get_fresh_aux_symbol(
    array_type,
    "cprover_string_content",
    "cprover_string_content",


function_id

peterschrammel · 2018-08-06T12:08:07Z

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -763,7 +766,7 @@ refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
  code_blockt &code)
 {
  // int return_code;
-  symbolt return_code_sym = get_fresh_aux_symbol(
+  const symbolt return_code_sym = get_fresh_aux_symbol(
    java_int_type(),
    std::string("return_code_") + function_name.c_str(),
    std::string("return_code_") + function_name.c_str(),


function_id

peterschrammel · 2018-08-06T12:08:22Z

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

-  symbolt class1_sym=get_fresh_aux_symbol(
+  const pointer_typet class_type =
+    java_reference_type(symbol_table.lookup_ref("java::java.lang.Class").type);
+  const symbolt class1_sym = get_fresh_aux_symbol(
    class_type, "class_symbol", "class_symbol", loc, ID_java, symbol_table);


function_id

allredj · 2018-08-06T13:06:47Z

jbmc/regression/jbmc-strings/java_append_char/test_append_char.java

-      char[] blue = {'b', 'l', 'u', 'e'};
-
-      StringBuilder buffer = new StringBuilder();
+    public static String ofCharArray(char value[], int offset, int count) {


Both notations are acceptable.

allredj · 2018-08-06T13:09:09Z

jbmc/regression/jbmc-strings/java_append_char/test_append_char.java

-      char[] blue = {'b', 'l', 'u', 'e'};
-
-      StringBuilder buffer = new StringBuilder();
+    public static String ofCharArray(char value[], int offset, int count) {


I'm not sure what this whole change is about. The regression is not clear as to its purpose. Also you mention the test uses CProverString but I don't see where.

Also I fail to see how the commit and the commit message are related.

Yes you are right, I updated java-models-library so that we don't have to change this test.

allredj

Passed Diffblue compatibility checks (cbmc commit: 70f2b64).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84258693

allredj

This PR failed Diffblue compatibility checks (cbmc commit: a04f3c0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84407246
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

allredj

Passed Diffblue compatibility checks (cbmc commit: 6cb91f5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86574191

allredj

Passed Diffblue compatibility checks (cbmc commit: 6146855).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86718492

romainbrenguier · 2018-10-03T10:51:23Z

@allredj @peterschrammel this is ready for review

allredj

Looks good!
diffblue/java-models-library#9 must be merged first.

peterschrammel · 2018-10-09T08:19:08Z

jbmc/src/java_bytecode/java_utils.cpp

+  const source_locationt &source_location,
+  symbol_table_baset &symbol_table)
+{
+  const std::string name_prefix = id2string(source_location.get_function());


🚫 Unfortunately, this is in conflict with #2149
@tautschnig, we must come to a decision there.

I strongly believe that the information in the source_location is a string aimed at the user, and should relate to whatever is found in the source. The actual identifier of the function (the key in goto_functionst::function_map) used internally may be entirely different. I don't know which one is required here.

Here, something is required that is unique to a goto function. Reason: adding a function to a goto model must not affect the identifiers of another function. This was the source of many goto-diff bugs in the past.

Then a function_id must be passed in. In some call sites in this PR this would be symbol.name, others require further digging.

romainbrenguier · 2018-10-16T15:38:11Z

@peterschrammel the part that I think is most important in this PR is independent of the problem with symbols, so I put this part in another #3189
Can you check there is nothing blocking in the commits that are left?

allredj

Passed Diffblue compatibility checks (cbmc commit: 8475bc1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88137195

…of char array) diffblue/java-models-library#9

Conversion from char array to string does not work, because the string refinement is not aware of the operations performed on the arrays. To construct strings from char array, the constructors have to be implemented using loops instead.

romainbrenguier · 2018-10-17T17:29:57Z

Now pointing to diffblue/java-models-library#master

allredj

Passed Diffblue compatibility checks (cbmc commit: f6c3023).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88298542

romainbrenguier requested review from cesaro, mgudemann, peterschrammel, smowton and thk123 as code owners June 20, 2018 13:16

romainbrenguier force-pushed the clean-up/preprocessing branch from 4defa93 to b00b5f1 Compare June 28, 2018 08:32

allredj reviewed Jun 28, 2018

View reviewed changes

romainbrenguier force-pushed the clean-up/preprocessing branch from b00b5f1 to abf0bb0 Compare July 4, 2018 08:27

allredj reviewed Jul 4, 2018

View reviewed changes

romainbrenguier force-pushed the clean-up/preprocessing branch from abf0bb0 to 6968a82 Compare July 8, 2018 09:00

romainbrenguier requested review from cristina-david, NathanJPhillips, pkesseli and a team as code owners July 8, 2018 09:00

allredj reviewed Jul 8, 2018

View reviewed changes

allredj suggested changes Jul 11, 2018

View reviewed changes

romainbrenguier force-pushed the clean-up/preprocessing branch from 6968a82 to 2a3420f Compare August 3, 2018 09:33

allredj reviewed Aug 3, 2018

View reviewed changes

romainbrenguier force-pushed the clean-up/preprocessing branch 2 times, most recently from 8dc4b9d to d26d482 Compare August 6, 2018 09:14

allredj reviewed Aug 6, 2018

View reviewed changes

romainbrenguier force-pushed the clean-up/preprocessing branch from d26d482 to b0afa53 Compare August 6, 2018 12:02

peterschrammel reviewed Aug 6, 2018

View reviewed changes

allredj reviewed Aug 6, 2018

View reviewed changes

romainbrenguier force-pushed the clean-up/preprocessing branch 3 times, most recently from e5a88ab to 8115027 Compare August 9, 2018 09:44

romainbrenguier requested review from chrisr-diffblue, kroening and tautschnig as code owners August 9, 2018 09:44

allredj reviewed Sep 10, 2018

View reviewed changes

romainbrenguier force-pushed the clean-up/preprocessing branch from 70f2b64 to a04f3c0 Compare September 11, 2018 09:17

allredj reviewed Sep 11, 2018

View reviewed changes

tautschnig assigned romainbrenguier and allredj Sep 24, 2018

romainbrenguier force-pushed the clean-up/preprocessing branch from a04f3c0 to 6cb91f5 Compare October 2, 2018 07:57

allredj reviewed Oct 2, 2018

View reviewed changes

romainbrenguier force-pushed the clean-up/preprocessing branch from 6cb91f5 to 6146855 Compare October 3, 2018 08:54

allredj reviewed Oct 3, 2018

View reviewed changes

allredj added the do not merge label Oct 4, 2018

allredj approved these changes Oct 4, 2018

View reviewed changes

peterschrammel reviewed Oct 9, 2018

View reviewed changes

peterschrammel assigned romainbrenguier and unassigned romainbrenguier and allredj Oct 9, 2018

romainbrenguier force-pushed the clean-up/preprocessing branch from 6146855 to 8475bc1 Compare October 16, 2018 15:30

romainbrenguier mentioned this pull request Oct 16, 2018

Cleanup in string preprocessing #3189

Merged

6 tasks

allredj reviewed Oct 16, 2018

View reviewed changes

peterschrammel approved these changes Oct 17, 2018

View reviewed changes

romainbrenguier added 3 commits October 17, 2018 18:28

Update jbmc/lib/java-models-library to java-models-library#9 (String …

6d86626

…of char array) diffblue/java-models-library#9

Stop preprocessing for unsupported functions

bd292f7

Conversion from char array to string does not work, because the string refinement is not aware of the operations performed on the arrays. To construct strings from char array, the constructors have to be implemented using loops instead.

Remove unused functions

f6c3023

romainbrenguier force-pushed the clean-up/preprocessing branch from 8475bc1 to f6c3023 Compare October 17, 2018 17:28

romainbrenguier removed the do not merge label Oct 17, 2018

allredj reviewed Oct 17, 2018

View reviewed changes

romainbrenguier merged commit c6a220c into diffblue:develop Oct 18, 2018

romainbrenguier deleted the clean-up/preprocessing branch October 18, 2018 05:32

Cleanup in string preprocessing #2374

Cleanup in string preprocessing #2374

Uh oh!

Conversation

romainbrenguier commented Jun 20, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

romainbrenguier commented Oct 3, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

romainbrenguier commented Oct 16, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!