LARA – Lab for Automated Reasoning and Analysis -

Translating If Expressions

int activityLevel
boolean action(int signals, boolean objects, int smart, int pretty) {
  if ((signals > 5 || !objects) && smart + 2*pretty > 10) {
    activityLevel++;
    return true;
  } else {
    activityLevel--;
    return false;
  }
}

can be abstracted as:

[| if (condition) {...} else {...} |]

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

	branch( condition, cYes, cNo)
cYes:	[|activityLevel++; return true;|]
	goto lAfter
cNo:	[|activityLevel--;return false;	|]
lAfter:

Translating Complex Boolean Conditions

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

	branch( condition1 && condition2, cYes, cNo)
cYes:	[|activityLevel++; return true;|]
	goto lAfter
cNo:	[|activityLevel--;return false;	|]
lAfter:

Using the rule for translating conjunctions, this becomes:

	branch( condition1, c1Yes, cNo) 
c1Yes:	branch( condition2, cYes, cNo) 
cYes:	[|activityLevel++; return true;|]
	goto lAfter
cNo:	[|activityLevel--;return false;	|]
lAfter:

The boolean condition condition1 is a disjunction of two conditions:

	branch( condition11 || condition12, c1Yes, cNo) 
c1Yes:	branch( condition2, cYes, cNo) 
cYes:	[|activityLevel++; return true;|]
	goto lAfter
cNo:	[|activityLevel--;return false;	|]
lAfter:

Using the rule for translating disjunctions, this becomes:

	branch( condition11, c1Yes, c11No) 
c11No:	branch( condition12, c1Yes, cNo) 
c1Yes:	branch( condition2, cYes, cNo) 
cYes:	[|activityLevel++; return true;|]
	goto lAfter
cNo:	[|activityLevel--;return false;	|]
lAfter:

Using the real boolean conditions from the program we obtain:

	branch( signals > 5, c1Yes, c11No) 
c11No:	branch( !objects, c1Yes, cNo) 
c1Yes:	branch( smart + 2*pretty > 10, cYes, cNo) 
cYes:	[|activityLevel++; return true;|]
	goto lAfter
cNo:	[|activityLevel--;return false;	|]
lAfter:

Negation is eliminated by reversing the labels:

	branch( signals > 5, c1Yes, c11No) 
c11No:	branch( objects, cNo, c1Yes) 
c1Yes:	branch( smart + 2*pretty > 10, cYes, cNo) 
cYes:	[|activityLevel++; return true;|]
	goto lAfter
cNo:	[|activityLevel--;return false;	|]
lAfter:

Translation of Relations in Boolean Conditions

Translating a boolean condition involving > operator is done using a bytecode comparison instruction:

	[| signals |]
	[| 5 |]
	if_icmpgt c1Yes
	goto c1No
c11No:	branch( objects, cNo, c1Yes) 
c1Yes:	branch( smart + 2*pretty > 10, cYes, cNo) 
cYes:	[|activityLevel++; return true;|]
	goto lAfter
cNo:	[|activityLevel--;return false;	|]
lAfter:

Finally, we derive a beginning of the bytecode program:

0:	iload_1
1:	iconst_5
2:	if_icmpgt c1Yes
3:	goto c1No
c11No:	branch( objects, cNo, c1Yes) 
c1Yes:	branch( smart + 2*pretty > 10, cYes, cNo) 
cYes:	[|activityLevel++; return true;|]
	goto lAfter
cNo:	[|activityLevel--;return false;	|]
lAfter:

We apply the same procedure on the piece of code labeled with c1Yes:

0:	iload_1
1:	iconst_5
2:	if_icmpgt c1Yes
3:	goto c1No
c11No:	branch( objects, cNo, c1Yes) 
c1Yes:	[| smart + 2*pretty |]
	[| 10 |]
	if_icmple cNo
	goto cYes
cYes:	[|activityLevel++; return true;|]
	goto lAfter
cNo:	[|activityLevel--;return false;	|]
lAfter:

Note that label c11No is not needed, so the code can be optimized:

0:	iload_1
1:	iconst_5
2:	if_icmpgt c1Yes
3:	branch( objects, cNo, c1Yes) 
c1Yes:	[| smart + 2*pretty |]
	[| 10 |]
	if_icmple cNo
	goto cYes
cYes:	[|activityLevel++; return true;|]
	goto lAfter
cNo:	[|activityLevel--;return false;	|]
lAfter:

Translating of Boolean Variables

The next unprocessed branch instruction ckecks the value of a boolean variable objects:

0:	iload_1
1:	iconst_5
2:	if_icmpgt c1Yes
3:	iload_2
4:	ifne cNo
5:	goto c1Yes
c1Yes:	[| smart + 2*pretty |]
	[| 10 |]
	if_icmple cNo
	goto cYes
cYes:	[|activityLevel++; return true;|]
	goto lAfter
cNo:	[|activityLevel--;return false;	|]
lAfter:

Note that we can further optimize the code since the command currently labeled with 5 is not needed. This way, the label c1Yes gets the value 5.

0:	iload_1
1:	iconst_5
2:	if_icmpgt 5
3:	iload_2
4:	ifne cNo
5:	[| smart + 2*pretty |]
	[| 10 |]
	if_icmple cNo
	goto cYes
cYes:	[|activityLevel++; return true;|]
	goto lAfter
cNo:	[|activityLevel--;return false;	|]
lAfter:

Translating Arithmetical Expressions

Arithemtical expressions are translated using standard postfix notation:

0:	iload_1
1:	iconst_5
2:	if_icmpgt 5
3:	iload_2
4:	ifne cNo
5:	[| smart |] :: [| 2 |] :: [| pretty |] :: * :: + 
	[| 10 |]
	if_icmple cNo
	goto cYes
cYes:	[|activityLevel++; return true;|]
	goto lAfter
cNo:	[|activityLevel--;return false;	|]
lAfter:

At the end this piece of code translates to:

0:	iload_1
1:	iconst_5
2:	if_icmpgt 5
3:	iload_2
4:	ifne cNo
5:	iload_3
6:	iconst_2
7:	iload_4
8:	imul
9:	iadd
10:	bipush 10
11:	if_icmple cNo
12:	goto cYes
cYes:	[|activityLevel++; return true;|]
	goto lAfter
cNo:	[|activityLevel--;return false;	|]
lAfter:

Note that we can again optimize the code since the command currently labeled with 12 is not needed. This way, the label cYes gets the value 12.

0:	iload_1
1:	iconst_5
2:	if_icmpgt 5
3:	iload_2
4:	ifne cNo
5:	iload_3
6:	iconst_2
7:	iload_4
8:	imul
9:	iadd
10:	bipush 10
11:	if_icmple cNo
12:	[|activityLevel++; return true;|]
	goto lAfter
cNo:	[|activityLevel--;return false;	|]
lAfter:

Manipulating an Object Reference

We continue to translate block statements:

0:	iload_1
1:	iconst_5
2:	if_icmpgt 5
3:	iload_2
4:	ifne cNo
5:	iload_3
6:	iconst_2
7:	iload_4
8:	imul
9:	iadd
10:	bipush 10
11:	if_icmple cNo
12:	[|activityLevel++|] 
	iconst_1
	ireturn
	goto lAfter
cNo:	[|activityLevel--|]
	iconst_0
	ireturn
lAfter:

There is no need for goto command after ireturn and we do not have any code after if_then_else command, so we can delete lAfter label:

0:	iload_1
1:	iconst_5
2:	if_icmpgt 5
3:	iload_2
4:	ifne cNo
5:	iload_3
6:	iconst_2
7:	iload_4
8:	imul
9:	iadd
10:	bipush 10
11:	if_icmple cNo
12:	[|activityLevel++|] 
	iconst_1
	ireturn
cNo:	[|activityLevel--|]
	iconst_0
	ireturn

In the tutorial we increased (and decreased) the variable activityLevel using the following command: iinc 0, 1 (iinc 0, -1). This was not completely correct as activityLevel is a field of a class so the correct version is by using aload, getfield and putfield.

This way the command

activityLevel++

is translated as:

aload_0
dup
getfield        #2; //Field activityLevel:I
iconst_1
iadd
putfield        #2; //Field activityLevel:I

The command for decrement of activityLevel is translated similarly. If we intagrate that into the bytecode program we obtain:

0:	iload_1
1:	iconst_5
2:	if_icmpgt 5
3:	iload_2
4:	ifne cNo
5:	iload_3
6:	iconst_2
7:	iload_4
8:	imul
9:	iadd
10:	bipush 10
11:	if_icmple cNo
12:	aload_0
13:	dup
14:	getfield
15:	iconst_1
16:	iadd
17:	putfield
18:	iconst_1
19:	ireturn
cNo:	[|activityLevel--|]
	iconst_0
	ireturn

At the end we see that the label cNo has value 20 and finally, the complete translated program looks as follows:

0:	iload_1
1:	iconst_5
2:	if_icmpgt 5
3:	iload_2
4:	ifne 20
5:	iload_3
6:	iconst_2
7:	iload_4
8:	imul
9:	iadd
10:	bipush 10
11:	if_icmple 20
12:	aload_0
13:	dup
14:	getfield
15:	iconst_1
16:	iadd
17:	putfield
18:	iconst_1
19:	ireturn
20:	aload_0
21:	dup
22:	getfield
23:	iconst_1
24:	isub
25:	putfield
26:	iconst_0
27:	ireturn