001package daikon.simplify;
002
003import static daikon.inv.Invariant.asInvClass;
004
005import daikon.PptSlice;
006import daikon.PptSlice0;
007import daikon.inv.GuardingImplication;
008import daikon.inv.Implication;
009import daikon.inv.Invariant;
010import daikon.inv.OutputFormat;
011import org.checkerframework.checker.lock.qual.GuardSatisfied;
012
013/**
014 * InvariantLemmas are Lemmas created by printing a Daikon invariant in Simplify format, sometimes
015 * with some hacks.
016 */
017public class InvariantLemma extends Lemma {
018  public String from; // A note explaining our derivation
019  public Invariant invariant; // A pointer back to the invariant we
020
021  // were made from
022
023  public InvariantLemma(Invariant inv) {
024    super(inv.format(), inv.format_using(OutputFormat.SIMPLIFY));
025    from = inv.ppt.parent.name;
026    invariant = inv;
027  }
028
029  @Override
030  public String summarize(@GuardSatisfied InvariantLemma this) {
031    return summary + " from " + from;
032  }
033
034  /** If this lemma came from an invariant, get its class. */
035  @Override
036  public Class<? extends Invariant> invClass() {
037    Class<? extends Invariant> c;
038    if (invariant instanceof GuardingImplication) {
039      c = ((Implication) invariant).consequent().getClass();
040    } else {
041      c = invariant.getClass();
042    }
043
044    Class<?> outer = c.getDeclaringClass();
045    if (outer != null) {
046      c = asInvClass(outer);
047    }
048    return c;
049  }
050
051  /**
052   * Make a lemma corresponding to the given invariant, except referring to the prestate versions of
053   * all the variables that inv referred to.
054   */
055  // The argument is an invariant at the entry point, where no orig(...) variables exist.
056  public static InvariantLemma makeLemmaAddOrig(Invariant inv) {
057    // XXX Side-effecting the invariant to change its ppt (and then
058    // to change it back afterward) isn't such a hot thing to do, but
059    // it isn't that hard, and seems to work so long as the new ppt is valid.
060    InvariantLemma result;
061    if (inv instanceof Implication) {
062      Implication imp = (Implication) inv;
063      PptSlice lhs_saved = imp.predicate().ppt;
064      PptSlice rhs_saved = imp.consequent().ppt;
065      imp.predicate().ppt = PptSlice0.makeFakePrestate(lhs_saved);
066      imp.consequent().ppt = PptSlice0.makeFakePrestate(rhs_saved);
067      result = new InvariantLemma(imp);
068      imp.predicate().ppt = lhs_saved;
069      imp.consequent().ppt = rhs_saved;
070    } else {
071      PptSlice saved = inv.ppt;
072      PptSlice orig = PptSlice0.makeFakePrestate(saved);
073      inv.ppt = orig;
074      result = new InvariantLemma(inv);
075      inv.ppt = saved;
076    }
077    result.from += " (orig() added)";
078    return result;
079  }
080}