Skip to content

Refactor in java bytecode instrument [TG-2331] #1777

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.

Sign up for GitHub

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 5 commits into from
Feb 22, 2018
Merged

Refactor in java bytecode instrument [TG-2331] #1777

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
f6488d7
Using constant string vector instead of irep_idt
romainbrenguier Jan 25, 2018
ea3ba42
Remove unused includes
romainbrenguier Jan 25, 2018
9c838a1
Documentation improvements in bytecode instrument
romainbrenguier Jan 25, 2018
b0df38d
Make return type of expr_instrumentation an optional
romainbrenguier Jan 26, 2018
7e176f7
Make argument of instrument_code be of type codet
romainbrenguier Jan 26, 2018
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
83 changes: 36 additions & 47 deletions src/java_bytecode/java_bytecode_instrument.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,15 +14,11 @@ Date: June 2017
#include <util/fresh_symbol.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <util/symbol_table.h>
#include <util/c_types.h>

#include <goto-programs/goto_functions.h>

#include "java_bytecode_convert_class.h"
#include "java_entry_point.h"
#include "java_root_class.h"
#include "java_types.h"
#include "java_utils.h"

class java_bytecode_instrumentt:public messaget
Expand All @@ -39,7 +35,7 @@ class java_bytecode_instrumentt:public messaget
{
}

void operator()(exprt &expr);
void operator()(codet &code);

protected:
symbol_table_baset &symbol_table;
Expand Down Expand Up @@ -73,29 +69,26 @@ class java_bytecode_instrumentt:public messaget
const exprt &length,
const source_locationt &original_loc);

void instrument_code(exprt &expr);
void instrument_code(codet &code);
void add_expr_instrumentation(code_blockt &block, const exprt &expr);
void prepend_instrumentation(codet &code, code_blockt &instrumentation);
codet instrument_expr(const exprt &expr);
optionalt<codet> instrument_expr(const exprt &expr);
};


const std::vector<irep_idt> exception_needed_classes =
{
const std::vector<std::string> exception_needed_classes = { // NOLINT
"java.lang.ArithmeticException",
"java.lang.ArrayIndexOutOfBoundsException",
"java.lang.ClassCastException",
"java.lang.NegativeArraySizeException",
"java.lang.NullPointerException"
};
"java.lang.NullPointerException"};
Copy link
Contributor

Choose a reason for hiding this comment

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

The existing brace style seems more consistent with our usual style, but I guess clang-format wouldn't take it?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

clang-format puts it that way, but it's one of those cases where clang-format and cpp-lint disagree


/// Creates a class stub for exc_name and generates a
/// conditional GOTO such that exc_name is thrown when
/// cond is met.
/// \par parameters: `cond`: condition to be met in order
/// \param cond: condition to be met in order
/// to throw an exception
/// `original_loc`: source location in the original program
/// `exc_name`: the name of the exception to be thrown
/// \param original_loc: source location in the original program
/// \param exc_name: the name of the exception to be thrown
/// \return Returns the code initialising the throwing the
/// exception
codet java_bytecode_instrumentt::throw_exception(
Expand Down Expand Up @@ -178,9 +171,9 @@ codet java_bytecode_instrumentt::check_arithmetic_exception(
/// and throws ArrayIndexOutofBoundsException/generates an assertion
/// if necessary; Exceptions are thrown when the `throw_runtime_exceptions`
/// flag is set. Otherwise, assertions are emitted.
/// \par parameters: `array_struct`: the array being accessed
/// `idx`: index into the array
/// `original_loc: source location in the original code
/// \param array_struct: array being accessed
/// \param idx: index into the array
/// \param original_loc: source location in the original code
/// \return Based on the value of the flag `throw_runtime_exceptions`,
/// it returns code that either throws an ArrayIndexOutPfBoundsException
/// or emits an assertion checking the array access
Expand Down Expand Up @@ -223,9 +216,9 @@ codet java_bytecode_instrumentt::check_array_access(
/// ClassCastException/generates an assertion when necessary;
/// Exceptions are thrown when the `throw_runtime_exceptions` flag is set.
/// Otherwise, assertions are emitted.
/// \par parameters: `class1`: the subclass
/// `class2`: the super class
/// `original_loc: source location in the original code
/// \param class1: the subclass
/// \param class2: the super class
/// \param original_loc: source location in the original code
/// \return Based on the value of the flag `throw_runtime_exceptions`,
/// it returns code that either throws an ClassCastException or emits an
/// assertion checking the subtype relation
Expand Down Expand Up @@ -272,7 +265,7 @@ codet java_bytecode_instrumentt::check_class_cast(
/// generates an assertion when necessary;
/// Exceptions are thrown when the `throw_runtime_exceptions` flag is set.
/// Otherwise, assertions are emitted.
/// \par parameters: `expr`: the checked expression
/// \param expr: the checked expression
/// `original_loc: source location in the original code
/// \return Based on the value of the flag `throw_runtime_exceptions`,
/// it returns code that either throws an NullPointerException or emits an
Expand Down Expand Up @@ -302,8 +295,8 @@ codet java_bytecode_instrumentt::check_null_dereference(
/// generates an assertion when necessary;
/// Exceptions are thrown when the `throw_runtime_exceptions` flag is set.
/// Otherwise, assertions are emitted.
/// \par parameters: `length`: the checked length
/// `original_loc: source location in the original code
/// \param length: the checked length
/// \param original_loc: source location in the original code
/// \return Based on the value of the flag `throw_runtime_exceptions`,
/// it returns code that either throws an NegativeArraySizeException
/// or emits an assertion checking the subtype relation
Expand Down Expand Up @@ -335,13 +328,12 @@ void java_bytecode_instrumentt::add_expr_instrumentation(
code_blockt &block,
const exprt &expr)
{
codet expr_instrumentation=instrument_expr(expr);
if(expr_instrumentation!=code_skipt())
if(optionalt<codet> expr_instrumentation = instrument_expr(expr))
{
if(expr_instrumentation.get_statement()==ID_block)
block.append(to_code_block(expr_instrumentation));
if(expr_instrumentation->get_statement() == ID_block)
block.append(to_code_block(*expr_instrumentation));
else
block.move_to_operands(expr_instrumentation);
block.move_to_operands(*expr_instrumentation);
}
}

Expand All @@ -365,10 +357,9 @@ void java_bytecode_instrumentt::prepend_instrumentation(

/// Augments `expr` with instrumentation in the form of either
/// assertions or runtime exceptions
/// \par parameters: `expr`: the expression to be instrumented
void java_bytecode_instrumentt::instrument_code(exprt &expr)
/// \param `expr` the expression to be instrumented
void java_bytecode_instrumentt::instrument_code(codet &code)
{
codet &code=to_code(expr);
source_locationt old_source_location=code.source_location();

const irep_idt &statement=code.get_statement();
Expand Down Expand Up @@ -480,19 +471,17 @@ void java_bytecode_instrumentt::instrument_code(exprt &expr)

/// Computes the instrumentation for `expr` in the form of
/// either assertions or runtime exceptions.
/// \par parameters: `expr`: the expression for which we compute
/// \param expr: the expression for which we compute
/// instrumentation
/// \return: The instrumentation required for `expr`
codet java_bytecode_instrumentt::instrument_expr(
const exprt &expr)
/// \return: The instrumentation for `expr` if required
optionalt<codet> java_bytecode_instrumentt::instrument_expr(const exprt &expr)
{
code_blockt result;
// First check our operands:
forall_operands(it, expr)
{
codet op_result=instrument_expr(*it);
if(op_result!=code_skipt())
result.move_to_operands(op_result);
if(optionalt<codet> op_result = instrument_expr(*it))
result.move_to_operands(*op_result);
}

// Add any check due at this node:
Expand Down Expand Up @@ -524,7 +513,7 @@ codet java_bytecode_instrumentt::instrument_expr(
const irep_idt &statement=side_effect_expr.get_statement();
if(statement==ID_throw)
{
// this corresponds to athrow and so we check that
// this corresponds to a throw and so we check that
// we don't throw null
result.copy_to_operands(
check_null_dereference(
Expand All @@ -533,7 +522,7 @@ codet java_bytecode_instrumentt::instrument_expr(
}
else if(statement==ID_java_new_array)
{
// this correpond to new array so we check that
// this corresponds to new array so we check that
// length is >=0
result.copy_to_operands(
check_array_length(
Expand Down Expand Up @@ -563,16 +552,16 @@ codet java_bytecode_instrumentt::instrument_expr(
}

if(result==code_blockt())
return code_skipt();
return {};
else
return result;
}

/// Instruments `expr`
/// \par parameters: `expr`: the expression to be instrumented
void java_bytecode_instrumentt::operator()(exprt &expr)
/// \param expr: the expression to be instrumented
void java_bytecode_instrumentt::operator()(codet &code)
{
instrument_code(expr);
instrument_code(code);
}

/// Instruments the code attached to `symbol` with
Expand Down Expand Up @@ -601,7 +590,7 @@ void java_bytecode_instrument_symbol(
"java_bytecode_instrument expects a code-typed symbol but was called with"
" " + id2string(symbol.name) + " which has a value with an id of " +
id2string(symbol.value.id()));
instrument(symbol.value);
instrument(to_code(symbol.value));
}

/// Instruments all the code in the symbol_table with
Expand Down Expand Up @@ -634,5 +623,5 @@ void java_bytecode_instrument(
// instrument(...) can add symbols to the table, so it's
// not safe to hold a reference to a symbol across a call.
for(const auto &symbol : symbols_to_instrument)
instrument(symbol_table.get_writeable_ref(symbol).value);
instrument(to_code(symbol_table.get_writeable_ref(symbol).value));
}
2 changes: 1 addition & 1 deletion src/java_bytecode/java_bytecode_instrument.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,6 @@ void java_bytecode_instrument(
const bool throw_runtime_exceptions,
message_handlert &_message_handler);

extern const std::vector<irep_idt> exception_needed_classes;
extern const std::vector<std::string> exception_needed_classes;

#endif