001// ***** This file is automatically generated from SequenceSubscriptFactory.java.jpp 002 003package daikon.derive.binary; 004 005import daikon.*; 006import daikon.inv.binary.twoScalar.*; // for IntComparison 007import daikon.inv.unary.scalar.*; // for LowerBound 008import java.util.*; 009import org.checkerframework.checker.nullness.qual.Nullable; 010 011// This controls derivations which use the scalar as an index into the 012// sequence, such as getting the element at that index or a subsequence up 013// to that index. 014 015public final class SequenceFloatSubscriptFactory extends BinaryDerivationFactory { 016 static boolean debug_set = false; 017 static boolean debug_class_match = false; 018 019 // When calling/creating the derivations, arrange that: 020 // base1 is the sequence 021 // base2 is the scalar 022 023 @Override 024 public BinaryDerivation @Nullable [] instantiate(VarInfo vi1, VarInfo vi2) { 025 026 Debug debug = null; 027 if (!debug_set) { 028 debug_class_match = Debug.class_match(getClass()); 029 debug_set = true; 030 } 031 if (debug_class_match && Debug.logOn()) { 032 debug = Debug.newDebug(getClass(), vi1.ppt, Debug.vis(vi1, vi2)); 033 } 034 if (debug != null) { 035 debug.log("Considering Sequence Subscript Derivation"); 036 } 037 038 // check if the derivations are globally disabled 039 boolean enable_subscript = SequenceFloatSubscript.dkconfig_enabled; 040 boolean enable_subsequence = SequenceFloatSubsequence.dkconfig_enabled; 041 if (!enable_subscript && !enable_subsequence) { 042 if (debug != null) { 043 debug.log("Not Enabled"); 044 } 045 return null; 046 } 047 048 // This is not the very most efficient way to do this, but at least it is 049 // comprehensible. 050 VarInfo seqvar; 051 VarInfo sclvar; 052 053 if ((vi1.rep_type == ProglangType.DOUBLE_ARRAY) && (vi2.rep_type == ProglangType.DOUBLE)) { 054 seqvar = vi1; 055 sclvar = vi2; 056 } else if ((vi2.rep_type == ProglangType.DOUBLE_ARRAY) && (vi1.rep_type == ProglangType.DOUBLE)) { 057 seqvar = vi2; 058 sclvar = vi1; 059 } else { 060 if (debug != null) { 061 debug.log("Not Array/Int combination"); 062 } 063 return null; 064 } 065 066 if (!seqvar.aux.hasOrder()) { 067 // Indexing doesn't make sense if order doesn't matter 068 if (debug != null) { 069 debug.log("Not ordered"); 070 } 071 return null; 072 } 073 074 if (!seqvar.indexCompatible(sclvar)) { 075 if (debug != null) { 076 debug.log("variables are not comparable"); 077 } 078 return null; 079 } 080 081 // For now, do nothing if the sequence is itself derived. 082 if (seqvar.derived != null) { 083 if (debug != null) { 084 debug.log("Sequence variable derived"); 085 } 086 return null; 087 } 088 // For now, do nothing if the scalar is itself derived. 089 if (sclvar.derived != null) { 090 if (debug != null) { 091 debug.log("Scalar variable derived"); 092 } 093 return null; 094 } 095 096 VarInfo seqsize = seqvar.sequenceSize(); 097 // System.out.println("BinaryDerivation.instantiate: sclvar=" + sclvar.name 098 // + ", sclvar_rep=" + sclvar.canonicalRep().name 099 // + ", seqsize=" + seqsize.name 100 // + ", seqsize_rep=" + seqsize.canonicalRep().name); 101 102 // SUPPRESS DERIVED VARIABLE: a[i] where i == a.length 103 // SUPPRESS DERIVED VARIABLE: a[i-1] where i == a.length 104 // SUPPRESS DERIVED VARIABLE: a[..i] where i == a.length 105 // SUPPRESS DERIVED VARIABLE: a[..i-1] where i == a.length 106 // SUPPRESS DERIVED VARIABLE: a[i..] where i == a.length 107 // SUPPRESS DERIVED VARIABLE: a[i+1..] where i == a.length 108 // Since both are canonical, this is equivalent to 109 // "if (sclvar.canonicalRep() == seqsize.canonicalRep()) ..." 110 if (sclvar == seqsize) { 111 // a[len] a[len-1] a[0..len] a[0..len-1] a[len..] a[len+1..] 112 Global.tautological_suppressed_derived_variables += 6; 113 if (debug != null) { 114 debug.log("sclvar related to length"); 115 } 116 return null; 117 } 118 119 // SUPPRESS DERIVED VARIABLE: a[i] where (i >= a.length) can be true 120 // SUPPRESS DERIVED VARIABLE: a[i-1] where (i > a.length) can be true 121 // SUPPRESS DERIVED VARIABLE: a[..i] where (i >= a.length) can be true 122 // SUPPRESS DERIVED VARIABLE: a[..i-1] where (i > a.length) can be true 123 // SUPPRESS DERIVED VARIABLE: a[i..] where (i > a.length) can be true 124 // SUPPRESS DERIVED VARIABLE: a[i+1..] where (i >= a.length) can be true 125 // ***** This eliminates the derivation if it can *ever* be 126 // nonsensical/missing. Is that what I want? 127 // Find an IntComparison relationship over the scalar and the sequence 128 // size, if possible. 129 if (seqsize != null) { 130 assert sclvar.ppt == seqsize.ppt; 131 PptSlice compar_slice = sclvar.ppt.findSlice_unordered(sclvar, seqsize); 132 if (compar_slice != null) { 133 if ((sclvar.varinfo_index < seqsize.varinfo_index) 134 ? FloatLessEqual.find(compar_slice) == null // sclvar can be more than seqsize 135 : FloatGreaterEqual.find(compar_slice) == null // seqsize can be less than sclvar 136 ) { 137 Global.nonsensical_suppressed_derived_variables += 6; 138 if (debug != null) { 139 debug.log("sclvar is sometimes > length sequence"); 140 } 141 return null; 142 } else if (FloatEqual.find(compar_slice) != null) { 143 Global.nonsensical_suppressed_derived_variables += 3; 144 ArrayList<BinaryDerivation> result = new ArrayList<>(); 145 if (enable_subscript) { 146 result.add(new SequenceFloatSubscript(seqvar, sclvar, true)); // a[i-1] 147 } 148 if (enable_subsequence) { 149 result.add(new SequenceFloatSubsequence(seqvar, sclvar, true, true)); // a[..i-1] 150 result.add(new SequenceFloatSubsequence(seqvar, sclvar, false, false)); // a[i..] 151 } 152 if (debug != null) { 153 debug.log("Found derivations: " + result); 154 } 155 return result.toArray(new BinaryDerivation[0]); 156 } 157 } 158 } 159 160 // Abstract out these next two. 161 162 // If the scalar is a constant, then do all the following checks: 163 // 164 // If the scalar is a constant < 0: 165 // all derived variables are nonsensical 166 // SUPPRESS DERIVED VARIABLE: a[i] where i<0 and i is constant 167 // SUPPRESS DERIVED VARIABLE: a[i-1] where i<0 and i is constant 168 // SUPPRESS DERIVED VARIABLE: a[..i] where i<0 and i is constant 169 // SUPPRESS DERIVED VARIABLE: a[..i-1] where i<0 and i is constant 170 // SUPPRESS DERIVED VARIABLE: a[i..] where i<0 and i is constant 171 // SUPPRESS DERIVED VARIABLE: a[i+1..] where i<0 and i is constant 172 // If the scalar is the constant 0: 173 // array[0] is already extracted 174 // array[-1] is nonsensical 175 // array[0..0] is already extracted 176 // array[0..-1] is nonsensical 177 // array[0..] is the same as array[] 178 // array[1..] should be extracted 179 // SUPPRESS DERIVED VARIABLE: a[i] where i==0 180 // SUPPRESS DERIVED VARIABLE: a[i-1] where i==0 181 // SUPPRESS DERIVED VARIABLE: a[..i] where i==0 182 // SUPPRESS DERIVED VARIABLE: a[..i-1] where i==0 183 // SUPPRESS DERIVED VARIABLE: a[i..] where i==0 184 // If the scalar is the constant 1: 185 // array[1] is already extracted 186 // array[0] is already extracted 187 // array[0..1] should be extracted 188 // array[0..0] is already extracted 189 // array[1..] should be extracted 190 // array[2..] should be extracted 191 // SUPPRESS DERIVED VARIABLE: a[i] where i==1 192 // SUPPRESS DERIVED VARIABLE: a[i-1] where i==1 193 // SUPPRESS DERIVED VARIABLE: a[..i] where i==1 194 // SUPPRESS DERIVED VARIABLE: a[..i-1] where i==1 195 196 // Commented out: seems to be eliminating desired invariants. 197 if (false) { 198 // If the lower bound for the variable is less than 0 (that is, if the 199 // putative index can ever be negative), then suppress most of the 200 // derived variables. 201 // SUPPRESS DERIVED VARIABLE: a[i] where i<0 can be true 202 // SUPPRESS DERIVED VARIABLE: a[i-1] where i<1 can be true 203 // SUPPRESS DERIVED VARIABLE: a[..i] where i<-1 can be true 204 // SUPPRESS DERIVED VARIABLE: a[..i-1] where i<0 can be true 205 // SUPPRESS DERIVED VARIABLE: a[i..] where i<0 can be true 206 // SUPPRESS DERIVED VARIABLE: a[i+1..] where i<-1 can be true 207 PptSlice unary_slice = sclvar.ppt.findSlice(sclvar); 208 if (unary_slice != null) { 209 LowerBound lb_inv = LowerBound.find(unary_slice); 210 if (lb_inv != null) { 211 long lower_bound = lb_inv.min(); 212 if (lower_bound < -1) { 213 Global.nonsensical_suppressed_derived_variables += 6; 214 return null; 215 } else if (lower_bound == -1) { 216 Global.nonsensical_suppressed_derived_variables += 5; 217 return enable_subsequence 218 ? new BinaryDerivation[] { 219 new SequenceFloatSubsequence(seqvar, sclvar, true, false), // a[..i] 220 new SequenceFloatSubsequence(seqvar, sclvar, false, true), // a[i+1..] 221 } 222 : null; 223 } else if (lower_bound == 0) { 224 Global.nonsensical_suppressed_derived_variables += 1; 225 ArrayList<BinaryDerivation> result = new ArrayList<>(); 226 if (enable_subscript) { 227 result.add(new SequenceFloatSubscript(seqvar, sclvar, false)); // a[i] 228 } 229 if (enable_subsequence) { 230 result.add(new SequenceFloatSubsequence(seqvar, sclvar, false, false)); // a[i..] 231 result.add(new SequenceFloatSubsequence(seqvar, sclvar, false, true)); // a[i+1..] 232 result.add(new SequenceFloatSubsequence(seqvar, sclvar, true, false)); // a[..i] 233 result.add(new SequenceFloatSubsequence(seqvar, sclvar, true, true)); // a[..i-1] 234 } 235 return result.toArray(new BinaryDerivation[0]); 236 } 237 } 238 } 239 } 240 241 // If, for some canonical j, j=index+1, don't create array[index+1..]. 242 // If j=index-1, then don't create array[index-1] or array[0..index-1]. 243 // (j can have higher or lower VarInfo index than i.) 244 boolean suppress_minus_1 = false; 245 boolean suppress_plus_1 = false; 246 247 // This ought to be abstracted out, maybe 248 { 249 assert sclvar.ppt == seqvar.ppt; 250 List<LinearBinaryFloat> lbs = LinearBinaryFloat.findAll(sclvar); 251 // System.out.println("For " + sclvar.name + ", " + lbs.size() + " LinearBinary invariants"); 252 for (Object lbObject : lbs) { 253 LinearBinaryFloat lb = (LinearBinaryFloat) lbObject; 254 // lb asserts that lb.var2() = lb.core.a * lb.var1() + lb.core.b <-- old 255 // Note that var2 comes before var1; this makes the most sense 256 // if you think of them as "y" and "x". <-- old 257 258 // lb asserts that lb.core.a * lb.var1() + lb.core.b * lb.var2() + lb.core.c == 0 259 // or lb.var2() == - (lb.core.a / lb.core.b) * lb.var1() - lb.core.c / lb.core.b 260 261 // if (lb.core.a == 1) { 262 if (-lb.core.a / lb.core.b == 1) { 263 // Don't set unconditionally, and don't break: we want to check 264 // other variables as well. 265 // if (lb.core.b == -1) { 266 if (-lb.core.c / lb.core.b == -1) { 267 if (lb.var1() == sclvar) { 268 // j = index - 1 269 suppress_minus_1 = true; 270 } else { 271 // index = j - 1, so j = index + 1 272 suppress_plus_1 = true; 273 } 274 } 275 // if (lb.core.b == 1) { 276 if (-lb.core.c / lb.core.b == -1) { 277 if (lb.var1() == sclvar) { 278 // j = index + 1 279 suppress_plus_1 = true; 280 } else { 281 // index = j + 1, so j = index - 1 282 suppress_minus_1 = true; 283 } 284 } 285 // System.out.println("For " + sclvar.name + " suppression: " 286 // + "minus=" + suppress_minus_1 287 // + " plus=" + suppress_plus_1 288 // + " because of " + lb.format()); 289 } 290 } 291 } 292 293 if (suppress_minus_1) { 294 Global.tautological_suppressed_derived_variables += 2; 295 } 296 if (suppress_plus_1) { 297 Global.tautological_suppressed_derived_variables += 1; 298 } 299 300 // End of applicability tests; now actually create the invariants 301 302 List<BinaryDerivation> result = new ArrayList<>(6); 303 if (enable_subscript) { 304 // a[i] 305 result.add(new SequenceFloatSubscript(seqvar, sclvar, false)); 306 // a[i-1] 307 if (!suppress_minus_1) { 308 result.add(new SequenceFloatSubscript(seqvar, sclvar, true)); 309 } 310 } 311 if (enable_subsequence) { 312 // a[i..] 313 result.add(new SequenceFloatSubsequence(seqvar, sclvar, false, false)); 314 // a[i+1..] 315 if (!suppress_plus_1) { 316 result.add(new SequenceFloatSubsequence(seqvar, sclvar, false, true)); 317 } 318 // a[..i] 319 result.add(new SequenceFloatSubsequence(seqvar, sclvar, true, false)); 320 // a[..i-1] 321 if (!suppress_minus_1) { 322 result.add(new SequenceFloatSubsequence(seqvar, sclvar, true, true)); 323 } 324 } 325 if (debug != null) { 326 debug.log("Found derivations " + result); 327 } 328 return result.toArray(new BinaryDerivation[0]); 329 } 330}