Class AbstractDomain<Value, Top, Bot, Lift>`Abstract`

An abstract domain as complete lattice with a widening and narrowing operator. All operations of value abstract domains should not modify the domain in-place but return new values using create.

Type Parameters

Value
Type of an abstract element of the abstract domain representing possible elements (excludes Top and Bot)
Top
Type of the Top element of the abstract domain representing all possible elements
Bot
Type of the Bottom element of the abstract domain representing no possible elements
Lift extends Value | Top | Bot = Value | Top | Bot
Type of the current abstract value in the abstract domain (defaults to Value or Top or Bot)

Hierarchy (View Summary)

AbstractDomain

Implements

Lattice<Value, Top, Bot, Lift>

Hierarchy-Diagram

Index

Constructors

constructor

new AbstractDomain<Value, Top, Bot, Lift = Value | Top | Bot>(
value: Lift,
): AbstractDomain<Value, Top, Bot, Lift>
Type Parameters
- Value
  Type of an abstract element of the abstract domain representing possible elements (excludes Top and Bot)
- Top
  Type of the Top element of the abstract domain representing all possible elements
- Bot
  Type of the Bottom element of the abstract domain representing no possible elements
- Lift = Value | Top | Bot
  Type of the current abstract value in the abstract domain (defaults to Value or Top or Bot)
Parameters
- value: Lift
Returns AbstractDomain<Value, Top, Bot, Lift>
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:22

Properties

`Protected` `Readonly`_value

_value: Lift

Accessors

value

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

Returns Lift
Implementation of Lattice.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
- 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
- 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
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:246

`Abstract`bottom

bottom(): AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
    Value,
    Top,
    Bot,
    Bot,
>
Gets the Bottom element (least element) of the complete lattice (should additionally be provided as static function).

Returns AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<Value, Top, Bot, Bot>
Implementation of Lattice.bottom
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:34

`Abstract`create

create(value: Value | Top | Bot): this
Creates an abstract value of the lattice for a given value.
Parameters
- value: Value | Top | Bot
Returns this
Implementation of Lattice.create
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:30

equals

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

`Protected` `Abstract`equalsValue

equalsValue(
this: AbstractDomain<Value, Top, Bot, Value>,
other: AbstractDomain<Value, Top, Bot, Value>,
): boolean
Parameters
- this: AbstractDomain<Value, Top, Bot, Value>
- other: AbstractDomain<Value, Top, Bot, Value>
Returns boolean
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:45

`Abstract`isBottom

isBottom(): this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
    Value,
    Top,
    Bot,
    Bot,
>
Checks whether the current abstract value is the Bottom element of the complete lattice.

Returns this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
    Value,
    Top,
    Bot,
    Bot,
>
Implementation of Lattice.isBottom
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:213

isNotBottom

isNotBottom(): this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
    Value,
    Top,
    Bot,
    Value
    | Top,
>
Returns this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
    Value,
    Top,
    Bot,
    Value
    | Top,
>
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:215

isNotTop

isNotTop(): this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
    Value,
    Top,
    Bot,
    Value
    | Bot,
>
Returns this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
    Value,
    Top,
    Bot,
    Value
    | Bot,
>
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:209

isNotValue

isNotValue(): this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
    Value,
    Top,
    Bot,
    Top
    | Bot,
>
Returns this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
    Value,
    Top,
    Bot,
    Top
    | Bot,
>
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:221

`Abstract`isTop

isTop(): this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
    Value,
    Top,
    Bot,
    Top,
>
Checks whether the current abstract value is the Top element of the complete lattice.

Returns this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
    Value,
    Top,
    Bot,
    Top,
>
Implementation of Lattice.isTop
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:207

`Abstract`isValue

isValue(): this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
    Value,
    Top,
    Bot,
    Value,
>
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 this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
    Value,
    Top,
    Bot,
    Value,
>
Implementation of Lattice.isValue
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:219

join

join(other: AbstractDomain<Value, Top, Bot, Lift> | Value | Top | Bot): this
Joins the current abstract value with another abstract value by creating the least upper bound (LUB) in the lattice.
Parameters
- other: AbstractDomain<Value, Top, Bot, Lift> | Value | Top | Bot
Returns this
Implementation of Lattice.join
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:58

joinAll

joinAll(values: readonly AbstractDomain<Value, Top, Bot, Lift>[]): this
Joins the current abstract value with multiple other abstract values.
Parameters
- values: readonly AbstractDomain<Value, Top, Bot, Lift>[]
Returns this
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:78

`Protected` `Abstract`joinValue

joinValue(
this: AbstractDomain<Value, Top, Bot, Value>,
other: AbstractDomain<Value, Top, Bot, Value>,
): this
Parameters
- this: AbstractDomain<Value, Top, Bot, Value>
- other: AbstractDomain<Value, Top, Bot, Value>
Returns this
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:73

`Protected` `Abstract`jsonify

jsonify(
    this: AbstractDomain<
        Value,
        Top,
        Bot,
        | Exclude<Value, typeof Bottom | typeof Top>
        | Exclude<Top, typeof Bottom | typeof Top>
        | Exclude<Bot, typeof Bottom | typeof Top>,
    >,
): unknown
Parameters
- this: AbstractDomain<
      Value,
      Top,
      Bot,
      | Exclude<Value, typeof Bottom | typeof Top>
      | Exclude<Top, typeof Bottom | typeof Top>
      | Exclude<Bot, typeof Bottom | typeof Top>,
  >
Returns unknown
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:194

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
Implementation of Lattice.leq
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:47

`Protected` `Abstract`leqValue

leqValue(
this: AbstractDomain<Value, Top, Bot, Value>,
other: AbstractDomain<Value, Top, Bot, Value>,
): boolean
Parameters
- this: AbstractDomain<Value, Top, Bot, Value>
- other: AbstractDomain<Value, Top, Bot, Value>
Returns boolean
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:56

meet

meet(other: AbstractDomain<Value, Top, Bot, Lift> | Value | Top | Bot): this
Meets the current abstract value with another abstract value by creating the greatest lower bound (GLB) in the lattice.
Parameters
- other: AbstractDomain<Value, Top, Bot, Lift> | Value | Top | Bot
Returns this
Implementation of Lattice.meet
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:87

meetAll

meetAll(values: readonly AbstractDomain<Value, Top, Bot, Lift>[]): this
Meets the current abstract value with multiple other abstract values.
Parameters
- values: readonly AbstractDomain<Value, Top, Bot, Lift>[]
Returns this
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:107

`Protected` `Abstract`meetValue

meetValue(
this: AbstractDomain<Value, Top, Bot, Value>,
other: AbstractDomain<Value, Top, Bot, Value>,
): this
Parameters
- this: AbstractDomain<Value, Top, Bot, Value>
- other: AbstractDomain<Value, Top, Bot, Value>
Returns this
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:102

merge

merge(
    other: this,
    merge: (first: Value, second: Value) => Value | Top | Bot,
    bottomDefault: (other: Value | Top | Bot) => Value | Top | Bot,
    topDefault: (other: Value | Top | Bot) => Value | Top | Bot,
): this
Parameters
- other: this
- merge: (first: Value, second: Value) => Value | Top | Bot
- bottomDefault: (other: Value | Top | Bot) => Value | Top | Bot
- topDefault: (other: Value | Top | Bot) => Value | Top | Bot
Returns this
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:164
merge(
    other: this,
    merge: (first: Value | Top, second: Value | Top) => Value | Top | Bot,
    bottomDefault: (other: Value | Top | Bot) => Value | Top | Bot,
): this
Parameters
- other: this
- merge: (first: Value | Top, second: Value | Top) => Value | Top | Bot
- bottomDefault: (other: Value | Top | Bot) => Value | Top | Bot
Returns this
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:165
merge(
    other: this,
    merge: (
        first: Value | Top | Bot,
        second: Value | Top | Bot,
    ) => Value | Top | Bot,
): this
Parameters
- other: this
- merge: (first: Value | Top | Bot, second: Value | Top | Bot) => Value | Top | Bot
Returns this
- 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
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:137

`Protected` `Optional`narrowValue

narrowValue?(
this: AbstractDomain<Value, Top, Bot, Value>,
other: AbstractDomain<Value, Top, Bot, Value>,
): this
Parameters
- this: AbstractDomain<Value, Top, Bot, Value>
- other: AbstractDomain<Value, Top, Bot, Value>
Returns this
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:150

`Protected` `Abstract`stringify

stringify(
    this: AbstractDomain<
        Value,
        Top,
        Bot,
        | Exclude<Value, typeof Bottom | typeof Top>
        | Exclude<Top, typeof Bottom | typeof Top>
        | Exclude<Bot, typeof Bottom | typeof Top>,
    >,
): string
Parameters
- this: AbstractDomain<
      Value,
      Top,
      Bot,
      | Exclude<Value, typeof Bottom | typeof Top>
      | Exclude<Top, typeof Bottom | typeof Top>
      | Exclude<Bot, typeof Bottom | typeof Top>,
  >
Returns string
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:205

toJSON

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

Returns unknown
Implementation of Lattice.toJSON
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:185

`Abstract`top

top(): AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
    Value,
    Top,
    Bot,
    Top,
>
Gets the Top element (greatest element) of the complete lattice (should additionally be provided as static function).

Returns AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<Value, Top, Bot, Top>
Implementation of Lattice.top
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:32

toString

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

Returns string
Implementation of Lattice.toString
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:196

transform

transform(
    transform: (value: Value) => Value | Top | Bot,
    bottomDefault: Value | Top | Bot,
    topDefault: Value | Top | Bot,
): this
Parameters
- transform: (value: Value) => Value | Top | Bot
- bottomDefault: Value | Top | Bot
- topDefault: Value | Top | Bot
Returns this
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:152
transform(
transform: (value: Value | Top) => Value | Top | Bot,
bottomDefault: Value | Top | Bot,
): this
Parameters
- transform: (value: Value | Top) => Value | Top | Bot
- bottomDefault: Value | Top | Bot
Returns this
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:153
transform(transform: (value: Value | Top | Bot) => Value | Top | Bot): this
Parameters
- transform: (value: Value | Top | Bot) => Value | Top | Bot
Returns this
- 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
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:119

`Protected` `Optional`widenValue

widenValue?(
this: AbstractDomain<Value, Top, Bot, Value>,
other: AbstractDomain<Value, Top, Bot, Value>,
): this
Parameters
- this: AbstractDomain<Value, Top, Bot, Value>
- other: AbstractDomain<Value, Top, Bot, Value>
Returns this
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:132

Class AbstractDomain<Value, Top, Bot, Lift>Abstract

Type Parameters

Hierarchy (View Summary)

Implements

Hierarchy-Diagram

Index

Constructors

Properties

Accessors

Methods

Constructors

constructor

Type Parameters

Parameters

Returns AbstractDomain<Value, Top, Bot, Lift>

Properties

Protected Readonly_value

Accessors

value

Returns Lift

Methods

StaticjoinAll

Type Parameters

Parameters

Returns Domain

StaticmeetAll

Type Parameters

Parameters

Returns Domain

StatictoString

Parameters

Returns string

Abstractbottom

Returns AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<Value, Top, Bot, Bot>

Abstractcreate

Parameters

Returns this

equals

Parameters

Returns boolean

Protected AbstractequalsValue

Parameters

Returns boolean

AbstractisBottom

Returns this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain< Value, Top, Bot, Bot,>

isNotBottom

Returns this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain< Value, Top, Bot, Value | Top,>

isNotTop

Returns this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain< Value, Top, Bot, Value | Bot,>

isNotValue

Returns this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain< Value, Top, Bot, Top | Bot,>

AbstractisTop

Returns this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain< Value, Top, Bot, Top,>

AbstractisValue

Returns this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain< Value, Top, Bot, Value,>

join

Parameters

Returns this

joinAll

Parameters

Returns this

Protected AbstractjoinValue

Parameters

Returns this

Protected Abstractjsonify

Parameters

Returns unknown

leq

Parameters

Returns boolean

Protected AbstractleqValue

Parameters

Returns boolean

meet

Parameters

Returns this

meetAll

Parameters

Returns this

Protected AbstractmeetValue

Class AbstractDomain<Value, Top, Bot, Lift>`Abstract`

`Protected` `Readonly`_value

`Static`joinAll

`Static`meetAll

`Static`toString

`Abstract`bottom

`Abstract`create

`Protected` `Abstract`equalsValue

`Abstract`isBottom

Returns this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
Value,
Top,
Bot,
Bot,
>

Returns this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
Value,
Top,
Bot,
Value
| Top,
>

Returns this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
Value,
Top,
Bot,
Value
| Bot,
>

Returns this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
Value,
Top,
Bot,
Top
| Bot,
>

`Abstract`isTop

Returns this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
Value,
Top,
Bot,
Top,
>

`Abstract`isValue

Returns this is AbstractDomain<Value, Top, Bot, Lift> & AbstractDomain<
Value,
Top,
Bot,
Value,
>

`Protected` `Abstract`joinValue

`Protected` `Abstract`jsonify

`Protected` `Abstract`leqValue

`Protected` `Abstract`meetValue

`Protected` `Optional`narrowValue

`Protected` `Abstract`stringify

`Abstract`top

`Protected` `Optional`widenValue