cprover
Loading...
Searching...
No Matches
constant_propagator.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Constant propagation
4
5Author: Peter Schrammel
6
7\*******************************************************************/
8
11
12#include "constant_propagator.h"
13
15
16#ifdef DEBUG
17#include <iostream>
18#include <util/format_expr.h>
19#endif
20
21#include <util/arith_tools.h>
22#include <util/c_types.h>
23#include <util/cprover_prefix.h>
24#include <util/expr_util.h>
25#include <util/ieee_float.h>
27#include <util/simplify_expr.h>
28#include <util/std_code.h>
29
31
32#include <algorithm>
33#include <array>
34
54 valuest &dest_values,
55 const exprt &lhs,
56 const exprt &rhs,
57 const namespacet &ns,
59 bool is_assignment)
60{
61 if(lhs.id() == ID_dereference)
62 {
63 exprt eval_lhs = lhs;
64 if(partial_evaluate(dest_values, eval_lhs, ns))
65 {
66 if(is_assignment)
67 {
68 const bool have_dirty = (cp != nullptr);
69
70 if(have_dirty)
71 dest_values.set_dirty_to_top(cp->dirty, ns);
72 else
73 dest_values.set_to_top();
74 }
75 // Otherwise disregard this unknown deref in a read-only context.
76 }
77 else
78 assign_rec(dest_values, eval_lhs, rhs, ns, cp, is_assignment);
79 }
80 else if(lhs.id() == ID_index)
81 {
82 const index_exprt &index_expr = to_index_expr(lhs);
83 with_exprt new_rhs(index_expr.array(), index_expr.index(), rhs);
84 assign_rec(dest_values, index_expr.array(), new_rhs, ns, cp, is_assignment);
85 }
86 else if(lhs.id() == ID_member)
87 {
88 const member_exprt &member_expr = to_member_expr(lhs);
89 with_exprt new_rhs(member_expr.compound(), exprt(ID_member_name), rhs);
90 new_rhs.where().set(ID_component_name, member_expr.get_component_name());
92 dest_values, member_expr.compound(), new_rhs, ns, cp, is_assignment);
93 }
94 else if(lhs.id() == ID_symbol)
95 {
96 if(cp && !cp->should_track_value(lhs, ns))
97 return;
98
99 const symbol_exprt &s = to_symbol_expr(lhs);
100
101 exprt tmp = rhs;
102 partial_evaluate(dest_values, tmp, ns);
103
104 if(dest_values.is_constant(tmp))
105 {
107 ns.lookup(s).type == tmp.type(),
108 "type of constant to be replaced should match");
109 dest_values.set_to(s, tmp);
110 }
111 else
112 {
113 if(is_assignment)
114 dest_values.set_to_top(s);
115 }
116 }
117 else if(is_assignment)
118 {
119 // it's an assignment, but we don't really know what object is being written
120 // to: assume it may write to anything.
121 dest_values.set_to_top();
122 }
123}
124
126 const irep_idt &function_from,
127 trace_ptrt trace_from,
128 const irep_idt &function_to,
129 trace_ptrt trace_to,
130 ai_baset &ai,
131 const namespacet &ns)
132{
133 locationt from{trace_from->current_location()};
134 locationt to{trace_to->current_location()};
135
136#ifdef DEBUG
137 std::cout << "Transform from/to:\n";
138 std::cout << from->location_number << " --> "
139 << to->location_number << '\n';
140#endif
141
142#ifdef DEBUG
143 std::cout << "Before:\n";
144 output(std::cout, ai, ns);
145#endif
146
147 // When the domain is used with constant_propagator_ait,
148 // information about dirty variables and config flags are
149 // available. Otherwise, the below will be null and we use default
150 // values
151 const constant_propagator_ait *cp=
152 dynamic_cast<constant_propagator_ait *>(&ai);
153 bool have_dirty=(cp!=nullptr);
154
155 // Transform on a domain that is bottom is possible
156 // if a branch is impossible the target can still wind
157 // up on the work list.
158 if(values.is_bottom)
159 return;
160
161 if(from->is_decl())
162 {
163 const symbol_exprt &symbol = from->decl_symbol();
164 values.set_to_top(symbol);
165 }
166 else if(from->is_assign())
167 {
168 const exprt &lhs = from->assign_lhs();
169 const exprt &rhs = from->assign_rhs();
170 assign_rec(values, lhs, rhs, ns, cp, true);
171 }
172 else if(from->is_assume())
173 {
174 two_way_propagate_rec(from->get_condition(), ns, cp);
175 }
176 else if(from->is_goto())
177 {
178 exprt g;
179
180 // Comparing iterators is safe as the target must be within the same list
181 // of instructions because this is a GOTO.
182 if(from->get_target()==to)
183 g = from->get_condition();
184 else
185 g = not_exprt(from->get_condition());
186 partial_evaluate(values, g, ns);
187 if(g.is_false())
189 else
190 two_way_propagate_rec(g, ns, cp);
191 }
192 else if(from->is_dead())
193 {
194 values.set_to_top(from->dead_symbol());
195 }
196 else if(from->is_function_call())
197 {
198 const exprt &function = from->call_function();
199
200 if(function.id()==ID_symbol)
201 {
202 // called function identifier
203 const symbol_exprt &symbol_expr=to_symbol_expr(function);
204 const irep_idt id=symbol_expr.get_identifier();
205
206 // Functions with no body
207 if(function_from == function_to)
208 {
209 if(id==CPROVER_PREFIX "set_must" ||
210 id==CPROVER_PREFIX "get_must" ||
211 id==CPROVER_PREFIX "set_may" ||
212 id==CPROVER_PREFIX "get_may" ||
213 id==CPROVER_PREFIX "cleanup" ||
214 id==CPROVER_PREFIX "clear_may" ||
215 id==CPROVER_PREFIX "clear_must")
216 {
217 // no effect on constants
218 }
219 else
220 {
221 if(have_dirty)
223 else
225 }
226 }
227 else
228 {
229 // we have an actual call
230
231 // parameters of called function
232 const symbolt &symbol=ns.lookup(id);
233 const code_typet &code_type=to_code_type(symbol.type);
234 const code_typet::parameterst &parameters=code_type.parameters();
235
236 const code_function_callt::argumentst &arguments =
237 from->call_arguments();
238
239 code_typet::parameterst::const_iterator p_it=parameters.begin();
240 for(const auto &arg : arguments)
241 {
242 if(p_it==parameters.end())
243 break;
244
245 const symbol_exprt parameter_expr(p_it->get_identifier(), arg.type());
246 assign_rec(values, parameter_expr, arg, ns, cp, true);
247
248 ++p_it;
249 }
250 }
251 }
252 else
253 {
254 // unresolved call
255 INVARIANT(
256 function_from == function_to,
257 "Unresolved call can only be approximated if a skip");
258
259 if(have_dirty)
261 else
263 }
264 }
265 else if(from->is_end_function())
266 {
267 // erase parameters
268
269 const irep_idt id = function_from;
270 const symbolt &symbol=ns.lookup(id);
271
272 const code_typet &type=to_code_type(symbol.type);
273
274 for(const auto &param : type.parameters())
275 values.set_to_top(symbol_exprt(param.get_identifier(), param.type()));
276 }
277
278 INVARIANT(from->is_goto() || !values.is_bottom,
279 "Transform only sets bottom by using branch conditions");
280
281#ifdef DEBUG
282 std::cout << "After:\n";
283 output(std::cout, ai, ns);
284#endif
285}
286
287static void
289{
290 // (int)var xx 0 ==> var xx (_Bool)0 or similar (xx is == or !=)
291 // Note this is restricted to bools because in general turning a widening
292 // into a narrowing typecast is not correct.
293 if(lhs.id() != ID_typecast)
294 return;
295
296 const exprt &lhs_underlying = to_typecast_expr(lhs).op();
297 if(
298 lhs_underlying.type() == bool_typet() ||
299 lhs_underlying.type() == c_bool_type())
300 {
301 rhs = typecast_exprt(rhs, lhs_underlying.type());
302 simplify(rhs, ns);
303
304 lhs = lhs_underlying;
305 }
306}
307
310 const exprt &expr,
311 const namespacet &ns,
312 const constant_propagator_ait *cp)
313{
314#ifdef DEBUG
315 std::cout << "two_way_propagate_rec: " << format(expr) << '\n';
316#endif
317
318 bool change=false;
319
320 if(expr.id()==ID_and)
321 {
322 // need a fixed point here to get the most out of it
323 bool change_this_time;
324 do
325 {
326 change_this_time = false;
327
328 forall_operands(it, expr)
329 {
330 change_this_time |= two_way_propagate_rec(*it, ns, cp);
331 if(change_this_time)
332 change = true;
333 }
334 } while(change_this_time);
335 }
336 else if(expr.id() == ID_not)
337 {
338 const auto &op = to_not_expr(expr).op();
339
340 if(op.id() == ID_equal || op.id() == ID_notequal)
341 {
342 exprt subexpr = op;
343 subexpr.id(subexpr.id() == ID_equal ? ID_notequal : ID_equal);
344 change = two_way_propagate_rec(subexpr, ns, cp);
345 }
346 else if(op.id() == ID_symbol && expr.type() == bool_typet())
347 {
348 // Treat `IF !x` like `IF x == FALSE`:
349 change = two_way_propagate_rec(equal_exprt(op, false_exprt()), ns, cp);
350 }
351 }
352 else if(expr.id() == ID_symbol)
353 {
354 if(expr.type() == bool_typet())
355 {
356 // Treat `IF x` like `IF x == TRUE`:
357 change = two_way_propagate_rec(equal_exprt(expr, true_exprt()), ns, cp);
358 }
359 }
360 else if(expr.id() == ID_notequal)
361 {
362 // Treat "symbol != constant" like "symbol == !constant" when the constant
363 // is a boolean.
364 exprt lhs = to_notequal_expr(expr).lhs();
365 exprt rhs = to_notequal_expr(expr).rhs();
366
367 if(lhs.is_constant() && !rhs.is_constant())
368 std::swap(lhs, rhs);
369
370 if(lhs.is_constant() || !rhs.is_constant())
371 return false;
372
373 replace_typecast_of_bool(lhs, rhs, ns);
374
375 if(lhs.type() != bool_typet() && lhs.type() != c_bool_type())
376 return false;
377
378 // x != FALSE ==> x == TRUE
379
380 if(rhs.is_zero() || rhs.is_false())
381 rhs = from_integer(1, rhs.type());
382 else
383 rhs = from_integer(0, rhs.type());
384
385 change = two_way_propagate_rec(equal_exprt(lhs, rhs), ns, cp);
386 }
387 else if(expr.id() == ID_equal)
388 {
389 exprt lhs = to_equal_expr(expr).lhs();
390 exprt rhs = to_equal_expr(expr).rhs();
391
392 replace_typecast_of_bool(lhs, rhs, ns);
393
394 // two-way propagation
395 valuest copy_values=values;
396 assign_rec(copy_values, lhs, rhs, ns, cp, false);
397 if(!values.is_constant(rhs) || values.is_constant(lhs))
398 assign_rec(values, rhs, lhs, ns, cp, false);
399 change = values.meet(copy_values, ns);
400 }
401
402#ifdef DEBUG
403 std::cout << "two_way_propagate_rec: " << change << '\n';
404#endif
405
406 return change;
407}
408
414 exprt &condition,
415 const namespacet &ns) const
416{
417 return partial_evaluate(values, condition, ns);
418}
419
421{
422public:
426 {
427 }
428
429 bool is_constant(const irep_idt &id) const
430 {
432 }
433
434protected:
435 bool is_constant(const exprt &expr) const override
436 {
437 if(expr.id() == ID_symbol)
439
440 return is_constantt::is_constant(expr);
441 }
442
444};
445
447{
449}
450
452{
453 return constant_propagator_is_constantt(replace_const).is_constant(id);
454}
455
458 const symbol_exprt &symbol_expr)
459{
460 const auto n_erased = replace_const.erase(symbol_expr.get_identifier());
461
462 INVARIANT(n_erased==0 || !is_bottom, "bottom should have no elements at all");
463
464 return n_erased>0;
465}
466
467
469 const dirtyt &dirty,
470 const namespacet &ns)
471{
473 expr_mapt &expr_map = replace_const.get_expr_map();
474
475 for(expr_mapt::iterator it=expr_map.begin();
476 it!=expr_map.end();)
477 {
478 const irep_idt id=it->first;
479
480 const symbolt &symbol=ns.lookup(id);
481
482 if(
483 (symbol.is_static_lifetime || dirty(id)) &&
484 !symbol.type.get_bool(ID_C_constant))
485 {
486 it = replace_const.erase(it);
487 }
488 else
489 it++;
490 }
491}
492
494 std::ostream &out,
495 const namespacet &ns) const
496{
497 out << "const map:\n";
498
499 if(is_bottom)
500 {
501 out << " bottom\n";
503 "If the domain is bottom, the map must be empty");
504 return;
505 }
506
507 INVARIANT(!is_bottom, "Have handled bottom");
508 if(is_empty())
509 {
510 out << "top\n";
511 return;
512 }
513
514 for(const auto &p : replace_const.get_expr_map())
515 {
516 out << ' ' << p.first << "=" << from_expr(ns, p.first, p.second) << '\n';
517 }
518}
519
521 std::ostream &out,
522 const ai_baset &,
523 const namespacet &ns) const
524{
525 values.output(out, ns);
526}
527
531{
532 // nothing to do
533 if(src.is_bottom)
534 return false;
535
536 // just copy
537 if(is_bottom)
538 {
540 replace_const=src.replace_const; // copy
541 is_bottom=false;
542 return true;
543 }
544
545 INVARIANT(!is_bottom && !src.is_bottom, "Case handled");
546
547 bool changed=false;
548
549 // handle top
550 if(src.is_empty())
551 {
552 // change if it was not top
553 changed = !is_empty();
554
555 set_to_top();
556
557 return changed;
558 }
559
560 replace_symbolt::expr_mapt &expr_map = replace_const.get_expr_map();
561 const replace_symbolt::expr_mapt &src_expr_map =
563
564 // remove those that are
565 // - different in src
566 // - do not exist in src
567 for(replace_symbolt::expr_mapt::iterator it=expr_map.begin();
568 it!=expr_map.end();)
569 {
570 const irep_idt id=it->first;
571 const exprt &expr=it->second;
572
573 replace_symbolt::expr_mapt::const_iterator s_it;
574 s_it=src_expr_map.find(id);
575
576 if(s_it!=src_expr_map.end())
577 {
578 // check value
579 const exprt &src_expr=s_it->second;
580
581 if(expr!=src_expr)
582 {
583 it = replace_const.erase(it);
584 changed=true;
585 }
586 else
587 it++;
588 }
589 else
590 {
591 it = replace_const.erase(it);
592 changed=true;
593 }
594 }
595
596 return changed;
597}
598
602 const valuest &src,
603 const namespacet &ns)
604{
605 if(src.is_bottom || is_bottom)
606 return false;
607
608 bool changed=false;
609
610 for(const auto &m : src.replace_const.get_expr_map())
611 {
612 replace_symbolt::expr_mapt::const_iterator c_it =
613 replace_const.get_expr_map().find(m.first);
614
615 if(c_it != replace_const.get_expr_map().end())
616 {
617 if(c_it->second!=m.second)
618 {
619 set_to_bottom();
620 changed=true;
621 break;
622 }
623 }
624 else
625 {
626 const typet &m_id_type = ns.lookup(m.first).type;
628 m_id_type == m.second.type(),
629 "type of constant to be stored should match");
630 set_to(symbol_exprt(m.first, m_id_type), m.second);
631 changed=true;
632 }
633 }
634
635 return changed;
636}
637
640 const constant_propagator_domaint &other,
643{
644 return values.merge(other.values);
645}
646
654 const valuest &known_values,
655 exprt &expr,
656 const namespacet &ns)
657{
658 // if the current rounding mode is top we can
659 // still get a non-top result by trying all rounding
660 // modes and checking if the results are all the same
661 if(!known_values.is_constant(rounding_mode_identifier()))
662 return partial_evaluate_with_all_rounding_modes(known_values, expr, ns);
663
664 return replace_constants_and_simplify(known_values, expr, ns);
665}
666
675 const valuest &known_values,
676 exprt &expr,
677 const namespacet &ns)
678{ // NOLINTNEXTLINE (whitespace/braces)
679 auto rounding_modes = std::array<ieee_floatt::rounding_modet, 4>{
680 // NOLINTNEXTLINE (whitespace/braces)
684 // NOLINTNEXTLINE (whitespace/braces)
686 exprt first_result;
687 for(std::size_t i = 0; i < rounding_modes.size(); ++i)
688 {
689 valuest tmp_values = known_values;
690 tmp_values.set_to(
692 from_integer(rounding_modes[i], integer_typet()));
693 exprt result = expr;
694 if(replace_constants_and_simplify(tmp_values, result, ns))
695 {
696 return true;
697 }
698 else if(i == 0)
699 {
700 first_result = result;
701 }
702 else if(result != first_result)
703 {
704 return true;
705 }
706 }
707 expr = first_result;
708 return false;
709}
710
712 const valuest &known_values,
713 exprt &expr,
714 const namespacet &ns)
715{
716 bool did_not_change_anything = true;
717
718 // iterate constant propagation and simplification until we cannot
719 // constant-propagate any further - a prime example is pointer dereferencing,
720 // where constant propagation may have a value of the pointer, the simplifier
721 // takes care of evaluating dereferencing, and we might then have the value of
722 // the resulting symbol known to constant propagation and thus replace the
723 // dereferenced expression by a constant
724 while(!known_values.replace_const.replace(expr))
725 {
726 did_not_change_anything = false;
727 simplify(expr, ns);
728 }
729
730 // even if we haven't been able to constant-propagate anything, run the
731 // simplifier on the expression
732 if(did_not_change_anything)
733 did_not_change_anything &= simplify(expr, ns);
734
735 return did_not_change_anything;
736}
737
739 goto_functionst &goto_functions,
740 const namespacet &ns)
741{
742 for(auto &gf_entry : goto_functions.function_map)
743 replace(gf_entry.second, ns);
744}
745
746
748 goto_functionst::goto_functiont &goto_function,
749 const namespacet &ns)
750{
751 Forall_goto_program_instructions(it, goto_function.body)
752 {
753 auto const current_domain_ptr =
754 std::dynamic_pointer_cast<const constant_propagator_domaint>(
755 this->abstract_state_before(it));
756 const constant_propagator_domaint &d = *current_domain_ptr;
757
758 if(d.is_bottom())
759 continue;
760
761 replace_types_rec(d.values.replace_const, it->code_nonconst());
762
763 if(it->is_goto() || it->is_assume() || it->is_assert())
764 {
765 exprt c = it->get_condition();
766 replace_types_rec(d.values.replace_const, c);
768 it->set_condition(c);
769 }
770 else if(it->is_assign())
771 {
772 exprt &rhs = it->assign_rhs_nonconst();
773
775 {
776 if(rhs.id() == ID_constant)
777 rhs.add_source_location() = it->assign_lhs().source_location();
778 }
779 }
780 else if(it->is_function_call())
781 {
783 d.values, it->call_function(), ns);
784
785 for(auto &arg : it->call_arguments())
787 }
788 else if(it->is_other())
789 {
790 if(it->get_other().get_statement() == ID_expression)
791 {
792 auto c = to_code_expression(it->get_other());
794 d.values, c.expression(), ns))
795 {
796 it->set_other(c);
797 }
798 }
799 }
800 }
801}
802
804 const replace_symbolt &replace_const,
805 exprt &expr)
806{
807 replace_const(expr.type());
808
809 Forall_operands(it, expr)
810 replace_types_rec(replace_const, *it);
811}
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Symbolic Execution.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
typet c_bool_type()
Definition: c_types.cpp:118
bool replace(exprt &dest) const override
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:74
goto_programt::const_targett locationt
Definition: ai_domain.h:73
exprt & lhs()
Definition: std_expr.h:580
exprt & rhs()
Definition: std_expr.h:590
The Boolean type.
Definition: std_types.h:36
exprt::operandst argumentst
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:542
const parameterst & parameters() const
Definition: std_types.h:655
void replace_types_rec(const replace_symbolt &replace_const, exprt &expr)
should_track_valuet should_track_value
void replace(goto_functionst::goto_functiont &, const namespacet &)
static void assign_rec(valuest &dest_values, const exprt &lhs, const exprt &rhs, const namespacet &ns, const constant_propagator_ait *cp, bool is_assignment)
Assign value rhs to lhs, recording any newly-known constants in dest_values.
virtual bool is_bottom() const final override
static bool partial_evaluate(const valuest &known_values, exprt &expr, const namespacet &ns)
Attempt to evaluate expression using domain knowledge This function changes the expression that is pa...
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const final override
Simplify the condition given context-sensitive knowledge from the abstract state.
static bool partial_evaluate_with_all_rounding_modes(const valuest &known_values, exprt &expr, const namespacet &ns)
Attempt to evaluate an expression in all rounding modes.
virtual void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai_base, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
static bool replace_constants_and_simplify(const valuest &known_values, exprt &expr, const namespacet &ns)
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns, const constant_propagator_ait *cp)
handles equalities and conjunctions containing equalities
virtual void output(std::ostream &out, const ai_baset &ai_base, const namespacet &ns) const override
bool merge(const constant_propagator_domaint &other, trace_ptrt from, trace_ptrt to)
constant_propagator_is_constantt(const replace_symbolt &replace_const)
bool is_constant(const irep_idt &id) const
bool is_constant(const exprt &expr) const override
This function determines what expressions are to be propagated as "constants".
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Definition: dirty.h:27
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
source_locationt & add_source_location()
Definition: expr.h:235
The Boolean constant false.
Definition: std_expr.h:2865
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
@ ROUND_TO_PLUS_INF
Definition: ieee_float.h:126
@ ROUND_TO_MINUS_INF
Definition: ieee_float.h:125
Array index operator.
Definition: std_expr.h:1328
exprt & index()
Definition: std_expr.h:1363
exprt & array()
Definition: std_expr.h:1353
Unbounded, signed integers (mathematical integers, not bitvectors)
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
const irep_idt & id() const
Definition: irep.h:396
Determine whether an expression is constant.
Definition: expr_util.h:89
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Definition: expr_util.cpp:226
Extract member of struct or union.
Definition: std_expr.h:2667
const exprt & compound() const
Definition: std_expr.h:2708
irep_idt get_component_name() const
Definition: std_expr.h:2681
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
Boolean negation.
Definition: std_expr.h:2181
Replace expression or type symbols by an expression or type, respectively.
const expr_mapt & get_expr_map() const
std::unordered_map< irep_idt, exprt > expr_mapt
bool replaces_symbol(const irep_idt &id) const
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
bool is_static_lifetime
Definition: symbol.h:65
typet type
Type of symbol.
Definition: symbol.h:31
The Boolean constant true.
Definition: std_expr.h:2856
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:293
Operator to update elements in structs and arrays.
Definition: std_expr.h:2312
exprt & where()
Definition: std_expr.h:2332
static void replace_typecast_of_bool(exprt &lhs, exprt &rhs, const namespacet &ns)
Constant propagation.
#define CPROVER_PREFIX
bool is_empty(const std::string &s)
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
Deprecated expression utility functions.
static format_containert< T > format(const T &o)
Definition: format.h:37
#define Forall_goto_program_instructions(it, program)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Mathematical types.
bool simplify(exprt &expr, const namespacet &ns)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#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(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1428
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1308
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2206
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
bool is_constant(const exprt &expr) const
bool meet(const valuest &src, const namespacet &ns)
meet
void output(std::ostream &out, const namespacet &ns) const
void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns)
address_of_aware_replace_symbolt replace_const
void set_to(const symbol_exprt &lhs, const exprt &rhs)