CBMC
goto_convert_side_effect.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 <util/arith_tools.h>
15 #include <util/bitvector_expr.h>
16 #include <util/c_types.h>
17 #include <util/expr_util.h>
18 #include <util/fresh_symbol.h>
20 #include <util/std_expr.h>
21 #include <util/symbol.h>
22 
23 #include <ansi-c/c_expr.h>
24 
25 #include "destructor.h"
26 
28  side_effect_exprt &expr,
29  bool result_is_used,
30  bool address_taken,
31  const irep_idt &mode)
32 {
33  const irep_idt statement = expr.get_statement();
34 
35  std::optional<exprt> replacement_expr_opt;
36 
37  clean_expr_resultt side_effects;
38 
39  if(statement == ID_assign)
40  {
41  auto &old_assignment = to_side_effect_expr_assign(expr);
42  exprt new_lhs = skip_typecast(old_assignment.lhs());
43 
44  if(
45  result_is_used && !address_taken &&
46  assignment_lhs_needs_temporary(old_assignment.lhs()))
47  {
48  if(!old_assignment.rhs().is_constant())
49  {
50  side_effects.add_temporary(make_temp_symbol(
51  old_assignment.rhs(), "assign", side_effects.side_effects, mode));
52  }
53 
54  replacement_expr_opt =
55  typecast_exprt::conditional_cast(old_assignment.rhs(), new_lhs.type());
56  }
57 
58  exprt new_rhs =
59  typecast_exprt::conditional_cast(old_assignment.rhs(), new_lhs.type());
60  code_assignt new_assignment(std::move(new_lhs), std::move(new_rhs));
61  new_assignment.add_source_location() = expr.source_location();
62 
63  convert_assign(new_assignment, side_effects.side_effects, mode);
64  }
65  else if(
66  statement == ID_assign_plus || statement == ID_assign_minus ||
67  statement == ID_assign_mult || statement == ID_assign_div ||
68  statement == ID_assign_mod || statement == ID_assign_shl ||
69  statement == ID_assign_ashr || statement == ID_assign_lshr ||
70  statement == ID_assign_bitand || statement == ID_assign_bitxor ||
71  statement == ID_assign_bitor)
72  {
74  expr.operands().size() == 2,
75  id2string(statement) + " expects two arguments",
76  expr.find_source_location());
77 
78  irep_idt new_id;
79 
80  if(statement == ID_assign_plus)
81  new_id = ID_plus;
82  else if(statement == ID_assign_minus)
83  new_id = ID_minus;
84  else if(statement == ID_assign_mult)
85  new_id = ID_mult;
86  else if(statement == ID_assign_div)
87  new_id = ID_div;
88  else if(statement == ID_assign_mod)
89  new_id = ID_mod;
90  else if(statement == ID_assign_shl)
91  new_id = ID_shl;
92  else if(statement == ID_assign_ashr)
93  new_id = ID_ashr;
94  else if(statement == ID_assign_lshr)
95  new_id = ID_lshr;
96  else if(statement == ID_assign_bitand)
97  new_id = ID_bitand;
98  else if(statement == ID_assign_bitxor)
99  new_id = ID_bitxor;
100  else if(statement == ID_assign_bitor)
101  new_id = ID_bitor;
102  else
103  {
104  UNREACHABLE;
105  }
106 
107  const binary_exprt &binary_expr = to_binary_expr(expr);
108  exprt new_lhs = skip_typecast(binary_expr.op0());
109  const typet &op0_type = binary_expr.op0().type();
110 
111  PRECONDITION(
112  op0_type.id() != ID_c_enum_tag && op0_type.id() != ID_c_enum &&
113  op0_type.id() != ID_c_bool && op0_type.id() != ID_bool);
114 
115  exprt rhs = binary_exprt{binary_expr.op0(), new_id, binary_expr.op1()};
116  rhs.add_source_location() = expr.source_location();
117 
118  if(
119  result_is_used && !address_taken &&
120  assignment_lhs_needs_temporary(binary_expr.op0()))
121  {
122  side_effects.add_temporary(
123  make_temp_symbol(rhs, "assign", side_effects.side_effects, mode));
124  replacement_expr_opt =
125  typecast_exprt::conditional_cast(rhs, new_lhs.type());
126  }
127 
128  rhs = typecast_exprt::conditional_cast(rhs, new_lhs.type());
129  rhs.add_source_location() = expr.source_location();
130  code_assignt assignment(new_lhs, rhs);
131  assignment.add_source_location() = expr.source_location();
132 
133  convert(assignment, side_effects.side_effects, mode);
134  }
135  else
136  UNREACHABLE;
137 
138  // revert assignment in the expression to its LHS
139  if(replacement_expr_opt.has_value())
140  {
141  exprt new_lhs =
142  typecast_exprt::conditional_cast(*replacement_expr_opt, expr.type());
143  expr.swap(new_lhs);
144 
145  return side_effects;
146  }
147 
148  destruct_locals(side_effects.temporaries, side_effects.side_effects, ns);
149  side_effects.temporaries.clear();
150 
151  if(result_is_used)
152  {
153  exprt lhs = to_binary_expr(expr).op0();
154  // assign_* statements can have an lhs operand with a different type than
155  // that of the overall expression, because of integer promotion (which may
156  // have introduced casts to the lhs).
157  if(expr.type() != lhs.type())
158  {
159  // Skip over those type casts, but also
160  // make sure the resulting expression has the same type as before.
162  lhs.id() == ID_typecast,
163  id2string(expr.id()) +
164  " expression with different operand type expected to have a "
165  "typecast");
167  to_typecast_expr(lhs).op().type() == expr.type(),
168  id2string(expr.id()) + " type mismatch in lhs operand");
169  lhs = to_typecast_expr(lhs).op();
170  }
171  expr.swap(lhs);
172  }
173  else
174  expr.make_nil();
175 
176  return side_effects;
177 }
178 
180  side_effect_exprt &expr,
181  bool result_is_used,
182  bool address_taken,
183  const irep_idt &mode)
184 {
186  expr.operands().size() == 1,
187  "preincrement/predecrement must have one operand",
188  expr.find_source_location());
189 
190  const irep_idt statement = expr.get_statement();
191 
193  statement == ID_preincrement || statement == ID_predecrement,
194  "expects preincrement or predecrement");
195 
196  const auto &op = to_unary_expr(expr).op();
197  const typet &op_type = op.type();
198 
199  PRECONDITION(
200  op_type.id() != ID_c_enum_tag && op_type.id() != ID_c_enum &&
201  op_type.id() != ID_c_bool && op_type.id() != ID_bool);
202 
203  typet constant_type;
204 
205  if(op_type.id() == ID_pointer)
206  constant_type = c_index_type();
207  else if(is_number(op_type))
208  constant_type = op_type;
209  else
210  {
211  UNREACHABLE;
212  }
213 
214  exprt constant;
215 
216  if(constant_type.id() == ID_complex)
217  {
218  exprt real = from_integer(1, to_complex_type(constant_type).subtype());
219  exprt imag = from_integer(0, to_complex_type(constant_type).subtype());
220  constant = complex_exprt(real, imag, to_complex_type(constant_type));
221  }
222  else
223  constant = from_integer(1, constant_type);
224 
225  exprt rhs = binary_exprt{
226  op, statement == ID_preincrement ? ID_plus : ID_minus, std::move(constant)};
227  rhs.add_source_location() = expr.source_location();
228 
229  // Is there a typecast, e.g., for _Bool? If so, transform
230  // t1(op : t2) := op+1 --> op := t2(op+1)
231  exprt lhs;
232  if(op.id() == ID_typecast)
233  {
234  lhs = to_typecast_expr(op).op();
235  rhs = typecast_exprt(rhs, lhs.type());
236  }
237  else
238  {
239  lhs = op;
240  }
241 
242  const bool cannot_use_lhs =
243  result_is_used && !address_taken && assignment_lhs_needs_temporary(lhs);
244  clean_expr_resultt side_effects;
245  if(cannot_use_lhs)
246  side_effects.add_temporary(
247  make_temp_symbol(rhs, "pre", side_effects.side_effects, mode));
248 
249  code_assignt assignment(lhs, rhs);
250  assignment.add_source_location() = expr.find_source_location();
251 
252  convert(assignment, side_effects.side_effects, mode);
253 
254  if(result_is_used)
255  {
256  if(cannot_use_lhs)
257  {
258  auto tmp = typecast_exprt::conditional_cast(rhs, expr.type());
259  expr.swap(tmp);
260  }
261  else
262  {
263  // revert to argument of pre-inc/pre-dec
264  auto tmp = typecast_exprt::conditional_cast(lhs, expr.type());
265  expr.swap(tmp);
266  }
267  }
268  else
269  expr.make_nil();
270 
271  return side_effects;
272 }
273 
275  side_effect_exprt &expr,
276  const irep_idt &mode,
277  bool result_is_used)
278 {
279  goto_programt tmp1, tmp2;
280 
281  // we have ...(op++)...
282 
284  expr.operands().size() == 1,
285  "postincrement/postdecrement must have one operand",
286  expr.find_source_location());
287 
288  const irep_idt statement = expr.get_statement();
289 
291  statement == ID_postincrement || statement == ID_postdecrement,
292  "expects postincrement or postdecrement");
293 
294  const auto &op = to_unary_expr(expr).op();
295  const typet &op_type = op.type();
296 
297  PRECONDITION(
298  op_type.id() != ID_c_enum_tag && op_type.id() != ID_c_enum &&
299  op_type.id() != ID_c_bool && op_type.id() != ID_bool);
300 
301  typet constant_type;
302 
303  if(op_type.id() == ID_pointer)
304  constant_type = c_index_type();
305  else if(is_number(op_type))
306  constant_type = op_type;
307  else
308  {
309  UNREACHABLE;
310  }
311 
312  exprt constant;
313 
314  if(constant_type.id() == ID_complex)
315  {
316  exprt real = from_integer(1, to_complex_type(constant_type).subtype());
317  exprt imag = from_integer(0, to_complex_type(constant_type).subtype());
318  constant = complex_exprt(real, imag, to_complex_type(constant_type));
319  }
320  else
321  constant = from_integer(1, constant_type);
322 
323  binary_exprt rhs{
324  op,
325  statement == ID_postincrement ? ID_plus : ID_minus,
326  std::move(constant)};
327  rhs.add_source_location() = expr.source_location();
328 
329  code_assignt assignment(op, rhs);
330  assignment.add_source_location() = expr.find_source_location();
331 
332  convert(assignment, tmp2, mode);
333 
334  // fix up the expression, if needed
335 
336  clean_expr_resultt side_effects;
337 
338  if(result_is_used)
339  {
340  exprt tmp = op;
341  std::string suffix = "post";
342  if(auto sym_expr = expr_try_dynamic_cast<symbol_exprt>(tmp))
343  {
344  const irep_idt &base_name = ns.lookup(*sym_expr).base_name;
345  suffix += "_" + id2string(base_name);
346  }
347 
348  side_effects.add_temporary(
349  make_temp_symbol(tmp, suffix, side_effects.side_effects, mode));
350  expr.swap(tmp);
351  }
352  else
353  expr.make_nil();
354 
355  side_effects.side_effects.destructive_append(tmp1);
356  side_effects.side_effects.destructive_append(tmp2);
357 
358  return side_effects;
359 }
360 
363  const irep_idt &mode,
364  bool result_is_used)
365 {
366  clean_expr_resultt side_effects;
367 
368  if(!result_is_used)
369  {
370  code_function_callt call(expr.function(), expr.arguments());
371  call.add_source_location() = expr.source_location();
372  convert_function_call(call, side_effects.side_effects, mode);
373  expr.make_nil();
374  return side_effects;
375  }
376 
377  // get name of function, if available
378  std::string new_base_name = "return_value";
379  irep_idt new_symbol_mode = mode;
380 
381  if(expr.function().id() == ID_symbol)
382  {
383  const irep_idt &identifier =
385  const symbolt &symbol = ns.lookup(identifier);
386 
387  new_base_name += '_';
388  new_base_name += id2string(symbol.base_name);
389  new_symbol_mode = symbol.mode;
390  }
391 
392  const symbolt &new_symbol = get_fresh_aux_symbol(
393  expr.type(),
395  new_base_name,
396  expr.find_source_location(),
397  new_symbol_mode,
398  symbol_table);
399 
400  PRECONDITION(expr.type().id() != ID_code);
401  side_effects.side_effects.add(
402  goto_programt::make_decl(new_symbol.symbol_expr(), new_symbol.location));
403 
404  {
405  goto_programt tmp_program2;
406  code_function_callt call(
407  new_symbol.symbol_expr(), expr.function(), expr.arguments());
408  call.add_source_location() = new_symbol.location;
409  convert_function_call(call, side_effects.side_effects, mode);
410  }
411 
412  static_cast<exprt &>(expr) = new_symbol.symbol_expr();
413 
414  side_effects.add_temporary(to_symbol_expr(expr).get_identifier());
415 
416  return side_effects;
417 }
418 
420 {
421  if(dest.id() == "new_object")
422  dest = object;
423  else
424  Forall_operands(it, dest)
425  replace_new_object(object, *it);
426 }
427 
430 {
431  const symbolt &new_symbol = get_fresh_aux_symbol(
432  expr.type(),
434  "new_ptr",
435  expr.find_source_location(),
436  ID_cpp,
437  symbol_table);
438 
439  clean_expr_resultt side_effects;
440 
441  PRECONDITION(expr.type().id() != ID_code);
442  side_effects.side_effects.add(
443  goto_programt::make_decl(new_symbol.symbol_expr(), new_symbol.location));
444 
445  const code_assignt call(new_symbol.symbol_expr(), expr);
446 
447  convert(call, side_effects.side_effects, ID_cpp);
448 
449  if(result_is_used)
450  {
451  static_cast<exprt &>(expr) = new_symbol.symbol_expr();
452  side_effects.add_temporary(to_symbol_expr(expr).get_identifier());
453  }
454  else
455  expr.make_nil();
456 
457  return side_effects;
458 }
459 
462 {
463  DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expects one operand");
464 
465  codet tmp(expr.get_statement());
466  tmp.add_source_location() = expr.source_location();
467  tmp.copy_to_operands(to_unary_expr(expr).op());
468  tmp.set(ID_destructor, expr.find(ID_destructor));
469 
470  clean_expr_resultt side_effects;
471  convert_cpp_delete(tmp, side_effects.side_effects);
472 
473  expr.make_nil();
474 
475  return side_effects;
476 }
477 
479  side_effect_exprt &expr,
480  const irep_idt &mode,
481  bool result_is_used)
482 {
483  clean_expr_resultt side_effects;
484 
485  if(result_is_used)
486  {
487  const symbolt &new_symbol = get_fresh_aux_symbol(
488  expr.type(),
490  "malloc_value",
491  expr.source_location(),
492  mode,
493  symbol_table);
494 
495  code_frontend_declt decl(new_symbol.symbol_expr());
496  decl.add_source_location() = new_symbol.location;
497  convert_frontend_decl(decl, side_effects.side_effects, mode);
498 
499  code_assignt call(new_symbol.symbol_expr(), expr);
500  call.add_source_location() = expr.source_location();
501 
502  static_cast<exprt &>(expr) = new_symbol.symbol_expr();
503 
504  convert(call, side_effects.side_effects, mode);
505 
506  side_effects.add_temporary(to_symbol_expr(expr).get_identifier());
507  }
508  else
509  convert(code_expressiont(std::move(expr)), side_effects.side_effects, mode);
510 
511  return side_effects;
512 }
513 
516 {
517  clean_expr_resultt side_effects;
518 
519  const irep_idt &mode = expr.get(ID_mode);
521  expr.operands().size() <= 1,
522  "temporary_object takes zero or one operands",
523  expr.find_source_location());
524 
525  symbolt &new_symbol = new_tmp_symbol(
526  expr.type(),
527  "obj",
528  side_effects.side_effects,
529  expr.find_source_location(),
530  mode);
531 
532  if(expr.operands().size() == 1)
533  {
534  const code_assignt assignment(
535  new_symbol.symbol_expr(), to_unary_expr(expr).op());
536 
537  convert(assignment, side_effects.side_effects, mode);
538  }
539 
540  if(expr.find(ID_initializer).is_not_nil())
541  {
543  expr.operands().empty(),
544  "temporary_object takes zero operands",
545  expr.find_source_location());
546  exprt initializer = static_cast<const exprt &>(expr.find(ID_initializer));
547  replace_new_object(new_symbol.symbol_expr(), initializer);
548 
549  convert(to_code(initializer), side_effects.side_effects, mode);
550  }
551 
552  static_cast<exprt &>(expr) = new_symbol.symbol_expr();
553 
554  side_effects.add_temporary(to_symbol_expr(expr).get_identifier());
555 
556  return side_effects;
557 }
558 
560  side_effect_exprt &expr,
561  const irep_idt &mode,
562  bool result_is_used)
563 {
564  clean_expr_resultt side_effects;
565 
566  // This is a gcc extension of the form ({ ....; expr; })
567  // The value is that of the final expression.
568  // The expression is copied into a temporary before the
569  // scope is destroyed.
570 
572 
573  if(!result_is_used)
574  {
575  convert(code, side_effects.side_effects, mode);
576  expr.make_nil();
577  return side_effects;
578  }
579 
581  code.get_statement() == ID_block,
582  "statement_expression takes block as operand",
583  code.find_source_location());
584 
586  !code.operands().empty(),
587  "statement_expression takes non-empty block as operand",
588  expr.find_source_location());
589 
590  // get last statement from block, following labels
591  codet &last = to_code_block(code).find_last_statement();
592 
593  source_locationt source_location = last.find_source_location();
594 
595  symbolt &new_symbol = new_tmp_symbol(
596  expr.type(),
597  "statement_expression",
598  side_effects.side_effects,
599  source_location,
600  mode);
601 
602  symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type);
603  tmp_symbol_expr.add_source_location() = source_location;
604 
605  if(last.get(ID_statement) == ID_expression)
606  {
607  // we turn this into an assignment
608  exprt e = to_code_expression(last).expression();
609  last = code_assignt(tmp_symbol_expr, e);
610  last.add_source_location() = source_location;
611  }
612  else if(last.get(ID_statement) == ID_assign)
613  {
614  exprt e = to_code_assign(last).lhs();
615  code_assignt assignment(tmp_symbol_expr, e);
616  assignment.add_source_location() = source_location;
617  code.operands().push_back(assignment);
618  }
619  else
620  {
621  UNREACHABLE;
622  }
623 
624  convert(code, side_effects.side_effects, mode);
625 
626  static_cast<exprt &>(expr) = tmp_symbol_expr;
627 
628  side_effects.add_temporary(to_symbol_expr(expr).get_identifier());
629 
630  return side_effects;
631 }
632 
635  bool result_is_used,
636  const irep_idt &mode)
637 {
638  const irep_idt &statement = expr.get_statement();
639  const exprt &lhs = expr.lhs();
640  const exprt &rhs = expr.rhs();
641  const exprt &result = expr.result();
642 
643  clean_expr_resultt side_effects;
644 
645  if(result.type().id() != ID_pointer)
646  {
647  // result of the arithmetic operation is _not_ used, just evaluate side
648  // effects
649  exprt tmp = result;
650  side_effects.add(clean_expr(tmp, mode, false));
651 
652  // the is-there-an-overflow result may be used
653  if(result_is_used)
654  {
655  binary_overflow_exprt overflow_check{
657  statement,
659  overflow_check.add_source_location() = expr.source_location();
660  expr.swap(overflow_check);
661  }
662  else
663  expr.make_nil();
664  }
665  else
666  {
667  const typet &arith_type = to_pointer_type(result.type()).base_type();
668  irep_idt arithmetic_operation = statement == ID_overflow_plus ? ID_plus
669  : statement == ID_overflow_minus ? ID_minus
670  : statement == ID_overflow_mult ? ID_mult
671  : ID_nil;
672  CHECK_RETURN(arithmetic_operation != ID_nil);
673  exprt overflow_with_result = overflow_result_exprt{
674  typecast_exprt::conditional_cast(lhs, arith_type),
675  arithmetic_operation,
676  typecast_exprt::conditional_cast(rhs, arith_type)};
677  overflow_with_result.add_source_location() = expr.source_location();
678 
679  if(result_is_used)
680  {
681  side_effects.add_temporary(make_temp_symbol(
682  overflow_with_result,
683  "overflow_result",
684  side_effects.side_effects,
685  mode));
686  }
687 
688  const struct_typet::componentst &result_comps =
689  to_struct_type(overflow_with_result.type()).components();
690  CHECK_RETURN(result_comps.size() == 2);
691  code_assignt result_assignment{
694  member_exprt{overflow_with_result, result_comps[0]}, arith_type),
695  expr.source_location()};
696  convert_assign(result_assignment, side_effects.side_effects, mode);
697 
698  if(result_is_used)
699  {
700  member_exprt overflow_check{overflow_with_result, result_comps[1]};
701  overflow_check.add_source_location() = expr.source_location();
702 
703  expr.swap(overflow_check);
704  }
705  else
706  expr.make_nil();
707  }
708 
709  return side_effects;
710 }
711 
713  side_effect_exprt &expr,
714  const irep_idt &mode,
715  bool result_is_used,
716  bool address_taken)
717 {
718  const irep_idt &statement = expr.get_statement();
719 
720  if(statement == ID_function_call)
721  {
722  return remove_function_call(
723  to_side_effect_expr_function_call(expr), mode, result_is_used);
724  }
725  else if(
726  statement == ID_assign || statement == ID_assign_plus ||
727  statement == ID_assign_minus || statement == ID_assign_mult ||
728  statement == ID_assign_div || statement == ID_assign_bitor ||
729  statement == ID_assign_bitxor || statement == ID_assign_bitand ||
730  statement == ID_assign_lshr || statement == ID_assign_ashr ||
731  statement == ID_assign_shl || statement == ID_assign_mod)
732  {
733  return remove_assignment(expr, result_is_used, address_taken, mode);
734  }
735  else if(statement == ID_postincrement || statement == ID_postdecrement)
736  {
737  return remove_post(expr, mode, result_is_used);
738  }
739  else if(statement == ID_preincrement || statement == ID_predecrement)
740  {
741  return remove_pre(expr, result_is_used, address_taken, mode);
742  }
743  else if(statement == ID_cpp_new || statement == ID_cpp_new_array)
744  {
745  return remove_cpp_new(expr, result_is_used);
746  }
747  else if(statement == ID_cpp_delete || statement == ID_cpp_delete_array)
748  {
749  return remove_cpp_delete(expr);
750  }
751  else if(statement == ID_allocate)
752  {
753  return remove_malloc(expr, mode, result_is_used);
754  }
755  else if(statement == ID_temporary_object)
756  {
757  return remove_temporary_object(expr);
758  }
759  else if(statement == ID_statement_expression)
760  {
761  return remove_statement_expression(expr, mode, result_is_used);
762  }
763  else if(statement == ID_nondet)
764  {
765  // these are fine
766  return {};
767  }
768  else if(statement == ID_skip)
769  {
770  expr.make_nil();
771  return {};
772  }
773  else if(statement == ID_throw)
774  {
775  clean_expr_resultt side_effects;
776 
778  expr.find(ID_exception_list), expr.type(), expr.source_location()));
779  code.op0().operands().swap(expr.operands());
780  code.add_source_location() = expr.source_location();
782  std::move(code), expr.source_location(), THROW, nil_exprt(), {}));
783 
784  // the result can't be used, these are void
785  expr.make_nil();
786  return side_effects;
787  }
788  else if(
789  statement == ID_overflow_plus || statement == ID_overflow_minus ||
790  statement == ID_overflow_mult)
791  {
792  return remove_overflow(
793  to_side_effect_expr_overflow(expr), result_is_used, mode);
794  }
795  else
796  {
797  UNREACHABLE;
798  }
799 }
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
API to expression classes for bitvectors.
API to expression classes that are internal to the C frontend.
const side_effect_expr_overflowt & to_side_effect_expr_overflow(const exprt &expr)
Cast an exprt to a side_effect_expr_overflowt.
Definition: c_expr.h:183
bitvector_typet c_index_type()
Definition: c_types.cpp:16
A base class for binary expressions.
Definition: std_expr.h:638
exprt & op1()
Definition: expr.h:136
exprt & op0()
Definition: expr.h:133
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A goto_instruction_codet representing an assignment in the program.
codet & find_last_statement()
Definition: std_code.cpp:96
codet representation of an expression statement.
Definition: std_code.h:1394
const exprt & expression() const
Definition: std_code.h:1401
A codet representing the declaration of a local variable.
Definition: std_code.h:347
goto_instruction_codet representation of a function call statement.
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt & op0()
Definition: expr.h:133
const irep_idt & get_statement() const
Definition: std_code_base.h:65
Complex constructor from a pair of numbers.
Definition: std_expr.h:1916
Operator to dereference a pointer.
Definition: pointer_expr.h:834
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:147
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:163
source_locationt & add_source_location()
Definition: expr.h:236
const source_locationt & source_location() const
Definition: expr.h:231
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
symbol_table_baset & symbol_table
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
clean_expr_resultt remove_pre(side_effect_exprt &expr, bool result_is_used, bool address_taken, const irep_idt &mode)
clean_expr_resultt remove_post(side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)
std::string tmp_symbol_prefix
void convert_frontend_decl(const code_frontend_declt &, goto_programt &, const irep_idt &mode)
void convert_function_call(const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
clean_expr_resultt remove_assignment(side_effect_exprt &expr, bool result_is_used, bool address_taken, const irep_idt &mode)
void convert_cpp_delete(const codet &code, goto_programt &dest)
clean_expr_resultt remove_malloc(side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)
clean_expr_resultt remove_side_effect(side_effect_exprt &expr, const irep_idt &mode, bool result_is_used, bool address_taken)
irep_idt make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)
clean_expr_resultt remove_cpp_new(side_effect_exprt &expr, bool result_is_used)
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
clean_expr_resultt remove_temporary_object(side_effect_exprt &expr)
clean_expr_resultt remove_function_call(side_effect_expr_function_callt &expr, const irep_idt &mode, bool result_is_used)
static void replace_new_object(const exprt &object, exprt &dest)
clean_expr_resultt remove_cpp_delete(side_effect_exprt &expr)
clean_expr_resultt remove_statement_expression(side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)
clean_expr_resultt clean_expr(exprt &expr, const irep_idt &mode, bool result_is_used=true)
clean_expr_resultt remove_overflow(side_effect_expr_overflowt &expr, bool result_is_used, const irep_idt &mode)
static bool assignment_lhs_needs_temporary(const exprt &lhs)
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:722
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:739
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:964
const irept & find(const irep_idt &name) const
Definition: irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:412
bool is_not_nil() const
Definition: irep.h:372
const irep_idt & id() const
Definition: irep.h:388
void make_nil()
Definition: irep.h:446
void swap(irept &irep)
Definition: irep.h:434
Extract member of struct or union.
Definition: std_expr.h:2849
mstreamt & result() const
Definition: message.h:401
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
The NIL expression.
Definition: std_expr.h:3086
An expression returning both the result of the arithmetic operation under wrap-around semantics as we...
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:1692
exprt::operandst & arguments()
Definition: std_code.h:1718
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
Definition: c_expr.h:118
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:1757
An expression containing a side effect.
Definition: std_code.h:1450
const irep_idt & get_statement() const
Definition: std_code.h:1472
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt mode
Language mode.
Definition: symbol.h:49
Semantic type conversion.
Definition: std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2081
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:391
void destruct_locals(const std::list< irep_idt > &vars, goto_programt &dest, const namespacet &ns)
Definition: destructor.cpp:62
Destructor Calls.
#define Forall_operands(it, expr)
Definition: expr.h:27
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:193
Deprecated expression utility functions.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
Program Transformation.
const code_assignt & to_code_assign(const goto_instruction_codet &code)
@ THROW
Definition: goto_program.h:50
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Mathematical types.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
Definition: invariant.h:437
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
Definition: std_code.h:1669
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1739
side_effect_expr_assignt & to_side_effect_expr_assign(exprt &expr)
Definition: std_code.h:1618
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1428
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:203
const codet & to_code(const exprt &expr)
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2107
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:715
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:426
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1155
std::list< irep_idt > temporaries
Identifiers of temporaries introduced while cleaning an expression.
void add(clean_expr_resultt &&other)
void add_temporary(const irep_idt &id)
goto_programt side_effects
Statements implementing side effects of the expression that was subject to cleaning.
Symbol table entry.