Lots of bugfixes...
authorbdemsky <bdemsky>
Thu, 6 May 2004 02:05:51 +0000 (02:05 +0000)
committerbdemsky <bdemsky>
Thu, 6 May 2004 02:05:51 +0000 (02:05 +0000)
Repair/RepairCompiler/MCC/IR/ArrayAnalysis.java
Repair/RepairCompiler/MCC/IR/RepairGenerator.java
Repair/RepairCompiler/MCC/IR/Sources.java
Repair/RepairCompiler/MCC/IR/Termination.java
Repair/RepairCompiler/MCC/IR/UpdateNode.java
Repair/RepairCompiler/MCC/Runtime/size.h
Repair/RepairCompiler/MCC/ex.constraints
Repair/RepairCompiler/MCC/ex.model

index dc5f289..bf26ad2 100755 (executable)
@@ -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;
index 456ef87..42823cd 100755 (executable)
@@ -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*/
index d5cd1de..e119936 100755 (executable)
@@ -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();
index 2687f51..da03dac 100755 (executable)
@@ -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();
index 97ec852..bc66998 100755 (executable)
@@ -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());
index 1b5021d..89f9dc6 100755 (executable)
@@ -1,4 +1,4 @@
-#include "ex_aux.h"
+#include "test3_aux.h"
 class typeobject {
 public:
 typeobject();
index cde2dbc..42e959e 100755 (executable)
@@ -1 +1 @@
-[], sizeof(Nodes) >= literal(1);
+[], sizeof(Nodes) >= 1;
index fb4c2cf..2528d0e 100755 (executable)
@@ -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;