+ }
+ break;
+
+ }
+
+ computeNewMapping(curr, readWriteKillSet, readWriteGenSet);
+ if (fn instanceof FlatCall) {
+ checkManyRead((FlatCall) fn, curr);
+ }
+
+ }
+
+ }
+
+ private void computeGENSetForSharedNonCoverWrite(
+ Hashtable<NTuple<Descriptor>, Set<WriteAge>> curr, NTuple<Descriptor> heapPath,
+ Hashtable<NTuple<Descriptor>, Set<WriteAge>> genSet) {
+
+ Set<WriteAge> writeAgeSet = genSet.get(heapPath);
+ if (writeAgeSet == null) {
+ writeAgeSet = new HashSet<WriteAge>();
+ genSet.put(heapPath, writeAgeSet);
+ }
+
+ writeAgeSet.add(new WriteAge(1));
+
+ }
+
+ private void computeGENSetForSharedAllCoverWrite(
+ Hashtable<NTuple<Descriptor>, Set<WriteAge>> curr, Set<NTuple<Descriptor>> writtenSet,
+ Hashtable<NTuple<Descriptor>, Set<WriteAge>> genSet) {
+
+ for (Iterator iterator = writtenSet.iterator(); iterator.hasNext();) {
+ NTuple<Descriptor> writeHeapPath = (NTuple<Descriptor>) iterator.next();
+
+ Set<WriteAge> writeAgeSet = new HashSet<WriteAge>();
+ writeAgeSet.add(new WriteAge(0));
+
+ genSet.put(writeHeapPath, writeAgeSet);
+ }
+
+ }
+
+ private void computeKILLSetForSharedWrite(Hashtable<NTuple<Descriptor>, Set<WriteAge>> curr,
+ Set<NTuple<Descriptor>> writtenSet, Hashtable<NTuple<Descriptor>, Set<WriteAge>> killSet) {
+
+ for (Iterator iterator = writtenSet.iterator(); iterator.hasNext();) {
+ NTuple<Descriptor> writeHeapPath = (NTuple<Descriptor>) iterator.next();
+ Set<WriteAge> writeSet = curr.get(writeHeapPath);
+ if (writeSet != null) {
+ killSet.put(writeHeapPath, writeSet);
+ }
+ }
+
+ }
+
+ private boolean isCovered(NTuple<Location> locTuple, Set<NTuple<Descriptor>> curWrittenSet) {
+
+ Set<NTuple<Descriptor>> coverSet =
+ mapMethodToSharedLocCoverSet.get(methodContainingSSJavaLoop).get(locTuple);
+
+ if (curWrittenSet == null) {
+ return false;
+ }
+
+ return curWrittenSet.containsAll(coverSet);
+ }
+
+ private boolean isCovered(NTuple<Location> locTuple, Set<NTuple<Descriptor>> curWrittenSet,
+ Set<NTuple<Descriptor>> mustClearSet) {
+
+ Set<NTuple<Descriptor>> coverSet =
+ mapMethodToSharedLocCoverSet.get(methodContainingSSJavaLoop).get(locTuple);
+
+ if (mustClearSet != null && mustClearSet.containsAll(coverSet)) {
+ return true;
+ }
+
+ if (curWrittenSet == null) {
+ return false;
+ }
+
+ return curWrittenSet.containsAll(coverSet);
+ }
+
+ private void checkManyRead(FlatCall fc, Hashtable<NTuple<Descriptor>, Set<WriteAge>> curr) {
+ Set<NTuple<Descriptor>> boundReadSet = mapFlatNodeToBoundReadSet.get(fc);
+ for (Iterator iterator = boundReadSet.iterator(); iterator.hasNext();) {
+ NTuple<Descriptor> readHeapPath = (NTuple<Descriptor>) iterator.next();
+ Set<WriteAge> writeAgeSet = curr.get(readHeapPath);
+ checkWriteAgeSet(writeAgeSet, readHeapPath, fc);
+ }
+
+ }
+
+ private void checkWriteAgeSet(Set<WriteAge> writeAgeSet, NTuple<Descriptor> path, FlatNode fn) {
+
+ if (writeAgeSet != null) {
+ for (Iterator iterator = writeAgeSet.iterator(); iterator.hasNext();) {
+ WriteAge writeAge = (WriteAge) iterator.next();
+ if (writeAge.getAge() > MAXAGE) {
+ generateErrorMessage(path, fn);
+ }
+ }
+ }
+ }
+
+ private void generateErrorMessage(NTuple<Descriptor> path, FlatNode fn) {
+
+ Descriptor lastDesc = path.get(getArrayBaseDescriptorIdx(path));
+ if (ssjava.isSharedLocation(getLocation(lastDesc))) {
+
+ NTuple<Location> locPathTuple = getLocationTuple(path);
+ Set<NTuple<Descriptor>> 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,
+ SharedLocMap mustClearMap, Hashtable<NTuple<Descriptor>, Set<WriteAge>> GENSet) {
+
+ Set<NTuple<Descriptor>> boundMayWriteSet = mapFlatNodeToBoundMayWriteSet.get(fc);
+
+ for (Iterator iterator = boundMayWriteSet.iterator(); iterator.hasNext();) {
+ NTuple<Descriptor> heapPath = (NTuple<Descriptor>) iterator.next();
+
+ if (!isSharedLocation(heapPath)) {
+ addWriteAgeToSet(heapPath, GENSet, new WriteAge(0));
+ } else {
+ // if the current heap path is shared location
+
+ NTuple<Location> locTuple = getLocationTuple(heapPath);
+
+ Set<NTuple<Descriptor>> sharedWriteHeapPathSet = 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<Descriptor> sharedHeapPath = (NTuple<Descriptor>) iterator2.next();
+ addWriteAgeToSet(sharedHeapPath, GENSet, new WriteAge(0));