cprover
|
#include <invariant_set.h>
Public Types | |
typedef std::set< std::pair< unsigned, unsigned > > | ineq_sett |
typedef interval_templatet< mp_integer > | boundst |
typedef std::map< unsigned, boundst > | bounds_mapt |
Public Member Functions | |
invariant_sett () | |
void | output (const irep_idt &identifier, std::ostream &out) const |
bool | make_union (const invariant_sett &other_invariants) |
void | strengthen (const exprt &expr) |
void | make_true () |
void | make_false () |
void | make_threaded () |
void | apply_code (const codet &code) |
void | modifies (const exprt &lhs) |
void | assignment (const exprt &lhs, const exprt &rhs) |
void | set_value_sets (value_setst &_value_sets) |
void | set_object_store (inv_object_storet &_object_store) |
void | set_namespace (const namespacet &_ns) |
tvt | implies (const exprt &expr) const |
void | simplify (exprt &expr) const |
Static Public Member Functions | |
static void | intersection (ineq_sett &dest, const ineq_sett &other) |
static void | remove (ineq_sett &dest, unsigned a) |
Public Attributes | |
unsigned_union_find | eq_set |
ineq_sett | le_set |
ineq_sett | ne_set |
bounds_mapt | bounds_map |
bool | threaded |
bool | is_false |
Protected Member Functions | |
tvt | implies_rec (const exprt &expr) const |
void | strengthen_rec (const exprt &expr) |
void | add_type_bounds (const exprt &expr, const typet &type) |
void | add_bounds (unsigned a, const boundst &bound) |
void | get_bounds (unsigned a, boundst &dest) const |
bool | make_union_bounds_map (const bounds_mapt &other) |
void | modifies (unsigned a) |
std::string | to_string (unsigned a, const irep_idt &identifier) const |
bool | get_object (const exprt &expr, unsigned &n) const |
exprt | get_constant (const exprt &expr) const |
bool | has_eq (const std::pair< unsigned, unsigned > &p) const |
bool | has_le (const std::pair< unsigned, unsigned > &p) const |
bool | has_ne (const std::pair< unsigned, unsigned > &p) const |
tvt | is_eq (std::pair< unsigned, unsigned > p) const |
tvt | is_le (std::pair< unsigned, unsigned > p) const |
tvt | is_lt (std::pair< unsigned, unsigned > p) const |
tvt | is_ge (std::pair< unsigned, unsigned > p) const |
tvt | is_gt (std::pair< unsigned, unsigned > p) const |
tvt | is_ne (std::pair< unsigned, unsigned > p) const |
void | add (const std::pair< unsigned, unsigned > &p, ineq_sett &dest) |
void | add_le (const std::pair< unsigned, unsigned > &p) |
void | add_ne (const std::pair< unsigned, unsigned > &p) |
void | add_eq (const std::pair< unsigned, unsigned > &eq) |
void | add_eq (ineq_sett &dest, const std::pair< unsigned, unsigned > &eq, const std::pair< unsigned, unsigned > &ineq) |
Static Protected Member Functions | |
static void | nnf (exprt &expr, bool negate=false) |
Protected Attributes | |
value_setst * | value_sets |
inv_object_storet * | object_store |
const namespacet * | ns |
Definition at line 77 of file invariant_set.h.
typedef std::map<unsigned, boundst> invariant_sett::bounds_mapt |
Definition at line 92 of file invariant_set.h.
Definition at line 91 of file invariant_set.h.
typedef std::set<std::pair<unsigned, unsigned> > invariant_sett::ineq_sett |
Definition at line 84 of file invariant_set.h.
|
inline |
Definition at line 98 of file invariant_set.h.
|
protected |
Definition at line 180 of file invariant_set.cpp.
References unsigned_union_find::check_index(), eq_set, unsigned_union_find::find(), and unsigned_union_find::size().
|
inlineprotected |
Definition at line 210 of file invariant_set.h.
References bounds_map.
Referenced by add_type_bounds(), and strengthen_rec().
|
protected |
Definition at line 202 of file invariant_set.cpp.
References eq_set, unsigned_union_find::find(), inv_object_storet::is_constant(), le_set, make_false(), unsigned_union_find::make_union(), ne_set, object_store, r, and unsigned_union_find::size().
Referenced by strengthen_rec().
|
protected |
Definition at line 239 of file invariant_set.cpp.
|
inlineprotected |
Definition at line 274 of file invariant_set.h.
Referenced by strengthen_rec().
|
inlineprotected |
Definition at line 279 of file invariant_set.h.
Referenced by strengthen_rec().
Definition at line 363 of file invariant_set.cpp.
References add_bounds(), get_object(), bitvector_typet::get_width(), irept::id(), power(), to_unsignedbv_type(), and exprt::type().
Referenced by strengthen_rec().
void invariant_sett::apply_code | ( | const codet & | code | ) |
Definition at line 1078 of file invariant_set.cpp.
References assignment(), forall_operands, irept::get(), id2string(), make_true(), modifies(), exprt::op0(), exprt::op1(), exprt::operands(), irept::pretty(), and to_code().
Referenced by invariant_set_domaint::transform().
Definition at line 1059 of file invariant_set.cpp.
References binary_relation_exprt::lhs(), modifies(), ns, binary_relation_exprt::rhs(), simplify(), and strengthen().
Referenced by apply_code(), and invariant_set_domaint::transform().
|
protected |
Definition at line 682 of file invariant_set.cpp.
References bounds_map, inv_object_storet::get_expr(), irept::id(), lower_interval(), object_store, to_integer(), and exprt::type().
Referenced by implies_rec().
Definition at line 837 of file invariant_set.cpp.
References bounds_map, exprt::copy_to_operands(), eq_set, unsigned_union_find::find(), from_integer(), inv_object_storet::get_expr(), get_nil_irep(), get_object(), irept::id(), exprt::is_constant(), inv_object_storet::is_constant_address(), object_store, r, irept::set(), unsigned_union_find::size(), to_integer(), and exprt::type().
Referenced by simplify().
|
protected |
Definition at line 144 of file invariant_set.cpp.
References inv_object_storet::get(), object_store, and PRECONDITION.
Referenced by add_type_bounds(), get_constant(), implies_rec(), modifies(), and strengthen_rec().
|
inlineprotected |
Definition at line 233 of file invariant_set.h.
References eq_set, and unsigned_union_find::same_set().
Referenced by is_eq(), is_le(), and strengthen_rec().
|
inlineprotected |
|
inlineprotected |
Definition at line 243 of file invariant_set.h.
References ne_set.
Referenced by is_eq(), is_le(), and strengthen_rec().
Definition at line 591 of file invariant_set.cpp.
References implies_rec(), and nnf().
Referenced by invariant_propagationt::simplify().
Definition at line 598 of file invariant_set.cpp.
References forall_operands, from_expr(), get_bounds(), get_object(), irept::id(), is_eq(), is_false, is_le(), is_lt(), is_ne(), exprt::is_true(), ns, exprt::op0(), exprt::op1(), exprt::operands(), r, exprt::type(), and tvt::unknown().
Referenced by implies().
Definition at line 163 of file invariant_set.h.
Referenced by make_union().
|
protected |
Definition at line 277 of file invariant_set.cpp.
References has_eq(), has_ne(), and tvt::unknown().
Referenced by implies_rec(), is_ge(), is_lt(), and is_ne().
|
inlineprotected |
Definition at line 256 of file invariant_set.h.
|
inlineprotected |
Definition at line 262 of file invariant_set.h.
References is_le().
|
protected |
Definition at line 291 of file invariant_set.cpp.
References has_eq(), has_le(), has_ne(), and tvt::unknown().
Referenced by implies_rec(), is_gt(), and is_lt().
|
inlineprotected |
Definition at line 251 of file invariant_set.h.
References is_eq(), and is_le().
Referenced by implies_rec(), and is_ge().
|
inlineprotected |
|
inline |
Definition at line 124 of file invariant_set.h.
References unsigned_union_find::clear(), eq_set, is_false, le_set, and ne_set.
Referenced by add_eq(), invariant_propagationt::initialize(), invariant_set_domaint::make_bottom(), and strengthen_rec().
|
inline |
Definition at line 132 of file invariant_set.h.
References make_true(), and threaded.
Referenced by make_union(), and invariant_set_domaint::transform().
|
inline |
Definition at line 116 of file invariant_set.h.
References unsigned_union_find::clear(), eq_set, is_false, le_set, and ne_set.
Referenced by apply_code(), invariant_propagationt::initialize(), invariant_set_domaint::make_entry(), make_threaded(), invariant_set_domaint::make_top(), and modifies().
bool invariant_sett::make_union | ( | const invariant_sett & | other_invariants | ) |
Definition at line 908 of file invariant_set.cpp.
References bounds_map, unsigned_union_find::count_roots(), eq_set, unsigned_union_find::intersection(), intersection(), is_false, le_set, make_threaded(), make_union_bounds_map(), ne_set, and threaded.
Referenced by invariant_set_domaint::merge().
|
protected |
Definition at line 959 of file invariant_set.cpp.
References bounds_map.
Referenced by make_union().
void invariant_sett::modifies | ( | const exprt & | lhs | ) |
Definition at line 999 of file invariant_set.cpp.
References get_object(), irept::id(), irept::id_string(), make_true(), exprt::op0(), exprt::op1(), exprt::op2(), and exprt::operands().
Referenced by apply_code(), and assignment().
|
protected |
Definition at line 991 of file invariant_set.cpp.
References bounds_map, eq_set, unsigned_union_find::isolate(), le_set, and ne_set.
|
staticprotected |
Definition at line 706 of file invariant_set.cpp.
References Forall_operands, from_integer(), irept::id(), exprt::is_false(), exprt::is_true(), binary_relation_exprt::lhs(), exprt::make_not(), exprt::op0(), exprt::op1(), exprt::operands(), binary_relation_exprt::rhs(), irept::swap(), and exprt::type().
Referenced by implies(), and strengthen().
void invariant_sett::output | ( | const irep_idt & | identifier, |
std::ostream & | out | ||
) | const |
Definition at line 309 of file invariant_set.cpp.
References bounds_map, unsigned_union_find::count(), eq_set, unsigned_union_find::find(), INVARIANT_STRUCTURED, is_false, unsigned_union_find::is_root(), le_set, ne_set, object_store, unsigned_union_find::size(), and to_string().
Referenced by invariant_set_domaint::output().
|
inlinestatic |
Definition at line 179 of file invariant_set.h.
|
inline |
Definition at line 158 of file invariant_set.h.
References ns.
Referenced by invariant_propagationt::initialize().
|
inline |
Definition at line 153 of file invariant_set.h.
References object_store.
Referenced by invariant_propagationt::initialize().
|
inline |
Definition at line 148 of file invariant_set.h.
References value_sets.
Referenced by invariant_propagationt::initialize().
void invariant_sett::simplify | ( | exprt & | expr | ) | const |
Definition at line 819 of file invariant_set.cpp.
References Forall_operands, get_constant(), irept::id(), irept::is_not_nil(), and irept::swap().
Referenced by assignment(), and invariant_propagationt::simplify().
void invariant_sett::strengthen | ( | const exprt & | expr | ) |
Definition at line 383 of file invariant_set.cpp.
References nnf(), and strengthen_rec().
Referenced by assignment(), and invariant_set_domaint::transform().
|
protected |
Definition at line 390 of file invariant_set.cpp.
References add_bounds(), add_eq(), add_le(), add_ne(), add_type_bounds(), struct_union_typet::components(), exprt::copy_to_operands(), namespace_baset::follow(), forall_operands, from_expr(), get_object(), has_eq(), has_ne(), irept::id(), is_false, exprt::is_false(), exprt::is_true(), binary_relation_exprt::lhs(), lower_interval(), make_false(), ns, exprt::op0(), exprt::op1(), exprt::operands(), binary_relation_exprt::rhs(), irept::set(), to_integer(), to_struct_type(), exprt::type(), and upper_interval().
Referenced by strengthen().
|
protected |
Definition at line 900 of file invariant_set.cpp.
References object_store, PRECONDITION, and inv_object_storet::to_string().
Referenced by output().
bounds_mapt invariant_sett::bounds_map |
Definition at line 93 of file invariant_set.h.
Referenced by add_bounds(), get_bounds(), get_constant(), make_union(), make_union_bounds_map(), modifies(), and output().
unsigned_union_find invariant_sett::eq_set |
Definition at line 81 of file invariant_set.h.
Referenced by add(), add_eq(), get_constant(), has_eq(), make_false(), make_true(), make_union(), modifies(), and output().
bool invariant_sett::is_false |
Definition at line 96 of file invariant_set.h.
Referenced by implies_rec(), make_false(), make_true(), make_union(), output(), and strengthen_rec().
ineq_sett invariant_sett::le_set |
Definition at line 85 of file invariant_set.h.
Referenced by add_eq(), add_le(), has_le(), make_false(), make_true(), make_union(), modifies(), and output().
ineq_sett invariant_sett::ne_set |
Definition at line 88 of file invariant_set.h.
Referenced by add_eq(), add_ne(), has_ne(), make_false(), make_true(), make_union(), modifies(), and output().
|
protected |
Definition at line 202 of file invariant_set.h.
Referenced by assignment(), implies_rec(), set_namespace(), and strengthen_rec().
|
protected |
Definition at line 201 of file invariant_set.h.
Referenced by add_eq(), get_bounds(), get_constant(), get_object(), output(), set_object_store(), and to_string().
bool invariant_sett::threaded |
Definition at line 95 of file invariant_set.h.
Referenced by make_threaded(), and make_union().
|
protected |
Definition at line 200 of file invariant_set.h.
Referenced by set_value_sets().