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}