1) Checking in filesystem example

2) Checking in code to handle Booleans/other expressions
3) Added invariants to updatenodes...

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
index affa0354239bd36d432d88bc34465bbdd832f27d..5ae9aaac4beb8b97d73c7e82c051fc533828d4ac 100755 (executable)
--- 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;
                
                 (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 (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 24617a3e243d7962a80d165bb4e87b797ab188b9..830e07551e74c93ceb39d068260dbc1457811dd3 100755 (executable)
--- 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);
                    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()) {
                } 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);
                    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()) {
                } 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 bc669986eef83ecbc77021ec69373e0821551422..397a7a7ce16b176748ba49b79c0eadb06be3245f 100755 (executable)
--- 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;
 class UpdateNode {
     Vector updates;
     Vector bindings;

+    Vector invariants;

     Hashtable binding;
     Rule rule;
     Hashtable binding;
     Rule rule;

-    

 
     public UpdateNode(Rule r) {
        updates=new Vector();
        bindings=new Vector();
 
     public UpdateNode(Rule r) {
        updates=new Vector();
        bindings=new Vector();

+       invariants=new Vector();

        binding=new Hashtable();
        rule=r;
     }
        binding=new Hashtable();
        rule=r;
     }


@@ -22,14 +23,21 @@ class UpdateNode {
 
     public String toString() {
        String st="";
 
     public String toString() {
        String st="";

+       st+="Bindings:\n";

        for(int i=0;i<bindings.size();i++)
            st+=bindings.get(i).toString()+"\n";
        st+="---------------------\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";
        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;
     }
        return st;
     }

-
+  

     public void addBindings(Vector v) {
        for (int i=0;i<v.size();i++) {
            addBinding((Binding)v.get(i));
     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);
        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)
            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;
     }
 
            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);
     }
     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 (executable)
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 (executable)
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 (executable)
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 (executable)
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;
+}
+
+
+
+
+