001// ***** This file is automatically generated from SequenceArbitrarySubsequence.java.jpp 002 003package daikon.derive.ternary; 004 005import org.checkerframework.dataflow.qual.SideEffectFree; 006import org.checkerframework.dataflow.qual.Pure; 007import org.checkerframework.checker.interning.qual.Interned; 008import daikon.*; 009import daikon.derive.*; 010import org.plumelib.util.ArraysPlume; 011import org.plumelib.util.Intern; 012 013public final class SequenceStringArbitrarySubsequence extends TernaryDerivation { 014 // We are Serializable, so we specify a version to allow changes to 015 // method signatures without breaking serialization. If you add or 016 // remove fields, you should change this number to the current date. 017 static final long serialVersionUID = 20020122L; 018 019 // Variables starting with dkconfig_ should only be set via the 020 // daikon.config.Configuration interface. 021 /** Boolean. True iff SequenceStringArbitrarySubsequence derived variables should be generated. */ 022 public static boolean dkconfig_enabled = false; 023 024 // base1 is the sequence 025 // base2 is the starting index 026 // base3 is the ending index 027 public VarInfo seqvar() { 028 return base1; 029 } 030 031 public VarInfo startvar() { 032 return base2; 033 } 034 035 public VarInfo endvar() { 036 return base3; 037 } 038 039 // True if the subsequence includes its left endpoint. 040 public final boolean left_closed; 041 042 // True if the subsequence includes its right endpoint. 043 public final boolean right_closed; 044 045 /** 046 * Represents a subsequence of a sequence. The subsequence a[i..j] includes the endpoints i and j. 047 * The subsequence is meaningful if: 048 * 049 * <pre> 050 * i ≥ 0 051 * i ≤ a.length 052 * j ≥ -1 053 * j ≤ a.length-1 054 * i ≤ j+1 055 * </pre> 056 * 057 * These are the empty array: 058 * 059 * <pre> 060 * a[0..-1] 061 * a[a.length..a.length-1] 062 * </pre> 063 * 064 * These are illegal: 065 * 066 * <pre> 067 * a[1..-1] 068 * a[a.length..a.length-2] 069 * a[a.length+1..a.length] 070 * </pre> 071 * 072 * @param left_closed true means the range starts at i; false means it starts at i+1 073 * @param right_closed true means the range ends at j; false means it ends at j-1 074 */ 075 SequenceStringArbitrarySubsequence( 076 VarInfo vi1, VarInfo vi2, VarInfo vi3, boolean left_closed, boolean right_closed) { 077 super(vi1, vi2, vi3); 078 this.left_closed = left_closed; 079 this.right_closed = right_closed; 080 } 081 082 @Override 083 public ValueAndModified computeValueAndModified(ValueTuple full_vt) { 084 int mod1 = base1.getModified(full_vt); 085 if (mod1 == ValueTuple.MISSING_NONSENSICAL) { 086 return ValueAndModified.MISSING_NONSENSICAL; 087 } 088 int mod2 = base2.getModified(full_vt); 089 if (mod2 == ValueTuple.MISSING_NONSENSICAL) { 090 return ValueAndModified.MISSING_NONSENSICAL; 091 } 092 int mod3 = base2.getModified(full_vt); 093 if (mod3 == ValueTuple.MISSING_NONSENSICAL) { 094 return ValueAndModified.MISSING_NONSENSICAL; 095 } 096 097 Object val1 = base1.getValue(full_vt); 098 if (val1 == null) { 099 return ValueAndModified.MISSING_NONSENSICAL; 100 } 101 @Interned String[] val1_array = (@Interned String[]) val1; 102 int val2 = base2.getIndexValue(full_vt); 103 int val3 = base3.getIndexValue(full_vt); 104 105 // One could argue that if the range exceeds the array bounds, one 106 // should just return the whole array; but we don't do that. We 107 // say MISSING instead. 108 109 // Note that the resulting array 110 // is a[begin_inclusive..end_exclusive-1], 111 // not a[begin_inclusive..end_exclusive]. 112 int begin_inclusive, end_exclusive; 113 if (left_closed) { 114 begin_inclusive = val2; 115 } else { 116 begin_inclusive = val2 + 1; 117 } 118 // begin_inclusive = val1_array.length is acceptable; that means the 119 // empty array (given that end_exclusive is val1_arrayl.length) 120 // (It is permitted to have a[a.length..a.length-1], which means 121 // the empty array. But a[MAX_INT..MAX_INT-1] is not meaningful.) 122 if ((begin_inclusive < 0) || (begin_inclusive > val1_array.length)) { 123 missing_array_bounds = true; 124 return ValueAndModified.MISSING_NONSENSICAL; 125 } 126 127 if (right_closed) { 128 end_exclusive = val3 + 1; 129 } else { 130 end_exclusive = val3; 131 } 132 // end_exclusive = 0 is acceptable; that means the empty array (given 133 // that begin_inclusive is 0) 134 if ((end_exclusive < 0) || (end_exclusive > val1_array.length)) { 135 missing_array_bounds = true; 136 return ValueAndModified.MISSING_NONSENSICAL; 137 } 138 139 if (end_exclusive - begin_inclusive < 0) { 140 missing_array_bounds = true; 141 return ValueAndModified.MISSING_NONSENSICAL; 142 } 143 144 int mod = 145 (((mod1 == ValueTuple.UNMODIFIED) 146 && (mod2 == ValueTuple.UNMODIFIED) 147 && (mod3 == ValueTuple.UNMODIFIED)) 148 ? ValueTuple.UNMODIFIED 149 : ValueTuple.MODIFIED); 150 151 if ((begin_inclusive == 0) && (end_exclusive == val1_array.length)) { 152 return new ValueAndModified(val1, mod); 153 } 154 155 @Interned String[] subarr = 156 ArraysPlume.subarray(val1_array, begin_inclusive, end_exclusive - begin_inclusive); 157 subarr = Intern.intern(subarr); 158 return new ValueAndModified(subarr, mod); 159 } 160 161 @Override 162 protected VarInfo makeVarInfo() { 163 164 return VarInfo.make_subsequence( 165 seqvar(), startvar(), (left_closed ? 0 : 1), endvar(), (right_closed ? 0 : -1)); 166 } 167 168 /** Returns the lower bound of the slice. */ 169 @Override 170 public Quantify.Term get_lower_bound() { 171 return new Quantify.VarPlusOffset(startvar(), (left_closed ? 0 : 1)); 172 } 173 174 /** Returns the upper bound of the slice. */ 175 @Override 176 public Quantify.Term get_upper_bound() { 177 return new Quantify.VarPlusOffset(endvar(), (right_closed ? 0 : 1)); 178 } 179 180 /** Returns the array variable for this slice. */ 181 @Override 182 public VarInfo get_array_var() { 183 return seqvar(); 184 } 185 186 @Pure 187 @Override 188 public boolean isSameFormula(Derivation other) { 189 return (other instanceof SequenceStringArbitrarySubsequence) 190 && (((SequenceStringArbitrarySubsequence) other).left_closed == this.left_closed) 191 && (((SequenceStringArbitrarySubsequence) other).right_closed == this.right_closed); 192 } 193 194 /** Returns the csharp name. */ 195 @SideEffectFree 196 @Override 197 public String csharp_name(String index) { 198 String lower = get_lower_bound().csharp_name(); 199 String upper = get_upper_bound().csharp_name(); 200 // We do not need to check if seqvar().isPrestate() because it is redundant. 201 return seqvar().csharp_name() + ".Slice(" + lower + ", " + upper + ")"; 202 } 203 204 /** Returns the ESC name. */ 205 @SideEffectFree 206 @Override 207 public String esc_name(String index) { 208 return String.format( 209 "%s[%s..%s]", 210 seqvar().esc_name(), get_lower_bound().esc_name(), get_upper_bound().esc_name()); 211 } 212}