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