001package daikon.inv;
002
003import daikon.PptSlice;
004import daikon.PptSlice1;
005import daikon.PptSlice2;
006import daikon.PptSlice3;
007import daikon.PptTopLevel;
008import daikon.VarInfo;
009import java.util.HashSet;
010import java.util.Iterator;
011import java.util.List;
012import org.checkerframework.checker.lock.qual.GuardSatisfied;
013import org.checkerframework.checker.nullness.qual.Nullable;
014import org.checkerframework.dataflow.qual.SideEffectFree;
015import typequals.prototype.qual.NonPrototype;
016import typequals.prototype.qual.Prototype;
017
018/**
019 * This is a special invariant used internally by Daikon to represent invariants whose meaning
020 * Daikon doesn't understand. The only operation that can be performed on a DummyInvariant is to
021 * print it. In particular, the invariant cannot be tested against a sample: the invariant is always
022 * assumed to hold and is always considered to be statistically justified.
023 *
024 * <p>The main use for a dummy invariant is to represent a splitting condition that appears in a
025 * {@code .spinfo} file. The {@code .spinfo} file can indicate an arbitrary Java expression, which
026 * might not be equivalent to any invariant in Daikon's grammar.
027 *
028 * <p>Ordinarily, Daikon uses splitting conditions to split data, then seeks to use that split data
029 * to form conditional invariants out of its standard built-in invariants. If you wish the
030 * expression in the .spinfo file to be printed as an invariant, whether or not it is itself
031 * discovered by Daikon during invariant detection, then the configuration option {@code
032 * daikon.split.PptSplitter.dummy_invariant_level} must be set, and formatting information must be
033 * supplied in the splitter info file.
034 */
035public class DummyInvariant extends Invariant {
036  static final long serialVersionUID = 20030220L;
037
038  private @Nullable String daikonFormat;
039  private @Nullable String javaFormat;
040  private @Nullable String escFormat;
041  private @Nullable String simplifyFormat;
042  private @Nullable String jmlFormat;
043  private @Nullable String dbcFormat;
044  private @Nullable String csharpFormat;
045
046  private boolean negated = false;
047
048  // Pre-instatiate(), set to true if we have reason to believe the user
049  // explicitly wanted this invariant to appear in the output.
050  // [What evidence is required, and when does the evidence show the user
051  // didn't want it?  Does the fact that this is a DummyInvariant indicate
052  // the user explicitly cares?]
053  // After instantiation, also requires that we've found an appropriate
054  // slice for the invariant to live in.
055  public boolean valid = false;
056
057  public DummyInvariant(
058      PptSlice ppt,
059      @Nullable String daikonStr,
060      @Nullable String java,
061      @Nullable String esc,
062      @Nullable String simplify,
063      @Nullable String jml,
064      @Nullable String dbc,
065      @Nullable String csharp,
066      boolean valid) {
067    super(ppt);
068    daikonFormat = daikonStr;
069    javaFormat = java;
070    escFormat = esc;
071    simplifyFormat = simplify;
072    jmlFormat = jml;
073    dbcFormat = dbc;
074    csharpFormat = csharp;
075    this.valid = valid;
076  }
077
078  public @Prototype DummyInvariant(
079      @Nullable String daikonStr,
080      @Nullable String java,
081      @Nullable String esc,
082      @Nullable String simplify,
083      @Nullable String jml,
084      @Nullable String dbc,
085      @Nullable String csharp,
086      boolean valid) {
087    super();
088    daikonFormat = daikonStr;
089    javaFormat = java;
090    escFormat = esc;
091    simplifyFormat = simplify;
092    jmlFormat = jml;
093    dbcFormat = dbc;
094    csharpFormat = csharp;
095    this.valid = valid;
096  }
097
098  public DummyInvariant instantiate(PptTopLevel parent, VarInfo[] vars) {
099    assert !this.negated : "Only instantiated invariants should be negated";
100    DummyInvariant inv =
101        new DummyInvariant(
102            ppt,
103            daikonFormat,
104            javaFormat,
105            escFormat,
106            simplifyFormat,
107            jmlFormat,
108            dbcFormat,
109            csharpFormat,
110            // Not valid until we find a slice for it
111            /* valid= */ false);
112
113    // Find between 1 and 3 unique variables, to pick a slice to put
114    // this in.
115    HashSet<VarInfo> uniqVarsSet = new HashSet<>();
116    for (int i = 0; i < vars.length; i++) {
117      uniqVarsSet.add(vars[i].canonicalRep());
118    }
119    int sliceSize = uniqVarsSet.size();
120    if (sliceSize > 3) {
121      sliceSize = 3;
122    }
123    /*NNC:@MonotonicNonNull*/ VarInfo[] newVars = new VarInfo[sliceSize];
124    {
125      Iterator<VarInfo> it = uniqVarsSet.iterator();
126      int i = 0;
127      while (it.hasNext()) {
128        newVars[i++] = it.next();
129        if (i == sliceSize) {
130          break;
131        }
132      }
133    }
134    vars = newVars;
135    assert vars.length >= 1 && vars.length <= 3;
136    if (vars.length == 1) {
137      PptSlice1 slice = parent.findSlice(vars[0]);
138      if (slice == null) {
139        slice = new PptSlice1(parent, vars);
140        parent.addSlice(slice);
141      }
142      inv.ppt = slice;
143    } else if (vars.length == 2) {
144      if (vars[0] == vars[1]) {
145        return inv;
146      } else if (vars[0].varinfo_index > vars[1].varinfo_index) {
147        VarInfo tmp = vars[0];
148        vars[0] = vars[1];
149        vars[1] = tmp;
150      }
151      PptSlice2 slice = parent.findSlice(vars[0], vars[1]);
152      if (slice == null) {
153        slice = new PptSlice2(parent, vars);
154        parent.addSlice(slice);
155      }
156      inv.ppt = slice;
157    } else if (vars.length == 3) {
158      if (vars[0] == vars[1] || vars[1] == vars[2] || vars[0] == vars[2]) {
159        return inv;
160      }
161      // bubble sort
162      VarInfo tmp;
163      if (vars[0].varinfo_index > vars[1].varinfo_index) {
164        tmp = vars[0];
165        vars[0] = vars[1];
166        vars[1] = tmp;
167      }
168      if (vars[1].varinfo_index > vars[2].varinfo_index) {
169        tmp = vars[1];
170        vars[1] = vars[2];
171        vars[2] = tmp;
172      }
173      if (vars[0].varinfo_index > vars[1].varinfo_index) {
174        tmp = vars[0];
175        vars[0] = vars[1];
176        vars[1] = tmp;
177      }
178      PptSlice3 slice = parent.findSlice(vars[0], vars[1], vars[2]);
179      if (slice == null) {
180        slice = new PptSlice3(parent, vars);
181        parent.addSlice(slice);
182      }
183      inv.ppt = slice;
184    }
185    // We found a slice, so set the DummyInvariant to valid.
186    inv.valid = true;
187    return inv;
188  }
189
190  @Override
191  protected double computeConfidence() {
192    return Invariant.CONFIDENCE_JUSTIFIED;
193  }
194
195  public void negate() {
196    negated = !negated;
197  }
198
199  @SideEffectFree
200  @Override
201  public String format_using(@GuardSatisfied DummyInvariant this, OutputFormat format) {
202    if (format == OutputFormat.DAIKON) {
203      return format_daikon();
204    }
205    if (format == OutputFormat.JAVA) {
206      return format_java();
207    }
208    if (format == OutputFormat.ESCJAVA) {
209      return format_esc();
210    }
211    if (format == OutputFormat.SIMPLIFY) {
212      return format_simplify();
213    }
214    if (format == OutputFormat.JML) {
215      return format_jml();
216    }
217    if (format == OutputFormat.DBCJAVA) {
218      return format_dbc();
219    }
220    if (format == OutputFormat.CSHARPCONTRACT) {
221      return format_csharp();
222    }
223
224    return format_unimplemented(format);
225  }
226
227  public String format_daikon(@GuardSatisfied DummyInvariant this) {
228    String df;
229    if (daikonFormat == null) {
230      df = "<dummy>";
231    } else {
232      df = daikonFormat;
233    }
234    if (negated) {
235      return "not(" + df + ")";
236    } else {
237      return df;
238    }
239  }
240
241  public String format_java(@GuardSatisfied DummyInvariant this) {
242    if (javaFormat == null) {
243      return "format_java not implemented for dummy invariant";
244    }
245    if (negated) {
246      return "!(" + javaFormat + ")";
247    } else {
248      return javaFormat;
249    }
250  }
251
252  public String format_esc(@GuardSatisfied DummyInvariant this) {
253    if (escFormat == null) {
254      return "format_esc not implemented for dummy invariant";
255    }
256    if (negated) {
257      return "!(" + escFormat + ")";
258    } else {
259      return escFormat;
260    }
261  }
262
263  public String format_simplify(@GuardSatisfied DummyInvariant this) {
264    if (simplifyFormat == null) {
265      return "format_simplify not implemented for dummy invariant";
266    }
267    if (negated) {
268      return "(NOT " + simplifyFormat + ")";
269    } else {
270      return simplifyFormat;
271    }
272  }
273
274  public String format_jml(@GuardSatisfied DummyInvariant this) {
275    if (jmlFormat == null) {
276      return "format_jml not implemented for dummy invariant";
277    }
278    if (negated) {
279      return "!(" + jmlFormat + ")";
280    } else {
281      return jmlFormat;
282    }
283  }
284
285  public String format_dbc(@GuardSatisfied DummyInvariant this) {
286    if (dbcFormat == null) {
287      return "format_dbc not implemented for dummy invariant";
288    }
289    if (negated) {
290      return "!(" + dbcFormat + ")";
291    } else {
292      return dbcFormat;
293    }
294  }
295
296  public String format_csharp(@GuardSatisfied DummyInvariant this) {
297    if (csharpFormat == null) {
298      return "format_csharp not implemented for dummy invariant";
299    }
300    if (negated) {
301      return "!(" + csharpFormat + ")";
302    } else {
303      return csharpFormat;
304    }
305  }
306
307  @Override
308  protected Invariant resurrect_done(int[] permutation) {
309    throw new Error("Not implemented");
310  }
311
312  @Override
313  public boolean isSameFormula(Invariant other) {
314    throw new Error("Not implemented");
315  }
316
317  @Override
318  public boolean enabled(@Prototype DummyInvariant this) {
319    throw new Error("do not invoke " + getClass() + ".enabled()");
320  }
321
322  @Override
323  public boolean valid_types(@Prototype DummyInvariant this, VarInfo[] vis) {
324    throw new Error("do not invoke " + getClass() + ".valid_types()");
325  }
326
327  @Override
328  protected @NonPrototype DummyInvariant instantiate_dyn(
329      @Prototype DummyInvariant this, PptSlice slice) {
330    throw new Error("do not invoke " + getClass() + ".instantiate_dyn()");
331  }
332
333  @Override
334  public @Nullable @NonPrototype DummyInvariant merge(
335      @Prototype DummyInvariant this, List<@NonPrototype Invariant> invs, PptSlice parent_ppt) {
336    throw new Error("Don't merge DummyInvariant invariants");
337  }
338}