Go to the documentation of this file.
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";
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)
327 return is_constant_address_of(
to_index_expr(expr).array()) &&
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);
#define Forall_goto_program_instructions(it, program)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const char ID_cprover_rounding_mode_str[]
#define PRECONDITION(CONDITION)
address_of_aware_replace_symbolt replace_const
bool replaces_symbol(const irep_idt &id) const
bool is_constant_address_of(const exprt &expr) const
#define Forall_operands(it, expr)
should_track_valuet should_track_value
bool is_constant(const exprt &expr) const
const code_declt & to_code_decl(const codet &code)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns, const constant_propagator_ait *cp)
handles equalities and conjunctions containing equalities
The type of an expression, extends irept.
std::vector< parametert > parameterst
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
typet type
Type of symbol.
void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns)
std::unordered_map< irep_idt, exprt > expr_mapt
const expr_mapt & get_expr_map() const
const irept & find(const irep_namet &name) const
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
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...
Unbounded, signed integers (mathematical integers, not bitvectors)
Base class for all expressions.
virtual void output(std::ostream &out, const ai_baset &ai_base, const namespacet &ns) const override
side_effect_exprt & to_side_effect_expr(exprt &expr)
Expression to hold a symbol (variable)
bool is_false() const
Return whether the expression is a constant representing false.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
bool get_bool(const irep_namet &name) const
bool is_empty(const std::string &s)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
void assign_rec(valuest &values, const exprt &lhs, const exprt &rhs, const namespacet &ns, const constant_propagator_ait *cp)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
#define forall_operands(it, expr)
bool merge(const constant_propagator_domaint &other, locationt from, locationt to)
bool replace_constants_and_simplify(exprt &expr, const namespacet &ns) const
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
void output(std::ostream &out, const namespacet &ns) const
const code_deadt & to_code_dead(const codet &code)
const irep_idt & get_identifier() const
bool replace(exprt &dest) const override
bool simplify(exprt &expr, const namespacet &ns)
bool is_procedure_local() const
bool merge(const valuest &src)
join
virtual bool is_bottom() const final override
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
std::vector< exprt > operandst
exprt::operandst argumentst
A codet representing the removal of a local variable going out of scope.
const parameterst & parameters() const
void replace_types_rec(const replace_symbolt &replace_const, exprt &expr)
#define Forall_goto_functions(it, functions)
bool partial_evaluate_with_all_rounding_modes(exprt &expr, const namespacet &ns) const
Attempt to evaluate an expression in all rounding modes.
::goto_functiont goto_functiont
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 collection of goto functions.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
goto_programt::const_targett locationt
const code_assignt & to_code_assign(const codet &code)
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const final override
Simplify the condition given context-sensitive knowledge from the abstract state.
bool is_constant() const
Return whether the expression is a constant.
void set_to(const symbol_exprt &lhs, const exprt &rhs)
The basic interface of an abstract interpreter.
bool meet(const valuest &src, const namespacet &ns)
meet
void replace(goto_functionst::goto_functiont &, const namespacet &)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
source_locationt & add_source_location()
A codet representing an assignment in the program.
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
const source_locationt & source_location() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Replace expression or type symbols by an expression or type, respectively.