001// ***** This file is automatically generated from SequenceSubsequence.java.jpp 002 003package daikon.derive.binary; 004 005import org.checkerframework.dataflow.qual.Pure; 006import org.checkerframework.checker.lock.qual.GuardSatisfied; 007import org.checkerframework.dataflow.qual.SideEffectFree; 008import org.checkerframework.checker.interning.qual.Interned; 009import daikon.*; 010import daikon.derive.*; 011import org.plumelib.util.Intern; 012import org.plumelib.util.UtilPlume; 013 014public final class SequenceScalarSubsequence extends SequenceSubsequence { 015 // We are Serializable, so we specify a version to allow changes to 016 // method signatures without breaking serialization. If you add or 017 // remove fields, you should change this number to the current date. 018 static final long serialVersionUID = 20020801L; 019 020 // Variables starting with dkconfig_ should only be set via the 021 // daikon.config.Configuration interface. 022 /** Boolean. True iff SequenceScalarSubsequence derived variables should be generated. */ 023 public static boolean dkconfig_enabled = false; 024 025 /** 026 * Represents a subsequence of a sequence. The subsequence a[i..j] includes the endpoints i and j. 027 * The subsequence is meaningful if: 028 * 029 * <pre> 030 * i ≥ 0 031 * i ≤ a.length 032 * j ≥ -1 033 * j ≤ a.length-1 034 * i ≤ j+1 035 * </pre> 036 * 037 * These are the empty array: 038 * 039 * <pre> 040 * a[0..-1] 041 * a[a.length..a.length-1] 042 * </pre> 043 * 044 * These are illegal: 045 * 046 * <pre> 047 * a[1..-1] 048 * a[a.length..a.length-2] 049 * a[a.length+1..a.length] 050 * </pre> 051 * 052 * @param from_start true means the range goes 0..n; false means the range goes n..end. (n might 053 * be fudged through off_by_one.) 054 * @param off_by_one true means we should exclude the scalar from the range; false means we should 055 * include it 056 */ 057 SequenceScalarSubsequence( 058 VarInfo vi1, VarInfo vi2, boolean from_start, boolean off_by_one) { 059 super(vi1, vi2, from_start, off_by_one); 060 } 061 062 @SideEffectFree 063 @Override 064 public String toString(@GuardSatisfied SequenceScalarSubsequence this) { 065 String shift = ""; 066 if (index_shift < 0) { 067 shift = "" + index_shift; 068 } else if (index_shift > 0) { 069 shift = "+" + index_shift; 070 } 071 String seqname = seqvar().name().replace("[]", ""); 072 if (from_start) { 073 return seqname + "[.." + sclvar().name() + shift + "]"; 074 } else { 075 return seqname + "[" + sclvar().name() + shift + "..]"; 076 } 077 } 078 079 @Override 080 public ValueAndModified computeValueAndModifiedImpl(ValueTuple full_vt) { 081 int mod1 = base1.getModified(full_vt); 082 if (mod1 == ValueTuple.MISSING_NONSENSICAL) { 083 return ValueAndModified.MISSING_NONSENSICAL; 084 } 085 int mod2 = base2.getModified(full_vt); 086 if (mod2 == ValueTuple.MISSING_NONSENSICAL) { 087 return ValueAndModified.MISSING_NONSENSICAL; 088 } 089 090 Object val1 = base1.getValue(full_vt); 091 if (val1 == null) { 092 return ValueAndModified.MISSING_NONSENSICAL; 093 } 094 long[] val1_array = (long[]) val1; 095 int val2 = base2.getIndexValue(full_vt); 096 097 // One could argue that if the range exceeds the array bounds, one 098 // should just return the whole array; but we don't do that. We 099 // say MISSING instead. 100 101 // Note that the resulting array 102 // is a[begin_inclusive..end_exclusive-1], 103 // not a[begin_inclusive..end_exclusive]. 104 int begin_inclusive, end_exclusive; 105 if (from_start) { 106 // The subsequence is a[0..val2+index_shift] 107 begin_inclusive = 0; 108 end_exclusive = val2 + index_shift + 1; // +1: endpoint is exclusive 109 // end_exclusive = 0 is acceptable; that means the empty array (given 110 // that begin_inclusive is 0) 111 if ((end_exclusive < 0) || (end_exclusive > val1_array.length)) { 112 missing_array_bounds = true; 113 return ValueAndModified.MISSING_NONSENSICAL; 114 } 115 } else { 116 // The subsequence is a[val2+index_shift..a.length-1] 117 begin_inclusive = val2 + index_shift; 118 end_exclusive = val1_array.length; 119 // begin_inclusive = val1_array.length is acceptable; that means the 120 // empty array (given that end_exclusive is val1_arrayl.length) 121 // (It is permitted to have a[a.length..a.length-1], which means 122 // the empty array. But a[MAX_INT..MAX_INT-1] is not meaningful.) 123 if ((begin_inclusive < 0) || (begin_inclusive > val1_array.length)) { 124 missing_array_bounds = true; 125 return ValueAndModified.MISSING_NONSENSICAL; 126 } 127 } 128 129 int mod = 130 (((mod1 == ValueTuple.UNMODIFIED) && (mod2 == ValueTuple.UNMODIFIED)) 131 ? ValueTuple.UNMODIFIED 132 : ValueTuple.MODIFIED); 133 134 if ((begin_inclusive == 0) && (end_exclusive == val1_array.length)) { 135 return new ValueAndModified(val1, mod); 136 } 137 138 long[] subarr = Intern.internSubsequence(val1_array, begin_inclusive, end_exclusive); 139 return new ValueAndModified(subarr, mod); 140 } 141 142 @Pure 143 @Override 144 public boolean isSameFormula(Derivation other) { 145 return (other instanceof SequenceScalarSubsequence) 146 && (((SequenceScalarSubsequence) other).index_shift == this.index_shift) 147 && (((SequenceScalarSubsequence) other).from_start == this.from_start); 148 } 149}