From 514db345d1b8cd3f5d31a421bd66bc7fca64c061 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 6 May 2024 20:29:21 +0200 Subject: [PATCH] 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);