TG-374 Feature/java support generics

[mgudemann]

No description provided.

[thk123]

It is a big ask, but what would really help to understand what this new data means would be some unit tests on the results of the parsing. If you look in cbmc/unit/java_bytecode/java_bytecode_convert_class you should find some inspiration on how you might go about this.

[thk123]

Shouldn't this be an invariant?

[thk123]

I would expression the condition and the comment in the same way:

method.local_variable_table.size() >= local_variable_type_table_length

I would probably also use variable table instead of LVT to be consistent with type table (or change both to acronyms, as I initially assumed LVT=LVTT).

[thk123]

Sorry, I know we talked about it, but what is the difference between this and just a java_generic_typet?

[peterschrammel]

has_signature

[peterschrammel]

remove code that is commented out (several instances)

[peterschrammel]

This looks very error-prone. Is there no better way of parsing this? At least some unit tests would be good.

[mgudemann]

why would it be error prone? The idea is to identify corresponding opening and closing > to see where the type variables are defined or substituted.
The java_generics_find_closing deals this by counting the opening and closing >.

[thk123]

Don't check in with this define

[thk123]

I have some concerns about the fields added to the type - I fear we pass ireps by value and hence non-tracked fields might be sliced away (perhaps unit tests will prove I am wrong).

I think the naming change will significantly aid understanding.

[thk123]

Is it OK for this to be a reference?

[thk123]

Is it OK to add fields to a irep class? I would worry that sometimes they are passed around by value - though I don't know, if there are other irep's that do this I guess it is fine?

[thk123]

Specifically, we return typet by value from java_type_from_string in java_types.cpp, won't these extra fields be sliced away?

[thk123]

Could this be a std::vector<java_generic_typet>?

[thk123]

Also I think this might be sliced away.

[thk123]

Consider pulling this case out into its own function

[NlightNFotis]

I agree with this assessment as a matter of consistency with the other cases.

[mgudemann]

this seems consistent with the other more complex case 'L'

[thk123]

I think I get it - this is type that is a generic parameter (either with a bound or it is a java_inst_generic_typet if we know the actual type). Consider renaming to java_generic_parameter_typet since a generic type in Java normally means a type that has generic parameters rather than the parameters themselves.

[thk123]

You might consider calling this java_generic_typet though if you wish to keep it as this since more explicit then that's fine.

[NlightNFotis]

The fact that the if statement has braces around its body, but else doesn't, and is also followed by another statement immediately after its body. This is inviting bugs and confusion in the future, I think.

[NlightNFotis]

I agree with this assessment as a matter of consistency with the other cases.

[mgudemann]

@NlightNFotis @thk123 @peterschrammel maybe you could have another look
as @NlightNFotis has begun working on this branch, I have not yet squashed rebased this.

[thk123]

I will review the unit tests tomorrow but this looks good. No major changes but a few bits of tidy up.

[thk123]

Nit:

const typet &t=java_type_from_string(m.has_signature ? m.signature : m.descriptor);

Since reduces duplication and allows const-correctness on t.

[mgudemann]

agreed, but then we will have to split up again when doing this in a try block to fall-back to parsing the descriptor in case we hit a signature we do not support yet

[thk123]

I remain slightly concerned about turning tests off (even with issues to turn them back on). Did this do anything useful that it now no longer does?

[mgudemann]

it fails to parse the signature and therefore bails out with an invariant violation, same for the two other cases
This will be restored temporally once we ignore signatures we cannot parse currently, and then be fixed once we can parse classes with instantiated signatures.

[thk123]

I'm not sure there should be code after UNREACHABLE;. Consider converting the if to an assertion?

[thk123]

For convenience, could you add a comment suggesting what kind of field would take this path. I think this would be:

T f;

(I.e. a field whose type is a generic parameter)

[thk123]

As above, a comment saying what kind of field would follow this path. I think:

List<Float>
List<T>

[thk123]

As with others - I think a comment showing the kind of Java that would have this type:

/// For example, a class definition `class MyGenericClass<T>`

[thk123]

Nit: const java_generic_typet &t

[thk123]

Prefer const java_generic_class_typet &t then you can drop the precondition

[thk123]

Prefer const java_generic_class_typet &t then you can drop the precondition

[thk123]

You might consider unit testing this since this is the kind of thing it is a) easy to unit test and b) easy to make silly mistakes. It also has the added benefit of documenting the "fence post" behaviour (e.g. does it return the position immediately before or after the closing >)

You might also consider pulling it into a utility and taking the bracket as an arg as I guess this is quite a common thing to want to do.

[thk123]

There is a reasonable amount of duplication in the unit tests that I think would massively help readability if tidied up. In particular, you can nest the Catch macros as much as needed

[thk123]

To aid test readability - you might want to pull you the parse/typecheck/final into a utility function at the top:

void load_and_parse(std::unique_ptr<languaget>java_lang, const std::string class_path, symbol_tablet &out_symbol_table)
{
  java_lang->parse(...
  java_lang->typecheck(out_symbol_table, "");
  java_lang->final(out_symbol_table)
}

[thk123]

This looks to overlap with the above test - probably better to have more REQUIREs in one test than duplicate it as it makes it hard to see what is being tested. (It can go in a separate THEN block but the common loading code can be shared. something like THEN("The class symbol should be generic")...THEN("The element should be a generic parameter")

[thk123]

Can we add some more assertions here (e.g. is there a way to find out the generic parameter name is "E"?)

[thk123]

Again - try and combine the overlap with the above tests and just have different THEN blocks for documenting different checks

[thk123]

For clarity, you might want to pull these checks into a single function:

java_class_typet CheckIsJavaClass(const typet &type)
{
  REQUIRE(symbol_type.id()==ID_struct);
  class_typet class_type=to_class_type(symbol_type);
  REQUIRE(class_type.is_class());
  return to_java_class_type(class_type);
}

I've done something like this in an unrelated PR: write_expr.cpp which you might consider using as a model. I think it helps keep the intent of the tests clear and reduces total number of lines in the test.

[thk123]

Overlap with the other test that parses this file to keep tests together and to reduce duplication

[thk123]

The unit tests look great! Just a few nits to apply as you see fit but no need to get re-approved. Could you however create a bumping PR on test-gen to check it doesn't break anything downstream.

[thk123]

Nit: multi-line body of if should be wrapped in braces

[thk123]

Nit: multi-line body should be wrapped in braces

[thk123]

Nit: multi-line body should be wrapped in braces

[thk123]

Old comment style; should be doxy

[thk123]

And do please document class_name as this is not obvious what it does

[thk123]

Nit: a summary of what a lvtt in doxygen comment might be good

[thk123]

Should probably use close_char rather than >

[thk123]

Nit: name the parameters so users of the function can know which char does what. You might also consider overloading this with a method that takes just one char (say '(') and figure out the closing one.

[thk123]

How come this works, you only parse the generics.class file? Does it auto pull in the others as dependencies?

[NlightNFotis]

Some comments with small requests for documentation changes. Nothing too big I think, and they are non-blocking changes (feel free to merge without them)

[NlightNFotis]

Why is it config.ansi_c.pointer_width in some calls to the reference_typet constructor, but it's a hardcoded 64 here? Is there any significance to this value here?

[NlightNFotis]

Can this be documented why this happens? Why when we create a new java_generic_inst_parametert we pass an empty string essentially to the java_generic_parametert constructor, causing an empty symbol to be pushed to type_variables?

[NlightNFotis]

Doesn't this return an instantiated java_generic_parameter?

[NlightNFotis]

Can there be some spacing, or better yet, some curly braces enclosing the else statement to better denote intention?

[NlightNFotis]

This is part of the rest of the work to support generics, right?

[NlightNFotis]

I support the usage of optional here, and around lines 107 in the same file.

[NlightNFotis]

This is a cast, and doesn't return a boolean value.

[NlightNFotis]

LGTM