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