Trivial, conjunctive interval domain for both float and integers. More...

#include <interval_domain.h>

Inheritance diagram for interval_domaint:

Public Types
using	integer_intervalt = interval_templatet<BigInt>
using	real_intervalt
using	interval
using	interval_map = std::unordered_map<irep_idt, interval, irep_id_hash>

Public Member Functions
	interval_domaint ()
void	transform (goto_programt::const_targett from, goto_programt::const_targett 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)
void	output (std::ostream &out) const override
void	dump () const
bool	merge (const interval_domaint &b, goto_programt::const_targett, goto_programt::const_targett to)
void	clear_state ()
void	make_bottom () final override
	no states
void	make_top () final override
	all states – the analysis doesn't use this, and domains may refuse to implement it.
void	make_entry () final override
	a reasonable entry-point state
bool	is_bottom () const override final
bool	is_top () const override final
expr2tc	make_expression (const expr2tc &symbol) const
	Creates an expression with the intervals found for the given symbol.
void	assume (const expr2tc &)
	Adds a restriction over all intervals.
void	assume_assertion (const expr2tc &guard, const ai_baset &ai)
	Under –interval-analysis-assume-asserts, narrows the state to `guard`.
void	process_instruction (goto_programt::const_targett from)
	Updates the interval state based on a single goto-program instruction.
void	join_snapshot (const std::shared_ptr< interval_map > &snapshot)
	Join the domain recorded when another symex path was parked into this one, over every variable: a path narrows intervals by ASSUME as well as by assignment, so joining only the phi-assigned variables is unsound.
void	havoc_rec (const expr2tc &expr)
	Recursively explores an Expression until it reaches a symbol, then removes it from the int_map whatever the symbol's type.
void	havoc_written_arguments (const code_function_call2t &call)
	Forget what a body-less call that symex models may write through its pointer arguments (#8083).
bool	havoc_pointee (const expr2tc &arg, bool any_type)
	Havoc the variable `arg` points into; false when that is unknown and `arg`, a pointer or `any_type`, may still have been written through.
virtual bool	ai_simplify (expr2tc &condition, const namespacet &ns) const override
	Uses the abstract state to simplify a given expression using context- specific information.
void	copy_if_needed ()
template<class Interval>
Interval	get_interval (const expr2tc &e) const
	Get the interval for expression.
template<class Interval>
Interval	get_interval_from_symbol (const symbol2t &sym) const
	Get the interval from symbol object or top.
template<size_t Index, class Interval>
Interval	get_interval_from_variant (const symbol2t &sym) const
template<class Interval>
bool	join_intervals (const std::shared_ptr< Interval > &after, std::shared_ptr< Interval > &dst, bool can_extrapolate) const
template<class Interval>
Interval	get_interval_from_const (const expr2tc &sym) const
	Get the interval from constant expression.
template<class Interval>
Interval	get_interval_from_typecast (const typecast2t &cast, Interval result) const
template<class Interval>
Interval	get_top_interval_from_expr (const expr2tc &sym) const
template<class Interval>
bool	is_mapped (const symbol2t &sym) const
template<class Interval>
expr2tc	make_expression_helper (const expr2tc &symbol) const
template<class Interval>
expr2tc	make_expression_value (const Interval &interval, const type2tc &type, bool upper) const
template<>
interval_domaint::integer_intervalt	get_interval_from_symbol (const symbol2t &sym) const
template<>
interval_domaint::real_intervalt	get_interval_from_symbol (const symbol2t &sym) const
template<>
wrapped_interval	get_interval_from_symbol (const symbol2t &sym) const
template<>
void	update_symbol_interval (const symbol2t &sym, const interval_domaint::integer_intervalt &value)
template<>
void	update_symbol_interval (const symbol2t &sym, const interval_domaint::real_intervalt &value)
template<>
void	update_symbol_interval (const symbol2t &sym, const wrapped_interval &value)
template<>
interval_domaint::integer_intervalt	get_interval_from_const (const expr2tc &e) const
template<>
interval_domaint::real_intervalt	get_interval_from_const (const expr2tc &e) const
template<>
wrapped_interval	get_interval_from_const (const expr2tc &e) const
template<>
interval_domaint::integer_intervalt	wrap_to_type (const integer_intervalt &i, const type2tc &t) const
template<class T>
T	extrapolate_intervals (const T &before, const T &after) const
template<>
wrapped_interval	extrapolate_intervals (const wrapped_interval &before, const wrapped_interval &after) const
template<>
wrapped_interval	get_top_interval_from_expr (const expr2tc &e) const
template<class T>
T	interpolate_intervals (const T &before, const T &after)
template<class T>
T	get_interval_from_typecast (const typecast2t &cast, T result) const
template<class T>
T	get_interval (const expr2tc &e) const
template<>
bool	is_mapped (const symbol2t &sym) const
template<>
expr2tc	make_expression_value (const wrapped_interval &interval, const type2tc &type, bool upper) const
template<>
expr2tc	make_expression_helper (const expr2tc &symbol) const
Public Member Functions inherited from ai_domain_baset
virtual	~ai_domain_baset ()
virtual bool	ai_simplify_lhs (expr2tc &condition, const namespacet &ns) const
	Simplifies the expression but keeps it as an l-value.
virtual expr2tc	to_predicate (void) const
	Gives a Boolean condition that is true for all values represented by the domain.

Static Public Member Functions
static void	set_options (const optionst &options)
static tvt	eval_boolean_expression (const expr2tc &cond, const interval_domaint &id)
	Interpolate bound back after fixpoint.
static std::shared_ptr< interval_map >	get_empty ()

Public Attributes
std::shared_ptr< interval_map >	intervals
bool	copied = false

Static Public Attributes
static bool	enable_interval_arithmetic = false
static bool	enable_interval_bitwise_arithmetic = false
	Enable simplification for arithmetic operators.
static bool	enable_modular_intervals = false
	Enable simplification for bitwise operations.
static bool	enable_assertion_simplification = false
	Make a modular operation after every assignment.
static bool	enable_contraction_for_abstract_states = true
	Simplify condition and assertions with the intervals.
static bool	enable_wrapped_intervals = false
	Use contractor for <= operations.
static bool	enable_real_intervals = true
	Enabled wrapped intervals (disables Integers).
static bool	enable_assume_asserts = true
	Enable real (floating-point) intervals.
static bool	enable_eval_assumptions = true
	Asserts are propagates as assumptions.
static bool	enable_ibex_contractor = false
	Try to evaluate in a guard in a TVT to accelerate bottoms.
static bool	skip_inductive_step_instructions = false
	Use ibex contractor.
static unsigned	fixpoint_limit = 5
static bool	widening_under_approximate_bound = false
	Sets a limit for number of iterations before widening.
static bool	widening_extrapolate = false
	Whether to considers overflows for Integers.
static bool	widening_narrowing = false
	Extrapolate bound to infinity based on previous iteration.

Protected Member Functions
bool	join (const interval_domaint &b, const goto_programt::const_targett &to)
	Sets *this to the mathematical join between the two domains.
void	assume_rec (const expr2tc &expr, bool negation=false)
	Recursively explores intervals of an assume expression.
void	assume_rec (const expr2tc &lhs, expr2t::expr_ids id, const expr2tc &rhs)
	Recursively explores intervals over a comparation expression, inserting them into int_map.
void	assign (const expr2tc &assignment, const bool recursive=false)
	Computes an assignment expression.
template<class Interval>
void	apply_assignment (const expr2tc &lhs, const expr2tc &rhs, bool recursive)
	Applies LHS <= RHS and RHS <= LHS from assignment instructions.
template<class Interval>
Interval	extrapolate_intervals (const Interval &before, const Interval &after) const
	Applies Extrapolation widening algorithm.
template<class Interval>
Interval	interpolate_intervals (const Interval &before, const Interval &after)
	Applies Interpolation narrowing algorithm.
template<class Interval>
void	apply_assume_less (const expr2tc &lhs, const expr2tc &rhs)
	Applies LHS < RHS.
template<class Interval>
void	apply_assume_symbol_truth (const symbol2t &sym, bool is_false)
	Applies symbol = truth.
template<class Interval>
Interval	generate_modular_interval (const type2tc &t) const
	Generates interval with [min, max] of type t.
template<class Interval>
Interval	wrap_to_type (const Interval &i, const type2tc &t) const
	Bring an interval computed over unbounded integers back into the range of the bitvector type t, as the solver's modular arithmetic would.
template<class IntervalMap>
bool	join (IntervalMap &new_map, const IntervalMap &previous_map, const bool is_guard_instruction=true)
template<class Interval>
void	update_symbol_interval (const symbol2t &sym, const Interval &value)
	Sets new interval for symbol.
template<size_t Index, class Interval>
void	update_symbol_from_variant (const symbol2t &sym, const Interval &value)
template<>
wrapped_interval	generate_modular_interval (const type2tc &t) const
template<>
void	apply_assume_less (const expr2tc &a, const expr2tc &b)
Protected Member Functions inherited from ai_domain_baset
	ai_domain_baset ()
	The constructor is expected to produce 'false' or 'bottom'.

Protected Attributes
bool	bottom
	Is this state a bottom.

Detailed Description

Trivial, conjunctive interval domain for both float and integers.

The categorization 'float' and 'integers' is done by is_int and is_float.

Member Typedef Documentation

◆ integer_intervalt

using interval_domaint::integer_intervalt = interval_templatet<BigInt>

◆ interval

using interval_domaint::interval

Initial value:

 std::variant<
    std::shared_ptr<integer_intervalt>,
    std::shared_ptr<real_intervalt>,
    std::shared_ptr<wrapped_interval>>

◆ interval_map

using interval_domaint::interval_map = std::unordered_map<irep_idt, interval, irep_id_hash>

◆ real_intervalt

using interval_domaint::real_intervalt

Initial value:

interval_templatet<boost::multiprecision::cpp_bin_float_100>

interval_templatet

This class is used to store intervals in the form of lower <= upper.

Definition interval_template.h:20

Constructor & Destructor Documentation

◆ interval_domaint()

interval_domaint::interval_domaint ( )

inline

Member Function Documentation

◆ ai_simplify()

bool interval_domaint::ai_simplify	(	expr2tc &	condition,
		const namespacet &	ns ) const

overridevirtual

Uses the abstract state to simplify a given expression using context- specific information.

Parameters

parameters The expression to simplify.

Returns: A simplified version of the expression.

This implementation is aimed at reducing assertions to true, particularly range checks for arrays and other bounds checks.

Rather than work with the various kinds of exprt directly, we use assume, join and is_bottom. It is sufficient for the use case and avoids duplicating functionality that is in assume anyway.

As some expressions (1<=a && a<=2) can be represented exactly as intervals and some can't (a<1 || a>2), the way these operations are used varies depending on the structure of the expression to try to give the best results. For example negating a disjunction makes it easier for assume to handle.

Implements ai_domain_baset.

◆ apply_assignment()

template<class T>

void interval_domaint::apply_assignment	(	const expr2tc &	lhs,
		const expr2tc &	rhs,
		bool	recursive )

protected

Applies LHS <= RHS and RHS <= LHS from assignment instructions.

This is separate from the usual assume_rec as LHS symbol may be inside RHS

Template Parameters

Interval interval template specialization (Integers, Reals)

Parameters

lhs
rhs

◆ apply_assume_less() [1/2]

template<>

void interval_domaint::apply_assume_less	(	const expr2tc &	a,
		const expr2tc &	b )

protected

◆ apply_assume_less() [2/2]

template<class Interval>

void interval_domaint::apply_assume_less	(	const expr2tc &	lhs,
		const expr2tc &	rhs )

protected

Applies LHS < RHS.

Template Parameters

Interval interval template specialization (Integers, Reals)

Parameters

lhs
rhs
less_than_equal	if operation should be <=

◆ apply_assume_symbol_truth()

template<class Interval>

void interval_domaint::apply_assume_symbol_truth	(	const symbol2t &	sym,
		bool	is_false )

protected

Applies symbol = truth.

Template Parameters

Interval interval template specialization (Integers, Reals)

Parameters

symbol
negation

◆ assign()

void interval_domaint::assign	(	const expr2tc &	assignment,
		const bool	recursive = false )

protected

Computes an assignment expression.

This recomputes the interval of the LHS to be of RHS, i.e. LHS == RHS.

Parameters

assignment

◆ assume()

void interval_domaint::assume ( const expr2tc & cond )

Adds a restriction over all intervals.

Do not mistake this by an ASSUME instruction! This can take any type of expression!

◆ assume_assertion()

void interval_domaint::assume_assertion	(	const expr2tc &	guard,
		const ai_baset &	ai )

Under –interval-analysis-assume-asserts, narrows the state to guard.

◆ assume_rec() [1/2]

void interval_domaint::assume_rec	(	const expr2tc &	expr,
		bool	negation = false )

protected

Recursively explores intervals of an assume expression.

This is the entry-point of the function, it does the following:

If the current negation flag is set. Then the operator is inverted (e.g. lower becomes greater_eq)
For if2t and or2t... de morgan is applied and this function is called again for its operands

Parameters

expr
negation	sets whether the current expr is a negation

◆ assume_rec() [2/2]

void interval_domaint::assume_rec	(	const expr2tc &	lhs,
		expr2t::expr_ids	id,
		const expr2tc &	rhs )

protected

Recursively explores intervals over a comparation expression, inserting them into int_map.

Parameters

lhs
id
rhs

◆ clear_state()

void interval_domaint::clear_state ( )

inline

◆ copy_if_needed()

void interval_domaint::copy_if_needed ( )

inline

◆ dump()

void interval_domaint::dump ( ) const

◆ eval_boolean_expression()

tvt interval_domaint::eval_boolean_expression	(	const expr2tc &	cond,
		const interval_domaint &	id )

static

Interpolate bound back after fixpoint.

Eval whether a boolean expression is always true, always false, or either (for the current state)

◆ extrapolate_intervals() [1/3]

template<class Interval>

Interval interval_domaint::extrapolate_intervals	(	const Interval &	before,
		const Interval &	after ) const

protected

Applies Extrapolation widening algorithm.

Given two intervals: (a0, b0) (before the computation) and (a1, b1) (after the computation): The objective of the extrapolation is to accelerate the convergence at the cost of precision

Example: int i = 0; while(i < 10) i++; <— what is the interval for i before the increment?

Computing the interval of sum would need 11 iterations to arrive to [0,9], it 1 = [0,0] it 2 = [0,1] it 3 = [0,2] ... it 10 = [0,9] it 11 = [0,9] fixpoint

By extrapolating, we can arrive at [0, +inf] in two iterations. it 1 = [0,0] it 2 = [0,1] => [0, inf] it 3 = [0,inf] fixpoint

Widening((a0,b0), (a1,b1)) = (a1 < a0 ? -infinity : a0, b1 > b0 ? infinity : b0 )

Template Parameters

Interval interval template specialization (Integers, Reals)

Parameters

lhs
rhs

◆ extrapolate_intervals() [2/3]

template<class T>

T interval_domaint::extrapolate_intervals	(	const T &	before,
		const T &	after ) const

◆ extrapolate_intervals() [3/3]

template<>

wrapped_interval interval_domaint::extrapolate_intervals	(	const wrapped_interval &	before,
		const wrapped_interval &	after ) const

◆ generate_modular_interval() [1/2]

template<>

wrapped_interval interval_domaint::generate_modular_interval ( const type2tc & t ) const

protected

◆ generate_modular_interval() [2/2]

template<class Interval>

Interval interval_domaint::generate_modular_interval ( const type2tc & t ) const

protected

Generates interval with [min, max] of type t.

Template Parameters

Interval interval template specialization (Integers, Reals)

Parameters

t

Returns: Interval the returned interval is either [min, max] or (-infinity, infinity)

◆ get_empty()

std::shared_ptr< interval_map > interval_domaint::get_empty ( )

inlinestatic

◆ get_interval() [1/2]

template<class T>

T interval_domaint::get_interval ( const expr2tc & e ) const

◆ get_interval() [2/2]

template<class Interval>

Interval interval_domaint::get_interval ( const expr2tc & e ) const

Get the interval for expression.

This computes the interval of a given expression and returns it

Template Parameters

Interval interval template specialization (Integers, Reals)

Parameters

e

Returns: Interval

◆ get_interval_from_const() [1/4]

template<>

wrapped_interval interval_domaint::get_interval_from_const ( const expr2tc & e ) const

◆ get_interval_from_const() [2/4]

template<>

interval_domaint::real_intervalt interval_domaint::get_interval_from_const ( const expr2tc & e ) const

◆ get_interval_from_const() [3/4]

template<>

interval_domaint::integer_intervalt interval_domaint::get_interval_from_const ( const expr2tc & e ) const

◆ get_interval_from_const() [4/4]

template<class Interval>

Interval interval_domaint::get_interval_from_const ( const expr2tc & sym ) const

Get the interval from constant expression.

Template Parameters

Interval interval template specialization (Integers, Reals)

Parameters

sym

Returns: Interval

◆ get_interval_from_symbol() [1/4]

template<>

wrapped_interval interval_domaint::get_interval_from_symbol ( const symbol2t & sym ) const

◆ get_interval_from_symbol() [2/4]

template<>

interval_domaint::real_intervalt interval_domaint::get_interval_from_symbol ( const symbol2t & sym ) const

◆ get_interval_from_symbol() [3/4]

template<>

interval_domaint::integer_intervalt interval_domaint::get_interval_from_symbol ( const symbol2t & sym ) const

◆ get_interval_from_symbol() [4/4]

template<class Interval>

Interval interval_domaint::get_interval_from_symbol ( const symbol2t & sym ) const

Get the interval from symbol object or top.

Template Parameters

Interval interval template specialization (Integers, Reals)

Parameters

sym

Returns: Interval

◆ get_interval_from_typecast() [1/2]

template<class Interval>

Interval interval_domaint::get_interval_from_typecast	(	const typecast2t &	cast,
		Interval	result ) const

◆ get_interval_from_typecast() [2/2]

template<class T>

T interval_domaint::get_interval_from_typecast	(	const typecast2t &	cast,
		T	result ) const

◆ get_interval_from_variant()

template<size_t Index, class Interval>

Interval interval_domaint::get_interval_from_variant ( const symbol2t & sym ) const

◆ get_top_interval_from_expr() [1/2]

template<>

wrapped_interval interval_domaint::get_top_interval_from_expr ( const expr2tc & e ) const

◆ get_top_interval_from_expr() [2/2]

template<class Interval>

Interval interval_domaint::get_top_interval_from_expr ( const expr2tc & sym ) const

◆ havoc_pointee()

bool interval_domaint::havoc_pointee	(	const expr2tc &	arg,
		bool	any_type )

Havoc the variable arg points into; false when that is unknown and arg, a pointer or any_type, may still have been written through.

◆ havoc_rec()

void interval_domaint::havoc_rec ( const expr2tc & expr )

Recursively explores an Expression until it reaches a symbol, then removes it from the int_map whatever the symbol's type.

TODO: There are a lot of expressions that are not supported TODO: A utility function that recursively extracts all the symbols of an expr would be very useful

Parameters

expr

◆ havoc_written_arguments()

void interval_domaint::havoc_written_arguments ( const code_function_call2t & call )

Forget what a body-less call that symex models may write through its pointer arguments (#8083).

◆ interpolate_intervals() [1/2]

template<class Interval>

Interval interval_domaint::interpolate_intervals	(	const Interval &	before,
		const Interval &	after )

protected

Applies Interpolation narrowing algorithm.

Given two intervals: (a0, b0) (before the computation) and (a1, b1) (after the computation): The objective of the interpolation is to bring back some of the precision lost from an extrapolation.

Example: int i = 0; while(i < 10) i++; <— what is the interval for i before the increment?

Coming back from an extrapolation [0, +inf] (which is a fixpoint) we can narrow the interval by checking the interval post the loop condition (i < 10) it 4 = narrowing([0, inf], [0, 9]) => [0,9] it 5 = [0,9]

Narrowing((a0,b0), (a1,b1)) = (a0 == -inf ? a1 : a0, b0 = +inf ? b1 : b0)

Template Parameters

Interval interval template specialization (Integers, Reals)

Parameters

lhs
rhs

◆ interpolate_intervals() [2/2]

template<class T>

T interval_domaint::interpolate_intervals	(	const T &	before,
		const T &	after )

◆ is_bottom()

bool interval_domaint::is_bottom ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

◆ is_mapped() [1/2]

template<>

bool interval_domaint::is_mapped ( const symbol2t & sym ) const

◆ is_mapped() [2/2]

template<class Interval>

bool interval_domaint::is_mapped ( const symbol2t & sym ) const

◆ is_top()

bool interval_domaint::is_top ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

◆ join() [1/2]

bool interval_domaint::join	(	const interval_domaint &	b,
		const goto_programt::const_targett &	to )

protected

Sets *this to the mathematical join between the two domains.

This can be thought of as an abstract version of union; *this is increased so that it contains all of the values that are represented by b as well as its original intervals. The result is an overapproximation, for example: "[0,1]".join("[3,4]") --> "[0,4]" includes 2 which isn't in [0,1] or [3,4].

     Join is used in several places, the most significant being
     merge, which uses it to bring together two different paths
     of analysis.

Parameters

b	The interval domain, b, to join to this domain.

Returns: True if the join increases the set represented by *this, False if there is no change.

◆ join() [2/2]

template<class IntervalMap>

bool interval_domaint::join	(	IntervalMap &	new_map,
		const IntervalMap &	previous_map,
		const bool	is_guard_instruction = true )

protected

◆ join_intervals()

template<class Interval>

bool interval_domaint::join_intervals	(	const std::shared_ptr< Interval > &	after,
		std::shared_ptr< Interval > &	dst,
		bool	can_extrapolate ) const

◆ join_snapshot()

void interval_domaint::join_snapshot ( const std::shared_ptr< interval_map > & snapshot )

Join the domain recorded when another symex path was parked into this one, over every variable: a path narrows intervals by ASSUME as well as by assignment, so joining only the phi-assigned variables is unsound.

◆ make_bottom()

void interval_domaint::make_bottom ( )

inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

◆ make_entry()

void interval_domaint::make_entry ( )

inlinefinaloverridevirtual

a reasonable entry-point state

Implements ai_domain_baset.

◆ make_expression()

expr2tc interval_domaint::make_expression ( const expr2tc & symbol ) const

Creates an expression with the intervals found for the given symbol.

For example, if given a symbol expression with the variable 'FOO'. If at the current abstract state the interval for it is of: [2, 42]

This would return an expression of the form: AND (>= FOO 2) (<= FOO 42)

If top, it will return a true expr. If bottom, it will return a false expr.

Parameters

symbol to construct the interval

Returns: expr2tc

◆ make_expression_helper() [1/2]

template<>

expr2tc interval_domaint::make_expression_helper ( const expr2tc & symbol ) const

◆ make_expression_helper() [2/2]

template<class T>

expr2tc interval_domaint::make_expression_helper ( const expr2tc & symbol ) const

◆ make_expression_value() [1/2]

template<class Interval>

expr2tc interval_domaint::make_expression_value	(	const Interval &	interval,
		const type2tc &	type,
		bool	upper ) const

◆ make_expression_value() [2/2]

template<>

expr2tc interval_domaint::make_expression_value	(	const wrapped_interval &	interval,
		const type2tc &	type,
		bool	upper ) const

◆ make_top()

void interval_domaint::make_top ( )

inlinefinaloverridevirtual

all states – the analysis doesn't use this, and domains may refuse to implement it.

Implements ai_domain_baset.

◆ merge()

bool interval_domaint::merge	(	const interval_domaint &	b,
		goto_programt::const_targett	,
		goto_programt::const_targett	to )

inline

◆ output()

void interval_domaint::output ( std::ostream & out ) const

overridevirtual

Implements ai_domain_baset.

◆ process_instruction()

void interval_domaint::process_instruction ( goto_programt::const_targett from )

Updates the interval state based on a single goto-program instruction.

Handles ASSIGN, ASSUME, DECL, DEAD and FUNCTION_CALL without requiring an ai_baset reference. Intended for online use during symbolic execution (default guard pruning; disable guard with –no-interval-symex-guard; assertion pruning via –interval-symex-assert).

Parameters

from	iterator to the instruction to process

◆ set_options()

void interval_domaint::set_options ( const optionst & options )

static

◆ transform()

void interval_domaint::transform	(	goto_programt::const_targett	from,
		goto_programt::const_targett	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 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())

Implements ai_domain_baset.

◆ update_symbol_from_variant()

template<size_t Index, class Interval>

void interval_domaint::update_symbol_from_variant	(	const symbol2t &	sym,
		const Interval &	value )

protected

◆ update_symbol_interval() [1/4]

template<class Interval>

void interval_domaint::update_symbol_interval	(	const symbol2t &	sym,
		const Interval &	value )

protected

Sets new interval for symbol.

Template Parameters

Interval interval template specialization (Integers, Reals)

Parameters

sym
value

◆ update_symbol_interval() [2/4]

template<>

void interval_domaint::update_symbol_interval	(	const symbol2t &	sym,
		const interval_domaint::integer_intervalt &	value )

◆ update_symbol_interval() [3/4]

template<>

void interval_domaint::update_symbol_interval	(	const symbol2t &	sym,
		const interval_domaint::real_intervalt &	value )

◆ update_symbol_interval() [4/4]

template<>

void interval_domaint::update_symbol_interval	(	const symbol2t &	sym,
		const wrapped_interval &	value )

◆ wrap_to_type() [1/2]

template<>

interval_domaint::integer_intervalt interval_domaint::wrap_to_type	(	const integer_intervalt &	i,
		const type2tc &	t ) const

◆ wrap_to_type() [2/2]

template<class Interval>

Interval interval_domaint::wrap_to_type	(	const Interval &	i,
		const type2tc &	t ) const

protected

Bring an interval computed over unbounded integers back into the range of the bitvector type t, as the solver's modular arithmetic would.

Member Data Documentation

◆ bottom

bool interval_domaint::bottom

protected

Is this state a bottom.

I.e., there is a contradiction between an assignment and an assume

◆ copied

bool interval_domaint::copied = false

◆ enable_assertion_simplification

bool interval_domaint::enable_assertion_simplification = false

static

Make a modular operation after every assignment.

◆ enable_assume_asserts

bool interval_domaint::enable_assume_asserts = true

static

Enable real (floating-point) intervals.

◆ enable_contraction_for_abstract_states

bool interval_domaint::enable_contraction_for_abstract_states = true

static

Simplify condition and assertions with the intervals.

◆ enable_eval_assumptions

bool interval_domaint::enable_eval_assumptions = true

static

Asserts are propagates as assumptions.

◆ enable_ibex_contractor

bool interval_domaint::enable_ibex_contractor = false

static

Try to evaluate in a guard in a TVT to accelerate bottoms.

◆ enable_interval_arithmetic

bool interval_domaint::enable_interval_arithmetic = false

static

◆ enable_interval_bitwise_arithmetic

bool interval_domaint::enable_interval_bitwise_arithmetic = false

static

Enable simplification for arithmetic operators.

◆ enable_modular_intervals

bool interval_domaint::enable_modular_intervals = false

static

Enable simplification for bitwise operations.

◆ enable_real_intervals

bool interval_domaint::enable_real_intervals = true

static

Enabled wrapped intervals (disables Integers).

◆ enable_wrapped_intervals

bool interval_domaint::enable_wrapped_intervals = false

static

Use contractor for <= operations.

◆ fixpoint_limit

unsigned interval_domaint::fixpoint_limit = 5

static

◆ intervals

std::shared_ptr<interval_map> interval_domaint::intervals

◆ skip_inductive_step_instructions

bool interval_domaint::skip_inductive_step_instructions = false

thread_localstatic

Use ibex contractor.

When set, the transformer skips any instruction whose inductive_step_instruction flag is true. Used by the post-k-induction loop-bounds pass: havoc'd assignments and entry-condition assumes that k-induction emitted before each loop head are made transparent, so the fixpoint at the loop head matches the bounds at the original loop head (before k-induction's transformation). The bounds are then a sound inductive hypothesis to assume right after the havoc.

thread_local so a future threaded –k-induction-parallel can run concurrent interval analyses without one transformer's "skip" leaking into another's. Always toggled via scoped_skip_inductive (interval_analysis.cpp), which save-and-restores the prior value so an exception or a nested call cannot leave it stuck.

◆ widening_extrapolate

bool interval_domaint::widening_extrapolate = false

static

Whether to considers overflows for Integers.

◆ widening_narrowing

bool interval_domaint::widening_narrowing = false

static

Extrapolate bound to infinity based on previous iteration.

◆ widening_under_approximate_bound

bool interval_domaint::widening_under_approximate_bound = false

static

Sets a limit for number of iterations before widening.

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

src/goto-programs/abstract-interpretation/interval_domain.h
src/goto-programs/abstract-interpretation/interval_domain.cpp

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Static Public Attributes

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ integer_intervalt

◆ interval

◆ interval_map

◆ real_intervalt

Constructor & Destructor Documentation

◆ interval_domaint()

Member Function Documentation

◆ ai_simplify()

◆ apply_assignment()

◆ apply_assume_less() [1/2]

◆ apply_assume_less() [2/2]

◆ apply_assume_symbol_truth()

◆ assign()

◆ assume()

◆ assume_assertion()

◆ assume_rec() [1/2]

◆ assume_rec() [2/2]

◆ clear_state()

◆ copy_if_needed()

◆ dump()

◆ eval_boolean_expression()

◆ extrapolate_intervals() [1/3]

◆ extrapolate_intervals() [2/3]

◆ extrapolate_intervals() [3/3]

◆ generate_modular_interval() [1/2]

◆ generate_modular_interval() [2/2]

◆ get_empty()

◆ get_interval() [1/2]

◆ get_interval() [2/2]

◆ get_interval_from_const() [1/4]

◆ get_interval_from_const() [2/4]

◆ get_interval_from_const() [3/4]

◆ get_interval_from_const() [4/4]

◆ get_interval_from_symbol() [1/4]

◆ get_interval_from_symbol() [2/4]

◆ get_interval_from_symbol() [3/4]

◆ get_interval_from_symbol() [4/4]

◆ get_interval_from_typecast() [1/2]

◆ get_interval_from_typecast() [2/2]

◆ get_interval_from_variant()

◆ get_top_interval_from_expr() [1/2]

◆ get_top_interval_from_expr() [2/2]

◆ havoc_pointee()

◆ havoc_rec()

◆ havoc_written_arguments()

◆ interpolate_intervals() [1/2]

◆ interpolate_intervals() [2/2]

◆ is_bottom()

◆ is_mapped() [1/2]

◆ is_mapped() [2/2]

◆ is_top()

◆ join() [1/2]

◆ join() [2/2]

◆ join_intervals()

◆ join_snapshot()

◆ make_bottom()

◆ make_entry()

◆ make_expression()

◆ make_expression_helper() [1/2]

◆ make_expression_helper() [2/2]

◆ make_expression_value() [1/2]

◆ make_expression_value() [2/2]

◆ make_top()

◆ merge()

◆ output()

◆ process_instruction()

◆ set_options()

◆ transform()

◆ update_symbol_from_variant()

◆ update_symbol_interval() [1/4]

◆ update_symbol_interval() [2/4]