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 org.plumelib.reflection.Signatures;
027import org.plumelib.util.ArraysPlume;
028import org.plumelib.util.Intern;
029import org.plumelib.util.StringsPlume;
030import org.plumelib.util.UtilPlume;
031import typequals.prototype.qual.NonPrototype;
032import typequals.prototype.qual.Prototype;
033
034// This subsumes an "exact" invariant that says the value is always exactly
035// a specific value.  Do I want to make that a separate invariant
036// nonetheless?  Probably not, as this will simplify implication and such.
037
038  /**
039   * Represents String variables that take on only a few distinct values. Prints as either
040   * {@code x == c} (when there is only one value) or as {@code x one of {c1, c2, c3}}
041   * (when there are multiple values).
042
043   */
044
045@SuppressWarnings("UnnecessaryParentheses")  // generated code, parentheses are sometimes needed
046public final class OneOfString extends SingleString implements OneOf {
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 = 20030822L;
051
052  /** Debugging logger. */
053  public static final Logger debug =
054    Logger.getLogger(OneOfString.class.getName());
055
056  // Variables starting with dkconfig_ should only be set via the
057  // daikon.config.Configuration interface.
058  /** Boolean. True iff OneOf invariants should be considered. */
059  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
060
061  /**
062   * Positive integer. Specifies the maximum set size for this type of invariant (x is one of
063   * {@code size} items).
064   */
065
066  public static int dkconfig_size = 3;
067
068  // Probably needs to keep its own list of the values, and number of each seen.
069  // (That depends on the slice; maybe not until the slice is cleared out.
070  // But so few values is cheap, so this is quite fine for now and long-term.)
071
072  @Unused(when=Prototype.class)
073  private @Interned String[] elts;
074  @Unused(when=Prototype.class)
075  private int num_elts;
076
077  @Prototype OneOfString() {
078    super();
079  }
080
081  OneOfString(PptSlice slice) {
082    super(slice);
083
084    elts = new @Interned String[dkconfig_size];
085
086    num_elts = 0;
087
088  }
089
090  private static @Prototype OneOfString proto = new @Prototype OneOfString();
091
092  /** Returns the prototype invariant for OneOfString */
093  public static @Prototype OneOfString get_proto() {
094    return proto;
095  }
096
097  /** returns whether or not this invariant is enabled */
098  @Override
099  public boolean enabled() {
100    return dkconfig_enabled;
101  }
102
103  /** instantiate an invariant on the specified slice */
104  @Override
105  public OneOfString instantiate_dyn(@Prototype OneOfString this, PptSlice slice) {
106    return new OneOfString(slice);
107  }
108
109  @Pure
110  public boolean is_boolean(@GuardSatisfied OneOfString this) {
111    return var().file_rep_type.elementType() == ProglangType.BOOLEAN;
112  }
113  @Pure
114  public boolean is_hashcode(@GuardSatisfied OneOfString this) {
115    return var().file_rep_type.elementType() == ProglangType.HASHCODE;
116  }
117
118  @SideEffectFree
119  @Override
120  public OneOfString clone(@GuardSatisfied OneOfString this) {
121    OneOfString result = (OneOfString) super.clone();
122    result.elts = elts.clone();
123
124    result.num_elts = this.num_elts;
125    return result;
126  }
127
128  @Override
129  public int num_elts() {
130    return num_elts;
131  }
132
133  @Override
134  public Object elt() {
135    return elt(0);
136  }
137
138  public Object elt(int index) {
139    if (num_elts <= index) {
140      throw new Error("Represents " + num_elts + " elements, index " + index + " not valid");
141    }
142
143    return elts[index];
144  }
145
146  static Comparator<@Nullable String> comparator = Comparator.nullsFirst(Comparator.naturalOrder());
147
148  private void sort_rep(@GuardSatisfied OneOfString this) {
149    Arrays.sort(elts, 0, num_elts , comparator);
150  }
151
152  public @Interned String min_elt() {
153    if (num_elts == 0) {
154      throw new Error("Represents no elements");
155    }
156    sort_rep();
157    return elts[0];
158  }
159
160  public @Interned String max_elt() {
161    if (num_elts == 0) {
162      throw new Error("Represents no elements");
163    }
164    sort_rep();
165    return elts[num_elts - 1];
166  }
167
168  // Assumes the other array is already sorted
169  public boolean compare_rep(int num_other_elts, @Interned String[] other_elts) {
170    if (num_elts != num_other_elts) {
171      return false;
172    }
173    sort_rep();
174    for (int i = 0; i < num_elts; i++) {
175      if (!((elts[i]) == (other_elts[i]))) { // elements are interned
176        return false;
177      }
178    }
179    return true;
180  }
181
182  private String subarray_rep(@GuardSatisfied OneOfString this) {
183    // Not so efficient an implementation, but simple;
184    // and how often will we need to print this anyway?
185    sort_rep();
186    StringBuilder sb = new StringBuilder();
187    sb.append("{ ");
188    for (int i = 0; i < num_elts; i++) {
189      if (i != 0) {
190        sb.append(", ");
191      }
192
193      if (PrintInvariants.dkconfig_static_const_infer) {
194        boolean curVarMatch = false;
195        PptTopLevel pptt = ppt.parent;
196        for (VarInfo vi : pptt.var_infos) {
197          if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
198            Object constantVal = vi.constantValue();
199            if (constantVal.equals(elts[i])) {
200              sb.append(vi.name());
201              curVarMatch = true;
202            }
203          }
204        }
205
206        if (curVarMatch == false) {
207          sb.append(((elts[i] == null) ? "null" : "\"" + StringsPlume.escapeNonASCII(elts[i]) + "\""));
208        }
209      } else {
210        sb.append(((elts[i] == null) ? "null" : "\"" + StringsPlume.escapeNonASCII(elts[i]) + "\""));
211      }
212
213    }
214    sb.append(" }");
215    return sb.toString();
216  }
217
218  @Override
219  public String repr(@GuardSatisfied OneOfString this) {
220    return "OneOfString" + varNames() + ": falsified=" + falsified
221      + ", num_elts=" + num_elts
222      + ", elts=" + subarray_rep();
223  }
224
225  public @Interned String[] getElts() {
226    @Interned String[] temp = new @Interned String[elts.length];
227    for (int i = 0; i < elts.length; i++) {
228      temp[i] = elts[i];
229    }
230    return temp;
231  }
232
233  @SideEffectFree
234  @Override
235  public String format_using(@GuardSatisfied OneOfString this, OutputFormat format) {
236    sort_rep();
237
238    if (format.isJavaFamily()) {
239      return format_java_family(format);
240    }
241
242    if (format == OutputFormat.DAIKON) {
243      return format_daikon();
244    } else if (format == OutputFormat.SIMPLIFY) {
245      return format_simplify();
246    } else if (format == OutputFormat.ESCJAVA) {
247      String result = format_esc();
248      return result;
249    } else if (format == OutputFormat.CSHARPCONTRACT) {
250      return format_csharp_contract();
251    } else {
252      return format_unimplemented(format);
253    }
254  }
255
256  public String format_daikon(@GuardSatisfied OneOfString this) {
257    String varname = var().name();
258    if (num_elts == 1) {
259
260        boolean is_type = is_type();
261        if (!is_type) {
262          return varname + " == " + ((elts[0] == null) ? "null" : "\"" + StringsPlume.escapeNonASCII(elts[0]) + "\"");
263        } else {
264          // It's a type
265          String str = elts[0];
266          if ((str == null) || "null".equals(str)) {
267            return varname + " == null";
268          } else {
269            if (str.startsWith("[")) {
270              str = Signatures.fieldDescriptorToBinaryName(str);
271            }
272            if (PrintInvariants.dkconfig_static_const_infer) {
273              PptTopLevel pptt = ppt.parent;
274              for (VarInfo vi : pptt.var_infos) {
275                if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
276                  Object constantVal = vi.constantValue();
277                  if (constantVal.equals(str)) {
278                    return varname + " == " + vi.name();
279                  }
280                }
281              }
282            }
283            // ".class" (which is a suffix for a type name) and not
284            // getClassSuffix (which is a suffix for an expression).
285            return varname + " == " + str + ".class";
286          }
287        }
288
289    } else {
290      return varname + " one of " + subarray_rep();
291    }
292  }
293
294  @Pure
295  private boolean is_type(@GuardSatisfied OneOfString this) {
296    return var().has_typeof();
297  }
298
299  private static Pattern dollar_char_pat = Pattern.compile("\\$([A-Za-z])");
300
301  private static String format_esc_string2type(String str) {
302    if ((str == null) || "null".equals(str)) {
303      return "\\typeof(null)";
304    }
305    String type_str;
306    if (str.startsWith("[")) {
307      type_str = Signatures.fieldDescriptorToBinaryName(str);
308    } else {
309      type_str = str;
310      if (type_str.startsWith("\"") && type_str.endsWith("\"")) {
311        type_str = type_str.substring(1, type_str.length()-1);
312      }
313    }
314
315    // Inner classes
316    // type_str = type_str.replace('$', '.');
317    // For named inner classes, convert "$" to ".".
318    // For anonymous inner classes, leave as "$".
319    Matcher m = dollar_char_pat.matcher(type_str);
320    type_str = m.replaceAll(".$1");
321
322    return "\\type(" + type_str + ")";
323  }
324
325  public String format_esc(@GuardSatisfied OneOfString this) {
326    sort_rep();
327
328    String varname = var().esc_name();
329
330    String result;
331
332    // We cannot say anything about Strings in ESC, just types (which
333    // Daikon stores as Strings).
334    if (!is_type()) {
335      result = format_unimplemented(OutputFormat.ESCJAVA); // "needs to be implemented"
336    } else {
337      // Format   \typeof(theArray) = "[Ljava.lang.Object;"
338      //   as     \typeof(theArray) == \type(java.lang.Object[])
339      // ... but still ...
340      // format   \typeof(other) = "package.SomeClass;"
341      //   as     \typeof(other) == \type(package.SomeClass)
342
343      result = "";
344      for (int i = 0; i < num_elts; i++) {
345        if (i != 0) { result += " || "; }
346        result += varname + " == " + format_esc_string2type(elts[i]);
347      }
348    }
349
350    return result;
351  }
352
353public String format_csharp_contract(@GuardSatisfied OneOfString this) {
354
355    @NonNull @Initialized String result;
356
357  String varname = var().csharp_name();
358
359    if (is_type()) {
360        List<String> names = new ArrayList<>();
361        for (int i = 0; i < num_elts; i++) {
362             String str = elts[i];
363             if ((str == null) || "null".equals(str)) {
364                 names.add(varname + " == null");
365             } else {
366                 names.add(varname + " == typeof(" + str + ")");
367             }
368        }
369        result = String.join(" || ", names);
370    } else if (num_elts == 1) {
371        String str = elts[0];
372        result = (str == null || "null".equals(str))
373               ? (varname + " == null")
374               : (varname + ".Equals(" + ((str == null) ? "null" : "\"" + StringsPlume.escapeNonASCII(str) + "\"") + ")");
375    } else {
376        List<String> names = new ArrayList<>();
377        for (int i = 0; i < num_elts; i++) {
378            String str = elts[i];
379            names.add((str == null) ? "null" : ((str == null) ? "null" : "\"" + StringsPlume.escapeNonASCII(str) + "\""));
380        }
381        result = varname + ".OneOf(" + String.join(", ", names) + ")";
382    }
383
384    return result;
385  }
386
387  public String format_java_family(@GuardSatisfied OneOfString this, OutputFormat format) {
388
389    String result;
390
391    // Setting up the name of the unary variable
392    String varname = var().name_using(format);
393
394    result = "";
395    boolean is_type = is_type();
396    for (int i = 0; i < num_elts; i++) {
397      if (i != 0) { result += " || "; }
398      String str = elts[i];
399      if (!is_type) {
400        result += varname + ".equals(" + ((str == null) ? "null" : "\"" + StringsPlume.escapeNonASCII(str) + "\"") + ")";
401      } else {
402        // It's a type
403        if ((str == null) || "null".equals(str)) {
404          result += varname + " == null";
405        } else {
406          if (str.startsWith("[")) {
407            str = Signatures.fieldDescriptorToBinaryName(str);
408          }
409          // ".class" (which is a suffix for a type name) and not
410          // getClassSuffix (which is a suffix for an expression).
411          // we need ".class.getName()" to make result a string
412          result += varname + " == " + str + ".class.getName()";
413        }
414      }
415    }
416
417    return result;
418  }
419
420  public String format_simplify(@GuardSatisfied OneOfString this) {
421
422    sort_rep();
423
424    String varname =
425      var().simplifyFixup(var().name_using(OutputFormat.SIMPLIFY));
426
427    String result;
428
429    result = "";
430    boolean is_type = is_type();
431    for (int i = 0; i < num_elts; i++) {
432      String value = elts[i];
433      if (is_type) {
434        if (value == null) {
435          // do nothing
436        } else if (value.startsWith("[")) {
437          value = Signatures.fieldDescriptorToBinaryName(value);
438        } else if (value.startsWith("\"") && value.endsWith("\"")) {
439          value = value.substring(1, value.length()-1);
440        }
441        value = "|T_" + value + "|";
442      } else {
443        value = simplify_format_string(value);
444      }
445      result += " (EQ " + varname + " " + value + ")";
446    }
447    if (num_elts > 1) {
448      result = "(OR" + result + ")";
449    } else if (num_elts == 1) {
450      // chop leading space
451      result = result.substring(1);
452    } else if (num_elts == 0) {
453      return format_too_few_samples(OutputFormat.SIMPLIFY, null);
454    }
455
456    if (result.indexOf("format_simplify") == -1) {
457      daikon.simplify.SimpUtil.assert_well_formed(result);
458    }
459    return result;
460  }
461
462  @Override
463  public InvariantStatus add_modified(@Interned String a, int count) {
464    return runValue(a, count, true);
465  }
466
467  @Override
468  public InvariantStatus check_modified(@Interned String a, int count) {
469    return runValue(a, count, false);
470  }
471
472  private InvariantStatus runValue(@Interned String v, int count, boolean mutate) {
473    InvariantStatus status;
474    if (mutate) {
475      status = add_mod_elem(v, count);
476    } else {
477      status = check_mod_elem(v, count);
478    }
479    if (status == InvariantStatus.FALSIFIED) {
480      if (logOn() && mutate) {
481        StringBuilder eltString = new StringBuilder();
482        for (int i = 0; i < num_elts; i++) {
483          eltString.append(((elts[i] == null) ? "null" : "\"" + StringsPlume.escapeNonASCII(elts[i]) + "\"") + " ");
484        }
485        log("destroyed on sample %s previous vals = {%s} num_elts = %s",
486             ((v == null) ? "null" : "\"" + StringsPlume.escapeNonASCII(v) + "\""), eltString, num_elts);
487      }
488      return InvariantStatus.FALSIFIED;
489    }
490    return status;
491  }
492
493  /**
494   * Adds a single sample to the invariant. Returns
495   * the appropriate InvariantStatus from the result
496   * of adding the sample to this.
497   */
498  public InvariantStatus add_mod_elem(@Interned String v, int count) {
499    InvariantStatus status = check_mod_elem(v, count);
500    if (status == InvariantStatus.WEAKENED) {
501      elts[num_elts] = v;
502      num_elts++;
503    }
504    return status;
505  }
506
507  /**
508   * Checks a single sample to the invariant. Returns
509   * the appropriate InvariantStatus from the result
510   * of adding the sample to this.
511   */
512  public InvariantStatus check_mod_elem(@Interned String v, int count) {
513
514    // Look for v in our list of previously seen values.  If it's
515    // found, we're all set.
516    for (int i = 0; i < num_elts; i++) {
517      // if (logDetail())
518      //  log ("add_modified (" + v + ")");
519      if (((elts[i]) == ( v))) {
520        return InvariantStatus.NO_CHANGE;
521      }
522    }
523
524    if (num_elts == dkconfig_size) {
525      return InvariantStatus.FALSIFIED;
526    }
527
528    if (is_type() && (num_elts == 1)) {
529      return InvariantStatus.FALSIFIED;
530    }
531
532    return InvariantStatus.WEAKENED;
533  }
534
535  @Override
536  protected double computeConfidence() {
537    // This is not ideal.
538    if (num_elts == 0) {
539      return Invariant.CONFIDENCE_UNJUSTIFIED;
540    } else {
541      return Invariant.CONFIDENCE_JUSTIFIED;
542    }
543  }
544
545  @Pure
546  @Override
547  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
548    // Static constants are necessarily OneOf precisely one value.
549    // This removes static constants from the output, which might not be
550    // desirable if the user doesn't know their actual value.
551    if (vis[0].isStaticConstant()) {
552      assert num_elts <= 1;
553      return new DiscardInfo(this, DiscardCode.obvious, vis[0].name() + " is a static constant.");
554    }
555    return super.isObviousStatically(vis);
556  }
557
558  /** {@inheritDoc} */
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 Invariant 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}