From ed82760e308e352225afca7e119b4fdeffda0a2f Mon Sep 17 00:00:00 2001 From: yeom Date: Sat, 23 Jul 2011 00:13:36 +0000 Subject: [PATCH] changes. --- Robust/src/Analysis/SSJava/FlowDownCheck.java | 78 +++-- Robust/src/Analysis/SSJava/MethodLattice.java | 9 + .../src/Analysis/SSJava/SSJavaAnalysis.java | 12 +- .../Tests/ssJava/mp3decoder/BitReserve.java | 331 +++++++----------- 4 files changed, 196 insertions(+), 234 deletions(-) diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java index 0a1752c6..f1133415 100644 --- a/Robust/src/Analysis/SSJava/FlowDownCheck.java +++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java @@ -11,7 +11,6 @@ import java.util.Set; import java.util.StringTokenizer; import java.util.Vector; - import Analysis.SSJava.FlowDownCheck.ComparisonResult; import Analysis.SSJava.FlowDownCheck.CompositeLattice; import IR.AnnotationDescriptor; @@ -222,6 +221,7 @@ public class FlowDownCheck { while (!toAnalyzeMethodIsEmpty()) { MethodDescriptor md = toAnalyzeMethodNext(); if (ssjava.needTobeAnnotated(md)) { + System.out.println("SSJAVA: Checking assignments: " + md); checkMethodBody(cd, md); } } @@ -292,10 +292,18 @@ public class FlowDownCheck { private void checkDeclarationInMethodBody(ClassDescriptor cd, MethodDescriptor md) { BlockNode bn = state.getMethodBody(md); - if (ssjava.needTobeAnnotated(md)) { - // first, check annotations on method declaration + // first, check annotations on method parameters + List paramList = new ArrayList(); + for (int i = 0; i < md.numParameters(); i++) { + // process annotations on method parameters + VarDescriptor vd = (VarDescriptor) md.getParameter(i); + assignLocationOfVarDescriptor(vd, md, md.getParameterTable(), bn); + paramList.add(d2loc.get(vd)); + } - // parsing returnloc annotation + // second, check return location annotation + if (!md.getReturnType().isVoid()) { + CompositeLocation returnLocComp = null; Vector methodAnnotations = md.getModifiers().getAnnotations(); if (methodAnnotations != null) { for (int i = 0; i < methodAnnotations.size(); i++) { @@ -303,47 +311,42 @@ public class FlowDownCheck { if (an.getMarker().equals(ssjava.RETURNLOC)) { // developer explicitly defines method lattice String returnLocDeclaration = an.getValue(); - CompositeLocation returnLocComp = - parseLocationDeclaration(md, null, returnLocDeclaration); + returnLocComp = parseLocationDeclaration(md, null, returnLocDeclaration); md2ReturnLoc.put(md, returnLocComp); } } - if (!md.getReturnType().isVoid() && !md2ReturnLoc.containsKey(md)) { - throw new Error("Return location is not specified for the method " + md + " at " - + cd.getSourceFileName()); - } } - - List paramList = new ArrayList(); - - boolean hasReturnValue = (!md.getReturnType().isVoid()); - if (hasReturnValue) { - MethodLattice methodLattice = ssjava.getMethodLattice(md); - String thisLocId = methodLattice.getThisLoc(); - if (thisLocId == null) { - throw new Error("Method '" + md + "' does not have the definition of 'this' location at " - + md.getClassDesc().getSourceFileName()); + if (returnLocComp == null) { + MethodLattice methodDefaultLattice = ssjava.getMethodDefaultLattice(cd); + if (methodDefaultLattice.getReturnLoc() != null) { + returnLocComp = parseLocationDeclaration(md, null, methodDefaultLattice.getReturnLoc()); + md2ReturnLoc.put(md, returnLocComp); } - CompositeLocation thisLoc = new CompositeLocation(new Location(md, thisLocId)); - paramList.add(thisLoc); } - for (int i = 0; i < md.numParameters(); i++) { - // process annotations on method parameters - VarDescriptor vd = (VarDescriptor) md.getParameter(i); - assignLocationOfVarDescriptor(vd, md, md.getParameterTable(), bn); - if (hasReturnValue) { - paramList.add(d2loc.get(vd)); - } + if (!md2ReturnLoc.containsKey(md)) { + throw new Error("Return location is not specified for the method " + md + " at " + + cd.getSourceFileName()); } - if (hasReturnValue) { - md2ReturnLocGen.put(md, new ReturnLocGenerator(md2ReturnLoc.get(md), paramList, - generateErrorMessage(cd, null))); + // check this location + MethodLattice methodLattice = ssjava.getMethodLattice(md); + String thisLocId = methodLattice.getThisLoc(); + if (thisLocId == null) { + throw new Error("Method '" + md + "' does not have the definition of 'this' location at " + + md.getClassDesc().getSourceFileName()); } - checkDeclarationInBlockNode(md, md.getParameterTable(), bn); + CompositeLocation thisLoc = new CompositeLocation(new Location(md, thisLocId)); + paramList.add(0, thisLoc); + + md2ReturnLocGen.put(md, new ReturnLocGenerator(md2ReturnLoc.get(md), paramList, + generateErrorMessage(cd, null))); } + // third, check declarations inside of method + + checkDeclarationInBlockNode(md, md.getParameterTable(), bn); + } private void checkDeclarationInBlockNode(MethodDescriptor md, SymbolTable nametable, BlockNode bn) { @@ -528,6 +531,15 @@ public class FlowDownCheck { checkLocationFromExpressionNode(md, nametable, returnExp, new CompositeLocation(), constraint, false); + // if this return statement is inside branch, return value has an implicit + // flow from conditional location + if (constraint != null) { + Set inputGLB = new HashSet(); + inputGLB.add(returnValueLoc); + inputGLB.add(constraint); + returnValueLoc = CompositeLattice.calculateGLB(inputGLB); + } + // check if return value is equal or higher than RETRUNLOC of method // declaration annotation CompositeLocation declaredReturnLoc = md2ReturnLoc.get(md); diff --git a/Robust/src/Analysis/SSJava/MethodLattice.java b/Robust/src/Analysis/SSJava/MethodLattice.java index 095c736e..88eb7b70 100644 --- a/Robust/src/Analysis/SSJava/MethodLattice.java +++ b/Robust/src/Analysis/SSJava/MethodLattice.java @@ -4,6 +4,7 @@ public class MethodLattice extends SSJavaLattice { private T thisLoc; private T globalLoc; + private T returnLoc; public MethodLattice(T top, T bottom) { super(top, bottom); @@ -25,4 +26,12 @@ public class MethodLattice extends SSJavaLattice { return globalLoc; } + public void setReturnLoc(T returnLoc) { + this.returnLoc = returnLoc; + } + + public T getReturnLoc() { + return returnLoc; + } + } diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java index 17db8a82..5e0d556f 100644 --- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java +++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java @@ -88,8 +88,9 @@ public class SSJavaAnalysis { System.out.println("SSJAVA: SSJava is checking the following methods:"); for (Iterator iterator = annotationRequireSet.iterator(); iterator.hasNext();) { MethodDescriptor md = iterator.next(); - System.out.println("SSJAVA: " + md); + System.out.print(" " + md); } + System.out.println(); } private void doMethodAnnotationCheck() { @@ -131,7 +132,7 @@ public class SSJavaAnalysis { MethodLattice locOrder = new MethodLattice(SSJavaLattice.TOP, SSJavaLattice.BOTTOM); cd2methodDefault.put(cd, locOrder); - parseMethodLatticeDefinition(cd, an.getValue(), locOrder); + parseMethodDefaultLatticeDefinition(cd, an.getValue(), locOrder); } } @@ -149,7 +150,7 @@ public class SSJavaAnalysis { MethodLattice locOrder = new MethodLattice(SSJavaLattice.TOP, SSJavaLattice.BOTTOM); md2lattice.put(md, locOrder); - parseMethodLatticeDefinition(cd, an.getValue(), locOrder); + parseMethodDefaultLatticeDefinition(cd, an.getValue(), locOrder); } else if (an.getMarker().equals(TERMINATE)) { // developer explicitly wants to skip loop termination analysis String value = an.getValue(); @@ -169,7 +170,7 @@ public class SSJavaAnalysis { } } - private void parseMethodLatticeDefinition(ClassDescriptor cd, String value, + private void parseMethodDefaultLatticeDefinition(ClassDescriptor cd, String value, MethodLattice locOrder) { value = value.replaceAll(" ", ""); // remove all blank spaces @@ -193,6 +194,9 @@ public class SSJavaAnalysis { } else if (orderElement.startsWith(GLOBALLOC + "=")) { String globalLoc = orderElement.substring(10); locOrder.setGlobalLoc(globalLoc); + } else if (orderElement.startsWith(RETURNLOC + "=")) { + String returnLoc = orderElement.substring(10); + locOrder.setReturnLoc(returnLoc); } else if (orderElement.contains("*")) { // spin loc definition locOrder.addSpinLoc(orderElement.substring(0, orderElement.length() - 1)); diff --git a/Robust/src/Tests/ssJava/mp3decoder/BitReserve.java b/Robust/src/Tests/ssJava/mp3decoder/BitReserve.java index 3c907a79..4f558216 100644 --- a/Robust/src/Tests/ssJava/mp3decoder/BitReserve.java +++ b/Robust/src/Tests/ssJava/mp3decoder/BitReserve.java @@ -24,209 +24,146 @@ * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. *---------------------------------------------------------------------- */ - + /** * Implementation of Bit Reservoir for Layer III. *

- * The implementation stores single bits as a word in the buffer. If - * a bit is set, the corresponding word in the buffer will be non-zero. - * If a bit is clear, the corresponding word is zero. Although this - * may seem waseful, this can be a factor of two quicker than - * packing 8 bits to a byte and extracting. - *

+ * The implementation stores single bits as a word in the buffer. If a bit is + * set, the corresponding word in the buffer will be non-zero. If a bit is + * clear, the corresponding word is zero. Although this may seem waseful, this + * can be a factor of two quicker than packing 8 bits to a byte and extracting. + *

*/ // REVIEW: there is no range checking, so buffer underflow or overflow // can silently occur. -@LATTICE("SH 0) { + val <<= 1; + val |= ((buf[pos++] != 0) ? 1 : 0); + } + } else { + while (N-- > 0) { + val <<= 1; + val |= ((buf[pos] != 0) ? 1 : 0); + pos = (pos + 1) & BUFSIZE_MASK; + } + } + + buf_byte_idx = pos; + + return val; + + } + + /** + * Returns next bit from reserve. + * + * @returns 0 if next bit is reset, or 1 if next bit is set. + */ + public int hget1bit() { + totbit++; + @LOC("OUT") int val = buf[buf_byte_idx]; + buf_byte_idx = (buf_byte_idx + 1) & BUFSIZE_MASK; + return val; + } + + /** + * Write 8 bits into the bit stream. + */ + @LATTICE("OUT 0) - { - val <<= 1; - val |= ((buf[pos++]!=0) ? 1 : 0); - } - } - else - { - while (N-- > 0) - { - val <<= 1; - val |= ((buf[pos]!=0) ? 1 : 0); - pos = (pos+1) & BUFSIZE_MASK; - } - } - buf_byte_idx = pos; - return val; - } - - - - /** - * Read 1 bit from the bit stream. - */ -/* - public int hget1bit_old() - { - int val; - totbit++; - if (buf_bit_idx == 0) - { - buf_bit_idx = 8; - buf_byte_idx++; - } - // BUFSIZE = 4096 = 2^12, so - // buf_byte_idx%BUFSIZE == buf_byte_idx & 0xfff - val = buf[buf_byte_idx & BUFSIZE_MASK] & putmask[buf_bit_idx]; - buf_bit_idx--; - val = val >>> buf_bit_idx; - return val; - } - */ - /** - * Returns next bit from reserve. - * @returns 0 if next bit is reset, or 1 if next bit is set. - */ - @RETURNLOC("OUT") - public int hget1bit() - { - totbit++; - @LOC("OUT") int val = buf[buf_byte_idx]; - buf_byte_idx = (buf_byte_idx+1) & BUFSIZE_MASK; - return val; - } - - /** - * Retrieves bits from the reserve. - */ -/* - public int readBits(int[] out, int len) - { - if (buf_bit_idx == 0) - { - buf_bit_idx = 8; - buf_byte_idx++; - current = buf[buf_byte_idx & BUFSIZE_MASK]; - } - - - - // save total number of bits returned - len = buf_bit_idx; - buf_bit_idx = 0; - - int b = current; - int count = len-1; - - while (count >= 0) - { - out[count--] = (b & 0x1); - b >>>= 1; - } - - totbit += len; - return len; - } - */ - - /** - * Write 8 bits into the bit stream. - */ - @LATTICE("OUT