36 if(lhs.
id()!=ID_symbol)
57 std::cout <<
"Transform from/to:\n";
58 std::cout << from->location_number <<
" --> " 59 << to->location_number <<
'\n';
63 std::cout <<
"Before:\n";
73 bool have_dirty=(cp!=
nullptr);
87 else if(from->is_assign())
94 else if(from->is_assume())
98 else if(from->is_goto())
104 if(from->get_target()==to)
119 "Without two-way propagation this should be impossible.");
122 else if(from->is_dead())
127 else if(from->is_function_call())
132 if(
function.
id()==ID_symbol)
139 if(from->function == to->function)
171 code_typet::parameterst::const_iterator p_it=parameters.begin();
172 for(
const auto &arg : arguments)
174 if(p_it==parameters.end())
177 const symbol_exprt parameter_expr(p_it->get_identifier(), arg.type());
188 from->function == to->function,
189 "Unresolved call can only be approximated if a skip");
197 else if(from->is_end_function())
211 "Transform only sets bottom by using branch conditions");
214 std::cout <<
"After:\n";
215 output(std::cout, ai, ns);
226 std::cout <<
"two_way_propagate_rec: " <<
format(expr) <<
'\n';
233 if(expr.
id()==ID_and)
246 else if(expr.
id()==ID_equal)
261 std::cout <<
"two_way_propagate_rec: " << change <<
'\n';
281 if(expr.
id()==ID_side_effect &&
285 if(expr.
id()==ID_side_effect &&
289 if(expr.
id()==ID_symbol)
294 if(expr.
id()==ID_index)
297 if(expr.
id()==ID_address_of)
308 const exprt &expr)
const 310 if(expr.
id()==ID_index)
314 if(expr.
id()==ID_member)
317 if(expr.
id()==ID_dereference)
320 if(expr.
id()==ID_string_constant)
330 replace_const.expr_map.erase(
id);
343 expr_mapt &expr_map=replace_const.expr_map;
345 for(expr_mapt::iterator it=expr_map.begin();
354 it=expr_map.erase(it);
364 out <<
"const map:\n";
370 "If the domain is bottom, the map must be empty");
375 if(replace_const.expr_map.empty())
381 for(
const auto &p : replace_const.expr_map)
383 out <<
' ' << p.first <<
"=" <<
from_expr(ns, p.first, p.second) <<
'\n';
420 if(src_expr_map.empty())
423 changed=!expr_map.empty();
433 for(replace_symbolt::expr_mapt::iterator it=expr_map.begin();
437 const exprt &expr=it->second;
439 replace_symbolt::expr_mapt::const_iterator s_it;
440 s_it=src_expr_map.
find(
id);
442 if(s_it!=src_expr_map.end())
445 const exprt &src_expr=s_it->second;
449 it=expr_map.erase(it);
457 it=expr_map.erase(it);
476 replace_symbolt::expr_mapt::iterator
477 c_it=replace_const.expr_map.find(m.first);
479 if(c_it!=replace_const.expr_map.end())
481 if(c_it->second!=m.second)
490 set_to(m.first, m.second);
534 auto rounding_modes = std::array<ieee_floatt::rounding_modet, 4>{
542 for(std::size_t i = 0; i < rounding_modes.size(); ++i)
555 first_result = result;
557 else if(result != first_result)
571 did_not_change_anything &=
simplify(expr, ns);
572 return did_not_change_anything;
580 replace(f_it->second, ns);
590 state_mapt::iterator s_it=state_map.find(it);
592 if(s_it==state_map.end())
595 replace_types_rec(s_it->second.values.replace_const, it->code);
596 replace_types_rec(s_it->second.values.replace_const, it->guard);
598 if(it->is_goto() || it->is_assume() || it->is_assert())
600 s_it->second.partial_evaluate(it->guard, ns);
602 else if(it->is_assign())
605 s_it->second.partial_evaluate(rhs, ns);
606 if(rhs.
id()==ID_constant)
609 else if(it->is_function_call())
612 s_it->second.partial_evaluate(
function, ns);
617 for(
auto &arg : args)
619 s_it->second.partial_evaluate(arg, ns);
622 else if(it->is_other())
624 if(it->code.get_statement()==ID_expression)
626 s_it->second.partial_evaluate(it->code, ns);
636 replace_const(expr.
type());
639 replace_types_rec(replace_const, *it);
const code_declt & to_code_decl(const codet &code)
virtual void transform(locationt from, locationt to, ai_baset &ai_base, const namespacet &ns) final override
bool is_constant_address_of(const exprt &expr) const
const code_deadt & to_code_dead(const codet &code)
bool replace_constants_and_simplify(exprt &expr, const namespacet &ns) const
void replace_types_rec(const replace_symbolt &replace_const, exprt &expr)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
const irep_idt & get_identifier() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< parametert > parameterst
exprt::operandst argumentst
unsignedbv_typet size_type()
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
bool meet(const valuest &src)
meet
bool get_bool(const irep_namet &name) const
bool merge(const valuest &src)
join
#define INVARIANT(CONDITION, REASON)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
side_effect_exprt & to_side_effect_expr(exprt &expr)
bool is_constant(const exprt &expr) const
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
A declaration of a local variable.
bool partial_evaluate(exprt &expr, const namespacet &ns) const
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. ...
::goto_functiont goto_functiont
#define PRECONDITION(CONDITION)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
replace_symbolt replace_const
std::vector< exprt > operandst
std::unordered_map< irep_idt, exprt > expr_mapt
virtual bool is_bottom() const final override
bool partial_evaluate_with_all_rounding_modes(exprt &expr, const namespacet &ns) const
Attempt to evaluate an expression in all rounding modes.
Unbounded, signed integers.
virtual void output(std::ostream &out, const ai_baset &ai_base, const namespacet &ns) const override
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns)
handles equalities and conjunctions containing equalities
typet type
Type of symbol.
void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns)
virtual bool replace(exprt &dest, const bool replace_with_const=true) const
Replaces a symbol with a constant If you are replacing symbols with constants in an l-value...
const char ID_cprover_rounding_mode_str[]
Base class for all expressions.
const exprt & struct_op() const
const parameterst & parameters() const
#define Forall_goto_functions(it, functions)
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
bool is_procedure_local() const
Expression to hold a symbol (variable)
void set_to(const irep_idt &lhs, const exprt &rhs)
#define DATA_INVARIANT(CONDITION, REASON)
void replace(goto_functionst::goto_functiont &, const namespacet &)
void assign_rec(valuest &values, const exprt &lhs, const exprt &rhs, const namespacet &ns)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
const irept & find(const irep_namet &name) const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void output(std::ostream &out, const namespacet &ns) const
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
const irep_idt & get_statement() const
const code_function_callt & to_code_function_call(const codet &code)
bool simplify(exprt &expr, const namespacet &ns)
bool merge(const constant_propagator_domaint &other, locationt from, locationt to)