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.
@@ -114,12 +114,11 @@ 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(
+    symbolt &aux_symbol = fresh_java_symbol(
       op.type(),
-      id2string(goto_programt::get_function_id(goto_program)),
       "nondet_tmp",
       source_loc,
-      ID_java,
+      goto_programt::get_function_id(goto_program),
       symbol_table);
 
     const symbol_exprt aux_symbol_expr = aux_symbol.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(symbol_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>
@@ -113,14 +112,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/pointer_offset_size.h>
 
@@ -18,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "generic_parameter_specialization_map_keys.h"
 #include "java_root_class.h"
+#include "java_utils.h"
 
 class java_object_factoryt
 {
@@ -206,12 +206,11 @@ exprt allocate_dynamic_object(
     // create a symbol for the malloc expression so we can initialize
     // without having to do it potentially through a double-deref, which
     // breaks the to-SSA phase.
-    symbolt &malloc_sym = get_fresh_aux_symbol(
+    symbolt &malloc_sym = fresh_java_symbol(
       pointer_type(allocate_type),
-      id2string(function_id),
       "malloc_site",
       loc,
-      ID_java,
+      function_id,
       symbol_table);
     symbols_created.push_back(&malloc_sym);
     code_assignt assign(malloc_sym.symbol_expr(), malloc_expr);
@@ -306,12 +305,11 @@ exprt java_object_factoryt::allocate_object(
     case allocation_typet::LOCAL:
     case allocation_typet::GLOBAL:
     {
-      symbolt &aux_symbol = get_fresh_aux_symbol(
+      symbolt &aux_symbol = fresh_java_symbol(
         allocate_type,
-        id2string(object_factory_parameters.function_id),
         "tmp_object_factory",
         loc,
-        ID_java,
+        object_factory_parameters.function_id,
         symbol_table);
       if(alloc_type==allocation_typet::GLOBAL)
         aux_symbol.is_static_lifetime=true;
@@ -610,13 +608,8 @@ bool 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));
@@ -918,12 +911,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
@@ -1240,12 +1232,11 @@ const symbol_exprt java_object_factoryt::gen_nondet_int_init(
 {
   PRECONDITION(min_value_expr.type() == max_value_expr.type());
   // Allocate a new symbol for the int
-  const symbolt &int_symbol = get_fresh_aux_symbol(
+  const symbolt &int_symbol = fresh_java_symbol(
     min_value_expr.type(),
-    id2string(object_factory_parameters.function_id),
     basename_prefix,
     loc,
-    ID_java,
+    object_factory_parameters.function_id,
     symbol_table);
   symbols_created.push_back(&int_symbol);
   const auto &int_symbol_expr = int_symbol.symbol_expr();
@@ -1364,12 +1355,11 @@ void java_object_factoryt::gen_nondet_array_init(
 
   // Interpose a new symbol, as the goto-symex stage can't handle array indexing
   // via a cast.
-  symbolt &array_init_symbol = get_fresh_aux_symbol(
+  symbolt &array_init_symbol = fresh_java_symbol(
     init_array_expr.type(),
-    id2string(object_factory_parameters.function_id),
     "array_data_init",
     loc,
-    ID_java,
+    object_factory_parameters.function_id,
     symbol_table);
   symbols_created.push_back(&array_init_symbol);
   const auto &array_init_symexpr=array_init_symbol.symbol_expr();
@@ -1379,12 +1369,11 @@ void java_object_factoryt::gen_nondet_array_init(
 
   // Emit init loop for(array_init_iter=0; array_init_iter!=array.length;
   //                  ++array_init_iter) init(array[array_init_iter]);
-  symbolt &counter = get_fresh_aux_symbol(
+  symbolt &counter = fresh_java_symbol(
     length_expr.type(),
-    id2string(object_factory_parameters.function_id),
     "array_init_iter",
     loc,
-    ID_java,
+    object_factory_parameters.function_id,
     symbol_table);
   symbols_created.push_back(&counter);
   exprt counter_expr=counter.symbol_expr();

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -249,12 +249,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();
@@ -453,8 +452,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);
@@ -483,8 +482,8 @@ symbol_exprt java_string_library_preprocesst::fresh_string(
   const source_locationt &loc,
   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, loc.get_function(), symbol_table);
   string_symbol.is_static_lifetime=true;
   return string_symbol.symbol_expr();
 }
@@ -500,21 +499,15 @@ 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, loc.get_function(), 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(
+  const symbolt sym_content = fresh_java_symbol(
     array_type,
     "cprover_string_content",
-    "cprover_string_content",
     loc,
-    ID_java,
+    loc.get_function(),
     symbol_table);
   const symbol_exprt content_field = sym_content.symbol_expr();
   code.add(code_declt(content_field), loc);
@@ -644,12 +637,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,
+    loc.get_function(),
     symbol_table);
 
   const symbol_exprt data_pointer = data_sym.symbol_expr();
@@ -677,13 +669,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, loc.get_function(), symbol_table);
   const auto return_expr = return_sym.symbol_expr();
   code.add(code_declt(return_expr), loc);
   code.add(
@@ -709,13 +696,8 @@ void add_array_to_length_association(
   const source_locationt &loc,
   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, loc.get_function(), symbol_table);
   const auto return_expr = return_sym.symbol_expr();
   code.add(code_declt(return_expr), loc);
   code.add(
@@ -746,8 +728,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());
@@ -784,12 +766,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_name.c_str(),
-    std::string("return_code_") + function_name.c_str(),
     loc,
-    ID_java,
+    loc.get_function(),
     symbol_table);
   const auto return_code = return_code_sym.symbol_expr();
   code.add(code_declt(return_code), loc);
@@ -1232,8 +1213,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,
@@ -1341,8 +1322,8 @@ exprt java_string_library_preprocesst::make_argument_for_format(
     if(name!="string_expr")
     {
       std::string tmp_name="tmp_"+id2string(name);
-      symbolt field_symbol = get_fresh_aux_symbol(
-        type, id2string(function_id), tmp_name, loc, ID_java, symbol_table);
+      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);
@@ -1357,13 +1338,8 @@ 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_dynamic_object_with_decl(
     arg_i, symbol_table, loc, function_id, code);
@@ -1503,8 +1479,8 @@ codet 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);