001// ***** This file is automatically generated from BinaryInvariant.java.jpp
002
003package daikon.inv.binary.twoScalar;
004
005import daikon.*;
006import daikon.inv.*;
007import daikon.inv.InvariantStatus;
008import daikon.inv.binary.*;
009import org.checkerframework.checker.interning.qual.Interned;
010import org.checkerframework.checker.lock.qual.GuardSatisfied;
011import org.checkerframework.dataflow.qual.Pure;
012import org.plumelib.util.ArraysPlume;
013import org.plumelib.util.Intern;
014import typequals.prototype.qual.NonPrototype;
015import typequals.prototype.qual.Prototype;
016
017/**
018 * Base class for invariants over two variables of type double.
019 * An example is {@code y = abs(x)}.
020 *
021 * <p>Provides a simpler mechanism for non-symmetric invariants to function over both permutations
022 * of their variables.
023 *
024 * <p>Non-symmetric invariants must instantiate two objects (one for each argument order). This is
025 * tracked by the variable swap. They must always access their variables via the methods var1() and
026 * var2() which return the correct variable (based on the swap setting). No other work is necessary,
027 * all permuations and resurrection is handled here.
028 *
029 * <p>Symmetric invariants should define symmetric() to return true or override
030 * resurrect_done_swapped to do nothing. Non-symmetric invariants that use converse operations (eg,
031 * less than and greater than) rather than argument swapping should override resurrect_done_swapped
032 * to return the correct class.
033 */
034public abstract class TwoFloat extends BinaryInvariant {
035  static final long serialVersionUID = 20040113L;
036
037  // if true, swap the order of the invariant variables
038  protected boolean swap = false;
039
040  protected TwoFloat(PptSlice ppt) {
041    super(ppt);
042  }
043
044  protected @Prototype TwoFloat() {
045    super();
046  }
047
048  @Override
049  final public boolean valid_types(VarInfo[] vis) {
050
051    if (vis.length != 2) {
052      return false;
053    }
054
055      boolean dim_ok = !vis[0].file_rep_type.isArray() && !vis[1].file_rep_type.isArray();
056
057    return dim_ok && vis[0].file_rep_type.baseIsFloat() && vis[1].file_rep_type.baseIsFloat();
058  }
059
060  /** Returns whether or not the variable order is currently swapped for this invariant. */
061  @Override
062  public boolean get_swap() {
063    return swap;
064  }
065
066  /** Checks to see if the variable order was swapped and calls the correct routine to handle it. */
067  @Override
068  protected Invariant resurrect_done(int[] permutation) {
069    assert permutation.length == 2;
070    // assert ArraysPlume.fnIsPermutation(permutation);
071    if (permutation[0] == 1) {
072      return resurrect_done_swapped();
073    } else {
074      return resurrect_done_unswapped();
075    }
076  }
077
078  /** Swaps the variables by inverting the state of swap. */
079  protected Invariant resurrect_done_swapped() {
080    if (!is_symmetric()) {
081      swap = !swap;
082    }
083    return this;
084  }
085
086   /** Subclasses can override in the rare cases they need to fix things even when not swapped. */
087  protected Invariant resurrect_done_unswapped() {
088    // do nothing
089    return this;
090  }
091
092  /**
093   * Returns the first variable. This is the only mechanism by which subclasses should access
094   * variables.
095   */
096  public VarInfo var1(@GuardSatisfied TwoFloat this) {
097    if (swap) {
098      return ppt.var_infos[1];
099    } else {
100      return ppt.var_infos[0];
101    }
102  }
103
104  /**
105   * Returns the first variable. This is the only mechanism by which subclasses should access
106   * variables.
107   */
108  public VarInfo var2(@GuardSatisfied TwoFloat this) {
109    if (swap) {
110      return ppt.var_infos[0];
111    } else {
112      return ppt.var_infos[1];
113    }
114  }
115
116  /**
117   * Returns the first variable from the specified vis. This is the only mechanism by which
118   * subclasses should access variables.
119   */
120  public VarInfo var1(VarInfo[] vis) {
121    if (swap) {
122      return vis[1];
123    } else {
124      return vis[0];
125    }
126  }
127
128  /**
129   * Returns the first variable in the specified vis. This is the only mechanism by which subclasses
130   * should access variables.
131   */
132  public VarInfo var2(VarInfo[] vis) {
133    if (swap) {
134      return vis[0];
135    } else {
136      return vis[1];
137    }
138  }
139
140  @Override
141  public InvariantStatus check(
142      @Interned Object val1, @Interned Object val2, int mod_index, int count) {
143    // Tests for whether a value is missing should be performed before
144    // making this call, so as to reduce overall work.
145    assert ! falsified;
146    assert (mod_index >= 0) && (mod_index < 4);
147    double v1 = ((Double) val1).doubleValue();
148    double v2 = ((Double) val2).doubleValue();
149    if (mod_index == 0) {
150      if (swap) {
151        return check_unmodified(v2, v1, count);
152      } else {
153        return check_unmodified(v1, v2, count);
154      }
155    } else {
156      if (swap) {
157        return check_modified(v2, v1, count);
158      } else {
159        return check_modified(v1, v2, count);
160      }
161    }
162  }
163
164  @Override
165  public InvariantStatus add(
166      @Interned Object val1, @Interned Object val2, int mod_index, int count) {
167    // Tests for whether a value is missing should be performed before
168    // making this call, so as to reduce overall work.
169    assert ! falsified;
170    assert (mod_index >= 0) && (mod_index < 4);
171    double v1 = ((Double) val1).doubleValue();
172    double v2 = ((Double) val2).doubleValue();
173    if (mod_index == 0) {
174      if (swap) {
175        return add_unmodified(v2, v1, count);
176      } else {
177        return add_unmodified(v1, v2, count);
178      }
179    } else {
180      if (swap) {
181        return add_modified(v2, v1, count);
182      } else {
183        return add_modified(v1, v2, count);
184      }
185    }
186  }
187
188  /**
189   * Presents a sample to the invariant. Returns whether the sample is consistent with the
190   * invariant. Does not change the state of the invariant.
191   *
192   * @param count how many identical samples were observed in a row. For example, three calls to
193   *     check_modified with a count parameter of 1 is equivalent to one call to check_modified with
194   *     a count parameter of 3.
195   * @return whether or not the sample is consistent with the invariant
196   */
197  public abstract InvariantStatus check_modified(double v1, double v2, int count);
198
199  public InvariantStatus check_unmodified(double v1, double v2, int count) {
200    return InvariantStatus.NO_CHANGE;
201  }
202
203  /** Default implementation simply calls check. Subclasses can override. */
204  public InvariantStatus add_modified(double v1, double v2, int count) {
205    return check_modified(v1, v2, count);
206  }
207
208  /** By default, do nothing if the value hasn't been seen yet. Subclasses can override this. */
209  public InvariantStatus add_unmodified(double v1, double v2, int count) {
210    return InvariantStatus.NO_CHANGE;
211  }
212
213  /** Returns a representation of the class. This includes the classname, variables, and swap state. */
214  @Override
215  public String repr(@GuardSatisfied TwoFloat this) {
216    return getClass().getName() + " (" + var1().name() + ", "
217      + var2().name() + ") [swap=" + swap + "]";
218  }
219
220  /**
221   * Return true if both invariants are the same class and the order of the variables (swap) is the
222   * same.
223   */
224  @Pure
225  @Override
226  public boolean isSameFormula(Invariant other) {
227    TwoFloat inv = (TwoFloat) other;
228    return (this.getClass() == inv.getClass()) && (this.swap == inv.swap);
229  }
230
231  @Override
232  protected double computeConfidence() {
233    return Invariant.conf_is_ge(ppt.num_values(), 5);
234  }
235}