insert-annotations-to-source tool: Replace instead of add annotation.

[pbsf]

The insert-annotations-to-source tool adds annotations on top of existing programmer-written annotations.
For example, consider the programmer-written annotated field on a source code file:

@top String field;

If, for example, in the .jaif file associated to this source code file "field" has type @bottom, after running the insert-annotations-to-source tool the resulting source code file will contain:

@bottom
@top String field;

That may generate errors depending on the type system, which is a problem.

Possible solution: Passing an argument to the tool would state whether the user wants to replace programmer-written annotations in cases of conflict. (-ra, --replaceannotations)

[wmdietl]

I assume you mean "replace" within one type system. In the general case, some source code might be annotated with multiple type systems.
The feature would then need to be implemented in a way such that the annotation gets added, if no annotation from the same hierarchy exists yet, or it replaces an annotation from the same hierarchy.

However, this would require annotation-tools to understand the type hierarchies of the type systems, which is coupling with the Checker Framework that we don't want.

I see two options:

• In the beginning of the .jaif file we currently declare the annotations that get handled. We could add a simple format to also declare the qualifier hierarchy, which would then allow a meaningful implementation of "replace".
• In the .jaif file, instead of just specifying that "@bottom" gets added you would need to specify to also remove "@top". When generating the .jaif file you should have the information about what annotations already exist in that location and can generate this easily.

Do you see other options?

[pbsf]

Yes, I was considering a single type system.

I can't think of any better options than the ones you suggested. Both solutions seems good to me.

The disadvantage that I can see in the first option is that describing the hierarchy can be a problem if type annotations have other type annotations as fields - it seems easy to describe the nullness type hierarchy for example, but the intent type system hierarchy would be a problem.

Should .jaif files be readable by developers? I think the .jaif file can get confusing if there are a lot of "remove this", "add that", which are related to the second option. It's simpler to just have some reserved space on the beginning of the file to describe hierarchies, even if they are hard to describe.

[mernst]

I agree about defining the hierarchy at the beginning of the file. That is also more robust than removal commands that assume the source code is exactly as it was when the inference tool was run.