import java.util.*;
public class ExprPredicate extends Predicate {
-
+
Expr expr;
+
+ public static final int SIZE=1;
+ public static final int COMPARISON=2;
+
+ public int getType() {
+ if (((OpExpr)expr).left instanceof SizeofExpr)
+ return SIZE;
+ else if (((OpExpr)expr).left instanceof RelationExpr)
+ return COMPARISON;
+ else throw new Error("Unidentifiable Type");
+ }
+
+ public Opcode getOp() {
+ return ((OpExpr)expr).opcode;
+ }
+
+ public int leftsize() {
+ return ((IntegerLiteralExpr)((OpExpr)expr).right).getValue();
+ }
+
public ExprPredicate(Expr expr) {
if (expr == null) {
throw new NullPointerException();
}
-
this.expr = expr;
}
return expr.getInversedRelations();
}
+ public int[] getRepairs(boolean negated) {
+ return expr.getRepairs(negated);
+ }
+
+ public Descriptor getDescriptor() {
+ return expr.getDescriptor();
+ }
+
+ public boolean inverted() {
+ return expr.inverted();
+ }
+
+ public boolean usesDescriptor(RelationDescriptor rd) {
+ return expr.usesDescriptor(rd);
+ }
+
public Set getRequiredDescriptors() {
return expr.getRequiredDescriptors();
}
public void generate(CodeWriter writer, VarDescriptor dest) {
expr.generate(writer, dest);
}
-
- public int[] getRepairs(boolean negated) {
- return new int[] {};
- }
}
} else throw new Error();
}
+ public boolean usesDescriptor(RelationDescriptor rd) {
+ if (opcode==Opcode.GT||opcode==Opcode.GE||opcode==Opcode.LT||
+ opcode==Opcode.LE||opcode==Opcode.EQ||opcode==Opcode.NE)
+ return right.usesDescriptor(rd);
+ else
+ return left.usesDescriptor(rd)||(right!=null&&right.usesDescriptor(rd));
+ }
+
+ public int[] getRepairs(boolean negated) {
+ if (left instanceof RelationExpr)
+ return new int[] {AbstractRepair.MODIFYRELATION};
+ if (left instanceof SizeofExpr) {
+ boolean isRelation=((SizeofExpr)left).setexpr instanceof ImageSetExpr;
+ if (isRelation) {
+ if (opcode==Opcode.EQ)
+ return new int[] {AbstractRepair.ADDTORELATION,
+ AbstractRepair.REMOVEFROMRELATION};
+ if (((opcode==Opcode.GE)&&!negated)||
+ ((opcode==Opcode.LE)&&negated))
+ return new int[]{AbstractRepair.ADDTORELATION};
+ else
+ return new int[]{AbstractRepair.REMOVEFROMRELATION};
+ } else {
+ if (opcode==Opcode.EQ)
+ return new int[] {AbstractRepair.ADDTOSET,
+ AbstractRepair.REMOVEFROMSET};
+
+ if (((opcode==Opcode.GE)&&!negated)||
+ ((opcode==Opcode.LE)&&negated))
+ return new int[] {AbstractRepair.ADDTOSET};
+ else
+ return new int[] {AbstractRepair.REMOVEFROMSET};
+ }
+ }
+ throw new Error("BAD");
+ }
+
+ public Descriptor getDescriptor() {
+ return left.getDescriptor();
+ }
+ public boolean inverted() {
+ return left.inverted();
+ }
public Set getInversedRelations() {
Set set = left.getInversedRelations();
package MCC.IR;
import java.util.*;
+import MCC.State;
-class Termination {
+public class Termination {
HashSet conjunctions;
Hashtable conjunctionmap;
HashSet abstractrepair;
+ HashSet scopenodes;
+ Hashtable scopesatisfy;
+ Hashtable scopefalsify;
+
State state;
public Termination(State state) {
this.state=state;
+ conjunctions=new HashSet();
+ conjunctionmap=new Hashtable();
+ abstractrepair=new HashSet();
+ scopenodes=new HashSet();
+ scopesatisfy=new Hashtable();
+ scopefalsify=new Hashtable();
+
generateconjunctionnodes();
generaterepairnodes();
+ generateabstractedges();
+ generatedatastructureupdatenodes();
+ generatescopenodes();
}
void generateconjunctionnodes() {
}
}
+ void generateabstractedges() {
+ for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
+ GraphNode gn=(GraphNode)absiterator.next();
+ TermNode tn=(TermNode)gn.getOwner();
+ AbstractRepair ar=(AbstractRepair)tn.getAbstract();
+
+ for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
+ GraphNode gn2=(GraphNode)conjiterator.next();
+ TermNode tn2=(TermNode)gn2.getOwner();
+ Conjunction conj=tn2.getConjunction();
+ for(int i=0;i<conj.size();i++) {
+ DNFPredicate dp=conj.get(i);
+ if (AbstractInterferes.interferes(ar,dp)) {
+ GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
+ gn.addEdge(e);
+ break;
+ }
+ }
+ }
+ }
+ }
+
+
void generaterepairnodes() {
for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
GraphNode gn=(GraphNode)conjiterator.next();
Conjunction conj=tn.getConjunction();
for(int i=0;i<conj.size();i++) {
DNFPredicate dp=conj.get(i);
- int[] array=dp.getPredicate().getRepairs();
- for {int j=0;j<array.length;j++) {
- AbstractRepair ar=new AbstractRepair(dp,array[j]);
- TermNode tn=new TermNode(ar);
- GraphNode gn2=new GraphNode(gn.getLabel()+"-"+i+","+j,tn);
- Edge e=new Edge("abstract",gn2);
+ int[] array=dp.getPredicate().getRepairs(dp.isNegated());
+ Descriptor d=dp.getPredicate().getDescriptor();
+ for(int j=0;j<array.length;j++) {
+ AbstractRepair ar=new AbstractRepair(dp,array[j],d);
+ TermNode tn2=new TermNode(ar);
+ GraphNode gn2=new GraphNode(gn.getLabel()+"-"+i+","+j,tn2);
+ GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
gn.addEdge(e);
abstractrepair.add(gn2);
}
}
}
}
-}
-
-class AbstractRepair {
- public final static int ADDTOSET=1;
- public final static int REMOVEFROMSET=2;
- public final static int ADDTORELATION=3;
- public final static int REMOVEFROMRELATION=4;
- public final static int MODIFYRELATION=5;
- DNFPredicate torepair;
- int type;
-
- public AbstractRepair(DNFPredicate dp,int typ) {
- torepair=dp;
- type=typ;
+ void generatedatastructureupdatenodes() {
+ for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
+ GraphNode gn=(GraphNode)absiterator.next();
+ TermNode tn=(TermNode) gn.getOwner();
+ AbstractRepair ar=tn.getAbstract();
+ if (ar.getType()==AbstractRepair.ADDTOSET) {
+ generateaddtoset(ar);
+ } else if (ar.getType()==AbstractRepair.REMOVEFROMSET) {
+ generateremovefromset(ar);
+ } else if (ar.getType()==AbstractRepair.ADDTORELATION) {
+ generateaddtorelation(ar);
+ } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
+ generateremovefromrelation(ar);
+ } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
+ generatemodifyrelation(ar);
+ }
+ }
}
-}
-
-class TermNode {
- public final static int CONJUNCTION=1;
- public final static int ABSTRACT=2;
- Constraint constr;
- Conjunction conj;
- int type;
- AbstractRepair repair;
+ void generateaddtoset(AbstractRepair ar) {
+ for(int i=0;i<state.vRules.size();i++) {
+ Rule r=(Rule) state.vRules.get(i);
+ if (r.getInclusion() instanceof SetInclusion) {
+ if (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()) {
+ //Generate add instruction
+
- public TermNode(Constraint constr, Conjunction conj) {
- this.constr=constr;
- this.conj=conj;
- type=CONJUNCTION;
+ }
+ }
+ }
}
- public TermNode(AbstractRepair ar) {
- repair=ar;
- type=ABSTRACT;
- }
+ void generatescopenodes() {
+ for(int i=0;i<state.vRules.size();i++) {
+ Rule r=(Rule) state.vRules.get(i);
+ ScopeNode satisfy=new ScopeNode(r,true);
+ TermNode tnsatisfy=new TermNode(satisfy);
+ GraphNode gnsatisfy=new GraphNode("Satisfy Rule"+i,tnsatisfy);
- public Conjunction getConjunction() {
- return conj;
+ ScopeNode falsify=new ScopeNode(r,false);
+ TermNode tnfalsify=new TermNode(falsify);
+ GraphNode gnfalsify=new GraphNode("Falsify Rule"+i,tnfalsify);
+ scopesatisfy.put(r,gnsatisfy);
+ scopefalsify.put(r,gnfalsify);
+ scopenodes.add(gnsatisfy);
+ scopenodes.add(gnfalsify);
+ }
}
}
-
projects / repair.git / commitdiff