From: yeom <yeom>
Date: Tue, 23 Aug 2011 23:19:05 +0000 (+0000)
Subject: 1) changes on the definitely written analysis: it only takes care about locations...
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=95ade08265a30f939a5f49aa3d25db6152d0e6fd;p=IRC.git
1) changes on the definitely written analysis: it only takes care about locations that are written to inside of the SSJava loop
2) bug fix on the definitely written analysis: static method doesn't have implicit 'this' argument.
3) add a set of static functions that initialize array elements
4) changes on mp3decoder: move init() method out of SSJava loop and start to use SSJava array init method
---
diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
index 2536171d..cec3a49d 100644
--- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
+++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
@@ -57,6 +57,10 @@ public class DefinitelyWrittenCheck {
// overwritten on every possible path during method invocation
private Hashtable<FlatMethod, Set<NTuple<Descriptor>>> mapFlatMethodToOverWrite;
+ // maps a flat method to the WRITE that is the set of heap path that is
+ // written to
+ private Hashtable<FlatMethod, Set<NTuple<Descriptor>>> mapFlatMethodToWrite;
+
// points to method containing SSJAVA Loop
private MethodDescriptor methodContainingSSJavaLoop;
@@ -98,6 +102,7 @@ public class DefinitelyWrittenCheck {
private Set<NTuple<Descriptor>> calleeUnionBoundReadSet;
private Set<NTuple<Descriptor>> calleeIntersectBoundOverWriteSet;
+ private Set<NTuple<Descriptor>> calleeBoundWriteSet;
private TempDescriptor LOCAL;
@@ -110,10 +115,12 @@ public class DefinitelyWrittenCheck {
this.mapHeapPath = new Hashtable<Descriptor, NTuple<Descriptor>>();
this.mapFlatMethodToRead = new Hashtable<FlatMethod, Set<NTuple<Descriptor>>>();
this.mapFlatMethodToOverWrite = new Hashtable<FlatMethod, Set<NTuple<Descriptor>>>();
+ this.mapFlatMethodToWrite = new Hashtable<FlatMethod, Set<NTuple<Descriptor>>>();
this.definitelyWrittenResults =
new Hashtable<FlatNode, Hashtable<NTuple<Descriptor>, Hashtable<FlatNode, Boolean>>>();
this.calleeUnionBoundReadSet = new HashSet<NTuple<Descriptor>>();
this.calleeIntersectBoundOverWriteSet = new HashSet<NTuple<Descriptor>>();
+ this.calleeBoundWriteSet = new HashSet<NTuple<Descriptor>>();
this.mapMethodDescriptorToCompleteClearingSummary =
new Hashtable<MethodDescriptor, ClearingSummary>();
@@ -131,8 +138,8 @@ public class DefinitelyWrittenCheck {
if (!ssjava.getAnnotationRequireSet().isEmpty()) {
methodReadOverWriteAnalysis();
writtenAnalyis();
- sharedLocationAnalysis();
- checkSharedLocationResult();
+ // sharedLocationAnalysis();
+ // checkSharedLocationResult();
}
}
@@ -143,7 +150,6 @@ public class DefinitelyWrittenCheck {
ClearingSummary result =
mapMethodDescriptorToCompleteClearingSummary.get(sortedDescriptors.peekFirst());
-
Set<NTuple<Descriptor>> hpKeySet = result.keySet();
for (Iterator iterator = hpKeySet.iterator(); iterator.hasNext();) {
NTuple<Descriptor> hpKey = (NTuple<Descriptor>) iterator.next();
@@ -342,18 +348,36 @@ public class DefinitelyWrittenCheck {
case FKind.FlatFieldNode:
case FKind.FlatElementNode: {
- FlatFieldNode ffn = (FlatFieldNode) fn;
- lhs = ffn.getDst();
- rhs = ffn.getSrc();
- fld = ffn.getField();
+ if (fn.kind() == FKind.FlatFieldNode) {
+ FlatFieldNode ffn = (FlatFieldNode) fn;
+ lhs = ffn.getDst();
+ rhs = ffn.getSrc();
+ fld = ffn.getField();
+ } else {
+ FlatElementNode fen = (FlatElementNode) fn;
+ lhs = fen.getDst();
+ rhs = fen.getSrc();
+ TypeDescriptor td = rhs.getType().dereference();
+ fld = getArrayField(td);
+ }
+
+ // FlatFieldNode ffn = (FlatFieldNode) fn;
+ // lhs = ffn.getDst();
+ // rhs = ffn.getSrc();
+ // fld = ffn.getField();
// read field
NTuple<Descriptor> srcHeapPath = mapHeapPath.get(rhs);
+
+ // if (srcHeapPath != null) {
+ // // if lhs srcHeapPath is null, it means that it is not reachable from
+ // // callee's parameters. so just ignore it
NTuple<Descriptor> fldHeapPath = new NTuple<Descriptor>(srcHeapPath.getList());
if (fld.getType().isImmutable()) {
readLocation(curr, fldHeapPath, fld);
}
+ // }
}
break;
@@ -395,8 +419,8 @@ public class DefinitelyWrittenCheck {
MethodDescriptor mdCallee = fc.getMethod();
FlatMethod fmCallee = state.getMethodFlat(mdCallee);
Set<MethodDescriptor> setPossibleCallees = new HashSet<MethodDescriptor>();
- TypeDescriptor typeDesc = fc.getThis().getType();
- setPossibleCallees.addAll(callGraph.getMethods(mdCallee, typeDesc));
+ // TypeDescriptor typeDesc = fc.getThis().getType();
+ setPossibleCallees.addAll(callGraph.getMethods(mdCallee));
possibleCalleeCompleteSummarySetToCaller.clear();
@@ -453,15 +477,17 @@ public class DefinitelyWrittenCheck {
Hashtable<Integer, NTuple<Descriptor>> mapArgIdx2CallerArgHeapPath =
new Hashtable<Integer, NTuple<Descriptor>>();
- // arg idx is starting from 'this' arg
- NTuple<Descriptor> thisHeapPath = mapHeapPath.get(fc.getThis());
- if (thisHeapPath == null) {
- // method is called without creating new flat node representing 'this'
- thisHeapPath = new NTuple<Descriptor>();
- thisHeapPath.add(fc.getThis());
- }
+ if (fc.getThis() != null) {
+ // arg idx is starting from 'this' arg
+ NTuple<Descriptor> thisHeapPath = mapHeapPath.get(fc.getThis());
+ if (thisHeapPath == null) {
+ // method is called without creating new flat node representing 'this'
+ thisHeapPath = new NTuple<Descriptor>();
+ thisHeapPath.add(fc.getThis());
+ }
- mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath);
+ mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath);
+ }
for (int i = 0; i < fc.numArgs(); i++) {
TempDescriptor arg = fc.getArg(i);
@@ -635,10 +661,23 @@ public class DefinitelyWrittenCheck {
case FKind.FlatFieldNode:
case FKind.FlatElementNode: {
- FlatFieldNode ffn = (FlatFieldNode) fn;
- lhs = ffn.getDst();
- rhs = ffn.getSrc();
- fld = ffn.getField();
+ if (fn.kind() == FKind.FlatFieldNode) {
+ FlatFieldNode ffn = (FlatFieldNode) fn;
+ lhs = ffn.getDst();
+ rhs = ffn.getSrc();
+ fld = ffn.getField();
+ } else {
+ FlatElementNode fen = (FlatElementNode) fn;
+ lhs = fen.getDst();
+ rhs = fen.getSrc();
+ TypeDescriptor td = rhs.getType().dereference();
+ fld = getArrayField(td);
+ }
+
+ // FlatFieldNode ffn = (FlatFieldNode) fn;
+ // lhs = ffn.getDst();
+ // rhs = ffn.getSrc();
+ // fld = ffn.getField();
// read field
NTuple<Descriptor> srcHeapPath = mapHeapPath.get(rhs);
@@ -954,12 +993,13 @@ public class DefinitelyWrittenCheck {
case FKind.FlatCall: {
FlatCall fc = (FlatCall) fn;
+
bindHeapPathCallerArgWithCaleeParam(fc);
// add <hp,statement,false> in which hp is an element of
// READ_bound set
// of callee: callee has 'read' requirement!
-
+
for (Iterator iterator = calleeUnionBoundReadSet.iterator(); iterator.hasNext();) {
NTuple<Descriptor> read = (NTuple<Descriptor>) iterator.next();
Hashtable<FlatNode, Boolean> gen = curr.get(read);
@@ -1030,80 +1070,119 @@ public class DefinitelyWrittenCheck {
// caller
calleeUnionBoundReadSet.clear();
calleeIntersectBoundOverWriteSet.clear();
+ calleeBoundWriteSet.clear();
- MethodDescriptor mdCallee = fc.getMethod();
- FlatMethod fmCallee = state.getMethodFlat(mdCallee);
- Set<MethodDescriptor> setPossibleCallees = new HashSet<MethodDescriptor>();
- TypeDescriptor typeDesc = fc.getThis().getType();
- setPossibleCallees.addAll(callGraph.getMethods(mdCallee, typeDesc));
+ if (ssjava.isSSJavaUtil(fc.getMethod().getClassDesc())) {
+ // ssjava util case!
+ // have write effects on the first argument
+ TempDescriptor arg = fc.getArg(0);
+ NTuple<Descriptor> argHeapPath = computePath(arg);
+ calleeIntersectBoundOverWriteSet.add(argHeapPath);
+ } else {
+ MethodDescriptor mdCallee = fc.getMethod();
+ // FlatMethod fmCallee = state.getMethodFlat(mdCallee);
+ Set<MethodDescriptor> setPossibleCallees = new HashSet<MethodDescriptor>();
+ // setPossibleCallees.addAll(callGraph.getMethods(mdCallee, typeDesc));
+ setPossibleCallees.addAll(callGraph.getMethods(mdCallee));
- // create mapping from arg idx to its heap paths
- Hashtable<Integer, NTuple<Descriptor>> mapArgIdx2CallerArgHeapPath =
- new Hashtable<Integer, NTuple<Descriptor>>();
+ // create mapping from arg idx to its heap paths
+ Hashtable<Integer, NTuple<Descriptor>> mapArgIdx2CallerArgHeapPath =
+ new Hashtable<Integer, NTuple<Descriptor>>();
- // arg idx is starting from 'this' arg
- NTuple<Descriptor> thisHeapPath = mapHeapPath.get(fc.getThis());
- if (thisHeapPath == null) {
- // method is called without creating new flat node representing 'this'
- thisHeapPath = new NTuple<Descriptor>();
- thisHeapPath.add(fc.getThis());
- }
+ // arg idx is starting from 'this' arg
+ if (fc.getThis() != null) {
+ NTuple<Descriptor> thisHeapPath = mapHeapPath.get(fc.getThis());
+ if (thisHeapPath == null) {
+ // method is called without creating new flat node representing 'this'
+ thisHeapPath = new NTuple<Descriptor>();
+ thisHeapPath.add(fc.getThis());
+ }
- mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath);
+ mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath);
+ }
- for (int i = 0; i < fc.numArgs(); i++) {
- TempDescriptor arg = fc.getArg(i);
- NTuple<Descriptor> argHeapPath = computePath(arg);
- mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(i + 1), argHeapPath);
- }
+ for (int i = 0; i < fc.numArgs(); i++) {
+ TempDescriptor arg = fc.getArg(i);
+ NTuple<Descriptor> 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);
+ 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
+ // binding caller's args and callee's params
- Set<NTuple<Descriptor>> calleeReadSet = mapFlatMethodToRead.get(calleeFlatMethod);
- if (calleeReadSet == null) {
- calleeReadSet = new HashSet<NTuple<Descriptor>>();
- mapFlatMethodToRead.put(calleeFlatMethod, calleeReadSet);
- }
- Set<NTuple<Descriptor>> calleeOverWriteSet = mapFlatMethodToOverWrite.get(calleeFlatMethod);
- if (calleeOverWriteSet == null) {
- calleeOverWriteSet = new HashSet<NTuple<Descriptor>>();
- mapFlatMethodToOverWrite.put(calleeFlatMethod, calleeOverWriteSet);
- }
+ Set<NTuple<Descriptor>> calleeReadSet = mapFlatMethodToRead.get(calleeFlatMethod);
+ if (calleeReadSet == null) {
+ calleeReadSet = new HashSet<NTuple<Descriptor>>();
+ mapFlatMethodToRead.put(calleeFlatMethod, calleeReadSet);
+ }
- Hashtable<Integer, TempDescriptor> mapParamIdx2ParamTempDesc =
- new Hashtable<Integer, TempDescriptor>();
- for (int i = 0; i < calleeFlatMethod.numParameters(); i++) {
- TempDescriptor param = calleeFlatMethod.getParameter(i);
- mapParamIdx2ParamTempDesc.put(Integer.valueOf(i), param);
+ Set<NTuple<Descriptor>> calleeOverWriteSet = mapFlatMethodToOverWrite.get(calleeFlatMethod);
+
+ if (calleeOverWriteSet == null) {
+ calleeOverWriteSet = new HashSet<NTuple<Descriptor>>();
+ mapFlatMethodToOverWrite.put(calleeFlatMethod, calleeOverWriteSet);
+ }
+
+ Set<NTuple<Descriptor>> calleeWriteSet = mapFlatMethodToWrite.get(calleeFlatMethod);
+
+ if (calleeWriteSet == null) {
+ calleeWriteSet = new HashSet<NTuple<Descriptor>>();
+ mapFlatMethodToWrite.put(calleeFlatMethod, calleeWriteSet);
+ }
+
+ Hashtable<Integer, TempDescriptor> mapParamIdx2ParamTempDesc =
+ new Hashtable<Integer, TempDescriptor>();
+ 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<NTuple<Descriptor>> calleeBoundReadSet =
+ bindSet(calleeReadSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath);
+ // union of the current read set and the current callee's
+ // read set
+ calleeUnionBoundReadSet.addAll(calleeBoundReadSet);
+ Set<NTuple<Descriptor>> calleeBoundOverWriteSet =
+ bindSet(calleeOverWriteSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath);
+ // intersection of the current overwrite set and the current
+ // callee's
+ // overwrite set
+ merge(calleeIntersectBoundOverWriteSet, calleeBoundOverWriteSet);
+
+ Set<NTuple<Descriptor>> boundWriteSetFromCallee =
+ bindSet(calleeWriteSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath);
+ calleeBoundWriteSet.addAll(boundWriteSetFromCallee);
}
- Set<NTuple<Descriptor>> calleeBoundReadSet =
- bindSet(calleeReadSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath);
- // union of the current read set and the current callee's
- // read set
- calleeUnionBoundReadSet.addAll(calleeBoundReadSet);
- Set<NTuple<Descriptor>> calleeBoundWriteSet =
- bindSet(calleeOverWriteSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath);
- // intersection of the current overwrite set and the current
- // callee's
- // overwrite set
- merge(calleeIntersectBoundOverWriteSet, calleeBoundWriteSet);
}
}
private void checkFlag(boolean booleanValue, FlatNode fn, NTuple<Descriptor> hp) {
if (booleanValue) {
- throw new Error(
- "There is a variable, which is reachable through references "
- + hp
- + ", who comes back to the same read statement without being overwritten at the out-most iteration at "
- + methodContainingSSJavaLoop.getClassDesc().getSourceFileName() + "::"
- + fn.getNumLine());
+ // the definitely written analysis only takes care about locations that
+ // are written to inside of the SSJava loop
+ for (Iterator iterator = calleeBoundWriteSet.iterator(); iterator.hasNext();) {
+ NTuple<Descriptor> write = (NTuple<Descriptor>) iterator.next();
+ if (hp.startsWith(write)) {
+ // it has write effect!
+ //throw new Error(
+ System.out.println("###"+
+ "There is a variable, which is reachable through references "
+ + hp
+ + ", who comes back to the same read statement without being overwritten at the out-most iteration at "
+ + methodContainingSSJavaLoop.getClassDesc().getSourceFileName() + "::"
+ + fn.getNumLine());
+ }
+ }
}
}
@@ -1174,15 +1253,19 @@ public class DefinitelyWrittenCheck {
Set<NTuple<Descriptor>> readSet = new HashSet<NTuple<Descriptor>>();
Set<NTuple<Descriptor>> overWriteSet = new HashSet<NTuple<Descriptor>>();
+ Set<NTuple<Descriptor>> writeSet = new HashSet<NTuple<Descriptor>>();
- methodReadOverWrite_analyzeMethod(fm, readSet, overWriteSet);
+ methodReadOverWrite_analyzeMethod(fm, readSet, overWriteSet, writeSet);
Set<NTuple<Descriptor>> prevRead = mapFlatMethodToRead.get(fm);
Set<NTuple<Descriptor>> prevOverWrite = mapFlatMethodToOverWrite.get(fm);
+ Set<NTuple<Descriptor>> prevWrite = mapFlatMethodToWrite.get(fm);
- if (!(readSet.equals(prevRead) && overWriteSet.equals(prevOverWrite))) {
+ if (!(readSet.equals(prevRead) && overWriteSet.equals(prevOverWrite) && writeSet
+ .equals(prevWrite))) {
mapFlatMethodToRead.put(fm, readSet);
mapFlatMethodToOverWrite.put(fm, overWriteSet);
+ mapFlatMethodToWrite.put(fm, writeSet);
// results for callee changed, so enqueue dependents caller for
// further
@@ -1204,7 +1287,7 @@ public class DefinitelyWrittenCheck {
}
private void methodReadOverWrite_analyzeMethod(FlatMethod fm, Set<NTuple<Descriptor>> readSet,
- Set<NTuple<Descriptor>> overWriteSet) {
+ Set<NTuple<Descriptor>> overWriteSet, Set<NTuple<Descriptor>> writeSet) {
if (state.SSJAVADEBUG) {
System.out.println("Definitely written Analyzing: " + fm);
}
@@ -1227,7 +1310,7 @@ public class DefinitelyWrittenCheck {
}
}
- methodReadOverWrite_nodeActions(fn, curr, readSet, overWriteSet);
+ methodReadOverWrite_nodeActions(fn, curr, readSet, overWriteSet, writeSet);
Set<NTuple<Descriptor>> writtenSetPrev = mapFlatNodeToWrittenSet.get(fn);
if (!curr.equals(writtenSetPrev)) {
@@ -1240,10 +1323,12 @@ public class DefinitelyWrittenCheck {
}
+
}
private void methodReadOverWrite_nodeActions(FlatNode fn, Set<NTuple<Descriptor>> writtenSet,
- Set<NTuple<Descriptor>> readSet, Set<NTuple<Descriptor>> overWriteSet) {
+ Set<NTuple<Descriptor>> readSet, Set<NTuple<Descriptor>> overWriteSet,
+ Set<NTuple<Descriptor>> writeSet) {
TempDescriptor lhs;
TempDescriptor rhs;
FieldDescriptor fld;
@@ -1320,7 +1405,7 @@ public class DefinitelyWrittenCheck {
}
}
- //no need to kill hp(x.f) from WT
+ // no need to kill hp(x.f) from WT
}
}
@@ -1356,6 +1441,8 @@ public class DefinitelyWrittenCheck {
// write(x.f)
// need to add hp(y) to WT
writtenSet.add(newHeapPath);
+
+ writeSet.add(newHeapPath);
}
}
@@ -1365,26 +1452,31 @@ public class DefinitelyWrittenCheck {
FlatCall fc = (FlatCall) fn;
- if (fc.getThis() != null) {
- bindHeapPathCallerArgWithCaleeParam(fc);
-
- // add heap path, which is an element of READ_bound set and is not
- // an
- // element of WT set, to the caller's READ set
- for (Iterator iterator = calleeUnionBoundReadSet.iterator(); iterator.hasNext();) {
- NTuple<Descriptor> read = (NTuple<Descriptor>) iterator.next();
- if (!writtenSet.contains(read)) {
- readSet.add(read);
- }
- }
+ bindHeapPathCallerArgWithCaleeParam(fc);
- // add heap path, which is an element of OVERWRITE_bound set, to the
- // caller's WT set
- for (Iterator iterator = calleeIntersectBoundOverWriteSet.iterator(); iterator.hasNext();) {
- NTuple<Descriptor> write = (NTuple<Descriptor>) iterator.next();
- writtenSet.add(write);
+ // add heap path, which is an element of READ_bound set and is not
+ // an
+ // element of WT set, to the caller's READ set
+ for (Iterator iterator = calleeUnionBoundReadSet.iterator(); iterator.hasNext();) {
+ NTuple<Descriptor> read = (NTuple<Descriptor>) iterator.next();
+ if (!writtenSet.contains(read)) {
+ readSet.add(read);
}
- }
+ }
+
+ // add heap path, which is an element of OVERWRITE_bound set, to the
+ // caller's WT set
+ for (Iterator iterator = calleeIntersectBoundOverWriteSet.iterator(); iterator.hasNext();) {
+ NTuple<Descriptor> write = (NTuple<Descriptor>) iterator.next();
+ writtenSet.add(write);
+ }
+
+ // add heap path, which is an element of WRITE_BOUND set, to the
+ // caller's writeSet
+ for (Iterator iterator = calleeBoundWriteSet.iterator(); iterator.hasNext();) {
+ NTuple<Descriptor> write = (NTuple<Descriptor>) iterator.next();
+ writeSet.add(write);
+ }
}
break;
@@ -1521,7 +1613,6 @@ public class DefinitelyWrittenCheck {
NTuple<Descriptor> callerArgHeapPath = mapCallerArgIdx2HeapPath.get(idx);
TempDescriptor calleeParam = mapParamIdx2ParamTempDesc.get(idx);
-
for (Iterator iterator2 = calleeSet.iterator(); iterator2.hasNext();) {
NTuple<Descriptor> element = (NTuple<Descriptor>) iterator2.next();
if (element.startsWith(calleeParam)) {
diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 89ba8091..259893ce 100644
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -852,7 +852,8 @@ public class FlowDownCheck {
isSystemout = baseName.getSymbol().equals("System.out");
}
- if (!ssjava.isTrustMethod(calleeMD) && !calleeMD.getModifiers().isNative() && !isSystemout) {
+ if (!ssjava.isSSJavaUtil(calleeMD.getClassDesc()) && !ssjava.isTrustMethod(calleeMD)
+ && !calleeMD.getModifiers().isNative() && !isSystemout) {
CompositeLocation baseLocation = null;
if (min.getExpression() != null) {
@@ -897,7 +898,8 @@ public class FlowDownCheck {
checkCalleeConstraints(md, nametable, min, baseLocation, constraint);
- checkCallerArgumentLocationConstraints(md, nametable, min, baseLocation, constraint);
+ // checkCallerArgumentLocationConstraints(md, nametable, min,
+ // baseLocation, constraint);
if (!min.getMethod().getReturnType().isVoid()) {
// If method has a return value, compute the highest possible return
@@ -1359,13 +1361,13 @@ public class FlowDownCheck {
return loc;
}
}
-
- if(left instanceof ArrayAccessNode){
+
+ if (left instanceof ArrayAccessNode) {
System.out.println("HEREE!!");
- ArrayAccessNode aan=(ArrayAccessNode)left;
- left=aan.getExpression();
+ ArrayAccessNode aan = (ArrayAccessNode) left;
+ left = aan.getExpression();
}
-
+
loc = checkLocationFromExpressionNode(md, nametable, left, loc, constraint, false);
System.out.println("### checkLocationFromFieldAccessNode=" + fan.printNode(0));
System.out.println("### left=" + left.printNode(0));
@@ -1373,7 +1375,7 @@ public class FlowDownCheck {
Location fieldLoc = getFieldLocation(fd);
loc.addLocation(fieldLoc);
}
- System.out.println("### field loc="+loc);
+ System.out.println("### field loc=" + loc);
return loc;
}
diff --git a/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java b/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
index 778c0553..b4a862a4 100644
--- a/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
+++ b/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
@@ -64,7 +64,7 @@ public class MethodAnnotationCheck {
ClassDescriptor cd = (ClassDescriptor) obj;
toanalyze.remove(cd);
- if (!cd.isInterface()) {
+ if (!ssjava.isSSJavaUtil(cd) && !cd.isInterface()) {
for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
MethodDescriptor md = (MethodDescriptor) method_it.next();
checkTrustworthyMethodAnnotation(md);
diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
index fb137633..28635cab 100644
--- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
+++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
@@ -97,16 +97,16 @@ public class SSJavaAnalysis {
this.mapSharedLocation2DescriptorSet = new Hashtable<Location, Set<Descriptor>>();
this.linearTypeCheckMethodSet = new HashSet<MethodDescriptor>();
this.bf = bf;
- trustWorthyMDSet = new HashSet<MethodDescriptor>();
+ this.trustWorthyMDSet = new HashSet<MethodDescriptor>();
}
public void doCheck() {
doMethodAnnotationCheck();
// computeLinearTypeCheckMethodSet();
// doLinearTypeCheck();
- // if (state.SSJAVADEBUG) {
- // debugPrint();
- // }
+ if (state.SSJAVADEBUG) {
+ debugPrint();
+ }
parseLocationAnnotation();
// doFlowDownCheck();
doDefinitelyWrittenCheck();
@@ -450,8 +450,10 @@ public class SSJavaAnalysis {
ClassDescriptor cd = md.getClassDesc();
// if a method requires to be annotated, class containg that method also
// requires to be annotated
- annotationRequireClassSet.add(cd);
- annotationRequireSet.add(md);
+ if (!isSSJavaUtil(cd)) {
+ annotationRequireClassSet.add(cd);
+ annotationRequireSet.add(md);
+ }
}
public Set<MethodDescriptor> getAnnotationRequireSet() {
@@ -504,4 +506,11 @@ public class SSJavaAnalysis {
public void setMethodContainingSSJavaLoop(MethodDescriptor methodContainingSSJavaLoop) {
this.methodContainingSSJavaLoop = methodContainingSSJavaLoop;
}
+
+ public boolean isSSJavaUtil(ClassDescriptor cd) {
+ if (cd.getSymbol().equals("SSJAVA")) {
+ return true;
+ }
+ return false;
+ }
}
diff --git a/Robust/src/ClassLibrary/SSJava/SSJAVA.java b/Robust/src/ClassLibrary/SSJava/SSJAVA.java
new file mode 100644
index 00000000..fbe5dad0
--- /dev/null
+++ b/Robust/src/ClassLibrary/SSJava/SSJAVA.java
@@ -0,0 +1,47 @@
+public class SSJAVA {
+
+ // Definitely written analysis assumes that the first parameter may have write
+ // effects through the below methods
+
+ static void arrayinit(float array[], float value) {
+ for (int i = 0; i < array.length; i++) {
+ array[i] = value;
+ }
+ }
+
+ static void arrayinit(int array[], int value) {
+ for (int i = 0; i < array.length; i++) {
+ array[i] = value;
+ }
+ }
+
+ static void arrayinit(float array[][][], int size_1, int size_2, int size_3, float value) {
+
+ for (int idx1 = 0; idx1 < size_1; idx1++) {
+ if (array[idx1].length != size_2) {
+ throw new Error("Array initilizatiion failed to assign to all of elements.");
+ }
+ for (int idx2 = 0; idx2 < size_2; idx2++) {
+ if (array[idx1][idx2].length != size_2) {
+ throw new Error("Array initilizatiion failed to assign to all of elements.");
+ }
+ for (int idx3 = 0; idx3 < size_3; idx3++) {
+ array[idx1][idx2][idx3] = value;
+ }
+ }
+ }
+ }
+
+ static void arrayinit(float array[][], int size_1, int size_2, float value) {
+
+ for (int idx1 = 0; idx1 < size_1; idx1++) {
+ if (array[idx1].length != size_2) {
+ throw new Error("Array initilizatiion failed to assign to all of elements.");
+ }
+ for (int idx2 = 0; idx2 < size_2; idx2++) {
+ array[idx1][idx2] = value;
+ }
+ }
+ }
+
+}
diff --git a/Robust/src/Tests/ssJava/mp3decoder/Decoder.java b/Robust/src/Tests/ssJava/mp3decoder/Decoder.java
index 94486847..12287b1c 100644
--- a/Robust/src/Tests/ssJava/mp3decoder/Decoder.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/Decoder.java
@@ -127,6 +127,35 @@ public class Decoder implements DecoderErrors {
// if (filter2 != null)
// filter2.setEQ(factors);
// }
+ @LATTICE("THIS<VAR,THISLOC=THIS,VAR*")
+ public void init( @LOC("THIS,Decoder.H") Header header) {
+ @LOC("VAR") float scalefactor = 32700.0f;
+
+ @LOC("THIS,Decoder.PARAM") int mode = header.mode();
+ @LOC("THIS,Decoder.PARAM") int layer = header.layer();
+ @LOC("THIS,Decoder.PARAM") int channels = mode == Header.SINGLE_CHANNEL ? 1 : 2;
+
+ // set up output buffer if not set up by client.
+ // if (output == null)
+ // output = new SampleBuffer(header.frequency(), channels);
+ SampleBufferWrapper.init(header.frequency(), channels);
+
+ @LOC("THIS,Decoder.FACTORS") float[] factors = equalizer.getBandFactors();
+ @LOC("THIS,Decoder.FILTER") SynthesisFilter filter1 =
+ new SynthesisFilter(0, scalefactor, factors);
+
+ // REVIEW: allow mono output for stereo
+ @LOC("THIS,Decoder.FILTER") SynthesisFilter filter2 = null;
+ if (channels == 2) {
+ filter2 = new SynthesisFilter(1, scalefactor, factors);
+ }
+
+ outputChannels = channels;
+ outputFrequency = header.frequency();
+
+ l3decoder = new LayerIIIDecoder(header,filter1, filter2, OutputChannels.BOTH_CHANNELS);
+
+ }
/**
* Decodes one frame from an MPEG audio bitstream.
@@ -141,36 +170,6 @@ public class Decoder implements DecoderErrors {
@LATTICE("THIS<VAR,THISLOC=THIS,VAR*")
public void decodeFrame(@LOC("THIS,Decoder.H") Header header) throws DecoderException {
- if (!initialized) {
- @LOC("VAR") float scalefactor = 32700.0f;
-
- @LOC("THIS,Decoder.PARAM") int mode = header.mode();
- @LOC("THIS,Decoder.PARAM") int layer = header.layer();
- @LOC("THIS,Decoder.PARAM") int channels = mode == Header.SINGLE_CHANNEL ? 1 : 2;
-
- // set up output buffer if not set up by client.
- // if (output == null)
- // output = new SampleBuffer(header.frequency(), channels);
- SampleBufferWrapper.init(header.frequency(), channels);
-
- @LOC("THIS,Decoder.FACTORS") float[] factors = equalizer.getBandFactors();
- @LOC("THIS,Decoder.FILTER") SynthesisFilter filter1 =
- new SynthesisFilter(0, scalefactor, factors);
-
- // REVIEW: allow mono output for stereo
- @LOC("THIS,Decoder.FILTER") SynthesisFilter filter2 = null;
- if (channels == 2) {
- filter2 = new SynthesisFilter(1, scalefactor, factors);
- }
-
- outputChannels = channels;
- outputFrequency = header.frequency();
-
- l3decoder = new LayerIIIDecoder(filter1, filter2, OutputChannels.BOTH_CHANNELS);
-
- initialized = true;
- }
-
SampleBufferWrapper.clear_buffer();
l3decoder.decode(header);
// SampleBufferWrapper.getOutput().write_buffer(1);
diff --git a/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java b/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
index 8714428b..602ea5b1 100644
--- a/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
@@ -113,7 +113,7 @@ final class LayerIIIDecoder implements FrameDecoder {
private boolean initialized = false;
// constructor for the linear type system
- public LayerIIIDecoder(@DELEGATE @LOC("VAR") SynthesisFilter filtera,
+ public LayerIIIDecoder(Header h, @DELEGATE @LOC("VAR") SynthesisFilter filtera,
@DELEGATE @LOC("VAR") SynthesisFilter filterb, @LOC("VAR") int which_ch0) {
filter1 = filtera;
@@ -205,6 +205,7 @@ final class LayerIIIDecoder implements FrameDecoder {
scalefac_buffer = new int[54];
// END OF scalefac_buffer
+ init(h);
}
@LATTICE("THIS<C,THIS<IN,C*,THISLOC=THIS")
@@ -456,13 +457,22 @@ final class LayerIIIDecoder implements FrameDecoder {
@LATTICE("HEADER<VAR,VAR<THIS,C<THIS,THIS<IN,THISLOC=THIS,C*,VAR*")
public void decode(@LOC("THIS,LayerIIIDecoder.HD") Header header) {
- if (!initialized) {
- init(header);
- }
+ // if (!initialized) {
+ // init(header);
+ // }
// overwrites once per a loop
- samples1 = new float[32];
- samples2 = new float[32];
+ SSJAVA.arrayinit(samples1, 0);
+ SSJAVA.arrayinit(samples2, 0);
+ SSJAVA.arrayinit(ro, 2, SBLIMIT, SSLIMIT, 0);
+ SSJAVA.arrayinit(lr, 2, SBLIMIT, SSLIMIT, 0);
+ SSJAVA.arrayinit(is_pos, 7);
+ SSJAVA.arrayinit(is_ratio, 0);
+ SSJAVA.arrayinit(out_1d, 0);
+ SSJAVA.arrayinit(inter, 0);
+ SSJAVA.arrayinit(k, 2, SBLIMIT * SSLIMIT, 0);
+ SSJAVA.arrayinit(is_1d, 0);
+ CheckSumHuff = 0;
// prevblck = new float[2][SBLIMIT * SSLIMIT];
si = new III_side_info_t();
//
@@ -1379,9 +1389,9 @@ final class LayerIIIDecoder implements FrameDecoder {
if ((si.ch[ch].gr[gr].window_switching_flag != 0) && (si.ch[ch].gr[gr].block_type == 2)) {
- for (index = 0; index < 576; index++) {
- inter[index] = 0.0f;
- }
+ // for (index = 0; index < 576; index++) {
+ // inter[index] = 0.0f;
+ // }
if (si.ch[ch].gr[gr].mixed_block_flag != 0) {
// NO REORDER FOR LOW 2 SUBBANDS
@@ -1495,12 +1505,10 @@ final class LayerIIIDecoder implements FrameDecoder {
@LOC("THIS,LayerIIIDecoder.LR") int io_type = (si.ch[0].gr[gr].scalefac_compress & 1);
// initialization
-
- for (i = 0; i < 576; i++) {
- is_pos[i] = 7;
-
- is_ratio[i] = 0.0f;
- }
+ // for (i = 0; i < 576; i++) {
+ // is_pos[i] = 7;
+ // is_ratio[i] = 0.0f;
+ // }
if (i_stereo) {
if ((si.ch[0].gr[gr].window_switching_flag != 0) && (si.ch[0].gr[gr].block_type == 2)) {
diff --git a/Robust/src/Tests/ssJava/mp3decoder/Player.java b/Robust/src/Tests/ssJava/mp3decoder/Player.java
index d82e6e89..e3a92107 100644
--- a/Robust/src/Tests/ssJava/mp3decoder/Player.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/Player.java
@@ -107,16 +107,22 @@ public class Player {
* @return true if the last frame was played, or false if there are more
* frames.
*/
- @LATTICE("T<IN,T*,IN*,THISLOC=T")
- @RETURNLOC("T")
+ @LATTICE("OUT<THIS,THIS<IN,IN*,THISLOC=THIS")
+ @RETURNLOC("OUT")
public boolean play(@LOC("IN") int frames) throws JavaLayerException {
- @LOC("T") boolean ret = true;
-
- @LOC("T") int count=0;
+ @LOC("OUT") boolean ret = true;
+
+ // initialization before ssjava loop
+ @LOC("THIS,Player.FR") boolean init = true;
+ @LOC("THIS,Player.ST") Header h = BitstreamWrapper.readFrame();
+ decoder.init(h);
+
+ @LOC("IN") int count = 0;
SSJAVA: while (count++ < 2147483646) {
- ret = decodeFrame();
- if(!ret){
- break;
+ ret = decodeFrame(init, h);
+ init = false;
+ if (!ret) {
+ break;
}
}
@@ -175,14 +181,17 @@ public class Player {
* @return true if there are no more frames to decode, false otherwise.
*/
@LATTICE("C<THIS,O<THIS,THIS<IN,C*,THISLOC=THIS,RETURNLOC=O,GLOBALLOC=THIS")
- protected boolean decodeFrame() throws JavaLayerException {
+ protected boolean decodeFrame(@LOC("THIS,Player.FR") boolean init, @LOC("THIS,Player.ST") Header h)
+ throws JavaLayerException {
try {
// AudioDevice out = audio;
// if (out==null)
// return false;
// Header h = bitstream.readFrame();
- @LOC("THIS,Player.ST") Header h = BitstreamWrapper.readFrame();
+ if (!init) {
+ h = BitstreamWrapper.readFrame();
+ }
if (h == null)
return false;
@@ -194,8 +203,7 @@ public class Player {
@LOC("C") int sum = 0;
@LOC("C") short[] outbuf = SampleBufferWrapper.getBuffer();
// short[] outbuf = output.getBuffer();
- TERMINATE:
- for (@LOC("C") int i = 0; i < SampleBufferWrapper.getBufferLength(); i++) {
+ TERMINATE: for (@LOC("C") int i = 0; i < SampleBufferWrapper.getBufferLength(); i++) {
// System.out.println(outbuf[i]);
sum += outbuf[i];
}