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