LARA

Translate manually into bytecodes using the techniques in Compilation as Tree Transformation:

  • First translate the while loop to $branch$ instructions.
  • Give code for the loop
  • Take care of the rest

b should be treated as a member of the current class.

boolean b;
int f(int x, int y, int z) {
  while ((!b && (x > 2*(y+z))) || (x < 2*y +z)) {
    x = x +3;
  }
  return x;
}

Translating While Expressions

Using the branch(c, l1, l2) instruction this will translate into

lLoop:	branch( condition, cYes, lAfter)
cYes:	[|x=x+3|]
	goto lLoop
lAfter:

Translating Complex Boolean Conditions

The boolean condition is again complex and it can be represented as a disjunction of two simpler conditions.

lLoop:	branch( condition1 || condition2, cYes, lAfter)
cYes:	[|x=x+3|]
	goto lLoop
lAfter:

Using the rule for translating disjunctions, this becomes:

lLoop:	branch( condition1, cYes, c1No)
c1No:   branch( condition2, cYes, lAfter)
cYes:	[|x=x+3|]
	goto lLoop
 
lAfter:

The boolean condition condition1 is a conjunction of two conditions:

lLoop:	branch( condition11 && condition12, cYes, c1No)
c1No:   branch( condition2, cYes, lAfter)
cYes:	[|x=x+3|]
	goto lLoop
lAfter:

Using the rule for translating conjunctions, this becomes:

lLoop:	branch( condition11, c11Yes, c1No)
c11Yes: branch( condition12, cYes, c1No)
c1No:   branch( condition2, cYes, lAfter)
cYes:	[|x=x+3|]
	goto lLoop
lAfter:

Using the real boolean conditions from the program we obtain:

lLoop:	branch( !b, c11Yes, c1No)
c11Yes: branch( x > 2*(y+z), cYes, c1No)
c1No:   branch( x < 2*y +z, cYes, lAfter)
cYes:	[|x=x+3|]
	goto lLoop
lAfter:

Negation is eliminated by reversing the labels:

lLoop:	branch( b, c1No, c11Yes)
c11Yes: branch( x > 2*(y+z), cYes, c1No)
c1No:   branch( x < 2*y +z, cYes, lAfter)
cYes:	[|x=x+3|]
	goto lLoop
lAfter:

Translation of Relations in Boolean Conditions

Translating a boolean condition is done using a bytecode comparison instruction:

lLoop:	branch(b, c1No, c11Yes)
c11Yes: [| x |] 
        [| 2*(y+z) |]
        if_icmpgt cYes
c1No:   [| x |]
        [| 2*y+z |]
        if_icmplt cYes
        goto lAfter
cYes:	[|x=x+3|]
	goto lLoop
lAfter:
<\code>
 
===== Translating of Boolean Variables =====
 
The next unprocessed branch instruction checks the value of a boolean variable objects:
 
<code java>
	[| b |]
        [| 0 |]
	if_icmpne c1No
c11Yes: [| x |] 
        [| 2*(y+z) |]
        if_icmpgt cYes
c1No:   [| x |]
        [| 2*y+z |]
        if_icmplt cYes
        goto lAfter
cYes:	[|x=x+3|]
	goto lLoop
lAfter:

We must load the object member b:

	aload_0
        getfield
	iconst_0
	if_icmpne c1No
c11Yes: [| x |] 
        [| 2*(y+z) |]
        if_icmpgt cYes
c1No:   [| x |]
        [| 2*y+z |]
        if_icmplt cYes
        goto lAfter
cYes:	[|x=x+3|]
	goto lLoop
lAfter:

Translating Arithmetical Expressions

Arithemtical expressions are translated using standard postfix notation:

	aload_0
        getfield
	iconst_0
	if_icmpne c1No
c11Yes: [| x |] 
        [| 2 |] [| y |] [| z |] [| + ]| [| * |] 
        if_icmpgt cYes
c1No:   [| x |]
        [| 2 |] [| y |] [| * |] [| z |] [| + |]
        if_icmplt cYes
        goto lAfter
cYes:	[|x=x+3|]
	goto lLoop
lAfter:

At the end this piece of code translates to:

	 aload_0
         getfield
	 iconst_0
	 if_icmpne c1No
c11Yes:  iload_1
         iconst_2
         iload_2
         iload_3
         iadd
         imul
         if_icmpgt cYes
c1No:    iload_1
         iconst_2
         iload_2
         imul
         iload_3
         iadd 
         if_icmplt cYes
         goto lAfter
cYes:    [|x=x+3|]
	 goto lLoop
lAfter:

Integrating the rest of the program gives:

	 aload_0
         getfield
	 iconst_0
	 if_icmpne c1No
c11Yes:  iload_1
         iconst_2
         iload_2
         iload_3
         iadd
         imul
         if_icmpgt cYes
c1No:    iload_1
         iconst_2
         iload_2
         imul
         iload_3
         iadd 
         if_icmplt cYes
         goto lAfter
cYes:    iload_1
         iconst_3
         iadd
         istore_1
	 goto lLoop
lAfter:  iload_1
         ireturn