diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index 80b9725b8f2..b59cd44fae3 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -32,7 +32,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include @@ -214,8 +213,6 @@ bool clobber_parse_optionst::process_goto_program( goto_modelt &goto_model) { { - remove_java_new(goto_model, get_message_handler()); - // do partial inlining status() << "Partial Inlining" << eom; goto_partial_inline(goto_model, get_message_handler()); diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 1074652f042..9b92bf94cff 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -37,7 +37,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -745,8 +744,6 @@ bool goto_analyzer_parse_optionst::process_goto_program( link_to_library(goto_model, ui_message_handler); #endif - remove_java_new(goto_model, get_message_handler()); - // remove function pointers status() << "Removing function pointers and virtual functions" << eom; remove_function_pointers( diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index c1beca078c0..26809476b35 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -37,7 +37,6 @@ Author: Peter Schrammel #include #include #include -#include #include @@ -412,8 +411,6 @@ bool goto_diff_parse_optionst::process_goto_program( { namespacet ns(symbol_table); - remove_java_new(goto_model, get_message_handler()); - // Remove inline assembler; this needs to happen before // adding the library. remove_asm(goto_model); diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index bf4e5bb2491..38a75637776 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -45,7 +45,6 @@ SRC = basic_blocks.cpp \ remove_exceptions.cpp \ remove_function_pointers.cpp \ remove_instanceof.cpp \ - remove_java_new.cpp \ remove_returns.cpp \ remove_skip.cpp \ remove_static_init_loops.cpp \ diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 6a5826da46d..e4c6fb3849c 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -540,6 +540,43 @@ void goto_convertt::do_cpp_new( dest.destructive_append(tmp_initializer); } +void goto_convertt::do_java_new( + const exprt &lhs, + const side_effect_exprt &rhs, + goto_programt &dest) +{ + PRECONDITION(!lhs.is_nil()); + PRECONDITION(rhs.operands().empty()); + PRECONDITION(rhs.type().id() == ID_pointer); + source_locationt location=rhs.source_location(); + typet object_type=rhs.type().subtype(); + + // build size expression + exprt object_size=size_of_expr(object_type, ns); + CHECK_RETURN(object_size.is_not_nil()); + + // we produce a malloc side-effect, which stays + side_effect_exprt malloc_expr(ID_allocate); + malloc_expr.copy_to_operands(object_size); + // could use true and get rid of the code below + malloc_expr.copy_to_operands(false_exprt()); + malloc_expr.type()=rhs.type(); + + goto_programt::targett t_n=dest.add_instruction(ASSIGN); + t_n->code=code_assignt(lhs, malloc_expr); + t_n->source_location=location; + + // zero-initialize the object + dereference_exprt deref(lhs, object_type); + exprt zero_object= + zero_initializer(object_type, location, ns, get_message_handler()); + set_class_identifier( + to_struct_expr(zero_object), ns, to_symbol_type(object_type)); + goto_programt::targett t_i=dest.add_instruction(ASSIGN); + t_i->code=code_assignt(deref, zero_object); + t_i->source_location=location; +} + void goto_convertt::do_java_new_array( const exprt &lhs, const side_effect_exprt &rhs, diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 23135646621..505cf4c1e79 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -766,7 +766,10 @@ void goto_convertt::convert_assign( else if(rhs.id()==ID_side_effect && rhs.get(ID_statement)==ID_java_new) { - copy(code, ASSIGN, dest); + Forall_operands(it, rhs) + clean_expr(*it, dest); + + do_java_new(lhs, to_side_effect_expr(rhs), dest); } else if(rhs.id()==ID_side_effect && rhs.get(ID_statement)==ID_java_new_array) diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 8944e0dc3e6..1084f8353b1 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -142,6 +142,11 @@ class goto_convertt:public messaget const side_effect_exprt &rhs, goto_programt &dest); + void do_java_new( + const exprt &lhs, + const side_effect_exprt &rhs, + goto_programt &dest); + void do_java_new_array( const exprt &lhs, const side_effect_exprt &rhs, diff --git a/src/goto-programs/remove_java_new.cpp b/src/goto-programs/remove_java_new.cpp deleted file mode 100644 index b7059bbadff..00000000000 --- a/src/goto-programs/remove_java_new.cpp +++ /dev/null @@ -1,105 +0,0 @@ -// Copyright 2017 Diffblue Limited. All Rights Reserved. - -/// \file -/// Function-level/module-level pass to remove java_new and replace with -/// malloc & zero-initialize - -#include "remove_java_new.h" - -#include -#include -#include - -#include "class_identifier.h" - -static bool remove_java_new( - goto_programt &goto_program, - const namespacet &ns, - message_handlert &message_handler) -{ - messaget msg(message_handler); - - bool changed=false; - for(goto_programt::targett target=goto_program.instructions.begin(); - target!=goto_program.instructions.end(); - ++target) - { - code_assignt *assign=expr_try_dynamic_cast(target->code); - if(assign==nullptr) - continue; - side_effect_exprt *rhs= - expr_try_dynamic_cast(assign->rhs()); - if(rhs==nullptr) - continue; - if(rhs->get_statement()!=ID_java_new) - continue; - INVARIANT(rhs->operands().empty(), "java_new does not have operands"); - INVARIANT(rhs->type().id()==ID_pointer, "java_new returns pointer"); - - const exprt &lhs=assign->lhs(); - INVARIANT( - !lhs.is_nil(), "remove_java_new without lhs is yet to be implemented"); - - typet object_type=rhs->type().subtype(); - - // build size expression - exprt object_size=size_of_expr(object_type, ns); - CHECK_RETURN(object_size.is_not_nil()); - - changed=true; - - source_locationt location=rhs->source_location(); - - // We produce a malloc side-effect - side_effect_exprt malloc_expr(ID_allocate); - malloc_expr.copy_to_operands(object_size); - // could use true and get rid of the code below - malloc_expr.copy_to_operands(false_exprt()); - malloc_expr.type()=rhs->type(); - *rhs=std::move(malloc_expr); - - // zero-initialize the object - dereference_exprt deref(lhs, object_type); - exprt zero_object= - zero_initializer(object_type, location, ns, message_handler); - set_class_identifier( - expr_dynamic_cast(zero_object), - ns, - to_symbol_type(object_type)); - goto_programt::targett zi_assign=goto_program.insert_after(target); - zi_assign->make_assignment(); - zi_assign->code=code_assignt(deref, zero_object); - zi_assign->source_location=location; - } - if(!changed) - return false; - goto_program.update(); - return true; -} - -bool remove_java_new( - goto_functionst::goto_functiont &goto_function, - const namespacet &ns, - message_handlert &message_handler) -{ - return remove_java_new(goto_function.body, ns, message_handler); -} - -void remove_java_new( - goto_functionst &goto_functions, - const namespacet &ns, - message_handlert &message_handler) -{ - for(auto &named_fn : goto_functions.function_map) - remove_java_new(named_fn.second, ns, message_handler); -} - -void remove_java_new( - goto_modelt &goto_model, - message_handlert &message_handler) -{ - remove_java_new( - goto_model.goto_functions, - namespacet(goto_model.symbol_table), - message_handler); -} diff --git a/src/goto-programs/remove_java_new.h b/src/goto-programs/remove_java_new.h deleted file mode 100644 index 99263203a0f..00000000000 --- a/src/goto-programs/remove_java_new.h +++ /dev/null @@ -1,29 +0,0 @@ -// Copyright 2017 Diffblue Limited. All Rights Reserved. - -/// \file -/// Function-level/module-level pass to remove java_new and replace with -/// malloc & zero-initialize - -#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_JAVA_NEW_H -#define CPROVER_GOTO_PROGRAMS_REMOVE_JAVA_NEW_H - -#include "goto_model.h" - -class message_handlert; - - -bool remove_java_new( - goto_functionst::goto_functiont &goto_function, - const namespacet &ns, - message_handlert &message_handler); - -void remove_java_new( - goto_functionst &goto_functions, - const namespacet &ns, - message_handlert &message_handler); - -void remove_java_new( - goto_modelt &goto_model, - message_handlert &message_handler); - -#endif // CPROVER_GOTO_PROGRAMS_REMOVE_JAVA_NEW_H diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 29eeb903919..fb5efc6634d 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -44,7 +44,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include @@ -735,9 +734,7 @@ bool jbmc_parse_optionst::process_goto_functions( { try { - remove_java_new(goto_model, get_message_handler()); - - status() << "Removal of virtual functions" << eom; + status() << "Running GOTO functions transformation passes" << eom; // remove catch and throw (introduces instanceof but request it is removed) remove_exceptions( goto_model, remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF); diff --git a/unit/pointer-analysis/custom_value_set_analysis.cpp b/unit/pointer-analysis/custom_value_set_analysis.cpp index db657133a51..b3f64a14476 100644 --- a/unit/pointer-analysis/custom_value_set_analysis.cpp +++ b/unit/pointer-analysis/custom_value_set_analysis.cpp @@ -12,7 +12,6 @@ Author: Chris Smowton, chris@smowton.net #include #include #include -#include #include #include #include @@ -184,9 +183,6 @@ SCENARIO("test_value_set_analysis", namespacet ns(goto_model.symbol_table); - // VSA doesn't currently support java_new as an allocator - remove_java_new(goto_model, null_output); - // Fully inline the test program, to avoid VSA conflating // constructor callsites confusing the results we're trying to check: goto_function_inline(goto_model, TEST_FUNCTION_NAME, null_output);