From 5d11fc4a359b9fcb882e2f9c7bbde8ed632668da Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Thu, 6 May 2004 20:41:15 +0000
Subject: [PATCH] 1) Checking in filesystem example 2) Checking in code to
 handle Booleans/other expressions 3) Added invariants to updatenodes...

---
 .../MCC/IR/AbstractInterferes.java            |  6 ++
 Repair/RepairCompiler/MCC/IR/Termination.java | 15 +++-
 Repair/RepairCompiler/MCC/IR/UpdateNode.java  | 32 +++++++-
 .../MCC/specs/filesystem/test3.constraints    | 66 +++++++++++++++
 .../MCC/specs/filesystem/test3.model          | 82 +++++++++++++++++++
 .../MCC/specs/filesystem/test3.space          | 66 +++++++++++++++
 .../MCC/specs/filesystem/test3.struct         | 67 +++++++++++++++
 7 files changed, 328 insertions(+), 6 deletions(-)
 create mode 100755 Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
 create mode 100755 Repair/RepairCompiler/MCC/specs/filesystem/test3.model
 create mode 100755 Repair/RepairCompiler/MCC/specs/filesystem/test3.space
 create mode 100755 Repair/RepairCompiler/MCC/specs/filesystem/test3.struct

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
index affa035..5ae9aaa 100755
--- a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
@@ -159,6 +159,12 @@ class AbstractInterferes {
 		 (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))&&
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 24617a3..830e075 100755
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -683,8 +683,11 @@ public class Termination {
 		    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()) {
@@ -697,8 +700,12 @@ public class Termination {
 		    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()) {
diff --git a/Repair/RepairCompiler/MCC/IR/UpdateNode.java b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
index bc66998..397a7a7 100755
--- a/Repair/RepairCompiler/MCC/IR/UpdateNode.java
+++ b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
@@ -5,13 +5,14 @@ import MCC.State;
 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;
     }
@@ -22,14 +23,21 @@ class UpdateNode {
 
     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));
@@ -98,6 +106,14 @@ class UpdateNode {
 	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)
@@ -192,6 +208,18 @@ class UpdateNode {
 	    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);
     }
diff --git a/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints b/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
new file mode 100755
index 0000000..42b53d9
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/filesystem/test3.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=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;*/
diff --git a/Repair/RepairCompiler/MCC/specs/filesystem/test3.model b/Repair/RepairCompiler/MCC/specs/filesystem/test3.model
new file mode 100755
index 0000000..3a86486
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/filesystem/test3.model
@@ -0,0 +1,82 @@
+// 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;
+
diff --git a/Repair/RepairCompiler/MCC/specs/filesystem/test3.space b/Repair/RepairCompiler/MCC/specs/filesystem/test3.space
new file mode 100755
index 0000000..41f7504
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/filesystem/test3.space
@@ -0,0 +1,66 @@
+// 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);
diff --git a/Repair/RepairCompiler/MCC/specs/filesystem/test3.struct b/Repair/RepairCompiler/MCC/specs/filesystem/test3.struct
new file mode 100755
index 0000000..411b65d
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/filesystem/test3.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[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;
+}
+
+
+
+
+
-- 
2.34.1