cprover
expr2c.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "expr2c.h"
10 
11 #include <algorithm>
12 #include <sstream>
13 
14 #include <map>
15 
16 #include <util/arith_tools.h>
17 #include <util/c_types.h>
18 #include <util/config.h>
19 #include <util/cprover_prefix.h>
20 #include <util/find_symbols.h>
21 #include <util/fixedbv.h>
22 #include <util/floatbv_expr.h>
23 #include <util/lispexpr.h>
24 #include <util/lispirep.h>
25 #include <util/namespace.h>
26 #include <util/pointer_expr.h>
28 #include <util/prefix.h>
29 #include <util/string_constant.h>
30 #include <util/string_utils.h>
31 #include <util/suffix.h>
32 #include <util/symbol.h>
33 
34 #include "c_misc.h"
35 #include "c_qualifiers.h"
36 #include "expr2c_class.h"
37 
38 // clang-format off
39 
41 {
42  true,
43  true,
44  true,
45  "TRUE",
46  "FALSE",
47  true,
48  false,
49  false
50 };
51 
53 {
54  false,
55  false,
56  false,
57  "1",
58  "0",
59  false,
60  true,
61  true
62 };
63 
64 // clang-format on
65 /*
66 
67 Precedences are as follows. Higher values mean higher precedence.
68 
69 16 function call ()
70  ++ -- [] . ->
71 
72 1 comma
73 
74 */
75 
76 irep_idt expr2ct::id_shorthand(const irep_idt &identifier) const
77 {
78  const symbolt *symbol;
79 
80  if(!ns.lookup(identifier, symbol) &&
81  !symbol->base_name.empty() &&
82  has_suffix(id2string(identifier), id2string(symbol->base_name)))
83  return symbol->base_name;
84 
85  std::string sh=id2string(identifier);
86 
87  std::string::size_type pos=sh.rfind("::");
88  if(pos!=std::string::npos)
89  sh.erase(0, pos+2);
90 
91  return sh;
92 }
93 
94 static std::string clean_identifier(const irep_idt &id)
95 {
96  std::string dest=id2string(id);
97 
98  std::string::size_type c_pos=dest.find("::");
99  if(c_pos!=std::string::npos &&
100  dest.rfind("::")==c_pos)
101  dest.erase(0, c_pos+2);
102  else if(c_pos!=std::string::npos)
103  {
104  for(char &ch : dest)
105  if(ch == ':')
106  ch = '$';
107  else if(ch == '-')
108  ch = '_';
109  }
110 
111  // rewrite . as used in ELF section names
112  std::replace(dest.begin(), dest.end(), '.', '_');
113 
114  return dest;
115 }
116 
118 {
119  const std::unordered_set<irep_idt> symbols = find_symbol_identifiers(expr);
120 
121  // avoid renaming parameters, if possible
122  for(const auto &symbol_id : symbols)
123  {
124  const symbolt *symbol;
125  bool is_param = !ns.lookup(symbol_id, symbol) && symbol->is_parameter;
126 
127  if(!is_param)
128  continue;
129 
130  irep_idt sh = id_shorthand(symbol_id);
131 
132  std::string func = id2string(symbol_id);
133  func = func.substr(0, func.rfind("::"));
134 
135  // if there is a global symbol of the same name as the shorthand (even if
136  // not present in this particular expression) then there is a collision
137  const symbolt *global_symbol;
138  if(!ns.lookup(sh, global_symbol))
139  sh = func + "$$" + id2string(sh);
140 
141  ns_collision[func].insert(sh);
142 
143  if(!shorthands.insert(std::make_pair(symbol_id, sh)).second)
144  UNREACHABLE;
145  }
146 
147  for(const auto &symbol_id : symbols)
148  {
149  if(shorthands.find(symbol_id) != shorthands.end())
150  continue;
151 
152  irep_idt sh = id_shorthand(symbol_id);
153 
154  bool has_collision=
155  ns_collision[irep_idt()].find(sh)!=
156  ns_collision[irep_idt()].end();
157 
158  if(!has_collision)
159  {
160  // if there is a global symbol of the same name as the shorthand (even if
161  // not present in this particular expression) then there is a collision
162  const symbolt *symbol;
163  has_collision=!ns.lookup(sh, symbol);
164  }
165 
166  if(!has_collision)
167  {
168  irep_idt func;
169 
170  const symbolt *symbol;
171  // we use the source-level function name as a means to detect collisions,
172  // which is ok, because this is about generating user-visible output
173  if(!ns.lookup(symbol_id, symbol))
174  func=symbol->location.get_function();
175 
176  has_collision=!ns_collision[func].insert(sh).second;
177  }
178 
179  if(!has_collision)
180  {
181  // We could also conflict with a function argument, the code below
182  // finds the function we're in, and checks we don't conflict with
183  // any argument to the function
184  const std::string symbol_str = id2string(symbol_id);
185  const std::string func = symbol_str.substr(0, symbol_str.find("::"));
186  const symbolt *func_symbol;
187  if(!ns.lookup(func, func_symbol))
188  {
189  if(can_cast_type<code_typet>(func_symbol->type))
190  {
191  const auto func_type =
192  type_checked_cast<code_typet>(func_symbol->type);
193  const auto params = func_type.parameters();
194  for(const auto &param : params)
195  {
196  const auto param_id = param.get_identifier();
197  if(param_id != symbol_id && sh == id_shorthand(param_id))
198  {
199  has_collision = true;
200  break;
201  }
202  }
203  }
204  }
205  }
206 
207  if(has_collision)
208  sh = clean_identifier(symbol_id);
209 
210  shorthands.insert(std::make_pair(symbol_id, sh));
211  }
212 }
213 
214 std::string expr2ct::convert(const typet &src)
215 {
216  return convert_rec(src, c_qualifierst(), "");
217 }
218 
220  const typet &src,
221  const qualifierst &qualifiers,
222  const std::string &declarator)
223 {
224  std::unique_ptr<qualifierst> clone = qualifiers.clone();
225  c_qualifierst &new_qualifiers = dynamic_cast<c_qualifierst &>(*clone);
226  new_qualifiers.read(src);
227 
228  std::string q=new_qualifiers.as_string();
229 
230  std::string d = declarator.empty() ? declarator : " " + declarator;
231 
232  if(!configuration.expand_typedef && src.find(ID_C_typedef).is_not_nil())
233  {
234  return q+id2string(src.get(ID_C_typedef))+d;
235  }
236 
237  if(src.id()==ID_bool)
238  {
239  return q + CPROVER_PREFIX + "bool" + d;
240  }
241  else if(src.id()==ID_c_bool)
242  {
243  return q+"_Bool"+d;
244  }
245  else if(src.id()==ID_string)
246  {
247  return q + CPROVER_PREFIX + "string" + d;
248  }
249  else if(src.id()==ID_natural ||
250  src.id()==ID_integer ||
251  src.id()==ID_rational)
252  {
253  return q+src.id_string()+d;
254  }
255  else if(src.id()==ID_empty)
256  {
257  return q+"void"+d;
258  }
259  else if(src.id()==ID_complex)
260  {
261  // these take more or less arbitrary subtypes
262  return q+"_Complex "+convert(src.subtype())+d;
263  }
264  else if(src.id()==ID_floatbv)
265  {
266  std::size_t width=to_floatbv_type(src).get_width();
267 
268  if(width==config.ansi_c.single_width)
269  return q+"float"+d;
270  else if(width==config.ansi_c.double_width)
271  return q+"double"+d;
272  else if(width==config.ansi_c.long_double_width)
273  return q+"long double"+d;
274  else
275  {
276  std::string swidth = std::to_string(width);
277  std::string fwidth=src.get_string(ID_f);
278  return q + CPROVER_PREFIX + "floatbv[" + swidth + "][" + fwidth + "]";
279  }
280  }
281  else if(src.id()==ID_fixedbv)
282  {
283  const std::size_t width=to_fixedbv_type(src).get_width();
284 
285  const std::size_t fraction_bits=to_fixedbv_type(src).get_fraction_bits();
286  return q + CPROVER_PREFIX + "fixedbv[" + std::to_string(width) + "][" +
287  std::to_string(fraction_bits) + "]" + d;
288  }
289  else if(src.id()==ID_c_bit_field)
290  {
291  std::string width=std::to_string(to_c_bit_field_type(src).get_width());
292  return q+convert(src.subtype())+d+" : "+width;
293  }
294  else if(src.id()==ID_signedbv ||
295  src.id()==ID_unsignedbv)
296  {
297  // annotated?
298  irep_idt c_type=src.get(ID_C_c_type);
299  const std::string c_type_str=c_type_as_string(c_type);
300 
301  if(c_type==ID_char &&
302  config.ansi_c.char_is_unsigned!=(src.id()==ID_unsignedbv))
303  {
304  if(src.id()==ID_signedbv)
305  return q+"signed char"+d;
306  else
307  return q+"unsigned char"+d;
308  }
309  else if(c_type!=ID_wchar_t && !c_type_str.empty())
310  return q+c_type_str+d;
311 
312  // There is also wchar_t among the above, but this isn't a C type.
313 
314  const std::size_t width = to_bitvector_type(src).get_width();
315 
316  bool is_signed=src.id()==ID_signedbv;
317  std::string sign_str=is_signed?"signed ":"unsigned ";
318 
319  if(width==config.ansi_c.int_width)
320  {
321  if(is_signed)
322  sign_str.clear();
323  return q+sign_str+"int"+d;
324  }
325  else if(width==config.ansi_c.long_int_width)
326  {
327  if(is_signed)
328  sign_str.clear();
329  return q+sign_str+"long int"+d;
330  }
331  else if(width==config.ansi_c.char_width)
332  {
333  // always include sign
334  return q+sign_str+"char"+d;
335  }
336  else if(width==config.ansi_c.short_int_width)
337  {
338  if(is_signed)
339  sign_str.clear();
340  return q+sign_str+"short int"+d;
341  }
342  else if(width==config.ansi_c.long_long_int_width)
343  {
344  if(is_signed)
345  sign_str.clear();
346  return q+sign_str+"long long int"+d;
347  }
348  else if(width==128)
349  {
350  if(is_signed)
351  sign_str.clear();
352  return q + sign_str + "__int128" + d;
353  }
354  else
355  {
356  return q + sign_str + CPROVER_PREFIX + "bitvector[" +
357  integer2string(width) + "]" + d;
358  }
359  }
360  else if(src.id()==ID_struct)
361  {
362  return convert_struct_type(src, q, d);
363  }
364  else if(src.id()==ID_union)
365  {
366  const union_typet &union_type=to_union_type(src);
367 
368  std::string dest=q+"union";
369 
370  const irep_idt &tag=union_type.get_tag();
371  if(!tag.empty())
372  dest+=" "+id2string(tag);
373 
374  if(!union_type.is_incomplete())
375  {
376  dest += " {";
377 
378  for(const auto &c : union_type.components())
379  {
380  dest += ' ';
381  dest += convert_rec(c.type(), c_qualifierst(), id2string(c.get_name()));
382  dest += ';';
383  }
384 
385  dest += " }";
386  }
387 
388  dest+=d;
389 
390  return dest;
391  }
392  else if(src.id()==ID_c_enum)
393  {
394  std::string result;
395  result+=q;
396  result+="enum";
397 
398  // do we have a tag?
399  const irept &tag=src.find(ID_tag);
400 
401  if(tag.is_nil())
402  {
403  }
404  else
405  {
406  result+=' ';
407  result+=tag.get_string(ID_C_base_name);
408  }
409 
410  result+=' ';
411 
412  if(!to_c_enum_type(src).is_incomplete())
413  {
414  const c_enum_typet &c_enum_type = to_c_enum_type(src);
415  const bool is_signed = c_enum_type.subtype().id() == ID_signedbv;
416  const auto width = to_bitvector_type(c_enum_type.subtype()).get_width();
417 
418  result += '{';
419 
420  // add members
421  const c_enum_typet::memberst &members = c_enum_type.members();
422 
423  for(c_enum_typet::memberst::const_iterator it = members.begin();
424  it != members.end();
425  it++)
426  {
427  mp_integer int_value = bvrep2integer(it->get_value(), width, is_signed);
428 
429  if(it != members.begin())
430  result += ',';
431  result += ' ';
432  result += id2string(it->get_base_name());
433  result += '=';
434  result += integer2string(int_value);
435  }
436 
437  result += " }";
438  }
439 
440  result += d;
441  return result;
442  }
443  else if(src.id()==ID_c_enum_tag)
444  {
445  const c_enum_tag_typet &c_enum_tag_type=to_c_enum_tag_type(src);
446  const symbolt &symbol=ns.lookup(c_enum_tag_type);
447  std::string result=q+"enum";
448  result+=" "+id2string(symbol.base_name);
449  result+=d;
450  return result;
451  }
452  else if(src.id()==ID_pointer)
453  {
454  c_qualifierst sub_qualifiers;
455  sub_qualifiers.read(src.subtype());
456  const typet &subtype = src.subtype();
457 
458  // The star gets attached to the declarator.
459  std::string new_declarator="*";
460 
461  if(!q.empty() && (!declarator.empty() || subtype.id() == ID_pointer))
462  {
463  new_declarator+=" "+q;
464  }
465 
466  new_declarator+=declarator;
467 
468  // Depending on precedences, we may add parentheses.
469  if(
470  subtype.id() == ID_code ||
471  (sizeof_nesting == 0 && subtype.id() == ID_array))
472  {
473  new_declarator="("+new_declarator+")";
474  }
475 
476  return convert_rec(subtype, sub_qualifiers, new_declarator);
477  }
478  else if(src.id()==ID_array)
479  {
480  return convert_array_type(src, qualifiers, declarator);
481  }
482  else if(src.id()==ID_struct_tag)
483  {
484  const struct_tag_typet &struct_tag_type=
485  to_struct_tag_type(src);
486 
487  std::string dest=q+"struct";
488  const std::string &tag=ns.follow_tag(struct_tag_type).get_string(ID_tag);
489  if(!tag.empty())
490  dest+=" "+tag;
491  dest+=d;
492 
493  return dest;
494  }
495  else if(src.id()==ID_union_tag)
496  {
497  const union_tag_typet &union_tag_type=
498  to_union_tag_type(src);
499 
500  std::string dest=q+"union";
501  const std::string &tag=ns.follow_tag(union_tag_type).get_string(ID_tag);
502  if(!tag.empty())
503  dest+=" "+tag;
504  dest+=d;
505 
506  return dest;
507  }
508  else if(src.id()==ID_code)
509  {
510  const code_typet &code_type=to_code_type(src);
511 
512  // C doesn't really have syntax for function types,
513  // i.e., the following won't parse without declarator
514  std::string dest=declarator+"(";
515 
516  const code_typet::parameterst &parameters=code_type.parameters();
517 
518  if(parameters.empty())
519  {
520  if(!code_type.has_ellipsis())
521  dest+="void"; // means 'no parameters'
522  }
523  else
524  {
525  for(code_typet::parameterst::const_iterator
526  it=parameters.begin();
527  it!=parameters.end();
528  it++)
529  {
530  if(it!=parameters.begin())
531  dest+=", ";
532 
533  if(it->get_identifier().empty())
534  dest+=convert(it->type());
535  else
536  {
537  std::string arg_declarator=
538  convert(symbol_exprt(it->get_identifier(), it->type()));
539  dest+=convert_rec(it->type(), c_qualifierst(), arg_declarator);
540  }
541  }
542 
543  if(code_type.has_ellipsis())
544  dest+=", ...";
545  }
546 
547  dest+=')';
548 
549  c_qualifierst ret_qualifiers;
550  ret_qualifiers.read(code_type.return_type());
551  // _Noreturn should go with the return type
552  if(new_qualifiers.is_noreturn)
553  {
554  ret_qualifiers.is_noreturn=true;
555  new_qualifiers.is_noreturn=false;
556  q=new_qualifiers.as_string();
557  }
558 
559  const typet &return_type=code_type.return_type();
560 
561  // return type may be a function pointer or array
562  const typet *non_ptr_type = &return_type;
563  while(non_ptr_type->id()==ID_pointer)
564  non_ptr_type = &(non_ptr_type->subtype());
565 
566  if(non_ptr_type->id()==ID_code ||
567  non_ptr_type->id()==ID_array)
568  dest=convert_rec(return_type, ret_qualifiers, dest);
569  else
570  dest=convert_rec(return_type, ret_qualifiers, "")+" "+dest;
571 
572  if(!q.empty())
573  {
574  dest+=" "+q;
575  // strip trailing space off q
576  if(dest[dest.size()-1]==' ')
577  dest.resize(dest.size()-1);
578  }
579 
580  // contract, if any
581  for(auto &requires : to_code_with_contract_type(src).requires())
582  {
583  dest += " [[requires " + convert(requires) + "]]";
584  }
585 
586  if(!to_code_with_contract_type(src).assigns().operands().empty())
587  {
588  dest += " [[assigns " +
589  convert(to_code_with_contract_type(src).assigns()) + "]]";
590  }
591 
592  for(auto &ensures : to_code_with_contract_type(src).ensures())
593  {
594  dest += " [[ensures " + convert(ensures) + "]]";
595  }
596 
597  return dest;
598  }
599  else if(src.id()==ID_vector)
600  {
601  const vector_typet &vector_type=to_vector_type(src);
602 
603  const mp_integer size_int = numeric_cast_v<mp_integer>(vector_type.size());
604  std::string dest="__gcc_v"+integer2string(size_int);
605 
606  std::string tmp=convert(vector_type.subtype());
607 
608  if(tmp=="signed char" || tmp=="char")
609  dest+="qi";
610  else if(tmp=="signed short int")
611  dest+="hi";
612  else if(tmp=="signed int")
613  dest+="si";
614  else if(tmp=="signed long long int")
615  dest+="di";
616  else if(tmp=="float")
617  dest+="sf";
618  else if(tmp=="double")
619  dest+="df";
620  else
621  {
622  const std::string subtype=convert(vector_type.subtype());
623  dest=subtype;
624  dest+=" __attribute__((vector_size (";
625  dest+=convert(vector_type.size());
626  dest+="*sizeof("+subtype+"))))";
627  }
628 
629  return q+dest+d;
630  }
631  else if(src.id()==ID_constructor ||
632  src.id()==ID_destructor)
633  {
634  return q+"__attribute__(("+id2string(src.id())+")) void"+d;
635  }
636 
637  {
638  lispexprt lisp;
639  irep2lisp(src, lisp);
640  std::string dest="irep(\""+MetaString(lisp.expr2string())+"\")";
641  dest+=d;
642 
643  return dest;
644  }
645 }
646 
653 std::string expr2ct::convert_struct_type(
654  const typet &src,
655  const std::string &qualifiers_str,
656  const std::string &declarator_str)
657 {
658  return convert_struct_type(
659  src,
660  qualifiers_str,
661  declarator_str,
664 }
665 
676 std::string expr2ct::convert_struct_type(
677  const typet &src,
678  const std::string &qualifiers,
679  const std::string &declarator,
680  bool inc_struct_body,
681  bool inc_padding_components)
682 {
683  // Either we are including the body (in which case it makes sense to include
684  // or exclude the parameters) or there is no body so therefore we definitely
685  // shouldn't be including the parameters
686  assert(inc_struct_body || !inc_padding_components);
687 
688  const struct_typet &struct_type=to_struct_type(src);
689 
690  std::string dest=qualifiers+"struct";
691 
692  const irep_idt &tag=struct_type.get_tag();
693  if(!tag.empty())
694  dest+=" "+id2string(tag);
695 
696  if(inc_struct_body && !struct_type.is_incomplete())
697  {
698  dest+=" {";
699 
700  for(const auto &component : struct_type.components())
701  {
702  // Skip padding parameters unless we including them
703  if(component.get_is_padding() && !inc_padding_components)
704  {
705  continue;
706  }
707 
708  dest+=' ';
709  dest+=convert_rec(
710  component.type(),
711  c_qualifierst(),
712  id2string(component.get_name()));
713  dest+=';';
714  }
715 
716  dest+=" }";
717  }
718 
719  dest+=declarator;
720 
721  return dest;
722 }
723 
730 std::string expr2ct::convert_array_type(
731  const typet &src,
732  const qualifierst &qualifiers,
733  const std::string &declarator_str)
734 {
735  return convert_array_type(
736  src, qualifiers, declarator_str, configuration.include_array_size);
737 }
738 
747 std::string expr2ct::convert_array_type(
748  const typet &src,
749  const qualifierst &qualifiers,
750  const std::string &declarator_str,
751  bool inc_size_if_possible)
752 {
753  // The [...] gets attached to the declarator.
754  std::string array_suffix;
755 
756  if(to_array_type(src).size().is_nil() || !inc_size_if_possible)
757  array_suffix="[]";
758  else
759  array_suffix="["+convert(to_array_type(src).size())+"]";
760 
761  // This won't really parse without declarator.
762  // Note that qualifiers are passed down.
763  return convert_rec(
764  src.subtype(), qualifiers, declarator_str+array_suffix);
765 }
766 
767 std::string expr2ct::convert_typecast(
768  const typecast_exprt &src,
769  unsigned &precedence)
770 {
771  if(src.operands().size()!=1)
772  return convert_norep(src, precedence);
773 
774  // some special cases
775 
776  const typet &to_type = src.type();
777  const typet &from_type = src.op().type();
778 
779  if(to_type.id()==ID_c_bool &&
780  from_type.id()==ID_bool)
781  return convert_with_precedence(src.op(), precedence);
782 
783  if(to_type.id()==ID_bool &&
784  from_type.id()==ID_c_bool)
785  return convert_with_precedence(src.op(), precedence);
786 
787  std::string dest = "(" + convert(to_type) + ")";
788 
789  unsigned p;
790  std::string tmp=convert_with_precedence(src.op(), p);
791 
792  if(precedence>p)
793  dest+='(';
794  dest+=tmp;
795  if(precedence>p)
796  dest+=')';
797 
798  return dest;
799 }
800 
801 std::string expr2ct::convert_trinary(
802  const ternary_exprt &src,
803  const std::string &symbol1,
804  const std::string &symbol2,
805  unsigned precedence)
806 {
807  const exprt &op0=src.op0();
808  const exprt &op1=src.op1();
809  const exprt &op2=src.op2();
810 
811  unsigned p0, p1, p2;
812 
813  std::string s_op0=convert_with_precedence(op0, p0);
814  std::string s_op1=convert_with_precedence(op1, p1);
815  std::string s_op2=convert_with_precedence(op2, p2);
816 
817  std::string dest;
818 
819  if(precedence>=p0)
820  dest+='(';
821  dest+=s_op0;
822  if(precedence>=p0)
823  dest+=')';
824 
825  dest+=' ';
826  dest+=symbol1;
827  dest+=' ';
828 
829  if(precedence>=p1)
830  dest+='(';
831  dest+=s_op1;
832  if(precedence>=p1)
833  dest+=')';
834 
835  dest+=' ';
836  dest+=symbol2;
837  dest+=' ';
838 
839  if(precedence>=p2)
840  dest+='(';
841  dest+=s_op2;
842  if(precedence>=p2)
843  dest+=')';
844 
845  return dest;
846 }
847 
848 std::string expr2ct::convert_quantifier(
849  const quantifier_exprt &src,
850  const std::string &symbol,
851  unsigned precedence)
852 {
853  // our made-up syntax can only do one symbol
854  if(src.op0().operands().size() != 1)
855  return convert_norep(src, precedence);
856 
857  unsigned p0, p1;
858 
859  std::string op0 = convert_with_precedence(src.symbol(), p0);
860  std::string op1 = convert_with_precedence(src.where(), p1);
861 
862  std::string dest=symbol+" { ";
863  dest += convert(src.symbol().type());
864  dest+=" "+op0+"; ";
865  dest+=op1;
866  dest+=" }";
867 
868  return dest;
869 }
870 
871 std::string expr2ct::convert_with(
872  const exprt &src,
873  unsigned precedence)
874 {
875  if(src.operands().size()<3)
876  return convert_norep(src, precedence);
877 
878  unsigned p0;
879  const auto &old = to_with_expr(src).old();
880  std::string op0 = convert_with_precedence(old, p0);
881 
882  std::string dest;
883 
884  if(precedence>p0)
885  dest+='(';
886  dest+=op0;
887  if(precedence>p0)
888  dest+=')';
889 
890  dest+=" WITH [";
891 
892  for(size_t i=1; i<src.operands().size(); i+=2)
893  {
894  std::string op1, op2;
895  unsigned p1, p2;
896 
897  if(i!=1)
898  dest+=", ";
899 
900  if(src.operands()[i].id()==ID_member_name)
901  {
902  const irep_idt &component_name=
903  src.operands()[i].get(ID_component_name);
904 
905  const typet &full_type = ns.follow(old.type());
906 
907  const struct_union_typet &struct_union_type=
908  to_struct_union_type(full_type);
909 
910  const struct_union_typet::componentt &comp_expr=
911  struct_union_type.get_component(component_name);
912 
913  assert(comp_expr.is_not_nil());
914 
915  irep_idt display_component_name;
916 
917  if(comp_expr.get_pretty_name().empty())
918  display_component_name=component_name;
919  else
920  display_component_name=comp_expr.get_pretty_name();
921 
922  op1="."+id2string(display_component_name);
923  p1=10;
924  }
925  else
926  op1=convert_with_precedence(src.operands()[i], p1);
927 
928  op2=convert_with_precedence(src.operands()[i+1], p2);
929 
930  dest+=op1;
931  dest+=":=";
932  dest+=op2;
933  }
934 
935  dest+=']';
936 
937  return dest;
938 }
939 
940 std::string expr2ct::convert_let(
941  const let_exprt &src,
942  unsigned precedence)
943 {
944  if(src.operands().size()<3)
945  return convert_norep(src, precedence);
946 
947  unsigned p0;
948  std::string op0=convert_with_precedence(src.op0(), p0);
949 
950  std::string dest="LET ";
951  dest+=convert(src.symbol());
952  dest+='=';
953  dest+=convert(src.value());
954  dest+=" IN ";
955  dest+=convert(src.where());
956 
957  return dest;
958 }
959 
960 std::string
961 expr2ct::convert_update(const update_exprt &src, unsigned precedence)
962 {
963  std::string dest;
964 
965  dest+="UPDATE(";
966 
967  std::string op0, op1, op2;
968  unsigned p0, p2;
969 
970  op0 = convert_with_precedence(src.op0(), p0);
971  op2 = convert_with_precedence(src.op2(), p2);
972 
973  if(precedence>p0)
974  dest+='(';
975  dest+=op0;
976  if(precedence>p0)
977  dest+=')';
978 
979  dest+=", ";
980 
981  const exprt &designator = src.op1();
982 
983  forall_operands(it, designator)
984  dest+=convert(*it);
985 
986  dest+=", ";
987 
988  if(precedence>p2)
989  dest+='(';
990  dest+=op2;
991  if(precedence>p2)
992  dest+=')';
993 
994  dest+=')';
995 
996  return dest;
997 }
998 
999 std::string expr2ct::convert_cond(
1000  const exprt &src,
1001  unsigned precedence)
1002 {
1003  if(src.operands().size()<2)
1004  return convert_norep(src, precedence);
1005 
1006  bool condition=true;
1007 
1008  std::string dest="cond {\n";
1009 
1010  forall_operands(it, src)
1011  {
1012  unsigned p;
1013  std::string op=convert_with_precedence(*it, p);
1014 
1015  if(condition)
1016  dest+=" ";
1017 
1018  dest+=op;
1019 
1020  if(condition)
1021  dest+=": ";
1022  else
1023  dest+=";\n";
1024 
1025  condition=!condition;
1026  }
1027 
1028  dest+="} ";
1029 
1030  return dest;
1031 }
1032 
1033 std::string expr2ct::convert_binary(
1034  const binary_exprt &src,
1035  const std::string &symbol,
1036  unsigned precedence,
1037  bool full_parentheses)
1038 {
1039  const exprt &op0 = src.op0();
1040  const exprt &op1 = src.op1();
1041 
1042  unsigned p0, p1;
1043 
1044  std::string s_op0=convert_with_precedence(op0, p0);
1045  std::string s_op1=convert_with_precedence(op1, p1);
1046 
1047  std::string dest;
1048 
1049  // In pointer arithmetic, x+(y-z) is unfortunately
1050  // not the same as (x+y)-z, even though + and -
1051  // have the same precedence. We thus add parentheses
1052  // for the case x+(y-z). Similarly, (x*y)/z is not
1053  // the same as x*(y/z), but * and / have the same
1054  // precedence.
1055 
1056  bool use_parentheses0=
1057  precedence>p0 ||
1058  (precedence==p0 && full_parentheses) ||
1059  (precedence==p0 && src.id()!=op0.id());
1060 
1061  if(use_parentheses0)
1062  dest+='(';
1063  dest+=s_op0;
1064  if(use_parentheses0)
1065  dest+=')';
1066 
1067  dest+=' ';
1068  dest+=symbol;
1069  dest+=' ';
1070 
1071  bool use_parentheses1=
1072  precedence>p1 ||
1073  (precedence==p1 && full_parentheses) ||
1074  (precedence==p1 && src.id()!=op1.id());
1075 
1076  if(use_parentheses1)
1077  dest+='(';
1078  dest+=s_op1;
1079  if(use_parentheses1)
1080  dest+=')';
1081 
1082  return dest;
1083 }
1084 
1085 std::string expr2ct::convert_multi_ary(
1086  const exprt &src,
1087  const std::string &symbol,
1088  unsigned precedence,
1089  bool full_parentheses)
1090 {
1091  if(src.operands().size()<2)
1092  return convert_norep(src, precedence);
1093 
1094  std::string dest;
1095  bool first=true;
1096 
1097  forall_operands(it, src)
1098  {
1099  if(first)
1100  first=false;
1101  else
1102  {
1103  if(symbol!=", ")
1104  dest+=' ';
1105  dest+=symbol;
1106  dest+=' ';
1107  }
1108 
1109  unsigned p;
1110  std::string op=convert_with_precedence(*it, p);
1111 
1112  // In pointer arithmetic, x+(y-z) is unfortunately
1113  // not the same as (x+y)-z, even though + and -
1114  // have the same precedence. We thus add parentheses
1115  // for the case x+(y-z). Similarly, (x*y)/z is not
1116  // the same as x*(y/z), but * and / have the same
1117  // precedence.
1118 
1119  bool use_parentheses=
1120  precedence>p ||
1121  (precedence==p && full_parentheses) ||
1122  (precedence==p && src.id()!=it->id());
1123 
1124  if(use_parentheses)
1125  dest+='(';
1126  dest+=op;
1127  if(use_parentheses)
1128  dest+=')';
1129  }
1130 
1131  return dest;
1132 }
1133 
1134 std::string expr2ct::convert_unary(
1135  const unary_exprt &src,
1136  const std::string &symbol,
1137  unsigned precedence)
1138 {
1139  unsigned p;
1140  std::string op = convert_with_precedence(src.op(), p);
1141 
1142  std::string dest=symbol;
1143  if(precedence>=p ||
1144  (!symbol.empty() && has_prefix(op, symbol)))
1145  dest+='(';
1146  dest+=op;
1147  if(precedence>=p ||
1148  (!symbol.empty() && has_prefix(op, symbol)))
1149  dest+=')';
1150 
1151  return dest;
1152 }
1153 
1154 std::string expr2ct::convert_allocate(const exprt &src, unsigned &precedence)
1155 {
1156  if(src.operands().size() != 2)
1157  return convert_norep(src, precedence);
1158 
1159  unsigned p0;
1160  std::string op0 = convert_with_precedence(to_binary_expr(src).op0(), p0);
1161 
1162  unsigned p1;
1163  std::string op1 = convert_with_precedence(to_binary_expr(src).op1(), p1);
1164 
1165  std::string dest = "ALLOCATE";
1166  dest += '(';
1167 
1168  if(src.type().id()==ID_pointer &&
1169  src.type().subtype().id()!=ID_empty)
1170  {
1171  dest+=convert(src.type().subtype());
1172  dest+=", ";
1173  }
1174 
1175  dest += op0 + ", " + op1;
1176  dest += ')';
1177 
1178  return dest;
1179 }
1180 
1181 std::string expr2ct::convert_nondet(
1182  const exprt &src,
1183  unsigned &precedence)
1184 {
1185  if(!src.operands().empty())
1186  return convert_norep(src, precedence);
1187 
1188  return "NONDET("+convert(src.type())+")";
1189 }
1190 
1192  const exprt &src,
1193  unsigned &precedence)
1194 {
1195  if(
1196  src.operands().size() != 1 ||
1197  to_code(to_unary_expr(src).op()).get_statement() != ID_block)
1198  {
1199  return convert_norep(src, precedence);
1200  }
1201 
1202  return "(" +
1203  convert_code(to_code_block(to_code(to_unary_expr(src).op())), 0) + ")";
1204 }
1205 
1206 std::string expr2ct::convert_prob_coin(
1207  const exprt &src,
1208  unsigned &precedence)
1209 {
1210  if(src.operands().size()==1)
1211  return "COIN(" + convert(to_unary_expr(src).op()) + ")";
1212  else
1213  return convert_norep(src, precedence);
1214 }
1215 
1216 std::string expr2ct::convert_literal(const exprt &src)
1217 {
1218  return "L("+src.get_string(ID_literal)+")";
1219 }
1220 
1221 std::string expr2ct::convert_prob_uniform(
1222  const exprt &src,
1223  unsigned &precedence)
1224 {
1225  if(src.operands().size()==1)
1226  return "PROB_UNIFORM(" + convert(src.type()) + "," +
1227  convert(to_unary_expr(src).op()) + ")";
1228  else
1229  return convert_norep(src, precedence);
1230 }
1231 
1232 std::string expr2ct::convert_function(const exprt &src, const std::string &name)
1233 {
1234  std::string dest=name;
1235  dest+='(';
1236 
1237  forall_operands(it, src)
1238  {
1239  unsigned p;
1240  std::string op=convert_with_precedence(*it, p);
1241 
1242  if(it!=src.operands().begin())
1243  dest+=", ";
1244 
1245  dest+=op;
1246  }
1247 
1248  dest+=')';
1249 
1250  return dest;
1251 }
1252 
1253 std::string expr2ct::convert_comma(
1254  const exprt &src,
1255  unsigned precedence)
1256 {
1257  if(src.operands().size()!=2)
1258  return convert_norep(src, precedence);
1259 
1260  unsigned p0;
1261  std::string op0 = convert_with_precedence(to_binary_expr(src).op0(), p0);
1262  if(*op0.rbegin()==';')
1263  op0.resize(op0.size()-1);
1264 
1265  unsigned p1;
1266  std::string op1 = convert_with_precedence(to_binary_expr(src).op1(), p1);
1267  if(*op1.rbegin()==';')
1268  op1.resize(op1.size()-1);
1269 
1270  std::string dest=op0;
1271  dest+=", ";
1272  dest+=op1;
1273 
1274  return dest;
1275 }
1276 
1277 std::string expr2ct::convert_complex(
1278  const exprt &src,
1279  unsigned precedence)
1280 {
1281  if(
1282  src.operands().size() == 2 && to_binary_expr(src).op0().is_zero() &&
1283  to_binary_expr(src).op1().id() == ID_constant)
1284  {
1285  // This is believed to be gcc only; check if this is sensible
1286  // in MSC mode.
1287  return convert_with_precedence(to_binary_expr(src).op1(), precedence) + "i";
1288  }
1289 
1290  // ISO C11 offers:
1291  // double complex CMPLX(double x, double y);
1292  // float complex CMPLXF(float x, float y);
1293  // long double complex CMPLXL(long double x, long double y);
1294 
1295  const typet &subtype = src.type().subtype();
1296 
1297  std::string name;
1298 
1299  if(subtype==double_type())
1300  name="CMPLX";
1301  else if(subtype==float_type())
1302  name="CMPLXF";
1303  else if(subtype==long_double_type())
1304  name="CMPLXL";
1305  else
1306  name="CMPLX"; // default, possibly wrong
1307 
1308  std::string dest=name;
1309  dest+='(';
1310 
1311  forall_operands(it, src)
1312  {
1313  unsigned p;
1314  std::string op=convert_with_precedence(*it, p);
1315 
1316  if(it!=src.operands().begin())
1317  dest+=", ";
1318 
1319  dest+=op;
1320  }
1321 
1322  dest+=')';
1323 
1324  return dest;
1325 }
1326 
1327 std::string expr2ct::convert_array_of(
1328  const exprt &src,
1329  unsigned precedence)
1330 {
1331  if(src.operands().size()!=1)
1332  return convert_norep(src, precedence);
1333 
1334  return "ARRAY_OF(" + convert(to_unary_expr(src).op()) + ')';
1335 }
1336 
1337 std::string expr2ct::convert_byte_extract(
1338  const byte_extract_exprt &src,
1339  unsigned precedence)
1340 {
1341  if(src.operands().size()!=2)
1342  return convert_norep(src, precedence);
1343 
1344  unsigned p0;
1345  std::string op0 = convert_with_precedence(src.op0(), p0);
1346 
1347  unsigned p1;
1348  std::string op1 = convert_with_precedence(src.op1(), p1);
1349 
1350  std::string dest=src.id_string();
1351  dest+='(';
1352  dest+=op0;
1353  dest+=", ";
1354  dest+=op1;
1355  dest+=", ";
1356  dest+=convert(src.type());
1357  dest+=')';
1358 
1359  return dest;
1360 }
1361 
1362 std::string
1363 expr2ct::convert_byte_update(const byte_update_exprt &src, unsigned precedence)
1364 {
1365  unsigned p0;
1366  std::string op0 = convert_with_precedence(src.op0(), p0);
1367 
1368  unsigned p1;
1369  std::string op1 = convert_with_precedence(src.op1(), p1);
1370 
1371  unsigned p2;
1372  std::string op2 = convert_with_precedence(src.op2(), p2);
1373 
1374  std::string dest=src.id_string();
1375  dest+='(';
1376  dest+=op0;
1377  dest+=", ";
1378  dest+=op1;
1379  dest+=", ";
1380  dest+=op2;
1381  dest+=", ";
1382  dest += convert(src.op2().type());
1383  dest+=')';
1384 
1385  return dest;
1386 }
1387 
1388 std::string expr2ct::convert_unary_post(
1389  const exprt &src,
1390  const std::string &symbol,
1391  unsigned precedence)
1392 {
1393  if(src.operands().size()!=1)
1394  return convert_norep(src, precedence);
1395 
1396  unsigned p;
1397  std::string op = convert_with_precedence(to_unary_expr(src).op(), p);
1398 
1399  std::string dest;
1400  if(precedence>p)
1401  dest+='(';
1402  dest+=op;
1403  if(precedence>p)
1404  dest+=')';
1405  dest+=symbol;
1406 
1407  return dest;
1408 }
1409 
1410 std::string expr2ct::convert_index(
1411  const exprt &src,
1412  unsigned precedence)
1413 {
1414  if(src.operands().size()!=2)
1415  return convert_norep(src, precedence);
1416 
1417  unsigned p;
1418  std::string op = convert_with_precedence(to_index_expr(src).array(), p);
1419 
1420  std::string dest;
1421  if(precedence>p)
1422  dest+='(';
1423  dest+=op;
1424  if(precedence>p)
1425  dest+=')';
1426 
1427  dest+='[';
1428  dest += convert(to_index_expr(src).index());
1429  dest+=']';
1430 
1431  return dest;
1432 }
1433 
1435  const exprt &src, unsigned &precedence)
1436 {
1437  if(src.operands().size()!=2)
1438  return convert_norep(src, precedence);
1439 
1440  std::string dest="POINTER_ARITHMETIC(";
1441 
1442  unsigned p;
1443  std::string op;
1444 
1445  op = convert(to_binary_expr(src).op0().type());
1446  dest+=op;
1447 
1448  dest+=", ";
1449 
1450  op = convert_with_precedence(to_binary_expr(src).op0(), p);
1451  if(precedence>p)
1452  dest+='(';
1453  dest+=op;
1454  if(precedence>p)
1455  dest+=')';
1456 
1457  dest+=", ";
1458 
1459  op = convert_with_precedence(to_binary_expr(src).op1(), p);
1460  if(precedence>p)
1461  dest+='(';
1462  dest+=op;
1463  if(precedence>p)
1464  dest+=')';
1465 
1466  dest+=')';
1467 
1468  return dest;
1469 }
1470 
1472  const exprt &src, unsigned &precedence)
1473 {
1474  if(src.operands().size()!=2)
1475  return convert_norep(src, precedence);
1476 
1477  const auto &binary_expr = to_binary_expr(src);
1478 
1479  std::string dest="POINTER_DIFFERENCE(";
1480 
1481  unsigned p;
1482  std::string op;
1483 
1484  op = convert(binary_expr.op0().type());
1485  dest+=op;
1486 
1487  dest+=", ";
1488 
1489  op = convert_with_precedence(binary_expr.op0(), p);
1490  if(precedence>p)
1491  dest+='(';
1492  dest+=op;
1493  if(precedence>p)
1494  dest+=')';
1495 
1496  dest+=", ";
1497 
1498  op = convert_with_precedence(binary_expr.op1(), p);
1499  if(precedence>p)
1500  dest+='(';
1501  dest+=op;
1502  if(precedence>p)
1503  dest+=')';
1504 
1505  dest+=')';
1506 
1507  return dest;
1508 }
1509 
1510 std::string expr2ct::convert_member_designator(const exprt &src)
1511 {
1512  unsigned precedence;
1513 
1514  if(!src.operands().empty())
1515  return convert_norep(src, precedence);
1516 
1517  return "."+src.get_string(ID_component_name);
1518 }
1519 
1520 std::string expr2ct::convert_index_designator(const exprt &src)
1521 {
1522  unsigned precedence;
1523 
1524  if(src.operands().size()!=1)
1525  return convert_norep(src, precedence);
1526 
1527  return "[" + convert(to_unary_expr(src).op()) + "]";
1528 }
1529 
1530 std::string expr2ct::convert_member(
1531  const member_exprt &src,
1532  unsigned precedence)
1533 {
1534  const auto &compound = src.compound();
1535 
1536  unsigned p;
1537  std::string dest;
1538 
1539  if(compound.id() == ID_dereference)
1540  {
1541  const auto &pointer = to_dereference_expr(compound).pointer();
1542 
1543  std::string op = convert_with_precedence(pointer, p);
1544 
1545  if(precedence > p || pointer.id() == ID_typecast)
1546  dest+='(';
1547  dest+=op;
1548  if(precedence > p || pointer.id() == ID_typecast)
1549  dest+=')';
1550 
1551  dest+="->";
1552  }
1553  else
1554  {
1555  std::string op = convert_with_precedence(compound, p);
1556 
1557  if(precedence > p || compound.id() == ID_typecast)
1558  dest+='(';
1559  dest+=op;
1560  if(precedence > p || compound.id() == ID_typecast)
1561  dest+=')';
1562 
1563  dest+='.';
1564  }
1565 
1566  const typet &full_type = ns.follow(compound.type());
1567 
1568  if(full_type.id()!=ID_struct &&
1569  full_type.id()!=ID_union)
1570  return convert_norep(src, precedence);
1571 
1572  const struct_union_typet &struct_union_type=
1573  to_struct_union_type(full_type);
1574 
1575  irep_idt component_name=src.get_component_name();
1576 
1577  if(!component_name.empty())
1578  {
1579  const exprt &comp_expr = struct_union_type.get_component(component_name);
1580 
1581  if(comp_expr.is_nil())
1582  return convert_norep(src, precedence);
1583 
1584  if(!comp_expr.get(ID_pretty_name).empty())
1585  dest+=comp_expr.get_string(ID_pretty_name);
1586  else
1587  dest+=id2string(component_name);
1588 
1589  return dest;
1590  }
1591 
1592  std::size_t n=src.get_component_number();
1593 
1594  if(n>=struct_union_type.components().size())
1595  return convert_norep(src, precedence);
1596 
1597  const exprt &comp_expr = struct_union_type.components()[n];
1598 
1599  dest+=comp_expr.get_string(ID_pretty_name);
1600 
1601  return dest;
1602 }
1603 
1605  const exprt &src,
1606  unsigned precedence)
1607 {
1608  if(src.operands().size()!=1)
1609  return convert_norep(src, precedence);
1610 
1611  return "[]=" + convert(to_unary_expr(src).op());
1612 }
1613 
1615  const exprt &src,
1616  unsigned precedence)
1617 {
1618  if(src.operands().size()!=1)
1619  return convert_norep(src, precedence);
1620 
1621  return "." + src.get_string(ID_name) + "=" + convert(to_unary_expr(src).op());
1622 }
1623 
1624 std::string expr2ct::convert_norep(
1625  const exprt &src,
1626  unsigned &precedence)
1627 {
1628  lispexprt lisp;
1629  irep2lisp(src, lisp);
1630  std::string dest="irep(\""+MetaString(lisp.expr2string())+"\")";
1631  precedence=16;
1632  return dest;
1633 }
1634 
1635 std::string expr2ct::convert_symbol(const exprt &src)
1636 {
1637  const irep_idt &id=src.get(ID_identifier);
1638  std::string dest;
1639 
1640  if(
1641  src.operands().size() == 1 &&
1642  to_unary_expr(src).op().id() == ID_predicate_passive_symbol)
1643  {
1644  dest = to_unary_expr(src).op().get_string(ID_identifier);
1645  }
1646  else
1647  {
1648  std::unordered_map<irep_idt, irep_idt>::const_iterator entry =
1649  shorthands.find(id);
1650  // we might be called from conversion of a type
1651  if(entry==shorthands.end())
1652  {
1653  get_shorthands(src);
1654 
1655  entry=shorthands.find(id);
1656  assert(entry!=shorthands.end());
1657  }
1658 
1659  dest=id2string(entry->second);
1660 
1661  #if 0
1662  if(has_prefix(id2string(id), SYMEX_DYNAMIC_PREFIX "dynamic_object"))
1663  {
1664  if(sizeof_nesting++ == 0)
1665  dest+=" /*"+convert(src.type());
1666  if(--sizeof_nesting == 0)
1667  dest+="*/";
1668  }
1669  #endif
1670  }
1671 
1672  if(src.id()==ID_next_symbol)
1673  dest="NEXT("+dest+")";
1674 
1675  return dest;
1676 }
1677 
1679 {
1680  const irep_idt id=src.get_identifier();
1681  return "nondet_symbol("+id2string(id)+")";
1682 }
1683 
1684 std::string expr2ct::convert_predicate_symbol(const exprt &src)
1685 {
1686  const std::string &id=src.get_string(ID_identifier);
1687  return "ps("+id+")";
1688 }
1689 
1690 std::string expr2ct::convert_predicate_next_symbol(const exprt &src)
1691 {
1692  const std::string &id=src.get_string(ID_identifier);
1693  return "pns("+id+")";
1694 }
1695 
1696 std::string expr2ct::convert_predicate_passive_symbol(const exprt &src)
1697 {
1698  const std::string &id=src.get_string(ID_identifier);
1699  return "pps("+id+")";
1700 }
1701 
1702 std::string expr2ct::convert_quantified_symbol(const exprt &src)
1703 {
1704  const std::string &id=src.get_string(ID_identifier);
1705  return id;
1706 }
1707 
1708 std::string expr2ct::convert_nondet_bool()
1709 {
1710  return "nondet_bool()";
1711 }
1712 
1714  const exprt &src,
1715  unsigned &precedence)
1716 {
1717  if(src.operands().size()!=2)
1718  return convert_norep(src, precedence);
1719 
1720  std::string result="<";
1721 
1722  result += convert(to_binary_expr(src).op0());
1723  result+=", ";
1724  result += convert(to_binary_expr(src).op1());
1725  result+=", ";
1726 
1727  if(src.type().is_nil())
1728  result+='?';
1729  else
1730  result+=convert(src.type());
1731 
1732  result+='>';
1733 
1734  return result;
1735 }
1736 
1737 std::string expr2ct::convert_constant(
1738  const constant_exprt &src,
1739  unsigned &precedence)
1740 {
1741  const irep_idt &base=src.get(ID_C_base);
1742  const typet &type = src.type();
1743  const irep_idt value=src.get_value();
1744  std::string dest;
1745 
1746  if(type.id()==ID_integer ||
1747  type.id()==ID_natural ||
1748  type.id()==ID_rational)
1749  {
1750  dest=id2string(value);
1751  }
1752  else if(type.id()==ID_c_enum ||
1753  type.id()==ID_c_enum_tag)
1754  {
1755  typet c_enum_type=
1756  type.id()==ID_c_enum?to_c_enum_type(type):
1757  ns.follow_tag(to_c_enum_tag_type(type));
1758 
1759  if(c_enum_type.id()!=ID_c_enum)
1760  return convert_norep(src, precedence);
1761 
1763  {
1764  const c_enum_typet::memberst &members =
1765  to_c_enum_type(c_enum_type).members();
1766 
1767  for(const auto &member : members)
1768  {
1769  if(member.get_value() == value)
1770  return "/*enum*/" + id2string(member.get_base_name());
1771  }
1772  }
1773 
1774  // lookup failed or enum is to be output as integer
1775  const bool is_signed = c_enum_type.subtype().id() == ID_signedbv;
1776  const auto width = to_bitvector_type(c_enum_type.subtype()).get_width();
1777 
1778  std::string value_as_string =
1779  integer2string(bvrep2integer(value, width, is_signed));
1780 
1782  return value_as_string;
1783  else
1784  return "/*enum*/" + value_as_string;
1785  }
1786  else if(type.id()==ID_rational)
1787  return convert_norep(src, precedence);
1788  else if(type.id()==ID_bv)
1789  {
1790  // not C
1791  dest=id2string(value);
1792  }
1793  else if(type.id()==ID_bool)
1794  {
1795  dest=convert_constant_bool(src.is_true());
1796  }
1797  else if(type.id()==ID_unsignedbv ||
1798  type.id()==ID_signedbv ||
1799  type.id()==ID_c_bit_field ||
1800  type.id()==ID_c_bool)
1801  {
1802  const auto width = to_bitvector_type(type).get_width();
1803 
1804  mp_integer int_value =
1805  bvrep2integer(value, width, type.id() == ID_signedbv);
1806 
1807  const irep_idt &c_type=
1808  type.id()==ID_c_bit_field?type.subtype().get(ID_C_c_type):
1809  type.get(ID_C_c_type);
1810 
1811  if(type.id()==ID_c_bool)
1812  {
1813  dest=convert_constant_bool(int_value!=0);
1814  }
1815  else if(type==char_type() &&
1816  type!=signed_int_type() &&
1817  type!=unsigned_int_type())
1818  {
1819  if(int_value=='\n')
1820  dest+="'\\n'";
1821  else if(int_value=='\r')
1822  dest+="'\\r'";
1823  else if(int_value=='\t')
1824  dest+="'\\t'";
1825  else if(int_value=='\'')
1826  dest+="'\\''";
1827  else if(int_value=='\\')
1828  dest+="'\\\\'";
1829  else if(int_value>=' ' && int_value<126)
1830  {
1831  dest+='\'';
1832  dest += numeric_cast_v<char>(int_value);
1833  dest+='\'';
1834  }
1835  else
1836  dest=integer2string(int_value);
1837  }
1838  else
1839  {
1840  if(base=="16")
1841  dest="0x"+integer2string(int_value, 16);
1842  else if(base=="8")
1843  dest="0"+integer2string(int_value, 8);
1844  else if(base=="2")
1845  dest="0b"+integer2string(int_value, 2);
1846  else
1847  dest=integer2string(int_value);
1848 
1849  if(c_type==ID_unsigned_int)
1850  dest+='u';
1851  else if(c_type==ID_unsigned_long_int)
1852  dest+="ul";
1853  else if(c_type==ID_signed_long_int)
1854  dest+='l';
1855  else if(c_type==ID_unsigned_long_long_int)
1856  dest+="ull";
1857  else if(c_type==ID_signed_long_long_int)
1858  dest+="ll";
1859 
1860  if(src.find(ID_C_c_sizeof_type).is_not_nil() &&
1861  sizeof_nesting==0)
1862  {
1863  const auto sizeof_expr_opt =
1865 
1866  if(sizeof_expr_opt.has_value())
1867  {
1868  ++sizeof_nesting;
1869  dest = convert(sizeof_expr_opt.value()) + " /*" + dest + "*/ ";
1870  --sizeof_nesting;
1871  }
1872  }
1873  }
1874  }
1875  else if(type.id()==ID_floatbv)
1876  {
1878 
1879  if(!dest.empty() && isdigit(dest[dest.size() - 1]))
1880  {
1881  if(dest.find('.')==std::string::npos)
1882  dest+=".0";
1883 
1884  // ANSI-C: double is default; float/long-double require annotation
1885  if(src.type()==float_type())
1886  dest+='f';
1887  else if(src.type()==long_double_type() &&
1889  dest+='l';
1890  }
1891  else if(dest.size()==4 &&
1892  (dest[0]=='+' || dest[0]=='-'))
1893  {
1895  {
1896  if(dest == "+inf")
1897  dest = "+INFINITY";
1898  else if(dest == "-inf")
1899  dest = "-INFINITY";
1900  else if(dest == "+NaN")
1901  dest = "+NAN";
1902  else if(dest == "-NaN")
1903  dest = "-NAN";
1904  }
1905  else
1906  {
1907  // ANSI-C: double is default; float/long-double require annotation
1908  std::string suffix = "";
1909  if(src.type() == float_type())
1910  suffix = "f";
1911  else if(
1912  src.type() == long_double_type() &&
1914  {
1915  suffix = "l";
1916  }
1917 
1918  if(dest == "+inf")
1919  dest = "(1.0" + suffix + "/0.0" + suffix + ")";
1920  else if(dest == "-inf")
1921  dest = "(-1.0" + suffix + "/0.0" + suffix + ")";
1922  else if(dest == "+NaN")
1923  dest = "(0.0" + suffix + "/0.0" + suffix + ")";
1924  else if(dest == "-NaN")
1925  dest = "(-0.0" + suffix + "/0.0" + suffix + ")";
1926  }
1927  }
1928  }
1929  else if(type.id()==ID_fixedbv)
1930  {
1932 
1933  if(!dest.empty() && isdigit(dest[dest.size() - 1]))
1934  {
1935  if(src.type()==float_type())
1936  dest+='f';
1937  else if(src.type()==long_double_type())
1938  dest+='l';
1939  }
1940  }
1941  else if(type.id() == ID_array)
1942  {
1943  dest = convert_array(src);
1944  }
1945  else if(type.id()==ID_pointer)
1946  {
1947  if(
1948  value == ID_NULL ||
1949  (value == std::string(value.size(), '0') && config.ansi_c.NULL_is_zero))
1950  {
1952  dest = "NULL";
1953  else
1954  dest = "0";
1955  if(type.subtype().id()!=ID_empty)
1956  dest="(("+convert(type)+")"+dest+")";
1957  }
1958  else if(src.operands().size() == 1)
1959  {
1960  const auto &annotation = to_unary_expr(src).op();
1961 
1962  if(annotation.id() == ID_constant)
1963  {
1964  const irep_idt &op_value = to_constant_expr(annotation).get_value();
1965 
1966  if(op_value=="INVALID" ||
1967  has_prefix(id2string(op_value), "INVALID-") ||
1968  op_value=="NULL+offset")
1969  dest=id2string(op_value);
1970  else
1971  return convert_norep(src, precedence);
1972  }
1973  else
1974  return convert_with_precedence(annotation, precedence);
1975  }
1976  else
1977  {
1978  const auto width = to_pointer_type(type).get_width();
1979  mp_integer int_value = bvrep2integer(value, width, false);
1980  return "(" + convert(type) + ")" + integer2string(int_value);
1981  }
1982  }
1983  else if(type.id()==ID_string)
1984  {
1985  return '"'+id2string(src.get_value())+'"';
1986  }
1987  else
1988  return convert_norep(src, precedence);
1989 
1990  return dest;
1991 }
1992 
1997 std::string expr2ct::convert_constant_bool(bool boolean_value)
1998 {
1999  if(boolean_value)
2000  return configuration.true_string;
2001  else
2002  return configuration.false_string;
2003 }
2004 
2005 std::string expr2ct::convert_struct(
2006  const exprt &src,
2007  unsigned &precedence)
2008 {
2009  return convert_struct(
2011 }
2012 
2021 std::string expr2ct::convert_struct(
2022  const exprt &src,
2023  unsigned &precedence,
2024  bool include_padding_components)
2025 {
2026  const typet full_type=ns.follow(src.type());
2027 
2028  if(full_type.id()!=ID_struct)
2029  return convert_norep(src, precedence);
2030 
2031  const struct_typet &struct_type=
2032  to_struct_type(full_type);
2033 
2034  const struct_typet::componentst &components=
2035  struct_type.components();
2036 
2037  if(components.size()!=src.operands().size())
2038  return convert_norep(src, precedence);
2039 
2040  std::string dest="{ ";
2041 
2042  exprt::operandst::const_iterator o_it=src.operands().begin();
2043 
2044  bool first=true;
2045  bool newline=false;
2046  size_t last_size=0;
2047 
2048  for(const auto &component : struct_type.components())
2049  {
2050  if(o_it->type().id()==ID_code)
2051  continue;
2052 
2053  if(component.get_is_padding() && !include_padding_components)
2054  {
2055  ++o_it;
2056  continue;
2057  }
2058 
2059  if(first)
2060  first=false;
2061  else
2062  {
2063  dest+=',';
2064 
2065  if(newline)
2066  dest+="\n ";
2067  else
2068  dest+=' ';
2069  }
2070 
2071  std::string tmp=convert(*o_it);
2072 
2073  if(last_size+40<dest.size())
2074  {
2075  newline=true;
2076  last_size=dest.size();
2077  }
2078  else
2079  newline=false;
2080 
2081  dest+='.';
2082  dest+=component.get_string(ID_name);
2083  dest+='=';
2084  dest+=tmp;
2085 
2086  o_it++;
2087  }
2088 
2089  dest+=" }";
2090 
2091  return dest;
2092 }
2093 
2094 std::string expr2ct::convert_vector(
2095  const exprt &src,
2096  unsigned &precedence)
2097 {
2098  const typet &type = src.type();
2099 
2100  if(type.id() != ID_vector)
2101  return convert_norep(src, precedence);
2102 
2103  std::string dest="{ ";
2104 
2105  bool first=true;
2106  bool newline=false;
2107  size_t last_size=0;
2108 
2109  forall_operands(it, src)
2110  {
2111  if(first)
2112  first=false;
2113  else
2114  {
2115  dest+=',';
2116 
2117  if(newline)
2118  dest+="\n ";
2119  else
2120  dest+=' ';
2121  }
2122 
2123  std::string tmp=convert(*it);
2124 
2125  if(last_size+40<dest.size())
2126  {
2127  newline=true;
2128  last_size=dest.size();
2129  }
2130  else
2131  newline=false;
2132 
2133  dest+=tmp;
2134  }
2135 
2136  dest+=" }";
2137 
2138  return dest;
2139 }
2140 
2141 std::string expr2ct::convert_union(
2142  const exprt &src,
2143  unsigned &precedence)
2144 {
2145  std::string dest="{ ";
2146 
2147  if(src.operands().size()!=1)
2148  return convert_norep(src, precedence);
2149 
2150  dest+='.';
2151  dest+=src.get_string(ID_component_name);
2152  dest+='=';
2153  dest += convert(to_union_expr(src).op());
2154 
2155  dest+=" }";
2156 
2157  return dest;
2158 }
2159 
2160 std::string expr2ct::convert_array(const exprt &src)
2161 {
2162  std::string dest;
2163 
2164  // we treat arrays of characters as string constants,
2165  // and arrays of wchar_t as wide strings
2166 
2167  const typet &subtype = src.type().subtype();
2168 
2169  bool all_constant=true;
2170 
2171  forall_operands(it, src)
2172  if(!it->is_constant())
2173  all_constant=false;
2174 
2175  if(src.get_bool(ID_C_string_constant) &&
2176  all_constant &&
2177  (subtype==char_type() || subtype==wchar_t_type()))
2178  {
2179  bool wide=subtype==wchar_t_type();
2180 
2181  if(wide)
2182  dest+='L';
2183 
2184  dest+="\"";
2185 
2186  dest.reserve(dest.size()+1+src.operands().size());
2187 
2188  bool last_was_hex=false;
2189 
2190  forall_operands(it, src)
2191  {
2192  // these have a trailing zero
2193  if(it==--src.operands().end())
2194  break;
2195 
2196  const unsigned int ch = numeric_cast_v<unsigned>(to_constant_expr(*it));
2197 
2198  if(last_was_hex)
2199  {
2200  // we use "string splicing" to avoid ambiguity
2201  if(isxdigit(ch))
2202  dest+="\" \"";
2203 
2204  last_was_hex=false;
2205  }
2206 
2207  switch(ch)
2208  {
2209  case '\n': dest+="\\n"; break; /* NL (0x0a) */
2210  case '\t': dest+="\\t"; break; /* HT (0x09) */
2211  case '\v': dest+="\\v"; break; /* VT (0x0b) */
2212  case '\b': dest+="\\b"; break; /* BS (0x08) */
2213  case '\r': dest+="\\r"; break; /* CR (0x0d) */
2214  case '\f': dest+="\\f"; break; /* FF (0x0c) */
2215  case '\a': dest+="\\a"; break; /* BEL (0x07) */
2216  case '\\': dest+="\\\\"; break;
2217  case '"': dest+="\\\""; break;
2218 
2219  default:
2220  if(ch>=' ' && ch!=127 && ch<0xff)
2221  dest+=static_cast<char>(ch);
2222  else
2223  {
2224  std::ostringstream oss;
2225  oss << "\\x" << std::hex << ch;
2226  dest += oss.str();
2227  last_was_hex=true;
2228  }
2229  }
2230  }
2231 
2232  dest+="\"";
2233 
2234  return dest;
2235  }
2236 
2237  dest="{ ";
2238 
2239  forall_operands(it, src)
2240  {
2241  std::string tmp;
2242 
2243  if(it->is_not_nil())
2244  tmp=convert(*it);
2245 
2246  if((it+1)!=src.operands().end())
2247  {
2248  tmp+=", ";
2249  if(tmp.size()>40)
2250  tmp+="\n ";
2251  }
2252 
2253  dest+=tmp;
2254  }
2255 
2256  dest+=" }";
2257 
2258  return dest;
2259 }
2260 
2261 std::string expr2ct::convert_array_list(
2262  const exprt &src,
2263  unsigned &precedence)
2264 {
2265  std::string dest="{ ";
2266 
2267  if((src.operands().size()%2)!=0)
2268  return convert_norep(src, precedence);
2269 
2270  forall_operands(it, src)
2271  {
2272  std::string tmp1=convert(*it);
2273 
2274  it++;
2275 
2276  std::string tmp2=convert(*it);
2277 
2278  std::string tmp="["+tmp1+"]="+tmp2;
2279 
2280  if((it+1)!=src.operands().end())
2281  {
2282  tmp+=", ";
2283  if(tmp.size()>40)
2284  tmp+="\n ";
2285  }
2286 
2287  dest+=tmp;
2288  }
2289 
2290  dest+=" }";
2291 
2292  return dest;
2293 }
2294 
2295 std::string expr2ct::convert_initializer_list(const exprt &src)
2296 {
2297  std::string dest;
2298  if(src.id()!=ID_compound_literal)
2299  dest+="{ ";
2300 
2301  forall_operands(it, src)
2302  {
2303  std::string tmp=convert(*it);
2304 
2305  if((it+1)!=src.operands().end())
2306  {
2307  tmp+=", ";
2308  if(tmp.size()>40)
2309  tmp+="\n ";
2310  }
2311 
2312  dest+=tmp;
2313  }
2314 
2315  if(src.id()!=ID_compound_literal)
2316  dest+=" }";
2317 
2318  return dest;
2319 }
2320 
2321 std::string expr2ct::convert_rox(const shift_exprt &src, unsigned precedence)
2322 {
2323  // AAAA rox n == (AAAA lhs_op n % width(AAAA))
2324  // | (AAAA rhs_op (width(AAAA) - n % width(AAAA)))
2325  // Where lhs_op and rhs_op depend on whether it is rol or ror
2326  // Get AAAA and if it's signed wrap it in a cast to remove
2327  // the sign since this messes with C shifts
2328  exprt op0 = src.op();
2329  size_t type_width;
2331  {
2332  // Set the type width
2333  type_width = to_signedbv_type(op0.type()).get_width();
2334  // Shifts in C are arithmetic and care about sign, by forcing
2335  // a cast to unsigned we force the shifts to perform rol/r
2336  op0 = typecast_exprt(op0, unsignedbv_typet(type_width));
2337  }
2338  else if(can_cast_type<unsignedbv_typet>(op0.type()))
2339  {
2340  // Set the type width
2341  type_width = to_unsignedbv_type(op0.type()).get_width();
2342  }
2343  else
2344  {
2345  UNREACHABLE;
2346  }
2347  // Construct the "width(AAAA)" constant
2348  const exprt width_expr = from_integer(type_width, src.distance().type());
2349  // Apply modulo to n since shifting will overflow
2350  // That is: 0001 << 4 == 0, but 0001 rol 4 == 0001
2351  const exprt distance_modulo_width = mod_exprt(src.distance(), width_expr);
2352  // Now put the pieces together
2353  // width(AAAA) - (n % width(AAAA))
2354  const auto complement_width_expr =
2355  minus_exprt(width_expr, distance_modulo_width);
2356  // lhs and rhs components defined according to rol/ror
2357  exprt lhs_expr;
2358  exprt rhs_expr;
2359  if(src.id() == ID_rol)
2360  {
2361  // AAAA << (n % width(AAAA))
2362  lhs_expr = shl_exprt(op0, distance_modulo_width);
2363  // AAAA >> complement_width_expr
2364  rhs_expr = ashr_exprt(op0, complement_width_expr);
2365  }
2366  else if(src.id() == ID_ror)
2367  {
2368  // AAAA >> (n % width(AAAA))
2369  lhs_expr = ashr_exprt(op0, distance_modulo_width);
2370  // AAAA << complement_width_expr
2371  rhs_expr = shl_exprt(op0, complement_width_expr);
2372  }
2373  else
2374  {
2375  // Someone called this function when they shouldn't have.
2376  UNREACHABLE;
2377  }
2378  return convert_with_precedence(bitor_exprt(lhs_expr, rhs_expr), precedence);
2379 }
2380 
2381 std::string expr2ct::convert_designated_initializer(const exprt &src)
2382 {
2383  if(src.operands().size()!=1)
2384  {
2385  unsigned precedence;
2386  return convert_norep(src, precedence);
2387  }
2388 
2389  const exprt &value = to_unary_expr(src).op();
2390 
2391  const exprt &designator = static_cast<const exprt &>(src.find(ID_designator));
2392  if(designator.operands().size() != 1)
2393  {
2394  unsigned precedence;
2395  return convert_norep(src, precedence);
2396  }
2397 
2398  const exprt &designator_id = to_unary_expr(designator).op();
2399 
2400  std::string dest;
2401 
2402  if(designator_id.id() == ID_member)
2403  {
2404  dest = "." + id2string(designator_id.get(ID_component_name));
2405  }
2406  else if(
2407  designator_id.id() == ID_index && designator_id.operands().size() == 1)
2408  {
2409  dest = "[" + convert(to_unary_expr(designator_id).op()) + "]";
2410  }
2411  else
2412  {
2413  unsigned precedence;
2414  return convert_norep(src, precedence);
2415  }
2416 
2417  dest+='=';
2418  dest += convert(value);
2419 
2420  return dest;
2421 }
2422 
2423 std::string
2425 {
2426  std::string dest;
2427 
2428  {
2429  unsigned p;
2430  std::string function_str=convert_with_precedence(src.function(), p);
2431  dest+=function_str;
2432  }
2433 
2434  dest+='(';
2435 
2436  forall_expr(it, src.arguments())
2437  {
2438  unsigned p;
2439  std::string arg_str=convert_with_precedence(*it, p);
2440 
2441  if(it!=src.arguments().begin())
2442  dest+=", ";
2443  // TODO: ggf. Klammern je nach p
2444  dest+=arg_str;
2445  }
2446 
2447  dest+=')';
2448 
2449  return dest;
2450 }
2451 
2454 {
2455  std::string dest;
2456 
2457  {
2458  unsigned p;
2459  std::string function_str=convert_with_precedence(src.function(), p);
2460  dest+=function_str;
2461  }
2462 
2463  dest+='(';
2464 
2465  forall_expr(it, src.arguments())
2466  {
2467  unsigned p;
2468  std::string arg_str=convert_with_precedence(*it, p);
2469 
2470  if(it!=src.arguments().begin())
2471  dest+=", ";
2472  // TODO: ggf. Klammern je nach p
2473  dest+=arg_str;
2474  }
2475 
2476  dest+=')';
2477 
2478  return dest;
2479 }
2480 
2481 std::string expr2ct::convert_overflow(
2482  const exprt &src,
2483  unsigned &precedence)
2484 {
2485  precedence=16;
2486 
2487  std::string dest="overflow(\"";
2488  dest+=src.id().c_str()+9;
2489  dest+="\"";
2490 
2491  if(!src.operands().empty())
2492  {
2493  dest+=", ";
2494  dest += convert(to_multi_ary_expr(src).op0().type());
2495  }
2496 
2497  forall_operands(it, src)
2498  {
2499  unsigned p;
2500  std::string arg_str=convert_with_precedence(*it, p);
2501 
2502  dest+=", ";
2503  // TODO: ggf. Klammern je nach p
2504  dest+=arg_str;
2505  }
2506 
2507  dest+=')';
2508 
2509  return dest;
2510 }
2511 
2512 std::string expr2ct::indent_str(unsigned indent)
2513 {
2514  return std::string(indent, ' ');
2515 }
2516 
2517 std::string expr2ct::convert_code_asm(
2518  const code_asmt &src,
2519  unsigned indent)
2520 {
2521  std::string dest=indent_str(indent);
2522 
2523  if(src.get_flavor()==ID_gcc)
2524  {
2525  if(src.operands().size()==5)
2526  {
2527  dest+="asm(";
2528  dest+=convert(src.op0());
2529  if(!src.operands()[1].operands().empty() ||
2530  !src.operands()[2].operands().empty() ||
2531  !src.operands()[3].operands().empty() ||
2532  !src.operands()[4].operands().empty())
2533  {
2534  // need extended syntax
2535 
2536  // outputs
2537  dest+=" : ";
2538  forall_operands(it, src.op1())
2539  {
2540  if(it->operands().size()==2)
2541  {
2542  if(it!=src.op1().operands().begin())
2543  dest+=", ";
2544  dest += convert(to_binary_expr(*it).op0());
2545  dest+="(";
2546  dest += convert(to_binary_expr(*it).op1());
2547  dest+=")";
2548  }
2549  }
2550 
2551  // inputs
2552  dest+=" : ";
2553  forall_operands(it, src.op2())
2554  {
2555  if(it->operands().size()==2)
2556  {
2557  if(it!=src.op2().operands().begin())
2558  dest+=", ";
2559  dest += convert(to_binary_expr(*it).op0());
2560  dest+="(";
2561  dest += convert(to_binary_expr(*it).op1());
2562  dest+=")";
2563  }
2564  }
2565 
2566  // clobbered registers
2567  dest+=" : ";
2568  forall_operands(it, src.op3())
2569  {
2570  if(it!=src.op3().operands().begin())
2571  dest+=", ";
2572  if(it->id()==ID_gcc_asm_clobbered_register)
2573  dest += convert(to_unary_expr(*it).op());
2574  else
2575  dest+=convert(*it);
2576  }
2577  }
2578  dest+=");";
2579  }
2580  }
2581  else if(src.get_flavor()==ID_msc)
2582  {
2583  if(src.operands().size()==1)
2584  {
2585  dest+="__asm {\n";
2586  dest+=indent_str(indent);
2587  dest+=convert(src.op0());
2588  dest+="\n}";
2589  }
2590  }
2591 
2592  return dest;
2593 }
2594 
2595 std::string expr2ct::convert_code_while(
2596  const code_whilet &src,
2597  unsigned indent)
2598 {
2599  if(src.operands().size()!=2)
2600  {
2601  unsigned precedence;
2602  return convert_norep(src, precedence);
2603  }
2604 
2605  std::string dest=indent_str(indent);
2606  dest+="while("+convert(src.cond());
2607 
2608  if(src.body().is_nil())
2609  dest+=");";
2610  else
2611  {
2612  dest+=")\n";
2613  dest+=convert_code(
2614  src.body(),
2615  src.body().get_statement()==ID_block ? indent : indent+2);
2616  }
2617 
2618  return dest;
2619 }
2620 
2621 std::string expr2ct::convert_code_dowhile(
2622  const code_dowhilet &src,
2623  unsigned indent)
2624 {
2625  if(src.operands().size()!=2)
2626  {
2627  unsigned precedence;
2628  return convert_norep(src, precedence);
2629  }
2630 
2631  std::string dest=indent_str(indent);
2632 
2633  if(src.body().is_nil())
2634  dest+="do;";
2635  else
2636  {
2637  dest+="do\n";
2638  dest+=convert_code(
2639  src.body(),
2640  src.body().get_statement()==ID_block ? indent : indent+2);
2641  dest+="\n";
2642  dest+=indent_str(indent);
2643  }
2644 
2645  dest+="while("+convert(src.cond())+");";
2646 
2647  return dest;
2648 }
2649 
2651  const code_ifthenelset &src,
2652  unsigned indent)
2653 {
2654  if(src.operands().size()!=3)
2655  {
2656  unsigned precedence;
2657  return convert_norep(src, precedence);
2658  }
2659 
2660  std::string dest=indent_str(indent);
2661  dest+="if("+convert(src.cond())+")\n";
2662 
2663  if(src.then_case().is_nil())
2664  {
2665  dest+=indent_str(indent+2);
2666  dest+=';';
2667  }
2668  else
2669  dest += convert_code(
2670  src.then_case(),
2671  src.then_case().get_statement() == ID_block ? indent : indent + 2);
2672  dest+="\n";
2673 
2674  if(!src.else_case().is_nil())
2675  {
2676  dest+="\n";
2677  dest+=indent_str(indent);
2678  dest+="else\n";
2679  dest += convert_code(
2680  src.else_case(),
2681  src.else_case().get_statement() == ID_block ? indent : indent + 2);
2682  }
2683 
2684  return dest;
2685 }
2686 
2687 std::string expr2ct::convert_code_return(
2688  const codet &src,
2689  unsigned indent)
2690 {
2691  if(src.operands().size() != 1)
2692  {
2693  unsigned precedence;
2694  return convert_norep(src, precedence);
2695  }
2696 
2697  std::string dest=indent_str(indent);
2698  dest+="return";
2699 
2700  if(to_code_return(src).has_return_value())
2701  dest+=" "+convert(src.op0());
2702 
2703  dest+=';';
2704 
2705  return dest;
2706 }
2707 
2708 std::string expr2ct::convert_code_goto(
2709  const codet &src,
2710  unsigned indent)
2711 {
2712  std:: string dest=indent_str(indent);
2713  dest+="goto ";
2714  dest+=clean_identifier(src.get(ID_destination));
2715  dest+=';';
2716 
2717  return dest;
2718 }
2719 
2720 std::string expr2ct::convert_code_break(unsigned indent)
2721 {
2722  std::string dest=indent_str(indent);
2723  dest+="break";
2724  dest+=';';
2725 
2726  return dest;
2727 }
2728 
2729 std::string expr2ct::convert_code_switch(
2730  const codet &src,
2731  unsigned indent)
2732 {
2733  if(src.operands().empty())
2734  {
2735  unsigned precedence;
2736  return convert_norep(src, precedence);
2737  }
2738 
2739  std::string dest=indent_str(indent);
2740  dest+="switch(";
2741  dest+=convert(src.op0());
2742  dest+=")\n";
2743 
2744  dest+=indent_str(indent);
2745  dest+='{';
2746 
2747  forall_operands(it, src)
2748  {
2749  if(it==src.operands().begin())
2750  continue;
2751  const exprt &op=*it;
2752 
2753  if(op.get(ID_statement)!=ID_block)
2754  {
2755  unsigned precedence;
2756  dest+=convert_norep(op, precedence);
2757  }
2758  else
2759  {
2760  forall_operands(it2, op)
2761  dest+=convert_code(to_code(*it2), indent+2);
2762  }
2763  }
2764 
2765  dest+="\n";
2766  dest+=indent_str(indent);
2767  dest+='}';
2768 
2769  return dest;
2770 }
2771 
2772 std::string expr2ct::convert_code_continue(unsigned indent)
2773 {
2774  std::string dest=indent_str(indent);
2775  dest+="continue";
2776  dest+=';';
2777 
2778  return dest;
2779 }
2780 
2781 std::string expr2ct::convert_code_decl(
2782  const codet &src,
2783  unsigned indent)
2784 {
2785  // initializer to go away
2786  if(src.operands().size()!=1 &&
2787  src.operands().size()!=2)
2788  {
2789  unsigned precedence;
2790  return convert_norep(src, precedence);
2791  }
2792 
2793  std::string declarator=convert(src.op0());
2794 
2795  std::string dest=indent_str(indent);
2796 
2797  const symbolt *symbol=nullptr;
2798  if(!ns.lookup(to_symbol_expr(src.op0()).get_identifier(), symbol))
2799  {
2800  if(symbol->is_file_local &&
2801  (src.op0().type().id()==ID_code || symbol->is_static_lifetime))
2802  dest+="static ";
2803  else if(symbol->is_extern)
2804  dest+="extern ";
2805  else if(
2807  {
2808  dest += "__declspec(dllexport) ";
2809  }
2810 
2811  if(symbol->type.id()==ID_code &&
2812  to_code_type(symbol->type).get_inlined())
2813  dest+="inline ";
2814  }
2815 
2816  dest+=convert_rec(src.op0().type(), c_qualifierst(), declarator);
2817 
2818  if(src.operands().size()==2)
2819  dest+="="+convert(src.op1());
2820 
2821  dest+=';';
2822 
2823  return dest;
2824 }
2825 
2826 std::string expr2ct::convert_code_dead(
2827  const codet &src,
2828  unsigned indent)
2829 {
2830  // initializer to go away
2831  if(src.operands().size()!=1)
2832  {
2833  unsigned precedence;
2834  return convert_norep(src, precedence);
2835  }
2836 
2837  return indent_str(indent) + "dead " + convert(src.op0()) + ";";
2838 }
2839 
2840 std::string expr2ct::convert_code_for(
2841  const code_fort &src,
2842  unsigned indent)
2843 {
2844  if(src.operands().size()!=4)
2845  {
2846  unsigned precedence;
2847  return convert_norep(src, precedence);
2848  }
2849 
2850  std::string dest=indent_str(indent);
2851  dest+="for(";
2852 
2853  if(!src.init().is_nil())
2854  dest += convert(src.init());
2855  else
2856  dest+=' ';
2857  dest+="; ";
2858  if(!src.cond().is_nil())
2859  dest += convert(src.cond());
2860  dest+="; ";
2861  if(!src.iter().is_nil())
2862  dest += convert(src.iter());
2863 
2864  if(src.body().is_nil())
2865  dest+=");\n";
2866  else
2867  {
2868  dest+=")\n";
2869  dest+=convert_code(
2870  src.body(),
2871  src.body().get_statement()==ID_block ? indent : indent+2);
2872  }
2873 
2874  return dest;
2875 }
2876 
2877 std::string expr2ct::convert_code_block(
2878  const code_blockt &src,
2879  unsigned indent)
2880 {
2881  std::string dest=indent_str(indent);
2882  dest+="{\n";
2883 
2884  for(const auto &statement : src.statements())
2885  {
2886  if(statement.get_statement() == ID_label)
2887  dest += convert_code(statement, indent);
2888  else
2889  dest += convert_code(statement, indent + 2);
2890 
2891  dest+="\n";
2892  }
2893 
2894  dest+=indent_str(indent);
2895  dest+='}';
2896 
2897  return dest;
2898 }
2899 
2901  const codet &src,
2902  unsigned indent)
2903 {
2904  std::string dest;
2905 
2906  forall_operands(it, src)
2907  {
2908  dest+=convert_code(to_code(*it), indent);
2909  dest+="\n";
2910  }
2911 
2912  return dest;
2913 }
2914 
2916  const codet &src,
2917  unsigned indent)
2918 {
2919  std::string dest=indent_str(indent);
2920 
2921  std::string expr_str;
2922  if(src.operands().size()==1)
2923  expr_str=convert(src.op0());
2924  else
2925  {
2926  unsigned precedence;
2927  expr_str=convert_norep(src, precedence);
2928  }
2929 
2930  dest+=expr_str;
2931  if(dest.empty() || *dest.rbegin()!=';')
2932  dest+=';';
2933 
2934  return dest;
2935 }
2936 
2937 std::string expr2ct::convert_code(
2938  const codet &src,
2939  unsigned indent)
2940 {
2941  static bool comment_done=false;
2942 
2943  if(
2944  !comment_done && (!src.source_location().get_comment().empty() ||
2945  !src.source_location().get_pragmas().empty()))
2946  {
2947  comment_done=true;
2948  std::string dest;
2949  if(!src.source_location().get_comment().empty())
2950  {
2951  dest += indent_str(indent);
2952  dest += "/* " + id2string(src.source_location().get_comment()) + " */\n";
2953  }
2954  if(!src.source_location().get_pragmas().empty())
2955  {
2956  std::ostringstream oss;
2957  oss << indent_str(indent) << "/* ";
2958  const auto &pragmas = src.source_location().get_pragmas();
2959  join_strings(
2960  oss,
2961  pragmas.begin(),
2962  pragmas.end(),
2963  ',',
2964  [](const std::pair<irep_idt, irept> &p) { return p.first; });
2965  oss << " */\n";
2966  dest += oss.str();
2967  }
2968  dest+=convert_code(src, indent);
2969  comment_done=false;
2970  return dest;
2971  }
2972 
2973  const irep_idt &statement=src.get_statement();
2974 
2975  if(statement==ID_expression)
2976  return convert_code_expression(src, indent);
2977 
2978  if(statement==ID_block)
2979  return convert_code_block(to_code_block(src), indent);
2980 
2981  if(statement==ID_switch)
2982  return convert_code_switch(src, indent);
2983 
2984  if(statement==ID_for)
2985  return convert_code_for(to_code_for(src), indent);
2986 
2987  if(statement==ID_while)
2988  return convert_code_while(to_code_while(src), indent);
2989 
2990  if(statement==ID_asm)
2991  return convert_code_asm(to_code_asm(src), indent);
2992 
2993  if(statement==ID_skip)
2994  return indent_str(indent)+";";
2995 
2996  if(statement==ID_dowhile)
2997  return convert_code_dowhile(to_code_dowhile(src), indent);
2998 
2999  if(statement==ID_ifthenelse)
3000  return convert_code_ifthenelse(to_code_ifthenelse(src), indent);
3001 
3002  if(statement==ID_return)
3003  return convert_code_return(src, indent);
3004 
3005  if(statement==ID_goto)
3006  return convert_code_goto(src, indent);
3007 
3008  if(statement==ID_printf)
3009  return convert_code_printf(src, indent);
3010 
3011  if(statement==ID_fence)
3012  return convert_code_fence(src, indent);
3013 
3015  return convert_code_input(src, indent);
3016 
3018  return convert_code_output(src, indent);
3019 
3020  if(statement==ID_assume)
3021  return convert_code_assume(src, indent);
3022 
3023  if(statement==ID_assert)
3024  return convert_code_assert(src, indent);
3025 
3026  if(statement==ID_break)
3027  return convert_code_break(indent);
3028 
3029  if(statement==ID_continue)
3030  return convert_code_continue(indent);
3031 
3032  if(statement==ID_decl)
3033  return convert_code_decl(src, indent);
3034 
3035  if(statement==ID_decl_block)
3036  return convert_code_decl_block(src, indent);
3037 
3038  if(statement==ID_dead)
3039  return convert_code_dead(src, indent);
3040 
3041  if(statement==ID_assign)
3042  return convert_code_assign(to_code_assign(src), indent);
3043 
3044  if(statement=="lock")
3045  return convert_code_lock(src, indent);
3046 
3047  if(statement=="unlock")
3048  return convert_code_unlock(src, indent);
3049 
3050  if(statement==ID_atomic_begin)
3051  return indent_str(indent) + CPROVER_PREFIX + "atomic_begin();";
3052 
3053  if(statement==ID_atomic_end)
3054  return indent_str(indent) + CPROVER_PREFIX + "atomic_end();";
3055 
3056  if(statement==ID_function_call)
3058 
3059  if(statement==ID_label)
3060  return convert_code_label(to_code_label(src), indent);
3061 
3062  if(statement==ID_switch_case)
3063  return convert_code_switch_case(to_code_switch_case(src), indent);
3064 
3065  if(statement==ID_array_set)
3066  return convert_code_array_set(src, indent);
3067 
3068  if(statement==ID_array_copy)
3069  return convert_code_array_copy(src, indent);
3070 
3071  if(statement==ID_array_replace)
3072  return convert_code_array_replace(src, indent);
3073 
3074  if(statement == ID_set_may || statement == ID_set_must)
3075  return indent_str(indent) + convert_function(src, id2string(statement)) +
3076  ";";
3077 
3078  unsigned precedence;
3079  return convert_norep(src, precedence);
3080 }
3081 
3082 std::string expr2ct::convert_code_assign(
3083  const code_assignt &src,
3084  unsigned indent)
3085 {
3086  return indent_str(indent) +
3087  convert_binary(to_binary_expr(src), "=", 2, true) + ";";
3088 }
3089 
3090 std::string expr2ct::convert_code_lock(
3091  const codet &src,
3092  unsigned indent)
3093 {
3094  if(src.operands().size()!=1)
3095  {
3096  unsigned precedence;
3097  return convert_norep(src, precedence);
3098  }
3099 
3100  return indent_str(indent)+"LOCK("+convert(src.op0())+");";
3101 }
3102 
3103 std::string expr2ct::convert_code_unlock(
3104  const codet &src,
3105  unsigned indent)
3106 {
3107  if(src.operands().size()!=1)
3108  {
3109  unsigned precedence;
3110  return convert_norep(src, precedence);
3111  }
3112 
3113  return indent_str(indent)+"UNLOCK("+convert(src.op0())+");";
3114 }
3115 
3117  const code_function_callt &src,
3118  unsigned indent)
3119 {
3120  if(src.operands().size()!=3)
3121  {
3122  unsigned precedence;
3123  return convert_norep(src, precedence);
3124  }
3125 
3126  std::string dest=indent_str(indent);
3127 
3128  if(src.lhs().is_not_nil())
3129  {
3130  unsigned p;
3131  std::string lhs_str=convert_with_precedence(src.lhs(), p);
3132 
3133  // TODO: ggf. Klammern je nach p
3134  dest+=lhs_str;
3135  dest+='=';
3136  }
3137 
3138  {
3139  unsigned p;
3140  std::string function_str=convert_with_precedence(src.function(), p);
3141  dest+=function_str;
3142  }
3143 
3144  dest+='(';
3145 
3146  const exprt::operandst &arguments=src.arguments();
3147 
3148  forall_expr(it, arguments)
3149  {
3150  unsigned p;
3151  std::string arg_str=convert_with_precedence(*it, p);
3152 
3153  if(it!=arguments.begin())
3154  dest+=", ";
3155  // TODO: ggf. Klammern je nach p
3156  dest+=arg_str;
3157  }
3158 
3159  dest+=");";
3160 
3161  return dest;
3162 }
3163 
3164 std::string expr2ct::convert_code_printf(
3165  const codet &src,
3166  unsigned indent)
3167 {
3168  std::string dest=indent_str(indent)+"printf(";
3169 
3170  forall_operands(it, src)
3171  {
3172  unsigned p;
3173  std::string arg_str=convert_with_precedence(*it, p);
3174 
3175  if(it!=src.operands().begin())
3176  dest+=", ";
3177  // TODO: ggf. Klammern je nach p
3178  dest+=arg_str;
3179  }
3180 
3181  dest+=");";
3182 
3183  return dest;
3184 }
3185 
3186 std::string expr2ct::convert_code_fence(
3187  const codet &src,
3188  unsigned indent)
3189 {
3190  std::string dest=indent_str(indent)+"FENCE(";
3191 
3192  irep_idt att[]=
3193  { ID_WRfence, ID_RRfence, ID_RWfence, ID_WWfence,
3194  ID_RRcumul, ID_RWcumul, ID_WWcumul, ID_WRcumul,
3195  irep_idt() };
3196 
3197  bool first=true;
3198 
3199  for(unsigned i=0; !att[i].empty(); i++)
3200  {
3201  if(src.get_bool(att[i]))
3202  {
3203  if(first)
3204  first=false;
3205  else
3206  dest+='+';
3207 
3208  dest+=id2string(att[i]);
3209  }
3210  }
3211 
3212  dest+=");";
3213  return dest;
3214 }
3215 
3216 std::string expr2ct::convert_code_input(
3217  const codet &src,
3218  unsigned indent)
3219 {
3220  std::string dest=indent_str(indent)+"INPUT(";
3221 
3222  forall_operands(it, src)
3223  {
3224  unsigned p;
3225  std::string arg_str=convert_with_precedence(*it, p);
3226 
3227  if(it!=src.operands().begin())
3228  dest+=", ";
3229  // TODO: ggf. Klammern je nach p
3230  dest+=arg_str;
3231  }
3232 
3233  dest+=");";
3234 
3235  return dest;
3236 }
3237 
3238 std::string expr2ct::convert_code_output(
3239  const codet &src,
3240  unsigned indent)
3241 {
3242  std::string dest=indent_str(indent)+"OUTPUT(";
3243 
3244  forall_operands(it, src)
3245  {
3246  unsigned p;
3247  std::string arg_str=convert_with_precedence(*it, p);
3248 
3249  if(it!=src.operands().begin())
3250  dest+=", ";
3251  dest+=arg_str;
3252  }
3253 
3254  dest+=");";
3255 
3256  return dest;
3257 }
3258 
3260  const codet &src,
3261  unsigned indent)
3262 {
3263  std::string dest=indent_str(indent)+"ARRAY_SET(";
3264 
3265  forall_operands(it, src)
3266  {
3267  unsigned p;
3268  std::string arg_str=convert_with_precedence(*it, p);
3269 
3270  if(it!=src.operands().begin())
3271  dest+=", ";
3272  // TODO: ggf. Klammern je nach p
3273  dest+=arg_str;
3274  }
3275 
3276  dest+=");";
3277 
3278  return dest;
3279 }
3280 
3282  const codet &src,
3283  unsigned indent)
3284 {
3285  std::string dest=indent_str(indent)+"ARRAY_COPY(";
3286 
3287  forall_operands(it, src)
3288  {
3289  unsigned p;
3290  std::string arg_str=convert_with_precedence(*it, p);
3291 
3292  if(it!=src.operands().begin())
3293  dest+=", ";
3294  // TODO: ggf. Klammern je nach p
3295  dest+=arg_str;
3296  }
3297 
3298  dest+=");";
3299 
3300  return dest;
3301 }
3302 
3304  const codet &src,
3305  unsigned indent)
3306 {
3307  std::string dest=indent_str(indent)+"ARRAY_REPLACE(";
3308 
3309  forall_operands(it, src)
3310  {
3311  unsigned p;
3312  std::string arg_str=convert_with_precedence(*it, p);
3313 
3314  if(it!=src.operands().begin())
3315  dest+=", ";
3316  dest+=arg_str;
3317  }
3318 
3319  dest+=");";
3320 
3321  return dest;
3322 }
3323 
3324 std::string expr2ct::convert_code_assert(
3325  const codet &src,
3326  unsigned indent)
3327 {
3328  if(src.operands().size()!=1)
3329  {
3330  unsigned precedence;
3331  return convert_norep(src, precedence);
3332  }
3333 
3334  return indent_str(indent)+"assert("+convert(src.op0())+");";
3335 }
3336 
3337 std::string expr2ct::convert_code_assume(
3338  const codet &src,
3339  unsigned indent)
3340 {
3341  if(src.operands().size()!=1)
3342  {
3343  unsigned precedence;
3344  return convert_norep(src, precedence);
3345  }
3346 
3347  return indent_str(indent) + CPROVER_PREFIX + "assume(" + convert(src.op0()) +
3348  ");";
3349 }
3350 
3351 std::string expr2ct::convert_code_label(
3352  const code_labelt &src,
3353  unsigned indent)
3354 {
3355  std::string labels_string;
3356 
3357  irep_idt label=src.get_label();
3358 
3359  labels_string+="\n";
3360  labels_string+=indent_str(indent);
3361  labels_string+=clean_identifier(label);
3362  labels_string+=":\n";
3363 
3364  std::string tmp=convert_code(src.code(), indent+2);
3365 
3366  return labels_string+tmp;
3367 }
3368 
3370  const code_switch_caset &src,
3371  unsigned indent)
3372 {
3373  std::string labels_string;
3374 
3375  if(src.is_default())
3376  {
3377  labels_string+="\n";
3378  labels_string+=indent_str(indent);
3379  labels_string+="default:\n";
3380  }
3381  else
3382  {
3383  labels_string+="\n";
3384  labels_string+=indent_str(indent);
3385  labels_string+="case ";
3386  labels_string+=convert(src.case_op());
3387  labels_string+=":\n";
3388  }
3389 
3390  unsigned next_indent=indent;
3391  if(src.code().get_statement()!=ID_block &&
3392  src.code().get_statement()!=ID_switch_case)
3393  next_indent+=2;
3394  std::string tmp=convert_code(src.code(), next_indent);
3395 
3396  return labels_string+tmp;
3397 }
3398 
3399 std::string expr2ct::convert_code(const codet &src)
3400 {
3401  return convert_code(src, 0);
3402 }
3403 
3404 std::string expr2ct::convert_Hoare(const exprt &src)
3405 {
3406  unsigned precedence;
3407 
3408  if(src.operands().size()!=2)
3409  return convert_norep(src, precedence);
3410 
3411  const exprt &assumption = to_binary_expr(src).op0();
3412  const exprt &assertion = to_binary_expr(src).op1();
3413  const codet &code=
3414  static_cast<const codet &>(src.find(ID_code));
3415 
3416  std::string dest="\n";
3417  dest+='{';
3418 
3419  if(!assumption.is_nil())
3420  {
3421  std::string assumption_str=convert(assumption);
3422  dest+=" assume(";
3423  dest+=assumption_str;
3424  dest+=");\n";
3425  }
3426  else
3427  dest+="\n";
3428 
3429  {
3430  std::string code_str=convert_code(code);
3431  dest+=code_str;
3432  }
3433 
3434  if(!assertion.is_nil())
3435  {
3436  std::string assertion_str=convert(assertion);
3437  dest+=" assert(";
3438  dest+=assertion_str;
3439  dest+=");\n";
3440  }
3441 
3442  dest+='}';
3443 
3444  return dest;
3445 }
3446 
3447 std::string
3448 expr2ct::convert_extractbit(const extractbit_exprt &src, unsigned precedence)
3449 {
3450  std::string dest = convert_with_precedence(src.src(), precedence);
3451  dest+='[';
3452  dest += convert_with_precedence(src.index(), precedence);
3453  dest+=']';
3454 
3455  return dest;
3456 }
3457 
3458 std::string
3459 expr2ct::convert_extractbits(const extractbits_exprt &src, unsigned precedence)
3460 {
3461  std::string dest = convert_with_precedence(src.src(), precedence);
3462  dest+='[';
3463  dest += convert_with_precedence(src.upper(), precedence);
3464  dest+=", ";
3465  dest += convert_with_precedence(src.lower(), precedence);
3466  dest+=']';
3467 
3468  return dest;
3469 }
3470 
3471 std::string expr2ct::convert_sizeof(
3472  const exprt &src,
3473  unsigned &precedence)
3474 {
3475  if(src.has_operands())
3476  return convert_norep(src, precedence);
3477 
3478  std::string dest="sizeof(";
3479  dest+=convert(static_cast<const typet&>(src.find(ID_type_arg)));
3480  dest+=')';
3481 
3482  return dest;
3483 }
3484 
3486  const exprt &src,
3487  unsigned &precedence)
3488 {
3489  precedence=16;
3490 
3491  if(src.id()==ID_plus)
3492  return convert_multi_ary(src, "+", precedence=12, false);
3493 
3494  else if(src.id()==ID_minus)
3495  return convert_binary(to_binary_expr(src), "-", precedence = 12, true);
3496 
3497  else if(src.id()==ID_unary_minus)
3498  return convert_unary(to_unary_expr(src), "-", precedence = 15);
3499 
3500  else if(src.id()==ID_unary_plus)
3501  return convert_unary(to_unary_expr(src), "+", precedence = 15);
3502 
3503  else if(src.id()==ID_floatbv_typecast)
3504  {
3505  const auto &floatbv_typecast = to_floatbv_typecast_expr(src);
3506 
3507  std::string dest="FLOAT_TYPECAST(";
3508 
3509  unsigned p0;
3510  std::string tmp0 = convert_with_precedence(floatbv_typecast.op(), p0);
3511 
3512  if(p0<=1)
3513  dest+='(';
3514  dest+=tmp0;
3515  if(p0<=1)
3516  dest+=')';
3517 
3518  dest+=", ";
3519  dest += convert(src.type());
3520  dest+=", ";
3521 
3522  unsigned p1;
3523  std::string tmp1 =
3524  convert_with_precedence(floatbv_typecast.rounding_mode(), p1);
3525 
3526  if(p1<=1)
3527  dest+='(';
3528  dest+=tmp1;
3529  if(p1<=1)
3530  dest+=')';
3531 
3532  dest+=')';
3533  return dest;
3534  }
3535 
3536  else if(src.id()==ID_sign)
3537  {
3538  if(to_unary_expr(src).op().type().id() == ID_floatbv)
3539  return convert_function(src, "signbit");
3540  else
3541  return convert_function(src, "SIGN");
3542  }
3543 
3544  else if(src.id()==ID_popcount)
3545  {
3547  return convert_function(src, "__popcnt");
3548  else
3549  return convert_function(src, "__builtin_popcount");
3550  }
3551 
3552  else if(src.id()=="pointer_arithmetic")
3553  return convert_pointer_arithmetic(src, precedence=16);
3554 
3555  else if(src.id()=="pointer_difference")
3556  return convert_pointer_difference(src, precedence=16);
3557 
3558  else if(src.id() == ID_null_object)
3559  return "NULL-object";
3560 
3561  else if(src.id()==ID_integer_address ||
3562  src.id()==ID_integer_address_object ||
3563  src.id()==ID_stack_object ||
3564  src.id()==ID_static_object)
3565  {
3566  return id2string(src.id());
3567  }
3568 
3569  else if(src.id()=="builtin-function")
3570  return src.get_string(ID_identifier);
3571 
3572  else if(src.id()==ID_array_of)
3573  return convert_array_of(src, precedence=16);
3574 
3575  else if(src.id()==ID_bswap)
3576  return convert_function(
3577  src,
3578  "__builtin_bswap" + integer2string(*pointer_offset_bits(
3579  to_unary_expr(src).op().type(), ns)));
3580 
3581  else if(has_prefix(src.id_string(), "byte_extract"))
3582  return convert_byte_extract(to_byte_extract_expr(src), precedence = 16);
3583 
3584  else if(has_prefix(src.id_string(), "byte_update"))
3585  return convert_byte_update(to_byte_update_expr(src), precedence = 16);
3586 
3587  else if(src.id()==ID_address_of)
3588  {
3589  const auto &object = to_address_of_expr(src).object();
3590 
3591  if(object.id() == ID_label)
3592  return "&&" + object.get_string(ID_identifier);
3593  else if(object.id() == ID_index && to_index_expr(object).index().is_zero())
3594  return convert(to_index_expr(object).array());
3595  else if(src.type().subtype().id()==ID_code)
3596  return convert_unary(to_unary_expr(src), "", precedence = 15);
3597  else
3598  return convert_unary(to_unary_expr(src), "&", precedence = 15);
3599  }
3600 
3601  else if(src.id()==ID_dereference)
3602  {
3603  const auto &pointer = to_dereference_expr(src).pointer();
3604 
3605  if(src.type().id() == ID_code)
3606  return convert_unary(to_unary_expr(src), "", precedence = 15);
3607  else if(
3608  pointer.id() == ID_plus && pointer.operands().size() == 2 &&
3609  to_plus_expr(pointer).op0().type().id() == ID_pointer)
3610  {
3611  // Note that index[pointer] is legal C, but we avoid it nevertheless.
3612  return convert(
3613  index_exprt(to_plus_expr(pointer).op0(), to_plus_expr(pointer).op1()));
3614  }
3615  else
3616  return convert_unary(to_unary_expr(src), "*", precedence = 15);
3617  }
3618 
3619  else if(src.id()==ID_index)
3620  return convert_index(src, precedence=16);
3621 
3622  else if(src.id()==ID_member)
3623  return convert_member(to_member_expr(src), precedence=16);
3624 
3625  else if(src.id()=="array-member-value")
3626  return convert_array_member_value(src, precedence=16);
3627 
3628  else if(src.id()=="struct-member-value")
3629  return convert_struct_member_value(src, precedence=16);
3630 
3631  else if(src.id()==ID_function_application)
3633 
3634  else if(src.id()==ID_side_effect)
3635  {
3636  const irep_idt &statement=src.get(ID_statement);
3637  if(statement==ID_preincrement)
3638  return convert_unary(to_unary_expr(src), "++", precedence = 15);
3639  else if(statement==ID_predecrement)
3640  return convert_unary(to_unary_expr(src), "--", precedence = 15);
3641  else if(statement==ID_postincrement)
3642  return convert_unary_post(to_unary_expr(src), "++", precedence = 16);
3643  else if(statement==ID_postdecrement)
3644  return convert_unary_post(to_unary_expr(src), "--", precedence = 16);
3645  else if(statement==ID_assign_plus)
3646  return convert_binary(to_binary_expr(src), "+=", precedence = 2, true);
3647  else if(statement==ID_assign_minus)
3648  return convert_binary(to_binary_expr(src), "-=", precedence = 2, true);
3649  else if(statement==ID_assign_mult)
3650  return convert_binary(to_binary_expr(src), "*=", precedence = 2, true);
3651  else if(statement==ID_assign_div)
3652  return convert_binary(to_binary_expr(src), "/=", precedence = 2, true);
3653  else if(statement==ID_assign_mod)
3654  return convert_binary(to_binary_expr(src), "%=", precedence = 2, true);
3655  else if(statement==ID_assign_shl)
3656  return convert_binary(to_binary_expr(src), "<<=", precedence = 2, true);
3657  else if(statement==ID_assign_shr)
3658  return convert_binary(to_binary_expr(src), ">>=", precedence = 2, true);
3659  else if(statement==ID_assign_bitand)
3660  return convert_binary(to_binary_expr(src), "&=", precedence = 2, true);
3661  else if(statement==ID_assign_bitxor)
3662  return convert_binary(to_binary_expr(src), "^=", precedence = 2, true);
3663  else if(statement==ID_assign_bitor)
3664  return convert_binary(to_binary_expr(src), "|=", precedence = 2, true);
3665  else if(statement==ID_assign)
3666  return convert_binary(to_binary_expr(src), "=", precedence = 2, true);
3667  else if(statement==ID_function_call)
3670  else if(statement == ID_allocate)
3671  return convert_allocate(src, precedence = 15);
3672  else if(statement==ID_printf)
3673  return convert_function(src, "printf");
3674  else if(statement==ID_nondet)
3675  return convert_nondet(src, precedence=16);
3676  else if(statement=="prob_coin")
3677  return convert_prob_coin(src, precedence=16);
3678  else if(statement=="prob_unif")
3679  return convert_prob_uniform(src, precedence=16);
3680  else if(statement==ID_statement_expression)
3681  return convert_statement_expression(src, precedence=15);
3682  else if(statement == ID_va_start)
3683  return convert_function(src, CPROVER_PREFIX "va_start");
3684  else
3685  return convert_norep(src, precedence);
3686  }
3687 
3688  else if(src.id()==ID_literal)
3689  return convert_literal(src);
3690 
3691  else if(src.id()==ID_not)
3692  return convert_unary(to_not_expr(src), "!", precedence = 15);
3693 
3694  else if(src.id()==ID_bitnot)
3695  return convert_unary(to_bitnot_expr(src), "~", precedence = 15);
3696 
3697  else if(src.id()==ID_mult)
3698  return convert_multi_ary(src, "*", precedence=13, false);
3699 
3700  else if(src.id()==ID_div)
3701  return convert_binary(to_div_expr(src), "/", precedence = 13, true);
3702 
3703  else if(src.id()==ID_mod)
3704  return convert_binary(to_mod_expr(src), "%", precedence = 13, true);
3705 
3706  else if(src.id()==ID_shl)
3707  return convert_binary(to_shl_expr(src), "<<", precedence = 11, true);
3708 
3709  else if(src.id()==ID_ashr || src.id()==ID_lshr)
3710  return convert_binary(to_shift_expr(src), ">>", precedence = 11, true);
3711 
3712  else if(src.id()==ID_lt || src.id()==ID_gt ||
3713  src.id()==ID_le || src.id()==ID_ge)
3714  {
3715  return convert_binary(
3716  to_binary_relation_expr(src), src.id_string(), precedence = 10, true);
3717  }
3718 
3719  else if(src.id()==ID_notequal)
3720  return convert_binary(to_notequal_expr(src), "!=", precedence = 9, true);
3721 
3722  else if(src.id()==ID_equal)
3723  return convert_binary(to_equal_expr(src), "==", precedence = 9, true);
3724 
3725  else if(src.id()==ID_complex)
3726  return convert_complex(src, precedence=16);
3727 
3728  else if(src.id()==ID_bitand)
3729  return convert_multi_ary(src, "&", precedence=8, false);
3730 
3731  else if(src.id()==ID_bitxor)
3732  return convert_multi_ary(src, "^", precedence=7, false);
3733 
3734  else if(src.id()==ID_bitor)
3735  return convert_multi_ary(src, "|", precedence=6, false);
3736 
3737  else if(src.id()==ID_and)
3738  return convert_multi_ary(src, "&&", precedence=5, false);
3739 
3740  else if(src.id()==ID_or)
3741  return convert_multi_ary(src, "||", precedence=4, false);
3742 
3743  else if(src.id()==ID_xor)
3744  return convert_multi_ary(src, "!=", precedence = 9, false);
3745 
3746  else if(src.id()==ID_implies)
3747  return convert_binary(to_implies_expr(src), "==>", precedence = 3, true);
3748 
3749  else if(src.id()==ID_if)
3750  return convert_trinary(to_if_expr(src), "?", ":", precedence = 3);
3751 
3752  else if(src.id()==ID_forall)
3753  return convert_quantifier(
3754  to_quantifier_expr(src), "forall", precedence = 2);
3755 
3756  else if(src.id()==ID_exists)
3757  return convert_quantifier(
3758  to_quantifier_expr(src), "exists", precedence = 2);
3759 
3760  else if(src.id()==ID_lambda)
3761  return convert_quantifier(
3762  to_quantifier_expr(src), "LAMBDA", precedence = 2);
3763 
3764  else if(src.id()==ID_with)
3765  return convert_with(src, precedence=16);
3766 
3767  else if(src.id()==ID_update)
3768  return convert_update(to_update_expr(src), precedence = 16);
3769 
3770  else if(src.id()==ID_member_designator)
3771  return precedence=16, convert_member_designator(src);
3772 
3773  else if(src.id()==ID_index_designator)
3774  return precedence=16, convert_index_designator(src);
3775 
3776  else if(src.id()==ID_symbol)
3777  return convert_symbol(src);
3778 
3779  else if(src.id()==ID_next_symbol)
3780  return convert_symbol(src);
3781 
3782  else if(src.id()==ID_nondet_symbol)
3784 
3785  else if(src.id()==ID_predicate_symbol)
3786  return convert_predicate_symbol(src);
3787 
3788  else if(src.id()==ID_predicate_next_symbol)
3789  return convert_predicate_next_symbol(src);
3790 
3791  else if(src.id()==ID_predicate_passive_symbol)
3793 
3794  else if(src.id()=="quant_symbol")
3795  return convert_quantified_symbol(src);
3796 
3797  else if(src.id()==ID_nondet_bool)
3798  return convert_nondet_bool();
3799 
3800  else if(src.id()==ID_object_descriptor)
3801  return convert_object_descriptor(src, precedence);
3802 
3803  else if(src.id()=="Hoare")
3804  return convert_Hoare(src);
3805 
3806  else if(src.id()==ID_code)
3807  return convert_code(to_code(src));
3808 
3809  else if(src.id()==ID_constant)
3810  return convert_constant(to_constant_expr(src), precedence);
3811 
3812  else if(src.id()==ID_string_constant)
3813  return '"' + MetaString(id2string(to_string_constant(src).get_value())) +
3814  '"';
3815 
3816  else if(src.id()==ID_struct)
3817  return convert_struct(src, precedence);
3818 
3819  else if(src.id()==ID_vector)
3820  return convert_vector(src, precedence);
3821 
3822  else if(src.id()==ID_union)
3823  return convert_union(to_unary_expr(src), precedence);
3824 
3825  else if(src.id()==ID_array)
3826  return convert_array(src);
3827 
3828  else if(src.id() == ID_array_list)
3829  return convert_array_list(src, precedence);
3830 
3831  else if(src.id()==ID_typecast)
3832  return convert_typecast(to_typecast_expr(src), precedence=14);
3833 
3834  else if(src.id()==ID_comma)
3835  return convert_comma(src, precedence=1);
3836 
3837  else if(src.id()==ID_ptr_object)
3838  return "PTR_OBJECT("+id2string(src.get(ID_identifier))+")";
3839 
3840  else if(src.id()==ID_cond)
3841  return convert_cond(src, precedence);
3842 
3843  else if(
3844  src.id() == ID_overflow_unary_minus || src.id() == ID_overflow_minus ||
3845  src.id() == ID_overflow_mult || src.id() == ID_overflow_plus ||
3846  src.id() == ID_overflow_shl)
3847  {
3848  return convert_overflow(src, precedence);
3849  }
3850 
3851  else if(src.id()==ID_unknown)
3852  return "*";
3853 
3854  else if(src.id()==ID_invalid)
3855  return "#";
3856 
3857  else if(src.id()==ID_extractbit)
3858  return convert_extractbit(to_extractbit_expr(src), precedence);
3859 
3860  else if(src.id()==ID_extractbits)
3861  return convert_extractbits(to_extractbits_expr(src), precedence);
3862 
3863  else if(src.id()==ID_initializer_list ||
3864  src.id()==ID_compound_literal)
3865  {
3866  precedence = 15;
3867  return convert_initializer_list(src);
3868  }
3869 
3870  else if(src.id()==ID_designated_initializer)
3871  {
3872  precedence = 15;
3873  return convert_designated_initializer(src);
3874  }
3875 
3876  else if(src.id()==ID_sizeof)
3877  return convert_sizeof(src, precedence);
3878 
3879  else if(src.id()==ID_let)
3880  return convert_let(to_let_expr(src), precedence=16);
3881 
3882  else if(src.id()==ID_type)
3883  return convert(src.type());
3884 
3885  else if(src.id() == ID_rol || src.id() == ID_ror)
3886  return convert_rox(to_shift_expr(src), precedence);
3887 
3888  auto function_string_opt = convert_function(src);
3889  if(function_string_opt.has_value())
3890  return *function_string_opt;
3891 
3892  // no C language expression for internal representation
3893  return convert_norep(src, precedence);
3894 }
3895 
3897 {
3898  static const std::map<irep_idt, std::string> function_names = {
3899  {"buffer_size", "BUFFER_SIZE"},
3900  {"is_zero_string", "IS_ZERO_STRING"},
3901  {"object_value", "OBJECT_VALUE"},
3902  {"pointer_base", "POINTER_BASE"},
3903  {"pointer_cons", "POINTER_CONS"},
3904  {"zero_string", "ZERO_STRING"},
3905  {"zero_string_length", "ZERO_STRING_LENGTH"},
3906  {ID_abs, "abs"},
3907  {ID_alignof, "alignof"}, // C uses "_Alignof", C++ uses "alignof"
3908  {ID_builtin_offsetof, "builtin_offsetof"},
3909  {ID_complex_imag, "__imag__"},
3910  {ID_complex_real, "__real__"},
3911  {ID_concatenation, "CONCATENATION"},
3912  {ID_count_leading_zeros, "__builtin_clz"},
3913  {ID_count_trailing_zeros, "__builtin_ctz"},
3914  {ID_dynamic_object, "DYNAMIC_OBJECT"},
3915  {ID_floatbv_div, "FLOAT/"},
3916  {ID_floatbv_minus, "FLOAT-"},
3917  {ID_floatbv_mult, "FLOAT*"},
3918  {ID_floatbv_plus, "FLOAT+"},
3919  {ID_floatbv_rem, "FLOAT%"},
3920  {ID_gcc_builtin_va_arg, "gcc_builtin_va_arg"},
3921  {ID_get_may, CPROVER_PREFIX "get_may"},
3922  {ID_get_must, CPROVER_PREFIX "get_must"},
3923  {ID_good_pointer, "GOOD_POINTER"},
3924  {ID_ieee_float_equal, "IEEE_FLOAT_EQUAL"},
3925  {ID_ieee_float_notequal, "IEEE_FLOAT_NOTEQUAL"},
3926  {ID_infinity, "INFINITY"},
3927  {ID_is_dynamic_object, "IS_DYNAMIC_OBJECT"},
3928  {ID_is_invalid_pointer, "IS_INVALID_POINTER"},
3929  {ID_is_invalid_pointer, CPROVER_PREFIX "is_invalid_pointer"},
3930  {ID_isfinite, "isfinite"},
3931  {ID_isinf, "isinf"},
3932  {ID_isnan, "isnan"},
3933  {ID_isnormal, "isnormal"},
3934  {ID_object_size, "OBJECT_SIZE"},
3935  {ID_pointer_object, "POINTER_OBJECT"},
3936  {ID_pointer_offset, "POINTER_OFFSET"},
3937  {ID_r_ok, "R_OK"},
3938  {ID_w_ok, "W_OK"},
3939  {ID_rw_ok, "RW_OK"},
3940  {ID_width, "WIDTH"},
3941  };
3942 
3943  const auto function_entry = function_names.find(src.id());
3944  if(function_entry == function_names.end())
3945  return nullopt;
3946 
3947  return convert_function(src, function_entry->second);
3948 }
3949 
3950 std::string expr2ct::convert(const exprt &src)
3951 {
3952  unsigned precedence;
3953  return convert_with_precedence(src, precedence);
3954 }
3955 
3962  const typet &src,
3963  const std::string &identifier)
3964 {
3965  return convert_rec(src, c_qualifierst(), identifier);
3966 }
3967 
3968 std::string expr2c(
3969  const exprt &expr,
3970  const namespacet &ns,
3971  const expr2c_configurationt &configuration)
3972 {
3973  std::string code;
3974  expr2ct expr2c(ns, configuration);
3975  expr2c.get_shorthands(expr);
3976  return expr2c.convert(expr);
3977 }
3978 
3979 std::string expr2c(const exprt &expr, const namespacet &ns)
3980 {
3982 }
3983 
3984 std::string type2c(
3985  const typet &type,
3986  const namespacet &ns,
3987  const expr2c_configurationt &configuration)
3988 {
3989  expr2ct expr2c(ns, configuration);
3990  // expr2c.get_shorthands(expr);
3991  return expr2c.convert(type);
3992 }
3993 
3994 std::string type2c(const typet &type, const namespacet &ns)
3995 {
3997 }
3998 
3999 std::string type2c(
4000  const typet &type,
4001  const std::string &identifier,
4002  const namespacet &ns,
4003  const expr2c_configurationt &configuration)
4004 {
4005  expr2ct expr2c(ns, configuration);
4006  return expr2c.convert_with_identifier(type, identifier);
4007 }
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
bool can_cast_type< signedbv_typet >(const typet &type)
Check whether a reference to a typet is a signedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
bool can_cast_type< unsignedbv_typet >(const typet &type)
Check whether a reference to a typet is a unsignedbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
std::string MetaString(const std::string &in)
Definition: c_misc.cpp:95
ANSI-C Misc Utilities.
floatbv_typet float_type()
Definition: c_types.cpp:185
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
unsignedbv_typet size_type()
Definition: c_types.cpp:58
std::string c_type_as_string(const irep_idt &c_type)
Definition: c_types.cpp:259
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
bitvector_typet char_type()
Definition: c_types.cpp:114
bitvector_typet wchar_t_type()
Definition: c_types.cpp:149
floatbv_typet long_double_type()
Definition: c_types.cpp:201
floatbv_typet double_type()
Definition: c_types.cpp:193
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 code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
Definition: c_types.h:399
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:317
exprt & object()
Definition: pointer_expr.h:350
Arithmetic right shift.
A base class for binary expressions.
Definition: std_expr.h:550
exprt & op1()
Definition: expr.h:102
exprt & op0()
Definition: expr.h:99
exprt & where()
Definition: std_expr.h:2877
Bit-wise OR.
std::size_t get_width() const
Definition: std_types.h:843
Expression of type type extracted from some object op starting at position offset (given in number of...
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:292
The type of C enums.
Definition: c_types.h:204
const memberst & members() const
Definition: c_types.h:242
std::vector< c_enum_membert > memberst
Definition: c_types.h:240
virtual std::string as_string() const override
virtual void read(const typet &src) override
codet representation of an inline assembler statement.
Definition: std_code.h:1699
const irep_idt & get_flavor() const
Definition: std_code.h:1709
A codet representing an assignment in the program.
Definition: std_code.h:293
A codet representing sequential composition of program statements.
Definition: std_code.h:168
code_operandst & statements()
Definition: std_code.h:176
codet representation of a do while statement.
Definition: std_code.h:988
const exprt & cond() const
Definition: std_code.h:995
const codet & body() const
Definition: std_code.h:1005
codet representation of a for statement.
Definition: std_code.h:1050
const exprt & init() const
Definition: std_code.h:1065
const exprt & iter() const
Definition: std_code.h:1085
const exprt & cond() const
Definition: std_code.h:1075
const codet & body() const
Definition: std_code.h:1095
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
codet representation of an if-then-else statement.
Definition: std_code.h:776
const codet & then_case() const
Definition: std_code.h:804
const exprt & cond() const
Definition: std_code.h:794
const codet & else_case() const
Definition: std_code.h:814
codet representation of a label for branch targets.
Definition: std_code.h:1405
const irep_idt & get_label() const
Definition: std_code.h:1413
codet & code()
Definition: std_code.h:1423
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1469
codet & code()
Definition: std_code.h:1496
const exprt & case_op() const
Definition: std_code.h:1486
bool is_default() const
Definition: std_code.h:1476
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
bool get_inlined() const
Definition: std_types.h:665
bool has_ellipsis() const
Definition: std_types.h:611
const parameterst & parameters() const
Definition: std_types.h:655
codet representing a while statement.
Definition: std_code.h:926
const exprt & cond() const
Definition: std_code.h:933
const codet & body() const
Definition: std_code.h:943
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
exprt & op3()
Definition: expr.h:108
exprt & op1()
Definition: expr.h:102
exprt & op2()
Definition: expr.h:105
exprt & op0()
Definition: expr.h:99
const irep_idt & get_statement() const
Definition: std_code.h:69
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition: std_expr.h:2753
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
const char * c_str() const
Definition: dstring.h:99
size_t size() const
Definition: dstring.h:104
optionalt< std::string > convert_function(const exprt &src)
Returns a string if src is a function with a known conversion, else returns nullopt.
std::string convert_nondet(const exprt &src, unsigned &precedence)
std::string convert_literal(const exprt &src)
std::string convert_code_continue(unsigned indent)
std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent)
virtual std::string convert_symbol(const exprt &src)
std::string convert_typecast(const typecast_exprt &src, unsigned &precedence)
std::string convert_comma(const exprt &src, unsigned precedence)
std::string convert_code_assert(const codet &src, unsigned indent)
std::string convert_quantifier(const quantifier_exprt &, const std::string &symbol, unsigned precedence)
std::string convert_union(const exprt &src, unsigned &precedence)
std::string convert_code_expression(const codet &src, unsigned indent)
std::string convert_code_goto(const codet &src, unsigned indent)
std::string convert_code_switch(const codet &src, unsigned indent)
std::string convert_initializer_list(const exprt &src)
std::string convert_quantified_symbol(const exprt &src)
std::string convert_function_application(const function_application_exprt &src)
std::string convert_code_unlock(const codet &src, unsigned indent)
std::string convert_code_decl_block(const codet &src, unsigned indent)
std::string convert_byte_update(const byte_update_exprt &, unsigned precedence)
std::string convert_code(const codet &src)
std::string convert_pointer_arithmetic(const exprt &src, unsigned &precedence)
std::string convert_let(const let_exprt &, unsigned precedence)
std::string convert_nondet_bool()
std::string convert_norep(const exprt &src, unsigned &precedence)
const expr2c_configurationt & configuration
Definition: expr2c_class.h:49
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > ns_collision
Definition: expr2c_class.h:81
std::string convert_code_output(const codet &src, unsigned indent)
std::string convert_code_while(const code_whilet &src, unsigned indent)
virtual std::string convert_array_type(const typet &src, const qualifierst &qualifiers, const std::string &declarator_str)
std::string convert_index_designator(const exprt &src)
std::string convert_pointer_difference(const exprt &src, unsigned &precedence)
std::string convert_code_block(const code_blockt &src, unsigned indent)
std::string convert_code_asm(const code_asmt &src, unsigned indent)
std::string convert_allocate(const exprt &src, unsigned &precedence)
std::string convert_Hoare(const exprt &src)
std::string convert_sizeof(const exprt &src, unsigned &precedence)
std::string convert_code_lock(const codet &src, unsigned indent)
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent)
irep_idt id_shorthand(const irep_idt &identifier) const
Definition: expr2c.cpp:76
std::string convert_cond(const exprt &src, unsigned precedence)
std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src)
std::string convert_overflow(const exprt &src, unsigned &precedence)
std::string convert_member(const member_exprt &src, unsigned precedence)
void get_shorthands(const exprt &expr)
Definition: expr2c.cpp:117
std::string convert_code_for(const code_fort &src, unsigned indent)
std::string convert_with_identifier(const typet &src, const std::string &identifier)
std::string convert_extractbits(const extractbits_exprt &src, unsigned precedence)
std::string convert_code_decl(const codet &src, unsigned indent)
std::string convert_trinary(const ternary_exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence)
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
std::string convert_prob_coin(const exprt &src, unsigned &precedence)
std::string convert_update(const update_exprt &, unsigned precedence)
std::string convert_nondet_symbol(const nondet_symbol_exprt &)
std::string convert_code_printf(const codet &src, unsigned indent)
std::string convert_unary(const unary_exprt &, const std::string &symbol, unsigned precedence)
std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent)
std::string convert_member_designator(const exprt &src)
virtual std::string convert_struct_type(const typet &src, const std::string &qualifiers_str, const std::string &declarator_str)
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
Definition: expr2c.cpp:219
static std::string indent_str(unsigned indent)
std::string convert_byte_extract(const byte_extract_exprt &, unsigned precedence)
std::string convert_code_label(const code_labelt &src, unsigned indent)
std::string convert_code_array_copy(const codet &src, unsigned indent)
virtual std::string convert_constant_bool(bool boolean_value)
std::string convert_statement_expression(const exprt &src, unsigned &precendence)
std::string convert_struct_member_value(const exprt &src, unsigned precedence)
std::string convert_code_dead(const codet &src, unsigned indent)
const namespacet & ns
Definition: expr2c_class.h:48
std::string convert_rox(const shift_exprt &src, unsigned precedence)
Conversion function from rol/ror expressions to C code strings Note that this constructs a complex ex...
std::string convert_designated_initializer(const exprt &src)
std::string convert_vector(const exprt &src, unsigned &precedence)
std::string convert_multi_ary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
std::string convert_array_member_value(const exprt &src, unsigned precedence)
std::string convert_unary_post(const exprt &src, const std::string &symbol, unsigned precedence)
std::unordered_map< irep_idt, irep_idt > shorthands
Definition: expr2c_class.h:82
std::string convert_complex(const exprt &src, unsigned precedence)
std::string convert_code_assign(const code_assignt &src, unsigned indent)
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
std::string convert_code_fence(const codet &src, unsigned indent)
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:214
std::string convert_code_return(const codet &src, unsigned indent)
std::string convert_code_break(unsigned indent)
std::string convert_with(const exprt &src, unsigned precedence)
std::string convert_object_descriptor(const exprt &src, unsigned &precedence)
std::string convert_predicate_passive_symbol(const exprt &src)
std::string convert_array_list(const exprt &src, unsigned &precedence)
unsigned sizeof_nesting
Definition: expr2c_class.h:84
std::string convert_array_of(const exprt &src, unsigned precedence)
std::string convert_code_array_replace(const codet &src, unsigned indent)
std::string convert_index(const exprt &src, unsigned precedence)
std::string convert_code_assume(const codet &src, unsigned indent)
std::string convert_code_input(const codet &src, unsigned indent)
std::string convert_extractbit(const extractbit_exprt &, unsigned precedence)
std::string convert_predicate_next_symbol(const exprt &src)
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
std::string convert_code_array_set(const codet &src, unsigned indent)
std::string convert_binary(const binary_exprt &, const std::string &symbol, unsigned precedence, bool full_parentheses)
std::string convert_predicate_symbol(const exprt &src)
std::string convert_array(const exprt &src)
std::string convert_prob_uniform(const exprt &src, unsigned &precedence)
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
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
const source_locationt & source_location() const
Definition: expr.h:230
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
Extracts a single bit of a bit-vector operand.
Extracts a sub-range of a bit-vector operand.
std::size_t get_fraction_bits() const
std::string to_ansi_c_string() const
Definition: fixedbv.h:62
Application of (mathematical) function.
std::string to_ansi_c_string() const
Definition: ieee_float.h:281
Array index operator.
Definition: std_expr.h:1328
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
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
const std::string & id_string() const
Definition: irep.h:410
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
bool is_nil() const
Definition: irep.h:387
A let expression.
Definition: std_expr.h:2919
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:3012
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition: std_expr.h:2958
exprt & value()
convenience accessor for the value of a single binding
Definition: std_expr.h:2974
std::string expr2string() const
Definition: lispexpr.cpp:15
Extract member of struct or union.
Definition: std_expr.h:2613
const exprt & compound() const
Definition: std_expr.h:2654
irep_idt get_component_name() const
Definition: std_expr.h:2627
std::size_t get_component_number() const
Definition: std_expr.h:2637
Binary minus.
Definition: std_expr.h:973
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
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
Expression to hold a nondeterministic choice.
Definition: std_expr.h:209
const irep_idt & get_identifier() const
Definition: std_expr.h:237
virtual std::unique_ptr< qualifierst > clone() const =0
A base class for quantifier expressions.
symbol_exprt & symbol()
A base class for shift and rotate operators.
exprt & distance()
exprt & op()
Left shift.
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2138
exprt::operandst & arguments()
Definition: std_code.h:2164
const irep_idt & get_function() const
const irep_idt & get_comment() const
const irept::named_subt & get_pragmas() const
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
const irep_idt & get_pretty_name() const
Definition: std_types.h:109
Base type for structs and unions.
Definition: std_types.h:62
irep_idt get_tag() const
Definition: std_types.h:168
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:49
bool is_incomplete() const
A struct/union may be incomplete.
Definition: std_types.h:185
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
const irep_idt & get_identifier() const
Definition: std_expr.h:109
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_file_local
Definition: symbol.h:66
bool is_static_lifetime
Definition: symbol.h:65
bool is_parameter
Definition: symbol.h:67
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
typet type
Type of symbol.
Definition: symbol.h:31
bool is_exported
Definition: symbol.h:61
An expression with three operands.
Definition: std_expr.h:53
exprt & op1()
Definition: expr.h:102
exprt & op2()
Definition: expr.h:105
exprt & op0()
Definition: expr.h:99
Semantic type conversion.
Definition: std_expr.h:1866
The type of an expression, extends irept.
Definition: type.h:28
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
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.
Operator to update elements in structs and arrays.
Definition: std_expr.h:2442
The vector type.
Definition: std_types.h:975
const constant_exprt & size() const
Definition: std_types.cpp:239
exprt & old()
Definition: std_expr.h:2268
configt config
Definition: config.cpp:25
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
static std::string clean_identifier(const irep_idt &id)
Definition: expr2c.cpp:94
std::string type2c(const typet &type, const namespacet &ns)
std::string expr2c(const exprt &expr, const namespacet &ns)
#define forall_operands(it, expr)
Definition: expr.h:18
#define forall_expr(it, expr)
Definition: expr.h:30
std::unordered_set< irep_idt > find_symbol_identifiers(const exprt &src)
Find identifiers of the sub expressions with id ID_symbol.
API to expression classes for floating-point arithmetic.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: floatbv_expr.h:68
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
void irep2lisp(const irept &src, lispexprt &dest)
Definition: lispirep.cpp:43
literalt pos(literalt a)
Definition: literal.h:194
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
optionalt< exprt > build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
#define SYMEX_DYNAMIC_PREFIX
BigInt mp_integer
Definition: smt_terms.h:12
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:846
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1389
bool can_cast_expr< code_inputt >(const exprt &base)
Definition: std_code.h:703
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:970
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1523
bool can_cast_expr< code_outputt >(const exprt &base)
Definition: std_code.h:749
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1450
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:2185
const codet & to_code(const exprt &expr)
Definition: std_code.h:153
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:1032
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:254
const code_fort & to_code_for(const codet &code)
Definition: std_code.h:1139
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1324
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1728
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:381
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1308
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:2507
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:3043
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 mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1160
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2152
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1648
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1113
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2320
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:953
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition: std_expr.h:260
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2008
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:807
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1000
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
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition: std_types.h:731
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 struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
const string_constantt & to_string_constant(const exprt &expr)
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.
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.
Definition: string_utils.h:62
std::size_t long_double_width
Definition: config.h:119
std::size_t double_width
Definition: config.h:118
bool char_is_unsigned
Definition: config.h:123
std::size_t long_long_int_width
Definition: config.h:115
bool NULL_is_zero
Definition: config.h:167
std::size_t long_int_width
Definition: config.h:111
std::size_t single_width
Definition: config.h:117
std::size_t short_int_width
Definition: config.h:114
std::size_t char_width
Definition: config.h:113
flavourt mode
Definition: config.h:195
std::size_t int_width
Definition: config.h:110
Used for configuring the behaviour of expr2c and type2c.
Definition: expr2c.h:21
bool print_enum_int_value
When printing an enum-typed constant, print the integer representation.
Definition: expr2c.h:43
static expr2c_configurationt clean_configuration
This prints compilable C that loses some of the internal details of the GOTO program.
Definition: expr2c.h:75
bool expand_typedef
Print the expanded type instead of a typedef name, even when a typedef is present.
Definition: expr2c.h:47
static expr2c_configurationt default_configuration
This prints a human readable C like syntax that closely mirrors the internals of the GOTO program.
Definition: expr2c.h:71
std::string true_string
This is the string that will be printed for the true boolean expression.
Definition: expr2c.h:34
bool print_struct_body_in_type
When printing a struct_typet, should the components of the struct be printed inline.
Definition: expr2c.h:28
bool use_library_macros
This is the string that will be printed for null pointers.
Definition: expr2c.h:40
bool include_struct_padding_components
When printing struct_typet or struct_exprt, include the artificial padding components introduced to k...
Definition: expr2c.h:24
std::string false_string
This is the string that will be printed for the false boolean expression.
Definition: expr2c.h:37
bool include_array_size
When printing array_typet, should the size of the array be printed.
Definition: expr2c.h:31
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
Symbol table entry.
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45