[TG-1422] Bugfix for a precondition fail in the interpreter after generics support has been introduced

[NlightNFotis]

So some notes about this:

The new datatype introduced java_specialised_generic_class_typet will be further modified, as this is part of an active PR (#1576), so do not make blocking comments on its design if possible, as it's not final.

The same applies for the concretisation process in src/java_bytecode/generate_java_generic_type.cpp. It is to be heavily revamped very soon.

The whole point of this PR is to allow an urgent fix to be applied to CBMC so that tests for generics can be generated without hitting invariant violations because of some spurious goto statements in the goto program.

For more information about the nature of the bug that this fixes, feel free to contact me directly, or @smowton or @antlechner.

This needs an urgent review from @peterschrammel

[tautschnig]

As urgent as it may be: this has conflicts.

[tautschnig]

There seem to be at least two problems here:

1. A dependency from goto-programs on java_bytecode is introduced. (There may be a case for moving java_types.h to util/.)
2. If code taking the address of a struct is generated, then this code must be fixed rather than weakening the preconditions elsewhere. Taking the address of a non-lvalue never is valid code.

[smowton]

@tautschnig I don't believe anyone is taking the address of a struct. The problem is aliasing incompatible types. If I had a C program:

struct A { int x; int y; };
struct B { int z; int w; };

int main() {
  struct A a;
  struct B *b = (struct B*)&a;
  b->z = 0;
}

...then symex would turn b->z = 0; into ((struct B)a).z = 0; after it removes the deref operation.

The current Java generics code is running into the same problem because it uses unrelated types to represent Generic<T> and Generic<Object>; thus when symex executes Generic<T>::f() { this->x = 0; } it notes that this is a Generic<T>* while *this is a Generic<Object> and again a typecast is produced.

The long-term fix is to either restructure generics so that existing code for handling inheritance deals with the situation, or else to teach symex about type specialisations. Meanwhile I'll suggest hacking the trace in test-gen to remove casts and make it acceptable to the current GOTO interpreter.

[tautschnig]

[...] again a typecast is produced.

I don't see a problem with typecasts per se, but here we are talking about the function evaluate_address, and the newly introduced comment suggests that we aren't actually getting something that is an address?

[smowton]

It would be better named evaluate_address_of. For example, look at the base case for an ID_symbol --
that looks the symbol up in the address map. The expression that was originally causing trouble was of the form ((struct A)some_symbol).some_field, which is a legitimate thing to take the address of.

[tautschnig]

It would be better named evaluate_address_of.

Indeed; wasn't the precondition introduced in 520cf38 actually always too strong? I'd say the correct fix is to drop the precondition altogether, which would right away also resolve my other concerns about introducing Java-specifics into goto-programs/.

[smowton]

That would be ok with me, though I still think generics long-term need encoding in a way that symex understands. (In particular some type attribute indicating that as a specialisation of another type it matches it in field names, field widths etc, so it always suffices to cast the member rather than cast the whole struct)

[NlightNFotis]

The workaround for the problem that we have is going to be fixed with the way that was suggested, removing the strong precondition, rendering this PR invalid.

Thank you all for your input.