Skip to content

Commit

Permalink
Adpat to new CF version
Browse files Browse the repository at this point in the history
  • Loading branch information
Ao-senXiong committed Mar 29, 2024
1 parent f804e02 commit 45dd837
Show file tree
Hide file tree
Showing 21 changed files with 86 additions and 72 deletions.
8 changes: 4 additions & 4 deletions .ci-build-without-test.sh
Original file line number Diff line number Diff line change
Expand Up @@ -24,10 +24,10 @@ export AFU="${AFU:-../annotation-tools/annotation-file-utilities}"
AT=$(dirname "${AFU}")

## Build annotation-tools (Annotation File Utilities)
/tmp/plume-scripts/git-clone-related opprop annotation-tools "${AT}"
if [ ! -d ../annotation-tools ] ; then
ln -s "${AT}" ../annotation-tools
fi
#/tmp/plume-scripts/git-clone-related opprop annotation-tools "${AT}"
#if [ ! -d ../annotation-tools ] ; then
# ln -s "${AT}" ../annotation-tools
#fi

echo "Running: (cd ${AT} && ./.build-without-test.sh)"
(cd "${AT}" && ./.build-without-test.sh)
Expand Down
3 changes: 2 additions & 1 deletion scripts/inference-dev
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,8 @@ 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="${stubparserDir}"/javaparser-core/target/stubparser-3.25.5.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
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
4 changes: 2 additions & 2 deletions src/checkers/inference/InferenceAnnotatedTypeFactory.java
Original file line number Diff line number Diff line change
Expand Up @@ -228,7 +228,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 +352,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
15 changes: 8 additions & 7 deletions src/checkers/inference/InferenceVisitor.java
Original file line number Diff line number Diff line change
Expand Up @@ -489,13 +489,13 @@ protected void checkTypeArguments(Tree toptree,
* @param extraArgs arguments to the error message key, before "found" and "expected" types
*/
@Override
protected void commonAssignmentCheck(
protected boolean commonAssignmentCheck(
Tree varTree,
ExpressionTree valueExp,
@CompilerMessageKey String errorKey,
Object... extraArgs) {
if (!validateTypeOf(varTree)) {
return;
return true;
}

AnnotatedTypeMirror var;
Expand All @@ -516,11 +516,11 @@ protected void commonAssignmentCheck(

assert var != null : "no variable found for tree: " + varTree;

commonAssignmentCheck(var, valueExp, errorKey, extraArgs);
return commonAssignmentCheck(var, valueExp, errorKey, extraArgs);
}

@Override
protected void commonAssignmentCheck(
protected boolean commonAssignmentCheck(
AnnotatedTypeMirror varType,
AnnotatedTypeMirror valueType,
Tree valueTree,
Expand Down Expand Up @@ -583,7 +583,7 @@ protected void commonAssignmentCheck(
mono.getCanonicalName(),
mono.getCanonicalName(),
valueType.toString());
return;
return true;
}
}
}
Expand All @@ -606,6 +606,7 @@ protected void commonAssignmentCheck(
errorKey,
ArraysPlume.concatenate(extraArgs, valueTypeString, varTypeString));
}
return success;
// ####### End Copied Code ########
}

Expand Down Expand Up @@ -805,7 +806,7 @@ protected void checkExceptionParameter(CatchTree node) {

if (exPar.getKind() != TypeKind.UNION) {
if (!atypeFactory.getQualifierHierarchy()
.isSubtype(required, found)) {
.isSubtypeQualifiersOnly(required, found)) {
checker.reportError(node.getParameter(), "exception.parameter.invalid",
found, required);
}
Expand All @@ -814,7 +815,7 @@ protected void checkExceptionParameter(CatchTree node) {
for (AnnotatedTypeMirror alterntive : aut.getAlternatives()) {
AnnotationMirror foundAltern = alterntive
.getAnnotationInHierarchy(required);
if (!atypeFactory.getQualifierHierarchy().isSubtype(
if (!atypeFactory.getQualifierHierarchy().isSubtypeQualifiersOnly(
required, foundAltern)) {
checker.reportError(node.getParameter(), "exception.parameter.invalid", foundAltern,
required);
Expand Down
21 changes: 11 additions & 10 deletions src/checkers/inference/VariableAnnotator.java
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,7 @@
import checkers.inference.util.ASTPathUtil;
import checkers.inference.util.CopyUtil;
import checkers.inference.util.InferenceUtil;
import org.checkerframework.org.plumelib.util.IPair;


/**
Expand Down Expand Up @@ -108,12 +109,12 @@ public class VariableAnnotator extends AnnotatedTypeScanner<Void,Tree> {
* annotation mirror for a tree is calculated (i.e least upper bound for
* binary tree), and the calculated result is cached in the set.
**/
protected final Map<Tree, Pair<Slot, Set<? extends AnnotationMirror>>> treeToVarAnnoPair;
protected final Map<Tree, IPair<Slot, Set<? extends AnnotationMirror>>> treeToVarAnnoPair;

/** Store elements that have already been annotated **/
private final Map<Element, AnnotatedTypeMirror> elementToAtm;

private final Map<Pair<Integer,Integer>, ExistentialVariableSlot> idsToExistentialSlots;
private final Map<IPair<Integer,Integer>, ExistentialVariableSlot> idsToExistentialSlots;

private final AnnotatedTypeFactory realTypeFactory;
private final InferrableChecker realChecker;
Expand Down Expand Up @@ -238,7 +239,7 @@ private SourceVariableSlot createVariable(final Tree tree) {
// }
// }

final Pair<Slot, Set<? extends AnnotationMirror>> varATMPair = Pair
final IPair<Slot, Set<? extends AnnotationMirror>> varATMPair = IPair
.<Slot, Set<? extends AnnotationMirror>> of(varSlot,
new AnnotationMirrorSet());
treeToVarAnnoPair.put(tree, varATMPair);
Expand Down Expand Up @@ -273,7 +274,7 @@ public ConstantSlot createConstant(final AnnotationMirror value, final Tree tree
// }
Set<AnnotationMirror> annotations = new AnnotationMirrorSet();
annotations.add(constantSlot.getValue());
final Pair<Slot, Set<? extends AnnotationMirror>> varATMPair = Pair
final IPair<Slot, Set<? extends AnnotationMirror>> varATMPair = IPair
.<Slot, Set<? extends AnnotationMirror>> of(constantSlot,
annotations);
treeToVarAnnoPair.put(tree, varATMPair);
Expand Down Expand Up @@ -311,7 +312,7 @@ ExistentialVariableSlot getOrCreateExistentialVariable(final AnnotatedTypeMirror
*/
ExistentialVariableSlot getOrCreateExistentialVariable(final Slot potentialVariable,
final Slot alternativeSlot) {
final Pair<Integer, Integer> idPair = Pair.of(potentialVariable.getId(), alternativeSlot.getId());
final IPair<Integer, Integer> idPair = IPair.of(potentialVariable.getId(), alternativeSlot.getId());
ExistentialVariableSlot existentialVariable = idsToExistentialSlots.get(idPair);

if (existentialVariable == null) {
Expand Down Expand Up @@ -436,7 +437,7 @@ private void addExistentialVariable(final AnnotatedTypeVariable typeVar, final T
}

potentialVariable = createVariable(typeTree);
final Pair<Slot, Set<? extends AnnotationMirror>> varATMPair = Pair
final IPair<Slot, Set<? extends AnnotationMirror>> varATMPair = IPair
.<Slot, Set<? extends AnnotationMirror>> of(
potentialVariable, typeVar.getAnnotations());
treeToVarAnnoPair.put(typeTree, varATMPair);
Expand Down Expand Up @@ -517,7 +518,7 @@ private Slot addPrimaryVariable(AnnotatedTypeMirror atm, final Tree tree) {
((SourceVariableSlot) variable).setInsertable(false);
}

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

Expand Down Expand Up @@ -1542,12 +1543,12 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) {
AnnotatedTypeMirror a = inferenceTypeFactory.getAnnotatedType(binaryTree.getLeftOperand());
AnnotatedTypeMirror b = inferenceTypeFactory.getAnnotatedType(binaryTree.getRightOperand());
Set<? extends AnnotationMirror> lubs = inferenceTypeFactory
.getQualifierHierarchy().leastUpperBounds(a.getEffectiveAnnotations(),
b.getEffectiveAnnotations());
.getQualifierHierarchy().leastUpperBoundsShallow(a.getEffectiveAnnotations(), a.getUnderlyingType(),
b.getEffectiveAnnotations(), b.getUnderlyingType());
atm.clearAnnotations();
atm.addAnnotations(lubs);
if (slotManager.getSlot(atm) instanceof VariableSlot) {
final Pair<Slot, Set<? extends AnnotationMirror>> varATMPair = Pair.<Slot, Set<? extends AnnotationMirror>>of(
final IPair<Slot, Set<? extends AnnotationMirror>> varATMPair = IPair.<Slot, Set<? extends AnnotationMirror>>of(
slotManager.getSlot(atm), lubs);
treeToVarAnnoPair.put(binaryTree, varATMPair);
} else {
Expand Down
7 changes: 4 additions & 3 deletions src/checkers/inference/dataflow/InferenceTransfer.java
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@
import checkers.inference.model.Slot;
import checkers.inference.model.VariableSlot;
import checkers.inference.util.InferenceUtil;
import org.checkerframework.org.plumelib.util.IPair;

/**
*
Expand All @@ -58,7 +59,7 @@ public class InferenceTransfer extends CFTransfer {

// Type variables will have two refinement variables (one for each bound). This covers the
// case where the correct, inferred RHS has no primary annotation
private final Map<Tree, Pair<RefinementVariableSlot, RefinementVariableSlot>> createdTypeVarRefinementVariables = new HashMap<>();
private final Map<Tree, IPair<RefinementVariableSlot, RefinementVariableSlot>> createdTypeVarRefinementVariables = new HashMap<>();

private final InferenceAnnotatedTypeFactory typeFactory;

Expand Down Expand Up @@ -320,7 +321,7 @@ private TransferResult<CFValue, CFStore> createTypeVarRefinementVars(Node lhs, T
final RefinementVariableSlot upperBoundRefVar;
final RefinementVariableSlot lowerBoundRefVar;
if (createdTypeVarRefinementVariables.containsKey(assignmentTree)) {
Pair<RefinementVariableSlot, RefinementVariableSlot> ubToLb = createdTypeVarRefinementVariables.get(assignmentTree);
IPair<RefinementVariableSlot, RefinementVariableSlot> ubToLb = createdTypeVarRefinementVariables.get(assignmentTree);
upperBoundRefVar = ubToLb.first;
lowerBoundRefVar = ubToLb.second;

Expand All @@ -337,7 +338,7 @@ private TransferResult<CFValue, CFStore> createTypeVarRefinementVars(Node lhs, T
upperBoundSlot.getRefinedToSlots().add(upperBoundRefVar);
lowerBoundSlot.getRefinedToSlots().add(lowerBoundRefVar);

createdTypeVarRefinementVariables.put(assignmentTree, Pair.of(upperBoundRefVar, lowerBoundRefVar));
createdTypeVarRefinementVariables.put(assignmentTree, IPair.of(upperBoundRefVar, lowerBoundRefVar));
}

upperBoundType.replaceAnnotation(slotManager.getAnnotation(upperBoundRefVar));
Expand Down
2 changes: 1 addition & 1 deletion src/checkers/inference/dataflow/InferenceValue.java
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ public CFValue leastUpperBound(CFValue other) {

// Delegate the LUB computation to inferenceQualifierHierarchy, by passing
// the two VarAnnos getting from slotManager.
final AnnotationMirror lub = qualifierHierarchy.leastUpperBound(anno1, anno2);
final AnnotationMirror lub = qualifierHierarchy.leastUpperBoundQualifiersOnly(anno1, anno2);

return analysis.createAbstractValue(AnnotationMirrorSet.singleton(lub), getLubType(other, null));
}
Expand Down
Loading

0 comments on commit 45dd837

Please sign in to comment.