diff --git a/regression/cbmc-cpp/Constructor7/main.cpp b/regression/cbmc-cpp/Constructor7/main.cpp new file mode 100644 index 00000000000..519705346db --- /dev/null +++ b/regression/cbmc-cpp/Constructor7/main.cpp @@ -0,0 +1,17 @@ +#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..dc89ed5b065 --- /dev/null +++ b/regression/cpp/brace_initializer1/main.cpp @@ -0,0 +1,26 @@ +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 92ce6cae565..1bc02c661b1 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 ac122dd7612..fd491abfe3f 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..13331f678de 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 2685771889c..11e3305c86e 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -126,6 +126,12 @@ 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); } @@ -966,13 +972,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); } } @@ -1274,53 +1275,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(); @@ -1414,21 +1382,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), @@ -1555,14 +1508,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 777f4b2f0bd..0f149737202 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 &); @@ -4224,11 +4225,21 @@ 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); @@ -4306,7 +4317,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 ')'. */ @@ -4321,7 +4332,7 @@ bool Parser::rFunctionArguments(exprt &args) for(;;) { - if(!rExpression(exp, false)) + if(!rInitializeExpr(exp)) return false; args.add_to_operands(std::move(exp)); @@ -4860,7 +4871,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) { @@ -4871,7 +4884,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 @@ -4893,7 +4929,7 @@ bool Parser::rExpression(exprt &exp, bool template_args) #endif exprt right; - if(!rExpression(right, template_args)) + if(!rInitializeExpr(right)) return false; #ifdef DEBUG @@ -4941,7 +4977,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) { @@ -5462,6 +5498,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) { @@ -5499,6 +5536,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; @@ -5742,9 +5793,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) @@ -5824,8 +5875,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) @@ -6057,7 +6106,7 @@ bool Parser::rAlignofExpr(exprt &exp) /* noexcept.expr - : NOEXCEPT '(' expression ')' + : NOEXCEPT '(' comma.expression ')' */ bool Parser::rNoexceptExpr(exprt &exp) { @@ -6071,29 +6120,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) @@ -6106,7 +6150,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) @@ -6367,21 +6411,27 @@ 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) { @@ -6390,8 +6440,106 @@ 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"; @@ -6407,7 +6555,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 @@ -6428,11 +6583,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; @@ -6516,6 +6671,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 ) @@ -6726,9 +6923,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 @@ -6845,15 +7039,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 @@ -6880,74 +7065,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"; @@ -7414,6 +7541,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 diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index f1728411191..3e62b49939e 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -729,7 +729,6 @@ IREP_ID_ONE(is_vtptr) IREP_ID_ONE(prefix) IREP_ID_ONE(cv) IREP_ID_ONE(cpp_dummy_destructor) -IREP_ID_ONE(cast_expression) IREP_ID_ONE(pod_constructor) IREP_ID_ONE(template_decls) IREP_ID_ONE(throw_decl)