Hacks to allow repairs of fields used to define layouts of arrays.
authorbdemsky <bdemsky>
Mon, 17 Oct 2005 00:29:51 +0000 (00:29 +0000)
committerbdemsky <bdemsky>
Mon, 17 Oct 2005 00:29:51 +0000 (00:29 +0000)
Repair/RepairCompiler/MCC/CLI.java
Repair/RepairCompiler/MCC/CRuntime/instrument.c
Repair/RepairCompiler/MCC/CRuntime/instrument.h
Repair/RepairCompiler/MCC/CRuntime/memory.h
Repair/RepairCompiler/MCC/CRuntime/redblack.c
Repair/RepairCompiler/MCC/CRuntime/redblack.h
Repair/RepairCompiler/MCC/CRuntime/tmap.c
Repair/RepairCompiler/MCC/CRuntime/tmap.h
Repair/RepairCompiler/MCC/Compiler.java
Repair/RepairCompiler/MCC/IR/DotExpr.java

index 9b2e961..9f3badc 100755 (executable)
@@ -11,7 +11,7 @@ import MCC.IR.DebugItem;
  * files.
  *
  * @author  le01, 6.035 Staff (<tt>6.035-staff@mit.edu</tt>)
- * @version <tt>$Id: CLI.java,v 1.18 2005/10/14 18:31:41 bdemsky Exp $</tt>
+ * @version <tt>$Id: CLI.java,v 1.19 2005/10/17 00:29:13 bdemsky Exp $</tt>
  */
 public class CLI {
     /**
@@ -112,6 +112,8 @@ public class CLI {
            System.out.println("-debuggraph -- add edge labels and support to debug graph");
            System.out.println("-rejectlengthchanges -- reject all updates which change the length of an array");
            System.out.println("-printrepairs -- print log of repair actions");
+           System.out.println("-exactallocation -- application calls malloc for each struct and");
+           System.out.println("                    allocates exactly the right amount of space.");
 
            System.exit(-1);
        }
@@ -122,6 +124,8 @@ public class CLI {
                 debug = true;
            } else if (args[i].equals("-checkonly")) {
                 Compiler.REPAIR=false;
+           } else if (args[i].equals("-exactallocation")) {
+                Compiler.EXACTALLOCATION=true;
            } else if (args[i].equals("-omitcomp")) {
                 Compiler.OMITCOMP=true;
            } else if (args[i].equals("-debuggraph")) {
index dd1ccc0..8284975 100755 (executable)
@@ -8,6 +8,7 @@
 #include <stdio.h>
 #include "tmap.h"
 #include "size.h"
+#include <string.h>
 
 struct typemap * memmap;
 
@@ -44,6 +45,14 @@ void *ourrealloc(void *ptr, size_t size) {
   return orr;
 }
 
+char *ourstrdup(const char *ptr) {
+  char *new_ptr=strdup(ptr);
+  int length=strlen(ptr)+1;
+  typemapallocate(memmap,new_ptr,length);
+  return new_ptr;
+}
+
+
 void alloc(void *ptr,int size) {
   typemapallocate(memmap, ptr,size);
 }
@@ -67,6 +76,14 @@ bool assertvalidmemory(int ptr, int structure) {
   return typemapassertvalidmemory(memmap, (void *)ptr, structure);
 }
 
+bool assertexactmemory(int ptr, int structure) {
+  return typemapassertexactmemory(memmap, (void *)ptr, structure);
+}
+
+void * getendofblock(int ptr) {
+  return typemapgetendofblock(memmap, (void *)ptr);
+}
+
 void initializestack(void *high) {
   initializetypemapstack(memmap, high);
 }
index 7709e05..5e2ecb0 100755 (executable)
@@ -20,6 +20,9 @@ void initializemmap();
 void resettypemap();
 bool assertvalidtype(int ptr, int structure);
 bool assertvalidmemory(int ptr, int structure);
+bool assertexactmemory(int ptr, int structure);
+char *ourstrdup(const char *ptr);
+void * getendofblock(int ptr);
 void initializestack(void *);
 extern struct typemap * memmap;
 #endif
index 3a1c76b..4c8dbf5 100755 (executable)
@@ -5,5 +5,6 @@
 #define malloc(size) ourmalloc(size)
 #define calloc(memb,size) ourcalloc(memb,size)
 #define realloc(ptr,size) ourrealloc(ptr,size)
+#define strdup(str) ourstrdup(str)
 #define free(size) ourfree(size)
 #endif
index 98cf02a..840a4ec 100755 (executable)
@@ -1,4 +1,4 @@
-static char rcsid[]="$Id: redblack.c,v 1.2 2004/11/10 05:44:00 bdemsky Exp $";
+static char rcsid[]="$Id: redblack.c,v 1.3 2005/10/17 00:29:49 bdemsky Exp $";
 
 /*
    Redblack balanced tree algorithm
@@ -380,7 +380,7 @@ static struct rbnode * rb_lookup(const void *low, const void *high, struct rbtre
 
   /* walk x down the tree */
   while(x!=RBNULL) {
-    if (low<x->high&&
+    if (low<x->high &&
        x->key<high)
       return x;
     if (x->left!=RBNULL && x->left->max>low)
@@ -923,33 +923,28 @@ dumptree(struct rbnode *x, int n)
 
 /*
  * $Log: redblack.c,v $
- * Revision 1.2  2004/11/10 05:44:00  bdemsky
- *
+ * Revision 1.3  2005/10/17 00:29:49  bdemsky
  *
- * 1) Fixed some bugs in the redblack tree implementation...removing a non-present node resulted in a segfault.
  *
- * 2) Fixed bug in constructbindings method.
+ * Hacks to allow repairs of fields used to define layouts of arrays.
  *
- * Revision 1.1  2004/10/28 19:28:59  bdemsky
- * Checking in C runtime.
+ * Revision 1.1  2005/10/10 03:30:12  bdemsky
  *
- * Revision 1.2  2004/03/10 06:15:03  bdemsky
  *
+ * Checking in repair runtime and generated repair code for freeciv.
  *
- * Added:
- * Concrete Interference rule that falsify a rule that quantifies over a set can't
- * remove the last element of the set.
+ * Revision 1.2  2004/11/10 05:44:37  bdemsky
  *
- * Concrete Interference rule that updates that definitely falsify a rule can't modify
- * the inclusion condition causing a possible addition.
  *
- * Intelligence in the GraphAnalysis package that computes must & cant remove sets.
- * Search through only unique combinations.
+ * 1) Fixed some bugs in the redblack tree implementation...removing a non-present node resulted in a segfault.
  *
- * Revision 1.1  2004/03/07 22:02:43  bdemsky
+ * 2) Fixed bug in constructbindings method.
  *
+ * Revision 1.1  2004/10/28 19:29:04  bdemsky
+ * Checking in C runtime.
  *
- * Still buggy, but getting closer...
+ * Revision 1.1  2004/04/06 19:57:17  bdemsky
+ * Checking in redblack sources
  *
  * Revision 1.3  2003/06/18 06:06:18  bdemsky
  *
index 45c3394..ed10ff5 100755 (executable)
@@ -1,5 +1,5 @@
 /*
- * RCS $Id: redblack.h,v 1.1 2004/10/28 19:28:59 bdemsky Exp $
+ * RCS $Id: redblack.h,v 1.2 2005/10/17 00:29:49 bdemsky Exp $
  */
 
 /*
@@ -76,13 +76,21 @@ void rbcloselist(RBLIST *);
 /*
  *
  * $Log: redblack.h,v $
- * Revision 1.1  2004/10/28 19:28:59  bdemsky
- * Checking in C runtime.
+ * Revision 1.2  2005/10/17 00:29:49  bdemsky
+ *
+ *
+ * Hacks to allow repairs of fields used to define layouts of arrays.
  *
- * Revision 1.1  2004/03/07 22:02:43  bdemsky
+ * Revision 1.1  2005/10/10 03:30:12  bdemsky
  *
  *
- * Still buggy, but getting closer...
+ * Checking in repair runtime and generated repair code for freeciv.
+ *
+ * Revision 1.1  2004/10/28 19:29:04  bdemsky
+ * Checking in C runtime.
+ *
+ * Revision 1.1  2004/04/06 19:57:17  bdemsky
+ * Checking in redblack sources
  *
  * Revision 1.2  2003/06/18 06:06:18  bdemsky
  *
index 25c326d..56bac20 100755 (executable)
@@ -80,6 +80,26 @@ bool typemapassertvalidmemory(struct typemap * thisvar, void* low, int s) {
   return typemapassertvalidmemoryB(thisvar, low,((char *)low)+toadd);
 }
 
+bool typemapassertexactmemory(struct typemap * thisvar, void* low, int s) {
+  int toadd=sizeBytes(s);
+#ifdef CHECKMEMORY
+  {
+    void * high=((char *)low)+toadd;
+    struct pair allocp=rbfind(low,high,thisvar->alloctree);
+    if (allocp.low == NULL) {
+      return false;
+    } else if ((allocp.low != low) || (allocp.high != high)) {
+    /* make sure this block exactly lines up */
+      return false;
+    } else {
+      return true;
+    }
+  }
+#else
+  return true;
+#endif
+}
+
 bool typemapassertvalidmemoryB(struct typemap * thisvar, void* low, void* high) {
 #ifdef CHECKMEMORY
   return typemapcheckmemory(thisvar, low, high);
@@ -161,6 +181,17 @@ bool typemapcheckmemory(struct typemap *thisvar, void* low, void* high) {
   }
 }
 
+void * typemapgetendofblock(struct typemap *thisvar, void* low) {
+  struct pair allocp=rbfind(low,((char*)low)+1,thisvar->alloctree);
+  if (allocp.low == NULL) {
+    return NULL;
+  } else if ((allocp.low > low)||(allocp.high <= allocp.low)) { /* make sure this block is used */
+    return NULL;
+  } else {
+    return (void *)allocp.high;
+  }
+}
+
 
 bool typemapchecktype(struct typemap *thisvar, bool doaction,void *ptr, int structure) {
   int ssize=sizeBytes(structure);
index 535ecc5..7b607f6 100755 (executable)
@@ -25,9 +25,11 @@ void typemapdeallocate(struct typemap *, void *);
 bool typemapassertvalidmemoryB(struct typemap *, void* low, void* high);
 bool typemapasserttypeB(struct typemap *, void *ptr, void *high, int structure);
 bool typemapassertvalidmemory(struct typemap *, void* low, int structure);
+bool typemapassertexactmemory(struct typemap *, void* low, int structure);
 bool typemapasserttype(struct typemap *, void *ptr, int structure);
 bool typemapistype(struct typemap *, void *ptr, void *high, int structure);
 bool typemapcheckmemory(struct typemap *, void* low, void* high);
+void * typemapgetendofblock(struct typemap *thisvar, void* low);
 bool typemapchecktype(struct typemap *, bool doaction,void *ptr, int structure);
 bool typemapchecktypeB(struct typemap *, bool doaction, void *low, void *high,int structure, struct rbtree *ttree);
 int typemapfindoffsetstructure(struct typemap *, int s, int offset);
index 6151f2d..a53acc7 100755 (executable)
@@ -31,6 +31,7 @@ public class Compiler {
     public static boolean DEBUGGRAPH=false;
     public static boolean REJECTLENGTH=false;
     public static boolean PRINTREPAIRS=false;
+    public static boolean EXACTALLOCATION=false;
 
     public static Vector debuggraphs=new Vector();
 
index 5413302..8da5317 100755 (executable)
@@ -174,6 +174,31 @@ public class DotExpr extends Expr {
        return intindex;
     }
 
+    private boolean exactalloc(TypeDescriptor td) {
+        if (!(td instanceof StructureTypeDescriptor))
+            return false;
+        StructureTypeDescriptor std=(StructureTypeDescriptor)td;
+        if (std.size()!=1) /* Just looking for arrays */
+            return false;
+        FieldDescriptor tmpfd=std.get(0);
+        if (!(tmpfd instanceof ArrayDescriptor))
+            return false;
+        ArrayDescriptor afd=(ArrayDescriptor)tmpfd;
+        TypeDescriptor elementdescriptor=afd.getType();
+        Expr sizeexpr=elementdescriptor.getSizeExpr();
+        if (!OpExpr.isInt(sizeexpr))
+            return false;
+        Expr indexbound=afd.getIndexBound();
+        if (indexbound instanceof DotExpr)
+            return true;
+        if ((indexbound instanceof OpExpr)&&
+            (((OpExpr)indexbound).getOpcode()==Opcode.MULT)&&
+            (((OpExpr)indexbound).getLeftExpr() instanceof DotExpr)&&
+            (((OpExpr)indexbound).getRightExpr() instanceof DotExpr))
+            return true;
+        return false;
+    }
+
     public void generate(CodeWriter writer, VarDescriptor dest) {
         VarDescriptor leftd = VarDescriptor.makeNew("left");
 
@@ -300,24 +325,140 @@ public class DotExpr extends Expr {
            if (fd.getPtr()) {
                writer.outputline("if ("+dest.getSafeSymbol()+")");
                writer.startblock();
-               VarDescriptor typevar=VarDescriptor.makeNew("typechecks");
-               if (DOMEMCHECKS&&(!DOTYPECHECKS)) {
-                   writer.addDeclaration("bool", typevar.getSafeSymbol());
-                   writer.outputline(typevar.getSafeSymbol()+"=assertvalidmemory(" + dest.getSafeSymbol() + ", " + this.td.getId() + ");");
-                   dotypecheck = true;
-               } else if (DOTYPECHECKS) {
-                   writer.addDeclaration("bool", typevar.getSafeSymbol());
-                   writer.outputline(typevar.getSafeSymbol()+"=assertvalidtype(" + dest.getSafeSymbol() + ", " + this.td.getId() + ");");
-               }
+
 
                if (DOTYPECHECKS||DOMEMCHECKS) {
-                   writer.outputline("if (!"+typevar.getSafeSymbol()+")");
-                   writer.startblock();
-                   writer.outputline(dest.getSafeSymbol()+"=0;");
-                   if (DONULL)
-                       writer.outputline(ptr + "(" + leftd.getSafeSymbol() + " + " + offset.getSafeSymbol() + ")=0;");
-                   writer.endblock();
-               }
+                    /* NEED TO CHECK IF THERE ARE VARIABLES TO PLAY WITH IN THE STRUCT!!!! */
+                    if (Compiler.EXACTALLOCATION&&exactalloc(td)) {
+                        writer.outputline("if (!assertexactmemory("+dest.getSafeSymbol()+", "+this.td.getId()+"))");
+                        {
+                            writer.startblock();
+                            /* Okay, we've failed to fit it in here */
+
+                            VarDescriptor highptr=VarDescriptor.makeNew("highptr");
+                            writer.addDeclaration("int", highptr.getSafeSymbol());
+                            writer.outputline(highptr.getSafeSymbol()+"=getendofblock("+dest.getSafeSymbol()+");");
+                            VarDescriptor size=VarDescriptor.makeNew("size");
+                            writer.addDeclaration("int", size.getSafeSymbol());
+                            writer.outputline(size.getSafeSymbol()+"="+highptr.getSafeSymbol()+"-"+dest.getSafeSymbol()+";");
+
+                            StructureTypeDescriptor std=(StructureTypeDescriptor)this.td;
+                            ArrayDescriptor afd=(ArrayDescriptor)std.get(0);
+                            TypeDescriptor elementdescriptor=afd.getType();
+                            Expr sizeexpr=elementdescriptor.getSizeExpr();
+                            int elementsize=OpExpr.getInt(sizeexpr);
+                            //convert size to bytes
+                            if (elementsize%8==0)
+                                elementsize=elementsize/8;
+                            else
+                                elementsize=(elementsize/8)+1;
+                            /* Basic sanity check */
+                            writer.outputline("if ("+size.getSafeSymbol()+"%"+
+                                              elementsize+"==0)");
+                            {
+                                writer.startblock();
+                                VarDescriptor numElements=VarDescriptor.makeNew("numberofelements");
+                                writer.addDeclaration("int", numElements.getSafeSymbol());
+                                writer.outputline(numElements.getSafeSymbol()+"="+size.getSafeSymbol()+"/"+elementsize+";");
+                                Expr indexbound=afd.getIndexBound();
+                                if  (indexbound instanceof DotExpr) {
+                                /* NEED TO IMPLEMENT */
+
+                                    VarExpr ve=new VarExpr(numElements);
+                                    numElements.setType(ReservedTypeDescriptor.INT);
+                                    ve.td=ReservedTypeDescriptor.INT;
+                                    Updates u=new Updates(indexbound,ve);
+                                    UpdateNode un=new UpdateNode(null);
+                                    un.addUpdate(u);
+                                    un.generate(writer,false,false,null,null,null,null);
+                                    writer.outputline("break;");
+                                } else if ((indexbound instanceof OpExpr)&&
+                                           (((OpExpr)indexbound).getOpcode()==Opcode.MULT)&&
+                                           (((OpExpr)indexbound).getLeftExpr() instanceof DotExpr)&&
+                                           (((OpExpr)indexbound).getRightExpr() instanceof DotExpr)) {
+
+                                    DotExpr leftexpr=(DotExpr)(((OpExpr)indexbound).getLeftExpr());
+                                    VarDescriptor leftside=VarDescriptor.makeNew("leftvalue");
+                                    writer.addDeclaration("int", leftside.getSafeSymbol());
+                                    leftexpr.generate(writer,leftside);
+                                    DotExpr rightexpr=(DotExpr)(((OpExpr)indexbound).getRightExpr());
+                                    VarDescriptor rightside=VarDescriptor.makeNew("rightvalue");
+                                    writer.addDeclaration("int", rightside.getSafeSymbol());
+                                    rightexpr.generate(writer,rightside);
+                                    writer.outputline("if ("+numElements.getSafeSymbol()+"%"+leftside.getSafeSymbol()+"==0)");
+                                    {
+                                        writer.startblock();
+                                        VarDescriptor newvalue=VarDescriptor.makeNew("newvalue");
+                                        writer.addDeclaration("int", newvalue.getSafeSymbol());
+                                        writer.outputline(newvalue.getSafeSymbol()+"="+numElements.getSafeSymbol()+"/"+leftside.getSafeSymbol()+";");
+                                        VarExpr ve=new VarExpr(newvalue);
+                                        newvalue.setType(ReservedTypeDescriptor.INT);
+                                        ve.td=ReservedTypeDescriptor.INT;
+                                        Updates u=new Updates(rightexpr,ve);
+                                        UpdateNode un=new UpdateNode(null);
+                                        un.addUpdate(u);
+                                        un.generate(writer,false,false,null,null,null,null);
+                                        writer.outputline("break;");
+                                        writer.endblock();
+                                    }
+                                    writer.outputline("else if ("+numElements.getSafeSymbol()+"%"+rightside.getSafeSymbol()+"==0)");
+                                    {
+                                        writer.startblock();
+                                        VarDescriptor newvalue=VarDescriptor.makeNew("newvalue");
+                                        writer.addDeclaration("int", newvalue.getSafeSymbol());
+                                        writer.outputline(newvalue.getSafeSymbol()+"="+numElements.getSafeSymbol()+"/"+rightside.getSafeSymbol()+";");
+                                        VarExpr ve=new VarExpr(newvalue);
+                                        newvalue.setType(ReservedTypeDescriptor.INT);
+                                        ve.td=ReservedTypeDescriptor.INT;
+                                        Updates u=new Updates(leftexpr,ve);
+                                        UpdateNode un=new UpdateNode(null);
+                                        un.addUpdate(u);
+                                        un.generate(writer,false,false,null,null,null,null);
+                                        writer.outputline("break;");
+                                        writer.endblock();
+                                    }
+
+
+                                } else throw new Error("Should be here");
+
+                                writer.endblock();
+                            }
+
+                            writer.endblock();
+                        }
+                            /*
+
+                              if (indexbound instanceof DotExpr)
+                              return true;
+                              if ((indexbound instanceof OpExpr)&&
+                              (((OpExpr)indexbound).getOpcode()==Opcode.MULT)&&
+                              (((OpExpr)indexbound).getLeftExpr() instanceof DotExpr)&&
+                              (((OpExpr)indexbound).getRightExpr() instanceof DotExpr))
+                              return true;
+                              return false;
+                            */
+
+
+                            /* Give up and null out bad pointer */
+                    }
+                    VarDescriptor typevar=VarDescriptor.makeNew("typechecks");
+                    if (DOMEMCHECKS&&(!DOTYPECHECKS)) {
+                        writer.addDeclaration("bool", typevar.getSafeSymbol());
+                        writer.outputline(typevar.getSafeSymbol()+"=assertvalidmemory(" + dest.getSafeSymbol() + ", " + this.td.getId() + ");");
+                        dotypecheck = true;
+                    } else if (DOTYPECHECKS) {
+                        writer.addDeclaration("bool", typevar.getSafeSymbol());
+                        writer.outputline(typevar.getSafeSymbol()+"=assertvalidtype(" + dest.getSafeSymbol() + ", " + this.td.getId() + ");");
+                    }
+                    if (DOMEMCHECKS||DOTYPECHECKS) {
+                        writer.outputline("if (!"+typevar.getSafeSymbol()+")");
+                        writer.startblock();
+                        writer.outputline(dest.getSafeSymbol()+"=0;");
+                        if (DONULL)
+                            writer.outputline(ptr + "(" + leftd.getSafeSymbol() + " + " + offset.getSafeSymbol() + ")=0;");
+                        writer.endblock();
+                    }
+                }
 
                writer.endblock();
            }