remove_instanceof.h File Reference

Remove Instance-of Operators. More...

#include <goto-programs/goto_functions.h>

Include dependency graph for remove_instanceof.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
void	remove_instanceof (const irep_idt &function_identifier, goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &)
	Replace an instanceof in the expression or guard of the passed instruction of the given function body with an explicit class-identifier test. More...
void	remove_instanceof (const irep_idt &function_identifier, goto_functionst::goto_functiont &function, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &)
	Replace every instanceof in the passed function with an explicit class-identifier test. More...
void	remove_instanceof (goto_functionst &goto_functions, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &)
	Replace every instanceof in every function with an explicit class-identifier test. More...
void	remove_instanceof (goto_modelt &model, const class_hierarchyt &class_hierarchy, message_handlert &)
	Replace every instanceof in every function with an explicit class-identifier test. More...

Detailed Description

Remove Instance-of Operators.

Java has an operator called instanceof, which is used to check if an instance of a class is of a particular type. For example given that A and B are the identifiers of classes, which directly extend Object. If the following example java code is executed -

Object a = new A();
boolean x = a instanceof A; // true
boolean y = a instanceof B; // false

Then, x will be set to true and y will be set to false.

instanceof also works with inheritance. Given classes C and D, where C extends from Object and D extends C. If the following example java code is executed -

Object c = new C();
Object d = new D();
boolean b1 = c instanceof C; // true
boolean b2 = c instanceof D; // false
boolean b3 = d instanceof C; // true
boolean b4 = d instanceof D; // true

Then, b1 will be true, b2 will be false, b3 will be true and b4 will be true.

instanceof has its own instruction type in the java bytecode. We need to rewrite it in terms of other, more fundamental operations in order to analyse it. This operation is referred to as "lowering" or in this specific case - remove_instanceof.

For a simple example where class A extends Object and no classes extend A, the expression e instanceof A needs to be lowered to an expression equivalent to e == null ? false : e->@class_identifier == "A". The null case needs to be taken into account first, as we can't lookup the value of a @class_identifier field in a null pointer. Note that according to the Java specification, null is not an instance of any type.

For an example with inheritance where class D extends C and C extends Object, then e instanceof C needs to be lowered to an expression equivalent to e == null ? false : (e->@class_identifier == "C" || e->@class_identifier == "D"). To lower e instanceof C correctly, we need to take into account each of the classes extends from C. Working out what classes extend a given class type is performed using an instance of the class_hierarchyt class.

In terms of the goto program, the instanceof operator is identified in the expression tree, based on the exprt.id() being ID_java_instance_of. The left hand side of the operator must be a pointer and the right hand side must be a type.

The lowered form has a refinement to help with null pointer analysis later on. Instead of dereferencing the pointer to get @class_identifier in each comparision, it is dereferenced a single time and the result is reused. This is easier to analyse for null pointers, because there is only a single dereference to consider. So the constructed program takes the form -

if(expr == null)
  instanceof_result = false;
else
  string class_identifier_tmpX = expr->@class_identifier;
  instanceof_result =
    class_identifier_tmpX == "C" ||
    class_identifier_tmpX == "D";

Where the X in class_identifier_tmp is a number which makes the identifier unique.

Definition in file remove_instanceof.h.

Function Documentation

remove_instanceof() [1/4]

void remove_instanceof	(	const irep_idt &	function_identifier,
		goto_functionst::goto_functiont &	function,
		symbol_table_baset &	symbol_table,
		const class_hierarchyt &	class_hierarchy,
		message_handlert &	message_handler
	)

Replace every instanceof in the passed function with an explicit class-identifier test.

Remarks

Extra auxiliary variables may be introduced into symbol_table.

Parameters

function_identifier	name of the goto function function
function	The function to work on.
symbol_table	The symbol table to add symbols to.
class_hierarchy	class hierarchy analysis of symbol_table
message_handler	logging output

Definition at line 326 of file remove_instanceof.cpp.

remove_instanceof() [2/4]

void remove_instanceof	(	const irep_idt &	function_identifier,
		goto_programt::targett	target,
		goto_programt &	goto_program,
		symbol_table_baset &	symbol_table,
		const class_hierarchyt &	class_hierarchy,
		message_handlert &	message_handler
	)

Replace an instanceof in the expression or guard of the passed instruction of the given function body with an explicit class-identifier test.

Remarks

Extra auxiliary variables may be introduced into symbol_table.

Parameters

function_identifier	name of the goto function goto_program
target	The instruction to work on.
goto_program	The function body containing the instruction.
symbol_table	The symbol table to add symbols to.
class_hierarchy	class hierarchy analysis of symbol_table
message_handler	logging output

Definition at line 306 of file remove_instanceof.cpp.

remove_instanceof() [3/4]

void remove_instanceof	(	goto_functionst &	goto_functions,
		symbol_table_baset &	symbol_table,
		const class_hierarchyt &	class_hierarchy,
		message_handlert &	message_handler
	)

Replace every instanceof in every function with an explicit class-identifier test.

Remarks

Extra auxiliary variables may be introduced into symbol_table.

Parameters

goto_functions	The functions to work on.
symbol_table	The symbol table to add symbols to.
class_hierarchy	class hierarchy analysis of symbol_table
message_handler	logging output

Definition at line 344 of file remove_instanceof.cpp.

remove_instanceof() [4/4]

void remove_instanceof	(	goto_modelt &	goto_model,
		const class_hierarchyt &	class_hierarchy,
		message_handlert &	message_handler
	)

Replace every instanceof in every function with an explicit class-identifier test.

Remarks

Extra auxiliary variables may be introduced into symbol_table.

Parameters

goto_model	The functions to work on and the symbol table to add
class_hierarchy	class hierarchy analysis of goto_model's symbol table
message_handler	logging output symbols to.

Definition at line 366 of file remove_instanceof.cpp.