cprover
goto_convert_new_switch_case.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Program Transformation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_convert_class.h"
13 
14 #include <cassert>
15 
16 #include <util/cprover_prefix.h>
17 #include <util/prefix.h>
18 #include <util/std_expr.h>
19 #include <util/symbol_table.h>
20 #include <util/simplify_expr.h>
21 #include <util/rename.h>
22 
23 #include <util/c_types.h>
24 
25 #include "goto_convert.h"
26 #include "destructor.h"
27 
28 static bool is_empty(const goto_programt &goto_program)
29 {
30  forall_goto_program_instructions(it, goto_program)
31  if(!it->is_skip() ||
32  !it->labels.empty() ||
33  !it->code.is_nil())
34  return false;
35 
36  return true;
37 }
38 
40 {
41  for(const auto &target : targets.gotos)
42  {
43  goto_programt::instructiont &i=*target;
44 
45  if(i.code.get_statement()=="non-deterministic-goto")
46  {
47  const irept &destinations=i.code.find("destinations");
48 
49  i.make_goto();
50 
51  forall_irep(it, destinations.get_sub())
52  {
53  labelst::const_iterator l_it=
54  targets.labels.find(it->id_string());
55 
56  if(l_it==targets.labels.end())
57  {
58  err_location(i.code);
59  str << "goto label `" << it->id_string() << "' not found";
60  error_msg();
61  throw 0;
62  }
63 
64  i.targets.push_back(l_it->second);
65  }
66  }
67  else if(i.is_start_thread())
68  {
69  const irep_idt &goto_label=i.code.get(ID_destination);
70 
71  labelst::const_iterator l_it=
72  targets.labels.find(goto_label);
73 
74  if(l_it==targets.labels.end())
75  {
76  err_location(i.code);
77  str << "goto label `" << goto_label << "' not found";
78  error_msg();
79  throw 0;
80  }
81 
82  i.targets.push_back(l_it->second);
83  }
84  else if(i.code.get_statement()==ID_goto)
85  {
86  const irep_idt &goto_label=i.code.get(ID_destination);
87 
88  labelst::const_iterator l_it=targets.labels.find(goto_label);
89 
90  if(l_it==targets.labels.end())
91  {
92  err_location(i.code);
93  str << "goto label `" << goto_label << "' not found";
94  error_msg();
95  throw 0;
96  }
97 
98  i.targets.clear();
99  i.targets.push_back(l_it->second);
100  }
101  else
102  {
103  err_location(i.code);
104  error() << "finish_gotos: unexpected goto" << eom;
105  throw 0;
106  }
107  }
108 
109  targets.gotos.clear();
110 }
111 
113 {
114  for(const auto &target : targets.computed_gotos)
115  {
116  goto_programt::instructiont &i=*target;
117  exprt destination=i.code.op0();
118 
119  assert(destination.id()==ID_dereference);
120  assert(destination.operands().size()==1);
121 
122  exprt pointer=destination.op0();
123 
124  // remember the expression for later checks
125  i.type=OTHER;
126  i.code=code_expressiont(pointer);
127 
128  // insert huge case-split
129  for(const auto &label : targets.labels)
130  {
131  exprt label_expr(ID_label, empty_typet());
132  label_expr.set(ID_identifier, label.first);
133 
134  equal_exprt guard;
135 
136  guard.lhs()=pointer;
137  guard.rhs()=address_of_exprt(label_expr);
138 
140  goto_program.insert_after(target);
141 
142  t->make_goto(label.second);
143  t->source_location=i.source_location;
144  t->guard=guard;
145  }
146  }
147 
148  targets.computed_gotos.clear();
149 }
150 
151 void goto_convertt::goto_convert(const codet &code, goto_programt &dest)
152 {
153  goto_convert_rec(code, dest);
154 }
155 
157  const codet &code,
158  goto_programt &dest)
159 {
160  convert(code, dest);
161 
162  finish_gotos();
163  finish_computed_gotos(dest);
164 }
165 
167  const codet &code,
169  goto_programt &dest)
170 {
172  t->code=code;
174 }
175 
177  const code_labelt &code,
178  goto_programt &dest)
179 {
180  if(code.operands().size()!=1)
181  {
182  err_location(code);
183  error() << "label statement expected to have one operand" << eom;
184  throw 0;
185  }
186 
187  // grab the label
188  const irep_idt &label=code.get_label();
189 
190  goto_programt tmp;
191 
192  // magic thread creation label?
193  if(has_prefix(id2string(label), "__CPROVER_ASYNC_"))
194  {
195  // this is like a START_THREAD
196  codet tmp_code(ID_start_thread);
197  tmp_code.copy_to_operands(code.op0());
198  tmp_code.add_source_location()=code.source_location();
199  convert(tmp_code, tmp);
200  }
201  else
202  convert(to_code(code.op0()), tmp);
203 
204  goto_programt::targett target=tmp.instructions.begin();
205  dest.destructive_append(tmp);
206 
207  targets.labels.insert(std::pair<irep_idt, goto_programt::targett>
208  (label, target));
209  target->labels.push_front(label);
210 }
211 
213  const codet &code,
214  goto_programt &dest)
215 {
216  // ignore for now
217 }
218 
220  const code_switch_caset &code,
221  goto_programt &dest)
222 {
223  if(code.operands().size()!=2)
224  {
225  err_location(code);
226  error() << "switch-case statement expected to have two operands" << eom;
227  throw 0;
228  }
229 
230  goto_programt tmp;
231  convert(code.code(), tmp);
232 
233  goto_programt::targett target=tmp.instructions.begin();
234  dest.destructive_append(tmp);
235 
236  // default?
237 
238  if(code.is_default())
239  targets.set_default(target);
240  else
241  {
242  // cases?
243 
244  cases_mapt::iterator cases_entry=targets.cases_map.find(target);
245  if(cases_entry==targets.cases_map.end())
246  {
247  // We generate a 'goto'-instruction for this.
249  dest.add_instruction(GOTO);
250 
251  g->source_location=code.source_location();
252 
253  targets.cases.push_back(std::make_pair(g, caset()));
254 
255  cases_entry=targets.cases_map.insert(std::make_pair(
256  g, --targets.cases.end())).first;
257  }
258 
259  exprt::operandst &case_op_dest=cases_entry->second->second;
260  case_op_dest.push_back(code.case_op());
261  }
262 }
263 
265  const codet &code,
266  goto_programt &dest)
267 {
268  if(code.operands().size()!=3)
269  {
270  err_location(code);
271  error() << "GCC's switch-case-range statement expected to have "
272  << "three operands" << eom;
273  throw 0;
274  }
275 
276  goto_programt tmp;
277  convert(to_code(code.op2()), tmp);
278 
279  // goto_programt::targett target=tmp.instructions.begin();
280  dest.destructive_append(tmp);
281 
282  #if 0
283  cases_mapt::iterator cases_entry=targets.cases_map.find(target);
284  if(cases_entry==targets.cases_map.end())
285  {
286  targets.cases.push_back(std::make_pair(target, caset()));
287  cases_entry=targets.cases_map.insert(std::make_pair(
288  target, --targets.cases.end())).first;
289  }
290 
291  // TODO
292  exprt::operandst &case_op_dest=cases_entry->second->second;
293  case_op_dest.push_back(code.case_op());
294  #endif
295 }
296 
299  const codet &code,
300  goto_programt &dest)
301 {
302  const irep_idt &statement=code.get_statement();
303 
304  if(statement==ID_block)
305  convert_block(to_code_block(code), dest);
306  else if(statement==ID_decl)
307  convert_decl(to_code_decl(code), dest);
308  else if(statement==ID_decl_type)
309  convert_decl_type(code, dest);
310  else if(statement==ID_expression)
312  else if(statement==ID_assign)
313  convert_assign(to_code_assign(code), dest);
314  else if(statement==ID_init)
315  convert_init(code, dest);
316  else if(statement==ID_assert)
317  convert_assert(to_code_assert(code), dest);
318  else if(statement==ID_assume)
319  convert_assume(to_code_assume(code), dest);
320  else if(statement==ID_function_call)
322  else if(statement==ID_label)
323  convert_label(to_code_label(code), dest);
324  else if(statement==ID_gcc_local_label)
325  convert_gcc_local_label(code, dest);
326  else if(statement==ID_switch_case)
328  else if(statement==ID_gcc_switch_case_range)
329  convert_gcc_switch_case_range(code, dest);
330  else if(statement==ID_for)
331  convert_for(to_code_for(code), dest);
332  else if(statement==ID_while)
333  convert_while(to_code_while(code), dest);
334  else if(statement==ID_dowhile)
335  convert_dowhile(code, dest);
336  else if(statement==ID_switch)
337  convert_switch(to_code_switch(code), dest);
338  else if(statement==ID_break)
339  convert_break(to_code_break(code), dest);
340  else if(statement==ID_return)
341  convert_return(to_code_return(code), dest);
342  else if(statement==ID_continue)
343  convert_continue(to_code_continue(code), dest);
344  else if(statement==ID_goto)
345  convert_goto(code, dest);
346  else if(statement==ID_gcc_computed_goto)
347  convert_gcc_computed_goto(code, dest);
348  else if(statement==ID_skip)
349  convert_skip(code, dest);
350  else if(statement=="non-deterministic-goto")
351  convert_non_deterministic_goto(code, dest);
352  else if(statement==ID_ifthenelse)
354  else if(statement==ID_specc_notify)
355  convert_specc_notify(code, dest);
356  else if(statement==ID_specc_wait)
357  convert_specc_wait(code, dest);
358  else if(statement==ID_specc_par)
359  convert_specc_par(code, dest);
360  else if(statement==ID_start_thread)
361  convert_start_thread(code, dest);
362  else if(statement==ID_end_thread)
363  convert_end_thread(code, dest);
364  else if(statement==ID_atomic_begin)
365  convert_atomic_begin(code, dest);
366  else if(statement==ID_atomic_end)
367  convert_atomic_end(code, dest);
368  else if(statement==ID_bp_enforce)
369  convert_bp_enforce(code, dest);
370  else if(statement==ID_bp_abortif)
371  convert_bp_abortif(code, dest);
372  else if(statement==ID_cpp_delete ||
373  statement=="cpp_delete[]")
374  convert_cpp_delete(code, dest);
375  else if(statement==ID_msc_try_except)
376  convert_msc_try_except(code, dest);
377  else if(statement==ID_msc_try_finally)
378  convert_msc_try_finally(code, dest);
379  else if(statement==ID_msc_leave)
380  convert_msc_leave(code, dest);
381  else if(statement==ID_try_catch) // C++ try/catch
382  convert_try_catch(code, dest);
383  else if(statement==ID_CPROVER_try_catch) // CPROVER-homemade
384  convert_CPROVER_try_catch(code, dest);
385  else if(statement==ID_CPROVER_throw) // CPROVER-homemade
386  convert_CPROVER_throw(code, dest);
387  else if(statement==ID_CPROVER_try_finally)
388  convert_CPROVER_try_finally(code, dest);
389  else if(statement==ID_asm)
390  convert_asm(to_code_asm(code), dest);
391  else if(statement==ID_static_assert)
392  {
393  assert(code.operands().size()==2);
394  exprt assertion=code.op0();
395  assertion.make_typecast(bool_typet());
396  simplify(assertion, ns);
397  if(assertion.is_false())
398  {
399  err_location(code.op0());
400  str << "static assertion "
401  << get_string_constant(code.op1());
402  error_msg();
403  throw 0;
404  }
405  else if(assertion.is_true())
406  {
407  }
408  else
409  {
410  // we may wish to complain
411  }
412  }
413  else if(statement==ID_dead)
414  copy(code, DEAD, dest);
415  else if(statement==ID_decl_block)
416  {
417  forall_operands(it, code)
418  convert(to_code(*it), dest);
419  }
420  else
421  copy(code, OTHER, dest);
422 
423  // make sure dest is never empty
424  if(dest.instructions.empty())
425  {
426  dest.add_instruction(SKIP);
427  dest.instructions.back().code.make_nil();
428  dest.instructions.back().source_location=code.source_location();
429  }
430 }
431 
433  const code_blockt &code,
434  goto_programt &dest)
435 {
436  const source_locationt &end_location=code.end_location();
437 
438  // this saves the size of the destructor stack
439  std::size_t old_stack_size=targets.destructor_stack.size();
440 
441  // now convert block
442  forall_operands(it, code)
443  {
444  const codet &b_code=to_code(*it);
445  convert(b_code, dest);
446  }
447 
448  // see if we need to do any destructors
449  unwind_destructor_stack(end_location, old_stack_size, dest);
450 
451  // remove those destructors
452  targets.destructor_stack.resize(old_stack_size);
453 }
454 
456  const code_expressiont &code,
457  goto_programt &dest)
458 {
459  if(code.operands().size()!=1)
460  {
461  err_location(code);
462  error() << "expression statement takes one operand" << eom;
463  throw 0;
464  }
465 
466  exprt expr=code.op0();
467 
468  if(expr.id()==ID_if)
469  {
470  // We do a special treatment for c?t:f
471  // by compiling to if(c) t; else f;
472  const if_exprt &if_expr=to_if_expr(expr);
473  code_ifthenelset tmp_code;
474  tmp_code.add_source_location()=expr.source_location();
475  tmp_code.cond()=if_expr.cond();
476  tmp_code.then_case()=code_expressiont(if_expr.true_case());
477  tmp_code.then_case().add_source_location()=expr.source_location();
478  tmp_code.else_case()=code_expressiont(if_expr.false_case());
479  tmp_code.else_case().add_source_location()=expr.source_location();
480  convert_ifthenelse(tmp_code, dest);
481  }
482  else
483  {
484  clean_expr(expr, dest, false); // result _not_ used
485 
486  // Any residual expression?
487  // We keep it to add checks later.
488  if(expr.is_not_nil())
489  {
490  codet tmp=code;
491  tmp.op0()=expr;
493  copy(tmp, OTHER, dest);
494  }
495  }
496 }
497 
499  const code_declt &code,
500  goto_programt &dest)
501 {
502  const exprt &op0=code.op0();
503 
504  if(op0.id()!=ID_symbol)
505  {
506  err_location(op0);
507  error() << "decl statement expects symbol as first operand" << eom;
508  throw 0;
509  }
510 
511  const irep_idt &identifier=op0.get(ID_identifier);
512 
513  const symbolt &symbol=lookup(identifier);
514 
515  if(symbol.is_static_lifetime ||
516  symbol.type.id()==ID_code)
517  return; // this is a SKIP!
518 
519  if(code.operands().size()==1)
520  {
521  copy(code, DECL, dest);
522  }
523  else
524  {
525  // this is expected to go away
526  exprt initializer;
527 
528  codet tmp=code;
529  initializer=code.op1();
530  tmp.operands().resize(1);
531 
532  // Break up into decl and assignment.
533  // Decl must be visible before initializer.
534  copy(tmp, DECL, dest);
535 
536  code_assignt assign(code.op0(), initializer);
537  assign.add_source_location()=tmp.source_location();
538 
539  convert_assign(assign, dest);
540  }
541 
542  // now create a 'dead' instruction -- will be added after the
543  // destructor created below as unwind_destructor_stack pops off the
544  // top of the destructor stack
545  const symbol_exprt symbol_expr(symbol.name, symbol.type);
546 
547  {
548  code_deadt code_dead(symbol_expr);
549  targets.destructor_stack.push_back(code_dead);
550  }
551 
552  // do destructor
553  code_function_callt destructor=get_destructor(ns, symbol.type);
554 
555  if(destructor.is_not_nil())
556  {
557  // add "this"
558  address_of_exprt this_expr(symbol_expr, pointer_type(symbol.type));
559  destructor.arguments().push_back(this_expr);
560 
561  targets.destructor_stack.push_back(destructor);
562  }
563 }
564 
566  const codet &code,
567  goto_programt &dest)
568 {
569  // we remove these
570 }
571 
573  const code_assignt &code,
574  goto_programt &dest)
575 {
576  exprt lhs=code.lhs(),
577  rhs=code.rhs();
578 
579  clean_expr(lhs, dest);
580 
581  if(rhs.id()==ID_side_effect &&
582  rhs.get(ID_statement)==ID_function_call)
583  {
584  if(rhs.operands().size()!=2)
585  {
586  err_location(rhs);
587  error() << "function_call sideeffect takes two operands" << eom;
588  throw 0;
589  }
590 
591  Forall_operands(it, rhs)
592  clean_expr(*it, dest);
593 
594  do_function_call(lhs, rhs.op0(), rhs.op1().operands(), dest);
595  }
596  else if(rhs.id()==ID_side_effect &&
597  (rhs.get(ID_statement)==ID_cpp_new ||
598  rhs.get(ID_statement)==ID_cpp_new_array))
599  {
600  Forall_operands(it, rhs)
601  clean_expr(*it, dest);
602 
603  do_cpp_new(lhs, to_side_effect_expr(rhs), dest);
604  }
605  else if(rhs.id()==ID_side_effect &&
606  rhs.get(ID_statement)==ID_java_new)
607  {
608  Forall_operands(it, rhs)
609  clean_expr(*it, dest);
610 
611  do_java_new(lhs, to_side_effect_expr(rhs), dest);
612  }
613  else if(rhs.id()==ID_side_effect &&
614  rhs.get(ID_statement)==ID_java_new_array)
615  {
616  Forall_operands(it, rhs)
617  clean_expr(*it, dest);
618 
619  do_java_new_array(lhs, to_side_effect_expr(rhs), dest);
620  }
621  else if(rhs.id()==ID_side_effect &&
622  rhs.get(ID_statement)==ID_malloc)
623  {
624  // just preserve
625  Forall_operands(it, rhs)
626  clean_expr(*it, dest);
627 
628  code_assignt new_assign(code);
629  new_assign.lhs()=lhs;
630  new_assign.rhs()=rhs;
631 
632  copy(new_assign, ASSIGN, dest);
633  }
634  else
635  {
636  clean_expr(rhs, dest);
637 
638  if(lhs.id()==ID_typecast)
639  {
640  assert(lhs.operands().size()==1);
641 
642  // add a typecast to the rhs
643  exprt new_rhs=rhs;
644  rhs.make_typecast(lhs.op0().type());
645 
646  // remove typecast from lhs
647  exprt tmp=lhs.op0();
648  lhs.swap(tmp);
649  }
650 
651  code_assignt new_assign(code);
652  new_assign.lhs()=lhs;
653  new_assign.rhs()=rhs;
654 
655  copy(new_assign, ASSIGN, dest);
656  }
657 }
658 
660  const codet &code,
661  goto_programt &dest)
662 {
663  if(code.operands().size()!=2)
664  {
665  err_location(code);
666  error() << "init statement takes two operands" << eom;
667  throw 0;
668  }
669 
670  // make it an assignment
671  codet assignment=code;
672  assignment.set_statement(ID_assign);
673 
674  convert(to_code_assign(assignment), dest);
675 }
676 
678  const codet &code,
679  goto_programt &dest)
680 {
681  if(code.operands().size()!=1)
682  {
683  err_location(code);
684  error() << "cpp_delete statement takes one operand" << eom;
685  throw 0;
686  }
687 
688  exprt tmp_op=code.op0();
689 
690  clean_expr(tmp_op, dest);
691 
692  // we call the destructor, and then free
693  const exprt &destructor=
694  static_cast<const exprt &>(code.find(ID_destructor));
695 
696  irep_idt delete_identifier;
697 
698  if(code.get_statement()==ID_cpp_delete_array)
699  delete_identifier="__delete_array";
700  else if(code.get_statement()==ID_cpp_delete)
701  delete_identifier="__delete";
702  else
703  assert(false);
704 
705  if(destructor.is_not_nil())
706  {
707  if(code.get_statement()==ID_cpp_delete_array)
708  {
709  // build loop
710  }
711  else if(code.get_statement()==ID_cpp_delete)
712  {
713  // just one object
714  exprt deref_op(ID_dereference, tmp_op.type().subtype());
715  deref_op.copy_to_operands(tmp_op);
716 
717  codet tmp_code=to_code(destructor);
718  replace_new_object(deref_op, tmp_code);
719  convert(tmp_code, dest);
720  }
721  else
722  assert(false);
723  }
724 
725  // now do "free"
726  exprt delete_symbol=ns.lookup(delete_identifier).symbol_expr();
727 
728  assert(to_code_type(delete_symbol.type()).parameters().size()==1);
729 
730  typet arg_type=
731  to_code_type(delete_symbol.type()).parameters().front().type();
732 
733  code_function_callt delete_call;
734  delete_call.function()=delete_symbol;
735  delete_call.arguments().push_back(typecast_exprt(tmp_op, arg_type));
736  delete_call.lhs().make_nil();
737  delete_call.add_source_location()=code.source_location();
738 
739  convert(delete_call, dest);
740 }
741 
743  const code_assertt &code,
744  goto_programt &dest)
745 {
746  exprt cond=code.assertion();
747 
748  clean_expr(cond, dest);
749 
751  t->guard.swap(cond);
752  t->source_location=code.source_location();
753  t->source_location.set(ID_property, ID_assertion);
754  t->source_location.set("user-provided", true);
755 }
756 
758  const codet &code,
759  goto_programt &dest)
760 {
762  t->source_location=code.source_location();
763  t->code=code;
764 }
765 
767  const code_assumet &code,
768  goto_programt &dest)
769 {
770  exprt op=code.assumption();
771 
772  clean_expr(op, dest);
773 
775  t->guard.swap(op);
776  t->source_location=code.source_location();
777 }
778 
780  const code_fort &code,
781  goto_programt &dest)
782 {
783  // turn for(A; c; B) { P } into
784  // A; while(c) { P; B; }
785  //-----------------------------
786  // A;
787  // u: sideeffects in c
788  // v: if(!c) goto z;
789  // w: P;
790  // x: B; <-- continue target
791  // y: goto u;
792  // z: ; <-- break target
793 
794  // A;
795  if(code.init().is_not_nil())
796  convert(to_code(code.init()), dest);
797 
798  exprt cond=code.cond();
799 
800  goto_programt sideeffects;
801  clean_expr(cond, sideeffects);
802 
803  // save break/continue targets
804  break_continue_targetst old_targets(targets);
805 
806  // do the u label
807  goto_programt::targett u=sideeffects.instructions.begin();
808 
809  // do the v label
810  goto_programt tmp_v;
812 
813  // do the z label
814  goto_programt tmp_z;
816  z->source_location=code.source_location();
817 
818  // do the x label
819  goto_programt tmp_x;
820 
821  if(code.op2().is_nil())
822  {
823  tmp_x.add_instruction(SKIP);
824  tmp_x.instructions.back().source_location=code.source_location();
825  }
826  else
827  {
828  exprt tmp_B=code.iter();
829 
830  clean_expr(tmp_B, tmp_x, false);
831 
832  if(tmp_x.instructions.empty())
833  {
834  tmp_x.add_instruction(SKIP);
835  tmp_x.instructions.back().source_location=code.source_location();
836  }
837  }
838 
839  // optimize the v label
840  if(sideeffects.instructions.empty())
841  u=v;
842 
843  // set the targets
844  targets.set_break(z);
845  targets.set_continue(tmp_x.instructions.begin());
846 
847  // v: if(!c) goto z;
848  v->make_goto(z);
849  v->guard=cond;
850  v->guard.make_not();
851  v->source_location=cond.source_location();
852 
853  // do the w label
854  goto_programt tmp_w;
855  convert(code.body(), tmp_w);
856 
857  // y: goto u;
858  goto_programt tmp_y;
859  goto_programt::targett y=tmp_y.add_instruction();
860  y->make_goto(u);
861  y->guard=true_exprt();
862  y->source_location=code.source_location();
863 
864  dest.destructive_append(sideeffects);
865  dest.destructive_append(tmp_v);
866  dest.destructive_append(tmp_w);
867  dest.destructive_append(tmp_x);
868  dest.destructive_append(tmp_y);
869  dest.destructive_append(tmp_z);
870 
871  // restore break/continue
872  old_targets.restore(targets);
873 }
874 
876  const code_whilet &code,
877  goto_programt &dest)
878 {
879  const exprt &cond=code.cond();
880  const source_locationt &source_location=code.source_location();
881 
882  // while(c) P;
883  //--------------------
884  // v: sideeffects in c
885  // if(!c) goto z;
886  // x: P;
887  // y: goto v; <-- continue target
888  // z: ; <-- break target
889 
890  // save break/continue targets
891  break_continue_targetst old_targets(targets);
892 
893  // do the z label
894  goto_programt tmp_z;
896  z->make_skip();
897  z->source_location=source_location;
898 
899  goto_programt tmp_branch;
901  boolean_negate(cond), z, source_location, tmp_branch);
902 
903  // do the v label
904  goto_programt::targett v=tmp_branch.instructions.begin();
905 
906  // do the y label
907  goto_programt tmp_y;
909 
910  // set the targets
911  targets.set_break(z);
913 
914  // do the x label
915  goto_programt tmp_x;
916  convert(code.body(), tmp_x);
917 
918  // y: if(c) goto v;
919  y->make_goto(v);
920  y->guard=true_exprt();
921  y->source_location=code.source_location();
922 
923  dest.destructive_append(tmp_branch);
924  dest.destructive_append(tmp_x);
925  dest.destructive_append(tmp_y);
926  dest.destructive_append(tmp_z);
927 
928  // restore break/continue
929  old_targets.restore(targets);
930 }
931 
933  const codet &code,
934  goto_programt &dest)
935 {
936  if(code.operands().size()!=2)
937  {
938  err_location(code);
939  error() << "dowhile takes two operands" << eom;
940  throw 0;
941  }
942 
943  // save source location
944  source_locationt condition_location=code.op0().find_source_location();
945 
946  exprt cond=code.op0();
947 
948  goto_programt sideeffects;
949  clean_expr(cond, sideeffects);
950 
951  // do P while(c);
952  //--------------------
953  // w: P;
954  // x: sideeffects in c <-- continue target
955  // y: if(c) goto w;
956  // z: ; <-- break target
957 
958  // save break/continue targets
959  break_continue_targetst old_targets(targets);
960 
961  // do the y label
962  goto_programt tmp_y;
964 
965  // do the z label
966  goto_programt tmp_z;
968  z->make_skip();
969  z->source_location=code.source_location();
970 
971  // do the x label
973  if(sideeffects.instructions.empty())
974  x=y;
975  else
976  x=sideeffects.instructions.begin();
977 
978  // set the targets
979  targets.set_break(z);
981 
982  // do the w label
983  goto_programt tmp_w;
984  convert(to_code(code.op1()), tmp_w);
985  goto_programt::targett w=tmp_w.instructions.begin();
986 
987  // y: if(c) goto w;
988  y->make_goto(w);
989  y->guard=cond;
990  y->source_location=condition_location;
991 
992  dest.destructive_append(tmp_w);
993  dest.destructive_append(sideeffects);
994  dest.destructive_append(tmp_y);
995  dest.destructive_append(tmp_z);
996 
997  // restore break/continue targets
998  old_targets.restore(targets);
999 }
1000 
1002  const exprt &value,
1003  const exprt::operandst &case_op)
1004 {
1005  exprt dest=exprt(ID_or, bool_typet());
1006  dest.reserve_operands(case_op.size());
1007 
1008  forall_expr(it, case_op)
1009  {
1010  equal_exprt eq_expr;
1011  eq_expr.lhs()=value;
1012  eq_expr.rhs()=*it;
1013  dest.move_to_operands(eq_expr);
1014  }
1015 
1016  assert(!dest.operands().empty());
1017 
1018  if(dest.operands().size()==1)
1019  {
1020  exprt tmp;
1021  tmp.swap(dest.op0());
1022  dest.swap(tmp);
1023  }
1024 
1025  return dest;
1026 }
1027 
1029  const code_switcht &code,
1030  goto_programt &dest)
1031 {
1032  // switch(v) {
1033  // case x: Px;
1034  // case y: Py;
1035  // ...
1036  // default: Pd;
1037  // }
1038  // --------------------
1039  // a: goto X;
1040  // X: if(v!=x) goto Y;
1041  // Px;
1042  // Y: if(v!=y) goto Z;
1043  // Py;
1044  // Z: ...
1045  // Pd;
1046  // z: ;
1047 
1048  if(code.operands().size()<2)
1049  {
1050  err_location(code);
1051  error() << "switch takes at least two operands" << eom;
1052  throw 0;
1053  }
1054 
1055  exprt argument=code.value();
1056 
1057  goto_programt sideeffects;
1058  clean_expr(argument, sideeffects);
1059 
1060  // save break/default/cases targets
1061  break_switch_targetst old_targets(targets);
1062 
1063  // do the a label
1064  goto_programt tmp_a;
1066  a->make_goto();
1067  a->source_location=code.source_location();
1068 
1069  // do the z label
1070  goto_programt tmp_z;
1072  z->make_skip();
1073  z->source_location=code.source_location();
1074 
1075  // set the new targets -- continue stays as is
1076  targets.set_break(z);
1077  targets.set_default(z);
1078  targets.cases.clear();
1079  targets.cases_map.clear();
1080 
1081  goto_programt tmp;
1082 
1083  forall_operands(it, code)
1084  if(it!=code.operands().begin())
1085  convert(to_code(*it), tmp);
1086 
1087  goto_programt tmp_cases;
1088 
1089  goto_programt::targett previous=a;
1090 
1091  for(casest::iterator it=targets.cases.begin();
1092  it!=targets.cases.end();
1093  it++)
1094  {
1095  const caset &case_ops=it->second;
1096 
1097  // we generate a goto for 'case'
1098  assert(it->first->is_goto());
1099 
1100  assert(!case_ops.empty());
1101 
1102  exprt guard_expr=case_guard(argument, case_ops);
1103 
1104  // adjust previous case to jump here
1105  previous->set_target(it->first);
1106  it->first->guard=guard_expr;
1107 
1108  previous=it->first;
1109  }
1110 
1111  {
1112  // adjust previous to jump to default target
1113  previous->set_target(targets.default_target);
1114  }
1115 
1116  dest.destructive_append(sideeffects);
1117  dest.destructive_append(tmp_a);
1118  dest.destructive_append(tmp_cases);
1119  dest.destructive_append(tmp);
1120  dest.destructive_append(tmp_z);
1121 
1122  // restore old targets
1123  old_targets.restore(targets);
1124 }
1125 
1127  const code_breakt &code,
1128  goto_programt &dest)
1129 {
1130  if(!targets.break_set)
1131  {
1132  err_location(code);
1133  error() << "break without target" << eom;
1134  throw 0;
1135  }
1136 
1137  // need to process destructor stack
1139  code.source_location(), targets.break_stack_size, dest);
1140 
1141  // add goto
1143  t->make_goto(targets.break_target);
1144  t->source_location=code.source_location();
1145 }
1146 
1148  const code_returnt &code,
1149  goto_programt &dest)
1150 {
1151  if(!targets.return_set)
1152  {
1153  err_location(code);
1154  error() << "return without target" << eom;
1155  throw 0;
1156  }
1157 
1158  if(!code.operands().empty() &&
1159  code.operands().size()!=1)
1160  {
1161  err_location(code);
1162  error() << "return takes none or one operand" << eom;
1163  throw 0;
1164  }
1165 
1166  code_returnt new_code(code);
1167 
1168  if(new_code.has_return_value())
1169  {
1170  bool result_is_used=
1171  new_code.return_value().type().id()!=ID_empty;
1172 
1173  goto_programt sideeffects;
1174  clean_expr(new_code.return_value(), sideeffects, result_is_used);
1175  dest.destructive_append(sideeffects);
1176 
1177  // remove void-typed return value
1178  if(!result_is_used)
1179  new_code.return_value().make_nil();
1180  }
1181 
1183  {
1184  if(!new_code.has_return_value())
1185  {
1186  err_location(new_code);
1187  error() << "function must return value" << eom;
1188  throw 0;
1189  }
1190 
1191  // Now add a return node to set the return value.
1193  t->make_return();
1194  t->code=new_code;
1195  t->source_location=new_code.source_location();
1196  }
1197  else
1198  {
1199  if(new_code.has_return_value() &&
1200  new_code.return_value().type().id()!=ID_empty)
1201  {
1202  err_location(new_code);
1203  error() << "function must not return value" << eom;
1204  throw 0;
1205  }
1206  }
1207 
1208  // Need to process _entire_ destructor stack.
1209  unwind_destructor_stack(code.source_location(), 0, dest);
1210 
1211  // add goto to end-of-function
1213  t->make_goto(targets.return_target, true_exprt());
1214  t->source_location=new_code.source_location();
1215 }
1216 
1218  const code_continuet &code,
1219  goto_programt &dest)
1220 {
1221  if(!targets.continue_set)
1222  {
1223  err_location(code);
1224  error() << "continue without target" << eom;
1225  throw 0;
1226  }
1227 
1228  // need to process destructor stack
1231 
1232  // add goto
1234  t->make_goto(targets.continue_target);
1235  t->source_location=code.source_location();
1236 }
1237 
1239  const codet &code,
1240  goto_programt &dest)
1241 {
1243  t->make_goto();
1244  t->source_location=code.source_location();
1245  t->code=code;
1246 
1247  // remember it to do target later
1248  targets.gotos.push_back(t);
1249 }
1250 
1252  const codet &code,
1253  goto_programt &dest)
1254 {
1256  t->make_skip();
1257  t->source_location=code.source_location();
1258  t->code=code;
1259 
1260  // remember it to do this later
1261  targets.computed_gotos.push_back(t);
1262 }
1263 
1265  const codet &code,
1266  goto_programt &dest)
1267 {
1268  convert_goto(code, dest);
1269 }
1270 
1272  const codet &code,
1273  goto_programt &dest)
1274 {
1275  #if 0
1277 
1278  forall_operands(it, code)
1279  convert_specc_event(*it, t->events);
1280 
1281  t->code.swap(code);
1282  t->source_location=code.source_location();
1283  #endif
1284 
1285  copy(code, OTHER, dest);
1286 }
1287 
1289  const exprt &op,
1290  std::set<irep_idt> &events)
1291 {
1292  if(op.id()==ID_or || op.id()==ID_and)
1293  {
1294  forall_operands(it, op)
1295  convert_specc_event(*it, events);
1296  }
1297  else if(op.id()==ID_specc_event)
1298  {
1299  irep_idt event=op.get(ID_identifier);
1300 
1301  if(has_prefix(id2string(event), "specc::"))
1302  event=std::string(id2string(event), 7, std::string::npos);
1303 
1304  events.insert(event);
1305  }
1306  else
1307  {
1308  err_location(op);
1309  error() << "convert_convert_event got " << op.id() << eom;
1310  throw 0;
1311  }
1312 }
1313 
1315  const codet &code,
1316  goto_programt &dest)
1317 {
1318  #if 0
1320 
1321  if(code.operands().size()!=1)
1322  {
1323  err_location(code);
1324  error() << "specc_wait expects one operand" << eom;
1325  throw 0;
1326  }
1327 
1328  const exprt &op=code.op0();
1329 
1330  if(op.id()=="or")
1331  t->or_semantics=true;
1332 
1333  convert_specc_event(op, t->events);
1334 
1335  t->code.swap(code);
1336  t->source_location=code.source_location();
1337  #endif
1338 
1339  copy(code, OTHER, dest);
1340 }
1341 
1343  const codet &code,
1344  goto_programt &dest)
1345 {
1346  copy(code, OTHER, dest);
1347 }
1348 
1350  const codet &code,
1351  goto_programt &dest)
1352 {
1353  if(code.operands().size()!=1)
1354  {
1355  err_location(code);
1356  error() << "start_thread expects one operand" << eom;
1357  throw 0;
1358  }
1359 
1360  goto_programt::targett start_thread=
1362 
1363  start_thread->source_location=code.source_location();
1364 
1365  {
1366  // start_thread label;
1367  // goto tmp;
1368  // label: op0-code
1369  // end_thread
1370  // tmp: skip
1371 
1372  goto_programt::targett goto_instruction=dest.add_instruction(GOTO);
1373  goto_instruction->guard=true_exprt();
1374  goto_instruction->source_location=code.source_location();
1375 
1376  goto_programt tmp;
1377  convert(to_code(code.op0()), tmp);
1379  end_thread->source_location=code.source_location();
1380 
1381  start_thread->targets.push_back(tmp.instructions.begin());
1382  dest.destructive_append(tmp);
1383  goto_instruction->targets.push_back(dest.add_instruction(SKIP));
1384  dest.instructions.back().source_location=code.source_location();
1385  }
1386 }
1387 
1389  const codet &code,
1390  goto_programt &dest)
1391 {
1392  if(!code.operands().empty())
1393  {
1394  err_location(code);
1395  error() << "end_thread expects no operands" << eom;
1396  throw 0;
1397  }
1398 
1399  copy(code, END_THREAD, dest);
1400 }
1401 
1403  const codet &code,
1404  goto_programt &dest)
1405 {
1406  if(!code.operands().empty())
1407  {
1408  err_location(code);
1409  error() << "atomic_begin expects no operands" << eom;
1410  throw 0;
1411  }
1412 
1413  copy(code, ATOMIC_BEGIN, dest);
1414 }
1415 
1417  const codet &code,
1418  goto_programt &dest)
1419 {
1420  if(!code.operands().empty())
1421  {
1422  err_location(code);
1423  error() << "atomic_end expects no operands" << eom;
1424  throw 0;
1425  }
1426 
1427  copy(code, ATOMIC_END, dest);
1428 }
1429 
1431  const codet &code,
1432  goto_programt &dest)
1433 {
1434  if(code.operands().size()!=2)
1435  {
1436  err_location(code);
1437  str << "bp_enfroce expects two arguments";
1438  error_msg();
1439  throw 0;
1440  }
1441 
1442  // do an assume
1443  exprt op=code.op0();
1444 
1445  clean_expr(op, dest);
1446 
1448  t->guard=op;
1449  t->source_location=code.source_location();
1450 
1451  // change the assignments
1452 
1453  goto_programt tmp;
1454  convert(to_code(code.op1()), tmp);
1455 
1456  if(!op.is_true())
1457  {
1458  exprt constraint(op);
1459  make_next_state(constraint);
1460 
1462  {
1463  if(it->is_assign())
1464  {
1465  assert(it->code.get(ID_statement)==ID_assign);
1466 
1467  // add constrain
1468  codet constrain(ID_bp_constrain);
1469  constrain.reserve_operands(2);
1470  constrain.move_to_operands(it->code);
1471  constrain.copy_to_operands(constraint);
1472  it->code.swap(constrain);
1473 
1474  it->type=OTHER;
1475  }
1476  else if(it->is_other() &&
1477  it->code.get(ID_statement)==ID_bp_constrain)
1478  {
1479  // add to constraint
1480  assert(it->code.operands().size()==2);
1481  it->code.op1()=
1482  and_exprt(it->code.op1(), constraint);
1483  }
1484  }
1485  }
1486 
1487  dest.destructive_append(tmp);
1488 }
1489 
1491  const codet &code,
1492  goto_programt &dest)
1493 {
1494  if(code.operands().size()!=1)
1495  {
1496  err_location(code);
1497  error() << "bp_abortif expects one argument" << eom;
1498  throw 0;
1499  }
1500 
1501  // do an assert
1502  exprt op=code.op0();
1503 
1504  clean_expr(op, dest);
1505 
1506  op.make_not();
1507 
1509  t->guard.swap(op);
1510  t->source_location=code.source_location();
1511 }
1512 
1514  const code_ifthenelset &code,
1515  goto_programt &dest)
1516 {
1517  if(code.operands().size()!=3)
1518  {
1519  err_location(code);
1520  error() << "ifthenelse takes three operands" << eom;
1521  throw 0;
1522  }
1523 
1524  assert(code.then_case().is_not_nil());
1525 
1526  bool has_else=
1527  !code.else_case().is_nil();
1528 
1529  const source_locationt &source_location=code.source_location();
1530 
1531  // We do a bit of special treatment for && in the condition
1532  // in case cleaning would be needed otherwise.
1533  if(code.cond().id()==ID_and &&
1534  code.cond().operands().size()==2 &&
1535  (needs_cleaning(code.cond().op0()) || needs_cleaning(code.cond().op1())) &&
1536  !has_else)
1537  {
1538  // if(a && b) XX --> if(a) if(b) XX
1539  code_ifthenelset new_if0, new_if1;
1540  new_if0.cond()=code.cond().op0();
1541  new_if1.cond()=code.cond().op1();
1542  new_if0.add_source_location()=source_location;
1543  new_if1.add_source_location()=source_location;
1544  new_if1.then_case()=code.then_case();
1545  new_if0.then_case()=new_if1;
1546  return convert_ifthenelse(new_if0, dest);
1547  }
1548 
1549  // convert 'then'-branch
1550  goto_programt tmp_then;
1551  convert(to_code(code.then_case()), tmp_then);
1552 
1553  goto_programt tmp_else;
1554 
1555  if(has_else)
1556  convert(to_code(code.else_case()), tmp_else);
1557 
1558  exprt tmp_guard=code.cond();
1559  clean_expr(tmp_guard, dest);
1560 
1561  generate_ifthenelse(tmp_guard, tmp_then, tmp_else, source_location, dest);
1562 }
1563 
1565  const exprt &expr,
1566  const irep_idt &id,
1567  std::list<exprt> &dest)
1568 {
1569  if(expr.id()!=id)
1570  {
1571  dest.push_back(expr);
1572  }
1573  else
1574  {
1575  // left-to-right is important
1576  forall_operands(it, expr)
1577  collect_operands(*it, id, dest);
1578  }
1579 }
1580 
1583  const exprt &guard,
1584  goto_programt &true_case,
1585  goto_programt &false_case,
1586  const source_locationt &source_location,
1587  goto_programt &dest)
1588 {
1589  if(is_empty(true_case) &&
1590  is_empty(false_case))
1591  return;
1592 
1593  // do guarded gotos directly
1594  if(is_empty(false_case) &&
1595  // true_case.instructions.size()==1 optimised
1596  !true_case.instructions.empty() &&
1597  ++true_case.instructions.begin()==true_case.instructions.end() &&
1598  true_case.instructions.back().is_goto() &&
1599  true_case.instructions.back().guard.is_true() &&
1600  true_case.instructions.back().labels.empty())
1601  {
1602  // The above conjunction deliberately excludes the instance
1603  // if(some) { label: goto somewhere; }
1604  true_case.instructions.back().guard=guard;
1605  dest.destructive_append(true_case);
1606  return;
1607  }
1608 
1609  // similarly, do guarded assertions directly
1610  if(true_case.instructions.size()==1 &&
1611  true_case.instructions.back().is_assert() &&
1612  true_case.instructions.back().guard.is_false() &&
1613  true_case.instructions.back().labels.empty())
1614  {
1615  // The above conjunction deliberately excludes the instance
1616  // if(some) { label: assert(0); }
1617  true_case.instructions.back().guard=boolean_negate(guard);
1618  dest.destructive_append(true_case);
1619  true_case.instructions.clear();
1620  }
1621 
1622  // similarly, do guarded assertions directly
1623  if(false_case.instructions.size()==1 &&
1624  false_case.instructions.back().is_assert() &&
1625  false_case.instructions.back().guard.is_false() &&
1626  false_case.instructions.back().labels.empty())
1627  {
1628  // The above conjunction deliberately excludes the instance
1629  // if(some) ... else { label: assert(0); }
1630  false_case.instructions.back().guard=guard;
1631  dest.destructive_append(false_case);
1632  false_case.instructions.clear();
1633  }
1634 
1635  // Flip around if no 'true' case code.
1636  if(is_empty(true_case))
1637  return generate_ifthenelse(
1638  boolean_negate(guard), false_case, true_case, source_location, dest);
1639 
1640  bool has_else=!is_empty(false_case);
1641 
1642  // if(c) P;
1643  //--------------------
1644  // v: if(!c) goto z;
1645  // w: P;
1646  // z: ;
1647 
1648  // if(c) P; else Q;
1649  //--------------------
1650  // v: if(!c) goto y;
1651  // w: P;
1652  // x: goto z;
1653  // y: Q;
1654  // z: ;
1655 
1656  // do the x label
1657  goto_programt tmp_x;
1659 
1660  // do the z label
1661  goto_programt tmp_z;
1663  z->make_skip();
1664  z->source_location=source_location;
1665 
1666  // y: Q;
1667  goto_programt tmp_y;
1669  if(has_else)
1670  {
1671  tmp_y.swap(false_case);
1672  y=tmp_y.instructions.begin();
1673  }
1674 
1675  // v: if(!c) goto z/y;
1676  goto_programt tmp_v;
1678  boolean_negate(guard), has_else?y:z, source_location, tmp_v);
1679 
1680  // w: P;
1681  goto_programt tmp_w;
1682  tmp_w.swap(true_case);
1683 
1684  // x: goto z;
1685  x->make_goto(z);
1686  assert(!tmp_w.instructions.empty());
1687  x->source_location=tmp_w.instructions.back().source_location;
1688 
1689  dest.destructive_append(tmp_v);
1690  dest.destructive_append(tmp_w);
1691 
1692  if(has_else)
1693  {
1694  dest.destructive_append(tmp_x);
1695  dest.destructive_append(tmp_y);
1696  }
1697 
1698  dest.destructive_append(tmp_z);
1699 }
1700 
1702 static bool has_and_or(const exprt &expr)
1703 {
1704  forall_operands(it, expr)
1705  if(has_and_or(*it))
1706  return true;
1707 
1708  if(expr.id()==ID_and || expr.id()==ID_or)
1709  return true;
1710 
1711  return false;
1712 }
1713 
1715  const exprt &guard,
1716  goto_programt::targett target_true,
1717  const source_locationt &source_location,
1718  goto_programt &dest)
1719 {
1720  if(has_and_or(guard) && needs_cleaning(guard))
1721  {
1722  // if(guard) goto target;
1723  // becomes
1724  // if(guard) goto target; else goto next;
1725  // next: skip;
1726 
1727  goto_programt tmp;
1728  goto_programt::targett target_false=tmp.add_instruction();
1729  target_false->make_skip();
1730  target_false->source_location=source_location;
1731 
1733  guard, target_true, target_false, source_location, dest);
1734 
1735  dest.destructive_append(tmp);
1736  }
1737  else
1738  {
1739  // simple branch
1740  exprt cond=guard;
1741  clean_expr(cond, dest);
1742 
1743  goto_programt tmp;
1745  g->make_goto(target_true);
1746  g->guard=cond;
1747  g->source_location=source_location;
1748  dest.destructive_append(tmp);
1749  }
1750 }
1751 
1754  const exprt &guard,
1755  goto_programt::targett target_true,
1756  goto_programt::targett target_false,
1757  const source_locationt &source_location,
1758  goto_programt &dest)
1759 {
1760  if(guard.id()==ID_not)
1761  {
1762  assert(guard.operands().size()==1);
1763  // simply swap targets
1765  guard.op0(), target_false, target_true, source_location, dest);
1766  return;
1767  }
1768 
1769  if(guard.id()==ID_and)
1770  {
1771  // turn
1772  // if(a && b) goto target_true; else goto target_false;
1773  // into
1774  // if(!a) goto target_false;
1775  // if(!b) goto target_false;
1776  // goto target_true;
1777 
1778  std::list<exprt> op;
1779  collect_operands(guard, guard.id(), op);
1780 
1781  forall_expr_list(it, op)
1783  boolean_negate(*it), target_false, source_location, dest);
1784 
1786  t_true->make_goto(target_true);
1787  t_true->guard=true_exprt();
1788  t_true->source_location=source_location;
1789 
1790  return;
1791  }
1792  else if(guard.id()==ID_or)
1793  {
1794  // turn
1795  // if(a || b) goto target_true; else goto target_false;
1796  // into
1797  // if(a) goto target_true;
1798  // if(b) goto target_true;
1799  // goto target_false;
1800 
1801  std::list<exprt> op;
1802  collect_operands(guard, guard.id(), op);
1803 
1804  forall_expr_list(it, op)
1806  *it, target_true, source_location, dest);
1807 
1808  goto_programt::targett t_false=dest.add_instruction();
1809  t_false->make_goto(target_false);
1810  t_false->guard=true_exprt();
1811  t_false->source_location=guard.source_location();
1812 
1813  return;
1814  }
1815 
1816  exprt cond=guard;
1817  clean_expr(cond, dest);
1818 
1820  t_true->make_goto(target_true);
1821  t_true->guard=cond;
1822  t_true->source_location=source_location;
1823 
1824  goto_programt::targett t_false=dest.add_instruction();
1825  t_false->make_goto(target_false);
1826  t_false->guard=true_exprt();
1827  t_false->source_location=source_location;
1828 }
1829 
1831  const exprt &expr)
1832 {
1833  if(expr.id()==ID_typecast &&
1834  expr.operands().size()==1)
1835  return get_string_constant(expr.op0());
1836 
1837  if(expr.id()==ID_address_of &&
1838  expr.operands().size()==1 &&
1839  expr.op0().id()==ID_index &&
1840  expr.op0().operands().size()==2)
1841  {
1842  exprt index_op=get_constant(expr.op0().op0());
1843  simplify(index_op, ns);
1844 
1845  if(index_op.id()==ID_string_constant)
1846  return index_op.get(ID_value);
1847  else if(index_op.id()==ID_array)
1848  {
1849  std::string result;
1850  forall_operands(it, index_op)
1851  if(it->is_constant())
1852  {
1853  unsigned i=integer2long(
1855 
1856  if(i!=0) // to skip terminating 0
1857  result+=static_cast<char>(i);
1858  }
1859 
1860  return result;
1861  }
1862  }
1863 
1864  if(expr.id()==ID_string_constant)
1865  return expr.get(ID_value);
1866 
1867  err_location(expr);
1868  str << "expected string constant, but got: "
1869  << expr.pretty();
1870  error_msg();
1871 
1872  throw 0;
1873 }
1874 
1876 {
1877  if(expr.id()==ID_symbol)
1878  {
1879  const symbolt &symbol=
1880  ns.lookup(to_symbol_expr(expr));
1881 
1882  return symbol.value;
1883  }
1884  else if(expr.id()==ID_member)
1885  {
1886  exprt tmp=expr;
1887  tmp.op0()=get_constant(expr.op0());
1888  return tmp;
1889  }
1890  else if(expr.id()==ID_index)
1891  {
1892  exprt tmp=expr;
1893  tmp.op0()=get_constant(expr.op0());
1894  tmp.op1()=get_constant(expr.op1());
1895  return tmp;
1896  }
1897  else
1898  return expr;
1899 }
1900 
1902  const typet &type,
1903  const std::string &suffix,
1904  goto_programt &dest,
1905  const source_locationt &source_location)
1906 {
1907  auxiliary_symbolt new_symbol;
1908  symbolt *symbol_ptr;
1909 
1910  do
1911  {
1912  new_symbol.base_name="tmp_"+suffix+"$"+std::to_string(++temporary_counter);
1913  new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
1914  new_symbol.type=type;
1915  new_symbol.location=source_location;
1916  }
1917  while(symbol_table.move(new_symbol, symbol_ptr));
1918 
1919  tmp_symbols.push_back(symbol_ptr->name);
1920 
1922  t->code=code_declt(symbol_ptr->symbol_expr());
1923  t->source_location=source_location;
1924 
1925  return *symbol_ptr;
1926 }
1927 
1929  exprt &expr,
1930  const std::string &suffix,
1931  goto_programt &dest)
1932 {
1933  const source_locationt source_location=expr.find_source_location();
1934 
1935  symbolt &new_symbol=
1936  new_tmp_symbol(expr.type(), suffix, dest, source_location);
1937 
1938  code_assignt assignment;
1939  assignment.lhs()=new_symbol.symbol_expr();
1940  assignment.rhs()=expr;
1941  assignment.add_source_location()=source_location;
1942 
1943  convert(assignment, dest);
1944 
1945  expr=new_symbol.symbol_expr();
1946 }
1947 
1948 void goto_convertt::new_name(symbolt &symbol)
1949 {
1950  // rename it
1951  get_new_name(symbol, ns);
1952 
1953  // store in symbol_table
1954  symbol_table.add(symbol);
1955 }
1956 
1957 const symbolt &goto_convertt::lookup(const irep_idt &identifier) const
1958 {
1959  const symbolt *symbol;
1960  if(ns.lookup(identifier, symbol))
1961  {
1962  error() << "failed to find symbol " << identifier << eom;
1963  throw 0;
1964  }
1965  return *symbol;
1966 }
1967 
1969  const codet &code,
1970  symbol_tablet &symbol_table,
1971  goto_programt &dest,
1972  message_handlert &message_handler)
1973 {
1974  goto_convertt goto_convert(symbol_table, message_handler);
1975 
1976  try
1977  {
1978  goto_convert.goto_convert(code, dest);
1979  }
1980 
1981  catch(int)
1982  {
1983  goto_convert.error_msg();
1984  }
1985 
1986  catch(const char *e)
1987  {
1988  goto_convert.str << e;
1989  goto_convert.error_msg();
1990  }
1991 
1992  catch(const std::string &e)
1993  {
1994  goto_convert.str << e;
1995  goto_convert.error_msg();
1996  }
1997 
1998  if(goto_convert.get_error_found())
1999  throw 0;
2000 }
2001 
2003  symbol_tablet &symbol_table,
2004  goto_programt &dest,
2005  message_handlert &message_handler)
2006 {
2007  // find main symbol
2008  const symbol_tablet::symbolst::const_iterator s_it=
2009  symbol_table.symbols.find("main");
2010 
2011  if(s_it==symbol_table.symbols.end())
2012  {
2013  error() << "failed to find main symbol" << eom;
2014  throw 0;
2015  }
2016 
2017  const symbolt &symbol=s_it->second;
2018 
2019  ::goto_convert(to_code(symbol.value), symbol_table, dest, message_handler);
2020 }
void convert_atomic_begin(const codet &code, goto_programt &dest)
const irep_idt & get_statement() const
Definition: std_code.h:37
void convert_specc_event(const exprt &op, std::set< irep_idt > &events)
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
void convert_skip(const codet &code, goto_programt &dest)
const codet & then_case() const
Definition: std_code.h:370
mstreamt & result()
Definition: message.h:233
void convert_gcc_switch_case_range(const codet &code, goto_programt &dest)
goto_program_instruction_typet
The type of an instruction in a GOTO program.
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:218
exprt & true_case()
Definition: std_expr.h:2805
semantic type conversion
Definition: std_expr.h:1725
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
exprt::operandst caset
targett add_instruction()
Adds an instruction at the end.
A ‘switch’ instruction.
Definition: std_code.h:412
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
void convert(const codet &code, goto_programt &dest)
converts &#39;code&#39; and appends the result to &#39;dest&#39;
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
const exprt & init() const
Definition: std_code.h:556
symbol_tablet & symbol_table
goto_programt::targett return_target
exprt & op0()
Definition: expr.h:84
void unwind_destructor_stack(const source_locationt &, std::size_t stack_size, goto_programt &dest)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:298
const exprt & cond() const
Definition: std_code.h:465
A continue for ‘for’ and ‘while’ loops.
Definition: std_code.h:898
void convert_ifthenelse(const code_ifthenelset &code, goto_programt &dest)
virtual void do_function_call(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
struct goto_convertt::targetst targets
const exprt & cond() const
Definition: std_code.h:360
const codet & body() const
Definition: std_code.h:586
instructionst instructions
The list of instructions in the goto program.
goto_programt::targett break_target
codet & code()
Definition: std_code.h:851
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
source_locationt end_location() const
Definition: std_code.h:89
#define forall_expr(it, expr)
Definition: expr.h:28
Destructor Calls.
void convert_gcc_computed_goto(const codet &code, goto_programt &dest)
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
void convert_atomic_end(const codet &code, goto_programt &dest)
const irep_idt & get_value() const
Definition: std_expr.h:3702
const code_breakt & to_code_break(const codet &code)
Definition: std_code.h:884
void convert_assign(const code_assignt &code, goto_programt &dest)
void convert_dowhile(const codet &code, goto_programt &dest)
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
exprt value
Initial value of symbol.
Definition: symbol.h:40
void convert_init(const codet &code, goto_programt &dest)
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt & cond()
Definition: std_expr.h:2795
bool is_true() const
Definition: expr.cpp:133
void convert_goto(const codet &code, goto_programt &dest)
typet & type()
Definition: expr.h:60
The proper Booleans.
Definition: std_types.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
void convert_end_thread(const codet &code, goto_programt &dest)
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
void goto_convert(const codet &code, symbol_tablet &symbol_table, goto_programt &dest, message_handlert &message_handler)
An expression statement.
Definition: std_code.h:957
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:981
void set_default(goto_programt::targett _default_target)
bool is_static_lifetime
Definition: symbol.h:70
const exprt & case_op() const
Definition: std_code.h:841
subt & get_sub()
Definition: irep.h:245
void convert_specc_wait(const codet &code, goto_programt &dest)
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1023
equality
Definition: std_expr.h:1082
destructor_stackt destructor_stack
static void collect_operands(const exprt &expr, const irep_idt &id, std::list< exprt > &dest)
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
void goto_convert(const codet &code, goto_programt &dest)
const irep_idt & id() const
Definition: irep.h:189
void convert_switch(const code_switcht &code, goto_programt &dest)
exprt & lhs()
Definition: std_code.h:157
void convert_decl_type(const codet &code, goto_programt &dest)
void do_java_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
The boolean constant true.
Definition: std_expr.h:3742
irep_idt get_string_constant(const exprt &expr)
argumentst & arguments()
Definition: std_code.h:689
symbolst symbols
Definition: symbol_table.h:57
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
void make_next_state(exprt &expr)
Definition: expr_util.cpp:20
void convert_bp_abortif(const codet &code, goto_programt &dest)
void convert_for(const code_fort &code, goto_programt &dest)
std::string tmp_symbol_prefix
void convert_msc_try_finally(const codet &code, goto_programt &dest)
A declaration of a local variable.
Definition: std_code.h:192
static bool has_and_or(const exprt &expr)
if(guard) goto target;
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
exprt & rhs()
Definition: std_code.h:162
void convert_label(const code_labelt &code, goto_programt &dest)
const source_locationt & find_source_location() const
Definition: expr.cpp:466
const exprt & cond() const
Definition: std_code.h:566
The empty type.
Definition: std_types.h:53
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:486
Program Transformation.
goto_programt::targett default_target
exprt case_guard(const exprt &value, const caset &case_op)
boolean AND
Definition: std_expr.h:1852
API to expression classes.
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:52
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:137
void convert_specc_notify(const codet &code, goto_programt &dest)
void convert_continue(const code_continuet &code, goto_programt &dest)
void convert_while(const code_whilet &code, goto_programt &dest)
void convert_CPROVER_try_finally(const codet &code, goto_programt &dest)
A label for branch targets.
Definition: std_code.h:760
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:746
Base class for tree-like data structures with sharing.
Definition: irep.h:87
A function call.
Definition: std_code.h:657
#define forall_operands(it, expr)
Definition: expr.h:17
void convert_msc_leave(const codet &code, goto_programt &dest)
A ‘while’ instruction.
Definition: std_code.h:457
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:862
targett insert_after(const_targett target)
Insertion after the given target.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table.
void convert_asm(const code_asmt &code, goto_programt &dest)
Definition: goto_asm.cpp:14
void do_java_new_array(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
void convert_specc_par(const codet &code, goto_programt &dest)
void finish_computed_gotos(goto_programt &dest)
Operator to return the address of an object.
Definition: std_expr.h:2593
void convert_return(const code_returnt &code, goto_programt &dest)
void convert_cpp_delete(const codet &code, goto_programt &dest)
void clean_expr(exprt &expr, goto_programt &dest, bool result_is_used=true)
#define forall_expr_list(it, expr)
Definition: expr.h:36
exprt & false_case()
Definition: std_expr.h:2815
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
void goto_convert_rec(const codet &code, goto_programt &dest)
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:441
void convert_gcc_local_label(const codet &code, goto_programt &dest)
std::vector< exprt > operandst
Definition: expr.h:49
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
void convert_function_call(const code_function_callt &code, goto_programt &dest)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
void convert_assert(const code_assertt &code, goto_programt &dest)
An assertion.
Definition: std_code.h:312
void convert_CPROVER_try_catch(const codet &code, goto_programt &dest)
An assumption.
Definition: std_code.h:274
exprt get_constant(const exprt &expr)
void set_continue(goto_programt::targett _continue_target)
const exprt & value() const
Definition: std_code.h:420
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
const code_continuet & to_code_continue(const codet &code)
Definition: std_code.h:906
void make_not()
Definition: expr.cpp:100
static bool needs_cleaning(const exprt &expr)
goto_programt::targett continue_target
void convert_decl(const code_declt &code, goto_programt &dest)
void new_name(symbolt &symbol)
void convert_try_catch(const codet &code, goto_programt &dest)
void generate_conditional_branch(const exprt &guard, goto_programt::targett target_true, goto_programt::targett target_false, const source_locationt &, goto_programt &dest)
if(guard) goto target_true; else goto target_false;
void set_break(goto_programt::targett _break_target)
exprt & function()
Definition: std_code.h:677
void set_statement(const irep_idt &statement)
Definition: std_code.h:32
bool is_default() const
Definition: std_code.h:831
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &)
Base class for all expressions.
Definition: expr.h:46
const symbolt & lookup(const irep_idt &identifier)
A break for ‘for’ and ‘while’ loops.
Definition: std_code.h:876
void finish_gotos(goto_programt &dest)
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
void convert_break(const code_breakt &code, goto_programt &dest)
void convert_switch_case(const code_switch_caset &code, goto_programt &dest)
const exprt & assumption() const
Definition: std_code.h:287
computed_gotost computed_gotos
const source_locationt & source_location() const
Definition: expr.h:142
const exprt & iter() const
Definition: std_code.h:576
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &)
static bool is_empty(const goto_programt &goto_program)
unsigned temporary_counter
Program Transformation.
void convert_assume(const code_assumet &code, goto_programt &dest)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void convert_block(const code_blockt &code, goto_programt &dest)
A removal of a local variable.
Definition: std_code.h:234
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
mstreamt & error()
Definition: message.h:223
source_locationt & add_source_location()
Definition: expr.h:147
Sequential composition.
Definition: std_code.h:63
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
const irep_idt & get_label() const
Definition: std_code.h:782
const code_fort & to_code_for(const codet &code)
Definition: std_code.h:597
An if-then-else.
Definition: std_code.h:350
Expression to hold a symbol (variable)
Definition: std_expr.h:82
exprt & op2()
Definition: expr.h:90
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:120
void destructive_append(goto_program_templatet< codeT, guardT > &p)
Appends the given program, which is destroyed.
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
A switch-case.
Definition: std_code.h:817
A statement in a programming language.
Definition: std_code.h:19
void convert_msc_try_except(const codet &code, goto_programt &dest)
Return from a function.
Definition: std_code.h:714
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
code_function_callt get_destructor(const namespacet &ns, const typet &type)
Definition: destructor.cpp:17
A ‘for’ instruction.
Definition: std_code.h:547
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:803
void convert_bp_enforce(const codet &code, goto_programt &dest)
const typet & subtype() const
Definition: type.h:31
const code_assertt & to_code_assert(const codet &code)
Definition: std_code.h:336
void convert_expression(const code_expressiont &code, goto_programt &dest)
operandst & operands()
Definition: expr.h:70
void convert_start_thread(const codet &code, goto_programt &dest)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
const codet & else_case() const
Definition: std_code.h:380
void get_new_name(symbolt &symbol, const namespacet &ns)
automated variable renaming
Definition: rename.cpp:20
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:396
void make_typecast(const typet &_type)
Definition: expr.cpp:90
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true ...
Definition: expr_util.cpp:120
static void replace_new_object(const exprt &object, exprt &dest)
const codet & body() const
Definition: std_code.h:475
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:943
Assignment.
Definition: std_code.h:144
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
void reserve_operands(operandst::size_type n)
Definition: expr.h:108
void swap(goto_program_templatet< codeT, guardT > &program)
Swap the goto program.
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700
void convert_CPROVER_throw(const codet &code, goto_programt &dest)
bool simplify(exprt &expr, const namespacet &ns)
const exprt & assertion() const
Definition: std_code.h:325
void generate_ifthenelse(const exprt &cond, goto_programt &true_case, goto_programt &false_case, const source_locationt &, goto_programt &dest)
if(guard) true_case; else false_case;
void convert_non_deterministic_goto(const codet &code, goto_programt &dest)
#define forall_irep(it, irep)
Definition: irep.h:62