From: bdemsky <bdemsky>
Date: Fri, 6 Feb 2004 22:33:01 +0000 (+0000)
Subject: Checking in code to perform safety checks on repair dependency graph.
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=6e6caa157ea20e565ea92786ef266c952e6f39b3;p=repair.git

Checking in code to perform safety checks on repair dependency graph.
---

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
index 4217361..5b24327 100755
--- a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
@@ -1,6 +1,55 @@
 package MCC.IR;
 
 class AbstractInterferes {
+    static public boolean interferes(AbstractRepair ar, Rule r, boolean satisfy) {
+	boolean mayadd=false;
+	boolean mayremove=false;
+	switch (ar.getType()) {
+	case AbstractRepair.ADDTOSET:
+	case AbstractRepair.ADDTORELATION:
+	    if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
+		return true;
+	    mayadd=true;
+	    break;
+	case AbstractRepair.REMOVEFROMSET:
+	case AbstractRepair.REMOVEFROMRELATION:
+	    if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
+		return true;
+	    mayremove=true;
+	    break;
+	case AbstractRepair.MODIFYRELATION:
+	    if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
+		return true;
+	    if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
+		return true;
+	    mayadd=true;
+	    mayremove=true;
+	break;
+	default:
+	    throw new Error("Unrecognized Abstract Repair");
+	}
+	DNFRule drule=null;
+	if (satisfy)
+	    drule=r.getDNFGuardExpr();
+	else
+	    drule=r.getDNFNegGuardExpr();
+	
+	for(int i=0;i<drule.size();i++) {
+	    RuleConjunction rconj=drule.get(i);
+	    for(int j=0;j<rconj.size();j++) {
+		DNFExpr dexpr=rconj.get(j);
+		Expr expr=dexpr.getExpr();
+		if (expr.usesDescriptor(ar.getDescriptor())) {
+		    /* Need to check */
+		    if ((mayadd&&!dexpr.getNegation())||(mayremove&&dexpr.getNegation()))
+			return true;
+		}
+	    }
+	}
+	return false;
+    }
+
+
     static public boolean interferes(AbstractRepair ar, DNFPredicate dp) {
 	if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
 	    ((ar.getDescriptor() instanceof SetDescriptor)||
diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
index c4855bc..c711d82 100755
--- a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
@@ -3,6 +3,8 @@ import java.util.*;
 
 class ConcreteInterferes {
     static public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
+	if (!initialinterferes(mun,r,satisfy)) /* Can't falsify a rule adding something to a set on an initial addition*/
+	    return false;
 	for(int i=0;i<mun.numUpdates();i++) {
 	    UpdateNode un=mun.getUpdate(i);
 	    for (int j=0;j<un.numUpdates();j++) {
@@ -12,15 +14,35 @@ class ConcreteInterferes {
 		if (satisfy)
 		    drule=r.getDNFNegGuardExpr();
 
+
 		if (!update.isAbstract()) {
 		    Descriptor updated_des=update.getDescriptor();
 		    assert updated_des!=null;
+		    /* Update is local to this rule, and the effect is intentional */
+		    /* If we're adding something, a side effect could be to falsify some other binding
+		       If we're removing something, there is no similar side effect */
+		    if ((un.getRule()==r)&&
+			(((mun.op==MultUpdateNode.ADD)&&satisfy)||(mun.op==MultUpdateNode.REMOVE))&&
+			(r.numQuantifiers()==1)&&
+			(r.getQuantifier(0) instanceof SetQuantifier)&&
+			update.isField()&&
+			(((DotExpr)update.getLeftExpr()).getExpr() instanceof VarExpr)&&
+			((SetQuantifier)r.getQuantifier(0)).getVar()==((VarExpr)((DotExpr)update.getLeftExpr()).getExpr()).getVar())
+			continue;
+    		    if ((un.getRule()==r)&&
+			(((mun.op==MultUpdateNode.ADD)&&satisfy)||(mun.op==MultUpdateNode.REMOVE))&&
+			(r.numQuantifiers()==0))
+			continue;
+
+
 		    if (r.getInclusion().usesDescriptor(updated_des))
 			return true; /* Interferes with inclusion condition */
 		    
 		    for(int k=0;k<drule.size();k++) {
 			RuleConjunction rconj=drule.get(k);
 			for(int l=0;l<rconj.size();l++) {
+
+
 			    DNFExpr dexpr=rconj.get(l);
 			    /* See if update interferes w/ dexpr */
 			    if (interferes(un,update, r,dexpr))
@@ -33,10 +55,57 @@ class ConcreteInterferes {
 	return false;
     }
 
+    static private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
+	AbstractRepair ar=mun.getRepair();
+	if (satisfy)
+	    return true;
+	if (ar==null)
+	    return true;
+	if (ar.getType()!=AbstractRepair.ADDTOSET)
+	    return true;
+	//	if (mun.op!=MultUpdateNode.ADD)  (Redundant)
+	//    return true;
+	if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
+	    return true;
+	boolean negated=ar.getPredicate().isNegated();
+	Predicate p=ar.getPredicate().getPredicate();
+	if (!(p instanceof ExprPredicate))
+	    return true;
+	ExprPredicate ep=(ExprPredicate)p;
+	if (ep.getType()!=ExprPredicate.SIZE)
+	    return true;
+	if ((ep.getOp()==Opcode.EQ)&&(ep.leftsize()==1)&&!negated)
+	    return false;
+	if ((ep.getOp()==Opcode.NE)&&(ep.leftsize()==1)&&negated)
+	    return false;
+
+	if ((ep.getOp()==Opcode.NE)&&(ep.leftsize()==0)&&!negated)
+	    return false;
+	if ((ep.getOp()==Opcode.EQ)&&(ep.leftsize()==0)&&negated)
+	    return false;
+
+
+
+	if ((ep.getOp()==Opcode.GT)&&(ep.leftsize()==0)&&!negated)
+	    return false;
+	if ((ep.getOp()==Opcode.LE)&&(ep.leftsize()==0)&&negated)
+	    return false;
+
+	if ((ep.getOp()==Opcode.GE)&&(ep.leftsize()==1)&&!negated)
+	    return false;
+	if ((ep.getOp()==Opcode.LT)&&(ep.leftsize()==1)&&negated)
+	    return false;
+	
+	return true;
+
+	
+    }
+
     static private boolean interferes(UpdateNode un,Updates update, Rule r,DNFExpr dexpr) {
 	Descriptor descriptor=update.getDescriptor();
 	if (!dexpr.getExpr().usesDescriptor(descriptor))
 	    return false;
+	    
 	/* We need to pair the variables */
 	if (update.isExpr()) {
 	    Set vars=update.getRightExpr().freeVars();
diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
new file mode 100755
index 0000000..fd32767
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
@@ -0,0 +1,117 @@
+package MCC.IR;
+import java.util.*;
+import MCC.State;
+
+public class GraphAnalysis {
+    Termination termination;
+    static final int WORKS=0;
+    static final int ERR_NOREPAIR=1;
+    static final int ERR_CYCLE=2;
+    static final int ERR_RULE=3;
+    static final int ERR_ABSTRACT=4;
+
+    public GraphAnalysis(Termination t) {
+	termination=t;
+    }
+    /* This function checks that
+       1) All abstract repairs have a corresponding data structure update
+          that isn't removed.
+       2) All scope nodes have either a consequence node or a compensation
+          node that isn't removed.
+     */
+    public int checkRepairs(Set removed) {
+	Set nodes=new HashSet();
+	nodes.addAll(termination.conjunctions);
+	nodes.removeAll(removed);
+	GraphNode.computeclosure(nodes,removed);
+	Set toretain=new HashSet();
+	toretain.addAll(termination.abstractrepair);
+	toretain.addAll(termination.scopenodes);
+	nodes.retainAll(toretain);
+	/* Nodes is now the reachable set of abstractrepairs */
+	/* Check to see that each has an implementation */
+	for(Iterator it=nodes.iterator();it.hasNext();) {
+	    GraphNode gn=(GraphNode)it.next();
+	    TermNode tn=(TermNode)gn.getOwner();
+	    if (tn.getType()==TermNode.RULESCOPE) {
+		boolean foundnode=false;
+		for (Iterator edgeit=gn.edges();it.hasNext();) {
+		    GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
+		    GraphNode gn2=edge.getTarget();
+		    if (!removed.contains(gn2)) {
+			TermNode tn2=(TermNode)gn2.getOwner();
+			if (tn2.getType()==TermNode.CONSEQUENCE||
+			    tn2.getType()==TermNode.UPDATE) {
+			    foundnode=true;
+			    break;
+			}
+		    }
+		}
+		if (!foundnode)
+		    return ERR_RULE;
+	    } else if (tn.getType()==TermNode.ABSTRACT) {
+		boolean foundnode=false;
+		for (Iterator edgeit=gn.edges();it.hasNext();) {
+		    GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
+		    GraphNode gn2=edge.getTarget();
+		    if (!removed.contains(gn2)) {
+			TermNode tn2=(TermNode)gn2.getOwner();
+			if (tn2.getType()==TermNode.UPDATE) {
+			    foundnode=true;
+			    break;
+			}
+		    }
+		}
+		if (!foundnode)
+		    return ERR_ABSTRACT;
+	    } else throw new Error("Unanticipated Node");
+	}
+	return WORKS;
+    }
+    /* This method checks that all constraints have a conjunction nodes
+       and that there are no bad cycles in the abstract portion of the graph.
+     */
+    public int checkAbstract(Set removed) {
+	Vector constraints=termination.state.vConstraints;
+	for(int i=0;i<constraints.size();i++) {
+	    Constraint c=(Constraint)constraints.get(i);
+	    Set conjunctionset=(Set)termination.conjunctionmap.get(c);
+
+   	    boolean foundrepair=false;
+	    for(Iterator it=conjunctionset.iterator();it.hasNext();) {
+		GraphNode gn=(GraphNode)it.next();
+		if (!removed.contains(gn)) {
+		    foundrepair=true;
+		}
+   	    }
+	    if (!foundrepair)
+		return ERR_NOREPAIR;
+	}
+	Set abstractnodes=new HashSet();
+       	abstractnodes.addAll(termination.conjunctions);
+	abstractnodes.removeAll(removed);
+	GraphNode.computeclosure(abstractnodes,removed);
+
+	Set tset=new HashSet();
+	tset.addAll(termination.conjunctions);
+	tset.addAll(termination.abstractrepair);
+	tset.addAll(termination.scopenodes);
+	tset.addAll(termination.consequencenodes);
+	abstractnodes.retainAll(tset);
+	Set cycles=GraphNode.findcycles(abstractnodes);
+
+	for(Iterator it=cycles.iterator();it.hasNext();) {
+	    GraphNode gn=(GraphNode)it.next();
+	    TermNode tn=(TermNode)gn.getOwner();
+	    switch(tn.getType()) {
+	    case TermNode.CONJUNCTION:
+	    case TermNode.ABSTRACT:
+		return ERR_CYCLE;
+	    case TermNode.UPDATE:
+		throw new Error("No Update Nodes should be here");
+	    default:
+	    }
+	}
+	return WORKS;
+    }
+}
diff --git a/Repair/RepairCompiler/MCC/IR/GraphNode.java b/Repair/RepairCompiler/MCC/IR/GraphNode.java
index 5a3a85b..eab9691 100755
--- a/Repair/RepairCompiler/MCC/IR/GraphNode.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphNode.java
@@ -83,7 +83,7 @@ public class GraphNode {
         return owner;
     }
 
-    public static void computeclosure(Set nodes) {
+    public static void computeclosure(Set nodes, Set removed) {
 	Stack tovisit=new Stack();
 	tovisit.addAll(nodes);
 	while(!tovisit.isEmpty()) {
@@ -92,8 +92,11 @@ public class GraphNode {
 		Edge edge=(Edge)it.next();
 		GraphNode target=edge.getTarget();
 		if (!nodes.contains(target)) {
-		    nodes.add(target);
-		    tovisit.push(target);
+		    if ((removed!=null)&&
+			(!removed.contains(target))) {
+			nodes.add(target);
+			tovisit.push(target);
+		    }
 		}
 	    }
 	}
@@ -301,7 +304,7 @@ public class GraphNode {
             i = nodes.iterator();
             while (i.hasNext()) {
                 GraphNode gn = (GraphNode) i.next();
-                assert gn.getStatus() != PROCESSING;                    
+		assert gn.getStatus() != PROCESSING;                    
                 if (gn.getStatus() == UNVISITED) {
                     if (!dfs(gn))
 			acyclic=false;
@@ -318,6 +321,8 @@ public class GraphNode {
             while (edges.hasNext()) {
                 Edge edge = (Edge) edges.next();
                 GraphNode node = edge.getTarget();
+		if (!nodes.contains(node)) /* Skip nodes which aren't in the set */
+		    continue;
                 if (node.getStatus() == UNVISITED) {
                     if (!dfs(node))
 			acyclic=false;
diff --git a/Repair/RepairCompiler/MCC/IR/MultUpdateNode.java b/Repair/RepairCompiler/MCC/IR/MultUpdateNode.java
index 94c109b..206aeab 100755
--- a/Repair/RepairCompiler/MCC/IR/MultUpdateNode.java
+++ b/Repair/RepairCompiler/MCC/IR/MultUpdateNode.java
@@ -26,6 +26,7 @@ class MultUpdateNode {
     public MultUpdateNode(ScopeNode sn) {
 	updates=new Vector();
 	scopenode=sn;
+	op=MultUpdateNode.REMOVE;
     }
     void addUpdate(UpdateNode un) {
 	updates.add(un);
diff --git a/Repair/RepairCompiler/MCC/IR/ScopeNode.java b/Repair/RepairCompiler/MCC/IR/ScopeNode.java
index 168117d..e125dd0 100755
--- a/Repair/RepairCompiler/MCC/IR/ScopeNode.java
+++ b/Repair/RepairCompiler/MCC/IR/ScopeNode.java
@@ -16,6 +16,10 @@ class ScopeNode {
 	    return ((RelationInclusion)inc).getRelation();
 	else throw new Error("Unrecognized Inclusion");
     }
+
+    public Rule getRule() {
+	return rule;
+    }
     public boolean getSatisfy() {
 	return satisfy;
     }
diff --git a/Repair/RepairCompiler/MCC/IR/TermNode.java b/Repair/RepairCompiler/MCC/IR/TermNode.java
index 7fadf32..337c569 100755
--- a/Repair/RepairCompiler/MCC/IR/TermNode.java
+++ b/Repair/RepairCompiler/MCC/IR/TermNode.java
@@ -15,6 +15,10 @@ class TermNode {
     ScopeNode scope;
     MultUpdateNode update;
 
+    public int getType() {
+	return type;
+    }
+
     public TermNode(Constraint constr, Conjunction conj) {
 	this.constr=constr;
 	this.conj=conj;
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index f3d134f..b788acc 100755
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -51,7 +51,7 @@ public class Termination {
 	//superset.addAll(updatenodes);
 	//superset.addAll(scopenodes);
 	//superset.addAll(consequencenodes);
-	GraphNode.computeclosure(superset);
+	GraphNode.computeclosure(superset,null);
 	try {
 	    GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
 	} catch (Exception e) {
@@ -65,6 +65,7 @@ public class Termination {
 	    System.out.println(gn.getTextLabel());
 	    System.out.println(mun.toString());
 	}
+	GraphAnalysis ga=new GraphAnalysis(this);
     }
     
     void generateconjunctionnodes() {
@@ -78,7 +79,9 @@ public class Termination {
 					   "Conj ("+i+","+j+") "+dnf.get(j).name()
 					   ,tn);
 		conjunctions.add(gn);
-		conjunctionmap.put(c,gn);
+		if (!conjunctionmap.containsKey(c))
+		    conjunctionmap.put(c,new HashSet());
+		((Set)conjunctionmap.get(c)).add(gn);
 	    }
 	}
     }
@@ -127,6 +130,16 @@ public class Termination {
 		    }
 		}
 	    }
+
+	    for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
+		GraphNode gn2=(GraphNode)scopeiterator.next();
+		TermNode tn2=(TermNode)gn2.getOwner();
+		ScopeNode sn2=tn2.getScope();
+		if (AbstractInterferes.interferes(ar,sn2.getRule(),sn2.getSatisfy())) {
+		    GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
+		    gn.addEdge(e);
+		}
+	    }
 	}
     }
     
@@ -261,7 +274,7 @@ public class Termination {
 		MultUpdateNode mun=new MultUpdateNode(sn);
 		TermNode tn2=new TermNode(mun);
 		GraphNode gn2=new GraphNode("CompRem"+compensationcount,tn2);
-		UpdateNode un=new UpdateNode();
+		UpdateNode un=new UpdateNode(r);
 		un.addBindings(bindings);
 		if (j<r.numQuantifiers()) {
 		    /* Remove quantifier */
@@ -360,7 +373,7 @@ public class Termination {
 	    boolean goodflag=true;
 	    for(int i=0;i<possiblerules.size();i++) {
 		Rule r=(Rule)possiblerules.get(i);
-		UpdateNode un=new UpdateNode();
+		UpdateNode un=new UpdateNode(r);
 		/* Construct bindings */
 		Vector bindings=new Vector();
 		constructbindings(bindings, r,true);
@@ -559,7 +572,7 @@ public class Termination {
 		DNFRule dnfrule=r.getDNFGuardExpr();
 		for(int j=0;j<dnfrule.size();j++) {
 		    Inclusion inc=r.getInclusion();
-		    UpdateNode un=new UpdateNode();
+		    UpdateNode un=new UpdateNode(r);
 		    un.addBindings(bindings);
 		    /* Now build update for tuple/set inclusion condition */
 		    if(inc instanceof SetInclusion) {
diff --git a/Repair/RepairCompiler/MCC/IR/UpdateNode.java b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
index 16388e0..5bb9236 100755
--- a/Repair/RepairCompiler/MCC/IR/UpdateNode.java
+++ b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
@@ -5,11 +5,18 @@ class UpdateNode {
     Vector updates;
     Vector bindings;
     Hashtable binding;
+    Rule rule;
+    
 
-    public UpdateNode() {
+    public UpdateNode(Rule r) {
 	updates=new Vector();
 	bindings=new Vector();
 	binding=new Hashtable();
+	rule=r;
+    }
+
+    public Rule getRule() {
+	return rule;
     }
 
     public String toString() {