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 (<>) 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}