#include <constant_propagator.h>

Inheritance diagram for constant_propagator_domaint:

Collaboration diagram for constant_propagator_domaint:

Classes
struct	valuest

Public Member Functions
virtual void	transform (const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_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, trace_ptrt from, trace_ptrt 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 directly (see make_entry) and domains may refuse to implement it. More...

virtual bool	is_bottom () const final override

virtual bool	is_top () const final override

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 void	make_entry ()
	Make this domain a reasonable entry-point state For most domains top is sufficient. 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 bool	partial_evaluate (const valuest &known_values, exprt &expr, const namespacet &ns)
	Attempt to evaluate expression using domain knowledge This function changes the expression that is passed into it. More...

Public Attributes
valuest	values

Protected Member Functions
bool	two_way_propagate_rec (const exprt &expr, const namespacet &ns, const constant_propagator_ait *cp)
	handles equalities and conjunctions containing equalities More...

Protected Member Functions inherited from ai_domain_baset
	ai_domain_baset ()
	The constructor is expected to produce 'false' or 'bottom' A default constructor is not part of the domain interface. More...

	ai_domain_baset (const ai_domain_baset &old)
	A copy constructor is part of the domain interface. More...

Static Protected Member Functions
static void	assign_rec (valuest &dest_values, const exprt &lhs, const exprt &rhs, const namespacet &ns, const constant_propagator_ait *cp, bool is_assignment)
	Assign value `rhs` to `lhs`, recording any newly-known constants in `dest_values`. More...

static bool	partial_evaluate_with_all_rounding_modes (const valuest &known_values, exprt &expr, const namespacet &ns)
	Attempt to evaluate an expression in all rounding modes. More...

static bool	replace_constants_and_simplify (const valuest &known_values, exprt &expr, const namespacet &ns)

Additional Inherited Members
Public Types inherited from ai_domain_baset
typedef goto_programt::const_targett	locationt

typedef ai_history_baset::trace_ptrt	trace_ptrt

Detailed Description

Definition at line 33 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 412 of file constant_propagator.cpp.

◆ assign_rec()

void constant_propagator_domaint::assign_rec	(	valuest &	dest_values,
		const exprt &	lhs,
		const exprt &	rhs,
		const namespacet &	ns,
		const constant_propagator_ait *	cp,
		bool	is_assignment
	)

staticprotected

Assign value rhs to lhs, recording any newly-known constants in dest_values.

Parameters

[out]	dest_values	results of the assignment are recorded here. We might add extra entries (if we determine some symbol is constant), or might remove existing ones (if the lhs expression is unknown), except if `is_assignment` is false, in which case only the former is done.
	lhs	lhs expression to assign
	rhs	rhs expression to assign to lhs
	ns	namespace, used to check for type mismatches
	cp	owning constant propagator instance, used to filter out symbols that the user doesn't want tracked
	is_assignment	if true, assign_rec may remove entries from dest_values when a constant assignment cannot be determined. This is used when an actual assignment instruction is processed. If false, new entries can be added but existing ones will not be removed; this is used when the "assignment" is actually implied by a read-only operation, such as passing "IF x == y" – if we know what 'y' is that tells us the value for x, but if we don't there is no reason to discard pre-existing knowledge about x.

Definition at line 52 of file constant_propagator.cpp.

◆ is_bottom()

virtual bool constant_propagator_domaint::is_bottom ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 68 of file constant_propagator.h.

◆ is_top()

virtual bool constant_propagator_domaint::is_top ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 73 of file constant_propagator.h.

◆ make_bottom()

virtual void constant_propagator_domaint::make_bottom ( )

inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 58 of file constant_propagator.h.

◆ make_top()

virtual void constant_propagator_domaint::make_top ( )

inlinefinaloverridevirtual

all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implement it.

Implements ai_domain_baset.

Definition at line 63 of file constant_propagator.h.

◆ merge()

bool constant_propagator_domaint::merge	(	const constant_propagator_domaint &	other,
		trace_ptrt	from,
		trace_ptrt	to
	)

Returns: Return true if "this" has changed.

Definition at line 644 of file constant_propagator.cpp.

◆ 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 525 of file constant_propagator.cpp.

◆ partial_evaluate()

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

static

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

Parameters

known_values	The constant values under which to evaluate `expr`
expr	The expression to evaluate
ns	The namespace for symbols in the expression

Returns: True if the expression is unchanged, false otherwise

Definition at line 658 of file constant_propagator.cpp.

◆ partial_evaluate_with_all_rounding_modes()

bool constant_propagator_domaint::partial_evaluate_with_all_rounding_modes	(	const valuest &	known_values,
		exprt &	expr,
		const namespacet &	ns
	)

staticprotected

Attempt to evaluate an expression in all rounding modes.

Parameters

known_values	The constant values under which to evaluate `expr`
expr	The expression to evaluate
ns	The namespace for symbols in the expression

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

Definition at line 679 of file constant_propagator.cpp.

◆ replace_constants_and_simplify()

bool constant_propagator_domaint::replace_constants_and_simplify	(	const valuest &	known_values,
		exprt &	expr,
		const namespacet &	ns
	)

staticprotected

Definition at line 716 of file constant_propagator.cpp.

◆ transform()

void constant_propagator_domaint::transform	(	const irep_idt &	function_from,
		trace_ptrt	from,
		const irep_idt &	function_to,
		trace_ptrt	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)

in some cases, function calls are skipped, in which case: c) there is an edge from the call instruction to the instruction after

"this" is the domain before the instruction "from" "from" is the instruction to be interpreted "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())

The history aware version is used by the abstract interpreter for backwards compatability it calls the older signature

Implements ai_domain_baset.

Definition at line 124 of file constant_propagator.cpp.

◆ two_way_propagate_rec()

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

protected

handles equalities and conjunctions containing equalities

Definition at line 308 of file constant_propagator.cpp.

Member Data Documentation

◆ values

valuest constant_propagator_domaint::values

Definition at line 133 of file constant_propagator.h.

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

/home/runner/work/cbmc/cbmc/src/analyses/constant_propagator.h
/home/runner/work/cbmc/cbmc/src/analyses/constant_propagator.cpp

Classes

Public Member Functions

Static Public Member Functions

Public Attributes

Protected Member Functions

Static Protected Member Functions

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ ai_simplify()

◆ assign_rec()

◆ is_bottom()

◆ is_top()

◆ make_bottom()

◆ make_top()

◆ merge()

◆ output()

◆ partial_evaluate()

◆ partial_evaluate_with_all_rounding_modes()

◆ replace_constants_and_simplify()

◆ transform()

◆ two_way_propagate_rec()

Member Data Documentation

◆ values