From: bdemsky Date: Tue, 11 May 2004 17:12:17 +0000 (+0000) Subject: 1) Further updates to specifications. X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=commitdiff_plain;h=1865e2c81c6c387dcc48114a33921e26fc0211b1 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 --- 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 99c4d89..ead3fce 100755 --- 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 42823cd..ba75dae 100755 --- 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 0b4dc23..39d4462 100755 --- 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;