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