cprover
|
#include <constant_propagator.h>
Classes | |
struct | valuest |
Public Member Functions | |
virtual void | transform (locationt from, locationt to, ai_baset &ai_base, const namespacet &ns) final override |
virtual void | output (std::ostream &out, const ai_baset &ai_base, const namespacet &ns) const override |
bool | merge (const constant_propagator_domaint &other, locationt from, locationt to) |
virtual bool | ai_simplify (exprt &condition, const namespacet &ns) const final override |
Simplify the condition given context-sensitive knowledge from the abstract state. More... | |
virtual void | make_bottom () final override |
virtual void | make_top () final override |
virtual void | make_entry () final override |
virtual bool | is_bottom () const final override |
virtual bool | is_top () const final override |
bool | partial_evaluate (exprt &expr, const namespacet &ns) const |
Attempt to evaluate expression using domain knowledge This function changes the expression that is passed into it. More... | |
![]() | |
ai_domain_baset () | |
virtual | ~ai_domain_baset () |
virtual jsont | output_json (const ai_baset &ai, const namespacet &ns) const |
virtual xmlt | output_xml (const ai_baset &ai, const namespacet &ns) const |
virtual bool | ai_simplify_lhs (exprt &condition, const namespacet &ns) const |
Use the information in the domain to simplify the expression on the LHS of an assignment. More... | |
Public Attributes | |
valuest | values |
Protected Member Functions | |
void | assign_rec (valuest &values, const exprt &lhs, const exprt &rhs, const namespacet &ns) |
bool | two_way_propagate_rec (const exprt &expr, const namespacet &ns) |
handles equalities and conjunctions containing equalities More... | |
bool | partial_evaluate_with_all_rounding_modes (exprt &expr, const namespacet &ns) const |
Attempt to evaluate an expression in all rounding modes. More... | |
bool | replace_constants_and_simplify (exprt &expr, const namespacet &ns) const |
Additional Inherited Members | |
![]() | |
typedef goto_programt::const_targett | locationt |
Definition at line 21 of file constant_propagator.h.
|
finaloverridevirtual |
Simplify the condition given context-sensitive knowledge from the abstract state.
Reimplemented from ai_domain_baset.
Definition at line 271 of file constant_propagator.cpp.
References partial_evaluate().
|
protected |
Definition at line 30 of file constant_propagator.cpp.
References irept::id(), exprt::is_constant(), partial_evaluate(), constant_propagator_domaint::valuest::set_to(), constant_propagator_domaint::valuest::set_to_top(), to_symbol_expr(), and values.
Referenced by transform(), and two_way_propagate_rec().
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 59 of file constant_propagator.h.
References constant_propagator_domaint::valuest::is_bot(), and values.
Referenced by constant_propagator_domaint::valuest::meet(), constant_propagator_domaint::valuest::merge(), constant_propagator_domaint::valuest::output(), and constant_propagator_domaint::valuest::set_to_top().
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 64 of file constant_propagator.h.
References constant_propagator_domaint::valuest::is_top(), and values.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 44 of file constant_propagator.h.
References constant_propagator_domaint::valuest::set_to_bottom(), and values.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 54 of file constant_propagator.h.
References make_top().
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 49 of file constant_propagator.h.
References constant_propagator_domaint::valuest::set_to_top(), and values.
Referenced by make_entry().
bool constant_propagator_domaint::merge | ( | const constant_propagator_domaint & | other, |
locationt | from, | ||
locationt | to | ||
) |
Definition at line 499 of file constant_propagator.cpp.
References constant_propagator_domaint::valuest::merge(), and values.
|
overridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 387 of file constant_propagator.cpp.
References constant_propagator_domaint::valuest::output(), and values.
Referenced by transform().
bool constant_propagator_domaint::partial_evaluate | ( | exprt & | expr, |
const namespacet & | ns | ||
) | const |
Attempt to evaluate expression using domain knowledge This function changes the expression that is passed into it.
expr | The expression to evaluate |
ns | The namespace for symbols in the expression |
Definition at line 512 of file constant_propagator.cpp.
References ID_cprover_rounding_mode_str, constant_propagator_domaint::valuest::is_constant(), partial_evaluate_with_all_rounding_modes(), replace_constants_and_simplify(), and values.
Referenced by ai_simplify(), assign_rec(), and transform().
|
protected |
Attempt to evaluate an expression in all rounding modes.
If the result is the same for all rounding modes, change expr to that result and return false. Otherwise, return true.
Definition at line 530 of file constant_propagator.cpp.
References from_integer(), ID_cprover_rounding_mode_str, replace_constants_and_simplify(), ieee_floatt::ROUND_TO_EVEN, ieee_floatt::ROUND_TO_MINUS_INF, ieee_floatt::ROUND_TO_PLUS_INF, ieee_floatt::ROUND_TO_ZERO, constant_propagator_domaint::valuest::set_to(), and values.
Referenced by partial_evaluate().
|
protected |
Definition at line 566 of file constant_propagator.cpp.
References replace_symbolt::replace(), constant_propagator_domaint::valuest::replace_const, simplify(), and values.
Referenced by partial_evaluate(), and partial_evaluate_with_all_rounding_modes().
|
finaloverridevirtual |
Implements ai_domain_baset.
Definition at line 50 of file constant_propagator.cpp.
References code_function_callt::arguments(), assign_rec(), CPROVER_PREFIX, constant_propagator_ait::dirty, code_function_callt::function(), symbol_exprt::get_identifier(), INVARIANT, constant_propagator_domaint::valuest::is_bottom, exprt::is_false(), code_assignt::lhs(), namespacet::lookup(), output(), code_typet::parameters(), partial_evaluate(), code_assignt::rhs(), constant_propagator_domaint::valuest::set_dirty_to_top(), constant_propagator_domaint::valuest::set_to_bottom(), constant_propagator_domaint::valuest::set_to_top(), code_declt::symbol(), code_deadt::symbol(), to_code_assign(), to_code_dead(), to_code_decl(), to_code_function_call(), to_code_type(), to_symbol_expr(), two_way_propagate_rec(), symbolt::type, and values.
|
protected |
handles equalities and conjunctions containing equalities
Definition at line 221 of file constant_propagator.cpp.
References assign_rec(), forall_operands, format(), irept::id(), constant_propagator_domaint::valuest::is_constant(), constant_propagator_domaint::valuest::meet(), exprt::op0(), exprt::op1(), and values.
Referenced by transform().
valuest constant_propagator_domaint::values |
Definition at line 139 of file constant_propagator.h.
Referenced by assign_rec(), is_bottom(), is_top(), make_bottom(), make_top(), merge(), output(), partial_evaluate(), partial_evaluate_with_all_rounding_modes(), replace_constants_and_simplify(), transform(), and two_way_propagate_rec().