60 if(lhs.
id() == ID_dereference)
67 const bool have_dirty = (cp !=
nullptr);
77 assign_rec(dest_values, eval_lhs, rhs, ns, cp, is_assignment);
79 else if(lhs.
id() == ID_index)
83 assign_rec(dest_values, index_expr.
array(), new_rhs, ns, cp, is_assignment);
85 else if(lhs.
id() == ID_member)
91 dest_values, member_expr.
compound(), new_rhs, ns, cp, is_assignment);
93 else if(lhs.
id() == ID_symbol)
107 "type of constant to be replaced should match");
108 dest_values.
set_to(s, tmp);
116 else if(is_assignment)
132 locationt from{trace_from->current_location()};
133 locationt to{trace_to->current_location()};
136 std::cout <<
"Transform from/to:\n";
137 std::cout << from->location_number <<
" --> "
138 << to->location_number <<
'\n';
142 std::cout <<
"Before:\n";
143 output(std::cout, ai, ns);
152 bool have_dirty=(cp!=
nullptr);
165 else if(from->is_assign())
167 const exprt &lhs = from->assign_lhs();
168 const exprt &rhs = from->assign_rhs();
171 else if(from->is_assume())
175 else if(from->is_goto())
181 if(from->get_target()==to)
182 g = from->get_condition();
191 else if(from->is_dead())
195 else if(from->is_function_call())
197 const exprt &
function = from->call_function();
199 if(
function.
id()==ID_symbol)
206 if(function_from == function_to)
236 from->call_arguments();
238 code_typet::parameterst::const_iterator p_it=parameters.begin();
239 for(
const auto &arg : arguments)
241 if(p_it==parameters.end())
244 const symbol_exprt parameter_expr(p_it->get_identifier(), arg.type());
255 function_from == function_to,
256 "Unresolved call can only be approximated if a skip");
264 else if(from->is_end_function())
278 "Transform only sets bottom by using branch conditions");
281 std::cout <<
"After:\n";
282 output(std::cout, ai, ns);
292 if(lhs.
id() != ID_typecast)
303 lhs = lhs_underlying;
314 std::cout <<
"two_way_propagate_rec: " <<
format(expr) <<
'\n';
319 if(expr.
id()==ID_and)
322 bool change_this_time;
325 change_this_time =
false;
333 }
while(change_this_time);
335 else if(expr.
id() == ID_not)
339 if(op.id() == ID_equal || op.id() == ID_notequal)
342 subexpr.
id(subexpr.
id() == ID_equal ? ID_notequal : ID_equal);
351 else if(expr.
id() == ID_symbol)
359 else if(expr.
id() == ID_notequal)
386 else if(expr.
id() == ID_equal)
395 assign_rec(copy_values, lhs, rhs, ns, cp,
false);
402 std::cout <<
"two_way_propagate_rec: " << change <<
'\n';
436 if(expr.
id() == ID_symbol)
459 const auto n_erased = replace_const.erase(symbol_expr.
get_identifier());
472 expr_mapt &expr_map = replace_const.get_expr_map();
474 for(expr_mapt::iterator it=expr_map.begin();
485 it = replace_const.erase(it);
496 out <<
"const map:\n";
502 "If the domain is bottom, the map must be empty");
513 for(
const auto &p : replace_const.get_expr_map())
515 out <<
' ' << p.first <<
"=" <<
from_expr(ns, p.first, p.second) <<
'\n';
566 for(replace_symbolt::expr_mapt::iterator it=expr_map.begin();
570 const exprt &expr=it->second;
572 replace_symbolt::expr_mapt::const_iterator s_it;
573 s_it=src_expr_map.
find(
id);
575 if(s_it!=src_expr_map.end())
578 const exprt &src_expr=s_it->second;
582 it = replace_const.erase(it);
590 it = replace_const.erase(it);
611 replace_symbolt::expr_mapt::const_iterator c_it =
612 replace_const.get_expr_map().find(m.first);
614 if(c_it != replace_const.get_expr_map().end())
616 if(c_it->second!=m.second)
627 m_id_type == m.second.type(),
628 "type of constant to be stored should match");
678 auto rounding_modes = std::array<ieee_floatt::rounding_modet, 4>{
686 for(std::size_t i = 0; i < rounding_modes.size(); ++i)
688 valuest tmp_values = known_values;
699 first_result = result;
701 else if(result != first_result)
715 bool did_not_change_anything =
true;
725 did_not_change_anything =
false;
731 if(did_not_change_anything)
732 did_not_change_anything &=
simplify(expr, ns);
734 return did_not_change_anything;
752 auto const current_domain_ptr =
753 std::dynamic_pointer_cast<const constant_propagator_domaint>(
754 this->abstract_state_before(it));
762 if(it->is_goto() || it->is_assume() || it->is_assert())
764 exprt c = it->get_condition();
767 it->set_condition(c);
769 else if(it->is_assign())
771 exprt &rhs = it->assign_rhs_nonconst();
775 if(rhs.
id() == ID_constant)
779 else if(it->is_function_call())
782 d.
values, it->call_function(), ns);
784 for(
auto &arg : it->call_arguments())
787 else if(it->is_other())
789 if(it->get_other().get_statement() == ID_expression)
793 d.
values, c.expression(), ns))
806 replace_const(expr.
type());
809 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)
void set(const irep_namet &name, const irep_idt &value)
bool get_bool(const irep_namet &name) const
const irept & find(const irep_namet &name) const
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)
#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)