Replace fresh_java_symbol in object factory

[antlechner]

It looks to me like allocate_objectst, which is a relatively new class, is supposed to take care of all kinds of variable and memory allocations for both Java and C now. It seems likely that we will eventually want to replace all calls to fresh_java_symbol with calls to allocate_objectst::allocate_automatic_local_object.

I am not 100% sure if this is really the intention behind the new class, which is why am making the change in the object factory only for now, and hoping to get some comments from reviewers to clarify if this should be done elsewhere as well.

A related question is the naming of the methods of allocate_objectst: all of them start with allocate_..., while only the dynamic version corresponds to an ALLOCATE in the GOTO program; the others just create new variable symbols but don't allocate any memory. I found this quite confusing, is there a good reason behind the common name?

Any advice on this would be appreciated.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a 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.

[smowton]

All variations of allocate_* allocate memory, they just do it in different ways:

Allocating a global creates a static-lifetime symbol and with it an allocation of memory that lives as long as the program

Allocating a local creates a non-static-lifetime symbol, which itself doesn't embody memory, but the DECL / code_declt instruction that is also created allocates memory that lives as long as the function containing it (in practice when we do this in __CPROVER__start that memory lives as long as the program)

Allocating using the actual ALLOCATE instruction produces a fresh block of memory every time it is executed; since we don't implement free / delete, it too lives as long as the program.

[owen-mc-diffblue]

@antlechner Doxygen failure:

/home/travis/build/diffblue/cbmc/jbmc/src/java_bytecode/java_object_factory.cpp:361: warning: The following parameters of initialize_nondet_string_fields(struct_exprt &struct_expr, code_blockt &code, const std::size_t &min_nondet_string_length, const std::size_t &max_nondet_string_length, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, bool printable, allocate_objectst &allocate_objects) are not documented:
  parameter 'allocate_objects'

[antlechner]

@owen-jones-diffblue I added Doxygen for the new parameter.
@smowton Thank you for the explanation. I'm still a bit confused about the difference between static allocation and dynamic allocation in a GOTO program that never frees memory after it is allocated. As a GOTO program isn't compiled and run like a C program would be (where static allocation would be handled by the compiler and dynamic allocation would be at runtime), and as it doesn't use free, wouldn't the two types of allocation just end up doing the same thing?

[tautschnig]

@antlechner There still is a difference, and it isn't all that different from dynamic execution: statically allocated objects will get an entry in the symbol table (e.g., you will find them in cbmc --show-symbol-table), while the same symbol table is not going to hold information about dynamic objects. Also, statically allocated objects will typically have a defined initial value, while the same is typically not true of dynamically allocated ones. In the same vein, goto-analyzer or janalyzer will know what to do with statically allocated objects, while typically they have no idea about dynamically allocated ones. That situation is different for cbmc/jbmc, as during symbolic execution indeed there isn't really a big difference anymore between statically and dynamically allocated ones.

[allredj]

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

[antlechner]

@tautschnig Thank you, that clarifies things a lot. I had thought about this only from a CBMC/JBMC perspective and hadn't considered other related tools. I'll try to find time to document these differences in allocate_objects.h.