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 3e44b831fd3fb6e4f788638cc90a2da0baf41633..6b6a7153c9a79ad12019b4ddcd1df321806febde 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();
+       boolean needcyclecheck=false;
+       HashSet cantremovetrans=new HashSet();
        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;
+                   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)||
-                       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);
                }
@@ -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;
     }
 
@@ -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;
@@ -377,6 +430,13 @@ public class GraphAnalysis {
                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");

diff --git a/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java b/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
index 99c4d893bd2707fb9b6c1adab363b2cdb4aa9294..ead3fce5811d91865a96b3b326b5154da08a4bd7 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;
-           if (remap.containsKey(nvde))
+           if (remap!=null&&remap.containsKey(nvde))
                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 42823cd12826248cc99618e184c8c856639cfc6a..ba75daeaa973125c4642b5eb5e1ef01c5b2b2cc6 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+=", "+stleft+", "+stright+", "+stnew;
+                   methodcall+=", int "+stleft+", int "+stright+", int "+stnew;
                    methodcall+=")";
                    crhead.outputline(methodcall+";");
                    craux.outputline(methodcall);
@@ -1392,14 +1392,14 @@ public class RepairGenerator {
                    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.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();
                    }

diff --git a/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints b/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
index 0b4dc230777f185e2b90c9a3a1fd3b5a437a3696..39d44626db78a758c41f02151d1b4a589ab21b0a 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'
-//[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'
-//[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'
-//[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'
-//[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
-//[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)
-//[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
-//[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
@@ -63,4 +55,4 @@
 
 // C13
 // verify that there is one rootdirectoryinode
-//[],sizeof(RootDirectoryInode)=1;
+[],sizeof(RootDirectoryInode)=1;