Source code

001// ***** This file is automatically generated from SubSet.java.jpp
002
003package daikon.inv.binary.twoSequence;
004
005import daikon.*;
006import daikon.inv.*;
007import daikon.suppress.*;
008import java.util.*;
009import java.util.logging.Level;
010import java.util.logging.Logger;
011import org.checkerframework.checker.lock.qual.GuardSatisfied;
012import org.checkerframework.checker.nullness.qual.NonNull;
013import org.checkerframework.checker.nullness.qual.Nullable;
014import org.checkerframework.dataflow.qual.Pure;
015import org.checkerframework.dataflow.qual.SideEffectFree;
016import org.plumelib.util.ArraysPlume;
017import typequals.prototype.qual.NonPrototype;
018import typequals.prototype.qual.Prototype;
019
020/**
021 * Represents two sequences of long values where one of the sequences is a subset of the other; that
022 * is each element of one sequence appears in the other. Prints as either
023 * {@code x[] is a subset of y[]} or as {@code x[] is a superset of y[]}.
024 */
025public class SuperSet extends TwoSequence {
026  static final long serialVersionUID = 20031024L;
027
028  private static final Logger debug =
029    Logger.getLogger("daikon.inv.binary.twoSequence.SuperSet");
030
031  // Variables starting with dkconfig_ should only be set via the
032  // daikon.config.Configuration interface.
033  /** Boolean. True iff SubSet invariants should be considered. */
034  public static boolean dkconfig_enabled = false;
035
036  protected SuperSet(PptSlice ppt) {
037    super(ppt);
038  }
039
040  protected @Prototype SuperSet() {
041    super();
042  }
043
044  private static @Prototype SuperSet proto = new @Prototype SuperSet();
045
046  /** Returns the prototype invariant for SuperSet */
047  public static @Prototype SuperSet get_proto() {
048    return proto;
049  }
050
051  @Override
052  public boolean enabled() {
053    return dkconfig_enabled;
054  }
055
056  @Override
057  public boolean instantiate_ok(VarInfo[] vis) {
058
059    if (!valid_types(vis)) {
060      return false;
061    }
062
063    return true;
064  }
065
066  @Override
067  public SuperSet instantiate_dyn(@Prototype SuperSet this, PptSlice slice) {
068    return new SuperSet(slice);
069  }
070
071  @Override
072  protected Invariant resurrect_done_swapped() {
073    return new SubSet(ppt);
074  }
075
076  @Override
077  public String repr(@GuardSatisfied SuperSet this) {
078    return "SuperSet" + varNames() + ": ,falsified=" + falsified;
079  }
080
081  @SideEffectFree
082  @Override
083  public String format_using(@GuardSatisfied SuperSet this, OutputFormat format) {
084    if (format == OutputFormat.DAIKON) {
085      return format();
086    }
087    if (format == OutputFormat.ESCJAVA) {
088      return format_esc();
089    }
090    if (format == OutputFormat.SIMPLIFY) {
091      return format_simplify();
092    }
093    if (format == OutputFormat.CSHARPCONTRACT) {
094      return format_csharp_contract();
095    }
096    if (format.isJavaFamily()) {
097      return format_java_family(format);
098    }
099
100    return format_unimplemented(format);
101  }
102
103  @SideEffectFree
104  @Override
105  public String format(@GuardSatisfied SuperSet this) {
106    String v1 = var1().name();
107    String v2 = var2().name();
108
109    return v1 + " is a superset of " + v2;
110  }
111
112  public String format_csharp_contract(@GuardSatisfied SuperSet this) {
113    String v1 = var1().csharp_collection_string();
114    String v2 = var2().csharp_collection_string();
115
116    return "Contract.ForAll(" + v2 + ", i => " + v1 + ".Contains(i))";
117  }
118
119  public String format_esc(@GuardSatisfied SuperSet this) {
120    String classname = this.getClass().toString().substring(6); // remove leading "class"
121    return "warning: method " + classname + ".format_esc() needs to be implemented: " + format();
122  }
123
124  public String format_simplify(@GuardSatisfied SuperSet this) {
125    if (Invariant.dkconfig_simplify_define_predicates) {
126      return format_simplify_defined();
127    } else {
128      return format_simplify_explicit();
129    }
130  }
131
132  private String format_simplify_defined(@GuardSatisfied SuperSet this) {
133
134    VarInfo subvar = var2();
135    VarInfo supervar = var1();
136
137    String[] sub_name = subvar.simplifyNameAndBounds();
138    String[] super_name = supervar.simplifyNameAndBounds();
139
140    if (sub_name == null || super_name == null) {
141      return String.format("%s.format_simplify_defined(%s): sub_name=%s, super_name=%s, for %s",
142                           getClass().getSimpleName(), this,
143                           Arrays.toString(sub_name), Arrays.toString(super_name), format());
144    }
145
146    return "(subset "
147      + sub_name[0] + " " + sub_name[1] + " " + sub_name[2] + " "
148      + super_name[0] + " " + super_name[1] + " " + super_name[2] + ")";
149  }
150
151  private String format_simplify_explicit(@GuardSatisfied SuperSet this) {
152
153    VarInfo subvar = var2();
154    VarInfo supervar = var1();
155
156    String[] sub_name = subvar.simplifyNameAndBounds();
157    String[] super_name = supervar.simplifyNameAndBounds();
158
159    if (sub_name == null || super_name == null) {
160      return String.format("%s.format_simplify_explicit(%s): sub_name=%s, super_name=%s, for %s",
161                           getClass().getSimpleName(), this,
162                           Arrays.toString(sub_name), Arrays.toString(super_name), format());
163    }
164
165    String indices[] = VarInfo.get_simplify_free_indices(subvar, supervar);
166
167    // (FORALL (a i j b ip jp)
168    //    (IFF (subset a i j b ip jp)
169    //         (FORALL (x)
170    //           (IMPLIES
171    //              (AND (<= i x) (<= x j))
172    //              (EXISTS (y)
173    //                  (AND (<= ip y) (<= y jp)
174    //                        (EQ (select (select elems a) x)
175    //                            (select (select elems b) y))))))))
176
177    return "(FORALL (" + indices[0] + ") (IMPLIES (AND (<= " + sub_name[1]
178      + " " + indices[0] + ") (<= " + indices[0] + " " + sub_name[2] + "))"
179      + "(EXISTS (" + indices[1] + ")(AND (<= " + super_name[1] + " "
180      + indices[1] + ") (<= " + indices[1] + " " + super_name[2]+ ")"
181      + "(EQ (select (select elems " + sub_name[0] + ") " + indices[0] + ") "
182      + "(select (select elems " + super_name[0] +") " + indices[1] + "))))))";
183
184  }
185
186  public String format_java_family(@GuardSatisfied SuperSet this, OutputFormat format) {
187
188    String v1 = var1().name_using(format);
189    String v2 = var2().name_using(format);
190
191    return "daikon.Quant.subsetOf(" + v2 + ", " + v1 + ")";
192  }
193
194  @Override
195  public InvariantStatus check_modified(long[] a1, long[] a2, int count) {
196
197    if (!ArraysPlume.isSubset(a2, a1)) {
198
199      return InvariantStatus.FALSIFIED;
200    } else {
201      return InvariantStatus.NO_CHANGE;
202    }
203
204  }
205
206  @Override
207  public InvariantStatus add_modified(long[] a1, long[] a2, int count) {
208    if (debug.isLoggable(Level.FINE)) {
209      debug.fine(Arrays.toString(a1));
210      debug.fine(Arrays.toString(a2));
211    }
212    return check_modified(a1, a2, count);
213  }
214
215  @Override
216  protected double computeConfidence() {
217    return Invariant.CONFIDENCE_JUSTIFIED;
218  }
219
220  // Convenience name to make this easier to find.
221  @Pure
222  public static @Nullable DiscardInfo isObviousSubSet(Invariant inv, VarInfo subvar, VarInfo supervar) {
223    return SubSequence.isObviousSubSequence(inv, subvar, supervar);
224  }
225
226  @Pure
227  @Override
228  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
229    VarInfo var1 = vis[0];
230    VarInfo var2 = vis[1];
231
232    DiscardInfo di;
233    di = SuperSet.isObviousSubSet(this, var1, var2);
234    if (di == null) {
235      di = SuperSet.isObviousSubSet(this, var2, var1);
236    }
237    if (di != null) {
238      return di;
239    }
240
241    VarInfo subvar, supervar;
242
243    subvar = var2;
244    supervar = var2;
245
246    // Uninteresting if this is of the form x[0..i] subsequence
247    // x[0..j].  Not necessarily obvious.
248    VarInfo subvar_super = subvar.isDerivedSubSequenceOf();
249    if (subvar_super == supervar) {
250      debug.fine("  returning true because subvar_super == supervar");
251      return new DiscardInfo(this, DiscardCode.obvious, "x[0..i] subsequence of x[0..j] is uninteresting");
252    }
253
254    VarInfo supervar_super = supervar.isDerivedSubSequenceOf();
255    if (subvar_super != null && subvar_super == supervar_super) {
256      debug.fine("  returning true because subvar_super == supervar_super");
257      return new DiscardInfo(this, DiscardCode.obvious, "x[0..i] subsequence of x[0..j] is uninteresting");
258    }
259
260    di = SubSequence.isObviousSubSequence(this, var1, var2);
261    if (di == null) {
262      di = SubSequence.isObviousSubSequence(this, var2, var1);
263    }
264    if (di != null) {
265      return di;
266    }
267    return super.isObviousStatically(vis);
268  }
269
270  // Look up a previously instantiated SubSet relationship.
271  public static @Nullable SuperSet find(PptSlice ppt) {
272    assert ppt.arity() == 2;
273    for (Invariant inv : ppt.invs) {
274      if (inv instanceof SuperSet) {
275        return (SuperSet) inv;
276      }
277    }
278    return null;
279  }
280
281  @Pure
282  @Override
283  public boolean isSameFormula(Invariant other) {
284    assert other instanceof SuperSet;
285    return true;
286  }
287
288  /** NI suppressions, initialized in get_ni_suppressions() */
289  private static @Nullable NISuppressionSet suppressions = null;
290
291  /** returns the ni-suppressions for SuperSet */
292  @Pure
293  @Override
294  public NISuppressionSet get_ni_suppressions() {
295    if (suppressions == null) {
296      NISuppressee suppressee = new NISuppressee(SuperSet.class, 2);
297
298      // suppressor definitions (used in suppressions below)
299      NISuppressor v1_eq_v2 = new NISuppressor(0, 1, SeqSeqIntEqual.class);
300      NISuppressor v1_pw_eq_v2 = new NISuppressor(0, 1, PairwiseIntEqual.class);
301
302      // sub/super set suppressions.  We have both SeqSeq and Pairwise
303      // as suppressions because each can be enabled separately.
304      suppressions = new NISuppressionSet(
305          new NISuppression[] {
306              // a[] == b[] ==> a[] sub/superset b[]
307              new NISuppression(v1_eq_v2, suppressee),
308              // a[] == b[] ==> a[] sub/superset b[]
309              new NISuppression(v1_pw_eq_v2, suppressee),
310          });
311    }
312
313    return suppressions;
314  }
315}