projects
/
IRC.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
a439ce6
)
Finally, all benchmarks pass the definitely written analysis
author
yeom
<yeom>
Thu, 15 Dec 2011 21:57:19 +0000
(21:57 +0000)
committer
yeom
<yeom>
Thu, 15 Dec 2011 21:57:19 +0000
(21:57 +0000)
Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
patch
|
blob
|
history
diff --git
a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
index 26b7c9ba0abc17366e577efdc23e061ba5b00e44..f187a38d027af700918b77e204cdce2f6a511e14 100644
(file)
--- a/
Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
+++ b/
Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
@@
-366,14
+366,6
@@
public class DefinitelyWrittenCheck {
updateDeleteSetForSameHeightWrite(currDeleteSet, lhsLocTuple, lhsHeapPath);
}
updateDeleteSetForSameHeightWrite(currDeleteSet, 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);
-
}
} else {
break;
}
} else {
break;
@@
-455,14
+447,6
@@
public class DefinitelyWrittenCheck {
updateDeleteSetForSameHeightWrite(currDeleteSet, 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);
}
}
}
}
@@
-477,11
+461,6
@@
public class DefinitelyWrittenCheck {
generateKILLSetForFlatCall(curr, killSet);
generateGENSetForFlatCall(curr, genSet);
generateKILLSetForFlatCall(curr, killSet);
generateGENSetForFlatCall(curr, genSet);
- // System.out.println("#FLATCALL=" + fc);
- // System.out.println("KILLSET=" + killSet);
- // System.out.println("GENSet=" + genSet);
- // System.out.println("bound DELETE Set=" + calleeUnionBoundDeleteSet);
-
}
break;
}
break;
@@
-490,16
+469,12
@@
public class DefinitelyWrittenCheck {
mergeSharedLocMap(sharedLocMap, curr);
mergeDeleteSet(deleteSet, currDeleteSet);
mergeSharedLocMap(sharedLocMap, curr);
mergeDeleteSet(deleteSet, currDeleteSet);
- // System.out.println("#FLATEXIT sharedLocMap=" + sharedLocMap);
}
break;
}
computeNewMapping(curr, killSet, genSet);
}
break;
}
computeNewMapping(curr, killSet, genSet);
- if (!curr.map.isEmpty()) {
- // System.out.println(fn + "#######" + curr);
- }
}
}
@@
-639,8
+614,7
@@
public class DefinitelyWrittenCheck {
private void computeSharedCoverSet_analyzeMethod(FlatMethod fm, boolean onlyVisitSSJavaLoop) {
private void computeSharedCoverSet_analyzeMethod(FlatMethod fm, boolean onlyVisitSSJavaLoop) {
- System.out.println("\n###");
- System.out.println("computeSharedCoverSet_analyzeMethod=" + fm);
+ // System.out.println("computeSharedCoverSet_analyzeMethod=" + fm);
MethodDescriptor md = fm.getMethod();
Set<FlatNode> flatNodesToVisit = new HashSet<FlatNode>();
MethodDescriptor md = fm.getMethod();
Set<FlatNode> flatNodesToVisit = new HashSet<FlatNode>();
@@
-792,7
+766,18
@@
public class DefinitelyWrittenCheck {
}
NTuple<Location> lhsLocTuple = new NTuple<Location>();
}
NTuple<Location> lhsLocTuple = new NTuple<Location>();
- lhsLocTuple.addAll(deriveLocationTuple(md, lhs));
+ 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));
+ }
+
mapDescriptorToLocationPath.put(lhs, lhsLocTuple);
NTuple<Location> fieldLocTuple = new NTuple<Location>();
mapDescriptorToLocationPath.put(lhs, lhsLocTuple);
NTuple<Location> fieldLocTuple = new NTuple<Location>();
@@
-1334,10
+1319,6
@@
public class DefinitelyWrittenCheck {
computeGENSetForWrite(lhsHeapPath, readWriteGenSet);
}
computeGENSetForWrite(lhsHeapPath, readWriteGenSet);
}
- // System.out.println("write effect on =" + lhsHeapPath);
- // System.out.println("#KILLSET=" + readWriteKillSet);
- // System.out.println("#GENSet=" + readWriteGenSet + "\n");
-
Set<WriteAge> writeAgeSet = curr.get(lhsHeapPath);
checkWriteAgeSet(writeAgeSet, lhsHeapPath, fn);
}
Set<WriteAge> writeAgeSet = curr.get(lhsHeapPath);
checkWriteAgeSet(writeAgeSet, lhsHeapPath, fn);
}
@@
-1440,9
+1421,6
@@
public class DefinitelyWrittenCheck {
computeGENSetForWrite(fldHeapPath, readWriteGenSet);
}
computeGENSetForWrite(fldHeapPath, readWriteGenSet);
}
- // System.out.println("KILLSET=" + readWriteKillSet);
- // System.out.println("GENSet=" + readWriteGenSet);
-
}
}
}
}
@@
-1452,13
+1430,9
@@
public class DefinitelyWrittenCheck {
FlatCall fc = (FlatCall) fn;
SharedLocMap sharedLocMap = mapFlatNodeToSharedLocMapping.get(fc);
FlatCall fc = (FlatCall) fn;
SharedLocMap sharedLocMap = mapFlatNodeToSharedLocMapping.get(fc);
- // System.out.println("FLATCALL:" + fn);
generateKILLSetForFlatCall(fc, curr, sharedLocMap, readWriteKillSet);
generateGENSetForFlatCall(fc, sharedLocMap, readWriteGenSet);
generateKILLSetForFlatCall(fc, curr, sharedLocMap, readWriteKillSet);
generateGENSetForFlatCall(fc, sharedLocMap, readWriteGenSet);
- // System.out.println("KILLSET=" + readWriteKillSet);
- // System.out.println("GENSet=" + readWriteGenSet);
-
}
break;
}
break;
@@
-1469,8
+1443,6
@@
public class DefinitelyWrittenCheck {
checkManyRead((FlatCall) fn, curr);
}
checkManyRead((FlatCall) fn, curr);
}
- // System.out.println("#######" + curr);
-
}
}
}
}
@@
-1526,9
+1498,6
@@
public class DefinitelyWrittenCheck {
Set<NTuple<Descriptor>> coverSet =
mapMethodToSharedLocCoverSet.get(methodContainingSSJavaLoop).get(locTuple);
Set<NTuple<Descriptor>> coverSet =
mapMethodToSharedLocCoverSet.get(methodContainingSSJavaLoop).get(locTuple);
- // System.out.println("locTuple=" + locTuple + " coverSet=" + coverSet +
- // " currSet=" + inSet);
-
return inSet.containsAll(coverSet);
}
return inSet.containsAll(coverSet);
}
@@
-1546,9
+1515,6
@@
public class DefinitelyWrittenCheck {
private void checkWriteAgeSet(Set<WriteAge> writeAgeSet, NTuple<Descriptor> path, FlatNode fn) {
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 (writeAgeSet != null) {
for (Iterator iterator = writeAgeSet.iterator(); iterator.hasNext();) {
WriteAge writeAge = (WriteAge) iterator.next();
@@
-1587,7
+1553,6
@@
public class DefinitelyWrittenCheck {
Hashtable<NTuple<Descriptor>, Set<WriteAge>> GENSet) {
Set<NTuple<Descriptor>> boundMayWriteSet = mapFlatNodeToBoundMayWriteSet.get(fc);
Hashtable<NTuple<Descriptor>, Set<WriteAge>> GENSet) {
Set<NTuple<Descriptor>> boundMayWriteSet = mapFlatNodeToBoundMayWriteSet.get(fc);
- // System.out.println("boundMayWriteSet=" + boundMayWriteSet);
for (Iterator iterator = boundMayWriteSet.iterator(); iterator.hasNext();) {
NTuple<Descriptor> heapPath = (NTuple<Descriptor>) iterator.next();
for (Iterator iterator = boundMayWriteSet.iterator(); iterator.hasNext();) {
NTuple<Descriptor> heapPath = (NTuple<Descriptor>) iterator.next();