Typecheck friend type declarations

This does not yet include typechecking of friend methods. Includes a fix
to permit rvalue conversion to const references, which ensures
unambiguous resolution for member functions.

Author: peterschrammel

regression/systemc/BitvectorSc1/main.cpp

@@ -1,5 +1,3 @@
-#include <cassert>
-
 template <int W>
 class sc_uint {
   public:
@@ -41,8 +39,8 @@ int main(int argc, char** argv)
   x.test1();
   x.test2();
 
-  assert(x.to_uint() == 1);
-  assert(x.to_uint() == 2);
+  __CPROVER_assert(x.to_uint() == 1, "");
+  __CPROVER_assert(x.to_uint() == 2, "");
 
   return 0;
 }

regression/systemc/BitvectorSc2/main.cpp

@@ -1,5 +1,3 @@
-#include <cassert>
-
 template <int W>
 class sc_uint {
   public:
@@ -56,7 +54,7 @@ int main(int argc, char** argv)
   z += y;
 
   sc_uint<10> w(3);
-  assert(z == w);
+  __CPROVER_assert(z == w, "");
 
   return 0;
 }

regression/systemc/BitvectorSc3/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 
 ^EXIT=0$

regression/systemc/EqualOp1/main.cpp

@@ -1,5 +1,3 @@
-#include <cassert>
-
 template<class T>
 class myclass
 {
@@ -20,5 +18,5 @@ int main(int argc, char** argv)
   myclass<int> x(0);
   myclass<int> y(1);
   x = y;
-  assert(x == y);
+  __CPROVER_assert(x == y, "");
 }

regression/systemc/EqualOp2/main.cpp

@@ -1,5 +1,3 @@
-#include <cassert>
-
 template<class T>
 class myclass
 {
@@ -26,5 +24,5 @@ int main(int argc, char** argv)
   myclass<int> y(1);
   //x = y;
   x += 1;
-  assert(x == y);
+  __CPROVER_assert(x == y, "");
 }

regression/systemc/EqualOp3/main.cpp

@@ -1,5 +1,3 @@
-#include <cassert>
-
 template<class T>
 class myclass2;
 
@@ -38,6 +36,6 @@ int main(int argc, char** argv)
   myclass2<int> x(0);
   myclass<int> y(1);
   x = y;
-  assert(x == y);
+  __CPROVER_assert(x == y, "");
   return 0;
 }

regression/systemc/ForwardDecl1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 
 ^EXIT=0$

regression/systemc/FunTempl1/main.cpp

@@ -1,5 +1,3 @@
-#include <cassert>
-
 template<class T>
 T inc(T x)
 {
@@ -15,5 +13,5 @@ int main(int argc, char** argv)
   x = inc<int>(x);
   y = inc<unsigned char>(y);
 
-  assert(x == y);
+  __CPROVER_assert(x == y, "");
 }

regression/systemc/Mult1/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.cpp
-
+--object-bits 10
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/systemc/SimpleSc1/main.cpp

@@ -1,5 +1,3 @@
-#include <cassert>
-
 template <int W>
 class sc_uint {
   public:
@@ -54,7 +52,7 @@ int main(int argc, char** argv)
   z += y;
 
   sc_uint<10> w(3);
-  assert(z == w);
+  __CPROVER_assert(z == w, "");
 
   return 0;
 }

regression/systemc/Template1/main.cpp

@@ -1,5 +1,3 @@
-#include <cassert>
-
 #define DEF_INSIDE
 
 template<class T>
@@ -35,8 +33,8 @@ int main (int argc, char *argv[])
   my_template<int> x;
   x.set(5);
   int y = x.get();
-  assert(y==5);
-  assert(z.get()==3);
+  __CPROVER_assert(y == 5, "");
+  __CPROVER_assert(z.get() == 3, "");
 
   return 0;
 }

regression/systemc/Tuple1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$

regression/systemc/Tuple2/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$

src/cpp/cpp_declarator_converter.cpp

@@ -64,11 +64,22 @@ symbolt &cpp_declarator_convertert::convert(
     cpp_typecheck_resolve.resolve_scope(
       declarator.name(), base_name, template_args);
 
+    cpp_scopet *friend_scope = nullptr;
+
+    if(is_friend)
+    {
+      friend_scope = &cpp_typecheck.cpp_scopes.current_scope();
+      save_scope.restore();
+    }
+
     scope=&cpp_typecheck.cpp_scopes.current_scope();
 
-    // check the declarator-part of the type, in that scope
+    // check the declarator-part of the type, in the current scope
     if(declarator.value().is_nil() || !cpp_typecheck.has_auto(final_type))
       cpp_typecheck.typecheck_type(final_type);
+
+    if(friend_scope)
+      scope = friend_scope;
   }
 
   is_code=is_code_type(final_type);
@@ -80,9 +91,9 @@ symbolt &cpp_declarator_convertert::convert(
   get_final_identifier();
 
   // first see if it is a member
-  if(scope->id_class==cpp_idt::id_classt::CLASS && !is_friend)
+  if(scope->id_class == cpp_idt::id_classt::CLASS)
   {
-    // it's a member! it must be declared already
+    // it's a member! it must be declared already, unless it's a friend
 
     typet &method_qualifier=
       static_cast<typet &>(declarator.method_qualifier());
@@ -118,7 +129,15 @@ symbolt &cpp_declarator_convertert::convert(
 
       // try again
       maybe_symbol=cpp_typecheck.symbol_table.get_writeable(final_identifier);
-      if(!maybe_symbol)
+      if(!maybe_symbol && is_friend)
+      {
+        symbolt &friend_symbol =
+          convert_new_symbol(storage_spec, member_spec, declarator);
+        // mark it as weak so that the full declaration can replace the symbol
+        friend_symbol.is_weak = true;
+        return friend_symbol;
+      }
+      else if(!maybe_symbol)
       {
         cpp_typecheck.error().source_location=
           declarator.name().source_location();
@@ -411,9 +430,7 @@ void cpp_declarator_convertert::get_final_identifier()
     }
   }
 
-  final_identifier=
-    scope->prefix+
-    identifier;
+  final_identifier = scope->prefix + identifier;
 }
 
 symbolt &cpp_declarator_convertert::convert_new_symbol(

src/cpp/cpp_scopes.cpp

@@ -48,7 +48,6 @@ cpp_idt &cpp_scopest::put_into_scope(
   {
     cpp_save_scopet saved_scope(*this);
     go_to(scope);
-    go_to_global_scope();
 
     cpp_idt &id=current_scope().insert(symbol.base_name);
     id.identifier=symbol.name;

src/cpp/cpp_typecheck_compound_type.cpp

@@ -861,13 +861,9 @@ void cpp_typecheckt::typecheck_friend_declaration(
 
   if(declaration.is_template())
   {
-    return; // TODO
-
-#if 0
     error().source_location=declaration.type().source_location();
     error() << "friend template not supported" << eom;
     throw 0;
-#endif
   }
 
   // we distinguish these whether there is a declarator
@@ -890,51 +886,41 @@ void cpp_typecheckt::typecheck_friend_declaration(
       throw 0;
     }
 
-    // typecheck ftype
-
-    // TODO
-    //    typecheck_type(ftype);
-    //    symbol.type.add("ID_C_friends").move_to_sub(ftype);
+    cpp_save_scopet saved_scope(cpp_scopes);
+    cpp_scopes.go_to_global_scope();
+    typecheck_type(ftype);
+    symbol.type.add(ID_C_friends).move_to_sub(ftype);
 
     return;
   }
 
   // It should be a friend function.
   // Do the declarators.
 
+#ifdef DEBUG
+  std::cout << "friend declaration: " << declaration.pretty() << '\n';
+#endif
+
   for(auto &sub_it : declaration.declarators())
   {
-    bool has_value = sub_it.value().is_not_nil();
-
-    if(!has_value)
-    {
-      // If no value is found, then we jump to the
-      // global scope, and we convert the declarator
-      // as if it were declared there
-      cpp_save_scopet saved_scope(cpp_scopes);
-      cpp_scopes.go_to_global_scope();
-      cpp_declarator_convertert cpp_declarator_converter(*this);
-      const symbolt &conv_symb=cpp_declarator_converter.convert(
-          declaration.type(), declaration.storage_spec(),
-          declaration.member_spec(), sub_it);
-      exprt symb_expr=cpp_symbol_expr(conv_symb);
-      symbol.type.add(ID_C_friends).move_to_sub(symb_expr);
-    }
-    else
-    {
-      cpp_declarator_convertert cpp_declarator_converter(*this);
-      cpp_declarator_converter.is_friend=true;
+#ifdef DEBUG
+    std::cout << "decl: " << sub_it.pretty() << "\n with value "
+              << sub_it.value().pretty() << '\n';
+    std::cout << "  scope: " << cpp_scopes.current_scope().prefix << '\n';
+#endif
 
+    if(sub_it.value().is_not_nil())
       declaration.member_spec().set_inline(true);
 
-      const symbolt &conv_symb=cpp_declarator_converter.convert(
-        declaration.type(), declaration.storage_spec(),
-        declaration.member_spec(), sub_it);
-
-      exprt symb_expr=cpp_symbol_expr(conv_symb);
-
-      symbol.type.add(ID_C_friends).move_to_sub(symb_expr);
-    }
+    cpp_declarator_convertert cpp_declarator_converter(*this);
+    cpp_declarator_converter.is_friend = true;
+    const symbolt &conv_symb = cpp_declarator_converter.convert(
+      declaration.type(),
+      declaration.storage_spec(),
+      declaration.member_spec(),
+      sub_it);
+    exprt symb_expr = cpp_symbol_expr(conv_symb);
+    symbol.type.add(ID_C_friends).move_to_sub(symb_expr);
   }
 }
 
@@ -1322,7 +1308,13 @@ void cpp_typecheckt::typecheck_member_function(
   // move early, it must be visible before doing any value
   symbolt *new_symbol;
 
-  if(symbol_table.move(symbol, new_symbol))
+  const bool symbol_exists = symbol_table.move(symbol, new_symbol);
+  if(symbol_exists && new_symbol->is_weak)
+  {
+    // there might have been an earlier friend declaration
+    *new_symbol = std::move(symbol);
+  }
+  else if(symbol_exists)
   {
     error().source_location=symbol.location;
     error() << "failed to insert new method symbol: " << symbol.name << '\n'

src/cpp/cpp_typecheck_conversions.cpp

@@ -1251,10 +1251,21 @@ bool cpp_typecheckt::reference_binding(
       return false;
   }
 
-  if(expr.get_bool(ID_C_lvalue))
+  if(expr.get_bool(ID_C_lvalue) || type.subtype().get_bool(ID_C_constant))
   {
     if(reference_compatible(expr, type, rank))
     {
+      if(!expr.get_bool(ID_C_lvalue))
+      {
+        // create temporary object
+        side_effect_exprt tmp{ID_temporary_object,
+                              {std::move(expr)},
+                              type.subtype(),
+                              expr.source_location()};
+        tmp.set(ID_mode, ID_cpp);
+        expr.swap(tmp);
+      }
+
       {
         address_of_exprt tmp(expr, reference_type(expr.type()));
         tmp.add_source_location()=expr.source_location();

src/cpp/cpp_typecheck_expr.cpp

@@ -1175,11 +1175,9 @@ void cpp_typecheckt::typecheck_expr_member(
         if(pcomp.is_nil())
         {
           error().source_location=expr.find_source_location();
-          error() << "error: `"
-                  << symbol_expr.get(ID_identifier)
+          error() << "error: `" << symbol_expr.get(ID_identifier)
                   << "' is not static member "
-                  << "of class `" << to_string(type) << "'"
-                  << eom;
+                  << "of class `" << to_string(op0.type()) << "'" << eom;
           throw 0;
         }
       }