#include <vstore.hpp>

Classes
struct	var_dom

Public Types
using	universe_type = U

using	local_universe = typename universe_type::local_type

using	allocator_type = Allocator

using	this_type = VStore<universe_type, allocator_type>

template<class Alloc >
using	tell_type = battery::vector<var_dom<Alloc>, Alloc>

template<class Alloc >
using	ask_type = tell_type<Alloc>

template<class Alloc = allocator_type>
using	snapshot_type = battery::vector<local_universe, Alloc>

Public Member Functions
CUDA	VStore (const this_type &other)

CUDA	VStore (AType atype, const allocator_type &alloc=allocator_type())

CUDA	VStore (AType atype, size_t size, const allocator_type &alloc=allocator_type())

template<class R >
CUDA	VStore (const VStore< R, allocator_type > &other)

template<class R , class Alloc2 >
CUDA	VStore (const VStore< R, Alloc2 > &other, const allocator_type &alloc=allocator_type())

template<class R , class Alloc2 , class... Allocators>
CUDA	VStore (const VStore< R, Alloc2 > &other, const AbstractDeps< Allocators... > &deps)

CUDA	VStore (this_type &&other)

CUDA allocator_type	get_allocator () const

CUDA AType	aty () const

CUDA size_t	vars () const

CUDA local::BInc	is_top () const

CUDA local::BDec	is_bot () const

template<class Alloc = allocator_type>
CUDA snapshot_type< Alloc >	snapshot (const Alloc &alloc=Alloc()) const

template<class Alloc >
CUDA this_type &	restore (const snapshot_type< Alloc > &snap)

template<IKind kind, bool diagnose = false, class F , class Env , class I >
CUDA NI bool	interpret (const F &f, Env &env, I &intermediate, IDiagnostics &diagnostics) const

template<bool diagnose = false, class F , class Env , class Alloc2 >
CUDA NI bool	interpret_tell (const F &f, Env &env, tell_type< Alloc2 > &tell, IDiagnostics &diagnostics) const

template<bool diagnose = false, class F , class Env , class Alloc2 >
CUDA NI bool	interpret_ask (const F &f, const Env &env, ask_type< Alloc2 > &ask, IDiagnostics &diagnostics) const

CUDA const universe_type &	project (AVar x) const

CUDA const universe_type &	operator[] (int x) const

CUDA this_type &	tell_top ()

CUDA this_type &	tell (int x, const universe_type &dom)

template<class Mem >
CUDA this_type &	tell (int x, const universe_type &dom, BInc< Mem > &has_changed)

CUDA this_type &	tell (AVar x, const universe_type &dom)

template<class Mem >
CUDA this_type &	tell (AVar x, const universe_type &dom, BInc< Mem > &has_changed)

template<class Alloc2 , class Mem >
CUDA this_type &	tell (const tell_type< Alloc2 > &t, BInc< Mem > &has_changed)

template<class Alloc2 >
CUDA this_type &	tell (const tell_type< Alloc2 > &t)

template<class U2 , class Alloc2 , class Mem >
CUDA this_type &	tell (const VStore< U2, Alloc2 > &other, BInc< Mem > &has_changed)

template<class U2 , class Alloc2 >
CUDA this_type &	tell (const VStore< U2, Alloc2 > &other)

CUDA this_type &	dtell_bot ()

template<class U2 , class Alloc2 , class Mem >
CUDA this_type &	dtell (const VStore< U2, Alloc2 > &other, BInc< Mem > &has_changed)

template<class U2 , class Alloc2 , class Mem >
CUDA this_type &	dtell (const VStore< U2, Alloc2 > &other)

template<class Alloc2 >
CUDA local::BInc	ask (const ask_type< Alloc2 > &t) const

CUDA size_t	num_refinements () const

template<class M >
CUDA void	refine (size_t, BInc< M > &) const

template<class ExtractionStrategy = NonAtomicExtraction>
CUDA bool	is_extractable (const ExtractionStrategy &strategy=ExtractionStrategy()) const

template<class U2 , class Alloc2 >
CUDA void	extract (VStore< U2, Alloc2 > &ua) const

template<class Env >
CUDA NI TFormula< typename Env::allocator_type >	deinterpret (const Env &env) const

CUDA void	print () const

Static Public Member Functions
static CUDA this_type	bot (AType atype=UNTYPED, const allocator_type &alloc=allocator_type{})

static CUDA this_type	top (AType atype=UNTYPED, const allocator_type &alloc=allocator_type{})

template<class Env >
static CUDA this_type	bot (Env &env, const allocator_type &alloc=allocator_type{})

template<class Env >
static CUDA this_type	top (Env &env, const allocator_type &alloc=allocator_type{})

Static Public Attributes
static constexpr const bool	is_abstract_universe = false

static constexpr const bool	sequential = universe_type::sequential

static constexpr const bool	is_totally_ordered = false

static constexpr const bool	preserve_bot = true

static constexpr const bool	preserve_top = true

static constexpr const bool	preserve_join = universe_type::preserve_join

static constexpr const bool	preserve_meet = universe_type::preserve_meet

static constexpr const bool	injective_concretization = universe_type::injective_concretization

static constexpr const bool	preserve_concrete_covers = universe_type::preserve_concrete_covers

static constexpr const char *	name = "VStore"

Friends
template<class U2 , class Alloc2 >
class	VStore

Detailed Description

template<class U, class Allocator>
class lala::VStore< U, Allocator >

The variable store abstract domain is a domain transformer built on top of an abstract universe U. Concretization function: \( \gamma(\rho) := \bigcap_{x \in \pi(\rho)} \gamma_{U_x}(\rho(x)) \). The top element is smashed and the equality between two stores is represented by the following equivalence relation, for two stores \( S \) and \( T \): \( S \equiv T \Leftrightarrow \forall{x \in \mathit{Vars}},~S(x) = T(x) \lor \exists{x \in \mathit{dom}(S)},\exists{y \in \mathit{dom}(T)},~S(x) = \top \land T(y) = \top \). Intuitively, it means that either all elements are equal or both stores have a top element, in which case they "collapse" to the top element, and are considered equal.

The bottom element is the element \( \langle \bot, \ldots \rangle \), that is an infinite number of variables initialized to bottom. In practice, we cannot represent infinite collections, so we represent bottom either as the empty collection or with a finite number of bottom elements. Any finite store \( \langle x_1, \ldots, x_n \rangle \) should be seen as the concrete store \( \langle x_1, \ldots, x_n, \bot, \ldots \rangle \).

This semantics has implication when joining or merging two elements. For instance, \( \langle 1 \rangle.\mathit{dtell}(\langle \bot, 4 \rangle) \) will be equal to bottom, in that case represented by \( \langle \bot \rangle \).

Template parameters:

U is the type of the abstract universe.
Allocator is the allocator of the underlying array of universes.

Member Typedef Documentation

◆ universe_type

template<class U , class Allocator >

using lala::VStore< U, Allocator >::universe_type = U

◆ local_universe

template<class U , class Allocator >

using lala::VStore< U, Allocator >::local_universe = typename universe_type::local_type

◆ allocator_type

template<class U , class Allocator >

using lala::VStore< U, Allocator >::allocator_type = Allocator

◆ this_type

template<class U , class Allocator >

using lala::VStore< U, Allocator >::this_type = VStore<universe_type, allocator_type>

◆ tell_type

template<class U , class Allocator >

template<class Alloc >

using lala::VStore< U, Allocator >::tell_type = battery::vector<var_dom<Alloc>, Alloc>

◆ ask_type

template<class U , class Allocator >

template<class Alloc >

using lala::VStore< U, Allocator >::ask_type = tell_type<Alloc>

◆ snapshot_type

template<class U , class Allocator >

template<class Alloc = allocator_type>

using lala::VStore< U, Allocator >::snapshot_type = battery::vector<local_universe, Alloc>

Constructor & Destructor Documentation

◆ VStore() [1/7]

template<class U , class Allocator >

CUDA lala::VStore< U, Allocator >::VStore ( const this_type & other )

inline

◆ VStore() [2/7]

template<class U , class Allocator >

CUDA lala::VStore< U, Allocator >::VStore	(	AType	atype,
		const allocator_type &	alloc = allocator_type() )

inline

Initialize an empty store.

◆ VStore() [3/7]

template<class U , class Allocator >

CUDA lala::VStore< U, Allocator >::VStore	(	AType	atype,
		size_t	size,
		const allocator_type &	alloc = allocator_type() )

inline

◆ VStore() [4/7]

template<class U , class Allocator >

template<class R >

CUDA lala::VStore< U, Allocator >::VStore ( const VStore< R, allocator_type > & other )

inline

◆ VStore() [5/7]

template<class U , class Allocator >

template<class R , class Alloc2 >

CUDA lala::VStore< U, Allocator >::VStore	(	const VStore< R, Alloc2 > &	other,
		const allocator_type &	alloc = allocator_type() )

inline

◆ VStore() [6/7]

template<class U , class Allocator >

template<class R , class Alloc2 , class... Allocators>

CUDA lala::VStore< U, Allocator >::VStore	(	const VStore< R, Alloc2 > &	other,
		const AbstractDeps< Allocators... > &	deps )

inline

Copy the vstore other in the current element. deps can be empty and is not used besides to get the allocator (since this abstract domain does not have dependencies).

◆ VStore() [7/7]

template<class U , class Allocator >

CUDA lala::VStore< U, Allocator >::VStore ( this_type && other )

inline

Member Function Documentation

◆ get_allocator()

template<class U , class Allocator >

CUDA allocator_type lala::VStore< U, Allocator >::get_allocator ( ) const

inline

◆ aty()

template<class U , class Allocator >

CUDA AType lala::VStore< U, Allocator >::aty ( ) const

inline

◆ vars()

template<class U , class Allocator >

CUDA size_t lala::VStore< U, Allocator >::vars ( ) const

inline

Returns the number of variables currently represented by this abstract element.

◆ bot() [1/2]

template<class U , class Allocator >

static CUDA this_type lala::VStore< U, Allocator >::bot	(	AType	atype = UNTYPED,
		const allocator_type &	alloc = allocator_type{} )

inlinestatic

◆ top() [1/2]

template<class U , class Allocator >

static CUDA this_type lala::VStore< U, Allocator >::top	(	AType	atype = UNTYPED,
		const allocator_type &	alloc = allocator_type{} )

inlinestatic

A special symbolic element representing top.

◆ bot() [2/2]

template<class U , class Allocator >

template<class Env >

static CUDA this_type lala::VStore< U, Allocator >::bot	(	Env &	env,
		const allocator_type &	alloc = allocator_type{} )

inlinestatic

◆ top() [2/2]

template<class U , class Allocator >

template<class Env >

static CUDA this_type lala::VStore< U, Allocator >::top	(	Env &	env,
		const allocator_type &	alloc = allocator_type{} )

inlinestatic

◆ is_top()

template<class U , class Allocator >

CUDA local::BInc lala::VStore< U, Allocator >::is_top ( ) const

inline

true if at least one element is equal to top in the store, false otherwise.

◆ is_bot()

template<class U , class Allocator >

CUDA local::BDec lala::VStore< U, Allocator >::is_bot ( ) const

inline

The bottom element of a store of n variables is when all variables are at bottom, or the store is empty. We do not expect to use this operation a lot, so its complexity is linear in the number of variables.

◆ snapshot()

template<class U , class Allocator >

template<class Alloc = allocator_type>

CUDA snapshot_type< Alloc > lala::VStore< U, Allocator >::snapshot ( const Alloc & alloc = Alloc() ) const

inline

Take a snapshot of the current variable store.

◆ restore()

template<class U , class Allocator >

template<class Alloc >

CUDA this_type & lala::VStore< U, Allocator >::restore ( const snapshot_type< Alloc > & snap )

inline

◆ interpret()

template<class U , class Allocator >

template<IKind kind, bool diagnose = false, class F , class Env , class I >

CUDA NI bool lala::VStore< U, Allocator >::interpret	(	const F &	f,
		Env &	env,
		I &	intermediate,
		IDiagnostics &	diagnostics ) const

inline

◆ interpret_tell()

template<class U , class Allocator >

template<bool diagnose = false, class F , class Env , class Alloc2 >

CUDA NI bool lala::VStore< U, Allocator >::interpret_tell	(	const F &	f,
		Env &	env,
		tell_type< Alloc2 > &	tell,
		IDiagnostics &	diagnostics ) const

inline

The store of variables lattice expects a formula with a single variable (including existential quantifiers) that can be handled by the abstract universe U.

Variables must be existentially quantified before a formula containing variables can be interpreted. Variables are immediately assigned to an index of VStore and initialized to \( \bot_U \). Shadowing/redeclaration of variables with existential quantifier is not supported. The variable mapping is added to the environment only if the interpretation succeeds.

There is a small quirk: different stores might be produced if quantifiers do not appear in the same order. This is because we attribute the first available index to variables when interpreting the quantifier. In that case, the store will only be equivalent modulo the env structure.

◆ interpret_ask()

template<class U , class Allocator >

template<bool diagnose = false, class F , class Env , class Alloc2 >

CUDA NI bool lala::VStore< U, Allocator >::interpret_ask	(	const F &	f,
		const Env &	env,
		ask_type< Alloc2 > &	ask,
		IDiagnostics &	diagnostics ) const

inline

Similar to interpret_tell but do not support existential quantifier and therefore leaves env unchanged.

◆ project()

template<class U , class Allocator >

CUDA const universe_type & lala::VStore< U, Allocator >::project ( AVar x ) const

inline

The projection must stay const, otherwise the user might tell new information in the universe, but we need to know in case we reach top.

◆ operator[]()

template<class U , class Allocator >

CUDA const universe_type & lala::VStore< U, Allocator >::operator[] ( int x ) const

inline

See note on projection.

◆ tell_top()

template<class U , class Allocator >

CUDA this_type & lala::VStore< U, Allocator >::tell_top ( )

inline

◆ tell() [1/8]

template<class U , class Allocator >

CUDA this_type & lala::VStore< U, Allocator >::tell	(	int	x,
		const universe_type &	dom )

inline

Given an abstract variable v, tell(VID(v), dom) will update the domain of this variable with the new information dom. This tell method follows PCCP's model, but the variable x must already be initialized in the store.

◆ tell() [2/8]

template<class U , class Allocator >

template<class Mem >

CUDA this_type & lala::VStore< U, Allocator >::tell	(	int	x,
		const universe_type &	dom,
		BInc< Mem > &	has_changed )

inline

This tell method follows PCCP's model, but the variable x must already be initialized in the store.

◆ tell() [3/8]

template<class U , class Allocator >

CUDA this_type & lala::VStore< U, Allocator >::tell	(	AVar	x,
		const universe_type &	dom )

inline

This tell method follows PCCP's model, but the variable x must already be initialized in the store.

◆ tell() [4/8]

template<class U , class Allocator >

template<class Mem >

CUDA this_type & lala::VStore< U, Allocator >::tell	(	AVar	x,
		const universe_type &	dom,
		BInc< Mem > &	has_changed )

inline

This tell method follows PCCP's model, but the variable x must already be initialized in the store.

◆ tell() [5/8]

template<class U , class Allocator >

template<class Alloc2 , class Mem >

CUDA this_type & lala::VStore< U, Allocator >::tell	(	const tell_type< Alloc2 > &	t,
		BInc< Mem > &	has_changed )

inline

This tell method can grow the store if required, and therefore do not satisfy the PCCP model. /!\ It should not be used in parallel.

◆ tell() [6/8]

template<class U , class Allocator >

template<class Alloc2 >

CUDA this_type & lala::VStore< U, Allocator >::tell ( const tell_type< Alloc2 > & t )

inline

This tell method can grow the store if required, and therefore do not satisfy the PCCP model. /!\ It should not be used in parallel.

◆ tell() [7/8]

template<class U , class Allocator >

template<class U2 , class Alloc2 , class Mem >

CUDA this_type & lala::VStore< U, Allocator >::tell	(	const VStore< U2, Alloc2 > &	other,
		BInc< Mem > &	has_changed )

inline

Precondition: other must be smaller or equal in size than the current store.

◆ tell() [8/8]

template<class U , class Allocator >

template<class U2 , class Alloc2 >

CUDA this_type & lala::VStore< U, Allocator >::tell ( const VStore< U2, Alloc2 > & other )

inline

Precondition: other must be smaller or equal in size than the current store.

◆ dtell_bot()

template<class U , class Allocator >

CUDA this_type & lala::VStore< U, Allocator >::dtell_bot ( )

inline

◆ dtell() [1/2]

template<class U , class Allocator >

template<class U2 , class Alloc2 , class Mem >

CUDA this_type & lala::VStore< U, Allocator >::dtell	(	const VStore< U2, Alloc2 > &	other,
		BInc< Mem > &	has_changed )

inline

Precondition: other must be smaller or equal in size than the current store.

◆ dtell() [2/2]

template<class U , class Allocator >

template<class U2 , class Alloc2 , class Mem >

CUDA this_type & lala::VStore< U, Allocator >::dtell ( const VStore< U2, Alloc2 > & other )

inline

Precondition: other must be smaller or equal in size than the current store.

◆ ask()

template<class U , class Allocator >

template<class Alloc2 >

CUDA local::BInc lala::VStore< U, Allocator >::ask ( const ask_type< Alloc2 > & t ) const

inline

Returns: true when we can deduce the content of t from the current domain. For instance, if we have in the store x = [0..10], we can deduce x = [-1..11] but we cannot deduce x = [5..8].

◆ num_refinements()

template<class U , class Allocator >

CUDA size_t lala::VStore< U, Allocator >::num_refinements ( ) const

inline

◆ refine()

template<class U , class Allocator >

template<class M >

CUDA void lala::VStore< U, Allocator >::refine	(	size_t	,
		BInc< M > &	) const

inline

◆ is_extractable()

template<class U , class Allocator >

template<class ExtractionStrategy = NonAtomicExtraction>

CUDA bool lala::VStore< U, Allocator >::is_extractable ( const ExtractionStrategy & strategy = ExtractionStrategy() ) const

inline

An abstract element is extractable when it is not equal to top. If the strategy is atoms, we check the domains are singleton.

◆ extract()

template<class U , class Allocator >

template<class U2 , class Alloc2 >

CUDA void lala::VStore< U, Allocator >::extract ( VStore< U2, Alloc2 > & ua ) const

inline

Whenever this is different from top, we extract its data into ua.

Precondition: is_extractable() must be true. For now, we suppose VStore is only used to store under-approximation, I'm not sure yet how we would interact with over-approximation.

◆ deinterpret()

template<class U , class Allocator >

template<class Env >

CUDA NI TFormula< typename Env::allocator_type > lala::VStore< U, Allocator >::deinterpret ( const Env & env ) const

inline

◆ print()

template<class U , class Allocator >

CUDA void lala::VStore< U, Allocator >::print ( ) const

inline

Friends And Related Symbol Documentation

◆ VStore

template<class U , class Allocator >

template<class U2 , class Alloc2 >

friend class VStore

friend

Member Data Documentation

◆ is_abstract_universe

template<class U , class Allocator >

constexpr const bool lala::VStore< U, Allocator >::is_abstract_universe = false

staticconstexpr

◆ sequential

template<class U , class Allocator >

constexpr const bool lala::VStore< U, Allocator >::sequential = universe_type::sequential

staticconstexpr

◆ is_totally_ordered

template<class U , class Allocator >

constexpr const bool lala::VStore< U, Allocator >::is_totally_ordered = false

staticconstexpr

◆ preserve_bot

template<class U , class Allocator >

constexpr const bool lala::VStore< U, Allocator >::preserve_bot = true

staticconstexpr

◆ preserve_top

template<class U , class Allocator >

constexpr const bool lala::VStore< U, Allocator >::preserve_top = true

staticconstexpr

◆ preserve_join

template<class U , class Allocator >

constexpr const bool lala::VStore< U, Allocator >::preserve_join = universe_type::preserve_join

staticconstexpr

◆ preserve_meet

template<class U , class Allocator >

constexpr const bool lala::VStore< U, Allocator >::preserve_meet = universe_type::preserve_meet

staticconstexpr

◆ injective_concretization

template<class U , class Allocator >

constexpr const bool lala::VStore< U, Allocator >::injective_concretization = universe_type::injective_concretization

staticconstexpr

◆ preserve_concrete_covers

template<class U , class Allocator >

constexpr const bool lala::VStore< U, Allocator >::preserve_concrete_covers = universe_type::preserve_concrete_covers

staticconstexpr

◆ name

template<class U , class Allocator >

constexpr const char* lala::VStore< U, Allocator >::name = "VStore"

staticconstexpr

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

include/lala/vstore.hpp

Classes

Public Types

Public Member Functions

Static Public Member Functions

Static Public Attributes

Friends

Detailed Description

Member Typedef Documentation

◆ universe_type

◆ local_universe

◆ allocator_type

◆ this_type

◆ tell_type

◆ ask_type

◆ snapshot_type

Constructor & Destructor Documentation

◆ VStore() [1/7]

◆ VStore() [2/7]

◆ VStore() [3/7]

◆ VStore() [4/7]

◆ VStore() [5/7]

◆ VStore() [6/7]

◆ VStore() [7/7]

Member Function Documentation

◆ get_allocator()

◆ aty()

◆ vars()

◆ bot() [1/2]

◆ top() [1/2]

◆ bot() [2/2]

◆ top() [2/2]

◆ is_top()

◆ is_bot()

◆ snapshot()

◆ restore()

◆ interpret()

◆ interpret_tell()

◆ interpret_ask()

◆ project()

◆ operator[]()

◆ tell_top()

◆ tell() [1/8]

◆ tell() [2/8]

◆ tell() [3/8]

◆ tell() [4/8]

◆ tell() [5/8]

◆ tell() [6/8]

◆ tell() [7/8]

◆ tell() [8/8]

◆ dtell_bot()

◆ dtell() [1/2]

◆ dtell() [2/2]

◆ ask()

◆ num_refinements()

◆ refine()

◆ is_extractable()

◆ extract()

◆ deinterpret()

◆ print()

Friends And Related Symbol Documentation

◆ VStore

Member Data Documentation

◆ is_abstract_universe

◆ sequential

◆ is_totally_ordered

◆ preserve_bot

◆ preserve_top

◆ preserve_join

◆ preserve_meet

◆ injective_concretization

◆ preserve_concrete_covers

◆ name