cprover
Loading...
Searching...
No Matches
dump_c.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dump Goto-Program as C/C++ Source
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "dump_c.h"
13
14#include <util/byte_operators.h>
15#include <util/c_types.h>
16#include <util/config.h>
18#include <util/find_symbols.h>
19#include <util/get_base_name.h>
20#include <util/invariant.h>
21#include <util/namespace.h>
22#include <util/replace_symbol.h>
23#include <util/std_code.h>
24#include <util/string_utils.h>
25
26#include <ansi-c/expr2c.h>
27#include <cpp/expr2cpp.h>
28
30
31#include "dump_c_class.h"
32#include "goto_program2code.h"
33
36
43
44inline std::ostream &operator << (std::ostream &out, dump_ct &src)
45{
46 src(out);
47 return out;
48}
49
50void dump_ct::operator()(std::ostream &os)
51{
52 std::stringstream func_decl_stream;
53 std::stringstream compound_body_stream;
54 std::stringstream global_var_stream;
55 std::stringstream global_decl_stream;
56 std::stringstream global_decl_header_stream;
57 std::stringstream func_body_stream;
58 local_static_declst local_static_decls;
59
60 // add copies of struct types when ID_C_transparent_union is only
61 // annotated to parameter
62 symbol_tablet symbols_transparent;
63 for(const auto &named_symbol : copied_symbol_table.symbols)
64 {
65 const symbolt &symbol=named_symbol.second;
66
67 if(symbol.type.id()!=ID_code)
68 continue;
69
70 code_typet &code_type=to_code_type(
71 copied_symbol_table.get_writeable_ref(named_symbol.first).type);
72 code_typet::parameterst &parameters=code_type.parameters();
73
74 for(code_typet::parameterst::iterator
75 it2=parameters.begin();
76 it2!=parameters.end();
77 ++it2)
78 {
79 typet &type=it2->type();
80
81 if(type.id() == ID_union_tag && type.get_bool(ID_C_transparent_union))
82 {
83 symbolt new_type_sym =
85
86 new_type_sym.name=id2string(new_type_sym.name)+"$transparent";
87 new_type_sym.type.set(ID_C_transparent_union, true);
88
89 // we might have it already, in which case this has no effect
90 symbols_transparent.add(new_type_sym);
91
92 to_union_tag_type(type).set_identifier(new_type_sym.name);
93 type.remove(ID_C_transparent_union);
94 }
95 }
96 }
97 for(const auto &symbol_pair : symbols_transparent.symbols)
98 {
99 copied_symbol_table.add(symbol_pair.second);
100 }
101
102 typedef std::unordered_map<irep_idt, unsigned> unique_tagst;
103 unique_tagst unique_tags;
104
105 // add tags to anonymous union/struct/enum,
106 // and prepare lexicographic order
107 std::set<std::string> symbols_sorted;
108 for(const auto &named_symbol : copied_symbol_table.symbols)
109 {
110 symbolt &symbol = copied_symbol_table.get_writeable_ref(named_symbol.first);
111 bool tag_added=false;
112
113 // TODO we could get rid of some of the ID_anonymous by looking up
114 // the origin symbol types in typedef_types and adjusting any other
115 // uses of ID_tag
116 if((symbol.type.id()==ID_union || symbol.type.id()==ID_struct) &&
117 symbol.type.get(ID_tag).empty())
118 {
119 PRECONDITION(symbol.is_type);
120 symbol.type.set(ID_tag, ID_anonymous);
121 tag_added=true;
122 }
123 else if(symbol.type.id()==ID_c_enum &&
124 symbol.type.find(ID_tag).get(ID_C_base_name).empty())
125 {
126 PRECONDITION(symbol.is_type);
127 symbol.type.add(ID_tag).set(ID_C_base_name, ID_anonymous);
128 tag_added=true;
129 }
130
131 const std::string name_str=id2string(named_symbol.first);
132 if(symbol.is_type &&
133 (symbol.type.id()==ID_union ||
134 symbol.type.id()==ID_struct ||
135 symbol.type.id()==ID_c_enum))
136 {
137 std::string new_tag=symbol.type.id()==ID_c_enum?
138 symbol.type.find(ID_tag).get_string(ID_C_base_name):
139 symbol.type.get_string(ID_tag);
140
141 std::string::size_type tag_pos=new_tag.rfind("tag-");
142 if(tag_pos!=std::string::npos)
143 new_tag.erase(0, tag_pos+4);
144 const std::string new_tag_base=new_tag;
145
146 for(std::pair<unique_tagst::iterator, bool>
147 unique_entry=unique_tags.insert(std::make_pair(new_tag, 0));
148 !unique_entry.second;
149 unique_entry=unique_tags.insert(std::make_pair(new_tag, 0)))
150 {
151 new_tag=new_tag_base+"$"+
152 std::to_string(unique_entry.first->second);
153 ++(unique_entry.first->second);
154 }
155
156 if(symbol.type.id()==ID_c_enum)
157 {
158 symbol.type.add(ID_tag).set(ID_C_base_name, new_tag);
159 symbol.base_name=new_tag;
160 }
161 else
162 symbol.type.set(ID_tag, new_tag);
163 }
164
165 // we don't want to dump in full all definitions; in particular
166 // do not dump anonymous types that are defined in system headers
167 if((!tag_added || symbol.is_type) &&
170 continue;
171
172 bool inserted=symbols_sorted.insert(name_str).second;
173 CHECK_RETURN(inserted);
174 }
175
177
178 // collect all declarations we might need, include local static variables
179 bool skip_function_main=false;
180 std::vector<std::string> header_files;
181 for(std::set<std::string>::const_iterator
182 it=symbols_sorted.begin();
183 it!=symbols_sorted.end();
184 ++it)
185 {
186 const symbolt &symbol=ns.lookup(*it);
187 const irep_idt &type_id=symbol.type.id();
188
189 if(symbol.is_type &&
190 symbol.location.get_function().empty() &&
191 (type_id==ID_struct ||
192 type_id==ID_union ||
193 type_id==ID_c_enum))
194 {
196 {
197 global_decl_stream << "// " << symbol.name << '\n';
198 global_decl_stream << "// " << symbol.location << '\n';
199
200 std::string location_file =
201 get_base_name(id2string(symbol.location.get_file()), false);
202 // collect header the types are borrowed from
203 // expect header files to end in .h
204 if(
205 location_file.length() > 1 &&
206 location_file[location_file.length() - 1] == 'h')
207 {
208 std::vector<std::string>::iterator it =
209 find(header_files.begin(), header_files.end(), location_file);
210 if(it == header_files.end())
211 {
212 header_files.push_back(location_file);
213 global_decl_header_stream << "#include \"" << location_file
214 << "\"\n";
215 }
216 }
217
218 if(type_id==ID_c_enum)
219 convert_compound_enum(symbol.type, global_decl_stream);
220 else if(type_id == ID_struct)
221 {
222 global_decl_stream << type_to_string(struct_tag_typet{symbol.name})
223 << ";\n\n";
224 }
225 else
226 {
227 global_decl_stream << type_to_string(union_tag_typet{symbol.name})
228 << ";\n\n";
229 }
230 }
231 }
232 else if(
233 symbol.is_static_lifetime && symbol.type.id() != ID_code &&
234 !symbol.type.get_bool(ID_C_do_not_dump))
236 symbol,
237 global_var_stream,
238 local_static_decls);
239 else if(symbol.type.id()==ID_code)
240 {
241 goto_functionst::function_mapt::const_iterator func_entry=
242 goto_functions.function_map.find(symbol.name);
243
244 if(
245 !harness && func_entry != goto_functions.function_map.end() &&
246 func_entry->second.body_available() &&
247 (symbol.name == ID_main ||
248 (config.main.has_value() && symbol.name == config.main.value())))
249 {
250 skip_function_main=true;
251 }
252 }
253 }
254
255 // function declarations and definitions
256 for(std::set<std::string>::const_iterator
257 it=symbols_sorted.begin();
258 it!=symbols_sorted.end();
259 ++it)
260 {
261 const symbolt &symbol=ns.lookup(*it);
262
263 if(symbol.type.id()!=ID_code ||
264 symbol.is_type)
265 continue;
266
268 symbol,
269 skip_function_main,
270 func_decl_stream,
271 func_body_stream,
272 local_static_decls);
273 }
274
275 // (possibly modified) compound types
276 for(std::set<std::string>::const_iterator
277 it=symbols_sorted.begin();
278 it!=symbols_sorted.end();
279 ++it)
280 {
281 const symbolt &symbol=ns.lookup(*it);
282
283 if(
284 symbol.is_type &&
285 (symbol.type.id() == ID_struct || symbol.type.id() == ID_union))
287 symbol,
288 compound_body_stream);
289 }
290
291 // Dump the code to the target stream;
292 // the statements before to this point collect the code to dump!
293 for(std::set<std::string>::const_iterator
294 it=system_headers.begin();
295 it!=system_headers.end();
296 ++it)
297 os << "#include <" << *it << ">\n";
298 if(!system_headers.empty())
299 os << '\n';
300
301 if(!global_decl_header_stream.str().empty() && dump_c_config.include_headers)
302 os << global_decl_header_stream.str() << '\n';
303
304 if(global_var_stream.str().find("NULL")!=std::string::npos ||
305 func_body_stream.str().find("NULL")!=std::string::npos)
306 {
307 os << "#ifndef NULL\n"
308 << "#define NULL ((void*)0)\n"
309 << "#endif\n\n";
310 }
311 if(func_body_stream.str().find("FENCE")!=std::string::npos)
312 {
313 os << "#ifndef FENCE\n"
314 << "#define FENCE(x) ((void)0)\n"
315 << "#endif\n\n";
316 }
317 if(func_body_stream.str().find("IEEE_FLOAT_")!=std::string::npos)
318 {
319 os << "#ifndef IEEE_FLOAT_EQUAL\n"
320 << "#define IEEE_FLOAT_EQUAL(x,y) ((x)==(y))\n"
321 << "#endif\n"
322 << "#ifndef IEEE_FLOAT_NOTEQUAL\n"
323 << "#define IEEE_FLOAT_NOTEQUAL(x,y) ((x)!=(y))\n"
324 << "#endif\n\n";
325 }
326
327 if(!global_decl_stream.str().empty() && dump_c_config.include_global_decls)
328 os << global_decl_stream.str() << '\n';
329
331 dump_typedefs(os);
332
333 if(!func_decl_stream.str().empty() && dump_c_config.include_function_decls)
334 os << func_decl_stream.str() << '\n';
335 if(!compound_body_stream.str().empty() && dump_c_config.include_compounds)
336 os << compound_body_stream.str() << '\n';
337 if(!global_var_stream.str().empty() && dump_c_config.include_global_vars)
338 os << global_var_stream.str() << '\n';
340 os << func_body_stream.str();
341}
342
345 const symbolt &symbol,
346 std::ostream &os_body)
347{
348 if(
349 !symbol.location.get_function().empty() ||
350 symbol.type.get_bool(ID_C_do_not_dump))
351 {
352 return;
353 }
354
355 // do compound type body
356 if(symbol.type.id() == ID_struct)
358 symbol.type,
359 struct_tag_typet(symbol.name),
361 os_body);
362 else if(symbol.type.id() == ID_union)
364 symbol.type,
365 union_tag_typet(symbol.name),
367 os_body);
368 else if(symbol.type.id() == ID_c_enum)
370 symbol.type,
371 c_enum_tag_typet(symbol.name),
373 os_body);
374}
375
377 const typet &type,
378 const typet &unresolved,
379 bool recursive,
380 std::ostream &os)
381{
382 if(
383 type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
384 type.id() == ID_union_tag)
385 {
386 const symbolt &symbol = ns.lookup(to_tag_type(type));
387 DATA_INVARIANT(symbol.is_type, "tag expected to be type symbol");
388
390 convert_compound(symbol.type, unresolved, recursive, os);
391 }
392 else if(type.id()==ID_array || type.id()==ID_pointer)
393 {
394 if(!recursive)
395 return;
396
398 to_type_with_subtype(type).subtype(),
399 to_type_with_subtype(type).subtype(),
400 recursive,
401 os);
402
403 // sizeof may contain a type symbol that has to be declared first
404 if(type.id()==ID_array)
405 {
408
409 for(find_symbols_sett::const_iterator
410 it=syms.begin();
411 it!=syms.end();
412 ++it)
413 {
414 const symbolt &type_symbol = ns.lookup(*it);
415 irep_idt tag_kind =
416 type_symbol.type.id() == ID_c_enum
417 ? ID_c_enum_tag
418 : (type_symbol.type.id() == ID_union ? ID_union_tag
419 : ID_struct_tag);
420 tag_typet s_type(tag_kind, *it);
421 convert_compound(s_type, s_type, recursive, os);
422 }
423 }
424 }
425 else if(type.id()==ID_struct || type.id()==ID_union)
426 convert_compound(to_struct_union_type(type), unresolved, recursive, os);
427 else if(type.id()==ID_c_enum)
428 convert_compound_enum(type, os);
429}
430
432 const struct_union_typet &type,
433 const typet &unresolved,
434 bool recursive,
435 std::ostream &os)
436{
437 const irep_idt &name=type.get(ID_tag);
438
439 if(!converted_compound.insert(name).second || type.get_bool(ID_C_do_not_dump))
440 return;
441
442 // make sure typedef names used in the declaration are available
443 collect_typedefs(type, true);
444
445 const irept &bases = type.find(ID_bases);
446 std::stringstream base_decls;
447 for(const auto &parent : bases.get_sub())
448 {
450 (void)parent;
451#if 0
452 assert(parent.id() == ID_base);
453 assert(parent.get(ID_type) == ID_struct_tag);
454
455 const irep_idt &base_id=
456 parent.find(ID_type).get(ID_identifier);
457 const irep_idt &renamed_base_id=global_renaming[base_id];
458 const symbolt &parsymb=ns.lookup(renamed_base_id);
459
460 convert_compound_rec(parsymb.type, os);
461
462 base_decls << id2string(renamed_base_id) +
463 (parent_it+1==bases.get_sub().end()?"":", ");
464#endif
465 }
466
467#if 0
468 // for the constructor
469 string constructor_args;
470 string constructor_body;
471
472 std::string component_name = id2string(renaming[compo.get(ID_name)]);
473 assert(component_name != "");
474
475 if(it != struct_type.components().begin()) constructor_args += ", ";
476
477 if(compo.type().id() == ID_pointer)
478 constructor_args += type_to_string(compo.type()) + component_name;
479 else
480 constructor_args += "const " + type_to_string(compo.type()) + "& " + component_name;
481
482 constructor_body += indent + indent + "this->"+component_name + " = " + component_name + ";\n";
483#endif
484
485 std::stringstream struct_body;
486
487 for(const auto &comp : type.components())
488 {
489 const typet &comp_type = comp.type();
490
491 if(comp_type.id()==ID_code ||
492 comp.get_bool(ID_from_base) ||
493 comp.get_is_padding())
494 continue;
495
496 const typet *non_array_type = &comp_type;
497 while(non_array_type->id()==ID_array)
498 non_array_type = &(to_array_type(*non_array_type).element_type());
499
500 if(recursive)
501 {
502 if(non_array_type->id()!=ID_pointer)
503 convert_compound(comp.type(), comp.type(), recursive, os);
504 else
505 collect_typedefs(comp.type(), true);
506 }
507
508 irep_idt comp_name=comp.get_name();
509
510 struct_body << indent(1) << "// " << comp_name << '\n';
511 struct_body << indent(1);
512
513 // component names such as "main" would collide with other objects in the
514 // namespace
515 std::string fake_unique_name="NO/SUCH/NS::"+id2string(comp_name);
516 std::string s=make_decl(fake_unique_name, comp.type());
517 POSTCONDITION(s.find("NO/SUCH/NS")==std::string::npos);
518
519 if(comp_type.id()==ID_c_bit_field &&
520 to_c_bit_field_type(comp_type).get_width()==0)
521 {
522 comp_name.clear();
523 s=type_to_string(comp_type);
524 }
525
526 if(s.find(CPROVER_PREFIX "bitvector") == std::string::npos)
527 {
528 struct_body << s;
529 }
530 else if(comp_type.id()==ID_signedbv)
531 {
532 const signedbv_typet &t=to_signedbv_type(comp_type);
534 struct_body << "long long int " << comp_name
535 << " : " << t.get_width();
536 else if(mode == ID_cpp)
537 struct_body << "__signedbv<" << t.get_width() << "> "
538 << comp_name;
539 else
540 struct_body << s;
541 }
542 else if(comp_type.id()==ID_unsignedbv)
543 {
544 const unsignedbv_typet &t=to_unsignedbv_type(comp_type);
546 struct_body << "unsigned long long " << comp_name
547 << " : " << t.get_width();
548 else if(mode == ID_cpp)
549 struct_body << "__unsignedbv<" << t.get_width() << "> "
550 << comp_name;
551 else
552 struct_body << s;
553 }
554 else
556
557 struct_body << ";\n";
558 }
559
560 typet unresolved_clean=unresolved;
561 irep_idt typedef_str;
562 for(auto td_entry : typedef_types)
563 {
564 if(
565 td_entry.first.get(ID_identifier) == unresolved.get(ID_identifier) &&
566 (td_entry.first.source_location() == unresolved.source_location()))
567 {
568 unresolved_clean.remove(ID_C_typedef);
569 typedef_str = td_entry.second;
570 std::pair<typedef_mapt::iterator, bool> td_map_entry =
571 typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
572 PRECONDITION(!td_map_entry.second);
573 if(!td_map_entry.first->second.early)
574 td_map_entry.first->second.type_decl_str.clear();
575 os << "typedef ";
576 break;
577 }
578 }
579
580 os << type_to_string(unresolved_clean);
581 if(!base_decls.str().empty())
582 {
583 PRECONDITION(mode == ID_cpp);
584 os << ": " << base_decls.str();
585 }
586 os << '\n';
587 os << "{\n";
588 os << struct_body.str();
589
590 /*
591 if(!struct_type.components().empty())
592 {
593 os << indent << name << "(){}\n";
594 os << indent << "explicit " << name
595 << "(" + constructor_args + ")\n";
596 os << indent << "{\n";
597 os << constructor_body;
598 os << indent << "}\n";
599 }
600 */
601
602 os << "}";
603 if(type.get_bool(ID_C_transparent_union))
604 os << " __attribute__ ((__transparent_union__))";
605 if(type.get_bool(ID_C_packed))
606 os << " __attribute__ ((__packed__))";
607 if(!typedef_str.empty())
608 os << " " << typedef_str;
609 os << ";\n\n";
610}
611
613 const typet &type,
614 std::ostream &os)
615{
616 PRECONDITION(type.id()==ID_c_enum);
617
618 const irept &tag=type.find(ID_tag);
619 const irep_idt &name=tag.get(ID_C_base_name);
620
621 if(tag.is_nil() ||
622 !converted_enum.insert(name).second)
623 return;
624
625 c_enum_typet enum_type=to_c_enum_type(type);
626 c_enum_typet::memberst &members=
627 (c_enum_typet::memberst &)(enum_type.add(ID_body).get_sub());
628 for(c_enum_typet::memberst::iterator
629 it=members.begin();
630 it!=members.end();
631 ++it)
632 {
633 const irep_idt bn=it->get_base_name();
634
635 if(declared_enum_constants.find(bn)!=
638 {
639 std::string new_bn=id2string(name)+"$$"+id2string(bn);
640 it->set_base_name(new_bn);
641 }
642
644 std::make_pair(bn, it->get_base_name()));
645 }
646
647 os << type_to_string(enum_type);
648
649 if(enum_type.get_bool(ID_C_packed))
650 os << " __attribute__ ((__packed__))";
651
652 os << ";\n\n";
653}
654
657 std::list<irep_idt> &local_static,
658 std::list<irep_idt> &local_type_decls)
659{
660 goto_programt tmp;
662
663 if(optionalt<exprt> value = decl.initial_value())
664 {
665 decl.set_initial_value({});
666 tmp.add(goto_programt::make_assignment(decl.symbol(), std::move(*value)));
667 }
668
670
671 // goto_program2codet requires valid location numbers:
672 tmp.update();
673
674 std::unordered_set<irep_idt> typedef_names;
675 for(const auto &td : typedef_map)
676 typedef_names.insert(td.first);
677
678 code_blockt b;
680 irep_idt(),
681 tmp,
683 b,
684 local_static,
685 local_type_decls,
686 typedef_names,
688 p2s();
689
690 POSTCONDITION(b.statements().size() == 1);
691 decl.swap(b.op0());
692}
693
699void dump_ct::collect_typedefs(const typet &type, bool early)
700{
701 std::unordered_set<irep_idt> deps;
702 collect_typedefs_rec(type, early, deps);
703}
704
713 const typet &type,
714 bool early,
715 std::unordered_set<irep_idt> &dependencies)
716{
718 return;
719
720 std::unordered_set<irep_idt> local_deps;
721
722 if(type.id()==ID_code)
723 {
724 const code_typet &code_type=to_code_type(type);
725
726 collect_typedefs_rec(code_type.return_type(), early, local_deps);
727 for(const auto &param : code_type.parameters())
728 collect_typedefs_rec(param.type(), early, local_deps);
729 }
730 else if(type.id()==ID_pointer || type.id()==ID_array)
731 {
733 to_type_with_subtype(type).subtype(), early, local_deps);
734 }
735 else if(
736 type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
737 type.id() == ID_union_tag)
738 {
739 const symbolt &symbol = ns.lookup(to_tag_type(type));
740 collect_typedefs_rec(symbol.type, early, local_deps);
741 }
742
743 const irep_idt &typedef_str=type.get(ID_C_typedef);
744
745 if(!typedef_str.empty())
746 {
747 std::pair<typedef_mapt::iterator, bool> entry=
748 typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
749
750 if(entry.second ||
751 (early && entry.first->second.type_decl_str.empty()))
752 {
753 if(typedef_str=="__gnuc_va_list" || typedef_str == "va_list")
754 {
755 system_headers.insert("stdarg.h");
756 early=false;
757 }
758 else
759 {
760 typet t=type;
761 t.remove(ID_C_typedef);
762
763 std::ostringstream oss;
764 oss << "typedef " << make_decl(typedef_str, t) << ';';
765
766 entry.first->second.type_decl_str=oss.str();
767 entry.first->second.dependencies=local_deps;
768 }
769 }
770
771 if(early)
772 {
773 entry.first->second.early=true;
774
775 for(const auto &d : local_deps)
776 {
777 auto td_entry=typedef_map.find(d);
778 PRECONDITION(td_entry!=typedef_map.end());
779 td_entry->second.early=true;
780 }
781 }
782
783 dependencies.insert(typedef_str);
784 }
785
786 dependencies.insert(local_deps.begin(), local_deps.end());
787}
788
791{
792 // sort the symbols first to ensure deterministic replacement in
793 // typedef_types below as there could be redundant declarations
794 // typedef int x;
795 // typedef int y;
796 std::map<std::string, symbolt> symbols_sorted;
797 for(const auto &symbol_entry : copied_symbol_table.symbols)
798 symbols_sorted.insert(
799 {id2string(symbol_entry.first), symbol_entry.second});
800
801 for(const auto &symbol_entry : symbols_sorted)
802 {
803 const symbolt &symbol=symbol_entry.second;
804
805 if(symbol.is_macro && symbol.is_type &&
806 symbol.location.get_function().empty())
807 {
808 const irep_idt &typedef_str=symbol.type.get(ID_C_typedef);
809 PRECONDITION(!typedef_str.empty());
810 typedef_types[symbol.type]=typedef_str;
812 typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
813 else
814 collect_typedefs(symbol.type, false);
815 }
816 }
817}
818
821void dump_ct::dump_typedefs(std::ostream &os) const
822{
823 // we need to compute a topological sort; we do so by picking all
824 // typedefs the dependencies of which have been emitted into to_insert
825 std::vector<typedef_infot> typedefs_sorted;
826 typedefs_sorted.reserve(typedef_map.size());
827
828 // elements in to_insert are lexicographically sorted and ready for
829 // output
830 std::map<std::string, typedef_infot> to_insert;
831
832 std::unordered_set<irep_idt> typedefs_done;
833 std::unordered_map<irep_idt, std::unordered_set<irep_idt>> forward_deps,
834 reverse_deps;
835
836 for(const auto &td : typedef_map)
837 if(!td.second.type_decl_str.empty())
838 {
839 if(td.second.dependencies.empty())
840 // those can be dumped immediately
841 to_insert.insert({id2string(td.first), td.second});
842 else
843 {
844 // delay them until dependencies are dumped
845 forward_deps.insert({td.first, td.second.dependencies});
846 for(const auto &d : td.second.dependencies)
847 reverse_deps[d].insert(td.first);
848 }
849 }
850
851 while(!to_insert.empty())
852 {
853 // the topologically next element (lexicographically ranked first
854 // among all the dependencies of which have been dumped)
855 typedef_infot t=to_insert.begin()->second;
856 to_insert.erase(to_insert.begin());
857 // move to the output queue
858 typedefs_sorted.push_back(t);
859
860 // find any depending typedefs that are now valid, or at least
861 // reduce the remaining dependencies
862 auto r_it=reverse_deps.find(t.typedef_name);
863 if(r_it==reverse_deps.end())
864 continue;
865
866 // reduce remaining dependencies
867 std::unordered_set<irep_idt> &r_deps = r_it->second;
868 for(std::unordered_set<irep_idt>::iterator it = r_deps.begin();
869 it != r_deps.end();) // no ++it
870 {
871 auto f_it=forward_deps.find(*it);
872 if(f_it==forward_deps.end()) // might be done already
873 {
874 it=r_deps.erase(it);
875 continue;
876 }
877
878 // update dependencies
879 std::unordered_set<irep_idt> &f_deps = f_it->second;
880 PRECONDITION(!f_deps.empty());
881 PRECONDITION(f_deps.find(t.typedef_name)!=f_deps.end());
882 f_deps.erase(t.typedef_name);
883
884 if(f_deps.empty()) // all depenencies done now!
885 {
886 const auto td_entry=typedef_map.find(*it);
887 PRECONDITION(td_entry!=typedef_map.end());
888 to_insert.insert({id2string(*it), td_entry->second});
889 forward_deps.erase(*it);
890 it=r_deps.erase(it);
891 }
892 else
893 ++it;
894 }
895 }
896
897 POSTCONDITION(forward_deps.empty());
898
899 for(const auto &td : typedefs_sorted)
900 os << td.type_decl_str << '\n';
901
902 if(!typedefs_sorted.empty())
903 os << '\n';
904}
905
907 const symbolt &symbol,
908 std::ostream &os,
909 local_static_declst &local_static_decls)
910{
911 const irep_idt &func=symbol.location.get_function();
912 if((func.empty() || symbol.is_extern || symbol.value.is_not_nil()) &&
913 !converted_global.insert(symbol.name).second)
914 return;
915
917
919 if(symbol.value.is_not_nil())
920 find_symbols_or_nexts(symbol.value, syms);
921
922 // add a tentative declaration to cater for symbols in the initializer
923 // relying on it this symbol
924 if((func.empty() || symbol.is_extern) &&
925 (symbol.value.is_nil() || !syms.empty()))
926 {
927 os << "// " << symbol.name << '\n';
928 os << "// " << symbol.location << '\n';
929 os << expr_to_string(d) << '\n';
930 }
931
932 if(!symbol.value.is_nil())
933 {
934 std::set<std::string> symbols_sorted;
935 for(find_symbols_sett::const_iterator
936 it=syms.begin();
937 it!=syms.end();
938 ++it)
939 {
940 bool inserted=symbols_sorted.insert(id2string(*it)).second;
941 CHECK_RETURN(inserted);
942 }
943
944 for(std::set<std::string>::const_iterator
945 it=symbols_sorted.begin();
946 it!=symbols_sorted.end();
947 ++it)
948 {
949 const symbolt &sym=ns.lookup(*it);
950 if(!sym.is_type && sym.is_static_lifetime && sym.type.id()!=ID_code)
951 convert_global_variable(sym, os, local_static_decls);
952 }
953
954 d.copy_to_operands(symbol.value);
955 }
956
957 if(!func.empty() && !symbol.is_extern)
958 {
959 local_static_decls.emplace(symbol.name, d);
960 }
961 else if(!symbol.value.is_nil())
962 {
963 os << "// " << symbol.name << '\n';
964 os << "// " << symbol.location << '\n';
965
966 std::list<irep_idt> empty_static, empty_types;
967 cleanup_decl(d, empty_static, empty_types);
968 CHECK_RETURN(empty_static.empty());
969 os << expr_to_string(d) << '\n';
970 }
971}
972
977{
979 code_blockt decls;
980
981 const symbolt *argc_sym=nullptr;
982 if(!ns.lookup("argc'", argc_sym))
983 {
984 symbol_exprt argc("argc", argc_sym->type);
985 replace.insert(argc_sym->symbol_expr(), argc);
986 code_declt d(argc);
987 decls.add(d);
988 }
989 const symbolt *argv_sym=nullptr;
990 if(!ns.lookup("argv'", argv_sym))
991 {
992 symbol_exprt argv("argv", argv_sym->type);
993 // replace argc' by argc in the type of argv['] to maintain type consistency
994 // while replacing
995 replace(argv);
996 replace.insert(symbol_exprt(argv_sym->name, argv.type()), argv);
997 code_declt d(argv);
998 decls.add(d);
999 }
1000 const symbolt *return_sym=nullptr;
1001 if(!ns.lookup("return'", return_sym))
1002 {
1003 symbol_exprt return_value("return_value", return_sym->type);
1004 replace.insert(return_sym->symbol_expr(), return_value);
1005 code_declt d(return_value);
1006 decls.add(d);
1007 }
1008
1009 for(auto &code : b.statements())
1010 {
1011 if(code.get_statement()==ID_function_call)
1012 {
1013 exprt &func=to_code_function_call(code).function();
1014 if(func.id()==ID_symbol)
1015 {
1017 if(s.get_identifier()==ID_main)
1019 else if(s.get_identifier() == INITIALIZE_FUNCTION)
1020 continue;
1021 }
1022 }
1023
1024 decls.add(code);
1025 }
1026
1027 b.swap(decls);
1028 replace(b);
1029}
1030
1032 const symbolt &symbol,
1033 const bool skip_main,
1034 std::ostream &os_decl,
1035 std::ostream &os_body,
1036 local_static_declst &local_static_decls)
1037{
1038 // don't dump artificial main
1039 if(skip_main && symbol.name==goto_functionst::entry_point())
1040 return;
1041
1042 // convert the goto program back to code - this might change
1043 // the function type
1044 goto_functionst::function_mapt::const_iterator func_entry=
1045 goto_functions.function_map.find(symbol.name);
1046 if(func_entry!=goto_functions.function_map.end() &&
1047 func_entry->second.body_available())
1048 {
1049 code_blockt b;
1050 std::list<irep_idt> type_decls, local_static;
1051
1052 std::unordered_set<irep_idt> typedef_names;
1053 for(const auto &td : typedef_map)
1054 typedef_names.insert(td.first);
1055
1057 symbol.name,
1058 func_entry->second.body,
1060 b,
1061 local_static,
1062 type_decls,
1063 typedef_names,
1065 p2s();
1066
1068 b,
1069 local_static,
1070 local_static_decls,
1071 type_decls);
1072
1073 convertedt converted_c_bak(converted_compound);
1074 convertedt converted_e_bak(converted_enum);
1075
1077 enum_constants_bak(declared_enum_constants);
1078
1080 b,
1081 type_decls);
1082
1083 converted_enum.swap(converted_e_bak);
1084 converted_compound.swap(converted_c_bak);
1085
1086 if(harness && symbol.name==goto_functions.entry_point())
1087 cleanup_harness(b);
1088
1089 os_body << "// " << symbol.name << '\n';
1090 os_body << "// " << symbol.location << '\n';
1091 if(symbol.name==goto_functions.entry_point())
1092 os_body << make_decl(ID_main, symbol.type) << '\n';
1093 else if(!harness || symbol.name!=ID_main)
1094 os_body << make_decl(symbol.name, symbol.type) << '\n';
1095 else if(harness && symbol.name==ID_main)
1096 {
1097 os_body << make_decl(CPROVER_PREFIX+id2string(symbol.name), symbol.type)
1098 << '\n';
1099 }
1100 os_body << expr_to_string(b);
1101 os_body << "\n\n";
1102
1103 declared_enum_constants.swap(enum_constants_bak);
1104 }
1105
1106 if(symbol.name!=goto_functionst::entry_point() &&
1107 symbol.name!=ID_main)
1108 {
1109 os_decl << "// " << symbol.name << '\n';
1110 os_decl << "// " << symbol.location << '\n';
1111 os_decl << make_decl(symbol.name, symbol.type) << ";\n";
1112 }
1113 else if(harness && symbol.name==ID_main)
1114 {
1115 os_decl << "// " << symbol.name << '\n';
1116 os_decl << "// " << symbol.location << '\n';
1117 os_decl << make_decl(CPROVER_PREFIX+id2string(symbol.name), symbol.type)
1118 << ";\n";
1119 }
1120
1121 // make sure typedef names used in the function declaration are
1122 // available
1123 collect_typedefs(symbol.type, true);
1124}
1125
1127 const irep_idt &identifier,
1128 codet &root,
1129 code_blockt* &dest,
1130 exprt::operandst::iterator &before)
1131{
1132 if(!root.has_operands())
1133 return false;
1134
1135 code_blockt *our_dest=nullptr;
1136
1137 exprt::operandst &operands=root.operands();
1138 exprt::operandst::iterator first_found=operands.end();
1139
1140 Forall_expr(it, operands)
1141 {
1142 bool found=false;
1143
1144 // be aware of the skip-carries-type hack
1145 if(it->id()==ID_code &&
1146 to_code(*it).get_statement()!=ID_skip)
1148 identifier,
1149 to_code(*it),
1150 our_dest,
1151 before);
1152 else
1153 {
1154 find_symbols_sett syms;
1155 find_type_and_expr_symbols(*it, syms);
1156
1157 found=syms.find(identifier)!=syms.end();
1158 }
1159
1160 if(!found)
1161 continue;
1162
1163 if(!our_dest)
1164 {
1165 // first containing block
1166 if(root.get_statement()==ID_block)
1167 {
1168 dest=&(to_code_block(root));
1169 before=it;
1170 }
1171
1172 return true;
1173 }
1174 else
1175 {
1176 // there is a containing block and this is the first operand
1177 // that contains identifier
1178 if(first_found==operands.end())
1179 first_found=it;
1180 // we have seen it already - pick the first occurrence in this
1181 // block
1182 else if(root.get_statement()==ID_block)
1183 {
1184 dest=&(to_code_block(root));
1185 before=first_found;
1186
1187 return true;
1188 }
1189 // we have seen it already - outer block has to deal with this
1190 else
1191 return true;
1192 }
1193 }
1194
1195 if(first_found!=operands.end())
1196 {
1197 dest=our_dest;
1198
1199 return true;
1200 }
1201
1202 return false;
1203}
1204
1206 code_blockt &b,
1207 const std::list<irep_idt> &local_static,
1208 local_static_declst &local_static_decls,
1209 std::list<irep_idt> &type_decls)
1210{
1211 // look up last identifier first as its value may introduce the
1212 // other ones
1213 for(std::list<irep_idt>::const_reverse_iterator
1214 it=local_static.rbegin();
1215 it!=local_static.rend();
1216 ++it)
1217 {
1218 local_static_declst::const_iterator d_it=
1219 local_static_decls.find(*it);
1220 PRECONDITION(d_it!=local_static_decls.end());
1221
1222 code_frontend_declt d = d_it->second;
1223 std::list<irep_idt> redundant;
1224 cleanup_decl(d, redundant, type_decls);
1225
1226 code_blockt *dest_ptr=nullptr;
1227 exprt::operandst::iterator before=b.operands().end();
1228
1229 // some use of static variables might be optimised out if it is
1230 // within an if(false) { ... } block
1231 if(find_block_position_rec(*it, b, dest_ptr, before))
1232 {
1233 CHECK_RETURN(dest_ptr!=nullptr);
1234 dest_ptr->operands().insert(before, d);
1235 }
1236 }
1237}
1238
1240 code_blockt &b,
1241 const std::list<irep_idt> &type_decls)
1242{
1243 // look up last identifier first as its value may introduce the
1244 // other ones
1245 for(std::list<irep_idt>::const_reverse_iterator
1246 it=type_decls.rbegin();
1247 it!=type_decls.rend();
1248 ++it)
1249 {
1250 const typet &type=ns.lookup(*it).type;
1251 // feed through plain C to expr2c by ending and re-starting
1252 // a comment block ...
1253 std::ostringstream os_body;
1254 os_body << *it << " */\n";
1255 irep_idt tag_kind =
1256 type.id() == ID_c_enum
1257 ? ID_c_enum_tag
1258 : (type.id() == ID_union ? ID_union_tag : ID_struct_tag);
1259 convert_compound(type, tag_typet(tag_kind, *it), false, os_body);
1260 os_body << "/*";
1261
1262 code_skipt skip;
1263 skip.add_source_location().set_comment(os_body.str());
1264 // another hack to ensure symbols inside types are seen
1265 skip.type()=type;
1266
1267 code_blockt *dest_ptr=nullptr;
1268 exprt::operandst::iterator before=b.operands().end();
1269
1270 // we might not find it in case a transparent union type cast
1271 // has been removed by cleanup operations
1272 if(find_block_position_rec(*it, b, dest_ptr, before))
1273 {
1274 CHECK_RETURN(dest_ptr!=nullptr);
1275 dest_ptr->operands().insert(before, skip);
1276 }
1277 }
1278}
1279
1281{
1282 Forall_operands(it, expr)
1283 cleanup_expr(*it);
1284
1285 cleanup_type(expr.type());
1286
1287 if(expr.id()==ID_struct)
1288 {
1289 struct_typet type=
1290 to_struct_type(ns.follow(expr.type()));
1291
1292 struct_union_typet::componentst old_components;
1293 old_components.swap(type.components());
1294
1295 exprt::operandst old_ops;
1296 old_ops.swap(expr.operands());
1297
1298 PRECONDITION(old_components.size()==old_ops.size());
1299 exprt::operandst::iterator o_it=old_ops.begin();
1300 for(const auto &old_comp : old_components)
1301 {
1302 const bool is_zero_bit_field =
1303 old_comp.type().id() == ID_c_bit_field &&
1304 to_c_bit_field_type(old_comp.type()).get_width() == 0;
1305
1306 if(!old_comp.get_is_padding() && !is_zero_bit_field)
1307 {
1308 type.components().push_back(old_comp);
1309 expr.add_to_operands(std::move(*o_it));
1310 }
1311 ++o_it;
1312 }
1313 expr.type().swap(type);
1314 }
1315 else if(expr.id()==ID_union)
1316 {
1317 union_exprt &u=to_union_expr(expr);
1318 const union_typet &u_type_f=to_union_type(ns.follow(u.type()));
1319
1320 if(!u.type().get_bool(ID_C_transparent_union) &&
1321 !u_type_f.get_bool(ID_C_transparent_union))
1322 {
1324 // we just use an empty struct to fake an empty union
1325 expr = struct_exprt({}, struct_typet());
1326 }
1327 // add a typecast for NULL
1328 else if(u.op().id()==ID_constant &&
1329 u.op().type().id()==ID_pointer &&
1330 u.op().type().subtype().id()==ID_empty &&
1331 (u.op().is_zero() ||
1332 to_constant_expr(u.op()).get_value()==ID_NULL))
1333 {
1335 u_type_f.get_component(u.get_component_name());
1336 const typet &u_op_type=comp.type();
1337 PRECONDITION(u_op_type.id()==ID_pointer);
1338
1339 typecast_exprt tc(u.op(), u_op_type);
1340 expr.swap(tc);
1341 }
1342 else
1343 {
1344 exprt tmp;
1345 tmp.swap(u.op());
1346 expr.swap(tmp);
1347 }
1348 }
1349 else if(
1350 expr.id() == ID_typecast &&
1351 to_typecast_expr(expr).op().id() == ID_typecast &&
1352 expr.type() == to_typecast_expr(expr).op().type())
1353 {
1354 exprt tmp = to_typecast_expr(expr).op();
1355 expr.swap(tmp);
1356 }
1357 else if(expr.id()==ID_code &&
1358 to_code(expr).get_statement()==ID_function_call &&
1359 to_code_function_call(to_code(expr)).function().id()==ID_symbol)
1360 {
1362 const symbol_exprt &fn=to_symbol_expr(call.function());
1364
1365 // don't edit function calls we might have introduced
1366 const symbolt *s;
1367 if(!ns.lookup(fn.get_identifier(), s))
1368 {
1369 const symbolt &fn_sym=ns.lookup(fn.get_identifier());
1370 const code_typet &code_type=to_code_type(fn_sym.type);
1371 const code_typet::parameterst &parameters=code_type.parameters();
1372
1373 if(parameters.size()==arguments.size())
1374 {
1375 code_typet::parameterst::const_iterator it=parameters.begin();
1376 for(auto &argument : arguments)
1377 {
1378 const typet &type=ns.follow(it->type());
1379 if(type.id()==ID_union &&
1380 type.get_bool(ID_C_transparent_union))
1381 {
1382 if(argument.id() == ID_typecast && argument.type() == type)
1383 argument = to_typecast_expr(argument).op();
1384
1385 // add a typecast for NULL or 0
1386 if(
1387 argument.id() == ID_constant &&
1388 (argument.is_zero() ||
1389 to_constant_expr(argument).get_value() == ID_NULL))
1390 {
1391 const typet &comp_type=
1392 to_union_type(type).components().front().type();
1393
1394 if(comp_type.id()==ID_pointer)
1395 argument = typecast_exprt(argument, comp_type);
1396 }
1397 }
1398
1399 ++it;
1400 }
1401 }
1402 }
1403 }
1404 else if(expr.id()==ID_constant &&
1405 expr.type().id()==ID_signedbv)
1406 {
1407 #if 0
1408 const irep_idt &cformat=expr.get(ID_C_cformat);
1409
1410 if(!cformat.empty())
1411 {
1412 declared_enum_constants_mapt::const_iterator entry=
1413 declared_enum_constants.find(cformat);
1414
1415 if(entry!=declared_enum_constants.end() &&
1416 entry->first!=entry->second)
1417 expr.set(ID_C_cformat, entry->second);
1418 else if(entry==declared_enum_constants.end() &&
1419 !std::isdigit(id2string(cformat)[0]))
1420 expr.remove(ID_C_cformat);
1421 }
1422 #endif
1423 }
1424 else if(
1425 expr.id() == ID_byte_update_little_endian ||
1426 expr.id() == ID_byte_update_big_endian)
1427 {
1428 const byte_update_exprt &bu = to_byte_update_expr(expr);
1429
1430 if(bu.op().id() == ID_union && bu.offset().is_zero())
1431 {
1432 const union_exprt &union_expr = to_union_expr(bu.op());
1433 const union_typet &union_type =
1434 to_union_type(ns.follow(union_expr.type()));
1435
1436 for(const auto &comp : union_type.components())
1437 {
1438 if(bu.value().type() == comp.type())
1439 {
1440 exprt member1{ID_member};
1441 member1.set(ID_component_name, union_expr.get_component_name());
1442 exprt designated_initializer1{ID_designated_initializer};
1443 designated_initializer1.add_to_operands(union_expr.op());
1444 designated_initializer1.add(ID_designator).move_to_sub(member1);
1445
1446 exprt member2{ID_member};
1447 member2.set(ID_component_name, comp.get_name());
1448 exprt designated_initializer2{ID_designated_initializer};
1449 designated_initializer2.add_to_operands(bu.value());
1450 designated_initializer2.add(ID_designator).move_to_sub(member2);
1451
1452 binary_exprt initializer_list{std::move(designated_initializer1),
1453 ID_initializer_list,
1454 std::move(designated_initializer2)};
1455 expr.swap(initializer_list);
1456
1457 return;
1458 }
1459 }
1460 }
1461 else if(
1462 bu.op().id() == ID_side_effect &&
1463 to_side_effect_expr(bu.op()).get_statement() == ID_nondet &&
1464 ns.follow(bu.op().type()).id() == ID_union && bu.offset().is_zero())
1465 {
1466 const union_typet &union_type = to_union_type(ns.follow(bu.op().type()));
1467
1468 for(const auto &comp : union_type.components())
1469 {
1470 if(bu.value().type() == comp.type())
1471 {
1472 union_exprt union_expr{comp.get_name(), bu.value(), bu.op().type()};
1473 expr.swap(union_expr);
1474
1475 return;
1476 }
1477 }
1478 }
1479
1480 optionalt<exprt> clean_init;
1481 if(
1482 ns.follow(bu.type()).id() == ID_union &&
1484 {
1485 clean_init = zero_initializer(bu.op().type(), source_locationt{}, ns)
1486 .value_or(nil_exprt{});
1487 if(clean_init->id() != ID_struct || clean_init->has_operands())
1488 cleanup_expr(*clean_init);
1489 }
1490
1491 if(clean_init.has_value() && bu.op() == *clean_init)
1492 {
1493 const union_typet &union_type = to_union_type(ns.follow(bu.type()));
1494
1495 for(const auto &comp : union_type.components())
1496 {
1497 if(bu.value().type() == comp.type())
1498 {
1499 union_exprt union_expr{comp.get_name(), bu.value(), bu.type()};
1500 expr.swap(union_expr);
1501
1502 return;
1503 }
1504 }
1505
1506 // we still haven't found a suitable component, so just ignore types and
1507 // build an initializer list without designators
1508 expr = unary_exprt{ID_initializer_list, bu.value()};
1509 }
1510 }
1511}
1512
1514{
1515 for(typet &subtype : to_type_with_subtypes(type).subtypes())
1516 cleanup_type(subtype);
1517
1518 if(type.id()==ID_code)
1519 {
1520 code_typet &code_type=to_code_type(type);
1521
1522 cleanup_type(code_type.return_type());
1523
1524 for(code_typet::parameterst::iterator
1525 it=code_type.parameters().begin();
1526 it!=code_type.parameters().end();
1527 ++it)
1528 cleanup_type(it->type());
1529 }
1530
1531 if(type.id()==ID_array)
1532 cleanup_expr(to_array_type(type).size());
1533
1535 (type.id()!=ID_union && type.id()!=ID_struct) ||
1536 !type.get(ID_tag).empty());
1537}
1538
1540{
1541 // future TODO: with C++20 we can actually use designated initializers as
1542 // commented out below
1543 static expr2c_configurationt configuration{
1544 /* .include_struct_padding_components = */ true,
1545 /* .print_struct_body_in_type = */ true,
1546 /* .include_array_size = */ true,
1547 /* .true_string = */ "1",
1548 /* .false_string = */ "0",
1549 /* .use_library_macros = */ true,
1550 /* .print_enum_int_value = */ false,
1551 /* .expand_typedef = */ false};
1552
1553 return configuration;
1554}
1555
1556std::string dump_ct::type_to_string(const typet &type)
1557{
1558 std::string ret;
1559 typet t=type;
1560 cleanup_type(t);
1561
1562 if(mode == ID_C)
1563 return type2c(t, ns, expr2c_configuration());
1564 else if(mode == ID_cpp)
1565 return type2cpp(t, ns);
1566 else
1568}
1569
1570std::string dump_ct::expr_to_string(const exprt &expr)
1571{
1572 std::string ret;
1573 exprt e=expr;
1574 cleanup_expr(e);
1575
1576 if(mode == ID_C)
1577 return expr2c(e, ns, expr2c_configuration());
1578 else if(mode == ID_cpp)
1579 return expr2cpp(e, ns);
1580 else
1582}
1583
1585 const goto_functionst &src,
1586 const bool use_system_headers,
1587 const bool use_all_headers,
1588 const bool include_harness,
1589 const namespacet &ns,
1590 std::ostream &out)
1591{
1592 dump_ct goto2c(
1593 src, use_system_headers, use_all_headers, include_harness, ns, ID_C);
1594 out << goto2c;
1595}
1596
1598 const goto_functionst &src,
1599 const bool use_system_headers,
1600 const bool use_all_headers,
1601 const bool include_harness,
1602 const namespacet &ns,
1603 std::ostream &out)
1604{
1605 dump_ct goto2cpp(
1606 src, use_system_headers, use_all_headers, include_harness, ns, ID_cpp);
1607 out << goto2cpp;
1608}
1609
1610static bool
1611module_local_declaration(const symbolt &symbol, const std::string module)
1612{
1613 std::string base_name =
1614 get_base_name(id2string(symbol.location.get_file()), true);
1615 std::string symbol_module = strip_string(id2string(symbol.module));
1616 return (base_name == module && symbol_module == module);
1617}
1618
1620 const goto_functionst &src,
1621 const bool use_system_headers,
1622 const bool use_all_headers,
1623 const bool include_harness,
1624 const namespacet &ns,
1625 const std::string module,
1626 std::ostream &out)
1627{
1628 symbol_tablet symbol_table = ns.get_symbol_table();
1629 for(symbol_tablet::iteratort it = symbol_table.begin();
1630 it != symbol_table.end();
1631 it++)
1632 {
1633 symbolt &new_symbol = it.get_writeable_symbol();
1634 if(module_local_declaration(new_symbol, module))
1635 {
1636 new_symbol.type.set(ID_C_do_not_dump, 0);
1637 }
1638 else
1639 {
1640 new_symbol.type.set(ID_C_do_not_dump, 1);
1641 }
1642 }
1643
1644 namespacet new_ns(symbol_table);
1645 dump_ct goto2c(
1646 src,
1647 use_system_headers,
1648 use_all_headers,
1649 include_harness,
1650 new_ns,
1651 ID_C,
1653 out << goto2c;
1654}
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: c_types.h:58
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:162
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
A base class for binary expressions.
Definition: std_expr.h:550
std::size_t get_width() const
Definition: std_types.h:864
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & offset() const
const exprt & op() const
const exprt & value() const
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:319
The type of C enums.
Definition: c_types.h:217
std::vector< c_enum_membert > memberst
Definition: c_types.h:253
A codet representing sequential composition of program statements.
Definition: std_code.h:130
code_operandst & statements()
Definition: std_code.h:138
void add(const codet &code)
Definition: std_code.h:168
A codet representing the declaration of a local variable.
A codet representing the declaration of a local variable.
Definition: std_code.h:347
void set_initial_value(optionalt< exprt > initial_value)
Sets the value to which this declaration initializes the declared variable.
Definition: std_code.h:384
symbol_exprt & symbol()
Definition: std_code.h:354
optionalt< exprt > initial_value() const
Returns the initial value to which the declared variable is initialized, or empty in the case where n...
Definition: std_code.h:373
codet representation of a function call statement.
exprt::operandst argumentst
A codet representing a skip statement.
Definition: std_code.h:322
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:542
const parameterst & parameters() const
Definition: std_types.h:655
const typet & return_type() const
Definition: std_types.h:645
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt & op0()
Definition: expr.h:99
const irep_idt & get_statement() const
Definition: std_code_base.h:65
optionalt< std::string > main
Definition: config.h:326
struct configt::ansi_ct ansi_c
const irep_idt & get_value() const
Definition: std_expr.h:2815
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
void clear()
Definition: dstring.h:142
std::unordered_set< irep_idt > convertedt
Definition: dump_c_class.h:160
void convert_compound_declaration(const symbolt &symbol, std::ostream &os_body)
declare compound types
Definition: dump_c.cpp:344
void convert_compound(const typet &type, const typet &unresolved, bool recursive, std::ostream &os)
Definition: dump_c.cpp:376
const namespacet ns
Definition: dump_c_class.h:155
void insert_local_type_decls(code_blockt &b, const std::list< irep_idt > &type_decls)
Definition: dump_c.cpp:1239
void cleanup_expr(exprt &expr)
Definition: dump_c.cpp:1280
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)
Definition: dump_c.cpp:1205
std::string expr_to_string(const exprt &expr)
Definition: dump_c.cpp:1570
void operator()(std::ostream &out)
Definition: dump_c.cpp:50
const goto_functionst & goto_functions
Definition: dump_c_class.h:153
convertedt converted_compound
Definition: dump_c_class.h:161
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...
Definition: dump_c.cpp:699
void gather_global_typedefs()
Find all global typdefs in the symbol table and store them in typedef_types.
Definition: dump_c.cpp:790
typedef_typest typedef_types
Definition: dump_c_class.h:186
symbol_tablet copied_symbol_table
Definition: dump_c_class.h:154
typedef_mapt typedef_map
Definition: dump_c_class.h:184
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...
Definition: dump_c.cpp:712
declared_enum_constants_mapt declared_enum_constants
Definition: dump_c_class.h:168
std::string make_decl(const irep_idt &identifier, const typet &type)
Definition: dump_c_class.h:196
convertedt converted_enum
Definition: dump_c_class.h:161
const irep_idt mode
Definition: dump_c_class.h:157
void convert_global_variable(const symbolt &symbol, std::ostream &os, local_static_declst &local_static_decls)
Definition: dump_c.cpp:906
std::set< std::string > system_headers
Definition: dump_c_class.h:163
void dump_typedefs(std::ostream &os) const
Print all typedefs that are not covered via typedef struct xyz { ... } name;.
Definition: dump_c.cpp:821
const bool harness
Definition: dump_c_class.h:158
system_library_symbolst system_symbols
Definition: dump_c_class.h:165
void convert_compound_enum(const typet &type, std::ostream &os)
Definition: dump_c.cpp:612
std::unordered_map< irep_idt, irep_idt > declared_enum_constants_mapt
Definition: dump_c_class.h:167
const dump_c_configurationt dump_c_config
Definition: dump_c_class.h:156
void cleanup_harness(code_blockt &b)
Replace CPROVER internal symbols in b by printable values and generate necessary declarations.
Definition: dump_c.cpp:976
void cleanup_type(typet &type)
Definition: dump_c.cpp:1513
void cleanup_decl(code_frontend_declt &decl, std::list< irep_idt > &local_static, std::list< irep_idt > &local_type_decls)
Definition: dump_c.cpp:655
std::string type_to_string(const typet &type)
Definition: dump_c.cpp:1556
std::unordered_map< irep_idt, code_frontend_declt > local_static_declst
Definition: dump_c_class.h:235
static std::string indent(const unsigned n)
Definition: dump_c_class.h:191
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)
Definition: dump_c.cpp:1031
convertedt converted_global
Definition: dump_c_class.h:161
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:89
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
A collection of goto functions.
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
void update()
Update all indices.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:986
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:949
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void remove(const irep_idt &name)
Definition: irep.cpp:96
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
bool is_not_nil() const
Definition: irep.h:380
subt & get_sub()
Definition: irep.h:456
void swap(irept &irep)
Definition: irep.h:442
const irep_idt & id() const
Definition: irep.h:396
irept & add(const irep_idt &name)
Definition: irep.cpp:116
bool is_nil() const
Definition: irep.h:376
const std::string & get_string(const irep_idt &name) const
Definition: irep.h:409
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:123
The NIL expression.
Definition: std_expr.h:2874
Replace expression or type symbols by an expression or type, respectively.
const irep_idt & get_statement() const
Definition: std_code.h:1472
Fixed-width bit-vector with two's complement interpretation.
void set_comment(const irep_idt &comment)
const irep_idt & get_function() const
const irep_idt & get_file() const
Struct constructor from list of elements.
Definition: std_expr.h:1722
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
Structure type, corresponds to C style structs.
Definition: std_types.h:231
Base type for structs and unions.
Definition: std_types.h:62
const componentst & components() const
Definition: std_types.h:147
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:57
std::vector< componentt > componentst
Definition: std_types.h:140
Expression to hold a symbol (variable)
Definition: std_expr.h:80
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:104
const irep_idt & get_identifier() const
Definition: std_expr.h:109
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
The symbol table.
Definition: symbol_table.h:14
virtual iteratort begin() override
Definition: symbol_table.h:108
virtual iteratort end() override
Definition: symbol_table.h:112
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_extern
Definition: symbol.h:66
bool is_macro
Definition: symbol.h:61
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
bool is_static_lifetime
Definition: symbol.h:65
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
exprt value
Initial value of symbol.
Definition: symbol.h:34
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.
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,...
A tag-based type, i.e., typet with an identifier.
Definition: std_types.h:396
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:405
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
const source_locationt & source_location() const
Definition: type.h:74
Generic base class for unary expressions.
Definition: std_expr.h:281
const exprt & op() const
Definition: std_expr.h:293
Union constructor from single element.
Definition: std_expr.h:1611
irep_idt get_component_name() const
Definition: std_expr.h:1619
A union tag type, i.e., union_typet with an identifier.
Definition: c_types.h:177
The union type.
Definition: c_types.h:125
Fixed-width bit-vector with unsigned binary interpretation.
configt config
Definition: config.cpp:25
#define CPROVER_PREFIX
std::ostream & operator<<(std::ostream &out, dump_ct &src)
Definition: dump_c.cpp:44
static bool find_block_position_rec(const irep_idt &identifier, codet &root, code_blockt *&dest, exprt::operandst::iterator &before)
Definition: dump_c.cpp:1126
static bool module_local_declaration(const symbolt &symbol, const std::string module)
Definition: dump_c.cpp:1611
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)
Definition: dump_c.cpp:1597
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)
Definition: dump_c.cpp:1584
static expr2c_configurationt expr2c_configuration()
Definition: dump_c.cpp:1539
void dump_c_type_header(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, const std::string module, std::ostream &out)
Definition: dump_c.cpp:1619
Dump C from Goto Program.
Dump Goto-Program as C/C++ Source.
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:4011
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:4027
std::string type2cpp(const typet &type, const namespacet &ns)
Definition: expr2cpp.cpp:498
std::string expr2cpp(const exprt &expr, const namespacet &ns)
Definition: expr2cpp.cpp:491
#define Forall_operands(it, expr)
Definition: expr.h:25
#define Forall_expr(it, expr)
Definition: expr.h:34
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
void find_non_pointer_type_symbols(const exprt &src, find_symbols_sett &dest)
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
Add to the set dest the sub-expressions of src with id ID_symbol or ID_next_symbol.
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:23
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
const code_function_callt & to_code_function_call(const codet &code)
Dump Goto-Program as C/C++ Source.
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
nonstd::optional< T > optionalt
Definition: optional.h:35
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define POSTCONDITION(CONDITION)
Definition: invariant.h:479
#define INITIALIZE_FUNCTION
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1506
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:203
const codet & to_code(const exprt &expr)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1657
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:434
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
std::string strip_string(const std::string &s)
Remove all whitespace characters from either end of a string.
std::size_t long_long_int_width
Definition: config.h:114
Used for configuring the behaviour of dump_c.
Definition: dump_c_class.h:24
dump_c_configurationt disable_include_function_decls()
Definition: dump_c_class.h:59
bool include_global_decls
Include the global declarations in the dump.
Definition: dump_c_class.h:32
bool include_typedefs
Include the typedefs in the dump.
Definition: dump_c_class.h:35
bool include_global_vars
Include global variable definitions in the dump.
Definition: dump_c_class.h:38
static dump_c_configurationt default_configuration
The default used for dump-c and dump-cpp.
Definition: dump_c_class.h:54
bool include_function_decls
Include the function declarations in the dump.
Definition: dump_c_class.h:26
bool include_headers
Include headers type declarations are borrowed from.
Definition: dump_c_class.h:47
bool include_compounds
Include struct definitions in the dump.
Definition: dump_c_class.h:41
dump_c_configurationt disable_include_global_vars()
Definition: dump_c_class.h:83
static dump_c_configurationt type_header_configuration
The config used for dump-c-type-header.
Definition: dump_c_class.h:57
dump_c_configurationt disable_include_function_bodies()
Definition: dump_c_class.h:65
dump_c_configurationt enable_include_headers()
Definition: dump_c_class.h:101
bool include_function_bodies
Include the functions in the dump.
Definition: dump_c_class.h:29
bool follow_compounds
Define whether to follow compunds recursively.
Definition: dump_c_class.h:44
Used for configuring the behaviour of expr2c and type2c.
Definition: expr2c.h:21
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:221
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177