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>
25#include <util/symbol_table.h>
27
28#include "goto_convert_class.h"
29#include "destructor.h"
30#include "remove_skip.h"
31
32static bool is_empty(const goto_programt &goto_program)
33{
34 forall_goto_program_instructions(it, goto_program)
35 if(!is_skip(goto_program, it))
36 return false;
37
38 return true;
39}
40
44{
45 std::map<irep_idt, goto_programt::targett> label_targets;
46
47 // in the first pass collect the labels and the corresponding targets
49 {
50 if(!it->labels.empty())
51 {
52 for(auto label : it->labels)
53 // record the label and the corresponding target
54 label_targets.insert(std::make_pair(label, it));
55 }
56 }
57
58 // in the second pass set the targets
59 for(auto &instruction : dest.instructions)
60 {
61 if(
62 instruction.is_catch() &&
63 instruction.get_code().get_statement() == ID_push_catch)
64 {
65 // Populate `targets` with a GOTO instruction target per
66 // exception handler if it isn't already populated.
67 // (Java handlers, for example, need this finish step; C++
68 // handlers will already be populated by now)
69
70 if(instruction.targets.empty())
71 {
72 bool handler_added=true;
74 to_code_push_catch(instruction.get_code()).exception_list();
75
76 for(const auto &handler : handler_list)
77 {
78 // some handlers may not have been converted (if there was no
79 // exception to be caught); in such a situation we abort
80 if(label_targets.find(handler.get_label())==label_targets.end())
81 {
82 handler_added=false;
83 break;
84 }
85 }
86
87 if(!handler_added)
88 continue;
89
90 for(const auto &handler : handler_list)
91 instruction.targets.push_back(label_targets.at(handler.get_label()));
92 }
93 }
94 }
95}
96
97/******************************************************************* \
98
99Function: goto_convertt::finish_gotos
100
101 Inputs:
102
103 Outputs:
104
105 Purpose:
106
107\*******************************************************************/
108
110{
111 for(const auto &g_it : targets.gotos)
112 {
114
115 if(i.is_start_thread())
116 {
117 const irep_idt &goto_label = i.get_code().get(ID_destination);
118
119 labelst::const_iterator l_it=
120 targets.labels.find(goto_label);
121
122 if(l_it == targets.labels.end())
123 {
125 "goto label \'" + id2string(goto_label) + "\' not found",
126 i.get_code().find_source_location());
127 }
128
129 i.targets.push_back(l_it->second.first);
130 }
131 else if(i.is_incomplete_goto())
132 {
133 const irep_idt &goto_label = i.get_code().get(ID_destination);
134
135 labelst::const_iterator l_it=targets.labels.find(goto_label);
136
137 if(l_it == targets.labels.end())
138 {
140 "goto label \'" + id2string(goto_label) + "\' not found",
141 i.get_code().find_source_location());
142 }
143
144 i.complete_goto(l_it->second.first);
145
146 node_indext label_target = l_it->second.second;
148
149 // Compare the currently-live variables on the path of the GOTO and label.
150 // We want to work out what variables should die during the jump.
152 targets.destructor_stack.get_nearest_common_ancestor_info(
154
155 bool not_prefix =
156 intersection_result.right_depth_below_common_ancestor != 0;
157
158 // If our goto had no variables of note, just skip
159 if(goto_target != 0)
160 {
161 // If the goto recorded a destructor stack, execute as much as is
162 // appropriate for however many automatic variables leave scope.
163 // We don't currently handle variables *entering* scope, which
164 // is illegal for C++ non-pod types and impossible in Java in any case.
165 if(not_prefix)
166 {
167 debug().source_location = i.source_location();
168 debug() << "encountered goto '" << goto_label
169 << "' that enters one or more lexical blocks; "
170 << "omitting constructors and destructors" << eom;
171 }
172 else
173 {
174 debug().source_location = i.source_location();
175 debug() << "adding goto-destructor code on jump to '" << goto_label
176 << "'" << eom;
177
181 i.source_location(),
183 mode,
186 dest.destructive_insert(g_it.first, destructor_code);
187
188 // This should leave iterators intact, as long as
189 // goto_programt::instructionst is std::list.
190 }
191 }
192 }
193 else
194 {
196 }
197 }
198
199 targets.gotos.clear();
200}
201
203{
204 for(auto &g_it : targets.computed_gotos)
205 {
208 const exprt pointer = destination.pointer();
209
210 // remember the expression for later checks
211 i =
212 goto_programt::make_other(code_expressiont(pointer), i.source_location());
213
214 // insert huge case-split
215 for(const auto &label : targets.labels)
216 {
218 label_expr.set(ID_identifier, label.first);
219
220 const equal_exprt guard(pointer, address_of_exprt(label_expr));
221
222 goto_program.insert_after(
223 g_it,
225 label.second.first, guard, i.source_location()));
226 }
227 }
228
229 targets.computed_gotos.clear();
230}
231
236{
237 // We cannot use a set of targets, as target iterators
238 // cannot be compared at this stage.
239
240 // collect targets: reset marking
241 for(auto &i : dest.instructions)
243
244 // mark the goto targets
245 unsigned cnt = 0;
246 for(const auto &i : dest.instructions)
247 if(i.is_goto())
248 i.get_target()->target_number = (++cnt);
249
250 for(auto it = dest.instructions.begin(); it != dest.instructions.end(); it++)
251 {
252 if(!it->is_goto())
253 continue;
254
255 auto it_goto_y = std::next(it);
256
257 if(
258 it_goto_y == dest.instructions.end() || !it_goto_y->is_goto() ||
259 !it_goto_y->get_condition().is_true() || it_goto_y->is_target())
260 {
261 continue;
262 }
263
264 auto it_z = std::next(it_goto_y);
265
266 if(it_z == dest.instructions.end())
267 continue;
268
269 // cannot compare iterators, so compare target number instead
270 if(it->get_target()->target_number == it_z->target_number)
271 {
272 it->set_target(it_goto_y->get_target());
273 it->condition_nonconst() = boolean_negate(it->condition());
274 it_goto_y->turn_into_skip();
275 }
276 }
277}
278
280 const codet &code,
282 const irep_idt &mode)
283{
284 goto_convert_rec(code, dest, mode);
285}
286
288 const codet &code,
290 const irep_idt &mode)
291{
292 convert(code, dest, mode);
293
294 finish_gotos(dest, mode);
298}
299
301 const codet &code,
304{
306 code, code.source_location(), type, nil_exprt(), {}));
307}
308
310 const code_labelt &code,
312 const irep_idt &mode)
313{
314 // grab the label
315 const irep_idt &label=code.get_label();
316
318
319 // magic thread creation label.
320 // The "__CPROVER_ASYNC_" signals the start of a sequence of instructions
321 // that can be executed in parallel, i.e, a new thread.
322 if(has_prefix(id2string(label), CPROVER_PREFIX "ASYNC_"))
323 {
324 // the body of the thread is expected to be
325 // in the operand.
327 to_code_label(code).code().is_not_nil(),
328 "code() in magic thread creation label is null");
329
330 // replace the magic thread creation label with a
331 // thread block (START_THREAD...END_THREAD).
333 thread_body.add(to_code_label(code).code());
334 thread_body.add_source_location()=code.source_location();
336 }
337 else
338 {
339 convert(to_code_label(code).code(), tmp, mode);
340
341 goto_programt::targett target=tmp.instructions.begin();
342 dest.destructive_append(tmp);
343
344 targets.labels.insert(
345 {label, {target, targets.destructor_stack.get_current_node()}});
346 target->labels.push_front(label);
347 }
348}
349
351 const codet &,
353{
354 // ignore for now
355}
356
358 const code_switch_caset &code,
360 const irep_idt &mode)
361{
363 convert(code.code(), tmp, mode);
364
365 goto_programt::targett target=tmp.instructions.begin();
366 dest.destructive_append(tmp);
367
368 // is a default target given?
369
370 if(code.is_default())
371 targets.set_default(target);
372 else
373 {
374 // cases?
375
376 cases_mapt::iterator cases_entry=targets.cases_map.find(target);
377 if(cases_entry==targets.cases_map.end())
378 {
379 targets.cases.push_back(std::make_pair(target, caset()));
380 cases_entry=targets.cases_map.insert(std::make_pair(
381 target, --targets.cases.end())).first;
382 }
383
385 case_op_dest.push_back(code.case_op());
386 }
387}
388
390 const code_gcc_switch_case_ranget &code,
392 const irep_idt &mode)
393{
394 const auto lb = numeric_cast<mp_integer>(code.lower());
395 const auto ub = numeric_cast<mp_integer>(code.upper());
396
398 lb.has_value() && ub.has_value(),
399 "GCC's switch-case-range statement requires constant bounds",
400 code.find_source_location());
401
402 if(*lb > *ub)
403 {
405 warning() << "GCC's switch-case-range statement with empty case range"
406 << eom;
407 }
408
410 convert(code.code(), tmp, mode);
411
412 goto_programt::targett target = tmp.instructions.begin();
413 dest.destructive_append(tmp);
414
415 cases_mapt::iterator cases_entry = targets.cases_map.find(target);
416 if(cases_entry == targets.cases_map.end())
417 {
418 targets.cases.push_back({target, caset()});
420 targets.cases_map.insert({target, --targets.cases.end()}).first;
421 }
422
423 // create a skeleton for case_guard
424 cases_entry->second->second.push_back(
427}
428
431 const codet &code,
433 const irep_idt &mode)
434{
435 const irep_idt &statement=code.get_statement();
436
437 if(statement==ID_block)
438 convert_block(to_code_block(code), dest, mode);
439 else if(statement==ID_decl)
441 else if(statement==ID_decl_type)
442 convert_decl_type(code, dest);
443 else if(statement==ID_expression)
445 else if(statement==ID_assign)
446 convert_assign(to_code_assign(code), dest, mode);
447 else if(statement==ID_assert)
448 convert_assert(to_code_assert(code), dest, mode);
449 else if(statement==ID_assume)
450 convert_assume(to_code_assume(code), dest, mode);
451 else if(statement==ID_function_call)
453 else if(statement==ID_label)
454 convert_label(to_code_label(code), dest, mode);
455 else if(statement==ID_gcc_local_label)
457 else if(statement==ID_switch_case)
459 else if(statement==ID_gcc_switch_case_range)
462 else if(statement==ID_for)
463 convert_for(to_code_for(code), dest, mode);
464 else if(statement==ID_while)
465 convert_while(to_code_while(code), dest, mode);
466 else if(statement==ID_dowhile)
468 else if(statement==ID_switch)
469 convert_switch(to_code_switch(code), dest, mode);
470 else if(statement==ID_break)
471 convert_break(to_code_break(code), dest, mode);
472 else if(statement==ID_return)
474 else if(statement==ID_continue)
476 else if(statement==ID_goto)
478 else if(statement==ID_gcc_computed_goto)
480 else if(statement==ID_skip)
481 convert_skip(code, dest);
482 else if(statement==ID_ifthenelse)
484 else if(statement==ID_start_thread)
486 else if(statement==ID_end_thread)
488 else if(statement==ID_atomic_begin)
490 else if(statement==ID_atomic_end)
492 else if(statement==ID_cpp_delete ||
493 statement=="cpp_delete[]")
495 else if(statement==ID_msc_try_except)
496 convert_msc_try_except(code, dest, mode);
497 else if(statement==ID_msc_try_finally)
498 convert_msc_try_finally(code, dest, mode);
499 else if(statement==ID_msc_leave)
500 convert_msc_leave(code, dest, mode);
501 else if(statement==ID_try_catch) // C++ try/catch
502 convert_try_catch(code, dest, mode);
503 else if(statement==ID_CPROVER_try_catch) // CPROVER-homemade
504 convert_CPROVER_try_catch(code, dest, mode);
505 else if(statement==ID_CPROVER_throw) // CPROVER-homemade
506 convert_CPROVER_throw(code, dest, mode);
507 else if(statement==ID_CPROVER_try_finally)
509 else if(statement==ID_asm)
511 else if(statement==ID_static_assert)
512 {
513 PRECONDITION(code.operands().size() == 2);
514 exprt assertion =
516 simplify(assertion, ns);
518 !assertion.is_false(),
519 "static assertion " + id2string(get_string_constant(code.op1())),
520 code.op0().find_source_location());
521 }
522 else if(statement==ID_dead)
523 copy(code, DEAD, dest);
524 else if(statement==ID_decl_block)
525 {
526 forall_operands(it, code)
527 convert(to_code(*it), dest, mode);
528 }
529 else if(statement==ID_push_catch ||
530 statement==ID_pop_catch ||
531 statement==ID_exception_landingpad)
532 copy(code, CATCH, dest);
533 else
534 copy(code, OTHER, dest);
535
536 // make sure dest is never empty
537 if(dest.instructions.empty())
538 {
540 }
541}
542
544 const code_blockt &code,
546 const irep_idt &mode)
547{
548 const source_locationt &end_location=code.end_location();
549
550 // this saves the index of the destructor stack
552 targets.destructor_stack.get_current_node();
553
554 // now convert block
555 for(const auto &b_code : code.statements())
556 convert(b_code, dest, mode);
557
558 // see if we need to do any destructors -- may have been processed
559 // in a prior break/continue/return already, don't create dead code
560 if(
561 !dest.empty() && dest.instructions.back().is_goto() &&
562 dest.instructions.back().get_condition().is_true())
563 {
564 // don't do destructors when we are unreachable
565 }
566 else
567 unwind_destructor_stack(end_location, dest, mode, old_stack_top);
568
569 // Set the current node of our destructor stack back to before the block.
570 targets.destructor_stack.set_current_node(old_stack_top);
571}
572
574 const code_expressiont &code,
576 const irep_idt &mode)
577{
578 exprt expr = code.expression();
579
580 if(expr.id()==ID_if)
581 {
582 // We do a special treatment for c?t:f
583 // by compiling to if(c) t; else f;
584 const if_exprt &if_expr=to_if_expr(expr);
586 if_expr.cond(),
587 code_expressiont(if_expr.true_case()),
588 code_expressiont(if_expr.false_case()));
589 tmp_code.add_source_location()=expr.source_location();
590 tmp_code.then_case().add_source_location()=expr.source_location();
591 tmp_code.else_case().add_source_location()=expr.source_location();
593 }
594 else
595 {
596 clean_expr(expr, dest, mode, false); // result _not_ used
597
598 // Any residual expression?
599 // We keep it to add checks later.
600 if(expr.is_not_nil())
601 {
602 codet tmp=code;
603 tmp.op0()=expr;
604 tmp.add_source_location()=expr.source_location();
605 copy(tmp, OTHER, dest);
606 }
607 }
608}
609
611 const code_frontend_declt &code,
613 const irep_idt &mode)
614{
615 const irep_idt &identifier = code.get_identifier();
616
617 const symbolt &symbol = ns.lookup(identifier);
618
619 if(symbol.is_static_lifetime ||
620 symbol.type.id()==ID_code)
621 return; // this is a SKIP!
622
623 if(code.operands().size()==1)
624 {
625 copy(code, DECL, dest);
626 }
627 else
628 {
629 // this is expected to go away
630 exprt initializer;
631
632 codet tmp=code;
633 initializer=code.op1();
634 tmp.operands().resize(1);
635
636 // Break up into decl and assignment.
637 // Decl must be visible before initializer.
638 copy(tmp, DECL, dest);
639
640 clean_expr(initializer, dest, mode);
641
642 if(initializer.is_not_nil())
643 {
644 code_assignt assign(code.op0(), initializer);
645 assign.add_source_location() = tmp.source_location();
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,
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
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
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
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
761 }
762}
763
765 const codet &code,
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
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);
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
824}
825
827 const code_assertt &code,
829 const irep_idt &mode)
830{
831 exprt cond=code.assertion();
832
833 clean_expr(cond, dest, mode);
834
837 t->source_location_nonconst().set(ID_property, ID_assertion);
838 t->source_location_nonconst().set("user-provided", true);
839}
840
842 const codet &code,
844{
846 code, code.source_location(), SKIP, nil_exprt(), {}));
847}
848
850 const code_assumet &code,
852 const irep_idt &mode)
853{
854 exprt op=code.assumption();
855
856 clean_expr(op, dest, mode);
857
859}
860
862 const codet &code,
864 const irep_idt &mode)
865{
866 auto assigns = static_cast<const unary_exprt &>(code.find(ID_C_spec_assigns));
867 if(assigns.is_not_nil())
868 {
869 PRECONDITION(loop->is_goto());
870 loop->guard.add(ID_C_spec_assigns).swap(assigns.op());
871 }
872
873 auto invariant =
874 static_cast<const exprt &>(code.find(ID_C_spec_loop_invariant));
875 if(!invariant.is_nil())
876 {
877 if(has_subexpr(invariant, ID_side_effect))
878 {
880 "Loop invariant is not side-effect free.", code.find_source_location());
881 }
882
883 PRECONDITION(loop->is_goto());
884 loop->condition_nonconst().add(ID_C_spec_loop_invariant).swap(invariant);
885 }
886
887 auto decreases_clause =
888 static_cast<const exprt &>(code.find(ID_C_spec_decreases));
889 if(!decreases_clause.is_nil())
890 {
892 {
894 "Decreases clause is not side-effect free.",
895 code.find_source_location());
896 }
897
898 PRECONDITION(loop->is_goto());
899 loop->condition_nonconst().add(ID_C_spec_decreases).swap(decreases_clause);
900 }
901}
902
904 const code_fort &code,
906 const irep_idt &mode)
907{
908 // turn for(A; c; B) { P } into
909 // A; while(c) { P; B; }
910 //-----------------------------
911 // A;
912 // u: sideeffects in c
913 // v: if(!c) goto z;
914 // w: P;
915 // x: B; <-- continue target
916 // y: goto u;
917 // z: ; <-- break target
918
919 // A;
920 if(code.init().is_not_nil())
921 convert(to_code(code.init()), dest, mode);
922
923 exprt cond=code.cond();
924
926 clean_expr(cond, sideeffects, mode);
927
928 // save break/continue targets
930
931 // do the u label
932 goto_programt::targett u=sideeffects.instructions.begin();
933
934 // do the v label
937
938 // do the z label
942
943 // do the x label
945
946 if(code.iter().is_nil())
947 {
949 }
950 else
951 {
952 exprt tmp_B=code.iter();
953
954 clean_expr(tmp_B, tmp_x, mode, false);
955
956 if(tmp_x.instructions.empty())
958 }
959
960 // optimize the v label
961 if(sideeffects.instructions.empty())
962 u=v;
963
964 // set the targets
965 targets.set_break(z);
966 targets.set_continue(tmp_x.instructions.begin());
967
968 // v: if(!c) goto z;
969 *v =
971
972 // do the w label
974 convert(code.body(), tmp_w, mode);
975
976 // y: goto u;
980
981 // assigns clause, loop invariant and decreases clause
982 convert_loop_contracts(code, y, mode);
983
984 dest.destructive_append(sideeffects);
985 dest.destructive_append(tmp_v);
986 dest.destructive_append(tmp_w);
987 dest.destructive_append(tmp_x);
988 dest.destructive_append(tmp_y);
989 dest.destructive_append(tmp_z);
990
991 // restore break/continue
992 old_targets.restore(targets);
993}
994
996 const code_whilet &code,
998 const irep_idt &mode)
999{
1000 const exprt &cond=code.cond();
1001 const source_locationt &source_location=code.source_location();
1002
1003 // while(c) P;
1004 //--------------------
1005 // v: sideeffects in c
1006 // if(!c) goto z;
1007 // x: P;
1008 // y: goto v; <-- continue target
1009 // z: ; <-- break target
1010
1011 // save break/continue targets
1013
1014 // do the z label
1017 tmp_z.add(goto_programt::make_skip(source_location));
1018
1021 boolean_negate(cond), z, source_location, tmp_branch, mode);
1022
1023 // do the v label
1024 goto_programt::targett v=tmp_branch.instructions.begin();
1025
1026 // y: goto v;
1030
1031 // set the targets
1032 targets.set_break(z);
1033 targets.set_continue(y);
1034
1035 // do the x label
1037 convert(code.body(), tmp_x, mode);
1038
1039 // assigns clause, loop invariant and decreases clause
1040 convert_loop_contracts(code, y, mode);
1041
1042 dest.destructive_append(tmp_branch);
1043 dest.destructive_append(tmp_x);
1044 dest.destructive_append(tmp_y);
1045 dest.destructive_append(tmp_z);
1046
1047 // restore break/continue
1048 old_targets.restore(targets);
1049}
1050
1052 const code_dowhilet &code,
1054 const irep_idt &mode)
1055{
1057 code.operands().size() == 2,
1058 "dowhile takes two operands",
1059 code.find_source_location());
1060
1061 // save source location
1063
1064 exprt cond=code.cond();
1065
1067 clean_expr(cond, sideeffects, mode);
1068
1069 // do P while(c);
1070 //--------------------
1071 // w: P;
1072 // x: sideeffects in c <-- continue target
1073 // y: if(c) goto w;
1074 // z: ; <-- break target
1075
1076 // save break/continue targets
1078
1079 // do the y label
1083
1084 // do the z label
1088
1089 // do the x label
1091 if(sideeffects.instructions.empty())
1092 x=y;
1093 else
1094 x=sideeffects.instructions.begin();
1095
1096 // set the targets
1097 targets.set_break(z);
1098 targets.set_continue(x);
1099
1100 // do the w label
1102 convert(code.body(), tmp_w, mode);
1103 goto_programt::targett w=tmp_w.instructions.begin();
1104
1105 // y: if(c) goto w;
1106 y->complete_goto(w);
1107
1108 // assigns_clause, loop invariant and decreases clause
1109 convert_loop_contracts(code, y, mode);
1110
1111 dest.destructive_append(tmp_w);
1112 dest.destructive_append(sideeffects);
1113 dest.destructive_append(tmp_y);
1114 dest.destructive_append(tmp_z);
1115
1116 // restore break/continue targets
1117 old_targets.restore(targets);
1118}
1119
1121 const exprt &value,
1122 const exprt::operandst &case_op)
1123{
1124 PRECONDITION(!case_op.empty());
1125
1127 disjuncts.reserve(case_op.size());
1128
1129 for(const auto &op : case_op)
1130 {
1131 // could be a skeleton generated by convert_gcc_switch_case_range
1132 if(op.id() == ID_and)
1133 {
1137 binary_exprt skeleton = and_expr;
1138 to_binary_expr(skeleton.op0()).op1() = value;
1139 to_binary_expr(skeleton.op1()).op0() = value;
1140 disjuncts.push_back(skeleton);
1141 }
1142 else
1143 disjuncts.push_back(equal_exprt(value, op));
1144 }
1145
1146 return disjunction(disjuncts);
1147}
1148
1150 const code_switcht &code,
1152 const irep_idt &mode)
1153{
1154 // switch(v) {
1155 // case x: Px;
1156 // case y: Py;
1157 // ...
1158 // default: Pd;
1159 // }
1160 // --------------------
1161 // location
1162 // x: if(v==x) goto X;
1163 // y: if(v==y) goto Y;
1164 // goto d;
1165 // X: Px;
1166 // Y: Py;
1167 // d: Pd;
1168 // z: ;
1169
1170 // we first add a 'location' node for the switch statement,
1171 // which would otherwise not be recorded
1173
1174 // get the location of the end of the body, but
1175 // default to location of switch, if none
1177 code.body().get_statement()==ID_block?
1179 code.source_location();
1180
1181 // do the value we switch over
1182 exprt argument=code.value();
1183
1186
1187 // Avoid potential performance penalties caused by evaluating the value
1188 // multiple times (as the below chain-of-ifs does). "needs_cleaning" isn't
1189 // necessarily the right check here, and we may need to introduce a different
1190 // way of identifying the class of non-trivial expressions that warrant
1191 // introduction of a temporary.
1193 {
1194 symbolt &new_symbol = new_tmp_symbol(
1195 argument.type(),
1196 "switch_value",
1198 code.source_location(),
1199 mode);
1200
1202 new_symbol.symbol_expr(), argument, code.source_location()};
1204
1205 argument = new_symbol.symbol_expr();
1206 }
1207
1208 // save break/default/cases targets
1210
1211 // do the z label
1215
1216 // set the new targets -- continue stays as is
1217 targets.set_break(z);
1218 targets.set_default(z);
1219 targets.cases.clear();
1220 targets.cases_map.clear();
1221
1223 convert(code.body(), tmp, mode);
1224
1226
1227 // The case number represents which case this corresponds to in the sequence
1228 // of case statements.
1229 //
1230 // switch (x)
1231 // {
1232 // case 2: // case_number 1
1233 // ...;
1234 // case 3: // case_number 2
1235 // ...;
1236 // case 10: // case_number 3
1237 // ...;
1238 // }
1239 size_t case_number=1;
1240 for(auto &case_pair : targets.cases)
1241 {
1242 const caset &case_ops=case_pair.second;
1243
1244 if (case_ops.empty())
1245 continue;
1246
1247 exprt guard_expr=case_guard(argument, case_ops);
1248
1249 source_locationt source_location=case_ops.front().find_source_location();
1250 source_location.set_case_number(std::to_string(case_number));
1251 case_number++;
1252 guard_expr.add_source_location()=source_location;
1253
1255 case_pair.first, std::move(guard_expr), source_location));
1256 }
1257
1259 targets.default_target, targets.default_target->source_location()));
1260
1261 dest.destructive_append(sideeffects);
1262 dest.destructive_append(tmp_cases);
1263 dest.destructive_append(tmp);
1264 dest.destructive_append(tmp_z);
1265
1266 // restore old targets
1267 old_targets.restore(targets);
1268}
1269
1271 const code_breakt &code,
1273 const irep_idt &mode)
1274{
1276 targets.break_set, "break without target", code.find_source_location());
1277
1278 // need to process destructor stack
1280 code.source_location(), dest, mode, targets.break_stack_node);
1281
1282 // add goto
1283 dest.add(
1284 goto_programt::make_goto(targets.break_target, code.source_location()));
1285}
1286
1288 const code_frontend_returnt &code,
1290 const irep_idt &mode)
1291{
1292 if(!targets.return_set)
1293 {
1295 "return without target", code.find_source_location());
1296 }
1297
1299 code.operands().empty() || code.operands().size() == 1,
1300 "return takes none or one operand",
1301 code.find_source_location());
1302
1303 code_frontend_returnt new_code(code);
1304
1305 if(new_code.has_return_value())
1306 {
1307 bool result_is_used=
1308 new_code.return_value().type().id()!=ID_empty;
1309
1312 dest.destructive_append(sideeffects);
1313
1314 // remove void-typed return value
1315 if(!result_is_used)
1316 new_code.return_value().make_nil();
1317 }
1318
1319 if(targets.has_return_value)
1320 {
1322 new_code.has_return_value(),
1323 "function must return value",
1324 new_code.find_source_location());
1325
1326 // Now add a 'set return value' instruction to set the return value.
1328 new_code.return_value(), new_code.source_location()));
1329 }
1330 else
1331 {
1333 !new_code.has_return_value() ||
1334 new_code.return_value().type().id() == ID_empty,
1335 "function must not return value",
1336 code.find_source_location());
1337 }
1338
1339 // Need to process _entire_ destructor stack.
1341
1342 // add goto to end-of-function
1344 targets.return_target, new_code.source_location()));
1345}
1346
1348 const code_continuet &code,
1350 const irep_idt &mode)
1351{
1353 targets.continue_set,
1354 "continue without target",
1355 code.find_source_location());
1356
1357 // need to process destructor stack
1359 code.source_location(), dest, mode, targets.continue_stack_node);
1360
1361 // add goto
1362 dest.add(
1363 goto_programt::make_goto(targets.continue_target, code.source_location()));
1364}
1365
1367{
1368 // this instruction will be completed during post-processing
1371
1372 // remember it to do the target later
1373 targets.gotos.emplace_back(t, targets.destructor_stack.get_current_node());
1374}
1375
1377 const codet &code,
1379{
1380 // this instruction will turn into OTHER during post-processing
1382 code, code.source_location(), NO_INSTRUCTION_TYPE, nil_exprt(), {}));
1383
1384 // remember it to do this later
1385 targets.computed_gotos.push_back(t);
1386}
1387
1389 const codet &code,
1391{
1393 code, code.source_location(), START_THREAD, nil_exprt(), {}));
1394
1395 // remember it to do target later
1396 targets.gotos.emplace_back(
1397 start_thread, targets.destructor_stack.get_current_node());
1398}
1399
1401 const codet &code,
1403{
1405 code.operands().empty(),
1406 "end_thread expects no operands",
1407 code.find_source_location());
1408
1409 copy(code, END_THREAD, dest);
1410}
1411
1413 const codet &code,
1415{
1417 code.operands().empty(),
1418 "atomic_begin expects no operands",
1419 code.find_source_location());
1420
1421 copy(code, ATOMIC_BEGIN, dest);
1422}
1423
1425 const codet &code,
1427{
1429 code.operands().empty(),
1430 ": atomic_end expects no operands",
1431 code.find_source_location());
1432
1433 copy(code, ATOMIC_END, dest);
1434}
1435
1437 const code_ifthenelset &code,
1439 const irep_idt &mode)
1440{
1441 DATA_INVARIANT(code.then_case().is_not_nil(), "cannot accept an empty body");
1442
1443 bool has_else=
1444 !code.else_case().is_nil();
1445
1446 const source_locationt &source_location=code.source_location();
1447
1448 // We do a bit of special treatment for && in the condition
1449 // in case cleaning would be needed otherwise.
1450 if(
1451 code.cond().id() == ID_and && code.cond().operands().size() == 2 &&
1452 (needs_cleaning(to_binary_expr(code.cond()).op0()) ||
1453 needs_cleaning(to_binary_expr(code.cond()).op1())) &&
1454 !has_else)
1455 {
1456 // if(a && b) XX --> if(a) if(b) XX
1458 to_binary_expr(code.cond()).op1(), code.then_case());
1459 new_if1.add_source_location() = source_location;
1461 to_binary_expr(code.cond()).op0(), std::move(new_if1));
1462 new_if0.add_source_location() = source_location;
1463 return convert_ifthenelse(new_if0, dest, mode);
1464 }
1465
1466 // convert 'then'-branch
1468 convert(code.then_case(), tmp_then, mode);
1469
1471
1472 if(has_else)
1473 convert(code.else_case(), tmp_else, mode);
1474
1475 exprt tmp_guard=code.cond();
1476 clean_expr(tmp_guard, dest, mode);
1477
1479 tmp_guard, tmp_then, tmp_else, source_location, dest, mode);
1480}
1481
1483 const exprt &expr,
1484 const irep_idt &id,
1485 std::list<exprt> &dest)
1486{
1487 if(expr.id()!=id)
1488 {
1489 dest.push_back(expr);
1490 }
1491 else
1492 {
1493 // left-to-right is important
1494 forall_operands(it, expr)
1495 collect_operands(*it, id, dest);
1496 }
1497}
1498
1502static inline bool is_size_one(const goto_programt &g)
1503{
1504 return (!g.instructions.empty()) &&
1505 ++g.instructions.begin()==g.instructions.end();
1506}
1507
1510 const exprt &guard,
1511 goto_programt &true_case,
1512 goto_programt &false_case,
1513 const source_locationt &source_location,
1515 const irep_idt &mode)
1516{
1517 if(is_empty(true_case) &&
1518 is_empty(false_case))
1519 {
1520 // hmpf. Useless branch.
1523 dest.add(goto_programt::make_goto(z, guard, source_location));
1524 dest.destructive_append(tmp_z);
1525 return;
1526 }
1527
1528 // do guarded assertions directly
1529 if(
1530 is_size_one(true_case) && true_case.instructions.back().is_assert() &&
1531 true_case.instructions.back().get_condition().is_false() &&
1532 true_case.instructions.back().labels.empty())
1533 {
1534 // The above conjunction deliberately excludes the instance
1535 // if(some) { label: assert(false); }
1536 true_case.instructions.back().set_condition(boolean_negate(guard));
1537 dest.destructive_append(true_case);
1538 true_case.instructions.clear();
1539 if(
1540 is_empty(false_case) ||
1541 (is_size_one(false_case) &&
1542 is_skip(false_case, false_case.instructions.begin())))
1543 return;
1544 }
1545
1546 // similarly, do guarded assertions directly
1547 if(
1548 is_size_one(false_case) && false_case.instructions.back().is_assert() &&
1549 false_case.instructions.back().get_condition().is_false() &&
1550 false_case.instructions.back().labels.empty())
1551 {
1552 // The above conjunction deliberately excludes the instance
1553 // if(some) ... else { label: assert(false); }
1554 false_case.instructions.back().set_condition(guard);
1555 dest.destructive_append(false_case);
1556 false_case.instructions.clear();
1557 if(
1558 is_empty(true_case) ||
1559 (is_size_one(true_case) &&
1560 is_skip(true_case, true_case.instructions.begin())))
1561 return;
1562 }
1563
1564 // a special case for C libraries that use
1565 // (void)((cond) || (assert(0),0))
1566 if(
1567 is_empty(false_case) && true_case.instructions.size() == 2 &&
1568 true_case.instructions.front().is_assert() &&
1569 true_case.instructions.front().get_condition().is_false() &&
1570 true_case.instructions.front().labels.empty() &&
1571 true_case.instructions.back().labels.empty())
1572 {
1573 true_case.instructions.front().set_condition(boolean_negate(guard));
1574 true_case.instructions.erase(--true_case.instructions.end());
1575 dest.destructive_append(true_case);
1576 true_case.instructions.clear();
1577
1578 return;
1579 }
1580
1581 // Flip around if no 'true' case code.
1582 if(is_empty(true_case))
1583 return generate_ifthenelse(
1584 boolean_negate(guard),
1585 false_case,
1586 true_case,
1587 source_location,
1588 dest,
1589 mode);
1590
1591 bool has_else=!is_empty(false_case);
1592
1593 // if(c) P;
1594 //--------------------
1595 // v: if(!c) goto z;
1596 // w: P;
1597 // z: ;
1598
1599 // if(c) P; else Q;
1600 //--------------------
1601 // v: if(!c) goto y;
1602 // w: P;
1603 // x: goto z;
1604 // y: Q;
1605 // z: ;
1606
1607 // do the x label
1611
1612 // do the z label
1615 // We deliberately don't set a location for 'z', it's a dummy
1616 // target.
1617
1618 // y: Q;
1621 if(has_else)
1622 {
1623 tmp_y.swap(false_case);
1624 y=tmp_y.instructions.begin();
1625 }
1626
1627 // v: if(!c) goto z/y;
1630 boolean_negate(guard), has_else ? y : z, source_location, tmp_v, mode);
1631
1632 // w: P;
1634 tmp_w.swap(true_case);
1635
1636 // x: goto z;
1637 CHECK_RETURN(!tmp_w.instructions.empty());
1638 x->complete_goto(z);
1639 x->source_location_nonconst() = tmp_w.instructions.back().source_location();
1640
1641 dest.destructive_append(tmp_v);
1642 dest.destructive_append(tmp_w);
1643
1644 if(has_else)
1645 {
1646 dest.destructive_append(tmp_x);
1647 dest.destructive_append(tmp_y);
1648 }
1649
1650 dest.destructive_append(tmp_z);
1651}
1652
1654static bool has_and_or(const exprt &expr)
1655{
1656 forall_operands(it, expr)
1657 if(has_and_or(*it))
1658 return true;
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,
1671 const irep_idt &mode)
1672{
1673 if(has_and_or(guard) && needs_cleaning(guard))
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,
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
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 {
1792 return false;
1793 }
1794 else if(index_op.id()==ID_array)
1795 {
1796 std::string result;
1798 if(it->is_constant())
1799 {
1800 const auto i = numeric_cast<std::size_t>(*it);
1801 if(!i.has_value())
1802 return true;
1803
1804 if(i.value() != 0) // to skip terminating 0
1805 result += static_cast<char>(i.value());
1806 }
1807
1808 return value=result, false;
1809 }
1810 }
1811
1812 if(expr.id()==ID_string_constant)
1813 {
1814 value = to_string_constant(expr).get_value();
1815 return false;
1816 }
1817
1818 return true;
1819}
1820
1822{
1824
1825 const bool res = get_string_constant(expr, result);
1827 !res,
1828 "expected string constant",
1829 expr.find_source_location(),
1830 expr.pretty());
1831
1832 return result;
1833}
1834
1836{
1837 if(expr.id()==ID_symbol)
1838 {
1839 const symbolt &symbol=
1840 ns.lookup(to_symbol_expr(expr));
1841
1842 return symbol.value;
1843 }
1844 else if(expr.id()==ID_member)
1845 {
1846 auto tmp = to_member_expr(expr);
1847 tmp.compound() = get_constant(tmp.compound());
1848 return std::move(tmp);
1849 }
1850 else if(expr.id()==ID_index)
1851 {
1852 auto tmp = to_index_expr(expr);
1853 tmp.op0() = get_constant(tmp.op0());
1854 tmp.op1() = get_constant(tmp.op1());
1855 return std::move(tmp);
1856 }
1857 else
1858 return expr;
1859}
1860
1862 const typet &type,
1863 const std::string &suffix,
1865 const source_locationt &source_location,
1866 const irep_idt &mode)
1867{
1868 PRECONDITION(!mode.empty());
1869 symbolt &new_symbol = get_fresh_aux_symbol(
1870 type,
1872 "tmp_" + suffix,
1873 source_location,
1874 mode,
1875 symbol_table);
1876
1877 code_frontend_declt decl(new_symbol.symbol_expr());
1878 decl.add_source_location()=source_location;
1879 convert_frontend_decl(decl, dest, mode);
1880
1881 return new_symbol;
1882}
1883
1885 exprt &expr,
1886 const std::string &suffix,
1888 const irep_idt &mode)
1889{
1890 const source_locationt source_location=expr.find_source_location();
1891
1892 symbolt &new_symbol =
1893 new_tmp_symbol(expr.type(), suffix, dest, source_location, mode);
1894
1895 code_assignt assignment;
1896 assignment.lhs()=new_symbol.symbol_expr();
1897 assignment.rhs()=expr;
1898 assignment.add_source_location()=source_location;
1899
1900 convert(assignment, dest, mode);
1901
1902 expr=new_symbol.symbol_expr();
1903}
1904
1906 const codet &code,
1907 symbol_table_baset &symbol_table,
1909 message_handlert &message_handler,
1910 const irep_idt &mode)
1911{
1913 symbol_table_buildert::wrap(symbol_table);
1915 goto_convert.goto_convert(code, dest, mode);
1916}
1917
1919 symbol_table_baset &symbol_table,
1921 message_handlert &message_handler)
1922{
1923 // find main symbol
1924 const symbol_tablet::symbolst::const_iterator s_it=
1925 symbol_table.symbols.find("main");
1926
1928 s_it != symbol_table.symbols.end(), "failed to find main symbol");
1929
1930 const symbolt &symbol=s_it->second;
1931
1933 to_code(symbol.value), symbol_table, dest, message_handler, symbol.mode);
1934}
1935
1951 const code_blockt &thread_body,
1953 const irep_idt &mode)
1954{
1956
1958 convert(thread_body, body, mode);
1959
1961 static_cast<const codet &>(get_nil_irep()),
1962 thread_body.source_location(),
1963 END_THREAD,
1964 nil_exprt(),
1965 {}));
1966 e->source_location_nonconst() = thread_body.source_location();
1968
1970 static_cast<const codet &>(get_nil_irep()),
1971 thread_body.source_location(),
1973 nil_exprt(),
1974 {c}));
1975 preamble.add(goto_programt::make_goto(z, thread_body.source_location()));
1976
1977 dest.destructive_append(preamble);
1978 dest.destructive_append(body);
1979 dest.destructive_append(postamble);
1980}
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:253
Operator to return the address of an object.
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Result of an attempt to find ancestor information about two nodes.
Boolean AND.
Definition std_expr.h:1974
A base class for binary expressions.
Definition std_expr.h:550
exprt & op0()
Definition expr.h:99
exprt & op1()
Definition expr.h:102
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:674
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 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 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
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
const parameterst & parameters() const
Definition std_types.h:655
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:99
exprt & op1()
Definition expr.h:102
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:37
bool empty() const
Definition dstring.h:88
The empty type.
Definition std_types.h:51
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:165
std::vector< exprt > operandst
Definition expr.h:56
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:42
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
const source_locationt & source_location() const
Definition expr.h:230
source_locationt & add_source_location()
Definition expr.h:235
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)
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.
static const unsigned nil_target
Uniquely identify an invalid target or location.
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())
instructionst::iterator targett
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_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())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_other(const codet &_code, 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:2226
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:495
const irept & find(const irep_idt &name) const
Definition irep.cpp:106
bool is_not_nil() const
Definition irep.h:380
void make_nil()
Definition irep.h:454
const irep_idt & id() const
Definition irep.h:396
bool is_nil() const
Definition irep.h:376
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:2874
void set_case_number(const irep_idt &number)
const irep_idt & get_value() const
Expression to hold a symbol (variable)
Definition std_expr.h:80
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:65
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:2856
Semantic type conversion.
Definition std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:1928
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:281
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:18
#define Forall_operands(it, expr)
Definition expr.h:25
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 codet &code)
const code_assignt & to_code_assign(const 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:20
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:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
#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:22
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:1954
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:627
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2206
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
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)
Author: Diffblue Ltd.