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);
1261  l.code().swap(b);
1262  l.add_source_location()=target->source_location;
1263  b.swap(l);
1264  }
1265 
1266  assert(b.get_statement()==ID_label);
1267  dest.add(std::move(b));
1268  return this_end;
1269  }
1270 
1271  // code is supposed to look like this:
1272  // __CPROVER_ASYNC_0: START THREAD 1
1273  // GOTO 2
1274  // 1: code in new thread
1275  // END THREAD
1276  // 2: code in existing thread
1277  /* check the structure and compute the iterators */
1278  assert(next->is_goto() && next->guard.is_true());
1279  assert(!next->is_backwards_goto());
1280  assert(thread_start->location_number < next->get_target()->location_number);
1281  goto_programt::const_targett after_thread_start=thread_start;
1282  ++after_thread_start;
1283 
1284  goto_programt::const_targett thread_end=next->get_target();
1285  --thread_end;
1286  assert(thread_start->location_number < thread_end->location_number);
1287  assert(thread_end->is_end_thread());
1288 
1289  assert(upper_bound==goto_program.instructions.end() ||
1290  thread_end->location_number < upper_bound->location_number);
1291  /* end structure check */
1292 
1293  // use pthreads if "code in new thread" is a function call to a function with
1294  // suitable signature
1295  if(
1296  thread_start->is_function_call() &&
1297  thread_start->get_function_call().arguments().size() == 1 &&
1298  after_thread_start == thread_end)
1299  {
1300  const code_function_callt &cf = thread_start->get_function_call();
1301 
1302  system_headers.insert("pthread.h");
1303 
1305  dest.add(code_function_callt(
1306  cf.lhs(),
1307  symbol_exprt("pthread_create", code_typet({}, empty_typet())),
1308  {n, n, cf.function(), cf.arguments().front()}));
1309 
1310  return thread_end;
1311  }
1312 
1313  codet b=code_blockt();
1314  for( ; thread_start!=thread_end; ++thread_start)
1315  thread_start =
1316  convert_instruction(thread_start, upper_bound, to_code_block(b));
1317 
1318  for(goto_programt::instructiont::labelst::const_iterator
1319  it=target->labels.begin();
1320  it!=target->labels.end();
1321  ++it)
1322  if(has_prefix(id2string(*it), CPROVER_PREFIX "ASYNC_"))
1323  {
1324  labels_in_use.insert(*it);
1325 
1326  code_labelt l(*it);
1327  l.code().swap(b);
1328  l.add_source_location()=target->source_location;
1329  b.swap(l);
1330  }
1331 
1332  assert(b.get_statement()==ID_label);
1333  dest.add(std::move(b));
1334  return thread_end;
1335 }
1336 
1339  code_blockt &)
1340 {
1341  // this isn't really clear as throw is not supported in expr2cpp either
1342  UNREACHABLE;
1343  return target;
1344 }
1345 
1349  code_blockt &)
1350 {
1351  // this isn't really clear as catch is not supported in expr2cpp either
1352  UNREACHABLE;
1353  return target;
1354 }
1355 
1357 {
1358  if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
1359  {
1360  const typet &full_type=ns.follow(type);
1361 
1362  const irep_idt &identifier = to_tag_type(type).get_identifier();
1363  const symbolt &symbol = ns.lookup(identifier);
1364 
1365  if(
1366  symbol.location.get_function().empty() ||
1367  !type_names_set.insert(identifier).second)
1368  return;
1369 
1370  for(const auto &c : to_struct_union_type(full_type).components())
1371  add_local_types(c.type());
1372 
1373  type_names.push_back(identifier);
1374  }
1375  else if(type.id()==ID_c_enum_tag)
1376  {
1377  const irep_idt &identifier=to_c_enum_tag_type(type).get_identifier();
1378  const symbolt &symbol=ns.lookup(identifier);
1379 
1380  if(symbol.location.get_function().empty() ||
1381  !type_names_set.insert(identifier).second)
1382  return;
1383 
1384  assert(!identifier.empty());
1385  type_names.push_back(identifier);
1386  }
1387  else if(type.id()==ID_pointer ||
1388  type.id()==ID_array)
1389  {
1390  add_local_types(type.subtype());
1391  }
1392 }
1393 
1395  codet &code,
1396  const irep_idt parent_stmt)
1397 {
1398  if(code.get_statement()==ID_decl)
1399  {
1400  if(code.operands().size()==2 &&
1401  code.op1().id()==ID_side_effect &&
1402  to_side_effect_expr(code.op1()).get_statement()==ID_function_call)
1403  {
1406  cleanup_function_call(call.function(), call.arguments());
1407 
1408  cleanup_expr(code.op1(), false);
1409  }
1410  else
1411  Forall_operands(it, code)
1412  cleanup_expr(*it, true);
1413 
1414  if(code.op0().type().id()==ID_array)
1415  cleanup_expr(to_array_type(code.op0().type()).size(), true);
1416 
1417  add_local_types(code.op0().type());
1418 
1419  const irep_idt &typedef_str=code.op0().type().get(ID_C_typedef);
1420  if(!typedef_str.empty() &&
1421  typedef_names.find(typedef_str)==typedef_names.end())
1422  code.op0().type().remove(ID_C_typedef);
1423 
1424  return;
1425  }
1426  else if(code.get_statement()==ID_function_call)
1427  {
1429 
1430  cleanup_function_call(call.function(), call.arguments());
1431 
1432  while(call.lhs().is_not_nil() &&
1433  call.lhs().id()==ID_typecast)
1434  call.lhs()=to_typecast_expr(call.lhs()).op();
1435  }
1436 
1437  if(code.has_operands())
1438  {
1439  exprt::operandst &operands=code.operands();
1440  Forall_expr(it, operands)
1441  {
1442  if(it->id()==ID_code)
1443  cleanup_code(to_code(*it), code.get_statement());
1444  else
1445  cleanup_expr(*it, false);
1446  }
1447  }
1448 
1449  const irep_idt &statement=code.get_statement();
1450  if(statement==ID_label)
1451  {
1452  code_labelt &cl=to_code_label(code);
1453  const irep_idt &label=cl.get_label();
1454 
1455  assert(!label.empty());
1456 
1457  if(labels_in_use.find(label)==labels_in_use.end())
1458  {
1459  codet tmp = cl.code();
1460  code.swap(tmp);
1461  }
1462  }
1463  else if(statement==ID_block)
1464  cleanup_code_block(code, parent_stmt);
1465  else if(statement==ID_ifthenelse)
1466  cleanup_code_ifthenelse(code, parent_stmt);
1467  else if(statement==ID_dowhile)
1468  {
1469  code_dowhilet &do_while=to_code_dowhile(code);
1470 
1471  // turn an empty do {} while(...); into a while(...);
1472  // to ensure convergence
1473  if(do_while.body().get_statement()==ID_skip)
1474  do_while.set_statement(ID_while);
1475  // do stmt while(false) is just stmt
1476  else if(do_while.cond().is_false() &&
1477  do_while.body().get_statement()!=ID_block)
1478  code=do_while.body();
1479  }
1480 }
1481 
1483  const exprt &function,
1485 {
1486  if(function.id()!=ID_symbol)
1487  return;
1488 
1489  const symbol_exprt &fn=to_symbol_expr(function);
1490 
1491  // don't edit function calls we might have introduced
1492  const symbolt *s;
1493  if(!ns.lookup(fn.get_identifier(), s))
1494  {
1495  const symbolt &fn_sym=ns.lookup(fn.get_identifier());
1496  const code_typet &code_type=to_code_type(fn_sym.type);
1497  const code_typet::parameterst &parameters=code_type.parameters();
1498 
1499  if(parameters.size()==arguments.size())
1500  {
1501  code_typet::parameterst::const_iterator it=parameters.begin();
1502  Forall_expr(it2, arguments)
1503  {
1504  if(it2->type().id() == ID_union || it2->type().id() == ID_union_tag)
1505  it2->type()=it->type();
1506  ++it;
1507  }
1508  }
1509  }
1510 }
1511 
1513  codet &code,
1514  const irep_idt parent_stmt)
1515 {
1516  assert(code.get_statement()==ID_block);
1517 
1518  exprt::operandst &operands=code.operands();
1520  operands.size()>1 && i<operands.size();
1521  ) // no ++i
1522  {
1523  exprt::operandst::iterator it=operands.begin()+i;
1524  // remove skip
1525  if(to_code(*it).get_statement()==ID_skip &&
1526  it->source_location().get_comment().empty())
1527  operands.erase(it);
1528  // merge nested blocks, unless there are declarations in the inner block
1529  else if(to_code(*it).get_statement()==ID_block)
1530  {
1531  bool has_decl=false;
1532  forall_operands(it2, *it)
1533  if(it2->id()==ID_code && to_code(*it2).get_statement()==ID_decl)
1534  {
1535  has_decl=true;
1536  break;
1537  }
1538 
1539  if(!has_decl)
1540  {
1541  operands.insert(operands.begin()+i+1,
1542  it->operands().begin(), it->operands().end());
1543  operands.erase(operands.begin()+i);
1544  // no ++i
1545  }
1546  else
1547  ++i;
1548  }
1549  else
1550  ++i;
1551  }
1552 
1553  if(operands.empty() && parent_stmt!=ID_nil)
1554  code=code_skipt();
1555  else if(operands.size()==1 &&
1556  parent_stmt!=ID_nil &&
1557  to_code(code.op0()).get_statement()!=ID_decl)
1558  {
1559  codet tmp = to_code(code.op0());
1560  code.swap(tmp);
1561  }
1562 }
1563 
1565 {
1566  if(type.get_bool(ID_C_constant))
1567  type.remove(ID_C_constant);
1568 
1569  if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
1570  {
1571  const irep_idt &identifier = to_tag_type(type).get_identifier();
1572  if(!const_removed.insert(identifier).second)
1573  return;
1574 
1575  symbolt &symbol = symbol_table.get_writeable_ref(identifier);
1576  INVARIANT(
1577  symbol.is_type,
1578  "Symbol "+id2string(identifier)+" should be a type");
1579 
1580  remove_const(symbol.type);
1581  }
1582  else if(type.id()==ID_array)
1583  remove_const(type.subtype());
1584  else if(type.id()==ID_struct ||
1585  type.id()==ID_union)
1586  {
1589 
1590  for(struct_union_typet::componentst::iterator
1591  it=c.begin();
1592  it!=c.end();
1593  ++it)
1594  remove_const(it->type());
1595  }
1596 }
1597 
1598 static bool has_labels(const codet &code)
1599 {
1600  if(code.get_statement()==ID_label)
1601  return true;
1602 
1603  forall_operands(it, code)
1604  if(it->id()==ID_code && has_labels(to_code(*it)))
1605  return true;
1606 
1607  return false;
1608 }
1609 
1610 static bool move_label_ifthenelse(exprt &expr, exprt &label_dest)
1611 {
1612  if(expr.is_nil() || to_code(expr).get_statement() != ID_block)
1613  return false;
1614 
1615  code_blockt &block=to_code_block(to_code(expr));
1616  if(
1617  !block.has_operands() ||
1618  block.statements().back().get_statement() != ID_label)
1619  {
1620  return false;
1621  }
1622 
1623  code_labelt &label = to_code_label(block.statements().back());
1624 
1625  if(label.get_label().empty() ||
1626  label.code().get_statement()!=ID_skip)
1627  {
1628  return false;
1629  }
1630 
1631  label_dest=label;
1632  code_skipt s;
1633  label.swap(s);
1634 
1635  return true;
1636 }
1637 
1639  codet &code,
1640  const irep_idt parent_stmt)
1641 {
1642  code_ifthenelset &i_t_e=to_code_ifthenelse(code);
1643  const exprt cond=simplify_expr(i_t_e.cond(), ns);
1644 
1645  // assert(false) expands to if(true) assert(false), simplify again (and also
1646  // simplify other cases)
1647  if(
1648  cond.is_true() &&
1649  (i_t_e.else_case().is_nil() || !has_labels(i_t_e.else_case())))
1650  {
1651  codet tmp = i_t_e.then_case();
1652  code.swap(tmp);
1653  }
1654  else if(cond.is_false() && !has_labels(i_t_e.then_case()))
1655  {
1656  if(i_t_e.else_case().is_nil())
1657  code=code_skipt();
1658  else
1659  {
1660  codet tmp = i_t_e.else_case();
1661  code.swap(tmp);
1662  }
1663  }
1664  else
1665  {
1666  if(
1667  i_t_e.then_case().is_not_nil() &&
1668  i_t_e.then_case().get_statement() == ID_ifthenelse)
1669  {
1670  // we re-introduce 1-code blocks with if-then-else to avoid dangling-else
1671  // ambiguity
1672  i_t_e.then_case() = code_blockt({i_t_e.then_case()});
1673  }
1674 
1675  if(
1676  i_t_e.else_case().is_not_nil() &&
1677  i_t_e.then_case().get_statement() == ID_skip &&
1678  i_t_e.else_case().get_statement() == ID_ifthenelse)
1679  {
1680  // we re-introduce 1-code blocks with if-then-else to avoid dangling-else
1681  // ambiguity
1682  i_t_e.else_case() = code_blockt({i_t_e.else_case()});
1683  }
1684  }
1685 
1686  // move labels at end of then or else case out
1687  if(code.get_statement()==ID_ifthenelse)
1688  {
1689  codet then_label=code_skipt(), else_label=code_skipt();
1690 
1691  bool moved=false;
1692  if(i_t_e.then_case().is_not_nil())
1693  moved|=move_label_ifthenelse(i_t_e.then_case(), then_label);
1694  if(i_t_e.else_case().is_not_nil())
1695  moved|=move_label_ifthenelse(i_t_e.else_case(), else_label);
1696 
1697  if(moved)
1698  {
1699  code = code_blockt({i_t_e, then_label, else_label});
1700  cleanup_code(code, parent_stmt);
1701  }
1702  }
1703 
1704  // remove empty then/else
1705  if(
1706  code.get_statement() == ID_ifthenelse &&
1707  i_t_e.then_case().get_statement() == ID_skip)
1708  {
1709  not_exprt tmp(i_t_e.cond());
1710  simplify(tmp, ns);
1711  // simplification might have removed essential type casts
1712  cleanup_expr(tmp, false);
1713  i_t_e.cond().swap(tmp);
1714  i_t_e.then_case().swap(i_t_e.else_case());
1715  }
1716  if(
1717  code.get_statement() == ID_ifthenelse && i_t_e.else_case().is_not_nil() &&
1718  i_t_e.else_case().get_statement() == ID_skip)
1719  i_t_e.else_case().make_nil();
1720  // or even remove the if altogether if the then case is now empty
1721  if(
1722  code.get_statement() == ID_ifthenelse && i_t_e.else_case().is_nil() &&
1723  (i_t_e.then_case().is_nil() ||
1724  i_t_e.then_case().get_statement() == ID_skip))
1725  code=code_skipt();
1726 }
1727 
1728 void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
1729 {
1730  // we might have to do array -> pointer conversions
1731  if(no_typecast &&
1732  (expr.id()==ID_address_of || expr.id()==ID_member))
1733  {
1734  Forall_operands(it, expr)
1735  cleanup_expr(*it, false);
1736  }
1737  else if(!no_typecast &&
1738  (expr.id()==ID_union || expr.id()==ID_struct ||
1739  expr.id()==ID_array || expr.id()==ID_vector))
1740  {
1741  Forall_operands(it, expr)
1742  cleanup_expr(*it, true);
1743  }
1744  else
1745  {
1746  Forall_operands(it, expr)
1747  cleanup_expr(*it, no_typecast);
1748  }
1749 
1750  // work around transparent union argument
1751  if(
1752  expr.id() == ID_union && expr.type().id() != ID_union &&
1753  expr.type().id() != ID_union_tag)
1754  {
1755  expr=to_union_expr(expr).op();
1756  }
1757 
1758  // try to get rid of type casts, revealing (char)97 -> 'a'
1759  if(expr.id()==ID_typecast &&
1760  to_typecast_expr(expr).op().is_constant())
1761  simplify(expr, ns);
1762 
1763  if(expr.id()==ID_union ||
1764  expr.id()==ID_struct)
1765  {
1766  if(no_typecast)
1767  return;
1768 
1770  expr.type().id() == ID_struct_tag || expr.type().id() == ID_union_tag,
1771  "union/struct expressions should have a tag type");
1772 
1773  const typet &t=expr.type();
1774 
1775  add_local_types(t);
1776  expr=typecast_exprt(expr, t);
1777 
1778  const irep_idt &typedef_str=expr.type().get(ID_C_typedef);
1779  if(!typedef_str.empty() &&
1780  typedef_names.find(typedef_str)==typedef_names.end())
1781  expr.type().remove(ID_C_typedef);
1782  }
1783  else if(expr.id()==ID_array ||
1784  expr.id()==ID_vector)
1785  {
1786  if(no_typecast ||
1787  expr.get_bool(ID_C_string_constant))
1788  return;
1789 
1790  const typet &t=expr.type();
1791 
1792  expr = typecast_exprt(expr, t);
1793  add_local_types(t);
1794 
1795  const irep_idt &typedef_str=expr.type().get(ID_C_typedef);
1796  if(!typedef_str.empty() &&
1797  typedef_names.find(typedef_str)==typedef_names.end())
1798  expr.type().remove(ID_C_typedef);
1799  }
1800  else if(expr.id()==ID_side_effect)
1801  {
1802  const irep_idt &statement=to_side_effect_expr(expr).get_statement();
1803 
1804  if(statement==ID_nondet)
1805  {
1806  // Replace by a function call to nondet_...
1807  // We first search for a suitable one in the symbol table.
1808 
1809  irep_idt id;
1810 
1811  for(symbol_tablet::symbolst::const_iterator
1812  it=symbol_table.symbols.begin();
1813  it!=symbol_table.symbols.end();
1814  it++)
1815  {
1816  if(it->second.type.id()!=ID_code)
1817  continue;
1818  if(!has_prefix(id2string(it->second.base_name), "nondet_"))
1819  continue;
1820  const code_typet &code_type=to_code_type(it->second.type);
1821  if(code_type.return_type() != expr.type())
1822  continue;
1823  if(!code_type.parameters().empty())
1824  continue;
1825  id=it->second.name;
1826  break;
1827  }
1828 
1829  // none found? make one
1830 
1831  if(id.empty())
1832  {
1833  irep_idt base_name;
1834 
1835  if(!expr.type().get(ID_C_c_type).empty())
1836  {
1837  irep_idt suffix;
1838  suffix=expr.type().get(ID_C_c_type);
1839 
1840  if(symbol_table.symbols.find("nondet_"+id2string(suffix))==
1841  symbol_table.symbols.end())
1842  base_name="nondet_"+id2string(suffix);
1843  }
1844 
1845  if(base_name.empty())
1846  {
1847  unsigned count=0;
1848  while(symbol_table.symbols.find("nondet_"+std::to_string(count))!=
1849  symbol_table.symbols.end())
1850  ++count;
1851  base_name="nondet_"+std::to_string(count);
1852  }
1853 
1854  symbolt symbol;
1855  symbol.base_name=base_name;
1856  symbol.name=base_name;
1857  symbol.type = code_typet({}, expr.type());
1858  id=symbol.name;
1859 
1860  symbol_table.insert(std::move(symbol));
1861  }
1862 
1863  const symbolt &symbol=ns.lookup(id);
1864 
1865  symbol_exprt symbol_expr(symbol.name, symbol.type);
1866  symbol_expr.add_source_location()=expr.source_location();
1867 
1869  symbol_expr, {}, expr.type(), expr.source_location());
1870 
1871  expr.swap(call);
1872  }
1873  }
1874  else if(expr.id()==ID_isnan ||
1875  expr.id()==ID_sign)
1876  system_headers.insert("math.h");
1877  else if(expr.id()==ID_constant)
1878  {
1879  if(expr.type().id()==ID_floatbv)
1880  {
1881  const ieee_floatt f(to_constant_expr(expr));
1882  if(f.is_NaN() || f.is_infinity())
1883  system_headers.insert("math.h");
1884  }
1885  else if(expr.type().id()==ID_pointer)
1886  add_local_types(expr.type());
1887  else if(expr.type().id()==ID_bool ||
1888  expr.type().id()==ID_c_bool)
1889  {
1890  expr = typecast_exprt(
1891  from_integer(
1892  expr.is_true() ? 1 : 0, signedbv_typet(config.ansi_c.int_width)),
1893  bool_typet());
1894  }
1895 
1896  const irept &c_sizeof_type=expr.find(ID_C_c_sizeof_type);
1897 
1898  if(c_sizeof_type.is_not_nil())
1899  add_local_types(static_cast<const typet &>(c_sizeof_type));
1900  }
1901  else if(expr.id()==ID_typecast)
1902  {
1903  if(expr.type().id() == ID_c_bit_field)
1904  expr=to_typecast_expr(expr).op();
1905  else
1906  {
1907  add_local_types(expr.type());
1908 
1909  const irep_idt &typedef_str=expr.type().get(ID_C_typedef);
1910  if(!typedef_str.empty() &&
1911  typedef_names.find(typedef_str)==typedef_names.end())
1912  expr.type().remove(ID_C_typedef);
1913 
1914  assert(expr.type().id()!=ID_union &&
1915  expr.type().id()!=ID_struct);
1916  }
1917  }
1918  else if(expr.id()==ID_symbol)
1919  {
1920  if(expr.type().id()!=ID_code)
1921  {
1922  const irep_idt &identifier=to_symbol_expr(expr).get_identifier();
1923  const symbolt &symbol=ns.lookup(identifier);
1924 
1925  if(symbol.is_static_lifetime &&
1926  symbol.type.id()!=ID_code &&
1927  !symbol.is_extern &&
1928  !symbol.location.get_function().empty() &&
1929  local_static_set.insert(identifier).second)
1930  {
1931  if(symbol.value.is_not_nil())
1932  {
1933  exprt value=symbol.value;
1934  cleanup_expr(value, true);
1935  }
1936 
1937  local_static.push_back(identifier);
1938  }
1939  }
1940  }
1941 }
1942 
1945  codet &dst)
1946 {
1947  if(src->code.source_location().is_not_nil())
1948  dst.add_source_location() = src->code.source_location();
1949  else if(src->source_location.is_not_nil())
1950  dst.add_source_location() = src->source_location;
1951 }
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:148
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:173
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:1449
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:2192
goto_program2codet::cleanup_code_ifthenelse
void cleanup_code_ifthenelse(codet &code, const irep_idt parent_stmt)
Definition: goto_program2code.cpp:1638
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:899
codet::op0
exprt & op0()
Definition: expr.h:101
address_of_exprt::object
exprt & object()
Definition: std_expr.h:2824
goto_program2codet::cleanup_function_call
void cleanup_function_call(const exprt &function, code_function_callt::argumentst &arguments)
Definition: goto_program2code.cpp:1482
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:1023
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:320
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:777
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:1461
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:2917
side_effect_expr_function_callt
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2127
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:1943
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:1728
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:405
code_assertt
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:590
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:1625
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:1644
bool_typet
The Boolean type.
Definition: std_types.h:37
code_ifthenelset::cond
const exprt & cond() const
Definition: std_code.h:767
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:1941
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:1211
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:749
code_labelt::code
codet & code()
Definition: std_code.h:1403
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:158
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:1346
to_code_switch_case
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1503
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:1356
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:181
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:1186
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:961
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:4018
code_breakt
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1608
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:2852
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:1130
to_code_ifthenelse
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:819
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1378
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:4002
goto_program2codet::cleanup_code
void cleanup_code(codet &code, const irep_idt parent_stmt)
Definition: goto_program2code.cpp:1394
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:538
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:1430
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:315
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:1005
goto_program2code.h
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:1598
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:1297
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:1195
dstringt::empty
bool empty() const
Definition: dstring.h:88
code_blockt::add
void add(const codet &code)
Definition: std_code.h:211
false_exprt
The Boolean constant false.
Definition: std_expr.h:3993
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:1610
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:1231
code_declt::symbol
symbol_exprt & symbol()
Definition: std_code.h:411
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:1907
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:2321
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:1393
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:844
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2973
code_returnt::has_return_value
bool has_return_value() const
Definition: std_code.h:1333
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:273
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1313
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:837
goto_program2codet::convert_throw
goto_programt::const_targett convert_throw(goto_programt::const_targett target, code_blockt &dest)
Definition: goto_program2code.cpp:1337
symbolt
Symbol table entry.
Definition: symbol.h:28
code_dowhilet::body
const codet & body() const
Definition: std_code.h:978
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:2171
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2076
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:787
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:1236
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:1476
goto_program2codet::operator()
void operator()()
Definition: goto_program2code.cpp:24
config.h
code_dowhilet::cond
const exprt & cond() const
Definition: std_code.h:968
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:259
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:2161
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:104
goto_program2codet::remove_const
void remove_const(typet &type)
Definition: goto_program2code.cpp:1564
index_exprt
Array index operator.
Definition: std_expr.h:1299
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:43
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:257
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:854
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2042
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
code_returnt::return_value
const exprt & return_value() const
Definition: std_code.h:1323
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:298
true_exprt
The Boolean constant true.
Definition: std_expr.h:3984
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:817
exprt::reserve_operands
void reserve_operands(operandst::size_type n)
Definition: expr.h:125
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:252
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:1512
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:1221
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1172
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:1820
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:2872
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:3968