From f6488d774eb06eca3976eef4cd8320d03064f366 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 25 Jan 2018 10:17:53 +0000 Subject: [PATCH 1/5] Using constant string vector instead of irep_idt The irep_idt class may not have been initialized when we reach this vector declaration, which could lead to a runtime error. Using a vector of string instead is safe. --- src/java_bytecode/java_bytecode_instrument.cpp | 7 ++----- src/java_bytecode/java_bytecode_instrument.h | 2 +- 2 files changed, 3 insertions(+), 6 deletions(-) diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index b0bb08ef14b..608755b02e4 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -79,15 +79,12 @@ class java_bytecode_instrumentt:public messaget codet instrument_expr(const exprt &expr); }; - -const std::vector exception_needed_classes = -{ +const std::vector exception_needed_classes = { // NOLINT "java.lang.ArithmeticException", "java.lang.ArrayIndexOutOfBoundsException", "java.lang.ClassCastException", "java.lang.NegativeArraySizeException", - "java.lang.NullPointerException" -}; + "java.lang.NullPointerException"}; /// Creates a class stub for exc_name and generates a /// conditional GOTO such that exc_name is thrown when diff --git a/src/java_bytecode/java_bytecode_instrument.h b/src/java_bytecode/java_bytecode_instrument.h index cb5102fb49d..075b6467765 100644 --- a/src/java_bytecode/java_bytecode_instrument.h +++ b/src/java_bytecode/java_bytecode_instrument.h @@ -26,6 +26,6 @@ void java_bytecode_instrument( const bool throw_runtime_exceptions, message_handlert &_message_handler); -extern const std::vector exception_needed_classes; +extern const std::vector exception_needed_classes; #endif From ea3ba42fe57d34593375db6925df35ec35617bac Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 25 Jan 2018 10:19:19 +0000 Subject: [PATCH 2/5] Remove unused includes --- src/java_bytecode/java_bytecode_instrument.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index 608755b02e4..0542bb1b871 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -14,15 +14,11 @@ Date: June 2017 #include #include #include -#include #include #include #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 From 9c838a1252c3149ca06e2c24e34c86a987133cbd Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 25 Jan 2018 10:19:57 +0000 Subject: [PATCH 3/5] Documentation improvements in bytecode instrument --- .../java_bytecode_instrument.cpp | 34 +++++++++---------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index 0542bb1b871..343f1c6b18a 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -85,10 +85,10 @@ const std::vector exception_needed_classes = { // NOLINT /// 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( @@ -171,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 @@ -216,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 @@ -265,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 @@ -295,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 @@ -358,7 +358,7 @@ 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 +/// \param `expr` the expression to be instrumented void java_bytecode_instrumentt::instrument_code(exprt &expr) { codet &code=to_code(expr); @@ -473,7 +473,7 @@ 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( @@ -517,7 +517,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( @@ -526,7 +526,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( @@ -562,7 +562,7 @@ codet java_bytecode_instrumentt::instrument_expr( } /// Instruments `expr` -/// \par parameters: `expr`: the expression to be instrumented +/// \param expr: the expression to be instrumented void java_bytecode_instrumentt::operator()(exprt &expr) { instrument_code(expr); From b0df38d3241692b65e881c74347bdfe0d487ff3e Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 26 Jan 2018 17:59:09 +0000 Subject: [PATCH 4/5] Make return type of expr_instrumentation an optional --- .../java_bytecode_instrument.cpp | 23 ++++++++----------- 1 file changed, 10 insertions(+), 13 deletions(-) diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index 343f1c6b18a..694c7f492eb 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -72,7 +72,7 @@ class java_bytecode_instrumentt:public messaget void instrument_code(exprt &expr); 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 instrument_expr(const exprt &expr); }; const std::vector exception_needed_classes = { // NOLINT @@ -328,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 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); } } @@ -475,17 +474,15 @@ void java_bytecode_instrumentt::instrument_code(exprt &expr) /// either assertions or runtime exceptions. /// \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 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 op_result = instrument_expr(*it)) + result.move_to_operands(*op_result); } // Add any check due at this node: @@ -556,7 +553,7 @@ codet java_bytecode_instrumentt::instrument_expr( } if(result==code_blockt()) - return code_skipt(); + return {}; else return result; } From 7e176f7aea65af0382b054f84c25ba2e0a6ce7f4 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 26 Jan 2018 18:05:58 +0000 Subject: [PATCH 5/5] Make argument of instrument_code be of type codet --- src/java_bytecode/java_bytecode_instrument.cpp | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index 694c7f492eb..ef302e1c9c5 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -35,7 +35,7 @@ class java_bytecode_instrumentt:public messaget { } - void operator()(exprt &expr); + void operator()(codet &code); protected: symbol_table_baset &symbol_table; @@ -69,7 +69,7 @@ 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); optionalt instrument_expr(const exprt &expr); @@ -358,9 +358,8 @@ void java_bytecode_instrumentt::prepend_instrumentation( /// Augments `expr` with instrumentation in the form of either /// assertions or runtime exceptions /// \param `expr` the expression to be instrumented -void java_bytecode_instrumentt::instrument_code(exprt &expr) +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(); @@ -560,9 +559,9 @@ optionalt java_bytecode_instrumentt::instrument_expr(const exprt &expr) /// Instruments `expr` /// \param expr: the expression to be instrumented -void java_bytecode_instrumentt::operator()(exprt &expr) +void java_bytecode_instrumentt::operator()(codet &code) { - instrument_code(expr); + instrument_code(code); } /// Instruments the code attached to `symbol` with @@ -591,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 @@ -624,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)); }