From 02e38408e1e6c4f3501a9c59bcaec0021238d0cf Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 31 Jul 2017 17:54:11 +0200 Subject: [PATCH] Fix delayed method body conversion for templates Do not add method body on declaration - they are handled upon use. --- regression/cpp/Function_Overloading2/main.cpp | 12 +++- .../cpp/Function_Overloading2/test.desc | 2 +- .../cpp/Template_Instantiation5/test.desc | 2 +- regression/systemc/BitvectorSc1/test.desc | 2 +- regression/systemc/BitvectorSc2/test.desc | 2 +- regression/systemc/EqualOp1/test.desc | 2 +- regression/systemc/EqualOp2/test.desc | 2 +- regression/systemc/EqualOp3/test.desc | 2 +- regression/systemc/FunTempl1/test.desc | 2 +- regression/systemc/SimpleSc1/test.desc | 2 +- regression/systemc/Template1/test.desc | 2 +- src/cpp/cpp_declarator_converter.cpp | 3 - src/cpp/cpp_instantiate_template.cpp | 39 ++++++++++--- src/cpp/cpp_typecheck.cpp | 2 + src/cpp/cpp_typecheck.h | 9 +-- src/cpp/cpp_typecheck_compound_type.cpp | 6 +- src/cpp/cpp_typecheck_declaration.cpp | 13 ++--- src/cpp/cpp_typecheck_expr.cpp | 24 +++++++- src/cpp/cpp_typecheck_method_bodies.cpp | 49 ++++++++++++++-- src/cpp/cpp_typecheck_resolve.cpp | 57 +++++++++++++++---- src/cpp/cpp_typecheck_resolve.h | 5 ++ 21 files changed, 182 insertions(+), 57 deletions(-) diff --git a/regression/cpp/Function_Overloading2/main.cpp b/regression/cpp/Function_Overloading2/main.cpp index 06204bf75ed..ff0f216b453 100644 --- a/regression/cpp/Function_Overloading2/main.cpp +++ b/regression/cpp/Function_Overloading2/main.cpp @@ -1,10 +1,16 @@ +#ifdef __GNUC__ +#define NOTHROW __attribute__((nothrow)) +#else +#define NOTHROW +#endif + namespace std { extern "C" { - double fabs(double) __attribute__((nothrow)) ; + double fabs(double) NOTHROW ; } - __inline float fabs(float x) __attribute__((nothrow)); - __inline long double fabs(long double x) __attribute__((nothrow)); + __inline float fabs(float x) NOTHROW; + __inline long double fabs(long double x) NOTHROW; /* original code from CodeWarrior */ template diff --git a/regression/cpp/Function_Overloading2/test.desc b/regression/cpp/Function_Overloading2/test.desc index 5893356edf6..a003b07b93c 100644 --- a/regression/cpp/Function_Overloading2/test.desc +++ b/regression/cpp/Function_Overloading2/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.cpp ^EXIT=0$ diff --git a/regression/cpp/Template_Instantiation5/test.desc b/regression/cpp/Template_Instantiation5/test.desc index 5893356edf6..a003b07b93c 100644 --- a/regression/cpp/Template_Instantiation5/test.desc +++ b/regression/cpp/Template_Instantiation5/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.cpp ^EXIT=0$ diff --git a/regression/systemc/BitvectorSc1/test.desc b/regression/systemc/BitvectorSc1/test.desc index 65a2556e7e0..e778f120e58 100644 --- a/regression/systemc/BitvectorSc1/test.desc +++ b/regression/systemc/BitvectorSc1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.cpp ^EXIT=10$ diff --git a/regression/systemc/BitvectorSc2/test.desc b/regression/systemc/BitvectorSc2/test.desc index 6666d172f47..91d9cf8b52e 100644 --- a/regression/systemc/BitvectorSc2/test.desc +++ b/regression/systemc/BitvectorSc2/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.cpp ^EXIT=0$ diff --git a/regression/systemc/EqualOp1/test.desc b/regression/systemc/EqualOp1/test.desc index 6666d172f47..91d9cf8b52e 100644 --- a/regression/systemc/EqualOp1/test.desc +++ b/regression/systemc/EqualOp1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.cpp ^EXIT=0$ diff --git a/regression/systemc/EqualOp2/test.desc b/regression/systemc/EqualOp2/test.desc index 65a2556e7e0..e778f120e58 100644 --- a/regression/systemc/EqualOp2/test.desc +++ b/regression/systemc/EqualOp2/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.cpp ^EXIT=10$ diff --git a/regression/systemc/EqualOp3/test.desc b/regression/systemc/EqualOp3/test.desc index 65a2556e7e0..e778f120e58 100644 --- a/regression/systemc/EqualOp3/test.desc +++ b/regression/systemc/EqualOp3/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.cpp ^EXIT=10$ diff --git a/regression/systemc/FunTempl1/test.desc b/regression/systemc/FunTempl1/test.desc index 6666d172f47..91d9cf8b52e 100644 --- a/regression/systemc/FunTempl1/test.desc +++ b/regression/systemc/FunTempl1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.cpp ^EXIT=0$ diff --git a/regression/systemc/SimpleSc1/test.desc b/regression/systemc/SimpleSc1/test.desc index 6666d172f47..91d9cf8b52e 100644 --- a/regression/systemc/SimpleSc1/test.desc +++ b/regression/systemc/SimpleSc1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.cpp ^EXIT=0$ diff --git a/regression/systemc/Template1/test.desc b/regression/systemc/Template1/test.desc index 6666d172f47..91d9cf8b52e 100644 --- a/regression/systemc/Template1/test.desc +++ b/regression/systemc/Template1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.cpp ^EXIT=0$ diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp index da13cea78d4..df74fa22206 100644 --- a/src/cpp/cpp_declarator_converter.cpp +++ b/src/cpp/cpp_declarator_converter.cpp @@ -346,9 +346,6 @@ void cpp_declarator_convertert::handle_initializer( // no initial value yet symbol.value.swap(value); - if(is_code && declarator.type().id()!=ID_template) - cpp_typecheck.add_method_body(&symbol); - if(!is_code) cpp_typecheck.convert_initializer(symbol); } diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp index 896986cf869..b47a864814e 100644 --- a/src/cpp/cpp_instantiate_template.cpp +++ b/src/cpp/cpp_instantiate_template.cpp @@ -11,6 +11,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_typecheck.h" +#ifdef DEBUG +#include +#endif + #include #include #include @@ -220,6 +224,10 @@ const symbolt &cpp_typecheckt::instantiate_template( const cpp_template_args_tct &full_template_args, const typet &specialization) { +#ifdef DEBUG + std::cout << "instantiate_template: " << template_symbol.name << '\n'; +#endif + if(instantiation_stack.size()==MAX_DEPTH) { error().source_location=source_location; @@ -233,10 +241,10 @@ const symbolt &cpp_typecheckt::instantiate_template( instantiation_stack.back().identifier=template_symbol.name; instantiation_stack.back().full_template_args=full_template_args; - #if 0 +#ifdef DEBUG std::cout << "L: " << source_location << '\n'; std::cout << "I: " << template_symbol.name << '\n'; - #endif +#endif cpp_saved_template_mapt saved_map(template_map); @@ -246,7 +254,7 @@ const symbolt &cpp_typecheckt::instantiate_template( assert(!specialization_template_args.has_unassigned()); assert(!full_template_args.has_unassigned()); - #if 0 +#ifdef DEBUG std::cout << "A: <"; forall_expr(it, specialization_template_args.arguments()) { @@ -257,8 +265,8 @@ const symbolt &cpp_typecheckt::instantiate_template( else std::cout << to_string(*it); } - std::cout << ">\n"; - #endif + std::cout << ">\n\n"; +#endif // do we have arguments? if(full_template_args.arguments().empty()) @@ -373,8 +381,8 @@ const symbolt &cpp_typecheckt::instantiate_template( instantiated_with.get_sub().push_back(specialization_template_args); } - #if 0 - std::cout << "MAP:\n"; + #ifdef DEBUG + std::cout << "CLASS MAP:\n"; template_map.print(std::cout); #endif @@ -432,6 +440,10 @@ const symbolt &cpp_typecheckt::instantiate_template( // mapping from template arguments to values/types template_map.build(method_type, specialization_template_args); +#ifdef DEBUG + std::cout << "METHOD MAP:\n"; + template_map.print(std::cout); +#endif method_decl.remove(ID_template_type); method_decl.remove(ID_is_template); @@ -439,7 +451,18 @@ const symbolt &cpp_typecheckt::instantiate_template( convert(method_decl); } - const symbolt &new_symb = lookup(new_decl.type().get(ID_identifier)); + const irep_idt& new_symb_id = new_decl.type().get(ID_identifier); + symbolt &new_symb = symbol_table.get_writeable_ref(new_symb_id); + + // add template arguments to type in order to retrieve template map when + // typechecking function body + new_symb.type.set(ID_C_template, template_type); + new_symb.type.set(ID_C_template_arguments, specialization_template_args); + +#ifdef DEBUG + std::cout << "instance symbol: " << new_symb.name << "\n\n"; + std::cout << "template type: " << template_type.pretty() << "\n\n"; +#endif return new_symb; } diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index 8b3c64cebc3..fb08185b76b 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -54,6 +54,8 @@ void cpp_typecheckt::typecheck() for(auto &item : cpp_parse_tree.items) convert(item); + typecheck_method_bodies(); + static_and_dynamic_initialization(); do_not_typechecked(); diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h index e7a74aed1ff..51580d79a1a 100644 --- a/src/cpp/cpp_typecheck.h +++ b/src/cpp/cpp_typecheck.h @@ -338,13 +338,10 @@ class cpp_typecheckt:public c_typecheck_baset }; typedef std::list method_bodiest; + std::set methods_seen; method_bodiest method_bodies; - void add_method_body(symbolt *_method_symbol) - { - method_bodies.push_back(method_bodyt( - _method_symbol, template_map, instantiation_stack)); - } + void add_method_body(symbolt *_method_symbol); bool builtin_factory(const irep_idt &); @@ -384,7 +381,7 @@ class cpp_typecheckt:public c_typecheck_baset void typecheck_compound_body(symbolt &symbol); void typecheck_compound_body(struct_union_typet &type) { UNREACHABLE; } void typecheck_enum_body(symbolt &symbol); - void typecheck_method_bodies(method_bodiest &); + void typecheck_method_bodies(); void typecheck_compound_bases(struct_typet &type); void add_anonymous_members_to_scope(const symbolt &struct_union_symbol); diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 45b0d3be30b..e59a8b9421c 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -11,6 +11,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_typecheck.h" +#ifdef DEBUG +#include +#endif + #include #include @@ -395,7 +399,7 @@ void cpp_typecheckt::typecheck_compound_declarator( irep_idt identifier; // the below is a temporary hack - // if(is_method || is_static)d + // if(is_method || is_static) if(id2string(cpp_scopes.current_scope().prefix).find("#anon")== std::string::npos || is_method || is_static) diff --git a/src/cpp/cpp_typecheck_declaration.cpp b/src/cpp/cpp_typecheck_declaration.cpp index a2c1487585d..f6033d91f63 100644 --- a/src/cpp/cpp_typecheck_declaration.cpp +++ b/src/cpp/cpp_typecheck_declaration.cpp @@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu \********************************************************************/ + /// \file /// C++ Language Type Checking @@ -19,21 +20,15 @@ void cpp_typecheckt::convert(cpp_declarationt &declaration) if(declaration.is_empty()) return; - // Record the function bodies so we can check them later. - // This function is used recursively, so we save them. - method_bodiest old_method_bodies; - old_method_bodies.swap(method_bodies); + // The function bodies must not be checked here, + // but only at the very end when all declarations have been + // processed (or considering forward declarations at least) // templates are done in a dedicated function if(declaration.is_template()) convert_template_declaration(declaration); else convert_non_template_declaration(declaration); - - method_bodiest b; - b.swap(method_bodies); - typecheck_method_bodies(b); - method_bodies.swap(old_method_bodies); } void cpp_typecheckt::convert_anonymous_union( diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index 501baeeeb22..9153c0fd4c0 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -432,6 +432,7 @@ bool cpp_typecheckt::overloadable(const exprt &expr) t=t.subtype(); if(t.id()==ID_struct || + t.id() == ID_incomplete_struct || t.id()==ID_union || t.id()==ID_c_enum || t.id() == ID_c_enum_tag) return true; @@ -602,6 +603,7 @@ bool cpp_typecheckt::operator_is_overloaded(exprt &expr) // We try and fail silently, maybe conversions will work // instead. + // TODO: need to resolve an incomplete struct (template) here // go into scope of first operand if(expr.op0().type().id()==ID_symbol && follow(expr.op0().type()).id()==ID_struct) @@ -2380,7 +2382,27 @@ void cpp_typecheckt::typecheck_method_application( member_expr.swap(expr.function()); const symbolt &symbol=lookup(member_expr.get(ID_component_name)); - add_method_body(&symbol_table.get_writeable_ref(symbol.name)); + symbolt &method_symbol=symbol_table.get_writeable_ref(symbol.name); + const symbolt &tag_symbol=lookup(symbol.type.get("#member_name")); + + // build the right template map + // if this is an instantiated template class method + if(tag_symbol.type.find(ID_C_template)!=irept()) + { + cpp_saved_template_mapt saved_map(template_map); + const irept &template_type = tag_symbol.type.find(ID_C_template); + const irept &template_args = tag_symbol.type.find(ID_C_template_arguments); + template_map.build( + static_cast(template_type), + static_cast(template_args)); + add_method_body(&method_symbol); +#ifdef DEBUG + std::cout << "MAP for " << symbol << ":" << std::endl; + template_map.print(std::cout); +#endif + } + else + add_method_body(&method_symbol); // build new function expression exprt new_function(cpp_symbol_expr(symbol)); diff --git a/src/cpp/cpp_typecheck_method_bodies.cpp b/src/cpp/cpp_typecheck_method_bodies.cpp index cbabd9e7728..785985984ef 100644 --- a/src/cpp/cpp_typecheck_method_bodies.cpp +++ b/src/cpp/cpp_typecheck_method_bodies.cpp @@ -9,19 +9,28 @@ Author: Daniel Kroening, kroening@cs.cmu.edu /// \file /// C++ Language Type Checking +#ifdef DEBUG +#include +#endif + #include "cpp_typecheck.h" -void cpp_typecheckt::typecheck_method_bodies( - method_bodiest &bodies) +void cpp_typecheckt::typecheck_method_bodies() { instantiation_stackt old_instantiation_stack; old_instantiation_stack.swap(instantiation_stack); - for(auto &b : bodies) + while(!method_bodies.empty()) { - symbolt &method_symbol=*b.method_symbol; - template_map.swap(b.template_map); - instantiation_stack.swap(b.instantiation_stack); + // Dangerous not to take a copy here. We'll have to make sure that + // convert is never called with the same symbol twice. + method_bodyt &method_body = *method_bodies.begin(); + symbolt &method_symbol = *method_body.method_symbol; + + template_map.swap(method_body.template_map); + instantiation_stack.swap(method_body.instantiation_stack); + + method_bodies.erase(method_bodies.begin()); if(method_symbol.name==ID_main) add_argc_argv(method_symbol); @@ -30,9 +39,37 @@ void cpp_typecheckt::typecheck_method_bodies( if(body.id()=="cpp_not_typechecked") continue; +#ifdef DEBUG + std::cout << "convert_method_body: " << method_symbol.name << std::endl; + std::cout << " is_not_nil: " << body.is_not_nil() << std::endl; + std::cout << " !is_zero: " << (!body.is_zero()) << std::endl; +#endif if(body.is_not_nil() && !body.is_zero()) convert_function(method_symbol); } old_instantiation_stack.swap(instantiation_stack); } + +void cpp_typecheckt::add_method_body(symbolt *_method_symbol) +{ +#ifdef DEBUG + std::cout << "add_method_body: " << _method_symbol->name << std::endl; +#endif + + // We have to prevent the same method to be added multiple times + // otherwise we get duplicated symbol prefixes + if(methods_seen.find(_method_symbol->name) != methods_seen.end()) + { +#ifdef DEBUG + std::cout << " already exists" << std::endl; +#endif + return; + } + method_bodies.push_back( + method_bodyt(_method_symbol, template_map, instantiation_stack)); + + // Converting a method body might add method bodies for methods + // that we have already analyzed. Hence, we have to keep track. + methods_seen.insert(_method_symbol->name); +} diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index 5ceb5418416..8d3f5f4a5f1 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -11,6 +11,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_typecheck_resolve.h" +#ifdef DEBUG +#include +#endif + #include #include @@ -189,6 +193,11 @@ void cpp_typecheck_resolvet::remove_duplicates( exprt cpp_typecheck_resolvet::convert_template_parameter( const cpp_idt &identifier) { +#ifdef DEBUG + std::cout << "RESOLVE MAP:" << std::endl; + cpp_typecheck.template_map.print(std::cout); +#endif + // look up the parameter in the template map exprt e=cpp_typecheck.template_map.lookup(identifier.identifier); @@ -668,8 +677,23 @@ void cpp_typecheck_resolvet::make_constructors( identifiers.swap(new_identifiers); } +void cpp_typecheck_resolvet::resolve_argument( + exprt &argument, + const cpp_typecheck_fargst &fargs) +{ + if(argument.id()=="ambiguous") // could come from a template parameter + { + // this must be resolved in the template scope + cpp_save_scopet save_scope(cpp_typecheck.cpp_scopes); + cpp_typecheck.cpp_scopes.go_to(*original_scope); + + argument = resolve(to_cpp_name(argument.type()), wantt::VAR, fargs, false); + } +} + exprt cpp_typecheck_resolvet::do_builtin( const irep_idt &base_name, + const cpp_typecheck_fargst &fargs, const cpp_template_args_non_tct &template_args) { exprt dest; @@ -689,7 +713,7 @@ exprt cpp_typecheck_resolvet::do_builtin( throw 0; } - const exprt &argument=arguments.front(); + exprt argument=arguments.front(); // copy if(argument.id()==ID_type) { @@ -700,6 +724,8 @@ exprt cpp_typecheck_resolvet::do_builtin( throw 0; } + resolve_argument(argument, fargs); + mp_integer i; if(to_integer(argument, i)) { @@ -732,8 +758,10 @@ exprt cpp_typecheck_resolvet::do_builtin( throw 0; } - const exprt &argument0=arguments[0]; - const exprt &argument1=arguments[1]; + exprt argument0=arguments[0]; + resolve_argument(argument0, fargs); + exprt argument1=arguments[1]; + resolve_argument(argument1, fargs); if(argument0.id()==ID_type) { @@ -901,12 +929,13 @@ cpp_scopet &cpp_typecheck_resolvet::resolve_scope( cpp_idt::id_classt::TEMPLATE, id_set); - // std::cout << "S: " - // << cpp_typecheck.cpp_scopes.current_scope().identifier - // << '\n'; - // cpp_typecheck.cpp_scopes.current_scope().print(std::cout); - // std::cout << "X: " << id_set.size() << '\n'; - +#ifdef DEBUG + std::cout << "S: " + << cpp_typecheck.cpp_scopes.current_scope().identifier + << '\n'; + cpp_typecheck.cpp_scopes.current_scope().print(std::cout); + std::cout << "X: " << id_set.size() << '\n'; +#endif symbol_typet instance= disambiguate_template_classes(final_base_name, id_set, template_args); @@ -1380,6 +1409,14 @@ exprt cpp_typecheck_resolvet::resolve( // this changes the scope resolve_scope(cpp_name, base_name, template_args); +#ifdef DEBUG + std::cout << "base name: " << base_name << std::endl; + std::cout << "template args: " << template_args.pretty() << std::endl; + std::cout << "original-scope: " << original_scope->prefix << std::endl; + std::cout << "scope: " + << cpp_typecheck.cpp_scopes.current_scope().prefix << std::endl; +#endif + const source_locationt &source_location=cpp_name.source_location(); bool qualified=cpp_name.is_qualified(); @@ -1387,7 +1424,7 @@ exprt cpp_typecheck_resolvet::resolve( if(qualified) { if(cpp_typecheck.cpp_scopes.current_scope().identifier=="__CPROVER") - return do_builtin(base_name, template_args); + return do_builtin(base_name, fargs, template_args); } else { diff --git a/src/cpp/cpp_typecheck_resolve.h b/src/cpp/cpp_typecheck_resolve.h index 0a8e6d4616a..783b18f8111 100644 --- a/src/cpp/cpp_typecheck_resolve.h +++ b/src/cpp/cpp_typecheck_resolve.h @@ -116,8 +116,13 @@ class cpp_typecheck_resolvet unsigned &args_distance, const cpp_typecheck_fargst &fargs); + void resolve_argument( + exprt &argument, + const cpp_typecheck_fargst &fargs); + exprt do_builtin( const irep_idt &base_name, + const cpp_typecheck_fargst &fargs, const cpp_template_args_non_tct &template_args); void show_identifiers(