001package daikon;
002
003import java.io.Serializable;
004import java.util.Arrays;
005import java.util.BitSet;
006import org.checkerframework.checker.initialization.qual.UnknownInitialization;
007import org.checkerframework.checker.nullness.qual.NonNull;
008import org.checkerframework.checker.nullness.qual.Nullable;
009import org.checkerframework.checker.signedness.qual.Signed;
010
011// "ModBitTracker" is a poor name for this class, since it tracks
012// whether a value is missing, not whether it is modified.
013/**
014 * ModBitTracker maintains a BitSet for each variable at a program point. The BitSet indicates, for
015 * each sample seen in order, whether that variable was present or not.
016 */
017public class ModBitTracker implements Serializable, Cloneable {
018  static final long serialVersionUID = 20031014L;
019
020  // Should make this a configuration option.
021  private static boolean debug = false;
022
023  /** The maximum number of BitSets; the size of modbits_arrays. */
024  private int num_vars;
025
026  /** The size of each BitSet in modbits_arrays. */
027  private int num_samples;
028
029  /** The BitSets themselves. */
030  // In the future, I could imagine trying to optimize this with (say)
031  // run-length encoding; but it's probably not worth it.
032  // All elements of modbits_arrays at or past num_sets are null.
033  private @Nullable BitSet[] modbits_arrays;
034
035  /**
036   * Conceptually, there is a BitSet per variable. In actuality, when two different variables have
037   * the same modbits, they can share a single BitSet; we say the variables are in an equivalence
038   * set. "index" indicates, for each variable, which BitSet it should use; it is the identifier of
039   * the variable's equivalence set.
040   */
041  private int[] index;
042
043  /**
044   * The number of BitSets (equivalence sets) in use. All elements of modbits_arrays before this
045   * index are non-null, and all elements at or past this index are null.
046   */
047  private int num_sets;
048
049  // Member variables to avoid re-allocating every time "add" is entered.
050  /** The bits for this ValueTuple (indexed by equivalence set. */
051  private boolean[] this_bits;
052
053  /** True if the corresponding element of this_bits has a valid value. */
054  private boolean[] this_bits_valid;
055
056  /**
057   * The equivalence set for when an equivalence set is split: if a variable has a conflicting bit,
058   * then it goes to the specified index instead.
059   */
060  private int[] this_bits_exception_index;
061
062  /**
063   * Creates a ModBitTracker.
064   *
065   * @param num_vars number of variables to allocate space for
066   */
067  public ModBitTracker(int num_vars) {
068    assert num_vars >= 0;
069    this.num_vars = num_vars;
070    modbits_arrays = new @Nullable BitSet[num_vars];
071    if (num_vars > 0) {
072      modbits_arrays[0] = new BitSet();
073      num_sets = 1;
074    } else {
075      num_sets = 0;
076    }
077    num_samples = 0;
078    index = new int[num_vars];
079    this_bits = new boolean[num_vars];
080    this_bits_valid = new boolean[num_vars];
081    this_bits_exception_index = new int[num_vars];
082    if (debug) {
083      checkRep();
084    }
085  }
086
087  public int num_vars() {
088    return num_vars;
089  }
090
091  public int num_samples() {
092    return num_samples;
093  }
094
095  /** Accessor for testing only. */
096  public int num_sets() {
097    return num_sets;
098  }
099
100  /** Check the representation invariant. */
101  public void checkRep(@UnknownInitialization(ModBitTracker.class) ModBitTracker this) {
102    assert index.length == num_vars;
103    assert modbits_arrays.length == num_vars;
104    for (int i = 0; i < num_vars; i++) {
105      int this_index = index[i];
106      assert this_index >= 0;
107      assert this_index < num_sets;
108      assert modbits_arrays[this_index] != null;
109    }
110    for (int i = 0; i < num_vars; i++) {
111      if (i < num_sets) {
112        assert modbits_arrays[i] != null;
113        // Can't make this assertion, as there is no method that tells
114        // the highest index that has been used in the BitSet.  (size()
115        // gives physical size.)
116        // assert modbits_arrays[i].size() == num_samples
117        //                   : "modbits_arrays.[" + i + "].size() == "
118        //                   + modbits_arrays[i].size()
119        //                   + ", num_samples == " + num_samples;
120      } else {
121        assert modbits_arrays[i] == null;
122      }
123    }
124  }
125
126  /**
127   * Returns a BitSet of modbit values for the given variable. The caller must not modify the
128   * returned value!
129   */
130  @SuppressWarnings(
131      "nullness") // application invariant: index[varindex] is an index for a non-null BitSet in
132  // modbits_arrays
133  public BitSet get(int varindex) {
134    return modbits_arrays[index[varindex]];
135  }
136
137  /** Returns the modbit for the given variable and sample number. */
138  public boolean get(int varindex, int sampleno) {
139    return get(varindex).get(sampleno);
140  }
141
142  /**
143   * Split the specified equivalence set into two pieces. Returns the index of the copy.
144   *
145   * @param split_index where to split modbits_arrays
146   * @return the index of the copy
147   */
148  private int split(int split_index) {
149    @SuppressWarnings("nullness") // application invariant: split_index is in range
150    @NonNull BitSet bs = (BitSet) modbits_arrays[split_index].clone();
151    modbits_arrays[num_sets] = bs;
152    num_sets++;
153    return num_sets - 1;
154  }
155
156  /** Add to this the modbits for the given ValueTuple. */
157  public void add(ValueTuple vt, int count) {
158    if (debug) {
159      checkRep();
160    }
161    assert vt.size() == num_vars : "vt.size()=" + vt.size() + ", num_vars = " + num_vars;
162    if (num_vars == 0) {
163      num_samples += count;
164      return;
165    }
166    Arrays.fill(this_bits_valid, false);
167    Arrays.fill(this_bits_exception_index, (@Signed int) -1);
168    for (int i = 0; i < num_vars; i++) {
169      int this_index = index[i];
170      // Should this use the whole modbit, not just a boolean?
171      boolean modbit = !vt.isMissing(i);
172      if (!this_bits_valid[this_index]) {
173        // This is the first variable belonging to this equivalence set
174        // that we have seen so far.
175        this_bits[this_index] = modbit;
176        this_bits_valid[this_index] = true;
177        assert this_bits_exception_index[this_index] == -1;
178      } else {
179        // We have seen some other variable belonging to this equivalence set.
180        if (this_bits[this_index] == modbit) {
181          // This bit has the same value as we saw previously for its
182          // equivalence set.
183        } else {
184          // This bit has a different value than we have previously seen
185          // for its equivalence set.
186          if (this_bits_exception_index[this_index] == -1) {
187            // We have't previously seen an exception.
188            this_bits_exception_index[this_index] = split(this_index);
189          }
190          index[i] = this_bits_exception_index[this_index];
191          this_index = index[i];
192          this_bits[this_index] = modbit;
193          this_bits_valid[this_index] = true;
194        }
195      }
196    }
197    for (int i = 0; i < num_sets; i++) {
198      @SuppressWarnings("nullness") // application invariant: non-null up to index=num_sets
199      @NonNull BitSet bs = modbits_arrays[i];
200      bs.set(num_samples, num_samples + count, this_bits[i]);
201    }
202    num_samples += count;
203
204    if (debug) {
205      checkRep();
206    }
207  }
208}