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 =
84  ns.lookup(to_union_tag_type(type).get_identifier());
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 
397  convert_compound(type.subtype(), type.subtype(), recursive, os);
398 
399  // sizeof may contain a type symbol that has to be declared first
400  if(type.id()==ID_array)
401  {
402  find_symbols_sett syms;
403  find_non_pointer_type_symbols(to_array_type(type).size(), syms);
404 
405  for(find_symbols_sett::const_iterator
406  it=syms.begin();
407  it!=syms.end();
408  ++it)
409  {
410  const symbolt &type_symbol = ns.lookup(*it);
411  irep_idt tag_kind =
412  type_symbol.type.id() == ID_c_enum
413  ? ID_c_enum_tag
414  : (type_symbol.type.id() == ID_union ? ID_union_tag
415  : ID_struct_tag);
416  tag_typet s_type(tag_kind, *it);
417  convert_compound(s_type, s_type, recursive, os);
418  }
419  }
420  }
421  else if(type.id()==ID_struct || type.id()==ID_union)
422  convert_compound(to_struct_union_type(type), unresolved, recursive, os);
423  else if(type.id()==ID_c_enum)
424  convert_compound_enum(type, os);
425 }
426 
428  const struct_union_typet &type,
429  const typet &unresolved,
430  bool recursive,
431  std::ostream &os)
432 {
433  const irep_idt &name=type.get(ID_tag);
434 
435  if(!converted_compound.insert(name).second || type.get_bool(ID_C_do_not_dump))
436  return;
437 
438  // make sure typedef names used in the declaration are available
439  collect_typedefs(type, true);
440 
441  const irept &bases = type.find(ID_bases);
442  std::stringstream base_decls;
443  for(const auto &parent : bases.get_sub())
444  {
445  UNREACHABLE;
446  (void)parent;
447 #if 0
448  assert(parent.id() == ID_base);
449  assert(parent.get(ID_type) == ID_struct_tag);
450 
451  const irep_idt &base_id=
452  parent.find(ID_type).get(ID_identifier);
453  const irep_idt &renamed_base_id=global_renaming[base_id];
454  const symbolt &parsymb=ns.lookup(renamed_base_id);
455 
456  convert_compound_rec(parsymb.type, os);
457 
458  base_decls << id2string(renamed_base_id) +
459  (parent_it+1==bases.get_sub().end()?"":", ");
460 #endif
461  }
462 
463 #if 0
464  // for the constructor
465  string constructor_args;
466  string constructor_body;
467 
468  std::string component_name = id2string(renaming[compo.get(ID_name)]);
469  assert(component_name != "");
470 
471  if(it != struct_type.components().begin()) constructor_args += ", ";
472 
473  if(compo.type().id() == ID_pointer)
474  constructor_args += type_to_string(compo.type()) + component_name;
475  else
476  constructor_args += "const " + type_to_string(compo.type()) + "& " + component_name;
477 
478  constructor_body += indent + indent + "this->"+component_name + " = " + component_name + ";\n";
479 #endif
480 
481  std::stringstream struct_body;
482 
483  for(const auto &comp : type.components())
484  {
485  const typet &comp_type = comp.type();
486 
487  if(comp_type.id()==ID_code ||
488  comp.get_bool(ID_from_base) ||
489  comp.get_is_padding())
490  continue;
491 
492  const typet *non_array_type = &comp_type;
493  while(non_array_type->id()==ID_array)
494  non_array_type = &(non_array_type->subtype());
495 
496  if(recursive)
497  {
498  if(non_array_type->id()!=ID_pointer)
499  convert_compound(comp.type(), comp.type(), recursive, os);
500  else
501  collect_typedefs(comp.type(), true);
502  }
503 
504  irep_idt comp_name=comp.get_name();
505 
506  struct_body << indent(1) << "// " << comp_name << '\n';
507  struct_body << indent(1);
508 
509  // component names such as "main" would collide with other objects in the
510  // namespace
511  std::string fake_unique_name="NO/SUCH/NS::"+id2string(comp_name);
512  std::string s=make_decl(fake_unique_name, comp.type());
513  POSTCONDITION(s.find("NO/SUCH/NS")==std::string::npos);
514 
515  if(comp_type.id()==ID_c_bit_field &&
516  to_c_bit_field_type(comp_type).get_width()==0)
517  {
518  comp_name.clear();
519  s=type_to_string(comp_type);
520  }
521 
522  if(s.find(CPROVER_PREFIX "bitvector") == std::string::npos)
523  {
524  struct_body << s;
525  }
526  else if(comp_type.id()==ID_signedbv)
527  {
528  const signedbv_typet &t=to_signedbv_type(comp_type);
530  struct_body << "long long int " << comp_name
531  << " : " << t.get_width();
532  else if(mode == ID_cpp)
533  struct_body << "__signedbv<" << t.get_width() << "> "
534  << comp_name;
535  else
536  struct_body << s;
537  }
538  else if(comp_type.id()==ID_unsignedbv)
539  {
540  const unsignedbv_typet &t=to_unsignedbv_type(comp_type);
542  struct_body << "unsigned long long " << comp_name
543  << " : " << t.get_width();
544  else if(mode == ID_cpp)
545  struct_body << "__unsignedbv<" << t.get_width() << "> "
546  << comp_name;
547  else
548  struct_body << s;
549  }
550  else
551  UNREACHABLE;
552 
553  struct_body << ";\n";
554  }
555 
556  typet unresolved_clean=unresolved;
557  irep_idt typedef_str;
558  for(auto td_entry : typedef_types)
559  {
560  if(
561  td_entry.first.get(ID_identifier) == unresolved.get(ID_identifier) &&
562  (td_entry.first.source_location() == unresolved.source_location()))
563  {
564  unresolved_clean.remove(ID_C_typedef);
565  typedef_str = td_entry.second;
566  std::pair<typedef_mapt::iterator, bool> td_map_entry =
567  typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
568  PRECONDITION(!td_map_entry.second);
569  if(!td_map_entry.first->second.early)
570  td_map_entry.first->second.type_decl_str.clear();
571  os << "typedef ";
572  break;
573  }
574  }
575 
576  os << type_to_string(unresolved_clean);
577  if(!base_decls.str().empty())
578  {
579  PRECONDITION(mode == ID_cpp);
580  os << ": " << base_decls.str();
581  }
582  os << '\n';
583  os << "{\n";
584  os << struct_body.str();
585 
586  /*
587  if(!struct_type.components().empty())
588  {
589  os << indent << name << "(){}\n";
590  os << indent << "explicit " << name
591  << "(" + constructor_args + ")\n";
592  os << indent << "{\n";
593  os << constructor_body;
594  os << indent << "}\n";
595  }
596  */
597 
598  os << "}";
599  if(type.get_bool(ID_C_transparent_union))
600  os << " __attribute__ ((__transparent_union__))";
601  if(type.get_bool(ID_C_packed))
602  os << " __attribute__ ((__packed__))";
603  if(!typedef_str.empty())
604  os << " " << typedef_str;
605  os << ";\n\n";
606 }
607 
609  const typet &type,
610  std::ostream &os)
611 {
612  PRECONDITION(type.id()==ID_c_enum);
613 
614  const irept &tag=type.find(ID_tag);
615  const irep_idt &name=tag.get(ID_C_base_name);
616 
617  if(tag.is_nil() ||
618  !converted_enum.insert(name).second)
619  return;
620 
621  c_enum_typet enum_type=to_c_enum_type(type);
622  c_enum_typet::memberst &members=
623  (c_enum_typet::memberst &)(enum_type.add(ID_body).get_sub());
624  for(c_enum_typet::memberst::iterator
625  it=members.begin();
626  it!=members.end();
627  ++it)
628  {
629  const irep_idt bn=it->get_base_name();
630 
631  if(declared_enum_constants.find(bn)!=
632  declared_enum_constants.end() ||
634  {
635  std::string new_bn=id2string(name)+"$$"+id2string(bn);
636  it->set_base_name(new_bn);
637  }
638 
640  std::make_pair(bn, it->get_base_name()));
641  }
642 
643  os << type_to_string(enum_type);
644 
645  if(enum_type.get_bool(ID_C_packed))
646  os << " __attribute__ ((__packed__))";
647 
648  os << ";\n\n";
649 }
650 
652  code_declt &decl,
653  std::list<irep_idt> &local_static,
654  std::list<irep_idt> &local_type_decls)
655 {
656  goto_programt tmp;
657  tmp.add(goto_programt::make_decl(decl.symbol()));
658 
659  if(optionalt<exprt> value = decl.initial_value())
660  {
661  decl.set_initial_value({});
662  tmp.add(goto_programt::make_assignment(decl.symbol(), std::move(*value)));
663  }
664 
666 
667  // goto_program2codet requires valid location numbers:
668  tmp.update();
669 
670  std::unordered_set<irep_idt> typedef_names;
671  for(const auto &td : typedef_map)
672  typedef_names.insert(td.first);
673 
674  code_blockt b;
675  goto_program2codet p2s(
676  irep_idt(),
677  tmp,
679  b,
680  local_static,
681  local_type_decls,
682  typedef_names,
684  p2s();
685 
686  POSTCONDITION(b.statements().size() == 1);
687  decl.swap(b.op0());
688 }
689 
695 void dump_ct::collect_typedefs(const typet &type, bool early)
696 {
697  std::unordered_set<irep_idt> deps;
698  collect_typedefs_rec(type, early, deps);
699 }
700 
709  const typet &type,
710  bool early,
711  std::unordered_set<irep_idt> &dependencies)
712 {
714  return;
715 
716  std::unordered_set<irep_idt> local_deps;
717 
718  if(type.id()==ID_code)
719  {
720  const code_typet &code_type=to_code_type(type);
721 
722  collect_typedefs_rec(code_type.return_type(), early, local_deps);
723  for(const auto &param : code_type.parameters())
724  collect_typedefs_rec(param.type(), early, local_deps);
725  }
726  else if(type.id()==ID_pointer || type.id()==ID_array)
727  {
728  collect_typedefs_rec(type.subtype(), early, local_deps);
729  }
730  else if(
731  type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
732  type.id() == ID_union_tag)
733  {
734  const symbolt &symbol = ns.lookup(to_tag_type(type));
735  collect_typedefs_rec(symbol.type, early, local_deps);
736  }
737 
738  const irep_idt &typedef_str=type.get(ID_C_typedef);
739 
740  if(!typedef_str.empty())
741  {
742  std::pair<typedef_mapt::iterator, bool> entry=
743  typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
744 
745  if(entry.second ||
746  (early && entry.first->second.type_decl_str.empty()))
747  {
748  if(typedef_str=="__gnuc_va_list" || typedef_str == "va_list")
749  {
750  system_headers.insert("stdarg.h");
751  early=false;
752  }
753  else
754  {
755  typet t=type;
756  t.remove(ID_C_typedef);
757 
758  std::ostringstream oss;
759  oss << "typedef " << make_decl(typedef_str, t) << ';';
760 
761  entry.first->second.type_decl_str=oss.str();
762  entry.first->second.dependencies=local_deps;
763  }
764  }
765 
766  if(early)
767  {
768  entry.first->second.early=true;
769 
770  for(const auto &d : local_deps)
771  {
772  auto td_entry=typedef_map.find(d);
773  PRECONDITION(td_entry!=typedef_map.end());
774  td_entry->second.early=true;
775  }
776  }
777 
778  dependencies.insert(typedef_str);
779  }
780 
781  dependencies.insert(local_deps.begin(), local_deps.end());
782 }
783 
786 {
787  // sort the symbols first to ensure deterministic replacement in
788  // typedef_types below as there could be redundant declarations
789  // typedef int x;
790  // typedef int y;
791  std::map<std::string, symbolt> symbols_sorted;
792  for(const auto &symbol_entry : copied_symbol_table.symbols)
793  symbols_sorted.insert(
794  {id2string(symbol_entry.first), symbol_entry.second});
795 
796  for(const auto &symbol_entry : symbols_sorted)
797  {
798  const symbolt &symbol=symbol_entry.second;
799 
800  if(symbol.is_macro && symbol.is_type &&
801  symbol.location.get_function().empty())
802  {
803  const irep_idt &typedef_str=symbol.type.get(ID_C_typedef);
804  PRECONDITION(!typedef_str.empty());
805  typedef_types[symbol.type]=typedef_str;
807  typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
808  else
809  collect_typedefs(symbol.type, false);
810  }
811  }
812 }
813 
816 void dump_ct::dump_typedefs(std::ostream &os) const
817 {
818  // we need to compute a topological sort; we do so by picking all
819  // typedefs the dependencies of which have been emitted into to_insert
820  std::vector<typedef_infot> typedefs_sorted;
821  typedefs_sorted.reserve(typedef_map.size());
822 
823  // elements in to_insert are lexicographically sorted and ready for
824  // output
825  std::map<std::string, typedef_infot> to_insert;
826 
827  std::unordered_set<irep_idt> typedefs_done;
828  std::unordered_map<irep_idt, std::unordered_set<irep_idt>> forward_deps,
829  reverse_deps;
830 
831  for(const auto &td : typedef_map)
832  if(!td.second.type_decl_str.empty())
833  {
834  if(td.second.dependencies.empty())
835  // those can be dumped immediately
836  to_insert.insert({id2string(td.first), td.second});
837  else
838  {
839  // delay them until dependencies are dumped
840  forward_deps.insert({td.first, td.second.dependencies});
841  for(const auto &d : td.second.dependencies)
842  reverse_deps[d].insert(td.first);
843  }
844  }
845 
846  while(!to_insert.empty())
847  {
848  // the topologically next element (lexicographically ranked first
849  // among all the dependencies of which have been dumped)
850  typedef_infot t=to_insert.begin()->second;
851  to_insert.erase(to_insert.begin());
852  // move to the output queue
853  typedefs_sorted.push_back(t);
854 
855  // find any depending typedefs that are now valid, or at least
856  // reduce the remaining dependencies
857  auto r_it=reverse_deps.find(t.typedef_name);
858  if(r_it==reverse_deps.end())
859  continue;
860 
861  // reduce remaining dependencies
862  std::unordered_set<irep_idt> &r_deps = r_it->second;
863  for(std::unordered_set<irep_idt>::iterator it = r_deps.begin();
864  it != r_deps.end();) // no ++it
865  {
866  auto f_it=forward_deps.find(*it);
867  if(f_it==forward_deps.end()) // might be done already
868  {
869  it=r_deps.erase(it);
870  continue;
871  }
872 
873  // update dependencies
874  std::unordered_set<irep_idt> &f_deps = f_it->second;
875  PRECONDITION(!f_deps.empty());
876  PRECONDITION(f_deps.find(t.typedef_name)!=f_deps.end());
877  f_deps.erase(t.typedef_name);
878 
879  if(f_deps.empty()) // all depenencies done now!
880  {
881  const auto td_entry=typedef_map.find(*it);
882  PRECONDITION(td_entry!=typedef_map.end());
883  to_insert.insert({id2string(*it), td_entry->second});
884  forward_deps.erase(*it);
885  it=r_deps.erase(it);
886  }
887  else
888  ++it;
889  }
890  }
891 
892  POSTCONDITION(forward_deps.empty());
893 
894  for(const auto &td : typedefs_sorted)
895  os << td.type_decl_str << '\n';
896 
897  if(!typedefs_sorted.empty())
898  os << '\n';
899 }
900 
902  const symbolt &symbol,
903  std::ostream &os,
904  local_static_declst &local_static_decls)
905 {
906  const irep_idt &func=symbol.location.get_function();
907  if((func.empty() || symbol.is_extern || symbol.value.is_not_nil()) &&
908  !converted_global.insert(symbol.name).second)
909  return;
910 
911  code_declt d(symbol.symbol_expr());
912 
913  find_symbols_sett syms;
914  if(symbol.value.is_not_nil())
915  find_symbols_or_nexts(symbol.value, syms);
916 
917  // add a tentative declaration to cater for symbols in the initializer
918  // relying on it this symbol
919  if((func.empty() || symbol.is_extern) &&
920  (symbol.value.is_nil() || !syms.empty()))
921  {
922  os << "// " << symbol.name << '\n';
923  os << "// " << symbol.location << '\n';
924  os << expr_to_string(d) << '\n';
925  }
926 
927  if(!symbol.value.is_nil())
928  {
929  std::set<std::string> symbols_sorted;
930  for(find_symbols_sett::const_iterator
931  it=syms.begin();
932  it!=syms.end();
933  ++it)
934  {
935  bool inserted=symbols_sorted.insert(id2string(*it)).second;
936  CHECK_RETURN(inserted);
937  }
938 
939  for(std::set<std::string>::const_iterator
940  it=symbols_sorted.begin();
941  it!=symbols_sorted.end();
942  ++it)
943  {
944  const symbolt &sym=ns.lookup(*it);
945  if(!sym.is_type && sym.is_static_lifetime && sym.type.id()!=ID_code)
946  convert_global_variable(sym, os, local_static_decls);
947  }
948 
949  d.copy_to_operands(symbol.value);
950  }
951 
952  if(!func.empty() && !symbol.is_extern)
953  {
954  local_static_decls.emplace(symbol.name, d);
955  }
956  else if(!symbol.value.is_nil())
957  {
958  os << "// " << symbol.name << '\n';
959  os << "// " << symbol.location << '\n';
960 
961  std::list<irep_idt> empty_static, empty_types;
962  cleanup_decl(d, empty_static, empty_types);
963  CHECK_RETURN(empty_static.empty());
964  os << expr_to_string(d) << '\n';
965  }
966 }
967 
972 {
974  code_blockt decls;
975 
976  const symbolt *argc_sym=nullptr;
977  if(!ns.lookup("argc'", argc_sym))
978  {
979  symbol_exprt argc("argc", argc_sym->type);
980  replace.insert(argc_sym->symbol_expr(), argc);
981  code_declt d(argc);
982  decls.add(d);
983  }
984  const symbolt *argv_sym=nullptr;
985  if(!ns.lookup("argv'", argv_sym))
986  {
987  symbol_exprt argv("argv", argv_sym->type);
988  // replace argc' by argc in the type of argv['] to maintain type consistency
989  // while replacing
990  replace(argv);
991  replace.insert(symbol_exprt(argv_sym->name, argv.type()), argv);
992  code_declt d(argv);
993  decls.add(d);
994  }
995  const symbolt *return_sym=nullptr;
996  if(!ns.lookup("return'", return_sym))
997  {
998  symbol_exprt return_value("return_value", return_sym->type);
999  replace.insert(return_sym->symbol_expr(), return_value);
1000  code_declt d(return_value);
1001  decls.add(d);
1002  }
1003 
1004  for(auto &code : b.statements())
1005  {
1006  if(code.get_statement()==ID_function_call)
1007  {
1008  exprt &func=to_code_function_call(code).function();
1009  if(func.id()==ID_symbol)
1010  {
1011  symbol_exprt &s=to_symbol_expr(func);
1012  if(s.get_identifier()==ID_main)
1014  else if(s.get_identifier() == INITIALIZE_FUNCTION)
1015  continue;
1016  }
1017  }
1018 
1019  decls.add(code);
1020  }
1021 
1022  b.swap(decls);
1023  replace(b);
1024 }
1025 
1027  const symbolt &symbol,
1028  const bool skip_main,
1029  std::ostream &os_decl,
1030  std::ostream &os_body,
1031  local_static_declst &local_static_decls)
1032 {
1033  // don't dump artificial main
1034  if(skip_main && symbol.name==goto_functionst::entry_point())
1035  return;
1036 
1037  // convert the goto program back to code - this might change
1038  // the function type
1039  goto_functionst::function_mapt::const_iterator func_entry=
1040  goto_functions.function_map.find(symbol.name);
1041  if(func_entry!=goto_functions.function_map.end() &&
1042  func_entry->second.body_available())
1043  {
1044  code_blockt b;
1045  std::list<irep_idt> type_decls, local_static;
1046 
1047  std::unordered_set<irep_idt> typedef_names;
1048  for(const auto &td : typedef_map)
1049  typedef_names.insert(td.first);
1050 
1051  goto_program2codet p2s(
1052  symbol.name,
1053  func_entry->second.body,
1055  b,
1056  local_static,
1057  type_decls,
1058  typedef_names,
1059  system_headers);
1060  p2s();
1061 
1063  b,
1064  local_static,
1065  local_static_decls,
1066  type_decls);
1067 
1068  convertedt converted_c_bak(converted_compound);
1069  convertedt converted_e_bak(converted_enum);
1070 
1072  enum_constants_bak(declared_enum_constants);
1073 
1075  b,
1076  type_decls);
1077 
1078  converted_enum.swap(converted_e_bak);
1079  converted_compound.swap(converted_c_bak);
1080 
1081  if(harness && symbol.name==goto_functions.entry_point())
1082  cleanup_harness(b);
1083 
1084  os_body << "// " << symbol.name << '\n';
1085  os_body << "// " << symbol.location << '\n';
1086  if(symbol.name==goto_functions.entry_point())
1087  os_body << make_decl(ID_main, symbol.type) << '\n';
1088  else if(!harness || symbol.name!=ID_main)
1089  os_body << make_decl(symbol.name, symbol.type) << '\n';
1090  else if(harness && symbol.name==ID_main)
1091  {
1092  os_body << make_decl(CPROVER_PREFIX+id2string(symbol.name), symbol.type)
1093  << '\n';
1094  }
1095  os_body << expr_to_string(b);
1096  os_body << "\n\n";
1097 
1098  declared_enum_constants.swap(enum_constants_bak);
1099  }
1100 
1101  if(symbol.name!=goto_functionst::entry_point() &&
1102  symbol.name!=ID_main)
1103  {
1104  os_decl << "// " << symbol.name << '\n';
1105  os_decl << "// " << symbol.location << '\n';
1106  os_decl << make_decl(symbol.name, symbol.type) << ";\n";
1107  }
1108  else if(harness && symbol.name==ID_main)
1109  {
1110  os_decl << "// " << symbol.name << '\n';
1111  os_decl << "// " << symbol.location << '\n';
1112  os_decl << make_decl(CPROVER_PREFIX+id2string(symbol.name), symbol.type)
1113  << ";\n";
1114  }
1115 
1116  // make sure typedef names used in the function declaration are
1117  // available
1118  collect_typedefs(symbol.type, true);
1119 }
1120 
1122  const irep_idt &identifier,
1123  codet &root,
1124  code_blockt* &dest,
1125  exprt::operandst::iterator &before)
1126 {
1127  if(!root.has_operands())
1128  return false;
1129 
1130  code_blockt *our_dest=nullptr;
1131 
1132  exprt::operandst &operands=root.operands();
1133  exprt::operandst::iterator first_found=operands.end();
1134 
1135  Forall_expr(it, operands)
1136  {
1137  bool found=false;
1138 
1139  // be aware of the skip-carries-type hack
1140  if(it->id()==ID_code &&
1141  to_code(*it).get_statement()!=ID_skip)
1143  identifier,
1144  to_code(*it),
1145  our_dest,
1146  before);
1147  else
1148  {
1149  find_symbols_sett syms;
1150  find_type_and_expr_symbols(*it, syms);
1151 
1152  found=syms.find(identifier)!=syms.end();
1153  }
1154 
1155  if(!found)
1156  continue;
1157 
1158  if(!our_dest)
1159  {
1160  // first containing block
1161  if(root.get_statement()==ID_block)
1162  {
1163  dest=&(to_code_block(root));
1164  before=it;
1165  }
1166 
1167  return true;
1168  }
1169  else
1170  {
1171  // there is a containing block and this is the first operand
1172  // that contains identifier
1173  if(first_found==operands.end())
1174  first_found=it;
1175  // we have seen it already - pick the first occurrence in this
1176  // block
1177  else if(root.get_statement()==ID_block)
1178  {
1179  dest=&(to_code_block(root));
1180  before=first_found;
1181 
1182  return true;
1183  }
1184  // we have seen it already - outer block has to deal with this
1185  else
1186  return true;
1187  }
1188  }
1189 
1190  if(first_found!=operands.end())
1191  {
1192  dest=our_dest;
1193 
1194  return true;
1195  }
1196 
1197  return false;
1198 }
1199 
1201  code_blockt &b,
1202  const std::list<irep_idt> &local_static,
1203  local_static_declst &local_static_decls,
1204  std::list<irep_idt> &type_decls)
1205 {
1206  // look up last identifier first as its value may introduce the
1207  // other ones
1208  for(std::list<irep_idt>::const_reverse_iterator
1209  it=local_static.rbegin();
1210  it!=local_static.rend();
1211  ++it)
1212  {
1213  local_static_declst::const_iterator d_it=
1214  local_static_decls.find(*it);
1215  PRECONDITION(d_it!=local_static_decls.end());
1216 
1217  code_declt d=d_it->second;
1218  std::list<irep_idt> redundant;
1219  cleanup_decl(d, redundant, type_decls);
1220 
1221  code_blockt *dest_ptr=nullptr;
1222  exprt::operandst::iterator before=b.operands().end();
1223 
1224  // some use of static variables might be optimised out if it is
1225  // within an if(false) { ... } block
1226  if(find_block_position_rec(*it, b, dest_ptr, before))
1227  {
1228  CHECK_RETURN(dest_ptr!=nullptr);
1229  dest_ptr->operands().insert(before, d);
1230  }
1231  }
1232 }
1233 
1235  code_blockt &b,
1236  const std::list<irep_idt> &type_decls)
1237 {
1238  // look up last identifier first as its value may introduce the
1239  // other ones
1240  for(std::list<irep_idt>::const_reverse_iterator
1241  it=type_decls.rbegin();
1242  it!=type_decls.rend();
1243  ++it)
1244  {
1245  const typet &type=ns.lookup(*it).type;
1246  // feed through plain C to expr2c by ending and re-starting
1247  // a comment block ...
1248  std::ostringstream os_body;
1249  os_body << *it << " */\n";
1250  irep_idt tag_kind =
1251  type.id() == ID_c_enum
1252  ? ID_c_enum_tag
1253  : (type.id() == ID_union ? ID_union_tag : ID_struct_tag);
1254  convert_compound(type, tag_typet(tag_kind, *it), false, os_body);
1255  os_body << "/*";
1256 
1257  code_skipt skip;
1258  skip.add_source_location().set_comment(os_body.str());
1259  // another hack to ensure symbols inside types are seen
1260  skip.type()=type;
1261 
1262  code_blockt *dest_ptr=nullptr;
1263  exprt::operandst::iterator before=b.operands().end();
1264 
1265  // we might not find it in case a transparent union type cast
1266  // has been removed by cleanup operations
1267  if(find_block_position_rec(*it, b, dest_ptr, before))
1268  {
1269  CHECK_RETURN(dest_ptr!=nullptr);
1270  dest_ptr->operands().insert(before, skip);
1271  }
1272  }
1273 }
1274 
1276 {
1277  Forall_operands(it, expr)
1278  cleanup_expr(*it);
1279 
1280  cleanup_type(expr.type());
1281 
1282  if(expr.id()==ID_struct)
1283  {
1284  struct_typet type=
1285  to_struct_type(ns.follow(expr.type()));
1286 
1287  struct_union_typet::componentst old_components;
1288  old_components.swap(type.components());
1289 
1290  exprt::operandst old_ops;
1291  old_ops.swap(expr.operands());
1292 
1293  PRECONDITION(old_components.size()==old_ops.size());
1294  exprt::operandst::iterator o_it=old_ops.begin();
1295  for(const auto &old_comp : old_components)
1296  {
1297  const bool is_zero_bit_field =
1298  old_comp.type().id() == ID_c_bit_field &&
1299  to_c_bit_field_type(old_comp.type()).get_width() == 0;
1300 
1301  if(!old_comp.get_is_padding() && !is_zero_bit_field)
1302  {
1303  type.components().push_back(old_comp);
1304  expr.add_to_operands(std::move(*o_it));
1305  }
1306  ++o_it;
1307  }
1308  expr.type().swap(type);
1309  }
1310  else if(expr.id()==ID_union)
1311  {
1312  union_exprt &u=to_union_expr(expr);
1313  const union_typet &u_type_f=to_union_type(ns.follow(u.type()));
1314 
1315  if(!u.type().get_bool(ID_C_transparent_union) &&
1316  !u_type_f.get_bool(ID_C_transparent_union))
1317  {
1318  if(u_type_f.get_component(u.get_component_name()).get_is_padding())
1319  // we just use an empty struct to fake an empty union
1320  expr = struct_exprt({}, struct_typet());
1321  }
1322  // add a typecast for NULL
1323  else if(u.op().id()==ID_constant &&
1324  u.op().type().id()==ID_pointer &&
1325  u.op().type().subtype().id()==ID_empty &&
1326  (u.op().is_zero() ||
1327  to_constant_expr(u.op()).get_value()==ID_NULL))
1328  {
1329  const struct_union_typet::componentt &comp=
1330  u_type_f.get_component(u.get_component_name());
1331  const typet &u_op_type=comp.type();
1332  PRECONDITION(u_op_type.id()==ID_pointer);
1333 
1334  typecast_exprt tc(u.op(), u_op_type);
1335  expr.swap(tc);
1336  }
1337  else
1338  {
1339  exprt tmp;
1340  tmp.swap(u.op());
1341  expr.swap(tmp);
1342  }
1343  }
1344  else if(
1345  expr.id() == ID_typecast &&
1346  to_typecast_expr(expr).op().id() == ID_typecast &&
1347  expr.type() == to_typecast_expr(expr).op().type())
1348  {
1349  exprt tmp = to_typecast_expr(expr).op();
1350  expr.swap(tmp);
1351  }
1352  else if(expr.id()==ID_code &&
1353  to_code(expr).get_statement()==ID_function_call &&
1354  to_code_function_call(to_code(expr)).function().id()==ID_symbol)
1355  {
1357  const symbol_exprt &fn=to_symbol_expr(call.function());
1358  code_function_callt::argumentst &arguments=call.arguments();
1359 
1360  // don't edit function calls we might have introduced
1361  const symbolt *s;
1362  if(!ns.lookup(fn.get_identifier(), s))
1363  {
1364  const symbolt &fn_sym=ns.lookup(fn.get_identifier());
1365  const code_typet &code_type=to_code_type(fn_sym.type);
1366  const code_typet::parameterst &parameters=code_type.parameters();
1367 
1368  if(parameters.size()==arguments.size())
1369  {
1370  code_typet::parameterst::const_iterator it=parameters.begin();
1371  for(auto &argument : arguments)
1372  {
1373  const typet &type=ns.follow(it->type());
1374  if(type.id()==ID_union &&
1375  type.get_bool(ID_C_transparent_union))
1376  {
1377  if(argument.id() == ID_typecast && argument.type() == type)
1378  argument = to_typecast_expr(argument).op();
1379 
1380  // add a typecast for NULL or 0
1381  if(
1382  argument.id() == ID_constant &&
1383  (argument.is_zero() ||
1384  to_constant_expr(argument).get_value() == ID_NULL))
1385  {
1386  const typet &comp_type=
1387  to_union_type(type).components().front().type();
1388 
1389  if(comp_type.id()==ID_pointer)
1390  argument = typecast_exprt(argument, comp_type);
1391  }
1392  }
1393 
1394  ++it;
1395  }
1396  }
1397  }
1398  }
1399  else if(expr.id()==ID_constant &&
1400  expr.type().id()==ID_signedbv)
1401  {
1402  #if 0
1403  const irep_idt &cformat=expr.get(ID_C_cformat);
1404 
1405  if(!cformat.empty())
1406  {
1407  declared_enum_constants_mapt::const_iterator entry=
1408  declared_enum_constants.find(cformat);
1409 
1410  if(entry!=declared_enum_constants.end() &&
1411  entry->first!=entry->second)
1412  expr.set(ID_C_cformat, entry->second);
1413  else if(entry==declared_enum_constants.end() &&
1414  !std::isdigit(id2string(cformat)[0]))
1415  expr.remove(ID_C_cformat);
1416  }
1417  #endif
1418  }
1419  else if(
1420  expr.id() == ID_byte_update_little_endian ||
1421  expr.id() == ID_byte_update_big_endian)
1422  {
1423  const byte_update_exprt &bu = to_byte_update_expr(expr);
1424 
1425  if(bu.op().id() == ID_union && bu.offset().is_zero())
1426  {
1427  const union_exprt &union_expr = to_union_expr(bu.op());
1428  const union_typet &union_type =
1429  to_union_type(ns.follow(union_expr.type()));
1430 
1431  for(const auto &comp : union_type.components())
1432  {
1433  if(bu.value().type() == comp.type())
1434  {
1435  exprt member1{ID_member};
1436  member1.set(ID_component_name, union_expr.get_component_name());
1437  exprt designated_initializer1{ID_designated_initializer};
1438  designated_initializer1.add_to_operands(union_expr.op());
1439  designated_initializer1.add(ID_designator).move_to_sub(member1);
1440 
1441  exprt member2{ID_member};
1442  member2.set(ID_component_name, comp.get_name());
1443  exprt designated_initializer2{ID_designated_initializer};
1444  designated_initializer2.add_to_operands(bu.value());
1445  designated_initializer2.add(ID_designator).move_to_sub(member2);
1446 
1447  binary_exprt initializer_list{std::move(designated_initializer1),
1448  ID_initializer_list,
1449  std::move(designated_initializer2)};
1450  expr.swap(initializer_list);
1451 
1452  return;
1453  }
1454  }
1455  }
1456  else if(
1457  bu.op().id() == ID_side_effect &&
1458  to_side_effect_expr(bu.op()).get_statement() == ID_nondet &&
1459  ns.follow(bu.op().type()).id() == ID_union && bu.offset().is_zero())
1460  {
1461  const union_typet &union_type = to_union_type(ns.follow(bu.op().type()));
1462 
1463  for(const auto &comp : union_type.components())
1464  {
1465  if(bu.value().type() == comp.type())
1466  {
1467  union_exprt union_expr{comp.get_name(), bu.value(), bu.op().type()};
1468  expr.swap(union_expr);
1469 
1470  return;
1471  }
1472  }
1473  }
1474 
1475  optionalt<exprt> clean_init;
1476  if(
1477  ns.follow(bu.type()).id() == ID_union &&
1479  {
1480  clean_init = zero_initializer(bu.op().type(), source_locationt{}, ns)
1481  .value_or(nil_exprt{});
1482  if(clean_init->id() != ID_struct || clean_init->has_operands())
1483  cleanup_expr(*clean_init);
1484  }
1485 
1486  if(clean_init.has_value() && bu.op() == *clean_init)
1487  {
1488  const union_typet &union_type = to_union_type(ns.follow(bu.type()));
1489 
1490  for(const auto &comp : union_type.components())
1491  {
1492  if(bu.value().type() == comp.type())
1493  {
1494  union_exprt union_expr{comp.get_name(), bu.value(), bu.type()};
1495  expr.swap(union_expr);
1496 
1497  return;
1498  }
1499  }
1500 
1501  // we still haven't found a suitable component, so just ignore types and
1502  // build an initializer list without designators
1503  expr = unary_exprt{ID_initializer_list, bu.value()};
1504  }
1505  }
1506 }
1507 
1509 {
1510  for(typet &subtype : to_type_with_subtypes(type).subtypes())
1511  cleanup_type(subtype);
1512 
1513  if(type.id()==ID_code)
1514  {
1515  code_typet &code_type=to_code_type(type);
1516 
1517  cleanup_type(code_type.return_type());
1518 
1519  for(code_typet::parameterst::iterator
1520  it=code_type.parameters().begin();
1521  it!=code_type.parameters().end();
1522  ++it)
1523  cleanup_type(it->type());
1524  }
1525 
1526  if(type.id()==ID_array)
1527  cleanup_expr(to_array_type(type).size());
1528 
1529  POSTCONDITION(
1530  (type.id()!=ID_union && type.id()!=ID_struct) ||
1531  !type.get(ID_tag).empty());
1532 }
1533 
1535 {
1536  // future TODO: with C++20 we can actually use designated initializers as
1537  // commented out below
1538  static expr2c_configurationt configuration{
1539  /* .include_struct_padding_components = */ true,
1540  /* .print_struct_body_in_type = */ true,
1541  /* .include_array_size = */ true,
1542  /* .true_string = */ "1",
1543  /* .false_string = */ "0",
1544  /* .use_library_macros = */ true,
1545  /* .print_enum_int_value = */ false,
1546  /* .expand_typedef = */ false};
1547 
1548  return configuration;
1549 }
1550 
1551 std::string dump_ct::type_to_string(const typet &type)
1552 {
1553  std::string ret;
1554  typet t=type;
1555  cleanup_type(t);
1556 
1557  if(mode == ID_C)
1558  return type2c(t, ns, expr2c_configuration());
1559  else if(mode == ID_cpp)
1560  return type2cpp(t, ns);
1561  else
1562  UNREACHABLE;
1563 }
1564 
1565 std::string dump_ct::expr_to_string(const exprt &expr)
1566 {
1567  std::string ret;
1568  exprt e=expr;
1569  cleanup_expr(e);
1570 
1571  if(mode == ID_C)
1572  return expr2c(e, ns, expr2c_configuration());
1573  else if(mode == ID_cpp)
1574  return expr2cpp(e, ns);
1575  else
1576  UNREACHABLE;
1577 }
1578 
1579 void dump_c(
1580  const goto_functionst &src,
1581  const bool use_system_headers,
1582  const bool use_all_headers,
1583  const bool include_harness,
1584  const namespacet &ns,
1585  std::ostream &out)
1586 {
1587  dump_ct goto2c(
1588  src, use_system_headers, use_all_headers, include_harness, ns, ID_C);
1589  out << goto2c;
1590 }
1591 
1593  const goto_functionst &src,
1594  const bool use_system_headers,
1595  const bool use_all_headers,
1596  const bool include_harness,
1597  const namespacet &ns,
1598  std::ostream &out)
1599 {
1600  dump_ct goto2cpp(
1601  src, use_system_headers, use_all_headers, include_harness, ns, ID_cpp);
1602  out << goto2cpp;
1603 }
1604 
1605 static bool
1606 module_local_declaration(const symbolt &symbol, const std::string module)
1607 {
1608  std::string base_name =
1609  get_base_name(id2string(symbol.location.get_file()), true);
1610  std::string symbol_module = strip_string(id2string(symbol.module));
1611  return (base_name == module && symbol_module == module);
1612 }
1613 
1615  const goto_functionst &src,
1616  const bool use_system_headers,
1617  const bool use_all_headers,
1618  const bool include_harness,
1619  const namespacet &ns,
1620  const std::string module,
1621  std::ostream &out)
1622 {
1623  symbol_tablet symbol_table = ns.get_symbol_table();
1624  for(symbol_tablet::iteratort it = symbol_table.begin();
1625  it != symbol_table.end();
1626  it++)
1627  {
1628  symbolt &new_symbol = it.get_writeable_symbol();
1629  if(module_local_declaration(new_symbol, module))
1630  {
1631  new_symbol.type.set(ID_C_do_not_dump, 0);
1632  }
1633  else
1634  {
1635  new_symbol.type.set(ID_C_do_not_dump, 1);
1636  }
1637  }
1638 
1639  namespacet new_ns(symbol_table);
1640  dump_ct goto2c(
1641  src,
1642  use_system_headers,
1643  use_all_headers,
1644  include_harness,
1645  new_ns,
1646  ID_C,
1648  out << goto2c;
1649 }
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:58
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:277
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
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:47
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
A base class for binary expressions.
Definition: std_expr.h:550
std::size_t get_width() const
Definition: std_types.h:843
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:292
The type of C enums.
Definition: c_types.h:204
std::vector< c_enum_membert > memberst
Definition: c_types.h:240
A codet representing sequential composition of program statements.
Definition: std_code.h:168
void add(const codet &code)
Definition: std_code.h:206
code_operandst & statements()
Definition: std_code.h:176
A codet representing the declaration of a local variable.
Definition: std_code.h:400
void set_initial_value(optionalt< exprt > initial_value)
Sets the value to which this declaration initializes the declared variable.
Definition: std_code.h:436
symbol_exprt & symbol()
Definition: std_code.h:406
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:425
codet representation of a function call statement.
Definition: std_code.h:1213
exprt & function()
Definition: std_code.h:1248
argumentst & arguments()
Definition: std_code.h:1258
exprt::operandst argumentst
Definition: std_code.h:1222
A codet representing a skip statement.
Definition: std_code.h:268
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.h:33
exprt & op0()
Definition: expr.h:99
const irep_idt & get_statement() const
Definition: std_code.h:69
optionalt< std::string > main
Definition: config.h:260
struct configt::ansi_ct ansi_c
const irep_idt & get_value() const
Definition: std_expr.h:2761
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:1234
void cleanup_expr(exprt &expr)
Definition: dump_c.cpp:1275
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:1200
std::string expr_to_string(const exprt &expr)
Definition: dump_c.cpp:1565
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:695
void gather_global_typedefs()
Find all global typdefs in the symbol table and store them in typedef_types.
Definition: dump_c.cpp:785
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 cleanup_decl(code_declt &decl, std::list< irep_idt > &local_static, std::list< irep_idt > &local_type_decls)
Definition: dump_c.cpp:651
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:708
std::unordered_map< irep_idt, code_declt > local_static_declst
Definition: dump_c_class.h:235
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:901
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:816
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:608
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:971
void cleanup_type(typet &type)
Definition: dump_c.cpp:1508
std::string type_to_string(const typet &type)
Definition: dump_c.cpp:1551
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:1026
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:71
void update()
Update all indices.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:753
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:978
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
subt & get_sub()
Definition: irep.h:467
irept & add(const irep_namet &name)
Definition: irep.cpp:116
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:420
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:58
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:453
void remove(const irep_namet &name)
Definition: irep.cpp:96
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
bool is_nil() const
Definition: irep.h:387
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:2820
Replace expression or type symbols by an expression or type, respectively.
const irep_idt & get_statement() const
Definition: std_code.h:1918
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:1668
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:49
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:1866
The type of an expression, extends irept.
Definition: type.h:28
const source_locationt & source_location() const
Definition: type.h:71
const typet & subtype() const
Definition: type.h:47
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:1602
irep_idt get_component_name() const
Definition: std_expr.h:1610
A union tag type, i.e., union_typet with an identifier.
Definition: c_types.h:164
The union type.
Definition: c_types.h:112
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:1121
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:1606
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:1592
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:1579
static expr2c_configurationt expr2c_configuration()
Definition: dump_c.cpp:1534
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:1614
Dump C from Goto Program.
Dump Goto-Program as C/C++ Source.
std::string type2c(const typet &type, const namespacet &ns)
std::string expr2c(const exprt &expr, const namespacet &ns)
std::string type2cpp(const typet &type, const namespacet &ns)
Definition: expr2cpp.cpp:497
std::string expr2cpp(const exprt &expr, const namespacet &ns)
Definition: expr2cpp.cpp:490
#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
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:49
nonstd::optional< T > optionalt
Definition: optional.h:35
#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:1952
const codet & to_code(const exprt &expr)
Definition: std_code.h:153
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:254
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1324
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786
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:1900
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1648
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:813
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:115
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:198