cprover
Loading...
Searching...
No Matches
goto_convert.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Program Transformation
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "goto_convert.h"
13
14#include <util/arith_tools.h>
15#include <util/c_types.h>
16#include <util/cprover_prefix.h>
18#include <util/expr_util.h>
19#include <util/fresh_symbol.h>
20#include <util/pointer_expr.h>
21#include <util/prefix.h>
22#include <util/simplify_expr.h>
23#include <util/std_expr.h>
26
27#include "goto_convert_class.h"
28#include "destructor.h"
29#include "remove_skip.h"
30
31static bool is_empty(const goto_programt &goto_program)
32{
33 forall_goto_program_instructions(it, goto_program)
34 if(!is_skip(goto_program, it))
35 return false;
36
37 return true;
38}
39
43{
44 std::map<irep_idt, goto_programt::targett> label_targets;
45
46 // in the first pass collect the labels and the corresponding targets
48 {
49 if(!it->labels.empty())
50 {
51 for(auto label : it->labels)
52 // record the label and the corresponding target
53 label_targets.insert(std::make_pair(label, it));
54 }
55 }
56
57 // in the second pass set the targets
58 for(auto &instruction : dest.instructions)
59 {
60 if(
61 instruction.is_catch() &&
62 instruction.code().get_statement() == ID_push_catch)
63 {
64 // Populate `targets` with a GOTO instruction target per
65 // exception handler if it isn't already populated.
66 // (Java handlers, for example, need this finish step; C++
67 // handlers will already be populated by now)
68
69 if(instruction.targets.empty())
70 {
71 bool handler_added=true;
73 to_code_push_catch(instruction.code()).exception_list();
74
75 for(const auto &handler : handler_list)
76 {
77 // some handlers may not have been converted (if there was no
78 // exception to be caught); in such a situation we abort
79 if(label_targets.find(handler.get_label())==label_targets.end())
80 {
81 handler_added=false;
82 break;
83 }
84 }
85
86 if(!handler_added)
87 continue;
88
89 for(const auto &handler : handler_list)
90 instruction.targets.push_back(label_targets.at(handler.get_label()));
91 }
92 }
93 }
94}
95
96/******************************************************************* \
97
98Function: goto_convertt::finish_gotos
99
100 Inputs:
101
102 Outputs:
103
104 Purpose:
105
106\*******************************************************************/
107
109{
110 for(const auto &g_it : targets.gotos)
111 {
113
114 if(i.is_start_thread())
115 {
116 const irep_idt &goto_label = i.code().get(ID_destination);
117
118 labelst::const_iterator l_it=
119 targets.labels.find(goto_label);
120
121 if(l_it == targets.labels.end())
122 {
124 "goto label \'" + id2string(goto_label) + "\' not found",
125 i.code().find_source_location());
126 }
127
128 i.targets.push_back(l_it->second.first);
129 }
130 else if(i.is_incomplete_goto())
131 {
132 const irep_idt &goto_label = i.code().get(ID_destination);
133
134 labelst::const_iterator l_it=targets.labels.find(goto_label);
135
136 if(l_it == targets.labels.end())
137 {
139 "goto label \'" + id2string(goto_label) + "\' not found",
140 i.code().find_source_location());
141 }
142
143 i.complete_goto(l_it->second.first);
144
145 node_indext label_target = l_it->second.second;
147
148 // Compare the currently-live variables on the path of the GOTO and label.
149 // We want to work out what variables should die during the jump.
151 targets.destructor_stack.get_nearest_common_ancestor_info(
153
154 bool not_prefix =
155 intersection_result.right_depth_below_common_ancestor != 0;
156
157 // If our goto had no variables of note, just skip
158 if(goto_target != 0)
159 {
160 // If the goto recorded a destructor stack, execute as much as is
161 // appropriate for however many automatic variables leave scope.
162 // We don't currently handle variables *entering* scope, which
163 // is illegal for C++ non-pod types and impossible in Java in any case.
164 if(not_prefix)
165 {
167 debug() << "encountered goto '" << goto_label
168 << "' that enters one or more lexical blocks; "
169 << "omitting constructors and destructors" << eom;
170 }
171 else
172 {
174 debug() << "adding goto-destructor code on jump to '" << goto_label
175 << "'" << eom;
176
180 i.source_location(),
182 mode,
186
187 // This should leave iterators intact, as long as
188 // goto_programt::instructionst is std::list.
189 }
190 }
191 }
192 else
193 {
195 }
196 }
197
198 targets.gotos.clear();
199}
200
202{
203 for(auto &g_it : targets.computed_gotos)
204 {
207 const exprt pointer = destination.pointer();
208
209 // remember the expression for later checks
210 i =
212
213 // insert huge case-split
214 for(const auto &label : targets.labels)
215 {
217 label_expr.set(ID_identifier, label.first);
218
220
221 goto_program.insert_after(
222 g_it,
224 label.second.first, guard, i.source_location()));
225 }
226 }
227
228 targets.computed_gotos.clear();
229}
230
235{
236 // We cannot use a set of targets, as target iterators
237 // cannot be compared at this stage.
238
239 // collect targets: reset marking
240 for(auto &i : dest.instructions)
242
243 // mark the goto targets
244 unsigned cnt = 0;
245 for(auto &i : dest.instructions)
246 if(i.is_goto())
247 i.get_target()->target_number = (++cnt);
248
249 for(auto it = dest.instructions.begin(); it != dest.instructions.end(); it++)
250 {
251 if(!it->is_goto())
252 continue;
253
254 auto it_goto_y = std::next(it);
255
256 if(
257 it_goto_y == dest.instructions.end() || !it_goto_y->is_goto() ||
258 !it_goto_y->condition().is_true() || it_goto_y->is_target())
259 {
260 continue;
261 }
262
263 auto it_z = std::next(it_goto_y);
264
265 if(it_z == dest.instructions.end())
266 continue;
267
268 // cannot compare iterators, so compare target number instead
269 if(it->get_target()->target_number == it_z->target_number)
270 {
271 it->set_target(it_goto_y->get_target());
272 it->condition_nonconst() = boolean_negate(it->condition());
273 it_goto_y->turn_into_skip();
274 }
275 }
276}
277
279 const codet &code,
280 goto_programt &dest,
281 const irep_idt &mode)
282{
283 goto_convert_rec(code, dest, mode);
284}
285
287 const codet &code,
288 goto_programt &dest,
289 const irep_idt &mode)
290{
291 convert(code, dest, mode);
292
293 finish_gotos(dest, mode);
297}
298
300 const codet &code,
302 goto_programt &dest)
303{
305 code, code.source_location(), type, nil_exprt(), {}));
306}
307
309 const code_labelt &code,
310 goto_programt &dest,
311 const irep_idt &mode)
312{
313 // grab the label
314 const irep_idt &label=code.get_label();
315
317
318 // magic thread creation label.
319 // The "__CPROVER_ASYNC_" signals the start of a sequence of instructions
320 // that can be executed in parallel, i.e, a new thread.
321 if(has_prefix(id2string(label), CPROVER_PREFIX "ASYNC_"))
322 {
323 // the body of the thread is expected to be
324 // in the operand.
326 to_code_label(code).code().is_not_nil(),
327 "code() in magic thread creation label is null");
328
329 // replace the magic thread creation label with a
330 // thread block (START_THREAD...END_THREAD).
332 thread_body.add(to_code_label(code).code());
333 thread_body.add_source_location()=code.source_location();
335 }
336 else
337 {
338 convert(to_code_label(code).code(), tmp, mode);
339
340 goto_programt::targett target=tmp.instructions.begin();
342
343 targets.labels.insert(
344 {label, {target, targets.destructor_stack.get_current_node()}});
345 target->labels.push_front(label);
346 }
347}
348
350 const codet &,
352{
353 // ignore for now
354}
355
357 const code_switch_caset &code,
358 goto_programt &dest,
359 const irep_idt &mode)
360{
362 convert(code.code(), tmp, mode);
363
364 goto_programt::targett target=tmp.instructions.begin();
366
367 // is a default target given?
368
369 if(code.is_default())
370 targets.set_default(target);
371 else
372 {
373 // cases?
374
375 cases_mapt::iterator cases_entry=targets.cases_map.find(target);
376 if(cases_entry==targets.cases_map.end())
377 {
378 targets.cases.push_back(std::make_pair(target, caset()));
379 cases_entry=targets.cases_map.insert(std::make_pair(
380 target, --targets.cases.end())).first;
381 }
382
384 case_op_dest.push_back(code.case_op());
385 }
386}
387
389 const code_gcc_switch_case_ranget &code,
390 goto_programt &dest,
391 const irep_idt &mode)
392{
393 const auto lb = numeric_cast<mp_integer>(code.lower());
394 const auto ub = numeric_cast<mp_integer>(code.upper());
395
397 lb.has_value() && ub.has_value(),
398 "GCC's switch-case-range statement requires constant bounds",
399 code.find_source_location());
400
401 if(*lb > *ub)
402 {
404 warning() << "GCC's switch-case-range statement with empty case range"
405 << eom;
406 }
407
409 convert(code.code(), tmp, mode);
410
411 goto_programt::targett target = tmp.instructions.begin();
413
414 cases_mapt::iterator cases_entry = targets.cases_map.find(target);
415 if(cases_entry == targets.cases_map.end())
416 {
417 targets.cases.push_back({target, caset()});
419 targets.cases_map.insert({target, --targets.cases.end()}).first;
420 }
421
422 // create a skeleton for case_guard
423 cases_entry->second->second.push_back(
426}
427
430 const codet &code,
431 goto_programt &dest,
432 const irep_idt &mode)
433{
434 const irep_idt &statement=code.get_statement();
435
436 if(statement==ID_block)
437 convert_block(to_code_block(code), dest, mode);
438 else if(statement==ID_decl)
440 else if(statement==ID_decl_type)
441 convert_decl_type(code, dest);
442 else if(statement==ID_expression)
443 convert_expression(to_code_expression(code), dest, mode);
444 else if(statement==ID_assign)
445 convert_assign(to_code_assign(code), dest, mode);
446 else if(statement==ID_assert)
447 convert_assert(to_code_assert(code), dest, mode);
448 else if(statement==ID_assume)
449 convert_assume(to_code_assume(code), dest, mode);
450 else if(statement==ID_function_call)
452 else if(statement==ID_label)
453 convert_label(to_code_label(code), dest, mode);
454 else if(statement==ID_gcc_local_label)
455 convert_gcc_local_label(code, dest);
456 else if(statement==ID_switch_case)
457 convert_switch_case(to_code_switch_case(code), dest, mode);
458 else if(statement==ID_gcc_switch_case_range)
460 to_code_gcc_switch_case_range(code), dest, mode);
461 else if(statement==ID_for)
462 convert_for(to_code_for(code), dest, mode);
463 else if(statement==ID_while)
464 convert_while(to_code_while(code), dest, mode);
465 else if(statement==ID_dowhile)
466 convert_dowhile(to_code_dowhile(code), dest, mode);
467 else if(statement==ID_switch)
468 convert_switch(to_code_switch(code), dest, mode);
469 else if(statement==ID_break)
470 convert_break(to_code_break(code), dest, mode);
471 else if(statement==ID_return)
472 convert_return(to_code_frontend_return(code), dest, mode);
473 else if(statement==ID_continue)
474 convert_continue(to_code_continue(code), dest, mode);
475 else if(statement==ID_goto)
476 convert_goto(to_code_goto(code), dest);
477 else if(statement==ID_gcc_computed_goto)
478 convert_gcc_computed_goto(code, dest);
479 else if(statement==ID_skip)
480 convert_skip(code, dest);
481 else if(statement==ID_ifthenelse)
482 convert_ifthenelse(to_code_ifthenelse(code), dest, mode);
483 else if(statement==ID_start_thread)
484 convert_start_thread(code, dest);
485 else if(statement==ID_end_thread)
486 convert_end_thread(code, dest);
487 else if(statement==ID_atomic_begin)
488 convert_atomic_begin(code, dest);
489 else if(statement==ID_atomic_end)
490 convert_atomic_end(code, dest);
491 else if(statement==ID_cpp_delete ||
492 statement=="cpp_delete[]")
493 convert_cpp_delete(code, dest);
494 else if(statement==ID_msc_try_except)
495 convert_msc_try_except(code, dest, mode);
496 else if(statement==ID_msc_try_finally)
497 convert_msc_try_finally(code, dest, mode);
498 else if(statement==ID_msc_leave)
499 convert_msc_leave(code, dest, mode);
500 else if(statement==ID_try_catch) // C++ try/catch
501 convert_try_catch(code, dest, mode);
502 else if(statement==ID_CPROVER_try_catch) // CPROVER-homemade
503 convert_CPROVER_try_catch(code, dest, mode);
504 else if(statement==ID_CPROVER_throw) // CPROVER-homemade
505 convert_CPROVER_throw(code, dest, mode);
506 else if(statement==ID_CPROVER_try_finally)
507 convert_CPROVER_try_finally(code, dest, mode);
508 else if(statement==ID_asm)
509 convert_asm(to_code_asm(code), dest);
510 else if(statement==ID_static_assert)
511 {
512 PRECONDITION(code.operands().size() == 2);
513 exprt assertion =
515 simplify(assertion, ns);
517 !assertion.is_false(),
518 "static assertion " + id2string(get_string_constant(code.op1())),
519 code.op0().find_source_location());
520 }
521 else if(statement==ID_dead)
522 copy(code, DEAD, dest);
523 else if(statement==ID_decl_block)
524 {
525 for(const auto &op : code.operands())
526 convert(to_code(op), dest, mode);
527 }
528 else if(statement==ID_push_catch ||
529 statement==ID_pop_catch ||
530 statement==ID_exception_landingpad)
531 copy(code, CATCH, dest);
532 else
533 copy(code, OTHER, dest);
534
535 // make sure dest is never empty
536 if(dest.instructions.empty())
537 {
539 }
540}
541
543 const code_blockt &code,
544 goto_programt &dest,
545 const irep_idt &mode)
546{
547 const source_locationt &end_location=code.end_location();
548
549 // this saves the index of the destructor stack
551 targets.destructor_stack.get_current_node();
552
553 // now convert block
554 for(const auto &b_code : code.statements())
555 convert(b_code, dest, mode);
556
557 // see if we need to do any destructors -- may have been processed
558 // in a prior break/continue/return already, don't create dead code
559 if(
560 !dest.empty() && dest.instructions.back().is_goto() &&
561 dest.instructions.back().condition().is_true())
562 {
563 // don't do destructors when we are unreachable
564 }
565 else
566 unwind_destructor_stack(end_location, dest, mode, old_stack_top);
567
568 // Set the current node of our destructor stack back to before the block.
569 targets.destructor_stack.set_current_node(old_stack_top);
570}
571
573 const code_expressiont &code,
574 goto_programt &dest,
575 const irep_idt &mode)
576{
577 exprt expr = code.expression();
578
579 if(expr.id()==ID_if)
580 {
581 // We do a special treatment for c?t:f
582 // by compiling to if(c) t; else f;
583 const if_exprt &if_expr=to_if_expr(expr);
585 if_expr.cond(),
586 code_expressiont(if_expr.true_case()),
587 code_expressiont(if_expr.false_case()));
588 tmp_code.add_source_location()=expr.source_location();
589 tmp_code.then_case().add_source_location()=expr.source_location();
590 tmp_code.else_case().add_source_location()=expr.source_location();
591 convert_ifthenelse(tmp_code, dest, mode);
592 }
593 else
594 {
595 clean_expr(expr, dest, mode, false); // result _not_ used
596
597 // Any residual expression?
598 // We keep it to add checks later.
599 if(expr.is_not_nil())
600 {
601 codet tmp=code;
602 tmp.op0()=expr;
603 tmp.add_source_location()=expr.source_location();
604 copy(tmp, OTHER, dest);
605 }
606 }
607}
608
610 const code_frontend_declt &code,
611 goto_programt &dest,
612 const irep_idt &mode)
613{
614 const irep_idt &identifier = code.get_identifier();
615
616 const symbolt &symbol = ns.lookup(identifier);
617
618 if(symbol.is_static_lifetime ||
619 symbol.type.id()==ID_code)
620 return; // this is a SKIP!
621
622 if(code.operands().size()==1)
623 {
624 copy(code, DECL, dest);
625 }
626 else
627 {
628 exprt initializer = code.op1();
629
630 codet tmp=code;
631 tmp.operands().resize(1);
632 // hide this declaration-without-initializer step in the goto trace
633 tmp.add_source_location().set_hide();
634
635 // Break up into decl and assignment.
636 // Decl must be visible before initializer.
637 copy(tmp, DECL, dest);
638
639 auto initializer_location = initializer.find_source_location();
640 clean_expr(initializer, dest, mode);
641
642 if(initializer.is_not_nil())
643 {
644 code_assignt assign(code.op0(), initializer);
646
647 convert_assign(assign, dest, mode);
648 }
649 }
650
651 // now create a 'dead' instruction -- will be added after the
652 // destructor created below as unwind_destructor_stack pops off the
653 // top of the destructor stack
654 const symbol_exprt symbol_expr(symbol.name, symbol.type);
655
656 {
657 code_deadt code_dead(symbol_expr);
658 targets.destructor_stack.add(code_dead);
659 }
660
661 // do destructor
662 code_function_callt destructor=get_destructor(ns, symbol.type);
663
664 if(destructor.is_not_nil())
665 {
666 // add "this"
667 address_of_exprt this_expr(symbol_expr, pointer_type(symbol.type));
668 destructor.arguments().push_back(this_expr);
669
670 targets.destructor_stack.add(destructor);
671 }
672}
673
675 const codet &,
677{
678 // we remove these
679}
680
682 const code_assignt &code,
683 goto_programt &dest,
684 const irep_idt &mode)
685{
686 exprt lhs=code.lhs(),
687 rhs=code.rhs();
688
689 clean_expr(lhs, dest, mode);
690
691 if(rhs.id()==ID_side_effect &&
693 {
695
697 rhs.operands().size() == 2,
698 "function_call sideeffect takes two operands",
699 rhs.find_source_location());
700
701 Forall_operands(it, rhs)
702 clean_expr(*it, dest, mode);
703
705 lhs,
706 rhs_function_call.function(),
707 rhs_function_call.arguments(),
708 dest,
709 mode);
710 }
711 else if(rhs.id()==ID_side_effect &&
712 (rhs.get(ID_statement)==ID_cpp_new ||
714 {
715 Forall_operands(it, rhs)
716 clean_expr(*it, dest, mode);
717
718 // TODO: This should be done in a separate pass
719 do_cpp_new(lhs, to_side_effect_expr(rhs), dest);
720 }
721 else if(
722 rhs.id() == ID_side_effect &&
723 (rhs.get(ID_statement) == ID_assign ||
724 rhs.get(ID_statement) == ID_postincrement ||
725 rhs.get(ID_statement) == ID_preincrement ||
728 {
729 // handle above side effects
730 clean_expr(rhs, dest, mode);
731
733 new_assign.lhs() = lhs;
734 new_assign.rhs() = rhs;
735
736 copy(new_assign, ASSIGN, dest);
737 }
738 else if(rhs.id() == ID_side_effect)
739 {
740 // preserve side effects that will be handled at later stages,
741 // such as allocate, new operators of other languages, e.g. java, etc
742 Forall_operands(it, rhs)
743 clean_expr(*it, dest, mode);
744
746 new_assign.lhs()=lhs;
747 new_assign.rhs()=rhs;
748
749 copy(new_assign, ASSIGN, dest);
750 }
751 else
752 {
753 // do everything else
754 clean_expr(rhs, dest, mode);
755
757 new_assign.lhs()=lhs;
758 new_assign.rhs()=rhs;
759
760 copy(new_assign, ASSIGN, dest);
761 }
762}
763
765 const codet &code,
766 goto_programt &dest)
767{
769 code.operands().size() == 1,
770 "cpp_delete statement takes one operand",
771 code.find_source_location());
772
773 exprt tmp_op=code.op0();
774
775 clean_expr(tmp_op, dest, ID_cpp);
776
777 // we call the destructor, and then free
778 const exprt &destructor=
779 static_cast<const exprt &>(code.find(ID_destructor));
780
782
784 delete_identifier="__delete_array";
785 else if(code.get_statement()==ID_cpp_delete)
786 delete_identifier="__delete";
787 else
789
790 if(destructor.is_not_nil())
791 {
793 {
794 // build loop
795 }
796 else if(code.get_statement()==ID_cpp_delete)
797 {
798 // just one object
800
801 codet tmp_code=to_code(destructor);
803 convert(tmp_code, dest, ID_cpp);
804 }
805 else
807 }
808
809 // now do "free"
811
813 to_code_type(delete_symbol.type()).parameters().size() == 1,
814 "delete statement takes 1 parameter");
815
817 to_code_type(delete_symbol.type()).parameters().front().type();
818
821 delete_call.add_source_location()=code.source_location();
822
823 convert(delete_call, dest, ID_cpp);
824}
825
827 const code_assertt &code,
828 goto_programt &dest,
829 const irep_idt &mode)
830{
831 exprt cond=code.assertion();
832
833 clean_expr(cond, dest, mode);
834
836 annotated_location.set("user-provided", true);
838}
839
841 const codet &code,
842 goto_programt &dest)
843{
845 code, code.source_location(), SKIP, nil_exprt(), {}));
846}
847
849 const code_assumet &code,
850 goto_programt &dest,
851 const irep_idt &mode)
852{
853 exprt op=code.assumption();
854
855 clean_expr(op, dest, mode);
856
858}
859
861 const codet &code,
863 const irep_idt &mode)
864{
865 auto assigns = static_cast<const unary_exprt &>(code.find(ID_C_spec_assigns));
866 if(assigns.is_not_nil())
867 {
868 PRECONDITION(loop->is_goto());
869 loop->condition_nonconst().add(ID_C_spec_assigns).swap(assigns.op());
870 }
871
872 auto invariant =
873 static_cast<const exprt &>(code.find(ID_C_spec_loop_invariant));
874 if(!invariant.is_nil())
875 {
876 if(has_subexpr(invariant, ID_side_effect))
877 {
879 "Loop invariant is not side-effect free.", code.find_source_location());
880 }
881
882 PRECONDITION(loop->is_goto());
883 loop->condition_nonconst().add(ID_C_spec_loop_invariant).swap(invariant);
884 }
885
886 auto decreases_clause =
887 static_cast<const exprt &>(code.find(ID_C_spec_decreases));
888 if(!decreases_clause.is_nil())
889 {
891 {
893 "Decreases clause is not side-effect free.",
894 code.find_source_location());
895 }
896
897 PRECONDITION(loop->is_goto());
898 loop->condition_nonconst().add(ID_C_spec_decreases).swap(decreases_clause);
899 }
900}
901
903 const code_fort &code,
904 goto_programt &dest,
905 const irep_idt &mode)
906{
907 // turn for(A; c; B) { P } into
908 // A; while(c) { P; B; }
909 //-----------------------------
910 // A;
911 // u: sideeffects in c
912 // v: if(!c) goto z;
913 // w: P;
914 // x: B; <-- continue target
915 // y: goto u;
916 // z: ; <-- break target
917
918 // A;
919 if(code.init().is_not_nil())
920 convert(to_code(code.init()), dest, mode);
921
922 exprt cond=code.cond();
923
925 clean_expr(cond, sideeffects, mode);
926
927 // save break/continue targets
929
930 // do the u label
931 goto_programt::targett u=sideeffects.instructions.begin();
932
933 // do the v label
936
937 // do the z label
941
942 // do the x label
944
945 if(code.iter().is_nil())
946 {
948 }
949 else
950 {
951 exprt tmp_B=code.iter();
952
953 clean_expr(tmp_B, tmp_x, mode, false);
954
955 if(tmp_x.instructions.empty())
957 }
958
959 // optimize the v label
960 if(sideeffects.instructions.empty())
961 u=v;
962
963 // set the targets
964 targets.set_break(z);
965 targets.set_continue(tmp_x.instructions.begin());
966
967 // v: if(!c) goto z;
968 *v =
970
971 // do the w label
973 convert(code.body(), tmp_w, mode);
974
975 // y: goto u;
979
980 // assigns clause, loop invariant and decreases clause
981 convert_loop_contracts(code, y, mode);
982
989
990 // restore break/continue
991 old_targets.restore(targets);
992}
993
995 const code_whilet &code,
996 goto_programt &dest,
997 const irep_idt &mode)
998{
999 const exprt &cond=code.cond();
1000 const source_locationt &source_location=code.source_location();
1001
1002 // while(c) P;
1003 //--------------------
1004 // v: sideeffects in c
1005 // if(!c) goto z;
1006 // x: P;
1007 // y: goto v; <-- continue target
1008 // z: ; <-- break target
1009
1010 // save break/continue targets
1012
1013 // do the z label
1016 tmp_z.add(goto_programt::make_skip(source_location));
1017
1020 boolean_negate(cond), z, source_location, tmp_branch, mode);
1021
1022 // do the v label
1023 goto_programt::targett v=tmp_branch.instructions.begin();
1024
1025 // y: goto v;
1029
1030 // set the targets
1031 targets.set_break(z);
1032 targets.set_continue(y);
1033
1034 // do the x label
1036 convert(code.body(), tmp_x, mode);
1037
1038 // assigns clause, loop invariant and decreases clause
1039 convert_loop_contracts(code, y, mode);
1040
1045
1046 // restore break/continue
1047 old_targets.restore(targets);
1048}
1049
1051 const code_dowhilet &code,
1052 goto_programt &dest,
1053 const irep_idt &mode)
1054{
1056 code.operands().size() == 2,
1057 "dowhile takes two operands",
1058 code.find_source_location());
1059
1060 // save source location
1061 source_locationt condition_location=code.cond().find_source_location();
1062
1063 exprt cond=code.cond();
1064
1066 clean_expr(cond, sideeffects, mode);
1067
1068 // do P while(c);
1069 //--------------------
1070 // w: P;
1071 // x: sideeffects in c <-- continue target
1072 // y: if(c) goto w;
1073 // z: ; <-- break target
1074
1075 // save break/continue targets
1077
1078 // do the y label
1082
1083 // do the z label
1087
1088 // do the x label
1090 if(sideeffects.instructions.empty())
1091 x=y;
1092 else
1093 x=sideeffects.instructions.begin();
1094
1095 // set the targets
1096 targets.set_break(z);
1097 targets.set_continue(x);
1098
1099 // do the w label
1101 convert(code.body(), tmp_w, mode);
1102 goto_programt::targett w=tmp_w.instructions.begin();
1103
1104 // y: if(c) goto w;
1105 y->complete_goto(w);
1106
1107 // assigns_clause, loop invariant and decreases clause
1108 convert_loop_contracts(code, y, mode);
1109
1114
1115 // restore break/continue targets
1116 old_targets.restore(targets);
1117}
1118
1120 const exprt &value,
1121 const exprt::operandst &case_op)
1122{
1123 PRECONDITION(!case_op.empty());
1124
1126 disjuncts.reserve(case_op.size());
1127
1128 for(const auto &op : case_op)
1129 {
1130 // could be a skeleton generated by convert_gcc_switch_case_range
1131 if(op.id() == ID_and)
1132 {
1134 PRECONDITION(to_binary_expr(and_expr.op0()).op1().is_nil());
1135 PRECONDITION(to_binary_expr(and_expr.op1()).op0().is_nil());
1136 binary_exprt skeleton = and_expr;
1137 to_binary_expr(skeleton.op0()).op1() = value;
1138 to_binary_expr(skeleton.op1()).op0() = value;
1139 disjuncts.push_back(skeleton);
1140 }
1141 else
1142 disjuncts.push_back(equal_exprt(value, op));
1143 }
1144
1145 return disjunction(disjuncts);
1146}
1147
1149 const code_switcht &code,
1150 goto_programt &dest,
1151 const irep_idt &mode)
1152{
1153 // switch(v) {
1154 // case x: Px;
1155 // case y: Py;
1156 // ...
1157 // default: Pd;
1158 // }
1159 // --------------------
1160 // location
1161 // x: if(v==x) goto X;
1162 // y: if(v==y) goto Y;
1163 // goto d;
1164 // X: Px;
1165 // Y: Py;
1166 // d: Pd;
1167 // z: ;
1168
1169 // we first add a 'location' node for the switch statement,
1170 // which would otherwise not be recorded
1172
1173 // get the location of the end of the body, but
1174 // default to location of switch, if none
1176 code.body().get_statement()==ID_block?
1177 to_code_block(code.body()).end_location():
1178 code.source_location();
1179
1180 // do the value we switch over
1181 exprt argument=code.value();
1182
1185
1186 // Avoid potential performance penalties caused by evaluating the value
1187 // multiple times (as the below chain-of-ifs does). "needs_cleaning" isn't
1188 // necessarily the right check here, and we may need to introduce a different
1189 // way of identifying the class of non-trivial expressions that warrant
1190 // introduction of a temporary.
1192 {
1193 symbolt &new_symbol = new_tmp_symbol(
1194 argument.type(),
1195 "switch_value",
1197 code.source_location(),
1198 mode);
1199
1201 new_symbol.symbol_expr(), argument, code.source_location()};
1203
1204 argument = new_symbol.symbol_expr();
1205 }
1206
1207 // save break/default/cases targets
1209
1210 // do the z label
1214
1215 // set the new targets -- continue stays as is
1216 targets.set_break(z);
1217 targets.set_default(z);
1218 targets.cases.clear();
1219 targets.cases_map.clear();
1220
1222 convert(code.body(), tmp, mode);
1223
1225
1226 // The case number represents which case this corresponds to in the sequence
1227 // of case statements.
1228 //
1229 // switch (x)
1230 // {
1231 // case 2: // case_number 1
1232 // ...;
1233 // case 3: // case_number 2
1234 // ...;
1235 // case 10: // case_number 3
1236 // ...;
1237 // }
1238 size_t case_number=1;
1239 for(auto &case_pair : targets.cases)
1240 {
1241 const caset &case_ops=case_pair.second;
1242
1243 if (case_ops.empty())
1244 continue;
1245
1246 exprt guard_expr=case_guard(argument, case_ops);
1247
1248 source_locationt source_location=case_ops.front().find_source_location();
1249 source_location.set_case_number(std::to_string(case_number));
1250 case_number++;
1251 guard_expr.add_source_location()=source_location;
1252
1254 case_pair.first, std::move(guard_expr), source_location));
1255 }
1256
1258 targets.default_target, targets.default_target->source_location()));
1259
1262 dest.destructive_append(tmp);
1264
1265 // restore old targets
1266 old_targets.restore(targets);
1267}
1268
1270 const code_breakt &code,
1271 goto_programt &dest,
1272 const irep_idt &mode)
1273{
1275 targets.break_set, "break without target", code.find_source_location());
1276
1277 // need to process destructor stack
1279 code.source_location(), dest, mode, targets.break_stack_node);
1280
1281 // add goto
1282 dest.add(
1283 goto_programt::make_goto(targets.break_target, code.source_location()));
1284}
1285
1287 const code_frontend_returnt &code,
1288 goto_programt &dest,
1289 const irep_idt &mode)
1290{
1291 if(!targets.return_set)
1292 {
1294 "return without target", code.find_source_location());
1295 }
1296
1298 code.operands().empty() || code.operands().size() == 1,
1299 "return takes none or one operand",
1300 code.find_source_location());
1301
1302 code_frontend_returnt new_code(code);
1303
1304 if(new_code.has_return_value())
1305 {
1306 bool result_is_used=
1307 new_code.return_value().type().id()!=ID_empty;
1308
1312
1313 // remove void-typed return value
1314 if(!result_is_used)
1315 new_code.return_value().make_nil();
1316 }
1317
1318 if(targets.has_return_value)
1319 {
1321 new_code.has_return_value(),
1322 "function must return value",
1323 new_code.find_source_location());
1324
1325 // Now add a 'set return value' instruction to set the return value.
1327 new_code.return_value(), new_code.source_location()));
1328 }
1329 else
1330 {
1332 !new_code.has_return_value() ||
1333 new_code.return_value().type().id() == ID_empty,
1334 "function must not return value",
1335 code.find_source_location());
1336 }
1337
1338 // Need to process _entire_ destructor stack.
1339 unwind_destructor_stack(code.source_location(), dest, mode);
1340
1341 // add goto to end-of-function
1343 targets.return_target, new_code.source_location()));
1344}
1345
1347 const code_continuet &code,
1348 goto_programt &dest,
1349 const irep_idt &mode)
1350{
1352 targets.continue_set,
1353 "continue without target",
1354 code.find_source_location());
1355
1356 // need to process destructor stack
1358 code.source_location(), dest, mode, targets.continue_stack_node);
1359
1360 // add goto
1361 dest.add(
1362 goto_programt::make_goto(targets.continue_target, code.source_location()));
1363}
1364
1366{
1367 // this instruction will be completed during post-processing
1370
1371 // remember it to do the target later
1372 targets.gotos.emplace_back(t, targets.destructor_stack.get_current_node());
1373}
1374
1376 const codet &code,
1377 goto_programt &dest)
1378{
1379 // this instruction will turn into OTHER during post-processing
1381 code, code.source_location(), NO_INSTRUCTION_TYPE, nil_exprt(), {}));
1382
1383 // remember it to do this later
1384 targets.computed_gotos.push_back(t);
1385}
1386
1388 const codet &code,
1389 goto_programt &dest)
1390{
1392 code, code.source_location(), START_THREAD, nil_exprt(), {}));
1393
1394 // remember it to do target later
1395 targets.gotos.emplace_back(
1396 start_thread, targets.destructor_stack.get_current_node());
1397}
1398
1400 const codet &code,
1401 goto_programt &dest)
1402{
1404 code.operands().empty(),
1405 "end_thread expects no operands",
1406 code.find_source_location());
1407
1408 copy(code, END_THREAD, dest);
1409}
1410
1412 const codet &code,
1413 goto_programt &dest)
1414{
1416 code.operands().empty(),
1417 "atomic_begin expects no operands",
1418 code.find_source_location());
1419
1420 copy(code, ATOMIC_BEGIN, dest);
1421}
1422
1424 const codet &code,
1425 goto_programt &dest)
1426{
1428 code.operands().empty(),
1429 ": atomic_end expects no operands",
1430 code.find_source_location());
1431
1432 copy(code, ATOMIC_END, dest);
1433}
1434
1436 const code_ifthenelset &code,
1437 goto_programt &dest,
1438 const irep_idt &mode)
1439{
1440 DATA_INVARIANT(code.then_case().is_not_nil(), "cannot accept an empty body");
1441
1442 bool has_else=
1443 !code.else_case().is_nil();
1444
1445 const source_locationt &source_location=code.source_location();
1446
1447 // We do a bit of special treatment for && in the condition
1448 // in case cleaning would be needed otherwise.
1449 if(
1450 code.cond().id() == ID_and && code.cond().operands().size() == 2 &&
1451 (needs_cleaning(to_binary_expr(code.cond()).op0()) ||
1452 needs_cleaning(to_binary_expr(code.cond()).op1())) &&
1453 !has_else)
1454 {
1455 // if(a && b) XX --> if(a) if(b) XX
1457 to_binary_expr(code.cond()).op1(), code.then_case());
1458 new_if1.add_source_location() = source_location;
1460 to_binary_expr(code.cond()).op0(), std::move(new_if1));
1461 new_if0.add_source_location() = source_location;
1462 return convert_ifthenelse(new_if0, dest, mode);
1463 }
1464
1465 // convert 'then'-branch
1467 convert(code.then_case(), tmp_then, mode);
1468
1470
1471 if(has_else)
1472 convert(code.else_case(), tmp_else, mode);
1473
1474 exprt tmp_guard=code.cond();
1475 clean_expr(tmp_guard, dest, mode);
1476
1478 tmp_guard, tmp_then, tmp_else, source_location, dest, mode);
1479}
1480
1482 const exprt &expr,
1483 const irep_idt &id,
1484 std::list<exprt> &dest)
1485{
1486 if(expr.id()!=id)
1487 {
1488 dest.push_back(expr);
1489 }
1490 else
1491 {
1492 // left-to-right is important
1493 for(const auto &op : expr.operands())
1494 collect_operands(op, id, dest);
1495 }
1496}
1497
1501static inline bool is_size_one(const goto_programt &g)
1502{
1503 return (!g.instructions.empty()) &&
1504 ++g.instructions.begin()==g.instructions.end();
1505}
1506
1509 const exprt &guard,
1510 goto_programt &true_case,
1511 goto_programt &false_case,
1512 const source_locationt &source_location,
1513 goto_programt &dest,
1514 const irep_idt &mode)
1515{
1516 if(is_empty(true_case) &&
1517 is_empty(false_case))
1518 {
1519 // hmpf. Useless branch.
1522 dest.add(goto_programt::make_goto(z, guard, source_location));
1524 return;
1525 }
1526
1527 // do guarded assertions directly
1528 if(
1529 is_size_one(true_case) && true_case.instructions.back().is_assert() &&
1530 true_case.instructions.back().condition().is_false() &&
1531 true_case.instructions.back().labels.empty())
1532 {
1533 // The above conjunction deliberately excludes the instance
1534 // if(some) { label: assert(false); }
1535 true_case.instructions.back().condition_nonconst() = boolean_negate(guard);
1536 dest.destructive_append(true_case);
1537 true_case.instructions.clear();
1538 if(
1539 is_empty(false_case) ||
1540 (is_size_one(false_case) &&
1541 is_skip(false_case, false_case.instructions.begin())))
1542 return;
1543 }
1544
1545 // similarly, do guarded assertions directly
1546 if(
1547 is_size_one(false_case) && false_case.instructions.back().is_assert() &&
1548 false_case.instructions.back().condition().is_false() &&
1549 false_case.instructions.back().labels.empty())
1550 {
1551 // The above conjunction deliberately excludes the instance
1552 // if(some) ... else { label: assert(false); }
1553 false_case.instructions.back().condition_nonconst() = guard;
1554 dest.destructive_append(false_case);
1555 false_case.instructions.clear();
1556 if(
1557 is_empty(true_case) ||
1558 (is_size_one(true_case) &&
1559 is_skip(true_case, true_case.instructions.begin())))
1560 return;
1561 }
1562
1563 // a special case for C libraries that use
1564 // (void)((cond) || (assert(0),0))
1565 if(
1566 is_empty(false_case) && true_case.instructions.size() == 2 &&
1567 true_case.instructions.front().is_assert() &&
1568 true_case.instructions.front().condition().is_false() &&
1569 true_case.instructions.front().labels.empty() &&
1570 true_case.instructions.back().labels.empty())
1571 {
1572 true_case.instructions.front().condition_nonconst() = boolean_negate(guard);
1573 true_case.instructions.erase(--true_case.instructions.end());
1574 dest.destructive_append(true_case);
1575 true_case.instructions.clear();
1576
1577 return;
1578 }
1579
1580 // Flip around if no 'true' case code.
1581 if(is_empty(true_case))
1582 return generate_ifthenelse(
1584 false_case,
1585 true_case,
1586 source_location,
1587 dest,
1588 mode);
1589
1590 bool has_else=!is_empty(false_case);
1591
1592 // if(c) P;
1593 //--------------------
1594 // v: if(!c) goto z;
1595 // w: P;
1596 // z: ;
1597
1598 // if(c) P; else Q;
1599 //--------------------
1600 // v: if(!c) goto y;
1601 // w: P;
1602 // x: goto z;
1603 // y: Q;
1604 // z: ;
1605
1606 // do the x label
1609 true_exprt(), true_case.instructions.back().source_location()));
1610
1611 // do the z label
1614 // We deliberately don't set a location for 'z', it's a dummy
1615 // target.
1616
1617 // y: Q;
1620 if(has_else)
1621 {
1622 tmp_y.swap(false_case);
1623 y=tmp_y.instructions.begin();
1624 }
1625
1626 // v: if(!c) goto z/y;
1629 boolean_negate(guard), has_else ? y : z, source_location, tmp_v, mode);
1630
1631 // w: P;
1633 tmp_w.swap(true_case);
1634
1635 // x: goto z;
1636 CHECK_RETURN(!tmp_w.instructions.empty());
1637 x->complete_goto(z);
1638
1641
1642 if(has_else)
1643 {
1646 }
1647
1649}
1650
1652static bool has_and_or(const exprt &expr)
1653{
1654 for(const auto &op : expr.operands())
1655 {
1656 if(has_and_or(op))
1657 return true;
1658 }
1659
1660 if(expr.id()==ID_and || expr.id()==ID_or)
1661 return true;
1662
1663 return false;
1664}
1665
1667 const exprt &guard,
1669 const source_locationt &source_location,
1670 goto_programt &dest,
1671 const irep_idt &mode)
1672{
1674 {
1675 // if(guard) goto target;
1676 // becomes
1677 // if(guard) goto target; else goto next;
1678 // next: skip;
1679
1682 tmp.add(goto_programt::make_skip(source_location));
1683
1685 guard, target_true, target_false, source_location, dest, mode);
1686
1687 dest.destructive_append(tmp);
1688 }
1689 else
1690 {
1691 // simple branch
1692 exprt cond=guard;
1693 clean_expr(cond, dest, mode);
1694
1695 dest.add(goto_programt::make_goto(target_true, cond, source_location));
1696 }
1697}
1698
1701 const exprt &guard,
1704 const source_locationt &source_location,
1705 goto_programt &dest,
1706 const irep_idt &mode)
1707{
1708 if(guard.id()==ID_not)
1709 {
1710 // simply swap targets
1712 to_not_expr(guard).op(),
1715 source_location,
1716 dest,
1717 mode);
1718 return;
1719 }
1720
1721 if(guard.id()==ID_and)
1722 {
1723 // turn
1724 // if(a && b) goto target_true; else goto target_false;
1725 // into
1726 // if(!a) goto target_false;
1727 // if(!b) goto target_false;
1728 // goto target_true;
1729
1730 std::list<exprt> op;
1731 collect_operands(guard, guard.id(), op);
1732
1733 for(const auto &expr : op)
1735 boolean_negate(expr), target_false, source_location, dest, mode);
1736
1737 dest.add(goto_programt::make_goto(target_true, source_location));
1738
1739 return;
1740 }
1741 else if(guard.id()==ID_or)
1742 {
1743 // turn
1744 // if(a || b) goto target_true; else goto target_false;
1745 // into
1746 // if(a) goto target_true;
1747 // if(b) goto target_true;
1748 // goto target_false;
1749
1750 std::list<exprt> op;
1751 collect_operands(guard, guard.id(), op);
1752
1753 // true branch(es)
1754 for(const auto &expr : op)
1756 expr, target_true, source_location, dest, mode);
1757
1758 // false branch
1759 dest.add(goto_programt::make_goto(target_false, guard.source_location()));
1760
1761 return;
1762 }
1763
1764 exprt cond=guard;
1765 clean_expr(cond, dest, mode);
1766
1767 // true branch
1768 dest.add(goto_programt::make_goto(target_true, cond, source_location));
1769
1770 // false branch
1771 dest.add(goto_programt::make_goto(target_false, source_location));
1772}
1773
1775 const exprt &expr,
1776 irep_idt &value)
1777{
1778 if(expr.id() == ID_typecast)
1779 return get_string_constant(to_typecast_expr(expr).op(), value);
1780
1781 if(
1782 expr.id() == ID_address_of &&
1783 to_address_of_expr(expr).object().id() == ID_index)
1784 {
1785 exprt index_op =
1786 get_constant(to_index_expr(to_address_of_expr(expr).object()).array());
1788
1790 {
1791 value = to_string_constant(index_op).get_value();
1792 return false;
1793 }
1794 else if(index_op.id()==ID_array)
1795 {
1796 std::string result;
1797 for(const auto &op : as_const(index_op).operands())
1798 {
1799 if(op.is_constant())
1800 {
1801 const auto i = numeric_cast<std::size_t>(op);
1802 if(!i.has_value())
1803 return true;
1804
1805 if(i.value() != 0) // to skip terminating 0
1806 result += static_cast<char>(i.value());
1807 }
1808 }
1809
1810 return value=result, false;
1811 }
1812 }
1813
1814 if(expr.id()==ID_string_constant)
1815 {
1816 value = to_string_constant(expr).get_value();
1817 return false;
1818 }
1819
1820 return true;
1821}
1822
1824{
1826
1827 const bool res = get_string_constant(expr, result);
1829 !res,
1830 "expected string constant",
1831 expr.find_source_location(),
1832 expr.pretty());
1833
1834 return result;
1835}
1836
1838{
1839 if(expr.id()==ID_symbol)
1840 {
1841 const symbolt &symbol=
1842 ns.lookup(to_symbol_expr(expr));
1843
1844 return symbol.value;
1845 }
1846 else if(expr.id()==ID_member)
1847 {
1848 auto tmp = to_member_expr(expr);
1849 tmp.compound() = get_constant(tmp.compound());
1850 return std::move(tmp);
1851 }
1852 else if(expr.id()==ID_index)
1853 {
1854 auto tmp = to_index_expr(expr);
1855 tmp.op0() = get_constant(tmp.op0());
1856 tmp.op1() = get_constant(tmp.op1());
1857 return std::move(tmp);
1858 }
1859 else
1860 return expr;
1861}
1862
1864 const typet &type,
1865 const std::string &suffix,
1866 goto_programt &dest,
1867 const source_locationt &source_location,
1868 const irep_idt &mode)
1869{
1870 PRECONDITION(!mode.empty());
1871 symbolt &new_symbol = get_fresh_aux_symbol(
1872 type,
1874 "tmp_" + suffix,
1875 source_location,
1876 mode,
1877 symbol_table);
1878
1879 code_frontend_declt decl(new_symbol.symbol_expr());
1880 decl.add_source_location()=source_location;
1881 convert_frontend_decl(decl, dest, mode);
1882
1883 return new_symbol;
1884}
1885
1887 exprt &expr,
1888 const std::string &suffix,
1889 goto_programt &dest,
1890 const irep_idt &mode)
1891{
1892 const source_locationt source_location=expr.find_source_location();
1893
1894 symbolt &new_symbol =
1895 new_tmp_symbol(expr.type(), suffix, dest, source_location, mode);
1896
1897 code_assignt assignment;
1898 assignment.lhs()=new_symbol.symbol_expr();
1899 assignment.rhs()=expr;
1900 assignment.add_source_location()=source_location;
1901
1902 convert(assignment, dest, mode);
1903
1904 expr=new_symbol.symbol_expr();
1905}
1906
1908 const codet &code,
1909 symbol_table_baset &symbol_table,
1910 goto_programt &dest,
1911 message_handlert &message_handler,
1912 const irep_idt &mode)
1913{
1915 symbol_table_buildert::wrap(symbol_table);
1917 goto_convert.goto_convert(code, dest, mode);
1918}
1919
1921 symbol_table_baset &symbol_table,
1922 goto_programt &dest,
1923 message_handlert &message_handler)
1924{
1925 // find main symbol
1926 const symbol_table_baset::symbolst::const_iterator s_it =
1927 symbol_table.symbols.find("main");
1928
1930 s_it != symbol_table.symbols.end(), "failed to find main symbol");
1931
1932 const symbolt &symbol=s_it->second;
1933
1935 to_code(symbol.value), symbol_table, dest, message_handler, symbol.mode);
1936}
1937
1953 const code_blockt &thread_body,
1954 goto_programt &dest,
1955 const irep_idt &mode)
1956{
1957 goto_programt preamble, body, postamble;
1958
1960 convert(thread_body, body, mode);
1961
1963 static_cast<const codet &>(get_nil_irep()),
1964 thread_body.source_location(),
1965 END_THREAD,
1966 nil_exprt(),
1967 {}));
1969
1971 static_cast<const codet &>(get_nil_irep()),
1972 thread_body.source_location(),
1974 nil_exprt(),
1975 {c}));
1976 preamble.add(goto_programt::make_goto(z, thread_body.source_location()));
1977
1978 dest.destructive_append(preamble);
1979 dest.destructive_append(body);
1980 dest.destructive_append(postamble);
1981}
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
static exprt guard(const exprt::operandst &guards, exprt cond)
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
Operator to return the address of an object.
virtual void clear()
Reset the abstract state.
Definition ai.h:266
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Result of an attempt to find ancestor information about two nodes.
Boolean AND.
Definition std_expr.h:2071
A base class for binary expressions.
Definition std_expr.h:583
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
The Boolean type.
Definition std_types.h:36
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition std_code.h:270
const exprt & assertion() const
Definition std_code.h:276
A goto_instruction_codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
Definition std_code.h:217
const exprt & assumption() const
Definition std_code.h:223
A codet representing sequential composition of program statements.
Definition std_code.h:130
code_operandst & statements()
Definition std_code.h:138
source_locationt end_location() const
Definition std_code.h:187
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
A goto_instruction_codet representing the removal of a local variable going out of scope.
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
const exprt & expression() const
Definition std_code.h:1401
codet representation of a for statement.
Definition std_code.h:734
const exprt & cond() const
Definition std_code.h:759
const exprt & iter() const
Definition std_code.h:769
const codet & body() const
Definition std_code.h:779
const exprt & init() const
Definition std_code.h:749
A codet representing the declaration of a local variable.
Definition std_code.h:347
const irep_idt & get_identifier() const
Definition std_code.h:364
codet representation of a "return from a function" statement.
Definition std_code.h:893
const exprt & return_value() const
Definition std_code.h:903
bool has_return_value() const
Definition std_code.h:913
goto_instruction_codet representation of a function call statement.
codet representation of a switch-case, i.e. a case statement within a switch.
Definition std_code.h:1097
const exprt & upper() const
upper bound of range
Definition std_code.h:1119
const exprt & lower() const
lower bound of range
Definition std_code.h:1107
codet & code()
the statement to be executed when the case applies
Definition std_code.h:1131
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
std::vector< exception_list_entryt > exception_listt
Definition std_code.h:1849
codet representation of a switch-case, i.e. a case statement within a switch.
Definition std_code.h:1023
const exprt & case_op() const
Definition std_code.h:1040
bool is_default() const
Definition std_code.h:1030
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
codet representing a while statement.
Definition std_code.h:610
const exprt & cond() const
Definition std_code.h:617
const codet & body() const
Definition std_code.h:627
Data structure for representing an arbitrary statement in a program.
exprt & 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
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:147
std::vector< exprt > operandst
Definition expr.h:58
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
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
void convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode)
void convert_assume(const code_assumet &code, goto_programt &dest, const irep_idt &mode)
symbol_table_baset & symbol_table
void convert_expression(const code_expressiont &code, goto_programt &dest, const irep_idt &mode)
void convert_while(const code_whilet &code, goto_programt &dest, const irep_idt &mode)
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
void convert_gcc_computed_goto(const codet &code, goto_programt &dest)
void goto_convert_rec(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_CPROVER_throw(const codet &code, goto_programt &dest, const irep_idt &mode)
void optimize_guarded_gotos(goto_programt &dest)
Rewrite "if(x) goto z; goto y; z:" into "if(!x) goto y;" This only works if the "goto y" is not a bra...
void convert_atomic_begin(const codet &code, goto_programt &dest)
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_msc_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_gcc_switch_case_range(const code_gcc_switch_case_ranget &, goto_programt &dest, const irep_idt &mode)
virtual void do_function_call(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
irep_idt get_string_constant(const exprt &expr)
void convert_label(const code_labelt &code, goto_programt &dest, const irep_idt &mode)
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
exprt get_constant(const exprt &expr)
void convert_start_thread(const codet &code, goto_programt &dest)
void finish_gotos(goto_programt &dest, const irep_idt &mode)
void generate_conditional_branch(const exprt &guard, goto_programt::targett target_true, goto_programt::targett target_false, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) goto target_true; else goto target_false;
void convert_ifthenelse(const code_ifthenelset &code, goto_programt &dest, const irep_idt &mode)
void convert_atomic_end(const codet &code, goto_programt &dest)
std::string tmp_symbol_prefix
void convert_frontend_decl(const code_frontend_declt &, goto_programt &, const irep_idt &mode)
void convert_gcc_local_label(const codet &code, goto_programt &dest)
struct goto_convertt::targetst targets
void convert_break(const code_breakt &code, goto_programt &dest, const irep_idt &mode)
void convert_function_call(const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
void convert_goto(const code_gotot &code, goto_programt &dest)
exprt case_guard(const exprt &value, const caset &case_op)
void convert_CPROVER_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_cpp_delete(const codet &code, goto_programt &dest)
void convert_switch(const code_switcht &code, goto_programt &dest, const irep_idt &mode)
static void collect_operands(const exprt &expr, const irep_idt &id, std::list< exprt > &dest)
void convert_decl_type(const codet &code, goto_programt &dest)
void convert_dowhile(const code_dowhilet &code, goto_programt &dest, const irep_idt &mode)
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
void convert_loop_contracts(const codet &code, goto_programt::targett loop, const irep_idt &mode)
void convert_skip(const codet &code, goto_programt &dest)
void convert_asm(const code_asmt &code, goto_programt &dest)
Definition goto_asm.cpp:14
void convert_switch_case(const code_switch_caset &code, goto_programt &dest, const irep_idt &mode)
void unwind_destructor_stack(const source_locationt &source_location, goto_programt &dest, const irep_idt &mode, optionalt< node_indext > destructor_start_point={}, optionalt< node_indext > destructor_end_point={})
Unwinds the destructor stack and creates destructors for each node between destructor_start_point and...
void convert_msc_try_except(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_continue(const code_continuet &code, goto_programt &dest, const irep_idt &mode)
void convert_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_assert(const code_assertt &code, goto_programt &dest, const irep_idt &mode)
static bool needs_cleaning(const exprt &expr)
Returns 'true' for expressions that may change the program state.
void finish_computed_gotos(goto_programt &dest)
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
void convert_CPROVER_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
exprt::operandst caset
void generate_ifthenelse(const exprt &cond, goto_programt &true_case, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) true_case; else false_case;
static void replace_new_object(const exprt &object, exprt &dest)
void convert_msc_leave(const codet &code, goto_programt &dest, const irep_idt &mode)
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)
void convert_return(const code_frontend_returnt &, goto_programt &dest, const irep_idt &mode)
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
void convert_block(const code_blockt &code, goto_programt &dest, const irep_idt &mode)
void generate_thread_block(const code_blockt &thread_body, goto_programt &dest, const irep_idt &mode)
Generates the necessary goto-instructions to represent a thread-block.
void convert_end_thread(const codet &code, goto_programt &dest)
This class represents an instruction in the GOTO intermediate representation.
void complete_goto(targett _target)
const goto_instruction_codet & code() const
Get the code represented by this instruction.
targetst targets
The list of successor instructions.
static const unsigned nil_target
Uniquely identify an invalid target or location.
const source_locationt & source_location() const
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
instructionst::iterator targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
static instructiont make_other(const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil())
static instructiont make_location(const source_locationt &l)
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
bool empty() const
Is the program empty?
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
The trinary if-then-else operator.
Definition std_expr.h:2323
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:490
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
bool is_not_nil() const
Definition irep.h:380
const irep_idt & id() const
Definition irep.h:396
source_locationt source_location
Definition message.h:247
mstreamt & debug() const
Definition message.h:429
mstreamt & warning() const
Definition message.h:404
mstreamt & result() const
Definition message.h:409
static eomt eom
Definition message.h:297
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The NIL expression.
Definition std_expr.h:3026
void set_case_number(const irep_idt &number)
Expression to hold a symbol (variable)
Definition std_expr.h:113
The symbol table base class interface.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Author: Diffblue Ltd.
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
Symbol table entry.
Definition symbol.h:28
bool is_static_lifetime
Definition symbol.h:70
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
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
irep_idt mode
Language mode.
Definition symbol.h:49
The Boolean constant true.
Definition std_expr.h:3008
Semantic type conversion.
Definition std_expr.h:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:314
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
code_function_callt get_destructor(const namespacet &ns, const typet &type)
Destructor Calls.
std::size_t node_indext
bool is_empty(const std::string &s)
#define Forall_operands(it, expr)
Definition expr.h:27
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
static bool has_and_or(const exprt &expr)
if(guard) goto target;
static bool is_size_one(const goto_programt &g)
This is (believed to be) faster than using std::list.size.
static void finish_catch_push_targets(goto_programt &dest)
Populate the CATCH instructions with the targets corresponding to their associated labels.
static bool is_empty(const goto_programt &goto_program)
Program Transformation.
Program Transformation.
const code_function_callt & to_code_function_call(const goto_instruction_codet &code)
const code_assignt & to_code_assign(const goto_instruction_codet &code)
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
goto_program_instruction_typet
The type of an instruction in a GOTO program.
@ ATOMIC_END
@ DEAD
@ ASSIGN
@ ATOMIC_BEGIN
@ CATCH
@ END_THREAD
@ SKIP
@ NO_INSTRUCTION_TYPE
@ START_THREAD
@ DECL
@ OTHER
const irept & get_nil_irep()
Definition irep.cpp:19
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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 is_skip(const goto_programt &body, goto_programt::const_targett it, bool ignore_labels)
Determine whether the instruction is semantically equivalent to a skip (no-op).
Program Transformation.
bool simplify(exprt &expr, 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_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
Definition invariant.h:437
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition std_code.h:1506
const code_breakt & to_code_break(const codet &code)
Definition std_code.h:1203
const code_switch_caset & to_code_switch_case(const codet &code)
Definition std_code.h:1077
const code_gotot & to_code_goto(const codet &code)
Definition std_code.h:875
const code_assertt & to_code_assert(const codet &code)
Definition std_code.h:304
static code_push_catcht & to_code_push_catch(codet &code)
Definition std_code.h:1883
const code_frontend_returnt & to_code_frontend_return(const codet &code)
Definition std_code.h:943
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition std_code.h:1739
const code_dowhilet & to_code_dowhile(const codet &code)
Definition std_code.h:716
const code_assumet & to_code_assume(const codet &code)
Definition std_code.h:251
const code_whilet & to_code_while(const codet &code)
Definition std_code.h:654
const code_labelt & to_code_label(const codet &code)
Definition std_code.h:1004
const code_blockt & to_code_block(const codet &code)
Definition std_code.h:203
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition std_code.h:530
const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)
Definition std_code.h:1161
code_asmt & to_code_asm(codet &code)
Definition std_code.h:1282
const code_fort & to_code_for(const codet &code)
Definition std_code.h:823
const code_switcht & to_code_switch(const codet &code)
Definition std_code.h:592
const code_frontend_declt & to_code_frontend_decl(const codet &code)
Definition std_code.h:429
code_expressiont & to_code_expression(codet &code)
Definition std_code.h:1428
const code_continuet & to_code_continue(const codet &code)
Definition std_code.h:1239
const codet & to_code(const exprt &expr)
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:51
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:660
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2303
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
const string_constantt & to_string_constant(const exprt &expr)