*/
public class Compiler {
- public static boolean REPAIR=true;
+ public static boolean REPAIR=false;
public static void main(String[] args) {
State state = null;
success = parse(state) || error(state, "Parsing failed, not attempting semantic analysis.");
success = semantics(state) || error(state, "Semantic analysis failed, not attempting variable initialization.");
+ /* Check partition constraints */
+ (new ImplicitSchema(state)).update();
+
if (REPAIR) {
- (new ImplicitSchema(state)).update();
Termination t=new Termination(state);
}
-
+ state.printall();
(new DependencyBuilder(state)).calculate();
try {
return false;
}
}
- /* This if handles all the c comparisons in the paper */
+
+ if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
+ (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
+ (dp.getPredicate() instanceof ExprPredicate)&&
+ (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+ boolean neg2=dp.isNegated();
+ Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+ int size2=((ExprPredicate)dp.getPredicate()).leftsize();
+ if ((!neg2&&(op2==Opcode.EQ)&&(size2==0))||
+ (neg2&&(op2==Opcode.NE)&&(size2==0))||
+ (!neg2&&(op2==Opcode.GE))||
+ (!neg2&&(op2==Opcode.GT))||
+ (neg2&&(op2==Opcode.LE))||
+ (neg2&&(op2==Opcode.LT)))
+ return false;
+ }
+
+ /* This handles all the c comparisons in the paper */
if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
(ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
(ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
boolean neg2=dp.isNegated();
Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
int size2=((ExprPredicate)dp.getPredicate()).leftsize();
- if ((neg1&&((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE))||
- (!neg1&&((op1==Opcode.EQ)||(op1==Opcode.GT)||op1==Opcode.GE)||(op1==Opcode.NE))) {
+ if ((!neg1&&((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE))||
+ (neg1&&((op1==Opcode.EQ)||(op1==Opcode.GT)||op1==Opcode.GE)||(op1==Opcode.NE))) {
int size1a=0;
if (neg1) {
if((op1==Opcode.EQ)||(op1==Opcode.GE))
(neg2&&(op2==Opcode.LE)&&(size1a>size2))||
(neg2&&(op2==Opcode.LT)&&(size1a>=size2)))
return false;
- }
+ }
+ }
+
+ if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
+ (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
+ (dp.getPredicate() instanceof ExprPredicate)&&
+ (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+ boolean neg2=dp.isNegated();
+ Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+ int size2=((ExprPredicate)dp.getPredicate()).leftsize();
+ if ((!neg2&&(op2==Opcode.EQ)&&(size2==0))||
+ (neg2&&(op2==Opcode.NE)&&(size2==0))||
+ (neg2&&(op2==Opcode.GE))||
+ (neg2&&(op2==Opcode.GT))||
+ (!neg2&&(op2==Opcode.LE))||
+ (!neg2&&(op2==Opcode.LT)))
+ return false;
+
}
+ if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
+ (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
+ (dp.getPredicate() instanceof InclusionPredicate)&&
+ (dp.isNegated()==false))
+ return false; /* Could only satisfy this predicate */
+
+ if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
+ (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
+ (dp.getPredicate() instanceof InclusionPredicate)&&
+ (dp.isNegated()==true))
+ return false; /* Could only satisfy this predicate */
+
return true;
}
{
if ((!neg2&&(op2==Opcode.GE))||
(!neg2&&(op2==Opcode.GT))||
+ (neg2&&(op2==Opcode.EQ)&&(size2==0))||
+ (!neg2&&(op2==Opcode.NE)&&(size2==0))||
(neg2&&(op2==Opcode.LE))||
(neg2&&(op2==Opcode.LT)))
return false;
{
if ((neg2&&(op2==Opcode.GE))||
(neg2&&(op2==Opcode.GT))||
+ (!neg2&&(op2==Opcode.EQ)&&(size2==0))||
+ (neg2&&(op2==Opcode.NE)&&(size2==0))||
(!neg2&&(op2==Opcode.LE))||
(!neg2&&(op2==Opcode.LT)))
return false;
}
}
+ if ((des==dp.getPredicate().getDescriptor())&&
+ satisfy&&
+ (dp.getPredicate() instanceof InclusionPredicate)&&
+ (dp.isNegated()==false))
+ return false; /* Could only satisfy this predicate */
+
+ if ((des==dp.getPredicate().getDescriptor())&&
+ (!satisfy)&&
+ (dp.getPredicate() instanceof InclusionPredicate)&&
+ (dp.isNegated()==true))
+ return false; /* Could only satisfy this predicate */
+
return true;
}
- static public boolean interferes(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
+ static public boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
for(int i=0;i<r.numQuantifiers();i++) {
Quantifier q=r.getQuantifier(i);
if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
return true;
} else throw new Error("Unrecognized Quantifier");
}
+ return false;
+ }
+
+ static public boolean interferes(AbstractRepair ar, Quantifiers q) {
+ if (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)
+ return interferesquantifier(ar.getDescriptor(),true,q,true);
+ return false;
+ }
+
+ static public boolean interferes(Descriptor des, boolean satisfy, Quantifiers q) {
+ return interferesquantifier(des, satisfy, q,true);
+ }
+
+ static public boolean interferes(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
+ if (interferesquantifier(des,satisfy,r,satisfyrule))
+ return true;
/* Scan DNF form */
DNFRule drule=r.getDNFGuardExpr();
for(int i=0;i<drule.size();i++) {
this.expr = expr;
}
+ public String name() {
+ String str="";
+ str="(("+type.toString()+")"+expr.name()+")";
+ return str;
+ }
+
public boolean equals(Map remap, Expr e) {
if (e==null)
return false;
RuleConjunction rconj=drule.get(k);
for(int l=0;l<rconj.size();l++) {
DNFExpr dexpr=rconj.get(l);
- /* See if update interfers w/ dexpr */
+ /* See if update interferes w/ dexpr */
if (!dexpr.getExpr().usesDescriptor(updated_des))
continue; /* No use of the descriptor */
import java.util.*;
-public class Constraint {
+public class Constraint implements Quantifiers {
private static int count = 1;
label = new String("c" + count++);
}
+ public String toString() {
+ String name="";
+ for(int i=0;i<numQuantifiers();i++) {
+ name+=getQuantifier(i).toString()+",";
+ }
+ name+=logicstatement.name();
+ return name;
+ }
+
public int getNum() {
return num;
}
+ public int numQuantifiers() {
+ return quantifiers.size();
+ }
+
+ public Quantifier getQuantifier(int i) {
+ return (Quantifier) quantifiers.get(i);
+ }
+
public String getLabel() {
return label;
}
for (int i = 0; i < quantifiers.size(); i++) {
Quantifier q = (Quantifier) quantifiers.elementAt(i);
- topdescriptors.addAll(q.getRequiredDescriptors());
+ topdescriptors.addAll(q.getRequiredDescriptors());
}
return SetDescriptor.expand(topdescriptors);
}
public void calculate() {
-
- /* reinitialize (clear) nodes */
+ /* reinitialize (clear) nodes */
constraintnodes = new Hashtable();
rulenodes = new Hashtable();
edge.setDotNodeParameters("style=dotted");
otherrulenode.addEdge(edge);
}
- }
- }
+ }
+ }
}
/* store results in state */
}
public String name() {
+ System.out.println(this.getClass().getName());
return "?";
}
}
public String toString() {
- return "for quantifier " + var.getSymbol() + " = " + lower + " to " + upper;
+ return "for quantifier " + var.getSymbol() + " = " + lower.name() + " to " + upper.name();
}
public void generate_open(CodeWriter writer) {
return owner;
}
+ public static void computeclosure(Set nodes) {
+ Stack tovisit=new Stack();
+ tovisit.addAll(nodes);
+ while(!tovisit.isEmpty()) {
+ GraphNode gn=(GraphNode)tovisit.pop();
+ for(Iterator it=gn.edges();it.hasNext();) {
+ Edge edge=(Edge)it.next();
+ GraphNode target=edge.getTarget();
+ if (!nodes.contains(target)) {
+ nodes.add(target);
+ tovisit.push(target);
+ }
+ }
+ }
+ }
+
public void setDotNodeParameters(String param) {
if (param == null) {
throw new NullPointerException();
while (edges.hasNext()) {
Edge edge = (Edge) edges.next();
GraphNode node = edge.getTarget();
- String edgelabel = useEdgeLabels ? "label=\"" + edge.getLabel() + "\"" : "label=\"\"";
- output.println("\t" + gn.getLabel() + " -> " + node.getLabel() + " [" + edgelabel + edge.dotnodeparams + "];");
+ if (nodes.contains(node)) {
+ String edgelabel = useEdgeLabels ? "label=\"" + edge.getLabel() + "\"" : "label=\"\"";
+ output.println("\t" + gn.getLabel() + " -> " + node.getLabel() + " [" + edgelabel + edge.dotnodeparams + "];");
+ }
}
}
}
}
public void update() {
- updaterules();
+ // updaterules();
updateconstraints();
updaterelationconstraints();
}
+ boolean needDomain(RelationDescriptor rd) {
+ return needDR(rd, true);
+ }
+
+ boolean needDR(RelationDescriptor rd,boolean isdomain) {
+ Vector rules=state.vRules;
+ SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
+ for(int i=0;i<rules.size();i++) {
+ Rule r=(Rule)rules.get(i);
+ if ((r.numQuantifiers()==1)&&
+ (r.getQuantifier(0) instanceof RelationQuantifier)&&
+ (((RelationQuantifier)r.getQuantifier(0)).getRelation()==rd)&&
+ r.getInclusion().getTargetDescriptors().contains(sd)) {
+ SetInclusion rinc=(SetInclusion)r.getInclusion();
+ RelationQuantifier rq=(RelationQuantifier)r.getQuantifier(0);
+ VarDescriptor vd=isdomain?rq.x:rq.y;
+ if ((rinc.getExpr() instanceof VarExpr)&&
+ (((VarExpr)rinc.getExpr()).getVar()==vd)&&
+ (r.getGuardExpr() instanceof BooleanLiteralExpr)&&
+ (((BooleanLiteralExpr)r.getGuardExpr()).getValue()))
+ return false;
+ }
+ }
+
+
+ for(int i=0;i<rules.size();i++) {
+ Rule r=(Rule)rules.get(i);
+ Inclusion inc=r.getInclusion();
+ if (inc.getTargetDescriptors().contains(rd)) {
+ /* Need to check this rule */
+ boolean good=false;
+ RelationInclusion rinc=(RelationInclusion)inc;
+ Expr expr=isdomain?rinc.getLeftExpr():rinc.getRightExpr();
+ if (expr instanceof VarExpr) {
+ VarDescriptor vd=((VarExpr)expr).getVar();
+ assert vd!=null;
+ for (int j=0;j<r.numQuantifiers();j++) {
+ Quantifier q=r.getQuantifier(j);
+ if ((q instanceof SetQuantifier)&&
+ (((SetQuantifier)q).getVar()==vd)&&
+ (sd.allSubsets().contains(((SetQuantifier)q).getSet()))) {
+ good=true;
+ break;
+ }
+ if ((q instanceof RelationQuantifier)&&
+ (
+ ((((RelationQuantifier)q).x==vd)&&
+ (sd.allSubsets().contains(((RelationQuantifier)q).getRelation().getDomain())))
+ ||
+ ((((RelationQuantifier)q).y==vd)&&
+ (sd.allSubsets().contains(((RelationQuantifier)q).getRelation().getRange())))
+ )) {
+ good=true;
+ break;
+ }
+
+ }
+ if (good)
+ continue; /* Proved for this case */
+ }
+ for(int j=0;j<rules.size();j++) {
+ Rule r2=(Rule)rules.get(j);
+ Inclusion inc2=r2.getInclusion();
+
+ if (checkimplication(r,r2,isdomain)) {
+ good=true;
+ break;
+ }
+ }
+ if (good)
+ continue;
+
+ return true; /* Couldn't prove we didn't need */
+ }
+ }
+ return false;
+ }
+
+ boolean checkimplication(Rule r1, Rule r2, boolean isdomain) {
+ /* r1 is the relation */
+ /* See if this rule guarantees relation */
+ /* Steps:
+ 1. match up quantifiers
+ 2. check inclusion condition
+ 3. see if guard expr of set rule is more general */
+
+ RelationInclusion inc1=(RelationInclusion) r1.getInclusion();
+ RelationDescriptor rd=inc1.getRelation();
+ SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
+ Expr expr=isdomain?inc1.getLeftExpr():inc1.getRightExpr();
+
+ Inclusion inc2=r2.getInclusion();
+ if (!(inc2 instanceof SetInclusion))
+ return false;
+ 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 */
+ Quantifier q2=r2.getQuantifier(j);
+ if (q1 instanceof SetQuantifier && q2 instanceof SetQuantifier&&
+ ((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 &&
+ ((RelationQuantifier)q1).getRelation()==((RelationQuantifier)q2).getRelation()) {
+ mapping[j]=1;
+ map.put(((RelationQuantifier)q1).x,((RelationQuantifier)q2).x);
+ map.put(((RelationQuantifier)q1).y,((RelationQuantifier)q2).y);
+ foundmapping=true;
+ break;
+ }
+ }
+ if (!foundmapping)
+ 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++) {
+ RuleConjunction rconj1=drule1.get(i);
+ boolean foundmatch=false;
+ 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)) {
+ foundmatch=true;
+ break;
+ }
+ }
+ if (!foundmatch)
+ return false;
+ }
+ return true;
+ }
+
+ boolean implication(HashMap map, RuleConjunction rc1, RuleConjunction rc2) {
+ for(int i=0;i<rc2.size();i++) {
+ /* Check that rc1 has all predicates that rc2 has */
+ DNFExpr de2=rc2.get(i);
+ boolean havematch=false;
+ for(int j=0;j<rc1.size();j++) {
+ DNFExpr de1=rc1.get(i);
+ if (de1.getNegation()!=de2.getNegation())
+ continue;
+ if (de1.getExpr().equals(map,de2.getExpr())) {
+ havematch=true;
+ break;
+ }
+ }
+ if (!havematch)
+ return false;
+ }
+ return true;
+ }
+
+ boolean needRange(RelationDescriptor rd) {
+ return needDR(rd, false);
+ }
+
void updaterelationconstraints() {
Vector reldescriptors=state.stRelations.getAllDescriptors();
for(int i=0;i<reldescriptors.size();i++) {
RelationDescriptor rd=(RelationDescriptor) reldescriptors.get(i);
- Constraint c=new Constraint();
-
- /* Construct quantifier */
- RelationQuantifier rq=new RelationQuantifier();
- String varname1=new String("relationvar1");
- String varname2=new String("relationvar2");
- VarDescriptor var1=new VarDescriptor(varname1);
- VarDescriptor var2=new VarDescriptor(varname2);
- c.getSymbolTable().add(var1);
- c.getSymbolTable().add(var2);
- var1.setType(rd.getDomain().getType());
- var2.setType(rd.getRange().getType());
- rq.setTuple(var1,var2);
- rq.setRelation(rd);
- c.addQuantifier(rq);
- VarExpr ve1=new VarExpr(varname1);
- SetExpr se1=new SetExpr(rd.getDomain());
- LogicStatement incpred1=new InclusionPredicate(ve1,se1);
- VarExpr ve2=new VarExpr(varname2);
- SetExpr se2=new SetExpr(rd.getRange());
- LogicStatement incpred2=new InclusionPredicate(ve2,se2);
- c.setLogicStatement(new LogicStatement(LogicStatement.AND,incpred1,incpred2));
- state.vConstraints.add(c);
+ if (needDomain(rd)||needRange(rd)) {
+
+ Constraint c=new Constraint();
+ /* Construct quantifier */
+ LogicStatement ls=null;
+
+ RelationQuantifier rq=new RelationQuantifier();
+ String varname1=new String("relationvar1");
+ VarDescriptor var1=new VarDescriptor(varname1);
+ String varname2=new String("relationvar2");
+ VarDescriptor var2=new VarDescriptor(varname2);
+ rq.setTuple(var1,var2);
+ rq.setRelation(rd);
+ c.addQuantifier(rq);
+ c.getSymbolTable().add(var1);
+ c.getSymbolTable().add(var2);
+ var1.setType(rd.getDomain().getType());
+ var2.setType(rd.getRange().getType());
+
+ if (needDomain(rd)) {
+ VarExpr ve1=new VarExpr(var1);
+ SetExpr se1=new SetExpr(rd.getDomain());
+ se1.td=rd.getDomain().getType();
+ ls=new InclusionPredicate(ve1,se1);
+ }
+
+
+ if (needRange(rd)) {
+ VarExpr ve2=new VarExpr(var2);
+ SetExpr se2=new SetExpr(rd.getRange());
+ se2.td=rd.getRange().getType();
+ LogicStatement incpred2=new InclusionPredicate(ve2,se2);
+ if (ls==null) ls=incpred2;
+ else ls=new LogicStatement(LogicStatement.AND,ls,incpred2);
+ }
+ rd.addUsage(RelationDescriptor.IMAGE);
+
+ c.setLogicStatement(ls);
+ state.vConstraints.add(c);
+ }
}
}
for(int j=0;j<sd.getSubsets().size();j++) {
LogicStatement conj=null;
for(int k=0;k<sd.getSubsets().size();k++) {
- VarExpr ve=new VarExpr(varname);
+ VarExpr ve=new VarExpr(var);
SetExpr se=new SetExpr((SetDescriptor) sd.getSubsets().get(k));
+ se.td=sd.getType();
LogicStatement incpred=new InclusionPredicate(ve,se);
if (j!=k) {
incpred=new LogicStatement(LogicStatement.NOT ,incpred);
public static final Operation NOT = new Operation("NOT");
public String name() {
+ if (op==NOT)
+ return "!"+left.name();
String name=left.name();
- name+=op.toString();
+ name+=" "+op.toString()+" ";
if (right!=null)
name+=right.name();
return name;
class MultUpdateNode {
Vector updates;
AbstractRepair abstractrepair;
- public MultUpdateNode(AbstractRepair ar) {
+ ScopeNode scopenode;
+ int op;
+ static public final int ADD=0;
+ static public final int REMOVE=1;
+ static public final int MODIFY=2;
+
+ public MultUpdateNode(AbstractRepair ar, int op) {
updates=new Vector();
abstractrepair=ar;
+ this.op=op;
+ }
+
+ public MultUpdateNode(ScopeNode sn) {
+ updates=new Vector();
+ scopenode=sn;
}
void addUpdate(UpdateNode un) {
updates.add(un);
return opcode;
}
+
+
+
public boolean equals(Map remap, Expr e) {
if (e==null||!(e instanceof OpExpr))
return false;
public boolean usesDescriptor(Descriptor d) {
if (opcode==Opcode.GT||opcode==Opcode.GE||opcode==Opcode.LT||
opcode==Opcode.LE||opcode==Opcode.EQ||opcode==Opcode.NE)
- return right.usesDescriptor(d);
+ return left.usesDescriptor(d)||(right!=null&&right.usesDescriptor(d));
+ // return right.usesDescriptor(d);
else
return left.usesDescriptor(d)||(right!=null&&right.usesDescriptor(d));
}
+
public int[] getRepairs(boolean negated) {
if (left instanceof RelationExpr)
return new int[] {AbstractRepair.MODIFYRELATION};
boolean isRelation=((SizeofExpr)left).setexpr instanceof ImageSetExpr;
if (isRelation) {
if (opcode==Opcode.EQ)
- return new int[] {AbstractRepair.ADDTORELATION,
- AbstractRepair.REMOVEFROMRELATION};
+ if (((IntegerLiteralExpr)right).getValue()==0)
+ return new int[] {AbstractRepair.REMOVEFROMRELATION};
+ else
+ return new int[] {AbstractRepair.ADDTORELATION,
+ AbstractRepair.REMOVEFROMRELATION};
if (((opcode==Opcode.GE)&&!negated)||
- ((opcode==Opcode.LE)&&negated))
- return new int[]{AbstractRepair.ADDTORELATION};
+ ((opcode==Opcode.LE)&&negated)) {
+ if (((IntegerLiteralExpr)right).getValue()==0)
+ return new int[0];
+ else
+ return new int[]{AbstractRepair.ADDTORELATION}; }
else
return new int[]{AbstractRepair.REMOVEFROMRELATION};
} else {
if (opcode==Opcode.EQ)
- return new int[] {AbstractRepair.ADDTOSET,
- AbstractRepair.REMOVEFROMSET};
+ if (((IntegerLiteralExpr)right).getValue()==0)
+ return new int[] {AbstractRepair.REMOVEFROMSET};
+ else
+ return new int[] {AbstractRepair.ADDTOSET,
+ AbstractRepair.REMOVEFROMSET};
if (((opcode==Opcode.GE)&&!negated)||
- ((opcode==Opcode.LE)&&negated))
- return new int[] {AbstractRepair.ADDTOSET};
+ ((opcode==Opcode.LE)&&negated)) {
+ if (((IntegerLiteralExpr)right).getValue()==0)
+ return new int[0];
+ else
+ return new int[] {AbstractRepair.ADDTOSET}; }
else
return new int[] {AbstractRepair.REMOVEFROMSET};
}
public abstract int generate_worklistload(CodeWriter writer, int offset);
public abstract int generate_workliststore(CodeWriter writer, int offset);
-
}
this.relation = relation;
}
+ public String toString() {
+ String str="<"+leftelementexpr.name()+","+rightelementexpr.name()+"> in "+relation.toString();
+ return str;
+ }
+
public boolean usesDescriptor(Descriptor d) {
if (d==relation)
return true;
relation = rd;
}
+ public RelationDescriptor getRelation() {
+ return relation;
+ }
+
public void setTuple(VarDescriptor x, VarDescriptor y) {
this.x = x;
this.y = y;
public void generate_open(CodeWriter writer) {
writer.outputline("for (SimpleIterator* " + x.getSafeSymbol() + "_iterator = " + relation.getSafeSymbol() + "_hash->iterator(); " + x.getSafeSymbol() + "_iterator->hasNext(); )");
writer.startblock();
- writer.outputline(y.getType().getSafeSymbol() + " " + y.getSafeSymbol() + " = (" + y.getType().getSafeSymbol() + ") " + x.getSafeSymbol() + "_iterator->next();");
+ writer.outputline(y.getType().getGenerateType() + " " + y.getSafeSymbol() + " = (" + y.getType().getGenerateType() + ") " + x.getSafeSymbol() + "_iterator->next();");
// #ATTN#: key is called second because next() forwards ptr and key does not!
- writer.outputline(x.getType().getSafeSymbol() + " " + x.getSafeSymbol() + " = (" + x.getType().getSafeSymbol() + ") " + x.getSafeSymbol() + "_iterator->key();");
+ writer.outputline(x.getType().getGenerateType() + " " + x.getSafeSymbol() + " = (" + x.getType().getGenerateType() + ") " + x.getSafeSymbol() + "_iterator->key();");
}
public int generate_worklistload(CodeWriter writer, int offset) {
import java.util.*;
-public class Rule {
+public class Rule implements Quantifiers {
static int count = 1;
label = new String("rule" + count++);
}
+ public String toString() {
+ String name="";
+ for(int i=0;i<numQuantifiers();i++) {
+ name+=getQuantifier(i).toString()+",";
+ }
+ name+=guard.name()+"=>"+inclusion.toString();
+ return name;
+ }
+
public int numQuantifiers() {
return quantifiers.size();
}
if (descriptor instanceof SetDescriptor) {
expanded.addAll(((SetDescriptor) descriptor).allSubsets());
- }
+ } else
+ expanded.add(descriptor); /* Still need the descriptor */
}
expanded.addAll(descriptors);
static boolean worklist = false;
public boolean dostore = true;
+ public String toString() {
+ String str="";
+ str+=elementexpr.name()+" in "+set;
+ return str;
+ }
+
public SetInclusion(Expr elementexpr, SetDescriptor set) {
this.elementexpr = elementexpr;
this.set = set;
return elementexpr.usesDescriptor(d);
}
+ public Expr getExpr() {
+ return elementexpr;
+ }
+
public SetDescriptor getSet() {
return set;
}
return conj;
}
+ public Constraint getConstraint() {
+ if (type!=CONJUNCTION)
+ throw new Error("Not Conjunction Node!");
+ else
+ return constr;
+ }
+
public MultUpdateNode getUpdate() {
if (type!=UPDATE)
throw new Error("Not Update Node!");
Hashtable scopesatisfy;
Hashtable scopefalsify;
Hashtable consequence;
+ Hashtable abstractadd;
+ Hashtable abstractremove;
State state;
consequence=new Hashtable();
updatenodes=new HashSet();
consequencenodes=new HashSet();
+ abstractadd=new Hashtable();
+ abstractremove=new Hashtable();
+
generateconjunctionnodes();
generatescopenodes();
generaterepairnodes();
generatedatastructureupdatenodes();
+ generatecompensationnodes();
generateabstractedges();
generatescopeedges();
HashSet superset=new HashSet();
superset.addAll(conjunctions);
superset.addAll(abstractrepair);
- superset.addAll(updatenodes);
- superset.addAll(scopenodes);
- superset.addAll(consequencenodes);
+ //superset.addAll(updatenodes);
+ //superset.addAll(scopenodes);
+ //superset.addAll(consequencenodes);
+ //GraphNode.computeclosure(superset);
try {
GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
} catch (Exception e) {
GraphNode gn2=(GraphNode)conjiterator.next();
TermNode tn2=(TermNode)gn2.getOwner();
Conjunction conj=tn2.getConjunction();
+ Constraint cons=tn2.getConstraint();
+
for(int i=0;i<conj.size();i++) {
DNFPredicate dp=conj.get(i);
- if (AbstractInterferes.interferes(ar,dp)) {
+ if (AbstractInterferes.interferes(ar,cons)||
+ AbstractInterferes.interferes(ar,dp)) {
GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
gn.addEdge(e);
break;
GraphNode gn2=(GraphNode)conjiterator.next();
TermNode tn2=(TermNode)gn2.getOwner();
Conjunction conj=tn2.getConjunction();
+ Constraint constr=tn2.getConstraint();
for(int i=0;i<conj.size();i++) {
DNFPredicate dp=conj.get(i);
- if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),dp)) {
+ if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),dp)||
+ AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),constr)) {
GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
GraphNode gnconseq=(GraphNode)consequence.get(sn);
gnconseq.addEdge(e);
}
}
-
+ /* Generates the abstract repair nodes */
void generaterepairnodes() {
+ /* Generate repairs of conjunctions */
for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
GraphNode gn=(GraphNode)conjiterator.next();
TermNode tn=(TermNode)gn.getOwner();
}
}
}
+ /* Generate additional abstract repairs */
+ Vector setdescriptors=state.stSets.getAllDescriptors();
+ 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);
+ GraphNode gn=new GraphNode("AbstractAddSetRule"+i,tn);
+ abstractrepair.add(gn);
+ abstractadd.put(sd,gn);
+
+ DNFPredicate tp2=new DNFPredicate(true,ip);
+ AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMSET, sd);
+ TermNode tn2=new TermNode(ar2);
+ GraphNode gn2=new GraphNode("AbstractRemSetRule"+i,tn2);
+ abstractrepair.add(gn2);
+ abstractremove.put(sd,gn2);
+ }
+
+ 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");
+
+ InclusionPredicate ip=new InclusionPredicate(ve2,new ImageSetExpr(vd1, rd));
+
+ DNFPredicate tp=new DNFPredicate(false,ip);
+ AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTORELATION, rd);
+ TermNode tn=new TermNode(ar);
+ GraphNode gn=new GraphNode("AbstractAddRelRule"+i,tn);
+ abstractrepair.add(gn);
+ abstractadd.put(rd,gn);
+
+ DNFPredicate tp2=new DNFPredicate(true,ip);
+ AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMRELATION, rd);
+ TermNode tn2=new TermNode(ar2);
+ GraphNode gn2=new GraphNode("AbstractRemRelRule"+i,tn2);
+ abstractrepair.add(gn2);
+ abstractremove.put(rd,gn2);
+ }
+
+ }
+
+ int compensationcount=0;
+ void generatecompensationnodes() {
+ for(int i=0;i<state.vRules.size();i++) {
+ Rule r=(Rule) state.vRules.get(i);
+ Vector possiblerules=new Vector();
+ /* Construct bindings */
+ 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();
+ ScopeNode sn=tn.getScope();
+ MultUpdateNode mun=new MultUpdateNode(sn);
+ TermNode tn2=new TermNode(mun);
+ GraphNode gn2=new GraphNode("CompRem"+compensationcount,tn2);
+ UpdateNode un=new UpdateNode();
+ un.addBindings(bindings);
+ if (j<r.numQuantifiers()) {
+ /* Remove quantifier */
+ Quantifier q=r.getQuantifier(j);
+ if (q instanceof RelationQuantifier) {
+ RelationQuantifier rq=(RelationQuantifier)q;
+ TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
+ toe.td=ReservedTypeDescriptor.INT;
+ Updates u=new Updates(toe,true);
+ un.addUpdate(u);
+ if (abstractremove.containsKey(rq.relation)) {
+ GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
+ GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+ gn2.addEdge(e);
+ } else {
+ continue; /* Abstract repair doesn't exist */
+ }
+ } else if (q instanceof SetQuantifier) {
+ SetQuantifier sq=(SetQuantifier)q;
+ ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
+ eoe.td=ReservedTypeDescriptor.INT;
+ Updates u=new Updates(eoe,true);
+ un.addUpdate(u);
+ if (abstractremove.containsKey(sq.set)) {
+ GraphNode agn=(GraphNode)abstractremove.get(sq.set);
+ GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+ gn2.addEdge(e);
+ } else {
+ continue; /* Abstract repair doesn't exist */
+ }
+ } else {
+ continue;
+ }
+ } else {
+ int c=j-r.numQuantifiers();
+ if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
+ continue;
+ }
+ }
+
+ mun.addUpdate(un);
+
+ GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
+ compensationcount++;
+ gn.addEdge(e);
+ updatenodes.add(gn2);
+ }
+ }
}
void generatedatastructureupdatenodes() {
} else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
generateremovefromsetrelation(gn,ar);
} else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
+ /* Generate remove/add pairs */
+ generateremovefromsetrelation(gn,ar);
+ generateaddtosetrelation(gn,ar);
+ /* Generate atomic modify */
generatemodifyrelation(gn,ar);
}
}
(ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation()))
possiblerules.add(r);
}
+ if (possiblerules.size()==0)
+ return;
int[] count=new int[possiblerules.size()];
while(remains(count,possiblerules)) {
- MultUpdateNode mun=new MultUpdateNode(ar);
+ MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.REMOVE);
+ TermNode tn=new TermNode(mun);
+ GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
+
boolean goodflag=true;
for(int i=0;i<possiblerules.size();i++) {
Rule r=(Rule)possiblerules.get(i);
/* Construct bindings */
Vector bindings=new Vector();
constructbindings(bindings, r,true);
+ un.addBindings(bindings);
if (count[i]<r.numQuantifiers()) {
/* Remove quantifier */
Quantifier q=r.getQuantifier(count[i]);
toe.td=ReservedTypeDescriptor.INT;
Updates u=new Updates(toe,true);
un.addUpdate(u);
+ if (abstractremove.containsKey(rq.relation)) {
+ GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
+ GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+ gn2.addEdge(e);
+ } else {
+ goodflag=false;break; /* Abstract repair doesn't exist */
+ }
} else if (q instanceof SetQuantifier) {
SetQuantifier sq=(SetQuantifier)q;
ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
eoe.td=ReservedTypeDescriptor.INT;
Updates u=new Updates(eoe,true);
un.addUpdate(u);
+ if (abstractremove.containsKey(sq.set)) {
+ GraphNode agn=(GraphNode)abstractremove.get(sq.set);
+ GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+ gn2.addEdge(e);
+ } else {
+ goodflag=false;break; /* Abstract repair doesn't exist */
+ }
} else {goodflag=false;break;}
} else {
int c=count[i]-r.numQuantifiers();
mun.addUpdate(un);
}
if (goodflag) {
- TermNode tn=new TermNode(mun);
- GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
GraphNode.Edge e=new GraphNode.Edge("abstract"+removefromcount,gn2);
removefromcount++;
gn.addEdge(e);
RuleConjunction ruleconj=dnfrule.get(j);
/* Add in updates for quantifiers */
System.out.println("Attempting to generate add to set #4");
- if (processquantifers(un, r)&&debugdd()&&
+ MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.ADD);
+ TermNode tn=new TermNode(mun);
+ GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
+
+ if (processquantifers(gn2,un, r)&&debugdd()&&
processconjunction(un,ruleconj)) {
System.out.println("Attempting to generate add to set #5");
- MultUpdateNode mun=new MultUpdateNode(ar);
mun.addUpdate(un);
- TermNode tn=new TermNode(mun);
- GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
addtocount++;
gn.addEdge(e);
return true;
}
- boolean processquantifers(UpdateNode un, Rule r) {
- boolean goodupdate=true;
+ boolean processquantifers(GraphNode gn,UpdateNode un, Rule r) {
Inclusion inc=r.getInclusion();
for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
Quantifier q=(Quantifier)iterator.next();
toe.td=ReservedTypeDescriptor.INT;
Updates u=new Updates(toe,false);
un.addUpdate(u);
+ if (abstractremove.containsKey(rq.relation)) {
+ GraphNode agn=(GraphNode)abstractadd.get(rq.relation);
+ GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+ gn.addEdge(e);
+ } else {
+ return false;
+ }
+
} else if (q instanceof SetQuantifier) {
SetQuantifier sq=(SetQuantifier)q;
ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
eoe.td=ReservedTypeDescriptor.INT;
Updates u=new Updates(eoe,false);
un.addUpdate(u);
- } else {goodupdate=false; break;}
+ if (abstractremove.containsKey(sq.set)) {
+ GraphNode agn=(GraphNode)abstractadd.get(sq.set);
+ GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+ gn.addEdge(e);
+ } else {
+ return false;
+ }
+ } else return false;
}
- return goodupdate;
+ return true;
}
boolean processconjunction(UpdateNode un,RuleConjunction ruleconj){
ptSpace = null;
}
+ void printall() {
+ for(int i=0;i<vRules.size();i++) {
+ Rule r=(Rule)vRules.get(i);
+ System.out.println(r.toString());
+ }
+ for(int i=0;i<vConstraints.size();i++) {
+ Constraint c=(Constraint)vConstraints.get(i);
+ System.out.println(c.toString());
+ }
+ }
+
}
[], literal(true) => head in Nodes;
[forall node in Nodes], !(node.next=literal(0)) => node.next in Nodes;
[forall node in Nodes], !(node.next=literal(0)) => <node, node.next> in nextnodes;
-[forall node in Nodes], !(node.prev=literal(0)) => node.prev in Nodes;
[forall node in Nodes], !(node.prev=literal(0)) => <node, node.prev> in prevnodes;
projects / repair.git / commitdiff