[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 oand @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 @Null annotation is type checked and means that the only value of a type with this annotation is null) we could have something like the following snippet:

class Nop {
    @Null Object o;

    /*@ ensures o == null; */
    void nop() {}
}

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

selectNull {
    \schemaVar \term Object o;
    \schemaVar \term Field f;
    \schemaVar \term Heap h;

    \find(select<Object>(h, o, f))

    \varcond(\hasAnnotation(f, Null))

    \replacewith(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.

[WolframPfeifer]

For documentation: The above example does not work with the current implementation. The HasAnnotation varcond is not applicable (throws an error in the constructor). I think the issue is that at the time when the varcond is evaluated, the information about the annotation is already lost, so there is no possibility to access the annotations of parameters (of the current method under proving) in taclets. I think this is a general limitation and cannot be overcome with taclets.

That is the reason why for the branch that adds Universe Type support, a new pipeline step had to be added (UniverseMethodContractAdder), which adds the information from the annotations via the UT predicates.

The PR description needs to be changed, maybe with the working example from the test cases instead.
As far as I understood, the new varconds support annotations with field select, on new statements, and local variable declarations.