Add --dump-c-type-header to goto-instrument

The --dump-c-type-header flag is going to dump a header file
containing the file local type definitions in a c file.
While it might be desirable to keep a type definition
only in a c module, for some proofs it is required to
include the type definition supporting the harness setup.
If the file local type definition requires to include types defined
in other header files, an include for the other header file
is added as well.

src/goto-instrument/dump_c.cpp

@@ -13,8 +13,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/config.h>
 #include <util/find_symbols.h>
+#include <util/get_base_name.h>
 #include <util/invariant.h>
 #include <util/replace_symbol.h>
+#include <util/string_utils.h>
 
 #include <ansi-c/ansi_c_language.h>
 #include <cpp/cpp_language.h>
@@ -46,6 +48,7 @@ void dump_ct::operator()(std::ostream &os)
   std::stringstream compound_body_stream;
   std::stringstream global_var_stream;
   std::stringstream global_decl_stream;
+  std::stringstream global_decl_header_stream;
   std::stringstream func_body_stream;
   local_static_declst local_static_decls;
 
@@ -169,6 +172,7 @@ void dump_ct::operator()(std::ostream &os)
 
   // collect all declarations we might need, include local static variables
   bool skip_function_main=false;
+  std::vector<std::string> header_files;
   for(std::set<std::string>::const_iterator
       it=symbols_sorted.begin();
       it!=symbols_sorted.end();
@@ -188,6 +192,24 @@ void dump_ct::operator()(std::ostream &os)
         global_decl_stream << "// " << symbol.name << '\n';
         global_decl_stream << "// " << symbol.location << '\n';
 
+        std::string location_file =
+          get_base_name(id2string(symbol.location.get_file()), false);
+        // collect header the types are borrowed from
+        // expect header files to end in .h
+        if(
+          location_file.length() > 1 &&
+          location_file[location_file.length() - 1] == 'h')
+        {
+          std::vector<std::string>::iterator it =
+            find(header_files.begin(), header_files.end(), location_file);
+          if(it == header_files.end())
+          {
+            header_files.push_back(location_file);
+            global_decl_header_stream << "#include \"" << location_file
+                                      << "\"\n";
+          }
+        }
+
         if(type_id==ID_c_enum)
           convert_compound_enum(symbol.type, global_decl_stream);
         else if(type_id == ID_struct)
@@ -204,7 +226,7 @@ void dump_ct::operator()(std::ostream &os)
     }
     else if(
       symbol.is_static_lifetime && symbol.type.id() != ID_code &&
-      !symbol.type.get_bool(ID_C_no_dump))
+      !symbol.type.get_bool(ID_C_do_not_dump))
       convert_global_variable(
           symbol,
           global_var_stream,
@@ -320,8 +342,10 @@ void dump_ct::convert_compound_declaration(
 {
   if(
     !symbol.location.get_function().empty() ||
-    symbol.type.get_bool(ID_C_no_dump))
+    symbol.type.get_bool(ID_C_do_not_dump))
+  {
     return;
+  }
 
   // do compound type body
   if(symbol.type.id() == ID_struct)
@@ -403,7 +427,7 @@ void dump_ct::convert_compound(
 {
   const irep_idt &name=type.get(ID_tag);
 
-  if(!converted_compound.insert(name).second || type.get_bool(ID_C_no_dump))
+  if(!converted_compound.insert(name).second || type.get_bool(ID_C_do_not_dump))
     return;
 
   // make sure typedef names used in the declaration are available
@@ -524,19 +548,23 @@ void dump_ct::convert_compound(
   }
 
   typet unresolved_clean=unresolved;
-  typedef_typest::const_iterator td_entry=
-    typedef_types.find(unresolved);
   irep_idt typedef_str;
-  if(td_entry!=typedef_types.end())
+  for(auto td_entry : typedef_types)
   {
-    unresolved_clean.remove(ID_C_typedef);
-    typedef_str=td_entry->second;
-    std::pair<typedef_mapt::iterator, bool> td_map_entry=
-      typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
-    PRECONDITION(!td_map_entry.second);
-    if(!td_map_entry.first->second.early)
-      td_map_entry.first->second.type_decl_str.clear();
-    os << "typedef ";
+    if(
+      td_entry.first.get(ID_identifier) == unresolved.get(ID_identifier) &&
+      (td_entry.first.source_location() == unresolved.source_location()))
+    {
+      unresolved_clean.remove(ID_C_typedef);
+      typedef_str = td_entry.second;
+      std::pair<typedef_mapt::iterator, bool> td_map_entry =
+        typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
+      PRECONDITION(!td_map_entry.second);
+      if(!td_map_entry.first->second.early)
+        td_map_entry.first->second.type_decl_str.clear();
+      os << "typedef ";
+      break;
+    }
   }
 
   os << type_to_string(unresolved_clean);
@@ -1463,3 +1491,49 @@ void dump_cpp(
     new_cpp_language);
   out << goto2cpp;
 }
+
+static bool
+module_local_declaration(const symbolt &symbol, const std::string module)
+{
+  std::string base_name =
+    get_base_name(id2string(symbol.location.get_file()), true);
+  std::string symbol_module = strip_string(id2string(symbol.module));
+  return (base_name == module && symbol_module == module);
+}
+
+void dump_c_type_header(
+  const goto_functionst &src,
+  const bool use_system_headers,
+  const bool use_all_headers,
+  const bool include_harness,
+  const namespacet &ns,
+  const std::string module,
+  std::ostream &out)
+{
+  symbol_tablet symbol_table = ns.get_symbol_table();
+  for(symbol_tablet::iteratort it = symbol_table.begin();
+      it != symbol_table.end();
+      it++)
+  {
+    symbolt &new_symbol = it.get_writeable_symbol();
+    if(module_local_declaration(new_symbol, module))
+    {
+      new_symbol.type.set(ID_C_do_not_dump, 0);
+    }
+    else
+    {
+      new_symbol.type.set(ID_C_do_not_dump, 1);
+    }
+  }
+
+  namespacet new_ns(symbol_table);
+  dump_ct goto2c(
+    src,
+    use_system_headers,
+    use_all_headers,
+    include_harness,
+    new_ns,
+    new_ansi_c_language,
+    dump_c_configurationt::type_header_configuration);
+  out << goto2c;
+}

src/goto-instrument/dump_c.h

@@ -22,6 +22,15 @@ void dump_c(
   const namespacet &ns,
   std::ostream &out);
 
+void dump_c_type_header(
+  const goto_functionst &src,
+  const bool use_system_headers,
+  const bool use_all_headers,
+  const bool include_harness,
+  const namespacet &ns,
+  const std::string module,
+  std::ostream &out);
+
 void dump_cpp(
   const goto_functionst &src,
   const bool use_system_headers,

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -639,9 +639,12 @@ int goto_instrument_parse_optionst::doit()
       return CPROVER_EXIT_SUCCESS;
     }
 
-    if(cmdline.isset("dump-c") || cmdline.isset("dump-cpp"))
+    if(
+      cmdline.isset("dump-c") || cmdline.isset("dump-cpp") ||
+      cmdline.isset("dump-c-type-header"))
     {
       const bool is_cpp=cmdline.isset("dump-cpp");
+      const bool is_header = cmdline.isset("dump-c-type-header");
       const bool h_libc=!cmdline.isset("no-system-headers");
       const bool h_all=cmdline.isset("use-all-headers");
       const bool harness=cmdline.isset("harness");
@@ -663,22 +666,42 @@ int goto_instrument_parse_optionst::doit()
           log.error() << "failed to write to `" << cmdline.args[1] << "'";
           return CPROVER_EXIT_CONVERSION_FAILED;
         }
-        (is_cpp ? dump_cpp : dump_c)(
-          goto_model.goto_functions,
-          h_libc,
-          h_all,
-          harness,
-          ns,
-          out);
+        if(is_header)
+        {
+          dump_c_type_header(
+            goto_model.goto_functions,
+            h_libc,
+            h_all,
+            harness,
+            ns,
+            cmdline.get_value("dump-c-type-header"),
+            out);
+        }
+        else
+        {
+          (is_cpp ? dump_cpp : dump_c)(
+            goto_model.goto_functions, h_libc, h_all, harness, ns, out);
+        }
       }
       else
-        (is_cpp ? dump_cpp : dump_c)(
-          goto_model.goto_functions,
-          h_libc,
-          h_all,
-          harness,
-          ns,
-          std::cout);
+      {
+        if(is_header)
+        {
+          dump_c_type_header(
+            goto_model.goto_functions,
+            h_libc,
+            h_all,
+            harness,
+            ns,
+            cmdline.get_value("dump-c-type-header"),
+            std::cout);
+        }
+        else
+        {
+          (is_cpp ? dump_cpp : dump_c)(
+            goto_model.goto_functions, h_libc, h_all, harness, ns, std::cout);
+        }
+      }
 
       return CPROVER_EXIT_SUCCESS;
     }
@@ -1555,6 +1578,7 @@ void goto_instrument_parse_optionst::help()
     " --document-properties-html   generate HTML property documentation\n"
     " --document-properties-latex  generate Latex property documentation\n"
     " --dump-c                     generate C source\n"
+    " --dump-c-type-header m       generate a C header for types local in m\n"
     " --dump-cpp                   generate C++ source\n"
     " --dot                        generate CFG graph in DOT format\n"
     " --interpreter                do concrete execution\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -39,6 +39,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(all)" \
   "(document-claims-latex)(document-claims-html)" \
   "(document-properties-latex)(document-properties-html)" \
+  "(dump-c-type-header):" \
   "(dump-c)(dump-cpp)(no-system-headers)(use-all-headers)(dot)(xml)" \
   "(harness)" \
   OPT_GOTO_CHECK \

src/util/irep_ids.def

@@ -19,6 +19,7 @@ IREP_ID_ONE(x86_extended)
 IREP_ID_TWO(C_source_location, #source_location)
 IREP_ID_TWO(C_end_location, #end_location)
 IREP_ID_TWO(C_is_padding, #is_padding)
+IREP_ID_ONE(C_do_not_dump)
 IREP_ID_ONE(file)
 IREP_ID_ONE(line)
 IREP_ID_ONE(column)