Merge pull request #4509 from antlechner/antonia/refactor-constant-string-symbol

Add a version of get_or_create_string_literal_symbol that takes a string parameter

Author: antlechner

jbmc/src/java_bytecode/expr2java.cpp

@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/expr2c_class.h>
 
 #include "java_qualifiers.h"
+#include "java_string_literal_expr.h"
 #include "java_types.h"
 
 std::string expr2javat::convert(const typet &src)
@@ -414,8 +415,11 @@ std::string expr2javat::convert_with_precedence(
       id2string(src.get(ID_component_name)) +
       ")";
   }
-  else if(src.id()==ID_java_string_literal)
-    return '"'+MetaString(src.get_string(ID_value))+'"';
+  else if(
+    const auto &literal = expr_try_dynamic_cast<java_string_literal_exprt>(src))
+  {
+    return '"' + MetaString(id2string(literal->value())) + '"';
+  }
   else if(src.id()==ID_constant)
     return convert_constant(to_constant_expr(src), precedence=16);
   else

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_bytecode_convert_method_class.h"
 #include "java_static_initializers.h"
 #include "java_string_library_preprocess.h"
+#include "java_string_literal_expr.h"
 #include "java_types.h"
 #include "java_utils.h"
 #include "pattern.h"
@@ -1313,7 +1314,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
       PRECONDITION(op.empty() && results.size() == 1);
 
       INVARIANT(
-        arg0.id() != ID_java_string_literal && arg0.id() != ID_type,
+        !can_cast_expr<java_string_literal_exprt>(arg0) && arg0.id() != ID_type,
         "String and Class literals should have been lowered in "
         "generate_constant_global_variables");
 

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -26,19 +26,20 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/class_hierarchy.h>
 
+#include "ci_lazy_methods.h"
 #include "java_bytecode_concurrency_instrumentation.h"
 #include "java_bytecode_convert_class.h"
 #include "java_bytecode_convert_method.h"
-#include "java_bytecode_internal_additions.h"
 #include "java_bytecode_instrument.h"
-#include "java_bytecode_typecheck.h"
-#include "java_entry_point.h"
+#include "java_bytecode_internal_additions.h"
 #include "java_bytecode_parser.h"
+#include "java_bytecode_typecheck.h"
 #include "java_class_loader.h"
-#include "java_string_literals.h"
+#include "java_entry_point.h"
 #include "java_static_initializers.h"
+#include "java_string_literal_expr.h"
+#include "java_string_literals.h"
 #include "java_utils.h"
-#include "ci_lazy_methods.h"
 
 #include "expr2java.h"
 #include "load_method_by_regex.h"
@@ -417,12 +418,12 @@ static exprt get_ldc_result(
       address_of_exprt(
         get_or_create_class_literal_symbol(class_id, symbol_table));
   }
-  else if(ldc_arg0.id() == ID_java_string_literal)
+  else if(
+    const auto &literal =
+      expr_try_dynamic_cast<java_string_literal_exprt>(ldc_arg0))
   {
-    return
-      address_of_exprt(
-        get_or_create_string_literal_symbol(
-          ldc_arg0, symbol_table, string_refinement_enabled));
+    return address_of_exprt(get_or_create_string_literal_symbol(
+      *literal, symbol_table, string_refinement_enabled));
   }
   else
   {

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -21,9 +21,10 @@ Author: Daniel Kroening, [email protected]
 #include <util/string_constant.h>
 #include <util/optional.h>
 
+#include "bytecode_info.h"
 #include "java_bytecode_parse_tree.h"
+#include "java_string_literal_expr.h"
 #include "java_types.h"
-#include "bytecode_info.h"
 
 #ifdef DEBUG
 #include <iostream>
@@ -839,9 +840,7 @@ void java_bytecode_parsert::rconstant_pool()
     case CONSTANT_String:
       {
         // ldc turns these into references to java.lang.String
-        exprt string_literal(ID_java_string_literal);
-        string_literal.set(ID_value, pool_entry(it->ref1).s);
-        it->expr=string_literal;
+        it->expr = java_string_literal_exprt{pool_entry(it->ref1).s};
       }
       break;
 

jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp

@@ -17,10 +17,11 @@ Author: Daniel Kroening, [email protected]
 #include <util/unicode.h>
 
 #include "java_pointer_casts.h"
-#include "java_types.h"
-#include "java_utils.h"
 #include "java_root_class.h"
 #include "java_string_library_preprocess.h"
+#include "java_string_literal_expr.h"
+#include "java_types.h"
+#include "java_utils.h"
 
 void java_bytecode_typecheckt::typecheck_expr(exprt &expr)
 {
@@ -39,7 +40,7 @@ void java_bytecode_typecheckt::typecheck_expr(exprt &expr)
     typecheck_expr(*it);
 
   INVARIANT(
-    expr.id() != ID_java_string_literal,
+    !can_cast_expr<java_string_literal_exprt>(expr),
     "String literals should have been converted to constant globals "
     "before typecheck_expr");
 

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

@@ -720,10 +720,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_literal_expr.h

@@ -0,0 +1,38 @@
+/*******************************************************************\
+
+Module: Java Bytecode
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+/// \file
+/// Representation of a constant Java string
+
+#ifndef CPROVER_JAVA_BYTECODE_JAVA_STRING_LITERAL_EXPR_H
+#define CPROVER_JAVA_BYTECODE_JAVA_STRING_LITERAL_EXPR_H
+
+#include <util/expr.h>
+
+class java_string_literal_exprt : public exprt
+{
+public:
+  explicit java_string_literal_exprt(const irep_idt &literal)
+    : exprt(ID_java_string_literal)
+  {
+    set(ID_value, literal);
+  }
+
+  irep_idt value() const
+  {
+    return get(ID_value);
+  }
+};
+
+template <>
+inline bool can_cast_expr<java_string_literal_exprt>(const exprt &base)
+{
+  return base.id() == ID_java_string_literal;
+}
+
+#endif // CPROVER_JAVA_BYTECODE_JAVA_STRING_LITERAL_EXPR_H

jbmc/src/java_bytecode/java_string_literals.cpp

@@ -8,6 +8,7 @@ Author: Chris Smowton, [email protected]
 
 #include "java_string_literals.h"
 #include "java_root_class.h"
+#include "java_string_literal_expr.h"
 #include "java_types.h"
 #include "java_utils.h"
 
@@ -55,21 +56,12 @@ static array_exprt utf16_to_array(const std::wstring &in)
   return ret;
 }
 
-/// Creates or gets an existing constant global symbol for a given string
-/// literal.
-/// \param string_expr: string literal expression to convert
-/// \param symbol_table: global symbol table. If not already present, constant
-///   global symbols will be added.
-/// \param string_refinement_enabled: if true, string refinement's string data
-///   structure will also be initialised and added to the symbol table.
-/// \return a symbol_expr corresponding to the new or existing literal symbol.
 symbol_exprt get_or_create_string_literal_symbol(
-  const exprt &string_expr,
+  const java_string_literal_exprt &string_expr,
   symbol_table_baset &symbol_table,
   bool string_refinement_enabled)
 {
-  PRECONDITION(string_expr.id() == ID_java_string_literal);
-  const irep_idt value = string_expr.get(ID_value);
+  const irep_idt value = string_expr.value();
   const struct_tag_typet string_type("java::java.lang.String");
 
   const std::string escaped_symbol_name = escape_non_alnum(id2string(value));
@@ -215,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)
+{
+  return get_or_create_string_literal_symbol(
+    java_string_literal_exprt{string_value},
+    symbol_table,
+    string_refinement_enabled);
+}

jbmc/src/java_bytecode/java_string_literals.h

@@ -12,8 +12,26 @@ Author: Chris Smowton, [email protected]
 #include <util/symbol_table.h>
 #include <util/std_expr.h>
 
+class java_string_literal_exprt;
+
+/// Creates or gets an existing constant global symbol for a given string
+/// literal.
+/// \param string_expr: string literal expression to convert
+/// \param symbol_table: global symbol table. If not already present, constant
+///   global symbols will be added.
+/// \param string_refinement_enabled: if true, string refinement's string data
+///   structure will also be initialised and added to the symbol table.
+/// \return a symbol_expr corresponding to the new or existing literal symbol.
+symbol_exprt get_or_create_string_literal_symbol(
+  const java_string_literal_exprt &string_expr,
+  symbol_table_baset &symbol_table,
+  bool string_refinement_enabled);
+
+/// Same as
+/// 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 exprt &string_expr,
+  const irep_idt &string_value,
   symbol_table_baset &symbol_table,
   bool string_refinement_enabled);