Merge pull request #1793 from smowton/smowton/cleanup/remove-java-new-lowering-pass

Revert "Do lowering of java_new as a function-level pass"

Author: smowton

src/clobber/clobber_parse_options.cpp

@@ -32,7 +32,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/xml_goto_trace.h>
-#include <goto-programs/remove_java_new.h>
 
 #include <goto-instrument/dump_c.h>
 
@@ -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());

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -37,7 +37,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/link_to_library.h>
-#include <goto-programs/remove_java_new.h>
 
 #include <analyses/is_threaded.h>
 #include <analyses/goto_check.h>
@@ -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(

src/goto-diff/goto_diff_parse_options.cpp

@@ -37,7 +37,6 @@ Author: Peter Schrammel
 #include <goto-programs/string_instrumentation.h>
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/link_to_library.h>
-#include <goto-programs/remove_java_new.h>
 
 #include <pointer-analysis/add_failed_symbols.h>
 
@@ -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);

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 \

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,

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)

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,

src/goto-programs/remove_java_new.cpp

@@ -44,7 +44,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_symbol_table.h>
 #include <goto-programs/show_properties.h>
-#include <goto-programs/remove_java_new.h>
 
 #include <goto-symex/adjust_float_expressions.h>
 
@@ -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);