001package daikon.diff; 002 003import daikon.PptTopLevel; 004import daikon.inv.Invariant; 005import org.checkerframework.checker.nullness.qual.MonotonicNonNull; 006import org.checkerframework.checker.nullness.qual.NonNull; 007import org.checkerframework.checker.nullness.qual.RequiresNonNull; 008 009/** Computes A union B, where A and B are the two sets of invariants. */ 010public class UnionVisitor extends DepthFirstVisitor { 011 012 private InvMap result = new InvMap(); 013 private @MonotonicNonNull PptTopLevel currentPpt; 014 015 public InvMap getResult() { 016 return result; 017 } 018 019 /** Every node has at least one non-null ppt. Add one of the non-null ppt to the result. */ 020 @Override 021 public void visit(PptNode node) { 022 PptTopLevel ppt1 = node.getPpt1(); 023 PptTopLevel ppt2 = node.getPpt2(); 024 @SuppressWarnings( 025 "nullness") // application invariant: at least one of ppt1 and ppt2 is non-null 026 @NonNull PptTopLevel pptNonNull = (ppt1 != null ? ppt1 : ppt2); 027 result.addPpt(pptNonNull); 028 currentPpt = pptNonNull; 029 super.visit(node); 030 } 031 032 /** 033 * If only one invariant is non-null, always add it. If two invariants are non-null, add the 034 * invariant with the better (higher) confidence. 035 */ 036 @Override 037 @SuppressWarnings( 038 "nullness:contracts.precondition.override" // visitor invariant, because the PptNode has 039 // already been visited 040 ) 041 @RequiresNonNull("currentPpt") 042 // visitor invariant 043 public void visit(InvNode node) { 044 Invariant inv1 = node.getInv1(); 045 Invariant inv2 = node.getInv2(); 046 if (inv1 == null) { 047 assert inv2 != null : "@AssumeAssertion(nullness): at least one of inv1 and inv2 is non-null"; 048 result.add(currentPpt, inv2); 049 } else if (inv2 == null) { 050 result.add(currentPpt, inv1); 051 } else { 052 if (inv1.getConfidence() >= inv2.getConfidence()) { 053 result.add(currentPpt, inv1); 054 } else { 055 result.add(currentPpt, inv2); 056 } 057 } 058 } 059}