Merge pull request #3837 from tautschnig/function-remove_java_new

remove_java_new now takes function identifier [blocks: #3126]

Author: tautschnig

jbmc/src/java_bytecode/remove_java_new.cpp

@@ -33,23 +33,27 @@ class remove_java_newt : public messaget
   }
 
   // Lower java_new for a single function
-  bool lower_java_new(goto_programt &);
+  bool lower_java_new(const irep_idt &function_identifier, goto_programt &);
 
   // Lower java_new for a single instruction
-  goto_programt::targett
-  lower_java_new(goto_programt &, goto_programt::targett);
+  goto_programt::targett lower_java_new(
+    const irep_idt &function_identifier,
+    goto_programt &,
+    goto_programt::targett);
 
 protected:
   symbol_table_baset &symbol_table;
   namespacet ns;
 
   goto_programt::targett lower_java_new(
+    const irep_idt &function_identifier,
     exprt lhs,
     side_effect_exprt rhs,
     goto_programt &,
     goto_programt::targett);
 
   goto_programt::targett lower_java_new_array(
+    const irep_idt &function_identifier,
     exprt lhs,
     side_effect_exprt rhs,
     goto_programt &,
@@ -60,6 +64,7 @@ class remove_java_newt : public messaget
 /// two instructions:
 ///   lhs = ALLOCATE(java_type)
 ///   *lhs = { zero-initialized java_type }
+/// \param function_identifier: Name of the function containing \p target.
 /// \param lhs: the lhs
 /// \param rhs: the rhs
 /// \param dest: the goto program to modify
@@ -68,6 +73,7 @@ class remove_java_newt : public messaget
 /// Note: we have to take a copy of `lhs` and `rhs` since they would suffer
 ///   destruction when replacing the instruction.
 goto_programt::targett remove_java_newt::lower_java_new(
+  const irep_idt &function_identifier,
   exprt lhs,
   side_effect_exprt rhs,
   goto_programt &dest,
@@ -108,6 +114,7 @@ goto_programt::targett remove_java_newt::lower_java_new(
 /// the following code:
 ///   lhs = ALLOCATE(java_type)
 ///   loops to initialize the elements (including multi-dimensional arrays)
+/// \param function_identifier: Name of the function containing \p target.
 /// \param lhs: the lhs
 /// \param rhs: the rhs
 /// \param dest: the goto program to modify
@@ -116,6 +123,7 @@ goto_programt::targett remove_java_newt::lower_java_new(
 /// Note: we have to take a copy of `lhs` and `rhs` since they would suffer
 ///   destruction when replacing the instruction.
 goto_programt::targett remove_java_newt::lower_java_new_array(
+  const irep_idt &function_identifier,
   exprt lhs,
   side_effect_exprt rhs,
   goto_programt &dest,
@@ -206,7 +214,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
   // `x=typecast_exprt(side_effect_exprt(...))`
   symbol_exprt new_array_data_symbol = get_fresh_aux_symbol(
                                          data_java_new_expr.type(),
-                                         id2string(target->function),
+                                         id2string(function_identifier),
                                          "tmp_new_data_array",
                                          location,
                                          ID_java,
@@ -254,7 +262,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
 
     symbol_exprt tmp_i = get_fresh_aux_symbol(
                            length.type(),
-                           id2string(target->function),
+                           id2string(function_identifier),
                            "tmp_index",
                            location,
                            ID_java,
@@ -286,7 +294,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
     code_blockt for_body;
     symbol_exprt init_sym = get_fresh_aux_symbol(
                               sub_type,
-                              id2string(target->function),
+                              id2string(function_identifier),
                               "subarray_init",
                               location,
                               ID_java,
@@ -311,7 +319,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
     goto_convert(for_loop, symbol_table, tmp, get_message_handler(), ID_java);
 
     // lower new side effects recursively
-    lower_java_new(tmp);
+    lower_java_new(function_identifier, tmp);
 
     dest.destructive_insert(next, tmp);
   }
@@ -321,10 +329,12 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
 
 /// Replace every java_new or java_new_array by a malloc side-effect
 /// and zero initialization.
+/// \param function_identifier: Name of the function containing \p target.
 /// \param goto_program: program to process
 /// \param target: instruction to check for java_new expressions
 /// \return true if a replacement has been made
 goto_programt::targett remove_java_newt::lower_java_new(
+  const irep_idt &function_identifier,
   goto_programt &goto_program,
   goto_programt::targett target)
 {
@@ -338,13 +348,14 @@ goto_programt::targett remove_java_newt::lower_java_new(
 
   if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_java_new)
   {
-    return lower_java_new(lhs, to_side_effect_expr(rhs), goto_program, target);
+    return lower_java_new(
+      function_identifier, lhs, to_side_effect_expr(rhs), goto_program, target);
   }
 
   if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_java_new_array)
   {
     return lower_java_new_array(
-      lhs, to_side_effect_expr(rhs), goto_program, target);
+      function_identifier, lhs, to_side_effect_expr(rhs), goto_program, target);
   }
 
   return target;
@@ -353,17 +364,21 @@ goto_programt::targett remove_java_newt::lower_java_new(
 /// Replace every java_new or java_new_array by a malloc side-effect
 /// and zero initialization.
 /// Extra auxiliary variables may be introduced into symbol_table.
+/// \param function_identifier: Name of the function \p goto_program.
 /// \param goto_program: The function body to work on.
 /// \return true if one or more java_new expressions have been replaced
-bool remove_java_newt::lower_java_new(goto_programt &goto_program)
+bool remove_java_newt::lower_java_new(
+  const irep_idt &function_identifier,
+  goto_programt &goto_program)
 {
   bool changed = false;
   for(goto_programt::instructionst::iterator target =
         goto_program.instructions.begin();
       target != goto_program.instructions.end();
       ++target)
   {
-    goto_programt::targett new_target = lower_java_new(goto_program, target);
+    goto_programt::targett new_target =
+      lower_java_new(function_identifier, goto_program, target);
     changed = changed || new_target == target;
     target = new_target;
   }
@@ -376,33 +391,37 @@ bool remove_java_newt::lower_java_new(goto_programt &goto_program)
 /// Replace every java_new or java_new_array by a malloc side-effect
 /// and zero initialization.
 /// \remarks Extra auxiliary variables may be introduced into symbol_table.
+/// \param function_identifier: Name of the function containing \p target.
 /// \param target: The instruction to work on.
 /// \param goto_program: The function body containing the instruction.
 /// \param symbol_table: The symbol table to add symbols to.
 /// \param message_handler: a message handler
 void remove_java_new(
+  const irep_idt &function_identifier,
   goto_programt::targett target,
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler)
 {
   remove_java_newt rem(symbol_table, message_handler);
-  rem.lower_java_new(goto_program, target);
+  rem.lower_java_new(function_identifier, goto_program, target);
 }
 
 /// Replace every java_new or java_new_array by a malloc side-effect
 /// and zero initialization.
 /// \remarks Extra auxiliary variables may be introduced into symbol_table.
+/// \param function_identifier: Name of the function \p function.
 /// \param function: The function to work on.
 /// \param symbol_table: The symbol table to add symbols to.
 /// \param message_handler: a message handler
 void remove_java_new(
+  const irep_idt &function_identifier,
   goto_functionst::goto_functiont &function,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler)
 {
   remove_java_newt rem(symbol_table, message_handler);
-  rem.lower_java_new(function.body);
+  rem.lower_java_new(function_identifier, function.body);
 }
 
 /// Replace every java_new or java_new_array by a malloc side-effect
@@ -419,7 +438,7 @@ void remove_java_new(
   remove_java_newt rem(symbol_table, message_handler);
   bool changed = false;
   for(auto &f : goto_functions.function_map)
-    changed = rem.lower_java_new(f.second.body) || changed;
+    changed = rem.lower_java_new(f.first, f.second.body) || changed;
   if(changed)
     goto_functions.compute_location_numbers();
 }

jbmc/src/java_bytecode/remove_java_new.h

@@ -20,12 +20,14 @@ Author: Peter Schrammel
 class message_handlert;
 
 void remove_java_new(
+  const irep_idt &function_identifier,
   goto_programt::targett target,
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
   message_handlert &_message_handler);
 
 void remove_java_new(
+  const irep_idt &function_identifier,
   goto_functionst::goto_functiont &function,
   symbol_table_baset &symbol_table,
   message_handlert &_message_handler);

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -811,7 +811,11 @@ void jbmc_parse_optionst::process_goto_function(
       function.get_function_id(), function.get_goto_function(), ns, options);
 
     // Replace Java new side effects
-    remove_java_new(goto_function, symbol_table, get_message_handler());
+    remove_java_new(
+      function.get_function_id(),
+      goto_function,
+      symbol_table,
+      get_message_handler());
 
     // checks don't know about adjusted float expressions
     adjust_float_expressions(goto_function, ns);