001package daikon; 002 003import daikon.inv.Invariant; 004import daikon.inv.InvariantStatus; 005import daikon.inv.binary.twoScalar.LinearBinary; 006import daikon.inv.binary.twoScalar.LinearBinaryFloat; 007import daikon.inv.ternary.threeScalar.LinearTernary; 008import daikon.inv.ternary.threeScalar.LinearTernaryFloat; 009import daikon.inv.unary.scalar.OneOfFloat; 010import daikon.inv.unary.scalar.OneOfScalar; 011import daikon.inv.unary.sequence.OneOfFloatSequence; 012import daikon.inv.unary.sequence.OneOfSequence; 013import daikon.inv.unary.string.OneOfString; 014import daikon.inv.unary.stringsequence.OneOfStringSequence; 015import daikon.suppress.NIS; 016import java.io.PrintWriter; 017import java.io.Serializable; 018import java.util.ArrayList; 019import java.util.Arrays; 020import java.util.Comparator; 021import java.util.Iterator; 022import java.util.LinkedHashSet; 023import java.util.List; 024import java.util.Set; 025import java.util.logging.Level; 026import java.util.logging.Logger; 027import org.checkerframework.checker.interning.qual.Interned; 028import org.checkerframework.checker.lock.qual.GuardSatisfied; 029import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf; 030import org.checkerframework.checker.nullness.qual.MonotonicNonNull; 031import org.checkerframework.checker.nullness.qual.NonNull; 032import org.checkerframework.checker.nullness.qual.Nullable; 033import org.checkerframework.checker.nullness.qual.RequiresNonNull; 034import org.checkerframework.checker.signedness.qual.UnknownSignedness; 035import org.checkerframework.dataflow.qual.Pure; 036import org.checkerframework.dataflow.qual.SideEffectFree; 037 038/** 039 * Class that implements dynamic constants optimization. This optimization doesn't instantiate 040 * invariants over constant variables (i.e., that that have only seen one value). When the variable 041 * receives a second value, invariants are instantiated and are given the sample representing the 042 * previous constant value. Each DynamicConstants object is associated with a single program point, 043 * ppt. 044 */ 045public class DynamicConstants implements Serializable { 046 047 // We are Serializable, so we specify a version to allow changes to 048 // method signatures without breaking serialization. If you add or 049 // remove fields, you should change this number to the current date. 050 static final long serialVersionUID = 20040401L; 051 052 // If true don't create any invariants (including OneOfs) over dynamic 053 // constants during post processing. Normally, the configuration 054 // variable OneOf_only is more appropriate. 055 static final boolean no_post_process = false; 056 057 // Variables starting with dkconfig_ should only be set via the 058 // daikon.config.Configuration interface. 059 060 /** 061 * Whether to use the dynamic constants optimization. This optimization doesn't instantiate 062 * invariants over constant variables (i.e., that that have only seen one value). When the 063 * variable receives a second value, invariants are instantiated and are given the sample 064 * representing the previous constant value. 065 */ 066 public static boolean dkconfig_use_dynamic_constant_optimization = true; 067 068 /** 069 * Boolean. Controls which invariants are created for variables that are constant for the entire 070 * run. If true, create only OneOf invariants. If false, create all possible invariants. 071 * 072 * <p>Note that setting this to true only fails to create invariants between constants. Invariants 073 * between constants and non-constants are created regardless. 074 * 075 * <p>A problem occurs with merging when this is turned on. If a var_info is constant at one child 076 * slice, but not constant at the other child slice, interesting invariants may not be merged 077 * because they won't exist on the slice with the constant. This is thus currently defaulted to 078 * false. 079 */ 080 public static boolean dkconfig_OneOf_only = false; 081 082 /** Debug tracer. */ 083 public static final Logger debug = Logger.getLogger("daikon.DynamicConstants"); 084 085 /** 086 * List of dynamic constants. 087 * 088 * <p>Each element, c, has c.constant = true, c.count > 0, elt.val != null. 089 */ 090 @SuppressWarnings("serial") 091 List<Constant> con_list = new ArrayList<>(); 092 093 /** 094 * List of variables that have always been missing. 095 * 096 * <p>For each element c, c.always_missing = true or con.vi.missingOutOfBounds(). 097 */ 098 @SuppressWarnings("serial") 099 List<Constant> missing_list = new ArrayList<>(); 100 101 // Same contents in both. Why two data structures? 102 /** Array of all variables. Some may be non-constant. */ 103 Constant[] all_vars; 104 105 // Same contents in both. Why two data structures? 106 /** List of all variables. Some may be non-constant. */ 107 @SuppressWarnings("serial") 108 List<Constant> all_list = new ArrayList<>(); 109 110 /** Program point of these constants. */ 111 PptTopLevel ppt; 112 113 /** Number of samples received. */ 114 int sample_cnt = 0; 115 116 /** 117 * Class used to indicate, for each variable, whether it is constant (see boolean field 118 * "constant"). If it is, then the class also stores its constant value and its sample count. 119 * 120 * <p>Note that two objects of this class are equal if they refer to the same variable. This 121 * allows these to be stored in sets. 122 */ 123 public static @Interned class Constant implements Serializable { 124 125 // We are Serializable, so we specify a version to allow changes to 126 // method signatures without breaking serialization. If you add or 127 // remove fields, you should change this number to the current date. 128 static final long serialVersionUID = 20030913L; 129 130 // XXX Question: what if the constant value is itself null, as for a 131 // String or pointer? Does the code distinguish that case from val not 132 // being set? 133 /** 134 * The value of the constant, or the previous constant value if constant==false and 135 * previously_constant==true. Null iff count=0. 136 */ 137 @SuppressWarnings("serial") 138 public @MonotonicNonNull @Interned Object val = null; 139 140 /** The sample count of the constant. */ 141 public int count = 0; 142 143 /** The variable that has this value. */ 144 public VarInfo vi; 145 146 /** Whether or not this has been missing for every sample to date. */ 147 boolean always_missing = true; 148 149 /** Whether or not this is constant. */ 150 boolean constant = false; 151 152 /** 153 * Whether or not this was constant at the beginning of this sample. At the beginning of the 154 * add() method, all newly non-constant variables are marked (constant=false). It is sometimes 155 * useful within the remainder of processing that sample to know that a variable was constant at 156 * the beginning. The field previously_constant is set to true when constant is set to false, 157 * and then is itself set to false at the end of the add() method. 158 */ 159 boolean previously_constant = false; 160 161 /** 162 * Whether or not this was always missing at the beginning of this sample. At the beginning of 163 * the add() method, all newly non missing variables are marked (always_missing=false). It is 164 * sometimes useful within the remainder of processing that sample to know that a variable was 165 * missing at the beginning. The field previous_missing set to true when missing is set to 166 * false, and then is itself set to false at the end of the add() method. 167 */ 168 boolean previous_missing = false; 169 170 /** Check representation invariant. */ 171 public void checkRep() { 172 // This assertion is not valid. If first sample is missing, then 173 // always_missing=true and previous_missing=false. 174 // assert (always_missing ? previous_missing : true) : toString(); 175 176 assert !(constant && previously_constant) : toString(); 177 178 // Whereas values can be null, null is never the value for a dynamic 179 // constant. 180 assert ((constant || previously_constant) 181 ? (val != null && count > 0) 182 : (val == null && count == 0)) 183 : toString(); 184 } 185 186 /** 187 * Creates a new Constant, indicating whether the given variable is a constant. 188 * 189 * @param vi the variable that might be a constant 190 */ 191 @SuppressWarnings("super.invocation") 192 public Constant(VarInfo vi) { 193 this.vi = vi; 194 } 195 196 /** 197 * Returns whether the specified variable is currently a constant OR was a constant at the 198 * beginning of constants processing. 199 */ 200 @Pure 201 public boolean is_prev_constant() { 202 return constant || previously_constant; 203 } 204 205 @EnsuresNonNullIf(result = true, expression = "#1") 206 @Pure 207 @Override 208 public boolean equals(@GuardSatisfied Constant this, @GuardSatisfied @Nullable Object obj) { 209 if (!(obj instanceof Constant)) { 210 return false; 211 } 212 Constant c = (Constant) obj; 213 return c.vi == vi; 214 } 215 216 @Pure 217 @Override 218 public int hashCode(@GuardSatisfied @UnknownSignedness Constant this) { 219 return vi.hashCode(); 220 } 221 222 @Override 223 @SuppressWarnings("all:purity") // side effects to local state (string creation) 224 @SideEffectFree 225 public String toString(@GuardSatisfied Constant this) { 226 227 StringBuilder out = new StringBuilder(); 228 out.append(vi.name()); 229 if (val == null) { 230 out.append(" (val missing)"); 231 } else { 232 out.append(" (val=" + val + ")"); 233 } 234 if (vi.isCanonical()) out.append(" (leader) "); 235 out.append( 236 " [always_missing=" 237 + always_missing 238 + ", constant=" 239 + constant 240 + ", previously_constant=" 241 + previously_constant 242 + ", previous_missing=" 243 + previous_missing 244 + "]"); 245 return out.toString(); 246 } 247 } 248 249 /** Compares two constants based on the vi_index of their variable. */ 250 public static final class ConIndexComparator implements Comparator<Constant>, Serializable { 251 // We are Serializable, so we specify a version to allow changes to 252 // method signatures without breaking serialization. If you add or 253 // remove fields, you should change this number to the current date. 254 static final long serialVersionUID = 20050923L; 255 256 private ConIndexComparator() {} 257 258 @Pure 259 @Override 260 public int compare(Constant con1, Constant con2) { 261 return con1.vi.varinfo_index - con2.vi.varinfo_index; 262 } 263 264 public static ConIndexComparator getInstance() { 265 return theInstance; 266 } 267 268 static final ConIndexComparator theInstance = new ConIndexComparator(); 269 } 270 271 /** Create an initial list of constants and missing variables for the specified ppt. */ 272 public DynamicConstants(PptTopLevel ppt) { 273 274 this.ppt = ppt; 275 276 // Start everything off as missing (since we haven't seen any values yet) 277 for (VarInfo vi : ppt.var_infos) { 278 @SuppressWarnings("interning") // one Constant per VarInfo 279 @Interned Constant c = new Constant(vi); 280 all_list.add(c); 281 missing_list.add(c); 282 } 283 all_vars = all_list.toArray(new Constant[all_list.size()]); 284 } 285 286 /** 287 * Checks each current constant to see if it is still a constant. Constants must have the same 288 * value and cannot be missing. In the long run a better job of dealing with missing might be 289 * helpful. Also checks each variable that has always been missing to date to insure that it is 290 * still missing. 291 * 292 * <p>Creates all new views required for the newly non constants (noncons) and the newly 293 * non-missing (non_missing). 294 */ 295 public void add(ValueTuple vt, int count) { 296 297 // System.out.println("DynamicConstants.add : " + vt.toString(ppt.var_infos)); 298 299 List<Constant> non_missing = new ArrayList<>(); 300 List<Constant> non_con = new ArrayList<>(); 301 302 // Check each constant, destroy any that are missing or different 303 for (Iterator<Constant> i = con_list.iterator(); i.hasNext(); ) { 304 Constant con = i.next(); 305 assert con.constant; 306 con.checkRep(); 307 308 if (Debug.logDetail()) { 309 Debug.log( 310 getClass(), 311 ppt, 312 Debug.vis(con.vi), 313 "Adding " 314 + Debug.toString(con.vi.getValueOrNull(vt)) 315 + " to constant " 316 + con.val 317 + " : missing = " 318 + missing(con.vi, vt) 319 + ": samples = " 320 + con.count 321 + "/" 322 + count); 323 } 324 if (missing(con.vi, vt) || (con.val != con.vi.getValue(vt))) { 325 i.remove(); 326 con.constant = false; 327 con.previously_constant = true; 328 assert all_vars[con.vi.varinfo_index].constant == false; 329 non_con.add(con); 330 } else { 331 con.count += count; 332 } 333 con.checkRep(); 334 } 335 336 // Move any non-missing variables to the constant list and init their val. 337 // If a variable is missing out of bounds, leave it on this list 338 // forever (guaranteeing that invariants will never be instantiated over 339 // it). 340 for (Iterator<Constant> i = missing_list.iterator(); i.hasNext(); ) { 341 Constant con = i.next(); 342 con.checkRep(); 343 if (con.vi.missingOutOfBounds()) { 344 continue; 345 } 346 347 if (missing(con.vi, vt)) { 348 // value is still missing, nothing to do (we incremented its count above) 349 continue; 350 } 351 352 @Interned Object val = con.vi.getValue(vt); 353 // the variable is not missing, so it is non-null 354 assert val != null; 355 356 i.remove(); 357 con.always_missing = false; 358 if (Debug.logDetail()) { 359 Debug.log( 360 getClass(), 361 ppt, 362 Debug.vis(con.vi), 363 "Adding " 364 + Debug.toString(val) 365 + " to missing : missing = " 366 + missing(con.vi, vt) 367 + ": samples = " 368 + con.count 369 + "/" 370 + count 371 + "/" 372 + sample_cnt); 373 } 374 // Is the Constant missing because it was initialized that way, or 375 // has the program point seen values in the past? 376 if (sample_cnt == 0) { 377 // First sample for this program point (& this variable) 378 con.val = val; 379 con.count = count; 380 con.constant = true; 381 con_list.add(con); 382 } else { 383 // This variable truly is missing; has seen a missing value in the past. 384 non_missing.add(con); 385 con.previous_missing = true; 386 } 387 } 388 389 sample_cnt += count; 390 391 // Create slices over newly non-constant and non-missing variables 392 instantiate_new_views(non_con, non_missing); 393 394 // Turn off previously_constant on all newly non-constants 395 for (Constant con : non_con) { 396 con.previously_constant = false; 397 @SuppressWarnings("nullness") // reinitialization 398 @NonNull Object nullValue = null; 399 con.val = nullValue; 400 con.count = 0; 401 con.checkRep(); 402 } 403 404 // Turn off previous_missing on all newly non-missing 405 for (Constant con : non_missing) { 406 con.previous_missing = false; 407 con.checkRep(); 408 } 409 } 410 411 /** Returns whether the specified variable is missing in this ValueTuple. */ 412 private boolean missing(VarInfo vi, ValueTuple vt) { 413 414 int mod = vt.getModified(vi); 415 return (mod == ValueTuple.MISSING_FLOW) || (mod == ValueTuple.MISSING_NONSENSICAL); 416 } 417 418 /** Returns the Constant for the specified variable. */ 419 @Pure 420 public Constant getConstant(VarInfo vi) { 421 422 Constant result = all_vars[vi.varinfo_index]; 423 result.checkRep(); 424 return result; 425 } 426 427 /** Returns whether the specified variable is currently a constant. */ 428 @Pure 429 public boolean is_constant(VarInfo vi) { 430 431 return getConstant(vi).constant; 432 } 433 434 /** 435 * Returns whether the specified variable is currently a constant OR was a constant at the 436 * beginning of constants processing. 437 */ 438 @Pure 439 public boolean is_prev_constant(VarInfo vi) { 440 441 return getConstant(vi).is_prev_constant(); 442 } 443 444 /** 445 * Returns the constant value of the specified variable, or null if the variable is not constant 446 * or prev_constant. But, it is apparently only called on constants with a value. 447 */ 448 public @Interned Object constant_value(VarInfo vi) { 449 450 @SuppressWarnings("nullness") // non-missing value, so non-null val field 451 @NonNull Object result = getConstant(vi).val; 452 return result; 453 } 454 455 /** Returns whether the specified variable missing for all values so far. */ 456 @Pure 457 public boolean is_missing(VarInfo vi) { 458 459 return getConstant(vi).always_missing; 460 } 461 462 /** 463 * Returns whether the specified variable is currently missing OR was missing at the beginning of 464 * constants processing. 465 */ 466 @Pure 467 public boolean is_prev_missing(VarInfo vi) { 468 469 Constant c = all_vars[vi.varinfo_index]; 470 return c.always_missing || c.previous_missing; 471 } 472 473 /** Returns the number of constants that are leaders. */ 474 public int constant_leader_cnt() { 475 476 int con_cnt = 0; 477 for (Constant con : con_list) { 478 if (con.vi.isCanonical()) con_cnt++; 479 } 480 481 return con_cnt; 482 } 483 484 /** 485 * Creates all new views required for the newly non constants (noncons) and the newly non-missing 486 * (non_missing). 487 */ 488 public void instantiate_new_views(List<Constant> noncons, List<Constant> non_missing) { 489 490 if (Debug.logOn()) { 491 for (Constant con : noncons) { 492 Debug.log( 493 getClass(), 494 ppt, 495 Debug.vis(con.vi), 496 "is non constant" 497 + " with val = " 498 + Debug.toString(con.val) 499 + " with count = " 500 + con.count); 501 } 502 for (Constant con : non_missing) { 503 Debug.log(getClass(), ppt, Debug.vis(con.vi), "is non missing"); 504 } 505 } 506 507 for (Constant con : noncons) { 508 con.checkRep(); 509 } 510 for (Constant con : non_missing) { 511 con.checkRep(); 512 } 513 514 // Create all of the views over noncons and noncons+con_list. 515 // Since everything starts out as a constant, it is only necessary 516 // to combine the newly non-constants with a combination of 517 // the remaining constants and the newly-non constants. Any slices 518 // between the non-constants and other variables will have already 519 // been created when those other variables became non-constants. 520 if (noncons.size() > 0) { 521 List<Constant> cons = new ArrayList<>(); 522 cons.addAll(con_list); 523 cons.addAll(noncons); 524 debug.fine("Instantiating non constants in ppt: " + ppt.name()); 525 instantiate_views(noncons, cons); 526 } 527 528 // Create all views over the newly non-missing. Since missing 529 // vars were not included in any previous views, we must match them 530 // against all variables. 531 if (non_missing.size() > 0) { 532 debug.fine("Instantiating non missing in ppt: " + ppt.name()); 533 instantiate_views(non_missing, all_list); 534 } 535 536 // Create any ternary invariants that are suppressed when one 537 // of the variables is a constant. Currently, only LinearTernary 538 // falls into this list (It is suppressed by (x = C) && (Ay + Bz = D)) 539 if (NIS.dkconfig_enabled) instantiate_constant_suppressions(noncons, all_list); 540 } 541 542 /** 543 * Instantiate views and invariants across each combination of vars from list1 and list2. If each 544 * item in a new slice was a constant, the constant values are applied. 545 * 546 * <p>The following slices will be created: 547 * 548 * <pre> 549 * unary: list1-vars 550 * binary: list1-vars X list2-vars 551 * ternary: list1-vars X list2-vars X list2-vars 552 * </pre> 553 */ 554 private void instantiate_views(List<Constant> list1, List<Constant> list2) { 555 556 // Get list1 leaders 557 Set<Constant> leaders1 = new LinkedHashSet<>(); 558 for (Constant con : list1) { 559 if (con.vi.isCanonical()) leaders1.add(con); 560 } 561 562 // Get list2 leaders 563 Set<Constant> leaders2 = new LinkedHashSet<>(); 564 for (Constant con : list2) { 565 if (con.vi.isCanonical()) leaders2.add(con); 566 } 567 568 if (debug.isLoggable(Level.FINE)) { 569 debug.fine("instantiating over " + leaders1.size() + " leaders1: " + leaders1); 570 debug.fine("instantiating over " + leaders2.size() + " leaders2: " + leaders2); 571 } 572 573 // any new views created 574 List<PptSlice> new_views = new ArrayList<>(); 575 576 int mod = ValueTuple.MODIFIED; 577 578 // Unary slices/invariants 579 for (Constant con : leaders1) { 580 if (Debug.logOn()) Debug.log(getClass(), ppt, Debug.vis(con.vi), "Considering slice"); 581 if (!ppt.is_slice_ok(con.vi)) { 582 continue; 583 } 584 PptSlice1 slice1 = new PptSlice1(ppt, con.vi); 585 slice1.instantiate_invariants(); 586 if (Debug.logOn()) Debug.log(getClass(), ppt, Debug.vis(con.vi), "Instantiated invs"); 587 if (con.count > 0) { 588 assert con.val != null : "@AssumeAssertion(nullness): dependent: val != null when count>0"; 589 slice1.add_val_bu(con.val, mod, con.count); 590 } 591 new_views.add(slice1); 592 } 593 594 // Binary slices/invariants. 595 for (Constant con1 : leaders1) { 596 for (Constant con2 : leaders2) { 597 Constant c1 = con1; 598 Constant c2 = con2; 599 Debug.log(getClass(), ppt, Debug.vis(c1.vi, c2.vi), "Considering slice"); 600 if (con2.vi.varinfo_index < con1.vi.varinfo_index) { 601 if (leaders1.contains(con2)) { 602 // The variable is in both leader lists. 603 // Don't add it on this iteration; add it when the variables 604 // are given in order (to prevent creating the slice twice). 605 continue; 606 } 607 c1 = con2; 608 c2 = con1; 609 } 610 if (!ppt.is_slice_ok(c1.vi, c2.vi)) { 611 if (Debug.logOn()) { 612 Debug.log( 613 debug, 614 getClass(), 615 ppt, 616 Debug.vis(c1.vi, c2.vi), 617 "Not instantiating slice " + c1.vi.equalitySet.size()); 618 } 619 continue; 620 } 621 PptSlice2 slice2 = new PptSlice2(ppt, c1.vi, c2.vi); 622 Debug.log( 623 getClass(), 624 ppt, 625 Debug.vis(c1.vi, c2.vi), 626 String.format("instantiating slice %s [%s %s]%n", slice2, c1, c2)); 627 slice2.instantiate_invariants(); 628 if (c1.count > 0 && c2.count > 0) { 629 assert c1.val != null : "@AssumeAssertion(nullness): dependent: val != null when count>0"; 630 assert c2.val != null : "@AssumeAssertion(nullness): dependent: val != null when count>0"; 631 slice2.add_val_bu(c1.val, c2.val, mod, mod, con1.count); 632 } 633 new_views.add(slice2); 634 } 635 } 636 637 // Ternary slices/invariants. Note that if a variable is in both 638 // leader lists, it is only added when it is in order (to prevent 639 // creating the slice twice). 640 for (Constant con1 : leaders1) { 641 for (Constant con2 : leaders2) { 642 if ((con2.vi.varinfo_index < con1.vi.varinfo_index) && leaders1.contains(con2)) { 643 continue; 644 } 645 for (Constant con3 : leaders2) { 646 if ((con3.vi.varinfo_index < con2.vi.varinfo_index) 647 || ((con3.vi.varinfo_index < con1.vi.varinfo_index) && leaders1.contains(con3))) 648 continue; 649 Constant[] con_arr = {con1, con2, con3}; 650 Arrays.sort(con_arr, ConIndexComparator.getInstance()); 651 assert (con_arr[0].vi.varinfo_index <= con_arr[1].vi.varinfo_index) 652 && (con_arr[1].vi.varinfo_index <= con_arr[2].vi.varinfo_index); 653 if (!ppt.is_slice_ok(con_arr[0].vi, con_arr[1].vi, con_arr[2].vi)) { 654 continue; 655 } 656 657 PptSlice3 slice3 = new PptSlice3(ppt, con_arr[0].vi, con_arr[1].vi, con_arr[2].vi); 658 slice3.instantiate_invariants(); 659 if ((con_arr[0].count > 0) && (con_arr[1].count > 0) && (con_arr[2].count > 0)) { 660 assert con_arr[0].val != null 661 : "@AssumeAssertion(nullness): dependent: val != null when count>0"; 662 assert con_arr[1].val != null 663 : "@AssumeAssertion(nullness): dependent: val != null when count>0"; 664 assert con_arr[2].val != null 665 : "@AssumeAssertion(nullness): dependent: val != null when count>0"; 666 slice3.add_val_bu( 667 con_arr[0].val, con_arr[1].val, con_arr[2].val, mod, mod, mod, con_arr[0].count); 668 } 669 new_views.add(slice3); 670 } 671 } 672 } 673 674 // Debug print the created slices 675 if (Debug.logOn() || debug.isLoggable(Level.FINE)) { 676 int[] slice_cnt = {0, 0, 0, 0}; 677 int[] inv_cnt = {0, 0, 0, 0}; 678 int[] true_inv_cnt = {0, 0, 0, 0}; 679 for (PptSlice slice : new_views) { 680 for (Invariant inv : slice.invs) { 681 inv.log("created, falsified = %b", inv.is_false()); 682 if (!inv.is_false()) { 683 true_inv_cnt[slice.arity()]++; 684 } else { 685 String vals = ""; 686 for (VarInfo vi : slice.var_infos) { 687 vals += vi.name() + "=" + Debug.toString(constant_value(vi)) + " "; 688 } 689 inv.log("Invariant %s destroyed by constant values %s", inv.format(), vals); 690 } 691 } 692 if (slice.invs.size() > 0) slice_cnt[slice.arity()]++; 693 inv_cnt[slice.arity()] += slice.invs.size(); 694 if (Debug.logDetail()) { 695 StringBuilder sb = new StringBuilder(); 696 for (int j = 0; j < slice.arity(); j++) { 697 VarInfo v = slice.var_infos[j]; 698 sb.append(v.name() + " [" + v.file_rep_type + "] [" + v.comparability + "] "); 699 } 700 Debug.log( 701 debug, 702 getClass(), 703 ppt, 704 slice.var_infos, 705 "Adding slice over " + sb + ": with " + slice.invs.size() + " invariants"); 706 } 707 } 708 for (int i = 1; i <= 3; i++) { 709 debug.fine( 710 "Added " 711 + slice_cnt[i] 712 + " slice" 713 + i 714 + "s with " 715 + true_inv_cnt[i] 716 + " invariants (" 717 + inv_cnt[i] 718 + " total)"); 719 } 720 721 String leader1_str = ""; 722 int leader1_cnt = 0; 723 for (Constant con1 : leaders1) { 724 if (con1.vi.file_rep_type == ProglangType.INT) { 725 leader1_str += con1.vi.name() + " "; 726 leader1_cnt++; 727 } 728 } 729 730 String leader2_str = ""; 731 int leader2_cnt = 0; 732 for (Constant con1 : leaders2) { 733 if (con1.vi.file_rep_type == ProglangType.INT) { 734 leader2_str += con1.vi.name() + " "; 735 leader2_cnt++; 736 } 737 } 738 debug.fine( 739 leader1_cnt 740 + " leader1 ints (" 741 + leader1_str 742 + "): " 743 + leader2_cnt 744 + " leader2 ints (" 745 + leader2_str); 746 } 747 748 // Remove any falsified invariants from the new views. Don't 749 // call remove_falsified() since that has side-effects (such as 750 // NIS processing on the falsified invariants) that we don't want. 751 for (PptSlice slice : new_views) { 752 List<Invariant> to_remove = new ArrayList<>(); 753 for (Invariant inv : slice.invs) { 754 if (inv.is_false()) { 755 to_remove.add(inv); 756 } 757 } 758 slice.removeInvariants(to_remove); 759 } 760 761 // Add the new slices to the top level ppt. This will discard any 762 // slices that ended up with zero invariants 763 ppt.addViews(new_views); 764 } 765 766 public void instantiate_constant_suppressions(List<Constant> new_noncons, List<Constant> all) { 767 768 // Find all of the variable (non-constant) non-missing 769 // integral/float leaders 770 List<Constant> vars = new ArrayList<>(); 771 for (Constant con : all) { 772 if (con.always_missing || con.previous_missing) { 773 continue; 774 } 775 if (con.constant || con.previously_constant) { 776 continue; 777 } 778 if (!con.vi.isCanonical()) { 779 continue; 780 } 781 if (!con.vi.file_rep_type.isIntegral() && !con.vi.file_rep_type.isFloat()) { 782 continue; 783 } 784 if (con.vi.rep_type.isArray()) { 785 continue; 786 } 787 vars.add(con); 788 } 789 790 // Find all of the new non-constant integer/float leaders 791 List<Constant> new_leaders = new ArrayList<>(); 792 for (Constant con : new_noncons) { 793 if (!con.vi.isCanonical()) { 794 continue; 795 } 796 if (!con.vi.file_rep_type.isIntegral() && !con.vi.file_rep_type.isFloat()) { 797 continue; 798 } 799 if (con.vi.rep_type.isArray()) { 800 continue; 801 } 802 new_leaders.add(con); 803 } 804 805 if (debug.isLoggable(Level.FINE)) { 806 debug.fine("new non-con leaders = " + new_leaders); 807 debug.fine("variable leaders = " + vars); 808 } 809 810 // Consider all of the ternary slices with one new non-constant 811 for (int i = 0; i < new_leaders.size(); i++) { 812 Constant con1 = new_leaders.get(i); 813 assert con1.val != null : "@AssumeAssertion(nullness)"; 814 for (int j = 0; j < vars.size(); j++) { 815 Constant con2 = vars.get(j); 816 assert con1 != con2; 817 for (int k = j; k < vars.size(); k++) { 818 Constant con3 = vars.get(k); 819 assert con1 != con3; 820 if (!ppt.is_slice_ok(con1.vi, con2.vi, con3.vi)) { 821 continue; 822 } 823 824 if (debug.isLoggable(Level.FINE)) { 825 debug.fine(String.format("considering slice %s %s %s", con1, con2, con3)); 826 } 827 828 // Look for a LinearBinary over two variables. If it doesn't 829 // exist we don't create a LinearTernary 830 Invariant lb = find_linear_binary(ppt.findSlice(con2.vi, con3.vi)); 831 if (lb == null) { 832 continue; 833 } 834 835 // Find the ternary slice and create it if it is not there 836 PptSlice slice = ppt.get_or_instantiate_slice(con1.vi, con2.vi, con3.vi); 837 838 // Create the LinearTernary invariant from the LinearBinary 839 // invariant and the constant value 840 Invariant lt = null; 841 if (con1.vi.file_rep_type.isIntegral()) { 842 lt = LinearTernary.get_proto().instantiate(slice); 843 if (lt != null) { 844 ((LinearTernary) lt).setup((LinearBinary) lb, con1.vi, ((Long) con1.val).longValue()); 845 } 846 } else /* must be float */ { 847 lt = LinearTernaryFloat.get_proto().instantiate(slice); 848 if (lt != null) { 849 ((LinearTernaryFloat) lt) 850 .setup((LinearBinaryFloat) lb, con1.vi, ((Double) con1.val).doubleValue()); 851 } 852 } 853 if (lt != null) { 854 if (Debug.dkconfig_internal_check) { 855 assert slice.find_inv_by_class(lt.getClass()) == null 856 : "inv = " + lt.format() + " slice = " + slice; 857 } 858 slice.addInvariant(lt); 859 if (debug.isLoggable(Level.FINE)) { 860 debug.fine("Adding invariant " + lt.format() + " to slice " + slice); 861 } 862 } 863 } 864 } 865 } 866 867 // Consider all of the ternary slices with two new non-constants 868 for (int i = 0; i < new_leaders.size(); i++) { 869 Constant con1 = new_leaders.get(i); 870 assert con1.val != null : "@AssumeAssertion(nullness)"; 871 for (int j = i; j < new_leaders.size(); j++) { 872 Constant con2 = new_leaders.get(j); 873 for (int k = 0; k < vars.size(); k++) { 874 Constant con3 = vars.get(k); 875 assert con2 != con3; 876 assert con1 != con3; 877 if (!ppt.is_slice_ok(con1.vi, con2.vi, con3.vi)) { 878 continue; 879 } 880 881 if (debug.isLoggable(Level.FINE)) { 882 debug.fine(String.format("considering slice %s %s %s", con1, con2, con3)); 883 } 884 885 // Create the ternary slice 886 887 // Create the LinearTernary invariant from the OneOf invariant 888 // (if any) and the constant values. If no OneOf exists, 889 // there can be no interesting plane of the points 890 Invariant lt = null; 891 PptSlice slice = null; 892 InvariantStatus sts = InvariantStatus.NO_CHANGE; 893 if (con1.vi.file_rep_type.isIntegral()) { 894 OneOfScalar oo = 895 (OneOfScalar) ppt.find_inv_by_class(new VarInfo[] {con3.vi}, OneOfScalar.class); 896 if (oo == null) { 897 continue; 898 } 899 slice = ppt.get_or_instantiate_slice(con1.vi, con2.vi, con3.vi); 900 901 lt = LinearTernary.get_proto().instantiate(slice); 902 if (lt != null) { 903 assert con2.val != null : "@AssumeAssertion(nullness)"; 904 sts = 905 ((LinearTernary) lt) 906 .setup( 907 oo, 908 con1.vi, 909 ((Long) con1.val).longValue(), 910 con2.vi, 911 ((Long) con2.val).longValue()); 912 } 913 } else /* must be float */ { 914 OneOfFloat oo = 915 (OneOfFloat) ppt.find_inv_by_class(new VarInfo[] {con3.vi}, OneOfFloat.class); 916 if (oo == null) { 917 continue; 918 } 919 slice = ppt.get_or_instantiate_slice(con1.vi, con2.vi, con3.vi); 920 lt = LinearTernaryFloat.get_proto().instantiate(slice); 921 if (lt != null) { 922 assert con2.val != null : "@AssumeAssertion(nullness)"; 923 sts = 924 ((LinearTernaryFloat) lt) 925 .setup( 926 oo, 927 con1.vi, 928 ((Double) con1.val).doubleValue(), 929 con2.vi, 930 ((Double) con2.val).doubleValue()); 931 } 932 } 933 if ((lt != null) && (sts == InvariantStatus.NO_CHANGE)) { 934 if (Debug.dkconfig_internal_check) { 935 assert slice.find_inv_by_class(lt.getClass()) == null 936 : "inv = " + lt.format() + " slice = " + slice; 937 } 938 slice.addInvariant(lt); 939 debug.fine("Adding invariant " + lt.format() + " to slice " + slice); 940 } 941 } 942 } 943 } 944 } 945 946 /** 947 * Looks for a LinearBinary invariant in the specified slice. Will match either float or integer 948 * versions. 949 */ 950 private @Nullable Invariant find_linear_binary(@Nullable PptSlice slice) { 951 952 // if (debug.isLoggable (Level.FINE)) 953 // debug.fine ("considering slice " + slice); 954 955 if (slice == null) { 956 return null; 957 } 958 959 for (Invariant inv : slice.invs) { 960 // debug.fine ("inv = " + inv.getClass()); 961 if ((inv.getClass() == LinearBinary.class) || (inv.getClass() == LinearBinaryFloat.class)) { 962 return inv; 963 } 964 } 965 966 return null; 967 } 968 969 /** 970 * Create invariants for any remaining constants. Right now, this looks for invariants between all 971 * of the constants. It's not clear that invariants between constants are interesting, but to 972 * match previous behavior, this is what we will do for now. 973 */ 974 public void post_process() { 975 976 // if requested, don't create any post-processed invariants 977 if (no_post_process) { 978 int con_count = 0; 979 for (Constant con : con_list) { 980 if (!con.vi.isCanonical()) { 981 continue; 982 } 983 System.out.println( 984 " Not creating invariants over leader " + con.vi.name() + " = " + con.val); 985 con_count++; 986 } 987 System.out.println(con_count + " constants at ppt " + ppt); 988 return; 989 } 990 991 // If specified, create only OneOf invariants. Also create a reflexive 992 // equality invariant, since that is assumed to exist in many places. 993 if (dkconfig_OneOf_only) { 994 for (Constant con : con_list) { 995 if (!con.vi.isCanonical()) { 996 continue; 997 } 998 instantiate_oneof(con); 999 ppt.create_equality_inv(con.vi, con.vi, con.count); 1000 } 1001 return; 1002 } 1003 1004 // Get a list of all remaining constants and clear the existing list 1005 // (if the existing list is not cleared, constant slices will not 1006 // be created). 1007 List<Constant> noncons = con_list; 1008 for (Constant con : con_list) { 1009 con.constant = false; 1010 con.previously_constant = true; 1011 } 1012 con_list = new ArrayList<Constant>(); 1013 1014 // Don't do anything with variables that have always been missing. They 1015 // should have no invariants over them. 1016 List<Constant> non_missing = new ArrayList<>(); 1017 1018 instantiate_new_views(noncons, non_missing); 1019 1020 /* Code to just create just unary slices for constants 1021 for (Constant con : con_list) { 1022 if (!con.vi.isCanonical()) { 1023 continue; 1024 } 1025 PptSlice1 slice1 = new PptSlice1 (ppt, con.vi); 1026 slice1.instantiate_invariants(); 1027 if (con.val != null) { 1028 slice1.add_val (con.val, ValueTuple.MODIFIED, con.count); 1029 } 1030 new_views.add (slice1); 1031 } 1032 ppt.addViews (new_views); 1033 */ 1034 } 1035 1036 /** 1037 * Create unary and binary constant invariants. The slices and invariants are created and 1038 * returned, but not added to the ppt. Note that when NIS.dkconfig_suppressor_list is turned on 1039 * (default is on), only unary and binary invariants that can be suppressors in NIS suppressions 1040 * are created. 1041 */ 1042 @RequiresNonNull("daikon.suppress.NIS.suppressor_proto_invs") 1043 public List<PptSlice> create_constant_invs() { 1044 1045 // Turn off track logging so that we don't get voluminous messages 1046 // each time this is called 1047 boolean debug_on = Logger.getLogger("daikon.Debug").isLoggable(Level.FINE); 1048 if (debug_on) { 1049 LogHelper.setLevel("daikon.Debug", Level.OFF); 1050 } 1051 1052 // Get constant leaders 1053 List<Constant> leaders = new ArrayList<>(100); 1054 for (Constant con : con_list) { 1055 if (!con.vi.isCanonical()) { 1056 continue; 1057 } 1058 1059 // hashcode types are not involved in suppressions 1060 if (NIS.dkconfig_skip_hashcode_type) { 1061 if (con.vi.file_rep_type.isHashcode()) { 1062 continue; 1063 } 1064 } 1065 1066 leaders.add(con); 1067 } 1068 1069 List<PptSlice> new_views = new ArrayList<>(100); 1070 int mod = ValueTuple.MODIFIED; 1071 1072 // Unary slices/invariants 1073 for (Constant con : leaders) { 1074 1075 PptSlice1 slice1 = new PptSlice1(ppt, con.vi); 1076 1077 if (NIS.dkconfig_suppressor_list) { 1078 slice1.instantiate_invariants(NIS.suppressor_proto_invs); 1079 } else { 1080 slice1.instantiate_invariants(); 1081 } 1082 1083 if (con.count > 0) { 1084 assert con.val != null : "@AssumeAssertion(nullness): dependent: val when count>0"; 1085 slice1.add_val_bu(con.val, mod, con.count); 1086 } 1087 if (slice1.invs.size() > 0) new_views.add(slice1); 1088 } 1089 1090 // Binary slices/invariants 1091 for (int i = 0; i < leaders.size(); i++) { 1092 Constant con1 = leaders.get(i); 1093 for (int j = i; j < leaders.size(); j++) { 1094 Constant con2 = leaders.get(j); 1095 if (!con1.vi.compatible(con2.vi)) { 1096 continue; 1097 } 1098 1099 PptSlice2 slice2 = new PptSlice2(ppt, con1.vi, con2.vi); 1100 if (NIS.dkconfig_suppressor_list) { 1101 slice2.instantiate_invariants(NIS.suppressor_proto_invs); 1102 } else { 1103 slice2.instantiate_invariants(); 1104 } 1105 1106 if (con1.count > 0 && con2.count > 0) { 1107 assert con1.val != null 1108 : "@AssumeAssertion(nullness): dependent: val != null when count>0"; 1109 assert con2.val != null 1110 : "@AssumeAssertion(nullness): dependent: val != null when count>0"; 1111 slice2.add_val_bu(con1.val, con2.val, mod, mod, con1.count); 1112 } 1113 if (slice2.invs.size() > 0) new_views.add(slice2); 1114 } 1115 } 1116 1117 // Remove any falsified invariants from the new views. 1118 for (PptSlice slice : new_views) { 1119 for (Iterator<Invariant> j = slice.invs.iterator(); j.hasNext(); ) { 1120 Invariant inv = j.next(); 1121 if (inv.is_false()) { 1122 j.remove(); 1123 } 1124 } 1125 } 1126 1127 if (debug_on) { 1128 LogHelper.setLevel("daikon.Debug", Level.FINE); 1129 } 1130 1131 return new_views; 1132 } 1133 1134 public void print_missing(PrintWriter out) { 1135 1136 for (Constant con : missing_list) { 1137 out.println(con.vi.name() + " is always missing"); 1138 } 1139 } 1140 1141 /** 1142 * Merge dynamic constants from the children of this ppt. Only missing is merged since constants 1143 * are not used after we are done processing samples. 1144 */ 1145 public void merge() { 1146 1147 // clear the constant and missing lists 1148 missing_list.clear(); 1149 con_list.clear(); 1150 1151 // Process each variable at this ppt. If the variable is missing at 1152 // each of the children, it is also missing here. Ignore children that 1153 // have no mapping for this variable 1154 for (VarInfo pvar : ppt.var_infos) { 1155 boolean missing = true; 1156 for (PptRelation rel : ppt.children) { 1157 VarInfo cvar = rel.childVar(pvar); 1158 if ((cvar != null) 1159 && (rel.child.constants != null) 1160 && !rel.child.constants.is_missing(cvar)) { 1161 missing = false; 1162 break; 1163 } 1164 } 1165 Constant c = all_vars[pvar.varinfo_index]; 1166 c.checkRep(); 1167 c.always_missing = missing; 1168 c.checkRep(); 1169 if (missing) missing_list.add(c); 1170 } 1171 } 1172 1173 /** Creates OneOf invariants for each constant. */ 1174 public void instantiate_oneof(Constant con) { 1175 assert con.val != null : "@AssumeAssertion(nullness)"; 1176 1177 // @NonNull, but not marked that way to ease warning suppression. 1178 Invariant inv; 1179 PptSlice1 slice1 = (PptSlice1) ppt.get_or_instantiate_slice(con.vi); 1180 1181 // Create the correct OneOf invariant 1182 ProglangType rep_type = con.vi.rep_type; 1183 boolean is_scalar = rep_type.isScalar(); 1184 if (is_scalar) { 1185 if (!OneOfScalar.dkconfig_enabled) { 1186 return; 1187 } 1188 inv = OneOfScalar.get_proto().instantiate(slice1); 1189 } else if (rep_type == ProglangType.INT_ARRAY) { 1190 if (!OneOfSequence.dkconfig_enabled) { 1191 return; 1192 } 1193 inv = OneOfSequence.get_proto().instantiate(slice1); 1194 } else if (rep_type == ProglangType.DOUBLE) { 1195 if (!OneOfFloat.dkconfig_enabled) { 1196 return; 1197 } 1198 inv = OneOfFloat.get_proto().instantiate(slice1); 1199 } else if (rep_type == ProglangType.DOUBLE_ARRAY) { 1200 if (!OneOfFloatSequence.dkconfig_enabled) { 1201 return; 1202 } 1203 inv = OneOfFloatSequence.get_proto().instantiate(slice1); 1204 } else if (rep_type == ProglangType.STRING) { 1205 if (!OneOfString.dkconfig_enabled) { 1206 return; 1207 } 1208 inv = OneOfString.get_proto().instantiate(slice1); 1209 } else if (rep_type == ProglangType.STRING_ARRAY) { 1210 if (!OneOfStringSequence.dkconfig_enabled) { 1211 return; 1212 } 1213 inv = OneOfStringSequence.get_proto().instantiate(slice1); 1214 } else { 1215 throw new Error("Unrecognized rep_type in instantiate_oneof"); 1216 } 1217 assert inv != null 1218 : "@AssumeAssertion(nullness): instantiation of the given invariants always succeeds"; 1219 slice1.addInvariant(inv); 1220 1221 // Add the value to it 1222 slice1.add_val_bu(con.val, ValueTuple.MODIFIED, con.count); 1223 } 1224}