From 493f2391c27e874c524f8ad36c1d04734e0de9b9 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Mon, 19 Apr 2004 21:48:08 +0000 Subject: [PATCH] Update: 1. Removes some old debugging code 2. Simplifies some complex case statements 3. Uses maxsize calculations for set additions 4. Starts to support create/search new element type bindings. --- .../MCC/IR/AbstractInterferes.java | 152 +++++++----------- Repair/RepairCompiler/MCC/IR/Binding.java | 44 ++++- .../RepairCompiler/MCC/IR/ComputeMaxSize.java | 11 +- .../MCC/IR/ConcreteInterferes.java | 33 +--- .../RepairCompiler/MCC/IR/ForQuantifier.java | 1 - Repair/RepairCompiler/MCC/IR/Opcode.java | 21 +++ Repair/RepairCompiler/MCC/IR/Termination.java | 80 +++++---- Repair/RepairCompiler/MCC/IR/UpdateNode.java | 13 +- Repair/RepairCompiler/MCC/IR/Updates.java | 18 +-- 9 files changed, 196 insertions(+), 177 deletions(-) diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java index ea024cd..affa035 100755 --- a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java +++ b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java @@ -2,6 +2,11 @@ package MCC.IR; 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 */ @@ -55,7 +60,7 @@ class AbstractInterferes { /** 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()))) @@ -74,35 +79,24 @@ class AbstractInterferes { 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)&&(size1amaxsize)|| + (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())&& @@ -142,8 +143,8 @@ class AbstractInterferes { 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)|| @@ -236,8 +237,8 @@ class AbstractInterferes { 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; @@ -264,12 +265,11 @@ class AbstractInterferes { 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; } @@ -288,30 +288,10 @@ class AbstractInterferes { 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(); @@ -333,21 +313,8 @@ class AbstractInterferes { 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; @@ -362,7 +329,7 @@ class AbstractInterferes { /** 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))) @@ -376,13 +343,20 @@ class AbstractInterferes { 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; } } @@ -394,13 +368,11 @@ class AbstractInterferes { 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; } } diff --git a/Repair/RepairCompiler/MCC/IR/Binding.java b/Repair/RepairCompiler/MCC/IR/Binding.java index 163f237..33e9bae 100755 --- a/Repair/RepairCompiler/MCC/IR/Binding.java +++ b/Repair/RepairCompiler/MCC/IR/Binding.java @@ -2,28 +2,56 @@ package MCC.IR; 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"; + } } } diff --git a/Repair/RepairCompiler/MCC/IR/ComputeMaxSize.java b/Repair/RepairCompiler/MCC/IR/ComputeMaxSize.java index 0dec8e0..51221c3 100755 --- a/Repair/RepairCompiler/MCC/IR/ComputeMaxSize.java +++ b/Repair/RepairCompiler/MCC/IR/ComputeMaxSize.java @@ -44,13 +44,22 @@ public class ComputeMaxSize { } 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; } diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java index 8cb19f8..f8d82d5 100755 --- a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java +++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java @@ -93,22 +93,8 @@ class ConcreteInterferes { 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>"); + + 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; diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java index 73c89f1..d6a792f 100755 --- a/Repair/RepairCompiler/MCC/IR/Termination.java +++ b/Repair/RepairCompiler/MCC/IR/Termination.java @@ -25,6 +25,8 @@ public class Termination { Set removedset; ComputeMaxSize maxsize; State state; + AbstractInterferes abstractinterferes; + public Termination(State state) { this.state=state; @@ -45,6 +47,7 @@ public class Termination { if (!Compiler.REPAIR) return; + for(int i=0;i=num) { @@ -635,7 +645,10 @@ public class Termination { 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; @@ -647,8 +660,10 @@ public class Termination { 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)&& @@ -656,8 +671,9 @@ public class Termination { /* 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; @@ -679,11 +695,17 @@ public class Termination { } 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++) { @@ -718,8 +740,9 @@ public class Termination { } 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; @@ -731,15 +754,17 @@ public class Termination { 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