From: yeom Date: Sat, 2 Jul 2011 00:34:52 +0000 (+0000) Subject: bug fixes X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=6af1f2a5f54ecb7285fc30638792d966d1e2f9c7;p=IRC.git bug fixes --- diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java index d99f44f4..2a0d0c93 100644 --- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java +++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java @@ -187,30 +187,15 @@ public class DefinitelyWrittenCheck { NTuple rhsHeapPath = computePath(rhs); if (!rhs.getType().isImmutable()) { mapHeapPath.put(lhs, rhsHeapPath); - } - - if (fon.getOp().getOp() == Operation.ASSIGN) { - // read(rhs) - Hashtable gen = curr.get(rhsHeapPath); - - if (gen == null) { - gen = new Hashtable(); - curr.put(rhsHeapPath, gen); - } - Boolean currentStatus = gen.get(fn); - if (currentStatus == null) { - gen.put(fn, Boolean.FALSE); - } else { - if (!rhs.getType().isClass()) { - checkFlag(currentStatus.booleanValue(), fn); - } + } else { + if (fon.getOp().getOp() == Operation.ASSIGN) { + // read(rhs) + readValue(fn, rhsHeapPath, curr); } - + // write(lhs) + NTuple lhsHeapPath = computePath(lhs); + removeHeapPath(curr, lhsHeapPath); } - // write(lhs) - NTuple lhsHeapPath = computePath(lhs); - removeHeapPath(curr, lhsHeapPath); - // curr.put(lhsHeapPath, new Hashtable()); } break; @@ -229,26 +214,21 @@ public class DefinitelyWrittenCheck { case FKind.FlatElementNode: { FlatFieldNode ffn = (FlatFieldNode) fn; - lhs = ffn.getSrc(); + lhs = ffn.getDst(); + rhs = ffn.getSrc(); fld = ffn.getField(); // read field - NTuple srcHeapPath = mapHeapPath.get(lhs); + NTuple srcHeapPath = mapHeapPath.get(rhs); NTuple fldHeapPath = new NTuple(srcHeapPath.getList()); fldHeapPath.add(fld); - Hashtable gen = curr.get(fldHeapPath); - if (gen == null) { - gen = new Hashtable(); - curr.put(fldHeapPath, gen); + if (fld.getType().isImmutable()) { + readValue(fn, fldHeapPath, curr); } - Boolean currentStatus = gen.get(fn); - if (currentStatus == null) { - gen.put(fn, Boolean.FALSE); - } else { - checkFlag(currentStatus.booleanValue(), fn); - } + // propagate rhs's heap path to the lhs + mapHeapPath.put(lhs, fldHeapPath); } break; @@ -261,11 +241,10 @@ public class DefinitelyWrittenCheck { fld = fsfn.getField(); // write(field) - NTuple lhsHeapPath = mapHeapPath.get(lhs); + NTuple lhsHeapPath = computePath(lhs); NTuple fldHeapPath = new NTuple(lhsHeapPath.getList()); fldHeapPath.add(fld); removeHeapPath(curr, fldHeapPath); - // curr.put(fldHeapPath, new Hashtable()); } break; @@ -273,7 +252,6 @@ public class DefinitelyWrittenCheck { case FKind.FlatCall: { FlatCall fc = (FlatCall) fn; - bindHeapPathCallerArgWithCaleeParam(fc); // add in which hp is an element of @@ -301,13 +279,27 @@ public class DefinitelyWrittenCheck { for (Iterator iterator = calleeIntersectBoundOverWriteSet.iterator(); iterator.hasNext();) { NTuple write = (NTuple) iterator.next(); removeHeapPath(curr, write); - // curr.put(write, new Hashtable()); } } break; } + } + } + + private void readValue(FlatNode fn, NTuple hp, + Hashtable, Hashtable> curr) { + Hashtable gen = curr.get(hp); + if (gen == null) { + gen = new Hashtable(); + curr.put(hp, gen); + } + Boolean currentStatus = gen.get(fn); + if (currentStatus == null) { + gen.put(fn, Boolean.FALSE); + } else { + checkFlag(currentStatus.booleanValue(), fn); } } @@ -334,6 +326,10 @@ public class DefinitelyWrittenCheck { // transform all READ/OVERWRITE set from the any possible // callees to the // caller + + calleeUnionBoundReadSet.clear(); + calleeIntersectBoundOverWriteSet.clear(); + MethodDescriptor mdCallee = fc.getMethod(); FlatMethod fmCallee = state.getMethodFlat(mdCallee); Set setPossibleCallees = new HashSet(); @@ -360,6 +356,7 @@ public class DefinitelyWrittenCheck { FlatMethod calleeFlatMethod = state.getMethodFlat(callee); // binding caller's args and callee's params + Set> calleeReadSet = mapFlatMethodToRead.get(calleeFlatMethod); if (calleeReadSet == null) { calleeReadSet = new HashSet>(); @@ -396,8 +393,9 @@ public class DefinitelyWrittenCheck { private void checkFlag(boolean booleanValue, FlatNode fn) { if (booleanValue) { throw new Error( - "There is a variable who comes back to the same read statement at the out-most iteration at " - + methodContainingSSJavaLoop.getClassDesc().getSourceFileName() + "::" + "There is a variable who comes back to the same read statement without being overwritten at the out-most iteration at " + + methodContainingSSJavaLoop.getClassDesc().getSourceFileName() + + "::" + fn.getNumLine()); } } @@ -502,11 +500,13 @@ public class DefinitelyWrittenCheck { // intraprocedural analysis Set flatNodesToVisit = new HashSet(); + Set visited = new HashSet(); flatNodesToVisit.add(fm); while (!flatNodesToVisit.isEmpty()) { FlatNode fn = flatNodesToVisit.iterator().next(); flatNodesToVisit.remove(fn); + visited.add(fn); Set> curr = new HashSet>(); @@ -524,7 +524,9 @@ public class DefinitelyWrittenCheck { for (int i = 0; i < fn.numNext(); i++) { FlatNode nn = fn.getNext(i); - flatNodesToVisit.add(nn); + if (!visited.contains(nn)) { + flatNodesToVisit.add(nn); + } } } @@ -585,9 +587,11 @@ public class DefinitelyWrittenCheck { mapHeapPath.put(lhs, readingHeapPath); // read (x.f) - // if WT doesnot have hp(x.f), add hp(x.f) to READ - if (!writtenSet.contains(readingHeapPath)) { - readSet.add(readingHeapPath); + if (fld.getType().isImmutable()) { + // if WT doesnot have hp(x.f), add hp(x.f) to READ + if (!writtenSet.contains(readingHeapPath)) { + readSet.add(readingHeapPath); + } } // need to kill hp(x.f) from WT @@ -656,7 +660,6 @@ public class DefinitelyWrittenCheck { } private void merge(Set> curr, Set> in) { - if (curr.isEmpty()) { // WrittenSet has a special initial value which covers all possible // elements diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java index 970b1929..b14fecfc 100644 --- a/Robust/src/Analysis/SSJava/FlowDownCheck.java +++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java @@ -713,10 +713,10 @@ public class FlowDownCheck { VarDescriptor calleevd2 = (VarDescriptor) min.getMethod().getParameter(currentIdx); CompositeLocation calleeLoc2 = d2loc.get(calleevd2); - boolean callerResult = CompositeLattice.isGreaterThan(callerArg1, callerArg2); - boolean calleeResult = CompositeLattice.isGreaterThan(calleeLoc1, calleeLoc2); - - if (calleeResult && !callerResult) { + int callerResult = CompositeLattice.compare(callerArg1, callerArg2); + int calleeResult = CompositeLattice.compare(calleeLoc1, calleeLoc2); + if (calleeResult == ComparisonResult.GREATER + && callerResult != ComparisonResult.GREATER) { // If calleeLoc1 is higher than calleeLoc2 // then, caller should have same ordering relation in-bet // callerLoc1 & callerLoc2 @@ -1194,9 +1194,7 @@ public class FlowDownCheck { public static boolean isGreaterThan(CompositeLocation loc1, CompositeLocation loc2) { - // System.out.println("isGreaterThan= " + loc1 + " " + loc2); - - int baseCompareResult = compareBaseLocationSet(loc1, loc2); + int baseCompareResult = compareBaseLocationSet(loc1, loc2, true); if (baseCompareResult == ComparisonResult.EQUAL) { if (compareDelta(loc1, loc2) == ComparisonResult.GREATER) { return true; @@ -1214,7 +1212,7 @@ public class FlowDownCheck { public static int compare(CompositeLocation loc1, CompositeLocation loc2) { // System.out.println("compare=" + loc1 + " " + loc2); - int baseCompareResult = compareBaseLocationSet(loc1, loc2); + int baseCompareResult = compareBaseLocationSet(loc1, loc2, false); if (baseCompareResult == ComparisonResult.EQUAL) { return compareDelta(loc1, loc2); @@ -1245,7 +1243,8 @@ public class FlowDownCheck { } - private static int compareBaseLocationSet(CompositeLocation compLoc1, CompositeLocation compLoc2) { + private static int compareBaseLocationSet(CompositeLocation compLoc1, + CompositeLocation compLoc2, boolean awareSharedLoc) { // if compLoc1 is greater than compLoc2, return true // else return false; @@ -1297,7 +1296,7 @@ public class FlowDownCheck { // check if the current location is the spinning location // note that the spinning location only can be appeared in the last // part of the composite location - if (numOfTie == compLoc1.getSize() + if (awareSharedLoc && numOfTie == compLoc1.getSize() && lattice1.getSpinLocSet().contains(loc1.getLocIdentifier())) { return ComparisonResult.GREATER; } diff --git a/Robust/src/Analysis/SSJava/NTuple.java b/Robust/src/Analysis/SSJava/NTuple.java index d69708de..800c3652 100644 --- a/Robust/src/Analysis/SSJava/NTuple.java +++ b/Robust/src/Analysis/SSJava/NTuple.java @@ -77,12 +77,14 @@ public class NTuple { } for (int i = 0; i < prefix.size(); i++) { - if (prefix.get(i).equals(get(i))) { + if (!prefix.get(i).equals(get(i))) { return false; } } return true; } + + }