001package daikon.diff;
002
003import daikon.FileIO;
004import daikon.Global;
005import daikon.PptTopLevel;
006import daikon.inv.Invariant;
007import java.io.IOException;
008import java.io.ObjectInputStream;
009import java.io.ObjectOutputStream;
010import java.io.Serializable;
011import java.util.ArrayList;
012import java.util.Collections;
013import java.util.Comparator;
014import java.util.HashMap;
015import java.util.Iterator;
016import java.util.List;
017import java.util.Map;
018import org.checkerframework.checker.lock.qual.GuardSatisfied;
019import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
020import org.checkerframework.checker.nullness.qual.RequiresNonNull;
021import org.checkerframework.dataflow.qual.Pure;
022import org.checkerframework.dataflow.qual.SideEffectFree;
023import org.plumelib.util.CollectionsPlume;
024
025/**
026 * Maps ppts to lists of invariants. Has an iterator to return the ppts in the order they were
027 * inserted.
028 *
029 * <p>The ppts are used only as keys in this data structure. Do not attempt to look up invariants
030 * stored in the ppts; instead, obtain invariants via the get() method.
031 */
032public class InvMap implements Serializable {
033  /** If you add or remove fields, change this number to the current date. */
034  static final long serialVersionUID = 20090612L;
035
036  /** A map from program points to the invariants true at the program point. */
037  @SuppressWarnings("serial")
038  private Map<PptTopLevel, List<Invariant>> pptToInvs = new HashMap<>();
039
040  /**
041   * The purpose of this field is apparently to permit the ppts to be extracted in the same order in
042   * which they were inserted. Why not use a LinkedHashMap? Maybe because it was only added in JDK
043   * 1.4.
044   */
045  @SuppressWarnings("serial")
046  private List<PptTopLevel> ppts = new ArrayList<>();
047
048  public InvMap() {}
049
050  public void addPpt(PptTopLevel ppt) {
051    put(ppt, new ArrayList<Invariant>());
052  }
053
054  public void put(PptTopLevel ppt, List<Invariant> invs) {
055    if (ppts.contains(ppt)) {
056      throw new Error("Tried to add duplicate PptTopLevel " + ppt.name());
057    }
058    ppts.add(ppt);
059    pptToInvs.put(ppt, invs);
060  }
061
062  public void add(PptTopLevel ppt, Invariant inv) {
063    if (!ppts.contains(ppt)) {
064      throw new Error("ppt has not yet been added: " + ppt.name());
065    }
066    get(ppt).add(inv);
067  }
068
069  public List<Invariant> get(@GuardSatisfied InvMap this, PptTopLevel ppt) {
070    if (!pptToInvs.containsKey(ppt)) {
071      throw new Error("ppt has not yet been added: " + ppt.name());
072    }
073    return pptToInvs.get(ppt);
074  }
075
076  /**
077   * Returns an iterator over the ppts, in the order they were added to the map. Each element is a
078   * PptTopLevel. These ppts are only used as keys: do not look in these Ppts to find the invariants
079   * associated with them in the InvMap! Use invariantIterator instead.
080   *
081   * @see #invariantIterator()
082   */
083  public Iterator<PptTopLevel> pptIterator(@GuardSatisfied InvMap this) {
084    return ppts.iterator();
085  }
086
087  /**
088   * Returns an iterable over the ppts, in the order they were added to the map. Each element is a
089   * PptTopLevel. These ppts are only used as keys: do not look in these Ppts to find the invariants
090   * associated with them in the InvMap! Use invariantIterator instead.
091   *
092   * @see #invariantIterator()
093   */
094  public Iterable<PptTopLevel> pptIterable(@GuardSatisfied InvMap this) {
095    return CollectionsPlume.iteratorToIterable(pptIterator());
096  }
097
098  // Returns a sorted iterator over the Ppts using c as the comparator
099  public Iterator<PptTopLevel> pptSortedIterator(Comparator<PptTopLevel> c) {
100    List<PptTopLevel> ppts_copy = new ArrayList<>(ppts);
101    Collections.sort(ppts_copy, c);
102    return ppts_copy.iterator();
103  }
104
105  /** Returns an iterator over the invariants in this. */
106  // The ppts are in the order added, and the invariants are in the order
107  // added within each ppt, but the order of all invariants is not
108  // necessarily that in which they were added, depending on calling
109  // sequences.
110  public Iterator<Invariant> invariantIterator() {
111    ArrayList<Invariant> answer = new ArrayList<>();
112    for (PptTopLevel ppt : ppts) {
113      answer.addAll(get(ppt));
114    }
115    return answer.iterator();
116  }
117
118  @SideEffectFree
119  @Override
120  public String toString(@GuardSatisfied InvMap this) {
121    String result = "";
122    for (PptTopLevel ppt : pptIterable()) {
123      result += ppt.name() + Global.lineSep;
124      List<Invariant> invs = get(ppt);
125      for (Invariant inv : invs) {
126        result += "  " + inv.format() + Global.lineSep;
127      }
128    }
129    return result;
130  }
131
132  @Pure
133  public int size() {
134    int size1 = ppts.size();
135    int size2 = pptToInvs.size();
136    assert size1 == size2;
137    return size1;
138  }
139
140  /** Include FileIO.new_decl_format in the stream */
141  @RequiresNonNull("daikon.FileIO.new_decl_format")
142  private void writeObject(ObjectOutputStream oos) throws IOException {
143    oos.defaultWriteObject();
144    oos.writeObject(FileIO.new_decl_format);
145  }
146
147  /** Serialize pptmap and FileIO.new_decl_format */
148  @EnsuresNonNull("daikon.FileIO.new_decl_format")
149  private void readObject(ObjectInputStream ois) throws ClassNotFoundException, IOException {
150    ois.defaultReadObject();
151    FileIO.new_decl_format = (Boolean) ois.readObject();
152    // System.out.printf("Restoring new_decl_format to %b%n",
153    //                   FileIO.new_decl_format);
154  }
155}