Merge pull request #6591 from tautschnig/cleanup/symbolt

Add and use symbolt constructors

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -47,17 +47,14 @@ static symbolt add_or_get_symbol(
   ns.lookup(name, psymbol);
   if(psymbol != nullptr)
     return *psymbol;
-  symbolt new_symbol;
-  new_symbol.name = name;
+  symbolt new_symbol{name, type, ID_java};
   new_symbol.pretty_name = name;
   new_symbol.base_name = base_name;
-  new_symbol.type = type;
   new_symbol.value = value;
   new_symbol.is_lvalue = true;
   new_symbol.is_state_var = true;
   new_symbol.is_static_lifetime = is_static_lifetime;
   new_symbol.is_thread_local = is_thread_local;
-  new_symbol.mode = ID_java;
   symbol_table.add(new_symbol);
   return new_symbol;
 }

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -449,14 +449,10 @@ void java_bytecode_convert_classt::convert(
   }(id2string(c.name));
 
   // produce class symbol
-  symbolt new_symbol;
+  class_type.set_name(qualified_classname);
+  type_symbolt new_symbol{qualified_classname, class_type, ID_java};
   new_symbol.base_name = base_name;
   new_symbol.pretty_name=c.name;
-  new_symbol.name=qualified_classname;
-  class_type.set_name(new_symbol.name);
-  new_symbol.type=class_type;
-  new_symbol.mode=ID_java;
-  new_symbol.is_type=true;
 
   symbolt *class_symbol;
 
@@ -714,23 +710,22 @@ void java_bytecode_convert_classt::convert(
     component.type() = field_type;
 
     // Create the symbol
-    symbolt new_symbol;
+    symbolt new_symbol{
+      id2string(class_symbol.name) + "." + id2string(f.name),
+      field_type,
+      ID_java};
 
     new_symbol.is_static_lifetime=true;
     new_symbol.is_lvalue=true;
     new_symbol.is_state_var=true;
-    new_symbol.name=id2string(class_symbol.name)+"."+id2string(f.name);
     new_symbol.base_name=f.name;
-    new_symbol.type=field_type;
     // Provide a static field -> class link, like
     // java_bytecode_convert_method::convert does for method -> class.
     set_declaring_class(new_symbol, class_symbol.name);
     new_symbol.type.set(ID_C_field, f.name);
     new_symbol.type.set(ID_C_constant, f.is_final);
     new_symbol.pretty_name=id2string(class_symbol.pretty_name)+
       "."+id2string(f.name);
-    new_symbol.mode=ID_java;
-    new_symbol.is_type=false;
 
     // These annotations use `ID_C_access` instead of `ID_access` like methods
     // to avoid type clashes in expressions like `some_static_field = 0`, where
@@ -862,12 +857,8 @@ void add_java_array_types(symbol_table_baset &symbol_table)
       "Constructed a new type representing a Java Array "
       "object that doesn't match expectations");
 
-    symbolt symbol;
-    symbol.name = struct_tag_type_identifier;
+    type_symbolt symbol{struct_tag_type_identifier, class_type, ID_java};
     symbol.base_name = struct_tag_type.get(ID_C_base_name);
-    symbol.is_type=true;
-    symbol.type = class_type;
-    symbol.mode = ID_java;
     symbol_table.add(symbol);
 
     // Also provide a clone method:
@@ -992,14 +983,11 @@ void add_java_array_types(symbol_table_baset &symbol_table)
                                   copy_loop,
                                   return_inst});
 
-    symbolt clone_symbol;
-    clone_symbol.name=clone_name;
+    symbolt clone_symbol{clone_name, clone_type, ID_java};
     clone_symbol.pretty_name =
       id2string(struct_tag_type_identifier) + ".clone:()";
     clone_symbol.base_name="clone";
-    clone_symbol.type=clone_type;
     clone_symbol.value=clone_body;
-    clone_symbol.mode=ID_java;
     symbol_table.add(clone_symbol);
   }
 }

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -102,15 +102,11 @@ void create_method_stub_symbol(
 {
   messaget log(message_handler);
 
-  symbolt symbol;
-  symbol.name = identifier;
+  symbolt symbol{identifier, type, ID_java};
   symbol.base_name = base_name;
   symbol.pretty_name = pretty_name;
-  symbol.type = type;
   symbol.type.set(ID_access, ID_private);
   to_java_method_type(symbol.type).set_is_final(true);
-  symbol.value.make_nil();
-  symbol.mode = ID_java;
   assign_parameter_names(
     to_java_method_type(symbol.type), symbol.name, symbol_table);
   set_declaring_class(symbol, declaring_class);
@@ -307,18 +303,15 @@ void java_bytecode_convert_method_lazy(
   symbol_table_baset &symbol_table,
   message_handlert &message_handler)
 {
-  symbolt method_symbol;
-
   java_method_typet member_type = member_type_lazy(
     m.descriptor,
     m.signature,
     id2string(class_symbol.name),
     id2string(m.base_name),
     message_handler);
 
-  method_symbol.name=method_identifier;
+  symbolt method_symbol{method_identifier, typet{}, ID_java};
   method_symbol.base_name=m.base_name;
-  method_symbol.mode=ID_java;
   method_symbol.location=m.source_location;
   method_symbol.location.set_function(method_identifier);
 
@@ -1900,13 +1893,9 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
   // Add anonymous locals to the symtab:
   for(const auto &var : used_local_names)
   {
-    symbolt new_symbol;
-    new_symbol.name=var.get_identifier();
-    new_symbol.type=var.type();
+    symbolt new_symbol{var.get_identifier(), var.type(), ID_java};
     new_symbol.base_name=var.get(ID_C_base_name);
     new_symbol.pretty_name=strip_java_namespace_prefix(var.get_identifier());
-    new_symbol.mode=ID_java;
-    new_symbol.is_type=false;
     new_symbol.is_file_local=true;
     new_symbol.is_thread_local=true;
     new_symbol.is_lvalue=true;

jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp

@@ -24,26 +24,22 @@ void java_internal_additions(symbol_table_baset &dest)
   // add __CPROVER_rounding_mode
 
   {
-    symbolt symbol;
-    symbol.name = rounding_mode_identifier();
+    symbolt symbol{rounding_mode_identifier(), signed_int_type(), ID_C};
     symbol.base_name = symbol.name;
-    symbol.type=signed_int_type();
-    symbol.mode=ID_C;
     symbol.is_lvalue=true;
     symbol.is_state_var=true;
     symbol.is_thread_local=true;
     dest.add(symbol);
   }
 
   {
-    auxiliary_symbolt symbol;
+    auxiliary_symbolt symbol{
+      INFLIGHT_EXCEPTION_VARIABLE_NAME,
+      pointer_type(java_void_type()),
+      ID_java};
     symbol.base_name = INFLIGHT_EXCEPTION_VARIABLE_BASENAME;
-    symbol.name = INFLIGHT_EXCEPTION_VARIABLE_NAME;
-    symbol.mode = ID_java;
-    symbol.type = pointer_type(java_void_type());
     symbol.type.set(ID_C_no_nondet_initialization, true);
     symbol.value = null_pointer_exprt(to_pointer_type(symbol.type));
-    symbol.is_file_local = false;
     symbol.is_static_lifetime = true;
     dest.add(symbol);
   }

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -528,15 +528,13 @@ static symbol_exprt get_or_create_class_literal_symbol(
     java_lang_Class);
   if(!symbol_table.has_symbol(symbol_expr.get_identifier()))
   {
-    symbolt new_class_symbol;
-    new_class_symbol.name = symbol_expr.get_identifier();
-    new_class_symbol.type = symbol_expr.type();
+    symbolt new_class_symbol{
+      symbol_expr.get_identifier(), symbol_expr.type(), ID_java};
     INVARIANT(
       has_prefix(id2string(new_class_symbol.name), "java::"),
       "class identifier should have 'java::' prefix");
     new_class_symbol.base_name =
       id2string(new_class_symbol.name).substr(6);
-    new_class_symbol.mode = ID_java;
     new_class_symbol.is_lvalue = true;
     new_class_symbol.is_state_var = true;
     new_class_symbol.is_static_lifetime = true;
@@ -651,13 +649,11 @@ static void create_stub_global_symbol(
   const irep_idt &class_id,
   bool force_nondet_init)
 {
-  symbolt new_symbol;
+  symbolt new_symbol{symbol_id, symbol_type, ID_java};
   new_symbol.is_static_lifetime = true;
   new_symbol.is_lvalue = true;
   new_symbol.is_state_var = true;
-  new_symbol.name = symbol_id;
   new_symbol.base_name = symbol_basename;
-  new_symbol.type = symbol_type;
   set_declaring_class(new_symbol, class_id);
   // Public access is a guess; it encourages merging like-typed static fields,
   // whereas a more restricted visbility would encourage separating them.
@@ -666,8 +662,6 @@ static void create_stub_global_symbol(
   // We set the field as final to avoid assuming they can be overridden.
   new_symbol.type.set(ID_C_constant, true);
   new_symbol.pretty_name = new_symbol.name;
-  new_symbol.mode = ID_java;
-  new_symbol.is_type = false;
   // If pointer-typed, initialise to null and a static initialiser will be
   // created to initialise on first reference. If primitive-typed, specify
   // nondeterministic initialisation by setting a nil value.

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -50,12 +50,10 @@ void create_java_initialize(symbol_table_baset &symbol_table)
   // if a GOTO binary provided it. This behaviour mirrors the ANSI-C frontend.
   symbol_table.remove(INITIALIZE_FUNCTION);
 
-  symbolt initialize;
-  initialize.name=INITIALIZE_FUNCTION;
+  symbolt initialize{
+    INITIALIZE_FUNCTION, java_method_typet({}, java_void_type()), ID_java};
   initialize.base_name=INITIALIZE_FUNCTION;
-  initialize.mode=ID_java;
 
-  initialize.type = java_method_typet({}, java_void_type());
   symbol_table.add(initialize);
 }
 
@@ -764,13 +762,12 @@ bool generate_java_start_function(
 
   // create a symbol for the __CPROVER__start function, associate the code that
   // we just built and register it in the symbol table
-  symbolt new_symbol;
-
-  new_symbol.name=goto_functionst::entry_point();
+  symbolt new_symbol{
+    goto_functionst::entry_point(),
+    java_method_typet{{}, java_void_type()},
+    ID_java};
   new_symbol.base_name = goto_functionst::entry_point();
-  new_symbol.type = java_method_typet({}, java_void_type());
   new_symbol.value.swap(init_code);
-  new_symbol.mode=ID_java;
 
   if(!symbol_table.insert(std::move(new_symbol)).second)
   {

jbmc/src/java_bytecode/java_local_variable_table.cpp

@@ -832,13 +832,9 @@ void java_bytecode_convert_methodt::setup_local_variables(
       result, v.var.start_pc, v.var.length, false, std::move(v.holes));
 
     // Register the local variable in the symbol table
-    symbolt new_symbol;
-    new_symbol.name=identifier;
-    new_symbol.type=t;
+    symbolt new_symbol{identifier, t, ID_java};
     new_symbol.base_name=v.var.name;
     new_symbol.pretty_name=id2string(identifier).substr(6, std::string::npos);
-    new_symbol.mode=ID_java;
-    new_symbol.is_type=false;
     new_symbol.is_file_local=true;
     new_symbol.is_thread_local=true;
     new_symbol.is_lvalue=true;

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -120,18 +120,15 @@ static symbolt add_new_variable_symbol(
   const bool is_thread_local,
   const bool is_static_lifetime)
 {
-  symbolt new_symbol;
-  new_symbol.name = name;
+  symbolt new_symbol{name, type, ID_java};
   new_symbol.pretty_name = name;
   new_symbol.base_name = name;
-  new_symbol.type = type;
   new_symbol.type.set(ID_C_no_nondet_initialization, true);
   new_symbol.value = value;
   new_symbol.is_lvalue = true;
   new_symbol.is_state_var = true;
   new_symbol.is_static_lifetime = is_static_lifetime;
   new_symbol.is_thread_local = is_thread_local;
-  new_symbol.mode = ID_java;
   symbol_table.add(new_symbol);
   return new_symbol;
 }
@@ -336,16 +333,14 @@ static void create_function_symbol(
   symbol_table_baset &symbol_table,
   synthetic_methods_mapt &synthetic_methods)
 {
-  symbolt function_symbol;
-  const java_method_typet function_type({}, java_void_type());
+  symbolt function_symbol{
+    function_name, java_method_typet({}, java_void_type()), ID_java};
   function_symbol.name = function_name;
   function_symbol.pretty_name = function_symbol.name;
   function_symbol.base_name = function_base_name;
-  function_symbol.type = function_type;
   // This provides a back-link from a method to its associated class, as is done
   // for java_bytecode_convert_methodt::convert.
   set_declaring_class(function_symbol, class_name);
-  function_symbol.mode = ID_java;
   bool failed = symbol_table.add(function_symbol);
   INVARIANT(!failed, id2string(function_base_name) + " symbol should be fresh");
 
@@ -969,14 +964,10 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
       "a class cannot be both incomplete, and so have stub static fields, and "
       "also define a static initializer");
 
-    const java_method_typet thunk_type({}, java_void_type());
-
-    symbolt static_init_symbol;
-    static_init_symbol.name = static_init_name;
+    symbolt static_init_symbol{
+      static_init_name, java_method_typet({}, java_void_type()), ID_java};
     static_init_symbol.pretty_name = static_init_name;
     static_init_symbol.base_name = "clinit():V";
-    static_init_symbol.mode = ID_java;
-    static_init_symbol.type = thunk_type;
     // This provides a back-link from a method to its associated class, as is
     // done for java_bytecode_convert_methodt::convert.
     set_declaring_class(static_init_symbol, it->first);

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -221,8 +221,7 @@ void java_string_library_preprocesst::add_string_type(
   symbol_table_baset &symbol_table)
 {
   irep_idt class_symbol_name = "java::" + id2string(class_name);
-  symbolt tmp_string_symbol;
-  tmp_string_symbol.name = class_symbol_name;
+  type_symbolt tmp_string_symbol{class_symbol_name, typet{}, ID_java};
   symbolt *string_symbol = nullptr;
   bool already_exists = symbol_table.move(tmp_string_symbol, string_symbol);
 
@@ -250,8 +249,6 @@ void java_string_library_preprocesst::add_string_type(
     string_symbol->base_name = id2string(class_name);
     string_symbol->pretty_name = id2string(class_name);
     string_symbol->type = new_string_type;
-    string_symbol->is_type = true;
-    string_symbol->mode = ID_java;
   }
 
   auto &string_type = to_java_class_type(string_symbol->type);

jbmc/src/java_bytecode/java_string_literals.cpp

@@ -57,14 +57,10 @@ symbol_exprt get_or_create_string_literal_symbol(
 #endif
 
   // Create a new symbol:
-  symbolt new_symbol;
-  new_symbol.name = escaped_symbol_name_with_prefix;
-  new_symbol.type = string_type;
+  symbolt new_symbol{escaped_symbol_name_with_prefix, string_type, ID_java};
   new_symbol.type.set(ID_C_constant, true);
   new_symbol.base_name = escaped_symbol_name;
   new_symbol.pretty_name = value;
-  new_symbol.mode = ID_java;
-  new_symbol.is_type = false;
   new_symbol.is_lvalue = true;
   new_symbol.is_state_var = true;
   new_symbol.is_static_lifetime = true;
@@ -97,18 +93,15 @@ symbol_exprt get_or_create_string_literal_symbol(
     literal_init.operands()[length_nb] = length;
 
     // Initialize the string with a constant utf-16 array:
-    symbolt array_symbol;
-    array_symbol.name = escaped_symbol_name_with_prefix + "_constarray";
+    symbolt array_symbol{
+      escaped_symbol_name_with_prefix + "_constarray", data.type(), ID_java};
     array_symbol.base_name = escaped_symbol_name + "_constarray";
     array_symbol.pretty_name = value;
-    array_symbol.mode = ID_java;
-    array_symbol.is_type = false;
     array_symbol.is_lvalue = true;
     // These are basically const global data:
     array_symbol.is_static_lifetime = true;
     array_symbol.is_state_var = true;
     array_symbol.value = data;
-    array_symbol.type = array_symbol.value.type();
     array_symbol.type.set(ID_C_constant, true);
 
     if(symbol_table.add(array_symbol))
@@ -122,15 +115,13 @@ symbol_exprt get_or_create_string_literal_symbol(
     literal_init.operands()[data_nb] = array_pointer;
 
     // Associate array with pointer
-    symbolt return_symbol;
-    return_symbol.name = escaped_symbol_name_with_prefix + "_return_value";
+    symbolt return_symbol{
+      escaped_symbol_name_with_prefix + "_return_value", typet{}, ID_java};
     return_symbol.base_name = escaped_symbol_name + "_return_value";
     return_symbol.pretty_name =
       escaped_symbol_name.length() > 10
         ? escaped_symbol_name.substr(0, 10) + "..._return_value"
         : escaped_symbol_name + "_return_value";
-    return_symbol.mode = ID_java;
-    return_symbol.is_type = false;
     return_symbol.is_lvalue = true;
     return_symbol.is_static_lifetime = true;
     return_symbol.is_state_var = true;