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