Skip to content

Allow to remove instanceof when remove exceptions #1710

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
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
119 changes: 65 additions & 54 deletions src/goto-programs/remove_exceptions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ Date: December 2016
/// Remove exception handling

#include "remove_exceptions.h"
#include "remove_instanceof.h"

#ifdef DEBUG
#include <iostream>
Expand Down Expand Up @@ -43,8 +44,9 @@ Date: December 2016
/// (in instruction->code.exception_list()) and a corresponding GOTO program
/// target for each (in instruction->targets).
/// Thrown instructions are currently always matched to tags using
/// java_instanceof, so a language frontend wanting to use this class
/// must use exceptions with a Java-compatible structure.
/// java_instanceof, optionally lowered to a check on the @class_identifier
/// field, so a language frontend wanting to use this class must use
/// exceptions with a Java-compatible structure.
///
/// CATCH with a code_pop_catcht operand terminates a try-block begun by
/// a code_push_catcht. At present the try block consists of the instructions
Expand Down Expand Up @@ -72,9 +74,6 @@ Date: December 2016
/// instructions copy back to an ordinary local variable (or other expression)
/// and set \#exception_value back to null, indicating the exception has been
/// caught and normal control flow resumed.
///
/// Note that remove_exceptions introduces java_instanceof comparisons at
/// present, so a remove_instanceof may be necessary after it completes.
class remove_exceptionst
{
typedef std::vector<std::pair<
Expand All @@ -84,55 +83,62 @@ class remove_exceptionst
public:
explicit remove_exceptionst(
symbol_tablet &_symbol_table,
std::map<irep_idt, std::set<irep_idt>> &_exceptions_map):
symbol_table(_symbol_table),
exceptions_map(_exceptions_map)
std::map<irep_idt, std::set<irep_idt>> &_exceptions_map,
bool remove_added_instanceof)
: symbol_table(_symbol_table),
exceptions_map(_exceptions_map),
remove_added_instanceof(remove_added_instanceof)
{
}

void operator()(
goto_functionst &goto_functions);
void operator()(goto_functionst &goto_functions);

protected:
symbol_tablet &symbol_table;
std::map<irep_idt, std::set<irep_idt>> &exceptions_map;
bool remove_added_instanceof;

void add_exceptional_returns(
const goto_functionst::function_mapt::iterator &);
const irep_idt &function_id,
goto_programt &goto_program);

void instrument_exception_handler(
const goto_functionst::function_mapt::iterator &,
const irep_idt &function_id,
goto_programt &goto_program,
const goto_programt::targett &);

void add_exception_dispatch_sequence(
const goto_functionst::function_mapt::iterator &,
const irep_idt &function_id,
goto_programt &goto_program,
const goto_programt::targett &instr_it,
const stack_catcht &stack_catch,
const std::vector<exprt> &locals);

void instrument_throw(
const goto_functionst::function_mapt::iterator &,
const irep_idt &function_id,
goto_programt &goto_program,
const goto_programt::targett &,
const stack_catcht &,
const std::vector<exprt> &);

void instrument_function_call(
const goto_functionst::function_mapt::iterator &,
const irep_idt &function_id,
goto_programt &goto_program,
const goto_programt::targett &,
const stack_catcht &,
const std::vector<exprt> &);

void instrument_exceptions(
const goto_functionst::function_mapt::iterator &);
const irep_idt &function_id,
goto_programt &goto_program);
};

/// adds exceptional return variables for every function that may escape
/// exceptions
void remove_exceptionst::add_exceptional_returns(
const goto_functionst::function_mapt::iterator &func_it)
const irep_idt &function_id,
goto_programt &goto_program)
{
const irep_idt &function_id=func_it->first;
goto_programt &goto_program=func_it->second.body;

auto maybe_symbol=symbol_table.lookup(function_id);
INVARIANT(maybe_symbol, "functions should be recorded in the symbol table");
Expand Down Expand Up @@ -236,17 +242,17 @@ void remove_exceptionst::add_exceptional_returns(
/// Translates an exception landing-pad into instructions that copy the
/// in-flight exception pointer to a nominated expression, then clear the
/// in-flight exception (i.e. null the pointer), hence marking it caught.
/// \param func_it: iterator pointing to the function containing this
/// landingpad instruction
/// \param instr_it [in, out]: iterator pointing to the landingpad instruction.
/// \param function_id: name of the function containing this landingpad
/// instruction
/// \param goto_program: body of the function containing this landingpad
/// instruction
/// \param instr_it: iterator pointing to the landingpad instruction.
/// Will be overwritten.
void remove_exceptionst::instrument_exception_handler(
const goto_functionst::function_mapt::iterator &func_it,
const irep_idt &function_id,
goto_programt &goto_program,
const goto_programt::targett &instr_it)
{
const irep_idt &function_id=func_it->first;
goto_programt &goto_program=func_it->second.body;

PRECONDITION(instr_it->type==CATCH);

// retrieve the exception variable
Expand Down Expand Up @@ -285,20 +291,19 @@ void remove_exceptionst::instrument_exception_handler(
/// if (exception instanceof ExnA) then goto handlerA
/// else if (exception instanceof ExnB) then goto handlerB
/// else goto universal_handler or (dead locals; function exit)
/// \param func_it: iterator pointing to function instr_it belongs to
/// \param function_id: name of the function to which instr_it belongs
/// \param goto_program: body of the function to which instr_it belongs
/// \param instr_it: throw or call instruction that may be an
/// exception source
/// \param stack_catch: exception handlers currently registered
/// \param locals: local variables to kill on a function-exit edge
void remove_exceptionst::add_exception_dispatch_sequence(
const goto_functionst::function_mapt::iterator &func_it,
const irep_idt &function_id,
goto_programt &goto_program,
const goto_programt::targett &instr_it,
const remove_exceptionst::stack_catcht &stack_catch,
const std::vector<exprt> &locals)
{
const irep_idt &function_id=func_it->first;
goto_programt &goto_program=func_it->second.body;

// Unless we have a universal exception handler, jump to end of function
// if not caught:
goto_programt::targett default_target=goto_program.get_end_function();
Expand Down Expand Up @@ -343,6 +348,9 @@ void remove_exceptionst::add_exception_dispatch_sequence(

binary_predicate_exprt check(exc_thrown, ID_java_instanceof, expr);
t_exc->guard=check;

if(remove_added_instanceof)
remove_instanceof(t_exc, goto_program, symbol_table);
}
}
}
Expand All @@ -360,10 +368,11 @@ void remove_exceptionst::add_exception_dispatch_sequence(
}
}

/// instruments each throw with conditional GOTOS to the corresponding
/// instruments each throw with conditional GOTOS to the corresponding
/// exception handlers
void remove_exceptionst::instrument_throw(
const goto_functionst::function_mapt::iterator &func_it,
const irep_idt &function_id,
goto_programt &goto_program,
const goto_programt::targett &instr_it,
const remove_exceptionst::stack_catcht &stack_catch,
const std::vector<exprt> &locals)
Expand All @@ -383,11 +392,11 @@ void remove_exceptionst::instrument_throw(
return;

add_exception_dispatch_sequence(
func_it, instr_it, stack_catch, locals);
function_id, goto_program, instr_it, stack_catch, locals);

// find the symbol where the thrown exception should be stored:
const symbolt &exc_symbol=
symbol_table.lookup_ref(id2string(func_it->first)+EXC_SUFFIX);
const symbolt &exc_symbol =
symbol_table.lookup_ref(id2string(function_id) + EXC_SUFFIX);
symbol_exprt exc_thrown=exc_symbol.symbol_expr();

// add the assignment with the appropriate cast
Expand All @@ -401,16 +410,14 @@ void remove_exceptionst::instrument_throw(
/// instruments each function call that may escape exceptions with conditional
/// GOTOS to the corresponding exception handlers
void remove_exceptionst::instrument_function_call(
const goto_functionst::function_mapt::iterator &func_it,
const irep_idt &function_id,
goto_programt &goto_program,
const goto_programt::targett &instr_it,
const stack_catcht &stack_catch,
const std::vector<exprt> &locals)
{
PRECONDITION(instr_it->type==FUNCTION_CALL);

goto_programt &goto_program=func_it->second.body;
const irep_idt &function_id=func_it->first;

// save the address of the next instruction
goto_programt::targett next_it=instr_it;
next_it++;
Expand All @@ -430,7 +437,7 @@ void remove_exceptionst::instrument_function_call(
if(callee_inflight_exception && local_inflight_exception)
{
add_exception_dispatch_sequence(
func_it, instr_it, stack_catch, locals);
function_id, goto_program, instr_it, stack_catch, locals);

const symbol_exprt callee_inflight_exception_expr=
callee_inflight_exception->symbol_expr();
Expand Down Expand Up @@ -463,12 +470,12 @@ void remove_exceptionst::instrument_function_call(
/// handlers. Additionally, it re-computes the live-range of local variables in
/// order to add DEAD instructions.
void remove_exceptionst::instrument_exceptions(
const goto_functionst::function_mapt::iterator &func_it)
const irep_idt &function_id,
goto_programt &goto_program)
{
stack_catcht stack_catch; // stack of try-catch blocks
std::vector<std::vector<exprt>> stack_locals; // stack of local vars
std::vector<exprt> locals;
goto_programt &goto_program=func_it->second.body;

if(goto_program.empty())
return;
Expand All @@ -486,7 +493,7 @@ void remove_exceptionst::instrument_exceptions(
// Is it an exception landing pad (start of a catch block)?
if(statement==ID_exception_landingpad)
{
instrument_exception_handler(func_it, instr_it);
instrument_exception_handler(function_id, goto_program, instr_it);
}
// Is it a catch handler pop?
else if(statement==ID_pop_catch)
Expand Down Expand Up @@ -551,39 +558,43 @@ void remove_exceptionst::instrument_exceptions(
}
else if(instr_it->type==THROW)
{
instrument_throw(func_it, instr_it, stack_catch, locals);
instrument_throw(
function_id, goto_program, instr_it, stack_catch, locals);
}
else if(instr_it->type==FUNCTION_CALL)
{
instrument_function_call(func_it, instr_it, stack_catch, locals);
instrument_function_call(
function_id, goto_program, instr_it, stack_catch, locals);
}
}
}

void remove_exceptionst::operator()(goto_functionst &goto_functions)
{
Forall_goto_functions(it, goto_functions)
add_exceptional_returns(it);
add_exceptional_returns(it->first, it->second.body);
Forall_goto_functions(it, goto_functions)
instrument_exceptions(it);
instrument_exceptions(it->first, it->second.body);
}

/// removes throws/CATCH-POP/CATCH-PUSH
void remove_exceptions(
symbol_tablet &symbol_table,
goto_functionst &goto_functions)
goto_functionst &goto_functions,
remove_exceptions_typest type)
{
const namespacet ns(symbol_table);
std::map<irep_idt, std::set<irep_idt>> exceptions_map;
uncaught_exceptions(goto_functions, ns, exceptions_map);
remove_exceptionst remove_exceptions(symbol_table, exceptions_map);
remove_exceptionst remove_exceptions(
symbol_table,
exceptions_map,
type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);
remove_exceptions(goto_functions);
}

/// removes throws/CATCH-POP/CATCH-PUSH
void remove_exceptions(goto_modelt &goto_model)
void remove_exceptions(goto_modelt &goto_model, remove_exceptions_typest type)
{
remove_exceptions(
goto_model.symbol_table,
goto_model.goto_functions);
remove_exceptions(goto_model.symbol_table, goto_model.goto_functions, type);
}
12 changes: 10 additions & 2 deletions src/goto-programs/remove_exceptions.h
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,15 @@ Date: December 2016
// Removes 'throw x' and CATCH-PUSH/CATCH-POP
// and adds the required instrumentation (GOTOs and assignments)

void remove_exceptions(symbol_tablet &, goto_functionst &);
void remove_exceptions(goto_modelt &);
enum class remove_exceptions_typest
{
REMOVE_ADDED_INSTANCEOF,
DONT_REMOVE_INSTANCEOF,
};
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this more than a Boolean?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I favour keeping the enum since it makes the callsite clearer

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, makes sense, but might warrant a comment to clarify that that's the sole intent?


void remove_exceptions(
goto_modelt &goto_model,
remove_exceptions_typest type =
remove_exceptions_typest::DONT_REMOVE_INSTANCEOF);

#endif
31 changes: 26 additions & 5 deletions src/goto-programs/remove_instanceof.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -28,16 +28,17 @@ class remove_instanceoft
class_hierarchy(symbol_table);
}

// Lower instanceof for a single functions
// Lower instanceof for a single function
bool lower_instanceof(goto_programt &);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Question to compiler experts: is "lowering" a well-defined technical term? I would have used "translate" or "rewrite".

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, for example http://www.drdobbs.com/architecture-and-design/so-you-want-to-write-your-own-language/240165488?pgno=2 -- "rewriting more complex semantic constructs in terms of simpler ones", here "instanceof" in terms of classid equality comparisons.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not that I consider Dr Dobbs an authoritative reference, but ok. But then you made me search and it seems that GCC and LLVM do use that terminology. So maybe not Dragon-book style, but apparently common in practice.


// Lower instanceof for a single instruction
bool lower_instanceof(goto_programt &, goto_programt::targett);

protected:
symbol_tablet &symbol_table;
namespacet ns;
class_hierarchyt class_hierarchy;

bool lower_instanceof(goto_programt &, goto_programt::targett);

std::size_t lower_instanceof(
exprt &, goto_programt &, goto_programt::targett);
};
Expand Down Expand Up @@ -168,9 +169,24 @@ bool remove_instanceoft::lower_instanceof(goto_programt &goto_program)
}


/// 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.
/// \param target: The instruction to work on.
/// \param goto_program: The function body containing the instruction.
/// \param symbol_table: The symbol table to add symbols to.
void remove_instanceof(
goto_programt::targett target,
goto_programt &goto_program,
symbol_tablet &symbol_table)
{
remove_instanceoft rem(symbol_table);
rem.lower_instanceof(goto_program, target);
}

/// Replace every instanceof in the passed function with an explicit
/// class-identifier test.
/// Extra auxiliary variables may be introduced into symbol_table.
/// \remarks Extra auxiliary variables may be introduced into symbol_table.
/// \param function: The function to work on.
/// \param symbol_table: The symbol table to add symbols to.
void remove_instanceof(
Expand All @@ -183,7 +199,7 @@ void remove_instanceof(

/// Replace every instanceof in every function with an explicit
/// class-identifier test.
/// Extra auxiliary variables may be introduced into symbol_table.
/// \remarks Extra auxiliary variables may be introduced into symbol_table.
/// \param goto_functions: The functions to work on.
/// \param symbol_table: The symbol table to add symbols to.
void remove_instanceof(
Expand All @@ -198,6 +214,11 @@ void remove_instanceof(
goto_functions.compute_location_numbers();
}

/// Replace every instanceof in every function with an explicit
/// class-identifier test.
/// \remarks Extra auxiliary variables may be introduced into symbol_table.
/// \param goto_model: The functions to work on and the symbol table to add
/// symbols to.
void remove_instanceof(goto_modelt &goto_model)
{
remove_instanceof(goto_model.goto_functions, goto_model.symbol_table);
Expand Down
5 changes: 5 additions & 0 deletions src/goto-programs/remove_instanceof.h
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,11 @@ Author: Chris Smowton, [email protected]
#include "goto_functions.h"
#include "goto_model.h"

void remove_instanceof(
goto_programt::targett target,
goto_programt &goto_program,
symbol_tablet &symbol_table);

void remove_instanceof(
goto_functionst::goto_functiont &function,
symbol_tablet &symbol_table);
Expand Down
Loading