From f333c424d7cf2f4cffc869f6041b2fe5d2e3c487 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 6 May 2024 20:29:21 +0200 Subject: [PATCH 01/12] C++ front-end: support constexpr Mark `constexpr` symbols as macros and use direct replacement (non-function symbols) or in-place evaluation (uses of `constexpr` function symbols). --- regression/cpp/constexpr1/main.cpp | 12 +++++ regression/cpp/constexpr1/test.desc | 2 +- src/cpp/cpp_convert_type.cpp | 2 - src/cpp/cpp_declarator_converter.cpp | 17 ++++--- src/cpp/cpp_storage_spec.cpp | 2 + src/cpp/cpp_storage_spec.h | 13 +++++- src/cpp/cpp_typecheck_expr.cpp | 66 ++++++++++++++++++++++++++++ src/cpp/cpp_typecheck_resolve.cpp | 12 ++++- src/cpp/parse.cpp | 32 ++++++-------- 9 files changed, 128 insertions(+), 30 deletions(-) diff --git a/regression/cpp/constexpr1/main.cpp b/regression/cpp/constexpr1/main.cpp index 4c54dd28cec..55724408fa7 100644 --- a/regression/cpp/constexpr1/main.cpp +++ b/regression/cpp/constexpr1/main.cpp @@ -14,6 +14,18 @@ constexpr int some_other_value = static_assert(some_other_value == 2, "some_other_value == 2"); +constexpr int some_function2(int a) +{ + int b; + a = a + 1; + b = a; + return b + 1; +} + +constexpr int some_other_value2 = some_function2(1); + +static_assert(some_other_value2 == 3, "some_other_value == 2"); + int main() { } diff --git a/regression/cpp/constexpr1/test.desc b/regression/cpp/constexpr1/test.desc index 0daa9695017..3862862ffd3 100644 --- a/regression/cpp/constexpr1/test.desc +++ b/regression/cpp/constexpr1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.cpp -std=c++11 ^EXIT=0$ diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp index d55fd811898..f77bd262eab 100644 --- a/src/cpp/cpp_convert_type.cpp +++ b/src/cpp/cpp_convert_type.cpp @@ -63,8 +63,6 @@ void cpp_convert_typet::read_rec(const typet &type) ++char16_t_count; else if(type.id()==ID_char32_t) ++char32_t_count; - else if(type.id()==ID_constexpr) - c_qualifiers.is_constant = true; else if(type.id()==ID_function_type) { read_function_type(type); diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp index cfeeaf929d5..a1ad94f9679 100644 --- a/src/cpp/cpp_declarator_converter.cpp +++ b/src/cpp/cpp_declarator_converter.cpp @@ -456,7 +456,8 @@ symbolt &cpp_declarator_convertert::convert_new_symbol( symbol.is_weak = storage_spec.is_weak(); symbol.module=cpp_typecheck.module; symbol.is_type=is_typedef; - symbol.is_macro=is_typedef && !is_template_parameter; + symbol.is_macro = + (is_typedef && !is_template_parameter) || storage_spec.is_constexpr(); symbol.pretty_name=pretty_name; if(is_code && !symbol.is_type) @@ -493,7 +494,7 @@ symbolt &cpp_declarator_convertert::convert_new_symbol( storage_spec.is_thread_local(); symbol.is_file_local = - symbol.is_macro || + (symbol.is_macro && !storage_spec.is_constexpr()) || (!cpp_typecheck.cpp_scopes.current_scope().is_global_scope() && !storage_spec.is_extern()) || (cpp_typecheck.cpp_scopes.current_scope().is_global_scope() && @@ -553,10 +554,14 @@ symbolt &cpp_declarator_convertert::convert_new_symbol( // do the value if(!new_symbol->is_type) { - if(is_code && declarator.type().id()!=ID_template) - cpp_typecheck.add_method_body(new_symbol); - - if(!is_code) + if(is_code) + { + if(new_symbol->is_macro) + cpp_typecheck.convert_function(*new_symbol); + else if(declarator.type().id() != ID_template) + cpp_typecheck.add_method_body(new_symbol); + } + else cpp_typecheck.convert_initializer(*new_symbol); } diff --git a/src/cpp/cpp_storage_spec.cpp b/src/cpp/cpp_storage_spec.cpp index 170abe0d6f5..df8c7587c01 100644 --- a/src/cpp/cpp_storage_spec.cpp +++ b/src/cpp/cpp_storage_spec.cpp @@ -33,4 +33,6 @@ void cpp_storage_spect::read(const typet &type) set_asm(); else if(type.id() == ID_weak) set_weak(); + else if(type.id() == ID_constexpr) + set_constexpr(); } diff --git a/src/cpp/cpp_storage_spec.h b/src/cpp/cpp_storage_spec.h index db9d0e52833..d7118a848ef 100644 --- a/src/cpp/cpp_storage_spec.h +++ b/src/cpp/cpp_storage_spec.h @@ -47,6 +47,10 @@ class cpp_storage_spect:public irept { return get_bool(ID_weak); } + bool is_constexpr() const + { + return get_bool(ID_constexpr); + } void set_static() { set(ID_static, true); } void set_extern() { set(ID_extern, true); } @@ -59,11 +63,16 @@ class cpp_storage_spect:public irept { set(ID_weak, true); } + void set_constexpr() + { + set(ID_constexpr, true); + } bool is_empty() const { return !is_static() && !is_extern() && !is_auto() && !is_register() && - !is_mutable() && !is_thread_local() && !is_asm() && !is_weak(); + !is_mutable() && !is_thread_local() && !is_asm() && !is_weak() && + !is_constexpr(); } cpp_storage_spect &operator|=(const cpp_storage_spect &other) @@ -84,6 +93,8 @@ class cpp_storage_spect:public irept set_asm(); if(other.is_weak()) set_weak(); + if(other.is_constexpr()) + set_constexpr(); return *this; } diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index 2685771889c..6675545d33d 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include +#include #include #include @@ -1825,6 +1826,71 @@ void cpp_typecheckt::typecheck_side_effect_function_call( add_implicit_dereference(expr); + if(auto sym_expr = expr_try_dynamic_cast(expr.function())) + { + const auto &symbol = lookup(sym_expr->get_identifier()); + if(symbol.is_macro) + { + // constexpr functions evaluated using a mini interpreter + const auto &code_type = to_code_type(symbol.type); + // PRECONDITION(code_type.return_type().id() != ID_empty); + PRECONDITION(expr.arguments().size() == code_type.parameters().size()); + replace_symbolt value_map; + auto param_it = code_type.parameters().begin(); + for(const auto &arg : expr.arguments()) + { + value_map.insert( + symbol_exprt{param_it->get_identifier(), param_it->type()}, + typecast_exprt::conditional_cast(arg, param_it->type())); + ++param_it; + } + const auto &block = to_code_block(to_code(symbol.value)); + for(const auto &stmt : block.statements()) + { + if( + auto return_stmt = expr_try_dynamic_cast(stmt)) + { + PRECONDITION(return_stmt->has_return_value()); + exprt tmp = return_stmt->return_value(); + value_map.replace(tmp); + expr.swap(tmp); + return; + } + else if(auto expr_stmt = expr_try_dynamic_cast(stmt)) + { + // C++14 and later only + if( + auto assign = expr_try_dynamic_cast( + expr_stmt->expression())) + { + PRECONDITION(assign->lhs().id() == ID_symbol); + exprt rhs = assign->rhs(); + value_map.replace(rhs); + value_map.set(to_symbol_expr(assign->lhs()), rhs); + } + else + UNIMPLEMENTED_FEATURE( + "constexpr with " + expr_stmt->expression().pretty()); + } + else if(stmt.get_statement() == ID_decl_block) + { + // C++14 and later only + for(const auto &expect_decl : stmt.operands()) + { + PRECONDITION(to_code(expect_decl).get_statement() == ID_decl); + PRECONDITION(!to_code_frontend_decl(to_code(expect_decl)) + .initial_value() + .has_value()); + } + } + else + { + UNIMPLEMENTED_FEATURE("constexpr with " + stmt.pretty()); + } + } + } + } + // we will deal with some 'special' functions here exprt tmp=do_special_functions(expr); if(tmp.is_not_nil()) diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index e555353ed55..b855f095fa1 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -359,8 +359,16 @@ exprt cpp_typecheck_resolvet::convert_identifier( } else if(symbol.is_macro) { - e=symbol.value; - PRECONDITION(e.is_not_nil()); + if(symbol.type.id() == ID_code) + { + // constexpr function + e = cpp_symbol_expr(symbol); + } + else + { + e = symbol.value; + PRECONDITION(e.is_not_nil()); + } } else { diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 777f4b2f0bd..46d6b937574 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -764,11 +764,10 @@ bool Parser::isTypeSpecifier() { int t=lex.LookAhead(0); - return is_identifier(t) || t == TOK_SCOPE || t == TOK_CONSTEXPR || - t == TOK_CONST || t == TOK_VOLATILE || t == TOK_RESTRICT || - t == TOK_CHAR || t == TOK_INT || t == TOK_SHORT || t == TOK_LONG || - t == TOK_CHAR16_T || t == TOK_CHAR32_T || t == TOK_WCHAR_T || - t == TOK_COMPLEX // new !!! + return is_identifier(t) || t == TOK_SCOPE || t == TOK_CONST || + t == TOK_VOLATILE || t == TOK_RESTRICT || t == TOK_CHAR || + t == TOK_INT || t == TOK_SHORT || t == TOK_LONG || t == TOK_CHAR16_T || + t == TOK_CHAR32_T || t == TOK_WCHAR_T || t == TOK_COMPLEX // new !!! || t == TOK_SIGNED || t == TOK_UNSIGNED || t == TOK_FLOAT || t == TOK_DOUBLE || t == TOK_INT8 || t == TOK_INT16 || t == TOK_INT32 || t == TOK_INT64 || t == TOK_GCC_INT128 || t == TOK_PTR32 || @@ -2018,7 +2017,7 @@ bool Parser::optMemberSpec(cpp_member_spect &member_spec) /* storage.spec : STATIC | EXTERN | AUTO | REGISTER | MUTABLE | ASM | - THREAD_LOCAL + THREAD_LOCAL | CONSTEXPR */ bool Parser::optStorageSpec(cpp_storage_spect &storage_spec) { @@ -2027,7 +2026,7 @@ bool Parser::optStorageSpec(cpp_storage_spect &storage_spec) if( t == TOK_STATIC || t == TOK_EXTERN || (t == TOK_AUTO && !cpp11) || t == TOK_REGISTER || t == TOK_MUTABLE || t == TOK_GCC_ASM || - t == TOK_THREAD_LOCAL) + t == TOK_THREAD_LOCAL || t == TOK_CONSTEXPR) { cpp_tokent tk; lex.get_token(tk); @@ -2041,6 +2040,9 @@ bool Parser::optStorageSpec(cpp_storage_spect &storage_spec) case TOK_MUTABLE: storage_spec.set_mutable(); break; case TOK_GCC_ASM: storage_spec.set_asm(); break; case TOK_THREAD_LOCAL: storage_spec.set_thread_local(); break; + case TOK_CONSTEXPR: + storage_spec.set_constexpr(); + break; default: UNREACHABLE; } @@ -2051,17 +2053,17 @@ bool Parser::optStorageSpec(cpp_storage_spect &storage_spec) } /* - cv.qualify : (CONSTEXPR | CONST | VOLATILE | RESTRICT)+ + cv.qualify : (CONST | VOLATILE | RESTRICT)+ */ bool Parser::optCvQualify(typet &cv) { for(;;) { int t=lex.LookAhead(0); - if(t==TOK_CONSTEXPR || - t==TOK_CONST || t==TOK_VOLATILE || t==TOK_RESTRICT || - t==TOK_PTR32 || t==TOK_PTR64 || - t==TOK_GCC_ATTRIBUTE || t==TOK_GCC_ASM) + if( + t == TOK_CONST || t == TOK_VOLATILE || t == TOK_RESTRICT || + t == TOK_PTR32 || t == TOK_PTR64 || t == TOK_GCC_ATTRIBUTE || + t == TOK_GCC_ASM) { cpp_tokent tk; lex.get_token(tk); @@ -2069,12 +2071,6 @@ bool Parser::optCvQualify(typet &cv) switch(t) { - case TOK_CONSTEXPR: - p=typet(ID_constexpr); - set_location(p, tk); - merge_types(p, cv); - break; - case TOK_CONST: p=typet(ID_const); set_location(p, tk); From cb7651aed49c322caa2df9f22bcf8c3852e50f99 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 6 May 2024 22:32:46 +0200 Subject: [PATCH 02/12] C++ front-end: parse template parameter packs Attach the "ellipsis" information to the declarator and not to the type. --- .../cpp/type_traits_essentials1/test.desc | 2 +- src/cpp/cpp_declarator.h | 10 ++++ src/cpp/parse.cpp | 51 ++++++------------- 3 files changed, 26 insertions(+), 37 deletions(-) diff --git a/regression/cpp/type_traits_essentials1/test.desc b/regression/cpp/type_traits_essentials1/test.desc index 0daa9695017..3862862ffd3 100644 --- a/regression/cpp/type_traits_essentials1/test.desc +++ b/regression/cpp/type_traits_essentials1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.cpp -std=c++11 ^EXIT=0$ diff --git a/src/cpp/cpp_declarator.h b/src/cpp/cpp_declarator.h index 2f62817383a..a459e73eb3f 100644 --- a/src/cpp/cpp_declarator.h +++ b/src/cpp/cpp_declarator.h @@ -55,6 +55,16 @@ class cpp_declaratort:public exprt set(ID_is_parameter, is_parameter); } + bool get_has_ellipsis() const + { + return get_bool(ID_ellipsis); + } + + void set_has_ellipsis() + { + set(ID_ellipsis, true); + } + // initializers for function arguments exprt &init_args() { diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 46d6b937574..260f3dc6cf5 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -1207,14 +1207,11 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration) declarator.type().make_nil(); set_location(declarator, tk1); - bool has_ellipsis=false; - if(lex.LookAhead(0)==TOK_ELLIPSIS) { cpp_tokent tk2; lex.get_token(tk2); - - has_ellipsis=true; + declarator.set_has_ellipsis(); } if(is_identifier(lex.LookAhead(0))) @@ -1226,16 +1223,11 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration) set_location(declarator.name(), tk2); add_id(declarator.name(), new_scopet::kindt::TYPE_TEMPLATE_PARAMETER); - - if(has_ellipsis) - { - // TODO - } } if(lex.LookAhead(0)=='=') { - if(has_ellipsis) + if(declarator.get_has_ellipsis()) return false; typet default_type; @@ -1308,19 +1300,16 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration) << "Parser::rTempArgDeclaration 3\n"; #endif - bool has_ellipsis=false; + declaration.declarators().resize(1); + cpp_declaratort &declarator = declaration.declarators().front(); if(lex.LookAhead(0)==TOK_ELLIPSIS) { cpp_tokent tk2; lex.get_token(tk2); - - has_ellipsis=true; + declarator.set_has_ellipsis(); } - declaration.declarators().resize(1); - cpp_declaratort &declarator=declaration.declarators().front(); - if(!rDeclarator(declarator, kArgDeclarator, true, false)) return false; @@ -1331,16 +1320,11 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration) add_id(declarator.name(), new_scopet::kindt::NON_TYPE_TEMPLATE_PARAMETER); - if(has_ellipsis) - { - // TODO - } - exprt &value=declarator.value(); if(lex.LookAhead(0)=='=') { - if(has_ellipsis) + if(declarator.get_has_ellipsis()) return false; cpp_tokent tk; @@ -4006,8 +3990,7 @@ bool Parser::rTemplateArgs(irept &template_args) if(lex.LookAhead(0)==TOK_ELLIPSIS) { lex.get_token(tk1); - - // TODO + exp.set(ID_ellipsis, true); } #ifdef DEBUG std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4.2\n"; @@ -4025,13 +4008,6 @@ bool Parser::rTemplateArgs(irept &template_args) if(!rConditionalExpr(exp, true)) return false; - - if(lex.LookAhead(0)==TOK_ELLIPSIS) - { - lex.get_token(tk1); - - // TODO - } } #ifdef DEBUG @@ -5684,18 +5660,21 @@ bool Parser::rTypeNameOrFunctionType(typet &tname) type.parameters().push_back(parameter); t=lex.LookAhead(0); - if(t==',') + if(t == TOK_ELLIPSIS) { cpp_tokent tk; lex.get_token(tk); + to_cpp_declaration(type.parameters().back()) + .declarators() + .back() + .set_has_ellipsis(); + t = lex.LookAhead(0); } - else if(t==TOK_ELLIPSIS) + + if(t == ',') { - // TODO -- this is actually ambiguous as it could refer to a - // template parameter pack or declare a variadic function cpp_tokent tk; lex.get_token(tk); - type.make_ellipsis(); } else if(t==')') break; From 55b0cd02032221e2ffa1a294fd5add4305353e03 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 7 May 2024 10:43:37 +0000 Subject: [PATCH 03/12] DEBUG --- src/cpp/parse.cpp | 90 +++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 88 insertions(+), 2 deletions(-) diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 260f3dc6cf5..08569f44e0d 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_member_spec.h" #include "cpp_enum_type.h" +#define DEBUG #ifdef DEBUG #include @@ -1030,6 +1031,11 @@ bool Parser::rLinkageBody(cpp_linkage_spect::itemst &items) */ bool Parser::rTemplateDecl(cpp_declarationt &decl) { +#ifdef DEBUG + indenter _i; + std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl 1\n"; +#endif + TemplateDeclKind kind=tdk_unknown; make_sub_scope("#template", new_scopet::kindt::TEMPLATE); @@ -1039,6 +1045,10 @@ bool Parser::rTemplateDecl(cpp_declarationt &decl) if(!rTemplateDecl2(template_type, kind)) return false; +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl 2\n"; +#endif + cpp_declarationt body; if(lex.LookAhead(0)==TOK_USING) { @@ -1086,11 +1096,20 @@ bool Parser::rTemplateDecl(cpp_declarationt &decl) bool Parser::rTemplateDecl2(typet &decl, TemplateDeclKind &kind) { +#ifdef DEBUG + indenter _i; + std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 1\n"; +#endif + cpp_tokent tk; if(lex.get_token(tk)!=TOK_TEMPLATE) return false; +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 2\n"; +#endif + decl=typet(ID_template); set_location(decl, tk); @@ -1101,17 +1120,33 @@ bool Parser::rTemplateDecl2(typet &decl, TemplateDeclKind &kind) return true; // ignore TEMPLATE } +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 3\n"; +#endif + if(lex.get_token(tk)!='<') return false; irept &template_parameters=decl.add(ID_template_parameters); +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 4\n"; +#endif + if(!rTempArgList(template_parameters)) return false; +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 5\n"; +#endif + if(lex.get_token(tk)!='>') return false; +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 6\n"; +#endif + // ignore nested TEMPLATE while(lex.LookAhead(0)==TOK_TEMPLATE) { @@ -1128,6 +1163,10 @@ bool Parser::rTemplateDecl2(typet &decl, TemplateDeclKind &kind) return false; } +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 7\n"; +#endif + if(template_parameters.get_sub().empty()) // template < > declaration kind=tdk_specialization; @@ -1188,6 +1227,10 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration) if((t0==TOK_CLASS || t0==TOK_TYPENAME)) { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.1\n"; +#endif + cpp_token_buffert::post pos=lex.Save(); cpp_tokent tk1; @@ -1227,6 +1270,10 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration) if(lex.LookAhead(0)=='=') { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.2\n"; +#endif + if(declarator.get_has_ellipsis()) return false; @@ -1239,10 +1286,38 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration) declarator.value()=exprt(ID_type); declarator.value().type().swap(default_type); } +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.3\n"; +#endif if(lex.LookAhead(0)==',' || lex.LookAhead(0)=='>') return true; +#if 0 + else if(lex.LookAhead(0) == TOK_SHIFTRIGHT) + { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.4\n"; +#endif + + // turn >> into > > + cpp_token_buffert::post pos=lex.Save(); + cpp_tokent tk; + lex.get_token(tk); + lex.Restore(pos); + tk.kind='>'; + tk.text='>'; + lex.Replace(tk); + lex.Insert(tk); + DATA_INVARIANT(lex.LookAhead(0) == '>', "should be >"); + DATA_INVARIANT(lex.LookAhead(1) == '>', "should be >"); + return true; + } +#endif +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.5\n"; +#endif + lex.Restore(pos); } @@ -3968,7 +4043,8 @@ bool Parser::rTemplateArgs(irept &template_args) ) { #ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4\n"; + std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4 " << + lex.LookAhead(0) << "\n"; #endif // ok @@ -3980,20 +4056,30 @@ bool Parser::rTemplateArgs(irept &template_args) lex.Restore(pos); exprt tmp; if(rConditionalExpr(tmp, true)) + { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4.0\n"; +#endif exp.id(ID_ambiguous); + } #ifdef DEBUG std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4.1\n"; #endif lex.Restore(pos); rTypeNameOrFunctionType(a); +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4.1a " << + lex.LookAhead(0) << "\n"; +#endif if(lex.LookAhead(0)==TOK_ELLIPSIS) { lex.get_token(tk1); exp.set(ID_ellipsis, true); } #ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4.2\n"; + std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4.2 " << + lex.LookAhead(0) << "\n"; #endif } else From 0fff3a7562fcbb16fdd1628c77cb1e62ecf3a916 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 7 May 2024 10:43:45 +0000 Subject: [PATCH 04/12] Revert "DEBUG" This reverts commit 4c299cc716f9e0bf639411296f1ee5f2c5d96300. --- src/cpp/parse.cpp | 90 ++--------------------------------------------- 1 file changed, 2 insertions(+), 88 deletions(-) diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 08569f44e0d..260f3dc6cf5 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -23,7 +23,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_member_spec.h" #include "cpp_enum_type.h" -#define DEBUG #ifdef DEBUG #include @@ -1031,11 +1030,6 @@ bool Parser::rLinkageBody(cpp_linkage_spect::itemst &items) */ bool Parser::rTemplateDecl(cpp_declarationt &decl) { -#ifdef DEBUG - indenter _i; - std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl 1\n"; -#endif - TemplateDeclKind kind=tdk_unknown; make_sub_scope("#template", new_scopet::kindt::TEMPLATE); @@ -1045,10 +1039,6 @@ bool Parser::rTemplateDecl(cpp_declarationt &decl) if(!rTemplateDecl2(template_type, kind)) return false; -#ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl 2\n"; -#endif - cpp_declarationt body; if(lex.LookAhead(0)==TOK_USING) { @@ -1096,20 +1086,11 @@ bool Parser::rTemplateDecl(cpp_declarationt &decl) bool Parser::rTemplateDecl2(typet &decl, TemplateDeclKind &kind) { -#ifdef DEBUG - indenter _i; - std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 1\n"; -#endif - cpp_tokent tk; if(lex.get_token(tk)!=TOK_TEMPLATE) return false; -#ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 2\n"; -#endif - decl=typet(ID_template); set_location(decl, tk); @@ -1120,33 +1101,17 @@ bool Parser::rTemplateDecl2(typet &decl, TemplateDeclKind &kind) return true; // ignore TEMPLATE } -#ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 3\n"; -#endif - if(lex.get_token(tk)!='<') return false; irept &template_parameters=decl.add(ID_template_parameters); -#ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 4\n"; -#endif - if(!rTempArgList(template_parameters)) return false; -#ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 5\n"; -#endif - if(lex.get_token(tk)!='>') return false; -#ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 6\n"; -#endif - // ignore nested TEMPLATE while(lex.LookAhead(0)==TOK_TEMPLATE) { @@ -1163,10 +1128,6 @@ bool Parser::rTemplateDecl2(typet &decl, TemplateDeclKind &kind) return false; } -#ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 7\n"; -#endif - if(template_parameters.get_sub().empty()) // template < > declaration kind=tdk_specialization; @@ -1227,10 +1188,6 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration) if((t0==TOK_CLASS || t0==TOK_TYPENAME)) { -#ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.1\n"; -#endif - cpp_token_buffert::post pos=lex.Save(); cpp_tokent tk1; @@ -1270,10 +1227,6 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration) if(lex.LookAhead(0)=='=') { -#ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.2\n"; -#endif - if(declarator.get_has_ellipsis()) return false; @@ -1286,38 +1239,10 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration) declarator.value()=exprt(ID_type); declarator.value().type().swap(default_type); } -#ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.3\n"; -#endif if(lex.LookAhead(0)==',' || lex.LookAhead(0)=='>') return true; -#if 0 - else if(lex.LookAhead(0) == TOK_SHIFTRIGHT) - { -#ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.4\n"; -#endif - - // turn >> into > > - cpp_token_buffert::post pos=lex.Save(); - cpp_tokent tk; - lex.get_token(tk); - lex.Restore(pos); - tk.kind='>'; - tk.text='>'; - lex.Replace(tk); - lex.Insert(tk); - DATA_INVARIANT(lex.LookAhead(0) == '>', "should be >"); - DATA_INVARIANT(lex.LookAhead(1) == '>', "should be >"); - return true; - } -#endif -#ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.5\n"; -#endif - lex.Restore(pos); } @@ -4043,8 +3968,7 @@ bool Parser::rTemplateArgs(irept &template_args) ) { #ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4 " << - lex.LookAhead(0) << "\n"; + std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4\n"; #endif // ok @@ -4056,30 +3980,20 @@ bool Parser::rTemplateArgs(irept &template_args) lex.Restore(pos); exprt tmp; if(rConditionalExpr(tmp, true)) - { -#ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4.0\n"; -#endif exp.id(ID_ambiguous); - } #ifdef DEBUG std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4.1\n"; #endif lex.Restore(pos); rTypeNameOrFunctionType(a); -#ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4.1a " << - lex.LookAhead(0) << "\n"; -#endif if(lex.LookAhead(0)==TOK_ELLIPSIS) { lex.get_token(tk1); exp.set(ID_ellipsis, true); } #ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4.2 " << - lex.LookAhead(0) << "\n"; + std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4.2\n"; #endif } else From 7278536c4b4932c660ae4c3e952957dd1115a0cb Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 8 May 2024 11:18:14 +0000 Subject: [PATCH 05/12] C++ front-end: support explicit type conversion with braced-init-list Now follows the grammar described in the C++ standard: Explicit type conversions are postfix expressions. This required adding rules for C++ cast expressions, which in turn simplifies type checking for we no longer treat them as function calls with template arguments. --- regression/cbmc-cpp/Constructor7/main.cpp | 16 + regression/cbmc-cpp/Constructor7/test.desc | 8 + regression/cpp/brace_initializer1/main.cpp | 24 ++ regression/cpp/brace_initializer1/test.desc | 8 + src/ansi-c/parser.y | 4 + src/ansi-c/scanner.l | 5 + src/cpp/cpp_is_pod.cpp | 4 + src/cpp/cpp_typecheck_expr.cpp | 78 +--- src/cpp/parse.cpp | 378 +++++++++++++------- 9 files changed, 336 insertions(+), 189 deletions(-) create mode 100644 regression/cbmc-cpp/Constructor7/main.cpp create mode 100644 regression/cbmc-cpp/Constructor7/test.desc create mode 100644 regression/cpp/brace_initializer1/main.cpp create mode 100644 regression/cpp/brace_initializer1/test.desc diff --git a/regression/cbmc-cpp/Constructor7/main.cpp b/regression/cbmc-cpp/Constructor7/main.cpp new file mode 100644 index 00000000000..e01ab3ffd00 --- /dev/null +++ b/regression/cbmc-cpp/Constructor7/main.cpp @@ -0,0 +1,16 @@ +#include + +int main(int argc, char * argv[]) +{ + struct S { + S() : x(42) + { + } + + int x; + }; + S s = S{}; + + __CPROVER_assert(s.x == 42, ""); + assert(s.x == 42); +} diff --git a/regression/cbmc-cpp/Constructor7/test.desc b/regression/cbmc-cpp/Constructor7/test.desc new file mode 100644 index 00000000000..91d9cf8b52e --- /dev/null +++ b/regression/cbmc-cpp/Constructor7/test.desc @@ -0,0 +1,8 @@ +CORE +main.cpp + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cpp/brace_initializer1/main.cpp b/regression/cpp/brace_initializer1/main.cpp new file mode 100644 index 00000000000..0910fc42dd8 --- /dev/null +++ b/regression/cpp/brace_initializer1/main.cpp @@ -0,0 +1,24 @@ +struct __invoke_memfun_ref {}; + constexpr bool __call_is_nt(__invoke_memfun_ref) + { + return false; + } + + template + struct __call_is_nothrow + { + constexpr static bool is_nt = +__call_is_nt(typename _Result::__invoke_type{}); + }; + +int main(int argc, char * argv[]) +{ + struct S { + S() : x(42) + { + } + + int x; + }; + S s = S{}; +} diff --git a/regression/cpp/brace_initializer1/test.desc b/regression/cpp/brace_initializer1/test.desc new file mode 100644 index 00000000000..3862862ffd3 --- /dev/null +++ b/regression/cpp/brace_initializer1/test.desc @@ -0,0 +1,8 @@ +CORE +main.cpp +-std=c++11 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 59e320f7112..bb8a8057688 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -279,6 +279,10 @@ int yyansi_cerror(const std::string &error); %token TOK_MSC_IF_EXISTS "__if_exists" %token TOK_MSC_IF_NOT_EXISTS "__if_not_exists" %token TOK_UNDERLYING_TYPE "__underlying_type" +%token TOK_DYNAMIC_CAST "dynamic_cast" +%token TOK_STATIC_CAST "static_cast" +%token TOK_REINTERPRET_CAST "reinterpret_cast" +%token TOK_CONST_CAST "const_cast" /*** priority, associativity, etc. definitions **************************/ diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index ad408dbeb31..b02a0111339 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -1316,6 +1316,11 @@ __decltype { if(PARSER.cpp98 && return make_identifier(); } +"dynamic_cast" { return cpp98_keyword(TOK_DYNAMIC_CAST); } +"static_cast" { return cpp98_keyword(TOK_STATIC_CAST); } +"reinterpret_cast" { return cpp98_keyword(TOK_REINTERPRET_CAST); } +"const_cast" { return cpp98_keyword(TOK_CONST_CAST); } + {CPROVER_PREFIX}"atomic" { loc(); return TOK_CPROVER_ATOMIC; } {CPROVER_PREFIX}"forall" { loc(); return TOK_FORALL; } {CPROVER_PREFIX}"exists" { loc(); return TOK_EXISTS; } diff --git a/src/cpp/cpp_is_pod.cpp b/src/cpp/cpp_is_pod.cpp index d1acd9b71b8..c11ffb54b6a 100644 --- a/src/cpp/cpp_is_pod.cpp +++ b/src/cpp/cpp_is_pod.cpp @@ -73,6 +73,10 @@ bool cpp_typecheckt::cpp_is_pod(const typet &type) const { return cpp_is_pod(to_array_type(type).element_type()); } + else if(type.id()==ID_vector) + { + return cpp_is_pod(to_vector_type(type).element_type()); + } else if(type.id()==ID_pointer) { if(is_reference(type)) // references are not PODs diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index 6675545d33d..8cee6b3f829 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -127,6 +127,13 @@ void cpp_typecheckt::typecheck_expr_main(exprt &expr) { expr.type().id(ID_initializer_list); } + else if(expr.id() == ID_const_cast || + expr.id() == ID_dynamic_cast || + expr.id() == ID_reinterpret_cast || + expr.id() == ID_static_cast) + { + typecheck_cast_expr(expr); + } else c_typecheck_baset::typecheck_expr_main(expr); } @@ -967,13 +974,8 @@ void cpp_typecheckt::typecheck_expr_explicit_constructor_call(exprt &expr) } else { - CHECK_RETURN(expr.type().id() == ID_struct); - - struct_tag_typet tag(expr.type().get(ID_name)); - tag.add_source_location() = expr.source_location(); - exprt e=expr; - new_temporary(e.source_location(), tag, e.operands(), expr); + new_temporary(e.source_location(), e.type(), e.operands(), expr); } } @@ -1275,53 +1277,20 @@ void cpp_typecheckt::typecheck_expr_ptrmember( void cpp_typecheckt::typecheck_cast_expr(exprt &expr) { - side_effect_expr_function_callt e = - to_side_effect_expr_function_call(expr); - - if(e.arguments().size() != 1) + if(expr.operands().size() != 1) { error().source_location=expr.find_source_location(); error() << "cast expressions expect one operand" << eom; throw 0; } - exprt &f_op=e.function(); - exprt &cast_op=e.arguments().front(); + exprt &cast_op = to_unary_expr(expr).op(); add_implicit_dereference(cast_op); - const irep_idt &id= - f_op.get_sub().front().get(ID_identifier); - - if(f_op.get_sub().size()!=2 || - f_op.get_sub()[1].id()!=ID_template_args) - { - error().source_location=expr.find_source_location(); - error() << id << " expects template argument" << eom; - throw 0; - } - - irept &template_arguments=f_op.get_sub()[1].add(ID_arguments); - - if(template_arguments.get_sub().size()!=1) - { - error().source_location=expr.find_source_location(); - error() << id << " expects one template argument" << eom; - throw 0; - } - - irept &template_arg=template_arguments.get_sub().front(); - - if(template_arg.id() != ID_type && template_arg.id() != ID_ambiguous) - { - error().source_location=expr.find_source_location(); - error() << id << " expects a type as template argument" << eom; - throw 0; - } - - typet &type=static_cast( - template_arguments.get_sub().front().add(ID_type)); + const irep_idt &id = expr.id(); + typet &type = expr.type(); typecheck_type(type); source_locationt source_location=expr.source_location(); @@ -1415,21 +1384,6 @@ void cpp_typecheckt::typecheck_expr_cpp_name( } } - if(expr.get_sub().size()>=1 && - expr.get_sub().front().id()==ID_name) - { - const irep_idt &id=expr.get_sub().front().get(ID_identifier); - - if(id==ID_const_cast || - id==ID_dynamic_cast || - id==ID_reinterpret_cast || - id==ID_static_cast) - { - expr.id(ID_cast_expression); - return; - } - } - exprt symbol_expr= resolve( to_cpp_name(expr), @@ -1556,14 +1510,6 @@ void cpp_typecheckt::typecheck_side_effect_function_call( return; } - else if(expr.function().id() == ID_cast_expression) - { - // These are not really function calls, - // but usually just type adjustments. - typecheck_cast_expr(expr); - add_implicit_dereference(expr); - return; - } else if(expr.function().id() == ID_cpp_dummy_destructor) { // these don't do anything, e.g., (char*)->~char() diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 260f3dc6cf5..a0cdb418139 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -341,6 +341,7 @@ class Parser // NOLINT(readability/identifiers) bool rAllocateType(exprt &, typet &, exprt &); bool rNewDeclarator(typet &); bool rAllocateInitializer(exprt &); + bool rCppCastExpr(exprt &); bool rPostfixExpr(exprt &); bool rPrimaryExpr(exprt &); bool rVarName(exprt &); @@ -4196,11 +4197,23 @@ bool Parser::rArgDeclaration(cpp_declarationt &declaration) */ bool Parser::rInitializeExpr(exprt &expr) { +#ifdef DEBUG + indenter _i; + std::cout << std::string(__indent, ' ') << "Parser::rInitializeExpr 0 " + << lex.LookAhead(0) + << ' ' << lex.current_token().text + << '\n'; +#endif + if(lex.LookAhead(0)!='{') return rExpression(expr, false); // we want { initialize_expr, ... } +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rInitializeExpr 1\n"; +#endif + cpp_tokent tk; lex.get_token(tk); @@ -4278,7 +4291,7 @@ bool Parser::rInitializeExpr(exprt &expr) /* function.arguments : empty - | expression (',' expression)* + | initializer.expr (',' initializer.expr)* This assumes that the next token following function.arguments is ')'. */ @@ -4293,7 +4306,7 @@ bool Parser::rFunctionArguments(exprt &args) for(;;) { - if(!rExpression(exp, false)) + if(!rInitializeExpr(exp)) return false; args.add_to_operands(std::move(exp)); @@ -4832,7 +4845,9 @@ bool Parser::rCommaExpression(exprt &exp) /* expression - : conditional.expr {(AssignOp | '=') expression} right-to-left + : conditional.expr + | logical.or.expr (AssignOp | '=') initialize.expr + | throw.expression */ bool Parser::rExpression(exprt &exp, bool template_args) { @@ -4843,7 +4858,30 @@ bool Parser::rExpression(exprt &exp, bool template_args) std::cout << std::string(__indent, ' ') << "Parser::rExpression 0\n"; #endif - if(!rConditionalExpr(exp, template_args)) + if(lex.LookAhead(0) == TOK_THROW) + return rThrowExpr(exp); + + cpp_token_buffert::post pos=lex.Save(); + + // see whether we have logical.or.expr followed by '?'; the parsed expression + // will be discarded and be parsed again, below + exprt tmp; + if(!rLogicalOrExpr(tmp, template_args)) + return false; + + if(lex.LookAhead(0) == '?') + { + lex.Restore(pos); + return rConditionalExpr(exp, template_args); + } + +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rExpression 0.1\n"; +#endif + + lex.Restore(pos); + + if(!rLogicalOrExpr(exp, template_args)) return false; #ifdef DEBUG @@ -4865,7 +4903,7 @@ bool Parser::rExpression(exprt &exp, bool template_args) #endif exprt right; - if(!rExpression(right, template_args)) + if(!rInitializeExpr(right)) return false; #ifdef DEBUG @@ -4913,7 +4951,7 @@ bool Parser::rExpression(exprt &exp, bool template_args) /* conditional.expr - : logical.or.expr {'?' comma.expression ':' conditional.expr} right-to-left + : logical.or.expr {'?' comma.expression ':' expression} right-to-left */ bool Parser::rConditionalExpr(exprt &exp, bool template_args) { @@ -5434,6 +5472,7 @@ bool Parser::rPmExpr(exprt &exp) cast.expr : unary.expr | '(' type.name ')' cast.expr + | '(' type.name ')' initializer.expr -- GCC/Clang extension */ bool Parser::rCastExpr(exprt &exp) { @@ -5471,6 +5510,20 @@ bool Parser::rCastExpr(exprt &exp) // we have (x) & 123 // This is likely a binary bit-wise 'and' } + else if(lex.LookAhead(0)=='{') + { + // this is a GCC/Clang extension + exprt exp2; + if(!rInitializeExpr(exp2)) + return false; + + exp=exprt("explicit-typecast"); + exp.type().swap(tname); + exp.add_to_operands(std::move(exp2)); + set_location(exp, tk1); + + return true; + } else if(rCastExpr(exp)) { exprt op; @@ -5717,9 +5770,9 @@ bool Parser::rTypeNameOrFunctionType(typet &tname) : postfix.expr | ('*' | '&' | '+' | '-' | '!' | '~' | IncOp) cast.expr | sizeof.expr - | allocate.expr - | throw.expression + | alignof.expr | noexcept.expr + | allocate.expr */ bool Parser::rUnaryExpr(exprt &exp) @@ -5799,8 +5852,6 @@ bool Parser::rUnaryExpr(exprt &exp) return rSizeofExpr(exp); else if(t==TOK_ALIGNOF) return rAlignofExpr(exp); - else if(t==TOK_THROW) - return rThrowExpr(exp); else if(t==TOK_NOEXCEPT) return rNoexceptExpr(exp); else if(t==TOK_REAL || t==TOK_IMAG) @@ -6032,7 +6083,7 @@ bool Parser::rAlignofExpr(exprt &exp) /* noexcept.expr - : NOEXCEPT '(' expression ')' + : NOEXCEPT '(' comma.expression ')' */ bool Parser::rNoexceptExpr(exprt &exp) { @@ -6046,29 +6097,24 @@ bool Parser::rNoexceptExpr(exprt &exp) if(lex.get_token(tk)!=TOK_NOEXCEPT) return false; - if(lex.LookAhead(0)=='(') - { - exprt subexp; - cpp_tokent op, cp; + if(lex.LookAhead(0)!='(') + return false; - lex.get_token(op); + exprt subexp; + cpp_tokent op, cp; - if(rExpression(subexp, false)) - { - if(lex.get_token(cp)==')') - { - // TODO - exp=exprt(ID_noexcept); - exp.add_to_operands(std::move(subexp)); - set_location(exp, tk); - return true; - } - } - } - else - return true; + lex.get_token(op); - return false; + if(!rCommaExpression(subexp)) + return false; + + if(lex.get_token(cp)!=')') + return false; + + exp=exprt(ID_noexcept); + exp.add_to_operands(std::move(subexp)); + set_location(exp, tk); + return true; } bool Parser::isAllocateExpr(int t) @@ -6081,7 +6127,7 @@ bool Parser::isAllocateExpr(int t) /* allocate.expr - : {Scope | userdef.keyword} NEW allocate.type + : {Scope} NEW allocate.type | {Scope} DELETE {'[' ']'} cast.expr */ bool Parser::rAllocateExpr(exprt &exp) @@ -6342,21 +6388,26 @@ bool Parser::rAllocateInitializer(exprt &init) return true; } +static bool isCppCastExpr(int t) +{ + return t == TOK_DYNAMIC_CAST || t == TOK_STATIC_CAST || t == TOK_REINTERPRET_CAST || t == TOK_CONST_CAST; +} + /* - postfix.exp - : primary.exp + postfix.expr + : primary.expr | postfix.expr '[' comma.expression ']' + | postfix.expr '[' initializer.expr ']' | postfix.expr '(' function.arguments ')' + | integral.or.class.spec '(' function.arguments ')' + | integral.or.class.spec initializer.expr + | postfix.expr '.' userdef.statement + | postfix.expr ArrowOp userdef.statement | postfix.expr '.' var.name | postfix.expr ArrowOp var.name | postfix.expr IncOp - | openc++.postfix.expr - - openc++.postfix.expr - : postfix.expr '.' userdef.statement - | postfix.expr ArrowOp userdef.statement - - Note: function-style casts are accepted as function calls. + | c++cast.expr + | typeid.expr */ bool Parser::rPostfixExpr(exprt &exp) { @@ -6365,8 +6416,102 @@ bool Parser::rPostfixExpr(exprt &exp) std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 0\n"; #endif - if(!rPrimaryExpr(exp)) - return false; + typet type; + + cpp_token_buffert::post pos=lex.Save(); + + if(isCppCastExpr(lex.LookAhead(0))) + { + if(!rCppCastExpr(exp)) + return false; + } + else if(lex.LookAhead(0) == TOK_TYPEID) + { + if(!rTypeidExpr(exp)) + return false; + } + // try to see whether this is explicit type conversion, else it has to be + // a primary-expression + else if(optIntegralTypeOrClassSpec(type) && + type.is_not_nil() && + (lex.LookAhead(0) == '(' || lex.LookAhead(0) == '{')) + { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 0.1\n"; +#endif + + cpp_tokent tk; + lex.LookAhead(0, tk); + exprt exp2; + if(tk.kind == '{') + { + if(!rInitializeExpr(exp2)) + return false; + } + else + { + // tk.kind == '(' + lex.get_token(tk); + + if(!rFunctionArguments(exp2)) + return false; + + cpp_tokent tk2; + if(lex.get_token(tk2)!=')') + return false; + } + + exp=exprt("explicit-constructor-call"); + exp.type().swap(type); + exp.operands().swap(exp2.operands()); + set_location(exp, tk); + } + else + { + lex.Restore(pos); + + exprt type_or_function_name; + if(rName(type_or_function_name) && + (lex.LookAhead(0) == '(' || lex.LookAhead(0) == '{')) + { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 0.2\n"; +#endif + + cpp_tokent tk; + lex.LookAhead(0, tk); + exprt exp2; + if(lex.LookAhead(0)=='{') + { + if(!rInitializeExpr(exp2)) + return false; + } + else + { + // lex.LookAhead(0)=='(' + lex.get_token(tk); + + if(!rFunctionArguments(exp2)) + return false; + + cpp_tokent tk2; + if(lex.get_token(tk2)!=')') + return false; + } + + side_effect_expr_function_callt fc( + std::move(type_or_function_name), exp2.operands(), typet{}, source_locationt{}); + set_location(fc, tk); + + exp.swap(fc); + } + else + { + lex.Restore(pos); + if(!rPrimaryExpr(exp)) + return false; + } + } #ifdef DEBUG std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 1\n"; @@ -6382,7 +6527,14 @@ bool Parser::rPostfixExpr(exprt &exp) { case '[': lex.get_token(op); - if(!rCommaExpression(e)) + + if(lex.LookAhead(0) == '{') + { + // C++11 initialisation expression + if(!rInitializeExpr(e)) + return false; + } + else if(!rCommaExpression(e)) return false; #ifdef DEBUG @@ -6403,11 +6555,11 @@ bool Parser::rPostfixExpr(exprt &exp) break; case '(': + lex.get_token(op); #ifdef DEBUG std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 3\n"; #endif - lex.get_token(op); if(!rFunctionArguments(e)) return false; @@ -6491,6 +6643,48 @@ bool Parser::rPostfixExpr(exprt &exp) } } +/* + c++cast.expr + : castOp '<' type.name '>' '(' comma.expression ')' +*/ +bool Parser::rCppCastExpr(exprt &expr) +{ + cpp_tokent tk; + + lex.get_token(tk); + + expr.id(irep_idt(tk.text)); + set_location(expr, tk); + + if(!isCppCastExpr(tk.kind)) + return false; + + if(lex.get_token(tk) != '<') + return false; + + typet tname; + if(!rTypeName(tname)) + return false; + + if(lex.get_token(tk) != '>') + return false; + + if(lex.get_token(tk) != '(') + return false; + + exprt op; + if(!rCommaExpression(op)) + return false; + + if(lex.get_token(tk) != ')') + return false; + + expr.type().swap(tname); + expr.add_to_operands(std::move(op)); + + return true; +} + /* __uuidof( expression ) __uuidof( type ) @@ -6701,9 +6895,6 @@ bool Parser::rTypePredicate(exprt &expr) | THIS | var.name | '(' comma.expression ')' - | integral.or.class.spec '(' function.arguments ')' - | integral.or.class.spec initializer - | typeid.expr | true | false | nullptr @@ -6820,15 +7011,6 @@ bool Parser::rPrimaryExpr(exprt &exp) #endif return true; - case '{': // C++11 initialisation expression -#ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 10\n"; -#endif - return rInitializeExpr(exp); - - case TOK_TYPEID: - return rTypeidExpr(exp); - case TOK_UNARY_TYPE_PREDICATE: case TOK_BINARY_TYPE_PREDICATE: #ifdef DEBUG @@ -6855,74 +7037,16 @@ bool Parser::rPrimaryExpr(exprt &exp) #ifdef DEBUG std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 14\n"; #endif - { - typet type; - - if(!optIntegralTypeOrClassSpec(type)) - return false; - -#ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 15\n"; -#endif - - if(type.is_not_nil() && lex.LookAhead(0)==TOK_SCOPE) - { - lex.get_token(tk); - lex.get_token(tk); - - // TODO - } - else if(type.is_not_nil()) - { -#ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 16\n"; -#endif - if(lex.LookAhead(0)=='{') - { - lex.LookAhead(0, tk); - - exprt exp2; - if(!rInitializeExpr(exp2)) - return false; - - exp=exprt("explicit-constructor-call"); - exp.type().swap(type); - exp.add_to_operands(std::move(exp2)); - set_location(exp, tk); - } - else if(lex.LookAhead(0)=='(') - { - lex.get_token(tk); - - exprt exp2; - if(!rFunctionArguments(exp2)) - return false; - - if(lex.get_token(tk2)!=')') - return false; - - exp=exprt("explicit-constructor-call"); - exp.type().swap(type); - exp.operands().swap(exp2.operands()); - set_location(exp, tk); - } - else - return false; - } - else - { - if(!rVarName(exp)) - return false; + if(!rVarName(exp)) + return false; - if(lex.LookAhead(0)==TOK_SCOPE) - { - lex.get_token(tk); + if(lex.LookAhead(0)==TOK_SCOPE) + { + lex.get_token(tk); - // exp=new PtreeStaticUserStatementExpr(exp, - // Ptree::Cons(new Leaf(tk), exp2)); - // TODO - } - } + // exp=new PtreeStaticUserStatementExpr(exp, + // Ptree::Cons(new Leaf(tk), exp2)); + // TODO } #ifdef DEBUG std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 17\n"; @@ -7389,6 +7513,14 @@ std::optional Parser::rStatement() #endif lex.get_token(tk2); } + else if(lex.LookAhead(0) == '{') + { + if(!rInitializeExpr(statement.return_value())) + return {}; + + if(lex.get_token(tk2)!=';') + return {}; + } else { #ifdef DEBUG From e5094027d809007aaf9448124b3a2ed165ecc792 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 9 Feb 2025 15:30:53 +0100 Subject: [PATCH 06/12] Reapply "DEBUG" This reverts commit ce919cfb2176716a66a8124c9022464476798081. --- src/cpp/parse.cpp | 90 +++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 88 insertions(+), 2 deletions(-) diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index a0cdb418139..e72f314bbdf 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_member_spec.h" #include "cpp_enum_type.h" +#define DEBUG #ifdef DEBUG #include @@ -1031,6 +1032,11 @@ bool Parser::rLinkageBody(cpp_linkage_spect::itemst &items) */ bool Parser::rTemplateDecl(cpp_declarationt &decl) { +#ifdef DEBUG + indenter _i; + std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl 1\n"; +#endif + TemplateDeclKind kind=tdk_unknown; make_sub_scope("#template", new_scopet::kindt::TEMPLATE); @@ -1040,6 +1046,10 @@ bool Parser::rTemplateDecl(cpp_declarationt &decl) if(!rTemplateDecl2(template_type, kind)) return false; +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl 2\n"; +#endif + cpp_declarationt body; if(lex.LookAhead(0)==TOK_USING) { @@ -1087,11 +1097,20 @@ bool Parser::rTemplateDecl(cpp_declarationt &decl) bool Parser::rTemplateDecl2(typet &decl, TemplateDeclKind &kind) { +#ifdef DEBUG + indenter _i; + std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 1\n"; +#endif + cpp_tokent tk; if(lex.get_token(tk)!=TOK_TEMPLATE) return false; +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 2\n"; +#endif + decl=typet(ID_template); set_location(decl, tk); @@ -1102,17 +1121,33 @@ bool Parser::rTemplateDecl2(typet &decl, TemplateDeclKind &kind) return true; // ignore TEMPLATE } +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 3\n"; +#endif + if(lex.get_token(tk)!='<') return false; irept &template_parameters=decl.add(ID_template_parameters); +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 4\n"; +#endif + if(!rTempArgList(template_parameters)) return false; +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 5\n"; +#endif + if(lex.get_token(tk)!='>') return false; +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 6\n"; +#endif + // ignore nested TEMPLATE while(lex.LookAhead(0)==TOK_TEMPLATE) { @@ -1129,6 +1164,10 @@ bool Parser::rTemplateDecl2(typet &decl, TemplateDeclKind &kind) return false; } +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTemplateDecl2 7\n"; +#endif + if(template_parameters.get_sub().empty()) // template < > declaration kind=tdk_specialization; @@ -1189,6 +1228,10 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration) if((t0==TOK_CLASS || t0==TOK_TYPENAME)) { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.1\n"; +#endif + cpp_token_buffert::post pos=lex.Save(); cpp_tokent tk1; @@ -1228,6 +1271,10 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration) if(lex.LookAhead(0)=='=') { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.2\n"; +#endif + if(declarator.get_has_ellipsis()) return false; @@ -1240,10 +1287,38 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration) declarator.value()=exprt(ID_type); declarator.value().type().swap(default_type); } +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.3\n"; +#endif if(lex.LookAhead(0)==',' || lex.LookAhead(0)=='>') return true; +#if 0 + else if(lex.LookAhead(0) == TOK_SHIFTRIGHT) + { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.4\n"; +#endif + + // turn >> into > > + cpp_token_buffert::post pos=lex.Save(); + cpp_tokent tk; + lex.get_token(tk); + lex.Restore(pos); + tk.kind='>'; + tk.text='>'; + lex.Replace(tk); + lex.Insert(tk); + DATA_INVARIANT(lex.LookAhead(0) == '>', "should be >"); + DATA_INVARIANT(lex.LookAhead(1) == '>', "should be >"); + return true; + } +#endif +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTempArgDeclaration 0.5\n"; +#endif + lex.Restore(pos); } @@ -3969,7 +4044,8 @@ bool Parser::rTemplateArgs(irept &template_args) ) { #ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4\n"; + std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4 " << + lex.LookAhead(0) << "\n"; #endif // ok @@ -3981,20 +4057,30 @@ bool Parser::rTemplateArgs(irept &template_args) lex.Restore(pos); exprt tmp; if(rConditionalExpr(tmp, true)) + { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4.0\n"; +#endif exp.id(ID_ambiguous); + } #ifdef DEBUG std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4.1\n"; #endif lex.Restore(pos); rTypeNameOrFunctionType(a); +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4.1a " << + lex.LookAhead(0) << "\n"; +#endif if(lex.LookAhead(0)==TOK_ELLIPSIS) { lex.get_token(tk1); exp.set(ID_ellipsis, true); } #ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4.2\n"; + std::cout << std::string(__indent, ' ') << "Parser::rTemplateArgs 4.2 " << + lex.LookAhead(0) << "\n"; #endif } else From 83c69c68f03b545d13c55eb377136845fd369803 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 9 Feb 2025 15:44:54 +0100 Subject: [PATCH 07/12] fixup! C++ front-end: parse template parameter packs --- src/cpp/parse.cpp | 31 +++++++++++++++++++++++++------ 1 file changed, 25 insertions(+), 6 deletions(-) diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index e72f314bbdf..ea2e0e91760 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -1215,7 +1215,7 @@ bool Parser::rTempArgList(irept &args) : CLASS [Identifier] {'=' type.name} | CLASS Ellipsis [Identifier] | type.specifier arg.declarator {'=' conditional.expr} - | template.decl2 CLASS Identifier {'=' type.name} + | template.decl2 CLASS {Identifier {'=' type.name}} */ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration) { @@ -1340,9 +1340,14 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration) cpp_tokent tk1, tk2; - if(lex.get_token(tk1) != TOK_CLASS || !is_identifier(lex.get_token(tk2))) + if(lex.get_token(tk1) != TOK_CLASS) return false; + if(lex.LookAhead(0) == ',') + return true; + + if(!is_identifier(lex.get_token(tk2))) + return false; // Ptree cspec=new PtreeClassSpec(new LeafReserved(tk1), // Ptree::Cons(new Leaf(tk2),nil), // nil); @@ -3144,6 +3149,13 @@ bool Parser::rDeclarator( if(!rDeclaratorQualifier()) return false; + if(lex.LookAhead(0)==TOK_ELLIPSIS) + { + cpp_tokent tk; + lex.get_token(tk); + d_outer.set(ID_ellipsis, true); + } + #ifdef DEBUG std::cout << std::string(__indent, ' ') << "Parser::rDeclarator2 2\n"; #endif @@ -4095,6 +4107,12 @@ bool Parser::rTemplateArgs(irept &template_args) if(!rConditionalExpr(exp, true)) return false; + + if(lex.LookAhead(0)==TOK_ELLIPSIS) + { + lex.get_token(tk1); + exp.set(ID_ellipsis, true); + } } #ifdef DEBUG @@ -4208,14 +4226,15 @@ bool Parser::rArgDeclList(irept &arglist) list.get_sub().push_back(irept(irep_idt())); list.get_sub().back().swap(declaration); - t=lex.LookAhead(0); - if(t==',') - lex.get_token(tk); - else if(t==TOK_ELLIPSIS) + if(lex.LookAhead(0)==TOK_ELLIPSIS) { lex.get_token(tk); list.get_sub().push_back(irept(ID_ellipsis)); } + + t=lex.LookAhead(0); + if(t==',') + lex.get_token(tk); else if(t!=')' && t!=TOK_ELLIPSIS) return false; } From a29b9522408d285855166fa85f226436db95cf38 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 9 Feb 2025 17:43:44 +0100 Subject: [PATCH 08/12] More DEBUG --- src/cpp/cpp_token_buffer.h | 5 +++ src/cpp/parse.cpp | 92 ++++++++++++++++++++++++++++++++++---- 2 files changed, 88 insertions(+), 9 deletions(-) diff --git a/src/cpp/cpp_token_buffer.h b/src/cpp/cpp_token_buffer.h index 0721c85878d..6e0ddc5ff4c 100644 --- a/src/cpp/cpp_token_buffer.h +++ b/src/cpp/cpp_token_buffer.h @@ -49,6 +49,11 @@ class cpp_token_buffert void Restore(post pos); void Replace(const cpp_tokent &token); void Insert(const cpp_tokent &token); + const cpp_tokent &peek() + { + PRECONDITION(current_pos <= token_vector.size()); + return *token_vector[current_pos]; + } void clear() { diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index ea2e0e91760..f0125f9c7c7 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -23,7 +23,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_member_spec.h" #include "cpp_enum_type.h" -#define DEBUG +// #define DEBUG #ifdef DEBUG #include @@ -3157,7 +3157,10 @@ bool Parser::rDeclarator( } #ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rDeclarator2 2\n"; + std::cout << std::string(__indent, ' ') << "Parser::rDeclarator2 2 " + << lex.LookAhead(0) + << ' ' << lex.peek().text + << '\n'; #endif t=lex.LookAhead(0); @@ -3621,7 +3624,11 @@ bool Parser::rName(irept &name) { #ifdef DEBUG indenter _i; - std::cout << std::string(__indent, ' ') << "Parser::rName 0\n"; + std::cout << std::string(__indent, ' ') << "Parser::rName 0 " + << lex.LookAhead(0) + << ' ' << lex.peek().text + << ' ' << lex.Save() + << '\n'; #endif name=cpp_namet(); @@ -4167,9 +4174,20 @@ bool Parser::rArgDeclListOrInit( bool &is_args, bool maybe_init) { +#ifdef DEBUG + indenter _i; + std::cout << std::string(__indent, ' ') << "Parser::rArgDeclListOrInit 0 " + << lex.LookAhead(0) + << ' ' << lex.peek().text + << '\n'; +#endif + cpp_token_buffert::post pos=lex.Save(); if(maybe_init) { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rArgDeclListOrInit 1" << std::endl; +#endif if(rFunctionArguments(arglist)) if(lex.LookAhead(0)==')') { @@ -4183,12 +4201,18 @@ bool Parser::rArgDeclListOrInit( } else { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rArgDeclListOrInit 2" << std::endl; +#endif is_args = rArgDeclList(arglist); if(is_args) return true; else { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rArgDeclListOrInit 3" << std::endl; +#endif lex.Restore(pos); // encode.Clear(); return rFunctionArguments(arglist); @@ -4203,11 +4227,22 @@ bool Parser::rArgDeclListOrInit( */ bool Parser::rArgDeclList(irept &arglist) { +#ifdef DEBUG + indenter _i; + std::cout << std::string(__indent, ' ') << "Parser::rArgDeclList 0 " + << lex.LookAhead(0) + << ' ' << lex.peek().text + << '\n'; +#endif + irept list; list.clear(); for(;;) { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rArgDeclList 1" << std::endl; +#endif cpp_declarationt declaration; int t=lex.LookAhead(0); @@ -4215,6 +4250,9 @@ bool Parser::rArgDeclList(irept &arglist) break; else if(t==TOK_ELLIPSIS) { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rArgDeclList 2" << std::endl; +#endif cpp_tokent tk; lex.get_token(tk); list.get_sub().push_back(irept(ID_ellipsis)); @@ -4222,6 +4260,12 @@ bool Parser::rArgDeclList(irept &arglist) } else if(rArgDeclaration(declaration)) { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rArgDeclList 3 " + << lex.LookAhead(0) + << ' ' << lex.peek().text + << '\n'; +#endif cpp_tokent tk; list.get_sub().push_back(irept(irep_idt())); @@ -4306,7 +4350,7 @@ bool Parser::rInitializeExpr(exprt &expr) indenter _i; std::cout << std::string(__indent, ' ') << "Parser::rInitializeExpr 0 " << lex.LookAhead(0) - << ' ' << lex.current_token().text + << ' ' << lex.peek().text << '\n'; #endif @@ -4402,6 +4446,11 @@ bool Parser::rInitializeExpr(exprt &expr) */ bool Parser::rFunctionArguments(exprt &args) { +#ifdef DEBUG + indenter _i; + std::cout << std::string(__indent, ' ') << "Parser::rFunctionArguments 1\n"; +#endif + exprt exp; cpp_tokent tk; @@ -4411,11 +4460,19 @@ bool Parser::rFunctionArguments(exprt &args) for(;;) { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rFunctionArguments 2\n"; +#endif + if(!rInitializeExpr(exp)) return false; args.add_to_operands(std::move(exp)); +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rFunctionArguments 3\n"; +#endif + if(lex.LookAhead(0)==TOK_ELLIPSIS && (lex.LookAhead(1)==')' || lex.LookAhead(1)==',')) { @@ -5111,7 +5168,10 @@ bool Parser::rLogicalOrExpr(exprt &exp, bool template_args) { #ifdef DEBUG indenter _i; - std::cout << std::string(__indent, ' ') << "Parser::rLogicalOrExpr 0\n"; + std::cout << std::string(__indent, ' ') << "Parser::rLogicalOrExpr 0 " + << lex.LookAhead(0) + << ' ' << lex.peek().text + << '\n'; #endif if(!rLogicalAndExpr(exp, template_args)) @@ -6518,7 +6578,11 @@ bool Parser::rPostfixExpr(exprt &exp) { #ifdef DEBUG indenter _i; - std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 0\n"; + std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 0 " + << lex.LookAhead(0) + << ' ' << lex.peek().text + << ' ' << lex.Save() + << '\n'; #endif typet type; @@ -6574,13 +6638,16 @@ bool Parser::rPostfixExpr(exprt &exp) else { lex.Restore(pos); +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 0.2\n"; +#endif exprt type_or_function_name; if(rName(type_or_function_name) && (lex.LookAhead(0) == '(' || lex.LookAhead(0) == '{')) { #ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 0.2\n"; + std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 0.3\n"; #endif cpp_tokent tk; @@ -6612,6 +6679,9 @@ bool Parser::rPostfixExpr(exprt &exp) } else { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rPostfixExpr 0.4\n"; +#endif lex.Restore(pos); if(!rPrimaryExpr(exp)) return false; @@ -7011,7 +7081,7 @@ bool Parser::rPrimaryExpr(exprt &exp) #ifdef DEBUG indenter _i; std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 0 " - << lex.LookAhead(0) << ' ' << lex.current_token().text << '\n'; + << lex.LookAhead(0) << ' ' << lex.peek().text << '\n'; #endif switch(lex.LookAhead(0)) @@ -7175,7 +7245,11 @@ bool Parser::rVarName(exprt &name) { #ifdef DEBUG indenter _i; - std::cout << std::string(__indent, ' ') << "Parser::rVarName 0\n"; + std::cout << std::string(__indent, ' ') << "Parser::rVarName 0 " + << lex.LookAhead(0) + << ' ' << lex.peek().text + << ' ' << lex.Save() + << '\n'; #endif if(rVarNameCore(name)) From 9f2759129a10115ff28e22b46c1d74094d4ba691 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 9 Feb 2025 19:04:18 +0100 Subject: [PATCH 09/12] Fix decltype(X)::member parsing --- src/cpp/parse.cpp | 64 +++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 56 insertions(+), 8 deletions(-) diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index f0125f9c7c7..7ca7a417b32 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -3750,6 +3750,34 @@ bool Parser::rName(irept &name) return true; break; + case TOK_DECLTYPE: +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rName 9\n"; +#endif + lex.get_token(tk); + { + components.push_back(typet{ID_decltype}); + set_location(components.back(), tk); + + if(lex.get_token(tk)!='(') + return false; + + // the argument is always an expression + + exprt expr; + if(!rCommaExpression(expr)) + return false; + + if(lex.get_token(tk)!=')') + return false; + + components.back().add(ID_expr_arg).swap(expr); + + if(lex.LookAhead(0) != TOK_SCOPE) + return false; + } + break; + default: return false; } @@ -7215,14 +7243,6 @@ bool Parser::rPrimaryExpr(exprt &exp) if(!rVarName(exp)) return false; - if(lex.LookAhead(0)==TOK_SCOPE) - { - lex.get_token(tk); - - // exp=new PtreeStaticUserStatementExpr(exp, - // Ptree::Cons(new Leaf(tk), exp2)); - // TODO - } #ifdef DEBUG std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 17\n"; #endif @@ -7385,6 +7405,34 @@ bool Parser::rVarNameCore(exprt &name) } return true; + case TOK_DECLTYPE: +#ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rVarNameCore 8\n"; +#endif + lex.get_token(tk); + { + components.push_back(typet{ID_decltype}); + set_location(components.back(), tk); + + if(lex.get_token(tk)!='(') + return false; + + // the argument is always an expression + + exprt expr; + if(!rCommaExpression(expr)) + return false; + + if(lex.get_token(tk)!=')') + return false; + + components.back().add(ID_expr_arg).swap(expr); + + if(lex.LookAhead(0) != TOK_SCOPE) + return false; + } + break; + default: return false; } From 111319ebac569ece1d3493085c1e1be436d2093b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 9 Feb 2025 19:16:55 +0100 Subject: [PATCH 10/12] fixup! fixup! C++ front-end: parse template parameter packs --- src/cpp/parse.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 7ca7a417b32..abbeeab0b00 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -3149,7 +3149,7 @@ bool Parser::rDeclarator( if(!rDeclaratorQualifier()) return false; - if(lex.LookAhead(0)==TOK_ELLIPSIS) + if(lex.LookAhead(0)==TOK_ELLIPSIS && lex.LookAhead(1)!=')') { cpp_tokent tk; lex.get_token(tk); From 2d70182182fb45b393631a874958ba9c9701ec2e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 9 Feb 2025 19:59:57 +0100 Subject: [PATCH 11/12] C++ front-end: enum attributes and multiple attributes Clang's standard library includes enum member attributes and uses of `__attribute__((...)) __attribute__((...))` rather than combining multiple attributes via a comma between them. --- src/cpp/parse.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index abbeeab0b00..fee2bf923d7 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -2458,7 +2458,7 @@ bool Parser::rGCCAttribute(typet &t) bool Parser::optAttribute(typet &t) { - if(lex.LookAhead(0) == TOK_GCC_ATTRIBUTE) + while(lex.LookAhead(0) == TOK_GCC_ATTRIBUTE) { lex.get_token(); @@ -4627,6 +4627,10 @@ bool Parser::rEnumBody(irept &body) set_location(n, tk); n.set(ID_name, tk.data.get(ID_C_base_name)); + typet discarded_attribute; + if(!optAttribute(discarded_attribute)) + return false; + if(lex.LookAhead(0, tk2)=='=') // set the constant { lex.get_token(tk2); // read the '=' From 2824885c9d7d95391b48e445a9c1ab703dd8174b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 9 Feb 2025 21:57:56 +0100 Subject: [PATCH 12/12] C++ front-end: various fixes and DEBUG --- src/ansi-c/scanner.l | 2 +- src/cpp/cpp_typecheck_template.cpp | 4 +++ src/cpp/parse.cpp | 56 ++++++++++++++++++++++++++++-- 3 files changed, 58 insertions(+), 4 deletions(-) diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index b02a0111339..10a3bde914c 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -1458,7 +1458,7 @@ __decltype { if(PARSER.cpp98 && "_Atomic"{ws}"(" { // put back all but _Atomic yyless(7); - if(!PARSER.cpp98 && + if((!PARSER.cpp98 || PARSER.cpp11) && (PARSER.mode==configt::ansi_ct::flavourt::GCC || PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM)) diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp index 6dfcd4a05e2..4e9b276685a 100644 --- a/src/cpp/cpp_typecheck_template.cpp +++ b/src/cpp/cpp_typecheck_template.cpp @@ -20,6 +20,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_type2name.h" #include "cpp_typecheck.h" +#include + void cpp_typecheckt::salvage_default_arguments( const template_typet &old_type, template_typet &new_type) @@ -714,6 +716,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters( // put template parameters into this scope template_typet::template_parameterst ¶meters= type.template_parameters(); + std::cerr << type.pretty() << std::endl; unsigned anon_count=0; @@ -730,6 +733,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters( cpp_declarator_convertert cpp_declarator_converter(*this); // there must be _one_ declarator + std::cerr << declaration.pretty() << std::endl; PRECONDITION(declaration.declarators().size() == 1); cpp_declaratort &declarator=declaration.declarators().front(); diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index fee2bf923d7..c60d83537bd 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -778,7 +778,7 @@ bool Parser::isTypeSpecifier() t == TOK_CPROVER_BOOL || t == TOK_CLASS || t == TOK_STRUCT || t == TOK_UNION || t == TOK_ENUM || t == TOK_INTERFACE || t == TOK_TYPENAME || t == TOK_TYPEOF || t == TOK_DECLTYPE || - t == TOK_UNDERLYING_TYPE; + t == TOK_UNDERLYING_TYPE || t == TOK_ATOMIC_TYPE_SPECIFIER; } /* @@ -1343,7 +1343,7 @@ bool Parser::rTempArgDeclaration(cpp_declarationt &declaration) if(lex.get_token(tk1) != TOK_CLASS) return false; - if(lex.LookAhead(0) == ',') + if(lex.LookAhead(0) == ',' || lex.LookAhead(0) == '>') return true; if(!is_identifier(lex.get_token(tk2))) @@ -2502,6 +2502,17 @@ bool Parser::optAttribute(typet &t) break; } + case TOK_GCC_IDENTIFIER: + if(tk.text == "clang" && lex.LookAhead(0) == TOK_SCOPE) + { + exprt discarded; + if(!rExpression(discarded, false)) + return false; + } + else + return false; + break; + default: // TODO: way may wish to change this: GCC, Clang, Visual Studio merely // warn when they see an attribute that they don't recognize @@ -2737,8 +2748,34 @@ bool Parser::optIntegralTypeOrClassSpec(typet &p) return true; } + else if(t == TOK_ATOMIC_TYPE_SPECIFIER) + { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') + << "Parser::optIntegralTypeOrClassSpec 9\n"; +#endif // DEBUG + cpp_tokent atomic_tk; + lex.get_token(atomic_tk); + + cpp_tokent tk; + if(lex.get_token(tk)!='(') + return false; + + // the argument is always a type + if(!rTypeSpecifier(p, false)) + return false; + + if(lex.get_token(tk)!=')') + return false; + + return true; + } else { +#ifdef DEBUG + std::cout << std::string(__indent, ' ') + << "Parser::optIntegralTypeOrClassSpec 10\n"; +#endif // DEBUG p.make_nil(); return true; } @@ -4549,6 +4586,9 @@ bool Parser::rEnumSpec(typet &spec) spec.set(ID_C_class, true); } + if(!optAttribute(spec)) + return false; + if(lex.LookAhead(0)!='{' && lex.LookAhead(0)!=':') { @@ -7903,7 +7943,9 @@ std::optional Parser::rStatement() if(!rUsing(cpp_using)) return {}; - UNIMPLEMENTED; + codet statement(ID_cpp_using); + // UNIMPLEMENTED; + return std::move(statement); } case TOK_STATIC_ASSERT: @@ -7920,6 +7962,14 @@ std::optional Parser::rStatement() return std::move(statement); } + case '[': + { + typet discard; + if(!optAttribute(discard)) + return {}; + return code_blockt{}; + } + default: return rExprStatement(); }