CBMC
Loading...
Searching...
No Matches
goto_clean_expr.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/config.h>
15#include <util/expr_util.h>
16#include <util/fresh_symbol.h>
18#include <util/pointer_expr.h>
19#include <util/replace_expr.h>
20#include <util/std_expr.h>
21#include <util/symbol.h>
22
24
25#include "destructor.h"
26
27#include <unordered_map>
28
30{
31 if(expr.id() == ID_symbol)
32 {
33 return to_symbol_expr(expr);
34 }
35 else if(expr.id() == ID_member)
36 {
37 return find_base_symbol(to_member_expr(expr).struct_op());
38 }
39 else if(expr.id() == ID_index)
40 {
41 return find_base_symbol(to_index_expr(expr).array());
42 }
43 else if(expr.id() == ID_dereference)
44 {
45 return find_base_symbol(to_dereference_expr(expr).pointer());
46 }
47 else if(expr.id() == ID_typecast)
48 {
49 return find_base_symbol(to_typecast_expr(expr).op());
50 }
51 else if(expr.id() == ID_address_of)
52 {
53 return find_base_symbol(to_address_of_expr(expr).op());
54 }
55 else
56 {
57 throw "unsupported expression type for finding base symbol";
58 }
59}
60
62 const quantifier_exprt &qex,
63 const code_expressiont &code,
64 const irep_idt &mode,
65 symbol_table_baset &symbol_table,
66 message_handlert &message_handler)
67{
68 goto_programt where;
69 goto_convertt converter{symbol_table, message_handler};
70 converter.goto_convert(code, where, mode);
72
73 natural_loops_mutablet natural_loops(where);
75 natural_loops.loop_map.size() == 0, "quantifier must not contain loops");
76
77 std::unordered_set<symbol_exprt, irep_hash> declared_symbols;
78 // All bound variables are local.
79 declared_symbols.insert(qex.variables().begin(), qex.variables().end());
80
81 // `last` is the instruction corresponding to the last expression in the
82 // statement expression.
84 for(goto_programt::const_targett it = where.instructions.begin();
85 it != where.instructions.end();
86 ++it)
87 {
88 // `last` is an other-instruction.
89 if(it->is_other())
90 {
91 last = it;
92 }
93
94 if(it->is_decl())
95 {
96 declared_symbols.insert(it->decl_symbol());
97 }
98 }
99
101 last != where.instructions.end(),
102 "expression statements must contain a terminator expression");
103
104 auto last_expr = to_code_expression(last->get_other()).expression();
105 if(
106 last_expr.id() == ID_typecast &&
107 to_typecast_expr(last_expr).type().id() == ID_empty)
108 {
110 }
111
112 struct pathst
113 {
114 // `paths` contains all the `targett` we are iterating over.
115 std::vector<goto_programt::const_targett> paths;
116 std::vector<std::pair<exprt, replace_mapt>> path_conditions_and_value_maps;
117
118 pathst(
119 std::vector<goto_programt::const_targett> paths,
120 std::vector<std::pair<exprt, replace_mapt>>
122 : paths(paths),
124 {
125 }
126
127 bool empty()
128 {
129 return paths.empty();
130 }
131
133 {
134 return paths.back();
135 }
136
138 {
139 return path_conditions_and_value_maps.back().first;
140 }
141
143 {
144 return path_conditions_and_value_maps.back().second;
145 }
146
147 void push_back(
150 replace_mapt value_map)
151 {
152 paths.push_back(target);
154 std::make_pair(path_condition, value_map));
155 }
156
157 void pop_back()
158 {
159 paths.pop_back();
161 }
162 };
163
164 pathst paths(
165 {1, where.instructions.begin()},
166 {1, std::make_pair(true_exprt(), replace_mapt())});
167
168 exprt res = true_exprt();
169
170 // Visit the quantifier body along `paths`.
171 while(!paths.empty())
172 {
173 auto &current_it = paths.back_it();
174 auto &path_condition = paths.back_path_condition();
175 auto &value_map = paths.back_value_map();
176
177 if(current_it == where.instructions.end())
178 {
179 paths.pop_back();
180 continue;
181 }
182
183 switch(current_it->type())
184 {
185 // Add all local-declared symbols into `declared_symbols`.
187 declared_symbols.insert(current_it->decl_symbol());
188 break;
189
190 // ASSIGN lhs := rhs
191 // Add the replace lhr <- value_map(rhs) to the current value_map.
193 {
194 // Check that if lhs is a declared symbol.
195 auto lhs = current_it->assign_lhs();
196 INVARIANT(
198 "quantifier must not contain side effects");
199 exprt rhs = current_it->assign_rhs();
200 replace_expr(value_map, rhs);
201 value_map[lhs] = rhs;
202 }
203 break;
204
205 // GOTO label
206 // -----------
207 // Move the current targett to label.
208 // or
209 // IF cond GOTO label
210 // ----------
211 // Move the current targett to targett+1 with path condition
212 // path_condition && !cond;
213 // and add a new path starting from label with path condition
214 // path_condition && cond.
216 {
217 exprt condition = current_it->condition();
218 replace_expr(value_map, condition);
219 if(condition != true)
220 {
221 auto next_it = current_it->targets.front();
224 current_it++;
225 paths.push_back(
226 next_it, and_exprt(copy_path_condition, condition), value_map);
227 }
228 else
229 {
230 current_it = current_it->targets.front();
231 }
232 continue;
233 }
234
235 // EXPRESSION(expr)
236 // The last instruction is an expression statement.
237 // We add the predicate path_condition ==> value_map(expr) to res.
239 {
240 if(current_it == last)
241 {
245 paths.pop_back();
246 continue;
247 }
248 }
249 break;
250
251 // Ignored instructions.
260 break;
261
262 // Unsupported instructions.
272 }
273
274 current_it++;
275 }
276 return res;
277}
278
280 const exprt &expr,
281 goto_programt &dest,
282 const irep_idt &mode)
283{
284 const source_locationt source_location = expr.find_source_location();
285
286 symbolt &new_symbol = get_fresh_aux_symbol(
287 expr.type(),
289 "literal",
290 source_location,
291 mode,
294 new_symbol.value = expr;
295
296 // The value might depend on a variable, thus
297 // generate code for this.
298
299 symbol_exprt result = new_symbol.symbol_expr();
300 result.add_source_location() = source_location;
301
302 // The lifetime of compound literals is really that of
303 // the block they are in.
304 if(!new_symbol.is_static_lifetime)
305 copy(code_declt(result), DECL, dest);
306
308 code_assign.add_source_location() = source_location;
309 convert(code_assign, dest, mode);
310
311 // now create a 'dead' instruction
312 if(!new_symbol.is_static_lifetime)
313 {
315 targets.scope_stack.add(std::move(code_dead), {});
316 }
317
318 return result;
319}
320
327{
328 if(
329 expr.id() == ID_side_effect || expr.id() == ID_compound_literal ||
330 expr.id() == ID_comma)
331 {
332 return true;
333 }
334
335 // We can't flatten quantified expressions by introducing new literals for
336 // conditional expressions. This is because the body of the quantified
337 // may refer to bound variables, which are not visible outside the scope
338 // of the quantifier.
339 //
340 // For example, the following transformation would not be valid:
341 //
342 // forall (i : int) (i == 0 || i > 10)
343 //
344 // transforming to
345 //
346 // g1 = (i == 0)
347 // g2 = (i > 10)
348 // forall (i : int) (g1 || g2)
349 if(expr.id() == ID_forall || expr.id() == ID_exists)
350 {
351 code_expressiont where{to_quantifier_expr(expr).where()};
352 // Need cleaning when the quantifier body is a side-effect expression.
353 if(has_subexpr(expr, ID_side_effect))
354 return true;
355
356 return false;
357 }
358
359 for(const auto &op : expr.operands())
360 {
361 if(needs_cleaning(op))
362 return true;
363 }
364
365 return false;
366}
367
370{
372 expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies);
374 expr.is_boolean(),
376 "'",
377 expr.id(),
378 "' must be Boolean, but got ",
380
381 const source_locationt source_location = expr.find_source_location();
382
383 // re-write "a ==> b" into a?b:1
384 if(auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
385 {
386 expr = if_exprt{
387 std::move(implies->lhs()),
388 std::move(implies->rhs()),
389 true_exprt{}.with_source_location(source_location),
390 bool_typet{}};
391 return;
392 }
393
394 // re-write "a && b" into nested a?b:0
395 // re-write "a || b" into nested a?1:b
396
397 exprt tmp;
398
399 if(expr.id() == ID_and)
400 tmp = true_exprt();
401 else // ID_or
402 tmp = false_exprt();
403
404 tmp.add_source_location() = source_location;
405
406 exprt::operandst &ops = expr.operands();
407
408 // start with last one
409 for(exprt::operandst::reverse_iterator it = ops.rbegin(); it != ops.rend();
410 ++it)
411 {
412 exprt &op = *it;
413
415 op.is_boolean(),
416 "boolean operators must have only boolean operands",
417 source_location);
418
419 if(expr.id() == ID_and)
420 {
421 exprt if_e =
422 if_exprt{op, tmp, false_exprt{}.with_source_location(source_location)}
423 .with_source_location(source_location);
424 tmp.swap(if_e);
425 continue;
426 }
427 if(expr.id() == ID_or)
428 {
429 exprt if_e =
430 if_exprt{op, true_exprt{}.with_source_location(source_location), tmp}
431 .with_source_location(source_location);
432 tmp.swap(if_e);
433 continue;
434 }
436 }
437
438 expr.swap(tmp);
439}
440
442 exprt &expr,
443 const irep_idt &mode,
444 bool result_is_used)
445{
446 // this cleans:
447 // && || ==> ?: comma (control-dependency)
448 // function calls
449 // object constructors like arrays, string constants, structs
450 // ++ -- (pre and post)
451 // compound assignments
452 // compound literals
453
454 if(!needs_cleaning(expr))
455 return {};
456
457 if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies)
458 {
459 // rewrite into ?:
460 rewrite_boolean(expr);
461
462 // recursive call
463 return clean_expr(expr, mode, result_is_used);
464 }
465 else if(expr.id() == ID_if)
466 {
467 // first clean condition
468 clean_expr_resultt side_effects =
469 clean_expr(to_if_expr(expr).cond(), mode, true);
470
471 // possibly done now
472 if(
473 !needs_cleaning(to_if_expr(expr).true_case()) &&
474 !needs_cleaning(to_if_expr(expr).false_case()))
475 {
476 return side_effects;
477 }
478
479 // copy expression
481
483 if_expr.cond().is_boolean(),
484 "condition for an 'if' must be boolean",
485 if_expr.find_source_location());
486
487 const source_locationt source_location = expr.find_source_location();
488
489#if 0
490 // We do some constant-folding here, to mimic
491 // what typical compilers do.
492 {
493 exprt tmp_cond=if_expr.cond();
495 if(tmp_cond.is_true())
496 {
497 clean_expr(if_expr.true_case(), dest, result_is_used);
498 expr=if_expr.true_case();
499 return;
500 }
501 else if(tmp_cond.is_false())
502 {
503 clean_expr(if_expr.false_case(), dest, result_is_used);
504 expr=if_expr.false_case();
505 return;
506 }
507 }
508#endif
509
511 clean_expr(if_expr.true_case(), mode, result_is_used));
512
514 clean_expr(if_expr.false_case(), mode, result_is_used));
515
517 {
518 symbolt &new_symbol = new_tmp_symbol(
519 expr.type(),
520 "if_expr",
521 side_effects.side_effects,
522 source_location,
523 mode);
524
526 assignment_true.lhs() = new_symbol.symbol_expr();
527 assignment_true.rhs() = if_expr.true_case();
528 assignment_true.add_source_location() = source_location;
529 convert(assignment_true, tmp_true.side_effects, mode);
530
532 assignment_false.lhs() = new_symbol.symbol_expr();
533 assignment_false.rhs() = if_expr.false_case();
534 assignment_false.add_source_location() = source_location;
535 convert(assignment_false, tmp_false.side_effects, mode);
536
537 // overwrites expr
538 expr = new_symbol.symbol_expr();
539 }
540 else
541 {
542 // preserve the expressions for possible later checks
543 if(if_expr.true_case().is_not_nil())
544 {
545 // add a (void) type cast so that is_skip catches it in case the
546 // expression is just a constant
548 typecast_exprt(if_expr.true_case(), empty_typet()));
549 convert(code_expression, tmp_true.side_effects, mode);
550 }
551
552 if(if_expr.false_case().is_not_nil())
553 {
554 // add a (void) type cast so that is_skip catches it in case the
555 // expression is just a constant
557 typecast_exprt(if_expr.false_case(), empty_typet()));
558 convert(code_expression, tmp_false.side_effects, mode);
559 }
560
561 expr = nil_exprt();
562 }
563
564 // generate guard for argument side-effects
566 if_expr.cond(),
567 source_location,
568 tmp_true.side_effects,
569 if_expr.true_case().source_location(),
570 tmp_false.side_effects,
571 if_expr.false_case().source_location(),
572 side_effects.side_effects,
573 mode);
574
575 destruct_locals(tmp_false.temporaries, side_effects.side_effects, ns);
576 destruct_locals(tmp_true.temporaries, side_effects.side_effects, ns);
577 destruct_locals(side_effects.temporaries, side_effects.side_effects, ns);
578 side_effects.temporaries.clear();
579
580 if(expr.is_not_nil())
581 side_effects.add_temporary(to_symbol_expr(expr).identifier());
582
583 return side_effects;
584 }
585 else if(expr.id() == ID_comma)
586 {
587 clean_expr_resultt side_effects;
588
590 {
592
593 Forall_operands(it, expr)
594 {
595 bool last = (it == --expr.operands().end());
596
597 // special treatment for last one
598 if(last)
599 {
600 result.swap(*it);
601 side_effects.add(clean_expr(result, mode, true));
602 }
603 else
604 {
605 side_effects.add(clean_expr(*it, mode, false));
606
607 // remember these for later checks
608 if(it->is_not_nil())
609 convert(code_expressiont(*it), side_effects.side_effects, mode);
610 }
611 }
612
613 expr.swap(result);
614 }
615 else // result not used
616 {
617 Forall_operands(it, expr)
618 {
619 side_effects.add(clean_expr(*it, mode, false));
620
621 // remember as expression statement for later checks
622 if(it->is_not_nil())
623 convert(code_expressiont(*it), side_effects.side_effects, mode);
624 }
625
626 expr = nil_exprt();
627 }
628
629 return side_effects;
630 }
631 else if(expr.id() == ID_typecast)
632 {
633 typecast_exprt &typecast = to_typecast_expr(expr);
634
635 // preserve 'result_is_used'
636 clean_expr_resultt side_effects =
637 clean_expr(typecast.op(), mode, result_is_used);
638
639 if(typecast.op().is_nil())
640 expr.make_nil();
641
642 return side_effects;
643 }
644 else if(expr.id() == ID_side_effect)
645 {
646 // some of the side-effects need special treatment!
647 const irep_idt statement = to_side_effect_expr(expr).get_statement();
648
649 if(statement == ID_gcc_conditional_expression)
650 {
651 // need to do separately
652 return remove_gcc_conditional_expression(expr, mode);
653 }
654 else if(statement == ID_statement_expression)
655 {
656 // need to do separately to prevent that
657 // the operands of expr get 'cleaned'
660 }
661 else if(statement == ID_assign)
662 {
663 // we do a special treatment for x=f(...)
664 INVARIANT(
665 expr.operands().size() == 2,
666 "side-effect assignment expressions must have two operands");
667
669
670 if(
671 side_effect_assign.rhs().id() == ID_side_effect &&
674 {
675 clean_expr_resultt side_effects =
676 clean_expr(side_effect_assign.lhs(), mode);
677 exprt lhs = side_effect_assign.lhs();
678
680 if(must_use_rhs)
681 {
682 side_effects.add(remove_function_call(
684 mode,
685 true));
686 }
687
688 // turn into code
691 side_effect_assign.rhs(), new_lhs.type());
692 code_assignt assignment(std::move(new_lhs), new_rhs);
693 assignment.add_source_location() = expr.source_location();
694 convert_assign(assignment, side_effects.side_effects, mode);
695
697 expr = must_use_rhs ? new_rhs : lhs;
698 else
699 expr.make_nil();
700
701 return side_effects;
702 }
703 }
704 }
705 else if(expr.id() == ID_forall || expr.id() == ID_exists)
706 {
708 code_expressiont code{qex.where()};
710 !has_subexpr(expr, ID_side_effect) ||
711 (code.operands()[0].id() == ID_side_effect &&
712 code.operands()[0].get_named_sub()[ID_statement].id() ==
714 "quantifier must not contain side effects");
715
716 // Handle the case that quantifier body is a statement expression.
717 if(
718 code.operands()[0].id() == ID_side_effect &&
719 code.operands()[0].get_named_sub()[ID_statement].id() ==
721 {
723 qex, code, mode, symbol_table, get_message_handler());
724 qex.where() = res;
725 return clean_expr(res, mode, result_is_used);
726 }
727 }
728 else if(expr.id() == ID_address_of)
729 {
731 return clean_expr_address_of(addr.object(), mode);
732 }
733
734 clean_expr_resultt side_effects;
735
736 if(
737 expr.id() == ID_side_effect &&
738 to_side_effect_expr(expr).get_statement() == ID_function_call)
739 {
742 side_effects.add(
743 clean_function_call_operands(call.function(), call.arguments(), mode));
744 }
745 else
746 {
747 Forall_operands(it, expr)
748 side_effects.add(clean_expr(*it, mode));
749 }
750
751 if(expr.id() == ID_side_effect)
752 {
753 side_effects.add(remove_side_effect(
754 to_side_effect_expr(expr), mode, result_is_used, false));
755 }
756 else if(expr.id() == ID_compound_literal)
757 {
758 // This is simply replaced by the literal
760 expr.operands().size() == 1, "ID_compound_literal has a single operand");
761 expr = to_unary_expr(expr).op();
762 }
763
764 return side_effects;
765}
766
769{
770 clean_expr_resultt side_effects;
771
772 // The address of object constructors can be taken,
773 // which is re-written into the address of a variable.
774
775 if(expr.id() == ID_compound_literal)
776 {
778 expr.operands().size() == 1, "ID_compound_literal has a single operand");
779 side_effects.add(clean_expr(to_unary_expr(expr).op(), mode));
781 to_unary_expr(expr).op(), side_effects.side_effects, mode);
782 }
783 else if(expr.id() == ID_string_constant)
784 {
785 // Leave for now, but long-term these might become static symbols.
786 // LLVM appears to do precisely that.
787 }
788 else if(expr.id() == ID_index)
789 {
791 side_effects.add(clean_expr_address_of(index_expr.array(), mode));
792 side_effects.add(clean_expr(index_expr.index(), mode));
793 }
794 else if(expr.id() == ID_dereference)
795 {
797 side_effects.add(clean_expr(deref_expr.pointer(), mode));
798 }
799 else if(expr.id() == ID_comma)
800 {
801 // Yes, one can take the address of a comma expression.
802 // Treatment is similar to clean_expr() above.
803
805
806 Forall_operands(it, expr)
807 {
808 bool last = (it == --expr.operands().end());
809
810 // special treatment for last one
811 if(last)
812 result.swap(*it);
813 else
814 {
815 side_effects.add(clean_expr(*it, mode, false));
816
817 // get any side-effects
818 if(it->is_not_nil())
819 convert(code_expressiont(*it), side_effects.side_effects, mode);
820 }
821 }
822
823 expr.swap(result);
824
825 // do again
826 side_effects.add(clean_expr_address_of(expr, mode));
827 }
828 else if(expr.id() == ID_side_effect)
829 {
830 side_effects.add(
831 remove_side_effect(to_side_effect_expr(expr), mode, true, true));
832 }
833 else
834 Forall_operands(it, expr)
835 side_effects.add(clean_expr_address_of(*it, mode));
836
837 return side_effects;
838}
839
842 exprt &expr,
843 const irep_idt &mode)
844{
845 clean_expr_resultt side_effects;
846
847 {
848 auto &binary_expr = to_binary_expr(expr);
849
850 // first remove side-effects from condition
851 side_effects = clean_expr(to_binary_expr(expr).op0(), mode);
852
853 // now we can copy op0 safely
856 binary_expr.op0(),
857 binary_expr.op1(),
858 expr.type());
859 if_expr.add_source_location() = expr.source_location();
860
861 expr.swap(if_expr);
862 }
863
864 // there might still be junk in expr.op2()
865 side_effects.add(clean_expr(expr, mode));
866
867 return side_effects;
868}
869
871 exprt &function,
872 exprt::operandst &arguments,
873 const irep_idt &mode)
874{
875 clean_expr_resultt side_effects;
876
877 // The function operand is evaluated before the arguments either way.
878 side_effects.add(clean_expr(function, mode));
879
880 // The C and C++ standards leave the order of evaluation of function call
881 // arguments unspecified; model the fixed order that the configured
882 // architecture/compiler combination uses.
883 if(
884 config.ansi_c.argument_evaluation_order ==
886 {
887 for(auto it = arguments.rbegin(); it != arguments.rend(); ++it)
888 side_effects.add(clean_expr(*it, mode));
889 }
890 else
891 {
892 for(auto &argument : arguments)
893 side_effects.add(clean_expr(argument, mode));
894 }
895
896 return side_effects;
897}
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
configt config
Definition config.cpp:25
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Boolean AND All operands must be boolean, and the result is always boolean.
Definition std_expr.h:2043
The Boolean type.
Definition std_types.h:35
A goto_instruction_codet representing an assignment in the program.
A goto_instruction_codet representing the removal of a local variable going out of scope.
A goto_instruction_codet representing the declaration of a local variable.
codet representation of an expression statement.
Definition std_code.h:1394
const exprt & expression() const
Definition std_code.h:1401
struct configt::ansi_ct ansi_c
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
The empty type.
Definition std_types.h:50
Base class for all expressions.
Definition expr.h:57
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:68
std::vector< exprt > operandst
Definition expr.h:59
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:229
typet & type()
Return the type of the expression.
Definition expr.h:85
operandst & operands()
Definition expr.h:95
const source_locationt & source_location() const
Definition expr.h:236
source_locationt & add_source_location()
Definition expr.h:241
exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
Definition expr.h:102
The Boolean constant false.
Definition std_expr.h:3135
clean_expr_resultt clean_expr_address_of(exprt &expr, const irep_idt &mode)
symbol_table_baset & symbol_table
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
clean_expr_resultt remove_gcc_conditional_expression(exprt &expr, const irep_idt &mode)
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
void generate_ifthenelse(const exprt &cond, const source_locationt &, goto_programt &true_case, const source_locationt &, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) true_case; else false_case;
std::string tmp_symbol_prefix
struct goto_convertt::targetst targets
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
symbol_exprt make_compound_literal(const exprt &expr, goto_programt &dest, const irep_idt &mode)
clean_expr_resultt remove_side_effect(side_effect_exprt &expr, const irep_idt &mode, bool result_is_used, bool address_taken)
clean_expr_resultt clean_function_call_operands(exprt &function, exprt::operandst &arguments, const irep_idt &mode)
Remove side effects from the function operand and the argument operands of a function call,...
static bool needs_cleaning(const exprt &expr)
Returns 'true' for expressions that may change the program state.
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
clean_expr_resultt remove_function_call(side_effect_expr_function_callt &expr, const irep_idt &mode, bool result_is_used)
clean_expr_resultt remove_statement_expression(side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)
clean_expr_resultt clean_expr(exprt &expr, const irep_idt &mode, bool result_is_used=true)
void rewrite_boolean(exprt &dest)
re-write boolean operators into ?:
static bool assignment_lhs_needs_temporary(const exprt &lhs)
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
void compute_location_numbers(unsigned &nr)
Compute location numbers.
The trinary if-then-else operator.
Definition std_expr.h:2426
Boolean implication.
Definition std_expr.h:2154
Array index operator.
Definition std_expr.h:1431
bool is_not_nil() const
Definition irep.h:372
void make_nil()
Definition irep.h:446
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
loop_mapt loop_map
message_handlert & get_message_handler()
Definition message.h:183
mstreamt & result() const
Definition message.h:411
The NIL expression.
Definition std_expr.h:3144
Boolean negation.
Definition std_expr.h:2388
A base class for quantifier expressions.
A side_effect_exprt representation of a function call side effect.
Definition std_code.h:1692
const irep_idt & get_statement() const
Definition std_code.h:1472
Expression to hold a symbol (variable)
Definition std_expr.h:132
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
bool is_static_lifetime
Definition symbol.h:70
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
exprt value
Initial value of symbol.
Definition symbol.h:34
The Boolean constant true.
Definition std_expr.h:3126
Semantic type conversion.
Definition std_expr.h:1995
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2003
const exprt & op() const
Definition std_expr.h:394
void destruct_locals(const std::list< irep_idt > &vars, goto_programt &dest, const namespacet &ns)
Destructor Calls.
#define Forall_operands(it, expr)
Definition expr.h:28
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
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.
static symbol_exprt find_base_symbol(const exprt &expr)
static exprt convert_statement_expression(const quantifier_exprt &qex, const code_expressiont &code, const irep_idt &mode, symbol_table_baset &symbol_table, message_handlert &message_handler)
Program Transformation.
@ FUNCTION_CALL
@ ATOMIC_END
@ DEAD
@ LOCATION
@ END_FUNCTION
@ ASSIGN
@ ASSERT
@ SET_RETURN_VALUE
@ ATOMIC_BEGIN
@ CATCH
@ END_THREAD
@ SKIP
@ NO_INSTRUCTION_TYPE
@ START_THREAD
@ THROW
@ DECL
@ OTHER
@ GOTO
@ INCOMPLETE_GOTO
@ ASSUME
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Compute natural loops in a goto_function.
std::list< patht > pathst
Definition path.h:45
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
exprt deref_expr(const exprt &expr)
Wraps a given expression into a dereference_exprt unless it is an address_of_exprt in which case it j...
bool simplify(exprt &expr, const namespacet &ns)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:464
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition invariant.h:535
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition std_code.h:1506
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition std_code.h:1739
side_effect_expr_assignt & to_side_effect_expr_assign(exprt &expr)
Definition std_code.h:1618
code_expressiont & to_code_expression(codet &code)
Definition std_code.h:1428
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1494
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2024
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:721
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:424
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2501
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2953
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:221
std::list< irep_idt > temporaries
Identifiers of temporaries introduced while cleaning an expression.
void add(clean_expr_resultt &&other)
void add_temporary(const irep_idt &id)
goto_programt side_effects
Statements implementing side effects of the expression that was subject to cleaning.
Symbol table entry.