X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;ds=sidebyside;f=Robust%2Fsrc%2FAnalysis%2FSSJava%2FDefinitelyWrittenCheck.java;fp=Robust%2Fsrc%2FAnalysis%2FSSJava%2FDefinitelyWrittenCheck.java;h=237cacd41ab7ad90665acca1826f66f500e7a94f;hb=4d83008119b742748914ee8e2aeba801cbdb3bd9;hp=63cbf7e38c71bfc338063c0e285980de4d55077a;hpb=7ce913a34454700dd6546fa2f86b6024a7b404e9;p=IRC.git diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java index 63cbf7e3..237cacd4 100644 --- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java +++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java @@ -13,7 +13,6 @@ import java.util.Stack; import Analysis.CallGraph.CallGraph; import Analysis.Loops.LoopFinder; -import IR.ClassDescriptor; import IR.Descriptor; import IR.FieldDescriptor; import IR.MethodDescriptor; @@ -58,7 +57,7 @@ public class DefinitelyWrittenCheck { private Hashtable> mapHeapPath; // maps a temp descriptor to its composite location - private Hashtable> mapDescriptorToLocationStrPath; + private Hashtable> mapDescriptorToLocationPath; // maps a flat method to the READ that is the set of heap path that is // expected to be written before method invocation @@ -71,11 +70,11 @@ public class DefinitelyWrittenCheck { // maps a flat method to the DELETE SET that is a set of heap path to shared // locations that are // written to but not overwritten by the higher value - private Hashtable>> mapFlatMethodToDeleteSet; + private Hashtable mapFlatMethodToDeleteSet; // maps a flat method to the S SET that is a set of heap path to shared // locations that are overwritten by the higher value - private Hashtable mapFlatMethodToSharedLocMappingSet; + private Hashtable mapFlatMethodToSharedLocMap; // maps a flat method to the may-wirte set that is the set of heap path that // might be written to @@ -133,7 +132,8 @@ public class DefinitelyWrittenCheck { private Hashtable> mapMethodToSharedWriteMapping; - private Hashtable mapFlatNodeToSharedLocMapping; + private Hashtable mapFlatNodeToSharedLocMapping; + private Hashtable mapFlatNodeToDeleteSet; private Hashtable> mapSharedLocationToCoverSet; @@ -147,7 +147,7 @@ public class DefinitelyWrittenCheck { private Set> calleeIntersectBoundMustWriteSet; private Set> calleeUnionBoundMayWriteSet; private Set> calleeUnionBoundDeleteSet; - private SharedLocMappingSet calleeIntersectBoundSharedSet; + private Hashtable, Set> calleeIntersectBoundSharedSet; private Hashtable mapDescToLocation; @@ -162,7 +162,7 @@ public class DefinitelyWrittenCheck { this.mapFlatNodeToMustWriteSet = new Hashtable>>(); this.mapDescriptorToSetDependents = new Hashtable>(); this.mapHeapPath = new Hashtable>(); - this.mapDescriptorToLocationStrPath = new Hashtable>(); + this.mapDescriptorToLocationPath = new Hashtable>(); this.mapFlatMethodToReadSet = new Hashtable>>(); this.mapFlatMethodToMustWriteSet = new Hashtable>>(); this.mapFlatMethodToMayWriteSet = new Hashtable>>(); @@ -188,14 +188,15 @@ public class DefinitelyWrittenCheck { this.mapFlatNodeToBoundMustWriteSet = new Hashtable>>(); this.mapFlatNodeToBoundMayWriteSet = new Hashtable>>(); this.mapSharedLocationToCoverSet = new Hashtable>(); - this.mapFlatNodeToSharedLocMapping = new Hashtable(); - this.mapFlatMethodToDeleteSet = new Hashtable>>(); + this.mapFlatNodeToSharedLocMapping = new Hashtable(); + this.mapFlatMethodToDeleteSet = new Hashtable(); this.calleeUnionBoundDeleteSet = new HashSet>(); - this.calleeIntersectBoundSharedSet = new SharedLocMappingSet(); - this.mapFlatMethodToSharedLocMappingSet = new Hashtable(); + this.calleeIntersectBoundSharedSet = new Hashtable, Set>(); + this.mapFlatMethodToSharedLocMap = new Hashtable(); this.mapLocationPathToMayWrittenSet = new MultiSourceMap(); this.mapMethodToSharedWriteMapping = new Hashtable>(); + this.mapFlatNodeToDeleteSet = new Hashtable(); } public void definitelyWrittenCheck() { @@ -207,8 +208,7 @@ public class DefinitelyWrittenCheck { System.out.println(mapLocationPathToMayWrittenSet); methodReadWriteSetAnalysis(); - - // sharedLocAnalysis(); + sharedLocAnalysis(); // eventLoopAnalysis(); @@ -249,14 +249,15 @@ public class DefinitelyWrittenCheck { MethodDescriptor md = methodDescriptorsToVisitStack.pop(); FlatMethod fm = state.getMethodFlat(md); - Set> deleteSet = new HashSet>(); - - sharedLoc_analyzeMethod(fm, deleteSet); - System.out.println("deleteSet result=" + deleteSet); + SharedLocMap sharedLocMap = new SharedLocMap(); + SharedLocMap deleteSet = new SharedLocMap(); - Set> prevDeleteSet = mapFlatMethodToDeleteSet.get(fm); + sharedLoc_analyzeMethod(fm, sharedLocMap, deleteSet); + SharedLocMap prevSharedLocMap = mapFlatMethodToSharedLocMap.get(fm); + SharedLocMap prevDeleteSet = mapFlatMethodToDeleteSet.get(fm); - if (!deleteSet.equals(prevDeleteSet)) { + if (!(deleteSet.equals(prevDeleteSet) && sharedLocMap.equals(prevSharedLocMap))) { + mapFlatMethodToSharedLocMap.put(fm, sharedLocMap); mapFlatMethodToDeleteSet.put(fm, deleteSet); // results for callee changed, so enqueue dependents caller for @@ -276,19 +277,32 @@ public class DefinitelyWrittenCheck { } + sharedLoc_analyzeEventLoop(); + + } + + private void sharedLoc_analyzeEventLoop() { + if (state.SSJAVADEBUG) { + System.out.println("SSJAVA: Definite clearance for shared locations Analyzing: eventloop"); + } + SharedLocMap sharedLocMap = new SharedLocMap(); + SharedLocMap deleteSet = new SharedLocMap(); + sharedLoc_analyzeBody(state.getMethodFlat(methodContainingSSJavaLoop), ssjavaLoopEntrance, + sharedLocMap, deleteSet, true); } - private void sharedLoc_analyzeMethod(FlatMethod fm, Set> deleteSet) { + private void sharedLoc_analyzeMethod(FlatMethod fm, SharedLocMap sharedLocMap, + SharedLocMap deleteSet) { if (state.SSJAVADEBUG) { System.out.println("SSJAVA: Definite clearance for shared locations Analyzing: " + fm); } - sharedLoc_analyzeBody(fm, deleteSet, false); + sharedLoc_analyzeBody(fm, fm, sharedLocMap, deleteSet, false); } - private void sharedLoc_analyzeBody(FlatNode startNode, Set> deleteSet, - boolean isEventLoopBody) { + private void sharedLoc_analyzeBody(FlatMethod fm, FlatNode startNode, SharedLocMap sharedLocMap, + SharedLocMap deleteSet, boolean isEventLoopBody) { // intraprocedural analysis Set flatNodesToVisit = new HashSet(); @@ -298,21 +312,31 @@ public class DefinitelyWrittenCheck { FlatNode fn = flatNodesToVisit.iterator().next(); flatNodesToVisit.remove(fn); - SharedLocMappingSet currSharedSet = new SharedLocMappingSet(); + SharedLocMap currSharedSet = new SharedLocMap(); + SharedLocMap currDeleteSet = new SharedLocMap(); for (int i = 0; i < fn.numPrev(); i++) { FlatNode prevFn = fn.getPrev(i); - SharedLocMappingSet in = mapFlatNodeToSharedLocMapping.get(prevFn); - if (in != null) { - merge(currSharedSet, in); + SharedLocMap inSharedLoc = mapFlatNodeToSharedLocMapping.get(prevFn); + if (inSharedLoc != null) { + mergeSharedLocMap(currSharedSet, inSharedLoc); + } + + SharedLocMap inDeleteLoc = mapFlatNodeToDeleteSet.get(prevFn); + if (inDeleteLoc != null) { + mergeDeleteSet(currDeleteSet, inDeleteLoc); } } - sharedLoc_nodeActions(fn, currSharedSet, deleteSet, isEventLoopBody); + sharedLoc_nodeActions(fm, fn, currSharedSet, currDeleteSet, sharedLocMap, deleteSet, + isEventLoopBody); + + SharedLocMap prevSharedSet = mapFlatNodeToSharedLocMapping.get(fn); + SharedLocMap prevDeleteSet = mapFlatNodeToDeleteSet.get(fn); - SharedLocMappingSet mustSetPrev = mapFlatNodeToSharedLocMapping.get(fn); - if (!currSharedSet.equals(mustSetPrev)) { + if (!(currSharedSet.equals(prevSharedSet) && currDeleteSet.equals(prevDeleteSet))) { mapFlatNodeToSharedLocMapping.put(fn, currSharedSet); + mapFlatNodeToDeleteSet.put(fn, currDeleteSet); for (int i = 0; i < fn.numNext(); i++) { FlatNode nn = fn.getNext(i); if ((!isEventLoopBody) || loopIncElements.contains(nn)) { @@ -326,11 +350,12 @@ public class DefinitelyWrittenCheck { } - private void sharedLoc_nodeActions(FlatNode fn, SharedLocMappingSet curr, - Set> deleteSet, boolean isEventLoopBody) { + private void sharedLoc_nodeActions(FlatMethod fm, FlatNode fn, SharedLocMap curr, + SharedLocMap currDeleteSet, SharedLocMap sharedLocMap, SharedLocMap deleteSet, + boolean isEventLoopBody) { - SharedLocMappingSet killSet = new SharedLocMappingSet(); - SharedLocMappingSet genSet = new SharedLocMappingSet(); + SharedLocMap killSet = new SharedLocMap(); + SharedLocMap genSet = new SharedLocMap(); TempDescriptor lhs; TempDescriptor rhs; @@ -342,55 +367,45 @@ public class DefinitelyWrittenCheck { if (isEventLoopBody) { FlatOpNode fon = (FlatOpNode) fn; - lhs = fon.getDest(); - rhs = fon.getLeft(); - if (!lhs.getSymbol().startsWith("neverused")) { - - if (rhs.getType().isImmutable()) { - NTuple rhsHeapPath = computePath(rhs); + if (fon.getOp().getOp() == Operation.ASSIGN) { + lhs = fon.getDest(); + rhs = fon.getLeft(); - if (rhs.getType().getExtension() instanceof Location - && lhs.getType().getExtension() instanceof CompositeLocation) { - // rhs is field! - Location rhsLoc = (Location) rhs.getType().getExtension(); - - CompositeLocation lhsCompLoc = (CompositeLocation) lhs.getType().getExtension(); - Location dstLoc = lhsCompLoc.get(lhsCompLoc.getSize() - 1); + if (!lhs.getSymbol().startsWith("neverused") && rhs.getType().isImmutable()) { - NTuple heapPath = new NTuple(); - for (int i = 0; i < rhsHeapPath.size() - 1; i++) { - heapPath.add(rhsHeapPath.get(i)); - } + Location dstLoc = getLocation(lhs); + if (dstLoc != null && ssjava.isSharedLocation(dstLoc)) { + System.out.println("FlatOpNode=" + fon); + } - NTuple writeHeapPath = new NTuple(); - writeHeapPath.addAll(heapPath); - writeHeapPath.add(lhs); + NTuple lhsHeapPath = computePath(lhs); + NTuple lhsLocTuple = mapDescriptorToLocationPath.get(lhs); - System.out.println("VAR WRITE:" + fn); - System.out.println("LHS TYPE EXTENSION=" + lhs.getType().getExtension()); - System.out.println("RHS TYPE EXTENSION=" + rhs.getType().getExtension() - + " HEAPPATH=" + rhsHeapPath); + Location srcLoc = getLocation(lhs); - // computing gen/kill set - computeKILLSetForWrite(curr, heapPath, dstLoc, killSet); - if (!dstLoc.equals(rhsLoc)) { - computeGENSetForHigherWrite(curr, heapPath, dstLoc, lhs, genSet); - deleteSet.remove(writeHeapPath); - } else { - computeGENSetForSharedWrite(curr, heapPath, dstLoc, lhs, genSet); - deleteSet.add(writeHeapPath); - } + System.out.println("VAR WRITE:" + fn); + System.out.println("lhsLocTuple=" + lhsLocTuple + " lhsHeapPath=" + lhsHeapPath); + System.out.println("dstLoc=" + dstLoc + " srcLoc=" + srcLoc); + // computing gen/kill set + computeKILLSetForWrite(curr, killSet, lhsLocTuple, lhsHeapPath); + if (!dstLoc.equals(srcLoc)) { + System.out.println("LOC IS DIFFERENT"); + computeGENSetForHigherWrite(curr, killSet, lhsLocTuple, lhsHeapPath); + updateDeleteSetForHigherWrite(currDeleteSet, lhsLocTuple, lhsHeapPath); + } else { + computeGENSetForSameHeightWrite(curr, killSet, lhsLocTuple, lhsHeapPath); + updateDeleteSetForSameHeightWrite(currDeleteSet, lhsLocTuple, lhsHeapPath); } - // System.out.println("fieldLoc=" + fieldLoc + " srcLoc=" + srcLoc); System.out.println("KILLSET=" + killSet); System.out.println("GENSet=" + genSet); - System.out.println("DELETESET=" + deleteSet); + System.out.println("DELETESET=" + currDeleteSet); } } + } } @@ -418,28 +433,29 @@ public class DefinitelyWrittenCheck { if (ssjava.isSharedLocation(fieldLoc)) { // only care the case that loc(f) is shared location // write(field) - NTuple lhsHeapPath = computePath(lhs); - NTuple fldHeapPath = new NTuple(lhsHeapPath.getList()); - fldHeapPath.add(fld); + + NTuple fieldLocTuple = mapDescriptorToLocationPath.get(fld); + NTuple fldHeapPath = computePath(fld); // computing gen/kill set - computeKILLSetForWrite(curr, lhsHeapPath, fieldLoc, killSet); + computeKILLSetForWrite(curr, killSet, fieldLocTuple, fldHeapPath); if (!fieldLoc.equals(srcLoc)) { System.out.println("LOC IS DIFFERENT"); - computeGENSetForHigherWrite(curr, lhsHeapPath, fieldLoc, fld, genSet); - deleteSet.remove(fldHeapPath); + computeGENSetForHigherWrite(curr, killSet, fieldLocTuple, fldHeapPath); + updateDeleteSetForHigherWrite(currDeleteSet, fieldLocTuple, fldHeapPath); } else { - computeGENSetForSharedWrite(curr, lhsHeapPath, fieldLoc, fld, genSet); - deleteSet.add(fldHeapPath); + computeGENSetForSameHeightWrite(curr, killSet, fieldLocTuple, fldHeapPath); + updateDeleteSetForSameHeightWrite(currDeleteSet, fieldLocTuple, fldHeapPath); } - } - System.out.println("################"); - System.out.println("FIELD WRITE:" + fn); - System.out.println("fieldLoc=" + fieldLoc + " srcLoc=" + srcLoc); - System.out.println("KILLSET=" + killSet); - System.out.println("GENSet=" + genSet); - System.out.println("DELETESET=" + deleteSet); + System.out.println("################"); + System.out.println("FIELD WRITE:" + fn); + System.out.println("FldHeapPath=" + fldHeapPath); + System.out.println("fieldLocTuple=" + fieldLocTuple + " srcLoc=" + srcLoc); + System.out.println("KILLSET=" + killSet); + System.out.println("GENSet=" + genSet); + System.out.println("DELETESET=" + currDeleteSet); + } } break; @@ -476,59 +492,95 @@ public class DefinitelyWrittenCheck { // // System.out.println("GENSet=" + GENSet); // } - // break; + break; + + case FKind.FlatExit: { + // merge the current delete/shared loc mapping + mergeSharedLocMap(sharedLocMap, curr); + mergeDeleteSet(deleteSet, currDeleteSet); } - // computeNewMapping(curr, readWriteKillSet, readWriteGenSet); - // System.out.println("#######" + curr); + } + + computeNewMapping(curr, killSet, genSet); + System.out.println("#######" + curr); } - private void computeKILLSetForWrite(SharedLocMappingSet curr, NTuple hp, - Location loc, SharedLocMappingSet killSet) { + private void mergeDeleteSet(SharedLocMap currDeleteSet, SharedLocMap inDeleteLoc) { + + Set> locTupleKeySet = inDeleteLoc.keySet(); + + for (Iterator iterator = locTupleKeySet.iterator(); iterator.hasNext();) { + NTuple locTupleKey = (NTuple) iterator.next(); + + Set> inSet = inDeleteLoc.get(locTupleKey); + currDeleteSet.addWrite(locTupleKey, inSet); - Set currWriteSet = curr.getWriteSet(hp, loc); - if (!currWriteSet.isEmpty()) { - killSet.addWriteSet(hp, loc, currWriteSet); } + } + + private void computeNewMapping(SharedLocMap curr, SharedLocMap killSet, SharedLocMap genSet) { + curr.kill(killSet); + curr.gen(genSet); + } + private void updateDeleteSetForHigherWrite(SharedLocMap currDeleteSet, NTuple locTuple, + NTuple hp) { + currDeleteSet.removeWrite(locTuple, hp); } - private void computeGENSetForHigherWrite(SharedLocMappingSet curr, NTuple hp, - Location loc, Descriptor desc, SharedLocMappingSet genSet) { + private void updateDeleteSetForSameHeightWrite(SharedLocMap currDeleteSet, + NTuple locTuple, NTuple hp) { + currDeleteSet.addWrite(locTuple, hp); + } - Set genWriteSet = new HashSet(); - genWriteSet.addAll(curr.getWriteSet(hp, loc)); - genWriteSet.add(desc); + private void computeGENSetForHigherWrite(SharedLocMap curr, SharedLocMap genSet, + NTuple locTuple, NTuple hp) { + Set> currWriteSet = curr.get(locTuple); - genSet.addWriteSet(hp, loc, genWriteSet); + if (currWriteSet != null) { + genSet.addWrite(locTuple, currWriteSet); + } + genSet.addWrite(locTuple, hp); } - private void computeGENSetForSharedWrite(SharedLocMappingSet curr, NTuple hp, - Location loc, Descriptor desc, SharedLocMappingSet genSet) { + private void computeGENSetForSameHeightWrite(SharedLocMap curr, SharedLocMap genSet, + NTuple locTuple, NTuple hp) { + Set> currWriteSet = curr.get(locTuple); - Set genWriteSet = new HashSet(); - genWriteSet.addAll(curr.getWriteSet(hp, loc)); - genWriteSet.remove(desc); + if (currWriteSet != null) { + genSet.addWrite(locTuple, currWriteSet); + } + genSet.removeWrite(locTuple, hp); + } + + private void computeKILLSetForWrite(SharedLocMap curr, SharedLocMap killSet, + NTuple locTuple, NTuple hp) { - if (!genWriteSet.isEmpty()) { - genSet.addWriteSet(hp, loc, genWriteSet); + Set> writeSet = curr.get(locTuple); + if (writeSet != null) { + killSet.addWrite(locTuple, writeSet); } + } - private void merge(SharedLocMappingSet currSharedSet, SharedLocMappingSet in) { + private void mergeSharedLocMap(SharedLocMap currSharedSet, SharedLocMap in) { - Set> hpKeySet = in.getHeapPathKeySet(); - for (Iterator iterator = hpKeySet.iterator(); iterator.hasNext();) { - NTuple hpKey = (NTuple) iterator.next(); - Set locSet = in.getLocationKeySet(hpKey); - for (Iterator iterator2 = locSet.iterator(); iterator2.hasNext();) { - Location locKey = (Location) iterator2.next(); - Set writeSet = in.getWriteSet(hpKey, locKey); - currSharedSet.intersectWriteSet(hpKey, locKey, writeSet); + Set> locTupleKeySet = in.keySet(); + for (Iterator iterator = locTupleKeySet.iterator(); iterator.hasNext();) { + NTuple locTupleKey = (NTuple) iterator.next(); + + Set> inSet = in.get(locTupleKey); + Set> currSet = currSharedSet.get(locTupleKey); + if (currSet == null) { + currSet = new HashSet>(); + currSet.addAll(inSet); + currSharedSet.addWrite(locTupleKey, currSet); } + currSet.retainAll(inSet); } } @@ -1196,13 +1248,13 @@ public class DefinitelyWrittenCheck { } - if (mapDescriptorToLocationStrPath.containsKey(rhs)) { - mapDescriptorToLocationStrPath.put(lhs, mapDescriptorToLocationStrPath.get(rhs)); + if (mapDescriptorToLocationPath.containsKey(rhs)) { + mapDescriptorToLocationPath.put(lhs, mapDescriptorToLocationPath.get(rhs)); } else { if (rhs.getType().getExtension() instanceof SSJavaType) { NTuple locTuple = ((SSJavaType) rhs.getType().getExtension()).getCompLoc().getTuple(); - mapDescriptorToLocationStrPath.put(lhs, locTuple); + mapDescriptorToLocationPath.put(lhs, locTuple); } } @@ -1232,13 +1284,15 @@ public class DefinitelyWrittenCheck { if (ssjava.isSharedLocation(fieldLocation)) { addSharedLocDescriptor(fieldLocation, fld); - System.out.println("FIELD WRITE FN=" + fn); + // System.out.println("FIELD WRITE FN=" + fn); NTuple locTuple = deriveLocationTuple(md, lhs); locTuple.addAll(deriveLocationTuple(md, fld)); - System.out.println("LOC TUPLE=" + locTuple); + // System.out.println("LOC TUPLE=" + locTuple); // mapLocationPathToMayWrittenSet.put(locTuple, null, fld); addMayWrittenSet(md, locTuple, fld); + + mapDescriptorToLocationPath.put(fld, locTuple); } } @@ -1269,7 +1323,7 @@ public class DefinitelyWrittenCheck { NTuple locTuple = deriveLocationTuple(md, rhs); locTuple.addAll(deriveLocationTuple(md, fld)); - mapDescriptorToLocationStrPath.put(lhs, locTuple); + mapDescriptorToLocationPath.put(lhs, locTuple); } break; @@ -1301,7 +1355,7 @@ public class DefinitelyWrittenCheck { } writeSet.add(d); - System.out.println("ADD WRITE DESC=" + d + " TO locTuple=" + locTuple); + // System.out.println("ADD WRITE DESC=" + d + " TO locTuple=" + locTuple); } private void bindLocationPathCallerArgWithCalleeParam(MethodDescriptor mdCaller, FlatCall fc) { @@ -1739,12 +1793,15 @@ public class DefinitelyWrittenCheck { case FKind.FlatCall: { FlatCall fc = (FlatCall) fn; + // System.out.println("FLATCALL:" + fn); + generateKILLSetForFlatCall(fc, curr, readWriteKillSet); generateGENSetForFlatCall(fc, readWriteGenSet); - // System.out.println("FLATCALL:" + fn); - // System.out.println("KILLSET=" + KILLSet); - // System.out.println("GENSet=" + GENSet); + checkManyRead(fc, curr); + + // System.out.println("KILLSET=" + readWriteKillSet); + // System.out.println("GENSet=" + readWriteGenSet); } break; @@ -1758,6 +1815,18 @@ public class DefinitelyWrittenCheck { } + private void checkManyRead(FlatCall fc, Hashtable, Set> curr) { + + Set> boundReadSet = mapFlatNodeToBoundReadSet.get(fc); + + for (Iterator iterator = boundReadSet.iterator(); iterator.hasNext();) { + NTuple readHeapPath = (NTuple) iterator.next(); + Set writeAgeSet = curr.get(readHeapPath); + checkWriteAgeSet(writeAgeSet, readHeapPath, fc); + } + + } + private void checkWriteAgeSet(Set writeAgeSet, NTuple path, FlatNode fn) { if (writeAgeSet != null) { for (Iterator iterator = writeAgeSet.iterator(); iterator.hasNext();) { @@ -1805,12 +1874,6 @@ public class DefinitelyWrittenCheck { } - private void computeNewMapping(SharedLocMappingSet curr, SharedLocMappingSet KILLSet, - SharedLocMappingSet GENSet) { - curr.kill(KILLSet); - curr.add(GENSet); - } - private void computeNewMapping(Hashtable, Set> curr, Hashtable, Set> KILLSet, Hashtable, Set> GENSet) { @@ -1828,7 +1891,13 @@ public class DefinitelyWrittenCheck { for (Enumeration> e = GENSet.keys(); e.hasMoreElements();) { NTuple key = e.nextElement(); - curr.put(key, GENSet.get(key)); + + Set currWriteAgeSet = curr.get(key); + if (currWriteAgeSet == null) { + currWriteAgeSet = new HashSet(); + curr.put(key, currWriteAgeSet); + } + currWriteAgeSet.addAll(GENSet.get(key)); } } @@ -1981,95 +2050,106 @@ public class DefinitelyWrittenCheck { } private void bindHeapPathCallerArgWithCaleeParamForSharedLoc(FlatCall fc) { - // compute all possible callee set - // transform all DELETE set from the any possible - // callees to the caller - calleeUnionBoundDeleteSet.clear(); - calleeIntersectBoundSharedSet.clear(); - - MethodDescriptor mdCallee = fc.getMethod(); - Set setPossibleCallees = new HashSet(); - setPossibleCallees.addAll(callGraph.getMethods(mdCallee)); - - // create mapping from arg idx to its heap paths - Hashtable> mapArgIdx2CallerArgHeapPath = - new Hashtable>(); - - // arg idx is starting from 'this' arg - if (fc.getThis() != null) { - NTuple thisHeapPath = mapHeapPath.get(fc.getThis()); - if (thisHeapPath == null) { - // method is called without creating new flat node representing 'this' - thisHeapPath = new NTuple(); - thisHeapPath.add(fc.getThis()); - } - - mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath); - } - - for (int i = 0; i < fc.numArgs(); i++) { - TempDescriptor arg = fc.getArg(i); - NTuple argHeapPath = computePath(arg); - mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(i + 1), argHeapPath); - } - - for (Iterator iterator = setPossibleCallees.iterator(); iterator.hasNext();) { - MethodDescriptor callee = (MethodDescriptor) iterator.next(); - FlatMethod calleeFlatMethod = state.getMethodFlat(callee); - - // binding caller's args and callee's params - - Set> calleeReadSet = mapFlatMethodToDeleteSet.get(calleeFlatMethod); - if (calleeReadSet == null) { - calleeReadSet = new HashSet>(); - mapFlatMethodToDeleteSet.put(calleeFlatMethod, calleeReadSet); - } - - Hashtable mapParamIdx2ParamTempDesc = - new Hashtable(); - int offset = 0; - if (calleeFlatMethod.getMethod().isStatic()) { - // static method does not have implicit 'this' arg - offset = 1; - } - for (int i = 0; i < calleeFlatMethod.numParameters(); i++) { - TempDescriptor param = calleeFlatMethod.getParameter(i); - mapParamIdx2ParamTempDesc.put(Integer.valueOf(i + offset), param); - } - - Set> calleeBoundDeleteSet = - bindSet(calleeReadSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath); - // union of the current read set and the current callee's - // read set - calleeUnionBoundDeleteSet.addAll(calleeBoundDeleteSet); - - SharedLocMappingSet calleeSharedLocMap = - mapFlatMethodToSharedLocMappingSet.get(calleeFlatMethod); - - Set> calleeHeapPathKeySet = calleeSharedLocMap.getHeapPathKeySet(); - - for (Iterator iterator2 = calleeHeapPathKeySet.iterator(); iterator2.hasNext();) { - NTuple calleeHeapPathKey = (NTuple) iterator2.next(); - - NTuple calleeBoundHeapPathKey = - bind(calleeHeapPathKey, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath); - - Set calleeLocSet = calleeSharedLocMap.getLocationKeySet(calleeHeapPathKey); - - for (Iterator iterator3 = calleeLocSet.iterator(); iterator3.hasNext();) { - Location calleeLocKey = (Location) iterator3.next(); - Set calleeWriteSet = - calleeSharedLocMap.getWriteSet(calleeHeapPathKey, calleeLocKey); - - calleeIntersectBoundSharedSet.intersectWriteSet(calleeBoundHeapPathKey, calleeLocKey, - calleeWriteSet); - - } - - } - - } - + // // compute all possible callee set + // // transform all DELETE set from the any possible + // // callees to the caller + // calleeUnionBoundDeleteSet.clear(); + // calleeIntersectBoundSharedSet.clear(); + // + // MethodDescriptor mdCallee = fc.getMethod(); + // Set setPossibleCallees = new + // HashSet(); + // setPossibleCallees.addAll(callGraph.getMethods(mdCallee)); + // + // // create mapping from arg idx to its heap paths + // Hashtable> mapArgIdx2CallerArgHeapPath = + // new Hashtable>(); + // + // // arg idx is starting from 'this' arg + // if (fc.getThis() != null) { + // NTuple thisHeapPath = mapHeapPath.get(fc.getThis()); + // if (thisHeapPath == null) { + // // method is called without creating new flat node representing 'this' + // thisHeapPath = new NTuple(); + // thisHeapPath.add(fc.getThis()); + // } + // + // mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath); + // } + // + // for (int i = 0; i < fc.numArgs(); i++) { + // TempDescriptor arg = fc.getArg(i); + // NTuple argHeapPath = computePath(arg); + // mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(i + 1), argHeapPath); + // } + // + // for (Iterator iterator = setPossibleCallees.iterator(); + // iterator.hasNext();) { + // MethodDescriptor callee = (MethodDescriptor) iterator.next(); + // FlatMethod calleeFlatMethod = state.getMethodFlat(callee); + // + // // binding caller's args and callee's params + // + // Set> calleeReadSet = + // mapFlatMethodToDeleteSet.get(calleeFlatMethod); + // if (calleeReadSet == null) { + // calleeReadSet = new HashSet>(); + // mapFlatMethodToDeleteSet.put(calleeFlatMethod, calleeReadSet); + // } + // + // Hashtable mapParamIdx2ParamTempDesc = + // new Hashtable(); + // int offset = 0; + // if (calleeFlatMethod.getMethod().isStatic()) { + // // static method does not have implicit 'this' arg + // offset = 1; + // } + // for (int i = 0; i < calleeFlatMethod.numParameters(); i++) { + // TempDescriptor param = calleeFlatMethod.getParameter(i); + // mapParamIdx2ParamTempDesc.put(Integer.valueOf(i + offset), param); + // } + // + // Set> calleeBoundDeleteSet = + // bindSet(calleeReadSet, mapParamIdx2ParamTempDesc, + // mapArgIdx2CallerArgHeapPath); + // // union of the current read set and the current callee's + // // read set + // calleeUnionBoundDeleteSet.addAll(calleeBoundDeleteSet); + // + // SharedLocMappingSet calleeSharedLocMap = + // mapFlatMethodToSharedLocMappingSet.get(calleeFlatMethod); + // + // Set> calleeHeapPathKeySet = + // calleeSharedLocMap.getHeapPathKeySet(); + // + // for (Iterator iterator2 = calleeHeapPathKeySet.iterator(); + // iterator2.hasNext();) { + // NTuple calleeHeapPathKey = (NTuple) + // iterator2.next(); + // + // NTuple calleeBoundHeapPathKey = + // bind(calleeHeapPathKey, mapParamIdx2ParamTempDesc, + // mapArgIdx2CallerArgHeapPath); + // + // Set calleeLocSet = + // calleeSharedLocMap.getLocationKeySet(calleeHeapPathKey); + // + // for (Iterator iterator3 = calleeLocSet.iterator(); iterator3.hasNext();) + // { + // Location calleeLocKey = (Location) iterator3.next(); + // Set calleeWriteSet = + // calleeSharedLocMap.getWriteSet(calleeHeapPathKey, calleeLocKey); + // + // calleeIntersectBoundSharedSet.intersectWriteSet(calleeBoundHeapPathKey, + // calleeLocKey, + // calleeWriteSet); + // + // } + // + // } + // + // } + // } private NTuple bind(NTuple calleeHeapPathKey, @@ -2193,26 +2273,18 @@ public class DefinitelyWrittenCheck { Set> readSet = new HashSet>(); Set> mustWriteSet = new HashSet>(); Set> mayWriteSet = new HashSet>(); - SharedLocMappingSet sharedLocMapping = new SharedLocMappingSet(); - Set> deleteSet = new HashSet>(); - methodReadWriteSet_analyzeMethod(fm, readSet, mustWriteSet, mayWriteSet, sharedLocMapping, - deleteSet); + methodReadWriteSet_analyzeMethod(fm, readSet, mustWriteSet, mayWriteSet); Set> prevRead = mapFlatMethodToReadSet.get(fm); Set> prevMustWrite = mapFlatMethodToMustWriteSet.get(fm); Set> prevMayWrite = mapFlatMethodToMayWriteSet.get(fm); - SharedLocMappingSet prevSharedLocMapping = mapFlatMethodToSharedLocMappingSet.get(fm); - Set> prevDeleteSet = mapFlatMethodToDeleteSet.get(fm); - if (!(readSet.equals(prevRead) && mustWriteSet.equals(prevMustWrite) - && mayWriteSet.equals(prevMayWrite) && sharedLocMapping.equals(prevSharedLocMapping) && deleteSet - .equals(prevDeleteSet))) { + if (!(readSet.equals(prevRead) && mustWriteSet.equals(prevMustWrite) && mayWriteSet + .equals(prevMayWrite))) { mapFlatMethodToReadSet.put(fm, readSet); mapFlatMethodToMustWriteSet.put(fm, mustWriteSet); mapFlatMethodToMayWriteSet.put(fm, mayWriteSet); - mapFlatMethodToSharedLocMappingSet.put(fm, sharedLocMapping); - mapFlatMethodToDeleteSet.put(fm, deleteSet); // results for callee changed, so enqueue dependents caller for // further @@ -2236,14 +2308,12 @@ public class DefinitelyWrittenCheck { } private void methodReadWriteSet_analyzeMethod(FlatMethod fm, Set> readSet, - Set> mustWriteSet, Set> mayWriteSet, - SharedLocMappingSet sharedLocMapping, Set> deleteSet) { + Set> mustWriteSet, Set> mayWriteSet) { if (state.SSJAVADEBUG) { System.out.println("SSJAVA: Definitely written Analyzing: " + fm); } - methodReadWriteSet_analyzeBody(fm, readSet, mustWriteSet, mayWriteSet, sharedLocMapping, - deleteSet, false); + methodReadWriteSet_analyzeBody(fm, readSet, mustWriteSet, mayWriteSet, false); } @@ -2261,23 +2331,17 @@ public class DefinitelyWrittenCheck { Set> readSet = new HashSet>(); Set> mustWriteSet = new HashSet>(); Set> mayWriteSet = new HashSet>(); - SharedLocMappingSet sharedLocMapping = new SharedLocMappingSet(); - Set> deleteSet = new HashSet>(); mapFlatMethodToReadSet.put(flatMethodContainingSSJavaLoop, readSet); mapFlatMethodToMustWriteSet.put(flatMethodContainingSSJavaLoop, mustWriteSet); mapFlatMethodToMayWriteSet.put(flatMethodContainingSSJavaLoop, mayWriteSet); - mapFlatMethodToSharedLocMappingSet.put(flatMethodContainingSSJavaLoop, sharedLocMapping); - mapFlatMethodToDeleteSet.put(flatMethodContainingSSJavaLoop, deleteSet); - methodReadWriteSet_analyzeBody(ssjavaLoopEntrance, readSet, mustWriteSet, mayWriteSet, - sharedLocMapping, deleteSet, true); + methodReadWriteSet_analyzeBody(ssjavaLoopEntrance, readSet, mustWriteSet, mayWriteSet, true); } private void methodReadWriteSet_analyzeBody(FlatNode startNode, Set> readSet, Set> mustWriteSet, Set> mayWriteSet, - SharedLocMappingSet sharedLocMapping, Set> deleteSet, boolean isEventLoopBody) { // intraprocedural analysis @@ -2288,29 +2352,23 @@ public class DefinitelyWrittenCheck { FlatNode fn = flatNodesToVisit.iterator().next(); flatNodesToVisit.remove(fn); - SharedLocMappingSet currSharedLocMapping = new SharedLocMappingSet(); Set> currMustWriteSet = new HashSet>(); for (int i = 0; i < fn.numPrev(); i++) { FlatNode prevFn = fn.getPrev(i); Set> in = mapFlatNodeToMustWriteSet.get(prevFn); - SharedLocMappingSet inSharedLoc = mapFlatNodeToSharedLocMapping.get(prevFn); if (in != null) { merge(currMustWriteSet, in); - merge(currSharedLocMapping, inSharedLoc); } } methodReadWriteSet_nodeActions(fn, currMustWriteSet, readSet, mustWriteSet, mayWriteSet, - currSharedLocMapping, sharedLocMapping, deleteSet, isEventLoopBody); + isEventLoopBody); - SharedLocMappingSet prevSharedLocSet = mapFlatNodeToSharedLocMapping.get(fn); Set> mustSetPrev = mapFlatNodeToMustWriteSet.get(fn); - if ((!currMustWriteSet.equals(mustSetPrev)) - || (!currSharedLocMapping.equals(prevSharedLocSet))) { + if (!currMustWriteSet.equals(mustSetPrev)) { mapFlatNodeToMustWriteSet.put(fn, currMustWriteSet); - mapFlatNodeToSharedLocMapping.put(fn, currSharedLocMapping); for (int i = 0; i < fn.numNext(); i++) { FlatNode nn = fn.getNext(i); if ((!isEventLoopBody) || loopIncElements.contains(nn)) { @@ -2327,11 +2385,7 @@ public class DefinitelyWrittenCheck { private void methodReadWriteSet_nodeActions(FlatNode fn, Set> currMustWriteSet, Set> readSet, Set> mustWriteSet, Set> mayWriteSet, - SharedLocMappingSet currSharedLocMapping, SharedLocMappingSet sharedLocMapping, - Set> deleteSet, boolean isEventLoopBody) { - - SharedLocMappingSet killSetSharedLoc = new SharedLocMappingSet(); - SharedLocMappingSet genSetSharedLoc = new SharedLocMappingSet(); + boolean isEventLoopBody) { TempDescriptor lhs; TempDescriptor rhs; @@ -2394,17 +2448,21 @@ public class DefinitelyWrittenCheck { System.out.println("RHS TYPE EXTENSION=" + rhs.getType().getExtension() + " HEAPPATH=" + rhsHeapPath); + // TODO // computing gen/kill set - computeKILLSetForWrite(currSharedLocMapping, heapPath, dstLoc, killSetSharedLoc); - if (!dstLoc.equals(rhsLoc)) { - computeGENSetForHigherWrite(currSharedLocMapping, heapPath, dstLoc, lhs, - genSetSharedLoc); - deleteSet.remove(writeHeapPath); - } else { - computeGENSetForSharedWrite(currSharedLocMapping, heapPath, dstLoc, lhs, - genSetSharedLoc); - deleteSet.add(writeHeapPath); - } + // computeKILLSetForWrite(currSharedLocMapping, heapPath, dstLoc, + // killSetSharedLoc); + // if (!dstLoc.equals(rhsLoc)) { + // computeGENSetForHigherWrite(currSharedLocMapping, heapPath, + // dstLoc, lhs, + // genSetSharedLoc); + // deleteSet.remove(writeHeapPath); + // } else { + // computeGENSetForSharedWrite(currSharedLocMapping, heapPath, + // dstLoc, lhs, + // genSetSharedLoc); + // deleteSet.add(writeHeapPath); + // } } } @@ -2467,8 +2525,6 @@ public class DefinitelyWrittenCheck { // x.f=y; if (fn.kind() == FKind.FlatSetFieldNode) { - SharedLocMappingSet killSet = new SharedLocMappingSet(); - SharedLocMappingSet genSet = new SharedLocMappingSet(); FlatSetFieldNode fsfn = (FlatSetFieldNode) fn; lhs = fsfn.getDst(); fld = fsfn.getField(); @@ -2496,32 +2552,6 @@ public class DefinitelyWrittenCheck { currMustWriteSet.add(fldHeapPath); mayWriteSet.add(fldHeapPath); - // shared loc extension - Location srcLoc = getLocation(rhs); - Location fieldLoc = (Location) fld.getType().getExtension(); - if (ssjava.isSharedLocation(fieldLoc)) { - // only care the case that loc(f) is shared location - // write(field) - - computeKILLSetForWrite(currSharedLocMapping, lhsHeapPath, fieldLoc, killSetSharedLoc); - if (!fieldLoc.equals(srcLoc)) { - computeGENSetForHigherWrite(currSharedLocMapping, lhsHeapPath, fieldLoc, fld, - genSetSharedLoc); - deleteSet.remove(fldHeapPath); - } else { - computeGENSetForSharedWrite(currSharedLocMapping, lhsHeapPath, fieldLoc, fld, - genSetSharedLoc); - deleteSet.add(fldHeapPath); - } - } - - System.out.println("################"); - System.out.println("FIELD WRITE:" + fn); - System.out.println("fieldLoc=" + fieldLoc + " srcLoc=" + srcLoc); - System.out.println("KILLSET=" + killSetSharedLoc); - System.out.println("GENSet=" + genSetSharedLoc); - System.out.println("DELETESET=" + deleteSet); - } } @@ -2561,59 +2591,17 @@ public class DefinitelyWrittenCheck { mayWriteSet.add(write); } - // shared loc extension - bindHeapPathCallerArgWithCaleeParamForSharedLoc(fc); - - generateKILLSharedSetForFlatCall(currSharedLocMapping, killSetSharedLoc); - generateGENSharedSetForFlatCall(currSharedLocMapping, genSetSharedLoc); - - System.out.println("### Analyzing FC=" + fc); - System.out.println("### BOUNDSET=" + calleeIntersectBoundSharedSet); - System.out.println("### GEN=" + genSetSharedLoc); - System.out.println("### KILL=" + killSetSharedLoc); } break; case FKind.FlatExit: { // merge the current written set with OVERWRITE set merge(mustWriteSet, currMustWriteSet); - - // shared loc extension - merge(sharedLocMapping, currSharedLocMapping); } break; } - computeNewMapping(currSharedLocMapping, killSetSharedLoc, genSetSharedLoc); - - } - - private void generateGENSharedSetForFlatCall(SharedLocMappingSet currSharedLocMapping, - SharedLocMappingSet genSetSharedLoc) { - - Set> hpKeySet = calleeIntersectBoundSharedSet.getHeapPathKeySet(); - for (Iterator iterator = hpKeySet.iterator(); iterator.hasNext();) { - NTuple hpKey = (NTuple) iterator.next(); - Set locKeySet = calleeIntersectBoundSharedSet.getLocationKeySet(hpKey); - for (Iterator iterator2 = locKeySet.iterator(); iterator2.hasNext();) { - Location locKey = (Location) iterator2.next(); - - Set calleeBoundWriteSet = - calleeIntersectBoundSharedSet.getWriteSet(hpKey, locKey); - System.out.println("calleeBoundWriteSet=" + calleeBoundWriteSet + " hp=" + hpKey + " loc=" - + locKey); - Set removeSet = computeRemoveSet(hpKey, locKey); - - Set currWriteSet = currSharedLocMapping.getWriteSet(hpKey, locKey); - - genSetSharedLoc.addWriteSet(hpKey, locKey, currWriteSet); - genSetSharedLoc.addWriteSet(hpKey, locKey, calleeBoundWriteSet); - genSetSharedLoc.removeWriteSet(hpKey, locKey, removeSet); - - } - } - } public NTuple getPrefix(NTuple in) { @@ -2637,21 +2625,6 @@ public class DefinitelyWrittenCheck { return removeSet; } - private void generateKILLSharedSetForFlatCall(SharedLocMappingSet currSharedLocMapping, - SharedLocMappingSet killSetSharedLoc) { - - Set> hpKeySet = calleeIntersectBoundSharedSet.getHeapPathKeySet(); - for (Iterator iterator = hpKeySet.iterator(); iterator.hasNext();) { - NTuple hpKey = (NTuple) iterator.next(); - Set locKeySet = calleeIntersectBoundSharedSet.getLocationKeySet(hpKey); - for (Iterator iterator2 = locKeySet.iterator(); iterator2.hasNext();) { - Location locKey = (Location) iterator2.next(); - Set currWriteSet = currSharedLocMapping.getWriteSet(hpKey, locKey); - killSetSharedLoc.addWriteSet(hpKey, locKey, currWriteSet); - } - } - } - static public FieldDescriptor getArrayField(TypeDescriptor td) { FieldDescriptor fd = mapTypeToArrayField.get(td); if (fd == null) { @@ -2858,7 +2831,7 @@ public class DefinitelyWrittenCheck { return deps; } - private NTuple computePath(TempDescriptor td) { + private NTuple computePath(Descriptor td) { // generate proper path fot input td // if td is local variable, it just generate one element tuple path if (mapHeapPath.containsKey(td)) { @@ -2882,8 +2855,8 @@ public class DefinitelyWrittenCheck { assert td.getType() != null; - if (mapDescriptorToLocationStrPath.containsKey(td)) { - return mapDescriptorToLocationStrPath.get(td); + if (mapDescriptorToLocationPath.containsKey(td)) { + return mapDescriptorToLocationPath.get(td); } else { if (td.getSymbol().startsWith("this")) { return deriveThisLocationTuple(md);