001package daikon.inv.unary.scalar; 002 003import daikon.PptSlice; 004import daikon.VarInfo; 005import daikon.inv.DiscardInfo; 006import daikon.inv.Invariant; 007import daikon.inv.InvariantStatus; 008import daikon.inv.OutputFormat; 009import daikon.inv.ValueSet; 010import java.io.Serializable; 011import java.util.ArrayList; 012import java.util.List; 013import org.checkerframework.checker.lock.qual.GuardSatisfied; 014import org.checkerframework.checker.nullness.qual.Nullable; 015import org.checkerframework.dataflow.qual.Pure; 016import org.checkerframework.dataflow.qual.SideEffectFree; 017import org.checkerframework.framework.qual.Unused; 018import typequals.prototype.qual.Prototype; 019 020/** 021 * Tracks every unique value and how many times it occurs. Prints as {@code x has values: v1 v2 v3 022 * ...}. 023 */ 024public final class CompleteOneOfScalar extends SingleScalar { 025 // We are Serializable, so we specify a version to allow changes to 026 // method signatures without breaking serialization. If you add or 027 // remove fields, you should change this number to the current date. 028 static final long serialVersionUID = 20091210L; 029 030 /** Information about each value encountered. */ 031 public static class Info implements Serializable { 032 static final long serialVersionUID = 20091210L; 033 public long val; 034 public int cnt; 035 036 public Info(long val, int cnt) { 037 this.val = val; 038 this.cnt = cnt; 039 } 040 } 041 042 /** List of values seen. */ 043 @Unused(when = Prototype.class) 044 @SuppressWarnings("serial") 045 public List<Info> vals; 046 047 /** Boolean. True iff CompleteOneOfScalar invariants should be considered. */ 048 public static boolean dkconfig_enabled = false; 049 050 public CompleteOneOfScalar(PptSlice slice) { 051 super(slice); 052 vals = new ArrayList<Info>(); 053 } 054 055 public @Prototype CompleteOneOfScalar() { 056 super(); 057 } 058 059 private static @Prototype CompleteOneOfScalar proto = new @Prototype CompleteOneOfScalar(); 060 061 /** Returns the prototype invariant for CompleteOneOFScalar. */ 062 public static @Prototype CompleteOneOfScalar get_proto() { 063 return proto; 064 } 065 066 /** returns whether or not this invariant is enabled */ 067 @Override 068 public boolean enabled() { 069 return dkconfig_enabled; 070 } 071 072 /** instantiate an invariant on the specified slice */ 073 @Override 074 public CompleteOneOfScalar instantiate_dyn(@Prototype CompleteOneOfScalar this, PptSlice slice) { 075 return new CompleteOneOfScalar(slice); 076 } 077 078 /** Return description of invariant. Only Daikon format is implemented. */ 079 @SideEffectFree 080 @Override 081 public String format_using(@GuardSatisfied CompleteOneOfScalar this, OutputFormat format) { 082 if (format == OutputFormat.DAIKON) { 083 String out = var().name() + " has values: "; 084 for (Info val : vals) { 085 out += String.format(" %s[%d]", val.val, val.cnt); 086 } 087 return out; 088 } else { 089 return format_unimplemented(format); 090 } 091 } 092 093 /** Check to see if a only contains printable ascii characters. */ 094 @Override 095 public InvariantStatus add_modified(long a, int count) { 096 return check_modified(a, count); 097 } 098 099 /** Check to see if a only contains printable ascii characters. */ 100 @Override 101 public InvariantStatus check_modified(long a, int count) { 102 for (Info val : vals) { 103 if (val.val == a) { 104 val.cnt += count; 105 return InvariantStatus.NO_CHANGE; 106 } 107 } 108 vals.add(new Info(a, count)); 109 // System.out.printf("check_modified %s%n", format()); 110 return InvariantStatus.NO_CHANGE; 111 } 112 113 @Override 114 protected double computeConfidence() { 115 ValueSet vs = ppt.var_infos[0].get_value_set(); 116 // System.out.printf("%s value set = %s%n", ppt.var_infos[0].name(), vs); 117 if (vs.size() > 0) { 118 return Invariant.CONFIDENCE_JUSTIFIED; 119 } else { 120 return Invariant.CONFIDENCE_UNJUSTIFIED; 121 } 122 } 123 124 /** 125 * Returns whether or not this is obvious statically. The only check is for static constants which 126 * are obviously printable (or not) from their values. 127 */ 128 @Pure 129 @Override 130 public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) { 131 return super.isObviousStatically(vis); 132 } 133 134 /** 135 * Same formula if each value is the same and has the same count. Not implemented for now, just 136 * presumed to be false. 137 */ 138 @Pure 139 @Override 140 public boolean isSameFormula(Invariant o) { 141 return false; 142 } 143}