001// ***** This file is automatically generated from SeqIntComparison.java.jpp 002 003package daikon.inv.binary.sequenceScalar; 004 005import daikon.*; 006import daikon.derive.unary.*; 007import daikon.inv.*; 008import daikon.inv.binary.twoSequence.*; 009import daikon.inv.unary.sequence.*; 010import daikon.suppress.*; 011import java.util.*; 012import java.util.logging.Logger; 013import org.checkerframework.checker.interning.qual.Interned; 014import org.checkerframework.checker.lock.qual.GuardSatisfied; 015import org.checkerframework.checker.nullness.qual.Nullable; 016import org.checkerframework.dataflow.qual.Pure; 017import org.checkerframework.dataflow.qual.SideEffectFree; 018import org.plumelib.util.Intern; 019import typequals.prototype.qual.NonPrototype; 020import typequals.prototype.qual.Prototype; 021 022/** 023 * Represents an invariant between a long scalar and a a sequence of long values. Prints 024 * as {@code x[] elements == y} where {@code x} is a long sequence and 025 * {@code y} is a long scalar. 026 */ 027public final class SeqIntEqual extends SequenceScalar { 028 static final long serialVersionUID = 20030822L; 029 030 // Variables starting with dkconfig_ should only be set via the 031 // daikon.config.Configuration interface. 032 /** Boolean. True iff SeqIntEqual invariants should be considered. */ 033 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 034 035 public static final Logger debug = 036 Logger.getLogger("daikon.inv.binary.sequenceScalar.SeqIntEqual"); 037 038 static boolean debugSeqIntComparison = false; 039 040 SeqIntEqual(PptSlice ppt) { 041 super(ppt); 042 } 043 044 @Prototype SeqIntEqual() { 045 super(); 046 } 047 048 private static @Prototype SeqIntEqual proto = new @Prototype SeqIntEqual(); 049 050 /** Returns the prototype invariant for SeqIntEqual. */ 051 public static @Prototype SeqIntEqual get_proto() { 052 return proto; 053 } 054 055 @Override 056 public boolean enabled() { 057 return dkconfig_enabled; 058 } 059 060 @Override 061 public boolean instantiate_ok(VarInfo[] vis) { 062 063 if (!valid_types(vis)) { 064 return false; 065 } 066 067 VarInfo seqvar; 068 VarInfo sclvar; 069 if (vis[0].rep_type == ProglangType.INT_ARRAY) { 070 seqvar = vis[0]; 071 sclvar = vis[1]; 072 } else { 073 seqvar = vis[1]; 074 sclvar = vis[0]; 075 } 076 077 assert sclvar.rep_type == ProglangType.INT; 078 assert seqvar.rep_type == ProglangType.INT_ARRAY; 079 080 return true; 081 } 082 083 @Override 084 protected SeqIntEqual instantiate_dyn(@Prototype SeqIntEqual this, PptSlice slice) { 085 return new SeqIntEqual(slice); 086 } 087 088 /** 089 * Checks to see if the comparison is obvious statically. Makes the following checks: 090 * 091 * <pre> 092 * max(A[]) op A[] 093 * min(A[]) op A[] 094 * </pre> 095 * 096 * JHP: Note that these are not strict implications, these are merely uninteresting comparisons 097 * (except when op is GreaterEqual for max and LessEqual for min). 098 */ 099 @Pure 100 @Override 101 public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) { 102 103 SequenceMin seqmin = null; 104 SequenceMax seqmax = null; 105 VarInfo sclseq = null; 106 VarInfo sclvar = sclvar(vis); 107 if (sclvar.derived instanceof SequenceMin) { 108 seqmin = (SequenceMin) sclvar.derived; 109 sclseq = seqmin.base; 110 } else if (sclvar.derived instanceof SequenceMax) { 111 seqmax = (SequenceMax) sclvar.derived; 112 sclseq = seqmax.base; 113 } 114 if (seqvar(vis) == sclseq) { 115 return new DiscardInfo(this, DiscardCode.obvious, sclvar(vis).name() + " is min/max "); 116 } 117 return null; 118 } 119 120 @SideEffectFree 121 @Override 122 public SeqIntEqual clone(@GuardSatisfied SeqIntEqual this) { 123 SeqIntEqual result = (SeqIntEqual) super.clone(); 124 return result; 125 } 126 127 @Override 128 public String repr(@GuardSatisfied SeqIntEqual this) { 129 return "SeqIntEqual" + varNames() + ": ,falsified=" + falsified; 130 } 131 132 @SideEffectFree 133 @Override 134 public String format_using(@GuardSatisfied SeqIntEqual this, OutputFormat format) { 135 136 if (format.isJavaFamily()) { 137 return format_java_family(format); 138 } 139 140 if (format == OutputFormat.DAIKON) { 141 return format_daikon(); 142 } 143 if (format == OutputFormat.ESCJAVA) { 144 return format_esc(); 145 } 146 if (format == OutputFormat.SIMPLIFY) { 147 return format_simplify(); 148 } 149 if (format == OutputFormat.CSHARPCONTRACT) { 150 return format_csharp_contract(); 151 } 152 153 return format_unimplemented(format); 154 } 155 156 public String format_daikon(@GuardSatisfied SeqIntEqual this) { 157 return seqvar().name() + " elements == " + sclvar().name(); 158 } 159 160 public String format_esc(@GuardSatisfied SeqIntEqual this) { 161 String[] form = VarInfo.esc_quantify(seqvar(), sclvar()); 162 return form[0] + "(" + form[1] + " == " + form[2] + ")" + form[3]; 163 } 164 165 public String format_simplify(@GuardSatisfied SeqIntEqual this) { 166 String[] form = VarInfo.simplify_quantify(seqvar(), sclvar()); 167 return form[0] + "(EQ " + form[1] + " " + form[2] + ")" + form[3]; 168 } 169 170 public String format_java_family(@GuardSatisfied SeqIntEqual this, OutputFormat format) { 171 return "daikon.Quant.eltsEqual(" 172 + seqvar().name_using(format) 173 + ", " 174 + sclvar().name_using(format) 175 + ")"; 176 } 177 178 public String format_csharp_contract(@GuardSatisfied SeqIntEqual this) { 179 String[] split = seqvar().csharp_array_split(); 180 return "Contract.ForAll(" 181 + split[0] 182 + ", x => x" 183 + split[1] 184 + " == " 185 + sclvar().csharp_name() 186 + ")"; 187 } 188 189 @Override 190 public InvariantStatus check_modified(long @Interned [] a, long x, int count) { 191 /*if (logDetail() || debug.isLoggable(Level.FINE)) 192 log(debug,"(== " + Arrays.toString(a) 193 + " " + x);*/ 194 for (int i = 0; i < a.length; i++) { 195 196 if (!(a[i] == x)) { 197 return InvariantStatus.FALSIFIED; 198 } 199 } 200 return InvariantStatus.NO_CHANGE; 201 } 202 203 @Override 204 public InvariantStatus add_modified(long @Interned [] a, long x, int count) { 205 return check_modified(a, x, count); 206 } 207 208 @Override 209 protected double computeConfidence() { 210 211 // If there are no samples over our variables, its unjustified 212 if (ppt.num_samples() == 0) { 213 return CONFIDENCE_UNJUSTIFIED; 214 } 215 216 // If the array never has any elements, its unjustified 217 ValueSet.ValueSetScalarArray vs = (ValueSet.ValueSetScalarArray) seqvar().get_value_set(); 218 if (vs.elem_cnt() == 0) { 219 return CONFIDENCE_UNJUSTIFIED; 220 } 221 222 // It's an equality invariant. I ought to use the actual ranges somehow. 223 // Actually, I can't even use this .5 test because it can make 224 // equality non-transitive. 225 // return Math.pow(.5, ppt.num_samples()); 226 return Invariant.CONFIDENCE_JUSTIFIED; 227 } 228 229 @Pure 230 @Override 231 public boolean isExact() { 232 233 return true; 234 } 235 236 @Pure 237 @Override 238 public boolean isSameFormula(Invariant other) { 239 return true; 240 } 241 242 @Pure 243 @Override 244 public boolean isExclusiveFormula(Invariant other) { 245 return false; 246 } 247 248 // Look up a previously instantiated invariant. 249 public static @Nullable SeqIntEqual find(PptSlice ppt) { 250 assert ppt.arity() == 2; 251 for (Invariant inv : ppt.invs) { 252 if (inv instanceof SeqIntEqual) { 253 return (SeqIntEqual) inv; 254 } 255 } 256 return null; 257 } 258 259 /** 260 * Checks to see if this is obvious over the specified variables. Implements the following checks: 261 * 262 * <pre> 263 * (x op B[]) ^ (B[] subsequence A[]) ⇒ (x op A[]) 264 * (A[] == []) ⇒ (x op A[]) 265 * </pre> 266 */ 267 @Pure 268 @Override 269 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 270 271 DiscardInfo super_result = super.isObviousDynamically(vis); 272 if (super_result != null) { 273 return super_result; 274 } 275 276 VarInfo seqvar = seqvar(vis); 277 @SuppressWarnings("UnusedVariable") // generated code, sometimes is necessary 278 VarInfo sclvar = sclvar(vis); 279 // Debug.log(getClass(), ppt, vis, "Considering over" + seqvar.name() 280 // + " and " + sclvar.name()); 281 282 // Look for the same property over a supersequence of this one. This 283 // doesn't need to explicitly ignore oher members of the equality set 284 // because those members won't have any invariants over them. 285 PptTopLevel pptt = ppt.parent; 286 for (Iterator<Invariant> inv_itor = pptt.invariants_iterator(); inv_itor.hasNext(); ) { 287 Invariant inv = inv_itor.next(); 288 if (inv == this) { 289 continue; 290 } 291 if (inv instanceof SeqIntEqual) { 292 SeqIntEqual other = (SeqIntEqual) inv; 293 // System.out.printf("considering %s seqvar=%s, other=%s%n", other.format(), 294 // seqvar().name(), other.seqvar().name()); 295 if (pptt.is_subsequence(seqvar(), other.seqvar()) && (sclvar(vis) == other.sclvar())) { 296 // System.out.println ("is subsequence"); 297 return new DiscardInfo( 298 this, 299 DiscardCode.obvious, 300 seqvar().name() 301 + " is a subsequence of " 302 + other.seqvar().name() 303 + " and " 304 + other.format() 305 + " holds"); 306 } 307 } 308 } 309 310 // JHP: handled in confidence test now 311 // (A[] == []) ==> A[] op x 312 if (false) { 313 if (pptt.is_empty(seqvar)) { 314 return new DiscardInfo( 315 this, DiscardCode.obvious, "The sequence " + seqvar.name() + " is always empty"); 316 } 317 } 318 319 if (isExact()) { 320 return null; 321 } 322 323 // JHP: this presumes that this invariant is true and should thus be 324 // moved to uninteresting or removed. 325 { 326 PptSlice1 seqslice = pptt.findSlice(seqvar); 327 if (seqslice != null) { 328 EltOneOf eoo = EltOneOf.find(seqslice); 329 if ((eoo != null) && eoo.enoughSamples() && (eoo.num_elts() == 1)) { 330 return new DiscardInfo(this, DiscardCode.obvious, "Obvious implied by " + eoo.format()); 331 } 332 } 333 } 334 335 return null; 336 } 337 338 /** Returns a list of non-instantiating suppressions for this invariant. */ 339 @Pure 340 @Override 341 public @Nullable NISuppressionSet get_ni_suppressions() { 342 return suppressions; 343 } 344 345 /** NI Suppressions for each type of comparison. */ 346 private static @Nullable NISuppressionSet suppressions = null; 347 348}