001package daikon; 002 003import daikon.inv.DiscardInfo; 004import daikon.inv.Invariant; 005import daikon.suppress.NIS; 006import java.util.ArrayList; 007import java.util.Arrays; 008import java.util.Comparator; 009import java.util.Iterator; 010import java.util.List; 011import java.util.logging.Level; 012import java.util.logging.Logger; 013import org.checkerframework.checker.initialization.qual.UnknownInitialization; 014import org.checkerframework.checker.lock.qual.GuardSatisfied; 015import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf; 016import org.checkerframework.checker.nullness.qual.Nullable; 017import org.checkerframework.checker.nullness.qual.RequiresNonNull; 018import org.checkerframework.dataflow.qual.Pure; 019import org.checkerframework.dataflow.qual.SideEffectFree; 020import org.plumelib.util.ArraysPlume; 021 022/** 023 * A Slice is a view of some of the variables for a program point. A program point (that is, 024 * PptTopLevel) does not directly contain invariants. Instead, slices contain the invariants that 025 * involve (all) the Slice's variables. 026 * 027 * <p>Suppose a program point has variables A, B, C, and D.<br> 028 * There would be 4 unary slices -- one each for variables A, B, C, and D.<br> 029 * There would be 6 binary slices -- for {A,B}, {A,C}, {A,D}, {B,C}, {B,D}, and {C,D}.<br> 030 * There would be 4 ternary slices -- for {A,B,C}, {A,B,D}, {A,C,D}, and {B,C,D}. 031 */ 032public abstract class PptSlice extends Ppt { 033 // We are Serializable, so we specify a version to allow changes to 034 // method signatures without breaking serialization. If you add or 035 // remove fields, you should change this number to the current date. 036 static final long serialVersionUID = 20040921L; 037 038 // Permit subclasses to use it. 039 protected static final String lineSep = Global.lineSep; 040 041 /** Debug tracer. */ 042 public static final Logger debug = Logger.getLogger("daikon.PptSlice"); 043 044 /** Debug tracer for debugging both this and PptSlices. */ 045 public static final Logger debugGeneral = Logger.getLogger("daikon.PptSlice.general"); 046 047 public static final Logger debugFlow = Logger.getLogger("daikon.flow.flow"); 048 049 public static final Logger debugGuarding = Logger.getLogger("daikon.guard"); 050 051 // A better name would perhaps be "container", as this has nothing to do 052 // with the program point hierarchy. 053 /** This is a slice of the 'parent' ppt. */ 054 public PptTopLevel parent; 055 056 public abstract int arity(@UnknownInitialization(PptSlice.class) PptSlice this); 057 058 /** 059 * The invariants contained in this slice. This should not be used directly, in general. In 060 * particular, subclasses such as PptSlice0 need to synchronize it with other values. Therefore, 061 * it should be manipulated via {@link #addInvariant} and {@link #removeInvariant}. 062 */ 063 @SuppressWarnings("serial") 064 public List<Invariant> invs; 065 066 PptSlice(PptTopLevel parent, VarInfo[] var_infos) { 067 super(var_infos); 068 this.parent = parent; 069 invs = new ArrayList<Invariant>(); 070 // Ensure that the VarInfo objects are in order (and not duplicated). 071 for (int i = 0; i < var_infos.length - 1; i++) { 072 assert var_infos[i].varinfo_index <= var_infos[i + 1].varinfo_index; 073 } 074 assert this instanceof PptSliceEquality || arity() == var_infos.length; 075 076 if (debugGeneral.isLoggable(Level.FINE)) { 077 debugGeneral.fine(Arrays.toString(var_infos)); 078 } 079 } 080 081 @SideEffectFree 082 @Override 083 @SuppressWarnings("nullness:override.receiver") // see comment on overridden definition in Ppt 084 public final String name(@GuardSatisfied @UnknownInitialization(PptSlice.class) PptSlice this) { 085 return parent.name + varNames(var_infos); 086 } 087 088 public boolean usesVar(VarInfo vi) { 089 return (ArraysPlume.indexOfEq(var_infos, vi) != -1); 090 } 091 092 // This is only called from inv.filter.VariableFilter. 093 public boolean usesVar(String name) { 094 for (int i = 0; i < var_infos.length; i++) { 095 // mistere: I'm not sure is this is the right thing for 096 // the gui, but it's probably close 097 if (var_infos[i].name().equals(name)) { 098 return true; 099 } 100 } 101 return false; 102 } 103 104 /** 105 * Returns true if any of our variables is named NAME, or is derived from a variable named NAME. 106 * 107 * @return true if any of our variables is named NAME, or is derived from a variable named NAME 108 */ 109 // Only called right now from tools/ExtractConsequent 110 public boolean usesVarDerived(String name) { 111 for (VarInfo vi : var_infos) { 112 if (vi.includes_simple_name(name)) { 113 return true; 114 } 115 } 116 return false; 117 } 118 119 /** 120 * Returns true if all of this slice's variables are orig() variables. 121 * 122 * @return true if all of this slice's variables are orig() variables 123 */ 124 public boolean allPrestate() { 125 for (VarInfo vi : var_infos) { 126 if (!vi.isPrestateDerived()) { 127 return false; 128 } 129 } 130 return true; 131 } 132 133 public abstract void addInvariant(Invariant inv); 134 135 /** This method actually removes the invariant from its PptSlice. */ 136 // I don't just use ppt.invs.remove because I want to be able to defer 137 // and to take action if the vector becomes void. 138 public void removeInvariant(Invariant inv) { 139 140 if (Debug.logDetail()) log("Removing invariant '" + inv.format() + "'"); 141 if (Debug.logOn()) inv.log("Removed from slice: %s", inv.format()); 142 boolean removed = invs.remove(inv); 143 assert removed : "inv " + inv + " not in ppt " + name(); 144 Global.falsified_invariants++; 145 if (invs.size() == 0) { 146 if (Debug.logDetail()) log("last invariant removed"); 147 } 148 } 149 150 // This can be called with very long lists by the conditionals code. 151 // At least until that's fixed, it's important for it not to be 152 // quadratic. 153 public void removeInvariants(List<Invariant> to_remove) { 154 if (to_remove.size() < 10) { 155 for (Invariant trinv : to_remove) { 156 removeInvariant(trinv); 157 } 158 } else { 159 int old_invs_size = invs.size(); 160 invs.removeAll(to_remove); 161 assert old_invs_size - invs.size() == to_remove.size(); 162 Global.falsified_invariants += to_remove.size(); 163 if (invs.size() == 0) { 164 if (Debug.logDetail()) log("last invariant removed"); 165 } 166 } 167 } 168 169 /** 170 * This procedure accepts a sample (a ValueTuple), extracts the values from it, casts them to the 171 * proper types, and passes them along to the invariants proper. (The invariants accept typed 172 * values rather than a ValueTuple that encapsulates objects of any type whatever.) 173 * 174 * @return a List of Invariants that weakened due to the processing 175 */ 176 abstract List<Invariant> add(ValueTuple full_vt, int count); 177 178 /** Removes any falsified invariants from our list. */ 179 @RequiresNonNull("daikon.suppress.NIS.suppressor_map") 180 protected void remove_falsified() { 181 182 // Remove the dead invariants 183 for (Iterator<Invariant> iFalsified = invs.iterator(); iFalsified.hasNext(); ) { 184 Invariant inv = iFalsified.next(); 185 if (inv.is_false()) { 186 iFalsified.remove(); 187 NIS.falsified(inv); 188 } 189 } 190 } 191 192 /** Return an approximation of the number of samples seen on this slice. */ 193 public abstract int num_samples(@UnknownInitialization @GuardSatisfied PptSlice this); 194 195 /** Return an approximation of the number of distinct values seen on this slice. */ 196 public abstract int num_values(); 197 198 /** Instantiate invariants on the VarInfos this slice contains. */ 199 abstract void instantiate_invariants(); 200 201 /** 202 * This class is used for comparing PptSlice objects. It orders by arity, then by variable names. 203 * It's somewhat less efficient than ArityPptnameComparator. 204 */ 205 public static final class ArityVarnameComparator implements Comparator<PptSlice> { 206 @Pure 207 @Override 208 public int compare(PptSlice slice1, PptSlice slice2) { 209 if (slice1 == slice2) { 210 return 0; 211 } 212 // Don't do this assert, which prevents comparison across different Ppts. 213 // (The assert check may be useful in some situations, though.) 214 // assert slice1.parent == slice2.parent; 215 if (slice1.arity() != slice2.arity()) { 216 return slice2.arity() - slice1.arity(); 217 } 218 return Ppt.varNames(slice1.var_infos).compareTo(Ppt.varNames(slice2.var_infos)); 219 } 220 } 221 222 /** 223 * This class is used for comparing PptSlice objects. It orders by arity, then by name. Because of 224 * the dependence on name, it should be used only for slices on the same Ppt. 225 */ 226 public static final class ArityPptnameComparator implements Comparator<PptSlice> { 227 @Pure 228 @Override 229 public int compare(PptSlice slice1, PptSlice slice2) { 230 if (slice1 == slice2) { 231 return 0; 232 } 233 // Don't do this, to permit comparison across different Ppts. 234 // (The check may be useful in some situations, though.) 235 // assert slice1.parent == slice2.parent; 236 if (slice1.arity() != slice2.arity()) { 237 return slice2.arity() - slice1.arity(); 238 } 239 return slice1.name().compareTo(slice2.name()); 240 } 241 } 242 243 /////////////////////////////////////////////////////////////////////////// 244 /// Invariant guarding 245 246 public boolean containsOnlyGuardingPredicates() { 247 for (Invariant inv : invs) { 248 if (!inv.isGuardingPredicate) { 249 return false; 250 } 251 } 252 return true; 253 } 254 255 /////////////////////////////////////////////////////////////////////////// 256 /// Miscellaneous 257 258 /** Remove the invariants noted in omitTypes. */ 259 public void processOmissions(boolean[] omitTypes) { 260 if (invs.size() == 0) { 261 return; 262 } 263 List<Invariant> toRemove = new ArrayList<>(); 264 for (Invariant inv : invs) { 265 if (omitTypes['r'] && inv.isReflexive()) toRemove.add(inv); 266 } 267 removeInvariants(toRemove); 268 } 269 270 /** 271 * Check the internals of this slice. Each invariant in the slice is checked for consistency and 272 * each inv.ppt must equal this. 273 */ 274 public void repCheck() { 275 276 // System.out.printf("Checking slice %s%n", this); 277 278 // Make sure that each variable is a leader. There is one exception to this 279 // rule. Post processing of equality sets creates equality invariants between the 280 // various members of the equality set. Thus one non-leader is acceptable 281 // in binary (two variable) slices if it is in the same equality set as the 282 // other variable. 283 for (VarInfo vi : var_infos) { 284 // System.out.printf("equality set for vi %s = %s%n", vi, vi.equalitySet); 285 if (!vi.isCanonical()) { 286 assert var_infos.length == 2 : this + " - " + vi; 287 assert var_infos[0].canonicalRep() == var_infos[1].canonicalRep() : this + " - " + vi; 288 } 289 } 290 291 for (Invariant inv : invs) { 292 inv.repCheck(); 293 assert inv.ppt == this; 294 } 295 } 296 297 /** 298 * Clone self and replace this.var_infos with newVis. Do the same in all invariants that this 299 * holds. Return a new PptSlice that's like this except with the above replacement, along with 300 * correct flow pointers for varInfos. Invariants are also pivoted so that any VarInfo index order 301 * swapping is handled correctly. 302 * 303 * @param newVis to replace this.var_infos 304 * @return a new PptSlice that satisfies the characteristics above 305 */ 306 PptSlice cloneAndPivot(VarInfo[] newVis) { 307 throw new Error("Shouldn't get called"); 308 } 309 310 public PptSlice copy_new_invs(PptTopLevel ppt, VarInfo[] vis) { 311 throw new Error("Shouldn't get called"); 312 } 313 314 /** For debugging only. */ 315 @Override 316 @SuppressWarnings("all:purity") // string creation 317 @SideEffectFree 318 public String toString(@GuardSatisfied PptSlice this) { 319 StringBuilder sb = new StringBuilder(); 320 for (VarInfo vi : var_infos) { 321 sb.append(" " + vi.name()); 322 } 323 return this.getClass().getName() 324 + ": " 325 + parent.ppt_name 326 + " " 327 + sb 328 + " samples: " 329 + num_samples(); 330 } 331 332 /** 333 * Returns whether or not this slice already contains the specified invariant. Whether not 334 * invariants match is determine by Invariant.match() This will return true for invariants of the 335 * same kind with different formulas (eg, one_of, bound, linearbinary). 336 */ 337 public boolean contains_inv(Invariant inv) { 338 339 for (Invariant mine : invs) { 340 if (mine.match(inv)) { 341 return true; 342 } 343 } 344 return false; 345 } 346 347 /** 348 * Returns whether or not this slice contains an exact match for the specified invariant. An exact 349 * match requires that the invariants be of the same class and have the same formula. 350 */ 351 @EnsuresNonNullIf(result = true, expression = "find_inv_exact(#1)") 352 public boolean contains_inv_exact(Invariant inv) { 353 354 return (find_inv_exact(inv) != null); 355 } 356 357 /** 358 * Returns the invariant that matches the specified invariant if it exists. Otherwise returns 359 * null. An exact match requires that the invariants be of the same class and have the same 360 * formula. 361 */ 362 @Pure 363 public @Nullable Invariant find_inv_exact(Invariant inv) { 364 365 for (Invariant mine : invs) { 366 if ((mine.getClass() == inv.getClass()) && mine.isSameFormula(inv)) { 367 return mine; 368 } 369 } 370 return null; 371 } 372 373 /** 374 * Returns the invariant that matches the specified class if it exists. Otherwise returns null. 375 */ 376 public @Nullable Invariant find_inv_by_class(Class<? extends Invariant> cls) { 377 378 for (Invariant inv : invs) { 379 if ((inv.getClass() == cls)) { 380 return inv; 381 } 382 } 383 return null; 384 } 385 386 /** 387 * Returns true if the invariant is true in this slice. This can occur if the invariant exists in 388 * this slice, is suppressed, or is obvious statically. 389 */ 390 @Pure 391 public boolean is_inv_true(Invariant inv) { 392 393 if (contains_inv_exact(inv)) { 394 if (Debug.logOn() && (Daikon.current_inv != null)) { 395 Daikon.current_inv.log("inv %s exists", inv.format()); 396 } 397 return true; 398 } 399 400 // Check to see if the invariant is obvious statically over the leaders. 401 // This check should be sufficient since if it isn't obvious statically 402 // over the leaders, it should have been created. 403 DiscardInfo di = inv.isObviousStatically(var_infos); 404 if (di != null) { 405 if (Debug.logOn() && (Daikon.current_inv != null)) { 406 Daikon.current_inv.log("inv %s is obv statically", inv.format()); 407 } 408 return true; 409 } 410 411 boolean suppressed = inv.is_ni_suppressed(); 412 if (suppressed && Debug.logOn() && (Daikon.current_inv != null)) { 413 Daikon.current_inv.log("inv %s is ni suppressed", inv.format()); 414 } 415 return suppressed; 416 } 417 418 /** 419 * Output specified log information if the PtpSlice class, and this ppt and variables are enabled 420 * for logging. 421 */ 422 public void log(String msg) { 423 Debug.log(getClass(), this, msg); 424 } 425}