X-Git-Url: http://plrg.eecs.uci.edu/git/?p=IRC.git;a=blobdiff_plain;f=Robust%2Fsrc%2FAnalysis%2FSSJava%2FDefinitelyWrittenCheck.java;h=fabdf9dbbdbe09f2fb0f0f7c7c9b9618d53be0de;hp=fd51237cd61d76f4e4a5d912509a5fb76bc46704;hb=d45bb251bdc1196d7848094fa2ccd566b39e021c;hpb=721409a448d35d8ef42faf7fbbe96d4e425081ae diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java index fd51237c..fabdf9db 100644 --- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java +++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java @@ -1,8 +1,5 @@ package Analysis.SSJava; -import java.io.BufferedWriter; -import java.io.FileWriter; -import java.io.IOException; import java.util.Enumeration; import java.util.HashSet; import java.util.Hashtable; @@ -11,6 +8,7 @@ import java.util.LinkedList; import java.util.Set; import java.util.Stack; +import Analysis.Liveness; import Analysis.CallGraph.CallGraph; import Analysis.Loops.LoopFinder; import IR.Descriptor; @@ -33,7 +31,6 @@ import IR.Flat.FlatSetElementNode; import IR.Flat.FlatSetFieldNode; import IR.Flat.TempDescriptor; import IR.Tree.Modifiers; -import Util.Pair; public class DefinitelyWrittenCheck { @@ -41,12 +38,9 @@ public class DefinitelyWrittenCheck { State state; CallGraph callGraph; - int debugcount = 0; + Liveness liveness; - // maps a descriptor to its known dependents: namely - // methods or tasks that call the descriptor's method - // AND are part of this analysis (reachable from main) - private Hashtable> mapDescriptorToSetDependents; + int debugcount = 0; // maps a flat node to its WrittenSet: this keeps all heap path overwritten // previously. @@ -73,6 +67,8 @@ public class DefinitelyWrittenCheck { // written to but not overwritten by the higher value private Hashtable mapFlatMethodToDeleteSet; + private Hashtable mapFlatMethodToMustClearMap; + // 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 mapFlatMethodToSharedLocMap; @@ -119,10 +115,7 @@ public class DefinitelyWrittenCheck { private Hashtable mapFlatNodeToSharedLocMapping; private Hashtable mapFlatNodeToDeleteSet; - - private Hashtable> mapSharedLocationToCoverSet; - - private LinkedList sortedDescriptors; + private Hashtable mapFlatNodeToMustClearMap; private LoopFinder ssjavaLoop; private Set loopIncElements; @@ -132,6 +125,9 @@ public class DefinitelyWrittenCheck { private Set> calleeUnionBoundMayWriteSet; private SharedLocMap calleeUnionBoundDeleteSet; private SharedLocMap calleeIntersectBoundSharedSet; + private SharedLocMap calleeIntersectBoundMustClearSet; + + Set liveInTempSetToEventLoop; private Hashtable mapDescToLocation; @@ -144,7 +140,6 @@ public class DefinitelyWrittenCheck { this.ssjava = ssjava; this.callGraph = ssjava.getCallGraph(); this.mapFlatNodeToMustWriteSet = new Hashtable>>(); - this.mapDescriptorToSetDependents = new Hashtable>(); this.mapHeapPath = new Hashtable>(); this.mapDescriptorToLocationPath = new Hashtable>(); this.mapFlatMethodToReadSet = new Hashtable>>(); @@ -166,7 +161,6 @@ public class DefinitelyWrittenCheck { this.mapFlatNodeToBoundReadSet = new Hashtable>>(); this.mapFlatNodeToBoundMustWriteSet = new Hashtable>>(); this.mapFlatNodeToBoundMayWriteSet = new Hashtable>>(); - this.mapSharedLocationToCoverSet = new Hashtable>(); this.mapFlatNodeToSharedLocMapping = new Hashtable(); this.mapFlatMethodToDeleteSet = new Hashtable(); this.calleeUnionBoundDeleteSet = new SharedLocMap(); @@ -175,6 +169,11 @@ public class DefinitelyWrittenCheck { this.mapMethodToSharedLocCoverSet = new Hashtable, NTuple>>(); this.mapFlatNodeToDeleteSet = new Hashtable(); + this.liveness = new Liveness(); + this.liveInTempSetToEventLoop = new HashSet(); + this.mapFlatNodeToMustClearMap = new Hashtable(); + this.calleeIntersectBoundMustClearSet = new SharedLocMap(); + this.mapFlatMethodToMustClearMap = new Hashtable(); } public void definitelyWrittenCheck() { @@ -194,8 +193,7 @@ public class DefinitelyWrittenCheck { private void sharedLocAnalysis() { // perform method READ/OVERWRITE analysis - LinkedList descriptorListToAnalyze = - (LinkedList) sortedDescriptors.clone(); + LinkedList descriptorListToAnalyze = ssjava.getSortedDescriptors(); // current descriptors to visit in fixed-point interprocedural analysis, // prioritized by @@ -220,19 +218,23 @@ public class DefinitelyWrittenCheck { SharedLocMap sharedLocMap = new SharedLocMap(); SharedLocMap deleteSet = new SharedLocMap(); + SharedLocMap mustClearMap = new SharedLocMap(); - sharedLoc_analyzeMethod(fm, sharedLocMap, deleteSet); + sharedLoc_analyzeMethod(fm, sharedLocMap, deleteSet, mustClearMap); SharedLocMap prevSharedLocMap = mapFlatMethodToSharedLocMap.get(fm); SharedLocMap prevDeleteSet = mapFlatMethodToDeleteSet.get(fm); + SharedLocMap prevMustClearMap = mapFlatMethodToMustClearMap.get(fm); - if (!(deleteSet.equals(prevDeleteSet) && sharedLocMap.equals(prevSharedLocMap))) { + if (!(deleteSet.equals(prevDeleteSet) && sharedLocMap.equals(prevSharedLocMap) && mustClearMap + .equals(prevMustClearMap))) { mapFlatMethodToSharedLocMap.put(fm, sharedLocMap); mapFlatMethodToDeleteSet.put(fm, deleteSet); + mapFlatMethodToMustClearMap.put(fm, mustClearMap); // results for callee changed, so enqueue dependents caller for // further // analysis - Iterator depsItr = getDependents(md).iterator(); + Iterator depsItr = ssjava.getDependents(md).iterator(); while (depsItr.hasNext()) { MethodDescriptor methodNext = depsItr.next(); if (!methodDescriptorsToVisitStack.contains(methodNext) @@ -256,23 +258,24 @@ public class DefinitelyWrittenCheck { } SharedLocMap sharedLocMap = new SharedLocMap(); SharedLocMap deleteSet = new SharedLocMap(); + SharedLocMap mustClearMap = new SharedLocMap(); sharedLoc_analyzeBody(state.getMethodFlat(methodContainingSSJavaLoop), - ssjava.getSSJavaLoopEntrance(), sharedLocMap, deleteSet, true); + ssjava.getSSJavaLoopEntrance(), sharedLocMap, deleteSet, mustClearMap, true); } private void sharedLoc_analyzeMethod(FlatMethod fm, SharedLocMap sharedLocMap, - SharedLocMap deleteSet) { + SharedLocMap deleteSet, SharedLocMap mustClearMap) { if (state.SSJAVADEBUG) { System.out.println("SSJAVA: Definite clearance for shared locations Analyzing: " + fm); } - sharedLoc_analyzeBody(fm, fm, sharedLocMap, deleteSet, false); + sharedLoc_analyzeBody(fm, fm, sharedLocMap, deleteSet, mustClearMap, false); } private void sharedLoc_analyzeBody(FlatMethod fm, FlatNode startNode, SharedLocMap sharedLocMap, - SharedLocMap deleteSet, boolean isEventLoopBody) { + SharedLocMap deleteSet, SharedLocMap mustClearMap, boolean isEventLoopBody) { // intraprocedural analysis Set flatNodesToVisit = new HashSet(); @@ -284,6 +287,7 @@ public class DefinitelyWrittenCheck { SharedLocMap currSharedSet = new SharedLocMap(); SharedLocMap currDeleteSet = new SharedLocMap(); + SharedLocMap currMustClearMap = new SharedLocMap(); for (int i = 0; i < fn.numPrev(); i++) { FlatNode prevFn = fn.getPrev(i); @@ -296,17 +300,26 @@ public class DefinitelyWrittenCheck { if (inDeleteLoc != null) { mergeDeleteSet(currDeleteSet, inDeleteLoc); } + + SharedLocMap inMustClearMap = mapFlatNodeToMustClearMap.get(prevFn); + if (inMustClearMap != null) { + mergeSharedLocMap(currMustClearMap, inMustClearMap); + } + } - sharedLoc_nodeActions(fm, fn, currSharedSet, currDeleteSet, sharedLocMap, deleteSet, - isEventLoopBody); + sharedLoc_nodeActions(fm, fn, currSharedSet, currDeleteSet, currMustClearMap, sharedLocMap, + deleteSet, mustClearMap, isEventLoopBody); SharedLocMap prevSharedSet = mapFlatNodeToSharedLocMapping.get(fn); SharedLocMap prevDeleteSet = mapFlatNodeToDeleteSet.get(fn); + SharedLocMap prevMustClearMap = mapFlatNodeToMustClearMap.get(fn); - if (!(currSharedSet.equals(prevSharedSet) && currDeleteSet.equals(prevDeleteSet))) { + if (!(currSharedSet.equals(prevSharedSet) && currDeleteSet.equals(prevDeleteSet) && currMustClearMap + .equals(prevMustClearMap))) { mapFlatNodeToSharedLocMapping.put(fn, currSharedSet); mapFlatNodeToDeleteSet.put(fn, currDeleteSet); + mapFlatNodeToMustClearMap.put(fn, currMustClearMap); for (int i = 0; i < fn.numNext(); i++) { FlatNode nn = fn.getNext(i); if ((!isEventLoopBody) || loopIncElements.contains(nn)) { @@ -321,8 +334,10 @@ public class DefinitelyWrittenCheck { } private void sharedLoc_nodeActions(FlatMethod fm, FlatNode fn, SharedLocMap curr, - SharedLocMap currDeleteSet, SharedLocMap sharedLocMap, SharedLocMap deleteSet, - boolean isEventLoopBody) { + SharedLocMap currDeleteSet, SharedLocMap currMustClearMap, SharedLocMap sharedLocMap, + SharedLocMap deleteSet, SharedLocMap mustClearMap, boolean isEventLoopBody) { + + MethodDescriptor md = fm.getMethod(); SharedLocMap killSet = new SharedLocMap(); SharedLocMap genSet = new SharedLocMap(); @@ -331,6 +346,10 @@ public class DefinitelyWrittenCheck { TempDescriptor rhs; FieldDescriptor fld; + NTuple fieldLocTuple = null; + Location fieldLoc = null; + boolean isHigherWriteCase = false; + switch (fn.kind()) { case FKind.FlatOpNode: { @@ -342,37 +361,35 @@ public class DefinitelyWrittenCheck { lhs = fon.getDest(); rhs = fon.getLeft(); - if (!lhs.getSymbol().startsWith("neverused") && rhs.getType().isImmutable()) { + if (!lhs.getSymbol().startsWith("neverused") && !lhs.getSymbol().startsWith("leftop") + && !lhs.getSymbol().startsWith("rightop") && rhs.getType().isImmutable()) { - Location dstLoc = getLocation(lhs); - if (dstLoc != null && ssjava.isSharedLocation(dstLoc)) { - NTuple lhsHeapPath = computePath(lhs); - NTuple lhsLocTuple = mapDescriptorToLocationPath.get(lhs); + if (mapHeapPath.containsKey(rhs)) { + Location dstLoc = getLocation(lhs); + if (dstLoc != null && ssjava.isSharedLocation(dstLoc)) { + NTuple lhsHeapPath = computePath(lhs); + NTuple lhsLocTuple = mapDescriptorToLocationPath.get(lhs); - Location srcLoc = getLocation(lhs); + Location srcLoc = getLocation(lhs); - // computing gen/kill set - computeKILLSetForWrite(curr, killSet, lhsLocTuple, lhsHeapPath); - if (!dstLoc.equals(srcLoc)) { - computeGENSetForHigherWrite(curr, killSet, lhsLocTuple, lhsHeapPath); - updateDeleteSetForHigherWrite(currDeleteSet, lhsLocTuple, lhsHeapPath); - } else { - computeGENSetForSameHeightWrite(curr, killSet, lhsLocTuple, lhsHeapPath); - updateDeleteSetForSameHeightWrite(currDeleteSet, lhsLocTuple, lhsHeapPath); - } + // computing gen/kill set + computeKILLSetForWrite(curr, killSet, lhsLocTuple, lhsHeapPath); - // System.out.println("VAR WRITE:" + fn); - // System.out.println("lhsLocTuple=" + lhsLocTuple + - // " lhsHeapPath=" - // + lhsHeapPath); - // System.out.println("dstLoc=" + dstLoc + " srcLoc=" + srcLoc); - // System.out.println("KILLSET=" + killSet); - // System.out.println("GENSet=" + genSet); - // System.out.println("DELETESET=" + currDeleteSet); + if (!ssjava.isSameHeightWrite(fn)) { + computeGENSetForHigherWrite(curr, killSet, lhsLocTuple, lhsHeapPath); + updateDeleteSetForHigherWrite(currDeleteSet, lhsLocTuple, lhsHeapPath); + } else { + computeGENSetForSameHeightWrite(curr, killSet, lhsLocTuple, lhsHeapPath); + updateDeleteSetForSameHeightWrite(currDeleteSet, lhsLocTuple, lhsHeapPath); + } + } + } else { + break; } } + } } @@ -383,7 +400,6 @@ public class DefinitelyWrittenCheck { case FKind.FlatSetFieldNode: case FKind.FlatSetElementNode: { - Location fieldLoc; if (fn.kind() == FKind.FlatSetFieldNode) { FlatSetFieldNode fsfn = (FlatSetFieldNode) fn; lhs = fsfn.getDst(); @@ -391,14 +407,33 @@ public class DefinitelyWrittenCheck { rhs = fsfn.getSrc(); fieldLoc = (Location) fld.getType().getExtension(); } else { - FlatSetElementNode fsen = (FlatSetElementNode) fn; - lhs = fsen.getDst(); - rhs = fsen.getSrc(); - TypeDescriptor td = lhs.getType().dereference(); - fld = getArrayField(td); + break; + } + + if (!isEventLoopBody && fieldLoc.getDescriptor().equals(md)) { + // if the field belongs to the local lattice, no reason to calculate + // shared location + break; + } + + fieldLocTuple = new NTuple(); + if (fld.isStatic()) { + if (fld.isFinal()) { + // in this case, fld has TOP location + Location topLocation = Location.createTopLocation(md); + fieldLocTuple.add(topLocation); + } else { + fieldLocTuple.addAll(deriveGlobalLocationTuple(md)); + if (fn.kind() == FKind.FlatSetFieldNode) { + fieldLocTuple.add((Location) fld.getType().getExtension()); + } + } - NTuple locTuple = mapDescriptorToLocationPath.get(lhs); - fieldLoc = locTuple.get(locTuple.size() - 1); + } else { + fieldLocTuple.addAll(deriveLocationTuple(md, lhs)); + if (fn.kind() == FKind.FlatSetFieldNode) { + fieldLocTuple.add((Location) fld.getType().getExtension()); + } } // shared loc extension @@ -407,31 +442,30 @@ public class DefinitelyWrittenCheck { // only care the case that loc(f) is shared location // write(field) - NTuple fieldLocTuple = new NTuple(); - - fieldLocTuple.addAll(mapDescriptorToLocationPath.get(lhs)); - fieldLocTuple.add(fieldLoc); + // NTuple fieldLocTuple = new NTuple(); + // fieldLocTuple.addAll(mapDescriptorToLocationPath.get(lhs)); + // fieldLocTuple.add(fieldLoc); - NTuple fldHeapPath = computePath(fld); + NTuple fldHeapPath = new NTuple(); + fldHeapPath.addAll(computePath(lhs)); + if (fn.kind() == FKind.FlatSetFieldNode) { + fldHeapPath.add(fld); + } // computing gen/kill set computeKILLSetForWrite(curr, killSet, fieldLocTuple, fldHeapPath); - if (!fieldLoc.equals(srcLoc)) { + + if (!ssjava.isSameHeightWrite(fn)) { computeGENSetForHigherWrite(curr, genSet, fieldLocTuple, fldHeapPath); updateDeleteSetForHigherWrite(currDeleteSet, fieldLocTuple, fldHeapPath); + + isHigherWriteCase = true; + } else { computeGENSetForSameHeightWrite(curr, genSet, fieldLocTuple, fldHeapPath); updateDeleteSetForSameHeightWrite(currDeleteSet, fieldLocTuple, fldHeapPath); } - // 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); } } @@ -440,19 +474,17 @@ public class DefinitelyWrittenCheck { case FKind.FlatCall: { FlatCall fc = (FlatCall) fn; - if (ssjava.needTobeAnnotated(fc.getMethod())) { - - bindHeapPathCallerArgWithCaleeParamForSharedLoc(fm.getMethod(), fc); + bindHeapPathCallerArgWithCaleeParamForSharedLoc(fm.getMethod(), fc); - // computing gen/kill set - generateKILLSetForFlatCall(curr, killSet); - generateGENSetForFlatCall(curr, genSet); + // computing gen/kill set + generateKILLSetForFlatCall(curr, killSet); + generateGENSetForFlatCall(curr, genSet); + Set> locTupleSet = calleeIntersectBoundMustClearSet.keySet(); + for (Iterator iterator = locTupleSet.iterator(); iterator.hasNext();) { + NTuple locTupleKey = (NTuple) iterator.next(); + currMustClearMap.addWrite(locTupleKey, calleeIntersectBoundMustClearSet.get(locTupleKey)); } - // System.out.println("#FLATCALL=" + fc); - // System.out.println("KILLSET=" + killSet); - // System.out.println("GENSet=" + genSet); - // System.out.println("bound DELETE Set=" + calleeUnionBoundDeleteSet); } break; @@ -461,15 +493,38 @@ public class DefinitelyWrittenCheck { // merge the current delete/shared loc mapping mergeSharedLocMap(sharedLocMap, curr); mergeDeleteSet(deleteSet, currDeleteSet); - - // System.out.println("#FLATEXIT sharedLocMap=" + sharedLocMap); + mergeSharedLocMap(mustClearMap, currMustClearMap); } break; } computeNewMapping(curr, killSet, genSet); - // System.out.println("#######" + curr); + if (isHigherWriteCase) { + // check all locations with the same shared location are cleared out at this point + Set> writtenSet = curr.get(fieldLocTuple); + Set requirementSet = ssjava.getSharedDescSet(fieldLoc); + + if (checkAllSharedLocationsAreOverwritten(requirementSet, writtenSet)) { + currMustClearMap.addWrite(fieldLocTuple, writtenSet); + } + } + } + + private boolean checkAllSharedLocationsAreOverwritten(Set sharedDescSet, + Set> writtenSet) { + + if (sharedDescSet == null || writtenSet == null) { + return false; + } + Set writtenDescSet = new HashSet(); + for (Iterator iterator = writtenSet.iterator(); iterator.hasNext();) { + NTuple tuple = (NTuple) iterator.next(); + writtenDescSet.add(tuple.get(tuple.size() - 1)); + } + + return writtenDescSet.containsAll(sharedDescSet); + // return sharedDescSet.containsAll(writtenDescSet); } @@ -531,7 +586,6 @@ public class DefinitelyWrittenCheck { if (currWriteSet != null) { genSet.addWrite(locTuple, currWriteSet); } - genSet.addWrite(locTuple, hp); } @@ -574,8 +628,7 @@ public class DefinitelyWrittenCheck { } private void computeSharedCoverSet() { - LinkedList descriptorListToAnalyze = - (LinkedList) sortedDescriptors.clone(); + LinkedList descriptorListToAnalyze = ssjava.getSortedDescriptors(); // current descriptors to visit in fixed-point interprocedural analysis, // prioritized by @@ -610,6 +663,7 @@ public class DefinitelyWrittenCheck { private void computeSharedCoverSet_analyzeMethod(FlatMethod fm, boolean onlyVisitSSJavaLoop) { MethodDescriptor md = fm.getMethod(); + Set flatNodesToVisit = new HashSet(); Set visited = new HashSet(); @@ -625,7 +679,7 @@ public class DefinitelyWrittenCheck { flatNodesToVisit.remove(fn); visited.add(fn); - computeSharedCoverSet_nodeActions(md, fn); + computeSharedCoverSet_nodeActions(md, fn, onlyVisitSSJavaLoop); for (int i = 0; i < fn.numNext(); i++) { FlatNode nn = fn.getNext(i); @@ -642,12 +696,12 @@ public class DefinitelyWrittenCheck { } - private void computeSharedCoverSet_nodeActions(MethodDescriptor md, FlatNode fn) { + private void computeSharedCoverSet_nodeActions(MethodDescriptor md, FlatNode fn, + boolean isEventLoopBody) { TempDescriptor lhs; TempDescriptor rhs; FieldDescriptor fld; - switch (fn.kind()) { case FKind.FlatLiteralNode: { @@ -664,10 +718,6 @@ public class DefinitelyWrittenCheck { if (lhs.getType().getExtension() instanceof SSJavaType) { CompositeLocation compLoc = ((SSJavaType) lhs.getType().getExtension()).getCompLoc(); Location lastLocElement = compLoc.get(compLoc.getSize() - 1); - // check if the last one is shared loc - if (ssjava.isSharedLocation(lastLocElement)) { - addSharedLocDescriptor(lastLocElement, lhs); - } } } @@ -682,53 +732,60 @@ public class DefinitelyWrittenCheck { rhs = fon.getLeft(); lhs = fon.getDest(); - NTuple rhsLocTuple = new NTuple(); - NTuple lhsLocTuple = new NTuple(); - if (mapDescriptorToLocationPath.containsKey(rhs)) { - mapDescriptorToLocationPath.put(lhs, mapDescriptorToLocationPath.get(rhs)); - } else { - // rhs side - if (rhs.getType().getExtension() != null - && rhs.getType().getExtension() instanceof SSJavaType) { - - if (((SSJavaType) rhs.getType().getExtension()).getCompLoc() != null) { - rhsLocTuple.addAll(((SSJavaType) rhs.getType().getExtension()).getCompLoc() - .getTuple()); - } + if (!lhs.getSymbol().startsWith("neverused") && !lhs.getSymbol().startsWith("leftop") + && !lhs.getSymbol().startsWith("rightop")) { - } else { - NTuple locTuple = deriveLocationTuple(md, rhs); - if (locTuple != null) { - rhsLocTuple.addAll(locTuple); - } - } - if (rhsLocTuple.size() > 0) { - mapDescriptorToLocationPath.put(rhs, rhsLocTuple); - } + if (mapHeapPath.containsKey(rhs)) { + NTuple rhsLocTuple = new NTuple(); + NTuple lhsLocTuple = new NTuple(); + if (mapDescriptorToLocationPath.containsKey(rhs)) { + mapDescriptorToLocationPath.put(lhs, deriveLocationTuple(md, rhs)); + lhsLocTuple = mapDescriptorToLocationPath.get(lhs); + } else { + // rhs side + if (rhs.getType().getExtension() != null + && rhs.getType().getExtension() instanceof SSJavaType) { - // lhs side - if (lhs.getType().getExtension() != null - && lhs.getType().getExtension() instanceof SSJavaType) { - lhsLocTuple.addAll(((SSJavaType) lhs.getType().getExtension()).getCompLoc().getTuple()); - mapDescriptorToLocationPath.put(lhs, lhsLocTuple); - } else if (mapDescriptorToLocationPath.get(rhs) != null) { - // propagate rhs's location to lhs - lhsLocTuple.addAll(mapDescriptorToLocationPath.get(rhs)); - mapDescriptorToLocationPath.put(lhs, lhsLocTuple); - } + if (((SSJavaType) rhs.getType().getExtension()).getCompLoc() != null) { + rhsLocTuple.addAll(((SSJavaType) rhs.getType().getExtension()).getCompLoc() + .getTuple()); + } - } + } else { + NTuple locTuple = deriveLocationTuple(md, rhs); + if (locTuple != null) { + rhsLocTuple.addAll(locTuple); + } + } + if (rhsLocTuple.size() > 0) { + mapDescriptorToLocationPath.put(rhs, rhsLocTuple); + } + // lhs side + if (lhs.getType().getExtension() != null + && lhs.getType().getExtension() instanceof SSJavaType) { + lhsLocTuple.addAll(((SSJavaType) lhs.getType().getExtension()).getCompLoc() + .getTuple()); + mapDescriptorToLocationPath.put(lhs, lhsLocTuple); + } else if (mapDescriptorToLocationPath.get(rhs) != null) { + // propagate rhs's location to lhs + lhsLocTuple.addAll(mapDescriptorToLocationPath.get(rhs)); + mapDescriptorToLocationPath.put(lhs, lhsLocTuple); + } + } - if (lhs.getType().isPrimitive() && !lhs.getSymbol().startsWith("neverused") - && !lhs.getSymbol().startsWith("srctmp") && !lhs.getSymbol().startsWith("leftop") - && !lhs.getSymbol().startsWith("rightop")) { + if (isEventLoopBody && lhs.getType().isPrimitive() + && !lhs.getSymbol().startsWith("srctmp")) { + NTuple lhsHeapPath = computePath(lhs); - NTuple lhsHeapPath = computePath(lhs); + if (lhsLocTuple != null) { + addMayWrittenSet(md, lhsLocTuple, lhsHeapPath); + } - if (lhsLocTuple != null) { - addMayWrittenSet(md, lhsLocTuple, lhsHeapPath); + } + } else { + break; } } @@ -742,45 +799,71 @@ public class DefinitelyWrittenCheck { // x.f=y; - Location fieldLocation; if (fn.kind() == FKind.FlatSetFieldNode) { FlatSetFieldNode fsfn = (FlatSetFieldNode) fn; lhs = fsfn.getDst(); fld = fsfn.getField(); rhs = fsfn.getSrc(); - fieldLocation = (Location) fld.getType().getExtension(); } else { FlatSetElementNode fsen = (FlatSetElementNode) fn; lhs = fsen.getDst(); rhs = fsen.getSrc(); TypeDescriptor td = lhs.getType().dereference(); fld = getArrayField(td); + } - NTuple locTuple = mapDescriptorToLocationPath.get(lhs); - fieldLocation = locTuple.get(locTuple.size() - 1); + NTuple lhsLocTuple = new NTuple(); + if (fld.isStatic()) { + if (fld.isFinal()) { + // in this case, fld has TOP location + Location topLocation = Location.createTopLocation(md); + lhsLocTuple.add(topLocation); + } else { + lhsLocTuple.addAll(deriveGlobalLocationTuple(md)); + } + } else { + lhsLocTuple.addAll(deriveLocationTuple(md, lhs)); } - NTuple lTuple = deriveLocationTuple(md, lhs); - if (lTuple != null) { - NTuple lhsLocTuple = new NTuple(); - lhsLocTuple.addAll(lTuple); - mapDescriptorToLocationPath.put(lhs, lhsLocTuple); + mapDescriptorToLocationPath.put(lhs, lhsLocTuple); + + NTuple fieldLocTuple = new NTuple(); + fieldLocTuple.addAll(lhsLocTuple); + + if (fn.kind() == FKind.FlatSetFieldNode) { + fieldLocTuple.add((Location) fld.getType().getExtension()); } - if (ssjava.isSharedLocation(fieldLocation)) { - addSharedLocDescriptor(fieldLocation, fld); + if (mapHeapPath.containsKey(lhs)) { + // fields reachable from the param can have heap path entry. + NTuple lhsHeapPath = new NTuple(); + lhsHeapPath.addAll(mapHeapPath.get(lhs)); + + Location fieldLocation; + if (fn.kind() == FKind.FlatSetFieldNode) { + fieldLocation = getLocation(fld); + } else { + fieldLocation = getLocation(lhsHeapPath.get(getArrayBaseDescriptorIdx(lhsHeapPath))); + } + + // Location fieldLocation = getLocation(lhs); + if (!isEventLoopBody && fieldLocation.getDescriptor().equals(md)) { + // if the field belongs to the local lattice, no reason to calculate + // shared location + break; + } - NTuple locTuple = new NTuple(); - locTuple.addAll(deriveLocationTuple(md, lhs)); - locTuple.add(fieldLocation); + if (ssjava.isSharedLocation(fieldLocation)) { - NTuple fieldHeapPath = new NTuple(); - fieldHeapPath.addAll(computePath(lhs)); - fieldHeapPath.add(fld); + NTuple fieldHeapPath = new NTuple(); + fieldHeapPath.addAll(computePath(lhs)); + if (fn.kind() == FKind.FlatSetFieldNode) { + fieldHeapPath.add(fld); + } - // mapLocationPathToMayWrittenSet.put(locTuple, null, fld); - addMayWrittenSet(md, locTuple, fieldHeapPath); + addMayWrittenSet(md, fieldLocTuple, fieldHeapPath); + } } } @@ -804,14 +887,27 @@ public class DefinitelyWrittenCheck { fld = getArrayField(td); } - if (fld.isFinal()) { - // if field is final no need to check - break; - } - NTuple locTuple = new NTuple(); - locTuple.addAll(deriveLocationTuple(md, rhs)); - locTuple.add((Location) fld.getType().getExtension()); + + if (fld.isStatic()) { + + if (fld.isFinal()) { + // in this case, fld has TOP location + Location topLocation = Location.createTopLocation(md); + locTuple.add(topLocation); + } else { + locTuple.addAll(deriveGlobalLocationTuple(md)); + if (fn.kind() == FKind.FlatFieldNode) { + locTuple.add((Location) fld.getType().getExtension()); + } + } + + } else { + locTuple.addAll(deriveLocationTuple(md, rhs)); + if (fn.kind() == FKind.FlatFieldNode) { + locTuple.add((Location) fld.getType().getExtension()); + } + } mapDescriptorToLocationPath.put(lhs, locTuple); @@ -822,9 +918,7 @@ public class DefinitelyWrittenCheck { FlatCall fc = (FlatCall) fn; - if (ssjava.needTobeAnnotated(fc.getMethod())) { - bindLocationPathCallerArgWithCalleeParam(md, fc); - } + bindLocationPathCallerArgWithCalleeParam(md, fc); } break; @@ -873,7 +967,7 @@ public class DefinitelyWrittenCheck { NTuple argLocationPath = deriveLocationTuple(mdCaller, arg); NTuple argHeapPath = computePath(arg); addMayWrittenSet(mdCaller, argLocationPath, argHeapPath); - } else { + } else if (ssjava.needTobeAnnotated(fc.getMethod())) { // if arg is not primitive type, we need to propagate maywritten set to // the caller's location path @@ -890,52 +984,46 @@ public class DefinitelyWrittenCheck { Hashtable> mapArgIdx2CallerArgLocationPath = new Hashtable>(); - // arg idx is starting from 'this' arg if (fc.getThis() != null) { - // loc path for 'this' - NTuple thisLocationPath = deriveLocationTuple(mdCaller, fc.getThis()); - if (thisLocationPath != null) { - mapArgIdx2CallerArgLocationPath.put(Integer.valueOf(0), thisLocationPath); - // heap path for 'this' - 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()); - } + if (mapHeapPath.containsKey(fc.getThis())) { + + // setup heap path for 'this' + NTuple thisHeapPath = new NTuple(); + thisHeapPath.addAll(mapHeapPath.get(fc.getThis())); mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath); - } + // setup location path for 'this' + NTuple thisLocationPath = deriveLocationTuple(mdCaller, fc.getThis()); + mapArgIdx2CallerArgLocationPath.put(Integer.valueOf(0), thisLocationPath); + + } } for (int i = 0; i < fc.numArgs(); i++) { TempDescriptor arg = fc.getArg(i); // create mapping arg to loc path - NTuple argLocationPath = deriveLocationTuple(mdCaller, arg); - if (argLocationPath != null) { - mapArgIdx2CallerArgLocationPath.put(Integer.valueOf(i + 1), argLocationPath); - // create mapping arg to heap path - NTuple argHeapPath = computePath(arg); + + if (mapHeapPath.containsKey(arg)) { + // setup heap path + NTuple argHeapPath = mapHeapPath.get(arg); mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(i + 1), argHeapPath); + // setup loc path + NTuple argLocationPath = deriveLocationTuple(mdCaller, arg); + mapArgIdx2CallerArgLocationPath.put(Integer.valueOf(i + 1), argLocationPath); } } - Hashtable>> mapParamIdx2WriteSet = - new Hashtable>>(); - - for (int i = 0; i < fc.numArgs() + 1; i++) { - mapParamIdx2WriteSet.put(Integer.valueOf(i), new HashSet>()); - } - 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 + Hashtable, NTuple> mapParamHeapPathToCallerArgHeapPath = + new Hashtable, NTuple>(); + Hashtable mapParamIdx2ParamTempDesc = new Hashtable(); int offset = 0; @@ -943,26 +1031,40 @@ public class DefinitelyWrittenCheck { // 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); + + NTuple calleeHeapPath = computePath(param); + + NTuple argHeapPath = + mapArgIdx2CallerArgHeapPath.get(Integer.valueOf(i + offset)); + + if (argHeapPath != null) { + mapParamHeapPathToCallerArgHeapPath.put(calleeHeapPath, argHeapPath); + + } + } Set keySet = mapArgIdx2CallerArgLocationPath.keySet(); for (Iterator iterator2 = keySet.iterator(); iterator2.hasNext();) { Integer idx = (Integer) iterator2.next(); + NTuple callerArgLocationPath = mapArgIdx2CallerArgLocationPath.get(idx); TempDescriptor calleeParam = mapParamIdx2ParamTempDesc.get(idx); + NTuple calleeLocationPath = deriveLocationTuple(mdCallee, calleeParam); NTuple callerArgHeapPath = mapArgIdx2CallerArgHeapPath.get(idx); - NTuple calleeLocationPath = deriveLocationTuple(mdCallee, calleeParam); NTuple calleeHeapPath = computePath(calleeParam); - createNewMappingOfMayWrittenSet(mdCaller, callee, callerArgHeapPath, - callerArgLocationPath, calleeHeapPath, calleeLocationPath, - mapParamIdx2WriteSet.get(idx)); - + if (!calleeParam.getType().isPrimitive()) { + createNewMappingOfMayWrittenSet(mdCaller, callee, callerArgHeapPath, + callerArgLocationPath, calleeHeapPath, calleeLocationPath, + mapParamHeapPathToCallerArgHeapPath); + } } } @@ -993,7 +1095,7 @@ public class DefinitelyWrittenCheck { private void createNewMappingOfMayWrittenSet(MethodDescriptor caller, MethodDescriptor callee, NTuple callerArgHeapPath, NTuple callerArgLocPath, NTuple calleeParamHeapPath, NTuple calleeParamLocPath, - Set> writeSet) { + Hashtable, NTuple> mapParamHeapPathToCallerArgHeapPath) { // propagate may-written-set associated with the key that is started with // calleepath to the caller @@ -1005,6 +1107,10 @@ public class DefinitelyWrittenCheck { MultiSourceMap, NTuple> calleeMapping = mapMethodToSharedLocCoverSet.get(callee); + if (calleeMapping == null) { + return; + } + MultiSourceMap, NTuple> callerMapping = mapMethodToSharedLocCoverSet.get(caller); @@ -1013,24 +1119,25 @@ public class DefinitelyWrittenCheck { mapMethodToSharedLocCoverSet.put(caller, callerMapping); } - if (calleeMapping == null) { - return; - } - Hashtable, Set>> paramMapping = getMappingByStartedWith(calleeMapping, calleeParamLocPath); - Set> calleeKeySet = calleeMapping.keySet(); + Set> calleeKeySet = paramMapping.keySet(); + for (Iterator iterator = calleeKeySet.iterator(); iterator.hasNext();) { NTuple calleeKey = (NTuple) iterator.next(); + Set> calleeMayWriteSet = paramMapping.get(calleeKey); if (calleeMayWriteSet != null) { - Set> boundWriteSet = - convertCallerMayWriteSet(callerArgHeapPath, calleeParamHeapPath, calleeMayWriteSet); + Set> boundMayWriteSet = new HashSet>(); + + Set> boundSet = + convertToCallerMayWriteSet(calleeParamHeapPath, calleeMayWriteSet, callerMapping, + mapParamHeapPathToCallerArgHeapPath); - writeSet.addAll(boundWriteSet); + boundMayWriteSet.addAll(boundSet); NTuple newKey = new NTuple(); newKey.addAll(callerArgLocPath); @@ -1040,16 +1147,17 @@ public class DefinitelyWrittenCheck { newKey.add(calleeKey.get(i)); } - callerMapping.union(newKey, writeSet); - // mapLocationPathToMayWrittenSet.put(calleeKey, newKey, writeSet); + callerMapping.union(newKey, boundMayWriteSet); } } } - private Set> convertCallerMayWriteSet(NTuple callerArgHeapPath, - NTuple calleeParamHeapPath, Set> calleeMayWriteSet) { + private Set> convertToCallerMayWriteSet( + NTuple calleeParamHeapPath, Set> calleeMayWriteSet, + MultiSourceMap, NTuple> callerMapping, + Hashtable, NTuple> mapParamHeapPathToCallerArgHeapPath) { Set> boundSet = new HashSet>(); @@ -1057,12 +1165,15 @@ public class DefinitelyWrittenCheck { for (Iterator iterator = calleeMayWriteSet.iterator(); iterator.hasNext();) { NTuple calleeWriteHeapPath = (NTuple) iterator.next(); + NTuple writeHeapPathParamHeapPath = calleeWriteHeapPath.subList(0, 1); + + NTuple callerArgHeapPath = + mapParamHeapPathToCallerArgHeapPath.get(writeHeapPathParamHeapPath); + NTuple boundHeapPath = new NTuple(); boundHeapPath.addAll(callerArgHeapPath); - int startIdx = calleeParamHeapPath.size(); - - for (int i = startIdx; i < calleeWriteHeapPath.size(); i++) { + for (int i = 1; i < calleeWriteHeapPath.size(); i++) { boundHeapPath.add(calleeWriteHeapPath.get(i)); } @@ -1073,18 +1184,6 @@ public class DefinitelyWrittenCheck { return boundSet; } - private void addSharedLocDescriptor(Location sharedLoc, Descriptor desc) { - - Set descSet = mapSharedLocationToCoverSet.get(sharedLoc); - if (descSet == null) { - descSet = new HashSet(); - mapSharedLocationToCoverSet.put(sharedLoc, descSet); - } - - descSet.add(desc); - - } - private Location getLocation(Descriptor d) { if (d instanceof FieldDescriptor) { @@ -1217,16 +1316,33 @@ public class DefinitelyWrittenCheck { if (fon.getOp().getOp() == Operation.ASSIGN) { - if (!lhs.getSymbol().startsWith("neverused")) { - NTuple rhsHeapPath = computePath(rhs); - if (!rhs.getType().isImmutable()) { - mapHeapPath.put(lhs, rhsHeapPath); - } else { - // write(lhs) - // NTuple lhsHeapPath = computePath(lhs); - NTuple path = new NTuple(); - path.add(lhs); + if (!lhs.getSymbol().startsWith("neverused") && !lhs.getSymbol().startsWith("leftop") + && !lhs.getSymbol().startsWith("rightop")) { + + boolean hasWriteEffect = false; + if (rhs.getType().getExtension() instanceof SSJavaType + && lhs.getType().getExtension() instanceof SSJavaType) { + + CompositeLocation rhsCompLoc = + ((SSJavaType) rhs.getType().getExtension()).getCompLoc(); + + CompositeLocation lhsCompLoc = + ((SSJavaType) lhs.getType().getExtension()).getCompLoc(); + + if (lhsCompLoc != rhsCompLoc) { + // have a write effect! + hasWriteEffect = true; + } + + } else if (lhs.getType().isImmutable()) { + hasWriteEffect = true; + } + + if (hasWriteEffect && mapHeapPath.containsKey(lhs)) { + // write(lhs) + NTuple lhsHeapPath = new NTuple(); + lhsHeapPath.addAll(mapHeapPath.get(lhs)); Location lhsLoc = getLocation(lhs); if (ssjava.isSharedLocation(lhsLoc)) { @@ -1237,7 +1353,10 @@ public class DefinitelyWrittenCheck { Set> writtenSet = mapFlatNodeToSharedLocMapping.get(fn).get(varLocTuple); - if (isCovered(varLocTuple, writtenSet)) { + Set> mustClearSet = + mapFlatNodeToMustClearMap.get(fn).get(varLocTuple); + + if (isCovered(varLocTuple, writtenSet, mustClearSet)) { computeKILLSetForSharedWrite(curr, writtenSet, readWriteKillSet); computeGENSetForSharedAllCoverWrite(curr, writtenSet, readWriteGenSet); } else { @@ -1246,16 +1365,12 @@ public class DefinitelyWrittenCheck { } else { - computeKILLSetForWrite(curr, path, readWriteKillSet); - computeGENSetForWrite(path, readWriteGenSet); + computeKILLSetForWrite(curr, lhsHeapPath, readWriteKillSet); + computeGENSetForWrite(lhsHeapPath, readWriteGenSet); } - // System.out.println("#KILLSET=" + readWriteKillSet); - // System.out.println("#GENSet=" + readWriteGenSet); - - Set writeAgeSet = curr.get(path); - checkWriteAgeSet(writeAgeSet, path, fn); - + Set writeAgeSet = curr.get(lhsHeapPath); + checkWriteAgeSet(writeAgeSet, lhsHeapPath, fn); } } @@ -1315,61 +1430,67 @@ public class DefinitelyWrittenCheck { fld = getArrayField(td); } - // System.out.println("FIELD WRITE:" + fn); + // set up heap path + NTuple lhsHeapPath = mapHeapPath.get(lhs); + if (lhsHeapPath != null) { + // write(field) + NTuple fldHeapPath = new NTuple(lhsHeapPath.getList()); + if (fn.kind() == FKind.FlatSetFieldNode) { + fldHeapPath.add(fld); + } - // write(field) - NTuple lhsHeapPath = computePath(lhs); - NTuple fldHeapPath = new NTuple(lhsHeapPath.getList()); - fldHeapPath.add(fld); + // shared loc extension + Location fieldLoc; + if (fn.kind() == FKind.FlatSetFieldNode) { + fieldLoc = (Location) fld.getType().getExtension(); + } else { + NTuple locTuple = mapDescriptorToLocationPath.get(lhs); + fieldLoc = locTuple.get(locTuple.size() - 1); + } - // shared loc extension - Location fieldLoc = (Location) fld.getType().getExtension(); - if (ssjava.isSharedLocation(fieldLoc)) { + if (ssjava.isSharedLocation(fieldLoc)) { - NTuple fieldLocTuple = new NTuple(); - fieldLocTuple.addAll(mapDescriptorToLocationPath.get(lhs)); - fieldLocTuple.add(fieldLoc); + NTuple fieldLocTuple = new NTuple(); + fieldLocTuple.addAll(mapDescriptorToLocationPath.get(lhs)); + if (fn.kind() == FKind.FlatSetFieldNode) { + fieldLocTuple.add(fieldLoc); + } - Set> writtenSet = - mapFlatNodeToSharedLocMapping.get(fn).get(fieldLocTuple); + Set> writtenSet = + mapFlatNodeToSharedLocMapping.get(fn).get(fieldLocTuple); + if (isCovered(fieldLocTuple, writtenSet)) { + computeKILLSetForSharedWrite(curr, writtenSet, readWriteKillSet); + computeGENSetForSharedAllCoverWrite(curr, writtenSet, readWriteGenSet); + } else { + computeGENSetForSharedNonCoverWrite(curr, fldHeapPath, readWriteGenSet); + } - if (isCovered(fieldLocTuple, writtenSet)) { - computeKILLSetForSharedWrite(curr, writtenSet, readWriteKillSet); - computeGENSetForSharedAllCoverWrite(curr, writtenSet, readWriteGenSet); } else { - computeGENSetForSharedNonCoverWrite(curr, fldHeapPath, readWriteGenSet); + computeKILLSetForWrite(curr, fldHeapPath, readWriteKillSet); + computeGENSetForWrite(fldHeapPath, readWriteGenSet); } - } else { - computeKILLSetForWrite(curr, fldHeapPath, readWriteKillSet); - computeGENSetForWrite(fldHeapPath, readWriteGenSet); } - // System.out.println("KILLSET=" + readWriteKillSet); - // System.out.println("GENSet=" + readWriteGenSet); - } break; case FKind.FlatCall: { FlatCall fc = (FlatCall) fn; - SharedLocMap sharedLocMap = mapFlatNodeToSharedLocMapping.get(fc); - // System.out.println("FLATCALL:" + fn); - generateKILLSetForFlatCall(fc, curr, sharedLocMap, readWriteKillSet); - generateGENSetForFlatCall(fc, sharedLocMap, readWriteGenSet); - - // System.out.println("KILLSET=" + readWriteKillSet); - // System.out.println("GENSet=" + readWriteGenSet); + SharedLocMap mustClearMap = mapFlatNodeToMustClearMap.get(fc); + generateKILLSetForFlatCall(fc, curr, sharedLocMap, mustClearMap, readWriteKillSet); + generateGENSetForFlatCall(fc, sharedLocMap, mustClearMap, readWriteGenSet); - checkManyRead(fc, curr); } break; } computeNewMapping(curr, readWriteKillSet, readWriteGenSet); - // System.out.println("#######" + curr); + if (fn instanceof FlatCall) { + checkManyRead((FlatCall) fn, curr); + } } @@ -1417,22 +1538,37 @@ public class DefinitelyWrittenCheck { } - private boolean isCovered(NTuple locTuple, Set> inSet) { + private boolean isCovered(NTuple locTuple, Set> curWrittenSet) { - if (inSet == null) { + Set> coverSet = + mapMethodToSharedLocCoverSet.get(methodContainingSSJavaLoop).get(locTuple); + + if (curWrittenSet == null) { return false; } + return curWrittenSet.containsAll(coverSet); + } + + private boolean isCovered(NTuple locTuple, Set> curWrittenSet, + Set> mustClearSet) { + Set> coverSet = mapMethodToSharedLocCoverSet.get(methodContainingSSJavaLoop).get(locTuple); - return inSet.containsAll(coverSet); + if (mustClearSet != null && mustClearSet.containsAll(coverSet)) { + return true; + } + + if (curWrittenSet == null) { + return false; + } + + return curWrittenSet.containsAll(coverSet); } 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); @@ -1443,26 +1579,42 @@ public class DefinitelyWrittenCheck { private void checkWriteAgeSet(Set writeAgeSet, NTuple path, FlatNode fn) { - // System.out.println("# CHECK WRITE AGE of " + path + " from set=" + - // writeAgeSet); - if (writeAgeSet != null) { for (Iterator iterator = writeAgeSet.iterator(); iterator.hasNext();) { WriteAge writeAge = (WriteAge) iterator.next(); if (writeAge.getAge() > MAXAGE) { - throw new Error( - "Memory location, which is reachable through references " - + path - + ", who comes back to the same read statement without being overwritten at the out-most iteration at " - + methodContainingSSJavaLoop.getClassDesc().getSourceFileName() + "::" - + fn.getNumLine()); + generateErrorMessage(path, fn); } } } } + private void generateErrorMessage(NTuple path, FlatNode fn) { + + Descriptor lastDesc = path.get(getArrayBaseDescriptorIdx(path)); + if (ssjava.isSharedLocation(getLocation(lastDesc))) { + + NTuple locPathTuple = getLocationTuple(path); + Set> coverSet = + mapMethodToSharedLocCoverSet.get(methodContainingSSJavaLoop).get(locPathTuple); + throw new Error("Shared memory locations, which is reachable through references " + path + + ", are not completely overwritten by the higher values at " + + methodContainingSSJavaLoop.getClassDesc().getSourceFileName() + "::" + fn.getNumLine() + + ".\nThe following memory locations belong to the same shared locations:" + coverSet); + + } else { + throw new Error( + "Memory location, which is reachable through references " + + path + + ", who comes back to the same read statement without being overwritten at the out-most iteration at " + + methodContainingSSJavaLoop.getClassDesc().getSourceFileName() + "::" + + fn.getNumLine()); + } + + } + private void generateGENSetForFlatCall(FlatCall fc, SharedLocMap sharedLocMap, - Hashtable, Set> GENSet) { + SharedLocMap mustClearMap, Hashtable, Set> GENSet) { Set> boundMayWriteSet = mapFlatNodeToBoundMayWriteSet.get(fc); @@ -1474,14 +1626,13 @@ public class DefinitelyWrittenCheck { } else { // if the current heap path is shared location - NTuple locTuple = getLocationTuple(heapPath, sharedLocMap); + NTuple locTuple = getLocationTuple(heapPath); Set> sharedWriteHeapPathSet = sharedLocMap.get(locTuple); - if (isCovered(locTuple, sharedLocMap.get(locTuple))) { + if (isCovered(locTuple, sharedLocMap.get(locTuple), mustClearMap.get(locTuple))) { // if it is covered, add all of heap paths belong to the same shared // loc with write age 0 - for (Iterator iterator2 = sharedWriteHeapPathSet.iterator(); iterator2.hasNext();) { NTuple sharedHeapPath = (NTuple) iterator2.next(); addWriteAgeToSet(sharedHeapPath, GENSet, new WriteAge(0)); @@ -1513,7 +1664,7 @@ public class DefinitelyWrittenCheck { private void generateKILLSetForFlatCall(FlatCall fc, Hashtable, Set> curr, SharedLocMap sharedLocMap, - Hashtable, Set> KILLSet) { + SharedLocMap mustClearMap, Hashtable, Set> KILLSet) { Set> boundMustWriteSet = mapFlatNodeToBoundMustWriteSet.get(fc); @@ -1521,32 +1672,55 @@ public class DefinitelyWrittenCheck { NTuple heapPath = (NTuple) iterator.next(); if (isSharedLocation(heapPath)) { - NTuple locTuple = getLocationTuple(heapPath, sharedLocMap); + NTuple locTuple = getLocationTuple(heapPath); - if (isCovered(locTuple, sharedLocMap.get(locTuple))) { + if (isCovered(locTuple, sharedLocMap.get(locTuple), mustClearMap.get(locTuple)) + && curr.containsKey(heapPath)) { // if it is shared loc and corresponding shared loc has been covered KILLSet.put(heapPath, curr.get(heapPath)); } } else { - if (curr.get(heapPath) != null) { - KILLSet.put(heapPath, curr.get(heapPath)); + + for (Enumeration> e = curr.keys(); e.hasMoreElements();) { + NTuple key = e.nextElement(); + if (key.startsWith(heapPath)) { + KILLSet.put(key, curr.get(key)); + } } + } } } + private int getArrayBaseDescriptorIdx(NTuple heapPath) { + + for (int i = heapPath.size() - 1; i >= 0; i--) { + if (!heapPath.get(i).getSymbol().equals(arrayElementFieldName)) { + return i; + } + } + + return -1; + + } + private boolean isSharedLocation(NTuple heapPath) { - return ssjava.isSharedLocation(getLocation(heapPath.get(heapPath.size() - 1))); + + Descriptor d = heapPath.get(getArrayBaseDescriptorIdx(heapPath)); + + return ssjava.isSharedLocation(getLocation(heapPath.get(getArrayBaseDescriptorIdx(heapPath)))); + } - private NTuple getLocationTuple(NTuple heapPath, SharedLocMap sharedLocMap) { + private NTuple getLocationTuple(NTuple heapPath) { NTuple locTuple = new NTuple(); locTuple.addAll(mapDescriptorToLocationPath.get(heapPath.get(0))); - for (int i = 1; i < heapPath.size(); i++) { + + for (int i = 1; i <= getArrayBaseDescriptorIdx(heapPath); i++) { locTuple.add(getLocation(heapPath.get(i))); } @@ -1635,13 +1809,10 @@ public class DefinitelyWrittenCheck { // 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()); + if (thisHeapPath != null) { + // if 'this' does not have heap path, it is local reference + mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath); } - - mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath); } for (int i = 0; i < fc.numArgs(); i++) { @@ -1718,94 +1889,142 @@ public class DefinitelyWrittenCheck { calleeIntersectBoundSharedSet.clear(); calleeUnionBoundDeleteSet.clear(); - // if arg is not primitive type, we need to propagate maywritten set to - // the caller's location path + if (ssjava.isSSJavaUtil(fc.getMethod().getClassDesc())) { + // ssjava util case! + // have write effects on the first argument + TempDescriptor arg = fc.getArg(0); + NTuple argHeapPath = computePath(arg); - MethodDescriptor mdCallee = fc.getMethod(); - Set setPossibleCallees = new HashSet(); - setPossibleCallees.addAll(callGraph.getMethods(mdCallee)); + // convert heap path to location path + NTuple argLocTuple = new NTuple(); + argLocTuple.addAll(deriveLocationTuple(mdCaller, (TempDescriptor) argHeapPath.get(0))); + for (int i = 1; i < argHeapPath.size(); i++) { + argLocTuple.add(getLocation(argHeapPath.get(i))); + } - // create mapping from arg idx to its heap paths - Hashtable> mapArgIdx2CallerArgHeapPath = - new Hashtable>(); + calleeIntersectBoundSharedSet.addWrite(argLocTuple, argHeapPath); - // 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()); - } + } else if (ssjava.needTobeAnnotated(fc.getMethod())) { - mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath); - } + // if arg is not primitive type, we need to propagate maywritten set to + // the caller's location path - for (int i = 0; i < fc.numArgs(); i++) { - TempDescriptor arg = fc.getArg(i); - NTuple argHeapPath = computePath(arg); - mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(i + 1), argHeapPath); - } + MethodDescriptor mdCallee = fc.getMethod(); + Set setPossibleCallees = new HashSet(); + setPossibleCallees.addAll(callGraph.getMethods(mdCallee)); - // create mapping from arg idx to its location paths - Hashtable> mapArgIdx2CallerAgLocationPath = - new Hashtable>(); + // 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 thisLocationPath = deriveLocationTuple(mdCaller, fc.getThis()); - mapArgIdx2CallerAgLocationPath.put(Integer.valueOf(0), thisLocationPath); - } + // 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()); + } - for (int i = 0; i < fc.numArgs(); i++) { - TempDescriptor arg = fc.getArg(i); - NTuple argLocationPath = deriveLocationTuple(mdCaller, arg); - if (argLocationPath != null) { - mapArgIdx2CallerAgLocationPath.put(Integer.valueOf(i + 1), argLocationPath); + mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath); } - } - for (Iterator iterator = setPossibleCallees.iterator(); iterator.hasNext();) { - MethodDescriptor callee = (MethodDescriptor) iterator.next(); - FlatMethod calleeFlatMethod = state.getMethodFlat(callee); + for (int i = 0; i < fc.numArgs(); i++) { + TempDescriptor arg = fc.getArg(i); + NTuple argHeapPath = computePath(arg); + mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(i + 1), argHeapPath); + } - // binding caller's args and callee's params + // create mapping from arg idx to its location paths + Hashtable> mapArgIdx2CallerAgLocationPath = + new Hashtable>(); - Hashtable mapParamIdx2ParamTempDesc = - new Hashtable(); - int offset = 0; - if (calleeFlatMethod.getMethod().isStatic()) { - // static method does not have implicit 'this' arg - offset = 1; + // arg idx is starting from 'this' arg + if (fc.getThis() != null) { + NTuple thisLocationPath = deriveLocationTuple(fc.getMethod(), fc.getThis()); + if (thisLocationPath != null) { + mapArgIdx2CallerAgLocationPath.put(Integer.valueOf(0), thisLocationPath); + } } - for (int i = 0; i < calleeFlatMethod.numParameters(); i++) { - TempDescriptor param = calleeFlatMethod.getParameter(i); - mapParamIdx2ParamTempDesc.put(Integer.valueOf(i + offset), param); + + for (int i = 0; i < fc.numArgs(); i++) { + TempDescriptor arg = fc.getArg(i); + NTuple argLocationPath = deriveLocationTuple(mdCaller, arg); + if (argLocationPath != null) { + mapArgIdx2CallerAgLocationPath.put(Integer.valueOf(i + 1), argLocationPath); + } } - Set keySet = mapArgIdx2CallerAgLocationPath.keySet(); - for (Iterator iterator2 = keySet.iterator(); iterator2.hasNext();) { - Integer idx = (Integer) iterator2.next(); - NTuple callerArgLocationPath = mapArgIdx2CallerAgLocationPath.get(idx); - NTuple callerArgHeapPath = mapArgIdx2CallerArgHeapPath.get(idx); + for (Iterator iterator = setPossibleCallees.iterator(); iterator.hasNext();) { + MethodDescriptor callee = (MethodDescriptor) iterator.next(); + FlatMethod calleeFlatMethod = state.getMethodFlat(callee); - TempDescriptor calleeParam = mapParamIdx2ParamTempDesc.get(idx); - NTuple calleeLocationPath = deriveLocationTuple(mdCallee, calleeParam); - SharedLocMap calleeDeleteSet = mapFlatMethodToDeleteSet.get(calleeFlatMethod); - SharedLocMap calleeSharedLocMap = mapFlatMethodToSharedLocMap.get(calleeFlatMethod); + // binding caller's args and callee's params - if (calleeDeleteSet != null) { - createNewMappingOfDeleteSet(callerArgLocationPath, callerArgHeapPath, calleeLocationPath, - calleeDeleteSet); + 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); } - if (calleeSharedLocMap != null) { - createNewMappingOfSharedSet(callerArgLocationPath, callerArgHeapPath, calleeLocationPath, - calleeSharedLocMap); + Set keySet = mapArgIdx2CallerAgLocationPath.keySet(); + for (Iterator iterator2 = keySet.iterator(); iterator2.hasNext();) { + Integer idx = (Integer) iterator2.next(); + NTuple callerArgLocationPath = mapArgIdx2CallerAgLocationPath.get(idx); + NTuple callerArgHeapPath = mapArgIdx2CallerArgHeapPath.get(idx); + + TempDescriptor calleeParam = mapParamIdx2ParamTempDesc.get(idx); + NTuple calleeLocationPath = deriveLocationTuple(mdCallee, calleeParam); + SharedLocMap calleeDeleteSet = mapFlatMethodToDeleteSet.get(calleeFlatMethod); + SharedLocMap calleeSharedLocMap = mapFlatMethodToSharedLocMap.get(calleeFlatMethod); + SharedLocMap calleeMustClearMap = mapFlatMethodToMustClearMap.get(calleeFlatMethod); + + if (calleeDeleteSet != null) { + createNewMappingOfDeleteSet(callerArgLocationPath, callerArgHeapPath, + calleeLocationPath, calleeDeleteSet); + } + + if (calleeSharedLocMap != null) { + createNewMappingOfSharedSet(callerArgLocationPath, callerArgHeapPath, + calleeLocationPath, calleeSharedLocMap); + } + + if (calleeMustClearMap != null) { + createNewMappingOfMustClearMap(callerArgLocationPath, callerArgHeapPath, + calleeLocationPath, calleeMustClearMap); + } + } } + } + + } + + private void createNewMappingOfMustClearMap(NTuple callerArgLocationPath, + NTuple callerArgHeapPath, NTuple calleeLocationPath, + SharedLocMap calleeMustClearMap) { + SharedLocMap calleeParamSharedSet = + calleeMustClearMap.getHeapPathStartedWith(calleeLocationPath); + + Set> keySet = calleeParamSharedSet.keySet(); + for (Iterator iterator = keySet.iterator(); iterator.hasNext();) { + NTuple calleeLocTupleKey = (NTuple) iterator.next(); + Set> heapPathSet = calleeParamSharedSet.get(calleeLocTupleKey); + Set> boundHeapPathSet = new HashSet>(); + for (Iterator iterator2 = heapPathSet.iterator(); iterator2.hasNext();) { + NTuple calleeHeapPath = (NTuple) iterator2.next(); + boundHeapPathSet.add(bindHeapPath(callerArgHeapPath, calleeHeapPath)); + } + calleeIntersectBoundMustClearSet.intersect( + bindLocationPath(callerArgLocationPath, calleeLocTupleKey), boundHeapPathSet); } } @@ -1918,15 +2137,19 @@ public class DefinitelyWrittenCheck { // perform topological sort over the set of methods accessed by the main // event loop - Set methodDescriptorsToAnalyze = new HashSet(); - methodDescriptorsToAnalyze.addAll(ssjava.getAnnotationRequireSet()); - sortedDescriptors = topologicalSort(methodDescriptorsToAnalyze); + // Set methodDescriptorsToAnalyze = new + // HashSet(); + // methodDescriptorsToAnalyze.addAll(ssjava.getAnnotationRequireSet()); + // sortedDescriptors = topologicalSort(methodDescriptorsToAnalyze); + + liveInTempSetToEventLoop = + liveness.getLiveInTemps(state.getMethodFlat(methodContainingSSJavaLoop), + ssjava.getSSJavaLoopEntrance()); } private void methodReadWriteSetAnalysis() { // perform method READ/OVERWRITE analysis - LinkedList descriptorListToAnalyze = - (LinkedList) sortedDescriptors.clone(); + LinkedList descriptorListToAnalyze = ssjava.getSortedDescriptors(); // current descriptors to visit in fixed-point interprocedural analysis, // prioritized by @@ -1968,7 +2191,7 @@ public class DefinitelyWrittenCheck { // results for callee changed, so enqueue dependents caller for // further // analysis - Iterator depsItr = getDependents(md).iterator(); + Iterator depsItr = ssjava.getDependents(md).iterator(); while (depsItr.hasNext()) { MethodDescriptor methodNext = depsItr.next(); if (!methodDescriptorsToVisitStack.contains(methodNext) @@ -2015,6 +2238,13 @@ public class DefinitelyWrittenCheck { mapFlatMethodToMustWriteSet.put(flatMethodContainingSSJavaLoop, mustWriteSet); mapFlatMethodToMayWriteSet.put(flatMethodContainingSSJavaLoop, mayWriteSet); + for (Iterator iterator = liveInTempSetToEventLoop.iterator(); iterator.hasNext();) { + TempDescriptor liveIn = (TempDescriptor) iterator.next(); + NTuple heapPath = new NTuple(); + heapPath.add(liveIn); + mapHeapPath.put(liveIn, heapPath); + } + methodReadWriteSet_analyzeBody(ssjava.getSSJavaLoopEntrance(), readSet, mustWriteSet, mayWriteSet, true); @@ -2096,16 +2326,23 @@ public class DefinitelyWrittenCheck { NTuple rhsHeapPath = mapHeapPath.get(rhs); - if (lhs.getType().isPrimitive()) { - NTuple lhsHeapPath = new NTuple(); - lhsHeapPath.add(lhs); - mapHeapPath.put(lhs, lhsHeapPath); - } else if (rhsHeapPath != null) { + // if (lhs.getType().isPrimitive()) { + // NTuple lhsHeapPath = new NTuple(); + // lhsHeapPath.add(lhs); + // mapHeapPath.put(lhs, lhsHeapPath); + // } else + + if (rhsHeapPath != null && (!lhs.getType().isPrimitive())) { mapHeapPath.put(lhs, mapHeapPath.get(rhs)); } else { - NTuple heapPath = new NTuple(); - heapPath.add(rhs); - mapHeapPath.put(lhs, heapPath); + break; + // if (isEventLoopBody) { + // NTuple lhsHeapPath = new NTuple(); + // lhsHeapPath.add(rhs); + // mapHeapPath.put(lhs, lhsHeapPath); + // } else { + // break; + // } } // shared loc extension @@ -2129,7 +2366,6 @@ public class DefinitelyWrittenCheck { writeHeapPath.addAll(heapPath); writeHeapPath.add(lhs); - } } } @@ -2168,7 +2404,10 @@ public class DefinitelyWrittenCheck { // callee's parameters. so just ignore it NTuple readingHeapPath = new NTuple(srcHeapPath.getList()); - readingHeapPath.add(fld); + if (fn.kind() == FKind.FlatFieldNode) { + readingHeapPath.add(fld); + } + mapHeapPath.put(lhs, readingHeapPath); // read (x.f) @@ -2210,12 +2449,16 @@ public class DefinitelyWrittenCheck { // if lhs heap path is null, it means that it is not reachable from // callee's parameters. so just ignore it NTuple fldHeapPath = new NTuple(lhsHeapPath.getList()); - fldHeapPath.add(fld); - mapHeapPath.put(fld, fldHeapPath); + if (fn.kind() != FKind.FlatSetElementNode) { + fldHeapPath.add(fld); + } + // mapHeapPath.put(fld, fldHeapPath); // write(x.f) // need to add hp(y) to WT - currMustWriteSet.add(fldHeapPath); + if (fn.kind() != FKind.FlatSetElementNode) { + currMustWriteSet.add(fldHeapPath); + } mayWriteSet.add(fldHeapPath); } @@ -2347,87 +2590,17 @@ public class DefinitelyWrittenCheck { } - // Borrowed it from disjoint analysis - private LinkedList topologicalSort(Set toSort) { - - Set discovered = new HashSet(); - - LinkedList sorted = new LinkedList(); - - Iterator itr = toSort.iterator(); - while (itr.hasNext()) { - MethodDescriptor d = itr.next(); - - if (!discovered.contains(d)) { - dfsVisit(d, toSort, sorted, discovered); - } - } - - return sorted; - } - - // While we're doing DFS on call graph, remember - // dependencies for efficient queuing of methods - // during interprocedural analysis: - // - // a dependent of a method decriptor d for this analysis is: - // 1) a method or task that invokes d - // 2) in the descriptorsToAnalyze set - private void dfsVisit(MethodDescriptor md, Set toSort, - LinkedList sorted, Set discovered) { - - discovered.add(md); - - Iterator itr = callGraph.getCallerSet(md).iterator(); - while (itr.hasNext()) { - MethodDescriptor dCaller = (MethodDescriptor) itr.next(); - // only consider callers in the original set to analyze - if (!toSort.contains(dCaller)) { - continue; - } - if (!discovered.contains(dCaller)) { - addDependent(md, // callee - dCaller // caller - ); - - dfsVisit(dCaller, toSort, sorted, discovered); - } - } - - // for leaf-nodes last now! - sorted.addLast(md); - } - - // a dependent of a method decriptor d for this analysis is: - // 1) a method or task that invokes d - // 2) in the descriptorsToAnalyze set - private void addDependent(MethodDescriptor callee, MethodDescriptor caller) { - Set deps = mapDescriptorToSetDependents.get(callee); - if (deps == null) { - deps = new HashSet(); - } - deps.add(caller); - mapDescriptorToSetDependents.put(callee, deps); - } - - private Set getDependents(MethodDescriptor callee) { - Set deps = mapDescriptorToSetDependents.get(callee); - if (deps == null) { - deps = new HashSet(); - mapDescriptorToSetDependents.put(callee, deps); - } - return deps; - } - 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)) { - return mapHeapPath.get(td); + NTuple rtrHeapPath = new NTuple(); + rtrHeapPath.addAll(mapHeapPath.get(td)); + return rtrHeapPath; } else { - NTuple path = new NTuple(); - path.add(td); - return path; + NTuple rtrHeapPath = new NTuple(); + rtrHeapPath.add(td); + return rtrHeapPath; } } @@ -2439,23 +2612,36 @@ public class DefinitelyWrittenCheck { return locTuple; } - private NTuple deriveLocationTuple(MethodDescriptor md, TempDescriptor td) { + private NTuple deriveGlobalLocationTuple(MethodDescriptor md) { + String globalLocIdentifier = ssjava.getMethodLattice(md).getGlobalLoc(); + Location globalLoc = new Location(md, globalLocIdentifier); + NTuple locTuple = new NTuple(); + locTuple.add(globalLoc); + return locTuple; + } + private NTuple deriveLocationTuple(MethodDescriptor md, TempDescriptor td) { assert td.getType() != null; if (mapDescriptorToLocationPath.containsKey(td)) { - return mapDescriptorToLocationPath.get(td); + NTuple locPath = mapDescriptorToLocationPath.get(td); + NTuple rtrPath = new NTuple(); + rtrPath.addAll(locPath); + return rtrPath; } else { if (td.getSymbol().startsWith("this")) { - return deriveThisLocationTuple(md); + NTuple thisPath = deriveThisLocationTuple(md); + NTuple rtrPath = new NTuple(); + rtrPath.addAll(thisPath); + return rtrPath; } else { if (td.getType().getExtension() != null) { SSJavaType ssJavaType = (SSJavaType) td.getType().getExtension(); if (ssJavaType.getCompLoc() != null) { - NTuple locTuple = new NTuple(); - locTuple.addAll(ssJavaType.getCompLoc().getTuple()); - return locTuple; + NTuple rtrPath = new NTuple(); + rtrPath.addAll(ssJavaType.getCompLoc().getTuple()); + return rtrPath; } }