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