Type argument inference fixes. (#7002)

Co-authored-by: Michael Ernst <mernst@cs.washington.edu> Fixes #6891.

Author: smillst

framework/src/main/java/org/checkerframework/framework/util/typeinference8/InvocationTypeInference.java

@@ -462,9 +462,6 @@ public ConstraintSet createC(
  c.addAll(aa.reduce(context));
  }
  } else {
- // Wait to reduce additional argument constraints from lambdas and method references
- // because the additional constraints might require other inference variables to be
- // resolved before the constraint can be created.
  c.addAll(createAdditionalArgConstraints(ei, fi, map));
  }
  }
@@ -513,7 +510,7 @@ private ConstraintSet createAdditionalArgConstraints(
  case METHOD_INVOCATION:
  case NEW_CLASS:
  if (TreeUtils.isPolyExpression(ei)) {
- c.add(new AdditionalArgument(ei));
+ c.addAll(new AdditionalArgument(ei).reduce(context));
  }
  break;
  case PARENTHESIZED:
@@ -564,7 +561,15 @@ private ConstraintSet createAdditionalArgConstraintsNoLambda(ExpressionTree expr
  case METHOD_INVOCATION:
  case NEW_CLASS:
  if (TreeUtils.isPolyExpression(expression)) {
- c.add(new AdditionalArgument(expression));
+ try {
+ c.addAll(new AdditionalArgument(expression).reduce(context));
+ } catch (Exception e) {
+ // Sometimes in order to create the additional argument constraint, other inference
+ // variables must be resolved first. This happens when a lambda parameter is used in the
+ // additional argument constraint.
+ // See framework/tests/all-systems/SimpleLambdaParameter.java
+ c.add(new AdditionalArgument(expression));
+ }
  }
  break;
  case PARENTHESIZED:
@@ -666,7 +671,7 @@ private BoundSet getB4(BoundSet b3, ConstraintSet c) {
  Set<Variable> newVariables = c.getAllInferenceVariables();
  while (!c.isEmpty()) {
 
- ConstraintSet subset = c.getClosedSubset(b3.getDependencies(newVariables));
+ ConstraintSet subset = ConstraintSet.getClosedSubset(c, b3.getDependencies(newVariables));
  Set<Variable> alphas = subset.getAllInputVariables();
  if (!alphas.isEmpty()) {
  // First resolve only the variables with proper bounds.

framework/src/main/java/org/checkerframework/framework/util/typeinference8/bound/BoundSet.java

@@ -272,10 +272,8 @@ public Dependencies getDependencies(Collection<Variable> additionalVars) {
  Set<Variable> allVariables = new LinkedHashSet<>(variables);
  allVariables.addAll(additionalVars);
  for (Variable alpha : allVariables) {
- LinkedHashSet<Variable> alphaDependencies = new LinkedHashSet<>();
- // An inference variable alpha depends on the resolution of itself.
- alphaDependencies.add(alpha);
- alphaDependencies.addAll(alpha.getBounds().getVariablesMentionedInBounds());
+ LinkedHashSet<Variable> alphaDependencies =
+ new LinkedHashSet<>(alpha.getBounds().getVariablesMentionedInBounds());
 
  if (alpha.isCaptureVariable()) {
  // If alpha appears on the left-hand side of another bound of the form
@@ -292,6 +290,8 @@ public Dependencies getDependencies(Collection<Variable> additionalVars) {
  }
  }
  }
+ // An inference variable alpha depends on the resolution of itself.
+ dependencies.putOrAdd(alpha, alpha);
  }
 
  // Add transitive dependencies

framework/src/main/java/org/checkerframework/framework/util/typeinference8/constraint/CheckedExceptionConstraint.java

@@ -1,14 +1,20 @@
 package org.checkerframework.framework.util.typeinference8.constraint;
 
 import com.sun.source.tree.ExpressionTree;
+import com.sun.source.tree.LambdaExpressionTree;
+import com.sun.source.tree.MemberReferenceTree;
 import com.sun.source.tree.Tree;
 import java.util.ArrayList;
+import java.util.Collections;
 import java.util.List;
 import java.util.Objects;
+import javax.lang.model.type.TypeKind;
 import org.checkerframework.framework.util.typeinference8.types.AbstractType;
+import org.checkerframework.framework.util.typeinference8.types.UseOfVariable;
 import org.checkerframework.framework.util.typeinference8.types.Variable;
 import org.checkerframework.framework.util.typeinference8.util.Java8InferenceContext;
 import org.checkerframework.framework.util.typeinference8.util.Theta;
+import org.checkerframework.javacutil.TreeUtils;
 
 /**
  * <LambdaExpression →throws T>: The checked exceptions thrown by the body of the
@@ -53,6 +59,52 @@ public Kind getKind() {
 
  @Override
  public List<Variable> getInputVariables() {
+ if (getKind() == Kind.LAMBDA_EXCEPTION) {
+ if (T.isUseOfVariable()) {
+ return Collections.singletonList(((UseOfVariable) T).getVariable());
+ } else {
+ LambdaExpressionTree lambdaTree = (LambdaExpressionTree) expression;
+ List<Variable> inputs = new ArrayList<>();
+ if (TreeUtils.isImplicitlyTypedLambda(lambdaTree)) {
+ List<AbstractType> params = this.T.getFunctionTypeParameterTypes();
+ if (params == null) {
+ // T is not a function type.
+ return Collections.emptyList();
+ }
+ for (AbstractType param : params) {
+ inputs.addAll(param.getInferenceVariables());
+ }
+ }
+ AbstractType R = this.T.getFunctionTypeReturnType();
+ if (R == null || R.getTypeKind() == TypeKind.NONE) {
+ return inputs;
+ }
+ inputs.addAll(R.getInferenceVariables());
+ return inputs;
+ }
+ } else if (getKind() == Kind.METHOD_REF_EXCEPTION) {
+ if (T.isUseOfVariable()) {
+ return Collections.singletonList(((UseOfVariable) T).getVariable());
+ } else if (TreeUtils.isExactMethodReference((MemberReferenceTree) expression)) {
+ return Collections.emptyList();
+ } else {
+ List<AbstractType> params = this.T.getFunctionTypeParameterTypes();
+ if (params == null) {
+ // T is not a function type.
+ return Collections.emptyList();
+ }
+ List<Variable> inputs = new ArrayList<>();
+ for (AbstractType param : params) {
+ inputs.addAll(param.getInferenceVariables());
+ }
+ AbstractType R = this.T.getFunctionTypeReturnType();
+ if (R == null || R.getTypeKind() == TypeKind.NONE) {
+ return inputs;
+ }
+ inputs.addAll(R.getInferenceVariables());
+ return inputs;
+ }
+ }
  return getInputVariablesForExpression(expression, getT());
  }
 

framework/src/main/java/org/checkerframework/framework/util/typeinference8/constraint/ConstraintSet.java

@@ -56,7 +56,7 @@ public String toString() {
  /**
  * A list of constraints in this set. It does not contain constraints that are equal. This needs
  * to be kept in the order created, which should be lexically left to right. This is so the {@link
- * #getClosedSubset(Dependencies)} is computed correctly.
+ * #getClosedSubset(ConstraintSet, Dependencies)} is computed correctly.
  */
  private final List<Constraint> list;
 
@@ -139,6 +139,28 @@ public Constraint pop() {
  return list.remove(0);
  }
 
+ /**
+ * Adds the constraint to the beginning of this set.
+ *
+ * @param constraint a constraint
+ */
+ public void push(Constraint constraint) {
+ if (constraint != null && !list.contains(constraint)) {
+ list.add(0, constraint);
+ }
+ }
+
+ /**
+ * Adds the constraints to the beginning of this set and maintains the order of the constraints.
+ *
+ * @param constraints constraints
+ */
+ public void pushAll(ConstraintSet constraints) {
+ for (int i = constraints.list.size() - 1; i > -1; i--) {
+ this.push(constraints.list.get(i));
+ }
+ }
+
  /**
  * Remove all constraints in {@code subset} from this constraint set.
  *
@@ -153,35 +175,61 @@ public void remove(ConstraintSet subset) {
  }
 
  /**
- * A subset of constraints is selected in this constraint set, satisfying the property that, for
- * each constraint, no input variable can influence an output variable of another constraint in
- * this constraint set. (See JLS 18.5.2.2)
+ * Returns a subset of {@code c}; for each constraint in the subset, no input variable can
+ * influence an output variable of another constraint in C. If that subset is empty, returns a set
+ * containing a single constraint that participates in a constraint cycle. (See JLS 18.5.2.2)
  *
+ * @param c a constraint set
  * @param dependencies an object describing the dependencies of inference variables
- * @return s a subset of constraints is this constraint set
+ * @return s a subset of constraints in {@code c} whose inputs do not affect {@code c}'s outputs,
+ * or a singleton constraint from a constraint cycle
  */
- public ConstraintSet getClosedSubset(Dependencies dependencies) {
+ public static ConstraintSet getClosedSubset(ConstraintSet c, Dependencies dependencies) {
  ConstraintSet subset = new ConstraintSet();
- Set<Variable> inputDependencies = new LinkedHashSet<>();
- Set<Variable> outDependencies = new LinkedHashSet<>();
- for (Constraint constraint : list) {
+ // Collection of all outputs of c.
+ Set<Variable> allOutputsOfC = new LinkedHashSet<>();
+ for (Constraint constraint : c.list) {
+ if (constraint instanceof TypeConstraint) {
+ allOutputsOfC.addAll(((TypeConstraint) constraint).getOutputVariables());
+ }
+ // No other constraints have output variables
+ }
+
+ // From JLS 18.5.2.2:
+ // A subset of constraints is selected in C, satisfying the property that, for each
+ // constraint, no input variable can influence an output variable of another
+ // constraint in C. The terms input variable and output variable are defined
+ // below. An inference variable alpha can influence an inference variable beta if alpha
+ // depends on the resolution of beta (§18.4), or vice versa; or if there exists a third
+ // inference variable gamma such that alpha can influence gamma and gamma can influence beta.
+
+ // Put another way:
+ // Find a subset of the set c where the following is true for all the constraints in the subset:
+ // no input variable of a constraint can influence an output variable of any constraint in c.
+ // (Influence means that neither variable can depend on the other.)
+ // The JLS does not specify whether this subset should be as large as possible, but this
+ // implementation returns the largest subset possible.
+ for (Constraint constraint : c.list) {
  if (constraint.getKind() == Kind.EXPRESSION
  || constraint.getKind() == Kind.LAMBDA_EXCEPTION
  || constraint.getKind() == Kind.METHOD_REF_EXCEPTION) {
- TypeConstraint c = (TypeConstraint) constraint;
- Set<Variable> newInputs = dependencies.get(c.getInputVariables());
- Set<Variable> newOutputs = dependencies.get(c.getOutputVariables());
- if (Collections.disjoint(newInputs, outDependencies)
- && Collections.disjoint(newOutputs, inputDependencies)) {
- inputDependencies.addAll(newInputs);
- outDependencies.addAll(newOutputs);
- subset.add(c);
- } else {
- // A cycle (or cycles) in the graph of dependencies between constraints exists.
- subset = new ConstraintSet();
- break;
+ List<Variable> inputsOfSingleConstraint = ((TypeConstraint) constraint).getInputVariables();
+ boolean foundInfluence = false;
+ inputLoop:
+ for (Variable in : inputsOfSingleConstraint) {
+ for (Variable out : allOutputsOfC) {
+ if (dependencies.get(in).contains(out) || dependencies.get(out).contains(in)) {
+ foundInfluence = true;
+ break inputLoop;
+ }
+ }
+ }
+ if (!foundInfluence) {
+ // None of the inputs of constraint influence any output of any constraint in C.
+ subset.add(constraint);
  }
  } else {
+ // Other kinds of constraints do not have input variables.
  subset.add(constraint);
  }
  }
@@ -190,40 +238,47 @@ public ConstraintSet getClosedSubset(Dependencies dependencies) {
  return subset;
  }
 
- outDependencies.clear();
- inputDependencies.clear();
- // If this subset is empty, then there is a cycle (or cycles) in the graph of dependencies
- // between constraints.
+ // TODO: double check that this code is correct.
+ // checker/tests/all-systems/java8inference/MapEntryGetFails.java is a test that uses this code.
+
+ Set<Variable> inputDependencies = new LinkedHashSet<>();
+ Set<Variable> outDependencies = new LinkedHashSet<>();
+ // If this subset is empty then no closed subset was found and there is a cycle (or cycles) in
+ // the graph of dependencies between constraints.
+
+ // From JLS 18.5.2.2:
+ // In this case, the constraints in C that participate in a dependency cycle (or cycles) and do
+ // not depend on any constraints outside of the cycle (or cycles) are considered.
+ // A single constraint is selected from the considered constraints, as follows:
+
+ // If any of the considered constraints have the form <Expression -> T>, then the selected
+ // constraint is the considered constraint of this form that contains the expression to the
+ // left (3.5) of the expression of every other considered constraint of this form.
+
+ // If no considered constraint has the form <Expression -> T>, then the selected constraint
+ // is the considered constraint that contains the expression to the left of the expression
+ // of every other considered constraint.
  List<Constraint> consideredConstraints = new ArrayList<>();
- for (Constraint constraint : list) {
+ for (Constraint constraint : c.list) {
  if (!(constraint instanceof TypeConstraint)) {
  continue;
  }
- TypeConstraint c = (TypeConstraint) constraint;
- Set<Variable> newInputs = dependencies.get(c.getInputVariables());
- Set<Variable> newOutputs = dependencies.get(c.getOutputVariables());
+
+ TypeConstraint typeConstraint = (TypeConstraint) constraint;
+ Set<Variable> newInputs = dependencies.get(typeConstraint.getInputVariables());
+ Set<Variable> newOutputs = dependencies.get(typeConstraint.getOutputVariables());
  if (inputDependencies.isEmpty()
  || !Collections.disjoint(newInputs, outDependencies)
  || !Collections.disjoint(newOutputs, inputDependencies)) {
  inputDependencies.addAll(newInputs);
  outDependencies.addAll(newOutputs);
- consideredConstraints.add(c);
+ consideredConstraints.add(typeConstraint);
  }
  }
 
- // A single constraint is selected from the considered constraints, as follows:
-
- // If any of the considered constraints have the form <Expression -> T>, then the selected
- // constraint is the considered constraint of this form that contains the expression to the
- // left (3.5) of the expression of every other considered constraint of this form.
-
- // If no considered constraint has the form <Expression -> T>, then the selected constraint
- // is the considered constraint that contains the expression to the left of the expression
- // of every other considered constraint.
-
- for (Constraint c : consideredConstraints) {
- if (c.getKind() == Kind.EXPRESSION) {
- return new ConstraintSet(c);
+ for (Constraint constraint : consideredConstraints) {
+ if (constraint.getKind() == Kind.EXPRESSION) {
+ return new ConstraintSet(constraint);
  }
  }
 
@@ -334,9 +389,19 @@ public BoundSet reduceOneStep(Java8InferenceContext context) {
  }
  this.addAll(((ReductionResultPair) result).constraintSet);
  } else if (result instanceof TypeConstraint) {
- this.add((Constraint) result);
+ // Add the new constraints to the beginning of the list so they are reduced first. This is
+ // because each constraint is supposed to be reduced until no other constraints are produced
+ // before moving onto another constraint.
+ this.push((Constraint) result);
  } else if (result instanceof ConstraintSet) {
- this.addAll((ConstraintSet) result);
+ if (result == TRUE_ANNO_FAIL) {
+ this.annotationFailure = true;
+ } else {
+ // Add the new constraints to the beginning of the list so they are reduced first. This is
+ // because each constraint is supposed to be reduced until no other constraints are produced
+ // before moving onto another constraint.
+ this.pushAll((ConstraintSet) result);
+ }
  } else if (result instanceof BoundSet) {
  boundSet.merge((BoundSet) result);
  if (boundSet.containsFalse()) {