Class MultiValueDomain<Product>

A multi-value abstract domain as a (partial) product domain that combines multiple abstract domains. The Bottom element is defined as mapping every sub abstract domain to Bottom and the Top element is defined as having no sub abstract domain value.

See

MultiValueStateDomain for a state abstract domain of a multi-value domain

Type Parameters

Product extends AbstractProduct
Type of the abstract product of the multi-value domain combining multiple abstract values

Hierarchy (View Summary)

PartialProductDomain<Product>
- MultiValueDomain

Index

Constructors

constructor

new MultiValueDomain<Product extends AbstractProduct>(
    value: Product,
    domain: Required<Product>,
    reductions?: readonly ProductReduction<Product>[],
): MultiValueDomain<Product>
Type Parameters
- Product extends AbstractProduct
  Type of the abstract product of the multi-value domain combining multiple abstract values
Parameters
- value: Product
- domain: Required<Product>
- reductions: readonly ProductReduction<Product>[] = []
Returns MultiValueDomain<Product>
Overrides PartialProductDomain.constructor
- Defined in src/abstract-interpretation/domains/multi-value-state-domain.ts:51

Properties

`Protected` `Readonly`_value

_value: Product

`Readonly`domain

domain: Required<Product>

`Readonly`reductions

reductions: readonly ProductReduction<Product>[]

Accessors

value

get value(): Lift
The current abstract value of the lattice.

Returns Lift
Inherited from PartialProductDomain.value
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:26

Methods

`Static`joinAll

joinAll<Domain extends AnyAbstractDomain>(
values: Domain[],
defaultValue?: Domain,
): Domain
Joins an array of abstract values by joining the first abstract value with the other values in the array. The provided array of abstract values must not be empty or a default value must be provided!
Type Parameters
- Domain extends AnyAbstractDomain
Parameters
- values: Domain[]
- OptionaldefaultValue: Domain
Returns Domain
Inherited from PartialProductDomain.joinAll
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:229

`Static`meetAll

meetAll<Domain extends AnyAbstractDomain>(
values: Domain[],
defaultValue?: Domain,
): Domain
Meets an array of abstract values by meeting the first abstract value with the other values in the array. The provided array of abstract values must not be empty or a default value must be provided!
Type Parameters
- Domain extends AnyAbstractDomain
Parameters
- values: Domain[]
- OptionaldefaultValue: Domain
Returns Domain
Inherited from PartialProductDomain.meetAll
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:238

`Static`top

top<Product extends AbstractProduct>(
domain: Required<Product>,
reductions?: readonly ProductReduction<Product>[],
): MultiValueDomain<Product>
Type Parameters
- Product extends AbstractProduct
Parameters
- domain: Required<Product>
- reductions: readonly ProductReduction<Product>[] = []
Returns MultiValueDomain<Product>
- Defined in src/abstract-interpretation/domains/multi-value-state-domain.ts:59

`Static`toString

toString(this: void, value: unknown): string
Converts an element of an abstract domain into a string.
Parameters
- this: void
- value: unknown
Returns string
Inherited from PartialProductDomain.toString
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:246

bottom

bottom(): this
Gets the Bottom element (least element) of the complete lattice (should additionally be provided as static function).

Returns this
Inherited from PartialProductDomain.bottom
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:39

create

create(value: Product): this
Creates an abstract value of the lattice for a given value.
Parameters
- value: Product
Returns this
Overrides PartialProductDomain.create
- Defined in src/abstract-interpretation/domains/multi-value-state-domain.ts:55

equals

equals(other: this): boolean
Checks whether the current abstract value equals to another abstract value.
Parameters
- other: this
Returns boolean
Inherited from PartialProductDomain.equals
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:36

`Protected`equalsValue

equalsValue(other: this): boolean
Parameters
- other: this
Returns boolean
Inherited from PartialProductDomain.equalsValue
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:52

isBottom

isBottom(): boolean
Checks whether the current abstract value is the Bottom element of the complete lattice.

Returns boolean
Inherited from PartialProductDomain.isBottom
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:146
isBottom(): this is MultiValueDomain<Product>
Returns this is MultiValueDomain<Product>
Inherited from PartialProductDomain.isBottom
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:147

isNotBottom

isNotBottom(): this is MultiValueDomain<Product> & AbstractDomain<
    Product,
    Product,
    Product,
    Product,
>
Returns this is MultiValueDomain<Product> & AbstractDomain<
    Product,
    Product,
    Product,
    Product,
>
Inherited from PartialProductDomain.isNotBottom
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:215

isNotTop

isNotTop(): this is MultiValueDomain<Product> & AbstractDomain<
    Product,
    Product,
    Product,
    Product,
>
Returns this is MultiValueDomain<Product> & AbstractDomain<
    Product,
    Product,
    Product,
    Product,
>
Inherited from PartialProductDomain.isNotTop
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:209

isNotValue

isNotValue(): this is MultiValueDomain<Product> & AbstractDomain<
    Product,
    Product,
    Product,
    Product,
>
Returns this is MultiValueDomain<Product> & AbstractDomain<
    Product,
    Product,
    Product,
    Product,
>
Inherited from PartialProductDomain.isNotValue
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:221

isTop

isTop(): boolean
Checks whether the current abstract value is the Top element of the complete lattice.

Returns boolean
Inherited from PartialProductDomain.isTop
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:140
isTop(): this is MultiValueDomain<Product>
Returns this is MultiValueDomain<Product>
Inherited from PartialProductDomain.isTop
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:141

isValue

isValue(): boolean
Checks whether the current abstract value is an actual value of the complete lattice (this may include the Top or Bottom element if they are also values and no separate symbols, for example).

Returns boolean
Inherited from PartialProductDomain.isValue
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:152
isValue(): this is MultiValueDomain<Product>
Returns this is MultiValueDomain<Product>
Inherited from PartialProductDomain.isValue
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:153

join

join(other: MultiValueDomain<Product> | Product): this
Joins the current abstract value with another abstract value by creating the least upper bound (LUB) in the lattice.
Parameters
- other: MultiValueDomain<Product> | Product
Returns this
Inherited from PartialProductDomain.join
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:58

joinAll

joinAll(values: readonly MultiValueDomain<Product>[]): this
Joins the current abstract value with multiple other abstract values.
Parameters
- values: readonly MultiValueDomain<Product>[]
Returns this
Inherited from PartialProductDomain.joinAll
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:78

`Protected`joinValue

joinValue(other: this): this
Parameters
- other: this
Returns this
Inherited from PartialProductDomain.joinValue
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:80

`Protected`jsonify

jsonify(): unknown
Returns unknown
Inherited from PartialProductDomain.jsonify
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:132

leq

leq(other: this): boolean
Checks whether the current abstract value is less than or equal to another abstract value with respect to the partial order of the lattice.
Parameters
- other: this
Returns boolean
Inherited from PartialProductDomain.leq
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:47

`Protected`leqValue

leqValue(other: this): boolean
Parameters
- other: this
Returns boolean
Inherited from PartialProductDomain.leqValue
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:66

meet

meet(other: MultiValueDomain<Product> | Product): this
Meets the current abstract value with another abstract value by creating the greatest lower bound (GLB) in the lattice.
Parameters
- other: MultiValueDomain<Product> | Product
Returns this
Inherited from PartialProductDomain.meet
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:87

meetAll

meetAll(values: readonly MultiValueDomain<Product>[]): this
Meets the current abstract value with multiple other abstract values.
Parameters
- values: readonly MultiValueDomain<Product>[]
Returns this
Inherited from PartialProductDomain.meetAll
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:107

`Protected`meetValue

meetValue(other: this): this
Parameters
- other: this
Returns this
Inherited from PartialProductDomain.meetValue
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:91

merge

merge(
    other: this,
    merge: (first: Product, second: Product) => Product,
    bottomDefault: (other: Product) => Product,
    topDefault: (other: Product) => Product,
): this
Parameters
- other: this
- merge: (first: Product, second: Product) => Product
- bottomDefault: (other: Product) => Product
- topDefault: (other: Product) => Product
Returns this
Inherited from PartialProductDomain.merge
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:164
merge(
    other: this,
    merge: (first: Product, second: Product) => Product,
    bottomDefault: (other: Product) => Product,
): this
Parameters
- other: this
- merge: (first: Product, second: Product) => Product
- bottomDefault: (other: Product) => Product
Returns this
Inherited from PartialProductDomain.merge
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:165
merge(other: this, merge: (first: Product, second: Product) => Product): this
Parameters
- other: this
- merge: (first: Product, second: Product) => Product
Returns this
Inherited from PartialProductDomain.merge
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:166

narrow

narrow(other: this): this
Narrows the current abstract value with another abstract value as a sound over-approximation of the meet (greatest lower bound) to refine the value after widening.
Parameters
- other: this
Returns this
Inherited from PartialProductDomain.narrow
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:137

`Protected`narrowValue

narrowValue(other: this): this
Parameters
- other: this
Returns this
Inherited from PartialProductDomain.narrowValue
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:117

`Protected`reduce

reduce(value: Product): Product
Applies the reductions of the (reduced) product domain to refine the abstract value based on its components. Subclasses may override this to implement a fixed reduction instead of (or in addition to) the configurable reductions.
Parameters
- value: Product
Returns Product
Inherited from PartialProductDomain.reduce
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:162

`Protected`stringify

stringify(): string
Returns string
Inherited from PartialProductDomain.stringify
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:136

toJSON

toJSON(): unknown
Converts the lattice into a JSON serializable value.

Returns unknown
Inherited from PartialProductDomain.toJSON
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:185

top

top(): this
Gets the Top element (greatest element) of the complete lattice (should additionally be provided as static function).

Returns this
Inherited from PartialProductDomain.top
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:48

toString

toString(): string
Converts the lattice into a human-readable string.

Returns string
Inherited from PartialProductDomain.toString
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:196

transform

transform(
    transform: (value: Product) => Product,
    bottomDefault: Product,
    topDefault: Product,
): this
Parameters
- transform: (value: Product) => Product
- bottomDefault: Product
- topDefault: Product
Returns this
Inherited from PartialProductDomain.transform
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:152
transform(transform: (value: Product) => Product, bottomDefault: Product): this
Parameters
- transform: (value: Product) => Product
- bottomDefault: Product
Returns this
Inherited from PartialProductDomain.transform
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:153
transform(transform: (value: Product) => Product): this
Parameters
- transform: (value: Product) => Product
Returns this
Inherited from PartialProductDomain.transform
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:154

widen

widen(other: this): this
Widens the current abstract value with another abstract value as a sound over-approximation of the join (least upper bound) for fixpoint iteration acceleration.
Parameters
- other: this
Returns this
Inherited from PartialProductDomain.widen
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:119

`Protected`widenValue

widenValue(other: this): this
Parameters
- other: this
Returns this
Inherited from PartialProductDomain.widenValue
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:106

Class MultiValueDomain<Product>

See

Type Parameters

Hierarchy (View Summary)

Index

Constructors

Properties

Accessors

Methods

Constructors

constructor

Type Parameters

Parameters

Returns MultiValueDomain<Product>

Properties

Protected Readonly_value

Readonlydomain

Readonlyreductions

Accessors

value

Returns Lift

Methods

StaticjoinAll

Type Parameters

Parameters

Returns Domain

StaticmeetAll

Type Parameters

Parameters

Returns Domain

Statictop

Type Parameters

Parameters

Returns MultiValueDomain<Product>

StatictoString

Parameters

Returns string

bottom

Returns this

create

Parameters

Returns this

equals

Parameters

Returns boolean

ProtectedequalsValue

Parameters

Returns boolean

isBottom

Returns boolean

Returns this is MultiValueDomain<Product>

isNotBottom

Returns this is MultiValueDomain<Product> & AbstractDomain< Product, Product, Product, Product,>

isNotTop

Returns this is MultiValueDomain<Product> & AbstractDomain< Product, Product, Product, Product,>

isNotValue

Returns this is MultiValueDomain<Product> & AbstractDomain< Product, Product, Product, Product,>

isTop

Returns boolean

Returns this is MultiValueDomain<Product>

isValue

Returns boolean

Returns this is MultiValueDomain<Product>

join

Parameters

Returns this

joinAll

Parameters

Returns this

ProtectedjoinValue

Parameters

Returns this

Protectedjsonify

Returns unknown

leq

Parameters

Returns boolean

ProtectedleqValue

Parameters

Returns boolean

`Protected` `Readonly`_value

`Readonly`domain

`Readonly`reductions

`Static`joinAll

`Static`meetAll

`Static`top

`Static`toString

`Protected`equalsValue

Returns this is MultiValueDomain<Product> & AbstractDomain<
Product,
Product,
Product,
Product,
>

Returns this is MultiValueDomain<Product> & AbstractDomain<
Product,
Product,
Product,
Product,
>

Returns this is MultiValueDomain<Product> & AbstractDomain<
Product,
Product,
Product,
Product,
>

`Protected`joinValue

`Protected`jsonify

`Protected`leqValue

`Protected`meetValue

`Protected`narrowValue

`Protected`reduce

`Protected`stringify

`Protected`widenValue