From: bdemsky Date: Thu, 6 May 2004 20:59:21 +0000 (+0000) Subject: Organizing X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=3469d127f4a400205edf2663a33e53258f934be7;p=repair.git Organizing --- diff --git a/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.constraints b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.constraints new file mode 100755 index 0000000..a6073fd --- /dev/null +++ b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.constraints @@ -0,0 +1,3 @@ + +[forall u in UsedInode], u.inodestatus=literal(Used); +[],sizeof(RootDirectoryInode)=1; \ No newline at end of file diff --git a/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.model b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.model new file mode 100755 index 0000000..2c4e062 --- /dev/null +++ b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.model @@ -0,0 +1 @@ +[], true => literal(0) in SuperBlock; diff --git a/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.space b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.space new file mode 100755 index 0000000..bd84734 --- /dev/null +++ b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.space @@ -0,0 +1,73 @@ +// sEXT2 - Simple File System Example +// Space Definition Language File + +set Block(int) : partition + UsedBlock | + FreeBlock; + +set FreeBlock(int); + +set Inode(int) : partition + UsedInode | + FreeInode; + +set FreeInode(int); + +set UsedInode(int) : partition + FileInode | + DirectoryInode ; + +set FileInode(int); + +set DirectoryInode(int) : RootDirectoryInode; + +set RootDirectoryInode(int); + +set UsedBlock(int) : partition + SuperBlock | + GroupBlock | + FileDirectoryBlock | + InodeTableBlock | + InodeBitmapBlock | + BlockBitmapBlock; + +set FileDirectoryBlock(int) : + DirectoryBlock | + FileBlock; + +set SuperBlock(int); + +set GroupBlock(int); + +set FileBlock(int); + +set DirectoryBlock(int); + +set InodeTableBlock(int); + +set InodeBitmapBlock(int); + +set BlockBitmapBlock(int); + +set DirectoryEntry(DirectoryEntry); + +// relations xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx + +inodeof: DirectoryEntry -> UsedInode (many->1); + +contents: UsedInode -> FileDirectoryBlock (1->many); + +inodestatus: Inode -> token (many->1); + +blockstatus: Block -> token (many->1); + +referencecount: Inode -> int (many->1); + +filesize: Inode -> int (many->1); + + + + + + + diff --git a/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.struct b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.struct new file mode 100755 index 0000000..c956e8b --- /dev/null +++ b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test.struct @@ -0,0 +1,3 @@ +structure Block { + reserved byte[d.s.blocksize]; +} \ No newline at end of file diff --git a/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.constraints b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.constraints new file mode 100755 index 0000000..bbc92e4 --- /dev/null +++ b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.constraints @@ -0,0 +1,66 @@ +// sEXT2 - Simple File System Example +// Constraint Definition Language File + +// Constraints 1-4 verify that the bitmaps and references to block's match up +// Constraints 5-6 verify that references counts and filesizes match up +// Constraints 7-13 are singleton tests + +// C1 +// for all used inodes, verify that the inodestatus (built from the +// inodebitmap is marked '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(false); + +// C3 +// for all used blocks, verify that the blockstatus (built from the +// blockbitmap is marked '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(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); + +// 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); + +// C7 +// ??? for all files and directory blocks check that +// only one inode references this block +//[forall b in FileDirectoryBlock],sizeof(b.~contents)=literal(1); + +// C8 +// verify that there is one superblock +//[],sizeof(SuperBlock)=literal(1); + +// C9 +// verify that there is one groupblock +//[],sizeof(GroupBlock)=literal(1); + +// C10 +// verify that there is one inodetableblock +//[],sizeof(InodeTableBlock)=literal(1); + +// C11 +// verify that there is one inodebitmapblock +[],sizeof(InodeBitmapBlock)=literal(1); + +// C12 +// verify that there is one blockbitmapblock +//[],sizeof(BlockBitmapBlock)=literal(1); + +// C13 +// verify that there is one rootdirectoryinode +//[],sizeof(RootDirectoryInode)=literal(1); diff --git a/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.model b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.model new file mode 100755 index 0000000..78f8a9d --- /dev/null +++ b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.model @@ -0,0 +1,96 @@ +// sEXT2 - Simple FileSystem Example - MODEL DEFINITION FILE + +// rule 1 - adds the block number of the superblock to the superblock set +[], literal(true) => literal(0) in SuperBlock; + +// rule 2 - adds the block number of the groupblock to the groupblock set +[], 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; + +// rule 4 - adds the inodebitmapblock block number to the inodebitmapblock set +[], 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; + +// rule 6 - adds the rootdirectoryinode number to the set +//[], 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; + +// rule 8 +delay [for j=literal(0) to d.s.NumberofBlocks-literal(1)], +!(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; + +// 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)) => +// in contents; + + +// rule 11 seems to be imperfect because it is adding directories and files +// to the filedirectoryblock but these automatically get funneled into +// fileblock (and hence the change below). Perhaps these should discriminate +// because otherwise, there is no direct use of DirectoryBlock (subset +// of FileDirectoryBlock) anywhere in the model definition at all. + +// 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] +//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. +[forall j in Inode, forall ibb in InodeBitmapBlock], literal(true) => in inodestatus; + +// rule 14 +// adds all non-zero inodenumbers of directory entries to the set +// FileInode +//[forall de in DirectoryEntry], de.inodenumber de.inodenumber in FileInode; + +// rule 15 +// builds up relation 'inodeof' such that means x is a +// directory entry with inode numbered y +//[forall de in DirectoryEntry], 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) => +// in referencecount; + +// rule 17 - populate the filesize relation with the sizes inodes' files +//[forall j in UsedInode, forall itb in InodeTableBlock], literal(true) => +// 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 +//[forall j in Block, forall bbb in BlockBitmapBlock], literal(true) => in blockstatus; + diff --git a/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.space b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.space new file mode 100755 index 0000000..8b303c6 --- /dev/null +++ b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.space @@ -0,0 +1,66 @@ +// sEXT2 - Simple File System Example +// Space Definition Language File + +set Block(int) : + UsedBlock | + FreeBlock; + +set FreeBlock(int); + +set Inode(int) : + UsedInode | + FreeInode; + +set FreeInode(int); + +set UsedInode(int) : partition + FileInode | + DirectoryInode ; + +set FileInode(int); + +set DirectoryInode(int) : RootDirectoryInode; + +set RootDirectoryInode(int); + +set UsedBlock(int) : + SuperBlock | + GroupBlock | + FileDirectoryBlock | + InodeTableBlock | + InodeBitmapBlock | + BlockBitmapBlock; + +set FileDirectoryBlock(int) : + DirectoryBlock | + FileBlock; + +set SuperBlock(int); + +set GroupBlock(int); + +set FileBlock(int); + +set DirectoryBlock(int); + +set InodeTableBlock(int); + +set InodeBitmapBlock(int); + +set BlockBitmapBlock(int); + +set DirectoryEntry(DirectoryEntry); + +// relations xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx + +inodeof: DirectoryEntry -> UsedInode (many->1); + +contents: UsedInode -> FileDirectoryBlock (1->many); + +inodestatus: Inode -> int (many->1); + +blockstatus: Block -> int (many->1); + +referencecount: Inode -> int (many->1); + +filesize: Inode -> int (many->1); diff --git a/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.struct b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.struct new file mode 100755 index 0000000..bf765ef --- /dev/null +++ b/Repair/RepairCompiler/MCC/specs/oldfilesystem/test2.struct @@ -0,0 +1,67 @@ +// sEXT2 - Simple File System Example +// Type Definition Language File + +// structures are assumed to be aligned to double-word +// boundaries. fields are tightly packed, so reserved bits +// can be used to add neccesary padding + +Disk *d; + +structure Block { + reserved byte[d.s.blocksize]; +} + +structure Disk { + Block b[d.s.NumberofBlocks]; + label b[literal(0)]: Superblock s; + label b[literal(1)]: Groupblock g; +} + +structure Superblock subtype of Block { + int FreeBlockCount; + int FreeInodeCount; + int NumberofBlocks; + int NumberofInodes; + int RootDirectoryInode; + int blocksize; +} + +structure Groupblock subtype of Block { + int BlockBitmapBlock; + int InodeBitmapBlock; + int InodeTableBlock; + int GroupFreeBlockCount; + int GroupFreeInodeCount; +} + +structure InodeTable subtype of Block { + Inode itable[d.s.NumberofInodes]; +} + +structure InodeBitmap subtype of Block { + bit inodebitmap[d.s.NumberofInodes]; +} + +structure BlockBitmap subtype of Block { + bit blockbitmap[d.s.NumberofBlocks]; +} + +structure Inode { + int filesize; + int Blockptr[literal(12)]; + int referencecount; +} + +structure DirectoryBlock subtype of Block { + DirectoryEntry de[d.s.blocksize/literal(128)]; +} + +structure DirectoryEntry { + byte name[literal(124)]; + int inodenumber; +} + + + + + diff --git a/Repair/RepairCompiler/MCC/test.constraints b/Repair/RepairCompiler/MCC/test.constraints deleted file mode 100755 index a6073fd..0000000 --- a/Repair/RepairCompiler/MCC/test.constraints +++ /dev/null @@ -1,3 +0,0 @@ - -[forall u in UsedInode], u.inodestatus=literal(Used); -[],sizeof(RootDirectoryInode)=1; \ No newline at end of file diff --git a/Repair/RepairCompiler/MCC/test.model b/Repair/RepairCompiler/MCC/test.model deleted file mode 100755 index 2c4e062..0000000 --- a/Repair/RepairCompiler/MCC/test.model +++ /dev/null @@ -1 +0,0 @@ -[], true => literal(0) in SuperBlock; diff --git a/Repair/RepairCompiler/MCC/test.space b/Repair/RepairCompiler/MCC/test.space deleted file mode 100755 index bd84734..0000000 --- a/Repair/RepairCompiler/MCC/test.space +++ /dev/null @@ -1,73 +0,0 @@ -// sEXT2 - Simple File System Example -// Space Definition Language File - -set Block(int) : partition - UsedBlock | - FreeBlock; - -set FreeBlock(int); - -set Inode(int) : partition - UsedInode | - FreeInode; - -set FreeInode(int); - -set UsedInode(int) : partition - FileInode | - DirectoryInode ; - -set FileInode(int); - -set DirectoryInode(int) : RootDirectoryInode; - -set RootDirectoryInode(int); - -set UsedBlock(int) : partition - SuperBlock | - GroupBlock | - FileDirectoryBlock | - InodeTableBlock | - InodeBitmapBlock | - BlockBitmapBlock; - -set FileDirectoryBlock(int) : - DirectoryBlock | - FileBlock; - -set SuperBlock(int); - -set GroupBlock(int); - -set FileBlock(int); - -set DirectoryBlock(int); - -set InodeTableBlock(int); - -set InodeBitmapBlock(int); - -set BlockBitmapBlock(int); - -set DirectoryEntry(DirectoryEntry); - -// relations xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx - -inodeof: DirectoryEntry -> UsedInode (many->1); - -contents: UsedInode -> FileDirectoryBlock (1->many); - -inodestatus: Inode -> token (many->1); - -blockstatus: Block -> token (many->1); - -referencecount: Inode -> int (many->1); - -filesize: Inode -> int (many->1); - - - - - - - diff --git a/Repair/RepairCompiler/MCC/test.struct b/Repair/RepairCompiler/MCC/test.struct deleted file mode 100755 index c956e8b..0000000 --- a/Repair/RepairCompiler/MCC/test.struct +++ /dev/null @@ -1,3 +0,0 @@ -structure Block { - reserved byte[d.s.blocksize]; -} \ No newline at end of file diff --git a/Repair/RepairCompiler/MCC/test2.constraints b/Repair/RepairCompiler/MCC/test2.constraints deleted file mode 100755 index bbc92e4..0000000 --- a/Repair/RepairCompiler/MCC/test2.constraints +++ /dev/null @@ -1,66 +0,0 @@ -// sEXT2 - Simple File System Example -// Constraint Definition Language File - -// Constraints 1-4 verify that the bitmaps and references to block's match up -// Constraints 5-6 verify that references counts and filesizes match up -// Constraints 7-13 are singleton tests - -// C1 -// for all used inodes, verify that the inodestatus (built from the -// inodebitmap is marked '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(false); - -// C3 -// for all used blocks, verify that the blockstatus (built from the -// blockbitmap is marked '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(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); - -// 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); - -// C7 -// ??? for all files and directory blocks check that -// only one inode references this block -//[forall b in FileDirectoryBlock],sizeof(b.~contents)=literal(1); - -// C8 -// verify that there is one superblock -//[],sizeof(SuperBlock)=literal(1); - -// C9 -// verify that there is one groupblock -//[],sizeof(GroupBlock)=literal(1); - -// C10 -// verify that there is one inodetableblock -//[],sizeof(InodeTableBlock)=literal(1); - -// C11 -// verify that there is one inodebitmapblock -[],sizeof(InodeBitmapBlock)=literal(1); - -// C12 -// verify that there is one blockbitmapblock -//[],sizeof(BlockBitmapBlock)=literal(1); - -// C13 -// verify that there is one rootdirectoryinode -//[],sizeof(RootDirectoryInode)=literal(1); diff --git a/Repair/RepairCompiler/MCC/test2.model b/Repair/RepairCompiler/MCC/test2.model deleted file mode 100755 index 78f8a9d..0000000 --- a/Repair/RepairCompiler/MCC/test2.model +++ /dev/null @@ -1,96 +0,0 @@ -// sEXT2 - Simple FileSystem Example - MODEL DEFINITION FILE - -// rule 1 - adds the block number of the superblock to the superblock set -[], literal(true) => literal(0) in SuperBlock; - -// rule 2 - adds the block number of the groupblock to the groupblock set -[], 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; - -// rule 4 - adds the inodebitmapblock block number to the inodebitmapblock set -[], 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; - -// rule 6 - adds the rootdirectoryinode number to the set -//[], 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; - -// rule 8 -delay [for j=literal(0) to d.s.NumberofBlocks-literal(1)], -!(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; - -// 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)) => -// in contents; - - -// rule 11 seems to be imperfect because it is adding directories and files -// to the filedirectoryblock but these automatically get funneled into -// fileblock (and hence the change below). Perhaps these should discriminate -// because otherwise, there is no direct use of DirectoryBlock (subset -// of FileDirectoryBlock) anywhere in the model definition at all. - -// 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] -//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. -[forall j in Inode, forall ibb in InodeBitmapBlock], literal(true) => in inodestatus; - -// rule 14 -// adds all non-zero inodenumbers of directory entries to the set -// FileInode -//[forall de in DirectoryEntry], de.inodenumber de.inodenumber in FileInode; - -// rule 15 -// builds up relation 'inodeof' such that means x is a -// directory entry with inode numbered y -//[forall de in DirectoryEntry], 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) => -// in referencecount; - -// rule 17 - populate the filesize relation with the sizes inodes' files -//[forall j in UsedInode, forall itb in InodeTableBlock], literal(true) => -// 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 -//[forall j in Block, forall bbb in BlockBitmapBlock], literal(true) => in blockstatus; - diff --git a/Repair/RepairCompiler/MCC/test2.model.dep b/Repair/RepairCompiler/MCC/test2.model.dep deleted file mode 100755 index 13befd7..0000000 --- a/Repair/RepairCompiler/MCC/test2.model.dep +++ /dev/null @@ -1,108 +0,0 @@ -// dependency information for -// testabstract from sEXT2 - -1-6: none - -7: delayed 14 -8: delayed 1 2 3 4 5 11 - - 9: 3 6 -10: 3 6 14 -11: 3 6 14 -12: 4 -13: 4 -14: 9 -15: 9 -16: 3 6 14 -17: 3 6 14 -18: 5 -19: 5 - - 9: 3 6 -10: 3 6 14 -11: 3 6 14 -12: 4 -13: 4 -14: 9 -15: 9 -16: 3 6 14 -17: 3 6 14 -18: 5 -19: 5 - - -algorithm: - -a. if quantifiers are empty than rule has no dependencies -b. if not ( x in Set ) or relation than dependent on everything that - touches the Set or Relation (also known as delayed). -c. otherwise, if set or relation mentioned in quantifier, edge between - that rule and any rule who modifies that set or relation (in the - inclusion constraint portion of any rule) - - -// dependency information betweeen constraints and rules - - 1: 6 12 13 14 - 2: 7 12 13 - 3: 1 2 3 4 5 11 18 19 - 4: 8 18 19 - 5: 6 14 15 16 - 6: 6 10 14 17 - 7: 10 11 - 8: 1 - 9: 2 -10: 3 -11: 4 -12: 5 -13: 6 - - 1: 6 12 13 14 - 2: 7 12 13 - 3: 1 2 3 4 5 11 18 19 - 4: 8 18 19 - 5: 6 14 15 16 - 6: 6 10 14 17 - 7: 10 11 - 8: 1 - 9: 2 -10: 3 -11: 4 -12: 5 -13: 6 - - -algorithm: - -a. if quantifier mentions a set, include all rules that touch that set - or its subsets/partitions -b. if the body mentions a set or relation, add that an edge to any rule - that touches those sets or relations - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/Repair/RepairCompiler/MCC/test2.space b/Repair/RepairCompiler/MCC/test2.space deleted file mode 100755 index 8b303c6..0000000 --- a/Repair/RepairCompiler/MCC/test2.space +++ /dev/null @@ -1,66 +0,0 @@ -// sEXT2 - Simple File System Example -// Space Definition Language File - -set Block(int) : - UsedBlock | - FreeBlock; - -set FreeBlock(int); - -set Inode(int) : - UsedInode | - FreeInode; - -set FreeInode(int); - -set UsedInode(int) : partition - FileInode | - DirectoryInode ; - -set FileInode(int); - -set DirectoryInode(int) : RootDirectoryInode; - -set RootDirectoryInode(int); - -set UsedBlock(int) : - SuperBlock | - GroupBlock | - FileDirectoryBlock | - InodeTableBlock | - InodeBitmapBlock | - BlockBitmapBlock; - -set FileDirectoryBlock(int) : - DirectoryBlock | - FileBlock; - -set SuperBlock(int); - -set GroupBlock(int); - -set FileBlock(int); - -set DirectoryBlock(int); - -set InodeTableBlock(int); - -set InodeBitmapBlock(int); - -set BlockBitmapBlock(int); - -set DirectoryEntry(DirectoryEntry); - -// relations xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx - -inodeof: DirectoryEntry -> UsedInode (many->1); - -contents: UsedInode -> FileDirectoryBlock (1->many); - -inodestatus: Inode -> int (many->1); - -blockstatus: Block -> int (many->1); - -referencecount: Inode -> int (many->1); - -filesize: Inode -> int (many->1); diff --git a/Repair/RepairCompiler/MCC/test2.struct b/Repair/RepairCompiler/MCC/test2.struct deleted file mode 100755 index bf765ef..0000000 --- a/Repair/RepairCompiler/MCC/test2.struct +++ /dev/null @@ -1,67 +0,0 @@ -// sEXT2 - Simple File System Example -// Type Definition Language File - -// structures are assumed to be aligned to double-word -// boundaries. fields are tightly packed, so reserved bits -// can be used to add neccesary padding - -Disk *d; - -structure Block { - reserved byte[d.s.blocksize]; -} - -structure Disk { - Block b[d.s.NumberofBlocks]; - label b[literal(0)]: Superblock s; - label b[literal(1)]: Groupblock g; -} - -structure Superblock subtype of Block { - int FreeBlockCount; - int FreeInodeCount; - int NumberofBlocks; - int NumberofInodes; - int RootDirectoryInode; - int blocksize; -} - -structure Groupblock subtype of Block { - int BlockBitmapBlock; - int InodeBitmapBlock; - int InodeTableBlock; - int GroupFreeBlockCount; - int GroupFreeInodeCount; -} - -structure InodeTable subtype of Block { - Inode itable[d.s.NumberofInodes]; -} - -structure InodeBitmap subtype of Block { - bit inodebitmap[d.s.NumberofInodes]; -} - -structure BlockBitmap subtype of Block { - bit blockbitmap[d.s.NumberofBlocks]; -} - -structure Inode { - int filesize; - int Blockptr[literal(12)]; - int referencecount; -} - -structure DirectoryBlock subtype of Block { - DirectoryEntry de[d.s.blocksize/literal(128)]; -} - -structure DirectoryEntry { - byte name[literal(124)]; - int inodenumber; -} - - - - -