Skip to content

Commit

Permalink
Update to EISOP 3.39-eisop1 from 3.34-eisop1 (#439)
Browse files Browse the repository at this point in the history
Co-authored-by: Haifeng Shi <shihaifeng1998@gmail.com>
Co-authored-by: Werner Dietl <wdietl@gmail.com>
  • Loading branch information
3 people authored Apr 7, 2024
1 parent f804e02 commit e740339
Show file tree
Hide file tree
Showing 36 changed files with 268 additions and 135 deletions.
2 changes: 1 addition & 1 deletion build.gradle
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,7 @@ dependencies {
implementation group: 'com.google.errorprone', name: 'javac', version: "$errorproneJavacVersion"

implementation 'org.plumelib:options:1.0.5'
implementation 'org.plumelib:plume-util:1.5.9'
implementation 'org.plumelib:plume-util:1.8.1'

implementation 'com.google.guava:guava:31.1-jre'

Expand Down
2 changes: 1 addition & 1 deletion scripts/inference-dev
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ libDir="$cfiDir"/lib
CFBuild="${cfDir}"/dataflow/"${classes}":"${cfDir}"/javacutil/"${classes}":"${cfDir}"/framework/"${classes}":"${cfDir}"/framework/"${resources}"
CFBuild="${CFBuild}":"${cfDir}"/checker/"${classes}":"${cfDir}"/checker/"${resources}":"${annoToolsDir}"/scene-lib/bin

CFDepJars="${stubparserDir}"/javaparser-core/target/stubparser-3.25.2.jar:"${afuDir}"/annotation-file-utilities-all.jar
CFDepJars="${afuDir}"/annotation-file-utilities-all.jar

# sanity check: ensure each jar in CFDepJars actually exists in the file system
# total number of jars
Expand Down
3 changes: 0 additions & 3 deletions src/checkers/inference/BaseInferrableChecker.java
Original file line number Diff line number Diff line change
Expand Up @@ -6,12 +6,9 @@
import org.checkerframework.framework.flow.CFTransfer;
import org.checkerframework.framework.flow.CFValue;
import org.checkerframework.framework.type.GenericAnnotatedTypeFactory;
import org.checkerframework.javacutil.Pair;
import java.lang.annotation.Annotation;
import java.util.Collections;
import java.util.List;
import java.util.Set;
import javax.lang.model.element.VariableElement;

import checkers.inference.dataflow.InferenceAnalysis;
import checkers.inference.dataflow.InferenceTransfer;
Expand Down
2 changes: 1 addition & 1 deletion src/checkers/inference/ExistentialVariableInserter.java
Original file line number Diff line number Diff line change
Expand Up @@ -159,7 +159,7 @@ public void matchAndReplacePrimary(final AnnotatedTypeMirror typeUse, final Anno
}

@Override
protected String defaultErrorMessage(org.checkerframework.framework.type.AnnotatedTypeMirror type1, org.checkerframework.framework.type.AnnotatedTypeMirror type2, Void aVoid) {
public String defaultErrorMessage(org.checkerframework.framework.type.AnnotatedTypeMirror type1, org.checkerframework.framework.type.AnnotatedTypeMirror type2, Void aVoid) {
return "Input types should have identical structures. Input types are limited to those types" +
"that can appear in a type variable bound:\n"
+ "type1=" + type1 + "\n"
Expand Down
12 changes: 2 additions & 10 deletions src/checkers/inference/InferenceAnnotatedTypeFactory.java
Original file line number Diff line number Diff line change
@@ -1,8 +1,6 @@
package checkers.inference;

import checkers.inference.model.ConstantSlot;
import checkers.inference.model.Slot;
import com.sun.source.util.TreePath;
import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
import org.checkerframework.framework.flow.CFAbstractAnalysis;
import org.checkerframework.framework.flow.CFAnalysis;
Expand All @@ -25,18 +23,14 @@
import org.checkerframework.framework.type.visitor.AnnotatedTypeScanner;
import org.checkerframework.framework.util.AnnotatedTypes;
import org.checkerframework.framework.util.defaults.QualifierDefaults;
import org.checkerframework.framework.util.dependenttypes.DependentTypesHelper;
import org.checkerframework.javacutil.AnnotationBuilder;
import org.checkerframework.javacutil.AnnotationMirrorSet;
import org.checkerframework.javacutil.BugInCF;
import org.checkerframework.javacutil.ElementUtils;
import org.checkerframework.javacutil.Pair;
import org.checkerframework.javacutil.TreeUtils;

import java.lang.annotation.Annotation;
import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
Expand All @@ -49,14 +43,12 @@
import javax.lang.model.element.ExecutableElement;
import javax.lang.model.element.TypeElement;
import javax.lang.model.element.TypeParameterElement;
import javax.lang.model.element.VariableElement;
import javax.lang.model.type.TypeKind;
import javax.lang.model.type.TypeMirror;
import javax.lang.model.type.TypeVariable;

import checkers.inference.dataflow.InferenceAnalysis;
import checkers.inference.model.ConstraintManager;
import checkers.inference.model.Slot;
import checkers.inference.qual.VarAnnot;
import checkers.inference.util.ConstantToVariableAnnotator;
import checkers.inference.util.InferenceUtil;
Expand Down Expand Up @@ -228,7 +220,7 @@ protected TypeHierarchy createTypeHierarchy() {

@Override
protected QualifierHierarchy createQualifierHierarchy() {
return new InferenceQualifierHierarchy(getSupportedTypeQualifiers(), elements);
return new InferenceQualifierHierarchy(getSupportedTypeQualifiers(), elements, realTypeFactory);
}

@Override
Expand Down Expand Up @@ -352,7 +344,7 @@ public ParameterizedExecutableType methodFromUse(final MethodInvocationTree meth
// Adapt parameters, which makes parameters and arguments be the same size for later
// checking.
List<AnnotatedTypeMirror> parameters =
AnnotatedTypes.adaptParameters(this, method, methodInvocationTree.getArguments());
AnnotatedTypes.adaptParameters(this, method, methodInvocationTree.getArguments(), null);
method.setParameterTypes(parameters);

inferencePoly.replacePolys(methodInvocationTree, method);
Expand Down
39 changes: 23 additions & 16 deletions src/checkers/inference/InferenceQualifierHierarchy.java
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
import com.google.common.collect.ImmutableMap;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.framework.type.ElementQualifierHierarchy;
import org.checkerframework.framework.type.GenericAnnotatedTypeFactory;
import org.checkerframework.framework.type.QualifierHierarchy;
import org.checkerframework.framework.util.DefaultQualifierKindHierarchy;
import org.checkerframework.framework.util.QualifierKind;
Expand All @@ -19,6 +20,7 @@
import org.plumelib.util.StringsPlume;

import javax.lang.model.element.AnnotationMirror;
import javax.lang.model.type.TypeMirror;
import javax.lang.model.util.Elements;
import java.lang.annotation.Annotation;
import java.util.Collection;
Expand All @@ -42,9 +44,10 @@ public class InferenceQualifierHierarchy extends ElementQualifierHierarchy {

public InferenceQualifierHierarchy(
Collection<Class<? extends Annotation>> qualifierClasses,
Elements elements
Elements elements,
GenericAnnotatedTypeFactory<?, ?, ?, ?> atypeFactory
) {
super(qualifierClasses, elements);
super(qualifierClasses, elements, atypeFactory);

slotMgr = inferenceMain.getSlotManager();
constraintMgr = inferenceMain.getConstraintManager();
Expand Down Expand Up @@ -137,8 +140,10 @@ public static AnnotationMirror findVarAnnot(final Iterable<? extends AnnotationM
}

@Override
public boolean isSubtype(final Collection<? extends AnnotationMirror> rhsAnnos,
final Collection<? extends AnnotationMirror> lhsAnnos ) {
public boolean isSubtypeShallow(final Collection<? extends AnnotationMirror> rhsAnnos,
TypeMirror subType,
final Collection<? extends AnnotationMirror> lhsAnnos,
TypeMirror superType ) {

final AnnotationMirror rhsVarAnnot = findVarAnnot(rhsAnnos);
final AnnotationMirror lhsVarAnnot = findVarAnnot(lhsAnnos);
Expand All @@ -156,11 +161,11 @@ public boolean isSubtype(final Collection<? extends AnnotationMirror> rhsAnnos,
+ " rhs=" + StringsPlume.join(", ", rhsAnnos) + "\n"
+ " lhs=" + StringsPlume.join(", ", lhsAnnos );

return isSubtype(rhsVarAnnot, lhsVarAnnot);
return isSubtypeQualifiers(rhsVarAnnot, lhsVarAnnot);
}

@Override
public boolean isSubtype(final AnnotationMirror subtype, final AnnotationMirror supertype) {
public boolean isSubtypeQualifiers(final AnnotationMirror subtype, final AnnotationMirror supertype) {

// NOTE: subtype and supertype are nullable because, for example, in BaseTypeVisitor::checkConstructorInvocation,
// findAnnotationInSameHierarchy may return null since @VarAnnot and some constant real qualifier
Expand All @@ -187,31 +192,33 @@ public boolean isSubtype(final AnnotationMirror subtype, final AnnotationMirror
}

@Override
public AnnotationMirror greatestLowerBound(AnnotationMirror a1, AnnotationMirror a2) {
public AnnotationMirror greatestLowerBoundQualifiers(AnnotationMirror a1, AnnotationMirror a2) {
return merge(a1, a2, false);
}

@Override
public Set<? extends AnnotationMirror> leastUpperBounds(
public Set<? extends AnnotationMirror> leastUpperBoundsShallow(
Collection<? extends AnnotationMirror> annos1,
Collection<? extends AnnotationMirror> annos2) {
TypeMirror tm1,
Collection<? extends AnnotationMirror> annos2,
TypeMirror tm2) {
if (InferenceMain.isHackMode(annos1.size() != annos2.size())) {
Set<AnnotationMirror> result = new AnnotationMirrorSet();
for (AnnotationMirror a1 : annos1) {
for (AnnotationMirror a2 : annos2) {
AnnotationMirror lub = leastUpperBound(a1, a2);
AnnotationMirror lub = leastUpperBoundQualifiersOnly(a1, a2);
if (lub != null) {
result.add(lub);
}
}
}
return result;
}
return super.leastUpperBounds(annos1, annos2);
return super.leastUpperBoundsShallow(annos1, tm1, annos2, tm2);
}

@Override
public AnnotationMirror leastUpperBound(final AnnotationMirror a1, final AnnotationMirror a2) {
public AnnotationMirror leastUpperBoundQualifiers(final AnnotationMirror a1, final AnnotationMirror a2) {
return merge(a1, a2, true);
}

Expand Down Expand Up @@ -239,9 +246,9 @@ private AnnotationMirror merge(final AnnotationMirror a1, final AnnotationMirror

if (!isA1VarAnnot && !isA2VarAnnot) {
if (isLub) {
return realQualifierHierarchy.leastUpperBound(a1, a2);
return realQualifierHierarchy.leastUpperBoundQualifiersOnly(a1, a2);
} else {
return realQualifierHierarchy.greatestLowerBound(a1, a2);
return realQualifierHierarchy.greatestLowerBoundQualifiersOnly(a1, a2);
}
} else {
// two annotations are not under the same qualifier hierarchy
Expand All @@ -262,9 +269,9 @@ private AnnotationMirror merge(final AnnotationMirror a1, final AnnotationMirror

AnnotationMirror mergedType;
if (isLub) {
mergedType = realQualifierHierarchy.leastUpperBound(realAnno1, realAnno2);
mergedType = realQualifierHierarchy.leastUpperBoundQualifiersOnly(realAnno1, realAnno2);
} else {
mergedType = realQualifierHierarchy.greatestLowerBound(realAnno1, realAnno2);
mergedType = realQualifierHierarchy.greatestLowerBoundQualifiersOnly(realAnno1, realAnno2);
}

Slot constantSlot = slotMgr.createConstantSlot(mergedType);
Expand Down
2 changes: 1 addition & 1 deletion src/checkers/inference/InferenceTypeHierarchy.java
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ public boolean areEqual(AnnotatedTypeMirror type1, AnnotatedTypeMirror type2) {
public StructuralEqualityComparer createEqualityComparer() {
return new InferenceEqualityComparer(
this.areEqualVisitHistory,
InferenceQualifierHierarchy.findVarAnnot(qualifierHierarchy.getTopAnnotations()));
InferenceQualifierHierarchy.findVarAnnot(qualHierarchy.getTopAnnotations()));
}

private static class InferenceEqualityComparer extends StructuralEqualityComparer {
Expand Down
28 changes: 28 additions & 0 deletions src/checkers/inference/InferenceValidator.java
Original file line number Diff line number Diff line change
@@ -1,9 +1,15 @@
package checkers.inference;


import com.sun.source.tree.Tree;
import org.checkerframework.common.basetype.BaseTypeChecker;
import org.checkerframework.common.basetype.BaseTypeValidator;
import org.checkerframework.framework.qual.TypeUseLocation;
import org.checkerframework.framework.type.AnnotatedTypeFactory;
import org.checkerframework.framework.type.AnnotatedTypeMirror;
import org.checkerframework.javacutil.AnnotationUtils;

import javax.lang.model.element.AnnotationMirror;

/**
* A visitor to validate the types in a tree.
Expand All @@ -29,4 +35,26 @@ public InferenceValidator(BaseTypeChecker checker,
public void setInfer(boolean infer) {
this.infer = infer;
}

@Override
protected void validateWildCardTargetLocation(AnnotatedTypeMirror.AnnotatedWildcardType type, Tree tree) {

InferenceVisitor<?,?> inferVisitor = (InferenceVisitor<?,?>) visitor;
if (inferVisitor.ignoreTargetLocations) {
return;
}

AnnotationMirror[] mirrors = new AnnotationMirror[0];
for (AnnotationMirror am : type.getSuperBound().getAnnotations()) {
inferVisitor.annoIsNoneOf(type, am,
inferVisitor.locationToIllegalQuals.get(TypeUseLocation.LOWER_BOUND).toArray(mirrors),
"type.invalid.annotations.on.location", tree);
}

for (AnnotationMirror am : type.getExtendsBound().getAnnotations()) {
inferVisitor.annoIsNoneOf(type, am,
inferVisitor.locationToIllegalQuals.get(TypeUseLocation.UPPER_BOUND).toArray(mirrors),
"type.invalid.annotations.on.location", tree);
}
}
}
Loading

0 comments on commit e740339

Please sign in to comment.