Go to the documentation of this file.
59 if(lhs.
id() == ID_dereference)
66 const bool have_dirty = (cp !=
nullptr);
76 assign_rec(dest_values, eval_lhs, rhs, ns, cp, is_assignment);
78 else if(lhs.
id() == ID_index)
82 assign_rec(dest_values, index_expr.
array(), new_rhs, ns, cp, is_assignment);
84 else if(lhs.
id() == ID_member)
90 dest_values, member_expr.
compound(), new_rhs, ns, cp, is_assignment);
92 else if(lhs.
id() == ID_symbol)
106 "type of constant to be replaced should match");
107 dest_values.
set_to(s, tmp);
115 else if(is_assignment)
132 std::cout <<
"Transform from/to:\n";
133 std::cout << from->location_number <<
" --> "
134 << to->location_number <<
'\n';
138 std::cout <<
"Before:\n";
139 output(std::cout, ai, ns);
148 bool have_dirty=(cp!=
nullptr);
158 const auto &code_decl = from->get_decl();
162 else if(from->is_assign())
164 const auto &assignment = from->get_assign();
165 const exprt &lhs=assignment.lhs();
166 const exprt &rhs=assignment.rhs();
169 else if(from->is_assume())
173 else if(from->is_goto())
179 if(from->get_target()==to)
180 g = from->get_condition();
189 else if(from->is_dead())
191 const auto &code_dead = from->get_dead();
194 else if(from->is_function_call())
196 const auto &function_call = from->get_function_call();
197 const exprt &
function=function_call.function();
199 if(
function.
id()==ID_symbol)
206 if(function_from == function_to)
236 function_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;
760 if(it->is_goto() || it->is_assume() || it->is_assert())
762 exprt c = it->get_condition();
765 it->set_condition(c);
767 else if(it->is_assign())
769 auto assign = it->get_assign();
770 exprt &rhs = assign.rhs();
774 if(rhs.
id() == ID_constant)
776 it->set_assign(assign);
779 else if(it->is_function_call())
781 auto call = it->get_function_call();
783 bool call_changed =
false;
786 d.
values, call.function(), ns))
791 for(
auto &arg : call.arguments())
796 it->set_function_call(call);
798 else if(it->is_other())
800 if(it->get_other().get_statement() == ID_expression)
804 d.
values, c.expression(), ns))
817 replace_const(expr.
type());
820 replace_types_rec(replace_const, *it);
Determine whether an expression is constant.
Operator to update elements in structs and arrays.
#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[]
code_expressiont & to_code_expression(codet &code)
address_of_aware_replace_symbolt replace_const
bool replaces_symbol(const irep_idt &id) const
#define Forall_operands(it, expr)
should_track_valuet should_track_value
bool is_constant(const exprt &expr) const
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
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
bool is_constant(const irep_idt &id) const
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...
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
typet type
Type of symbol.
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.
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)
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
Expression to hold a symbol (variable)
bool is_false() const
Return whether the expression is a constant representing false.
static bool replace_constants_and_simplify(const valuest &known_values, exprt &expr, const namespacet &ns)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
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().
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.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const exprt & compound() const
#define forall_operands(it, expr)
bool merge(const constant_propagator_domaint &other, locationt from, locationt to)
void output(std::ostream &out, const namespacet &ns) const
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
bool replace(exprt &dest) const override
bool is_constant(const exprt &expr) const override
This function determines what expressions are to be propagated as "constants".
bool simplify(exprt &expr, const namespacet &ns)
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
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
exprt::operandst argumentst
The Boolean constant false.
const parameterst & parameters() const
constant_propagator_is_constantt(const replace_symbolt &replace_const)
void replace_types_rec(const replace_symbolt &replace_const, exprt &expr)
#define Forall_goto_functions(it, functions)
::goto_functiont goto_functiont
bool is_zero() const
Return whether the expression is a constant representing 0.
Extract member of struct or union.
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
Deprecated expression utility functions.
A collection of goto functions.
goto_programt::const_targett locationt
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
void set(const irep_namet &name, const irep_idt &value)
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.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
bool is_constant() const
Return whether the expression is a constant.
void set_to(const symbol_exprt &lhs, const exprt &rhs)
This is the basic interface of the abstract interpreter with default implementations of the core func...
bool meet(const valuest &src, const namespacet &ns)
meet
const replace_symbolt & replace_const
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
void replace(goto_functionst::goto_functiont &, const namespacet &)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
irep_idt get_component_name() const
static void replace_typecast_of_bool(exprt &lhs, exprt &rhs, const namespacet &ns)
source_locationt & add_source_location()
Semantic type conversion.
The Boolean constant true.
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
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.