cprover
|
#include <value_set_fivr.h>
Classes | |
struct | entryt |
class | object_map_dt |
class | objectt |
Public Types | |
typedef irep_idt | idt |
typedef reference_counting< object_map_dt > | object_mapt |
typedef std::unordered_set< exprt, irep_hash > | expr_sett |
typedef std::unordered_set< unsigned int > | dynamic_object_id_sett |
typedef std::unordered_map< idt, entryt, string_hash > | valuest |
typedef std::unordered_set< idt, string_hash > | flatten_seent |
typedef std::unordered_set< idt, string_hash > | gvs_recursion_sett |
typedef std::unordered_set< idt, string_hash > | recfind_recursion_sett |
typedef std::unordered_set< idt, string_hash > | assign_recursion_sett |
Public Member Functions | |
value_set_fivrt () | |
void | set_from (const irep_idt &function, unsigned inx) |
void | set_to (const irep_idt &function, unsigned inx) |
exprt | to_expr (object_map_dt::const_iterator it) const |
void | set (object_mapt &dest, object_map_dt::const_iterator it) const |
bool | insert_to (object_mapt &dest, object_map_dt::const_iterator it) const |
bool | insert_to (object_mapt &dest, const exprt &src) const |
bool | insert_to (object_mapt &dest, const exprt &src, const mp_integer &offset) const |
bool | insert_to (object_mapt &dest, unsigned n, const objectt &object) const |
bool | insert_to (object_mapt &dest, const exprt &expr, const objectt &object) const |
bool | insert_from (object_mapt &dest, object_map_dt::const_iterator it) const |
bool | insert_from (object_mapt &dest, const exprt &src) const |
bool | insert_from (object_mapt &dest, const exprt &src, const mp_integer &offset) const |
bool | insert_from (object_mapt &dest, unsigned n, const objectt &object) const |
bool | insert_from (object_mapt &dest, const exprt &expr, const objectt &object) const |
void | get_value_set (const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const |
expr_sett & | get (const idt &identifier, const std::string &suffix) |
void | make_any () |
void | clear () |
void | add_var (const idt &id, const std::string &suffix) |
void | add_var (const entryt &e) |
entryt & | get_entry (const idt &id, const std::string &suffix) |
entryt & | get_entry (const entryt &e) |
entryt & | get_temporary_entry (const idt &id, const std::string &suffix) |
void | add_vars (const std::list< entryt > &vars) |
void | output (const namespacet &ns, std::ostream &out) const |
bool | make_union (object_mapt &dest, const object_mapt &src) const |
bool | make_valid_union (object_mapt &dest, const object_mapt &src) const |
void | copy_objects (object_mapt &dest, const object_mapt &src) const |
void | apply_code (const exprt &code, const namespacet &ns) |
bool | handover () |
void | assign (const exprt &lhs, const exprt &rhs, const namespacet &ns, bool add_to_sets=false) |
void | do_function_call (const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns) |
void | do_end_function (const exprt &lhs, const namespacet &ns) |
void | get_reference_set (const exprt &expr, expr_sett &expr_set, const namespacet &ns) const |
Public Attributes | |
unsigned | to_function |
unsigned | from_function |
unsigned | to_target_index |
unsigned | from_target_index |
valuest | values |
valuest | temporary_values |
Static Public Attributes | |
static object_numberingt | object_numbering |
static hash_numbering< irep_idt, irep_id_hash > | function_numbering |
Protected Member Functions | |
void | get_reference_set_sharing (const exprt &expr, expr_sett &expr_set, const namespacet &ns) const |
void | get_value_set_rec (const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns, gvs_recursion_sett &recursion_set) const |
void | get_value_set (const exprt &expr, object_mapt &dest, const namespacet &ns) const |
void | get_reference_set_sharing (const exprt &expr, object_mapt &dest, const namespacet &ns) const |
void | get_reference_set_sharing_rec (const exprt &expr, object_mapt &dest, const namespacet &ns) const |
void | dereference_rec (const exprt &src, exprt &dest) const |
void | assign_rec (const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set, bool add_to_sets) |
void | do_free (const exprt &op, const namespacet &ns) |
void | flatten (const entryt &e, object_mapt &dest) const |
void | flatten_rec (const entryt &, object_mapt &, flatten_seent &, unsigned from_function, unsigned from_index) const |
bool | recursive_find (const irep_idt &ident, const object_mapt &rhs, recfind_recursion_sett &recursion_set) const |
Definition at line 26 of file value_set_fivr.h.
typedef std::unordered_set<idt, string_hash> value_set_fivrt::assign_recursion_sett |
Definition at line 236 of file value_set_fivr.h.
typedef std::unordered_set<unsigned int> value_set_fivrt::dynamic_object_id_sett |
Definition at line 223 of file value_set_fivr.h.
typedef std::unordered_set<exprt, irep_hash> value_set_fivrt::expr_sett |
Definition at line 221 of file value_set_fivr.h.
typedef std::unordered_set<idt, string_hash> value_set_fivrt::flatten_seent |
Definition at line 233 of file value_set_fivr.h.
typedef std::unordered_set<idt, string_hash> value_set_fivrt::gvs_recursion_sett |
Definition at line 234 of file value_set_fivr.h.
typedef irep_idt value_set_fivrt::idt |
Definition at line 50 of file value_set_fivr.h.
Definition at line 143 of file value_set_fivr.h.
typedef std::unordered_set<idt, string_hash> value_set_fivrt::recfind_recursion_sett |
Definition at line 235 of file value_set_fivr.h.
typedef std::unordered_map<idt, entryt, string_hash> value_set_fivrt::valuest |
Definition at line 232 of file value_set_fivr.h.
|
inline |
Definition at line 29 of file value_set_fivr.h.
|
inline |
Definition at line 258 of file value_set_fivr.h.
References get_entry().
Referenced by add_vars(), and do_function_call().
|
inline |
Definition at line 263 of file value_set_fivr.h.
References get_entry(), value_set_fivrt::entryt::identifier, and value_set_fivrt::entryt::suffix.
|
inline |
Definition at line 289 of file value_set_fivr.h.
References add_var(), and output().
Referenced by value_set_analysis_fivrt::add_vars().
void value_set_fivrt::apply_code | ( | const exprt & | code, |
const namespacet & | ns | ||
) |
Definition at line 1575 of file value_set_fivr.cpp.
References assign(), do_free(), forall_operands, from_function, irept::get(), irept::id(), id2string(), exprt::op0(), exprt::op1(), exprt::operands(), irept::pretty(), and exprt::type().
Referenced by value_set_domain_fivrt::transform().
void value_set_fivrt::assign | ( | const exprt & | lhs, |
const exprt & | rhs, | ||
const namespacet & | ns, | ||
bool | add_to_sets = false |
||
) |
Definition at line 1081 of file value_set_fivr.cpp.
References assign_rec(), base_type_eq(), struct_union_typet::components(), exprt::copy_to_operands(), namespace_baset::follow(), forall_operands, from_expr(), get_value_set(), irept::id(), index_type(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), irept::pretty(), irept::set(), typet::subtype(), to_struct_type(), and exprt::type().
Referenced by apply_code(), do_end_function(), and do_function_call().
|
protected |
Definition at line 1321 of file value_set_fivr.cpp.
References value_set_fivrt::object_map_dt::begin(), dynamic_object(), value_set_fivrt::object_map_dt::end(), namespace_baset::follow(), forall_objects, get_entry(), dynamic_object_exprt::get_instance(), get_reference_set_sharing(), get_temporary_entry(), get_value_set_rec(), has_prefix(), irept::id(), id2string(), make_union(), make_valid_union(), value_set_fivrt::entryt::object_map, object_numbering, typecast_exprt::op(), reference_counting< T >::read(), recursive_find(), to_dynamic_object_expr(), to_expr(), to_typecast_expr(), and values.
Referenced by assign(), and get_reference_set_sharing().
|
inline |
Definition at line 253 of file value_set_fivr.h.
References values.
Referenced by value_set_domain_fivrt::clear(), and value_set_domain_fivrt::initialize().
void value_set_fivrt::copy_objects | ( | object_mapt & | dest, |
const object_mapt & | src | ||
) | const |
Definition at line 396 of file value_set_fivr.cpp.
References forall_valid_objects, from_function, from_target_index, reference_counting< T >::read(), value_set_fivrt::object_map_dt::validity_ranges, and reference_counting< T >::write().
Referenced by get_value_set_rec().
Definition at line 802 of file value_set_fivr.cpp.
References irept::id(), exprt::op0(), exprt::operands(), and exprt::type().
Referenced by get_reference_set_sharing().
void value_set_fivrt::do_end_function | ( | const exprt & | lhs, |
const namespacet & | ns | ||
) |
Definition at line 1562 of file value_set_fivr.cpp.
References assign(), from_function, irept::is_nil(), and exprt::type().
Referenced by value_set_domain_fivrt::transform().
|
protected |
Definition at line 1240 of file value_set_fivr.cpp.
References dynamic_object(), flatten(), forall_objects, dynamic_object_exprt::get_instance(), get_temporary_entry(), get_value_set(), irept::id(), value_set_fivrt::entryt::identifier, insert_to(), exprt::is_true(), value_set_fivrt::entryt::object_map, object_numbering, reference_counting< T >::read(), to_dynamic_object_expr(), exprt::type(), dynamic_object_exprt::valid(), and values.
Referenced by apply_code(), and get_reference_set_sharing().
void value_set_fivrt::do_function_call | ( | const irep_idt & | function, |
const exprt::operandst & | arguments, | ||
const namespacet & | ns | ||
) |
Definition at line 1495 of file value_set_fivr.cpp.
References add_var(), assign(), from_function, from_target_index, id2string(), namespacet::lookup(), make_union(), code_typet::parameters(), temporary_values, to_code_type(), to_function, to_target_index, symbolt::type, and values.
Referenced by value_set_domain_fivrt::transform().
|
protected |
Definition at line 215 of file value_set_fivr.cpp.
References flatten_rec(), from_function, from_target_index, value_set_fivrt::entryt::identifier, and value_set_fivrt::entryt::suffix.
Referenced by do_free(), get_reference_set(), get_reference_set_sharing(), get_reference_set_sharing_rec(), get_value_set(), and output().
|
protected |
Definition at line 231 of file value_set_fivr.cpp.
References value_set_fivrt::object_map_dt::begin(), value_set_fivrt::object_map_dt::end(), forall_objects, Forall_objects, forall_valid_objects, irept::get(), irept::id(), id2string(), value_set_fivrt::entryt::identifier, insert_from(), value_set_fivrt::entryt::object_map, object_numbering, reference_counting< T >::read(), irept::set(), value_set_fivrt::object_map_dt::set_valid_at(), typet::subtype(), value_set_fivrt::entryt::suffix, exprt::type(), value_set_fivrt::object_map_dt::validity_ranges, values, and reference_counting< T >::write().
Referenced by flatten(), and get_reference_set_sharing().
Definition at line 268 of file value_set_fivr.h.
Referenced by add_var(), and assign_rec().
Definition at line 273 of file value_set_fivr.h.
References id2string(), value_set_fivrt::entryt::identifier, r, value_set_fivrt::entryt::suffix, and values.
void value_set_fivrt::get_reference_set | ( | const exprt & | expr, |
expr_sett & | expr_set, | ||
const namespacet & | ns | ||
) | const |
Definition at line 820 of file value_set_fivr.cpp.
References value_set_fivrt::object_map_dt::begin(), value_set_fivrt::object_map_dt::end(), flatten(), forall_objects, irept::get(), get_reference_set_sharing(), irept::id(), object_numbering, reference_counting< T >::read(), to_expr(), exprt::type(), values, and reference_counting< T >::write().
Referenced by value_set_domain_fivrt::get_reference_set().
|
protected |
Definition at line 869 of file value_set_fivr.cpp.
References forall_objects, reference_counting< T >::read(), and to_expr().
Referenced by assign_rec(), get_reference_set(), get_reference_set_sharing_rec(), and get_value_set_rec().
|
inlineprotected |
Definition at line 364 of file value_set_fivr.h.
References assign_rec(), dereference_rec(), do_free(), flatten(), flatten_rec(), get_reference_set_sharing_rec(), and recursive_find().
|
protected |
Definition at line 881 of file value_set_fivr.cpp.
References value_set_fivrt::object_map_dt::begin(), exprt::copy_to_operands(), value_set_fivrt::object_map_dt::end(), flatten(), namespace_baset::follow(), forall_objects, forall_valid_objects, from_expr(), from_integer(), irept::get(), get_reference_set_sharing(), get_value_set_rec(), irept::id(), irept::id_string(), index_type(), insert_from(), exprt::is_zero(), object_numbering, value_set_fivrt::objectt::offset, value_set_fivrt::objectt::offset_is_set, value_set_fivrt::objectt::offset_is_zero(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), reference_counting< T >::read(), typet::subtype(), to_integer(), exprt::type(), values, and reference_counting< T >::write().
Referenced by get_reference_set_sharing().
Definition at line 283 of file value_set_fivr.h.
References id2string(), and temporary_values.
Referenced by assign_rec(), and do_free().
void value_set_fivrt::get_value_set | ( | const exprt & | expr, |
std::list< exprt > & | expr_set, | ||
const namespacet & | ns | ||
) | const |
Definition at line 410 of file value_set_fivr.cpp.
References value_set_fivrt::object_map_dt::begin(), value_set_fivrt::object_map_dt::end(), flatten(), forall_objects, from_expr(), object_numbering, reference_counting< T >::read(), to_expr(), values, and reference_counting< T >::write().
Referenced by assign(), do_free(), and value_set_analysis_fivrt::get_values().
|
protected |
Definition at line 474 of file value_set_fivr.cpp.
References get_value_set_rec(), simplify(), and exprt::type().
|
protected |
Definition at line 486 of file value_set_fivr.cpp.
References alloc_adapter_prefix, value_set_fivrt::object_map_dt::begin(), copy_objects(), dynamic_object(), value_set_fivrt::object_map_dt::end(), namespace_baset::follow(), forall_objects, forall_operands, forall_valid_objects, from_function, from_target_index, dynamic_object_exprt::get_instance(), get_reference_set_sharing(), irept::get_string(), has_prefix(), irept::id(), id2string(), insert_from(), object_numbering, value_set_fivrt::objectt::offset_is_set, reference_counting< T >::read(), dynamic_object_exprt::set_instance(), typet::subtype(), to_dynamic_object_expr(), to_integer(), exprt::type(), dynamic_object_exprt::valid(), and values.
Referenced by assign_rec(), get_reference_set_sharing_rec(), and get_value_set().
bool value_set_fivrt::handover | ( | void | ) |
Definition at line 1906 of file value_set_fivr.cpp.
References Forall_valid_objects, id2string(), make_union(), value_set_fivrt::object_map_dt::set_valid_at(), temporary_values, to_function, to_target_index, values, and reference_counting< T >::write().
Referenced by value_set_domain_fivrt::transform().
|
inline |
Definition at line 178 of file value_set_fivr.h.
Referenced by flatten_rec(), get_reference_set_sharing_rec(), get_value_set_rec(), and insert_from().
|
inline |
Definition at line 183 of file value_set_fivr.h.
References insert_from(), hash_numbering< T, hash_fkt >::number(), and value_set_fivrt::objectt::objectt().
|
inline |
Definition at line 188 of file value_set_fivr.h.
References insert_from(), hash_numbering< T, hash_fkt >::number(), and value_set_fivrt::objectt::objectt().
bool value_set_fivrt::insert_from | ( | object_mapt & | dest, |
unsigned | n, | ||
const objectt & | object | ||
) | const |
Definition at line 1712 of file value_set_fivr.cpp.
References value_set_fivrt::object_map_dt::end(), value_set_fivrt::object_map_dt::find(), from_function, from_target_index, value_set_fivrt::objectt::offset, value_set_fivrt::objectt::offset_is_set, value_set_fivrt::object_map_dt::set_valid_at(), and reference_counting< T >::write().
|
inline |
Definition at line 198 of file value_set_fivr.h.
References insert_from(), and hash_numbering< T, hash_fkt >::number().
|
inline |
Definition at line 150 of file value_set_fivr.h.
Referenced by do_free(), insert_to(), make_union(), and make_valid_union().
|
inline |
Definition at line 155 of file value_set_fivr.h.
References insert_to(), hash_numbering< T, hash_fkt >::number(), and value_set_fivrt::objectt::objectt().
|
inline |
Definition at line 160 of file value_set_fivr.h.
References insert_to(), hash_numbering< T, hash_fkt >::number(), and value_set_fivrt::objectt::objectt().
bool value_set_fivrt::insert_to | ( | object_mapt & | dest, |
unsigned | n, | ||
const objectt & | object | ||
) | const |
Definition at line 1671 of file value_set_fivr.cpp.
References value_set_fivrt::object_map_dt::end(), value_set_fivrt::object_map_dt::find(), value_set_fivrt::objectt::offset, value_set_fivrt::objectt::offset_is_set, value_set_fivrt::object_map_dt::set_valid_at(), to_function, to_target_index, and reference_counting< T >::write().
|
inline |
Definition at line 170 of file value_set_fivr.h.
References insert_to(), and hash_numbering< T, hash_fkt >::number().
|
inline |
Definition at line 248 of file value_set_fivr.h.
References values.
bool value_set_fivrt::make_union | ( | object_mapt & | dest, |
const object_mapt & | src | ||
) | const |
Definition at line 366 of file value_set_fivr.cpp.
References forall_objects, insert_to(), and reference_counting< T >::read().
Referenced by assign_rec(), do_function_call(), and handover().
bool value_set_fivrt::make_valid_union | ( | object_mapt & | dest, |
const object_mapt & | src | ||
) | const |
Definition at line 381 of file value_set_fivr.cpp.
References forall_valid_objects, insert_to(), and reference_counting< T >::read().
Referenced by assign_rec().
void value_set_fivrt::output | ( | const namespacet & | ns, |
std::ostream & | out | ||
) | const |
Definition at line 57 of file value_set_fivr.cpp.
References symbolt::display_name(), value_set_fivrt::object_map_dt::empty(), value_set_fivrt::object_map_dt::end(), flatten(), forall_objects, from_expr(), from_function, from_target_index, from_type(), function_numbering, irept::id(), id2string(), value_set_fivrt::entryt::identifier, integer2string(), namespacet::lookup(), symbolt::name, object_numbering, reference_counting< T >::read(), value_set_fivrt::entryt::suffix, exprt::type(), value_set_fivrt::object_map_dt::validity_ranges, and values.
Referenced by add_vars(), and value_set_domain_fivrt::output().
|
protected |
Definition at line 1867 of file value_set_fivr.cpp.
References forall_objects, irept::get(), irept::id(), value_set_fivrt::entryt::object_map, object_numbering, reference_counting< T >::read(), exprt::type(), and values.
Referenced by assign_rec(), and get_reference_set_sharing().
|
inline |
Definition at line 145 of file value_set_fivr.h.
References reference_counting< T >::write().
|
inline |
Definition at line 38 of file value_set_fivr.h.
References hash_numbering< T, hash_fkt >::number().
Referenced by value_set_analysis_fivrt::output(), and value_set_domain_fivrt::transform().
|
inline |
Definition at line 44 of file value_set_fivr.h.
References hash_numbering< T, hash_fkt >::number().
Referenced by value_set_analysis_fivrt::output(), and value_set_domain_fivrt::transform().
exprt value_set_fivrt::to_expr | ( | object_map_dt::const_iterator | it | ) | const |
Definition at line 346 of file value_set_fivr.cpp.
References from_integer(), index_type(), object_descriptor_exprt::object(), object_numbering, object_descriptor_exprt::offset(), and exprt::type().
Referenced by assign_rec(), get_reference_set(), get_reference_set_sharing(), and get_value_set().
unsigned value_set_fivrt::from_function |
Definition at line 33 of file value_set_fivr.h.
Referenced by apply_code(), copy_objects(), do_end_function(), do_function_call(), flatten(), get_value_set_rec(), value_set_analysis_fivrt::get_values(), insert_from(), and output().
unsigned value_set_fivrt::from_target_index |
Definition at line 34 of file value_set_fivr.h.
Referenced by copy_objects(), do_function_call(), flatten(), get_value_set_rec(), value_set_analysis_fivrt::get_values(), insert_from(), and output().
|
static |
Definition at line 36 of file value_set_fivr.h.
Referenced by value_set_analysis_fivrt::get_values(), and output().
|
static |
Definition at line 35 of file value_set_fivr.h.
Referenced by assign_rec(), do_free(), flatten_rec(), get_reference_set(), get_reference_set_sharing_rec(), get_value_set(), get_value_set_rec(), output(), recursive_find(), and to_expr().
valuest value_set_fivrt::temporary_values |
Definition at line 303 of file value_set_fivr.h.
Referenced by do_function_call(), get_temporary_entry(), and handover().
unsigned value_set_fivrt::to_function |
Definition at line 33 of file value_set_fivr.h.
Referenced by do_function_call(), value_set_analysis_fivrt::get_values(), handover(), and insert_to().
unsigned value_set_fivrt::to_target_index |
Definition at line 34 of file value_set_fivr.h.
Referenced by do_function_call(), value_set_analysis_fivrt::get_values(), handover(), and insert_to().
valuest value_set_fivrt::values |
Definition at line 302 of file value_set_fivr.h.
Referenced by assign_rec(), clear(), do_free(), do_function_call(), flatten_rec(), get_entry(), get_reference_set(), get_reference_set_sharing_rec(), get_value_set(), get_value_set_rec(), handover(), make_any(), output(), and recursive_find().