From 95ade08265a30f939a5f49aa3d25db6152d0e6fd Mon Sep 17 00:00:00 2001 From: yeom Date: Tue, 23 Aug 2011 23:19:05 +0000 Subject: [PATCH] 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 --- .../SSJava/DefinitelyWrittenCheck.java | 299 ++++++++++++------ Robust/src/Analysis/SSJava/FlowDownCheck.java | 18 +- .../SSJava/MethodAnnotationCheck.java | 2 +- .../src/Analysis/SSJava/SSJavaAnalysis.java | 21 +- Robust/src/ClassLibrary/SSJava/SSJAVA.java | 47 +++ .../src/Tests/ssJava/mp3decoder/Decoder.java | 59 ++-- .../ssJava/mp3decoder/LayerIIIDecoder.java | 38 ++- .../src/Tests/ssJava/mp3decoder/Player.java | 32 +- 8 files changed, 340 insertions(+), 176 deletions(-) create mode 100644 Robust/src/ClassLibrary/SSJava/SSJAVA.java 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>> mapFlatMethodToOverWrite; + // maps a flat method to the WRITE that is the set of heap path that is + // written to + private Hashtable>> mapFlatMethodToWrite; + // points to method containing SSJAVA Loop private MethodDescriptor methodContainingSSJavaLoop; @@ -98,6 +102,7 @@ public class DefinitelyWrittenCheck { private Set> calleeUnionBoundReadSet; private Set> calleeIntersectBoundOverWriteSet; + private Set> calleeBoundWriteSet; private TempDescriptor LOCAL; @@ -110,10 +115,12 @@ public class DefinitelyWrittenCheck { this.mapHeapPath = new Hashtable>(); this.mapFlatMethodToRead = new Hashtable>>(); this.mapFlatMethodToOverWrite = new Hashtable>>(); + this.mapFlatMethodToWrite = new Hashtable>>(); this.definitelyWrittenResults = new Hashtable, Hashtable>>(); this.calleeUnionBoundReadSet = new HashSet>(); this.calleeIntersectBoundOverWriteSet = new HashSet>(); + this.calleeBoundWriteSet = new HashSet>(); this.mapMethodDescriptorToCompleteClearingSummary = new Hashtable(); @@ -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> hpKeySet = result.keySet(); for (Iterator iterator = hpKeySet.iterator(); iterator.hasNext();) { NTuple hpKey = (NTuple) 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 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 fldHeapPath = new NTuple(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 setPossibleCallees = new HashSet(); - 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> mapArgIdx2CallerArgHeapPath = new Hashtable>(); - // arg idx is starting from 'this' arg - 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 (fc.getThis() != null) { + // arg idx is starting from 'this' arg + 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()); + } - 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 srcHeapPath = mapHeapPath.get(rhs); @@ -954,12 +993,13 @@ public class DefinitelyWrittenCheck { case FKind.FlatCall: { FlatCall fc = (FlatCall) fn; + bindHeapPathCallerArgWithCaleeParam(fc); // add in which hp is an element of // READ_bound set // of callee: callee has 'read' requirement! - + for (Iterator iterator = calleeUnionBoundReadSet.iterator(); iterator.hasNext();) { NTuple read = (NTuple) iterator.next(); Hashtable 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 setPossibleCallees = new HashSet(); - 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 argHeapPath = computePath(arg); + calleeIntersectBoundOverWriteSet.add(argHeapPath); + } else { + MethodDescriptor mdCallee = fc.getMethod(); + // FlatMethod fmCallee = state.getMethodFlat(mdCallee); + Set setPossibleCallees = new HashSet(); + // setPossibleCallees.addAll(callGraph.getMethods(mdCallee, typeDesc)); + setPossibleCallees.addAll(callGraph.getMethods(mdCallee)); - // create mapping from arg idx to its heap paths - Hashtable> mapArgIdx2CallerArgHeapPath = - new Hashtable>(); + // create mapping from arg idx to its heap paths + Hashtable> mapArgIdx2CallerArgHeapPath = + new Hashtable>(); - // arg idx is starting from 'this' arg - 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()); - } + // 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()); + } - 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 argHeapPath = computePath(arg); - mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(i + 1), argHeapPath); - } + for (int i = 0; i < fc.numArgs(); i++) { + TempDescriptor arg = fc.getArg(i); + NTuple 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> calleeReadSet = mapFlatMethodToRead.get(calleeFlatMethod); - if (calleeReadSet == null) { - calleeReadSet = new HashSet>(); - mapFlatMethodToRead.put(calleeFlatMethod, calleeReadSet); - } - Set> calleeOverWriteSet = mapFlatMethodToOverWrite.get(calleeFlatMethod); - if (calleeOverWriteSet == null) { - calleeOverWriteSet = new HashSet>(); - mapFlatMethodToOverWrite.put(calleeFlatMethod, calleeOverWriteSet); - } + Set> calleeReadSet = mapFlatMethodToRead.get(calleeFlatMethod); + if (calleeReadSet == null) { + calleeReadSet = new HashSet>(); + mapFlatMethodToRead.put(calleeFlatMethod, calleeReadSet); + } - Hashtable mapParamIdx2ParamTempDesc = - new Hashtable(); - for (int i = 0; i < calleeFlatMethod.numParameters(); i++) { - TempDescriptor param = calleeFlatMethod.getParameter(i); - mapParamIdx2ParamTempDesc.put(Integer.valueOf(i), param); + Set> calleeOverWriteSet = mapFlatMethodToOverWrite.get(calleeFlatMethod); + + if (calleeOverWriteSet == null) { + calleeOverWriteSet = new HashSet>(); + mapFlatMethodToOverWrite.put(calleeFlatMethod, calleeOverWriteSet); + } + + Set> calleeWriteSet = mapFlatMethodToWrite.get(calleeFlatMethod); + + if (calleeWriteSet == null) { + calleeWriteSet = new HashSet>(); + mapFlatMethodToWrite.put(calleeFlatMethod, calleeWriteSet); + } + + 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); + } + + Set> calleeBoundReadSet = + bindSet(calleeReadSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath); + // union of the current read set and the current callee's + // read set + calleeUnionBoundReadSet.addAll(calleeBoundReadSet); + Set> calleeBoundOverWriteSet = + bindSet(calleeOverWriteSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath); + // intersection of the current overwrite set and the current + // callee's + // overwrite set + merge(calleeIntersectBoundOverWriteSet, calleeBoundOverWriteSet); + + Set> boundWriteSetFromCallee = + bindSet(calleeWriteSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath); + calleeBoundWriteSet.addAll(boundWriteSetFromCallee); } - Set> calleeBoundReadSet = - bindSet(calleeReadSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath); - // union of the current read set and the current callee's - // read set - calleeUnionBoundReadSet.addAll(calleeBoundReadSet); - Set> 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 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 write = (NTuple) 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> readSet = new HashSet>(); Set> overWriteSet = new HashSet>(); + Set> writeSet = new HashSet>(); - methodReadOverWrite_analyzeMethod(fm, readSet, overWriteSet); + methodReadOverWrite_analyzeMethod(fm, readSet, overWriteSet, writeSet); Set> prevRead = mapFlatMethodToRead.get(fm); Set> prevOverWrite = mapFlatMethodToOverWrite.get(fm); + Set> 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> readSet, - Set> overWriteSet) { + Set> overWriteSet, Set> 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> writtenSetPrev = mapFlatNodeToWrittenSet.get(fn); if (!curr.equals(writtenSetPrev)) { @@ -1240,10 +1323,12 @@ public class DefinitelyWrittenCheck { } + } private void methodReadOverWrite_nodeActions(FlatNode fn, Set> writtenSet, - Set> readSet, Set> overWriteSet) { + Set> readSet, Set> overWriteSet, + Set> 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 read = (NTuple) 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 write = (NTuple) 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 read = (NTuple) 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 write = (NTuple) 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 write = (NTuple) iterator.next(); + writeSet.add(write); + } } break; @@ -1521,7 +1613,6 @@ public class DefinitelyWrittenCheck { NTuple callerArgHeapPath = mapCallerArgIdx2HeapPath.get(idx); TempDescriptor calleeParam = mapParamIdx2ParamTempDesc.get(idx); - for (Iterator iterator2 = calleeSet.iterator(); iterator2.hasNext();) { NTuple element = (NTuple) 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>(); this.linearTypeCheckMethodSet = new HashSet(); this.bf = bf; - trustWorthyMDSet = new HashSet(); + this.trustWorthyMDSet = new HashSet(); } 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 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