From fde09cad47460accf4d704abf07429588ac036f4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 20 Aug 2017 17:01:02 +0100 Subject: [PATCH 1/7] C++ front-end: parse GCC attributes --- src/ansi-c/scanner.l | 11 +- src/cpp/cpp_typecheck_type.cpp | 4 + src/cpp/parse.cpp | 194 +++++++++++++++++++++++++++++++-- 3 files changed, 194 insertions(+), 15 deletions(-) diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 29e5da340e7..ec8991f543f 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -938,14 +938,9 @@ __decltype { if(PARSER.cpp98 && PARSER.mode==configt::ansi_ct::flavourt::CODEWARRIOR || PARSER.mode==configt::ansi_ct::flavourt::ARM) { - if(PARSER.cpp98) - BEGIN(IGNORE_PARENS); - else - { - BEGIN(GCC_ATTRIBUTE1); - loc(); - return TOK_GCC_ATTRIBUTE; - } + BEGIN(GCC_ATTRIBUTE1); + loc(); + return TOK_GCC_ATTRIBUTE; } else return make_identifier(); diff --git a/src/cpp/cpp_typecheck_type.cpp b/src/cpp/cpp_typecheck_type.cpp index 8c94f0dbb27..1beac5ebd1d 100644 --- a/src/cpp/cpp_typecheck_type.cpp +++ b/src/cpp/cpp_typecheck_type.cpp @@ -140,6 +140,10 @@ void cpp_typecheckt::typecheck_type(typet &type) if(type.subtype().get_bool(ID_C_volatile)) type.set(ID_C_volatile, true); } + else if(type.id()==ID_vector) + { + typecheck_vector_type(to_vector_type(type)); + } else if(type.id()==ID_code) { code_typet &code_type=to_code_type(type); diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 7246108160f..eb58cdcddb0 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -276,7 +276,7 @@ class Parser // NOLINT(readability/identifiers) bool optStorageSpec(cpp_storage_spect &); bool optCvQualify(typet &); bool optAlignas(typet &); - bool rAttribute(); + bool rAttribute(typet &); bool optAttribute(cpp_declarationt &); bool optIntegralTypeOrClassSpec(typet &); bool rConstructorDecl( @@ -473,8 +473,10 @@ void Parser::merge_types(const typet &src, typet &dest) { if(dest.id()!=ID_merged_type) { + source_locationt location=dest.source_location(); typet tmp(ID_merged_type); tmp.move_to_subtypes(dest); + tmp.add_source_location()=location; dest=tmp; } @@ -2044,7 +2046,7 @@ bool Parser::optCvQualify(typet &cv) break; case TOK_GCC_ATTRIBUTE: - if(!rAttribute()) + if(!rAttribute(cv)) return false; break; @@ -2103,28 +2105,204 @@ bool Parser::optAlignas(typet &cv) return true; } -bool Parser::rAttribute() +bool Parser::rAttribute(typet &t) { + #ifdef DEBUG + indenter _i; + std::cout << std::string(__indent, ' ') << "Parser::rAttribute " + << lex.LookAhead(0); + #endif cpp_tokent tk; lex.get_token(tk); switch(tk.kind) { case '(': - rAttribute(); + if(lex.LookAhead(0)!=')') + rAttribute(t); + if(lex.LookAhead(0)!=')') return false; lex.get_token(tk); - break; + return true; - case TOK_IDENTIFIER: + case TOK_GCC_ATTRIBUTE_PACKED: + { + typet attr(ID_packed); + set_location(attr, tk); + merge_types(attr, t); + break; + } + + case TOK_GCC_ATTRIBUTE_TRANSPARENT_UNION: + { + typet attr(ID_transparent_union); + set_location(attr, tk); + merge_types(attr, t); + break; + } + + case TOK_GCC_ATTRIBUTE_VECTOR_SIZE: + { + cpp_tokent tk2, tk3; + + if(lex.get_token(tk2)!='(') + return false; + + exprt exp; + if(!rCommaExpression(exp)) + return false; + + if(lex.get_token(tk3)!=')') + return false; + + vector_typet attr(nil_typet(), exp); + attr.add_source_location()=exp.source_location(); + merge_types(attr, t); + break; + } + + case TOK_GCC_ATTRIBUTE_ALIGNED: + { + typet attr(ID_aligned); + set_location(attr, tk); + + if(lex.LookAhead(0)=='(') + { + cpp_tokent tk2, tk3; + + if(lex.get_token(tk2)!='(') + return false; + + exprt exp; + if(!rCommaExpression(exp)) + return false; + + if(lex.get_token(tk3)!=')') + return false; + + attr.add(ID_size, exp); + } + + merge_types(attr, t); + break; + } + + case TOK_GCC_ATTRIBUTE_MODE: + { + cpp_tokent tk2, tk3; + + if(lex.get_token(tk2)!='(') + return false; + + irept name; + if(!rName(name)) + return false; + + if(lex.get_token(tk3)!=')') + return false; + + typet attr(ID_gcc_attribute_mode); + set_location(attr, tk); + attr.set(ID_size, name.get(ID_identifier)); + merge_types(attr, t); + break; + } + + case TOK_GCC_ATTRIBUTE_GNU_INLINE: + { + typet attr(ID_static); + set_location(attr, tk); + merge_types(attr, t); + break; + } + + case TOK_GCC_ATTRIBUTE_WEAK: + { + typet attr(ID_weak); + set_location(attr, tk); + merge_types(attr, t); + break; + } + + case TOK_GCC_ATTRIBUTE_ALIAS: + { + cpp_tokent tk2, tk3, tk4; + + if(lex.get_token(tk2)!='(') + return false; + + if(!rString(tk3)) + return false; + + if(lex.get_token(tk4)!=')') + return false; + + typet attr(ID_alias); + set_location(attr, tk); + attr.move_to_sub(tk3.data); + merge_types(attr, t); + break; + } + + case TOK_GCC_ATTRIBUTE_SECTION: + { + cpp_tokent tk2, tk3, tk4; + + if(lex.get_token(tk2)!='(') + return false; + + if(!rString(tk3)) + return false; + + if(lex.get_token(tk4)!=')') + return false; + + typet attr(ID_section); + set_location(attr, tk); + attr.move_to_sub(tk3.data); + merge_types(attr, t); + break; + } + + case TOK_GCC_ATTRIBUTE_NORETURN: + { + typet attr(ID_noreturn); + set_location(attr, tk); + merge_types(attr, t); + break; + } + + case TOK_GCC_ATTRIBUTE_CONSTRUCTOR: + { + typet attr(ID_constructor); + set_location(attr, tk); + merge_types(attr, t); + break; + } + + case TOK_GCC_ATTRIBUTE_DESTRUCTOR: + { + typet attr(ID_destructor); + set_location(attr, tk); + merge_types(attr, t); + break; + } + + case ',': + if(lex.LookAhead(0)==')') + // the scanner ignored an attribute + return true; break; default: return false; } - return true; + if(lex.LookAhead(0)==')') + return true; + + return rAttribute(t); } bool Parser::optAttribute(cpp_declarationt &declaration) @@ -2971,6 +3149,8 @@ bool Parser::rDeclarator( break; } + optCvQualify(d_outer); + #ifdef DEBUG std::cout << std::string(__indent, ' ') << "Parser::rDeclarator2 13\n"; #endif From d82f55467472aee582b0ee5a37df1fbb53145ca4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 20 Aug 2017 23:46:12 +0100 Subject: [PATCH 2/7] Permit asm post-declarator mixed in any order with other qualifiers --- src/cpp/parse.cpp | 30 +++++++++++++----------------- 1 file changed, 13 insertions(+), 17 deletions(-) diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index eb58cdcddb0..e21beddd57b 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -2001,7 +2001,7 @@ bool Parser::optCvQualify(typet &cv) 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_ATTRIBUTE || t==TOK_GCC_ASM) { cpp_tokent tk; lex.get_token(tk); @@ -2050,6 +2050,18 @@ bool Parser::optCvQualify(typet &cv) return false; break; + case TOK_GCC_ASM: + // asm post-declarator + // this is stuff like + // int x __asm("asd")=1, y; + if(lex.get_token(tk)!='(') + return false; + if(!rString(tk)) + return false; + if(lex.get_token(tk)!=')') + return false; + break; + default: UNREACHABLE; break; @@ -2816,22 +2828,6 @@ bool Parser::rDeclaratorWithInit( should_be_declarator, is_statement)) return false; - // asm post-declarator - if(lex.LookAhead(0)==TOK_GCC_ASM) - { - // this is stuff like - // int x __asm("asd")=1, y; - cpp_tokent tk; - lex.get_token(tk); // TOK_GCC_ASM - - if(lex.get_token(tk)!='(') - return false; - if(!rString(tk)) - return false; - if(lex.get_token(tk)!=')') - return false; - } - int t=lex.LookAhead(0); if(t=='=') { From d5183fb460c0122087d7e33da06f49e8d59f2f4b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 21 Aug 2017 09:13:56 +0100 Subject: [PATCH 3/7] Permit GCC attributes after struct/class in class declaration --- src/cpp/parse.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index e21beddd57b..213279a97e6 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -4398,6 +4398,16 @@ bool Parser::rClassSpec(typet &spec) { if(!optAlignas(spec)) return false; + + if(lex.LookAhead(0)==TOK_GCC_ATTRIBUTE) + { + cpp_tokent tk; + lex.get_token(tk); + + if(!rAttribute(spec)) + return false; + } + irept name; if(!rName(name)) From 4a47de684166ae34938f1f6731e2c66677ae5d50 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 20 Aug 2017 23:51:55 +0100 Subject: [PATCH 4/7] Mark already-typechecked types as such --- src/cpp/cpp_typecheck_code.cpp | 3 +++ src/cpp/cpp_typecheck_declaration.cpp | 4 ++++ src/cpp/cpp_typecheck_type.cpp | 4 ++++ src/cpp/cpp_util.h | 2 +- 4 files changed, 12 insertions(+), 1 deletion(-) diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp index 21d0fe6aae7..f879edfaf5d 100644 --- a/src/cpp/cpp_typecheck_code.cpp +++ b/src/cpp/cpp_typecheck_code.cpp @@ -384,6 +384,9 @@ void cpp_typecheckt::typecheck_decl(codet &code) return; } + // mark as 'already typechecked' + make_already_typechecked(type); + codet new_code(ID_decl_block); new_code.reserve_operands(declaration.declarators().size()); diff --git a/src/cpp/cpp_typecheck_declaration.cpp b/src/cpp/cpp_typecheck_declaration.cpp index 16bbd081123..10739129156 100644 --- a/src/cpp/cpp_typecheck_declaration.cpp +++ b/src/cpp/cpp_typecheck_declaration.cpp @@ -129,6 +129,10 @@ void cpp_typecheckt::convert_non_template_declaration( if(!is_typedef) elaborate_class_template(declaration_type); + // mark as 'already typechecked' + if(!declaration.declarators().empty()) + make_already_typechecked(declaration_type); + // Special treatment for anonymous unions if(declaration.declarators().empty() && follow(declaration.type()).get_bool(ID_C_is_anonymous)) diff --git a/src/cpp/cpp_typecheck_type.cpp b/src/cpp/cpp_typecheck_type.cpp index 1beac5ebd1d..bab972ae41d 100644 --- a/src/cpp/cpp_typecheck_type.cpp +++ b/src/cpp/cpp_typecheck_type.cpp @@ -260,6 +260,10 @@ void cpp_typecheckt::typecheck_type(typet &type) else if(type.id()==ID_nullptr) { } + else if(type.id()==ID_already_typechecked) + { + c_typecheck_baset::typecheck_type(type); + } else { error().source_location=type.source_location(); diff --git a/src/cpp/cpp_util.h b/src/cpp/cpp_util.h index aeb48be73a2..87a667b3a6a 100644 --- a/src/cpp/cpp_util.h +++ b/src/cpp/cpp_util.h @@ -17,7 +17,7 @@ exprt cpp_symbol_expr(const symbolt &symbol); inline void already_typechecked(irept &irep) { - exprt tmp("already_typechecked"); + exprt tmp(ID_already_typechecked); tmp.copy_to_operands(static_cast(irep)); irep.swap(tmp); } From 999ad1562982854ab4ed4744c9213920247cb06a Mon Sep 17 00:00:00 2001 From: Andreas Tiemeyer Date: Tue, 3 Oct 2017 18:55:38 +0100 Subject: [PATCH 5/7] Swap order of subtypes in construction of merged_type nodes Main type needs to be at the end. Handle and record GCC function attribute noreturn. --- src/cpp/cpp_convert_type.cpp | 8 ++++++-- src/cpp/parse.cpp | 25 ++++++++++++------------- 2 files changed, 18 insertions(+), 15 deletions(-) diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp index 1b7bab029eb..d89a820a7d4 100644 --- a/src/cpp/cpp_convert_type.cpp +++ b/src/cpp/cpp_convert_type.cpp @@ -30,7 +30,7 @@ class cpp_convert_typet unsigned unsigned_cnt, signed_cnt, char_cnt, int_cnt, short_cnt, long_cnt, const_cnt, restrict_cnt, constexpr_cnt, volatile_cnt, double_cnt, float_cnt, complex_cnt, cpp_bool_cnt, proper_bool_cnt, - extern_cnt, wchar_t_cnt, char16_t_cnt, char32_t_cnt, + extern_cnt, noreturn_cnt, wchar_t_cnt, char16_t_cnt, char32_t_cnt, int8_cnt, int16_cnt, int32_cnt, int64_cnt, ptr32_cnt, ptr64_cnt, float128_cnt, int128_cnt; @@ -53,7 +53,7 @@ void cpp_convert_typet::read(const typet &type) unsigned_cnt=signed_cnt=char_cnt=int_cnt=short_cnt= long_cnt=const_cnt=restrict_cnt=constexpr_cnt=volatile_cnt= double_cnt=float_cnt=complex_cnt=cpp_bool_cnt=proper_bool_cnt= - extern_cnt=wchar_t_cnt=char16_t_cnt=char32_t_cnt= + extern_cnt=noreturn_cnt=wchar_t_cnt=char16_t_cnt=char32_t_cnt= int8_cnt=int16_cnt=int32_cnt=int64_cnt= ptr32_cnt=ptr64_cnt=float128_cnt=int128_cnt=0; @@ -132,6 +132,10 @@ void cpp_convert_typet::read_rec(const typet &type) constexpr_cnt++; else if(type.id()==ID_extern) extern_cnt++; + else if(type.id()==ID_noreturn) + { + noreturn_cnt++; + } else if(type.id()==ID_function_type) { read_function_type(type); diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 213279a97e6..f2862c55255 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -480,7 +480,12 @@ void Parser::merge_types(const typet &src, typet &dest) dest=tmp; } - dest.copy_to_subtypes(src); + // the end of the subtypes container needs to stay the same, + // since several analysis functions traverse via the end for + // merged_types + typet::subtypest &sub=dest.subtypes(); + sub.emplace(sub.begin(), src); + POSTCONDITION(!dest.subtypes().empty()); } } @@ -3199,12 +3204,9 @@ bool Parser::optPtrOperator(typet &ptrs) cv.make_nil(); optCvQualify(cv); // the qualifier is for the pointer if(cv.is_not_nil()) - { - merge_types(op, cv); - t_list.push_back(cv); - } - else - t_list.push_back(op); + merge_types(cv, op); + + t_list.push_back(op); } else if(t=='^') { @@ -3218,12 +3220,9 @@ bool Parser::optPtrOperator(typet &ptrs) cv.make_nil(); optCvQualify(cv); // the qualifier is for the pointer if(cv.is_not_nil()) - { - merge_types(op, cv); - t_list.push_back(cv); - } - else - t_list.push_back(op); + merge_types(cv, op); + + t_list.push_back(op); } else if(isPtrToMember(0)) { From e229b4c57c9b3b71f8917236573a4ea0c52bfca6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 21 Aug 2017 00:34:17 +0100 Subject: [PATCH 6/7] Typecheck initializer lists --- regression/cpp/gcc_vector1/main.cpp | 22 ++++++++++++++++++++++ regression/cpp/gcc_vector1/test.desc | 8 ++++++++ src/cpp/cpp_typecheck_expr.cpp | 19 +++++++++++++++++++ 3 files changed, 49 insertions(+) create mode 100644 regression/cpp/gcc_vector1/main.cpp create mode 100644 regression/cpp/gcc_vector1/test.desc diff --git a/regression/cpp/gcc_vector1/main.cpp b/regression/cpp/gcc_vector1/main.cpp new file mode 100644 index 00000000000..d7cb6310718 --- /dev/null +++ b/regression/cpp/gcc_vector1/main.cpp @@ -0,0 +1,22 @@ +#ifdef __GNUC__ + +typedef float __m128 __attribute__ ((__vector_size__ (16), __may_alias__)); + +__m128 setzero(void) +{ + return (__m128){ 0.0f, 0.0f, 0.0f, 0.0f }; +} + +#else + +void setzero() +{ +} + +#endif + +int main(int argc, char* argv[]) +{ + setzero(); + return 0; +} diff --git a/regression/cpp/gcc_vector1/test.desc b/regression/cpp/gcc_vector1/test.desc new file mode 100644 index 00000000000..420aca5252c --- /dev/null +++ b/regression/cpp/gcc_vector1/test.desc @@ -0,0 +1,8 @@ +CORE +main.cpp + +^EXIT=0$ +^SIGNAL=0$ +-- +^CONVERSION ERROR$ +^warning: ignoring diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index 7beeb255b6a..310407853a5 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -939,6 +939,25 @@ void cpp_typecheckt::typecheck_expr_explicit_typecast(exprt &expr) else typecheck_type(expr.type()); + // We allow (TYPE){ initializer_list } + // This is called "compound literal", and is syntactic + // sugar for a (possibly local) declaration. + if(expr.op0().id()==ID_initializer_list) + { + // just do a normal initialization + do_initializer(expr.op0(), expr.type(), false); + + // This produces a struct-expression, + // union-expression, array-expression, + // or an expression for a pointer or scalar. + // We produce a compound_literal expression. + exprt tmp(ID_compound_literal, expr.type()); + tmp.move_to_operands(expr.op0()); + expr=tmp; + expr.set(ID_C_lvalue, true); // these are l-values + return; + } + exprt new_expr; if(const_typecast(expr.op0(), expr.type(), new_expr) || From 1d95ab427f8c497a373e311c95b8e95c36f8c4d3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 8 Jun 2018 22:09:07 +0000 Subject: [PATCH 7/7] Permit compound literals in place of PODs --- regression/cpp/List_initialization1/test.desc | 2 +- src/cpp/cpp_typecheck.h | 2 -- src/cpp/cpp_typecheck_code.cpp | 22 ------------------- src/cpp/cpp_typecheck_conversions.cpp | 7 ++++++ src/cpp/cpp_typecheck_fargs.cpp | 8 +++++++ 5 files changed, 16 insertions(+), 25 deletions(-) diff --git a/regression/cpp/List_initialization1/test.desc b/regression/cpp/List_initialization1/test.desc index 0daa9695017..3862862ffd3 100644 --- a/regression/cpp/List_initialization1/test.desc +++ b/regression/cpp/List_initialization1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.cpp -std=c++11 ^EXIT=0$ diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h index 307a6188fa2..235dca86d0c 100644 --- a/src/cpp/cpp_typecheck.h +++ b/src/cpp/cpp_typecheck.h @@ -483,8 +483,6 @@ class cpp_typecheckt:public c_typecheck_baset void typecheck_method_application( side_effect_expr_function_callt &expr); - void typecheck_assign(codet &code); - public: // // Type Conversions diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp index f879edfaf5d..9af27abfa3e 100644 --- a/src/cpp/cpp_typecheck_code.cpp +++ b/src/cpp/cpp_typecheck_code.cpp @@ -449,25 +449,3 @@ void cpp_typecheckt::typecheck_block(codet &code) c_typecheck_baset::typecheck_block(code); } - -void cpp_typecheckt::typecheck_assign(codet &code) -{ - if(code.operands().size()!=2) - { - error().source_location=code.find_source_location(); - error() << "assignment statement expected to have two operands" - << eom; - throw 0; - } - - // turn into a side effect - side_effect_exprt expr(code.get(ID_statement)); - expr.operands() = code.operands(); - typecheck_expr(expr); - - code_expressiont code_expr; - code_expr.expression()=expr; - code_expr.add_source_location() = code.source_location(); - - code.swap(code_expr); -} diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp index 4eb8eadbbfa..e665265dce3 100644 --- a/src/cpp/cpp_typecheck_conversions.cpp +++ b/src/cpp/cpp_typecheck_conversions.cpp @@ -1508,6 +1508,13 @@ void cpp_typecheckt::implicit_typecast(exprt &expr, const typet &type) { exprt e=expr; + if( + e.id() == ID_initializer_list && cpp_is_pod(type) && + e.operands().size() == 1) + { + e = expr.op0(); + } + if(!implicit_conversion_sequence(e, type, expr)) { show_instantiation_stack(error()); diff --git a/src/cpp/cpp_typecheck_fargs.cpp b/src/cpp/cpp_typecheck_fargs.cpp index 6f6f905c327..623f786b1c7 100644 --- a/src/cpp/cpp_typecheck_fargs.cpp +++ b/src/cpp/cpp_typecheck_fargs.cpp @@ -129,6 +129,14 @@ bool cpp_typecheck_fargst::match( std::cout << "OK " << rank << '\n'; #endif } + else if( + operand.id() == ID_initializer_list && cpp_typecheck.cpp_is_pod(type) && + operand.operands().size() == 1 && + cpp_typecheck.implicit_conversion_sequence( + operand.op0(), type, new_expr, rank)) + { + distance += rank; + } else { #if 0