package org.checkerframework.checker.index.inequality;

import com.sun.source.tree.ExpressionTree;
import com.sun.source.tree.Tree;
import com.sun.source.util.TreePath;
import java.lang.annotation.Annotation;
import java.util.Arrays;
import java.util.Collections;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Set;
import javax.lang.model.element.AnnotationMirror;
import javax.lang.model.element.ExecutableElement;
import javax.lang.model.type.TypeKind;
import javax.lang.model.util.Elements;
import org.checkerframework.checker.index.BaseAnnotatedTypeFactoryForIndexChecker;
import org.checkerframework.checker.index.OffsetDependentTypesHelper;
import org.checkerframework.checker.index.qual.LessThan;
import org.checkerframework.checker.index.qual.LessThanBottom;
import org.checkerframework.checker.index.qual.LessThanUnknown;
import org.checkerframework.checker.index.upperbound.OffsetEquation;
import org.checkerframework.common.basetype.BaseTypeChecker;
import org.checkerframework.common.value.ValueAnnotatedTypeFactory;
import org.checkerframework.common.value.ValueChecker;
import org.checkerframework.common.value.ValueCheckerUtils;
import org.checkerframework.common.value.qual.ArrayLen;
import org.checkerframework.common.value.qual.ArrayLenRange;
import org.checkerframework.common.value.qual.IntRange;
import org.checkerframework.common.value.qual.IntVal;
import org.checkerframework.dataflow.expression.FieldAccess;
import org.checkerframework.dataflow.expression.JavaExpression;
import org.checkerframework.framework.type.AnnotatedTypeMirror;
import org.checkerframework.framework.type.ElementQualifierHierarchy;
import org.checkerframework.framework.type.QualifierHierarchy;
import org.checkerframework.framework.util.JavaExpressionParseUtil.JavaExpressionParseException;
import org.checkerframework.framework.util.dependenttypes.DependentTypesHelper;
import org.checkerframework.javacutil.AnnotationBuilder;
import org.checkerframework.javacutil.AnnotationUtils;
import org.checkerframework.javacutil.SystemUtil;
import org.checkerframework.javacutil.TreeUtils;

/** The type factory for the Less Than Checker. */
public class LessThanAnnotatedTypeFactory extends BaseAnnotatedTypeFactoryForIndexChecker {
  /** The @LessThanBottom annotation. */
  private final AnnotationMirror LESS_THAN_BOTTOM =
      AnnotationBuilder.fromClass(elements, LessThanBottom.class);
  /** The @LessThanUnknown annotation. */
  public final AnnotationMirror LESS_THAN_UNKNOWN =
      AnnotationBuilder.fromClass(elements, LessThanUnknown.class);

  /** The LessThan.value argument/element. */
  private final ExecutableElement lessThanValueElement =
      TreeUtils.getMethod(LessThan.class, "value", 0, processingEnv);

  /**
   * Creates a new LessThanAnnotatedTypeFactory.
   *
   * @param checker the type-checker associated with this type factory
   */
  public LessThanAnnotatedTypeFactory(BaseTypeChecker checker) {
    super(checker);
    postInit();
  }

  /**
   * Returns the Value Checker's annotated type factory.
   *
   * @return the Value Checker's annotated type factory
   */
  public ValueAnnotatedTypeFactory getValueAnnotatedTypeFactory() {
    return getTypeFactoryOfSubchecker(ValueChecker.class);
  }

  @Override
  protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
    return new LinkedHashSet<>(
        Arrays.asList(LessThan.class, LessThanUnknown.class, LessThanBottom.class));
  }

  @Override
  protected DependentTypesHelper createDependentTypesHelper() {
    // Allows + or - in a @LessThan.
    return new OffsetDependentTypesHelper(this);
  }

  @Override
  protected QualifierHierarchy createQualifierHierarchy() {
    return new LessThanQualifierHierarchy(this.getSupportedTypeQualifiers(), elements);
  }

  /** LessThanQualifierHierarchy. */
  class LessThanQualifierHierarchy extends ElementQualifierHierarchy {

    /**
     * Creates a LessThanQualifierHierarchy from the given classes.
     *
     * @param qualifierClasses classes of annotations that are the qualifiers
     * @param elements element utils
     */
    public LessThanQualifierHierarchy(
        Set<Class<? extends Annotation>> qualifierClasses, Elements elements) {
      super(qualifierClasses, elements);
    }

    @Override
    public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) {
      List<String> subList = getLessThanExpressions(subAnno);
      if (subList == null) {
        return true;
      }
      List<String> superList = getLessThanExpressions(superAnno);
      if (superList == null) {
        return false;
      }

      return subList.containsAll(superList);
    }

    @Override
    public AnnotationMirror leastUpperBound(AnnotationMirror a1, AnnotationMirror a2) {
      if (isSubtype(a1, a2)) {
        return a2;
      } else if (isSubtype(a2, a1)) {
        return a1;
      }

      List<String> a1List = getLessThanExpressions(a1);
      List<String> a2List = getLessThanExpressions(a2);
      a1List.retainAll(a2List); // intersection
      return createLessThanQualifier(a1List);
    }

    @Override
    public AnnotationMirror greatestLowerBound(AnnotationMirror a1, AnnotationMirror a2) {
      if (isSubtype(a1, a2)) {
        return a1;
      } else if (isSubtype(a2, a1)) {
        return a2;
      }

      List<String> a1List = getLessThanExpressions(a1);
      List<String> a2List = getLessThanExpressions(a2);
      SystemUtil.addWithoutDuplicates(a1List, a2List); // union
      return createLessThanQualifier(a1List);
    }
  }

  /**
   * Returns true if {@code left} is less than {@code right}.
   *
   * @param left the first tree to compare
   * @param right the second tree to compare
   * @return is left less than right?
   */
  public boolean isLessThan(Tree left, String right) {
    AnnotatedTypeMirror leftATM = getAnnotatedType(left);
    return isLessThan(leftATM.getAnnotationInHierarchy(LESS_THAN_UNKNOWN), right);
  }

  /**
   * Returns true if {@code left} is less than {@code right}.
   *
   * @param left the first value to compare (an annotation)
   * @param right the second value to compare (an expression)
   * @return is left less than right?
   */
  public boolean isLessThan(AnnotationMirror left, String right) {
    List<String> expressions = getLessThanExpressions(left);
    if (expressions == null) {
      // `left` is @LessThanBottom
      return true;
    }
    return expressions.contains(right);
  }

  /**
   * Returns true if {@code smaller < bigger}.
   *
   * @param smaller the first value to compare
   * @param bigger the second value to compare
   * @return {@code smaller < bigger}, using information from the Value Checker
   */
  public boolean isLessThanByValue(Tree smaller, String bigger, TreePath path) {
    Long smallerValue = ValueCheckerUtils.getMinValue(smaller, getValueAnnotatedTypeFactory());
    if (smallerValue == null) {
      return false;
    }

    OffsetEquation offsetEquation = OffsetEquation.createOffsetFromJavaExpression(bigger);
    if (offsetEquation.isInt()) {
      // bigger is an int literal
      return smallerValue < offsetEquation.getInt();
    }
    // If bigger is "expression + literal", then smaller < expression + literal
    // can be reduced to smaller - literal < expression + literal - literal
    smallerValue = smallerValue - offsetEquation.getInt();
    offsetEquation =
        offsetEquation.copyAdd('-', OffsetEquation.createOffsetForInt(offsetEquation.getInt()));

    long minValueOfBigger = getMinValueFromString(offsetEquation.toString(), smaller, path);
    return smallerValue < minValueOfBigger;
  }

  /**
   * Returns the minimum value of {@code expression} at {@code tree}.
   *
   * @param expression the expression whose minimum value to retrieve
   * @param tree where to determine the value
   * @param path the path to {@code tree}
   * @return the minimum value of {@code expression} at {@code tree}
   */
  private long getMinValueFromString(String expression, Tree tree, TreePath path) {
    ValueAnnotatedTypeFactory valueAtypeFactory = getValueAnnotatedTypeFactory();
    JavaExpression expressionJe;
    try {
      expressionJe = valueAtypeFactory.parseJavaExpressionString(expression, path);
    } catch (JavaExpressionParseException e) {
      return Long.MIN_VALUE;
    }

    AnnotationMirror intRange =
        valueAtypeFactory.getAnnotationFromJavaExpression(expressionJe, tree, IntRange.class);
    if (intRange != null) {
      return valueAtypeFactory.getRange(intRange).from;
    }
    AnnotationMirror intValue =
        valueAtypeFactory.getAnnotationFromJavaExpression(expressionJe, tree, IntVal.class);
    if (intValue != null) {
      List<Long> possibleValues = valueAtypeFactory.getIntValues(intValue);
      return Collections.min(possibleValues);
    }

    if (expressionJe instanceof FieldAccess) {
      FieldAccess fieldAccess = ((FieldAccess) expressionJe);
      if (fieldAccess.getReceiver().getType().getKind() == TypeKind.ARRAY) {
        // array.length might not be in the store, so check for the length of the array.
        AnnotationMirror arrayRange =
            valueAtypeFactory.getAnnotationFromJavaExpression(
                fieldAccess.getReceiver(), tree, ArrayLenRange.class);
        if (arrayRange != null) {
          return valueAtypeFactory.getRange(arrayRange).from;
        }
        AnnotationMirror arrayLen =
            valueAtypeFactory.getAnnotationFromJavaExpression(expressionJe, tree, ArrayLen.class);
        if (arrayLen != null) {
          List<Integer> possibleValues = valueAtypeFactory.getArrayLength(arrayLen);
          return Collections.min(possibleValues);
        }
        // Even arrays that we know nothing about must have at least zero length.
        return 0;
      }
    }

    return Long.MIN_VALUE;
  }

  /**
   * Returns true if left is less than or equal to right.
   *
   * @param left the first value to compare
   * @param right the second value to compare
   * @return is left less than or equal to right?
   */
  public boolean isLessThanOrEqual(Tree left, String right) {
    AnnotatedTypeMirror leftATM = getAnnotatedType(left);
    return isLessThanOrEqual(leftATM.getAnnotationInHierarchy(LESS_THAN_UNKNOWN), right);
  }

  /**
   * Returns true if left is less than or equal to right.
   *
   * @param left the first value to compare
   * @param right the second value to compare
   * @return is left less than or equal to right?
   */
  public boolean isLessThanOrEqual(AnnotationMirror left, String right) {
    List<String> expressions = getLessThanExpressions(left);
    if (expressions == null) {
      // left is bottom so it is always less than right.
      return true;
    }
    if (expressions.contains(right)) {
      return true;
    }
    // {@code @LessThan("end + 1")} is equivalent to {@code @LessThanOrEqual("end")}.
    for (String expression : expressions) {
      if (expression.endsWith(" + 1")
          && expression.substring(0, expression.length() - 4).equals(right)) {
        return true;
      }
    }
    return false;
  }

  /**
   * Returns a sorted, modifiable list of expressions that {@code expression} is less than. If the
   * {@code expression} is annotated with {@link LessThanBottom}, null is returned.
   *
   * @param expression an expression
   * @return expressions that {@code expression} is less than
   */
  public List<String> getLessThanExpressions(ExpressionTree expression) {
    AnnotatedTypeMirror annotatedTypeMirror = getAnnotatedType(expression);
    return getLessThanExpressions(annotatedTypeMirror.getAnnotationInHierarchy(LESS_THAN_UNKNOWN));
  }

  /**
   * Creates a less than qualifier given the expressions.
   *
   * <p>If expressions is null, {@link LessThanBottom} is returned. If expressions is empty, {@link
   * LessThanUnknown} is returned. Otherwise, {@code @LessThan(expressions)} is returned.
   *
   * @param expressions a list of expressions
   * @return a @LessThan qualifier with the given arguments
   */
  public AnnotationMirror createLessThanQualifier(List<String> expressions) {
    if (expressions == null) {
      return LESS_THAN_BOTTOM;
    } else if (expressions.isEmpty()) {
      return LESS_THAN_UNKNOWN;
    } else {
      AnnotationBuilder builder = new AnnotationBuilder(processingEnv, LessThan.class);
      builder.setValue("value", expressions);
      return builder.build();
    }
  }

  /** Returns {@code @LessThan(expression)}. */
  public AnnotationMirror createLessThanQualifier(String expression) {
    return createLessThanQualifier(Collections.singletonList(expression));
  }

  /**
   * If the annotation is LessThan, returns a list of expressions in the annotation. If the
   * annotation is {@link LessThanBottom}, returns null. If the annotation is {@link
   * LessThanUnknown}, returns the empty list.
   *
   * @param annotation an annotation from the same hierarchy as LessThan
   * @return the list of expressions in the annotation
   */
  public List<String> getLessThanExpressions(AnnotationMirror annotation) {
    if (AnnotationUtils.areSameByName(
        annotation, "org.checkerframework.checker.index.qual.LessThanBottom")) {
      return null;
    } else if (AnnotationUtils.areSameByName(
        annotation, "org.checkerframework.checker.index.qual.LessThanUnknown")) {
      return Collections.emptyList();
    } else {
      // The annotation is @LessThan.
      return AnnotationUtils.getElementValueArray(annotation, lessThanValueElement, String.class);
    }
  }
}