Skip to content

Clean up remove-instanceof #1405

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Sep 21, 2017
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/goto-programs/goto_program_template.h
Original file line number Diff line number Diff line change
Expand Up @@ -361,6 +361,7 @@ class goto_program_templatet
}
};

// Never try to change this to vector-we mutate the list while iterating
typedef std::list<instructiont> instructionst;

typedef typename instructionst::iterator targett;
Expand Down
243 changes: 109 additions & 134 deletions src/goto-programs/remove_instanceof.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ Author: Chris Smowton, [email protected]
#include "class_identifier.h"

#include <util/fresh_symbol.h>
#include <java_bytecode/java_types.h>

#include <sstream>

Expand Down Expand Up @@ -42,160 +43,135 @@ class remove_instanceoft

bool lower_instanceof(goto_programt &);

typedef std::vector<
std::pair<goto_programt::targett, goto_programt::targett>> instanceof_instt;
bool lower_instanceof(goto_programt &, goto_programt::targett);

void lower_instanceof(
goto_programt &,
goto_programt::targett,
instanceof_instt &);

void lower_instanceof(
exprt &,
goto_programt &,
goto_programt::targett,
instanceof_instt &);

bool contains_instanceof(const exprt &);
std::size_t lower_instanceof(
exprt &, goto_programt &, goto_programt::targett);
};

/// Avoid breaking sharing by checking for instanceof before calling
/// lower_instanceof.
/// \par parameters: Expression `expr`
/// \return Returns true if `expr` contains any instanceof ops
bool remove_instanceoft::contains_instanceof(
const exprt &expr)
{
if(expr.id()==ID_java_instanceof)
return true;
forall_operands(it, expr)
if(contains_instanceof(*it))
return true;
return false;
}

/// Replaces an expression like e instanceof A with e.@class_identifier == "A"
/// Or a big-or of similar expressions if we know of subtypes that also satisfy
/// Replaces an expression like e instanceof A with e.\@class_identifier == "A"
/// or a big-or of similar expressions if we know of subtypes that also satisfy
/// the given test.
/// \par parameters: Expression to lower `expr` and the `goto_program` and
/// instruction `this_inst` it belongs to.
/// \return Side-effect on `expr` replacing it with an explicit clsid test
void remove_instanceoft::lower_instanceof(
/// \param expr: Expression to lower (the code or the guard of an instruction)
/// \param goto_program: program the expression belongs to
/// \param this_inst: instruction the expression is found at
/// \return number of instanceof expressions that have been replaced
std::size_t remove_instanceoft::lower_instanceof(
exprt &expr,
goto_programt &goto_program,
goto_programt::targett this_inst,
instanceof_instt &inst_switch)
goto_programt::targett this_inst)
{
if(expr.id()==ID_java_instanceof)
if(expr.id()!=ID_java_instanceof)
{
const exprt &check_ptr=expr.op0();
assert(check_ptr.type().id()==ID_pointer);
const exprt &target_arg=expr.op1();
assert(target_arg.id()==ID_type);
const typet &target_type=target_arg.type();

// Find all types we know about that satisfy the given requirement:
assert(target_type.id()==ID_symbol);
const irep_idt &target_name=
to_symbol_type(target_type).get_identifier();
std::vector<irep_idt> children=
class_hierarchy.get_children_trans(target_name);
children.push_back(target_name);

assert(!children.empty() && "Unable to execute instanceof");

// Insert an instruction before this one that assigns the clsid we're
// checking against to a temporary, as GOTO program if-expressions should
// not contain derefs.

symbol_typet jlo("java::java.lang.Object");
exprt object_clsid=get_class_identifier_field(check_ptr, jlo, ns);

symbolt &newsym=
get_fresh_aux_symbol(
object_clsid.type(),
"instanceof_tmp",
"instanceof_tmp",
source_locationt(),
ID_java,
symbol_table);

auto newinst=goto_program.insert_after(this_inst);
newinst->make_assignment();
newinst->code=code_assignt(newsym.symbol_expr(), object_clsid);
newinst->source_location=this_inst->source_location;
newinst->function=this_inst->function;

// Insert the check instruction after the existing one.
// This will briefly be ill-formed (use before def of
// instanceof_tmp) but the two will subsequently switch
// places in lower_instanceof(goto_programt &) below.
inst_switch.push_back(make_pair(this_inst, newinst));
// Replace the instanceof construct with a big-or.
exprt::operandst or_ops;
for(const auto &clsname : children)
{
constant_exprt clsexpr(clsname, string_typet());
equal_exprt test(newsym.symbol_expr(), clsexpr);
or_ops.push_back(test);
}
expr=disjunction(or_ops);
std::size_t replacements=0;
Forall_operands(it, expr)
replacements+=lower_instanceof(*it, goto_program, this_inst);
return replacements;
}
else

INVARIANT(
expr.operands().size()==2,
"java_instanceof should have two operands");

const exprt &check_ptr=expr.op0();
INVARIANT(
check_ptr.type().id()==ID_pointer,
"instanceof first operand should be a pointer");

const exprt &target_arg=expr.op1();
INVARIANT(
target_arg.id()==ID_type,
"instanceof second operand should be a type");
const typet &target_type=target_arg.type();

// Find all types we know about that satisfy the given requirement:
INVARIANT(
target_type.id()==ID_symbol,
"instanceof second operand should have a simple type");
const irep_idt &target_name=
to_symbol_type(target_type).get_identifier();
std::vector<irep_idt> children=
class_hierarchy.get_children_trans(target_name);
children.push_back(target_name);

// Insert an instruction before the new check that assigns the clsid we're
// checking for to a temporary, as GOTO program if-expressions should
// not contain derefs.
// We actually insert the assignment instruction after the existing one.
// This will briefly be ill-formed (use before def of instanceof_tmp) but the
// two will subsequently switch places. This makes sure that the inserted
// assignement doesn't end up before any labels pointing at this instruction.
symbol_typet jlo=to_symbol_type(java_lang_object_type().subtype());
exprt object_clsid=get_class_identifier_field(check_ptr, jlo, ns);

symbolt &newsym=
get_fresh_aux_symbol(
object_clsid.type(),
"instanceof_tmp",
"instanceof_tmp",
source_locationt(),
ID_java,
symbol_table);

auto newinst=goto_program.insert_after(this_inst);
newinst->make_assignment();
newinst->code=code_assignt(newsym.symbol_expr(), object_clsid);
newinst->source_location=this_inst->source_location;
newinst->function=this_inst->function;

// Replace the instanceof construct with a big-or.
exprt::operandst or_ops;
for(const auto &clsname : children)
{
Forall_operands(it, expr)
lower_instanceof(*it, goto_program, this_inst, inst_switch);
constant_exprt clsexpr(clsname, string_typet());
equal_exprt test(newsym.symbol_expr(), clsexpr);
or_ops.push_back(test);
}
expr=disjunction(or_ops);

return 1;
}

/// See function above
/// \par parameters: GOTO program instruction `target` whose instanceof
/// expressions,
/// if any, should be replaced with explicit tests, and the
/// `goto_program` it is part of.
/// \return Side-effect on `target` as above.
void remove_instanceoft::lower_instanceof(
/// Replaces expressions like e instanceof A with e.\@class_identifier == "A"
/// or a big-or of similar expressions if we know of subtypes that also satisfy
/// the given test. Does this for the code or guard at a specific instruction.
/// \param goto_program: program to process
/// \param target: instruction to check for instanceof expressions
/// \return true if an instanceof has been replaced
bool remove_instanceoft::lower_instanceof(
goto_programt &goto_program,
goto_programt::targett target,
instanceof_instt &inst_switch)
goto_programt::targett target)
{
bool code_iof=contains_instanceof(target->code);
bool guard_iof=contains_instanceof(target->guard);
// The instruction-switching step below will malfunction if a check
// has been added for the code *and* for the guard. This should
// be impossible, because guarded instructions currently have simple
// code (e.g. a guarded-goto), but this assertion checks that this
// assumption is correct and remains true on future evolution of the
// allowable goto instruction types.
assert(!(code_iof && guard_iof));
if(code_iof)
lower_instanceof(target->code, goto_program, target, inst_switch);
if(guard_iof)
lower_instanceof(target->guard, goto_program, target, inst_switch);
std::size_t replacements=
lower_instanceof(target->code, goto_program, target)+
lower_instanceof(target->guard, goto_program, target);

if(replacements==0)
return false;
// Swap the original instruction with the last assignment added after it
target->swap(*std::next(target, replacements));
return true;
}

/// See function above
/// \par parameters: `goto_program`, all of whose instanceof expressions will
/// be replaced by explicit class-identifier tests.
/// \return Side-effect on `goto_program` as above.
/// Replace every instanceof in the passed function body with an explicit
/// class-identifier test.
/// Extra auxiliary variables may be introduced into symbol_table.
/// \param goto_program: The function body to work on.
/// \return true if one or more instanceof expressions have been replaced
bool remove_instanceoft::lower_instanceof(goto_programt &goto_program)
{
instanceof_instt inst_switch;
Forall_goto_program_instructions(target, goto_program)
lower_instanceof(goto_program, target, inst_switch);
if(!inst_switch.empty())
bool changed=false;
for(goto_programt::instructionst::iterator target=
goto_program.instructions.begin();
target!=goto_program.instructions.end();
++target)
{
for(auto &p : inst_switch)
{
const goto_programt::targett &this_inst=p.first;
const goto_programt::targett &newinst=p.second;
this_inst->swap(*newinst);
}
goto_program.update();
return true;
changed=lower_instanceof(goto_program, target) || changed;
}
else
if(!changed)
return false;
goto_program.update();
return true;
}

/// See function above
Expand Down Expand Up @@ -226,6 +202,5 @@ void remove_instanceof(

void remove_instanceof(goto_modelt &goto_model)
{
remove_instanceof(
goto_model.symbol_table, goto_model.goto_functions);
remove_instanceof(goto_model.symbol_table, goto_model.goto_functions);
}