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