cprover
Loading...
Searching...
No Matches
goto_convert_side_effect.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Program Transformation
4
5Author: 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
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",
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 {
113 }
114
115 exprt rhs;
116
117 const typet &op0_type = to_binary_expr(expr).op0().type();
118
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);
125 to_binary_expr(expr).op0(), to_binary_expr(expr).op1());
126 rhs.type() = to_binary_expr(expr).op0().type();
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());
140 code_assignt assignment(new_lhs, rhs);
141 assignment.add_source_location()=expr.source_location();
142
143 convert(assignment, dest, mode);
144 }
145 else
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
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 = c_index_type();
218 else if(is_number(op_type))
219 constant_type = op_type;
220 else
221 {
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
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 = c_index_type();
304 else if(is_number(op_type))
305 constant_type = op_type;
306 else
307 {
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());
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,
380 new_symbol_mode,
382
383 {
384 code_frontend_declt decl(new_symbol.symbol_expr());
385 decl.add_source_location()=new_symbol.location;
386 convert_frontend_decl(decl, dest, mode);
387 }
388
389 {
390 goto_programt tmp_program2;
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",
421 ID_cpp,
423
424 code_frontend_declt decl(new_symbol.symbol_expr());
425 decl.add_source_location()=new_symbol.location;
426 convert_frontend_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,
469
470 code_frontend_declt decl(new_symbol.symbol_expr());
471 decl.add_source_location()=new_symbol.location;
472 convert_frontend_decl(decl, dest, mode);
473
474 code_assignt call(new_symbol.symbol_expr(), expr);
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 {
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()).base_type();
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 {
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 c_index_type()
Definition: c_types.cpp:16
exprt & op0()
Definition: expr.h:99
std::size_t get_width() const
Definition: std_types.h:864
A codet representing an assignment in the program.
codet & find_last_statement()
Definition: std_code.cpp:99
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
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:99
const irep_idt & get_statement() const
Definition: std_code_base.h:65
Complex constructor from a pair of numbers.
Definition: std_expr.h:1761
Operator to dereference a pointer.
Definition: pointer_expr.h:648
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
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
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 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 convert_frontend_decl(const code_frontend_declt &, goto_programt &, const irep_idt &mode)
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:180
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:698
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
Fixed-width bit-vector representing a signed or unsigned integer.
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
bool is_not_nil() const
Definition: irep.h:380
void make_nil()
Definition: irep.h:454
void swap(irept &irep)
Definition: irep.h:442
const irep_idt & id() const
Definition: irep.h:396
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:2874
Disequality.
Definition: std_expr.h:1283
The plus expression Associativity is not specified.
Definition: std_expr.h:914
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:117
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
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:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
source_locationt & add_source_location()
Definition: type.h:79
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:216
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 codet &code)
@ THROW
Definition: goto_program.h:50
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
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:79
#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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
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
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:203
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 codet & to_code(const exprt &expr)
API to expression classes.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
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 symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1082
Symbol table entry.