+ if (!constructbindings(bindings,r,ar,setmapping,false))
+ continue;
+ System.out.println("Bindings constructed");
+ //Generate add instruction
+ DNFRule dnfrule=r.getDNFGuardExpr();
+ endloop:
+ 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;
+ Expr e=si.elementexpr;
+
+ while(e instanceof CastExpr) {
+ CastExpr ce=(CastExpr)e;
+ if (ce.getType()!=si.getSet().getType())
+ continue endloop;
+ e=ce.getExpr();
+ }
+
+ if (!(e instanceof VarExpr)) {
+ if (e.isValue(si.getSet().getType())) {
+ Updates up=new Updates(e,0,si.getSet().getType());
+ un.addUpdate(up);
+ } else {
+ /* We're an add to set*/
+ ArrayAnalysis.AccessPath rap=arrayanalysis.analyzeExpr(r,e);
+ SetDescriptor set=sources.setSource(si.getSet())?
+ sources.getSourceSet(si.getSet()):null;
+ if (set==null)
+ continue;
+ ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
+ if (rap==ArrayAnalysis.AccessPath.NONE)
+ continue;
+ if (!rap.equal(ap))
+ continue;
+ if (!constructarrayupdate(un, e, rap, 0))
+ continue;
+ }
+ } else {
+ VarDescriptor vd=((VarExpr)e).getVar();
+ if (vd.isGlobal()) {
+ Updates up=new Updates(e,0,null);
+ un.addUpdate(up);
+ }
+ }
+ } else if (inc instanceof RelationInclusion) {
+ RelationInclusion ri=(RelationInclusion)inc;
+
+ Expr e=ri.getLeftExpr();
+
+ while(e instanceof CastExpr) {
+ CastExpr ce=(CastExpr)e;
+ if (ce.getType()!=ri.getRelation().getDomain().getType())
+ continue endloop;
+ e=ce.getExpr();
+ }
+ if (!(e instanceof VarExpr)) {
+ if (e.isValue(ri.getRelation().getDomain().getType())) {
+ Updates up=new Updates(e,0,ri.getRelation().getDomain().getType());
+ if (ar.getDomainSet()!=null)
+ setmapping.put(e,ar.getDomainSet());
+ 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,e);
+ 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, e, rap, 0))
+ continue;
+ if (ar.getDomainSet()!=null)
+ setmapping.put(e,ar.getDomainSet());
+
+ }
+ } else {
+ VarDescriptor vd=((VarExpr)e).getVar();
+ if (vd.isGlobal()) {
+ Updates up=new Updates(e,0,null);
+ if (ar.getDomainSet()!=null)
+ setmapping.put(e,ar.getDomainSet());
+ un.addUpdate(up);
+ }
+ }
+
+ e=ri.getRightExpr();
+
+ while(e instanceof CastExpr) {
+ CastExpr ce=(CastExpr)e;
+ if (ce.getType()!=ri.getRelation().getRange().getType())
+ continue endloop;
+ e=ce.getExpr();
+ }
+ if (!(e instanceof VarExpr)) {
+ if (e.isValue(ri.getRelation().getRange().getType())) {
+ Updates up=new Updates(e,1,ri.getRelation().getRange().getType());
+ 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,e);
+ 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, e, rap, 1))
+ continue;
+ if (ar.getRangeSet()!=null)
+ setmapping.put(e,ar.getRangeSet());
+ }
+ } else {
+ VarDescriptor vd=((VarExpr)e).getVar();
+ if (vd.isGlobal()) {
+ Updates up=new Updates(e,1,null);
+ if (ar.getRangeSet()!=null)
+ setmapping.put(e,ar.getRangeSet());
+ un.addUpdate(up);
+ }
+ }
+ }
+ System.out.println("Built inclusion condition updates.");
+ //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);
+ gn2.setOption(updateoption);
+
+ if (debugmsg("Start processing quantifiers")&&
+ processquantifiers(gn2,un, r,setmapping)&&
+ debugmsg("Finished processing quantifiers")&&
+ processconjunction(un,ruleconj,setmapping)&&
+ debugmsg("Finished processing conjunction")&&
+ un.checkupdates()&&
+ debugmsg("Updates checked")) {
+ mun.addUpdate(un);
+ GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
+ addtocount++;
+ gn.addEdge(e);
+ updatenodes.add(gn2);
+ }
+ }
+ }
+ }
+ }
+
+ boolean debugmsg(String st) {
+ System.out.println(st);
+ return true;
+ }
+
+ 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(null)) {/* Not assignable */
+ System.out.println("ERROR:Index isn't assignable");
+ return false;
+ }
+ Updates updates=new Updates(index,i,ap,lexpr,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
+ * generate a valid set of bindings and false otherwise. */
+
+ boolean constructbindings(Vector bindings, Rule r, AbstractRepair ar, Hashtable setmapping, boolean isremoval) {