cprover
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/expr_util.h>
16 #include <util/fresh_symbol.h>
18 #include <util/std_expr.h>
19 #include <util/symbol.h>
20 
21 #include <util/c_types.h>
22 
23 #include <ansi-c/c_expr.h>
24 
26 {
27  forall_operands(it, expr)
28  if(has_function_call(*it))
29  return true;
30 
31  if(expr.id()==ID_side_effect &&
32  expr.get(ID_statement)==ID_function_call)
33  return true;
34 
35  return false;
36 }
37 
39  side_effect_exprt &expr,
40  goto_programt &dest,
41  bool result_is_used,
42  bool address_taken,
43  const irep_idt &mode)
44 {
45  const irep_idt statement=expr.get_statement();
46 
47  optionalt<exprt> replacement_expr_opt;
48 
49  if(statement==ID_assign)
50  {
51  auto &old_assignment = to_side_effect_expr_assign(expr);
52 
53  if(result_is_used && !address_taken && needs_cleaning(old_assignment.lhs()))
54  {
55  if(!old_assignment.rhs().is_constant())
56  make_temp_symbol(old_assignment.rhs(), "assign", dest, mode);
57 
58  replacement_expr_opt = old_assignment.rhs();
59  }
60 
61  exprt new_lhs = skip_typecast(old_assignment.lhs());
62  exprt new_rhs =
63  typecast_exprt::conditional_cast(old_assignment.rhs(), new_lhs.type());
64  code_assignt new_assignment(std::move(new_lhs), std::move(new_rhs));
65  new_assignment.add_source_location() = expr.source_location();
66 
67  convert_assign(new_assignment, dest, mode);
68  }
69  else if(statement==ID_assign_plus ||
70  statement==ID_assign_minus ||
71  statement==ID_assign_mult ||
72  statement==ID_assign_div ||
73  statement==ID_assign_mod ||
74  statement==ID_assign_shl ||
75  statement==ID_assign_ashr ||
76  statement==ID_assign_lshr ||
77  statement==ID_assign_bitand ||
78  statement==ID_assign_bitxor ||
79  statement==ID_assign_bitor)
80  {
82  expr.operands().size() == 2,
83  id2string(statement) + " expects two arguments",
84  expr.find_source_location());
85 
86  irep_idt new_id;
87 
88  if(statement==ID_assign_plus)
89  new_id=ID_plus;
90  else if(statement==ID_assign_minus)
91  new_id=ID_minus;
92  else if(statement==ID_assign_mult)
93  new_id=ID_mult;
94  else if(statement==ID_assign_div)
95  new_id=ID_div;
96  else if(statement==ID_assign_mod)
97  new_id=ID_mod;
98  else if(statement==ID_assign_shl)
99  new_id=ID_shl;
100  else if(statement==ID_assign_ashr)
101  new_id=ID_ashr;
102  else if(statement==ID_assign_lshr)
103  new_id=ID_lshr;
104  else if(statement==ID_assign_bitand)
105  new_id=ID_bitand;
106  else if(statement==ID_assign_bitxor)
107  new_id=ID_bitxor;
108  else if(statement==ID_assign_bitor)
109  new_id=ID_bitor;
110  else
111  {
112  UNREACHABLE;
113  }
114 
115  exprt rhs;
116 
117  const typet &op0_type = to_binary_expr(expr).op0().type();
118 
119  PRECONDITION(
120  op0_type.id() != ID_c_enum_tag && op0_type.id() != ID_c_enum &&
121  op0_type.id() != ID_c_bool && op0_type.id() != ID_bool);
122 
123  rhs.id(new_id);
124  rhs.copy_to_operands(
125  to_binary_expr(expr).op0(), to_binary_expr(expr).op1());
126  rhs.type() = to_binary_expr(expr).op0().type();
127  rhs.add_source_location() = expr.source_location();
128 
129  if(
130  result_is_used && !address_taken &&
131  needs_cleaning(to_binary_expr(expr).op0()))
132  {
133  make_temp_symbol(rhs, "assign", dest, mode);
134  replacement_expr_opt = rhs;
135  }
136 
137  exprt new_lhs = skip_typecast(to_binary_expr(expr).op0());
138  rhs = typecast_exprt::conditional_cast(rhs, new_lhs.type());
139  rhs.add_source_location() = expr.source_location();
140  code_assignt assignment(new_lhs, rhs);
141  assignment.add_source_location()=expr.source_location();
142 
143  convert(assignment, dest, mode);
144  }
145  else
146  UNREACHABLE;
147 
148  // revert assignment in the expression to its LHS
149  if(replacement_expr_opt.has_value())
150  {
151  exprt new_lhs =
152  typecast_exprt::conditional_cast(*replacement_expr_opt, expr.type());
153  expr.swap(new_lhs);
154  }
155  else if(result_is_used)
156  {
157  exprt lhs = to_binary_expr(expr).op0();
158  // assign_* statements can have an lhs operand with a different type than
159  // that of the overall expression, because of integer promotion (which may
160  // have introduced casts to the lhs).
161  if(expr.type() != lhs.type())
162  {
163  // Skip over those type casts, but also
164  // make sure the resulting expression has the same type as before.
166  lhs.id() == ID_typecast,
167  id2string(expr.id()) +
168  " expression with different operand type expected to have a "
169  "typecast");
171  to_typecast_expr(lhs).op().type() == expr.type(),
172  id2string(expr.id()) + " type mismatch in lhs operand");
173  lhs = to_typecast_expr(lhs).op();
174  }
175  expr.swap(lhs);
176  }
177  else
178  expr.make_nil();
179 }
180 
182  side_effect_exprt &expr,
183  goto_programt &dest,
184  bool result_is_used,
185  bool address_taken,
186  const irep_idt &mode)
187 {
189  expr.operands().size() == 1,
190  "preincrement/predecrement must have one operand",
191  expr.find_source_location());
192 
193  const irep_idt statement=expr.get_statement();
194 
196  statement == ID_preincrement || statement == ID_predecrement,
197  "expects preincrement or predecrement");
198 
199  exprt rhs;
201 
202  if(statement==ID_preincrement)
203  rhs.id(ID_plus);
204  else
205  rhs.id(ID_minus);
206 
207  const auto &op = to_unary_expr(expr).op();
208  const typet &op_type = op.type();
209 
210  PRECONDITION(
211  op_type.id() != ID_c_enum_tag && op_type.id() != ID_c_enum &&
212  op_type.id() != ID_c_bool && op_type.id() != ID_bool);
213 
214  typet constant_type;
215 
216  if(op_type.id() == ID_pointer)
217  constant_type = index_type();
218  else if(is_number(op_type))
219  constant_type = op_type;
220  else
221  {
222  UNREACHABLE;
223  }
224 
225  exprt constant;
226 
227  if(constant_type.id() == ID_complex)
228  {
229  exprt real = from_integer(1, constant_type.subtype());
230  exprt imag = from_integer(0, constant_type.subtype());
231  constant = complex_exprt(real, imag, to_complex_type(constant_type));
232  }
233  else
234  constant = from_integer(1, constant_type);
235 
236  rhs.add_to_operands(op, std::move(constant));
237  rhs.type() = op.type();
238 
239  const bool cannot_use_lhs =
240  result_is_used && !address_taken && needs_cleaning(op);
241  if(cannot_use_lhs)
242  make_temp_symbol(rhs, "pre", dest, mode);
243 
244  code_assignt assignment(op, rhs);
245  assignment.add_source_location()=expr.find_source_location();
246 
247  convert(assignment, dest, mode);
248 
249  if(result_is_used)
250  {
251  if(cannot_use_lhs)
252  expr.swap(rhs);
253  else
254  {
255  // revert to argument of pre-inc/pre-dec
256  exprt tmp = op;
257  expr.swap(tmp);
258  }
259  }
260  else
261  expr.make_nil();
262 }
263 
265  side_effect_exprt &expr,
266  goto_programt &dest,
267  const irep_idt &mode,
268  bool result_is_used)
269 {
270  goto_programt tmp1, tmp2;
271 
272  // we have ...(op++)...
273 
275  expr.operands().size() == 1,
276  "postincrement/postdecrement must have one operand",
277  expr.find_source_location());
278 
279  const irep_idt statement=expr.get_statement();
280 
282  statement == ID_postincrement || statement == ID_postdecrement,
283  "expects postincrement or postdecrement");
284 
285  exprt rhs;
287 
288  if(statement==ID_postincrement)
289  rhs.id(ID_plus);
290  else
291  rhs.id(ID_minus);
292 
293  const auto &op = to_unary_expr(expr).op();
294  const typet &op_type = op.type();
295 
296  PRECONDITION(
297  op_type.id() != ID_c_enum_tag && op_type.id() != ID_c_enum &&
298  op_type.id() != ID_c_bool && op_type.id() != ID_bool);
299 
300  typet constant_type;
301 
302  if(op_type.id() == ID_pointer)
303  constant_type = index_type();
304  else if(is_number(op_type))
305  constant_type = op_type;
306  else
307  {
308  UNREACHABLE;
309  }
310 
311  exprt constant;
312 
313  if(constant_type.id() == ID_complex)
314  {
315  exprt real = from_integer(1, constant_type.subtype());
316  exprt imag = from_integer(0, constant_type.subtype());
317  constant = complex_exprt(real, imag, to_complex_type(constant_type));
318  }
319  else
320  constant = from_integer(1, constant_type);
321 
322  rhs.add_to_operands(op, std::move(constant));
323  rhs.type() = op.type();
324 
325  code_assignt assignment(op, rhs);
326  assignment.add_source_location()=expr.find_source_location();
327 
328  convert(assignment, tmp2, mode);
329 
330  // fix up the expression, if needed
331 
332  if(result_is_used)
333  {
334  exprt tmp = op;
335  make_temp_symbol(tmp, "post", dest, mode);
336  expr.swap(tmp);
337  }
338  else
339  expr.make_nil();
340 
341  dest.destructive_append(tmp1);
342  dest.destructive_append(tmp2);
343 }
344 
347  goto_programt &dest,
348  const irep_idt &mode,
349  bool result_is_used)
350 {
351  if(!result_is_used)
352  {
353  code_function_callt call(expr.function(), expr.arguments());
354  call.add_source_location()=expr.source_location();
355  convert_function_call(call, dest, mode);
356  expr.make_nil();
357  return;
358  }
359 
360  // get name of function, if available
361  std::string new_base_name = "return_value";
362  irep_idt new_symbol_mode = mode;
363 
364  if(expr.function().id() == ID_symbol)
365  {
366  const irep_idt &identifier =
368  const symbolt &symbol = ns.lookup(identifier);
369 
370  new_base_name+='_';
371  new_base_name+=id2string(symbol.base_name);
372  new_symbol_mode = symbol.mode;
373  }
374 
375  const symbolt &new_symbol = get_fresh_aux_symbol(
376  expr.type(),
378  new_base_name,
379  expr.find_source_location(),
380  new_symbol_mode,
381  symbol_table);
382 
383  {
384  code_declt decl(new_symbol.symbol_expr());
385  decl.add_source_location()=new_symbol.location;
386  convert_decl(decl, dest, mode);
387  }
388 
389  {
390  goto_programt tmp_program2;
391  code_function_callt call(
392  new_symbol.symbol_expr(), expr.function(), expr.arguments());
393  call.add_source_location()=new_symbol.location;
394  convert_function_call(call, dest, mode);
395  }
396 
397  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
398 }
399 
401  const exprt &object,
402  exprt &dest)
403 {
404  if(dest.id()=="new_object")
405  dest=object;
406  else
407  Forall_operands(it, dest)
408  replace_new_object(object, *it);
409 }
410 
412  side_effect_exprt &expr,
413  goto_programt &dest,
414  bool result_is_used)
415 {
416  const symbolt &new_symbol = get_fresh_aux_symbol(
417  expr.type(),
419  "new_ptr",
420  expr.find_source_location(),
421  ID_cpp,
422  symbol_table);
423 
424  code_declt decl(new_symbol.symbol_expr());
425  decl.add_source_location()=new_symbol.location;
426  convert_decl(decl, dest, ID_cpp);
427 
428  const code_assignt call(new_symbol.symbol_expr(), expr);
429 
430  if(result_is_used)
431  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
432  else
433  expr.make_nil();
434 
435  convert(call, dest, ID_cpp);
436 }
437 
439  side_effect_exprt &expr,
440  goto_programt &dest)
441 {
442  DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expects one operand");
443 
444  codet tmp(expr.get_statement());
446  tmp.copy_to_operands(to_unary_expr(expr).op());
447  tmp.set(ID_destructor, expr.find(ID_destructor));
448 
449  convert_cpp_delete(tmp, dest);
450 
451  expr.make_nil();
452 }
453 
455  side_effect_exprt &expr,
456  goto_programt &dest,
457  const irep_idt &mode,
458  bool result_is_used)
459 {
460  if(result_is_used)
461  {
462  const symbolt &new_symbol = get_fresh_aux_symbol(
463  expr.type(),
465  "malloc_value",
466  expr.source_location(),
467  mode,
468  symbol_table);
469 
470  code_declt decl(new_symbol.symbol_expr());
471  decl.add_source_location()=new_symbol.location;
472  convert_decl(decl, dest, mode);
473 
474  code_assignt call(new_symbol.symbol_expr(), expr);
475  call.add_source_location()=expr.source_location();
476 
477  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
478 
479  convert(call, dest, mode);
480  }
481  else
482  {
483  convert(code_expressiont(std::move(expr)), dest, mode);
484  }
485 }
486 
488  side_effect_exprt &expr,
489  goto_programt &dest)
490 {
491  const irep_idt &mode = expr.get(ID_mode);
493  expr.operands().size() <= 1,
494  "temporary_object takes zero or one operands",
495  expr.find_source_location());
496 
497  symbolt &new_symbol = new_tmp_symbol(
498  expr.type(), "obj", dest, expr.find_source_location(), mode);
499 
500  if(expr.operands().size()==1)
501  {
502  const code_assignt assignment(
503  new_symbol.symbol_expr(), to_unary_expr(expr).op());
504 
505  convert(assignment, dest, mode);
506  }
507 
508  if(expr.find(ID_initializer).is_not_nil())
509  {
511  expr.operands().empty(),
512  "temporary_object takes zero operands",
513  expr.find_source_location());
514  exprt initializer=static_cast<const exprt &>(expr.find(ID_initializer));
515  replace_new_object(new_symbol.symbol_expr(), initializer);
516 
517  convert(to_code(initializer), dest, mode);
518  }
519 
520  static_cast<exprt &>(expr)=new_symbol.symbol_expr();
521 }
522 
524  side_effect_exprt &expr,
525  goto_programt &dest,
526  const irep_idt &mode,
527  bool result_is_used)
528 {
529  // This is a gcc extension of the form ({ ....; expr; })
530  // The value is that of the final expression.
531  // The expression is copied into a temporary before the
532  // scope is destroyed.
533 
535 
536  if(!result_is_used)
537  {
538  convert(code, dest, mode);
539  expr.make_nil();
540  return;
541  }
542 
544  code.get_statement() == ID_block,
545  "statement_expression takes block as operand",
546  code.find_source_location());
547 
549  !code.operands().empty(),
550  "statement_expression takes non-empty block as operand",
551  expr.find_source_location());
552 
553  // get last statement from block, following labels
555 
556  source_locationt source_location=last.find_source_location();
557 
558  symbolt &new_symbol = new_tmp_symbol(
559  expr.type(), "statement_expression", dest, source_location, mode);
560 
561  symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type);
562  tmp_symbol_expr.add_source_location()=source_location;
563 
564  if(last.get(ID_statement)==ID_expression)
565  {
566  // we turn this into an assignment
568  last=code_assignt(tmp_symbol_expr, e);
569  last.add_source_location()=source_location;
570  }
571  else if(last.get(ID_statement)==ID_assign)
572  {
573  exprt e=to_code_assign(last).lhs();
574  code_assignt assignment(tmp_symbol_expr, e);
575  assignment.add_source_location()=source_location;
576  code.operands().push_back(assignment);
577  }
578  else
579  {
580  UNREACHABLE;
581  }
582 
583  {
584  goto_programt tmp;
585  convert(code, tmp, mode);
586  dest.destructive_append(tmp);
587  }
588 
589  static_cast<exprt &>(expr)=tmp_symbol_expr;
590 }
591 
594  goto_programt &dest,
595  bool result_is_used,
596  const irep_idt &mode)
597 {
598  const irep_idt &statement = expr.get_statement();
599  const exprt &lhs = expr.lhs();
600  const exprt &rhs = expr.rhs();
601  const exprt &result = expr.result();
602 
603  // actual logic implementing the operators: perform operations on signed
604  // bitvector types of sufficiently large size to hold the result
605  auto const make_operation = [&statement](exprt lhs, exprt rhs) -> exprt {
606  std::size_t lhs_ssize = to_bitvector_type(lhs.type()).get_width();
607  if(lhs.type().id() == ID_unsignedbv)
608  ++lhs_ssize;
609  std::size_t rhs_ssize = to_bitvector_type(rhs.type()).get_width();
610  if(rhs.type().id() == ID_unsignedbv)
611  ++rhs_ssize;
612 
613  if(statement == ID_overflow_plus)
614  {
615  std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1;
616  integer_bitvector_typet ssize_type{ID_signedbv, ssize};
617  return plus_exprt{typecast_exprt{lhs, ssize_type},
618  typecast_exprt{rhs, ssize_type}};
619  }
620  else if(statement == ID_overflow_minus)
621  {
622  std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1;
623  integer_bitvector_typet ssize_type{ID_signedbv, ssize};
624  return minus_exprt{typecast_exprt{lhs, ssize_type},
625  typecast_exprt{rhs, ssize_type}};
626  }
627  else
628  {
629  INVARIANT(
630  statement == ID_overflow_mult,
631  "the three overflow operations are add, sub and mul");
632  std::size_t ssize = lhs_ssize + rhs_ssize;
633  integer_bitvector_typet ssize_type{ID_signedbv, ssize};
634  return mult_exprt{typecast_exprt{lhs, ssize_type},
635  typecast_exprt{rhs, ssize_type}};
636  }
637  };
638 
639  // Generating the following sequence of statements:
640  // large_signedbv tmp = (large_signedbv)lhs OP (large_signedbv)rhs;
641  // *result = (result_type)tmp; // only if result is a pointer
642  // (large_signedbv)(result_type)tmp != tmp;
643  // This performs the operation (+, -, *) on a signed bitvector type of
644  // sufficiently large width to store the precise result, cast to result
645  // type, check if the cast result is not equivalent to the full-length
646  // result.
647  auto operation = make_operation(lhs, rhs);
648  // Disable overflow checks as the operation cannot overflow on the larger
649  // type
650  operation.add_source_location() = expr.source_location();
651  operation.add_source_location().add_pragma("disable:signed-overflow-check");
652 
653  make_temp_symbol(operation, "large_bv", dest, mode);
654 
655  optionalt<typet> result_type;
656  if(result.type().id() == ID_pointer)
657  {
658  result_type = to_pointer_type(result.type()).subtype();
659  code_assignt result_assignment{dereference_exprt{result},
660  typecast_exprt{operation, *result_type},
661  expr.source_location()};
662  convert_assign(result_assignment, dest, mode);
663  }
664  else
665  {
666  result_type = result.type();
667  // evaluate side effects
668  exprt tmp = result;
669  clean_expr(tmp, dest, mode, false); // result _not_ used
670  }
671 
672  if(result_is_used)
673  {
674  typecast_exprt inner_tc{operation, *result_type};
675  inner_tc.add_source_location() = expr.source_location();
676  inner_tc.add_source_location().add_pragma("disable:conversion-check");
677  typecast_exprt outer_tc{inner_tc, operation.type()};
678  outer_tc.add_source_location() = expr.source_location();
679  outer_tc.add_source_location().add_pragma("disable:conversion-check");
680 
681  notequal_exprt overflow_check{outer_tc, operation};
682  overflow_check.add_source_location() = expr.source_location();
683 
684  expr.swap(overflow_check);
685  }
686  else
687  expr.make_nil();
688 }
689 
691  side_effect_exprt &expr,
692  goto_programt &dest,
693  const irep_idt &mode,
694  bool result_is_used,
695  bool address_taken)
696 {
697  const irep_idt &statement=expr.get_statement();
698 
699  if(statement==ID_function_call)
701  to_side_effect_expr_function_call(expr), dest, mode, result_is_used);
702  else if(statement==ID_assign ||
703  statement==ID_assign_plus ||
704  statement==ID_assign_minus ||
705  statement==ID_assign_mult ||
706  statement==ID_assign_div ||
707  statement==ID_assign_bitor ||
708  statement==ID_assign_bitxor ||
709  statement==ID_assign_bitand ||
710  statement==ID_assign_lshr ||
711  statement==ID_assign_ashr ||
712  statement==ID_assign_shl ||
713  statement==ID_assign_mod)
714  remove_assignment(expr, dest, result_is_used, address_taken, mode);
715  else if(statement==ID_postincrement ||
716  statement==ID_postdecrement)
717  remove_post(expr, dest, mode, result_is_used);
718  else if(statement==ID_preincrement ||
719  statement==ID_predecrement)
720  remove_pre(expr, dest, result_is_used, address_taken, mode);
721  else if(statement==ID_cpp_new ||
722  statement==ID_cpp_new_array)
723  remove_cpp_new(expr, dest, result_is_used);
724  else if(statement==ID_cpp_delete ||
725  statement==ID_cpp_delete_array)
726  remove_cpp_delete(expr, dest);
727  else if(statement==ID_allocate)
728  remove_malloc(expr, dest, mode, result_is_used);
729  else if(statement==ID_temporary_object)
730  remove_temporary_object(expr, dest);
731  else if(statement==ID_statement_expression)
732  remove_statement_expression(expr, dest, mode, result_is_used);
733  else if(statement==ID_nondet)
734  {
735  // these are fine
736  }
737  else if(statement==ID_skip)
738  {
739  expr.make_nil();
740  }
741  else if(statement==ID_throw)
742  {
744  expr.find(ID_exception_list), expr.type(), expr.source_location()));
745  code.op0().operands().swap(expr.operands());
746  code.add_source_location() = expr.source_location();
748  std::move(code), expr.source_location(), THROW, nil_exprt(), {}));
749 
750  // the result can't be used, these are void
751  expr.make_nil();
752  }
753  else if(
754  statement == ID_overflow_plus || statement == ID_overflow_minus ||
755  statement == ID_overflow_mult)
756  {
758  to_side_effect_expr_overflow(expr), dest, result_is_used, mode);
759  }
760  else
761  {
762  UNREACHABLE;
763  }
764 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
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:182
bitvector_typet index_type()
Definition: c_types.cpp:16
exprt & op0()
Definition: expr.h:99
std::size_t get_width() const
Definition: std_types.h:843
A codet representing an assignment in the program.
Definition: std_code.h:293
exprt & lhs()
Definition: std_code.h:310
codet & find_last_statement()
Definition: std_code.cpp:99
A codet representing the declaration of a local variable.
Definition: std_code.h:400
codet representation of an expression statement.
Definition: std_code.h:1840
const exprt & expression() const
Definition: std_code.h:1847
codet representation of a function call statement.
Definition: std_code.h:1213
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
exprt & op0()
Definition: expr.h:99
const irep_idt & get_statement() const
Definition: std_code.h:69
Complex constructor from a pair of numbers.
Definition: std_expr.h:1707
Operator to dereference a pointer.
Definition: pointer_expr.h:628
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
source_locationt & add_source_location()
Definition: expr.h:235
const source_locationt & source_location() const
Definition: expr.h:230
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
void remove_temporary_object(side_effect_exprt &expr, goto_programt &dest)
void remove_function_call(side_effect_expr_function_callt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
symbol_table_baset & symbol_table
void remove_pre(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode)
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
void convert_decl(const code_declt &code, goto_programt &dest, const irep_idt &mode)
void remove_overflow(side_effect_expr_overflowt &expr, goto_programt &dest, bool result_is_used, const irep_idt &mode)
void remove_post(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
void remove_malloc(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest)
std::string tmp_symbol_prefix
void remove_side_effect(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used, bool address_taken)
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)
void remove_statement_expression(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
void convert_cpp_delete(const codet &code, goto_programt &dest)
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
static bool has_function_call(const exprt &expr)
static bool needs_cleaning(const exprt &expr)
void remove_assignment(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode)
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
void remove_cpp_new(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
static void replace_new_object(const exprt &object, exprt &dest)
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:736
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:753
Fixed-width bit-vector representing a signed or unsigned integer.
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void make_nil()
Definition: irep.h:465
void swap(irept &irep)
Definition: irep.h:453
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
mstreamt & result() const
Definition: message.h:409
Binary minus.
Definition: std_expr.h:973
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The NIL expression.
Definition: std_expr.h:2820
Disequality.
Definition: std_expr.h:1283
The plus expression Associativity is not specified.
Definition: std_expr.h:914
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2138
exprt::operandst & arguments()
Definition: std_code.h:2164
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
Definition: c_expr.h:117
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:2203
An expression containing a side effect.
Definition: std_code.h:1896
const irep_idt & get_statement() const
Definition: std_code.h:1918
void add_pragma(const irep_idt &pragma)
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
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:1866
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
source_locationt & add_source_location()
Definition: type.h:76
const exprt & op() const
Definition: std_expr.h:293
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:215
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.
@ THROW
Definition: goto_program.h:48
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Mathematical types.
nonstd::optional< T > optionalt
Definition: optional.h:35
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#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:2115
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:2185
const codet & to_code(const exprt &expr)
Definition: std_code.h:153
side_effect_expr_assignt & to_side_effect_expr_assign(exprt &expr)
Definition: std_code.h:2064
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1874
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:254
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:381
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1040
Symbol table entry.