Cleanup in string preprocessing

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,8 @@ 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, "new_exception", 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_entry_point.cpp

@@ -375,12 +375,11 @@ exprt::operandst java_build_arguments(
       // method(..., param, ...)
       //
 
-      const symbolt result_symbol = get_fresh_aux_symbol(
+      const symbolt result_symbol = fresh_java_symbol(
         p.type(),
-        id2string(function.name),
         "nondet_parameter_" + std::to_string(param_number),
         function.location,
-        ID_java,
+        function.name,
         symbol_table);
       main_arguments[param_number] = result_symbol.symbol_expr();
 

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));
@@ -476,18 +471,18 @@ void initialize_nondet_string_fields(
     index_exprt(data_expr, from_integer(0, java_int_type())));
 
   add_pointer_to_array_association(
-    array_pointer, data_expr, symbol_table, loc, code);
+    array_pointer, data_expr, symbol_table, loc, function_id, code);
 
   add_array_to_length_association(
-    data_expr, length_expr, symbol_table, loc, code);
+    data_expr, length_expr, symbol_table, loc, function_id, code);
 
   struct_expr.operands()[struct_type.component_number("data")] = array_pointer;
 
   // Printable ASCII characters are between ' ' and '~'.
   if(printable)
   {
     add_character_set_constraint(
-      array_pointer, length_expr, " -~", symbol_table, loc, code);
+      array_pointer, length_expr, " -~", symbol_table, loc, function_id, code);
   }
 }
 
@@ -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