Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Generalize improvement of initialization type frames #642

Merged
merged 9 commits into from
Nov 28, 2023
Merged

Generalize improvement of initialization type frames #642

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
30fbb9e
Generalize fix for where receivers of final classes were sometimes no…
flo2702 Nov 27, 2023
1141a3e
Extend test case to also cover eisop-issue-641
flo2702 Nov 27, 2023
80f0b21
Merge branch 'master' of github.com:eisop/checker-framework into issu…
wmdietl Nov 27, 2023
ff1cf8b
Update changelog
wmdietl Nov 27, 2023
59619b8
Update expected output
wmdietl Nov 27, 2023
43161a8
Better name for test classes
flo2702 Nov 27, 2023
7711658
Merge branch 'issue-640' of github.com:flo2702/checker-framework into…
flo2702 Nov 27, 2023
8ba8311
Make initialization explicit
wmdietl Nov 28, 2023
d118db8
Expand tests
wmdietl Nov 28, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
60 changes: 60 additions & 0 deletions .../java/org/checkerframework/checker/initialization/InitializationAnnotatedTypeFactory.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@
import com.sun.source.tree.Tree;
import com.sun.source.tree.VariableTree;
import com.sun.source.util.TreePath;
import com.sun.tools.javac.code.Type;
import com.sun.tools.javac.tree.JCTree;

import org.checkerframework.checker.initialization.qual.HoldsForDefaultValue;
import org.checkerframework.checker.nullness.qual.Nullable;
Expand Down Expand Up @@ -33,6 +35,7 @@

import java.lang.annotation.Annotation;
import java.util.Collection;
import java.util.Collections;
import java.util.List;
import java.util.Set;

Expand Down Expand Up @@ -113,6 +116,63 @@ public InitializationStore getExceptionalExitStore(Tree tree) {
return getFieldAccessFactory().getReturnStatementStores(methodTree);
}

/**
* {@inheritDoc}
*
* <p>This implementaiton also takes the target checker into account.
*
* @see #getUninitializedFields(InitializationStore, CFAbstractStore, TreePath, boolean,
* Collection)
*/
@Override
protected void setSelfTypeInInitializationCode(
Tree tree, AnnotatedTypeMirror.AnnotatedDeclaredType selfType, TreePath path) {
ClassTree enclosingClass = TreePathUtil.enclosingClass(path);
Type classType = ((JCTree) enclosingClass).type;
AnnotationMirror annotation;

// If all fields are initialized-only, and they are all initialized,
// then:
// - if the class is final, this is @Initialized
// - otherwise, this is @UnderInitialization(CurrentClass) as
// there might still be subclasses that need initialization.
if (areAllFieldsInitializedOnly(enclosingClass)) {
GenericAnnotatedTypeFactory<?, ?, ?, ?> targetFactory =
checker.getTypeFactoryOfSubcheckerOrNull(
((InitializationChecker) checker).getTargetCheckerClass());
InitializationStore initStore = getStoreBefore(tree);
CFAbstractStore<?, ?> targetStore = targetFactory.getStoreBefore(tree);
if (initStore != null
&& targetStore != null
&& getUninitializedFields(
initStore, targetStore, path, false, Collections.emptyList())
.isEmpty()) {
if (classType.isFinal()) {
annotation = INITIALIZED;
} else {
annotation = createUnderInitializationAnnotation(classType);
}
} else if (initStore != null
&& getUninitializedFields(initStore, path, false, Collections.emptyList())
.isEmpty()) {
if (classType.isFinal()) {
annotation = INITIALIZED;
} else {
annotation = createUnderInitializationAnnotation(classType);
}
} else {
annotation = null;
}
} else {
annotation = null;
}

if (annotation == null) {
annotation = getUnderInitializationAnnotationOfSuperType(classType);
}
selfType.replaceAnnotation(annotation);
}

/**
* Returns the fields that are not yet initialized in a given store, taking into account the
* target checker.
Expand Down
141 changes: 0 additions & 141 deletions checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,9 +14,6 @@
import com.sun.source.util.TreePath;

import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey;
import org.checkerframework.checker.initialization.qual.Initialized;
import org.checkerframework.checker.initialization.qual.UnderInitialization;
import org.checkerframework.checker.initialization.qual.UnknownInitialization;
import org.checkerframework.checker.nullness.NullnessChecker;
import org.checkerframework.common.basetype.BaseTypeChecker;
import org.checkerframework.common.basetype.BaseTypeVisitor;
Expand All @@ -31,8 +28,6 @@
import org.checkerframework.javacutil.AnnotationUtils;
import org.checkerframework.javacutil.ElementUtils;
import org.checkerframework.javacutil.TreeUtils;
import org.checkerframework.javacutil.TypesUtils;
import org.plumelib.util.ArraysPlume;

import java.lang.annotation.Annotation;
import java.util.ArrayList;
Expand All @@ -45,7 +40,6 @@
import javax.lang.model.element.AnnotationMirror;
import javax.lang.model.element.ExecutableElement;
import javax.lang.model.element.VariableElement;
import javax.lang.model.type.TypeMirror;

/* NO-AFU
import org.checkerframework.common.wholeprograminference.WholeProgramInference;
Expand Down Expand Up @@ -298,141 +292,6 @@ public Void visitMethodInvocation(MethodInvocationTree node, Void p) {
return null;
}

@Override
protected void reportCommonAssignmentError(
AnnotatedTypeMirror varType,
AnnotatedTypeMirror valueType,
Tree valueTree,
@CompilerMessageKey String errorKey,
Object... extraArgs) {
FoundRequired pair = FoundRequired.of(valueType, varType);
String valueTypeString = pair.found;
String varTypeString = pair.required;

// If the stored value of valueTree is wrong, we still do not report an error
// if all necessary fields of valueTree are initialized in the store before the assignment.

InitializationStore initStoreBefore = atypeFactory.getStoreBefore(commonAssignmentTree);

// We can't check if all necessary fields are initialized without a store.
if (initStoreBefore == null) {
super.reportCommonAssignmentError(varType, valueType, valueTree, errorKey, extraArgs);
return;
}

// We only track field initialization for the current receiver.
if (!valueTree.toString().equals("this")) {
super.reportCommonAssignmentError(varType, valueType, valueTree, errorKey, extraArgs);
return;
}

// If the required type is @Initialized and the value type is not final,
// we always need to report an error.
if (varType.getAnnotation(Initialized.class) != null
&& !ElementUtils.isFinal(
TypesUtils.getTypeElement(valueType.getUnderlyingType()))) {
super.reportCommonAssignmentError(varType, valueType, valueTree, errorKey, extraArgs);
return;
}

// Otherwise, we check if there are any uninitialized fields and only report the error
// if this is the case.
GenericAnnotatedTypeFactory<?, ?, ?, ?> targetFactory =
checker.getTypeFactoryOfSubcheckerOrNull(
((InitializationChecker) checker).getTargetCheckerClass());
List<VariableTree> uninitializedFields =
atypeFactory.getUninitializedFields(
initStoreBefore,
targetFactory.getStoreBefore(commonAssignmentTree),
getCurrentPath(),
false,
Collections.emptyList());
uninitializedFields.removeAll(initializedFields);

if (!uninitializedFields.isEmpty()) {
StringJoiner fieldsString = new StringJoiner(", ");
for (VariableTree f : uninitializedFields) {
fieldsString.add(f.getName());
}
checker.reportError(
commonAssignmentTree,
errorKey,
ArraysPlume.concatenate(extraArgs, valueTypeString, varTypeString));
}
}

@Override
protected void reportMethodInvocabilityError(
MethodInvocationTree node, AnnotatedTypeMirror found, AnnotatedTypeMirror expected) {
// We only track field initialization for the current receiver.
if (!TreeUtils.isSelfAccess(node)) {
super.reportMethodInvocabilityError(node, found, expected);
return;
}

AnnotationMirror init = expected.getAnnotation(Initialized.class);
AnnotationMirror unknownInit = expected.getAnnotation(UnknownInitialization.class);
AnnotationMirror underInit = expected.getAnnotation(UnderInitialization.class);

// If the actual receiver type (found) is not a subtype of expected,
// we still do not report an error if all necessary fields are initialized in the store
// before the method call.

// Find the frame for which the receiver must be initialized to discharge this error:
// * If the expected type is @UnknownInitialization(A) or @UnderInitialization(A), the frame
// is A.
// * If the expected type is @Initialized and the receiver type is final, the frame
// is the receiver type.
// * Otherwise, this error cannot be discharged and is reported by the super method.
TypeMirror frame;
if (unknownInit != null) {
frame = atypeFactory.getTypeFrameFromAnnotation(unknownInit);
} else if (underInit != null) {
frame = atypeFactory.getTypeFrameFromAnnotation(underInit);
} else if (init != null
&& ElementUtils.isFinal(TypesUtils.getTypeElement(expected.getUnderlyingType()))) {
frame = expected.getUnderlyingType();
} else {
super.reportMethodInvocabilityError(node, found, expected);
return;
}

TypeMirror underlyingReceiverType = atypeFactory.getReceiverType(node).getUnderlyingType();
if (!atypeFactory
.getProcessingEnv()
.getTypeUtils()
.isSubtype(frame, underlyingReceiverType)) {
super.reportMethodInvocabilityError(node, found, expected);
return;
}

GenericAnnotatedTypeFactory<?, ?, ?, ?> targetFactory =
checker.getTypeFactoryOfSubcheckerOrNull(
((InitializationChecker) checker).getTargetCheckerClass());
List<VariableTree> uninitializedFields =
atypeFactory.getUninitializedFields(
atypeFactory.getStoreBefore(node),
targetFactory.getStoreBefore(node),
getCurrentPath(),
false,
Collections.emptyList());
uninitializedFields.removeAll(initializedFields);

if (!uninitializedFields.isEmpty()) {
// TODO: improve the error message by showing the uninitialized fields
// StringJoiner fieldsString = new StringJoiner(", ");
// for (VariableTree f : uninitializedFields) {
// fieldsString.add(f.getName());
// }
checker.reportError(
node,
"method.invocation.invalid",
TreeUtils.elementFromUse(node),
found.toString(),
expected.toString());
}
}

/**
* Returns the full list of annotations on the receiver.
*
Expand Down
Loading
Loading