001// ***** This file is automatically generated from PairwiseIntComparison.java.jpp 002 003package daikon.inv.binary.twoSequence; 004 005import daikon.*; 006import daikon.Quantify.QuantFlags; 007import daikon.derive.binary.*; 008import daikon.inv.*; 009import daikon.inv.binary.twoScalar.*; 010import daikon.suppress.*; 011import java.util.Arrays; 012import java.util.Iterator; 013import java.util.logging.Level; 014import java.util.logging.Logger; 015import org.checkerframework.checker.interning.qual.Interned; 016import org.checkerframework.checker.lock.qual.GuardSatisfied; 017import org.checkerframework.checker.nullness.qual.NonNull; 018import org.checkerframework.checker.nullness.qual.Nullable; 019import org.checkerframework.dataflow.qual.Pure; 020import org.checkerframework.dataflow.qual.SideEffectFree; 021import org.plumelib.util.ArraysPlume; 022import org.plumelib.util.Intern; 023import typequals.prototype.qual.NonPrototype; 024import typequals.prototype.qual.Prototype; 025 026/** 027 * Represents an invariant between corresponding elements of two sequences of double values. The 028 * length of the sequences must match for the invariant to hold. A comparison is made over each 029 * {@code (x[i], y[i])} pair. Thus, {@code x[0]} is compared to {@code y[0]}, 030 * {@code x[1]} to {@code y[1]}, and so forth. Prints as {@code x[] <= y[]}. 031 */ 032public class PairwiseFloatLessEqual extends TwoSequenceFloat { 033 static final long serialVersionUID = 20030822L; 034 035 /** Debug tracer. */ 036 public static final Logger debug = 037 Logger.getLogger("daikon.inv.binary.twoSequence.PairwiseFloatLessEqual"); 038 039 // Variables starting with dkconfig_ should only be set via the 040 // daikon.config.Configuration interface. 041 /** Boolean. True iff PairwiseIntComparison invariants should be considered. */ 042 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 043 044 static final boolean debugPairwiseIntComparison = false; 045 046 protected PairwiseFloatLessEqual(PptSlice ppt) { 047 super(ppt); 048 } 049 050 protected @Prototype PairwiseFloatLessEqual() { 051 super(); 052 } 053 054 private static @Prototype PairwiseFloatLessEqual proto = new @Prototype PairwiseFloatLessEqual(); 055 056 /** Returns the prototype invariant for PairwiseFloatLessEqual. */ 057 public static @Prototype PairwiseFloatLessEqual get_proto() { 058 return proto; 059 } 060 061 @Override 062 public boolean enabled() { 063 return dkconfig_enabled; 064 } 065 066 @Override 067 public boolean instantiate_ok(VarInfo[] vis) { 068 069 if (!valid_types(vis)) { 070 return false; 071 } 072 073 if (!(vis[0].type.elementIsFloat() && vis[1].type.elementIsFloat())) { 074 return false; 075 } 076 077 return true; 078 } 079 080 @Override 081 protected PairwiseFloatLessEqual instantiate_dyn(@Prototype PairwiseFloatLessEqual this, PptSlice slice) { 082 PairwiseFloatLessEqual inv = new PairwiseFloatLessEqual(slice); 083 if (logOn()) { 084 inv.log("instantiate"); 085 } 086 return inv; 087 } 088 089 protected PairwiseFloatLessEqual(PairwiseFloatGreaterEqual swapped_pic) { 090 super(swapped_pic.ppt); 091 if (logOn()) { 092 log("Instantiated from resurrect_done_swapped"); 093 } 094 } 095 096 @Pure 097 @Override 098 public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) { 099 VarInfo var1 = vis[0]; 100 VarInfo var2 = vis[1]; 101 102 DiscardInfo di = SubSequence.isObviousSubSequence(this, var1, var2); 103 if (di == null) { 104 di = SubSequence.isObviousSubSequence(this, var2, var1); 105 } 106 if (di != null) { 107 Global.implied_noninstantiated_invariants++; 108 return di; 109 } 110 111 // Don't instantiate if the variables can't have order 112 if (!var1.aux.hasOrder() || !var2.aux.hasOrder()) { 113 if (debug.isLoggable(Level.FINE)) { 114 debug.fine("Not instantitating for because order has no meaning: " 115 + var1.name() + " and " + var2.name()); 116 } 117 return new DiscardInfo(this, DiscardCode.obvious, "Obvious statically since order has no meaning"); 118 } 119 120 return super.isObviousStatically(vis); 121 } 122 123 @Pure 124 @Override 125 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 126 DiscardInfo super_result = super.isObviousDynamically(vis); 127 if (super_result != null) { 128 return super_result; 129 } 130 131 // Subsequence invariants are implied by the same invariant over 132 // the supersequence 133 DiscardInfo di = superseq_implies(vis); 134 if (di != null) { 135 return di; 136 } 137 138 return null; 139 } 140 141 /** 142 * Checks to see if the same invariant exists over supersequences of these variables: 143 * 144 * <pre> 145 * (A[] op B[]) ^ (i == j) ⇒ A[i..] op B[j..] 146 * (A[] op B[]) ^ (i == j) ⇒ A[..i] op B[..j] 147 * </pre> 148 */ 149 private @Nullable DiscardInfo superseq_implies(VarInfo[] vis) { 150 151 // Make sure the variables are SequenceFloatSubsequence with the same start/end 152 VarInfo v1 = vis[0]; 153 VarInfo v2 = vis[1]; 154 if (!v1.isDerived() || !(v1.derived instanceof SequenceFloatSubsequence)) { 155 return null; 156 } 157 if (!v2.isDerived() || !(v2.derived instanceof SequenceFloatSubsequence)) { 158 return null; 159 } 160 @NonNull SequenceFloatSubsequence der1 = (SequenceFloatSubsequence) v1.derived; 161 @NonNull SequenceFloatSubsequence der2 = (SequenceFloatSubsequence) v2.derived; 162 if ((der1.from_start != der2.from_start) 163 || (der1.index_shift != der2.index_shift)) 164 return null; 165 166 // Make sure the subscripts are equal 167 DiscardInfo di = new DiscardInfo(this, DiscardCode.obvious, ""); 168 if (!ppt.parent.check_implied_canonical(di, der1.sclvar(), der2.sclvar(), 169 IntEqual.get_proto())) 170 return null; 171 172 // See if the super-sequences have the same invariant 173 if (!ppt.parent.check_implied_canonical(di, der1.seqvar(), der2.seqvar(), 174 PairwiseFloatLessEqual.get_proto())) 175 return null; 176 177 // Add in the vis variables to di reason (if they are different) 178 di.add_implied_vis(vis); 179 return di; 180 } 181 182 @Override 183 protected Invariant resurrect_done_swapped() { 184 185 return new PairwiseFloatGreaterEqual(this); 186 } 187 188 /** Returns the class that corresponds to this class with its variable order swapped. */ 189 public static Class<PairwiseFloatGreaterEqual> swap_class() { 190 return PairwiseFloatGreaterEqual.class; 191 } 192 193 @Override 194 public String repr(@GuardSatisfied PairwiseFloatLessEqual this) { 195 return "PairwiseFloatLessEqual" + varNames() + ": "; 196 } 197 198 public String getComparator() { 199 return "<="; 200 } 201 202 @SideEffectFree 203 @Override 204 public String format_using(@GuardSatisfied PairwiseFloatLessEqual this, OutputFormat format) { 205 206 if (format.isJavaFamily()) { 207 return format_java_family(format); 208 } 209 210 if (format == OutputFormat.DAIKON) { 211 return format_daikon(); 212 } 213 if (format == OutputFormat.ESCJAVA) { 214 return format_esc(); 215 } 216 if (format == OutputFormat.SIMPLIFY) { 217 return format_simplify(); 218 } 219 if (format == OutputFormat.CSHARPCONTRACT) { 220 return format_csharp(); 221 } 222 223 return format_unimplemented(format); 224 } 225 226 public String format_daikon(@GuardSatisfied PairwiseFloatLessEqual this) { 227 return var1().name() + " <= " + var2().name() + " (elementwise)"; 228 } 229 230 public String format_esc(@GuardSatisfied PairwiseFloatLessEqual this) { 231 String[] form = VarInfo.esc_quantify(var1(), var2()); 232 return form[0] + "(" + form[1] + " <= " + form[2] + ")" + form[3]; 233 } 234 235 public String format_simplify(@GuardSatisfied PairwiseFloatLessEqual this) { 236 String[] form = VarInfo.simplify_quantify(QuantFlags.element_wise(), var1(), var2()); 237 return form[0] + "(<= " + form[1] + " " + form[2] + ")" + form[3]; 238 } 239 240 public String format_java_family(@GuardSatisfied PairwiseFloatLessEqual this, OutputFormat format) { 241 return "daikon.Quant.pairwiseLTE(" + var1().name_using(format) 242 + ", " + var2().name_using(format) + ")"; 243 } 244 245 public String format_csharp(@GuardSatisfied PairwiseFloatLessEqual this) { 246 247 String[] split1 = var1().csharp_array_split(); 248 String[] split2 = var2().csharp_array_split(); 249 250 String equals_str; 251 String end_str; 252 253 equals_str = " <= "; 254 end_str = ""; 255 256 return "Contract.ForAll(0, " + split1[0] + ".Count(), i => " + split1[0] + "[i]" + split1[1] + equals_str + split2[0] + "[i]" + split2[1] + end_str + ")"; 257 } 258 259 @Override 260 public InvariantStatus check_modified(double @Interned [] a1, double @Interned [] a2, int count) { 261 assert a1 != null && a2 != null 262 : var1() + " " + var2() + " " + FileIO.get_linenum(); 263 if (a1.length != a2.length || a1.length == 0 || a2.length == 0) { 264 // destroyAndFlow(); 265 return InvariantStatus.FALSIFIED; 266 } 267 268 int len = a1.length; 269 // int len = Math.min(a1.length, a2.length); 270 271 for (int i = 0; i < len; i++) { 272 double v1 = a1[i]; 273 double v2 = a2[i]; 274 if (!Global.fuzzy.lte(v1, v2) ) { 275 // destroyAndFlow(); 276 return InvariantStatus.FALSIFIED; 277 } 278 } 279 return InvariantStatus.NO_CHANGE; 280 } 281 282 @Override 283 public InvariantStatus add_modified(double @Interned [] a1, double @Interned [] a2, 284 int count) { 285 if (logDetail()) { 286 log(debug, "saw add_modified (" + Arrays.toString(a1) 287 + ", " + Arrays.toString(a2) + ")"); 288 } 289 return check_modified(a1, a2, count); 290 } 291 292 @Override 293 protected double computeConfidence() { 294 // num_elt_values() would be more appropriate 295 // int num_values = ((PptSlice2) ppt).num_elt_values(); 296 int num_values = ppt.num_samples(); 297 if (num_values == 0) { 298 return Invariant.CONFIDENCE_UNJUSTIFIED; 299 } else { 300 301 return 1 - Math.pow(.5, num_values); 302 } 303 } 304 305 @Pure 306 @Override 307 public boolean isSameFormula(Invariant other) { 308 return true; 309 } 310 311 @Pure 312 @Override 313 public boolean isExclusiveFormula(Invariant other) { 314 return false; 315 } 316 317 // Look up a previously instantiated invariant. 318 public static @Nullable PairwiseFloatLessEqual find(PptSlice ppt) { 319 assert ppt.arity() == 2; 320 for (Invariant inv : ppt.invs) { 321 if (inv instanceof PairwiseFloatLessEqual) { 322 return (PairwiseFloatLessEqual) inv; 323 } 324 } 325 return null; 326 } 327 328 /** Returns a list of non-instantiating suppressions for this invariant. */ 329 @Pure 330 @Override 331 public @Nullable NISuppressionSet get_ni_suppressions() { 332 return suppressions; 333 } 334 335 /** Definition of this invariant (the suppressee) */ 336 private static NISuppressee suppressee = new NISuppressee(PairwiseFloatLessEqual.class, 2); 337 338 // Suppressor definitions (used in suppressions below) 339 private static NISuppressor v1_eq_v2 = new NISuppressor(0, 1, PairwiseFloatEqual.class); 340 private static NISuppressor v1_lt_v2 = new NISuppressor(0, 1, PairwiseFloatLessThan.class); 341 342 private static NISuppressionSet suppressions = 343 new NISuppressionSet( 344 new NISuppression[] { 345 346 // v1 == v2 => v1 <= v2 347 new NISuppression(v1_eq_v2, suppressee), 348 349 // v1 < v2 => v1 <= v2 350 new NISuppression(v1_lt_v2, suppressee), 351 352 }); 353 354}