Improvements in string preprocessing to facilitate constant propagation #984

romainbrenguier · 2017-06-01T15:38:42Z

This make string assignments take place in one step instead of field by field which makes constant propagation easier.
This also adds concatenation with start_index and end_index arguments in the solver.
~~This depends on pull requests #983 #980 #978 #906~~
and is part of the implementation of https://github.com/diffblue/test-gen/issues/256

This is a new implementation of the string preprocessing for Java functions. Which now takes place during java bytecode processing instead of being a step in the goto-program treatment. Rename code_of_function to code_for_function Update documentation Minor corrections on the code Make all methods non-static This is to allow using class variables in them. The conversion_functiont map had to be adapted. Use class variable for refined string type Instead of recreating a new refined string type each time it is requested, we add a field to hold it in java_string_library_preprocess. Squash in Replacement Replace code.copy_to_operands() with code.add() Correct implementation and usage of string_length_type()

…onversion Removing add_string_type declaration, not used anymore

Removing string_refine_preprocess from Makefile Removing include of string_refine_preprocess

Only one instance of this class should exist for a program.

We now do this at the end of the bytecode conversion, in function java_bytecode_languaget::final instead of the middle of the conversion.

String classes that are present in a loaded model will generate a type that may be different from the internal type constructed for Java strings in cbmc. Thus we now create a String type and write it in the table, possibly overwriting a pre-existing Java string type.

…e/test-gen#159 We now have a special way of dealing with contains in the case the argument is a constant, which seems to be much more efficient.

Adding constraints to make sure the index_of primitive of the string solver is precise. Also add specific constraints for constant argument in indexOf to improve performances in that case.

…hat they also get concretized

We now assign strings in one step instead of field by field. This makes constant propagation work better in later step of the analysis.

This adds a substring of the second argument. This will make the encoding of StringBuilder.append(CharSequence s, int start, int end) more efficient.

smowton · 2017-06-06T09:43:56Z

Ping me when deps merged?

smowton · 2017-06-07T10:50:46Z

Needs a rebase

romainbrenguier · 2017-06-07T13:09:20Z

Actually I think we will split this pull request into several smaller ones. Once this is done we will close this one.

cristina-david

This is pretty long so I was wondering if there is any way it can be split? For instance, the axioms for constant strings in string_constraint_generator_main.cpp appear in a different PR #828. Should this be rebased?

cristina-david · 2017-06-08T09:19:26Z

src/java_bytecode/java_bytecode_convert_method.cpp

+
+      // Replacing call if it is a function of the Character library,
+      // returning the same call otherwise
+      c=string_preprocess.replace_character_call(call);


Can we remove this here and do all the instrumentation in java_bytecode_language.cpp in a separate pass?

cristina-david · 2017-06-08T09:26:47Z