Rules of de_nite assignment - JVM

Each local variable must have a de_nitely assigned value when any access of its value occurs. An access to its value consists of using the identi_er of the variable occurring anywhere in an expression except as the left-hand operand of the simple assignment operator =. A Java compiler must carry out a speci_c conservative ow analysis to make sure that, for every access of a local variable, the local variable is de_nitely assigned before the access; otherwise a compile-time error must occur.

Since local variables are not initialized with default values like class variables or instance _elds, a Java program that does not obey the rules of de_nite assignment could violate the invariants of Theorem below and would not be type safe. For example, a local pointer variable which is not initialized could point to an unde_ned location on the heap. Moreover, the rules of de_nite assignment ensure that the bytecode generated by a correct Java compiler is not rejected by the bytecode veri_er (Theorems below).

The rules of de_nite assignment have been changed in the second edition of the JLS [19, x16]. Boolean operators &, |, ^, == as well as assignments of boolean expressions to boolean variables are no longer treated in a special way. We take the rules of the second edition, because it simpli_es the task of writing a compiler that generates code that is accepted by the veri_er.

In order to precisely specify all the cases of de_nite assignment, static functions before, after , true, false and vars are computed at compile-time.

These functions assign sets of variables (identi_ers) to each position in the body of a method. The static functions have the following intended meanings (the functions true(_) and false(_) are de_ned for expressions of type boolean only):

x 2 before(_)

The variable x is de_nitely assigned before the evaluation of the statement or expression at position _.

x 2 after (_)

The variable x is de_nitely assigned after the statement or expression at position _ when this statement or expression completes normally.

x 2 true(_)

The variable x is de_nitely assigned after the evaluation of the expression at position _ when this expression evaluates to true.

x 2 false(_)

The variable x is de_nitely assigned after the evaluation of the expression at position _ when this expression evaluates to false.

x 2 vars(_)

The position _ is in the scope of the local variable, formal parameter or catch parameter x . The functions satisfy the following inclusions:

De_nite assignment for boolean expressions

De_nite assignment for boolean expressions

  1. before(_) _ after (_) _ vars(_).
  2. If type(_) = boolean, then before(_) _ true(_) false(_).
  3. If type(_) = boolean, then true(_) [ false(_) _ vars(_). At the root position of a method body the function before is determined by the following initial conditions: Let _block be the body of an instance method, constructor or class method with declaration m(c1 loc1; : : : ; cn locn).

Then before(_) = floc1; : : : ; locng, because when the body is invoked there are always values assigned to the formal parameters loc1; : : : ; locn. If _block is a static initializer, then before(_) is the empty set.

For the other positions in the block the functions before, after , true and false can then be computed in a top-down manner. Instead of explaining exactly how the functions are computed, we just state the equations the functions have to satisfy.

Table below contains the equations for boolean expressions. It is assumed that type(_) = boolean in each row. There are no conditions for after in Table below, since by de_nition in all cases after (_) = true(_)false(_). Constant boolean expressions with value true (resp. false) are treated like the literal true (resp. false). If type(_) is boolean and _exp is not an instance of one of the expressions in Table below, then true(_) = after (_) and false(_) = after (_).

Table below contains the equations for non-boolean expressions. The most important condition is the _rst one for local variables. It requires for a local variable loc at a position _ that loc 2 before(_). Hence loc must be de_nitely assigned before it is used.

In addition to the constraints in Table below there are the following conditions for an expression _exp with direct subexpressions _1exp1; : : : ; _n expn:

De_nite assignment for arbitrary expressions

De_nite assignment for arbitrary expressions

Table below contains the constraints for statements. For a statement with label lab at position _ a set break(_; lab) is needed.

De_nition. A variable x belongs to break(_; lab) if the following two conditions are true:

  1. x is in before(_) for each statement _break lab inside the statement at position _ that can exit _ (Def. below) and
  2. x is in after (_) for each statement _(s finally b) inside _ such that s contains a break lab that can exit _.

If there are no substatements break lab inside _stm, then break(_; lab) = vars(_).

In a block statement the variables which are de_nitely assigned after the normal execution of the statement are the variables which are de_nitely assigned after the last substatement of the block. However, the variables must still be in the scope of a declaration. Consider the following example:

{ _{ int i; i = 3; } { int i; i = 2 * _i; } }

The set after (_) is empty and does not contain the variable i because at the end of block _, i is not in the scope of a declaration. Thus before(_) is empty, too, and the block is rejected by the compiler. Note that in Java it is not allowed to declare the same variable again in the scope of another declaration.

What does it mean that the rules for de_nite assignment are sound? It means that at run-time all variables of the compile-time computed set before(pos) are de_ned in the local environment. If there is a normal value at the current position pos in restbody, then all variables of the set after (pos) are de_ned in the local environment. If the value is the boolean value True, then the variables of the set true(pos) are de_ned in the local environment;

De_nite assignment for statements

De_nite assignment for statements

if the value is False, then the variables of the set after (pos) are de_ned in the local environment. The soundness of the rules of de_nite assignment is included in Theorem below.

Remark . The constraints in Table below di_er from the rules of de_nite assignment in [19, x16] in two points. First, the o_cial JLS de_nes for a try-finally statement _(_stm finally block):

after (_) = after (_) [ after ():

Our de_nition in Table below is more restrictive. A variable x in after (_) belongs to after (_) only if there is no subphrase x = exp in block. Why do we restrict the set in this way? The reason is the program in Fig.below which is legal according to the JLS. If we compile the program following [23, x7.13], then the resulting bytecode is rejected by any bytecode veri_er we tried. If we take our constraints in Table below, then the program in Fig. below is no longer legal, since there is an assignment i = 3 in the finally block and the variable i is not regarded as de_nitely assigned after the try-finally statement. Hence, it cannot be used in the return statement. The e_ect of our restriction of the rules of de_nite assignment for the try-finally statement is that a variable which is de_nitely assigned after the try-finally statement but not after the finally block is|in the eyes of the bytecode veri_er|not modi_ed by the subroutine that implements the finally block.

The second di_erence between Table below and the rules of de_nite assignment in the o_cial JLS a_ects the labeled statement. The second clause of Def. below is not contained in the o_cial JLS. Hence, according to the JLS a variable is de_nitely assigned after a labeled statement, if it is de_nitely assigned after the statement and before every break that can exit the labeled statement. We restrict the set further. The reason for our restriction is that the program in Fig. below which is legal according to the JLS is rejected by all known bytecode veri_ers. Therefore we exclude the (rather exotic) program in Fig. below from the Java programming language. Both of our restrictions of the rules of de_nite assignments are chosen so that we can prove that our compiler in Part II generates veri_able code.

All rights reserved © 2020 Wisdom IT Services India Pvt. Ltd DMCA.com Protection Status

JVM Topics