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