26 std::string a, idx, identifier;
29 if (index.
id()==ID_typecast)
45 std::string a, identifier;
62 std::cout <<
"assign: " <<
from_expr(ns,
"", lhs)
63 <<
" := " <<
from_type(ns,
"", rhs_type) <<
'\n';
66 if(lhs.
id()==ID_symbol && rhs.
id()==ID_if)
73 if(cond.
op0().
id()==ID_index)
87 else if(lhs.
id()==ID_symbol && rhs_type.
id()!=ID_array
88 && rhs_type.
id()!=ID_struct
89 && rhs_type.
id()!=ID_union)
96 else if(lhs.
id()==ID_symbol && lhs_type.
id()==ID_array
97 && rhs_type.
id()==ID_array)
108 else if (lhs.
id()==ID_index)
131 std::cout << from->location_number <<
" --> " 132 << to->location_number <<
'\n';
136 std::cout <<
"before:\n";
137 output(std::cout, ai, ns);
146 else if(from->is_assign())
149 const exprt &lhs = assignment.
lhs();
150 const exprt &rhs = assignment.
rhs();
153 else if(from->is_assume())
157 else if(from->is_goto())
161 if(from->get_target()==to)
177 else if(from->is_dead())
182 else if(from->is_function_call())
186 if(
function.
id()==ID_symbol)
190 if(identifier==
"__CPROVER_set_must" ||
191 identifier==
"__CPROVER_get_must" ||
192 identifier==
"__CPROVER_set_may" ||
193 identifier==
"__CPROVER_get_may" ||
194 identifier==
"__CPROVER_cleanup" ||
195 identifier==
"__CPROVER_clear_may" ||
196 identifier==
"__CPROVER_clear_must")
207 std::cout <<
"after:\n";
208 output(std::cout, ai, ns);
219 std::cout <<
"two_way_propagate_rec: " <<
from_expr(ns,
"", expr) <<
'\n';
223 if(expr.
id()==ID_and)
236 else if(expr.
id()==ID_equal)
250 std::cout <<
"two_way_propagate_rec: " << change <<
'\n';
294 if(expr.
id()==ID_side_effect &&
298 if(expr.
id()==ID_side_effect &&
302 if(expr.
id()==ID_symbol)
303 if(replace_const.expr_map.find(
to_symbol_expr(expr).get_identifier()) ==
304 replace_const.expr_map.end())
307 if (expr.
id()==ID_index)
308 return is_array_constant(expr);
310 if(expr.
id()==ID_address_of)
314 if(!is_constant(*it))
321 const exprt &expr)
const 323 if(expr.
id()==ID_index)
327 if(expr.
id()==ID_member)
330 if(expr.
id()==ID_dereference)
333 if(expr.
id()==ID_string_constant)
344 replace_symbolt::expr_mapt::iterator r_it =
345 replace_const.expr_map.find(
id);
347 if(r_it != replace_const.expr_map.end())
350 replace_const.expr_map.erase(r_it);
361 out <<
"const map:\n";
366 for(
const auto &replace_pair : replace_const.expr_map)
367 out <<
' ' << replace_pair.first <<
"=" 368 <<
from_expr(ns,
"", replace_pair.second) <<
'\n';
395 bool changed =
false;
398 for(replace_symbolt::expr_mapt::const_iterator
399 it=replace_const.expr_map.begin();
400 it!=replace_const.expr_map.end();
403 const replace_symbolt::expr_mapt::const_iterator
409 replace_const.expr_map.erase(it);
415 const exprt previous=it->second;
416 replace_const.expr_map[b_it->first]=b_it->second;
417 if (it->second != previous) changed =
true;
432 bool changed =
false;
436 replace_symbolt::expr_mapt::iterator c_it=
437 replace_const.expr_map.find(src_replace_pair.first);
439 if(c_it!=replace_const.expr_map.end())
441 if(c_it->second!=src_replace_pair.second)
450 set_to(src_replace_pair.first, src_replace_pair.second);
472 replace(f_it->second, ns);
477 if (expr.
id()==ID_index)
483 if (it->id()==ID_equal)
484 replace_array_symbol(it->op0());
485 else if (it->id()==ID_index)
486 replace_array_symbol(expr.
op0());
497 state_mapt::iterator s_it = state_map.find(it);
499 if(s_it == state_map.end())
502 replace_types_rec(s_it->second.values.replace_const, it->code);
503 replace_types_rec(s_it->second.values.replace_const, it->guard);
505 if(it->is_goto() || it->is_assume() || it->is_assert())
507 replace_array_symbol(it->guard);
508 s_it->second.values.replace_const(it->guard);
511 else if(it->is_assign())
514 s_it->second.values.replace_const(rhs);
516 if (rhs.
id()==ID_constant)
519 else if(it->is_function_call())
521 s_it->second.values.replace_const(
528 for(exprt::operandst::iterator o_it = args.begin();
529 o_it != args.end(); ++o_it)
531 s_it->second.values.replace_const(*o_it);
535 else if(it->is_other())
537 if(it->code.get_statement()==ID_expression)
538 s_it->second.values.replace_const(it->code);
547 replace_const(expr.
type());
550 replace_types_rec(replace_const, *it);
The type of an expression.
const typet & follow(const typet &src) const
const code_declt & to_code_decl(const codet &code)
void assign(valuest &dest, const symbol_exprt &lhs, exprt rhs, const namespacet &ns) const
bool is_array_constant(const exprt &expr) const
const mp_integer string2integer(const std::string &n, unsigned base)
const std::string integer2string(const mp_integer &n, unsigned base)
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const override
Simplify the condition given context-sensitive knowledge from the abstract state. ...
bool is_constant_address_of(const exprt &expr) const
exprt simplify_expr(const exprt &src, const namespacet &ns)
const code_deadt & to_code_dead(const codet &code)
void replace_types_rec(const replace_symbolt &replace_const, exprt &expr)
void transform(locationt, locationt, ai_baset &, const namespacet &) final
virtual bool replace(exprt &dest) const
does not replace object in address_of expressions
const irep_idt & get_identifier() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
bool meet(const valuest &src)
meet
bool merge(const valuest &src)
join
side_effect_exprt & to_side_effect_expr(exprt &expr)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
bool is_constant(const exprt &expr) const
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
A declaration of a local variable.
#define forall_operands(it, expr)
goto_function_templatet< goto_programt > goto_functiont
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
std::vector< exprt > operandst
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns)
handles equalities and conjunctions containing equalities
bool set_to_top(const irep_idt &id)
Do not call this when iterating over replace_const.expr_map!
Base class for all expressions.
const exprt & struct_op() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
void output(std::ostream &, const namespacet &) const
#define Forall_goto_functions(it, functions)
void set_to(const irep_idt &lhs_id, const exprt &rhs_val)
const std::string & get_string(const irep_namet &name) const
A removal of a local variable.
#define Forall_operands(it, expr)
source_locationt & add_source_location()
#define Forall_goto_program_instructions(it, program)
goto_programt::const_targett locationt
Expression to hold a symbol (variable)
exprt concatenate_array_id(const exprt &array, const exprt &index, const typet &type)
bool merge(const constant_propagator_domaint &, locationt, locationt)
void replace_array_symbol(exprt &expr)
void replace(goto_functionst::goto_functiont &, const namespacet &)
void assign_rec(valuest &values, const exprt &lhs, const exprt &rhs, const namespacet &ns)
void output(std::ostream &, const ai_baset &, const namespacet &) const final
const irep_idt & get_statement() const
const code_function_callt & to_code_function_call(const codet &code)
bool simplify(exprt &expr, const namespacet &ns)
replace_symbol_extt replace_const