001package daikon.diff; 002 003import daikon.PptConditional; 004import daikon.inv.Implication; 005import daikon.inv.Invariant; 006import java.util.ArrayList; 007import java.util.HashSet; 008import java.util.Iterator; 009import java.util.List; 010import org.checkerframework.checker.nullness.qual.Nullable; 011 012/** 013 * <B>ConsequentExtractorVisitor</B> is a visitor that takes in RootNode tree used by the other 014 * visitors in Diff and only modifies the first inv tree out of the pair of two inv trees (the 015 * second tree is never read or modified). 016 * 017 * <p>The goal is to take the right hand side of any implication and extract it for later use. The 018 * implementation completely replaces the previous inv tree with the a new inv tree. The new inv 019 * tree contains only the extracted consequents of the original inv tree. 020 */ 021public class ConsequentExtractorVisitor extends DepthFirstVisitor { 022 023 private int nonce; 024 025 // Gets rid of repeated reports 026 private HashSet<String> repeatFilter = new HashSet<>(); 027 028 // Accumulation of extracted consequents 029 private List<Invariant> accum = new ArrayList<>(); 030 031 public ConsequentExtractorVisitor() { 032 nonce = 0; 033 } 034 035 @Override 036 public void visit(PptNode node) { 037 assert node.getPpt1() != null 038 : "@AssumeAssertion(nullness): method precondition: has a (non-null) consequent"; 039 if (node.getPpt1() instanceof PptConditional) { 040 return; 041 } 042 System.out.println(node.getPpt1().name); 043 repeatFilter.clear(); 044 accum.clear(); 045 super.visit(node); 046 // clear all of the old ppts 047 048 for (Iterator<InvNode> i = node.children(); i.hasNext(); ) { 049 InvNode child = i.next(); 050 if (child.getInv1() != null) { 051 child.getInv1().ppt.invs.clear(); 052 } 053 } 054 /* 055 for (Invariant inv : accum) { 056 inv.ppt.invs.clear(); 057 } 058 */ 059 // Now add back everything in accum 060 for (Invariant inv : accum) { 061 inv.ppt.addInvariant(inv); 062 } 063 System.out.println("NONCE: " + nonce); 064 } 065 066 /** 067 * The idea is to check if the node is an Implication Invariant. If not, immediately remove the 068 * invariant. Otherwise, extract the Consequent, remove the Implication, and then add the 069 * consequent to the list. 070 */ 071 @Override 072 public void visit(InvNode node) { 073 Invariant inv1 = node.getInv1(); 074 // do nothing if the invariant does not exist 075 if (inv1 != null) { 076 if (inv1.justified() && (inv1 instanceof Implication)) { 077 nonce++; 078 Implication imp = (Implication) inv1; 079 if (repeatFilter.add(imp.consequent().format())) { 080 // inv1.ppt.invs.add (imp.consequent()); 081 accum.add(imp.consequent()); 082 } 083 // add both sides of a biimplication 084 if (imp.iff == true) { 085 if (repeatFilter.add(imp.predicate().format())) { 086 // inv1.ppt.invs.add (imp.predicate()); 087 accum.add(imp.predicate()); 088 } 089 } 090 } 091 inv1.ppt.removeInvariant(inv1); 092 System.out.println(inv1.ppt.invs.size() + " " + repeatFilter.size()); 093 } else { 094 095 } 096 } 097 098 /** 099 * Returns true if the pair of invariants should be printed, depending on their type, 100 * relationship, and printability. 101 */ 102 protected boolean shouldPrint(@Nullable Invariant inv1, @Nullable Invariant inv2) { 103 int rel = DetailedStatisticsVisitor.determineRelationship(inv1, inv2); 104 if (rel == DetailedStatisticsVisitor.REL_SAME_JUST1_JUST2 105 || rel == DetailedStatisticsVisitor.REL_SAME_UNJUST1_UNJUST2 106 || rel == DetailedStatisticsVisitor.REL_DIFF_UNJUST1_UNJUST2 107 || rel == DetailedStatisticsVisitor.REL_MISS_UNJUST1 108 || rel == DetailedStatisticsVisitor.REL_MISS_UNJUST2) { 109 return false; 110 } 111 112 if ((inv1 == null || !inv1.isWorthPrinting()) && (inv2 == null || !inv2.isWorthPrinting())) { 113 return false; 114 } 115 116 return true; 117 } 118}