001package daikon.split.misc;
002
003import daikon.Ppt;
004import daikon.ValueTuple;
005import daikon.VarInfo;
006import daikon.inv.DummyInvariant;
007import daikon.split.Splitter;
008import org.checkerframework.checker.initialization.qual.UnknownInitialization;
009import org.checkerframework.checker.lock.qual.GuardSatisfied;
010import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
011import org.checkerframework.checker.nullness.qual.Nullable;
012import org.checkerframework.checker.nullness.qual.RequiresNonNull;
013import org.checkerframework.dataflow.qual.SideEffectFree;
014import org.plumelib.util.ArraysPlume;
015
016/** This splitter tests the condition "$caller one of { some set of integers }". */
017public final class CallerContextSplitter extends Splitter {
018  static final long serialVersionUID = 20030112L;
019
020  /** Create a new splitter for the given ppt using this as a prototype. */
021  @SuppressWarnings("nullness:return") // why is "new ...Splitter" @UnderInitialization?
022  @Override
023  public Splitter instantiateSplitter(@UnknownInitialization(Ppt.class) Ppt ppt) {
024    return new CallerContextSplitter(ppt, ids, condition);
025  }
026
027  /** Name of the variable used by the front end to store caller (callsite) information. */
028  public final String CALLER_INDICATOR_NAME_STRING = "daikon_callsite_id";
029
030  private final @Nullable VarInfo caller_varinfo;
031  private final long[] ids;
032  private final String condition;
033
034  /** Create a new instantiated CallerContextSplitter. */
035  CallerContextSplitter(@UnknownInitialization(Ppt.class) Ppt ppt, long[] ids, String condition) {
036    caller_varinfo = ppt.find_var_by_name(CALLER_INDICATOR_NAME_STRING);
037    this.ids = ids;
038    this.condition = condition;
039    instantiated = true;
040  }
041
042  /** Create a prototype (factory) splitter for the given set of ids and condition. */
043  public CallerContextSplitter(long[] ids, String condition) {
044    this.caller_varinfo = null;
045    this.ids = ids.clone();
046    this.condition = condition;
047  }
048
049  @EnsuresNonNullIf(result = true, expression = "caller_varinfo")
050  @Override
051  public boolean valid() {
052    return (caller_varinfo != null);
053  }
054
055  @SuppressWarnings(
056      "nullness:contracts.precondition.override") // application invariant about private
057  // variable
058  @RequiresNonNull("caller_varinfo")
059  @Override
060  public boolean test(ValueTuple vt) {
061    long caller = caller_varinfo.getIntValue(vt);
062    return (ArraysPlume.indexOf(ids, caller) >= 0);
063  }
064
065  @Override
066  public String condition() {
067    return condition;
068  }
069
070  @SideEffectFree
071  @Override
072  public String toString(@GuardSatisfied CallerContextSplitter this) {
073    String attach = "(unattached prototype)";
074    if (caller_varinfo != null) {
075      attach = "attached to " + caller_varinfo.ppt.name();
076    }
077    return "CallerContextSplitter<" + condition + ", " + attach + ">";
078  }
079
080  @Override
081  public @Nullable DummyInvariant getDummyInvariant() {
082    return null;
083  }
084}