feat: closed pentagon domain - Implemented closed pentagon domain

src/abstract-interpretation/interval/closed-pentagon-domain.ts

@@ -0,0 +1,72 @@
+import { IntervalDomain } from '../domains/interval-domain';
+import { UpperBoundsDomain } from './upper-bounds-domain';
+import { ProductDomain } from '../domains/product-domain';
+import type { NodeId } from '../../r-bridge/lang-4.x/ast/model/processing/node-id';
+import { StateAbstractDomain } from '../domains/state-abstract-domain';
+
+/** The type of the abstract product representing the closed pentagon */
+export type AbstractClosedPentagon = {
+	interval:    StateAbstractDomain<IntervalDomain>;
+	upperBounds: UpperBoundsDomain;
+};
+
+/**
+ * The closed pentagon domain as reduced product domain of an interval state domain and a weakly relational upper bounds domain.
+ */
+export class ClosedPentagonDomain extends ProductDomain<AbstractClosedPentagon> {
+	public create(value: AbstractClosedPentagon): this;
+	public create(value: AbstractClosedPentagon): ClosedPentagonDomain {
+		return new ClosedPentagonDomain(value);
+	}
+
+	/**
+	 * The current abstract value of the interval state domain.
+	 */
+	public get interval(): AbstractClosedPentagon['interval'] {
+		return this.value.interval;
+	}
+
+	/**
+	 * The current abstract value of the upper bounds domain.
+	 */
+	public get upperBounds(): AbstractClosedPentagon['upperBounds'] {
+		return this.value.upperBounds;
+	}
+
+	public static top(): ClosedPentagonDomain {
+		return new ClosedPentagonDomain({ interval: StateAbstractDomain.top(IntervalDomain.top()), upperBounds: UpperBoundsDomain.top() });
+	}
+
+	public static bottom(): ClosedPentagonDomain {
+		return new ClosedPentagonDomain({ interval: StateAbstractDomain.bottom(IntervalDomain.bottom()), upperBounds: UpperBoundsDomain.bottom() });
+	}
+
+	protected override reduce(value: AbstractClosedPentagon): AbstractClosedPentagon {
+		if(value.interval.isTop() && value.upperBounds.isTop()) {
+			return value;
+		}
+		if(value.interval.isBottom() || value.upperBounds.isBottom()) {
+			return { interval: StateAbstractDomain.bottom(IntervalDomain.bottom()), upperBounds: UpperBoundsDomain.bottom() };
+		}
+		if(value.interval.isValue() && value.upperBounds.isValue()) {
+			const allKeys = new Set<NodeId>([...value.interval.value.keys(), ...value.upperBounds.value.keys()]);
+
+			for(const key of allKeys) {
+				const inferredUpperBounds = new Set<NodeId>();
+				for(const otherKey of allKeys){
+					const keyInterval = value.interval.get(key);
+					const otherKeyInterval = value.interval.get(otherKey);
+					if(keyInterval?.isValue() && otherKeyInterval?.isValue() && keyInterval.value[1] <= otherKeyInterval.value[0]) {
+						inferredUpperBounds.add(otherKey);
+					}
+				}
+
+				const prevUpperBounds = value.upperBounds.value.get(key) ?? new Set();
+				const newUpperBounds = prevUpperBounds.union(inferredUpperBounds);
+
+				(value.upperBounds.value as Map<NodeId, ReadonlySet<NodeId>>).set(key, newUpperBounds);
+			}
+		}
+		return value;
+	}
+}

src/abstract-interpretation/interval/upper-bounds-domain.ts

@@ -0,0 +1,260 @@
+import type { NodeId } from '../../r-bridge/lang-4.x/ast/model/processing/node-id';
+import { Bottom, BottomSymbol, Top } from '../domains/lattice';
+import { AbstractDomain } from '../domains/abstract-domain';
+import { isNotUndefined, isUndefined } from '../../util/assert';
+import { setEquals } from '../../util/collections/set';
+
+/** The type of the actual values of the upper bounds domain as mapping from NodeId to all NodeIds that are greater or equal */
+type UpperBoundsValue = ReadonlyMap<NodeId, ReadonlySet<NodeId>>;
+/** The type of the Top element of the upper bounds domain as empty mapping from NodeId to NodeIds */
+type UpperBoundsTop = ReadonlyMap<NodeId, never>;
+/** The type of the Bottom element of the upper bounds domain as {@link Bottom} symbol */
+type UpperBoundsBottom = typeof Bottom;
+/** The type of the abstract values of the upper bounds domain that are Top, Bottom, or actual values */
+type UpperBoundsLift = UpperBoundsValue | UpperBoundsBottom;
+
+/**
+ * A weakly relational abstract domain that maps NodeIds to a set of all NodeIds that are associated with greater or equal values.
+ * The Bottom element is defined as {@link Bottom} symbol and the Top element as empty mapping.
+ * @template Value - Type of the abstract elements of the abstract domain (extends the UpperBoundsLift)
+ */
+export class UpperBoundsDomain<Value extends UpperBoundsLift = UpperBoundsLift> extends AbstractDomain<ReadonlyMap<NodeId, number>, UpperBoundsValue, UpperBoundsTop, UpperBoundsBottom, Value> {
+	constructor(value: Value) {
+		if(value === Bottom) {
+			super(Bottom as Value);
+		} else {
+			super(new Map(value.entries().map(([key, value]) => [key, new Set(value)])) as UpperBoundsValue as Value);
+		}
+	}
+
+	public create(value: Value): this;
+	public create(value: Value): UpperBoundsDomain {
+		return new UpperBoundsDomain(value);
+	}
+
+	/**
+	 * Sets the upper bounds for the provided key if the domain is not Bottom.
+	 * @param key - The node to set the upper bounds for.
+	 * @param value - The upper bounds of the node.
+	 * @private
+	 */
+	private setBounds(key: NodeId, value: ReadonlySet<NodeId>): void {
+		if(this.value !== Bottom) {
+			(this.value as Map<NodeId, ReadonlySet<NodeId>>).set(key, value);
+		}
+	}
+
+	/**
+	 * Removes the upper bounds for the provided key if the domain is not Bottom.
+	 * @param key - The node to remove the upper bounds for.
+	 * @private
+	 */
+	private removeBounds(key: NodeId): void {
+		if(this.value !== Bottom) {
+			(this.value as Map<NodeId, ReadonlySet<NodeId>>).delete(key);
+		}
+	}
+
+	/**
+	 * Retrieves the upper bounds for the provided key or undefined if the domain is Bottom.
+	 * Assures that the key is part of the returned set (as x &leq; x always holds).
+	 * @param key - The node to receive the upper bounds for.
+	 * @private
+	 */
+	private getBounds(key: NodeId): ReadonlySet<NodeId> | undefined {
+		if(this.value === Bottom) {
+			return undefined;
+		}
+		return this.value.get(key)?.union(new Set([key])) ?? new Set([key]);
+	}
+
+	public static top(): UpperBoundsDomain<UpperBoundsTop> {
+		return new UpperBoundsDomain(new Map<NodeId, never>());
+	}
+
+	public static bottom(): UpperBoundsDomain<UpperBoundsBottom> {
+		return new UpperBoundsDomain(Bottom);
+	}
+
+	public top(): this & UpperBoundsDomain<UpperBoundsTop>;
+	public top(): UpperBoundsDomain<UpperBoundsTop> {
+		return UpperBoundsDomain.top();
+	}
+
+	public bottom(): this & UpperBoundsDomain<UpperBoundsBottom>;
+	public bottom(): UpperBoundsDomain<UpperBoundsBottom> {
+		return UpperBoundsDomain.bottom();
+	}
+
+	public equals(other: this): boolean {
+		if(this.value === other.value){
+			return true;
+		} else if(this.value === Bottom || other.value === Bottom) {
+			return false;
+		}
+
+		const allKeys = new Set<NodeId>([...this.value.keys(), ...other.value.keys()]);
+		for(const key of allKeys){
+			const thisBounds = this.getBounds(key);
+			const otherBounds = other.getBounds(key);
+			if(isUndefined(thisBounds) || isUndefined(otherBounds) || !setEquals(thisBounds, otherBounds)) {
+				return false;
+			}
+		}
+
+		return true;
+	}
+
+	public leq(other: this): boolean {
+		if(this.value === Bottom){
+			return true;
+		} else if(other.value === Bottom){
+			return false;
+		}
+
+		for(const [key, otherValue] of other.value.entries()) {
+			const thisValue = this.getBounds(key);
+			if(isNotUndefined(thisValue) && !otherValue.isSubsetOf(thisValue)) {
+				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 & UpperBoundsDomain<UpperBoundsValue>;
+
+		for(const key of result.value.keys()) {
+			if(!other.value.has(key)) {
+				result.removeBounds(key);
+			}
+		}
+		for(const [key, value] of other.value.entries()) {
+			const currValue = result.value.get(key);
+
+			if(isNotUndefined(currValue)) {
+				result.setBounds(key, currValue.intersection(value));
+			}
+		}
+		return result;
+	}
+
+	public meet(other: this): this {
+		if(this.value === Bottom || other.value === Bottom) {
+			return this.bottom();
+		}
+		const result = this.create(this.value) as this & UpperBoundsDomain<UpperBoundsValue>;
+
+		for(const [key, value] of other.value.entries()) {
+			const currValue = result.value.get(key);
+
+			if(isUndefined(currValue)) {
+				result.setBounds(key, value);
+			} else {
+				result.setBounds(key, currValue.union(value));
+			}
+		}
+		return 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.top() as this & UpperBoundsDomain<UpperBoundsValue>;
+		const allKeys = new Set<NodeId>([...this.value.keys(), ...other.value.keys()]);
+
+		for(const key of allKeys.values()) {
+			const thisValue = this.getBounds(key);
+			const otherValue = other.getBounds(key);
+
+			if(isNotUndefined(thisValue) && isNotUndefined(otherValue) && otherValue.isSubsetOf(thisValue)) {
+				result.setBounds(key, otherValue);
+			}
+		}
+		return result;
+	}
+
+	public narrow(_other: this): this {
+		throw new Error('Not Implemented');
+	}
+
+	public concretize(_limit: number): ReadonlySet<ReadonlyMap<NodeId, number>> | typeof Top {
+		if(this.value === Bottom) {
+			return new Set();
+		}
+		return Top;
+	}
+
+	public abstract(concrete: ReadonlySet<ReadonlyMap<NodeId, number>> | typeof Top): this {
+		if(concrete === Top) {
+			return this.top();
+		}
+		if(concrete.size === 0){
+			return this.bottom();
+		}
+		const allNodeIds = new Set<NodeId>();
+		for(const map of concrete.values()) {
+			for(const key of map.keys()) {
+				allNodeIds.add(key);
+			}
+		}
+		const result = this.top() as this & UpperBoundsDomain<UpperBoundsValue>;
+
+		for(const nodeIdA of allNodeIds.values()) {
+			for(const nodeIdB of allNodeIds.values()) {
+				if(nodeIdA === nodeIdB){
+					continue;
+				}
+
+				if(concrete.values().every(map => {
+					const valueA = map.get(nodeIdA);
+					const valueB = map.get(nodeIdB);
+
+					return isNotUndefined(valueA) && isNotUndefined(valueB) && valueA <= valueB;
+				})) {
+					const currentValue = result.value.get(nodeIdA);
+					if(isNotUndefined(currentValue)) {
+						result.setBounds(nodeIdA, currentValue.union(new Set([nodeIdB])));
+					} else {
+						result.setBounds(nodeIdA, new Set([nodeIdB]));
+					}
+				}
+			}
+		}
+		return result;
+	}
+
+	public toJson(): unknown {
+		if(this.value === Bottom){
+			return this.value.description;
+		}
+		return Object.fromEntries(this.value.entries().map(([key, value]) => [key, [...value]]));
+	}
+
+	public toString(): string {
+		if(this.value === Bottom) {
+			return BottomSymbol;
+		}
+		return '(' + this.value.entries().map(([key, value]) => `${key} -> {${value.values().map(id => id.toString()).toArray().join(', ')}}`).toArray().join(', ') + ')';
+	}
+
+	public isTop(): this is this & UpperBoundsDomain<UpperBoundsTop> {
+		return this.value !== Bottom && this.value.entries().every(([key, value]) => value.size === 0 || (value.size === 1 && value.has(key)));
+	}
+
+	public isBottom(): this is this & UpperBoundsDomain<UpperBoundsBottom> {
+		return this.value == Bottom;
+	}
+
+	public isValue(): this is this & UpperBoundsDomain<UpperBoundsValue> {
+		return this.value !== Bottom;
+	}
+}

test/functionality/abstract-interpretation/domains/domain.ts

@@ -1,5 +1,9 @@
 import { assert, test } from 'vitest';
-import { DEFAULT_INFERENCE_LIMIT, type AnyAbstractDomain, type ConcreteDomain } from '../../../../src/abstract-interpretation/domains/abstract-domain';
+import {
+	type AnyAbstractDomain,
+	type ConcreteDomain,
+	DEFAULT_INFERENCE_LIMIT
+} from '../../../../src/abstract-interpretation/domains/abstract-domain';
 import { Top, TopSymbol } from '../../../../src/abstract-interpretation/domains/lattice';
 
 export interface DomainTestExpectation<AbstractValue, ConcreteValue>{
@@ -8,7 +12,7 @@ export interface DomainTestExpectation<AbstractValue, ConcreteValue>{
 	readonly join:      AbstractValue,
 	readonly meet:      AbstractValue,
 	readonly widen:     AbstractValue,
-	readonly narrow:    AbstractValue,
+	readonly narrow?:   AbstractValue,
 	readonly concrete?: ConcreteValue[] | typeof Top,
 	readonly abstract?: AbstractValue
 }
@@ -28,7 +32,7 @@ export function assertAbstractDomain<AbstractValue, Domain extends AnyAbstractDo
 	const join = create(expected.join);
 	const meet = create(expected.meet);
 	const widen = create(expected.widen);
-	const narrow = create(expected.narrow);
+	const narrow = create(expected.narrow ?? value1);
 	const concrete = expected.concrete === Top ? Top : new Set(expected.concrete);
 	const abstract = create(expected.abstract ?? value1);
 
@@ -58,12 +62,14 @@ export function assertAbstractDomain<AbstractValue, Domain extends AnyAbstractDo
 		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.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()}`);
+		});
+	}
 	if(expected.concrete) {
 		test(`γ(${domain1.toString()})`, () => {
 			assert.deepStrictEqual(domain1.concretize(DEFAULT_INFERENCE_LIMIT), concrete, `expected ${toString(concrete)} but was ${toString(domain1.concretize(DEFAULT_INFERENCE_LIMIT))}`);