C++ front-end: Remove internal symbols before linking

This mirrors what the C front-end already does, but requires changes to
constant propagation in the C++ front-end: we previously used macros,
which serve a very different purpose otherwise.

Fixes: #1490

Author: tautschnig

regression/goto-cc-cbmc/chain.sh

@@ -6,13 +6,14 @@ is_windows=$3
 
 options=${*:4:$#-4}
 name=${*:$#}
-name=${name%.c}
+base_name=${name%.c}
+base_name=${base_name%.cpp}
 
 if [[ "${is_windows}" == "true" ]]; then
-  "${goto_cc}" "${name}.c"
-  mv "${name}.exe" "${name}.gb"
+  "${goto_cc}" "${name}"
+  mv "${base_name}.exe" "${base_name}.gb"
 else
-  "${goto_cc}" "${name}.c" -o "${name}.gb"
+  "${goto_cc}" "${name}" -o "${base_name}.gb"
 fi
 
-"${cbmc}" "${name}.gb" ${options}
+"${cbmc}" "${base_name}.gb" ${options}

regression/goto-cc-cbmc/cpp/main.cpp

@@ -0,0 +1,4 @@
+int main()
+{
+  return 0;
+}

regression/goto-cc-cbmc/cpp/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/cpp/cpp_declarator_converter.cpp

@@ -460,11 +460,6 @@ symbolt &cpp_declarator_convertert::convert_new_symbol(
   symbol.is_macro=is_typedef && !is_template_parameter;
   symbol.pretty_name=pretty_name;
 
-  // Constant? These are propagated.
-  if(symbol.type.get_bool(ID_C_constant) &&
-     symbol.value.is_not_nil())
-    symbol.is_macro=true;
-
   if(is_code && !symbol.is_type)
   {
     // it is a function

src/cpp/cpp_instantiate_template.cpp

@@ -54,6 +54,16 @@ std::string cpp_typecheckt::template_suffix(
     else // expression
     {
       exprt e=expr;
+
+      if(e.id() == ID_symbol)
+      {
+        const symbol_exprt &s = to_symbol_expr(e);
+        const symbolt &symbol = lookup(s.get_identifier());
+
+        if(cpp_is_pod(symbol.type) && symbol.type.get_bool(ID_C_constant))
+          e = symbol.value;
+      }
+
       make_constant(e);
 
       // this must be a constant, which includes true/false

src/cpp/cpp_language.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/get_base_name.h>
 
 #include <linking/linking.h>
+#include <linking/remove_internal_symbols.h>
 
 #include <ansi-c/ansi_c_entry_point.h>
 #include <ansi-c/c_preprocess.h>
@@ -132,6 +133,8 @@ bool cpp_languaget::typecheck(
       cpp_parse_tree, new_symbol_table, module, get_message_handler()))
     return true;
 
+  remove_internal_symbols(new_symbol_table, get_message_handler(), false);
+
   return linking(symbol_table, new_symbol_table, get_message_handler());
 }
 

src/cpp/cpp_typecheck_compound_type.cpp

@@ -733,13 +733,6 @@ void cpp_typecheckt::typecheck_compound_declarator(
       {
         new_symbol->value.swap(value);
         c_typecheck_baset::do_initializer(*new_symbol);
-
-        // these are macros if they are PODs and come with a (constant) value
-        if(new_symbol->type.get_bool(ID_C_constant))
-        {
-          simplify(new_symbol->value, *this);
-          new_symbol->is_macro=true;
-        }
       }
       else
       {
@@ -771,7 +764,18 @@ void cpp_typecheckt::check_fixed_size_array(typet &type)
     array_typet &array_type=to_array_type(type);
 
     if(array_type.size().is_not_nil())
+    {
+      if(array_type.size().id() == ID_symbol)
+      {
+        const symbol_exprt &s = to_symbol_expr(array_type.size());
+        const symbolt &symbol = lookup(s.get_identifier());
+
+        if(cpp_is_pod(symbol.type) && symbol.type.get_bool(ID_C_constant))
+          array_type.size() = symbol.value;
+      }
+
       make_constant_index(array_type.size());
+    }
 
     // recursive call for multi-dimensional arrays
     check_fixed_size_array(array_type.subtype());

src/cpp/cpp_typecheck_enum_type.cpp

@@ -63,6 +63,8 @@ void cpp_typecheckt::typecheck_enum_body(symbolt &enum_symbol)
     symbol.type=enum_tag_type;
     symbol.is_type=false;
     symbol.is_macro=true;
+    symbol.is_file_local = true;
+    symbol.is_thread_local = true;
 
     symbolt *new_symbol;
     if(symbol_table.move(symbol, new_symbol))

src/cpp/cpp_typecheck_resolve.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/mathematical_types.h>
 #include <util/prefix.h>
+#include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 #include <util/string_constant.h>
@@ -1046,6 +1047,26 @@ struct_tag_typet cpp_typecheck_resolvet::disambiguate_template_classes(
         source_location,
         primary_template_symbol,
         full_template_args);
+
+    for(auto &arg : full_template_args_tc.arguments())
+    {
+      if(arg.id() == ID_type)
+        continue;
+      if(arg.id() == ID_symbol)
+      {
+        const symbol_exprt &s = to_symbol_expr(arg);
+        const symbolt &symbol = cpp_typecheck.lookup(s.get_identifier());
+
+        if(
+          cpp_typecheck.cpp_is_pod(symbol.type) &&
+          symbol.type.get_bool(ID_C_constant))
+        {
+          arg = symbol.value;
+        }
+      }
+      simplify(arg, cpp_typecheck);
+    }
+
     // go back to where we used to be
   }
 

src/linking/remove_internal_symbols.cpp

@@ -95,6 +95,12 @@ void remove_internal_symbols(
   special.insert(CPROVER_PREFIX "deallocated");
   special.insert(CPROVER_PREFIX "dead_object");
   special.insert(CPROVER_PREFIX "rounding_mode");
+  special.insert("__new");
+  special.insert("__new_array");
+  special.insert("__placement_new");
+  special.insert("__placement_new_array");
+  special.insert("__delete");
+  special.insert("__delete_array");
 
   for(symbol_tablet::symbolst::const_iterator
       it=symbol_table.symbols.begin();
@@ -139,8 +145,9 @@ void remove_internal_symbols(
     {
       // body? not local (i.e., "static")?
       if(
-        has_body && (!is_file_local || (config.main.has_value() &&
-                                        symbol.name == config.main.value())))
+        has_body &&
+        (!is_file_local ||
+         (config.main.has_value() && symbol.base_name == config.main.value())))
       {
         get_symbols(ns, symbol, exported);
       }