Checking in code to perform safety checks on repair dependency graph.
authorbdemsky <bdemsky>
Fri, 6 Feb 2004 22:33:01 +0000 (22:33 +0000)
committerbdemsky <bdemsky>
Fri, 6 Feb 2004 22:33:01 +0000 (22:33 +0000)
Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
Repair/RepairCompiler/MCC/IR/GraphAnalysis.java [new file with mode: 0755]
Repair/RepairCompiler/MCC/IR/GraphNode.java
Repair/RepairCompiler/MCC/IR/MultUpdateNode.java
Repair/RepairCompiler/MCC/IR/ScopeNode.java
Repair/RepairCompiler/MCC/IR/TermNode.java
Repair/RepairCompiler/MCC/IR/Termination.java
Repair/RepairCompiler/MCC/IR/UpdateNode.java

index 4217361..5b24327 100755 (executable)
@@ -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)||
index c4855bc..c711d82 100755 (executable)
@@ -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 (executable)
index 0000000..fd32767
--- /dev/null
@@ -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;
+    }
+}
index 5a3a85b..eab9691 100755 (executable)
@@ -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;
index 94c109b..206aeab 100755 (executable)
@@ -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);
index 168117d..e125dd0 100755 (executable)
@@ -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;
     }
index 7fadf32..337c569 100755 (executable)
@@ -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;
index f3d134f..b788acc 100755 (executable)
@@ -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) {
index 16388e0..5bb9236 100755 (executable)
@@ -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() {