C++ destructors: Ensure "this" is a fully qualified name

Typechecking does not magically expand `ID_this`, and there isn't
sufficient context to use "cpp-this."

Fixes: #661

Author: tautschnig

regression/cbmc-cpp/cpp1/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.cpp
-
+--unwind 1 --unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

src/cpp/cpp_typecheck.h

@@ -257,7 +257,7 @@ class cpp_typecheckt:public c_typecheck_baset
 
   void default_dtor(const symbolt &symb, cpp_declarationt &dtor);
 
-  codet dtor(const symbolt &symb);
+  codet dtor(const symbolt &symb, const symbol_exprt &this_expr);
 
   void check_member_initializers(
     const struct_typet::basest &bases,

src/cpp/cpp_typecheck_destructor.cpp

@@ -47,7 +47,7 @@ void cpp_typecheckt::default_dtor(
 }
 
 /// produces destructor code for a class object
-codet cpp_typecheckt::dtor(const symbolt &symbol)
+codet cpp_typecheckt::dtor(const symbolt &symbol, const symbol_exprt &this_expr)
 {
   assert(symbol.type.id()==ID_struct ||
          symbol.type.id()==ID_union);
@@ -85,7 +85,7 @@ codet cpp_typecheckt::dtor(const symbolt &symbol)
 
       exprt ptrmember(ID_ptrmember);
       ptrmember.set(ID_component_name, c.get_name());
-      ptrmember.operands().push_back(exprt("cpp-this"));
+      ptrmember.operands().push_back(this_expr);
 
       code_assignt assign(ptrmember, address);
       block.add(assign);
@@ -113,8 +113,7 @@ codet cpp_typecheckt::dtor(const symbolt &symbol)
 
     exprt member(ID_ptrmember, type);
     member.set(ID_component_cpp_name, cppname);
-    member.operands().push_back(
-      symbol_exprt(ID_this, pointer_type(symbol.type)));
+    member.operands().push_back(this_expr);
     member.add_source_location() = source_location;
 
     const bool disabled_access_control = disable_access_control;
@@ -139,8 +138,7 @@ codet cpp_typecheckt::dtor(const symbolt &symbol)
     DATA_INVARIANT(bit->id() == ID_base, "base class expression expected");
     const symbolt &psymb = lookup(bit->type());
 
-    symbol_exprt this_ptr(ID_this, pointer_type(symbol.type));
-    dereference_exprt object(this_ptr, psymb.type);
+    dereference_exprt object{this_expr, psymb.type};
     object.add_source_location() = source_location;
 
     const bool disabled_access_control = disable_access_control;

src/cpp/cpp_typecheck_function.cpp

@@ -90,22 +90,6 @@ void cpp_typecheckt::convert_function(symbolt &symbol)
   if(symbol.value.is_nil())
     return;
 
-  // if it is a destructor, add the implicit code
-  if(to_code_type(symbol.type).return_type().id() == ID_destructor)
-  {
-    const symbolt &msymb=lookup(symbol.type.get(ID_C_member_name));
-
-    assert(symbol.value.id()==ID_code);
-    assert(symbol.value.get(ID_statement)==ID_block);
-
-    if(
-      !symbol.value.has_operands() || !symbol.value.op0().has_operands() ||
-      symbol.value.op0().op0().id() != ID_already_typechecked)
-    {
-      symbol.value.copy_to_operands(dtor(msymb));
-    }
-  }
-
   // enter appropriate scope
   cpp_save_scopet saved_scope(cpp_scopes);
   cpp_scopet &function_scope=cpp_scopes.set_scope(symbol.name);
@@ -123,13 +107,29 @@ void cpp_typecheckt::convert_function(symbolt &symbol)
     code_typet::parameterst &parameters=function_type.parameters();
     assert(parameters.size()>=1);
     code_typet::parametert &this_parameter_expr=parameters.front();
-    function_scope.this_expr=exprt(ID_symbol, this_parameter_expr.type());
-    function_scope.this_expr.set(
-      ID_identifier, this_parameter_expr.get_identifier());
+    function_scope.this_expr = symbol_exprt{
+      this_parameter_expr.get_identifier(), this_parameter_expr.type()};
   }
   else
     function_scope.this_expr.make_nil();
 
+  // if it is a destructor, add the implicit code
+  if(to_code_type(symbol.type).return_type().id() == ID_destructor)
+  {
+    const symbolt &msymb = lookup(symbol.type.get(ID_C_member_name));
+
+    assert(symbol.value.id() == ID_code);
+    assert(symbol.value.get(ID_statement) == ID_block);
+
+    if(
+      !symbol.value.has_operands() || !symbol.value.op0().has_operands() ||
+      symbol.value.op0().op0().id() != ID_already_typechecked)
+    {
+      symbol.value.copy_to_operands(
+        dtor(msymb, to_symbol_expr(function_scope.this_expr)));
+    }
+  }
+
   // do the function body
   start_typecheck_code();