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 String 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 PairwiseStringGreaterThan extends TwoSequenceString { 033 // We are Serializable, so we specify a version to allow changes to 034 // method signatures without breaking serialization. If you add or 035 // remove fields, you should change this number to the current date. 036 static final long serialVersionUID = 20030822L; 037 038 /** Debug tracer. */ 039 public static final Logger debug = 040 Logger.getLogger("daikon.inv.binary.twoSequence.PairwiseStringGreaterThan"); 041 042 // Variables starting with dkconfig_ should only be set via the 043 // daikon.config.Configuration interface. 044 /** Boolean. True iff PairwiseIntComparison invariants should be considered. */ 045 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 046 047 static final boolean debugPairwiseIntComparison = false; 048 049 protected PairwiseStringGreaterThan(PptSlice ppt) { 050 super(ppt); 051 } 052 053 protected @Prototype PairwiseStringGreaterThan() { 054 super(); 055 } 056 057 private static @Prototype PairwiseStringGreaterThan proto = new @Prototype PairwiseStringGreaterThan(); 058 059 /** Returns the prototype invariant for PairwiseStringGreaterThan */ 060 public static @Prototype PairwiseStringGreaterThan get_proto() { 061 return proto; 062 } 063 064 /** Returns whether or not this invariant is enabled. */ 065 @Override 066 public boolean enabled() { 067 return dkconfig_enabled; 068 } 069 070 /** PairwiseStringGreaterThan is only valid on integral types. */ 071 @Override 072 public boolean instantiate_ok(VarInfo[] vis) { 073 074 if (!valid_types(vis)) { 075 return false; 076 } 077 078 if (!(vis[0].type.elementIsString() && vis[1].type.elementIsString())) { 079 return false; 080 } 081 082 return true; 083 } 084 085 /** instantiates the invariant on the specified slice */ 086 @Override 087 protected PairwiseStringGreaterThan instantiate_dyn(@Prototype PairwiseStringGreaterThan this, PptSlice slice) { 088 PairwiseStringGreaterThan inv = new PairwiseStringGreaterThan(slice); 089 if (logOn()) { 090 inv.log("instantiate"); 091 } 092 return inv; 093 } 094 095 protected PairwiseStringGreaterThan(PairwiseStringLessThan swapped_pic) { 096 super(swapped_pic.ppt); 097 if (logOn()) { 098 log("Instantiated from resurrect_done_swapped"); 099 } 100 } 101 102 @Pure 103 @Override 104 public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) { 105 VarInfo var1 = vis[0]; 106 VarInfo var2 = vis[1]; 107 108 DiscardInfo di = SubSequence.isObviousSubSequence(this, var1, var2); 109 if (di == null) { 110 di = SubSequence.isObviousSubSequence(this, var2, var1); 111 } 112 if (di != null) { 113 Global.implied_noninstantiated_invariants++; 114 return di; 115 } 116 117 // Don't instantiate if the variables can't have order 118 if (!var1.aux.hasOrder() || !var2.aux.hasOrder()) { 119 if (debug.isLoggable(Level.FINE)) { 120 debug.fine("Not instantitating for because order has no meaning: " 121 + var1.name() + " and " + var2.name()); 122 } 123 return new DiscardInfo(this, DiscardCode.obvious, "Obvious statically since order has no meaning"); 124 } 125 126 return super.isObviousStatically(vis); 127 } 128 129 @Pure 130 @Override 131 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 132 DiscardInfo super_result = super.isObviousDynamically(vis); 133 if (super_result != null) { 134 return super_result; 135 } 136 137 // Subsequence invariants are implied by the same invariant over 138 // the supersequence 139 DiscardInfo di = superseq_implies(vis); 140 if (di != null) { 141 return di; 142 } 143 144 return null; 145 } 146 147 /** 148 * Checks to see if the same invariant exists over supersequences of these variables: 149 * 150 * <pre> 151 * (A[] op B[]) ^ (i == j) ⇒ A[i..] op B[j..] 152 * (A[] op B[]) ^ (i == j) ⇒ A[..i] op B[..j] 153 * </pre> 154 */ 155 private @Nullable DiscardInfo superseq_implies(VarInfo[] vis) { 156 157 // Make sure the variables are SequenceStringSubsequence with the same start/end 158 VarInfo v1 = vis[0]; 159 VarInfo v2 = vis[1]; 160 if (!v1.isDerived() || !(v1.derived instanceof SequenceStringSubsequence)) { 161 return null; 162 } 163 if (!v2.isDerived() || !(v2.derived instanceof SequenceStringSubsequence)) { 164 return null; 165 } 166 @NonNull SequenceStringSubsequence der1 = (SequenceStringSubsequence) v1.derived; 167 @NonNull SequenceStringSubsequence der2 = (SequenceStringSubsequence) v2.derived; 168 if ((der1.from_start != der2.from_start) 169 || (der1.index_shift != der2.index_shift)) 170 return null; 171 172 // Make sure the subscripts are equal 173 DiscardInfo di = new DiscardInfo(this, DiscardCode.obvious, ""); 174 if (!ppt.parent.check_implied_canonical(di, der1.sclvar(), der2.sclvar(), 175 IntEqual.get_proto())) 176 return null; 177 178 // See if the super-sequences have the same invariant 179 if (!ppt.parent.check_implied_canonical(di, der1.seqvar(), der2.seqvar(), 180 PairwiseStringGreaterThan.get_proto())) 181 return null; 182 183 // Add in the vis variables to di reason (if they are different) 184 di.add_implied_vis(vis); 185 return di; 186 } 187 188 @Override 189 protected Invariant resurrect_done_swapped() { 190 191 return new PairwiseStringLessThan(this); 192 } 193 194 /** Returns the class that corresponds to this class with its variable order swapped. */ 195 public static Class<PairwiseStringLessThan> swap_class() { 196 return PairwiseStringLessThan.class; 197 } 198 199 @Override 200 public String repr(@GuardSatisfied PairwiseStringGreaterThan this) { 201 return "PairwiseStringGreaterThan" + varNames() + ": "; 202 } 203 204 public String getComparator() { 205 return ">"; 206 } 207 208 @SideEffectFree 209 @Override 210 public String format_using(@GuardSatisfied PairwiseStringGreaterThan this, OutputFormat format) { 211 212 if (format.isJavaFamily()) { 213 return format_java_family(format); 214 } 215 216 if (format == OutputFormat.DAIKON) { 217 return format_daikon(); 218 } 219 if (format == OutputFormat.ESCJAVA) { 220 return format_esc(); 221 } 222 if (format == OutputFormat.SIMPLIFY) { 223 return format_simplify(); 224 } 225 if (format == OutputFormat.CSHARPCONTRACT) { 226 return format_csharp(); 227 } 228 229 return format_unimplemented(format); 230 } 231 232 public String format_daikon(@GuardSatisfied PairwiseStringGreaterThan this) { 233 return var1().name() + " > " + var2().name() + " (elementwise)"; 234 } 235 236 public String format_esc(@GuardSatisfied PairwiseStringGreaterThan this) { 237 String[] form = VarInfo.esc_quantify(var1(), var2()); 238 return form[0] + "(" + form[1] + " > " + form[2] + ")" + form[3]; 239 } 240 241 public String format_simplify(@GuardSatisfied PairwiseStringGreaterThan this) { 242 String[] form = VarInfo.simplify_quantify(QuantFlags.element_wise(), var1(), var2()); 243 return form[0] + "(> " + form[1] + " " + form[2] + ")" + form[3]; 244 } 245 246 public String format_java_family(@GuardSatisfied PairwiseStringGreaterThan this, OutputFormat format) { 247 return "daikon.Quant.pairwiseGT(" + var1().name_using(format) 248 + ", " + var2().name_using(format) + ")"; 249 } 250 251 public String format_csharp(@GuardSatisfied PairwiseStringGreaterThan this) { 252 253 String[] split1 = var1().csharp_array_split(); 254 String[] split2 = var2().csharp_array_split(); 255 256 String equals_str; 257 String end_str; 258 259 equals_str = " > "; 260 end_str = ""; 261 262 return "Contract.ForAll(0, " + split1[0] + ".Count(), i => " + split1[0] + "[i]" + split1[1] + equals_str + split2[0] + "[i]" + split2[1] + end_str + ")"; 263 } 264 265 @Override 266 public InvariantStatus check_modified(String @Interned [] a1, String @Interned [] a2, int count) { 267 assert a1 != null && a2 != null 268 : var1() + " " + var2() + " " + FileIO.get_linenum(); 269 if (a1.length != a2.length || a1.length == 0 || a2.length == 0) { 270 // destroyAndFlow(); 271 return InvariantStatus.FALSIFIED; 272 } 273 274 int len = a1.length; 275 // int len = Math.min(a1.length, a2.length); 276 277 for (int i = 0; i < len; i++) { 278 String v1 = a1[i]; 279 String v2 = a2[i]; 280 if (!(v1 != null && v2 != null && v1.compareTo( v2) > 0) ) { 281 // destroyAndFlow(); 282 return InvariantStatus.FALSIFIED; 283 } 284 } 285 return InvariantStatus.NO_CHANGE; 286 } 287 288 @Override 289 public InvariantStatus add_modified(String @Interned [] a1, String @Interned [] a2, 290 int count) { 291 if (logDetail()) { 292 log(debug, "saw add_modified (" + Arrays.toString(a1) 293 + ", " + Arrays.toString(a2) + ")"); 294 } 295 return check_modified(a1, a2, count); 296 } 297 298 @Override 299 protected double computeConfidence() { 300 // num_elt_values() would be more appropriate 301 // int num_values = ((PptSlice2) ppt).num_elt_values(); 302 int num_values = ppt.num_samples(); 303 if (num_values == 0) { 304 return Invariant.CONFIDENCE_UNJUSTIFIED; 305 } else { 306 307 return 1 - Math.pow(.5, num_values); 308 } 309 } 310 311 @Pure 312 @Override 313 public boolean isSameFormula(Invariant other) { 314 return true; 315 } 316 317 @Pure 318 @Override 319 public boolean isExclusiveFormula(Invariant other) { 320 return false; 321 } 322 323 // Look up a previously instantiated invariant. 324 public static @Nullable PairwiseStringGreaterThan find(PptSlice ppt) { 325 assert ppt.arity() == 2; 326 for (Invariant inv : ppt.invs) { 327 if (inv instanceof PairwiseStringGreaterThan) { 328 return (PairwiseStringGreaterThan) inv; 329 } 330 } 331 return null; 332 } 333 334 /** Returns a list of non-instantiating suppressions for this invariant. */ 335 @Pure 336 @Override 337 public @Nullable NISuppressionSet get_ni_suppressions() { 338 return suppressions; 339 } 340 341 private static @Nullable NISuppressionSet suppressions = null; 342 343}