cprover
rd_range_domaint Class Reference

#include <reaching_definitions.h>

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

Public Types

typedef std::multimap< range_spect, range_spectrangest
 
typedef std::map< locationt, rangestranges_at_loct
 
- Public Types inherited from ai_domain_baset
typedef goto_programt::const_targett locationt
 

Public Member Functions

 rd_range_domaint ()
 
void set_bitvector_container (sparse_bitvector_analysist< reaching_definitiont > &_bv_container)
 
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 &, const namespacet &) const final override
 
void make_top () final override
 all states – the analysis doesn't use this, and domains may refuse to implement it. More...
 
void make_bottom () final override
 no states More...
 
void make_entry () final override
 a reasonable entry-point state More...
 
bool is_top () const override final
 
bool is_bottom () const override final
 
bool merge (const rd_range_domaint &other, locationt from, locationt to)
 
bool merge_shared (const rd_range_domaint &other, locationt from, locationt to, const namespacet &ns)
 
const ranges_at_loctget (const irep_idt &identifier) const
 
void clear_cache (const irep_idt &identifier) 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...
 

Private Types

typedef std::set< std::size_t > values_innert
 
typedef std::unordered_map< irep_idt, values_innertvaluest
 
typedef std::unordered_map< irep_idt, ranges_at_loctexport_cachet
 

Private Member Functions

void populate_cache (const irep_idt &identifier) const
 
void transform_dead (const namespacet &ns, locationt from)
 
void transform_start_thread (const namespacet &ns, reaching_definitions_analysist &rd)
 
void transform_function_call (const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
 
void transform_end_function (const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
 
void transform_assign (const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
 
void kill (const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
 
void kill_inf (const irep_idt &identifier, const range_spect &range_start)
 
bool gen (locationt from, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
 
void output (std::ostream &out) const
 
bool merge_inner (values_innert &dest, const values_innert &other)
 

Private Attributes

tvt has_values
 
sparse_bitvector_analysist< reaching_definitiont > * bv_container
 
valuest values
 
export_cachet export_cache
 

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 100 of file reaching_definitions.h.

Member Typedef Documentation

◆ export_cachet

typedef std::unordered_map<irep_idt, ranges_at_loct> rd_range_domaint::export_cachet
private

Definition at line 201 of file reaching_definitions.h.

◆ ranges_at_loct

Definition at line 177 of file reaching_definitions.h.

◆ rangest

Definition at line 176 of file reaching_definitions.h.

◆ values_innert

typedef std::set<std::size_t> rd_range_domaint::values_innert
private

Definition at line 190 of file reaching_definitions.h.

◆ valuest

typedef std::unordered_map<irep_idt, values_innert> rd_range_domaint::valuest
private

Definition at line 194 of file reaching_definitions.h.

Constructor & Destructor Documentation

◆ rd_range_domaint()

rd_range_domaint::rd_range_domaint ( )
inline

Definition at line 103 of file reaching_definitions.h.

Member Function Documentation

◆ clear_cache()

void rd_range_domaint::clear_cache ( const irep_idt identifier) const
inline

Definition at line 180 of file reaching_definitions.h.

References export_cache.

Referenced by output().

◆ gen()

◆ get()

const rd_range_domaint::ranges_at_loct & rd_range_domaint::get ( const irep_idt identifier) const

Definition at line 714 of file reaching_definitions.cpp.

References export_cache, and populate_cache().

◆ is_bottom()

bool rd_range_domaint::is_bottom ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 156 of file reaching_definitions.h.

References DATA_INVARIANT, has_values, tvt::is_false(), and values.

◆ is_top()

bool rd_range_domaint::is_top ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 149 of file reaching_definitions.h.

References DATA_INVARIANT, has_values, tvt::is_true(), and values.

◆ kill()

void rd_range_domaint::kill ( const irep_idt identifier,
const range_spect range_start,
const range_spect range_end 
)
private

◆ kill_inf()

void rd_range_domaint::kill_inf ( const irep_idt identifier,
const range_spect range_start 
)
private

Definition at line 432 of file reaching_definitions.cpp.

References values.

Referenced by kill().

◆ make_bottom()

void rd_range_domaint::make_bottom ( )
inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 136 of file reaching_definitions.h.

References bv_container, sparse_bitvector_analysist< V >::clear(), has_values, and values.

◆ make_entry()

void rd_range_domaint::make_entry ( )
inlinefinaloverridevirtual

a reasonable entry-point state

Implements ai_domain_baset.

Definition at line 144 of file reaching_definitions.h.

References make_top().

◆ make_top()

void rd_range_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 128 of file reaching_definitions.h.

References bv_container, sparse_bitvector_analysist< V >::clear(), has_values, and values.

Referenced by make_entry().

◆ merge()

bool rd_range_domaint::merge ( const rd_range_domaint other,
locationt  from,
locationt  to 
)
Returns
returns true iff there is something new

Definition at line 629 of file reaching_definitions.cpp.

References export_cache, has_values, tvt::is_false(), merge_inner(), tvt::unknown(), and values.

◆ merge_inner()

bool rd_range_domaint::merge_inner ( values_innert dest,
const values_innert other 
)
private
Returns
returns true iff there is something new

Definition at line 578 of file reaching_definitions.cpp.

References gen().

Referenced by merge(), and merge_shared().

◆ merge_shared()

bool rd_range_domaint::merge_shared ( const rd_range_domaint other,
locationt  from,
locationt  to,
const namespacet ns 
)
Returns
returns true iff there is something new

Definition at line 665 of file reaching_definitions.cpp.

References export_cache, has_values, tvt::is_false(), namespacet::lookup(), merge_inner(), tvt::unknown(), and values.

◆ output() [1/2]

void rd_range_domaint::output ( std::ostream &  out,
const ai_baset ,
const namespacet  
) const
inlinefinaloverridevirtual

Reimplemented from ai_domain_baset.

Definition at line 120 of file reaching_definitions.h.

◆ output() [2/2]

void rd_range_domaint::output ( std::ostream &  out) const
private

◆ populate_cache()

void rd_range_domaint::populate_cache ( const irep_idt identifier) const
private

◆ set_bitvector_container()

void rd_range_domaint::set_bitvector_container ( sparse_bitvector_analysist< reaching_definitiont > &  _bv_container)
inline

Definition at line 110 of file reaching_definitions.h.

References bv_container.

Referenced by reaching_definitions_analysist::get_state().

◆ transform()

void rd_range_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 58 of file reaching_definitions.cpp.

References bv_container, forall_rw_range_set_w_objects, reaching_definitions_analysist::get_is_dirty(), reaching_definitions_analysist::get_is_threaded(), reaching_definitions_analysist::get_value_sets(), goto_rw(), INVARIANT_STRUCTURED, irept::is_not_nil(), symbolt::is_shared(), kill(), code_function_callt::lhs(), namespacet::lookup(), to_code_function_call(), transform_assign(), transform_dead(), transform_end_function(), transform_function_call(), and transform_start_thread().

◆ transform_assign()

◆ transform_dead()

void rd_range_domaint::transform_dead ( const namespacet ns,
locationt  from 
)
private

Definition at line 127 of file reaching_definitions.cpp.

References export_cache, code_deadt::symbol(), to_code_dead(), to_symbol_expr(), and values.

Referenced by transform().

◆ transform_end_function()

◆ transform_function_call()

◆ transform_start_thread()

void rd_range_domaint::transform_start_thread ( const namespacet ns,
reaching_definitions_analysist rd 
)
private

Member Data Documentation

◆ bv_container

◆ export_cache

◆ has_values

tvt rd_range_domaint::has_values
private

◆ values


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