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