Loop-less initialization of primitive arrays #3649

allredj · 2018-12-31T11:02:19Z

Nondeterministic primitive arrays are now initialized using a single NONDET instruction, instead of being initialized element-wise in a loop over the length of the array.

This removes the coupling between the length of nondeterministic primitive arrays and the maximum unwind value.

Advantages when dealing with arrays of primitive type:

--max-nondet-array-length can now be set to a value larger than --unwind
jbmc can now deal with large primitive arrays while keeping --unwind low

For multi-dimensional arrays, only the innermost dimension benefits from loop-less initialization. Higher dimensions are still initialized via a loop, and so are bound by --unwind.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

Will also be used in java_object_factory

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 997d692).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95984671

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 65af890).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95985244

peterschrammel · 2018-12-31T13:16:50Z

jbmc/src/java_bytecode/java_object_factory.cpp

+/// loop.
+/// The code produced is of the form (supposing an array of type OBJ):
+/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+///        struct java.lang.Integer **array_data_init;


peterschrammel · 2018-12-31T13:20:19Z

jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.java

@@ -0,0 +1,16 @@
+class NondetArrayPrimitive
+{
+  void intArray(int[] array)


Is there a test for non-primitive arrays too?

And byte, char, short, long, double...

Added tests for all primitive types.
Not for non-primitive types as this PR doesn't change behaviour for those.

this PR doesn't change behaviour for those.

Is there a test that checks that?

peterschrammel · 2018-12-31T13:22:09Z

jbmc/src/java_bytecode/java_object_factory.cpp

+/// Create code to nondeterministically initialize arrays of primitive type.
+/// The code produced is of the form:
+/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+///     int (*array_data_init)[max_length_expr];


Why int? Shouldn't it be the primitive type? Or otherwise say 'example'.

peterschrammel · 2018-12-31T13:24:46Z

jbmc/src/java_bytecode/java_object_factory.cpp

+{
+  array_typet array_type(element_type, max_length_expr);
+
+  // int (*array_data_init)[max_length_expr];


Why int? What about byte, long, ...?

Makes gen_nondet_array_init smaller and clarifies process.

Get rid of the initilization loop for nondet arrays, so the size of nondeterministic arrays of primitive types no longer depend on the max unwind value.

Array variable name is now of type "dynamic_object" for primitive arrays. "dynamic_N_array" is a name generated by symex_cpp_new when loop-initializing arrays (in remove_java_newt::lower_java_new_array). We no longer loop-initialize primitive arrays.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 2d24bbd).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95995687

allredj self-assigned this Dec 31, 2018

allredj requested review from cesaro, cristina-david, NathanJPhillips, peterschrammel, pkesseli, smowton and thk123 as code owners December 31, 2018 11:02

allredj changed the title ~~Loop-less primitive array initialization~~ Loop-less initialization of primitive arrays Dec 31, 2018

Move make_allocate_code to java_object_factory

b497e38

Will also be used in java_object_factory

allredj force-pushed the loop-less-array-init branch from e30da83 to 997d692 Compare December 31, 2018 11:39

allredj commented Dec 31, 2018

View reviewed changes

peterschrammel reviewed Dec 31, 2018

View reviewed changes

Joel Allred added 4 commits December 31, 2018 15:44

Factor loop init out of gen_nondet_array_init

0fce0ba

Makes gen_nondet_array_init smaller and clarifies process.

Initialize nondet arrays with a single NONDET

6f851a9

Get rid of the initilization loop for nondet arrays, so the size of nondeterministic arrays of primitive types no longer depend on the max unwind value.

Tests for loop-less array init

9041b6e

Update trace test

2d24bbd

Array variable name is now of type "dynamic_object" for primitive arrays. "dynamic_N_array" is a name generated by symex_cpp_new when loop-initializing arrays (in remove_java_newt::lower_java_new_array). We no longer loop-initialize primitive arrays.

allredj force-pushed the loop-less-array-init branch from 65af890 to 2d24bbd Compare December 31, 2018 16:04

allredj commented Dec 31, 2018

View reviewed changes

kroening approved these changes Jan 2, 2019

View reviewed changes

peterschrammel approved these changes Jan 2, 2019

View reviewed changes

kroening merged commit 8e145fa into diffblue:develop Jan 2, 2019

allredj deleted the loop-less-array-init branch January 2, 2019 18:45

allredj mentioned this pull request Jan 17, 2019

Disable loop-less init of primitive arrays #3825

Closed

7 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Loop-less initialization of primitive arrays #3649

Loop-less initialization of primitive arrays #3649

Uh oh!

allredj commented Dec 31, 2018 •

edited

Loading

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

peterschrammel Dec 31, 2018

Uh oh!

allredj Dec 31, 2018

Uh oh!

peterschrammel Dec 31, 2018

Uh oh!

peterschrammel Dec 31, 2018

Uh oh!

allredj Dec 31, 2018

Uh oh!

peterschrammel Jan 2, 2019 •

edited

Loading

Uh oh!

peterschrammel Dec 31, 2018

Uh oh!

allredj Dec 31, 2018 •

edited

Loading

Uh oh!

peterschrammel Dec 31, 2018

Uh oh!

allredj Dec 31, 2018

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

Loop-less initialization of primitive arrays #3649

Loop-less initialization of primitive arrays #3649

Uh oh!

Conversation

allredj commented Dec 31, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

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

peterschrammel Jan 2, 2019 • 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!

allredj Dec 31, 2018 • 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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

allredj commented Dec 31, 2018 •

edited

Loading

peterschrammel Jan 2, 2019 •

edited

Loading

allredj Dec 31, 2018 •

edited

Loading