cprover
|
#include <custom_bitvector_analysis.h>
Classes | |
struct | vectorst |
Public Types | |
typedef unsigned long long | bit_vectort |
typedef std::map< irep_idt, bit_vectort > | bitst |
![]() | |
typedef goto_programt::const_targett | locationt |
Public Member Functions | |
void | transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns) final override |
void | output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override |
void | make_bottom () final override |
void | make_top () final override |
void | make_entry () final override |
bool | is_bottom () const final override |
bool | is_top () const final override |
bool | merge (const custom_bitvector_domaint &b, locationt from, locationt to) |
void | assign_struct_rec (locationt from, const exprt &lhs, const exprt &rhs, custom_bitvector_analysist &, const namespacet &) |
void | assign_lhs (const exprt &, const vectorst &) |
void | assign_lhs (const irep_idt &, const vectorst &) |
vectorst | get_rhs (const exprt &) const |
vectorst | get_rhs (const irep_idt &) const |
custom_bitvector_domaint () | |
exprt | eval (const exprt &src, custom_bitvector_analysist &) const |
![]() | |
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 (exprt &condition, 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... | |
Static Public Member Functions | |
static vectorst | merge (const vectorst &a, const vectorst &b) |
static bool | has_get_must_or_may (const exprt &) |
Public Attributes | |
bitst | may_bits |
bitst | must_bits |
tvt | has_values |
Private Types | |
enum | modet { modet::SET_MUST, modet::CLEAR_MUST, modet::SET_MAY, modet::CLEAR_MAY } |
Private Member Functions | |
void | set_bit (const exprt &, unsigned bit_nr, modet) |
void | set_bit (const irep_idt &, unsigned bit_nr, modet) |
void | erase_blank_vectors (bitst &) |
erase blank bitvectors More... | |
Static Private Member Functions | |
static void | set_bit (bit_vectort &dest, unsigned bit_nr) |
static void | clear_bit (bit_vectort &dest, unsigned bit_nr) |
static bool | get_bit (const bit_vectort src, unsigned bit_nr) |
static irep_idt | object2id (const exprt &) |
Definition at line 23 of file custom_bitvector_analysis.h.
typedef unsigned long long custom_bitvector_domaint::bit_vectort |
Definition at line 75 of file custom_bitvector_analysis.h.
typedef std::map<irep_idt, bit_vectort> custom_bitvector_domaint::bitst |
Definition at line 77 of file custom_bitvector_analysis.h.
|
strongprivate |
Enumerator | |
---|---|
SET_MUST | |
CLEAR_MUST | |
SET_MAY | |
CLEAR_MAY |
Definition at line 121 of file custom_bitvector_analysis.h.
|
inline |
Definition at line 111 of file custom_bitvector_analysis.h.
Definition at line 108 of file custom_bitvector_analysis.cpp.
References object2id().
Referenced by assign_struct_rec(), and transform().
Definition at line 117 of file custom_bitvector_analysis.cpp.
References custom_bitvector_domaint::vectorst::may_bits, may_bits, custom_bitvector_domaint::vectorst::must_bits, and must_bits.
void custom_bitvector_domaint::assign_struct_rec | ( | locationt | from, |
const exprt & | lhs, | ||
const exprt & | rhs, | ||
custom_bitvector_analysist & | cba, | ||
const namespacet & | ns | ||
) |
Definition at line 227 of file custom_bitvector_analysis.cpp.
References custom_bitvector_analysist::aliases(), assign_lhs(), struct_union_typet::components(), namespace_baset::follow(), get_rhs(), irept::id(), to_struct_type(), and exprt::type().
Referenced by transform().
|
inlinestaticprivate |
Definition at line 131 of file custom_bitvector_analysis.h.
Referenced by set_bit(), and transform().
|
private |
erase blank bitvectors
Definition at line 655 of file custom_bitvector_analysis.cpp.
Referenced by merge(), and transform().
exprt custom_bitvector_domaint::eval | ( | const exprt & | src, |
custom_bitvector_analysist & | custom_bitvector_analysis | ||
) | const |
Definition at line 681 of file custom_bitvector_analysis.cpp.
References Forall_operands, get_bit(), custom_bitvector_analysist::get_bit_nr(), get_rhs(), constant_exprt::get_value(), irept::id(), exprt::is_constant(), custom_bitvector_domaint::vectorst::may_bits, may_bits, custom_bitvector_domaint::vectorst::must_bits, exprt::op0(), exprt::op1(), exprt::operands(), to_constant_expr(), and exprt::type().
Referenced by custom_bitvector_analysist::eval(), and transform().
|
inlinestaticprivate |
Definition at line 137 of file custom_bitvector_analysis.h.
Referenced by eval().
custom_bitvector_domaint::vectorst custom_bitvector_domaint::get_rhs | ( | const exprt & | rhs | ) | const |
Definition at line 151 of file custom_bitvector_analysis.cpp.
References irept::id(), merge(), object2id(), to_if_expr(), and to_typecast_expr().
Referenced by assign_struct_rec(), eval(), and transform().
custom_bitvector_domaint::vectorst custom_bitvector_domaint::get_rhs | ( | const irep_idt & | identifier | ) | const |
Definition at line 135 of file custom_bitvector_analysis.cpp.
References custom_bitvector_domaint::vectorst::may_bits, may_bits, custom_bitvector_domaint::vectorst::must_bits, and must_bits.
|
static |
Definition at line 668 of file custom_bitvector_analysis.cpp.
References forall_operands, and irept::id().
Referenced by custom_bitvector_analysist::check(), taint_analysist::operator()(), and transform().
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 54 of file custom_bitvector_analysis.h.
References DATA_INVARIANT, has_values, tvt::is_false(), may_bits, and must_bits.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 62 of file custom_bitvector_analysis.h.
References DATA_INVARIANT, has_values, tvt::is_true(), may_bits, and must_bits.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 35 of file custom_bitvector_analysis.h.
References has_values, may_bits, and must_bits.
Referenced by transform().
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 49 of file custom_bitvector_analysis.h.
References make_top().
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 42 of file custom_bitvector_analysis.h.
References has_values, may_bits, and must_bits.
Referenced by make_entry().
bool custom_bitvector_domaint::merge | ( | const custom_bitvector_domaint & | b, |
locationt | from, | ||
locationt | to | ||
) |
Definition at line 590 of file custom_bitvector_analysis.cpp.
References erase_blank_vectors(), has_values, tvt::is_false(), may_bits, must_bits, and tvt::unknown().
Referenced by get_rhs().
|
inlinestatic |
Definition at line 87 of file custom_bitvector_analysis.h.
References custom_bitvector_domaint::vectorst::may_bits, and custom_bitvector_domaint::vectorst::must_bits.
Definition at line 56 of file custom_bitvector_analysis.cpp.
References dstringt::empty(), symbol_exprt::get_identifier(), irept::id(), id2string(), unary_exprt::op(), dereference_exprt::pointer(), to_address_of_expr(), to_dereference_expr(), to_member_expr(), to_symbol_expr(), and to_typecast_expr().
Referenced by assign_lhs(), get_rhs(), and set_bit().
|
finaloverridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 543 of file custom_bitvector_analysis.cpp.
References custom_bitvector_analysist::bits, has_values, tvt::is_known(), may_bits, must_bits, template_numberingt< Map >::size(), and tvt::to_string().
Definition at line 46 of file custom_bitvector_analysis.cpp.
References object2id().
Referenced by set_bit(), and transform().
|
private |
Definition at line 21 of file custom_bitvector_analysis.cpp.
References clear_bit(), CLEAR_MAY, CLEAR_MUST, may_bits, must_bits, set_bit(), SET_MAY, and SET_MUST.
|
inlinestaticprivate |
Definition at line 126 of file custom_bitvector_analysis.h.
|
finaloverridevirtual |
Implements ai_domain_baset.
Definition at line 270 of file custom_bitvector_analysis.cpp.
References custom_bitvector_analysist::aliases(), code_function_callt::arguments(), ASSIGN, assign_lhs(), assign_struct_rec(), clear_bit(), CLEAR_MAY, CLEAR_MUST, goto_programt::instructiont::code, DEAD, DECL, dstringt::empty(), erase_blank_vectors(), eval(), code_function_callt::function(), FUNCTION_CALL, custom_bitvector_analysist::get_bit_nr(), symbol_exprt::get_identifier(), get_rhs(), codet::get_statement(), constant_exprt::get_value(), GOTO, goto_programt::instructiont::guard, has_get_must_or_may(), irept::id(), exprt::is_constant(), exprt::is_false(), code_assignt::lhs(), namespacet::lookup(), make_bottom(), exprt::make_not(), may_bits, must_bits, exprt::op0(), exprt::op1(), exprt::operands(), OTHER, code_typet::parameters(), code_assignt::rhs(), set_bit(), SET_MAY, SET_MUST, simplify_expr(), code_declt::symbol(), code_deadt::symbol(), to_code_assign(), to_code_dead(), to_code_decl(), to_code_function_call(), to_code_type(), to_constant_expr(), to_symbol_expr(), exprt::type(), goto_programt::instructiont::type, and UNREACHABLE.
tvt custom_bitvector_domaint::has_values |
Definition at line 109 of file custom_bitvector_analysis.h.
Referenced by is_bottom(), is_top(), make_bottom(), make_top(), merge(), and output().
bitst custom_bitvector_domaint::may_bits |
Definition at line 95 of file custom_bitvector_analysis.h.
Referenced by assign_lhs(), eval(), get_rhs(), is_bottom(), is_top(), make_bottom(), make_top(), merge(), output(), set_bit(), and transform().
bitst custom_bitvector_domaint::must_bits |
Definition at line 95 of file custom_bitvector_analysis.h.
Referenced by assign_lhs(), get_rhs(), is_bottom(), is_top(), make_bottom(), make_top(), merge(), output(), set_bit(), and transform().