Adding code to generate repair algorithms. Its not complete yet...
authorbdemsky <bdemsky>
Thu, 12 Feb 2004 06:53:39 +0000 (06:53 +0000)
committerbdemsky <bdemsky>
Thu, 12 Feb 2004 06:53:39 +0000 (06:53 +0000)
This checkin sets defaults to repair...

14 files changed:
Repair/RepairCompiler/MCC/Compiler.java
Repair/RepairCompiler/MCC/IR/DotExpr.java
Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
Repair/RepairCompiler/MCC/IR/GraphNode.java
Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
Repair/RepairCompiler/MCC/IR/RelationInclusion.java
Repair/RepairCompiler/MCC/IR/Repair.java [new file with mode: 0755]
Repair/RepairCompiler/MCC/IR/RepairGenerator.java [new file with mode: 0755]
Repair/RepairCompiler/MCC/IR/Rule.java
Repair/RepairCompiler/MCC/IR/SetDescriptor.java
Repair/RepairCompiler/MCC/IR/SetInclusion.java
Repair/RepairCompiler/MCC/IR/StructureTypeDescriptor.java
Repair/RepairCompiler/MCC/IR/Termination.java
Repair/RepairCompiler/MCC/State.java

index 7773d7fa9a47dd14b57f61dfff0c9aab590c2fa5..ebda670ebd356603137db75373233fba87bd4b85 100755 (executable)
@@ -85,14 +85,16 @@ public class Compiler {
             
             try {
                 FileOutputStream gcode = new FileOutputStream(cli.infile + ".cc");
             
             try {
                 FileOutputStream gcode = new FileOutputStream(cli.infile + ".cc");
+                FileOutputStream gcode2 = new FileOutputStream(cli.infile + "_aux.cc");
+                FileOutputStream gcode3 = new FileOutputStream(cli.infile + "_aux.h");
 
                 // do model optimizations
                 //(new Optimizer(state)).optimize();
 
 
                 // do model optimizations
                 //(new Optimizer(state)).optimize();
 
-                NaiveGenerator ng = new NaiveGenerator(state);
-                ng.generate(gcode);
-                //WorklistGenerator wg = new WorklistGenerator(state);
-                //wg.generate(gcode);
+                //NaiveGenerator ng = new NaiveGenerator(state);
+                //ng.generate(gcode);
+                RepairGenerator wg = new RepairGenerator(state);
+                wg.generate(gcode,gcode2,gcode3, cli.infile + "_aux.h");
                 gcode.close();
             } catch (Exception e) {
                 e.printStackTrace();
                 gcode.close();
             } catch (Exception e) {
                 e.printStackTrace();
index 93beabc066126c04e55a3e0c25bc47a306a0a15b..82539912aa4f4042c6a243022f92231493be1ce8 100755 (executable)
@@ -115,7 +115,7 @@ public class DotExpr extends Expr {
         // descriptor not the underlying field descriptor
 
         /* we calculate the offset in bits */
         // descriptor not the underlying field descriptor
 
         /* we calculate the offset in bits */
-        offsetbits = struct.getOffsetExpr(fd);                    
+        offsetbits = struct.getOffsetExpr(fd);
 
         if (fd instanceof ArrayDescriptor) {
             fd = ((ArrayDescriptor) fd).getField();
 
         if (fd instanceof ArrayDescriptor) {
             fd = ((ArrayDescriptor) fd).getField();
index fd3276752e3c28544c276b5e828498737363f68d..3488a66ab383d29183a3a1db02a447a8ffd13acd 100755 (executable)
@@ -13,13 +13,118 @@ public class GraphAnalysis {
     public GraphAnalysis(Termination t) {
        termination=t;
     }
     public GraphAnalysis(Termination t) {
        termination=t;
     }
+
+    public Set doAnalysis() {
+       HashSet nodes=new HashSet();
+       nodes.addAll(termination.conjunctions);
+       GraphNode.computeclosure(nodes,null);
+       Set cycles=GraphNode.findcycles(nodes);
+       Set couldremove=new HashSet();
+       couldremove.addAll(termination.conjunctions);
+       couldremove.addAll(termination.updatenodes);
+       couldremove.addAll(termination.consequencenodes);
+       couldremove.retainAll(cycles);
+       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);
+           if (conjunctionset.size()==1)
+               couldremove.removeAll(conjunctionset);
+       }
+
+
+       Vector couldremovevector=new Vector();
+       couldremovevector.addAll(couldremove);
+       Vector combination=new Vector();
+
+       while(true) {
+           if (illegal(combination,couldremovevector))
+               break;
+           Set combinationset=buildset(combination,couldremovevector);
+           if (combinationset!=null) {
+               System.out.println("Checkabstract="+checkAbstract(combinationset));
+               System.out.println("Checkrepairs="+checkRepairs(combinationset));
+               System.out.println("Checkall="+checkAll(combinationset));
+               
+               if (checkAbstract(combinationset)==0&&
+                   checkRepairs(combinationset)==0&&
+                   checkAll(combinationset)==0) {
+                   return combinationset;
+               }
+           }
+           increment(combination,couldremovevector);
+       }
+       return null;
+    }
+
+    private static Set buildset(Vector combination, Vector couldremove) {
+       Set s=new HashSet();
+       for(int i=0;i<combination.size();i++) {
+           int index=((Integer)combination.get(i)).intValue();
+           Object o=couldremove.get(index);
+           if (s.contains(o))
+               return null;
+           else
+               s.add(o);
+       }
+       return s;
+    }
+
+    private static boolean illegal(Vector combination, Vector couldremove) {
+       if (combination.size()>couldremove.size())
+           return true;
+       else return false;
+    }
+    private static void increment(Vector combination, Vector couldremove) {
+       boolean incremented=false;
+       for(int i=0;i<combination.size();i++) {
+           int newindex=((Integer)combination.get(i)).intValue()+1;
+           while(combination.contains(new Integer(newindex)))
+               newindex++;
+           if (newindex==couldremove.size()) {
+               newindex=0;
+               combination.set(i,new Integer(newindex));
+           } else {
+               incremented=true;
+               combination.set(i,new Integer(newindex));
+               break;
+           }
+       }
+       if (incremented==false) /* Increase length */
+           combination.add(new Integer(0));
+    }
+
+    /* This function checks the graph as a whole for bad cycles */
+    public int checkAll(Collection removed) {
+       Set nodes=new HashSet();
+       nodes.addAll(termination.conjunctions);
+       nodes.removeAll(removed);
+       GraphNode.computeclosure(nodes,removed);
+       Set cycles=GraphNode.findcycles(nodes);
+       for(Iterator it=cycles.iterator();it.hasNext();) {
+           GraphNode gn=(GraphNode)it.next();
+           TermNode tn=(TermNode)gn.getOwner();
+           switch(tn.getType()) {
+           case TermNode.UPDATE:
+           case TermNode.CONJUNCTION:
+               return ERR_CYCLE;
+           case TermNode.ABSTRACT:
+           case TermNode.RULESCOPE:
+           case TermNode.CONSEQUENCE:
+           default:
+               break;
+           }
+       }
+       return WORKS;
+    }
+
     /* 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.
      */
     /* 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) {
+    public int checkRepairs(Collection removed) {
        Set nodes=new HashSet();
        nodes.addAll(termination.conjunctions);
        nodes.removeAll(removed);
        Set nodes=new HashSet();
        nodes.addAll(termination.conjunctions);
        nodes.removeAll(removed);
@@ -35,23 +140,25 @@ public class GraphAnalysis {
            TermNode tn=(TermNode)gn.getOwner();
            if (tn.getType()==TermNode.RULESCOPE) {
                boolean foundnode=false;
            TermNode tn=(TermNode)gn.getOwner();
            if (tn.getType()==TermNode.RULESCOPE) {
                boolean foundnode=false;
-               for (Iterator edgeit=gn.edges();it.hasNext();) {
+               for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
                    GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
                    GraphNode gn2=edge.getTarget();
                    if (!removed.contains(gn2)) {
                        TermNode tn2=(TermNode)gn2.getOwner();
                    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) {
+                       if ((tn2.getType()==TermNode.CONSEQUENCE)||
+                           (tn2.getType()==TermNode.UPDATE)) {
                            foundnode=true;
                            break;
                        }
                    }
                }
                            foundnode=true;
                            break;
                        }
                    }
                }
-               if (!foundnode)
+               if (!foundnode) {
+                   System.out.println(gn.getTextLabel());
                    return ERR_RULE;
                    return ERR_RULE;
+               }
            } else if (tn.getType()==TermNode.ABSTRACT) {
                boolean foundnode=false;
            } else if (tn.getType()==TermNode.ABSTRACT) {
                boolean foundnode=false;
-               for (Iterator edgeit=gn.edges();it.hasNext();) {
+               for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
                    GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
                    GraphNode gn2=edge.getTarget();
                    if (!removed.contains(gn2)) {
                    GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
                    GraphNode gn2=edge.getTarget();
                    if (!removed.contains(gn2)) {
@@ -68,10 +175,10 @@ public class GraphAnalysis {
        }
        return WORKS;
     }
        }
        return WORKS;
     }
-    /* This method checks that all constraints have conjunction nodes
+    /* This method checks that all constraints have conjunction nodes
        and that there are no bad cycles in the abstract portion of the graph.
      */
        and that there are no bad cycles in the abstract portion of the graph.
      */
-    public int checkAbstract(Set removed) {
+    public int checkAbstract(Collection removed) {
        Vector constraints=termination.state.vConstraints;
        for(int i=0;i<constraints.size();i++) {
            Constraint c=(Constraint)constraints.get(i);
        Vector constraints=termination.state.vConstraints;
        for(int i=0;i<constraints.size();i++) {
            Constraint c=(Constraint)constraints.get(i);
@@ -99,9 +206,10 @@ public class GraphAnalysis {
        tset.addAll(termination.consequencenodes);
        abstractnodes.retainAll(tset);
        Set cycles=GraphNode.findcycles(abstractnodes);
        tset.addAll(termination.consequencenodes);
        abstractnodes.retainAll(tset);
        Set cycles=GraphNode.findcycles(abstractnodes);
-
+       
        for(Iterator it=cycles.iterator();it.hasNext();) {
            GraphNode gn=(GraphNode)it.next();
        for(Iterator it=cycles.iterator();it.hasNext();) {
            GraphNode gn=(GraphNode)it.next();
+           System.out.println("NODE: "+gn.getTextLabel());
            TermNode tn=(TermNode)gn.getOwner();
            switch(tn.getType()) {
            case TermNode.CONJUNCTION:
            TermNode tn=(TermNode)gn.getOwner();
            switch(tn.getType()) {
            case TermNode.CONJUNCTION:
index eab969124c546d50472d840635950ed79de42dc9..f5448e3e8819e89a07412b541347593f4882bb36 100755 (executable)
@@ -83,7 +83,7 @@ public class GraphNode {
         return owner;
     }
 
         return owner;
     }
 
-    public static void computeclosure(Set nodes, Set removed) {
+    public static void computeclosure(Collection nodes, Collection removed) {
        Stack tovisit=new Stack();
        tovisit.addAll(nodes);
        while(!tovisit.isEmpty()) {
        Stack tovisit=new Stack();
        tovisit.addAll(nodes);
        while(!tovisit.isEmpty()) {
@@ -92,7 +92,7 @@ public class GraphNode {
                Edge edge=(Edge)it.next();
                GraphNode target=edge.getTarget();
                if (!nodes.contains(target)) {
                Edge edge=(Edge)it.next();
                GraphNode target=edge.getTarget();
                if (!nodes.contains(target)) {
-                   if ((removed!=null)&&
+                   if ((removed==null)||
                        (!removed.contains(target))) {
                        nodes.add(target);
                        tovisit.push(target);
                        (!removed.contains(target))) {
                        nodes.add(target);
                        tovisit.push(target);
index fc8396716618b2b9e4c54a3694a7df4dd03d1581..7e8aee5aca37d2697b51692012c827031155e76c 100755 (executable)
@@ -299,7 +299,9 @@ public class ImplicitSchema {
                        nr.isdelay=r.isdelay;
                        nr.inclusion=new SetInclusion(((SetInclusion)r.inclusion).elementexpr,sd1);
                        nr.st=r.st;
                        nr.isdelay=r.isdelay;
                        nr.inclusion=new SetInclusion(((SetInclusion)r.inclusion).elementexpr,sd1);
                        nr.st=r.st;
+                       nr.setnogenerate();
                        newrules.add(nr);
                        newrules.add(nr);
+                       state.implicitrule.put(nr,r);
                    }
            }
        }
                    }
            }
        }
index d1b3a02d1b281ad31526904079d9b567e291a29a..76d60acc09b356e293fa1b764f70efa802326a73 100755 (executable)
@@ -1,5 +1,5 @@
 package MCC.IR;
 package MCC.IR;
-
+import MCC.Compiler;
 import java.util.*;
 
 public class RelationInclusion extends Inclusion {
 import java.util.*;
 
 public class RelationInclusion extends Inclusion {
@@ -106,6 +106,14 @@ public class RelationInclusion extends Inclusion {
             writer.endblock();
         }
 
             writer.endblock();
         }
 
+        if (Compiler.REPAIR) {
+            writer.outputline("if (" + addeditem + ")");
+            writer.startblock(); {                
+                Repair.generate_dispatch(writer, relation, rd.getSafeSymbol(), ld.getSafeSymbol());
+            }
+            writer.endblock();
+        }
+
         if (!typesafe) {
             writer.endblock();
         }            
         if (!typesafe) {
             writer.endblock();
         }            
@@ -138,7 +146,6 @@ public class RelationInclusion extends Inclusion {
             sa.getErrorReporter().report(null, "Type of right element '" + rd.getSymbol() + "' must match range type '" + relation.getRange().getType().getSymbol() + "'");
             ok = false;
         }
             sa.getErrorReporter().report(null, "Type of right element '" + rd.getSymbol() + "' must match range type '" + relation.getRange().getType().getSymbol() + "'");
             ok = false;
         }
-
         return ok;
     }
 
         return ok;
     }
 
diff --git a/Repair/RepairCompiler/MCC/IR/Repair.java b/Repair/RepairCompiler/MCC/IR/Repair.java
new file mode 100755 (executable)
index 0000000..e2fd969
--- /dev/null
@@ -0,0 +1,86 @@
+package MCC.IR;
+
+import MCC.State;
+import java.util.*;
+
+public class Repair {
+
+
+    public static Vector getrulelist(Descriptor d) {
+
+        Vector dispatchrules = new Vector();
+        Vector rules = State.currentState.vRules;        
+        
+        for (int i = 0; i < rules.size(); i++) {
+            Rule rule = (Rule) rules.elementAt(i);
+            Set requiredsymbols = rule.getRequiredDescriptors();
+            
+            // #TBD#: in general this is wrong because these descriptors may contain descriptors
+            // bound in "in?" expressions which need to be dealt with in a topologically sorted
+            // fashion...
+
+            if (rule.getRequiredDescriptors().contains(d)) {
+                dispatchrules.addElement(rule);
+            }
+        }
+        return dispatchrules;
+    }
+    
+
+    public static void generate_dispatch(CodeWriter cr, RelationDescriptor rd, String leftvar, String rightvar) {
+
+        cr.outputline("// RELATION DISPATCH ");        
+
+        Vector dispatchrules = getrulelist(rd);
+        
+        if (dispatchrules.size() == 0) {
+            cr.outputline("// nothing to dispatch");
+            return;
+        }
+       
+        for(int i = 0; i < dispatchrules.size(); i++) {
+            Rule rule = (Rule) dispatchrules.elementAt(i);
+           if (rule.getGuardExpr().getRequiredDescriptors().contains(rd)) {
+               /* Guard depends on this relation, so we recomput everything */
+               cr.outputline("WORKLIST->add("+rule.getNum()+",-1,0,0);");
+           } else {
+               for (int j=0;j<rule.numQuantifiers();j++) {
+                   Quantifier q=rule.getQuantifier(j);
+                   if (q.getRequiredDescriptors().contains(rd)) {
+                       /* Generate add */
+                       cr.outputline("WORKLIST->add("+rule.getNum()+","+j+","+leftvar+","+rightvar+");");
+                   }
+               }
+           }
+        }
+    }
+
+
+    public static void generate_dispatch(CodeWriter cr, SetDescriptor sd, String setvar) {
+               
+        cr.outputline("// SET DISPATCH ");        
+        Vector dispatchrules = getrulelist(sd);
+
+        if (dispatchrules.size() == 0) {
+            cr.outputline("// nothing to dispatch");
+            return;
+        }
+
+        for(int i = 0; i < dispatchrules.size(); i++) {
+            Rule rule = (Rule) dispatchrules.elementAt(i);
+           if (SetDescriptor.expand(rule.getGuardExpr().getRequiredDescriptors()).contains(sd)) {
+               /* Guard depends on this relation, so we recomput everything */
+               cr.outputline("WORKLIST->add("+rule.getNum()+",-1,0,0);");
+           } else {
+               for (int j=0;j<rule.numQuantifiers();j++) {
+                   Quantifier q=rule.getQuantifier(j);
+                   if (SetDescriptor.expand(q.getRequiredDescriptors()).contains(sd)) {
+                       /* Generate add */
+                       cr.outputline("WORKLIST->add("+rule.getNum()+","+j+","+setvar+",0);");
+                   }
+               }
+           }
+       }
+    }
+}
diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
new file mode 100755 (executable)
index 0000000..b20ae6f
--- /dev/null
@@ -0,0 +1,401 @@
+package MCC.IR;
+
+import java.io.*;
+import java.util.*;
+import MCC.State;
+
+public class RepairGenerator {
+
+    State state;
+    java.io.PrintWriter outputrepair = null;
+    java.io.PrintWriter outputaux = null;
+    java.io.PrintWriter outputhead = null;
+    String name="foo";
+    String headername;
+    public RepairGenerator(State state) {
+        this.state = state;
+    }
+
+    public void generate(OutputStream outputrepair, OutputStream outputaux,OutputStream outputhead, String st) {
+        this.outputrepair = new java.io.PrintWriter(outputrepair, true); 
+        this.outputaux = new java.io.PrintWriter(outputaux, true); 
+        this.outputhead = new java.io.PrintWriter(outputhead, true); 
+        headername=st;
+
+        generate_tokentable();
+        generate_hashtables();
+       generate_stateobject();
+       generate_call();
+       /*        generate_worklist();
+        generate_rules();
+        generate_checks();
+        generate_teardown();*/
+
+    }
+
+    private void generate_call() {
+        CodeWriter cr = new StandardCodeWriter(outputrepair);        
+       VarDescriptor vdstate=VarDescriptor.makeNew("repairstate");
+       cr.outputline(name+"_state * "+vdstate.getSafeSymbol()+"=new "+name+"_state();");
+       
+
+       Iterator globals=state.stGlobals.descriptors();
+       while (globals.hasNext()) {
+           VarDescriptor vd=(VarDescriptor) globals.next();
+           cr.outputline(vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+"=("+vd.getType().getGenerateType().getSafeSymbol()+")"+vd.getSafeSymbol()+";");
+       }
+       /* Insert repair here */
+
+       globals=state.stGlobals.descriptors();
+       while (globals.hasNext()) {
+           VarDescriptor vd=(VarDescriptor) globals.next();
+           cr.outputline("*(("+vd.getType().getGenerateType().getSafeSymbol()+"*) &"+vd.getSafeSymbol()+")="+vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+";");
+       }
+       
+       cr.outputline("delete ("+vdstate.getSafeSymbol()+");");
+    }
+    private void generate_tokentable() {
+
+        CodeWriter cr = new StandardCodeWriter(outputrepair);        
+        Iterator tokens = TokenLiteralExpr.tokens.keySet().iterator();        
+
+        cr.outputline("");
+        cr.outputline("// Token values");
+        cr.outputline("");
+
+        while (tokens.hasNext()) {
+            Object token = tokens.next();
+            cr.outputline("// " + token.toString() + " = " + TokenLiteralExpr.tokens.get(token).toString());            
+        }
+
+        cr.outputline("");
+        cr.outputline("");
+    }
+
+    private void generate_stateobject() {
+        CodeWriter crhead = new StandardCodeWriter(outputhead);
+       crhead.outputline("class "+name+"_state {");
+       crhead.outputline("public:");
+       Iterator globals=state.stGlobals.descriptors();
+       while (globals.hasNext()) {
+           VarDescriptor vd=(VarDescriptor) globals.next();
+           crhead.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+";");
+       }
+    }
+
+    private void generate_hashtables() {
+        CodeWriter craux = new StandardCodeWriter(outputaux);
+        CodeWriter crhead = new StandardCodeWriter(outputhead);
+        crhead.outputline("#include \"SimpleHash.h\"");
+       crhead.outputline("class "+name+" {");
+       crhead.outputline("public:");
+       crhead.outputline(name+"();");
+       crhead.outputline("~"+name+"();");
+        craux.outputline("#include \""+headername+"\"");
+
+        craux.outputline(name+"::"+name+"() {");
+        craux.outputline("// creating hashtables ");
+        
+        /* build sets */
+        Iterator sets = state.stSets.descriptors();
+        
+        /* first pass create all the hash tables */
+        while (sets.hasNext()) {
+            SetDescriptor set = (SetDescriptor) sets.next();
+           crhead.outputline("SimpleHash* " + set.getSafeSymbol() + "_hash;");
+            craux.outputline(set.getSafeSymbol() + "_hash = new SimpleHash();");
+        } 
+        
+        /* second pass build relationships between hashtables */
+        sets = state.stSets.descriptors();
+        
+        while (sets.hasNext()) {
+            SetDescriptor set = (SetDescriptor) sets.next();
+            Iterator subsets = set.subsets();
+            
+            while (subsets.hasNext()) {
+                SetDescriptor subset = (SetDescriptor) subsets.next();                
+                craux.outputline(subset.getSafeSymbol() + "_hash->addParent(" + set.getSafeSymbol() + "_hash);");
+            }
+        } 
+
+        /* build relations */
+        Iterator relations = state.stRelations.descriptors();
+        
+        /* first pass create all the hash tables */
+        while (relations.hasNext()) {
+            RelationDescriptor relation = (RelationDescriptor) relations.next();
+            
+            if (relation.testUsage(RelationDescriptor.IMAGE)) {
+                crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hash;");
+                craux.outputline(relation.getSafeSymbol() + "_hash = new SimpleHash();");
+            }
+
+            if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
+                crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hashinv;");
+                craux.outputline(relation.getSafeSymbol() + "_hashinv = new SimpleHash();");
+            } 
+        }
+
+        craux.outputline("}");
+        crhead.outputline("};");
+        craux.outputline(name+"::~"+name+"() {");
+        craux.outputline("// deleting hashtables");
+
+        /* build destructor */
+        sets = state.stSets.descriptors();
+        
+        /* first pass create all the hash tables */
+        while (sets.hasNext()) {
+            SetDescriptor set = (SetDescriptor) sets.next();
+            craux.outputline("delete("+set.getSafeSymbol() + "_hash);");
+        } 
+        
+        /* destroy relations */
+        relations = state.stRelations.descriptors();
+        
+        /* first pass create all the hash tables */
+        while (relations.hasNext()) {
+            RelationDescriptor relation = (RelationDescriptor) relations.next();
+            
+            if (relation.testUsage(RelationDescriptor.IMAGE)) {
+                craux.outputline("delete("+relation.getSafeSymbol() + "_hash);");
+            }
+
+            if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
+                craux.outputline("delete(" + relation.getSafeSymbol() + ");");
+            } 
+        }
+        craux.outputline("}");
+    }
+
+    private void generate_worklist() {
+        CodeWriter cr = new StandardCodeWriter(outputrepair);
+        cr.outputline("WORKLIST = new WorkList();");
+    }
+    
+    private void generate_teardown() {
+        CodeWriter cr = new StandardCodeWriter(outputrepair);        
+        cr.outputline("delete WORKLIST;");
+    }
+
+    private void generate_rules() {
+        
+        /* first we must sort the rules */
+        Iterator allrules = state.vRules.iterator();
+
+        Vector emptyrules = new Vector(); // rules with no quantifiers
+        Vector worklistrules = new Vector(); // the rest of the rules
+
+        while (allrules.hasNext()) {
+            Rule rule = (Rule) allrules.next();
+            ListIterator quantifiers = rule.quantifiers();
+
+            boolean noquantifiers = true;
+            while (quantifiers.hasNext()) {
+                Quantifier quantifier = (Quantifier) quantifiers.next();
+                if (quantifier instanceof ForQuantifier) {
+                    // ok, because integers exist already!
+                } else {
+                    // real quantifier
+                    noquantifiers = false;
+                    break;
+                }
+            }
+
+            if (noquantifiers) {
+                emptyrules.add(rule);
+            } else {
+                worklistrules.add(rule);
+            }
+        }
+       
+        Iterator iterator_er = emptyrules.iterator();
+        while (iterator_er.hasNext()) {
+
+            Rule rule = (Rule) iterator_er.next();            
+
+            {
+                final SymbolTable st = rule.getSymbolTable();                
+                CodeWriter cr = new StandardCodeWriter(outputrepair) {
+                        public SymbolTable getSymbolTable() { return st; }
+                    };
+                
+                cr.outputline("// build " + rule.getLabel());
+                cr.startblock();
+
+                ListIterator quantifiers = rule.quantifiers();
+
+                while (quantifiers.hasNext()) {
+                    Quantifier quantifier = (Quantifier) quantifiers.next();                   
+                    quantifier.generate_open(cr);
+                }            
+                        
+                /* pretty print! */
+                cr.output("//");
+                rule.getGuardExpr().prettyPrint(cr);
+                cr.outputline("");
+
+                /* now we have to generate the guard test */
+        
+                VarDescriptor guardval = VarDescriptor.makeNew();
+                rule.getGuardExpr().generate(cr, guardval);
+                
+                cr.outputline("if (" + guardval.getSafeSymbol() + ")");
+                cr.startblock();
+
+                /* now we have to generate the inclusion code */
+                rule.getInclusion().generate(cr);
+                cr.endblock();
+
+                while (quantifiers.hasPrevious()) {
+                    Quantifier quantifier = (Quantifier) quantifiers.previous();
+                    cr.endblock();
+                }
+
+                cr.endblock();
+                cr.outputline("");
+                cr.outputline("");
+            }
+        }
+
+        CodeWriter cr2 = new StandardCodeWriter(outputrepair);        
+
+        cr2.outputline("WORKLIST->reset();");
+        cr2.outputline("while (WORKLIST->hasMoreElements())");
+        cr2.startblock();
+        cr2.outputline("WORKITEM *wi = (WORKITEM *) WORKLIST->nextElement();");
+        
+        String elseladder = "if";
+
+        Iterator iterator_rules = worklistrules.iterator();
+        while (iterator_rules.hasNext()) {
+            
+            Rule rule = (Rule) iterator_rules.next();            
+            int dispatchid = rule.getNum();
+
+            {
+                final SymbolTable st = rule.getSymbolTable();                
+                CodeWriter cr = new StandardCodeWriter(outputrepair) {
+                        public SymbolTable getSymbolTable() { return st; }
+                    };
+
+                cr.indent();
+                cr.outputline(elseladder + " (wi->id == " + dispatchid + ")");
+                cr.startblock();
+
+                cr.outputline("// build " + rule.getLabel());
+
+                ListIterator quantifiers = rule.quantifiers();
+
+                int count = 0;
+                while (quantifiers.hasNext()) {
+                    Quantifier quantifier = (Quantifier) quantifiers.next();
+                    count = quantifier.generate_worklistload(cr, count );                    
+                }
+                        
+                /* pretty print! */
+                cr.output("//");
+                rule.getGuardExpr().prettyPrint(cr);
+                cr.outputline("");
+
+                /* now we have to generate the guard test */
+        
+                VarDescriptor guardval = VarDescriptor.makeNew();
+                rule.getGuardExpr().generate(cr, guardval);
+                
+                cr.outputline("if (" + guardval.getSafeSymbol() + ")");
+                cr.startblock();
+
+                /* now we have to generate the inclusion code */
+                rule.getInclusion().generate(cr);
+                cr.endblock();
+
+                // close startblocks generated by DotExpr memory checks
+                //DotExpr.generate_memory_endblocks(cr);                
+
+                cr.endblock(); // end else-if WORKLIST ladder
+
+                elseladder = "else if";
+            }
+        }
+
+        cr2.outputline("else");
+        cr2.startblock();
+        cr2.outputline("printf(\"VERY BAD !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\\n\\n\");");
+        cr2.outputline("exit(1);");
+        cr2.endblock();
+
+        // end block created for worklist
+        cr2.endblock();
+
+    }
+
+    private void generate_checks() {
+
+        /* do constraint checks */
+        Vector constraints = state.vConstraints;
+
+        for (int i = 0; i < constraints.size(); i++) {
+
+            Constraint constraint = (Constraint) constraints.elementAt(i); 
+
+            {
+
+                final SymbolTable st = constraint.getSymbolTable();
+                
+                CodeWriter cr = new StandardCodeWriter(outputrepair) {
+                        public SymbolTable getSymbolTable() { return st; }
+                    };
+                
+                cr.outputline("// checking " + constraint.getLabel());
+                cr.startblock();
+
+                ListIterator quantifiers = constraint.quantifiers();
+
+                while (quantifiers.hasNext()) {
+                    Quantifier quantifier = (Quantifier) quantifiers.next();                   
+                    quantifier.generate_open(cr);
+                }            
+
+                cr.outputline("int maybe = 0;");
+                        
+                /* now we have to generate the guard test */
+        
+                VarDescriptor constraintboolean = VarDescriptor.makeNew("constraintboolean");
+                constraint.getLogicStatement().generate(cr, constraintboolean);
+                
+                cr.outputline("if (maybe)");
+                cr.startblock();
+                cr.outputline("__Success = 0;");
+                cr.outputline("printf(\"maybe fail " + (i+1) + ". \");");
+                cr.outputline("exit(1);");
+                cr.endblock();
+
+                cr.outputline("else if (!" + constraintboolean.getSafeSymbol() + ")");
+                cr.startblock();
+
+                cr.outputline("__Success = 0;");
+                cr.outputline("printf(\"fail " + (i+1) + ". \");");
+                cr.outputline("exit(1);");
+                cr.endblock();
+
+                while (quantifiers.hasPrevious()) {
+                    Quantifier quantifier = (Quantifier) quantifiers.previous();
+                    cr.endblock();
+                }
+
+                cr.endblock();
+                cr.outputline("");
+                cr.outputline("");
+            }
+            
+        }
+
+        outputrepair.println("// if (__Success) { printf(\"all tests passed\"); }");
+    }    
+
+}
+
+
+
index 806b3f8085bd5bb0876a7fcfec8604fd8598ad0c..4cfa2a885274afde3cf888c387779024623c611d 100755 (executable)
@@ -13,7 +13,7 @@ public class Rule implements Quantifiers {
     Inclusion inclusion = null;    
     SymbolTable st = new SymbolTable();
     DNFRule dnfguard=null,dnfnegguard=null;
     Inclusion inclusion = null;    
     SymbolTable st = new SymbolTable();
     DNFRule dnfguard=null,dnfnegguard=null;
-
+    boolean nogenerate=false;
     String label;
     
     int num;
     String label;
     
     int num;
@@ -23,6 +23,14 @@ public class Rule implements Quantifiers {
         label = new String("rule" + count++);
     }
     
         label = new String("rule" + count++);
     }
     
+    public void setnogenerate() {
+       nogenerate=true;
+    }
+
+    public boolean getnogenerate() {
+       return nogenerate;
+    }
+    
     public String toString() {
        String name="";
        for(int i=0;i<numQuantifiers();i++) {
     public String toString() {
        String name="";
        for(int i=0;i<numQuantifiers();i++) {
@@ -125,5 +133,4 @@ public class Rule implements Quantifiers {
         
         return SetDescriptor.expand(topdescriptors);
     }
         
         return SetDescriptor.expand(topdescriptors);
     }
-
 }
 }
index 2b42ac2b12cf92182b0cd9a1c89b5d2d1fe549a8..767167e6d92cc8059760e370ed7c77488f66400f 100755 (executable)
@@ -33,7 +33,7 @@ public class SetDescriptor extends Descriptor {
         }
 
         expanded.addAll(descriptors);
         }
 
         expanded.addAll(descriptors);
-        return expanded;        
+        return expanded;
     }
 
     public boolean isPartition() {
     }
 
     public boolean isPartition() {
index 9d375728d8db7266e4ded5463d57c9b8dc3849e3..f80c63116045c619663688ad1dcf103f1a94e319 100755 (executable)
@@ -1,5 +1,5 @@
 package MCC.IR;
 package MCC.IR;
-
+import MCC.Compiler;
 import java.util.*;
 
 public class SetInclusion extends Inclusion {
 import java.util.*;
 
 public class SetInclusion extends Inclusion {
@@ -64,10 +64,9 @@ public class SetInclusion extends Inclusion {
         writer.outputline("int " + addeditem + " = 1;");
 
         if (dostore) {
         writer.outputline("int " + addeditem + " = 1;");
 
         if (dostore) {
-        
-            writer.outputline(addeditem + " = " + set.getSafeSymbol() + "_hash->add((int)" + vd.getSafeSymbol() 
+           writer.outputline(addeditem + " = " + set.getSafeSymbol() + "_hash->add((int)" + vd.getSafeSymbol() 
                               +  ", (int)" + vd.getSafeSymbol() + ");");
                               +  ", (int)" + vd.getSafeSymbol() + ");");
-
+           
             if (SetInclusion.worklist) {
                 writer.outputline("if (" + addeditem + ")");
                 writer.startblock(); {                
             if (SetInclusion.worklist) {
                 writer.outputline("if (" + addeditem + ")");
                 writer.startblock(); {                
@@ -75,7 +74,14 @@ public class SetInclusion extends Inclusion {
                 }
                 writer.endblock();
             }
                 }
                 writer.endblock();
             }
-
+            if (Compiler.REPAIR) {
+                writer.outputline("if (" + addeditem + ")");
+                writer.startblock(); {                
+                    Repair.generate_dispatch(writer, set, vd.getSafeSymbol());
+                }
+                writer.endblock();
+            }
+           
         }
         
     }
         }
         
     }
index a9fd29c5d6c8d3f5ddcfe55d977902959b42308d..7296606a1da912945afa51978a528bd6157d167b 100755 (executable)
@@ -88,7 +88,7 @@ public class StructureTypeDescriptor extends TypeDescriptor {
             size = new OpExpr(Opcode.ADD, fieldsize, size);
         }
         
             size = new OpExpr(Opcode.ADD, fieldsize, size);
         }
         
-        return size;        
+        return size;
     }
 
     public Iterator getFields() {
     }
 
     public Iterator getFields() {
index b788acc3ac8937242cd905b7a216dbe8ff5778f5..ff5985fcefb81b24caafe0c254552203dd7de80d 100755 (executable)
@@ -66,6 +66,12 @@ public class Termination {
            System.out.println(mun.toString());
        }
        GraphAnalysis ga=new GraphAnalysis(this);
            System.out.println(mun.toString());
        }
        GraphAnalysis ga=new GraphAnalysis(this);
+       Set toremove=ga.doAnalysis();
+       System.out.println("Removing:");
+       for(Iterator it=toremove.iterator();it.hasNext();) {
+           GraphNode gn=(GraphNode)it.next();
+           System.out.println(gn.getTextLabel());
+       }
     }
     
     void generateconjunctionnodes() {
     }
     
     void generateconjunctionnodes() {
index 9f907a918e14f965b40dc525c61467923903349e..024aed37ec7aa0a555c5f001e983a23bf73e0a0b 100755 (executable)
@@ -33,7 +33,7 @@ public class State {
 
     public Hashtable rulenodes;
     public Hashtable constraintnodes;    
 
     public Hashtable rulenodes;
     public Hashtable constraintnodes;    
-
+    public Hashtable implicitrule;
     State() {
         vConstraints = null;
         vRules = null;
     State() {
         vConstraints = null;
         vRules = null;
@@ -47,6 +47,7 @@ public class State {
         ptModel = null;
         ptConstraints = null;
         ptSpace = null;
         ptModel = null;
         ptConstraints = null;
         ptSpace = null;
+       implicitrule=new Hashtable();
     }
 
     void printall() {
     }
 
     void printall() {