+ // read field
+ NTuple<Descriptor> srcHeapPath = mapHeapPath.get(rhs);
+ NTuple<Descriptor> fldHeapPath;
+ if (srcHeapPath != null) {
+ fldHeapPath = new NTuple<Descriptor>(srcHeapPath.getList());
+ } else {
+ // if srcHeapPath is null, it is static reference
+ fldHeapPath = new NTuple<Descriptor>();
+ fldHeapPath.add(rhs);
+ }
+ fldHeapPath.add(fld);
+
+ Set<WriteAge> writeAgeSet = curr.get(fldHeapPath);
+
+ checkWriteAgeSet(writeAgeSet, fldHeapPath, fn);
+
+ }
+ break;
+
+ case FKind.FlatSetFieldNode:
+ case FKind.FlatSetElementNode: {
+
+ if (fn.kind() == FKind.FlatSetFieldNode) {
+ FlatSetFieldNode fsfn = (FlatSetFieldNode) fn;
+ lhs = fsfn.getDst();
+ fld = fsfn.getField();
+ } else {
+ FlatSetElementNode fsen = (FlatSetElementNode) fn;
+ lhs = fsen.getDst();
+ rhs = fsen.getSrc();
+ TypeDescriptor td = lhs.getType().dereference();
+ fld = getArrayField(td);
+ }
+
+ // System.out.println("FIELD WRITE:" + fn);
+
+ // write(field)
+ NTuple<Descriptor> lhsHeapPath = computePath(lhs);
+ NTuple<Descriptor> fldHeapPath = new NTuple<Descriptor>(lhsHeapPath.getList());
+ fldHeapPath.add(fld);
+
+ // shared loc extension
+ Location fieldLoc = (Location) fld.getType().getExtension();
+ if (ssjava.isSharedLocation(fieldLoc)) {
+
+ NTuple<Location> fieldLocTuple = new NTuple<Location>();
+ fieldLocTuple.addAll(mapDescriptorToLocationPath.get(lhs));
+ fieldLocTuple.add(fieldLoc);
+
+ Set<NTuple<Descriptor>> writtenSet =
+ mapFlatNodeToSharedLocMapping.get(fn).get(fieldLocTuple);
+
+ if (isCovered(fieldLocTuple, writtenSet)) {
+ computeKILLSetForSharedWrite(curr, writtenSet, readWriteKillSet);
+ computeGENSetForSharedAllCoverWrite(curr, writtenSet, readWriteGenSet);
+ } else {
+ computeGENSetForSharedNonCoverWrite(curr, 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);
+
+ checkManyRead(fc, curr);
+ }
+ break;
+
+ }
+
+ computeNewMapping(curr, readWriteKillSet, readWriteGenSet);
+ // System.out.println("#######" + 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>> inSet) {
+
+ if (inSet == null) {
+ return false;
+ }
+
+ Set<NTuple<Descriptor>> coverSet =
+ mapMethodToSharedLocCoverSet.get(methodContainingSSJavaLoop).get(locTuple);
+
+ return inSet.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) {
+
+ // 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());
+ }
+ }
+ }
+ }
+
+ private void generateGENSetForFlatCall(FlatCall fc, SharedLocMap sharedLocMap,
+ 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, sharedLocMap);
+
+ Set<NTuple<Descriptor>> sharedWriteHeapPathSet = sharedLocMap.get(locTuple);
+
+ if (isCovered(locTuple, sharedLocMap.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));
+ }
+
+ } else {
+ // if not covered, add write age 1 to the heap path that is
+ // may-written but not covered
+ addWriteAgeToSet(heapPath, GENSet, new WriteAge(1));
+ }
+
+ }
+
+ }
+
+ }
+
+ private void addWriteAgeToSet(NTuple<Descriptor> heapPath,
+ Hashtable<NTuple<Descriptor>, Set<WriteAge>> map, WriteAge age) {
+
+ Set<WriteAge> currSet = map.get(heapPath);
+ if (currSet == null) {
+ currSet = new HashSet<WriteAge>();
+ map.put(heapPath, currSet);
+ }
+
+ currSet.add(age);
+ }
+
+ private void generateKILLSetForFlatCall(FlatCall fc,
+ Hashtable<NTuple<Descriptor>, Set<WriteAge>> curr, SharedLocMap sharedLocMap,
+ Hashtable<NTuple<Descriptor>, Set<WriteAge>> KILLSet) {