Is this redundant with #2125?

No, the two problems are distinct. The null-pointer-might-be-accessed situation results in a pessimistic assumption about the pointer (ptr == &dynamic_object1 ? dynamic_object1.accessed_field : ptr$invalid_object.accessed_field), whereas the phi-merge-of-version-0 problem introduces uncertainty about the value of dynamic_object1.accessed_field itself by merging dynamic_object1#1, which is initialised, with dynamic_object1#0, which isn't (introducing dynamic_object1#2 == guard ? dynamic_object1#1 : dynamic_object1#0). Thus even if we were certain about the value of ptr an access to ptr->accessed_field would not be constant propagated.

It is however related to #2125 in that both rely on a safe memory model to prevent me from accessing the memory associated with dynamic_object1 when it hasn't been initialised.

To phrase that differently, in the program

A a = null;
if(nondet)
  a = new A(1);
// PHI

if(a != null)
  return a.somefield;

There are two things preventing symex from propagating 1 to the return value. Symex thinks there are two possible paths: one where new A was called, a is non-null, and the return value is 1, and one where new A was not called, a is null, and the return value is nondet.

#2125 says that because the access is checked, at the line return a.somefield we can safely assume a != null, and this PR says that we can disregard the dynamic-object-is-uninitialised path from consideration at the phi node labelled // PHI, because ability to access the object implies it has been initialised.

@tautschnig possible idea for removing language-specificity in Symex: the ID_allocate side-effect expression already has its zero-init attribute. Even if we intend to overwrite it immediately, we could just set that to true for Java allocations, then symex would copy the attribute onto the dynamic object it creates.

Then the test wouldn't be "is this Java," it would be "does the object have ID_C_always_initialized?"

Discussed in person with @kroening: the agreed solution is for symex to ensure some explicit nondet value is written on malloc, similar to what is already done for code_declt, then we can always assume that a particular identifier being of generation 0 implies it doesn't exist at all on that path, and avoid merging it (i.e. remove the limitation to Java code)

Note on that: check that array allocations, in C, C++ and Java, are all subject to this rule (that some nondet init happens if there isn't an explicit zero init)

Replaced by #2168