/
WholeProgramInferenceImplementation.java
929 lines (852 loc) · 40 KB
/
WholeProgramInferenceImplementation.java
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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
package org.checkerframework.common.wholeprograminference;
import com.sun.source.tree.ClassTree;
import com.sun.source.tree.MethodTree;
import com.sun.source.tree.Tree;
import com.sun.tools.javac.code.Symbol.ClassSymbol;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import javax.lang.model.SourceVersion;
import javax.lang.model.element.AnnotationMirror;
import javax.lang.model.element.Element;
import javax.lang.model.element.ExecutableElement;
import javax.lang.model.element.TypeElement;
import javax.lang.model.element.VariableElement;
import javax.lang.model.type.TypeKind;
import javax.lang.model.util.ElementFilter;
import org.checkerframework.afu.scenelib.util.JVMNames;
import org.checkerframework.common.basetype.BaseTypeChecker;
import org.checkerframework.dataflow.analysis.Analysis;
import org.checkerframework.dataflow.cfg.node.FieldAccessNode;
import org.checkerframework.dataflow.cfg.node.LocalVariableNode;
import org.checkerframework.dataflow.cfg.node.MethodInvocationNode;
import org.checkerframework.dataflow.cfg.node.Node;
import org.checkerframework.dataflow.cfg.node.ObjectCreationNode;
import org.checkerframework.dataflow.cfg.node.ReturnNode;
import org.checkerframework.dataflow.expression.ClassName;
import org.checkerframework.dataflow.expression.FieldAccess;
import org.checkerframework.dataflow.expression.LocalVariable;
import org.checkerframework.dataflow.expression.ThisReference;
import org.checkerframework.framework.flow.CFAbstractStore;
import org.checkerframework.framework.flow.CFAbstractValue;
import org.checkerframework.framework.qual.IgnoreInWholeProgramInference;
import org.checkerframework.framework.qual.TypeUseLocation;
import org.checkerframework.framework.type.AnnotatedTypeFactory;
import org.checkerframework.framework.type.AnnotatedTypeMirror;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedNullType;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable;
import org.checkerframework.framework.type.GenericAnnotatedTypeFactory;
import org.checkerframework.framework.util.AnnotatedTypes;
import org.checkerframework.framework.util.dependenttypes.DependentTypesHelper;
import org.checkerframework.javacutil.BugInCF;
import org.checkerframework.javacutil.ElementUtils;
import org.checkerframework.javacutil.TreePathUtil;
import org.checkerframework.javacutil.TreeUtils;
import org.checkerframework.javacutil.TypesUtils;
/**
* This is the primary implementation of {@link
* org.checkerframework.common.wholeprograminference.WholeProgramInference}. It uses an instance of
* {@link WholeProgramInferenceStorage} to store annotations and to create output files.
*
* <p>This class does not perform inference for an element if the element has explicit annotations.
* That is, calling an {@code update*} method on an explicitly annotated field, method return, or
* method parameter has no effect.
*
* <p>In addition, whole program inference ignores inferred types in a few scenarios. When
* discovering a use, WPI ignores an inferred type if:
*
* <ol>
* <li>The inferred type of an element that should be written into a file is a subtype of the
* upper bounds of this element's written type in the source code.
* <li>The annotation annotates a {@code null} literal, except when doing inference for the
* NullnessChecker. (The rationale for this is that {@code null} is a frequently-used default
* value, and it would be undesirable to infer the bottom type if {@code null} were the only
* value passed as an argument.)
* </ol>
*
* When outputting a file, WPI ignores an inferred type if:
*
* <ol>
* <li>The @Target annotation does not permit the annotation to be written at this location.
* <li>The @RelevantJavaTypes annotation does not permit the annotation to be written at this
* location.
* <li>The inferred annotation has the @InvisibleQualifier meta-annotation.
* <li>The inferred annotation would be the same annotation applied via defaulting — that
* is, if omitting it has the same effect as writing it.
* </ol>
*
* @param <T> the type used by the storage to store annotations. See {@link
* WholeProgramInferenceStorage}
*/
// TODO: We could add an option to update the type of explicitly annotated elements, but this
// currently is not recommended since the insert-annotations-to-source tool, which adds annotations
// from .jaif files into source code, adds annotations on top of existing annotations. See
// https://github.com/typetools/annotation-tools/issues/105 .
// TODO: Ensure that annotations are inserted deterministically into files. This is important for
// debugging and comparison; otherwise running the whole-program inference on the same set of files
// can yield different results (order of annotations).
public class WholeProgramInferenceImplementation<T> implements WholeProgramInference {
/** The type factory associated with this. */
protected final AnnotatedTypeFactory atypeFactory;
/**
* Whether to print debugging information when an inference is attempted, but cannot be completed.
* An inference can be attempted without success for example because the current storage system
* does not support placing annotation in the location for which an annotation was inferred.
*/
private final boolean showWpiFailedInferences;
/** The storage for the inferred annotations. */
private WholeProgramInferenceStorage<T> storage;
/** Whether to ignore assignments where the rhs is null. */
private final boolean ignoreNullAssignments;
/**
* Constructs a new {@code WholeProgramInferenceImplementation} that has not yet inferred any
* annotations.
*
* @param atypeFactory the associated type factory
* @param storage the storage used for inferred annotations and for writing output files
* @param showWpiFailedInferences whether the {@code -AshowWpiFailedInferences} argument was
* passed to the checker, and therefore whether to print debugging messages when inference
* fails
*/
public WholeProgramInferenceImplementation(
AnnotatedTypeFactory atypeFactory,
WholeProgramInferenceStorage<T> storage,
boolean showWpiFailedInferences) {
this.atypeFactory = atypeFactory;
this.storage = storage;
boolean isNullness =
atypeFactory.getClass().getSimpleName().equals("NullnessAnnotatedTypeFactory");
this.ignoreNullAssignments = !isNullness;
this.showWpiFailedInferences = showWpiFailedInferences;
}
/**
* Returns the storage for inferred annotations.
*
* @return the storage for the inferred annotations
*/
public WholeProgramInferenceStorage<T> getStorage() {
return storage;
}
@Override
public void updateFromObjectCreation(
ObjectCreationNode objectCreationNode,
ExecutableElement constructorElt,
CFAbstractStore<?, ?> store) {
// Don't infer types for code that isn't presented as source.
if (!ElementUtils.isElementFromSourceCode(constructorElt)) {
return;
}
// Don't infer types for code that can't be annotated anyway.
if (!storage.hasStorageLocationForMethod(constructorElt)) {
if (showWpiFailedInferences) {
printFailedInferenceDebugMessage(
"WPI could not store information"
+ "about this constructor: "
+ JVMNames.getJVMMethodSignature(constructorElt));
}
return;
}
List<Node> arguments = objectCreationNode.getArguments();
updateInferredExecutableParameterTypes(constructorElt, arguments, objectCreationNode.getTree());
updateContracts(Analysis.BeforeOrAfter.BEFORE, constructorElt, store);
}
@Override
public void updateFromMethodInvocation(
MethodInvocationNode methodInvNode,
ExecutableElement methodElt,
CFAbstractStore<?, ?> store) {
// Don't infer types for code that isn't presented as source.
if (!ElementUtils.isElementFromSourceCode(methodElt)) {
return;
}
if (!storage.hasStorageLocationForMethod(methodElt)) {
return;
}
// Don't infer formal parameter types from recursive calls.
//
// When performing WPI on a library, if there are no external calls (only recursive calls), then
// each iteration of WPI would make the formal parameter types more restrictive, leading to an
// infinite (or very long) loop.
//
// Consider
// void myMethod(int x) { ... myMethod(x-1) ... }`
// On one iteration, if x has type IntRange(to=100), the recursive call's argument has type
// IntRange(to=99). If that is the only call to `MyMethod`, then the formal parameter type
// would be updated. On the next iteration it would be refined again to @IntRange(to=98), and
// so forth. A recursive call should never restrict a formal parameter type.
if (isRecursiveCall(methodInvNode)) {
return;
}
List<Node> arguments = methodInvNode.getArguments();
updateInferredExecutableParameterTypes(methodElt, arguments, methodInvNode.getTree());
updateContracts(Analysis.BeforeOrAfter.BEFORE, methodElt, store);
}
/**
* Returns true if the given call is a recursive call.
*
* @param methodInvNode a method invocation
* @return true if the given call is a recursive call
*/
private boolean isRecursiveCall(MethodInvocationNode methodInvNode) {
MethodTree enclosingMethod = TreePathUtil.enclosingMethod(methodInvNode.getTreePath());
if (enclosingMethod == null) {
return false;
}
ExecutableElement methodInvocEle = TreeUtils.elementFromUse(methodInvNode.getTree());
ExecutableElement methodDeclEle = TreeUtils.elementFromDeclaration(enclosingMethod);
return methodDeclEle.equals(methodInvocEle);
}
/**
* Updates inferred parameter types based on a call to a method or constructor.
*
* @param methodElt the element of the method or constructor being invoked
* @param arguments the arguments of the invocation
* @param invocationTree the method or constructor invocation, used to viewpoint adapt any
* dependent types when storing newly-inferred annotations
*/
private void updateInferredExecutableParameterTypes(
ExecutableElement methodElt, List<Node> arguments, Tree invocationTree) {
// TODO: this method should be updated to:
// 1. take the receiver parameter of the method being invoked as an argument, in node form,
// if there is one (the argument should be null otherwise)
// 2. infer types for the method declaration based on the type of the receiver
// 3. DependentTypesHelper#delocalizeAtCallsite should be updated to handle dependent types
// that refer to the receiver (there is a (commented-out) test for this in
// tests/ainfer-index/non-annotated/DependentTypesViewpointAdapationTest.java).
String file = storage.getFileForElement(methodElt);
for (int i = 0; i < arguments.size(); i++) {
Node arg = arguments.get(i);
Tree argTree = arg.getTree();
VariableElement ve;
boolean varargsParam = i >= methodElt.getParameters().size() - 1 && methodElt.isVarArgs();
if (varargsParam && this.atypeFactory.wpiOutputFormat == OutputFormat.JAIF) {
// The AFU's org.checkerframework.afu.annotator.Main produces a non-compilable source file
// when JAIF-based WPI tries to output an annotated varargs parameter, such as when running
// the test checker/tests/ainfer-testchecker/non-annotated/AnonymousAndInnerClass.java.
// Until that bug is fixed, do not attempt to infer information about varargs parameters in
// JAIF mode.
if (showWpiFailedInferences) {
printFailedInferenceDebugMessage(
"Annotations cannot be placed on varargs parameters in -Ainfer=jaifs mode, because"
+ " the JAIF format does not correctly support it.\n"
+ "The signature of the method whose varargs parameter was not annotated is: "
+ JVMNames.getJVMMethodSignature(methodElt));
}
return;
}
if (varargsParam) {
ve = methodElt.getParameters().get(methodElt.getParameters().size() - 1);
} else {
ve = methodElt.getParameters().get(i);
}
AnnotatedTypeMirror paramATM = atypeFactory.getAnnotatedType(ve);
AnnotatedTypeMirror argATM = atypeFactory.getAnnotatedType(argTree);
if (varargsParam) {
// Check whether argATM needs to be turned into an array type, so that the type structure
// matches paramATM.
boolean expandArgATM = false;
if (argATM.getKind() == TypeKind.ARRAY) {
int argATMDepth = AnnotatedTypes.getArrayDepth((AnnotatedArrayType) argATM);
// This unchecked cast is safe because the declared type of a varargs parameter
// is guaranteed to be an array of some kind.
int paramATMDepth = AnnotatedTypes.getArrayDepth((AnnotatedArrayType) paramATM);
if (paramATMDepth != argATMDepth) {
assert argATMDepth + 1 == paramATMDepth;
expandArgATM = true;
}
} else {
expandArgATM = true;
}
if (expandArgATM) {
if (argATM.getKind() == TypeKind.WILDCARD) {
if (showWpiFailedInferences) {
printFailedInferenceDebugMessage(
"Javac cannot create an array type "
+ "from a wildcard, so WPI did not attempt to infer a type for an array "
+ "parameter.\n"
+ "The signature of the method whose parameter had inference skipped is: "
+ JVMNames.getJVMMethodSignature(methodElt));
}
return;
}
AnnotatedTypeMirror argArray =
AnnotatedTypeMirror.createType(
TypesUtils.createArrayType(argATM.getUnderlyingType(), atypeFactory.types),
atypeFactory,
false);
((AnnotatedArrayType) argArray).setComponentType(argATM);
argATM = argArray;
}
}
atypeFactory.wpiAdjustForUpdateNonField(argATM);
// If storage.getParameterAnnotations receives an index that's larger than the size
// of the parameter list, scenes-backed inference can create duplicate entries
// for the varargs parameter (it indexes inferred annotations by the parameter number).
int paramIndex = varargsParam ? methodElt.getParameters().size() - 1 : i;
T paramAnnotations =
storage.getParameterAnnotations(methodElt, paramIndex, paramATM, ve, atypeFactory);
if (this.atypeFactory instanceof GenericAnnotatedTypeFactory) {
((GenericAnnotatedTypeFactory) this.atypeFactory)
.getDependentTypesHelper()
.delocalizeAtCallsite(argATM, invocationTree, arguments, methodElt);
}
updateAnnotationSet(paramAnnotations, TypeUseLocation.PARAMETER, argATM, paramATM, file);
}
}
@Override
public void updateContracts(
Analysis.BeforeOrAfter preOrPost, ExecutableElement methodElt, CFAbstractStore<?, ?> store) {
// Don't infer types for code that isn't presented as source.
if (!ElementUtils.isElementFromSourceCode(methodElt)) {
return;
}
if (store == null) {
throw new BugInCF(
"updateContracts(%s, %s, null) for %s",
preOrPost, methodElt, atypeFactory.getClass().getSimpleName());
}
if (!storage.hasStorageLocationForMethod(methodElt)) {
return;
}
// TODO: Probably move some part of this into the AnnotatedTypeFactory.
// This code handles fields of "this" and method parameters (including the receiver parameter
// "this"), for now. In the future, extend it to other expressions.
TypeElement containingClass = (TypeElement) methodElt.getEnclosingElement();
ThisReference thisReference = new ThisReference(containingClass.asType());
ClassName classNameReceiver = new ClassName(containingClass.asType());
// Fields of "this":
for (VariableElement fieldElement :
ElementFilter.fieldsIn(containingClass.getEnclosedElements())) {
if (atypeFactory.wpiOutputFormat == OutputFormat.JAIF
&& containingClass.getNestingKind().isNested()) {
// Don't infer facts about fields of inner classes, because IndexFileWriter
// places the annotations incorrectly on the class declarations.
continue;
}
FieldAccess fa =
new FieldAccess(
(ElementUtils.isStatic(fieldElement) ? classNameReceiver : thisReference),
fieldElement.asType(),
fieldElement);
CFAbstractValue<?> v = store.getFieldValue(fa);
AnnotatedTypeMirror fieldDeclType = atypeFactory.getAnnotatedType(fieldElement);
AnnotatedTypeMirror inferredType;
if (v != null) {
// This field is in the store.
inferredType = convertCFAbstractValueToAnnotatedTypeMirror(v, fieldDeclType);
atypeFactory.wpiAdjustForUpdateNonField(inferredType);
} else {
// This field is not in the store. Use the declared type.
inferredType = fieldDeclType;
}
T preOrPostConditionAnnos =
storage.getPreOrPostconditions(
preOrPost, methodElt, fa.toString(), fieldDeclType, atypeFactory);
if (preOrPostConditionAnnos == null) {
continue;
}
String file = storage.getFileForElement(methodElt);
updateAnnotationSet(
preOrPostConditionAnnos, TypeUseLocation.FIELD, inferredType, fieldDeclType, file, false);
}
// Method parameters (other than the receiver parameter "this"):
// This loop is 1-indexed to match the syntax used in annotation arguments.
for (int index = 1; index <= methodElt.getParameters().size(); index++) {
VariableElement paramElt = methodElt.getParameters().get(index - 1);
// Do not infer information about non-effectively-final method parameters, to avoid
// spurious flowexpr.parameter.not.final warnings.
if (!ElementUtils.isEffectivelyFinal(paramElt)) {
continue;
}
LocalVariable param = new LocalVariable(paramElt);
CFAbstractValue<?> v = store.getValue(param);
AnnotatedTypeMirror declType = atypeFactory.getAnnotatedType(paramElt);
AnnotatedTypeMirror inferredType;
if (v != null) {
// This parameter is in the store.
inferredType = convertCFAbstractValueToAnnotatedTypeMirror(v, declType);
atypeFactory.wpiAdjustForUpdateNonField(inferredType);
} else {
// The parameter is not in the store, so don't attempt to create a postcondition for it,
// since anything other than its default type would not be verifiable. (Only postconditions
// are supported for parameters.)
continue;
}
T preOrPostConditionAnnos =
storage.getPreOrPostconditions(preOrPost, methodElt, "#" + index, declType, atypeFactory);
if (preOrPostConditionAnnos != null) {
String file = storage.getFileForElement(methodElt);
updateAnnotationSet(
preOrPostConditionAnnos,
TypeUseLocation.PARAMETER,
inferredType,
declType,
file,
false);
}
}
// Receiver parameter ("this"):
if (!ElementUtils.isStatic(methodElt)) { // Static methods do not have a receiver.
CFAbstractValue<?> v = store.getValue(thisReference);
if (v != null) {
// This parameter is in the store.
AnnotatedTypeMirror declaredType =
atypeFactory.getAnnotatedType(methodElt).getReceiverType();
if (declaredType == null) {
// declaredType is null when the method being analyzed is a constructor (which doesn't
// have a receiver).
return;
}
AnnotatedTypeMirror inferredType =
AnnotatedTypeMirror.createType(declaredType.getUnderlyingType(), atypeFactory, false);
inferredType.replaceAnnotations(v.getAnnotations());
atypeFactory.wpiAdjustForUpdateNonField(inferredType);
T preOrPostConditionAnnos =
storage.getPreOrPostconditions(
preOrPost, methodElt, "this", declaredType, atypeFactory);
if (preOrPostConditionAnnos != null) {
String file = storage.getFileForElement(methodElt);
updateAnnotationSet(
preOrPostConditionAnnos,
TypeUseLocation.PARAMETER,
inferredType,
declaredType,
file,
false);
}
}
}
}
/**
* Converts a CFAbstractValue to an AnnotatedTypeMirror.
*
* @param v a value to convert to an AnnotatedTypeMirror
* @param fieldType an {@code AnnotatedTypeMirror} with the same underlying type as {@code v} that
* is copied, then the copy is updated to use {@code v}'s annotations
* @return a copy of {@code fieldType} with {@code v}'s annotations
*/
private AnnotatedTypeMirror convertCFAbstractValueToAnnotatedTypeMirror(
CFAbstractValue<?> v, AnnotatedTypeMirror fieldType) {
AnnotatedTypeMirror result = fieldType.deepCopy();
result.replaceAnnotations(v.getAnnotations());
return result;
}
@Override
public void updateFromOverride(
MethodTree methodTree,
ExecutableElement methodElt,
AnnotatedExecutableType overriddenMethod) {
// Don't infer types for code that isn't presented as source.
if (!ElementUtils.isElementFromSourceCode(methodElt)) {
return;
}
String file = storage.getFileForElement(methodElt);
for (int i = 0; i < overriddenMethod.getParameterTypes().size(); i++) {
VariableElement ve = methodElt.getParameters().get(i);
AnnotatedTypeMirror paramATM = atypeFactory.getAnnotatedType(ve);
AnnotatedTypeMirror argATM = overriddenMethod.getParameterTypes().get(i);
atypeFactory.wpiAdjustForUpdateNonField(argATM);
T paramAnnotations =
storage.getParameterAnnotations(methodElt, i, paramATM, ve, atypeFactory);
updateAnnotationSet(paramAnnotations, TypeUseLocation.PARAMETER, argATM, paramATM, file);
}
AnnotatedDeclaredType argADT = overriddenMethod.getReceiverType();
if (argADT != null) {
AnnotatedTypeMirror paramATM = atypeFactory.getAnnotatedType(methodTree).getReceiverType();
if (paramATM != null) {
T receiver = storage.getReceiverAnnotations(methodElt, paramATM, atypeFactory);
updateAnnotationSet(receiver, TypeUseLocation.RECEIVER, argADT, paramATM, file);
}
}
}
@Override
public void updateFromFormalParameterAssignment(
LocalVariableNode lhs, Node rhs, VariableElement paramElt) {
// Don't infer types for code that isn't presented as source.
if (!ElementUtils.isElementFromSourceCode(lhs.getElement())) {
return;
}
Tree rhsTree = rhs.getTree();
if (rhsTree == null) {
// TODO: Handle variable-length list as parameter.
// An ArrayCreationNode with a null tree is created when the
// parameter is a variable-length list. We are ignoring it for now.
// See Issue 682: https://github.com/typetools/checker-framework/issues/682
if (showWpiFailedInferences) {
printFailedInferenceDebugMessage(
"Could not update from formal parameter "
+ "assignment, because an ArrayCreationNode with a null tree is created when "
+ "the parameter is a variable-length list.\nParameter: "
+ paramElt);
}
return;
}
ExecutableElement methodElt = (ExecutableElement) paramElt.getEnclosingElement();
int i = methodElt.getParameters().indexOf(paramElt);
if (i == -1) {
// When paramElt is the parameter of a lambda contained in another
// method body, the enclosing element is the outer method body
// rather than the lambda itself (which has no element). WPI
// does not support inferring types for lambda parameters, so
// ignore it.
if (showWpiFailedInferences) {
printFailedInferenceDebugMessage(
"Could not update from formal "
+ "parameter assignment inside a lambda expression, because lambda parameters "
+ "cannot be annotated.\nParameter: "
+ paramElt);
}
return;
}
AnnotatedTypeMirror paramATM = atypeFactory.getAnnotatedType(paramElt);
AnnotatedTypeMirror argATM = atypeFactory.getAnnotatedType(rhsTree);
atypeFactory.wpiAdjustForUpdateNonField(argATM);
T paramAnnotations =
storage.getParameterAnnotations(methodElt, i, paramATM, paramElt, atypeFactory);
String file = storage.getFileForElement(methodElt);
updateAnnotationSet(paramAnnotations, TypeUseLocation.PARAMETER, argATM, paramATM, file);
}
@Override
public void updateFromFieldAssignment(Node lhs, Node rhs) {
Element element;
String fieldName;
if (lhs instanceof FieldAccessNode) {
element = ((FieldAccessNode) lhs).getElement();
fieldName = ((FieldAccessNode) lhs).getFieldName();
} else if (lhs instanceof LocalVariableNode) {
element = ((LocalVariableNode) lhs).getElement();
fieldName = ((LocalVariableNode) lhs).getName();
} else {
throw new BugInCF(
"updateFromFieldAssignment received an unexpected node type: " + lhs.getClass());
}
// TODO: For a primitive such as long, this is yielding just @GuardedBy rather than
// @GuardedBy({}).
AnnotatedTypeMirror rhsATM = atypeFactory.getAnnotatedType(rhs.getTree());
atypeFactory.wpiAdjustForUpdateField(lhs.getTree(), element, fieldName, rhsATM);
updateFieldFromType(lhs.getTree(), element, fieldName, rhsATM);
}
@Override
public void updateFieldFromType(
Tree lhsTree, Element element, String fieldName, AnnotatedTypeMirror rhsATM) {
if (ignoreFieldInWPI(element, fieldName)) {
return;
}
// Don't infer types for code that isn't presented as source.
if (!ElementUtils.isElementFromSourceCode(element)) {
return;
}
String file = storage.getFileForElement(element);
AnnotatedTypeMirror lhsATM = atypeFactory.getAnnotatedType(lhsTree);
T fieldAnnotations = storage.getFieldAnnotations(element, fieldName, lhsATM, atypeFactory);
if (fieldAnnotations == null) {
return;
}
updateAnnotationSet(fieldAnnotations, TypeUseLocation.FIELD, rhsATM, lhsATM, file);
}
/**
* Returns true if an assignment to the given field should be ignored by WPI.
*
* @param element the field's element
* @param fieldName the field's name
* @return true if an assignment to the given field should be ignored by WPI
*/
protected boolean ignoreFieldInWPI(Element element, String fieldName) {
// Do not attempt to infer types for fields that do not have valid names. For example,
// compiler-generated temporary variables will have invalid names. Recording facts about fields
// with invalid names causes jaif-based WPI to crash when reading the .jaif file, and stub-based
// WPI to generate unparsable stub files. See
// https://github.com/typetools/checker-framework/issues/3442
if (!SourceVersion.isIdentifier(fieldName)) {
return true;
}
// Don't infer types if the inferred field has a declaration annotation with the
// @IgnoreInWholeProgramInference meta-annotation.
if (atypeFactory.getDeclAnnotation(element, IgnoreInWholeProgramInference.class) != null
|| atypeFactory
.getDeclAnnotationWithMetaAnnotation(element, IgnoreInWholeProgramInference.class)
.size()
> 0) {
return true;
}
// Don't infer types for code that isn't presented as source.
if (!ElementUtils.isElementFromSourceCode(element)) {
return true;
}
return false;
}
@Override
public void updateFromReturn(
ReturnNode retNode,
ClassSymbol classSymbol,
MethodTree methodDeclTree,
Map<AnnotatedDeclaredType, ExecutableElement> overriddenMethods) {
// Don't infer types for code that isn't presented as source.
if (methodDeclTree == null
|| !ElementUtils.isElementFromSourceCode(
TreeUtils.elementFromDeclaration(methodDeclTree))) {
return;
}
// Whole-program inference ignores some locations. See Issue 682:
// https://github.com/typetools/checker-framework/issues/682
if (classSymbol == null) { // TODO: Handle anonymous classes.
return;
}
ExecutableElement methodElt = TreeUtils.elementFromDeclaration(methodDeclTree);
String file = storage.getFileForElement(methodElt);
AnnotatedTypeMirror lhsATM = atypeFactory.getAnnotatedType(methodDeclTree).getReturnType();
// Type of the expression returned
AnnotatedTypeMirror rhsATM = atypeFactory.getAnnotatedType(retNode.getTree().getExpression());
atypeFactory.wpiAdjustForUpdateNonField(rhsATM);
DependentTypesHelper dependentTypesHelper =
((GenericAnnotatedTypeFactory) atypeFactory).getDependentTypesHelper();
dependentTypesHelper.delocalize(rhsATM, methodDeclTree);
T returnTypeAnnos = storage.getReturnAnnotations(methodElt, lhsATM, atypeFactory);
updateAnnotationSet(returnTypeAnnos, TypeUseLocation.RETURN, rhsATM, lhsATM, file);
// Now, update return types of overridden methods based on the implementation we just saw.
// This inference is similar to the inference procedure for method parameters: both are
// updated based only on the implementations (in this case) or call-sites (for method
// parameters) that are available to WPI.
//
// An alternative implementation would be to:
// * update only the method (not overridden methods)
// * when finished, propagate the final result to overridden methods
//
for (Map.Entry<AnnotatedDeclaredType, ExecutableElement> pair : overriddenMethods.entrySet()) {
AnnotatedDeclaredType superclassDecl = pair.getKey();
ExecutableElement overriddenMethodElement = pair.getValue();
// Don't infer types for code that isn't presented as source.
if (!ElementUtils.isElementFromSourceCode(overriddenMethodElement)) {
continue;
}
AnnotatedExecutableType overriddenMethod =
AnnotatedTypes.asMemberOf(
atypeFactory.getProcessingEnv().getTypeUtils(),
atypeFactory,
superclassDecl,
overriddenMethodElement);
String superClassFile = storage.getFileForElement(overriddenMethodElement);
AnnotatedTypeMirror overriddenMethodReturnType = overriddenMethod.getReturnType();
T storedOverriddenMethodReturnTypeAnnotations =
storage.getReturnAnnotations(
overriddenMethodElement, overriddenMethodReturnType, atypeFactory);
updateAnnotationSet(
storedOverriddenMethodReturnTypeAnnotations,
TypeUseLocation.RETURN,
rhsATM,
overriddenMethodReturnType,
superClassFile);
}
}
@Override
public void addMethodDeclarationAnnotation(ExecutableElement methodElt, AnnotationMirror anno) {
// Do not infer types for library code, only for type-checked source code.
if (!ElementUtils.isElementFromSourceCode(methodElt)) {
return;
}
String file = storage.getFileForElement(methodElt);
boolean isNewAnnotation = storage.addMethodDeclarationAnnotation(methodElt, anno);
if (isNewAnnotation) {
storage.setFileModified(file);
}
}
@Override
public void addFieldDeclarationAnnotation(VariableElement field, AnnotationMirror anno) {
if (!ElementUtils.isElementFromSourceCode(field)) {
return;
}
String file = storage.getFileForElement(field);
boolean isNewAnnotation = storage.addFieldDeclarationAnnotation(field, anno);
if (isNewAnnotation) {
storage.setFileModified(file);
}
}
/**
* Updates the set of annotations in a location in a program.
*
* <ul>
* <li>If there was no previous annotation for that location, then the updated set will be the
* annotations in rhsATM.
* <li>If there was a previous annotation, the updated set will be the LUB between the previous
* annotation and rhsATM.
* </ul>
*
* <p>Subclasses can customize this behavior.
*
* @param annotationsToUpdate the type whose annotations are modified by this method
* @param defLoc the location where the annotation will be added
* @param rhsATM the RHS of the annotated type on the source code
* @param lhsATM the LHS of the annotated type on the source code
* @param file the annotation file containing the executable; used for marking the scene as
* modified (needing to be written to disk)
*/
protected void updateAnnotationSet(
T annotationsToUpdate,
TypeUseLocation defLoc,
AnnotatedTypeMirror rhsATM,
AnnotatedTypeMirror lhsATM,
String file) {
updateAnnotationSet(annotationsToUpdate, defLoc, rhsATM, lhsATM, file, true);
}
/**
* Updates the set of annotations in a location in a program.
*
* <ul>
* <li>If there was no previous annotation for that location, then the updated set will be the
* annotations in rhsATM.
* <li>If there was a previous annotation, the updated set will be the LUB between the previous
* annotation and rhsATM.
* </ul>
*
* <p>Subclasses can customize this behavior.
*
* @param annotationsToUpdate the type whose annotations are modified by this method
* @param defLoc the location where the annotation will be added
* @param rhsATM the RHS of the annotated type on the source code
* @param lhsATM the LHS of the annotated type on the source code
* @param file annotation file containing the executable; used for marking the scene as modified
* (needing to be written to disk)
* @param ignoreIfAnnotated if true, don't update any type that is explicitly annotated in the
* source code
*/
protected void updateAnnotationSet(
T annotationsToUpdate,
TypeUseLocation defLoc,
AnnotatedTypeMirror rhsATM,
AnnotatedTypeMirror lhsATM,
String file,
boolean ignoreIfAnnotated) {
if (rhsATM instanceof AnnotatedNullType && ignoreNullAssignments) {
return;
}
AnnotatedTypeMirror atmFromStorage =
storage.atmFromStorageLocation(rhsATM.getUnderlyingType(), annotationsToUpdate);
updateAtmWithLub(rhsATM, atmFromStorage);
if (lhsATM instanceof AnnotatedTypeVariable) {
Set<AnnotationMirror> upperAnnos =
((AnnotatedTypeVariable) lhsATM).getUpperBound().getEffectiveAnnotations();
// If the inferred type is a subtype of the upper bounds of the
// current type in the source code, do nothing.
if (upperAnnos.size() == rhsATM.getAnnotations().size()
&& atypeFactory.getQualifierHierarchy().isSubtype(rhsATM.getAnnotations(), upperAnnos)) {
return;
}
}
storage.updateStorageLocationFromAtm(
rhsATM, lhsATM, annotationsToUpdate, defLoc, ignoreIfAnnotated);
storage.setFileModified(file);
}
/**
* Prints a debugging message about a failed inference. Must only be called after {@link
* #showWpiFailedInferences} has been checked, to avoid constructing the debugging message
* eagerly.
*
* @param reason a message describing the reason an inference was unsuccessful, which will be
* displayed to the user
*/
private void printFailedInferenceDebugMessage(String reason) {
assert showWpiFailedInferences;
// TODO: it would be nice if this message also included a line number
// for the file being analyzed, but I don't know how to get that information
// here, given that this message is called from places where only the annotated
// type mirrors for the LHS and RHS of some pseduo-assignment are available.
System.out.println("WPI failed to make an inference: " + reason);
}
/**
* Updates sourceCodeATM to contain the LUB between sourceCodeATM and ajavaATM, ignoring missing
* AnnotationMirrors from ajavaATM -- it considers the LUB between an AnnotationMirror am and a
* missing AnnotationMirror to be am. The results are stored in sourceCodeATM.
*
* @param sourceCodeATM the annotated type on the source code; side effected by this method
* @param ajavaATM the annotated type on the ajava file
*/
private void updateAtmWithLub(AnnotatedTypeMirror sourceCodeATM, AnnotatedTypeMirror ajavaATM) {
if (sourceCodeATM.getKind() != ajavaATM.getKind()) {
// Ignore null types: passing them to asSuper causes a crash, as they cannot be
// substituted for type variables. If sourceCodeATM is a null type, only the primary
// annotation will be considered anyway, so there is no danger of recursing into
// typevar bounds.
if (sourceCodeATM.getKind() != TypeKind.NULL) {
// This can happen e.g. when recursing into the bounds of a type variable:
// the bound on sourceCodeATM might be a declared type (such as T), while
// the ajavaATM might be a typevar (such as S extends T), or vice-versa. In
// that case, use asSuper to make the two ATMs fully-compatible.
sourceCodeATM = AnnotatedTypes.asSuper(this.atypeFactory, sourceCodeATM, ajavaATM);
}
}
switch (sourceCodeATM.getKind()) {
case TYPEVAR:
updateAtmWithLub(
((AnnotatedTypeVariable) sourceCodeATM).getLowerBound(),
((AnnotatedTypeVariable) ajavaATM).getLowerBound());
updateAtmWithLub(
((AnnotatedTypeVariable) sourceCodeATM).getUpperBound(),
((AnnotatedTypeVariable) ajavaATM).getUpperBound());
break;
case WILDCARD:
break;
// throw new BugInCF("This can't happen");
// TODO: This comment is wrong: the wildcard case does get entered.
// Because inferring type arguments is not supported, wildcards won't be encountered.
// updateATMWithLUB(
// atf,
// ((AnnotatedWildcardType) sourceCodeATM).getExtendsBound(),
// ((AnnotatedWildcardType) ajavaATM).getExtendsBound());
// updateATMWithLUB(
// atf,
// ((AnnotatedWildcardType) sourceCodeATM).getSuperBound(),
// ((AnnotatedWildcardType) ajavaATM).getSuperBound());
// break;
case ARRAY:
AnnotatedTypeMirror sourceCodeComponent =
((AnnotatedArrayType) sourceCodeATM).getComponentType();
AnnotatedTypeMirror ajavaComponent = ((AnnotatedArrayType) ajavaATM).getComponentType();
if (sourceCodeComponent.getKind() == ajavaComponent.getKind()) {
updateAtmWithLub(sourceCodeComponent, ajavaComponent);
} else {
if (showWpiFailedInferences) {
printFailedInferenceDebugMessage(
"attempted to update the component type of an array type, but found an unexpected"
+ " difference in type structure.\n"
+ "LHS kind: "
+ sourceCodeComponent.getKind()
+ "\nRHS kind: "
+ ajavaComponent.getKind());
break;
}
}
break;
// case DECLARED:
// Inferring annotations on type arguments is not supported, so no need to recur on generic
// types. If this was ever implemented, this method would need a VisitHistory object to
// prevent infinite recursion on types such as T extends List<T>.
default:
// ATM only has primary annotations
break;
}
// LUB primary annotations
Set<AnnotationMirror> annosToReplace = new HashSet<>(sourceCodeATM.getAnnotations().size());
for (AnnotationMirror amSource : sourceCodeATM.getAnnotations()) {
AnnotationMirror amAjava = ajavaATM.getAnnotationInHierarchy(amSource);
// amAjava only contains annotations from the ajava file, so it might be missing
// an annotation in the hierarchy.
if (amAjava != null) {
amSource = atypeFactory.getQualifierHierarchy().leastUpperBound(amSource, amAjava);
}
annosToReplace.add(amSource);
}
sourceCodeATM.replaceAnnotations(annosToReplace);
}
@Override
public void writeResultsToFile(OutputFormat outputFormat, BaseTypeChecker checker) {
storage.writeResultsToFile(outputFormat, checker);
}
@Override
public void preprocessClassTree(ClassTree classTree) {
storage.preprocessClassTree(classTree);
}
}