cprover
goto_program2code.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dump Goto-Program as C/C++ Source
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "goto_program2code.h"
13
14#include <sstream>
15
16#include <util/arith_tools.h>
17#include <util/c_types.h>
18#include <util/expr_util.h>
19#include <util/ieee_float.h>
20#include <util/pointer_expr.h>
21#include <util/prefix.h>
22#include <util/simplify_expr.h>
23
25{
26 // labels stored for cleanup
27 labels_in_use.clear();
28
29 // just an estimate
31
32 // find loops first
34
35 // gather variable scope information
37
38 // see whether var args are in use, identify va_list symbol
40
41 // convert
44 target,
47
49}
50
52{
53 loop_map.clear();
54 loops.loop_map.clear();
56
57 for(natural_loopst::loop_mapt::const_iterator
58 l_it=loops.loop_map.begin();
59 l_it!=loops.loop_map.end();
60 ++l_it)
61 {
62 assert(!l_it->second.empty());
63
64 // l_it->first need not be the program-order first instruction in the
65 // natural loop, because a natural loop may have multiple entries. But we
66 // ignore all those before l_it->first
67 // Furthermore the loop may contain code after the source of the actual back
68 // edge -- we also ignore such code
69 goto_programt::const_targett loop_start=l_it->first;
70 goto_programt::const_targett loop_end=loop_start;
72 it=l_it->second.begin();
73 it!=l_it->second.end();
74 ++it)
75 if((*it)->is_goto())
76 {
77 if((*it)->get_target()==loop_start &&
78 (*it)->location_number>loop_end->location_number)
79 loop_end=*it;
80 }
81
82 if(!loop_map.insert(std::make_pair(loop_start, loop_end)).second)
84 }
85}
86
88{
89 dead_map.clear();
90
91 // record last dead X
92 for(const auto &instruction : goto_program.instructions)
93 {
94 if(instruction.is_dead())
95 {
96 dead_map[instruction.dead_symbol().get_identifier()] =
97 instruction.location_number;
98 }
99 }
100}
101
103{
104 va_list_expr.clear();
105
106 for(const auto &instruction : goto_program.instructions)
107 {
108 if(instruction.is_assign())
109 {
110 const exprt &l = instruction.assign_lhs();
111 const exprt &r = instruction.assign_rhs();
112
113 // find va_start
114 if(
115 r.id() == ID_side_effect &&
116 to_side_effect_expr(r).get_statement() == ID_va_start)
117 {
118 va_list_expr.insert(to_unary_expr(r).op());
119 }
120 // try our modelling of va_start
121 else if(l.type().id()==ID_pointer &&
122 l.type().get(ID_C_typedef)=="va_list" &&
123 l.id()==ID_symbol &&
124 r.id()==ID_typecast &&
125 to_typecast_expr(r).op().id()==ID_address_of)
126 va_list_expr.insert(l);
127 }
128 }
129
130 if(!va_list_expr.empty())
131 system_headers.insert("stdarg.h");
132}
133
137 code_blockt &dest)
138{
139 assert(target!=goto_program.instructions.end());
140
141 if(
142 target->type() != ASSERT &&
143 !target->source_location().get_comment().empty())
144 {
145 dest.add(code_skipt());
146 dest.statements().back().add_source_location().set_comment(
147 target->source_location().get_comment());
148 }
149
150 // try do-while first
151 if(target->is_target() && !target->is_goto())
152 {
153 loopt::const_iterator loop_entry=loop_map.find(target);
154
155 if(loop_entry!=loop_map.end() &&
156 (upper_bound==goto_program.instructions.end() ||
157 upper_bound->location_number > loop_entry->second->location_number))
158 return convert_do_while(target, loop_entry->second, dest);
159 }
160
161 convert_labels(target, dest);
162
163 switch(target->type())
164 {
165 case SKIP:
166 case LOCATION:
167 case END_FUNCTION:
168 case DEAD:
169 // ignore for now
170 dest.add(code_skipt());
171 return target;
172
173 case FUNCTION_CALL:
174 {
176 target->call_lhs(), target->call_function(), target->call_arguments());
177 dest.add(call);
178 }
179 return target;
180
181 case OTHER:
182 dest.add(target->get_other());
183 return target;
184
185 case ASSIGN:
186 return convert_assign(target, upper_bound, dest);
187
188 case SET_RETURN_VALUE:
189 return convert_set_return_value(target, upper_bound, dest);
190
191 case DECL:
192 return convert_decl(target, upper_bound, dest);
193
194 case ASSERT:
195 system_headers.insert("assert.h");
196 dest.add(code_assertt(target->get_condition()));
197 dest.statements().back().add_source_location().set_comment(
198 target->source_location().get_comment());
199 return target;
200
201 case ASSUME:
202 dest.add(code_assumet(target->guard));
203 return target;
204
205 case GOTO:
206 return convert_goto(target, upper_bound, dest);
207
208 case START_THREAD:
209 return convert_start_thread(target, upper_bound, dest);
210
211 case END_THREAD:
213 dest.statements().back().add_source_location().set_comment("END_THREAD");
214 return target;
215
216 case ATOMIC_BEGIN:
217 case ATOMIC_END:
218 {
219 const code_typet void_t({}, empty_typet());
221 target->is_atomic_begin() ? CPROVER_PREFIX "atomic_begin"
222 : CPROVER_PREFIX "atomic_end",
223 void_t));
224 dest.add(std::move(f));
225 return target;
226 }
227
228 case THROW:
229 return convert_throw(target, dest);
230
231 case CATCH:
232 return convert_catch(target, upper_bound, dest);
233
235 case INCOMPLETE_GOTO:
237 }
238
239 // not reached
241 return target;
242}
243
246 code_blockt &dest)
247{
248 code_blockt *latest_block = &dest;
249
250 irep_idt target_label;
251 if(target->is_target())
252 {
253 std::stringstream label;
254 label << CPROVER_PREFIX "DUMP_L" << target->target_number;
255 code_labelt l(label.str(), code_blockt());
256 l.add_source_location() = target->source_location();
257 target_label=l.get_label();
258 latest_block->add(std::move(l));
259 latest_block =
260 &to_code_block(to_code_label(latest_block->statements().back()).code());
261 }
262
263 for(goto_programt::instructiont::labelst::const_iterator
264 it=target->labels.begin();
265 it!=target->labels.end();
266 ++it)
267 {
268 if(
269 has_prefix(id2string(*it), CPROVER_PREFIX "ASYNC_") ||
270 has_prefix(id2string(*it), CPROVER_PREFIX "DUMP_L"))
271 {
272 continue;
273 }
274
275 // keep all original labels
276 labels_in_use.insert(*it);
277
278 code_labelt l(*it, code_blockt());
279 l.add_source_location() = target->source_location();
280 latest_block->add(std::move(l));
281 latest_block =
282 &to_code_block(to_code_label(latest_block->statements().back()).code());
283 }
284
285 if(latest_block!=&dest)
286 latest_block->add(code_skipt());
287}
288
292 code_blockt &dest)
293{
294 const code_assignt a{target->assign_lhs(), target->assign_rhs()};
295
296 if(va_list_expr.find(a.lhs())!=va_list_expr.end())
297 return convert_assign_varargs(target, upper_bound, dest);
298 else
299 convert_assign_rec(a, dest);
300
301 return target;
302}
303
307 code_blockt &dest)
308{
309 const exprt this_va_list_expr = target->assign_lhs();
310 const exprt &r = skip_typecast(target->assign_rhs());
311
312 if(r.id()==ID_constant &&
313 (r.is_zero() || to_constant_expr(r).get_value()==ID_NULL))
314 {
316 symbol_exprt("va_end", code_typet({}, empty_typet())),
317 {this_va_list_expr});
318
319 dest.add(std::move(f));
320 }
321 else if(
322 r.id() == ID_side_effect &&
323 to_side_effect_expr(r).get_statement() == ID_va_start)
324 {
326 symbol_exprt(ID_va_start, code_typet({}, empty_typet())),
327 {this_va_list_expr,
329
330 dest.add(std::move(f));
331 }
332 else if(r.id() == ID_plus)
333 {
335 symbol_exprt("va_arg", code_typet({}, empty_typet())),
336 {this_va_list_expr});
337
338 // we do not bother to set the correct types here, they are not relevant for
339 // generating the correct dumped output
341 symbol_exprt("__typeof__", code_typet({}, empty_typet())),
342 {},
343 typet{},
345
346 // if the return value is used, the next instruction will be assign
348 ++next;
349 assert(next!=goto_program.instructions.end());
350 if(next!=upper_bound &&
351 next->is_assign())
352 {
353 const exprt &n_r = next->assign_rhs();
354 if(
355 n_r.id() == ID_dereference &&
356 skip_typecast(to_dereference_expr(n_r).pointer()) == this_va_list_expr)
357 {
358 f.lhs() = next->assign_lhs();
359
360 type_of.arguments().push_back(f.lhs());
361 f.arguments().push_back(type_of);
362
363 dest.add(std::move(f));
364 return next;
365 }
366 }
367
368 // assignment not found, still need a proper typeof expression
369 assert(r.find(ID_C_va_arg_type).is_not_nil());
370 const typet &va_arg_type=
371 static_cast<typet const&>(r.find(ID_C_va_arg_type));
372
373 dereference_exprt deref(
374 null_pointer_exprt(pointer_type(va_arg_type)),
375 va_arg_type);
376
377 type_of.arguments().push_back(deref);
378 f.arguments().push_back(type_of);
379
381
382 dest.add(std::move(void_f));
383 }
384 else
385 {
387 symbol_exprt("va_copy", code_typet({}, empty_typet())),
388 {this_va_list_expr, r});
389
390 dest.add(std::move(f));
391 }
392
393 return target;
394}
395
397 const code_assignt &assign,
398 code_blockt &dest)
399{
400 if(assign.rhs().id()==ID_array)
401 {
402 const array_typet &type = to_array_type(assign.rhs().type());
403
404 unsigned i=0;
405 forall_operands(it, assign.rhs())
406 {
407 index_exprt index(
408 assign.lhs(),
409 from_integer(i++, type.index_type()),
410 type.element_type());
411 convert_assign_rec(code_assignt(index, *it), dest);
412 }
413 }
414 else
415 dest.add(assign);
416}
417
421 code_blockt &dest)
422{
423 // add return instruction unless original code was missing a return
424 if(
425 target->return_value().id() != ID_side_effect ||
426 to_side_effect_expr(target->return_value()).get_statement() != ID_nondet)
427 {
428 dest.add(code_returnt{target->return_value()});
429 }
430
431 // all v3 (or later) goto programs have an explicit GOTO after return
433 ++next;
434 assert(next!=goto_program.instructions.end());
435
436 // skip goto (and possibly dead), unless crossing the current boundary
437 while(next!=upper_bound && next->is_dead() && !next->is_target())
438 ++next;
439
440 if(next!=upper_bound &&
441 next->is_goto() &&
442 !next->is_target())
443 target=next;
444
445 return target;
446}
447
451 code_blockt &dest)
452{
453 code_frontend_declt d = code_frontend_declt{target->decl_symbol()};
454 symbol_exprt &symbol = d.symbol();
455
457 ++next;
458 assert(next!=goto_program.instructions.end());
459
460 // see if decl can go in current dest block
461 dead_mapt::const_iterator entry=dead_map.find(symbol.get_identifier());
462 bool move_to_dest= &toplevel_block==&dest ||
463 (entry!=dead_map.end() &&
464 upper_bound->location_number > entry->second);
465
466 // move back initialising assignments into the decl, unless crossing the
467 // current boundary
468 if(next!=upper_bound &&
469 move_to_dest &&
470 !next->is_target() &&
471 (next->is_assign() || next->is_function_call()))
472 {
473 exprt lhs = next->is_assign() ? next->assign_lhs() : next->call_lhs();
474 if(lhs==symbol &&
475 va_list_expr.find(lhs)==va_list_expr.end())
476 {
477 if(next->is_assign())
478 {
479 d.set_initial_value({next->assign_rhs()});
480 }
481 else
482 {
483 // could hack this by just erasing the first operand
485 next->call_function(),
486 next->call_arguments(),
487 typet{},
489 d.copy_to_operands(call);
490 }
491
492 ++target;
493 convert_labels(target, dest);
494 }
495 else
496 remove_const(symbol.type());
497 }
498 // if we have a constant but can't initialize them right away, we need to
499 // remove the const marker
500 else
501 remove_const(symbol.type());
502
503 if(move_to_dest)
504 dest.add(std::move(d));
505 else
507
508 return target;
509}
510
514 code_blockt &dest)
515{
516 assert(loop_end->is_goto() && loop_end->is_backwards_goto());
517
518 code_dowhilet d(loop_end->guard, code_blockt());
519 simplify(d.cond(), ns);
520
521 copy_source_location(loop_end->targets.front(), d);
522
523 loop_last_stack.push_back(std::make_pair(loop_end, true));
524
525 for( ; target!=loop_end; ++target)
526 target = convert_instruction(target, loop_end, to_code_block(d.body()));
527
528 loop_last_stack.pop_back();
529
530 convert_labels(loop_end, to_code_block(d.body()));
531
532 dest.add(std::move(d));
533 return target;
534}
535
539 code_blockt &dest)
540{
541 assert(target->is_goto());
542 // we only do one target for now
543 assert(target->targets.size()==1);
544
545 loopt::const_iterator loop_entry=loop_map.find(target);
546
547 if(loop_entry!=loop_map.end() &&
548 (upper_bound==goto_program.instructions.end() ||
549 upper_bound->location_number > loop_entry->second->location_number))
550 return convert_goto_while(target, loop_entry->second, dest);
551 else if(!target->guard.is_true())
552 return convert_goto_switch(target, upper_bound, dest);
553 else if(!loop_last_stack.empty())
554 return convert_goto_break_continue(target, upper_bound, dest);
555 else
556 return convert_goto_goto(target, dest);
557}
558
562 code_blockt &dest)
563{
564 assert(loop_end->is_goto() && loop_end->is_backwards_goto());
565
566 if(target==loop_end) // 1: GOTO 1
567 return convert_goto_goto(target, dest);
568
570 goto_programt::const_targett after_loop=loop_end;
571 ++after_loop;
572 assert(after_loop!=goto_program.instructions.end());
573
574 copy_source_location(target, w);
575
576 if(target->get_target()==after_loop)
577 {
578 w.cond()=not_exprt(target->guard);
579 simplify(w.cond(), ns);
580 }
581 else if(target->guard.is_true())
582 {
583 target = convert_goto_goto(target, to_code_block(w.body()));
584 }
585 else
586 {
587 target = convert_goto_switch(target, loop_end, to_code_block(w.body()));
588 }
589
590 loop_last_stack.push_back(std::make_pair(loop_end, true));
591
592 for(++target; target!=loop_end; ++target)
593 target = convert_instruction(target, loop_end, to_code_block(w.body()));
594
595 loop_last_stack.pop_back();
596
597 convert_labels(loop_end, to_code_block(w.body()));
598 if(loop_end->guard.is_false())
599 {
600 to_code_block(w.body()).add(code_breakt());
601 }
602 else if(!loop_end->guard.is_true())
603 {
604 code_ifthenelset i(not_exprt(loop_end->guard), code_breakt());
605 simplify(i.cond(), ns);
606
607 copy_source_location(target, i);
608
609 to_code_block(w.body()).add(std::move(i));
610 }
611
612 if(w.body().has_operands() &&
613 to_code(w.body().operands().back()).get_statement()==ID_assign)
614 {
615 exprt increment = w.body().operands().back();
616 w.body().operands().pop_back();
617 increment.id(ID_side_effect);
618
619 code_fort f(nil_exprt(), w.cond(), increment, w.body());
620
621 copy_source_location(target, f);
622
623 f.swap(w);
624 }
625 else if(w.body().has_operands() &&
626 w.cond().is_true())
627 {
628 const codet &back=to_code(w.body().operands().back());
629
630 if(back.get_statement()==ID_break ||
631 (back.get_statement()==ID_ifthenelse &&
632 to_code_ifthenelse(back).cond().is_true() &&
633 to_code_ifthenelse(back).then_case().get_statement()==ID_break))
634 {
635 w.body().operands().pop_back();
636 code_dowhilet d(false_exprt(), w.body());
637
638 copy_source_location(target, d);
639
640 d.swap(w);
641 }
642 }
643
644 dest.add(std::move(w));
645
646 return target;
647}
648
652 const exprt &switch_var,
653 cases_listt &cases,
654 goto_programt::const_targett &first_target,
655 goto_programt::const_targett &default_target)
656{
658 std::set<goto_programt::const_targett> unique_targets;
659
660 goto_programt::const_targett cases_it=target;
661 for( ;
662 cases_it!=upper_bound && cases_it!=first_target;
663 ++cases_it)
664 {
665 if(cases_it->is_goto() &&
666 !cases_it->is_backwards_goto() &&
667 cases_it->guard.is_true())
668 {
669 default_target=cases_it->get_target();
670
671 if(first_target==goto_program.instructions.end() ||
672 first_target->location_number > default_target->location_number)
673 first_target=default_target;
674 if(last_target==goto_program.instructions.end() ||
675 last_target->location_number < default_target->location_number)
676 last_target=default_target;
677
678 cases.push_back(caset(
680 nil_exprt(),
681 cases_it,
682 default_target));
683 unique_targets.insert(default_target);
684
685 ++cases_it;
686 break;
687 }
688 else if(cases_it->is_goto() &&
689 !cases_it->is_backwards_goto() &&
690 (cases_it->guard.id()==ID_equal ||
691 cases_it->guard.id()==ID_or))
692 {
694 if(cases_it->guard.id()==ID_equal)
695 eqs.push_back(cases_it->guard);
696 else
697 eqs=cases_it->guard.operands();
698
699 // goto conversion builds disjunctions in reverse order
700 // to ensure convergence, we turn this around again
701 for(exprt::operandst::const_reverse_iterator
702 e_it=eqs.rbegin();
703 e_it!=(exprt::operandst::const_reverse_iterator)eqs.rend();
704 ++e_it)
705 {
706 if(e_it->id()!=ID_equal ||
708 switch_var!=to_equal_expr(*e_it).lhs())
709 return target;
710
711 cases.push_back(caset(
713 to_equal_expr(*e_it).rhs(),
714 cases_it,
715 cases_it->get_target()));
716 assert(cases.back().value.is_not_nil());
717
718 if(first_target==goto_program.instructions.end() ||
719 first_target->location_number>
720 cases.back().case_start->location_number)
721 first_target=cases.back().case_start;
722 if(last_target==goto_program.instructions.end() ||
723 last_target->location_number<
724 cases.back().case_start->location_number)
725 last_target=cases.back().case_start;
726
727 unique_targets.insert(cases.back().case_start);
728 }
729 }
730 else
731 return target;
732 }
733
734 // if there are less than 3 targets, we revert to if/else instead; this should
735 // help convergence
736 if(unique_targets.size()<3)
737 return target;
738
739 // make sure we don't have some overlap of gotos and switch/case
740 if(cases_it==upper_bound ||
741 (upper_bound!=goto_program.instructions.end() &&
742 upper_bound->location_number < last_target->location_number) ||
743 (last_target!=goto_program.instructions.end() &&
744 last_target->location_number > default_target->location_number) ||
745 target->get_target()==default_target)
746 return target;
747
748 return cases_it;
749}
750
753 const cfg_dominatorst &dominators,
754 cases_listt &cases,
755 std::set<unsigned> &processed_locations)
756{
757 std::set<goto_programt::const_targett> targets_done;
758
759 for(cases_listt::iterator it=cases.begin();
760 it!=cases.end();
761 ++it)
762 {
763 // some branch targets may be shared by multiple branch instructions,
764 // as in case 1: case 2: code; we build a nested code_switch_caset
765 if(!targets_done.insert(it->case_start).second)
766 continue;
767
768 // compute the block that belongs to this case
769 for(goto_programt::const_targett case_end = it->case_start;
770 case_end != goto_program.instructions.end() &&
771 case_end->type() != END_FUNCTION && case_end != upper_bound;
772 ++case_end)
773 {
774 const auto &case_end_node = dominators.get_node(case_end);
775
776 // ignore dead instructions for the following checks
777 if(!dominators.program_point_reachable(case_end_node))
778 {
779 // simplification may have figured out that a case is unreachable
780 // this is possibly getting too weird, abort to be safe
781 if(case_end==it->case_start)
782 return true;
783
784 continue;
785 }
786
787 // find the last instruction dominated by the case start
788 if(!dominators.dominates(it->case_start, case_end_node))
789 break;
790
791 if(!processed_locations.insert(case_end->location_number).second)
793
794 it->case_last=case_end;
795 }
796 }
797
798 return false;
799}
800
802 const cfg_dominatorst &dominators,
803 const cases_listt &cases,
804 goto_programt::const_targett default_target)
805{
806 for(cases_listt::const_iterator it=cases.begin();
807 it!=cases.end();
808 ++it)
809 {
810 // ignore empty cases
811 if(it->case_last==goto_program.instructions.end())
812 continue;
813
814 // the last case before default is the most interesting
815 cases_listt::const_iterator last=--cases.end();
816 if(last->case_start==default_target &&
817 it==--last)
818 {
819 // ignore dead instructions for the following checks
820 goto_programt::const_targett next_case=it->case_last;
821 for(++next_case;
822 next_case!=goto_program.instructions.end();
823 ++next_case)
824 {
825 if(dominators.program_point_reachable(next_case))
826 break;
827 }
828
829 if(
830 next_case != goto_program.instructions.end() &&
831 next_case == default_target &&
832 (!it->case_last->is_goto() ||
833 (it->case_last->get_condition().is_true() &&
834 it->case_last->get_target() == default_target)))
835 {
836 // if there is no goto here, yet we got here, all others would
837 // branch to this - we don't need default
838 return true;
839 }
840 }
841
842 // jumps to default are ok
843 if(it->case_last->is_goto() &&
844 it->case_last->guard.is_true() &&
845 it->case_last->get_target()==default_target)
846 continue;
847
848 // fall-through is ok
849 if(!it->case_last->is_goto())
850 continue;
851
852 return false;
853 }
854
855 return false;
856}
857
861 code_blockt &dest)
862{
863 // try to figure out whether this was a switch/case
864 exprt eq_cand=target->guard;
865 if(eq_cand.id()==ID_or)
866 eq_cand = to_or_expr(eq_cand).op0();
867
868 if(target->is_backwards_goto() ||
869 eq_cand.id()!=ID_equal ||
870 !skip_typecast(to_equal_expr(eq_cand).rhs()).is_constant())
871 return convert_goto_if(target, upper_bound, dest);
872
873 const cfg_dominatorst &dominators=loops.get_dominator_info();
874
875 // always use convert_goto_if for dead code as the construction below relies
876 // on effective dominator information
877 if(!dominators.program_point_reachable(target))
878 return convert_goto_if(target, upper_bound, dest);
879
880 // maybe, let's try some more
881 code_switcht s(to_equal_expr(eq_cand).lhs(), code_blockt());
882
883 copy_source_location(target, s);
884
885 // find the cases or fall back to convert_goto_if
886 cases_listt cases;
887 goto_programt::const_targett first_target=
889 goto_programt::const_targett default_target=
891
893 get_cases(
894 target,
895 upper_bound,
896 s.value(),
897 cases,
898 first_target,
899 default_target);
900
901 if(cases_start==target)
902 return convert_goto_if(target, upper_bound, dest);
903
904 // backup the top-level block as we might have to backtrack
905 code_blockt toplevel_block_bak=toplevel_block;
906
907 // add any instructions that go in the body of the switch before any cases
908 goto_programt::const_targett orig_target=target;
909 for(target=cases_start; target!=first_target; ++target)
910 target = convert_instruction(target, first_target, to_code_block(s.body()));
911
912 std::set<unsigned> processed_locations;
913
914 // iterate over all cases to identify block end points
915 if(set_block_end_points(upper_bound, dominators, cases, processed_locations))
916 {
917 toplevel_block.swap(toplevel_block_bak);
918 return convert_goto_if(orig_target, upper_bound, dest);
919 }
920
921 // figure out whether we really had a default target by testing
922 // whether all cases eventually jump to the default case
923 if(remove_default(dominators, cases, default_target))
924 {
925 cases.pop_back();
926 default_target=goto_program.instructions.end();
927 }
928
929 // find the last instruction belonging to any of the cases
930 goto_programt::const_targett max_target=target;
931 for(cases_listt::const_iterator it=cases.begin();
932 it!=cases.end();
933 ++it)
934 if(it->case_last!=goto_program.instructions.end() &&
935 it->case_last->location_number > max_target->location_number)
936 max_target=it->case_last;
937
938 std::map<goto_programt::const_targett, unsigned> targets_done;
939 loop_last_stack.push_back(std::make_pair(max_target, false));
940
941 // iterate over all <branch conditions, branch instruction, branch target>
942 // triples, build their corresponding code
943 for(cases_listt::const_iterator it=cases.begin();
944 it!=cases.end();
945 ++it)
946 {
948 // branch condition is nil_exprt for default case;
949 if(it->value.is_nil())
950 csc.set_default();
951 else
952 csc.case_op()=it->value;
953
954 // some branch targets may be shared by multiple branch instructions,
955 // as in case 1: case 2: code; we build a nested code_switch_caset
956 if(targets_done.find(it->case_start)!=targets_done.end())
957 {
958 assert(it->case_selector==orig_target ||
959 !it->case_selector->is_target());
960
961 // maintain the order to ensure convergence -> go to the innermost
963 to_code(s.body().operands()[targets_done[it->case_start]]));
964 while(cscp->code().get_statement()==ID_switch_case)
965 cscp=&to_code_switch_case(cscp->code());
966
967 csc.code().swap(cscp->code());
968 cscp->code().swap(csc);
969
970 continue;
971 }
972
973 code_blockt c;
974 if(it->case_selector!=orig_target)
975 convert_labels(it->case_selector, c);
976
977 // convert the block that belongs to this case
978 target=it->case_start;
979
980 // empty case
981 if(it->case_last==goto_program.instructions.end())
982 {
983 // only emit the jump out of the switch if it's not the last case
984 // this improves convergence
985 if(it->case_start!=(--cases.end())->case_start)
986 {
988 goto_programt::instructiont i=*(it->case_selector);
989 i.guard=true_exprt();
990 goto_programt tmp;
991 tmp.insert_before_swap(tmp.insert_before(tmp.instructions.end()), i);
992 convert_goto_goto(tmp.instructions.begin(), c);
993 }
994 }
995 else
996 {
997 goto_programt::const_targett after_last=it->case_last;
998 ++after_last;
999 for( ; target!=after_last; ++target)
1000 target=convert_instruction(target, after_last, c);
1001 }
1002
1003 csc.code().swap(c);
1004 targets_done[it->case_start]=s.body().operands().size();
1005 to_code_block(s.body()).add(std::move(csc));
1006 }
1007
1008 loop_last_stack.pop_back();
1009
1010 // make sure we didn't miss any non-dead instruction
1011 for(goto_programt::const_targett it=first_target;
1012 it!=target;
1013 ++it)
1014 if(processed_locations.find(it->location_number)==
1015 processed_locations.end())
1016 {
1017 if(dominators.program_point_reachable(it))
1018 {
1019 toplevel_block.swap(toplevel_block_bak);
1020 return convert_goto_if(orig_target, upper_bound, dest);
1021 }
1022 }
1023
1024 dest.add(std::move(s));
1025 return max_target;
1026}
1027
1030 goto_programt::const_targett upper_bound,
1031 code_blockt &dest)
1032{
1033 goto_programt::const_targett else_case=target->get_target();
1034 goto_programt::const_targett before_else=else_case;
1035 goto_programt::const_targett end_if=target->get_target();
1036 assert(end_if!=goto_program.instructions.end());
1037 bool has_else=false;
1038
1039 if(!target->is_backwards_goto())
1040 {
1041 assert(else_case!=goto_program.instructions.begin());
1042 --before_else;
1043
1044 // goto 1
1045 // 1: ...
1046 if(before_else==target)
1047 {
1048 dest.add(code_skipt());
1049 return target;
1050 }
1051
1052 has_else=
1053 before_else->is_goto() &&
1054 before_else->get_target()->location_number > end_if->location_number &&
1055 before_else->guard.is_true() &&
1056 (upper_bound==goto_program.instructions.end() ||
1057 upper_bound->location_number>=
1058 before_else->get_target()->location_number);
1059
1060 if(has_else)
1061 end_if=before_else->get_target();
1062 }
1063
1064 // some nesting of loops and branches we might not be able to deal with
1065 if(target->is_backwards_goto() ||
1066 (upper_bound!=goto_program.instructions.end() &&
1067 upper_bound->location_number < end_if->location_number))
1068 {
1069 if(!loop_last_stack.empty())
1070 return convert_goto_break_continue(target, upper_bound, dest);
1071 else
1072 return convert_goto_goto(target, dest);
1073 }
1074
1075 code_ifthenelset i(not_exprt(target->guard), code_blockt());
1076 copy_source_location(target, i);
1077 simplify(i.cond(), ns);
1078
1079 if(has_else)
1080 i.else_case()=code_blockt();
1081
1082 if(has_else)
1083 {
1084 for(++target; target!=before_else; ++target)
1085 target =
1086 convert_instruction(target, before_else, to_code_block(i.then_case()));
1087
1088 convert_labels(before_else, to_code_block(i.then_case()));
1089
1090 for(++target; target!=end_if; ++target)
1091 target =
1092 convert_instruction(target, end_if, to_code_block(i.else_case()));
1093 }
1094 else
1095 {
1096 for(++target; target!=end_if; ++target)
1097 target =
1098 convert_instruction(target, end_if, to_code_block(i.then_case()));
1099 }
1100
1101 dest.add(std::move(i));
1102 return --target;
1103}
1104
1107 goto_programt::const_targett upper_bound,
1108 code_blockt &dest)
1109{
1110 assert(!loop_last_stack.empty());
1111 const cfg_dominatorst &dominators=loops.get_dominator_info();
1112
1113 // goto 1
1114 // 1: ...
1115 goto_programt::const_targett next=target;
1116 for(++next;
1117 next!=upper_bound && next!=goto_program.instructions.end();
1118 ++next)
1119 {
1120 if(dominators.program_point_reachable(next))
1121 break;
1122 }
1123
1124 if(target->get_target()==next)
1125 {
1126 dest.add(code_skipt());
1127 // skip over all dead instructions
1128 return --next;
1129 }
1130
1131 goto_programt::const_targett loop_end=loop_last_stack.back().first;
1132
1133 if(target->get_target()==loop_end &&
1134 loop_last_stack.back().second)
1135 {
1136 code_ifthenelset i(target->guard, code_continuet());
1137 simplify(i.cond(), ns);
1138
1139 copy_source_location(target, i);
1140
1141 if(i.cond().is_true())
1142 dest.add(std::move(i.then_case()));
1143 else
1144 dest.add(std::move(i));
1145
1146 return target;
1147 }
1148
1149 goto_programt::const_targett after_loop=loop_end;
1150 for(++after_loop;
1151 after_loop!=goto_program.instructions.end();
1152 ++after_loop)
1153 {
1154 if(dominators.program_point_reachable(after_loop))
1155 break;
1156 }
1157
1158 if(target->get_target()==after_loop)
1159 {
1160 code_ifthenelset i(target->guard, code_breakt());
1161 simplify(i.cond(), ns);
1162
1163 copy_source_location(target, i);
1164
1165 if(i.cond().is_true())
1166 dest.add(std::move(i.then_case()));
1167 else
1168 dest.add(std::move(i));
1169
1170 return target;
1171 }
1172
1173 return convert_goto_goto(target, dest);
1174}
1175
1178 code_blockt &dest)
1179{
1180 // filter out useless goto 1; 1: ...
1181 goto_programt::const_targett next=target;
1182 ++next;
1183 if(target->get_target()==next)
1184 return target;
1185
1186 const cfg_dominatorst &dominators=loops.get_dominator_info();
1187
1188 // skip dead goto L as the label might be skipped if it is dead
1189 // as well and at the end of a case block
1190 if(!dominators.program_point_reachable(target))
1191 return target;
1192
1193 std::stringstream label;
1194 // try user-defined labels first
1195 for(goto_programt::instructiont::labelst::const_iterator
1196 it=target->get_target()->labels.begin();
1197 it!=target->get_target()->labels.end();
1198 ++it)
1199 {
1200 if(
1201 has_prefix(id2string(*it), CPROVER_PREFIX "ASYNC_") ||
1202 has_prefix(id2string(*it), CPROVER_PREFIX "DUMP_L"))
1203 {
1204 continue;
1205 }
1206
1207 label << *it;
1208 break;
1209 }
1210
1211 if(label.str().empty())
1212 label << CPROVER_PREFIX "DUMP_L" << target->get_target()->target_number;
1213
1214 labels_in_use.insert(label.str());
1215
1216 code_gotot goto_code(label.str());
1217
1218 code_ifthenelset i(target->guard, std::move(goto_code));
1219 simplify(i.cond(), ns);
1220
1221 copy_source_location(target, i);
1222
1223 if(i.cond().is_true())
1224 dest.add(std::move(i.then_case()));
1225 else
1226 dest.add(std::move(i));
1227
1228 return target;
1229}
1230
1233 goto_programt::const_targett upper_bound,
1234 code_blockt &dest)
1235{
1236 assert(target->is_start_thread());
1237
1238 goto_programt::const_targett thread_start=target->get_target();
1239 assert(thread_start->location_number > target->location_number);
1240
1241 goto_programt::const_targett next=target;
1242 ++next;
1243 assert(next!=goto_program.instructions.end());
1244
1245 // first check for old-style code:
1246 // __CPROVER_DUMP_0: START THREAD 1
1247 // code in existing thread
1248 // END THREAD
1249 // 1: code in new thread
1250 if(!next->is_goto())
1251 {
1252 goto_programt::const_targett this_end=next;
1253 ++this_end;
1254 assert(this_end->is_end_thread());
1255 assert(thread_start->location_number > this_end->location_number);
1256
1257 codet b=code_blockt();
1258 convert_instruction(next, this_end, to_code_block(b));
1259
1260 for(goto_programt::instructiont::labelst::const_iterator
1261 it=target->labels.begin();
1262 it!=target->labels.end();
1263 ++it)
1264 if(has_prefix(id2string(*it), CPROVER_PREFIX "ASYNC_"))
1265 {
1266 labels_in_use.insert(*it);
1267
1268 code_labelt l(*it, std::move(b));
1269 l.add_source_location() = target->source_location();
1270 b = std::move(l);
1271 }
1272
1273 assert(b.get_statement()==ID_label);
1274 dest.add(std::move(b));
1275 return this_end;
1276 }
1277
1278 // code is supposed to look like this:
1279 // __CPROVER_ASYNC_0: START THREAD 1
1280 // GOTO 2
1281 // 1: code in new thread
1282 // END THREAD
1283 // 2: code in existing thread
1284 /* check the structure and compute the iterators */
1285 assert(next->is_goto() && next->guard.is_true());
1286 assert(!next->is_backwards_goto());
1287 assert(thread_start->location_number < next->get_target()->location_number);
1288 goto_programt::const_targett after_thread_start=thread_start;
1289 ++after_thread_start;
1290
1291 goto_programt::const_targett thread_end=next->get_target();
1292 --thread_end;
1293 assert(thread_start->location_number < thread_end->location_number);
1294 assert(thread_end->is_end_thread());
1295
1296 assert(upper_bound==goto_program.instructions.end() ||
1297 thread_end->location_number < upper_bound->location_number);
1298 /* end structure check */
1299
1300 // use pthreads if "code in new thread" is a function call to a function with
1301 // suitable signature
1302 if(
1303 thread_start->is_function_call() &&
1304 thread_start->call_arguments().size() == 1 &&
1305 after_thread_start == thread_end)
1306 {
1307 system_headers.insert("pthread.h");
1308
1311 thread_start->call_lhs(),
1312 symbol_exprt("pthread_create", code_typet({}, empty_typet())),
1313 {n,
1314 n,
1315 thread_start->call_function(),
1316 thread_start->call_arguments().front()}));
1317
1318 return thread_end;
1319 }
1320
1321 codet b=code_blockt();
1322 for( ; thread_start!=thread_end; ++thread_start)
1323 thread_start =
1324 convert_instruction(thread_start, upper_bound, to_code_block(b));
1325
1326 for(goto_programt::instructiont::labelst::const_iterator
1327 it=target->labels.begin();
1328 it!=target->labels.end();
1329 ++it)
1330 if(has_prefix(id2string(*it), CPROVER_PREFIX "ASYNC_"))
1331 {
1332 labels_in_use.insert(*it);
1333
1334 code_labelt l(*it, std::move(b));
1335 l.add_source_location() = target->source_location();
1336 b = std::move(l);
1337 }
1338
1339 assert(b.get_statement()==ID_label);
1340 dest.add(std::move(b));
1341 return thread_end;
1342}
1343
1346 code_blockt &)
1347{
1348 // this isn't really clear as throw is not supported in expr2cpp either
1350 return target;
1351}
1352
1356 code_blockt &)
1357{
1358 // this isn't really clear as catch is not supported in expr2cpp either
1360 return target;
1361}
1362
1364{
1365 if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
1366 {
1367 const typet &full_type=ns.follow(type);
1368
1369 const irep_idt &identifier = to_tag_type(type).get_identifier();
1370 const symbolt &symbol = ns.lookup(identifier);
1371
1372 if(
1373 symbol.location.get_function().empty() ||
1374 !type_names_set.insert(identifier).second)
1375 return;
1376
1377 for(const auto &c : to_struct_union_type(full_type).components())
1378 add_local_types(c.type());
1379
1380 type_names.push_back(identifier);
1381 }
1382 else if(type.id()==ID_c_enum_tag)
1383 {
1384 const irep_idt &identifier=to_c_enum_tag_type(type).get_identifier();
1385 const symbolt &symbol=ns.lookup(identifier);
1386
1387 if(symbol.location.get_function().empty() ||
1388 !type_names_set.insert(identifier).second)
1389 return;
1390
1391 assert(!identifier.empty());
1392 type_names.push_back(identifier);
1393 }
1394 else if(type.id()==ID_pointer ||
1395 type.id()==ID_array)
1396 {
1397 add_local_types(to_type_with_subtype(type).subtype());
1398 }
1399}
1400
1402 codet &code,
1403 const irep_idt parent_stmt)
1404{
1405 if(code.get_statement()==ID_decl)
1406 {
1407 if(code.operands().size()==2 &&
1408 code.op1().id()==ID_side_effect &&
1409 to_side_effect_expr(code.op1()).get_statement()==ID_function_call)
1410 {
1414
1415 cleanup_expr(code.op1(), false);
1416 }
1417 else
1418 Forall_operands(it, code)
1419 cleanup_expr(*it, true);
1420
1421 if(code.op0().type().id()==ID_array)
1422 cleanup_expr(to_array_type(code.op0().type()).size(), true);
1423
1424 add_local_types(code.op0().type());
1425
1426 const irep_idt &typedef_str=code.op0().type().get(ID_C_typedef);
1427 if(!typedef_str.empty() &&
1428 typedef_names.find(typedef_str)==typedef_names.end())
1429 code.op0().type().remove(ID_C_typedef);
1430
1431 return;
1432 }
1433 else if(code.get_statement()==ID_function_call)
1434 {
1436
1438
1439 while(call.lhs().is_not_nil() &&
1440 call.lhs().id()==ID_typecast)
1441 call.lhs()=to_typecast_expr(call.lhs()).op();
1442 }
1443
1444 if(code.has_operands())
1445 {
1446 for(auto &op : code.operands())
1447 {
1448 if(op.id() == ID_code)
1449 cleanup_code(to_code(op), code.get_statement());
1450 else
1451 cleanup_expr(op, false);
1452 }
1453 }
1454
1455 const irep_idt &statement=code.get_statement();
1456 if(statement==ID_label)
1457 {
1458 code_labelt &cl=to_code_label(code);
1459 const irep_idt &label=cl.get_label();
1460
1461 assert(!label.empty());
1462
1463 if(labels_in_use.find(label)==labels_in_use.end())
1464 {
1465 codet tmp = cl.code();
1466 code.swap(tmp);
1467 }
1468 }
1469 else if(statement==ID_block)
1470 cleanup_code_block(code, parent_stmt);
1471 else if(statement==ID_ifthenelse)
1472 cleanup_code_ifthenelse(code, parent_stmt);
1473 else if(statement==ID_dowhile)
1474 {
1475 code_dowhilet &do_while=to_code_dowhile(code);
1476
1477 // turn an empty do {} while(...); into a while(...);
1478 // to ensure convergence
1479 if(do_while.body().get_statement()==ID_skip)
1480 do_while.set_statement(ID_while);
1481 // do stmt while(false) is just stmt
1482 else if(do_while.cond().is_false() &&
1483 do_while.body().get_statement()!=ID_block)
1484 code=do_while.body();
1485 }
1486}
1487
1489 const exprt &function,
1491{
1492 if(function.id()!=ID_symbol)
1493 return;
1494
1495 const symbol_exprt &fn=to_symbol_expr(function);
1496
1497 // don't edit function calls we might have introduced
1498 const symbolt *s;
1499 if(!ns.lookup(fn.get_identifier(), s))
1500 {
1501 const symbolt &fn_sym=ns.lookup(fn.get_identifier());
1502 const code_typet &code_type=to_code_type(fn_sym.type);
1503 const code_typet::parameterst &parameters=code_type.parameters();
1504
1505 if(parameters.size()==arguments.size())
1506 {
1507 code_typet::parameterst::const_iterator it=parameters.begin();
1508 for(auto &argument : arguments)
1509 {
1510 if(
1511 argument.type().id() == ID_union ||
1512 argument.type().id() == ID_union_tag)
1513 {
1514 argument.type() = it->type();
1515 }
1516 ++it;
1517 }
1518 }
1519 }
1520}
1521
1523 codet &code,
1524 const irep_idt parent_stmt)
1525{
1526 assert(code.get_statement()==ID_block);
1527
1528 exprt::operandst &operands=code.operands();
1530 operands.size()>1 && i<operands.size();
1531 ) // no ++i
1532 {
1533 exprt::operandst::iterator it=operands.begin()+i;
1534 // remove skip
1535 if(to_code(*it).get_statement()==ID_skip &&
1536 it->source_location().get_comment().empty())
1537 operands.erase(it);
1538 // merge nested blocks, unless there are declarations in the inner block
1539 else if(to_code(*it).get_statement()==ID_block)
1540 {
1541 bool has_decl=false;
1542 forall_operands(it2, *it)
1543 if(it2->id()==ID_code && to_code(*it2).get_statement()==ID_decl)
1544 {
1545 has_decl=true;
1546 break;
1547 }
1548
1549 if(!has_decl)
1550 {
1551 operands.insert(operands.begin()+i+1,
1552 it->operands().begin(), it->operands().end());
1553 operands.erase(operands.begin()+i);
1554 // no ++i
1555 }
1556 else
1557 ++i;
1558 }
1559 else
1560 ++i;
1561 }
1562
1563 if(operands.empty() && parent_stmt!=ID_nil)
1564 code=code_skipt();
1565 else if(operands.size()==1 &&
1566 parent_stmt!=ID_nil &&
1567 to_code(code.op0()).get_statement()!=ID_decl)
1568 {
1569 codet tmp = to_code(code.op0());
1570 code.swap(tmp);
1571 }
1572}
1573
1575{
1576 if(type.get_bool(ID_C_constant))
1577 type.remove(ID_C_constant);
1578
1579 if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
1580 {
1581 const irep_idt &identifier = to_tag_type(type).get_identifier();
1582 if(!const_removed.insert(identifier).second)
1583 return;
1584
1585 symbolt &symbol = symbol_table.get_writeable_ref(identifier);
1586 INVARIANT(
1587 symbol.is_type,
1588 "Symbol "+id2string(identifier)+" should be a type");
1589
1590 remove_const(symbol.type);
1591 }
1592 else if(type.id()==ID_array)
1593 remove_const(type.subtype());
1594 else if(type.id()==ID_struct ||
1595 type.id()==ID_union)
1596 {
1599
1600 for(struct_union_typet::componentst::iterator
1601 it=c.begin();
1602 it!=c.end();
1603 ++it)
1604 remove_const(it->type());
1605 }
1606 else if(type.id() == ID_c_bit_field)
1607 {
1608 to_c_bit_field_type(type).underlying_type().remove(ID_C_constant);
1609 }
1610}
1611
1612static bool has_labels(const codet &code)
1613{
1614 if(code.get_statement()==ID_label)
1615 return true;
1616
1617 forall_operands(it, code)
1618 if(it->id()==ID_code && has_labels(to_code(*it)))
1619 return true;
1620
1621 return false;
1622}
1623
1624static bool move_label_ifthenelse(exprt &expr, exprt &label_dest)
1625{
1626 if(expr.is_nil() || to_code(expr).get_statement() != ID_block)
1627 return false;
1628
1629 code_blockt &block=to_code_block(to_code(expr));
1630 if(
1631 !block.has_operands() ||
1632 block.statements().back().get_statement() != ID_label)
1633 {
1634 return false;
1635 }
1636
1637 code_labelt &label = to_code_label(block.statements().back());
1638
1639 if(label.get_label().empty() ||
1640 label.code().get_statement()!=ID_skip)
1641 {
1642 return false;
1643 }
1644
1645 label_dest=label;
1646 code_skipt s;
1647 label.swap(s);
1648
1649 return true;
1650}
1651
1653 codet &code,
1654 const irep_idt parent_stmt)
1655{
1657 const exprt cond=simplify_expr(i_t_e.cond(), ns);
1658
1659 // assert(false) expands to if(true) assert(false), simplify again (and also
1660 // simplify other cases)
1661 if(
1662 cond.is_true() &&
1663 (i_t_e.else_case().is_nil() || !has_labels(i_t_e.else_case())))
1664 {
1665 codet tmp = i_t_e.then_case();
1666 code.swap(tmp);
1667 }
1668 else if(cond.is_false() && !has_labels(i_t_e.then_case()))
1669 {
1670 if(i_t_e.else_case().is_nil())
1671 code=code_skipt();
1672 else
1673 {
1674 codet tmp = i_t_e.else_case();
1675 code.swap(tmp);
1676 }
1677 }
1678 else
1679 {
1680 if(
1681 i_t_e.then_case().is_not_nil() &&
1682 i_t_e.then_case().get_statement() == ID_ifthenelse)
1683 {
1684 // we re-introduce 1-code blocks with if-then-else to avoid dangling-else
1685 // ambiguity
1686 i_t_e.then_case() = code_blockt({i_t_e.then_case()});
1687 }
1688
1689 if(
1690 i_t_e.else_case().is_not_nil() &&
1691 i_t_e.then_case().get_statement() == ID_skip &&
1692 i_t_e.else_case().get_statement() == ID_ifthenelse)
1693 {
1694 // we re-introduce 1-code blocks with if-then-else to avoid dangling-else
1695 // ambiguity
1696 i_t_e.else_case() = code_blockt({i_t_e.else_case()});
1697 }
1698 }
1699
1700 // move labels at end of then or else case out
1701 if(code.get_statement()==ID_ifthenelse)
1702 {
1703 codet then_label=code_skipt(), else_label=code_skipt();
1704
1705 bool moved=false;
1706 if(i_t_e.then_case().is_not_nil())
1707 moved|=move_label_ifthenelse(i_t_e.then_case(), then_label);
1708 if(i_t_e.else_case().is_not_nil())
1709 moved|=move_label_ifthenelse(i_t_e.else_case(), else_label);
1710
1711 if(moved)
1712 {
1713 code = code_blockt({i_t_e, then_label, else_label});
1714 cleanup_code(code, parent_stmt);
1715 }
1716 }
1717
1718 // remove empty then/else
1719 if(
1720 code.get_statement() == ID_ifthenelse &&
1721 i_t_e.then_case().get_statement() == ID_skip)
1722 {
1723 not_exprt tmp(i_t_e.cond());
1724 simplify(tmp, ns);
1725 // simplification might have removed essential type casts
1726 cleanup_expr(tmp, false);
1727 i_t_e.cond().swap(tmp);
1728 i_t_e.then_case().swap(i_t_e.else_case());
1729 }
1730 if(
1731 code.get_statement() == ID_ifthenelse && i_t_e.else_case().is_not_nil() &&
1732 i_t_e.else_case().get_statement() == ID_skip)
1733 i_t_e.else_case().make_nil();
1734 // or even remove the if altogether if the then case is now empty
1735 if(
1736 code.get_statement() == ID_ifthenelse && i_t_e.else_case().is_nil() &&
1737 (i_t_e.then_case().is_nil() ||
1738 i_t_e.then_case().get_statement() == ID_skip))
1739 code=code_skipt();
1740}
1741
1742void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
1743{
1744 // we might have to do array -> pointer conversions
1745 if(no_typecast &&
1746 (expr.id()==ID_address_of || expr.id()==ID_member))
1747 {
1748 Forall_operands(it, expr)
1749 cleanup_expr(*it, false);
1750 }
1751 else if(!no_typecast &&
1752 (expr.id()==ID_union || expr.id()==ID_struct ||
1753 expr.id()==ID_array || expr.id()==ID_vector))
1754 {
1755 Forall_operands(it, expr)
1756 cleanup_expr(*it, true);
1757 }
1758 else
1759 {
1760 Forall_operands(it, expr)
1761 cleanup_expr(*it, no_typecast);
1762 }
1763
1764 // work around transparent union argument
1765 if(
1766 expr.id() == ID_union && expr.type().id() != ID_union &&
1767 expr.type().id() != ID_union_tag)
1768 {
1769 expr=to_union_expr(expr).op();
1770 }
1771
1772 // try to get rid of type casts, revealing (char)97 -> 'a'
1773 if(expr.id()==ID_typecast &&
1774 to_typecast_expr(expr).op().is_constant())
1775 simplify(expr, ns);
1776
1777 if(expr.id()==ID_union ||
1778 expr.id()==ID_struct)
1779 {
1780 if(no_typecast)
1781 return;
1782
1784 expr.type().id() == ID_struct_tag || expr.type().id() == ID_union_tag,
1785 "union/struct expressions should have a tag type");
1786
1787 const typet &t=expr.type();
1788
1789 add_local_types(t);
1790 expr=typecast_exprt(expr, t);
1791
1792 const irep_idt &typedef_str=expr.type().get(ID_C_typedef);
1793 if(!typedef_str.empty() &&
1794 typedef_names.find(typedef_str)==typedef_names.end())
1795 expr.type().remove(ID_C_typedef);
1796 }
1797 else if(expr.id()==ID_array ||
1798 expr.id()==ID_vector)
1799 {
1800 if(no_typecast ||
1801 expr.get_bool(ID_C_string_constant))
1802 return;
1803
1804 const typet &t=expr.type();
1805
1806 expr = typecast_exprt(expr, t);
1807 add_local_types(t);
1808
1809 const irep_idt &typedef_str=expr.type().get(ID_C_typedef);
1810 if(!typedef_str.empty() &&
1811 typedef_names.find(typedef_str)==typedef_names.end())
1812 expr.type().remove(ID_C_typedef);
1813 }
1814 else if(expr.id()==ID_side_effect)
1815 {
1816 const irep_idt &statement=to_side_effect_expr(expr).get_statement();
1817
1818 if(statement==ID_nondet)
1819 {
1820 // Replace by a function call to nondet_...
1821 // We first search for a suitable one in the symbol table.
1822
1823 irep_idt id;
1824
1825 for(symbol_tablet::symbolst::const_iterator
1826 it=symbol_table.symbols.begin();
1827 it!=symbol_table.symbols.end();
1828 it++)
1829 {
1830 if(it->second.type.id()!=ID_code)
1831 continue;
1832 if(!has_prefix(id2string(it->second.base_name), "nondet_"))
1833 continue;
1834 const code_typet &code_type=to_code_type(it->second.type);
1835 if(code_type.return_type() != expr.type())
1836 continue;
1837 if(!code_type.parameters().empty())
1838 continue;
1839 id=it->second.name;
1840 break;
1841 }
1842
1843 // none found? make one
1844
1845 if(id.empty())
1846 {
1847 irep_idt base_name;
1848
1849 if(!expr.type().get(ID_C_c_type).empty())
1850 {
1851 irep_idt suffix;
1852 suffix=expr.type().get(ID_C_c_type);
1853
1854 if(symbol_table.symbols.find("nondet_"+id2string(suffix))==
1855 symbol_table.symbols.end())
1856 base_name="nondet_"+id2string(suffix);
1857 }
1858
1859 if(base_name.empty())
1860 {
1861 unsigned count=0;
1862 while(symbol_table.symbols.find("nondet_"+std::to_string(count))!=
1863 symbol_table.symbols.end())
1864 ++count;
1865 base_name="nondet_"+std::to_string(count);
1866 }
1867
1868 symbolt symbol;
1869 symbol.base_name=base_name;
1870 symbol.name=base_name;
1871 symbol.type = code_typet({}, expr.type());
1872 id=symbol.name;
1873
1874 symbol_table.insert(std::move(symbol));
1875 }
1876
1877 const symbolt &symbol=ns.lookup(id);
1878
1879 symbol_exprt symbol_expr(symbol.name, symbol.type);
1880 symbol_expr.add_source_location()=expr.source_location();
1881
1883 symbol_expr, {}, expr.type(), expr.source_location());
1884
1885 expr.swap(call);
1886 }
1887 }
1888 else if(expr.id()==ID_isnan ||
1889 expr.id()==ID_sign)
1890 system_headers.insert("math.h");
1891 else if(expr.id()==ID_constant)
1892 {
1893 if(expr.type().id()==ID_floatbv)
1894 {
1895 const ieee_floatt f(to_constant_expr(expr));
1896 if(f.is_NaN() || f.is_infinity())
1897 system_headers.insert("math.h");
1898 }
1899 else if(expr.type().id()==ID_pointer)
1900 add_local_types(expr.type());
1901
1902 const irept &c_sizeof_type=expr.find(ID_C_c_sizeof_type);
1903
1904 if(c_sizeof_type.is_not_nil())
1905 add_local_types(static_cast<const typet &>(c_sizeof_type));
1906 }
1907 else if(expr.id()==ID_typecast)
1908 {
1909 if(expr.type().id() == ID_c_bit_field)
1910 expr=to_typecast_expr(expr).op();
1911 else
1912 {
1913 add_local_types(expr.type());
1914
1915 const irep_idt &typedef_str=expr.type().get(ID_C_typedef);
1916 if(!typedef_str.empty() &&
1917 typedef_names.find(typedef_str)==typedef_names.end())
1918 expr.type().remove(ID_C_typedef);
1919
1920 assert(expr.type().id()!=ID_union &&
1921 expr.type().id()!=ID_struct);
1922 }
1923 }
1924 else if(expr.id()==ID_symbol)
1925 {
1926 if(expr.type().id()!=ID_code)
1927 {
1928 const irep_idt &identifier=to_symbol_expr(expr).get_identifier();
1929 const symbolt &symbol=ns.lookup(identifier);
1930
1931 if(symbol.is_static_lifetime &&
1932 symbol.type.id()!=ID_code &&
1933 !symbol.is_extern &&
1934 !symbol.location.get_function().empty() &&
1935 local_static_set.insert(identifier).second)
1936 {
1937 if(symbol.value.is_not_nil())
1938 {
1939 exprt value=symbol.value;
1940 cleanup_expr(value, true);
1941 }
1942
1943 local_static.push_back(identifier);
1944 }
1945 }
1946 }
1947}
1948
1951 codet &dst)
1952{
1953 if(src->get_code().source_location().is_not_nil())
1954 dst.add_source_location() = src->get_code().source_location();
1955 else if(src->source_location().is_not_nil())
1956 dst.add_source_location() = src->source_location();
1957}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
unsignedbv_typet size_type()
Definition: c_types.cpp:68
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: c_types.h:58
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:344
exprt & object()
Definition: pointer_expr.h:370
Arrays with given size.
Definition: std_types.h:763
typet index_type() const
The type of the index expressions into any instance of this type.
Definition: std_types.cpp:33
const exprt & size() const
Definition: std_types.h:790
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
exprt & lhs()
Definition: std_expr.h:580
exprt & rhs()
Definition: std_expr.h:590
const typet & underlying_type() const
Definition: c_types.h:30
const cfgt::nodet & get_node(const T &program_point) const
Get the graph node (which gives dominators, predecessors and successors) for program_point.
bool dominates(T lhs, const nodet &rhs_node) const
Returns true if the program point corresponding to rhs_node is dominated by program point lhs.
bool program_point_reachable(const nodet &program_point_node) const
Returns true if the program point for program_point_node is reachable from the entry point.
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:270
A codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
Definition: std_code.h:217
A codet representing sequential composition of program statements.
Definition: std_code.h:130
code_operandst & statements()
Definition: std_code.h:138
void add(const codet &code)
Definition: std_code.h:168
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1182
codet representation of a continue statement (within a for or while loop).
Definition: std_code.h:1218
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 an expression statement.
Definition: std_code.h:1394
codet representation of a for statement.
Definition: std_code.h:734
A codet representing the declaration of a local variable.
Definition: std_code.h:347
void set_initial_value(optionalt< exprt > initial_value)
Sets the value to which this declaration initializes the declared variable.
Definition: std_code.h:384
symbol_exprt & symbol()
Definition: std_code.h:354
codet representation of a function call statement.
exprt::operandst argumentst
codet representation of a goto statement.
Definition: std_code.h:841
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 "return from a function" statement.
const exprt & return_value() const
A codet representing a skip statement.
Definition: std_code.h:322
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1023
void set_default()
Definition: std_code.h:1035
codet & code()
Definition: std_code.h:1050
codet representing a switch statement.
Definition: std_code.h:548
const codet & body() const
Definition: std_code.h:565
const exprt & value() const
Definition: std_code.h:555
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:542
const parameterst & parameters() const
Definition: std_types.h:655
const typet & return_type() const
Definition: std_types.h:645
codet representing a while statement.
Definition: std_code.h:610
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
const irep_idt & get_statement() const
Definition: std_code_base.h:65
void set_statement(const irep_idt &statement)
Definition: std_code_base.h:60
Operator to dereference a pointer.
Definition: pointer_expr.h:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
The empty type.
Definition: std_types.h:51
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:89
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
void reserve_operands(operandst::size_type n)
Definition: expr.h:124
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
The Boolean constant false.
Definition: std_expr.h:2865
goto_programt::const_targett convert_goto_switch(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
goto_programt::const_targett convert_assign_varargs(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
std::unordered_set< irep_idt > local_static_set
std::unordered_set< irep_idt > type_names_set
goto_programt::const_targett convert_goto_break_continue(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
void cleanup_code_ifthenelse(codet &code, const irep_idt parent_stmt)
loop_last_stackt loop_last_stack
void convert_labels(goto_programt::const_targett target, code_blockt &dest)
goto_programt::const_targett convert_decl(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
symbol_tablet & symbol_table
goto_programt::const_targett convert_do_while(goto_programt::const_targett target, goto_programt::const_targett loop_end, code_blockt &dest)
goto_programt::const_targett convert_goto_goto(goto_programt::const_targett target, code_blockt &dest)
const goto_programt & goto_program
goto_programt::const_targett convert_start_thread(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
goto_programt::const_targett get_cases(goto_programt::const_targett target, goto_programt::const_targett upper_bound, const exprt &switch_var, cases_listt &cases, goto_programt::const_targett &first_target, goto_programt::const_targett &default_target)
void cleanup_code_block(codet &code, const irep_idt parent_stmt)
std::list< caset > cases_listt
void copy_source_location(goto_programt::const_targett, codet &dst)
bool remove_default(const cfg_dominatorst &dominators, const cases_listt &cases, goto_programt::const_targett default_target)
goto_programt::const_targett convert_throw(goto_programt::const_targett target, code_blockt &dest)
std::unordered_set< irep_idt > const_removed
goto_programt::const_targett convert_catch(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
void remove_const(typet &type)
std::unordered_set< exprt, irep_hash > va_list_expr
goto_programt::const_targett convert_goto(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
void add_local_types(const typet &type)
void cleanup_expr(exprt &expr, bool no_typecast)
void cleanup_code(codet &code, const irep_idt parent_stmt)
void cleanup_function_call(const exprt &function, code_function_callt::argumentst &arguments)
goto_programt::const_targett convert_assign(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
goto_programt::const_targett convert_instruction(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
void convert_assign_rec(const code_assignt &assign, code_blockt &dest)
std::unordered_set< irep_idt > labels_in_use
goto_programt::const_targett convert_goto_while(goto_programt::const_targett target, goto_programt::const_targett loop_end, code_blockt &dest)
goto_programt::const_targett convert_goto_if(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
std::set< std::string > & system_headers
const namespacet ns
code_blockt & toplevel_block
const std::unordered_set< irep_idt > & typedef_names
natural_loopst loops
goto_programt::const_targett convert_set_return_value(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
bool set_block_end_points(goto_programt::const_targett upper_bound, const cfg_dominatorst &dominators, cases_listt &cases, std::set< unsigned > &processed_locations)
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
exprt guard
Guard for gotos, assume, assert Use condition() method to access.
Definition: goto_program.h:357
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:619
instructionst::const_iterator const_targett
Definition: goto_program.h:593
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:668
bool is_NaN() const
Definition: ieee_float.h:249
bool is_infinity() const
Definition: ieee_float.h:250
Array index operator.
Definition: std_expr.h:1328
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void remove(const irep_idt &name)
Definition: irep.cpp:96
bool is_not_nil() const
Definition: irep.h:380
void make_nil()
Definition: irep.h:454
void swap(irept &irep)
Definition: irep.h:442
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
loop_mapt loop_map
Definition: loop_analysis.h:88
loop_instructionst::const_iterator const_iterator
Definition: loop_analysis.h:46
exprt & op0()
Definition: std_expr.h:844
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
const cfg_dominators_templatet< P, T, false > & get_dominator_info() const
Definition: natural_loops.h:59
The NIL expression.
Definition: std_expr.h:2874
Boolean negation.
Definition: std_expr.h:2181
The null pointer constant.
Definition: pointer_expr.h:723
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_statement() const
Definition: std_code.h:1472
const irep_idt & get_function() const
Base type for structs and unions.
Definition: std_types.h:62
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_extern
Definition: symbol.h:66
bool is_static_lifetime
Definition: symbol.h:65
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
exprt value
Initial value of symbol.
Definition: symbol.h:34
const irep_idt & get_identifier() const
Definition: std_types.h:410
The Boolean constant true.
Definition: std_expr.h:2856
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
const exprt & op() const
Definition: std_expr.h:293
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:216
Deprecated expression utility functions.
const code_function_callt & to_code_function_call(const codet &code)
static bool has_labels(const codet &code)
static bool move_label_ifthenelse(exprt &expr, exprt &label_dest)
Dump Goto-Program as C/C++ Source.
#define forall_goto_program_instructions(it, program)
@ FUNCTION_CALL
Definition: goto_program.h:49
@ ATOMIC_END
Definition: goto_program.h:44
@ DEAD
Definition: goto_program.h:48
@ END_FUNCTION
Definition: goto_program.h:42
@ ASSIGN
Definition: goto_program.h:46
@ ASSERT
Definition: goto_program.h:36
@ SET_RETURN_VALUE
Definition: goto_program.h:45
@ ATOMIC_BEGIN
Definition: goto_program.h:43
@ CATCH
Definition: goto_program.h:51
@ END_THREAD
Definition: goto_program.h:40
@ SKIP
Definition: goto_program.h:38
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
@ START_THREAD
Definition: goto_program.h:39
@ THROW
Definition: goto_program.h:50
@ DECL
Definition: goto_program.h:47
@ OTHER
Definition: goto_program.h:37
@ GOTO
Definition: goto_program.h:34
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
static int8_t r
Definition: irep_hash.h:60
bool is_true(const literalt &l)
Definition: literal.h:198
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1506
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1077
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_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 codet & to_code(const exprt &expr)
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2129
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1657
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:29
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:434
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177