TG-58 Complete rework of string solver to avoid using infinite arrays #1420

romainbrenguier · 2017-09-25T07:44:03Z

This makes the string solver algorithm work only on finite size arrays. The input program may have pointers and infinite arrays in which case the solver associate finite arrays to them.
The type for the String class in java-bytecode is changed to contain a char pointer instead of a pointer to an infinite array, however infinite array are still present there for non-deterministic assignment.

smowton

Reviewed about a quarter of this. It's just too big. Don't have time to leaf through the rest; suggest finding another reviewer to pick up where I left off, or find a way to split the huge 3000-line commit in the middle of this into stages so each can be reviewed individually.

smowton · 2017-09-26T10:07:59Z

regression/strings-smoke-tests/java_append_char/test_append_char.java

Bad indentation in this function

smowton · 2017-09-26T10:08:54Z

regression/strings-smoke-tests/java_char_array/test_char_array.java

smowton · 2017-09-26T10:09:10Z

regression/strings-smoke-tests/java_if/test.java

smowton · 2017-09-26T10:09:22Z

regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.java

smowton · 2017-09-26T10:10:09Z

regression/strings/StringMiscellaneous04/StringMiscellaneous04.java

smowton · 2017-09-26T13:51:33Z

src/util/string_expr.h

const typet &?

smowton · 2017-09-26T13:54:24Z

src/solvers/refinement/string_constraint_generator_main.cpp

If you're expecting this to be a fresh insert, check insert's return value

smowton · 2017-09-26T13:54:33Z

src/solvers/refinement/string_constraint_generator_main.cpp

again, check insert's return value

smowton · 2017-09-26T13:58:29Z

src/java_bytecode/java_object_factory.cpp

Always follow; take return by const ref

smowton · 2017-09-26T13:59:23Z

unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp

You shouldn't need to do this -- jlo is always in the class loader's queue

Not sure we have a class loader here (did you see we are in a unit test?)

jasigal

First pass, I need to better understand more of the string refinement changes to comment on structure.

jasigal · 2017-09-27T12:06:33Z

src/solvers/refinement/string_refinement.cpp

Both of these appear to be unused.

Not sure, there clearly is a usage of optional in the file for example. Question is whether we should start removing headers if they were already included in parent file. Or make some sort of stdafx.h precompiled header file, which would include most commonly used headers (STL utilities, containers, strings, etc.)

I went to go look in CODING_STANDARD.md. It's not completely clear on this type of case, but it does say avoid unnecessary #includes, which they are in the literal sense.

jasigal · 2017-09-27T12:06:54Z

src/solvers/refinement/string_refinement.cpp

const & for both

jasigal · 2017-09-27T12:07:45Z

src/solvers/refinement/string_refinement.cpp

Can be deleted, other declaration below.

jasigal · 2017-09-27T12:08:12Z

src/solvers/refinement/string_refinement.cpp

Can delete these added args, they are unneeded in the function.

jasigal · 2017-09-27T12:08:37Z

src/solvers/refinement/string_refinement.cpp

Can delete first two args.

jasigal · 2017-09-27T12:30:57Z

src/solvers/refinement/string_refinement.cpp

Can be &.

jasigal · 2017-09-27T12:31:30Z

src/solvers/refinement/string_refinement.cpp

Loop could use expression iterator.

jasigal · 2017-09-27T12:32:02Z

src/solvers/refinement/string_refinement.cpp

~~Quite the opposite.~~

(It wasn't needed.)

jasigal · 2017-09-27T12:32:39Z

src/solvers/refinement/string_refinement.cpp

Update this by removing unused arguments and updating index_set (and removing current_index set).

jasigal · 2017-09-27T12:33:56Z

src/solvers/refinement/string_refinement.cpp

Should this be all arrays? It used to just be character arrays. For instance, the skolem functions in not contains constraints are arrays. This code seems to assume the arrays are strings.

jasigal · 2017-09-27T13:38:46Z

One thing I think we should address with such a big change to the string refinement process is stop the solver from treating skolem functions as strings. If I run the solver on cbmc/regression/strings-smoke-test/java_contains (so skolem functions from not contains axioms exist), it has its own index set. I have a comment above where any array seems to be treated as a string.

romainbrenguier · 2017-09-28T06:19:13Z

@smowton

or find a way to split the huge 3000-line commit in the middle of this into stages so each can be reviewed individually.

The problem is that it's very difficult to find any significant intermediary stage in this big commit that wouldn't break all the string tests.

jasigal · 2017-09-28T09:18:38Z

src/solvers/refinement/string_refinement.cpp

@romainbrenguier Changed the behavior of the solver here, probably not on purpose. In a later commit to revert to what was originally there for the most part, but not completely.

jasigal · 2017-09-28T11:25:30Z

src/solvers/refinement/string_refinement.cpp

I was debugging something with Justing, and this debug output and the one below make this impossible, get is called too often. Please delete.

Remove duplicate code for add_axioms_for_insert_float. Style: indentation in add_axioms_for_insert. Remove useless comment.

Remove unused function: associate_char_array_to_char_pointers. Rename solver in symbol_resolve. Rename function in generate_symbol_resolution_from_eq. Rename function get_char_array_and_concretize. Documentation update for generate_symbol_resolution, add_lemma, substitute_function_application, is_char_type. Some documentation and style fixes.

Debug information for arrays of pointers Debug information for check_axioms steps Refactoring: put debug information out of check_axioms Replace warning by invariant

This is necessary for the negation procedure to know the existential bounds and unfold the quantification as a conjunction.

This is in the case where super_get does not anything about the array we give it. This is necessary so that the string solver returns an array of the correct size, if the size is the only thing we know about the string. Add warning message in the case where the symbol is unknown to super_get

This is done by looking at which arrays were associted to pointers in the generator.

We use this in get to distinguish between strings and arrays of characters

This removes unused functions, declaration of unimplemented function, unused constants and unused fields.

In initialisation of string objects, this prevents the created objects from getting out of scope.

The function what was there before was not correct. It was calling cprover_string_copy which is deprecated.

The check for a specific object number was removed so this does not check what we want anyway. It is difficult to make it check the original intended behaviour using only regular expressions.

This more accurately describe what this object is.

romainbrenguier · 2017-10-29T21:02:29Z

@peterschrammel I squashed a lot of the correction commits with the corresponding original commit, I don't think there is much more to be done. For the cpp linter failure, this is due to a disagreement with what clang-format does for brackets in lamdbas.

romainbrenguier · 2017-10-30T10:30:24Z

@peterschrammel

How come? The function seems misplaced then.

Would java_utils.cpp be appropriate for this?

Add nolint marker on line with lambdas, which are formatted by clang in a way that is not compatible with cpp-lint.

romainbrenguier · 2017-10-31T10:12:26Z

This should be replaced by #1539

romainbrenguier force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch 2 times, most recently from 7148616 to 59fc1bd Compare September 25, 2017 08:02

romainbrenguier requested a review from jasigal September 25, 2017 08:02

romainbrenguier force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch 4 times, most recently from 6371f41 to aca00ce Compare September 25, 2017 10:29

romainbrenguier requested a review from smowton September 25, 2017 11:22

romainbrenguier force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch from 330d8da to 4e6fd78 Compare September 26, 2017 09:43

romainbrenguier changed the title ~~Complete rework of string solver to avoid using infinite arrays~~ TG-58 Complete rework of string solver to avoid using infinite arrays Sep 26, 2017

smowton reviewed Sep 26, 2017

View reviewed changes

romainbrenguier force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch 4 times, most recently from e63e2e9 to 2bf15cd Compare September 27, 2017 09:38

LAJW force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch 2 times, most recently from 1873cf3 to e34064f Compare September 27, 2017 12:21

jasigal suggested changes Sep 27, 2017

View reviewed changes

LAJW force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch 3 times, most recently from a7df645 to d8d91e9 Compare September 27, 2017 13:09

LAJW force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch 4 times, most recently from 01e6dd2 to dad57d7 Compare September 27, 2017 14:39

jasigal suggested changes Sep 28, 2017

View reviewed changes

jasigal reviewed Sep 28, 2017

View reviewed changes

romainbrenguier force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch from 2fa3500 to ef9aeaf Compare September 28, 2017 17:36

romainbrenguier added 21 commits October 28, 2017 18:43

Minor code improvements in generator_insert

3d5465e

Remove duplicate code for add_axioms_for_insert_float. Style: indentation in add_axioms_for_insert. Remove useless comment.

String refinement: Improve debug information

145364c

Debug information for arrays of pointers Debug information for check_axioms steps Refactoring: put debug information out of check_axioms Replace warning by invariant

Style fixes in string_constraint_generator.h

92897f7

Simplify not_contains constraints before negation

ca8213f

This is necessary for the negation procedure to know the existential bounds and unfold the quantification as a conjunction.

Distinguish strings and char arrays in get

26e895d

This is done by looking at which arrays were associted to pointers in the generator.

Fix set of created strings in generator and use it

2355e8e

We use this in get to distinguish between strings and arrays of characters

Cleanup unused fields of constraint generator

bb22700

This removes unused functions, declaration of unimplemented function, unused constants and unused fields.

Remove insert_long which duplicates insert_int

73d51fc

Allow index for argument of associate array to pointer

038b476

Remove redundant check in from_int_with_radix

e59349f

Style: rename i in chr_int to avoid clash

ad65847

Splitting is_string and init_string parts of init

daef30f

Use dynamic object instead of tmp_object in init

a2d7811

In initialisation of string objects, this prevents the created objects from getting out of scope.

Add code for String constructor from array

232617c

The function what was there before was not correct. It was calling cprover_string_copy which is deprecated.

Improve tests for StringBuilder.append([C)

90c8495

Remove regression test that is not checking anything

d03b8cc

The check for a specific object number was removed so this does not check what we want anyway. It is difficult to make it check the original intended behaviour using only regular expressions.

Rename first_index in array_expr

5a0d6b4

This more accurately describe what this object is.

Refactoring: simplify and remove unused expression

539ff9f

Refactor: remove m_ prefix from member fields

3ee3b25

romainbrenguier force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch from 27c1f83 to 3ee3b25 Compare October 28, 2017 17:44

romainbrenguier added 2 commits October 30, 2017 10:40

Move make_function_application to java_utils

21b2641

Style: add nolint marker on lines formated by clang

aa94fe8

Add nolint marker on line with lambdas, which are formatted by clang in a way that is not compatible with cpp-lint.

romainbrenguier force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch from dfc6942 to aa94fe8 Compare October 30, 2017 16:09

romainbrenguier mentioned this pull request Oct 31, 2017

TG-58 New PR for Complete rework of string solver to avoid using infinite arrays #1539

Merged

peterschrammel merged commit aa94fe8 into diffblue:develop Oct 31, 2017

TG-58 Complete rework of string solver to avoid using infinite arrays #1420

TG-58 Complete rework of string solver to avoid using infinite arrays #1420

Uh oh!

Conversation

romainbrenguier commented Sep 25, 2017

Uh oh!

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

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

LAJW Sep 27, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

jasigal commented Sep 27, 2017

Uh oh!

romainbrenguier commented Sep 28, 2017

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

romainbrenguier commented Oct 29, 2017

Uh oh!

romainbrenguier commented Oct 30, 2017

Uh oh!

romainbrenguier commented Oct 31, 2017

Uh oh!

Reviewers

Assignees

LAJW Sep 27, 2017 •

edited

Loading