From: bdemsky <bdemsky>
Date: Tue, 27 Apr 2004 21:06:40 +0000 (+0000)
Subject: Added array analysis (computes paths used to add elements/tuples to sets/relations.
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=commitdiff_plain;h=803278c8eed228616a37dc70d17b391d7e220625;ds=sidebyside

Added array analysis (computes paths used to add elements/tuples to sets/relations.

Added a bug fix to the graphanalysis routine (must consider nodes not involved in cycles also for removal).
---

diff --git a/Repair/RepairCompiler/MCC/IR/ArrayAnalysis.java b/Repair/RepairCompiler/MCC/IR/ArrayAnalysis.java
new file mode 100755
index 0000000..4940d3b
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/ArrayAnalysis.java
@@ -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;
+	}
+    }
+}
diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
index e89898a..1e5a0ce 100755
--- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
@@ -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 */
 	    
diff --git a/Repair/RepairCompiler/MCC/IR/Sources.java b/Repair/RepairCompiler/MCC/IR/Sources.java
index 04203ba..d5cd1de 100755
--- a/Repair/RepairCompiler/MCC/IR/Sources.java
+++ b/Repair/RepairCompiler/MCC/IR/Sources.java
@@ -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;
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 1ec1dc2..751ff99 100755
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -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();
diff --git a/Repair/RepairCompiler/MCC/test2.constraints b/Repair/RepairCompiler/MCC/test2.constraints
index 44e92f6..bbc92e4 100755
--- a/Repair/RepairCompiler/MCC/test2.constraints
+++ b/Repair/RepairCompiler/MCC/test2.constraints
@@ -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);
diff --git a/Repair/RepairCompiler/MCC/test2.model b/Repair/RepairCompiler/MCC/test2.model
index 9784e28..78f8a9d 100755
--- a/Repair/RepairCompiler/MCC/test2.model
+++ b/Repair/RepairCompiler/MCC/test2.model
@@ -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;
+
diff --git a/Repair/RepairCompiler/MCC/test2.space b/Repair/RepairCompiler/MCC/test2.space
index bd84734..8b303c6 100755
--- a/Repair/RepairCompiler/MCC/test2.space
+++ b/Repair/RepairCompiler/MCC/test2.space
@@ -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);
-
-
-
-
-
-
-