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