[PiIsRational]

Intended Change

The Goal of this Pull Request is to be able to use Java Type Annotations in Taclets.
To make this work the Type Annotations were added to the KeY Ast at the TypeReference level.
The annotations were added to the type references, since they correspond to the syntactical
version of the types. Since in most places KeYJavaTypes were used, there was the need
to replace them.

The default matching behaviour was not altered and is compatible with the current
master branch. This means that there is no semantic difference between Object o
and @Rep Object o. Therefore, no taclets need to be altered and annotations are simply
ignored per default.

To interact with annotations in taclets there are currently 3 variable conditions:

• hasAnnotation(SchemaVariable variable, String annot):
  It checks that the type (TypeReference) of variable has an annotation whose
  fully qualified name matches annot. It supports ProgramVariables, New
  (simple constuctor calls) and Fields.
• addAnnotation(SchemaVariable store, SchemaVariable read, String annot):
  It creates a copy of read and stores in store except that the last annotation
  of the type of store now corresponds to annot. If the given string annot does
  not match an annotation, the variable condition fails.
  It supports ProgramVariables and New (simple constructor calls).
• removeAnnotation(SchemaVariable store, SchemaVariable read, String annot):
  It creates a copy of read where all annotations of the type of read
  with the fully qualified name matching annot are removed and stores it in store.
  This variable condition matches always and only supports New (simple constructor calls).

Currently only, Marker annotations so annotations with no arguments
(such as @NonNull or @Rep) are supported.

Example

In the context of a Nullness type system (where the @NonNull) annotation
is type checked we could have something like the following snippet:

import checker.qual.NonNull;

/*@ normal_behaviour
  @ ensures o != null; */
public Object id(@NonNull Object o) {
    return o;
}

To be able to use the guarantee expressed by the annotation we could write the following
Taclet:

nonNull {
    \schemaVar \term Object o;

    \find(o)
    \varcond(\hasAnnotation(o, checker.qual.NonNull))

    \add(o != null)
}

A further (similar) example can be found here.
The main use of this change is PR #3724 and can be found here (mainly in universeDefs.key).

Plan

• Add tests for the variable conditions
• Add documentation

Type of pull request

• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• I added new test case(s) for new functionality.
• I have tested the feature as follows:
  • I made use of it in Universe Type Rules #3724

Additional information and contact(s)

@WolframPfeifer is involved in this Pull Request

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[wadoon]

Stupid remarks:

• The documentation of the variable conditions are generated (see Generate user documentation for varconds and proof script commands #3977). You do not add your documentation there (so the plan(tm))

• \addAnnotation seems a bit odd. Is this the "right" way, or should we prefer transformers instead (@unp1)? I thought the same for the instanceof pattern thing.