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}