1) Further updates to specifications.

2) Further updates to search algorith.

diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
index 3e44b83..6b6a715 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
@@ -19,6 +19,8 @@ public class GraphAnalysis {
     private boolean safetransclosure(GraphNode gn, Set removed, Set cantremove, Set couldremove) {
        Stack workset=new Stack();
        HashSet closureset=new HashSet();
     private boolean safetransclosure(GraphNode gn, Set removed, Set cantremove, Set couldremove) {
        Stack workset=new Stack();
        HashSet closureset=new HashSet();

+       boolean needcyclecheck=false;
+       HashSet cantremovetrans=new HashSet();

        workset.push(gn);
        while(!workset.empty()) {
            GraphNode gn2=(GraphNode)workset.pop();
        workset.push(gn);
        while(!workset.empty()) {
            GraphNode gn2=(GraphNode)workset.pop();


@@ -29,12 +31,24 @@ public class GraphAnalysis {
                    GraphNode gn3=((GraphNode.Edge)edgeit.next()).getTarget();
                    if (removed.contains(gn3))
                        continue;
                    GraphNode gn3=((GraphNode.Edge)edgeit.next()).getTarget();
                    if (removed.contains(gn3))
                        continue;

+                   if (((cantremove.contains(gn2)||!couldremove.contains(gn2))
+                        &&termination.conjunctions.contains(gn2))||
+                       cantremovetrans.contains(gn2))
+                       cantremovetrans.add(gn3);
+                   

                    if (termination.abstractrepair.contains(gn3)||
                        termination.conjunctions.contains(gn3)||
                    if (termination.abstractrepair.contains(gn3)||
                        termination.conjunctions.contains(gn3)||

-                       termination.updatenodes.contains(gn3))
-                       return false;
-                   if (!removed.contains(gn3)&&
-                       ((!couldremove.contains(gn3))||cantremove.contains(gn3)))
+                       termination.updatenodes.contains(gn3)) {
+                       /**  Check for cycles if the graphnode can't
+                        * be removed (we know we aren't introducing
+                        * new things to repair). */
+                       if ((!termination.abstractrepair.contains(gn3)&&
+                            cantremove.contains(gn3))||
+                           cantremovetrans.contains(gn3)) {
+                           needcyclecheck=true;
+                       } else return false;
+                   }
+                   if ((!couldremove.contains(gn3))||cantremove.contains(gn3))

                        goodoption=true;
                    workset.push(gn3);
                }
                        goodoption=true;
                    workset.push(gn3);
                }


@@ -44,6 +58,16 @@ public class GraphAnalysis {
                }                   
            }
        }
                }                   
            }
        }

+       if (needcyclecheck) {
+           Set cycles=GraphNode.findcycles(closureset);
+           for(Iterator it=cycles.iterator();it.hasNext();) {
+               GraphNode gn2=(GraphNode)it.next();
+               if (termination.abstractrepair.contains(gn2)||
+                   termination.conjunctions.contains(gn2)||
+                   termination.updatenodes.contains(gn2))
+                   return false;
+           }
+       }

        return true;
     }
 
        return true;
     }
 


@@ -86,6 +110,35 @@ public class GraphAnalysis {
                }
            }
 
                }
            }
 

+           /* Check for conjunction nodes which are fine */
+
+           for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
+               GraphNode gn=(GraphNode) it.next();
+               if (mustremove.contains(gn)||cantremove.contains(gn))
+                   continue;
+
+               boolean allgood=true;
+               for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
+                   GraphNode gn2=((GraphNode.Edge)edgeit.next()).getTarget();
+                   TermNode tn2=(TermNode)gn2.getOwner();
+                   assert tn2.getType()==TermNode.ABSTRACT;
+                   boolean foundupdate=false;
+                   for(Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
+                       GraphNode gn3=((GraphNode.Edge)edgeit2.next()).getTarget();                 
+                       if (!couldremove.contains(gn3)&&!mustremove.contains(gn3)) {
+                           TermNode tn3=(TermNode)gn3.getOwner();
+                           if (tn3.getType()==TermNode.UPDATE)
+                               foundupdate=true;
+                       }
+                   }
+                   if (!foundupdate)
+                       allgood=false;
+               }
+               if (allgood)
+                   couldremove.remove(gn);
+           }
+
+

            /* Look for constraints which can only be satisfied one way */
            
            Vector constraints=termination.state.vConstraints;
            /* Look for constraints which can only be satisfied one way */
            
            Vector constraints=termination.state.vConstraints;


@@ -377,6 +430,13 @@ public class GraphAnalysis {
                e.printStackTrace();
                System.exit(-1);
            }
                e.printStackTrace();
                System.exit(-1);
            }

+
+           try {
+               GraphNode.DOTVisitor.visit(new FileOutputStream("graphcycle.dot"),GraphNode.findcycles(nodes),couldremove);
+           } catch (Exception e) {
+               e.printStackTrace();
+               System.exit(-1);
+           }

            
            System.out.println("Searching set of "+couldremove.size()+" nodes.");
            System.out.println("Eliminated must "+mustremove.size()+" nodes");
            
            System.out.println("Searching set of "+couldremove.size()+" nodes.");
            System.out.println("Eliminated must "+mustremove.size()+" nodes");

diff --git a/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java b/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
index 99c4d89..ead3fce 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
@@ -69,7 +69,7 @@ public class ImageSetExpr extends SetExpr {
            return ise.equals(remap,ise2.ise);
        } else {
            VarDescriptor nvde=vd;
            return ise.equals(remap,ise2.ise);
        } else {
            VarDescriptor nvde=vd;

-           if (remap.containsKey(nvde))
+           if (remap!=null&&remap.containsKey(nvde))

                nvde=(VarDescriptor)remap.get(nvde);
            if (nvde!=ise2.vd)
                return false;
                nvde=(VarDescriptor)remap.get(nvde);
            if (nvde!=ise2.vd)
                return false;

diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
index 42823cd..ba75dae 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
+++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
@@ -206,7 +206,7 @@ public class RepairGenerator {
                            methodcall+=", int "+fq.getVar().getSafeSymbol();
                        }
                    }
                            methodcall+=", int "+fq.getVar().getSafeSymbol();
                        }
                    }

-                   methodcall+=", "+stleft+", "+stright+", "+stnew;
+                   methodcall+=", int "+stleft+", int "+stright+", int "+stnew;

                    methodcall+=")";
                    crhead.outputline(methodcall+";");
                    craux.outputline(methodcall);
                    methodcall+=")";
                    crhead.outputline(methodcall+";");
                    craux.outputline(methodcall);


@@ -1392,14 +1392,14 @@ public class RepairGenerator {
                    cr.outputline("if ("+mdfyptr.getSafeSymbol()+")");
                    {
                        cr.startblock();
                    cr.outputline("if ("+mdfyptr.getSafeSymbol()+")");
                    {
                        cr.startblock();

-                       cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+",int,int,int)="+"(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+",int,int,int)) "+tmpptr.getSafeSymbol());
-                       cr.outputline(methodcall+leftvar+", "+rightvar+", "+mdfyptr.getSafeSymbol() +");");
+                       cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+",int,int,int)="+"(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+",int,int,int)) "+tmpptr.getSafeSymbol()+";");
+                       cr.outputline(methodcall+","+leftvar+", "+rightvar+", "+mdfyptr.getSafeSymbol() +");");

                        cr.endblock();
                    }
                    cr.outputline("else ");
                    {
                        cr.startblock();
                        cr.endblock();
                    }
                    cr.outputline("else ");
                    {
                        cr.startblock();

-                       cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")="+"(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+tmpptr.getSafeSymbol());
+                       cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")="+"(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+tmpptr.getSafeSymbol()+";");

                        cr.outputline(methodcall+");");
                        cr.endblock();
                    }
                        cr.outputline(methodcall+");");
                        cr.endblock();
                    }

diff --git a/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints b/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
index 0b4dc23..39d4462 100755 (executable)
--- a/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
+++ b/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
@@ -8,46 +8,38 @@
 // C1
 // for all used inodes, verify that the inodestatus (built from the
 // inodebitmap is marked 'used'
 // C1
 // for all used inodes, verify that the inodestatus (built from the
 // inodebitmap is marked 'used'

-//[forall u in UsedInode], u.inodestatus=true;
+[forall u in UsedInode], u.inodestatus=true;

 
 // C2
 // for all free inodes, verify that the inodestatus (built from the 
 // inodebitmap is marked 'free'
 
 // C2
 // for all free inodes, verify that the inodestatus (built from the 
 // inodebitmap is marked 'free'

-//[forall f in FreeInode], f.inodestatus=false;
+[forall f in FreeInode], f.inodestatus=false;

 
 // C3
 // for all used blocks, verify that the blockstatus (built from the
 // blockbitmap is marked 'used'
 
 // C3
 // for all used blocks, verify that the blockstatus (built from the
 // blockbitmap is marked 'used'

-//[forall u in UsedBlock], u.blockstatus=true;
+[forall u in UsedBlock], u.blockstatus=true;

 
 // C4
 // for all free blocks, verify that the blockstatus (built from the
 // block bitmap is marked 'free'
 
 // C4
 // for all free blocks, verify that the blockstatus (built from the
 // block bitmap is marked 'free'

-//[forall f in FreeBlock], f.blockstatus=false;
+[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
 
 // 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)
 
 // 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)*8192;
+[forall i in UsedInode], i.filesize <= sizeof(i.contents)*8192;

 
 // C7
 // ??? for all files and directory blocks check that
 // only one inode references this block
 
 // C7
 // ??? for all files and directory blocks check that
 // only one inode references this block

-//[forall b in FileDirectoryBlock],sizeof(b.~contents)=1;
-
-// C8
-// verify that there is one superblock
-//[],sizeof(SuperBlock)=1;
-
-// C9
-// verify that there is one groupblock
-//[],sizeof(GroupBlock)=1;
+[forall b in FileDirectoryBlock],sizeof(b.~contents)=1;

 
 // C10
 // verify that there is one inodetableblock
 
 // C10
 // verify that there is one inodetableblock


@@ -63,4 +55,4 @@
 
 // C13
 // verify that there is one rootdirectoryinode
 
 // C13
 // verify that there is one rootdirectoryinode

-//[],sizeof(RootDirectoryInode)=1;
+[],sizeof(RootDirectoryInode)=1;