[TG-3581] Better Support for Enums in JBMC #2569

mgudemann · 2018-07-10T04:45:56Z

Introduce secific unwind bounds for copy loops in array clone for enumerations.

allredj

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

allredj

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

allredj

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

peterschrammel · 2018-07-10T15:14:19Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2197,7 +2212,7 @@ void java_bytecode_convert_methodt::convert_invoke(
  //   generate code that may wrongly assume that such a method is
  //   accessible if we assume that its access attribute is "more
  //   accessible" than it actually is.
-  irep_idt id = arg0.get(ID_identifier);
+  const irep_idt id = arg0.get(ID_identifier);


it's not clear for me what arg0 represents, if you have an intuition about that can you rename the parameter?

peterschrammel · 2018-07-10T15:15:56Z

jbmc/src/java_bytecode/java_utils.cpp

+  // Also provide a clone method:
+  // ----------------------------
+
+  const irep_idt clone_name = identifier + +".clone:()Ljava/lang/Object;";


peterschrammel · 2018-07-10T15:18:26Z

jbmc/src/java_bytecode/java_utils.cpp

@@ -5,7 +5,6 @@
 Author: Daniel Kroening, [email protected]

 \*******************************************************************/
-


spurious change?

peterschrammel · 2018-07-10T15:19:04Z

jbmc/src/java_bytecode/java_utils.cpp

@@ -446,184 +445,222 @@ const std::unordered_set<std::string> cprover_methods_to_ignore
  "getCurrentThreadID"
 };

+/// Register in the \p symbol_table a new symbol type
+/// java::array[X] where X is byte, float, int, char...
+void add_array_type(


maybe add doxygen for parameters

peterschrammel · 2018-07-10T15:20:09Z

jbmc/src/java_bytecode/java_utils.cpp

+{
+  symbol_typet symbol_type = to_symbol_type(java_array_type(l).subtype());
+
+  const std::string identifier = enum_name


you could assign that directly to an irep_idt

romainbrenguier · 2018-07-11T08:02:40Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2197,7 +2212,7 @@ void java_bytecode_convert_methodt::convert_invoke(
  //   generate code that may wrongly assume that such a method is
  //   accessible if we assume that its access attribute is "more
  //   accessible" than it actually is.
-  irep_idt id = arg0.get(ID_identifier);
+  const irep_idt id = arg0.get(ID_identifier);


it's not clear for me what arg0 represents, if you have an intuition about that can you rename the parameter?

romainbrenguier · 2018-07-11T08:03:20Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+  const bool is_enum_values_clone_call =
+    enum_clone_symbol.type.get_bool(ID_enumeration) &&
+    (full_method_name ==
+     (calling_class_name + ".values:()[L" + class_type_name + ";"));


define is_enum_values_clone_call closer to where it is used

romainbrenguier · 2018-07-11T08:07:05Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+  if(is_enum_values_clone_call)
+  {
+    const std::string clone_name =
+      "java::array[" + calling_class_name + "].clone:()Ljava/lang/Object;";


I don't think you can add to a string literal. You should use std::string("java::array[") + ... instead

romainbrenguier · 2018-07-11T08:10:55Z

jbmc/src/java_bytecode/java_utils.cpp

+  code_blockt clone_body;
+
+  code_declt declare_cloned(local_symexpr);
+  clone_body.move_to_operands(declare_cloned);


code_blockt has a move method

will change, but this is old code that just moved

romainbrenguier · 2018-07-11T08:12:37Z

jbmc/src/java_bytecode/java_utils.cpp

+
+  member_exprt new_base_class(
+    new_array, base_class_component.get_name(), base_class_component.type());
+  address_of_exprt retval(new_base_class);


romainbrenguier · 2018-07-11T08:15:17Z

jbmc/src/java_bytecode/java_utils.cpp

+    plus_exprt(old_data, index_symexpr), old_data.type().subtype());
+  dereference_exprt new_cell(
+    plus_exprt(new_data, index_symexpr), new_data.type().subtype());
+  code_assignt copy_cell(new_cell, old_cell);


romainbrenguier · 2018-07-11T08:15:47Z

jbmc/src/java_bytecode/java_utils.cpp

+}
+
+/// Register in the \p symbol_table a new symbol for an enum type
+/// \param enum_type_name: Name of the enum type.


say that it contains the "java::" prefix?

romainbrenguier · 2018-07-11T08:18:14Z

jbmc/src/java_bytecode/java_enum_array_clone_unwind_handler.cpp

+
+#include <java_bytecode/java_utils.h>
+
+/// Unwind handler that special-cases the clone functions of arrays of


specializes?

romainbrenguier · 2018-07-11T08:20:38Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+  if(is_enum_values_clone_call)
+  {
+    const std::string clone_name =
+      "java::array[" + class_type_name + "].clone:()Ljava/lang/Object;";


I don't think you can add to a string literal

I am not sure I understand what you mean, it seems to work without a problem.

smowton

It strikes me this can be done more simply if we can expose a bit of symex's state to the loop unwind handlers (called here https://github.com/diffblue/cbmc/blob/develop/src/cbmc/symex_bmc.cpp#L119, and implemented here https://github.com/diffblue/cbmc/blob/develop/jbmc/src/jbmc/jbmc_parse_options.cpp#L508)

Basically we want to inspect a little bit of the calling context, to check whether we're in clone(), and if so whether this->length (the length of the array being cloned) is a constant.

Possible approaches:

Give the unwind handler the ability to call symext::clean_expr (which among other things performs constant propagation), so it can directly ask symex for this->length and find out whether we know a bound
Annotate the loop! When generating .clone() we know the actual loop length is bounded and that bound is this->length. Then symex can evaluate the given bound and give it to the unwind handler.

I think either of these would be much simpler and cleaner than method cloning just so we have a unique function ID key to associate with the decision to unwind.

mgudemann · 2018-07-13T11:39:32Z

@smowton We decided to go with this solution, look at the outcome and look at the alternative in a new issue.

allredj

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

tautschnig

I acknowledge that this is work-in-progress, but just to jot down my expectations anyway: 1) there need to be tests added; 2) a change to the interpreter has been added, but it's not clear to me how that relates to the PR subject.

romainbrenguier · 2018-07-13T13:45:28Z

jbmc/src/java_bytecode/java_utils.cpp

+  const auto &index_symexpr = index_symbol.symbol_expr();
+
+  code_declt declare_index(index_symexpr);
+  clone_body.move_to_operands(declare_index);


clone_body.add(code_declt(...

romainbrenguier · 2018-07-13T13:46:42Z

jbmc/src/java_bytecode/java_utils.cpp

+
+  dereference_exprt old_cell(
+    plus_exprt(old_data, index_symexpr), old_data.type().subtype());
+  dereference_exprt new_cell(


done

please note that this code was just moved, not written by me

done, please note that I mainly moved the code and didn't write it

mgudemann · 2018-07-17T10:47:54Z

@tautschnig please find some regression tests in the latest commit (these were just in TG before)
The interpreter change is to prevent a warning / error message that occurred

tautschnig · 2018-07-17T11:20:38Z

The interpreter change is to prevent a warning / error message that occurred

Would it somehow be possible to explain what this is? The change seems entirely sensible to me, but I still don't really get why it would fit this PR.

mgudemann · 2018-07-19T12:44:37Z

@tautschnig this fixes the interpreter when it got a member-of-constant-struct like
void*[{.length = 6, .data = &dynamic_7_array}.length]

mgudemann · 2018-07-19T12:45:22Z

these occurred with my PR, but I am not sure whether it was the cause or I just paid more attention to the output here

For Enum classes this replaces calls to clone via a specialized clone method call that allows for explicit unwind bounds depending on the number of enum elements.

Change argument names to more meaningful identifiers, lint code

This handler unwinds loops in specialized `.clone` functions for `Enum` arrays.

Before we considered the `code_switch_caset` to belong to the target instruction which lead to uncoverable goals of the form: IF condition 1 then GOTO 1 ... 1: GOTO 2 ASSERT false // uncoverable block ... 2:

It could already do index-of-constant-array -- by replacing its custom code with simplify_expr we can expand that to also support member-of-constant-struct, as occurs when symex's deref'ing and then the interpreter's environment translate a variable-length array type like int[obj->length] into int[particular_object.length] and then int[{.length = 1, .data = &xyz}.length].

Update regression tests

Currently the regression tests fail with symex driven lazy loading due to a difference in generated properties.

allredj

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

smowton · 2018-08-01T11:38:39Z

Proposed alternative implementation here: #2651

mgudemann · 2018-08-03T11:06:12Z

superseded by #2651

mgudemann requested review from cesaro, cristina-david, NathanJPhillips, peterschrammel, pkesseli, smowton and thk123 as code owners July 10, 2018 04:45

mgudemann self-assigned this Jul 10, 2018

mgudemann added the work in progress label Jul 10, 2018

mgudemann force-pushed the feature/java/enum_support branch from c5690b2 to 8ca5290 Compare July 10, 2018 04:49

allredj reviewed Jul 10, 2018

View reviewed changes

mgudemann force-pushed the feature/java/enum_support branch from 8ca5290 to 1fe1e37 Compare July 10, 2018 14:29

mgudemann removed the work in progress label Jul 10, 2018

allredj reviewed Jul 10, 2018

View reviewed changes

peterschrammel reviewed Jul 10, 2018

View reviewed changes

romainbrenguier reviewed Jul 11, 2018

View reviewed changes

smowton suggested changes Jul 11, 2018

View reviewed changes

mgudemann force-pushed the feature/java/enum_support branch from 1fe1e37 to d449275 Compare July 13, 2018 11:36

mgudemann requested review from kroening and tautschnig as code owners July 13, 2018 11:36

allredj reviewed Jul 13, 2018

View reviewed changes

tautschnig reviewed Jul 13, 2018

View reviewed changes

romainbrenguier reviewed Jul 13, 2018

View reviewed changes

mgudemann force-pushed the feature/java/enum_support branch from d449275 to 2a2cef5 Compare July 17, 2018 10:33

mgudemann force-pushed the feature/java/enum_support branch from 2a2cef5 to b288c80 Compare July 17, 2018 11:18

mgudemann force-pushed the feature/java/enum_support branch 5 times, most recently from 6163718 to 17d982d Compare July 18, 2018 11:22

Matthias Güdemann and others added 8 commits July 31, 2018 11:44

Move add_array_types to java_utils

b7c741c

Replace calls to array.clone in values for Enum

b741f33

For Enum classes this replaces calls to clone via a specialized clone method call that allows for explicit unwind bounds depending on the number of enum elements.

Clarify in convert methods

d78d984

Change argument names to more meaningful identifiers, lint code

Split add_array_type, specialize for enums

4b3e725

Add java_enum_array_clone_unwind_handler

a3f20f2

This handler unwinds loops in specialized `.clone` functions for `Enum` arrays.

Change source location of jump target in {table|lookup}switch

5e2dd60

Before we considered the `code_switch_caset` to belong to the target instruction which lead to uncoverable goals of the form: IF condition 1 then GOTO 1 ... 1: GOTO 2 ASSERT false // uncoverable block ... 2:

Add regression tests for changes to JBMC enumeration support

8c77ad7

Update regression tests

mgudemann force-pushed the feature/java/enum_support branch from 17d982d to 1e01432 Compare July 31, 2018 12:30

Matthias Güdemann added 2 commits July 31, 2018 16:00

Evaluate array index before simplify

ce641c4

Mark regression tests as expecting failure for symex driven loading

9b82377

Currently the regression tests fail with symex driven lazy loading due to a difference in generated properties.

mgudemann force-pushed the feature/java/enum_support branch from 1e01432 to 9b82377 Compare July 31, 2018 15:29

allredj reviewed Jul 31, 2018

View reviewed changes

smowton mentioned this pull request Aug 1, 2018

Unroll enumeration values() loops #2651

Merged

mgudemann closed this Aug 3, 2018

		@@ -5,7 +5,6 @@
		Author: Daniel Kroening, [email protected]

		\*******************************************************************/


		#include <java_bytecode/java_utils.h>

		/// Unwind handler that special-cases the clone functions of arrays of

[TG-3581] Better Support for Enums in JBMC #2569

[TG-3581] Better Support for Enums in JBMC #2569

Conversation

mgudemann commented Jul 10, 2018

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton left a comment

Choose a reason for hiding this comment

mgudemann commented Jul 13, 2018

allredj left a comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mgudemann commented Jul 17, 2018

tautschnig commented Jul 17, 2018

mgudemann commented Jul 19, 2018

mgudemann commented Jul 19, 2018

allredj left a comment

Choose a reason for hiding this comment

smowton commented Aug 1, 2018

mgudemann commented Aug 3, 2018