cprover
custom_bitvector_domaint Class Reference

#include <custom_bitvector_analysis.h>

Inheritance diagram for custom_bitvector_domaint:
[legend]
Collaboration diagram for custom_bitvector_domaint:
[legend]

Classes

struct  vectorst
 

Public Types

typedef unsigned long long bit_vectort
 
typedef std::map< irep_idt, bit_vectortbitst
 
- Public Types inherited from ai_domain_baset
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
 
- Public Member Functions inherited from 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
 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

- Protected Member Functions inherited from ai_domain_baset
 ai_domain_baset ()
 The constructor is expected to produce 'false' or 'bottom'. More...
 

Detailed Description

Definition at line 23 of file custom_bitvector_analysis.h.

Member Typedef Documentation

◆ bit_vectort

typedef unsigned long long custom_bitvector_domaint::bit_vectort

Definition at line 75 of file custom_bitvector_analysis.h.

◆ bitst

Definition at line 77 of file custom_bitvector_analysis.h.

Member Enumeration Documentation

◆ modet

enum custom_bitvector_domaint::modet
strongprivate
Enumerator
SET_MUST 
CLEAR_MUST 
SET_MAY 
CLEAR_MAY 

Definition at line 121 of file custom_bitvector_analysis.h.

Constructor & Destructor Documentation

◆ custom_bitvector_domaint()

custom_bitvector_domaint::custom_bitvector_domaint ( )
inline

Definition at line 111 of file custom_bitvector_analysis.h.

Member Function Documentation

◆ assign_lhs() [1/2]

void custom_bitvector_domaint::assign_lhs ( const exprt lhs,
const vectorst vectors 
)

Definition at line 108 of file custom_bitvector_analysis.cpp.

References object2id().

Referenced by assign_struct_rec(), and transform().

◆ assign_lhs() [2/2]

void custom_bitvector_domaint::assign_lhs ( const irep_idt identifier,
const vectorst vectors 
)

◆ assign_struct_rec()

void custom_bitvector_domaint::assign_struct_rec ( locationt  from,
const exprt lhs,
const exprt rhs,
custom_bitvector_analysist cba,
const namespacet ns 
)

◆ clear_bit()

static void custom_bitvector_domaint::clear_bit ( bit_vectort dest,
unsigned  bit_nr 
)
inlinestaticprivate

Definition at line 131 of file custom_bitvector_analysis.h.

Referenced by set_bit(), and transform().

◆ erase_blank_vectors()

void custom_bitvector_domaint::erase_blank_vectors ( bitst bits)
private

erase blank bitvectors

Definition at line 657 of file custom_bitvector_analysis.cpp.

Referenced by merge(), and transform().

◆ eval()

◆ get_bit()

static bool custom_bitvector_domaint::get_bit ( const bit_vectort  src,
unsigned  bit_nr 
)
inlinestaticprivate

Definition at line 137 of file custom_bitvector_analysis.h.

Referenced by eval().

◆ get_rhs() [1/2]

custom_bitvector_domaint::vectorst custom_bitvector_domaint::get_rhs ( const exprt rhs) const

◆ get_rhs() [2/2]

custom_bitvector_domaint::vectorst custom_bitvector_domaint::get_rhs ( const irep_idt identifier) const

◆ has_get_must_or_may()

bool custom_bitvector_domaint::has_get_must_or_may ( const exprt src)
static

◆ is_bottom()

bool custom_bitvector_domaint::is_bottom ( ) const
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.

◆ is_top()

bool custom_bitvector_domaint::is_top ( ) const
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.

◆ make_bottom()

void custom_bitvector_domaint::make_bottom ( )
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().

◆ make_entry()

void custom_bitvector_domaint::make_entry ( )
inlinefinaloverridevirtual

a reasonable entry-point state

Implements ai_domain_baset.

Definition at line 49 of file custom_bitvector_analysis.h.

References make_top().

◆ make_top()

void custom_bitvector_domaint::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().

◆ merge() [1/2]

bool custom_bitvector_domaint::merge ( const custom_bitvector_domaint b,
locationt  from,
locationt  to 
)

◆ merge() [2/2]

static vectorst custom_bitvector_domaint::merge ( const vectorst a,
const vectorst b 
)
inlinestatic

◆ object2id()

◆ output()

void custom_bitvector_domaint::output ( std::ostream &  out,
const ai_baset ai,
const namespacet ns 
) const
finaloverridevirtual

◆ set_bit() [1/3]

void custom_bitvector_domaint::set_bit ( const exprt lhs,
unsigned  bit_nr,
modet  mode 
)
private

Definition at line 46 of file custom_bitvector_analysis.cpp.

References object2id().

Referenced by set_bit(), and transform().

◆ set_bit() [2/3]

void custom_bitvector_domaint::set_bit ( const irep_idt identifier,
unsigned  bit_nr,
modet  mode 
)
private

◆ set_bit() [3/3]

static void custom_bitvector_domaint::set_bit ( bit_vectort dest,
unsigned  bit_nr 
)
inlinestaticprivate

Definition at line 126 of file custom_bitvector_analysis.h.

◆ transform()

void custom_bitvector_domaint::transform ( locationt  from,
locationt  to,
ai_baset ai,
const namespacet ns 
)
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.

Member Data Documentation

◆ has_values

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().

◆ may_bits

bitst custom_bitvector_domaint::may_bits

◆ must_bits

bitst custom_bitvector_domaint::must_bits

The documentation for this class was generated from the following files: