Lots of bugfixes...

diff --git a/Repair/RepairCompiler/MCC/IR/ArrayAnalysis.java b/Repair/RepairCompiler/MCC/IR/ArrayAnalysis.java
index dc5f289b313b6f47b4cd30f4a8dad9c422744be1..bf26ad20dbf95f8baecc47389bdbeae9dfea3818 100755 (executable)
--- 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 456ef87360ea27ff14db6c884ac74d3cfc3d5ec4..42823cd12826248cc99618e184c8c856639cfc6a 100755 (executable)
--- 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;i<max;i++) {
            TypeDescriptor td=tdarray[i];
            Expr size=td.getSizeExpr();
@@ -310,6 +315,7 @@ public class RepairGenerator {
                }
            }
        }
+       cr.outputline("if (maybe) printf(\"BAD ERROR\");");
        cr.outputline("}");
     }
 
@@ -325,6 +331,7 @@ public class RepairGenerator {
                public SymbolTable getSymbolTable() { return st; }
            };
        cr.outputline("void "+name+"_state::recomputesizes() {");
+       cr.outputline("int maybe=0;");
        for(int i=0;i<max;i++) {
            TypeDescriptor td=tdarray[i];
            Expr size=td.getSizeExpr();
@@ -346,6 +353,7 @@ public class RepairGenerator {
                }
            }
        }
+       cr.outputline("if (maybe) printf(\"BAD ERROR\");");
        cr.outputline("}");
     }
 
@@ -1106,15 +1114,16 @@ public class RepairGenerator {
                    SetDescriptor sd=termination.sources.relgetSourceSet(rd,!ep.inverted());
                    VarDescriptor iterator=VarDescriptor.makeNew("iterator");
                    cr.outputline(sd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
-                   cr.outputline("for("+iterator.getSafeSymbol()+"="+sd.getSafeSymbol()+"_hash->iterator();"+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 d5cd1def9aa77a28d9b2d887a3e85733086be739..e119936aef078f8345fcaa5016efbecba5de5b20 100755 (executable)
--- 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 2687f51711fccbd80b51fd6b5f06f9f8ef515afa..da03dac5d3a3ac8db8a2a495c762b6980fa487db 100755 (executable)
--- 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;i<mun.numUpdates();i++) {
                UpdateNode un=mun.getUpdate(i);
-               for(int j=0;j<mun.numUpdates();j++) {
+               for(int j=0;j<un.numUpdates();j++) {
                    Updates u=un.getUpdate(j);
                    if (u.getType()==Updates.ABSTRACT) {
                        Expr e=u.getLeftExpr();

diff --git a/Repair/RepairCompiler/MCC/IR/UpdateNode.java b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
index 97ec85278329228bc73a1f1d5b5846f2089f7b88..bc669986eef83ecbc77021ec69373e0821551422 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/UpdateNode.java
+++ b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
@@ -504,7 +504,7 @@ class UpdateNode {
 
            if (b.getType()==Binding.SEARCH) {
                VarDescriptor vd=b.getVar();
-               cr.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"="+b.getSet().getSafeSymbol()+"->firstkey();");
+               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 1b5021d33507c0250f6e2bcd0283c92f91be65c7..89f9dc6bee8d8a4fb9e9ba4b07c05e3b9077ce34 100755 (executable)
--- 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 cde2dbc9d3702ab964d7a67bb125af13c5e693d1..42e959e9b94b1c5591727ec25bc185c936bf2b55 100755 (executable)
--- 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 fb4c2cf2b960e3da4874647232662c984b7fcb8b..2528d0ec92893eee5fce7d610c5a80bd5a2fbc12 100755 (executable)
--- 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)) => <node, node.next> 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) => <node, node.next> in nextnodes;