(op2==Opcode.LE)))
return false;
+ if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
+ ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
+ expr1.equals(null,expr2)) {
+ return false;
+ }
+
if (isInt1&&isInt2) {
if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
if (ri.getLeftExpr().isValue()) {
Updates up=new Updates(ri.getLeftExpr(),leftindex);
un.addUpdate(up);
- } else
- goodflag=false;
+ } else {
+ if (inverted)
+ goodflag=false;
+ else un.addInvariant(ri.getLeftExpr());
+ }
} else {
VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
if (vd.isGlobal()) {
if (ri.getRightExpr().isValue()) {
Updates up=new Updates(ri.getRightExpr(),rightindex);
un.addUpdate(up);
- } else
- goodflag=false;
+ } else {
+ if (!inverted)
+ goodflag=false;
+ else
+ un.addInvariant(ri.getLeftExpr());
+ }
} else {
VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
if (vd.isGlobal()) {
class UpdateNode {
Vector updates;
Vector bindings;
+ Vector invariants;
Hashtable binding;
Rule rule;
-
public UpdateNode(Rule r) {
updates=new Vector();
bindings=new Vector();
+ invariants=new Vector();
binding=new Hashtable();
rule=r;
}
public String toString() {
String st="";
+ st+="Bindings:\n";
for(int i=0;i<bindings.size();i++)
st+=bindings.get(i).toString()+"\n";
st+="---------------------\n";
+ st+="Updates:\n";
for(int i=0;i<updates.size();i++)
st+=updates.get(i).toString()+"\n";
+ st+="---------------------\n";
+ st+="Invariants:\n";
+ for(int i=0;i<invariants.size();i++)
+ st+=((Expr)invariants.get(i)).name()+"\n";
+ st+="---------------------\n";
return st;
}
-
+
public void addBindings(Vector v) {
for (int i=0;i<v.size();i++) {
addBinding((Binding)v.get(i));
Set toremove=new HashSet();
for(int i=0;i<updates.size();i++) {
Updates u1=(Updates)updates.get(i);
+ if (!u1.isAbstract()) {
+ Descriptor d=u1.getDescriptor();
+ for(int j=0;j<invariants.size();j++) {
+ Expr invariant=(Expr)invariants.get(j);
+ if (invariant.usesDescriptor(d))
+ return false;
+ }
+ }
for(int j=0;j<updates.size();j++) {
Updates u2=(Updates)updates.get(j);
if (i==j)
return null;
}
+ public void addInvariant(Expr e) {
+ invariants.add(e);
+ }
+
+ public int numInvariants() {
+ return invariants.size();
+ }
+
+ public Expr getInvariant(int i) {
+ return (Expr)invariants.get(i);
+ }
+
public void addUpdate(Updates u) {
updates.add(u);
}
--- /dev/null
+// 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=true;
+
+// C2
+// for all free inodes, verify that the inodestatus (built from the
+// inodebitmap is marked 'free'
+//[forall f in FreeInode], f.inodestatus=false;
+
+// C3
+// for all used blocks, verify that the blockstatus (built from the
+// blockbitmap is marked 'used'
+//[forall u in UsedBlock], u.blockstatus=true;
+
+// C4
+// for all free blocks, verify that the blockstatus (built from the
+// block bitmap is marked 'free'
+[forall f in FreeBlock], f.blockstatus=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)=1;
+
+// C9
+// verify that there is one groupblock
+//[],sizeof(GroupBlock)=1;
+
+// C10
+// verify that there is one inodetableblock
+/*[],sizeof(InodeTableBlock)=1;*/
+
+// C11
+// verify that there is one inodebitmapblock
+/*[],sizeof(InodeBitmapBlock)=1;*/
+
+// C12
+// verify that there is one blockbitmapblock
+[],sizeof(BlockBitmapBlock)=1;
+
+// C13
+// verify that there is one rootdirectoryinode
+/*[],sizeof(RootDirectoryInode)=1;*/
--- /dev/null
+// sEXT2 - Simple FileSystem Example - MODEL DEFINITION FILE
+// rule 1 - adds the block number of the superblock to the superblock set
+/*[], true => d.s in SuperBlock;*/
+
+// rule 2 - adds the block number of the groupblock to the groupblock set
+/*[], true => d.g in GroupBlock;*/
+
+/*[], true => cast(InodeTable,d.b[d.g.InodeTableBlock]) in InodeTableBlock;*/
+
+// rule 4 - adds the inodebitmapblock block number to the inodebitmapblock set
+/*[], true => cast(InodeBitmap,d.b[d.g.InodeBitmapBlock]) in InodeBitmapBlock;*/
+
+// rule 5 - adds the blockbitmapblock number to the blockbitmapblock set
+[], true => cast(BlockBitmap,d.b[d.g.BlockBitmapBlock]) in BlockBitmapBlock;
+
+// rule 6 - adds the rootdirectoryinode number to the set
+/*[forall itb in InodeTableBlock], true => itb.itable[d.s.RootDirectoryInode] in RootDirectoryInode;*/
+
+/*[forall itb in InodeTableBlock, for j=0 to d.s.NumberofInodes-1], !(itb.itable[j] in? UsedInode) => itb.itable[j] in FreeInode;*/
+
+[for j=0 to d.s.NumberofBlocks-1], !(d.b[j] in? UsedBlock) => d.b[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, for j=0 to ((d.s.blocksize/128)-1), for k=0 to 11], true => cast(DirectoryBlock,d.b[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;
+
+
+// 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]<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=0 to d.s.NumberofInodes-1, forall itb in InodeTableBlock, forall ibb in InodeBitmapBlock], true => <itb.itable[j], 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;
+
+// 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;
+
+// rule 16
+// populating the referencecount relation with the referencecount
+// values for every usedinode
+/*[forall j in UsedInode], true => <j,j.referencecount> in referencecount;*/
+
+// rule 17 - populate the filesize relation with the sizes inodes' files
+/*[forall j in UsedInode], true => <j,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=0 to d.s.NumberofBlocks-1, forall bbb in BlockBitmapBlock], true => <d.b[j],bbb.blockbitmap[j]> in blockstatus;
+
--- /dev/null
+// sEXT2 - Simple File System Example
+// Space Definition Language File
+
+set Block(Block) :
+ UsedBlock |
+ FreeBlock;
+
+set FreeBlock(Block);
+
+set Inode(Inode) :
+ UsedInode |
+ FreeInode;
+
+set FreeInode(Inode);
+
+set UsedInode(Inode) :
+ FileInode |
+ DirectoryInode ;
+
+set FileInode(Inode);
+
+set DirectoryInode(Inode) : RootDirectoryInode;
+
+set RootDirectoryInode(Inode);
+
+set UsedBlock(Block) :
+ SuperBlock |
+ GroupBlock |
+ FileDirectoryBlock |
+ InodeTableBlock |
+ InodeBitmapBlock |
+ BlockBitmapBlock;
+
+set FileDirectoryBlock(Block) :
+ DirectoryBlock |
+ FileBlock;
+
+set SuperBlock(Superblock);
+
+set GroupBlock(Groupblock);
+
+set FileBlock(Block);
+
+set DirectoryBlock(Block);
+
+set InodeTableBlock(InodeTable);
+
+set InodeBitmapBlock(InodeBitmap);
+
+set BlockBitmapBlock(BlockBitmap);
+
+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);
--- /dev/null
+// 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[0]: Superblock s;
+ label b[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[12];
+ int referencecount;
+}
+
+structure DirectoryBlock subtype of Block {
+ DirectoryEntry de[d.s.blocksize/128];
+}
+
+structure DirectoryEntry {
+ byte name[124];
+ int inodenumber;
+}
+
+
+
+
+
projects / repair.git / commitdiff