Merge pull request #7162 from tautschnig/bugfixes/7158-dump-c

Dump-C: support struct/union types without tags

Author: tautschnig

regression/goto-instrument/dump-non-tag-struct/main.c

@@ -0,0 +1,9 @@
+#include <stdlib.h>
+
+int main()
+{
+  // CBMC's model of calloc includes an overflow check, which in turn creates a
+  // struct that holds both the arithmetic result and the overflow information.
+  // dump-c did not support this struct defined in place.
+  calloc(10, 1);
+}

regression/goto-instrument/dump-non-tag-struct/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--dump-c
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+^Invariant check failed
+^warning: ignoring
+irep
+--
+This test must pass compiling the output generated using dump-c, which implies
+that dump-c succeeded and that all struct declarations are present.

src/goto-instrument/dump_c.cpp

@@ -25,11 +25,35 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/string_utils.h>
 
 #include <ansi-c/expr2c.h>
+#include <ansi-c/type2name.h>
+#include <cpp/cpp_type2name.h>
 #include <cpp/expr2cpp.h>
 #include <linking/static_lifetime_init.h>
 
 #include "goto_program2code.h"
 
+static std::string clean_identifier(const irep_idt &id)
+{
+  std::string result;
+  result.reserve(id2string(id).size());
+
+  for(auto c : id2string(id))
+  {
+    if(c >= '0' && c <= '9')
+      result += c;
+    else if(c >= 'A' && c <= 'Z')
+      result += c;
+    else if(c >= 'a' && c <= 'z')
+      result += c;
+    else if(c == '_' || c == '$')
+      result += c;
+    else
+      result += "_" + std::to_string(c);
+  }
+
+  return result;
+}
+
 dump_c_configurationt dump_c_configurationt::default_configuration =
   dump_c_configurationt();
 
@@ -58,11 +82,32 @@ void dump_ct::operator()(std::ostream &os)
 
   // add copies of struct types when ID_C_transparent_union is only
   // annotated to parameter
-  symbol_tablet symbols_transparent;
+  symbol_tablet additional_symbols;
   for(const auto &named_symbol : copied_symbol_table.symbols)
   {
     const symbolt &symbol=named_symbol.second;
 
+    if(
+      (symbol.type.id() == ID_union || symbol.type.id() == ID_struct) &&
+      !symbol.is_type)
+    {
+      type_symbolt ts{symbol.type};
+      ts.mode = symbol.mode;
+      if(mode == ID_C)
+        ts.name = "tag-" + type2name(symbol.type, ns);
+      else if(mode == ID_cpp)
+        ts.name = "tag-" + cpp_type2name(symbol.type);
+      else
+        UNREACHABLE;
+      typet &type =
+        copied_symbol_table.get_writeable_ref(named_symbol.first).type;
+      if(ts.type.id() == ID_union)
+        type = union_tag_typet{ts.name};
+      else
+        type = struct_tag_typet{ts.name};
+      additional_symbols.add(ts);
+    }
+
     if(symbol.type.id()!=ID_code)
       continue;
 
@@ -86,14 +131,14 @@ void dump_ct::operator()(std::ostream &os)
         new_type_sym.type.set(ID_C_transparent_union, true);
 
         // we might have it already, in which case this has no effect
-        symbols_transparent.add(new_type_sym);
+        additional_symbols.add(new_type_sym);
 
         to_union_tag_type(type).set_identifier(new_type_sym.name);
         type.remove(ID_C_transparent_union);
       }
     }
   }
-  for(const auto &symbol_pair : symbols_transparent.symbols)
+  for(const auto &symbol_pair : additional_symbols.symbols)
   {
     copied_symbol_table.add(symbol_pair.second);
   }
@@ -509,11 +554,11 @@ void dump_ct::convert_compound(
         collect_typedefs(comp.type(), true);
     }
 
-    irep_idt comp_name=comp.get_name();
-
-    struct_body << indent(1) << "// " << comp_name << '\n';
+    struct_body << indent(1) << "// " << comp.get_name() << '\n';
     struct_body << indent(1);
 
+    irep_idt comp_name = clean_identifier(comp.get_name());
+
     // component names such as "main" would collide with other objects in the
     // namespace
     std::string fake_unique_name="NO/SUCH/NS::"+id2string(comp_name);
@@ -1519,6 +1564,12 @@ void dump_ct::cleanup_expr(exprt &expr)
       expr = unary_exprt{ID_initializer_list, bu.value()};
     }
   }
+  else if(expr.id() == ID_member)
+  {
+    member_exprt &member_expr = to_member_expr(expr);
+    member_expr.set_component_name(
+      clean_identifier(member_expr.get_component_name()));
+  }
 }
 
 void dump_ct::cleanup_type(typet &type)