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