36 std::stringstream func_decl_stream;
37 std::stringstream compound_body_stream;
38 std::stringstream global_var_stream;
39 std::stringstream global_decl_stream;
40 std::stringstream func_body_stream;
48 const symbolt &symbol=named_symbol.second;
50 if(symbol.
type.
id()!=ID_code)
57 for(code_typet::parameterst::iterator
58 it2=parameters.begin();
59 it2!=parameters.end();
62 typet &type=it2->type();
64 if(type.
id()==ID_symbol &&
65 type.
get_bool(ID_C_transparent_union))
71 new_type_sym.
type.
set(ID_C_transparent_union,
true);
74 symbols_transparent.
add(new_type_sym);
77 type.
remove(ID_C_transparent_union);
81 for(
const auto &symbol_pair : symbols_transparent.
symbols)
86 typedef std::unordered_map<irep_idt, unsigned> unique_tagst;
87 unique_tagst unique_tags;
91 std::set<std::string> symbols_sorted;
100 if((symbol.
type.
id()==ID_union || symbol.
type.
id()==ID_struct) &&
104 symbol.
type.
set(ID_tag, ID_anonymous);
107 else if(symbol.
type.
id()==ID_c_enum &&
111 symbol.
type.
add(ID_tag).
set(ID_C_base_name, ID_anonymous);
115 const std::string name_str=
id2string(named_symbol.first);
117 (symbol.
type.
id()==ID_union ||
118 symbol.
type.
id()==ID_struct ||
119 symbol.
type.
id()==ID_c_enum))
121 std::string new_tag=symbol.
type.
id()==ID_c_enum?
126 if(tag_pos!=std::string::npos)
127 new_tag.erase(0, tag_pos+4);
128 const std::string new_tag_base=new_tag;
130 for(std::pair<unique_tagst::iterator, bool>
131 unique_entry=unique_tags.insert(std::make_pair(new_tag, 0));
132 !unique_entry.second;
133 unique_entry=unique_tags.insert(std::make_pair(new_tag, 0)))
135 new_tag=new_tag_base+
"$"+
137 ++(unique_entry.first->second);
140 if(symbol.
type.
id()==ID_c_enum)
142 symbol.
type.
add(ID_tag).
set(ID_C_base_name, new_tag);
146 symbol.
type.
set(ID_tag, new_tag);
151 if((!tag_added || symbol.
is_type) &&
156 bool inserted=symbols_sorted.insert(name_str).second;
163 bool skip_function_main=
false;
164 for(std::set<std::string>::const_iterator
165 it=symbols_sorted.begin();
166 it!=symbols_sorted.end();
174 (type_id==ID_struct ||
175 type_id==ID_incomplete_struct ||
177 type_id==ID_incomplete_union ||
182 global_decl_stream <<
"// " << symbol.
name <<
'\n';
183 global_decl_stream <<
"// " << symbol.
location <<
'\n';
185 if(type_id==ID_c_enum)
197 else if(symbol.
type.
id()==ID_code)
199 goto_functionst::function_mapt::const_iterator func_entry=
204 func_entry->second.body_available() &&
205 (symbol.
name==ID_main ||
207 skip_function_main=
true;
212 for(std::set<std::string>::const_iterator
213 it=symbols_sorted.begin();
214 it!=symbols_sorted.end();
219 if(symbol.
type.
id()!=ID_code ||
232 for(std::set<std::string>::const_iterator
233 it=symbols_sorted.begin();
234 it!=symbols_sorted.end();
240 (symbol.
type.
id()==ID_struct ||
241 symbol.
type.
id()==ID_incomplete_struct ||
242 symbol.
type.
id()==ID_union ||
243 symbol.
type.
id()==ID_incomplete_union))
246 compound_body_stream);
251 for(std::set<std::string>::const_iterator
255 os <<
"#include <" << *it <<
">\n";
259 if(global_var_stream.str().find(
"NULL")!=std::string::npos ||
260 func_body_stream.str().find(
"NULL")!=std::string::npos)
262 os <<
"#ifndef NULL\n" 263 <<
"#define NULL ((void*)0)\n" 266 if(func_body_stream.str().find(
"FENCE")!=std::string::npos)
268 os <<
"#ifndef FENCE\n" 269 <<
"#define FENCE(x) ((void)0)\n" 272 if(func_body_stream.str().find(
"IEEE_FLOAT_")!=std::string::npos)
274 os <<
"#ifndef IEEE_FLOAT_EQUAL\n" 275 <<
"#define IEEE_FLOAT_EQUAL(x,y) ((x)==(y))\n" 277 <<
"#ifndef IEEE_FLOAT_NOTEQUAL\n" 278 <<
"#define IEEE_FLOAT_NOTEQUAL(x,y) ((x)!=(y))\n" 282 if(!global_decl_stream.str().empty())
283 os << global_decl_stream.str() <<
'\n';
287 if(!func_decl_stream.str().empty())
288 os << func_decl_stream.str() <<
'\n';
289 if(!compound_body_stream.str().empty())
290 os << compound_body_stream.str() <<
'\n';
291 if(!global_var_stream.str().empty())
292 os << global_var_stream.str() <<
'\n';
293 os << func_body_stream.str();
299 std::ostream &os_body)
305 if(symbol.
type.
id()==ID_struct ||
306 symbol.
type.
id()==ID_union ||
307 symbol.
type.
id()==ID_c_enum)
313 const typet &unresolved,
317 if(type.
id()==ID_symbol)
326 else if(type.
id()==ID_c_enum_tag)
335 else if(type.
id()==ID_array || type.
id()==ID_pointer)
343 if(type.
id()==ID_array)
348 for(find_symbols_sett::const_iterator
358 else if(type.
id()==ID_struct || type.
id()==ID_union)
360 else if(type.
id()==ID_c_enum)
366 const typet &unresolved,
378 const irept &bases = type.
find(ID_bases);
379 std::stringstream base_decls;
417 std::stringstream struct_body;
419 for(struct_union_typet::componentst::const_iterator
427 if(comp_type.
id()==ID_code ||
433 while(non_array_type->
id()==ID_array)
438 if(non_array_type->
id()!=ID_pointer)
446 struct_body <<
indent(1) <<
"// " << comp_name <<
'\n';
451 std::string fake_unique_name=
"NO/SUCH/NS::"+
id2string(comp_name);
455 if(comp_type.
id()==ID_c_bit_field &&
462 if(s.find(
"__CPROVER_bitvector")==std::string::npos)
466 else if(comp_type.
id()==ID_signedbv)
470 struct_body <<
"long long int " << comp_name
473 struct_body <<
"__signedbv<" << t.
get_width() <<
"> " 478 else if(comp_type.
id()==ID_unsignedbv)
482 struct_body <<
"unsigned long long " << comp_name
485 struct_body <<
"__unsignedbv<" << t.
get_width() <<
"> " 493 struct_body <<
";\n";
496 typet unresolved_clean=unresolved;
497 typedef_typest::const_iterator td_entry=
502 unresolved_clean.
remove(ID_C_typedef);
503 typedef_str=td_entry->second;
504 std::pair<typedef_mapt::iterator, bool> td_map_entry=
507 if(!td_map_entry.first->second.early)
508 td_map_entry.first->second.type_decl_str=
"";
513 if(!base_decls.str().empty())
516 os <<
": " << base_decls.str();
520 os << struct_body.str();
535 if(type.
get_bool(ID_C_transparent_union))
536 os <<
" __attribute__ ((__transparent_union__))";
538 os <<
" __attribute__ ((__packed__))";
539 if(!typedef_str.
empty())
540 os <<
" " << typedef_str;
551 const irep_idt &name=tag.get(ID_C_base_name);
560 for(c_enum_typet::memberst::iterator
565 const irep_idt bn=it->get_base_name();
572 it->set_base_name(new_bn);
576 std::make_pair(bn, it->get_base_name()));
582 os <<
" __attribute__ ((__packed__))";
589 std::list<irep_idt> &local_static,
590 std::list<irep_idt> &local_type_decls)
612 std::unordered_set<irep_idt> typedef_names;
614 typedef_names.insert(td.first);
639 std::unordered_set<irep_idt> deps;
653 std::unordered_set<irep_idt> &dependencies)
658 std::unordered_set<irep_idt> local_deps;
660 if(type.
id()==ID_code)
665 for(
const auto ¶m : code_type.
parameters())
668 else if(type.
id()==ID_pointer || type.
id()==ID_array)
672 else if(type.
id()==ID_symbol)
679 const irep_idt &typedef_str=type.
get(ID_C_typedef);
681 if(!typedef_str.
empty())
683 std::pair<typedef_mapt::iterator, bool> entry=
687 (early && entry.first->second.type_decl_str.empty()))
689 if(typedef_str==
"__gnuc_va_list" || typedef_str ==
"va_list")
699 std::ostringstream oss;
700 oss <<
"typedef " <<
make_decl(typedef_str, t) <<
';';
702 entry.first->second.type_decl_str=oss.str();
703 entry.first->second.dependencies=local_deps;
709 entry.first->second.early=
true;
711 for(
const auto &d : local_deps)
715 td_entry->second.early=
true;
719 dependencies.insert(typedef_str);
722 dependencies.insert(local_deps.begin(), local_deps.end());
732 std::map<std::string, symbolt> symbols_sorted;
734 symbols_sorted.insert(
735 {
id2string(symbol_entry.first), symbol_entry.second});
737 for(
const auto &symbol_entry : symbols_sorted)
739 const symbolt &symbol=symbol_entry.second;
748 typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
761 std::vector<typedef_infot> typedefs_sorted;
766 std::map<std::string, typedef_infot> to_insert;
768 std::unordered_set<irep_idt> typedefs_done;
769 std::unordered_map<irep_idt, std::unordered_set<irep_idt>> forward_deps,
773 if(!td.second.type_decl_str.empty())
775 if(td.second.dependencies.empty())
777 to_insert.insert({id2string(td.first), td.second});
781 forward_deps.insert({td.first, td.second.dependencies});
782 for(
const auto &d : td.second.dependencies)
783 reverse_deps[d].insert(td.first);
787 while(!to_insert.empty())
792 to_insert.erase(to_insert.begin());
794 typedefs_sorted.push_back(t);
799 if(r_it==reverse_deps.end())
803 std::unordered_set<irep_idt> &r_deps = r_it->second;
804 for(std::unordered_set<irep_idt>::iterator it = r_deps.begin();
807 auto f_it=forward_deps.find(*it);
808 if(f_it==forward_deps.end())
815 std::unordered_set<irep_idt> &f_deps = f_it->second;
824 to_insert.insert({
id2string(*it), td_entry->second});
825 forward_deps.erase(*it);
835 for(
const auto &td : typedefs_sorted)
836 os << td.type_decl_str <<
'\n';
838 if(!typedefs_sorted.empty())
863 os <<
"// " << symbol.
name <<
'\n';
864 os <<
"// " << symbol.
location <<
'\n';
870 std::set<std::string> symbols_sorted;
871 for(find_symbols_sett::const_iterator
876 bool inserted=symbols_sorted.insert(
id2string(*it)).second;
880 for(std::set<std::string>::const_iterator
881 it=symbols_sorted.begin();
882 it!=symbols_sorted.end();
890 d.copy_to_operands(symbol.
value);
894 local_static_decls[symbol.
name]=d;
897 os <<
"// " << symbol.
name <<
'\n';
898 os <<
"// " << symbol.
location <<
'\n';
900 std::list<irep_idt> empty_static, empty_types;
915 const symbolt *argc_sym=
nullptr;
923 const symbolt *argv_sym=
nullptr;
931 const symbolt *return_sym=
nullptr;
932 if(!
ns.
lookup(
"return'", return_sym))
935 replace.
insert(return_sym->
name, return_value);
947 if(func.
id()==ID_symbol)
966 const bool skip_main,
967 std::ostream &os_decl,
968 std::ostream &os_body,
977 goto_functionst::function_mapt::const_iterator func_entry=
980 func_entry->second.body_available())
983 std::list<irep_idt> type_decls, local_static;
985 std::unordered_set<irep_idt> typedef_names;
987 typedef_names.insert(td.first);
991 func_entry->second.body,
1022 os_body <<
"// " << symbol.
name <<
'\n';
1023 os_body <<
"// " << symbol.
location <<
'\n';
1040 symbol.
name!=ID_main)
1042 os_decl <<
"// " << symbol.
name <<
'\n';
1043 os_decl <<
"// " << symbol.
location <<
'\n';
1048 os_decl <<
"// " << symbol.
name <<
'\n';
1049 os_decl <<
"// " << symbol.
location <<
'\n';
1063 exprt::operandst::iterator &before)
1071 exprt::operandst::iterator first_found=operands.end();
1078 if(it->id()==ID_code &&
1090 found=syms.find(identifier)!=syms.end();
1111 if(first_found==operands.end())
1128 if(first_found!=operands.end())
1140 const std::list<irep_idt> &local_static,
1142 std::list<irep_idt> &type_decls)
1146 for(std::list<irep_idt>::const_reverse_iterator
1147 it=local_static.rbegin();
1148 it!=local_static.rend();
1151 local_static_declst::const_iterator d_it=
1152 local_static_decls.find(*it);
1156 std::list<irep_idt> redundant;
1160 exprt::operandst::iterator before=b.
operands().end();
1167 dest_ptr->
operands().insert(before, d);
1174 const std::list<irep_idt> &type_decls)
1178 for(std::list<irep_idt>::const_reverse_iterator
1179 it=type_decls.rbegin();
1180 it!=type_decls.rend();
1186 std::ostringstream os_body;
1187 os_body << *it <<
" */\n";
1197 exprt::operandst::iterator before=b.
operands().end();
1204 dest_ptr->
operands().insert(before, skip);
1216 if(expr.
id()==ID_struct)
1228 exprt::operandst::iterator o_it=old_ops.begin();
1229 for(struct_union_typet::componentst::const_iterator
1230 it=old_components.begin();
1231 it!=old_components.end();
1234 const bool is_zero_bit_field=
1235 it->type().id()==ID_c_bit_field &&
1238 if(!it->get_is_padding() && !is_zero_bit_field)
1247 else if(expr.
id()==ID_union)
1253 !u_type_f.
get_bool(ID_C_transparent_union))
1260 else if(u.
op().
id()==ID_constant &&
1281 else if(expr.
id()==ID_typecast &&
1282 expr.
op0().
id()==ID_typecast &&
1288 else if(expr.
id()==ID_code &&
1304 if(parameters.size()==arguments.size())
1306 code_typet::parameterst::const_iterator it=parameters.begin();
1310 if(type.
id()==ID_union &&
1311 type.
get_bool(ID_C_transparent_union))
1313 if(it2->id()==ID_typecast &&
1318 if(it2->id()==ID_constant &&
1321 const typet &comp_type=
1324 if(comp_type.
id()==ID_pointer)
1334 else if(expr.
id()==ID_constant &&
1335 expr.
type().
id()==ID_signedbv)
1340 if(!cformat.
empty())
1342 declared_enum_constants_mapt::const_iterator entry=
1346 entry->first!=entry->second)
1347 expr.
set(ID_C_cformat, entry->second);
1350 expr.
remove(ID_C_cformat);
1361 if(type.
id()==ID_code)
1367 for(code_typet::parameterst::iterator
1374 if(type.
id()==ID_array)
1378 (type.
id()!=ID_union && type.
id()!=ID_struct) ||
1402 const bool use_system_headers,
1403 const bool use_all_headers,
1404 const bool include_harness,
1420 const bool use_system_headers,
1421 const bool use_all_headers,
1422 const bool include_harness,
const irep_idt & get_statement() const
const irep_idt & get_name() const
The type of an expression.
irep_idt name
The unique identifier.
struct configt::ansi_ct ansi_c
void collect_typedefs(const typet &type, bool early)
Find any typedef names contained in the input type and store their declaration strings in typedef_map...
Fixed-width bit-vector with unsigned binary interpretation.
std::unique_ptr< languaget > new_cpp_language()
const std::string & id2string(const irep_idt &d)
void insert_local_static_decls(code_blockt &b, const std::list< irep_idt > &local_static, local_static_declst &local_static_decls, std::list< irep_idt > &type_decls)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
bool is_symbol_internal_symbol(const symbolt &symbol, std::set< std::string > &out_system_headers) const
To find out if a symbol is an internal symbol.
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
void set_comment(const irep_idt &comment)
declared_enum_constants_mapt declared_enum_constants
const irep_idt & get_function() const
const irep_idt & get_identifier() const
std::string type_to_string(const typet &type)
std::ostream & operator<<(std::ostream &out, dump_ct &src)
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
std::vector< componentt > componentst
std::unordered_map< irep_idt, code_declt > local_static_declst
void move_to_operands(exprt &expr)
const irep_idt & get_value() const
std::string expr_to_string(const exprt &expr)
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
std::vector< parametert > parameterst
exprt value
Initial value of symbol.
const componentst & components() const
Dump C from Goto Program.
Dump Goto-Program as C/C++ Source.
void set_identifier(const irep_idt &identifier)
function_mapt function_map
exprt::operandst argumentst
unsignedbv_typet size_type()
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
const goto_functionst & goto_functions
#define CHECK_RETURN(CONDITION)
bool get_bool(const irep_namet &name) const
#define POSTCONDITION(CONDITION)
convertedt converted_enum
std::unordered_set< irep_idt > convertedt
static bool find_block_position_rec(const irep_idt &identifier, codet &root, code_blockt *&dest, exprt::operandst::iterator &before)
virtual symbolt * get_writeable(const irep_idt &name) override
Find a symbol in the symbol table for read-write access.
std::string make_decl(const irep_idt &identifier, const typet &type)
void dump_c(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)
const irep_idt & id() const
typedef_typest typedef_types
void insert_local_type_decls(code_blockt &b, const std::list< irep_idt > &type_decls)
std::size_t long_long_int_width
void add(const codet &code)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
A reference into the symbol table.
instructionst::iterator targett
A declaration of a local variable.
#define Forall_expr(it, expr)
Fixed-width bit-vector with two's complement interpretation.
#define INITIALIZE_FUNCTION
union constructor from single element
void convert_compound(const typet &type, const typet &unresolved, bool recursive, std::ostream &os)
void cleanup_decl(code_declt &decl, std::list< irep_idt > &local_static, std::list< irep_idt > &local_type_decls)
const irep_idt & get(const irep_namet &name) const
void gather_global_typedefs()
Find all global typdefs in the symbol table and store them in typedef_types.
#define PRECONDITION(CONDITION)
bool is_type_internal(const typet &type, std::set< std::string > &out_system_headers) const
Helper function to call is_symbol_internal_symbol on a nameless fake symbol with the given type...
const exprt & size() const
system_library_symbolst system_symbols
Base class for tree-like data structures with sharing.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const typet & follow(const typet &) const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
std::set< std::string > system_headers
std::unique_ptr< languaget > language
convertedt converted_global
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool has_operands() const
std::size_t get_width() const
std::unordered_map< irep_idt, irep_idt > declared_enum_constants_mapt
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
void find_non_pointer_type_symbols(const exprt &src, find_symbols_sett &dest)
std::vector< exprt > operandst
Dump Goto-Program as C/C++ Source.
A generic container class for the GOTO intermediate representation of one function.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
void collect_typedefs_rec(const typet &type, bool early, std::unordered_set< irep_idt > &dependencies)
Find any typedef names contained in the input type and store their declaration strings in typedef_map...
static irep_idt entry_point()
void convert_compound_declaration(const symbolt &symbol, std::ostream &os_body)
declare compound types
Base type of C structs and unions, and C++ classes.
void cleanup_expr(exprt &expr)
targett add_instruction()
Adds an instruction at the end.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
const parameterst & parameters() const
irep_idt base_name
Base (non-scoped) name.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
irept & add(const irep_namet &name)
const std::string & get_string(const irep_namet &name) const
void convert_compound_enum(const typet &type, std::ostream &os)
std::unique_ptr< languaget > new_ansi_c_language()
#define Forall_subtypes(it, type)
void set_identifier(const irep_idt &identifier)
void operator()(std::ostream &out)
irep_idt get_component_name() const
#define Forall_operands(it, expr)
source_locationt & add_source_location()
void insert(const irep_idt &identifier, const exprt &expr)
const codet & to_code(const exprt &expr)
static std::string indent(const unsigned n)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
bool get_is_padding() const
Expression to hold a symbol (variable)
void convert_function_declaration(const symbolt &symbol, const bool skip_main, std::ostream &os_decl, std::ostream &os_body, local_static_declst &local_static_decls)
const code_blockt & to_code_block(const codet &code)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void dump_typedefs(std::ostream &os) const
Print all typedefs that are not covered via typedef struct xyz { ...
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a generic typet to a c_enum_typet.
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
A statement in a programming language.
std::unordered_set< irep_idt > find_symbols_sett
void remove(const irep_namet &name)
const typet & subtype() const
convertedt converted_compound
#define DATA_INVARIANT(CONDITION, REASON)
void cleanup_type(typet &type)
symbol_tablet copied_symbol_table
void convert_global_variable(const symbolt &symbol, std::ostream &os, local_static_declst &local_static_decls)
struct constructor from list of elements
std::vector< c_enum_membert > memberst
const irept & find(const irep_namet &name) const
void find_symbols(const exprt &src, find_symbols_sett &dest)
const typet & return_type() const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void set(const irep_namet &name, const irep_idt &value)
const componentt & get_component(const irep_idt &component_name) const
const code_function_callt & to_code_function_call(const codet &code)
void cleanup_harness(code_blockt &b)
Replace CPROVER internal symbols in b by printable values and generate necessary declarations.
#define forall_irep(it, irep)
void dump_cpp(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)