CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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/expr_util.h>
15#include <util/fresh_symbol.h>
17#include <util/pointer_expr.h>
18#include <util/replace_expr.h>
19#include <util/std_expr.h>
20#include <util/symbol.h>
21
23
24#include "destructor.h"
25
26#include <unordered_map>
27
29{
30 if(expr.id() == ID_symbol)
31 {
32 return to_symbol_expr(expr);
33 }
34 else if(expr.id() == ID_member)
35 {
36 return find_base_symbol(to_member_expr(expr).struct_op());
37 }
38 else if(expr.id() == ID_index)
39 {
40 return find_base_symbol(to_index_expr(expr).array());
41 }
42 else if(expr.id() == ID_dereference)
43 {
44 return find_base_symbol(to_dereference_expr(expr).pointer());
45 }
46 else
47 {
48 throw "unsupported expression type for finding base symbol";
49 }
50}
51
53 const quantifier_exprt &qex,
54 const code_expressiont &code,
55 const irep_idt &mode,
56 goto_convertt &converter)
57{
58 goto_programt where;
59 converter.goto_convert(code, where, mode);
61
62 natural_loops_mutablet natural_loops(where);
64 natural_loops.loop_map.size() == 0, "quantifier must not contain loops");
65
66 // `last` is the instruction corresponding to the last expression in the
67 // statement expression.
69 for(goto_programt::const_targett it = where.instructions.begin();
70 it != where.instructions.end();
71 ++it)
72 {
73 // `last` is an other-instruction.
74 if(it->is_other())
75 {
76 last = it;
77 }
78 }
79
81 last != where.instructions.end(),
82 "expression statements must contain a terminator expression");
83
84 auto last_expr = to_code_expression(last->get_other()).expression();
85
86 struct pathst
87 {
88 // `paths` contains all the `targett` we are iterating over.
89 std::vector<goto_programt::const_targett> paths;
90 std::vector<std::pair<exprt, replace_mapt>> path_conditions_and_value_maps;
91
92 pathst(
93 std::vector<goto_programt::const_targett> paths,
94 std::vector<std::pair<exprt, replace_mapt>>
96 : paths(paths),
98 {
99 }
100
101 bool empty()
102 {
103 return paths.empty();
104 }
105
107 {
108 return paths.back();
109 }
110
112 {
113 return path_conditions_and_value_maps.back().first;
114 }
115
117 {
118 return path_conditions_and_value_maps.back().second;
119 }
120
121 void push_back(
124 replace_mapt value_map)
125 {
126 paths.push_back(target);
128 std::make_pair(path_condition, value_map));
129 }
130
131 void pop_back()
132 {
133 paths.pop_back();
135 }
136 };
137
138 pathst paths(
139 {1, where.instructions.begin()},
140 {1, std::make_pair(true_exprt(), replace_mapt())});
141
142 std::unordered_set<symbol_exprt, irep_hash> declared_symbols;
143 // All bound variables are local.
144 declared_symbols.insert(qex.variables().begin(), qex.variables().end());
145
146 exprt res = true_exprt();
147
148 // Visit the quantifier body along `paths`.
149 while(!paths.empty())
150 {
151 auto &current_it = paths.back_it();
152 auto &path_condition = paths.back_path_condition();
153 auto &value_map = paths.back_value_map();
154 INVARIANT(
155 current_it != where.instructions.end(),
156 "Quantifier body must have a unique end expression.");
157
158 switch(current_it->type())
159 {
160 // Add all local-declared symbols into `declared_symbols`.
162 declared_symbols.insert(current_it->decl_symbol());
163 break;
164
165 // ASSIGN lhs := rhs
166 // Add the replace lhr <- value_map(rhs) to the current value_map.
168 {
169 // Check that if lhs is a declared symbol.
170 auto lhs = current_it->assign_lhs();
171 INVARIANT(
173 "quantifier must not contain side effects");
174 exprt rhs = current_it->assign_rhs();
175 replace_expr(value_map, rhs);
176 value_map[lhs] = rhs;
177 }
178 break;
179
180 // GOTO label
181 // -----------
182 // Move the current targett to label.
183 // or
184 // IF cond GOTO label
185 // ----------
186 // Move the current targett to targett+1 with path condition
187 // path_condition && !cond;
188 // and add a new path starting from label with path condition
189 // path_condition && cond.
191 {
192 if(!current_it->condition().is_true())
193 {
194 auto next_it = current_it->targets.front();
196 replace_mapt copy_symbol_map = value_map;
197 auto copy_condition = current_it->condition();
200 current_it++;
201 paths.push_back(
202 next_it,
205 }
206 else
207 {
208 current_it = current_it->targets.front();
209 }
210 continue;
211 }
212
213 // EXPRESSION(expr)
214 // The last instruction is an expression statement.
215 // We add the predicate path_condition ==> value_map(expr) to res.
217 {
218 if(current_it == last)
219 {
223 paths.pop_back();
224 continue;
225 }
226 }
227 break;
228
229 // Ignored instructions.
238 break;
239
240 // Unsupported instructions.
250 }
251
252 current_it++;
253 }
254 return res;
255}
256
258 const exprt &expr,
259 goto_programt &dest,
260 const irep_idt &mode)
261{
262 const source_locationt source_location = expr.find_source_location();
263
264 symbolt &new_symbol = get_fresh_aux_symbol(
265 expr.type(),
267 "literal",
268 source_location,
269 mode,
272 new_symbol.value = expr;
273
274 // The value might depend on a variable, thus
275 // generate code for this.
276
277 symbol_exprt result = new_symbol.symbol_expr();
278 result.add_source_location() = source_location;
279
280 // The lifetime of compound literals is really that of
281 // the block they are in.
282 if(!new_symbol.is_static_lifetime)
283 copy(code_declt(result), DECL, dest);
284
286 code_assign.add_source_location() = source_location;
287 convert(code_assign, dest, mode);
288
289 // now create a 'dead' instruction
290 if(!new_symbol.is_static_lifetime)
291 {
293 targets.scope_stack.add(std::move(code_dead), {});
294 }
295
296 return result;
297}
298
305{
306 if(
307 expr.id() == ID_side_effect || expr.id() == ID_compound_literal ||
308 expr.id() == ID_comma)
309 {
310 return true;
311 }
312
313 // We can't flatten quantified expressions by introducing new literals for
314 // conditional expressions. This is because the body of the quantified
315 // may refer to bound variables, which are not visible outside the scope
316 // of the quantifier.
317 //
318 // For example, the following transformation would not be valid:
319 //
320 // forall (i : int) (i == 0 || i > 10)
321 //
322 // transforming to
323 //
324 // g1 = (i == 0)
325 // g2 = (i > 10)
326 // forall (i : int) (g1 || g2)
327 if(expr.id() == ID_forall || expr.id() == ID_exists)
328 {
329 code_expressiont where{to_quantifier_expr(expr).where()};
330 // Need cleaning when the quantifier body is a side-effect expression.
331 if(has_subexpr(expr, ID_side_effect))
332 return true;
333
334 return false;
335 }
336
337 for(const auto &op : expr.operands())
338 {
339 if(needs_cleaning(op))
340 return true;
341 }
342
343 return false;
344}
345
348{
350 expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies);
352 expr.is_boolean(),
354 "'",
355 expr.id(),
356 "' must be Boolean, but got ",
358
359 const source_locationt source_location = expr.find_source_location();
360
361 // re-write "a ==> b" into a?b:1
362 if(auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
363 {
364 expr = if_exprt{
365 std::move(implies->lhs()),
366 std::move(implies->rhs()),
367 true_exprt{}.with_source_location(source_location),
368 bool_typet{}};
369 return;
370 }
371
372 // re-write "a && b" into nested a?b:0
373 // re-write "a || b" into nested a?1:b
374
375 exprt tmp;
376
377 if(expr.id() == ID_and)
378 tmp = true_exprt();
379 else // ID_or
380 tmp = false_exprt();
381
382 tmp.add_source_location() = source_location;
383
384 exprt::operandst &ops = expr.operands();
385
386 // start with last one
387 for(exprt::operandst::reverse_iterator it = ops.rbegin(); it != ops.rend();
388 ++it)
389 {
390 exprt &op = *it;
391
393 op.is_boolean(),
394 "boolean operators must have only boolean operands",
395 source_location);
396
397 if(expr.id() == ID_and)
398 {
399 exprt if_e =
400 if_exprt{op, tmp, false_exprt{}.with_source_location(source_location)}
401 .with_source_location(source_location);
402 tmp.swap(if_e);
403 continue;
404 }
405 if(expr.id() == ID_or)
406 {
407 exprt if_e =
408 if_exprt{op, true_exprt{}.with_source_location(source_location), tmp}
409 .with_source_location(source_location);
410 tmp.swap(if_e);
411 continue;
412 }
414 }
415
416 expr.swap(tmp);
417}
418
420 exprt &expr,
421 const irep_idt &mode,
422 bool result_is_used)
423{
424 // this cleans:
425 // && || ==> ?: comma (control-dependency)
426 // function calls
427 // object constructors like arrays, string constants, structs
428 // ++ -- (pre and post)
429 // compound assignments
430 // compound literals
431
432 if(!needs_cleaning(expr))
433 return {};
434
435 if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies)
436 {
437 // rewrite into ?:
438 rewrite_boolean(expr);
439
440 // recursive call
441 return clean_expr(expr, mode, result_is_used);
442 }
443 else if(expr.id() == ID_if)
444 {
445 // first clean condition
446 clean_expr_resultt side_effects =
447 clean_expr(to_if_expr(expr).cond(), mode, true);
448
449 // possibly done now
450 if(
451 !needs_cleaning(to_if_expr(expr).true_case()) &&
452 !needs_cleaning(to_if_expr(expr).false_case()))
453 {
454 return side_effects;
455 }
456
457 // copy expression
459
461 if_expr.cond().is_boolean(),
462 "condition for an 'if' must be boolean",
463 if_expr.find_source_location());
464
465 const source_locationt source_location = expr.find_source_location();
466
467#if 0
468 // We do some constant-folding here, to mimic
469 // what typical compilers do.
470 {
471 exprt tmp_cond=if_expr.cond();
473 if(tmp_cond.is_true())
474 {
475 clean_expr(if_expr.true_case(), dest, result_is_used);
476 expr=if_expr.true_case();
477 return;
478 }
479 else if(tmp_cond.is_false())
480 {
481 clean_expr(if_expr.false_case(), dest, result_is_used);
482 expr=if_expr.false_case();
483 return;
484 }
485 }
486#endif
487
489 clean_expr(if_expr.true_case(), mode, result_is_used));
490
492 clean_expr(if_expr.false_case(), mode, result_is_used));
493
495 {
496 symbolt &new_symbol = new_tmp_symbol(
497 expr.type(),
498 "if_expr",
499 side_effects.side_effects,
500 source_location,
501 mode);
502
504 assignment_true.lhs() = new_symbol.symbol_expr();
505 assignment_true.rhs() = if_expr.true_case();
506 assignment_true.add_source_location() = source_location;
507 convert(assignment_true, tmp_true.side_effects, mode);
508
510 assignment_false.lhs() = new_symbol.symbol_expr();
511 assignment_false.rhs() = if_expr.false_case();
512 assignment_false.add_source_location() = source_location;
513 convert(assignment_false, tmp_false.side_effects, mode);
514
515 // overwrites expr
516 expr = new_symbol.symbol_expr();
517 }
518 else
519 {
520 // preserve the expressions for possible later checks
521 if(if_expr.true_case().is_not_nil())
522 {
523 // add a (void) type cast so that is_skip catches it in case the
524 // expression is just a constant
526 typecast_exprt(if_expr.true_case(), empty_typet()));
527 convert(code_expression, tmp_true.side_effects, mode);
528 }
529
530 if(if_expr.false_case().is_not_nil())
531 {
532 // add a (void) type cast so that is_skip catches it in case the
533 // expression is just a constant
535 typecast_exprt(if_expr.false_case(), empty_typet()));
536 convert(code_expression, tmp_false.side_effects, mode);
537 }
538
539 expr = nil_exprt();
540 }
541
542 // generate guard for argument side-effects
544 if_expr.cond(),
545 source_location,
546 tmp_true.side_effects,
547 if_expr.true_case().source_location(),
548 tmp_false.side_effects,
549 if_expr.false_case().source_location(),
550 side_effects.side_effects,
551 mode);
552
553 destruct_locals(tmp_false.temporaries, side_effects.side_effects, ns);
554 destruct_locals(tmp_true.temporaries, side_effects.side_effects, ns);
555 destruct_locals(side_effects.temporaries, side_effects.side_effects, ns);
556 side_effects.temporaries.clear();
557
558 if(expr.is_not_nil())
559 side_effects.add_temporary(to_symbol_expr(expr).get_identifier());
560
561 return side_effects;
562 }
563 else if(expr.id() == ID_comma)
564 {
565 clean_expr_resultt side_effects;
566
568 {
570
571 Forall_operands(it, expr)
572 {
573 bool last = (it == --expr.operands().end());
574
575 // special treatment for last one
576 if(last)
577 {
578 result.swap(*it);
579 side_effects.add(clean_expr(result, mode, true));
580 }
581 else
582 {
583 side_effects.add(clean_expr(*it, mode, false));
584
585 // remember these for later checks
586 if(it->is_not_nil())
587 convert(code_expressiont(*it), side_effects.side_effects, mode);
588 }
589 }
590
591 expr.swap(result);
592 }
593 else // result not used
594 {
595 Forall_operands(it, expr)
596 {
597 side_effects.add(clean_expr(*it, mode, false));
598
599 // remember as expression statement for later checks
600 if(it->is_not_nil())
601 convert(code_expressiont(*it), side_effects.side_effects, mode);
602 }
603
604 expr = nil_exprt();
605 }
606
607 return side_effects;
608 }
609 else if(expr.id() == ID_typecast)
610 {
611 typecast_exprt &typecast = to_typecast_expr(expr);
612
613 // preserve 'result_is_used'
614 clean_expr_resultt side_effects =
615 clean_expr(typecast.op(), mode, result_is_used);
616
617 if(typecast.op().is_nil())
618 expr.make_nil();
619
620 return side_effects;
621 }
622 else if(expr.id() == ID_side_effect)
623 {
624 // some of the side-effects need special treatment!
625 const irep_idt statement = to_side_effect_expr(expr).get_statement();
626
627 if(statement == ID_gcc_conditional_expression)
628 {
629 // need to do separately
630 return remove_gcc_conditional_expression(expr, mode);
631 }
632 else if(statement == ID_statement_expression)
633 {
634 // need to do separately to prevent that
635 // the operands of expr get 'cleaned'
638 }
639 else if(statement == ID_assign)
640 {
641 // we do a special treatment for x=f(...)
642 INVARIANT(
643 expr.operands().size() == 2,
644 "side-effect assignment expressions must have two operands");
645
647
648 if(
649 side_effect_assign.rhs().id() == ID_side_effect &&
652 {
653 clean_expr_resultt side_effects =
654 clean_expr(side_effect_assign.lhs(), mode);
655 exprt lhs = side_effect_assign.lhs();
656
658 if(must_use_rhs)
659 {
660 side_effects.add(remove_function_call(
662 mode,
663 true));
664 }
665
666 // turn into code
669 side_effect_assign.rhs(), new_lhs.type());
670 code_assignt assignment(std::move(new_lhs), new_rhs);
671 assignment.add_source_location() = expr.source_location();
672 convert_assign(assignment, side_effects.side_effects, mode);
673
675 expr = must_use_rhs ? new_rhs : lhs;
676 else
677 expr.make_nil();
678
679 return side_effects;
680 }
681 }
682 }
683 else if(expr.id() == ID_forall || expr.id() == ID_exists)
684 {
686 code_expressiont code{qex.where()};
688 !has_subexpr(expr, ID_side_effect) ||
689 (code.operands()[0].id() == ID_side_effect &&
690 code.operands()[0].get_named_sub()[ID_statement].id() ==
692 "quantifier must not contain side effects");
693
694 // Handle the case that quantifier body is a statement expression.
695 if(
696 code.operands()[0].id() == ID_side_effect &&
697 code.operands()[0].get_named_sub()[ID_statement].id() ==
699 {
700 auto res = convert_statement_expression(qex, code, mode, *this);
701 qex.where() = res;
702 return clean_expr(res, mode, result_is_used);
703 }
704 }
705 else if(expr.id() == ID_address_of)
706 {
708 return clean_expr_address_of(addr.object(), mode);
709 }
710
711 clean_expr_resultt side_effects;
712
713 // TODO: evaluation order
714
715 Forall_operands(it, expr)
716 side_effects.add(clean_expr(*it, mode));
717
718 if(expr.id() == ID_side_effect)
719 {
720 side_effects.add(remove_side_effect(
721 to_side_effect_expr(expr), mode, result_is_used, false));
722 }
723 else if(expr.id() == ID_compound_literal)
724 {
725 // This is simply replaced by the literal
727 expr.operands().size() == 1, "ID_compound_literal has a single operand");
728 expr = to_unary_expr(expr).op();
729 }
730
731 return side_effects;
732}
733
736{
737 clean_expr_resultt side_effects;
738
739 // The address of object constructors can be taken,
740 // which is re-written into the address of a variable.
741
742 if(expr.id() == ID_compound_literal)
743 {
745 expr.operands().size() == 1, "ID_compound_literal has a single operand");
746 side_effects.add(clean_expr(to_unary_expr(expr).op(), mode));
748 to_unary_expr(expr).op(), side_effects.side_effects, mode);
749 }
750 else if(expr.id() == ID_string_constant)
751 {
752 // Leave for now, but long-term these might become static symbols.
753 // LLVM appears to do precisely that.
754 }
755 else if(expr.id() == ID_index)
756 {
758 side_effects.add(clean_expr_address_of(index_expr.array(), mode));
759 side_effects.add(clean_expr(index_expr.index(), mode));
760 }
761 else if(expr.id() == ID_dereference)
762 {
764 side_effects.add(clean_expr(deref_expr.pointer(), mode));
765 }
766 else if(expr.id() == ID_comma)
767 {
768 // Yes, one can take the address of a comma expression.
769 // Treatment is similar to clean_expr() above.
770
772
773 Forall_operands(it, expr)
774 {
775 bool last = (it == --expr.operands().end());
776
777 // special treatment for last one
778 if(last)
779 result.swap(*it);
780 else
781 {
782 side_effects.add(clean_expr(*it, mode, false));
783
784 // get any side-effects
785 if(it->is_not_nil())
786 convert(code_expressiont(*it), side_effects.side_effects, mode);
787 }
788 }
789
790 expr.swap(result);
791
792 // do again
793 side_effects.add(clean_expr_address_of(expr, mode));
794 }
795 else if(expr.id() == ID_side_effect)
796 {
797 side_effects.add(
798 remove_side_effect(to_side_effect_expr(expr), mode, true, true));
799 }
800 else
801 Forall_operands(it, expr)
802 side_effects.add(clean_expr_address_of(*it, mode));
803
804 return side_effects;
805}
806
809 exprt &expr,
810 const irep_idt &mode)
811{
812 clean_expr_resultt side_effects;
813
814 {
815 auto &binary_expr = to_binary_expr(expr);
816
817 // first remove side-effects from condition
818 side_effects = clean_expr(to_binary_expr(expr).op0(), mode);
819
820 // now we can copy op0 safely
823 binary_expr.op0(),
824 binary_expr.op1(),
825 expr.type());
826 if_expr.add_source_location() = expr.source_location();
827
828 expr.swap(if_expr);
829 }
830
831 // there might still be junk in expr.op2()
832 side_effects.add(clean_expr(expr, mode));
833
834 return side_effects;
835}
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
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:562
Boolean AND.
Definition std_expr.h:2125
The Boolean type.
Definition std_types.h:36
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
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:51
Base class for all expressions.
Definition expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:147
std::vector< exprt > operandst
Definition expr.h:58
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:224
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:231
source_locationt & add_source_location()
Definition expr.h:236
exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
Definition expr.h:101
The Boolean constant false.
Definition std_expr.h:3199
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 goto_convert(const codet &code, goto_programt &dest, 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)
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:2497
Boolean implication.
Definition std_expr.h:2225
Array index operator.
Definition std_expr.h:1470
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
mstreamt & result() const
Definition message.h:401
The NIL expression.
Definition std_expr.h:3208
Boolean negation.
Definition std_expr.h:2454
A base class for quantifier expressions.
const irep_idt & get_statement() const
Definition std_code.h:1472
Expression to hold a symbol (variable)
Definition std_expr.h:131
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:3190
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
const exprt & op() const
Definition std_expr.h:391
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:27
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, goto_convertt &converter)
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:1538
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2577
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
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.