[TG-9450] Allocate reference arrays with constant size in assignments from json #5112

romainbrenguier · 2019-09-17T13:30:39Z

This is to ensure static reference arrays retrieved from a json file are assigned with a constant size (when not marked as @nondetLength). This is so that array-cell-sensitivity can apply to such arrays.

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).
[na] My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
[na] White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov-io · 2019-09-20T10:01:44Z

Codecov Report

Merging #5112 into develop will increase coverage by <.01%.
The diff coverage is 94.28%.

@@             Coverage Diff             @@
##           develop    #5112      +/-   ##
===========================================
+ Coverage    66.95%   66.96%   +<.01%     
===========================================
  Files         1145     1146       +1     
  Lines        93653    93702      +49     
===========================================
+ Hits         62702    62743      +41     
- Misses       30951    30959       +8

Flag	Coverage Δ
#cproversmt2	`42.68% <ø> (ø)`	⬆️
#regression	`63.45% <82.85%> (ø)`	⬆️
#unit	`31.91% <74.28%> (+0.08%)`	⬆️

Impacted Files	Coverage Δ
jbmc/src/java_bytecode/java_bytecode_language.h	`76.92% <ø> (ø)`	⬆️
...bmc/src/java_bytecode/java_static_initializers.cpp	`99.11% <100%> (+0.02%)`	⬆️
jbmc/src/java_bytecode/code_with_references.h	`100% <100%> (ø)`
jbmc/src/java_bytecode/code_with_references.cpp	`80% <80%> (ø)`
jbmc/src/java_bytecode/assignments_from_json.cpp	`98% <96.96%> (-0.28%)`	⬇️
src/util/std_code.h	`91.95% <0%> (-0.49%)`	⬇️
...src/java_bytecode/java_bytecode_convert_method.cpp	`97.53% <0%> (ø)`	⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update f097054...69348e0. Read the comment docs.

allredj

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

smowton

I don't fully grasp why the references are necessary (perhaps add some high-level docs about what they're doing?), but I don't see anything troubling.

smowton · 2019-09-22T15:11:01Z

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -28,9 +28,6 @@ Author: Diffblue Ltd.
 /// ones that are not marked `const` may be mutated.
 struct object_creation_infot


Commit message: "We make is to make it so" -> "We make it so"

smowton · 2019-09-22T15:21:37Z

jbmc/src/java_bytecode/code_with_references.h

+public:
+  std::list<std::shared_ptr<code_with_referencest>> list;
+
+  void add(code_without_referencest code);


You seem to use add(code_without_referencest{...}) a lot, so perhaps just create an add(codet) overload?

smowton · 2019-09-22T15:23:03Z

jbmc/src/java_bytecode/assignments_from_json.cpp

-        *reference.array_length, ID_ge, from_integer(0, java_int_type())}}});
-      code.add(code_without_referencest{
-        allocate_array(reference.expr, *reference.array_length, info.loc)});
+      code.add(reference_allocationt{id, info.loc});


Commit "Add reference allocation code for references" doesn't seem to do what it says (it only deletes code from get_or_create_reference)

smowton · 2019-09-22T15:24:33Z

jbmc/src/java_bytecode/code_with_references.cpp

@@ -63,3 +63,9 @@ void code_with_references_listt::append(code_with_references_listt &&other)
 {
  list.splice(list.end(), other.list);
 }
+
+void code_with_references_listt::add_to_front(code_without_referencest code)


Commit message: typo "begginning"

romainbrenguier · 2019-09-23T07:09:31Z

@smowton

I don't fully grasp why the references are necessary (perhaps add some high-level docs about what they're doing?), but I don't see anything troubling.

This is already explained in the documentation of assign_from_json, we need them for objects that are reference-equal. For instance Object a = new Object(); Object b = new Object(); Object c = a;" We have c == abut notb == aand the way to distinguish the two cases in the json is to makeca reference toa`.

allredj

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

majakusber · 2019-09-23T10:49:16Z

jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc

+Not that the json file has been modified on purpose so that this checks
+that it is actually loaded and not retrieved by execution of the Util function.
+This test does not work with symex-driven-lazy-loading because this option is
+not compatible with --property.


⛏️ Missing new line

majakusber · 2019-09-23T10:53:33Z

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -902,11 +902,10 @@ code_with_references_listt assign_from_json_rec(
  return result;
 }

-void assign_from_json(
+code_with_references_listt assign_from_json(


⛏️ Typo in the commit message: the all the value pairs -> all the value pairs

This better reflects what this function does and make it easier to refactor.

This is in preparation for adding a new class in this file, we add there the function and class which will be needed by this class.

@ref

This will be use in assign_from_json for json files in which the "@ref" and "@id" entries are used, so that we can easily substitute code marked by "@ref" by the code corresponding to the object marked by "@id". This also move object_creation_referencet to the new header file since it will be used there, and the allocate_array is now declared in the new header and defined in the corresponding cpp file.

This should be an output of the functions rather than an "info". We make it so that assign_*_from_json functions have a return type which reflects what the function does. That way we separate the json to assignment conversion from the writting of code blocks, which will ultimately allow us to rewrite references in the assignments.

We know the number of elements of the reference array only when it is assigned so we replace the reference.array_length field at that point.

This will make it easier to add declarations at the begginning of a list of codet after the rest of the code has been generated.

This will allow references to be replaced after the all value pairs have been replaced. For instance in the regression test regression/jbmc/deterministic_assignments_json/test_char_array_pass.desc the reference 2 wouldn't have been assigned before the end of the assign_from_json call in which it is referenced for the first time so its allocation size would be non-deterministic but this is fixed by this commit.

This is a case for the json conversion which requires particular attention.

This checks that array cell sensitivity works fine for static arrays, whether we use the --static-values option or not.

allredj

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

romainbrenguier changed the title ~~Allocate reference arrays with constant size in assignments from json~~ [TG-9450] Allocate reference arrays with constant size in assignments from json Sep 17, 2019

romainbrenguier force-pushed the feature/assign-from-json-ref branch 7 times, most recently from 473a686 to d114b94 Compare September 20, 2019 09:13

romainbrenguier marked this pull request as ready for review September 20, 2019 09:33

romainbrenguier requested review from cesaro, cristina-david, NathanJPhillips, peterschrammel, pkesseli, smowton and thk123 as code owners September 20, 2019 09:33

allredj reviewed Sep 20, 2019

View reviewed changes

smowton approved these changes Sep 22, 2019

View reviewed changes

romainbrenguier force-pushed the feature/assign-from-json-ref branch from d114b94 to 69348e0 Compare September 23, 2019 07:09

allredj reviewed Sep 23, 2019

View reviewed changes

majakusber approved these changes Sep 23, 2019

View reviewed changes

romainbrenguier added 7 commits September 23, 2019 12:08

Make allocate_array take location and return code

85cf5a4

This better reflects what this function does and make it easier to refactor.

Move some code from assign_from_json to new file

4879a74

This is in preparation for adding a new class in this file, we add there the function and class which will be needed by this class.

Set the array length of reference when it is assigned

93aa152

We know the number of elements of the reference array only when it is assigned so we replace the reference.array_length field at that point.

add_to_front method for code_with_references_listt

5cd0c45

This will make it easier to add declarations at the begginning of a list of codet after the rest of the code has been generated.

romainbrenguier added 2 commits September 23, 2019 12:10

Add unit test for references to arrays

9d60ccf

This is a case for the json conversion which requires particular attention.

Add regression test for static array propagation

bc47e49

This checks that array cell sensitivity works fine for static arrays, whether we use the --static-values option or not.

romainbrenguier force-pushed the feature/assign-from-json-ref branch from 69348e0 to bc47e49 Compare September 23, 2019 11:10

allredj reviewed Sep 23, 2019

View reviewed changes

romainbrenguier merged commit bec782e into diffblue:develop Sep 23, 2019

romainbrenguier deleted the feature/assign-from-json-ref branch September 23, 2019 14:39

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[TG-9450] Allocate reference arrays with constant size in assignments from json #5112

[TG-9450] Allocate reference arrays with constant size in assignments from json #5112

Uh oh!

romainbrenguier commented Sep 17, 2019

Uh oh!

codecov-io commented Sep 20, 2019 •

edited

Loading

Uh oh!

allredj left a comment

Uh oh!

smowton left a comment

Uh oh!

smowton Sep 22, 2019

Uh oh!

smowton Sep 22, 2019

Uh oh!

smowton Sep 22, 2019

Uh oh!

smowton Sep 22, 2019

Uh oh!

romainbrenguier commented Sep 23, 2019

Uh oh!

allredj left a comment

Uh oh!

majakusber Sep 23, 2019

Uh oh!

majakusber Sep 23, 2019

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

		@@ -28,9 +28,6 @@ Author: Diffblue Ltd.
		/// ones that are not marked `const` may be mutated.
		struct object_creation_infot

[TG-9450] Allocate reference arrays with constant size in assignments from json #5112

[TG-9450] Allocate reference arrays with constant size in assignments from json #5112

Uh oh!

Conversation

romainbrenguier commented Sep 17, 2019

Uh oh!

codecov-io commented Sep 20, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

smowton Sep 22, 2019

Choose a reason for hiding this comment

Uh oh!

smowton Sep 22, 2019

Choose a reason for hiding this comment

Uh oh!

smowton Sep 22, 2019

Choose a reason for hiding this comment

Uh oh!

smowton Sep 22, 2019

Choose a reason for hiding this comment

Uh oh!

romainbrenguier commented Sep 23, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

majakusber Sep 23, 2019

Choose a reason for hiding this comment

Uh oh!

majakusber Sep 23, 2019

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov-io commented Sep 20, 2019 •

edited

Loading