Added improvements to ImplicitSchema analysis, bug fixes to ImplicitSchema
authorbdemsky <bdemsky>
Thu, 29 Apr 2004 04:47:36 +0000 (04:47 +0000)
committerbdemsky <bdemsky>
Thu, 29 Apr 2004 04:47:36 +0000 (04:47 +0000)
and SetAnalysis, added edges for abstract repairs.

Repair/RepairCompiler/MCC/IR/ArrayAnalysis.java
Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
Repair/RepairCompiler/MCC/IR/RepairGenerator.java
Repair/RepairCompiler/MCC/IR/SetAnalysis.java
Repair/RepairCompiler/MCC/IR/Termination.java
Repair/RepairCompiler/MCC/IR/UpdateNode.java
Repair/RepairCompiler/MCC/IR/Updates.java

index 670cd79..ca142f7 100755 (executable)
@@ -53,7 +53,7 @@ public class ArrayAnalysis {
                if (oldap==null) {
                    set.put(si.getSet(),newap);
                } else {
-                   if (!oldap.equals(newap))
+                   if (!oldap.equal(newap))
                        set.put(si.getSet(),AccessPath.NONE);
                }
            } else if (inc instanceof RelationInclusion) {
@@ -64,7 +64,7 @@ public class ArrayAnalysis {
                if (oldapl==null) {
                    leftrelation.put(ri.getRelation(),newapl);
                } else {
-                   if (!oldapl.equals(newapl))
+                   if (!oldapl.equal(newapl))
                        leftrelation.put(ri.getRelation(),AccessPath.NONE);
                }
 
@@ -73,7 +73,7 @@ public class ArrayAnalysis {
                if (oldapr==null) {
                    rightrelation.put(ri.getRelation(),newapr);
                } else {
-                   if (!oldapr.equals(newapr))
+                   if (!oldapr.equal(newapr))
                        rightrelation.put(ri.getRelation(),AccessPath.NONE);
                }
            } else throw new Error();
@@ -83,12 +83,22 @@ public class ArrayAnalysis {
     public AccessPath analyzeExpr(Rule r,Expr e) {
        Vector dotvector=new Vector();
        Expr ptr=e;
+       while (ptr instanceof CastExpr)
+           ptr=((CastExpr)ptr).getExpr();
+
        while(true) {
-           if (!(ptr instanceof DotExpr))
-               return AccessPath.NONE; /* Does something other than a dereference */
+           /* Does something other than a dereference? */
+
+           if (!(ptr instanceof DotExpr)) {
+               return AccessPath.NONE; 
+           }
+
            DotExpr de=(DotExpr)ptr;
            dotvector.add(de);
            ptr=de.left;
+           while (ptr instanceof CastExpr)
+               ptr=((CastExpr)ptr).getExpr();
+
            if (ptr instanceof VarExpr) {
                VarExpr ve=(VarExpr)ptr;
                VarDescriptor vd=ve.getVar();
@@ -105,13 +115,14 @@ public class ArrayAnalysis {
                            if (size==1) {
                                ap.startSet(sd);
                                break;
-                           } else
+                           } else {
                                return AccessPath.NONE;
-                           
+                           }
                        }
                    }
-                   if (!ap.setStart)
+                   if (!ap.setStart) {
                        return AccessPath.NONE;
+                   }
                }
                /* Starting point finished - parse dereferences */
                boolean foundarray=false;
@@ -120,11 +131,13 @@ public class ArrayAnalysis {
                    FieldDescriptor fd=de2.getField();
                    if (fd instanceof ArrayDescriptor) {
                        foundarray=true;
-                       if (((ArrayDescriptor)fd).getField().getPtr())
+                       if (((ArrayDescriptor)fd).getField().getPtr()) {
                            return AccessPath.NONE;
+                       }
                    } else {
-                       if (foundarray&&fd.getPtr())
+                       if (foundarray&&fd.getPtr()) {
                            return AccessPath.NONE;
+                       }
                    }
                    ap.addField(fd);
                }
@@ -143,6 +156,7 @@ public class ArrayAnalysis {
        SetDescriptor startset;
        VarDescriptor startvar;
 
+
        public void startSet(SetDescriptor sd) {
            this.startset=sd;
            setStart=true;
@@ -158,6 +172,28 @@ public class ArrayAnalysis {
        public void addField(FieldDescriptor fd) {
            path.add(fd);
        }
+
+       public int numFields() {
+           return path.size();
+       }
+
+       public FieldDescriptor getField(int i) {
+           return (FieldDescriptor)path.get(i);
+       }
+
+       public String toString() {
+           String st="";
+           if (setStart)
+               st+=this.startset;
+           else
+               st+=this.startvar;
+
+           for(int i=0;i<numFields();i++) {
+               st+="."+getField(i);
+           }
+           return st;
+       }
+
        public boolean equal(AccessPath ap) {
            if (this==ap)
                return true;
index 4e34613..dc66ecd 100755 (executable)
@@ -118,14 +118,12 @@ public class ImplicitSchema {
        SetInclusion sinc2=(SetInclusion)inc2;
        if (sinc2.getSet()!=sd)
            return false;
-       if (r1.numQuantifiers()!=r2.numQuantifiers())
-           return false; 
+
        /* Construct a mapping between quantifiers */
        int[] mapping=new int[r2.numQuantifiers()];
        HashMap map=new HashMap();
        for(int i=0;i<r1.numQuantifiers();i++) {
            Quantifier q1=r1.getQuantifier(i);
-           boolean foundmapping=false;
            for (int j=0;j<r2.numQuantifiers();j++) {
                if (mapping[j]==1)
                    continue; /* Its already used */
@@ -134,7 +132,6 @@ public class ImplicitSchema {
                    ((SetQuantifier)q1).getSet()==((SetQuantifier)q2).getSet()) {
                    mapping[j]=1;
                    map.put(((SetQuantifier)q1).getVar(),((SetQuantifier)q2).getVar());
-                   foundmapping=true;
                    break;
                }
                if (q1 instanceof RelationQuantifier && q2 instanceof RelationQuantifier &&
@@ -142,17 +139,28 @@ public class ImplicitSchema {
                    mapping[j]=1;
                    map.put(((RelationQuantifier)q1).x,((RelationQuantifier)q2).x);
                    map.put(((RelationQuantifier)q1).y,((RelationQuantifier)q2).y);
-                   foundmapping=true;
                    break;
                }
+               if (q1 instanceof ForQuantifier && q2 instanceof ForQuantifier &&
+                   ((ForQuantifier)q1).lower.equals(map,((ForQuantifier)q2).lower)&&
+                   ((ForQuantifier)q1).upper.equals(map,((ForQuantifier)q2).upper)) {
+                   mapping[j]=1;
+                   map.put(((ForQuantifier)q1).getVar(),((ForQuantifier)q2).getVar());
+               }
            }
-           if (!foundmapping)
+       }
+
+       /* Make sure all bindings in the set rule are bound */
+       for (int i=0;i<r2.numQuantifiers();i++) {
+           if (mapping[i]!=1)
                return false;
        }
+
        /* Built mapping */
        Expr sexpr=sinc2.getExpr();
        if (!expr.equals(map,sexpr))
            return false;  /* This rule doesn't add the right thing */
+
        DNFRule drule1=r1.getDNFGuardExpr();
        DNFRule drule2=r2.getDNFGuardExpr();
        for (int i=0;i<drule1.size();i++) {
@@ -161,7 +169,7 @@ public class ImplicitSchema {
            for (int j=0;j<drule2.size();j++) {
                RuleConjunction rconj2=drule2.get(j);
                /* Need to show than rconj2 is true if rconj1 is true */
-               if (implication(map,rconj1,rconj2)) {
+               if (implication(map,rconj1,rconj2,sinc2)) {
                    foundmatch=true;
                    break;
                }
@@ -172,10 +180,18 @@ public class ImplicitSchema {
        return true;
     }
 
-    boolean implication(HashMap map, RuleConjunction rc1, RuleConjunction rc2) {
+    boolean implication(HashMap map, RuleConjunction rc1, RuleConjunction rc2,SetInclusion si) {
        for(int i=0;i<rc2.size();i++) {
            /* Check that rc1 has all predicates that rc2 has */
            DNFExpr de2=rc2.get(i);
+           /* Predicates for objects that aren't in set */
+           if (de2.getNegation()&&
+               (de2.getExpr() instanceof ElementOfExpr)) {
+               ElementOfExpr eoe=(ElementOfExpr)de2.getExpr();
+               if (si.getSet().isSubset(eoe.set)&&
+                   si.getExpr().equals(null,eoe.element))
+                   continue; /* This predicate isn't a problem */
+           }
            boolean havematch=false;
            for(int j=0;j<rc1.size();j++) {
                DNFExpr de1=rc1.get(i);
index 71ff6ed..456ef87 100755 (executable)
@@ -25,7 +25,6 @@ public class RepairGenerator {
     HashSet togenerate;
     static boolean DEBUG=false;
     Cost cost;
-    Sources sources;
     ModelRuleDependence mrd;
 
     public RepairGenerator(State state, Termination t) {
@@ -40,7 +39,6 @@ public class RepairGenerator {
            togenerate.removeAll(removed);
         GraphNode.computeclosure(togenerate,removed);
        cost=new Cost();
-       sources=new Sources(state);
        mrd=ModelRuleDependence.doAnalysis(state);
        Repair.repairgenerator=this;
     }
@@ -1103,9 +1101,9 @@ public class RepairGenerator {
            if (d instanceof RelationDescriptor) {
                VarDescriptor otherside=((ImageSetExpr)((SizeofExpr)((OpExpr)ep.expr).left).setexpr).vd;
                RelationDescriptor rd=(RelationDescriptor)d;
-               if (sources.relsetSource(rd,!ep.inverted())) {
+               if (termination.sources.relsetSource(rd,!ep.inverted())) {
                    /* Set Source */
-                   SetDescriptor sd=sources.relgetSourceSet(rd,!ep.inverted());
+                   SetDescriptor sd=termination.sources.relgetSourceSet(rd,!ep.inverted());
                    VarDescriptor iterator=VarDescriptor.makeNew("iterator");
                    cr.outputline(sd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
                    cr.outputline("for("+iterator.getSafeSymbol()+"="+sd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)");
@@ -1118,9 +1116,9 @@ public class RepairGenerator {
                    cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
                    cr.outputline(iterator.getSafeSymbol()+"->next();");
                    cr.endblock();
-               } else if (sources.relallocSource(rd,!ep.inverted())) {
+               } else if (termination.sources.relallocSource(rd,!ep.inverted())) {
                    /* Allocation Source*/
-                   sources.relgenerateSourceAlloc(cr,newobject,rd,!ep.inverted());
+                   termination.sources.relgenerateSourceAlloc(cr,newobject,rd,!ep.inverted());
                } else throw new Error("No source for adding to Relation");
                if (ep.inverted()) {
                    boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
@@ -1146,10 +1144,10 @@ public class RepairGenerator {
                }
            } else {
                SetDescriptor sd=(SetDescriptor)d;
-               if (sources.setSource(sd)) {
+               if (termination.sources.setSource(sd)) {
                    /* Set Source */
                    /* Set Source */
-                   SetDescriptor sourcesd=sources.getSourceSet(sd);
+                   SetDescriptor sourcesd=termination.sources.getSourceSet(sd);
                    VarDescriptor iterator=VarDescriptor.makeNew("iterator");
                    cr.outputline(sourcesd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
                    cr.outputline("for("+iterator.getSafeSymbol()+"="+sourcesd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)");
@@ -1158,9 +1156,9 @@ public class RepairGenerator {
                    cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
                    cr.outputline(iterator.getSafeSymbol()+"->next();");
                    cr.endblock();
-               } else if (sources.allocSource(sd)) {
+               } else if (termination.sources.allocSource(sd)) {
                    /* Allocation Source*/
-                   sources.generateSourceAlloc(cr,newobject,sd);
+                   termination.sources.generateSourceAlloc(cr,newobject,sd);
                } else throw new Error("No source for adding to Set");
                cr.outputline(sd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
                UpdateNode un=munadd.getUpdate(0);
index 7717ca6..1f91029 100755 (executable)
@@ -21,11 +21,11 @@ public class SetAnalysis {
     }
 
     public boolean isSubset(SetDescriptor set1, SetDescriptor set2) {
-       return subset.contains(set1)&&((Set)subset.get(set1)).contains(set2);
+       return subset.containsKey(set1)&&((Set)subset.get(set1)).contains(set2);
     }
 
     public boolean noIntersection(SetDescriptor set1, SetDescriptor set2) {
-       return intersection.contains(set1)&&((Set)intersection.get(set1)).contains(set2);
+       return intersection.containsKey(set1)&&((Set)intersection.get(set1)).contains(set2);
     }
     
     void doanalysis() {
@@ -35,17 +35,27 @@ public class SetAnalysis {
            SetDescriptor sd=(SetDescriptor)descriptors.get(i);
            Stack st=new Stack();
            st.addAll(sd.getSubsets());
+
+           if (!subset.containsKey(sd))
+               subset.put(sd,new HashSet());
+           ((HashSet)subset.get(sd)).addAll(sd.getSubsets());
+           for(Iterator it=sd.getSubsets().iterator();it.hasNext();) {
+               SetDescriptor sd2=(SetDescriptor)it.next();
+               if (!superset.containsKey(sd2))
+                   superset.put(sd2,new HashSet());
+               ((HashSet)superset.get(sd2)).add(sd);
+           }
+
            while(!st.empty()) {
                SetDescriptor subsetsd=(SetDescriptor)st.pop();
-               System.out.print(subsetsd.toString());
 
                st.addAll(subsetsd.getSubsets());
-               if (!subset.contains(sd))
+               if (!subset.containsKey(sd))
                    subset.put(sd,new HashSet());
                ((HashSet)subset.get(sd)).addAll(subsetsd.getSubsets());
                for(Iterator it=subsetsd.getSubsets().iterator();it.hasNext();) {
                    SetDescriptor sd2=(SetDescriptor)it.next();
-                   if (!superset.contains(sd2))
+                   if (!superset.containsKey(sd2))
                        superset.put(sd2,new HashSet());
                    ((HashSet)superset.get(sd2)).add(sd);
                }
@@ -63,7 +73,7 @@ public class SetAnalysis {
                            for(Iterator it3=sd1.allSubsets().iterator();it3.hasNext();) {
                                SetDescriptor sd3=(SetDescriptor)it3.next();
                                
-                               if (!intersection.contains(sd3))
+                               if (!intersection.containsKey(sd3))
                                    intersection.put(sd3,new HashSet());
                                ((HashSet)intersection.get(sd3)).addAll(sd2.allSubsets());
                            }
index 751ff99..465675c 100755 (executable)
@@ -29,6 +29,7 @@ public class Termination {
     ConstraintDependence constraintdependence;
     ExactSize exactsize;
     ArrayAnalysis arrayanalysis;
+    Sources sources;
 
     public Termination(State state) {
        this.state=state;
@@ -48,13 +49,14 @@ public class Termination {
        predtoabstractmap=new Hashtable();
        if (!Compiler.REPAIR)
            return;
-
+       
 
        for(int i=0;i<state.vRules.size();i++)
            System.out.println(state.vRules.get(i));
        for(int i=0;i<state.vConstraints.size();i++)
            System.out.println(state.vConstraints.get(i));
 
+       sources=new Sources(state);
        maxsize=new ComputeMaxSize(state);
        exactsize=new ExactSize(state);
        arrayanalysis=new ArrayAnalysis(state,this);
@@ -119,9 +121,11 @@ public class Termination {
     }
 
 
-    /** This method generates a node for each conjunction in the DNF form of each constraint. 
-     * It also converts the quantifiers into conjunctions also - constraints can be satisfied by
-     * removing items from the sets and relations they are quantified over */
+    /** This method generates a node for each conjunction in the DNF
+     * form of each constraint.  It also converts the quantifiers into
+     * conjunctions also - constraints can be satisfied by removing
+     * items from the sets and relations they are quantified over */
+
     void generateconjunctionnodes() {
        Vector constraints=state.vConstraints;
        // Constructs conjunction nodes
@@ -186,6 +190,40 @@ public class Termination {
            GraphNode gn=(GraphNode)updateiterator.next();
            TermNode tn=(TermNode)gn.getOwner();
            MultUpdateNode mun=tn.getUpdate();
+           for(int i=0;i<mun.numUpdates();i++) {
+               UpdateNode un=mun.getUpdate(i);
+               for(int j=0;j<mun.numUpdates();j++) {
+                   Updates u=un.getUpdate(j);
+                   if (u.getType()==Updates.ABSTRACT) {
+                       Expr e=u.getLeftExpr();
+                       boolean negated=u.negate;
+                       if (e instanceof TupleOfExpr) {
+                           TupleOfExpr toe=(TupleOfExpr)e;
+                           if (negated) {
+                               GraphNode agn=(GraphNode)abstractremove.get(toe.relation);
+                               GraphNode.Edge edge=new GraphNode.Edge("requires",agn);
+                               gn.addEdge(edge);
+                           } else {
+                               GraphNode agn=(GraphNode)abstractadd.get(toe.relation);
+                               GraphNode.Edge edge=new GraphNode.Edge("requires",agn);
+                               gn.addEdge(edge);
+                           }
+                       } else if (e instanceof ElementOfExpr) {
+                           ElementOfExpr eoe=(ElementOfExpr)e;
+                           if (negated) {
+                               GraphNode agn=(GraphNode)abstractremove.get(eoe.set);
+                               GraphNode.Edge edge=new GraphNode.Edge("requires",agn);
+                               gn.addEdge(edge);
+                           } else {
+                               GraphNode agn=(GraphNode)abstractadd.get(eoe.set);
+                               GraphNode.Edge edge=new GraphNode.Edge("requires",agn);
+                               gn.addEdge(edge);
+                           }
+                       } else throw new Error("Unrecognized Abstract Update");
+                   }
+               }
+           }
+
            /* Cycle through the rules to look for possible conflicts */
            for(int i=0;i<state.vRules.size();i++) {
                Rule r=(Rule) state.vRules.get(i);  
@@ -237,6 +275,37 @@ public class Termination {
            }
        }
     }
+
+    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("SatisfyRule"+i,tnsatisfy);
+           ConsequenceNode cnsatisfy=new ConsequenceNode();
+           TermNode ctnsatisfy=new TermNode(cnsatisfy);
+           GraphNode cgnsatisfy=new GraphNode("ConseqSatisfyRule"+i,ctnsatisfy);
+           consequence.put(satisfy,cgnsatisfy);
+           GraphNode.Edge esat=new GraphNode.Edge("consequencesatisfy"+i,cgnsatisfy);
+           gnsatisfy.addEdge(esat);
+           consequencenodes.add(cgnsatisfy);
+           scopesatisfy.put(r,gnsatisfy);
+           scopenodes.add(gnsatisfy);
+
+           ScopeNode falsify=new ScopeNode(r,false);
+           TermNode tnfalsify=new TermNode(falsify);
+           GraphNode gnfalsify=new GraphNode("FalsifyRule"+i,tnfalsify);
+           ConsequenceNode cnfalsify=new ConsequenceNode();
+           TermNode ctnfalsify=new TermNode(cnfalsify);
+           GraphNode cgnfalsify=new GraphNode("ConseqFalsifyRule"+i,ctnfalsify);
+           consequence.put(falsify,cgnfalsify);
+           GraphNode.Edge efals=new GraphNode.Edge("consequencefalsify"+i,cgnfalsify);
+           gnfalsify.addEdge(efals);
+           consequencenodes.add(cgnfalsify);
+           scopefalsify.put(r,gnfalsify);
+           scopenodes.add(gnfalsify);
+       }
+    }
     
     void generatescopeedges() {
        for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
@@ -310,10 +379,8 @@ public class Termination {
        for(int i=0;i<setdescriptors.size();i++) {
            SetDescriptor sd=(SetDescriptor)setdescriptors.get(i);
 
-           /* XXXXXXX: Not sure what to do here */
            VarExpr ve=new VarExpr("DUMMY");
            InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sd));
-           
            DNFPredicate tp=new DNFPredicate(false,ip);
            AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTOSET, sd);
            TermNode tn=new TermNode(ar);
@@ -340,8 +407,6 @@ public class Termination {
        Vector relationdescriptors=state.stRelations.getAllDescriptors();
        for(int i=0;i<relationdescriptors.size();i++) {
            RelationDescriptor rd=(RelationDescriptor)relationdescriptors.get(i);
-
-           /* XXXXXXX: Not sure what to do here */
            VarDescriptor vd1=new VarDescriptor("DUMMY1");
            VarExpr ve2=new VarExpr("DUMMY2");
 
@@ -369,7 +434,6 @@ public class Termination {
            abstractrepairadd.add(gn2);
            abstractremove.put(rd,gn2);
        }
-       
     }
 
     int compensationcount=0;
@@ -377,11 +441,7 @@ public class Termination {
        for(int i=0;i<state.vRules.size();i++) {
            Rule r=(Rule) state.vRules.get(i);
            Vector possiblerules=new Vector();
-           /* Construct bindings */
-           /* No need to construct bindings on remove
-              Vector bindings=new Vector();
-              constructbindings(bindings, r,true);
-           */
+
            for(int j=0;j<(r.numQuantifiers()+r.getDNFNegGuardExpr().size());j++) {
                GraphNode gn=(GraphNode)scopesatisfy.get(r);
                TermNode tn=(TermNode) gn.getOwner();
@@ -390,8 +450,7 @@ public class Termination {
                TermNode tn2=new TermNode(mun);
                GraphNode gn2=new GraphNode("CompRem"+compensationcount,tn2);
                UpdateNode un=new UpdateNode(r);
-               //              un.addBindings(bindings);
-               // Not necessary
+
                if (j<r.numQuantifiers()) {
                    /* Remove quantifier */
                    Quantifier q=r.getQuantifier(j);
@@ -425,6 +484,7 @@ public class Termination {
                        continue;
                    }
                } else {
+                   /* Negate conjunction */
                    int c=j-r.numQuantifiers();
                    if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
                        continue;
@@ -434,7 +494,6 @@ public class Termination {
                    continue;
                
                mun.addUpdate(un);
-
                GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
                compensationcount++;
                gn.addEdge(e);
@@ -466,8 +525,14 @@ public class Termination {
        }
     }
 
+
+    /** This method generates concrete data structure updates which
+     * remove an object (or tuple) from a set (or relation).*/
+
     int removefromcount=0;
     void generateremovefromsetrelation(GraphNode gn,AbstractRepair ar) {
+       /* Construct the set of all rules which could add something to the given set or relation */
+
        Vector possiblerules=new Vector();
        for(int i=0;i<state.vRules.size();i++) {
            Rule r=(Rule) state.vRules.get(i);
@@ -480,6 +545,8 @@ public class Termination {
        }
        if (possiblerules.size()==0)
            return;
+       
+       /* Loop through different ways of falsifying each of these rules */
        int[] count=new int[possiblerules.size()];
        while(remains(count,possiblerules,true)) {
            MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.REMOVE);
@@ -490,11 +557,7 @@ public class Termination {
            for(int i=0;i<possiblerules.size();i++) {
                Rule r=(Rule)possiblerules.get(i);
                UpdateNode un=new UpdateNode(r);
-               /* Construct bindings */
-               /* No Need to construct bindings on remove
-                  Vector bindings=new Vector();
-                  constructbindings(bindings, r,true);
-                 un.addBindings(bindings);*/
+
                if (count[i]<r.numQuantifiers()) {
                    /* Remove quantifier */
                    Quantifier q=r.getQuantifier(count[i]);
@@ -547,6 +610,8 @@ public class Termination {
        }
     }
 
+    /** This method increments to the next possibility. */
+
     static private void increment(int count[], Vector rules,boolean isremove) {
        count[0]++;
        for(int i=0;i<(rules.size()-1);i++) {
@@ -558,6 +623,9 @@ public class Termination {
        }
     }
 
+
+    /** This method test if there remain any possibilities to loop
+     * through. */
     static private boolean remains(int count[], Vector rules, boolean isremove) {
        for(int i=0;i<rules.size();i++) {
            int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
@@ -570,6 +638,7 @@ public class Termination {
 
     /** This method generates data structure updates to implement the
      *         abstract atomic modification specified by ar. */
+
     int modifycount=0;
     void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {
        RelationDescriptor rd=(RelationDescriptor)ar.getDescriptor();
@@ -582,7 +651,7 @@ public class Termination {
        else 
            rightindex=2;
 
-
+       // construct set of possible rules
        Vector possiblerules=new Vector();
        for(int i=0;i<state.vRules.size();i++) {
            Rule r=(Rule) state.vRules.get(i);
@@ -592,6 +661,8 @@ public class Termination {
        }
        if (possiblerules.size()==0)
            return;
+
+       // increment through this set
        int[] count=new int[possiblerules.size()];
        while(remains(count,possiblerules,false)) {
            MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.MODIFY);
@@ -602,7 +673,6 @@ public class Termination {
            for(int i=0;i<possiblerules.size();i++) {
                Rule r=(Rule)possiblerules.get(i);
                UpdateNode un=new UpdateNode(r);
-               /* No Need to construct bindings on modify */
                
                int c=count[i];
                if (!processconjunction(un,r.getDNFGuardExpr().get(c))) {
@@ -653,6 +723,175 @@ public class Termination {
            increment(count,possiblerules,false);
        }
     }
+
+    /** Generate concrete data structure update to add an object(or
+     * tuple) to a set (or relation). */
+
+    static int addtocount=0;
+    void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) {
+       for(int i=0;i<state.vRules.size();i++) {
+           Rule r=(Rule) state.vRules.get(i);
+           /* See if this is a good rule*/
+           if ((r.getInclusion() instanceof SetInclusion&&
+                ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
+               (r.getInclusion() instanceof RelationInclusion&&
+                ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation())) {
+               
+               /* First solve for quantifiers */
+               Vector bindings=new Vector();
+               /* Construct bindings */
+               if (!constructbindings(bindings,r,false))
+                   continue;
+               //Generate add instruction
+               DNFRule dnfrule=r.getDNFGuardExpr();
+               for(int j=0;j<dnfrule.size();j++) {
+                   Inclusion inc=r.getInclusion();
+                   UpdateNode un=new UpdateNode(r);
+                   un.addBindings(bindings);
+                   /* Now build update for tuple/set inclusion condition */
+                   if(inc instanceof SetInclusion) {
+                       SetInclusion si=(SetInclusion)inc;
+                       if (!(si.elementexpr instanceof VarExpr)) {
+                           if (si.elementexpr.isValue()) {
+                               Updates up=new Updates(si.elementexpr,0);
+                               un.addUpdate(up);
+                           } else {
+                               /* We're an add to set*/
+                               System.out.println("Rule: "+r);
+                               ArrayAnalysis.AccessPath rap=arrayanalysis.analyzeExpr(r,si.elementexpr);
+                               System.out.println("Attempting perform array add");
+                               SetDescriptor set=sources.setSource(si.getSet())?
+                                   sources.getSourceSet(si.getSet()):null;
+                               if (set==null)
+                                   continue;
+                               System.out.println("Non-null source set");
+                               ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
+                               if (rap==ArrayAnalysis.AccessPath.NONE)
+                                   continue;
+                               System.out.println("A");
+                               if (!rap.equal(ap))
+                                   continue;
+                               System.out.println("B");
+                               if (!constructarrayupdate(un, si.elementexpr, rap, 0))
+                                   continue;
+                               System.out.println("C");
+                           }
+                       } else {
+                           VarDescriptor vd=((VarExpr)si.elementexpr).getVar();
+                           if (vd.isGlobal()) {
+                               Updates up=new Updates(si.elementexpr,0);
+                               un.addUpdate(up);
+                           }
+                       }
+                   } else if (inc instanceof RelationInclusion) {
+                       RelationInclusion ri=(RelationInclusion)inc;
+                       if (!(ri.getLeftExpr() instanceof VarExpr)) {
+                           if (ri.getLeftExpr().isValue()) {
+                               Updates up=new Updates(ri.getLeftExpr(),0);
+                               un.addUpdate(up);
+                           } else {
+                               /* We don't handly relation modifies */
+                               if (ar.getType()==AbstractRepair.MODIFYRELATION)
+                                   continue;
+                               /* We're an add to relation*/
+                               ArrayAnalysis.AccessPath rap=arrayanalysis.analyzeExpr(r,ri.getLeftExpr());
+                               SetDescriptor set=sources.relsetSource(ri.getRelation(),true /* Domain*/)?
+                                   sources.relgetSourceSet(ri.getRelation(),true):null;
+                               if (set==null)
+                                   continue;
+                               ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
+                               
+                               if (rap==ArrayAnalysis.AccessPath.NONE||
+                                   !rap.equal(ap)||
+                                   !constructarrayupdate(un, ri.getLeftExpr(), rap, 0))
+                                   continue;
+                           }
+                       } else {
+                           VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
+                           if (vd.isGlobal()) {
+                               Updates up=new Updates(ri.getLeftExpr(),0);
+                               un.addUpdate(up);
+                           }
+                       }
+                       if (!(ri.getRightExpr() instanceof VarExpr)) {
+                           if (ri.getRightExpr().isValue()) {
+                               Updates up=new Updates(ri.getRightExpr(),1);
+                               un.addUpdate(up);
+                           } else {
+                               /* We don't handly relation modifies */
+                               if (ar.getType()==AbstractRepair.MODIFYRELATION)
+                                   continue;
+                               /* We're an add to relation*/
+                               ArrayAnalysis.AccessPath rap=arrayanalysis.analyzeExpr(r,ri.getRightExpr());
+                               SetDescriptor set=sources.relsetSource(ri.getRelation(),false /* Range*/)?
+                                   sources.relgetSourceSet(ri.getRelation(),false):null;
+                               if (set==null)
+                                   continue;
+                               ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
+                               
+                               if (rap==ArrayAnalysis.AccessPath.NONE||
+                                   !rap.equal(ap)||
+                                   !constructarrayupdate(un, ri.getRightExpr(), rap, 1))
+                                   continue;
+                           }
+                       } else {
+                           VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
+                           if (vd.isGlobal()) {
+                               Updates up=new Updates(ri.getRightExpr(),1);
+                               un.addUpdate(up);
+                           }
+                       }
+                   }
+                   //Finally build necessary updates to satisfy conjunction
+                   RuleConjunction ruleconj=dnfrule.get(j);
+
+                   /* Add in updates for quantifiers */
+                   MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.ADD);
+                   TermNode tn=new TermNode(mun);
+                   GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
+
+                   if (processquantifiers(gn2,un, r)&&
+                       processconjunction(un,ruleconj)&&
+                       un.checkupdates()) {
+                       mun.addUpdate(un);
+                       GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
+                       addtocount++;
+                       gn.addEdge(e);
+                       updatenodes.add(gn2);
+                   }
+               }
+           }
+       }
+    }
+
+    boolean constructarrayupdate(UpdateNode un, Expr lexpr, ArrayAnalysis.AccessPath ap, int slotnumber) {
+       System.out.println("Constructing array update");
+       Expr e=null;
+       for (int i=ap.numFields()-1;i>=0;i--) {
+           if (e==null)
+               e=lexpr;
+           else 
+               e=((DotExpr)e).getExpr();
+
+           while (e instanceof CastExpr)
+               e=((CastExpr)e).getExpr();
+
+           DotExpr de=(DotExpr)e;
+           FieldDescriptor fd=ap.getField(i);
+           if (fd instanceof ArrayDescriptor) {
+               // We have an ArrayDescriptor!
+               Expr index=de.getIndex();
+               if (!index.isValue()) {/* Not assignable */
+                   System.out.println("ERROR:Index is assignable");
+                   return false;
+               }
+               Updates updates=new Updates(index,i,ap,slotnumber);
+               un.addUpdate(updates);
+           }
+       }
+       return true;
+    }
+
     /** This method constructs bindings for an update using rule
      * r. The boolean flag isremoval indicates that the update
      * performs a removal.  The function returns true if it is able to
@@ -763,94 +1002,6 @@ public class Termination {
        }
        return goodupdate;
     }
-
-    static int addtocount=0;
-    void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) {
-       for(int i=0;i<state.vRules.size();i++) {
-           Rule r=(Rule) state.vRules.get(i);
-           /* See if this is a good rule*/
-           if ((r.getInclusion() instanceof SetInclusion&&
-                ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
-               (r.getInclusion() instanceof RelationInclusion&&
-                ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation())) {
-               
-               /* First solve for quantifiers */
-               Vector bindings=new Vector();
-               /* Construct bindings */
-               if (!constructbindings(bindings,r,false))
-                   continue;
-               //Generate add instruction
-               DNFRule dnfrule=r.getDNFGuardExpr();
-               for(int j=0;j<dnfrule.size();j++) {
-                   Inclusion inc=r.getInclusion();
-                   UpdateNode un=new UpdateNode(r);
-                   un.addBindings(bindings);
-                   /* Now build update for tuple/set inclusion condition */
-                   if(inc instanceof SetInclusion) {
-                       SetInclusion si=(SetInclusion)inc;
-                       if (!(si.elementexpr instanceof VarExpr)) {
-                           if (si.elementexpr.isValue()) {
-                               Updates up=new Updates(si.elementexpr,0);
-                               un.addUpdate(up);
-                           } else
-                               continue;
-                       } else {
-                           VarDescriptor vd=((VarExpr)si.elementexpr).getVar();
-                           if (vd.isGlobal()) {
-                               Updates up=new Updates(si.elementexpr,0);
-                               un.addUpdate(up);
-                           }
-                       }
-                   } else if (inc instanceof RelationInclusion) {
-                       RelationInclusion ri=(RelationInclusion)inc;
-                       if (!(ri.getLeftExpr() instanceof VarExpr)) {
-                           if (ri.getLeftExpr().isValue()) {
-                               Updates up=new Updates(ri.getLeftExpr(),0);
-                               un.addUpdate(up);
-                           } else
-                               continue;
-                       } else {
-                           VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
-                           if (vd.isGlobal()) {
-                               Updates up=new Updates(ri.getLeftExpr(),0);
-                               un.addUpdate(up);
-                           }
-                       }
-                       if (!(ri.getRightExpr() instanceof VarExpr)) {
-                           if (ri.getRightExpr().isValue()) {
-                               Updates up=new Updates(ri.getRightExpr(),1);
-                               un.addUpdate(up);
-                           } else
-                               continue;
-                       } else {
-                           VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
-                           if (vd.isGlobal()) {
-                               Updates up=new Updates(ri.getRightExpr(),1);
-                               un.addUpdate(up);
-                           }
-                       }
-                   }
-                   //Finally build necessary updates to satisfy conjunction
-                   RuleConjunction ruleconj=dnfrule.get(j);
-
-                   /* Add in updates for quantifiers */
-                   MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.ADD);
-                   TermNode tn=new TermNode(mun);
-                   GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
-
-                   if (processquantifiers(gn2,un, r)&&
-                       processconjunction(un,ruleconj)&&
-                       un.checkupdates()) {
-                       mun.addUpdate(un);
-                       GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
-                       addtocount++;
-                       gn.addEdge(e);
-                       updatenodes.add(gn2);
-                   }
-               }
-           }
-       }
-    }
     
     /** Adds updates that add an item to the appropriate set or
      * relation quantified over by the model definition rule.. */
@@ -900,6 +1051,9 @@ public class Termination {
        return true;
     }
 
+    /** This method generates the necessary updates to satisfy the
+     * conjunction ruleconj. */
+
     boolean  processconjunction(UpdateNode un,RuleConjunction ruleconj){
        boolean okay=true;
        for(int k=0;k<ruleconj.size();k++) {
@@ -931,35 +1085,4 @@ public class Termination {
        }
        return okay;
     }
-
-    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("SatisfyRule"+i,tnsatisfy);
-           ConsequenceNode cnsatisfy=new ConsequenceNode();
-           TermNode ctnsatisfy=new TermNode(cnsatisfy);
-           GraphNode cgnsatisfy=new GraphNode("ConseqSatisfyRule"+i,ctnsatisfy);
-           consequence.put(satisfy,cgnsatisfy);
-           GraphNode.Edge esat=new GraphNode.Edge("consequencesatisfy"+i,cgnsatisfy);
-           gnsatisfy.addEdge(esat);
-           consequencenodes.add(cgnsatisfy);
-           scopesatisfy.put(r,gnsatisfy);
-           scopenodes.add(gnsatisfy);
-
-           ScopeNode falsify=new ScopeNode(r,false);
-           TermNode tnfalsify=new TermNode(falsify);
-           GraphNode gnfalsify=new GraphNode("FalsifyRule"+i,tnfalsify);
-           ConsequenceNode cnfalsify=new ConsequenceNode();
-           TermNode ctnfalsify=new TermNode(cnfalsify);
-           GraphNode cgnfalsify=new GraphNode("ConseqFalsifyRule"+i,ctnfalsify);
-           consequence.put(falsify,cgnfalsify);
-           GraphNode.Edge efals=new GraphNode.Edge("consequencefalsify"+i,cgnfalsify);
-           gnfalsify.addEdge(efals);
-           consequencenodes.add(cgnfalsify);
-           scopefalsify.put(r,gnfalsify);
-           scopenodes.add(gnfalsify);
-       }
-    }
 }
index e50b63f..7c0e5a4 100755 (executable)
@@ -340,6 +340,7 @@ class UpdateNode {
                u.getRightExpr().generate(cr,right);
                break;
            case Updates.POSITION:
+           case Updates.ACCESSPATH:
                if (u.getRightPos()==0)
                    cr.outputline("int "+right.getSafeSymbol()+"="+slot0+";");
                else if (u.getRightPos()==1)
@@ -351,6 +352,12 @@ class UpdateNode {
            default:
                throw new Error();
            }
+
+           if (u.getType()==Updates.ACCESSPATH) {
+               VarDescriptor newright=VarDescriptor.makeNew("right");
+               /* Need to do the modulo computation here...FIXME */
+               right=newright;
+           }
            VarDescriptor left=VarDescriptor.makeNew("left");
            u.getLeftExpr().generate(cr,left);
            Opcode op=u.getOpcode();
index 684dfc8..99694cd 100755 (executable)
@@ -3,23 +3,26 @@ package MCC.IR;
 class Updates {
     static public final int EXPR=0;
     static public final int POSITION=1;
-    static public final int ABSTRACT=2;
+    static public final int ACCESSPATH=2;
+    static public final int ABSTRACT=3;
+
     int type=-1;
     int rightposition;
     Expr rightexpr;
     Expr leftexpr;
     Opcode opcode;
     boolean negate=false;
+    ArrayAnalysis.AccessPath ap;
+    int fieldnum;
 
-    public String toString() {
-       if (type==EXPR)
-           return leftexpr.name()+opcode.toString()+rightexpr.name();
-       else if (type==POSITION)
-           return leftexpr.name()+opcode.toString()+"Position("+String.valueOf(rightposition)+")";
-       else if (type==ABSTRACT) {
-           if (negate) return "!"+leftexpr.name();
-           else return leftexpr.name();
-       } else throw new Error("Unrecognized type");
+    public Updates(Expr lexpr, int fieldnum, ArrayAnalysis.AccessPath ap, int slot) {
+       this.leftexpr=lexpr;
+       this.fieldnum=fieldnum;
+       this.ap=ap;
+       this.rightposition=slot;
+
+       this.type=Updates.ACCESSPATH;
+       this.opcode=Opcode.EQ;
     }
 
     public Updates(Expr lexpr, Expr rexpr, Opcode op, boolean negate) {
@@ -34,10 +37,29 @@ class Updates {
        rightexpr=rexpr;
     }
 
-    boolean isGlobal() {
-       if (leftexpr instanceof VarExpr)
-           return true;
-       else return false;
+    public Updates(Expr lexpr, Expr rexpr) {
+       if (!lexpr.isValue())
+           System.out.println("Building invalid update");
+       leftexpr=lexpr;
+       rightexpr=rexpr;
+       type=Updates.EXPR;
+       opcode=Opcode.EQ;
+    }
+
+    public Updates(Expr lexpr, int rpos) {
+       if (!lexpr.isValue())
+           System.out.println("Building invalid update");
+       leftexpr=lexpr;
+       rightposition=rpos;
+       type=Updates.POSITION;
+       opcode=Opcode.EQ;
+    }
+
+    public Updates(Expr lexpr,boolean negates) {
+       leftexpr=lexpr;
+       type=Updates.ABSTRACT;
+       negate=negates;
+       opcode=null;
     }
 
     VarDescriptor getVar() {
@@ -71,6 +93,12 @@ class Updates {
        }
     }
 
+    boolean isGlobal() {
+       if (leftexpr instanceof VarExpr)
+           return true;
+       else return false;
+    }
+
     boolean isField() {
        if (leftexpr instanceof DotExpr) {
            assert ((DotExpr)leftexpr).getIndex()==null;
@@ -88,47 +116,48 @@ class Updates {
        return opcode;
     }
 
-    public Updates(Expr lexpr, Expr rexpr) {
-       if (!lexpr.isValue())
-           System.out.println("Building invalid update");
-       leftexpr=lexpr;
-       rightexpr=rexpr;
-       type=Updates.EXPR;
-       opcode=Opcode.EQ;
-    }
-
-    public Updates(Expr lexpr, int rpos) {
-       if (!lexpr.isValue())
-           System.out.println("Building invalid update");
-       leftexpr=lexpr;
-       rightposition=rpos;
-       type=Updates.POSITION;
-       opcode=Opcode.EQ;
-    }
-
     boolean isAbstract() {
        return type==Updates.ABSTRACT;
     }
 
-    public Updates(Expr lexpr,boolean negates) {
-       leftexpr=lexpr;
-       type=Updates.ABSTRACT;
-       negate=negates;
-       opcode=null;
-    }
-
     public int getType() {
        return type;
     }
+
     public Expr getLeftExpr() {
        return leftexpr;
     }
+
     public int getRightPos() {
-       assert type==Updates.POSITION;
+       assert type==Updates.POSITION||type==Updates.ACCESSPATH;
        return rightposition;
     }
+
     public Expr getRightExpr() {
        assert type==Updates.EXPR;
        return rightexpr;
     }
+
+    public int getFieldNum() {
+       assert type==Updates.ACCESSPATH;
+       return fieldnum;
+    }
+
+    public ArrayAnalysis.AccessPath getAccessPath() {
+       assert type==Updates.ACCESSPATH;
+       return ap;
+    }
+
+    public String toString() {
+       if (type==EXPR)
+           return leftexpr.name()+opcode.toString()+rightexpr.name();
+       else if (type==POSITION)
+           return leftexpr.name()+opcode.toString()+"Position("+String.valueOf(rightposition)+")";
+       else if (type==ACCESSPATH) {
+           return leftexpr.name()+opcode.toString()+"Field("+fieldnum+","+ap+") of Position("+String.valueOf(rightposition)+")";
+       } else if (type==ABSTRACT) {
+           if (negate) return "!"+leftexpr.name();
+           else return leftexpr.name();
+       } else throw new Error("Unrecognized type");
+    }
 }