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}