Add string symbol creation function that takes a string

This simplifies the code in a few places, since we don't have to repeat
the same lines of constructing the string literal exprt every time.

Author: antlechner

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -135,14 +135,10 @@ static void java_static_lifetime_init(
   // and we can refer to them later when we initialize input values.
   for(const auto &val : object_factory_parameters.string_input_values)
   {
-    exprt my_literal(ID_java_string_literal);
-    my_literal.set(ID_value, val);
     // We ignore the return value of the following call, we just need to
     // make sure the string is in the symbol table.
     get_or_create_string_literal_symbol(
-      my_literal,
-      symbol_table,
-      string_refinement_enabled);
+      val, symbol_table, string_refinement_enabled);
   }
 
   // We need to zero out all static variables, or nondet-initialize if they're
@@ -174,15 +170,13 @@ static void java_static_lifetime_init(
 
         bool class_is_array = is_java_array_tag(sym.name);
 
-        exprt name_literal(ID_java_string_literal);
-        name_literal.set(ID_value, to_class_type(class_symbol.type).get_tag());
-
         journalling_symbol_tablet journalling_table =
           journalling_symbol_tablet::wrap(symbol_table);
 
-        symbol_exprt class_name_literal =
-          get_or_create_string_literal_symbol(
-            name_literal, journalling_table, string_refinement_enabled);
+        symbol_exprt class_name_literal = get_or_create_string_literal_symbol(
+          to_class_type(class_symbol.type).get_tag(),
+          journalling_table,
+          string_refinement_enabled);
 
         // If that created any new symbols make sure we initialise those too:
         const auto &new_symbols = journalling_table.get_inserted();

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -731,10 +731,8 @@ alternate_casest get_string_input_values_code(
   alternate_casest cases;
   for(const auto &val : string_input_values)
   {
-    exprt name_literal(ID_java_string_literal);
-    name_literal.set(ID_value, val);
     const symbol_exprt s =
-      get_or_create_string_literal_symbol(name_literal, symbol_table, true);
+      get_or_create_string_literal_symbol(val, symbol_table, true);
     cases.push_back(code_assignt(expr, s));
   }
   return cases;

jbmc/src/java_bytecode/java_string_literals.cpp

@@ -207,3 +207,14 @@ symbol_exprt get_or_create_string_literal_symbol(
 
   return new_symbol.symbol_expr();
 }
+
+symbol_exprt get_or_create_string_literal_symbol(
+  const irep_idt &string_value,
+  symbol_table_baset &symbol_table,
+  bool string_refinement_enabled)
+{
+  exprt literal{ID_java_string_literal};
+  literal.set(ID_value, string_value);
+  return get_or_create_string_literal_symbol(
+    literal, symbol_table, string_refinement_enabled);
+}

jbmc/src/java_bytecode/java_string_literals.h

@@ -25,4 +25,12 @@ symbol_exprt get_or_create_string_literal_symbol(
   symbol_table_baset &symbol_table,
   bool string_refinement_enabled);
 
+/// Same as \ref
+/// get_or_create_string_literal_symbol(const exprt&, symbol_table_baset&, bool)
+/// except it takes an id/string parameter rather than a string literal exprt.
+symbol_exprt get_or_create_string_literal_symbol(
+  const irep_idt &string_value,
+  symbol_table_baset &symbol_table,
+  bool string_refinement_enabled);
+
 #endif