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.

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

Update to EISOP 3.39-eisop1 from 3.34-eisop1 #439

Merged
merged 17 commits into from
Apr 7, 2024
Merged
Show file tree
Hide file tree
Changes from 12 commits
Commits
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
2 changes: 1 addition & 1 deletion .ci-build-without-test.sh
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ export AFU="${AFU:-../annotation-tools/annotation-file-utilities}"
# Don't use `AT=${AFU}/..` which causes a git failure.
AT=$(dirname "${AFU}")

## Build annotation-tools (Annotation File Utilities)
# Build annotation-tools (Annotation File Utilities)
Ao-senXiong marked this conversation as resolved.
Show resolved Hide resolved
/tmp/plume-scripts/git-clone-related opprop annotation-tools "${AT}"
if [ ! -d ../annotation-tools ] ; then
ln -s "${AT}" ../annotation-tools
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) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In a separate PR, look why this uses the fully-qualified name. The method before uses just ATM.

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
26 changes: 26 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,24 @@ 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;
Ao-senXiong marked this conversation as resolved.
Show resolved Hide resolved

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
Loading