001// ***** This file is automatically generated from SequencesPredicate.java.jpp
002
003package daikon.derive.binary;
004
005import org.checkerframework.dataflow.qual.Pure;
006import org.checkerframework.dataflow.qual.SideEffectFree;
007import org.checkerframework.checker.lock.qual.GuardSatisfied;
008import org.checkerframework.checker.interning.qual.Interned;
009import daikon.*;
010import daikon.derive.*;
011import java.util.logging.Logger;
012import org.plumelib.util.Intern;
013
014/**
015 * Derived variable representing the selecting of elements of one sequence based on the values of
016 * another sequence. We only predicate if we know that both sequences came from the same original
017 * data structure. Derived type is the same as that of the first sequence.
018 */
019public final class SequencesPredicate extends BinaryDerivation {
020  // We are Serializable, so we specify a version to allow changes to
021  // method signatures without breaking serialization.  If you add or
022  // remove fields, you should change this number to the current date.
023  static final long serialVersionUID = 20020122L;
024
025  /** Debug tracer. */
026  public static final Logger debug =
027    Logger.getLogger("daikon.derive.binary.SequencesPredicate");
028
029  // Variables starting with dkconfig_ should only be set via the
030  // daikon.config.Configuration interface.
031  /** Boolean. True iff SequencesPredicate derived variables should be generated. */
032  public static boolean dkconfig_enabled = false;
033
034  /**
035   * Boolean. True if Daikon should only generate derivations on fields of the same data structure.
036   */
037  public static boolean dkconfig_fieldOnly = true;
038
039  /** Boolean. True if Daikon should only generate derivations on boolean predicates. */
040  public static boolean dkconfig_boolOnly = true;
041
042  @Override
043  public VarInfo var1(@GuardSatisfied SequencesPredicate this) {
044    return base1;
045  }
046
047  @Override
048  public VarInfo var2(@GuardSatisfied SequencesPredicate this) {
049    return base2;
050  }
051
052  /** What value to predicate on. */
053  private long choose;
054
055  /** Whether we keep or discard values that match this.choose. */
056  private boolean keep;
057
058  /** What this predication is called (e.g. for choose == 0 and 1, use "false" and "true"). */
059  private String name;
060
061  /**
062   * Create a new SequencesJoin derivation.
063   *
064   * @param vi1 the first of the two variables this is based on
065   * @param vi2 the second of the two variables this is based on
066   */
067  SequencesPredicate(VarInfo vi1, VarInfo vi2, long argChoose, String argName) {
068    this(vi1, vi2, argChoose, argName, true);
069  }
070
071  /**
072   * Create a new SequencesJoin derivation.
073   *
074   * @param vi1 the first of the two variables this is based on
075   * @param vi2 the second of the two variables this is based on
076   */
077  SequencesPredicate(
078      VarInfo vi1, VarInfo vi2, long argChoose, String argName, boolean argKeep) {
079    super(vi1, vi2);
080    choose = argChoose;
081    name = argName;
082    keep = argKeep;
083  }
084
085  /**
086   * Returns a subset of val1 such that the corresponding element in var2 equals this.choose. It is
087   * assumed that val1 and val2 originated from the same, larger data structure.
088   *
089   * @param full_vt the value tuple of a program point to compute the derived value from
090   */
091  @Override
092  public ValueAndModified computeValueAndModifiedImpl(ValueTuple full_vt) {
093    Object val1 = var1().getValue(full_vt);
094    Object val2 = var2().getValue(full_vt);
095
096    int length1 = -1;
097    int length2 = -2; // They must equal in the end
098
099    if (val1 == null) {
100      length1 = 0;
101    }
102
103    if (val2 == null) {
104      length2 = 0;
105    }
106
107    if (val1 instanceof long[]) {
108      length1 = ((long[]) val1).length;
109    }
110
111    if (val2 instanceof long[]) {
112      length2 = ((long[]) val2).length;
113    }
114
115    if (val1 instanceof Object[]) {
116      length1 = ((Object[]) val1).length;
117    }
118
119    assert val2 == null || val2 instanceof long[];
120
121    if (length1 != length2) {
122      // This derived variable is no longer interesting
123      return new ValueAndModified(null, ValueTuple.MISSING_NONSENSICAL);
124    }
125
126    assert length1 == length2;
127
128    int mod = ValueTuple.UNMODIFIED;
129    int mod1 = var1().getModified(full_vt);
130    int mod2 = var2().getModified(full_vt);
131    if (mod1 == ValueTuple.MODIFIED) mod = ValueTuple.MODIFIED;
132    if (mod2 == ValueTuple.MODIFIED) mod = ValueTuple.MODIFIED;
133    if (mod1 == ValueTuple.MISSING_NONSENSICAL) mod = ValueTuple.MISSING_NONSENSICAL;
134    if (mod2 == ValueTuple.MISSING_NONSENSICAL) mod = ValueTuple.MISSING_NONSENSICAL;
135    /*
136     * v1\v2  Unm  Mod  Mis
137     *
138     * Unm    Unm  Mod  Mis
139     * Mod    Mod  Mod  Mis
140     * Mis    Mis  Mis  Mis
141     */
142
143    long[] predicate = (long[]) val2;
144    int count = 0;
145    // Find length of output first
146    for (int i = 0; i < predicate.length; i++) {
147      if ((predicate[i] == choose) ^ !keep) count += 1;
148    }
149
150    if (val1 instanceof long[]) {
151      long[] result = new long[count];
152      long[] values = (long[]) val1;
153      int j = 0;
154      for (int i = 0; i < length1; i++) {
155        if ((predicate[i] == choose) ^ !keep) {
156          result[j] = values[i];
157          j++;
158        }
159      }
160      return new ValueAndModified(Intern.intern(result), mod);
161    } else if (val1 instanceof Object[]) {
162      @Interned Object[] result = new @Interned Object[count];
163      @Interned Object[] values = (@Interned Object[]) val1;
164      int j = 0;
165      for (int i = 0; i < length1; i++) {
166        if ((predicate[i] == choose) ^ !keep) {
167          result[j] = values[i];
168          j++;
169        }
170      }
171      return new ValueAndModified(Intern.intern(result), mod);
172    } else if (val1 == null) {
173      return new ValueAndModified(null, mod);
174    } else {
175      throw new RuntimeException("Invalid input arrays");
176    }
177  }
178
179  @Override
180  protected VarInfo makeVarInfo() {
181    return VarInfo.make_function("predicateSlice", var1(), var2());
182  }
183
184  @SideEffectFree
185  @Override
186  public String toString(@GuardSatisfied SequencesPredicate this) {
187    return "[SequencesPredicate of "
188        + var1().name()
189        + " "
190        + var2().name()
191        + " for "
192        + name
193        + "]";
194  }
195
196  @Pure
197  @Override
198  public boolean isSameFormula(Derivation other) {
199    // For Toh (tohn) to do.
200    if (other instanceof SequencesPredicate) {
201      SequencesPredicate o = (SequencesPredicate) other;
202      return o.var1().equals(var1()) && o.var2().equals(var2()) && choose == o.choose;
203    }
204    return false;
205  }
206
207  /** Returns the ESC name. */
208  @SideEffectFree
209  @Override
210  public String esc_name(String index) {
211    return String.format("predicate(%s,%s)", var1().esc_name(), var2().esc_name());
212  }
213}