cprover
constant_propagator_domaint Class Reference

#include <constant_propagator.h>

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

Classes

struct  valuest
 

Public Member Functions

virtual void transform (locationt from, locationt to, ai_baset &ai_base, 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...
 
virtual void output (std::ostream &out, const ai_baset &ai_base, const namespacet &ns) const override
 
bool merge (const constant_propagator_domaint &other, locationt from, locationt to)
 
virtual bool ai_simplify (exprt &condition, const namespacet &ns) const final override
 Simplify the condition given context-sensitive knowledge from the abstract state. More...
 
virtual void make_bottom () final override
 no states More...
 
virtual void make_top () final override
 all states – the analysis doesn't use this, and domains may refuse to implement it. More...
 
virtual void make_entry () final override
 a reasonable entry-point state More...
 
virtual bool is_bottom () const final override
 
virtual bool is_top () const final override
 
bool partial_evaluate (exprt &expr, const namespacet &ns) const
 Attempt to evaluate expression using domain knowledge This function changes the expression that is passed into it. More...
 
- 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_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...
 

Public Attributes

valuest values
 

Protected Member Functions

void assign_rec (valuest &values, const exprt &lhs, const exprt &rhs, const namespacet &ns, const constant_propagator_ait *cp)
 
bool two_way_propagate_rec (const exprt &expr, const namespacet &ns, const constant_propagator_ait *cp)
 handles equalities and conjunctions containing equalities More...
 
bool partial_evaluate_with_all_rounding_modes (exprt &expr, const namespacet &ns) const
 Attempt to evaluate an expression in all rounding modes. More...
 
bool replace_constants_and_simplify (exprt &expr, const namespacet &ns) const
 
- Protected Member Functions inherited from ai_domain_baset
 ai_domain_baset ()
 The constructor is expected to produce 'false' or 'bottom'. More...
 

Additional Inherited Members

- Public Types inherited from ai_domain_baset
typedef goto_programt::const_targett locationt
 

Detailed Description

Definition at line 23 of file constant_propagator.h.

Member Function Documentation

◆ ai_simplify()

bool constant_propagator_domaint::ai_simplify ( exprt condition,
const namespacet ns 
) const
finaloverridevirtual

Simplify the condition given context-sensitive knowledge from the abstract state.

parameters: The condition to simplify and its namespace.
Returns
The simplified condition.

Reimplemented from ai_domain_baset.

Definition at line 282 of file constant_propagator.cpp.

References partial_evaluate().

◆ assign_rec()

◆ is_bottom()

◆ is_top()

virtual bool constant_propagator_domaint::is_top ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 66 of file constant_propagator.h.

References constant_propagator_domaint::valuest::is_top(), and values.

◆ make_bottom()

virtual void constant_propagator_domaint::make_bottom ( )
inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 46 of file constant_propagator.h.

References constant_propagator_domaint::valuest::set_to_bottom(), and values.

◆ make_entry()

virtual void constant_propagator_domaint::make_entry ( )
inlinefinaloverridevirtual

a reasonable entry-point state

Implements ai_domain_baset.

Definition at line 56 of file constant_propagator.h.

References make_top().

◆ make_top()

virtual void constant_propagator_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 51 of file constant_propagator.h.

References constant_propagator_domaint::valuest::set_to_top(), and values.

Referenced by make_entry().

◆ merge()

bool constant_propagator_domaint::merge ( const constant_propagator_domaint other,
locationt  from,
locationt  to 
)
Returns
Return true if "this" has changed.

Definition at line 515 of file constant_propagator.cpp.

References constant_propagator_domaint::valuest::merge(), and values.

◆ output()

void constant_propagator_domaint::output ( std::ostream &  out,
const ai_baset ai_base,
const namespacet ns 
) const
overridevirtual

Reimplemented from ai_domain_baset.

Definition at line 398 of file constant_propagator.cpp.

References constant_propagator_domaint::valuest::output(), and values.

Referenced by transform().

◆ partial_evaluate()

bool constant_propagator_domaint::partial_evaluate ( exprt expr,
const namespacet ns 
) const

Attempt to evaluate expression using domain knowledge This function changes the expression that is passed into it.

Parameters
exprThe expression to evaluate
nsThe namespace for symbols in the expression
Returns
True if the expression is unchanged, false otherwise

Definition at line 528 of file constant_propagator.cpp.

References ID_cprover_rounding_mode_str, constant_propagator_domaint::valuest::is_constant(), partial_evaluate_with_all_rounding_modes(), replace_constants_and_simplify(), and values.

Referenced by ai_simplify(), assign_rec(), constant_propagator_ait::replace(), and transform().

◆ partial_evaluate_with_all_rounding_modes()

bool constant_propagator_domaint::partial_evaluate_with_all_rounding_modes ( exprt expr,
const namespacet ns 
) const
protected

Attempt to evaluate an expression in all rounding modes.

If the result is the same for all rounding modes, change expr to that result and return false. Otherwise, return true.

Definition at line 546 of file constant_propagator.cpp.

References from_integer(), ID_cprover_rounding_mode_str, replace_constants_and_simplify(), ieee_floatt::ROUND_TO_EVEN, ieee_floatt::ROUND_TO_MINUS_INF, ieee_floatt::ROUND_TO_PLUS_INF, ieee_floatt::ROUND_TO_ZERO, constant_propagator_domaint::valuest::set_to(), and values.

Referenced by partial_evaluate().

◆ replace_constants_and_simplify()

bool constant_propagator_domaint::replace_constants_and_simplify ( exprt expr,
const namespacet ns 
) const
protected

◆ transform()

void constant_propagator_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 60 of file constant_propagator.cpp.

References code_function_callt::arguments(), assign_rec(), CPROVER_PREFIX, constant_propagator_ait::dirty, code_function_callt::function(), symbol_exprt::get_identifier(), INVARIANT, constant_propagator_domaint::valuest::is_bottom, exprt::is_false(), code_assignt::lhs(), namespacet::lookup(), output(), code_typet::parameters(), partial_evaluate(), code_assignt::rhs(), constant_propagator_domaint::valuest::set_dirty_to_top(), constant_propagator_domaint::valuest::set_to_bottom(), constant_propagator_domaint::valuest::set_to_top(), code_declt::symbol(), code_deadt::symbol(), to_code_assign(), to_code_dead(), to_code_decl(), to_code_function_call(), to_code_type(), to_symbol_expr(), two_way_propagate_rec(), symbolt::type, and values.

◆ two_way_propagate_rec()

bool constant_propagator_domaint::two_way_propagate_rec ( const exprt expr,
const namespacet ns,
const constant_propagator_ait cp 
)
protected

Member Data Documentation

◆ values


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