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}