1/*******************************************************************\
3Module: Remove Instance-of Operators
5Author: Chris Smowton, chris.smowton@diffblue.com
7\*******************************************************************/
36 // Lower instanceof for a single function
39 // Lower instanceof for a single instruction
72 std::vector<irep_idt> children =
74 children.push_back(target_type);
75 // Sort alphabetically to make order of generated disjuncts
76 // independent of class loading order
79 return a.compare(b) < 0;
83 for(
const auto &class_name : children)
102 const irep_idt &function_identifier,
109 bool changed =
false;
118 "java_instanceof should have two operands");
123 "instanceof first operand should be a pointer");
128 "instanceof second operand should be a type");
132 "instanceof second operand should have a simple type");
143 // If we're casting to a reference array type, check
144 // @class_identifier == "java::array[reference]" &&
145 // @array_dimension == target_array_dimension &&
146 // @array_element_type (subtype of) target_array_element_type
147 // Otherwise just check
148 // @class_identifier (subtype of) target_type
150 // Exception: when the target type is Object, nothing needs checking; when
151 // it is Object[], Object[][] etc, then we check that
152 // @array_dimension >= target_array_dimension (because
153 // String[][] (subtype of) Object[] for example) and don't check the element
156 // All tests are made directly against a pointer to the object whose type is
157 // queried. By operating directly on a pointer rather than using a temporary
158 // (x->@clsid == "A" rather than id = x->@clsid; id == "A") we enable symex's
159 // value-set filtering to discard no-longer-viable candidates for "x" (in the
160 // case where 'x' is a symbol, not a general expression like x->y->@clsid).
161 // This means there are more clean dereference operations (ones where there
162 // is no possibility of reading a null, invalid or incorrectly-typed object),
163 // and less pessimistic aliasing assumptions possibly causing goto-symex to
164 // explore in-fact-unreachable paths.
166 // In all cases require the input pointer is not null for any cast to succeed:
190 if(underlying_type ==
jlo)
201 underlying_type.get_identifier(),
205 else if(target_type !=
jlo)
209 target_type.get_identifier(),
240 const irep_idt &function_identifier,
247 target->is_target() &&
251 // If this is a branch target, add a skip beforehand so we can splice new
252 // GOTO programs before the target instruction without inserting into the
253 // wrong basic block.
255 target->turn_into_skip();
256 // Actually alter the now-moved instruction:
261 function_identifier, target->code_nonconst(), goto_program, target);
265 target->condition_nonconst(),
279 const irep_idt &function_identifier,
283 for(goto_programt::instructionst::iterator target=
307 const irep_idt &function_identifier,
327 const irep_idt &function_identifier,
exprt get_class_identifier_field(const exprt &this_expr_in, const struct_tag_typet &suggested_type, const namespacet &ns)
Extract class identifier.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A base class for relations, i.e., binary predicates whose two operands have the same type.
Non-graph-based representation of the class hierarchy.
idst get_children_trans(const irep_idt &id) const
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
void compute_location_numbers()
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void update()
Update all indices.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
bool lower_instanceof(const irep_idt &function_identifier, goto_programt &)
Replace every instanceof in the passed function body with an explicit class-identifier test.
message_handlert & message_handler
remove_instanceoft(symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
const class_hierarchyt & class_hierarchy
symbol_table_baset & symbol_table
The symbol table base class interface.
#define Forall_operands(it, expr)
std::pair< typet, std::size_t > java_array_dimension_and_element_type(const struct_tag_typet &type)
Returns the underlying element type and array dimensionality of Java struct type.
exprt get_array_element_type_field(const exprt &pointer)
exprt get_array_dimension_field(const exprt &pointer)
java_reference_typet java_lang_object_type()
#define JAVA_REFERENCE_ARRAY_CLASSID
bool can_cast_type< java_reference_typet >(const typet &type)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
static exprt subtype_expr(const exprt &classid_field, const irep_idt &target_type, const class_hierarchyt &class_hierarchy)
Produce an expression of the form classid_field == "A" || classid_field == "B" || ....
static bool contains_instanceof(const exprt &e)
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...
Remove Instance-of Operators.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.