Added array analysis (computes paths used to add elements/tuples to sets/relations.
authorbdemsky <bdemsky>
Tue, 27 Apr 2004 21:06:40 +0000 (21:06 +0000)
committerbdemsky <bdemsky>
Tue, 27 Apr 2004 21:06:40 +0000 (21:06 +0000)
Added a bug fix to the graphanalysis routine (must consider nodes not involved in cycles also for removal).

Repair/RepairCompiler/MCC/IR/ArrayAnalysis.java [new file with mode: 0755]
Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
Repair/RepairCompiler/MCC/IR/Sources.java
Repair/RepairCompiler/MCC/IR/Termination.java
Repair/RepairCompiler/MCC/test2.constraints
Repair/RepairCompiler/MCC/test2.model
Repair/RepairCompiler/MCC/test2.space

diff --git a/Repair/RepairCompiler/MCC/IR/ArrayAnalysis.java b/Repair/RepairCompiler/MCC/IR/ArrayAnalysis.java
new file mode 100755 (executable)
index 0000000..4940d3b
--- /dev/null
@@ -0,0 +1,177 @@
+package MCC.IR;
+import java.util.*;
+import MCC.State;
+
+public class ArrayAnalysis {
+    Termination termination;
+    State state;
+
+    public ArrayAnalysis(State state, Termination t) {
+       this.state=state;
+       this.termination=t;
+       this.set=new Hashtable();
+       this.leftrelation=new Hashtable();
+       this.rightrelation=new Hashtable();
+       
+       assert termination.exactsize!=null;
+       doAnalysis();
+    }
+
+    Hashtable set;
+    Hashtable leftrelation;
+    Hashtable rightrelation;
+
+    public AccessPath getSet(SetDescriptor sd) {
+       if (set.containsKey(sd))
+           return (AccessPath)set.get(sd);
+       return null;
+    }
+
+    
+    public AccessPath getDomain(RelationDescriptor rd) {
+       if (leftrelation.containsKey(rd))
+           return (AccessPath)leftrelation.get(rd);
+       return null;
+    }
+
+    public AccessPath getRange(RelationDescriptor rd) {
+       if (rightrelation.containsKey(rd))
+           return (AccessPath)rightrelation.get(rd);
+       return null;
+    }
+
+    private void doAnalysis() {
+       Vector rules=state.vRules;
+       for(int i=0;i<rules.size();i++) {
+           Rule r=(Rule)rules.get(i);
+           Inclusion inc=r.getInclusion();
+           if (inc instanceof SetInclusion) {
+               SetInclusion si=(SetInclusion)inc;
+
+               AccessPath oldap=set.containsKey(si.getSet())?(AccessPath)set.get(si.getSet()):null;
+               AccessPath newap=analyzeExpr(r,si.getExpr());
+               if (oldap==null) {
+                   set.put(si.getSet(),newap);
+               } else {
+                   if (!oldap.equals(newap))
+                       set.put(si.getSet(),AccessPath.NONE);
+               }
+           } else if (inc instanceof RelationInclusion) {
+               RelationInclusion ri=(RelationInclusion)inc;
+               
+               AccessPath oldapl=leftrelation.containsKey(ri.getRelation())?(AccessPath)leftrelation.get(ri.getRelation()):null;
+               AccessPath newapl=analyzeExpr(r,ri.getLeftExpr());
+               if (oldapl==null) {
+                   leftrelation.put(ri.getRelation(),newapl);
+               } else {
+                   if (!oldapl.equals(newapl))
+                       leftrelation.put(ri.getRelation(),AccessPath.NONE);
+               }
+
+               AccessPath oldapr=rightrelation.containsKey(ri.getRelation())?(AccessPath)rightrelation.get(ri.getRelation()):null;
+               AccessPath newapr=analyzeExpr(r,ri.getRightExpr());
+               if (oldapr==null) {
+                   rightrelation.put(ri.getRelation(),newapr);
+               } else {
+                   if (!oldapr.equals(newapr))
+                       rightrelation.put(ri.getRelation(),AccessPath.NONE);
+               }
+           } else throw new Error();
+       }
+    }
+
+    public AccessPath analyzeExpr(Rule r,Expr e) {
+       Vector dotvector=new Vector();
+       Expr ptr=e;
+       while(true) {
+           if (!(ptr instanceof DotExpr))
+               return null; /* Does something other than a dereference */
+           DotExpr de=(DotExpr)ptr;
+           dotvector.add(de);
+           ptr=de.left;
+           if (ptr instanceof VarExpr) {
+               VarExpr ve=(VarExpr)ptr;
+               VarDescriptor vd=ve.getVar();
+               AccessPath ap=new AccessPath();
+               if (vd.isGlobal()) {
+                   ap.startVar(vd);
+               } else {
+                   for(int i=0;i<r.numQuantifiers();i++) {
+                       Quantifier q=r.getQuantifier(i);
+                       if ((q instanceof SetQuantifier)&&
+                           ((SetQuantifier)q).getVar()==vd) {
+                           SetDescriptor sd=((SetQuantifier)q).getSet();
+                           int size=termination.exactsize.getsize(sd);
+                           if (size==1) {
+                               ap.startSet(sd);
+                               break;
+                           } else
+                               return AccessPath.NONE;
+                           
+                       }
+                   }
+                   if (!ap.setStart)
+                       return AccessPath.NONE;
+               }
+               /* Starting point finished - parse dereferences */
+               boolean foundarray=false;
+               for(int j=dotvector.size()-1;j>=0;j--) {
+                   DotExpr de2=(DotExpr) dotvector.get(j);
+                   FieldDescriptor fd=de2.getField();
+                   if (fd instanceof ArrayDescriptor) {
+                       foundarray=true;
+                       if (((ArrayDescriptor)fd).getField().getPtr())
+                           return AccessPath.NONE;
+                   } else {
+                       if (foundarray&&fd.getPtr())
+                           return AccessPath.NONE;
+                   }
+                   ap.addField(fd);
+               }
+               return ap;
+           }
+       }
+    }
+
+    public static class AccessPath {
+       public static final AccessPath NONE=new AccessPath();
+       
+       public AccessPath() {
+           path=new Vector();
+       }
+       boolean setStart;
+       SetDescriptor startset;
+       VarDescriptor startvar;
+
+       public void startSet(SetDescriptor sd) {
+           this.startset=sd;
+           setStart=true;
+       }
+
+       public void startVar(VarDescriptor vd) {
+           assert vd.isGlobal();
+           this.startvar=vd;
+           setStart=false;
+       }
+
+       Vector path;
+       public void addField(FieldDescriptor fd) {
+           path.add(fd);
+       }
+       public boolean equal(AccessPath ap) {
+           if (this==ap)
+               return true;
+           if (setStart&&this.startset!=ap.startset)
+               return false;
+           if ((!setStart)&&this.startvar!=ap.startvar)
+               return false;
+           if (this.path.size()!=ap.path.size())
+               return false;
+           for(int i=0;i<this.path.size();i++) {
+               if (this.path.get(i)!=ap.path.get(i))
+                   return false;
+           }
+           return true;
+       }
+    }
+}
index e89898a..1e5a0ce 100755 (executable)
@@ -33,7 +33,7 @@ public class GraphAnalysis {
            couldremove.addAll(termination.conjunctions);
            couldremove.addAll(termination.updatenodes);
            couldremove.addAll(termination.consequencenodes);
-           couldremove.retainAll(cycles);
+           couldremove.retainAll(nodes);
 
            /* Look for constraints which can only be satisfied one way */
            
index 04203ba..d5cd1de 100755 (executable)
@@ -10,12 +10,17 @@ public class Sources {
     }
 
     public boolean setSource(SetDescriptor sd) {
+       if (sd.getSymbol().equals("InodeBitmapBlock"))
+           return true;
+
        return false;
     }
     public boolean allocSource(SetDescriptor sd) {
-       return true;
+       return !setSource(sd);
     }
     public SetDescriptor getSourceSet(SetDescriptor sd) {
+       if (sd.getSymbol().equals("InodeBitmapBlock"))
+           return (SetDescriptor)state.stSets.get("FreeBlock");
        return null;
     }
     public void generateSourceAlloc(CodeWriter cr,VarDescriptor vd, SetDescriptor sd) {
@@ -29,13 +34,20 @@ public class Sources {
     }
 
     public boolean relsetSource(RelationDescriptor rd, boolean domain) {
-       return false;
+       if (domain)
+           return setSource(rd.getDomain());
+       else return setSource(rd.getRange());
     }
     public boolean relallocSource(RelationDescriptor rd, boolean domain) {
-       return true;
+       if (domain)
+           return allocSource(rd.getDomain());
+       else return allocSource(rd.getRange());
     }
+    
     public SetDescriptor relgetSourceSet(RelationDescriptor rd, boolean domain) {
-       return null;
+       if (domain)
+           return getSourceSet(rd.getDomain());
+       else return getSourceSet(rd.getRange());
     }
     public void relgenerateSourceAlloc(CodeWriter cr,VarDescriptor vd, RelationDescriptor rd, boolean domain) {
        SetDescriptor sd=null;
index 1ec1dc2..751ff99 100755 (executable)
@@ -28,6 +28,7 @@ public class Termination {
     AbstractInterferes abstractinterferes;
     ConstraintDependence constraintdependence;
     ExactSize exactsize;
+    ArrayAnalysis arrayanalysis;
 
     public Termination(State state) {
        this.state=state;
@@ -56,6 +57,7 @@ public class Termination {
 
        maxsize=new ComputeMaxSize(state);
        exactsize=new ExactSize(state);
+       arrayanalysis=new ArrayAnalysis(state,this);
 
        abstractinterferes=new AbstractInterferes(this);
        generateconjunctionnodes();
index 44e92f6..bbc92e4 100755 (executable)
@@ -8,50 +8,50 @@
 // C1
 // for all used inodes, verify that the inodestatus (built from the
 // inodebitmap is marked 'used'
-[forall u in UsedInode], u.inodestatus=literal(Used);
+//[forall u in UsedInode], u.inodestatus=literal(true);
 
 // C2
 // for all free inodes, verify that the inodestatus (built from the 
 // inodebitmap is marked 'free'
-[forall f in FreeInode], f.inodestatus=literal(Free);
+//[forall f in FreeInode], f.inodestatus=literal(false);
 
 // C3
 // for all used blocks, verify that the blockstatus (built from the
 // blockbitmap is marked 'used'
-[forall u in UsedBlock], u.blockstatus=literal(Used);
+//[forall u in UsedBlock], u.blockstatus=literal(true);
 
 // C4
 // for all free blocks, verify that the blockstatus (built from the
 // block bitmap is marked 'free'
-[forall f in FreeBlock], f.blockstatus=literal(Free);
+//[forall f in FreeBlock], f.blockstatus=literal(false);
 
 // C5
 // for all used inodes, verify that the reference count is equal to
 // the number of directory entries (files/links) that refer to that
 // inode
-[forall i in UsedInode], i.referencecount=sizeof(i.~inodeof);
+//[forall i in UsedInode], i.referencecount=sizeof(i.~inodeof);
 
 // C6
 // for all used inodes, verify that the filesize is consistent with
 // the number of blocks used (those in i.contents)
-[forall i in UsedInode], i.filesize <= sizeof(i.contents)*literal(8192);
+//[forall i in UsedInode], i.filesize <= sizeof(i.contents)*literal(8192);
 
 // C7
 // ??? for all files and directory blocks check that
 // only one inode references this block
-[forall b in FileDirectoryBlock],sizeof(b.~contents)=literal(1);
+//[forall b in FileDirectoryBlock],sizeof(b.~contents)=literal(1);
 
 // C8
 // verify that there is one superblock
-[],sizeof(SuperBlock)=literal(1);
+//[],sizeof(SuperBlock)=literal(1);
 
 // C9
 // verify that there is one groupblock
-[],sizeof(GroupBlock)=literal(1);
+//[],sizeof(GroupBlock)=literal(1);
 
 // C10
 // verify that there is one inodetableblock
-[],sizeof(InodeTableBlock)=literal(1);
+//[],sizeof(InodeTableBlock)=literal(1);
 
 // C11
 // verify that there is one inodebitmapblock 
@@ -59,8 +59,8 @@
 
 // C12
 // verify that there is one blockbitmapblock
-[],sizeof(BlockBitmapBlock)=literal(1);
+//[],sizeof(BlockBitmapBlock)=literal(1);
 
 // C13
 // verify that there is one rootdirectoryinode
-[],sizeof(RootDirectoryInode)=literal(1);
+//[],sizeof(RootDirectoryInode)=literal(1);
index 9784e28..78f8a9d 100755 (executable)
@@ -7,48 +7,46 @@
 [], literal(true) => literal(1) in GroupBlock;
 
 // rule 3 - adds the inodetableblock block number to the inodetableblock set
-[], d.g.InodeTableBlock < d.s.NumberofBlocks => 
-d.g.InodeTableBlock in InodeTableBlock; 
+//[], d.g.InodeTableBlock < d.s.NumberofBlocks => 
+//d.g.InodeTableBlock in InodeTableBlock;
 
 // rule 4 - adds the inodebitmapblock block number to the inodebitmapblock set
-[], d.g.InodeBitmapBlock < d.s.NumberofBlocks => 
-d.g.InodeBitmapBlock in InodeBitmapBlock; 
+[], literal(true) => d.g.InodeBitmapBlock in InodeBitmapBlock;
 
 // rule 5 - adds the blockbitmapblock number to the blockbitmapblock set
-[], d.g.BlockBitmapBlock < d.s.NumberofBlocks => 
-d.g.BlockBitmapBlock in BlockBitmapBlock; 
+//[], d.g.BlockBitmapBlock < d.s.NumberofBlocks => 
+//d.g.BlockBitmapBlock in BlockBitmapBlock;
 
 // rule 6 - adds the rootdirectoryinode number to the set
-[], d.s.RootDirectoryInode < d.s.NumberofInodes =>
-d.s.RootDirectoryInode in RootDirectoryInode; 
+//[], d.s.RootDirectoryInode < d.s.NumberofInodes =>
+//d.s.RootDirectoryInode in RootDirectoryInode;
 
 // rule 7 
 delay [for j=literal(0) to d.s.NumberofInodes-literal(1)], 
-!(j in? UsedInode) => j in FreeInode; 
+!(j in? UsedInode) => j in FreeInode;
 
 // rule 8
 delay [for j=literal(0) to d.s.NumberofBlocks-literal(1)], 
-!(j in? UsedBlock) => j in FreeBlock; 
+!(j in? UsedBlock) => j in FreeBlock;
 
 // rule 9
 // for all directoryinodes, loop through there blockptr's and then add
 // all their directoryentries to DirectoryEntry set
-[forall di in DirectoryInode, 
- forall itb in InodeTableBlock, 
- for j=literal(0) to (d.s.blocksize/literal(128))-literal(1), 
- for k=literal(0) to literal(11)], 
- cast(InodeTable,d.b[itb]).itable[di].Blockptr[k] < d.s.NumberofBlocks =>
- cast(DirectoryBlock,d.b[cast(InodeTable,d.b[itb]).itable[di].Blockptr[k]]).de[j]
- in DirectoryEntry;
+//[forall di in DirectoryInode, forall itb in InodeTableBlock, 
+// for j=literal(0) to (d.s.blocksize/literal(128))-literal(1), 
+// for k=literal(0) to literal(11)], 
+// cast(InodeTable,d.b[itb]).itable[di].Blockptr[k] < d.s.NumberofBlocks =>
+// cast(DirectoryBlock,d.b[cast(InodeTable,d.b[itb]).itable[di].Blockptr[k]]).de[j]
+// in DirectoryEntry;
 
 // rule 10
 // all non-zero blocks in an used inodes blockptr list should be 
 // added to the contents relation 
-[forall i in UsedInode, 
- forall itb in InodeTableBlock, 
- for j=literal(0) to literal(11)],
-     !(cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]=literal(0)) =>
-     <i,cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]> in contents; 
+//[forall i in UsedInode, 
+// forall itb in InodeTableBlock, 
+// for j=literal(0) to literal(11)],
+//     !(cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]=literal(0)) =>
+//     <i,cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]> in contents;
 
 
 // rule 11 seems to be imperfect because it is adding directories and files
@@ -60,55 +58,39 @@ delay [for j=literal(0) to d.s.NumberofBlocks-literal(1)],
 // rule 11 
 // for each inode in use, add non-zero, valid blocks mentioned in the 
 // inode's blockptr list in the inodetableblock to fileblock
-[forall i in UsedInode, forall itb in InodeTableBlock, for j=literal(0) to literal(11)],
-cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]<d.s.NumberofBlocks and
-!(cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]=literal(0)) =>
-cast(InodeTable,d.b[itb]).itable[i].Blockptr[j] in FileBlock; // was FileDirectoryBlock
-
-// rule 12
-// if the bit in the inodebitmap is 0 then that inode is marked as
-// free in the inodestatus relation
-[for j=literal(0) to d.s.NumberofInodes-literal(1), forall ibb in InodeBitmapBlock],
-cast(InodeBitmap,d.b[ibb]).inodebitmap[j]=literal(false) =>
-<j,literal(Free)> in inodestatus; 
+//[forall i in UsedInode, forall itb in InodeTableBlock, for j=literal(0) to literal(11)],
+//cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]<d.s.NumberofBlocks and
+//!(cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]=literal(0)) =>
+//cast(InodeTable,d.b[itb]).itable[i].Blockptr[j] in FileBlock;
+// was FileDirectoryBlock
 
 // rule 13
-// same as rule 12/19, but instead with used inodes. 
-[for j=literal(0) to d.s.NumberofInodes-literal(1), forall ibb in InodeBitmapBlock],
-cast(InodeBitmap,d.b[ibb]).inodebitmap[j]=literal(true) =>
-<j,literal(Used)> in inodestatus; 
+// same as rule 12/19, but instead with used inodes.
+[forall j in Inode, forall ibb in InodeBitmapBlock], literal(true) => <j, cast(InodeBitmap,d.b[ibb]).inodebitmap[j]> in inodestatus;
 
 // rule 14
 // adds all non-zero inodenumbers of directory entries to the set
 // FileInode
-[forall de in DirectoryEntry], de.inodenumber<d.s.NumberofInodes and
-!(de.inodenumber = literal(0)) => de.inodenumber in FileInode; 
+//[forall de in DirectoryEntry], de.inodenumber<d.s.NumberofInodes and
+//!(de.inodenumber = literal(0)) => de.inodenumber in FileInode;
 
 // rule 15
 // builds up relation 'inodeof' such that <x,y> means x is a
 // directory entry with inode numbered y
-[forall de in DirectoryEntry], de.inodenumber<d.s.NumberofInodes => 
-<de, de.inodenumber> in inodeof; 
+//[forall de in DirectoryEntry], de.inodenumber<d.s.NumberofInodes => 
+//<de, de.inodenumber> in inodeof;
 
 // rule 16
 // populating the referencecount relation with the referencecount 
 // values for every usedinode
-[forall j in UsedInode, forall itb in InodeTableBlock], literal(true) =>
-<j,cast(InodeTable,d.b[itb]).itable[j].referencecount> in referencecount; 
+//[forall j in UsedInode, forall itb in InodeTableBlock], literal(true) =>
+//<j,cast(InodeTable,d.b[itb]).itable[j].referencecount> in referencecount;
 
 // rule 17 - populate the filesize relation with the sizes inodes' files
-[forall j in UsedInode, forall itb in InodeTableBlock], literal(true) =>
-<j,cast(InodeTable,d.b[itb]).itable[j].filesize> in filesize; 
+//[forall j in UsedInode, forall itb in InodeTableBlock], literal(true) =>
+//<j,cast(InodeTable,d.b[itb]).itable[j].filesize> in filesize;
 
 // rule - similar to rule 19, if the bit in the block bitmap is 0 the that
 // block is marked as free in the blockstatus relation
-[for j=literal(0) to d.s.NumberofBlocks-literal(1), forall bbb in BlockBitmapBlock],
-cast(BlockBitmap,d.b[bbb]).blockbitmap[j]=literal(false) =>
-<j,literal(Free)> in blockstatus; 
-
-// rule 19
-// if the bit in the blockbitmap is 1 then that block is marked as 
-// used in the blockstatus relation
-[for j=literal(0) to d.s.NumberofBlocks-literal(1), forall bbb in BlockBitmapBlock],
-cast(BlockBitmap,d.b[bbb]).blockbitmap[j]=literal(true) =>
-<j,literal(Used)> in blockstatus; 
+//[forall j in Block, forall bbb in BlockBitmapBlock], literal(true) => <j,cast(BlockBitmap,d.b[bbb]).blockbitmap[j]> in blockstatus;
+
index bd84734..8b303c6 100755 (executable)
@@ -1,13 +1,13 @@
 // sEXT2 - Simple File System Example
 // Space Definition Language File
 
-set Block(int) : partition 
+set Block(int) :
     UsedBlock | 
     FreeBlock;
 
 set FreeBlock(int);
 
-set Inode(int) : partition 
+set Inode(int) :
     UsedInode | 
     FreeInode;
 
@@ -23,7 +23,7 @@ set DirectoryInode(int) : RootDirectoryInode;
 
 set RootDirectoryInode(int);
 
-set UsedBlock(int) : partition 
+set UsedBlock(int) :
     SuperBlock | 
     GroupBlock | 
     FileDirectoryBlock | 
@@ -57,17 +57,10 @@ inodeof: DirectoryEntry -> UsedInode (many->1);
 
 contents: UsedInode -> FileDirectoryBlock (1->many);
 
-inodestatus: Inode -> token (many->1);
+inodestatus: Inode -> int (many->1);
 
-blockstatus: Block -> token (many->1);
+blockstatus: Block -> int (many->1);
 
 referencecount: Inode -> int (many->1);
 
 filesize: Inode -> int (many->1);
-
-
-
-
-
-
-