From 30816378d0198b3cdeac43ad5bf80df3b7646406 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Sat, 10 Jan 2004 05:00:03 +0000 Subject: [PATCH] Fixed lot of random bugs. Added code generate strings for expr's. More code to generate concrete updates. Initial code for computing interference.... --- Repair/RepairCompiler/MCC/Compiler.java | 2 +- .../RepairCompiler/MCC/IR/AbstractRepair.java | 17 + Repair/RepairCompiler/MCC/IR/Binding.java | 8 +- .../MCC/IR/BooleanLiteralExpr.java | 15 +- Repair/RepairCompiler/MCC/IR/CastExpr.java | 10 +- .../MCC/IR/ConcreteInterferes.java | 28 +- Repair/RepairCompiler/MCC/IR/Conjunction.java | 10 +- .../RepairCompiler/MCC/IR/DNFConstraint.java | 2 +- .../RepairCompiler/MCC/IR/DNFPredicate.java | 8 + Repair/RepairCompiler/MCC/IR/DNFRule.java | 2 +- Repair/RepairCompiler/MCC/IR/DotExpr.java | 64 ++- .../RepairCompiler/MCC/IR/ElementOfExpr.java | 20 +- Repair/RepairCompiler/MCC/IR/Expr.java | 14 +- .../RepairCompiler/MCC/IR/ExprPredicate.java | 4 + Repair/RepairCompiler/MCC/IR/GraphNode.java | 10 +- .../RepairCompiler/MCC/IR/ImageSetExpr.java | 32 +- .../RepairCompiler/MCC/IR/ImplicitSchema.java | 7 +- Repair/RepairCompiler/MCC/IR/Inclusion.java | 1 + .../MCC/IR/InclusionPredicate.java | 5 +- .../MCC/IR/IntegerLiteralExpr.java | 13 +- .../RepairCompiler/MCC/IR/LogicStatement.java | 8 + .../RepairCompiler/MCC/IR/MetaInclusion.java | 4 + Repair/RepairCompiler/MCC/IR/OpExpr.java | 29 +- .../RepairCompiler/MCC/IR/RelationExpr.java | 23 +- .../MCC/IR/RelationFunctionExpr.java | 6 +- .../MCC/IR/RelationInclusion.java | 8 + .../MCC/IR/SemanticChecker.java | 2 +- Repair/RepairCompiler/MCC/IR/SetExpr.java | 19 +- .../RepairCompiler/MCC/IR/SetInclusion.java | 7 + Repair/RepairCompiler/MCC/IR/SizeofExpr.java | 13 +- .../RepairCompiler/MCC/IR/SizeofFunction.java | 4 + Repair/RepairCompiler/MCC/IR/Termination.java | 420 +++++++++++------- .../MCC/IR/TokenLiteralExpr.java | 16 +- Repair/RepairCompiler/MCC/IR/TupleOfExpr.java | 24 + Repair/RepairCompiler/MCC/IR/UpdateNode.java | 17 + Repair/RepairCompiler/MCC/IR/Updates.java | 42 +- Repair/RepairCompiler/MCC/IR/VarExpr.java | 32 ++ Repair/RepairCompiler/MCC/link.model | 8 +- 38 files changed, 730 insertions(+), 224 deletions(-) diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java index e87c112..df39d0f 100755 --- a/Repair/RepairCompiler/MCC/Compiler.java +++ b/Repair/RepairCompiler/MCC/Compiler.java @@ -68,7 +68,7 @@ public class Compiler { FileOutputStream dotfile; dotfile = new FileOutputStream(cli.infile + ".dependencies.edgelabels.dot"); GraphNode.useEdgeLabels = true; - GraphNode.DOTVisitor.visit(dotfile, nodes); + GraphNode.DOTVisitor.visit(dotfile, nodes); dotfile.close(); dotfile = new FileOutputStream(cli.infile + ".dependencies.dot"); diff --git a/Repair/RepairCompiler/MCC/IR/AbstractRepair.java b/Repair/RepairCompiler/MCC/IR/AbstractRepair.java index 037251a..01cba23 100755 --- a/Repair/RepairCompiler/MCC/IR/AbstractRepair.java +++ b/Repair/RepairCompiler/MCC/IR/AbstractRepair.java @@ -10,6 +10,23 @@ class AbstractRepair { DNFPredicate torepair; int type; Descriptor descriptor; + + public String type() { + switch(type) { + case ADDTOSET: + return "AddToSet"; + case REMOVEFROMSET: + return "RemoveToSet"; + case ADDTORELATION: + return "AddToRelation"; + case REMOVEFROMRELATION: + return "RemoveFromRelation"; + case MODIFYRELATION: + return "ModifyRelation"; + default: + return "Unknown"; + } + } public int getType() { return type; diff --git a/Repair/RepairCompiler/MCC/IR/Binding.java b/Repair/RepairCompiler/MCC/IR/Binding.java index 585107c..652c849 100755 --- a/Repair/RepairCompiler/MCC/IR/Binding.java +++ b/Repair/RepairCompiler/MCC/IR/Binding.java @@ -3,16 +3,20 @@ package MCC.IR; class Binding { VarDescriptor var; int position; - + boolean search; public Binding(VarDescriptor vd,int pos) { var=vd; position=pos; + search=false; } + public Binding(VarDescriptor vd) { + var=vd; + search=true; + } int getPosition() { return position; } - VarDescriptor getVar() { return var; } diff --git a/Repair/RepairCompiler/MCC/IR/BooleanLiteralExpr.java b/Repair/RepairCompiler/MCC/IR/BooleanLiteralExpr.java index be7eb88..7273818 100755 --- a/Repair/RepairCompiler/MCC/IR/BooleanLiteralExpr.java +++ b/Repair/RepairCompiler/MCC/IR/BooleanLiteralExpr.java @@ -1,6 +1,7 @@ package MCC.IR; import MCC.State; +import java.util.Map; public class BooleanLiteralExpr extends LiteralExpr { @@ -11,10 +12,20 @@ public class BooleanLiteralExpr extends LiteralExpr { td = ReservedTypeDescriptor.INT; } - public abstract boolean equals(Map remap, Expr e) { + public boolean usesDescriptor(Descriptor d) { + return false; + } + + public String name() { + if (value) + return "true"; + else return "false"; + } + + public boolean equals(Map remap, Expr e) { if (e==null) return false; - else if (!e instanceof BooleanLiteralExpr) + else if (!(e instanceof BooleanLiteralExpr)) return false; else return (((BooleanLiteralExpr)e).value==value); } diff --git a/Repair/RepairCompiler/MCC/IR/CastExpr.java b/Repair/RepairCompiler/MCC/IR/CastExpr.java index dc9c543..5b12c6d 100755 --- a/Repair/RepairCompiler/MCC/IR/CastExpr.java +++ b/Repair/RepairCompiler/MCC/IR/CastExpr.java @@ -12,12 +12,16 @@ public class CastExpr extends Expr { this.expr = expr; } - public abstract boolean equals(Map remap, Expr e) { + public boolean equals(Map remap, Expr e) { if (e==null) return false; - else if (!e instanceof CastExpr) + else if (!(e instanceof CastExpr)) return false; - else return ((this.type==((CastExpr)e).type)&&equals(remap,expr,((CastExpr)e).expr)); + else return ((this.type==((CastExpr)e).type)&&expr.equals(remap,((CastExpr)e).expr)); + } + + public boolean usesDescriptor(Descriptor d) { + return expr.usesDescriptor(d); } public Set getRequiredDescriptors() { diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java index e6718a6..aeaf4c9 100755 --- a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java +++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java @@ -6,14 +6,28 @@ class ConcreteInterferes { UpdateNode un=mun.getUpdate(i); for (int j=0;j Superblock, while, d.b ==> Block - fd = ld.getField(); - assert fd != null; - assert intindex == null; - intindex = ld.getIndex(); - } else { - fieldtype = fd.getType(); - intindex=index; - } - this.fd=fd; } public Set getRequiredDescriptors() { @@ -240,6 +255,25 @@ public class DotExpr extends Expr { public TypeDescriptor typecheck(SemanticAnalyzer sa) { TypeDescriptor lefttype = left.typecheck(sa); TypeDescriptor indextype = index == null ? null : index.typecheck(sa); + + { + /* finished typechecking...so we can fill the fields in */ + StructureTypeDescriptor struct = (StructureTypeDescriptor) left.getType(); + FieldDescriptor fd = struct.getField(field); + LabelDescriptor ld = struct.getLabel(field); + if (ld != null) { /* label */ + assert fd == null; + fieldtype = ld.getType(); // d.s ==> Superblock, while, d.b ==> Block + fd = ld.getField(); + assert fd != null; + assert intindex == null; + intindex = ld.getIndex(); + } else { + fieldtype = fd.getType(); + intindex=index; + } + this.fd=fd; + } if ((lefttype == null) || (index != null && indextype == null)) { return null; diff --git a/Repair/RepairCompiler/MCC/IR/ElementOfExpr.java b/Repair/RepairCompiler/MCC/IR/ElementOfExpr.java index 51941f9..1fdf42a 100755 --- a/Repair/RepairCompiler/MCC/IR/ElementOfExpr.java +++ b/Repair/RepairCompiler/MCC/IR/ElementOfExpr.java @@ -11,10 +11,28 @@ public class ElementOfExpr extends Expr { if (element == null || set == null) { throw new NullPointerException(); } - this.element = element; this.set = set; } + public boolean usesDescriptor(Descriptor d) { + if (d==set) + return true; + return element.usesDescriptor(d); + } + public String name() { + return element.name()+" in "+set.toString(); + } + + public boolean equals(Map remap, Expr e) { + if (e==null||!(e instanceof ElementOfExpr)) + return false; + ElementOfExpr eoe=(ElementOfExpr)e; + if (eoe.set!=set) + return false; + if (!element.equals(remap,eoe.element)) + return false; + return true; + } public Set getRequiredDescriptors() { Set v = element.getRequiredDescriptors(); diff --git a/Repair/RepairCompiler/MCC/IR/Expr.java b/Repair/RepairCompiler/MCC/IR/Expr.java index 77ccbc6..4e9d283 100755 --- a/Repair/RepairCompiler/MCC/IR/Expr.java +++ b/Repair/RepairCompiler/MCC/IR/Expr.java @@ -7,7 +7,7 @@ public abstract class Expr { TypeDescriptor td = null; public Expr() {} - + /* Remap this's variables using the remap mapping */ public abstract boolean equals(Map remap, Expr e); public abstract Set getRequiredDescriptors(); @@ -19,6 +19,10 @@ public abstract class Expr { return td; } + public String name() { + return "?"; + } + public abstract TypeDescriptor typecheck(SemanticAnalyzer sa); public abstract void prettyPrint(PrettyPrinter pp); @@ -36,15 +40,17 @@ public abstract class Expr { } public int[] getRepairs(boolean negated) { - return new int[0]; + System.out.println(this.getClass().getName()); + throw new Error("Unrecognized EXPR"); } public boolean inverted() { return false; } - public boolean usesDescriptor(RelationDescriptor rd) { - return false; + public boolean usesDescriptor(Descriptor rd) { + System.out.println(this.getClass().getName()); + throw new Error("UNIMPLEMENTED"); } } diff --git a/Repair/RepairCompiler/MCC/IR/ExprPredicate.java b/Repair/RepairCompiler/MCC/IR/ExprPredicate.java index 43ac5ad..04b223a 100755 --- a/Repair/RepairCompiler/MCC/IR/ExprPredicate.java +++ b/Repair/RepairCompiler/MCC/IR/ExprPredicate.java @@ -10,6 +10,10 @@ public class ExprPredicate extends Predicate { public static final int SIZE=1; public static final int COMPARISON=2; + public String name() { + return expr.name(); + } + public int getType() { if (((OpExpr)expr).left instanceof SizeofExpr) return SIZE; diff --git a/Repair/RepairCompiler/MCC/IR/GraphNode.java b/Repair/RepairCompiler/MCC/IR/GraphNode.java index 8059be3..fde26ad 100755 --- a/Repair/RepairCompiler/MCC/IR/GraphNode.java +++ b/Repair/RepairCompiler/MCC/IR/GraphNode.java @@ -171,11 +171,11 @@ public class GraphNode { private void make() { output.println("digraph dotvisitor {"); output.println("\trotate=90;"); - output.println("\tpage=\"8.5,11\";"); - output.println("\tnslimit=1000.0;"); - output.println("\tnslimit1=1000.0;"); - output.println("\tmclimit=1000.0;"); - output.println("\tremincross=true;"); + /* output.println("\tpage=\"8.5,11\";"); + output.println("\tnslimit=1000.0;"); + output.println("\tnslimit1=1000.0;"); + output.println("\tmclimit=1000.0;"); + output.println("\tremincross=true;");*/ output.println("\tnode [fontsize=10,height=\"0.1\", width=\"0.1\"];"); output.println("\tedge [fontsize=6];"); diff --git a/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java b/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java index 66437e3..152a4f8 100755 --- a/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java +++ b/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java @@ -3,9 +3,7 @@ package MCC.IR; import java.util.*; public class ImageSetExpr extends SetExpr { - - public static final boolean INVERSE = true; - + static final public boolean INVERSE=true; VarDescriptor vd; RelationDescriptor rd; boolean inverse; @@ -16,12 +14,36 @@ public class ImageSetExpr extends SetExpr { this.inverse = false; } + public String name() { + String name=vd.toString()+"."; + if (inverse) + name+="~"; + name+=rd.toString(); + return name; + } + public ImageSetExpr(boolean inverse, VarDescriptor vd, RelationDescriptor rd) { this.vd = vd; this.rd = rd; this.inverse = inverse; } + public boolean equals(Map remap, Expr e) { + if (e==null||!(e instanceof ImageSetExpr)) + return false; + ImageSetExpr ise=(ImageSetExpr)e; + if (ise.inverse!=inverse) + return false; + if (ise.rd!=rd) + return false; + VarDescriptor nvde=vd; + if (remap.containsKey(nvde)) + nvde=(VarDescriptor)remap.get(nvde); + if (nvde!=ise.vd) + return false; + return true; + } + public boolean inverted() { return inverse; } @@ -38,8 +60,8 @@ public class ImageSetExpr extends SetExpr { return rd; } - public boolean usesDescriptor(RelationDescriptor rd) { - return (rd==this.rd); + public boolean usesDescriptor(Descriptor d) { + return (d==rd)||(d==vd); } public Set getInversedRelations() { diff --git a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java index adea1ff..8d61947 100755 --- a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java +++ b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java @@ -24,8 +24,8 @@ public class ImplicitSchema { /* Construct quantifier */ RelationQuantifier rq=new RelationQuantifier(); - String varname1=new String("partitionvar1"); - String varname2=new String("partitionvar2"); + String varname1=new String("relationvar1"); + String varname2=new String("relationvar2"); VarDescriptor var1=new VarDescriptor(varname1); VarDescriptor var2=new VarDescriptor(varname2); c.getSymbolTable().add(var1); @@ -35,11 +35,9 @@ public class ImplicitSchema { rq.setTuple(var1,var2); rq.setRelation(rd); c.addQuantifier(rq); - VarExpr ve1=new VarExpr(varname1); SetExpr se1=new SetExpr(rd.getDomain()); LogicStatement incpred1=new InclusionPredicate(ve1,se1); - VarExpr ve2=new VarExpr(varname2); SetExpr se2=new SetExpr(rd.getRange()); LogicStatement incpred2=new InclusionPredicate(ve2,se2); @@ -54,7 +52,6 @@ public class ImplicitSchema { SetDescriptor sd=(SetDescriptor) setdescriptors.get(i); if(sd.isPartition()) { Constraint c=new Constraint(); - /* Construct quantifier */ SetQuantifier sq=new SetQuantifier(); String varname=new String("partitionvar"); diff --git a/Repair/RepairCompiler/MCC/IR/Inclusion.java b/Repair/RepairCompiler/MCC/IR/Inclusion.java index 0fe01da..8198b3f 100755 --- a/Repair/RepairCompiler/MCC/IR/Inclusion.java +++ b/Repair/RepairCompiler/MCC/IR/Inclusion.java @@ -13,6 +13,7 @@ public abstract class Inclusion { public abstract void generate(CodeWriter writer); public abstract boolean typecheck(SemanticAnalyzer sa); + public abstract boolean usesDescriptor(Descriptor d); } diff --git a/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java b/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java index e0d0d77..c27bb44 100755 --- a/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java +++ b/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java @@ -11,7 +11,10 @@ public class InclusionPredicate extends Predicate { return setexpr.inverted(); } - + public String name() { + return expr.name() + " in "+setexpr.name(); + } + public InclusionPredicate(Expr expr, SetExpr setexpr) { if (expr == null) { throw new NullPointerException(); diff --git a/Repair/RepairCompiler/MCC/IR/IntegerLiteralExpr.java b/Repair/RepairCompiler/MCC/IR/IntegerLiteralExpr.java index 49f52b5..e3f0d73 100755 --- a/Repair/RepairCompiler/MCC/IR/IntegerLiteralExpr.java +++ b/Repair/RepairCompiler/MCC/IR/IntegerLiteralExpr.java @@ -1,18 +1,27 @@ package MCC.IR; +import java.util.Map; public class IntegerLiteralExpr extends LiteralExpr { int value; + public boolean usesDescriptor(Descriptor d) { + return false; + } + public IntegerLiteralExpr(int value) { this.value = value; td = ReservedTypeDescriptor.INT; } - public abstract boolean equals(Map remap, Expr e) { + public String name() { + return (new Integer(value)).toString(); + } + + public boolean equals(Map remap, Expr e) { if (e==null) return false; - else if (!e instanceof IntegerLiteralExpr) + else if (!(e instanceof IntegerLiteralExpr)) return false; else return (((IntegerLiteralExpr)e).value==value); } diff --git a/Repair/RepairCompiler/MCC/IR/LogicStatement.java b/Repair/RepairCompiler/MCC/IR/LogicStatement.java index 6667422..aa093b4 100755 --- a/Repair/RepairCompiler/MCC/IR/LogicStatement.java +++ b/Repair/RepairCompiler/MCC/IR/LogicStatement.java @@ -8,6 +8,14 @@ public class LogicStatement { public static final Operation OR = new Operation("OR"); public static final Operation NOT = new Operation("NOT"); + public String name() { + String name=left.name(); + name+=op.toString(); + if (right!=null) + name+=right.name(); + return name; + } + public Set getInversedRelations() { if (left == null) { throw new IRException(); diff --git a/Repair/RepairCompiler/MCC/IR/MetaInclusion.java b/Repair/RepairCompiler/MCC/IR/MetaInclusion.java index 52ab078..3d00bbf 100755 --- a/Repair/RepairCompiler/MCC/IR/MetaInclusion.java +++ b/Repair/RepairCompiler/MCC/IR/MetaInclusion.java @@ -14,6 +14,10 @@ public class MetaInclusion extends Inclusion { constraints = new Vector(); } + public boolean usesDescriptor(Descriptor d) { + throw new Error("UNIMPLEMENTED"); + } + public Set getTargetDescriptors() { throw new IRException("unsupported"); } diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java index b3af827..f903a33 100755 --- a/Repair/RepairCompiler/MCC/IR/OpExpr.java +++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java @@ -16,10 +16,33 @@ public class OpExpr extends Expr { assert (right == null && opcode == Opcode.NOT) || (right != null); } + public String name() { + if (opcode==Opcode.NOT) + return "!("+left.name()+")"; + String name=left.name()+opcode.toString(); + if (right!=null) + name+=right.name(); + return name; + } + public Opcode getOpcode() { return opcode; } + public boolean equals(Map remap, Expr e) { + if (e==null||!(e instanceof OpExpr)) + return false; + OpExpr oe=(OpExpr)e; + if (opcode!=oe.opcode) + return false; + if (!left.equals(remap,oe.left)) + return false; + if (opcode!=Opcode.NOT) + if (!right.equals(remap,oe.right)) + return false; + return true; + } + public DNFRule constructDNF() { if (opcode==Opcode.AND) { DNFRule leftd=left.constructDNF(); @@ -35,12 +58,12 @@ public class OpExpr extends Expr { } else return new DNFRule(this); } - public boolean usesDescriptor(RelationDescriptor rd) { + public boolean usesDescriptor(Descriptor d) { if (opcode==Opcode.GT||opcode==Opcode.GE||opcode==Opcode.LT|| opcode==Opcode.LE||opcode==Opcode.EQ||opcode==Opcode.NE) - return right.usesDescriptor(rd); + return right.usesDescriptor(d); else - return left.usesDescriptor(rd)||(right!=null&&right.usesDescriptor(rd)); + return left.usesDescriptor(d)||(right!=null&&right.usesDescriptor(d)); } public int[] getRepairs(boolean negated) { diff --git a/Repair/RepairCompiler/MCC/IR/RelationExpr.java b/Repair/RepairCompiler/MCC/IR/RelationExpr.java index fc2a4c7..543b8e7 100755 --- a/Repair/RepairCompiler/MCC/IR/RelationExpr.java +++ b/Repair/RepairCompiler/MCC/IR/RelationExpr.java @@ -14,11 +14,32 @@ public class RelationExpr extends Expr { this.inverse = inverse; } + public String name() { + String name=expr.name()+"."; + if (inverse) + name+="~"; + name+=relation.toString(); + return name; + } + public Expr getExpr() { return expr; } - public boolean usesDescriptor(RelationDescriptor rd) { + public boolean equals(Map remap, Expr e) { + if (e==null||!(e instanceof RelationExpr)) + return false; + RelationExpr re=(RelationExpr)e; + if (re.relation!=relation) + return false; + if (!expr.equals(remap,re.expr)) + return false; + if (inverse!=re.inverse) + return false; + return true; + } + + public boolean usesDescriptor(Descriptor rd) { if (rd==relation) return true; else diff --git a/Repair/RepairCompiler/MCC/IR/RelationFunctionExpr.java b/Repair/RepairCompiler/MCC/IR/RelationFunctionExpr.java index cfbde5d..f7e37cf 100755 --- a/Repair/RepairCompiler/MCC/IR/RelationFunctionExpr.java +++ b/Repair/RepairCompiler/MCC/IR/RelationFunctionExpr.java @@ -17,6 +17,10 @@ public class RelationFunctionExpr extends Expr { this.rule = rule; } + public boolean equals(Map remap, Expr e) { + throw new Error("UNIMPLEMENTED!!!"); + } + public Descriptor getDescriptor() { return relation; } @@ -35,7 +39,7 @@ public class RelationFunctionExpr extends Expr { return v; } - public boolean usesDescriptor(RelationDescriptor rd) { + public boolean usesDescriptor(Descriptor rd) { if (rd==relation) return true; else diff --git a/Repair/RepairCompiler/MCC/IR/RelationInclusion.java b/Repair/RepairCompiler/MCC/IR/RelationInclusion.java index ab6a8d4..a2b40bc 100755 --- a/Repair/RepairCompiler/MCC/IR/RelationInclusion.java +++ b/Repair/RepairCompiler/MCC/IR/RelationInclusion.java @@ -17,6 +17,14 @@ public class RelationInclusion extends Inclusion { this.relation = relation; } + public boolean usesDescriptor(Descriptor d) { + if (d==relation) + return true; + else + return(leftelementexpr.usesDescriptor(d) + ||rightelementexpr.usesDescriptor(d)); + } + public Expr getLeftExpr() { return leftelementexpr; } diff --git a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java index 265663c..e94f7bd 100755 --- a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java +++ b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java @@ -474,7 +474,7 @@ public class SemanticChecker { /* return to caller */ return sq; - } else if (pn.getChild("relatiion") != null) { /* for < v1, v2 > in Relation */ + } else if (pn.getChild("relation") != null) { /* for < v1, v2 > in Relation */ RelationQuantifier rq = new RelationQuantifier(); /* get vars */ diff --git a/Repair/RepairCompiler/MCC/IR/SetExpr.java b/Repair/RepairCompiler/MCC/IR/SetExpr.java index b084b8e..d50c50e 100755 --- a/Repair/RepairCompiler/MCC/IR/SetExpr.java +++ b/Repair/RepairCompiler/MCC/IR/SetExpr.java @@ -9,7 +9,24 @@ public class SetExpr extends Expr { public SetExpr(SetDescriptor sd) { this.sd = sd; } - + + public String name() { + return sd.toString(); + } + + public boolean equals(Map remap, Expr e) { + if (e==null||!(e instanceof SetExpr)) + return false; + SetExpr se=(SetExpr)e; + if (sd!=se.sd) + return false; + return true; + } + + public boolean usesDescriptor(Descriptor s) { + return (s==sd); + } + public SetExpr() { this.sd = null; } diff --git a/Repair/RepairCompiler/MCC/IR/SetInclusion.java b/Repair/RepairCompiler/MCC/IR/SetInclusion.java index a9450d6..cdf67b2 100755 --- a/Repair/RepairCompiler/MCC/IR/SetInclusion.java +++ b/Repair/RepairCompiler/MCC/IR/SetInclusion.java @@ -18,6 +18,13 @@ public class SetInclusion extends Inclusion { this.set = set; } + public boolean usesDescriptor(Descriptor d) { + if (d==set) + return true; + else + return elementexpr.usesDescriptor(d); + } + public SetDescriptor getSet() { return set; } diff --git a/Repair/RepairCompiler/MCC/IR/SizeofExpr.java b/Repair/RepairCompiler/MCC/IR/SizeofExpr.java index 3d7f9ac..7570ddc 100755 --- a/Repair/RepairCompiler/MCC/IR/SizeofExpr.java +++ b/Repair/RepairCompiler/MCC/IR/SizeofExpr.java @@ -14,7 +14,18 @@ public class SizeofExpr extends Expr { this.setexpr = setexpr; } - public boolean usesDescriptor(RelationDescriptor rd) { + public String name() { + return "size("+setexpr.name()+")"; + } + + public boolean equals(Map remap, Expr e) { + if (e==null||!(e instanceof SizeofExpr)) + return false; + SizeofExpr soe=(SizeofExpr)e; + return setexpr.equals(remap,soe.setexpr); + } + + public boolean usesDescriptor(Descriptor rd) { return setexpr.usesDescriptor(rd); } diff --git a/Repair/RepairCompiler/MCC/IR/SizeofFunction.java b/Repair/RepairCompiler/MCC/IR/SizeofFunction.java index 1342cfd..45e63e7 100755 --- a/Repair/RepairCompiler/MCC/IR/SizeofFunction.java +++ b/Repair/RepairCompiler/MCC/IR/SizeofFunction.java @@ -18,6 +18,10 @@ public class SizeofFunction extends Expr { return new HashSet(); } + public boolean equals(Map remap,Expr e) { + throw new Error("UNIMPLEMENTED"); + } + public Set getRequiredDescriptors() { // because we don't actually use rd for any generation, we return the empty set return new HashSet(); diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java index 4d34f00..0b01ab9 100755 --- a/Repair/RepairCompiler/MCC/IR/Termination.java +++ b/Repair/RepairCompiler/MCC/IR/Termination.java @@ -60,7 +60,9 @@ public class Termination { DNFConstraint dnf=c.dnfconstraint; for(int j=0;j in "+relation.toString(); + } + + public boolean usesDescriptor(Descriptor d) { + if (d==relation) + return true; + else + return left.usesDescriptor(d)||right.usesDescriptor(d); + } + + public boolean equals(Map remap, Expr e) { + if (e==null||!(e instanceof TupleOfExpr)) + return false; + TupleOfExpr toe=(TupleOfExpr)e; + if (!left.equals(remap,toe.left)) + return false; + if (!right.equals(remap,toe.right)) + return false; + if (relation!=toe.relation) + return false; + return true; + } + public Set getRequiredDescriptors() { Set v = left.getRequiredDescriptors(); v.addAll(right.getRequiredDescriptors()); diff --git a/Repair/RepairCompiler/MCC/IR/UpdateNode.java b/Repair/RepairCompiler/MCC/IR/UpdateNode.java index 3a02c37..31e954c 100755 --- a/Repair/RepairCompiler/MCC/IR/UpdateNode.java +++ b/Repair/RepairCompiler/MCC/IR/UpdateNode.java @@ -4,16 +4,33 @@ import java.util.*; class UpdateNode { Vector updates; Vector bindings; + Hashtable binding; public UpdateNode() { updates=new Vector(); bindings=new Vector(); + binding=new Hashtable(); + } + + public void addBindings(Vector v) { + for (int i=0;i head in Nodes; -[forall node in Nodes], !node.next=literal(0) => node.next in Nodes; -[forall node in Nodes], !node.next=literal(0) => in nextnodes; -[forall node in Nodes], !node.prev=literal(0) => node.prev in Nodes; -[forall node in Nodes], !node.prev=literal(0) => in prevnodes; +[forall node in Nodes], !(node.next=literal(0)) => node.next in Nodes; +[forall node in Nodes], !(node.next=literal(0)) => in nextnodes; +[forall node in Nodes], !(node.prev=literal(0)) => node.prev in Nodes; +[forall node in Nodes], !(node.prev=literal(0)) => in prevnodes; -- 2.34.1