001package daikon.derive.binary;
002
003import daikon.Quantify;
004import daikon.VarInfo;
005import org.checkerframework.checker.lock.qual.GuardSatisfied;
006import org.checkerframework.dataflow.qual.SideEffectFree;
007
008/** Derivations of the form A[0..i] or A[i..<em>end</em>], derived from A and i. */
009public abstract class SequenceSubsequence extends BinaryDerivation {
010  static final long serialVersionUID = 20020801L;
011
012  // Variables starting with dkconfig_ should only be set via the
013  // daikon.config.Configuration interface.
014
015  // base1 is the sequence
016  // base2 is the scalar
017  public VarInfo seqvar(@GuardSatisfied SequenceSubsequence this) {
018    return base1;
019  }
020
021  public VarInfo sclvar(@GuardSatisfied SequenceSubsequence this) {
022    return base2;
023  }
024
025  // Indicates whether the subscript is an index of valid data or a limit
026  // (one element beyond the data of interest).  The first (or last)
027  // element of the derived variable is at index seqvar()+index_shift.
028  public final int index_shift;
029
030  // True for deriving from the start of the sequence to the scalar: B[0..I]
031  // False for deriving from the scalar to the end of the sequence: B[I..]
032  public final boolean from_start;
033
034  /**
035   * @param from_start true means the range goes 0..n; false means the range goes n..end. (n might
036   *     be fudged through off_by_one.)
037   * @param off_by_one true means we should exclude the scalar from the range; false means we should
038   *     include it
039   */
040  protected SequenceSubsequence(VarInfo vi1, VarInfo vi2, boolean from_start, boolean off_by_one) {
041    super(vi1, vi2);
042    this.from_start = from_start;
043    if (off_by_one) {
044      index_shift = from_start ? -1 : +1;
045    } else {
046      index_shift = 0;
047    }
048  }
049
050  @Override
051  protected VarInfo makeVarInfo() {
052    VarInfo seqvar = seqvar();
053    VarInfo sclvar = sclvar();
054
055    VarInfo vi;
056    if (from_start) {
057      vi = VarInfo.make_subsequence(seqvar, null, 0, sclvar, index_shift);
058    } else {
059      vi = VarInfo.make_subsequence(seqvar, sclvar, index_shift, null, 0);
060    }
061
062    return vi;
063  }
064
065  @Override
066  public Quantify.Term get_lower_bound() {
067    if (from_start) {
068      return new Quantify.Constant(0);
069    } else {
070      return new Quantify.VarPlusOffset(sclvar(), index_shift);
071    }
072  }
073
074  @Override
075  public Quantify.Term get_upper_bound() {
076    if (from_start) {
077      return new Quantify.VarPlusOffset(sclvar(), index_shift);
078    } else {
079      return new Quantify.Length(seqvar(), -1);
080    }
081  }
082
083  @Override
084  public VarInfo get_array_var() {
085    return seqvar();
086  }
087
088  @SideEffectFree
089  @Override
090  public String csharp_name(String index) {
091    // String lower = get_lower_bound().csharp_name();
092    // String upper = get_upper_bound().csharp_name();
093    // We do not need to check if seqvar().isPrestate() because it is redundant.
094    // return seqvar().csharp_name() + ".Slice(" + lower + ", " + upper + ")";
095    return "\"SequenceSubsequence.java.jpp unimplemented\" != null"; // "interned"
096  }
097
098  @SideEffectFree
099  @Override
100  public String esc_name(String index) {
101    return String.format(
102        "%s[%s..%s]",
103        seqvar().esc_name(), get_lower_bound().esc_name(), get_upper_bound().esc_name());
104  }
105
106  @Override
107  @SuppressWarnings("nullness")
108  public String jml_name(String index) {
109
110    // The slice routine needs the actual length as opposed to the
111    // highest legal index.
112    Quantify.Term upper = get_upper_bound();
113    if (upper instanceof Quantify.Length) {
114      ((Quantify.Length) upper).set_offset(0);
115    }
116
117    if (seqvar().isPrestate()) {
118      return String.format(
119          "\\old(daikon.Quant.slice(%s, %s, %s))",
120          seqvar().enclosing_var.postState.jml_name(),
121          get_lower_bound().jml_name(true),
122          upper.jml_name(true));
123    } else {
124      return String.format(
125          "daikon.Quant.slice(%s, %s, %s)",
126          seqvar().enclosing_var.jml_name(), get_lower_bound().jml_name(), upper.jml_name());
127    }
128  }
129
130  /** Adds one to the default complexity if index_shift is not 0. */
131  @Override
132  public int complexity() {
133    return super.complexity() + ((index_shift != 0) ? 1 : 0);
134  }
135}