CBMC: /home/runner/work/cbmc/cbmc/src/ansi-c/goto-conversion/goto_clean_expr.cpp Source File

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/expr_util.h>
15#include <util/fresh_symbol.h>
16#include <util/mathematical_expr.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
22#include <analyses/natural_loops.h>
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 if(expr.id() == ID_typecast)
47 {
48 return find_base_symbol(to_typecast_expr(expr).op());
49 }
50 else if(expr.id() == ID_address_of)
51 {
52 return find_base_symbol(to_address_of_expr(expr).op());
53 }
54 else
55 {
56 throw "unsupported expression type for finding base symbol";
57 }
58}
59
61 const quantifier_exprt &qex,
62 const code_expressiont &code,
63 const irep_idt &mode,
64 symbol_table_baset &symbol_table,
65 message_handlert &message_handler)
66{
67 goto_programt where;
68 goto_convertt converter{symbol_table, message_handler};
69 converter.goto_convert(code, where, mode);
71
72 natural_loops_mutablet natural_loops(where);
74 natural_loops.loop_map.size() == 0, "quantifier must not contain loops");
75
76 std::unordered_set<symbol_exprt, irep_hash> declared_symbols;
77 // All bound variables are local.
78 declared_symbols.insert(qex.variables().begin(), qex.variables().end());
79
80 // `last` is the instruction corresponding to the last expression in the
81 // statement expression.
83 for(goto_programt::const_targett it = where.instructions.begin();
84 it != where.instructions.end();
85 ++it)
86 {
87 // `last` is an other-instruction.
88 if(it->is_other())
89 {
90 last = it;
91 }
92
93 if(it->is_decl())
94 {
95 declared_symbols.insert(it->decl_symbol());
96 }
97 }
98
100 last != where.instructions.end(),
101 "expression statements must contain a terminator expression");
102
103 auto last_expr = to_code_expression(last->get_other()).expression();
104 if(
105 last_expr.id() == ID_typecast &&
106 to_typecast_expr(last_expr).type().id() == ID_empty)
107 {
109 }
110
111 struct pathst
112 {
113 // `paths` contains all the `targett` we are iterating over.
114 std::vector<goto_programt::const_targett> paths;
115 std::vector<std::pair<exprt, replace_mapt>> path_conditions_and_value_maps;
116
117 pathst(
118 std::vector<goto_programt::const_targett> paths,
119 std::vector<std::pair<exprt, replace_mapt>>
121 : paths(paths),
123 {
124 }
125
126 bool empty()
127 {
128 return paths.empty();
129 }
130
132 {
133 return paths.back();
134 }
135
137 {
138 return path_conditions_and_value_maps.back().first;
139 }
140
142 {
143 return path_conditions_and_value_maps.back().second;
144 }
145
146 void push_back(
149 replace_mapt value_map)
150 {
151 paths.push_back(target);
153 std::make_pair(path_condition, value_map));
154 }
155
156 void pop_back()
157 {
158 paths.pop_back();
160 }
161 };
162
163 pathst paths(
164 {1, where.instructions.begin()},
165 {1, std::make_pair(true_exprt(), replace_mapt())});
166
167 exprt res = true_exprt();
168
169 // Visit the quantifier body along `paths`.
170 while(!paths.empty())
171 {
172 auto &current_it = paths.back_it();
173 auto &path_condition = paths.back_path_condition();
174 auto &value_map = paths.back_value_map();
175
176 if(current_it == where.instructions.end())
177 {
178 paths.pop_back();
179 continue;
180 }
181
182 switch(current_it->type())
183 {
184 // Add all local-declared symbols into `declared_symbols`.
186 declared_symbols.insert(current_it->decl_symbol());
187 break;
188
189 // ASSIGN lhs := rhs
190 // Add the replace lhr <- value_map(rhs) to the current value_map.
192 {
193 // Check that if lhs is a declared symbol.
194 auto lhs = current_it->assign_lhs();
195 INVARIANT(
197 "quantifier must not contain side effects");
198 exprt rhs = current_it->assign_rhs();
199 replace_expr(value_map, rhs);
200 value_map[lhs] = rhs;
201 }
202 break;
203
204 // GOTO label
205 // -----------
206 // Move the current targett to label.
207 // or
208 // IF cond GOTO label
209 // ----------
210 // Move the current targett to targett+1 with path condition
211 // path_condition && !cond;
212 // and add a new path starting from label with path condition
213 // path_condition && cond.
215 {
216 exprt condition = current_it->condition();
217 replace_expr(value_map, condition);
218 if(condition != true)
219 {
220 auto next_it = current_it->targets.front();
223 current_it++;
224 paths.push_back(
225 next_it, and_exprt(copy_path_condition, condition), value_map);
226 }
227 else
228 {
229 current_it = current_it->targets.front();
230 }
231 continue;
232 }
233
234 // EXPRESSION(expr)
235 // The last instruction is an expression statement.
236 // We add the predicate path_condition ==> value_map(expr) to res.
238 {
239 if(current_it == last)
240 {
244 paths.pop_back();
245 continue;
246 }
247 }
248 break;
249
250 // Ignored instructions.
259 break;
260
261 // Unsupported instructions.
271 }
272
273 current_it++;
274 }
275 return res;
276}
277
279 const exprt &expr,
280 goto_programt &dest,
281 const irep_idt &mode)
282{
283 const source_locationt source_location = expr.find_source_location();
284
285 symbolt &new_symbol = get_fresh_aux_symbol(
286 expr.type(),
288 "literal",
289 source_location,
290 mode,
293 new_symbol.value = expr;
294
295 // The value might depend on a variable, thus
296 // generate code for this.
297
298 symbol_exprt result = new_symbol.symbol_expr();
299 result.add_source_location() = source_location;
300
301 // The lifetime of compound literals is really that of
302 // the block they are in.
303 if(!new_symbol.is_static_lifetime)
304 copy(code_declt(result), DECL, dest);
305
307 code_assign.add_source_location() = source_location;
308 convert(code_assign, dest, mode);
309
310 // now create a 'dead' instruction
311 if(!new_symbol.is_static_lifetime)
312 {
314 targets.scope_stack.add(std::move(code_dead), {});
315 }
316
317 return result;
318}
319
326{
327 if(
328 expr.id() == ID_side_effect || expr.id() == ID_compound_literal ||
329 expr.id() == ID_comma)
330 {
331 return true;
332 }
333
334 // We can't flatten quantified expressions by introducing new literals for
335 // conditional expressions. This is because the body of the quantified
336 // may refer to bound variables, which are not visible outside the scope
337 // of the quantifier.
338 //
339 // For example, the following transformation would not be valid:
340 //
341 // forall (i : int) (i == 0 || i > 10)
342 //
343 // transforming to
344 //
345 // g1 = (i == 0)
346 // g2 = (i > 10)
347 // forall (i : int) (g1 || g2)
348 if(expr.id() == ID_forall || expr.id() == ID_exists)
349 {
350 code_expressiont where{to_quantifier_expr(expr).where()};
351 // Need cleaning when the quantifier body is a side-effect expression.
352 if(has_subexpr(expr, ID_side_effect))
353 return true;
354
355 return false;
356 }
357
358 for(const auto &op : expr.operands())
359 {
360 if(needs_cleaning(op))
361 return true;
362 }
363
364 return false;
365}
366
369{
371 expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies);
373 expr.is_boolean(),
375 "'",
376 expr.id(),
377 "' must be Boolean, but got ",
379
380 const source_locationt source_location = expr.find_source_location();
381
382 // re-write "a ==> b" into a?b:1
383 if(auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
384 {
385 expr = if_exprt{
386 std::move(implies->lhs()),
387 std::move(implies->rhs()),
388 true_exprt{}.with_source_location(source_location),
389 bool_typet{}};
390 return;
391 }
392
393 // re-write "a && b" into nested a?b:0
394 // re-write "a || b" into nested a?1:b
395
396 exprt tmp;
397
398 if(expr.id() == ID_and)
399 tmp = true_exprt();
400 else // ID_or
401 tmp = false_exprt();
402
403 tmp.add_source_location() = source_location;
404
405 exprt::operandst &ops = expr.operands();
406
407 // start with last one
408 for(exprt::operandst::reverse_iterator it = ops.rbegin(); it != ops.rend();
409 ++it)
410 {
411 exprt &op = *it;
412
414 op.is_boolean(),
415 "boolean operators must have only boolean operands",
416 source_location);
417
418 if(expr.id() == ID_and)
419 {
420 exprt if_e =
421 if_exprt{op, tmp, false_exprt{}.with_source_location(source_location)}
422 .with_source_location(source_location);
423 tmp.swap(if_e);
424 continue;
425 }
426 if(expr.id() == ID_or)
427 {
428 exprt if_e =
429 if_exprt{op, true_exprt{}.with_source_location(source_location), tmp}
430 .with_source_location(source_location);
431 tmp.swap(if_e);
432 continue;
433 }
435 }
436
437 expr.swap(tmp);
438}
439
441 exprt &expr,
442 const irep_idt &mode,
443 bool result_is_used)
444{
445 // this cleans:
446 // && || ==> ?: comma (control-dependency)
447 // function calls
448 // object constructors like arrays, string constants, structs
449 // ++ -- (pre and post)
450 // compound assignments
451 // compound literals
452
453 if(!needs_cleaning(expr))
454 return {};
455
456 if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies)
457 {
458 // rewrite into ?:
459 rewrite_boolean(expr);
460
461 // recursive call
462 return clean_expr(expr, mode, result_is_used);
463 }
464 else if(expr.id() == ID_if)
465 {
466 // first clean condition
467 clean_expr_resultt side_effects =
468 clean_expr(to_if_expr(expr).cond(), mode, true);
469
470 // possibly done now
471 if(
472 !needs_cleaning(to_if_expr(expr).true_case()) &&
473 !needs_cleaning(to_if_expr(expr).false_case()))
474 {
475 return side_effects;
476 }
477
478 // copy expression
480
482 if_expr.cond().is_boolean(),
483 "condition for an 'if' must be boolean",
484 if_expr.find_source_location());
485
486 const source_locationt source_location = expr.find_source_location();
487
488#if 0
489 // We do some constant-folding here, to mimic
490 // what typical compilers do.
491 {
492 exprt tmp_cond=if_expr.cond();
494 if(tmp_cond.is_true())
495 {
496 clean_expr(if_expr.true_case(), dest, result_is_used);
497 expr=if_expr.true_case();
498 return;
499 }
500 else if(tmp_cond.is_false())
501 {
502 clean_expr(if_expr.false_case(), dest, result_is_used);
503 expr=if_expr.false_case();
504 return;
505 }
506 }
507#endif
508
510 clean_expr(if_expr.true_case(), mode, result_is_used));
511
513 clean_expr(if_expr.false_case(), mode, result_is_used));
514
516 {
517 symbolt &new_symbol = new_tmp_symbol(
518 expr.type(),
519 "if_expr",
520 side_effects.side_effects,
521 source_location,
522 mode);
523
525 assignment_true.lhs() = new_symbol.symbol_expr();
526 assignment_true.rhs() = if_expr.true_case();
527 assignment_true.add_source_location() = source_location;
528 convert(assignment_true, tmp_true.side_effects, mode);
529
531 assignment_false.lhs() = new_symbol.symbol_expr();
532 assignment_false.rhs() = if_expr.false_case();
533 assignment_false.add_source_location() = source_location;
534 convert(assignment_false, tmp_false.side_effects, mode);
535
536 // overwrites expr
537 expr = new_symbol.symbol_expr();
538 }
539 else
540 {
541 // preserve the expressions for possible later checks
542 if(if_expr.true_case().is_not_nil())
543 {
544 // add a (void) type cast so that is_skip catches it in case the
545 // expression is just a constant
547 typecast_exprt(if_expr.true_case(), empty_typet()));
548 convert(code_expression, tmp_true.side_effects, mode);
549 }
550
551 if(if_expr.false_case().is_not_nil())
552 {
553 // add a (void) type cast so that is_skip catches it in case the
554 // expression is just a constant
556 typecast_exprt(if_expr.false_case(), empty_typet()));
557 convert(code_expression, tmp_false.side_effects, mode);
558 }
559
560 expr = nil_exprt();
561 }
562
563 // generate guard for argument side-effects
565 if_expr.cond(),
566 source_location,
567 tmp_true.side_effects,
568 if_expr.true_case().source_location(),
569 tmp_false.side_effects,
570 if_expr.false_case().source_location(),
571 side_effects.side_effects,
572 mode);
573
574 destruct_locals(tmp_false.temporaries, side_effects.side_effects, ns);
575 destruct_locals(tmp_true.temporaries, side_effects.side_effects, ns);
576 destruct_locals(side_effects.temporaries, side_effects.side_effects, ns);
577 side_effects.temporaries.clear();
578
579 if(expr.is_not_nil())
580 side_effects.add_temporary(to_symbol_expr(expr).identifier());
581
582 return side_effects;
583 }
584 else if(expr.id() == ID_comma)
585 {
586 clean_expr_resultt side_effects;
587
589 {
591
592 Forall_operands(it, expr)
593 {
594 bool last = (it == --expr.operands().end());
595
596 // special treatment for last one
597 if(last)
598 {
599 result.swap(*it);
600 side_effects.add(clean_expr(result, mode, true));
601 }
602 else
603 {
604 side_effects.add(clean_expr(*it, mode, false));
605
606 // remember these for later checks
607 if(it->is_not_nil())
608 convert(code_expressiont(*it), side_effects.side_effects, mode);
609 }
610 }
611
612 expr.swap(result);
613 }
614 else // result not used
615 {
616 Forall_operands(it, expr)
617 {
618 side_effects.add(clean_expr(*it, mode, false));
619
620 // remember as expression statement for later checks
621 if(it->is_not_nil())
622 convert(code_expressiont(*it), side_effects.side_effects, mode);
623 }
624
625 expr = nil_exprt();
626 }
627
628 return side_effects;
629 }
630 else if(expr.id() == ID_typecast)
631 {
632 typecast_exprt &typecast = to_typecast_expr(expr);
633
634 // preserve 'result_is_used'
635 clean_expr_resultt side_effects =
636 clean_expr(typecast.op(), mode, result_is_used);
637
638 if(typecast.op().is_nil())
639 expr.make_nil();
640
641 return side_effects;
642 }
643 else if(expr.id() == ID_side_effect)
644 {
645 // some of the side-effects need special treatment!
646 const irep_idt statement = to_side_effect_expr(expr).get_statement();
647
648 if(statement == ID_gcc_conditional_expression)
649 {
650 // need to do separately
651 return remove_gcc_conditional_expression(expr, mode);
652 }
653 else if(statement == ID_statement_expression)
654 {
655 // need to do separately to prevent that
656 // the operands of expr get 'cleaned'
659 }
660 else if(statement == ID_assign)
661 {
662 // we do a special treatment for x=f(...)
663 INVARIANT(
664 expr.operands().size() == 2,
665 "side-effect assignment expressions must have two operands");
666
668
669 if(
670 side_effect_assign.rhs().id() == ID_side_effect &&
673 {
674 clean_expr_resultt side_effects =
675 clean_expr(side_effect_assign.lhs(), mode);
676 exprt lhs = side_effect_assign.lhs();
677
679 if(must_use_rhs)
680 {
681 side_effects.add(remove_function_call(
683 mode,
684 true));
685 }
686
687 // turn into code
690 side_effect_assign.rhs(), new_lhs.type());
691 code_assignt assignment(std::move(new_lhs), new_rhs);
692 assignment.add_source_location() = expr.source_location();
693 convert_assign(assignment, side_effects.side_effects, mode);
694
696 expr = must_use_rhs ? new_rhs : lhs;
697 else
698 expr.make_nil();
699
700 return side_effects;
701 }
702 }
703 }
704 else if(expr.id() == ID_forall || expr.id() == ID_exists)
705 {
707 code_expressiont code{qex.where()};
709 !has_subexpr(expr, ID_side_effect) ||
710 (code.operands()[0].id() == ID_side_effect &&
711 code.operands()[0].get_named_sub()[ID_statement].id() ==
713 "quantifier must not contain side effects");
714
715 // Handle the case that quantifier body is a statement expression.
716 if(
717 code.operands()[0].id() == ID_side_effect &&
718 code.operands()[0].get_named_sub()[ID_statement].id() ==
720 {
722 qex, code, mode, symbol_table, get_message_handler());
723 qex.where() = res;
724 return clean_expr(res, mode, result_is_used);
725 }
726 }
727 else if(expr.id() == ID_address_of)
728 {
730 return clean_expr_address_of(addr.object(), mode);
731 }
732
733 clean_expr_resultt side_effects;
734
735 // TODO: evaluation order
736
737 Forall_operands(it, expr)
738 side_effects.add(clean_expr(*it, mode));
739
740 if(expr.id() == ID_side_effect)
741 {
742 side_effects.add(remove_side_effect(
743 to_side_effect_expr(expr), mode, result_is_used, false));
744 }
745 else if(expr.id() == ID_compound_literal)
746 {
747 // This is simply replaced by the literal
749 expr.operands().size() == 1, "ID_compound_literal has a single operand");
750 expr = to_unary_expr(expr).op();
751 }
752
753 return side_effects;
754}
755
756goto_convertt::clean_expr_resultt
758{
759 clean_expr_resultt side_effects;
760
761 // The address of object constructors can be taken,
762 // which is re-written into the address of a variable.
763
764 if(expr.id() == ID_compound_literal)
765 {
767 expr.operands().size() == 1, "ID_compound_literal has a single operand");
768 side_effects.add(clean_expr(to_unary_expr(expr).op(), mode));
770 to_unary_expr(expr).op(), side_effects.side_effects, mode);
771 }
772 else if(expr.id() == ID_string_constant)
773 {
774 // Leave for now, but long-term these might become static symbols.
775 // LLVM appears to do precisely that.
776 }
777 else if(expr.id() == ID_index)
778 {
780 side_effects.add(clean_expr_address_of(index_expr.array(), mode));
781 side_effects.add(clean_expr(index_expr.index(), mode));
782 }
783 else if(expr.id() == ID_dereference)
784 {
786 side_effects.add(clean_expr(deref_expr.pointer(), mode));
787 }
788 else if(expr.id() == ID_comma)
789 {
790 // Yes, one can take the address of a comma expression.
791 // Treatment is similar to clean_expr() above.
792
794
795 Forall_operands(it, expr)
796 {
797 bool last = (it == --expr.operands().end());
798
799 // special treatment for last one
800 if(last)
801 result.swap(*it);
802 else
803 {
804 side_effects.add(clean_expr(*it, mode, false));
805
806 // get any side-effects
807 if(it->is_not_nil())
808 convert(code_expressiont(*it), side_effects.side_effects, mode);
809 }
810 }
811
812 expr.swap(result);
813
814 // do again
815 side_effects.add(clean_expr_address_of(expr, mode));
816 }
817 else if(expr.id() == ID_side_effect)
818 {
819 side_effects.add(
820 remove_side_effect(to_side_effect_expr(expr), mode, true, true));
821 }
822 else
823 Forall_operands(it, expr)
824 side_effects.add(clean_expr_address_of(*it, mode));
825
826 return side_effects;
827}
828
829goto_convertt::clean_expr_resultt
831 exprt &expr,
832 const irep_idt &mode)
833{
834 clean_expr_resultt side_effects;
835
836 {
837 auto &binary_expr = to_binary_expr(expr);
838
839 // first remove side-effects from condition
840 side_effects = clean_expr(to_binary_expr(expr).op0(), mode);
841
842 // now we can copy op0 safely
845 binary_expr.op0(),
846 binary_expr.op1(),
847 expr.type());
848 if_expr.add_source_location() = expr.source_location();
849
850 expr.swap(if_expr);
851 }
852
853 // there might still be junk in expr.op2()
854 side_effects.add(clean_expr(expr, mode));
855
856 return side_effects;
857}
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
Operator to return the address of an object.
Definition pointer_expr.h:540
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
Operator to dereference a pointer.
Definition pointer_expr.h:834
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)
lifetimet lifetime
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.
namespacet ns
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.
Definition goto_program.h:72
instructionst instructions
The list of instructions in the goto program.
Definition goto_program.h:621
instructionst::const_iterator const_targett
Definition goto_program.h:614
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition goto_program.h:765
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
Definition loop_analysis.h:88
Definition message.h:27
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.
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)
Definition destructor.cpp:62
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
Definition expr_util.cpp:188
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition expr_util.cpp:110
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
Definition goto_program.h:48
@ ATOMIC_END
Definition goto_program.h:43
@ DEAD
Definition goto_program.h:47
@ LOCATION
Definition goto_program.h:40
@ END_FUNCTION
Definition goto_program.h:41
@ ASSIGN
Definition goto_program.h:45
@ ASSERT
Definition goto_program.h:35
@ SET_RETURN_VALUE
Definition goto_program.h:44
@ ATOMIC_BEGIN
Definition goto_program.h:42
@ CATCH
Definition goto_program.h:50
@ END_THREAD
Definition goto_program.h:39
@ SKIP
Definition goto_program.h:37
@ NO_INSTRUCTION_TYPE
Definition goto_program.h:32
@ START_THREAD
Definition goto_program.h:38
@ THROW
Definition goto_program.h:49
@ DECL
Definition goto_program.h:46
@ OTHER
Definition goto_program.h:36
@ GOTO
Definition goto_program.h:33
@ INCOMPLETE_GOTO
Definition goto_program.h:51
@ ASSUME
Definition goto_program.h:34
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.
Definition pointer_expr.h:577
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition pointer_expr.h:890
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
Definition replace_expr.h:22
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.
Definition irep.h:495
Symbol table entry.

AltStyle によって変換されたページ (->オリジナル) /