95 if(
cp && !
cp->should_track_value(lhs, ns))
107 "type of constant to be replaced should match");
116 else if(is_assignment)
136 std::cout <<
"Transform from/to:\n";
137 std::cout <<
from->location_number <<
" --> "
138 <<
to->location_number <<
'\n';
142 std::cout <<
"Before:\n";
165 else if(
from->is_assign())
171 else if(
from->is_assume())
175 else if(
from->is_goto())
181 if(
from->get_target()==
to)
182 g =
from->condition();
191 else if(
from->is_dead())
195 else if(
from->is_function_call())
197 const exprt &function =
from->call_function();
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())
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";
314 std::cout <<
"two_way_propagate_rec: " <<
format(expr) <<
'\n';
327 for(
const auto &op : expr.
operands())
402 std::cout <<
"two_way_propagate_rec: " <<
change <<
'\n';
478 expr_mapt &expr_map = replace_const.get_expr_map();
480 for(expr_mapt::iterator it=expr_map.begin();
491 it = replace_const.erase(it);
502 out <<
"const map:\n";
508 "If the domain is bottom, the map must be empty");
519 for(
const auto &p : replace_const.get_expr_map())
521 out <<
' ' << p.first <<
"=" <<
from_expr(ns, p.first, p.second) <<
'\n';
572 for(replace_symbolt::expr_mapt::iterator it=expr_map.begin();
576 const exprt &expr=it->second;
578 replace_symbolt::expr_mapt::const_iterator
s_it;
588 it = replace_const.erase(it);
596 it = replace_const.erase(it);
617 replace_symbolt::expr_mapt::const_iterator
c_it =
618 replace_const.get_expr_map().find(m.first);
620 if(
c_it != replace_const.get_expr_map().end())
622 if(
c_it->second!=m.second)
634 "type of constant to be stored should match");
684 auto rounding_modes = std::array<ieee_floatt::rounding_modet, 4>{
692 for(std::size_t i = 0; i < rounding_modes.size(); ++i)
759 std::dynamic_pointer_cast<const constant_propagator_domaint>(
760 this->abstract_state_before(it));
768 if(it->is_goto() || it->is_assume() || it->is_assert())
770 exprt c = it->condition();
773 it->condition_nonconst() =
c;
775 else if(it->is_assign())
777 exprt &rhs = it->assign_rhs_nonconst();
785 else if(it->is_function_call())
788 d.
values, it->call_function(), ns);
790 for(
auto &arg : it->call_arguments())
793 else if(it->is_other())
812 replace_const(expr.
type());
815 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.
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Determine whether an expression is constant.
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
exprt::operandst argumentst
std::vector< parametert > parameterst
const parameterst & parameters() const
void replace_types_rec(const replace_symbolt &replace_const, exprt &expr)
void replace(goto_functionst::goto_functiont &, const namespacet &)
const replace_symbolt & replace_const
bool is_constant(const irep_idt &id) const
bool is_constant(const exprt &expr) const override
This function determines what expressions are to be propagated as "constants".
constant_propagator_can_forward_propagatet(const replace_symbolt &replace_const, const namespacet &ns)
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)
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.
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.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
source_locationt & add_source_location()
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 irep_idt & id() const
Extract member of struct or union.
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 a symbol expression by a given expression.
const expr_mapt & get_expr_map() const
std::unordered_map< irep_idt, exprt > expr_mapt
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)
#define Forall_operands(it, expr)
Deprecated expression utility functions.
static bool is_empty(const goto_programt &goto_program)
#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)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
code_expressiont & to_code_expression(codet &code)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_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 namespacet &ns) 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