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