Add a switch for fixed strings on input #3540

forejtv · 2018-12-06T16:20:42Z

This adds a --string-input-value switch for jbmc that allows to specify one or more fixed values that are considered for input strings, instead of an unbounded range of (possibly non-sensical) strings whose choice is at a mercy of the SAT solver.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 67e1a6b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/93866539

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 6f399ef).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/93876986
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).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 1f16d74).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/93899261

romainbrenguier

Needs more tests and some refactoring to not make gen_nondet_struct_init longer when it is already more than 100 lines. I suggest putting the code you want to add in a helper function.

romainbrenguier · 2018-12-07T07:48:16Z

jbmc/src/java_bytecode/java_object_factory.cpp

    CHECK_RETURN(initial_object.has_value());
    irep_idt qualified_clsid = "java::" + id2string(class_identifier);
    set_class_identifier(
      to_struct_expr(*initial_object), ns, symbol_typet(qualified_clsid));

-    // If the initialised type is a special-cased String type (one with length
-    // and data fields introduced by string-library preprocessing), initialise
-    // those fields with nondet values:


I think it's better to keep this comment

romainbrenguier · 2018-12-07T07:48:57Z

jbmc/src/java_bytecode/java_object_factory.cpp

+    }
+    // in the else case we have
+    // '!is_char_sequence || !has_data_length'
+    // and so we are not dealing with a string


this comment is not useful

romainbrenguier · 2018-12-07T07:51:15Z

jbmc/src/java_bytecode/java_object_factory.cpp

    // Add an initial all-zero write. Most of the fields of this will be
    // overwritten, but it helps to have a whole-structure write that analysis
    // passes can easily recognise leaves no uninitialised state behind.

    // This code mirrors the `remove_java_new` pass:
-    auto initial_object = zero_initializer(struct_type, source_locationt(), ns);
+    auto initial_object =
+      zero_initializer(struct_type, source_locationt(), ns);


⛏️ don't introduce reformatting if you don't touch these lines

romainbrenguier · 2018-12-07T07:51:33Z

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1009,29 +1005,40 @@ void java_object_factoryt::gen_nondet_struct_init(
  {
    class_identifier = struct_tag;

+    bool is_char_sequence =


romainbrenguier · 2018-12-07T07:52:19Z

jbmc/src/java_bytecode/java_object_factory.cpp

+    bool is_char_sequence =
+      java_string_library_preprocesst
+        ::implements_java_char_sequence(struct_type);
+    bool has_data_length =


const and ⛏️ rename has_length_and_data

romainbrenguier · 2018-12-07T08:13:06Z

jbmc/src/java_bytecode/java_object_factory.cpp

+        exprt name_literal(ID_java_string_literal);
+        name_literal.set(ID_value, val);
+        symbol_exprt s =
+          get_or_create_string_literal_symbol(name_literal, symbol_table, true);


jbmc/src/jbmc/jbmc_parse_options.cpp

romainbrenguier · 2018-12-07T08:17:44Z

src/solvers/refinement/string_refinement.h

  "(string-non-empty)" \
  "(max-nondet-string-length):"

 #define HELP_STRING_REFINEMENT \
  " --no-refine-strings          turn off string refinement\n" \
  " --string-printable           restrict to printable strings (experimental)\n" /* NOLINT(*) */ \
  " --string-non-empty           restrict to non-empty strings (experimental)\n" /* NOLINT(*) */ \
+  " --string-printable st        restrict non-null strings to a fixed value(s)\n" /* NOLINT(*) */ \


the help message should mention st, and should be made clearer for the multiple values case

romainbrenguier · 2018-12-07T08:18:34Z

jbmc/src/java_bytecode/java_object_factory.cpp

+      }
+      // in the else case we have
+      // '!is_char_sequence || !has_data_length'
+      // and so we are not dealing with a string


romainbrenguier · 2018-12-07T08:23:50Z

jbmc/src/java_bytecode/java_object_factory.cpp

-    irep_idt qualified_clsid = "java::" + id2string(class_identifier);
-    set_class_identifier(
-      to_struct_expr(*initial_object), ns, symbol_typet(qualified_clsid));
+    if(!is_char_sequence || !has_data_length || no_input_values)


⛏️ I think doing the special case first would be clearer

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: fdc941c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/94099113

peterschrammel · 2018-12-09T00:12:55Z

jbmc/src/jbmc/jbmc_parse_options.cpp

  {
-    warning() << "--string-printable ignored due to --no-refine-strings" << eom;
+    if(cmdline.isset("no-refine-strings"))


⚠️ There are 3 independent refactorings in this commit. Split them.

Good point. I've split this into two commits, since I think the two refactorings related to initialize_nondet_string_fields are too closely related to be done separately: one changes the caller to handle the informal preconditions, and one changes the callee to turn informal preconditions to proper preconditions.

peterschrammel · 2018-12-09T00:16:35Z

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -131,6 +131,21 @@ static void java_static_lifetime_init(
  code_blockt &code_block=to_code_block(to_code(initialize_symbol.value));
  object_factory_parameters.function_id = initialize_symbol.name;

+  // If there are strings given using --string-input-value, we need to add
+  // them to the symbol table now, so that they appear in __CPROVER_initialize
+  // and we can refer to them later when we initialise input values.


⛏️ initialize

peterschrammel · 2018-12-09T00:19:40Z

jbmc/src/java_bytecode/java_object_factory.cpp

+    {
+      // Add an initial all-zero write. Most of the fields of this will be
+      // overwritten, but it helps to have a whole-structure write that analysis
+      // passes can easily recognise leaves no uninitialised state behind.


I struggle to understand this sentence.

Me too :-) The sentence was there before, I've only put it in an else block and hence indentation changed. I don't know how to improve the sentence since I don't have good enough understanding of the code.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: fe74137).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/94119132

Just moving it by a few lines to make the code easier to follow.

…lled. Before, initialize_nondet_string_fields would check itself if the argument is a string, and would return true/false depending on whether any change was applied. Now the function asserts in precondition that the arguments are applicable, and the caller is responsible for checking this.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: f42b870).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/94121222

forejtv · 2018-12-09T21:38:59Z

@romainbrenguier @peterschrammel This is now ready to re-review.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 82a09fd).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/94127897

romainbrenguier · 2018-12-10T15:29:38Z

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -564,7 +564,7 @@ static mp_integer max_value(const typet &type)
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 /// Unit tests in `unit/java_bytecode/java_object_factory/` ensure
 /// it is the case.
-bool initialize_nondet_string_fields(
+void initialize_nondet_string_fields(


Update the documentation

romainbrenguier · 2018-12-10T15:31:52Z

jbmc/src/java_bytecode/java_entry_point.cpp

+  for(const auto &val : object_factory_parameters.string_input_values)
+  {
+    exprt my_literal(ID_java_string_literal);
+    my_literal.set(ID_value, val);


💡 ideally there would be a java_string_literal_exprt type

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

jbmc/regression/jbmc-strings/string-input-value/test1.desc

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--verbosity 10 --string-input-value fo --string-input-value barr --function Test.checkStringInputValue --string-input-value "" --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`


⛏️ Could we also have a test.desc where "" (and maybe others) are not given as string-input-value to see the difference?

romainbrenguier · 2018-12-10T15:40:03Z

jbmc/src/java_bytecode/java_object_factory.cpp

+      // We create a switch statement where each case is an assignment
+      // of one of the fixed input strings to the input variable in question
+
+      alternate_casest cases =


allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 0ad4ec1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/94254247

forejtv requested review from cesaro, cristina-david, kroening, martin-cs, NathanJPhillips, peterschrammel, pkesseli, romainbrenguier, smowton, tautschnig and thk123 as code owners December 6, 2018 16:20

forejtv force-pushed the forejtv/fixed-strings branch from 67e1a6b to 6f399ef Compare December 6, 2018 17:09

allredj reviewed Dec 6, 2018

View reviewed changes

forejtv force-pushed the forejtv/fixed-strings branch from 6f399ef to 8baaadd Compare December 6, 2018 17:16

allredj reviewed Dec 6, 2018

View reviewed changes

forejtv force-pushed the forejtv/fixed-strings branch from 8baaadd to 1f16d74 Compare December 6, 2018 18:50

allredj reviewed Dec 6, 2018

View reviewed changes

romainbrenguier suggested changes Dec 7, 2018

View reviewed changes

forejtv force-pushed the forejtv/fixed-strings branch 6 times, most recently from 1f617cf to fdc941c Compare December 8, 2018 23:06

allredj reviewed Dec 9, 2018

View reviewed changes

peterschrammel reviewed Dec 9, 2018

View reviewed changes

forejtv force-pushed the forejtv/fixed-strings branch from fdc941c to fe74137 Compare December 9, 2018 16:02

allredj reviewed Dec 9, 2018

View reviewed changes

Vojtech Forejt added 2 commits December 9, 2018 17:22

Move string-printable and no-refine-strings compatibility check.

4e5e26c

Just moving it by a few lines to make the code easier to follow.

forejtv force-pushed the forejtv/fixed-strings branch from fe74137 to f42b870 Compare December 9, 2018 17:30

allredj reviewed Dec 9, 2018

View reviewed changes

forejtv force-pushed the forejtv/fixed-strings branch from f42b870 to 82a09fd Compare December 9, 2018 21:06

allredj reviewed Dec 9, 2018

View reviewed changes

romainbrenguier approved these changes Dec 10, 2018

View reviewed changes

Add a switch for fixed strings on input

9c1d488

forejtv force-pushed the forejtv/fixed-strings branch from 82a09fd to b8d8dcc Compare December 10, 2018 18:51

Test for --string-input-value

0ad4ec1

forejtv force-pushed the forejtv/fixed-strings branch from b8d8dcc to 0ad4ec1 Compare December 10, 2018 20:25

allredj reviewed Dec 10, 2018

View reviewed changes

peterschrammel approved these changes Dec 11, 2018

View reviewed changes

peterschrammel assigned forejtv Dec 11, 2018

forejtv merged commit 6e085d2 into develop Dec 11, 2018

Add a switch for fixed strings on input #3540

Add a switch for fixed strings on input #3540

Uh oh!

Conversation

forejtv commented Dec 6, 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!

romainbrenguier 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!

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!

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!

forejtv commented Dec 9, 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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!