Java and the Java Virtual Machine (R. Stärk, J. Schmid, E. Börger)

Jbook Frequently Asked Questions and Answers

We list the questions by increasing page numbers. Click on the page number to jump to the corresponding answer.
Page(s) Problem
35, 42 Figure 3.1 and Figure 3.3: Labels can appear anywhere. Thus, the function up and sub-statements must be clearly defined.
40 What is the meaning of restbody[result/up(pos)]?
42, 43 How is Abr propagated upward in if and while statements?
44 Are the reductions for assignment operators on page 44 valid for arbitrary lvalues?
50 The introduction states that JavaC uses only static features, but Section 4.1.2 introduces non-static features (i.e. instance features).
52 Item 1 and Item 2: Same sentence "Let app(alpha) be the set ... such that" is confusing.
61-65 The function body must update the nullary global body.
64 Is there a need for primitive constant definitions?
65 invokeMethod need invokeNative which is defined in JavaT.
79 Declaration of defaultVal and type already used in the definition of initialize on Page 64.
239 The phrase "The verify type unusable is allowed ... but not as the type of a register" is in Definition 16.3.8. Why not prefixed by T9? Where does this restriction come from?
242 The page states that "A compiler for Java, however, had to use more local registers for storing return values and for storing exceptions in default handlers." Why?

Answers

Page 35 and Page 42 (Figure 3.1 and Figure 3.3): Labels can appear anywhere. Thus, the function up and substatements must be clearly defined.

A labeled statement lab: stm is represented in the abstract syntax tree as a node with label lab which has exactly one child, the abstract syntax tree for stm. The function up returns the parent position. Substatements are subtrees.

Page 40: What is the meaning of restbody[result/up(pos)]?

We have defined it as the result of replacing in restbody the subtree at position up(pos) by result.

Page 42 and Page 43: How is Abr propagated upward in if and while statements?

These cases are covered by the case phrase(-> abr) in Figure 3.3, because if and while statements propagate abruptions (see function propagateAbr).

Page 44: Are the reductions for assignment operators on page 44 valid for arbitrary lvalues?

No. The reductions of assignment operators in page 44 as well as the reductions of pre-increment and pre-decrement expressions in Table 3.6 are valid only for local variables. The reductions cannot be applied to array access expressions and field access expressions. Cases like ++exp1[exp2], exp1[exp2] += exp3, ++exp.field, exp1.field += exp2 require their own ASM rules.

Page 50: The introduction states that JavaC uses only static features, but Section 4.1.2 introduces non-static features (i.e. instance features).

From the point of view of presentation, we found it more economic to formulate the syntactic constraints for JavaC and JavaO in one blow. However, the dynamic semantics for JavaC does not have non-static features.

Page 52:
Item 1 and Item 2: Same sentence "Let app(alpha) be the set ... such that" is confusing.

Item 1 and Item 2 refer to the two different kinds of method invocations (at the bottom of Page 58).

Page 61-65: The function body must update the nullary global body.

The function body is a static function, it is never updated. Given a method signature, it provides the code for the method. We assume for JavaI that there is some (hidden) methond main and body(main) returns the code of the JavaI program.

Page 64: Is there a need for primitive constant definitions?

Yes. Primitive constants are inlined by the compiler. Hence, they do not trigger class initialization. However, the Java Language Specification does not cover the case of recursive definitions of final static fields.

Page 65: invokeMethod need invokeNative which is defined in JavaT.

Right. We assume that each of JavaC, JavaO, JavaE, JavaT has its own invokeNative. Only the invokeNative of JavaT is displayed in the book (for thread methods).

Page 79: Declaration of defaultVal and type already used in the definition of initialize on Page 64.

True, but on Page 64 we did not want to break the flow of explanations by the definitions of defaultVal and type. This happens in various places and is the reason why in the index one finds a reference to the definition of such terms. ;-)

Page 239: The phrase "The verify type unusable is allowed ... but not as the type of a register" is in Definition 16.3.8. Why not prefixed by T9? Where does this restriction come from?

The instructions Load and Store can move uninitialized objects, see Definition 15.4.1 on Page 216 which says that every verify type is less or equal than unusable. If we would allow the type unusable in registers, we had to change the definition of the relation <reg on Page 222. The reason that we work with partial functions regT is that also the function reg of the trustful VM is partial. The defensive VM extracts from reg the types of the registers and obtains a partial function regT.

Page 242: The page states that "A compiler for Java, however, had to use more local registers for storing return values and for storing exceptions in default handlers." Why?

More precisely, a compiler had to use more local registers in general as illustrated in the following Java program:
public class Test {

 public static void main(String[] argv) {
   m(true);
 }

 public static void m(boolean b) {
     try {
         int j, k, l;
         try {
             if (b) return;
             j = 1;
             k = 2;
             l = 3;
         } finally { // Subroutine S
             if (b) return;
         }
         if (j==1) return;
         if (k==2) return;
         if (l==3) return;
     } finally {     // Subroutine T
         if (b) return;
         Object o = new Object();
     }
 }
}
   

The Jbook-Compiler uses for the variables l and o the same register number in the bytecode. This is legal, because the variables are defined in disjoint scopes. Obviously, variable o is modified in subroutine T and therefore o is in the set mod(T). Since subroutine S calls subroutine T (due to the return statement), the variable o is also in the set mod(S) by Item 2 of the modified definition of the inductive mod. Since variable l uses the same register number as variable o, the bytecode verifier thinks, that l is modified by the subroutine S which is obviously not the case. In fact, the Jbook-Verifier with the inductive definition for mod as described on Page 239 would reject this program compiled with the Jbook-Compiler. Hence, for this example, a compiler must use different register numbers for l and o.
The Sun Java Compiler (in JDK 1.3, e.g.) already uses more local register numbers. Therefore, one has to use the Jbook-Compiler (which uses less register numbers) to reproduce the problem.

Home


ETH Home August 2001
Responsible
ETH Logo