Source code

001// ***** This file is automatically generated from OneOf.java.jpp
002
003package daikon.inv.unary.string;
004
005import daikon.*;
006import daikon.inv.*;
007import daikon.inv.unary.OneOf;
008
009import java.io.*;
010import java.util.logging.Logger;
011import java.util.logging.Level;
012import java.util.*;
013
014import java.util.Comparator;
015
016  import java.util.regex.*;
017
018import org.checkerframework.checker.initialization.qual.Initialized;
019import org.checkerframework.checker.interning.qual.Interned;
020import org.checkerframework.checker.lock.qual.GuardSatisfied;
021import org.checkerframework.checker.nullness.qual.NonNull;
022import org.checkerframework.checker.nullness.qual.Nullable;
023import org.checkerframework.dataflow.qual.Pure;
024import org.checkerframework.dataflow.qual.SideEffectFree;
025import org.checkerframework.framework.qual.Unused;
026import daikon.SignaturesUtil;
027import org.plumelib.reflection.Signatures;
028import org.plumelib.util.ArraysPlume;
029import org.plumelib.util.Intern;
030import org.plumelib.util.StringsPlume;
031import org.plumelib.util.UtilPlume;
032import typequals.prototype.qual.NonPrototype;
033import typequals.prototype.qual.Prototype;
034
035// This subsumes an "exact" invariant that says the value is always exactly
036// a specific value.  Do I want to make that a separate invariant
037// nonetheless?  Probably not, as this will simplify implication and such.
038
039  /**
040   * Represents String variables that take on only a few distinct values. Prints as either
041   * {@code x == c} (when there is only one value) or as {@code x one of {c1, c2, c3}}
042   * (when there are multiple values).
043
044   */
045
046@SuppressWarnings("UnnecessaryParentheses")  // generated code, parentheses are sometimes needed
047public final class OneOfString extends SingleString implements OneOf {
048  static final long serialVersionUID = 20030822L;
049
050  /** Debugging logger. */
051  public static final Logger debug =
052    Logger.getLogger(OneOfString.class.getName());
053
054  // Variables starting with dkconfig_ should only be set via the
055  // daikon.config.Configuration interface.
056  /** Boolean. True iff OneOf invariants should be considered. */
057  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
058
059  /**
060   * Positive integer. Specifies the maximum set size for this type of invariant (x is one of
061   * {@code size} items).
062   */
063
064  public static int dkconfig_size = 3;
065
066  // Probably needs to keep its own list of the values, and number of each seen.
067  // (That depends on the slice; maybe not until the slice is cleared out.
068  // But so few values is cheap, so this is quite fine for now and long-term.)
069
070  @Unused(when=Prototype.class)
071  private @Interned String[] elts;
072  @Unused(when=Prototype.class)
073  private int num_elts;
074
075  @Prototype OneOfString() {
076    super();
077  }
078
079  OneOfString(PptSlice slice) {
080    super(slice);
081
082    elts = new @Interned String[dkconfig_size];
083
084    num_elts = 0;
085
086  }
087
088  private static @Prototype OneOfString proto = new @Prototype OneOfString();
089
090  /** Returns the prototype invariant for OneOfString */
091  public static @Prototype OneOfString get_proto() {
092    return proto;
093  }
094
095  @Override
096  public boolean enabled() {
097    return dkconfig_enabled;
098  }
099
100  @Override
101  public OneOfString instantiate_dyn(@Prototype OneOfString this, PptSlice slice) {
102    return new OneOfString(slice);
103  }
104
105  @Pure
106  public boolean is_boolean(@GuardSatisfied OneOfString this) {
107    return var().file_rep_type.elementType() == ProglangType.BOOLEAN;
108  }
109  @Pure
110  public boolean is_hashcode(@GuardSatisfied OneOfString this) {
111    return var().file_rep_type.elementType() == ProglangType.HASHCODE;
112  }
113
114  @SideEffectFree
115  @Override
116  public OneOfString clone(@GuardSatisfied OneOfString this) {
117    OneOfString result = (OneOfString) super.clone();
118    result.elts = elts.clone();
119
120    result.num_elts = this.num_elts;
121    return result;
122  }
123
124  @Override
125  public int num_elts() {
126    return num_elts;
127  }
128
129  @Override
130  public Object elt() {
131    return elt(0);
132  }
133
134  public Object elt(int index) {
135    if (num_elts <= index) {
136      throw new Error("Represents " + num_elts + " elements, index " + index + " not valid");
137    }
138
139    return elts[index];
140  }
141
142  static Comparator<@Nullable String> comparator = Comparator.nullsFirst(Comparator.naturalOrder());
143
144  private void sort_rep(@GuardSatisfied OneOfString this) {
145    Arrays.sort(elts, 0, num_elts , comparator);
146  }
147
148  public @Interned String min_elt() {
149    if (num_elts == 0) {
150      throw new Error("Represents no elements");
151    }
152    sort_rep();
153    return elts[0];
154  }
155
156  public @Interned String max_elt() {
157    if (num_elts == 0) {
158      throw new Error("Represents no elements");
159    }
160    sort_rep();
161    return elts[num_elts - 1];
162  }
163
164  // Assumes the other array is already sorted
165  public boolean compare_rep(int num_other_elts, @Interned String[] other_elts) {
166    if (num_elts != num_other_elts) {
167      return false;
168    }
169    sort_rep();
170    for (int i = 0; i < num_elts; i++) {
171      if (!((elts[i]) == (other_elts[i]))) { // elements are interned
172        return false;
173      }
174    }
175    return true;
176  }
177
178  private String subarray_rep(@GuardSatisfied OneOfString this) {
179    // Not so efficient an implementation, but simple;
180    // and how often will we need to print this anyway?
181    sort_rep();
182    StringJoiner sj = new StringJoiner(", ", "{ ", " }");
183    for (int i = 0; i < num_elts; i++) {
184
185      if (PrintInvariants.dkconfig_static_const_infer) {
186        boolean curVarMatch = false;
187        PptTopLevel pptt = ppt.parent;
188        for (VarInfo vi : pptt.var_infos) {
189          if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
190            Object constantVal = vi.constantValue();
191            if (constantVal.equals(elts[i])) {
192              sj.add(vi.name());
193              curVarMatch = true;
194            }
195          }
196        }
197
198        if (curVarMatch == false) {
199          sj.add(((elts[i] == null) ? "null" : "\"" + StringsPlume.escapeNonASCII(elts[i]) + "\""));
200        }
201      } else {
202        sj.add(((elts[i] == null) ? "null" : "\"" + StringsPlume.escapeNonASCII(elts[i]) + "\""));
203      }
204
205    }
206    return sj.toString();
207  }
208
209  @Override
210  public String repr(@GuardSatisfied OneOfString this) {
211    return "OneOfString" + varNames() + ": falsified=" + falsified
212      + ", num_elts=" + num_elts
213      + ", elts=" + subarray_rep();
214  }
215
216  public @Interned String[] getElts() {
217    @Interned String[] temp = new @Interned String[elts.length];
218    for (int i = 0; i < elts.length; i++) {
219      temp[i] = elts[i];
220    }
221    return temp;
222  }
223
224  @SideEffectFree
225  @Override
226  public String format_using(@GuardSatisfied OneOfString this, OutputFormat format) {
227    sort_rep();
228
229    if (format.isJavaFamily()) {
230      return format_java_family(format);
231    }
232
233    if (format == OutputFormat.DAIKON) {
234      return format_daikon();
235    } else if (format == OutputFormat.SIMPLIFY) {
236      return format_simplify();
237    } else if (format == OutputFormat.ESCJAVA) {
238      String result = format_esc();
239      return result;
240    } else if (format == OutputFormat.CSHARPCONTRACT) {
241      return format_csharp_contract();
242    } else {
243      return format_unimplemented(format);
244    }
245  }
246
247  public String format_daikon(@GuardSatisfied OneOfString this) {
248    String varname = var().name();
249    if (num_elts == 1) {
250
251        boolean is_type = is_type();
252        if (!is_type) {
253          return varname + " == " + ((elts[0] == null) ? "null" : "\"" + StringsPlume.escapeNonASCII(elts[0]) + "\"");
254        } else {
255          // It's a type
256          String str = elts[0];
257          if ((str == null) || "null".equals(str)) {
258            return varname + " == null";
259          } else {
260            if (str.startsWith("[")) {
261              @SuppressWarnings("signature")
262              String tempStr = Signatures.fieldDescriptorToBinaryName(str);
263              str = tempStr;
264            }
265            if (PrintInvariants.dkconfig_static_const_infer) {
266              PptTopLevel pptt = ppt.parent;
267              for (VarInfo vi : pptt.var_infos) {
268                if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
269                  Object constantVal = vi.constantValue();
270                  if (constantVal.equals(str)) {
271                    return varname + " == " + vi.name();
272                  }
273                }
274              }
275            }
276            // ".class" (which is a suffix for a type name) and not
277            // getClassSuffix (which is a suffix for an expression).
278            return varname + " == " + str + ".class";
279          }
280        }
281
282    } else {
283      return varname + " one of " + subarray_rep();
284    }
285  }
286
287  @Pure
288  private boolean is_type(@GuardSatisfied OneOfString this) {
289    return var().has_typeof();
290  }
291
292  private static Pattern dollar_char_pat = Pattern.compile("\\$([A-Za-z])");
293
294  private static String format_esc_string2type(String str) {
295    if ((str == null) || "null".equals(str)) {
296      return "\\typeof(null)";
297    }
298    String type_str;
299    if (str.startsWith("[")) {
300      @SuppressWarnings("signature")
301      String temp_type_str = Signatures.fieldDescriptorToBinaryName(str);
302      type_str = temp_type_str;
303    } else {
304      type_str = str;
305      if (type_str.startsWith("\"") && type_str.endsWith("\"")) {
306        type_str = type_str.substring(1, type_str.length()-1);
307      }
308    }
309
310    // Inner classes
311    // type_str = type_str.replace('$', '.');
312    // For named inner classes, convert "$" to ".".
313    // For anonymous inner classes, leave as "$".
314    Matcher m = dollar_char_pat.matcher(type_str);
315    type_str = m.replaceAll(".$1");
316
317    return "\\type(" + type_str + ")";
318  }
319
320  public String format_esc(@GuardSatisfied OneOfString this) {
321    sort_rep();
322
323    String varname = var().esc_name();
324
325    String result;
326
327    // We cannot say anything about Strings in ESC, just types (which
328    // Daikon stores as Strings).
329    if (!is_type()) {
330      result = format_unimplemented(OutputFormat.ESCJAVA); // "needs to be implemented"
331    } else {
332      // Format   \typeof(theArray) = "[Ljava.lang.Object;"
333      //   as     \typeof(theArray) == \type(java.lang.Object[])
334      // ... but still ...
335      // format   \typeof(other) = "package.SomeClass;"
336      //   as     \typeof(other) == \type(package.SomeClass)
337
338      result = "";
339      for (int i = 0; i < num_elts; i++) {
340        if (i != 0) { result += " || "; }
341        result += varname + " == " + format_esc_string2type(elts[i]);
342      }
343    }
344
345    return result;
346  }
347
348public String format_csharp_contract(@GuardSatisfied OneOfString this) {
349
350    @NonNull @Initialized String result;
351
352  String varname = var().csharp_name();
353
354    if (is_type()) {
355        List<String> names = new ArrayList<>();
356        for (int i = 0; i < num_elts; i++) {
357             String str = elts[i];
358             if ((str == null) || "null".equals(str)) {
359                 names.add(varname + " == null");
360             } else {
361                 names.add(varname + " == typeof(" + str + ")");
362             }
363        }
364        result = String.join(" || ", names);
365    } else if (num_elts == 1) {
366        String str = elts[0];
367        result = (str == null || "null".equals(str))
368               ? (varname + " == null")
369               : (varname + ".Equals(" + ((str == null) ? "null" : "\"" + StringsPlume.escapeNonASCII(str) + "\"") + ")");
370    } else {
371        List<String> names = new ArrayList<>();
372        for (int i = 0; i < num_elts; i++) {
373            String str = elts[i];
374            names.add((str == null) ? "null" : ((str == null) ? "null" : "\"" + StringsPlume.escapeNonASCII(str) + "\""));
375        }
376        result = varname + ".OneOf(" + String.join(", ", names) + ")";
377    }
378
379    return result;
380  }
381
382  public String format_java_family(@GuardSatisfied OneOfString this, OutputFormat format) {
383
384    String result;
385
386    // Setting up the name of the unary variable
387    String varname = var().name_using(format);
388
389    result = "";
390    boolean is_type = is_type();
391    for (int i = 0; i < num_elts; i++) {
392      if (i != 0) {
393        result += " || ";
394      }
395      String str = elts[i];
396      if (!is_type) {
397        result += varname + ".equals(" + ((str == null) ? "null" : "\"" + StringsPlume.escapeNonASCII(str) + "\"") + ")";
398      } else {
399        // It's a type
400        if ((str == null) || "null".equals(str)) {
401          result += varname + " == null";
402        } else {
403          if (str.startsWith("[")) {
404            @SuppressWarnings("signature")
405            String tempStr = Signatures.fieldDescriptorToBinaryName(str);
406            str = tempStr;
407          }
408          // ".class" (which is a suffix for a type name) and not
409          // getClassSuffix (which is a suffix for an expression).
410          // we need ".class.getName()" to make result a string
411          result += varname + " == " + str + ".class.getName()";
412        }
413      }
414    }
415
416    return result;
417  }
418
419  public String format_simplify(@GuardSatisfied OneOfString this) {
420
421    sort_rep();
422
423    String varname =
424      var().simplifyFixup(var().name_using(OutputFormat.SIMPLIFY));
425
426    String result;
427
428    result = "";
429    boolean is_type = is_type();
430    for (int i = 0; i < num_elts; i++) {
431      String value = elts[i];
432      if (is_type) {
433        if (value == null) {
434          // do nothing
435        } else if (value.startsWith("[")) {
436          @SuppressWarnings("signature")
437          String tempValue = Signatures.fieldDescriptorToBinaryName(value);
438          value = tempValue;
439        } else if (value.startsWith("\"") && value.endsWith("\"")) {
440          value = value.substring(1, value.length()-1);
441        }
442        value = "|T_" + value + "|";
443      } else {
444        value = simplify_format_string(value);
445      }
446      result += " (EQ " + varname + " " + value + ")";
447    }
448    if (num_elts > 1) {
449      result = "(OR" + result + ")";
450    } else if (num_elts == 1) {
451      // chop leading space
452      result = result.substring(1);
453    } else if (num_elts == 0) {
454      return format_too_few_samples(OutputFormat.SIMPLIFY, null);
455    }
456
457    if (result.indexOf("format_simplify") == -1) {
458      daikon.simplify.SimpUtil.assert_well_formed(result);
459    }
460    return result;
461  }
462
463  @Override
464  public InvariantStatus add_modified(@Interned String a, int count) {
465    return runValue(a, count, true);
466  }
467
468  @Override
469  public InvariantStatus check_modified(@Interned String a, int count) {
470    return runValue(a, count, false);
471  }
472
473  private InvariantStatus runValue(@Interned String v, int count, boolean mutate) {
474    InvariantStatus status;
475    if (mutate) {
476      status = add_mod_elem(v, count);
477    } else {
478      status = check_mod_elem(v, count);
479    }
480    if (status == InvariantStatus.FALSIFIED) {
481      if (logOn() && mutate) {
482        StringBuilder eltString = new StringBuilder();
483        for (int i = 0; i < num_elts; i++) {
484          eltString.append(((elts[i] == null) ? "null" : "\"" + StringsPlume.escapeNonASCII(elts[i]) + "\"") + " ");
485        }
486        log("destroyed on sample %s previous vals = {%s} num_elts = %s",
487             ((v == null) ? "null" : "\"" + StringsPlume.escapeNonASCII(v) + "\""), eltString, num_elts);
488      }
489      return InvariantStatus.FALSIFIED;
490    }
491    return status;
492  }
493
494  /**
495   * Adds a single sample to the invariant. Returns
496   * the appropriate InvariantStatus from the result
497   * of adding the sample to this.
498   */
499  public InvariantStatus add_mod_elem(@Interned String v, int count) {
500    InvariantStatus status = check_mod_elem(v, count);
501    if (status == InvariantStatus.WEAKENED) {
502      elts[num_elts] = v;
503      num_elts++;
504    }
505    return status;
506  }
507
508  /**
509   * Checks a single sample to the invariant. Returns
510   * the appropriate InvariantStatus from the result
511   * of adding the sample to this.
512   */
513  public InvariantStatus check_mod_elem(@Interned String v, int count) {
514
515    // Look for v in our list of previously seen values.  If it's
516    // found, we're all set.
517    for (int i = 0; i < num_elts; i++) {
518      // if (logDetail())
519      //  log ("add_modified (" + v + ")");
520      if (((elts[i]) == ( v))) {
521        return InvariantStatus.NO_CHANGE;
522      }
523    }
524
525    if (num_elts == dkconfig_size) {
526      return InvariantStatus.FALSIFIED;
527    }
528
529    if (is_type() && (num_elts == 1)) {
530      return InvariantStatus.FALSIFIED;
531    }
532
533    return InvariantStatus.WEAKENED;
534  }
535
536  @Override
537  protected double computeConfidence() {
538    // This is not ideal.
539    if (num_elts == 0) {
540      return Invariant.CONFIDENCE_UNJUSTIFIED;
541    } else {
542      return Invariant.CONFIDENCE_JUSTIFIED;
543    }
544  }
545
546  @Pure
547  @Override
548  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
549    // Static constants are necessarily OneOf precisely one value.
550    // This removes static constants from the output, which might not be
551    // desirable if the user doesn't know their actual value.
552    if (vis[0].isStaticConstant()) {
553      assert num_elts <= 1;
554      return new DiscardInfo(this, DiscardCode.obvious, vis[0].name() + " is a static constant.");
555    }
556    return super.isObviousStatically(vis);
557  }
558
559  @Override
560  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
561    DiscardInfo super_result = super.isObviousDynamically(vis);
562    if (super_result != null) {
563      return super_result;
564    }
565
566    VarInfo v = vis[0];
567
568    // We can check if all values in the list match with the ones we know about
569    // (useful for booleans and numeric enumerations).
570    if (v.aux.hasValue(VarInfoAux.VALID_VALUES)) {
571      String[] vsValidValues         = v.aux.getList(VarInfoAux.VALID_VALUES);
572      Set<@Interned String> setValidValues = new TreeSet<>();
573      for (String s : vsValidValues) {
574        setValidValues.add(s.intern());
575      }
576      Set<@Interned String> setValuesInvariant = new TreeSet<>();
577      for (@Interned String e : elts) {
578        if (e == null) {
579  continue;
580}
581        setValuesInvariant.add(e);
582      }
583
584      if (setValidValues.equals(setValuesInvariant)) {
585        return new DiscardInfo(this, DiscardCode.obvious,
586          "The value list consists of all possible values");
587      }
588    }
589
590    return null;
591  }
592
593  /**
594   * Oneof can merge different formulas from lower points to create a single formula at an upper
595   * point.
596   */
597  @Override
598  public boolean mergeFormulasOk() {
599    return true;
600  }
601
602  @Pure
603  @Override
604  public boolean isSameFormula(Invariant o) {
605    OneOfString other = (OneOfString) o;
606    if (num_elts != other.num_elts) {
607      return false;
608    }
609    if (num_elts == 0 && other.num_elts == 0) {
610      return true;
611    }
612
613    sort_rep();
614    other.sort_rep();
615
616    for (int i = 0; i < num_elts; i++) {
617      if (!((elts[i]) == (other.elts[i]))) {
618        return false;
619      }
620    }
621
622    return true;
623  }
624
625  @Pure
626  @Override
627  public boolean isExclusiveFormula(Invariant o) {
628    if (o instanceof OneOfString) {
629      OneOfString other = (OneOfString) o;
630
631      if (num_elts == 0 || other.num_elts == 0) {
632        return false;
633      }
634      for (int i = 0; i < num_elts; i++) {
635        for (int j = 0; j < other.num_elts; j++) {
636          if (((elts[i]) == (other.elts[j]))) // elements are interned
637            return false;
638        }
639      }
640
641      return true;
642    }
643
644    return false;
645  }
646
647  @Override
648  public boolean hasUninterestingConstant() {
649
650    return false;
651  }
652
653  @Pure
654  @Override
655  public boolean isExact() {
656    return num_elts == 1;
657  }
658
659  // Look up a previously instantiated invariant.
660  public static @Nullable OneOfString find(PptSlice ppt) {
661    assert ppt.arity() == 1;
662    for (Invariant inv : ppt.invs) {
663      if (inv instanceof OneOfString) {
664        return (OneOfString) inv;
665      }
666    }
667    return null;
668  }
669
670  // Interning is lost when an object is serialized and deserialized.
671  // Manually re-intern any interned fields upon deserialization.
672  private void readObject(ObjectInputStream in) throws IOException,
673    ClassNotFoundException {
674    in.defaultReadObject();
675
676    for (int i = 0; i < num_elts; i++) {
677      elts[i] = Intern.intern(elts[i]);
678    }
679  }
680
681  /**
682   * Merge the invariants in invs to form a new invariant. Each must be a OneOfString invariant.
683   * This code finds all of the oneof values from each of the invariants and returns the merged
684   * invariant (if any).
685   *
686   * @param invs list of invariants to merge. The invariants must all be of the same type and should
687   *     come from the children of parent_ppt. They should also all be permuted to match the
688   *     variable order in parent_ppt.
689   * @param parent_ppt slice that will contain the new invariant
690   */
691  @Override
692  public @Nullable OneOfString merge(List<Invariant> invs, PptSlice parent_ppt) {
693
694    // Create the initial parent invariant from the first child
695    OneOfString  first = (OneOfString) invs.get(0);
696    OneOfString result = first.clone();
697    result.ppt = parent_ppt;
698
699    // Loop through the rest of the child invariants
700    for (int i = 1; i < invs.size(); i++ ) {
701
702      // Get this invariant
703      OneOfString inv = (OneOfString) invs.get(i);
704
705      // Loop through each distinct value found in this child and add
706      // it to the parent.  If the invariant is falsified, there is no parent
707      // invariant
708      for (int j = 0; j < inv.num_elts; j++) {
709        @Interned String val = inv.elts[j];
710
711        InvariantStatus status = result.add_mod_elem(val, 1);
712        if (status == InvariantStatus.FALSIFIED) {
713
714          result.log("%s", "child value '" + val + "' destroyed oneof");
715
716          return null;
717        }
718      }
719    }
720
721    result.log("Merged '%s' from %s child invariants", result.format(), invs.size());
722    return result;
723  }
724
725  /**
726   * Setup the invariant with the specified elements. Normally used when searching for a specified
727   * OneOf. The elements of vals are not necessarily interned; this method interns each element.
728   */
729  public void set_one_of_val(String[] vals) {
730
731    num_elts = vals.length;
732    for (int i = 0; i < num_elts; i++) {
733      elts[i] = Intern.intern(vals[i]);
734    }
735  }
736
737  /**
738   * Returns true if every element in this invariant is contained in the specified state. For
739   * example if x = 1 and the state contains 1 and 2, true will be returned.
740   */
741  @Override
742  public boolean state_match(Object state) {
743
744    if (num_elts == 0) {
745      return false;
746    }
747
748    if (!(state instanceof @Interned String[])) {
749      // Daikon is about to crash.  Produce some debugging output.
750      System.out.printf("state = %s [%s]%n", state, state.getClass());
751      System.out.printf("problem with %s%n", this);
752    }
753    @Interned String[] e = (@Interned String[]) state;
754    for (int i = 0; i < num_elts; i++) {
755      boolean match = false;
756      for (int j = 0; j < e.length; j++) {
757        if (elts[i] == e[j]) {
758          match = true;
759          break;
760        }
761      }
762      if (!match) {
763        return false;
764      }
765    }
766    return true;
767  }
768
769}