Class ProductDomain<Product>`Abstract`

A product abstract domain as named Cartesian product of sub abstract domains. The sub abstract domains are represented by a record mapping property names to abstract domains. The Bottom element is defined as mapping every sub abstract domain to Bottom and the Top element is defined as mapping every sub abstract domain to Top.

Type Parameters

Product extends Required<AbstractProduct>
Type of the abstract product of the product domain mapping property names to abstract domains

Hierarchy (View Summary)

PartialProductDomain<Product>
- ProductDomain
  - DataFrameDomain

Hierarchy-Diagram

Index

Constructors

constructor

new ProductDomain<Product extends Required<AbstractProduct>>(
value: Product,
): ProductDomain<Product>
Type Parameters
- Product extends Required<AbstractProduct>
  Type of the abstract product of the product domain mapping property names to abstract domains
Parameters
- value: Product
Returns ProductDomain<Product>
Overrides PartialProductDomain.constructor
- Defined in src/abstract-interpretation/domains/product-domain.ts:13

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`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

`Abstract`create

create(value: Product, reduce?: boolean): this
Creates an abstract value of the lattice for a given value.
Parameters
- value: Product
- Optionalreduce: boolean
Returns this
Overrides PartialProductDomain.create
- Defined in src/abstract-interpretation/domains/product-domain.ts:17

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 ProductDomain<Product>
Returns this is ProductDomain<Product>
Inherited from PartialProductDomain.isBottom
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:147

isNotBottom

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

isNotTop

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

isNotValue

isNotValue(): this is ProductDomain<Product> & AbstractDomain<
    Product,
    Product,
    Product,
    Product,
>
Returns this is ProductDomain<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
Overrides PartialProductDomain.isTop
- Defined in src/abstract-interpretation/domains/product-domain.ts:28
isTop(): this is ProductDomain<Product>
Returns this is ProductDomain<Product>
Overrides PartialProductDomain.isTop
- Defined in src/abstract-interpretation/domains/product-domain.ts:29

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 ProductDomain<Product>
Returns this is ProductDomain<Product>
Inherited from PartialProductDomain.isValue
- Defined in src/abstract-interpretation/domains/partial-product-domain.ts:153

join

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

joinAll

joinAll(values: readonly ProductDomain<Product>[]): this
Joins the current abstract value with multiple other abstract values.
Parameters
- values: readonly ProductDomain<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: ProductDomain<Product> | Product): this
Meets the current abstract value with another abstract value by creating the greatest lower bound (GLB) in the lattice.
Parameters
- other: ProductDomain<Product> | Product
Returns this
Inherited from PartialProductDomain.meet
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:87

meetAll

meetAll(values: readonly ProductDomain<Product>[]): this
Meets the current abstract value with multiple other abstract values.
Parameters
- values: readonly ProductDomain<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
Overrides PartialProductDomain.top
- Defined in src/abstract-interpretation/domains/product-domain.ts:19

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 ProductDomain<Product>Abstract

Type Parameters

Hierarchy (View Summary)

Hierarchy-Diagram

Index

Constructors

Properties

Accessors

Methods

Constructors

constructor

Type Parameters

Parameters

Returns ProductDomain<Product>

Properties

Protected Readonly_value

Readonlydomain

Readonlyreductions

Accessors

value

Returns Lift

Methods

StaticjoinAll

Type Parameters

Parameters

Returns Domain

StaticmeetAll

Type Parameters

Parameters

Returns Domain

StatictoString

Parameters

Returns string

bottom

Returns this

Abstractcreate

Parameters

Returns this

equals

Parameters

Returns boolean

ProtectedequalsValue

Parameters

Returns boolean

isBottom

Returns boolean

Returns this is ProductDomain<Product>

isNotBottom

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

isNotTop

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

isNotValue

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

isTop

Returns boolean

Returns this is ProductDomain<Product>

isValue

Returns boolean

Returns this is ProductDomain<Product>

join

Parameters

Returns this

joinAll

Parameters

Returns this

ProtectedjoinValue

Parameters

Returns this

Protectedjsonify

Returns unknown

leq

Parameters

Returns boolean

ProtectedleqValue

Parameters

Returns boolean

meet

Parameters

Returns this

meetAll

Class ProductDomain<Product>`Abstract`

`Protected` `Readonly`_value

`Readonly`domain

`Readonly`reductions

`Static`joinAll

`Static`meetAll

`Static`toString

`Abstract`create

`Protected`equalsValue

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

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

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

`Protected`joinValue

`Protected`jsonify

`Protected`leqValue

`Protected`meetValue

`Protected`narrowValue

`Protected`reduce

`Protected`stringify

`Protected`widenValue