CBMC
goto_convert.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Program Transformation
4 
5 Author: 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>
18 #include <util/exception_utils.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>
24 #include <util/string_constant.h>
26 
28 
29 #include "destructor.h"
30 
31 static 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;
72  const code_push_catcht::exception_listt &handler_list =
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 
97 {
104 };
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 
160  declaration_hop_instrumentationt instructions_to_add;
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;
166  source_locationt label_location =
167  inputs.label_instruction->source_location();
168  label_location.set_hide();
169  const symbolt &new_flag = get_fresh_aux_symbol(
170  bool_typet{},
171  CPROVER_PREFIX "going_to",
172  id2string(inputs.label),
173  label_location,
174  inputs.mode,
175  symbol_table);
176  label_flags.emplace(inputs.label, new_flag);
177 
178  // Create and initialise flag.
179  instructions_to_add.emplace_back(
180  program.instructions.begin(),
181  goto_programt::make_decl(new_flag.symbol_expr(), label_location));
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.
190  auto clear_on_arrival = make_clear_flag();
191  instructions_to_add.emplace_back(
192  inputs.label_instruction, clear_on_arrival);
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;
209  {
211  auto &declaration = targets.scope_stack.get_declaration(current_node);
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();
222  auto if_goto = goto_programt::make_goto(
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 
242 Function: 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;
255  declaration_hop_instrumentationt instructions_to_insert;
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;
290  node_indext goto_target = g_it.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.
294  ancestry_resultt intersection_result =
296  goto_target, label_target);
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 
308  node_indext end_destruct = intersection_result.common_ancestor;
309  goto_programt destructor_code;
311  i.source_location(),
312  destructor_code,
313  mode,
314  end_destruct,
315  goto_target);
316  dest.destructive_insert(g_it.first, destructor_code);
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;
327  if(variables_added_to_scope)
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;
342  inputs.label_scope_index = label_target;
343  inputs.end_scope_index = intersection_result.common_ancestor;
344  instructions_to_insert.splice(
345  instructions_to_insert.end(),
346  build_declaration_hops(dest, label_flags, inputs));
347  }
348  }
349  else
350  {
351  UNREACHABLE;
352  }
353  }
354 
355  for(auto r_it = instructions_to_insert.rbegin();
356  r_it != instructions_to_insert.rend();
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  {
369  goto_programt::instructiont &i = *g_it;
370  dereference_exprt destination = to_dereference_expr(i.code().op0());
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  {
380  exprt label_expr(ID_label, empty_typet());
381  label_expr.set(ID_identifier, label.first);
382 
383  const equal_exprt guard(pointer, address_of_exprt(label_expr));
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)
405  i.target_number = goto_programt::instructiont::nil_target;
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);
441  irept y_loop_invariant =
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())
448  updated_condition.add(ID_C_spec_assigns).swap(y_assigns);
449  if(y_loop_invariant.is_not_nil())
450  updated_condition.add(ID_C_spec_loop_invariant).swap(y_loop_invariant);
451  if(y_decreases.is_not_nil())
452  updated_condition.add(ID_C_spec_decreases).swap(y_decreases);
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);
475  finish_computed_gotos(dest);
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 
497  goto_programt tmp;
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).
512  code_blockt thread_body;
513  thread_body.add(to_code_label(code).code());
514  thread_body.add_source_location() = code.source_location();
515  generate_thread_block(thread_body, dest, mode);
516  }
517  else
518  {
519  convert(to_code_label(code).code(), tmp, mode);
520 
521  goto_programt::targett target = tmp.instructions.begin();
522  dest.destructive_append(tmp);
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 {
540  goto_programt tmp;
541  convert(code.code(), tmp, mode);
542 
543  goto_programt::targett target = tmp.instructions.begin();
544  dest.destructive_append(tmp);
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()));
558  cases_entry =
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 
595  goto_programt tmp;
596  convert(code.code(), tmp, mode);
597 
598  goto_programt::targett target = tmp.instructions.begin();
599  dest.destructive_append(tmp);
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()});
605  cases_entry =
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{
611  binary_relation_exprt{code.lower(), ID_le, nil_exprt{}},
612  binary_relation_exprt{nil_exprt{}, ID_le, code.upper()}});
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)
626  convert_frontend_decl(to_code_frontend_decl(code), dest, mode);
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)
638  convert_function_call(to_code_function_call(code), dest, mode);
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
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);
769  code_ifthenelset tmp_code(
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 
810  const goto_programt::targett declaration_iterator = [&]() {
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
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);
836  assign.add_source_location() = initializer_location;
837 
838  convert_assign(assign, dest, mode);
839  }
840 
841  destruct_locals(side_effects.temporaries, dest, ns);
842 
843  return declaration_iterator;
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  {
887  const auto &rhs_function_call = to_side_effect_expr_function_call(rhs);
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 ||
925  rhs.get(ID_statement) == ID_statement_expression ||
926  rhs.get(ID_statement) == ID_gcc_conditional_expression))
927  {
928  // handle above side effects
929  side_effects.add(clean_expr(rhs, mode));
930  dest.destructive_append(side_effects.side_effects);
931 
932  code_assignt new_assign(code);
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 
948  code_assignt new_assign(code);
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 
960  code_assignt new_assign(code);
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 
979  clean_expr_resultt side_effects = clean_expr(tmp_op, ID_cpp);
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 
986  irep_idt delete_identifier;
987 
988  if(code.get_statement() == ID_cpp_delete_array)
989  delete_identifier = "__delete_array";
990  else if(code.get_statement() == ID_cpp_delete)
991  delete_identifier = "__delete";
992  else
993  UNREACHABLE;
994 
995  if(destructor.is_not_nil())
996  {
997  if(code.get_statement() == ID_cpp_delete_array)
998  {
999  // build loop
1000  }
1001  else if(code.get_statement() == ID_cpp_delete)
1002  {
1003  // just one object
1004  const dereference_exprt deref_op(tmp_op);
1005 
1006  codet tmp_code = to_code(destructor);
1007  replace_new_object(deref_op, tmp_code);
1008  convert(tmp_code, dest, ID_cpp);
1009  }
1010  else
1011  UNREACHABLE;
1012  }
1013 
1014  // now do "free"
1015  exprt delete_symbol = ns.lookup(delete_identifier).symbol_expr();
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 
1024  code_function_callt delete_call(
1025  delete_symbol, {typecast_exprt(tmp_op, arg_type)});
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 
1043  source_locationt annotated_location = code.source_location();
1044  annotated_location.set("user-provided", true);
1045  dest.add(goto_programt::make_assertion(cond, annotated_location));
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
1126  break_continue_targetst old_targets(targets);
1127 
1128  // do the u label
1129  goto_programt::targett u = side_effects.side_effects.instructions.begin();
1130 
1131  // do the v label
1132  goto_programt tmp_v;
1134  destruct_locals(side_effects.temporaries, tmp_v, ns);
1135 
1136  // do the z and Z labels
1137  goto_programt tmp_z;
1138  destruct_locals(side_effects.temporaries, tmp_z, ns);
1141  goto_programt::targett Z = tmp_z.instructions.begin();
1142 
1143  // do the x label
1144  goto_programt tmp_x;
1145 
1146  if(code.iter().is_nil())
1147  {
1149  }
1150  else
1151  {
1152  exprt tmp_B = code.iter();
1153 
1154  clean_expr_resultt side_effects_iter = clean_expr(tmp_B, mode, false);
1155  tmp_x.destructive_append(side_effects_iter.side_effects);
1156  destruct_locals(side_effects_iter.temporaries, tmp_x, ns);
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
1175  goto_programt tmp_w;
1176  convert(code.body(), tmp_w, mode);
1177 
1178  // y: goto u;
1179  goto_programt tmp_y;
1180  goto_programt::targett y = tmp_y.add(
1182 
1183  // assigns clause, loop invariant and decreases clause
1184  convert_loop_contracts(code, y);
1185 
1186  dest.destructive_append(side_effects.side_effects);
1187  dest.destructive_append(tmp_v);
1188  dest.destructive_append(tmp_w);
1189  dest.destructive_append(tmp_x);
1190  dest.destructive_append(tmp_y);
1191  dest.destructive_append(tmp_z);
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
1214  break_continue_targetst old_targets(targets);
1215 
1216  // do the z label
1217  goto_programt tmp_z;
1219  tmp_z.add(goto_programt::make_skip(source_location));
1220 
1221  goto_programt tmp_branch;
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;
1229  goto_programt tmp_y;
1230  goto_programt::targett y = tmp_y.add(
1232 
1233  // set the targets
1234  targets.set_break(z);
1235  targets.set_continue(y);
1236 
1237  // do the x label
1238  goto_programt tmp_x;
1239  convert(code.body(), tmp_x, mode);
1240 
1241  // assigns clause, loop invariant and decreases clause
1242  convert_loop_contracts(code, y);
1243 
1244  dest.destructive_append(tmp_branch);
1245  dest.destructive_append(tmp_x);
1246  dest.destructive_append(tmp_y);
1247  dest.destructive_append(tmp_z);
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
1281  break_continue_targetst old_targets(targets);
1282 
1283  // do the y label
1284  goto_programt tmp_y;
1286  boolean_negate(cond), condition_location));
1287  destruct_locals(side_effects.temporaries, tmp_y, ns);
1288  goto_programt::targett W = tmp_y.add(
1289  goto_programt::make_incomplete_goto(true_exprt{}, condition_location));
1290 
1291  // do the z label and C labels
1292  goto_programt tmp_z;
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
1313  goto_programt tmp_w;
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
1321  convert_loop_contracts(code, W);
1322 
1323  dest.destructive_append(tmp_w);
1324  dest.destructive_append(side_effects.side_effects);
1325  dest.destructive_append(tmp_y);
1326  dest.destructive_append(tmp_z);
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 
1338  exprt::operandst disjuncts;
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  {
1346  const binary_exprt &and_expr = to_binary_expr(op);
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
1388  source_locationt body_end_location =
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.
1403  if(needs_cleaning(argument))
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 
1412  code_assignt copy_value{
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
1421  break_switch_targetst old_targets(targets);
1422 
1423  // do the z label
1424  goto_programt tmp_z;
1426  tmp_z.add(goto_programt::make_skip(body_end_location));
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 
1434  goto_programt tmp;
1435  convert(code.body(), tmp, mode);
1436 
1437  goto_programt tmp_cases;
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 
1469  tmp_cases.add(goto_programt::make_goto(
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 
1477  goto_programt::targett try_next =
1479  std::move(guard_expr), source_location));
1480  destruct_locals(side_effects.temporaries, tmp_cases, ns);
1481  tmp_cases.add(goto_programt::make_goto(
1482  case_pair.first, true_exprt{}, source_location));
1483  goto_programt::targett next_case =
1484  tmp_cases.add(goto_programt::make_skip(source_location));
1485  try_next->complete_goto(next_case);
1486  }
1487  }
1488 
1489  tmp_cases.add(goto_programt::make_goto(
1490  targets.default_target, targets.default_target->source_location()));
1491 
1492  dest.destructive_append(side_effects.side_effects);
1493  dest.destructive_append(tmp_cases);
1494  dest.destructive_append(tmp);
1495  dest.destructive_append(tmp_z);
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(
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 
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 {
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(
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
1682  code_ifthenelset new_if1(
1683  to_binary_expr(code.cond()).op1(), code.then_case());
1684  new_if1.add_source_location() = source_location;
1685  code_ifthenelset new_if0(
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
1696  goto_programt tmp_then;
1697  destruct_locals(side_effects.temporaries, tmp_then, ns);
1698  convert(code.then_case(), tmp_then, mode);
1699  source_locationt then_end_location =
1700  code.then_case().get_statement() == ID_block
1702  : code.then_case().source_location();
1703 
1704  goto_programt tmp_else;
1705  destruct_locals(side_effects.temporaries, tmp_else, ns);
1706  source_locationt else_end_location;
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
1713  : code.else_case().source_location();
1714  }
1715 
1717  tmp_guard,
1718  source_location,
1719  tmp_then,
1720  then_end_location,
1721  tmp_else,
1722  else_end_location,
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 
1747 static 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,
1758  const source_locationt &then_end_location,
1759  goto_programt &false_case,
1760  const source_locationt &else_end_location,
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.
1767  goto_programt tmp_z;
1769  dest.add(goto_programt::make_goto(z, guard, source_location));
1770  dest.destructive_append(tmp_z);
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,
1837  else_end_location,
1838  true_case,
1839  then_end_location,
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
1861  goto_programt tmp_x;
1862  goto_programt::targett x = tmp_x.add(
1863  goto_programt::make_incomplete_goto(true_exprt(), then_end_location));
1864 
1865  // do the z label
1866  goto_programt tmp_z;
1867  goto_programt::targett z = tmp_z.add(
1868  goto_programt::make_skip(has_else ? else_end_location : then_end_location));
1869 
1870  // y: Q;
1871  goto_programt tmp_y;
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;
1880  goto_programt tmp_v;
1882  boolean_negate(guard), has_else ? y : z, source_location, tmp_v, mode);
1883 
1884  // w: P;
1885  goto_programt tmp_w;
1886  tmp_w.swap(true_case);
1887 
1888  // x: goto z;
1889  CHECK_RETURN(!tmp_w.instructions.empty());
1890  x->complete_goto(z);
1891 
1892  dest.destructive_append(tmp_v);
1893  dest.destructive_append(tmp_w);
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
1905  if(!then_branch_returns)
1906  {
1907  dest.destructive_append(tmp_x);
1908  }
1909  dest.destructive_append(tmp_y);
1910  }
1911 
1912  // Don't add the `z` label at the end of the `if` when not needed.
1913  if(!has_else || !then_branch_returns)
1914  {
1915  dest.destructive_append(tmp_z);
1916  }
1917 }
1918 
1920 static 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,
1936  goto_programt::targett target_true,
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 
1948  goto_programt tmp;
1949  goto_programt::targett target_false =
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));
1965  goto_programt tmp_destruct;
1966  destruct_locals(side_effects.temporaries, tmp_destruct, ns);
1967  dest.insert_before_swap(target_true, tmp_destruct);
1968  destruct_locals(side_effects.temporaries, dest, ns);
1969  }
1970 }
1971 
1974  const exprt &guard,
1975  goto_programt::targett target_true,
1976  goto_programt::targett target_false,
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(),
1986  target_false,
1987  target_true,
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));
2043  goto_programt tmp_destruct;
2044  destruct_locals(side_effects.temporaries, tmp_destruct, ns);
2045  dest.insert_before_swap(target_true, tmp_destruct);
2046 
2047  // false branch
2048  dest.add(goto_programt::make_goto(target_false, source_location));
2049  destruct_locals(side_effects.temporaries, tmp_destruct, ns);
2050  dest.insert_before_swap(target_false, tmp_destruct);
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());
2064  simplify(index_op, ns);
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 {
2102  irep_idt result;
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 {
2194  symbol_table_buildert symbol_table_builder =
2195  symbol_table_buildert::wrap(symbol_table);
2196  goto_convertt goto_convert(symbol_table_builder, message_handler);
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 
2242  postamble.add(goto_programt::instructiont(
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(),
2253  START_THREAD,
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.
Definition: pointer_expr.h:540
Result of an attempt to find ancestor information about two nodes.
Definition: scope_tree.h:25
std::size_t right_depth_below_common_ancestor
Definition: scope_tree.h:44
node_indext common_ancestor
Definition: scope_tree.h:42
Boolean AND.
Definition: std_expr.h:2120
A base class for binary expressions.
Definition: std_expr.h:638
exprt & op1()
Definition: expr.h:136
exprt & op0()
Definition: expr.h:133
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
source_locationt end_location() const
Definition: std_code.h:187
void add(const codet &code)
Definition: std_code.h:168
code_operandst & statements()
Definition: std_code.h:138
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 exprt & cond() const
Definition: std_code.h:679
const codet & body() const
Definition: std_code.h:689
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 & init() const
Definition: std_code.h:749
const exprt & iter() const
Definition: std_code.h:769
const exprt & cond() const
Definition: std_code.h:759
const codet & body() const
Definition: std_code.h:779
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
codet & code()
the statement to be executed when the case applies
Definition: std_code.h:1131
const exprt & lower() const
lower bound of range
Definition: std_code.h:1107
const exprt & upper() const
upper bound of range
Definition: std_code.h:1119
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 codet & then_case() const
Definition: std_code.h:488
const exprt & cond() const
Definition: std_code.h:478
const codet & else_case() const
Definition: std_code.h:498
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
exception_listt & exception_list()
Definition: std_code.h:1860
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1023
codet & code()
Definition: std_code.h:1050
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 exprt & value() const
Definition: std_code.h:555
const codet & body() const
Definition: std_code.h:565
const parameterst & parameters() const
Definition: std_types.h:699
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.
Definition: std_code_base.h:29
exprt & op1()
Definition: expr.h:136
exprt & op0()
Definition: expr.h:133
const irep_idt & get_statement() const
Definition: std_code_base.h:65
Operator to dereference a pointer.
Definition: pointer_expr.h:834
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:1361
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
source_locationt & add_source_location()
Definition: expr.h:236
const source_locationt & source_location() const
Definition: expr.h:231
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
The Boolean constant false.
Definition: std_expr.h:3072
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.
Definition: goto_program.h:181
void complete_goto(targett _target)
Definition: goto_program.h:482
targetst targets
The list of successor instructions.
Definition: goto_program.h:414
const goto_instruction_codet & code() const
Get the code represented by this instruction.
Definition: goto_program.h:188
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:553
const source_locationt & source_location() const
Definition: goto_program.h:333
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:945
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:874
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:643
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:730
instructionst::iterator targett
Definition: goto_program.h:614
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:722
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())
Definition: goto_program.h:891
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:708
static instructiont make_other(const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:957
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:814
static instructiont make_location(const source_locationt &l)
Definition: goto_program.h:901
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:739
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
bool empty() const
Is the program empty?
Definition: goto_program.h:799
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:964
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:933
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:2370
exprt & true_case()
Definition: std_expr.h:2397
exprt & false_case()
Definition: std_expr.h:2407
exprt & cond()
Definition: std_expr.h:2387
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
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:412
bool is_not_nil() const
Definition: irep.h:372
const irep_idt & id() const
Definition: irep.h:388
void make_nil()
Definition: irep.h:446
void swap(irept &irep)
Definition: irep.h:434
irept & add(const irep_idt &name)
Definition: irep.cpp:103
bool is_nil() const
Definition: irep.h:368
source_locationt source_location
Definition: message.h:239
mstreamt & warning() const
Definition: message.h:396
mstreamt & result() const
Definition: message.h:401
mstreamt & debug() const
Definition: message.h:421
static eomt eom
Definition: message.h:289
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
The NIL expression.
Definition: std_expr.h:3081
std::optional< declaration_statet > & get_declaration(node_indext index)
Fetches the declaration value for the passed-in node index.
Definition: scope_tree.cpp:31
void add(const codet &destructor, std::optional< goto_programt::targett > declaration)
Adds a destructor/declaration pair to the current stack, attaching it to the current node.
Definition: scope_tree.cpp:11
void descend_tree()
Walks the current node down to its child.
Definition: scope_tree.cpp:100
void set_current_node(std::optional< node_indext > val)
Sets the current node.
Definition: scope_tree.cpp:89
node_indext get_current_node() const
Gets the node that the next addition will be added to as a child.
Definition: scope_tree.cpp:109
const ancestry_resultt get_nearest_common_ancestor_info(node_indext left_index, node_indext right_index)
Finds the nearest common ancestor of two nodes and then returns it.
Definition: scope_tree.cpp:37
void set_case_number(const irep_idt &number)
void value(const irep_idt &)
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
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:3063
Semantic type conversion.
Definition: std_expr.h:2068
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2076
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)
Definition: destructor.cpp:21
void destruct_locals(const std::list< irep_idt > &vars, goto_programt &dest, const namespacet &ns)
Definition: destructor.cpp:62
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
Definition: expr_util.cpp:103
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_assignt & to_code_assign(const goto_instruction_codet &code)
const code_function_callt & to_code_function_call(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.
Definition: goto_program.h:32
@ ATOMIC_END
Definition: goto_program.h:44
@ DEAD
Definition: goto_program.h:48
@ ASSIGN
Definition: goto_program.h:46
@ ATOMIC_BEGIN
Definition: goto_program.h:43
@ CATCH
Definition: goto_program.h:51
@ END_THREAD
Definition: goto_program.h:40
@ SKIP
Definition: goto_program.h:38
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
@ START_THREAD
Definition: goto_program.h:39
@ DECL
Definition: goto_program.h:47
@ OTHER
Definition: goto_program.h:37
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 dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:890
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
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).
Definition: remove_skip.cpp:27
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
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:530
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:875
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:654
const code_continuet & to_code_continue(const codet &code)
Definition: std_code.h:1239
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1506
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:251
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1077
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1004
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_switcht & to_code_switch(const codet &code)
Definition: std_code.h:592
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1428
const code_frontend_declt & to_code_frontend_decl(const codet &code)
Definition: std_code.h:429
const code_breakt & to_code_break(const codet &code)
Definition: std_code.h:1203
static code_push_catcht & to_code_push_catch(codet &code)
Definition: std_code.h:1883
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:203
const code_frontend_returnt & to_code_frontend_return(const codet &code)
Definition: std_code.h:943
const code_assertt & to_code_assert(const codet &code)
Definition: std_code.h:304
const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)
Definition: std_code.h:1161
const code_fort & to_code_for(const codet &code)
Definition: std_code.h:823
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1282
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 if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2450
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2102
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2352
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:715
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2936
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1533
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)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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.
computed_gotost computed_gotos
goto_programt::targett continue_target
void set_break(goto_programt::targett _break_target)
goto_programt::targett default_target
goto_programt::targett return_target
void set_default(goto_programt::targett _default_target)
void set_continue(goto_programt::targett _continue_target)
goto_programt::targett break_target