File: KeyForSubtyping.java

package info (click to toggle)
checker-framework-java 3.2.0%2Bds-3
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 23,104 kB
  • sloc: java: 145,916; xml: 839; sh: 518; makefile: 404; perl: 26
file content (130 lines) | stat: -rw-r--r-- 4,345 bytes parent folder | download | duplicates (3)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
import java.util.HashMap;
import org.checkerframework.checker.nullness.qual.*;

public class KeyForSubtyping {
    HashMap<String, String> mapA = new HashMap<>();
    HashMap<String, String> mapB = new HashMap<>();
    HashMap<String, String> mapC = new HashMap<>();

    public void testSubtypeAssignments(
            String not_a_key,
            @KeyFor("this.mapA") String a,
            @KeyFor("this.mapB") String b,
            @KeyFor({"this.mapA", "this.mapB"}) String ab) {
        // Try the error cases first, otherwise dataflow will change the inferred
        // annotations on the variables such that a line of code can have an
        // effect on a subsequent line of code. We want each of these tests to
        // be independent.

        // :: error: (assignment.type.incompatible)
        ab = a;
        // :: error: (assignment.type.incompatible)
        ab = b;
        // :: error: (assignment.type.incompatible)
        a = b;
        // :: error: (assignment.type.incompatible)
        a = not_a_key;
        // :: error: (assignment.type.incompatible)
        b = not_a_key;
        // :: error: (assignment.type.incompatible)
        ab = not_a_key;

        // Now try the success cases

        a = ab;
        b = ab;
        not_a_key = ab;
        not_a_key = a;
    }

    public void testDataFlow(
            String not_yet_a_key,
            @KeyFor("this.mapA") String a,
            @KeyFor("this.mapB") String b,
            @KeyFor({"this.mapA", "this.mapB"}) String ab) {
        // Test that when a valid assignment is made, dataflow transfers the
        // KeyFor type qualifier from the right hand side to the left hand side.

        // :: error: (argument.type.incompatible)
        method1(not_yet_a_key);
        not_yet_a_key = a;
        method1(not_yet_a_key);

        method1(a);
        // :: error: (argument.type.incompatible)
        method1(b);
        method1(ab);

        b = ab;
        method1(b);
    }

    public void testSetOrdering(
            @KeyFor({"this.mapC", "this.mapA"}) String ac,
            @KeyFor({"this.mapA", "this.mapB", "this.mapC"}) String abc) {
        // Test that the order of elements in the set doesn't matter when doing subtyping checks,
        // @KeyFor("A, B, C") <: @KeyFor("C, A")

        // Try the error case first - see the note in method testSubtypeAssignments

        // :: error: (assignment.type.incompatible)
        abc = ac;

        ac = abc;
    }

    public void testDataflowTransitivity(
            @KeyFor({"this.mapA"}) String a,
            @KeyFor({"this.mapA", "this.mapB"}) String ab,
            @KeyFor({"this.mapA", "this.mapB", "this.mapC"}) String abc) {
        ab = abc;
        // At this point, dataflow should have refined the type of ab to
        // @KeyFor({"this.mapA","this.mapB","this.mapC"})
        a = ab;
        // At this point, dataflow should have refined the type of a to
        // @KeyFor({"this.mapA","this.mapB","this.mapC"})

        // This would not succeed without the previous two assignments, but should now because of
        // dataflow.
        abc = a;
    }

    private void method1(@KeyFor("this.mapA") String a) {}

    private void testWithNullnessAnnotation(
            String not_a_key,
            @KeyFor("this.mapA") String a,
            @KeyFor("this.mapB") String b,
            @Nullable @KeyFor({"this.mapA", "this.mapB"}) String ab) {
        // These fail only because a @Nullable RHS cannot be assigned to a @NonNull LHS.

        // :: error: (assignment.type.incompatible)
        a = ab;
        // :: error: (assignment.type.incompatible)
        b = ab;
        // :: error: (assignment.type.incompatible)
        not_a_key = ab;

        not_a_key = a; // Succeeds because both sides are @NonNull
    }

    // Test overriding

    static class Super {
        HashMap<String, String> map1 = new HashMap<>();
        HashMap<String, String> map2 = new HashMap<>();

        void method1(@KeyFor({"this.map1", "this.map2"}) String s) {}

        void method2(@KeyFor("this.map1") String s) {}
    }

    static class Sub extends Super {
        @Override
        void method1(@KeyFor("this.map1") String s) {}

        @Override
        // :: error: (override.param.invalid)
        void method2(@KeyFor({"this.map1", "this.map2"}) String s) {}
    }
}