import java.util.StringTokenizer;
import java.util.Vector;
-
import Analysis.SSJava.FlowDownCheck.ComparisonResult;
import Analysis.SSJava.FlowDownCheck.CompositeLattice;
import IR.AnnotationDescriptor;
while (!toAnalyzeMethodIsEmpty()) {
MethodDescriptor md = toAnalyzeMethodNext();
if (ssjava.needTobeAnnotated(md)) {
+ System.out.println("SSJAVA: Checking assignments: " + md);
checkMethodBody(cd, md);
}
}
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<CompositeLocation> paramList = new ArrayList<CompositeLocation>();
+ 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<AnnotationDescriptor> methodAnnotations = md.getModifiers().getAnnotations();
if (methodAnnotations != null) {
for (int i = 0; i < methodAnnotations.size(); i++) {
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<CompositeLocation> paramList = new ArrayList<CompositeLocation>();
-
- boolean hasReturnValue = (!md.getReturnType().isVoid());
- if (hasReturnValue) {
- MethodLattice<String> 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<String> 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<String> 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) {
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<CompositeLocation> inputGLB = new HashSet<CompositeLocation>();
+ 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);
System.out.println("SSJAVA: SSJava is checking the following methods:");
for (Iterator<MethodDescriptor> iterator = annotationRequireSet.iterator(); iterator.hasNext();) {
MethodDescriptor md = iterator.next();
- System.out.println("SSJAVA: " + md);
+ System.out.print(" " + md);
}
+ System.out.println();
}
private void doMethodAnnotationCheck() {
MethodLattice<String> locOrder =
new MethodLattice<String>(SSJavaLattice.TOP, SSJavaLattice.BOTTOM);
cd2methodDefault.put(cd, locOrder);
- parseMethodLatticeDefinition(cd, an.getValue(), locOrder);
+ parseMethodDefaultLatticeDefinition(cd, an.getValue(), locOrder);
}
}
MethodLattice<String> locOrder =
new MethodLattice<String>(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();
}
}
- private void parseMethodLatticeDefinition(ClassDescriptor cd, String value,
+ private void parseMethodDefaultLatticeDefinition(ClassDescriptor cd, String value,
MethodLattice<String> locOrder) {
value = value.replaceAll(" ", ""); // remove all blank spaces
} 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));
* Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.\r
*----------------------------------------------------------------------\r
*/\r
- \r
+\r
/**\r
* Implementation of Bit Reservoir for Layer III.\r
* <p>\r
- * The implementation stores single bits as a word in the buffer. If\r
- * a bit is set, the corresponding word in the buffer will be non-zero.\r
- * If a bit is clear, the corresponding word is zero. Although this\r
- * may seem waseful, this can be a factor of two quicker than \r
- * packing 8 bits to a byte and extracting. \r
- * <p> \r
+ * The implementation stores single bits as a word in the buffer. If a bit is\r
+ * set, the corresponding word in the buffer will be non-zero. If a bit is\r
+ * clear, the corresponding word is zero. Although this may seem waseful, this\r
+ * can be a factor of two quicker than packing 8 bits to a byte and extracting.\r
+ * <p>\r
*/\r
\r
// REVIEW: there is no range checking, so buffer underflow or overflow\r
// can silently occur.\r
-@LATTICE("SH<V,V<T,TOT<OFF,OFF<T,SH*,TOT*,OFF*")\r
-@METHODDEFAULT("OUT<V,V<C,C<IN,C*,THISLOC=V,GLOBALLOC=V")\r
-final class BitReserve\r
-{\r
- /**\r
- * Size of the internal buffer to store the reserved bits.\r
- * Must be a power of 2. And x8, as each bit is stored as a single\r
- * entry.\r
- */\r
- @LOC("T") private static final int BUFSIZE = 4096*8;\r
- \r
- /**\r
- * Mask that can be used to quickly implement the\r
- * modulus operation on BUFSIZE.\r
- */\r
- @LOC("V") private static final int BUFSIZE_MASK = BUFSIZE-1;\r
- \r
- @LOC("OFF") private int offset;\r
- @LOC("TOT") private int totbit;\r
- @LOC("SH") private int buf_byte_idx;\r
- @LOC("V") private final int[] buf;\r
- @LOC("T") private int buf_bit_idx;\r
- \r
- BitReserve()\r
- { \r
+@LATTICE("BUF<OFF,BIT,BIT*,OFF*")\r
+@METHODDEFAULT("OUT<THIS,THIS<IN,IN*,THISLOC=THIS,RETURNLOC=OUT")\r
+final class BitReserve {\r
+ /**\r
+ * Size of the internal buffer to store the reserved bits. Must be a power of\r
+ * 2. And x8, as each bit is stored as a single entry.\r
+ */\r
+ private static final int BUFSIZE = 4096 * 8;\r
+\r
+ /**\r
+ * Mask that can be used to quickly implement the modulus operation on\r
+ * BUFSIZE.\r
+ */\r
+ private static final int BUFSIZE_MASK = BUFSIZE - 1;\r
+\r
+ @LOC("OFF")\r
+ private int offset;\r
+\r
+ @LOC("BIT")\r
+ private int totbit;\r
+\r
+ @LOC("BIT")\r
+ private int buf_byte_idx;\r
+\r
+ @LOC("BUF")\r
+ private final int[] buf;\r
+\r
+ BitReserve() {\r
+ offset = 0;\r
+ totbit = 0;\r
+ buf_byte_idx = 0;\r
+ buf = new int[BUFSIZE];\r
+ }\r
+\r
+ /**\r
+ * Return totbit Field.\r
+ */\r
+\r
+ public int hsstell() {\r
+ return (totbit);\r
+ }\r
+\r
+ /**\r
+ * Read a number bits from the bit stream.\r
+ * \r
+ * @param N\r
+ * the number of\r
+ */\r
+ public int hgetbits(@LOC("THIS,BitReserve.BIT") int N) {\r
+\r
+ totbit += N;\r
+\r
+ @LOC("OUT") int val = 0;\r
+\r
+ @LOC("THIS,BitReserve.BIT") int pos = buf_byte_idx;\r
+ if (pos + N < BUFSIZE) {\r
+ while (N-- > 0) {\r
+ val <<= 1;\r
+ val |= ((buf[pos++] != 0) ? 1 : 0);\r
+ }\r
+ } else {\r
+ while (N-- > 0) {\r
+ val <<= 1;\r
+ val |= ((buf[pos] != 0) ? 1 : 0);\r
+ pos = (pos + 1) & BUFSIZE_MASK;\r
+ }\r
+ }\r
+\r
+ buf_byte_idx = pos;\r
+\r
+ return val;\r
+\r
+ }\r
+\r
+ /**\r
+ * Returns next bit from reserve.\r
+ * \r
+ * @returns 0 if next bit is reset, or 1 if next bit is set.\r
+ */\r
+ public int hget1bit() {\r
+ totbit++;\r
+ @LOC("OUT") int val = buf[buf_byte_idx];\r
+ buf_byte_idx = (buf_byte_idx + 1) & BUFSIZE_MASK;\r
+ return val;\r
+ }\r
+\r
+ /**\r
+ * Write 8 bits into the bit stream.\r
+ */\r
+ @LATTICE("OUT<THIS,THIS<IN,THISLOC=THIS,GLOBALLOC=IN")\r
+ public void hputbuf(@LOC("IN") int val) {\r
+ @LOC("THIS,BitReserve.OFF") int ofs = offset;\r
+ buf[ofs++] = val & 0x80;\r
+ buf[ofs++] = val & 0x40;\r
+ buf[ofs++] = val & 0x20;\r
+ buf[ofs++] = val & 0x10;\r
+ buf[ofs++] = val & 0x08;\r
+ buf[ofs++] = val & 0x04;\r
+ buf[ofs++] = val & 0x02;\r
+ buf[ofs++] = val & 0x01;\r
+\r
+ if (ofs == BUFSIZE)\r
offset = 0;\r
- totbit = 0;\r
- buf_byte_idx = 0;\r
- buf = new int[BUFSIZE];\r
- }\r
- \r
- \r
- /**\r
- * Return totbit Field.\r
- */\r
-\r
- @RETURNLOC("OUT")\r
- public int hsstell() \r
- { \r
- return(totbit); \r
- }\r
-\r
- /**\r
- * Read a number bits from the bit stream.\r
- * @param N the number of\r
- */\r
- @LATTICE("OUT<SH,SH<THIS,THIS<C,C<GLOBAL,C*,SH*,THISLOC=THIS,GLOBALLOC=GLOBAL")\r
- @RETURNLOC("OUT") \r
- public int hgetbits(@LOC("C") int N)\r
- {\r
- totbit += N;\r
- \r
- @LOC("SH") int val = 0;\r
- \r
- @LOC("THIS,BitReserve.SH") int pos = buf_byte_idx;\r
- if (pos+N < BUFSIZE)\r
- {\r
- while (N-- > 0)\r
- {\r
- val <<= 1;\r
- val |= ((buf[pos++]!=0) ? 1 : 0); \r
- }\r
- }\r
- else\r
- { \r
- while (N-- > 0)\r
- {\r
- val <<= 1; \r
- val |= ((buf[pos]!=0) ? 1 : 0);\r
- pos = (pos+1) & BUFSIZE_MASK;\r
- } \r
- } \r
- buf_byte_idx = pos;\r
- return val;\r
- }\r
- \r
- \r
- \r
- /**\r
- * Read 1 bit from the bit stream.\r
- */\r
-/*\r
- public int hget1bit_old()\r
- {\r
- int val;\r
- totbit++;\r
- if (buf_bit_idx == 0)\r
- {\r
- buf_bit_idx = 8;\r
- buf_byte_idx++; \r
- }\r
- // BUFSIZE = 4096 = 2^12, so\r
- // buf_byte_idx%BUFSIZE == buf_byte_idx & 0xfff\r
- val = buf[buf_byte_idx & BUFSIZE_MASK] & putmask[buf_bit_idx];\r
- buf_bit_idx--;\r
- val = val >>> buf_bit_idx;\r
- return val; \r
- }\r
- */\r
- /**\r
- * Returns next bit from reserve.\r
- * @returns 0 if next bit is reset, or 1 if next bit is set.\r
- */\r
- @RETURNLOC("OUT")\r
- public int hget1bit()\r
- { \r
- totbit++; \r
- @LOC("OUT") int val = buf[buf_byte_idx];\r
- buf_byte_idx = (buf_byte_idx+1) & BUFSIZE_MASK;\r
- return val;\r
- }\r
- \r
- /**\r
- * Retrieves bits from the reserve. \r
- */\r
-/* \r
- public int readBits(int[] out, int len)\r
- {\r
- if (buf_bit_idx == 0)\r
- {\r
- buf_bit_idx = 8;\r
- buf_byte_idx++;\r
- current = buf[buf_byte_idx & BUFSIZE_MASK];\r
- } \r
- \r
- \r
- \r
- // save total number of bits returned\r
- len = buf_bit_idx;\r
- buf_bit_idx = 0;\r
- \r
- int b = current;\r
- int count = len-1;\r
- \r
- while (count >= 0)\r
- {\r
- out[count--] = (b & 0x1);\r
- b >>>= 1;\r
- }\r
- \r
- totbit += len;\r
- return len;\r
- }\r
- */\r
- \r
- /**\r
- * Write 8 bits into the bit stream.\r
- */\r
- @LATTICE("OUT<THIS,THIS<IN,THISLOC=THIS,GLOBALLOC=IN")\r
- public void hputbuf(@LOC("IN") int val)\r
- { \r
- @LOC("THIS,BitReserve.OFF") int ofs = offset;\r
- buf[ofs++] = val & 0x80;\r
- buf[ofs++] = val & 0x40;\r
- buf[ofs++] = val & 0x20;\r
- buf[ofs++] = val & 0x10;\r
- buf[ofs++] = val & 0x08;\r
- buf[ofs++] = val & 0x04;\r
- buf[ofs++] = val & 0x02;\r
- buf[ofs++] = val & 0x01;\r
- \r
- if (ofs==BUFSIZE)\r
- offset = 0;\r
- else\r
- offset = ofs;\r
- \r
- }\r
- \r
- /**\r
- * Rewind N bits in Stream.\r
- */\r
- public void rewindNbits(@LOC("IN") int N)\r
- {\r
- totbit -= N; \r
- buf_byte_idx -= N;\r
- if (buf_byte_idx<0)\r
- buf_byte_idx += BUFSIZE;\r
- }\r
- \r
- /**\r
- * Rewind N bytes in Stream.\r
- */\r
- @LATTICE("THIS<BIT,BIT<N,THISLOC=THIS,GLOBALLOC=N")\r
- public void rewindNbytes(@LOC("N") int N)\r
- {\r
- @LOC("BIT") int bits = (N << 3);\r
- totbit -= bits;\r
- buf_byte_idx -= bits; \r
- if (buf_byte_idx<0)\r
- buf_byte_idx += BUFSIZE;\r
- }\r
+ else\r
+ offset = ofs;\r
+\r
+ }\r
+\r
+ /**\r
+ * Rewind N bits in Stream.\r
+ */\r
+ public void rewindNbits(@LOC("IN") int N) {\r
+ totbit -= N;\r
+ buf_byte_idx -= N;\r
+ if (buf_byte_idx < 0)\r
+ buf_byte_idx += BUFSIZE;\r
+ }\r
+\r
+ /**\r
+ * Rewind N bytes in Stream.\r
+ */\r
+ @LATTICE("THIS<BIT,BIT<N,THISLOC=THIS,GLOBALLOC=N")\r
+ public void rewindNbytes(@LOC("N") int N) {\r
+ @LOC("BIT") int bits = (N << 3);\r
+ totbit -= bits;\r
+ buf_byte_idx -= bits;\r
+ if (buf_byte_idx < 0)\r
+ buf_byte_idx += BUFSIZE;\r
+ }\r
}\r
projects / IRC.git / commitdiff