package org.checkerframework.framework.flow;

import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.StringJoiner;
import java.util.concurrent.atomic.AtomicLong;
import java.util.function.BinaryOperator;
import javax.lang.model.element.AnnotationMirror;
import javax.lang.model.element.Element;
import javax.lang.model.element.ExecutableElement;
import javax.lang.model.element.Name;
import javax.lang.model.type.TypeMirror;
import javax.lang.model.util.Types;
import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.dataflow.analysis.Store;
import org.checkerframework.dataflow.cfg.node.ArrayAccessNode;
import org.checkerframework.dataflow.cfg.node.FieldAccessNode;
import org.checkerframework.dataflow.cfg.node.LocalVariableNode;
import org.checkerframework.dataflow.cfg.node.MethodInvocationNode;
import org.checkerframework.dataflow.cfg.node.Node;
import org.checkerframework.dataflow.cfg.node.ThisNode;
import org.checkerframework.dataflow.cfg.visualize.CFGVisualizer;
import org.checkerframework.dataflow.cfg.visualize.StringCFGVisualizer;
import org.checkerframework.dataflow.expression.ArrayAccess;
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.MethodCall;
import org.checkerframework.dataflow.expression.ThisReference;
import org.checkerframework.dataflow.qual.SideEffectFree;
import org.checkerframework.dataflow.util.PurityUtils;
import org.checkerframework.framework.qual.MonotonicQualifier;
import org.checkerframework.framework.type.AnnotatedTypeFactory;
import org.checkerframework.framework.type.GenericAnnotatedTypeFactory;
import org.checkerframework.javacutil.AnnotationBuilder;
import org.checkerframework.javacutil.AnnotationUtils;
import org.checkerframework.javacutil.BugInCF;
import org.checkerframework.javacutil.Pair;
import org.plumelib.util.CollectionsPlume;
import org.plumelib.util.ToStringComparator;
import org.plumelib.util.UniqueId;

/**
 * A store for the Checker Framework analysis. It tracks the annotations of memory locations such as
 * local variables and fields.
 *
 * <p>When adding a new field to track values for a code construct (similar to {@code
 * localVariableValues} and {@code thisValue}), it is important to review all constructors and
 * methods in this class for locations where the new field must be handled (such as the copy
 * constructor and {@code clearValue}), as well as all constructors/methods in subclasses of {code
 * CFAbstractStore}. Note that this includes not only overridden methods in the subclasses, but new
 * methods in the subclasses as well. Also check if
 * BaseTypeVisitor#getJavaExpressionContextFromNode(Node) needs to be updated. Failing to do so may
 * result in silent failures that are time consuming to debug.
 */
// TODO: Split this class into two parts: one that is reusable generally and
// one that is specific to the Checker Framework.
public abstract class CFAbstractStore<V extends CFAbstractValue<V>, S extends CFAbstractStore<V, S>>
    implements Store<S>, UniqueId {

  /** The analysis class this store belongs to. */
  protected final CFAbstractAnalysis<V, S, ?> analysis;

  /** Information collected about local variables (including method parameters). */
  protected final Map<LocalVariable, V> localVariableValues;

  /** Information collected about the current object. */
  protected V thisValue;

  /** Information collected about fields, using the internal representation {@link FieldAccess}. */
  protected Map<FieldAccess, V> fieldValues;

  /**
   * Returns information about fields. Clients should not side-effect the returned value, which is
   * aliased to internal state.
   *
   * @return information about fields
   */
  public Map<FieldAccess, V> getFieldValues() {
    return fieldValues;
  }

  /**
   * Information collected about array elements, using the internal representation {@link
   * ArrayAccess}.
   */
  protected Map<ArrayAccess, V> arrayValues;

  /**
   * Information collected about method calls, using the internal representation {@link MethodCall}.
   */
  protected Map<MethodCall, V> methodValues;

  /**
   * Information collected about <i>classname</i>.class values, using the internal representation
   * {@link ClassName}.
   */
  protected Map<ClassName, V> classValues;

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

  /** The unique ID for the next-created object. */
  static final AtomicLong nextUid = new AtomicLong(0);
  /** The unique ID of this object. */
  final transient long uid = nextUid.getAndIncrement();

  @Override
  public long getUid() {
    return uid;
  }

  /* --------------------------------------------------------- */
  /* Initialization */
  /* --------------------------------------------------------- */

  /**
   * Creates a new CFAbstractStore.
   *
   * @param analysis the analysis class this store belongs to
   * @param sequentialSemantics should the analysis use sequential Java semantics?
   */
  protected CFAbstractStore(CFAbstractAnalysis<V, S, ?> analysis, boolean sequentialSemantics) {
    this.analysis = analysis;
    localVariableValues = new HashMap<>();
    thisValue = null;
    fieldValues = new HashMap<>();
    methodValues = new HashMap<>();
    arrayValues = new HashMap<>();
    classValues = new HashMap<>();
    this.sequentialSemantics = sequentialSemantics;
  }

  /** Copy constructor. */
  protected CFAbstractStore(CFAbstractStore<V, S> other) {
    this.analysis = other.analysis;
    localVariableValues = new HashMap<>(other.localVariableValues);
    thisValue = other.thisValue;
    fieldValues = new HashMap<>(other.fieldValues);
    methodValues = new HashMap<>(other.methodValues);
    arrayValues = new HashMap<>(other.arrayValues);
    classValues = new HashMap<>(other.classValues);
    sequentialSemantics = other.sequentialSemantics;
  }

  /**
   * Set the abstract value of a method parameter (only adds the information to the store, does not
   * remove any other knowledge). Any previous information is erased; this method should only be
   * used to initialize the abstract value.
   */
  public void initializeMethodParameter(LocalVariableNode p, @Nullable V value) {
    if (value != null) {
      localVariableValues.put(new LocalVariable(p.getElement()), value);
    }
  }

  /**
   * Set the value of the current object. Any previous information is erased; this method should
   * only be used to initialize the value.
   */
  public void initializeThisValue(AnnotationMirror a, TypeMirror underlyingType) {
    if (a != null) {
      thisValue = analysis.createSingleAnnotationValue(a, underlyingType);
    }
  }

  /**
   * Indicates whether the given method is side-effect-free as far as the current store is
   * concerned. In some cases, a store for a checker allows for other mechanisms to specify whether
   * a method is side-effect-free. For example, unannotated methods may be considered
   * side-effect-free by default.
   *
   * @param atypeFactory the type factory used to retrieve annotations on the method element
   * @param method the method element
   * @return whether the method is side-effect-free
   */
  protected boolean isSideEffectFree(AnnotatedTypeFactory atypeFactory, ExecutableElement method) {
    return PurityUtils.isSideEffectFree(atypeFactory, method);
  }

  /* --------------------------------------------------------- */
  /* Handling of fields */
  /* --------------------------------------------------------- */

  /**
   * Remove any information that might not be valid any more after a method call, and add
   * information guaranteed by the method.
   *
   * <ol>
   *   <li>If the method is side-effect-free (as indicated by {@link
   *       org.checkerframework.dataflow.qual.SideEffectFree} or {@link
   *       org.checkerframework.dataflow.qual.Pure}), then no information needs to be removed.
   *   <li>Otherwise, all information about field accesses {@code a.f} needs to be removed, except
   *       if the method {@code n} cannot modify {@code a.f} (e.g., if {@code a} is a local variable
   *       or {@code this}, and {@code f} is final).
   *   <li>Furthermore, if the field has a monotonic annotation, then its information can also be
   *       kept.
   * </ol>
   *
   * Furthermore, if the method is deterministic, we store its result {@code val} in the store.
   */
  public void updateForMethodCall(
      MethodInvocationNode n, AnnotatedTypeFactory atypeFactory, V val) {
    ExecutableElement method = n.getTarget().getMethod();

    // case 1: remove information if necessary
    if (!(analysis.checker.hasOption("assumeSideEffectFree")
        || analysis.checker.hasOption("assumePure")
        || isSideEffectFree(atypeFactory, method))) {

      boolean sideEffectsUnrefineAliases =
          ((GenericAnnotatedTypeFactory) atypeFactory).sideEffectsUnrefineAliases;

      // update local variables
      // TODO: Also remove if any element/argument to the annotation is not
      // isUnmodifiableByOtherCode.  Example: @KeyFor("valueThatCanBeMutated").
      if (sideEffectsUnrefineAliases) {
        localVariableValues.entrySet().removeIf(e -> !e.getKey().isUnmodifiableByOtherCode());
      }

      // update this value
      if (sideEffectsUnrefineAliases) {
        thisValue = null;
      }

      // update field values
      if (sideEffectsUnrefineAliases) {
        fieldValues.entrySet().removeIf(e -> !e.getKey().isUnmodifiableByOtherCode());
      } else {
        Map<FieldAccess, V> newFieldValues =
            new HashMap<>(CollectionsPlume.mapCapacity(fieldValues));
        for (Map.Entry<FieldAccess, V> e : fieldValues.entrySet()) {
          FieldAccess fieldAccess = e.getKey();
          V otherVal = e.getValue();

          // case 3: the field has a monotonic annotation
          if (!((GenericAnnotatedTypeFactory<?, ?, ?, ?>) atypeFactory)
              .getSupportedMonotonicTypeQualifiers()
              .isEmpty()) {
            List<Pair<AnnotationMirror, AnnotationMirror>> fieldAnnotations =
                atypeFactory.getAnnotationWithMetaAnnotation(
                    fieldAccess.getField(), MonotonicQualifier.class);
            V newOtherVal = null;
            for (Pair<AnnotationMirror, AnnotationMirror> fieldAnnotation : fieldAnnotations) {
              AnnotationMirror monotonicAnnotation = fieldAnnotation.second;
              @SuppressWarnings("deprecation") // permitted for use in the framework
              Name annotation =
                  AnnotationUtils.getElementValueClassName(monotonicAnnotation, "value", false);
              AnnotationMirror target =
                  AnnotationBuilder.fromName(atypeFactory.getElementUtils(), annotation);
              // Make sure the 'target' annotation is present.
              if (AnnotationUtils.containsSame(otherVal.getAnnotations(), target)) {
                newOtherVal =
                    analysis
                        .createSingleAnnotationValue(target, otherVal.getUnderlyingType())
                        .mostSpecific(newOtherVal, null);
              }
            }
            if (newOtherVal != null) {
              // keep information for all hierarchies where we had a
              // monotone annotation.
              newFieldValues.put(fieldAccess, newOtherVal);
              continue;
            }
          }

          // case 2:
          if (!fieldAccess.isUnassignableByOtherCode()) {
            continue; // remove information completely
          }

          // keep information
          newFieldValues.put(fieldAccess, otherVal);
        }
        fieldValues = newFieldValues;
      }

      // update array values
      arrayValues.clear();

      // update method values
      methodValues.keySet().removeIf(e -> !e.isUnmodifiableByOtherCode());
    }

    // store information about method call if possible
    JavaExpression methodCall = JavaExpression.fromNode(n);
    replaceValue(methodCall, val);
  }

  /**
   * Add the annotation {@code a} for the expression {@code expr} (correctly deciding where to store
   * the information depending on the type of the expression {@code expr}).
   *
   * <p>This method does not take care of removing other information that might be influenced by
   * changes to certain parts of the state.
   *
   * <p>If there is already a value {@code v} present for {@code expr}, then the stronger of the new
   * and old value are taken (according to the lattice). Note that this happens per hierarchy, and
   * if the store already contains information about a hierarchy other than {@code a}s hierarchy,
   * that information is preserved.
   *
   * <p>If {@code expr} is nondeterministic, this method does not insert {@code value} into the
   * store.
   *
   * @param expr an expression
   * @param a an annotation for the expression
   */
  public void insertValue(JavaExpression expr, AnnotationMirror a) {
    insertValue(expr, analysis.createSingleAnnotationValue(a, expr.getType()));
  }

  /**
   * Like {@link #insertValue(JavaExpression, AnnotationMirror)}, but permits nondeterministic
   * expressions to be stored.
   *
   * <p>For an explanation of when to permit nondeterministic expressions, see {@link
   * #insertValuePermitNondeterministic(JavaExpression, CFAbstractValue)}.
   *
   * @param expr an expression
   * @param a an annotation for the expression
   */
  public void insertValuePermitNondeterministic(JavaExpression expr, AnnotationMirror a) {
    insertValuePermitNondeterministic(
        expr, analysis.createSingleAnnotationValue(a, expr.getType()));
  }

  /**
   * Add the annotation {@code newAnno} for the expression {@code expr} (correctly deciding where to
   * store the information depending on the type of the expression {@code expr}).
   *
   * <p>This method does not take care of removing other information that might be influenced by
   * changes to certain parts of the state.
   *
   * <p>If there is already a value {@code v} present for {@code expr}, then the greatest lower
   * bound of the new and old value is inserted into the store.
   *
   * <p>Note that this happens per hierarchy, and if the store already contains information about a
   * hierarchy other than {@code newAnno}'s hierarchy, that information is preserved.
   *
   * <p>If {@code expr} is nondeterministic, this method does not insert {@code value} into the
   * store.
   *
   * @param expr an expression
   * @param newAnno the expression's annotation
   */
  public final void insertOrRefine(JavaExpression expr, AnnotationMirror newAnno) {
    insertOrRefine(expr, newAnno, false);
  }

  /**
   * Like {@link #insertOrRefine(JavaExpression, AnnotationMirror)}, but permits nondeterministic
   * expressions to be inserted.
   *
   * <p>For an explanation of when to permit nondeterministic expressions, see {@link
   * #insertValuePermitNondeterministic(JavaExpression, CFAbstractValue)}.
   *
   * @param expr an expression
   * @param newAnno the expression's annotation
   */
  public final void insertOrRefinePermitNondeterministic(
      JavaExpression expr, AnnotationMirror newAnno) {
    insertOrRefine(expr, newAnno, true);
  }

  /**
   * Helper function for {@link #insertOrRefine(JavaExpression, AnnotationMirror)} and {@link
   * #insertOrRefinePermitNondeterministic}.
   *
   * @param expr an expression
   * @param newAnno the expression's annotation
   * @param permitNondeterministic whether nondeterministic expressions may be inserted into the
   *     store
   */
  protected void insertOrRefine(
      JavaExpression expr, AnnotationMirror newAnno, boolean permitNondeterministic) {
    if (!canInsertJavaExpression(expr)) {
      return;
    }
    if (!(permitNondeterministic || expr.isDeterministic(analysis.getTypeFactory()))) {
      return;
    }

    V newValue = analysis.createSingleAnnotationValue(newAnno, expr.getType());
    V oldValue = getValue(expr);
    if (oldValue == null) {
      insertValue(
          expr,
          analysis.createSingleAnnotationValue(newAnno, expr.getType()),
          permitNondeterministic);
      return;
    }
    computeNewValueAndInsert(
        expr, newValue, CFAbstractValue<V>::greatestLowerBound, permitNondeterministic);
  }

  /** Returns true if {@code expr} can be stored in this store. */
  public static boolean canInsertJavaExpression(JavaExpression expr) {
    if (expr instanceof FieldAccess
        || expr instanceof ThisReference
        || expr instanceof LocalVariable
        || expr instanceof MethodCall
        || expr instanceof ArrayAccess
        || expr instanceof ClassName) {
      return !expr.containsUnknown();
    }
    return false;
  }

  /**
   * Add the abstract value {@code value} for the expression {@code expr} (correctly deciding where
   * to store the information depending on the type of the expression {@code expr}).
   *
   * <p>This method does not take care of removing other information that might be influenced by
   * changes to certain parts of the state.
   *
   * <p>If there is already a value {@code v} present for {@code expr}, then the stronger of the new
   * and old value are taken (according to the lattice). Note that this happens per hierarchy, and
   * if the store already contains information about a hierarchy for which {@code value} does not
   * contain information, then that information is preserved.
   *
   * <p>If {@code expr} is nondeterministic, this method does not insert {@code value} into the
   * store.
   *
   * @param expr the expression to insert in the store
   * @param value the value of the expression
   */
  public final void insertValue(JavaExpression expr, @Nullable V value) {
    insertValue(expr, value, false);
  }
  /**
   * Like {@link #insertValue(JavaExpression, CFAbstractValue)}, but updates the store even if
   * {@code expr} is nondeterministic.
   *
   * <p>Usually, nondeterministic JavaExpressions should not be stored in a Store. For example, in
   * the body of {@code if (nondet() == 3) {...}}, the store should not record that the value of
   * {@code nondet()} is 3, because it might not be 3 the next time {@code nondet()} is executed.
   *
   * <p>However, contracts can mention a nondeterministic JavaExpression. For example, a contract
   * might have a postcondition that{@code nondet()} is odd. This means that the next call to{@code
   * nondet()} will return odd. Such a postcondition may be evicted from the store by calling a
   * side-effecting method.
   *
   * @param expr the expression to insert in the store
   * @param value the value of the expression
   */
  public final void insertValuePermitNondeterministic(JavaExpression expr, @Nullable V value) {
    insertValue(expr, value, true);
  }

  /**
   * Returns true if the given (expression, value) pair can be inserted in the store, namely if the
   * value is non-null and the expression does not contain unknown or a nondeterministic expression.
   *
   * <p>This method returning true does not guarantee that the value will be inserted; the
   * implementation of {@link #insertValue( JavaExpression, CFAbstractValue, boolean)} might still
   * not insert it.
   *
   * @param expr the expression to insert in the store
   * @param value the value of the expression
   * @param permitNondeterministic if false, returns false if {@code expr} is nondeterministic; if
   *     true, permits nondeterministic expressions to be placed in the store
   * @return true if the given (expression, value) pair can be inserted in the store
   */
  @EnsuresNonNullIf(expression = "#2", result = true)
  protected boolean shouldInsert(
      JavaExpression expr, @Nullable V value, boolean permitNondeterministic) {
    if (value == null) {
      // No need to insert a null abstract value because it represents
      // top and top is also the default value.
      return false;
    }
    if (expr.containsUnknown()) {
      // Expressions containing unknown expressions are not stored.
      return false;
    }
    if (!(permitNondeterministic || expr.isDeterministic(analysis.getTypeFactory()))) {
      // Nondeterministic expressions may not be stored.
      // (They are likely to be quickly evicted, as soon as a side-effecting method is called.)
      return false;
    }
    return true;
  }

  /**
   * Helper method for {@link #insertValue(JavaExpression, CFAbstractValue)} and {@link
   * #insertValuePermitNondeterministic}.
   *
   * <p>Every overriding implementation should start with
   *
   * <pre>{@code
   * if (!shouldInsert) {
   *   return;
   * }
   * }</pre>
   *
   * @param expr the expression to insert in the store
   * @param value the value of the expression
   * @param permitNondeterministic if false, does nothing if {@code expr} is nondeterministic; if
   *     true, permits nondeterministic expressions to be placed in the store
   */
  protected void insertValue(
      JavaExpression expr, @Nullable V value, boolean permitNondeterministic) {
    computeNewValueAndInsert(
        expr, value, (old, newValue) -> newValue.mostSpecific(old, null), permitNondeterministic);
  }

  /**
   * Inserts the result of applying {@code merger} to {@code value} and the previous value for
   * {@code expr}.
   *
   * @param expr the JavaExpression
   * @param value the value of the JavaExpression
   * @param merger the function used to merge {@code value} and the previous value of {@code expr}
   * @param permitNondeterministic if false, does nothing if {@code expr} is nondeterministic; if
   *     true, permits nondeterministic expressions to be placed in the store
   */
  protected void computeNewValueAndInsert(
      JavaExpression expr,
      @Nullable V value,
      BinaryOperator<V> merger,
      boolean permitNondeterministic) {
    if (!shouldInsert(expr, value, permitNondeterministic)) {
      return;
    }

    if (expr instanceof LocalVariable) {
      LocalVariable localVar = (LocalVariable) expr;
      V oldValue = localVariableValues.get(localVar);
      V newValue = merger.apply(oldValue, value);
      if (newValue != null) {
        localVariableValues.put(localVar, newValue);
      }
    } else if (expr instanceof FieldAccess) {
      FieldAccess fieldAcc = (FieldAccess) expr;
      // Only store information about final fields (where the receiver is
      // also fixed) if concurrent semantics are enabled.
      boolean isMonotonic = isMonotonicUpdate(fieldAcc, value);
      if (sequentialSemantics || isMonotonic || fieldAcc.isUnassignableByOtherCode()) {
        V oldValue = fieldValues.get(fieldAcc);
        V newValue = merger.apply(oldValue, value);
        if (newValue != null) {
          fieldValues.put(fieldAcc, newValue);
        }
      }
    } else if (expr instanceof MethodCall) {
      MethodCall method = (MethodCall) expr;
      // Don't store any information if concurrent semantics are enabled.
      if (sequentialSemantics) {
        V oldValue = methodValues.get(method);
        V newValue = merger.apply(oldValue, value);
        if (newValue != null) {
          methodValues.put(method, newValue);
        }
      }
    } else if (expr instanceof ArrayAccess) {
      ArrayAccess arrayAccess = (ArrayAccess) expr;
      if (sequentialSemantics) {
        V oldValue = arrayValues.get(arrayAccess);
        V newValue = merger.apply(oldValue, value);
        if (newValue != null) {
          arrayValues.put(arrayAccess, newValue);
        }
      }
    } else if (expr instanceof ThisReference) {
      ThisReference thisRef = (ThisReference) expr;
      if (sequentialSemantics || thisRef.isUnassignableByOtherCode()) {
        V oldValue = thisValue;
        V newValue = merger.apply(oldValue, value);
        if (newValue != null) {
          thisValue = newValue;
        }
      }
    } else if (expr instanceof ClassName) {
      ClassName className = (ClassName) expr;
      if (sequentialSemantics || className.isUnassignableByOtherCode()) {
        V oldValue = classValues.get(className);
        V newValue = merger.apply(oldValue, value);
        if (newValue != null) {
          classValues.put(className, newValue);
        }
      }
    } else {
      // No other types of expressions need to be stored.
    }
  }

  /**
   * Return true if fieldAcc is an update of a monotonic qualifier to its target qualifier.
   * (e.g. @MonotonicNonNull to @NonNull). Always returns false if {@code sequentialSemantics} is
   * true.
   *
   * @return true if fieldAcc is an update of a monotonic qualifier to its target qualifier
   *     (e.g. @MonotonicNonNull to @NonNull)
   */
  protected boolean isMonotonicUpdate(FieldAccess fieldAcc, V value) {
    if (analysis.atypeFactory.getSupportedMonotonicTypeQualifiers().isEmpty()) {
      return false;
    }
    boolean isMonotonic = false;
    // TODO: This check for !sequentialSemantics is an optimization that breaks the contract of
    // the method, since the method name and documentation say nothing about sequential
    // semantics.  This check should be performed by callers of this method when needed.
    // TODO: Update the javadoc of this method when the above to-do item is addressed.
    if (!sequentialSemantics) { // only compute if necessary
      AnnotatedTypeFactory atypeFactory = this.analysis.atypeFactory;
      List<Pair<AnnotationMirror, AnnotationMirror>> fieldAnnotations =
          atypeFactory.getAnnotationWithMetaAnnotation(
              fieldAcc.getField(), MonotonicQualifier.class);
      for (Pair<AnnotationMirror, AnnotationMirror> fieldAnnotation : fieldAnnotations) {
        AnnotationMirror monotonicAnnotation = fieldAnnotation.second;
        @SuppressWarnings("deprecation") // permitted for use in the framework
        Name annotation =
            AnnotationUtils.getElementValueClassName(monotonicAnnotation, "value", false);
        AnnotationMirror target =
            AnnotationBuilder.fromName(atypeFactory.getElementUtils(), annotation);
        // Make sure the 'target' annotation is present.
        if (AnnotationUtils.containsSame(value.getAnnotations(), target)) {
          isMonotonic = true;
          break;
        }
      }
    }
    return isMonotonic;
  }

  public void insertThisValue(AnnotationMirror a, TypeMirror underlyingType) {
    if (a == null) {
      return;
    }

    V value = analysis.createSingleAnnotationValue(a, underlyingType);

    V oldValue = thisValue;
    V newValue = value.mostSpecific(oldValue, null);
    if (newValue != null) {
      thisValue = newValue;
    }
  }

  /**
   * Completely replaces the abstract value {@code value} for the expression {@code expr} (correctly
   * deciding where to store the information depending on the type of the expression {@code expr}).
   * Any previous information is discarded.
   *
   * <p>This method does not take care of removing other information that might be influenced by
   * changes to certain parts of the state.
   */
  public void replaceValue(JavaExpression expr, @Nullable V value) {
    clearValue(expr);
    insertValue(expr, value);
  }

  /**
   * Remove any knowledge about the expression {@code expr} (correctly deciding where to remove the
   * information depending on the type of the expression {@code expr}).
   */
  public void clearValue(JavaExpression expr) {
    if (expr.containsUnknown()) {
      // Expressions containing unknown expressions are not stored.
      return;
    }
    if (expr instanceof LocalVariable) {
      LocalVariable localVar = (LocalVariable) expr;
      localVariableValues.remove(localVar);
    } else if (expr instanceof FieldAccess) {
      FieldAccess fieldAcc = (FieldAccess) expr;
      fieldValues.remove(fieldAcc);
    } else if (expr instanceof MethodCall) {
      MethodCall method = (MethodCall) expr;
      methodValues.remove(method);
    } else if (expr instanceof ArrayAccess) {
      ArrayAccess a = (ArrayAccess) expr;
      arrayValues.remove(a);
    } else if (expr instanceof ClassName) {
      ClassName c = (ClassName) expr;
      classValues.remove(c);
    } else { // thisValue ...
      // No other types of expressions are stored.
    }
  }

  /**
   * Returns the current abstract value of a Java expression, or {@code null} if no information is
   * available.
   *
   * @return the current abstract value of a Java expression, or {@code null} if no information is
   *     available
   */
  public @Nullable V getValue(JavaExpression expr) {
    if (expr instanceof LocalVariable) {
      LocalVariable localVar = (LocalVariable) expr;
      return localVariableValues.get(localVar);
    } else if (expr instanceof ThisReference) {
      return thisValue;
    } else if (expr instanceof FieldAccess) {
      FieldAccess fieldAcc = (FieldAccess) expr;
      return fieldValues.get(fieldAcc);
    } else if (expr instanceof MethodCall) {
      MethodCall method = (MethodCall) expr;
      return methodValues.get(method);
    } else if (expr instanceof ArrayAccess) {
      ArrayAccess a = (ArrayAccess) expr;
      return arrayValues.get(a);
    } else if (expr instanceof ClassName) {
      ClassName c = (ClassName) expr;
      return classValues.get(c);
    } else {
      throw new BugInCF("Unexpected JavaExpression: " + expr + " (" + expr.getClass() + ")");
    }
  }

  /**
   * Returns the current abstract value of a field access, or {@code null} if no information is
   * available.
   *
   * @param n the node whose abstract value to return
   * @return the current abstract value of a field access, or {@code null} if no information is
   *     available
   */
  public @Nullable V getValue(FieldAccessNode n) {
    JavaExpression je = JavaExpression.fromNodeFieldAccess(n);
    if (je instanceof FieldAccess) {
      return fieldValues.get((FieldAccess) je);
    } else if (je instanceof ClassName) {
      return classValues.get((ClassName) je);
    } else if (je instanceof ThisReference) {
      // "return thisValue" is wrong, because the node refers to an outer this.
      // So, return null for now.  TODO: improve.
      return null;
    } else {
      throw new BugInCF(
          "Unexpected JavaExpression %s %s for FieldAccessNode %s",
          je.getClass().getSimpleName(), je, n);
    }
  }

  /**
   * Returns the current abstract value of a field access, or {@code null} if no information is
   * available.
   *
   * @param fieldAccess the field access to look up in this store
   * @return current abstract value of a field access, or {@code null} if no information is
   *     available
   */
  public @Nullable V getFieldValue(FieldAccess fieldAccess) {
    return fieldValues.get(fieldAccess);
  }

  /**
   * Returns the current abstract value of a method call, or {@code null} if no information is
   * available.
   *
   * @param n a method call
   * @return the current abstract value of a method call, or {@code null} if no information is
   *     available
   */
  public @Nullable V getValue(MethodInvocationNode n) {
    JavaExpression method = JavaExpression.fromNode(n);
    if (method == null) {
      return null;
    }
    return methodValues.get(method);
  }

  /**
   * Returns the current abstract value of a field access, or {@code null} if no information is
   * available.
   *
   * @param n the node whose abstract value to return
   * @return the current abstract value of a field access, or {@code null} if no information is
   *     available
   */
  public @Nullable V getValue(ArrayAccessNode n) {
    ArrayAccess arrayAccess = JavaExpression.fromArrayAccess(n);
    return arrayValues.get(arrayAccess);
  }

  /**
   * Update the information in the store by considering an assignment with target {@code n}.
   *
   * @param n the left-hand side of an assignment
   * @param val the right-hand value of an assignment
   */
  public void updateForAssignment(Node n, @Nullable V val) {
    JavaExpression je = JavaExpression.fromNode(n);
    if (je instanceof ArrayAccess) {
      updateForArrayAssignment((ArrayAccess) je, val);
    } else if (je instanceof FieldAccess) {
      updateForFieldAccessAssignment((FieldAccess) je, val);
    } else if (je instanceof LocalVariable) {
      updateForLocalVariableAssignment((LocalVariable) je, val);
    } else {
      throw new BugInCF("Unexpected je of class " + je.getClass());
    }
  }

  /**
   * Update the information in the store by considering a field assignment with target {@code n},
   * where the right hand side has the abstract value {@code val}.
   *
   * @param val the abstract value of the value assigned to {@code n} (or {@code null} if the
   *     abstract value is not known).
   */
  protected void updateForFieldAccessAssignment(FieldAccess fieldAccess, @Nullable V val) {
    removeConflicting(fieldAccess, val);
    if (!fieldAccess.containsUnknown() && val != null) {
      // Only store information about final fields (where the receiver is
      // also fixed) if concurrent semantics are enabled.
      if (sequentialSemantics
          || isMonotonicUpdate(fieldAccess, val)
          || fieldAccess.isUnassignableByOtherCode()) {
        fieldValues.put(fieldAccess, val);
      }
    }
  }

  /**
   * Update the information in the store by considering an assignment with target {@code n}, where
   * the target is an array access.
   *
   * <p>See {@link #removeConflicting(ArrayAccess,CFAbstractValue)}, as it is called first by this
   * method.
   */
  protected void updateForArrayAssignment(ArrayAccess arrayAccess, @Nullable V val) {
    removeConflicting(arrayAccess, val);
    if (!arrayAccess.containsUnknown() && val != null) {
      // Only store information about final fields (where the receiver is
      // also fixed) if concurrent semantics are enabled.
      if (sequentialSemantics) {
        arrayValues.put(arrayAccess, val);
      }
    }
  }

  /**
   * Set the abstract value of a local variable in the store. Overwrites any value that might have
   * been available previously.
   *
   * @param val the abstract value of the value assigned to {@code n} (or {@code null} if the
   *     abstract value is not known).
   */
  protected void updateForLocalVariableAssignment(LocalVariable receiver, @Nullable V val) {
    removeConflicting(receiver);
    if (val != null) {
      localVariableValues.put(receiver, val);
    }
  }

  /**
   * Remove any information in this store that might not be true any more after {@code fieldAccess}
   * has been assigned a new value (with the abstract value {@code val}). This includes the
   * following steps (assume that {@code fieldAccess} is of the form <em>a.f</em> for some
   * <em>a</em>.
   *
   * <ol>
   *   <li value="1">Update the abstract value of other field accesses <em>b.g</em> where the field
   *       is equal (that is, <em>f=g</em>), and the receiver <em>b</em> might alias the receiver of
   *       {@code fieldAccess}, <em>a</em>. This update will raise the abstract value for such field
   *       accesses to at least {@code val} (or the old value, if that was less precise). However,
   *       this is only necessary if the field <em>g</em> is not final.
   *   <li value="2">Remove any abstract values for field accesses <em>b.g</em> where {@code
   *       fieldAccess} might alias any expression in the receiver <em>b</em>.
   *   <li value="3">Remove any information about method calls.
   *   <li value="4">Remove any abstract values an array access <em>b[i]</em> where {@code
   *       fieldAccess} might alias any expression in the receiver <em>a</em> or index <em>i</em>.
   * </ol>
   *
   * @param val the abstract value of the value assigned to {@code n} (or {@code null} if the
   *     abstract value is not known).
   */
  protected void removeConflicting(FieldAccess fieldAccess, @Nullable V val) {
    final Iterator<Map.Entry<FieldAccess, V>> fieldValuesIterator =
        fieldValues.entrySet().iterator();
    while (fieldValuesIterator.hasNext()) {
      Map.Entry<FieldAccess, V> entry = fieldValuesIterator.next();
      FieldAccess otherFieldAccess = entry.getKey();
      V otherVal = entry.getValue();
      // case 2:
      if (otherFieldAccess.getReceiver().containsModifiableAliasOf(this, fieldAccess)) {
        fieldValuesIterator.remove(); // remove information completely
      }
      // case 1:
      else if (fieldAccess.getField().equals(otherFieldAccess.getField())) {
        if (canAlias(fieldAccess.getReceiver(), otherFieldAccess.getReceiver())) {
          if (!otherFieldAccess.isFinal()) {
            if (val != null) {
              V newVal = val.leastUpperBound(otherVal);
              entry.setValue(newVal);
            } else {
              // remove information completely
              fieldValuesIterator.remove();
            }
          }
        }
      }
    }

    final Iterator<Map.Entry<ArrayAccess, V>> arrayValuesIterator =
        arrayValues.entrySet().iterator();
    while (arrayValuesIterator.hasNext()) {
      Map.Entry<ArrayAccess, V> entry = arrayValuesIterator.next();
      ArrayAccess otherArrayAccess = entry.getKey();
      if (otherArrayAccess.containsModifiableAliasOf(this, fieldAccess)) {
        // remove information completely
        arrayValuesIterator.remove();
      }
    }

    // case 3:
    methodValues.clear();
  }

  /**
   * Remove any information in the store that might not be true any more after {@code arrayAccess}
   * has been assigned a new value (with the abstract value {@code val}). This includes the
   * following steps (assume that {@code arrayAccess} is of the form <em>a[i]</em> for some
   * <em>a</em>.
   *
   * <ol>
   *   <li value="1">Remove any abstract value for other array access <em>b[j]</em> where <em>a</em>
   *       and <em>b</em> can be aliases, or where either <em>b</em> or <em>j</em> contains a
   *       modifiable alias of <em>a[i]</em>.
   *   <li value="2">Remove any abstract values for field accesses <em>b.g</em> where <em>a[i]</em>
   *       might alias any expression in the receiver <em>b</em> and there is an array expression
   *       somewhere in the receiver.
   *   <li value="3">Remove any information about method calls.
   * </ol>
   *
   * @param val the abstract value of the value assigned to {@code n} (or {@code null} if the
   *     abstract value is not known).
   */
  protected void removeConflicting(ArrayAccess arrayAccess, @Nullable V val) {
    final Iterator<Map.Entry<ArrayAccess, V>> arrayValuesIterator =
        arrayValues.entrySet().iterator();
    while (arrayValuesIterator.hasNext()) {
      Map.Entry<ArrayAccess, V> entry = arrayValuesIterator.next();
      ArrayAccess otherArrayAccess = entry.getKey();
      // case 1:
      if (otherArrayAccess.containsModifiableAliasOf(this, arrayAccess)) {
        arrayValuesIterator.remove(); // remove information completely
      } else if (canAlias(arrayAccess.getArray(), otherArrayAccess.getArray())) {
        // TODO: one could be less strict here, and only raise the abstract
        // value for all array expressions with potentially aliasing receivers.
        arrayValuesIterator.remove(); // remove information completely
      }
    }

    // case 2:
    final Iterator<Map.Entry<FieldAccess, V>> fieldValuesIterator =
        fieldValues.entrySet().iterator();
    while (fieldValuesIterator.hasNext()) {
      Map.Entry<FieldAccess, V> entry = fieldValuesIterator.next();
      FieldAccess otherFieldAccess = entry.getKey();
      JavaExpression otherReceiver = otherFieldAccess.getReceiver();
      if (otherReceiver.containsModifiableAliasOf(this, arrayAccess)
          && otherReceiver.containsOfClass(ArrayAccess.class)) {
        // remove information completely
        fieldValuesIterator.remove();
      }
    }

    // case 3:
    methodValues.clear();
  }

  /**
   * Remove any information in this store that might not be true any more after {@code localVar} has
   * been assigned a new value. This includes the following steps:
   *
   * <ol>
   *   <li value="1">Remove any abstract values for field accesses <em>b.g</em> where {@code
   *       localVar} might alias any expression in the receiver <em>b</em>.
   *   <li value="2">Remove any abstract values for array accesses <em>a[i]</em> where {@code
   *       localVar} might alias the receiver <em>a</em>.
   *   <li value="3">Remove any information about method calls where the receiver or any of the
   *       parameters contains {@code localVar}.
   * </ol>
   */
  protected void removeConflicting(LocalVariable var) {
    final Iterator<Map.Entry<FieldAccess, V>> fieldValuesIterator =
        fieldValues.entrySet().iterator();
    while (fieldValuesIterator.hasNext()) {
      Map.Entry<FieldAccess, V> entry = fieldValuesIterator.next();
      FieldAccess otherFieldAccess = entry.getKey();
      // case 1:
      if (otherFieldAccess.containsSyntacticEqualJavaExpression(var)) {
        fieldValuesIterator.remove();
      }
    }

    final Iterator<Map.Entry<ArrayAccess, V>> arrayValuesIterator =
        arrayValues.entrySet().iterator();
    while (arrayValuesIterator.hasNext()) {
      Map.Entry<ArrayAccess, V> entry = arrayValuesIterator.next();
      ArrayAccess otherArrayAccess = entry.getKey();
      // case 2:
      if (otherArrayAccess.containsSyntacticEqualJavaExpression(var)) {
        arrayValuesIterator.remove();
      }
    }

    final Iterator<Map.Entry<MethodCall, V>> methodValuesIterator =
        methodValues.entrySet().iterator();
    while (methodValuesIterator.hasNext()) {
      Map.Entry<MethodCall, V> entry = methodValuesIterator.next();
      MethodCall otherMethodAccess = entry.getKey();
      // case 3:
      if (otherMethodAccess.containsSyntacticEqualJavaExpression(var)) {
        methodValuesIterator.remove();
      }
    }
  }

  /**
   * Can the objects {@code a} and {@code b} be aliases? Returns a conservative answer (i.e.,
   * returns {@code true} if not enough information is available to determine aliasing).
   */
  @Override
  public boolean canAlias(JavaExpression a, JavaExpression b) {
    TypeMirror tb = b.getType();
    TypeMirror ta = a.getType();
    Types types = analysis.getTypes();
    return types.isSubtype(ta, tb) || types.isSubtype(tb, ta);
  }

  /* --------------------------------------------------------- */
  /* Handling of local variables */
  /* --------------------------------------------------------- */

  /**
   * Returns the current abstract value of a local variable, or {@code null} if no information is
   * available.
   *
   * @return the current abstract value of a local variable, or {@code null} if no information is
   *     available
   */
  public @Nullable V getValue(LocalVariableNode n) {
    Element el = n.getElement();
    return localVariableValues.get(new LocalVariable(el));
  }

  /* --------------------------------------------------------- */
  /* Handling of the current object */
  /* --------------------------------------------------------- */

  /**
   * Returns the current abstract value of the current object, or {@code null} if no information is
   * available.
   *
   * @param n a reference to "this"
   * @return the current abstract value of the current object, or {@code null} if no information is
   *     available
   */
  public @Nullable V getValue(ThisNode n) {
    return thisValue;
  }

  /* --------------------------------------------------------- */
  /* Helper and miscellaneous methods */
  /* --------------------------------------------------------- */

  @SuppressWarnings("unchecked")
  @Override
  public S copy() {
    return analysis.createCopiedStore((S) this);
  }

  @Override
  public S leastUpperBound(S other) {
    return upperBound(other, false);
  }

  @Override
  public S widenedUpperBound(S previous) {
    return upperBound(previous, true);
  }

  private S upperBound(S other, boolean shouldWiden) {
    S newStore = analysis.createEmptyStore(sequentialSemantics);

    for (Map.Entry<LocalVariable, V> e : other.localVariableValues.entrySet()) {
      // local variables that are only part of one store, but not the other are discarded, as one of
      // store implicitly contains 'top' for that variable.
      LocalVariable localVar = e.getKey();
      V thisVal = localVariableValues.get(localVar);
      if (thisVal != null) {
        V otherVal = e.getValue();
        V mergedVal = upperBoundOfValues(otherVal, thisVal, shouldWiden);

        if (mergedVal != null) {
          newStore.localVariableValues.put(localVar, mergedVal);
        }
      }
    }

    // information about the current object
    {
      V otherVal = other.thisValue;
      V myVal = thisValue;
      V mergedVal = myVal == null ? null : upperBoundOfValues(otherVal, myVal, shouldWiden);
      if (mergedVal != null) {
        newStore.thisValue = mergedVal;
      }
    }

    for (Map.Entry<FieldAccess, V> e : other.fieldValues.entrySet()) {
      // information about fields that are only part of one store, but not the other are discarded,
      // as one store implicitly contains 'top' for that field.
      FieldAccess el = e.getKey();
      V thisVal = fieldValues.get(el);
      if (thisVal != null) {
        V otherVal = e.getValue();
        V mergedVal = upperBoundOfValues(otherVal, thisVal, shouldWiden);
        if (mergedVal != null) {
          newStore.fieldValues.put(el, mergedVal);
        }
      }
    }
    for (Map.Entry<ArrayAccess, V> e : other.arrayValues.entrySet()) {
      // information about arrays that are only part of one store, but not the other are discarded,
      // as one store implicitly contains 'top' for that array access.
      ArrayAccess el = e.getKey();
      V thisVal = arrayValues.get(el);
      if (thisVal != null) {
        V otherVal = e.getValue();
        V mergedVal = upperBoundOfValues(otherVal, thisVal, shouldWiden);
        if (mergedVal != null) {
          newStore.arrayValues.put(el, mergedVal);
        }
      }
    }
    for (Map.Entry<MethodCall, V> e : other.methodValues.entrySet()) {
      // information about methods that are only part of one store, but not the other are discarded,
      // as one store implicitly contains 'top' for that field.
      MethodCall el = e.getKey();
      V thisVal = methodValues.get(el);
      if (thisVal != null) {
        V otherVal = e.getValue();
        V mergedVal = upperBoundOfValues(otherVal, thisVal, shouldWiden);
        if (mergedVal != null) {
          newStore.methodValues.put(el, mergedVal);
        }
      }
    }
    for (Map.Entry<ClassName, V> e : other.classValues.entrySet()) {
      ClassName el = e.getKey();
      V thisVal = classValues.get(el);
      if (thisVal != null) {
        V otherVal = e.getValue();
        V mergedVal = upperBoundOfValues(otherVal, thisVal, shouldWiden);
        if (mergedVal != null) {
          newStore.classValues.put(el, mergedVal);
        }
      }
    }
    return newStore;
  }

  private V upperBoundOfValues(V otherVal, V thisVal, boolean shouldWiden) {
    return shouldWiden ? thisVal.widenUpperBound(otherVal) : thisVal.leastUpperBound(otherVal);
  }

  /**
   * Returns true iff this {@link CFAbstractStore} contains a superset of the map entries of the
   * argument {@link CFAbstractStore}. Note that we test the entry keys and values by Java equality,
   * not by any subtype relationship. This method is used primarily to simplify the equals
   * predicate.
   */
  protected boolean supersetOf(CFAbstractStore<V, S> other) {
    for (Map.Entry<LocalVariable, V> e : other.localVariableValues.entrySet()) {
      LocalVariable key = e.getKey();
      V value = localVariableValues.get(key);
      if (value == null || !value.equals(e.getValue())) {
        return false;
      }
    }
    for (Map.Entry<FieldAccess, V> e : other.fieldValues.entrySet()) {
      FieldAccess key = e.getKey();
      V value = fieldValues.get(key);
      if (value == null || !value.equals(e.getValue())) {
        return false;
      }
    }
    for (Map.Entry<ArrayAccess, V> e : other.arrayValues.entrySet()) {
      ArrayAccess key = e.getKey();
      V value = arrayValues.get(key);
      if (value == null || !value.equals(e.getValue())) {
        return false;
      }
    }
    for (Map.Entry<MethodCall, V> e : other.methodValues.entrySet()) {
      MethodCall key = e.getKey();
      V value = methodValues.get(key);
      if (value == null || !value.equals(e.getValue())) {
        return false;
      }
    }
    for (Map.Entry<ClassName, V> e : other.classValues.entrySet()) {
      ClassName key = e.getKey();
      V value = classValues.get(key);
      if (value == null || !value.equals(e.getValue())) {
        return false;
      }
    }
    return true;
  }

  @Override
  public boolean equals(@Nullable Object o) {
    if (o instanceof CFAbstractStore) {
      @SuppressWarnings("unchecked")
      CFAbstractStore<V, S> other = (CFAbstractStore<V, S>) o;
      return this.supersetOf(other) && other.supersetOf(this);
    } else {
      return false;
    }
  }

  @Override
  public int hashCode() {
    // What is a good hash code to use?
    return 22;
  }

  @SideEffectFree
  @Override
  public String toString() {
    return visualize(new StringCFGVisualizer<>());
  }

  @Override
  public String visualize(CFGVisualizer<?, S, ?> viz) {
    /* This cast is guaranteed to be safe, as long as the CFGVisualizer is created by
     * CFGVisualizer<Value, Store, TransferFunction> createCFGVisualizer() of GenericAnnotatedTypeFactory */
    @SuppressWarnings("unchecked")
    CFGVisualizer<V, S, ?> castedViz = (CFGVisualizer<V, S, ?>) viz;
    String internal = internalVisualize(castedViz);
    if (internal.trim().isEmpty()) {
      return this.getClassAndUid() + "()";
    } else {
      return this.getClassAndUid() + "(" + viz.getSeparator() + internal + ")";
    }
  }

  /**
   * Adds a representation of the internal information of this Store to visualizer {@code viz}.
   *
   * @param viz the visualizer
   * @return a representation of the internal information of this {@link Store}
   */
  protected String internalVisualize(CFGVisualizer<V, S, ?> viz) {
    StringJoiner res = new StringJoiner(viz.getSeparator());
    for (Map.Entry<LocalVariable, V> entry : localVariableValues.entrySet()) {
      res.add(viz.visualizeStoreLocalVar(entry.getKey(), entry.getValue()));
    }
    if (thisValue != null) {
      res.add(viz.visualizeStoreThisVal(thisValue));
    }
    for (FieldAccess fa : ToStringComparator.sorted(fieldValues.keySet())) {
      res.add(viz.visualizeStoreFieldVal(fa, fieldValues.get(fa)));
    }
    for (ArrayAccess fa : ToStringComparator.sorted(arrayValues.keySet())) {
      res.add(viz.visualizeStoreArrayVal(fa, arrayValues.get(fa)));
    }
    for (MethodCall fa : ToStringComparator.sorted(methodValues.keySet())) {
      res.add(viz.visualizeStoreMethodVals(fa, methodValues.get(fa)));
    }
    for (ClassName fa : ToStringComparator.sorted(classValues.keySet())) {
      res.add(viz.visualizeStoreClassVals(fa, classValues.get(fa)));
    }
    return res.toString();
  }
}