Class BoundedSetDomain<T, Value>

The bounded set abstract domain as sets of possible values bounded by a limit indicating the maximum number of inferred values. The Bottom element is defined as the empty set and the Top element is defined as Top symbol.

Type Parameters

T
Type of the values in the abstract domain
Value extends BoundedSetLift<T> = BoundedSetLift<T>
Type of the constraint in the abstract domain (Top, Bottom, or an actual value)

Hierarchy (View Summary)

AbstractDomain<BoundedSetValue<T>, BoundedSetTop, BoundedSetBottom, Value>
- BoundedSetDomain

Implements

ValueDomain<T>

Hierarchy-Diagram

Index

Constructors

constructor

new BoundedSetDomain<T, Value extends BoundedSetLift<T> = BoundedSetLift<T>>(
    value: Value | T[],
    limit?: number,
    setType?: typeof Set,
): BoundedSetDomain<T, Value>
Type Parameters
- T
  Type of the values in the abstract domain
- Value extends BoundedSetLift<T> = BoundedSetLift<T>
  Type of the constraint in the abstract domain (Top, Bottom, or an actual value)
Parameters
- value: Value | T[]
- limit: number = DEFAULT_INFERENCE_LIMIT
  A limit for the maximum number of elements to store in the set
- setType: typeof Set = Set
  An optional set constructor for the domain elements if the type T is not storable in a HashSet
Returns BoundedSetDomain<T, Value>
Overrides AbstractDomain.constructor
- Defined in src/abstract-interpretation/domains/bounded-set-domain.ts:36

Properties

`Protected` `Readonly`_value

_value: Value

`Readonly`limit

limit: number

`Protected` `Readonly`setType

setType: typeof Set

Accessors

value

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

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

Methods

`Static`bottom

bottom<T>(
limit?: number,
setType?: typeof Set,
): BoundedSetDomain<T, ReadonlySet<never>>
Type Parameters
- T
Parameters
- Optionallimit: number
- OptionalsetType: typeof Set
Returns BoundedSetDomain<T, ReadonlySet<never>>
- Defined in src/abstract-interpretation/domains/bounded-set-domain.ts:62

`Static`from

from<T>(
    values: T | T[],
    limit?: number,
    setType?: typeof Set,
): BoundedSetDomain<T>
Type Parameters
- T
Parameters
- values: T | T[]
- Optionallimit: number
- OptionalsetType: typeof Set
Returns BoundedSetDomain<T>
- Defined in src/abstract-interpretation/domains/bounded-set-domain.ts:66

`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 AbstractDomain.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 AbstractDomain.meetAll
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:238

`Static`top

top<T>(limit?: number, setType?: typeof Set): BoundedSetDomain<T, typeof Top>
Type Parameters
- T
Parameters
- Optionallimit: number
- OptionalsetType: typeof Set
Returns BoundedSetDomain<T, typeof Top>
- Defined in src/abstract-interpretation/domains/bounded-set-domain.ts:58

`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 AbstractDomain.toString
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:246

bottom

bottom(): BoundedSetDomain<T, Value> & BoundedSetDomain<T, ReadonlySet<never>>
Gets the Bottom element (least element) of the complete lattice (should additionally be provided as static function).

Returns BoundedSetDomain<T, Value> & BoundedSetDomain<T, ReadonlySet<never>>
Overrides AbstractDomain.bottom
- Defined in src/abstract-interpretation/domains/bounded-set-domain.ts:74

create

create(value: BoundedSetLift<T> | T[]): this
Creates an abstract value of the lattice for a given value.
Parameters
- value: BoundedSetLift<T> | T[]
Returns this
Overrides AbstractDomain.create
- Defined in src/abstract-interpretation/domains/bounded-set-domain.ts:50

equals

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

`Protected`equalsValue

equalsValue(
this: BoundedSetDomain<T, BoundedSetValue<T>>,
other: BoundedSetDomain<T, BoundedSetValue<T>>,
): boolean
Parameters
- this: BoundedSetDomain<T, BoundedSetValue<T>>
- other: BoundedSetDomain<T, BoundedSetValue<T>>
Returns boolean
Overrides AbstractDomain.equalsValue
- Defined in src/abstract-interpretation/domains/bounded-set-domain.ts:78

from

from(...values: T[]): this
Abstracts a list of concrete values into an abstract value of the value abstract domain.
Parameters
- ...values: T[]
Returns this
Implementation of ValueDomain.from
- Defined in src/abstract-interpretation/domains/bounded-set-domain.ts:54

isBottom

isBottom(): this is BoundedSetDomain<T, Value> & BoundedSetDomain<
T,
ReadonlySet<never>,
>
Checks whether the current abstract value is the Bottom element of the complete lattice.

Returns this is BoundedSetDomain<T, Value> & BoundedSetDomain<T, ReadonlySet<never>>
Overrides AbstractDomain.isBottom
- Defined in src/abstract-interpretation/domains/bounded-set-domain.ts:115

isNotBottom

isNotBottom(): this is BoundedSetDomain<T, Value> & AbstractDomain<
    BoundedSetValue<T>,
    typeof Top,
    ReadonlySet<never>,
    typeof Top | BoundedSetValue<T>,
>
Returns this is BoundedSetDomain<T, Value> & AbstractDomain<
    BoundedSetValue<T>,
    typeof Top,
    ReadonlySet<never>,
    typeof Top | BoundedSetValue<T>,
>
Inherited from AbstractDomain.isNotBottom
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:215

isNotTop

isNotTop(): this is BoundedSetDomain<T, Value> & AbstractDomain<
    BoundedSetValue<T>,
    typeof Top,
    ReadonlySet<never>,
    ReadonlySet<never> | BoundedSetValue<T>,
>
Returns this is BoundedSetDomain<T, Value> & AbstractDomain<
    BoundedSetValue<T>,
    typeof Top,
    ReadonlySet<never>,
    ReadonlySet<never> | BoundedSetValue<T>,
>
Inherited from AbstractDomain.isNotTop
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:209

isNotValue

isNotValue(): this is BoundedSetDomain<T, Value> & AbstractDomain<
    BoundedSetValue<T>,
    typeof Top,
    ReadonlySet<never>,
    typeof Top | ReadonlySet<never>,
>
Returns this is BoundedSetDomain<T, Value> & AbstractDomain<
    BoundedSetValue<T>,
    typeof Top,
    ReadonlySet<never>,
    typeof Top | ReadonlySet<never>,
>
Inherited from AbstractDomain.isNotValue
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:221

isTop

isTop(): this is BoundedSetDomain<T, Value> & BoundedSetDomain<T, typeof Top>
Checks whether the current abstract value is the Top element of the complete lattice.

Returns this is BoundedSetDomain<T, Value> & BoundedSetDomain<T, typeof Top>
Overrides AbstractDomain.isTop
- Defined in src/abstract-interpretation/domains/bounded-set-domain.ts:111

isValue

isValue(): this is BoundedSetDomain<T, Value> & BoundedSetDomain<
T,
BoundedSetValue<T>,
>
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 BoundedSetDomain<T, Value> & BoundedSetDomain<T, BoundedSetValue<T>>
Overrides AbstractDomain.isValue
- Defined in src/abstract-interpretation/domains/bounded-set-domain.ts:119

join

join(
    other:
        | typeof Top
        | ReadonlySet<never>
        | BoundedSetValue<T>
        | BoundedSetDomain<T, Value>,
): this
Joins the current abstract value with another abstract value by creating the least upper bound (LUB) in the lattice.
Parameters
- other:
      | typeof Top
      | ReadonlySet<never>
      | BoundedSetValue<T>
      | BoundedSetDomain<T, Value>
Returns this
Inherited from AbstractDomain.join
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:58

joinAll

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

`Protected`joinValue

joinValue(
    this: BoundedSetDomain<T, Value> & BoundedSetDomain<
        T,
        BoundedSetValue<T>,
    >,
    other: BoundedSetDomain<T, BoundedSetValue<T>>,
): this
Parameters
- this: BoundedSetDomain<T, Value> & BoundedSetDomain<T, BoundedSetValue<T>>
- other: BoundedSetDomain<T, BoundedSetValue<T>>
Returns this
Overrides AbstractDomain.joinValue
- Defined in src/abstract-interpretation/domains/bounded-set-domain.ts:86

`Protected`jsonify

jsonify(this: BoundedSetDomain<T, BoundedSetValue<T>>): unknown
Parameters
- this: BoundedSetDomain<T, BoundedSetValue<T>>
Returns unknown
Overrides AbstractDomain.jsonify
- Defined in src/abstract-interpretation/domains/bounded-set-domain.ts:103

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

`Protected`leqValue

leqValue(
this: BoundedSetDomain<T, BoundedSetValue<T>>,
other: BoundedSetDomain<T, BoundedSetValue<T>>,
): boolean
Parameters
- this: BoundedSetDomain<T, BoundedSetValue<T>>
- other: BoundedSetDomain<T, BoundedSetValue<T>>
Returns boolean
Overrides AbstractDomain.leqValue
- Defined in src/abstract-interpretation/domains/bounded-set-domain.ts:82

meet

meet(
    other:
        | typeof Top
        | ReadonlySet<never>
        | BoundedSetValue<T>
        | BoundedSetDomain<T, Value>,
): this
Meets the current abstract value with another abstract value by creating the greatest lower bound (GLB) in the lattice.
Parameters
- other:
      | typeof Top
      | ReadonlySet<never>
      | BoundedSetValue<T>
      | BoundedSetDomain<T, Value>
Returns this
Inherited from AbstractDomain.meet
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:87

meetAll

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

`Protected`meetValue

meetValue(
    this: BoundedSetDomain<T, Value> & BoundedSetDomain<
        T,
        BoundedSetValue<T>,
    >,
    other: BoundedSetDomain<T, BoundedSetValue<T>>,
): this
Parameters
- this: BoundedSetDomain<T, Value> & BoundedSetDomain<T, BoundedSetValue<T>>
- other: BoundedSetDomain<T, BoundedSetValue<T>>
Returns this
Overrides AbstractDomain.meetValue
- Defined in src/abstract-interpretation/domains/bounded-set-domain.ts:90

merge

merge(
    other: this,
    merge: (
        first: BoundedSetValue,
        second: BoundedSetValue,
    ) => typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
    bottomDefault: (
        other: typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
    ) => typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
    topDefault: (
        other: typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
    ) => typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
): this
Parameters
- other: this
- merge: (
  first: BoundedSetValue,
  second: BoundedSetValue,
  ) => typeof Top | ReadonlySet<never> | BoundedSetValue<T>
- bottomDefault: (
  other: typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
  ) => typeof Top | ReadonlySet<never> | BoundedSetValue<T>
- topDefault: (
  other: typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
  ) => typeof Top | ReadonlySet<never> | BoundedSetValue<T>
Returns this
Inherited from AbstractDomain.merge
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:164
merge(
    other: this,
    merge: (
        first: typeof Top | BoundedSetValue<T>,
        second: typeof Top | BoundedSetValue<T>,
    ) => typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
    bottomDefault: (
        other: typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
    ) => typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
): this
Parameters
- other: this
- merge: (
  first: typeof Top | BoundedSetValue<T>,
  second: typeof Top | BoundedSetValue<T>,
  ) => typeof Top | ReadonlySet<never> | BoundedSetValue<T>
- bottomDefault: (
  other: typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
  ) => typeof Top | ReadonlySet<never> | BoundedSetValue<T>
Returns this
Inherited from AbstractDomain.merge
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:165
merge(
    other: this,
    merge: (
        first: typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
        second: typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
    ) => typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
): this
Parameters
- other: this
- merge: (
  first: typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
  second: typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
  ) => typeof Top | ReadonlySet<never> | BoundedSetValue<T>
Returns this
Inherited from AbstractDomain.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 AbstractDomain.narrow
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:137

`Protected` `Optional`narrowValue

narrowValue?(
    this: AbstractDomain<
        BoundedSetValue<T>,
        typeof Top,
        ReadonlySet<never>,
        BoundedSetValue<T>,
    >,
    other: AbstractDomain<
        BoundedSetValue<T>,
        typeof Top,
        ReadonlySet<never>,
        BoundedSetValue<T>,
    >,
): this
Parameters
- this: AbstractDomain<
      BoundedSetValue<T>,
      typeof Top,
      ReadonlySet<never>,
      BoundedSetValue<T>,
  >
- other: AbstractDomain<
      BoundedSetValue<T>,
      typeof Top,
      ReadonlySet<never>,
      BoundedSetValue<T>,
  >
Returns this
Inherited from AbstractDomain.narrowValue
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:150

satisfies

satisfies(value: T): Ternary
Checks whether the current abstract value satisfies a concrete value (i.e. includes a concrete value).
Parameters
- value: T
Returns Ternary
See
Ternary for the returned satisfiability result
Implementation of ValueDomain.satisfies
- Defined in src/abstract-interpretation/domains/bounded-set-domain.ts:94

`Protected`stringify

stringify(this: BoundedSetDomain<T, BoundedSetValue<T>>): string
Parameters
- this: BoundedSetDomain<T, BoundedSetValue<T>>
Returns string
Overrides AbstractDomain.stringify
- Defined in src/abstract-interpretation/domains/bounded-set-domain.ts:107

toJSON

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

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

top

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

Returns BoundedSetDomain<T, Value> & BoundedSetDomain<T, typeof Top>
Overrides AbstractDomain.top
- Defined in src/abstract-interpretation/domains/bounded-set-domain.ts:70

toString

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

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

transform

transform(
    transform: (
        value: BoundedSetValue,
    ) => typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
    bottomDefault: typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
    topDefault: typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
): this
Parameters
- transform: (value: BoundedSetValue) => typeof Top | ReadonlySet<never> | BoundedSetValue<T>
- bottomDefault: typeof Top | ReadonlySet<never> | BoundedSetValue<T>
- topDefault: typeof Top | ReadonlySet<never> | BoundedSetValue<T>
Returns this
Inherited from AbstractDomain.transform
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:152
transform(
    transform: (
        value: typeof Top | BoundedSetValue<T>,
    ) => typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
    bottomDefault: typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
): this
Parameters
- transform: (
  value: typeof Top | BoundedSetValue<T>,
  ) => typeof Top | ReadonlySet<never> | BoundedSetValue<T>
- bottomDefault: typeof Top | ReadonlySet<never> | BoundedSetValue<T>
Returns this
Inherited from AbstractDomain.transform
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:153
transform(
    transform: (
        value: typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
    ) => typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
): this
Parameters
- transform: (
  value: typeof Top | ReadonlySet<never> | BoundedSetValue<T>,
  ) => typeof Top | ReadonlySet<never> | BoundedSetValue<T>
Returns this
Inherited from AbstractDomain.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 AbstractDomain.widen
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:119

`Protected` `Optional`widenValue

widenValue?(
    this: AbstractDomain<
        BoundedSetValue<T>,
        typeof Top,
        ReadonlySet<never>,
        BoundedSetValue<T>,
    >,
    other: AbstractDomain<
        BoundedSetValue<T>,
        typeof Top,
        ReadonlySet<never>,
        BoundedSetValue<T>,
    >,
): this
Parameters
- this: AbstractDomain<
      BoundedSetValue<T>,
      typeof Top,
      ReadonlySet<never>,
      BoundedSetValue<T>,
  >
- other: AbstractDomain<
      BoundedSetValue<T>,
      typeof Top,
      ReadonlySet<never>,
      BoundedSetValue<T>,
  >
Returns this
Inherited from AbstractDomain.widenValue
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:132

Class BoundedSetDomain<T, Value>

Type Parameters

Hierarchy (View Summary)

Implements

Hierarchy-Diagram

Index

Constructors

Properties

Accessors

Methods

Constructors

constructor

Type Parameters

Parameters

Returns BoundedSetDomain<T, Value>

Properties

Protected Readonly_value

Readonlylimit

Protected ReadonlysetType

Accessors

value

Returns Lift

Methods

Staticbottom

Type Parameters

Parameters

Returns BoundedSetDomain<T, ReadonlySet<never>>

Staticfrom

Type Parameters

Parameters

Returns BoundedSetDomain<T>

StaticjoinAll

Type Parameters

Parameters

Returns Domain

StaticmeetAll

Type Parameters

Parameters

Returns Domain

Statictop

Type Parameters

Parameters

Returns BoundedSetDomain<T, typeof Top>

StatictoString

Parameters

Returns string

bottom

Returns BoundedSetDomain<T, Value> & BoundedSetDomain<T, ReadonlySet<never>>

create

Parameters

Returns this

equals

Parameters

Returns boolean

ProtectedequalsValue

Parameters

Returns boolean

from

Parameters

Returns this

isBottom

Returns this is BoundedSetDomain<T, Value> & BoundedSetDomain<T, ReadonlySet<never>>

isNotBottom

Returns this is BoundedSetDomain<T, Value> & AbstractDomain< BoundedSetValue<T>, typeof Top, ReadonlySet<never>, typeof Top | BoundedSetValue<T>,>

isNotTop

Returns this is BoundedSetDomain<T, Value> & AbstractDomain< BoundedSetValue<T>, typeof Top, ReadonlySet<never>, ReadonlySet<never> | BoundedSetValue<T>,>

isNotValue

Returns this is BoundedSetDomain<T, Value> & AbstractDomain< BoundedSetValue<T>, typeof Top, ReadonlySet<never>, typeof Top | ReadonlySet<never>,>

isTop

Returns this is BoundedSetDomain<T, Value> & BoundedSetDomain<T, typeof Top>

isValue

Returns this is BoundedSetDomain<T, Value> & BoundedSetDomain<T, BoundedSetValue<T>>

join

Parameters

Returns this

joinAll

Parameters

Returns this

ProtectedjoinValue

Parameters

`Protected` `Readonly`_value

`Readonly`limit

`Protected` `Readonly`setType

`Static`bottom

`Static`from

`Static`joinAll

`Static`meetAll

`Static`top

`Static`toString

`Protected`equalsValue

Returns this is BoundedSetDomain<T, Value> & AbstractDomain<
BoundedSetValue<T>,
typeof Top,
ReadonlySet<never>,
typeof Top | BoundedSetValue<T>,
>

Returns this is BoundedSetDomain<T, Value> & AbstractDomain<
BoundedSetValue<T>,
typeof Top,
ReadonlySet<never>,
ReadonlySet<never> | BoundedSetValue<T>,
>

Returns this is BoundedSetDomain<T, Value> & AbstractDomain<
BoundedSetValue<T>,
typeof Top,
ReadonlySet<never>,
typeof Top | ReadonlySet<never>,
>

`Protected`joinValue

`Protected`jsonify

`Protected`leqValue

`Protected`meetValue

`Protected` `Optional`narrowValue

`Protected`stringify

`Protected` `Optional`widenValue