* files.
*
* @author le01, 6.035 Staff (<tt>6.035-staff@mit.edu</tt>)
- * @version <tt>$Id: CLI.java,v 1.3 2004/04/21 21:15:48 bdemsky Exp $</tt>
+ * @version <tt>$Id: CLI.java,v 1.4 2004/05/10 21:54:40 bdemsky Exp $</tt>
*/
public class CLI {
/**
debug = true;
} else if (args[i].equals("-checkonly")) {
Compiler.REPAIR=false;
+ } else if (args[i].equals("-aggressivesearch")) {
+ Compiler.AGGRESSIVESEARCH=true;
} else if (args[i].equals("-verbose") || args[i].equals("-v")) {
context = 0;
verbose++;
public class Compiler {
/* Set this flag to false to turn repairs off */
public static boolean REPAIR=true;
-
+ public static boolean AGGRESSIVESEARCH=false;
+
public static void main(String[] args) {
State state = null;
boolean success = true;
Set s=providesfunction(f);
if (s.size()==0) {
- System.out.println("Error: No constraint ensures that [forall v in "+f.getSet()+"], size(v."+(f.isInverse()?"~":"")+f.getRelation()+")=1");
- System.exit(-1);
+ System.out.println("Warning: No constraint ensures that [forall v in "+f.getSet()+"], size(v."+(f.isInverse()?"~":"")+f.getRelation()+")=1");
+ continue;
}
Constraint c=(Constraint)s.iterator().next(); //Take the first one
requiresConstraint(conjnode,c);
Expr e=f.isInverse()?ri.getRightExpr():ri.getLeftExpr();
SetDescriptor sd=e.getSet();
if (sd==null)
- sd=f.isInverse()?ri.getRelation().getRange():ri.getRelation().getDomain();
+ return false;
if (!(sd.isSubset(f.getSet())||f.getSet().isSubset(sd)))
continue; /* This rule doesn't effect the function */
if (foundrule) /* two different rules are a problem */
private RelationDescriptor rd;
private SetDescriptor sd;
private boolean inverse;
+ private Expr expr;
- public Function(RelationDescriptor r, SetDescriptor sd, boolean inverse) {
+ public Function(RelationDescriptor r, SetDescriptor sd, boolean inverse,Expr e) {
this.inverse=inverse;
this.sd=sd;
this.rd=r;
+ this.expr=e;
+ }
+
+ public Expr getExpr() {
+ return expr;
}
public SetDescriptor getSet() {
public boolean isSafe() {
return true;
}
+
+ public Expr getLower() {
+ return null;
+ }
+
+ public Expr getUpper() {
+ return null;
+ }
}
import java.util.*;
import java.io.*;
import MCC.State;
+import MCC.Compiler;
public class GraphAnalysis {
Termination termination;
termination=t;
}
+ private boolean safetransclosure(GraphNode gn, Set removed, Set cantremove, Set couldremove) {
+ Stack workset=new Stack();
+ HashSet closureset=new HashSet();
+ workset.push(gn);
+ while(!workset.empty()) {
+ GraphNode gn2=(GraphNode)workset.pop();
+ if (!closureset.contains(gn2)) {
+ closureset.add(gn2);
+ boolean goodoption=false;
+ for(Iterator edgeit=gn2.edges();edgeit.hasNext();) {
+ GraphNode gn3=((GraphNode.Edge)edgeit.next()).getTarget();
+ if (removed.contains(gn3))
+ continue;
+ 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)))
+ goodoption=true;
+ workset.push(gn3);
+ }
+ if (!goodoption) {
+ if (termination.scopenodes.contains(gn2))
+ return false;
+ }
+ }
+ }
+ return true;
+ }
+
public Set doAnalysis() {
HashSet cantremove=new HashSet();
HashSet mustremove=new HashSet();
couldremove.addAll(termination.consequencenodes);
couldremove.retainAll(nodes);
+
+ /* Check for consequence nodes which are fine */
+
+ for(Iterator it=termination.consequencenodes.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode) it.next();
+ if (safetransclosure(gn, mustremove,cantremove, couldremove)) {
+ couldremove.remove(gn);
+ }
+ }
+
+ /* Check for update nodes which are fine */
+
+ for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode) it.next();
+ if (safetransclosure(gn, mustremove,cantremove, cantremove)) {
+ couldremove.remove(gn);
+ }
+ }
+
/* Look for constraints which can only be satisfied one way */
Vector constraints=termination.state.vConstraints;
}
}
+ if (Compiler.AGGRESSIVESEARCH) {
+ /* Aggressively remove compensation nodes */
+ for(Iterator scopeit=termination.scopenodes.iterator();scopeit.hasNext();) {
+ GraphNode gn=(GraphNode)scopeit.next();
+ HashSet tmpset=new HashSet();
+ boolean doremove=false;
+ for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
+ GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
+ GraphNode gn2=e.getTarget();
+ if (termination.consequencenodes.contains(gn2)) {
+ if (((!couldremove.contains(gn2))||cantremove.contains(gn2))&&
+ !mustremove.contains(gn2)) {
+ doremove=true;
+ } else
+ break;
+ } else tmpset.add(gn2);
+ }
+ if (doremove)
+ mustremove.addAll(tmpset);
+ }
+ }
+
Set cycles2=GraphNode.findcycles(cantremove);
for(Iterator it=cycles2.iterator();it.hasNext();) {
GraphNode gn=(GraphNode)it.next();
continue; //recalculate
try {
- GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes);
+ GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes,couldremove);
} catch (Exception e) {
e.printStackTrace();
System.exit(-1);
}
if (incremented==false) /* Increase length */ {
combination.add(new Integer(0));
- System.out.println("Expanding to :"+combination.size());
+ System.out.println("Expanding to: "+combination.size());
}
}
}
Collection nodes;
+ Collection special;
public static void visit(java.io.OutputStream output, Collection nodes) {
+ visit(output,nodes,null);
+ }
+
+ public static void visit(java.io.OutputStream output, Collection nodes, Collection special) {
DOTVisitor visitor = new DOTVisitor(output);
+ visitor.special=special;
visitor.nodes = nodes;
visitor.make();
-
}
private void make() {
String option="";
if (cycleset.contains(gn))
option=",style=bold";
+ if (special!=null&&special.contains(gn))
+ option+=",shape=box";
output.println("\t" + gn.getLabel() + " [label=\"" + label + "\"" + gn.dotnodeparams + option+"];");
while (edges.hasNext()) {
VarDescriptor vd;
RelationDescriptor rd;
boolean inverse;
+ ImageSetExpr ise;
+ boolean isimageset=false;
+
+ public ImageSetExpr(boolean inverse, VarDescriptor vd, RelationDescriptor rd) {
+ this.vd = vd;
+ this.rd = rd;
+ this.inverse = inverse;
+ }
public ImageSetExpr(VarDescriptor vd, RelationDescriptor rd) {
this.vd = vd;
this.inverse = false;
}
+ public ImageSetExpr(boolean inverse, ImageSetExpr ise, RelationDescriptor rd) {
+ this.ise = ise;
+ this.isimageset=true;
+ this.rd = rd;
+ this.inverse = inverse;
+ }
+
+ public ImageSetExpr(ImageSetExpr ise, RelationDescriptor rd) {
+ this.ise = ise;
+ this.isimageset=true;
+ this.rd = rd;
+ this.inverse = false;
+ }
+
public Set freeVars() {
HashSet hs=new HashSet();
hs.add(vd);
}
public String name() {
- String name=vd.toString()+".";
+ String name="";
+ if (isimageset)
+ name+=ise.name();
+ else
+ name+=vd.toString()+".";
if (inverse)
name+="~";
name+=rd.toString();
return name;
}
- public ImageSetExpr(boolean inverse, VarDescriptor vd, RelationDescriptor rd) {
- this.vd = vd;
- this.rd = rd;
- this.inverse = inverse;
- }
-
public boolean equals(Map remap, Expr e) {
if (e==null||!(e instanceof ImageSetExpr))
return false;
- ImageSetExpr ise=(ImageSetExpr)e;
- if (ise.inverse!=inverse)
+ ImageSetExpr ise2=(ImageSetExpr)e;
+ if (ise2.isimageset!=isimageset)
return false;
- if (ise.rd!=rd)
+ if (ise2.inverse!=inverse)
return false;
- VarDescriptor nvde=vd;
- if (remap.containsKey(nvde))
- nvde=(VarDescriptor)remap.get(nvde);
- if (nvde!=ise.vd)
+ if (ise2.rd!=rd)
return false;
- return true;
+
+ if (isimageset) {
+ return ise.equals(remap,ise2.ise);
+ } else {
+ VarDescriptor nvde=vd;
+ if (remap.containsKey(nvde))
+ nvde=(VarDescriptor)remap.get(nvde);
+ if (nvde!=ise2.vd)
+ return false;
+ return true;
+ }
}
public boolean inverted() {
return vd;
}
+ public ImageSetExpr getImageSetExpr() {
+ return ise;
+ }
+
public RelationDescriptor getRelation() {
return rd;
}
}
public boolean usesDescriptor(Descriptor d) {
+ if (isimageset)
+ return d==rd||ise.usesDescriptor(d);
return (d==rd)||(d==vd);
}
public void generate_inclusion(CodeWriter writer, VarDescriptor dest, VarDescriptor element) {
String hash = inverse ? "_hashinv->contains(" : "_hash->contains(" ;
writer.outputline("int " + dest.getSafeSymbol() + " = " + rd.getSafeSymbol() + hash + vd.getSafeSymbol() + ", " + element.getSafeSymbol() + ");");
- }
+ }
public void generate_size(CodeWriter writer, VarDescriptor dest) {
assert dest != null;
Expr right;
Opcode opcode;
+ public Expr getUpper() {
+ Expr lupper=left.getUpper();
+ if (lupper==null)
+ return null;
+ if (right!=null) {
+ Expr rupper=right.getUpper();
+ if (rupper==null)
+ return null;
+ OpExpr oe=new OpExpr(this.opcode,lupper,rupper);
+ oe.td = ReservedTypeDescriptor.INT;
+ return oe;
+ } else return lupper;
+ }
+
+ public Expr getLower() {
+ Expr llower=left.getLower();
+ if (llower==null)
+ return null;
+ if (right!=null) {
+ Expr rlower=right.getLower();
+ if (rlower==null)
+ return null;
+ OpExpr oe=new OpExpr(this.opcode,llower,rlower);
+ oe.td = ReservedTypeDescriptor.INT;
+ return oe;
+ } else return llower;
+ }
+
public boolean isSafe() {
if (right==null)
return left.isSafe();
Set exprfunctions=expr.getfunctions();
if (exprfunctions!=null)
functions.addAll(exprfunctions);
- functions.add(new ConstraintDependence.Function(relation,expr.getSet(),inverse));
+ functions.add(new ConstraintDependence.Function(relation,expr.getSet(),inverse,this));
return functions;
}
/* grab var */
VarDescriptor vd = reserveName(pn.getChild("var"));
-
+
if (vd == null) {
return null;
}
Expr lower = parse_expr(pn.getChild("lower").getChild("expr"));
Expr upper = parse_expr(pn.getChild("upper").getChild("expr"));
+
if ((lower == null) || (upper == null)) {
return null;
}
-
+ vd.setBounds(lower,upper);
fq.setBounds(lower, upper);
return fq;
SetDescriptor sd=null;
+ Expr lower=null;
+ Expr upper=null;
+
+ public void setBounds(Expr l,Expr u) {
+ lower=l;
+ upper=u;
+ }
+
+ public Expr getLower() {
+ return lower;
+ }
+
+ public Expr getUpper() {
+ return upper;
+ }
+
public SetDescriptor getSet() {
return sd;
}
return hs;
}
+ public Expr getLower() {
+ return vd.getLower();
+ }
+
+ public Expr getUpper() {
+ return vd.getUpper();
+ }
+
public SetDescriptor getSet() {
return vd.getSet();
}
// 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
// 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);
+//[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)=literal(1);
+//[forall b in FileDirectoryBlock],sizeof(b.~contents)=1;
// C8
// verify that there is one superblock
// C10
// verify that there is one inodetableblock
-/*[],sizeof(InodeTableBlock)=1;*/
+[],sizeof(InodeTableBlock)=1;
// C11
// verify that there is one inodebitmapblock
-/*[],sizeof(InodeBitmapBlock)=1;*/
+[],sizeof(InodeBitmapBlock)=1;
// C12
// verify that there is one blockbitmapblock
// C13
// verify that there is one rootdirectoryinode
-/*[],sizeof(RootDirectoryInode)=1;*/
+//[],sizeof(RootDirectoryInode)=1;
// 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;*/
+[], true => d.s in SuperBlock;
// rule 2 - adds the block number of the groupblock to the groupblock set
-/*[], true => d.g in GroupBlock;*/
+[], true => d.g in GroupBlock;
-/*[], true => cast(InodeTable,d.b[d.g.InodeTableBlock]) in InodeTableBlock;*/
+[], 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;*/
+[], 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], 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;*/
+//r7
+[forall itb in InodeTableBlock, for j=0 to d.s.NumberofInodes-1], !(itb.itable[j] in? UsedInode) => itb.itable[j] in FreeInode;
+//r8
[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;*/
+[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;
-
+[forall i in UsedInode, for j=0 to 11], !(i.Blockptr[j]=0) => <i,d.b[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
// 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
+
+[forall i in UsedInode, for j=0 to 11], !(i.Blockptr[j]=0) => d.b[i.Blockptr[j]] in FileBlock;
// 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;*/
+[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;
+[forall de in DirectoryEntry,forall itb in InodeTableBlock], !(de.inodenumber = 0) => itb.itable[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;
+[forall de in DirectoryEntry,forall itb in InodeTableBlock], !(de.inodenumber = 0 ) => <de, itb.itable[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;*/
+[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;*/
+[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
projects / repair.git / commitdiff