dump-c: use a custom expr2c configuration

This avoids working around expr2c internals.

Author: tautschnig

src/goto-instrument/dump_c.cpp

@@ -20,8 +20,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/replace_symbol.h>
 #include <util/string_utils.h>
 
-#include <ansi-c/ansi_c_language.h>
-#include <cpp/cpp_language.h>
+#include <ansi-c/expr2c.h>
+#include <cpp/expr2cpp.h>
 
 #include <linking/static_lifetime_init.h>
 
@@ -526,7 +526,7 @@ void dump_ct::convert_compound(
       if(t.get_width()<=config.ansi_c.long_long_int_width)
         struct_body << "long long int " << comp_name
           << " : " << t.get_width();
-      else if(language->id()=="cpp")
+      else if(mode == ID_cpp)
         struct_body << "__signedbv<" << t.get_width() << "> "
           << comp_name;
       else
@@ -538,7 +538,7 @@ void dump_ct::convert_compound(
       if(t.get_width()<=config.ansi_c.long_long_int_width)
         struct_body << "unsigned long long " << comp_name
           << " : " << t.get_width();
-      else if(language->id()=="cpp")
+      else if(mode == ID_cpp)
         struct_body << "__unsignedbv<" << t.get_width() << "> "
           << comp_name;
       else
@@ -573,7 +573,7 @@ void dump_ct::convert_compound(
   os << type_to_string(unresolved_clean);
   if(!base_decls.str().empty())
   {
-    PRECONDITION(language->id()=="cpp");
+    PRECONDITION(mode == ID_cpp);
     os << ": " << base_decls.str();
   }
   os << '\n';
@@ -1521,22 +1521,49 @@ void dump_ct::cleanup_type(typet &type)
     !type.get(ID_tag).empty());
 }
 
+static expr2c_configurationt expr2c_configuration()
+{
+  // future TODO: with C++20 we can actually use designated initializers as
+  // commented out below
+  static expr2c_configurationt configuration{
+    /* .include_struct_padding_components = */ true,
+    /* .print_struct_body_in_type = */ true,
+    /* .include_array_size = */ true,
+    /* .true_string = */ "1",
+    /* .false_string = */ "0",
+    /* .use_library_macros = */ true,
+    /* .print_enum_int_value = */ false,
+    /* .expand_typedef = */ false};
+
+  return configuration;
+}
+
 std::string dump_ct::type_to_string(const typet &type)
 {
   std::string ret;
   typet t=type;
   cleanup_type(t);
-  language->from_type(t, ret, ns);
-  return ret;
+
+  if(mode == ID_C)
+    return type2c(t, ns, expr2c_configuration());
+  else if(mode == ID_cpp)
+    return type2cpp(t, ns);
+  else
+    UNREACHABLE;
 }
 
 std::string dump_ct::expr_to_string(const exprt &expr)
 {
   std::string ret;
   exprt e=expr;
   cleanup_expr(e);
-  language->from_expr(e, ret, ns);
-  return ret;
+
+  if(mode == ID_C)
+    return expr2c(e, ns, expr2c_configuration());
+  else if(mode == ID_cpp)
+    return expr2cpp(e, ns);
+  else
+    UNREACHABLE;
 }
 
 void dump_c(
@@ -1548,12 +1575,7 @@ void dump_c(
   std::ostream &out)
 {
   dump_ct goto2c(
-    src,
-    use_system_headers,
-    use_all_headers,
-    include_harness,
-    ns,
-    new_ansi_c_language);
+    src, use_system_headers, use_all_headers, include_harness, ns, ID_C);
   out << goto2c;
 }
 
@@ -1566,12 +1588,7 @@ void dump_cpp(
   std::ostream &out)
 {
   dump_ct goto2cpp(
-    src,
-    use_system_headers,
-    use_all_headers,
-    include_harness,
-    ns,
-    new_cpp_language);
+    src, use_system_headers, use_all_headers, include_harness, ns, ID_cpp);
   out << goto2cpp;
 }
 
@@ -1616,7 +1633,7 @@ void dump_c_type_header(
     use_all_headers,
     include_harness,
     new_ns,
-    new_ansi_c_language,
+    ID_C,
     dump_c_configurationt::type_header_configuration);
   out << goto2c;
 }

src/goto-instrument/dump_c_class.h

@@ -14,10 +14,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <set>
 #include <string>
-#include <memory> // unique_ptr
-
-#include <langapi/language.h>
-#include <langapi/mode.h>
 
 #include <goto-programs/system_library_symbols.h>
 
@@ -116,13 +112,13 @@ class dump_ct
     const bool use_all_headers,
     const bool include_harness,
     const namespacet &_ns,
-    language_factoryt factory,
+    const irep_idt &mode,
     const dump_c_configurationt config)
     : goto_functions(_goto_functions),
       copied_symbol_table(_ns.get_symbol_table()),
       ns(copied_symbol_table),
       dump_c_config(config),
-      language(factory()),
+      mode(mode),
       harness(include_harness),
       system_symbols(use_system_headers)
   {
@@ -135,14 +131,14 @@ class dump_ct
     const bool use_all_headers,
     const bool include_harness,
     const namespacet &_ns,
-    language_factoryt factory)
+    const irep_idt &mode)
     : dump_ct(
         _goto_functions,
         use_system_headers,
         use_all_headers,
         include_harness,
         _ns,
-        factory,
+        mode,
         dump_c_configurationt::default_configuration)
   {
   }
@@ -156,7 +152,7 @@ class dump_ct
   symbol_tablet copied_symbol_table;
   const namespacet ns;
   const dump_c_configurationt dump_c_config;
-  std::unique_ptr<languaget> language;
+  const irep_idt mode;
   const bool harness;
 
   typedef std::unordered_set<irep_idt> convertedt;

src/goto-instrument/goto_program2code.cpp

@@ -1893,20 +1893,6 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
     }
     else if(expr.type().id()==ID_pointer)
       add_local_types(expr.type());
-    else if(expr.type().id() == ID_bool)
-    {
-      expr = typecast_exprt(
-        from_integer(
-          expr.is_true() ? 1 : 0, signedbv_typet(config.ansi_c.int_width)),
-        bool_typet());
-    }
-    else if(expr.type().id() == ID_c_bool)
-    {
-      expr = typecast_exprt(
-        from_integer(
-          expr.is_one() ? 1 : 0, signedbv_typet(config.ansi_c.int_width)),
-        c_bool_type());
-    }
 
     const irept &c_sizeof_type=expr.find(ID_C_c_sizeof_type);