001package daikon.diff; 002 003import daikon.PptTopLevel; 004import daikon.inv.Invariant; 005import java.util.logging.Level; 006import java.util.logging.Logger; 007import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf; 008import org.checkerframework.checker.nullness.qual.MonotonicNonNull; 009import org.checkerframework.checker.nullness.qual.NonNull; 010import org.checkerframework.checker.nullness.qual.Nullable; 011import org.checkerframework.checker.nullness.qual.RequiresNonNull; 012 013/** Computes A xor B, where A and B are the two sets of invariants. */ 014public class XorVisitor extends DepthFirstVisitor { 015 016 private InvMap result = new InvMap(); 017 private @MonotonicNonNull PptTopLevel currentPpt; 018 019 public static final Logger debug = Logger.getLogger("daikon.diff.XorVisitor"); 020 021 /** Every node has at least one non-null ppt. Add one of the non-null ppt to the result. */ 022 @Override 023 public void visit(PptNode node) { 024 PptTopLevel ppt1 = node.getPpt1(); 025 PptTopLevel ppt2 = node.getPpt2(); 026 @SuppressWarnings( 027 "nullness") // application invariant: at least one of ppt1 and ppt2 is non-null 028 @NonNull PptTopLevel pptNonNull = (ppt1 != null ? ppt1 : ppt2); 029 result.addPpt(pptNonNull); 030 currentPpt = pptNonNull; 031 super.visit(node); 032 } 033 034 /** 035 * If one invariant is null and the other is not, add the non-null invariant to the result set. 036 */ 037 @Override 038 @SuppressWarnings( 039 "nullness:contracts.precondition.override") // visitor invariant, because the PptNode 040 // has already been visited 041 @RequiresNonNull("currentPpt") 042 // visitor invariant 043 public void visit(InvNode node) { 044 Invariant inv1 = node.getInv1(); 045 Invariant inv2 = node.getInv2(); 046 if (debug.isLoggable(Level.FINE)) { 047 debug.fine( 048 "visit: " 049 + ((inv1 != null) ? inv1.ppt.parent.name() : "NULL") 050 + " " 051 + ((inv1 != null) ? inv1.repr() : "NULL") 052 + " - " 053 + ((inv2 != null) ? inv2.repr() : "NULL")); 054 } 055 if (shouldAddInv1(inv1, inv2)) { 056 assert inv1 != null; 057 result.add(currentPpt, inv1); 058 } else if (shouldAddInv2(inv1, inv2)) { 059 assert inv2 != null; 060 result.add(currentPpt, inv2); 061 } 062 } 063 064 @EnsuresNonNullIf(result = true, expression = "#1") 065 private static boolean shouldAddInv1(@Nullable Invariant inv1, @Nullable Invariant inv2) { 066 return (inv1 != null) && (inv2 == null); 067 } 068 069 @EnsuresNonNullIf(result = true, expression = "#2") 070 private static boolean shouldAddInv2(@Nullable Invariant inv1, @Nullable Invariant inv2) { 071 return (inv2 != null) && (inv1 == null); 072 } 073 074 /** Returns the InvMap generated as a result of the traversal. */ 075 public InvMap getResult() { 076 return result; 077 } 078}