Integrate the new structure of abstract domains

src/abstract-interpretation/data-frame/absint-info.ts

@@ -1,7 +1,7 @@
 import type { RNode } from '../../r-bridge/lang-4.x/ast/model/model';
 import type { ParentInformation } from '../../r-bridge/lang-4.x/ast/model/processing/decorate';
 import type { NodeId } from '../../r-bridge/lang-4.x/ast/model/processing/node-id';
-import type { DataFrameStateDomain } from './domain';
+import type { DataFrameStateDomain } from './dataframe-domain';
 import type { ConstraintType, DataFrameOperationArgs, DataFrameOperationName, DataFrameOperationOptions } from './semantics';
 
 /**

src/abstract-interpretation/data-frame/absint-visitor.ts

@@ -9,8 +9,7 @@ import type { NormalizedAst, ParentInformation } from '../../r-bridge/lang-4.x/a
 import type { NodeId } from '../../r-bridge/lang-4.x/ast/model/processing/node-id';
 import { isNotUndefined } from '../../util/assert';
 import { DataFrameInfoMarker, hasDataFrameAssignmentInfo, hasDataFrameExpressionInfo, hasDataFrameInfoMarker, type AbstractInterpretationInfo } from './absint-info';
-import type { DataFrameDomain, DataFrameStateDomain } from './domain';
-import { DataFrameTop, equalDataFrameState, joinDataFrameStates, wideningDataFrameStates } from './domain';
+import { DataFrameDomain, DataFrameStateDomain } from './dataframe-domain';
 import { mapDataFrameAccess } from './mappers/access-mapper';
 import { isAssignmentTarget, mapDataFrameVariableAssignment } from './mappers/assignment-mapper';
 import { mapDataFrameFunctionCall } from './mappers/function-mapper';
@@ -39,12 +38,12 @@ export class DataFrameShapeInferenceVisitor<
 	 * The old domain of an AST node before processing the node retrieved from the attached {@link AbstractInterpretationInfo}.
 	 * This is used to check whether the state has changed and successors should be visited again, and is also required for widening.
 	 */
-	private oldDomain: DataFrameStateDomain = new Map();
+	private oldDomain = DataFrameStateDomain.bottom();
 	/**
 	 * The new domain of an AST node during and after processing the node.
 	 * This information is stored in the {@link AbstractInterpretationInfo} afterward.
 	 */
-	private newDomain: DataFrameStateDomain = new Map();
+	private newDomain = DataFrameStateDomain.bottom();
 
 	constructor(config: Config) {
 		super({ ...config, defaultVisitingOrder: 'forward', defaultVisitingType: 'exit' });
@@ -58,14 +57,15 @@ export class DataFrameShapeInferenceVisitor<
 			return true;
 		}
 		const predecessors = this.getPredecessorNodes(vertex.id);
-		this.newDomain = joinDataFrameStates(...predecessors.map(node => node.info.dataFrame?.domain ?? new Map<NodeId, DataFrameDomain>()));
+		const predecessorDomains = predecessors.map(node => node.info.dataFrame?.domain ?? DataFrameStateDomain.bottom());
+		this.newDomain = DataFrameStateDomain.bottom().join(...predecessorDomains);
 		this.onVisitNode(nodeId);
 
 		const visitedCount = this.visited.get(vertex.id) ?? 0;
 		this.visited.set(vertex.id, visitedCount + 1);
 
 		// only continue visiting if the node has not been visited before or the data frame value of the node changed
-		return visitedCount === 0 || !equalDataFrameState(this.oldDomain, this.newDomain);
+		return visitedCount === 0 || !this.oldDomain.equals(this.newDomain);
 	}
 
 	protected override visitDataflowNode(vertex: Exclude<CfgSimpleVertex, CfgBasicBlockVertex>): void {
@@ -74,11 +74,11 @@ export class DataFrameShapeInferenceVisitor<
 		if(node === undefined) {
 			return;
 		}
-		this.oldDomain = node.info.dataFrame?.domain ?? new Map<NodeId, DataFrameDomain>();
+		this.oldDomain = node.info.dataFrame?.domain ?? DataFrameStateDomain.bottom();
 		super.visitDataflowNode(vertex);
 
 		if(this.shouldWiden(vertex)) {
-			this.newDomain = wideningDataFrameStates(this.oldDomain, this.newDomain);
+			this.newDomain = this.oldDomain.widen(this.newDomain);
 		}
 		node.info.dataFrame ??= {};
 		node.info.dataFrame.domain = this.newDomain;
@@ -142,12 +142,12 @@ export class DataFrameShapeInferenceVisitor<
 		const value = resolveIdToDataFrameShape(node.info.dataFrame.expression, this.config.dfg, this.newDomain);
 
 		if(value !== undefined) {
-			this.newDomain.set(node.info.dataFrame.identifier, value);
+			this.newDomain.value.set(node.info.dataFrame.identifier, value);
 			const identifier = this.getNormalizedAst(node.info.dataFrame.identifier);
 
 			if(identifier !== undefined) {
 				identifier.info.dataFrame ??= {};
-				identifier.info.dataFrame.domain = new Map(this.newDomain);
+				identifier.info.dataFrame.domain = this.newDomain.create(this.newDomain.value);
 			}
 		}
 	}
@@ -156,21 +156,22 @@ export class DataFrameShapeInferenceVisitor<
 		if(!hasDataFrameExpressionInfo(node)) {
 			return;
 		}
-		let value: DataFrameDomain = DataFrameTop;
+		const maxColNames = this.config.flowrConfig.abstractInterpretation.dataFrame.maxColNames;
+		let value = DataFrameDomain.top(maxColNames);
 
 		for(const { operation, operand, type, options, ...args } of node.info.dataFrame.operations) {
 			const operandValue = operand !== undefined ? resolveIdToDataFrameShape(operand, this.config.dfg, this.newDomain) : value;
-			value = applyDataFrameSemantics(operation, operandValue ?? DataFrameTop, args, options);
+			value = applyDataFrameSemantics(operation, operandValue ?? DataFrameDomain.top(maxColNames), args, options);
 			const constraintType = type ?? getConstraintType(operation);
 
 			if(operand !== undefined && constraintType === ConstraintType.OperandModification) {
-				this.newDomain.set(operand, value);
+				this.newDomain.value.set(operand, value);
 
 				for(const origin of getVariableOrigins(operand, this.config.dfg)) {
-					this.newDomain.set(origin.info.id, value);
+					this.newDomain.value.set(origin.info.id, value);
 				}
 			} else if(constraintType === ConstraintType.ResultPostcondition) {
-				this.newDomain.set(node.info.id, value);
+				this.newDomain.value.set(node.info.id, value);
 			}
 		}
 	}

src/abstract-interpretation/data-frame/dataframe-domain.ts

@@ -1,75 +1,90 @@
-import type { AbstractDomain } from '../domains/abstract-domain';
+import type { NodeId } from '../../r-bridge/lang-4.x/ast/model/processing/node-id';
+import type { AbstractDomainValue } from '../domains/abstract-domain';
 import { PosIntervalDomain } from '../domains/positive-interval-domain';
 import { ProductDomain } from '../domains/product-domain';
-import { SetBoundedSetDomain } from '../domains/set-bounded-set-domain';
+import { SetUpperBoundDomain } from '../domains/set-upper-bound-domain';
 import { StateAbstractDomain } from '../domains/state-abstract-domain';
 
 /** The type of the abstract product representing the shape of data frames */
 export type AbstractDataFrameShape = {
-	colnames: SetBoundedSetDomain<string>;
+	colnames: SetUpperBoundDomain<string>;
 	cols:     PosIntervalDomain;
 	rows:     PosIntervalDomain;
 }
 
-/** The type of abstract values of a sub abstract domain (shape property) of the data frame shape product */
-type DataFrameShapeProperty<Property extends keyof AbstractDataFrameShape> =
-	AbstractDataFrameShape[Property] extends AbstractDomain<unknown, unknown, unknown, unknown, infer Lift> ? Lift : never;
+/** The type of abstract values of a sub abstract domain (shape property) of the data frame shape product domain */
+export type DataFrameShapeProperty<Property extends keyof AbstractDataFrameShape> = AbstractDomainValue<AbstractDataFrameShape[Property]>;
 
 /**
  * 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<AbstractDataFrameShape> {
+export class DataFrameDomain extends ProductDomain<DataFrameDomain, AbstractDataFrameShape> {
 	constructor(value: AbstractDataFrameShape, maxColNames?: number) {
 		super({
-			colnames: new SetBoundedSetDomain(value.colnames.value, maxColNames),
+			colnames: new SetUpperBoundDomain(value.colnames.value, maxColNames ?? value.colnames.limit),
 			cols:     new PosIntervalDomain(value.cols.value),
 			rows:     new PosIntervalDomain(value.rows.value)
 		});
 	}
 
-	public create(value: AbstractDataFrameShape, maxColNames?: number): DataFrameDomain {
-		return new DataFrameDomain(value, maxColNames);
+	public create(value: AbstractDataFrameShape): DataFrameDomain {
+		return new DataFrameDomain(value, this.maxColNames);
 	}
 
 	/**
 	 * The current abstract value of the column names domain.
 	 */
-	public get colnames(): DataFrameShapeProperty<'colnames'> {
-		return this.value.colnames.value;
+	public get colnames(): AbstractDataFrameShape['colnames'] {
+		return this.value.colnames;
 	}
 
 	/**
 	 * The current abstract value of the column count domain.
 	 */
-	public get cols(): DataFrameShapeProperty<'cols'> {
-		return this.value.cols.value;
+	public get cols(): AbstractDataFrameShape['cols'] {
+		return this.value.cols;
 	}
 
 	/**
 	 * The current abstract value of the row count domain.
 	 */
-	public get rows(): DataFrameShapeProperty<'rows'> {
-		return this.value.rows.value;
+	public get rows(): AbstractDataFrameShape['rows'] {
+		return this.value.rows;
+	}
+
+	/**
+	 * The maximum number of inferred column names of the column names domain.
+	 */
+	public get maxColNames(): number {
+		return this.value.colnames.limit;
 	}
 
 	public static bottom(maxColNames?: number): DataFrameDomain {
 		return new DataFrameDomain({
-			colnames: SetBoundedSetDomain.bottom(maxColNames),
+			colnames: SetUpperBoundDomain.bottom(maxColNames),
 			cols:     PosIntervalDomain.bottom(),
 			rows:     PosIntervalDomain.bottom()
 		});
 	}
 
 	public static top(maxColNames?: number): DataFrameDomain {
 		return new DataFrameDomain({
-			colnames: SetBoundedSetDomain.top(maxColNames),
+			colnames: SetUpperBoundDomain.top(maxColNames),
 			cols:     PosIntervalDomain.top(),
 			rows:     PosIntervalDomain.top()
 		});
 	}
 }
 
 /**
- * The data frame state abstract domain as state abstract domain mapping AST node IDs to inferred abstract data frame shapes.
+ * The data frame state abstract domain as state domain mapping AST node IDs to inferred abstract data frame shapes.
  */
-export class DateFrameStateDomain extends StateAbstractDomain<DataFrameDomain> {}
+export class DataFrameStateDomain extends StateAbstractDomain<DataFrameStateDomain, DataFrameDomain> {
+	public create(value: ReadonlyMap<NodeId, DataFrameDomain>): DataFrameStateDomain {
+		return new DataFrameStateDomain(value);
+	}
+
+	public static bottom(): DataFrameStateDomain {
+		return new DataFrameStateDomain(new Map<NodeId, DataFrameDomain>());
+	}
+}