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