Create java_string_literal_exprt class

With this new class, we can avoid directly accessing named
subexpressions of exprts with id() == ID_java_string_literal.

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,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/unicode.h>
 
 #include "java_pointer_casts.h"
+#include "java_string_literal_expr.h"
 #include "java_types.h"
 #include "java_utils.h"
 #include "java_root_class.h"
@@ -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_string_literal_expr.h

@@ -0,0 +1,27 @@
+#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:
+  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"
 
@@ -56,12 +57,11 @@ static array_exprt utf16_to_array(const std::wstring &in)
 }
 
 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));
@@ -213,8 +213,8 @@ symbol_exprt get_or_create_string_literal_symbol(
   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);
+    java_string_literal_exprt{string_value},
+    symbol_table,
+    string_refinement_enabled);
 }

jbmc/src/java_bytecode/java_string_literals.h

@@ -12,6 +12,8 @@ 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
@@ -21,7 +23,7 @@ Author: Chris Smowton, [email protected]
 ///   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);