Merge pull request #6571 from tautschnig/cleanup/java-goto_instructions_code

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

Author: tautschnig

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -8,16 +8,6 @@ Author: Diffblue Ltd.
 
 #include "assignments_from_json.h"
 
-#include "ci_lazy_methods_needed.h"
-#include "code_with_references.h"
-#include "java_static_initializers.h"
-#include "java_string_literals.h"
-#include "java_types.h"
-#include "java_utils.h"
-
-#include <goto-programs/allocate_objects.h>
-#include <goto-programs/class_identifier.h>
-
 #include <util/arith_tools.h>
 #include <util/array_element_from_pointer.h>
 #include <util/expr_initializer.h>
@@ -26,6 +16,17 @@ Author: Diffblue Ltd.
 #include <util/symbol_table_base.h>
 #include <util/unicode.h>
 
+#include <goto-programs/allocate_objects.h>
+#include <goto-programs/class_identifier.h>
+#include <goto-programs/goto_instruction_code.h>
+
+#include "ci_lazy_methods_needed.h"
+#include "code_with_references.h"
+#include "java_static_initializers.h"
+#include "java_string_literals.h"
+#include "java_types.h"
+#include "java_utils.h"
+
 /// Values passed around between most functions of the recursive deterministic
 /// assignment algorithm entered from \ref assign_from_json.
 /// The values in a given `object_creation_infot` are never reassigned, but the
@@ -345,43 +346,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 +407,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 +435,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 +509,17 @@ 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 +590,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;
@@ -646,7 +650,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 +700,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 +833,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

@@ -8,22 +8,23 @@ Author: Chris Smowton, [email protected]
 
 #include "java_static_initializers.h"
 
-#include "assignments_from_json.h"
-#include "ci_lazy_methods_needed.h"
-#include "java_object_factory.h"
-#include "java_object_factory_parameters.h"
-#include "java_types.h"
-#include "java_utils.h"
-
-#include <goto-programs/class_hierarchy.h>
-
 #include <util/arith_tools.h>
 #include <util/cprover_prefix.h>
 #include <util/json.h>
 #include <util/std_code.h>
 #include <util/suffix.h>
 #include <util/symbol_table.h>
 
+#include <goto-programs/class_hierarchy.h>
+#include <goto-programs/goto_instruction_code.h>
+
+#include "assignments_from_json.h"
+#include "ci_lazy_methods_needed.h"
+#include "java_object_factory.h"
+#include "java_object_factory_parameters.h"
+#include "java_types.h"
+#include "java_utils.h"
+
 /// The three states in which a `<clinit>` method for a class can be before,
 /// after, and during static class initialization. These states are only used
 /// when the thread safe version of the clinit wrapper is generated.
@@ -580,7 +581,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);
   }
 

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
@@ -233,7 +235,7 @@ void allocate_objectst::declare_created_symbols(code_blockt &init_code)
     const symbolt &symbol = ns.lookup(symbol_id);
     if(!symbol.is_static_lifetime)
     {
-      code_declt decl{symbol.symbol_expr()};
+      code_frontend_declt decl{symbol.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