Added a bug fix to the graphanalysis routine (must consider nodes not involved in cycles also for removal).
--- /dev/null
+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;
+ }
+ }
+}
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 */
}
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) {
}
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;
AbstractInterferes abstractinterferes;
ConstraintDependence constraintdependence;
ExactSize exactsize;
+ ArrayAnalysis arrayanalysis;
public Termination(State state) {
this.state=state;
maxsize=new ComputeMaxSize(state);
exactsize=new ExactSize(state);
+ arrayanalysis=new ArrayAnalysis(state,this);
abstractinterferes=new AbstractInterferes(this);
generateconjunctionnodes();
// 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
// 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);
[], 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
// 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;
+
// 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;
set RootDirectoryInode(int);
-set UsedBlock(int) : partition
+set UsedBlock(int) :
SuperBlock |
GroupBlock |
FileDirectoryBlock |
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);
-
-
-
-
-
-
-
projects / repair.git / commitdiff