import java.util.*;
class AbstractInterferes {
+ Termination termination;
+
+ public AbstractInterferes(Termination t) {
+ termination=t;
+ }
/** Does performing the AbstractRepair ar satisfy (or falsify if satisfy=false)
* Rule r */
/** Does performing the AbstractRepair ar falsify the predicate dp */
- static public boolean interferes(AbstractRepair ar, DNFPredicate dp) {
+ public boolean interferes(AbstractRepair ar, DNFPredicate dp) {
if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
((ar.getDescriptor() instanceof SetDescriptor)||
!dp.getPredicate().usesDescriptor((RelationDescriptor)ar.getDescriptor())))
boolean neg2=dp.isNegated();
Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
int size2=((ExprPredicate)dp.getPredicate()).rightSize();
- if ((!neg1&&((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE))||
- (neg1&&((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.LT)||op1==Opcode.LE))) {
+ op1=Opcode.translateOpcode(neg1,op1);
+ op2=Opcode.translateOpcode(neg2,op2);
+
+ if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
int size1a=0;
- if (!neg1) {
- if((op1==Opcode.EQ)||(op1==Opcode.GE))
- size1a=size1;
- if((op1==Opcode.GT)||(op1==Opcode.NE))
- size1a=size1+1;
- }
- if (neg1) {
- if((op1==Opcode.EQ)||(op1==Opcode.LE))
- size1a=size1+1;
- if((op1==Opcode.LT)||(op1==Opcode.NE))
- size1a=size1;
- }
- if ((!neg2&&(op2==Opcode.EQ)&&(size1a==size2))||
- (neg2&&(op2==Opcode.EQ)&&(size1a!=size2))||
- (!neg2&&(op2==Opcode.NE)&&(size1a!=size2))||
- (neg2&&(op2==Opcode.NE)&&(size1a==size2))||
- (!neg2&&(op2==Opcode.GE))||
- (!neg2&&(op2==Opcode.GT))||
- (neg2&&(op2==Opcode.LE))||
- (neg2&&(op2==Opcode.LT))||
- (neg2&&(op2==Opcode.GE)&&(size1a<size2))||
- (neg2&&(op2==Opcode.GT)&&(size1a<=size2))||
- (!neg2&&(op2==Opcode.LE)&&(size1a<=size2))||
- (!neg2&&(op2==Opcode.LT)&&(size1a<size2)))
+ if((op1==Opcode.EQ)||(op1==Opcode.GE))
+ size1a=size1;
+ if((op1==Opcode.GT)||(op1==Opcode.NE))
+ size1a=size1+1;
+
+ if (((op2==Opcode.EQ)&&(size1a==size2))||
+ ((op2==Opcode.NE)&&(size1a!=size2))||
+ (op2==Opcode.GE)||
+ (op2==Opcode.GT)||
+ ((op2==Opcode.LE)&&(size1a<=size2))||
+ ((op2==Opcode.LT)&&(size1a<size2)))
return false;
- }
+ }
}
if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
int size2=((ExprPredicate)dp.getPredicate()).rightSize();
- op2=translateOpcode(neg2,op2);
+ op2=Opcode.translateOpcode(neg2,op2);
- if (((op2==Opcode.EQ)&&(size2==0))||
+ int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
+
+ if ((maxsize!=-1)&&
+ ((op2==Opcode.LT&&size2>maxsize)||
+ (op2==Opcode.LE&&size2>=maxsize)||
+ (op2==Opcode.EQ&&size2>=maxsize)))
+ return false;
+
+ if (((op2==Opcode.NE)&&(size2==0))||
(op2==Opcode.GE)||
(op2==Opcode.GT))
return false;
}
if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
-
(ar.getType()==AbstractRepair.MODIFYRELATION)&&
(dp.getPredicate() instanceof ExprPredicate)&&
(dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
Expr expr2=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).right;
/* Translate the opcodes */
- op1=translateOpcode(neg1,op1);
- op2=translateOpcode(neg2,op2);
+ op1=Opcode.translateOpcode(neg1,op1);
+ op2=Opcode.translateOpcode(neg2,op2);
/* Obvious cases which can't interfere */
if (((op1==Opcode.GT)||
Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
int size2=((ExprPredicate)dp.getPredicate()).rightSize();
/* Translate the opcodes */
- op1=translateOpcode(neg1,op1);
- op2=translateOpcode(neg2,op2);
+ op1=Opcode.translateOpcode(neg1,op1);
+ op2=Opcode.translateOpcode(neg2,op2);
if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
int size1a=0;
boolean neg2=dp.isNegated();
Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
int size2=((ExprPredicate)dp.getPredicate()).rightSize();
- 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)))
+ op2=Opcode.translateOpcode(neg2,op2);
+
+ if (((op2==Opcode.EQ)&&(size2==0))||
+ (op2==Opcode.LE)||
+ (op2==Opcode.LT))
return false;
}
return true;
}
- static private Opcode translateOpcode(boolean neg, Opcode op) {
- if (neg) {
- /* remove negation through opcode translation */
- if (op==Opcode.GT)
- op=Opcode.LE;
- else if (op==Opcode.GE)
- op=Opcode.LT;
- else if (op==Opcode.EQ)
- op=Opcode.NE;
- else if (op==Opcode.NE)
- op=Opcode.EQ;
- else if (op==Opcode.LT)
- op=Opcode.GE;
- else if (op==Opcode.LE)
- op=Opcode.GT;
- }
-
- return op;
- }
-
/** Does the increase (or decrease) in scope of a model defintion rule represented by sn
* falsify the predicate dp */
- static public boolean interferes(ScopeNode sn, DNFPredicate dp) {
+ public boolean interferes(ScopeNode sn, DNFPredicate dp) {
if (!sn.getSatisfy()&&(sn.getDescriptor() instanceof SetDescriptor)) {
Rule r=sn.getRule();
Set target=r.getInclusion().getTargetDescriptors();
boolean neg=dp.isNegated();
Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
int size=((ExprPredicate)dp.getPredicate()).rightSize();
- if (neg) {
- /* remove negation through opcode translation */
- if (op==Opcode.GT)
- op=Opcode.LE;
- else if (op==Opcode.GE)
- op=Opcode.LT;
- else if (op==Opcode.EQ)
- op=Opcode.NE;
- else if (op==Opcode.NE)
- op=Opcode.EQ;
- else if (op==Opcode.LT)
- op=Opcode.GE;
- else if (op==Opcode.LE)
- op=Opcode.GT;
- }
+ op=Opcode.translateOpcode(neg,op);
+
if ((op==Opcode.GE)&&
((size==0)||(size==1)))
return false;
/** Does increasing (or decreasing if satisfy=false) the size of the set or relation des
* falsify the predicate dp */
- static public boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
+ public boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
if ((des!=dp.getPredicate().getDescriptor()) &&
((des instanceof SetDescriptor)||
!dp.getPredicate().usesDescriptor((RelationDescriptor)des)))
boolean neg2=dp.isNegated();
Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
int size2=((ExprPredicate)dp.getPredicate()).rightSize();
+ op2=Opcode.translateOpcode(neg2,op2);
+
+
+ int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
{
- 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)))
+ if ((maxsize!=-1)&&
+ ((op2==Opcode.LT&&size2>maxsize)||
+ (op2==Opcode.LE&&size2>=maxsize)||
+ (op2==Opcode.EQ&&size2>=maxsize)))
+ return false;
+
+ if ((op2==Opcode.GE)||
+ (op2==Opcode.GT)||
+ (op2==Opcode.NE)&&(size2==0))
return false;
}
}
boolean neg2=dp.isNegated();
Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
int size2=((ExprPredicate)dp.getPredicate()).rightSize();
+ op2=Opcode.translateOpcode(neg2,op2);
{
- 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)))
+ if (((op2==Opcode.EQ)&&(size2==0))||
+ (op2==Opcode.LE)||
+ (op2==Opcode.LT))
return false;
}
}
class Binding {
VarDescriptor var;
+ SetDescriptor sd;
int position;
- boolean search;
+ int type;
+ public static final int POSITION=1;
+ public static final int CREATE=2;
+ public static final int SEARCH=3;
+
public Binding(VarDescriptor vd,int pos) {
var=vd;
position=pos;
- search=false;
+ type=POSITION;
}
- public Binding(VarDescriptor vd) {
- var=vd;
- search=true;
+ public Binding(VarDescriptor vd, SetDescriptor sd,boolean search) {
+ this.var=vd;
+ this.sd=sd;
+ if (search)
+ type=SEARCH;
+ else
+ type=CREATE;
}
+
+ public int getType() {
+ return type;
+ }
+
int getPosition() {
+ assert type==POSITION;
return position;
}
+
+ SetDescriptor getSet() {
+ assert type==CREATE||type==SEARCH;
+ return sd;
+ }
+
VarDescriptor getVar() {
return var;
}
+
public String toString() {
- if (search)
- return "SEARCHFOR"+var.toString();
- else
+ switch(type) {
+ case POSITION:
return var.toString()+"="+String.valueOf(position);
+ case CREATE:
+ return var.toString()+"=CREATE("+sd.toString()+")";
+ case SEARCH:
+ return var.toString()+"=SEARCH("+sd.toString()+")";
+ default:
+ return "UNRECOGNIZED Binding type";
+ }
}
}
}
if ((size!=0)&&(d==d2))
size=-1;
- } if (q instanceof SetQuantifier) {
+ } else if (q instanceof SetQuantifier) {
Descriptor d2=((SetQuantifier)q).getSet();
if (sizemap.containsKey(d2)) {
size=((Integer)sizemap.get(d2)).intValue();
}
if ((size!=0)&&(d==d2))
size=-1;
+ } else if (q instanceof ForQuantifier) {
+ ForQuantifier fq=(ForQuantifier)q;
+ boolean lowint=OpExpr.isInt(fq.lower);
+ boolean highint=OpExpr.isInt(fq.upper);
+ if (lowint&&highint) {
+ size=1+OpExpr.getInt(fq.upper)-OpExpr.getInt(fq.lower);
+ if (size<=0) /* Catch sneaky bounds */
+ throw new Error("Funny bounds in: "+fq);
+ } else size=-1;
} else {
size=-1;
}
Opcode op=expr.getOpcode();
+ op=Opcode.translateOpcode(dexpr.getNegation(),op);
- if (dexpr.getNegation()) {
- /* remove negation through opcode translation */
- if (op==Opcode.GT)
- op=Opcode.LE;
- else if (op==Opcode.GE)
- op=Opcode.LT;
- else if (op==Opcode.EQ)
- op=Opcode.NE;
- else if (op==Opcode.NE)
- op=Opcode.EQ;
- else if (op==Opcode.LT)
- op=Opcode.GE;
- else if (op==Opcode.LE)
- op=Opcode.GT;
- }
boolean match=false;
for(int k=0;k<un.numUpdates();k++) {
Updates update=un.getUpdate(k);
Expr lexpr2=expr.getLeftExpr();
Expr rexpr2=expr.getRightExpr();
Opcode op2=expr.getOpcode();
- if (dexpr.getNegation()) {
- /* remove negation through opcode translation */
- if (op2==Opcode.GT)
- op2=Opcode.LE;
- else if (op2==Opcode.GE)
- op2=Opcode.LT;
- else if (op2==Opcode.EQ)
- op2=Opcode.NE;
- else if (op2==Opcode.NE)
- op2=Opcode.EQ;
- else if (op2==Opcode.LT)
- op2=Opcode.GE;
- else if (op2==Opcode.LE)
- op2=Opcode.GT;
- }
+ op2=Opcode.translateOpcode(dexpr.getNegation(),op2);
+
good=true;
vars=rexpr2.freeVars();
VarDescriptor leftdescriptor=null;
return var;
}
-
public void setBounds(Expr lower, Expr upper) {
this.lower = lower;
this.upper = upper;
public static final Opcode NOP = new Opcode("NOP");
public static final Opcode SHL = new Opcode("<<");
public static final Opcode SHR = new Opcode(">>");
+
+ static public Opcode translateOpcode(boolean neg, Opcode op) {
+ if (neg) {
+ /* remove negation through opcode translation */
+ if (op==Opcode.GT)
+ op=Opcode.LE;
+ else if (op==Opcode.GE)
+ op=Opcode.LT;
+ else if (op==Opcode.EQ)
+ op=Opcode.NE;
+ else if (op==Opcode.NE)
+ op=Opcode.EQ;
+ else if (op==Opcode.LT)
+ op=Opcode.GE;
+ else if (op==Opcode.LE)
+ op=Opcode.GT;
+ else throw new Error("Unrecognized Opcode");
+ }
+
+ return op;
+ }
public static Opcode decodeFromString(String opname) {
Opcode opcode;
Set removedset;
ComputeMaxSize maxsize;
State state;
+ AbstractInterferes abstractinterferes;
+
public Termination(State state) {
this.state=state;
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++)
maxsize=new ComputeMaxSize(state);
+ abstractinterferes=new AbstractInterferes(this);
generateconjunctionnodes();
generatescopenodes();
generaterepairnodes();
}
}
-
+
+
+ /** 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
for(int i=0;i<constraints.size();i++) {
Constraint c=(Constraint)constraints.get(i);
DNFConstraint dnf=c.dnfconstraint;
((Set)conjunctionmap.get(c)).add(gn);
conjtonodemap.put(dnf.get(j),gn);
}
+ // Construct quantifier "conjunction" nodes
for(int j=0;j<c.numQuantifiers();j++) {
Quantifier q=c.getQuantifier(j);
if (q instanceof SetQuantifier) {
for(int i=0;i<conj.size();i++) {
DNFPredicate dp=conj.get(i);
if (AbstractInterferes.interferes(ar,cons)||
- AbstractInterferes.interferes(ar,dp)) {
+ abstractinterferes.interferes(ar,dp)) {
GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
gn.addEdge(e);
break;
Constraint constr=tn2.getConstraint();
for(int i=0;i<conj.size();i++) {
DNFPredicate dp=conj.get(i);
- if (AbstractInterferes.interferes(sn,dp)||
+ if (abstractinterferes.interferes(sn,dp)||
AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),constr)) {
GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
GraphNode gnconseq=(GraphNode)consequence.get(sn);
}
}
- /* Generates the abstract repair nodes */
+ /** This method generates the abstract repair nodes. */
void generaterepairnodes() {
/* Generate repairs of conjunctions */
for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
}
}
- static void increment(int count[], Vector rules,boolean isremove) {
+ static private void increment(int count[], Vector rules,boolean isremove) {
count[0]++;
for(int i=0;i<(rules.size()-1);i++) {
int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
}
}
- static boolean remains(int count[], Vector rules, boolean isremove) {
+ 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();
if (count[i]>=num) {
increment(count,possiblerules,false);
}
}
-
+ /** 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, boolean isremoval) {
boolean goodupdate=true;
SetDescriptor set=null;
if (q instanceof SetQuantifier) {
vd=((SetQuantifier)q).getVar();
- } else
+ set=((SetQuantifier)q).getSet();
+ } else {
vd=((ForQuantifier)q).getVar();
+ }
if(inc instanceof SetInclusion) {
SetInclusion si=(SetInclusion)inc;
if ((si.elementexpr instanceof VarExpr)&&
/* Can solve for v */
Binding binding=new Binding(vd,0);
bindings.add(binding);
- } else
+ } else {
goodupdate=false;
+ }
} else if (inc instanceof RelationInclusion) {
RelationInclusion ri=(RelationInclusion)inc;
boolean f1=true;
} else throw new Error("Inclusion not recognized");
if (!goodupdate)
if (isremoval) {
- Binding binding=new Binding(vd);
+ /* Removals don't need bindings anymore
+ Binding binding=new Binding(vd);
+ bindings.add(binding);*/
+ goodupdate=true;
+ } else {
+ /* Create new element to bind to */
+ Binding binding=new Binding(vd,set,createorsearch(set));
bindings.add(binding);
goodupdate=true;
- } else
- break;
+ //FIXME
+ }
} else if (q instanceof RelationQuantifier) {
RelationQuantifier rq=(RelationQuantifier)q;
for(int k=0;k<2;k++) {
} else throw new Error("Inclusion not recognized");
if (!goodupdate)
if (isremoval) {
- Binding binding=new Binding(vd);
- bindings.add(binding);
+ /* Removals don't need bindings anymore
+ Binding binding=new Binding(vd);
+ bindings.add(binding);*/
goodupdate=true;
} else
break;
return goodupdate;
}
+ /** Returns true if we search for an element from sd
+ * false if we create an element for sd */
+ private boolean createorsearch(SetDescriptor sd) {
+ return false;
+ }
+
static int addtocount=0;
void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) {
- // System.out.println("Attempting to generate add to set");
- //System.out.println(ar.getPredicate().getPredicate().name());
- //System.out.println(ar.getPredicate().isNegated());
for(int i=0;i<state.vRules.size();i++) {
Rule r=(Rule) state.vRules.get(i);
/* See if this is a good rule*/
- //System.out.println(r.getGuardExpr().name());
if ((r.getInclusion() instanceof SetInclusion&&
ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
(r.getInclusion() instanceof RelationInclusion&&
/* First solve for quantifiers */
Vector bindings=new Vector();
/* Construct bindings */
- //System.out.println("Attempting to generate add to set: #2");
if (!constructbindings(bindings,r,false))
continue;
- //System.out.println("Attempting to generate add to set: #3");
//Generate add instruction
DNFRule dnfrule=r.getDNFGuardExpr();
for(int j=0;j<dnfrule.size();j++) {
}
//Finally build necessary updates to satisfy conjunction
RuleConjunction ruleconj=dnfrule.get(j);
+
/* Add in updates for quantifiers */
- //System.out.println("Attempting to generate add to set #4");
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()&&
+ if (processquantifers(gn2,un, r)&&
processconjunction(un,ruleconj)&&
un.checkupdates()) {
- //System.out.println("Attempting to generate add to set #5");
mun.addUpdate(un);
GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
addtocount++;
}
}
}
-
- boolean debugdd() {
- //System.out.println("Attempting to generate add to set DD");
- return true;
- }
-
+
+ /** Adds updates that add an item to the appropriate set or
+ * relation quantified over by the model definition rule.. */
+
boolean processquantifers(GraphNode gn,UpdateNode un, Rule r) {
Inclusion inc=r.getInclusion();
for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
} else {
return false;
}
-
+
} else if (q instanceof SetQuantifier) {
SetQuantifier sq=(SetQuantifier)q;
ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
binding.put(b.getVar(),b);
}
+ public int numBindings() {
+ return bindings.size();
+ }
+
+ public Binding getBinding(int i) {
+ return (Binding)bindings.get(i);
+ }
+
public Binding getBinding(VarDescriptor vd) {
if (binding.containsKey(vd))
return (Binding)binding.get(vd);
private void generate_bindings(CodeWriter cr, String slot0, String slot1) {
for(int i=0;i<bindings.size();i++) {
Binding b=(Binding)bindings.get(i);
- if (b.search)
- throw new Error("Search not implemented for bindings");
+ if (b.getType()!=Binding.POSITION)
+ throw new Error("Only position bindings implemented!");
+
VarDescriptor vd=b.getVar();
switch(b.getPosition()) {
case 0:
System.out.println("Building invalid update");
leftexpr=lexpr;
type=Updates.EXPR;
- if (negate) {
- /* remove negation through opcode translation */
- if (op==Opcode.GT)
- op=Opcode.LE;
- else if (op==Opcode.GE)
- op=Opcode.LT;
- else if (op==Opcode.EQ)
- op=Opcode.NE;
- else if (op==Opcode.NE)
- op=Opcode.EQ;
- else if (op==Opcode.LT)
- op=Opcode.GE;
- else if (op==Opcode.LE)
- op=Opcode.GT;
- }
+
+ op=Opcode.translateOpcode(negate,op);
+
opcode=op;
rightexpr=rexpr;
}
projects / repair.git / commitdiff