C++ front-end: put "this" parameter in the symbol table

The "this" parameter must carry a unique name for each class and must be
stored in the symbol table. And indeed make sure that all parameters are
in the symbol table, unless the method a member of a class template and
is never used, in which case the method symbol must be removed.
Previously we mostly did this removal, but would fail for methods with a
body not involving any symbols (as we tested for the existence of some
cpp_name).

Author: tautschnig

src/cpp/cpp_declarator_converter.cpp

@@ -104,10 +104,15 @@ symbolt &cpp_declarator_convertert::convert(
     {
       // adjust type if it's a non-static member function
       if(final_type.id()==ID_code)
+      {
+        cpp_save_scopet save_scope(cpp_typecheck.cpp_scopes);
+        cpp_typecheck.cpp_scopes.go_to(*scope);
+
         cpp_typecheck.add_this_to_method_type(
           cpp_typecheck.lookup(scope->identifier),
           to_code_type(final_type),
           method_qualifier);
+      }
 
       get_final_identifier();
 

src/cpp/cpp_typecheck.cpp

@@ -54,10 +54,10 @@ void cpp_typecheckt::typecheck()
   for(auto &item : cpp_parse_tree.items)
     convert(item);
 
-  typecheck_method_bodies();
-
   static_and_dynamic_initialization();
 
+  typecheck_method_bodies();
+
   do_not_typechecked();
 
   clean_up();
@@ -276,13 +276,10 @@ void cpp_typecheckt::clean_up()
 
     const symbolt &symbol=cur_it->second;
 
-    // erase templates
-    if(symbol.type.get_bool(ID_is_template) ||
-       // Remove all symbols that have not been converted.
-       //   In particular this includes symbols created for functions
-       //   during template instantiation that are never called,
-       //   and hence, their bodies have not been converted.
-       contains_cpp_name(symbol.value))
+    // erase templates and all member functions that have not been converted
+    if(
+      symbol.type.get_bool(ID_is_template) ||
+      deferred_typechecking.find(symbol.name) != deferred_typechecking.end())
     {
       symbol_table.erase(cur_it);
       continue;

src/cpp/cpp_typecheck.h

@@ -12,10 +12,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #ifndef CPROVER_CPP_CPP_TYPECHECK_H
 #define CPROVER_CPP_CPP_TYPECHECK_H
 
-#include <cassert>
-#include <set>
 #include <list>
 #include <map>
+#include <set>
+#include <unordered_set>
 
 #include <util/std_code.h>
 #include <util/std_types.h>
@@ -588,6 +588,7 @@ class cpp_typecheckt:public c_typecheck_baset
   typedef std::list<irep_idt> dynamic_initializationst;
   dynamic_initializationst dynamic_initializations;
   bool disable_access_control;           // Disable protect and private
+  std::unordered_set<irep_idt> deferred_typechecking;
 };
 
 #endif // CPROVER_CPP_CPP_TYPECHECK_H

src/cpp/cpp_typecheck_compound_type.cpp

@@ -1335,8 +1335,7 @@ void cpp_typecheckt::typecheck_member_function(
   // Is this in a class template?
   // If so, we defer typechecking until used.
   if(cpp_scopes.current_scope().get_parent().is_template_scope())
-  {
-  }
+    deferred_typechecking.insert(new_symbol->name);
   else // remember for later typechecking of body
     add_method_body(new_symbol);
 }
@@ -1360,9 +1359,11 @@ void cpp_typecheckt::add_this_to_method_type(
     subtype.set(ID_C_volatile, true);
 
   code_typet::parametert parameter(pointer_type(subtype));
-  parameter.set_identifier(ID_this); // check? Not qualified
+  parameter.set_identifier(ID_this);
   parameter.set_base_name(ID_this);
   parameter.set_this();
+  if(!cpp_scopes.current_scope().get_parent().is_template_scope())
+    convert_parameter(compound_symbol.mode, parameter);
 
   code_typet::parameterst &parameters = type.parameters();
   parameters.insert(parameters.begin(), parameter);

src/cpp/cpp_typecheck_function.cpp

@@ -31,6 +31,7 @@ void cpp_typecheckt::convert_parameter(
     parameter.set_base_name(base_name);
   }
 
+  PRECONDITION(!cpp_scopes.current_scope().prefix.empty());
   irep_idt identifier=cpp_scopes.current_scope().prefix+
                       id2string(base_name);
 
@@ -147,6 +148,8 @@ void cpp_typecheckt::convert_function(symbolt &symbol)
   symbol.value.type()=symbol.type;
 
   return_type = old_return_type;
+
+  deferred_typechecking.erase(symbol.name);
 }
 
 /// for function overloading
@@ -171,8 +174,7 @@ irep_idt cpp_typecheckt::function_identifier(const typet &type)
   code_typet::parameterst::const_iterator it=
     parameters.begin();
 
-  if(it!=parameters.end() &&
-     it->get_identifier()==ID_this)
+  if(it != parameters.end() && it->get_base_name() == ID_this)
   {
     const typet &pointer=it->type();
     const typet &symbol =pointer.subtype();