C++ function disambiguation and template scope cleanup [blocks: #1260]

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_id.h

@@ -70,6 +70,11 @@ class cpp_idt
     return id_class==id_classt::TYPEDEF;
   }
 
+  bool is_template_scope() const
+  {
+    return id_class == id_classt::TEMPLATE_SCOPE;
+  }
+
   irep_idt identifier, base_name;
 
   // if it is a member or method, what class is it in?

src/cpp/cpp_instantiate_template.cpp

@@ -103,6 +103,40 @@ void cpp_typecheckt::show_instantiation_stack(std::ostream &out)
   }
 }
 
+/// Set up a scope as subscope of the template scope
+cpp_scopet &cpp_typecheckt::sub_scope_for_instantiation(
+  cpp_scopet &template_scope,
+  const std::string &suffix)
+{
+  cpp_scopet::id_sett id_set =
+    template_scope.lookup(suffix, cpp_scopet::SCOPE_ONLY);
+
+  CHECK_RETURN(id_set.size() <= 1);
+
+  if(id_set.size() == 1)
+  {
+    cpp_idt &cpp_id = **id_set.begin();
+    CHECK_RETURN(cpp_id.is_template_scope());
+
+    return static_cast<cpp_scopet &>(cpp_id);
+  }
+  else
+  {
+    cpp_scopet &sub_scope = template_scope.new_scope(suffix);
+    sub_scope.id_class = cpp_idt::id_classt::TEMPLATE_SCOPE;
+    sub_scope.prefix = template_scope.get_parent().prefix;
+    sub_scope.suffix = suffix;
+    sub_scope.add_using_scope(template_scope.get_parent());
+
+    const std::string subscope_name =
+      id2string(template_scope.identifier) + suffix;
+    cpp_scopes.id_map.insert(
+      cpp_scopest::id_mapt::value_type(subscope_name, &sub_scope));
+
+    return sub_scope;
+  }
+}
+
 const symbolt &cpp_typecheckt::class_template_symbol(
   const source_locationt &source_location,
   const symbolt &template_symbol,
@@ -131,10 +165,9 @@ const symbolt &cpp_typecheckt::class_template_symbol(
   INVARIANT_STRUCTURED(
     template_scope!=nullptr, nullptr_exceptiont, "template_scope is null");
 
-  irep_idt identifier=
-    id2string(template_scope->prefix)+
-    "tag-"+id2string(template_symbol.base_name)+
-    id2string(suffix);
+  irep_idt identifier = id2string(template_scope->get_parent().prefix) +
+                        "tag-" + id2string(template_symbol.base_name) +
+                        id2string(suffix);
 
   // already there?
   symbol_tablet::symbolst::const_iterator s_it=
@@ -171,9 +204,8 @@ const symbolt &cpp_typecheckt::class_template_symbol(
 
   id.id_class=cpp_idt::id_classt::CLASS;
   id.is_scope=true;
-  id.prefix=template_scope->prefix+
-            id2string(s_ptr->base_name)+
-            id2string(suffix)+"::";
+  id.prefix = template_scope->get_parent().prefix +
+              id2string(s_ptr->base_name) + id2string(suffix) + "::";
   id.class_identifier=s_ptr->name;
   id.id_class=cpp_idt::id_classt::CLASS;
 
@@ -318,18 +350,12 @@ const symbolt &cpp_typecheckt::instantiate_template(
     class_name=cpp_scopes.current_scope().get_parent().identifier;
 
   // sub-scope for fixing the prefix
-  std::string subscope_name=id2string(template_scope->identifier)+suffix;
+  cpp_scopet &sub_scope = sub_scope_for_instantiation(*template_scope, suffix);
 
   // let's see if we have the instance already
-  cpp_scopest::id_mapt::iterator scope_it=
-    cpp_scopes.id_map.find(subscope_name);
-
-  if(scope_it!=cpp_scopes.id_map.end())
   {
-    cpp_scopet &scope=cpp_scopes.get_scope(subscope_name);
-
-    const auto id_set =
-      scope.lookup(template_symbol.base_name, cpp_scopet::SCOPE_ONLY);
+    cpp_scopet::id_sett id_set =
+      sub_scope.lookup(template_symbol.base_name, cpp_scopet::SCOPE_ONLY);
 
     if(id_set.size()==1)
     {
@@ -349,20 +375,7 @@ const symbolt &cpp_typecheckt::instantiate_template(
         return symb;
     }
 
-    cpp_scopes.go_to(scope);
-  }
-  else
-  {
-    // set up a scope as subscope of the template scope
-    cpp_scopet &sub_scope=
-      cpp_scopes.current_scope().new_scope(subscope_name);
-    sub_scope.id_class=cpp_idt::id_classt::TEMPLATE_SCOPE;
-    sub_scope.prefix=template_scope->get_parent().prefix;
-    sub_scope.suffix=suffix;
-    sub_scope.add_using_scope(template_scope->get_parent());
     cpp_scopes.go_to(sub_scope);
-    cpp_scopes.id_map.insert(
-      cpp_scopest::id_mapt::value_type(subscope_name, &sub_scope));
   }
 
   // store the information that the template has

src/cpp/cpp_scope.h

@@ -85,11 +85,6 @@ class cpp_scopet:public cpp_idt
            id_class==id_classt::NAMESPACE;
   }
 
-  bool is_template_scope() const
-  {
-    return id_class==id_classt::TEMPLATE_SCOPE;
-  }
-
   cpp_scopet &get_parent() const
   {
     return static_cast<cpp_scopet &>(cpp_idt::get_parent());

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.h

@@ -230,6 +230,10 @@ class cpp_typecheckt:public c_typecheck_baset
   std::string template_suffix(
     const cpp_template_args_tct &template_args);
 
+  cpp_scopet &sub_scope_for_instantiation(
+    cpp_scopet &template_scope,
+    const std::string &suffix);
+
   void
   convert_parameters(const irep_idt &current_mode, code_typet &function_type);