001// ***** This file is automatically generated from EltwiseIntComparisons.java.jpp 002 003package daikon.inv.unary.sequence; 004 005import daikon.*; 006import daikon.Quantify.QuantFlags; 007import daikon.derive.*; 008import daikon.derive.binary.*; 009import daikon.inv.*; 010import java.util.*; 011import org.checkerframework.checker.interning.qual.Interned; 012import org.checkerframework.checker.lock.qual.GuardSatisfied; 013import org.checkerframework.checker.nullness.qual.Nullable; 014import org.checkerframework.dataflow.qual.Pure; 015import org.checkerframework.dataflow.qual.SideEffectFree; 016import org.plumelib.util.Intern; 017import typequals.prototype.qual.NonPrototype; 018import typequals.prototype.qual.Prototype; 019 020 /** 021 * Represents the invariant < between adjacent elements 022 * (x[i], x[i+1]) of a long sequence. Prints as 023 * {@code x[] sorted by <}. 024 */ 025 026public class EltwiseIntLessThan extends EltwiseIntComparison { 027 static final long serialVersionUID = 20030822L; 028 029 // Variables starting with dkconfig_ should only be set via the 030 // daikon.config.Configuration interface. 031 /** Boolean. True iff EltwiseIntComparison invariants should be considered. */ 032 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 033 034 static final boolean debugEltwiseIntComparison = false; 035 036 protected EltwiseIntLessThan(PptSlice ppt) { 037 super(ppt); 038 } 039 040 protected @Prototype EltwiseIntLessThan() { 041 super(); 042 } 043 044 private static @Prototype EltwiseIntLessThan proto = new @Prototype EltwiseIntLessThan(); 045 046 /** Returns the prototype invariant for EltwiseIntLessThan */ 047 public static @Prototype EltwiseIntLessThan get_proto() { 048 return proto; 049 } 050 051 @Override 052 public boolean enabled() { 053 return dkconfig_enabled; 054 } 055 056 /** Non-equality EltwiseIntLessThan invariants are only valid on integral types. */ 057 @Override 058 public boolean instantiate_ok(VarInfo[] vis) { 059 060 if (!valid_types(vis)) { 061 return false; 062 } 063 064 if (!vis[0].type.baseIsIntegral()) { 065 return false; 066 } 067 068 return true; 069 } 070 071 @Override 072 protected EltwiseIntLessThan instantiate_dyn(@Prototype EltwiseIntLessThan this, PptSlice slice) { 073 return new EltwiseIntLessThan(slice); 074 } 075 076 @SideEffectFree 077 @Override 078 public EltwiseIntLessThan clone(@GuardSatisfied EltwiseIntLessThan this) { 079 EltwiseIntLessThan result = (EltwiseIntLessThan) super.clone(); 080 return result; 081 } 082 083 @Override 084 public String repr(@GuardSatisfied EltwiseIntLessThan this) { 085 return "EltwiseIntLessThan" + varNames() + ": falsified=" + falsified; 086 } 087 088 @SideEffectFree 089 @Override 090 public String format_using(@GuardSatisfied EltwiseIntLessThan this, OutputFormat format) { 091 if (format.isJavaFamily()) { 092 return format_java_family(format); 093 } 094 095 if (format == OutputFormat.DAIKON) { 096 return format_daikon(); 097 } 098 if (format == OutputFormat.ESCJAVA) { 099 return format_esc(); 100 } 101 if (format == OutputFormat.CSHARPCONTRACT) { 102 return format_csharp_contract(); 103 } 104 if (format == OutputFormat.SIMPLIFY) { 105 return format_simplify(); 106 } 107 108 return format_unimplemented(format); 109 } 110 111 public String format_daikon(@GuardSatisfied EltwiseIntLessThan this) { 112 if (debugEltwiseIntComparison) { 113 System.out.println(repr()); 114 } 115 116 return var().name() + " sorted by <"; 117 } 118 119 public String format_esc(@GuardSatisfied EltwiseIntLessThan this) { 120 String[] form = VarInfo.esc_quantify(false, var(), var()); 121 122 return form[0] + "((i+1 == j) ==> (" + form[1] + " < " + form[2] + "))" + form[3]; 123 } 124 125 public String format_java_family(@GuardSatisfied EltwiseIntLessThan this, OutputFormat format) { 126 return "daikon.Quant.eltwiseLT(" + var().name_using(format) + ")"; 127 } 128 129 public String format_csharp_contract(@GuardSatisfied EltwiseIntLessThan this) { 130 String[] split = var().csharp_array_split(); 131 return "Contract.ForAll(0, " + split[0] + ".Count()-1, i => " + split[0] + "[i]" + split[1] + " < " + split[0] + "[i+1]" + split[1] + ")"; 132 } 133 134 public String format_simplify(@GuardSatisfied EltwiseIntLessThan this) { 135 String[] form = VarInfo.simplify_quantify(QuantFlags.adjacent(), 136 var(), var()); 137 138 String comparator = "<"; 139 140 return form[0] + "(" + comparator + " " + form[1] + " " + form[2] + ")" 141 + form[3]; 142 } 143 144 @Override 145 @SuppressWarnings("UnnecessaryParentheses") // generated code, parentheses are sometimes needed 146 public InvariantStatus check_modified(long @Interned [] a, int count) { 147 for (int i = 1; i < a.length; i++) { 148 if (!((a[i - 1]) < ( a[i]))) { 149 return InvariantStatus.FALSIFIED; 150 } 151 } 152 return InvariantStatus.NO_CHANGE; 153 } 154 155 @Override 156 public InvariantStatus add_modified(long @Interned [] a, int count) { 157 return check_modified(a, count); 158 } 159 160 // Perhaps check whether all the arrays of interest have length 0 or 1. 161 162 @Override 163 protected double computeConfidence() { 164 165 return 1 - Math.pow(.5, ppt.num_samples()); 166 } 167 168 @Pure 169 @Override 170 public boolean isExact() { 171 172 return false; 173 } 174 175 @Pure 176 @Override 177 public boolean isSameFormula(Invariant other) { 178 return (other instanceof EltwiseIntLessThan); 179 } 180 181 // Not pretty... is there another way? 182 // Also, reasonably complicated, need to ensure exact correctness, not sure if the 183 // regression tests test this functionality 184 185 @Pure 186 @Override 187 public boolean isExclusiveFormula(Invariant other) { 188 // This whole approach is wrong in the case when the sequence can 189 // ever consist of only one element. For now, just forget 190 // it. -SMcC 191 if (true) { 192 return false; 193 } 194 195 if (other instanceof EltwiseIntComparison) { 196 197 return !((other instanceof EltwiseIntLessThan) || (other instanceof EltwiseFloatLessThan) 198 || (other instanceof EltwiseIntLessEqual) || (other instanceof EltwiseFloatLessEqual)); 199 200 } 201 return false; 202 } 203 204 // Look up a previously instantiated invariant. 205 public static @Nullable EltwiseIntLessThan find(PptSlice ppt) { 206 assert ppt.arity() == 1; 207 for (Invariant inv : ppt.invs) { 208 if (inv instanceof EltwiseIntLessThan) { 209 return (EltwiseIntLessThan) inv; 210 } 211 } 212 return null; 213 } 214 215 // Copied from IntComparison. 216 // public boolean isExclusiveFormula(Invariant other) 217 // { 218 // if (other instanceof IntComparison) { 219 // return core.isExclusiveFormula(((IntComparison) other).core); 220 // } 221 // if (other instanceof IntNonEqual) { 222 // return isExact(); 223 // } 224 // return false; 225 // } 226 227 /** 228 * This function returns whether a sample has been seen by this Invariant that includes two or 229 * more entries in an array. For a 0 or 1 element array a, a[] sorted by any binary operation is 230 * "vacuously true" because no check is ever made since the binary operation requires two 231 * operands. Thus although invariants of this type are true regarding 0 or 1 length arrays, they 232 * are meaningless. This function is meant to be used in isObviousImplied() to prevent such 233 * meaningless invariants from being printed. 234 */ 235 @Override 236 public boolean hasSeenNonSingletonSample() { 237 ValueSet.ValueSetScalarArray vs = (ValueSet.ValueSetScalarArray) ppt.var_infos[0].get_value_set(); 238 return vs.nonsingleton_arr_cnt() > 0; 239 } 240 241 @Pure 242 @Override 243 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 244 DiscardInfo super_result = super.isObviousDynamically(vis); 245 if (super_result != null) { 246 return super_result; 247 } 248 249 if (!hasSeenNonSingletonSample()) { 250 return new DiscardInfo(this, DiscardCode.obvious, 251 "No samples sequences of size >=2 were seen. Vacuously true."); 252 } 253 254 EltOneOf eoo = EltOneOf.find(ppt); 255 if ((eoo != null) && eoo.enoughSamples() && (eoo.num_elts() == 1)) { 256 return new DiscardInfo(this, DiscardCode.obvious, "The sequence contains all equal values."); 257 } 258 259 // sorted by (any operation) for an entire sequence -> sorted by that same 260 // operation for a subsequence 261 262 // also, sorted by < for entire -> sorted by <= for subsequence 263 // sorted by > for entire -> sorted by >= for subsequence 264 265 Derivation deriv = vis[0].derived; 266 267 if ((deriv instanceof SequenceScalarSubsequence) || (deriv instanceof SequenceFloatSubsequence)) { 268 // Find the slice with the full sequence, check for an invariant of this type 269 PptSlice sliceToCheck; 270 271 if (deriv instanceof SequenceScalarSubsequence) { 272 sliceToCheck = ppt.parent.findSlice(((SequenceScalarSubsequence)deriv).seqvar()); 273 } else { 274 sliceToCheck = ppt.parent.findSlice(((SequenceFloatSubsequence)deriv).seqvar()); 275 } 276 277 if (sliceToCheck != null) { 278 for (Invariant inv : sliceToCheck.invs) { 279 280 if (inv.getClass().equals(getClass())) { 281 String discardString = "This is a subsequence of a sequence for which the same invariant holds."; 282 return new DiscardInfo(this, DiscardCode.obvious, discardString); 283 } 284 } 285 } 286 } 287 288 return null; 289 } 290}