diff --git a/regression/ansi-c/asm3/test.desc b/regression/ansi-c/asm3/test.desc index d809adda3df..0e9aada28d3 100644 --- a/regression/ansi-c/asm3/test.desc +++ b/regression/ansi-c/asm3/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c other.c ^EXIT=0$ diff --git a/regression/cbmc/gcc_attribute_alias1/main.c b/regression/cbmc/gcc_attribute_alias1/main.c new file mode 100644 index 00000000000..3e1bf1ebf4b --- /dev/null +++ b/regression/cbmc/gcc_attribute_alias1/main.c @@ -0,0 +1,21 @@ +#include + +int foo(int a) +{ + return a; +} + +// this is a GCC extension + +int bar(int b) __attribute__((alias("foo"))); + +__typeof__(foo) bar2 __attribute__((alias("foo"))); + +int main() +{ + #ifdef __GNUC__ + assert(bar(42)==42); + assert(bar2(42)==42); + #endif + return 0; +} diff --git a/regression/cbmc/gcc_attribute_alias1/test.desc b/regression/cbmc/gcc_attribute_alias1/test.desc new file mode 100644 index 00000000000..466da18b2b5 --- /dev/null +++ b/regression/cbmc/gcc_attribute_alias1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index e6e953ad3b5..3b2f66151c7 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -72,10 +72,11 @@ void ansi_c_convert_typet::read_rec(const typet &type) c_qualifiers.is_ptr64=true; else if(type.id()==ID_volatile) c_qualifiers.is_volatile=true; - else if(type.id()==ID_asm) + else if(type.id()==ID_asm && + type.has_subtype() && + type.subtype().id()==ID_string_constant) { - // These are called 'asm labels' by GCC. - // ignore for now + c_storage_spec.asm_label=type.subtype().get(ID_value); } else if(type.id()==ID_const) c_qualifiers.is_constant=true; @@ -233,6 +234,12 @@ void ansi_c_convert_typet::read_rec(const typet &type) constructor=true; else if(type.id()==ID_destructor) destructor=true; + else if(type.id()==ID_alias && + type.has_subtype() && + type.subtype().id()==ID_string_constant) + { + c_storage_spec.alias=type.subtype().get(ID_value); + } else other.push_back(type); } diff --git a/src/ansi-c/c_storage_spec.cpp b/src/ansi-c/c_storage_spec.cpp index fd8dc27834e..2facbcb7a91 100644 --- a/src/ansi-c/c_storage_spec.cpp +++ b/src/ansi-c/c_storage_spec.cpp @@ -55,4 +55,16 @@ void c_storage_spect::read(const typet &type) if(it->id()==ID_thread) is_thread_local=true; } + else if(type.id()==ID_alias && + type.has_subtype() && + type.subtype().id()==ID_string_constant) + { + alias=type.subtype().get(ID_value); + } + else if(type.id()==ID_asm && + type.has_subtype() && + type.subtype().id()==ID_string_constant) + { + asm_label=type.subtype().get(ID_value); + } } diff --git a/src/ansi-c/c_storage_spec.h b/src/ansi-c/c_storage_spec.h index 6c38d1b503e..b4b40b608a7 100644 --- a/src/ansi-c/c_storage_spec.h +++ b/src/ansi-c/c_storage_spec.h @@ -34,10 +34,18 @@ class c_storage_spect is_register=false; is_inline=false; is_weak=false; + alias.clear(); + asm_label.clear(); } bool is_typedef, is_extern, is_static, is_register, is_inline, is_thread_local, is_weak; + + // __attribute__((alias("foo"))) + irep_idt alias; + + // GCC asm labels __asm__("foo") - these change the symbol name + irep_idt asm_label; friend bool operator == ( const c_storage_spect &a, @@ -49,7 +57,9 @@ class c_storage_spect a.is_register==b.is_register && a.is_thread_local==b.is_thread_local && a.is_inline==b.is_inline && - a.is_weak==b.is_weak; + a.is_weak==b.is_weak && + a.alias==b.alias && + a.asm_label==b.asm_label; } friend bool operator != ( @@ -70,6 +80,8 @@ class c_storage_spect a.is_inline |=b.is_inline; a.is_thread_local |=b.is_thread_local; a.is_weak |=b.is_weak; + if(!b.alias.empty()) a.alias=b.alias; + if(!b.asm_label.empty()) a.asm_label=b.asm_label; return a; } diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 69938e4960b..81c09a9d849 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -193,7 +193,8 @@ void c_typecheck_baset::typecheck_new_symbol(symbolt &symbol) if(symbol.type.id()==ID_code) { - if(symbol.value.is_not_nil()) + if(symbol.value.is_not_nil() && + !symbol.is_macro) typecheck_function_body(symbol); else { @@ -359,7 +360,8 @@ void c_typecheck_baset::typecheck_redefinition_non_type( } // do initializer, this may change the type - if(follow(new_symbol.type).id()!=ID_code) + if(follow(new_symbol.type).id()!=ID_code && + !new_symbol.is_macro) do_initializer(new_symbol); const typet &final_new=follow(new_symbol.type); @@ -462,7 +464,10 @@ void c_typecheck_baset::typecheck_redefinition_non_type( old_symbol.is_weak=true; } - typecheck_function_body(new_symbol); + if(new_symbol.is_macro) + old_symbol.is_macro=true; + else + typecheck_function_body(new_symbol); // overwrite location old_symbol.location=new_symbol.location; @@ -590,6 +595,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type( { old_symbol.value=new_symbol.value; old_symbol.type=new_symbol.type; + old_symbol.is_macro=new_symbol.is_macro; } } @@ -688,6 +694,89 @@ void c_typecheck_baset::typecheck_function_body(symbolt &symbol) /*******************************************************************\ +Function: c_typecheck_baset::apply_asm_label + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void c_typecheck_baset::apply_asm_label( + const irep_idt &asm_label, + symbolt &symbol) +{ + const irep_idt orig_name=symbol.name; + + // restrict renaming to functions and global variables; + // procedure-local ones would require fixing the scope, as we + // do for parameters below + if(!asm_label.empty() && + !symbol.is_type && + (symbol.type.id()==ID_code || symbol.is_static_lifetime)) + { + symbol.name=asm_label; + symbol.base_name=asm_label; + } + + if(symbol.name!=orig_name) + { + if(!asm_label_map.insert( + std::make_pair(orig_name, asm_label)).second) + { + err_location(symbol.location); + if(asm_label_map[orig_name]==asm_label) + { + str << "duplicate (consistent) asm renaming"; + warning_msg(); + } + else + { + str << "error: conflicting asm renaming"; + throw 0; + } + } + } + else if(asm_label.empty()) + { + asm_label_mapt::const_iterator entry= + asm_label_map.find(symbol.name); + if(entry!=asm_label_map.end()) + { + symbol.name=entry->second; + symbol.base_name=entry->second; + } + } + + if(symbol.name!=orig_name && + symbol.type.id()==ID_code && + symbol.value.is_not_nil() && !symbol.is_macro) + { + const code_typet &code_type=to_code_type(symbol.type); + + for(code_typet::parameterst::const_iterator + p_it=code_type.parameters().begin(); + p_it!=code_type.parameters().end(); + ++p_it) + { + const irep_idt &p_bn=p_it->get_base_name(); + if(p_bn.empty()) + continue; + + irep_idt p_id=id2string(orig_name)+"::"+id2string(p_bn); + irep_idt p_new_id=id2string(symbol.name)+"::"+id2string(p_bn); + + if(!asm_label_map.insert( + std::make_pair(p_id, p_new_id)).second) + assert(asm_label_map[p_id]==p_new_id); + } + } +} + +/*******************************************************************\ + Function: c_typecheck_baset::typecheck_declaration Inputs: @@ -749,11 +838,24 @@ void c_typecheck_baset::typecheck_declaration( symbolt symbol; declaration.to_symbol(*d_it, symbol); - irep_idt identifier=symbol.name; // now check other half of type typecheck_type(symbol.type); + if(!full_spec.alias.empty()) + { + if(symbol.value.is_not_nil()) + throw "alias attribute cannot be used with a body"; + + // alias function need not have been declared yet, thus + // can't lookup + symbol.value=symbol_exprt(full_spec.alias); + symbol.is_macro=true; + } + + apply_asm_label(full_spec.asm_label, symbol); + irep_idt identifier=symbol.name; + typecheck_symbol(symbol); // add code contract (if any); we typecheck this after the diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 14819faa2cc..f2386a8e94d 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -283,6 +283,11 @@ class c_typecheck_baset: src.id()==ID_c_enum_tag || src.id()==ID_c_bit_field; } + + typedef hash_map_cont asm_label_mapt; + asm_label_mapt asm_label_map; + + void apply_asm_label(const irep_idt &asm_label, symbolt &symbol); }; #endif diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 1965cb2b69e..e020beeedbf 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -789,7 +789,7 @@ Function: c_typecheck_baset::typecheck_expr_symbol void c_typecheck_baset::typecheck_expr_symbol(exprt &expr) { - const irep_idt &identifier=to_symbol_expr(expr).get_identifier(); + irep_idt identifier=to_symbol_expr(expr).get_identifier(); // Is it a parameter? We do this while checking parameter lists. id_type_mapt::const_iterator p_it=parameter_map.find(identifier); @@ -801,6 +801,15 @@ void c_typecheck_baset::typecheck_expr_symbol(exprt &expr) return; } + // renaming via GCC asm label + asm_label_mapt::const_iterator entry= + asm_label_map.find(identifier); + if(entry!=asm_label_map.end()) + { + identifier=entry->second; + to_symbol_expr(expr).set_identifier(identifier); + } + // look it up const symbolt *symbol_ptr; if(lookup(identifier, symbol_ptr)) @@ -828,11 +837,13 @@ void c_typecheck_baset::typecheck_expr_symbol(exprt &expr) // preserve enum key irep_idt base_name=expr.get(ID_C_base_name); - expr=symbol.value; + follow_macros(expr); if(expr.id()==ID_constant && !base_name.empty()) expr.set(ID_C_cformat, base_name); + else + typecheck_expr(expr); // preserve location expr.add_source_location()=source_location; @@ -2143,8 +2154,12 @@ void c_typecheck_baset::typecheck_side_effect_function_call( if(f_op.id()==ID_symbol) { - const irep_idt &identifier= - to_symbol_expr(f_op).get_identifier(); + irep_idt identifier=to_symbol_expr(f_op).get_identifier(); + + asm_label_mapt::const_iterator entry= + asm_label_map.find(identifier); + if(entry!=asm_label_map.end()) + identifier=entry->second; if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end()) { diff --git a/src/ansi-c/library/unistd.c b/src/ansi-c/library/unistd.c index 839d71e6b68..8587036ddea 100644 --- a/src/ansi-c/library/unistd.c +++ b/src/ansi-c/library/unistd.c @@ -2,6 +2,7 @@ unsigned int sleep(unsigned int seconds) { + __CPROVER_HIDE:; // do nothing, but return nondet value unsigned remaining_time; @@ -10,6 +11,16 @@ unsigned int sleep(unsigned int seconds) return remaining_time; } +/* FUNCTION: _sleep */ + +unsigned int sleep(unsigned int seconds); + +inline unsigned int _sleep(unsigned int seconds) +{ + __CPROVER_HIDE:; + return sleep(seconds); +} + /* FUNCTION: unlink */ int unlink(const char *s) @@ -64,15 +75,6 @@ int pipe(int fildes[2]) /* FUNCTION: close */ -#ifdef _WIN32 -#include -#else -#ifndef __CPROVER_UNISTD_H_INCLUDED -#include -#define __CPROVER_UNISTD_H_INCLUDED -#endif -#endif - extern struct __CPROVER_pipet __CPROVER_pipes[]; // offset to make sure we don't collide with other fds extern const int __CPROVER_pipe_offset; @@ -98,14 +100,25 @@ int close(int fildes) return retval; } +/* FUNCTION: _close */ + +inline int _close(int fildes) +{ + __CPROVER_HIDE:; + return close(fildes); +} + /* FUNCTION: write */ -#ifdef _WIN32 -#include +// do not include unistd.h as this might trigger GCC asm renaming of +// write to _write; this is covered by the explicit definition of +// _write below +#ifdef _MSC_VER +#define ssize_t signed long #else -#ifndef __CPROVER_UNISTD_H_INCLUDED -#include -#define __CPROVER_UNISTD_H_INCLUDED +#ifndef __CPROVER_SYS_TYPES_H_INCLUDED +#include +#define __CPROVER_SYS_TYPES_H_INCLUDED #endif #endif @@ -113,10 +126,6 @@ extern struct __CPROVER_pipet __CPROVER_pipes[]; // offset to make sure we don't collide with other fds extern const int __CPROVER_pipe_offset; -#ifdef _MSC_VER -#define ssize_t signed long -#endif - ssize_t write(int fildes, const void *buf, size_t nbyte) { __CPROVER_HIDE:; @@ -146,25 +155,43 @@ ssize_t write(int fildes, const void *buf, size_t nbyte) return retval; } -/* FUNCTION: read */ +/* FUNCTION: _write */ -#ifdef _WIN32 -#include +#ifdef _MSC_VER +#define ssize_t signed long #else -#ifndef __CPROVER_UNISTD_H_INCLUDED -#include -#define __CPROVER_UNISTD_H_INCLUDED +#ifndef __CPROVER_SYS_TYPES_H_INCLUDED +#include +#define __CPROVER_SYS_TYPES_H_INCLUDED #endif #endif -extern struct __CPROVER_pipet __CPROVER_pipes[]; -// offset to make sure we don't collide with other fds -extern const int __CPROVER_pipe_offset; +ssize_t write(int fildes, const void *buf, size_t nbyte); +inline ssize_t _write(int fildes, const void *buf, size_t nbyte) +{ + __CPROVER_HIDE:; + return write(fildes, buf, nbyte); +} + +/* FUNCTION: read */ + +// do not include unistd.h as this might trigger GCC asm renaming of +// read to _read; this is covered by the explicit definition of _read +// below #ifdef _MSC_VER #define ssize_t signed long +#else +#ifndef __CPROVER_SYS_TYPES_H_INCLUDED +#include +#define __CPROVER_SYS_TYPES_H_INCLUDED +#endif #endif +extern struct __CPROVER_pipet __CPROVER_pipes[]; +// offset to make sure we don't collide with other fds +extern const int __CPROVER_pipe_offset; + ssize_t read(int fildes, void *buf, size_t nbyte) { __CPROVER_HIDE:; @@ -209,3 +236,21 @@ ssize_t read(int fildes, void *buf, size_t nbyte) return retval; } +/* FUNCTION: _read */ + +#ifdef _MSC_VER +#define ssize_t signed long +#else +#ifndef __CPROVER_SYS_TYPES_H_INCLUDED +#include +#define __CPROVER_SYS_TYPES_H_INCLUDED +#endif +#endif + +ssize_t read(int fildes, void *buf, size_t nbyte); + +inline ssize_t _read(int fildes, void *buf, size_t nbyte) +{ + __CPROVER_HIDE:; + return read(fildes, buf, nbyte); +} diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index b827e91bc74..cd1f76a6f8b 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -132,6 +132,7 @@ extern char *yyansi_ctext; %token TOK_GCC_ATTRIBUTE_MODE "mode" %token TOK_GCC_ATTRIBUTE_GNU_INLINE "__gnu_inline__" %token TOK_GCC_ATTRIBUTE_WEAK "weak" +%token TOK_GCC_ATTRIBUTE_ALIAS "alias" %token TOK_GCC_ATTRIBUTE_NORETURN "noreturn" %token TOK_GCC_ATTRIBUTE_CONSTRUCTOR "constructor" %token TOK_GCC_ATTRIBUTE_DESTRUCTOR "destructor" @@ -1564,6 +1565,8 @@ gcc_type_attribute: { $$=$1; set($$, ID_static); } /* GCC extern inline - cleanup in ansi_c_declarationt::to_symbol */ | TOK_GCC_ATTRIBUTE_WEAK TOK_GCC_ATTRIBUTE_END { $$=$1; set($$, ID_weak); } + | TOK_GCC_ATTRIBUTE_ALIAS '(' TOK_STRING ')' TOK_GCC_ATTRIBUTE_END + { $$=$1; set($$, ID_alias); mto($$, $3); } | TOK_NORETURN { $$=$1; set($$, ID_noreturn); } | TOK_GCC_ATTRIBUTE_NORETURN TOK_GCC_ATTRIBUTE_END diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 281239a5dd8..b1616940812 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -1,5 +1,6 @@ %option nounput %option noinput +%option stack %{ @@ -230,7 +231,7 @@ void ansi_c_scanner_init() } { - "*/" { BEGIN(STRING_LITERAL); } /* end comment state, back to STRING_LITERAL */ + "*/" { yy_pop_state(); } /* end comment state, back to STRING_LITERAL */ "/*" { yyansi_cerror("Probably nested comments"); } <> { yyansi_cerror("Unterminated comment"); return TOK_SCANNER_ERROR; } [^*/\n]* { /* ignore every char except '*' and NL (performance!) */ } @@ -252,14 +253,16 @@ void ansi_c_scanner_init() return TOK_CHARACTER; } -{string_lit} { +{string_lit} { PARSER.string_literal.clear(); PARSER.string_literal.append(yytext); newstack(yyansi_clval); PARSER.set_source_location(stack(yyansi_clval)); // String literals can be continued in // the next line - BEGIN(STRING_LITERAL); + yy_push_state(STRING_LITERAL); + // use yy_top_state() to keep the compiler happy + (void)yy_top_state(); } {string_lit} { PARSER.string_literal.append(yytext); } @@ -270,13 +273,13 @@ void ansi_c_scanner_init() PARSER.set_line_no(PARSER.get_line_no()-1); } {cppdirective} { /* ignore */ } -"/*" { BEGIN(STRING_LITERAL_COMMENT); /* C comment, ignore */ } +"/*" { yy_push_state(STRING_LITERAL_COMMENT); /* C comment, ignore */ } "//".*\n { /* C++ comment, ignore */ } . { // anything else: back to normal source_locationt l=stack(yyansi_clval).source_location(); stack(yyansi_clval)=convert_string_literal(PARSER.string_literal); stack(yyansi_clval).add_source_location().swap(l); - BEGIN(GRAMMAR); // back to normal + yy_pop_state(); // back to normal yyless(0); // put back return TOK_STRING; } @@ -1390,6 +1393,9 @@ __decltype { if(PARSER.cpp98 && PARSER.mode==ansi_c_parsert::GCC) "weak" | "__weak__" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_WEAK; } +"alias" | +"__alias__" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_ALIAS; } + "noreturn" | "__noreturn__" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_NORETURN; } diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 0f9c7a85701..0e04ca5c0a8 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -850,6 +850,7 @@ void compilet::convert_symbols(goto_functionst &dest) assert(s_it!=symbol_table.symbols.end()); if(s_it->second.type.id()==ID_code && + !s_it->second.is_macro && s_it->second.value.id()!="compiled" && s_it->second.value.is_not_nil()) { diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index 85d85ecc5d1..78747721772 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -77,6 +77,7 @@ void goto_convert_functionst::goto_convert() forall_symbols(it, symbol_table.symbols) { if(!it->second.is_type && + !it->second.is_macro && it->second.type.id()==ID_code && (it->second.mode==ID_C || it->second.mode==ID_cpp || diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp index 4abede465ae..622d03bd357 100644 --- a/src/goto-programs/read_goto_binary.cpp +++ b/src/goto-programs/read_goto_binary.cpp @@ -349,6 +349,33 @@ static bool link_functions( } } + // apply macros + rename_symbolt macro_application; + + forall_symbols(it, dest_symbol_table.symbols) + if(it->second.is_macro) + { + const symbolt &symbol=it->second; + + assert(symbol.value.id()==ID_symbol); + const irep_idt &id=to_symbol_expr(symbol.value).get_identifier(); + + #if 0 + if(!base_type_eq(symbol.type, ns.lookup(id).type, ns)) + { + std::cerr << symbol << std::endl; + std::cerr << ns.lookup(id) << std::endl; + } + assert(base_type_eq(symbol.type, ns.lookup(id).type, ns)); + #endif + + macro_application.insert_expr(symbol.name, id); + } + + if(!macro_application.expr_map.empty()) + Forall_goto_functions(dest_it, dest_functions) + rename_symbols_in_function(dest_it->second, macro_application); + return false; } diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 76724e30856..4be3377c69f 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -805,6 +805,7 @@ void linkingt::duplicate_code_symbol( old_symbol.value=new_symbol.value; old_symbol.type=new_symbol.type; // for parameter identifiers old_symbol.is_weak=new_symbol.is_weak; + old_symbol.is_macro=new_symbol.is_macro; } else if(to_code_type(old_symbol.type).get_inlined()) { @@ -932,6 +933,7 @@ void linkingt::duplicate_object_symbol( { // new_symbol wins old_symbol.value=new_symbol.value; + old_symbol.is_macro=new_symbol.is_macro; } else if(!new_symbol.is_weak) { diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index 096a4e7f749..e0aa6d19efe 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -74,7 +74,7 @@ bool static_lifetime_init( if(!symbol.is_static_lifetime) continue; - if(symbol.is_type) continue; + if(symbol.is_type || symbol.is_macro) continue; // special values if(identifier==CPROVER_PREFIX "constant_infinity_uint" ||