CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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#include "goto_convert_class.h"
14
15#include <util/arith_tools.h>
16#include <util/c_types.h>
17#include <util/cprover_prefix.h>
19#include <util/expr_util.h>
20#include <util/fresh_symbol.h>
21#include <util/pointer_expr.h>
22#include <util/simplify_expr.h>
23#include <util/std_expr.h>
26
28
29#include "destructor.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
105
108 goto_programt &program,
109 std::unordered_map<irep_idt, symbolt, irep_id_hash> &label_flags,
110 const build_declaration_hops_inputst &inputs)
111{
112 // In the case of a goto jumping into a scope, the declarations (but not the
113 // initialisations) need to be executed. This function prepares a
114 // transformation from code that looks like -
115 // {
116 // statement_block_a();
117 // if(...)
118 // goto user_label;
119 // statement_block_b();
120 // int x;
121 // x = 0;
122 // statement_block_c();
123 // int y;
124 // y = 0;
125 // statement_block_d();
126 // user_label:
127 // statement_block_e();
128 // }
129 // to code which looks like -
130 // {
131 // __CPROVER_bool __CPROVER_going_to::user_label;
132 // __CPROVER_going_to::user_label = false;
133 // statement_block_a();
134 // if(...)
135 // {
136 // __CPROVER_going_to::user_label = true;
137 // goto scope_x_label;
138 // }
139 // statement_block_b();
140 // scope_x_label:
141 // int x;
142 // if __CPROVER_going_to::user_label goto scope_y_label:
143 // x = 0;
144 // statement_block_c();
145 // scope_y_label:
146 // int y;
147 // if __CPROVER_going_to::user_label goto user_label:
148 // y = 0;
149 // statement_block_d();
150 // user_label:
151 // __CPROVER_going_to::user_label = false;
152 // statement_block_e();
153 // }
154 //
155 // The actual insertion of instructions needs to be performed by the caller,
156 // which needs to use the result of this method.
157
159
161
162 const auto flag = [&]() -> symbolt {
163 const auto existing_flag = label_flags.find(inputs.label);
164 if(existing_flag != label_flags.end())
165 return existing_flag->second;
167 inputs.label_instruction->source_location();
168 label_location.set_hide();
170 bool_typet{},
171 CPROVER_PREFIX "going_to",
172 id2string(inputs.label),
174 inputs.mode,
176 label_flags.emplace(inputs.label, new_flag);
177
178 // Create and initialise flag.
179 instructions_to_add.emplace_back(
180 program.instructions.begin(),
182 const auto make_clear_flag = [&]() -> goto_programt::instructiont {
184 new_flag.symbol_expr(), false_exprt{}, label_location);
185 };
186 instructions_to_add.emplace_back(
187 program.instructions.begin(), make_clear_flag());
188
189 // Clear flag on arrival at label.
191 instructions_to_add.emplace_back(
193 return new_flag;
194 }();
195
196 auto goto_instruction = inputs.goto_instruction;
197 {
198 // Set flag before the goto.
199 auto goto_location = goto_instruction->source_location();
200 goto_location.set_hide();
201 auto set_flag = goto_programt::make_assignment(
202 flag.symbol_expr(), true_exprt{}, goto_location);
203 instructions_to_add.emplace_back(goto_instruction, set_flag);
204 }
205
206 auto target = inputs.label_instruction;
207 targets.scope_stack.set_current_node(inputs.label_scope_index);
208 while(targets.scope_stack.get_current_node() > inputs.end_scope_index)
209 {
210 node_indext current_node = targets.scope_stack.get_current_node();
211 auto &declaration = targets.scope_stack.get_declaration(current_node);
212 targets.scope_stack.descend_tree();
213 if(!declaration)
214 continue;
215
216 bool add_if = declaration->accounted_flags.find(flag.name) ==
217 declaration->accounted_flags.end();
218 if(add_if)
219 {
220 auto declaration_location = declaration->instruction->source_location();
221 declaration_location.set_hide();
223 target, flag.symbol_expr(), declaration_location);
224 // this isn't changing any previously existing instruction so we insert
225 // directly rather than going through instructions_to_add
226 program.instructions.insert(
227 std::next(declaration->instruction), std::move(if_goto));
228 declaration->accounted_flags.insert(flag.name);
229 }
230 target = declaration->instruction;
231 }
232
233 // Update the goto so that it goes to the first declaration rather than its
234 // original/final destination.
235 goto_instruction->set_target(target);
236
237 return instructions_to_add;
238}
239
240/******************************************************************* \
241
242Function: goto_convertt::finish_gotos
243
244 Inputs:
245
246 Outputs:
247
248 Purpose:
249
250\*******************************************************************/
251
253{
254 std::unordered_map<irep_idt, symbolt, irep_id_hash> label_flags;
256
257 for(const auto &g_it : targets.gotos)
258 {
259 goto_programt::instructiont &i = *(g_it.first);
260
261 if(i.is_start_thread())
262 {
263 const irep_idt &goto_label = i.code().get(ID_destination);
264 const auto l_it = targets.labels.find(goto_label);
265
266 if(l_it == targets.labels.end())
267 {
269 "goto label \'" + id2string(goto_label) + "\' not found",
270 i.code().find_source_location());
271 }
272
273 i.targets.push_back(l_it->second.first);
274 }
275 else if(i.is_incomplete_goto())
276 {
277 const irep_idt &goto_label = i.code().get(ID_destination);
278 const auto l_it = targets.labels.find(goto_label);
279
280 if(l_it == targets.labels.end())
281 {
283 "goto label \'" + id2string(goto_label) + "\' not found",
284 i.code().find_source_location());
285 }
286
287 i.complete_goto(l_it->second.first);
288
289 node_indext label_target = l_it->second.second;
291
292 // Compare the currently-live variables on the path of the GOTO and label.
293 // We want to work out what variables should die during the jump.
295 targets.scope_stack.get_nearest_common_ancestor_info(
297
298 // If our goto had no variables of note, just skip (0 is the index of the
299 // root of the scope tree)
300 if(goto_target != 0)
301 {
302 // If the goto recorded a destructor stack, execute as much as is
303 // appropriate for however many automatic variables leave scope.
305 debug() << "adding goto-destructor code on jump to '" << goto_label
306 << "'" << eom;
307
311 i.source_location(),
313 mode,
317
318 // This should leave iterators intact, as long as
319 // goto_programt::instructionst is std::list.
320 }
321
322 // Variables *entering* scope on goto, is illegal for C++ non-pod types
323 // and impossible in Java. However, with the exception of Variable Length
324 // Arrays (VLAs), this is valid C and should be taken into account.
325 const bool variables_added_to_scope =
326 intersection_result.right_depth_below_common_ancestor > 0;
328 {
329 // If the goto recorded a destructor stack, execute as much as is
330 // appropriate for however many automatic variables leave scope.
332 debug() << "encountered goto '" << goto_label
333 << "' that enters one or more lexical blocks; "
334 << "adding declaration code on jump to '" << goto_label << "'"
335 << eom;
336
338 inputs.mode = mode;
339 inputs.label = l_it->first;
340 inputs.goto_instruction = g_it.first;
341 inputs.label_instruction = l_it->second.first;
343 inputs.end_scope_index = intersection_result.common_ancestor;
346 build_declaration_hops(dest, label_flags, inputs));
347 }
348 }
349 else
350 {
352 }
353 }
354
355 for(auto r_it = instructions_to_insert.rbegin();
357 ++r_it)
358 {
359 dest.insert_before_swap(r_it->first, r_it->second);
360 }
361
362 targets.gotos.clear();
363}
364
366{
367 for(auto &g_it : targets.computed_gotos)
368 {
371 const exprt pointer = destination.pointer();
372
373 // remember the expression for later checks
374 i =
376
377 // insert huge case-split
378 for(const auto &label : targets.labels)
379 {
381 label_expr.set(ID_identifier, label.first);
382
384
385 goto_program.insert_after(
386 g_it,
388 label.second.first, guard, i.source_location()));
389 }
390 }
391
392 targets.computed_gotos.clear();
393}
394
399{
400 // We cannot use a set of targets, as target iterators
401 // cannot be compared at this stage.
402
403 // collect targets: reset marking
404 for(auto &i : dest.instructions)
406
407 // mark the goto targets
408 unsigned cnt = 0;
409 for(auto &i : dest.instructions)
410 if(i.is_goto())
411 i.get_target()->target_number = (++cnt);
412
413 for(auto it = dest.instructions.begin(); it != dest.instructions.end(); it++)
414 {
415 if(!it->is_goto())
416 continue;
417
418 auto it_goto_y = std::next(it);
419
420 if(
421 it_goto_y == dest.instructions.end() || !it_goto_y->is_goto() ||
422 !it_goto_y->condition().is_true() || it_goto_y->is_target())
423 {
424 continue;
425 }
426
427 auto it_z = std::next(it_goto_y);
428
429 if(it_z == dest.instructions.end())
430 continue;
431
432 // cannot compare iterators, so compare target number instead
433 if(it->get_target()->target_number == it_z->target_number)
434 {
436 it->condition().find(ID_C_spec_assigns).is_nil() &&
437 it->condition().find(ID_C_spec_loop_invariant).is_nil() &&
438 it->condition().find(ID_C_spec_decreases).is_nil(),
439 "no loop invariant expected");
440 irept y_assigns = it_goto_y->condition().find(ID_C_spec_assigns);
442 it_goto_y->condition().find(ID_C_spec_loop_invariant);
443 irept y_decreases = it_goto_y->condition().find(ID_C_spec_decreases);
444
445 it->set_target(it_goto_y->get_target());
446 exprt updated_condition = boolean_negate(it->condition());
447 if(y_assigns.is_not_nil())
449 if(y_loop_invariant.is_not_nil())
451 if(y_decreases.is_not_nil())
453 it->condition_nonconst() = updated_condition;
454 it_goto_y->turn_into_skip();
455 }
456 }
457}
458
460 const codet &code,
461 goto_programt &dest,
462 const irep_idt &mode)
463{
464 goto_convert_rec(code, dest, mode);
465}
466
468 const codet &code,
469 goto_programt &dest,
470 const irep_idt &mode)
471{
472 convert(code, dest, mode);
473
474 finish_gotos(dest, mode);
478}
479
481 const codet &code,
483 goto_programt &dest)
484{
486 code, code.source_location(), type, nil_exprt(), {}));
487}
488
490 const code_labelt &code,
491 goto_programt &dest,
492 const irep_idt &mode)
493{
494 // grab the label
495 const irep_idt &label = code.get_label();
496
498
499 // magic thread creation label.
500 // The "__CPROVER_ASYNC_" signals the start of a sequence of instructions
501 // that can be executed in parallel, i.e, a new thread.
502 if(label.starts_with(CPROVER_PREFIX "ASYNC_"))
503 {
504 // the body of the thread is expected to be
505 // in the operand.
507 to_code_label(code).code().is_not_nil(),
508 "code() in magic thread creation label is null");
509
510 // replace the magic thread creation label with a
511 // thread block (START_THREAD...END_THREAD).
513 thread_body.add(to_code_label(code).code());
514 thread_body.add_source_location() = code.source_location();
516 }
517 else
518 {
519 convert(to_code_label(code).code(), tmp, mode);
520
521 goto_programt::targett target = tmp.instructions.begin();
523
524 targets.labels.insert(
525 {label, {target, targets.scope_stack.get_current_node()}});
526 target->labels.push_front(label);
527 }
528}
529
531{
532 // ignore for now
533}
534
536 const code_switch_caset &code,
537 goto_programt &dest,
538 const irep_idt &mode)
539{
541 convert(code.code(), tmp, mode);
542
543 goto_programt::targett target = tmp.instructions.begin();
545
546 // is a default target given?
547
548 if(code.is_default())
549 targets.set_default(target);
550 else
551 {
552 // cases?
553
554 cases_mapt::iterator cases_entry = targets.cases_map.find(target);
555 if(cases_entry == targets.cases_map.end())
556 {
557 targets.cases.push_back(std::make_pair(target, caset()));
559 targets.cases_map.insert(std::make_pair(target, --targets.cases.end()))
560 .first;
561 }
562
563 exprt::operandst &case_op_dest = cases_entry->second->second;
564 case_op_dest.push_back(code.case_op());
565 // make sure we have a source location in the case operand as otherwise we
566 // end up with a GOTO instruction without a source location
568 case_op_dest.back().source_location().is_not_nil(),
569 "case operand should have a source location",
570 case_op_dest.back().pretty(),
571 code.pretty());
572 }
573}
574
576 const code_gcc_switch_case_ranget &code,
577 goto_programt &dest,
578 const irep_idt &mode)
579{
580 const auto lb = numeric_cast<mp_integer>(code.lower());
581 const auto ub = numeric_cast<mp_integer>(code.upper());
582
584 lb.has_value() && ub.has_value(),
585 "GCC's switch-case-range statement requires constant bounds",
586 code.find_source_location());
587
588 if(*lb > *ub)
589 {
591 warning() << "GCC's switch-case-range statement with empty case range"
592 << eom;
593 }
594
596 convert(code.code(), tmp, mode);
597
598 goto_programt::targett target = tmp.instructions.begin();
600
601 cases_mapt::iterator cases_entry = targets.cases_map.find(target);
602 if(cases_entry == targets.cases_map.end())
603 {
604 targets.cases.push_back({target, caset()});
606 targets.cases_map.insert({target, --targets.cases.end()}).first;
607 }
608
609 // create a skeleton for case_guard
610 cases_entry->second->second.push_back(and_exprt{
613}
614
617 const codet &code,
618 goto_programt &dest,
619 const irep_idt &mode)
620{
621 const irep_idt &statement = code.get_statement();
622
623 if(statement == ID_block)
624 convert_block(to_code_block(code), dest, mode);
625 else if(statement == ID_decl)
627 else if(statement == ID_decl_type)
628 convert_decl_type(code, dest);
629 else if(statement == ID_expression)
630 convert_expression(to_code_expression(code), dest, mode);
631 else if(statement == ID_assign)
632 convert_assign(to_code_assign(code), dest, mode);
633 else if(statement == ID_assert)
634 convert_assert(to_code_assert(code), dest, mode);
635 else if(statement == ID_assume)
636 convert_assume(to_code_assume(code), dest, mode);
637 else if(statement == ID_function_call)
639 else if(statement == ID_label)
640 convert_label(to_code_label(code), dest, mode);
641 else if(statement == ID_gcc_local_label)
642 convert_gcc_local_label(code, dest);
643 else if(statement == ID_switch_case)
644 convert_switch_case(to_code_switch_case(code), dest, mode);
645 else if(statement == ID_gcc_switch_case_range)
647 to_code_gcc_switch_case_range(code), dest, mode);
648 else if(statement == ID_for)
649 convert_for(to_code_for(code), dest, mode);
650 else if(statement == ID_while)
651 convert_while(to_code_while(code), dest, mode);
652 else if(statement == ID_dowhile)
653 convert_dowhile(to_code_dowhile(code), dest, mode);
654 else if(statement == ID_switch)
655 convert_switch(to_code_switch(code), dest, mode);
656 else if(statement == ID_break)
657 convert_break(to_code_break(code), dest, mode);
658 else if(statement == ID_return)
659 convert_return(to_code_frontend_return(code), dest, mode);
660 else if(statement == ID_continue)
661 convert_continue(to_code_continue(code), dest, mode);
662 else if(statement == ID_goto)
663 convert_goto(to_code_goto(code), dest);
664 else if(statement == ID_gcc_computed_goto)
665 convert_gcc_computed_goto(code, dest);
666 else if(statement == ID_skip)
667 convert_skip(code, dest);
668 else if(statement == ID_ifthenelse)
669 convert_ifthenelse(to_code_ifthenelse(code), dest, mode);
670 else if(statement == ID_start_thread)
671 convert_start_thread(code, dest);
672 else if(statement == ID_end_thread)
673 convert_end_thread(code, dest);
674 else if(statement == ID_atomic_begin)
675 convert_atomic_begin(code, dest);
676 else if(statement == ID_atomic_end)
677 convert_atomic_end(code, dest);
678 else if(statement == ID_cpp_delete || statement == "cpp_delete[]")
679 convert_cpp_delete(code, dest);
680 else if(statement == ID_msc_try_except)
681 convert_msc_try_except(code, dest, mode);
682 else if(statement == ID_msc_try_finally)
683 convert_msc_try_finally(code, dest, mode);
684 else if(statement == ID_msc_leave)
685 convert_msc_leave(code, dest, mode);
686 else if(statement == ID_try_catch) // C++ try/catch
687 convert_try_catch(code, dest, mode);
688 else if(statement == ID_CPROVER_try_catch) // CPROVER-homemade
689 convert_CPROVER_try_catch(code, dest, mode);
690 else if(statement == ID_CPROVER_throw) // CPROVER-homemade
691 convert_CPROVER_throw(code, dest, mode);
692 else if(statement == ID_CPROVER_try_finally)
693 convert_CPROVER_try_finally(code, dest, mode);
694 else if(statement == ID_asm)
695 convert_asm(to_code_asm(code), dest);
696 else if(statement == ID_static_assert)
697 {
698 PRECONDITION(code.operands().size() == 2);
699 exprt assertion =
701 simplify(assertion, ns);
703 !assertion.is_false(),
704 "static assertion " + id2string(get_string_constant(code.op1())),
705 code.op0().find_source_location());
706 }
707 else if(statement == ID_dead)
708 copy(code, DEAD, dest);
709 else if(statement == ID_decl_block)
710 {
711 for(const auto &op : code.operands())
712 convert(to_code(op), dest, mode);
713 }
714 else if(
715 statement == ID_push_catch || statement == ID_pop_catch ||
716 statement == ID_exception_landingpad)
717 copy(code, CATCH, dest);
718 else
719 copy(code, OTHER, dest);
720
721 // make sure dest is never empty
722 if(dest.instructions.empty())
723 {
725 }
726}
727
729 const code_blockt &code,
730 goto_programt &dest,
731 const irep_idt &mode)
732{
733 const source_locationt &end_location = code.end_location();
734
735 // this saves the index of the destructor stack
736 node_indext old_stack_top = targets.scope_stack.get_current_node();
737
738 // now convert block
739 for(const auto &b_code : code.statements())
740 convert(b_code, dest, mode);
741
742 // see if we need to do any destructors -- may have been processed
743 // in a prior break/continue/return already, don't create dead code
744 if(
745 !dest.empty() && dest.instructions.back().is_goto() &&
746 dest.instructions.back().condition().is_true())
747 {
748 // don't do destructors when we are unreachable
749 }
750 else
751 unwind_destructor_stack(end_location, dest, mode, old_stack_top);
752
753 // Set the current node of our destructor stack back to before the block.
754 targets.scope_stack.set_current_node(old_stack_top);
755}
756
758 const code_expressiont &code,
759 goto_programt &dest,
760 const irep_idt &mode)
761{
762 exprt expr = code.expression();
763
764 if(expr.id() == ID_if)
765 {
766 // We do a special treatment for c?t:f
767 // by compiling to if(c) t; else f;
768 const if_exprt &if_expr = to_if_expr(expr);
770 if_expr.cond(),
771 code_expressiont(if_expr.true_case()),
772 code_expressiont(if_expr.false_case()));
773 tmp_code.add_source_location() = expr.source_location();
774 tmp_code.then_case().add_source_location() = expr.source_location();
775 tmp_code.else_case().add_source_location() = expr.source_location();
776 convert_ifthenelse(tmp_code, dest, mode);
777 }
778 else
779 {
780 // result _not_ used
781 clean_expr_resultt side_effects = clean_expr(expr, mode, false);
782 dest.destructive_append(side_effects.side_effects);
783
784 // Any residual expression?
785 // We keep it to add checks later.
786 if(expr.is_not_nil())
787 {
788 codet tmp = code;
789 tmp.op0() = expr;
790 tmp.add_source_location() = expr.source_location();
791 copy(tmp, OTHER, dest);
792 }
793
794 destruct_locals(side_effects.temporaries, dest, ns);
795 }
796}
797
799 const code_frontend_declt &code,
800 goto_programt &dest,
801 const irep_idt &mode)
802{
803 const irep_idt &identifier = code.get_identifier();
804
805 const symbolt &symbol = ns.lookup(identifier);
806
807 if(symbol.is_static_lifetime || symbol.type.id() == ID_code)
808 return; // this is a SKIP!
809
811 if(code.operands().size() == 1)
812 {
813 copy(code, DECL, dest);
814 return std::prev(dest.instructions.end());
815 }
816
817 exprt initializer = code.op1();
818
819 codet tmp = code;
820 tmp.operands().resize(1);
821 // hide this declaration-without-initializer step in the goto trace
822 tmp.add_source_location().set_hide();
823
824 // Break up into decl and assignment.
825 // Decl must be visible before initializer.
826 copy(tmp, DECL, dest);
827 const auto declaration_iterator = std::prev(dest.instructions.end());
828
829 auto initializer_location = initializer.find_source_location();
830 clean_expr_resultt side_effects = clean_expr(initializer, mode);
831 dest.destructive_append(side_effects.side_effects);
832
833 if(initializer.is_not_nil())
834 {
835 code_assignt assign(code.op0(), initializer);
837
838 convert_assign(assign, dest, mode);
839 }
840
841 destruct_locals(side_effects.temporaries, dest, ns);
842
844 }();
845
846 // now create a 'dead' instruction -- will be added after the
847 // destructor created below as unwind_destructor_stack pops off the
848 // top of the destructor stack
849 const symbol_exprt symbol_expr(symbol.name, symbol.type);
850
851 {
852 code_deadt code_dead(symbol_expr);
853
854 targets.scope_stack.add(code_dead, {declaration_iterator});
855 }
856
857 // do destructor
858 code_function_callt destructor = get_destructor(ns, symbol.type);
859
860 if(destructor.is_not_nil())
861 {
862 // add "this"
863 address_of_exprt this_expr(symbol_expr, pointer_type(symbol.type));
864 destructor.arguments().push_back(this_expr);
865
866 targets.scope_stack.add(destructor, {});
867 }
868}
869
871{
872 // we remove these
873}
874
876 const code_assignt &code,
877 goto_programt &dest,
878 const irep_idt &mode)
879{
880 exprt lhs = code.lhs(), rhs = code.rhs();
881
882 clean_expr_resultt side_effects = clean_expr(lhs, mode);
883 dest.destructive_append(side_effects.side_effects);
884
885 if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_function_call)
886 {
888
890 rhs.operands().size() == 2,
891 "function_call sideeffect takes two operands",
892 rhs.find_source_location());
893
894 Forall_operands(it, rhs)
895 {
896 side_effects.add(clean_expr(*it, mode));
897 dest.destructive_append(side_effects.side_effects);
898 }
899
901 lhs,
902 rhs_function_call.function(),
903 rhs_function_call.arguments(),
904 dest,
905 mode);
906 }
907 else if(
908 rhs.id() == ID_side_effect && (rhs.get(ID_statement) == ID_cpp_new ||
909 rhs.get(ID_statement) == ID_cpp_new_array))
910 {
911 Forall_operands(it, rhs)
912 {
913 side_effects.add(clean_expr(*it, mode));
914 dest.destructive_append(side_effects.side_effects);
915 }
916
917 // TODO: This should be done in a separate pass
918 do_cpp_new(lhs, to_side_effect_expr(rhs), dest);
919 }
920 else if(
921 rhs.id() == ID_side_effect &&
922 (rhs.get(ID_statement) == ID_assign ||
923 rhs.get(ID_statement) == ID_postincrement ||
924 rhs.get(ID_statement) == ID_preincrement ||
927 {
928 // handle above side effects
929 side_effects.add(clean_expr(rhs, mode));
930 dest.destructive_append(side_effects.side_effects);
931
933 new_assign.lhs() = lhs;
934 new_assign.rhs() = rhs;
935
936 copy(new_assign, ASSIGN, dest);
937 }
938 else if(rhs.id() == ID_side_effect)
939 {
940 // preserve side effects that will be handled at later stages,
941 // such as allocate, new operators of other languages, e.g. java, etc
942 Forall_operands(it, rhs)
943 {
944 side_effects.add(clean_expr(*it, mode));
945 dest.destructive_append(side_effects.side_effects);
946 }
947
949 new_assign.lhs() = lhs;
950 new_assign.rhs() = rhs;
951
952 copy(new_assign, ASSIGN, dest);
953 }
954 else
955 {
956 // do everything else
957 side_effects.add(clean_expr(rhs, mode));
958 dest.destructive_append(side_effects.side_effects);
959
961 new_assign.lhs() = lhs;
962 new_assign.rhs() = rhs;
963
964 copy(new_assign, ASSIGN, dest);
965 }
966
967 destruct_locals(side_effects.temporaries, dest, ns);
968}
969
971{
973 code.operands().size() == 1,
974 "cpp_delete statement takes one operand",
975 code.find_source_location());
976
977 exprt tmp_op = code.op0();
978
980 dest.destructive_append(side_effects.side_effects);
981
982 // we call the destructor, and then free
983 const exprt &destructor =
984 static_cast<const exprt &>(code.find(ID_destructor));
985
987
989 delete_identifier = "__delete_array";
990 else if(code.get_statement() == ID_cpp_delete)
991 delete_identifier = "__delete";
992 else
994
995 if(destructor.is_not_nil())
996 {
998 {
999 // build loop
1000 }
1001 else if(code.get_statement() == ID_cpp_delete)
1002 {
1003 // just one object
1005
1006 codet tmp_code = to_code(destructor);
1008 convert(tmp_code, dest, ID_cpp);
1009 }
1010 else
1012 }
1013
1014 // now do "free"
1016
1018 to_code_type(delete_symbol.type()).parameters().size() == 1,
1019 "delete statement takes 1 parameter");
1020
1021 typet arg_type =
1022 to_code_type(delete_symbol.type()).parameters().front().type();
1023
1026 delete_call.add_source_location() = code.source_location();
1027
1028 convert(delete_call, dest, ID_cpp);
1029
1030 destruct_locals(side_effects.temporaries, dest, ns);
1031}
1032
1034 const code_assertt &code,
1035 goto_programt &dest,
1036 const irep_idt &mode)
1037{
1038 exprt cond = code.assertion();
1039
1040 clean_expr_resultt side_effects = clean_expr(cond, mode);
1041 dest.destructive_append(side_effects.side_effects);
1042
1044 annotated_location.set("user-provided", true);
1046
1047 destruct_locals(side_effects.temporaries, dest, ns);
1048}
1049
1051{
1053 code, code.source_location(), SKIP, nil_exprt(), {}));
1054}
1055
1057 const code_assumet &code,
1058 goto_programt &dest,
1059 const irep_idt &mode)
1060{
1061 exprt op = code.assumption();
1062
1063 clean_expr_resultt side_effects = clean_expr(op, mode);
1064 dest.destructive_append(side_effects.side_effects);
1065
1067
1068 destruct_locals(side_effects.temporaries, dest, ns);
1069}
1070
1072 const codet &code,
1074{
1075 auto assigns = static_cast<const unary_exprt &>(code.find(ID_C_spec_assigns));
1076 if(assigns.is_not_nil())
1077 {
1078 PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
1079 loop->condition_nonconst().add(ID_C_spec_assigns).swap(assigns.op());
1080 }
1081
1082 auto invariant =
1083 static_cast<const exprt &>(code.find(ID_C_spec_loop_invariant));
1084 if(!invariant.is_nil())
1085 {
1086 PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
1087 loop->condition_nonconst().add(ID_C_spec_loop_invariant).swap(invariant);
1088 }
1089
1090 auto decreases_clause =
1091 static_cast<const exprt &>(code.find(ID_C_spec_decreases));
1092 if(!decreases_clause.is_nil())
1093 {
1094 PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
1095 loop->condition_nonconst().add(ID_C_spec_decreases).swap(decreases_clause);
1096 }
1097}
1098
1100 const code_fort &code,
1101 goto_programt &dest,
1102 const irep_idt &mode)
1103{
1104 // turn for(A; c; B) { P } into
1105 // A; while(c) { P; B; }
1106 //-----------------------------
1107 // A;
1108 // u: sideeffects in c
1109 // v: if(!c) goto Z;
1110 // cleanup-loop;
1111 // w: P;
1112 // x: B; <-- continue target
1113 // y: goto u;
1114 // Z: cleanup-out;
1115 // z: ; <-- break target
1116
1117 // A;
1118 if(code.init().is_not_nil())
1119 convert(to_code(code.init()), dest, mode);
1120
1121 exprt cond = code.cond();
1122
1123 clean_expr_resultt side_effects = clean_expr(cond, mode);
1124
1125 // save break/continue targets
1127
1128 // do the u label
1129 goto_programt::targett u = side_effects.side_effects.instructions.begin();
1130
1131 // do the v label
1134 destruct_locals(side_effects.temporaries, tmp_v, ns);
1135
1136 // do the z and Z labels
1138 destruct_locals(side_effects.temporaries, tmp_z, ns);
1141 goto_programt::targett Z = tmp_z.instructions.begin();
1142
1143 // do the x label
1145
1146 if(code.iter().is_nil())
1147 {
1149 }
1150 else
1151 {
1152 exprt tmp_B = code.iter();
1153
1155 tmp_x.destructive_append(side_effects_iter.side_effects);
1157
1158 if(tmp_x.instructions.empty())
1160 }
1161
1162 // optimize the v label
1163 if(side_effects.side_effects.instructions.empty())
1164 u = v;
1165
1166 // set the targets
1167 targets.set_break(z);
1168 targets.set_continue(tmp_x.instructions.begin());
1169
1170 // v: if(!c) goto Z;
1171 *v =
1173
1174 // do the w label
1176 convert(code.body(), tmp_w, mode);
1177
1178 // y: goto u;
1182
1183 // assigns clause, loop invariant and decreases clause
1185
1186 dest.destructive_append(side_effects.side_effects);
1192
1193 // restore break/continue
1194 old_targets.restore(targets);
1195}
1196
1198 const code_whilet &code,
1199 goto_programt &dest,
1200 const irep_idt &mode)
1201{
1202 const exprt &cond = code.cond();
1203 const source_locationt &source_location = code.source_location();
1204
1205 // while(c) P;
1206 //--------------------
1207 // v: sideeffects in c
1208 // if(!c) goto z;
1209 // x: P;
1210 // y: goto v; <-- continue target
1211 // z: ; <-- break target
1212
1213 // save break/continue targets
1215
1216 // do the z label
1219 tmp_z.add(goto_programt::make_skip(source_location));
1220
1223 boolean_negate(cond), z, source_location, tmp_branch, mode);
1224
1225 // do the v label
1226 goto_programt::targett v = tmp_branch.instructions.begin();
1227
1228 // y: goto v;
1232
1233 // set the targets
1234 targets.set_break(z);
1235 targets.set_continue(y);
1236
1237 // do the x label
1239 convert(code.body(), tmp_x, mode);
1240
1241 // assigns clause, loop invariant and decreases clause
1243
1248
1249 // restore break/continue
1250 old_targets.restore(targets);
1251}
1252
1254 const code_dowhilet &code,
1255 goto_programt &dest,
1256 const irep_idt &mode)
1257{
1259 code.operands().size() == 2,
1260 "dowhile takes two operands",
1261 code.find_source_location());
1262
1263 // save source location
1264 source_locationt condition_location = code.cond().find_source_location();
1265
1266 exprt cond = code.cond();
1267
1268 clean_expr_resultt side_effects = clean_expr(cond, mode);
1269
1270 // do P while(c);
1271 //--------------------
1272 // w: P;
1273 // x: sideeffects in c <-- continue target
1274 // y: if(!c) goto C;
1275 // cleanup-loop;
1276 // W: goto w;
1277 // C: cleanup-out;
1278 // z: ; <-- break target
1279
1280 // save break/continue targets
1282
1283 // do the y label
1287 destruct_locals(side_effects.temporaries, tmp_y, ns);
1290
1291 // do the z label and C labels
1293 destruct_locals(side_effects.temporaries, tmp_z, ns);
1296 goto_programt::targett C = tmp_z.instructions.begin();
1297
1298 // y: if(!c) goto C;
1299 y->complete_goto(C);
1300
1301 // do the x label
1303 if(side_effects.side_effects.instructions.empty())
1304 x = y;
1305 else
1306 x = side_effects.side_effects.instructions.begin();
1307
1308 // set the targets
1309 targets.set_break(z);
1310 targets.set_continue(x);
1311
1312 // do the w label
1314 convert(code.body(), tmp_w, mode);
1315 goto_programt::targett w = tmp_w.instructions.begin();
1316
1317 // W: goto w;
1318 W->complete_goto(w);
1319
1320 // assigns_clause, loop invariant and decreases clause
1322
1324 dest.destructive_append(side_effects.side_effects);
1327
1328 // restore break/continue targets
1329 old_targets.restore(targets);
1330}
1331
1333 const exprt &value,
1334 const exprt::operandst &case_op)
1335{
1336 PRECONDITION(!case_op.empty());
1337
1339 disjuncts.reserve(case_op.size());
1340
1341 for(const auto &op : case_op)
1342 {
1343 // could be a skeleton generated by convert_gcc_switch_case_range
1344 if(op.id() == ID_and)
1345 {
1347 PRECONDITION(to_binary_expr(and_expr.op0()).op1().is_nil());
1348 PRECONDITION(to_binary_expr(and_expr.op1()).op0().is_nil());
1349 binary_exprt skeleton = and_expr;
1350 to_binary_expr(skeleton.op0()).op1() = value;
1351 to_binary_expr(skeleton.op1()).op0() = value;
1352 disjuncts.push_back(skeleton);
1353 }
1354 else
1355 disjuncts.push_back(equal_exprt(value, op));
1356 }
1357
1358 return disjunction(disjuncts);
1359}
1360
1362 const code_switcht &code,
1363 goto_programt &dest,
1364 const irep_idt &mode)
1365{
1366 // switch(v) {
1367 // case x: Px;
1368 // case y: Py;
1369 // ...
1370 // default: Pd;
1371 // }
1372 // --------------------
1373 // location
1374 // x: if(v==x) goto X;
1375 // y: if(v==y) goto Y;
1376 // goto d;
1377 // X: Px;
1378 // Y: Py;
1379 // d: Pd;
1380 // z: ;
1381
1382 // we first add a 'location' node for the switch statement,
1383 // which would otherwise not be recorded
1385
1386 // get the location of the end of the body, but
1387 // default to location of switch, if none
1389 code.body().get_statement() == ID_block
1390 ? to_code_block(code.body()).end_location()
1391 : code.source_location();
1392
1393 // do the value we switch over
1394 exprt argument = code.value();
1395
1396 clean_expr_resultt side_effects = clean_expr(argument, mode);
1397
1398 // Avoid potential performance penalties caused by evaluating the value
1399 // multiple times (as the below chain-of-ifs does). "needs_cleaning" isn't
1400 // necessarily the right check here, and we may need to introduce a different
1401 // way of identifying the class of non-trivial expressions that warrant
1402 // introduction of a temporary.
1404 {
1405 symbolt &new_symbol = new_tmp_symbol(
1406 argument.type(),
1407 "switch_value",
1408 side_effects.side_effects,
1409 code.source_location(),
1410 mode);
1411
1413 new_symbol.symbol_expr(), argument, code.source_location()};
1414 convert(copy_value, side_effects.side_effects, mode);
1415
1416 argument = new_symbol.symbol_expr();
1417 side_effects.add_temporary(to_symbol_expr(argument).get_identifier());
1418 }
1419
1420 // save break/default/cases targets
1422
1423 // do the z label
1427
1428 // set the new targets -- continue stays as is
1429 targets.set_break(z);
1430 targets.set_default(z);
1431 targets.cases.clear();
1432 targets.cases_map.clear();
1433
1435 convert(code.body(), tmp, mode);
1436
1438
1439 // The case number represents which case this corresponds to in the sequence
1440 // of case statements.
1441 //
1442 // switch (x)
1443 // {
1444 // case 2: // case_number 1
1445 // ...;
1446 // case 3: // case_number 2
1447 // ...;
1448 // case 10: // case_number 3
1449 // ...;
1450 // }
1451 size_t case_number = 1;
1452 for(auto &case_pair : targets.cases)
1453 {
1454 const caset &case_ops = case_pair.second;
1455
1456 if(case_ops.empty())
1457 continue;
1458
1459 exprt guard_expr = case_guard(argument, case_ops);
1460
1461 source_locationt source_location = case_ops.front().find_source_location();
1462 source_location.set_case_number(std::to_string(case_number));
1463 case_number++;
1464
1465 if(side_effects.temporaries.empty())
1466 {
1467 guard_expr.add_source_location() = source_location;
1468
1470 case_pair.first, std::move(guard_expr), source_location));
1471 }
1472 else
1473 {
1474 guard_expr = boolean_negate(guard_expr);
1475 guard_expr.add_source_location() = source_location;
1476
1479 std::move(guard_expr), source_location));
1480 destruct_locals(side_effects.temporaries, tmp_cases, ns);
1482 case_pair.first, true_exprt{}, source_location));
1484 tmp_cases.add(goto_programt::make_skip(source_location));
1485 try_next->complete_goto(next_case);
1486 }
1487 }
1488
1490 targets.default_target, targets.default_target->source_location()));
1491
1492 dest.destructive_append(side_effects.side_effects);
1494 dest.destructive_append(tmp);
1496
1497 // restore old targets
1498 old_targets.restore(targets);
1499}
1500
1502 const code_breakt &code,
1503 goto_programt &dest,
1504 const irep_idt &mode)
1505{
1507 targets.break_set, "break without target", code.find_source_location());
1508
1509 // need to process destructor stack
1511 code.source_location(), dest, mode, targets.break_stack_node);
1512
1513 // add goto
1514 dest.add(
1515 goto_programt::make_goto(targets.break_target, code.source_location()));
1516}
1517
1519 const code_frontend_returnt &code,
1520 goto_programt &dest,
1521 const irep_idt &mode)
1522{
1523 if(!targets.return_set)
1524 {
1526 "return without target", code.find_source_location());
1527 }
1528
1530 code.operands().empty() || code.operands().size() == 1,
1531 "return takes none or one operand",
1532 code.find_source_location());
1533
1534 code_frontend_returnt new_code(code);
1535 clean_expr_resultt side_effects;
1536
1537 if(new_code.has_return_value())
1538 {
1539 bool result_is_used = new_code.return_value().type().id() != ID_empty;
1540
1541 side_effects = clean_expr(new_code.return_value(), mode, result_is_used);
1542 dest.destructive_append(side_effects.side_effects);
1543
1544 // remove void-typed return value
1545 if(!result_is_used)
1546 new_code.return_value().make_nil();
1547 }
1548
1549 if(targets.has_return_value)
1550 {
1552 new_code.has_return_value(),
1553 "function must return value",
1554 new_code.find_source_location());
1555
1556 // Now add a 'set return value' instruction to set the return value.
1558 new_code.return_value(), new_code.source_location()));
1559 destruct_locals(side_effects.temporaries, dest, ns);
1560 }
1561 else
1562 {
1564 !new_code.has_return_value() ||
1565 new_code.return_value().type().id() == ID_empty,
1566 "function must not return value",
1567 code.find_source_location());
1568 }
1569
1570 // Need to process _entire_ destructor stack.
1571 unwind_destructor_stack(code.source_location(), dest, mode);
1572
1573 // add goto to end-of-function
1575 targets.return_target, new_code.source_location()));
1576}
1577
1579 const code_continuet &code,
1580 goto_programt &dest,
1581 const irep_idt &mode)
1582{
1584 targets.continue_set,
1585 "continue without target",
1586 code.find_source_location());
1587
1588 // need to process destructor stack
1590 code.source_location(), dest, mode, targets.continue_stack_node);
1591
1592 // add goto
1593 dest.add(
1594 goto_programt::make_goto(targets.continue_target, code.source_location()));
1595}
1596
1598{
1599 // this instruction will be completed during post-processing
1602
1603 // Loop contracts annotated in GOTO
1604 convert_loop_contracts(code, t);
1605
1606 // remember it to do the target later
1607 targets.gotos.emplace_back(t, targets.scope_stack.get_current_node());
1608}
1609
1611 const codet &code,
1612 goto_programt &dest)
1613{
1614 // this instruction will turn into OTHER during post-processing
1616 code, code.source_location(), NO_INSTRUCTION_TYPE, nil_exprt(), {}));
1617
1618 // remember it to do this later
1619 targets.computed_gotos.push_back(t);
1620}
1621
1623{
1625 code, code.source_location(), START_THREAD, nil_exprt(), {}));
1626
1627 // remember it to do target later
1628 targets.gotos.emplace_back(
1629 start_thread, targets.scope_stack.get_current_node());
1630}
1631
1633{
1635 code.operands().empty(),
1636 "end_thread expects no operands",
1637 code.find_source_location());
1638
1639 copy(code, END_THREAD, dest);
1640}
1641
1643{
1645 code.operands().empty(),
1646 "atomic_begin expects no operands",
1647 code.find_source_location());
1648
1649 copy(code, ATOMIC_BEGIN, dest);
1650}
1651
1653{
1655 code.operands().empty(),
1656 ": atomic_end expects no operands",
1657 code.find_source_location());
1658
1659 copy(code, ATOMIC_END, dest);
1660}
1661
1663 const code_ifthenelset &code,
1664 goto_programt &dest,
1665 const irep_idt &mode)
1666{
1667 DATA_INVARIANT(code.then_case().is_not_nil(), "cannot accept an empty body");
1668
1669 bool has_else = !code.else_case().is_nil();
1670
1671 const source_locationt &source_location = code.source_location();
1672
1673 // We do a bit of special treatment for && in the condition
1674 // in case cleaning would be needed otherwise.
1675 if(
1676 code.cond().id() == ID_and && code.cond().operands().size() == 2 &&
1677 (needs_cleaning(to_binary_expr(code.cond()).op0()) ||
1678 needs_cleaning(to_binary_expr(code.cond()).op1())) &&
1679 !has_else)
1680 {
1681 // if(a && b) XX --> if(a) if(b) XX
1683 to_binary_expr(code.cond()).op1(), code.then_case());
1684 new_if1.add_source_location() = source_location;
1686 to_binary_expr(code.cond()).op0(), std::move(new_if1));
1687 new_if0.add_source_location() = source_location;
1688 return convert_ifthenelse(new_if0, dest, mode);
1689 }
1690
1691 exprt tmp_guard = code.cond();
1692 clean_expr_resultt side_effects = clean_expr(tmp_guard, mode);
1693 dest.destructive_append(side_effects.side_effects);
1694
1695 // convert 'then'-branch
1697 destruct_locals(side_effects.temporaries, tmp_then, ns);
1698 convert(code.then_case(), tmp_then, mode);
1700 code.then_case().get_statement() == ID_block
1701 ? to_code_block(code.then_case()).end_location()
1702 : code.then_case().source_location();
1703
1705 destruct_locals(side_effects.temporaries, tmp_else, ns);
1707
1708 if(has_else)
1709 {
1710 convert(code.else_case(), tmp_else, mode);
1711 else_end_location = code.else_case().get_statement() == ID_block
1712 ? to_code_block(code.else_case()).end_location()
1713 : code.else_case().source_location();
1714 }
1715
1717 tmp_guard,
1718 source_location,
1719 tmp_then,
1721 tmp_else,
1723 dest,
1724 mode);
1725}
1726
1728 const exprt &expr,
1729 const irep_idt &id,
1730 std::list<exprt> &dest)
1731{
1732 if(expr.id() != id)
1733 {
1734 dest.push_back(expr);
1735 }
1736 else
1737 {
1738 // left-to-right is important
1739 for(const auto &op : expr.operands())
1740 collect_operands(op, id, dest);
1741 }
1742}
1743
1747static inline bool is_size_one(const goto_programt &g)
1748{
1749 return (!g.instructions.empty()) &&
1750 ++g.instructions.begin() == g.instructions.end();
1751}
1752
1755 const exprt &guard,
1756 const source_locationt &source_location,
1757 goto_programt &true_case,
1759 goto_programt &false_case,
1761 goto_programt &dest,
1762 const irep_idt &mode)
1763{
1764 if(is_empty(true_case) && is_empty(false_case))
1765 {
1766 // hmpf. Useless branch.
1769 dest.add(goto_programt::make_goto(z, guard, source_location));
1771 return;
1772 }
1773
1774 // do guarded assertions directly
1775 if(
1776 is_size_one(true_case) && true_case.instructions.back().is_assert() &&
1777 true_case.instructions.back().condition().is_false() &&
1778 true_case.instructions.back().labels.empty())
1779 {
1780 // The above conjunction deliberately excludes the instance
1781 // if(some) { label: assert(false); }
1782 true_case.instructions.back().condition_nonconst() = boolean_negate(guard);
1783 dest.destructive_append(true_case);
1784 true_case.instructions.clear();
1785 if(
1786 is_empty(false_case) ||
1787 (is_size_one(false_case) &&
1788 is_skip(false_case, false_case.instructions.begin())))
1789 return;
1790 }
1791
1792 // similarly, do guarded assertions directly
1793 if(
1794 is_size_one(false_case) && false_case.instructions.back().is_assert() &&
1795 false_case.instructions.back().condition().is_false() &&
1796 false_case.instructions.back().labels.empty())
1797 {
1798 // The above conjunction deliberately excludes the instance
1799 // if(some) ... else { label: assert(false); }
1800 false_case.instructions.back().condition_nonconst() = guard;
1801 dest.destructive_append(false_case);
1802 false_case.instructions.clear();
1803 if(
1804 is_empty(true_case) ||
1805 (is_size_one(true_case) &&
1806 is_skip(true_case, true_case.instructions.begin())))
1807 return;
1808 }
1809
1810 // a special case for C libraries that use
1811 // (void)((cond) || (assert(0),0))
1812 if(
1813 is_empty(false_case) && true_case.instructions.size() == 2 &&
1814 true_case.instructions.front().is_assert() &&
1815 simplify_expr(true_case.instructions.front().condition(), ns).is_false() &&
1816 true_case.instructions.front().labels.empty() &&
1817 true_case.instructions.back().is_other() &&
1818 true_case.instructions.back().get_other().get_statement() ==
1819 ID_expression &&
1820 true_case.instructions.back().labels.empty())
1821 {
1822 true_case.instructions.front().condition_nonconst() = boolean_negate(guard);
1823 true_case.instructions.erase(--true_case.instructions.end());
1824 dest.destructive_append(true_case);
1825 true_case.instructions.clear();
1826
1827 return;
1828 }
1829
1830 // Flip around if no 'true' case code.
1831 if(is_empty(true_case))
1832 {
1833 return generate_ifthenelse(
1835 source_location,
1836 false_case,
1838 true_case,
1840 dest,
1841 mode);
1842 }
1843
1844 bool has_else = !is_empty(false_case);
1845
1846 // if(c) P;
1847 //--------------------
1848 // v: if(!c) goto z;
1849 // w: P;
1850 // z: ;
1851
1852 // if(c) P; else Q;
1853 //--------------------
1854 // v: if(!c) goto y;
1855 // w: P;
1856 // x: goto z;
1857 // y: Q;
1858 // z: ;
1859
1860 // do the x label
1864
1865 // do the z label
1869
1870 // y: Q;
1873 if(has_else)
1874 {
1875 tmp_y.swap(false_case);
1876 y = tmp_y.instructions.begin();
1877 }
1878
1879 // v: if(!c) goto z/y;
1882 boolean_negate(guard), has_else ? y : z, source_location, tmp_v, mode);
1883
1884 // w: P;
1886 tmp_w.swap(true_case);
1887
1888 // x: goto z;
1889 CHECK_RETURN(!tmp_w.instructions.empty());
1890 x->complete_goto(z);
1891
1894
1895 // When the `then` branch of a balanced `if` condition ends with a `return` or
1896 // a `goto` statement, it is not necessary to add the `goto z` and `z:` goto
1897 // elements as they are never used.
1898 // This helps for example when using `--cover location` as such command are
1899 // marked unreachable, but are not part of the user-provided code to analyze.
1900 bool then_branch_returns = dest.instructions.rbegin()->is_goto();
1901
1902 if(has_else)
1903 {
1904 // Don't add the `goto` at the end of the `then` branch if not needed
1906 {
1908 }
1910 }
1911
1912 // Don't add the `z` label at the end of the `if` when not needed.
1914 {
1916 }
1917}
1918
1920static bool has_and_or(const exprt &expr)
1921{
1922 for(const auto &op : expr.operands())
1923 {
1924 if(has_and_or(op))
1925 return true;
1926 }
1927
1928 if(expr.id() == ID_and || expr.id() == ID_or)
1929 return true;
1930
1931 return false;
1932}
1933
1935 const exprt &guard,
1937 const source_locationt &source_location,
1938 goto_programt &dest,
1939 const irep_idt &mode)
1940{
1942 {
1943 // if(guard) goto target;
1944 // becomes
1945 // if(guard) goto target; else goto next;
1946 // next: skip;
1947
1950 tmp.add(goto_programt::make_skip(source_location));
1951
1953 guard, target_true, target_false, source_location, dest, mode);
1954
1955 dest.destructive_append(tmp);
1956 }
1957 else
1958 {
1959 // simple branch
1960 exprt cond = guard;
1961 clean_expr_resultt side_effects = clean_expr(cond, mode);
1962 dest.destructive_append(side_effects.side_effects);
1963
1964 dest.add(goto_programt::make_goto(target_true, cond, source_location));
1968 destruct_locals(side_effects.temporaries, dest, ns);
1969 }
1970}
1971
1974 const exprt &guard,
1977 const source_locationt &source_location,
1978 goto_programt &dest,
1979 const irep_idt &mode)
1980{
1981 if(guard.id() == ID_not)
1982 {
1983 // simply swap targets
1985 to_not_expr(guard).op(),
1988 source_location,
1989 dest,
1990 mode);
1991 return;
1992 }
1993
1994 if(guard.id() == ID_and)
1995 {
1996 // turn
1997 // if(a && b) goto target_true; else goto target_false;
1998 // into
1999 // if(!a) goto target_false;
2000 // if(!b) goto target_false;
2001 // goto target_true;
2002
2003 std::list<exprt> op;
2004 collect_operands(guard, guard.id(), op);
2005
2006 for(const auto &expr : op)
2008 boolean_negate(expr), target_false, source_location, dest, mode);
2009
2010 dest.add(goto_programt::make_goto(target_true, source_location));
2011
2012 return;
2013 }
2014 else if(guard.id() == ID_or)
2015 {
2016 // turn
2017 // if(a || b) goto target_true; else goto target_false;
2018 // into
2019 // if(a) goto target_true;
2020 // if(b) goto target_true;
2021 // goto target_false;
2022
2023 std::list<exprt> op;
2024 collect_operands(guard, guard.id(), op);
2025
2026 // true branch(es)
2027 for(const auto &expr : op)
2029 expr, target_true, source_location, dest, mode);
2030
2031 // false branch
2032 dest.add(goto_programt::make_goto(target_false, guard.source_location()));
2033
2034 return;
2035 }
2036
2037 exprt cond = guard;
2038 clean_expr_resultt side_effects = clean_expr(cond, mode);
2039 dest.destructive_append(side_effects.side_effects);
2040
2041 // true branch
2042 dest.add(goto_programt::make_goto(target_true, cond, source_location));
2046
2047 // false branch
2048 dest.add(goto_programt::make_goto(target_false, source_location));
2051}
2052
2054{
2055 if(expr.id() == ID_typecast)
2056 return get_string_constant(to_typecast_expr(expr).op(), value);
2057
2058 if(
2059 expr.id() == ID_address_of &&
2060 to_address_of_expr(expr).object().id() == ID_index)
2061 {
2062 exprt index_op =
2063 get_constant(to_index_expr(to_address_of_expr(expr).object()).array());
2065
2066 if(index_op.id() == ID_string_constant)
2067 {
2068 value = to_string_constant(index_op).value();
2069 return false;
2070 }
2071 else if(index_op.id() == ID_array)
2072 {
2073 std::string result;
2074 for(const auto &op : as_const(index_op).operands())
2075 {
2076 if(op.is_constant())
2077 {
2078 const auto i = numeric_cast<std::size_t>(op);
2079 if(!i.has_value())
2080 return true;
2081
2082 if(i.value() != 0) // to skip terminating 0
2083 result += static_cast<char>(i.value());
2084 }
2085 }
2086
2087 return value = result, false;
2088 }
2089 }
2090
2091 if(expr.id() == ID_string_constant)
2092 {
2093 value = to_string_constant(expr).value();
2094 return false;
2095 }
2096
2097 return true;
2098}
2099
2101{
2103
2104 const bool res = get_string_constant(expr, result);
2106 !res,
2107 "expected string constant",
2108 expr.find_source_location(),
2109 expr.pretty());
2110
2111 return result;
2112}
2113
2115{
2116 if(expr.id() == ID_symbol)
2117 {
2118 const symbolt &symbol = ns.lookup(to_symbol_expr(expr));
2119
2120 return symbol.value;
2121 }
2122 else if(expr.id() == ID_member)
2123 {
2124 auto tmp = to_member_expr(expr);
2125 tmp.compound() = get_constant(tmp.compound());
2126 return std::move(tmp);
2127 }
2128 else if(expr.id() == ID_index)
2129 {
2130 auto tmp = to_index_expr(expr);
2131 tmp.op0() = get_constant(tmp.op0());
2132 tmp.op1() = get_constant(tmp.op1());
2133 return std::move(tmp);
2134 }
2135 else
2136 return expr;
2137}
2138
2140 const typet &type,
2141 const std::string &suffix,
2142 goto_programt &dest,
2143 const source_locationt &source_location,
2144 const irep_idt &mode)
2145{
2146 PRECONDITION(!mode.empty());
2147 symbolt &new_symbol = get_fresh_aux_symbol(
2148 type,
2150 "tmp_" + suffix,
2151 source_location,
2152 mode,
2153 symbol_table);
2154
2155 if(type.id() != ID_code)
2156 {
2157 dest.add(
2158 goto_programt::make_decl(new_symbol.symbol_expr(), source_location));
2159 }
2160
2161 return new_symbol;
2162}
2163
2165 exprt &expr,
2166 const std::string &suffix,
2167 goto_programt &dest,
2168 const irep_idt &mode)
2169{
2170 const source_locationt source_location = expr.find_source_location();
2171
2172 symbolt &new_symbol =
2173 new_tmp_symbol(expr.type(), suffix, dest, source_location, mode);
2174
2175 code_assignt assignment;
2176 assignment.lhs() = new_symbol.symbol_expr();
2177 assignment.rhs() = expr;
2178 assignment.add_source_location() = source_location;
2179
2180 convert(assignment, dest, mode);
2181
2182 expr = new_symbol.symbol_expr();
2183
2184 return to_symbol_expr(expr).get_identifier();
2185}
2186
2188 const codet &code,
2189 symbol_table_baset &symbol_table,
2190 goto_programt &dest,
2191 message_handlert &message_handler,
2192 const irep_idt &mode)
2193{
2195 symbol_table_buildert::wrap(symbol_table);
2197 goto_convert.goto_convert(code, dest, mode);
2198}
2199
2201 symbol_table_baset &symbol_table,
2202 goto_programt &dest,
2203 message_handlert &message_handler)
2204{
2205 // find main symbol
2206 const symbol_table_baset::symbolst::const_iterator s_it =
2207 symbol_table.symbols.find("main");
2208
2210 s_it != symbol_table.symbols.end(), "failed to find main symbol");
2211
2212 const symbolt &symbol = s_it->second;
2213
2215 to_code(symbol.value), symbol_table, dest, message_handler, symbol.mode);
2216}
2217
2233 const code_blockt &thread_body,
2234 goto_programt &dest,
2235 const irep_idt &mode)
2236{
2237 goto_programt preamble, body, postamble;
2238
2240 convert(thread_body, body, mode);
2241
2243 static_cast<const codet &>(get_nil_irep()),
2244 thread_body.source_location(),
2245 END_THREAD,
2246 nil_exprt(),
2247 {}));
2249
2251 static_cast<const codet &>(get_nil_irep()),
2252 thread_body.source_location(),
2254 nil_exprt(),
2255 {c}));
2256 preamble.add(goto_programt::make_goto(z, thread_body.source_location()));
2257
2258 dest.destructive_append(preamble);
2259 dest.destructive_append(body);
2260 dest.destructive_append(postamble);
2261}
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:235
Operator to return the address of an object.
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Result of an attempt to find ancestor information about two nodes.
Definition scope_tree.h:25
Boolean AND.
Definition std_expr.h:2125
A base class for binary expressions.
Definition std_expr.h:638
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
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:133
exprt & op1()
Definition expr.h:136
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:38
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition dstring.h:95
bool empty() const
Definition dstring.h:89
The empty type.
Definition std_types.h:51
Equality.
Definition std_expr.h:1366
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:231
source_locationt & add_source_location()
Definition expr.h:236
The Boolean constant false.
Definition std_expr.h:3199
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_loop_contracts(const codet &code, goto_programt::targett loop)
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 generate_ifthenelse(const exprt &cond, const source_locationt &, goto_programt &true_case, const source_locationt &, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) true_case; else false_case;
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)
void unwind_destructor_stack(const source_locationt &source_location, goto_programt &dest, const irep_idt &mode, std::optional< node_indext > destructor_end_point={}, std::optional< node_indext > destructor_start_point={})
Unwinds the destructor stack and creates destructors for each node between destructor_start_point and...
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 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 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)
irep_idt make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &, 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)
std::list< std::pair< goto_programt::targett, goto_programt::instructiont > > declaration_hop_instrumentationt
exprt::operandst caset
declaration_hop_instrumentationt build_declaration_hops(goto_programt &dest, std::unordered_map< irep_idt, symbolt, irep_id_hash > &label_flags, const build_declaration_hops_inputst &inputs)
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 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)
clean_expr_resultt clean_expr(exprt &expr, const irep_idt &mode, bool result_is_used=true)
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 insert_before_swap(targett target)
Insertion that preserves jumps to "target".
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_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
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_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
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:2497
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
bool is_not_nil() const
Definition irep.h:372
const irep_idt & id() const
Definition irep.h:388
source_locationt source_location
Definition message.h:239
mstreamt & debug() const
Definition message.h:421
mstreamt & warning() const
Definition message.h:396
mstreamt & result() const
Definition message.h:401
static eomt eom
Definition message.h:289
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The NIL expression.
Definition std_expr.h:3208
void set_case_number(const irep_idt &number)
Expression to hold a symbol (variable)
Definition std_expr.h:131
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:3190
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:361
#define CPROVER_PREFIX
code_function_callt get_destructor(const namespacet &ns, const typet &type)
void destruct_locals(const std::list< irep_idt > &vars, goto_programt &dest, const namespacet &ns)
Destructor Calls.
#define Forall_operands(it, expr)
Definition expr.h:27
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:44
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.
std::size_t node_indext
Definition scope_tree.h:19
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_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
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition invariant.h:535
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:71
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2577
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2479
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
const string_constantt & to_string_constant(const exprt &expr)
goto_programt::targett goto_instruction
goto_programt::targett label_instruction
std::list< irep_idt > temporaries
Identifiers of temporaries introduced while cleaning an expression.
void add(clean_expr_resultt &&other)
void add_temporary(const irep_idt &id)
goto_programt side_effects
Statements implementing side effects of the expression that was subject to cleaning.