De-duplicate "generate a nondet int in a given range" logic #4416

antlechner · 2019-03-21T17:52:53Z

This PR addresses code duplication between nondet.cpp and java_object_factory.cpp. The latter had a utility function gen_nondet_int_init which can be replaced with generate_nondet_int from nondet.h after a few small changes.
No functional change is made in this PR, only refactoring.

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.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
n/a 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).
n/a My commit message includes data points confirming performance improvements (if claimed).
n/a My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 1433c1c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105338866
Status will be re-evaluated on next push.
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).
the compatibility was already broken by an earlier merge.

romainbrenguier

Looks great

romainbrenguier · 2019-03-22T07:41:13Z

src/util/nondet.cpp

@@ -93,15 +82,16 @@ code_blockt generate_nondet_switch(

  code_blockt result_block;

+  allocate_objectst allocate_objects(
+    mode, source_location, name_prefix, symbol_table);


⛏️ prefer braces

Done. I keep forgetting about this new convention...

It's not really new, just that it wasn't really applied, then someone pointed out this guideline to me on one of my PR, so I have been annoying everyone with this since then. 😈

romainbrenguier · 2019-03-22T07:49:29Z

jbmc/src/java_bytecode/java_object_factory.cpp

    from_integer(0, java_int_type()),
    max_length_expr,
-    location);
+    "nondet_array_length",
+    loc,


❓ why is location replaced with loc?

Didn't even notice that as CLion suggested loc here. loc is a field of the object factory and location is the parameter to the function. From what I can see these two values are always the same so one of them is unnecessary. For now I changed it back to location, and I'll tidy up the loc/location duplication in a follow-up PR. 🍊

tautschnig · 2019-03-22T07:42:41Z

src/util/nondet.h

@@ -13,6 +13,25 @@ Author: Diffblue Ltd.
 #include <util/std_expr.h>
 #include <util/symbol_table.h>

+/// Same as \ref generate_nondet_int(
+///   const mp_integer &min_value,


Does this multi-line \ref actually render correctly in Doxygen?

I tried it locally and it links to the right function, though only the generate_nondet_init part turns into a link. Some of the parameter types (like source_locationt) also appear as links to the Doxygen for those types.
If there is a better / more standard way of linking between overloaded functions, please let me know.

tautschnig · 2019-03-22T07:45:40Z

src/util/nondet.cpp

@@ -7,6 +7,7 @@ Author: Diffblue Ltd.
 \*******************************************************************/

 #include "nondet.h"
+#include "allocate_objects.h"


Nit pick:

#include "nondet.h" #include "allocate_objects.h" #include "arith_tools.h" #include "c_types.h" #include "fresh_symbol.h" #include "symbol.h"

Fixed the linebreaks in the same commit and removed the "util" parts in a new commit (same as the one for the forward declarations below).

tautschnig · 2019-03-22T07:50:01Z

src/util/nondet.h

@@ -9,6 +9,7 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_JAVA_BYTECODE_NONDET_H
 #define CPROVER_JAVA_BYTECODE_NONDET_H

+#include <util/allocate_objects.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>


I guess it's the first time I'm properly looking at this: the only includes we really need here are #include "std_code.h" and #include "std_expr.h". Everything else can (and IMHO: should be) done via forward declarations.

Done in a new commit.

tautschnig · 2019-03-22T07:51:38Z

jbmc/src/java_bytecode/java_object_factory.cpp

    from_integer(0, java_int_type()),
    minus_exprt(length_expr, from_integer(1, java_int_type())),
-    location);
+    "enum_index_init",
+    loc,


Just like @romainbrenguier I'm surprised this even compiles? As it does, is the location parameter for this method unnecessary?

See my comment marked 🍊 above.
The way the object factory passes variables around is currently quite messy in general, it uses a mix of

class fields (even though there isn't a publicly visible class here; from what I can see the class is only used to store fields)

many parameters to most functions

a poorly named java_object_factory_parameterst which groups further arguments into a struct.

The three common ways of moving lots of variables around are all combined in one place here... I would like to generally tidy this up a bit, probably moving away from lots of function parameters and fields to bundling more things in (a) struct(s). Let me know what you think.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: fcb2ec6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105427335
Status will be re-evaluated on next push.
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).
the compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: f2c6f83).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105427499
Status will be re-evaluated on next push.
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).
the compatibility was already broken by an earlier merge.

kroening · 2019-03-22T12:32:29Z

src/util/nondet.cpp

+  allocate_objectst &allocate_objects,
+  code_blockt &instructions)
+{
+  PRECONDITION(min_value < max_value);


<= is fine

Done (in a new commit, as the previous version used < too).

Following the new coding standard

We will be able to use the exprt version in other parts of the code.

There is no reason why this function shouldn't work to "choose" between just one value.

This will make the functions more re-usable in parts of the code that use different prefixes.

This simplifies the code in generate_nondet_init and reduces code duplication.

Specifying "util" is not necessary as nondet.cpp is itself in the util folder. Forward declarations can be used in nondet.h.

Calls to java_object_factoryt::gen_nondet_int_init can be replaced with equivalent calls to generate_nondet_int from nondet.h.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 63d9f50).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105439082
Status will be re-evaluated on next push.
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).
the compatibility was already broken by an earlier merge.

antlechner requested review from romainbrenguier and majakusber March 21, 2019 17:52

antlechner requested review from cesaro, cristina-david, kroening, NathanJPhillips, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners March 21, 2019 17:52

allredj reviewed Mar 21, 2019

View reviewed changes

owen-mc-diffblue approved these changes Mar 22, 2019

View reviewed changes

romainbrenguier approved these changes Mar 22, 2019

View reviewed changes

tautschnig approved these changes Mar 22, 2019

View reviewed changes

tautschnig assigned smowton, thk123, peterschrammel and antlechner Mar 22, 2019

antlechner force-pushed the antonia/nondet-int-refactor branch 2 times, most recently from fcb2ec6 to f2c6f83 Compare March 22, 2019 11:03

allredj reviewed Mar 22, 2019

View reviewed changes

kroening reviewed Mar 22, 2019

View reviewed changes

smowton approved these changes Mar 22, 2019

View reviewed changes

antlechner added 5 commits March 22, 2019 12:37

Move nondet documentation to header file

0d32a43

Following the new coding standard

Split generate_nondet_int into two functions

6278e42

We will be able to use the exprt version in other parts of the code.

Make precondition on min/max values less strict

cbd00e6

There is no reason why this function shouldn't work to "choose" between just one value.

Parameterize basename_prefix

9e243c9

This will make the functions more re-usable in parts of the code that use different prefixes.

Use allocate_objects to manage new symbol creation

f6e6ad6

This simplifies the code in generate_nondet_init and reduces code duplication.

antlechner added 2 commits March 22, 2019 12:37

Tidy up includes

eeb9f22

Specifying "util" is not necessary as nondet.cpp is itself in the util folder. Forward declarations can be used in nondet.h.

Remove duplicate helper function in object factory

63d9f50

Calls to java_object_factoryt::gen_nondet_int_init can be replaced with equivalent calls to generate_nondet_int from nondet.h.

antlechner force-pushed the antonia/nondet-int-refactor branch from f2c6f83 to 63d9f50 Compare March 22, 2019 12:37

allredj reviewed Mar 22, 2019

View reviewed changes

antlechner merged commit 45e1186 into diffblue:develop Mar 22, 2019

antlechner deleted the antonia/nondet-int-refactor branch March 22, 2019 17:40

antlechner mentioned this pull request Mar 25, 2019

Remove two unnecessary fields from the Java object factory #4432

Merged

1 task

De-duplicate "generate a nondet int in a given range" logic #4416

De-duplicate "generate a nondet int in a given range" logic #4416

Uh oh!

Conversation

antlechner commented Mar 21, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

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

antlechner Mar 22, 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!

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

antlechner Mar 22, 2019 •

edited

Loading