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