From fca2f901d2ec73f9ff6902e35b827271cda87fbf Mon Sep 17 00:00:00 2001 From: bdemsky Date: Thu, 6 May 2004 02:05:51 +0000 Subject: [PATCH] Lots of bugfixes... --- .../RepairCompiler/MCC/IR/ArrayAnalysis.java | 6 +++-- .../MCC/IR/RepairGenerator.java | 26 +++++++++++++------ Repair/RepairCompiler/MCC/IR/Sources.java | 9 +++++++ Repair/RepairCompiler/MCC/IR/Termination.java | 2 +- Repair/RepairCompiler/MCC/IR/UpdateNode.java | 2 +- Repair/RepairCompiler/MCC/Runtime/size.h | 2 +- Repair/RepairCompiler/MCC/ex.constraints | 2 +- Repair/RepairCompiler/MCC/ex.model | 6 ++--- 8 files changed, 38 insertions(+), 17 deletions(-) diff --git a/Repair/RepairCompiler/MCC/IR/ArrayAnalysis.java b/Repair/RepairCompiler/MCC/IR/ArrayAnalysis.java index dc5f289..bf26ad2 100755 --- a/Repair/RepairCompiler/MCC/IR/ArrayAnalysis.java +++ b/Repair/RepairCompiler/MCC/IR/ArrayAnalysis.java @@ -207,11 +207,13 @@ public class ArrayAnalysis { } public boolean equal(AccessPath ap) { + if (ap==null) + return false; if (this==ap) return true; - if (setStart&&this.startset!=ap.startset) + if (this.setStart&&this.startset!=ap.startset) return false; - if ((!setStart)&&this.startvar!=ap.startvar) + if ((!this.setStart)&&this.startvar!=ap.startvar) return false; if (this.path.size()!=ap.path.size()) return false; diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java index 456ef87..42823cd 100755 --- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java +++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java @@ -86,7 +86,9 @@ public class RepairGenerator { generate_call(); generate_start(); generate_rules(); - generate_print(); + if (!Compiler.REPAIR) { + generate_print(); + } generate_checks(); generate_teardown(); CodeWriter crhead = new StandardCodeWriter(this.outputhead); @@ -115,6 +117,8 @@ public class RepairGenerator { int count=0; CodeWriter crhead = new StandardCodeWriter(outputhead); CodeWriter craux = new StandardCodeWriter(outputaux); + RelationDescriptor.prefix = "model->"; + SetDescriptor.prefix = "model->"; /* Rewrite globals */ @@ -287,6 +291,7 @@ public class RepairGenerator { }; cr.outputline("void "+name+"_state::computesizes(int *sizearray,int **numele) {"); + cr.outputline("int maybe=0;"); for(int i=0;iiterator();"+iterator.getSafeSymbol()+".hasNext();)"); + cr.outputline("SimpleIterator "+iterator.getSafeSymbol()+";"); + cr.outputline("for("+sd.getSafeSymbol()+"_hash->iterator("+ iterator.getSafeSymbol() +");"+iterator.getSafeSymbol()+".hasNext();)"); cr.startblock(); if (ep.inverted()) { - cr.outputline("if !"+rd.getSafeSymbol()+"_hashinv->contains("+iterator.getSafeSymbol()+"->key(),"+otherside.getSafeSymbol()+")"); + cr.outputline("if (!"+rd.getSafeSymbol()+"_hashinv->contains("+iterator.getSafeSymbol()+".key(),"+otherside.getSafeSymbol()+"))"); } else { - cr.outputline("if !"+rd.getSafeSymbol()+"_hash->contains("+otherside.getSafeSymbol()+","+iterator.getSafeSymbol()+"->key())"); + cr.outputline("if (!"+rd.getSafeSymbol()+"_hash->contains("+otherside.getSafeSymbol()+","+iterator.getSafeSymbol()+".key()))"); } cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();"); - cr.outputline(iterator.getSafeSymbol()+"->next();"); + cr.outputline(iterator.getSafeSymbol()+".next();"); cr.endblock(); } else if (termination.sources.relallocSource(rd,!ep.inverted())) { /* Allocation Source*/ @@ -1150,11 +1159,12 @@ public class RepairGenerator { SetDescriptor sourcesd=termination.sources.getSourceSet(sd); VarDescriptor iterator=VarDescriptor.makeNew("iterator"); cr.outputline(sourcesd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";"); - cr.outputline("for("+iterator.getSafeSymbol()+"="+sourcesd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)"); + cr.outputline("SimpleIterator "+iterator.getSafeSymbol()+";"); + cr.outputline("for("+sourcesd.getSafeSymbol()+"_hash->iterator("+iterator.getSafeSymbol()+");"+iterator.getSafeSymbol()+".hasNext();)"); cr.startblock(); - cr.outputline("if !"+sd.getSafeSymbol()+"_hash->contains("+iterator.getSafeSymbol()+"->key())"); + cr.outputline("if (!"+sd.getSafeSymbol()+"_hash->contains("+iterator.getSafeSymbol()+".key()))"); cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();"); - cr.outputline(iterator.getSafeSymbol()+"->next();"); + cr.outputline(iterator.getSafeSymbol()+".next();"); cr.endblock(); } else if (termination.sources.allocSource(sd)) { /* Allocation Source*/ diff --git a/Repair/RepairCompiler/MCC/IR/Sources.java b/Repair/RepairCompiler/MCC/IR/Sources.java index d5cd1de..e119936 100755 --- a/Repair/RepairCompiler/MCC/IR/Sources.java +++ b/Repair/RepairCompiler/MCC/IR/Sources.java @@ -12,6 +12,10 @@ public class Sources { public boolean setSource(SetDescriptor sd) { if (sd.getSymbol().equals("InodeBitmapBlock")) return true; + if (sd.getSymbol().equals("InodeTableBlock")) + return true; + if (sd.getSymbol().equals("RootDirectoryInode")) + return true; return false; } @@ -21,8 +25,13 @@ public class Sources { public SetDescriptor getSourceSet(SetDescriptor sd) { if (sd.getSymbol().equals("InodeBitmapBlock")) return (SetDescriptor)state.stSets.get("FreeBlock"); + if (sd.getSymbol().equals("InodeTableBlock")) + return (SetDescriptor)state.stSets.get("FreeBlock"); + if (sd.getSymbol().equals("RootDirectoryInode")) + return (SetDescriptor)state.stSets.get("FreeInode"); return null; } + public void generateSourceAlloc(CodeWriter cr,VarDescriptor vd, SetDescriptor sd) { TypeDescriptor td=sd.getType(); Expr e=td.getSizeExpr(); diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java index 2687f51..da03dac 100755 --- a/Repair/RepairCompiler/MCC/IR/Termination.java +++ b/Repair/RepairCompiler/MCC/IR/Termination.java @@ -192,7 +192,7 @@ public class Termination { MultUpdateNode mun=tn.getUpdate(); for(int i=0;ifirstkey();"); + cr.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"="+b.getSet().getSafeSymbol()+"_hash->firstkey();"); } else if (b.getType()==Binding.CREATE) { throw new Error("Creation not supported"); // source.generateSourceAlloc(cr,vd,b.getSet()); diff --git a/Repair/RepairCompiler/MCC/Runtime/size.h b/Repair/RepairCompiler/MCC/Runtime/size.h index 1b5021d..89f9dc6 100755 --- a/Repair/RepairCompiler/MCC/Runtime/size.h +++ b/Repair/RepairCompiler/MCC/Runtime/size.h @@ -1,4 +1,4 @@ -#include "ex_aux.h" +#include "test3_aux.h" class typeobject { public: typeobject(); diff --git a/Repair/RepairCompiler/MCC/ex.constraints b/Repair/RepairCompiler/MCC/ex.constraints index cde2dbc..42e959e 100755 --- a/Repair/RepairCompiler/MCC/ex.constraints +++ b/Repair/RepairCompiler/MCC/ex.constraints @@ -1 +1 @@ -[], sizeof(Nodes) >= literal(1); +[], sizeof(Nodes) >= 1; diff --git a/Repair/RepairCompiler/MCC/ex.model b/Repair/RepairCompiler/MCC/ex.model index fb4c2cf..2528d0e 100755 --- a/Repair/RepairCompiler/MCC/ex.model +++ b/Repair/RepairCompiler/MCC/ex.model @@ -1,5 +1,5 @@ -[], !(head=literal(0)) => 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; +[], !(head=0) => head in Nodes; +[forall node in Nodes], !(node.next=0) => node.next in Nodes; +[forall node in Nodes], !(node.next=0) => in nextnodes; -- 2.34.1