From 472bc7976276ec6771d9e22688c4926d488053e5 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 20 Jul 2004 19:17:27 +0000 Subject: [PATCH] Added needed comments, reorganized some code... --- Repair/RepairCompiler/MCC/IR/CastExpr.java | 8 +- .../MCC/IR/ConcreteInterferes.java | 245 ++++++++++-------- Repair/RepairCompiler/MCC/IR/DotExpr.java | 16 +- Repair/RepairCompiler/MCC/IR/OpExpr.java | 12 +- Repair/RepairCompiler/MCC/IR/Termination.java | 3 + 5 files changed, 161 insertions(+), 123 deletions(-) diff --git a/Repair/RepairCompiler/MCC/IR/CastExpr.java b/Repair/RepairCompiler/MCC/IR/CastExpr.java index 0785749..23e194f 100755 --- a/Repair/RepairCompiler/MCC/IR/CastExpr.java +++ b/Repair/RepairCompiler/MCC/IR/CastExpr.java @@ -31,10 +31,6 @@ public class CastExpr extends Expr { return expr.findInvariants(vars); } - public void findmatch(Descriptor d, Set s) { - expr.findmatch(d,s); - } - public CastExpr(TypeDescriptor type, Expr expr) { this.type = type; this.expr = expr; @@ -54,6 +50,10 @@ public class CastExpr extends Expr { else return ((this.type==((CastExpr)e).type)&&expr.equals(remap,((CastExpr)e).expr)); } + public void findmatch(Descriptor d, Set s) { + expr.findmatch(d,s); + } + public Set useDescriptor(Descriptor d) { return expr.useDescriptor(d); } diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java index e822841..4f6c333 100755 --- a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java +++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java @@ -8,25 +8,122 @@ public class ConcreteInterferes { this.termination=t; } + /** Returns true if the data structure updates performed by mun + * may increase (or decrease if satisfy=false) the scope of the + * model definition rule r. */ - static public boolean interferesinclusion(UpdateNode un, Updates update, Rule r) { + public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) { + + // A rule that adds something to a set can't be falsified by + // an update that is only performed if the set is empty + if (!initialinterferes(mun,r,satisfy)) + return false; + + for(int i=0;i0) ((op==Opcode.GE)&&(ep.rightSize()==1))) //(>=1) return false; } - return true; - - } - static private boolean interferes(UpdateNode un,Updates update, Rule r,DNFExpr dexpr) { + static private boolean interferes(Updates update, DNFExpr dexpr) { Descriptor descriptor=update.getDescriptor(); + /* If the DNFExpr expr doesn't use the updated descriptor, + there is no interference. */ if (!dexpr.getExpr().usesDescriptor(descriptor)) return false; - /* We need to pair the variables */ if (update.isExpr()) { + /* We need to pair the variables */ Set vars=update.getRightExpr().freeVars(); Opcode op1=update.getOpcode(); Expr lexpr1=update.getLeftExpr(); @@ -353,8 +389,8 @@ public class ConcreteInterferes { if (vars!=null) for(Iterator it=vars.iterator();it.hasNext();) { VarDescriptor vd=(VarDescriptor) it.next(); + /* VarDescriptor isn't a global */ if (!vd.isGlobal()) { - /* VarDescriptor isn't a global */ if (update.getVar()!=vd) { good=false; break; @@ -368,24 +404,21 @@ public class ConcreteInterferes { Opcode op2=expr.getOpcode(); op2=Opcode.translateOpcode(dexpr.getNegation(),op2); - good=true; - vars=rexpr2.freeVars(); VarDescriptor leftdescriptor=null; - if (lexpr2 instanceof VarExpr) - leftdescriptor=((VarExpr)lexpr2).getVar(); - else if (lexpr2 instanceof DotExpr) { + { Expr e=lexpr2; - do { + while(!(e instanceof VarExpr)) { for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ; if (e instanceof VarExpr) break; if (e instanceof CastExpr) e=((CastExpr)e).getExpr(); else throw new Error("Bad Expr Type:"+e.name()); - } while (true); + } leftdescriptor=((VarExpr)e).getVar(); - } else throw new Error("Bad Expr"); - + } + + vars=rexpr2.freeVars(); if (vars!=null) for(Iterator it=vars.iterator();it.hasNext();) { VarDescriptor vd=(VarDescriptor) it.next(); @@ -397,6 +430,8 @@ public class ConcreteInterferes { } } } + + if (good) { HashMap remap=new HashMap(); remap.put(update.getVar(),leftdescriptor); diff --git a/Repair/RepairCompiler/MCC/IR/DotExpr.java b/Repair/RepairCompiler/MCC/IR/DotExpr.java index 9361d5e..029b22c 100755 --- a/Repair/RepairCompiler/MCC/IR/DotExpr.java +++ b/Repair/RepairCompiler/MCC/IR/DotExpr.java @@ -65,14 +65,6 @@ public class DotExpr extends Expr { return true; } - public void findmatch(Descriptor d, Set s) { - if (d==fd) - s.add(this); - left.findmatch(d,s); - if (intindex!=null) - intindex.findmatch(d,s); - } - public Set freeVars() { Set lset=left.freeVars(); Set iset=null; @@ -108,6 +100,14 @@ public class DotExpr extends Expr { return name; } + public void findmatch(Descriptor d, Set s) { + if (d==fd) + s.add(this); + left.findmatch(d,s); + if (intindex!=null) + intindex.findmatch(d,s); + } + public Set useDescriptor(Descriptor d) { HashSet newset=new HashSet(); if (d==fd) diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java index 55aacfc..dfa0c14 100755 --- a/Repair/RepairCompiler/MCC/IR/OpExpr.java +++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java @@ -78,12 +78,6 @@ public class OpExpr extends Expr { return rightfunctions; } - public void findmatch(Descriptor d, Set s) { - left.findmatch(d,s); - if (right!=null) - right.findmatch(d,s); - } - public static boolean isInt(Expr e) { if (e==null) return false; @@ -239,6 +233,12 @@ public class OpExpr extends Expr { return left.usesDescriptor(d)||(right!=null&&right.usesDescriptor(d)); } + public void findmatch(Descriptor d, Set s) { + left.findmatch(d,s); + if (right!=null) + right.findmatch(d,s); + } + public Set useDescriptor(Descriptor d) { HashSet newset=new HashSet(); newset.addAll(left.useDescriptor(d)); diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java index 57cf6c9..9f00c5b 100755 --- a/Repair/RepairCompiler/MCC/IR/Termination.java +++ b/Repair/RepairCompiler/MCC/IR/Termination.java @@ -1160,6 +1160,9 @@ public class Termination { return okay; } + /** This method sees if when the quantifiers listed in set are + * fixed, whether there can be more than one unique binding for + * the constraint or model definition rule qs.*/ public boolean analyzeQuantifiers(Quantifiers qs,Set set) { for(int i=0;i