Do lowering of java_new as a function-level pass

Author: NathanJPhillips

src/clobber/clobber_parse_options.cpp

@@ -32,6 +32,7 @@ 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>
 
@@ -207,6 +208,8 @@ 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,6 +37,7 @@ 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>
@@ -735,6 +736,8 @@ 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,6 +37,7 @@ 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>
 
@@ -394,6 +395,8 @@ 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,6 +45,7 @@ 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

@@ -33,6 +33,7 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/string_constant.h>
 
 #include "format_strings.h"
+#include "class_identifier.h"
 
 void goto_convertt::do_prob_uniform(
   const exprt &lhs,
@@ -539,68 +540,6 @@ void goto_convertt::do_cpp_new(
   dest.destructive_append(tmp_initializer);
 }
 
-void set_class_identifier(
-  struct_exprt &expr,
-  const namespacet &ns,
-  const symbol_typet &class_type)
-{
-  const struct_typet &struct_type=
-    to_struct_type(ns.follow(expr.type()));
-  const struct_typet::componentst &components=struct_type.components();
-
-  if(components.empty())
-    return;
-  assert(!expr.operands().empty());
-
-  if(components.front().get_name()=="@class_identifier")
-  {
-    assert(expr.op0().id()==ID_constant);
-    expr.op0()=constant_exprt(class_type.get_identifier(), string_typet());
-  }
-  else
-  {
-    assert(expr.op0().id()==ID_struct);
-    set_class_identifier(to_struct_expr(expr.op0()), ns, class_type);
-  }
-}
-
-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/class_identifier.cpp

@@ -71,3 +71,39 @@ exprt get_class_identifier_field(
   exprt deref=dereference_exprt(this_expr, this_expr.type().subtype());
   return build_class_identifier(deref, ns);
 }
+
+/// If expr has its components filled in then sets the `@class_identifier`
+/// member of the struct
+/// \remarks Follows through base class members until it gets to the object
+/// type that contains the `@class_identifier` member
+/// \param expr: An expression that represents a struct
+/// \param ns: The namespace used to resolve symbol referencess in the type of
+/// the struct
+/// \param class_type: A symbol whose identifier is the name of the class
+void set_class_identifier(
+  struct_exprt &expr,
+  const namespacet &ns,
+  const symbol_typet &class_type)
+{
+  const struct_typet &struct_type=to_struct_type(ns.follow(expr.type()));
+  const struct_typet::componentst &components=struct_type.components();
+
+  if(components.empty())
+    // Presumably this means the type has not yet been determined
+    return;
+  PRECONDITION(!expr.operands().empty());
+
+  if(components.front().get_name()=="@class_identifier")
+  {
+    INVARIANT(
+      expr.op0().id()==ID_constant, "@class_identifier must be a constant");
+    expr.op0()=constant_exprt(class_type.get_identifier(), string_typet());
+  }
+  else
+  {
+    // The first member must be the base class
+    INVARIANT(
+      expr.op0().id()==ID_struct, "Non @class_identifier must be a structure");
+    set_class_identifier(to_struct_expr(expr.op0()), ns, class_type);
+  }
+}

src/goto-programs/class_identifier.h

@@ -15,10 +15,16 @@ Author: Chris Smowton, [email protected]
 class exprt;
 class namespacet;
 class symbol_typet;
+class struct_exprt;
 
 exprt get_class_identifier_field(
   const exprt &this_expr,
   const symbol_typet &suggested_type,
   const namespacet &ns);
 
+void set_class_identifier(
+  struct_exprt &expr,
+  const namespacet &ns,
+  const symbol_typet &class_type);
+
 #endif

src/goto-programs/goto_convert.cpp

@@ -756,10 +756,7 @@ void goto_convertt::convert_assign(
   else if(rhs.id()==ID_side_effect &&
           rhs.get(ID_statement)==ID_java_new)
   {
-    Forall_operands(it, rhs)
-      clean_expr(*it, dest);
-
-    do_java_new(lhs, to_side_effect_expr(rhs), dest);
+    copy(code, ASSIGN, dest);
   }
   else if(rhs.id()==ID_side_effect &&
           rhs.get(ID_statement)==ID_java_new_array)

src/goto-programs/goto_convert_class.h

@@ -142,11 +142,6 @@ 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

@@ -0,0 +1,105 @@
+// 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 <util/message.h>
+#include <util/pointer_offset_size.h>
+#include <linking/zero_initializer.h>
+
+#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<code_assignt>(target->code);
+    if(assign==nullptr)
+      continue;
+    side_effect_exprt *rhs=
+      expr_try_dynamic_cast<side_effect_exprt>(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<struct_exprt>(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);
+}

src/goto-programs/remove_java_new.h

@@ -0,0 +1,29 @@
+// 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

src/jbmc/jbmc_parse_options.cpp

@@ -50,6 +50,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/show_properties.h>
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
+#include <goto-programs/remove_java_new.h>
 
 #include <goto-symex/rewrite_union.h>
 #include <goto-symex/adjust_float_expressions.h>
@@ -675,6 +676,8 @@ bool jbmc_parse_optionst::process_goto_functions(
 {
   try
   {
+    remove_java_new(goto_model, get_message_handler());
+
     // add the library
     link_to_library(goto_model, get_message_handler());