38 if(lhs.
id()!=ID_symbol)
53 "type of constant to be replaced should match");
67 std::cout <<
"Transform from/to:\n";
68 std::cout << from->location_number <<
" --> " 69 << to->location_number <<
'\n';
73 std::cout <<
"Before:\n";
83 bool have_dirty=(cp!=
nullptr);
97 else if(from->is_assign())
104 else if(from->is_assume())
108 else if(from->is_goto())
114 if(from->get_target()==to)
129 "Without two-way propagation this should be impossible.");
132 else if(from->is_dead())
137 else if(from->is_function_call())
142 if(
function.
id()==ID_symbol)
149 if(from->function == to->function)
181 code_typet::parameterst::const_iterator p_it=parameters.begin();
182 for(
const auto &arg : arguments)
184 if(p_it==parameters.end())
187 const symbol_exprt parameter_expr(p_it->get_identifier(), arg.type());
198 from->function == to->function,
199 "Unresolved call can only be approximated if a skip");
207 else if(from->is_end_function())
221 "Transform only sets bottom by using branch conditions");
224 std::cout <<
"After:\n";
225 output(std::cout, ai, ns);
237 std::cout <<
"two_way_propagate_rec: " <<
format(expr) <<
'\n';
244 if(expr.
id()==ID_and)
257 else if(expr.
id()==ID_equal)
272 std::cout <<
"two_way_propagate_rec: " << change <<
'\n';
292 if(expr.
id()==ID_side_effect &&
296 if(expr.
id()==ID_side_effect &&
300 if(expr.
id()==ID_symbol)
305 if(expr.
id()==ID_index)
308 if(expr.
id()==ID_address_of)
319 const exprt &expr)
const 321 if(expr.
id()==ID_index)
325 if(expr.
id()==ID_member)
328 if(expr.
id()==ID_dereference)
331 if(expr.
id()==ID_string_constant)
341 replace_const.expr_map.erase(
id);
354 expr_mapt &expr_map=replace_const.expr_map;
356 for(expr_mapt::iterator it=expr_map.begin();
365 it=expr_map.erase(it);
375 out <<
"const map:\n";
381 "If the domain is bottom, the map must be empty");
386 if(replace_const.expr_map.empty())
392 for(
const auto &p : replace_const.expr_map)
394 out <<
' ' << p.first <<
"=" <<
from_expr(ns, p.first, p.second) <<
'\n';
431 if(src_expr_map.empty())
434 changed=!expr_map.empty();
444 for(replace_symbolt::expr_mapt::iterator it=expr_map.begin();
448 const exprt &expr=it->second;
450 replace_symbolt::expr_mapt::const_iterator s_it;
451 s_it=src_expr_map.
find(
id);
453 if(s_it!=src_expr_map.end())
456 const exprt &src_expr=s_it->second;
460 it=expr_map.erase(it);
468 it=expr_map.erase(it);
489 replace_symbolt::expr_mapt::iterator
490 c_it=replace_const.expr_map.find(m.first);
492 if(c_it!=replace_const.expr_map.end())
494 if(c_it->second!=m.second)
505 "type of constant to be stored should match");
506 set_to(m.first, m.second);
550 auto rounding_modes = std::array<ieee_floatt::rounding_modet, 4>{
558 for(std::size_t i = 0; i < rounding_modes.size(); ++i)
571 first_result = result;
573 else if(result != first_result)
587 did_not_change_anything &=
simplify(expr, ns);
588 return did_not_change_anything;
596 replace(f_it->second, ns);
615 if(it->is_goto() || it->is_assume() || it->is_assert())
619 else if(it->is_assign())
624 if(rhs.
id()==ID_constant)
627 else if(it->is_function_call())
635 for(
auto &arg : args)
640 else if(it->is_other())
642 if(it->code.get_statement()==ID_expression)
654 replace_const(expr.
type());
657 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
how function calls are treated: a) there is an edge from each call site to the function head b) there...
void assign_rec(valuest &values, const exprt &lhs, const exprt &rhs, const namespacet &ns, const constant_propagator_ait *cp)
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)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
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 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...
should_track_valuet should_track_value
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
replace_symbolt replace_const
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns, const constant_propagator_ait *cp)
handles equalities and conjunctions containing equalities
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
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[]
The basic interface of an abstract interpreter.
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 &)
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
bool meet(const valuest &src, const namespacet &ns)
meet
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)