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