Class MultiValueStateDomain<Product, Value>

Readonlydomain

value

• get value(): Value

  The current abstract value of the lattice.

  Returns Value

Staticbottom

• bottom<
      Domain extends AnyAbstractDomain,
      StateDomain extends StateAbstractDomain<Domain, typeof Bottom>,
  >(
      this: new (value: typeof Bottom, domain: Domain) => StateDomain,
      domain: Domain,
  ): StateDomain

  Type Parameters

  • Domain extends AnyAbstractDomain
  • StateDomain extends StateAbstractDomain<Domain, typeof Bottom>

  Parameters

  • this: new (value: typeof Bottom, domain: Domain) => StateDomain
  • domain: Domain

  Returns StateDomain

StaticjoinAll

• 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

StaticmeetAll

• 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

Statictop

• top<
      Domain extends AnyAbstractDomain,
      StateDomain extends StateAbstractDomain<Domain, StateDomainTop>,
  >(
      this: new (value: StateDomainTop, domain: Domain) => StateDomain,
      domain: Domain,
  ): StateDomain

  Type Parameters

  • Domain extends AnyAbstractDomain
  • StateDomain extends StateAbstractDomain<Domain, StateDomainTop>

  Parameters

  • this: new (value: StateDomainTop, domain: Domain) => StateDomain
  • domain: Domain

  Returns StateDomain

StatictoString

• toString(this: void, value: unknown): string

  Converts an element of an abstract domain into a string.

  Parameters

  • this: void
  • value: unknown

  Returns string

abstract

• abstract(
      concrete:
          | typeof Top
          | ReadonlySet<ConcreteState<MultiValueDomain<Product>>>,
  ): this

  Maps a set of possible concrete values into an abstract value as abstraction function of the abstract domain (should additionally be provided as static function).

  Parameters

  • concrete: typeof Top | ReadonlySet<ConcreteState<MultiValueDomain<Product>>>

  Returns this

bottom

• bottom(): MultiValueStateDomain<Product, Value> & StateAbstractDomain<
      MultiValueDomain<Product>,
      typeof Bottom,
  >

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

  Returns MultiValueStateDomain<Product, Value> & StateAbstractDomain<
      MultiValueDomain<Product>,
      typeof Bottom,
  >

concretize

• concretize(
      limit: number,
  ): typeof Top | ReadonlySet<ConcreteState<MultiValueDomain<Product>>>

  Maps the current abstract value into a set of possible concrete values as concretization function of the abstract domain. The result should be Top if the number of concrete values would reach the limit or the resulting set would have infinite many elements.

  Parameters

  • limit: number

  Returns typeof Top | ReadonlySet<ConcreteState<MultiValueDomain<Product>>>

equals

• equals(other: this): boolean

  Checks whether the current abstract value equals to another abstract value.

  Parameters

  • other: this

  Returns boolean

get

• get(node: NodeId): MultiValueDomain<Product> | undefined

  Gets the inferred abstract value for an AST node ID.

  Parameters

  • node: NodeId

  Returns MultiValueDomain<Product> | undefined

has

• has(node: NodeId): boolean

  Checks whether the state domain has an inferred value for an AST node ID.

  Parameters

  • node: NodeId

  Returns boolean

isBottom

• isBottom(): this is MultiValueStateDomain<Product, Value> & StateAbstractDomain<
      MultiValueDomain<Product>,
      typeof Bottom,
  >

  Checks whether the current abstract value is the Bottom element of the complete lattice.

  Returns this is MultiValueStateDomain<Product, Value> & StateAbstractDomain<
      MultiValueDomain<Product>,
      typeof Bottom,
  >

isTop

• isTop(): this is MultiValueStateDomain<Product, Value> & StateAbstractDomain<
      MultiValueDomain<Product>,
      StateDomainTop,
  >

  Checks whether the current abstract value is the Top element of the complete lattice.

  Returns this is MultiValueStateDomain<Product, Value> & StateAbstractDomain<
      MultiValueDomain<Product>,
      StateDomainTop,
  >

isValue

• isValue(): this is MultiValueStateDomain<Product, Value> & StateAbstractDomain<
      MultiValueDomain<Product>,
      StateDomainValue<MultiValueDomain<Product>>,
  >

  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 MultiValueStateDomain<Product, Value> & StateAbstractDomain<
      MultiValueDomain<Product>,
      StateDomainValue<MultiValueDomain<Product>>,
  >

join

• join(other: this): this

  Joins the current abstract value with another abstract value by creating the least upper bound (LUB) in the lattice.

  Parameters

  • other: this

  Returns this

joinAll

• joinAll(values: readonly MultiValueStateDomain<Product, Value>[]): this

  Joins the current abstract value with multiple other abstract values.

  Parameters

  • values: readonly MultiValueStateDomain<Product, Value>[]

  Returns this

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

meet

• meet(other: this): this

  Meets the current abstract value with another abstract value by creating the greatest lower bound (GLB) in the lattice.

  Parameters

  • other: this

  Returns this

meetAll

• meetAll(values: readonly MultiValueStateDomain<Product, Value>[]): this

  Meets the current abstract value with multiple other abstract values.

  Parameters

  • values: readonly MultiValueStateDomain<Product, Value>[]

  Returns this

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

remove

• remove(node: NodeId): void

  Removes the inferred value for an AST node ID from the state domain.

  Parameters

  • node: NodeId

  Returns void

set

• set(node: NodeId, value: MultiValueDomain): void

  Sets the inferred value for an AST node ID from the state domain.

  Parameters

  • node: NodeId
  • value: MultiValueDomain

  Returns void

toJson

• toJson(): unknown

  Converts the lattice into a JSON serializable value.

  Returns unknown

top

• top(): MultiValueStateDomain<Product, Value> & StateAbstractDomain<
      MultiValueDomain<Product>,
      StateDomainTop,
  >

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

  Returns MultiValueStateDomain<Product, Value> & StateAbstractDomain<
      MultiValueDomain<Product>,
      StateDomainTop,
  >

toString

• toString(): string

  Converts the lattice into a human-readable string.

  Returns string

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