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