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