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 <sstream>
15 #include <cctype>
16 
17 #include <util/config.h>
18 #include <util/invariant.h>
19 #include <util/prefix.h>
20 #include <util/suffix.h>
21 #include <util/find_symbols.h>
22 #include <util/base_type.h>
23 #include <util/cprover_prefix.h>
24 
25 #include <ansi-c/ansi_c_language.h>
26 #include <cpp/cpp_language.h>
27 
28 #include "goto_program2code.h"
29 #include "dump_c_class.h"
30 
31 inline std::ostream &operator << (std::ostream &out, dump_ct &src)
32 {
33  src(out);
34  return out;
35 }
36 
37 void dump_ct::operator()(std::ostream &os)
38 {
39  std::stringstream func_decl_stream;
40  std::stringstream compound_body_stream;
41  std::stringstream global_var_stream;
42  std::stringstream global_decl_stream;
43  std::stringstream func_body_stream;
44  local_static_declst local_static_decls;
45 
46  // add copies of struct types when ID_C_transparent_union is only
47  // annotated to parameter
48  symbol_tablet symbols_transparent;
50  {
51  symbolt &symbol=it->second;
52 
53  if(symbol.type.id()!=ID_code)
54  continue;
55 
56  code_typet &code_type=to_code_type(symbol.type);
57  code_typet::parameterst &parameters=code_type.parameters();
58 
59  for(code_typet::parameterst::iterator
60  it2=parameters.begin();
61  it2!=parameters.end();
62  ++it2)
63  {
64  typet &type=it2->type();
65 
66  if(type.id()==ID_symbol &&
67  type.get_bool(ID_C_transparent_union))
68  {
69  symbolt new_type_sym=
70  ns.lookup(to_symbol_type(type).get_identifier());
71 
72  new_type_sym.name=id2string(new_type_sym.name)+"$transparent";
73  new_type_sym.type.set(ID_C_transparent_union, true);
74 
75  // we might have it already, in which case this has no effect
76  symbols_transparent.add(new_type_sym);
77 
78  to_symbol_type(type).set_identifier(new_type_sym.name);
79  type.remove(ID_C_transparent_union);
80  }
81  }
82  }
83  forall_symbols(it, symbols_transparent.symbols)
84  copied_symbol_table.add(it->second);
85 
86  typedef std::unordered_map<irep_idt, unsigned, irep_id_hash> unique_tagst;
87  unique_tagst unique_tags;
88 
89  // add tags to anonymous union/struct/enum,
90  // and prepare lexicographic order
91  std::set<std::string> symbols_sorted;
93  {
94  symbolt &symbol=it->second;
95  bool tag_added=false;
96 
97  // TODO we could get rid of some of the ID_anonymous by looking up
98  // the origin symbol types in typedef_types and adjusting any other
99  // uses of ID_tag
100  if((symbol.type.id()==ID_union || symbol.type.id()==ID_struct) &&
101  symbol.type.get(ID_tag).empty())
102  {
103  PRECONDITION(symbol.is_type);
104  symbol.type.set(ID_tag, ID_anonymous);
105  tag_added=true;
106  }
107  else if(symbol.type.id()==ID_c_enum &&
108  symbol.type.find(ID_tag).get(ID_C_base_name).empty())
109  {
110  PRECONDITION(symbol.is_type);
111  symbol.type.add(ID_tag).set(ID_C_base_name, ID_anonymous);
112  tag_added=true;
113  }
114 
115  const std::string name_str=id2string(it->first);
116  if(symbol.is_type &&
117  (symbol.type.id()==ID_union ||
118  symbol.type.id()==ID_struct ||
119  symbol.type.id()==ID_c_enum))
120  {
121  std::string new_tag=symbol.type.id()==ID_c_enum?
122  symbol.type.find(ID_tag).get_string(ID_C_base_name):
123  symbol.type.get_string(ID_tag);
124 
125  std::string::size_type tag_pos=new_tag.rfind("tag-");
126  if(tag_pos!=std::string::npos)
127  new_tag.erase(0, tag_pos+4);
128  const std::string new_tag_base=new_tag;
129 
130  for(std::pair<unique_tagst::iterator, bool>
131  unique_entry=unique_tags.insert(std::make_pair(new_tag, 0));
132  !unique_entry.second;
133  unique_entry=unique_tags.insert(std::make_pair(new_tag, 0)))
134  {
135  new_tag=new_tag_base+"$"+
136  std::to_string(unique_entry.first->second);
137  ++(unique_entry.first->second);
138  }
139 
140  if(symbol.type.id()==ID_c_enum)
141  {
142  symbol.type.add(ID_tag).set(ID_C_base_name, new_tag);
143  symbol.base_name=new_tag;
144  }
145  else
146  symbol.type.set(ID_tag, new_tag);
147  }
148 
149  // we don't want to dump in full all definitions; in particular
150  // do not dump anonymous types that are defined in system headers
151  if((!tag_added || symbol.is_type) && ignore(symbol))
152  continue;
153 
154  bool inserted=symbols_sorted.insert(name_str).second;
155  CHECK_RETURN(inserted);
156  }
157 
159 
160  // collect all declarations we might need, include local static variables
161  bool skip_function_main=false;
162  for(std::set<std::string>::const_iterator
163  it=symbols_sorted.begin();
164  it!=symbols_sorted.end();
165  ++it)
166  {
167  const symbolt &symbol=ns.lookup(*it);
168  const irep_idt &type_id=symbol.type.id();
169 
170  if(symbol.is_type &&
171  symbol.location.get_function().empty() &&
172  (type_id==ID_struct ||
173  type_id==ID_incomplete_struct ||
174  type_id==ID_union ||
175  type_id==ID_incomplete_union ||
176  type_id==ID_c_enum))
177  {
178  if(!ignore(symbol))
179  {
180  global_decl_stream << "// " << symbol.name << '\n';
181  global_decl_stream << "// " << symbol.location << '\n';
182 
183  if(type_id==ID_c_enum)
184  convert_compound_enum(symbol.type, global_decl_stream);
185  else
186  global_decl_stream << type_to_string(symbol_typet(symbol.name))
187  << ";\n\n";
188  }
189  }
190  else if(symbol.is_static_lifetime && symbol.type.id()!=ID_code)
192  symbol,
193  global_var_stream,
194  local_static_decls);
195  else if(symbol.type.id()==ID_code)
196  {
197  goto_functionst::function_mapt::const_iterator func_entry=
198  goto_functions.function_map.find(symbol.name);
199 
200  if(func_entry!=goto_functions.function_map.end() &&
201  func_entry->second.body_available() &&
202  (symbol.name==ID_main ||
203  (!config.main.empty() && symbol.name==config.main)))
204  skip_function_main=true;
205  }
206  }
207 
208  // function declarations and definitions
209  for(std::set<std::string>::const_iterator
210  it=symbols_sorted.begin();
211  it!=symbols_sorted.end();
212  ++it)
213  {
214  const symbolt &symbol=ns.lookup(*it);
215 
216  if(symbol.type.id()!=ID_code ||
217  symbol.is_type)
218  continue;
219 
221  symbol,
222  skip_function_main,
223  func_decl_stream,
224  func_body_stream,
225  local_static_decls);
226  }
227 
228  // (possibly modified) compound types
229  for(std::set<std::string>::const_iterator
230  it=symbols_sorted.begin();
231  it!=symbols_sorted.end();
232  ++it)
233  {
234  const symbolt &symbol=ns.lookup(*it);
235 
236  if(symbol.is_type &&
237  (symbol.type.id()==ID_struct ||
238  symbol.type.id()==ID_incomplete_struct ||
239  symbol.type.id()==ID_union ||
240  symbol.type.id()==ID_incomplete_union))
242  symbol,
243  compound_body_stream);
244  }
245 
246  // Dump the code to the target stream;
247  // the statements before to this point collect the code to dump!
248  for(std::set<std::string>::const_iterator
249  it=system_headers.begin();
250  it!=system_headers.end();
251  ++it)
252  os << "#include <" << *it << ">\n";
253  if(!system_headers.empty())
254  os << '\n';
255 
256  if(global_var_stream.str().find("NULL")!=std::string::npos ||
257  func_body_stream.str().find("NULL")!=std::string::npos)
258  {
259  os << "#ifndef NULL\n"
260  << "#define NULL ((void*)0)\n"
261  << "#endif\n\n";
262  }
263  if(func_body_stream.str().find("FENCE")!=std::string::npos)
264  {
265  os << "#ifndef FENCE\n"
266  << "#define FENCE(x) ((void)0)\n"
267  << "#endif\n\n";
268  }
269  if(func_body_stream.str().find("IEEE_FLOAT_")!=std::string::npos)
270  {
271  os << "#ifndef IEEE_FLOAT_EQUAL\n"
272  << "#define IEEE_FLOAT_EQUAL(x,y) ((x)==(y))\n"
273  << "#endif\n"
274  << "#ifndef IEEE_FLOAT_NOTEQUAL\n"
275  << "#define IEEE_FLOAT_NOTEQUAL(x,y) ((x)!=(y))\n"
276  << "#endif\n\n";
277  }
278 
279  if(!global_decl_stream.str().empty())
280  os << global_decl_stream.str() << '\n';
281 
282  dump_typedefs(os);
283 
284  if(!func_decl_stream.str().empty())
285  os << func_decl_stream.str() << '\n';
286  if(!compound_body_stream.str().empty())
287  os << compound_body_stream.str() << '\n';
288  if(!global_var_stream.str().empty())
289  os << global_var_stream.str() << '\n';
290  os << func_body_stream.str();
291 }
292 
295  const symbolt &symbol,
296  std::ostream &os_body)
297 {
298  if(!symbol.location.get_function().empty())
299  return;
300 
301  // do compound type body
302  if(symbol.type.id()==ID_struct ||
303  symbol.type.id()==ID_union ||
304  symbol.type.id()==ID_c_enum)
305  convert_compound(symbol.type, symbol_typet(symbol.name), true, os_body);
306 }
307 
309  const typet &type,
310  const typet &unresolved,
311  bool recursive,
312  std::ostream &os)
313 {
314  if(type.id()==ID_symbol)
315  {
316  const symbolt &symbol=
317  ns.lookup(to_symbol_type(type).get_identifier());
318  DATA_INVARIANT(symbol.is_type, "symbol expected to be type symbol");
319 
320  if(!ignore(symbol))
321  convert_compound(symbol.type, unresolved, recursive, os);
322  }
323  else if(type.id()==ID_c_enum_tag)
324  {
325  const symbolt &symbol=
326  ns.lookup(to_c_enum_tag_type(type).get_identifier());
327  DATA_INVARIANT(symbol.is_type, "symbol expected to be type symbol");
328 
329  if(!ignore(symbol))
330  convert_compound(symbol.type, unresolved, recursive, os);
331  }
332  else if(type.id()==ID_array || type.id()==ID_pointer)
333  {
334  if(!recursive)
335  return;
336 
337  convert_compound(type.subtype(), type.subtype(), recursive, os);
338 
339  // sizeof may contain a type symbol that has to be declared first
340  if(type.id()==ID_array)
341  {
342  find_symbols_sett syms;
343  find_non_pointer_type_symbols(to_array_type(type).size(), syms);
344 
345  for(find_symbols_sett::const_iterator
346  it=syms.begin();
347  it!=syms.end();
348  ++it)
349  {
350  symbol_typet s_type(*it);
351  convert_compound(s_type, s_type, recursive, os);
352  }
353  }
354  }
355  else if(type.id()==ID_struct || type.id()==ID_union)
356  convert_compound(to_struct_union_type(type), unresolved, recursive, os);
357  else if(type.id()==ID_c_enum)
358  convert_compound_enum(type, os);
359 }
360 
362  const struct_union_typet &type,
363  const typet &unresolved,
364  bool recursive,
365  std::ostream &os)
366 {
367  const irep_idt &name=type.get(ID_tag);
368 
369  if(!converted_compound.insert(name).second)
370  return;
371 
372  // make sure typedef names used in the declaration are available
373  collect_typedefs(type, true);
374 
375  const irept &bases = type.find(ID_bases);
376  std::stringstream base_decls;
377  forall_irep(parent_it, bases.get_sub())
378  {
379  UNREACHABLE;
380  /*
381  assert(parent_it->id() == ID_base);
382  assert(parent_it->get(ID_type) == ID_symbol);
383 
384  const irep_idt &base_id=
385  parent_it->find(ID_type).get(ID_identifier);
386  const irep_idt &renamed_base_id=global_renaming[base_id];
387  const symbolt &parsymb=ns.lookup(renamed_base_id);
388 
389  convert_compound_rec(parsymb.type, os);
390 
391  base_decls << id2string(renamed_base_id) +
392  (parent_it+1==bases.get_sub().end()?"":", ");
393  */
394  }
395 
396  /*
397  // for the constructor
398  string constructor_args;
399  string constructor_body;
400 
401  std::string component_name = id2string(renaming[compo.get(ID_name)]);
402  assert(component_name != "");
403 
404  if(it != struct_type.components().begin()) constructor_args += ", ";
405 
406  if(compo.type().id() == ID_pointer)
407  constructor_args += type_to_string(compo.type()) + component_name;
408  else
409  constructor_args += "const " + type_to_string(compo.type()) + "& " + component_name;
410 
411  constructor_body += indent + indent + "this->"+component_name + " = " + component_name + ";\n";
412  */
413 
414  std::stringstream struct_body;
415 
416  for(struct_union_typet::componentst::const_iterator
417  it=type.components().begin();
418  it!=type.components().end();
419  it++)
420  {
421  const struct_typet::componentt &comp=*it;
422  const typet &comp_type=ns.follow(comp.type());
423 
424  if(comp_type.id()==ID_code ||
425  comp.get_bool(ID_from_base) ||
426  comp.get_is_padding())
427  continue;
428 
429  const typet *non_array_type=&ns.follow(comp_type);
430  while(non_array_type->id()==ID_array)
431  non_array_type=&(ns.follow(non_array_type->subtype()));
432 
433  if(recursive)
434  {
435  if(non_array_type->id()!=ID_pointer)
436  convert_compound(comp.type(), comp.type(), recursive, os);
437  else
438  collect_typedefs(comp.type(), true);
439  }
440 
441  irep_idt comp_name=comp.get_name();
442 
443  struct_body << indent(1) << "// " << comp_name << '\n';
444  struct_body << indent(1);
445 
446  // component names such as "main" would collide with other objects in the
447  // namespace
448  std::string fake_unique_name="NO/SUCH/NS::"+id2string(comp_name);
449  std::string s=make_decl(fake_unique_name, comp.type());
450  POSTCONDITION(s.find("NO/SUCH/NS")==std::string::npos);
451 
452  if(comp_type.id()==ID_c_bit_field &&
453  to_c_bit_field_type(comp_type).get_width()==0)
454  {
455  comp_name="";
456  s=type_to_string(comp_type);
457  }
458 
459  if(s.find("__CPROVER_bitvector")==std::string::npos)
460  {
461  struct_body << s;
462  }
463  else if(comp_type.id()==ID_signedbv)
464  {
465  const signedbv_typet &t=to_signedbv_type(comp_type);
467  struct_body << "long long int " << comp_name
468  << " : " << t.get_width();
469  else if(language->id()=="cpp")
470  struct_body << "__signedbv<" << t.get_width() << "> "
471  << comp_name;
472  else
473  struct_body << s;
474  }
475  else if(comp_type.id()==ID_unsignedbv)
476  {
477  const unsignedbv_typet &t=to_unsignedbv_type(comp_type);
479  struct_body << "unsigned long long " << comp_name
480  << " : " << t.get_width();
481  else if(language->id()=="cpp")
482  struct_body << "__unsignedbv<" << t.get_width() << "> "
483  << comp_name;
484  else
485  struct_body << s;
486  }
487  else
488  UNREACHABLE;
489 
490  struct_body << ";\n";
491  }
492 
493  typet unresolved_clean=unresolved;
494  typedef_typest::const_iterator td_entry=
495  typedef_types.find(unresolved);
496  irep_idt typedef_str;
497  if(td_entry!=typedef_types.end())
498  {
499  unresolved_clean.remove(ID_C_typedef);
500  typedef_str=td_entry->second;
501  std::pair<typedef_mapt::iterator, bool> td_map_entry=
502  typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
503  PRECONDITION(!td_map_entry.second);
504  if(!td_map_entry.first->second.early)
505  td_map_entry.first->second.type_decl_str="";
506  os << "typedef ";
507  }
508 
509  os << type_to_string(unresolved_clean);
510  if(!base_decls.str().empty())
511  {
512  PRECONDITION(language->id()=="cpp");
513  os << ": " << base_decls.str();
514  }
515  os << '\n';
516  os << "{\n";
517  os << struct_body.str();
518 
519  /*
520  if(!struct_type.components().empty())
521  {
522  os << indent << name << "(){}\n";
523  os << indent << "explicit " << name
524  << "(" + constructor_args + ")\n";
525  os << indent << "{\n";
526  os << constructor_body;
527  os << indent << "}\n";
528  }
529  */
530 
531  os << "}";
532  if(type.get_bool(ID_C_transparent_union))
533  os << " __attribute__ ((__transparent_union__))";
534  if(type.get_bool(ID_C_packed))
535  os << " __attribute__ ((__packed__))";
536  if(!typedef_str.empty())
537  os << " " << typedef_str;
538  os << ";\n\n";
539 }
540 
542  const typet &type,
543  std::ostream &os)
544 {
545  PRECONDITION(type.id()==ID_c_enum);
546 
547  const irept &tag=type.find(ID_tag);
548  const irep_idt &name=tag.get(ID_C_base_name);
549 
550  if(tag.is_nil() ||
551  !converted_enum.insert(name).second)
552  return;
553 
554  c_enum_typet enum_type=to_c_enum_type(type);
555  c_enum_typet::memberst &members=
556  (c_enum_typet::memberst &)(enum_type.add(ID_body).get_sub());
557  for(c_enum_typet::memberst::iterator
558  it=members.begin();
559  it!=members.end();
560  ++it)
561  {
562  const irep_idt bn=it->get_base_name();
563 
564  if(declared_enum_constants.find(bn)!=
565  declared_enum_constants.end() ||
567  {
568  std::string new_bn=id2string(name)+"$$"+id2string(bn);
569  it->set_base_name(new_bn);
570  }
571 
573  std::make_pair(bn, it->get_base_name()));
574  }
575 
576  os << type_to_string(enum_type);
577 
578  if(enum_type.get_bool(ID_C_packed))
579  os << " __attribute__ ((__packed__))";
580 
581  os << ";\n\n";
582 }
583 
584 #define ADD_TO_SYSTEM_LIBRARY(v, header) \
585  for(size_t i=0; i<sizeof(v)/sizeof(char*); ++i) \
586  system_library_map.insert( \
587  std::make_pair(v[i], header))
588 
590 {
591  // ctype.h
592  const char* ctype_syms[]=
593  {
594  "isalnum", "isalpha", "isblank", "iscntrl", "isdigit", "isgraph",
595  "islower", "isprint", "ispunct", "isspace", "isupper", "isxdigit",
596  "tolower", "toupper"
597  };
598  ADD_TO_SYSTEM_LIBRARY(ctype_syms, "ctype.h");
599 
600  // fcntl.h
601  const char* fcntl_syms[]=
602  {
603  "creat", "fcntl", "open"
604  };
605  ADD_TO_SYSTEM_LIBRARY(fcntl_syms, "fcntl.h");
606 
607  // locale.h
608  const char* locale_syms[]=
609  {
610  "setlocale"
611  };
612  ADD_TO_SYSTEM_LIBRARY(locale_syms, "locale.h");
613 
614  // math.h
615  const char* math_syms[]=
616  {
617  "acos", "acosh", "asin", "asinh", "atan", "atan2", "atanh",
618  "cbrt", "ceil", "copysign", "cos", "cosh", "erf", "erfc", "exp",
619  "exp2", "expm1", "fabs", "fdim", "floor", "fma", "fmax", "fmin",
620  "fmod", "fpclassify", "frexp", "hypot", "ilogb", "isfinite",
621  "isinf", "isnan", "isnormal", "j0", "j1", "jn", "ldexp", "lgamma",
622  "llrint", "llround", "log", "log10", "log1p", "log2", "logb",
623  "lrint", "lround", "modf", "nan", "nearbyint", "nextafter", "pow",
624  "remainder", "remquo", "rint", "round", "scalbln", "scalbn",
625  "signbit", "sin", "sinh", "sqrt", "tan", "tanh", "tgamma",
626  "trunc", "y0", "y1", "yn"
627  };
628  ADD_TO_SYSTEM_LIBRARY(math_syms, "math.h");
629 
630  // pthread.h
631  const char* pthread_syms[]=
632  {
633  "pthread_cleanup_pop", "pthread_cleanup_push",
634  "pthread_cond_broadcast", "pthread_cond_destroy",
635  "pthread_cond_init", "pthread_cond_signal",
636  "pthread_cond_timedwait", "pthread_cond_wait", "pthread_create",
637  "pthread_detach", "pthread_equal", "pthread_exit",
638  "pthread_getspecific", "pthread_join", "pthread_key_delete",
639  "pthread_mutex_destroy", "pthread_mutex_init",
640  "pthread_mutex_lock", "pthread_mutex_trylock",
641  "pthread_mutex_unlock", "pthread_once", "pthread_rwlock_destroy",
642  "pthread_rwlock_init", "pthread_rwlock_rdlock",
643  "pthread_rwlock_unlock", "pthread_rwlock_wrlock",
644  "pthread_rwlockattr_destroy", "pthread_rwlockattr_getpshared",
645  "pthread_rwlockattr_init", "pthread_rwlockattr_setpshared",
646  "pthread_self", "pthread_setspecific",
647  /* non-public struct types */
648  "tag-__pthread_internal_list", "tag-__pthread_mutex_s",
649  "pthread_mutex_t"
650  };
651  ADD_TO_SYSTEM_LIBRARY(pthread_syms, "pthread.h");
652 
653  // setjmp.h
654  const char* setjmp_syms[]=
655  {
656  "_longjmp", "_setjmp", "longjmp", "longjmperror", "setjmp",
657  "siglongjmp", "sigsetjmp"
658  };
659  ADD_TO_SYSTEM_LIBRARY(setjmp_syms, "setjmp.h");
660 
661  // stdio.h
662  const char* stdio_syms[]=
663  {
664  "asprintf", "clearerr", "fclose", "fdopen", "feof", "ferror",
665  "fflush", "fgetc", "fgetln", "fgetpos", "fgets", "fgetwc",
666  "fgetws", "fileno", "fopen", "fprintf", "fpurge", "fputc",
667  "fputs", "fputwc", "fputws", "fread", "freopen", "fropen",
668  "fscanf", "fseek", "fsetpos", "ftell", "funopen", "fwide",
669  "fwopen", "fwprintf", "fwrite", "getc", "getchar", "getdelim",
670  "getline", "gets", "getw", "getwc", "getwchar", "mkdtemp",
671  "mkstemp", "mktemp", "perror", "printf", "putc", "putchar",
672  "puts", "putw", "putwc", "putwchar", "remove", "rewind", "scanf",
673  "setbuf", "setbuffer", "setlinebuf", "setvbuf", "snprintf",
674  "sprintf", "sscanf", "swprintf", "sys_errlist",
675  "sys_nerr", "tempnam", "tmpfile", "tmpnam", "ungetc", "ungetwc",
676  "vasprintf", "vfprintf", "vfscanf", "vfwprintf", "vprintf",
677  "vscanf", "vsnprintf", "vsprintf", "vsscanf", "vswprintf",
678  "vwprintf", "wprintf",
679  /* non-public struct types */
680  "tag-__sFILE", "tag-__sbuf", // OS X
681  "tag-_IO_FILE", "tag-_IO_marker", // Linux
682  };
683  ADD_TO_SYSTEM_LIBRARY(stdio_syms, "stdio.h");
684 
685  // stdlib.h
686  const char* stdlib_syms[]=
687  {
688  "abort", "abs", "atexit", "atof", "atoi", "atol", "atoll",
689  "bsearch", "calloc", "div", "exit", "free", "getenv", "labs",
690  "ldiv", "llabs", "lldiv", "malloc", "mblen", "mbstowcs", "mbtowc",
691  "qsort", "rand", "realloc", "srand", "strtod", "strtof", "strtol",
692  "strtold", "strtoll", "strtoul", "strtoull", "system", "wcstombs",
693  "wctomb"
694  };
695  ADD_TO_SYSTEM_LIBRARY(stdlib_syms, "stdlib.h");
696 
697  // string.h
698  const char* string_syms[]=
699  {
700  "strcat", "strncat", "strchr", "strrchr", "strcmp", "strncmp",
701  "strcpy", "strncpy", "strerror", "strlen", "strpbrk", "strspn",
702  "strcspn", "strstr", "strtok"
703  };
704  ADD_TO_SYSTEM_LIBRARY(string_syms, "string.h");
705 
706  // time.h
707  const char* time_syms[]=
708  {
709  "asctime", "asctime_r", "ctime", "ctime_r", "difftime", "gmtime",
710  "gmtime_r", "localtime", "localtime_r", "mktime", "strftime",
711  /* non-public struct types */
712  "tag-timespec", "tag-timeval", "tag-tm"
713  };
714  ADD_TO_SYSTEM_LIBRARY(time_syms, "time.h");
715 
716  // unistd.h
717  const char* unistd_syms[]=
718  {
719  "_exit", "access", "alarm", "chdir", "chown", "close", "dup",
720  "dup2", "execl", "execle", "execlp", "execv", "execve", "execvp",
721  "fork", "fpathconf", "getcwd", "getegid", "geteuid", "getgid",
722  "getgroups", "getlogin", "getpgrp", "getpid", "getppid", "getuid",
723  "isatty", "link", "lseek", "pathconf", "pause", "pipe", "read",
724  "rmdir", "setgid", "setpgid", "setsid", "setuid", "sleep",
725  "sysconf", "tcgetpgrp", "tcsetpgrp", "ttyname", "ttyname_r",
726  "unlink", "write"
727  };
728  ADD_TO_SYSTEM_LIBRARY(unistd_syms, "unistd.h");
729 
730  // sys/select.h
731  const char* sys_select_syms[]=
732  {
733  "select",
734  /* non-public struct types */
735  "fd_set"
736  };
737  ADD_TO_SYSTEM_LIBRARY(sys_select_syms, "sys/select.h");
738 
739  // sys/socket.h
740  const char* sys_socket_syms[]=
741  {
742  "accept", "bind", "connect",
743  /* non-public struct types */
744  "tag-sockaddr"
745  };
746  ADD_TO_SYSTEM_LIBRARY(sys_socket_syms, "sys/socket.h");
747 
748  // sys/stat.h
749  const char* sys_stat_syms[]=
750  {
751  "fstat", "lstat", "stat",
752  /* non-public struct types */
753  "tag-stat"
754  };
755  ADD_TO_SYSTEM_LIBRARY(sys_stat_syms, "sys/stat.h");
756 
757  /*
758  // sys/types.h
759  const char* sys_types_syms[]=
760  {
761  };
762  ADD_TO_SYSTEM_LIBRARY(sys_types_syms, "sys/types.h");
763  */
764 
765  // sys/wait.h
766  const char* sys_wait_syms[]=
767  {
768  "wait", "waitpid"
769  };
770  ADD_TO_SYSTEM_LIBRARY(sys_wait_syms, "sys/wait.h");
771 }
772 
773 /*******************************************************************\
774 
775 Function: dump_ct::ignore
776 
777 Inputs: type input to check whether it should not be dumped
778 
779 Outputs: true, iff the type should not be printed
780 
781 Purpose: Ignore selected types as they are covered via system headers
782 
783 \*******************************************************************/
784 
785 bool dump_ct::ignore(const typet &type)
786 {
787  symbolt symbol;
788  symbol.type=type;
789 
790  return ignore(symbol);
791 }
792 
793 /*******************************************************************\
794 
795 Function: dump_ct::ignore
796 
797 Inputs: type input to check whether it should not be dumped
798 
799 Outputs: true, iff the symbol should not be printed
800 
801 Purpose: Ignore selected symbols as they are covered via system headers
802 
803 \*******************************************************************/
804 
805 bool dump_ct::ignore(const symbolt &symbol)
806 {
807  const std::string &name_str=id2string(symbol.name);
808 
809  if(has_prefix(name_str, CPROVER_PREFIX) ||
810  name_str=="__func__" ||
811  name_str=="__FUNCTION__" ||
812  name_str=="__PRETTY_FUNCTION__" ||
813  name_str=="argc'" ||
814  name_str=="argv'" ||
815  name_str=="envp'" ||
816  name_str=="envp_size'")
817  return true;
818 
819  if(has_suffix(name_str, "$object"))
820  return true;
821 
822  const std::string &file_str=id2string(symbol.location.get_file());
823 
824  // don't dump internal GCC builtins
825  if(has_prefix(file_str, "gcc_builtin_headers_") &&
826  has_prefix(name_str, "__builtin_"))
827  return true;
828 
829  if(name_str=="__builtin_va_start" ||
830  name_str=="__builtin_va_end" ||
831  symbol.name==ID_gcc_builtin_va_arg)
832  {
833  system_headers.insert("stdarg.h");
834  return true;
835  }
836 
837  system_library_mapt::const_iterator it=
838  system_library_map.find(symbol.name);
839 
840  if(it!=system_library_map.end())
841  {
842  system_headers.insert(it->second);
843  return true;
844  }
845 
846  if(use_all_headers &&
847  has_prefix(file_str, "/usr/include/"))
848  {
849  if(file_str.find("/bits/")==std::string::npos)
850  {
851  // Do not include transitive includes of system headers!
852  std::string::size_type prefix_len=std::string("/usr/include/").size();
853  system_headers.insert(file_str.substr(prefix_len));
854  }
855 
856  return true;
857  }
858 
859  return false;
860 }
861 
863  code_declt &decl,
864  std::list<irep_idt> &local_static,
865  std::list<irep_idt> &local_type_decls)
866 {
867  exprt value=nil_exprt();
868 
869  if(decl.operands().size()==2)
870  {
871  value=decl.op1();
872  decl.operands().resize(1);
873  }
874 
875  goto_programt tmp;
877  t->code=decl;
878 
879  if(value.is_not_nil())
880  {
881  t=tmp.add_instruction(ASSIGN);
882  t->code=code_assignt(decl.op0(), value);
883  }
884 
886 
887  std::unordered_set<irep_idt, irep_id_hash> typedef_names;
888  for(const auto &td : typedef_map)
889  typedef_names.insert(td.first);
890 
891  code_blockt b;
892  goto_program2codet p2s(
893  irep_idt(),
894  tmp,
896  b,
897  local_static,
898  local_type_decls,
899  typedef_names,
901  p2s();
902 
903  POSTCONDITION(b.operands().size()==1);
904  decl.swap(b.op0());
905 }
906 
907 /*******************************************************************\
908 
909 Function: dump_ct::collect_typedefs
910 
911 Inputs:
912  type Type to inspect for ID_C_typedef entry
913  early Set to true to enforce that typedef is dumped before any
914  function declarations or struct definitions
915 
916 Outputs:
917 
918 Purpose: Find any typedef names contained in the input type and store
919  their declaration strings in typedef_map for eventual output.
920 
921 \*******************************************************************/
922 
923 void dump_ct::collect_typedefs(const typet &type, bool early)
924 {
925  std::unordered_set<irep_idt, irep_id_hash> deps;
926  collect_typedefs_rec(type, early, deps);
927 }
928 
929 /*******************************************************************\
930 
931 Function: dump_ct::collect_typedefs_rec
932 
933 Inputs:
934  type Type to inspect for ID_C_typedef entry
935  early Set to true to enforce that typedef is dumped before any
936  function declarations or struct definitions
937  dependencies Typedefs used in the declaration of a given typedef
938 
939 Outputs:
940 
941 Purpose: Find any typedef names contained in the input type and store
942  their declaration strings in typedef_map for eventual output.
943 
944 \*******************************************************************/
945 
947  const typet &type,
948  bool early,
949  std::unordered_set<irep_idt, irep_id_hash> &dependencies)
950 {
951  if(ignore(type))
952  return;
953 
954  std::unordered_set<irep_idt, irep_id_hash> local_deps;
955 
956  if(type.id()==ID_code)
957  {
958  const code_typet &code_type=to_code_type(type);
959 
960  collect_typedefs_rec(code_type.return_type(), early, local_deps);
961  for(const auto &param : code_type.parameters())
962  collect_typedefs_rec(param.type(), early, local_deps);
963  }
964  else if(type.id()==ID_pointer || type.id()==ID_array)
965  {
966  collect_typedefs_rec(type.subtype(), early, local_deps);
967  }
968  else if(type.id()==ID_symbol)
969  {
970  const symbolt &symbol=
971  ns.lookup(to_symbol_type(type).get_identifier());
972  collect_typedefs_rec(symbol.type, early, local_deps);
973  }
974 
975  const irep_idt &typedef_str=type.get(ID_C_typedef);
976 
977  if(!typedef_str.empty())
978  {
979  std::pair<typedef_mapt::iterator, bool> entry=
980  typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
981 
982  if(entry.second ||
983  (early && entry.first->second.type_decl_str.empty()))
984  {
985  if(typedef_str=="__gnuc_va_list" || typedef_str == "va_list")
986  {
987  system_headers.insert("stdarg.h");
988  early=false;
989  }
990  else
991  {
992  typet t=type;
993  t.remove(ID_C_typedef);
994 
995  std::ostringstream oss;
996  oss << "typedef " << make_decl(typedef_str, t) << ';';
997 
998  entry.first->second.type_decl_str=oss.str();
999  entry.first->second.dependencies=local_deps;
1000  }
1001  }
1002 
1003  if(early)
1004  {
1005  entry.first->second.early=true;
1006 
1007  for(const auto &d : local_deps)
1008  {
1009  auto td_entry=typedef_map.find(d);
1010  PRECONDITION(td_entry!=typedef_map.end());
1011  td_entry->second.early=true;
1012  }
1013  }
1014 
1015  dependencies.insert(typedef_str);
1016  }
1017 
1018  dependencies.insert(local_deps.begin(), local_deps.end());
1019 }
1020 
1021 /*******************************************************************\
1022 
1023 Function: dump_ct::gather_global_typedefs
1024 
1025 Inputs:
1026 
1027 Outputs:
1028 
1029 Purpose: find all global typdefs in the symbol table and store them
1030  in typedef_types
1031 
1032 \*******************************************************************/
1033 
1035 {
1036  // sort the symbols first to ensure deterministic replacement in
1037  // typedef_types below as there could be redundant declarations
1038  // typedef int x;
1039  // typedef int y;
1040  std::map<std::string, symbolt> symbols_sorted;
1041  for(const auto &symbol_entry : copied_symbol_table.symbols)
1042  symbols_sorted.insert(
1043  {id2string(symbol_entry.first), symbol_entry.second});
1044 
1045  for(const auto &symbol_entry : symbols_sorted)
1046  {
1047  const symbolt &symbol=symbol_entry.second;
1048 
1049  if(symbol.is_macro && symbol.is_type &&
1050  symbol.location.get_function().empty())
1051  {
1052  const irep_idt &typedef_str=symbol.type.get(ID_C_typedef);
1053  PRECONDITION(!typedef_str.empty());
1054  typedef_types[symbol.type]=typedef_str;
1055  if(ignore(symbol))
1056  typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
1057  else
1058  collect_typedefs(symbol.type, false);
1059  }
1060  }
1061 }
1062 
1063 /*******************************************************************\
1064 
1065 Function: dump_ct::dump_typedefs
1066 
1067 Inputs:
1068 
1069 Outputs: os output stream
1070 
1071 Purpose: print all typedefs that are not covered via
1072  typedef struct xyz { ... } name;
1073 
1074 \*******************************************************************/
1075 
1076 void dump_ct::dump_typedefs(std::ostream &os) const
1077 {
1078  // we need to compute a topological sort; we do so by picking all
1079  // typedefs the dependencies of which have been emitted into to_insert
1080  std::vector<typedef_infot> typedefs_sorted;
1081  typedefs_sorted.reserve(typedef_map.size());
1082 
1083  // elements in to_insert are lexicographically sorted and ready for
1084  // output
1085  std::map<std::string, typedef_infot> to_insert;
1086 
1087  typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
1088  id_sett typedefs_done;
1089  std::unordered_map<irep_idt, id_sett, irep_id_hash>
1090  forward_deps, reverse_deps;
1091 
1092  for(const auto &td : typedef_map)
1093  if(!td.second.type_decl_str.empty())
1094  {
1095  if(td.second.dependencies.empty())
1096  // those can be dumped immediately
1097  to_insert.insert({id2string(td.first), td.second});
1098  else
1099  {
1100  // delay them until dependencies are dumped
1101  forward_deps.insert({td.first, td.second.dependencies});
1102  for(const auto &d : td.second.dependencies)
1103  reverse_deps[d].insert(td.first);
1104  }
1105  }
1106 
1107  while(!to_insert.empty())
1108  {
1109  // the topologically next element (lexicographically ranked first
1110  // among all the dependencies of which have been dumped)
1111  typedef_infot t=to_insert.begin()->second;
1112  to_insert.erase(to_insert.begin());
1113  // move to the output queue
1114  typedefs_sorted.push_back(t);
1115 
1116  // find any depending typedefs that are now valid, or at least
1117  // reduce the remaining dependencies
1118  auto r_it=reverse_deps.find(t.typedef_name);
1119  if(r_it==reverse_deps.end())
1120  continue;
1121 
1122  // reduce remaining dependencies
1123  id_sett &r_deps=r_it->second;
1124  for(id_sett::iterator it=r_deps.begin(); it!=r_deps.end(); ) // no ++it
1125  {
1126  auto f_it=forward_deps.find(*it);
1127  if(f_it==forward_deps.end()) // might be done already
1128  {
1129  it=r_deps.erase(it);
1130  continue;
1131  }
1132 
1133  // update dependencies
1134  id_sett &f_deps=f_it->second;
1135  PRECONDITION(!f_deps.empty());
1136  PRECONDITION(f_deps.find(t.typedef_name)!=f_deps.end());
1137  f_deps.erase(t.typedef_name);
1138 
1139  if(f_deps.empty()) // all depenencies done now!
1140  {
1141  const auto td_entry=typedef_map.find(*it);
1142  PRECONDITION(td_entry!=typedef_map.end());
1143  to_insert.insert({id2string(*it), td_entry->second});
1144  forward_deps.erase(*it);
1145  it=r_deps.erase(it);
1146  }
1147  else
1148  ++it;
1149  }
1150  }
1151 
1152  POSTCONDITION(forward_deps.empty());
1153 
1154  for(const auto &td : typedefs_sorted)
1155  os << td.type_decl_str << '\n';
1156 
1157  if(!typedefs_sorted.empty())
1158  os << '\n';
1159 }
1160 
1162  const symbolt &symbol,
1163  std::ostream &os,
1164  local_static_declst &local_static_decls)
1165 {
1166  const irep_idt &func=symbol.location.get_function();
1167  if((func.empty() || symbol.is_extern || symbol.value.is_not_nil()) &&
1168  !converted_global.insert(symbol.name).second)
1169  return;
1170 
1171  code_declt d(symbol.symbol_expr());
1172 
1173  find_symbols_sett syms;
1174  if(symbol.value.is_not_nil())
1175  find_symbols(symbol.value, syms);
1176 
1177  // add a tentative declaration to cater for symbols in the initializer
1178  // relying on it this symbol
1179  if((func.empty() || symbol.is_extern) &&
1180  (symbol.value.is_nil() || !syms.empty()))
1181  {
1182  os << "// " << symbol.name << '\n';
1183  os << "// " << symbol.location << '\n';
1184  os << expr_to_string(d) << '\n';
1185  }
1186 
1187  if(!symbol.value.is_nil())
1188  {
1189  std::set<std::string> symbols_sorted;
1190  for(find_symbols_sett::const_iterator
1191  it=syms.begin();
1192  it!=syms.end();
1193  ++it)
1194  {
1195  bool inserted=symbols_sorted.insert(id2string(*it)).second;
1196  CHECK_RETURN(inserted);
1197  }
1198 
1199  for(std::set<std::string>::const_iterator
1200  it=symbols_sorted.begin();
1201  it!=symbols_sorted.end();
1202  ++it)
1203  {
1204  const symbolt &sym=ns.lookup(*it);
1205  if(!sym.is_type && sym.is_static_lifetime && sym.type.id()!=ID_code)
1206  convert_global_variable(sym, os, local_static_decls);
1207  }
1208 
1209  d.copy_to_operands(symbol.value);
1210  }
1211 
1212  if(!func.empty() && !symbol.is_extern)
1213  local_static_decls[symbol.name]=d;
1214  else if(!symbol.value.is_nil())
1215  {
1216  os << "// " << symbol.name << '\n';
1217  os << "// " << symbol.location << '\n';
1218 
1219  std::list<irep_idt> empty_static, empty_types;
1220  cleanup_decl(d, empty_static, empty_types);
1221  CHECK_RETURN(empty_static.empty());
1222  os << expr_to_string(d) << '\n';
1223  }
1224 }
1225 
1227  const symbolt &symbol,
1228  const bool skip_main,
1229  std::ostream &os_decl,
1230  std::ostream &os_body,
1231  local_static_declst &local_static_decls)
1232 {
1233  // don't dump artificial main
1234  if(skip_main && symbol.name==goto_functionst::entry_point())
1235  return;
1236 
1237  // convert the goto program back to code - this might change
1238  // the function type
1239  goto_functionst::function_mapt::const_iterator func_entry=
1240  goto_functions.function_map.find(symbol.name);
1241  if(func_entry!=goto_functions.function_map.end() &&
1242  func_entry->second.body_available())
1243  {
1244  code_blockt b;
1245  std::list<irep_idt> type_decls, local_static;
1246 
1247  std::unordered_set<irep_idt, irep_id_hash> typedef_names;
1248  for(const auto &td : typedef_map)
1249  typedef_names.insert(td.first);
1250 
1251  goto_program2codet p2s(
1252  symbol.name,
1253  func_entry->second.body,
1255  b,
1256  local_static,
1257  type_decls,
1258  typedef_names,
1259  system_headers);
1260  p2s();
1261 
1263  b,
1264  local_static,
1265  local_static_decls,
1266  type_decls);
1267 
1268  convertedt converted_c_bak(converted_compound);
1269  convertedt converted_e_bak(converted_enum);
1270 
1272  enum_constants_bak(declared_enum_constants);
1273 
1275  b,
1276  type_decls);
1277 
1278  converted_enum.swap(converted_e_bak);
1279  converted_compound.swap(converted_c_bak);
1280 
1281  os_body << "// " << symbol.name << '\n';
1282  os_body << "// " << symbol.location << '\n';
1283  os_body << make_decl(symbol.name, symbol.type) << '\n';
1284  os_body << expr_to_string(b);
1285  os_body << "\n\n";
1286 
1287  declared_enum_constants.swap(enum_constants_bak);
1288  }
1289 
1290  if(symbol.name!=goto_functionst::entry_point() &&
1291  symbol.name!=ID_main)
1292  {
1293  os_decl << "// " << symbol.name << '\n';
1294  os_decl << "// " << symbol.location << '\n';
1295  os_decl << make_decl(symbol.name, symbol.type) << ";\n";
1296  }
1297 
1298  // make sure typedef names used in the function declaration are
1299  // available
1300  collect_typedefs(symbol.type, true);
1301 }
1302 
1304  const irep_idt &identifier,
1305  codet &root,
1306  code_blockt* &dest,
1307  exprt::operandst::iterator &before)
1308 {
1309  if(!root.has_operands())
1310  return false;
1311 
1312  code_blockt *our_dest=nullptr;
1313 
1314  exprt::operandst &operands=root.operands();
1315  exprt::operandst::iterator first_found=operands.end();
1316 
1317  Forall_expr(it, operands)
1318  {
1319  bool found=false;
1320 
1321  // be aware of the skip-carries-type hack
1322  if(it->id()==ID_code &&
1323  to_code(*it).get_statement()!=ID_skip)
1325  identifier,
1326  to_code(*it),
1327  our_dest,
1328  before);
1329  else
1330  {
1331  find_symbols_sett syms;
1332  find_type_and_expr_symbols(*it, syms);
1333 
1334  found=syms.find(identifier)!=syms.end();
1335  }
1336 
1337  if(!found)
1338  continue;
1339 
1340  if(!our_dest)
1341  {
1342  // first containing block
1343  if(root.get_statement()==ID_block)
1344  {
1345  dest=&(to_code_block(root));
1346  before=it;
1347  }
1348 
1349  return true;
1350  }
1351  else
1352  {
1353  // there is a containing block and this is the first operand
1354  // that contains identifier
1355  if(first_found==operands.end())
1356  first_found=it;
1357  // we have seen it already - pick the first occurrence in this
1358  // block
1359  else if(root.get_statement()==ID_block)
1360  {
1361  dest=&(to_code_block(root));
1362  before=first_found;
1363 
1364  return true;
1365  }
1366  // we have seen it already - outer block has to deal with this
1367  else
1368  return true;
1369  }
1370  }
1371 
1372  if(first_found!=operands.end())
1373  {
1374  dest=our_dest;
1375 
1376  return true;
1377  }
1378 
1379  return false;
1380 }
1381 
1383  code_blockt &b,
1384  const std::list<irep_idt> &local_static,
1385  local_static_declst &local_static_decls,
1386  std::list<irep_idt> &type_decls)
1387 {
1388  // look up last identifier first as its value may introduce the
1389  // other ones
1390  for(std::list<irep_idt>::const_reverse_iterator
1391  it=local_static.rbegin();
1392  it!=local_static.rend();
1393  ++it)
1394  {
1395  local_static_declst::const_iterator d_it=
1396  local_static_decls.find(*it);
1397  PRECONDITION(d_it!=local_static_decls.end());
1398 
1399  code_declt d=d_it->second;
1400  std::list<irep_idt> redundant;
1401  cleanup_decl(d, redundant, type_decls);
1402 
1403  code_blockt *dest_ptr=nullptr;
1404  exprt::operandst::iterator before=b.operands().end();
1405 
1406  // some use of static variables might be optimised out if it is
1407  // within an if(false) { ... } block
1408  if(find_block_position_rec(*it, b, dest_ptr, before))
1409  {
1410  CHECK_RETURN(dest_ptr!=nullptr);
1411  dest_ptr->operands().insert(before, d);
1412  }
1413  }
1414 }
1415 
1417  code_blockt &b,
1418  const std::list<irep_idt> &type_decls)
1419 {
1420  // look up last identifier first as its value may introduce the
1421  // other ones
1422  for(std::list<irep_idt>::const_reverse_iterator
1423  it=type_decls.rbegin();
1424  it!=type_decls.rend();
1425  ++it)
1426  {
1427  const typet &type=ns.lookup(*it).type;
1428  // feed through plain C to expr2c by ending and re-starting
1429  // a comment block ...
1430  std::ostringstream os_body;
1431  os_body << *it << " */\n";
1432  convert_compound(type, symbol_typet(*it), false, os_body);
1433  os_body << "/*";
1434 
1435  code_skipt skip;
1436  skip.add_source_location().set_comment(os_body.str());
1437  // another hack to ensure symbols inside types are seen
1438  skip.type()=type;
1439 
1440  code_blockt *dest_ptr=nullptr;
1441  exprt::operandst::iterator before=b.operands().end();
1442 
1443  // we might not find it in case a transparent union type cast
1444  // has been removed by cleanup operations
1445  if(find_block_position_rec(*it, b, dest_ptr, before))
1446  {
1447  CHECK_RETURN(dest_ptr!=nullptr);
1448  dest_ptr->operands().insert(before, skip);
1449  }
1450  }
1451 }
1452 
1454 {
1455  Forall_operands(it, expr)
1456  cleanup_expr(*it);
1457 
1458  cleanup_type(expr.type());
1459 
1460  if(expr.id()==ID_struct)
1461  {
1462  struct_typet type=
1463  to_struct_type(ns.follow(expr.type()));
1464 
1465  struct_union_typet::componentst old_components;
1466  old_components.swap(type.components());
1467 
1468  exprt::operandst old_ops;
1469  old_ops.swap(expr.operands());
1470 
1471  PRECONDITION(old_components.size()==old_ops.size());
1472  exprt::operandst::iterator o_it=old_ops.begin();
1473  for(struct_union_typet::componentst::const_iterator
1474  it=old_components.begin();
1475  it!=old_components.end();
1476  ++it)
1477  {
1478  const bool is_zero_bit_field=
1479  it->type().id()==ID_c_bit_field &&
1480  to_c_bit_field_type(it->type()).get_width()==0;
1481 
1482  if(!it->get_is_padding() && !is_zero_bit_field)
1483  {
1484  type.components().push_back(*it);
1485  expr.move_to_operands(*o_it);
1486  }
1487  ++o_it;
1488  }
1489  expr.type().swap(type);
1490  }
1491  else if(expr.id()==ID_union)
1492  {
1493  union_exprt &u=to_union_expr(expr);
1494  const union_typet &u_type_f=to_union_type(ns.follow(u.type()));
1495 
1496  if(!u.type().get_bool(ID_C_transparent_union) &&
1497  !u_type_f.get_bool(ID_C_transparent_union))
1498  {
1499  if(u_type_f.get_component(u.get_component_name()).get_is_padding())
1500  // we just use an empty struct to fake an empty union
1501  expr=struct_exprt(struct_typet());
1502  }
1503  // add a typecast for NULL
1504  else if(u.op().id()==ID_constant &&
1505  u.op().type().id()==ID_pointer &&
1506  u.op().type().subtype().id()==ID_empty &&
1507  (u.op().is_zero() ||
1508  to_constant_expr(u.op()).get_value()==ID_NULL))
1509  {
1510  const struct_union_typet::componentt &comp=
1511  u_type_f.get_component(u.get_component_name());
1512  const typet &u_op_type=comp.type();
1513  PRECONDITION(u_op_type.id()==ID_pointer);
1514 
1515  typecast_exprt tc(u.op(), u_op_type);
1516  expr.swap(tc);
1517  }
1518  else
1519  {
1520  exprt tmp;
1521  tmp.swap(u.op());
1522  expr.swap(tmp);
1523  }
1524  }
1525  else if(expr.id()==ID_typecast &&
1526  expr.op0().id()==ID_typecast &&
1527  base_type_eq(expr.type(), expr.op0().type(), ns))
1528  {
1529  exprt tmp=expr.op0();
1530  expr.swap(tmp);
1531  }
1532  else if(expr.id()==ID_code &&
1533  to_code(expr).get_statement()==ID_function_call &&
1534  to_code_function_call(to_code(expr)).function().id()==ID_symbol)
1535  {
1537  const symbol_exprt &fn=to_symbol_expr(call.function());
1538  code_function_callt::argumentst &arguments=call.arguments();
1539 
1540  // don't edit function calls we might have introduced
1541  const symbolt *s;
1542  if(!ns.lookup(fn.get_identifier(), s))
1543  {
1544  const symbolt &fn_sym=ns.lookup(fn.get_identifier());
1545  const code_typet &code_type=to_code_type(fn_sym.type);
1546  const code_typet::parameterst &parameters=code_type.parameters();
1547 
1548  if(parameters.size()==arguments.size())
1549  {
1550  code_typet::parameterst::const_iterator it=parameters.begin();
1551  Forall_expr(it2, arguments)
1552  {
1553  const typet &type=ns.follow(it->type());
1554  if(type.id()==ID_union &&
1555  type.get_bool(ID_C_transparent_union))
1556  {
1557  if(it2->id()==ID_typecast &&
1558  base_type_eq(it2->type(), type, ns))
1559  *it2=to_typecast_expr(*it2).op();
1560 
1561  // add a typecast for NULL or 0
1562  if(it2->id()==ID_constant &&
1563  (it2->is_zero() || to_constant_expr(*it2).get_value()==ID_NULL))
1564  {
1565  const typet &comp_type=
1566  to_union_type(type).components().front().type();
1567 
1568  if(comp_type.id()==ID_pointer)
1569  *it2=typecast_exprt(*it2, comp_type);
1570  }
1571  }
1572 
1573  ++it;
1574  }
1575  }
1576  }
1577  }
1578  else if(expr.id()==ID_constant &&
1579  expr.type().id()==ID_signedbv)
1580  {
1581  #if 0
1582  const irep_idt &cformat=expr.get(ID_C_cformat);
1583 
1584  if(!cformat.empty())
1585  {
1586  declared_enum_constants_mapt::const_iterator entry=
1587  declared_enum_constants.find(cformat);
1588 
1589  if(entry!=declared_enum_constants.end() &&
1590  entry->first!=entry->second)
1591  expr.set(ID_C_cformat, entry->second);
1592  else if(entry==declared_enum_constants.end() &&
1593  !std::isdigit(id2string(cformat)[0]))
1594  expr.remove(ID_C_cformat);
1595  }
1596  #endif
1597  }
1598 }
1599 
1601 {
1602  Forall_subtypes(it, type)
1603  cleanup_type(*it);
1604 
1605  if(type.id()==ID_code)
1606  {
1607  code_typet &code_type=to_code_type(type);
1608 
1609  cleanup_type(code_type.return_type());
1610 
1611  for(code_typet::parameterst::iterator
1612  it=code_type.parameters().begin();
1613  it!=code_type.parameters().end();
1614  ++it)
1615  cleanup_type(it->type());
1616  }
1617 
1618  if(type.id()==ID_array)
1619  cleanup_expr(to_array_type(type).size());
1620 
1621  POSTCONDITION(
1622  (type.id()!=ID_union && type.id()!=ID_struct) ||
1623  !type.get(ID_tag).empty());
1624 }
1625 
1626 std::string dump_ct::type_to_string(const typet &type)
1627 {
1628  std::string ret;
1629  typet t=type;
1630  cleanup_type(t);
1631  language->from_type(t, ret, ns);
1632  return ret;
1633 }
1634 
1635 std::string dump_ct::expr_to_string(const exprt &expr)
1636 {
1637  std::string ret;
1638  exprt e=expr;
1639  cleanup_expr(e);
1640  language->from_expr(e, ret, ns);
1641  return ret;
1642 }
1643 
1644 void dump_c(
1645  const goto_functionst &src,
1646  const bool use_system_headers,
1647  const bool use_all_headers,
1648  const namespacet &ns,
1649  std::ostream &out)
1650 {
1651  dump_ct goto2c(
1652  src, use_system_headers, use_all_headers, ns, new_ansi_c_language);
1653  out << goto2c;
1654 }
1655 
1657  const goto_functionst &src,
1658  const bool use_system_headers,
1659  const bool use_all_headers,
1660  const namespacet &ns,
1661  std::ostream &out)
1662 {
1663  dump_ct goto2cpp(
1664  src, use_system_headers, use_all_headers, ns, new_cpp_language);
1665  out << goto2cpp;
1666 }
const irep_idt & get_statement() const
Definition: std_code.h:37
const irep_idt & get_name() const
Definition: std_types.h:179
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
std::unordered_set< irep_idt, irep_id_hash > convertedt
Definition: dump_c_class.h:55
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
struct configt::ansi_ct ansi_c
void collect_typedefs(const typet &type, bool early)
Definition: dump_c.cpp:923
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1125
semantic type conversion
Definition: std_expr.h:1725
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
targett add_instruction()
Adds an instruction at the end.
void init_system_library_map()
Definition: dump_c.cpp:589
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
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:1382
#define forall_symbols(it, expr)
Definition: symbol_table.h:28
exprt & op0()
Definition: expr.h:84
#define CPROVER_PREFIX
const exprt & op() const
Definition: std_expr.h:258
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
void set_comment(const irep_idt &comment)
declared_enum_constants_mapt declared_enum_constants
Definition: dump_c_class.h:66
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:442
const irep_idt & get_function() const
const namespacet ns
Definition: dump_c_class.h:51
std::unordered_map< irep_idt, code_declt, irep_id_hash > local_static_declst
Definition: dump_c_class.h:140
const irep_idt & get_identifier() const
Definition: std_expr.h:120
std::string type_to_string(const typet &type)
Definition: dump_c.cpp:1626
std::ostream & operator<<(std::ostream &out, dump_ct &src)
Definition: dump_c.cpp:31
languaget * new_ansi_c_language()
std::vector< componentt > componentst
Definition: std_types.h:240
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
const irep_idt & get_value() const
Definition: std_expr.h:3702
std::string expr_to_string(const exprt &expr)
Definition: dump_c.cpp:1635
std::vector< parametert > parameterst
Definition: std_types.h:829
exprt value
Initial value of symbol.
Definition: symbol.h:40
const componentst & components() const
Definition: std_types.h:242
void collect_typedefs_rec(const typet &type, bool early, std::unordered_set< irep_idt, irep_id_hash > &dependencies)
Definition: dump_c.cpp:946
Dump C from Goto Program.
Dump Goto-Program as C/C++ Source.
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:121
typet & type()
Definition: expr.h:60
exprt::operandst argumentst
Definition: std_code.h:687
unsignedbv_typet size_type()
Definition: c_types.cpp:57
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
const goto_functionst & goto_functions
Definition: dump_c_class.h:49
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:240
Structure type.
Definition: std_types.h:296
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
exprt & op()
Definition: std_expr.h:1739
configt config
Definition: config.cpp:21
#define POSTCONDITION(CONDITION)
Definition: invariant.h:232
bool is_static_lifetime
Definition: symbol.h:70
convertedt converted_enum
Definition: dump_c_class.h:56
subt & get_sub()
Definition: irep.h:245
std::unordered_set< irep_idt, irep_id_hash > find_symbols_sett
Definition: find_symbols.h:20
const bool use_all_headers
Definition: dump_c_class.h:53
static bool find_block_position_rec(const irep_idt &identifier, codet &root, code_blockt *&dest, exprt::operandst::iterator &before)
Definition: dump_c.cpp:1303
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:277
#define Forall_symbols(it, expr)
Definition: symbol_table.h:32
std::string make_decl(const irep_idt &identifier, const typet &type)
Definition: dump_c_class.h:100
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
typedef_typest typedef_types
Definition: dump_c_class.h:85
void insert_local_type_decls(code_blockt &b, const std::list< irep_idt > &type_decls)
Definition: dump_c.cpp:1416
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a generic typet to a c_enum_typet.
Definition: std_types.h:680
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:142
argumentst & arguments()
Definition: std_code.h:689
symbolst symbols
Definition: symbol_table.h:57
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
Definition: std_types.h:717
A reference into the symbol table.
Definition: std_types.h:109
A declaration of a local variable.
Definition: std_code.h:192
#define Forall_expr(it, expr)
Definition: expr.h:32
The NIL expression.
Definition: std_expr.h:3764
virtual std::string id() const
Definition: language.h:82
unsigned long_long_int_width
Definition: config.h:35
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1171
system_library_mapt system_library_map
Definition: dump_c_class.h:62
std::string main
Definition: config.h:147
union constructor from single element
Definition: std_expr.h:1389
void convert_compound(const typet &type, const typet &unresolved, bool recursive, std::ostream &os)
Definition: dump_c.cpp:308
void cleanup_decl(code_declt &decl, std::list< irep_idt > &local_static, std::list< irep_idt > &local_type_decls)
Definition: dump_c.cpp:862
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:52
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
C++ Language Module.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void gather_global_typedefs()
Definition: dump_c.cpp:1034
#define PRECONDITION(CONDITION)
Definition: invariant.h:225
const exprt & size() const
Definition: std_types.h:915
Base class for tree-like data structures with sharing.
Definition: irep.h:87
A function call.
Definition: std_code.h:657
languaget * new_cpp_language()
void dump_cpp(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const namespacet &ns, std::ostream &out)
Definition: dump_c.cpp:1656
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
Definition: std_expr.h:1441
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
Definition: std_types.h:1319
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1154
std::set< std::string > system_headers
Definition: dump_c_class.h:58
convertedt converted_global
Definition: dump_c_class.h:56
bool has_operands() const
Definition: expr.h:67
std::size_t get_width() const
Definition: std_types.h:1030
void find_non_pointer_type_symbols(const exprt &src, find_symbols_sett &dest)
std::vector< exprt > operandst
Definition: expr.h:49
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
Dump Goto-Program as C/C++ Source.
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
bool ignore(const symbolt &symbol)
Definition: dump_c.cpp:805
bool is_extern
Definition: symbol.h:71
virtual bool from_type(const typet &type, std::string &code, const namespacet &ns)
Definition: language.cpp:41
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
const irep_idt & get_file() const
typedef_mapt typedef_map
Definition: dump_c_class.h:83
void convert_compound_declaration(const symbolt &symbol, std::ostream &os_body)
declare compound types
Definition: dump_c.cpp:294
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:159
void cleanup_expr(exprt &expr)
Definition: dump_c.cpp:1453
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
The union type.
Definition: std_types.h:424
const parameterst & parameters() const
Definition: std_types.h:841
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1200
#define UNREACHABLE
Definition: invariant.h:245
irept & add(const irep_namet &name)
Definition: irep.cpp:306
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
void convert_compound_enum(const typet &type, std::ostream &os)
Definition: dump_c.cpp:541
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
#define Forall_subtypes(it, type)
Definition: type.h:165
void dump_c(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const namespacet &ns, std::ostream &out)
Definition: dump_c.cpp:1644
void operator()(std::ostream &out)
Definition: dump_c.cpp:37
void swap(irept &irep)
Definition: irep.h:231
irep_idt get_component_name() const
Definition: std_expr.h:1410
#define Forall_operands(it, expr)
Definition: expr.h:23
bool has_symbol(const irep_idt &name) const
Definition: symbol_table.h:87
bool is_zero() const
Definition: expr.cpp:236
source_locationt & add_source_location()
Definition: expr.h:147
Sequential composition.
Definition: std_code.h:63
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
static std::string indent(const unsigned n)
Definition: dump_c_class.h:95
Skip.
Definition: std_code.h:134
Expression to hold a symbol (variable)
Definition: std_expr.h:82
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:1226
languaget * language
Definition: dump_c_class.h:52
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:120
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
void dump_typedefs(std::ostream &os) const
Definition: dump_c.cpp:1076
dstringt irep_idt
Definition: irep.h:32
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
A statement in a programming language.
Definition: std_code.h:19
virtual bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
Definition: language.cpp:32
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
void remove(const irep_namet &name)
Definition: irep.cpp:270
bool is_type
Definition: symbol.h:66
Base Type Computation.
const typet & subtype() const
Definition: type.h:31
convertedt converted_compound
Definition: dump_c_class.h:56
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:252
operandst & operands()
Definition: expr.h:70
void cleanup_type(typet &type)
Definition: dump_c.cpp:1600
symbol_tablet copied_symbol_table
Definition: dump_c_class.h:50
void convert_global_variable(const symbolt &symbol, std::ostream &os, local_static_declst &local_static_decls)
Definition: dump_c.cpp:1161
struct constructor from list of elements
Definition: std_expr.h:1464
std::unordered_map< irep_idt, irep_idt, irep_id_hash > declared_enum_constants_mapt
Definition: dump_c_class.h:65
std::vector< c_enum_membert > memberst
Definition: std_types.h:662
bool empty() const
Definition: dstring.h:61
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
void find_symbols(const exprt &src, find_symbols_sett &dest)
The type of C enums.
Definition: std_types.h:637
const typet & return_type() const
Definition: std_types.h:831
bool is_macro
Definition: symbol.h:66
Assignment.
Definition: std_code.h:144
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
const componentt & get_component(const irep_idt &component_name) const
Definition: std_types.cpp:51
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700
#define ADD_TO_SYSTEM_LIBRARY(v, header)
Definition: dump_c.cpp:584
#define forall_irep(it, irep)
Definition: irep.h:62