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