From 069d409048c60d6c3150f422850eae80f706491a Mon Sep 17 00:00:00 2001 From: "p.schrammel@sussex.ac.uk" Date: Fri, 7 Oct 2016 00:29:40 +0100 Subject: [PATCH 1/3] keep typedefs when dumping c with --use-system-headers --- src/ansi-c/ansi_c_convert_type.cpp | 2 + src/ansi-c/ansi_c_declaration.cpp | 4 + src/ansi-c/c_typecheck_base.cpp | 20 ++++- src/ansi-c/c_typecheck_type.cpp | 11 +++ src/ansi-c/expr2c.cpp | 32 +++++++- src/goto-instrument/dump_c.cpp | 95 +++++++++++++++++++++-- src/goto-instrument/dump_c_class.h | 2 + src/goto-instrument/goto_program2code.cpp | 8 +- src/goto-instrument/goto_program2code.h | 2 +- 9 files changed, 162 insertions(+), 14 deletions(-) diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 8fde8c57c4d..f8781ffd921 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -253,7 +253,9 @@ Function: ansi_c_convert_typet::write void ansi_c_convert_typet::write(typet &type) { + irep_idt _typedef = type.get(ID_typedef); type.clear(); + type.set(ID_typedef,_typedef); // first, do "other" diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp index f9dea43c02b..374dd1319cc 100644 --- a/src/ansi-c/ansi_c_declaration.cpp +++ b/src/ansi-c/ansi_c_declaration.cpp @@ -139,6 +139,10 @@ typet ansi_c_declarationt::full_type( *p=type(); + // retain typedef for dump-c + if(get_is_typedef()) + result.set(ID_typedef,declarator.get_name()); + return result; } diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index be7c58cc197..917d3e8adfd 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "type2name.h" #include "c_storage_spec.h" +#include + /*******************************************************************\ Function: c_typecheck_baset::to_string @@ -96,6 +98,9 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol) bool is_function=symbol.type.id()==ID_code; const typet &final_type=follow(symbol.type); +// std::cout << "BASENAME: " << symbol.base_name << std::endl; +// std::cout << "TYPE: " << symbol.type.pretty() << std::endl; +// std::cout << "FINAL: " << final_type.pretty() << std::endl; // set a few flags symbol.is_lvalue=!symbol.is_type && !symbol.is_macro; @@ -127,13 +132,23 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol) (final_type.id()==ID_struct || final_type.id()==ID_incomplete_struct)) { - symbol.pretty_name="struct "+id2string(symbol.base_name); + if(symbol.type.find(ID_typedef).is_not_nil()) + symbol.pretty_name=symbol.type.get(ID_typedef); + else + symbol.pretty_name="struct "+id2string(symbol.base_name); } else if(symbol.is_type && (final_type.id()==ID_union || final_type.id()==ID_incomplete_union)) { - symbol.pretty_name="union "+id2string(symbol.base_name); + if(symbol.type.find(ID_typedef).is_not_nil()) + { + symbol.pretty_name=symbol.type.get(ID_typedef); + symbol_table.symbols.find(symbol.type.get(ID_identifier))->second.pretty_name=symbol.type.get(ID_typedef); + symbol_table.symbols.find(symbol.type.get(ID_identifier))->second.type.set(ID_typedef,symbol.pretty_name); + } + else + symbol.pretty_name="union "+id2string(symbol.base_name); } else if(symbol.is_type && (final_type.id()==ID_c_enum || @@ -149,6 +164,7 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol) // see if we have it already symbol_tablet::symbolst::iterator old_it=symbol_table.symbols.find(symbol.name); + if(old_it==symbol_table.symbols.end()) { // just put into symbol_table diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 3002bd5c7d5..84502e2c4f3 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -23,6 +23,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "type2name.h" #include "ansi_c_convert_type.h" +#include + /*******************************************************************\ Function: c_typecheck_baset::typecheck_type @@ -52,12 +54,14 @@ void c_typecheck_baset::typecheck_type(typet &type) c_qualifiers+=c_qualifierst(type.subtype()); bool packed=type.get_bool(ID_C_packed); exprt alignment=static_cast(type.find(ID_C_alignment)); + irept _typedef=type.find(ID_typedef); type.swap(type.subtype()); c_qualifiers.write(type); if(packed) type.set(ID_C_packed, true); if(alignment.is_not_nil()) type.add(ID_C_alignment, alignment); + if(_typedef.is_not_nil()) type.add(ID_typedef, _typedef); return; // done } @@ -726,11 +730,15 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type) // Anonymous? Must come with body. assert(have_body); +// std::cout << "__TYPE: " << type.pretty() << std::endl; + // produce symbol symbolt compound_symbol; compound_symbol.is_type=true; compound_symbol.type=type; compound_symbol.location=type.source_location(); + if(compound_symbol.type.find(ID_typedef).is_not_nil()) + compound_symbol.pretty_name=compound_symbol.type.get(ID_typedef); typecheck_compound_body(to_struct_union_type(compound_symbol.type)); @@ -739,6 +747,9 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type) compound_symbol.name="tag-#anon#"+typestr; identifier=compound_symbol.name; +// std::cout << "TYPEDEF: " << compound_symbol.type.get_string(ID_typedef) << std::endl; +// std::cout << "BASENAME: " << id2string(compound_symbol.base_name) << std::endl; + // We might already have the same anonymous union/struct, // and this is simply ok. Note that the C standard treats // these as different types. diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 78ced9c86a3..4c35c1d7ef1 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -360,7 +360,12 @@ std::string expr2ct::convert_rec( { const struct_typet &struct_type=to_struct_type(src); - std::string dest=q+"struct"; + std::string dest=q; + + if(src.find(ID_typedef).is_not_nil()) + dest+="typedef struct"; + else + dest+="struct"; const irep_idt &tag=struct_type.get_tag(); if(tag!="") dest+=" "+id2string(tag); @@ -378,7 +383,10 @@ std::string expr2ct::convert_rec( dest+=" }"; - dest+=d; + if(src.find(ID_typedef).is_not_nil()) + dest+=src.get_string(ID_typedef); + else + dest+=d; return dest; } @@ -396,7 +404,12 @@ std::string expr2ct::convert_rec( { const union_typet &union_type=to_union_type(src); - std::string dest=q+"union"; + std::string dest=q; + + if(src.find(ID_typedef).is_not_nil()) + dest+="typedef union"; + else + dest+="union"; const irep_idt &tag=union_type.get_tag(); if(tag!="") dest+=" "+id2string(tag); @@ -414,7 +427,10 @@ std::string expr2ct::convert_rec( dest+=" }"; - dest+=d; + if(src.find(ID_typedef).is_not_nil()) + dest+=src.get_string(ID_typedef); + else + dest+=d; return dest; } @@ -542,6 +558,8 @@ std::string expr2ct::convert_rec( if(followed.id()==ID_struct) { + if(followed.find(ID_typedef).is_not_nil()) + return followed.get_string(ID_typedef)+d; std::string dest=q+"struct"; const irep_idt &tag=to_struct_type(followed).get_tag(); if(tag!="") dest+=" "+id2string(tag); @@ -550,6 +568,8 @@ std::string expr2ct::convert_rec( } else if(followed.id()==ID_union) { + if(followed.find(ID_typedef).is_not_nil()) + return followed.get_string(ID_typedef)+d; std::string dest=q+"union"; const irep_idt &tag=to_union_type(followed).get_tag(); if(tag!="") dest+=" "+id2string(tag); @@ -561,6 +581,8 @@ std::string expr2ct::convert_rec( } else if(src.id()==ID_struct_tag) { + if(src.find(ID_typedef).is_not_nil()) + return src.get_string(ID_typedef)+d; const struct_tag_typet &struct_tag_type= to_struct_tag_type(src); @@ -573,6 +595,8 @@ std::string expr2ct::convert_rec( } else if(src.id()==ID_union_tag) { + if(src.find(ID_typedef).is_not_nil()) + return src.get_string(ID_typedef)+d; const union_tag_typet &union_tag_type= to_union_tag_type(src); diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 1d6d7cc712e..0ca8beb74ef 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -161,6 +161,9 @@ void dump_ct::operator()(std::ostream &os) symbol.type.set(ID_tag, new_tag); } + if(ignore(symbol)) + ignored_symbol_rec(symbol); + // we don't want to dump in full all definitions if(!tag_added && ignore(symbol)) continue; @@ -177,6 +180,10 @@ void dump_ct::operator()(std::ostream &os) ++it) { const symbolt &symbol=ns.lookup(*it); + + if(ignore(symbol)) + continue; + const irep_idt &type_id=symbol.type.id(); if(symbol.is_type && @@ -192,6 +199,10 @@ void dump_ct::operator()(std::ostream &os) if(type_id==ID_c_enum) convert_compound_enum(symbol.type, os); + else if(symbol.type.find(ID_typedef).is_not_nil()) + { + //skip + } else os << type_to_string(symbol_typet(symbol.name)) << ";\n\n"; } @@ -221,6 +232,9 @@ void dump_ct::operator()(std::ostream &os) { const symbolt &symbol=ns.lookup(*it); + if(ignore(symbol)) + continue; + if(symbol.type.id()!=ID_code) continue; convert_function_declaration( @@ -239,6 +253,9 @@ void dump_ct::operator()(std::ostream &os) { const symbolt &symbol=ns.lookup(*it); + if(ignore(symbol)) + continue; + if(symbol.is_type && (symbol.type.id()==ID_struct || symbol.type.id()==ID_incomplete_struct || @@ -517,7 +534,12 @@ void dump_ct::convert_compound( struct_body << ";" << std::endl; } - os << type_to_string(unresolved); + + if(type.find(ID_typedef).is_not_nil()) + os << "typedef "+id2string(type.id()); + else + os << type_to_string(unresolved); + if(!base_decls.str().empty()) { assert(language->id()=="cpp"); @@ -544,6 +566,8 @@ void dump_ct::convert_compound( os << " __attribute__ ((__transparent_union__))"; if(type.get_bool(ID_C_packed)) os << " __attribute__ ((__packed__))"; + if(type.find(ID_typedef).is_not_nil()) + os << " " << type.get_string(ID_typedef); os << ";"; os << std::endl; os << std::endl; @@ -673,10 +697,18 @@ void dump_ct::init_system_library_map() "pthread_rwlock_unlock", "pthread_rwlock_wrlock", "pthread_rwlockattr_destroy", "pthread_rwlockattr_getpshared", "pthread_rwlockattr_init", "pthread_rwlockattr_setpshared", - "pthread_self", "pthread_setspecific" + "pthread_self", "pthread_setspecific", + "pthread_mutex_t", "pthread_attr_t", "pthread_cond_t", + "tag-__pthread_internal_list", "tag-__pthread_mutex_s" }; ADD_TO_SYSTEM_LIBRARY(pthread_syms, "pthread.h"); + // sys/resource.h + const char* sys_resource_syms[]={ + "getrusage", "tag-rusage" + }; + ADD_TO_SYSTEM_LIBRARY(sys_resource_syms, "sys/resource.h"); + // setjmp.h const char* setjmp_syms[]={ "_longjmp", "_setjmp", "longjmp", "longjmperror", "setjmp", @@ -722,7 +754,7 @@ void dump_ct::init_system_library_map() const char* string_syms[]={ "strcat", "strncat", "strchr", "strrchr", "strcmp", "strncmp", "strcpy", "strncpy", "strerror", "strlen", "strpbrk", "strspn", - "strcspn", "strstr", "strtok" + "strcspn", "strstr", "strtok", "memcpy", "memset" }; ADD_TO_SYSTEM_LIBRARY(string_syms, "string.h"); @@ -735,6 +767,12 @@ void dump_ct::init_system_library_map() }; ADD_TO_SYSTEM_LIBRARY(time_syms, "time.h"); + // sys/time.h + const char* sys_time_syms[]={ + "gettimeofday", "tag-timezone" + }; + ADD_TO_SYSTEM_LIBRARY(sys_time_syms, "sys/time.h"); + // unistd.h const char* unistd_syms[]={ "_exit", "access", "alarm", "chdir", "chown", "close", "dup", @@ -782,6 +820,41 @@ void dump_ct::init_system_library_map() /*******************************************************************\ +Function: dump_ct::ignored_symbol_rec + +Inputs: + +Outputs: + +Purpose: recursively marks symbols that shall be ignored + +\*******************************************************************/ + +void dump_ct::ignored_symbol_rec(const symbolt &symbol) +{ + ignored_symbols.insert(id2string(symbol.name)); + + if(!(symbol.is_type && + (symbol.type.id()==ID_union || + symbol.type.id()==ID_struct))) + return; + + const struct_union_typet &type= + to_struct_union_type(ns.follow(symbol.type)); + + for(struct_union_typet::componentst::const_iterator + it=type.components().begin(); + it!=type.components().end(); + it++) + { + const struct_typet::componentt &comp=*it; + if(comp.type().id()==ID_symbol) + ignored_symbol_rec(ns.lookup(to_symbol_type(comp.type()).get_identifier())); + } +} + +/*******************************************************************\ + Function: dump_ct::ignore Inputs: @@ -796,6 +869,9 @@ bool dump_ct::ignore(const symbolt &symbol) { const std::string &name_str=id2string(symbol.name); + if(ignored_symbols.find(name_str)!=ignored_symbols.end()) + return true; + if(has_prefix(name_str, CPROVER_PREFIX) || name_str=="__func__" || name_str=="__FUNCTION__" || @@ -827,10 +903,13 @@ bool dump_ct::ignore(const symbolt &symbol) } if(name_str.find("$link")!=std::string::npos) - return false; + return true; - system_library_mapt::const_iterator it= - system_library_map.find(symbol.name); + system_library_mapt::const_iterator it; + if(symbol.is_type && symbol.type.find(ID_typedef).is_not_nil()) + it=system_library_map.find(symbol.type.get_string(ID_typedef)); + else + it=system_library_map.find(symbol.name); if(it!=system_library_map.end()) { @@ -1446,6 +1525,10 @@ std::string dump_ct::type_to_string(const typet &type) std::string ret; typet t=type; cleanup_type(t); +/* if((t.id()==ID_union || t.id()==ID_struct) && + t.find(ID_typedef).is_not_nil()) + return id2string(t.get(ID_typedef)); +*/ language->from_type(t, ret, ns); return ret; } diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-instrument/dump_c_class.h index a84841ca9b9..3fba1c1b346 100644 --- a/src/goto-instrument/dump_c_class.h +++ b/src/goto-instrument/dump_c_class.h @@ -64,6 +64,8 @@ class dump_ct std::string type_to_string(const typet &type); std::string expr_to_string(const exprt &expr); + std::set ignored_symbols; + void ignored_symbol_rec(const symbolt &symbol); bool ignore(const symbolt &symbol); static std::string indent(const unsigned n) diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index edcc18a3792..b9d4963d788 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -1882,7 +1882,7 @@ Function: goto_program2codet::cleanup_function_call \*******************************************************************/ void goto_program2codet::cleanup_function_call( - const exprt &function, + exprt &function, code_function_callt::argumentst &arguments) { if(function.id()!=ID_symbol) @@ -1890,6 +1890,12 @@ void goto_program2codet::cleanup_function_call( const symbol_exprt &fn=to_symbol_expr(function); + //clean function identifier + std::string name_str=id2string(function.get(ID_identifier)); + size_t pos=name_str.find("$link"); + if(pos!=std::string::npos) + function.set(ID_identifier,name_str.substr(0,pos)); + // don't edit function calls we might have introduced const symbolt *s; if(!ns.lookup(fn.get_identifier(), s)) diff --git a/src/goto-instrument/goto_program2code.h b/src/goto-instrument/goto_program2code.h index 02346e388ef..8ccf9d4d3e4 100644 --- a/src/goto-instrument/goto_program2code.h +++ b/src/goto-instrument/goto_program2code.h @@ -96,7 +96,7 @@ class goto_program2codet void cleanup_code(codet &code, const irep_idt parent_stmt); void cleanup_function_call( - const exprt &function, + exprt &function, code_function_callt::argumentst &arguments); void cleanup_code_block( From a0b3676794396ffa2ac7f108a7ef972ca4122ffe Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 9 Dec 2016 16:42:13 +0000 Subject: [PATCH 2/3] Use the symbol in expr2c --- src/ansi-c/expr2c.cpp | 46 +++++++++++++++++++++++++++---------------- 1 file changed, 29 insertions(+), 17 deletions(-) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 4c35c1d7ef1..d24c7edfd17 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -554,30 +554,42 @@ std::string expr2ct::convert_rec( } else if(src.id()==ID_symbol) { - const typet &followed=ns.follow(src); + symbol_typet symbolic_type=to_symbol_type(src); + const irep_idt &typedef_identifer=symbolic_type.get(ID_typedef); - if(followed.id()==ID_struct) + // Providing we have a valid identifer, we can just use that rather than + // trying to find the concrete type + if(typedef_identifer!="") { - if(followed.find(ID_typedef).is_not_nil()) - return followed.get_string(ID_typedef)+d; - std::string dest=q+"struct"; - const irep_idt &tag=to_struct_type(followed).get_tag(); - if(tag!="") dest+=" "+id2string(tag); - dest+=d; - return dest; + return q+id2string(typedef_identifer)+d; } - else if(followed.id()==ID_union) + else { + const typet &followed=ns.follow(src); + + if(followed.id()==ID_struct) + { if(followed.find(ID_typedef).is_not_nil()) return followed.get_string(ID_typedef)+d; - std::string dest=q+"union"; - const irep_idt &tag=to_union_type(followed).get_tag(); - if(tag!="") dest+=" "+id2string(tag); - dest+=d; - return dest; + std::string dest=q+"struct"; + const irep_idt &tag=to_struct_type(followed).get_tag(); + if(tag!="") dest+=" "+id2string(tag); + dest+=d; + return dest; + } + else if(followed.id()==ID_union) + { + if(followed.find(ID_typedef).is_not_nil()) + return followed.get_string(ID_typedef)+d; + std::string dest=q+"union"; + const irep_idt &tag=to_union_type(followed).get_tag(); + if(tag!="") dest+=" "+id2string(tag); + dest+=d; + return dest; + } + else + return convert_rec(followed, new_qualifiers, declarator); } - else - return convert_rec(followed, new_qualifiers, declarator); } else if(src.id()==ID_struct_tag) { From 093da6a302f7ca33c4cc42a77ac2f1064722cbc4 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 13 Dec 2016 17:00:41 +0000 Subject: [PATCH 3/3] Add the typedef'd type in the parsing step Rather than adding the typedef name to the root type after parsing and type checking. Instead when processing each declaration, store in the declaration the type used. Then when we create the symbol for the declaration, we can look to see if the declaration contained ID_typedef and move it into the type for that specific symbol. This doesn't completely resolve the problem as for some reason the function return entry coming back from interpreter doesn't have this type (despite the corresponding sybol in the symbol_table having it) --- src/ansi-c/ansi_c_declaration.cpp | 7 +++++++ src/ansi-c/ansi_c_parser.cpp | 15 +++++++++++++++ src/linking/remove_internal_symbols.cpp | 10 ++++++++++ 3 files changed, 32 insertions(+) diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp index 374dd1319cc..80074545b79 100644 --- a/src/ansi-c/ansi_c_declaration.cpp +++ b/src/ansi-c/ansi_c_declaration.cpp @@ -142,6 +142,13 @@ typet ansi_c_declarationt::full_type( // retain typedef for dump-c if(get_is_typedef()) result.set(ID_typedef,declarator.get_name()); + // If this declaration was declared with a typedef'd type, we record it in the + // type of the expression. + irep_idt typedef_type=declarator.get(ID_typedef); + if(typedef_type!="") + { + result.set(ID_typedef, typedef_type); + } return result; } diff --git a/src/ansi-c/ansi_c_parser.cpp b/src/ansi-c/ansi_c_parser.cpp index 88787d4b519..8f3720546a9 100644 --- a/src/ansi-c/ansi_c_parser.cpp +++ b/src/ansi-c/ansi_c_parser.cpp @@ -136,6 +136,16 @@ void ansi_c_parsert::add_declarator( irept &declarator) { assert(declarator.is_not_nil()); + + irep_idt typedefd_name=""; + if(declarator.id()==ID_symbol) + { + if(declaration.type().id()==ID_symbol) + { + typedefd_name=declaration.type().get(ID_identifier); + } + } + ansi_c_declarationt &ansi_c_declaration= to_ansi_c_declaration(declaration); @@ -197,6 +207,11 @@ void ansi_c_parsert::add_declarator( identifier.prefixed_name=prefixed_name; } + if(typedefd_name!="") + { + new_declarator.set(ID_typedef, typedefd_name); + } + ansi_c_declaration.declarators().push_back(new_declarator); } diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp index 88d2c435642..56bad4b0cff 100644 --- a/src/linking/remove_internal_symbols.cpp +++ b/src/linking/remove_internal_symbols.cpp @@ -144,6 +144,16 @@ void remove_internal_symbols( if(is_type) { // never EXPORTED by itself + // Without this code the symbol is lost when compiling with + // goto-cc + // So the problem with this approach is that this is per typedef + // we move the name of the typedef into the type it corresponds to + // e.g. will not elegantly work when more than one typedef for the same + // type. Instead we want to somehow whenever we find an expression + // that directly uses a typedef we want to record that that is the case + // so we can use the correct typedef +#if 0 +#endif } else if(is_function) {