Add and use fresh_java_symbol function

This prevents forgetting that the basename of the symbol should be the
function identifier.

Author: romainbrenguier

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -15,12 +15,12 @@ Author: Reuben Thomas, [email protected]
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
 
-#include <util/fresh_symbol.h>
 #include <util/irep_ids.h>
 
 #include <memory>
 
 #include "java_object_factory.h" // gen_nondet_init
+#include "java_utils.h"
 
 /// Returns true if `expr` is a nondet pointer that isn't a function pointer or
 /// a void* pointer as these can be meaningfully non-det initialized.
@@ -116,13 +116,8 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
     //   target2: instruction containing op, with op replaced by aux_symbol
     //            dead aux_symbol
 
-    symbolt &aux_symbol = get_fresh_aux_symbol(
-      op.type(),
-      id2string(function_identifier),
-      "nondet_tmp",
-      source_loc,
-      ID_java,
-      symbol_table);
+    symbolt &aux_symbol = fresh_java_symbol(
+      op.type(), "nondet_tmp", source_loc, function_identifier, symbol_table);
 
     const symbol_exprt aux_symbol_expr = aux_symbol.symbol_expr();
     op = aux_symbol_expr;

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -9,12 +9,12 @@ Author: Kurt Degiogrio, [email protected]
 #include "java_bytecode_concurrency_instrumentation.h"
 #include "expr2java.h"
 #include "java_types.h"
+#include "java_utils.h"
 
 #include <util/expr_iterator.h>
 #include <util/namespace.h>
 #include <util/cprover_prefix.h>
 #include <util/std_types.h>
-#include <util/fresh_symbol.h>
 #include <util/arith_tools.h>
 
 // Disable linter to allow an std::string constant.
@@ -229,12 +229,11 @@ static void instrument_synchronized_code(
   code_pop_catcht catch_pop;
 
   // Create the finally block with the same label targeted in the catch-push
-  const symbolt &tmp_symbol = get_fresh_aux_symbol(
+  const symbolt &tmp_symbol = fresh_java_symbol(
     java_reference_type(struct_tag_typet("java::java.lang.Throwable")),
-    id2string(symbol.name),
     "caught-synchronized-exception",
     code.source_location(),
-    ID_java,
+    id2string(symbol.name),
     symbol_table);
   symbol_exprt catch_var(tmp_symbol.name, tmp_symbol.type);
   catch_var.set(ID_C_base_name, tmp_symbol.base_name);

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

@@ -11,7 +11,6 @@ Date:   June 2017
 #include "java_bytecode_instrument.h"
 
 #include <util/arith_tools.h>
-#include <util/fresh_symbol.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/c_types.h>
@@ -112,14 +111,12 @@ code_ifthenelset java_bytecode_instrumentt::throw_exception(
 
   // Allocate and throw an instance of the exception class:
 
-  symbolt &new_symbol=
-    get_fresh_aux_symbol(
-      exc_ptr_type,
-      "new_exception",
-      "new_exception",
-      original_loc,
-      ID_java,
-      symbol_table);
+  symbolt &new_symbol = fresh_java_symbol(
+    exc_ptr_type,
+    "new_exception",
+    original_loc,
+    original_loc.get_function(),
+    symbol_table);
 
   side_effect_exprt new_instance(ID_java_new, exc_ptr_type, original_loc);
   code_assignt assign_new(new_symbol.symbol_expr(), new_instance);

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -9,7 +9,6 @@ Author: Daniel Kroening, [email protected]
 #include "java_object_factory.h"
 
 #include <util/expr_initializer.h>
-#include <util/fresh_symbol.h>
 #include <util/nondet_bool.h>
 #include <util/nondet.h>
 #include <util/pointer_offset_size.h>
@@ -20,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include "generic_parameter_specialization_map_keys.h"
 #include "java_root_class.h"
 #include "java_string_literals.h"
+#include "java_utils.h"
 
 class java_object_factoryt
 {
@@ -442,13 +442,8 @@ void initialize_nondet_string_fields(
 
   /// \todo Refactor with make_nondet_string_expr
   // length_expr = nondet(int);
-  const symbolt length_sym = get_fresh_aux_symbol(
-    java_int_type(),
-    id2string(function_id),
-    "tmp_object_factory",
-    loc,
-    ID_java,
-    symbol_table);
+  const symbolt length_sym = fresh_java_symbol(
+    java_int_type(), "tmp_object_factory", loc, function_id, symbol_table);
   const symbol_exprt length_expr = length_sym.symbol_expr();
   const side_effect_expr_nondett nondet_length(length_expr.type(), loc);
   code.add(code_declt(length_expr));
@@ -745,12 +740,11 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
   size_t depth,
   const source_locationt &location)
 {
-  symbolt new_symbol = get_fresh_aux_symbol(
+  symbolt new_symbol = fresh_java_symbol(
     replacement_pointer,
-    id2string(object_factory_parameters.function_id),
     "tmp_object_factory",
-    loc,
-    ID_java,
+    location,
+    object_factory_parameters.function_id,
     symbol_table);
 
   // Generate a new object into this new symbol

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -251,12 +251,11 @@ symbol_exprt java_string_library_preprocesst::fresh_array(
   const source_locationt &location,
   symbol_tablet &symbol_table)
 {
-  symbolt array_symbol=get_fresh_aux_symbol(
+  symbolt array_symbol = fresh_java_symbol(
     type,
     "cprover_string_array",
-    "cprover_string_array",
     location,
-    ID_java,
+    location.get_function(),
     symbol_table);
   array_symbol.is_static_lifetime=true;
   return array_symbol.symbol_expr();
@@ -464,8 +463,8 @@ refined_string_exprt java_string_library_preprocesst::replace_char_array(
     checked_dereference(array_pointer, array_pointer.type().subtype());
   // array_data is array_pointer-> data
   const exprt array_data = get_data(array, symbol_table);
-  const symbolt &sym_char_array = get_fresh_aux_symbol(
-    array_data.type(), "char_array", "char_array", loc, ID_java, symbol_table);
+  const symbolt &sym_char_array = fresh_java_symbol(
+    array_data.type(), "char_array", loc, loc.get_function(), symbol_table);
   const symbol_exprt char_array = sym_char_array.symbol_expr();
   // char_array = array_pointer->data
   code.add(code_assignt(char_array, array_data), loc);
@@ -496,8 +495,8 @@ symbol_exprt java_string_library_preprocesst::fresh_string(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
-  symbolt string_symbol=get_fresh_aux_symbol(
-    type, "cprover_string", "cprover_string", loc, ID_java, symbol_table);
+  symbolt string_symbol =
+    fresh_java_symbol(type, "cprover_string", loc, function_id, symbol_table);
   string_symbol.is_static_lifetime=true;
   return string_symbol.symbol_expr();
 }
@@ -515,22 +514,12 @@ refined_string_exprt java_string_library_preprocesst::decl_string_expr(
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
-  const symbolt &sym_length = get_fresh_aux_symbol(
-    index_type,
-    "cprover_string_length",
-    "cprover_string_length",
-    loc,
-    ID_java,
-    symbol_table);
+  const symbolt &sym_length = fresh_java_symbol(
+    index_type, "cprover_string_length", loc, function_id, symbol_table);
   const symbol_exprt length_field = sym_length.symbol_expr();
   const pointer_typet array_type = pointer_type(java_char_type());
-  const symbolt &sym_content = get_fresh_aux_symbol(
-    array_type,
-    "cprover_string_content",
-    "cprover_string_content",
-    loc,
-    ID_java,
-    symbol_table);
+  const symbolt &sym_content = fresh_java_symbol(
+    array_type, "cprover_string_content", loc, function_id, symbol_table);
   const symbol_exprt content_field = sym_content.symbol_expr();
   code.add(code_declt(content_field), loc);
   const refined_string_exprt str{
@@ -656,12 +645,11 @@ exprt make_nondet_infinite_char_array(
 {
   const array_typet array_type(
     java_char_type(), infinity_exprt(java_int_type()));
-  const symbolt data_sym = get_fresh_aux_symbol(
+  const symbolt data_sym = fresh_java_symbol(
     pointer_type(array_type),
-    id2string(function_id),
     "nondet_infinite_array_pointer",
     loc,
-    ID_java,
+    function_id,
     symbol_table);
 
   const symbol_exprt data_pointer = data_sym.symbol_expr();
@@ -691,13 +679,8 @@ void add_pointer_to_array_association(
 {
   PRECONDITION(array.type().id() == ID_array);
   PRECONDITION(pointer.type().id() == ID_pointer);
-  const symbolt &return_sym = get_fresh_aux_symbol(
-    java_int_type(),
-    "return_array",
-    "return_array",
-    loc,
-    ID_java,
-    symbol_table);
+  const symbolt &return_sym = fresh_java_symbol(
+    java_int_type(), "return_array", loc, function_id, symbol_table);
   const auto return_expr = return_sym.symbol_expr();
   code.add(code_declt(return_expr), loc);
   code.add(
@@ -725,13 +708,8 @@ void add_array_to_length_association(
   const irep_idt &function_id,
   code_blockt &code)
 {
-  const symbolt &return_sym = get_fresh_aux_symbol(
-    java_int_type(),
-    "return_array",
-    "return_array",
-    loc,
-    ID_java,
-    symbol_table);
+  const symbolt &return_sym = fresh_java_symbol(
+    java_int_type(), "return_array", loc, function_id, symbol_table);
   const auto return_expr = return_sym.symbol_expr();
   code.add(code_declt(return_expr), loc);
   code.add(
@@ -762,8 +740,8 @@ void add_character_set_constraint(
   code_blockt &code)
 {
   PRECONDITION(pointer.type().id() == ID_pointer);
-  const symbolt &return_sym = get_fresh_aux_symbol(
-    java_int_type(), "cnstr_added", "cnstr_added", loc, ID_java, symbol_table);
+  const symbolt &return_sym = fresh_java_symbol(
+    java_int_type(), "cnstr_added", loc, loc.get_function(), symbol_table);
   const auto return_expr = return_sym.symbol_expr();
   code.add(code_declt(return_expr), loc);
   const constant_exprt char_set_expr(char_set, string_typet());
@@ -800,12 +778,11 @@ refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
   code_blockt &code)
 {
   // int return_code;
-  const symbolt &return_code_sym = get_fresh_aux_symbol(
+  const symbolt return_code_sym = fresh_java_symbol(
     java_int_type(),
     std::string("return_code_") + function_id.c_str(),
-    std::string("return_code_") + function_id.c_str(),
     loc,
-    ID_java,
+    function_id,
     symbol_table);
   const auto return_code = return_code_sym.symbol_expr();
   code.add(code_declt(return_code), loc);
@@ -1265,8 +1242,8 @@ java_string_library_preprocesst::get_primitive_value_of_object(
 
   // declare tmp_type_name to hold the value
   const std::string aux_name = "tmp_" + id2string(type_name);
-  const symbolt &symbol = get_fresh_aux_symbol(
-    value_type, aux_name, aux_name, loc, ID_java, symbol_table);
+  const symbolt &symbol = fresh_java_symbol(
+    value_type, aux_name, loc, loc.get_function(), symbol_table);
   const auto value = symbol.symbol_expr();
 
   // Check that the type of the object is in the symbol table,
@@ -1371,8 +1348,8 @@ struct_exprt java_string_library_preprocesst::make_argument_for_format(
     if(name!="string_expr")
     {
       std::string tmp_name="tmp_"+id2string(name);
-      const symbolt &field_symbol = get_fresh_aux_symbol(
-        type, id2string(function_id), tmp_name, loc, ID_java, symbol_table);
+      const symbolt &field_symbol = fresh_java_symbol(
+        type, tmp_name, loc, loc.get_function(), symbol_table);
       auto field_symbol_expr = field_symbol.symbol_expr();
       field_expr = field_symbol_expr;
       code.add(code_declt(field_symbol_expr), loc);
@@ -1387,13 +1364,8 @@ struct_exprt java_string_library_preprocesst::make_argument_for_format(
 
   // arg_i = argv[index]
   const exprt obj = get_object_at_index(argv, index);
-  const symbolt &object_symbol = get_fresh_aux_symbol(
-    obj.type(),
-    id2string(function_id),
-    "tmp_format_obj",
-    loc,
-    ID_java,
-    symbol_table);
+  const symbolt &object_symbol = fresh_java_symbol(
+    obj.type(), "tmp_format_obj", loc, loc.get_function(), symbol_table);
   const symbol_exprt arg_i = object_symbol.symbol_expr();
 
   allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table);
@@ -1538,8 +1510,8 @@ code_blockt java_string_library_preprocesst::make_object_get_class_code(
   // > Class class1;
   const pointer_typet class_type =
     java_reference_type(symbol_table.lookup_ref("java::java.lang.Class").type);
-  const symbolt &class1_sym = get_fresh_aux_symbol(
-    class_type, "class_symbol", "class_symbol", loc, ID_java, symbol_table);
+  const symbolt &class1_sym = fresh_java_symbol(
+    class_type, "class_symbol", loc, loc.get_function(), symbol_table);
   const symbol_exprt class1 = class1_sym.symbol_expr();
   code.add(code_declt(class1), loc);
 

jbmc/src/java_bytecode/java_utils.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "java_root_class.h"
 
+#include <util/fresh_symbol.h>
 #include <util/invariant.h>
 #include <util/mathematical_expr.h>
 #include <util/message.h>
@@ -433,3 +434,23 @@ const std::unordered_set<std::string> cprover_methods_to_ignore
   "endThread",
   "getCurrentThreadID"
 };
+
+/// \param type: type of new symbol
+/// \param basename_prefix: new symbol will be named
+///   function_name::basename_prefix$num
+/// \param source_location: new symbol source loc
+/// \param function_name: name of the function in which the symbol is defined
+/// \param symbol_table: table to add the new symbol to
+/// \return fresh-named symbol with the requested name pattern
+symbolt &fresh_java_symbol(
+  const typet &type,
+  const std::string &basename_prefix,
+  const source_locationt &source_location,
+  const irep_idt &function_name,
+  symbol_table_baset &symbol_table)
+{
+  PRECONDITION(!function_name.empty());
+  const std::string name_prefix = id2string(function_name);
+  return get_fresh_aux_symbol(
+    type, name_prefix, basename_prefix, source_location, ID_java, symbol_table);
+}

jbmc/src/java_bytecode/java_utils.h

@@ -109,4 +109,11 @@ bool is_non_null_library_global(const irep_idt &);
 
 extern const std::unordered_set<std::string> cprover_methods_to_ignore;
 
+symbolt &fresh_java_symbol(
+  const typet &type,
+  const std::string &basename_prefix,
+  const source_locationt &source_location,
+  const irep_idt &function_name,
+  symbol_table_baset &symbol_table);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H