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