Fix dump-c output involving typedef names

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

Thanks Andreas Stahlbauer for providing the regression tests and help in
debugging.

Fixes: #882

Author: tautschnig

regression/goto-instrument/typedef1/main.c

@@ -0,0 +1,63 @@
+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 func_s {
+    struct chain_s body;
+} func;
+
+typedef struct node_s {
+  struct node_s *n;
+} node;
+
+typedef struct dumper_t_x {
+  node n;
+  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;
+}
+
+typedef unsigned int uint32_t;
+
+const uint32_t xx[2];
+
+typedef struct node_s2 {
+  uint32_t info;
+} node2;
+
+typedef struct {
+  int x;
+} anon_name;
+
+typedef struct node_s3 {
+  union {
+    struct node_s *n;
+    func *f;
+  } r;
+} node3;
+
+int main() {
+  node n;
+  chain c;
+  dumper_t a;
+  dumper_t b[3];
+  node2* sn;
+  anon_name d;
+  node3* s3;
+  alloc_dumper();
+  return 0;
+}

regression/goto-instrument/typedef1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--dump-c
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test should be run via chain.sh, which will try to recompile the dumped C
+code. Missing/incomplete typedef output would cause a failure.

src/goto-instrument/dump_c.cpp

@@ -62,6 +62,8 @@ void dump_ct::operator()(std::ostream &os)
   std::stringstream func_body_stream;
   local_static_declst local_static_decls;
 
+  gather_global_typedefs();
+
   // add copies of struct types when ID_C_transparent_union is only
   // annotated to parameter
   symbol_tablet symbols_transparent;
@@ -113,6 +115,9 @@ void dump_ct::operator()(std::ostream &os)
     symbolt &symbol=it->second;
     bool tag_added=false;
 
+    // TODO we could get rid of some of the ID_anonymous by looking up
+    // the origin symbol types in typedef_types and adjusting any other
+    // uses of ID_tag
     if((symbol.type.id()==ID_union || symbol.type.id()==ID_struct) &&
        symbol.type.get(ID_tag).empty())
     {
@@ -285,6 +290,8 @@ void dump_ct::operator()(std::ostream &os)
     os << std::endl;
   }
 
+  dump_typedefs(os);
+
   if(!func_decl_stream.str().empty())
     os << func_decl_stream.str() << std::endl;
   if(!compound_body_stream.str().empty())
@@ -408,6 +415,9 @@ void dump_ct::convert_compound(
   if(!converted_compound.insert(name).second)
     return;
 
+  // make sure typedef names used in the declaration are available
+  collect_typedefs(type, true);
+
   const irept &bases = type.find(ID_bases);
   std::stringstream base_decls;
   forall_irep(parent_it, bases.get_sub())
@@ -466,8 +476,13 @@ void dump_ct::convert_compound(
     while(non_array_type->id()==ID_array)
       non_array_type=&(ns.follow(non_array_type->subtype()));
 
-    if(recursive && non_array_type->id()!=ID_pointer)
-      convert_compound(comp.type(), comp.type(), recursive, os);
+    if(recursive)
+    {
+      if(non_array_type->id()!=ID_pointer)
+        convert_compound(comp.type(), comp.type(), recursive, os);
+      else
+        collect_typedefs(comp.type(), true);
+    }
 
     irep_idt comp_name=comp.get_name();
 
@@ -521,7 +536,21 @@ void dump_ct::convert_compound(
     struct_body << ";" << std::endl;
   }
 
-  os << type_to_string(unresolved);
+  typet unresolved_clean=unresolved;
+  typedef_typest::const_iterator td_entry=
+    typedef_types.find(unresolved);
+  irep_idt typedef_str;
+  if(td_entry!=typedef_types.end())
+  {
+    unresolved_clean.remove(ID_C_typedef);
+    typedef_str=td_entry->second;
+    std::pair<std::string, bool> &td_map_entry=typedef_map[typedef_str];
+    if(!td_map_entry.second)
+      td_map_entry.first="";
+    os << "typedef ";
+  }
+
+  os << type_to_string(unresolved_clean);
   if(!base_decls.str().empty())
   {
     assert(language->id()=="cpp");
@@ -548,6 +577,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;
@@ -901,6 +932,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(),
@@ -909,6 +944,7 @@ void dump_ct::cleanup_decl(
     b,
     local_static,
     local_type_decls,
+    typedef_names,
     system_headers);
   p2s();
 
@@ -918,6 +954,132 @@ void dump_ct::cleanup_decl(
 
 /*******************************************************************\
 
+Function: dump_ct::collect_typedefs
+
+Inputs:
+    type  Type to inspect for ID_C_typedef entry
+    early Set to true to enforce that typedef is dumped before any
+          function declarations or struct definitions
+
+Outputs:
+
+Purpose: Find any typedef names contained in the input type and store
+         their declaration strings in typedef_map for eventual output.
+
+\*******************************************************************/
+
+void dump_ct::collect_typedefs(const typet &type, bool early)
+{
+  if(type.id()==ID_code)
+  {
+    const code_typet &code_type=to_code_type(type);
+
+    collect_typedefs(code_type.return_type(), early);
+    for(const auto &param : code_type.parameters())
+      collect_typedefs(param.type(), early);
+  }
+  else if(type.id()==ID_pointer || type.id()==ID_array)
+  {
+    collect_typedefs(type.subtype(), early);
+  }
+  else if(type.id()==ID_symbol)
+  {
+    const symbolt &symbol=
+      ns.lookup(to_symbol_type(type).get_identifier());
+    collect_typedefs(symbol.type, early);
+  }
+
+  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, {"", early}});
+
+    if(entry.second)
+    {
+      if(typedef_str=="__gnuc_va_list" || typedef_str == "va_list")
+      {
+        system_headers.insert("stdarg.h");
+      }
+      else
+      {
+        typet t=type;
+        t.remove(ID_C_typedef);
+
+        std::ostringstream oss;
+        oss << "typedef " << type_to_string(t) << " "
+            << typedef_str << ';';
+
+        entry.first->second.first=oss.str();
+      }
+    }
+    else if(early)
+    {
+      entry.first->second.second=true;
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: dump_ct::gather_global_typedefs
+
+Inputs:
+
+Outputs:
+
+Purpose: find all global typdefs in the symbol table and store them
+         in typedef_types
+
+\*******************************************************************/
+
+void dump_ct::gather_global_typedefs()
+{
+  for(const auto &symbol_entry : copied_symbol_table.symbols)
+  {
+    const symbolt &symbol=symbol_entry.second;
+
+    if(symbol.is_macro && symbol.is_type && !ignore(symbol) &&
+       symbol.location.get_function().empty())
+    {
+      assert(!symbol.type.get(ID_C_typedef).empty());
+      typedef_types[symbol.type]=symbol.type.get(ID_C_typedef);
+      collect_typedefs(symbol.type, false);
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: dump_ct::dump_typedefs
+
+Inputs:
+
+Outputs: os  output stream
+
+Purpose: print all typedefs that are not covered via
+         typedef struct xyz { ... } name;
+
+\*******************************************************************/
+
+void dump_ct::dump_typedefs(std::ostream &os) const
+{
+  bool need_newline=false;
+
+  for(const auto &td : typedef_map)
+    if(!td.second.first.empty())
+    {
+      need_newline=true;
+      os << td.second.first << std::endl;
+    }
+
+  if(need_newline)
+    os << std::endl;
+}
+
+/*******************************************************************\
+
 Function: dump_ct::convert_global_variables
 
 Inputs:
@@ -1024,13 +1186,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();
 
@@ -1069,6 +1236,10 @@ void dump_ct::convert_function_declaration(
     os_decl << "// " << symbol.location << std::endl;
     os_decl << make_decl(symbol.name, symbol.type) << ";" << std::endl;
   }
+
+  // make sure typedef names used in the function declaration are
+  // available
+  collect_typedefs(symbol.type, true);
 }
 
 /*******************************************************************\

src/goto-instrument/dump_c_class.h

@@ -59,6 +59,11 @@ class dump_ct
     declared_enum_constants_mapt;
   declared_enum_constants_mapt declared_enum_constants;
 
+  typedef std::map<irep_idt, std::pair<std::string, bool>> typedef_mapt;
+  typedef_mapt typedef_map;
+  typedef std::unordered_map<typet, irep_idt, irep_hash> typedef_typest;
+  typedef_typest typedef_types;
+
   void init_system_library_map();
 
   std::string type_to_string(const typet &type);
@@ -85,6 +90,10 @@ class dump_ct
     return d_str.substr(0, d_str.size()-1);
   }
 
+  void collect_typedefs(const typet &type, bool early);
+  void gather_global_typedefs();
+  void dump_typedefs(std::ostream &os) const;
+
   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)