java_bytecode

This module provides a front end for Java.

Overview of conversion from bytecode to codet

To be documented.

Object Factory

To be documented.

Pointer type selection

To be documented.

Generic substitution

To be documented.

Java bytecode parsing (parser, convert_class, convert_method)

To be documented.

How a java program / class is represented in a .class

To be documented.

Adding runtime exceptions (java_bytecode_instrument)

To be documented.

Concurrency instrumentation

To be documented.

Remove java new

remove_java_new.h remove_java_new is responsible for converting the new, newarray and multianewarray Java bytecode operation into codet. Specifically it converts the bytecode instruction into:

• An ALLOC with the size of the object being created
• An assignment to the value zeroing its contents
• If an array, initializing the size and data components
• If a multi-dimensional array, recursively calling java_new on each sub array

Note: it does not call the constructor as this is done by a separate java bytecode operation.

Java Objects (`new`)

The basic new operation is represented in Java bytecode by the new op

These are converted by remove_java_newt::lower_java_new

For example, the following Java code:

TestClass f = new TestClass();

Which is represented as the following Java bytecode:

0: new           #2                  // class TestClass
3: dup
4: invokespecial #3                  // Method "<init>":()V

The first instruction only is translated into the following codets:

tmp_object1 = side_effect_exprt(ALLOC, sizeof(TestClass))
*tmp_object1 = struct_exprt{.component = 0, ... }

For more details about the zero expression see expr_initializert

Single Dimensional Arrays (`newarray`)

The new Java array operation is represented in Java bytecode by the newarray operation.

These are converted by remove_java_newt::lower_java_new_array

See TODO:details about java arrays for details on how arrays are represented in codet. It first allocates the array object as with a regular Java object. Then the size component is set to be the size of the array and the data component is also initialized.

For example the following Java:

TestClass[] tArray = new TestClass[5];

Which is compiled into the following Java bytecode:

8: iconst_5
9: anewarray     #2                  // class TestClass

Is translated into the following codets:

tmp_object1 = side_effect_exprt(ALLOC, sizeof(java::array[referenence]))
*tmp_object1 = struct_exprt{.size = 0, .data = null}
tmp_object1->length = length
tmp_new_data_array1 = side_effect_exprt(java_new_array_data, TestClass)
tmp_object1->data = tmp_new_data_array1
ARRAY_SET(tmp_new_data_array1, NULL)

The ARRAY_SET codet sets all the values to null.

Multi Dimensional Arrays (`newmultiarray`)

The new Java multi dimensional array operation is represented in bytecode by multianewarray

These are also by remove_java_newt::lower_java_new_array

They work the same as single dimensional arrays but create a for loop for each element in the array since these start initialized.

{C++}
for(tmp_index = 0; tmp_index < dim_size; ++tmp_index)
{
  struct java::array[reference] *subarray_init;
  subarray_init = java_new_array
  newarray_tmp1->data[tmp_index] = (void *)subarray_init;
}

remove_javanew is then recursively applied to the new subarray.

remove_exceptions

To be documented.

Method stubbing

To be documented.

Context Insensitive lazy methods (aka lazy methods v1)

To be documented.

Core Models Library

To be documented.

java_types

To be documented.

String library

To be documented.

See also String Solver Interface.

A worked example of converting java bytecode to codet

To be documented.