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