cprover
remove_instanceof.h File Reference

Remove Instance-of Operators. More...

+ 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 (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 (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 ( 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
targetThe instruction to work on.
goto_programThe function body containing the instruction.
symbol_tableThe symbol table to add symbols to.
class_hierarchyclass hierarchy analysis of symbol_table
message_handlerlogging output

Definition at line 246 of file remove_instanceof.cpp.

◆ remove_instanceof() [2/4]

void remove_instanceof ( 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
functionThe function to work on.
symbol_tableThe symbol table to add symbols to.
class_hierarchyclass hierarchy analysis of symbol_table
message_handlerlogging output

Definition at line 264 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_functionsThe functions to work on.
symbol_tableThe symbol table to add symbols to.
class_hierarchyclass hierarchy analysis of symbol_table
message_handlerlogging output

Definition at line 281 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_modelThe functions to work on and the symbol table to add
class_hierarchyclass hierarchy analysis of goto_model's symbol table
message_handlerlogging output symbols to.

Definition at line 303 of file remove_instanceof.cpp.