public boolean interfereswithpredicate(AbstractRepair ar, DNFPredicate dp) {
if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
- ((ar.getDescriptor() instanceof SetDescriptor)||
- !dp.getPredicate().usesDescriptor((RelationDescriptor)ar.getDescriptor())))
+ // ((ar.getDescriptor() instanceof SetDescriptor)||
+ // If the second predicate uses the size of the set, modifying the set size could falsify it...
+ !dp.getPredicate().usesDescriptor(ar.getDescriptor()))
+ //)
return false;
/* This if handles all the c comparisons in the paper */
int size2=isInt2?((ExprPredicate)dp.getPredicate()).rightSize():0;
Expr expr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
+
+ /* If the left sides of the comparisons are both from
+ different sets, the update is orthogonal to the expr dp */
{
Expr lexpr1=((RelationExpr)((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).getLeftExpr()).getExpr();
Expr lexpr2=((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).getLeftExpr()).getExpr();
((op2==Opcode.LT)||
(op2==Opcode.LE)))
return false;
+ // FIXME
if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
expr1.equals(null,expr2)) {
+ // Need to check free variables...
return false;
}
if (isInt1&&isInt2) {
private boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
if ((des!=dp.getPredicate().getDescriptor()) &&
- ((des instanceof SetDescriptor)||
- !dp.getPredicate().usesDescriptor((RelationDescriptor)des)))
+ //((des instanceof SetDescriptor)||
+ !dp.getPredicate().usesDescriptor(des))//)
return false;
/* This if handles all the c comparisons in the paper */
state.rulenodes = rulenodes;
state.constraintnodes = constraintnodes;
}
-
- static class IntegerLattice {
-
- boolean top;
- boolean isNum;
- int num;
-
- public static final IntegerLattice TOP = new IntegerLattice(true);
- public static final IntegerLattice BOT = new IntegerLattice(false);
-
- private IntegerLattice(boolean top) {
- this.top = top;
- isNum = false;
- }
-
- public IntegerLattice(int num) {
- isNum = true;
- this.num = num;
- }
-
- }
-
- public IntegerLattice setSize(SetDescriptor sd) {
- String setname = sd.getSymbol();
-
- if (setname.equals("Block")) {
- return IntegerLattice.TOP;
- } else if (setname.equals("UsedBlock")) {
- return IntegerLattice.TOP;
- } else if (setname.equals("FreeBlock")) {
- return IntegerLattice.TOP;
- } else if (setname.equals("Inode")) {
- return IntegerLattice.TOP;
- } else if (setname.equals("UsedInode")) {
- return IntegerLattice.TOP;
- } else if (setname.equals("FileInode")) {
- return IntegerLattice.TOP;
- } else if (setname.equals("DirectoryInode")) {
- return new IntegerLattice(1);
- } else if (setname.equals("RootDirectoryInode")) {
- return new IntegerLattice(1);
- } else if (setname.equals("SuperBlock")) {
- return new IntegerLattice(1);
- } else if (setname.equals("GroupBlock")) {
- return new IntegerLattice(1);
- } else if (setname.equals("FileDirectoryBlock")) {
- return IntegerLattice.TOP;
- } else if (setname.equals("InodeTableBlock")) {
- return new IntegerLattice(1);
- } else if (setname.equals("InodeBitmapBlock")) {
- return new IntegerLattice(1);
- } else if (setname.equals("BlockBitmapBlock")) {
- return new IntegerLattice(1);
- } else if (setname.equals("DirectoryBlock")) {
- return new IntegerLattice(0);
- } else if (setname.equals("FileBlock")) {
- return IntegerLattice.TOP;
- } else if (setname.equals("DirectoryEntry")) {
- return IntegerLattice.TOP;
- } else {
- throw new IRException();
- }
-
- }
-
}
return expr.inverted();
}
- public boolean usesDescriptor(RelationDescriptor rd) {
+ public boolean usesDescriptor(Descriptor rd) {
return expr.usesDescriptor(rd);
}
abstract public int[] getRepairs(boolean negated, Termination t);
abstract public Descriptor getDescriptor();
abstract public boolean inverted();
- public boolean usesDescriptor(RelationDescriptor rd) {
+ public boolean usesDescriptor(Descriptor rd) {
return false;}
}
IR/ForQuantifier.class IR/GraphNode.class IR/DependencyBuilder.class \
IR/RelationInclusion.class IR/SetInclusion.class IR/TupleOfExpr.class \
IR/ElementOfExpr.class IR/Rule.class IR/Inclusion.class \
-IR/NaiveGenerator.class IR/CodeWriter.class IR/SymbolTableStack.class \
-IR/StandardCodeWriter.class IR/WorklistGenerator.class \
-IR/WorkList.class IR/Optimizer.class IR/MetaInclusion.class \
-IR/SizeofFunction.class IR/RelationFunctionExpr.class \
+IR/CodeWriter.class IR/SymbolTableStack.class \
+IR/StandardCodeWriter.class \
+IR/WorkList.class \
IR/RepairGenerator.class IR/AbstractInterferes.class \
IR/PrettyPrinter.class IR/AbstractRepair.class IR/Quantifiers.class \
IR/Binding.class IR/ConcreteInterferes.class IR/Conjunction.class \