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)
131 locationt from{trace_from->current_location()};
132 locationt to{trace_to->current_location()};
135 std::cout <<
"Transform from/to:\n";
136 std::cout << from->location_number <<
" --> "
137 << to->location_number <<
'\n';
141 std::cout <<
"Before:\n";
142 output(std::cout, ai, ns);
151 bool have_dirty=(cp!=
nullptr);
164 else if(from->is_assign())
166 const auto &assignment = from->get_assign();
167 const exprt &lhs=assignment.lhs();
168 const exprt &rhs=assignment.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 auto &function_call = from->get_function_call();
198 const exprt &
function=function_call.function();
200 if(
function.
id()==ID_symbol)
207 if(function_from == function_to)
237 function_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 auto assign = it->get_assign();
773 exprt &rhs = assign.rhs();
777 if(rhs.
id() == ID_constant)
779 it->set_assign(assign);
782 else if(it->is_function_call())
784 auto call = it->get_function_call();
786 bool call_changed =
false;
789 d.
values, call.function(), ns))
794 for(
auto &arg : call.arguments())
799 it->set_function_call(call);
801 else if(it->is_other())
803 if(it->get_other().get_statement() == ID_expression)
807 d.
values, c.expression(), ns))
820 replace_const(expr.
type());
823 replace_types_rec(replace_const, *it);
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
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
bool merge(const constant_propagator_domaint &other, locationt from, locationt to)
virtual void output(std::ostream &out, const ai_baset &ai_base, const namespacet &ns) const override
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)
const char ID_cprover_rounding_mode_str[]
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)