Merge pull request #5867 from tautschnig/dump-c-bool-constant

dump-c: fix output of _Bool-typed constants

Author: tautschnig

regression/goto-instrument/dump-bool/main.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int main()
+{
+  _Bool v;
+  v = 1;
+  assert(v == 1);
+}

regression/goto-instrument/dump-bool/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--dump-c
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Dump-c previously always generated 0 for _Bool or __CPROVER_bool-typed
+constants. This test ensures that the value "1" (in v = 1) is correctly
+generated, instead of a spurious (v = (__CPROVER_bool)0).

regression/goto-instrument/dump-union2/main.c

@@ -12,6 +12,7 @@ union U10 {
 };
 
 union U10 g_2110 = {.f0 = 53747};
+union U10 g_1256 = {-6L};
 
 union U6 {
   signed f0 : 3;

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';
@@ -1469,11 +1469,18 @@ void dump_ct::cleanup_expr(exprt &expr)
       }
     }
 
+    optionalt<exprt> clean_init;
     if(
       ns.follow(bu.type()).id() == ID_union &&
-      bu.source_location().get_function().empty() &&
-      bu.op() == zero_initializer(bu.op().type(), source_locationt{}, ns)
-                   .value_or(nil_exprt{}))
+      bu.source_location().get_function().empty())
+    {
+      clean_init = zero_initializer(bu.op().type(), source_locationt{}, ns)
+                     .value_or(nil_exprt{});
+      if(clean_init->id() != ID_struct || clean_init->has_operands())
+        cleanup_expr(*clean_init);
+    }
+
+    if(clean_init.has_value() && bu.op() == *clean_init)
     {
       const union_typet &union_type = to_union_type(ns.follow(bu.type()));
 
@@ -1521,22 +1528,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 +1582,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 +1595,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 +1640,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,14 +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.type().id()==ID_c_bool)
-    {
-      expr = typecast_exprt(
-        from_integer(
-          expr.is_true() ? 1 : 0, signedbv_typet(config.ansi_c.int_width)),
-        bool_typet());
-    }
 
     const irept &c_sizeof_type=expr.find(ID_C_c_sizeof_type);
 

src/util/expr.cpp

@@ -146,7 +146,9 @@ bool exprt::is_one() const
         CHECK_RETURN(false);
       return rat_value.is_one();
     }
-    else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
+    else if(
+      type_id == ID_unsignedbv || type_id == ID_signedbv ||
+      type_id == ID_c_bool || type_id == ID_c_bit_field)
     {
       const auto width = to_bitvector_type(type()).get_width();
       mp_integer int_value =