001// ***** This file is automatically generated from SequenceSubscript.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 java.util.logging.Logger;
010import daikon.*;
011import daikon.derive.*;
012import org.plumelib.util.Intern;
013import org.plumelib.util.UtilPlume;
014
015public final class SequenceScalarSubscript extends BinaryDerivation {
016  static final long serialVersionUID = 20020122L;
017
018  // Variables starting with dkconfig_ should only be set via the
019  // daikon.config.Configuration interface.
020  /** Boolean. True iff SequenceScalarSubscript derived variables should be generated. */
021  public static boolean dkconfig_enabled = true;
022
023  /** General debug tracer. */
024  public static final Logger debug = Logger.getLogger("daikon.derive.binary.SequenceScalarSubscript");
025
026  // base1 is the sequence
027  // base2 is the scalar
028  public VarInfo seqvar(@GuardSatisfied SequenceScalarSubscript this) {
029    return base1;
030  }
031
032  public VarInfo sclvar(@GuardSatisfied SequenceScalarSubscript this) {
033    return base2;
034  }
035
036  public VarInfo seq_enclosing_var() {
037    VarInfo result = seqvar().enclosing_var;
038    // When using old dtrace file format, this can fail.
039    assert result != null : "@AssumeAssertion(nullness): foo[] has enclosing_var foo";
040    return result;
041  }
042
043  // Indicates whether the subscript is an index of valid data or a limit
044  // (one element beyond the data of interest).
045  // Value is -1 or 0.
046  public final int index_shift;
047
048  SequenceScalarSubscript(VarInfo vi1, VarInfo vi2, boolean less1) {
049    super(vi1, vi2);
050    if (less1) {
051      index_shift = -1;
052    } else {
053      index_shift = 0;
054    }
055    debug.fine("SequenceScalarSubscript(" + vi1 + ", " + vi2 + ", " + less1 + ") => " + this);
056  }
057
058  @SideEffectFree
059  @Override
060  public String toString(@GuardSatisfied SequenceScalarSubscript this) {
061    String shift = "";
062    if (index_shift < 0) {
063      shift = "" + index_shift;
064    } else if (index_shift > 0) {
065      shift = "+" + index_shift;
066    }
067    return seqvar().name().replace("[]", "") + "[" + sclvar().name() + shift + "]";
068  }
069
070  @Override
071  public ValueAndModified computeValueAndModifiedImpl(ValueTuple full_vt) {
072    int mod1 = base1.getModified(full_vt);
073    if (mod1 == ValueTuple.MISSING_NONSENSICAL) {
074      return ValueAndModified.MISSING_NONSENSICAL;
075    }
076    int mod2 = base2.getModified(full_vt);
077    if (mod2 == ValueTuple.MISSING_NONSENSICAL) {
078      return ValueAndModified.MISSING_NONSENSICAL;
079    }
080    Object val1 = base1.getValue(full_vt);
081    if (val1 == null) {
082      return ValueAndModified.MISSING_NONSENSICAL;
083    }
084    long[] val1_array = (long[]) val1;
085    int val2 = base2.getIndexValue(full_vt) + index_shift;
086    if ((val2 < 0) || (val2 >= val1_array.length)) {
087      // if (!missing_array_bounds)
088      //   System.out.println ("out of bounds" + base1.name() + " "
089      //                      + base2.name() + " @" + base1.ppt.name());
090      missing_array_bounds = true;
091      return ValueAndModified.MISSING_NONSENSICAL;
092    }
093    long val = val1_array[val2];
094    int mod =
095        (((mod1 == ValueTuple.UNMODIFIED) && (mod2 == ValueTuple.UNMODIFIED))
096         ? ValueTuple.UNMODIFIED
097         : ValueTuple.MODIFIED);
098    return new ValueAndModified(Intern.internedLong(val), mod);
099  }
100
101  @Override
102  protected VarInfo makeVarInfo() {
103    return VarInfo.make_subscript(seqvar(), sclvar(), index_shift);
104  }
105
106  @Pure
107  @Override
108  public boolean isSameFormula(Derivation other) {
109    return (other instanceof SequenceScalarSubscript)
110      && (((SequenceScalarSubscript) other).index_shift == this.index_shift);
111  }
112
113  @SuppressWarnings("nullness")
114  @SideEffectFree
115  @Override
116  public String esc_name(String index) {
117    if (seqvar().isPrestate()) {
118      return String.format(
119          "\\old(%s[%s])",
120          seqvar().enclosing_var.postState.esc_name(),
121          inside_esc_name(sclvar(), true, index_shift));
122    } else {
123      return String.format(
124          "%s[%s%s]",
125          seqvar().enclosing_var.esc_name(), sclvar().esc_name(), shift_str(index_shift));
126    }
127  }
128
129  @SuppressWarnings("nullness")
130  @Override
131  public String jml_name(String index) {
132    String get_element = "daikon.Quant.getElement_int";
133    if (seqvar().file_rep_type.baseIsHashcode()) {
134      get_element = "daikon.Quant.getElement_Object";
135    } else if (seqvar().file_rep_type.baseIsBoolean()) {
136      get_element = "daikon.Quant.getElement_boolean";
137    }
138    if (seqvar().isPrestate()) {
139      return String.format(
140          "\\old(%s(%s, %s))",
141          get_element,
142          seqvar().enclosing_var.postState.jml_name(),
143          inside_jml_name(sclvar(), true, index_shift));
144    } else {
145      return String.format(
146          "%s(%s, %s%s)",
147          get_element,
148          seqvar().enclosing_var.jml_name(),
149          sclvar().jml_name(),
150          shift_str(index_shift));
151    }
152  }
153
154  @SuppressWarnings("nullness")
155  @SideEffectFree
156  @Override
157  public String csharp_name(String index) {
158    String[] split = seqvar().csharp_array_split();
159    if (seqvar().isPrestate()) {
160      return String.format(
161          "Contract.OldValue(%s[%s]%s)",
162          seqvar().enclosing_var.postState.csharp_name(),
163          inside_csharp_name(sclvar(), true, index_shift),
164          split[1]);
165    } else {
166      return String.format(
167          "%s[%s%s]%s", split[0], sclvar().csharp_name(), shift_str(index_shift), split[1]);
168    }
169  }
170
171  @SuppressWarnings("nullness")
172  @SideEffectFree
173  @Override
174  public String simplify_name() {
175    String subscript = sclvar().simplify_name();
176    if (index_shift < 0) {
177      subscript = String.format("(- %s %d)", subscript, -index_shift);
178    } else if (index_shift > 0) {
179      subscript = String.format("(+ %s %d)", subscript, index_shift);
180    }
181
182    return String.format(
183        "(select (select elems %s) %s)", seqvar().enclosing_var.simplify_name(), subscript);
184  }
185
186  /** Adds one to the default complexity if index_shift is not 0. */
187  @Override
188  public int complexity() {
189    return super.complexity() + ((index_shift != 0) ? 1 : 0);
190  }
191}