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 |
how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable) More... | |
void | output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override |
void | make_bottom () final override |
no states More... | |
void | make_top () final override |
all states – the analysis doesn't use this, and domains may refuse to implement it. More... | |
void | make_entry () final override |
a reasonable entry-point state More... | |
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 |
![]() | |
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 |
also add More... | |
virtual bool | ai_simplify_lhs (exprt &condition, const namespacet &ns) const |
Simplifies the expression but keeps it as an l-value. More... | |
virtual exprt | to_predicate (void) const |
Gives a Boolean condition that is true for all values represented by the domain. 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 &) |
Additional Inherited Members | |
![]() | |
ai_domain_baset () | |
The constructor is expected to produce 'false' or 'bottom'. More... | |
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 657 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 683 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 670 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 |
no states
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 |
a reasonable entry-point state
Implements ai_domain_baset.
Definition at line 49 of file custom_bitvector_analysis.h.
References make_top().
|
inlinefinaloverridevirtual |
all states – the analysis doesn't use this, and domains may refuse to implement it.
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 592 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 545 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 |
how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable)
"this" is the domain before the instruction "from" "from" is the instruction to be interpretted "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)
PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") PRECONDITION(are_comparable(from,to) || (from->is_function_call() || from->is_end_function())
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().