Adding preprocessing for functions of the Java Character library #640

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

+
+class character_refine_preprocesst:public messaget
+{
+ public:


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

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

src/goto-programs/character_refine_preprocess.h

+
+ private:
+  namespacet ns;
+  goto_functionst & goto_functions;


No whitespace after &

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

src/goto-programs/character_refine_preprocess.h

+      exprt (*expr_function)(exprt, typet), conversion_input &target);
+  static exprt in_interval_expr(
+    exprt arg, mp_integer lower_bound, mp_integer upper_bound);
+  static exprt in_list_expr(exprt chr, std::list<mp_integer> list);


Passing a list by value?

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

src/goto-programs/character_refine_preprocess.h

+};
+
+#endif // CPROVER_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

+  typet type=result.type();
+  exprt u010000=from_integer(0x010000, type);
+  exprt u0800=from_integer(0x0800, type);
+  exprt u0400=from_integer(0x0400, type);


Some comments around those magic numbers would really be appreciated.

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

src/goto-programs/character_refine_preprocess.cpp

+\*******************************************************************/
+
+exprt character_refine_preprocesst::expr_of_is_whitespace(
+  exprt expr, typet type)


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

@@ -20,7 +20,9 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \
      slice_global_inits.cpp goto_inline_class.cpp class_identifier.cpp \
      show_goto_functions_json.cpp \
      show_goto_functions_xml.cpp \
-      remove_static_init_loops.cpp remove_instanceof.cpp
+      remove_static_init_loops.cpp remove_instanceof.cpp \


put each cpp file on a separate line to facilitate merging

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

src/goto-programs/character_refine_preprocess.cpp

+  Inputs:
+    target - a position in a goto program
+
+ Purpose: Converts function call to an assignement of an expression


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

src/goto-programs/character_refine_preprocess.cpp

+void character_refine_preprocesst::convert_is_valid_code_point(
+    conversion_input &target)
+{
+  // TODO


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

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

src/goto-programs/character_refine_preprocess.cpp

+  Inputs:
+    target - a position in a goto program
+
+ Purpose: Converts function call to an assignement of an expression


assignment (several occurrences)

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

src/goto-programs/character_refine_preprocess.cpp

+void character_refine_preprocesst::convert_get_directionality_char(
+  conversion_input &target)
+{
+  // TODO


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

@@ -904,6 +905,13 @@ bool cbmc_parse_optionst::process_goto_program(
    status() << "Partial Inlining" << eom;
    goto_partial_inline(goto_functions, ns, ui_message_handler);

+    if(cmdline.isset("string-refine"))
+    {
+      status() << "Preprocessing for java Character library" << eom;


@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

+  exprt arg=function_call.arguments()[0];
+  exprt result=function_call.lhs();
+  target->make_assignment();
+  typet type=result.type();


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

+\*******************************************************************/
+
+exprt character_refine_preprocesst::in_interval_expr(
+  const exprt &chr, mp_integer lower_bound, mp_integer upper_bound)


Pass mp_integer by (const) reference

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

src/goto-programs/character_refine_preprocess.cpp

+  const exprt &chr, const std::list<mp_integer> &list)
+{
+  exprt res=false_exprt();
+  for(auto i : list)


const auto &i : list

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

src/goto-programs/character_refine_preprocess.cpp

+{
+  exprt res=false_exprt();
+  for(auto i : list)
+    res=or_exprt(res, equal_exprt(chr, from_integer(i, chr.type())));


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

+    expr - An expression of type character
+    type - A type for the output
+
+ Outputs: A character expression of the 


Use references

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

src/goto-programs/character_refine_preprocess.cpp

+    expr - An expression of type character
+    type - A type for the output
+
+ Outputs: A character expression of the 


Use references - see above

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

src/goto-programs/character_refine_preprocess.cpp

+    expr - An expression of type character
+    type - A type for the output
+
+ Outputs: A character expression of the 


No need for this return; statement

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

src/goto-programs/character_refine_preprocess.cpp

+    expr - An expression of type character
+    type - A type for the output
+
+ Outputs: A character expression of the 


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

+      exprt (*expr_function)(const exprt &chr, const typet &type),
+      conversion_input &target);
+  static exprt in_interval_expr(
+    const exprt &chr, mp_integer lower_bound, mp_integer upper_bound);


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

@@ -33,13 +33,15 @@ class java_bytecode_convert_methodt:public messaget
    bool _disable_runtime_checks,
    size_t _max_array_length,
    safe_pointer<std::vector<irep_idt> > _needed_methods,
-    safe_pointer<std::set<irep_idt> > _needed_classes):
+    safe_pointer<std::set<irep_idt> > _needed_classes,


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

		};

		#endif // CPROVER_GOTO_PROGRAMS_CHARACTER_REFINE_PREPROCESS_H

Adding preprocessing for functions of the Java Character library #640

Adding preprocessing for functions of the Java Character library #640

Uh oh!

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!

Uh oh!