61 if(lhs.
id() == ID_dereference)
68 const bool have_dirty = (cp !=
nullptr);
78 assign_rec(dest_values, eval_lhs, rhs, ns, cp, is_assignment);
80 else if(lhs.
id() == ID_index)
84 assign_rec(dest_values, index_expr.
array(), new_rhs, ns, cp, is_assignment);
86 else if(lhs.
id() == ID_member)
92 dest_values, member_expr.
compound(), new_rhs, ns, cp, is_assignment);
94 else if(lhs.
id() == ID_symbol)
108 "type of constant to be replaced should match");
109 dest_values.
set_to(s, tmp);
117 else if(is_assignment)
133 locationt from{trace_from->current_location()};
134 locationt to{trace_to->current_location()};
137 std::cout <<
"Transform from/to:\n";
138 std::cout << from->location_number <<
" --> "
139 << to->location_number <<
'\n';
143 std::cout <<
"Before:\n";
144 output(std::cout, ai, ns);
153 bool have_dirty=(cp!=
nullptr);
166 else if(from->is_assign())
168 const exprt &lhs = from->assign_lhs();
169 const exprt &rhs = from->assign_rhs();
172 else if(from->is_assume())
176 else if(from->is_goto())
182 if(from->get_target()==to)
183 g = from->get_condition();
192 else if(from->is_dead())
196 else if(from->is_function_call())
198 const exprt &
function = from->call_function();
200 if(
function.
id()==ID_symbol)
207 if(function_from == function_to)
237 from->call_arguments();
239 code_typet::parameterst::const_iterator p_it=parameters.begin();
240 for(
const auto &arg : arguments)
242 if(p_it==parameters.end())
245 const symbol_exprt parameter_expr(p_it->get_identifier(), arg.type());
256 function_from == function_to,
257 "Unresolved call can only be approximated if a skip");
265 else if(from->is_end_function())
279 "Transform only sets bottom by using branch conditions");
282 std::cout <<
"After:\n";
283 output(std::cout, ai, ns);
293 if(lhs.
id() != ID_typecast)
304 lhs = lhs_underlying;
315 std::cout <<
"two_way_propagate_rec: " <<
format(expr) <<
'\n';
320 if(expr.
id()==ID_and)
323 bool change_this_time;
326 change_this_time =
false;
334 }
while(change_this_time);
336 else if(expr.
id() == ID_not)
340 if(op.id() == ID_equal || op.id() == ID_notequal)
343 subexpr.
id(subexpr.
id() == ID_equal ? ID_notequal : ID_equal);
352 else if(expr.
id() == ID_symbol)
360 else if(expr.
id() == ID_notequal)
387 else if(expr.
id() == ID_equal)
396 assign_rec(copy_values, lhs, rhs, ns, cp,
false);
403 std::cout <<
"two_way_propagate_rec: " << change <<
'\n';
437 if(expr.
id() == ID_symbol)
460 const auto n_erased = replace_const.erase(symbol_expr.
get_identifier());
473 expr_mapt &expr_map = replace_const.get_expr_map();
475 for(expr_mapt::iterator it=expr_map.begin();
486 it = replace_const.erase(it);
497 out <<
"const map:\n";
503 "If the domain is bottom, the map must be empty");
514 for(
const auto &p : replace_const.get_expr_map())
516 out <<
' ' << p.first <<
"=" <<
from_expr(ns, p.first, p.second) <<
'\n';
567 for(replace_symbolt::expr_mapt::iterator it=expr_map.begin();
571 const exprt &expr=it->second;
573 replace_symbolt::expr_mapt::const_iterator s_it;
574 s_it=src_expr_map.
find(
id);
576 if(s_it!=src_expr_map.end())
579 const exprt &src_expr=s_it->second;
583 it = replace_const.erase(it);
591 it = replace_const.erase(it);
612 replace_symbolt::expr_mapt::const_iterator c_it =
613 replace_const.get_expr_map().find(m.first);
615 if(c_it != replace_const.get_expr_map().end())
617 if(c_it->second!=m.second)
628 m_id_type == m.second.type(),
629 "type of constant to be stored should match");
679 auto rounding_modes = std::array<ieee_floatt::rounding_modet, 4>{
687 for(std::size_t i = 0; i < rounding_modes.size(); ++i)
689 valuest tmp_values = known_values;
700 first_result = result;
702 else if(result != first_result)
716 bool did_not_change_anything =
true;
726 did_not_change_anything =
false;
732 if(did_not_change_anything)
733 did_not_change_anything &=
simplify(expr, ns);
735 return did_not_change_anything;
753 auto const current_domain_ptr =
754 std::dynamic_pointer_cast<const constant_propagator_domaint>(
755 this->abstract_state_before(it));
763 if(it->is_goto() || it->is_assume() || it->is_assert())
765 exprt c = it->get_condition();
768 it->set_condition(c);
770 else if(it->is_assign())
772 exprt &rhs = it->assign_rhs_nonconst();
776 if(rhs.
id() == ID_constant)
780 else if(it->is_function_call())
783 d.
values, it->call_function(), ns);
785 for(
auto &arg : it->call_arguments())
788 else if(it->is_other())
790 if(it->get_other().get_statement() == ID_expression)
794 d.
values, c.expression(), ns))
807 replace_const(expr.
type());
810 replace_types_rec(replace_const, *it);
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
bool replace(exprt &dest) const override
This is the basic interface of the abstract interpreter with default implementations of the core func...
ai_history_baset::trace_ptrt trace_ptrt
goto_programt::const_targett locationt
exprt::operandst argumentst
std::vector< parametert > parameterst
const parameterst & parameters() const
void replace_types_rec(const replace_symbolt &replace_const, exprt &expr)
should_track_valuet should_track_value
void replace(goto_functionst::goto_functiont &, const namespacet &)
static void assign_rec(valuest &dest_values, const exprt &lhs, const exprt &rhs, const namespacet &ns, const constant_propagator_ait *cp, bool is_assignment)
Assign value rhs to lhs, recording any newly-known constants in dest_values.
virtual bool is_bottom() const final override
static bool partial_evaluate(const valuest &known_values, exprt &expr, const namespacet &ns)
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.
static bool partial_evaluate_with_all_rounding_modes(const valuest &known_values, exprt &expr, const namespacet &ns)
Attempt to evaluate an expression in all rounding modes.
virtual void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_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...
static bool replace_constants_and_simplify(const valuest &known_values, exprt &expr, const namespacet &ns)
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns, const constant_propagator_ait *cp)
handles equalities and conjunctions containing equalities
virtual void output(std::ostream &out, const ai_baset &ai_base, const namespacet &ns) const override
bool merge(const constant_propagator_domaint &other, trace_ptrt from, trace_ptrt to)
constant_propagator_is_constantt(const replace_symbolt &replace_const)
bool is_constant(const irep_idt &id) const
const replace_symbolt & replace_const
bool is_constant(const exprt &expr) const override
This function determines what expressions are to be propagated as "constants".
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
source_locationt & add_source_location()
bool is_false() const
Return whether the expression is a constant representing false.
bool is_zero() const
Return whether the expression is a constant representing 0.
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
The Boolean constant false.
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
Unbounded, signed integers (mathematical integers, not bitvectors)
bool get_bool(const irep_idt &name) const
const irept & find(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
Determine whether an expression is constant.
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Extract member of struct or union.
const exprt & compound() const
irep_idt get_component_name() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Replace expression or type symbols by an expression or type, respectively.
const expr_mapt & get_expr_map() const
std::unordered_map< irep_idt, exprt > expr_mapt
bool replaces_symbol(const irep_idt &id) const
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
typet type
Type of symbol.
The Boolean constant true.
Semantic type conversion.
The type of an expression, extends irept.
Operator to update elements in structs and arrays.
static void replace_typecast_of_bool(exprt &lhs, exprt &rhs, const namespacet &ns)
bool is_empty(const std::string &s)
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
Deprecated expression utility functions.
#define Forall_goto_program_instructions(it, program)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool simplify(exprt &expr, const namespacet &ns)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
code_expressiont & to_code_expression(codet &code)
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
bool is_constant(const exprt &expr) const
bool meet(const valuest &src, const namespacet &ns)
meet
bool merge(const valuest &src)
join
void output(std::ostream &out, const namespacet &ns) const
void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns)
address_of_aware_replace_symbolt replace_const
void set_to(const symbol_exprt &lhs, const exprt &rhs)