001package daikon;
002
003import daikon.inv.DiscardCode;
004import daikon.inv.DiscardInfo;
005import daikon.inv.Invariant;
006import daikon.inv.InvariantInfo;
007import java.util.ArrayList;
008import java.util.HashMap;
009import java.util.List;
010import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
011import org.checkerframework.checker.nullness.qual.NonNull;
012
013public final class DiscReasonMap {
014
015  // Key: PptTopLevel name string
016  // Value: HashMap, such that:
017  //    Key: String containing variable names separated by commas,
018  //      e.g. "this.head, this.tail" (names appear in sorted order).
019  //    Value:  list containing DiscardInfo's for all Invariants using
020  //      those variable names in that PptTopLevel.
021  private static HashMap<String, HashMap<String, List<DiscardInfo>>> the_map;
022
023  // This seems to be a gross singleton pattern.
024  static {
025    initialize();
026  }
027
028  private DiscReasonMap() {
029    // Use initialize();
030  }
031
032  @EnsuresNonNull("the_map")
033  public static void initialize() {
034    the_map = new HashMap<>();
035  }
036
037  /**
038   * Adds disc_info to DiscReasonMap's internal data structure, unless a reason already exists for
039   * inv, in which case the old reason is kept and disc_info is discarded.
040   *
041   * <p>Requires: inv != null &and; disc_info != null &and; disc_info.shouldDiscard()
042   */
043  public static void put(Invariant inv, DiscardInfo disc_info) {
044    if (!PrintInvariants.print_discarded_invariants) {
045      return;
046    }
047
048    assert disc_info != null;
049
050    // Let's not keep track of DiscardInfo's from Invariants who have
051    // any repeated variables since we don't expect them to print anyway
052    for (int i = 1; i < inv.ppt.var_infos.length; i++) {
053      if (inv.ppt.var_infos[i] == inv.ppt.var_infos[i - 1]) {
054        return;
055      }
056    }
057
058    if (inv.ppt.var_infos.length == 0) {
059      System.out.println("no var infos");
060      return;
061    }
062    String vars_result = inv.ppt.var_infos[0].name();
063    for (int i = 1; i < inv.ppt.var_infos.length; i++) {
064      vars_result += "," + inv.ppt.var_infos[i].name();
065    }
066    put(vars_result, inv.ppt.parent.name, disc_info);
067  }
068
069  public static void put(Invariant inv, DiscardCode discardCode, String discardString) {
070    if (!PrintInvariants.print_discarded_invariants) {
071      return;
072    }
073
074    put(inv, new DiscardInfo(inv, discardCode, discardString));
075  }
076
077  public static void put(String vars, String ppt, DiscardInfo disc_info) {
078    if (!PrintInvariants.print_discarded_invariants) {
079      return;
080    }
081
082    assert disc_info != null;
083
084    // Get the vars out of inv in our proper format
085    // I should move this var_sorting stuff to a central
086    // place soon since it's being used kind of frequently
087    /*StringTokenizer st = new StringTokenizer(vars, ",");
088    ArrayList<String> temp_vars = new ArrayList();
089    while (st.hasMoreTokens()) {
090      temp_vars.add(st.nextToken());
091    }
092    Collections.sort(temp_vars);
093    String vars_result = "";
094    for (String temp_var : temp_vars) {
095      vars_result += temp_var + ",";
096      }*/
097
098    HashMap<String, List<DiscardInfo>> ppt_hashmap = the_map.get(ppt);
099    if (ppt_hashmap != null) {
100      List<DiscardInfo> disc_infos = ppt_hashmap.get(vars);
101      if (disc_infos != null) {
102        // Check to see if this invariant already has a DiscInfo
103        for (DiscardInfo di : disc_infos) {
104          if (disc_info.className().equals(di.className())) {
105            // We already have a reason for why the Invariant was discarded
106            // Perhaps we could replace it with the new reason, but maybe we
107            // want to be able to "default" to reasons.  i.e., set less specific
108            // reasons at the very end for everything not printed, just in case
109            // some discarded invariants haven't had their reasons set yet.
110            return;
111          }
112        }
113        disc_infos.add(disc_info);
114      } else {
115        List<DiscardInfo> temp = new ArrayList<>(1);
116        temp.add(disc_info);
117        ppt_hashmap.put(vars, temp);
118      }
119    } else {
120      // In case where nothing from this inv's PptTopLevel has been discarded yet
121      HashMap<String, List<DiscardInfo>> new_map = new HashMap<>();
122      List<DiscardInfo> temp = new ArrayList<>();
123      temp.add(disc_info);
124      new_map.put(vars, temp);
125      the_map.put(ppt, new_map);
126    }
127  }
128
129  /**
130   * Requires: vars is given in the form "var1,var2,var3" in ascending alphabetical order with no
131   * spaces &and; invInfo.ppt() != null.
132   *
133   * @return a List of all DiscardInfos di such that &and; the di is for an Invariant from discPpt
134   *     whose class and vars match the params passed into the method call. If the user wishes for
135   *     any of the 3 params to be a wildcard, they can pass that/those param(s) in as null.
136   */
137  public static List<DiscardInfo> returnMatches_from_ppt(InvariantInfo invInfo) {
138    ArrayList<DiscardInfo> result = new ArrayList<>();
139    HashMap<String, List<DiscardInfo>> vars_map_from_ppt = the_map.get(invInfo.ppt());
140
141    if (vars_map_from_ppt == null) {
142      return result;
143    }
144
145    List<DiscardInfo> di_list = new ArrayList<>();
146    if (invInfo.vars() != null) {
147      // The user entered the vars in a specific order, but let's give
148      // them matching invariants that have those vars in any order.
149      @SuppressWarnings("nullness") // because invInfo.vars() != null
150      @NonNull List<String> var_perms = invInfo.var_permutations();
151      for (String var_perm : var_perms) {
152        List<DiscardInfo> temp = vars_map_from_ppt.get(var_perm);
153        if (temp != null) {
154          di_list.addAll(temp);
155        }
156      }
157    } else {
158      di_list = all_vars_tied_from_ppt(invInfo.ppt());
159    }
160
161    for (DiscardInfo di : di_list) {
162      String shortName =
163          di.className()
164              .substring(di.className().lastIndexOf('.') + 1); // chop off hierarchical info
165      if ((invInfo.className() == null)
166          || invInfo.className().equals(di.className())
167          || invInfo.className().equals(shortName)) {
168        result.add(di);
169      }
170    }
171    return result;
172  }
173
174  // Helper function used to combine all the DiscardInfo lists associated
175  // with a set of vars at a ppt.  Only called when we know ppt has at
176  // least 1 DiscardInfo associated with it.
177  private static List<DiscardInfo> all_vars_tied_from_ppt(String ppt) {
178    @SuppressWarnings("nullness") // map:  method precondition
179    @NonNull HashMap<String, List<DiscardInfo>> vars_map = the_map.get(ppt);
180    assert vars_map != null;
181
182    ArrayList<DiscardInfo> result = new ArrayList<>();
183    for (List<DiscardInfo> ldi : vars_map.values()) {
184      result.addAll(ldi);
185    }
186    return result;
187  }
188
189  /** Prints out all vars from ppt that have DiscardInfo's in the Set.toString() format. */
190  public static void debugVarMap(String ppt) {
191    System.out.println();
192    System.out.println();
193    System.out.println("DEBUGGING PPT: " + ppt);
194    HashMap<String, List<DiscardInfo>> vars_map = the_map.get(ppt);
195    if (vars_map == null) {
196      System.out.println("No reasons for this ppt");
197      return;
198    }
199    System.out.println(vars_map.keySet().toString());
200  }
201}