checker/src/main/java/org/checkerframework/checker/index/OffsetDependentTypesHelper.java

package org.checkerframework.checker.index;

import com.sun.source.tree.MemberSelectTree;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.common.value.ValueCheckerUtils;
import org.checkerframework.dataflow.expression.JavaExpression;
import org.checkerframework.framework.type.AnnotatedTypeFactory;
import org.checkerframework.framework.type.AnnotatedTypeMirror;
import org.checkerframework.framework.type.treeannotator.TreeAnnotator;
import org.checkerframework.framework.util.dependenttypes.DependentTypesHelper;
import org.checkerframework.framework.util.dependenttypes.DependentTypesTreeAnnotator;
import org.checkerframework.javacutil.TreeUtils;

/**
 * Dependent type helper for array offset expressions. Each array offset expression may be the
 * addition or subtraction of several Java expressions. For example, {@code array.length - 1}.
 */
public class OffsetDependentTypesHelper extends DependentTypesHelper {
  public OffsetDependentTypesHelper(AnnotatedTypeFactory factory) {
    super(factory);
  }

  @Override
  protected @Nullable JavaExpression transform(JavaExpression javaExpr) {
    return ValueCheckerUtils.optimize(javaExpr, factory);
  }

  @Override
  public TreeAnnotator createDependentTypesTreeAnnotator() {
    return new DependentTypesTreeAnnotator(factory, this) {
      @Override
      public Void visitMemberSelect(MemberSelectTree tree, AnnotatedTypeMirror type) {
        // UpperBoundTreeAnnotator changes the type of array.length to @LTEL("array").
        // If the DependentTypesTreeAnnotator tries to viewpoint-adapt it based on the
        // declaration of length, it will fail.
        if (TreeUtils.isArrayLengthAccess(tree)) {
          return null;
        }
        return super.visitMemberSelect(tree, type);
      }
    };
  }
}