updates
authorbdemsky <bdemsky>
Mon, 22 Dec 2003 01:28:34 +0000 (01:28 +0000)
committerbdemsky <bdemsky>
Mon, 22 Dec 2003 01:28:34 +0000 (01:28 +0000)
13 files changed:
Repair/RepairCompiler/MCC/Compiler.java
Repair/RepairCompiler/MCC/IR/DNFPredicate.java
Repair/RepairCompiler/MCC/IR/Expr.java
Repair/RepairCompiler/MCC/IR/ExprPredicate.java
Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
Repair/RepairCompiler/MCC/IR/OpExpr.java
Repair/RepairCompiler/MCC/IR/Predicate.java
Repair/RepairCompiler/MCC/IR/RelationExpr.java
Repair/RepairCompiler/MCC/IR/RelationFunctionExpr.java
Repair/RepairCompiler/MCC/IR/SetExpr.java
Repair/RepairCompiler/MCC/IR/SizeofExpr.java
Repair/RepairCompiler/MCC/IR/Termination.java

index 8f90540..e87c112 100755 (executable)
@@ -54,9 +54,10 @@ public class Compiler {
            success = parse(state) || error(state, "Parsing failed, not attempting semantic analysis.");
            success = semantics(state) || error(state, "Semantic analysis failed, not attempting variable initialization.");
 
-           if (REPAIR)
+           if (REPAIR) {
                (new ImplicitSchema(state)).update();
-
+               Termination t=new Termination(state);
+           }
             
             (new DependencyBuilder(state)).calculate();
             
index 2328bfc..a1e5a65 100755 (executable)
@@ -18,4 +18,8 @@ public class DNFPredicate {
     void negatePred() {
        negate=!negate;
     }
+
+    boolean isNegated() {
+       return negate;
+    }
 }
index cd82227..310e5ae 100755 (executable)
@@ -29,4 +29,20 @@ public abstract class Expr {
        return new DNFRule(this);
     }
 
+    public Descriptor getDescriptor() {
+       return null;
+    }
+
+    public int[] getRepairs(boolean negated) {
+       return new int[0];
+    }
+
+    public boolean inverted() {
+       return false;
+    }
+
+    public boolean usesDescriptor(RelationDescriptor rd) {
+       return false;
+    }
+
 }
index 3242de1..43ac5ad 100755 (executable)
@@ -3,14 +3,33 @@ package MCC.IR;
 import java.util.*;
 
 public class ExprPredicate extends Predicate {
-
+    
     Expr expr;
 
+
+    public static final int SIZE=1;
+    public static final int COMPARISON=2;
+
+    public int getType() {
+       if (((OpExpr)expr).left instanceof SizeofExpr)
+           return SIZE;
+       else if (((OpExpr)expr).left instanceof RelationExpr)
+           return COMPARISON;
+       else throw new Error("Unidentifiable Type");
+    }
+
+    public Opcode getOp() {
+       return ((OpExpr)expr).opcode;
+    }
+
+    public int leftsize() {
+       return ((IntegerLiteralExpr)((OpExpr)expr).right).getValue();
+    }
+
     public ExprPredicate(Expr expr) {
         if (expr == null) {
             throw new NullPointerException();
         }
-
         this.expr = expr;
     }
 
@@ -18,6 +37,22 @@ public class ExprPredicate extends Predicate {
         return expr.getInversedRelations();
     }
 
+    public int[] getRepairs(boolean negated) {
+       return expr.getRepairs(negated);
+    }
+
+    public Descriptor getDescriptor() {
+       return expr.getDescriptor();
+    }
+
+    public boolean inverted() {
+       return expr.inverted();
+    }
+
+    public boolean usesDescriptor(RelationDescriptor rd) {
+       return expr.usesDescriptor(rd);
+    }
+
     public Set getRequiredDescriptors() {
         return expr.getRequiredDescriptors();
     }
@@ -25,9 +60,5 @@ public class ExprPredicate extends Predicate {
     public void generate(CodeWriter writer, VarDescriptor dest) {
         expr.generate(writer, dest);
     }
-
-    public int[] getRepairs(boolean negated) {
-       return new int[] {};
-    }
 }
     
index c7f5079..66437e3 100755 (executable)
@@ -22,6 +22,10 @@ public class ImageSetExpr extends SetExpr {
         this.inverse = inverse;
     }
 
+    public boolean inverted() {
+       return inverse;
+    }
+
     public VarDescriptor getVar() {
         return vd;
     }
@@ -30,6 +34,14 @@ public class ImageSetExpr extends SetExpr {
         return rd;
     }
 
+    public Descriptor getDescriptor() {
+       return rd;
+    }
+
+    public boolean usesDescriptor(RelationDescriptor rd) {
+       return (rd==this.rd);
+    }
+
     public Set getInversedRelations() {
         HashSet set = new HashSet();
         if (inverse) {
index 26b9f4a..e0d0d77 100755 (executable)
@@ -7,6 +7,11 @@ public class InclusionPredicate extends Predicate {
     Expr expr;
     SetExpr setexpr;
 
+    public boolean inverted() {
+       return setexpr.inverted();
+    }
+
+
     public InclusionPredicate(Expr expr, SetExpr setexpr) {
         if (expr == null) {
             throw new NullPointerException();
@@ -41,6 +46,13 @@ public class InclusionPredicate extends Predicate {
         //return set;
     }
 
+    public Descriptor getDescriptor() {
+       if (setexpr instanceof ImageSetExpr) {
+           return ((ImageSetExpr)setexpr).getRelation();
+       } else
+           return setexpr.sd;
+    }
+
     public int[] getRepairs(boolean negated) {
        if (setexpr instanceof ImageSetExpr) {
            if (negated)
@@ -56,3 +68,4 @@ public class InclusionPredicate extends Predicate {
     }
 }
     
+
index b576cbd..47a6fae 100755 (executable)
@@ -31,7 +31,50 @@ public class OpExpr extends Expr {
         } else throw new Error();
     }
 
+    public boolean usesDescriptor(RelationDescriptor rd) {
+       if (opcode==Opcode.GT||opcode==Opcode.GE||opcode==Opcode.LT||
+           opcode==Opcode.LE||opcode==Opcode.EQ||opcode==Opcode.NE)
+           return right.usesDescriptor(rd);
+       else
+           return left.usesDescriptor(rd)||(right!=null&&right.usesDescriptor(rd));
+    }
+    
+    public int[] getRepairs(boolean negated) {
+       if (left instanceof RelationExpr)
+           return new int[] {AbstractRepair.MODIFYRELATION};
+       if (left instanceof SizeofExpr) {
+           boolean isRelation=((SizeofExpr)left).setexpr instanceof ImageSetExpr;
+           if (isRelation) {
+               if (opcode==Opcode.EQ)
+                   return new int[] {AbstractRepair.ADDTORELATION,
+                                         AbstractRepair.REMOVEFROMRELATION};
+               if (((opcode==Opcode.GE)&&!negated)||
+                   ((opcode==Opcode.LE)&&negated))
+                   return new int[]{AbstractRepair.ADDTORELATION};
+               else
+                   return new int[]{AbstractRepair.REMOVEFROMRELATION};
+           } else {
+               if (opcode==Opcode.EQ)
+                   return new int[] {AbstractRepair.ADDTOSET,
+                                         AbstractRepair.REMOVEFROMSET};
+               
+               if (((opcode==Opcode.GE)&&!negated)||
+                   ((opcode==Opcode.LE)&&negated))
+                   return new int[] {AbstractRepair.ADDTOSET};
+               else
+                   return new int[] {AbstractRepair.REMOVEFROMSET};
+           }
+       }
+       throw new Error("BAD");
+    }
+    
+    public Descriptor getDescriptor() {
+       return left.getDescriptor();
+    }
 
+    public boolean inverted() {
+       return left.inverted();
+    }
 
     public Set getInversedRelations() {
         Set set = left.getInversedRelations();
index 7ab2179..cb9aa39 100755 (executable)
@@ -7,6 +7,10 @@ public abstract class Predicate extends LogicStatement {
     public DNFConstraint constructDNF() {
        return new DNFConstraint(this);
     }
-    public int[] getRepairs(boolean negated) {}
+    abstract public int[] getRepairs(boolean negated);
+    abstract public Descriptor getDescriptor();
+    abstract public boolean inverted();
+    public boolean usesDescriptor(RelationDescriptor rd) {
+       return false;}
 }
     
index 5a541f5..fc2a4c7 100755 (executable)
@@ -17,11 +17,26 @@ public class RelationExpr extends Expr {
     public Expr getExpr() {
         return expr;
     }
+
+    public boolean usesDescriptor(RelationDescriptor rd) {
+       if (rd==relation)
+           return true;
+       else
+           return expr.usesDescriptor(rd);
+    }
     
     public RelationDescriptor getRelation() {
         return relation;
     }
 
+    public Descriptor getDescriptor() {
+        return relation;
+    }
+
+    public boolean inverted() {
+        return inverse;
+    }
+
     public Set getInversedRelations() {
         Set set = expr.getInversedRelations();
         if (inverse) {
index bb4050f..cfbde5d 100755 (executable)
@@ -17,6 +17,10 @@ public class RelationFunctionExpr extends Expr {
         this.rule = rule;
     }
 
+    public Descriptor getDescriptor() {
+       return relation;
+    }
+
     public RelationDescriptor getRelation() {
         return relation;
     }
@@ -31,6 +35,13 @@ public class RelationFunctionExpr extends Expr {
         return v;
     }
 
+    public boolean usesDescriptor(RelationDescriptor rd) {
+       if (rd==relation)
+           return true;
+       else
+           return expr.usesDescriptor(rd);
+    }
+
     public void generate(CodeWriter cr, VarDescriptor dest) {
         
         String destname = dest.getSafeSymbol();
index b2a37cf..b084b8e 100755 (executable)
@@ -18,6 +18,10 @@ public class SetExpr extends Expr {
         return new HashSet();
     }
 
+    public Descriptor getDescriptor() {
+       return sd;
+    }
+
     public Set getRequiredDescriptors() {
         HashSet v = new HashSet();
         v.add(sd);
index 09d37e4..3d7f9ac 100755 (executable)
@@ -14,6 +14,19 @@ public class SizeofExpr extends Expr {
         this.setexpr = setexpr;
     }
 
+    public boolean usesDescriptor(RelationDescriptor rd) {
+       return setexpr.usesDescriptor(rd);
+    }
+
+
+    public Descriptor getDescriptor() {
+       return setexpr.getDescriptor();
+    }
+
+    public boolean inverted() {
+       return setexpr.inverted();
+    }
+
     public SetExpr getSetExpr() {
         return setexpr;
     }
index 14d144a..7f9adc0 100755 (executable)
@@ -1,18 +1,33 @@
 package MCC.IR;
 import java.util.*;
+import MCC.State;
 
-class Termination {
+public class Termination {
     HashSet conjunctions;
     Hashtable conjunctionmap;
 
     HashSet abstractrepair;
 
+    HashSet scopenodes;
+    Hashtable scopesatisfy;
+    Hashtable scopefalsify;
+
     State state;
 
     public Termination(State state) {
        this.state=state;
+       conjunctions=new HashSet();
+       conjunctionmap=new Hashtable();
+       abstractrepair=new HashSet();
+       scopenodes=new HashSet();
+       scopesatisfy=new Hashtable();
+       scopefalsify=new Hashtable();
+
        generateconjunctionnodes();
        generaterepairnodes();
+       generateabstractedges();
+       generatedatastructureupdatenodes();
+       generatescopenodes();
     }
     
     void generateconjunctionnodes() {
@@ -29,6 +44,29 @@ class Termination {
        }
     }
 
+    void generateabstractedges() {
+       for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
+           GraphNode gn=(GraphNode)absiterator.next();
+           TermNode tn=(TermNode)gn.getOwner();
+           AbstractRepair ar=(AbstractRepair)tn.getAbstract();
+       
+           for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
+               GraphNode gn2=(GraphNode)conjiterator.next();
+               TermNode tn2=(TermNode)gn2.getOwner();
+               Conjunction conj=tn2.getConjunction();
+               for(int i=0;i<conj.size();i++) {
+                   DNFPredicate dp=conj.get(i);
+                   if (AbstractInterferes.interferes(ar,dp)) {
+                       GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
+                       gn.addEdge(e);
+                       break;
+                   }
+               }
+           }
+       }
+    }
+    
+
     void generaterepairnodes() {
        for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
            GraphNode gn=(GraphNode)conjiterator.next();
@@ -36,58 +74,66 @@ class Termination {
            Conjunction conj=tn.getConjunction();
            for(int i=0;i<conj.size();i++) {
                DNFPredicate dp=conj.get(i);
-               int[] array=dp.getPredicate().getRepairs();
-               for {int j=0;j<array.length;j++) {
-                   AbstractRepair ar=new AbstractRepair(dp,array[j]);
-                   TermNode tn=new TermNode(ar);
-                   GraphNode gn2=new GraphNode(gn.getLabel()+"-"+i+","+j,tn);
-                   Edge e=new Edge("abstract",gn2);
+               int[] array=dp.getPredicate().getRepairs(dp.isNegated());
+               Descriptor d=dp.getPredicate().getDescriptor();
+               for(int j=0;j<array.length;j++) {
+                   AbstractRepair ar=new AbstractRepair(dp,array[j],d);
+                   TermNode tn2=new TermNode(ar);
+                   GraphNode gn2=new GraphNode(gn.getLabel()+"-"+i+","+j,tn2);
+                   GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
                    gn.addEdge(e);
                    abstractrepair.add(gn2);
                }
            }
        }
     }
-}
-
-class AbstractRepair {
-    public final static int ADDTOSET=1;
-    public final static int REMOVEFROMSET=2;
-    public final static int ADDTORELATION=3;
-    public final static int REMOVEFROMRELATION=4;
-    public final static int MODIFYRELATION=5;
 
-    DNFPredicate torepair;
-    int type;
-
-    public AbstractRepair(DNFPredicate dp,int typ) {
-       torepair=dp;
-       type=typ;
+    void generatedatastructureupdatenodes() {
+       for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
+           GraphNode gn=(GraphNode)absiterator.next();
+           TermNode tn=(TermNode) gn.getOwner();
+           AbstractRepair ar=tn.getAbstract();
+           if (ar.getType()==AbstractRepair.ADDTOSET) {
+               generateaddtoset(ar);
+           } else if (ar.getType()==AbstractRepair.REMOVEFROMSET) {
+               generateremovefromset(ar);
+           } else if (ar.getType()==AbstractRepair.ADDTORELATION) {
+               generateaddtorelation(ar);
+           } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
+               generateremovefromrelation(ar);
+           } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
+               generatemodifyrelation(ar);
+           }
+       }
     }
-}
-
-class TermNode {
-    public final static int CONJUNCTION=1;
-    public final static int ABSTRACT=2;
 
-    Constraint constr;
-    Conjunction conj;
-    int type;
-    AbstractRepair repair;
+    void generateaddtoset(AbstractRepair ar) {
+       for(int i=0;i<state.vRules.size();i++) {
+           Rule r=(Rule) state.vRules.get(i);
+           if (r.getInclusion() instanceof SetInclusion) {
+               if (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()) {
+                   //Generate add instruction
+                   
 
-    public TermNode(Constraint constr, Conjunction conj) {
-       this.constr=constr;
-       this.conj=conj;
-       type=CONJUNCTION;
+               }
+           }
+       }
     }
 
-    public TermNode(AbstractRepair ar) {
-       repair=ar;
-       type=ABSTRACT;
-    }
+    void generatescopenodes() {
+       for(int i=0;i<state.vRules.size();i++) {
+           Rule r=(Rule) state.vRules.get(i);
+           ScopeNode satisfy=new ScopeNode(r,true);
+           TermNode tnsatisfy=new TermNode(satisfy);
+           GraphNode gnsatisfy=new GraphNode("Satisfy Rule"+i,tnsatisfy);
 
-    public Conjunction getConjunction() {
-       return conj;
+           ScopeNode falsify=new ScopeNode(r,false);
+           TermNode tnfalsify=new TermNode(falsify);
+           GraphNode gnfalsify=new GraphNode("Falsify Rule"+i,tnfalsify);
+           scopesatisfy.put(r,gnsatisfy);
+           scopefalsify.put(r,gnfalsify);
+           scopenodes.add(gnsatisfy);
+           scopenodes.add(gnfalsify);
+       }
     }
 }
-