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,13 +114,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(goto_programt::get_function_id(goto_program)),
-      "nondet_tmp",
-      source_loc,
-      ID_java,
-      symbol_table);
+    symbolt &aux_symbol =
+      fresh_java_symbol(op.type(), "nondet_tmp", source_loc, 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.
@@ -236,12 +236,10 @@ 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,
     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,8 @@ codet 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, 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
 {
@@ -205,13 +205,8 @@ 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(
-      pointer_type(allocate_type),
-      id2string(function_id),
-      "malloc_site",
-      loc,
-      ID_java,
-      symbol_table);
+    symbolt &malloc_sym = fresh_java_symbol(
+      pointer_type(allocate_type), "malloc_site", loc, symbol_table);
     symbols_created.push_back(&malloc_sym);
     code_assignt assign=code_assignt(malloc_sym.symbol_expr(), malloc_expr);
     assign.add_source_location()=loc;
@@ -303,13 +298,8 @@ exprt java_object_factoryt::allocate_object(
     case allocation_typet::LOCAL:
     case allocation_typet::GLOBAL:
     {
-      symbolt &aux_symbol = get_fresh_aux_symbol(
-        allocate_type,
-        id2string(object_factory_parameters.function_id),
-        "tmp_object_factory",
-        loc,
-        ID_java,
-        symbol_table);
+      symbolt &aux_symbol = fresh_java_symbol(
+        allocate_type, "tmp_object_factory", loc, symbol_table);
       if(alloc_type==allocation_typet::GLOBAL)
         aux_symbol.is_static_lifetime=true;
       symbols_created.push_back(&aux_symbol);
@@ -615,13 +605,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, 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));
@@ -646,8 +631,8 @@ bool initialize_nondet_string_fields(
   const typet data_ptr_type = pointer_type(
     array_typet(java_char_type(), infinity_exprt(java_int_type())));
 
-  symbolt &data_pointer_sym = get_fresh_aux_symbol(
-    data_ptr_type, "", "string_data_pointer", loc, ID_java, symbol_table);
+  symbolt &data_pointer_sym =
+    fresh_java_symbol(data_ptr_type, "string_data_pointer", loc, symbol_table);
   const auto data_pointer = data_pointer_sym.symbol_expr();
   code.add(code_declt(data_pointer));
 
@@ -939,13 +924,8 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
   size_t depth,
   const source_locationt &location)
 {
-  symbolt new_symbol = get_fresh_aux_symbol(
-    replacement_pointer,
-    id2string(object_factory_parameters.function_id),
-    "tmp_object_factory",
-    loc,
-    ID_java,
-    symbol_table);
+  symbolt new_symbol = fresh_java_symbol(
+    replacement_pointer, "tmp_object_factory", location, symbol_table);
 
   // Generate a new object into this new symbol
   gen_nondet_init(
@@ -1260,13 +1240,8 @@ 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(
-    min_value_expr.type(),
-    id2string(object_factory_parameters.function_id),
-    basename_prefix,
-    loc,
-    ID_java,
-    symbol_table);
+  const symbolt &int_symbol = fresh_java_symbol(
+    min_value_expr.type(), basename_prefix, loc, symbol_table);
   symbols_created.push_back(&int_symbol);
   const auto &int_symbol_expr = int_symbol.symbol_expr();
 
@@ -1382,13 +1357,8 @@ 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(
-    init_array_expr.type(),
-    id2string(object_factory_parameters.function_id),
-    "array_data_init",
-    loc,
-    ID_java,
-    symbol_table);
+  symbolt &array_init_symbol = fresh_java_symbol(
+    init_array_expr.type(), "array_data_init", loc, symbol_table);
   symbols_created.push_back(&array_init_symbol);
   const auto &array_init_symexpr=array_init_symbol.symbol_expr();
   codet data_assign=code_assignt(array_init_symexpr, init_array_expr);
@@ -1397,13 +1367,8 @@ 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(
-    length_expr.type(),
-    id2string(object_factory_parameters.function_id),
-    "array_init_iter",
-    loc,
-    ID_java,
-    symbol_table);
+  symbolt &counter =
+    fresh_java_symbol(length_expr.type(), "array_init_iter", loc, symbol_table);
   symbols_created.push_back(&counter);
   exprt counter_expr=counter.symbol_expr();