Store has-local-scope information in symbolt

None of the existing flags (nor any combination thereof) would enable us to
distinguish procedure-local type declarations from translation-unit wide ones.

Author: tautschnig

src/ansi-c/ansi_c_declaration.cpp

@@ -139,6 +139,7 @@ void ansi_c_declarationt::to_symbol(
   symbol.is_macro=get_is_typedef() || get_is_enum_constant();
   symbol.is_parameter=get_is_parameter();
   symbol.is_weak=get_is_weak();
+  symbol.has_local_scope = !get_is_global();
 
   // is it a function?
 

src/ansi-c/type2name.cpp

@@ -38,21 +38,27 @@ static std::string type2name_tag(
   if(ns.lookup(identifier, symbol))
     return "SYM#"+id2string(identifier)+"#";
 
+  std::string result;
+
+  // this isn't really a qualifier, but the linker needs to
+  // distinguish these - should likely be fixed in the linker instead
+  if(symbol->has_local_scope)
+    result += 'l';
+
   assert(symbol && symbol->is_type);
 
   if(symbol->type.id()!=ID_struct &&
      symbol->type.id()!=ID_union)
-    return type2name(symbol->type, ns, symbol_number);
+    return result + type2name(symbol->type, ns, symbol_number);
 
   // assign each symbol a number when seen for the first time
   std::pair<symbol_numbert::iterator, bool> entry=
     symbol_number.insert(std::make_pair(
         identifier,
         std::make_pair(symbol_number.size(), true)));
 
-  std::string result = "SYM" +
-                       id2string(to_struct_union_type(symbol->type).get_tag()) +
-                       '#' + std::to_string(entry.first->second.first);
+  result += "SYM" + id2string(to_struct_union_type(symbol->type).get_tag()) +
+            '#' + std::to_string(entry.first->second.first);
 
   // new entry, add definition
   if(entry.second)
@@ -99,11 +105,6 @@ static std::string type2name(
   if(type.get_bool(ID_C_noreturn))
     result+='n';
 
-  // this isn't really a qualifier, but the linker needs to
-  // distinguish these - should likely be fixed in the linker instead
-  if(!type.source_location().get_function().empty())
-    result+='l';
-
   if(type.id().empty())
     throw "empty type encountered";
   else if(type.id()==ID_empty)

src/cpp/cpp_declarator_converter.cpp

@@ -426,6 +426,8 @@ symbolt &cpp_declarator_convertert::convert_new_symbol(
   symbol.is_type=is_typedef;
   symbol.is_macro=is_typedef && !is_template_parameter;
   symbol.pretty_name=pretty_name;
+  symbol.has_local_scope =
+    !cpp_typecheck.cpp_scopes.current_scope().is_global_scope();
 
   // Constant? These are propagated.
   if(symbol.type.get_bool(ID_C_constant) &&

src/cpp/cpp_typecheck_compound_type.cpp

@@ -233,6 +233,7 @@ void cpp_typecheckt::typecheck_compound_type(
       cpp_scopes.current_scope().suffix;
     symbol.type.set(
       ID_tag, cpp_scopes.current_scope().prefix+id2string(symbol.base_name));
+    symbol.has_local_scope = !cpp_scopes.current_scope().is_global_scope();
 
     // move early, must be visible before doing body
     symbolt *new_symbol;

src/cpp/cpp_typecheck_enum_type.cpp

@@ -178,6 +178,7 @@ void cpp_typecheckt::typecheck_enum_type(typet &type)
     symbol.is_type=true;
     symbol.is_macro=false;
     symbol.pretty_name=pretty_name;
+    symbol.has_local_scope = !cpp_scopes.current_scope().is_global_scope();
 
     // move early, must be visible before doing body
     symbolt *new_symbol;

src/cpp/cpp_typecheck_template.cpp

@@ -178,6 +178,7 @@ void cpp_typecheckt::typecheck_class_template(
 
   symbol.pretty_name=
     cpp_scopes.current_scope().prefix+id2string(symbol.base_name);
+  symbol.has_local_scope = !cpp_scopes.current_scope().is_global_scope();
 
   symbolt *new_symbol;
   if(symbol_table.move(symbol, new_symbol))

src/goto-instrument/dump_c.cpp

@@ -168,11 +168,9 @@ void dump_ct::operator()(std::ostream &os)
     const symbolt &symbol=ns.lookup(*it);
     const irep_idt &type_id=symbol.type.id();
 
-    if(symbol.is_type &&
-       symbol.location.get_function().empty() &&
-       (type_id==ID_struct ||
-        type_id==ID_union ||
-        type_id==ID_c_enum))
+    if(
+      symbol.is_type && !symbol.has_local_scope &&
+      (type_id == ID_struct || type_id == ID_union || type_id == ID_c_enum))
     {
       if(!system_symbols.is_symbol_internal_symbol(symbol, system_headers))
       {
@@ -293,7 +291,7 @@ void dump_ct::convert_compound_declaration(
     const symbolt &symbol,
     std::ostream &os_body)
 {
-  if(!symbol.location.get_function().empty())
+  if(symbol.has_local_scope)
     return;
 
   // do compound type body
@@ -737,8 +735,7 @@ void dump_ct::gather_global_typedefs()
   {
     const symbolt &symbol=symbol_entry.second;
 
-    if(symbol.is_macro && symbol.is_type &&
-       symbol.location.get_function().empty())
+    if(symbol.is_macro && symbol.is_type && !symbol.has_local_scope)
     {
       const irep_idt &typedef_str=symbol.type.get(ID_C_typedef);
       PRECONDITION(!typedef_str.empty());
@@ -843,9 +840,10 @@ void dump_ct::convert_global_variable(
     std::ostream &os,
     local_static_declst &local_static_decls)
 {
-  const irep_idt &func=symbol.location.get_function();
-  if((func.empty() || symbol.is_extern || symbol.value.is_not_nil()) &&
-      !converted_global.insert(symbol.name).second)
+  const bool global = !symbol.has_local_scope;
+  if(
+    (global || symbol.is_extern || symbol.value.is_not_nil()) &&
+    !converted_global.insert(symbol.name).second)
     return;
 
   code_declt d(symbol.symbol_expr());
@@ -856,8 +854,7 @@ void dump_ct::convert_global_variable(
 
   // add a tentative declaration to cater for symbols in the initializer
   // relying on it this symbol
-  if((func.empty() || symbol.is_extern) &&
-     (symbol.value.is_nil() || !syms.empty()))
+  if((global || symbol.is_extern) && (symbol.value.is_nil() || !syms.empty()))
   {
     os << "// " << symbol.name << '\n';
     os << "// " << symbol.location << '\n';
@@ -889,7 +886,7 @@ void dump_ct::convert_global_variable(
     d.copy_to_operands(symbol.value);
   }
 
-  if(!func.empty() && !symbol.is_extern)
+  if(!global && !symbol.is_extern)
   {
     local_static_decls.emplace(symbol.name, d);
   }

src/goto-instrument/goto_program2code.cpp

@@ -1416,8 +1416,7 @@ void goto_program2codet::add_local_types(const typet &type)
       const irep_idt &identifier=to_symbol_type(type).get_identifier();
       const symbolt &symbol=ns.lookup(identifier);
 
-      if(symbol.location.get_function().empty() ||
-         !type_names_set.insert(identifier).second)
+      if(!symbol.has_local_scope || !type_names_set.insert(identifier).second)
         return;
 
       for(const auto &c : to_struct_union_type(full_type).components())
@@ -1432,8 +1431,7 @@ void goto_program2codet::add_local_types(const typet &type)
     const irep_idt &identifier=to_c_enum_tag_type(type).get_identifier();
     const symbolt &symbol=ns.lookup(identifier);
 
-    if(symbol.location.get_function().empty() ||
-       !type_names_set.insert(identifier).second)
+    if(!symbol.has_local_scope || !type_names_set.insert(identifier).second)
       return;
 
     assert(!identifier.empty());
@@ -1979,11 +1977,10 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
       const irep_idt &identifier=to_symbol_expr(expr).get_identifier();
       const symbolt &symbol=ns.lookup(identifier);
 
-      if(symbol.is_static_lifetime &&
-         symbol.type.id()!=ID_code &&
-         !symbol.is_extern &&
-         !symbol.location.get_function().empty() &&
-         local_static_set.insert(identifier).second)
+      if(
+        symbol.is_static_lifetime && symbol.type.id() != ID_code &&
+        !symbol.is_extern && symbol.has_local_scope &&
+        local_static_set.insert(identifier).second)
       {
         if(symbol.value.is_not_nil())
         {

src/goto-programs/read_bin_goto_object.cpp

@@ -60,7 +60,7 @@ static bool read_bin_goto_object_v5(
     sym.is_state_var = (flags &(1 << 9))!=0;
     sym.is_parameter = (flags &(1 << 8))!=0;
     sym.is_auxiliary = (flags &(1 << 7))!=0;
-    // sym.binding = (flags &(1 << 6))!=0;
+    sym.has_local_scope = (flags & (1 << 6)) != 0;
     sym.is_lvalue = (flags &(1 << 5))!=0;
     sym.is_static_lifetime = (flags &(1 << 4))!=0;
     sym.is_thread_local = (flags &(1 << 3))!=0;

src/goto-programs/show_symbol_table.cpp

@@ -223,7 +223,8 @@ static void show_symbol_table_json_ui(
       {"isVolatile", jsont::json_boolean(symbol.is_volatile)},
       {"isParameter", jsont::json_boolean(symbol.is_parameter)},
       {"isAuxiliary", jsont::json_boolean(symbol.is_auxiliary)},
-      {"isWeak", jsont::json_boolean(symbol.is_weak)}};
+      {"isWeak", jsont::json_boolean(symbol.is_weak)},
+      {"hasLocalScope", jsont::json_boolean(symbol.has_local_scope)}};
 
     result.push_back(id2string(symbol.name), std::move(symbol_json));
   }

src/goto-programs/write_goto_binary.cpp

@@ -62,7 +62,7 @@ bool write_goto_binary_v5(
     flags = (flags << 1) | static_cast<int>(sym.is_state_var);
     flags = (flags << 1) | static_cast<int>(sym.is_parameter);
     flags = (flags << 1) | static_cast<int>(sym.is_auxiliary);
-    flags = (flags << 1) | static_cast<int>(false); // sym.binding;
+    flags = (flags << 1) | static_cast<int>(sym.has_local_scope);
     flags = (flags << 1) | static_cast<int>(sym.is_lvalue);
     flags = (flags << 1) | static_cast<int>(sym.is_static_lifetime);
     flags = (flags << 1) | static_cast<int>(sym.is_thread_local);

src/json-symtab-language/json_symbol.cpp

@@ -107,6 +107,8 @@ symbolt symbol_from_json(const jsont &in)
       result.is_auxiliary = try_get_bool(kv.second, "isAuxiliary");
     else if(kv.first == "isWeak")
       result.is_weak = try_get_bool(kv.second, "isWeak");
+    else if(kv.first == "hasLocalScope")
+      result.has_local_scope = try_get_bool(kv.second, "hasLocalScope");
     else if(kv.first == "prettyType")
     {
     } // ignore

src/util/symbol.cpp

@@ -48,6 +48,8 @@ void symbolt::show(std::ostream &out) const
     out << " auxiliary";
   if(is_weak)
     out << " weak";
+  if(has_local_scope)
+    out << " local_scope";
   if(is_property)
     out << " property";
   if(is_state_var)
@@ -108,6 +110,7 @@ void symbolt::swap(symbolt &b)
   SYM_SWAP2(is_parameter);
   SYM_SWAP2(is_auxiliary);
   SYM_SWAP2(is_weak);
+  SYM_SWAP2(has_local_scope);
   SYM_SWAP2(is_lvalue);
   SYM_SWAP2(is_static_lifetime);
   SYM_SWAP2(is_thread_local);
@@ -220,6 +223,7 @@ bool symbolt::operator==(const symbolt &other) const
     is_parameter == other.is_parameter &&
     is_auxiliary == other.is_auxiliary &&
     is_weak == other.is_weak &&
+    has_local_scope == other.has_local_scope &&
     is_lvalue == other.is_lvalue &&
     is_static_lifetime == other.is_static_lifetime &&
     is_thread_local == other.is_thread_local &&

src/util/symbol.h

@@ -63,8 +63,8 @@ class symbolt
 
   // ANSI-C
   bool is_static_lifetime, is_thread_local;
-  bool is_lvalue, is_file_local, is_extern, is_volatile,
-       is_parameter, is_auxiliary, is_weak;
+  bool is_lvalue, is_file_local, is_extern, is_volatile, is_parameter,
+    is_auxiliary, is_weak, has_local_scope;
 
   symbolt()
   {
@@ -80,11 +80,10 @@ class symbolt
 
     name=module=base_name=mode=pretty_name=irep_idt();
 
-    is_type=is_macro=is_exported=
-    is_input=is_output=is_state_var=is_property=
-    is_static_lifetime=is_thread_local=
-    is_lvalue=is_file_local=is_extern=is_volatile=
-    is_parameter=is_auxiliary=is_weak=false;
+    is_type = is_macro = is_exported = is_input = is_output = is_state_var =
+      is_property = is_static_lifetime = is_thread_local = is_lvalue =
+        is_file_local = is_extern = is_volatile = is_parameter = is_auxiliary =
+          is_weak = has_local_scope = false;
   }
 
   void swap(symbolt &b);
@@ -153,6 +152,7 @@ class auxiliary_symbolt:public symbolt
     is_thread_local=true;
     is_file_local=true;
     is_auxiliary=true;
+    has_local_scope = true;
   }
 
   auxiliary_symbolt(const irep_idt &name, const typet &type):
@@ -177,6 +177,7 @@ class parameter_symbolt:public symbolt
     is_thread_local=true;
     is_file_local=true;
     is_parameter=true;
+    has_local_scope = true;
   }
 };