001package daikon.inv.unary.string;
002
003import daikon.PptSlice;
004import daikon.VarInfo;
005import daikon.inv.DiscardCode;
006import daikon.inv.DiscardInfo;
007import daikon.inv.Invariant;
008import daikon.inv.InvariantStatus;
009import daikon.inv.OutputFormat;
010import daikon.inv.ValueSet;
011import org.checkerframework.checker.interning.qual.Interned;
012import org.checkerframework.checker.lock.qual.GuardSatisfied;
013import org.checkerframework.checker.nullness.qual.Nullable;
014import org.checkerframework.dataflow.qual.Pure;
015import org.checkerframework.dataflow.qual.SideEffectFree;
016import typequals.prototype.qual.Prototype;
017
018/**
019 * Represents a string that contains only printable ascii characters (values 32 through 126 plus 9
020 * (tab).
021 */
022public final class PrintableString extends SingleString {
023  static final long serialVersionUID = 20061016L;
024
025  /** Boolean. True iff PrintableString invariants should be considered. */
026  public static boolean dkconfig_enabled = false;
027
028  public PrintableString(PptSlice slice) {
029    super(slice);
030  }
031
032  public @Prototype PrintableString() {
033    super();
034  }
035
036  private static @Prototype PrintableString proto = new @Prototype PrintableString();
037
038  /** Returns the prototype invariant for PrintableString. */
039  public static @Prototype PrintableString get_proto() {
040    return proto;
041  }
042
043  @Override
044  public boolean enabled() {
045    return dkconfig_enabled;
046  }
047
048  @Override
049  public PrintableString instantiate_dyn(@Prototype PrintableString this, PptSlice slice) {
050    return new PrintableString(slice);
051  }
052
053  /** Return description of invariant. Only Daikon format is implemented. */
054  @SideEffectFree
055  @Override
056  public String format_using(@GuardSatisfied PrintableString this, OutputFormat format) {
057    if (format == OutputFormat.DAIKON) {
058      return var().name() + " is printable";
059    } else {
060      return format_unimplemented(format);
061    }
062  }
063
064  /** Check to see if a only contains printable ASCII characters. */
065  @Override
066  public InvariantStatus add_modified(@Interned String a, int count) {
067    return check_modified(a, count);
068  }
069
070  /** Check to see if a only contains printable ASCII characters. */
071  @Override
072  public InvariantStatus check_modified(@Interned String a, int count) {
073    for (int ii = 0; ii < a.length(); ii++) {
074      char ch = a.charAt(ii);
075      if (ch > 126) {
076        return InvariantStatus.FALSIFIED;
077      }
078      if ((ch < 32) && (ch != 9)) {
079        return InvariantStatus.FALSIFIED;
080      }
081    }
082    return InvariantStatus.NO_CHANGE;
083  }
084
085  @Override
086  protected double computeConfidence() {
087    ValueSet vs = ppt.var_infos[0].get_value_set();
088    if (vs.size() > 1) {
089      return Invariant.CONFIDENCE_JUSTIFIED;
090    } else {
091      return Invariant.CONFIDENCE_UNJUSTIFIED;
092    }
093  }
094
095  /**
096   * Returns whether or not this is obvious statically. The only check is for static constants which
097   * are obviously printable (or not) from their values.
098   */
099  @Pure
100  @Override
101  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
102    if (vis[0].isStaticConstant()) {
103      return new DiscardInfo(this, DiscardCode.obvious, vis[0].name() + " is a static constant.");
104    }
105    return super.isObviousStatically(vis);
106  }
107
108  @Pure
109  @Override
110  public boolean isSameFormula(Invariant o) {
111    assert o instanceof PrintableString;
112    return true;
113  }
114}