001package daikon;
002
003import daikon.inv.Invariant;
004import java.util.Arrays;
005import java.util.List;
006import java.util.Set;
007import java.util.logging.Level;
008import java.util.logging.Logger;
009import org.checkerframework.checker.initialization.qual.UnknownInitialization;
010import org.checkerframework.checker.nullness.qual.NonNull;
011import org.checkerframework.checker.nullness.qual.Nullable;
012import org.plumelib.util.ArraysPlume;
013
014/**
015 * Debug class used with the logger to create standardized output. It can be setup to track
016 * combinations of classes, program points, and variables. The most common class to track is an
017 * invariant, but any class can be used.
018 *
019 * <p>This allows detailed information about a particular class/ppt/variable combination to be
020 * printed without getting lost in a mass of other information (which is a particular problem in
021 * Daikon due to the volume of data considered).
022 *
023 * <p>Note that each of the three items (class, ppt, variable) must match in order for printing to
024 * occur.
025 */
026public final class Debug {
027
028  /** Debug Logger. */
029  public static final Logger debugTrack = Logger.getLogger("daikon.Debug");
030
031  /**
032   * List of classes for logging. Each name listed is compared to the fully qualified class name. If
033   * it matches (shows up anywhere in the class name) it will be included in debug prints. This is
034   * not a regular expression match
035   *
036   * @see #log(Logger, Class, Ppt, String)
037   */
038  public static String[] debugTrackClass = {
039    // "Bound",
040    // "DynamicConstants",
041    // "EltNonZero",
042    // "EltNonZeroFloat",
043    // "EltOneOf",
044    // "Equality",
045    // "FunctionBinary",
046    // "IntEqual",
047    // "IntGreaterEqual",
048    // "IntGreaterThan",
049    // "IntLessEqual",
050    // "IntLessThan",
051    // "IntNonEqual",
052    // "LinearBinary",
053    // "LowerBound",
054    // "Member",
055    // "NonZero",
056    // "OneOfSequence",
057    // "PptSlice",
058    // "PptSlice2",
059    // "PptSliceEquality",
060    // "PptTopLevel",
061    // "SeqIndexComparison",
062    // "SeqIndexNonEqual",
063    // "SeqIntEqual",
064    // "SeqSeqIntEqual",
065    // "NonZero",
066    // "FunctionBinary",
067    // "OneOfSequence",
068    // "IntLessEqual",
069    // "IntGreaterEqual",
070    // "IntLessThan",
071    // "IntGreaterThan",
072    // "IntNonEqual",
073    // "Member",
074    // "FunctionBinary"
075    // "EltNonZero",
076    // "SeqSeqIntGreaterThan",
077    // "SeqSeqIntLessThan",
078    // "SubSet",
079    // "SuperSet",
080    // "EltOneOf",
081    // "Bound",
082    // "SeqSeqIntLessThan",
083    // "SeqSeqIntGreaterThan",
084    // "OneOf"
085    // "StringEqual",
086    // "StringLessThan",
087    // "StringGreaterThan",
088    // "Modlong_zxy",
089    // "UpperBound",
090  };
091
092  /**
093   * Restrict function binary prints to the specified method. Implementation is in the
094   * FunctionBinary specific log functions. If null, there is no restriction (all function binary
095   * methods are printed). See Functions.java for a list of function names.
096   */
097  public static @Nullable String function_binary_method = null
098      // "java.lang.Math.max("
099      // "java.lang.Math.min("
100      // "org.plumelib.util.MathPlume.logicalXor("
101      // "org.plumelib.util.MathPlume.gcd("
102      ;
103
104  /**
105   * List of Ppts for logging. Each name listed is compared to the full program point name. If it
106   * matches (shows up anywhere in the ppt name) it will be included in the debug prints. This is
107   * not a regular expression match.
108   *
109   * @see #log(Logger, Class, Ppt, String)
110   */
111  public static String[] debugTrackPpt = {
112    // "DataStructures.DisjSets.unionDisjoint(int, int):::EXIT",
113    // "DataStructures.StackAr.StackAr(int):::EXIT",
114    // "DataStructures.StackAr.makeEmpty():::EXIT",
115    // "DataStructures.StackAr.makeEmpty()V:::ENTER",
116    // "DataStructures.StackAr.top():::EXIT74",
117    // "GLOBAL",
118    // "std.main(int;char **;)int:::EXIT",
119  };
120
121  /**
122   * List of variable names for logging. Each name listed is compared to each variable in turn. If
123   * each matches exactly it will be included in track debug prints. This is not a regular
124   * expression match. Note that the number of variables must match the slice exactly.
125   *
126   * @see #log(Logger, Class, Ppt, String)
127   */
128  public static String[][] debugTrackVars = {
129    // {"::printstats"},
130    // {"misc.Fib.STEPS", "orig(misc.Fib.a)"},
131    // {"misc.Fib.a", "misc.Fib.STEPS"},
132    // {"return"},
133  };
134
135  // Ordinarily, a client would have to supply a Class, Ppt, and
136  // List<Varinfo> with each call to a log method.  But the client can
137  // instead provide those values once (they are cached in these variables)
138  // and omit them in subsequent calls.  The subsequent calls can use forms
139  // of log() that take fewer arguments.
140
141  /**
142   * True if the cached values should be printed --- that is, they match what is currently being
143   * debugged.
144   */
145  public boolean cache_match = true;
146
147  // Note that throughout this file, inv_class is not necessarily a
148  // subclass of Invariant -- for instance, it might be a subclass of
149  // BinaryDerivationFactory.
150  /** cached class: class to use by default when calling variants of log() with few arguments */
151  public @Nullable Class<?> cache_class;
152
153  /** cached ppt: ppt to use by default when calling variants of log() with few arguments */
154  public @Nullable Ppt cache_ppt;
155
156  /**
157   * Cached variables: variables to use by default when calling variants of log() with few
158   * arguments.
159   */
160  public VarInfo @Nullable [] cache_vis;
161
162  /**
163   * Ordinarily, a client would have to supply a Class, Ppt, and {@code List<Varinfo>} with each
164   * call to a log method. This constructor sets as defaults c, ppt, and whatever variable (if any)
165   * from vis that is on the debugTrackVar list. Essentially this creates a debug object that will
166   * print if any of the variables in vis are being tracked (and c and ppt match).
167   */
168  public Debug(Class<?> c, Ppt ppt, VarInfo[] vis) {
169    set(c, ppt, vis);
170  }
171
172  /**
173   * Returns a Debug object if the specified class, ppt, and vis match what is being tracked.
174   * Otherwise, return NULL. Preferred over calling the constructor directly, since it doesn't
175   * create the object if it doesn't have to.
176   */
177  public static @Nullable Debug newDebug(Class<?> c, Ppt ppt, VarInfo[] vis) {
178    if (logOn() && class_match(c) && ppt_match(ppt) && var_match(vis)) {
179      return new Debug(c, ppt, vis);
180    } else {
181      return null;
182    }
183  }
184
185  /**
186   * Ordinarily, a client would have to supply a Class, Ppt, and {@code List<Varinfo>} with each
187   * call to a log method. This constructor sets as defaults c, ppt, and whatever variable (if any)
188   * from vis that is on the debugTrackVar list. Essentially this creates a debug object that will
189   * print if any of the variables in vis are being tracked (and c and ppt match).
190   */
191  public Debug(Class<?> c, Ppt ppt, List<VarInfo> vis) {
192
193    VarInfo v = visTracked(vis);
194    if (v != null) {
195      set(c, ppt, new VarInfo[] {v});
196    } else if (vis.size() > 0) {
197      set(c, ppt, new VarInfo[] {vis.get(0)});
198    } else {
199      set(c, ppt, null);
200    }
201  }
202
203  /**
204   * Looks for each of the variables in vis in the DebugTrackVar list. If any match, returns that
205   * variable. Returns null if there are no matches.
206   */
207  public @Nullable VarInfo visTracked(@UnknownInitialization Debug this, List<VarInfo> vis) {
208
209    for (VarInfo v : vis) {
210      Set<VarInfo> evars = null;
211      if (v.equalitySet != null) {
212        evars = v.equalitySet.getVars();
213      }
214      if (evars != null) {
215        for (VarInfo ev : evars) {
216          for (int k = 0; k < debugTrackVars.length; k++) {
217            if (ev.name().equals(debugTrackVars[k][0])) {
218              return v;
219            }
220          }
221        }
222      }
223    }
224
225    return null;
226  }
227
228  private static @Nullable String[] ourvars = new String[3];
229
230  private static final VarInfo[] vis1 = new VarInfo[1];
231  private static final VarInfo[] vis2 = new VarInfo[2];
232  private static final VarInfo[] vis3 = new VarInfo[3];
233
234  public static VarInfo[] vis(VarInfo v1) {
235    vis1[0] = v1;
236    return vis1;
237  }
238
239  public static VarInfo[] vis(VarInfo v1, VarInfo v2) {
240    vis2[0] = v1;
241    vis2[1] = v2;
242    return vis2;
243  }
244
245  public static VarInfo[] vis(VarInfo v1, VarInfo v2, VarInfo v3) {
246    vis3[0] = v1;
247    vis3[1] = v2;
248    vis3[2] = v3;
249    return vis3;
250  }
251
252  /**
253   * Sets the cache for class, ppt, and vis so that future calls to log don't have to set them -- in
254   * other words, future calls can use the versions of log with fewer arguments.
255   */
256  void set(
257      @UnknownInitialization Debug this,
258      @Nullable Class<?> c,
259      @Nullable Ppt ppt,
260      VarInfo @Nullable [] vis) {
261    cache_class = c;
262    cache_ppt = ppt;
263    cache_vis = vis;
264    if (c == null) {
265      System.out.println("Class = null");
266    }
267    if (ppt == null) {
268      System.out.println("ppt = null");
269    }
270    if (vis == null) {
271      System.out.println("vis = null");
272    } else {
273      for (int i = 0; i < vis.length; i++) {
274        if (vis[i] == null) System.out.println("vis[" + i + "] == null");
275      }
276    }
277    cache_match = class_match(c) && ppt_match(ppt) && var_match(vis);
278  }
279
280  /**
281   * When true, perform detailed internal checking. These are essentially additional, possibly
282   * costly assert statements.
283   */
284  public static boolean dkconfig_internal_check = false;
285
286  /** If true, show stack traces for errors such as file format errors. */
287  public static boolean dkconfig_show_stack_trace = false;
288
289  /**
290   * Determines whether or not traceback information is printed for each call to log.
291   *
292   * @see #log(Logger, Class, Ppt, String)
293   */
294  public static boolean dkconfig_showTraceback = false;
295
296  /**
297   * Determines whether or not detailed info (such as from {@code add_modified}) is printed.
298   *
299   * @see #log(Logger, Class, Ppt, String)
300   * @see #logDetail()
301   */
302  public static boolean dkconfig_logDetail = false;
303
304  /**
305   * Returns whether or not detailed logging is on. Note that this check is not performed inside the
306   * logging calls themselves, it must be performed by the caller.
307   *
308   * @see #log(Logger, Class, Ppt, String)
309   * @see #logOn()
310   */
311  public static final boolean logDetail() {
312    return dkconfig_logDetail && debugTrack.isLoggable(Level.FINE);
313  }
314
315  /**
316   * Returns whether or not logging is on.
317   *
318   * @see #log(Logger, Class, Ppt, String)
319   */
320  public static final boolean logOn() {
321    return debugTrack.isLoggable(Level.FINE);
322  }
323
324  /**
325   * Logs the cached class, cached ppt, cached variables and the specified msg via the logger as
326   * described in {@link #log(Logger, Class, Ppt, VarInfo[], String)}.
327   */
328  public void log(Logger debug, String msg) {
329    if (cache_match) log(debug, cache_class, cache_ppt, cache_vis, msg);
330  }
331
332  /**
333   * Logs a description of the class, ppt, ppt variables and the specified msg via the logger as
334   * described in {@link #log(Logger, Class, Ppt, VarInfo[], String)}.
335   */
336  public static void log(Logger debug, Class<?> inv_class, @Nullable Ppt ppt, String msg) {
337    if (ppt == null) {
338      log(debug, inv_class, ppt, null, msg);
339    } else {
340      log(debug, inv_class, ppt, ppt.var_infos, msg);
341    }
342  }
343
344  /**
345   * Logs a description of the class, ppt, variables and the specified msg via the logger. The
346   * class, ppt, and variables are checked against those described in {@link #debugTrackClass},
347   * {@link #debugTrackPpt}, and {@link #debugTrackVars}. Only those that match are printed.
348   * Variables will match if they are in the same equality set. The information is written as:
349   *
350   * <p>{@code class: ppt : var1 : var2 : var3 : msg }
351   *
352   * <p>Note that if {@link #debugTrack} is not enabled then nothing is printed. It is somewhat
353   * faster to check {@link #logOn()} directly rather than relying on the check here.
354   *
355   * <p>Other versions of this method (noted below) work without the Logger parameter and take
356   * class, ppt, and vis from the cached values, which were set by the constructor or by the set()
357   * method.
358   *
359   * @param debug a second Logger to query if debug tracking is turned off or does not match. If
360   *     this logger is enabled, the same information will be written to it. Note that the
361   *     information is never written to both loggers.
362   * @param inv_class the class. Can be obtained in a static context by ClassName.class
363   * @param ppt program point
364   * @param vis variables at the program point. These are sometimes different from the ones in the
365   *     ppt itself.
366   * @param msg string message to log
367   * @see #logOn()
368   * @see #logDetail()
369   * @see #log(Class, Ppt, VarInfo[], String)
370   * @see #log(Class, Ppt, String)
371   * @see #log(Logger, String)
372   * @see #log(String)
373   */
374  public static void log(
375      Logger debug,
376      @Nullable Class<?> inv_class,
377      @Nullable Ppt ppt,
378      VarInfo @Nullable [] vis,
379      String msg) {
380
381    // Try to log via the logger first
382    if (log(inv_class, ppt, vis, msg)) {
383      return;
384    }
385
386    // If debug isn't turned on, there is nothing to do
387    if (!debug.isLoggable(Level.FINE)) {
388      return;
389    }
390
391    // Get the non-qualified class name
392    String class_str;
393    if (inv_class == null) {
394      // when is inv_class null?
395      class_str = "null";
396    } else {
397      @SuppressWarnings("nullness") // getPackage(): invariant class always has a package
398      @NonNull String packageName = inv_class.getPackage().getName() + ".";
399      class_str = inv_class.getName().replace(packageName, "");
400    }
401
402    String vars = "";
403    if (vis == null) {
404      System.out.println("no var infos");
405    } else {
406
407      // Get a string with all of the variable names.  Each is separated by ': '
408      // 3 variable slots are always setup for consistency
409      for (VarInfo v : vis) {
410        vars += v.name() + ": ";
411      }
412      for (int i = vis.length; i < 3; i++) {
413        vars += ": ";
414      }
415    }
416
417    // Figure out the sample count if possible
418    String samp_str = "";
419    if (ppt instanceof PptSlice) {
420      PptSlice pslice = (PptSlice) ppt;
421      samp_str = " s" + pslice.num_samples();
422    }
423
424    String line = " line=" + FileIO.get_linenum();
425
426    String name = "ppt is null";
427    if (ppt != null) {
428      name = ppt.name();
429    }
430
431    debug.fine(class_str + ": " + name + samp_str + line + ": " + vars + msg);
432    if (dkconfig_showTraceback) {
433      Throwable stack = new Throwable("debug traceback");
434      stack.fillInStackTrace();
435      stack.printStackTrace();
436    }
437  }
438
439  /**
440   * Logs a description of the cached class, ppt, and variables and the specified msg via the logger
441   * as described in {@link #log(Logger, Class, Ppt, VarInfo[], String)}
442   *
443   * @return whether or not it logged anything
444   */
445  public boolean log(String msg) {
446    if (!logOn()) {
447      return false;
448    }
449    return log(cache_class, cache_ppt, cache_vis, msg);
450  }
451
452  /**
453   * Logs a description of the class, ppt, ppt variables and the specified msg via the logger as
454   * described in {@link #log(Logger, Class, Ppt, VarInfo[], String)}.
455   *
456   * @return whether or not it logged anything
457   */
458  // 3-argument form
459  public static boolean log(
460      Class<?> inv_class, @UnknownInitialization(PptTopLevel.class) Ppt ppt, String msg) {
461
462    return log(inv_class, ppt, ppt.var_infos, msg);
463  }
464
465  /**
466   * Logs a description of the class, ppt, variables and the specified msg via the logger as
467   * described in {@link #log(Logger, Class, Ppt, String)}. Accepts vis because sometimes the
468   * variables are different from those in the ppt.
469   *
470   * @return whether or not it logged anything
471   */
472  // 4-argument form
473  public static boolean log(
474      @Nullable Class<?> inv_class,
475      @Nullable @UnknownInitialization(PptTopLevel.class) Ppt ppt,
476      VarInfo @Nullable [] vis,
477      String msg) {
478
479    if (!debugTrack.isLoggable(Level.FINE)) {
480      return false;
481    }
482
483    // Make sure the class matches
484    if (!class_match(inv_class)) {
485      return false;
486    }
487
488    // Make sure the Ppt matches
489    if (!ppt_match(ppt)) {
490      return false;
491    }
492
493    // Make sure the variables match
494    if (!var_match(vis)) {
495      return false;
496    }
497
498    // Get the non-qualified class name
499    String class_str = "null";
500    if (inv_class != null) {
501      @SuppressWarnings("nullness") // getPackage(): invariant class always has a package
502      @NonNull String packageName = inv_class.getPackage().getName() + ".";
503      class_str = inv_class.getName().replace(packageName, "");
504    }
505
506    // Get a string with all of the variable names.  Each is separated by ': '.
507    // 3 variable slots are always setup for consistency.
508    String vars = "";
509    if (vis != null) {
510      int numvars = vis.length;
511      for (int i = 0; i < numvars; i++) {
512        VarInfo v = vis[i];
513        vars += v.name();
514        if (ourvars[i] != null) {
515          vars += " {" + ourvars[i] + "}";
516        }
517        vars += ": ";
518      }
519      for (int i = numvars; i < 3; i++) {
520        vars += ": ";
521      }
522    }
523
524    // Figure out the sample count if possible
525    String samp_str = "";
526    if (ppt instanceof PptSlice) {
527      PptSlice pslice = (PptSlice) ppt;
528      samp_str = " s" + pslice.num_samples();
529    }
530
531    String line = " line=" + FileIO.get_linenum();
532
533    debugTrack.fine(
534        class_str
535            + ": "
536            + ((ppt == null) ? "null" : ppt.name())
537            + samp_str
538            + line
539            + ": "
540            + vars
541            + msg);
542    if (dkconfig_showTraceback) {
543      Throwable stack = new Throwable("debug traceback");
544      stack.fillInStackTrace();
545      stack.printStackTrace();
546    }
547
548    return true;
549  }
550
551  /** Returns whether or not the specified class matches the classes being tracked. */
552  public static boolean class_match(@Nullable Class<?> inv_class) {
553
554    if ((debugTrackClass.length > 0) && (inv_class != null)) {
555      return strContainsElem(inv_class.getName(), debugTrackClass);
556    }
557    return true;
558  }
559
560  /** Returns whether or not the specified ppt matches the ppts being tracked. */
561  public static boolean ppt_match(
562      @Nullable @UnknownInitialization(daikon.PptTopLevel.class) Ppt ppt) {
563
564    if (debugTrackPpt.length > 0) {
565      return (ppt != null) && strContainsElem(ppt.name(), debugTrackPpt);
566    }
567    return true;
568  }
569
570  /**
571   * Returns whether or not the specified vars match the ones being tracked. Also, sets
572   * Debug.ourvars with the names of the variables matched if they are not the leader of their
573   * equality sets.
574   */
575  public static boolean var_match(VarInfo @Nullable [] vis) {
576
577    if (debugTrackVars.length == 0) {
578      return true;
579    }
580    if (vis == null) {
581      return false;
582    }
583
584    boolean match = false;
585
586    // Loop through each set of specified debug variables.
587    outer:
588    for (String[] cv : debugTrackVars) {
589      if (cv.length != vis.length) {
590        continue;
591      }
592      for (int j = 0; j < ourvars.length; j++) {
593        ourvars[j] = null;
594      }
595
596      // Flags to insure that we don't match a variable more than once
597      boolean[] used = {false, false, false};
598
599      // Loop through each variable in this set of debug variables
600      for (int j = 0; j < cv.length; j++) {
601        boolean this_match = false;
602
603        // Loop through each variable at this point
604        eachvis:
605        for (int k = 0; k < vis.length; k++) {
606
607          // Get the matching equality set
608          Set<VarInfo> evars = null;
609          if (vis[k].equalitySet != null) {
610            evars = vis[k].equalitySet.getVars();
611          }
612
613          // If there is an equality set
614          if ((evars != null) && vis[k].isCanonical()) {
615
616            // Loop through each variable in the equality set
617            for (VarInfo v : evars) {
618              if (!used[k] && (cv[j].equals("*") || cv[j].equals(v.name()))) {
619                used[k] = true;
620                this_match = true;
621                if (!cv[j].equals(vis[j].name())) {
622                  ourvars[j] = v.name();
623                  if (j != k) ourvars[j] += " (" + j + "/" + k + ")";
624                  if (v.isCanonical()) ourvars[j] += " (Leader)";
625                }
626                break eachvis;
627              }
628            }
629          } else { // sometimes, no equality set
630            if (cv[j].equals("*") || cv[j].equals(vis[k].name())) this_match = true;
631          }
632        }
633        if (!this_match) continue outer;
634      }
635      match = true;
636      break outer;
637    }
638
639    return match;
640  }
641
642  /** Looks for an element in arr that is a substring of str. */
643  private static boolean strContainsElem(String str, String[] arr) {
644
645    for (String elt : arr) {
646      if (str.indexOf(elt) >= 0) {
647        return true;
648      }
649    }
650    return false;
651  }
652
653  /**
654   * Looks through entire ppt tree and checks for any items we are interested in. If found, prints
655   * them out.
656   */
657  public static void check(PptMap all_ppts, String msg) {
658
659    boolean found = false;
660
661    for (PptTopLevel ppt : all_ppts.ppt_all_iterable()) {
662      if (ppt_match(ppt)) debugTrack.fine("Matched ppt '" + ppt.name() + "' at " + msg);
663      for (PptSlice slice : ppt.views_iterable()) {
664        for (int k = 0; k < slice.invs.size(); k++) {
665          Invariant inv = slice.invs.get(k);
666          if (inv.log("%s: found #%s=%s in slice %s", msg, k, inv.format(), slice)) found = true;
667        }
668      }
669    }
670    if (!found) debugTrack.fine("Found no points at '" + msg + "'");
671  }
672
673  /** Returns a string containing the integer variables and their values. */
674  public static String int_vars(PptTopLevel ppt, ValueTuple vt) {
675
676    String out = "";
677
678    for (VarInfo v : ppt.var_infos) {
679      if (!v.isCanonical()) {
680        continue;
681      }
682      if (v.file_rep_type != ProglangType.INT) {
683        continue;
684      }
685      out += v.name() + "=" + toString(v.getValueOrNull(vt)) + " [" + vt.getModified(v) + "]: ";
686    }
687    return out;
688  }
689
690  /**
691   * Returns a string containing the variable values for any variables that are currently being
692   * tracked in ppt. The string is of the form 'v1 = val1: v2 = val2, etc.
693   */
694  public static String related_vars(PptTopLevel ppt, ValueTuple vt) {
695
696    String out = "";
697
698    for (VarInfo v : ppt.var_infos) {
699      for (String[] cv : debugTrackVars) {
700        for (String cv_elt : cv) {
701          if (cv_elt.equals(v.name())) {
702            Object val = v.getValue(vt);
703            int mod = vt.getModified(v);
704            out += v.name() + "=";
705            out += toString(val);
706            if ((mod == ValueTuple.MISSING_FLOW) || (mod == ValueTuple.MISSING_NONSENSICAL)) {
707              out += " (missing)";
708            }
709            if (v.missingOutOfBounds()) out += " (out of bounds)";
710            if (v.equalitySet != null) {
711              if (!v.isCanonical()) out += " (leader=" + v.canonicalRep().name() + ")";
712            }
713            // out += " mod=" + mod;
714            out += ": ";
715          }
716        }
717      }
718    }
719
720    return out;
721  }
722
723  /** Like Object.toString(), but handles null, and has special handling for arrays. */
724  public static String toString(@Nullable Object val) {
725    if (val == null) {
726      return "none";
727    }
728    if (val instanceof String) {
729      return "\"" + val + "\"";
730    }
731    if (val instanceof VarInfo[]) {
732      return Arrays.toString((VarInfo[]) val);
733    }
734    if (val instanceof String[]) {
735      return Arrays.toString((String[]) val);
736    }
737    if (val instanceof boolean[]) {
738      return Arrays.toString((boolean[]) val);
739    }
740    if (val instanceof byte[]) {
741      return Arrays.toString((byte[]) val);
742    }
743    if (val instanceof char[]) {
744      return Arrays.toString((char[]) val);
745    }
746    if (val instanceof double[]) {
747      return Arrays.toString((double[]) val);
748    }
749    if (val instanceof float[]) {
750      return Arrays.toString((float[]) val);
751    }
752    if (val instanceof int[]) {
753      return Arrays.toString((int[]) val);
754    }
755    if (val instanceof long[]) {
756      return Arrays.toString((long[]) val);
757    }
758    if (val instanceof short[]) {
759      return Arrays.toString((short[]) val);
760    }
761    return val.toString();
762  }
763
764  /**
765   * Returns a string containing each variable and its value.
766   *
767   * <p>The string is of the form "v1 = val1: v2 = val2, ...".
768   */
769  public static String toString(VarInfo[] vis, ValueTuple vt) {
770
771    StringBuilder out = new StringBuilder();
772
773    for (VarInfo v : vis) {
774      Object val = v.getValue(vt);
775      // int mod = vt.getModified(v);
776      out.append(v.name());
777      out.append("=");
778      out.append(toString(val));
779      if (v.isMissing(vt)) out.append(" (missing)");
780      if (v.missingOutOfBounds()) out.append(" (out of bounds)");
781      if (v.equalitySet != null) {
782        if (!v.isCanonical()) out.append(" (leader=" + v.canonicalRep().name() + ")");
783      }
784      out.append(": ");
785    }
786
787    return out.toString();
788  }
789
790  /**
791   * Parses the specified argument to {@code --track} and sets up the track arrays accordingly. The
792   * syntax of the argument is
793   *
794   * <pre>{@code class|class|...<var,var,var>@ppt}</pre>
795   *
796   * As shown, multiple class arguments can be specified separated by pipe symbols (|). The
797   * variables are specified in angle brackets (&lt;&gt;) and the program point is preceeded by an
798   * at sign (@). Each is optional and can be left out. The add_track routine can be called multiple
799   * times. An invariant that matches any of the specifications will be tracked.
800   */
801  public static @Nullable String add_track(String def) {
802
803    String classes = null;
804    String vars = null;
805    String ppt = null;
806
807    // Get the classes, vars, and ppt
808    int var_start = def.indexOf('<');
809    int ppt_start = def.indexOf("@");
810    if ((var_start == -1) && (ppt_start == -1)) {
811      classes = def;
812    } else if (var_start != -1) {
813      if (var_start > 0) classes = def.substring(0, var_start);
814      if (ppt_start == -1) {
815        vars = def.substring(var_start + 1, def.length() - 1);
816      } else {
817        vars = def.substring(var_start + 1, ppt_start - 1);
818        ppt = def.substring(ppt_start + 1, def.length());
819      }
820    } else {
821      if (ppt_start > 0) classes = def.substring(0, ppt_start);
822      ppt = def.substring(ppt_start + 1, def.length());
823    }
824
825    // If classes were specified, get each class
826    if (classes != null) {
827      String[] class_arr = classes.split("\\|");
828      debugTrackClass = ArraysPlume.concat(debugTrackClass, class_arr);
829    }
830
831    // If vars were specified, get each var
832    if (vars != null) {
833      String[] var_arr = vars.split(", *");
834      String[][] new_var = new String[debugTrackVars.length + 1][];
835      for (int ii = 0; ii < debugTrackVars.length; ii++) {
836        new_var[ii] = debugTrackVars[ii];
837      }
838      new_var[debugTrackVars.length] = var_arr;
839      debugTrackVars = new_var;
840    }
841
842    // if a ppt was specified, add it to the array of tracked ppts
843    if (ppt != null) {
844      String[] newPpt = new String[] {ppt};
845      debugTrackPpt = ArraysPlume.concat(debugTrackPpt, newPpt);
846    }
847
848    System.out.println();
849    debugTrack.fine("After --track: " + def);
850    debugTrack.fine("Track Classes: " + ArraysPlume.toString(debugTrackClass, false));
851    String vars_out = "";
852    for (int ii = 0; ii < debugTrackVars.length; ii++) {
853      vars_out += Arrays.toString(debugTrackVars[ii]) + " ";
854    }
855    debugTrack.fine("Track Vars: " + vars_out);
856    debugTrack.fine("Track Ppts: " + ArraysPlume.toString(debugTrackPpt, false));
857
858    return null;
859  }
860}