Add support for type annotations

[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]

I have a stupid questions:

1. Does this impact KeyJavaType?
2. Is @NonNull <: @Nullable T? Or do we ignore annotations on type and sort hierarchy?
3. Why is KeyJavaType replaced by TypeReference? They have different purposes; the first one is semantical, the later one is syntactical.

[wadoon]

Review: PR #3992 — “Add support for type annotations”

• Repo: KeYProject/key
• Author: PiIsRational (@PiIsRational), WolframPfeifer involved
• State: draft, OPEN, milestone v3.1.0
• Scope: 142 files, +1561 / −8854 (net-negative due to ~20 deleted/regenerated example .proof files)
• Head branch: key-annotations (commits 230f842d…d563cb17, 69 commits vs main)
• Build check on branch head: ./gradlew compileJava compileTestJava → BUILD SUCCESSFUL

Summary

The PR reads type annotations from Java sources, stores them in TypeReferences (not KeYJavaTypes), and exposes them via three new variable conditions: \hasAnnotation, \addAnnotation, \removeAnnotation. To make annotations reachable on variables, KeYJavaType is replaced by TypeReference in ProgramVariable/LocationVariable and in most places that construct or copy typed program elements (metaconstructs, contract builders, WD/infoflow modules, tests).

The mechanical part of the refactor is careful and consistent; everything compiles, including the test sources. The new logic in the annotation path has several correctness problems that should be fixed before merge.

High severity

1. TypeReferenceImp.match is logically inverted (broken program matching)

key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/TypeReferenceImp.java:253-263

public MatchConditions match(SourceData source, MatchConditions matchCond) {
    final ProgramElement pe = source.getSource();

    if (pe instanceof TypeReference tr
            && tr.getDimensions() == getDimensions()
            && tr.getAnnotations().equals(getAnnotations())) {
        return null;      // <- `null` means MATCH FAILED
    }

    return super.match(source, matchCond);
}

The upstream version (main) fails the match only when the source is not a type reference or the dimensions differ:

if (!(pe instanceof TypeReference)
        || ((TypeReference) pe).getDimensions() != getDimensions()) {
    return null;
}
return super.match(source, matchCond);

The new code does the opposite: it fails the match exactly when the source is a matching type reference (same dims and same annotations) and delegates to super.match in all other cases — where super (class equality + children) does not compare annotations at all. Therefore:

• a plain pattern type ref matched against a plain source type ref → always fails via the monolithic matcher;
• a pattern with different annotations than the source → falls through to super.match and may succeed.

The intended change was to extend the guard, i.e. || !tr.getAnnotations().equals(getAnnotations()) inside the existing failure condition. Fix and add a unit test exercising the monolithic match path (e.g. a \program pattern containing a type ref).

2. Annotation.equals always returns false

key.core/src/main/java/de/uka/ilkd/key/java/ast/Annotation.java:31

return o instanceof Annotation annot
        ? annot.type.equals(type) && super.equals(type)
        : false;

super.equals(type) passes the KeYJavaType into JavaNonTerminalProgramElement.equals, which immediately rejects it with o.getClass() != this.getClass(). Hence the second conjunct is always false, and two structurally identical marker annotations (same annotation type) are never equal. Consequences:

• ImmutableList.equals on annotation lists (used in the match above and anywhere annotations are compared) never matches for non-empty lists;
• deduplication / set semantics for annotations are broken;
• no hashCode override either (inherited one is class-only), so equality and hash are inconsistent with the class hierarchy.

Should be super.equals(annot) (plus a hashCode).

3. Only marker annotations are supported; annotations with arguments abort loading

key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java:2112-2119

public Object visit(NormalAnnotationExpr n, Void arg) { return reportUnsupportedElement(n); }
public Object visit(SingleMemberAnnotationExpr n, Void arg) { return reportUnsupportedElement(n); }

reportUnsupportedElement throws JavaBuildingExceptions. So any type annotation with members — @Size(min = 1), @Nullable(reason = "..."), @Target(ElementType.TYPE_USE) used as value — fails the whole parse. At the same time, declaration annotations on fields/methods (@Override, @SuppressWarnings("..."), @Deprecated(since = "...")) are silently dropped, because visit(FieldDeclaration)/visit(MethodDeclaration) never visit getAnnotations().

Given that annotations are the core feature here, the marker-only limitation (and the hard failure) should at least be documented and ideally handled gracefully (skip + warning) instead of throwing.

Medium severity

4. AnnotationMover misses single-value @Target(TYPE_USE)

key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/AnnotationMover.java:95-120
isTypeAnnotationSlow only recognizes the target when the annotation value is an ArrayInitializerExpr (@Target({ElementType.TYPE_USE})). The very common shorthand @Target(ElementType.TYPE_USE) is a SingleMemberAnnotationExpr with a name expression → silently classified as not a type annotation → not moved → dropped by the converter.

5. AnnotationMover caches by simple name

AnnotationMover.java:90-91 — typeAnnotationMap is keyed by the annotation’s simple name; two distinct annotations with the same simple name in different packages poison the cache in both directions. Additionally, d.getParentNode().get() and annot.setParentNode(type) are manual javaparser AST manipulations that are easy to get out of sync; a comment on the intended AST invariant would help.

6. AddAnnotation.build() may create MarkerAnnotation(null)

key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AddAnnotation.java:122
services.getJavaInfo().getTypeByName(annot) returns null for unknown names; the resulting null-typed annotation NPEs later in toString / pretty printer / HasAnnotationCondition.matchesTypeAnnots (getKeyJavaType().getFullName()). Validate the annotation name up front with a meaningful error.

7. HasAnnotationCondition compares a sort by its string name

key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasAnnotationCondition.java:33-47
variable.sort().toString().equals("Field") — use the Field sort constant (HeapLDT / JavaDLTheory) instead of a name-string comparison.

8. Inconsistent annotation matching between the two matchers

key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/JavaProgramMatchPlanBuilder.java (typeReferencePlan), unchanged by this PR, guards only instanceof TypeReference + dimensions and ignores annotations, while the (broken) TypeReferenceImp.match above tries to compare them. Annotated types therefore match differently depending on the matcher path. If annotations are part of a type use’s identity, typeReferencePlan’s guard needs the same annotations check.

9. Annotations are not part of the AST child structure; TypeRef equality ignores them

key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/TypeReferenceImp.java — getChildCount/getChildAt cover only prefix + name, so JavaNonTerminalProgramElement.equals/hashCode treat TypeRef(@A C) and TypeRef(C) as equal. Combined with #1 and #2, annotation-related equality semantics are inconsistent across equals, match, and the VM guard. Choose one semantics and make all three agree.

10. ProgramVariable.getReferencePrefix() changed from null to the type ref’s prefix

key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java
Previously “we do not have a prefix, so fake it → null”; now return type.getReferencePrefix();. Every LocationVariable built from new TypeRef(kjt) therefore has a (package) reference prefix where it previously had none, changing ReferenceSuffix/parsing behavior for chains like a.b. Additionally getKeYJavaType() is now null-capable (type != null ? type.getKeYJavaType() : null) while proofToString() dereferences it without a null check. Verify this does not change how a.b is parsed/matched, or add a regression test.

Low / nits

• RemoveAnnotation.toString() prints \addAnnotation (copy-paste bug, RemoveAnnotation.java:115); its constructor throws RuntimeException while AddAnnotation/HasAnnotationCondition use IllegalArgumentException.
• New classes lack javadoc / class documentation: Annotation, MarkerAnnotation, AnnotationInterfaceMemberDeclaration. The javadoc of TypeRef now references a non-existent ImmutableList<AnnotationExpression> type.
• Package layout: Annotation lives in ...java.ast, but MarkerAnnotation in ...java.ast.annotation — inconsistent.
• Naming: HasAnnotationCondition vs AddAnnotation/RemoveAnnotation — inconsistent “Condition” suffix.
• The varcond annotation-name argument is a plain string; only simple names are demonstrated. For non-default packages the FQN must be spelled out — worth documenting or resolving via the symbol table.

Examples / shipped files

• ~20 user-facing example proofs were deleted (key.ui/examples/heap/observer/*.key.proof, pred_log/specialNat.key.proof, equalities2.key.proof). If they no longer replay because of the refactor, regenerate rather than delete — these ship in the UI. Also pred_log/count.key.proof was renamed to standard_key/unicode_test.key.proof; count.key does not exist, so verify the renamed proof actually replays for unicode_test.key.
• New test surface is thin: the PR’s own checklist (“Add tests for the variable conditions”) is still open. There is one g.provable("Java/Annotations/test_annotation.key") entry and the annotation-declaration coverage-load test (AnnDecl.java — @interface + a @Marker(3) single-member annotation). No unit tests for AddAnnotation/RemoveAnnotation/HasAnnotationCondition, no pretty-printer round-trip with annotations, no tests for @Target variants or annotated arrays/generics.

Answers to the design questions in the PR thread

Regarding @wadoon’s questions (and the general KeYJavaType vs TypeReference concern):

• KeYJavaType impact: minimal — it remains the semantic anchor (TypeRef still resolves to the same KJT; getDefaultValue merely became @Nullable). The refactor moves type-use information out of it.
• Are annotations part of the sort/hierarchy? No: annotations are inert w.r.t. sorts and subtyping; \hasAnnotation is a purely syntactic check on the type reference, and the demo unsound.key shows that the semantic content is whatever the rule author gives it.
• Why TypeReference for ProgramVariable? Justified by the goal — annotations live on syntactically annotated type uses, not on the resolved type. The trade-off: ProgramVariable is a logic-level name, and its behavior surface (getReferencePrefix, null-capable getKeYJavaType, name-only equality) changes as a result; findings KeY / Recoder transforms JML set statments for ghost variables wrongly #1/<deleted> #9/<deleted> #10 are exactly where this shows up.

Conclusion / requested changes

The refactor itself is clean and compiles, but before this goes much further:

1. Fix the inverted TypeReferenceImp.match (KeY / Recoder transforms JML set statments for ghost variables wrongly #1).
2. Fix Annotation.equals (+ hashCode) (<deleted> #2).
3. Decide the behavior for annotations with arguments and declaration annotations (fail vs. skip + warning) and document the marker-only scope (<deleted> #3).
4. Add unit tests for the three variable conditions and the matcher path.

If you want, this review can be posted (full or condensed) to the PR via gh.

Zeilen 1-148