Java front-end and allocate objects: do not use goto code types

Code that deals with symbol tables only should not create codet
structures defined in goto-programs/goto_instruction_code.h.

Author: tautschnig

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -345,43 +345,44 @@ assign_primitive_from_json(const exprt &expr, const jsont &json)
     return result;
   if(expr.type() == java_boolean_type())
   {
-    result.add(code_assignt{
+    result.add(code_frontend_assignt{
       expr, json.is_true() ? (exprt)true_exprt{} : (exprt)false_exprt{}});
   }
   else if(
     expr.type() == java_int_type() || expr.type() == java_byte_type() ||
     expr.type() == java_short_type() || expr.type() == java_long_type())
   {
-    result.add(
-      code_assignt{expr, from_integer(std::stoll(json.value), expr.type())});
+    result.add(code_frontend_assignt{
+      expr, from_integer(std::stoll(json.value), expr.type())});
   }
   else if(expr.type() == java_double_type())
   {
     ieee_floatt ieee_float(to_floatbv_type(expr.type()));
     ieee_float.from_double(std::stod(json.value));
-    result.add(code_assignt{expr, ieee_float.to_expr()});
+    result.add(code_frontend_assignt{expr, ieee_float.to_expr()});
   }
   else if(expr.type() == java_float_type())
   {
     ieee_floatt ieee_float(to_floatbv_type(expr.type()));
     ieee_float.from_float(std::stof(json.value));
-    result.add(code_assignt{expr, ieee_float.to_expr()});
+    result.add(code_frontend_assignt{expr, ieee_float.to_expr()});
   }
   else if(expr.type() == java_char_type())
   {
     const std::wstring wide_value = utf8_to_utf16_native_endian(json.value);
     PRECONDITION(wide_value.length() == 1);
-    result.add(
-      code_assignt{expr, from_integer(wide_value.front(), expr.type())});
+    result.add(code_frontend_assignt{
+      expr, from_integer(wide_value.front(), expr.type())});
   }
   return result;
 }
 
 /// One of the base cases of the recursive algorithm. See
 /// \ref assign_from_json_rec.
-static code_assignt assign_null(const exprt &expr)
+static code_frontend_assignt assign_null(const exprt &expr)
 {
-  return code_assignt{expr, null_pointer_exprt{to_pointer_type(expr.type())}};
+  return code_frontend_assignt{
+    expr, null_pointer_exprt{to_pointer_type(expr.type())}};
 }
 
 /// In the case of an assignment of an array given a JSON representation, this
@@ -405,7 +406,8 @@ static code_with_references_listt assign_array_data_component_from_json(
     info.allocate_objects.allocate_automatic_local_object(
       data_member_expr.type(), "user_specified_array_data_init");
   code_with_references_listt result;
-  result.add(code_assignt{array_init_data, data_member_expr, info.loc});
+  result.add(
+    code_frontend_assignt{array_init_data, data_member_expr, info.loc});
 
   size_t index = 0;
   const optionalt<std::string> inferred_element_type =
@@ -432,8 +434,8 @@ nondet_length(allocate_objectst &allocate, source_locationt loc)
   symbol_exprt length_expr = allocate.allocate_automatic_local_object(
     java_int_type(), "user_specified_array_length");
   code_with_references_listt code;
-  code.add(
-    code_assignt{length_expr, side_effect_expr_nondett{java_int_type(), loc}});
+  code.add(code_frontend_assignt{
+    length_expr, side_effect_expr_nondett{java_int_type(), loc}});
   code.add(code_assumet{binary_predicate_exprt{
     length_expr, ID_ge, from_integer(0, java_int_type())}});
   return std::make_pair(length_expr, std::move(code));
@@ -506,16 +508,16 @@ static code_with_references_listt assign_nondet_length_array_from_json(
 /// One of the cases in the recursive algorithm: the case where \p expr
 /// represents a string.
 /// See \ref assign_from_json_rec.
-static code_assignt assign_string_from_json(
+static code_frontend_assignt assign_string_from_json(
   const jsont &json,
   const exprt &expr,
   object_creation_infot &info)
 {
   const auto json_string = get_untyped_string(json);
   PRECONDITION(json_string.is_string());
-  return code_assignt{expr,
-                      get_or_create_string_literal_symbol(
-                        json_string.value, info.symbol_table, true)};
+  return code_frontend_assignt{expr,
+                               get_or_create_string_literal_symbol(
+                                 json_string.value, info.symbol_table, true)};
 }
 
 /// Helper function for \ref assign_struct_from_json which recursively assigns
@@ -586,7 +588,7 @@ static code_with_references_listt assign_struct_from_json(
       to_struct_expr(*initial_object),
       ns,
       struct_tag_typet("java::" + id2string(java_class_type.get_tag())));
-    result.add(code_assignt{expr, *initial_object});
+    result.add(code_frontend_assignt{expr, *initial_object});
     result.append(assign_struct_components_from_json(expr, json, info));
   }
   return result;
@@ -625,7 +627,10 @@ static code_with_references_listt assign_enum_from_json(
   const std::string &enum_name = id2string(java_class_type.get_name());
   code_with_references_listt result;
   if(const auto func = info.symbol_table.lookup(clinit_wrapper_name(enum_name)))
-    result.add(code_function_callt{func->symbol_expr()});
+  {
+    result.add(code_expressiont{side_effect_expr_function_callt{
+      func->symbol_expr(), {}, to_code_type(func->type), func->location}});
+  }
 
   const irep_idt values_name = enum_name + ".$VALUES";
   if(!info.symbol_table.has_symbol(values_name))
@@ -646,7 +651,7 @@ static code_with_references_listt assign_enum_from_json(
   const exprt ordinal_expr =
     from_integer(std::stoi(json["ordinal"].value), java_int_type());
 
-  result.add(code_assignt{
+  result.add(code_frontend_assignt{
     expr,
     typecast_exprt::conditional_cast(
       array_element_from_pointer(values_data, ordinal_expr), expr.type())});
@@ -696,7 +701,8 @@ static code_with_references_listt assign_pointer_with_given_type_from_json(
     }
 
     auto result = assign_pointer_from_json(new_symbol, json, info);
-    result.add(code_assignt{expr, typecast_exprt{new_symbol, pointer_type}});
+    result.add(
+      code_frontend_assignt{expr, typecast_exprt{new_symbol, pointer_type}});
     return result;
   }
   else
@@ -828,7 +834,7 @@ static code_with_references_listt assign_reference_from_json(
         assign_struct_from_json(dereference_exprt(reference.expr), json, info));
     }
   }
-  result.add(code_assignt{
+  result.add(code_frontend_assignt{
     expr, typecast_exprt::conditional_cast(reference.expr, expr.type())});
   return result;
 }

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -244,14 +244,26 @@ static void clinit_wrapper_do_recursive_calls(
     const auto base_name = base.type().get_identifier();
     irep_idt base_init_routine = clinit_wrapper_name(base_name);
     if(const auto base_init_func = symbol_table.lookup(base_init_routine))
-      init_body.add(code_function_callt{base_init_func->symbol_expr()});
+    {
+      init_body.add(code_expressiont{
+        side_effect_expr_function_callt{base_init_func->symbol_expr(),
+                                        {},
+                                        to_code_type(base_init_func->type),
+                                        base_init_func->location}});
+    }
   }
 
   const irep_idt &clinit_name = replace_clinit
                                   ? user_specified_clinit_name(class_name)
                                   : clinit_function_name(class_name);
   if(const auto clinit_func = symbol_table.lookup(clinit_name))
-    init_body.add(code_function_callt{clinit_func->symbol_expr()});
+  {
+    init_body.add(code_expressiont{
+      side_effect_expr_function_callt{clinit_func->symbol_expr(),
+                                      {},
+                                      to_code_type(clinit_func->type),
+                                      clinit_func->location}});
+  }
 
   // If nondet-static option is given, add a standard nondet initialization for
   // each non-final static field of this class. Note this is the same invocation
@@ -580,7 +592,7 @@ code_blockt get_thread_safe_clinit_wrapper_body(
 
   // bool init_complete;
   {
-    code_declt decl(init_complete.symbol_expr());
+    code_frontend_declt decl(init_complete.symbol_expr());
     function_body.add(decl);
   }
 
@@ -855,7 +867,11 @@ code_blockt get_user_specified_clinit_body(
       body.append(code_with_ref->to_code(reference_substitution));
     return body;
   }
-  return code_blockt{{code_function_callt{clinit_func->symbol_expr()}}};
+  return code_blockt{{code_expressiont{
+    side_effect_expr_function_callt{clinit_func->symbol_expr(),
+                                    {},
+                                    to_code_type(clinit_func->type),
+                                    clinit_func->location}}}};
 }
 
 /// Create static initializer wrappers and possibly user-specified functions for

jbmc/src/java_bytecode/nondet.cpp

@@ -49,7 +49,7 @@ symbol_exprt generate_nondet_int(
   // Declare a symbol for the non deterministic integer.
   const symbol_exprt &nondet_symbol =
     alocate_local_symbol(int_type, basename_prefix);
-  instructions.add(code_declt(nondet_symbol));
+  instructions.add(code_frontend_declt(nondet_symbol));
 
   // Assign the symbol any non deterministic integer value.
   //   int_type name_prefix::nondet_int = NONDET(int_type)

jbmc/src/java_bytecode/simple_method_stubbing.cpp

@@ -188,7 +188,7 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
       symbol.name,
       symbol_table);
     const symbol_exprt &init_symbol_expression = init_symbol.symbol_expr();
-    code_assignt get_argument(
+    code_frontend_assignt get_argument(
       init_symbol_expression,
       symbol_exprt(this_argument.get_identifier(), this_type));
     get_argument.add_source_location() = synthesized_source_location;
@@ -242,7 +242,7 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
           0,
           false,
           false);
-      new_instructions.add(code_returnt(to_return));
+      new_instructions.add(code_frontend_returnt(to_return));
     }
   }
 

src/goto-programs/allocate_objects.cpp

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_offset_size.h>
 #include <util/symbol.h>
 
+#include "goto_instruction_code.h"
+
 /// Allocates a new object, either by creating a local variable with automatic
 /// lifetime, a global variable with static lifetime, or by dynamically
 /// allocating memory via ALLOCATE(). Code is added to `assignments` which
@@ -232,7 +234,7 @@ void allocate_objectst::declare_created_symbols(code_blockt &init_code)
   {
     if(!symbol_ptr->is_static_lifetime)
     {
-      code_declt decl(symbol_ptr->symbol_expr());
+      code_frontend_declt decl(symbol_ptr->symbol_expr());
       decl.add_source_location() = source_location;
       init_code.add(decl);
     }

src/goto-programs/allocate_objects.h

@@ -9,10 +9,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_UTIL_ALLOCATE_OBJECTS_H
 #define CPROVER_UTIL_ALLOCATE_OBJECTS_H
 
-#include "goto_instruction_code.h"
-
 #include <util/namespace.h>
-#include <util/source_location.h>
 #include <util/std_code.h>
 
 /// Selects the kind of objects allocated