diff --git a/src/abstract-interpretation/data-frame/dataframe-domain.ts b/src/abstract-interpretation/data-frame/dataframe-domain.ts index 5af2670c864..366d0ea74ae 100644 --- a/src/abstract-interpretation/data-frame/dataframe-domain.ts +++ b/src/abstract-interpretation/data-frame/dataframe-domain.ts @@ -13,9 +13,8 @@ export type AbstractDataFrameShape = { * The data frame abstract domain as product domain of a column names domain, column count domain, and row count domain. */ export class DataFrameDomain extends ProductDomain { - public create(value: AbstractDataFrameShape): this; - public create(value: AbstractDataFrameShape): DataFrameDomain { - return new DataFrameDomain(value); + public create(value: AbstractDataFrameShape): this { + return new DataFrameDomain(value) as this; } /** @@ -57,21 +56,29 @@ export class DataFrameDomain extends ProductDomain { protected reduce(value: AbstractDataFrameShape): AbstractDataFrameShape { if(value.colnames.isValue() && value.cols.isValue()) { - if(value.colnames.value.min.size >= value.cols.value[1]) { + const minColNames = value.colnames.must.size; + const maxColNames = value.colnames.isFinite() ? value.colnames.must.size + value.colnames.may.size : Infinity; + + if(minColNames >= value.cols.upper) { + value = { + ...value, + colnames: value.colnames.create({ must: value.colnames.must, may: new Set() }) + }; + } else if(value.colnames.isFinite() && value.colnames.may.size > 0 && maxColNames <= value.cols.lower) { value = { ...value, - colnames: value.colnames.meet({ min: new Set(), range: value.colnames.value.min }) + colnames: value.colnames.create({ must: value.colnames.upper(), may: new Set() }) }; } } if(value.colnames.isValue() && value.cols.isValue()) { - const minColNames = value.colnames.value.min.size; - const maxColNames = value.colnames.isFinite() ? value.colnames.value.min.size + value.colnames.value.range.size : Infinity; + const minColNames = value.colnames.must.size; + const maxColNames = value.colnames.isFinite() ? value.colnames.must.size + value.colnames.may.size : Infinity; - if(minColNames > value.cols.value[0] || maxColNames < value.cols.value[1]) { + if((minColNames > value.cols.lower || maxColNames < value.cols.upper) && Math.max(minColNames, value.cols.lower) <= Math.min(maxColNames, value.cols.upper)) { value = { ...value, - cols: value.cols.meet([minColNames, maxColNames]) + cols: value.cols.create([Math.max(minColNames, value.cols.lower), Math.min(maxColNames, value.cols.upper)]) }; } } diff --git a/src/abstract-interpretation/data-frame/semantics.ts b/src/abstract-interpretation/data-frame/semantics.ts index 64435a9c151..9bd15ccedaf 100644 --- a/src/abstract-interpretation/data-frame/semantics.ts +++ b/src/abstract-interpretation/data-frame/semantics.ts @@ -1,7 +1,7 @@ import { assertUnreachable, isNotUndefined } from '../../util/assert'; import { Bottom, Top } from '../domains/lattice'; import { PosIntervalDomain, PosIntervalTop } from '../domains/positive-interval-domain'; -import type { ArrayRangeValue } from '../domains/set-range-domain'; +import type { SetRangeValue } from '../domains/set-range-domain'; import type { DataFrameDomain } from './dataframe-domain'; /** @@ -212,7 +212,7 @@ function applySetColNamesSemantics( rows: value.rows }); } - const allColNames = colnames?.every(isNotUndefined) && value.cols.value !== Bottom && colnames.length >= value.cols.value[1]; + const allColNames = colnames?.every(isNotUndefined) && value.cols.isValue() && colnames.length >= value.cols.upper; return value.create({ colnames: allColNames ? value.colnames.create(setRange(colnames)) : value.colnames.create(setRange(colnames)).widenUp(), @@ -236,7 +236,7 @@ function applyAddRowsSemantics( value: DataFrameDomain, { rows }: { rows: number | undefined } ): DataFrameDomain { - if(value.cols.value !== Bottom && value.cols.value[0] === 0) { + if(value.cols.isValue() && value.cols.lower === 0) { return value.create({ colnames: value.colnames.top(), cols: rows !== undefined ? value.cols.add([1, 1]) : value.cols.top(), @@ -303,7 +303,7 @@ function applyConcatRowsSemantics( value: DataFrameDomain, { other }: { other: DataFrameDomain } ): DataFrameDomain { - if(value.cols.value !== Bottom && value.cols.value[0] === 0) { + if(value.cols.value !== Bottom && value.cols.lower === 0) { return value.create({ colnames: value.colnames.join(other.colnames), cols: value.cols.join(other.cols), @@ -417,19 +417,17 @@ function applyJoinSemantics( ): DataFrameDomain { // Merge two intervals by creating the maximum of the lower bounds and adding the upper bounds const mergeInterval = (interval1: PosIntervalDomain, interval2: PosIntervalDomain): PosIntervalDomain => { - if(interval1.value === Bottom || interval2.value === Bottom) { - return interval1.bottom(); - } else { - return new PosIntervalDomain([Math.max(interval1.value[0], interval2.value[0]), interval1.value[1] + interval2.value[1]]); + if(interval1.isValue() && interval2.isValue()) { + return new PosIntervalDomain([Math.max(interval1.lower, interval2.lower), interval1.upper + interval2.upper]); } + return interval1.bottom(); }; // Creating the Cartesian product of two intervals by keeping the lower bound and multiplying the upper bounds const productInterval = (lower: PosIntervalDomain, interval1: PosIntervalDomain, interval2: PosIntervalDomain): PosIntervalDomain => { - if(lower.value === Bottom || interval1.value === Bottom || interval2.value === Bottom) { - return lower.bottom(); - } else { - return new PosIntervalDomain([lower.value[0], interval1.value[1] * interval2.value[1]]); + if(lower.isValue() && interval1.isValue() && interval2.isValue()) { + return new PosIntervalDomain([lower.lower, interval1.upper * interval2.upper]); } + return lower.bottom(); }; let duplicateCols: string[] | undefined; // columns that may be renamed due to occurring in both data frames let productRows: boolean; // whether the resulting rows may be a Cartesian product of the rows of the data frames @@ -461,10 +459,10 @@ function applyJoinSemantics( rows = value.rows.max(other.rows).widenDown(); break; case 'left': - rows = value.rows.max(other.rows.isValue() ? [0, other.rows.value[1]] : Bottom); + rows = value.rows.max(other.rows.isValue() ? [0, other.rows.upper] : Bottom); break; case 'right': - rows = other.rows.max(value.rows.isValue() ? [0, value.rows.value[1]] : Bottom); + rows = other.rows.max(value.rows.isValue() ? [0, value.rows.upper] : Bottom); break; case 'full': rows = mergeInterval(value.rows, other.rows); @@ -495,8 +493,8 @@ function applyUnknownSemantics( return value.top(); } -function setRange(colnames: (string | undefined)[] | undefined): ArrayRangeValue { +function setRange(colnames: (string | undefined)[] | undefined): SetRangeValue { const names = colnames?.filter(isNotUndefined) ?? []; - return { min: names, range: names.length === colnames?.length ? [] : Top }; + return { must: new Set(names), may: names.length === colnames?.length ? new Set() : Top }; } diff --git a/src/abstract-interpretation/domains/abstract-domain.ts b/src/abstract-interpretation/domains/abstract-domain.ts index 4f4327f486f..f24be0f622a 100644 --- a/src/abstract-interpretation/domains/abstract-domain.ts +++ b/src/abstract-interpretation/domains/abstract-domain.ts @@ -1,3 +1,4 @@ + import { guard } from '../../util/assert'; import { type Lattice, Bottom, BottomSymbol, Top, TopSymbol } from './lattice'; @@ -7,37 +8,69 @@ import { type Lattice, Bottom, BottomSymbol, Top, TopSymbol } from './lattice'; export const DEFAULT_INFERENCE_LIMIT = 50; /** - * An abstract domain as complete lattice with a widening operator, narrowing operator, concretization function, and abstraction function. + * 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 {@link create}. - * @template Concrete - Type of an concrete element of the concrete domain for the abstract domain - * @template Abstract - Type of an abstract element of the abstract domain representing possible elements (excludes `Top` and `Bot`) - * @template Top - Type of the Top element of the abstract domain representing all possible elements - * @template Bot - Type of the Bottom element of the abstract domain representing no possible elements - * @template Value - Type of the abstract elements of the abstract domain (defaults to `Abstract` or `Top` or `Bot`) + * @template Value - Type of an abstract element of the abstract domain representing possible elements (excludes `Top` and `Bot`) + * @template Top - Type of the Top element of the abstract domain representing all possible elements + * @template Bot - Type of the Bottom element of the abstract domain representing no possible elements + * @template Lift - Type of the current abstract value in the abstract domain (defaults to `Value` or `Top` or `Bot`) */ -export abstract class AbstractDomain -implements Lattice { - protected readonly _value: Value; +export abstract class AbstractDomain +implements Lattice { + protected readonly _value: Lift; - constructor(value: Value) { + constructor(value: Lift) { this._value = value; } - public get value(): Value { + public get value(): Lift { return this._value; } - public abstract create(value: Abstract | Top | Bot): this; + public abstract create(value: Value | Top | Bot): this; + + public abstract top(): this & AbstractDomain; + + public abstract bottom(): this & AbstractDomain; + + public equals(other: this): boolean { + if(this.value === other.value || (this.isTop() && other.isTop()) || (this.isBottom() && other.isBottom())) { + return true; + } else if(!this.isValue() || !other.isValue()) { + return false; + } + return this.equalsValue(other); + } + + protected abstract equalsValue(this: AbstractDomain, other: AbstractDomain): boolean; - public abstract top(): this & AbstractDomain; + public leq(other: this): boolean { + if(this.isBottom() || other.isTop() || this.equals(other)) { + return true; + } else if(!this.isValue() || !other.isValue()) { + return false; + } + return this.leqValue(other); + } - public abstract bottom(): this & AbstractDomain; + protected abstract leqValue(this: AbstractDomain, other: AbstractDomain): boolean; - public abstract equals(other: this): boolean; + public join(other: this | Value | Top | Bot): this { + other = other instanceof AbstractDomain ? other : this.create(other); - public abstract leq(other: this): boolean; + if(this.isTop() || other.isTop()) { + return this.top(); + } else if(this.isBottom()) { + return this.create(other.value); + } else if(other.isBottom()) { + return this.create(this.value); + } else if(!this.isValue() || !other.isValue()) { + return this.bottom(); + } + return this.joinValue(other); + } - public abstract join(other: this): this; + protected abstract joinValue(this: AbstractDomain, other: AbstractDomain): this; /** * Joins the current abstract value with multiple other abstract values. @@ -51,7 +84,22 @@ implements Lattice { return result; } - public abstract meet(other: this): this; + public meet(other: this | Value | Top | Bot): this { + other = other instanceof AbstractDomain ? other : this.create(other); + + if(this.isTop()) { + return this.create(other.value); + } else if(other.isTop()) { + return this.create(this.value); + } else if(this.isBottom() || other.isBottom()) { + return this.bottom(); + } else if(!this.isValue() || !other.isValue()) { + return this.top(); + } + return this.meetValue(other); + } + + protected abstract meetValue(this: AbstractDomain, other: AbstractDomain): this; /** * Meets the current abstract value with multiple other abstract values. @@ -68,33 +116,99 @@ implements Lattice { /** * Widens the current abstract value with another abstract value as a sound over-approximation of the join (least upper bound) for fixpoint iteration acceleration. */ - public abstract widen(other: this): this; + public widen(other: this): this { + if(this.isTop() || other.isTop()) { + return this.top(); + } else if(this.isBottom()) { + return this.create(other.value); + } else if(other.isBottom()) { + return this.create(this.value); + } else if(!this.isValue() || !other.isValue()) { + return this.bottom(); + } + return this.widenValue?.(other) ?? (other.leq(this) ? this.create(this.value) : this.top()); + } + + protected widenValue?(this: AbstractDomain, other: AbstractDomain): 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. */ - public abstract narrow(other: this): this; + public narrow(other: this): this { + if(this.isTop()) { + return this.create(other.value); + } else if(other.isTop()) { + return this.create(this.value); + } else if(this.isBottom() || other.isBottom()) { + return this.bottom(); + } else if(!this.isValue() || !other.isValue()) { + return this.top(); + } + return this.narrowValue?.(other) ?? (this.isTop() ? this.create(other.value) : this.create(this.value)); + } - /** - * 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. - */ - public abstract concretize(limit: number): ReadonlySet | typeof Top; + protected narrowValue?(this: AbstractDomain, other: AbstractDomain): 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). - */ - public abstract abstract(concrete: ReadonlySet | typeof Top): this; + public transform(transform: (value: Value) => Value | Top | Bot, bottomDefault: Value | Top | Bot, topDefault: Value | Top | Bot): this; + public transform(transform: (value: Value | Top) => Value | Top | Bot, bottomDefault: Value | Top | Bot): this; + public transform(transform: (value: Value | Top | Bot) => Value | Top | Bot): this; + public transform(transform: (value: Value) => Value | Top | Bot, bottomDefault?: Value | Top | Bot, topDefault?: Value | Top | Bot): this { + if(bottomDefault !== undefined && this.isBottom()) { + return this.create(bottomDefault); + } else if(topDefault !== undefined && this.isTop()) { + return this.create(topDefault); + } + return this.create(transform(this.value as Value)); + } + + public 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; + public merge(other: this, merge: (first: Value | Top, second: Value | Top) => Value | Top | Bot, bottomDefault: (other: Value | Top | Bot) => Value | Top | Bot): this; + public merge(other: this, merge: (first: Value | Top | Bot, second: Value | Top | Bot) => Value | Top | Bot): this; + public 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 { + if(bottomDefault !== undefined) { + if(this.isBottom() ) { + return this.create(bottomDefault(other.value)); + } else if(other.isBottom()) { + return this.create(bottomDefault(this.value)); + } + } + if(topDefault !== undefined) { + if(this.isTop()) { + return this.create(topDefault(other.value)); + } else if(other.isTop()) { + return this.create(topDefault(this.value)); + } + } + return this.create(merge(this.value as Value, other.value as Value)); + } + + public toJson(): unknown { + if(this.value === Top) { + return Top.description; + } else if(this.value === Bottom) { + return Bottom.description; + } + return (this as this & AbstractDomain>).jsonify(); + } + + protected abstract jsonify(this: AbstractDomain>): unknown; - public abstract toJson(): unknown; + public toString(): string { + if(this.value === Top) { + return TopSymbol; + } else if(this.value === Bottom) { + return BottomSymbol; + } + return (this as this & AbstractDomain>).stringify(); + } - public abstract toString(): string; + protected abstract stringify(this: AbstractDomain>): string; - public abstract isTop(): this is AbstractDomain; + public abstract isTop(): this is this & AbstractDomain; - public abstract isBottom(): this is AbstractDomain; + public abstract isBottom(): this is this & AbstractDomain; - public abstract isValue(): this is AbstractDomain; + public abstract isValue(): this is this & AbstractDomain; /** * Joins an array of abstract values by joining the first abstract value with the other values in the array. @@ -139,39 +253,32 @@ implements Lattice { /** * A type representing any abstract domain without additional information. */ -export type AnyAbstractDomain = AbstractDomain; +export type AnyAbstractDomain = AbstractDomain; /** * The type of the abstract values of an abstract domain (including the Top and Bottom element). * @template Domain - The abstract domain to get the abstract value type for */ export type AbstractValue = - Domain extends AbstractDomain ? Value | Top | Bot : never; - -/** - * The type of the concrete domain of an abstract domain. - * @template Domain - The abstract domain to get the concrete domain type for - */ -export type ConcreteDomain = - Domain extends AbstractDomain ? Concrete : never; + Domain extends AbstractDomain ? Value | Top | Bot : never; /** * The type of an abstract domain holding an abstract value of the domain. * @template Domain - The abstract domain abstract domain value type for */ export type AbstractDomainValue = - Domain extends AbstractDomain ? Domain & AbstractDomain : never; + Domain extends AbstractDomain ? Domain & AbstractDomain : never; /** * The type an abstract domain holding the Top element (greatest element) of the domain. * @template Domain - The abstract domain to get the abstract domain top for */ export type AbstractDomainTop = - Domain extends AbstractDomain ? Domain & AbstractDomain : never; + Domain extends AbstractDomain ? Domain & AbstractDomain : never; /** * The type an abstract domain holding the Bottom element (least element) of the domain. * @template Domain - The abstract domain to get the abstract domain bottom for */ export type AbstractDomainBottom = - Domain extends AbstractDomain ? Domain & AbstractDomain : never; + Domain extends AbstractDomain ? Domain & AbstractDomain : never; diff --git a/src/abstract-interpretation/domains/bounded-set-domain.ts b/src/abstract-interpretation/domains/bounded-set-domain.ts index 00b7a149b09..ae408a1263c 100644 --- a/src/abstract-interpretation/domains/bounded-set-domain.ts +++ b/src/abstract-interpretation/domains/bounded-set-domain.ts @@ -1,19 +1,18 @@ import { setEquals } from '../../util/collections/set'; import { Ternary } from '../../util/logic'; import { AbstractDomain, DEFAULT_INFERENCE_LIMIT } from './abstract-domain'; -import { Top, TopSymbol } from './lattice'; -import type { SatisfiableDomain } from './satisfiable-domain'; -/* eslint-disable @typescript-eslint/unified-signatures */ +import { Top } from './lattice'; +import type { ValueDomain } from './value-abstract-domain'; /** The Bottom element of the bounded set domain as empty set */ -export const BoundedSetBottom: ReadonlySet = new Set(); +export const SetBottom: ReadonlySet = new Set(); /** The type of the actual values of the bounded set domain as set */ type BoundedSetValue = ReadonlySet; /** The type of the Top element of the bounded set domain as {@link Top} symbol */ type BoundedSetTop = typeof Top; /** The type of the Bottom element of the bounded set domain as empty set */ -type BoundedSetBottom = typeof BoundedSetBottom; +type BoundedSetBottom = typeof SetBottom; /** The type of the abstract values of the bounded set domain that are Top, Bottom, or actual values */ type BoundedSetLift = BoundedSetValue | BoundedSetTop | BoundedSetBottom; @@ -24,11 +23,11 @@ type BoundedSetLift = BoundedSetValue | BoundedSetTop | BoundedSetBottom; * @template Value - Type of the constraint in the abstract domain (Top, Bottom, or an actual value) */ export class BoundedSetDomain = BoundedSetLift> - extends AbstractDomain, BoundedSetTop, BoundedSetBottom, Value> - implements SatisfiableDomain { + extends AbstractDomain, BoundedSetTop, BoundedSetBottom, Value> + implements ValueDomain { - public readonly limit: number; - private readonly setType: typeof Set; + public readonly limit: number; + protected readonly setType: typeof Set; /** * @param limit - A limit for the maximum number of elements to store in the set @@ -48,97 +47,48 @@ export class BoundedSetDomain = BoundedSetLif this.setType = setType; } - public create(value: BoundedSetLift | T[]): this; - public create(value: BoundedSetLift | T[]): BoundedSetDomain { - return new BoundedSetDomain(value, this.limit, this.setType); + public create(value: BoundedSetLift | T[]): this { + return new BoundedSetDomain(value, this.limit, this.setType) as this; } - public static top(limit?: number, setType?: typeof Set): BoundedSetDomain { - return new BoundedSetDomain(Top, limit, setType); - } - - public static bottom(limit?: number, setType?: typeof Set): BoundedSetDomain { - return new BoundedSetDomain(BoundedSetBottom, limit, setType); + public from(...values: T[]): this { + return this.create(values); } - public static abstract(concrete: ReadonlySet | typeof Top, limit?: number, setType?: typeof Set): BoundedSetDomain { - return new BoundedSetDomain(concrete, limit, setType); - } - - public top(): this & BoundedSetDomain; - public top(): BoundedSetDomain { - return BoundedSetDomain.top(this.limit, this.setType); - } - - public bottom(): this & BoundedSetDomain; - public bottom(): BoundedSetDomain { - return BoundedSetDomain.bottom(this.limit, this.setType); - } - - public equals(other: this): boolean { - return this.value === other.value || (this.isValue() && other.isValue() && setEquals(this.value, other.value)); + public static top(limit?: number, setType?: typeof Set): BoundedSetDomain { + return new this(Top, limit, setType); } - public leq(other: this): boolean { - return other.value === Top || (this.isValue() && this.value.isSubsetOf(other.value)); + public static bottom(limit?: number, setType?: typeof Set): BoundedSetDomain { + return new this(SetBottom, limit, setType); } - public join(other: BoundedSetLift | T[]): this; - public join(other: this): this; - public join(other: this | BoundedSetLift | T[]): this { - const otherValue = other instanceof BoundedSetDomain ? other.value : Array.isArray(other) ? new this.setType(other) : other; - - if(this.value === Top || otherValue === Top) { - return this.top(); - } else { - return this.create(this.value.union(otherValue)); - } + public static from(values: T | T[], limit?: number, setType?: typeof Set): BoundedSetDomain { + return new this(Array.isArray(values) ? values : [values], limit, setType); } - public meet(other: BoundedSetLift | T[]): this; - public meet(other: this): this; - public meet(other: this | BoundedSetLift | T[]): this { - const otherValue = other instanceof BoundedSetDomain ? other.value : Array.isArray(other) ? new this.setType(other) : other; - - if(this.value === Top) { - return this.create(otherValue); - } else if(otherValue === Top) { - return this.create(this.value); - } else { - return this.create(this.value.intersection(otherValue)); - } + public top(): this & BoundedSetDomain { + return this.create(Top) as this & BoundedSetDomain; } - /** - * Subtracts another abstract value from the current abstract value by removing all elements of the other abstract value from the current abstract value. - */ - public subtract(other: this | BoundedSetLift | T[]): this { - const otherValue = other instanceof BoundedSetDomain ? other.value : Array.isArray(other) ? new this.setType(other) : other; - - if(this.value === Top) { - return this.top(); - } else if(otherValue === Top) { - return this.create(this.value); - } else { - return this.create(this.value.difference(otherValue)); - } + public bottom(): this & BoundedSetDomain { + return this.create(SetBottom) as this & BoundedSetDomain; } - public widen(other: this): this { - return other.leq(this) ? this.create(this.value) : this.top(); + protected equalsValue(this: BoundedSetDomain>, other: BoundedSetDomain>): boolean { + return setEquals(this.value, other.value); } - public narrow(other: this): this { - return this.isTop() ? this.create(other.value) : this.create(this.value); + protected leqValue(this: BoundedSetDomain>, other: BoundedSetDomain>): boolean { + return this.value.isSubsetOf(other.value); } - public concretize(limit: number): ReadonlySet | typeof Top { - return this.value === Top || this.value.size > limit ? Top : this.value; + protected joinValue(this: this & BoundedSetDomain>, other: BoundedSetDomain>): this { + return this.create(this.value.union(other.value)); } - public abstract(concrete: ReadonlySet | typeof Top): this; - public abstract(concrete: ReadonlySet | typeof Top): BoundedSetDomain { - return BoundedSetDomain.abstract(concrete, this.limit, this.setType); + protected meetValue(this: this & BoundedSetDomain>, other: BoundedSetDomain>): this { + return this.create(this.value.intersection(other.value)); } public satisfies(value: T): Ternary { @@ -150,31 +100,23 @@ export class BoundedSetDomain = BoundedSetLif return Ternary.Never; } - public toJson(): unknown { - if(this.value === Top) { - return this.value.description; - } + protected jsonify(this: BoundedSetDomain>): unknown { return this.value.values().toArray(); } - public toString(): string { - if(this.value === Top) { - return TopSymbol; - } - const string = this.value.values().map(AbstractDomain.toString).toArray().join(', '); - - return `{${string}}`; + protected stringify(this: BoundedSetDomain>): string { + return `{${this.value.values().map(AbstractDomain.toString).toArray().join(', ')}}`; } - public isTop(): this is BoundedSetDomain { + public isTop(): this is this & BoundedSetDomain { return this.value === Top; } - public isBottom(): this is BoundedSetDomain { + public isBottom(): this is this & BoundedSetDomain { return this.value !== Top && this.value.size === 0; } - public isValue(): this is BoundedSetDomain> { + public isValue(): this is this & BoundedSetDomain> { return this.value !== Top; } } diff --git a/src/abstract-interpretation/domains/interval-domain.ts b/src/abstract-interpretation/domains/interval-domain.ts index 26a337be255..a8aa17d9385 100644 --- a/src/abstract-interpretation/domains/interval-domain.ts +++ b/src/abstract-interpretation/domains/interval-domain.ts @@ -1,21 +1,22 @@ import { assertUnreachable } from '../../util/assert'; import { Ternary } from '../../util/logic'; import { AbstractDomain } from './abstract-domain'; -import { Bottom, BottomSymbol, Top } from './lattice'; -import { type SatisfiableDomain, NumericalComparator } from './satisfiable-domain'; -/* eslint-disable @typescript-eslint/unified-signatures */ +import { Bottom } from './lattice'; +import { type NumericDomain, NumericalComparator } from './value-abstract-domain'; /** The Top element of the interval domain as interval [-∞, +∞] */ export const IntervalTop: IntervalValue = [-Infinity, +Infinity]; /** The type of the actual values of the interval domain as tuple of the lower and upper bound */ -type IntervalValue = readonly [lower: number, upper: number]; +export type IntervalValue = readonly [lower: number, upper: number]; /** The type of the Top element of the interval domain as interval [-∞, +∞] */ -type IntervalTop = typeof IntervalTop; +export type IntervalTop = typeof IntervalTop; /** The type of the Bottom element of the interval domain as {@link Bottom} symbol */ -type IntervalBottom = typeof Bottom; +export type IntervalBottom = typeof Bottom; /** The type of the abstract values of the interval domain that are Top, Bottom, or actual values */ -type IntervalLift = IntervalValue | IntervalBottom; +export type IntervalLift = IntervalValue | IntervalBottom; + +type IntervalBound = Value extends IntervalValue ? number : number | typeof Bottom; /** * The interval abstract domain as intervals with possibly infinite bounds representing possible numeric values. @@ -23,12 +24,12 @@ type IntervalLift = IntervalValue | IntervalBottom; * @template Value - Type of the constraint in the abstract domain (Top, Bottom, or an actual value) */ export class IntervalDomain - extends AbstractDomain - implements SatisfiableDomain { + extends AbstractDomain + implements NumericDomain { constructor(value: Value) { if(Array.isArray(value)) { - if(value.some(isNaN) || value[0] > value[1] || value[0] === +Infinity || value[1] === -Infinity) { + if(value.some(Number.isNaN) || value[0] > value[1] || value[0] === +Infinity || value[1] === -Infinity) { super(Bottom as Value); } else { super([value[0], value[1]] as const as Value); @@ -38,149 +39,114 @@ export class IntervalDomain } } - public create(value: IntervalLift): this; - public create(value: IntervalLift): IntervalDomain { - return new IntervalDomain(value); + public create(value: IntervalLift): this { + return new IntervalDomain(value) as this; } - public static top(): IntervalDomain { - return new IntervalDomain(IntervalTop); + public get lower(): IntervalBound { + return (this.isValue() ? this.value[0] : Bottom) as IntervalBound; } - public static bottom(): IntervalDomain { - return new IntervalDomain(Bottom); + public get upper(): IntervalBound { + return (this.isValue() ? this.value[1] : Bottom) as IntervalBound; } - public static abstract(concrete: ReadonlySet | typeof Top): IntervalDomain { - if(concrete === Top) { - return IntervalDomain.top(); - } else if(concrete.size === 0 || concrete.values().some(isNaN)) { - return IntervalDomain.bottom(); + public from(...values: number[]): this { + if(values.length === 0) { + return this.bottom(); } - return new IntervalDomain([Math.min(...concrete), Math.max(...concrete)]); + return this.create([Math.min(...values), Math.max(...values)]); } - public top(): this & IntervalDomain; - public top(): IntervalDomain { - return IntervalDomain.top(); + public static top(): IntervalDomain { + return new this(IntervalTop); } - public bottom(): this & IntervalDomain; - public bottom(): IntervalDomain { - return IntervalDomain.bottom(); + public static bottom(): IntervalDomain { + return new this(Bottom); } - public equals(other: this): boolean { - return this.value === other.value || (this.isValue() && other.isValue() && this.value[0] === other.value[0] && this.value[1] === other.value[1]); + public static from(...values: number[]): IntervalDomain { + if(values.length === 0) { + return this.bottom(); + } + return new this([Math.min(...values), Math.max(...values)]); } - public leq(other: this): boolean { - return this.value === Bottom || (other.isValue() && other.value[0] <= this.value[0] && this.value[1] <= other.value[1]); + public top(): this & IntervalDomain { + return this.create(IntervalTop) as this & IntervalDomain; } - public join(other: IntervalLift): this; - public join(other: this): this; - public join(other: this | IntervalLift): this { - const otherValue = other instanceof IntervalDomain ? other.value : other; + public bottom(): this & IntervalDomain { + return this.create(Bottom) as this & IntervalDomain; + } - if(this.value === Bottom) { - return this.create(otherValue); - } else if(otherValue === Bottom) { - return this.create(this.value); - } else { - return this.create([Math.min(this.value[0], otherValue[0]), Math.max(this.value[1], otherValue[1])]); - } + protected equalsValue(this: IntervalDomain, other: IntervalDomain): boolean { + return this.lower === other.lower && this.upper === other.upper; } - public meet(other: IntervalLift): this; - public meet(other: this): this; - public meet(other: this | IntervalLift): this { - const otherValue = other instanceof IntervalDomain ? other.value : other; + protected leqValue(this: IntervalDomain, other: IntervalDomain): boolean { + return other.lower <= this.lower && this.upper <= other.upper; + } - if(this.value === Bottom || otherValue === Bottom) { - return this.bottom(); - } else { - return this.create([Math.max(this.value[0], otherValue[0]), Math.min(this.value[1], otherValue[1])]); - } + protected joinValue(this: this & IntervalDomain, other: IntervalDomain): this { + return this.create([Math.min(this.lower, other.lower), Math.max(this.upper, other.upper)]); } - public widen(other: this): this { - if(this.value === Bottom) { - return this.create(other.value); - } else if(other.value === Bottom) { - return this.create(this.value); - } else { - return this.create([ - this.value[0] <= other.value[0] ? this.value[0] : -Infinity, - this.value[1] >= other.value[1] ? this.value[1] : +Infinity - ]); - } + protected meetValue(this: this & IntervalDomain, other: IntervalDomain): this { + return this.create([Math.max(this.lower, other.lower), Math.min(this.upper, other.upper)]); } - public narrow(other: this): this { - if(this.value === Bottom || other.value === Bottom) { - return this.bottom(); - } else if(Math.max(this.value[0], other.value[0]) > Math.min(this.value[1], other.value[1])) { - return this.bottom(); - } + protected widenValue(this: this & IntervalDomain, other: IntervalDomain): this { return this.create([ - this.value[0] === -Infinity ? other.value[0] : this.value[0], - this.value[1] === +Infinity ? other.value[1] : this.value[1] + this.lower <= other.lower ? this.lower : -Infinity, + this.upper >= other.upper ? this.upper : +Infinity ]); } - public concretize(limit: number): ReadonlySet | typeof Top { - if(this.value === Bottom) { - return new Set(); - } else if(!isFinite(this.value[0]) || !isFinite(this.value[1]) || this.value[1] - this.value[0] + 1 > limit) { - return Top; - } - const set = new Set(); - - for(let x = this.value[0]; x <= this.value[1]; x++) { - set.add(x); + protected narrowValue(this: this & IntervalDomain, other: IntervalDomain): this { + if(Math.max(this.lower, other.lower) > Math.min(this.upper, other.upper)) { + return this.bottom(); } - return set; - } - - public abstract(concrete: ReadonlySet | typeof Top): this; - public abstract(concrete: ReadonlySet | typeof Top): IntervalDomain { - return IntervalDomain.abstract(concrete); + return this.create([ + this.lower === -Infinity ? other.lower : this.lower, + this.upper === +Infinity ? other.upper : this.upper + ]); } public satisfies(value: number, comparator: NumericalComparator = NumericalComparator.Equal): Ternary { switch(comparator) { case NumericalComparator.Equal: { - if(this.isValue() && this.value[0] <= value && value <= this.value[1]) { - return this.value[0] === this.value[1] ? Ternary.Always : Ternary.Maybe; + if(this.isValue() && this.lower <= value && value <= this.upper) { + return this.lower === this.upper ? Ternary.Always : Ternary.Maybe; } else { return Ternary.Never; } } case NumericalComparator.Less: { - if(this.isValue() && value < this.value[1]) { - return value < this.value[0] ? Ternary.Always : Ternary.Maybe; + if(this.isValue() && value < this.upper) { + return value < this.lower ? Ternary.Always : Ternary.Maybe; } else { return Ternary.Never; } } case NumericalComparator.LessOrEqual: { - if(this.isValue() && value <= this.value[1]) { - return value <= this.value[0] ? Ternary.Always : Ternary.Maybe; + if(this.isValue() && value <= this.upper) { + return value <= this.lower ? Ternary.Always : Ternary.Maybe; } else { return Ternary.Never; } } case NumericalComparator.Greater: { - if(this.isValue() && this.value[0] <= value) { - return this.value[1] <= value ? Ternary.Always : Ternary.Maybe; + if(this.isValue() && this.lower <= value) { + return this.upper <= value ? Ternary.Always : Ternary.Maybe; } else { return Ternary.Never; } } case NumericalComparator.GreaterOrEqual: { - if(this.isValue() && this.value[0] < value) { - return this.value[1] < value ? Ternary.Always : Ternary.Maybe; + if(this.isValue() && this.lower < value) { + return this.upper < value ? Ternary.Always : Ternary.Maybe; } else { return Ternary.Never; } @@ -191,107 +157,117 @@ export class IntervalDomain } } - /** - * Adds another abstract value to the current abstract value by adding the two lower and upper bounds, respectively. - */ + public negate(): this { + if(this.isValue()) { + return this.create([-this.value[1], -this.value[0]]); + } + return this.bottom(); + } + public add(other: this | IntervalLift): this { - const otherValue = other instanceof IntervalDomain ? other.value : other; + const otherValue = other instanceof AbstractDomain ? other.value : other; - if(this.value === Bottom || otherValue === Bottom) { - return this.bottom(); - } else { - return this.create([this.value[0] + otherValue[0], this.value[1] + otherValue[1]]); + if(this.isValue() && otherValue !== Bottom) { + return this.create([this.lower + otherValue[0], this.upper + otherValue[1]]); } + return this.bottom(); } - /** - * Subtracts another abstract value from the current abstract value by subtracting the two lower and upper bounds from each other, respectively. - */ public subtract(other: this | IntervalLift): this { - const otherValue = other instanceof IntervalDomain ? other.value : other; + const otherValue = other instanceof AbstractDomain ? other.value : other; - if(this.value === Bottom || otherValue === Bottom) { - return this.bottom(); - } else { - return this.create([this.value[0] - otherValue[0], this.value[1] - otherValue[1]]); + if(this.isValue() && otherValue !== Bottom) { + return this.create([this.lower - otherValue[0], this.upper - otherValue[1]]); } + return this.bottom(); + } + + public multiply(other: this | IntervalLift): this { + const otherValue = other instanceof AbstractDomain ? other.value : other; + + if(this.isValue() && otherValue !== Bottom) { + const products = [ + this.value[0] * otherValue[0], + this.value[0] * otherValue[1], + this.value[1] * otherValue[0], + this.value[1] * otherValue[1] + ]; + return this.create([Math.min(...products), Math.max(...products)]); + } + return this.bottom(); + } + + public divide(other: this | IntervalLift): this { + const otherValue = other instanceof AbstractDomain ? other.value : other; + + if(this.isValue() && otherValue !== Bottom) { + if(otherValue[0] <= 0 && 0 <= otherValue[1]) { + return this.top(); + } + return this.multiply(this.create([1 / otherValue[1], 1 / otherValue[0]])); + } + return this.bottom(); } - /** - * Creates the minimum between the current abstract value and another abstract value by creating the minimum of the two lower and upper bounds, respectively. - */ public min(other: this | IntervalLift): this { - const otherValue = other instanceof IntervalDomain ? other.value : other; + const otherValue = other instanceof AbstractDomain ? other.value : other; - if(this.value === Bottom || otherValue === Bottom) { - return this.bottom(); - } else { - return this.create([Math.min(this.value[0], otherValue[0]), Math.min(this.value[1], otherValue[1])]); + if(this.isValue() && otherValue !== Bottom) { + return this.create([Math.min(this.lower, otherValue[0]), Math.min(this.upper, otherValue[1])]); } + return this.bottom(); } - /** - * Creates the maximum between the current abstract value and another abstract value by creating the maximum of the two lower and upper bounds, respectively. - */ public max(other: this | IntervalLift): this { - const otherValue = other instanceof IntervalDomain ? other.value : other; + const otherValue = other instanceof AbstractDomain ? other.value : other; - if(this.value === Bottom || otherValue === Bottom) { - return this.bottom(); - } else { - return this.create([Math.max(this.value[0], otherValue[0]), Math.max(this.value[1], otherValue[1])]); + if(this.isValue() && otherValue !== Bottom) { + return this.create([Math.max(this.lower, otherValue[0]), Math.max(this.upper, otherValue[1])]); } + return this.bottom(); } /** * Extends the lower bound of the current abstract value down to -∞. */ public widenDown(): this { - if(this.value === Bottom) { - return this.bottom(); - } else { - return this.create([-Infinity, this.value[1]]); + if(this.isValue()) { + return this.create([-Infinity, this.upper]); } + return this.bottom(); } /** * Extends the upper bound of the current abstract value up to +∞. */ public widenUp(): this { - if(this.value === Bottom) { - return this.bottom(); - } else { - return this.create([this.value[0], +Infinity]); + if(this.isValue()) { + return this.create([this.lower, +Infinity]); } + return this.bottom(); } - public toJson(): unknown { - if(this.value === Bottom) { - return this.value.description; - } + protected jsonify(): unknown { return this.value; } - public toString(): string { - if(this.value === Bottom) { - return BottomSymbol; - } - return `[${isFinite(this.value[0]) ? this.value[0] : '-∞'}, ${isFinite(this.value[1]) ? this.value[1] : '+∞'}]`; + protected stringify(this: IntervalDomain): string { + return `[${Number.isFinite(this.lower) ? this.lower : '-∞'}, ${Number.isFinite(this.upper) ? this.upper : '+∞'}]`; } - public isTop(): this is IntervalDomain { - return this.value !== Bottom && this.value[0] === -Infinity && this.value[1] === +Infinity; + public isTop(): this is this & IntervalDomain { + return this.value !== Bottom && this.lower === -Infinity && this.upper === +Infinity; } - public isBottom(): this is IntervalDomain { + public isBottom(): this is this & IntervalDomain { return this.value === Bottom; } - public isValue(): this is IntervalDomain { + public isValue(): this is this & IntervalDomain { return this.value !== Bottom; } - public isFinite(): this is IntervalDomain { - return this.isValue() && Number.isFinite(this.value[0]) && Number.isFinite(this.value[1]); + public isFinite(): this is this & IntervalDomain { + return this.isValue() && Number.isFinite(this.lower) && Number.isFinite(this.upper); } } diff --git a/src/abstract-interpretation/domains/lattice.ts b/src/abstract-interpretation/domains/lattice.ts index 973c62df989..96402679caf 100644 --- a/src/abstract-interpretation/domains/lattice.ts +++ b/src/abstract-interpretation/domains/lattice.ts @@ -15,7 +15,7 @@ export const BottomSymbol = '⊥'; * @template Value - Type of a lattice element representing a value (may exclude `Top` and `Bot`) * @template Top - Type of the Top element (greatest element) of the complete lattice * @template Bot - Type of the Bottom element (least element) of the complete lattice - * @template Lift - Type of the lattice elements (defaults to `Value` or `Top` or `Bot`) + * @template Lift - Type of the current element in the lattice (defaults to `Value | Top | Bot`) */ export interface Lattice { /** @@ -51,12 +51,12 @@ export interface Lattice>): this; - public create(value: StateDomainLift>): StateAbstractDomain> { - return new MultiValueStateDomain(value, this.domain.domain, this.domain.reductions); + public create(value: StateDomainLift>): this { + return new MultiValueStateDomain(value, this.domain.domain, this.domain.reductions) as this; } public getValue(node: NodeId, property: Key): Product[Key] | undefined { if(this.value === Bottom) { return this.domain.value[property]?.bottom() as Product[Key]; } - return this.value.get(node)?.value[property]; + return this.get(node)?.value[property]; } public hasValue(node: NodeId, property: keyof Product): boolean { - return this.value !== Bottom && this.value.get(node)?.value[property] !== undefined; + return this.value !== Bottom && this.get(node)?.value[property] !== undefined; } public setValue(node: NodeId, property: Key, value: Product[Key]): void { if(this.value !== Bottom) { const oldValue = this.get(node); const newValue = { ...oldValue?.value ?? {}, [property]: value }; - (this._value as Map>).set(node, new MultiValueDomain(newValue as Product, this.domain.domain, this.domain.reductions)); + this.set(node, new MultiValueDomain(newValue as Product, this.domain.domain, this.domain.reductions)); } } } @@ -61,9 +60,8 @@ export class MultiValueDomain this.reductions = reductions; } - public create(value: Product): this; - public create(value: Product): MultiValueDomain { - return new MultiValueDomain(value, this.domain, this.reductions); + public create(value: Product): this { + return new MultiValueDomain(value, this.domain, this.reductions) as this; } public static top(domain: Required, reductions: readonly Reduction[] = []): MultiValueDomain { diff --git a/src/abstract-interpretation/domains/partial-product-domain.ts b/src/abstract-interpretation/domains/partial-product-domain.ts index 60021a6e97b..dff1a575941 100644 --- a/src/abstract-interpretation/domains/partial-product-domain.ts +++ b/src/abstract-interpretation/domains/partial-product-domain.ts @@ -1,18 +1,13 @@ import type { Writable } from 'ts-essentials'; -import { type AnyAbstractDomain, AbstractDomain } from './abstract-domain'; -import { Top } from './lattice'; +import { isNotUndefined } from '../../util/assert'; import { Record } from '../../util/record'; +import { type AnyAbstractDomain, AbstractDomain } from './abstract-domain'; /** The type of an abstract product of a product domain mapping named properties of the product to abstract domains */ export type AbstractProduct = { [key in string]?: Domain }; -/** The type of the concrete product of an abstract product mapping each property to a concrete value in the respective concrete domain */ -export type ConcreteProductOf = { - [Key in keyof Product]: Product[Key] extends AbstractDomain ? Concrete : never; -}; - /** * A partial product abstract domain as named Cartesian product of (optional) sub abstract domains. * The sub abstract domains are represented by a (partial) record mapping property names to abstract domains. @@ -20,37 +15,40 @@ export type ConcreteProductOf = { * @template Product - Type of the abstract product of the product domain mapping (optional) property names to abstract domains */ export abstract class PartialProductDomain - extends AbstractDomain, Product, Product, Product> { + extends AbstractDomain { public readonly domain: Required; - constructor(value: Product, domain: Required) { + constructor(value: Product, domain: Required, reduce = true) { super(Record.mapProperties(value, entry => entry?.create(entry.value)) as Product); - (this._value as Writable) = this.reduce(this.value); this.domain = domain; + + if(reduce && this.reduce) { + (this._value as Writable) = this.reduce(this.value); + } } - public abstract create(value: Product): this; + public abstract create(value: Product, reduce?: boolean): this; public bottom(): this { - const result = this.create(this.domain); + const result = {} as Product; - for(const key in result.value) { - result.value[key] = this.domain[key]?.bottom() as typeof result.value[typeof key]; + for(const key in this.domain) { + result[key] = this.domain[key]?.bottom() as typeof result[typeof key]; } - return result; + return this.create(result); } public top(): this { return this.create({} as Product); } - public equals(other: this): boolean { + protected equalsValue(other: this): boolean { if(this.value === other.value) { return true; } for(const key in this.value) { - if(this.value[key] == other.value[key]) { + if(this.value[key] === other.value[key]) { continue; } else if(this.value[key] === undefined || other.value[key] === undefined || !this.value[key].equals(other.value[key])) { return false; @@ -59,7 +57,7 @@ export abstract class PartialProductDomain return true; } - public leq(other: this): boolean { + protected leqValue(other: this): boolean { if(this.value === other.value) { return true; } @@ -73,7 +71,7 @@ export abstract class PartialProductDomain return true; } - public join(other: this): this { + protected joinValue(other: this): this { const result = {} as Product; for(const key in this.domain) { @@ -84,7 +82,7 @@ export abstract class PartialProductDomain return this.create(result); } - public meet(other: this): this { + protected meetValue(other: this): this { const result = {} as Product; for(const key in this.domain) { @@ -99,7 +97,7 @@ export abstract class PartialProductDomain return this.create(result); } - public widen(other: this): this { + protected widenValue(other: this): this { const result = {} as Product; for(const key in this.domain) { @@ -110,7 +108,7 @@ export abstract class PartialProductDomain return this.create(result); } - public narrow(other: this): this { + protected narrowValue(other: this): this { const result = {} as Product; for(const key in this.domain) { @@ -125,64 +123,24 @@ export abstract class PartialProductDomain return this.create(result); } - public concretize(limit: number): ReadonlySet> | typeof Top { - let result = new Set([{} as ConcreteProductOf]); - - for(const key in this.value) { - if(this.value[key] === undefined) { - continue; - } - const concrete = this.value[key].concretize(limit); - - if(concrete === Top) { - return Top; - } - const newResult = new Set>(); - - for(const value of concrete) { - for(const entry of result) { - if(newResult.size >= limit) { - return Top; - } - newResult.add({ ...entry, [key]: value }); - } - } - result = newResult; - } - return result; - } - - public abstract(concrete: ReadonlySet> | typeof Top): this { - if(concrete === Top) { - return this.top(); - } - const result = {} as Product; - - for(const key in this.domain) { - const concreteValues = new Set(concrete.values().map(value => value[key])); - result[key] = this.domain[key]?.abstract(concreteValues) as typeof result[typeof key]; - } - return this.create(result); - } - - public toJson(): unknown { + protected jsonify(): unknown { return Record.mapProperties(this.value, entry => entry?.toJson()); } - public toString(): string { + protected stringify(): string { return '(' + Record.entries(this.value).map(([key, value]) => `${key}: ${value.toString()}`).join(', ') + ')'; } public isTop(): boolean; public isTop(): this is this; public isTop(): this is this { - return Record.values(this.value).length === 0; + return Record.values(this.value).filter(isNotUndefined).length === 0; } public isBottom(): boolean; public isBottom(): this is this; public isBottom(): this is this { - return Record.values(this.value).every(value => value.isBottom()); + return Record.values(this.value).some(value => value.isBottom()); } public isValue(): boolean; @@ -194,7 +152,5 @@ export abstract class PartialProductDomain /** * Optional reduction function for a reduced product domain. */ - protected reduce(value: Product): Product { - return value; - } + protected reduce?(value: Product): Product; } diff --git a/src/abstract-interpretation/domains/positive-interval-domain.ts b/src/abstract-interpretation/domains/positive-interval-domain.ts index e1d834aac22..f50a2630b78 100644 --- a/src/abstract-interpretation/domains/positive-interval-domain.ts +++ b/src/abstract-interpretation/domains/positive-interval-domain.ts @@ -1,17 +1,18 @@ +import { AbstractDomain } from './abstract-domain'; import { IntervalDomain } from './interval-domain'; -import { Bottom, Top } from './lattice'; +import { Bottom } from './lattice'; /** The Top element of the positive interval domain as interval [0, +∞] */ export const PosIntervalTop: PosIntervalValue = [0, +Infinity]; /** The type of the actual values of the positive interval domain as tuple of the lower and upper bound */ -type PosIntervalValue = readonly [lower: number, upper: number]; +export type PosIntervalValue = readonly [lower: number, upper: number]; /** The type of the Top element of the positive interval domain as interval [0, +∞] */ -type PosIntervalTop = typeof PosIntervalTop; +export type PosIntervalTop = typeof PosIntervalTop; /** The type of the Bottom element of the positive interval domain as {@link Bottom} symbol */ -type PosIntervalBottom = typeof Bottom; +export type PosIntervalBottom = typeof Bottom; /** The type of the abstract values of the positive interval domain that are Top, Bottom, or actual values */ -type PosIntervalLift = PosIntervalValue | PosIntervalBottom; +export type PosIntervalLift = PosIntervalValue | PosIntervalBottom; /** * The positive interval abstract domain as positive intervals with possibly zero lower bounds and infinite upper bounds representing possible numeric values. @@ -29,90 +30,59 @@ export class PosIntervalDomain } } - public create(value: PosIntervalLift): this; - public create(value: PosIntervalLift): PosIntervalDomain { - return new PosIntervalDomain(value); + public create(value: PosIntervalLift): this { + return new PosIntervalDomain(value) as this; } public static top(): PosIntervalDomain { - return new PosIntervalDomain(PosIntervalTop); + return new this(PosIntervalTop); } public static bottom(): PosIntervalDomain { - return new PosIntervalDomain(Bottom); + return new this(Bottom); } - public static abstract(concrete: ReadonlySet | typeof Top): PosIntervalDomain { - if(concrete === Top) { - return PosIntervalDomain.top(); - } else if(concrete.size === 0 || concrete.values().some(value => isNaN(value) || value < 0)) { - return PosIntervalDomain.bottom(); - } - return new PosIntervalDomain([Math.min(...concrete), Math.max(...concrete)]); - } - - public top(): this & PosIntervalDomain; - public top(): PosIntervalDomain { - return PosIntervalDomain.top(); - } - - public bottom(): this & PosIntervalDomain; - public bottom(): PosIntervalDomain { - return PosIntervalDomain.bottom(); + public top(): this & PosIntervalDomain { + return this.create(PosIntervalTop) as this & PosIntervalDomain; } - public widen(other: this): this { - if(this.value === Bottom) { - return this.create(other.value); - } else if(other.value === Bottom) { - return this.create(this.value); - } else { - return this.create([ - this.value[0] <= other.value[0] ? this.value[0] : 0, - this.value[1] >= other.value[1] ? this.value[1] : +Infinity - ]); - } + protected widenValue(this: this & PosIntervalDomain, other: PosIntervalDomain): this { + return this.create([ + this.lower <= other.lower ? this.lower : 0, + this.upper >= other.upper ? this.upper : +Infinity + ]); } - public narrow(other: this): this { - if(this.value === Bottom || other.value === Bottom) { - return this.bottom(); - } else if(Math.max(this.value[0], other.value[0]) > Math.min(this.value[1], other.value[1])) { + protected narrowValue(this: this & PosIntervalDomain, other: PosIntervalDomain): this { + if(Math.max(this.lower, other.lower) > Math.min(this.upper, other.upper)) { return this.bottom(); } return this.create([ - this.value[0] === 0 ? other.value[0] : this.value[0], - this.value[1] === +Infinity ? other.value[1] : this.value[1] + this.lower === 0 ? other.lower : this.lower, + this.upper === +Infinity ? other.upper : this.upper ]); } - public abstract(concrete: ReadonlySet | typeof Top): this; - public abstract(concrete: ReadonlySet | typeof Top): PosIntervalDomain { - return PosIntervalDomain.abstract(concrete); - } - public subtract(other: this | PosIntervalLift): this { - const otherValue = other instanceof PosIntervalDomain ? other.value : other; + const otherValue = other instanceof AbstractDomain ? other.value : other; - if(this.value === Bottom || otherValue === Bottom) { - return this.bottom(); - } else { - return this.create([Math.max(this.value[0] - otherValue[0], 0), Math.max(this.value[1] - otherValue[1], 0)]); + if(this.isValue() && otherValue !== Bottom) { + return this.create([Math.max(this.lower - otherValue[0], 0), Math.max(this.upper - otherValue[1], 0)]); } + return this.bottom(); } /** * Extends the lower bound of the current abstract value down to 0. */ public widenDown(): this { - if(this.value === Bottom) { - return this.bottom(); - } else { - return this.create([0, this.value[1]]); + if(this.isValue()) { + return this.create([0, this.upper]); } + return this.bottom(); } - public isTop(): this is PosIntervalDomain { - return this.value !== Bottom && this.value[0] === 0 && this.value[1] === +Infinity; + public isTop(): this is this & PosIntervalDomain { + return this.value !== Bottom && this.lower === 0 && this.upper === +Infinity; } } diff --git a/src/abstract-interpretation/domains/product-domain.ts b/src/abstract-interpretation/domains/product-domain.ts index a60975a4d80..4cef8ddb031 100644 --- a/src/abstract-interpretation/domains/product-domain.ts +++ b/src/abstract-interpretation/domains/product-domain.ts @@ -14,15 +14,15 @@ export abstract class ProductDomain> super(value, value as Required); } - public abstract create(value: Product): this; + public abstract create(value: Product, reduce?: boolean): this; public top(): this { - const result = this.create(this.domain); + const result = {} as Product; - for(const key in result.value) { - result.value[key] = result.value[key]?.top() as typeof result.value[typeof key]; + for(const key in this.domain) { + result[key] = this.domain[key]?.top() as typeof result[typeof key]; } - return result; + return this.create(result); } public isTop(): boolean; diff --git a/src/abstract-interpretation/domains/satisfiable-domain.ts b/src/abstract-interpretation/domains/satisfiable-domain.ts deleted file mode 100644 index 3549f5b73f3..00000000000 --- a/src/abstract-interpretation/domains/satisfiable-domain.ts +++ /dev/null @@ -1,32 +0,0 @@ -import type { Ternary } from '../../util/logic'; - -/** - * An abstract domain with satisfiability checks for concrete values. - */ -export interface SatisfiableDomain { - /** - * Checks whether the current abstract value satisfies a concrete value (i.e. includes a concrete value). - * @see {@link Ternary} for the returned satisfiability result - */ - satisfies(value: T): Ternary; -} - -/** - * Represents the different types of numerical comparators for satisfiability checks for an abstract domain. - */ -export enum NumericalComparator { - Equal, - Less, - LessOrEqual, - Greater, - GreaterOrEqual -} - -/** - * Represents the different types of set comparators for satisfiability checks for an abstract domain. - */ -export enum SetComparator { - Equal, - Subset, - SubsetOrEqual -} diff --git a/src/abstract-interpretation/domains/set-range-domain.ts b/src/abstract-interpretation/domains/set-range-domain.ts index b1450a1c9fd..06b1590a760 100644 --- a/src/abstract-interpretation/domains/set-range-domain.ts +++ b/src/abstract-interpretation/domains/set-range-domain.ts @@ -2,62 +2,63 @@ import { assertUnreachable } from '../../util/assert'; import { setEquals } from '../../util/collections/set'; import { Ternary } from '../../util/logic'; import { AbstractDomain, DEFAULT_INFERENCE_LIMIT } from './abstract-domain'; -import { Bottom, BottomSymbol, Top, TopSymbol } from './lattice'; -import type { SatisfiableDomain } from './satisfiable-domain'; -import { SetComparator } from './satisfiable-domain'; -/* eslint-disable @typescript-eslint/unified-signatures */ +import { Bottom, Top, TopSymbol } from './lattice'; +import { SetComparator, type SetDomain } from './value-abstract-domain'; -/** The Top element of the set range domain with an empty set as minimum set and {@link Top} as range set */ -export const SetRangeTop = { min: new Set(), range: Top } as const satisfies SetRangeValue; -/** The type of the actual values of the set range domain as tuple with a minimum set and range set of additional possible values (i.e. `[{"id","name"}, ∅]`, or `[{"id"}, {"score"}]`) */ -type SetRangeValue = { readonly min: ReadonlySet, readonly range: ReadonlySet | typeof Top }; -/** The type of the Top element of the set range domain as tuple with the empty set as minimum set and {@link Top} as range set (i.e. `[∅, Top]`) */ +/** The Top element of the set range domain with an empty set as must set and {@link Top} as may set */ +export const SetRangeTop = { must: new Set(), may: Top } as const satisfies SetRangeValue; + +/** The type of the actual values of the set range domain as tuple with a set of values that must be present and a set of values that may be present (i.e. `[{"id","name"}, ∅]`, or `[{"id"}, {"score"}]`) */ +export type SetRangeValue = { readonly must: ReadonlySet, readonly may: ReadonlySet | typeof Top }; +/** The type of the Top element of the set range domain as tuple with the empty set as must set and {@link Top} as may set (i.e. `[∅, Top]`) */ type SetRangeTop = typeof SetRangeTop; /** The type of the Bottom element of the set range domain as {@link Bottom} */ type SetRangeBottom = typeof Bottom; /** The type of the abstract values of the set range domain that are Top, Bottom, or actual values */ type SetRangeLift = SetRangeValue | SetRangeTop | SetRangeBottom; -/** The type of the actual values of the set range domain with a finite range (the range cannot be Top) */ -type SetRangeFinite = { readonly min: ReadonlySet, readonly range: ReadonlySet }; +/** The type of the actual values of the set range domain with a finite may set (the may set cannot be Top) */ +type SetRangeFinite = { readonly must: ReadonlySet, readonly may: ReadonlySet }; + +type SetRangeMustSet> = Value extends SetRangeValue ? ReadonlySet : ReadonlySet | typeof Bottom; +type SetRangeMaySet> = Value extends SetRangeFinite ? ReadonlySet : Value extends SetRangeValue ? ReadonlySet | typeof Top : ReadonlySet | typeof Top | typeof Bottom; -/** The type of the actual values of the set range domain as array tuple with a minimum array and range array for better readability (e.g. `[["id","name"], []]`, or `[["id"], ["score"]]`) */ -export type ArrayRangeValue = { readonly min: T[], readonly range: T[] | typeof Top }; +/** The type of the actual values of the set range domain as array tuple with a must array and may array for better readability (e.g. `[["id","name"], []]`, or `[["id"], ["score"]]`) */ +export type ArrayRangeValue = { readonly must: T[], readonly may: T[] | typeof Top }; -/** The type for the maximum number of elements in the minimum set and maximum set of the set range domain before over-approximation */ -export type SetRangeLimit = { readonly min: number, readonly range: number }; -const DefaultLimit = { min: DEFAULT_INFERENCE_LIMIT, range: DEFAULT_INFERENCE_LIMIT } as const satisfies SetRangeLimit; +/** The type for the maximum number of elements in the must set and may set of the set range domain before over-approximation */ +export type SetRangeLimit = { readonly must: number, readonly may: number }; /** - * The set range abstract domain as range of possible value sets with a minimum set of values and a range of possible additional values + * 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 {@link Bottom} symbol and the Top element is defined as the range `[∅, Top]` where the minimum set is the empty set and the range is {@link Top}. + * The Bottom element is defined as {@link 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 {@link Top}. * @template T - Type of the values in the sets in the abstract domain * @template Value - Type of the constraint in the abstract domain (Top, Bottom, or an actual value) */ export class SetRangeDomain = SetRangeLift> - extends AbstractDomain, SetRangeValue, SetRangeTop, SetRangeBottom, Value> - implements SatisfiableDomain> { + extends AbstractDomain, SetRangeTop, SetRangeBottom, Value> + implements SetDomain { - public readonly limit: SetRangeLimit; - private readonly setType: typeof Set; + public readonly limit: SetRangeLimit; + protected readonly setType: typeof Set; /** - * @param limit - A limit for the maximum number of elements to store in the minimum set and maximum set before over-approximation + * @param limit - A limit for the maximum number of elements to store in the must set and may set before over-approximation * @param newSet - An optional set constructor for the domain elements if the type `T` is not storable in a HashSet */ - constructor(value: Value | ArrayRangeValue, limit: SetRangeLimit | number = DefaultLimit, setType: typeof Set = Set) { - limit = typeof limit === 'number' ? { min: limit, range: limit } : limit; + constructor(value: Value | ArrayRangeValue, limit: SetRangeLimit | number = DEFAULT_INFERENCE_LIMIT, setType: typeof Set = Set) { + limit = typeof limit === 'number' ? { must: limit, may: limit } : limit; if(value !== Bottom) { - const minSet = new setType(value.min); - const rangeSet = value.range === Top ? Top : new setType(value.range); - const minExceeds = minSet.size > limit.min; - const rangeExceeds = rangeSet === Top || rangeSet.size > limit.range || minSet.size + rangeSet.size > limit.min + limit.range; - - const min = minExceeds ? new setType(minSet.values().take(limit.min)) : minSet; - const range = rangeExceeds ? Top : minSet.union(rangeSet).difference(min); - super({ min, range } as SetRangeValue as Value); + const mustSet = new setType(value.must); + const maySet = value.may === Top ? Top : new setType(value.may); + const mustExceeds = mustSet.size > limit.must; + const mayExceeds = maySet === Top || maySet.size > limit.may || mustSet.size + maySet.size > limit.must + limit.may; + + const must = mustExceeds ? new setType(mustSet.values().take(limit.must)) : mustSet; + const may = mayExceeds ? Top : mustSet.union(maySet).difference(must); + super({ must, may } as Value); } else { super(value); } @@ -65,100 +66,98 @@ export class SetRangeDomain = SetRangeLift> this.setType = setType; } - public create(value: SetRangeLift | ArrayRangeValue): this; - public create(value: SetRangeLift | ArrayRangeValue): SetRangeDomain { - return new SetRangeDomain(value, this.limit, this.setType); + public create(value: SetRangeLift | ArrayRangeValue): this { + return new SetRangeDomain(value, this.limit, this.setType) as this; } /** - * The minimum set (lower bound) of the set range representing all values that must exist (subset of {@link upper}). + * The set of values that must be present in the set. */ - public lower(): Value extends SetRangeValue ? ReadonlySet : ReadonlySet | typeof Bottom { - if(this.value === Bottom) { - return Bottom as Value extends SetRangeValue ? ReadonlySet : ReadonlySet | typeof Bottom; - } - return this.value.min; + public get must(): SetRangeMustSet { + return (this.isValue() ? this.value.must : Bottom) as SetRangeMustSet; + } + + /** + * The set of values that may be present in the set (can be {@link Top}). + */ + public get may(): SetRangeMaySet { + return (this.isValue() ? this.value.may : Bottom) as SetRangeMaySet; + } + + /** + * The lower bound of the set range representing all values that must be present (equals the must set). + */ + public lower(this: SetRangeDomain>): ReadonlySet; + public lower(this: SetRangeDomain>): ReadonlySet | typeof Bottom; + public lower(): ReadonlySet | typeof Bottom { + return this.must; } /** - * The maximum set (upper bound) of the set range representing all values that can possibly exist (union of {@link lower} and range). + * The upper bound of the set range representing all values that can possibly be present (union of must set and may set). */ - public upper(): Value extends SetRangeFinite ? ReadonlySet : Value extends SetRangeValue ? ReadonlySet | typeof Top : ReadonlySet | typeof Top | typeof Bottom { - if(this.value === Bottom) { - return Bottom as Value extends SetRangeFinite ? ReadonlySet : Value extends SetRangeValue ? ReadonlySet | typeof Top : ReadonlySet | typeof Top | typeof Bottom; - } else if(this.value.range === Top) { - return Top as Value extends SetRangeFinite ? ReadonlySet : ReadonlySet | typeof Top; + public upper(this: SetRangeDomain>): ReadonlySet; + public upper(this: SetRangeDomain>): ReadonlySet | typeof Top; + public upper(this: SetRangeDomain>): ReadonlySet | typeof Top | typeof Bottom; + public upper(): ReadonlySet | typeof Top | typeof Bottom { + return this.isFinite() ? this.must.union(this.may) : this.may; + } + + public from(...values: ReadonlySet[] | T[][]): this { + if(values.length === 0) { + return this.bottom(); } - return this.value.min.union(this.value.range) as ReadonlySet as Value extends SetRangeFinite ? ReadonlySet : ReadonlySet | typeof Top; + const sets = values.map(value => new Set(value)); + const must = sets.reduce((result, set) => result.intersection(set)); + const may = sets.reduce((result, set) => result.union(set)).difference(must); + + return this.create({ must, may }); } public static top(limit?: SetRangeLimit | number, setType?: typeof Set): SetRangeDomain { - return new SetRangeDomain(SetRangeTop, limit, setType); + return new this(SetRangeTop, limit, setType); } public static bottom(limit?: SetRangeLimit | number, setType?: typeof Set): SetRangeDomain { - return new SetRangeDomain(Bottom, limit, setType); + return new this(Bottom, limit, setType); } - public static abstract(concrete: ReadonlySet> | typeof Top, limit?: SetRangeLimit | number, setType?: typeof Set): SetRangeDomain { - if(concrete === Top) { - return SetRangeDomain.top(limit, setType); - } else if(concrete.size === 0) { - return SetRangeDomain.bottom(limit, setType); + public static from(values: Set | T[] | Set[] | T[][], limit?: SetRangeLimit | number, setType?: typeof Set): SetRangeDomain { + values = !Array.isArray(values) ? [values] : values.every(value => value instanceof Set || Array.isArray(value)) ? values : [values]; + + if(values.length === 0) { + return this.bottom(); } - const lower = concrete.values().reduce((result, set) => result.intersection(set)); - const upper = concrete.values().reduce((result, set) => result.union(set)); + const sets = values.map(value => new Set(value)); + const must = sets.reduce((result, set) => result.intersection(set)); + const may = sets.reduce((result, set) => result.union(set)).difference(must); - return new SetRangeDomain({ min: lower, range: upper.difference(lower) }, limit, setType); + return new this({ must, may }, limit, setType); } - public top(): this & SetRangeDomain; - public top(): SetRangeDomain { - return SetRangeDomain.top(this.limit, this.setType); + public top(): this & SetRangeDomain { + return this.create(SetRangeTop) as this & SetRangeDomain; } - public bottom(): this & SetRangeDomain; - public bottom(): SetRangeDomain { - return SetRangeDomain.bottom(this.limit, this.setType); + public bottom(): this & SetRangeDomain { + return this.create(Bottom) as this & SetRangeDomain; } - public equals(other: this): boolean { - if(this.value === other.value) { - return true; - } else if(this.value === Bottom || other.value === Bottom || !setEquals(this.value.min, other.value.min)) { - return false; - } else if(this.value.range === other.value.range) { - return true; - } - return this.value.range !== Top && other.value.range !== Top && setEquals(this.value.range, other.value.range); + protected equalsValue(this: SetRangeDomain>, other: SetRangeDomain>): boolean { + return setEquals(this.must, other.must) && (this.may === other.may || (this.may !== Top && other.may !== Top && setEquals(this.may, other.may))); } - public leq(other: this): boolean { + protected leqValue(this: SetRangeDomain>, other: SetRangeDomain>): boolean { const thisLower = this.lower(), thisUpper = this.upper(); const otherLower = other.lower(), otherUpper = other.upper(); - if(thisLower === Bottom || thisUpper === Bottom) { - return true; - } else if(otherLower === Bottom || otherUpper === Bottom || !otherLower.isSubsetOf(thisLower)) { - return false; - } else if(otherUpper === Top) { - return true; - } - return thisUpper !== Top && thisUpper.isSubsetOf(otherUpper); + return otherLower.isSubsetOf(thisLower) && (otherUpper === Top || (thisUpper !== Top && thisUpper.isSubsetOf(otherUpper))); } - public join(other: SetRangeLift | ArrayRangeValue): this; - public join(other: this): this; - public join(other: this | SetRangeLift | ArrayRangeValue): this { - other = other instanceof SetRangeDomain ? other : this.create(other); + protected joinValue(this: this & SetRangeDomain>, other: SetRangeDomain>): this { const thisLower = this.lower(), thisUpper = this.upper(); const otherLower = other.lower(), otherUpper = other.upper(); - if(thisLower === Bottom || thisUpper === Bottom) { - return this.create(other.value); - } else if(otherLower === Bottom || otherUpper === Bottom) { - return this.create(this.value); - } const joinLower = thisLower.intersection(otherLower); let joinUpper; @@ -167,19 +166,16 @@ export class SetRangeDomain = SetRangeLift> } else { joinUpper = thisUpper.union(otherUpper); } - return this.create({ min: joinLower, range: joinUpper === Top ? Top : joinUpper.difference(joinLower) }); + return this.create({ + must: joinLower, + may: joinUpper === Top ? Top : joinUpper.difference(joinLower) + }); } - public meet(other: SetRangeLift | ArrayRangeValue): this; - public meet(other: this): this; - public meet(other: this | SetRangeLift | ArrayRangeValue): this { - other = other instanceof SetRangeDomain ? other : this.create(other); + protected meetValue(this: this & SetRangeDomain>, other: SetRangeDomain>): this { const thisLower = this.lower(), thisUpper = this.upper(); const otherLower = other.lower(), otherUpper = other.upper(); - if(thisLower === Bottom || thisUpper === Bottom || otherLower === Bottom || otherUpper === Bottom) { - return this.bottom(); - } const meetLower = thisLower.union(otherLower); let meetUpper; @@ -193,22 +189,21 @@ export class SetRangeDomain = SetRangeLift> if(meetUpper !== Top && !meetLower.isSubsetOf(meetUpper)) { return this.bottom(); } - return this.create({ min: meetLower, range: meetUpper === Top ? Top : meetUpper.difference(meetLower) }); + return this.create({ + must: meetLower, + may: meetUpper === Top ? Top : meetUpper.difference(meetLower) + }); } - /** - * Creates the union of this abstract value and another abstract value by creating the union of the minimum and maximum set, respectively. - */ public union(other: this | SetRangeLift | ArrayRangeValue): this { other = other instanceof SetRangeDomain ? other : this.create(other); + + if(!this.isValue() || !other.isValue()) { + return this.bottom(); + } const thisLower = this.lower(), thisUpper = this.upper(); const otherLower = other.lower(), otherUpper = other.upper(); - if(thisLower === Bottom || thisUpper === Bottom) { - return this.create(other.value); - } else if(otherLower === Bottom || otherUpper === Bottom) { - return this.create(this.value); - } const unionLower = thisLower.union(otherLower); let unionUpper; @@ -217,20 +212,21 @@ export class SetRangeDomain = SetRangeLift> } else { unionUpper = thisUpper.union(otherUpper); } - return this.create({ min: unionLower, range: unionUpper === Top ? Top : unionUpper.difference(unionLower) }); + return this.create({ + must: unionLower, + may: unionUpper === Top ? Top : unionUpper.difference(unionLower) + }); } - /** - * Creates the intersection of this abstract value and another abstract value by creating the intersection of the minimum and maximum set, respectively. - */ public intersect(other: this | SetRangeLift | ArrayRangeValue): this { other = other instanceof SetRangeDomain ? other : this.create(other); - const thisLower = this.lower(), thisUpper = this.upper(); - const otherLower = other.lower(), otherUpper = other.upper(); - if(thisLower === Bottom || thisUpper === Bottom || otherLower === Bottom || otherUpper === Bottom) { + if(!this.isValue() || !other.isValue()) { return this.bottom(); } + const thisLower = this.lower(), thisUpper = this.upper(); + const otherLower = other.lower(), otherUpper = other.upper(); + const intersectLower = thisLower.intersection(otherLower); let intersectUpper; @@ -241,84 +237,72 @@ export class SetRangeDomain = SetRangeLift> } else { intersectUpper = thisUpper.intersection(otherUpper); } - return this.create({ min: intersectLower, range: intersectUpper === Top ? Top : intersectUpper.difference(intersectLower) }); + return this.create({ + must: intersectLower, + may: intersectUpper === Top ? Top : intersectUpper.difference(intersectLower) + }); } - /** - * Subtracts another abstract value from the current abstract value by removing all elements of the other abstract value from the current abstract value. - */ public subtract(other: this | SetRangeLift | ArrayRangeValue): this { other = other instanceof SetRangeDomain ? other : this.create(other); - const thisLower = this.lower(), thisUpper = this.upper(); - const otherLower = other.lower(), otherUpper = other.upper(); - if(thisLower === Bottom || thisUpper === Bottom) { + if(!this.isValue() || !other.isValue()) { return this.bottom(); - } else if(otherLower === Bottom || otherUpper === Bottom) { - return this.create(this.value); } - let subLower; + const thisLower = this.lower(), thisUpper = this.upper(); + const otherLower = other.lower(), otherUpper = other.upper(); + + let subtractLower; if(otherUpper === Top) { - subLower = new Set(); + subtractLower = new Set(); } else { - subLower = thisLower.difference(otherUpper); + subtractLower = thisLower.difference(otherUpper); } - let subUpper; + let subtractUpper; if(thisUpper === Top) { - subUpper = Top; + subtractUpper = Top; } else if(otherUpper === Top) { - subUpper = thisUpper.difference(otherLower); + subtractUpper = thisUpper.difference(otherLower); } else { - subUpper = thisUpper.difference(otherUpper); + subtractUpper = thisUpper.difference(otherUpper); } - return this.create({ min: subLower, range: subUpper === Top ? Top : subUpper.difference(subLower) }); + return this.create({ + must: subtractLower, + may: subtractUpper === Top ? Top : subtractUpper.difference(subtractLower) + }); } - public widen(other: this): this { + protected widenValue(this: this & SetRangeDomain>, other: SetRangeDomain>): this { const thisLower = this.lower(), thisUpper = this.upper(); const otherLower = other.lower(), otherUpper = other.upper(); - if(thisLower === Bottom || thisUpper === Bottom) { - return this.create(other.value); - } else if(otherLower === Bottom || otherUpper === Bottom) { - return this.create(this.value); - } let widenLower; - if(!thisLower.isSubsetOf(otherLower)) { - widenLower = new Set(); - } else { + if(thisLower.isSubsetOf(otherLower)) { widenLower = thisLower; + } else { + widenLower = new Set(); } let widenUpper; - if(thisUpper === Top || otherUpper === Top || !otherUpper.isSubsetOf(thisUpper)) { - widenUpper = Top; - } else { + if(thisUpper !== Top && otherUpper !== Top && otherUpper.isSubsetOf(thisUpper)) { widenUpper = thisUpper; + } else { + widenUpper = Top; } - return this.create({ min: widenLower, range: widenUpper === Top ? Top : widenUpper.difference(widenLower) }); + return this.create({ + must: widenLower, + may: widenUpper === Top ? Top : widenUpper.difference(widenLower) + }); } - public narrow(other: this): this { + protected narrowValue(this: this & SetRangeDomain>, other: SetRangeDomain>): this { const thisLower = this.lower(), thisUpper = this.upper(); const otherLower = other.lower(), otherUpper = other.upper(); - if(thisLower === Bottom || thisUpper === Bottom || otherLower === Bottom || otherUpper === Bottom) { - return this.bottom(); - } - let meetUpper; - - if(thisUpper === Top) { - meetUpper = otherUpper; - } else if(otherUpper === Top) { - meetUpper = thisUpper; - } else { - meetUpper = thisUpper.intersection(otherUpper); - } - if(meetUpper !== Top && !thisLower.union(otherLower).isSubsetOf(meetUpper)) { + if(this.meetValue(other).isBottom()) { return this.bottom(); } let narrowLower; @@ -335,30 +319,10 @@ export class SetRangeDomain = SetRangeLift> } else { narrowUpper = thisUpper; } - return this.create({ min: narrowLower, range: narrowUpper === Top ? Top : narrowUpper.difference(narrowLower) }); - } - - public concretize(limit: number): ReadonlySet> | typeof Top { - if(this.value === Bottom) { - return new Set(); - } else if(this.value.range === Top || 2**(this.value.range.size) > limit) { - return Top; - } - const subsets = [new this.setType()]; - - for(const element of this.value.range) { - const newSubsets = subsets.map(subset => new this.setType([...subset, element])); - - for(const subset of newSubsets) { - subsets.push(subset); - } - } - return new Set(subsets.map(subset => this.value === Bottom ? subset : this.value.min.union(subset))); - } - - public abstract(concrete: ReadonlySet> | typeof Top): this; - public abstract(concrete: ReadonlySet> | typeof Top): SetRangeDomain { - return SetRangeDomain.abstract(concrete, this.limit); + return this.create({ + must: narrowLower, + may: narrowUpper === Top ? Top : narrowUpper.difference(narrowLower) + }); } public satisfies(set: ReadonlySet | T[], comparator: SetComparator = SetComparator.Equal): Ternary { @@ -394,68 +358,56 @@ export class SetRangeDomain = SetRangeLift> } /** - * Extends the minimum set of the current abstract value down to the empty set. + * Extends the must set of the current abstract value down to the empty set. */ public widenDown(): this { - const upper = this.upper(); - - if(upper === Bottom) { - return this.bottom(); - } else { - return this.create({ min: new this.setType(), range: upper }); + if(this.isValue()) { + return this.create({ must: new this.setType(), may: this.upper() }); } + return this.bottom(); } /** - * Extends the maximum set of the current abstract value up to {@link Top}. + * Extends the may set of the current abstract value up to {@link Top}. */ public widenUp(): this { - const lower = this.lower(); - - if(lower === Bottom) { - return this.bottom(); - } else { - return this.create({ min: lower, range: Top }); + if(this.isValue()) { + return this.create({ must: this.must, may: Top }); } + return this.bottom(); } - public toJson(): unknown { - if(this.value === Bottom) { - return this.value.description; - } - const min = this.value.min.values().toArray(); - const range = this.value.range === Top ? this.value.range.description : this.value.range.values().toArray(); + protected jsonify(this: SetRangeDomain>): unknown { + const must = this.must.values().toArray(); + const may = this.may === Top ? Top.description : this.may.values().toArray(); - return { min, range }; + return { must, may }; } - public toString(): string { - if(this.value === Bottom) { - return BottomSymbol; - } else if(this.value.range === Top) { - const minString = this.value.min.values().map(AbstractDomain.toString).toArray().join(', '); + protected stringify(this: SetRangeDomain>): string { + const must = this.must.values().map(AbstractDomain.toString).toArray().join(', '); - return `[{${minString}}, ${TopSymbol}]`; + if(this.may === Top) { + return `[{${must}}, ${TopSymbol}]`; } - const minString = this.value.min.values().map(AbstractDomain.toString).toArray().join(', '); - const rangeString = this.value.range.values().map(AbstractDomain.toString).toArray().join(', '); + const may = this.may.values().map(AbstractDomain.toString).toArray().join(', '); - return `[{${minString}}, {${rangeString}}]`; + return `[{${must}}, {${may}}]`; } - public isTop(): this is SetRangeDomain { - return this.value !== Bottom && this.value.min.size === 0 && this.value.range === Top; + public isTop(): this is this & SetRangeDomain { + return this.isValue() && this.must.size === 0 && this.may === Top; } - public isBottom(): this is SetRangeDomain { + public isBottom(): this is this & SetRangeDomain { return this.value === Bottom; } - public isValue(): this is SetRangeDomain> { + public isValue(): this is this & SetRangeDomain> { return this.value !== Bottom; } - public isFinite(): this is SetRangeDomain> { - return this.value !== Bottom && this.value.range !== Top; + public isFinite(): this is this & SetRangeDomain> { + return this.isValue() && this.may !== Top; } } diff --git a/src/abstract-interpretation/domains/set-upper-bound-domain.ts b/src/abstract-interpretation/domains/set-upper-bound-domain.ts index 7f6e1d674ac..bb8db885f4b 100644 --- a/src/abstract-interpretation/domains/set-upper-bound-domain.ts +++ b/src/abstract-interpretation/domains/set-upper-bound-domain.ts @@ -2,9 +2,8 @@ import { assertUnreachable } from '../../util/assert'; import { setEquals } from '../../util/collections/set'; import { Ternary } from '../../util/logic'; import { AbstractDomain, DEFAULT_INFERENCE_LIMIT } from './abstract-domain'; -import { Bottom, BottomSymbol, Top, TopSymbol } from './lattice'; -import { type SatisfiableDomain, SetComparator } from './satisfiable-domain'; -/* eslint-disable @typescript-eslint/unified-signatures */ +import { Bottom, Top } from './lattice'; +import { type SetDomain, SetComparator } from './value-abstract-domain'; /** The type of the actual values of the set upper bound domain as set */ type SetUpperBoundValue = ReadonlySet; @@ -22,11 +21,11 @@ type SetUpperBoundLift = SetUpperBoundValue | SetUpperBoundTop | SetUpperB * @template Value - Type of the constraint in the abstract domain (Top, Bottom, or an actual value) */ export class SetUpperBoundDomain = SetUpperBoundLift> - extends AbstractDomain, SetUpperBoundValue, SetUpperBoundTop, SetUpperBoundBottom, Value> - implements SatisfiableDomain> { + extends AbstractDomain, SetUpperBoundTop, SetUpperBoundBottom, Value> + implements SetDomain { - public readonly limit: number; - private readonly setType: typeof Set; + public readonly limit: number; + protected readonly setType: typeof Set; /** * @param limit - A limit for the maximum number of elements to store in the set @@ -46,132 +45,91 @@ export class SetUpperBoundDomain = SetUppe this.setType = setType; } - public create(value: SetUpperBoundLift | T[]): this; - public create(value: SetUpperBoundLift | T[]): SetUpperBoundDomain { - return new SetUpperBoundDomain(value, this.limit, this.setType); + public create(value: SetUpperBoundLift | T[]): this { + return new SetUpperBoundDomain(value, this.limit, this.setType) as this; + } + + public from(...values: ReadonlySet[] | T[][]): this { + if(values.length === 0) { + return this.bottom(); + } + const sets = values.map(value => new Set(value)); + + return this.create(sets.reduce((result, set) => result.union(set))); } public static top(limit?: number, setType?: typeof Set): SetUpperBoundDomain { - return new SetUpperBoundDomain(Top, limit, setType); + return new this(Top, limit, setType); } public static bottom(limit?: number, setType?: typeof Set): SetUpperBoundDomain { - return new SetUpperBoundDomain(Bottom, limit, setType); + return new this(Bottom, limit, setType); } - public static abstract(concrete: ReadonlySet> | typeof Top, limit?: number, setType?: typeof Set): SetUpperBoundDomain { - if(concrete === Top) { - return SetUpperBoundDomain.top(limit, setType); - } else if(concrete.size === 0) { - return SetUpperBoundDomain.bottom(limit, setType); + public static from(values: Set | T[] | Set[] | T[][], limit?: number, setType?: typeof Set): SetUpperBoundDomain { + values = !Array.isArray(values) ? [values] : values.every(value => value instanceof Set || Array.isArray(value)) ? values : [values]; + + if(values.length === 0) { + return this.bottom(); } - return new SetUpperBoundDomain(concrete.values().reduce((result, set) => result.union(set)), limit, setType); - } + const sets = values.map(value => new Set(value)); - public top(): this & SetUpperBoundDomain; - public top(): SetUpperBoundDomain { - return SetUpperBoundDomain.top(this.limit, this.setType); + return new this(sets.reduce((result, set) => result.union(set)), limit, setType); } - public bottom(): this & SetUpperBoundDomain; - public bottom(): SetUpperBoundDomain { - return SetUpperBoundDomain.bottom(this.limit, this.setType); + public top(): this & SetUpperBoundDomain { + return this.create(Top) as this & SetUpperBoundDomain; } - public equals(other: this): boolean { - return this.value === other.value || (this.isValue() && other.isValue() && setEquals(this.value, other.value)); + public bottom(): this & SetUpperBoundDomain { + return this.create(Bottom) as this & SetUpperBoundDomain; } - public leq(other: this): boolean { - return this.value === Bottom || other.value === Top || (this.isValue() && other.isValue() && this.value.isSubsetOf(other.value)); + protected equalsValue(this: SetUpperBoundDomain>, other: SetUpperBoundDomain>): boolean { + return setEquals(this.value, other.value); } - public join(other: SetUpperBoundLift | T[]): this; - public join(other: this): this; - public join(other: this | SetUpperBoundLift | T[]): this { - const otherValue = other instanceof SetUpperBoundDomain ? other.value : Array.isArray(other) ? new this.setType(other) : other; - - if(this.value === Top || otherValue === Top) { - return this.top(); - } else if(this.value === Bottom) { - return this.create(otherValue); - } else if(otherValue === Bottom) { - return this.create(this.value); - } else { - return this.create(this.value.union(otherValue)); - } + protected leqValue(this: SetUpperBoundDomain>, other: SetUpperBoundDomain>): boolean { + return this.value.isSubsetOf(other.value); } - public meet(other: SetUpperBoundLift | T[]): this; - public meet(other: this): this; - public meet(other: this | SetUpperBoundLift | T[]): this { - const otherValue = other instanceof SetUpperBoundDomain ? other.value : Array.isArray(other) ? new this.setType(other) : other; + protected joinValue(this: this & SetUpperBoundDomain>, other: SetUpperBoundDomain>): this { + return this.create(this.value.union(other.value)); + } - if(this.value === Bottom || otherValue === Bottom) { - return this.bottom(); - } else if(this.value === Top) { - return this.create(otherValue); - } else if(otherValue === Top) { - return this.create(this.value); - } else { - return this.create(this.value.intersection(otherValue)); - } + protected meetValue(this: this & SetUpperBoundDomain>, other: SetUpperBoundDomain>): this { + return this.create(this.value.intersection(other.value)); } - /** - * Subtracts another abstract value from the current abstract value by removing all elements of the other abstract value from the current abstract value. - */ - public subtract(other: this | SetUpperBoundLift | T[]): this { - const otherValue = other instanceof SetUpperBoundDomain ? other.value : Array.isArray(other) ? new this.setType(other) : other; + public union(other: this | SetUpperBoundLift | T[]): this { + other = other instanceof AbstractDomain ? other : this.create(other); - if(this.value === Top) { - return this.top(); - } else if(this.value === Bottom) { + if(this.isBottom() || other.isBottom()) { return this.bottom(); - } else if(otherValue === Top || otherValue === Bottom) { - return this.create(this.value); - } else { - return this.create(this.value.difference(otherValue)); } + return this.join(other); } - public widen(other: this): this { - if(this.value === Bottom) { - return this.create(other.value); - } else if(other.value === Bottom) { - return this.create(this.value); - } - return other.leq(this) ? this.create(this.value) : this.top(); - } + public intersect(other: this | SetUpperBoundLift | T[]): this { + other = other instanceof AbstractDomain ? other : this.create(other); - public narrow(other: this): this { - if(this.value === Bottom || other.value === Bottom) { + if(this.isBottom() || other.isBottom()) { return this.bottom(); } - return this.isTop() ? this.create(other.value) : this.create(this.value); + return this.meet(other); } - public concretize(limit: number): ReadonlySet> | typeof Top { - if(this.value === Bottom) { - return new Set(); - } else if(this.value === Top || 2**(this.value.size) > limit) { - return Top; - } - const subsets = [new this.setType()]; - - for(const element of this.value.values()) { - const newSubsets = subsets.map(subset => new this.setType([...subset, element])); + public subtract(other: this | SetUpperBoundLift): this { + other = other instanceof AbstractDomain ? other : this.create(other); - for(const subset of newSubsets) { - subsets.push(subset); - } + if(this.isBottom() || other.isBottom()) { + return this.bottom(); + } else if(this.isValue() && other.isValue()) { + return this.create(this.value.difference(other.value)); + } else if(this.isValue()) { + return this.create(this.value); } - return new Set(subsets); - } - - public abstract(concrete: ReadonlySet> | typeof Top): this; - public abstract(concrete: ReadonlySet> | typeof Top): SetUpperBoundDomain { - return SetUpperBoundDomain.abstract(concrete, this.limit, this.setType); + return this.top(); } public satisfies(set: ReadonlySet | T[], comparator: SetComparator = SetComparator.Equal): Ternary { @@ -195,33 +153,23 @@ export class SetUpperBoundDomain = SetUppe } } - public toJson(): unknown { - if(this.value === Top || this.value === Bottom) { - return this.value.description; - } + protected jsonify(this: SetUpperBoundDomain>): unknown { return this.value.values().toArray(); } - public toString(): string { - if(this.value === Top) { - return TopSymbol; - } else if(this.value === Bottom) { - return BottomSymbol; - } - const string = this.value.values().map(AbstractDomain.toString).toArray().join(', '); - - return `{${string}}`; + protected stringify(this: SetUpperBoundDomain>): string { + return `{${this.value.values().map(AbstractDomain.toString).toArray().join(', ')}}`; } - public isTop(): this is SetUpperBoundDomain { + public isTop(): this is this & SetUpperBoundDomain { return this.value === Top; } - public isBottom(): this is SetUpperBoundDomain { + public isBottom(): this is this & SetUpperBoundDomain { return this.value === Bottom; } - public isValue(): this is SetUpperBoundDomain> { + public isValue(): this is this & SetUpperBoundDomain> { return this.value !== Top && this.value !== Bottom; } } diff --git a/src/abstract-interpretation/domains/singleton-domain.ts b/src/abstract-interpretation/domains/singleton-domain.ts index f016e7df701..d052dbb3d95 100644 --- a/src/abstract-interpretation/domains/singleton-domain.ts +++ b/src/abstract-interpretation/domains/singleton-domain.ts @@ -1,8 +1,7 @@ import { Ternary } from '../../util/logic'; import { AbstractDomain } from './abstract-domain'; -import { Bottom, BottomSymbol, Top, TopSymbol } from './lattice'; -import type { SatisfiableDomain } from './satisfiable-domain'; -/* eslint-disable @typescript-eslint/unified-signatures */ +import { Bottom, Top } from './lattice'; +import type { ValueDomain } from './value-abstract-domain'; /** The type of the actual values of the singleton domain as single value */ type SingletonValue = T; @@ -20,105 +19,73 @@ type SingletonLift = SingletonValue | SingletonTop | SingletonBottom; * @template Value - Type of the constraint in the abstract domain (Top, Bottom, or an actual value) */ export class SingletonDomain = SingletonLift> - extends AbstractDomain, SingletonTop, SingletonBottom, Value> - implements SatisfiableDomain { + extends AbstractDomain, SingletonTop, SingletonBottom, Value> + implements ValueDomain { - public create(value: SingletonLift): this; - public create(value: SingletonLift): SingletonDomain { - return new SingletonDomain(value); + public create(value: SingletonLift): this { + return new SingletonDomain(value) as this; + } + + public from(...values: T[]): this { + if(values.length === 0) { + return this.bottom(); + } else if(values.length > 1) { + return this.top(); + } + return this.create(values[0]); } public static top(): SingletonDomain { - return new SingletonDomain(Top); + return new this(Top); } public static bottom(): SingletonDomain { - return new SingletonDomain(Bottom); + return new this(Bottom); } - public static abstract(concrete: ReadonlySet | typeof Top): SingletonDomain { - if(concrete === Top || concrete.size > 1) { - return SingletonDomain.top(); - } else if(concrete.size === 0) { - return SingletonDomain.bottom(); + public static from(...values: T[]): SingletonDomain { + if(values.length === 0) { + return this.bottom(); + } else if(values.length > 1) { + return this.top(); } - return new SingletonDomain([...concrete][0]); + return new this(values[0]); } - public top(): this & SingletonDomain; - public top(): SingletonDomain { - return SingletonDomain.top(); + public top(): this & SingletonDomain { + return this.create(Top) as this & SingletonDomain; } - public bottom(): this & SingletonDomain; - public bottom(): SingletonDomain { - return SingletonDomain.bottom(); + public bottom(): this & SingletonDomain { + return this.create(Bottom) as this & SingletonDomain; } - public equals(other: this): boolean { + protected equalsValue(this: SingletonDomain>, other: SingletonDomain>): boolean { return this.value === other.value; } - public leq(other: this): boolean { - return this.value === Bottom || other.value === Top || (this.isValue() && other.isValue() && this.value <= other.value); - } - - public join(other: SingletonLift): this; - public join(other: this): this; - public join(other: this | SingletonLift): this { - const otherValue = other instanceof SingletonDomain ? other.value : other; - - if(this.value === Bottom) { - return this.create(otherValue); - } else if(otherValue === Bottom) { - return this.create(this.value); - } else if(this.value !== otherValue) { - return this.top(); - } else { - return this.create(this.value); - } - } - - public meet(other: SingletonLift): this; - public meet(other: this): this; - public meet(other: this | SingletonLift): this { - const otherValue = other instanceof SingletonDomain ? other.value : other; - - if(this.value === Top) { - return this.create(otherValue); - } else if(otherValue === Top) { - return this.create(this.value); - } else if(this.value !== otherValue) { - return this.bottom(); - } else { - return this.create(this.value); - } + protected leqValue(this: SingletonDomain>, other: SingletonDomain>): boolean { + return this.value <= other.value; } - public widen(other: this): this { - return this.join(other); // Using join for widening as the lattice is finite + protected joinValue(this: this & SingletonDomain>, other: this & SingletonDomain>): this { + return this.equals(other) ? this.create(this.value) : this.top(); } - public narrow(other: this): this { - return this.meet(other); // Using meet for narrowing as the lattice is finite + protected meetValue(this: this & SingletonDomain>, other: this & SingletonDomain>): this { + return this.equals(other) ? this.create(this.value) : this.bottom(); } - public concretize(): ReadonlySet | typeof Top { - if(this.value === Top) { - return Top; - } else if(this.value === Bottom) { - return new Set(); - } - return new Set([this.value as T]); + protected widenValue(this: this & SingletonDomain>, other: this & SingletonDomain>): this { + return this.joinValue(other); // Using join for widening as the lattice is finite } - public abstract(concrete: ReadonlySet | typeof Top): this; - public abstract(concrete: ReadonlySet | typeof Top): SingletonDomain { - return SingletonDomain.abstract(concrete); + protected narrowValue(this: this & SingletonDomain>, other: this & SingletonDomain>): this { + return this.meetValue(other); // Using meet for narrowing as the lattice is finite } public satisfies(value: T): Ternary { - if(this.isValue() && this.value === value) { + if(this.equals(this.from(value))) { return Ternary.Always; } else if(this.isTop()) { return Ternary.Maybe; @@ -126,33 +93,23 @@ export class SingletonDomain = SingletonLift { + public isTop(): this is this & SingletonDomain { return this.value === Top; } - public isBottom(): this is SingletonDomain { + public isBottom(): this is this & SingletonDomain { return this.value === Bottom; } - public isValue(): this is SingletonDomain> { + public isValue(): this is this & SingletonDomain> { return this.value !== Top && this.value !== Bottom; } } diff --git a/src/abstract-interpretation/domains/state-abstract-domain.ts b/src/abstract-interpretation/domains/state-abstract-domain.ts index 9aa67eb1ff2..bd775b9faec 100644 --- a/src/abstract-interpretation/domains/state-abstract-domain.ts +++ b/src/abstract-interpretation/domains/state-abstract-domain.ts @@ -1,10 +1,7 @@ import type { NodeId } from '../../r-bridge/lang-4.x/ast/model/processing/node-id'; -import { AbstractDomain, type AnyAbstractDomain, type ConcreteDomain } from './abstract-domain'; -import { Bottom, BottomSymbol, Top } from './lattice'; -import type { StateDomainLike } from './state-domain-like'; - -/** The type of the concrete state of the concrete domain of a state abstract domain that maps keys to a concrete value in the concrete domain */ -export type ConcreteState = ReadonlyMap>; +import { AbstractDomain, type AnyAbstractDomain } from './abstract-domain'; +import { Bottom } from './lattice'; +import type { StateDomain } from './state-domain-like'; /** The type of the actual values of the state abstract domain as map of keys to domain values */ export type StateDomainValue = ReadonlyMap; @@ -22,8 +19,8 @@ export type StateDomainLift = StateDomainValue * @see {@link NodeId} for the node IDs of the AST nodes */ export class StateAbstractDomain = StateDomainLift> - extends AbstractDomain, StateDomainValue, StateDomainTop, StateDomainBottom, Value> - implements StateDomainLike { + extends AbstractDomain, StateDomainTop, StateDomainBottom, Value> + implements StateDomain { public readonly domain: Domain; @@ -36,9 +33,8 @@ export class StateAbstractDomain): this; - public create(value: StateDomainLift): StateAbstractDomain { - return new StateAbstractDomain(value, this.domain); + public create(value: StateDomainLift): this { + return new StateAbstractDomain(value, this.domain) as this; } public static top>(this: new (value: StateDomainTop, domain: Domain) => StateDomain, domain: Domain): StateDomain { @@ -77,189 +73,96 @@ export class StateAbstractDomain; } - public equals(other: this): boolean { - if(this.value === other.value) { - return true; - } else if(this.value === Bottom || other.value === Bottom || this.value.size !== other.value.size) { + protected equalsValue(this: StateAbstractDomain>, other: StateAbstractDomain>): boolean { + if(this.value.size !== other.value.size) { return false; } - - for(const [key, value] of this.value.entries()) { + for(const [key, currValue] of this.value.entries()) { const otherValue = other.get(key); - if(otherValue === undefined || !value.equals(otherValue)) { + if(otherValue === undefined || !currValue.equals(otherValue)) { return false; } } return true; } - public leq(other: this): boolean { - if(this.value === other.value || this.value === Bottom) { - return true; - } else if(other.value === Bottom || this.value.size > other.value.size) { + protected leqValue(this: StateAbstractDomain>, other: StateAbstractDomain>): boolean { + if(this.value.size > other.value.size) { return false; } - for(const [key, value] of this.value.entries()) { + for(const [key, currValue] of this.value.entries()) { const otherValue = other.get(key); - if(otherValue === undefined || !value.leq(otherValue)) { + if(otherValue === undefined || !currValue.leq(otherValue)) { return false; } } return true; } - public join(other: this): this { - if(this.value === Bottom){ - return this.create(other.value); - } else if(other.value === Bottom) { - return this.create(this.value); - } - const result = this.create(this.value) as this & StateAbstractDomain>; + protected joinValue(this: this & StateAbstractDomain>, other: StateAbstractDomain>): this { + const result = new Map(this.value); - for(const [key, value] of other.value.entries()) { + for(const [key, otherValue] of other.value.entries()) { const currValue = result.get(key); if(currValue === undefined) { - result.set(key, value); + result.set(key, otherValue); } else { - result.set(key, currValue.join(value)); + result.set(key, currValue.join(otherValue)); } } - return result; + return this.create(result); } - public meet(other: this): this { - if(this.value === Bottom || other.value === Bottom) { - return this.bottom(); - } - const result = this.create(this.value) as this & StateAbstractDomain>; + protected meetValue(this: this & StateAbstractDomain>, other: StateAbstractDomain>): this { + const result = new Map(); - for(const key of result.value.keys()) { - if(!other.has(key)) { - result.remove(key); - } - } - for(const [key, value] of other.value.entries()) { - const currValue = result.get(key); + for(const [key, currValue] of this.value.entries()) { + const otherValue = other.value.get(key); - if(currValue !== undefined) { - result.set(key, currValue.meet(value)); + if(otherValue !== undefined) { + result.set(key, currValue.meet(otherValue)); } } - return result; + return this.create(result); } - public widen(other: this): this { - if(this.value === Bottom){ - return this.create(other.value); - } else if(other.value === Bottom) { - return this.create(this.value); - } - const result = this.create(this.value) as this & StateAbstractDomain>; + protected widenValue(this: this & StateAbstractDomain>, other: StateAbstractDomain>): this { + const result = new Map(this.value); - for(const [key, value] of other.value.entries()) { + for(const [key, otherValue] of other.value.entries()) { const currValue = result.get(key); if(currValue === undefined) { - result.set(key, value); + result.set(key, otherValue); } else { - result.set(key, currValue.widen(value)); + result.set(key, currValue.widen(otherValue)); } } - return result; - } - - public narrow(other: this): this { - if(this.value === Bottom || other.value === Bottom) { - return this.bottom(); - } - const result = this.create(this.value) as this & StateAbstractDomain>; - - for(const key of result.value.keys()) { - if(!other.has(key)) { - result.remove(key); - } - } - for(const [key, value] of other.value.entries()) { - const currValue = result.get(key); - - if(currValue !== undefined) { - result.set(key, currValue.narrow(value)); - } - } - return result; - } - - public concretize(limit: number): ReadonlySet> | typeof Top { - if(this.value === Bottom) { - return new Set(); - } - let mappings = new Set>([new Map()]); - - for(const [key, value] of this.value.entries()) { - const concreteValues = value.concretize(limit); - - if(concreteValues === Top) { - return Top; - } - const newMappings = new Set>(); - - for(const state of mappings) { - for(const concrete of concreteValues) { - if(newMappings.size > limit) { - return Top; - } - const map = new Map(state); - map.set(key, concrete as ConcreteDomain); - newMappings.add(map); - } - } - mappings = newMappings; - } - return mappings; + return this.create(result); } - public abstract(concrete: ReadonlySet> | typeof Top): this { - if(concrete === Top) { - return this.top(); - } else if(concrete.size === 0) { - return this.bottom(); - } - const mapping = new Map>>(); + protected narrowValue(this: this & StateAbstractDomain>, other: StateAbstractDomain>): this { + const result = new Map(); - for(const concreteMapping of concrete) { - for(const [key, value] of concreteMapping) { - const set = mapping.get(key); + for(const [key, currValue] of this.value.entries()) { + const otherValue = other.value.get(key); - if(set === undefined) { - mapping.set(key, new Set([value])); - } else { - set.add(value); - } + if(otherValue !== undefined) { + result.set(key, currValue.narrow(otherValue)); } } - const result = new Map(); - - for(const [key, values] of mapping) { - result.set(key, this.domain.abstract(values)); - } return this.create(result); } - public toJson(): unknown { - if(this.value === Bottom) { - return this.value.description; - } + protected jsonify(this: StateAbstractDomain>): unknown { return Object.fromEntries(this.value.entries().map(([key, value]) => [key, value.toJson()])); } - public toString(): string { - if(this.value === Bottom) { - return BottomSymbol; - } - return '(' + this.value.entries().toArray().map(([key, value]) => `${AbstractDomain.toString(key)} -> ${value.toString()}`).join(', ') + ')'; + protected stringify(this: StateAbstractDomain>): string { + return '(' + this.value.entries().toArray().map(([key, value]) => `${key} -> ${value.toString()}`).join(', ') + ')'; } public isTop(): this is this & StateAbstractDomain { diff --git a/src/abstract-interpretation/domains/state-domain-like.ts b/src/abstract-interpretation/domains/state-domain-like.ts index 0c42d329025..3bbeebd7fd8 100644 --- a/src/abstract-interpretation/domains/state-domain-like.ts +++ b/src/abstract-interpretation/domains/state-domain-like.ts @@ -4,7 +4,7 @@ import { type AnyAbstractDomain } from './abstract-domain'; /** * An interface for state-like domains that store abstract values for AST nodes. */ -export interface StateDomainLike { +export interface StateDomain { /** * The underlying value domain of the state domain. */ @@ -34,7 +34,7 @@ export interface StateDomainLike { /** * A type representing any state abstract domain that stores abstract values for AST nodes. */ -export type AnyStateDomain = AnyAbstractDomain & StateDomainLike; +export type AnyStateDomain = AnyAbstractDomain & StateDomain; /** * The type of the value abstract domain of a state abstract domain. diff --git a/src/abstract-interpretation/domains/value-abstract-domain.ts b/src/abstract-interpretation/domains/value-abstract-domain.ts new file mode 100644 index 00000000000..18427436303 --- /dev/null +++ b/src/abstract-interpretation/domains/value-abstract-domain.ts @@ -0,0 +1,140 @@ +import type { Ternary } from '../../util/logic'; + +/** + * A value abstract domain with abstraction function and a satisfiability check for concrete values. + */ +export interface ValueDomain { + /** + * Abstracts a list of concrete values into an abstract value of the value abstract domain. + */ + from(...values: T[]): this; + + /** + * Checks whether the current abstract value satisfies a concrete value (i.e. includes a concrete value). + * @see {@link Ternary} for the returned satisfiability result + */ + satisfies(value: T): Ternary; +} + +/** + * A string value abstract domain with string operations and a satisfiability check. + */ +export interface StringDomain extends ValueDomain { + /** + * Concatenates this string abstract value with another string abstract value. + */ + concat(other: this): this; + + satisfies(value: string, comparator?: StringComparator): Ternary; +} + +/** + * A numeric value abstract domain with numeric operations and a satisfiability check. + */ +export interface NumericDomain extends ValueDomain { + /** + * Negates this numeric abstract value. + */ + negate(): this; + + /** + * Adds an numeric abstract value to this numeric abstract value. + */ + add(other: this): this; + + /** + * Subtracts an numeric abstract value from this numeric abstract value. + */ + subtract(other: this): this; + + /** + * Multiplies this numeric abstract value with another numeric abstract value. + */ + multiply(other: this): this; + + /** + * Divides this numeric abstract value by another numeric abstract value. + */ + divide(other: this): this; + + /** + * Gets the minimum of this numeric abstract value and another numeric abstract value. + */ + min(other: this): this; + + /** + * Gets the maximum of this numeric abstract value and another numeric abstract value. + */ + max(other: this): this; + + satisfies(value: number, comparator?: NumericalComparator): Ternary; +} + +export interface BooleanDomain extends ValueDomain { + /** + * Negates this boolean abstract value. + */ + negate(): this; + + /** + * Creates the conjunction between this boolean abstract value and another boolean abstract value. + */ + and(other: this): this; + + /** + * Creates the disjunction between this boolean abstract value and another boolean abstract value. + */ + or(other: this): this; +} + +/** + * A set value abstract domain with set operations and a satisfiability check. + */ +export interface SetDomain extends ValueDomain> { + /** + * Creates the union between this set abstract value and another set abstract value. + */ + union(other: this): this; + + /** + * Creates the intersection between this set abstract value and another set abstract value. + */ + intersect(other: this): this; + + /** + * Subtracts another set abstract value from this set abstract value creating the set difference. + */ + subtract(other: this): this; + + satisfies(value: ReadonlySet, comparator?: SetComparator): Ternary; +} + +/** + * Represents the different types of string comparators for satisfiability checks for an abstract domain. + */ +export enum StringComparator { + Equal, + StartsWith, + EndsWith, + Includes +} + +/** + * Represents the different types of numerical comparators for satisfiability checks for an abstract domain. + */ +export enum NumericalComparator { + Equal, + Less, + LessOrEqual, + Greater, + GreaterOrEqual +} + +/** + * Represents the different types of set comparators for satisfiability checks for an abstract domain. + */ +export enum SetComparator { + Equal, + Subset, + SubsetOrEqual +} diff --git a/src/benchmark/slicer.ts b/src/benchmark/slicer.ts index eaf3e196f29..fca53222a47 100644 --- a/src/benchmark/slicer.ts +++ b/src/benchmark/slicer.ts @@ -53,8 +53,7 @@ import { DataFrameShapeInferenceVisitor } from '../abstract-interpretation/data- import type { PosIntervalDomain } from '../abstract-interpretation/domains/positive-interval-domain'; import { SetRangeDomain } from '../abstract-interpretation/domains/set-range-domain'; import fs from 'fs'; -import type { FlowrAnalyzerContext } from '../project/context/flowr-analyzer-context'; -import { contextFromInput } from '../project/context/flowr-analyzer-context'; +import { type FlowrAnalyzerContext, contextFromInput } from '../project/context/flowr-analyzer-context'; import { RProject } from '../r-bridge/lang-4.x/ast/model/nodes/r-project'; import { RComment } from '../r-bridge/lang-4.x/ast/model/nodes/r-comment'; import { CallGraph } from '../dataflow/graph/call-graph'; @@ -437,9 +436,9 @@ export class BenchmarkSlicer { private getInferredRange(value: SetRangeDomain | PosIntervalDomain): number { if(value.isValue()) { if(value instanceof SetRangeDomain) { - return value.isFinite() ? value.value.range.size : Infinity; + return value.isFinite() ? value.may.size : Infinity; } else { - return value.value[1] - value.value[0]; + return value.upper - value.lower; } } return 0; @@ -452,9 +451,9 @@ export class BenchmarkSlicer { if(!value.isFinite()) { return 'infinite'; } else if(value instanceof SetRangeDomain) { - return Math.floor(value.value.min.size + (value.value.range.size / 2)); + return Math.floor(value.value.must.size + (value.value.may.size / 2)); } else { - return Math.floor((value.value[0] + value.value[1]) / 2); + return Math.floor((value.lower + value.upper) / 2); } } return 'bottom'; diff --git a/src/documentation/wiki-absint.ts b/src/documentation/wiki-absint.ts index 8663e9a08d7..082c1eaee47 100644 --- a/src/documentation/wiki-absint.ts +++ b/src/documentation/wiki-absint.ts @@ -133,9 +133,6 @@ In _flowR_, an abstract domain is represented by the class ${ctx.link(AbstractDo * ${ctx.linkM(AbstractDomain, 'widen')} to perform widening with another abstract value to ensure termination of the fixpoint iteration * ${ctx.linkM(AbstractDomain, 'narrow')} to perform narrowing with another abstract value to refine the abstract value after widening - - ${ctx.linkM(AbstractDomain, 'concretize')} representing the concretization function of the abstract domain - - ${ctx.linkM(AbstractDomain, 'abstract')} representing the abstraction function of the abstract domain - ${details('Class Diagram', ` All boxes link to their respective implementation in the source code. ${codeBlock('mermaid', ctx.mermaid(AbstractDomain))} @@ -154,7 +151,7 @@ ${codeBlock('mermaid', ctx.mermaid(AbstractDomain, { simplify: true, reverse: tr Multiple abstract domains can be combined using a ${ctx.link(MultiValueDomain)} (for example, to use an interval domain for numbers and bounded set domain for strings at the same time). A multi-value state domain (${ctx.link(MultiValueStateDomain)}) as state domain of a multi-value domain can be used to track the state of multiple value domains in a program. Additionally, is enables to define reductions on the multi-value domain to refine the inferred value for a value domain based on the other value domains in the multi-value domain. For example, the following example shows how a multi-value state domain can be defined to track numbers and strings at the same time with a simple reduction that sets both domains to bottom if one domain is bottom. -${ctx.code(multiValueExample, { dropLinesStart: 1, dropLinesEnd: 1 })} +${ctx.code(multiValueExample, { dropLinesStart: 1, dropLinesEnd: 1, hideDefinedAt: true })} ${section('Abstract Interpretation', 2, 'abstract-interpretation')} diff --git a/src/linter/rules/dataframe-access-validation.ts b/src/linter/rules/dataframe-access-validation.ts index 33094e643e7..7373a1d9e33 100644 --- a/src/linter/rules/dataframe-access-validation.ts +++ b/src/linter/rules/dataframe-access-validation.ts @@ -1,6 +1,6 @@ import type { DataFrameDomain } from '../../abstract-interpretation/data-frame/dataframe-domain'; import { DataFrameShapeInferenceVisitor, type DataFrameOperationType } from '../../abstract-interpretation/data-frame/shape-inference'; -import { NumericalComparator, SetComparator } from '../../abstract-interpretation/domains/satisfiable-domain'; +import { NumericalComparator, SetComparator } from '../../abstract-interpretation/domains/value-abstract-domain'; import { FlowrConfig } from '../../config'; import { Identifier } from '../../dataflow/environments/identifier'; import { CfgKind } from '../../project/cfg-kind'; diff --git a/test/functionality/abstract-interpretation/data-frame/data-frame.ts b/test/functionality/abstract-interpretation/data-frame/data-frame.ts index cea42f0a90e..8dbbf0e56fe 100644 --- a/test/functionality/abstract-interpretation/data-frame/data-frame.ts +++ b/test/functionality/abstract-interpretation/data-frame/data-frame.ts @@ -4,8 +4,8 @@ import { type AbstractDataFrameShape, DataFrameDomain } from '../../../../src/ab import type { DataFrameOperationArgs, DataFrameOperationName } from '../../../../src/abstract-interpretation/data-frame/semantics'; import { type DataFrameOperations, DataFrameShapeInferenceVisitor } from '../../../../src/abstract-interpretation/data-frame/shape-inference'; import type { AbstractValue } from '../../../../src/abstract-interpretation/domains/abstract-domain'; -import { IntervalDomain } from '../../../../src/abstract-interpretation/domains/interval-domain'; import { Bottom, type Top } from '../../../../src/abstract-interpretation/domains/lattice'; +import { PosIntervalDomain } from '../../../../src/abstract-interpretation/domains/positive-interval-domain'; import { SetRangeDomain } from '../../../../src/abstract-interpretation/domains/set-range-domain'; import { FlowrConfig } from '../../../../src/config'; import { RoleInParent } from '../../../../src/r-bridge/lang-4.x/ast/model/processing/role'; @@ -21,7 +21,7 @@ import { type InferenceTestCase, type InferenceTestOptions, runInference, testIn * The expected data frame shape for data frame shape tests. */ export interface ExpectedDataFrameShape { - colnames: [min: string[], range: string[] | typeof Top] | typeof Bottom, + colnames: [must: string[], may: string[] | typeof Top] | typeof Bottom, cols: AbstractValue, rows: AbstractValue } @@ -126,9 +126,9 @@ function toDataFrameDomain(shape: ExpectedDataFrameShape | undefined, config?: F const maxColNames = config?.abstractInterpretation.dataFrame.maxColNames ?? FlowrConfig.default().abstractInterpretation.dataFrame.maxColNames; return new DataFrameDomain({ - colnames: new SetRangeDomain(shape.colnames === Bottom ? Bottom : { min: shape.colnames[0], range: shape.colnames[1] }, maxColNames), - cols: new IntervalDomain(shape.cols), - rows: new IntervalDomain(shape.rows) + colnames: new SetRangeDomain(shape.colnames === Bottom ? Bottom : { must: shape.colnames[0], may: shape.colnames[1] }, maxColNames), + cols: new PosIntervalDomain(shape.cols), + rows: new PosIntervalDomain(shape.rows) }); } diff --git a/test/functionality/abstract-interpretation/data-frame/dataframe-domain.test.ts b/test/functionality/abstract-interpretation/data-frame/dataframe-domain.test.ts index 134f028e48b..cc7956dc021 100644 --- a/test/functionality/abstract-interpretation/data-frame/dataframe-domain.test.ts +++ b/test/functionality/abstract-interpretation/data-frame/dataframe-domain.test.ts @@ -10,7 +10,7 @@ import type { ExpectedDataFrameShape } from './data-frame'; describe('Data Frame Domains', () => { const createDomain = ({ colnames, cols, rows }: ExpectedDataFrameShape) => new DataFrameDomain({ - colnames: new SetRangeDomain(colnames === Bottom ? colnames : { min: colnames[0], range: colnames[1] === Top ? Top : colnames[1] }), + colnames: new SetRangeDomain(colnames === Bottom ? colnames : { must: colnames[0], may: colnames[1] === Top ? Top : colnames[1] }), cols: new PosIntervalDomain(cols), rows: new PosIntervalDomain(rows) }); @@ -66,37 +66,37 @@ describe('Data Frame Domains', () => { equal: false, leq: true, join: { ...domain1, colnames: [[], Top] }, meet: domain1, widen: { ...domain1, colnames: [[], Top] }, narrow: domain1 }); assertAbstractDomain(create, { ...domain1, colnames: [[], Top] }, domain1, { - equal: false, leq: false, join: { ...domain1, colnames: [[], Top] }, meet: domain1, widen: { ...domain1, colnames: [[], Top] }, narrow: domain1, abstract: DataFrameTop + equal: false, leq: false, join: { ...domain1, colnames: [[], Top] }, meet: domain1, widen: { ...domain1, colnames: [[], Top] }, narrow: domain1 }); assertAbstractDomain(create, domain1, { ...domain1, colnames: [domain1.colnames[0], Top], cols: [2, +Infinity] }, { equal: false, leq: true, join: { ...domain1, colnames: [domain1.colnames[0], Top], cols: [2, +Infinity] }, meet: domain1, widen: { ...domain1, colnames: [domain1.colnames[0], Top], cols: [2, +Infinity] }, narrow: domain1 }); assertAbstractDomain(create, { ...domain1, colnames: [domain1.colnames[0], Top], cols: [2, +Infinity] }, domain1, { - equal: false, leq: false, join: { ...domain1, colnames: [domain1.colnames[0], Top], cols: [2, +Infinity] }, meet: domain1, widen: { ...domain1, colnames: [domain1.colnames[0], Top], cols: [2, +Infinity] }, narrow: domain1, abstract: DataFrameTop + equal: false, leq: false, join: { ...domain1, colnames: [domain1.colnames[0], Top], cols: [2, +Infinity] }, meet: domain1, widen: { ...domain1, colnames: [domain1.colnames[0], Top], cols: [2, +Infinity] }, narrow: domain1 }); assertAbstractDomain(create, domain1, { ...domain1, rows: PosIntervalTop }, { equal: false, leq: true, join: { ...domain1, rows: PosIntervalTop }, meet: domain1, widen: { ...domain1, rows: PosIntervalTop }, narrow: domain1 }); assertAbstractDomain(create, { ...domain1, rows: PosIntervalTop }, domain1, { - equal: false, leq: false, join: { ...domain1, rows: PosIntervalTop }, meet: domain1, widen: { ...domain1, rows: PosIntervalTop }, narrow: domain1, abstract: DataFrameTop + equal: false, leq: false, join: { ...domain1, rows: PosIntervalTop }, meet: domain1, widen: { ...domain1, rows: PosIntervalTop }, narrow: domain1 }); assertAbstractDomain(create, domain1, { ...domain1, colnames: Bottom }, { equal: false, leq: false, join: domain1, meet: { ...domain1, colnames: Bottom }, widen: domain1, narrow: { ...domain1, colnames: Bottom } }); assertAbstractDomain(create, { ...domain1, colnames: Bottom }, domain1, { - equal: false, leq: true, join: domain1, meet: { ...domain1, colnames: Bottom }, widen: domain1, narrow: { ...domain1, colnames: Bottom }, abstract: DataFrameBottom + equal: false, leq: true, join: domain1, meet: { ...domain1, colnames: Bottom }, widen: domain1, narrow: { ...domain1, colnames: Bottom } }); assertAbstractDomain(create, domain1, { ...domain1, cols: Bottom }, { equal: false, leq: false, join: domain1, meet: { ...domain1, cols: Bottom }, widen: domain1, narrow: { ...domain1, cols: Bottom } }); assertAbstractDomain(create, { ...domain1, cols: Bottom }, domain1, { - equal: false, leq: true, join: domain1, meet: { ...domain1, cols: Bottom }, widen: domain1, narrow: { ...domain1, cols: Bottom }, abstract: DataFrameBottom + equal: false, leq: true, join: domain1, meet: { ...domain1, cols: Bottom }, widen: domain1, narrow: { ...domain1, cols: Bottom } }); assertAbstractDomain(create, domain1, { ...domain1, rows: Bottom }, { equal: false, leq: false, join: domain1, meet: { ...domain1, rows: Bottom }, widen: domain1, narrow: { ...domain1, rows: Bottom } }); assertAbstractDomain(create, { ...domain1, rows: Bottom }, domain1, { - equal: false, leq: true, join: domain1, meet: { ...domain1, rows: Bottom }, widen: domain1, narrow: { ...domain1, rows: Bottom }, abstract: DataFrameBottom + equal: false, leq: true, join: domain1, meet: { ...domain1, rows: Bottom }, widen: domain1, narrow: { ...domain1, rows: Bottom } }); assertAbstractDomain(create, domain1, domain2, { equal: false, leq: false, join: join, meet: meet, widen: widen1, narrow: narrow1 @@ -116,25 +116,25 @@ describe('Data Frame Domains', () => { const create = createState; assertAbstractDomain(create, [[0, DataFrameBottom]], [[0, DataFrameBottom]], { - equal: true, leq: true, join: [[0, DataFrameBottom]], meet: [[0, DataFrameBottom]], widen: [[0, DataFrameBottom]], narrow: [[0, DataFrameBottom]], abstract: Bottom + equal: true, leq: true, join: [[0, DataFrameBottom]], meet: [[0, DataFrameBottom]], widen: [[0, DataFrameBottom]], narrow: [[0, DataFrameBottom]] }); assertAbstractDomain(create, [[0, DataFrameTop]], [[0, DataFrameTop]], { - equal: true, leq: true, join: [[0, DataFrameTop]], meet: [[0, DataFrameTop]], widen: [[0, DataFrameTop]], narrow: [[0, DataFrameTop]], abstract: [] + equal: true, leq: true, join: [[0, DataFrameTop]], meet: [[0, DataFrameTop]], widen: [[0, DataFrameTop]], narrow: [[0, DataFrameTop]] }); assertAbstractDomain(create, [[0, DataFrameBottom]], [[0, DataFrameTop]], { - equal: false, leq: true, join: [[0, DataFrameTop]], meet: [[0, DataFrameBottom]], widen: [[0, DataFrameTop]], narrow: [[0, DataFrameBottom]], abstract: Bottom + equal: false, leq: true, join: [[0, DataFrameTop]], meet: [[0, DataFrameBottom]], widen: [[0, DataFrameTop]], narrow: [[0, DataFrameBottom]] }); assertAbstractDomain(create, [[0, DataFrameTop]], [[0, DataFrameBottom]], { - equal: false, leq: false, join: [[0, DataFrameTop]], meet: [[0, DataFrameBottom]], widen: [[0, DataFrameTop]], narrow: [[0, DataFrameBottom]], abstract: [] + equal: false, leq: false, join: [[0, DataFrameTop]], meet: [[0, DataFrameBottom]], widen: [[0, DataFrameTop]], narrow: [[0, DataFrameBottom]] }); assertAbstractDomain(create, [[0, DataFrameBottom]], [[0, DataFrameEmpty]], { - equal: false, leq: true, join: [[0, DataFrameEmpty]], meet: [[0, DataFrameBottom]], widen: [[0, DataFrameEmpty]], narrow: [[0, DataFrameBottom]], abstract: Bottom + equal: false, leq: true, join: [[0, DataFrameEmpty]], meet: [[0, DataFrameBottom]], widen: [[0, DataFrameEmpty]], narrow: [[0, DataFrameBottom]] }); assertAbstractDomain(create, [[0, DataFrameEmpty]], [[0, DataFrameBottom]], { equal: false, leq: false, join: [[0, DataFrameEmpty]], meet: [[0, DataFrameBottom]], widen: [[0, DataFrameEmpty]], narrow: [[0, DataFrameBottom]] }); assertAbstractDomain(create, [[0, DataFrameBottom]], [[0, domain1]], { - equal: false, leq: true, join: [[0, domain1]], meet: [[0, DataFrameBottom]], widen: [[0, domain1]], narrow: [[0, DataFrameBottom]], abstract: Bottom + equal: false, leq: true, join: [[0, domain1]], meet: [[0, DataFrameBottom]], widen: [[0, domain1]], narrow: [[0, DataFrameBottom]] }); assertAbstractDomain(create, [[0, domain1]], [[0, DataFrameBottom]], { equal: false, leq: false, join: [[0, domain1]], meet: [[0, DataFrameBottom]], widen: [[0, domain1]], narrow: [[0, DataFrameBottom]] @@ -149,31 +149,31 @@ describe('Data Frame Domains', () => { equal: false, leq: false, join: [[0, join]], meet: [[0, meet]], widen: [[0, widen2]], narrow: [[0, narrow2]] }); assertAbstractDomain(create, [[0, domain1], [1, domain2]], [[0, domain1], [1, domain2]], { - equal: true, leq: true, join: [[0, domain1], [1, domain2]], meet: [[0, domain1], [1, domain2]], widen: [[0, domain1], [1, domain2]], narrow: [[0, domain1], [1, domain2]], abstract: [] + equal: true, leq: true, join: [[0, domain1], [1, domain2]], meet: [[0, domain1], [1, domain2]], widen: [[0, domain1], [1, domain2]], narrow: [[0, domain1], [1, domain2]] }); assertAbstractDomain(create, [[0, domain1], [1, domain1]], [[0, domain1], [1, domain2]], { equal: false, leq: false, join: [[0, domain1], [1, join]], meet: [[0, domain1], [1, meet]], widen: [[0, domain1], [1, widen1]], narrow: [[0, domain1], [1, narrow1]] }); assertAbstractDomain(create, [[1, DataFrameTop]], [[0, domain1], [1, domain2]], { - equal: false, leq: false, join: [[0, domain1], [1, DataFrameTop]], meet: [[1, domain2]], widen: [[0, domain1], [1, DataFrameTop]], narrow: [[1, domain2]], abstract: [] + equal: false, leq: false, join: [[0, domain1], [1, DataFrameTop]], meet: [[1, domain2]], widen: [[0, domain1], [1, DataFrameTop]], narrow: [[1, domain2]] }); assertAbstractDomain(create, [[0, domain1], [1, domain2]], [[1, DataFrameTop]], { - equal: false, leq: false, join: [[0, domain1], [1, DataFrameTop]], meet: [[1, domain2]], widen: [[0, domain1], [1, DataFrameTop]], narrow: [[1, domain2]], abstract: [] + equal: false, leq: false, join: [[0, domain1], [1, DataFrameTop]], meet: [[1, domain2]], widen: [[0, domain1], [1, DataFrameTop]], narrow: [[1, domain2]] }); assertAbstractDomain(create, [[0, domain1], [1, domain2]], [[0, DataFrameTop], [1, domain2]], { - equal: false, leq: true, join: [[0, DataFrameTop], [1, domain2]], meet: [[0, domain1], [1, domain2]], widen: [[0, DataFrameTop], [1, domain2]], narrow: [[0, domain1], [1, domain2]], abstract: [] + equal: false, leq: true, join: [[0, DataFrameTop], [1, domain2]], meet: [[0, domain1], [1, domain2]], widen: [[0, DataFrameTop], [1, domain2]], narrow: [[0, domain1], [1, domain2]] }); assertAbstractDomain(create, [[0, DataFrameTop], [1, domain2]], [[0, domain1], [1, domain2]], { - equal: false, leq: false, join: [[0, DataFrameTop], [1, domain2]], meet: [[0, domain1], [1, domain2]], widen: [[0, DataFrameTop], [1, domain2]], narrow: [[0, domain1], [1, domain2]], abstract: [] + equal: false, leq: false, join: [[0, DataFrameTop], [1, domain2]], meet: [[0, domain1], [1, domain2]], widen: [[0, DataFrameTop], [1, domain2]], narrow: [[0, domain1], [1, domain2]] }); assertAbstractDomain(create, [[0, domain1], [2, DataFrameBottom]], [[1, DataFrameTop]], { - equal: false, leq: true, join: [[1, DataFrameTop]], meet: Bottom, widen: [[1, DataFrameTop]], narrow: Bottom, abstract: Bottom + equal: false, leq: true, join: [[1, DataFrameTop]], meet: Bottom, widen: [[1, DataFrameTop]], narrow: Bottom }); assertAbstractDomain(create, [[1, DataFrameTop]], [[0, domain1], [2, DataFrameBottom]], { - equal: false, leq: false, join: [[1, DataFrameTop]], meet: Bottom, widen: [[1, DataFrameTop]], narrow: Bottom, abstract: [] + equal: false, leq: false, join: [[1, DataFrameTop]], meet: Bottom, widen: [[1, DataFrameTop]], narrow: Bottom }); assertAbstractDomain(create, [[0, DataFrameTop]], [[0, domain1]], { - equal: false, leq: false, join: [[0, DataFrameTop]], meet: [[0, domain1]], widen: [[0, DataFrameTop]], narrow: [[0, domain1]], abstract: [] + equal: false, leq: false, join: [[0, DataFrameTop]], meet: [[0, domain1]], widen: [[0, DataFrameTop]], narrow: [[0, domain1]] }); assertAbstractDomain(create, [[0, domain1]], [[0, DataFrameTop]], { equal: false, leq: true, join: [[0, DataFrameTop]], meet: [[0, domain1]], widen: [[0, DataFrameTop]], narrow: [[0, domain1]] diff --git a/test/functionality/abstract-interpretation/data-frame/inference.test.ts b/test/functionality/abstract-interpretation/data-frame/inference.test.ts index 8c0960522ba..4af319a08fd 100644 --- a/test/functionality/abstract-interpretation/data-frame/inference.test.ts +++ b/test/functionality/abstract-interpretation/data-frame/inference.test.ts @@ -364,9 +364,11 @@ print(df) shell, ` if (2 < 1) { - df <- data.frame(id = 1:5) + df1 <- data.frame(id = 1:5) +} else { + df2 <- data.frame(id = 1:5) } -print(df) +print(df1) `, ['4@df'] ); @@ -888,7 +890,7 @@ result <- df[1, c("id", "name")] df <- data.frame(id = 1:3, name = 4:6) result <- df[1, c(1, 2)] `, - { '2@result': { colnames: [[], ['id', 'name']], cols: [2, 2], rows: [1, 1] } } + { '2@result': { colnames: [['id', 'name'], []], cols: [2, 2], rows: [1, 1] } } ); testInferredDataFrameShape( @@ -897,7 +899,7 @@ result <- df[1, c(1, 2)] df <- data.frame(id = 1:3, name = 4:6) result <- df[1:2, c(1, 2)] `, - { '2@result': { colnames: [[], ['id', 'name']], cols: [2, 2], rows: [2, 2] } } + { '2@result': { colnames: [['id', 'name'], []], cols: [2, 2], rows: [2, 2] } } ); testInferredDataFrameShape( @@ -906,7 +908,7 @@ result <- df[1:2, c(1, 2)] df <- data.frame(id = 1:3, name = 4:6) result <- df[, 1:2] `, - { '2@result': { colnames: [[], ['id', 'name']], cols: [2, 2], rows: [3, 3] } } + { '2@result': { colnames: [['id', 'name'], []], cols: [2, 2], rows: [3, 3] } } ); testInferredDataFrameShape( @@ -5346,7 +5348,7 @@ df <- df[2:3, 1:2] '1@df': { colnames: [['id', 'age'], []], cols: [2, 2], rows: [3, 3] }, '2@df': { colnames: [['id', 'age'], []], cols: [2, 2], rows: [0, 3] }, '3@df': { colnames: [['id', 'age'], []], cols: [2, 2], rows: [2, 5] }, - '4@df': { colnames: [[], ['id', 'age']], cols: [2, 2], rows: [2, 2] }, + '4@df': { colnames: [['id', 'age'], []], cols: [2, 2], rows: [2, 2] }, }, { minRVersion: MIN_VERSION_PIPE } ); diff --git a/test/functionality/abstract-interpretation/domains/domain.ts b/test/functionality/abstract-interpretation/domains/domain.ts index d0d47e8c7ce..3c79ab10614 100644 --- a/test/functionality/abstract-interpretation/domains/domain.ts +++ b/test/functionality/abstract-interpretation/domains/domain.ts @@ -1,19 +1,16 @@ import { assert, test } from 'vitest'; -import { AbstractDomain, DEFAULT_INFERENCE_LIMIT, type AnyAbstractDomain, type ConcreteDomain } from '../../../../src/abstract-interpretation/domains/abstract-domain'; -import { Top } from '../../../../src/abstract-interpretation/domains/lattice'; +import { type AnyAbstractDomain } from '../../../../src/abstract-interpretation/domains/abstract-domain'; /** * The type of an object containing the expected results for the operations on abstract values of an abstract domain. */ -export interface DomainTestExpectation{ - readonly equal: boolean, - readonly leq: boolean, - readonly join: AbstractValue, - readonly meet: AbstractValue, - readonly widen: AbstractValue, - readonly narrow: AbstractValue, - readonly concrete?: ConcreteValue[] | typeof Top, - readonly abstract?: AbstractValue +export interface DomainTestExpectation{ + readonly equal: boolean, + readonly leq: boolean, + readonly join: AbstractValue, + readonly meet: AbstractValue, + readonly widen: AbstractValue, + readonly narrow?: AbstractValue } /** @@ -29,16 +26,10 @@ export function assertAbstractDomain Domain, value1: AbstractValue, value2: AbstractValue, - expected: DomainTestExpectation> + expected: DomainTestExpectation ) { const domain1 = create(value1); const domain2 = create(value2); - const join = create(expected.join); - const meet = create(expected.meet); - const widen = create(expected.widen); - const narrow = create(expected.narrow); - const concrete = expected.concrete === Top ? Top : new Set(expected.concrete); - const abstract = create(expected.abstract ?? value1); test(`${domain1.toString()} = ${domain2.toString()}`, () => { assert.strictEqual(domain1.equals(domain2), expected.equal, `Expected ${domain1.toString()} to ${expected.equal ? '' : 'not '}equal ${domain2.toString()}`); @@ -48,36 +39,34 @@ export function assertAbstractDomain { assert.isTrue(domain1.join(domain2).equals(join), `Expected ${join.toString()} but was ${domain1.join(domain2).toString()}`); assert.isTrue(domain2.join(domain1).equals(join), `Expected ${join.toString()} but was ${domain2.join(domain1).toString()}`); assert.isTrue(domain1.leq(domain1.join(domain2)), `Expected ${domain1.toString()} to be less than or equal to join ${domain1.join(domain2).toString()}`); assert.isTrue(domain2.leq(domain1.join(domain2)), `Expected ${domain2.toString()} to be less than or equal to join ${domain1.join(domain2).toString()}`); }); + const meet = create(expected.meet); test(`${domain1.toString()} ⊓ ${domain2.toString()}`, () => { assert.isTrue(domain1.meet(domain2).equals(meet), `Expected ${meet.toString()} but was ${domain1.meet(domain2).toString()}`); assert.isTrue(domain2.meet(domain1).equals(meet), `Expected ${meet.toString()} but was ${domain2.meet(domain1).toString()}`); assert.isTrue(domain1.meet(domain2).leq(domain1), `Expected meet ${domain1.meet(domain2).toString()} to be less than or equal to ${domain1.toString()}`); assert.isTrue(domain1.meet(domain2).leq(domain2), `Expected meet ${domain1.meet(domain2).toString()} to be less than or equal to ${domain2.toString()}`); }); + const widen = create(expected.widen); test(`${domain1.toString()} ▽ ${domain2.toString()}`, () => { assert.isTrue(domain1.widen(domain2).equals(widen), `Expected ${widen.toString()} but was ${domain1.widen(domain2).toString()}`); assert.isTrue(domain1.join(domain2).leq(domain1.widen(domain2)), `Expected join ${domain1.join(domain2).toString()} to be less than or equal to widening ${domain1.widen(domain2).toString()}`); assert.isTrue(domain1.leq(domain1.widen(domain2)), `Expected ${domain1.toString()} to be less than or equal to widening ${domain1.widen(domain2).toString()}`); assert.isTrue(domain2.leq(domain1.widen(domain2)), `Expected ${domain2.toString()} to be less than or equal to widening ${domain1.widen(domain2).toString()}`); }); - test(`${domain1.toString()} △ ${domain2.toString()}`, () => { - assert.isTrue(domain1.narrow(domain2).equals(narrow), `Expected ${narrow.toString()} but was ${domain1.narrow(domain2).toString()}`); - assert.isTrue(domain1.meet(domain2).leq(domain1.narrow(domain2)), `Expected meet ${domain1.meet(domain2).toString()} to be less than or equal to narrowing ${domain1.narrow(domain2).toString()}`); - assert.isTrue(domain1.narrow(domain2).leq(domain1), `Expected narrowing ${domain1.narrow(domain2).toString()} to be less than or equal to ${domain1.toString()}`); - assert.isTrue(domain2.narrow(domain2).leq(domain2), `Expected narrowing ${domain1.narrow(domain2).toString()} to be less than or equal to ${domain2.toString()}`); - }); - if(expected.concrete) { - test(`γ(${domain1.toString()})`, () => { - assert.deepStrictEqual(domain1.concretize(DEFAULT_INFERENCE_LIMIT), concrete, `Expected ${AbstractDomain.toString(concrete)} but was ${AbstractDomain.toString(domain1.concretize(DEFAULT_INFERENCE_LIMIT))}`); + if(expected.narrow !== undefined) { + const narrow = create(expected.narrow); + test(`${domain1.toString()} △ ${domain2.toString()}`, () => { + assert.isTrue(domain1.narrow(domain2).equals(narrow), `Expected ${narrow.toString()} but was ${domain1.narrow(domain2).toString()}`); + assert.isTrue(domain1.meet(domain2).leq(domain1.narrow(domain2)), `Expected meet ${domain1.meet(domain2).toString()} to be less than or equal to narrowing ${domain1.narrow(domain2).toString()}`); + assert.isTrue(domain1.narrow(domain2).leq(domain1), `Expected narrowing ${domain1.narrow(domain2).toString()} to be less than or equal to ${domain1.toString()}`); + assert.isTrue(domain2.narrow(domain2).leq(domain2), `Expected narrowing ${domain1.narrow(domain2).toString()} to be less than or equal to ${domain2.toString()}`); }); } - test(`α(γ(${domain1.toString()}))`, () => { - assert.isTrue(domain1.abstract(domain1.concretize(DEFAULT_INFERENCE_LIMIT)).equals(abstract), `Expected ${abstract.toString()} but was ${domain1.abstract(domain1.concretize(DEFAULT_INFERENCE_LIMIT)).toString()}`); - }); } diff --git a/test/functionality/abstract-interpretation/domains/domains.test.ts b/test/functionality/abstract-interpretation/domains/domains.test.ts index e7a6325c35f..0da77a7ad54 100644 --- a/test/functionality/abstract-interpretation/domains/domains.test.ts +++ b/test/functionality/abstract-interpretation/domains/domains.test.ts @@ -1,9 +1,9 @@ import { describe } from 'vitest'; import type { AbstractValue, AnyAbstractDomain } from '../../../../src/abstract-interpretation/domains/abstract-domain'; import { BoundedSetDomain } from '../../../../src/abstract-interpretation/domains/bounded-set-domain'; -import { IntervalDomain, IntervalTop } from '../../../../src/abstract-interpretation/domains/interval-domain'; +import { type IntervalLift, IntervalDomain, IntervalTop } from '../../../../src/abstract-interpretation/domains/interval-domain'; import { Bottom, Top } from '../../../../src/abstract-interpretation/domains/lattice'; -import { PosIntervalDomain, PosIntervalTop } from '../../../../src/abstract-interpretation/domains/positive-interval-domain'; +import { type PosIntervalLift, PosIntervalDomain, PosIntervalTop } from '../../../../src/abstract-interpretation/domains/positive-interval-domain'; import { SetRangeDomain } from '../../../../src/abstract-interpretation/domains/set-range-domain'; import { SetUpperBoundDomain } from '../../../../src/abstract-interpretation/domains/set-upper-bound-domain'; import { SingletonDomain } from '../../../../src/abstract-interpretation/domains/singleton-domain'; @@ -14,188 +14,184 @@ describe('Abstract Domains', () => { const create = (value: AbstractValue>) => new SingletonDomain(value); assertAbstractDomain(create, Bottom, Bottom, { - equal: true, leq: true, join: Bottom, meet: Bottom, widen: Bottom, narrow: Bottom, concrete: [] + equal: true, leq: true, join: Bottom, meet: Bottom, widen: Bottom, narrow: Bottom }); assertAbstractDomain(create, Top, Top, { - equal: true, leq: true, join: Top, meet: Top, widen: Top, narrow: Top, concrete: Top + equal: true, leq: true, join: Top, meet: Top, widen: Top, narrow: Top }); assertAbstractDomain(create, Bottom, Top, { - equal: false, leq: true, join: Top, meet: Bottom, widen: Top, narrow: Bottom, concrete: [] + equal: false, leq: true, join: Top, meet: Bottom, widen: Top, narrow: Bottom }); assertAbstractDomain(create, Top, Bottom, { - equal: false, leq: false, join: Top, meet: Bottom, widen: Top, narrow: Bottom, concrete: Top + equal: false, leq: false, join: Top, meet: Bottom, widen: Top, narrow: Bottom }); assertAbstractDomain(create, Bottom, 42, { - equal: false, leq: true, join: 42, meet: Bottom, widen: 42, narrow: Bottom, concrete: [] + equal: false, leq: true, join: 42, meet: Bottom, widen: 42, narrow: Bottom }); assertAbstractDomain(create, 42, Bottom, { - equal: false, leq: false, join: 42, meet: Bottom, widen: 42, narrow: Bottom, concrete: [42] + equal: false, leq: false, join: 42, meet: Bottom, widen: 42, narrow: Bottom }); assertAbstractDomain(create, 42, 42, { - equal: true, leq: true, join: 42, meet: 42, widen: 42, narrow: 42, concrete: [42] + equal: true, leq: true, join: 42, meet: 42, widen: 42, narrow: 42 }); assertAbstractDomain(create, 12, 42, { - equal: false, leq: true, join: Top, meet: Bottom, widen: Top, narrow: Bottom, concrete: [12] + equal: false, leq: true, join: Top, meet: Bottom, widen: Top, narrow: Bottom }); assertAbstractDomain(create, 42, 12, { - equal: false, leq: false, join: Top, meet: Bottom, widen: Top, narrow: Bottom, concrete: [42] + equal: false, leq: false, join: Top, meet: Bottom, widen: Top, narrow: Bottom }); assertAbstractDomain(create, 42, Top, { - equal: false, leq: true, join: Top, meet: 42, widen: Top, narrow: 42, concrete: [42] + equal: false, leq: true, join: Top, meet: 42, widen: Top, narrow: 42 }); assertAbstractDomain(create, Top, 42, { - equal: false, leq: false, join: Top, meet: 42, widen: Top, narrow: 42, concrete: Top + equal: false, leq: false, join: Top, meet: 42, widen: Top, narrow: 42 }); }); const setTests = [{ - name: 'Bounded Set Domain', - create: (value: string[] | typeof Top) => new BoundedSetDomain(value) as AnyAbstractDomain, - concrete: (...values: string[]) => values + name: 'Bounded Set Domain', + create: (value: string[] | typeof Bottom | typeof Top) => new BoundedSetDomain(value === Bottom ? [] : value) as AnyAbstractDomain }, { - name: 'Set Upper Bound Domain', - create: (value: string[] | typeof Top) => new SetUpperBoundDomain(value) as AnyAbstractDomain, - concrete: (...values: string[]) => values.reduce((sets, value) => [...sets, ...sets.map(set => new Set([...set, value]))], [new Set()]) + name: 'Set Upper Bound Domain', + create: (value: string[] | typeof Bottom | typeof Top) => new SetUpperBoundDomain(value) as AnyAbstractDomain }]; - for(const { name, create, concrete } of setTests) { + for(const { name, create } of setTests) { describe(name, () => { - assertAbstractDomain(create, [], [], { - equal: true, leq: true, join: [], meet: [], widen: [], narrow: [], concrete: concrete() + assertAbstractDomain(create, Bottom, Bottom, { + equal: true, leq: true, join: Bottom, meet: Bottom, widen: Bottom, narrow: Bottom }); assertAbstractDomain(create, Top, Top, { - equal: true, leq: true, join: Top, meet: Top, widen: Top, narrow: Top, concrete: Top + equal: true, leq: true, join: Top, meet: Top, widen: Top, narrow: Top }); - assertAbstractDomain(create, [], Top, { - equal: false, leq: true, join: Top, meet: [], widen: Top, narrow: [], concrete: concrete() + assertAbstractDomain(create, Bottom, Top, { + equal: false, leq: true, join: Top, meet: Bottom, widen: Top, narrow: Bottom }); - assertAbstractDomain(create, Top, [], { - equal: false, leq: false, join: Top, meet: [], widen: Top, narrow: [], concrete: Top + assertAbstractDomain(create, Top, Bottom, { + equal: false, leq: false, join: Top, meet: Bottom, widen: Top, narrow: Bottom }); - assertAbstractDomain(create, [], ['id', 'age'], { - equal: false, leq: true, join: ['id', 'age'], meet: [], widen: Top, narrow: [], concrete: concrete() + assertAbstractDomain(create, Bottom, ['id', 'age'], { + equal: false, leq: true, join: ['id', 'age'], meet: Bottom, widen: ['id', 'age'], narrow: Bottom }); - assertAbstractDomain(create, ['id', 'age'], [], { - equal: false, leq: false, join: ['id', 'age'], meet: [], widen: ['id', 'age'], narrow: ['id', 'age'], concrete: concrete('id', 'age') + assertAbstractDomain(create, ['id', 'age'], Bottom, { + equal: false, leq: false, join: ['id', 'age'], meet: Bottom, widen: ['id', 'age'], narrow: Bottom }); assertAbstractDomain(create, ['id', 'age'], ['age', 'id'], { - equal: true, leq: true, join: ['id', 'age'], meet: ['id', 'age'], widen: ['id', 'age'], narrow: ['id', 'age'], concrete: concrete('id', 'age') + equal: true, leq: true, join: ['id', 'age'], meet: ['id', 'age'], widen: ['id', 'age'], narrow: ['id', 'age'] }); assertAbstractDomain(create, ['id', 'age'], ['id', 'age', 'score'], { - equal: false, leq: true, join: ['id', 'age', 'score'], meet: ['id', 'age'], widen: Top, narrow: ['id', 'age'], concrete: concrete('id', 'age') + equal: false, leq: true, join: ['id', 'age', 'score'], meet: ['id', 'age'], widen: Top, narrow: ['id', 'age'] }); assertAbstractDomain(create, ['id', 'age', 'score'], ['id', 'age'], { - equal: false, leq: false, join: ['id', 'age', 'score'], meet: ['id', 'age'], widen: ['id', 'age', 'score'], narrow: ['id', 'age', 'score'], concrete: concrete('id', 'age', 'score') + equal: false, leq: false, join: ['id', 'age', 'score'], meet: ['id', 'age'], widen: ['id', 'age', 'score'], narrow: ['id', 'age', 'score'] }); assertAbstractDomain(create, ['id', 'age', 'score'], ['id', 'category'], { - equal: false, leq: false, join: ['id', 'age', 'score', 'category'], meet: ['id'], widen: Top, narrow: ['id', 'age', 'score'], concrete: concrete('id', 'age', 'score') + equal: false, leq: false, join: ['id', 'age', 'score', 'category'], meet: ['id'], widen: Top, narrow: ['id', 'age', 'score'] }); assertAbstractDomain(create, ['id', 'category'], ['id', 'age', 'score'], { - equal: false, leq: false, join: ['id', 'age', 'score', 'category'], meet: ['id'], widen: Top, narrow: ['id', 'category'], concrete: concrete('id', 'category') + equal: false, leq: false, join: ['id', 'age', 'score', 'category'], meet: ['id'], widen: Top, narrow: ['id', 'category'] }); assertAbstractDomain(create, ['id', 'age'], Top, { - equal: false, leq: true, join: Top, meet: ['id', 'age'], widen: Top, narrow: ['id', 'age'], concrete: concrete('id', 'age') + equal: false, leq: true, join: Top, meet: ['id', 'age'], widen: Top, narrow: ['id', 'age'] }); assertAbstractDomain(create, Top, ['id', 'age'], { - equal: false, leq: false, join: Top, meet: ['id', 'age'], widen: Top, narrow: ['id', 'age'], concrete: Top + equal: false, leq: false, join: Top, meet: ['id', 'age'], widen: Top, narrow: ['id', 'age'] }); }); } describe('Set Range Domain', () => { - const create = (value: [min: string[], range: string[] | typeof Top] | typeof Bottom) => - new SetRangeDomain(value === Bottom ? value : { min: value[0], range: value[1] === Top ? Top : value[1] }); - - const concrete = (...lists: string[][]) => lists.map(list => new Set(list)); + const create = (value: [must: string[], may: string[] | typeof Top] | typeof Bottom) => + new SetRangeDomain(value === Bottom ? value : { must: value[0], may: value[1] === Top ? Top : value[1] }); assertAbstractDomain(create, Bottom, Bottom, { - equal: true, leq: true, join: Bottom, meet: Bottom, widen: Bottom, narrow: Bottom, concrete: [] + equal: true, leq: true, join: Bottom, meet: Bottom, widen: Bottom, narrow: Bottom }); assertAbstractDomain(create, [[], Top], [[], Top], { - equal: true, leq: true, join: [[], Top], meet: [[], Top], widen: [[], Top], narrow: [[], Top], concrete: Top + equal: true, leq: true, join: [[], Top], meet: [[], Top], widen: [[], Top], narrow: [[], Top] }); assertAbstractDomain(create, Bottom, [[], Top], { - equal: false, leq: true, join: [[], Top], meet: Bottom, widen: [[], Top], narrow: Bottom, concrete: [] + equal: false, leq: true, join: [[], Top], meet: Bottom, widen: [[], Top], narrow: Bottom }); assertAbstractDomain(create, [[], Top], Bottom, { - equal: false, leq: false, join: [[], Top], meet: Bottom, widen: [[], Top], narrow: Bottom, concrete: Top + equal: false, leq: false, join: [[], Top], meet: Bottom, widen: [[], Top], narrow: Bottom }); assertAbstractDomain(create, Bottom, [['id'], ['name', 'age']], { - equal: false, leq: true, join: [['id'], ['name', 'age']], meet: Bottom, widen: [['id'], ['name', 'age']], narrow: Bottom, concrete: [] + equal: false, leq: true, join: [['id'], ['name', 'age']], meet: Bottom, widen: [['id'], ['name', 'age']], narrow: Bottom }); assertAbstractDomain(create, [['id'], ['name', 'age']], Bottom, { - equal: false, leq: false, join: [['id'], ['name', 'age']], meet: Bottom, widen: [['id'], ['name', 'age']], narrow: Bottom, concrete: concrete(['id'], ['id', 'name'], ['id', 'age'], ['id', 'name', 'age']) + equal: false, leq: false, join: [['id'], ['name', 'age']], meet: Bottom, widen: [['id'], ['name', 'age']], narrow: Bottom }); assertAbstractDomain(create, [[], []], [['id'], ['name', 'age']], { - equal: false, leq: false, join: [[], ['id', 'name', 'age']], meet: Bottom, widen: [[], Top], narrow: Bottom, concrete: concrete([]) + equal: false, leq: false, join: [[], ['id', 'name', 'age']], meet: Bottom, widen: [[], Top], narrow: Bottom }); assertAbstractDomain(create, [['id'], ['name', 'age']], [[], []], { - equal: false, leq: false, join: [[], ['id', 'name', 'age']], meet: Bottom, widen: [[], ['id', 'name', 'age']], narrow: Bottom, concrete: concrete(['id'], ['id', 'name'], ['id', 'age'], ['id', 'name', 'age']) + equal: false, leq: false, join: [[], ['id', 'name', 'age']], meet: Bottom, widen: [[], ['id', 'name', 'age']], narrow: Bottom }); assertAbstractDomain(create, [[], ['id']], [['id'], ['name', 'age']], { - equal: false, leq: false, join: [[], ['id', 'name', 'age']], meet: [['id'], []], widen: [[], Top], narrow: [['id'], []], concrete: concrete([], ['id']) + equal: false, leq: false, join: [[], ['id', 'name', 'age']], meet: [['id'], []], widen: [[], Top], narrow: [['id'], []] }); assertAbstractDomain(create, [['id'], ['name', 'age']], [[], ['id']], { - equal: false, leq: false, join: [[], ['id', 'name', 'age']], meet: [['id'], []], widen: [[], ['id', 'name', 'age']], narrow: [['id'], ['name', 'age']], concrete: concrete(['id'], ['id', 'name'], ['id', 'age'], ['id', 'name', 'age']) + equal: false, leq: false, join: [[], ['id', 'name', 'age']], meet: [['id'], []], widen: [[], ['id', 'name', 'age']], narrow: [['id'], ['name', 'age']] }); assertAbstractDomain(create, [['id'], ['name']], [[], ['id', 'name', 'age']], { - equal: false, leq: true, join: [[], ['id', 'name', 'age']], meet: [['id'], ['name']], widen: [[], Top], narrow: [['id'], ['name']], concrete: concrete(['id'], ['id', 'name']) + equal: false, leq: true, join: [[], ['id', 'name', 'age']], meet: [['id'], ['name']], widen: [[], Top], narrow: [['id'], ['name']] }); assertAbstractDomain(create, [[], ['id', 'name', 'age']], [['id'], ['name']], { - equal: false, leq: false, join: [[], ['id', 'name', 'age']], meet: [['id'], ['name']], widen: [[], ['id', 'name', 'age']], narrow: [['id'], ['name', 'age']], concrete: concrete([], ['id'], ['name'], ['id', 'name'], ['age'], ['id', 'age'], ['name', 'age'], ['id', 'name', 'age']) + equal: false, leq: false, join: [[], ['id', 'name', 'age']], meet: [['id'], ['name']], widen: [[], ['id', 'name', 'age']], narrow: [['id'], ['name', 'age']] }); assertAbstractDomain(create, [[], ['score']], [['id'], ['name', 'age']], { - equal: false, leq: false, join: [[], ['id', 'name', 'age', 'score']], meet: Bottom, widen: [[], Top], narrow: Bottom, concrete: concrete([], ['score']) + equal: false, leq: false, join: [[], ['id', 'name', 'age', 'score']], meet: Bottom, widen: [[], Top], narrow: Bottom }); assertAbstractDomain(create, [['id'], ['name', 'age']], [[], ['score']], { - equal: false, leq: false, join: [[], ['id', 'name', 'age', 'score']], meet: Bottom, widen: [[], Top], narrow: Bottom, concrete: concrete(['id'], ['id', 'name'], ['id', 'age'], ['id', 'name', 'age']) + equal: false, leq: false, join: [[], ['id', 'name', 'age', 'score']], meet: Bottom, widen: [[], Top], narrow: Bottom }); assertAbstractDomain(create, [['id'], []], [['id'], ['name', 'age']], { - equal: false, leq: true, join: [['id'], ['name', 'age']], meet: [['id'], []], widen: [['id'], Top], narrow: [['id'], []], concrete: concrete(['id']) + equal: false, leq: true, join: [['id'], ['name', 'age']], meet: [['id'], []], widen: [['id'], Top], narrow: [['id'], []] }); assertAbstractDomain(create, [['id'], ['name', 'age']], [['id'], []], { - equal: false, leq: false, join: [['id'], ['name', 'age']], meet: [['id'], []], widen: [['id'], ['name', 'age']], narrow: [['id'], ['name', 'age']], concrete: concrete(['id'], ['id', 'name'], ['id', 'age'], ['id', 'name', 'age']) + equal: false, leq: false, join: [['id'], ['name', 'age']], meet: [['id'], []], widen: [['id'], ['name', 'age']], narrow: [['id'], ['name', 'age']] }); assertAbstractDomain(create, [['id'], ['name', 'age', 'score']], [['id', 'name'], ['age']], { - equal: false, leq: false, join: [['id'], ['name', 'age', 'score']], meet: [['id', 'name'], ['age']], widen: [['id'], ['name', 'age', 'score']], narrow: [['id'], ['name', 'age', 'score']], concrete: concrete(['id'], ['id', 'name'], ['id', 'age'], ['id', 'name', 'age'], ['id', 'score'], ['id', 'name', 'score'], ['id', 'age', 'score'], ['id', 'name', 'age', 'score']) + equal: false, leq: false, join: [['id'], ['name', 'age', 'score']], meet: [['id', 'name'], ['age']], widen: [['id'], ['name', 'age', 'score']], narrow: [['id'], ['name', 'age', 'score']] }); assertAbstractDomain(create, [['id', 'name'], ['age']], [['id'], ['name', 'age', 'score']], { - equal: false, leq: true, join: [['id'], ['name', 'age', 'score']], meet: [['id', 'name'], ['age']], widen: [[], Top], narrow: [['id', 'name'], ['age']], concrete: concrete(['id', 'name'], ['id', 'name', 'age']) + equal: false, leq: true, join: [['id'], ['name', 'age', 'score']], meet: [['id', 'name'], ['age']], widen: [[], Top], narrow: [['id', 'name'], ['age']] }); assertAbstractDomain(create, [['id'], []], [[], ['name', 'age']], { - equal: false, leq: false, join: [[], ['id', 'name', 'age']], meet: Bottom, widen: [[], Top], narrow: Bottom, concrete: concrete(['id']) + equal: false, leq: false, join: [[], ['id', 'name', 'age']], meet: Bottom, widen: [[], Top], narrow: Bottom }); assertAbstractDomain(create, [[], ['name', 'age']], [['id'], []], { - equal: false, leq: false, join: [[], ['id', 'name', 'age']], meet: Bottom, widen: [[], Top], narrow: Bottom, concrete: concrete([], ['name'], ['age'], ['name', 'age']) + equal: false, leq: false, join: [[], ['id', 'name', 'age']], meet: Bottom, widen: [[], Top], narrow: Bottom }); assertAbstractDomain(create, [['id', 'name'], Top], [['id'], []], { - equal: false, leq: false, join: [['id'], Top], meet: Bottom, widen: [[], Top], narrow: Bottom, concrete: Top, abstract: [[], Top] + equal: false, leq: false, join: [['id'], Top], meet: Bottom, widen: [[], Top], narrow: Bottom }); assertAbstractDomain(create, [['id'], []], [['id', 'name'], Top], { - equal: false, leq: false, join: [['id'], Top], meet: Bottom, widen: [['id'], Top], narrow: Bottom, concrete: concrete(['id']) + equal: false, leq: false, join: [['id'], Top], meet: Bottom, widen: [['id'], Top], narrow: Bottom }); assertAbstractDomain(create, [['id'], Top], [['id', 'name'], ['age']], { - equal: false, leq: false, join: [['id'], Top], meet: [['id', 'name'], ['age']], widen: [['id'], Top], narrow: [['id'], ['name', 'age']], concrete: Top, abstract: [[], Top] + equal: false, leq: false, join: [['id'], Top], meet: [['id', 'name'], ['age']], widen: [['id'], Top], narrow: [['id'], ['name', 'age']] }); assertAbstractDomain(create, [['id', 'name'], ['age']], [['id'], Top], { - equal: false, leq: true, join: [['id'], Top], meet: [['id', 'name'], ['age']], widen: [[], Top], narrow: [['id', 'name'], ['age']], concrete: concrete(['id', 'name'], ['id', 'name', 'age']) + equal: false, leq: true, join: [['id'], Top], meet: [['id', 'name'], ['age']], widen: [[], Top], narrow: [['id', 'name'], ['age']] }); assertAbstractDomain(create, [[], Top], [['id'], ['name', 'age']], { - equal: false, leq: false, join: [[], Top], meet: [['id'], ['name', 'age']], widen: [[], Top], narrow: [['id'], ['name', 'age']], concrete: Top, abstract: [[], Top] + equal: false, leq: false, join: [[], Top], meet: [['id'], ['name', 'age']], widen: [[], Top], narrow: [['id'], ['name', 'age']] }); assertAbstractDomain(create, [['id'], ['name', 'age']], [[], Top], { - equal: false, leq: true, join: [[], Top], meet: [['id'], ['name', 'age']], widen: [[], Top], narrow: [['id'], ['name', 'age']], concrete: concrete(['id'], ['id', 'name'], ['id', 'age'], ['id', 'name', 'age']) + equal: false, leq: true, join: [[], Top], meet: [['id'], ['name', 'age']], widen: [[], Top], narrow: [['id'], ['name', 'age']] }); }); const intervalTests = [{ name: 'Interval Domain', - create: (value: AbstractValue) => new IntervalDomain(value), + create: (value: IntervalLift) => new IntervalDomain(value), min: IntervalTop[0], max: IntervalTop[1] }, { name: 'Positive Interval Domain', - create: (value: AbstractValue) => new PosIntervalDomain(value), + create: (value: PosIntervalLift) => new PosIntervalDomain(value), min: PosIntervalTop[0], max: PosIntervalTop[1] }]; @@ -203,103 +199,103 @@ describe('Abstract Domains', () => { for(const { name, create, min, max } of intervalTests) { describe(name, () => { assertAbstractDomain(create, Bottom, Bottom, { - equal: true, leq: true, join: Bottom, meet: Bottom, widen: Bottom, narrow: Bottom, concrete: [] + equal: true, leq: true, join: Bottom, meet: Bottom, widen: Bottom, narrow: Bottom }); assertAbstractDomain(create, [min, max], [min, max], { - equal: true, leq: true, join: [min, max], meet: [min, max], widen: [min, max], narrow: [min, max], concrete: Top + equal: true, leq: true, join: [min, max], meet: [min, max], widen: [min, max], narrow: [min, max] }); assertAbstractDomain(create, Bottom, [min, max], { - equal: false, leq: true, join: [min, max], meet: Bottom, widen: [min, max], narrow: Bottom, concrete: [] + equal: false, leq: true, join: [min, max], meet: Bottom, widen: [min, max], narrow: Bottom }); assertAbstractDomain(create, [min, max], Bottom, { - equal: false, leq: false, join: [min, max], meet: Bottom, widen: [min, max], narrow: Bottom, concrete: Top + equal: false, leq: false, join: [min, max], meet: Bottom, widen: [min, max], narrow: Bottom }); assertAbstractDomain(create, Bottom, [2, 2], { - equal: false, leq: true, join: [2, 2], meet: Bottom, widen: [2, 2], narrow: Bottom, concrete: [] + equal: false, leq: true, join: [2, 2], meet: Bottom, widen: [2, 2], narrow: Bottom }); assertAbstractDomain(create, [2, 2], Bottom, { - equal: false, leq: false, join: [2, 2], meet: Bottom, widen: [2, 2], narrow: Bottom, concrete: [2] + equal: false, leq: false, join: [2, 2], meet: Bottom, widen: [2, 2], narrow: Bottom }); assertAbstractDomain(create, Bottom, [2, 8], { - equal: false, leq: true, join: [2, 8], meet: Bottom, widen: [2, 8], narrow: Bottom, concrete: [] + equal: false, leq: true, join: [2, 8], meet: Bottom, widen: [2, 8], narrow: Bottom }); assertAbstractDomain(create, [2, 8], Bottom, { - equal: false, leq: false, join: [2, 8], meet: Bottom, widen: [2, 8], narrow: Bottom, concrete: [2, 3, 4, 5, 6, 7, 8] + equal: false, leq: false, join: [2, 8], meet: Bottom, widen: [2, 8], narrow: Bottom }); assertAbstractDomain(create, [2, 8], [2, 8], { - equal: true, leq: true, join: [2, 8], meet: [2, 8], widen: [2, 8], narrow: [2, 8], concrete: [2, 3, 4, 5, 6, 7, 8] + equal: true, leq: true, join: [2, 8], meet: [2, 8], widen: [2, 8], narrow: [2, 8] }); assertAbstractDomain(create, [0, 4], [2, 8], { - equal: false, leq: false, join: [0, 8], meet: [2, 4], widen: [0, max], narrow: [min === 0 ? 2 : 0, 4], concrete: [0, 1, 2, 3, 4] + equal: false, leq: false, join: [0, 8], meet: [2, 4], widen: [0, max], narrow: [min === 0 ? 2 : 0, 4] }); assertAbstractDomain(create, [2, 8], [0, 4], { - equal: false, leq: false, join: [0, 8], meet: [2, 4], widen: [min, 8], narrow: [2, 8], concrete: [2, 3, 4, 5, 6, 7, 8] + equal: false, leq: false, join: [0, 8], meet: [2, 4], widen: [min, 8], narrow: [2, 8] }); assertAbstractDomain(create, [0, 0], [1, 3], { - equal: false, leq: false, join: [0, 3], meet: Bottom, widen: [0, max], narrow: Bottom, concrete: [0] + equal: false, leq: false, join: [0, 3], meet: Bottom, widen: [0, max], narrow: Bottom }); assertAbstractDomain(create, [1, 3], [0, 0], { - equal: false, leq: false, join: [0, 3], meet: Bottom, widen: [min, 3], narrow: Bottom, concrete: [1, 2, 3] + equal: false, leq: false, join: [0, 3], meet: Bottom, widen: [min, 3], narrow: Bottom }); assertAbstractDomain(create, [2, 8], [4, 12], { - equal: false, leq: false, join: [2, 12], meet: [4, 8], widen: [2, max], narrow: [2, 8], concrete: [2, 3, 4, 5, 6, 7, 8] + equal: false, leq: false, join: [2, 12], meet: [4, 8], widen: [2, max], narrow: [2, 8] }); assertAbstractDomain(create, [4, 12], [2, 8], { - equal: false, leq: false, join: [2, 12], meet: [4, 8], widen: [min, 12], narrow: [4, 12], concrete: [4, 5, 6, 7, 8, 9, 10, 11, 12] + equal: false, leq: false, join: [2, 12], meet: [4, 8], widen: [min, 12], narrow: [4, 12] }); assertAbstractDomain(create, [2, 8], [8, max], { - equal: false, leq: false, join: [2, max], meet: [8, 8], widen: [2, max], narrow: [2, 8], concrete: [2, 3, 4, 5, 6, 7, 8] + equal: false, leq: false, join: [2, max], meet: [8, 8], widen: [2, max], narrow: [2, 8] }); assertAbstractDomain(create, [8, max], [2, 8], { - equal: false, leq: false, join: [2, max], meet: [8, 8], widen: [min, max], narrow: [8, 8], concrete: Top, abstract: [min, max] + equal: false, leq: false, join: [2, max], meet: [8, 8], widen: [min, max], narrow: [8, 8] }); assertAbstractDomain(create, [2, 8], [2, 4], { - equal: false, leq: false, join: [2, 8], meet: [2, 4], widen: [2, 8], narrow: [2, 8], concrete: [2, 3, 4, 5, 6, 7, 8] + equal: false, leq: false, join: [2, 8], meet: [2, 4], widen: [2, 8], narrow: [2, 8] }); assertAbstractDomain(create, [2, 4], [2, 8], { - equal: false, leq: true, join: [2, 8], meet: [2, 4], widen: [2, max], narrow: [2, 4], concrete: [2, 3, 4] + equal: false, leq: true, join: [2, 8], meet: [2, 4], widen: [2, max], narrow: [2, 4] }); assertAbstractDomain(create, [2, 8], [2, 2], { - equal: false, leq: false, join: [2, 8], meet: [2, 2], widen: [2, 8], narrow: [2, 8], concrete: [2, 3, 4, 5, 6, 7, 8] + equal: false, leq: false, join: [2, 8], meet: [2, 2], widen: [2, 8], narrow: [2, 8] }); assertAbstractDomain(create, [2, 2], [2, 8], { - equal: false, leq: true, join: [2, 8], meet: [2, 2], widen: [2, max], narrow: [2, 2], concrete: [2] + equal: false, leq: true, join: [2, 8], meet: [2, 2], widen: [2, max], narrow: [2, 2] }); assertAbstractDomain(create, [2, 8], [0, 0], { - equal: false, leq: false, join: [0, 8], meet: Bottom, widen: [min, 8], narrow: Bottom, concrete: [2, 3, 4, 5, 6, 7, 8] + equal: false, leq: false, join: [0, 8], meet: Bottom, widen: [min, 8], narrow: Bottom }); assertAbstractDomain(create, [0, 0], [2, 8], { - equal: false, leq: false, join: [0, 8], meet: Bottom, widen: [0, max], narrow: Bottom, concrete: [0] + equal: false, leq: false, join: [0, 8], meet: Bottom, widen: [0, max], narrow: Bottom }); assertAbstractDomain(create, [2, 8], [10, 12], { - equal: false, leq: false, join: [2, 12], meet: Bottom, widen: [2, max], narrow: Bottom, concrete: [2, 3, 4, 5, 6, 7, 8] + equal: false, leq: false, join: [2, 12], meet: Bottom, widen: [2, max], narrow: Bottom }); assertAbstractDomain(create, [10, 12], [2, 8], { - equal: false, leq: false, join: [2, 12], meet: Bottom, widen: [min, 12], narrow: Bottom, concrete: [10, 11, 12] + equal: false, leq: false, join: [2, 12], meet: Bottom, widen: [min, 12], narrow: Bottom }); assertAbstractDomain(create, [0, 0], [12, max], { - equal: false, leq: false, join: [0, max], meet: Bottom, widen: [0, max], narrow: Bottom, concrete: [0] + equal: false, leq: false, join: [0, max], meet: Bottom, widen: [0, max], narrow: Bottom }); assertAbstractDomain(create, [12, max], [0, 0], { - equal: false, leq: false, join: [0, max], meet: Bottom, widen: [min, max], narrow: Bottom, concrete: Top, abstract: [min, max] + equal: false, leq: false, join: [0, max], meet: Bottom, widen: [min, max], narrow: Bottom }); assertAbstractDomain(create, [4, max], [12, max], { - equal: false, leq: false, join: [4, max], meet: [12, max], widen: [4, max], narrow: [4, max], concrete: Top, abstract: [min, max] + equal: false, leq: false, join: [4, max], meet: [12, max], widen: [4, max], narrow: [4, max] }); assertAbstractDomain(create, [12, max], [4, max], { - equal: false, leq: true, join: [4, max], meet: [12, max], widen: [min, max], narrow: [12, max], concrete: Top, abstract: [min, max] + equal: false, leq: true, join: [4, max], meet: [12, max], widen: [min, max], narrow: [12, max] }); assertAbstractDomain(create, [2, 8], [min, max], { - equal: false, leq: true, join: [min, max], meet: [2, 8], widen: [min, max], narrow: [2, 8], concrete: [2, 3, 4, 5, 6, 7, 8] + equal: false, leq: true, join: [min, max], meet: [2, 8], widen: [min, max], narrow: [2, 8] }); assertAbstractDomain(create, [min, max], [2, 8], { - equal: false, leq: false, join: [min, max], meet: [2, 8], widen: [min, max], narrow: [2, 8], concrete: Top + equal: false, leq: false, join: [min, max], meet: [2, 8], widen: [min, max], narrow: [2, 8] }); assertAbstractDomain(create, [12, max], [min, max], { - equal: false, leq: true, join: [min, max], meet: [12, max], widen: [min, max], narrow: [12, max], concrete: Top, abstract: [min, max] + equal: false, leq: true, join: [min, max], meet: [12, max], widen: [min, max], narrow: [12, max] }); assertAbstractDomain(create, [min, max], [12, max], { - equal: false, leq: false, join: [min, max], meet: [12, max], widen: [min, max], narrow: [12, max], concrete: Top + equal: false, leq: false, join: [min, max], meet: [12, max], widen: [min, max], narrow: [12, max] }); }); }