Fix dump-c output involving typedef names

Follow-up to 99067de, which made expr2c prefer typedef names over
original type expressions.

Author: tautschnig

regression/goto-instrument/typedef1/main.c

@@ -0,0 +1,41 @@
+typedef long int off_t;
+typedef signed char smallint;
+
+typedef struct chain_s {
+    struct node_s *first;
+    struct node_s *last;
+    const char *programname;
+} chain;
+
+typedef struct node_s { 
+    struct node_s *n;
+} node;
+
+typedef struct dumper_t_x
+{
+  node n; //chaning this line to 'struct node_s n' removes some bugs
+  off_t dump_skip;
+  signed int dump_length;
+  smallint dump_vflag;
+} dumper_t;
+
+typedef struct FS_x
+{
+  struct FS *nextfs;
+  signed int bcnt;
+} FS;
+
+
+dumper_t * alloc_dumper(void)
+{
+  return (void*) 0;
+}
+
+int main() {
+    node n;
+    chain c;
+    dumper_t a;
+    dumper_t b[3];
+	alloc_dumper();
+	return 0;
+}

regression/goto-instrument/typedef1/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--dump-c
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/goto-instrument/dump_c.cpp

@@ -285,6 +285,13 @@ void dump_ct::operator()(std::ostream &os)
     os << std::endl;
   }
 
+  // global typedefs
+  for(const auto &td : typedef_map)
+    if(!td.second.empty())
+      os << td.second << std::endl;
+  if(!typedef_map.empty())
+    os << std::endl;
+
   if(!func_decl_stream.str().empty())
     os << func_decl_stream.str() << std::endl;
   if(!compound_body_stream.str().empty())
@@ -338,6 +345,8 @@ void dump_ct::convert_compound(
   bool recursive,
   std::ostream &os)
 {
+  collect_typedefs(type);
+
   if(type.id()==ID_symbol)
   {
     const symbolt &symbol=
@@ -468,6 +477,8 @@ void dump_ct::convert_compound(
 
     if(recursive && non_array_type->id()!=ID_pointer)
       convert_compound(comp.type(), comp.type(), recursive, os);
+    else
+      collect_typedefs(comp.type());
 
     irep_idt comp_name=comp.get_name();
 
@@ -521,7 +532,16 @@ void dump_ct::convert_compound(
     struct_body << ";" << std::endl;
   }
 
-  os << type_to_string(unresolved);
+  typet unresolved_clean=unresolved;
+  const irep_idt &typedef_str=unresolved.get(ID_C_typedef);
+  if(!typedef_str.empty())
+  {
+    unresolved_clean.remove(ID_C_typedef);
+    typedef_map[typedef_str]="";
+    os << "typedef ";
+  }
+
+  os << type_to_string(unresolved_clean);
   if(!base_decls.str().empty())
   {
     assert(language->id()=="cpp");
@@ -548,6 +568,8 @@ void dump_ct::convert_compound(
     os << " __attribute__ ((__transparent_union__))";
   if(type.get_bool(ID_C_packed))
     os << " __attribute__ ((__packed__))";
+  if(!typedef_str.empty())
+    os << " " << typedef_str;
   os << ";";
   os << std::endl;
   os << std::endl;
@@ -898,6 +920,10 @@ void dump_ct::cleanup_decl(
 
   tmp.add_instruction(END_FUNCTION);
 
+  std::unordered_set<irep_idt, irep_id_hash> typedef_names;
+  for(const auto &td : typedef_map)
+    typedef_names.insert(td.first);
+
   code_blockt b;
   goto_program2codet p2s(
     irep_idt(),
@@ -906,6 +932,7 @@ void dump_ct::cleanup_decl(
     b,
     local_static,
     local_type_decls,
+    typedef_names,
     system_headers);
   p2s();
 
@@ -915,6 +942,66 @@ void dump_ct::cleanup_decl(
 
 /*******************************************************************\
 
+Function: dump_ct::collect_typedefs
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+void dump_ct::collect_typedefs(const typet &type)
+{
+  if(type.id()==ID_code)
+  {
+    const code_typet &code_type=to_code_type(type);
+
+    collect_typedefs(code_type.return_type());
+    for(const auto &param : code_type.parameters())
+      collect_typedefs(param.type());
+  }
+  else if(type.id()==ID_pointer || type.id()==ID_array)
+  {
+    collect_typedefs(type.subtype());
+  }
+  else if(type.id()==ID_symbol)
+  {
+    const symbolt &symbol=
+      ns.lookup(to_symbol_type(type).get_identifier());
+    collect_typedefs(symbol.type);
+  }
+
+  const irep_idt &typedef_str=type.get(ID_C_typedef);
+
+  if(!typedef_str.empty())
+  {
+    std::pair<typedef_mapt::iterator, bool> entry=
+      typedef_map.insert({typedef_str, ""});
+
+    if(entry.second &&
+       (typedef_str=="__gnuc_va_list" ||
+        typedef_str == "va_list"))
+    {
+      system_headers.insert("stdarg.h");
+    }
+    else if(entry.second)
+    {
+      typet t=type;
+      t.remove(ID_C_typedef);
+
+      std::ostringstream oss;
+      oss << "typedef " << type_to_string(t) << " "
+          << typedef_str << ';';
+
+      entry.first->second=oss.str();
+    }
+  }
+}
+
+/*******************************************************************\
+
 Function: dump_ct::convert_global_variables
 
 Inputs:
@@ -935,6 +1022,9 @@ void dump_ct::convert_global_variable(
       !converted_global.insert(symbol.name).second)
     return;
 
+  if(func.empty() || symbol.is_extern)
+    collect_typedefs(symbol.type);
+
   code_declt d(symbol.symbol_expr());
 
   find_symbols_sett syms;
@@ -1021,13 +1111,18 @@ void dump_ct::convert_function_declaration(
     code_blockt b;
     std::list<irep_idt> type_decls, local_static;
 
+    std::unordered_set<irep_idt, irep_id_hash> typedef_names;
+    for(const auto &td : typedef_map)
+      typedef_names.insert(td.first);
+
     goto_program2codet p2s(
       symbol.name,
       func_entry->second.body,
       copied_symbol_table,
       b,
       local_static,
       type_decls,
+      typedef_names,
       system_headers);
     p2s();
 
@@ -1062,6 +1157,8 @@ void dump_ct::convert_function_declaration(
   if(symbol.name!=goto_functionst::entry_point() &&
      symbol.name!=ID_main)
   {
+    collect_typedefs(symbol.type);
+
     os_decl << "// " << symbol.name << std::endl;
     os_decl << "// " << symbol.location << std::endl;
     os_decl << make_decl(symbol.name, symbol.type) << ";" << std::endl;

src/goto-instrument/dump_c_class.h

@@ -59,6 +59,9 @@ class dump_ct
     declared_enum_constants_mapt;
   declared_enum_constants_mapt declared_enum_constants;
 
+  typedef std::map<irep_idt, std::string> typedef_mapt;
+  typedef_mapt typedef_map;
+
   void init_system_library_map();
 
   std::string type_to_string(const typet &type);
@@ -85,6 +88,8 @@ class dump_ct
     return d_str.substr(0, d_str.size()-1);
   }
 
+  void collect_typedefs(const typet &type);
+
   void convert_compound_declaration(
       const symbolt &symbol,
       std::ostream &os_body);

src/goto-instrument/goto_program2code.cpp

@@ -1818,6 +1818,11 @@ void goto_program2codet::cleanup_code(
 
     add_local_types(code.op0().type());
 
+    const irep_idt &typedef_str=code.op0().type().get(ID_C_typedef);
+    if(!typedef_str.empty() &&
+       typedef_names.find(typedef_str)==typedef_names.end())
+      code.op0().type().remove(ID_C_typedef);
+
     return;
   }
   else if(code.get_statement()==ID_function_call)

src/goto-instrument/goto_program2code.h

@@ -49,6 +49,7 @@ class goto_program2codet
       code_blockt &_dest,
       id_listt &_local_static,
       id_listt &_type_names,
+      const id_sett &_typedef_names,
       std::set<std::string> &_system_headers):
     func_name(identifier),
     goto_program(_goto_program),
@@ -57,6 +58,7 @@ class goto_program2codet
     toplevel_block(_dest),
     local_static(_local_static),
     type_names(_type_names),
+    typedef_names(_typedef_names),
     system_headers(_system_headers)
   {
     assert(local_static.empty());
@@ -78,6 +80,7 @@ class goto_program2codet
   code_blockt &toplevel_block;
   id_listt &local_static;
   id_listt &type_names;
+  const id_sett &typedef_names;
   std::set<std::string> &system_headers;
   std::unordered_set<exprt, irep_hash> va_list_expr;