Factor out object allocation from object factories [blocks: #3455] #3443

danpoe · 2018-11-19T15:54:35Z

The PR factors out the object allocation code from the Java object factory into a separate class allocate_objectst that can be used by both the C and Java object factories.

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/
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.

xbauch · 2018-11-19T16:12:24Z

src/util/allocate_objects.cpp

+/// \param allocate_type: Type of the object allocated
+/// \param alloc_type: Allocation type (global, local or dynamic)
+/// \return An expression denoting the address of the newly allocated object.
+exprt allocate_objectst::allocate_object(


I would expect doxygen to complain about not describing the symbols_created.

thk123

This should probably have a full TG bump before merging (I will make after the preceding PR is merged) - also does this mean that the cprover start for C programs will do non-det init of structs like how they are handled in Java? Or have I got the wrong end of the stick? If so - very exciting!

hannes-steffenhagen-diffblue · 2018-11-20T14:05:35Z

@thk123 Getting something like that to work for structs and arrays is indeed the intention here

hannes-steffenhagen-diffblue

LGTM, I think the allocate commits should be squashed though, they don't make much sense in isolatin.

jbmc/src/java_bytecode/java_object_factory.cpp

allredj

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

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

Recursive nondet init of pointers to structs [blocks: #3443]

allredj

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

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

chrisr-diffblue

LGTM

tautschnig

Overall ok, I'm just concerned about terminology.

tautschnig · 2018-12-01T18:51:31Z

src/util/allocate_objects.cpp

+
+#include <util/c_types.h>
+#include <util/fresh_symbol.h>
+#include <util/pointer_offset_size.h>


Nit pick: within the folder we generally seem to use "..." instead of <...>

tautschnig · 2018-12-01T18:52:28Z

src/util/allocate_objects.cpp

+#include <util/fresh_symbol.h>
+#include <util/pointer_offset_size.h>
+
+/// Installs a new symbol in the symbol table, pushing the corresponding


What is the input here that controls what symbol is to be created?

tautschnig · 2018-12-01T18:56:03Z

src/util/allocate_objects.cpp

+      assignments, target_expr, allocate_type, false, symbols_created);
+    break;
+
+  case allocation_typet::GLOBAL:


I'm not entirely happy with this terminology: the lifetime of an object vs its access scope are possibly different. In fact I don't know which one you are after for this one here. Is it about placing a symbol in the global namespace, or is it about allocation?

tautschnig · 2018-12-01T18:57:37Z

src/util/allocate_objects.cpp

+/// \param assignments: The code block to add code to.
+/// \param target_expr: The expression which we are allocating a symbol for.
+/// \param allocate_type: Type of the object allocated
+/// \param alloc_type: Allocation type (global, local or dynamic)


See also below: I'm used to static, stack, and heap allocation. The adjectives you use I would associate with "declaration," not "allocation." ("dynamic" is a weird one either way, but of course it so happens that it is used in CProver.)

Yeah this is a bit tricky terminology-wise since as you mentioned the access scope, lifetime, and the location of the allocated memory are different things.

The way I see it is that the main thing allocate_objectst does is generate code that allocates objects (irrespective of where the memory allocated for those objects might be located physically). The code to allocate the objects does so by either declaring a local variable (local scope, automatic lifetime), global variable (global scope, static lifetime), or using ALLOCATE() (dynamic).

I was thinking of renaming the members of allocation_typet to AUTOMATIC_LOCAL, STATIC_GLOBAL, and DYNAMIC. Would you be ok with that?

Would lifetimet be the most suitable name (instead of allocation_typet)? The suggested member names sound good to me, but mostly it's the use of "type" that makes me worried (hence suggesting lifetimet).

Yeah, liftetimet sounds good to me. I'll change it to that.

tautschnig · 2018-12-01T18:59:52Z

src/util/allocate_objects.cpp

+///
+/// \param assignments: Code block to which the necessary code is added
+/// \param target_expr: Expression to which the necessary memory will be
+///   allocated, its type should be pointer to `allocate_type`


I don't think you can allocate memory to an expression? Unless you are talking about the storage required by the syntax tree.

How about "A pointer to the allocated memory will be assigned to this (lvalue) expression"?

tautschnig · 2018-12-01T19:00:39Z

src/util/allocate_objects.cpp

+///   allocated, its type should be pointer to `allocate_type`
+/// \param allocate_type: Type of the object allocated
+/// \param static_lifetime: If `true` a global object will be created, if
+///   `false` a local object will be created


Ok, so "local" vs "global" is about the lifetime?

tautschnig · 2018-12-01T19:01:56Z

src/util/allocate_objects.cpp

+  if(!base_type_eq(allocate_type, target_expr.type().subtype(), ns))
+  {
+    aoe = typecast_exprt(aoe, target_expr.type());
+  }


Not exactly the same (because it uses plain equality), but still: I'd go for typecast_exprt::conditional_cast.

I also think it's likely that nearly-matching types (except at the very top level) may trip later passes into introducing (e.g.) unnecessary byte-extract operations

Also this (potentially over-eager) typecast omission is a change in behaviour compared to the old code AFAICT; I'd suggest in that case it would want testing with something which is base_type_eq but not type_eq (e.g. structs whose fields differ in using a symbol vs. a struct type for one of the members)

Ok, I've changed it to use typecast_exprt::conditional_cast (the original code used ns.follow on both types followed by comparing them via == to figure out whether a typecast should be introduced).

tautschnig · 2018-12-01T19:03:16Z

src/util/allocate_objects.cpp

+    {
+      malloc_symbol_expr =
+        typecast_exprt(malloc_symbol_expr, target_expr.type());
+    }


smowton · 2018-12-04T13:38:21Z

Unassigned for now as waiting for response re: base_type_eq

…ate_objects.h/cpp

…put order

allredj

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

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

danpoe requested review from cesaro, cristina-david, kroening, NathanJPhillips, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners November 19, 2018 15:54

xbauch reviewed Nov 19, 2018

View reviewed changes

thk123 reviewed Nov 20, 2018

View reviewed changes

hannes-steffenhagen-diffblue approved these changes Nov 20, 2018

View reviewed changes

hannes-steffenhagen-diffblue reviewed Nov 20, 2018

View reviewed changes

jbmc/src/java_bytecode/java_object_factory.cpp Outdated Show resolved Hide resolved

danpoe force-pushed the refactor/factor-out-object-allocation-from-object-factories branch from c1e0d0c to 3e21c82 Compare November 20, 2018 15:41

danpoe mentioned this pull request Nov 22, 2018

Generate function bodies that nondet havoc the function arguments [blocks: #3457] #3455

Merged

6 tasks

danpoe force-pushed the refactor/factor-out-object-allocation-from-object-factories branch from 3e21c82 to 4c17764 Compare November 23, 2018 12:15

allredj reviewed Nov 23, 2018

View reviewed changes

tautschnig changed the title ~~Factor out object allocation from object factories~~ Factor out object allocation from object factories [blocks: #3455] Nov 24, 2018

tautschnig added the blocker label Nov 24, 2018

tautschnig assigned danpoe Nov 24, 2018

danpoe added a commit that referenced this pull request Nov 27, 2018

Merge pull request #3251 from danpoe/feature/nondet-init-structs

28fd58d

Recursive nondet init of pointers to structs [blocks: #3443]

danpoe force-pushed the refactor/factor-out-object-allocation-from-object-factories branch from 4c17764 to 9c1348b Compare November 27, 2018 15:36

danpoe removed their assignment Nov 27, 2018

allredj reviewed Nov 27, 2018

View reviewed changes

chrisr-diffblue approved these changes Nov 29, 2018

View reviewed changes

tautschnig approved these changes Dec 1, 2018

View reviewed changes

tautschnig assigned smowton, peterschrammel and danpoe Dec 1, 2018

smowton unassigned smowton and peterschrammel Dec 4, 2018

danpoe force-pushed the refactor/factor-out-object-allocation-from-object-factories branch 7 times, most recently from 8b04439 to f071684 Compare December 17, 2018 18:01

danpoe assigned smowton and unassigned danpoe Dec 17, 2018

danpoe force-pushed the refactor/factor-out-object-allocation-from-object-factories branch 2 times, most recently from 0a1f50f to 68b3a4f Compare December 17, 2018 18:18

smowton approved these changes Dec 18, 2018

View reviewed changes

danpoe force-pushed the refactor/factor-out-object-allocation-from-object-factories branch from 68b3a4f to fda069a Compare December 18, 2018 14:22

danpoe assigned danpoe and unassigned smowton Dec 18, 2018

danpoe added 4 commits December 18, 2018 14:27

Factor out object allocation code from object factories to util/alloc…

9d4f8fe

…ate_objects.h/cpp

Use allocate_objectst in the c nondet object factory

1adfa5c

Use allocate_objectst in jbmc

255c6bd

Make nondet function arg regression tests independent of variable out…

890be45

…put order

danpoe force-pushed the refactor/factor-out-object-allocation-from-object-factories branch from fda069a to 890be45 Compare December 18, 2018 14:51

allredj reviewed Dec 18, 2018

View reviewed changes

danpoe merged commit 5594db6 into diffblue:develop Dec 19, 2018

danpoe deleted the refactor/factor-out-object-allocation-from-object-factories branch June 2, 2020 17:13

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Factor out object allocation from object factories [blocks: #3455] #3443

Factor out object allocation from object factories [blocks: #3455] #3443

danpoe commented Nov 19, 2018 •

edited

Loading

xbauch Nov 19, 2018

thk123 left a comment •

edited

Loading

hannes-steffenhagen-diffblue commented Nov 20, 2018

hannes-steffenhagen-diffblue left a comment

allredj left a comment

allredj left a comment

chrisr-diffblue left a comment

tautschnig left a comment

tautschnig Dec 1, 2018

tautschnig Dec 1, 2018

tautschnig Dec 1, 2018

tautschnig Dec 1, 2018

danpoe Dec 10, 2018

tautschnig Dec 14, 2018

danpoe Dec 14, 2018

tautschnig Dec 1, 2018

smowton Dec 3, 2018

tautschnig Dec 1, 2018

tautschnig Dec 1, 2018

smowton Dec 3, 2018

smowton Dec 3, 2018

danpoe Dec 15, 2018

tautschnig Dec 1, 2018

smowton commented Dec 4, 2018

allredj left a comment

Factor out object allocation from object factories [blocks: #3455] #3443

Factor out object allocation from object factories [blocks: #3455] #3443

Conversation

danpoe commented Nov 19, 2018 • edited Loading

Choose a reason for hiding this comment

thk123 left a comment • edited Loading

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue commented Nov 20, 2018

hannes-steffenhagen-diffblue 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

chrisr-diffblue 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

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 commented Dec 4, 2018

allredj left a comment

Choose a reason for hiding this comment

danpoe commented Nov 19, 2018 •

edited

Loading

thk123 left a comment •

edited

Loading