From f9e84f661a348d52ec5a96e246f028e3cb102fb4 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Mon, 2 Aug 2004 23:47:13 +0000 Subject: [PATCH] Fixed some errors in the Repair Generator code. --- .../RepairCompiler/MCC/IR/AbstractRepair.java | 12 +++ .../MCC/IR/ConstraintDependence.java | 14 +-- .../RepairCompiler/MCC/IR/GraphAnalysis.java | 4 +- .../MCC/IR/RepairGenerator.java | 90 +++++++++++++------ Repair/RepairCompiler/MCC/IR/Termination.java | 3 +- 5 files changed, 86 insertions(+), 37 deletions(-) diff --git a/Repair/RepairCompiler/MCC/IR/AbstractRepair.java b/Repair/RepairCompiler/MCC/IR/AbstractRepair.java index aecc4e9..153677f 100755 --- a/Repair/RepairCompiler/MCC/IR/AbstractRepair.java +++ b/Repair/RepairCompiler/MCC/IR/AbstractRepair.java @@ -1,4 +1,5 @@ package MCC.IR; +import MCC.State; class AbstractRepair { public final static int ADDTOSET=1; @@ -150,6 +151,17 @@ class AbstractRepair { return descriptor; } + + /** Thie method tells whether the repair needs to remove objects * + * from the relation, or whether the model definition rules make + * the remove unnecessary.*/ + + public boolean needsRemoves(State state) { + assert type==MODIFYRELATION; + SetDescriptor sd=getPredicate().getPredicate().inverted()?getRangeSet():getDomainSet(); + return !ConstraintDependence.rulesensurefunction(state,(RelationDescriptor)getDescriptor(), sd, getPredicate().getPredicate().inverted(), true); + } + public AbstractRepair(DNFPredicate dp,int typ, Descriptor d, Sources s) { torepair=dp; type=typ; diff --git a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java index cd3eb99..ae1ac7a 100755 --- a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java +++ b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java @@ -199,13 +199,15 @@ public class ConstraintDependence { SetQuantifier sq=(SetQuantifier)q; if (ve.getVar()!=sq.getVar()) return false; - if (!sq.getSet().isSubset(f.getSet())) - return false; - if (!(((r.getGuardExpr() instanceof BooleanLiteralExpr)&& - ((BooleanLiteralExpr)r.getGuardExpr()).getValue()==true))||isPartial) - return false; + if (!isPartial) { + if (!sq.getSet().isSubset(f.getSet())) + return false; + if (!((r.getGuardExpr() instanceof BooleanLiteralExpr)&& + ((BooleanLiteralExpr)r.getGuardExpr()).getValue()==true)) + return false; + } Expr e2=f.isInverse()?ri.getLeftExpr():ri.getRightExpr(); - if (e2.isSafe()) + if (isPartial||e2.isSafe()) foundrule=true; else return false; diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java index 3a5d56f..16a51f7 100755 --- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java +++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java @@ -359,7 +359,7 @@ public class GraphAnalysis { if (!containsgn3) cantremove.remove(gn3); } - if (ismodify&&((numadd==0)||(numremove==0))) { + if (ismodify&&((numadd==0)||(numremove==0&&ar.needsRemoves(termination.state)))) { for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) { GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next(); GraphNode gn3=e2.getTarget(); @@ -529,7 +529,7 @@ public class GraphAnalysis { numremove++; } } - if ((numadd==0)||(numremove==0)) { + if ((numadd==0)||(numremove==0&&ar.needsRemoves(termination.state))) { for(Iterator it2=gn.edges();it2.hasNext();) { GraphNode.Edge edge=(GraphNode.Edge)it2.next(); GraphNode gn2=edge.getTarget(); diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java index c096372..79b89a6 100755 --- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java +++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java @@ -753,13 +753,7 @@ public class RepairGenerator { } private void generate_checks() { - /* do constraint checks */ - // Vector constraints = state.vConstraints; - - - // for (int i = 0; i < constraints.size(); i++) { - // Constraint constraint = (Constraint) constraints.elementAt(i); Iterator i; if (Compiler.REPAIR) i=termination.constraintdependence.computeOrdering().iterator(); @@ -845,14 +839,14 @@ public class RepairGenerator { p.generate(cr,predvalue); if (k==0) cr.outputline("int "+costvar.getSafeSymbol()+"=0;"); - + if (negate) cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")"); else cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")"); cr.outputline(costvar.getSafeSymbol()+"+="+cost.getCost(dpred)+";"); } - + if(!first) { cr.outputline("if ("+costvar.getSafeSymbol()+"<"+mincost.getSafeSymbol()+")"); cr.startblock(); @@ -868,7 +862,6 @@ public class RepairGenerator { for(int j=0;jaddrelation("+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+");"); + + if (ar.needsRemoves(state)) + for(int i=0;iaddrelation("+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+");"); + } } } } - } /* Now do addition */ UpdateNode un=munadd.getUpdate(0); String name=(String)updatenames.get(un); diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java index 5e4bc91..d0197b5 100755 --- a/Repair/RepairCompiler/MCC/IR/Termination.java +++ b/Repair/RepairCompiler/MCC/IR/Termination.java @@ -547,7 +547,8 @@ public class Termination { generateremovefromsetrelation(gn,ar); } else if (ar.getType()==AbstractRepair.MODIFYRELATION) { /* Generate remove/add pairs */ - generateremovefromsetrelation(gn,ar); + if (ar.needsRemoves(state)) + generateremovefromsetrelation(gn,ar); generateaddtosetrelation(gn,ar); /* Generate atomic modify */ generatemodifyrelation(gn,ar); -- 2.34.1