38 if(lhs.
id()!=ID_symbol)
53 "type of constant to be replaced should match");
69 std::cout <<
"Transform from/to:\n";
70 std::cout << from->location_number <<
" --> " 71 << to->location_number <<
'\n';
75 std::cout <<
"Before:\n";
84 dynamic_cast<constant_propagator_ait *>(&ai);
85 bool have_dirty=(cp!=
nullptr);
99 else if(from->is_assign())
106 else if(from->is_assume())
110 else if(from->is_goto())
116 if(from->get_target()==to)
131 "Without two-way propagation this should be impossible.");
134 else if(from->is_dead())
139 else if(from->is_function_call())
144 if(
function.
id()==ID_symbol)
151 if(function_from == function_to)
183 code_typet::parameterst::const_iterator p_it=parameters.begin();
184 for(
const auto &arg : arguments)
186 if(p_it==parameters.end())
189 const symbol_exprt parameter_expr(p_it->get_identifier(), arg.type());
200 function_from == function_to,
201 "Unresolved call can only be approximated if a skip");
209 else if(from->is_end_function())
223 "Transform only sets bottom by using branch conditions");
226 std::cout <<
"After:\n";
227 output(std::cout, ai, ns);
239 std::cout <<
"two_way_propagate_rec: " <<
format(expr) <<
'\n';
248 if(expr.
id()==ID_and)
261 else if(expr.
id()==ID_equal)
278 std::cout <<
"two_way_propagate_rec: " << change <<
'\n';
298 if(expr.
id()==ID_side_effect &&
302 if(expr.
id()==ID_side_effect &&
306 if(expr.
id()==ID_symbol)
310 if(expr.
id()==ID_index)
313 if(expr.
id()==ID_address_of)
324 const exprt &expr)
const 326 if(expr.
id()==ID_index)
330 if(expr.
id()==ID_member)
333 if(expr.
id()==ID_dereference)
336 if(expr.
id()==ID_string_constant)
346 const auto n_erased = replace_const.erase(symbol_expr.
get_identifier());
359 expr_mapt &expr_map = replace_const.get_expr_map();
361 for(expr_mapt::iterator it=expr_map.begin();
371 it = replace_const.erase(it);
382 out <<
"const map:\n";
388 "If the domain is bottom, the map must be empty");
399 for(
const auto &p : replace_const.get_expr_map())
401 out <<
' ' << p.first <<
"=" <<
from_expr(ns, p.first, p.second) <<
'\n';
452 for(replace_symbolt::expr_mapt::iterator it=expr_map.begin();
456 const exprt &expr=it->second;
458 replace_symbolt::expr_mapt::const_iterator s_it;
459 s_it=src_expr_map.
find(
id);
461 if(s_it!=src_expr_map.end())
464 const exprt &src_expr=s_it->second;
468 it = replace_const.erase(it);
476 it = replace_const.erase(it);
497 replace_symbolt::expr_mapt::const_iterator c_it =
498 replace_const.get_expr_map().find(m.first);
500 if(c_it != replace_const.get_expr_map().end())
502 if(c_it->second!=m.second)
514 "type of constant to be stored should match");
559 auto rounding_modes = std::array<ieee_floatt::rounding_modet, 4>{
567 for(std::size_t i = 0; i < rounding_modes.size(); ++i)
580 first_result = result;
582 else if(result != first_result)
596 did_not_change_anything &=
simplify(expr, ns);
597 return did_not_change_anything;
624 if(it->is_goto() || it->is_assume() || it->is_assert())
628 else if(it->is_assign())
633 if(rhs.
id()==ID_constant)
637 else if(it->is_function_call())
645 for(
auto &arg : args)
650 else if(it->is_other())
652 if(it->code.get_statement()==ID_expression)
664 replace_const(expr.
type());
667 replace_types_rec(replace_const, *it);
The type of an expression, extends irept.
const code_declt & to_code_decl(const codet &code)
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)
Check types for equality across all levels of hierarchy.
const code_typet & to_code_type(const typet &type)
Cast a 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)
void set_to(const symbol_exprt &lhs, const exprt &rhs)
bool is_false() const
Return whether the expression is a constant representing false.
std::vector< parametert > parameterst
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
typet & type()
Return the type of the expression.
exprt::operandst argumentst
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
bool get_bool(const irep_namet &name) const
bool merge(const valuest &src)
join
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an 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
Replace expression or type symbols by an expression or type, respectively.
A codet representing the 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.
virtual void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, 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...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
::goto_functiont goto_functiont
#define PRECONDITION(CONDITION)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
codet representation of a function call statement.
#define forall_operands(it, expr)
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns, const constant_propagator_ait *cp)
handles equalities and conjunctions containing equalities
bool is_constant() const
Return whether the expression is a constant.
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 (mathematical integers, not bitvectors)
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)
address_of_aware_replace_symbolt replace_const
bool replaces_symbol(const irep_idt &id) const
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)
const source_locationt & source_location() const
bool is_empty(const std::string &s)
A codet representing the removal of a local variable going out of scope.
#define Forall_operands(it, expr)
source_locationt & add_source_location()
#define Forall_goto_program_instructions(it, program)
const expr_mapt & get_expr_map() const
goto_programt::const_targett locationt
bool is_procedure_local() const
Expression to hold a symbol (variable)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
void replace(goto_functionst::goto_functiont &, const namespacet &)
bool replace(exprt &dest) const override
const index_exprt & to_index_expr(const exprt &expr)
Cast an 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 documentation for namespace_baset::lookup().
A codet representing an assignment in the program.
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)