Skip to content

Commit

Permalink
Update to EISOP 3.32-eisop1 from 3.28-eisop1 (#435)
Browse files Browse the repository at this point in the history
  • Loading branch information
Ao-senXiong authored Feb 1, 2024
1 parent 695b92c commit bcb8e11
Show file tree
Hide file tree
Showing 13 changed files with 64 additions and 31 deletions.
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.24.7.jar:"${afuDir}"/annotation-file-utilities-all.jar
CFDepJars="${stubparserDir}"/javaparser-core/target/stubparser-3.25.1.jar:"${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: 2 additions & 1 deletion src/checkers/inference/DefaultSlotManager.java
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@
import org.checkerframework.framework.type.AnnotatedTypeFactory;
import org.checkerframework.framework.type.AnnotatedTypeMirror;
import org.checkerframework.javacutil.AnnotationBuilder;
import org.checkerframework.javacutil.AnnotationMirrorMap;
import org.checkerframework.javacutil.AnnotationUtils;
import org.checkerframework.javacutil.BugInCF;
import org.checkerframework.javacutil.TreeUtils;
Expand Down Expand Up @@ -164,7 +165,7 @@ public DefaultSlotManager( final ProcessingEnvironment processingEnvironment,
this.varAnnot = builder.build();

// Construct empty caches
constantCache = AnnotationUtils.createAnnotationMap();
constantCache = new AnnotationMirrorMap<>();
locationCache = new LinkedHashMap<>();
existentialSlotPairCache = new LinkedHashMap<>();
combSlotPairCache = new LinkedHashMap<>();
Expand Down
37 changes: 30 additions & 7 deletions src/checkers/inference/InferenceAnnotatedTypeFactory.java
Original file line number Diff line number Diff line change
Expand Up @@ -24,10 +24,10 @@
import org.checkerframework.framework.type.typeannotator.TypeAnnotator;
import org.checkerframework.framework.type.visitor.AnnotatedTypeScanner;
import org.checkerframework.framework.util.AnnotatedTypes;
import org.checkerframework.framework.util.AnnotationMirrorSet;
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;
Expand Down Expand Up @@ -342,8 +342,19 @@ public ParameterizedExecutableType methodFromUse(final MethodInvocationTree meth
viewpointAdapter.viewpointAdaptMethod(receiverType, methodElem, methodOfReceiver);
}
ParameterizedExecutableType mType = substituteTypeArgs(methodInvocationTree, methodElem, methodOfReceiver);

AnnotatedExecutableType method = mType.executableType;

// Take adapt parameter logic from AnnotatedTypeFactory#methodFromUse to
// InferenceAnnotatedTypeFactory#methodFromUse.
// Store varargType before calling setParameterTypes, otherwise we may lose the varargType
// as it is the last element of the original parameterTypes.
method.computeVarargType();
// Adapt parameters, which makes parameters and arguments be the same size for later
// checking.
List<AnnotatedTypeMirror> parameters =
AnnotatedTypes.adaptParameters(this, method, methodInvocationTree.getArguments());
method.setParameterTypes(parameters);

inferencePoly.replacePolys(methodInvocationTree, method);

if (methodInvocationTree.getKind() == Tree.Kind.METHOD_INVOCATION &&
Expand Down Expand Up @@ -383,7 +394,19 @@ public ParameterizedExecutableType constructorFromUse(final NewClassTree newClas
addComputedTypeAnnotations(newClassTree, constructorReturnType);

final AnnotatedExecutableType constructorType = AnnotatedTypes.asMemberOf(types, this, constructorReturnType, constructorElem);

// Take adapt parameter logic from AnnotatedTypeFactory#constructorFromUse to
// InferenceAnnotatedTypeFactory#constructorFromUse.
// Store varargType before calling setParameterTypes, otherwise we may lose the
// varargType as it is the last element of the original parameterTypes.
// AnnotatedTypes.asMemberOf handles vararg type properly, so we do not need to compute
// vararg type again.
constructorType.computeVarargType();
// Adapt parameters, which makes parameters and arguments be the same size for later
// checking. The vararg type of con has been already computed and stored when calling
// typeVarSubstitutor.substitute.
List<AnnotatedTypeMirror> parameters =
AnnotatedTypes.adaptParameters(this, constructorType, newClassTree.getArguments());
constructorType.setParameterTypes(parameters);
if (viewpointAdapter != null) {
viewpointAdapter.viewpointAdaptConstructor(constructorReturnType, constructorElem, constructorType);
}
Expand Down Expand Up @@ -570,11 +593,11 @@ protected InferenceViewpointAdapter createViewpointAdapter() {
* @return the singleton set with the {@link VarAnnot} on the class bound
*/
@Override
public Set<AnnotationMirror> getTypeDeclarationBounds(TypeMirror type) {
public AnnotationMirrorSet getTypeDeclarationBounds(TypeMirror type) {
final TypeElement elt = (TypeElement) getProcessingEnv().getTypeUtils().asElement(type);
AnnotationMirror vAnno = variableAnnotator.getClassDeclVarAnnot(elt);
if (vAnno != null) {
return Collections.singleton(vAnno);
return AnnotationMirrorSet.singleton(vAnno);
}

// This is to handle the special case of anonymous classes when the super class (or interface)
Expand All @@ -587,11 +610,11 @@ public Set<AnnotationMirror> getTypeDeclarationBounds(TypeMirror type) {
if (realAnno != null) {
Slot slot = slotManager.getSlot(realAnno);
vAnno = slotManager.getAnnotation(slot);
return Collections.singleton(vAnno);
return AnnotationMirrorSet.singleton(vAnno);
}

// If the declaration bound of the underlying type is not cached, use default
return (Set<AnnotationMirror>) getDefaultTypeDeclarationBounds();
return (AnnotationMirrorSet) getDefaultTypeDeclarationBounds();
}

/**
Expand Down
4 changes: 2 additions & 2 deletions src/checkers/inference/InferenceQualifierHierarchy.java
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,10 @@
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.framework.type.ElementQualifierHierarchy;
import org.checkerframework.framework.type.QualifierHierarchy;
import org.checkerframework.framework.util.AnnotationMirrorSet;
import org.checkerframework.framework.util.DefaultQualifierKindHierarchy;
import org.checkerframework.framework.util.QualifierKind;
import org.checkerframework.framework.util.QualifierKindHierarchy;
import org.checkerframework.javacutil.AnnotationMirrorSet;
import org.checkerframework.javacutil.AnnotationUtils;
import org.checkerframework.javacutil.BugInCF;
import org.plumelib.util.StringsPlume;
Expand Down Expand Up @@ -196,7 +196,7 @@ public Set<? extends AnnotationMirror> leastUpperBounds(
Collection<? extends AnnotationMirror> annos1,
Collection<? extends AnnotationMirror> annos2) {
if (InferenceMain.isHackMode(annos1.size() != annos2.size())) {
Set<AnnotationMirror> result = AnnotationUtils.createAnnotationSet();
Set<AnnotationMirror> result = new AnnotationMirrorSet();
for (AnnotationMirror a1 : annos1) {
for (AnnotationMirror a2 : annos2) {
AnnotationMirror lub = leastUpperBound(a1, a2);
Expand Down
7 changes: 4 additions & 3 deletions src/checkers/inference/VariableAnnotator.java
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedWildcardType;
import org.checkerframework.framework.type.visitor.AnnotatedTypeScanner;
import org.checkerframework.javacutil.AnnotationBuilder;
import org.checkerframework.javacutil.AnnotationMirrorSet;
import org.checkerframework.javacutil.AnnotationUtils;
import org.checkerframework.javacutil.ElementUtils;
import org.checkerframework.javacutil.BugInCF;
Expand Down Expand Up @@ -239,7 +240,7 @@ private SourceVariableSlot createVariable(final Tree tree) {

final Pair<Slot, Set<? extends AnnotationMirror>> varATMPair = Pair
.<Slot, Set<? extends AnnotationMirror>> of(varSlot,
AnnotationUtils.createAnnotationSet());
new AnnotationMirrorSet());
treeToVarAnnoPair.put(tree, varATMPair);
logger.fine("Created variable for tree:\n" + varSlot.getId() + " => " + tree);
return varSlot;
Expand Down Expand Up @@ -270,7 +271,7 @@ public ConstantSlot createConstant(final AnnotationMirror value, final Tree tree
//
// }
// }
Set<AnnotationMirror> annotations = AnnotationUtils.createAnnotationSet();
Set<AnnotationMirror> annotations = new AnnotationMirrorSet();
annotations.add(constantSlot.getValue());
final Pair<Slot, Set<? extends AnnotationMirror>> varATMPair = Pair
.<Slot, Set<? extends AnnotationMirror>> of(constantSlot,
Expand Down Expand Up @@ -518,7 +519,7 @@ private Slot addPrimaryVariable(AnnotatedTypeMirror atm, final Tree tree) {

final Pair<Slot, Set<? extends AnnotationMirror>> varATMPair = Pair
.of(variable,
AnnotationUtils.createAnnotationSet());
new AnnotationMirrorSet());

treeToVarAnnoPair.put(tree, varATMPair);
}
Expand Down
3 changes: 2 additions & 1 deletion src/checkers/inference/dataflow/InferenceAnalysis.java
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@
import org.checkerframework.framework.flow.CFTransfer;
import org.checkerframework.framework.flow.CFValue;
import org.checkerframework.framework.type.GenericAnnotatedTypeFactory;
import org.checkerframework.javacutil.AnnotationMirrorSet;
import org.checkerframework.javacutil.BugInCF;
import org.checkerframework.javacutil.Pair;

Expand Down Expand Up @@ -71,7 +72,7 @@ public InferenceAnalysis(
*/
@Override
public CFValue defaultCreateAbstractValue(CFAbstractAnalysis<CFValue, ?, ?> analysis,
Set<AnnotationMirror> annos,
AnnotationMirrorSet annos,
TypeMirror underlyingType) {

if (annos.size() == 0 && underlyingType.getKind() != TypeKind.TYPEVAR) {
Expand Down
5 changes: 3 additions & 2 deletions src/checkers/inference/dataflow/InferenceValue.java
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable;
import org.checkerframework.framework.type.QualifierHierarchy;
import org.checkerframework.framework.util.AnnotationFormatter;
import org.checkerframework.javacutil.AnnotationMirrorSet;
import org.checkerframework.javacutil.TypesUtils;

import java.util.Collections;
Expand Down Expand Up @@ -37,7 +38,7 @@
public class InferenceValue extends CFValue {


public InferenceValue(InferenceAnalysis analysis, Set<AnnotationMirror> annotations, TypeMirror underlyingType) {
public InferenceValue(InferenceAnalysis analysis, AnnotationMirrorSet annotations, TypeMirror underlyingType) {
super(analysis, annotations, underlyingType);
}

Expand Down Expand Up @@ -69,7 +70,7 @@ public CFValue leastUpperBound(CFValue other) {
// the two VarAnnos getting from slotManager.
final AnnotationMirror lub = qualifierHierarchy.leastUpperBound(anno1, anno2);

return analysis.createAbstractValue(Collections.singleton(lub), getLubType(other, null));
return analysis.createAbstractValue(AnnotationMirrorSet.singleton(lub), getLubType(other, null));
}

public Slot getEffectiveSlot(final CFValue value) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@
import checkers.inference.solver.backend.AbstractFormatTranslator;
import checkers.inference.solver.backend.encoder.ConstraintEncoderFactory;
import checkers.inference.solver.backend.maxsat.encoder.MaxSATConstraintEncoderFactory;
import org.checkerframework.javacutil.AnnotationMirrorMap;
import org.checkerframework.javacutil.AnnotationUtils;
import org.sat4j.core.VecInt;

Expand Down Expand Up @@ -41,7 +42,7 @@ public class MaxSatFormatTranslator extends AbstractFormatTranslator<VecInt[], V
public MaxSatFormatTranslator(Lattice lattice) {
super(lattice);
// Initialize mappings between type and int.
Map<AnnotationMirror, Integer>typeToIntRes = AnnotationUtils.createAnnotationMap();
Map<AnnotationMirror, Integer>typeToIntRes = new AnnotationMirrorMap<>();
Map<Integer, AnnotationMirror> intToTypeRes = new HashMap<Integer, AnnotationMirror>();

int curInt = 0;
Expand Down
18 changes: 10 additions & 8 deletions src/checkers/inference/solver/frontend/LatticeBuilder.java
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@
import checkers.inference.InferenceMain;
import org.checkerframework.framework.type.QualifierHierarchy;
import org.checkerframework.javacutil.AnnotationBuilder;
import org.checkerframework.javacutil.AnnotationMirrorMap;
import org.checkerframework.javacutil.AnnotationMirrorSet;
import org.checkerframework.javacutil.AnnotationUtils;

import checkers.inference.model.ConstantSlot;
Expand Down Expand Up @@ -66,10 +68,10 @@ public class LatticeBuilder {
public final Collection<AnnotationMirror> allAnnotations;

public LatticeBuilder() {
subType = AnnotationUtils .createAnnotationMap();
superType = AnnotationUtils.createAnnotationMap();
incomparableType = AnnotationUtils.createAnnotationMap();
allAnnotations = AnnotationUtils.createAnnotationSet();
subType = new AnnotationMirrorMap<>();
superType = new AnnotationMirrorMap<>();
incomparableType = new AnnotationMirrorMap<>();
allAnnotations = new AnnotationMirrorSet();

}

Expand All @@ -82,7 +84,7 @@ public LatticeBuilder() {
public Lattice buildLattice(QualifierHierarchy qualHierarchy, Collection<Slot> slots) {
clear();

Set<AnnotationMirror> supportedAnnos = AnnotationUtils.createAnnotationSet();
Set<AnnotationMirror> supportedAnnos = new AnnotationMirrorSet();
Set<Class<? extends Annotation>> annoClasses =
InferenceMain.getInstance().getRealTypeFactory().getSupportedTypeQualifiers();
for (Class<? extends Annotation> ac: annoClasses) {
Expand Down Expand Up @@ -145,7 +147,7 @@ public Lattice buildLattice(QualifierHierarchy qualHierarchy, Collection<Slot> s
*/
public TwoQualifiersLattice buildTwoTypeLattice(AnnotationMirror top, AnnotationMirror bottom) {
clear();
Set<AnnotationMirror> tempSet = AnnotationUtils.createAnnotationSet();
Set<AnnotationMirror> tempSet = new AnnotationMirrorSet();
tempSet.add(top);
tempSet.add(bottom);
allTypes = Collections.unmodifiableSet(tempSet);
Expand All @@ -154,8 +156,8 @@ public TwoQualifiersLattice buildTwoTypeLattice(AnnotationMirror top, Annotation
numTypes = 2;

// Calculate subertypes map and supertypes map.
Set<AnnotationMirror> topSet = AnnotationUtils.createAnnotationSet();
Set<AnnotationMirror> bottomSet = AnnotationUtils.createAnnotationSet();
Set<AnnotationMirror> topSet = new AnnotationMirrorSet();
Set<AnnotationMirror> bottomSet = new AnnotationMirrorSet();
topSet.add(top);
bottomSet.add(bottom);
subType.put(top, Collections.unmodifiableSet(allTypes));
Expand Down
4 changes: 2 additions & 2 deletions src/checkers/inference/util/ASTPathUtil.java
Original file line number Diff line number Diff line change
Expand Up @@ -207,10 +207,10 @@ public Void visitWildcard(AnnotatedWildcardType type, ASTRecord current) {
return null;
}

if (!AnnotatedTypes.isExplicitlySuperBounded(type)) {
if (!AnnotatedTypes.hasExplicitSuperBound(type)) {
mapping.put(type.getSuperBound(), current);

if (AnnotatedTypes.isExplicitlyExtendsBounded(type)) {
if (AnnotatedTypes.hasExplicitExtendsBound(type)) {
final ASTRecord toBound = extendParent(current, Kind.EXTENDS_WILDCARD, ASTPath.BOUND, 0);
visit(type.getExtendsBound(), toBound);
} else {
Expand Down
3 changes: 2 additions & 1 deletion src/checkers/inference/util/InferenceUtil.java
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedIntersectionType;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedWildcardType;
import org.checkerframework.javacutil.AnnotationMirrorSet;
import org.checkerframework.javacutil.AnnotationUtils;
import org.checkerframework.javacutil.BugInCF;

Expand Down Expand Up @@ -37,7 +38,7 @@ public class InferenceUtil {
*/
public static Set<AnnotationMirror> clearAnnos(final AnnotatedTypeMirror atm) {

final Set<AnnotationMirror> oldAnnos = AnnotationUtils.createAnnotationSet();
final Set<AnnotationMirror> oldAnnos = new AnnotationMirrorSet();
oldAnnos.addAll(atm.getAnnotations());

atm.clearAnnotations();
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@
import checkers.inference.DefaultInferenceResult;
import com.sun.tools.javac.util.Pair;
import org.checkerframework.javacutil.AnnotationBuilder;
import org.checkerframework.javacutil.AnnotationMirrorSet;
import org.checkerframework.javacutil.AnnotationUtils;

import checkers.inference.InferenceMain;
Expand Down Expand Up @@ -104,7 +105,7 @@ protected InferenceResult mergeInferenceResults(List<Pair<Map<Integer, Annotatio
if (AnnotationUtils.areSameByName(dataflowAnno, DATAFLOW_NAME)) {
Set<AnnotationMirror> datas = dataflowResults.get(id);
if (datas == null) {
datas = AnnotationUtils.createAnnotationSet();
datas = new AnnotationMirrorSet();
dataflowResults.put(id, datas);
}
datas.add(dataflowAnno);
Expand Down
3 changes: 2 additions & 1 deletion src/sparta/checkers/SimpleFlowAnnotatedTypeFactory.java
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@
import org.checkerframework.framework.type.treeannotator.TreeAnnotator;
import org.checkerframework.framework.util.defaults.QualifierDefaults;
import org.checkerframework.javacutil.AnnotationBuilder;
import org.checkerframework.javacutil.AnnotationMirrorSet;
import org.checkerframework.javacutil.AnnotationUtils;
import org.checkerframework.javacutil.ElementUtils;
import org.checkerframework.javacutil.TreeUtils;
Expand Down Expand Up @@ -164,7 +165,7 @@ public Void visitNewClass(NewClassTree node, AnnotatedTypeMirror p) {
}

if (empty) {
defaultedSet = AnnotationUtils.createAnnotationSet();
defaultedSet = new AnnotationMirrorSet();
defaultedSet.add(NOSOURCE);
defaultedSet.add(ANYSINK);
}
Expand Down

0 comments on commit bcb8e11

Please sign in to comment.