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}