+
+ /** 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;
+ }
+
projects / repair.git / commitdiff