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