Adding preprocessing for functions of the Java Character library by romainbrenguier · Pull Request #640 · diffblue/cbmc

romainbrenguier · 2017-03-15T15:33:49Z

This preprocessing is meant to replace simple methods of the Character
Java in goto-programs by expressions on characters.
About 60% of the library is supported, but for some of this
methods are limited to ASCII characters.
This is meant to be run in conjunction with the string refinement so
it is called if the string-refine option is activated.
Note that the string-refine option is added in PR #429, but this PR can be merged independently.

tautschnig · 2017-03-15T17:41:55Z

src/goto-programs/character_refine_preprocess.h

No single-character indent, please (just don't indent public/private).

tautschnig · 2017-03-15T17:42:10Z

src/goto-programs/character_refine_preprocess.h

No whitespace after &

tautschnig · 2017-03-15T17:43:44Z

src/goto-programs/character_refine_preprocess.h

Passing a list by value?

tautschnig · 2017-03-15T17:44:01Z

src/goto-programs/character_refine_preprocess.h

No blank line at end-of-file, please.

tautschnig · 2017-03-15T17:47:12Z

src/goto-programs/character_refine_preprocess.cpp

Some comments around those magic numbers would really be appreciated.

tautschnig · 2017-03-15T17:48:53Z

src/goto-programs/character_refine_preprocess.cpp

Rather random as it applies across this PR: use (const) references wherever possible, both in parameters and within the functions.

peterschrammel · 2017-03-17T19:05:13Z

src/goto-programs/Makefile

put each cpp file on a separate line to facilitate merging

peterschrammel · 2017-03-17T19:08:24Z

src/goto-programs/character_refine_preprocess.cpp

peterschrammel · 2017-03-17T19:08:40Z

src/goto-programs/character_refine_preprocess.cpp

Is there a reason why this has not been implemented yet?

peterschrammel · 2017-03-17T19:09:40Z

src/goto-programs/character_refine_preprocess.cpp

assignment (several occurrences)

peterschrammel · 2017-03-17T19:10:27Z

src/goto-programs/character_refine_preprocess.cpp

please comment on why this function is not implemented (several instances)

tautschnig

Mostly minor changes - many about the use of references.

tautschnig · 2017-03-20T13:09:24Z

src/cbmc/cbmc_parse_options.cpp

@kroening @peterschrammel @romainbrenguier I am wondering whether the invoked code should go in java_bytecode. (Yes, I have asked a similar question before.) If that folder isn't a good fit (for it introduces a dependency on goto-programs from java_bytecode), then maybe it's time for some folder like java_in-processing?

Yes, you're right it should probably go to java_bytecode, the dependencies in goto-programs are not strong here. I will investigate that.

I made some changes to the code which allows it to be called during java bytecode conversion.
So it can be moved there. See the commits 5801fbf , 848983b and 4c1986a

tautschnig · 2017-03-20T13:12:43Z

src/goto-programs/character_refine_preprocess.cpp

const typet &type=result.type(); If you delay the target->make_assignment() call until after code is constructed, you could even make all of the above const exprt &

tautschnig · 2017-03-20T13:13:15Z

src/goto-programs/character_refine_preprocess.cpp

Pass mp_integer by (const) reference

tautschnig · 2017-03-20T13:13:53Z

src/goto-programs/character_refine_preprocess.cpp

const auto &i : list

tautschnig · 2017-03-20T13:14:43Z

src/goto-programs/character_refine_preprocess.cpp

Use disjunction from util/std_expr.h to avoid a deeply nested expression.

tautschnig · 2017-03-20T13:26:24Z

src/goto-programs/character_refine_preprocess.cpp

Use references

tautschnig · 2017-03-20T13:26:36Z

src/goto-programs/character_refine_preprocess.cpp

Use references - see above

tautschnig · 2017-03-20T13:27:23Z

src/goto-programs/character_refine_preprocess.cpp

No need for this return; statement

tautschnig · 2017-03-20T13:30:24Z

src/goto-programs/character_refine_preprocess.cpp

Is there any way to catch or check additional function names (think about evolution of the Java SDK)? I'm thinking along the lines of "if the function call has prefix java::java.lang.Character." then it must be in the conversion_table or in some (to be created) conversion_not_supported table. Would that seem reasonable to do?

It would be nice to detect functions that we do not support, but I don't think it should stop CBMC if we encounter one, considering its result non-deterministic maybe enough for what we want to check. We could raise a warning in that case, but it's actually already done by CBMC: we get messages like **** WARNING: no body for function java::java.lang.Character.toUpperCase:(C)C for the functions we haven't translated.
The reasonable thing in my opinion would be to update the code with the new versions of the JDK. From what I have seen, there will not be much difference with the JDK9 (the only difference I see is a new codePointOf(String) function which is the inverse of getName).

tautschnig · 2017-03-20T13:31:46Z

src/goto-programs/character_refine_preprocess.h

There is some mixed indent of parameters - either seems ok, but consistency would be great.

tautschnig · 2017-03-21T12:53:14Z

With regard to the unsupported functions: won't the warning about missing function bodies continue to show up for all functions that are natively handled by the string solver?

romainbrenguier · 2017-03-21T15:19:51Z

@tautschnig the functions that we support are converted to some fake functions calls (which are understood by the solver), and these don't show up in the warnings.
So we only see the non-supported functions in the warnings.

tautschnig · 2017-03-21T20:05:30Z

src/java_bytecode/java_bytecode_convert_method_class.h

Just a note: with C++11 you don't need the space in > > anymore.

tautschnig

For all that I can tell from just reading code: this looks really good. Thanks a lot for all the changes and refactoring!

kroening · 2017-05-20T11:47:31Z

This needs a rebase!

This preprocessing is meant to replace simple methods of the Character Java library by expressions on characters during bytecode conversion. About 60% of the library is supported, but for some of this methods are limited to ASCII characters. This is meant to be run in conjunction with the string refinement so it is called if the string-refine option is activated.

romainbrenguier · 2017-05-21T10:27:19Z

@kroening this has been rebased.

tautschnig requested changes Mar 15, 2017

View reviewed changes

peterschrammel reviewed Mar 17, 2017

View reviewed changes

romainbrenguier force-pushed the java-character-library-support branch from e0cd4ee to b5cd96b Compare March 18, 2017 20:54

tautschnig requested changes Mar 20, 2017

View reviewed changes

tautschnig assigned romainbrenguier Mar 20, 2017

romainbrenguier force-pushed the java-character-library-support branch 2 times, most recently from 636c274 to 848983b Compare March 21, 2017 15:06

tautschnig reviewed Mar 21, 2017

View reviewed changes

tautschnig approved these changes Mar 21, 2017

View reviewed changes

tautschnig assigned kroening and unassigned romainbrenguier Mar 21, 2017

forejtv added the String solver label Mar 28, 2017

romainbrenguier added 2 commits May 21, 2017 10:25

Call to character preprocessing from java_bytecode

924e01b

romainbrenguier force-pushed the java-character-library-support branch from 848983b to 924e01b Compare May 21, 2017 09:31

kroening merged commit 9ec55a3 into diffblue:master May 21, 2017

Conversation

romainbrenguier commented Mar 15, 2017

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!

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

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Mar 21, 2017

Uh oh!

romainbrenguier commented Mar 21, 2017

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

kroening commented May 20, 2017

Uh oh!

romainbrenguier commented May 21, 2017

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants