22#ifndef CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
23#define CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
73 virtual bool is_top() const final
override
179 dirty(goto_functions),
187 dirty(goto_function),
195 dirty(goto_model.goto_functions),
204 const irep_idt &function_identifier,
210 operator()(function_identifier, goto_function, ns);
Replace symbols with constants while maintaining syntactically valid expressions.
This is the basic interface of the abstract interpreter with default implementations of the core func...
void operator()(const irep_idt &function_id, const goto_programt &goto_program, const namespacet &ns)
Run abstract interpretation on a single function.
ai_domain_baset()
The constructor is expected to produce 'false' or 'bottom' A default constructor is not part of the d...
ai_history_baset::trace_ptrt trace_ptrt
std::function< bool(const exprt &, const namespacet &)> should_track_valuet
constant_propagator_ait(goto_modelt &goto_model, should_track_valuet should_track_value=track_all_values)
void replace_types_rec(const replace_symbolt &replace_const, exprt &expr)
static bool track_all_values(const exprt &, const namespacet &)
constant_propagator_ait(const goto_functionst &goto_functions, should_track_valuet should_track_value=track_all_values)
should_track_valuet should_track_value
constant_propagator_ait(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, should_track_valuet should_track_value=track_all_values)
constant_propagator_ait(const goto_functiont &goto_function, should_track_valuet should_track_value=track_all_values)
friend class constant_propagator_domaint
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
virtual bool is_top() 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
virtual void make_top() final override
all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implem...
bool merge(const constant_propagator_domaint &other, trace_ptrt from, trace_ptrt to)
virtual void make_bottom() final override
no states
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Base class for all expressions.
A collection of goto functions.
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Replace a symbol expression by a given expression.
Expression to hold a symbol (variable)
Variables whose address is taken.
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
void set_to(const symbol_exprt &lhs, const exprt &rhs)