Class SetRangeDomain<T, Value>
Type Parameters
- T
Type of the values in the sets in the abstract domain
- Value extends SetRangeLift<T> = SetRangeLift<T>
Type of the constraint in the abstract domain (Top, Bottom, or an actual value)
Hierarchy (View Summary)
- AbstractDomain<SetRangeValue<T>, SetRangeTop, SetRangeBottom, Value>
- SetRangeDomain
Implements
Hierarchy-Diagram
Index
Constructors
Properties
Accessors
Methods
Constructors
constructor
- new SetRangeDomain<T, Value extends SetRangeLift<T> = SetRangeLift<T>>(
value: Value | ArrayRangeValue<T>,
limit?: number | SetRangeLimit,
setType?: typeof Set,
): SetRangeDomain<T, Value>Type Parameters
- T
Type of the values in the sets in the abstract domain
- Value extends SetRangeLift<T> = SetRangeLift<T>
Type of the constraint in the abstract domain (Top, Bottom, or an actual value)
Parameters
- value: Value | ArrayRangeValue<T>
- limit: number | SetRangeLimit = DEFAULT_INFERENCE_LIMIT
A limit for the maximum number of elements to store in the must set and may set before over-approximation
- setType: typeof Set = Set
Returns SetRangeDomain<T, Value>
- T
Accessors
may
The set of values that may be present in the set (can be Top).
Returns SetRangeMaySet<T, Value>
must
The set of values that must be present in the set.
Returns SetRangeMustSet<T, Value>
value
The current abstract value of the lattice.
Returns Lift
Methods
Staticbottom
Type Parameters
- T
Parameters
Optionallimit: number | SetRangeLimitOptionalsetType: typeof Set
Returns SetRangeDomain<T, typeof Bottom>
Staticfrom
- from<T>(
values: Set<T> | T[] | Set<T>[] | T[][],
limit?: number | SetRangeLimit,
setType?: typeof Set,
): SetRangeDomain<T>Type Parameters
- T
Parameters
- values: Set<T> | T[] | Set<T>[] | T[][]
Optionallimit: number | SetRangeLimitOptionalsetType: typeof Set
Returns SetRangeDomain<T>
Staticjoin
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
Returns Domain
Staticmeet
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
Returns Domain
Statictop
- top<T>(
limit?: number | SetRangeLimit,
setType?: typeof Set,
): SetRangeDomain<T, { may: typeof Top; must: Set<never> }>Type Parameters
- T
Parameters
Optionallimit: number | SetRangeLimitOptionalsetType: typeof Set
Returns SetRangeDomain<T, { may: typeof Top; must: Set<never> }>
Staticto
Converts an element of an abstract domain into a string.
Parameters
- this: void
- value: unknown
Returns string
bottom
Gets the Bottom element (least element) of the complete lattice (should additionally be provided as static function).
Returns SetRangeDomain<T, Value> & SetRangeDomain<T, typeof Bottom>
create
Creates an abstract value of the lattice for a given value.
Parameters
- value: SetRangeLift<T> | ArrayRangeValue<T>
Returns this
equals
Checks whether the current abstract value equals to another abstract value.
Parameters
- other: this
Returns boolean
Protectedequals
- equalsValue(
this: SetRangeDomain<T, SetRangeValue<T>>,
other: SetRangeDomain<T, SetRangeValue<T>>,
): booleanParameters
- this: SetRangeDomain<T, SetRangeValue<T>>
- other: SetRangeDomain<T, SetRangeValue<T>>
Returns boolean
from
intersect
Creates the intersection between this set abstract value and another set abstract value.
Parameters
- other: SetRangeDomain<T, Value> | SetRangeLift<T> | ArrayRangeValue<T>
Returns this
is
Checks whether the current abstract value is the Bottom element of the complete lattice.
Returns this is SetRangeDomain<T, Value> & SetRangeDomain<T, typeof Bottom>
is
Returns this is SetRangeDomain<T, Value> & SetRangeDomain<T, SetRangeFinite<T>>
is
- isInfinite(): this is SetRangeDomain<T, Value> & SetRangeDomain<
T,
{ may: typeof Top; must: ReadonlySet<T> },
>Returns this is SetRangeDomain<T, Value> & SetRangeDomain<
T,
{ may: typeof Top; must: ReadonlySet<T> },
>
is
- isNotBottom(): this is SetRangeDomain<T, Value> & AbstractDomain<
SetRangeValue<T>,
{ may: typeof Top; must: Set<never> },
typeof Bottom,
{ may: typeof Top; must: Set<never> } | SetRangeValue<T>,
>Returns this is SetRangeDomain<T, Value> & AbstractDomain<
SetRangeValue<T>,
{ may: typeof Top; must: Set<never> },
typeof Bottom,
{ may: typeof Top; must: Set<never> } | SetRangeValue<T>,
>
is
- isNotTop(): this is SetRangeDomain<T, Value> & AbstractDomain<
SetRangeValue<T>,
{ may: typeof Top; must: Set<never> },
typeof Bottom,
typeof Bottom | SetRangeValue<T>,
>Returns this is SetRangeDomain<T, Value> & AbstractDomain<
SetRangeValue<T>,
{ may: typeof Top; must: Set<never> },
typeof Bottom,
typeof Bottom | SetRangeValue<T>,
>
is
- isNotValue(): this is SetRangeDomain<T, Value> & AbstractDomain<
SetRangeValue<T>,
{ may: typeof Top; must: Set<never> },
typeof Bottom,
typeof Bottom | { may: typeof Top; must: Set<never> },
>Returns this is SetRangeDomain<T, Value> & AbstractDomain<
SetRangeValue<T>,
{ may: typeof Top; must: Set<never> },
typeof Bottom,
typeof Bottom | { may: typeof Top; must: Set<never> },
>
is
- isTop(): this is SetRangeDomain<T, Value> & SetRangeDomain<
T,
{ may: typeof Top; must: Set<never> },
>Checks whether the current abstract value is the Top element of the complete lattice.
Returns this is SetRangeDomain<T, Value> & SetRangeDomain<
T,
{ may: typeof Top; must: Set<never> },
>
is
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 SetRangeDomain<T, Value> & SetRangeDomain<T, SetRangeValue<T>>
join
- join(
other:
| typeof Bottom
| SetRangeDomain<T, Value>
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
): thisJoins the current abstract value with another abstract value by creating the least upper bound (LUB) in the lattice.
Parameters
- other:
| typeof Bottom
| SetRangeDomain<T, Value>
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>
Returns this
- other:
join
Joins the current abstract value with multiple other abstract values.
Parameters
- values: readonly SetRangeDomain<T, Value>[]
Returns this
Protectedjoin
- joinValue(
this: SetRangeDomain<T, Value> & SetRangeDomain<T, SetRangeValue<T>>,
other: SetRangeDomain<T, SetRangeValue<T>>,
): thisParameters
- this: SetRangeDomain<T, Value> & SetRangeDomain<T, SetRangeValue<T>>
- other: SetRangeDomain<T, SetRangeValue<T>>
Returns this
Protectedjsonify
Parameters
- this: SetRangeDomain<T, SetRangeValue<T>>
Returns unknown
leq
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
Protectedleq
- leqValue(
this: SetRangeDomain<T, SetRangeValue<T>>,
other: SetRangeDomain<T, SetRangeValue<T>>,
): booleanParameters
- this: SetRangeDomain<T, SetRangeValue<T>>
- other: SetRangeDomain<T, SetRangeValue<T>>
Returns boolean
lower
The lower bound of the set range representing all values that must be present (equals the must set).
Parameters
- this: SetRangeDomain<T, SetRangeValue<T>>
Returns ReadonlySet<T>
The lower bound of the set range representing all values that must be present (equals the must set).
Parameters
- this: SetRangeDomain<T, SetRangeLift<T>>
Returns typeof Bottom | ReadonlySet<T>
meet
- meet(
other:
| typeof Bottom
| SetRangeDomain<T, Value>
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
): thisMeets the current abstract value with another abstract value by creating the greatest lower bound (GLB) in the lattice.
Parameters
- other:
| typeof Bottom
| SetRangeDomain<T, Value>
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>
Returns this
- other:
meet
Meets the current abstract value with multiple other abstract values.
Parameters
- values: readonly SetRangeDomain<T, Value>[]
Returns this
Protectedmeet
- meetValue(
this: SetRangeDomain<T, Value> & SetRangeDomain<T, SetRangeValue<T>>,
other: SetRangeDomain<T, SetRangeValue<T>>,
): thisParameters
- this: SetRangeDomain<T, Value> & SetRangeDomain<T, SetRangeValue<T>>
- other: SetRangeDomain<T, SetRangeValue<T>>
Returns this
merge
- merge(
other: this,
merge: (
first: SetRangeValue,
second: SetRangeValue,
) =>
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
bottomDefault: (
other:
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
) =>
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
topDefault: (
other:
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
) =>
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
): thisParameters
- other: this
- merge: (
first: SetRangeValue,
second: SetRangeValue,
) =>
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T> - bottomDefault: (
other:
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
) =>
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T> - topDefault: (
other:
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
) =>
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>
Returns this
- merge(
other: this,
merge: (
first: { may: typeof Top; must: Set<never> } | SetRangeValue<T>,
second: { may: typeof Top; must: Set<never> } | SetRangeValue<T>,
) =>
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
bottomDefault: (
other:
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
) =>
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
): thisParameters
- other: this
- merge: (
first: { may: typeof Top; must: Set<never> } | SetRangeValue<T>,
second: { may: typeof Top; must: Set<never> } | SetRangeValue<T>,
) =>
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T> - bottomDefault: (
other:
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
) =>
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>
Returns this
- merge(
other: this,
merge: (
first:
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
second:
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
) =>
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
): thisParameters
- other: this
- merge: (
first:
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
second:
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
) =>
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>
Returns this
narrow
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
Protectednarrow
- narrowValue(
this: SetRangeDomain<T, Value> & SetRangeDomain<T, SetRangeValue<T>>,
other: SetRangeDomain<T, SetRangeValue<T>>,
): thisParameters
- this: SetRangeDomain<T, Value> & SetRangeDomain<T, SetRangeValue<T>>
- other: SetRangeDomain<T, SetRangeValue<T>>
Returns this
satisfies
Checks whether the current abstract value satisfies a concrete value (i.e. includes a concrete value).
Parameters
- set: T[] | ReadonlySet<T>
- comparator: SetComparator = SetComparator.Equal
Returns Ternary
See
Ternary for the returned satisfiability result
Protectedstringify
Parameters
- this: SetRangeDomain<T, SetRangeValue<T>>
Returns string
subtract
Subtracts another set abstract value from this set abstract value creating the set difference.
Parameters
- other: SetRangeDomain<T, Value> | SetRangeLift<T> | ArrayRangeValue<T>
Returns this
to
Converts the lattice into a JSON serializable value.
Returns unknown
top
Gets the Top element (greatest element) of the complete lattice (should additionally be provided as static function).
Returns SetRangeDomain<T, Value> & SetRangeDomain<
T,
{ may: typeof Top; must: Set<never> },
>
to
Converts the lattice into a human-readable string.
Returns string
transform
- transform(
transform: (
value: SetRangeValue,
) =>
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
bottomDefault:
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
topDefault:
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
): thisParameters
- transform: (
value: SetRangeValue,
) =>
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T> - bottomDefault: typeof Bottom | { may: typeof Top; must: Set<never> } | SetRangeValue<T>
- topDefault: typeof Bottom | { may: typeof Top; must: Set<never> } | SetRangeValue<T>
Returns this
- transform: (
- transform(
transform: (
value: { may: typeof Top; must: Set<never> } | SetRangeValue<T>,
) =>
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
bottomDefault:
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
): thisParameters
- transform: (
value: { may: typeof Top; must: Set<never> } | SetRangeValue<T>,
) =>
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T> - bottomDefault: typeof Bottom | { may: typeof Top; must: Set<never> } | SetRangeValue<T>
Returns this
- transform: (
- transform(
transform: (
value:
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
) =>
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
): thisParameters
- transform: (
value:
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>,
) =>
| typeof Bottom
| { may: typeof Top; must: Set<never> }
| SetRangeValue<T>
Returns this
- transform: (
union
Creates the union between this set abstract value and another set abstract value.
Parameters
- other: SetRangeDomain<T, Value> | SetRangeLift<T> | ArrayRangeValue<T>
Returns this
upper
The upper bound of the set range representing all values that can possibly be present (union of must set and may set).
Parameters
- this: SetRangeDomain<T, SetRangeFinite<T>>
Returns ReadonlySet<T>
The upper bound of the set range representing all values that can possibly be present (union of must set and may set).
Parameters
- this: SetRangeDomain<T, SetRangeValue<T>>
Returns typeof Top | ReadonlySet<T>
The upper bound of the set range representing all values that can possibly be present (union of must set and may set).
Parameters
- this: SetRangeDomain<T, SetRangeLift<T>>
Returns typeof Bottom | typeof Top | ReadonlySet<T>
widen
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
widen
Extends the must set of the current abstract value down to the empty set.
Returns this
widen
Extends the may set of the current abstract value up to Top.
Returns this
Protectedwiden
- widenValue(
this: SetRangeDomain<T, Value> & SetRangeDomain<T, SetRangeValue<T>>,
other: SetRangeDomain<T, SetRangeValue<T>>,
): thisParameters
- this: SetRangeDomain<T, Value> & SetRangeDomain<T, SetRangeValue<T>>
- other: SetRangeDomain<T, SetRangeValue<T>>
Returns this
The set range abstract domain as range of possible value sets with a set of values that must be present and a set of values that may be present (similar to an interval-like structure with a lower bound and a difference to the upper bound). The Bottom element is defined as Bottom symbol and the Top element is defined as the range
[∅, Top]where the must set is the empty set and the may set is Top.