package org.checkerframework.framework.flow;

import com.sun.source.tree.ClassTree;
import com.sun.source.tree.ExpressionTree;
import com.sun.source.tree.MethodTree;
import com.sun.source.tree.Tree;
import com.sun.source.tree.VariableTree;
import com.sun.source.util.TreePath;
import com.sun.tools.javac.code.Symbol.ClassSymbol;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import javax.lang.model.element.AnnotationMirror;
import javax.lang.model.element.Element;
import javax.lang.model.element.ElementKind;
import javax.lang.model.element.ExecutableElement;
import javax.lang.model.element.VariableElement;
import javax.lang.model.type.TypeMirror;
import org.checkerframework.checker.interning.qual.InternedDistinct;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.dataflow.analysis.ConditionalTransferResult;
import org.checkerframework.dataflow.analysis.ForwardTransferFunction;
import org.checkerframework.dataflow.analysis.RegularTransferResult;
import org.checkerframework.dataflow.analysis.TransferInput;
import org.checkerframework.dataflow.analysis.TransferResult;
import org.checkerframework.dataflow.cfg.UnderlyingAST;
import org.checkerframework.dataflow.cfg.UnderlyingAST.CFGLambda;
import org.checkerframework.dataflow.cfg.UnderlyingAST.CFGMethod;
import org.checkerframework.dataflow.cfg.UnderlyingAST.Kind;
import org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor;
import org.checkerframework.dataflow.cfg.node.ArrayAccessNode;
import org.checkerframework.dataflow.cfg.node.AssignmentNode;
import org.checkerframework.dataflow.cfg.node.CaseNode;
import org.checkerframework.dataflow.cfg.node.ClassNameNode;
import org.checkerframework.dataflow.cfg.node.ConditionalNotNode;
import org.checkerframework.dataflow.cfg.node.EqualToNode;
import org.checkerframework.dataflow.cfg.node.FieldAccessNode;
import org.checkerframework.dataflow.cfg.node.InstanceOfNode;
import org.checkerframework.dataflow.cfg.node.LambdaResultExpressionNode;
import org.checkerframework.dataflow.cfg.node.LocalVariableNode;
import org.checkerframework.dataflow.cfg.node.MethodInvocationNode;
import org.checkerframework.dataflow.cfg.node.NarrowingConversionNode;
import org.checkerframework.dataflow.cfg.node.Node;
import org.checkerframework.dataflow.cfg.node.NotEqualNode;
import org.checkerframework.dataflow.cfg.node.ObjectCreationNode;
import org.checkerframework.dataflow.cfg.node.ReturnNode;
import org.checkerframework.dataflow.cfg.node.StringConcatenateAssignmentNode;
import org.checkerframework.dataflow.cfg.node.StringConversionNode;
import org.checkerframework.dataflow.cfg.node.TernaryExpressionNode;
import org.checkerframework.dataflow.cfg.node.ThisNode;
import org.checkerframework.dataflow.cfg.node.VariableDeclarationNode;
import org.checkerframework.dataflow.cfg.node.WideningConversionNode;
import org.checkerframework.dataflow.expression.ClassName;
import org.checkerframework.dataflow.expression.FieldAccess;
import org.checkerframework.dataflow.expression.JavaExpression;
import org.checkerframework.dataflow.expression.LocalVariable;
import org.checkerframework.dataflow.expression.ThisReference;
import org.checkerframework.dataflow.util.NodeUtils;
import org.checkerframework.framework.type.AnnotatedTypeFactory;
import org.checkerframework.framework.type.AnnotatedTypeMirror;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType;
import org.checkerframework.framework.type.GenericAnnotatedTypeFactory;
import org.checkerframework.framework.util.AnnotatedTypes;
import org.checkerframework.framework.util.Contract;
import org.checkerframework.framework.util.Contract.ConditionalPostcondition;
import org.checkerframework.framework.util.Contract.Postcondition;
import org.checkerframework.framework.util.Contract.Precondition;
import org.checkerframework.framework.util.ContractsFromMethod;
import org.checkerframework.framework.util.JavaExpressionParseUtil.JavaExpressionParseException;
import org.checkerframework.framework.util.StringToJavaExpression;
import org.checkerframework.javacutil.ElementUtils;
import org.checkerframework.javacutil.Pair;
import org.checkerframework.javacutil.TreePathUtil;
import org.checkerframework.javacutil.TreeUtils;

/**
 * The default analysis transfer function for the Checker Framework propagates information through
 * assignments and uses the {@link AnnotatedTypeFactory} to provide checker-specific logic how to
 * combine types (e.g., what is the type of a string concatenation, given the types of the two
 * operands) and as an abstraction function (e.g., determine the annotations on literals).
 *
 * <p>Design note: CFAbstractTransfer and its subclasses are supposed to act as transfer functions.
 * But, since the AnnotatedTypeFactory already existed and performed checker-independent type
 * propagation, CFAbstractTransfer delegates work to it instead of duplicating some logic in
 * CFAbstractTransfer. The checker-specific subclasses of CFAbstractTransfer do implement transfer
 * function logic themselves.
 */
public abstract class CFAbstractTransfer<
        V extends CFAbstractValue<V>,
        S extends CFAbstractStore<V, S>,
        T extends CFAbstractTransfer<V, S, T>>
    extends AbstractNodeVisitor<TransferResult<V, S>, TransferInput<V, S>>
    implements ForwardTransferFunction<V, S> {

  /** The analysis used by this transfer function. */
  protected final CFAbstractAnalysis<V, S, T> analysis;

  /**
   * Should the analysis use sequential Java semantics (i.e., assume that only one thread is running
   * at all times)?
   */
  protected final boolean sequentialSemantics;

  /** Indicates that the whole-program inference is on. */
  private final boolean infer;

  /**
   * Create a CFAbstractTransfer.
   *
   * @param analysis the analysis used by this transfer function
   */
  protected CFAbstractTransfer(CFAbstractAnalysis<V, S, T> analysis) {
    this(analysis, false);
  }

  /**
   * Constructor that allows forcing concurrent semantics to be on for this instance of
   * CFAbstractTransfer.
   *
   * @param analysis the analysis used by this transfer function
   * @param forceConcurrentSemantics whether concurrent semantics should be forced to be on. If
   *     false, concurrent semantics are turned off by default, but the user can still turn them on
   *     via {@code -AconcurrentSemantics}. If true, the user cannot turn off concurrent semantics.
   */
  protected CFAbstractTransfer(
      CFAbstractAnalysis<V, S, T> analysis, boolean forceConcurrentSemantics) {
    this.analysis = analysis;
    this.sequentialSemantics =
        !(forceConcurrentSemantics || analysis.checker.hasOption("concurrentSemantics"));
    this.infer = analysis.checker.hasOption("infer");
  }

  /**
   * Returns true if the transfer function uses sequential semantics, false if it uses concurrent
   * semantics. Useful when creating an empty store, since a store makes different decisions
   * depending on whether sequential or concurrent semantics are used.
   *
   * @return true if the transfer function uses sequential semantics, false if it uses concurrent
   *     semantics
   */
  public boolean usesSequentialSemantics() {
    return sequentialSemantics;
  }

  /**
   * A hook for subclasses to modify the result of the transfer function. This method is called
   * before returning the abstract value {@code value} as the result of the transfer function.
   *
   * <p>If a subclass overrides this method, the subclass should also override {@link
   * #finishValue(CFAbstractValue,CFAbstractStore,CFAbstractStore)}.
   *
   * @param value a value to possibly modify
   * @param store the store
   * @return the possibly-modified value
   */
  protected @Nullable V finishValue(@Nullable V value, S store) {
    return value;
  }

  /**
   * A hook for subclasses to modify the result of the transfer function. This method is called
   * before returning the abstract value {@code value} as the result of the transfer function.
   *
   * <p>If a subclass overrides this method, the subclass should also override {@link
   * #finishValue(CFAbstractValue,CFAbstractStore)}.
   *
   * @param value the value to finish
   * @param thenStore the "then" store
   * @param elseStore the "else" store
   * @return the possibly-modified value
   */
  protected @Nullable V finishValue(@Nullable V value, S thenStore, S elseStore) {
    return value;
  }

  /**
   * Returns the abstract value of a non-leaf tree {@code tree}, as computed by the {@link
   * AnnotatedTypeFactory}.
   *
   * @return the abstract value of a non-leaf tree {@code tree}, as computed by the {@link
   *     AnnotatedTypeFactory}
   */
  protected V getValueFromFactory(Tree tree, Node node) {
    GenericAnnotatedTypeFactory<V, S, T, ? extends CFAbstractAnalysis<V, S, T>> factory =
        analysis.atypeFactory;
    Tree preTree = analysis.getCurrentTree();
    Pair<Tree, AnnotatedTypeMirror> preContext = factory.getVisitorState().getAssignmentContext();
    analysis.setCurrentTree(tree);
    // is there an assignment context node available?
    if (node != null && node.getAssignmentContext() != null) {
      // Get the declared type of the assignment context by looking up the assignment context tree's
      // type in the factory while flow is disabled.
      Tree contextTree = node.getAssignmentContext().getContextTree();
      AnnotatedTypeMirror assignmentContext = null;
      if (contextTree != null) {
        assignmentContext = factory.getAnnotatedTypeLhs(contextTree);
      } else {
        Element assignmentContextElement = node.getAssignmentContext().getElementForType();
        if (assignmentContextElement != null) {
          // if contextTree is null, use the element to get the type
          assignmentContext = factory.getAnnotatedType(assignmentContextElement);
        }
      }

      if (assignmentContext != null) {
        if (assignmentContext instanceof AnnotatedExecutableType) {
          // For a MethodReturnContext, we get the full type of the
          // method, but we only want the return type.
          assignmentContext = ((AnnotatedExecutableType) assignmentContext).getReturnType();
        }
        factory
            .getVisitorState()
            .setAssignmentContext(
                Pair.of(node.getAssignmentContext().getContextTree(), assignmentContext));
      }
    }
    AnnotatedTypeMirror at;
    if (node instanceof MethodInvocationNode
        && ((MethodInvocationNode) node).getIterableExpression() != null) {
      ExpressionTree iter = ((MethodInvocationNode) node).getIterableExpression();
      at = factory.getIterableElementType(iter);
    } else if (node instanceof ArrayAccessNode
        && ((ArrayAccessNode) node).getArrayExpression() != null) {
      ExpressionTree array = ((ArrayAccessNode) node).getArrayExpression();
      at = factory.getIterableElementType(array);
    } else {
      at = factory.getAnnotatedType(tree);
    }
    analysis.setCurrentTree(preTree);
    factory.getVisitorState().setAssignmentContext(preContext);
    return analysis.createAbstractValue(at);
  }

  /**
   * Returns an abstract value with the given {@code type} and the annotations from {@code
   * annotatedValue}.
   *
   * @param type the type to return
   * @param annotatedValue the annotations to return
   * @return an abstract value with the given {@code type} and the annotations from {@code
   *     annotatedValue}
   * @deprecated use {@link #getWidenedValue} or {@link #getNarrowedValue}
   */
  @Deprecated // 2020-10-02
  protected V getValueWithSameAnnotations(TypeMirror type, V annotatedValue) {
    if (annotatedValue == null) {
      return null;
    }
    return analysis.createAbstractValue(annotatedValue.getAnnotations(), type);
  }

  /** The fixed initial store. */
  private S fixedInitialStore = null;

  /** Set a fixed initial Store. */
  public void setFixedInitialStore(S s) {
    fixedInitialStore = s;
  }

  /** The initial store maps method formal parameters to their currently most refined type. */
  @Override
  public S initialStore(UnderlyingAST underlyingAST, @Nullable List<LocalVariableNode> parameters) {
    if (underlyingAST.getKind() != Kind.LAMBDA && underlyingAST.getKind() != Kind.METHOD) {
      if (fixedInitialStore != null) {
        return fixedInitialStore;
      } else {
        return analysis.createEmptyStore(sequentialSemantics);
      }
    }

    S info;

    if (underlyingAST.getKind() == Kind.METHOD) {

      if (fixedInitialStore != null) {
        // copy knowledge
        info = analysis.createCopiedStore(fixedInitialStore);
      } else {
        info = analysis.createEmptyStore(sequentialSemantics);
      }

      AnnotatedTypeFactory factory = analysis.getTypeFactory();
      for (LocalVariableNode p : parameters) {
        AnnotatedTypeMirror anno = factory.getAnnotatedType(p.getElement());
        info.initializeMethodParameter(p, analysis.createAbstractValue(anno));
      }

      // add properties known through precondition
      CFGMethod method = (CFGMethod) underlyingAST;
      MethodTree methodDeclTree = method.getMethod();
      ExecutableElement methodElem = TreeUtils.elementFromDeclaration(methodDeclTree);
      addInformationFromPreconditions(info, factory, method, methodDeclTree, methodElem);

      final ClassTree classTree = method.getClassTree();
      addFieldValues(info, factory, classTree, methodDeclTree);

      addFinalLocalValues(info, methodElem);

      if (shouldPerformWholeProgramInference(methodDeclTree, methodElem)) {
        Map<AnnotatedDeclaredType, ExecutableElement> overriddenMethods =
            AnnotatedTypes.overriddenMethods(
                analysis.atypeFactory.getElementUtils(), analysis.atypeFactory, methodElem);
        for (Map.Entry<AnnotatedDeclaredType, ExecutableElement> pair :
            overriddenMethods.entrySet()) {
          AnnotatedExecutableType overriddenMethod =
              AnnotatedTypes.asMemberOf(
                  analysis.atypeFactory.getProcessingEnv().getTypeUtils(),
                  analysis.atypeFactory,
                  pair.getKey(),
                  pair.getValue());

          // Infers parameter and receiver types of the method based
          // on the overridden method.
          analysis
              .atypeFactory
              .getWholeProgramInference()
              .updateFromOverride(methodDeclTree, methodElem, overriddenMethod);
        }
      }

    } else if (underlyingAST.getKind() == Kind.LAMBDA) {
      // Create a copy and keep only the field values (nothing else applies).
      info = analysis.createCopiedStore(fixedInitialStore);
      // Allow that local variables are retained; they are effectively final,
      // otherwise Java wouldn't allow access from within the lambda.
      // TODO: what about the other information? Can code further down be simplified?
      // info.localVariableValues.clear();
      info.classValues.clear();
      info.arrayValues.clear();
      info.methodValues.clear();

      AnnotatedTypeFactory factory = analysis.getTypeFactory();
      for (LocalVariableNode p : parameters) {
        AnnotatedTypeMirror anno = factory.getAnnotatedType(p.getElement());
        info.initializeMethodParameter(p, analysis.createAbstractValue(anno));
      }

      CFGLambda lambda = (CFGLambda) underlyingAST;
      @SuppressWarnings("interning:assignment") // used in == tests
      @InternedDistinct Tree enclosingTree =
          TreePathUtil.enclosingOfKind(
              factory.getPath(lambda.getLambdaTree()),
              new HashSet<>(
                  Arrays.asList(
                      Tree.Kind.METHOD,
                      // Tree.Kind for which TreeUtils.isClassTree is true
                      Tree.Kind.CLASS,
                      Tree.Kind.INTERFACE,
                      Tree.Kind.ANNOTATION_TYPE,
                      Tree.Kind.ENUM)));

      Element enclosingElement = null;
      if (enclosingTree.getKind() == Tree.Kind.METHOD) {
        // If it is in an initializer, we need to use locals from the initializer.
        enclosingElement = TreeUtils.elementFromTree(enclosingTree);

      } else if (TreeUtils.isClassTree(enclosingTree)) {

        // Try to find an enclosing initializer block.
        // Would love to know if there was a better way.
        // Find any enclosing element of the lambda (using trees).
        // Then go up the elements to find an initializer element (which can't be found with the
        // tree).
        TreePath loopTree = factory.getPath(lambda.getLambdaTree()).getParentPath();
        Element anEnclosingElement = null;
        while (loopTree.getLeaf() != enclosingTree) {
          Element sym = TreeUtils.elementFromTree(loopTree.getLeaf());
          if (sym != null) {
            anEnclosingElement = sym;
            break;
          }
          loopTree = loopTree.getParentPath();
        }
        while (anEnclosingElement != null
            && !anEnclosingElement.equals(TreeUtils.elementFromTree(enclosingTree))) {
          if (anEnclosingElement.getKind() == ElementKind.INSTANCE_INIT
              || anEnclosingElement.getKind() == ElementKind.STATIC_INIT) {
            enclosingElement = anEnclosingElement;
            break;
          }
          anEnclosingElement = anEnclosingElement.getEnclosingElement();
        }
      }
      if (enclosingElement != null) {
        addFinalLocalValues(info, enclosingElement);
      }

      // We want the initialization stuff, but need to throw out any refinements.
      Map<FieldAccess, V> fieldValuesClone = new HashMap<>(info.fieldValues);
      for (Map.Entry<FieldAccess, V> fieldValue : fieldValuesClone.entrySet()) {
        AnnotatedTypeMirror declaredType = factory.getAnnotatedType(fieldValue.getKey().getField());
        V lubbedValue =
            analysis.createAbstractValue(declaredType).leastUpperBound(fieldValue.getValue());
        info.fieldValues.put(fieldValue.getKey(), lubbedValue);
      }
    } else {
      assert false : "Unexpected tree: " + underlyingAST;
      info = null;
    }

    return info;
  }

  private void addFieldValues(
      S info, AnnotatedTypeFactory factory, ClassTree classTree, MethodTree methodTree) {

    // Add knowledge about final fields, or values of non-final fields
    // if we are inside a constructor (information about initializers)
    TypeMirror classType = TreeUtils.typeOf(classTree);
    List<Pair<VariableElement, V>> fieldValues = analysis.getFieldValues();
    for (Pair<VariableElement, V> p : fieldValues) {
      VariableElement element = p.first;
      V value = p.second;
      if (ElementUtils.isFinal(element) || TreeUtils.isConstructor(methodTree)) {
        JavaExpression receiver;
        if (ElementUtils.isStatic(element)) {
          receiver = new ClassName(classType);
        } else {
          receiver = new ThisReference(classType);
        }
        TypeMirror fieldType = ElementUtils.getType(element);
        JavaExpression field = new FieldAccess(receiver, fieldType, element);
        info.insertValue(field, value);
      }
    }

    // add properties about fields (static information from type)
    boolean isNotFullyInitializedReceiver = isNotFullyInitializedReceiver(methodTree);
    if (isNotFullyInitializedReceiver && !TreeUtils.isConstructor(methodTree)) {
      // cannot add information about fields if the receiver isn't initialized
      // and the method isn't a constructor
      return;
    }
    for (Tree member : classTree.getMembers()) {
      if (member instanceof VariableTree) {
        VariableTree vt = (VariableTree) member;
        final VariableElement element = TreeUtils.elementFromDeclaration(vt);
        AnnotatedTypeMirror type =
            ((GenericAnnotatedTypeFactory<?, ?, ?, ?>) factory).getAnnotatedTypeLhs(vt);
        TypeMirror fieldType = ElementUtils.getType(element);
        JavaExpression receiver;
        if (ElementUtils.isStatic(element)) {
          receiver = new ClassName(classType);
        } else {
          receiver = new ThisReference(classType);
        }
        V value = analysis.createAbstractValue(type);
        if (value == null) {
          continue;
        }
        if (TreeUtils.isConstructor(methodTree)) {
          // If we are in a constructor, then we can still use the static type, but only if there is
          // also an initializer that already does some initialization.
          boolean found = false;
          for (Pair<VariableElement, V> fieldValue : fieldValues) {
            if (fieldValue.first.equals(element)) {
              value = value.leastUpperBound(fieldValue.second);
              found = true;
              break;
            }
          }
          if (!found) {
            // no initializer found, cannot use static type
            continue;
          }
        }
        JavaExpression field = new FieldAccess(receiver, fieldType, element);
        info.insertValue(field, value);
      }
    }
  }

  private void addFinalLocalValues(S info, Element enclosingElement) {
    // add information about effectively final variables (from outer scopes)
    for (Map.Entry<Element, V> e : analysis.atypeFactory.getFinalLocalValues().entrySet()) {

      Element elem = e.getKey();

      // TODO: There is a design flaw where the values of final local values leaks
      // into other methods of the same class. For example, in
      // class a { void b() {...} void c() {...} }
      // final local values from b() would be visible in the store for c(),
      // even though they should only be visible in b() and in classes
      // defined inside the method body of b().
      // This is partly because GenericAnnotatedTypeFactory.performFlowAnalysis does not call itself
      // recursively to analyze inner classes, but instead pops classes off of a queue, and the
      // information about known final local values is stored by GenericAnnotatedTypeFactory.analyze
      // in GenericAnnotatedTypeFactory.flowResult, which is visible to all classes in the queue
      // regardless of their level of recursion.

      // We work around this here by ensuring that we only add a final local value to a method's
      // store if that method is enclosed by the method where the local variables were declared.

      // Find the enclosing method of the element
      Element enclosingMethodOfVariableDeclaration = elem.getEnclosingElement();

      if (enclosingMethodOfVariableDeclaration != null) {

        // Now find all the enclosing methods of the code we are analyzing. If any one of
        // them matches the above, then the final local variable value applies.
        Element enclosingMethodOfCurrentMethod = enclosingElement;

        while (enclosingMethodOfCurrentMethod != null) {
          if (enclosingMethodOfVariableDeclaration.equals(enclosingMethodOfCurrentMethod)) {
            LocalVariable l = new LocalVariable(elem);
            info.insertValue(l, e.getValue());
            break;
          }

          enclosingMethodOfCurrentMethod = enclosingMethodOfCurrentMethod.getEnclosingElement();
        }
      }
    }
  }

  /**
   * Returns true if the receiver of a method or constructor might not yet be fully initialized.
   *
   * @param methodDeclTree the declaration of the method or constructor
   * @return true if the receiver of a method or constructormight not yet be fully initialized
   */
  protected boolean isNotFullyInitializedReceiver(MethodTree methodDeclTree) {
    return TreeUtils.isConstructor(methodDeclTree);
  }

  /**
   * Add the information from all the preconditions of a method to the initial store in the method
   * body.
   *
   * @param initialStore the initial store for the method body
   * @param factory the type factory
   * @param methodAst the AST for a method declaration
   * @param methodDeclTree the declaration of the method; is a field of {@code methodAst}
   * @param methodElement the element for the method
   */
  protected void addInformationFromPreconditions(
      S initialStore,
      AnnotatedTypeFactory factory,
      CFGMethod methodAst,
      MethodTree methodDeclTree,
      ExecutableElement methodElement) {
    ContractsFromMethod contractsUtils = analysis.atypeFactory.getContractsFromMethod();
    Set<Precondition> preconditions = contractsUtils.getPreconditions(methodElement);
    StringToJavaExpression stringToJavaExpr =
        stringExpr ->
            StringToJavaExpression.atMethodBody(stringExpr, methodDeclTree, analysis.checker);
    for (Precondition p : preconditions) {
      String stringExpr = p.expressionString;
      AnnotationMirror annotation =
          p.viewpointAdaptDependentTypeAnnotation(
              analysis.atypeFactory, stringToJavaExpr, /*errorTree=*/ null);
      JavaExpression exprJe;
      try {
        // TODO: currently, these expressions are parsed at the declaration (i.e. here) and for
        // every use. this could be optimized to store the result the first time.
        // (same for other annotations)
        exprJe = StringToJavaExpression.atMethodBody(stringExpr, methodDeclTree, analysis.checker);
      } catch (JavaExpressionParseException e) {
        // Errors are reported by BaseTypeVisitor.checkContractsAtMethodDeclaration().
        continue;
      }
      initialStore.insertValuePermitNondeterministic(exprJe, annotation);
    }
  }

  /**
   * The default visitor returns the input information unchanged, or in the case of conditional
   * input information, merged.
   */
  @Override
  public TransferResult<V, S> visitNode(Node n, TransferInput<V, S> in) {
    V value = null;

    // TODO: handle implicit/explicit this and go to correct factory method
    Tree tree = n.getTree();
    if (tree != null) {
      if (TreeUtils.canHaveTypeAnnotation(tree)) {
        value = getValueFromFactory(tree, n);
      }
    }

    return createTransferResult(value, in);
  }

  /**
   * Creates a TransferResult.
   *
   * <p>This default implementation returns the input information unchanged, or in the case of
   * conditional input information, merged.
   *
   * @param value the value; possibly null
   * @param in the transfer input
   * @return the input information, as a TransferResult
   */
  protected TransferResult<V, S> createTransferResult(@Nullable V value, TransferInput<V, S> in) {
    if (in.containsTwoStores()) {
      S thenStore = in.getThenStore();
      S elseStore = in.getElseStore();
      return new ConditionalTransferResult<>(
          finishValue(value, thenStore, elseStore), thenStore, elseStore);
    } else {
      S info = in.getRegularStore();
      return new RegularTransferResult<>(finishValue(value, info), info);
    }
  }

  /**
   * Creates a TransferResult just like the given one, but with the given value.
   *
   * <p>This default implementation returns the input information unchanged, or in the case of
   * conditional input information, merged.
   *
   * @param value the value; possibly null
   * @param in the TransferResult to copy
   * @return the input informatio
   */
  protected TransferResult<V, S> recreateTransferResult(
      @Nullable V value, TransferResult<V, S> in) {
    if (in.containsTwoStores()) {
      S thenStore = in.getThenStore();
      S elseStore = in.getElseStore();
      return new ConditionalTransferResult<>(
          finishValue(value, thenStore, elseStore), thenStore, elseStore);
    } else {
      S info = in.getRegularStore();
      return new RegularTransferResult<>(finishValue(value, info), info);
    }
  }

  @Override
  public TransferResult<V, S> visitClassName(ClassNameNode n, TransferInput<V, S> in) {
    // The tree underlying a class name is a type tree.
    V value = null;

    Tree tree = n.getTree();
    if (tree != null) {
      if (TreeUtils.canHaveTypeAnnotation(tree)) {
        GenericAnnotatedTypeFactory<V, S, T, ? extends CFAbstractAnalysis<V, S, T>> factory =
            analysis.atypeFactory;
        analysis.setCurrentTree(tree);
        AnnotatedTypeMirror at = factory.getAnnotatedTypeFromTypeTree(tree);
        analysis.setCurrentTree(null);
        value = analysis.createAbstractValue(at);
      }
    }

    return createTransferResult(value, in);
  }

  @Override
  public TransferResult<V, S> visitFieldAccess(FieldAccessNode n, TransferInput<V, S> p) {
    S store = p.getRegularStore();
    V storeValue = store.getValue(n);
    // look up value in factory, and take the more specific one
    // TODO: handle cases, where this is not allowed (e.g. constructors in non-null type systems)
    V factoryValue = getValueFromFactory(n.getTree(), n);
    V value = moreSpecificValue(factoryValue, storeValue);
    return new RegularTransferResult<>(finishValue(value, store), store);
  }

  @Override
  public TransferResult<V, S> visitArrayAccess(ArrayAccessNode n, TransferInput<V, S> p) {
    S store = p.getRegularStore();
    V storeValue = store.getValue(n);
    // look up value in factory, and take the more specific one
    V factoryValue = getValueFromFactory(n.getTree(), n);
    V value = moreSpecificValue(factoryValue, storeValue);
    return new RegularTransferResult<>(finishValue(value, store), store);
  }

  /** Use the most specific type information available according to the store. */
  @Override
  public TransferResult<V, S> visitLocalVariable(LocalVariableNode n, TransferInput<V, S> in) {
    S store = in.getRegularStore();
    V valueFromStore = store.getValue(n);
    V valueFromFactory = getValueFromFactory(n.getTree(), n);
    V value = moreSpecificValue(valueFromFactory, valueFromStore);
    return new RegularTransferResult<>(finishValue(value, store), store);
  }

  @Override
  public TransferResult<V, S> visitThis(ThisNode n, TransferInput<V, S> in) {
    S store = in.getRegularStore();
    V valueFromStore = store.getValue(n);

    V valueFromFactory = null;
    V value = null;
    Tree tree = n.getTree();
    if (tree != null && TreeUtils.canHaveTypeAnnotation(tree)) {
      valueFromFactory = getValueFromFactory(tree, n);
    }

    if (valueFromFactory == null) {
      value = valueFromStore;
    } else {
      value = moreSpecificValue(valueFromFactory, valueFromStore);
    }

    return new RegularTransferResult<>(finishValue(value, store), store);
  }

  @Override
  public TransferResult<V, S> visitTernaryExpression(
      TernaryExpressionNode n, TransferInput<V, S> p) {
    TransferResult<V, S> result = super.visitTernaryExpression(n, p);
    S thenStore = result.getThenStore();
    S elseStore = result.getElseStore();
    V thenValue = p.getValueOfSubNode(n.getThenOperand());
    V elseValue = p.getValueOfSubNode(n.getElseOperand());
    V resultValue = null;
    if (thenValue != null && elseValue != null) {
      // The resulting abstract value is the merge of the 'then' and 'else' branch.
      resultValue = thenValue.leastUpperBound(elseValue);
    }
    V finishedValue = finishValue(resultValue, thenStore, elseStore);
    return new ConditionalTransferResult<>(finishedValue, thenStore, elseStore);
  }

  /** Reverse the role of the 'thenStore' and 'elseStore'. */
  @Override
  public TransferResult<V, S> visitConditionalNot(ConditionalNotNode n, TransferInput<V, S> p) {
    TransferResult<V, S> result = super.visitConditionalNot(n, p);
    S thenStore = result.getThenStore();
    S elseStore = result.getElseStore();
    return new ConditionalTransferResult<>(result.getResultValue(), elseStore, thenStore);
  }

  @Override
  public TransferResult<V, S> visitEqualTo(EqualToNode n, TransferInput<V, S> p) {
    TransferResult<V, S> res = super.visitEqualTo(n, p);

    Node leftN = n.getLeftOperand();
    Node rightN = n.getRightOperand();
    V leftV = p.getValueOfSubNode(leftN);
    V rightV = p.getValueOfSubNode(rightN);

    if (res.containsTwoStores()
        && (NodeUtils.isConstantBoolean(leftN, false)
            || NodeUtils.isConstantBoolean(rightN, false))) {
      S thenStore = res.getElseStore();
      S elseStore = res.getThenStore();
      res = new ConditionalTransferResult<>(res.getResultValue(), thenStore, elseStore);
    }

    // if annotations differ, use the one that is more precise for both
    // sides (and add it to the store if possible)
    res = strengthenAnnotationOfEqualTo(res, leftN, rightN, leftV, rightV, false);
    res = strengthenAnnotationOfEqualTo(res, rightN, leftN, rightV, leftV, false);
    return res;
  }

  @Override
  public TransferResult<V, S> visitNotEqual(NotEqualNode n, TransferInput<V, S> p) {
    TransferResult<V, S> res = super.visitNotEqual(n, p);

    Node leftN = n.getLeftOperand();
    Node rightN = n.getRightOperand();
    V leftV = p.getValueOfSubNode(leftN);
    V rightV = p.getValueOfSubNode(rightN);

    if (res.containsTwoStores()
        && (NodeUtils.isConstantBoolean(leftN, true)
            || NodeUtils.isConstantBoolean(rightN, true))) {
      S thenStore = res.getElseStore();
      S elseStore = res.getThenStore();
      res = new ConditionalTransferResult<>(res.getResultValue(), thenStore, elseStore);
    }

    // if annotations differ, use the one that is more precise for both
    // sides (and add it to the store if possible)
    res = strengthenAnnotationOfEqualTo(res, leftN, rightN, leftV, rightV, true);
    res = strengthenAnnotationOfEqualTo(res, rightN, leftN, rightV, leftV, true);

    return res;
  }

  /**
   * Refine the annotation of {@code secondNode} if the annotation {@code secondValue} is less
   * precise than {@code firstValue}. This is possible, if {@code secondNode} is an expression that
   * is tracked by the store (e.g., a local variable or a field). Clients usually call this twice
   * with {@code firstNode} and {@code secondNode} reversed, to refine each of them.
   *
   * <p>Note that when overriding this method, when a new type is inserted into the store, {@link
   * #splitAssignments} should be called, and the new type should be inserted into the store for
   * each of the resulting nodes.
   *
   * @param firstNode the node that might be more precise
   * @param secondNode the node whose type to possibly refine
   * @param firstValue the abstract value that might be more precise
   * @param secondValue the abstract value that might be less precise
   * @param res the previous result
   * @param notEqualTo if true, indicates that the logic is flipped (i.e., the information is added
   *     to the {@code elseStore} instead of the {@code thenStore}) for a not-equal comparison.
   * @return the conditional transfer result (if information has been added), or {@code null}
   */
  protected TransferResult<V, S> strengthenAnnotationOfEqualTo(
      TransferResult<V, S> res,
      Node firstNode,
      Node secondNode,
      V firstValue,
      V secondValue,
      boolean notEqualTo) {
    if (firstValue != null) {
      // Only need to insert if the second value is actually different.
      if (!firstValue.equals(secondValue)) {
        List<Node> secondParts = splitAssignments(secondNode);
        for (Node secondPart : secondParts) {
          JavaExpression secondInternal = JavaExpression.fromNode(secondPart);
          if (!secondInternal.isDeterministic(analysis.atypeFactory)) {
            continue;
          }
          if (CFAbstractStore.canInsertJavaExpression(secondInternal)) {
            S thenStore = res.getThenStore();
            S elseStore = res.getElseStore();
            if (notEqualTo) {
              elseStore.insertValue(secondInternal, firstValue);
            } else {
              thenStore.insertValue(secondInternal, firstValue);
            }
            // To handle `(a = b = c) == x`, repeat for all insertable receivers of
            // splitted assignments instead of returning.
            res = new ConditionalTransferResult<>(res.getResultValue(), thenStore, elseStore);
          }
        }
      }
    }
    return res;
  }

  /**
   * Takes a node, and either returns the node itself again (as a singleton list), or if the node is
   * an assignment node, returns the lhs and rhs (where splitAssignments is applied recursively to
   * the rhs -- that is, the rhs may not appear in the result, but rather its lhs and rhs may).
   *
   * @param node possibly an assignment node
   * @return a list containing all the right- and left-hand sides in the given assignment node; it
   *     contains just the node itself if it is not an assignment)
   */
  protected List<Node> splitAssignments(Node node) {
    if (node instanceof AssignmentNode) {
      List<Node> result = new ArrayList<>(2);
      AssignmentNode a = (AssignmentNode) node;
      result.add(a.getTarget());
      result.addAll(splitAssignments(a.getExpression()));
      return result;
    } else {
      return Collections.singletonList(node);
    }
  }

  @Override
  public TransferResult<V, S> visitAssignment(AssignmentNode n, TransferInput<V, S> in) {
    Node lhs = n.getTarget();
    Node rhs = n.getExpression();

    S info = in.getRegularStore();
    V rhsValue = in.getValueOfSubNode(rhs);

    if (shouldPerformWholeProgramInference(n.getTree(), lhs.getTree())) {
      // Fields defined in interfaces are LocalVariableNodes with ElementKind of FIELD.
      if (lhs instanceof FieldAccessNode
          || (lhs instanceof LocalVariableNode
              && ((LocalVariableNode) lhs).getElement().getKind() == ElementKind.FIELD)) {
        // Updates inferred field type
        analysis
            .atypeFactory
            .getWholeProgramInference()
            .updateFromFieldAssignment(lhs, rhs, analysis.getContainingClass(n.getTree()));
      } else if (lhs instanceof LocalVariableNode
          && ((LocalVariableNode) lhs).getElement().getKind() == ElementKind.PARAMETER) {
        // lhs is a formal parameter of some method
        VariableElement param = (VariableElement) ((LocalVariableNode) lhs).getElement();
        analysis
            .atypeFactory
            .getWholeProgramInference()
            .updateFromFormalParameterAssignment((LocalVariableNode) lhs, rhs, param);
      }
    }

    processCommonAssignment(in, lhs, rhs, info, rhsValue);

    return new RegularTransferResult<>(finishValue(rhsValue, info), info);
  }

  @Override
  public TransferResult<V, S> visitReturn(ReturnNode n, TransferInput<V, S> p) {
    TransferResult<V, S> result = super.visitReturn(n, p);

    if (shouldPerformWholeProgramInference(n.getTree())) {
      // Retrieves class containing the method
      ClassTree classTree = analysis.getContainingClass(n.getTree());
      // classTree is null e.g. if this is a return statement in a lambda.
      if (classTree == null) {
        return result;
      }
      ClassSymbol classSymbol = (ClassSymbol) TreeUtils.elementFromTree(classTree);

      ExecutableElement methodElem =
          TreeUtils.elementFromDeclaration(analysis.getContainingMethod(n.getTree()));

      Map<AnnotatedDeclaredType, ExecutableElement> overriddenMethods =
          AnnotatedTypes.overriddenMethods(
              analysis.atypeFactory.getElementUtils(), analysis.atypeFactory, methodElem);

      // Updates the inferred return type of the method
      analysis
          .atypeFactory
          .getWholeProgramInference()
          .updateFromReturn(
              n, classSymbol, analysis.getContainingMethod(n.getTree()), overriddenMethods);
    }

    return result;
  }

  @Override
  public TransferResult<V, S> visitLambdaResultExpression(
      LambdaResultExpressionNode n, TransferInput<V, S> in) {
    return n.getResult().accept(this, in);
  }

  @Override
  public TransferResult<V, S> visitStringConcatenateAssignment(
      StringConcatenateAssignmentNode n, TransferInput<V, S> in) {
    // This gets the type of LHS + RHS
    TransferResult<V, S> result = super.visitStringConcatenateAssignment(n, in);
    Node lhs = n.getLeftOperand();
    Node rhs = n.getRightOperand();

    // update the results store if the assignment target is something we can process
    S info = result.getRegularStore();
    // ResultValue is the type of LHS + RHS
    V resultValue = result.getResultValue();

    if (lhs instanceof FieldAccessNode
        && shouldPerformWholeProgramInference(n.getTree(), lhs.getTree())) {
      // Updates inferred field type
      analysis
          .atypeFactory
          .getWholeProgramInference()
          .updateFromFieldAssignment(
              (FieldAccessNode) lhs, rhs, analysis.getContainingClass(n.getTree()));
    }

    processCommonAssignment(in, lhs, rhs, info, resultValue);

    return new RegularTransferResult<>(finishValue(resultValue, info), info);
  }

  /**
   * Determine abstract value of right-hand side and update the store accordingly to the assignment.
   */
  protected void processCommonAssignment(
      TransferInput<V, S> in, Node lhs, Node rhs, S info, V rhsValue) {

    // update information in the store
    info.updateForAssignment(lhs, rhsValue);
  }

  @Override
  public TransferResult<V, S> visitObjectCreation(ObjectCreationNode n, TransferInput<V, S> p) {
    if (shouldPerformWholeProgramInference(n.getTree())) {
      ExecutableElement constructorElt =
          analysis.getTypeFactory().constructorFromUse(n.getTree()).executableType.getElement();
      analysis
          .atypeFactory
          .getWholeProgramInference()
          .updateFromObjectCreation(n, constructorElt, p.getRegularStore());
    }
    return super.visitObjectCreation(n, p);
  }

  @Override
  public TransferResult<V, S> visitMethodInvocation(
      MethodInvocationNode n, TransferInput<V, S> in) {

    S store = in.getRegularStore();
    ExecutableElement method = n.getTarget().getMethod();

    // Perform WPI before the store has been side-effected.
    if (shouldPerformWholeProgramInference(n.getTree(), method)) {
      // Updates the inferred parameter types of the invoked method.
      analysis.atypeFactory.getWholeProgramInference().updateFromMethodInvocation(n, method, store);
    }

    Tree invocationTree = n.getTree();

    // Determine the abstract value for the method call.
    // look up the call's value from factory
    V factoryValue = (invocationTree == null) ? null : getValueFromFactory(invocationTree, n);
    // look up the call's value in the store (if possible)
    V storeValue = store.getValue(n);
    V resValue = moreSpecificValue(factoryValue, storeValue);

    store.updateForMethodCall(n, analysis.atypeFactory, resValue);

    // add new information based on postcondition
    processPostconditions(n, store, method, invocationTree);

    S thenStore = store;
    S elseStore = thenStore.copy();

    // add new information based on conditional postcondition
    processConditionalPostconditions(n, method, invocationTree, thenStore, elseStore);

    return new ConditionalTransferResult<>(
        finishValue(resValue, thenStore, elseStore), thenStore, elseStore);
  }

  @Override
  public TransferResult<V, S> visitInstanceOf(InstanceOfNode node, TransferInput<V, S> in) {
    TransferResult<V, S> result = super.visitInstanceOf(node, in);
    // The "reference type" is the type after "instanceof".
    Tree refTypeTree = node.getTree().getType();
    if (refTypeTree.getKind() == Tree.Kind.ANNOTATED_TYPE) {
      AnnotatedTypeMirror refType = analysis.atypeFactory.getAnnotatedType(refTypeTree);
      AnnotatedTypeMirror expType =
          analysis.atypeFactory.getAnnotatedType(node.getTree().getExpression());
      if (analysis.atypeFactory.getTypeHierarchy().isSubtype(refType, expType)
          && !refType.getAnnotations().equals(expType.getAnnotations())
          && !expType.getAnnotations().isEmpty()) {
        JavaExpression expr = JavaExpression.fromTree(node.getTree().getExpression());
        for (AnnotationMirror anno : refType.getAnnotations()) {
          in.getRegularStore().insertOrRefine(expr, anno);
        }
        return new RegularTransferResult<>(result.getResultValue(), in.getRegularStore());
      }
    }
    return result;
  }

  /**
   * Returns true if whole-program inference should be performed. If the tree is in the scope of
   * a @SuppressWarnings, then this method returns false.
   *
   * @param tree a tree
   * @return whether to perform whole-program inference on the tree
   */
  private boolean shouldPerformWholeProgramInference(Tree tree) {
    return infer && (tree == null || !analysis.checker.shouldSuppressWarnings(tree, ""));
  }

  /**
   * Returns true if whole-program inference should be performed. If the expressionTree or lhsTree
   * is in the scope of a @SuppressWarnings, then this method returns false.
   *
   * @param expressionTree the right-hand side of an assignment
   * @param lhsTree the left-hand side of an assignment
   * @return whether to perform whole-program inference
   */
  private boolean shouldPerformWholeProgramInference(Tree expressionTree, Tree lhsTree) {
    // Check that infer is true and the tree isn't in scope of a @SuppressWarnings
    // before calling InternalUtils.symbol(lhs).
    if (!shouldPerformWholeProgramInference(expressionTree)) {
      return false;
    }
    Element elt = TreeUtils.elementFromTree(lhsTree);
    return !analysis.checker.shouldSuppressWarnings(elt, "");
  }

  /**
   * Returns true if whole-program inference should be performed. If the tree or element is in the
   * scope of a @SuppressWarnings, then this method returns false.
   *
   * @param tree a tree
   * @param elt its element
   * @return whether to perform whole-program inference
   */
  private boolean shouldPerformWholeProgramInference(Tree tree, Element elt) {
    return shouldPerformWholeProgramInference(tree)
        && !analysis.checker.shouldSuppressWarnings(elt, "");
  }

  /**
   * Add information from the postconditions of a method to the store after an invocation.
   *
   * @param invocationNode a method call
   * @param store a store; is side-effected by this method
   * @param methodElement the method being called
   * @param invocationTree the tree for the method call
   */
  protected void processPostconditions(
      MethodInvocationNode invocationNode,
      S store,
      ExecutableElement methodElement,
      Tree invocationTree) {
    ContractsFromMethod contractsUtils = analysis.atypeFactory.getContractsFromMethod();
    Set<Postcondition> postconditions = contractsUtils.getPostconditions(methodElement);
    processPostconditionsAndConditionalPostconditions(
        invocationNode, invocationTree, store, null, postconditions);
  }

  /**
   * Add information from the conditional postconditions of a method to the stores after an
   * invocation.
   *
   * @param invocationNode a method call
   * @param methodElement the method being called
   * @param invocationTree the tree for the method call
   * @param thenStore the "then" store; is side-effected by this method
   * @param elseStore the "else" store; is side-effected by this method
   */
  protected void processConditionalPostconditions(
      MethodInvocationNode invocationNode,
      ExecutableElement methodElement,
      Tree invocationTree,
      S thenStore,
      S elseStore) {
    ContractsFromMethod contractsUtils = analysis.atypeFactory.getContractsFromMethod();
    Set<ConditionalPostcondition> conditionalPostconditions =
        contractsUtils.getConditionalPostconditions(methodElement);
    processPostconditionsAndConditionalPostconditions(
        invocationNode, invocationTree, thenStore, elseStore, conditionalPostconditions);
  }

  /**
   * Add information from the postconditions and conditional postconditions of a method to the
   * stores after an invocation.
   *
   * @param invocationNode a method call
   * @param invocationTree the tree for the method call
   * @param thenStore the "then" store; is side-effected by this method
   * @param elseStore the "else" store; is side-effected by this method
   * @param postconditions the postconditions
   */
  private void processPostconditionsAndConditionalPostconditions(
      MethodInvocationNode invocationNode,
      Tree invocationTree,
      S thenStore,
      S elseStore,
      Set<? extends Contract> postconditions) {

    StringToJavaExpression stringToJavaExpr =
        stringExpr ->
            StringToJavaExpression.atMethodInvocation(stringExpr, invocationNode, analysis.checker);
    for (Contract p : postconditions) {
      // Viewpoint-adapt to the method use (the call site).
      AnnotationMirror anno =
          p.viewpointAdaptDependentTypeAnnotation(
              analysis.atypeFactory, stringToJavaExpr, /*errorTree=*/ null);

      String expressionString = p.expressionString;
      try {
        JavaExpression je = stringToJavaExpr.toJavaExpression(expressionString);

        // "insertOrRefine" is called so that the postcondition information is added to any
        // existing information rather than replacing it.  If the called method is not
        // side-effect-free, then the values that might have been changed by the method call
        // are removed from the store before this method is called.
        if (p.kind == Contract.Kind.CONDITIONALPOSTCONDITION) {
          if (((ConditionalPostcondition) p).resultValue) {
            thenStore.insertOrRefinePermitNondeterministic(je, anno);
          } else {
            elseStore.insertOrRefinePermitNondeterministic(je, anno);
          }
        } else {
          thenStore.insertOrRefinePermitNondeterministic(je, anno);
        }
      } catch (JavaExpressionParseException e) {
        // report errors here
        if (e.isFlowParseError()) {
          Object[] args = new Object[e.args.length + 1];
          args[0] =
              ElementUtils.getSimpleSignature(TreeUtils.elementFromUse(invocationNode.getTree()));
          System.arraycopy(e.args, 0, args, 1, e.args.length);
          analysis.checker.reportError(invocationTree, "flowexpr.parse.error.postcondition", args);
        } else {
          analysis.checker.report(invocationTree, e.getDiagMessage());
        }
      }
    }
  }

  /**
   * A case produces no value, but it may imply some facts about the argument to the switch
   * statement.
   */
  @Override
  public TransferResult<V, S> visitCase(CaseNode n, TransferInput<V, S> in) {
    S store = in.getRegularStore();
    TransferResult<V, S> result =
        new ConditionalTransferResult<>(
            finishValue(null, store), in.getThenStore(), in.getElseStore(), false);

    V caseValue = in.getValueOfSubNode(n.getCaseOperand());
    AssignmentNode assign = (AssignmentNode) n.getSwitchOperand();
    V switchValue = store.getValue(JavaExpression.fromNode(assign.getTarget()));
    result =
        strengthenAnnotationOfEqualTo(
            result, n.getCaseOperand(), assign.getExpression(), caseValue, switchValue, false);

    // Update value of switch temporary variable
    result =
        strengthenAnnotationOfEqualTo(
            result, n.getCaseOperand(), assign.getTarget(), caseValue, switchValue, false);
    return result;
  }

  /**
   * In a cast {@code (@A C) e} of some expression {@code e} to a new type {@code @A C}, we usually
   * take the annotation of the type {@code C} (here {@code @A}). However, if the inferred
   * annotation of {@code e} is more precise, we keep that one.
   */
  // @Override
  // public TransferResult<V, S> visitTypeCast(TypeCastNode n,
  // TransferInput<V, S> p) {
  // TransferResult<V, S> result = super.visitTypeCast(n, p);
  // V value = result.getResultValue();
  // V operandValue = p.getValueOfSubNode(n.getOperand());
  // // Normally we take the value of the type cast node. However, if the old
  // // flow-refined value was more precise, we keep that value.
  // V resultValue = moreSpecificValue(value, operandValue);
  // result.setResultValue(resultValue);
  // return result;
  // }

  /**
   * Returns the abstract value of {@code (value1, value2)} that is more specific. If the two are
   * incomparable, then {@code value1} is returned.
   */
  public V moreSpecificValue(V value1, V value2) {
    if (value1 == null) {
      return value2;
    }
    if (value2 == null) {
      return value1;
    }
    return value1.mostSpecific(value2, value1);
  }

  @Override
  public TransferResult<V, S> visitVariableDeclaration(
      VariableDeclarationNode n, TransferInput<V, S> p) {
    S store = p.getRegularStore();
    return new RegularTransferResult<>(finishValue(null, store), store);
  }

  @Override
  public TransferResult<V, S> visitWideningConversion(
      WideningConversionNode n, TransferInput<V, S> p) {
    TransferResult<V, S> result = super.visitWideningConversion(n, p);
    // Combine annotations from the operand with the wide type
    V operandValue = p.getValueOfSubNode(n.getOperand());
    V widenedValue = getWidenedValue(n.getType(), operandValue);
    result.setResultValue(widenedValue);
    return result;
  }

  /**
   * Returns an abstract value with the given {@code type} and the annotations from {@code
   * annotatedValue}, adapted for narrowing. This is only called at a narrowing conversion.
   *
   * @param type the type to narrow to
   * @param annotatedValue the type to narrow from
   * @return an abstract value with the given {@code type} and the annotations from {@code
   *     annotatedValue}; returns null if {@code annotatedValue} is null
   */
  protected V getNarrowedValue(TypeMirror type, V annotatedValue) {
    if (annotatedValue == null) {
      return null;
    }
    Set<AnnotationMirror> narrowedAnnos =
        analysis.atypeFactory.getNarrowedAnnotations(
            annotatedValue.getAnnotations(),
            annotatedValue.getUnderlyingType().getKind(),
            type.getKind());

    return analysis.createAbstractValue(narrowedAnnos, type);
  }

  /**
   * Returns an abstract value with the given {@code type} and the annotations from {@code
   * annotatedValue}, adapted for widening. This is only called at a widening conversion.
   *
   * @param type the type to widen to
   * @param annotatedValue the type to widen from
   * @return an abstract value with the given {@code type} and the annotations from {@code
   *     annotatedValue}; returns null if {@code annotatedValue} is null
   */
  protected V getWidenedValue(TypeMirror type, V annotatedValue) {
    if (annotatedValue == null) {
      return null;
    }
    Set<AnnotationMirror> widenedAnnos =
        analysis.atypeFactory.getWidenedAnnotations(
            annotatedValue.getAnnotations(),
            annotatedValue.getUnderlyingType().getKind(),
            type.getKind());

    return analysis.createAbstractValue(widenedAnnos, type);
  }

  @Override
  public TransferResult<V, S> visitNarrowingConversion(
      NarrowingConversionNode n, TransferInput<V, S> p) {
    TransferResult<V, S> result = super.visitNarrowingConversion(n, p);
    // Combine annotations from the operand with the narrow type
    V operandValue = p.getValueOfSubNode(n.getOperand());
    V narrowedValue = getNarrowedValue(n.getType(), operandValue);
    result.setResultValue(narrowedValue);
    return result;
  }

  @Override
  public TransferResult<V, S> visitStringConversion(StringConversionNode n, TransferInput<V, S> p) {
    TransferResult<V, S> result = super.visitStringConversion(n, p);
    result.setResultValue(p.getValueOfSubNode(n.getOperand()));
    return result;
  }

  /**
   * Inserts newAnno as the value into all stores (conditional or not) in the result for node. This
   * is a utility method for subclasses.
   *
   * @param result the TransferResult holding the stores to modify
   * @param target the receiver whose value should be modified
   * @param newAnno the new value
   */
  public static void insertIntoStores(
      TransferResult<CFValue, CFStore> result, JavaExpression target, AnnotationMirror newAnno) {
    if (result.containsTwoStores()) {
      result.getThenStore().insertValue(target, newAnno);
      result.getElseStore().insertValue(target, newAnno);
    } else {
      result.getRegularStore().insertValue(target, newAnno);
    }
  }
}